|
%------------------------------------------------------------------------------
% Basic properties of measures
%
% 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
%------------------------------------------------------------------------------
measure_props[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra, (IMPORTING measure_def[T,S])
m:measure_type]: THEORY
BEGIN
IMPORTING measure_space_def[T,S],
sigma_algebra[T,S],
structures@fun_preds_partial[nat,set[T],reals.<=,subset?[T]],
measure_def[T,S],
series@series_aux
n,i: VAR nat
a,b,M: VAR measurable_set
x,y: VAR extended_nnreal
X: VAR sequence[extended_nnreal]
DX: VAR disjoint_indexed_measurable
E: VAR sequence[measurable_set]
mu_fin?(M):bool = m(M)`1
mu(M:{m:(S) | mu_fin?(m)}):nnreal = m(M)`2
m_emptyset: LEMMA m(emptyset[T]) = (TRUE,0)
m_countably_additive: LEMMA x_eq(x_sum(m o DX), m(IUnion(DX)))
m_disjoint_union:LEMMA disjoint?(a,b) => x_eq(m(union(a,b)),x_add(m(a),m(b)))
m_monotone: LEMMA subset?(a,b) => x_le(m(a),m(b)) % 2.6.1
m_union: LEMMA x_le(m(union(a,b)),x_add(m(a),m(b)))
m_increasing_convergence: LEMMA increasing?(E) => % 2.6.2
x_converges?(m o E, m(IUnion(E)))
m_decreasing_convergence: LEMMA decreasing?(E) AND mu_fin?(E(0)) => % 2.6.3
x_converges?(m o E, m(IIntersection(E)))
END measure_props
¤ Dauer der Verarbeitung: 0.13 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.
|
