OAI/Analysis/KadisonKastler/ExpectedMatrixStability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Stability from an expected irreducible increasing matrix algebra

The actual two amenable corrections prepare the common left and right matrix algebras. The corrected neighbor remains type III₁ by core isomorphism, and its cyclic separating vector supplies the modular data for prepared matrix stability. All tolerances precede the algebras and the expectation data; no trace is required on either ambient factor.

  1. theorem OAI.KadisonKastler.corrected_neighbor_typeIII1 line 38
  2. theorem OAI.KadisonKastler.corrected_neighbor_core line 52
  3. theorem OAI.KadisonKastler.uniform_expected_matrix_typeIII1_stability line 82

    Source documentation

    Two type III₁ factors are strongly close when the source has the specified expected irreducible increasing matrix algebra and the pair is close on all matrix unit balls. The tolerance is independent of all representation, vector and expectation data.

    theorem uniform_expected_matrix_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 →
      ∀ (A : ℕ → FiniteMatrixStage M),
        Monotone (fun n => (A n).units.concreteAlgebra) →
      ∀ (τ : FaithfulTracialState (Algebra (FiniteMatrixStage.generatedVonNeumann A)))
        (P : Algebra M →L[ℂ] Algebra (FiniteMatrixStage.generatedVonNeumann A)), P 1 = 1 →
…

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