# 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.

**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)