|
%------------------------------------------------------------------------------
% Fubini-Tonelli Theorems
%
% Author: David Lester, Manchester University, NIA, Universite Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Version 1.0 5/06/09 Initial Version
%------------------------------------------------------------------------------
fubini_tonelli_scaf[(IMPORTING subset_algebra_def, measure_def)
T1,T2: TYPE,
S1:sigma_algebra[T1],S2:sigma_algebra[T2],
mu:sigma_finite_measure[T1,S1],
nu:sigma_finite_measure[T2,S2]]: THEORY
BEGIN
IMPORTING product_measure[T1,T2,S1,S2],
integral[[T1,T2],sigma_times(S1,S2),m_times(mu,nu)]
E: VAR (sigma_times(S1,S2))
X: VAR (S1)
Y: VAR (S2)
x: VAR T1
y: VAR T2
i,j,n: VAR nat
IMPORTING product_integral_def[T1,T2,S1,S2,mu,nu],
measure_contraction_props,
measure_equality, % Proof only
finite_fubini_tonelli, % Proof Only
finite_fubini, % Proof Only
indefinite_integral, % Proof only
extended_nnreal@double_nn_sequence, % Proof only
sigma_finite_measure_props % Proof Only
h: VAR nn_measurable[[T1,T2],sigma_times(S1,S2)]
IMPORTING product_integral_def, % Proof only
sigma_finite_measure_props % Proof only
convergent?: MACRO pred[sequence[real]] = topological_convergence.convergent?
product_measure_contraction: LEMMA % SKB 7.4.6
x_eq(contraction(m_times(mu, nu),cross_product(X,Y))(E),
m_times(contraction(mu,X),contraction(nu,Y))(E))
product_sfm_contraction: LEMMA
x_eq(contraction(m_times(mu, nu),
cross_product(A_of(mu)(i),A_of(nu)(j)))(E),
product_measure_approx(mu,nu)(i,j)(E))
product_measure_contraction_n: LEMMA
x_eq(m_times(contraction(mu, P_of(mu)(n)),
contraction(nu, P_of(nu)(n)))(E),
to_measure(fm_times(fm_contraction(mu, P_of(mu)(n)),
fm_contraction(nu, P_of(nu)(n))))(E))
fubini_tonelli_scaf1: LEMMA % 7.4.7
(integrable?(h) <=> integrable1?(h)) AND
(integrable?(h) => integral(h) = integral(integral1[T1,T2,S1,S2,mu,nu](h)))
fubini_tonelli_scaf2: LEMMA % 7.4.7
(integrable?(h) <=> integrable2?(h)) AND
(integrable?(h) => integral(h) = integral(integral2[T1,T2,S1,S2,mu,nu](h)))
END fubini_tonelli_scaf
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.0Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
