| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
Quelle outer_measure_props.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% 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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28