lintegral_eq_of_tendsto — Mathlib

English

If hφ is an ae-cover and f is AEMeasurable, and the Lintegral over φ i tends to I, then the Lintegral over μ equals I.

Русский

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

LaTeX

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

Lean4

theorem lintegral_eq_of_tendsto [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ) {f : α → ℝ≥0∞}
    (I : ℝ≥0∞) (hfm : AEMeasurable f μ) (htendsto : Tendsto (fun i => ∫⁻ x in φ i, f x ∂μ) l (𝓝 I)) :
    ∫⁻ x, f x ∂μ = I :=
  tendsto_nhds_unique (hφ.lintegral_tendsto_of_countably_generated hfm) htendsto

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