# Zulip Chat Archive

## Stream: maths

### Topic: Binomial theorem

#### Nicholas Scheel (Jun 08 2018 at 19:07):

Hey! I proved the binomial theorem, if anyone finds it interesting its in a gist here: https://gist.github.com/MonoidMusician/ad43301ee3b4e71c0e1c3d440c6898c5

#### Nicholas Scheel (Jun 08 2018 at 19:08):

just curious: is there an existing definition of the binomial coefficient anywhere, maybe with some lemmas? I couldn't find one

#### Kevin Buzzard (Jun 08 2018 at 19:11):

@Chris Hughes did this but I'm not sure it ever made it into mathlib. I think Chris did pretty much everything in my introduction to proof course. He even did the multinomial theorem (I think this is one of the reasons he's so good at finite stuff :-) )

#### Chris Hughes (Jun 08 2018 at 19:28):

just curious: is there an existing definition of the binomial coefficient anywhere, maybe with some lemmas? I couldn't find one

`data.nat.choose`

#### Scott Morrison (Jun 11 2018 at 08:41):

Hi @Nicholas Scheel , it would be great to PR this into mathlib. (@Chris Hughes, too :-)

#### Chris Hughes (Jun 11 2018 at 17:05):

Hi @Nicholas Scheel , it would be great to PR this into mathlib. (@Chris Hughes, too :-)

The main reason I didn't do this, is we don't have a sensible definition of sums between naturals yet.

#### Kevin Buzzard (Jun 11 2018 at 17:45):

You mean sums from a to b? Mario always argued that you should do sums from a to a+b (or perhaps a+b-1) and seeing the troubles Patrick had when summing from a to b I am inclined to take Mario's word for it. I know from years of worrying about this sort of thing that I'm completely happy to see a sum from i to j if (and only if) j>=i-1, but if j<i-1 then I always feel something has gone wrong.

#### Chris Hughes (Jun 11 2018 at 18:32):

I'm just waiting for some definition to end up in the library. I actually needed non commutative products for Sylow, so it would be useful if Patrick PRed his big operators.

#### Patrick Massot (Jun 11 2018 at 18:54):

I'm sorry I don't have a lot of time for Lean, and it seemed more fun to jump on the perfectoid train because it means team work. But help is very much welcome on the bigop front.

#### Kevin Buzzard (Jun 11 2018 at 18:55):

Last time I looked you were doing great with the bigop thing, there didn't seem to be any problems like there were with type class inference for the modules, and I was just leaving you to do it. Then you went back to the normed vector spaces and had type class problems again, which to be honest was a bit depressing, all I remember was the CS people talking about how interesting out_param was. What is the current state of the bigop stuff?

#### Patrick Massot (Jun 11 2018 at 18:59):

I got tired of nat substraction mainly, especially since `cooper`

seems to promise to make all this easier

#### Oliver Nash (Apr 29 2021 at 14:22):

I need to use the binomial theorem and I'm wondering about whether it is currently stated in the most convenient form.

We have it here: docs#commute.add_pow and I can think of at least two variations that might be preferable, specifically `add_pow₂`

and `add_pow₃`

in the following snippet:

#### Oliver Nash (Apr 29 2021 at 14:23):

```
import data.nat.choose.sum
import algebra.big_operators.finprod
namespace commute
open_locale big_operators
open finset nat
variables {R : Type*} [semiring R] {x y : R} (h : commute x y) (n : ℕ)
include h
-- 1. The statement as currently found in `src/data/nat/choose/sum.lean`
lemma add_pow₁ :
(x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * choose n m :=
h.add_pow n
-- 2. The statement I was expecting
lemma add_pow₂ :
(x + y) ^ n = ∑ m in range (n + 1), choose n m • (x ^ m * y ^ (n - m)) :=
by simp_rw [_root_.nsmul_eq_mul, cast_comm, h.add_pow n]
-- 3. We could even switch to the fancy new `finsum`
lemma add_pow₃ :
(x + y) ^ n = ∑ᶠ m ≤ n, choose n m • (x ^ m * y ^ (n - m)) :=
by simp [_root_.nsmul_eq_mul, cast_comm, h.add_pow n, ← finsum_mem_coe_finset, lt_succ_iff]
end commute
```

#### Oliver Nash (Apr 29 2021 at 14:27):

I'd be grateful for feedback on which of the following might be welcome:

- Change the statement to that of
`add_pow₂`

and refactor accordingly (fortunately it's not heavily used, so this would be easily doable) - Leave the current statement but add the alternate form
`add_pow₂`

(probably called`add_pow'`

I guess) - Similar to 2, but with
`add_pow₃`

- Leave everything as it is
- Something else?

#### Kevin Buzzard (Apr 29 2021 at 15:41):

You can also sum over `finset.nat.antidiagonal`

!

This came up a load when Ashvni and others were thinking about Bernoulli numbers and Bernoulli polynomials. I had just assumed that `finset.nat.antidiagonal`

would be the way to go (there was a long discussion about this, where I was even railing about the definition of `choose n m`

and arguing that the correct object was $f(i,j):=(i+j)!/i!j!$). But ultimately I came to the conclusion that whatever you chose, there was some pain involved. The perceived advantage of using `antidiagonal`

was that you don't have the `nat.sub`

in there, but somehow you still end up battling type theory anyway.

The definition of Bernoulli numbers is by well-founded recursion

```
def bernoulli' : ℕ → ℚ :=
well_founded.fix lt_wf $
λ n bernoulli', 1 - ∑ k : fin n, n.choose k / (n - k + 1) * bernoulli' k k.2
```

and it took me a while to decide which order to put `n.choose k / (n - k + 1) * bernoulli' k k.2`

but ultimately I am not convinced that it mattered much -- you make a "random" choice and then you battle through what you need to battle through.

Basically what I'm saying is that I kind of conjecture that all definitions will end up being mildly inconvenient and about the same amount of work. I did manage to convince myself though that one should have a "rule of thumb" about where the nats go and where the other stuff (in the Bernoulli case, rationals) go, and my rule was "keep the nats at the beginning", so I think I'd prefer 2 or 3 over 1. Whether finset.sum or finsum is best for you I think depends very much on your use case, by which I mean that I suspect you can't please all of the people all of the time so you'd be better off pleasing yourself.

#### Oliver Nash (Apr 29 2021 at 15:52):

Thanks for such a comprehensive answer. I will try the idea to sum over `finset.nat.antidiagonal`

if only because I think it will enable me to avoid having the following revolting lemma:

```
lemma foo (a b i : ℕ) : a ≤ i ∨ b ≤ a + b - 1 - i := by omega
```

for which I'm struggling to get a non-ridiculous proof that does not use `omega`

(which I believe is banned because of Lean 4).

#### Oliver Nash (Apr 29 2021 at 15:53):

(for clarity, `foo`

is required downstream in a separate proof when I use `add_pow₂`

or `add_pow₃`

)

#### Kevin Buzzard (Apr 29 2021 at 16:06):

```
import tactic
lemma foo (a b i : ℕ) : a ≤ i ∨ b ≤ a + b - 1 - i :=
begin
rw or_iff_not_imp_left,
intro h,
push_neg at h,
rcases nat.exists_eq_add_of_lt h with ⟨c, rfl⟩,
rw nat.succ_add_sub_one,
apply nat.le_sub_left_of_add_le,
simp,
end
```

#### Yakov Pechersky (Apr 29 2021 at 16:29):

```
lemma foo (a b i : ℕ) : a ≤ i ∨ b ≤ a + b - 1 - i :=
begin
cases le_or_gt a i with h h,
{ exact or.inl h },
{ rw [nat.add_comm, nat.sub_sub, nat.add_comm 1, nat.add_sub_assoc (nat.succ_le_of_lt h)],
exact or.inr (nat.le_add_right _ _) }
end
```

#### Yakov Pechersky (Apr 29 2021 at 16:30):

Basically the same

#### Oliver Nash (Apr 29 2021 at 19:28):

I decided to make a PR to try to settle this.

#### Scott Morrison (Apr 29 2021 at 23:02):

Did you experiment with making your `add_pow'`

the "main" (unprimed) version? I'd be curious to know whether it helps or hinders in the rest of the library.

#### Oliver Nash (Apr 30 2021 at 07:52):

Very good question @Scott Morrison , I'll try that out this morning.

#### Oliver Nash (May 02 2021 at 19:57):

Scott Morrison said:

Did you experiment with making your

`add_pow'`

the "main" (unprimed) version? I'd be curious to know whether it helps or hinders in the rest of the library.

I made a partial attempt to address this with this commit from which I concluded:

- There are only 8 (by my count) uses of the binomial theorem so the absolute impact is low.
- In terms of relative impact, it's not trivial to decide which form would help/hinder most because the code surrounding invocations of
`add_pow`

tends to caters for the exact form of the lemma as it stands (example).

#### Oliver Nash (May 02 2021 at 19:58):

For the sake of resolving #7415, I have picked just one restatement which I think is worth having (and which I want to use in other work) and have added a commit so the the PR now proposes just this.

#### Oliver Nash (May 02 2021 at 20:01):

Proofs of various alternate forms that I explored are contained in previous commits on that PR including the following appealing statement that @Eric Wieser suggested:

```
(x + y) ^ n = ∑ᶠ m p (h : m + p = n), choose n m • (x ^ m * y ^ p)
```

but I have decided to leave these out.

Last updated: May 11 2021 at 16:22 UTC