Tannery's theorem

Tannery's theorem gives a sufficient criterion for the limit of an infinite sum (with respect to an auxiliary parameter) to equal the sum of the pointwise limits. See https://en.wikipedia.org/wiki/Tannery%27s_theorem. It is a special case of the dominated convergence theorem (with the measure chosen to be the counting measure); but we give here a direct proof, in order to avoid some unnecessary hypotheses that appear when specialising the general measure-theoretic result.

theorem tendsto_tsum_of_dominated_convergence {α : Type u_1} {β : Type u_2} {G : Type u_3} {𝓕 : Filter α} [NormedAddCommGroup G] [CompleteSpace G] {f : α → β → G} {g : β → G} {bound : β → ℝ} (h_sum : Summable bound) (hab : ∀ (k : β), Filter.Tendsto (fun (x : α) => f x k) 𝓕 (nhds (g k))) (h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k) : Filter.Tendsto (fun (x : α) => ∑' (k : β), f x k) 𝓕 (nhds (∑' (k : β), g k))

Tannery's theorem: topological sums commute with termwise limits, when the norms of the summands are eventually uniformly bounded by a summable function.

(This is the special case of the Lebesgue dominated convergence theorem for the counting measure on a discrete set. However, we prove it under somewhat weaker assumptions than the general measure-theoretic result, e.g. G is not assumed to be an ℝ-vector space or second countable, and the limit is along an arbitrary filter rather than atTop ℕ.)

See also:

• MeasureTheory.tendsto_integral_of_dominated_convergence (for general integrals, but with more assumptions on G)
• continuous_tsum (continuity of infinite sums in a parameter)