Documentation

MIPStarRE.LDT.Commutativity.Transport.FullSlice.Machinery.Normalization

Full-slice normalization and self-consistency machinery #

Normalization-condition bounds, evaluated projective submeasurements, and full-slice and evaluated-slice self-consistency estimates used by the scalar-to-tensor comparison.

The tensor-form estimates are internal to the scalar/tensor comparison recorded in docs/decisions/713-scalar-tensor-decision.md; downstream code should use the scalar public API exposed by the full-slice transport theorems.

References #

source
theorem MIPStarRE.LDT.Commutativity.normalizationCondition_sandwich_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (P : SubMeas α ι) (Q : ProjSubMeas β ι) :
∑ a : α, (∑ b : β, Q.outcome b * P.outcome a * Q.outcome b) * (∑ b : β, Q.outcome b * P.outcome a * Q.outcome b).conjTranspose ≤ 1

Paper lem:normalization-condition (commutativity-G.tex line 309).

For a sub-measurement P and projective sub-measurement Q, the sandwiched family C_{a,b} = Q_b · P_a · Q_b satisfies the closenessOfIP normalization condition ∑_a (∑_b C_{a,b}) (∑_b C_{a,b})ᴴ ≤ I.

source
noncomputable def MIPStarRE.LDT.Commutativity.evaluateAtProjSubMeas {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (u : Point params) (P : ProjSubMeas (Polynomial params) ι) :
ProjSubMeas (Fq params) ι

Evaluate a polynomial-indexed projective submeasurement at a point, retaining projectivity of the postprocessed outcomes.

This reuses the shared postprocessing projectivity lemma rather than reproving the orthogonality/postprocessing infrastructure locally.

Equations
Instances For
    source
    theorem MIPStarRE.LDT.Commutativity.leftTensor_normalizationCondition_sandwich_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (P : SubMeas α ι) (Q : ProjSubMeas β ι) :
    ∑ a : α, (∑ b : β, leftTensor (Q.outcome b * P.outcome a * Q.outcome b)) * (∑ b : β, leftTensor (Q.outcome b * P.outcome a * Q.outcome b)).conjTranspose ≤ 1

    Tensor-lifted form of normalizationCondition_sandwich_bound, used as the C-normalization hypothesis in closenessOfIP.

    For C_{a,b} = Q_b P_a Q_b ⊗ I, the square-sum condition on the bipartite operator space follows by applying leftTensor to paper lem:normalization-condition.

    source
    theorem MIPStarRE.LDT.Commutativity.leftTensor_normalizationCondition_sandwich_adjoint_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (P : SubMeas α ι) (Q : ProjSubMeas β ι) :
    ∑ a : α, (∑ b : β, leftTensor (Q.outcome b * P.outcome a * Q.outcome b)).conjTranspose * ∑ b : β, leftTensor (Q.outcome b * P.outcome a * Q.outcome b) ≤ 1

    Adjoint-side tensor-lifted normalization condition used with closenessOfIPAdjoint.

    source
    theorem MIPStarRE.LDT.Commutativity.fullSlice_selfConsistency_fst_bound {ι : 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) :
    (avgOver (uniformDistribution (FullSliceQuestion params)) fun (xy : FullSliceQuestion params) => qSDDCore strategy.state (fun (g : Polynomial params) => leftTensor ((family.meas xy.1).outcome g)) fun (g : Polynomial params) => rightTensor ((family.meas xy.1).outcome g)) ≤ zeta

    Full-slice strong self-consistency pulled to the first coordinate of a full-slice question.

    This is the A^x_g = G^x_g ⊗ I, B^x_g = I ⊗ G^x_g input for the closenessOfIP applications in paper commutativity-G.tex line 334.

    source
    theorem MIPStarRE.LDT.Commutativity.fullSlice_selfConsistency_snd_bound {ι : 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) :
    (avgOver (uniformDistribution (FullSliceQuestion params)) fun (xy : FullSliceQuestion params) => qSDDCore strategy.state (fun (h : Polynomial params) => leftTensor ((family.meas xy.2).outcome h)) fun (h : Polynomial params) => rightTensor ((family.meas xy.2).outcome h)) ≤ zeta

    Full-slice strong self-consistency pulled to the second coordinate of a full-slice question.

    source
    theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_selfConsistency_snd_bound {ι : 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) :
    (avgOver (uniformDistribution (EvaluatedSliceQuestion params)) fun (q : EvaluatedSliceQuestion params) => qSDDCore strategy.state (fun (b : Fq params) => leftTensor ((evaluatedSliceSecondFactor params family q).outcome b)) fun (b : Fq params) => rightTensor ((evaluatedSliceSecondFactor params family q).outcome b)) ≤ zeta

    Evaluated-slice point self-consistency pulled to the second coordinate of an evaluated-slice question.

    source
    theorem MIPStarRE.LDT.Commutativity.xEvaluated_selfConsistency_fst_bound {ι : 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) :
    (avgOver (uniformDistribution (Point params × FullSliceQuestion params)) fun (ux : Point params × FullSliceQuestion params) => qSDDCore strategy.state (fun (a : Fq params) => leftTensor ((evaluateAt params ux.1 (family.meas ux.2.1).toSubMeas).outcome a)) fun (a : Fq params) => rightTensor ((evaluateAt params ux.1 (family.meas ux.2.1).toSubMeas).outcome a)) ≤ zeta

    Point-level self-consistency pulled to mixed (u, x, y) data for the already x-evaluated first coordinate.