If summable, then tsum is equal to partial sum plus tail

Stream: Is there code for X?

[Alex Kontorovich]

I can't seem to find something like this, breaking a sum on ℕ into the first few terms plus the rest? Thanks!

import Mathlib

open BigOperators

lemma tsum_eq_partial_add_tail (N : ℕ) (f : ℕ → ℂ) (hf : Summable f) :
  ∑' (n : ℕ), f n =
   (∑ n in Finset.Icc 0 (N - 1), f n) + ∑' (n : ℕ), f (n + N) := by
  sorry

[Yaël Dillies]

docs#sum_add_tsum_nat_add

[Alex Kontorovich]

Argh! Why doesn't exact? find it...? :( Thanks!!

[Yaël Dillies]

because it's stated using Finset.range, not Finset.Icc

[Sébastien Gouëzel]

Note that your version is wrong for N = 0...

[Alex Kontorovich]

Argh. I see, so Finset.range N is not the same thing as Finset.Icc 0 (N-1) when N=0...

[Alex Kontorovich]

That's why docs#Finset.range_eq_Ico uses Ico and not Icc. Got it.

[Alex Kontorovich]

While I'm asking stupid questions, do we have glue to connect Ico 0 N with Icc 0 (N-1)?

[Alex Kontorovich]

(When N \ge 1)

[Michael Stoll]

@loogle |- Set.Ico _ _ = Set.Icc _ _

[loogle]

:search: Order.Ico_succ_right, Order.Ico_succ_right_of_not_isMax

[Michael Stoll]

The first one looks close...

[Alex Kontorovich]

@loogle |- Finset.Ico _ _ = Finset.Icc _ _

[Michael Stoll]

(If you type "@loo" and then click on the right name in the pop-up window, it should work.)
(But I think, editing an old message will not do it.)

[Alex Kontorovich]

@loogle Finset.Ico _ _ = Finset.Icc _ _

[loogle]

:search: Nat.Ico_succ_right

[Michael Stoll]

@loogle |- Finset.Ico _ _ = Finset.Icc _ _

[loogle]

:search: Nat.Ico_succ_right

[Yaël Dillies]

Alex Kontorovich said:

While I'm asking stupid questions, do we have glue to connect Ico 0 N with Icc 0 (N-1)?

Yesn't. I wrote a very barebones API ages ago, but we're still missing a lot of lemmas

[Yaël Dillies]

The layout in mathlib is currently weird, so my plan is to first get #11765 in then add a bunch of lemmas

[Alex Kontorovich]

Hm, I seem to have gotten it to work with existing API (once the statement was corrected):

import Mathlib

open BigOperators

lemma tsum_eq_partial_add_tail {N : ℕ} (hN : 1 ≤ N) (f : ℕ → ℂ) (hf : Summable f) :
  ∑' (n : ℕ), f n =
   (∑ n in Finset.Icc 0 (N - 1), f n) + ∑' (n : ℕ), f (n + N) := by
  rw [← sum_add_tsum_nat_add (f := f) (h := hf) (k := N)]
  congr
  rw [Finset.range_eq_Ico, ← Nat.Ico_succ_right]
  congr
  rw [← Nat.sub_add_cancel hN]
  simp only [add_tsub_cancel_right]

Certainly not the "slickest" solution, lots of golf possibilities...

[Sébastien Gouëzel]

But are you sure you want to sum over Finset.Icc? We use Finset.Ico or finset.range because in general it's better behaved, as you can see in the above example -- and since we use it more this means that there will be more API around it, which makes it easier to use for yet another reason. Of course in some situations you don't really have a choice, but if you do have a choice my advice would be to use Finset.range.

[Alex Kontorovich]

Yes I'm sure you're right and I should refactor what I'm doing...