Quelle  lebesgue_fundamental.pvs

%------------------------------------------------------------------------------
% The Fundamental Theorem of Calculus for Lebesgue Integrals
%
%     Author: David Lester, Manchester University
%
% References: AJ Weir, "Lebesgue Integration and Measure" CUP, 1973.
%
%     Version 1.0            26/2/10   Initial Version
%------------------------------------------------------------------------------

lebesgue_fundamental[a:real,b:{x:real | a<x}]: THEORY

BEGIN

  IMPORTING
    riemann_link,
    analysis@fundamental_theorem[(closed(a,b))],
    analysis@derivative_props[(closed(a,b))],
    continuous_on[(closed(a,b))],
    restriction_integral[(closed(a,b)),real]

  F,G: VAR deriv_fun[(closed(a,b))]
  f,g: VAR continuous_on
  x:   VAR real

;
  *(f:[(closed(a,b))->real],g:[real->real]): MACRO [real->real]
      = lambda x: extend[real,(closed(a,b)),real,0](f)(x) * g(x);

  fundamental_lebesgue: THEOREM                        % AJW 3.4 Theorem 2, p57
    deriv(F) = f => integrable?(closed(a,b))(f) AND
                    integral(closed(a,b),f) = F(b) - F(a)

  integration_by_parts: THEOREM                     % AJW 3.4 Proposition 1 p58
    (deriv(F) = f AND deriv(G) = g) =>
    (integrable?(closed(a,b))(F*g) AND
     integrable?(closed(a,b))(G*f) AND
     integral(closed(a,b),F*g) = F(b)*G(b)-F(a)*G(a)-integral(closed(a,b),G*f))

END lebesgue_fundamental