|
integral_chg_var[T: TYPE+ FROM real, U: TYPE+ FROM real]: THEORY
%----------------------------------------------------------------------------
%
% Integral change of variable theorem
%
% Rosenlicht page 128
%
% Author: Rick Butler NASA Langley
%----------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
con_dom_U : ASSUMPTION connected?[U]
not_one_U : ASSUMPTION not_one_element?[U]
ENDASSUMING
deriv_domain_T: LEMMA deriv_domain?[T]
deriv_domain_U: LEMMA deriv_domain?[U]
IMPORTING composition_continuous,
fundamental_theorem,
chain_rule
f: VAR [T -> real]
phi: VAR [U -> T]
a,b: VAR U
t: VAR T
int_chg_var_prep: LEMMA continuous?(f) AND derivable?(phi)
AND continuous?(deriv(phi)) IMPLIES
continuous?((f o phi) * deriv(phi)) AND
Integrable?[U](a, b, LAMBDA (u: U): f(phi(u)) * deriv[U](phi)(u));
Int_chg_var: THEOREM derivable?(phi) AND continuous?(deriv(phi)) AND
continuous?(f)
IMPLIES
Integral(phi(a),phi(b),f) =
Integral(a,b,(LAMBDA (u:U): f(phi(u))*deriv(phi)(u)))
int_chg_var: THEOREM derivable?(phi) AND continuous?(deriv(phi)) AND
continuous?(f) AND a < b AND phi(a) < phi(b)
IMPLIES
integral(phi(a),phi(b),f) =
integral(a,b,(LAMBDA (u:U): f(phi(u))*deriv(phi)(u)))
END integral_chg_var
¤ Dauer der Verarbeitung: 0.0 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.
|
