(Joint Center)Library MathComp.binomial

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path div.
Require Import fintype tuple finfun bigop prime finset.

This files contains the definition of: n ^_ m == the falling (or lower) factorial of n with m terms, i.e., the product n * (n - 1) * ... * (n - m + 1) Note that n ^_ m = 0 if m > n. 'C(n, m) == the binomial coeficient n choose m := n ^_ m %/ fact m
In additions to the properties of these functions, triangular_sum, Wilson and Pascal are examples of how to manipulate expressions with bigops.

Set Implicit Arguments.

More properties of the factorial *

Lemma fact_smonotone m n : 0 < mm < nm`! < n`!.

Lemma fact_prod n : n`! = \prod_(1 i < n.+1) i.

Lemma logn_fact p n : prime plogn p n`! = \sum_(1 k < n.+1) n %/ p ^ k.

Theorem Wilson p : p > 1 → prime p = (p %| ((p.-1)`!).+1).

The falling factorial

Fixpoint ffact_rec n m := if m is m'.+1 then n × ffact_rec n.-1 m' else 1.

Definition falling_factorial := nosimpl ffact_rec.

Notation "n ^_ m" := (falling_factorial n m)
  (at level 30, right associativity) : nat_scope.

Lemma ffactE : falling_factorial = ffact_rec.

Lemma ffactn0 n : n ^_ 0 = 1.

Lemma ffact0n m : 0 ^_ m = (m == 0).

Lemma ffactnS n m : n ^_ m.+1 = n × n.-1 ^_ m.

Lemma ffactSS n m : n.+1 ^_ m.+1 = n.+1 × n ^_ m.

Lemma ffactn1 n : n ^_ 1 = n.

Lemma ffactnSr n m : n ^_ m.+1 = n ^_ m × (n - m).

Lemma ffact_gt0 n m : (0 < n ^_ m) = (m n).

Lemma ffact_small n m : n < mn ^_ m = 0.

Lemma ffactnn n : n ^_ n = n`!.

Lemma ffact_fact n m : m nn ^_ m × (n - m)`! = n`!.

Lemma ffact_factd n m : m nn ^_ m = n`! %/ (n - m)`!.

Binomial coefficients

Fixpoint binomial_rec n m :=
  match n, m with
  | n'.+1, m'.+1binomial_rec n' m + binomial_rec n' m'
  | _, 0 ⇒ 1
  | 0, _.+1 ⇒ 0
  end.

Definition binomial := nosimpl binomial_rec.

Notation "''C' ( n , m )" := (binomial n m)
  (at level 8, format "''C' ( n , m )") : nat_scope.

Lemma binE : binomial = binomial_rec.

Lemma bin0 n : 'C(n, 0) = 1.

Lemma bin0n m : 'C(0, m) = (m == 0).

Lemma binS n m : 'C(n.+1, m.+1) = 'C(n, m.+1) + 'C(n, m).

Lemma bin1 n : 'C(n, 1) = n.

Lemma bin_gt0 m n : (0 < 'C(m, n)) = (n m).

Lemma leq_bin2l m1 m2 n : m1 m2'C(m1, n) 'C(m2, n).

Lemma bin_small n m : n < m'C(n, m) = 0.

Lemma binn n : 'C(n, n) = 1.

Lemma mul_Sm_binm m n : m.+1 × 'C(m, n) = n.+1 × 'C(m.+1, n.+1).

Lemma bin_fact m n : n m'C(m, n) × (n`! × (m - n)`!) = m`!.

In fact the only exception is n = 0 and m = 1
Lemma bin_factd n m : 0 < n'C(n, m) = n`! %/ (m`! × (n - m)`!).

Lemma bin_ffact n m : 'C(n, m) × m`! = n ^_ m.

Lemma bin_ffactd n m : 'C(n, m) = n ^_ m %/ m`!.

Lemma bin_sub n m : m n'C(n, n - m) = 'C(n, m).

Lemma binSn n : 'C(n.+1, n) = n.+1.

Lemma bin2 n : 'C(n, 2) = (n × n.-1)./2.

Lemma bin2odd n : odd n'C(n, 2) = n × n.-1./2.

Lemma prime_dvd_bin k p : prime p → 0 < k < pp %| 'C(p, k).

Lemma triangular_sum n : \sum_(0 i < n) i = 'C(n, 2).

Lemma textbook_triangular_sum n : \sum_(0 i < n) i = 'C(n, 2).

Theorem Pascal a b n :
  (a + b) ^ n = \sum_(i < n.+1) 'C(n, i) × (a ^ (n - i) × b ^ i).
Definition expnDn := Pascal.

Lemma Vandermonde k l i :
  \sum_(j < i.+1) 'C(k, j) × 'C(l, i - j) = 'C(k + l , i).

Lemma subn_exp m n k :
  m ^ k - n ^ k = (m - n) × (\sum_(i < k) m ^ (k.-1 -i) × n ^ i).

Lemma predn_exp m k : (m ^ k).-1 = m.-1 × (\sum_(i < k) m ^ i).

Lemma dvdn_pred_predX n e : (n.-1 %| (n ^ e).-1)%N.

Lemma modn_summ I r (P : pred I) F d :
  \sum_(i <- r | P i) F i %% d = \sum_(i <- r | P i) F i %[mod d].

Combinatorial characterizations.