UniversalStability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The factor case split and central decomposition extend the fixed-factor perturbation estimates to arbitrary representations.

structure OAI.KadisonKastler.UniversalStabilityPublishedInputs line 29
Source documentation
Perturbation and decomposition hypotheses for universal strong stability, including type I injectivity, infinite-factor projection structure, central decomposition, and Dixmier averaging.
```
structure UniversalStabilityPublishedInputs : Prop extends FixedFactorPublishedInputs.{u} where
…
```
theorem OAI.KadisonKastler.uniform_factor_strong_stability_of_published line 40
Source documentation
The factor conclusion follows from the constructed properly infinite case and the type I/finite case split.
```
theorem uniform_factor_strong_stability_of_published
    (h : UniversalStabilityPublishedInputs.{u}) : UniformFactorStability.{u} :=
…
```
theorem OAI.KadisonKastler.universal_strong_stability_of_published line 49
Source documentation
Universal strong Kadison--Kastler stability, with its tolerance chosen before all Hilbert spaces and represented von Neumann algebras, under the perturbation and decomposition hypotheses.
```
theorem universal_strong_stability_of_published
    (h : UniversalStabilityPublishedInputs.{u}) : UniversalStrongStability.{u} :=
…
```