ExpectedModelStability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform stability using the actual expected matrix models

Expected matrix models supply the modular preparation data. The second model supplies its normalized cyclic separating vector.

theorem OAI.KadisonKastler.uniform_expected_models_typeIII1_stability line 20

Source documentation

The expected-matrix-model formulation keeps the tolerance independent of both models and all represented algebras.

theorem uniform_expected_models_typeIII1_stability
    (h : ModularCorePublishedInputs.{u})
    (hModular : PublishedModularSpectralResolution.{u})
    {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧
      ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
        [CompleteSpace H] [Nontrivial H] [TopologicalSpace.SeparableSpace H],
      ∀ (M N : VonNeumannAlgebra H), TypeIII1Factor M → TypeIII1Factor N →
      ExpectedMatrixSubfactorModel M → ExpectedMatrixSubfactorModel N →
      ∀ γ : ℝ, 0 < γ → γ < δ → kkDistance M N < γ →
        MatrixNearInclusion M N γ → MatrixNearInclusion N M γ → NearConjugacy M N ε := by
…

Mentions: OAI.KadisonKastler.TypeIII1Factor, OAI.KadisonKastler.ExpectedMatrixSubfactorModel, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.MatrixNearInclusion, OAI.KadisonKastler.NearConjugacy