|
%------------------------------------------------------------------------------
% Properties of Outer Measures
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
outer_measure_props[T:TYPE,(IMPORTING outer_measure_def[T])
m:outer_measure]: THEORY
BEGIN
IMPORTING outer_measure_def[T],
subset_algebra_def[T],
orders@bounded_nats % proof only
i: VAR nat
x,y: VAR set[T]
A: VAR sequence[set[T]]
m_outer_empty: LEMMA m(emptyset[T]) = (TRUE,0)
m_outer_increasing: LEMMA subset?(x,y) => x_le(m(x),m(y))
m_outer_subadditive: LEMMA x_le(m(IUnion(A)),x_sum(m o A))
outer_negligible?(x):bool = m(x) = (TRUE,0)
outer_measurable?(x):bool % (Generalised) 2.2.2
= FORALL y: x_eq(m(y), x_add(m(intersection(y,x)),
m(intersection(y,complement(x)))))
outer_negligible: TYPE+ = (outer_negligible?) CONTAINING emptyset[T]
outer_measurable: TYPE+ = (outer_measurable?) CONTAINING emptyset[T]
% (Generalised) 2.2.3
pairwise_subadditive:LEMMA x_le(m(y),x_add(m(intersection(y,x)),
m(intersection(y,complement(x)))))
outer_measurable_def:LEMMA
outer_measurable?(x) <=>
(FORALL y: x_le(x_add(m(intersection(y,x)),
m(intersection(y,complement(x)))),m(y)))
outer_negligible_is_outer_measurable:
JUDGEMENT outer_negligible SUBTYPE_OF outer_measurable
a,b: VAR outer_measurable
X: VAR sequence[outer_measurable]
S: VAR setofsets[T]
% (Generalised) 2.2.4
outer_measurable_complement:JUDGEMENT complement(a) HAS_TYPE outer_measurable
outer_measurable_emptyset: JUDGEMENT emptyset[T] HAS_TYPE outer_measurable
outer_measurable_fullset: JUDGEMENT fullset[T] HAS_TYPE outer_measurable
outer_measurable_union: JUDGEMENT union(a,b) HAS_TYPE outer_measurable
outer_measurable_intersection:
JUDGEMENT intersection(a,b) HAS_TYPE outer_measurable
outer_measurable_difference:
JUDGEMENT difference(a,b) HAS_TYPE outer_measurable
outer_measurable_disjoint_union: LEMMA disjoint?(a,b) =>
x_eq(m(intersection(x,union(a,b))),
x_add(m(intersection(x,a)),m(intersection(x,b))))
outer_measurable_IUnion: JUDGEMENT IUnion(X) HAS_TYPE outer_measurable
outer_measurable_IIntersection:
JUDGEMENT IIntersection(X) HAS_TYPE outer_measurable
outer_measurable_Union: LEMMA is_countable(S) AND
every(outer_measurable?,S) =>
outer_measurable?(Union(S))
outer_measurable_Intersection: LEMMA is_countable(S) AND
every(outer_measurable?,S) =>
outer_measurable?(Intersection(S))
outer_measurable_disjoint_IUnion: LEMMA disjoint?(X) => % (Generalised) 2.2.5
x_eq(m(intersection(x,IUnion(X))),
x_sum(lambda i: m(intersection(x,X(i)))))
outer_measure_disjoint_IUnion: LEMMA disjoint?(X) => % (Generalised) 2.2.10
x_eq(m(IUnion(X)),x_sum(m o X))
outer_measurable_is_sigma_algebra: LEMMA % 7.1.5
sigma_algebra?(fullset[outer_measurable])
induced_sigma_algebra:sigma_algebra[T] = (outer_measurable?)
IMPORTING measure_def[T,induced_sigma_algebra]
induced_measure:complete_measure % 7.1.5
= restrict[set[T],(induced_sigma_algebra),extended_nnreal](m)
induced_measure_rew: LEMMA induced_measure(a) = m(a)
n,n1,n2: VAR outer_negligible
outer_negligible_emptyset: JUDGEMENT emptyset[T] HAS_TYPE outer_negligible
outer_negligible_union: JUDGEMENT union(n1,n2) HAS_TYPE outer_negligible
outer_negligible_subset: LEMMA subset?(x,n) => outer_negligible?(x)
END outer_measure_props
¤ Dauer der Verarbeitung: 0.2 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.
|
