English
A function f: α×β → E is integrable with respect to μ×ν if and only if the sections x ↦ f(x, y) are integrable for ν-almost every x, and the outer integral of the x-integral of the norm is finite with respect to μ.
Русский
Функция f: α×β → E интегрируема по мере μ×ν тогда и только тогда, когда сечения x ↦ f(x,y) интегрируемы для ν-почти всех x и внешний интеграл по μ от нормы интеграла по ν конечен.
LaTeX
$$$\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 `y ↦ f (x, y)` is integrable for almost every
`x` and the function `x ↦ ∫ ‖f (x, y)‖ dy` is integrable. -/
theorem integrable_prod_iff ⦃f : α × β → E⦄ (h1f : AEStronglyMeasurable f (μ.prod ν)) :
Integrable f (μ.prod ν) ↔
(∀ᵐ x ∂μ, Integrable (fun y => f (x, y)) ν) ∧ Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂ν) μ :=
by simp [Integrable, h1f, hasFiniteIntegral_prod_iff', h1f.norm.integral_prod_right', h1f.prodMk_left]
