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