|
cal_L_complex[(IMPORTING measure_integration@subset_algebra_def)
T:TYPE, S:sigma_algebra[T]]: THEORY
BEGIN
IMPORTING essentially_bounded,
p_integrable
mu: VAR measure_type[T,S]
nu: VAR finite_measure[T,S]
h,h1,h2: VAR [T->complex]
x: VAR T
c: VAR complex
p,q: VAR {a:real | a >= 1}
cal_L_complex_infty?(mu,h):bool = essentially_bounded?[T,S,mu](h)
cal_L_complex_infty(mu): TYPE+ = (lambda h: cal_L_complex_infty?(mu,h))
CONTAINING (lambda x: complex_(0,0))
cal_L_complex_infty?(nu,h): bool = cal_L_complex_infty?(to_measure(nu),h)
cal_L_complex_infty(nu): TYPE+ = cal_L_complex_infty(to_measure(nu))
CONTAINING (lambda x: complex_(0,0))
cal_L_complex_infty_is_essentially_bounded: LEMMA
cal_L_complex_infty?(mu,h) <=> essentially_bounded?[T,S,mu](h)
cal_L_complex?(mu,p,h):bool = p_integrable?[T,S,mu,p](h)
cal_L_complex(mu,p): TYPE+ = (lambda h: cal_L_complex?(mu,p,h))
CONTAINING (lambda x: complex_(0,0))
cal_L_complex?(nu,p,h):bool = cal_L_complex?(to_measure(nu),p,h)
cal_L_complex(nu,p): TYPE+ = cal_L_complex(to_measure(nu),p)
CONTAINING (lambda x: complex_(0,0))
cal_L_complex_is_p_integrable: LEMMA
cal_L_complex?(mu,p,h) <=> p_integrable?[T,S,mu,p](h)
cal_L_complex_1_def: LEMMA cal_L_complex?(mu,1,h) <=> integrable?[T,S,mu](h)
scal_cal_L: LEMMA cal_L_complex?(mu,p,h) => cal_L_complex?(mu,p,c*h)
sum_cal_L: LEMMA cal_L_complex?(mu,p,h1) AND cal_L_complex?(mu,p,h2) =>
cal_L_complex?(mu,p,h1+h2)
opp_cal_L: LEMMA cal_L_complex?(mu,p,h) => cal_L_complex?(mu,p,-h)
diff_cal_L: LEMMA cal_L_complex?(mu,p,h1) AND cal_L_complex?(mu,p,h2) =>
cal_L_complex?(mu,p,h1-h2)
prod_cal_L: LEMMA p > 1 AND 1/p + 1/q = 1 AND
cal_L_complex?(mu,p,h1) AND
cal_L_complex?(mu,q,h2) =>
cal_L_complex?(mu,1,h1*h2)
scal_cal_L_infty: LEMMA cal_L_complex_infty?(mu,h) =>
cal_L_complex_infty?(mu,c*h)
sum_cal_L_infty: LEMMA cal_L_complex_infty?(mu,h1) AND
cal_L_complex_infty?(mu,h2) =>
cal_L_complex_infty?(mu,h1+h2)
opp_cal_L_infty: LEMMA cal_L_complex_infty?(mu,h) =>
cal_L_complex_infty?(mu,-h)
diff_cal_L_infty: LEMMA cal_L_complex_infty?(mu,h1) AND
cal_L_complex_infty?(mu,h2) =>
cal_L_complex_infty?(mu,h1-h2)
prod_cal_L_infty: LEMMA cal_L_complex_infty?(mu,h1) AND
cal_L_complex_infty?(mu,h2) =>
cal_L_complex_infty?(mu,h1*h2)
prod_cal_L_1_infty: LEMMA cal_L_complex?(mu,1,h1) AND
cal_L_complex_infty?(mu,h2) =>
cal_L_complex?(mu,1,h1*h2)
prod_cal_L_infty_1: LEMMA cal_L_complex_infty?(mu,h1) AND
cal_L_complex?(mu,1,h2) =>
cal_L_complex?(mu,1,h1*h2)
scal_cal_L_fm: LEMMA cal_L_complex?(nu,p,h) => cal_L_complex?(nu,p,c*h)
sum_cal_L_fm: LEMMA cal_L_complex?(nu,p,h1) AND cal_L_complex?(nu,p,h2) =>
cal_L_complex?(nu,p,h1+h2)
opp_cal_L_fm: LEMMA cal_L_complex?(nu,p,h) => cal_L_complex?(nu,p,-h)
diff_cal_L_fm: LEMMA cal_L_complex?(nu,p,h1) AND cal_L_complex?(nu,p,h2) =>
cal_L_complex?(nu,p,h1-h2)
prod_cal_L_fm: LEMMA p > 1 AND 1/p + 1/q = 1 AND
cal_L_complex?(nu,p,h1) AND
cal_L_complex?(nu,q,h2) =>
cal_L_complex?(nu,1,h1*h2)
scal_cal_L_infty_fm: LEMMA cal_L_complex_infty?(nu,h) =>
cal_L_complex_infty?(nu,c*h)
sum_cal_L_infty_fm: LEMMA cal_L_complex_infty?(nu,h1) AND
cal_L_complex_infty?(nu,h2) =>
cal_L_complex_infty?(nu,h1+h2)
opp_cal_L_infty_fm: LEMMA cal_L_complex_infty?(nu,h) =>
cal_L_complex_infty?(nu,-h)
diff_cal_L_infty_fm: LEMMA cal_L_complex_infty?(nu,h1) AND
cal_L_complex_infty?(nu,h2) =>
cal_L_complex_infty?(nu,h1-h2)
prod_cal_L_infty_fm: LEMMA cal_L_complex_infty?(nu,h1) AND
cal_L_complex_infty?(nu,h2) =>
cal_L_complex_infty?(nu,h1*h2)
prod_cal_L_1_infty_fm: LEMMA cal_L_complex?(nu,1,h1) AND
cal_L_complex_infty?(nu,h2) =>
cal_L_complex?(nu,1,h1*h2)
prod_cal_L_infty_1_fm: LEMMA cal_L_complex_infty?(nu,h1) AND
cal_L_complex?(nu,1,h2) =>
cal_L_complex?(nu,1,h1*h2)
END cal_L_complex
¤ Dauer der Verarbeitung: 0.3 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.
|
