|
chain_rule [ T1, T2 : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
% Author: Bruno Dutertre Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def
deriv_domain1 : ASSUMPTION deriv_domain?[T1]
not_one_element1 : ASSUMPTION not_one_element?[T1]
deriv_domain2 : ASSUMPTION deriv_domain?[T2]
not_one_element2 : ASSUMPTION not_one_element?[T2]
ENDASSUMING
IMPORTING derivative_props % , lim_of_composition
f : VAR [T1 -> T2]
g : VAR [T2 -> real]
x : VAR T1
DF, DG : VAR real
% chain_rule_cnvg : LEMMA convergence(NQ(f, x), 0, DF) AND
% convergence(NQ(g, f(x)), 0, DG)
% IMPLIES convergence(NQ(g o f, x), 0, DG * DF)
composition_derivable : AXIOM derivable?(f, x) AND derivable?(g, f(x))
IMPLIES derivable?(g o f, x)
composition_derivable_fun : LEMMA derivable?(f) AND derivable?(g)
IMPLIES derivable?(g o f)
deriv_composition : AXIOM derivable?(f, x) AND derivable?(g, f(x))
IMPLIES deriv(g o f, x) = deriv(g, f(x)) * deriv(f, x)
ff : VAR { f | derivable?(f) }
gg : VAR { g | derivable?(g) }
deriv_comp_fun : LEMMA deriv(gg o ff) = (deriv(gg) o ff) * deriv(ff)
comp_derivable_fun : LEMMA derivable?(f) AND derivable?(g)
IMPLIES derivable?(LAMBDA (x: T1): g(f(x)))
chain_rule : LEMMA deriv(LAMBDA (x: T1): gg(ff(x))) =
(LAMBDA (x: T1): deriv(gg)(ff(x))) * deriv(ff)
END chain_rule
¤ Dauer der Verarbeitung: 0.31 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.
|
