Zulip Chat Archive

Stream: new members

Topic: Candidate for inclusion in mathlib


view this post on Zulip Patrick Stevens (May 14 2020 at 21:13):

One of the lemmas in a proof of Bertrand's postulate is:

lemma sum_halfway_choose (m : nat) : finset.sum (finset.range m.succ) (nat.choose (2 * m + 1)) = 4 ^ m := sorry

Is that the kind of lemma that might go into nat.choose as a standalone thing? (I'm nowhere near finished with Bertrand's postulate itself yet, but there's a number of grubby bounding lemmas that go into it, and this is used for one of them.)

view this post on Zulip Patrick Stevens (May 14 2020 at 21:17):

I'm sure some variation on the below additionally belongs in mathlib somewhere, since it's of standalone interest independent of the binomial theorem:

lemma pascal_row_sum (m : nat) : finset.sum (finset.range m.succ) (λ i, nat.choose m i) = 2 ^ m :=
begin
  let t := (add_pow 1 1 m).symm,
  simp at t,
  exact t,
end

view this post on Zulip Reid Barton (May 14 2020 at 21:18):

Yes, the second one is useful for sure.

view this post on Zulip Reid Barton (May 14 2020 at 21:18):

By the way, another way to write the proof should be by simpa using (add_pow 1 1 m).symm (didn't try it, just mechanically reduced the proof).

view this post on Zulip Reid Barton (May 14 2020 at 21:20):

The first one would be sort of borderline if not for the fact that mathlib should have the proof you are formalizing anyways.

view this post on Zulip Patrick Stevens (May 14 2020 at 21:52):

I raised https://github.com/leanprover-community/mathlib/pull/2684/files for the latter

view this post on Zulip Johan Commelin (May 15 2020 at 03:11):

@Patrick Stevens It's on the merge queue

view this post on Zulip Johan Commelin (May 15 2020 at 03:12):

Concerning your first lemma: the name and the statement don't really match. Which means this should maybe be a helper lemma for the actual sum_halfway_choose.

view this post on Zulip Johan Commelin (May 15 2020 at 03:13):

Ooh, never mind. I can't read.

view this post on Zulip Johan Commelin (May 15 2020 at 03:13):

Please use more notation.

view this post on Zulip Johan Commelin (May 15 2020 at 03:15):

Most simp lemmas use (m+1) instead of m.succ. And the former looks a lot better in my eyes.
More importantly, you can write \sum i in range (m+1), choose (2 * m + 1) i = 4 ^ m.

view this post on Zulip Johan Commelin (May 15 2020 at 03:15):

(You may need to open finset. But that's fine, you can wrap it in a section ... end if you want.

view this post on Zulip Patrick Stevens (May 15 2020 at 13:05):

So I'd like to put into mathlib lemma sum_halfway_choose (m : nat) : finset.sum (finset.range (m + 1)) (nat.choose (2 * m + 1)) = 4 ^ m := sorry (however it's spelt), but the main problem is that my code is presumably absolute garbage; it's 150 lines, for a start. Is the right thing to do simply to make a PR and then let other people tell me how to completely rewrite it? It seems quite labour-intensive and I don't want to simply make work for other people, but I can't contribute without a few rounds of people showing me how to do it correctly

view this post on Zulip Johan Commelin (May 15 2020 at 13:10):

For the first few PRs, that's certainly fine. Probably the first suggestion would be to try to factor out 2 or 3 reusable sublemmas.

view this post on Zulip Johan Commelin (May 15 2020 at 13:10):

And most people won't mind spamming the PR page with little tricks

view this post on Zulip Patrick Stevens (May 15 2020 at 14:49):

Sure, I do have the benefit of being a programmer by trade, so it could certainly be a worse situation :P


Last updated: May 12 2021 at 03:23 UTC