Candidate for inclusion in mathlib

Stream: new members

[Patrick Stevens]

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.)

[Patrick Stevens]

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

[Reid Barton]

Yes, the second one is useful for sure.

[Reid Barton]

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).

[Reid Barton]

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

[Patrick Stevens]

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

[Johan Commelin]

@Patrick Stevens It's on the merge queue

[Johan Commelin]

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.

[Johan Commelin]

Ooh, never mind. I can't read.

[Johan Commelin]

Please use more notation.

[Johan Commelin]

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.

[Johan Commelin]

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

[Patrick Stevens]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Patrick Stevens]

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