|
%------------------------------------------------------------------------------
% Completing a measure
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Note: not described in Berberian
%
% Any measure can be "completed", by adding the negligible sets to the
% sigma_algebra and then extending the measure for these extra sets.
%
% Details of the actual extension mechanisms are in measure_completion_aux.
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
measure_completion[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra, (IMPORTING measure_def[T,S])
m:measure_type]: THEORY
BEGIN
IMPORTING measure_completion_aux[T],
measure_theory[T,S,m]
X: VAR (S)
N: VAR negligible[T,S,m]
sigma_algebra_completion: sigma_algebra[T] = completion(S,m)
generated_completion: LEMMA
generated_sigma_algebra(union(S,fullset[negligible[T,S,m]]))
= sigma_algebra_completion
completion: complete_measure[T,completion(S,m)] = completion(S,m)
completion_measurable: LEMMA x_eq(completion(X),m(X))
completion_negligible: LEMMA completion(N) = (TRUE,0)
END measure_completion
¤ Dauer der Verarbeitung: 0.15 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.
|
