Section 11 commutativity: product estimates

Basic product-style lemmas on projective submeasurement outcomes — in particular orthogonality of distinct outcomes — reused throughout the Section 11 commutativity argument.

References

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPStarRE.LDT.Commutativity.postprocess_proj_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (P : ProjSubMeas α ι) (f : α → β) (b : β) : (postprocess P.toSubMeas f).outcome b * (postprocess P.toSubMeas f).outcome b = (postprocess P.toSubMeas f).outcome b

Postprocessing a projective submeasurement preserves outcome projectivity.

theorem MIPStarRE.LDT.Commutativity.evaluatedPointFamily_outcome_proj {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) (u : Point params.next) (a : Fq params) : (evaluatedPointFamily params family u).outcome a * (evaluatedPointFamily params family u).outcome a = (evaluatedPointFamily params family u).outcome a

Evaluating a projective polynomial family at a point preserves outcome projectivity.

theorem MIPStarRE.LDT.Commutativity.sqrt_subMeas_outcome_mul_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} [Fintype α] (A : SubMeas α ι) (a : α) : CFC.sqrt (A.outcome a) * CFC.sqrt (A.outcome a) = A.outcome a

The positive square root of a submeasurement outcome squares back to that outcome.

theorem MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityOne_qSDDOp_expand {ι : 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) = ∑ ah : StabilityOneOutcome params, ev strategy.state (leftTensor ((1 - (G (pointHeight params q.2)).total) * (Matrix.conjTranspose ((evaluatedSliceSandwichRaw params strategy family q).outcome (ah.1, ah.2.toFun (truncatePoint params q.2))) * (evaluatedSliceSandwichRaw params strategy family q).outcome (ah.1, ah.2.toFun (truncatePoint params q.2))) * (1 - (G (pointHeight params q.2)).total)) * rightTensor ((G (pointHeight params q.2)).outcome ah.2))

Fixed-question expansion of the first scalar-stability qSDDOp term.

This is the pointwise algebra behind the paper's G^y insertion/removal step: the left-register defect is sandwiched by 1 - G^y, while the right-register weight is the projective outcome G^y_h.

theorem MIPStarRE.LDT.Commutativity.commDataProcessedGStabilityTwo_qSDDOp_expand {ι : 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 (commDataProcessedGStabilityTwoLeft params strategy family G q) (commDataProcessedGStabilityTwoRight params strategy family G q) = ∑ gb : StabilityTwoOutcome params, ev strategy.state (leftTensor ((1 - (G (pointHeight params q.1)).total) * (Matrix.conjTranspose ((CommutativityPoints.orderedProductOpFamily (evaluatedSliceFirstFactor params family q) (evaluatedSliceSecondFactor params family q)).outcome (gb.1.toFun (truncatePoint params q.1), gb.2)) * (CommutativityPoints.orderedProductOpFamily (evaluatedSliceFirstFactor params family q) (evaluatedSliceSecondFactor params family q)).outcome (gb.1.toFun (truncatePoint params q.1), gb.2)) * (1 - (G (pointHeight params q.1)).total)) * rightTensor ((G (pointHeight params q.1)).outcome gb.1))

For a projective submeasurement on a permutation-invariant bipartite state, the bipartite SSC defect is exactly half of the left/right SDD defect.

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSliceBABTerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : EvaluatedSliceQuestion params) (ab : EvaluatedSliceOutcome params) : Error

The BAB term in the evaluated-slice commutator expansion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSliceABATerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : EvaluatedSliceQuestion params) (ab : EvaluatedSliceOutcome params) : Error

The ABA term in the evaluated-slice commutator expansion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSliceBABATerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : EvaluatedSliceQuestion params) (ab : EvaluatedSliceOutcome params) : Error

The BABA term in the evaluated-slice commutator expansion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSliceABABTerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : EvaluatedSliceQuestion params) (ab : EvaluatedSliceOutcome params) : Error

The ABAB term in the evaluated-slice commutator expansion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSliceFirstProj {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxProjSubMeas (EvaluatedSliceQuestion params) (Fq params) ι

The first evaluated-slice factor viewed as a projective family.

Equations

• MIPStarRE.LDT.Commutativity.evaluatedSliceFirstProj params family q = { toSubMeas := MIPStarRE.LDT.Commutativity.evaluatedSliceFirstFactor params family q, proj := ⋯ }

noncomputable def MIPStarRE.LDT.Commutativity.evaluatedSliceSecondProj {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxProjSubMeas (EvaluatedSliceQuestion params) (Fq params) ι

The second evaluated-slice factor viewed as a projective family.

Equations

• MIPStarRE.LDT.Commutativity.evaluatedSliceSecondProj params family q = { toSubMeas := MIPStarRE.LDT.Commutativity.evaluatedSliceSecondFactor params family q, proj := ⋯ }

noncomputable def MIPStarRE.LDT.Commutativity.fullSliceFirstProj {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxProjSubMeas (FullSliceQuestion params) (Polynomial params) ι

The first full-slice factor viewed as a projective family.

Equations

• MIPStarRE.LDT.Commutativity.fullSliceFirstProj params family q = family.meas q.1

noncomputable def MIPStarRE.LDT.Commutativity.fullSliceSecondProj {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (family : IdxPolyFamily params ι) : IdxProjSubMeas (FullSliceQuestion params) (Polynomial params) ι

The second full-slice factor viewed as a projective family.

Equations

• MIPStarRE.LDT.Commutativity.fullSliceSecondProj params family q = family.meas q.2

noncomputable def MIPStarRE.LDT.Commutativity.fullSliceBABTerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : FullSliceQuestion params) (gh : FullSliceOutcome params) : Error

The BAB term in the full-slice commutator expansion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.fullSliceABATerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : FullSliceQuestion params) (gh : FullSliceOutcome params) : Error

The ABA term in the full-slice commutator expansion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.fullSliceBABATerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : FullSliceQuestion params) (gh : FullSliceOutcome params) : Error

The BABA term in the full-slice commutator expansion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.fullSliceABABTerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (q : FullSliceQuestion params) (gh : FullSliceOutcome params) : Error

The ABAB term in the full-slice commutator expansion.

Equations

• One or more equations did not get rendered due to their size.