Subtracting a partial sum from a sum

Stream: new members

[Mark Gerads]

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]

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]

That theorem is false?

[Mario Carneiro]

Or rather the lemma needs a + i in it

[Mark Gerads]

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

[Mario Carneiro]

Not the original goal, the proposed lemma is not correct

[Mario Carneiro]

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]

Fixed?

[Mario Carneiro]

:+1:

[Mark Gerads]

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]

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

[Mario Carneiro]

but it should be a one liner

[Eric Wieser]

Can you give a #mwe complete with imports?

[Mark Gerads]

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]

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

[Eric Wieser]

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

[Mark Gerads]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

Interesting. I will play around with it.

[Kevin Buzzard]

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]

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]

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

[Eric Wieser]

Ah right - removing f 0 vs f n

[Eric Wieser]

A sum_range_add lemma would be a nice first contribution to mathlib

[Mark Gerads]

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]

Maybe I should play the natural number game first.

[Mark Gerads]

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]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Adam Topaz]

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]

And THAT would be called sum_union

[Eric Wieser]

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

[Eric Wieser]

Which would be proved trivially from the lemma you suggest

[Adam Topaz]

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

[Eric Wieser]

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

[Adam Topaz]

Oh sure

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

imo it should probably be generalized

[Mark Gerads]

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]

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]

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]

Should I make a pull request for this?

[Mark Gerads]

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

[Yakov Pechersky]

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]

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

[Mark Gerads]

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]

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]

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

[Bryan Gin-ge Chen]

@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]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

But feel free to ask for help here as well!

[Eric Wieser]

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]

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

[Mark Gerads]

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

[Mark Gerads]

I'll just follow the instruction at the link.

[Moritz Firsching]

try git push --set-upstream origin your_branch_name

[Eric Wieser]

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

[Eric Wieser]

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