| Quellcodebibliothek Statistik Leitseite 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 ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28