Quelle  binomial_identities.pvs

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