English
Lebesgue dominated convergence for filters with a countable basis: if fs indexed by a countable directed set converge a.e. to f, and domination holds, then setToFun converges.
Русский
Сходимость доминированного типа через фильтры с дискретной базой: если fs сходятся почти везде к f и существуют границы, то setToFun сходится.
LaTeX
$$$\\operatorname{tendsto}\\_{n} \\mathrm{setToFun}(\\mu,T,hT,fsn) \\to \\mathrm{setToFun}(\\mu,T,hT,f)$$$
Lean4
/-- Lebesgue dominated convergence theorem for filters with a countable basis -/
theorem tendsto_setToFun_filter_of_dominated_convergence (hT : DominatedFinMeasAdditive μ T C) {ι} {l : Filter ι}
[l.IsCountablyGenerated] {fs : ι → α → E} {f : α → E} (bound : α → ℝ)
(hfs_meas : ∀ᶠ n in l, AEStronglyMeasurable (fs n) μ) (h_bound : ∀ᶠ n in l, ∀ᵐ a ∂μ, ‖fs n a‖ ≤ bound a)
(bound_integrable : Integrable bound μ) (h_lim : ∀ᵐ a ∂μ, Tendsto (fun n => fs n a) l (𝓝 (f a))) :
Tendsto (fun n => setToFun μ T hT (fs n)) l (𝓝 <| setToFun μ T hT f) :=
by
rw [tendsto_iff_seq_tendsto]
intro x xl
have hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s := by rwa [tendsto_atTop'] at xl
have h :
{x : ι | (fun n => AEStronglyMeasurable (fs n) μ) x} ∩ {x : ι | (fun n => ∀ᵐ a ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l :=
inter_mem hfs_meas h_bound
obtain ⟨k, h⟩ := hxl _ h
rw [← tendsto_add_atTop_iff_nat k]
refine tendsto_setToFun_of_dominated_convergence hT bound ?_ bound_integrable ?_ ?_
· exact fun n => (h _ (self_le_add_left _ _)).1
· exact fun n => (h _ (self_le_add_left _ _)).2
· filter_upwards [h_lim]
refine fun a h_lin => @Tendsto.comp _ _ _ (fun n => x (n + k)) (fun n => fs n a) _ _ _ h_lin ?_
rwa [tendsto_add_atTop_iff_nat]
