English
A version of dominated convergence for filters with a countable basis; convergence of integrals under domination.
Русский
Версия доминированной конвергенции для фильтров с счётной базисной структурой; схождение интегралов при доминировании.
LaTeX
$$tendsto (∫ f_n) l (𝓝 (∫ f))$$
Lean4
/-- **Dominated convergence theorem** for filters with a countable basis. -/
theorem tendsto_lintegral_filter_of_dominated_convergence {ι} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → α → ℝ≥0∞}
{f : α → ℝ≥0∞} (bound : α → ℝ≥0∞) (hF_meas : ∀ᶠ n in l, Measurable (F n))
(h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, F n a ≤ bound a) (h_fin : ∫⁻ a, bound a ∂μ ≠ ∞)
(h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))) : Tendsto (fun n => ∫⁻ a, F n a ∂μ) l (𝓝 <| ∫⁻ a, f a ∂μ) :=
by
rw [tendsto_iff_seq_tendsto]
intro x xl
have hxl := by
rw [tendsto_atTop'] at xl
exact xl
have h := inter_mem hF_meas h_bound
replace h := hxl _ h
rcases h with ⟨k, h⟩
rw [← tendsto_add_atTop_iff_nat k]
refine tendsto_lintegral_of_dominated_convergence ?_ ?_ ?_ ?_ ?_
· exact bound
· intro
refine (h _ ?_).1
exact Nat.le_add_left _ _
· intro
refine (h _ ?_).2
exact Nat.le_add_left _ _
· assumption
· refine h_lim.mono fun a h_lim => ?_
apply @Tendsto.comp _ _ _ (fun n => x (n + k)) fun n => F n a
· assumption
rw [tendsto_add_atTop_iff_nat]
assumption
