integrable_of_lintegral_enorm_tendsto'

English

If φ is an ae-cover and f is AEMeasurable, then the lintegral over φ i tends to the lim of Lintegral over μ.

Русский

Если φ — ae-покрытие и f — AEMeasurable, линеграл по φ(i) стремится к линегралу по μ.

LaTeX

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

Lean4

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

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