RegularLocalizationNormal.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded weak continuity of localization averages

The constant representation is a countable diagonal amplification in scalar Hilbert coordinates. Its bounded weak continuity therefore gives bounded weak continuity of the translated-cutoff sandwich. This permits finite packet compressions to be averaged before taking their limit.

theorem OAI.KadisonKastler.regularConstantHom_tendsto_weak line 26

Source documentation

Bounded weak operator limits pass through the constant representation.

theorem regularConstantHom_tendsto_weak {ι : Type*} {l : Filter ι}
    (T : ι → H →L[ℂ] H) (S : H →L[ℂ] H) (C : ℝ)
    (hC : ∀ᶠ i in l, ‖T i‖ ≤ C)
    (hT : ∀ x y : H, Tendsto (fun i => inner ℂ y (T i x)) l
      (𝓝 (inner ℂ y (S x))))
    (f g : RegularCoreHilbert H) :
    Tendsto (fun i => inner ℂ g (regularConstantHom (volume : Measure ℝ) (T i) f)) l
      (𝓝 (inner ℂ g (regularConstantHom (volume : Measure ℝ) S f))) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularConstantHom

theorem OAI.KadisonKastler.regularLocalizationAverage_tendsto_weak line 46

Source documentation

A localized Haar average preserves every bounded weak operator limit.

theorem regularLocalizationAverage_tendsto_weak {ι : Type*} {l : Filter ι}
    (s : Set ℝ) (hs : MeasurableSet s) (hfinite : volume s ≠ ⊤)
    (T : ι → RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (S : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) (C : ℝ)
    (hC : ∀ᶠ i in l, ‖T i‖ ≤ C)
    (hT : ∀ x y, Tendsto (fun i => inner ℂ y (T i x)) l
      (𝓝 (inner ℂ y (S x))))
    (f g : RegularCoreHilbert H) :
    Tendsto (fun i => inner ℂ g (regularLocalizationAverage s hs hfinite (T i) f)) l
      (𝓝 (inner ℂ g (regularLocalizationAverage s hs hfinite S f))) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularLocalizationAverage