English
A version of dominated convergence for filter indexing showing convergence of setToFun along a filter with countable generation.
Русский
Версия доминированной сходимости для фильтра с счетной генерацией: сходится setToFun вдоль фильтра.
LaTeX
$$$\\operatorname{tendsto}\\_{n} \\mathrm{setToFun} \\;\\mu\\; T\\; hT\\; (fs n) \\to \\mathrm{nhds}( \\mathrm{setToFun} \\;\\mu\\; T\\; hT\\; f)$$$
Lean4
theorem continuousAt_setToFun_of_dominated (hT : DominatedFinMeasAdditive μ T C) {fs : X → α → E} {x₀ : X}
{bound : α → ℝ} (hfs_meas : ∀ᶠ x in 𝓝 x₀, AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ᶠ x in 𝓝 x₀, ∀ᵐ a ∂μ, ‖fs x a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ a ∂μ, ContinuousAt (fun x => fs x a) x₀) : ContinuousAt (fun x => setToFun μ T hT (fs x)) x₀ :=
tendsto_setToFun_filter_of_dominated_convergence hT bound ‹_› ‹_› ‹_› ‹_›
