integrable_of_lintegral_enorm_bounded'

English

If hφ is an ae-cover and f is AEStronglyMeasurable, then the Tendsto with a real bound implies integrability.

Русский

Если ae-покрытие и f — AEStronglyMeasurable, тогда существование предела для линеграла норм обеспечивает интегрируемость.

LaTeX

$$$\\forall hφ, (AEStronglyMeasurable f μ) \\Rightarrow Tendsto (\\lambda i, lintegral (μ.restrict (φ i)) (f)) l (\\mathcal{N} (lintegral μ f)) \\Rightarrow Integrable f μ$$$

Lean4

theorem integrable_of_lintegral_enorm_bounded' [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ)
    {f : α → E} (I : ℝ≥0) (hfm : AEStronglyMeasurable f μ) (hbounded : ∀ᶠ i in l, ∫⁻ x in φ i, ‖f x‖ₑ ∂μ ≤ I) :
    Integrable f μ :=
  hφ.integrable_of_lintegral_enorm_bounded I hfm (by simpa only [ENNReal.ofReal_coe_nnreal] using hbounded)

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