ConstructedModularActionCorrection.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.constructed_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 constructed_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.constructed_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 constructed_exists_common_action_of_near_normalizers
    (P : VonNeumannAlgebra H) (hpub : SmallNormalizerFactorization P)
    (m : ScalarInvariantMean G)
    (U : G →* unitary (H →L[ℂ] H)) (v : G → unitary (H →L[ℂ] H))
    (hv : ∀ g, Conjugates (v g) P P)
    {d : ℝ} (hd : 0 ≤ d) (hsmall : 3 * d ≤ 1 / 16384)
    (hclose : ∀ g, ‖(v g : H →L[ℂ] H) - (U g : H →L[ℂ] H)‖ ≤ d) :
    ∃ q : unitary (H →L[ℂ] H), ‖(q : H →L[ℂ] H) - 1‖ ≤ 3074 * d ∧
      ∀ g, Conjugates (U g) (unitaryConjugateAlgebra q P)
        (unitaryConjugateAlgebra q P) := by
…

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