NormalizingRepresentations.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Transporting normalization between nearby representations

This is the final change of position in modular alignment. The exact normalizing representation is conjugated to the given representation using the actual averaged intertwiner and its polar unitary.

theorem OAI.KadisonKastler.conjugates_self_of_intertwined_representation line 24

Source documentation

An intertwiner transports a normalizing action to the conjugated algebra.

theorem conjugates_self_of_intertwined_representation
    (P : VonNeumannAlgebra H) (U z : G →* unitary (H →L[ℂ] H))
    (hz : ∀ g, Conjugates (z g) P P) (w : unitary (H →L[ℂ] H))
    (hw : ∀ g, (w : H →L[ℂ] H) * (U g : H →L[ℂ] H) =
      (z g : H →L[ℂ] H) * (w : H →L[ℂ] H)) (g : G) :
    Conjugates (U g) (unitaryConjugateAlgebra (star w) P)
      (unitaryConjugateAlgebra (star w) P) := by
…

Mentions: OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.unitaryConjugateAlgebra

theorem OAI.KadisonKastler.exists_near_conjugated_normalizing_action line 46
Source documentation
A translation-invariant bimodule mean gives the single small change of position. No regularity is required of the normalizing representation.
```
theorem exists_near_conjugated_normalizing_action
    (P : VonNeumannAlgebra H) (U z : G →* unitary (H →L[ℂ] H))
    (hz : ∀ g, Conjugates (z g) P P)
    (m : BimoduleMean (boundaryConstant (G := G) (B := H →L[ℂ] H)))
…
```
Mentions: OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.BimoduleMean, OAI.KadisonKastler.boundaryConstant