%------------------------------------------------------------------------------
% Measure Contraction
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% If mu is a measure, so is the contraction lambda E: mu(intersection(A,E)).
%
% The integrals using the contracted measure are the same as the indefinite
% integral
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

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

BEGIN

  IMPORTING measure_def[T,S],
            measure_space[T,S]
;
  *(f,g:[T -> real]): MACRO [T -> real] = (reals@real_fun_ops[T].*)(f,g)

  mu:  VAR measure_type
  nu:  VAR sigma_finite_measure
  A,E: VAR measurable_set
  f:   VAR measurable_function
  i:   VAR nat

  contraction(mu,A):measure_type = lambda E: mu(intersection(A,E))  % SKB 7.4.2

  fm_contraction(mu:measure_type,A:{E | mu(E)`1}):finite_measure
    = lambda E: mu(intersection(A,E))`2

  sigma_finite_contraction_def: LEMMA
    x_eq(nu(E),x_sum(LAMBDA i: (TRUE,fm_contraction(nu,A_of(nu)(i))(E))))

  IMPORTING isf,
            nn_integral,
            integral,
            indefinite_integral, % Proof only
            integral_convergence % Proof only

  contraction_is_sigma_finite:
                      JUDGEMENT contraction(nu,A) HAS_TYPE sigma_finite_measure

  contraction_isf: LEMMA FORALL (f:simple):
    isf?[T,S,contraction(mu,A)](f) <=> isf?[T,S,mu](phi[T,S](A)*f)

  contraction_isf_integral: LEMMA
    FORALL (f:isf[T,S,contraction(mu,A)]):
      isf_integral[T,S,contraction(mu,A)](f)
        = isf_integral[T,S,mu](phi[T,S](A)*f)

  contraction_nn_integrable: LEMMA FORALL (f:nn_measurable):
    nn_integrable?[T,S,contraction(mu,A)](f) <=>
    nn_integrable?[T,S,mu](phi[T,S](A)*f)

  contraction_nn_integral: LEMMA
    FORALL (f:nn_integrable[T,S,contraction(mu,A)]):
    nn_integral[T,S,contraction(mu,A)](f) = nn_integral[T,S,mu](phi[T,S](A)*f)

  contraction_integrable: LEMMA                                     % SKB 7.4.4
    integrable?[T,S,contraction(mu,A)](f)
      <=> integrable?[T,S,mu](phi[T,S](A)*f)

  contraction_integral:   LEMMA                                     % SKB 7.4.4
    FORALL (f:integrable[T,S,contraction(mu,A)]):
    integral[T,S,contraction(mu,A)](f) = integral[T,S,mu](phi[T,S](A)*f)

END measure_contraction