|
%------------------------------------------------------------------------------
% L^\infty
%
% 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
%------------------------------------------------------------------------------
cal_L_inf[(IMPORTING measure_integration@subset_algebra_def,
measure_integration@measure_def)
T:TYPE, S:sigma_algebra[T], mu:measure_type[T,S]]: THEORY
BEGIN
IMPORTING essentially_bounded[T,S,mu],
complex_alt@complex_fun_ops[T]
h: VAR [T->complex]
x: VAR T
cal_L_infty?(h):bool = essentially_bounded?(h)
cal_L_infty: TYPE+ = (cal_L_infty?) CONTAINING (lambda x: complex_(0,0))
cal_L_infty_is_essentially_bounded:
JUDGEMENT cal_L_infty SUBTYPE_OF essentially_bounded
f,f0,f1: VAR cal_L_infty
c: VAR complex
scal_cal_L_infty: JUDGEMENT *(c,f) HAS_TYPE cal_L_infty
add_cal_L_infty: JUDGEMENT +(f0,f1) HAS_TYPE cal_L_infty
opp_cal_L_infty: JUDGEMENT -(f) HAS_TYPE cal_L_infty
diff_cal_L_infty: JUDGEMENT -(f0,f1) HAS_TYPE cal_L_infty
prod_cal_L_infty: JUDGEMENT *(f0,f1) HAS_TYPE cal_L_infty
inf_norm(f):nnreal = essential_bound(f) % 6.6.5(1)
inf_norm_scal: LEMMA inf_norm(c*f) = abs(c)*inf_norm(f) % 6.6.5(2)
inf_norm_add: LEMMA inf_norm(f0+f1) <= inf_norm(f0)+inf_norm(f1) % 6.6.5(3)
inf_norm_opp: LEMMA inf_norm(-f) = inf_norm(f)
inf_norm_diff: LEMMA inf_norm(f0-f1) <= inf_norm(f0)+inf_norm(f1)
inf_norm_eq_0: LEMMA inf_norm(f) = 0 <=> cal_N?(f) % 6.6.5(4)
inf_norm_prod: LEMMA inf_norm(f0*f1) <= inf_norm(f0)*inf_norm(f1) % 6.6.5(5)
IMPORTING p_integrable_def[T,S,mu,1]
g: VAR p_integrable
holder_judge_inf_1: JUDGEMENT *(f,g) HAS_TYPE p_integrable
holder_judge_inf_2: JUDGEMENT *(g,f) HAS_TYPE p_integrable
holder_infty_1: LEMMA norm(f*g) <= inf_norm(f) * norm(g)
END cal_L_inf
¤ Dauer der Verarbeitung: 0.32 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
