| 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 1 kB |
|
Quelle outer_measure_def.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% Outer Measure Theory Definition file. % % Author: David Lester, Manchester University % % Version 1.0 20/08/07 Initial (DRL) %------------------------------------------------------------------------- outer_measure_def[T:TYPE]: THEORY BEGIN IMPORTING extended_nnreal@extended_nnreal, structures@fun_preds_partial[nat,set[T],reals.<=,subset?[T]], sets_aux@indexed_sets_aux[nat,T] f: VAR [set[T]->extended_nnreal] X: VAR [nat->set[T]] a,b: VAR set[T] om_empty?(f):bool = f(emptyset[T]) = (TRUE,0) om_increasing?(f):bool = FORALL a,b: subset?(a,b) => x_le(f(a),f(b)) om_countably_subadditive?(f):bool = FORALL X: x_le(f(IUnion(X)), x_sum(f o X)) outer_measure?(f):bool = om_empty?(f) AND om_increasing?(f) AND om_countably_subadditive?(f) zero_outer_measure(a):extended_nnreal = (TRUE,0) outer_measure: TYPE+ = (outer_measure?) CONTAINING zero_outer_measure END outer_measure_def ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28