OAI/Analysis/KadisonKastler/UnconditionalStability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Universal strong Kadison--Kastler stability

The two-ratio product's faithful-state homogeneity follows from its modular coisometries. Its expected matrix subfactor is constructed in the original representation. These constructions give a tolerance uniform over all Hilbert spaces and represented von Neumann algebras.

  1. theorem OAI.KadisonKastler.unconditional_properlyInfinite_strong_stability line 18
  2. theorem OAI.KadisonKastler.uniform_factor_strong_stability line 34
  3. theorem OAI.KadisonKastler.universal_strong_stability line 41

    Source documentation

    Theorem 1.1 of Universal strong Kadison–Kastler stability, at every universe level. The tolerance is chosen before the Hilbert space and both represented algebras.

    Distinct definitions of this name: ComparatorChallenges/StrongKadisonKastler.lean:37 (same statement text; different proof or body). Qualify references as OAI.KadisonKastler.universal_strong_stability@path.

    theorem universal_strong_stability : UniversalStrongStability.{u} :=
…