|
%-------------------------------------------------------------------------
%
% Finite Measure Theory file.
%
% Author: David Lester, Manchester University
%
%
% Version 1.0 10/4/05
%-------------------------------------------------------------------------
finite_measure[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra, (IMPORTING measure_def[T,S])
mu:finite_measure]: THEORY
BEGIN
IMPORTING sets_lemmas_aux, % Proof only, RWB: was sets_aux@
sets_aux@indexed_sets_aux[nat,T],
sigma_algebra[T,S],
series@series_aux, % Proof only
structures@fun_preds_partial[nat,set[T],reals.<=,subset?[T]]
X: VAR [nat->(S)]
A,B: VAR (S)
fm_emptyset: LEMMA mu(emptyset) = 0
fm_convergence: LEMMA disjoint?(X)
=> convergence(series(mu o X), mu(IUnion(X)))
fm_disjointunion: LEMMA disjoint?(A,B) => mu(union(A,B)) = mu(A) + mu(B)
fm_complement: LEMMA mu(complement(A)) = mu(fullset) - mu(A)
fm_union: LEMMA mu(union(A,B))
= mu(A) + mu(B) - mu(intersection(A,B))
fm_intersection: LEMMA mu(intersection(A,B))
= mu(A) + mu(B) - mu(union(A,B))
fm_difference: LEMMA mu(difference(A,B))
= mu(A) - mu(B) + mu(difference(B,A))
fm_subset: LEMMA subset?(A,B) => mu(B) = mu(A) + mu(difference(B,A))
fm_subset_le: LEMMA subset?(A,B) => mu(A) <= mu(B)
fm_monotone: LEMMA subset?(A,B) => mu(A) <= mu(B) % 2.6.1
fm_IUnion: LEMMA increasing?(X) => convergence(mu o X, mu(IUnion(X)))
fm_IIntersection: LEMMA decreasing?(X)
=> convergence(mu o X, mu(IIntersection(X)))
IMPORTING measure_def[T,S]
measure_from:measure_type = lambda A: (TRUE,mu(A))
END finite_measure
¤ Dauer der Verarbeitung: 0.19 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.
|
