OAI/Analysis/KadisonSimilarity/Representation/DecomposableColumns.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The columns of an operator commuting with localization are pointwise bounded by its operator norm. No essential-norm formula is assumed.

  1. theorem OAI.KadisonSimilarity.indicatorConstL2_norm_sq line 17
  2. theorem OAI.KadisonSimilarity.decomposable_column_ae_bound line 32

    Source documentation

    Commutation with localization bounds each constant-vector column almost everywhere. The null set is allowed to depend on the chosen vector.

    theorem decomposable_column_ae_bound
    (T : Lp H 2 μ →L[ℂ] Lp H 2 μ)
    (hlocal : ∀ (s : Set Ω) (hs : MeasurableSet s) (x : H),
      T (indicatorConstLp 2 hs (measure_ne_top μ s) x) =ᵐ[μ]
        s.indicator (T (Lp.const 2 μ x)))
    (x : H) :
    ∀ᵐ a ∂μ, ‖T (Lp.const 2 μ x) a‖ ≤ ‖T‖ * ‖x‖ := by
…