%------------------------------------------------------------------------------ % Properties of integrals with complete measures % % Author: David Lester, Manchester University, NIA, Université Perpignan % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % Some consequences of complete_integral_ae_eq; compare with the general % version of 4.4.16 (for non-complete measures) in integral library. % % Version 1.0 1/5/07 Initial Version %------------------------------------------------------------------------------
complete_integral[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra, (IMPORTING measure_def[T,S])
mu:complete_measure]: THEORY
complete_measurable_ae_0: LEMMA ae_0?(h) =>
(integrable?(h) AND integral(h) = 0)
monotone_convergence_complete: THEOREM% 4.5.3
ae_monotonic_converges?(F,h) AND bounded?(integral o F) =>
(integrable?(h) AND monotonic_converges?((integral o F),integral(h)))
dominated_convergence_complete: THEOREM% 4.5.4
(FORALL n: ae_le?(abs(F(n)),f)) AND ae_convergence?(F,h) =>
(integrable?(h) AND convergence?(integral o F, integral(h)))
END complete_integral
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
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.
