Documentation

MIPRE.Background.LIDT.Co.Commutativity.ScalarApproximation.Pointwise

Section 11 commutativity: pointwise scalar approximation #

Pointwise overlap terms ⟨Ψ, (I - G^x) ⊗ G^x Ψ⟩ controlling both sides of the G-stability estimate, used as the base for the averaged scalar bound: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/ScalarApproximation/Pointwise.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The overlap term is strategy.state.ev (strategy.state.L (1 - T) * strategy.state.R T) on the symmetric model of the strategy, and gCommStability_pointwise_sum_bound_core takes the model S : SymModel 𝔓 K as an explicit first argument in place of the vendored state ψ. The vendored hypothesis strategy.permInvState passed to qBipartiteSSCDefect_eq_half_qSDD_of_proj and Preliminaries.twoNotionsOfSelfConsistencyAfterEvaluation is gone with those lemmas' hperm; the one swap use left here is S.ev_L_eq_ev_R in gCommStability_ssc_point, in place of strategy.permInvState.swap_ev.

The proofs are shorter than the vendored ones. The vendored self-adjointness of G^x through Matrix.PosSemidef is IsSelfAdjoint.of_nonneg; the entrywise Kronecker identity (1 - T) ⊗ I = I ⊗ I - T ⊗ I of gCommStability_ssc_point is S.leftTensor_sub and map_one; and the sums over outcomes in gCommStability_pointwise_sum_bound_core and gCommStability_ssc_point collapse through the keystone's opTensor_sum_left_univ and opTensor_sum_right_univ.

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.gCommOverlapTerm {𝔓 : 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) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (x : MIPStarRE.LDT.Fq params) :
ℝ

The common overlap term ⟨Ψ, (I - G^x) ⊗ G^x Ψ⟩ controlling both stability estimates.

Equations
Instances For
    source
    theorem MIPRE.LIDT.Co.Commutativity.gCommStability_sliceSSC {𝔓 : 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) (zeta : ℝ) (family : IdxPolyFamily params 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) (hself : family.StronglySelfConsistent strategy.state zeta) :
    strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) G (zeta / 2)

    The slice self-consistency defect of G is at most zeta / 2.

    source
    theorem MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily_selfConsistency_of_stronglySelfConsistent {𝔓 : 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 𝔓) (zeta : ℝ) (hself : family.StronglySelfConsistent strategy.state zeta) :
    strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) (evaluatedPointFamilyLeft strategy.state params family) (evaluatedPointFamilyRight strategy.state params family) zeta

    Slice strong self-consistency transfers to the evaluated point family.

    The paper invokes the slice self-consistency item after postprocessing a slice measurement by the predicate g(truncatePoint u) = a. This lemma makes that implicit data-processing step explicit: projectivity converts the left/right SDD hypothesis into bipartite strong self-consistency with loss 1/2, question-dependent postprocessing converts it back to left/right SDD with the compensating factor 2, and uniform reindexing Point params.next ≃ Point params × Fq params averages the height coordinate.

    source
    theorem MIPRE.LIDT.Co.Commutativity.gCommStability_pointwise_sum_bound_core {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) (hB_sq : B.total * B.total = B.total) :
    ∑ ab : α × β, S.ev (S.L ((1 - B.total) * A.outcome ab.1 * (1 - B.total)) * S.R (B.outcome ab.2)) ≤ S.ev (S.L (1 - B.total) * S.R B.total)

    A sandwiched product of two submeasurements is controlled by the overlap of the right-hand total with its complement. The vendored state ψ is the symmetric model S.

    source
    theorem MIPRE.LIDT.Co.Commutativity.gCommStability_pointwise_summand_bound {𝔓 : 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 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (ah : MIPStarRE.LDT.Commutativity.StabilityOneOutcome params) :
    strategy.state.ev (strategy.state.L ((1 - (G (MIPStarRE.LDT.pointHeight params q.2)).total) * (star ((evaluatedSliceSandwichRaw params strategy family q).outcome (ah.1, ah.2.toFun (MIPStarRE.LDT.truncatePoint params q.2))) * (evaluatedSliceSandwichRaw params strategy family q).outcome (ah.1, ah.2.toFun (MIPStarRE.LDT.truncatePoint params q.2))) * (1 - (G (MIPStarRE.LDT.pointHeight params q.2)).total)) * strategy.state.R ((G (MIPStarRE.LDT.pointHeight params q.2)).outcome ah.2)) ≤ strategy.state.ev (strategy.state.L ((1 - (G (MIPStarRE.LDT.pointHeight params q.2)).total) * (evaluatedPointFamily params family q.1).outcome ah.1 * (1 - (G (MIPStarRE.LDT.pointHeight params q.2)).total)) * strategy.state.R ((G (MIPStarRE.LDT.pointHeight params q.2)).outcome ah.2))

    A single stability-one summand is controlled by replacing the inner evaluated slice sandwich with the corresponding evaluated point outcome.

    source
    theorem MIPRE.LIDT.Co.Commutativity.gCommStability_pointwise_bound {𝔓 : 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 𝔓) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (hG : ∀ (x : MIPStarRE.LDT.Fq params), G x = (family.meas x).toSubMeas) (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) :
    strategy.state.qSDDOp (commDataProcessedGStabilityOneLeft params strategy family G q) (commDataProcessedGStabilityOneRight params strategy family G q) ≤ strategy.state.ev (strategy.state.L (1 - (G (MIPStarRE.LDT.pointHeight params q.2)).total) * strategy.state.R (G (MIPStarRE.LDT.pointHeight params q.2)).total)

    The full stability-one defect is bounded by the overlap term for the target slice measurement G^y.

    source
    theorem MIPRE.LIDT.Co.Commutativity.gCommStability_ssc_point {𝔓 : 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) (G : MIPStarRE.LDT.Fq params → SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓) (x : MIPStarRE.LDT.Fq params) :
    gCommOverlapTerm params strategy G x ≤ strategy.state.qBipartiteSSCDefect (G x)

    The overlap term at x is bounded by the bipartite SSC defect of G x.