|
cal_L_real[(IMPORTING measure_integration@subset_algebra_def)
T:TYPE, S:sigma_algebra[T]]: THEORY
BEGIN
IMPORTING cal_L_complex[T,S]
mu: VAR measure_type[T,S]
nu: VAR finite_measure[T,S]
h,h1,h2: VAR [T->real]
x: VAR T
c: VAR real
p,q: VAR {a:real | a >= 1}
cal_L_real_infty?(mu,h):bool
= cal_L_complex_infty?(mu,lambda x: complex_(h(x),0))
cal_L_real_infty(mu): TYPE+ = (lambda h: cal_L_real_infty?(mu,h))
CONTAINING (lambda x: 0)
cal_L_real_infty?(nu,h): bool = cal_L_real_infty?(to_measure(nu),h)
cal_L_real_infty(nu): TYPE+ = cal_L_real_infty(to_measure(nu))
CONTAINING (lambda x: 0)
cal_L_real?(mu,p,h):bool
= cal_L_complex?(mu,p,lambda x: complex_(h(x),0))
cal_L_real(mu,p): TYPE+ = (lambda h: cal_L_real?(mu,p,h))
CONTAINING (lambda x: 0)
cal_L_real?(nu,p,h):bool = cal_L_real?(to_measure(nu),p,h)
cal_L_real(nu,p): TYPE+ = cal_L_real(to_measure(nu),p)
CONTAINING (lambda x: 0)
cal_L_real_1_def: LEMMA cal_L_real?(mu,1,h) <=> integrable?[T,S,mu](h)
scal_cal_LR: LEMMA cal_L_real?(mu,p,h) => cal_L_real?(mu,p,c*h)
sum_cal_LR: LEMMA cal_L_real?(mu,p,h1) AND cal_L_real?(mu,p,h2) =>
cal_L_real?(mu,p,h1+h2)
opp_cal_LR: LEMMA cal_L_real?(mu,p,h) => cal_L_real?(mu,p,-h)
diff_cal_LR: LEMMA cal_L_real?(mu,p,h1) AND cal_L_real?(mu,p,h2) =>
cal_L_real?(mu,p,h1-h2)
prod_cal_LR: LEMMA p > 1 AND 1/p + 1/q = 1 AND
cal_L_real?(mu,p,h1) AND
cal_L_real?(mu,q,h2) =>
cal_L_real?(mu,1,h1*h2)
scal_cal_L_inftyR: LEMMA cal_L_real_infty?(mu,h) =>
cal_L_real_infty?(mu,c*h)
sum_cal_L_inftyR: LEMMA cal_L_real_infty?(mu,h1) AND
cal_L_real_infty?(mu,h2) =>
cal_L_real_infty?(mu,h1+h2)
opp_cal_L_inftyR: LEMMA cal_L_real_infty?(mu,h) =>
cal_L_real_infty?(mu,-h)
diff_cal_L_inftyR: LEMMA cal_L_real_infty?(mu,h1) AND
cal_L_real_infty?(mu,h2) =>
cal_L_real_infty?(mu,h1-h2)
prod_cal_L_inftyR: LEMMA cal_L_real_infty?(mu,h1) AND
cal_L_real_infty?(mu,h2) =>
cal_L_real_infty?(mu,h1*h2)
prod_cal_L_1_inftyR: LEMMA cal_L_real?(mu,1,h1) AND
cal_L_real_infty?(mu,h2) =>
cal_L_real?(mu,1,h1*h2)
prod_cal_L_infty_1R: LEMMA cal_L_real_infty?(mu,h1) AND
cal_L_real?(mu,1,h2) =>
cal_L_real?(mu,1,h1*h2)
scal_cal_L_fmR: LEMMA cal_L_real?(nu,p,h) => cal_L_real?(nu,p,c*h)
sum_cal_L_fmR: LEMMA cal_L_real?(nu,p,h1) AND cal_L_real?(nu,p,h2) =>
cal_L_real?(nu,p,h1+h2)
opp_cal_L_fmR: LEMMA cal_L_real?(nu,p,h) => cal_L_real?(nu,p,-h)
diff_cal_L_fmR: LEMMA cal_L_real?(nu,p,h1) AND cal_L_real?(nu,p,h2) =>
cal_L_real?(nu,p,h1-h2)
prod_cal_L_fmR: LEMMA p > 1 AND 1/p + 1/q = 1 AND
cal_L_real?(nu,p,h1) AND
cal_L_real?(nu,q,h2) =>
cal_L_real?(nu,1,h1*h2)
scal_cal_L_infty_fmR: LEMMA cal_L_real_infty?(nu,h) =>
cal_L_real_infty?(nu,c*h)
sum_cal_L_infty_fmR: LEMMA cal_L_real_infty?(nu,h1) AND
cal_L_real_infty?(nu,h2) =>
cal_L_real_infty?(nu,h1+h2)
opp_cal_L_infty_fmR: LEMMA cal_L_real_infty?(nu,h) =>
cal_L_real_infty?(nu,-h)
diff_cal_L_infty_fmR: LEMMA cal_L_real_infty?(nu,h1) AND
cal_L_real_infty?(nu,h2) =>
cal_L_real_infty?(nu,h1-h2)
prod_cal_L_infty_fmR: LEMMA cal_L_real_infty?(nu,h1) AND
cal_L_real_infty?(nu,h2) =>
cal_L_real_infty?(nu,h1*h2)
prod_cal_L_1_infty_fmR: LEMMA cal_L_real?(nu,1,h1) AND
cal_L_real_infty?(nu,h2) =>
cal_L_real?(nu,1,h1*h2)
prod_cal_L_infty_1_fmR: LEMMA cal_L_real_infty?(nu,h1) AND
cal_L_real?(nu,1,h2) =>
cal_L_real?(nu,1,h1*h2)
END cal_L_real
¤ Dauer der Verarbeitung: 0.22 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.
|
