Section 11 commutativity: core operator estimates

Core operator-ordering notation and elementary comparison lemmas shared across the Section 11 commutativity argument.

References

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

noncomputable def MIPStarRE.LDT.Commutativity.commDataProcessedGError (params : Parameters) (gamma zeta : Error) : Error

Displayed error term for lem:comm-data-processed-g.

Equations

• MIPStarRE.LDT.Commutativity.commDataProcessedGError params gamma zeta = 48 * ↑params.m * (Real.rpow gamma (1 / 2) + Real.rpow zeta (1 / 2))

noncomputable def MIPStarRE.LDT.Commutativity.comMainError (params : Parameters) (gamma zeta : Error) : Error

Displayed error term for thm:com-main.

Equations

• MIPStarRE.LDT.Commutativity.comMainError params gamma zeta = 30 * ↑params.m * (Real.rpow gamma (1 / 4) + Real.rpow zeta (1 / 4) + Real.rpow (↑params.d / ↑params.q) (1 / 4))

@[reducible, inline]

abbrev MIPStarRE.LDT.Commutativity.CommDataProcessedGConclusion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) : Prop

Paper origin: references/ldt-paper/commutativity-G.tex:16-47 (\label{lem:comm-data-processed-g}).

Displayed conclusion of the commutativity-of-G-after-evaluation lemma. The strategy state is bipartite. Alice-side measurements are lifted to the left tensor factor, while Bob-side postprocessed point measurements are lifted to the right tensor factor.

Equations

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

@[reducible, inline]

abbrev MIPStarRE.LDT.Commutativity.ComMainConclusion {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (gamma zeta : Error) : Prop

Paper origin: references/ldt-paper/commutativity-G.tex:228-257 (\label{thm:com-main}).

Displayed conclusion of the commutativity-of-G theorem.

Equations

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

structure MIPStarRE.LDT.Commutativity.NormalizationConditionStatement {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) : Prop

Paper origin: references/ldt-paper/commutativity-G.tex:309-338 (\label{lem:normalization-condition}); records the Hermitian-square / identity-bound expansion used inside the proof of the commutativity theorem \label{thm:com-main} (references/ldt-paper/commutativity-G.tex:228-378).

Conclusion statement for lem:normalization-condition.

• sandwichedHermitianSquare : normalizationConditionAdjointSquareOperator P Q = normalizationConditionSquareOperator P Q

  The two square operators formed from ∑_b Q_b P_a Q_b agree.

• sandwichedBoundedByIdentity : normalizationConditionSquareOperator P Q ≤ normalizationConditionIdentityBound P Q

  The square operator formed from the sandwiched family is bounded by the identity operator.