continuous_tsum — Mathlib

English

If each f_i is continuous and u is summable with bounds on norms, then the tsum is continuous.

Русский

Если каждая f_i непрерывна и существуют верхние границы нормы суммы, тогда tsum непрерывна.

LaTeX

$$$\\text{continuous_tsum}$$$

Lean4

/-- An infinite sum of functions with summable sup norm is continuous if each individual
function is. -/
theorem continuous_tsum [TopologicalSpace β] {f : α → β → F} (hf : ∀ i, Continuous (f i)) (hu : Summable u)
    (hfu : ∀ n x, ‖f n x‖ ≤ u n) : Continuous fun x => ∑' n, f n x :=
  by
  simp_rw [← continuousOn_univ] at hf ⊢
  exact continuousOn_tsum hf hu fun n x _ => hfu n x

Похожие утверждения