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

@[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] lemma pascal_two_left' (n : ℕ) : pascal 2 n * 2 = n.succ * n.succ.succ :=
begin
induction n with d hd, refl,
simp only [mul_succ, ← succ_eq_add_one, succ_mul],
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,
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 },
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,
simp only [mul_succ, ← succ_eq_add_one, succ_mul],
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,
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 },
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
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] },
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?

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