SSL binomial_identities.pvs Sprache: 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

quality79%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.