Quelle  p_integrable.pvs

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

p_integrable[(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],
            minkowski_scaf[T,S,mu,p]

  x: VAR T

  f,f0,f1: VAR p_integrable
  c: VAR complex

  scal_p_integrable: JUDGEMENT *(c,f)   HAS_TYPE p_integrable
  sum_p_integrable:  JUDGEMENT +(f0,f1) HAS_TYPE p_integrable
  opp_p_integrable:  JUDGEMENT -(f)     HAS_TYPE p_integrable
  diff_p_integrable: JUDGEMENT -(f0,f1) HAS_TYPE p_integrable

  norm_scal: LEMMA norm(c*f)    = abs(c)*norm(f)
  norm_add:  LEMMA norm(f0+f1) <= norm(f0)+norm(f1)
  norm_opp:  LEMMA norm(-f)     = norm(f)
  norm_diff: LEMMA norm(f0-f1) <= norm(f0)+norm(f1)

END p_integrable