| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/while/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle cal_L_real.pvs Sprache: PVS |
|||||||||
|
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.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
