FactorStability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Reduction of factor stability to the properly infinite case

The type I, finite diffuse and properly infinite cases use one common minimum tolerance. The infinite-projection theorem identifies the properly infinite case of a factor with nonfinite identity.

def OAI.KadisonKastler.UniformProperInfiniteFactorStability line 23
Source documentation
The properly infinite factor case, with the tolerance uniform over all separable representations.
```
def UniformProperInfiniteFactorStability : Prop :=
…
```
theorem OAI.KadisonKastler.nearConjugacy_of_subsingleton line 30

theorem OAI.KadisonKastler.uniformFactorStability_of_properlyInfinite line 50

Source documentation

The full factor assertion follows from the type I, II₁ and properly infinite cases. Zero-dimensional representations are included in the conclusion.

theorem uniformFactorStability_of_properlyInfinite
    (hInfinite : UniformProperInfiniteFactorStability.{u})
    (hFinite : FiniteFactorPublishedInputs.{u})
    (_hTypeI : ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [TopologicalSpace.SeparableSpace H],
      PublishedTypeIInjectivity (H := H))
…

Mentions: OAI.KadisonKastler.PublishedTypeIInjectivity