| 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_equality.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Measure Equality % % Author: David Lester, Manchester University, NIA, Université Perpignan % % All references are to SK Berberian "Fundamentals of Real Analysis", % Springer, 1991 % % If mu(E) = nu(E) for every measurable set E, then the integrals are the same. % % Version 1.0 1/5/07 Initial Version %------------------------------------------------------------------------------ measure_equality[T:TYPE, (IMPORTING subset_algebra_def[T]) S:sigma_algebra]: THEORY BEGIN IMPORTING measure_def[T,S] mu,nu: VAR measure_type x: VAR T f: VAR [T->real] g: VAR [T->nnreal] E: VAR (S) IMPORTING integral measure_eq_isf?: LEMMA (FORALL E: x_eq(mu(E),nu(E))) => (isf?[T,S,mu](f) <=> isf?[T,S,nu](f)) measure_eq_isf: LEMMA (FORALL E: x_eq(mu(E),nu(E))) AND (isf?[T,S,mu](f) OR isf?[T,S,nu](f)) => (isf_integral[T,S,mu](f) = isf_integral[T,S,nu](f)) measure_eq_nn_integrable?: LEMMA (FORALL E: x_eq(mu(E),nu(E))) => (nn_integrable?[T,S,mu](g) <=> nn_integrable?[T,S,nu](g)) measure_eq_nn_integral: LEMMA (FORALL E: x_eq(mu(E),nu(E))) AND (nn_integrable?[T,S,mu](g) OR nn_integrable?[T,S,nu](g)) => (nn_integral[T,S,mu](g) = nn_integral[T,S,nu](g)) measure_eq_integrable?: LEMMA (FORALL E: x_eq(mu(E),nu(E))) => (integrable?[T,S,mu](f) <=> integrable?[T,S,nu](f)) measure_eq_integral: LEMMA (FORALL E: x_eq(mu(E),nu(E))) AND (integrable?[T,S,mu](f) OR integrable?[T,S,nu](f)) => (integral[T,S,mu](f) = integral[T,S,nu](f)) END measure_equality ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28