|
binomial: THEORY
%------------------------------------------------------------------------------
%
% Binomial coefficient
%
% Author: David Lester Manchester University
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING factorial, sigma_upto, product[posnat]
n: VAR nat
pn: VAR posnat
nge2: VAR {k:posnat| k>=2}
C(n:nat,k:{i:nat| i<=n}):posnat = factorial(n)/(factorial(k)*factorial(n-k))
C_0: LEMMA C(n,0) = 1
C_n: LEMMA C(n,n) = 1
C_1: LEMMA C(pn,1) = pn
C_n_1: LEMMA C(pn,pn-1) = pn
C_symmetry: LEMMA FORALL (k:{i:nat| i<=n}): C(n,k) = C(n,n-k)
C_n_plus_1: LEMMA FORALL (k:{i:posnat| i<=n}): C(n+1,k) = C(n,k)+C(n,k-1)
C_k_plus_1: LEMMA FORALL (k:{i:nat| i<n}): C(n,k)*(n-k) = C(n,k+1)*(k+1)
C_k_minus_1: LEMMA FORALL (k:{i:nat| i<n}): C(n,k+1) = C(n,k)*((n-k)/(k+1))
C_2: LEMMA C(nge2,2) = (nge2*(nge2-1))/2
C_n_2: LEMMA C(nge2,nge2-2) = (nge2*(nge2-1))/2
sigma_C: LEMMA sigma(0,n,LAMBDA (i:{i:nat| i<=n}): C(n,i)) = 2^n
% An iterative version of C(n,k) = product(1,k,(n-(k-i))/i)
C_it(n:nat,k:{i:nat| i<=n}):rat =
product_it(1,k,LAMBDA(i:posnat):(n-(k-i))/i)
C_it_C : LEMMA
C_it = C
C_it_posnat : JUDGEMENT
C_it(n:nat,k:{i:nat| i<=n}) HAS_TYPE posnat
END binomial
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
