English
If f is AEStronglyMeasurable on α × β, HasFiniteIntegral f (μ × ν) is equivalent to the same almost everywhere and a marginal integral criterion but with stronger measurability assumptions.
Русский
Если f является AEStronglyMeasurable на α × β, то HasFiniteIntegral f(μ×ν) эквивалентно аналогичным условиям почти-во-массива и маргинальной интегральной критерию с более сильной измеряемостью.
LaTeX
$$$\\mathrm{HasFiniteIntegral}_{μ×ν}(f) \\iff \\left(\\forall^{\\mathrm{ae}} x\\partial μ,\\ HasFiniteIntegral(\\lambda y. f(x,y), ν)\\right) \\land \\mathrm{HasFiniteIntegral}_{μ}\\left(x \\mapsto \\int y \\|f(x,y)\\| dν\\right)$$$
Lean4
theorem hasFiniteIntegral_prod_iff ⦃f : α × β → E⦄ (h1f : StronglyMeasurable f) :
HasFiniteIntegral f (μ.prod ν) ↔
(∀ᵐ x ∂μ, HasFiniteIntegral (fun y => f (x, y)) ν) ∧ HasFiniteIntegral (fun x => ∫ y, ‖f (x, y)‖ ∂ν) μ :=
by
simp only [hasFiniteIntegral_iff_enorm, lintegral_prod _ h1f.enorm.aemeasurable]
have (x : _) : ∀ᵐ y ∂ν, 0 ≤ ‖f (x, y)‖ := by filter_upwards with y using norm_nonneg _
simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
(h1f.norm.comp_measurable measurable_prodMk_left).aestronglyMeasurable,
enorm_eq_ofReal toReal_nonneg, ofReal_norm_eq_enorm]
-- this fact is probably too specialized to be its own lemma
have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun {p q r} h1 => by
rw [← and_congr_right_iff, and_iff_right_of_imp h1]
rw [this]
· intro h2f; rw [lintegral_congr_ae]
filter_upwards [h2f] with x hx
rw [ofReal_toReal]; rw [← lt_top_iff_ne_top]; exact hx
· intro h2f; refine ae_lt_top ?_ h2f.ne; exact h1f.enorm.lintegral_prod_right'
