Quelle  complex_measure_theory.pvs

%------------------------------------------------------------------------------
% Complex Measure Theory [T->complex]
%
%     Author: David Lester, Manchester University
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Definition and basic properties of measurable functions f: [T->complex]
%
%     Version 1.0            11/3/10   Initial Version
%------------------------------------------------------------------------------

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

BEGIN

  IMPORTING measure_integration@measure_theory[T,S,mu],
            complex_measurable[T,S]

  p:   VAR pred[[complex,complex]]
  f,g: VAR [T->complex]
  x:   VAR T
  n:   VAR nat
  K:   VAR nnreal

  pointwise_ae?(p)(f,g):bool = ae?(LAMBDA x: p(f(x),g(x)))

  ae?(p)(f,g):   bool = pointwise_ae?(p)(f,g)
  ae_eq?(f,g):   bool = pointwise_ae?(=)(f,g)
  ae_0?(f):      bool = pointwise_ae?(=)(f,lambda x: complex_(0,0))

  ae_bounded?(f):bool = EXISTS K: ae_le?(abs(f),lambda x: K)

  cal_N?(f):bool = ae_0?(f) AND complex_measurable?(f)

  cal_N: TYPE+ = (cal_N?) CONTAINING (lambda x: complex_(0,0))

  cal_N_is_measurable: JUDGEMENT cal_N SUBTYPE_OF complex_measurable

  cal_N_def: LEMMA cal_N?(f) <=>
                   ae_0?(Re(f)) AND measurable_function?(Re(f)) AND
                   ae_0?(Im(f)) AND measurable_function?(Im(f))

END complex_measure_theory