English
If the tail of filters bounds ∫ φ i ‖f‖ dμ by I and almost everywhere nonnegativity holds, then f is integrable.
Русский
Если неравенство на интеграле нормы по φ(i) ограничено, и почти везде неотрицательно, то f интегрируем.
LaTeX
$$$Integrable f μ$$$
Lean4
theorem integrable_of_integral_norm_bounded [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ)
{f : α → E} (I : ℝ) (hfi : ∀ i, IntegrableOn f (φ i) μ) (hbounded : ∀ᶠ i in l, (∫ x in φ i, ‖f x‖ ∂μ) ≤ I) :
Integrable f μ :=
by
have hfm : AEStronglyMeasurable f μ := hφ.aestronglyMeasurable fun i => (hfi i).aestronglyMeasurable
refine hφ.integrable_of_lintegral_enorm_bounded I hfm ?_
conv at hbounded in integral _ _ =>
rw [integral_eq_lintegral_of_nonneg_ae (ae_of_all _ fun x => @norm_nonneg E _ (f x)) hfm.norm.restrict]
conv at hbounded in ENNReal.ofReal _ => rw [← coe_nnnorm, ENNReal.ofReal_coe_nnreal]
refine hbounded.mono fun i hi => ?_
rw [← ENNReal.ofReal_toReal <| ne_top_of_lt <| hasFiniteIntegral_iff_enorm.mp (hfi i).2]
apply ENNReal.ofReal_le_ofReal hi
