Quellcode-Bibliothek 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)
%-------------------------------------------------------------------------

measure_def[T:TYPE,(IMPORTING subset_algebra_def[T])
            S:subset_algebra]: THEORY

BEGIN

  IMPORTING subset_algebra[T,S],
            generalized_measure_def[T,S]

  convergent: MACRO pred[sequence[real]] = convergence_sequences.convergent?;
  limit:      MACRO [(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]
  X:     VAR disjoint_indexed_measurable

  increasing_indexed_measurable?(A):bool = increasing_indexed?(A)

  increasing_indexed_measurable: TYPE+ =
       (increasing_indexed_measurable?) CONTAINING (LAMBDA i: fullset[T])

  P:   VAR increasing_indexed_measurable

  measure_sigma_finite?(f):bool
    = EXISTS X: IUnion(X) = fullset[T] AND FORALL i: f(X(i))`1

  sigma_finite_measure?(f):bool = measure?(f) AND measure_sigma_finite?(f)
  complete_sigma_finite?(f):bool = measure?(f) AND measure_complete?(f) AND
                                   measure_sigma_finite?(f)

  sigma_finite_measure: TYPE+ = (sigma_finite_measure?) CONTAINING zero_measure
  complete_sigma_finite:TYPE  = (complete_sigma_finite?)

  discrete_measure:measure_type
   = lambda a: IF is_finite(a) THEN (TRUE,card[T](a)) ELSE (FALSE,0) ENDIF

  sigma_finite_measure_is_measure:
                JUDGEMENT sigma_finite_measure SUBTYPE_OF measure_type
  complete_sigma_finite_is_complete_measure:
                JUDGEMENT complete_sigma_finite SUBTYPE_OF complete_measure
  complete_sigma_finite_is_sigma_finite_measure:
                JUDGEMENT complete_sigma_finite SUBTYPE_OF sigma_finite_measure

  measure_monotone: LEMMA measure?(f) AND subset?(a,b) => x_le(f(a),f(b))
  measure_union:    LEMMA measure?(f) => x_le(f(union(a,b)),x_add(f(a),f(b)))

  measure_def: LEMMA                                 % generalized SKB 2.6 Ex 4
   (measure?(f) <=>
    (measure_empty?(f) AND
     (FORALL (a,b:(S)): disjoint?(a,b)
                            => x_eq(f(union(a,b)),x_add(f(a),f(b)))) AND
     (FORALL X: S(IUnion(X)) => x_le(f(IUnion(X)),x_sum(f o X)))))

  finite_measure_def: LEMMA
    finite_measure?(g) <=>
     (g(emptyset[T]) = 0 AND
      (FORALL (a,b:(S)): disjoint?(a,b) => g(union(a,b)) = g(a)+g(b)) AND
      (FORALL X: S(IUnion(X)) AND convergent(series(g o X)) =>
                 g(IUnion(X)) <= limit(series(g o X))))

  A_of(f:sigma_finite_measure):disjoint_indexed_measurable
    = choose({X | IUnion(X) = fullset[T] AND FORALL i: f(X(i))`1})

  P_of(f:sigma_finite_measure)(n):(S)
    = IUnion(lambda i: IF i <= n THEN A_of(f)(i) ELSE emptyset[T] ENDIF)

  mu: VAR sigma_finite_measure

  A_of_def1: LEMMA IUnion(A_of(mu)) = fullset[T]
  A_of_def2: LEMMA FORALL n: mu(A_of(mu)(n))`1
  P_of_def1: LEMMA IUnion(P_of(mu)) = fullset[T]
  P_of_def2: LEMMA FORALL n: mu(P_of(mu)(n))`1
  P_of_def3: LEMMA FORALL i,j: i <= j => subset?(P_of(mu)(i),P_of(mu)(j))

  sigma_finite_def1: LEMMA
    sigma_finite_measure?(f) <=>
    (measure?(f) AND EXISTS X: IUnion(X) = fullset[T] AND FORALL i: f(X(i))`1)

  sigma_finite_def2: LEMMA
    sigma_finite_measure?(f) <=>
    (measure?(f) AND EXISTS P: IUnion(P) = fullset[T] AND FORALL i: f(P(i))`1)

END measure_def

quality68%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.