|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
