TypeIFactorStability.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The type I branch and the projection dichotomy

The diffuse predicate is exactly the projection clause of Generator.IsII1Factor and TypeIIInfinityFactor. Its alternative, for a scalar-center algebra, is the existence of a minimal projection. This dichotomy is proved directly. The separable type I branch uses the constructed finite-group embedding.

def OAI.KadisonKastler.ProjectionDiffuse line 27
Source documentation
The diffuseness condition, independent of a finite or semifinite factor structure.
```
def ProjectionDiffuse (M : VonNeumannAlgebra H) : Prop :=
…
```
theorem OAI.KadisonKastler.IsTypeIFactor.not_projectionDiffuse line 31
theorem OAI.KadisonKastler.isTypeIFactor_or_projectionDiffuse line 43
Source documentation
A factor either has a minimal projection or every nonzero projection has a proper nonzero subprojection. No spectral or classification input is used in this alternative.
```
theorem isTypeIFactor_or_projectionDiffuse {M : VonNeumannAlgebra H}
    (hM : ScalarCenter M) : IsTypeIFactor M ∨ ProjectionDiffuse M := by
…
```
Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.IsTypeIFactor, OAI.KadisonKastler.ProjectionDiffuse
theorem OAI.KadisonKastler.isTypeIFactor_iff_not_projectionDiffuse line 62
theorem OAI.KadisonKastler.isII1Factor_of_finite_of_not_typeI line 72
Source documentation
A nonzero finite factor without minimal projections is a II₁ factor. Finiteness is only assumed for its identity projection; the required isometry condition follows directly.
```
theorem isII1Factor_of_finite_of_not_typeI {M : VonNeumannAlgebra H}
    (hM : ScalarCenter M) (hnonzero : (0 : H →L[ℂ] H) ≠ 1)
    (hfinite : FiniteProjectionIn M 1) (htype : ¬ IsTypeIFactor M) :
    Generator.IsII1Factor M.toStarSubalgebra := by
…
```
Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.IsTypeIFactor, OAI.Generator.IsII1Factor
theorem OAI.KadisonKastler.uniform_typeI_strong_stability line 92
Source documentation
The type I tolerance is independent of both the representation and the algebras, under one-sided embedding and type I injectivity.
```
theorem uniform_typeI_strong_stability {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧
      ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H],
      PublishedAmenableEmbedding (H := H) → PublishedTypeIInjectivity (H := H) →
…
```
Mentions: OAI.KadisonKastler.PublishedAmenableEmbedding, OAI.KadisonKastler.PublishedTypeIInjectivity

theorem OAI.KadisonKastler.uniform_separable_typeI_strong_stability line 105

Source documentation

Type I stability on separable Hilbert spaces has a uniform tolerance.

theorem uniform_separable_typeI_strong_stability {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧
      ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
        [TopologicalSpace.SeparableSpace H],
      ∀ M N : VonNeumannAlgebra H, IsTypeIFactor M → kkDistance M N < δ →
        NearConjugacy M N ε := by
…

Mentions: OAI.KadisonKastler.IsTypeIFactor, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.NearConjugacy