memLp_map_measure_iff — Mathlib

English

If MemLp g on Measure.map f μ and f is AEMeasurable, then MemLp (g ∘ f) on μ holds.

Русский

Если g ∈ MemLp на Measure.map f μ и f - AEMeasurable, тогда MemLp (g ∘ f) на μ выполняется.

LaTeX

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

Lean4

theorem memLp_map_measure_iff (hg : AEStronglyMeasurable g (Measure.map f μ)) (hf : AEMeasurable f μ) :
    MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ := by
  simp [MemLp, eLpNorm_map_measure hg hf, hg.comp_aemeasurable hf, hg]

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