eLpNorm_trim — Mathlib

English

For any p, trimming the measure does not change the eLpNorm of f: eLpNorm f p (μ.trim hm) = eLpNorm f p μ.

Русский

Для любого p обрезание меры не меняет eLpNorm f: eLpNorm f p (μ.trim hm) = eLpNorm f p μ.

LaTeX

$$eLpNorm f p (μ.trim hm) = eLpNorm f p μ$$

Lean4

theorem eLpNorm_trim (hm : m ≤ m0) {f : α → ε} (hf : StronglyMeasurable[m] f) :
    eLpNorm f p (μ.trim hm) = eLpNorm f p μ := by
  by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · simpa only [h_top, eLpNorm_exponent_top] using eLpNormEssSup_trim hm hf
  simpa only [eLpNorm_eq_eLpNorm' h0 h_top] using eLpNorm'_trim hm hf

Похожие утверждения