|
polynomial_deriv: THEORY
%------------------------------------------------------------------------------
%
%
%
% David Lester Manchester University
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING reals@sigma
IMPORTING derivatives, chain_rule
IMPORTING derivative_props, convergence_ops
IMPORTING ints@factorial, nth_derivatives, reals@binomial
IMPORTING reals@polynomials
x,y: VAR real
n,m: VAR nat
pn: VAR posnat
a,b: VAR sequence[real]
derivable_polynomial: LEMMA derivable?(polynomial(a,n))
deriv_polynomial : LEMMA deriv(polynomial(a,n))
= IF n = 0 THEN (LAMBDA (x:real): 0)
ELSE polynomial((LAMBDA (i:nat): (i+1)*a(i+1)),n-1)
ENDIF
derivable_n_times_polynomial: LEMMA derivable_n_times?(polynomial(b,m),n)
nderiv_polynomial : LEMMA nderiv(n,polynomial(b,m))
= IF n > m THEN (LAMBDA (x:real): 0)
ELSE polynomial(LAMBDA (i:nat): C(i+n,n)*factorial(n)*b(i+n),m-n)
ENDIF
END polynomial_deriv
¤ Dauer der Verarbeitung: 0.0 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.
|
