|
lim_of_functions [ T : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
% Limit of a functions [T -> real] at a point a %
%
% Author: Bruno Dutertre Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN
IMPORTING convergence_functions
%------------------------------------------------
% Subtype of reals where the limit makes sense
%------------------------------------------------
a, b, l, l1, l2 : VAR real
c : VAR (adh[T](fullset[real]))
f, f1, f2 : VAR [ T -> real]
g : VAR [T -> nzreal]
epsilon, delta : VAR posreal
x : VAR T
%---------------------------------------------------
% Convergence of f at a point a towards a limit l
%---------------------------------------------------
convergence(f, a, l) : bool = convergence(f, fullset[real], a, l)
convergence_def : LEMMA
FORALL f, a, l :
convergence(f, a, l)
IFF
adh[T](fullset[real])(a)
AND FORALL epsilon : EXISTS delta :
FORALL x : abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon
adherence_fullset : LEMMA adh[T](fullset[real])(x)
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_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), c, b)
cv_scal : LEMMA convergence(f, a, l)
IMPLIES convergence(b * f, a, b * l)
cv_neg : LEMMA convergence(f, a, l)
IMPLIES convergence(- f, a, - l)
cv_div : LEMMA convergence(f, a, l1) AND convergence(g, a, l2) AND l2 /= 0
IMPLIES convergence(f / g, a, l1 / l2)
cv_inv : LEMMA convergence(g, a, l) AND l /= 0
IMPLIES convergence(1 / g, a, 1 / l)
cv_identity: LEMMA convergence(I[T], c, c)
cv_abs : LEMMA convergence(abs, c, abs(c))
conv_0_0_abs: LEMMA convergence(f, 0, 0) IFF convergence(abs(f), 0, 0)
%-------------------------
% f is convergent at a
%-------------------------
convergent?(f, a) : bool = EXISTS l : convergence(f, a, l)
% lim(f, (x0 : {a | convergent?(f, a)})) : real =
% choose(LAMBDA l : convergence(f, x0, l))
lim(f, (x0 : {a | convergent?(f, a)})) : {l: real | 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)
lim_e_del: LEMMA convergent?(f, a) IMPLIES
(lim(f, a) = l IFF FORALL (e: posreal): EXISTS (del: posreal): FORALL (x: T):
abs(x-a) < del IMPLIES abs(f(x) - l) < e)
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), c)
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)
convergent_identity : LEMMA convergent?(I[T], c)
%----------------------------
% 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), c) = 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)
lim_identity : LEMMA lim(I[T], c) = c
%--------------------
% Bounds on limits
%--------------------
E : VAR setof[real]
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)
lim_le2 : LEMMA convergent?(f, a) AND adh[T](E)(a) AND
(FORALL x : E(x) IMPLIES f(x) <= b)
IMPLIES lim(f, a) <= b
lim_ge2 : LEMMA convergent?(f, a) AND adh[T](E)(a) AND
(FORALL x : E(x) IMPLIES f(x) >= b)
IMPLIES lim(f, a) >= b
lim_order2 : LEMMA convergent?(f1, a) AND convergent?(f2, a) AND adh[T](E)(a)
AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x))
IMPLIES lim(f1, a) <= lim(f2, a)
AUTO_REWRITE+ adherence_fullset
END lim_of_functions
¤ Dauer der Verarbeitung: 0.0 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.
|
