InfiniteFactorStability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform strong stability for properly infinite factors

The auxiliary product is fixed before any tolerance or representation is chosen. Matrix preparation gives complete proximity, which passes to the spatial product. Expected-subfactor stability is then descended to the original Hilbert space. Every published assumption is in the named bundle.

theorem OAI.KadisonKastler.productStage_size_pos line 36

theorem OAI.KadisonKastler.uniform_properlyInfinite_strong_stability_of_product_models line 47

Source documentation

The properly infinite factor case, with a uniform modulus and no cyclic-vector or common-subfactor hypothesis on the original pair.

theorem uniform_properlyInfinite_strong_stability_of_product_models
    (h : ModularCorePublishedInputs.{u})
    (hmod : PublishedModularSpectralResolution.{u})
    (hclass : PublishedFactorialModularCore.{u})
    (hkap : PublishedKaplanskyDensity.{u})
    (P : TwoRatioProductModel.{u})
    (hexpected : ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [Nontrivial H] [TopologicalSpace.SeparableSpace H]
      (M : VonNeumannAlgebra H), ScalarCenter M →
      Nonempty (ExpectedMatrixSubfactorModel (spatialProductAlgebra M P.stages.algebra))) :
    UniformProperInfiniteFactorStability.{u} := by
…

Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.ExpectedMatrixSubfactorModel, OAI.KadisonKastler.spatialProductAlgebra

theorem OAI.KadisonKastler.uniform_properlyInfinite_strong_stability line 104
Source documentation
The original published-input theorem is preserved as a specialization.
```
theorem uniform_properlyInfinite_strong_stability
    (h : FixedFactorPublishedInputs.{u}) : UniformProperInfiniteFactorStability.{u} := by
…
```