integrable_of_lintegral_enorm_tendsto

English

If hφ is an ae-cover, f is AEStronglyMeasurable, and the Tendsto of the norms of f over φ i is to I, then f is integrable.

Русский

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

LaTeX

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

Lean4

theorem integrable_of_lintegral_enorm_tendsto [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ)
    {f : α → E} (I : ℝ) (hfm : AEStronglyMeasurable f μ)
    (htendsto : Tendsto (fun i => ∫⁻ x in φ i, ‖f x‖ₑ ∂μ) l (𝓝 <| .ofReal I)) : Integrable f μ :=
  by
  refine hφ.integrable_of_lintegral_enorm_bounded (max 1 (I + 1)) hfm ?_
  refine htendsto.eventually (ge_mem_nhds ?_)
  refine (ENNReal.ofReal_lt_ofReal_iff (lt_max_of_lt_left zero_lt_one)).2 ?_
  exact lt_max_of_lt_right (lt_add_one I)

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