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