integrable_of_integral_tendsto_of_nonneg_ae

English

If φ is an ae-cover with natural number index and f is AEMeasurable, then the integral over φ i tends to the integral over μ when i goes to ∞.

Русский

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

LaTeX

$$$Tendsto (\\lambda i, \\int_{φ i} f) l (\\mathcal{N} (\\int f))$$$

Lean4

theorem integrable_of_integral_tendsto_of_nonneg_ae [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α}
    (hφ : AECover μ l φ) {f : α → ℝ} (I : ℝ) (hfi : ∀ i, IntegrableOn f (φ i) μ) (hnng : ∀ᵐ x ∂μ, 0 ≤ f x)
    (htendsto : Tendsto (fun i => ∫ x in φ i, f x ∂μ) l (𝓝 I)) : Integrable f μ :=
  let ⟨I', hI'⟩ := htendsto.isBoundedUnder_le
  hφ.integrable_of_integral_bounded_of_nonneg_ae I' hfi hnng hI'

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