integrable_of_lintegral_enorm_bounded

English

If hφ is an ae-cover and the tail of φ i has lintegral of ‖f‖ bounded by I, then f is integrable with respect to μ.

Русский

Если ae-покрытие hφ и линеграл ‖f‖ по φ(i) ограничен сверху, то f интегрируем по μ.

LaTeX

$$$\\forall I, hfm : AEStronglyMeasurable f μ, \\ (∀^{\\mathrm{f}} i \\in l, ∫⁻ x in φ i, ‖f x‖ₑ ∂μ ≤ I) \\Rightarrow Integrable f μ$$$

Lean4

theorem integrable_of_lintegral_enorm_bounded [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ)
    {f : α → E} (I : ℝ) (hfm : AEStronglyMeasurable f μ)
    (hbounded : ∀ᶠ i in l, ∫⁻ x in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I) : Integrable f μ :=
  by
  refine ⟨hfm, (le_of_tendsto ?_ hbounded).trans_lt ENNReal.ofReal_lt_top⟩
  exact hφ.lintegral_tendsto_of_countably_generated hfm.enorm

Похожие утверждения