Discrete version of Dominated Convergence Theorem

Stream: Is there code for X?

[Gareth Ma]

Hi, does this version of the dominated convergence theorem exist in Mathlib? Basically if $\lim_{N \to \infty} f_N(n) = f(n)$ then $\lim_{N \to \infty} \sum_{n = -\infty}^{\infty} f_N(n) = \sum_{n = -\infty}^{\infty} f(n)$ (with some summability stuff of course)

[Daniel Weber]

Is this a valid formalization of the statement?

import Mathlib

open Filter Topology

example {α : Type*} {β : Type*} [NormedAddCommGroup α] (f_N : β → ℕ → α) (g : β → α) (f : β → α)
    (dom : ∀ x N, ‖f_N x N‖ ≤ ‖g x‖) (s : α) (h₂ : HasSum f s) (hg : Summable g)
    (h : ∀ x, Tendsto (f_N x) atTop (𝓝 (f x))) : Tendsto (fun n ↦ ∑' x, f_N x n) atTop (𝓝 s) := by
  sorry

[Gareth Ma]

I think so

[Gareth Ma]

If you have time, can you try to prove it by applying DCT with the counting measure? Or I think this is a simpler version:

example {α : Type*} {β : Type*} [NormedAddCommGroup α]
    (f_N : β → ℕ → α) (g : β → α) (f : β → α)
    (dom : ∀ x N, ‖f_N x N‖ ≤ ‖g x‖) (hg : Summable g) (h : ∀ x, Tendsto (f_N x) atTop (𝓝 (f x))) :
    HasSum (fun n ↦ ∑' x, f_N x n) (∑' x, f x) := by

I tried but I am not familiar with the measure theory / analysis part of Mathlib at all :(