English
A prime form of integrability equivalence: f is integrable relative to (η ∘ κ) a iff almost everywhere each η y is integrable and the outer integral of norms is integrable against κ a.
Русский
primes форма эквивалентности интегрируемости: f интегрируема относительно (η ∘ κ) a тогда и только тогда, когда почти повсеместно η y интегрируема и внешний интеграл норм интегрируем.
LaTeX
$$$\text{Integrable}\,f\;((η \circ κ)a) \iff (∀^{\ae} y \;∂κ a, \text{Integrable}\,f(y)\,(η y)) ∧ \text{Integrable}(y \mapsto ∫ z ‖f z‖ ∂η y) (κ a)$$$
Lean4
theorem integrable_comp_iff ⦃f : γ → E⦄ (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
Integrable f ((η ∘ₖ κ) a) ↔ (∀ᵐ y ∂κ a, Integrable f (η y)) ∧ Integrable (fun y ↦ ∫ z, ‖f z‖ ∂η y) (κ a) := by
simp only [Integrable, hf, hasFiniteIntegral_comp_iff' hf, true_and, eventually_and, hf.comp,
hf.norm.integral_kernel_comp]
