ModularActionCorrection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common action from nearby normalizers

Pointwise selected normalizers need no continuity or measurability. Their multiplicative error is corrected in the closed normalizer group, then a single polar intertwiner gives the change of position. This is the final part of the manuscript's modular-alignment argument.

theorem OAI.KadisonKastler.cocycleDefect_le_of_close_representation line 28

Source documentation

An arbitrary unitary family uniformly close to a representation has multiplication error at most three times that displacement.

theorem cocycleDefect_le_of_close_representation
    (U : G →* unitary (H →L[ℂ] H)) (v : G → unitary (H →L[ℂ] H))
    {d : ℝ} (hd : 0 ≤ d)
    (hclose : ∀ g, ‖(v g : H →L[ℂ] H) - (U g : H →L[ℂ] H)‖ ≤ d) :
    unitaryCocycleDefect 1 (boundedUnitaryFamily v) ≤ 3 * d := by
…

Mentions: OAI.KadisonKastler.unitaryCocycleDefect, OAI.KadisonKastler.boundedUnitaryFamily

theorem OAI.KadisonKastler.exists_common_action_of_near_normalizers line 48
Source documentation
The given action normalizes a single nearby conjugate algebra after correcting the arbitrary pointwise choices of nearby normalizers.
```
theorem exists_common_action_of_near_normalizers
    (hpub : PublishedNormalizerFactorization (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedNormalizerFactorization