lintegral_tendsto_of_countably_generated

English

If hφ is an ae-cover and f is AEMeasurable, then the Lintegral over φ i converges to the Lintegral over μ as i runs through a countably generated filter l.

Русский

Если hφ — ae-покрытие и f — AEMeasurable, тогда линтеграл по φ(i) сходится к линтегралу по μ при ходе через счетно образованный фильтр l.

LaTeX

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

Lean4

theorem lintegral_tendsto_of_countably_generated [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ)
    {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ) : Tendsto (fun i => ∫⁻ x in φ i, f x ∂μ) l (𝓝 <| ∫⁻ x, f x ∂μ) :=
  tendsto_of_seq_tendsto fun _u hu => (hφ.comp_tendsto hu).lintegral_tendsto_of_nat hfm

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