Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: binomial_identities.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.5 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.