# Zulip Chat Archive

## 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

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

Fixed?

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

:+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 [hk, nat.sub_add_cancel h],
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):

I suppose you mean adding

```
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,
exact nat.succ_add d m,
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),
intros,exact (nat.succ_add_eq_succ_add x d).symm,
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,
rw add_comm 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

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

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,
add_left_comm, add_comm m n] },
end
```

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

Could @Yakov Pechersky 's proof be added to Mathlib, please?

#### 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,
add_left_comm] },
end
```

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

Should I make a pull request for this?

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

Made one. https://github.com/leanprover-community/mathlib/pull/6482

#### 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
rw finset.range_add,
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 β) _ _ _ _
attribute [to_additive] prod_range_add
```

#### 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?

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

I'll just follow the instruction at the link.

#### 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