OAI/Analysis/KadisonSimilarity/Representation/L2Localization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Diagonal indicator projections on the actual L² space and the pointwise column bound for every operator in their commutant.

  1. def OAI.KadisonSimilarity.l2Localize line 17
  2. theorem OAI.KadisonSimilarity.l2Localize_ae line 21
  3. def OAI.KadisonSimilarity.l2LocalizationLinear line 24
  4. theorem OAI.KadisonSimilarity.norm_l2Localize_le line 49
  5. def OAI.KadisonSimilarity.l2Localization line 55
  6. theorem OAI.KadisonSimilarity.l2Localization_ae line 61
  7. theorem OAI.KadisonSimilarity.l2Localization_const line 67
  8. theorem OAI.KadisonSimilarity.diagonal_commutant_column_bound line 81

    Source documentation

    A genuine diagonal-commuting operator has pointwise bounded columns.

    theorem diagonal_commutant_column_bound
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (hT : ∀ (r : Set Ω) (hr : MeasurableSet r),
      T * l2Localization μ r hr = l2Localization μ r hr * T)
    (x : H) : ∀ᵐ a ∂μ, ‖T (Lp.const 2 μ x) a‖ ≤ ‖T‖ * ‖x‖ := by
…

    Mentions: OAI.KadisonSimilarity.l2Localization