| 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 1 kB |
|
Quelle p_integrable_def.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% p-th power integrable definitions % % Author: David Lester, Manchester University % % Version 1.0 12/03/10 Initial version (DRL) %------------------------------------------------------------------------------ p_integrable_def[(IMPORTING measure_integration@subset_algebra_def, measure_integration@measure_def) T:TYPE, S:sigma_algebra[T], mu:measure_type[T,S], p:{a:real | a >= 1}]: THEORY BEGIN IMPORTING complex_integral, complex_measure_theory[T,S,mu], measure_integration@integral[T,S,mu] h: VAR [T->complex] x: VAR T p_integrable?(h):bool = complex_measurable?(h) AND integrable?(abs(h)^p) p_integrable: TYPE+ = (p_integrable?) CONTAINING (lambda x: complex_(0,0)) cal_N_is_p_integrable: JUDGEMENT cal_N SUBTYPE_OF p_integrable f: VAR p_integrable norm(f):nnreal = integral(abs(f)^p)^(1/p) norm_eq_0: LEMMA norm(f) = 0 <=> cal_N?(f) END p_integrable_def ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28