products/Sources/formale Sprachen/PVS/measure_integration/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: measure_def.pvs   Sprache: Unknown

%-------------------------------------------------------------------------
% 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

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]