Section 11 commutativity: core definitions

The operator families of the evaluated-slice, full-slice and stability steps of the Section 11 commutativity argument: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Defs/Core.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

A polynomial family family : IdxPolyFamily params 𝔓 lives in the local C*-algebra 𝔓 (the vendored Op ι), and a strategy is a SymStrat params.next 𝔓 K. The vendored placements leftPlacedSubMeas (ιB := ι), OpFamily.leftPlacedOpFamily (ιB := ι) and rightPlacedSubMeas (ιA := ι) are the model's S.leftPlacedSubMeas, OpFamily.leftPlacedOpFamily S and S.rightPlacedSubMeas. The definitions that already take a strategy (evaluatedSliceProductLeft, fullSliceProductRight, …) place by strategy.state, so their vendored signatures are unchanged; the three that place without one (leftOrderedProductOpFamily, evaluatedPointFamilyLeft, evaluatedPointFamilyRight) take the symmetric model S as an explicit first argument, as M1's tensorProductSubMeas does (planning/c6b-plan.md, "Departures in M1"). appendRightTotalOpFamily is generic over any type with a multiplication and sandwichByOuterSubMeas over any C*-algebra with its order.

The classical half of the vendored file (the question and outcome types and the evaluation maps on them) is not ported: this file imports the vendored file and names those declarations through an explicit open MIPStarRE.LDT.Commutativity (…) list.

New here

sandwichByOuterSubMeas_sum_outcome, the identity ∑_{a,b} A_a B_b A_a = ∑_a A_a B A_a that is the vendored inline sum_eq_total proof of sandwichByOuterSubMeas.

Not ported

• EvaluatedSliceQuestion: classical, imported.
• EvaluatedSliceOutcome: classical, imported.
• FullSliceQuestion: classical, imported.
• FullSliceOutcome: classical, imported.
• StabilityOneOutcome: classical, imported.
• StabilityTwoOutcome: classical, imported.
• fullSliceQuestionOfEvaluatedSlice: classical, imported.
• evaluateFullSliceOutcomeAtQuestion: classical, imported.
• evaluateStabilityOneOutcomeAtQuestion: classical, imported.
• evaluateStabilityTwoOutcomeAtQuestion: classical, imported.

References

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

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

noncomputable def MIPRE.LIDT.Co.Commutativity.leftOrderedProductOpFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) : OpFamily (α × β) (K →L[ℂ] K)

Ordered product placed on the first factor by the symmetric model S: (A_a B_b) ⊗ I is S.L (A_a * B_b).

Equations

• MIPRE.LIDT.Co.Commutativity.leftOrderedProductOpFamily S A B = MIPRE.LIDT.Co.OpFamily.leftPlacedOpFamily S (MIPRE.LIDT.Co.CommutativityPoints.orderedProductOpFamily A B)

noncomputable def MIPRE.LIDT.Co.Commutativity.appendRightTotalOpFamily {α : Type u_3} {R : Type u_4} [Mul R] (A : OpFamily α R) (X : R) : OpFamily α R

Append a total operator on the right of every outcome operator.

Equations

• MIPRE.LIDT.Co.Commutativity.appendRightTotalOpFamily A X = { outcome := fun (a : α) => A.outcome a * X, total := A.total * X }

theorem MIPRE.LIDT.Co.Commutativity.sandwichByOuterSubMeas_sum_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) : ∑ ab : α × β, A.outcome ab.1 * B.outcome ab.2 * A.outcome ab.1 = ∑ a : α, A.outcome a * B.total * A.outcome a

The outcome operators A_a B_b A_a of sandwichByOuterSubMeas sum to its total ∑_a A_a (∑_b B_b) A_a.

noncomputable def MIPRE.LIDT.Co.Commutativity.sandwichByOuterSubMeas {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) : SubMeas (α × β) 𝔓

Sandwiched product A_a B_b A_a.

Its total operator is the sum of sandwiches ∑_a A_a (∑_b B_b) A_a.

Equations

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

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

The postprocessed family ((u,x) ↦ G^x_[g(u)=a]).

Equations

• MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily params family = family.evaluatedAtNextPoint

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedPointFamilyLeft {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxSubMeas (MIPStarRE.LDT.Point params.next) (MIPStarRE.LDT.Fq params) (K →L[ℂ] K)

The evaluated family G^x_[g(u)=a] placed on the first factor by S.

Equations

• MIPRE.LIDT.Co.Commutativity.evaluatedPointFamilyLeft S params family u = S.leftPlacedSubMeas (MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily params family u)

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedPointFamilyRight {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (family : IdxPolyFamily params 𝔓) : IdxSubMeas (MIPStarRE.LDT.Point params.next) (MIPStarRE.LDT.Fq params) (K →L[ℂ] K)

The evaluated family G^x_[g(u)=a] placed on the second factor by S.

Equations

• MIPRE.LIDT.Co.Commutativity.evaluatedPointFamilyRight S params family u = S.rightPlacedSubMeas (MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily params family u)

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

The first evaluated factor G^x_[g(u)=a].

Equations

• MIPRE.LIDT.Co.Commutativity.evaluatedSliceFirstFactor params family q = MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily params family q.1

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

The second evaluated factor G^y_[h(v)=b].

Equations

• MIPRE.LIDT.Co.Commutativity.evaluatedSliceSecondFactor params family q = MIPRE.LIDT.Co.Commutativity.evaluatedPointFamily params family q.2

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceProductLeft {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) (K →L[ℂ] K)

The ordered evaluated-slice product (G^x_[g(u)=a] G^y_[h(v)=b]) ⊗ I, placed by strategy.state.L.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceProductRight {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) (K →L[ℂ] K)

The reversed evaluated-slice product (G^y_[h(v)=b] G^x_[g(u)=a]) ⊗ I, placed by strategy.state.L.

Equations

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

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

The sandwiched evaluated product G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a] in the local algebra. The strategy is not used; it is kept for the vendored signature.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.evaluatedSliceSandwichFirstFactor {𝔓 : 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 𝔓) : IdxSubMeas (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) (MIPStarRE.LDT.Commutativity.EvaluatedSliceOutcome params) (K →L[ℂ] K)

The sandwiched evaluated product (G^x_[g(u)=a] G^y_[h(v)=b] G^x_[g(u)=a]) ⊗ I, placed by strategy.state.L.

Equations

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

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

The first full slice measurement G^x.

Equations

• MIPRE.LIDT.Co.Commutativity.fullSliceFirstFactor params family q = (family.meas q.1).toSubMeas

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

The second full slice measurement G^y.

Equations

• MIPRE.LIDT.Co.Commutativity.fullSliceSecondFactor params family q = (family.meas q.2).toSubMeas

noncomputable def MIPRE.LIDT.Co.Commutativity.fullSliceProductLeft {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.FullSliceQuestion params) (MIPStarRE.LDT.Commutativity.FullSliceOutcome params) (K →L[ℂ] K)

The ordered full-slice product (G^x_g G^y_h) ⊗ I, placed by strategy.state.L.

Equations

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

noncomputable def MIPRE.LIDT.Co.Commutativity.fullSliceProductRight {𝔓 : 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 𝔓) : IdxOpFamily (MIPStarRE.LDT.Commutativity.FullSliceQuestion params) (MIPStarRE.LDT.Commutativity.FullSliceOutcome params) (K →L[ℂ] K)

The reversed full-slice product (G^y_h G^x_g) ⊗ I, placed by strategy.state.L.

Equations

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