Section 11 commutativity: product estimates

Basic product-style lemmas on projective submeasurement outcomes, the expansion of the two scalar-stability defects, and the commutator-expansion terms reused throughout the Section 11 commutativity argument: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Scaffold/Products.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The expansion terms are expectations strategy.state.ev (strategy.state.L …) on the symmetric model of the strategy; the vendored leftTensor (ι₂ := ι) and rightTensor (ι₁ := ι) are strategy.state.L and strategy.state.R, and ᴴ is star. postprocess_proj_outcome is generic over any C*-algebra with its order.

The vendored proofs of the two stability expansions restate the Kronecker products in every step and prove self-adjointness through Matrix.PosSemidef; here both are one application of stabilityDefect_ev_eq (below), whose proof uses the keystone's opTensor algebra and the self-adjointness of nonnegative elements.

New here

stabilityDefect_ev_eq, the per-outcome identity ev((L(X T) R(√G) − L X R(√G))^* (L(X T) R(√G) − L X R(√G))) = ev(L((1 − T) X^* X (1 − T)) R G) for self-adjoint T and 0 ≤ G, which the vendored file proves inline twice.

Not ported

Every declaration of the vendored file has a counterpart here.

References

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

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

theorem MIPRE.LIDT.Co.Commutativity.postprocess_proj_outcome {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {R : Type u_3} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] (P : ProjSubMeas α R) (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 MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily_outcome_proj {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) (u : MIPStarRE.LDT.Point params.next) (a : MIPStarRE.LDT.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 MIPRE.LIDT.Co.Commutativity.sqrt_subMeas_outcome_mul_self {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {α : Type u_3} [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 MIPRE.LIDT.Co.Commutativity.stabilityDefect_ev_eq {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (X T G : 𝔓) (hT : IsSelfAdjoint T) (hG : 0 ≤ G) : S.ev (star (S.L X * S.L T * S.R (CFC.sqrt G) - S.L X * S.R (CFC.sqrt G)) * (S.L X * S.L T * S.R (CFC.sqrt G) - S.L X * S.R (CFC.sqrt G))) = S.ev (S.L ((1 - T) * (star X * X) * (1 - T)) * S.R G)

The defect of a trailing self-adjoint factor T, weighted on the second factor by √G: ev((L(X T) R(√G) − L X R(√G))^* (…)) = ev(L((1 − T) X^* X (1 − T)) R G).

theorem MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityOne_qSDDOp_expand {𝔓 : 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) = ∑ 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))

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 MIPRE.LIDT.Co.Commutativity.commDataProcessedGStabilityTwo_qSDDOp_expand {𝔓 : 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 (commDataProcessedGStabilityTwoLeft params strategy family G q) (commDataProcessedGStabilityTwoRight params strategy family G q) = ∑ gb : MIPStarRE.LDT.Commutativity.StabilityTwoOutcome params, strategy.state.ev (strategy.state.L ((1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total) * (star ((CommutativityPoints.orderedProductOpFamily (evaluatedSliceFirstFactor params family q) (evaluatedSliceSecondFactor params family q)).outcome (gb.1.toFun (MIPStarRE.LDT.truncatePoint params q.1), gb.2)) * (CommutativityPoints.orderedProductOpFamily (evaluatedSliceFirstFactor params family q) (evaluatedSliceSecondFactor params family q)).outcome (gb.1.toFun (MIPStarRE.LDT.truncatePoint params q.1), gb.2)) * (1 - (G (MIPStarRE.LDT.pointHeight params q.1)).total)) * strategy.state.R ((G (MIPStarRE.LDT.pointHeight params q.1)).outcome gb.1))

Fixed-question expansion of the second scalar-stability qSDDOp term: the left-register defect is sandwiched by 1 - G^x, while the right-register weight is the projective outcome G^x_g.

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceBABTerm {𝔓 : 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) (ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) : ℝ

The BAB term in the evaluated-slice commutator expansion.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceABATerm {𝔓 : 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) (ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) : ℝ

The ABA term in the evaluated-slice commutator expansion.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceBABATerm {𝔓 : 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) (ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) : ℝ

The BABA term in the evaluated-slice commutator expansion.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceABABTerm {𝔓 : 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) (ab : MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) : ℝ

The ABAB term in the evaluated-slice commutator expansion.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceFirstProj {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxProjSubMeas (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Fq params) 𝔓

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

Equations

• MIPRE.LIDT.Co.Commutativity.evaluatedSliceFirstProj params family q = { toSubMeas := MIPRE.LIDT.Co.Commutativity.evaluatedSliceFirstFactor params family q, proj := ⋯ }

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceSecondProj {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxProjSubMeas (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Fq params) 𝔓

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

Equations

• MIPRE.LIDT.Co.Commutativity.evaluatedSliceSecondProj params family q = { toSubMeas := MIPRE.LIDT.Co.Commutativity.evaluatedSliceSecondFactor params family q, proj := ⋯ }

noncomputable def MIPRE.LIDT.Co.Commutativity.fullSliceFirstProj {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxProjSubMeas (MIPStarRE.LDT.Commutativity.FullSliceQuestion params) (MIPStarRE.LDT.Polynomial params) 𝔓

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

Equations

• MIPRE.LIDT.Co.Commutativity.fullSliceFirstProj params family q = family.meas q.1

noncomputable def MIPRE.LIDT.Co.Commutativity.fullSliceSecondProj {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxProjSubMeas (MIPStarRE.LDT.Commutativity.FullSliceQuestion params) (MIPStarRE.LDT.Polynomial params) 𝔓

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

Equations

• MIPRE.LIDT.Co.Commutativity.fullSliceSecondProj params family q = family.meas q.2

noncomputable def MIPRE.LIDT.Co.Commutativity.fullSliceBABTerm {𝔓 : 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.FullSliceQuestion params) (gh : MIPStarRE.LDT.Commutativity.FullSliceOutcome params) : ℝ

The BAB term in the full-slice commutator expansion.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.fullSliceABATerm {𝔓 : 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.FullSliceQuestion params) (gh : MIPStarRE.LDT.Commutativity.FullSliceOutcome params) : ℝ

The ABA term in the full-slice commutator expansion.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.fullSliceBABATerm {𝔓 : 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.FullSliceQuestion params) (gh : MIPStarRE.LDT.Commutativity.FullSliceOutcome params) : ℝ

The BABA term in the full-slice commutator expansion.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.fullSliceABABTerm {𝔓 : 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.FullSliceQuestion params) (gh : MIPStarRE.LDT.Commutativity.FullSliceOutcome params) : ℝ

The ABAB term in the full-slice commutator expansion.

Equations

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