English
The pushforward equality on ℝ≥0∞ holds for ν and f_aemble: (ν.map f_aemble) {A} = ν (f^{-1} A).
Русский
Справедлива равенство образующей меры на ℝ≥0∞: (ν.map f_aemble) A = ν(f^{-1} A).
LaTeX
$$$ (ν.map f_{aemble}) A = ν (f^{-1} A) $$$
Lean4
/-- The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
Tonelli's theorem is measurable. -/
@[fun_prop, measurability]
theorem lintegral_prod_right' [SFinite ν] :
∀ {f : α × β → ℝ≥0∞}, Measurable f → Measurable fun x => ∫⁻ y, f (x, y) ∂ν :=
by
have m := @measurable_prodMk_left
refine Measurable.ennreal_induction (motive := fun f ↦ Measurable fun (x : α) ↦ ∫⁻ y, f (x, y) ∂ν) ?_ ?_ ?_
· intro c s hs
simp only [← indicator_comp_right]
suffices Measurable fun x => c * ν (Prod.mk x ⁻¹' s) by simpa [lintegral_indicator (m hs)]
exact (measurable_measure_prodMk_left hs).const_mul _
· rintro f g - hf - h2f h2g
simp only [Pi.add_apply]
conv => enter [1, x]; erw [lintegral_add_left (hf.comp m)]
exact h2f.add h2g
· intro f hf h2f h3f
have : ∀ x, Monotone fun n y => f n (x, y) := fun x i j hij y => h2f hij (x, y)
conv => enter [1, x]; erw [lintegral_iSup (fun n => (hf n).comp m) (this x)]
exact .iSup h3f
