English
For a sequence of sets φ: ℕ→Set α forming an ae-cover and an a.e.-measurable f: α→ℝ≥0∞, the sequence of Lintegrals ∫⁻ x in φ(n), f(x) dμ tends to ∫⁻ x f(x) dμ along ν (here ν = atTop).
Русский
Для последовательности множеств φ: ℕ→Set α, образующей ae-покрытие, и a.e.-измеримой f: α→ℝ≥0∞, ряд линг-интегралов сходится к интегралу по μ вдоль atTop.
LaTeX
$$$\\forall hφ : AECover μ atTop φ,\\forall f : α → ℝ≥0∞, AEMeasurable f μ \\Rightarrow Tendsto (\\lambda n, ∫⁻ x in φ n, f x ∂μ) atTop (\\mathcal{N} (∫⁻ x, f x ∂μ))$$$
Lean4
theorem lintegral_tendsto_of_nat {φ : ℕ → Set α} (hφ : AECover μ atTop φ) {f : α → ℝ≥0∞} (hfm : AEMeasurable f μ) :
Tendsto (∫⁻ x in φ ·, f x ∂μ) atTop (𝓝 <| ∫⁻ x, f x ∂μ) :=
by
have lim₁ :=
lintegral_tendsto_of_monotone_of_nat hφ.biInter_Ici_aecover
(fun i j hij => biInter_subset_biInter_left (Ici_subset_Ici.mpr hij)) hfm
have lim₂ :=
lintegral_tendsto_of_monotone_of_nat hφ.biUnion_Iic_aecover
(fun i j hij => biUnion_subset_biUnion_left (Iic_subset_Iic.mpr hij)) hfm
refine tendsto_of_tendsto_of_tendsto_of_le_of_le lim₁ lim₂ (fun n ↦ ?_) fun n ↦ ?_
exacts [lintegral_mono_set (biInter_subset_of_mem left_mem_Ici),
lintegral_mono_set (subset_biUnion_of_mem right_mem_Iic)]
