English
A prime version of the finite-integral equivalence: HasFiniteIntegral f((η ∘ κ) a) is equivalent to almost-everywhere finite integrals of η x and a finite outer integral.
Русский
Прайм-версия эквивалентности конечного интеграла: HasFiniteIntegral f((η ∘ κ) a) эквивалентно почти наверняка конечным интегралам η x и внешнему интегралу.
LaTeX
$$$\text{HasFiniteIntegral}\,f\ ((η \circ κ)a) \iff (∀^{\ae} x \;∂κ a, \text{HasFiniteIntegral}\,f(η x)) ∧ \text{HasFiniteIntegral}(\!x \mapsto \int y ‖f(y)‖ ∂η x) (κ a)$$$
Lean4
theorem hasFiniteIntegral_comp_iff ⦃f : γ → E⦄ (hf : StronglyMeasurable f) :
HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
(∀ᵐ x ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ y, ‖f y‖ ∂η x) (κ a) :=
by
simp_rw [hasFiniteIntegral_iff_enorm, lintegral_comp _ _ _ hf.enorm]
simp_rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun y ↦ norm_nonneg _) hf.norm.aestronglyMeasurable,
enorm_eq_ofReal toReal_nonneg, ofReal_norm_eq_enorm]
have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun h ↦ by
rw [← and_congr_right_iff, and_iff_right_of_imp h]
rw [this]
· intro h
rw [lintegral_congr_ae]
filter_upwards [h] with x hx
rw [ofReal_toReal]
finiteness
· exact fun h ↦ ae_lt_top hf.enorm.lintegral_kernel h.ne
