Proof that every grouping of convergent series is also convergent to the same sum

[ValeZAA]

To formalize that every grouping of a convergent series converges to the same sum in Lean 4, we need to show that the partial sums of the grouped series form a subsequence of the original partial sums. Since the original series converges, any subsequence of its partial sums will also converge to the same limit. Here's the detailed implementation:

theorem hasSum_grouped (a : ℕ → α) (S : α) (k : ℕ → ℕ) (hk : StrictMono k) (hk₀ : k 0 = 0)
  (h : HasSum a S) : HasSum (fun n => ∑ i in Finset.Ico (k n) (k (n + 1)), a i) S := by
  -- Show that the partial sums of the grouped series are a subsequence of the original partial sums.
  have h₁ : Tendsto (fun n => ∑ i in Finset.range (k (n + 1)), a i) atTop (𝓝 S) :=
    h.tendsto_sum_nat.comp (hk.comp_tendsto tendsto_succ_atTop)
  -- Convert the tendsto result to the HasSum statement by equating the partial sums.
  convert HasSum.tendsto_sum_nat _ using 1
  ext n
  -- Simplify the expression to show the equivalence of the partial sums.
  simp [Finset.sum_range_induction, hk, hk₀, Finset.sum_Ico_consecutive]
  <;> linarith [hk.strictMono]

Also, here is a paper that goes even further for functional series, would be good to formalise it.

https://pubs.lib.umn.edu/index.php/mjum/article/download/4158/2849/19184

Finally, this also means that if we suddenly get a divergent series after grouping that means original series is only ever divergent.

P.S. Code written by Deepseek R1, here is the whole Chain of thought. https://gist.github.com/ValeZAA/2217d8d2d41a97f932ee5cc17c6e1a10