%------------------------------------------------------------------------------ % Monotone and Dominated Convergence Theorems % % Author: David Lester, Manchester University, NIA, Université Perpignan % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % Version 1.0 1/5/07 Initial Version %------------------------------------------------------------------------------
integral_convergence[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra,(IMPORTING measure_def[T,S])
m:measure_type]: THEORY
BEGIN
IMPORTING integral_convergence_scaf[T,S,m]
i,j,n: VAR nat
f,g: VAR integrable
F: VAR sequence[integrable]
E: VAR negligible
x: VAR T
monotone_convergence: THEOREM% 4.5.3
ae_increasing?(F) =>
(((EXISTS f: ae_convergence?(F,f)) <=> bounded?(integral o F)) AND FORALL f: ae_convergence?(F,f) =>
converges_upto?((integral o F), integral(f)))
dominated_convergence: THEOREM% 4.5.4
(FORALL n: ae_le?(abs(F(n)),f)) AND ae_convergent?(F) => EXISTS g: ae_convergence?(F,g) AND convergence?(integral o F, integral(g))
END integral_convergence
¤ Dauer der Verarbeitung: 0.11 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.
