|
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 : LEMMA 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 : LEMMA 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.22Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
