English
A finite-integral condition for a product kernel κ ∘ η can be characterized by a particular equivalence involving almost everywhere behavior and an integral of a norm function.
Русский
Пусть есть интеграл по произведению κ и η; существование конечного интеграла эквивалентно соответствующему условию почти наверняка и интегралу нормы.
LaTeX
$$$\text{Iff}\left( \operatorname{HasFiniteIntegral} f ((κ ⊗ η) a) , \left(\text{Almost surely } x \sim κ a: \operatorname{HasFiniteIntegral}(f(x, ·)) (η(a, x)) \right) \land \operatorname{HasFiniteIntegral}\Big(\lambda x. \int_y \|f(x,y)\| dη(a,x)\Big) (κ a) \right)$$$
Lean4
theorem hasFiniteIntegral_compProd_iff' ⦃f : β × γ → E⦄ (h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) :
HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔
(∀ᵐ x ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧
HasFiniteIntegral (fun x => ∫ y, ‖f (x, y)‖ ∂η (a, x)) (κ a) :=
by
rw [hasFiniteIntegral_congr h1f.ae_eq_mk, hasFiniteIntegral_compProd_iff h1f.stronglyMeasurable_mk]
apply and_congr
· apply eventually_congr
filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with x hx using hasFiniteIntegral_congr hx
· apply hasFiniteIntegral_congr
filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with _ hx using
integral_congr_ae (EventuallyEq.fun_comp hx _)
