## Stream: new members

### Topic: Subtracting a partial sum from a sum

#### Mark Gerads (Feb 28 2021 at 11:18):

I have this:

k: ℕ+
z: ℂ
ε: ℝ
H: ε > 0
⊢ ∃ (i : ℕ), ∀ (j : ℕ), i ≤ j → abs' (∑ (x : ℕ) in range j, abs (z ^ (x * ↑k)) / ↑(x * ↑k)! - ∑ (x : ℕ) in range i, abs (z ^ (x * ↑k)) / ↑(x * ↑k)!) < ε


How do I rewrite this goal in the form ∑ (x : ℕ) in range (j - i), abs (z ^ (x * ↑(k + i))) / ↑(x * ↑(k + i))!?

#### Mark Gerads (Feb 28 2021 at 11:31):

I suspect there should be a lemma somewhere in the library for f: ℕ→ℂ
∀ (i : ℕ), ∀ (j : ℕ), i ≤ j → ∑ (x : ℕ) in range j, f x - ∑ (x : ℕ) in range i, f x = ∑ (x : ℕ) in range (j - i), f (x + i)
Actually, there should be something more general than this where f: ℕ→{some arbitrary structure with addition}.

#### Mario Carneiro (Feb 28 2021 at 11:34):

That theorem is false?

#### Mario Carneiro (Feb 28 2021 at 11:35):

Or rather the lemma needs a + i in it

#### Mark Gerads (Feb 28 2021 at 11:35):

Oh, I forgot i ≤ j. Did I forget anything else?
Copy pasted, and did not edit properly.

#### Mario Carneiro (Feb 28 2021 at 11:36):

Not the original goal, the proposed lemma is not correct

#### Mario Carneiro (Feb 28 2021 at 11:36):

There should be something along the lines range (a + b) = range a ++ map (+a) (range b) which can be transformed into something like your lemma

Fixed?

:+1:

#### Mark Gerads (Feb 28 2021 at 11:38):

I'll try to prove my lemma myself while waiting for feedback. It seems like something someone else would have already done though.

#### Mario Carneiro (Feb 28 2021 at 11:40):

This should be in algebra.big_operators.basic but it's not

#### Mario Carneiro (Feb 28 2021 at 11:41):

but it should be a one liner

#### Eric Wieser (Feb 28 2021 at 11:41):

Can you give a #mwe complete with imports?

#### Mark Gerads (Feb 28 2021 at 11:46):

import data.complex.basic

open_locale classical big_operators nat

open finset

lemma subtract_subsum_from_sum (i : ℕ) (j : ℕ) (f : ℕ → ℂ):
i ≤ j → ∑ (x : ℕ) in range j, f x
- ∑ (x : ℕ) in range i, f x
= ∑ (x : ℕ) in range (j - i), f (x + i):=
begin
sorry
end


#### Eric Wieser (Feb 28 2021 at 11:47):

It probably is easier to prove if you replace j with i+k and eliminate the hypothesis

#### Eric Wieser (Feb 28 2021 at 11:47):

Although that's not to say that what you have isn't also a useful lemma

#### Mark Gerads (Feb 28 2021 at 12:11):

Do we at least have a lemma like this in the library?

import data.complex.basic

open_locale classical big_operators nat

open finset

lemma take_first_from_sum (j : ℕ) (f : ℕ → ℂ):
1 ≤ j → ∑ (x : ℕ) in range j, f x
- f 0
= ∑ (x : ℕ) in range (j - 1), f (x + 1):=
begin
sorry
end


#### Kevin Buzzard (Feb 28 2021 at 12:15):

That's docs#finset.sum_range_succ' except that you made it harder by using the poorly-behaved subtraction function on the naturals. Why not let k be j-1 and then you can avoid subtraction on naturals and dump your hypothesis

#### Mark Gerads (Feb 28 2021 at 12:19):

I don't know how to do that; I am still a beginner.

#### Kevin Buzzard (Feb 28 2021 at 12:22):

import data.complex.basic

open_locale classical big_operators nat

open finset

lemma take_first_from_sum (j : ℕ) (f : ℕ → ℂ):
1 ≤ j → ∑ (x : ℕ) in range j, f x
- f 0
= ∑ (x : ℕ) in range (j - 1), f (x + 1):=
begin
intro h,
set k := j - 1 with hk,
have hj : j = k + 1,
rw hj, -- no more j
rw sum_range_succ',
simp,
end


#### Mark Gerads (Feb 28 2021 at 12:26):

Nice, Thanks! I think that can be used with induction to get

lemma subtract_subsum_from_sum (i : ℕ) (j : ℕ) (f : ℕ → ℂ):
i ≤ j → ∑ (x : ℕ) in range j, f x
- ∑ (x : ℕ) in range i, f x
= ∑ (x : ℕ) in range (j - i), f (x + i):=


Having this in Mathlib is worthwhile, IMO.

#### Kevin Buzzard (Feb 28 2021 at 12:26):

In general subtraction on the complexes is fine, but subtraction on the naturals involves a lot of faffing around because 2 - 3 = 0 (it has to be a natural because the type of subtraction is X -> X -> X) and a lot of the lemmas about subtraction come with extra hypotheses and are a pain to use. In your original question you have a hypothesis i <= j and are then using j - i: the proposal is that instead you define k := j - i and then kill j completely and use i + k instead. It will make things much smoother.

#### Mark Gerads (Feb 28 2021 at 12:28):

Interesting. I will play around with it.

#### Kevin Buzzard (Feb 28 2021 at 12:29):

Mathematically the statements are equivalent, but in practice the i + k version is better because it doesn't have the auxiliary hypothesis so is easier to use directly in things like rewrites.

#### Kevin Buzzard (Feb 28 2021 at 12:30):

The i + k version will be in mathlib already, or perhaps a combination of two lemmas: we have Ico a b, the naturals a<=n<b, and a bunch of lemmas about summing over that finite set.

#### Eric Wieser (Feb 28 2021 at 12:31):

What's the unprimed version, docs#finset.sum_range_succ?

#### Eric Wieser (Feb 28 2021 at 12:32):

Ah right - removing f 0 vs f n

#### Eric Wieser (Feb 28 2021 at 12:32):

A sum_range_add lemma would be a nice first contribution to mathlib

#### Mark Gerads (Feb 28 2021 at 13:03):

lemma sum_range_add {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) :
(∑ x in range (n + m), f x) =
(∑ x in range n, f x) + (∑ x in range m, f (x + n)) :=


to mathlib/src/algebra/big_operators/basic.lean? I will see what I can do, I hope someone else adds it if I don't.

#### Mark Gerads (Feb 28 2021 at 13:05):

Maybe I should play the natural number game first.

#### Mark Gerads (Feb 28 2021 at 18:46):

I proved it, but it is a monstrosity... far from a one-liner.

lemma sum_range_add {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) :
(∑ x in range (n + m), f x) =
(∑ x in range n, f x) + (∑ x in range m, f (x + n)) :=
begin
induction n with d hd,
simp,
have hsucc : d.succ + m = d + m + 1,
rw hsucc,
rw (sum_range_succ f (d + m)),
have hsucc2 : d.succ = d + 1,
refl,
rw hsucc2,
rw (sum_range_succ f d),
simp,
rw hd,
have h3 : ∑ (x : ℕ) in range  m     , f (x + (d + 1)) + f d =
∑ (x : ℕ) in range (m + 1), f (x +  d     ),
rw sum_range_succ' (λ a, f (a + d)),
simp,
have h4 : (∀ x : ℕ, x + (d + 1) = x + 1 + d),
have h5 : ∑ (x : ℕ) in range m, f (x + (d + 1))
= ∑ (i : ℕ) in range m, f (i + 1 + d),
refine congr rfl _,
refine funext _,
intros x,
exact congr_arg f (h4 x),
rw h5,
have h6 : f d + (range d).sum f = (range d).sum f + f d,
exact add_comm (f d) ((range d).sum f),
rw h6,
have h7 : f d + ∑ (x : ℕ) in range m, f (x + (d + 1))
= ∑ (x : ℕ) in range m, f (x + (d + 1)) + f d,
exact add_comm (f d) (∑ (x : ℕ) in range m, f (x + (d + 1))),
have h8 : (range d).sum f + f d + ∑ (x : ℕ) in range m, f (x + (d + 1))
= (range d).sum f + (f d + ∑ (x : ℕ) in range m, f (x + (d + 1))),
exact add_assoc ((range d).sum f) (f d) (∑ (x : ℕ) in range m, f (x + (d + 1))),
rw h8,
rw h7,
rw h3,
rw add_left_comm (f (d + m)) (∑ (x : ℕ) in range d, f x) (∑ (x : ℕ) in range m, f (x + d)),
rw sum_range_succ (λ a, f (a + d)) m,
end


#### Adam Topaz (Feb 28 2021 at 18:50):

Presumably we should have something like an inclusion/exclusion lemma for finest.sum

#### Eric Wieser (Feb 28 2021 at 18:50):

Have a look at src#finset.sum_range_succ' for some inspiration on how to shorten that. I'd expect you you want to use docs#finset.range_add and docs#finset.sum_union or something like that. If those lemmas don't exist, then probably you want to write those too.

#### Adam Topaz (Feb 28 2021 at 18:52):

Why isn't finset.sum_union called finset.sum_disjoint_union?

#### Eric Wieser (Feb 28 2021 at 18:52):

Because the expression it applies to is finset.sum (union a b)

#### Eric Wieser (Feb 28 2021 at 18:52):

disjoint is just the condition necessary for it to be true, it's not part of the goal state

#### Adam Topaz (Feb 28 2021 at 18:53):

Ok, but you you might want to know that the sum over a union in general is the sum of the individual components minus the sum over the intersection.

#### Adam Topaz (Feb 28 2021 at 18:53):

And THAT would be called sum_union

#### Eric Wieser (Feb 28 2021 at 18:53):

Good point - I guess when someone adds that lemma it should be renamed sum_union_of_disjoint or similar

#### Eric Wieser (Feb 28 2021 at 18:54):

Which would be proved trivially from the lemma you suggest

#### Adam Topaz (Feb 28 2021 at 18:54):

That's the exclusion/inclusion thing I was referring too

#### Eric Wieser (Feb 28 2021 at 18:55):

The lemma that's already there should be enough for this thread though

Oh sure

#### Yakov Pechersky (Feb 28 2021 at 18:56):

A simpler induction proof:

lemma sum_range_add {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) :
(∑ x in finset.range (n + m), f x) =
(∑ x in finset.range n, f x) + (∑ x in finset.range m, f (x + n)) :=
begin
induction m with m hm,
{ simp },
{ rw [nat.add_succ, finset.sum_range_succ, hm, finset.sum_range_succ,
end


#### Yakov Pechersky (Feb 28 2021 at 18:59):

imo it should probably be generalized

#### Mark Gerads (Feb 28 2021 at 19:03):

I suppose, so long as this result is accessible. It is quite useful for showing infinite sums are Cauchy. What generalization do you propose?

#### Eric Wieser (Feb 28 2021 at 19:05):

I'd probably have the conclusion be n + x not x + n, so that n is added on the right uniformly through the lemma

#### Mark Gerads (Feb 28 2021 at 19:14):

That does make it shorter.

lemma sum_range_add {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) :
(∑ x in range (n + m), f x) =
(∑ x in range n, f x) + (∑ x in range m, f (n + x)) :=
begin
induction m with m hm,
{ simp },
{ rw [nat.add_succ, finset.sum_range_succ, hm, finset.sum_range_succ,
end


#### Mark Gerads (Feb 28 2021 at 19:20):

Should I make a pull request for this?

#### Yakov Pechersky (Feb 28 2021 at 19:51):

Stubbing out the actual sublemma:

lemma finset.range_add (n m : ℕ) :
finset.range (n + m) = finset.range n ∪ (finset.range m).image (λ x, n + x) :=
begin
induction m with m hm,
{ simp },
{ simp [nat.add_succ, finset.range_succ, hm] }
end

lemma sum_range_add {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) :
(∑ x in finset.range (n + m), f x) =
(∑ x in finset.range n, f x) + (∑ x in finset.range m, f (n + x)) :=
begin
convert finset.sum_union _ using 1,
{ simp [finset.sum_image] },
{ refine finset.disjoint_iff_ne.mpr _,
simp only [and_imp, finset.mem_image, ne.def, forall_apply_eq_imp_iff₂,
finset.mem_range, exists_imp_distrib],
intros x hx _ _,
exact ne_of_lt (nat.lt_add_right _ _ _ hx) }
end


#### Yakov Pechersky (Feb 28 2021 at 19:52):

Of course, it makes the latter proof look more complicated. There's probably some golfing possible.

#### Mark Gerads (Feb 28 2021 at 19:58):

I now have this:

lemma prod_range_add (f : ℕ → β) (n : ℕ) (m : ℕ) :
(∏ x in range (n + m), f x) =
(∏ x in range n, f x) * (∏ x in range m, f (n + x)) :=
begin
induction m with m hm,
{ simp },
{ rw [nat.add_succ, finset.prod_range_succ, hm, finset.prod_range_succ, mul_left_comm _ _ _] },
end


#### Mark Gerads (Feb 28 2021 at 20:04):

And this seems to work, though I was just guessing.

lemma sum_range_add {β} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) :
(∑ x in range (n + m), f x) =
(∑ x in range n, f x) + (∑ x in range m, f (n + x)) :=
@prod_range_add (multiplicative β) _ _ _ _


#### Mark Gerads (Feb 28 2021 at 20:19):

I put these 2 in a pull request: https://github.com/leanprover-community/mathlib/pull/6483

#### Bryan Gin-ge Chen (Feb 28 2021 at 20:23):

@Mark Gerads I mentioned this briefly when I closed the previous PR, but I probably wasn't clear. Our CI scripts will only run on PRs made from branches in the main mathlib repo, not forks. Can you push your work to a new branch in the mathlib repo and open a PR from there?

(We set things up like this because the CI scripts upload files containing compiled versions of branch heads to an Azure server for use by leanproject.)

#### Mark Gerads (Feb 28 2021 at 20:26):

Hmmm. I have not used git this way before. Is there an example?
I will try to figure it out.

#### Bryan Gin-ge Chen (Feb 28 2021 at 20:27):

There are some instructions (and even a tutorial video) on our community site here.

#### Bryan Gin-ge Chen (Feb 28 2021 at 20:28):

But feel free to ask for help here as well!

#### Eric Wieser (Feb 28 2021 at 20:30):

git remote set-url origin <the url you have now but with leanprover-community instead of your name> is all you need to do

#### Bryan Gin-ge Chen (Feb 28 2021 at 20:31):

Right, that will make the origin remote (which presumably currently points to your fork) point to leanprover-community/mathlib.

#### Mark Gerads (Feb 28 2021 at 20:33):

If I do a git push, won't it go directly to master without a pull request though?

#### Moritz Firsching (Feb 28 2021 at 20:34):

try git push --set-upstream origin your_branch_name

#### Eric Wieser (Feb 28 2021 at 20:38):

Ah you're right, the way you made the original PR was also not the way it's normally done

#### Eric Wieser (Feb 28 2021 at 20:38):

I'd assumed you'd made a branch in your own local repo, not just used master

Last updated: Dec 20 2023 at 11:08 UTC