Quelle  complex_finite_measures.pvs

%------------------------------------------------------------------------------
% Complex Integration with Finite Measures
%
%     Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%%
%     Version 1.0            20/3/11   Initial Version
%------------------------------------------------------------------------------

complex_finite_measures[(IMPORTING measure_integration@subset_algebra_def,
                                   measure_integration@measure_def)
                 T:TYPE, S:sigma_algebra[T], mu:finite_measure[T,S]]: THEORY

BEGIN

  IMPORTING p_integrable,
            measure_integration@integral[T,S,to_measure(mu)],
            essentially_bounded[T,S,to_measure(mu)]

  p,q: VAR {a:real | a >= 1}
  f:   VAR [T -> complex]

  q_integrable_is_p_integrable: LEMMA
     p <= q AND
     p_integrable?[T,S,to_measure(mu),q](f) =>
     p_integrable?[T,S,to_measure(mu),p](f)

  essentially_bounded_is_p_integrable: LEMMA
     essentially_bounded?(f) => p_integrable?[T,S,to_measure(mu),p](f)

END complex_finite_measures