Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 3 kB

Quelle measure_space_def.pvs Sprache: PVS

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

measure_space_def[T:TYPE, (IMPORTING subset_algebra_def[T])
                  S:sigma_algebra]: THEORY

BEGIN

  IMPORTING sigma_algebra[T,S],
            reals@real_fun_ops_aux[T],
            structures@const_fun_def[T,real],
            metric_space@real_topology,
            topology@basis[real],
            borel[real,metric_induced_topology],
            real_borel,
            sets_aux@countable_props,
            sets_aux@inverse_image_Union,      % Proof Only
            sets_aux@countable_image,  % Proof Only
            sets_aux@countable_set     % Proof Only

  X: VAR set[T]
  Y: VAR set[real]
  x,y,z: VAR T
  f: VAR [T->real]
  B: VAR borel
  c: VAR real
  q: VAR rational
  r: VAR posreal

  measurable_set?(X):bool = S(X)

  measurable_set: TYPE+ = (measurable_set?) CONTAINING emptyset[T]

  a,b: VAR measurable_set
  SS:  VAR sequence[measurable_set]
  M:   VAR countable_set[(S)]

  measurable_emptyset:      JUDGEMENT emptyset[T]       HAS_TYPE measurable_set
  measurable_fullset:       JUDGEMENT fullset[T]        HAS_TYPE measurable_set
  measurable_complement:    JUDGEMENT complement(a)     HAS_TYPE measurable_set
  measurable_union:         JUDGEMENT union(a,b)        HAS_TYPE measurable_set
  measurable_intersection:  JUDGEMENT intersection(a,b) HAS_TYPE measurable_set
  measurable_difference:    JUDGEMENT difference(a,b)   HAS_TYPE measurable_set
  measurable_Union:         JUDGEMENT Union(M)          HAS_TYPE measurable_set
  measurable_Intersection:  JUDGEMENT Intersection(M)   HAS_TYPE measurable_set
  measurable_IUnion:        JUDGEMENT IUnion(SS)        HAS_TYPE measurable_set
  measurable_IIntersection: JUDGEMENT IIntersection(SS) HAS_TYPE measurable_set

  measurable_function?(f):bool = FORALL B: measurable_set?(inverse_image(f,B))

  measurable_function: TYPE+ = (measurable_function?) CONTAINING (LAMBDA x: 0)

  g,g1,g2: VAR measurable_function

  measurable_is_function: JUDGEMENT measurable_function SUBTYPE_OF [T->real]
  constant_is_measurable: JUDGEMENT (constant?[T,real]) SUBTYPE_OF
                                                            measurable_function

  U: VAR setofsets[real]

  measurable_def: LEMMA borel? = generated_sigma_algebra(U) =>
                        (measurable_function?(f) <=>
                         FORALL (X:(U)): S(inverse_image(f,X)))

  measurable_def2: LEMMA measurable_function?(f) <=>
                         FORALL (i:open_interval): S(inverse_image(f,i))

  measurable_gt: LEMMA measurable_function?(f) <=> FORALL c: S({z| f(z) >  c})
  measurable_le: LEMMA measurable_function?(f) <=> FORALL c: S({z| f(z) <= c})
  measurable_lt: LEMMA measurable_function?(f) <=> FORALL c: S({z| f(z) <  c})
  measurable_ge: LEMMA measurable_function?(f) <=> FORALL c: S({z| f(z) >= c})

  measurable_gt2: LEMMA measurable_function?(f) <=> FORALL q: S({z| f(z) >  q})
  measurable_le2: LEMMA measurable_function?(f) <=> FORALL q: S({z| f(z) <= q})
  measurable_lt2: LEMMA measurable_function?(f) <=> FORALL q: S({z| f(z) <  q})
  measurable_ge2: LEMMA measurable_function?(f) <=> FORALL q: S({z| f(z) >= q})

  scal_measurable:  JUDGEMENT *(c,g)   HAS_TYPE measurable_function
  sum_measurable:   JUDGEMENT +(g1,g2) HAS_TYPE measurable_function
  opp_measurable:   JUDGEMENT -(g)     HAS_TYPE measurable_function
  diff_measurable:  JUDGEMENT -(g1,g2) HAS_TYPE measurable_function

END measure_space_def

quality99%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

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.