Documentation

MIPRE.Background.LIDT.Co.Commutativity.Main.Auxiliary.HEvalTransport

Section 11 commutativity: hEval/closenessOfIP transport #

Evaluated-side closeness-of-IP transport and strong hEval bounds (eq:evaluate-gcom-at-points through eq:don't-understand-the-numbering-system): the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Main/Auxiliary/HEvalTransport.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

Provides the zero-family bounds on the evaluated-slice products, the sharp bound fullSlice_closenessOfIP_CAB_hEval_sqrt and its paper-envelope estimate fullSlice_closenessOfIP_CAB_hEval.

The two zero-family bounds are sum_ev_adjoint_self_leftTensor_mul_le_one of Co/Commutativity/Transport/FullSlice/ZeroBounds.lean applied to the evaluated factors, in place of the vendored Kronecker computation repeated per factor order. The vendored hypothesis hnorm : strategy.state.IsNormalized is dropped from all four lemmas: it is a theorem of the model (VecState.ev_one_of_isNormalized). zeroEvaluatedSliceOpFamily is generic over any type with a zero, as zeroFullSliceOpFamily is: a dependant writes zeroEvaluatedSliceOpFamily (R := K β†’L[β„‚] K) params where the vendored text has (ΞΉ := ΞΉ).

Not ported #

Every declaration of the vendored file has a counterpart here.

References #

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

source
noncomputable def MIPRE.LIDT.Co.Commutativity.zeroEvaluatedSliceOpFamily {R : Type u_3} [Zero R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] :
OpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) R

The zero operator family on the evaluated-slice outcome space.

Equations
Instances For
    source
    theorem MIPRE.LIDT.Co.Commutativity.evaluatedSliceProductLeft_qSDDOp_zero_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace β„‚ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) :
    strategy.state.qSDDOp (evaluatedSliceProductLeft params strategy family q) (zeroEvaluatedSliceOpFamily params) ≀ 1

    Questionwise, the ordered evaluated-slice product has squared distance at most 1 from the zero family.

    source
    theorem MIPRE.LIDT.Co.Commutativity.zero_qSDDOp_evaluatedSliceProductRight_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace β„‚ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) :
    strategy.state.qSDDOp (zeroEvaluatedSliceOpFamily params) (evaluatedSliceProductRight params strategy family q) ≀ 1

    Questionwise, the reversed evaluated-slice product has squared distance at most 1 from the zero family.

    source
    theorem MIPRE.LIDT.Co.Commutativity.fullSlice_closenessOfIP_CAB_hEval_sqrt {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace β„‚ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (hEval : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (evaluatedFromFullSliceProductLeft params strategy family) (evaluatedFromFullSliceProductRight params strategy family) (MIPStarRE.LDT.Commutativity.commDataProcessedGError params gamma zeta)) :
    |evaluatedSliceABAAvg params strategy family - evaluatedSliceABABAvg params strategy family| ≀ √(MIPStarRE.LDT.Commutativity.commDataProcessedGError params gamma zeta)

    Strong evaluated-side hEval transport bound.

    The direct evaluated-side route transports hEval to evaluatedSliceProductLeft/Right, rewrites the resulting SDDOpRel via evaluatedSliceCommutation_qSDDOp_avg_eq, and combines it with the a priori bound sddErrorOp ≀ 4 for the evaluated product families. It yields the sharper estimate |evaluatedSliceABAAvg - evaluatedSliceABABAvg| ≀ √ν, where Ξ½ = commDataProcessedGError params gamma zeta. The paper-envelope estimate fullSlice_closenessOfIP_CAB_hEval below recovers the older 6√΢ + √ν statement when that displayed Section 11 bound is convenient.

    source
    theorem MIPRE.LIDT.Co.Commutativity.fullSlice_closenessOfIP_CAB_hEval {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace β„‚ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (gamma zeta : ℝ) (hEval : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (evaluatedFromFullSliceProductLeft params strategy family) (evaluatedFromFullSliceProductRight params strategy family) (MIPStarRE.LDT.Commutativity.commDataProcessedGError params gamma zeta)) :
    |evaluatedSliceABAAvg params strategy family - evaluatedSliceABABAvg params strategy family| ≀ 6 * √zeta + √(MIPStarRE.LDT.Commutativity.commDataProcessedGError params gamma zeta)

    Combined closenessOfIP chain on the evaluated side (commutativity-G.tex lines 301, 334, 359-360, 394, 396), stated with the paper's displayed 6√΢ + √ν envelope.