|
%------------------------------------------------------------------------------
% Measure Contraction Properties
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Decomposition of an integral into a
% sequence of integrals over measures contractions
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
measure_contraction_props[T:TYPE, (IMPORTING subset_algebra_def[T])
S:sigma_algebra, (IMPORTING measure_def[T,S])
mu:measure_type]: THEORY
BEGIN
IMPORTING measure_props[T,S,mu],
measure_contraction[T,S],
integral_convergence_scaf % Proof only
A: VAR disjoint_indexed_measurable
h: VAR measurable_function
x: VAR T
n: VAR nat
convergent?: MACRO pred[sequence[real]] = topological_convergence.convergent?
contraction_integrable_def: LEMMA
IUnion(A) = fullset[T] AND
(FORALL x: h(x) >= 0) =>
(integrable?[T,S,mu](h) <=>
((FORALL n: integrable?[T,S,contraction(mu,A(n))](h)) AND
convergent?(series(lambda n: integral[T,S,contraction(mu,A(n))](h)))))
END measure_contraction_props
¤ Dauer der Verarbeitung: 0.25 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.
|
