English
If each f_i is continuous on a set s, and u is summable with bounds for f_i, then the tsum is continuous on s.
Русский
Если каждая f_i непрерывна на s и есть сходящаяся верхняя граница, то сумма непрерывна на s.
LaTeX
$$$\\text{continuousOn_tsum}$$$
Lean4
/-- An infinite sum of functions with summable sup norm is continuous on a set if each individual
function is. -/
theorem continuousOn_tsum [TopologicalSpace β] {f : α → β → F} {s : Set β} (hf : ∀ i, ContinuousOn (f i) s)
(hu : Summable u) (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) : ContinuousOn (fun x => ∑' n, f n x) s := by
classical
refine (tendstoUniformlyOn_tsum hu hfu).continuousOn (Eventually.of_forall ?_)
intro t
exact continuousOn_finset_sum _ fun i _ => hf i
