tendsto_tsum_of_dominated_convergence

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

**Tannery's Theorem**: Given a normed additive commutative group `G` that is also a complete space, and functions `f : α → β → G`, `g : β → G`, `bound : β → ℝ`. If the function `bound` is summable, for every `k` in `β`, the function `f(x, k)` tends to `g(k)` when `x` tends towards the filter `𝓕`, and there exists an element in the filter `𝓕` for which the norm of `f(n, k)` is less than or equal to `bound(k)` for all `k` in `β`, then the function `x ↦ ∑' k, f(x, k)` tends to `∑' k, g(k)` when `x` tends towards the filter `𝓕`. In simpler terms, under these conditions, the limit of the sum of the sequence of functions `f(x, k)` is equal to the sum of the limits of the functions `f(x, k)`, that is, termwise limit and summation are interchangeable. This theorem is a special case of the Lebesgue Dominated Convergence Theorem for counting measures on a discrete set and is proven under weaker assumptions than the general measure-theoretic result. For instance, `G` is not assumed to be a real vector space or second countable, and the limit is along an arbitrary filter rather than the countably infinite set of natural numbers.

More concisely: Given a normed additive commutative group `G`, a summable function `bound : β -> ℝ`, and functions `f : α -> β -> G` and `g : β -> G` such that `lim x (f x k) = g k` for all `k` and some `x` in the filter `𝓕` and `||f x k|| <= bound k` for all `k`, then `lim x (sum k, f x k) = sum k, g k`.