English
A general HasFiniteIntegral equivalence: HasFiniteIntegral f( (η ∘ₖ κ) a ) is equivalent to almost-everywhere HasFiniteIntegral of η x and HasFiniteIntegral of the κ–weighted norm integral.
Русский
Обобщённая эквивалентность HasFiniteIntegral: HasFiniteIntegral f((η ∘ κ) a) эквивалентно почти везде HasFiniteIntegral η x и HasFiniteIntegral интеграла по нормам.
LaTeX
$$$\text{HasFiniteIntegral}\ f\ ((η \circ κ)a) \iff (\forall^{\ae} x \;∂κ a, \text{HasFiniteIntegral}\ f(η x)) ∧ \text{HasFiniteIntegral}(x \mapsto ∫ y ‖f y‖ ∂η x) (κ a)$$$
Lean4
theorem hasFiniteIntegral_comp_iff' ⦃f : γ → E⦄ (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
(∀ᵐ x ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ y, ‖f y‖ ∂η x) (κ a) :=
by
rw [hasFiniteIntegral_congr hf.ae_eq_mk, hasFiniteIntegral_comp_iff hf.stronglyMeasurable_mk]
refine and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)
· filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using hasFiniteIntegral_congr hx
· filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using integral_congr_ae (EventuallyEq.fun_comp hx _)
