Quelle  integration_by_parts.pvs

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: LEMMA  FORALL (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