English
If f is integrable w.r.t μ and X is measurable, then the function (x, ω) ↦ f(ω) composed with (X ω, ω) is integrable with respect to μ.map ω ↦ (X ω, ω).
Русский
Если f интегрируемо по μ и X измеримо, то (x,ω) ↦ f(ω) через (X ω, ω) интегрируемо по μ.map.
LaTeX
$$$$ \\text{Integrable}(f, μ) \\Rightarrow \\text{Integrable}(λx, f x.2, μ.map ω ↦ (X ω, ω)). $$$$
Lean4
theorem _root_.MeasureTheory.Integrable.comp_snd_map_prodMk {Ω} {mΩ : MeasurableSpace Ω} (X : Ω → β) {μ : Measure Ω}
{f : Ω → F} (hf_int : Integrable f μ) : Integrable (fun x : β × Ω => f x.2) (μ.map fun ω => (X ω, ω)) :=
by
by_cases hX : AEMeasurable X μ
· have hf := hf_int.1.comp_snd_map_prodMk X (mΩ := mΩ) (mβ := mβ)
refine ⟨hf, ?_⟩
rw [hasFiniteIntegral_iff_enorm, lintegral_map' hf.enorm (hX.prodMk aemeasurable_id)]
exact hf_int.2
· rw [Measure.map_of_not_aemeasurable]
· simp
· contrapose! hX; exact measurable_fst.comp_aemeasurable hX
