ScalarLocalizationLimit.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Measurable localizations are strong limits of uniformly bounded continuous scalar multipliers. Consequently their commutant is already determined by the continuous scalar multipliers.

theorem OAI.KadisonSimilarity.exists_continuous_indicator_ae_sequence line 24

Source documentation

One bounded sequence works almost everywhere for a fixed measurable set.

theorem exists_continuous_indicator_ae_sequence (s : Set X) (hs : MeasurableSet s) :
    ∃ f : ℕ → C(X, ℂ), (∀ n x, ‖f n x‖ ≤ 1) ∧
      ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop
        (𝓝 (s.indicator (fun _ => (1 : ℂ)) x)) := by
…

theorem OAI.KadisonSimilarity.continuous_scalar_tendsto_localization line 44

Source documentation

Dominated convergence for bounded scalar multipliers on vector-valued L².

theorem continuous_scalar_tendsto_localization
    (s : Set X) (hs : MeasurableSet s) (f : ℕ → C(X, ℂ))
    (hf : ∀ n x, ‖f n x‖ ≤ 1)
    (ht : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop
      (𝓝 (s.indicator (fun _ => (1 : ℂ)) x))) (ξ : Lp H 2 μ) :
    Tendsto (fun n => VectorL2.continuousL2Mul μ (f n) ξ) atTop
      (𝓝 (l2Localization μ s hs ξ)) := by
…

Mentions: OAI.KadisonSimilarity.VectorL2.continuousL2Mul, OAI.KadisonSimilarity.l2Localization

theorem OAI.KadisonSimilarity.commutes_localizations_of_continuous line 95
Source documentation
Commutation with continuous scalar functions implies commutation with every measurable localization, on the actual vector-valued L² space.
```
theorem commutes_localizations_of_continuous
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (hT : ∀ f : C(X, ℂ),
      T * VectorL2.continuousL2Mul μ f = VectorL2.continuousL2Mul μ f * T)
    (s : Set X) (hs : MeasurableSet s) :
    T * l2Localization μ s hs = l2Localization μ s hs * T := by
…
```
Mentions: OAI.KadisonSimilarity.VectorL2.continuousL2Mul, OAI.KadisonSimilarity.l2Localization