|
%------------------------------------------------------------------------------
% Auxilliary results to complete a measure
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Note: not described in Berberian
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
measure_completion_aux[T:TYPE]: THEORY
BEGIN
IMPORTING subset_algebra_def[T],
measure_def,
measure_theory,
measure_props
XS: VAR setofsets[T]
A,B,X: VAR set[T]
z: VAR extended_nnreal
almost_measurable?(S:sigma_algebra[T],m:measure_type[T,S])(X):bool
= EXISTS (Y:(S),N1,N2:negligible[T,S,m]): X = difference(union(Y,N1),N2)
empty_almost_measurable: LEMMA
FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
almost_measurable?(S,m)(emptyset[T])
complement_almost_measurable: LEMMA
FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
almost_measurable?(S,m)(X) <=> almost_measurable?(S,m)(complement(X))
Union_almost_measurable: LEMMA
FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
every(almost_measurable?(S,m),XS) AND is_countable(XS) =>
almost_measurable?(S,m)(Union(XS))
completion(S:sigma_algebra[T],m:measure_type[T,S]):sigma_algebra[T]
= {X | almost_measurable?(S,m)(X)}
generated_completion: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
generated_sigma_algebra(union(S,fullset[negligible[T,S,m]]))
= completion(S,m)
completion_extends: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
S(X) => completion(S,m)(X)
negligible_completion: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
negligible_set?[T,S,m](X) => completion(S,m)(X)
is_completion(S:sigma_algebra[T],m:measure_type[T,S])(A,B):bool
= completion(S,m)(A) AND S(B) =>
EXISTS (N1,N2:negligible[T,S,m]): A = difference(union(B,N1),N2)
m_completions: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S],X,A,B):
completion(S,m)(X) AND S(A) AND S(B) AND
is_completion(S,m)(X,A) AND is_completion(S,m)(X,B) =>
x_eq(m(A),m(B))
choose_completion: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S],X):
completion(S,m)(X) =>
is_completion(S,m)(X,choose({Y:(S) | EXISTS (N1,N2:negligible[T,S,m]):
X = difference(union(Y,N1),N2)}))
completion(S:sigma_algebra[T],m:measure_type[T,S]):
complete_measure[T,completion(S,m)]
= lambda (X:(completion(S,m))):
m(choose({Y:(S) | EXISTS (N1,N2:negligible[T,S,m]):
X = difference(union(Y,N1),N2)}))
completion_measurable: LEMMA
FORALL (S:sigma_algebra[T],m:measure_type[T,S],X:(S)):
x_eq(completion(S,m)(X),m(X))
completion_negligible: LEMMA
FORALL (S:sigma_algebra[T],m:measure_type[T,S],N:negligible[T,S,m]):
completion(S,m)(N) = (TRUE,0)
END measure_completion_aux
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
