|
deriv_real_vect2 [ T : TYPE FROM real ] : THEORY
BEGIN
ASSUMING
IMPORTING analysis@deriv_domain_def
deriv_domain : ASSUMPTION deriv_domain?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING analysis@deriv_domain, analysis@derivatives[T],
vectors@det_2D
s,v : VAR Vect2
a,r : VAR T
derivable_rv?(V:[T->Vect2]): bool =
derivable?(LAMBDA(a):V(a)`x) AND
derivable?(LAMBDA(a):V(a)`y)
differentiable_rv?(V:[T->Vect2]): MACRO bool = derivable_rv?(V)
V : VAR (derivable_rv?)
deriv_rv(V)(r) : Vect2 =
(deriv(LAMBDA(a):V(a)`x,r),deriv(LAMBDA(a):V(a)`y,r))
% ------- Properties of deriv
deriv(V): [T -> Vect2] = (LAMBDA (r:T): deriv_rv(V)(r))
AUTO_REWRITE- deriv_rv
AUTO_REWRITE- deriv
AUTO_REWRITE- derivable_rv?
IMPORTING vect_fun_ops_rv
f, f1, f2 : VAR (derivable_rv?)
b,c : VAR real
h: VAR deriv_fun[T] % h:[T -> real] AND derivable?(h)
sum_derivable_rv : LEMMA derivable_rv?(LAMBDA (x: T): f1(x) + f2(x))
diff_derivable_rv : LEMMA derivable_rv?(LAMBDA (x: T): f1(x) - f2(x))
neg_derivable_rv : LEMMA derivable_rv?(LAMBDA (x: T): -f(x))
prod_derivable_rv : LEMMA derivable_rv?(LAMBDA (x: T): h(x)*f(x))
dot_derivable_rv : LEMMA derivable?(LAMBDA (x: T): f1(x)*f2(x))
sqv_derivable_rv : LEMMA derivable?(LAMBDA (x: T): sqv(f(x)))
const_derivable_rv : LEMMA derivable_rv?(LAMBDA (x: T): s)
scal_derivable_rv : LEMMA derivable_rv?(LAMBDA (x: T): c * f(x))
prod_id_derivable_rv: LEMMA derivable_rv?(LAMBDA (x: T): x * v)
deriv_sum_vfun : LEMMA deriv(LAMBDA (x: T): f1(x) + f2(x)) = deriv(f1) + deriv(f2)
deriv_diff_vfun : LEMMA deriv(LAMBDA (x: T): f1(x) - f2(x)) = deriv(f1) - deriv(f2)
deriv_neg_vfun : LEMMA deriv(LAMBDA (x:T): -f(x)) = -deriv(f)
deriv_prod_vfun : LEMMA deriv(LAMBDA (x: T): h(x) * f(x)) = deriv(h)*f + h*deriv(f)
deriv_dot_vfun : LEMMA deriv(LAMBDA (x: T): f1(x) * f2(x)) = deriv(f1)*f2 + f1*deriv(f2)
deriv_sqv_vfun : LEMMA
deriv(LAMBDA (x: T): sqv(f(x))) = (LAMBDA (x:T): 2*f(x)*deriv(f)(x))
deriv_const_vfun : LEMMA deriv(LAMBDA (x: T): s) = (LAMBDA (x:T): zero)
deriv_scal_vfun : LEMMA deriv(LAMBDA (x: T): c * f(x)) = c * deriv(f)
deriv_prod_id_vfun: LEMMA deriv(LAMBDA (x: T): x * v) = (LAMBDA (x: T): v)
d_sum_vfun : LEMMA derivable_rv?(LAMBDA (x: T): f1(x) + f2(x)) AND
deriv(LAMBDA (x: T): f1(x) + f2(x)) = deriv(f1) + deriv(f2)
d_diff_vfun : LEMMA derivable_rv?(LAMBDA (x: T): f1(x) - f2(x)) AND
deriv(LAMBDA (x: T): f1(x) - f2(x)) = deriv(f1) - deriv(f2)
d_neg_vfun : LEMMA derivable_rv?(LAMBDA (x: T): -f(x)) AND
deriv(LAMBDA (x:T): -f(x)) = -deriv(f)
d_prod_vfun : LEMMA derivable_rv?(LAMBDA (x: T): h(x)*f(x)) AND
deriv(LAMBDA (x: T): h(x) * f(x)) = deriv(h)*f + h*deriv(f)
d_dot_vfun : LEMMA derivable?(LAMBDA (x: T): f1(x)*f2(x)) AND
deriv(LAMBDA (x: T): f1(x) * f2(x)) = deriv(f1)*f2 + f1*deriv(f2)
d_const_vfun : LEMMA derivable_rv?(LAMBDA (x: T): s) AND
deriv(LAMBDA (x: T): s) = (LAMBDA (x:T): zero)
d_scal_vfun : LEMMA derivable_rv?(LAMBDA (x: T): c * f(x)) AND
deriv(LAMBDA (x: T): c * f(x)) = c * deriv(f)
END deriv_real_vect2
¤ 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.
|
