Group an infinite sum into finite sums

Stream: Is there code for X?

[Yaël Dillies]

Is there a way to split an infinite sum into an infinite sum of finite sums (where the domains of the sum form a partition of the original space?

[Yaël Dillies]

Context is I'm trying to generalise

lemma summable_lemma (f : (Fin 2 → ℤ) → ℝ) (h : ∀ y : (Fin 2 → ℤ), 0 ≤ f y)
    (ι : ℕ → Finset (ℤ × ℤ)) (HI : ∀ y : ℤ × ℤ, ∃! i : ℕ, y ∈ ι i) :
      Summable f ↔ Summable fun n : ℕ => ∑ x in ι n, f ![x.1, x.2]

from #10377

[Eric Wieser]

You can there there via an equivalence between the original index type and Prod I think?

[Eric Wieser]

That is, first group into infinite sums, then show that the infinite sums are finite

[Yaël Dillies]

It can't be that easy because (1 - 1) + (1 - 1) + ... is summable while 1 - 1 + 1 - 1 + ... is not

[Yaël Dillies]

cc @Chris Birkbeck

[Yaël Dillies]

Ahah! docs#summable_sigma_of_nonneg

[Chris Birkbeck]

yes I was about to say that. I used it in the PR

[Chris Birkbeck]

This is the reason I had this sigmaEquiv since I needed to turn the domain into a sigma to use this result. Although I didn't think if there was a more direct way to do this.