OAI/Analysis/KadisonSimilarity/Representation/LocalizedL2Bound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Localized L² estimates recover pointwise bounds. This is the norm argument for the columns of an operator commuting with diagonal projections.

  1. lemma OAI.KadisonSimilarity.l2_norm_sq_eq_integral line 19
  2. theorem OAI.KadisonSimilarity.ae_norm_le_of_localized_square_bound line 32

    Source documentation

    Bounds on every localized square norm imply an almost-everywhere bound. The localized vector is allowed to be any representative of the indicator.

    theorem ae_norm_le_of_localized_square_bound (f : Lp H 2 μ) {C : ℝ} (hC : 0 ≤ C)
    (hlocal : ∀ (s : Set Ω), MeasurableSet s →
      ∃ g : Lp H 2 μ, g =ᵐ[μ] s.indicator f ∧ ‖g‖ ^ 2 ≤ C ^ 2 * μ.real s) :
    ∀ᵐ a ∂μ, ‖f a‖ ≤ C := by
…