Quelle generalized_measure_def.pvs Sprache: PVS

%-------------------------------------------------------------------------
% Measure Theory Definition file.
%
%     Author: David Lester, Manchester University
%
%  EXPORTS: finite_measure?
%
%     Version 1.0           10/04/05
%     Version 1.1           20/08/07 Extended to subset algebra (DRL)
%-------------------------------------------------------------------------

generalized_measure_def[T:TYPE,S:setofsets[T]]: THEORY

BEGIN

  ASSUMING

    S_empty:        ASSUMPTION S(emptyset)

  ENDASSUMING

  IMPORTING series@series,
            sets_aux@indexed_sets_aux[nat,T],
            sets_aux@nat_indexed_sets[T],
            metric_space@convergence_aux,
            extended_nnreal@extended_nnreal

%  limit: MACRO [(convergence_sequences.convergent?)->real]
%                                          = convergence_sequences.limit ;

  i,j,n: VAR nat
  f:     VAR [(S)->extended_nnreal]
  g:     VAR [(S)->nnreal]
  A:     VAR [nat->(S)]
  a,b:   VAR (S)
  x:     VAR set[T]

  disjoint_indexed_measurable?(A):bool = disjoint?(A)

  disjoint_indexed_measurable: TYPE+ =
       (disjoint_indexed_measurable?) CONTAINING (LAMBDA i: emptyset[T])

  disjoint_indexed_measurable_is_disjoint_indexed_set: JUDGEMENT
       disjoint_indexed_measurable SUBTYPE_OF disjoint_indexed_set[nat,T]

  X:   VAR disjoint_indexed_measurable

  measure_empty?(f):bool
    = f(emptyset[T]) = (TRUE,0)

  measure_countably_additive?(f): bool
    = FORALL X: S(IUnion(X)) => x_eq(x_sum(f o X),f(IUnion(X)))

  measure_complete?(f):bool
    = (FORALL x,a: (subset?(x,a) AND f(a) = (TRUE,0)) => S(x))

  measure?(f):bool              = measure_empty?(f) AND
                                  measure_countably_additive?(f)
  complete_measure?(f):bool     = measure?(f) AND measure_complete?(f)

  zero_measure(a):extended_nnreal = (TRUE,0)

  measure_type:         TYPE+ = (measure?)              CONTAINING zero_measure

  trivial_measure:measure_type
   = lambda a: IF empty?(a) THEN (TRUE,0) ELSE (FALSE,0) ENDIF

  complete_measure: TYPE+ = (complete_measure?) CONTAINING trivial_measure

  complete_measure_is_measure:
                JUDGEMENT complete_measure     SUBTYPE_OF measure_type

  measure_disjoint_union: LEMMA
    measure?(f) AND disjoint?(a,b) AND S(union(a,b)) =>
                                          x_eq(f(union(a,b)),x_add(f(a),f(b)))

  finite_measure?(g):bool
    = g(emptyset[T]) = 0 AND
      FORALL X: S(IUnion(X)) => convergence(series(g o X),g(IUnion(X)))

  complete_finite_measure?(g):bool
    = finite_measure?(g) AND FORALL x,a: subset?(x,a) AND g(a) = 0 => S(x)

  trivial_finite_measure(A:(S)):[nnreal] = 0

  finite_measure:   TYPE+ = (finite_measure?) CONTAINING trivial_finite_measure
  complete_finite_measure: TYPE  = (complete_finite_measure?)

  complete_finite_measure_is_finite_measure:
                   JUDGEMENT complete_finite_measure SUBTYPE_OF finite_measure

  to_measure(m:finite_measure):measure_type = lambda a: (TRUE,m(a))

  F: VAR sequence[measure_type]

  x_sum_measure:   LEMMA measure?(lambda a: (x_sum(lambda i: F(i)(a))))

END generalized_measure_def

quality82%

¤ 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.