MatrixPairPreparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Two-sided matrix preparation of an expected finite subalgebra

The first constructed matrix embedding makes the finite algebra common. The second, localized matrix embedding aligns its conjugate right algebra without destroying the first inclusion. All matrix and ordinary-gap losses are calculated from the actual two unitaries. The expected vector is then proved cyclic and separating for the corrected neighbor.

theorem OAI.KadisonKastler.norm_star_unitary_sub_one line 29

theorem OAI.KadisonKastler.exists_matrixPair_preparation line 39

Source documentation

Actual two-correction preparation, including the matrix error and cyclic/separating conclusions needed by the modular spectral theorem. The trace belongs only to R; the vector state on M is its composition with the supplied expectation.

theorem exists_matrixPair_preparation
    (hDistance : ∀ Q : VonNeumannAlgebra H,
      PublishedBlockCommutantApproximation (Algebra Q) H)
    (M N R : VonNeumannAlgebra H) (hRM : R ≤ M)
    (τ : FaithfulTracialState (Algebra R))
    (P : Algebra M →L[ℂ] Algebra R) (hP : P 1 = 1)
    (hleft : ∀ (r : Algebra R) (x : Algebra M),
      P (StarSubalgebra.inclusion hRM r * x) = r * P x)
    (hright : ∀ (r : Algebra R) (x : Algebra M),
      P (x * StarSubalgebra.inclusion hRM r) = P x * r)
    (Ω : H) (hΩ : ∀ x : Algebra M, expectedTrace τ P x = inner ℂ Ω (x.val Ω))
    (d : ModularConjugationData M Ω)
…

Mentions: OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.expectedTrace, OAI.KadisonKastler.ModularConjugationData