|
indefinite_integral[T: TYPE+ FROM real]: THEORY
%------------------------------------------------------------------------------
%
% Author: Rick Butler NASA Langley
%
% convention:
% Definite integral : Integral(a,b,f)
% Indefinite integral: integral(f)
%
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
deriv_domain: LEMMA deriv_domain?[T]
IMPORTING integral[T], derivative_props[T]
a,b,c,x: VAR T
f,g,F,G,H: VAR [T -> real]
antiderivative?(F,f): bool = derivable?(F) AND deriv(F) = f
antiderivative_lem: LEMMA antiderivative?(F,f) AND derivable?(G) AND
deriv(G) = f
IMPLIES (EXISTS (c: real): F = G + const_fun(c))
derivs_eq: THEOREM derivable?(F) AND derivable?(G) AND deriv(F) = deriv(G)
IMPLIES (EXISTS (c: real): F = G + const_fun(c))
% ------ indefinite integral defined over continuous functions ------
integrable?(f): bool = (EXISTS F: antiderivative?(F,f))
integrable_fun: TYPE = { f | integrable?(f)}
IMPORTING fundamental_theorem[T]
cont_fun_integrable?: LEMMA continuous?(f) IMPLIES integrable?(f)
integral(f: integrable_fun): { F: [T -> real] |
derivable?(F) AND deriv(F) = f }
integral_lem: LEMMA integrable?(f) AND integral(f) = F AND
derivable?(G) AND deriv(G) = f
IMPLIES (EXISTS (c: real): F = G + const_fun(c))
deriv_integ: LEMMA derivable?(F) IMPLIES integrable?[T](deriv(F))
indef_integral_thm : THEOREM derivable?(F) IMPLIES
(EXISTS (c: real):
integral(deriv(F)) = F + const_fun(c))
fundamental_indef : THEOREM continuous?(f) IMPLIES
Integrable?(a,b,f) AND
Integral(a,b,f) = integral(f)(b) - integral(f)(a)
END indefinite_integral
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
