# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: (m+n)!/(m!n!)

#### Kevin Buzzard (Dec 23 2020 at 15:29):

Do we have `f : nat -> nat -> nat`

defined by `f m n := (m + n).choose n`

? I've been refactoring Bernoulli numbers and I've been working with binomial coefficients `n.choose k`

a lot. One is forever having to carry around a proof of `k <= n`

to ensure that the coefficient does not have pathological behaviour, the basic "symmetry" `n.choose k = n.choose (n - k)`

needs it. And the rewrite lemmas are ugly e.g.

```
lemma choose_mul_succ_eq (n k : ℕ) :
(n.choose k) * (n + 1) = ((n+1).choose k) * (n + 1 - k) :=
```

-- ugh. Is that even the best form? I think `(n - k + 1)`

would be easier to work with because if you have `n.choose k`

then you almost certainly have a proof of `k <= n`

in your context because you need it to do anything. But actually this just a clue that the corresponding theorem for `f`

above will be more beautiful, and indeed it is. Currently Bernoullli numbers are defined in terms of `choose`

but they would be easier to work with, I suspect, if I refactor the entire file and replace the definition with `f`

. What is its name?

#### Kevin Buzzard (Dec 23 2020 at 15:35):

I think I might be saying that there is an argument for interpreting the binomial theorem $(X+Y)^n=\sum_{i=0}^n\binom niX^iY^{n-i}$ as actually a sum over `i : nat.antidiagonal n`

of `f i.1 i.2 * X^i.1 * Y^i.2`

#### Johan Commelin (Dec 23 2020 at 15:38):

I think this is a good idea

#### Johan Commelin (Dec 23 2020 at 15:38):

how about `binom'`

as name?

#### Johan Commelin (Dec 23 2020 at 15:38):

the `'`

should be a warning sign that it's not exactly `binom`

#### Kevin Buzzard (Dec 23 2020 at 15:59):

```
lemma choose_succ_succ (n k : ℕ) : choose (succ n) (succ k) = choose n k + choose n (succ k) := ...
@[simp] lemma bryan_succ_succ (a b : ℕ) :
bryan a.succ b.succ = bryan a b.succ + bryan a.succ b := ...
```

Bryan wins hands down. This must be some standard function in quantum stuff.

#### Johan Commelin (Dec 23 2020 at 16:18):

```
def bryan : ℕ → ℕ → ℕ
| _ 0 := 1
| 0 (b+1) := 1
| (a+1) (b+1) := bryan a (b+1) + bryan (a+1) b
lemma bryan_eq_choose : ∀ (a b : ℕ), bryan a b = nat.choose (a+b) b
| 0 0 := rfl
| (a+1) 0 := rfl
| 0 (b+1) := by { simp only [nat.choose_self, zero_add], refl }
| (a+1) (b+1) :=
calc bryan a (b+1) + bryan (a+1) b
= nat.choose (a+b+1) (b+1) + nat.choose (a+1+b) b : by rw [bryan_eq_choose, bryan_eq_choose]; refl
... = nat.choose (a+1+b) b + nat.choose (a+1+b) (b+1) : by rw [add_comm, add_right_comm]
... = nat.choose (a+1+b+1) (b+1) : rfl
```

#### Adam Topaz (Dec 23 2020 at 16:21):

I don't know who Bryan is, but these coefficients show up in the multiplication table of divided power polynomial algebras. Maybe we can derive a name from that?

#### Johan Commelin (Dec 23 2020 at 16:29):

how about we call the function `pascal`

?

#### Johan Commelin (Dec 23 2020 at 16:29):

`pascal a b`

is "`a`

steps left, `b`

steps right" in Pascal's triangle.

#### Adam Topaz (Dec 23 2020 at 16:38):

I don't know. I would prefer `binom'`

over `pascal`

. Maybe `binom_symm`

to emphasize that it's a symmetric version of `binom`

?

#### Kyle Miller (Dec 23 2020 at 16:40):

What about a generalization, `list.multinomial : list ℕ → ℕ`

where `[c1, ..., cn].multinomial`

is the coefficient of `x1^c1 * ... * xn^cn`

in `(x1 + ... + xn)^(c1 + ... + cn)`

? Then `bryan a b = [a, b].multinomial`

.

#### Eric Wieser (Dec 23 2020 at 16:46):

@Kyle Miller, your proposed `list.multinomial`

is invariant to the order of the list, right? So maybe `multiset.multinomial`

or perhaps a function `(ι → ℕ) → ℕ`

would also make sense, then it would be `multinomial ![a, b]`

#### Kyle Miller (Dec 23 2020 at 16:48):

Indeed, it's invariant under `list.perm`

, so it descends to `multiset`

. With `(ι → ℕ) → ℕ`

, were you thinking that this is whenever `ι`

is a `fintype`

?

#### Adam Topaz (Dec 23 2020 at 16:49):

Or you could use `finsupp`

#### Adam Topaz (Dec 23 2020 at 16:50):

This way the formula could be used in a polynomial ring generated by an arbitrary type :)

#### Adam Topaz (Dec 23 2020 at 16:50):

I guess this general binomial formula should be in mathlib anyway

#### Kevin Buzzard (Dec 23 2020 at 17:18):

Johan suggests `pascal`

which I think is a lovely name if we can't get one. I asked on Twitter . Here's a basic API (with proofs, but it would probably be easier to prove everything from first principles if there is a need):

```
-- pascal
import data.nat.choose.basic
import tactic
open_locale nat
namespace nat
def pascal (a b : ℕ) : ℕ := (a + b).choose a
variables {a b : ℕ}
theorem pascal_def : pascal a b = (a + b)! / (a! * b!) :=
by {unfold pascal,
simp [choose_eq_factorial_div_factorial (le.intro rfl)] }
theorem pascal_spec : a! * b! * pascal a b = (a + b)! :=
by {unfold pascal,
convert choose_mul_factorial_mul_factorial (show a ≤ a + b, by simp) using 1,
rw [nat.sub_eq_of_eq_add rfl, mul_comm, ← mul_assoc]}
theorem pascal_symm : pascal a b = pascal b a :=
by { simp [pascal_def, add_comm, mul_comm] }
@[simp] lemma pascal_zero_right (n : ℕ) : pascal n 0 = 1 := choose_self n
@[simp] lemma pascal_zero_left (n : ℕ) : pascal 0 n = 1 := @pascal_symm n 0 ▸ pascal_zero_right n
@[simp] lemma pascal_one_left (n : ℕ) : pascal 1 n = n.succ :=
by {unfold pascal,
convert choose_one_right n.succ,
apply add_comm }
@[simp] lemma pascal_one_right (n : ℕ) : pascal n 1 = n.succ := @pascal_symm 1 n ▸ pascal_one_left n
@[simp] lemma pascal_succ_succ : pascal a.succ b.succ = pascal a b.succ + pascal a.succ b :=
by {unfold pascal,
convert choose_succ_succ (a + b + 1) a using 3;
simp [succ_add, ← succ_eq_add_one ] }
@[simp] lemma pascal_two_left' (n : ℕ) : pascal 2 n * 2 = n.succ * n.succ.succ :=
begin
induction n with d hd, refl,
rw [pascal_succ_succ, add_mul, hd, pascal_one_left],
simp only [mul_succ, ← succ_eq_add_one, succ_mul],
simp [mul_succ, succ_mul, succ_eq_add_one, add_assoc, add_left_comm]
end
lemma pascal_pos : 0 < pascal a b := choose_pos (show a ≤ a + b, from le.intro rfl)
lemma succ_mul_pascal : (a + b).succ * pascal a b = a.succ * pascal a.succ b :=
begin
unfold pascal,
rw mul_comm a.succ,
convert succ_mul_choose_eq (a + b) a,
exact succ_add a b,
end
lemma succ_mul_pascal' : (a + b).succ * pascal a b = b.succ * pascal a b.succ :=
by rw [pascal_symm, add_comm, succ_mul_pascal, pascal_symm]
lemma succ_mul_pascal'' : a.succ * pascal a.succ b = b.succ * pascal a b.succ :=
by rw [← succ_mul_pascal, succ_mul_pascal']
-- this is strictly stronger than choose_le_succ_of_lt_half_left (edge cases)
lemma pascal_succ_le (h : a ≤ b) : pascal a b.succ <= pascal a.succ b :=
begin
rw ← _root_.mul_le_mul_left
(show 0 < a.succ! * b.succ!, from mul_pos (factorial_pos _) (factorial_pos _)),
suffices : a.succ * (a! * b.succ! * pascal a b.succ) ≤ b.succ * (a.succ! * b! * pascal a.succ b),
convert this using 1,
{ rw factorial_succ a,
ring },
{ rw factorial_succ b, ring },
{ rw [pascal_spec, pascal_spec, succ_add, add_succ],
mono,
{ exact zero_le _},
{ exact succ_le_succ h } }
end
lemma pascal_le_middle : pascal a b ≤ pascal ((a + b) / 2) ((a + b - (a + b) / 2)) :=
sorry
end nat
```

#### Kevin Buzzard (Dec 23 2020 at 17:19):

PS I had to import `tactic`

because I am lazy.

#### Bhavik Mehta (Dec 23 2020 at 17:21):

I think there's something in `data.nat.choose`

which should make the last proof easier, possibly

#### Bhavik Mehta (Dec 23 2020 at 17:21):

```
lemma choose_le_middle (r n : ℕ) : choose n r ≤ choose n (n/2) :=
```

#### Kyle Miller (Dec 23 2020 at 17:49):

If you commit to always writing `(a+b).choose a`

, does there need to be a special name for it? Argument duplication is certainly annoying, but it seems like `pascal`

would lead to API duplication.

I don't know how it looks for the Bernoulli number refactoring, but at least in the code you gave, writing the expanded version seems like it might be ok (except for the last lemma):

```
import data.nat.choose.basic
import tactic
open_locale nat
namespace nat
variables {a b : ℕ}
theorem pascal_def : (a + b).choose a = (a + b)! / (a! * b!) :=
by { simp [choose_eq_factorial_div_factorial (le.intro rfl)] }
theorem pascal_spec : a! * b! * (a + b).choose a = (a + b)! :=
by { convert choose_mul_factorial_mul_factorial (show a ≤ a + b, by simp) using 1,
rw [nat.sub_eq_of_eq_add rfl, mul_comm, ← mul_assoc]}
theorem pascal_symm : (a + b).choose a = (b + a).choose b :=
by rw [pascal_def, pascal_def, add_comm b, mul_comm]
@[simp] lemma pascal_zero_right (n : ℕ) : (n + 0).choose n = 1 := choose_self n
@[simp] lemma pascal_zero_left (n : ℕ) : (0 + n).choose 0 = 1 :=
@pascal_symm n 0 ▸ pascal_zero_right n
@[simp] lemma pascal_one_left (n : ℕ) : (1 + n).choose 1 = n.succ :=
by { convert choose_one_right n.succ, apply add_comm }
@[simp] lemma pascal_one_right (n : ℕ) : (n + 1).choose n = n.succ :=
@pascal_symm 1 n ▸ pascal_one_left n
@[simp] lemma pascal_succ_succ :
(a.succ + b.succ).choose a.succ = (a + b.succ).choose a + (a.succ + b).choose a.succ :=
by { convert choose_succ_succ (a + b + 1) a using 3; simp [succ_add, ← succ_eq_add_one ] }
@[simp] lemma pascal_two_left' (n : ℕ) : (2 + n).choose 2 * 2 = n.succ * n.succ.succ :=
begin
induction n with d hd, refl,
rw [pascal_succ_succ, add_mul, hd, pascal_one_left],
simp only [mul_succ, ← succ_eq_add_one, succ_mul],
simp [mul_succ, succ_mul, succ_eq_add_one, add_assoc, add_left_comm]
end
lemma pascal_pos : 0 < (a + b).choose a := choose_pos (show a ≤ a + b, from le.intro rfl)
lemma succ_mul_pascal : (a + b).succ * (a + b).choose a = a.succ * (a.succ + b).choose a.succ :=
begin
rw mul_comm a.succ,
convert succ_mul_choose_eq (a + b) a,
exact succ_add a b,
end
lemma succ_mul_pascal' : (a + b).succ * (a + b).choose a = b.succ * (a + b.succ).choose a :=
by rw [pascal_symm, add_comm, succ_mul_pascal, pascal_symm]
lemma succ_mul_pascal'' : a.succ * (a.succ + b).choose a.succ = b.succ * (a + b.succ).choose a :=
by rw [← succ_mul_pascal, succ_mul_pascal']
-- this is strictly stronger than choose_le_succ_of_lt_half_left (edge cases)
lemma pascal_succ_le (h : a ≤ b) : (a + b.succ).choose a <= (a.succ + b).choose a.succ :=
begin
rw ← _root_.mul_le_mul_left
(show 0 < a.succ! * b.succ!, from mul_pos (factorial_pos _) (factorial_pos _)),
suffices : a.succ * (a! * b.succ! * (a + b.succ).choose a) ≤ b.succ * (a.succ! * b! * (a.succ + b).choose a.succ),
convert this using 1,
{ rw factorial_succ a,
ring },
{ rw factorial_succ b, ring },
{ rw [pascal_spec, pascal_spec, succ_add, add_succ],
mono,
{ exact zero_le _},
{ exact succ_le_succ h } }
end
lemma pascal_le_middle : (a + b).choose a ≤ (((a + b) / 2) + ((a + b - (a + b) / 2))).choose ((a + b) / 2) :=
sorry
end nat
```

#### Bhavik Mehta (Dec 23 2020 at 17:52):

I think the frustration is that you keep needing to prove `a <= a + b`

each time, but an api for `pascal`

wouldn't need this (correct me if I'm wrong Kevin!)

#### Kevin Buzzard (Dec 23 2020 at 18:14):

This is the correct thing to prove (and it works for me):

```
lemma pascal_le_middle {a b c d : ℕ} (h1 : a ≤ b) (h2 : b ≤ c)
(h3 : a + d = b + c) : pascal a d ≤ pascal b c :=
begin
rw le_iff_exists_add at h1,
cases h1 with n hn,
induction n with n hn hm generalizing b c,
{ simp * at * },
cases b,
{ cases hn_1 },
have hb : b = a + n,
{ rw [← succ_inj', hn_1, add_succ] },
rw [succ_add, ← add_succ] at h3,
exact le_trans (hn (le_trans (le_succ _) (le_trans h2 (le_succ _))) h3 hb)
(pascal_succ_le (le_trans (le_succ _) h2)),
end
```

#### Kevin Buzzard (Dec 23 2020 at 18:17):

Yes this is exactly the issue. When dealing with "trivial" statements about n choose k which follow immediately from the expression in terms of factorials and basic stuff like `factorial_succ`

, you are forever hobbling along because any e.g. casts you're doing won't do `sub`

unless you explicitly tell them to by feeding in the relevant inequality. The API has come out beautifully. `choose`

is defined as junk values if k > n but I think restricting the domain like this gives in some sense a more fundamental function.

#### Kevin Buzzard (Dec 23 2020 at 18:34):

And furthermore I claim that if I define `Bernoulli`

using `pascal`

instead of `choose`

then my proofs will be nicer.

#### Kevin Buzzard (Dec 23 2020 at 18:35):

OK I've pushed a branch `binomial`

. I've build the API mostly from the `choose`

API but I strongly suspect it would have been easier to build it from the ground up, as it's much easier to steer than `choose`

.

#### Kyle Miller (Dec 23 2020 at 19:23):

Kevin Buzzard said:

Yes this is exactly the issue. When dealing with "trivial" statements about n choose k which follow immediately from the expression in terms of factorials and basic stuff like

`factorial_succ`

, you are forever hobbling along because any e.g. casts you're doing won't do`sub`

unless you explicitly tell them to by feeding in the relevant inequality. The API has come out beautifully.`choose`

is defined as junk values if k > n but I think restricting the domain like this gives in some sense a more fundamental function.

The thing I'm wondering about is what `binomial`

/`pascal`

gives you that a bunch of lemmas about expressions of the form `(a+b).choose a`

wouldn't? All I'm really able to see is that you don't have to write the `a`

argument twice.

Secondly (and more importantly), if you're going through the effort of defining `pascal`

, why not do the natural generalization to the multinomial coefficient? This is probably not the best way to define it, but there's at least

```
open_locale nat
def list.multinomial (m : list ℕ) : ℕ := m.sum! / (m.map nat.factorial).prod
lemma multinomial_eq_choose (a b : ℕ) : [a, b].multinomial = (a + b).choose a :=
by simp [list.multinomial, nat.choose_eq_factorial_div_factorial (nat.le.intro rfl)]
```

#### Kyle Miller (Dec 23 2020 at 19:32):

(I'm not against `binomial`

-- I wish this is what mathematicians used rather than `choose`

-- but I'm worrying that `binomial`

is "just" `choose`

, and it will end up involving lots of duplication of the API since you would need to unfold the definition to rewrite.)

#### Kevin Buzzard (Dec 23 2020 at 23:37):

The problem is that in practice you get `n.choose k`

and a proof that `k <= n`

and this is just harder to deal with. The lemmas with `(a+b).choose a`

are nice, but they force the user to get their binomial coefficients into this form. if your "default" API is `binomial`

instead of `choose`

then your proofs are shorter because the API is more natural.

#### Kyle Miller (Dec 24 2020 at 00:29):

Is there some reason though to define `binomial a b`

rather than `[a, b].multinomial`

or something similar? I was thinking that `multinomial`

would be a useful generalization to have, it's not much more complex to define, and it seems to have the properties that you want.

#### Kevin Buzzard (Dec 24 2020 at 00:30):

Yeah that would be fine

#### Jz Pan (Dec 24 2020 at 05:51):

off-topic: I think the binomial polynomial is nice to have, i.e. `x.choose k`

where `k`

is a natural number and `x`

is an element of a ring on which `k!`

is invertible

#### Jz Pan (Dec 24 2020 at 05:53):

sometimes `k!`

is invertible is not necessary, for example `x.choose k`

can be defined for $x\in\mathbb{Z}_p$

#### Kevin Buzzard (Dec 24 2020 at 09:49):

Yes I agree, we will need this very soon in a project a student of mine is working on

#### Adam Topaz (Dec 24 2020 at 14:31):

It would be a nice project to formalize the classification of integer values polynomials :smile:

#### Kevin Buzzard (Dec 24 2020 at 14:56):

That would need Jz Pan's generalisation of `choose`

. In fact there are some subtleties there. As they point out, binomial coefficients can be evaluated if n is a p-adic integer but this isn't true for eg the Witt vectors of a field with p^2 elements.

#### Adam Topaz (Dec 24 2020 at 15:01):

There's a generalization of the integer valued stuff to rings of integers of number fields here:

http://www.ma.huji.ac.il/~deshalit/new_site/files/Integer-valued.pdf

#### Kevin Buzzard (Dec 24 2020 at 15:02):

Yeah we need Lubin-Tate groups too! They're really fun and we have a lot of the framework available.

#### Jz Pan (Dec 28 2020 at 07:43):

... and local class field theory?

#### Kevin Buzzard (Dec 28 2020 at 10:08):

Right

#### Kevin Buzzard (Dec 28 2020 at 10:09):

I have a student who did group cohomology, we should start with the statements

#### Adam Topaz (Dec 28 2020 at 14:30):

Seems to me that there are a LOT of prereqs to get done before one can even define the local reciprocity map...

#### Kevin Buzzard (Dec 28 2020 at 14:45):

Yeah, but from where I'm standing they all look feasible.

#### Kevin Buzzard (Dec 28 2020 at 14:46):

I mean, making the type of the map, not making the map itself! The map itself will be hard work. But first one should state the theorem.

Last updated: May 16 2021 at 05:21 UTC