memLp_map_measure_iff — Mathlib

English

Let f be a measurable embedding. For any p, a function g on the target space belongs to Lp with respect to the pushforward measure map f μ if and only if g ∘ f belongs to Lp with respect to μ.

Русский

Пусть f — измеримое вложение. Тогда для любого p функция g на целевом пространстве принадлежит Lp по мере map f μ тогда и только тогда, когда g ∘ f принадлежит Lp по μ.

LaTeX

$$$\operatorname{MemLp}(g,p,\operatorname{Measure.map}(f,\mu)) \iff \operatorname{MemLp}(g\circ f,p,\mu)$$$

Lean4

theorem _root_.MeasurableEmbedding.memLp_map_measure_iff (hf : MeasurableEmbedding f) :
    MemLp g p (Measure.map f μ) ↔ MemLp (g ∘ f) p μ := by
  simp_rw [MemLp, hf.aestronglyMeasurable_map_iff, hf.eLpNorm_map_measure]

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