(m+n)!/(m!n!)

Stream: Is there code for X?

[Kevin Buzzard]

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]

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]

I think this is a good idea

[Johan Commelin]

how about binom' as name?

[Johan Commelin]

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

[Kevin Buzzard]

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]

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]

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]

how about we call the function pascal?

[Johan Commelin]

pascal a b is "a steps left, b steps right" in Pascal's triangle.

[Adam Topaz]

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]

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]

@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]

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]

Or you could use finsupp

[Adam Topaz]

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

[Adam Topaz]

I guess this general binomial formula should be in mathlib anyway

[Kevin Buzzard]

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]

PS I had to import tactic because I am lazy.

[Bhavik Mehta]

I think there's something in data.nat.choose which should make the last proof easier, possibly

[Bhavik Mehta]

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

[Kyle Miller]

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]

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]

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]

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]

And furthermore I claim that if I define Bernoulli using pascal instead of choose then my proofs will be nicer.

[Kevin Buzzard]

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]

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]

(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]

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]

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]

Yeah that would be fine

[Jz Pan]

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]

sometimes k! is invertible is not necessary, for example x.choose k can be defined for $x\in\mathbb{Z}_p$

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

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

[Jz Pan]

... and local class field theory?

[Kevin Buzzard]

Right

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.