Documentation

MIPRE.Background.LIDT.Co.Commutativity.Scaffold.Core

Section 11 commutativity: displayed conclusions #

The displayed conclusions of lem:comm-data-processed-g, thm:com-main and lem:normalization-condition: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Scaffold/Core.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The two commutativity conclusions are state-dependent distances of joint operator families on the symmetric model strategy.state of a SymStrat params.next 𝔓 K, written strategy.state.SDDOpRel … (a VecState relation, reached through the parent structure); the normalization statement is about local operators of any C*-algebra 𝔓 with its order.

The two error terms of the vendored file are real-valued functions of the parameters alone: this file imports the vendored file for them and names them through an explicit open MIPStarRE.LDT.Commutativity (…) list.

Not ported #

References #

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

source
@[reducible, inline]
abbrev MIPRE.LIDT.Co.Commutativity.CommDataProcessedGConclusion {𝔓 : 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 𝔓) (gamma zeta : ℝ) :
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 local measurements are placed on the first factor of the strategy's symmetric model.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev MIPRE.LIDT.Co.Commutativity.ComMainConclusion {𝔓 : 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 𝔓) (gamma zeta : ℝ) :
    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.
    Instances For
      source
      structure MIPRE.LIDT.Co.Commutativity.NormalizationConditionStatement {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {OutcomeA : Type u_3} {OutcomeB : Type u_4} [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.

      Instances For