Binomial theorem

Stream: maths

[Nicholas Scheel]

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

[Nicholas Scheel]

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

[Kevin Buzzard]

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

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]

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

[Chris Hughes]

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]

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]

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]

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]

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]

I got tired of nat substraction mainly, especially since cooper seems to promise to make all this easier

[Oliver Nash]

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]

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]

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]

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]

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]

(for clarity, foo is required downstream in a separate proof when I use add_pow₂ or add_pow₃)

[Kevin Buzzard]

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]

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]

Basically the same

[Oliver Nash]

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

[Scott Morrison]

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]

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

[Oliver Nash]

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]

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]

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.