Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: measure_completion_aux.pvs Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% Auxilliary results to complete a measure
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Note: not described in Berberian
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

measure_completion_aux[T:TYPE]: THEORY

BEGIN

  IMPORTING subset_algebra_def[T],
            measure_def,
            measure_theory,
            measure_props

  XS: VAR setofsets[T]
  A,B,X:  VAR set[T]
  z:  VAR extended_nnreal

  almost_measurable?(S:sigma_algebra[T],m:measure_type[T,S])(X):bool
    = EXISTS (Y:(S),N1,N2:negligible[T,S,m]): X = difference(union(Y,N1),N2)

  empty_almost_measurable: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
      almost_measurable?(S,m)(emptyset[T])

  complement_almost_measurable: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
      almost_measurable?(S,m)(X) <=> almost_measurable?(S,m)(complement(X))

  Union_almost_measurable: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
      every(almost_measurable?(S,m),XS) AND is_countable(XS) =>
            almost_measurable?(S,m)(Union(XS))

  completion(S:sigma_algebra[T],m:measure_type[T,S]):sigma_algebra[T]
    = {X | almost_measurable?(S,m)(X)}

  generated_completion: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
    generated_sigma_algebra(union(S,fullset[negligible[T,S,m]]))
      = completion(S,m)

  completion_extends: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
                            S(X) => completion(S,m)(X)

  negligible_completion: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S]):
                            negligible_set?[T,S,m](X) => completion(S,m)(X)

  is_completion(S:sigma_algebra[T],m:measure_type[T,S])(A,B):bool
    = completion(S,m)(A) AND S(B) =>
      EXISTS (N1,N2:negligible[T,S,m]): A = difference(union(B,N1),N2)

  m_completions: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S],X,A,B):
                       completion(S,m)(X) AND S(A) AND S(B) AND
                       is_completion(S,m)(X,A) AND  is_completion(S,m)(X,B) =>
                       x_eq(m(A),m(B))

  choose_completion: LEMMA FORALL (S:sigma_algebra[T],m:measure_type[T,S],X):
                       completion(S,m)(X) =>
         is_completion(S,m)(X,choose({Y:(S) | EXISTS (N1,N2:negligible[T,S,m]):
                 X = difference(union(Y,N1),N2)}))

  completion(S:sigma_algebra[T],m:measure_type[T,S]):
                                            complete_measure[T,completion(S,m)]
    = lambda (X:(completion(S,m))):
        m(choose({Y:(S) | EXISTS (N1,N2:negligible[T,S,m]):
                 X = difference(union(Y,N1),N2)}))

  completion_measurable: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S],X:(S)):
           x_eq(completion(S,m)(X),m(X))

  completion_negligible: LEMMA
    FORALL (S:sigma_algebra[T],m:measure_type[T,S],N:negligible[T,S,m]):
           completion(S,m)(N) = (TRUE,0)

END measure_completion_aux

¤ Dauer der Verarbeitung: 0.1 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.