Quelle essentially_bounded.pvs Sprache: PVS

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

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

BEGIN

  IMPORTING complex_measure_theory[T,S,mu]

  h: VAR [T->complex]
  x: VAR T
  K: VAR nnreal
  c: VAR complex

  essentially_bounded?(h):bool = complex_measurable?(h) AND ae_bounded?(h)

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

  f,f0,f1: VAR essentially_bounded

  essential_bound(f): nnreal = inf({K | ae_le?(abs(f),lambda x: K)})

  essential_bound_def1: LEMMA ae_le?(abs(f),lambda x: K) =>
                              essential_bound(f) <= K
  essential_bound_def2: LEMMA ae_le?(abs(f),lambda x: essential_bound(f))

  scal_essentially_bounded: JUDGEMENT *(c,f)   HAS_TYPE essentially_bounded
  add_essentially_bounded:  JUDGEMENT +(f0,f1) HAS_TYPE essentially_bounded
  opp_essentially_bounded:  JUDGEMENT -(f)     HAS_TYPE essentially_bounded
  diff_essentially_bounded: JUDGEMENT -(f0,f1) HAS_TYPE essentially_bounded
  prod_essentially_bounded: JUDGEMENT *(f0,f1) HAS_TYPE essentially_bounded

  essential_bound_scal: LEMMA                                        % 6.6.5(2)
    essential_bound(c*f)    = abs(c)*essential_bound(f)
  essential_bound_add:  LEMMA                                        % 6.6.5(3)
     essential_bound(f0+f1) <= essential_bound(f0)+essential_bound(f1)
  essential_bound_opp:  LEMMA essential_bound(-f) = essential_bound(f)
  essential_bound_diff: LEMMA
    essential_bound(f0-f1) <= essential_bound(f0)+essential_bound(f1)
  essential_bound_eq_0: LEMMA essential_bound(f) = 0 <=> cal_N?(f)   % 6.6.5(4)
  essential_bound_prod: LEMMA                                        % 6.6.5(5)
    essential_bound(f0*f1) <= essential_bound(f0)*essential_bound(f1)

  IMPORTING p_integrable_def[T,S,mu,1]

  g: VAR p_integrable

  holder_judge_infty_1: JUDGEMENT *(f,g) HAS_TYPE p_integrable
  holder_judge_infty_2: JUDGEMENT *(g,f) HAS_TYPE p_integrable

  holder_infty_1: LEMMA norm(f*g) <= essential_bound(f) * norm(g)
  holder_infty_2: LEMMA norm(g*f) <= norm(g) * essential_bound(f)

END essentially_bounded

quality91%