|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Definition and properties of %
% convergent sequences of reals %
% -> limit of a sequence, %
% -> point of accumulation %
% -> cauchy criterion %
% -> Bolzano-Weierstrass theorem %
% -> completeness of the reals %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
convergence_sequences : THEORY
BEGIN
IMPORTING sequence_props, reals@abs_lems, monotone_subsequence
u, u1, u2 : VAR sequence[real]
l, l1, l2 : VAR real
a, b, c, x : VAR real
epsilon : VAR posreal
i, j, n, m : VAR nat
%--------------------
% Convergence to l
%--------------------
convergence(u, l) : bool =
FORALL epsilon : EXISTS n :
FORALL i : i >= n IMPLIES abs(u(i) - l) < epsilon
%-------------------------
% Point of accumulation
%-------------------------
accumulation(u, a) : bool =
FORALL epsilon, n : EXISTS i : i >= n AND abs(u(i) - a) < epsilon
%--------------------
% Cauchy sequence
%--------------------
cauchy(u) : bool =
FORALL epsilon : EXISTS n :
FORALL i, j : i >= n AND j >= n IMPLIES abs(u(i) - u(j)) < epsilon
%-----------------------
% The limit is unique
%-----------------------
unique_limit : LEMMA
convergence(u, l1) AND convergence(u, l2) IMPLIES l1 = l2
%---------------------------------
% Limit of convergent sequences
%---------------------------------
convergent?(u) : bool = EXISTS l : convergence(u, l)
convergent_seq?(u): MACRO bool = convergent?(u)
v : VAR (convergent?)
limit(v) : real = epsilon(LAMBDA l : convergence(v, l))
limit_lemma : LEMMA convergence(v, limit(v))
limit_def : LEMMA limit(v) = l IFF convergence(v, l)
%--------------------------------------------------------
% A subsequence of a convergent sequence is convergent
%--------------------------------------------------------
convergence_subsequence : LEMMA
convergence(u1, l) AND subseq(u2, u1) IMPLIES convergence(u2, l)
%----------------------------------------
% The limit is a point of accumulation
%----------------------------------------
limit_accumulation : LEMMA
convergence(u, l) IMPLIES accumulation(u, l)
%------------------------------------------------------------------
% a is a point of accumulation iff a sub-sequence converges to a
%------------------------------------------------------------------
%--- extraction ---%
g(u, a)(n) : RECURSIVE nat =
IF n = 0 THEN 0
ELSE epsilon! i : g(u, a)(n - 1) < i AND abs(u(i) - a) < 1/n
ENDIF
MEASURE n
%--- property of g when a is an accumulation point of a ---%
g_prop : LEMMA accumulation(u, a) IMPLIES
FORALL n : g(u, a)(n) < g(u, a)(n+1) AND abs(u(g(u, a)(n + 1)) - a) < 1/(n + 1)
g_increasing : COROLLARY
accumulation(u, a) IMPLIES strict_increasing?(g(u, a))
g_convergence : COROLLARY
accumulation(u, a) IMPLIES FORALL n : abs(u(g(u, a)(n + 1)) - a) < 1/(n + 1)
%--- main theorem ---%
accumulation_subsequence : THEOREM
accumulation(u, a) IFF EXISTS u1 : subseq(u1, u) AND convergence(u1, a)
%-------------------------------------------------------------
% a point of accumulation of a Cauchy sequence is its limit
%-------------------------------------------------------------
cauchy_accumulation : THEOREM
cauchy(u) AND accumulation(u, a) IMPLIES convergence(u, a)
cauchy_subsequence : COROLLARY
cauchy(u) AND subseq(u1, u) AND convergence(u1, l)
IMPLIES convergence(u, l)
%----------------------------------------------
% Monotone, bounded sequences are convergent
%----------------------------------------------
v1 : VAR { u | bounded_above?(u) }
v2 : VAR { u | bounded_below?(u) }
increasing_bounded_convergence : LEMMA
increasing?(v1) IMPLIES convergence(v1, sup(v1))
decreasing_bounded_convergence : LEMMA
decreasing(v2) IMPLIES convergence(v2, inf(v2))
%--------------------------------------------------
% Bolzano-Weierstrass theorem:
% a bounded sequence has a point of accumulation
%--------------------------------------------------
%--- bounded sequence ---%
w : VAR { u | bounded_above?(u) AND bounded_below?(u) }
%--- Bolzano/Weirstrass theorem ---%
bolzano_weierstrass1 : COROLLARY
EXISTS a : inf(w) <= a AND a <= sup(w) AND accumulation(w, a)
bolzano_weierstrass2 : COROLLARY EXISTS a : accumulation(w, a)
bolzano_weierstrass3 : COROLLARY
EXISTS u : subseq(u, w) AND convergent?(u)
bolzano_weierstrass4 : COROLLARY
(FORALL i : a <= u(i) AND u(i) <= b) IMPLIES
(EXISTS c : a <= c AND c <= b AND accumulation(u, c))
%--------------------------------
% A Cauchy sequence is bounded
%--------------------------------
prefix_bounded1 : LEMMA
EXISTS a : FORALL i : i <= n IMPLIES u(i) <= a
prefix_bounded2 : LEMMA
EXISTS a : FORALL i : i <= n IMPLIES a <= u(i)
cauchy_bounded : LEMMA
cauchy(u) IMPLIES bounded_above?(u) AND bounded_below?(u)
%--------------------------------------------------
% Completeness : a Cauchy sequence is convergent
%--------------------------------------------------
convergence_cauchy1 : LEMMA convergent?(u) IMPLIES cauchy(u)
convergence_cauchy2 : LEMMA cauchy(u) IMPLIES convergent?(u)
convergence_cauchy : THEOREM convergent?(u) IFF cauchy(u)
END convergence_sequences
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
