SSL riemann_link.pvs

%------------------------------------------------------------------------------
% The Lebesgue criterion for Riemann Integrability
%
%     Author: David Lester, Manchester University
%
% References: AJ Weir, "Lebesgue Integration and Measure" CUP, 1973.
%
%     Version 1.0            26/2/10   Initial Version
%------------------------------------------------------------------------------

riemann_link: THEORY

BEGIN

  IMPORTING
    riemann_scaf,
    analysis@integral_def[real],
    analysis@integral_bounded[real],
    analysis@integral_cont[real],
    metric_space@continuity_link[real]


  a,b,x: VAR real
  f:     VAR [real->real]

  continuous_at?(f,x): MACRO bool = continuity_def.continuous_at?(f,x)
  continuous?(f):      MACRO bool = continuity_def.continuous?(f)

  bounded_on_def: LEMMA FORALL (a:real,b:{x | a < x},f):
    bounded_on?(a,b,f) <=> zeroed_bounded?[a,b](phi(closed(a,b))*f)

  riemann_integrable_def: LEMMA a <= b =>
    (Integrable?(a,b,f) <=> bounded_on?(a,b,f) AND ae_continuous?(a,b,f))

  riemann_lebesgue_integrable: LEMMA
    a <= b AND Integrable?(a,b,f) => integrable?(closed(a,b))(f)

  riemann_lebesgue_integral: LEMMA
    a <= b AND Integrable?(a,b,f) => Integral(a,b,f) = integral(closed(a,b),f)

  bounded_ae_continuous_integrable: LEMMA
    a <= b AND bounded_on?(a,b,f) AND ae_continuous?(a,b,f) =>
    integrable?(closed(a,b))(f)

  continuous_is_Integrable: LEMMA
    a <= b AND continuous?(f) => Integrable?(a,b,f)

  continuous_is_integrable: LEMMA
    a <= b AND continuous?(f) => integrable?(closed(a,b))(f)

  continuous_at_is_bounded: LEMMA
    a <= b AND (FORALL x: a <= x AND x <= b => continuous_at?(f,x)) =>
    bounded_on?(a,b,f)

END riemann_link