integrable_map_measure — Mathlib

English

Let f: α → α' and g: α' → ε with g AEStronglyMeasurable with respect to μ.map f and f AEMeasurable. Then g is integrable with respect to μ.map f if and only if g ∘ f is integrable with respect to μ.

Русский

Пусть f: α → α' и g: α' → ε; пусть g является AEStronglyMeasurable относительно μ.map f, а f — AEMeasurable. Тогда g интегрируемо по μ.map f тогда же, когда g ∘ f интегрируемо по μ.

LaTeX

$$$\\mathrm{Integrable}(g,\\mathrm{map}\, f\, μ) \\;\\Longleftrightarrow\\; \\mathrm{Integrable}(g \\circ f, μ)$$$

Lean4

theorem integrable_map_measure {f : α → α'} {g : α' → ε} (hg : AEStronglyMeasurable g (Measure.map f μ))
    (hf : AEMeasurable f μ) : Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ :=
  by
  simp_rw [← memLp_one_iff_integrable]
  exact memLp_map_measure_iff hg hf

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