products/sources/formale Sprachen/PVS/probability/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   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.19 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

in der Quellcodebibliothek suchen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff