ConstructedNormalizerCorrection.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Quadratic correction while preserving normalizers

Averages are corrected inside the algebra and its commutant before they are multiplied. The iteration therefore takes place in the complete space of normalizing families, not in all ambient unitary families.

theorem OAI.KadisonKastler.product_defect_of_near_averages line 18
Also declared: OAI/Analysis/KadisonKastler/NormalizerCorrection.lean:18 (same declaration text).
theorem OAI.KadisonKastler.scaled_normalizer_estimates line 43
Distinct definitions of this name: OAI/Analysis/KadisonKastler/NormalizerCorrection.lean:43 (different declaration text). Qualify references as OAI.KadisonKastler.scaled_normalizer_estimates@path.
theorem OAI.KadisonKastler.constructed_exists_normalizing_quadratic_step line 55
Source documentation
One averaging step stays in the normalizer group and has quadratic multiplicative defect.
```
theorem constructed_exists_normalizing_quadratic_step
    (P : VonNeumannAlgebra H) (hpub : SmallNormalizerFactorization P)
    (m : BimoduleMean (boundaryConstant (G := G) (B := H →L[ℂ] H)))
…
```
Mentions: OAI.KadisonKastler.SmallNormalizerFactorization, OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant
theorem OAI.KadisonKastler.constructed_exists_normalizing_representation line 117
Source documentation
Uniform iteration corrects the selected normalizers to an exact group representation, still inside the normalizer group at every parameter.
```
theorem constructed_exists_normalizing_representation
    (P : VonNeumannAlgebra H) (hpub : SmallNormalizerFactorization P)
    (m : BimoduleMean (boundaryConstant (G := G) (B := H →L[ℂ] H)))
…
```
Mentions: OAI.KadisonKastler.SmallNormalizerFactorization, OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant