MatrixStagePairPreparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Two-correction preparation for actual increasing matrix stages

The faithful trace vector discharges the injectivity premise using the tracial matrix-closure theorem while preserving the state, expectation, vector, and modular-conjugation data.

theorem OAI.KadisonKastler.nearConjugacy_of_matrixPair_preparation line 28

Source documentation

Returning through the two actual preparation corrections adds their displacements, while preserving the strict final tolerance.

theorem nearConjugacy_of_matrixPair_preparation
    (M N : VonNeumannAlgebra H) (a b : unitary (H →L[ℂ] H)) {γ ε : ℝ}
    (ha : ‖(a : H →L[ℂ] H) - 1‖ ≤ 150 * γ)
    (hb : ‖(b : H →L[ℂ] H) - 1‖ ≤ 45300 * γ)
    (h : NearConjugacy M
      (unitaryConjugateAlgebra (star b) (unitaryConjugateAlgebra (star a) N)) ε) :
    NearConjugacy M N (45450 * γ + ε) := by
…

Mentions: OAI.KadisonKastler.NearConjugacy, OAI.KadisonKastler.unitaryConjugateAlgebra

theorem OAI.KadisonKastler.exists_matrixStagePair_preparation line 54

Source documentation

Increasing full matrix stages give both amenable corrections and the cyclic separating vector of the final neighbor. No separate injectivity assumption on the generated algebra is needed.

theorem exists_matrixStagePair_preparation
    (hDistance : ∀ Q : VonNeumannAlgebra H,
      PublishedBlockCommutantApproximation (Algebra Q) H)
    (M N : VonNeumannAlgebra H) (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    (τ : FaithfulTracialState (Algebra (FiniteMatrixStage.generatedVonNeumann A)))
    (P : Algebra M →L[ℂ] Algebra (FiniteMatrixStage.generatedVonNeumann A))
    (hP : P 1 = 1)
    (hleft : ∀ (r : Algebra (FiniteMatrixStage.generatedVonNeumann A)) (x : Algebra M),
      P (StarSubalgebra.inclusion (FiniteMatrixStage.generatedVonNeumann_le A) r * x) =
        r * P x)
    (hright : ∀ (r : Algebra (FiniteMatrixStage.generatedVonNeumann A)) (x : Algebra M),
…

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