eLpNorm_map_measure — Mathlib

English

For AEStronglyMeasurable g and AEMeasurable f, MemLp g on Measure.map f μ is equivalent to MemLp (g ∘ f) on μ.

Русский

Для AEStronglyMeasurable g и AEMeasurable f совместимо MemLp g на Measure.map f μ и MemLp (g ∘ f) на μ.

LaTeX

$$MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ$$

Lean4

theorem eLpNorm_map_measure (hg : AEStronglyMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
    eLpNorm g p (Measure.map f μ) = eLpNorm (g ∘ f) p μ :=
  by
  by_cases hp_zero : p = 0
  · simp only [hp_zero, eLpNorm_exponent_zero]
  by_cases hp_top : p = ∞
  · simp_rw [hp_top, eLpNorm_exponent_top]
    exact eLpNormEssSup_map_measure hg hf
  simp_rw [eLpNorm_eq_lintegral_rpow_enorm hp_zero hp_top, lintegral_map' (hg.enorm.pow_const p.toReal) hf,
    Function.comp_apply]

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