|
%------------------------------------------------------------------------------
% A primitive version of the Monotone Convergence Theorem
%
% 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_scaf[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra,(IMPORTING measure_def[T,S])
m:measure_type]: THEORY
BEGIN
IMPORTING measure_space[T,S],
measure_theory[T,S,m],
integral[T,S,m]
f: VAR [T->real]
F: VAR sequence[integrable]
monotone_convergence_scaf: LEMMA % 4.5.1
pointwise_converges_upto?(F,f) AND bounded?(integral o F) =>
(integrable?(f) AND converges_upto?((integral o F), integral(f)))
END integral_convergence_scaf
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
