ValeZAA

Formalize in Lean 4 that every grouping of convergent series is convergent to the the same sum. Grouping is not a rearrangement.
Okay, so I need to formalize in Lean 4 that every grouping of a convergent series is convergent to the same sum. And the user mentioned that grouping is not a rearrangement. Hmm. Let me start by recalling what this means in real analysis.

First, a convergent series means that the partial sums approach a specific limit. Grouping here refers to adding parentheses around certain terms, creating a new series where each term is the sum of a group of original terms. For example, if the original series is a₁ + a₂ + a₃ + a₄ + ..., a grouping might be (a₁ + a₂) + (a₃ + a₄) + ..., forming a new series with terms b₁ = a₁ + a₂, b₂ = a₃ + a₄, etc. The theorem states that if the original series converges to sum S, then the grouped series also converges to S, provided that the grouping doesn't rearrange the terms, just adds parentheses.

So, to formalize this in Lean 4, I need to work with the de