English
If f is strongly measurable on α × β and has finite integral with respect to μ × ν, then f is integrable in a decomposed sense: almost everywhere in x the function y ↦ f(x,y) has finite integral with respect to ν, and the x-averaged norm-integral ∫‖f(x,y)‖ dν is finite with respect to μ.
Русский
Если f сильно измерима на α × β и имеет конечный интеграл по мере μ × ν, то f допускает разложение интеграла: почти для каждого x по μ интеграл по y устойчив по ν, и интеграл по x от ∫‖f(x,y)‖ dν конечен.
LaTeX
$$$\text{HasFiniteIntegral}(f, \mu\times\nu) \iff (\forall^{\mathrm{ae}} x\,\partial\mu,\ HasFiniteIntegral(y \mapsto f(x,y), \nu)) \\ \land HasFiniteIntegral\left(x \mapsto \int y\, \|f(x,y)\| \, d\nu\right)\, d\mu$$$
Lean4
theorem swap [SFinite μ] ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) : Integrable (f ∘ Prod.swap) (ν.prod μ) :=
integrable_swap_iff.2 hf
