|
%-------------------------------------------------------------------------
% Measure Theory Definition file.
%
% Author: David Lester, Manchester University
%
% EXPORTS: finite_measure?
%
% Version 1.0 10/04/05
% Version 1.1 20/08/07 Extended to subset algebra (DRL)
%-------------------------------------------------------------------------
measure_def[T:TYPE,(IMPORTING subset_algebra_def[T])
S:subset_algebra]: THEORY
BEGIN
IMPORTING subset_algebra[T,S],
generalized_measure_def[T,S]
convergent: MACRO pred[sequence[real]] = convergence_sequences.convergent?;
limit: MACRO [(convergent)->real] = convergence_sequences.limit ;
i,j,n: VAR nat
f: VAR [(S)->extended_nnreal]
g: VAR [(S)->nnreal]
A: VAR [nat->(S)]
a,b: VAR (S)
x: VAR set[T]
X: VAR disjoint_indexed_measurable
increasing_indexed_measurable?(A):bool = increasing_indexed?(A)
increasing_indexed_measurable: TYPE+ =
(increasing_indexed_measurable?) CONTAINING (LAMBDA i: fullset[T])
P: VAR increasing_indexed_measurable
measure_sigma_finite?(f):bool
= EXISTS X: IUnion(X) = fullset[T] AND FORALL i: f(X(i))`1
sigma_finite_measure?(f):bool = measure?(f) AND measure_sigma_finite?(f)
complete_sigma_finite?(f):bool = measure?(f) AND measure_complete?(f) AND
measure_sigma_finite?(f)
sigma_finite_measure: TYPE+ = (sigma_finite_measure?) CONTAINING zero_measure
complete_sigma_finite:TYPE = (complete_sigma_finite?)
discrete_measure:measure_type
= lambda a: IF is_finite(a) THEN (TRUE,card[T](a)) ELSE (FALSE,0) ENDIF
sigma_finite_measure_is_measure:
JUDGEMENT sigma_finite_measure SUBTYPE_OF measure_type
complete_sigma_finite_is_complete_measure:
JUDGEMENT complete_sigma_finite SUBTYPE_OF complete_measure
complete_sigma_finite_is_sigma_finite_measure:
JUDGEMENT complete_sigma_finite SUBTYPE_OF sigma_finite_measure
measure_monotone: LEMMA measure?(f) AND subset?(a,b) => x_le(f(a),f(b))
measure_union: LEMMA measure?(f) => x_le(f(union(a,b)),x_add(f(a),f(b)))
measure_def: LEMMA % generalized SKB 2.6 Ex 4
(measure?(f) <=>
(measure_empty?(f) AND
(FORALL (a,b:(S)): disjoint?(a,b)
=> x_eq(f(union(a,b)),x_add(f(a),f(b)))) AND
(FORALL X: S(IUnion(X)) => x_le(f(IUnion(X)),x_sum(f o X)))))
finite_measure_def: LEMMA
finite_measure?(g) <=>
(g(emptyset[T]) = 0 AND
(FORALL (a,b:(S)): disjoint?(a,b) => g(union(a,b)) = g(a)+g(b)) AND
(FORALL X: S(IUnion(X)) AND convergent(series(g o X)) =>
g(IUnion(X)) <= limit(series(g o X))))
A_of(f:sigma_finite_measure):disjoint_indexed_measurable
= choose({X | IUnion(X) = fullset[T] AND FORALL i: f(X(i))`1})
P_of(f:sigma_finite_measure)(n):(S)
= IUnion(lambda i: IF i <= n THEN A_of(f)(i) ELSE emptyset[T] ENDIF)
mu: VAR sigma_finite_measure
A_of_def1: LEMMA IUnion(A_of(mu)) = fullset[T]
A_of_def2: LEMMA FORALL n: mu(A_of(mu)(n))`1
P_of_def1: LEMMA IUnion(P_of(mu)) = fullset[T]
P_of_def2: LEMMA FORALL n: mu(P_of(mu)(n))`1
P_of_def3: LEMMA FORALL i,j: i <= j => subset?(P_of(mu)(i),P_of(mu)(j))
sigma_finite_def1: LEMMA
sigma_finite_measure?(f) <=>
(measure?(f) AND EXISTS X: IUnion(X) = fullset[T] AND FORALL i: f(X(i))`1)
sigma_finite_def2: LEMMA
sigma_finite_measure?(f) <=>
(measure?(f) AND EXISTS P: IUnion(P) = fullset[T] AND FORALL i: f(P(i))`1)
END measure_def
¤ Dauer der Verarbeitung: 0.20 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.
|
