| 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 complex_finite_measures.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Complex Integration with Finite Measures % % Author: David Lester, Manchester University % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 %% % Version 1.0 20/3/11 Initial Version %------------------------------------------------------------------------------ complex_finite_measures[(IMPORTING measure_integration@subset_algebra_def, measure_integration@measure_def) T:TYPE, S:sigma_algebra[T], mu:finite_measure[T,S]]: THEORY BEGIN IMPORTING p_integrable, measure_integration@integral[T,S,to_measure(mu)], essentially_bounded[T,S,to_measure(mu)] p,q: VAR {a:real | a >= 1} f: VAR [T -> complex] q_integrable_is_p_integrable: LEMMA p <= q AND p_integrable?[T,S,to_measure(mu),q](f) => p_integrable?[T,S,to_measure(mu),p](f) essentially_bounded_is_p_integrable: LEMMA essentially_bounded?(f) => p_integrable?[T,S,to_measure(mu),p](f) END complex_finite_measures ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28