|
limit_real_vect2[ T : TYPE FROM real ]: THEORY
BEGIN
IMPORTING vectors@distance_2D, vect_fun_ops_rv[T],
reals@abs_lems
f, f1, f2: VAR [ T -> Vect2]
g : VAR [T -> Vect2]
e, epsilon, delta : VAR posreal
a,b,x: VAR T
l,l1,l2,b,c,y1,y2,v: VAR Vect2
% const_fun(v) : [T -> Vect2] = LAMBDA x : v ;
% +(f1, f2) : [T -> Vect2] = LAMBDA x : f1(x) + f2(x);
% -(f1) : [T -> Vect2] = LAMBDA x : -f1(x);
% -(f1, f2) : [T -> Vect2] = LAMBDA x : f1(x) - f2(x);
% *(a, f2) : [T -> Vect2] = LAMBDA x : a * f2(x);
%% *(f1, f2) : [real -> Vect2] = (LAMBDA x : f1(x) * f2(x)); %%% ???
%---------------------------------------------------
% Convergence of f at a point a towards a limit l
%---------------------------------------------------
convergence(f, a, l) : bool =
%% (FORALL e: EXISTS x: abs(x - a) < e) AND % a has a ball containing T values
FORALL epsilon : EXISTS delta :
FORALL x: abs(x-a) < delta
IMPLIES norm(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_const : LEMMA convergence(const_vfun(b), a, b)
cv_scal : LEMMA convergence(f, a, l)
IMPLIES convergence(b * f, a, b * l)
%-------------------------
% f is convergent at a
%-------------------------
convergent?(f, a) : bool = EXISTS l : convergence(f, a, l)
lim(f, (x0 : {a | convergent?(f, a)})) : Vect2 =
choose(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)
const_fun_convergent: LEMMA convergent?(const_vfun(b), 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)
% %-----------------------------
% % 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_real_vect2
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
