| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis_ax/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle chain_rule.pvs Sprache: PVS |
|||||||||
|
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.9 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28