%------------------------------------------------------------------------------
% p-th power integrable definitions
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            12/03/10   Initial version (DRL)
%------------------------------------------------------------------------------

p_integrable_def[(IMPORTING measure_integration@subset_algebra_def,
                            measure_integration@measure_def)
                 T:TYPE, S:sigma_algebra[T], 
                 mu:measure_type[T,S], p:{a:real | a >= 1}]: THEORY

BEGIN

  IMPORTING complex_integral,
            complex_measure_theory[T,S,mu],
            measure_integration@integral[T,S,mu]

  h: VAR [T->complex]
  x: VAR T

  p_integrable?(h):bool = complex_measurable?(h) AND integrable?(abs(h)^p)

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

  cal_N_is_p_integrable: JUDGEMENT cal_N SUBTYPE_OF p_integrable

  f: VAR p_integrable

  norm(f):nnreal = integral(abs(f)^p)^(1/p)

  norm_eq_0: LEMMA norm(f) = 0 <=> cal_N?(f)

END p_integrable_def