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