Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


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

quality84%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.