|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% General convergence of functions [T -> real] %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
convergence_functions [T : TYPE FROM real] : THEORY
BEGIN
IMPORTING reals@real_fun_ops, epsilon_lemmas
epsilon, delta : VAR posreal
e, e1, e2 : VAR posreal
E, E1, E2 : VAR setof[real]
f, f1, f2 : VAR [T -> real]
g : VAR [T -> nzreal]
l, l1, l2, a, b, z : VAR real
x, y : VAR T
%---------------------------
% Reals adherent to a set
%---------------------------
adh(E) : setof[real] =
{ z | FORALL e : EXISTS x : E(x) AND abs(x - z) < e }
member_adherent : LEMMA E(x) IMPLIES adh(E)(x)
adherence_subset1 : LEMMA
subset?(E1, E2) AND adh(E1)(z) IMPLIES adh(E2)(z)
adherence_subset2 : LEMMA
subset?(E1, E2) IMPLIES subset?(adh(E1), adh(E2))
adherence_prop1 : LEMMA
FORALL e, E, (a : (adh(E))) :
EXISTS x : E(x) AND abs(x - a) < e
adherence_prop2 : LEMMA
FORALL e1, e2, E, (a : (adh(E))) :
EXISTS x : E(x) AND abs(x - a) < e1 AND abs(x - a) < e2
%------------------------------------------------------
% Definition of convergence and immediate properties
%------------------------------------------------------
convergence(f, E, a, l) : bool =
adh(E)(a) AND
FORALL epsilon : EXISTS delta :
FORALL x : E(x) AND abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon
convergence_unicity : LEMMA
FORALL E, f, a, l1, l2 :
convergence(f, E, a, l1) AND convergence(f, E, a, l2)
IMPLIES l1 = l2
subset_convergence : LEMMA
subset?(E1, E2) IMPLIES
FORALL f, (a : (adh(E1))), l :
convergence(f, E2, a, l) IMPLIES convergence(f, E1, a, l)
subset_convergence2 : LEMMA
FORALL E1, E2, f, (a : (adh(E1))), l :
subset?(E1, E2) AND convergence(f, E2, a, l)
IMPLIES convergence(f, E1, a, l)
convergence_in_domain : LEMMA
FORALL f, x, l : E(x) AND convergence(f, E, x, l) IMPLIES l = f(x)
%----------------------------------
% Limits and function operations
%----------------------------------
convergence_sum : LEMMA
FORALL E, f1, f2, a, l1, l2 :
convergence(f1, E, a, l1)
AND convergence(f2, E, a, l2)
IMPLIES convergence(f1 + f2, E, a, l1 + l2)
convergence_neg : LEMMA
FORALL E, f1, a, l1 :
convergence(f1, E, a, l1)
IMPLIES convergence(- f1, E, a, - l1)
convergence_diff : LEMMA
FORALL E, f1, f2, a, l1, l2 :
convergence(f1, E, a, l1)
AND convergence(f2, E, a, l2)
IMPLIES convergence(f1 - f2, E, a, l1 - l2)
convergence_prod : LEMMA
FORALL E, f1, f2, a, l1, l2 :
convergence(f1, E, a, l1)
AND convergence(f2, E, a, l2)
IMPLIES convergence(f1 * f2, E, a, l1 * l2)
convergence_const : LEMMA
FORALL E, (a : (adh(E))), b : convergence(const_fun(b), E, a, b)
convergence_scal : LEMMA
FORALL E, f1, a, l1, b :
convergence(f1, E, a, l1)
IMPLIES convergence(b * f1, E, a, b * l1)
convergence_inv : LEMMA
FORALL E, g, a, l1:
convergence(g, E, a, l1)
AND l1 /= 0
IMPLIES convergence(1/g, E, a, 1/l1)
convergence_div : LEMMA
FORALL E, f, g, a, l1, l2 :
convergence(f, E, a, l1)
AND convergence(g, E, a, l2)
AND l2 /= 0
IMPLIES convergence(f/g, E, a, l1/l2)
%---------------------
% Identity function
%---------------------
convergence_identity : LEMMA
FORALL E, (a : (adh(E))) : convergence(I[T], E, a, a)
%-----------------------------
% Limit preserve order
%-----------------------------
convergence_order : LEMMA
FORALL E, f1, f2, a, l1, l2 :
convergence(f1, E, a, l1)
AND convergence(f2, E, a, l2)
AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x))
IMPLIES l1 <= l2
%-------------------------------------------
% Bounds on function are bounds on limits
%-------------------------------------------
convergence_lower_bound : COROLLARY
FORALL E, f, b, a, l :
convergence(f, E, a, l)
AND (FORALL x : E(x) IMPLIES b <= f(x))
IMPLIES b <= l
convergence_upper_bound : COROLLARY
FORALL E, f, b, a, l :
convergence(f, E, a, l)
AND (FORALL x : E(x) IMPLIES f(x) <= b)
IMPLIES l <= b
%--------------------------
% Function constant on E
%--------------------------
convergence_locally_constant : LEMMA
FORALL E, f, b, (a : (adh(E))) :
(FORALL x : E(x) IMPLIES f(x) = b)
IMPLIES convergence(f, E, a, b)
%-------------
% Squeezing
%-------------
convergence_squeezing : LEMMA
FORALL f1, f2, f, a, l :
convergence(f1, E, a, l) AND convergence(f2, E, a, l)
AND (FORALL x : E(x) IMPLIES f1(x) <= f(x) AND f(x) <= f2(x))
IMPLIES
convergence(f, E, a, l)
END convergence_functions
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.15Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
