|
%------------------------------------------------------------------------------
% Product of two sigam-finite measures
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Generalizing the results for finite measures to sigma-finite measures.
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
product_measure[(IMPORTING subset_algebra_def)
T1,T2:TYPE,
S1:sigma_algebra[T1], S2:sigma_algebra[T2]]: THEORY
BEGIN
IMPORTING product_sigma[T1,T2,S1,S2],
measure_contraction[T1,S1],
measure_contraction[T2,S2],
measure_contraction[[T1,T2],sigma_times(S1,S2)],
product_finite_measure[T1,T2,S1,S2],
extended_nnreal@double_index[set[[T1,T2]]] % Proof Only
mu: VAR sigma_finite_measure[T1,S1]
nu: VAR sigma_finite_measure[T2,S2]
X: VAR (S1)
Y: VAR (S2)
M: VAR (sigma_times(S1,S2))
z: VAR [T1,T2]
i,j,n: VAR nat
product_measure_approx(mu,nu)(i,j):finite_measure[[T1,T2],sigma_times(S1,S2)]
= fm_times(fm_contraction[T1,S1](mu,A_of(mu)(i)),
fm_contraction[T2,S2](nu,A_of(nu)(j)))
m_times(mu,nu):sigma_finite_measure[[T1,T2],sigma_times(S1,S2)] % 7.2.12
= lambda M:
x_sum(lambda i: x_sum(lambda j:
to_measure(product_measure_approx(mu,nu)(i,j))(M)))
m_times_alt: LEMMA
x_eq(m_times(mu,nu)(M),
x_sum(lambda j: x_sum(lambda i:
to_measure(product_measure_approx(mu,nu)(i,j))(M))))
rectangle_measure: LEMMA
x_eq(m_times(mu,nu)(cross_product(X,Y)),x_times(mu(X),nu(Y)))
phi1(X):simple[[T1,T2],sigma_times(S1,S2)]= phi(cross_product(X,fullset[T2]))
phi2(Y):simple[[T1,T2],sigma_times(S1,S2)]= phi(cross_product(fullset[T1],Y))
END product_measure
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.59Angebot
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
|
