|
%------------------------------------------------------------------------------
% 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.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
