binomial_identities: THEORY %------------------------------------------------------------------------------ % % Author: Anthony Narkawicz NASA Langley % %------------------------------------------------------------------------------ BEGIN
IMPORTING polynomials,
binomial
x,y: VAR real
n,m,i,j,r,k,s,N,p: VAR nat
pn: VAR posnat
a,b: VAR sequence[real]
nge2: VAR {k:posnat| k>=2}
% Many of these identities are taken from Concrete Mathematics, by Graham, % Knuth, and Patashnik (Section 5.2) and from Combinatorial Identities by Riordan
binom_trinomial_revision: LEMMA r>=m AND m>=k IMPLIES
C(r,m)*C(m,k) = C(r,k)*C(r-k,m-k)
binom_absorption: LEMMA r>=k AND k>=1 IMPLIES
C(r,k) = (r/k)*C(r-1,k-1)
binom_upper_summation: LEMMA n>=m IMPLIES
sigma(m,n,LAMBDA (k:nat): IF k<m OR k>n THEN 0 ELSE C(k,m) ENDIF) = C(n+1,m+1)
binom_parallel_summation: LEMMA
sigma(0,n,LAMBDA (k:nat): IF k>n THEN 0 ELSE C(r+k,k) ENDIF) = C(r+n+1,n)
binom_vandermonde_convolution: LEMMA n>=m AND n>=p IMPLIES
sigma(0,m,LAMBDA (k:nat): IF k>p OR k>m or m+p-n> k THEN 0 ELSE C(n-p,m-k)*C(p,k) ENDIF) = C(n,m)
binom_vandermonde_convolution_2: LEMMA n+p>=m IMPLIES
sigma(0,m,LAMBDA (k:nat): IF k>p OR k>m OR m-n>k THEN 0 ELSE C(n,m-k)*C(p,k) ENDIF) = C(n+p,m)
binom_vandermonde_convolution_3: LEMMA n+p>=m IMPLIES
sigma(0,m,LAMBDA (k:nat): IF k>m OR m-k>p OR k>n THEN 0 ELSE C(n,k)*C(p,m-k) ENDIF) = C(n+p,m)
% The next lemmas are helpful in proving theorems about Bernstein polynomials.
binom_cross_sum: LEMMA k>=i IMPLIES
sigma(i,k,LAMBDA (j:nat):IF j<i OR j>k THEN 0 ELSE C(k,j)*C(j,i)*x^j*y^(k-j) ENDIF) = x^i*C(k,i)*(x+y)^(k-i)
binom_sum_cross_sum_half: LEMMA k>=i IMPLIES
sigma(i,k,LAMBDA (j:nat):IF j<i OR j>k THEN 0 ELSE C(k,j)*C(j,i)*(-1)^(k-j)*(1/2^j) ENDIF) =
(1/2^k)*C(k,i)*(-1)^(k-i)
binom_pr1: LEMMA m>=N AND m>=i AND m<=8 IMPLIES
sigma(max(N,i),m,LAMBDA (k:nat): IF k<max(N,i) OR k>m THEN 0 ELSE C(m-N,k-N)*C(k,i)*(-1)^(k-i)*1/2^k ENDIF) =
sigma(0,min(N,i),LAMBDA (j:nat): IF j > min(N,i) THEN 0 ELSE C(m-j,i-j)*C(N,j)*(-1)^(N-j)*1/2^(m-j) ENDIF)
binomial_triple_cancel: LEMMA m>=N AND m>=i AND m<=8 IMPLIES
sigma(max(N,i),m,LAMBDA (k:nat): IF k<max(N,i) OR k>m THEN 0 ELSE C(k,N)*C(m,k)*C(k,i)*(-1)^(k-i)*1/2^k ENDIF) =
sigma(0,min(N,i),LAMBDA (j:nat): IF j > min(N,i) THEN 0 ELSE C(m-j,i-j)*C(N,j)*C(m,N)*(-1)^(N-j)*1/2^(m-j) ENDIF)
END binomial_identities
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤
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.
