RemainingInputs.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Conditional strong stability from expected matrix subfactors

Existence of an expected matrix subfactor implies universal strong stability. The other hypotheses of the general stability criterion follow from the constructed operator-algebraic results.

structure OAI.KadisonKastler.RemainingStabilityPublishedInputs line 40
Source documentation
Existence of expected matrix subfactors in the absorbed type III₁ setting.
```
structure RemainingStabilityPublishedInputs : Prop where
…
```
theorem OAI.KadisonKastler.RemainingStabilityPublishedInputs.toPublished line 44
Source documentation
Expected matrix subfactors supply the hypotheses of the general stability criterion.
```
theorem RemainingStabilityPublishedInputs.toPublished
    (h : RemainingStabilityPublishedInputs.{u}) : UniversalStabilityPublishedInputs.{u} where
…
```
theorem OAI.KadisonKastler.universal_strong_stability_of_remaining line 74
Source documentation
Expected matrix subfactors imply the universal stability statement. Its tolerance precedes every representation.
```
theorem universal_strong_stability_of_remaining
    (h : RemainingStabilityPublishedInputs.{u}) : UniversalStrongStability.{u} :=
…
```