|
%-------------------------------------------------------------------------
% Extension of a measure to and outer measure
%
% Author: David Lester, Manchester University
%
% Version 1.0 20/08/07 Initial (DRL)
% Version 1.1 29/07/09 Now suitable for interval measures
% (DRL)
%-------------------------------------------------------------------------
ast_def[T:TYPE,A:(nonempty?[set[T]])]: THEORY
BEGIN
ASSUMING IMPORTING subset_algebra_def[T]
A_empty: ASSUMPTION A(emptyset)
A_fullset: ASSUMPTION A(fullset)
A_intersection: ASSUMPTION FORALL (a,b:(A)): A(intersection(a,b))
A_difference: ASSUMPTION FORALL (a,b:(A)):
finite_disjoint_union?(A)(difference(a,b))
ENDASSUMING
IMPORTING generalized_measure_def[T,A],
outer_measure_def[T],
extended_nnreal@double_index[set[T]] % Proof Only
mu: VAR measure_type
z: VAR extended_nnreal
epsilon: VAR posreal
X: VAR set[T]
Y: VAR (A)
I: VAR sequence[(A)]
a,b: VAR set[T]
i,n: VAR nat
A_difference_union: LEMMA A(a) AND finite_disjoint_union?(A)(b) =>
finite_disjoint_union?(A)(difference(a,b))
measure_subadditive: LEMMA A(IUnion(I)) => x_le(mu(IUnion(I)), x_sum(mu o I))
generalized_monotonicity: LEMMA
disjoint?(I) AND
subset?(IUnion(n,I),Y) AND
(FORALL i: i >= n => empty?(I(i))) =>
x_le(x_sum(mu o I),mu(Y))
generalized_measure_monotone: LEMMA FORALL (a,b:(A),mu): subset?(a,b) =>
x_le(mu(a),mu(b))
ast(mu):outer_measure = lambda X: % 7.1.3
x_inf({z | EXISTS I: x_eq(x_sum(mu o I),z) AND subset?(X,IUnion(I))})
outer_measure_eq: LEMMA x_eq(ast(mu)(Y),mu(Y)) % 7.1.3
outer_measure_def: LEMMA
EXISTS I: subset?(X,IUnion(I)) AND
x_le(x_sum(mu o I),x_add(ast(mu)(X),epsilon))
END ast_def
¤ 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.
|
