PreparedMatrixStability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Original-space stability for a prepared matrix pair

Row comparison, common-action alignment and core descent imply stability. All tolerances precede the represented algebras. The preparation data and the neighboring core type are explicit hypotheses.

theorem OAI.KadisonKastler.uniform_prepared_matrix_strong_stability line 22

Source documentation

Uniform stability once an actual common matrix subalgebra and its common right action have been prepared. Only matrix unit-ball proximity is used; no global linear selection of approximants is needed.

theorem uniform_prepared_matrix_strong_stability
    (h : ModularCorePublishedInputs.{u}) {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧
      ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
        [CompleteSpace H] [Nontrivial H] [TopologicalSpace.SeparableSpace H],
      ∀ (M N R : VonNeumannAlgebra H), TypeIIIFactor M →
      ∀ (Ω : H) (_m : ModularSpectralResolution M Ω) (n : ModularSpectralResolution N Ω)
        (J : H ≃ₗᵢ⋆[ℂ] H),
      Function.Involutive J → ‖Ω‖ = 1 →
      TypeIIInfinityFactor (regularCoreAlgebra n.group n.continuous N) →
      ∀ (s : ℕ → ℕ)
        (E : ∀ i, Generator.MatrixUnitSystem (Fin (s i)) (H →L[ℂ] H)),
…

Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.ModularSpectralResolution, OAI.KadisonKastler.TypeIIInfinityFactor, OAI.KadisonKastler.regularCoreAlgebra, OAI.Generator.MatrixUnitSystem