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