integral_eq_of_tendsto — Mathlib

English

If hφ is an ae-cover and f is AEMeasurable with nonempty index set, the iSup of lintegrals equals the lintegral over μ.

Русский

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

LaTeX

$$$iSup_i (lintegral (μ.restrict (φ i)) (f)) = lintegral μ (f)$$$

Lean4

/-- Slight reformulation of `MeasureTheory.AECover.integral_tendsto_of_countably_generated`. -/
theorem integral_eq_of_tendsto [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ) {f : α → E}
    (I : E) (hfi : Integrable f μ) (h : Tendsto (fun n => ∫ x in φ n, f x ∂μ) l (𝓝 I)) : ∫ x, f x ∂μ = I :=
  tendsto_nhds_unique (hφ.integral_tendsto_of_countably_generated hfi) h

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