## 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
(x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * choose n m :=

-- 2. The statement I was expecting
(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
(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:

1. Change the statement to that of add_pow₂ and refactor accordingly (fortunately it's not heavily used, so this would be easily doable)
2. Leave the current statement but add the alternate form add_pow₂ (probably called add_pow' I guess)
3. Similar to 2, but with add_pow₃
4. Leave everything as it is
5. 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⟩,
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 },
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:

1. There are only 8 (by my count) uses of the binomial theorem so the absolute impact is low.
2. 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