|
deriv_real_vect[T: TYPE FROM real, n: posnat ] : THEORY
%------------------------------------------------------------------------------
% Derivatives of Vector-Valued Functions
%
% Author: Rick Butler NASA Langley Research Center
%
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING analysis@deriv_domain_def
deriv_domain : ASSUMPTION deriv_domain?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING deriv_real_vect_def[T,n], deriv_dot_prod[T,n]
f, f1, f2, fp : VAR [T -> Vector[n]]
g : VAR [T -> nzreal]
x : VAR T
u : VAR nzreal
b : VAR real
l, l1, l2 : VAR real
h:[T -> real]
derivable?(f) : bool = FORALL x : derivable?(f, x)
deriv_vfun : TYPE = { f:[T -> Vector[n]] | derivable?(f) }
nz_deriv_vfun : TYPE = { g:[T -> Nz_vector[n]] | derivable?(g) }
deriv(ff: deriv_vfun) : [T -> Vector[n]] = LAMBDA x : deriv(ff, x)
sum_derivable_vfun : LEMMA derivable?(f1) AND derivable?(f2)
IMPLIES derivable?(f1 + f2)
neg_derivable_vfun : LEMMA derivable?(f) IMPLIES derivable?(- f)
diff_derivable_vfun : LEMMA derivable?(f1) AND derivable?(f2)
IMPLIES derivable?(f1 - f2)
%% prod_derivable_rv : LEMMA derivable?(h) IMPLIES derivable?(LAMBDA (x: T): h(x)*f(x))
dot_derivable_vfun : LEMMA derivable?(f1) AND derivable?(f2)
IMPLIES derivable?(f1 * f2)
scal_derivable_vfun : LEMMA derivable?(f) IMPLIES derivable?(b * f)
const_derivable_vfun : LEMMA derivable?(const_vfun(b))
inv_derivable_vfun : LEMMA derivable?(g) IMPLIES derivable?(1/g)
ff, ff1, ff2 : VAR deriv_vfun
hh: VAR deriv_fun[T]
derivable_sum : JUDGEMENT +(ff1, ff2) HAS_TYPE deriv_vfun
derivable_diff : JUDGEMENT -(ff1, ff2) HAS_TYPE deriv_vfun
derivable_scal : JUDGEMENT *(b, ff) HAS_TYPE deriv_vfun
derivable_neg : JUDGEMENT -(ff) HAS_TYPE deriv_vfun
derivable_const : JUDGEMENT const_vfun(b) HAS_TYPE deriv_vfun
%-----------------------------------
% Derivative vector-valued function
%-----------------------------------
deriv_sum_vfun : LEMMA deriv(ff1 + ff2) = deriv(ff1) + deriv(ff2)
deriv_neg_vfun : LEMMA deriv(- ff) = - deriv(ff)
deriv_diff_vfun : LEMMA deriv(ff1 - ff2) = deriv(ff1) - deriv(ff2)
%% deriv_prod_vfun : LEMMA deriv(LAMBDA (x: T): hh(x) * ff1(x)) = deriv(hh)*ff1 + hh*deriv(ff1)
deriv_dot_vfun : LEMMA deriv(ff1 * ff2) = deriv(ff1) * ff2 + deriv(ff2) * ff1
deriv_scal_vfun : LEMMA deriv(b * ff) = b * deriv(ff)
deriv_const_vfun : LEMMA deriv(const_vfun(b)) = const_vfun(0)
END deriv_real_vect
¤ Dauer der Verarbeitung: 0.1 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.
|
