|
%------------------------------------------------------------------------------
% Iterated Integrals over [T1,T2]
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Version 1.0 1/5/07 Initial Version
%------------------------------------------------------------------------------
product_integral_def[(IMPORTING subset_algebra_def, measure_def)
T1,T2: TYPE,
S1:sigma_algebra[T1],S2:sigma_algebra[T2],
mu:measure_type[T1,S1], nu:measure_type[T2,S2]]: THEORY
BEGIN
IMPORTING integral[T1,S1,mu],
integral[T2,S2,nu],
reals@real_fun_ops[[T1,T2]]
h: VAR [[T1,T2]->real]
f: VAR integrable[T1,S1,mu]
g: VAR integrable[T2,S2,nu]
N1: VAR null_set[T1,S1,mu]
N2: VAR null_set[T2,S2,nu]
x: VAR T1
y: VAR T2
c: VAR real
integrable1?(h):bool
= EXISTS N1,f: FORALL x: NOT member(x,N1) =>
integrable?(lambda y: h(x,y)) AND
integral(lambda y: h(x,y)) = f(x)
integrable2?(h):bool
= EXISTS N2,g: FORALL y: NOT member(y,N2) =>
integrable?(lambda x: h(x,y)) AND
integral(lambda x: h(x,y)) = g(y)
integrable1: TYPE+ = (integrable1?) CONTAINING (lambda x,y: 0)
integrable2: TYPE+ = (integrable2?) CONTAINING (lambda x,y: 0)
g1,h1: VAR integrable1
g2,h2: VAR integrable2
integrable1_zero: LEMMA integrable1?(lambda x,y: 0)
integrable1_add: JUDGEMENT +(g1,h1) HAS_TYPE integrable1
integrable1_scal: JUDGEMENT *(c,h1) HAS_TYPE integrable1
integrable1_opp: JUDGEMENT -(h1) HAS_TYPE integrable1
integrable1_diff: JUDGEMENT -(g1,h1) HAS_TYPE integrable1
integrable2_zero: LEMMA integrable2?(lambda x,y: 0)
integrable2_add: JUDGEMENT +(g2,h2) HAS_TYPE integrable2
integrable2_scal: JUDGEMENT *(c,h2) HAS_TYPE integrable2
integrable2_opp: JUDGEMENT -(h2) HAS_TYPE integrable2
integrable2_diff: JUDGEMENT -(g2,h2) HAS_TYPE integrable2
null_integrable1(h1):[null_set[T1,S1,mu],integrable[T1,S1,mu]]
= choose({(N1,f) | FORALL x: NOT member(x,N1) =>
integrable?(lambda y: h1(x,y)) AND
integral(lambda y: h1(x,y)) = f(x)})
null_integrable2(h2):[null_set[T2,S2,nu],integrable[T2,S2,nu]]
= choose({(N2,g) | FORALL y: NOT member(y,N2) =>
integrable?(lambda x: h2(x,y)) AND
integral(lambda x: h2(x,y)) = g(y)})
null_integral1_def: LEMMA
(N1,f) = null_integrable1(h1) AND
(NOT member(x,N1)) =>
(integrable?(lambda y: h1(x,y)) AND
integral(lambda y: h1(x,y)) = f(x))
null_integral2_def: LEMMA
(N2,g) = null_integrable2(h2) AND
(NOT member(y,N2)) =>
(integrable?(lambda x: h2(x,y)) AND
integral(lambda x: h2(x,y)) = g(y))
integral1(h1): integrable[T1,S1,mu]
= lambda x: LET (N1,f) = null_integrable1(h1) IN
IF member(x,N1) THEN 0 ELSE f(x) ENDIF
integral2(h2): integrable[T2,S2,nu]
= lambda y: LET (N2,g) = null_integrable2(h2) IN
IF member(y,N2) THEN 0 ELSE g(y) ENDIF
integral1_zero: LEMMA integral1(lambda x,y: 0) = lambda x: 0
integral1_add: LEMMA ae_eq?(integral1(g1+h1), integral1(g1) + integral1(h1))
integral1_scal: LEMMA ae_eq?(integral1(c*h1), c*integral1(h1))
integral1_opp: LEMMA ae_eq?(integral1(-(h1)), -integral1(h1))
integral1_diff: LEMMA ae_eq?(integral1(g1-h1), integral1(g1) - integral1(h1))
integral2_zero: LEMMA integral2(lambda x,y: 0) = lambda y: 0
integral2_add: LEMMA ae_eq?(integral2(g2+h2), integral2(g2) + integral2(h2))
integral2_scal: LEMMA ae_eq?(integral2(c*h2), c*integral2(h2))
integral2_opp: LEMMA ae_eq?(integral2(-(h2)), -integral2(h2))
integral2_diff: LEMMA ae_eq?(integral2(g2-h2), integral2(g2) - integral2(h2))
END product_integral_def
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.2Angebot
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
|
