English
If AEStronglyMeasurable f with respect to μ×ν holds, HasFiniteIntegral f (μ×ν) is equivalent to the same a.e. and a ν-integral constraint with μ in the outer integral.
Русский
Если AEStronglyMeasurable f по отношению к μ×ν, имеет место HasFiniteIntegral f(μ×ν), тогда равносильно тому же почти наверняка и требованию интеграла по ν с μ внутри.
LaTeX
$$$\mathrm{AEStronglyMeasurable}(f, μ×ν) \Rightarrow \mathrm{HasFiniteIntegral}(f, μ×ν) \iff (\forall^{ae} x\partial μ, \mathrm{HasFiniteIntegral}(f(x,·), ν)) \land \mathrm{HasFiniteIntegral}(x \mapsto \int y \|f(x,y)\| dμ, μ)$$$
Lean4
theorem hasFiniteIntegral_prod_iff' ⦃f : α × β → E⦄ (h1f : AEStronglyMeasurable f (μ.prod ν)) :
HasFiniteIntegral f (μ.prod ν) ↔
(∀ᵐ x ∂μ, HasFiniteIntegral (fun y => f (x, y)) ν) ∧ HasFiniteIntegral (fun x => ∫ y, ‖f (x, y)‖ ∂ν) μ :=
by
rw [hasFiniteIntegral_congr h1f.ae_eq_mk, hasFiniteIntegral_prod_iff h1f.stronglyMeasurable_mk]
apply and_congr
· apply eventually_congr
filter_upwards [ae_ae_of_ae_prod h1f.ae_eq_mk.symm]
intro x hx
exact hasFiniteIntegral_congr hx
· apply hasFiniteIntegral_congr
filter_upwards [ae_ae_of_ae_prod h1f.ae_eq_mk.symm] with _ hx using integral_congr_ae (EventuallyEq.fun_comp hx _)
