| products/sources/formale Sprachen/PVS/measure_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: measure_contraction.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
%------------------------------------------------------------------------------
% Measure Contraction % % Author: David Lester, Manchester University, NIA, Université Perpignan % % If mu is a measure, so is the contraction lambda E: mu(intersection(A,E)). % % The integrals using the contracted measure are the same as the indefinite % integral % % Version 1.0 1/5/07 Initial Version %------------------------------------------------------------------------------ measure_contraction[T:TYPE, (IMPORTING subset_algebra_def[T]) S:sigma_algebra]: THEORY BEGIN IMPORTING measure_def[T,S], measure_space[T,S] ; *(f,g:[T -> real]): MACRO [T -> real] = (reals@real_fun_ops[T].*)(f,g) mu: VAR measure_type nu: VAR sigma_finite_measure A,E: VAR measurable_set f: VAR measurable_function i: VAR nat contraction(mu,A):measure_type = lambda E: mu(intersection(A,E)) % SKB 7.4.2 fm_contraction(mu:measure_type,A:{E | mu(E)`1}):finite_measure = lambda E: mu(intersection(A,E))`2 sigma_finite_contraction_def: LEMMA x_eq(nu(E),x_sum(LAMBDA i: (TRUE,fm_contraction(nu,A_of(nu)(i))(E)))) IMPORTING isf, nn_integral, integral, indefinite_integral, % Proof only integral_convergence % Proof only contraction_is_sigma_finite: JUDGEMENT contraction(nu,A) HAS_TYPE sigma_finite_measure contraction_isf: LEMMA FORALL (f:simple): isf?[T,S,contraction(mu,A)](f) <=> isf?[T,S,mu](phi[T,S](A)*f) contraction_isf_integral: LEMMA FORALL (f:isf[T,S,contraction(mu,A)]): isf_integral[T,S,contraction(mu,A)](f) = isf_integral[T,S,mu](phi[T,S](A)*f) contraction_nn_integrable: LEMMA FORALL (f:nn_measurable): nn_integrable?[T,S,contraction(mu,A)](f) <=> nn_integrable?[T,S,mu](phi[T,S](A)*f) contraction_nn_integral: LEMMA FORALL (f:nn_integrable[T,S,contraction(mu,A)]): nn_integral[T,S,contraction(mu,A)](f) = nn_integral[T,S,mu](phi[T,S](A)*f) contraction_integrable: LEMMA % SKB 7.4.4 integrable?[T,S,contraction(mu,A)](f) <=> integrable?[T,S,mu](phi[T,S](A)*f) contraction_integral: LEMMA % SKB 7.4.4 FORALL (f:integrable[T,S,contraction(mu,A)]): integral[T,S,contraction(mu,A)](f) = integral[T,S,mu](phi[T,S](A)*f) END measure_contraction ¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
