# Zulip Chat Archive

## Stream: new members

### Topic: Candidate for inclusion in mathlib

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

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

#### Reid Barton (May 14 2020 at 21:18):

Yes, the second one is useful for sure.

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

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

#### Patrick Stevens (May 14 2020 at 21:52):

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

#### Johan Commelin (May 15 2020 at 03:11):

@Patrick Stevens It's on the merge queue

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

.

#### Johan Commelin (May 15 2020 at 03:13):

Ooh, never mind. I can't read.

#### Johan Commelin (May 15 2020 at 03:13):

Please use more notation.

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

.

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

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

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

#### Johan Commelin (May 15 2020 at 13:10):

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

#### 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: Dec 20 2023 at 11:08 UTC