%------------------------------------------------------------------------------
% Properties of integrals with complete measures
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Some consequences of complete_integral_ae_eq; compare with the general
% version of 4.4.16 (for non-complete measures) in integral library.
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

complete_integral[T:TYPE,           (IMPORTING subset_algebra_def[T])
                  S:sigma_algebra,  (IMPORTING measure_def[T,S])
                  mu:complete_measure]: THEORY

BEGIN

  IMPORTING complete_measure_theory[T,S,mu],
            integral[T,S,mu],
            integral_convergence[T,S,mu]

  f: VAR integrable
  h: VAR [T->real]
  F: VAR sequence[integrable]
  n: VAR nat
  x: VAR T

  complete_integral_ae_eq:  LEMMA ae_eq?(f,h) =>                       % 4.4.16
                                  (integrable?(h) AND
                                   integral(f) = integral(h))

  complete_measurable_ae_0: LEMMA ae_0?(h) =>
                                  (integrable?(h) AND integral(h) = 0)

  monotone_convergence_complete: THEOREM                               % 4.5.3
      ae_monotonic_converges?(F,h) AND bounded?(integral o F) =>
      (integrable?(h) AND monotonic_converges?((integral o F),integral(h)))

  dominated_convergence_complete: THEOREM                              % 4.5.4
    (FORALL n: ae_le?(abs(F(n)),f)) AND ae_convergence?(F,h) =>
    (integrable?(h) AND convergence?(integral o F, integral(h)))

END complete_integral