English
For f : Prod α β → E, if AEStronglyMeasurable f on μ.compProd κ, then integrability of f under μ.compProd κ is equivalent to slice integrability and the integrability of the x-integral of norms.
Русский
Для функции f на произведении интегрируемость относительно μ.compProd κ эквивалентна интегрируемости по срезам и интегрируемости нормы по x.
LaTeX
$$$$ \\mathrm{AEStronglyMeasurable}\, f\, (μ.compProd κ) \\Rightarrow \\mathrm{Integrable}\, f (μ.compProd κ) \\iff \\left( \\forall^{\\text{ae}} x \\in μ, \\mathrm{Integrable} (\\lambda y, f(x,y)) (κ x) \\land \\mathrm{Integrable} (\\lambda x, \\int y \\|f(x,y)\\| d(κ x)) μ \\right) $$$$
Lean4
theorem integrable_compProd_iff [SFinite μ] [IsSFiniteKernel κ] {E : Type*} [NormedAddCommGroup E] {f : α × β → E}
(hf : AEStronglyMeasurable f (μ ⊗ₘ κ)) :
Integrable f (μ ⊗ₘ κ) ↔
(∀ᵐ x ∂μ, Integrable (fun y => f (x, y)) (κ x)) ∧ Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂(κ x)) μ :=
by
simp_rw [Measure.compProd, ProbabilityTheory.integrable_compProd_iff hf, Kernel.prodMkLeft_apply, Kernel.const_apply]
