Zulip Chat Archive
Stream: Is there code for X?
Topic: If summable, then tsum is equal to partial sum plus tail
Alex Kontorovich (Apr 05 2024 at 12:41):
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 (Apr 05 2024 at 12:42):
Alex Kontorovich (Apr 05 2024 at 12:43):
Argh! Why doesn't exact?
find it...? :( Thanks!!
Yaël Dillies (Apr 05 2024 at 12:43):
because it's stated using Finset.range
, not Finset.Icc
Sébastien Gouëzel (Apr 05 2024 at 12:44):
Note that your version is wrong for N = 0
...
Alex Kontorovich (Apr 05 2024 at 12:48):
Argh. I see, so Finset.range N
is not the same thing as Finset.Icc 0 (N-1)
when N=0
...
Alex Kontorovich (Apr 05 2024 at 12:49):
That's why docs#Finset.range_eq_Ico uses Ico
and not Icc
. Got it.
Alex Kontorovich (Apr 05 2024 at 12:50):
While I'm asking stupid questions, do we have glue to connect Ico 0 N
with Icc 0 (N-1)
?
Alex Kontorovich (Apr 05 2024 at 12:50):
(When N \ge 1
)
Michael Stoll (Apr 05 2024 at 12:51):
@loogle |- Set.Ico _ _ = Set.Icc _ _
loogle (Apr 05 2024 at 12:51):
:search: Order.Ico_succ_right, Order.Ico_succ_right_of_not_isMax
Michael Stoll (Apr 05 2024 at 12:51):
The first one looks close...
Alex Kontorovich (Apr 05 2024 at 12:54):
@loogle |- Finset.Ico _ _ = Finset.Icc _ _
Michael Stoll (Apr 05 2024 at 12:54):
(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 (Apr 05 2024 at 12:55):
@loogle Finset.Ico _ _ = Finset.Icc _ _
loogle (Apr 05 2024 at 12:55):
:search: Nat.Ico_succ_right
Michael Stoll (Apr 05 2024 at 12:55):
@loogle |- Finset.Ico _ _ = Finset.Icc _ _
loogle (Apr 05 2024 at 12:55):
:search: Nat.Ico_succ_right
Yaël Dillies (Apr 05 2024 at 12:56):
Alex Kontorovich said:
While I'm asking stupid questions, do we have glue to connect
Ico 0 N
withIcc 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 (Apr 05 2024 at 12:57):
The layout in mathlib is currently weird, so my plan is to first get #11765 in then add a bunch of lemmas
Alex Kontorovich (Apr 05 2024 at 12:59):
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 (Apr 05 2024 at 13:37):
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 (Apr 05 2024 at 13:53):
Yes I'm sure you're right and I should refactor what I'm doing...
Last updated: May 02 2025 at 03:31 UTC