eLpNorm_trim_ae — Mathlib

English

If f is strongly measurable with respect to the trimmed σ-algebra, then eLpNorm of f remains unchanged after trimming: eLpNorm f p (μ.trim hm) = eLpNorm f p μ.

Русский

Если f устойчиво измерима относительно обрезанных σ-алгебр, то eLpNorm до и после обрезки совпадает.

LaTeX

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

Lean4

theorem eLpNorm_trim_ae (hm : m ≤ m0) {f : α → ε} (hf : AEStronglyMeasurable[m] f (μ.trim hm)) :
    eLpNorm f p (μ.trim hm) = eLpNorm f p μ :=
  by
  rw [eLpNorm_congr_ae hf.ae_eq_mk, eLpNorm_congr_ae (ae_eq_of_ae_eq_trim hf.ae_eq_mk)]
  exact eLpNorm_trim hm hf.stronglyMeasurable_mk

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