Quelle  integral_convergence.pvs

%------------------------------------------------------------------------------
% Monotone and Dominated Convergence Theorems
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

integral_convergence[T:TYPE,         (IMPORTING subset_algebra_def[T])
                     S:sigma_algebra,(IMPORTING measure_def[T,S])
                     m:measure_type]: THEORY

BEGIN

  IMPORTING integral_convergence_scaf[T,S,m]

  i,j,n: VAR nat
  f,g: VAR integrable
  F: VAR sequence[integrable]
  E: VAR negligible
  x: VAR T

  monotone_convergence: THEOREM                                         % 4.5.3
      ae_increasing?(F) =>
      (((EXISTS f: ae_convergence?(F,f)) <=> bounded?(integral o F)) AND
       FORALL f: ae_convergence?(F,f) =>
                 converges_upto?((integral o F), integral(f)))

  dominated_convergence: THEOREM                                        % 4.5.4
    (FORALL n: ae_le?(abs(F(n)),f)) AND ae_convergent?(F) =>
     EXISTS g: ae_convergence?(F,g) AND convergence?(integral o F, integral(g))

END integral_convergence