NormalizerAveraging.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Averaging close exact normalizers within the normalizer group

Separate the near-identity residual into its algebra and commutant factors, average these separately, and take their polar unitaries inside the respective algebras. The quadratic covariance estimate controls the loss from separating the average of the product.

theorem OAI.KadisonKastler.exists_polar_unitary_mem_of_near_one line 28

Source documentation

The polar correction is taken inside the given algebra.

theorem exists_polar_unitary_mem_of_near_one (P : VonNeumannAlgebra H)
    (x : H →L[ℂ] H) (hx : x ∈ P) (hnear : ‖x - 1‖ < 1) :
    ∃ u : unitary (H →L[ℂ] H), (u : H →L[ℂ] H) ∈ P ∧
      ‖(u : H →L[ℂ] H) - x‖ ≤ ‖star x * x - 1‖ := by
…

theorem OAI.KadisonKastler.exists_normalizer_near_mean line 44
Source documentation
A contractive bimodule mean that preserves the two concrete algebras replaces a close family of normalizers by a normalizer at quadratic cost.
```
theorem exists_normalizer_near_mean
    (hpub : PublishedNormalizerFactorization (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedNormalizerFactorization