| 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 measure_props.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Basic properties of measures % % Author: David Lester, Manchester University, NIA, Université Perpignan % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % Version 1.0 1/5/07 Initial Version %------------------------------------------------------------------------------ measure_props[T:TYPE, (IMPORTING subset_algebra_def[T]) S:sigma_algebra, (IMPORTING measure_def[T,S]) m:measure_type]: THEORY BEGIN IMPORTING measure_space_def[T,S], sigma_algebra[T,S], structures@fun_preds_partial[nat,set[T],reals.<=,subset?[T]], measure_def[T,S], series@series_aux n,i: VAR nat a,b,M: VAR measurable_set x,y: VAR extended_nnreal X: VAR sequence[extended_nnreal] DX: VAR disjoint_indexed_measurable E: VAR sequence[measurable_set] mu_fin?(M):bool = m(M)`1 mu(M:{m:(S) | mu_fin?(m)}):nnreal = m(M)`2 m_emptyset: LEMMA m(emptyset[T]) = (TRUE,0) m_countably_additive: LEMMA x_eq(x_sum(m o DX), m(IUnion(DX))) m_disjoint_union:LEMMA disjoint?(a,b) => x_eq(m(union(a,b)),x_add(m(a),m(b))) m_monotone: LEMMA subset?(a,b) => x_le(m(a),m(b)) % 2.6.1 m_union: LEMMA x_le(m(union(a,b)),x_add(m(a),m(b))) m_increasing_convergence: LEMMA increasing?(E) => % 2.6.2 x_converges?(m o E, m(IUnion(E))) m_decreasing_convergence: LEMMA decreasing?(E) AND mu_fin?(E(0)) => % 2.6.3 x_converges?(m o E, m(IIntersection(E))) END measure_props ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28