Section 11 commutativity: transport via evaluation specialization

Postprocessing identities for leftPlacedOpFamily of bilinear products, used to transport bounds across evaluation specializations of the full-slice commutation argument: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Transport/EvaluationSpecialization.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The vendored placement OpFamily.leftPlacedOpFamily (ιB := ι) is OpFamily.leftPlacedOpFamily S for a symmetric model S, which postprocess_leftPlacedOpFamily_product_outcome takes as an explicit first argument, as the placement lemmas of M1 and M3 do. The distance statements are strategy.state.sddErrorOp and strategy.state.SDDOpRel, vector-state quantities on joint operators.

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_leftPlacedOpFamily_product_outcome {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α₁ : Type u_3} {α₂ : Type u_4} {β₁ : Type u_5} {β₂ : Type u_6} [Fintype α₁] [Fintype α₂] [Fintype β₁] [Fintype β₂] (A : SubMeas α₁ 𝔓) (B : SubMeas α₂ 𝔓) (f₁ : α₁ → β₁) (f₂ : α₂ → β₂) (b₁ : β₁) (b₂ : β₂) (g : 𝔓 → 𝔓 → 𝔓) (hg_factor : ∀ (S : Finset α₁) (T : Finset α₂) (fA : α₁ → 𝔓) (fB : α₂ → 𝔓), ∑ a ∈ S ×ˢ T, g (fA a.1) (fB a.2) = g (∑ a ∈ S, fA a) (∑ b ∈ T, fB b)) : ((OpFamily.leftPlacedOpFamily S { outcome := fun (ab : α₁ × α₂) => g (A.outcome ab.1) (B.outcome ab.2), total := g A.total B.total }).postprocess fun (ab : α₁ × α₂) => (f₁ ab.1, f₂ ab.2)).outcome (b₁, b₂) = (OpFamily.leftPlacedOpFamily S { outcome := fun (ab : β₁ × β₂) => g ((postprocess A f₁).outcome ab.1) ((postprocess B f₂).outcome ab.2), total := g (postprocess A f₁).total (postprocess B f₂).total }).outcome (b₁, b₂)

Postprocessing a leftPlacedOpFamily of a bilinear product equals the leftPlacedOpFamily of the product of postprocessed submeasurements, for any binary operation g that factors over finite sums.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedFromFullSliceProductLeft_outcome_eq {𝔓 : 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) : (evaluatedFromFullSliceProductLeft params strategy family q).outcome ab = (evaluatedSliceProductLeft params strategy family q).outcome ab

The evaluated-from-full-slice ordered product equals the evaluated-slice ordered product at each question-outcome pair.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedFromFullSliceProductRight_outcome_eq {𝔓 : 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) : (evaluatedFromFullSliceProductRight params strategy family q).outcome ab = (evaluatedSliceProductRight params strategy family q).outcome ab

The evaluated-from-full-slice reversed product equals the evaluated-slice reversed product at each question-outcome pair.

theorem MIPRE.LIDT.Co.Commutativity.evaluationSpecialization_sddErrorOp_eq {𝔓 : 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 𝔓) : strategy.state.sddErrorOp (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (evaluatedFromFullSliceProductLeft params strategy family) (evaluatedFromFullSliceProductRight params strategy family) = strategy.state.sddErrorOp (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (evaluatedSliceProductLeft params strategy family) (evaluatedSliceProductRight params strategy family)

The evaluated-from-full-slice SDD error equals the evaluated-slice SDD error, because the postprocessed product equals the product of postprocessed submeasurements at every question-outcome pair.

theorem MIPRE.LIDT.Co.Commutativity.evaluatedSliceCommutation_of_evaluationSpecialization {𝔓 : 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 𝔓) (δ : ℝ) (hEval : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (evaluatedFromFullSliceProductLeft params strategy family) (evaluatedFromFullSliceProductRight params strategy family) δ) : strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (evaluatedSliceProductLeft params strategy family) (evaluatedSliceProductRight params strategy family) δ

Restate the evaluated-from-full-slice commutation bound as a bound for the evaluated-slice product families, using the pointwise postprocessing identities.