Triangular infinite sums

Stream: Is there code for X?

[Eric Wieser]

Do we have anything along the lines of:

/-- An infinite triangular sum can be transposed. -/
theorem HasSum_sum_range_iff {α} [TopologicalSpace α] [AddCommMonoid α] [ContinuousAdd α]
    (f : ℕ → ℕ → α) (a : α):
    HasSum (fun n => ∑ k in .range n, f n k) a ↔ HasSum (fun nk : ℕ × ℕ => f (nk.1 + nk.2) nk.2) a :=
  sorry

That is, that $\sum_{n=0}^\infty \sum_{k=0}^n f_{n,k} = \sum_{k=0}^\infty \sum_{n=0}^\infty f_{n+k,k}$? (modulo off-by-one errors)

[Antoine Chambert-Loir]

That's a particular case of Fubini, and it wouldn't bet that it holds without an additional absolute summability assumption.