- -

Library mathcomp.ssreflect.binomial

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- This files contains the definition of: - 'C(n, m) == the binomial coeficient n choose m. - 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, and 'C(n, m) = n ^_ m %/ m/!. - -

- - In additions to the properties of these functions, we prove a few seminal - results such as triangular_sum, Wilson and Pascal; their proofs are good - examples of how to manipulate expressions with bigops. -

- -
-Set Implicit Arguments.
- -
-

- -

- More properties of the factorial * -

- -
-Lemma fact_smonotone m n : 0 < m → m < n → m `! < n `!.
- -
-Lemma fact_prod n : n `! = \prod_(1 ≤ i < n .+1 ) i.
- -
-Lemma logn_fact p n : prime p → logn 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 < m → n ^_ m = 0.
- -
-Lemma ffactnn n : n ^_ n = n `!.
- -
-Lemma ffact_fact n m : m ≤ n → n ^_ m × (n - m )`! = n `!.
- -
-Lemma ffact_factd n m : m ≤ n → n ^_ m = n `! %/ (n - m )`!.
- -
-

- -

- Binomial coefficients -

- -
-Fixpoint binomial_rec n m :=
-  match n, m with
-  | n'.+1, m'.+1 ⇒ binomial_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 n m : (0 < 'C (n , m )) = (m ≤ n ).
- -
-Lemma leq_bin2l n1 n2 m : n1 ≤ n2 → 'C (n1 , m ) ≤ 'C (n2 , m ).
- -
-Lemma bin_small n m : n < m → 'C (n , m ) = 0.
- -
-Lemma binn n : 'C (n , n ) = 1.
- -
-

- -

- Multiply to move diagonally down and right in the Pascal triangle. -

-Lemma mul_bin_diag n m : n × 'C (n .-1 , m ) = m .+1 × 'C (n , m .+1 ).
- -
-Lemma bin_fact n m : m ≤ n → 'C (n , m ) × (m `! × (n - m )`!) = n `!.
- -
-

- -

- In fact the only exception for bin_factd 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 ).
- -
-

- -

- Multiply to move down in the Pascal triangle. -

-Lemma mul_bin_down n m : n × 'C (n .-1 , m ) = (n - m ) × 'C (n , m ).
- -
-

- -

- Multiply to move left in the Pascal triangle. -

-Lemma mul_bin_left n m : m .+1 × 'C (n , m .+1 ) = (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 < p → p %| '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. -

- -
-Section Combinations.
- -
-Implicit Types T D : finType.
- -
-Lemma card_uniq_tuples T n (A : pred T) :
-  #|[set t : n .-tuple T | all A t & uniq t ]| = #|A | ^_ n.
- -
-Lemma card_inj_ffuns_on D T (R : pred T) :
-  #|[set f : {ffun D → T } in ffun_on R | injectiveb f ]| = #|R | ^_ #|D |.
- -
-Lemma card_inj_ffuns D T :
-  #|[set f : {ffun D → T } | injectiveb f ]| = #|T | ^_ #|D |.
- -
-Lemma cards_draws T (B : {set T }) k :
-  #|[set A : {set T } | A \subset B & #|A | == k ]| = 'C (#|B |, k ).
- -
-Lemma card_draws T k : #|[set A : {set T } | #|A | == k ]| = 'C (#|T |, k ).
- -
-Lemma card_ltn_sorted_tuples m n :
-  #|[set t : m .-tuple 'I_n | sorted ltn (map val t)]| = 'C (n , m ).
- -
-Lemma card_sorted_tuples m n :
-  #|[set t : m .-tuple 'I_n .+1 | sorted leq (map val t)]| = 'C (m + n , m ).
- -
-Lemma card_partial_ord_partitions m n :
-  #|[set t : m .-tuple 'I_n .+1 | \sum_(i <- t ) i ≤ n ]| = 'C (m + n , m ).
- -
-Lemma card_ord_partitions m n :
-  #|[set t : m .+1 .-tuple 'I_n .+1 | \sum_(i <- t ) i == n ]| = 'C (m + n , m ).
- -
-End Combinations.
-