English
If f is AEStronglyMeasurable on α×β, then for a.e. x, the section y ↦ f(x,y) is AEStronglyMeasurable on β.
Русский
Если f измеримо по Паре, то почти всюду секция по y измерима.
LaTeX
$$$$\\operatorname{ AEStronglyMeasurable}\\left( f\\;\\text{on } α×β\\right)\\Rightarrow\\forall^{\\text{ae}} x,\\; \\text{AEStronglyMeasurable}(y\\mapsto f(x,y))\\;\\text{на } β$$$$
Lean4
/-- The Bochner integral is a.e.-measurable.
This shows that the integrand of (the right-hand-side of) Fubini's theorem is a.e.-measurable. -/
theorem integral_prod_right' [SFinite ν] [NormedSpace ℝ E] ⦃f : α × β → E⦄ (hf : AEStronglyMeasurable f (μ.prod ν)) :
AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂ν) μ :=
⟨fun x => ∫ y, hf.mk f (x, y) ∂ν, hf.stronglyMeasurable_mk.integral_prod_right', by
filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with _ hx using integral_congr_ae hx⟩
