SeparableReduction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Reduction of the universal theorem to separable Hilbert spaces

Local restrictions to separable reducing spaces give finite coefficient approximants and then a conjugacy on the original Hilbert space. The tolerance precedes every ambient space.

def OAI.KadisonKastler.SeparableStrongStability line 32
Source documentation
The separable-Hilbert-space intermediate conclusion of §9.
```
def SeparableStrongStability : Prop :=
…
```
theorem OAI.KadisonKastler.finiteCoefficientConjugations_of_separable_bound line 38

theorem OAI.KadisonKastler.universalStrongStability_of_separable line 87

Source documentation

Stability on arbitrary Hilbert spaces follows from separable stability, Kaplansky density, multiplication correction, and commutant approximation.

theorem universalStrongStability_of_separable
    (hsep : SeparableStrongStability.{u})
    (hK : PublishedKaplanskyDensity.{u})
    (hCorrection : ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H], ∀ M : VonNeumannAlgebra H, PublishedMultiplicationCorrection M)
    (hCommutant : ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H], ∀ M : VonNeumannAlgebra H,
        PublishedBlockCommutantApproximation (Algebra M) H) :
    UniversalStrongStability.{u} := by
…

Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra