Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: outer_measure_props.pvs Sprache: PVS

Original von: 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.5 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.