English
If f is AEStronglyMeasurable on α×β, then f is integrable with μ×ν if and only if the ν-sections are integrable for μ-almost every x and the μ-integral of the ν-norm is finite.
Русский
Если f является AEStronglyMeasurable на α×β, тогда интегрируемость по μ×ν эквивалентна тому, что сечения по ν интегрируемы почти для каждого x по μ и интеграл по μ от норм функции по ν конечен.
LaTeX
$$$\mathrm{AEStronglyMeasurable}(f, μ×ν) \Rightarrow \mathrm{Integrable}(f, μ×ν) \iff (\forall^{ae} x\partial μ, \mathrm{Integrable}(y \mapsto f(x,y), ν)) \land \mathrm{Integrable}\left(x \mapsto \int y \|f(x,y)\| dμ, ν\right)$$$
Lean4
/-- A binary function is integrable if the function `x ↦ f (x, y)` is integrable for almost every
`y` and the function `y ↦ ∫ ‖f (x, y)‖ dx` is integrable. -/
theorem integrable_prod_iff' [SFinite μ] ⦃f : α × β → E⦄ (h1f : AEStronglyMeasurable f (μ.prod ν)) :
Integrable f (μ.prod ν) ↔
(∀ᵐ y ∂ν, Integrable (fun x => f (x, y)) μ) ∧ Integrable (fun y => ∫ x, ‖f (x, y)‖ ∂μ) ν :=
by
convert integrable_prod_iff h1f.prod_swap using 1
rw [funext fun _ => Function.comp_apply.symm, integrable_swap_iff]
