|
limit_vect[n,m:posnat]: THEORY
BEGIN
IMPORTING vectors@vectors,
reals@abs_lems,
analysis@epsilon_lemmas
f, f1, f2: VAR [ Vector[n] -> Vector[m] ]
a,b,x,v : VAR Vector[n]
l,l1,l2 : VAR Vector[m]
epsilon, delta : VAR posreal
k : VAR real
;+(f1, f2)(v) : MACRO Vector[m] = f1(v) + f2(v)
;-(f)(v): MACRO Vector[m] = -f(v)
;-(f1, f2)(v) : MACRO Vector[m] = f1(v) - f2(v)
;*(k, f)(v) : MACRO Vector[m] = k*f(v)
;*(f1,f2)(v) : MACRO real = f1(v)*f2(v)
const_fun(l)(x): Vector[m] = l
%---------------------------------------------------
% Convergence of f at a point a towards a limit l
%--------------------------------------------------
convergence(f, a, l): bool =
FORALL epsilon : EXISTS delta :
FORALL v: norm(v-a) < delta
IMPLIES norm(f(v) - l) < epsilon
cv_unique : LEMMA
convergence(f, a, l1) AND convergence(f, a, l2)
IMPLIES l1 = l2
cv_in_domain : LEMMA
convergence(f, a, l)
IMPLIES l = f(a)
%-------------------------------------------
% 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(LAMBDA v: l, a, l)
cv_scal : LEMMA
convergence(f, a, l)
IMPLIES convergence(k*f, a, k*l)
%-------------------------
% f is convergent at a
%-------------------------
convergent?(f, a) : bool = EXISTS l : convergence(f, a, l)
lim(f, (x0 : {a | convergent?(f, a)})) : Vector[m] =
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 convergnce 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(l), a)
scal_fun_convergent : LEMMA convergent?(f, a) IMPLIES convergent?(k * f, 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(l), a) = l
lim_scal_fun : LEMMA convergent?(f, a)
IMPLIES lim(k * f, a) = k * lim(f, a)
END limit_vect
¤ Dauer der Verarbeitung: 0.15 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.
|
