|
nth_derivatives[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
% The nth_derivatives theory defines the nth derivative of a function
%
% Developed by Ricky W. Butler NASA Langley Research Center
% David Lester Manchester University
%
% Version 1.0 last modified 10/30/00
% Version 1.1 Generalised for an arbitrary interval: T DRL 27/10/03
%
%------------------------------------------------------------------------------
BEGIN
ASSUMING
% connected_domain : ASSUMPTION
% FORALL (x, y : T), (z : real) :
% x <= z AND z <= y IMPLIES T_pred(z)
IMPORTING deriv_domain_def
deriv_domain : ASSUMPTION deriv_domain?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING derivatives
f: VAR [T -> real]
m, n: VAR nat
derivable_n_times?(f,n): RECURSIVE bool =
IF n = 0 THEN TRUE
ELSE
derivable?(f) AND
derivable_n_times?(deriv(f),n-1)
ENDIF MEASURE n
derivable_n_times_lem: LEMMA derivable_n_times?(f,n) AND m <= n IMPLIES
derivable_n_times?(f,m)
derivable_n_times_def: LEMMA derivable_n_times?(f, n+1) IMPLIES
derivable_n_times?(deriv(f), n)
nderiv_fun(n: nat): TYPE = {g: [T -> real] | derivable_n_times?(g,n)}
nderiv(n: nat,f:nderiv_fun(n)):RECURSIVE [T -> real] =
IF n = 0 THEN f
ELSE
nderiv(n-1,deriv(f))
ENDIF MEASURE n
nderiv_derivable: LEMMA m <= n AND derivable_n_times?(f, 1 + n)
IMPLIES derivable?(nderiv(m, f))
nderiv_derivable_aux: LEMMA derivable_n_times?(f, n+1) IMPLIES
nderiv(n+1,f) = deriv(nderiv(n,f))
nderiv_derivable_eqv: LEMMA derivable_n_times?(f, 1 + n) IFF
derivable_n_times?(f,n) AND derivable?(nderiv(n, f))
END nth_derivatives
¤ Dauer der Verarbeitung: 0.20 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.
|
