Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.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.

References #

source
noncomputable def MIPStarRE.LDT.Commutativity.gCommOverlapTerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (G : Fq params → SubMeas (Polynomial params) ι) (x : Fq params) :
Error

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

Equations
Instances For
    source
    theorem MIPStarRE.LDT.Commutativity.gCommStability_sliceSSC {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (zeta : Error) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (hself : family.StronglySelfConsistent strategy.state zeta) :
    BipartiteSSCRel strategy.state (uniformDistribution (Fq params)) G (zeta / 2)

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

    source
    theorem MIPStarRE.LDT.Commutativity.evaluatedPointFamily_selfConsistency_of_stronglySelfConsistent {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (zeta : Error) (hself : family.StronglySelfConsistent strategy.state zeta) :
    SDDRel strategy.state (uniformDistribution (Point params.next)) (evaluatedPointFamilyLeft params family) (evaluatedPointFamilyRight 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 MIPStarRE.LDT.Commutativity.gCommStability_pointwise_sum_bound_core {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) (hB_sq : B.total * B.total = B.total) :
    ∑ ab : α × β, ev ψ (leftTensor ((1 - B.total) * A.outcome ab.1 * (1 - B.total)) * rightTensor (B.outcome ab.2)) ≤ ev ψ (leftTensor (1 - B.total) * rightTensor B.total)

    A sandwiched product of two submeasurements is controlled by the overlap of the right-hand total with its complement.

    source
    theorem MIPStarRE.LDT.Commutativity.gCommStability_pointwise_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (G : Fq params → SubMeas (Polynomial params) ι) (hG : ∀ (x : Fq params), G x = (family.meas x).toSubMeas) (q : EvaluatedSliceQuestion params) :
    qSDDOp strategy.state (commDataProcessedGStabilityOneLeft params strategy family G q) (commDataProcessedGStabilityOneRight params strategy family G q) ≤ ev strategy.state (leftTensor (1 - (G (pointHeight params q.2)).total) * rightTensor (G (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 MIPStarRE.LDT.Commutativity.gCommStability_ssc_point {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (G : Fq params → SubMeas (Polynomial params) ι) (x : Fq params) :
    gCommOverlapTerm params strategy G x ≤ qBipartiteSSCDefect strategy.state (G x)

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