Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Cobol/Test-Suite/SQL M/     Datei vom 4.1.2008 mit Größe 47 kB image not shown  

Quellcode-Bibliothek complete_measure_theory.pvs   Sprache: unbekannt

 
%-------------------------------------------------------------------------
% Complete Measure Theory
%
%     Author: David Lester, Manchester University
%
%     Version 1.0           04/05/09    Initial (DRL)
%-------------------------------------------------------------------------

complete_measure_theory[T:TYPE,          (IMPORTING subset_algebra_def[T])
                        S:sigma_algebra, (IMPORTING measure_def[T,S])
                        mu:complete_measure]: THEORY

BEGIN

  IMPORTING measure_space_def[T,S],
            sigma_algebra[T,S],
            measure_theory[T,S,mu],
            measure_props[T,S,mu]

  N: VAR null_set
  X: VAR set[T]
  E: VAR negligible
  f: VAR [T->real]
  g: VAR measurable_function

  null_subset:        LEMMA subset?(X,N)  => null_set?(X)
  null_is_negligible: LEMMA null_set?(X) <=> negligible_set?(X)
  ae_eq_measurable:   LEMMA ae_eq?(f,g)   => measurable_function?(f)

END complete_measure_theory

100%


[ 0.7Quellennavigators  Projekt   ]