Quelle  measure_equality.pvs

%------------------------------------------------------------------------------
% Measure Equality
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% If mu(E) = nu(E) for every measurable set E, then the integrals are the same.
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

measure_equality[T:TYPE,        (IMPORTING subset_algebra_def[T])
                 S:sigma_algebra]: THEORY

BEGIN

  IMPORTING measure_def[T,S]

  mu,nu: VAR measure_type
  x:     VAR T
  f:     VAR [T->real]
  g:     VAR [T->nnreal]
  E:     VAR (S)

  IMPORTING integral

  measure_eq_isf?: LEMMA (FORALL E: x_eq(mu(E),nu(E))) =>
                            (isf?[T,S,mu](f) <=> isf?[T,S,nu](f))

  measure_eq_isf:  LEMMA (FORALL E: x_eq(mu(E),nu(E))) AND
                            (isf?[T,S,mu](f) OR isf?[T,S,nu](f)) =>
                            (isf_integral[T,S,mu](f) = isf_integral[T,S,nu](f))

  measure_eq_nn_integrable?: LEMMA
    (FORALL E: x_eq(mu(E),nu(E))) =>
    (nn_integrable?[T,S,mu](g) <=> nn_integrable?[T,S,nu](g))

  measure_eq_nn_integral:  LEMMA
    (FORALL E: x_eq(mu(E),nu(E))) AND
    (nn_integrable?[T,S,mu](g) OR nn_integrable?[T,S,nu](g)) =>
    (nn_integral[T,S,mu](g) = nn_integral[T,S,nu](g))

  measure_eq_integrable?: LEMMA
    (FORALL E: x_eq(mu(E),nu(E))) =>
    (integrable?[T,S,mu](f) <=> integrable?[T,S,nu](f))

  measure_eq_integral:  LEMMA
    (FORALL E: x_eq(mu(E),nu(E))) AND
    (integrable?[T,S,mu](f) OR integrable?[T,S,nu](f)) =>
    (integral[T,S,mu](f) = integral[T,S,nu](f))

END measure_equality