|
limit_vect_real[n: posnat]: THEORY
BEGIN
IMPORTING vectors@vect_fun_ops[n],
reals@abs_lems,
analysis@epsilon_lemmas
f, f1, f2: VAR [ Vector -> real]
g : VAR [Vector -> nzreal]
epsilon, delta : VAR posreal
a,x,v: VAR Vector
l,l1,l2,b,c,y1,y2: VAR real
%---------------------------------------------------
% Convergence of f at a point a towards a limit l
%---------------------------------------------------
convergence(f, a, l) : bool =
FORALL epsilon : EXISTS delta :
FORALL x: %%% 0 < norm(x-a) AND
norm(x-a) < delta %% AND x in dom(f)
IMPLIES abs(f(x) - l) < epsilon
cv_unique : LEMMA convergence(f, a, l1) AND convergence(f, a, l2)
IMPLIES l1 = l2
cv_in_domain : LEMMA convergence(f, x, l) IMPLIES l = f(x)
%-------------------------------------------
% convergence and operations on functions
%-------------------------------------------
cv_sum : LEMMA convergence(f1, a, l1) AND convergence(f2, a, l2)
IMPLIES convergence(f1 + f2, a, l1 + l2)
cv_neg : LEMMA convergence(f, a, l)
IMPLIES convergence(- f, a, - l)
cv_diff : LEMMA convergence(f1, a, l1) AND convergence(f2, a, l2)
IMPLIES convergence(f1 - f2, a, l1 - l2)
cv_prod : LEMMA convergence(f1, a, l1) AND convergence(f2, a, l2)
IMPLIES convergence(f1 * f2, a, l1 * l2)
cv_const : LEMMA convergence(const_fun(b), v, b)
cv_scal : LEMMA convergence(f, a, l)
IMPLIES convergence(b * f, a, b * l)
cv_inv : LEMMA convergence(g, a, l) AND l /= 0
IMPLIES convergence(1 / g, a, 1 / l)
cv_div : LEMMA convergence(f, a, l1) AND convergence(g, a, l2) AND l2 /= 0
IMPLIES convergence(f / g, a, l1 / l2)
%-------------------------
% f is convergent at a
%-------------------------
convergent?(f, a) : bool = EXISTS l : convergence(f, a, l)
lim(f, (x0 : {a | convergent?(f, a)})) : real =
epsilon(LAMBDA l : convergence(f, x0, l))
lim_fun_lemma : LEMMA FORALL f, (x0 : {a | convergent?(f, a)}) :
convergence(f, x0, lim(f, x0))
lim_fun_def : LEMMA FORALL f, l, (x0 : {a | convergent?(f, a)}) :
lim(f, x0) = l IFF convergence(f, x0, l)
convergence_equiv : LEMMA convergence(f, a, l) IFF
convergent?(f, a) AND lim(f, a) = l
convergent_in_domain : LEMMA convergent?(f, x) IFF convergence(f, x, f(x))
lim_in_domain : LEMMA convergent?(f, x) IMPLIES lim(f, x) = f(x)
%------------------------------------------
% Operations preserving convergence at a
%------------------------------------------
sum_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a)
IMPLIES convergent?(f1 + f2, a)
neg_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(- f, a)
diff_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a)
IMPLIES convergent?(f1 - f2, a)
prod_fun_convergent : LEMMA convergent?(f1, a) AND convergent?(f2, a)
IMPLIES convergent?(f1 * f2, a)
const_fun_convergent: LEMMA convergent?(const_fun(b), v)
scal_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(b * f, a)
inv_fun_convergent : LEMMA convergent?(g, a) AND lim(g, a) /= 0
IMPLIES convergent?(1/g, a)
div_fun_convergent : LEMMA convergent?(f, a) AND convergent?(g, a)
AND lim(g, a) /= 0 IMPLIES convergent?(f / g, a)
%----------------------------
% Same things with lim(a)
%----------------------------
lim_sum_fun : LEMMA convergent?(f1, a) AND convergent?(f2, a)
IMPLIES lim(f1 + f2, a) = lim(f1, a) + lim(f2, a)
lim_neg_fun : LEMMA convergent?(f, a)
IMPLIES lim(- f, a) = - lim(f, a)
lim_diff_fun : LEMMA convergent?(f1, a) AND convergent?(f2, a)
IMPLIES lim(f1 - f2, a) = lim(f1, a) - lim(f2, a)
lim_prod_fun : LEMMA convergent?(f1, a) AND convergent?(f2, a)
IMPLIES lim(f1 * f2, a) = lim(f1, a) * lim(f2, a)
lim_const_fun : LEMMA lim(const_fun(b), v) = b
lim_scal_fun : LEMMA convergent?(f, a)
IMPLIES lim(b * f, a) = b * lim(f, a)
lim_inv_fun : LEMMA convergent?(g, a) AND lim(g, a) /= 0
IMPLIES lim(1/g, a) = 1/lim(g, a)
lim_div_fun : LEMMA convergent?(f, a) AND convergent?(g, a) AND lim(g, a) /= 0
IMPLIES lim(f / g, a) = lim(f, a)/lim(g, a)
%-----------------------------
% Limit preserve order
%-----------------------------
convergence_order : LEMMA
FORALL f1, f2, a, l1, l2 :
convergence(f1, a, l1)
AND convergence(f2, a, l2)
AND (FORALL x : f1(x) <= f2(x))
IMPLIES l1 <= l2
%-------------------------------------------
% Bounds on function are bounds on limits
%-------------------------------------------
convergence_lower_bound : COROLLARY
FORALL f, b, a, l :
convergence(f, a, l)
AND (FORALL x : b <= f(x))
IMPLIES b <= l
convergence_upper_bound : COROLLARY
FORALL f, b, a, l :
convergence(f, a, l)
AND (FORALL x : f(x) <= b)
IMPLIES l <= b
%--------------------
% Bounds on limits
%--------------------
lim_le1 : LEMMA
convergent?(f, a) AND (FORALL x : f(x) <= b) IMPLIES lim(f, a) <= b
lim_ge1 : LEMMA
convergent?(f, a) AND (FORALL x : f(x) >= b) IMPLIES lim(f, a) >= b
lim_order1 : LEMMA convergent?(f1, a) AND convergent?(f2, a)
AND (FORALL x : f1(x) <= f2(x))
IMPLIES lim(f1, a) <= lim(f2, a)
END limit_vect_real
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
