CommonCenterFromFactors.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The common-center reduction to the uniform factor theorem

Uniform stability of factors passes to algebras with a common center by constructing nearby separable test algebras, bounding their fibers, and assembling the factor implementers.

def OAI.KadisonKastler.UniformFactorStability line 32
Source documentation
Factor stability with a tolerance independent of the represented factors. Zero-dimensional representations are allowed.
```
def UniformFactorStability : Prop :=
…
```
theorem OAI.KadisonKastler.commonCenterSeparableStability_of_factors line 38

theorem OAI.KadisonKastler.universalStrongStability_of_factors line 100

Source documentation

Uniform factor stability, central decomposition and the perturbation properties give strong stability on arbitrary representations.

theorem universalStrongStability_of_factors
    (hFactor : UniformFactorStability.{u})
    (hCentral : PublishedCentralPairDecomposition.{u})
    (hK : PublishedKaplanskyDensity.{u})
    (hSelect : PublishedUnitaryBorelSelection.{u, u})
    (hDix : ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H], ∀ M : VonNeumannAlgebra H, PublishedDixmierAveraging M)
    (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) :
…

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