integration_by_parts[T: TYPE+ FROM real]: THEORY %------------------------------------------------------------------------------ % % Author: Rick Butler NASA Langley % %------------------------------------------------------------------------------
BEGIN
ASSUMING IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
IMPORTING fundamental_theorem[T]
a,b: VAR T
u,v: VAR [T -> real]
integ_parts_prep: LEMMAFORALL (a, b: T, u, v: [T -> real]):
derivable?(u) AND derivable?(v) AND continuous?(deriv(u)) IMPLIES Integrable?[T](a, b, LAMBDA (x: T): v(x) * deriv[T](u)(x));
integ_parts: THEOREM derivable?(u) AND continuous?(deriv(u)) AND
derivable?(v) AND continuous?(deriv(v)) IMPLIES
Integral(a,b,(LAMBDA (x:T): u(x)*deriv(v)(x))) =
u(b)*v(b) - u(a)*v(a) - Integral(a,b,(LAMBDA (x:T): v(x)*deriv(u)(x)))
END integration_by_parts
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
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.
