eLpNorm_compMeasurePreserving — Mathlib

English

For AEStronglyMeasurable g and MeasurePreserving f, MemLp g p (Measure.map f μ) implies MemLp (g ∘ f) p μ.

Русский

При AEStronglyMeasurable g и MeasurePreserving f, MemLp g p (Measure.map f μ) ⇒ MemLp (g ∘ f) p μ.

LaTeX

$$MemLp (g ∘ f) p μ$$

Lean4

theorem eLpNorm_compMeasurePreserving {ν : MeasureTheory.Measure β} (g : β →ₘ[ν] E) (hf : MeasurePreserving f μ ν) :
    eLpNorm (g.compMeasurePreserving f hf) p μ = eLpNorm g p ν :=
  by
  rw [eLpNorm_congr_ae (g.coeFn_compMeasurePreserving _)]
  exact eLpNorm_comp_measurePreserving g.aestronglyMeasurable hf

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