TypeIIISmallNormalizer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Small exact normalizers of the type III factors used by stability

Sakai innerness, logarithms, simplicity, finite spectral centering, and exponential factorization give small exact normalizers.

theorem OAI.KadisonKastler.typeIII_algebra_simple line 29

theorem OAI.KadisonKastler.exists_small_typeIII_normalizer_factors line 56

Source documentation

The precise type III local factorization needed in modular correction. Both constants are absolute.

theorem exists_small_typeIII_normalizer_factors
    (hSpectral : PublishedVonNeumannSpectralCut.{u})
    (hCompare : PublishedTypeIIIProjectionComparison.{u})
    (hSakai : PublishedSimpleDerivationInner.{u})
    (P : VonNeumannAlgebra H) (hP : TypeIIIFactor P)
    (v : unitary (H →L[ℂ] H)) (hv : Conjugates (H := H) v P P)
…

Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.Conjugates

def OAI.KadisonKastler.SmallNormalizerFactorization line 97
Source documentation
The local statement consumed by normalizer averaging.
```
def SmallNormalizerFactorization (P : VonNeumannAlgebra H) : Prop :=
…
```
theorem OAI.KadisonKastler.typeIII_smallNormalizerFactorization line 105