English
Let f be a β×γ → E function that is AEStronglyMeasurable with respect to (κ ⊗ η) a. Then f is integrable with respect to (κ ⊗ η) a if and only if: (i) for κ-a.e. x, the function y ↦ f(x,y) is integrable with respect to η(a,x), and (ii) the outer integral of the norm ∥f(x,y)∥ over η(a,x) integrated against κ a is finite.
Русский
Пусть f:β×γ→E является AEStronglyMeasurable относительно (κ ⊗ₖ η) a. Тогда f интегрируема по (κ ⊗ₖ η) a тогда и только тогда: (i) для почти всех x по κ a функция y↦f(x,y) интегрируема по η(a,x); (ii) интеграл по κ a от ∫‖f(x,y)‖ dη(a,x) конечен.
LaTeX
$$$\text{Integrable}\,f\;((κ \otimes_k η) a) \iff (\forall^{\ae} x \;∂κ a,\, \text{Integrable}(f(x,\cdot))\,(η(a,x))) \land \text{Integrable}\bigl(x \mapsto \int_y \|f(x,y)\| \partial η(a,x)\bigr)\,(κ a).$$$
Lean4
theorem integrable_compProd_iff ⦃f : β × γ → E⦄ (hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) :
Integrable f ((κ ⊗ₖ η) a) ↔
(∀ᵐ x ∂κ a, Integrable (fun y => f (x, y)) (η (a, x))) ∧ Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂η (a, x)) (κ a) :=
by
simp only [Integrable, hasFiniteIntegral_compProd_iff' hf, hf.norm.integral_kernel_compProd, hf, hf.compProd_mk_left,
eventually_and, true_and]
