| 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 finite_measure.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Finite Measure Theory file. % % Author: David Lester, Manchester University % % % Version 1.0 10/4/05 %------------------------------------------------------------------------- finite_measure[T:TYPE, (IMPORTING subset_algebra_def[T]) S:sigma_algebra, (IMPORTING measure_def[T,S]) mu:finite_measure]: THEORY BEGIN IMPORTING sets_lemmas_aux, % Proof only, RWB: was sets_aux@ sets_aux@indexed_sets_aux[nat,T], sigma_algebra[T,S], series@series_aux, % Proof only structures@fun_preds_partial[nat,set[T],reals.<=,subset?[T]] X: VAR [nat->(S)] A,B: VAR (S) fm_emptyset: LEMMA mu(emptyset) = 0 fm_convergence: LEMMA disjoint?(X) => convergence(series(mu o X), mu(IUnion(X))) fm_disjointunion: LEMMA disjoint?(A,B) => mu(union(A,B)) = mu(A) + mu(B) fm_complement: LEMMA mu(complement(A)) = mu(fullset) - mu(A) fm_union: LEMMA mu(union(A,B)) = mu(A) + mu(B) - mu(intersection(A,B)) fm_intersection: LEMMA mu(intersection(A,B)) = mu(A) + mu(B) - mu(union(A,B)) fm_difference: LEMMA mu(difference(A,B)) = mu(A) - mu(B) + mu(difference(B,A)) fm_subset: LEMMA subset?(A,B) => mu(B) = mu(A) + mu(difference(B,A)) fm_subset_le: LEMMA subset?(A,B) => mu(A) <= mu(B) fm_monotone: LEMMA subset?(A,B) => mu(A) <= mu(B) % 2.6.1 fm_IUnion: LEMMA increasing?(X) => convergence(mu o X, mu(IUnion(X))) fm_IIntersection: LEMMA decreasing?(X) => convergence(mu o X, mu(IIntersection(X))) IMPORTING measure_def[T,S] measure_from:measure_type = lambda A: (TRUE,mu(A)) END finite_measure ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28