|
%-------------------------------------------------------------------------
% 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)
%-------------------------------------------------------------------------
generalized_measure_def[T:TYPE,S:setofsets[T]]: THEORY
BEGIN
ASSUMING
S_empty: ASSUMPTION S(emptyset)
ENDASSUMING
IMPORTING series@series,
sets_aux@indexed_sets_aux[nat,T],
sets_aux@nat_indexed_sets[T],
metric_space@convergence_aux,
extended_nnreal@extended_nnreal
% limit: MACRO [(convergence_sequences.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]
disjoint_indexed_measurable?(A):bool = disjoint?(A)
disjoint_indexed_measurable: TYPE+ =
(disjoint_indexed_measurable?) CONTAINING (LAMBDA i: emptyset[T])
disjoint_indexed_measurable_is_disjoint_indexed_set: JUDGEMENT
disjoint_indexed_measurable SUBTYPE_OF disjoint_indexed_set[nat,T]
X: VAR disjoint_indexed_measurable
measure_empty?(f):bool
= f(emptyset[T]) = (TRUE,0)
measure_countably_additive?(f): bool
= FORALL X: S(IUnion(X)) => x_eq(x_sum(f o X),f(IUnion(X)))
measure_complete?(f):bool
= (FORALL x,a: (subset?(x,a) AND f(a) = (TRUE,0)) => S(x))
measure?(f):bool = measure_empty?(f) AND
measure_countably_additive?(f)
complete_measure?(f):bool = measure?(f) AND measure_complete?(f)
zero_measure(a):extended_nnreal = (TRUE,0)
measure_type: TYPE+ = (measure?) CONTAINING zero_measure
trivial_measure:measure_type
= lambda a: IF empty?(a) THEN (TRUE,0) ELSE (FALSE,0) ENDIF
complete_measure: TYPE+ = (complete_measure?) CONTAINING trivial_measure
complete_measure_is_measure:
JUDGEMENT complete_measure SUBTYPE_OF measure_type
measure_disjoint_union: LEMMA
measure?(f) AND disjoint?(a,b) AND S(union(a,b)) =>
x_eq(f(union(a,b)),x_add(f(a),f(b)))
finite_measure?(g):bool
= g(emptyset[T]) = 0 AND
FORALL X: S(IUnion(X)) => convergence(series(g o X),g(IUnion(X)))
complete_finite_measure?(g):bool
= finite_measure?(g) AND FORALL x,a: subset?(x,a) AND g(a) = 0 => S(x)
trivial_finite_measure(A:(S)):[nnreal] = 0
finite_measure: TYPE+ = (finite_measure?) CONTAINING trivial_finite_measure
complete_finite_measure: TYPE = (complete_finite_measure?)
complete_finite_measure_is_finite_measure:
JUDGEMENT complete_finite_measure SUBTYPE_OF finite_measure
to_measure(m:finite_measure):measure_type = lambda a: (TRUE,m(a))
F: VAR sequence[measure_type]
x_sum_measure: LEMMA measure?(lambda a: (x_sum(lambda i: F(i)(a))))
END generalized_measure_def
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
