English
A general dominated convergence statement for setToFun with a sequence of functions fs and bound, similar to the earlier theorems but for general index set ι and bound on the norm.
Русский
Обобщённая теорема доминированной сходимости для setToFun по последовательности fs и ограничению на норму.
LaTeX
$$$\\operatorname{tendsto}\\_{n} \\mathrm{setToFun} \\;\\mu\\; T\\; hT\\; (fs n) \\to \\mathrm{setToFun} \\;\\mu\\; T\\; hT \\; f$$$
Lean4
theorem continuousWithinAt_setToFun_of_dominated (hT : DominatedFinMeasAdditive μ T C) {fs : X → α → E} {x₀ : X}
{bound : α → ℝ} {s : Set X} (hfs_meas : ∀ᶠ x in 𝓝[s] x₀, AEStronglyMeasurable (fs x) μ)
(h_bound : ∀ᶠ x in 𝓝[s] x₀, ∀ᵐ a ∂μ, ‖fs x a‖ ≤ bound a) (bound_integrable : Integrable bound μ)
(h_cont : ∀ᵐ a ∂μ, ContinuousWithinAt (fun x => fs x a) s x₀) :
ContinuousWithinAt (fun x => setToFun μ T hT (fs x)) s x₀ :=
tendsto_setToFun_filter_of_dominated_convergence hT bound ‹_› ‹_› ‹_› ‹_›
