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]ASSUMPTION connected?[T]ASSUMPTION not_one_element?[T]ENDASSUMING LEMMA deriv_domain?[T]IMPORTING integral[T], derivative_props[T]VAR TVAR [T -> real]AND deriv(F) = fLEMMA antiderivative?(F,f) AND derivable?(G) AND IMPLIES (EXISTS (c: real): F = G + const_fun(c))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 ------ EXISTS F: antiderivative?(F,f))TYPE = { f | integrable?(f)}IMPORTING fundamental_theorem[T]LEMMA continuous?(f) IMPLIES integrable?(f)AND deriv(F) = f }LEMMA integrable?(f) AND integral(f) = F AND AND deriv(G) = fIMPLIES (EXISTS (c: real): F = G + const_fun(c))LEMMA derivable?(F) IMPLIES integrable?[T](deriv(F))THEOREM derivable?(F) IMPLIES EXISTS (c: real): THEOREM continuous?(f) IMPLIES AND END indefinite_integralquality 93%
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
