|
convergence_ops : THEORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Limits and operations on sequences of reals
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
BEGIN
IMPORTING convergence_sequences, epsilon_lemmas
s, s1, s2 : VAR sequence[real]
s3 : VAR sequence[nzreal]
a : VAR real
l, l1, l2 : VAR real
n, m, N : VAR nat
%---------------------------------
% limits of sum, product, etc.
%---------------------------------
cnv_seq_sum : LEMMA
convergence(s1, l1) AND convergence(s2, l2)
IMPLIES convergence(s1 + s2, l1 + l2)
cnv_seq_neg : LEMMA
convergence(s1, l1)
IMPLIES convergence(-s1, -l1)
cnv_seq_diff : LEMMA
convergence(s1, l1) AND convergence(s2, l2)
IMPLIES convergence(s1 - s2, l1 - l2)
cnv_seq_prod : LEMMA
convergence(s1, l1) AND convergence(s2, l2)
IMPLIES convergence(s1 * s2, l1 * l2)
cnv_seq_const : LEMMA convergence(const_fun(a), a)
cnv_seq_scal : LEMMA
convergence(s1, l1) IMPLIES convergence(a * s1, a * l1)
cnv_seq_inv : LEMMA
convergence(s3, l2) AND l2 /= 0
IMPLIES convergence(1 / s3, 1 / l2)
cnv_seq_div : LEMMA
convergence(s1, l1) AND convergence(s3, l2)
AND l2 /= 0
IMPLIES convergence(s1 / s3, l1 / l2)
cnv_seq_abs : LEMMA
convergence(s1, l1) IMPLIES convergence(abs(s1), abs(l1))
cnv_seq_order : LEMMA
convergence(s1, l1) and convergence(s2, l2)
AND (FORALL n : s1(n) <= s2(n))
IMPLIES l1 <= l2
convergence_shift: LEMMA convergence(s,l) IFF
convergence(LAMBDA n: s(n+m),l)
%-------------
% Squeezing
%-------------
squeezing_variant : LEMMA
convergence(s1, l) and convergence(s2, l)
AND (FORALL n : N <= n IMPLIES s1(n) <= s(n) and s(n) <= s2(n))
IMPLIES convergence(s, l)
squeezing_const1 : LEMMA
convergence(s1, l)
AND (FORALL n : N <= n IMPLIES l <= s(n) AND s(n) <= s1(n))
IMPLIES convergence(s, l)
squeezing_const2 : LEMMA
convergence(s1, l)
AND (FORALL n : N <= n IMPLIES s1(n) <= s(n) AND s(n) <= l)
IMPLIES convergence(s, l)
squeezing : LEMMA
convergence(s1, l) and convergence(s2, l)
AND (FORALL n : s1(n) <= s(n) and s(n) <= s2(n))
IMPLIES convergence(s, l)
squeezing_gen : LEMMA
convergence(s1, l) and convergence(s2, l)
AND (FORALL n : n >= N IMPLIES s1(n) <= s(n) and s(n) <= s2(n))
IMPLIES convergence(s, l)
abs_convergence : COROLLARY
convergence(s, 0) IFF convergence(abs(s), 0)
%----------------------------------
% Same properties with convergent
%----------------------------------
convergent_sum : LEMMA
convergent?(s1) AND convergent?(s2) IMPLIES convergent?(s1 + s2)
convergent_neg : LEMMA
convergent?(s1) IMPLIES convergent?(-s1)
convergent_diff : LEMMA
convergent?(s1) AND convergent?(s2) IMPLIES convergent?(s1 - s2)
convergent_prod : LEMMA
convergent?(s1) AND convergent?(s2) IMPLIES convergent?(s1 * s2)
convergent_const : LEMMA convergent?(const_fun(a))
convergent_scal : LEMMA
convergent?(s1) IMPLIES convergent?(a * s1)
convergent_inv : LEMMA
convergent?(s3) AND limit(s3) /= 0 IMPLIES convergent?(1 / s3)
convergent_div : LEMMA
convergent?(s1) AND convergent?(s3) AND limit(s3) /= 0
IMPLIES convergent?(s1 / s3)
convergent_abs : LEMMA
convergent?(s1) IMPLIES convergent?(abs(s1))
squeezing_abs_0 : LEMMA % BUTLER
convergence(s1, 0)
AND (FORALL n : abs(s(n)) <= s1(n))
IMPLIES convergence(s, 0)
squeezing_abs_0_gen : LEMMA % BUTLER
(convergence(s1, 0)
AND (EXISTS N: (FORALL n : n >= N IMPLIES abs(s(n)) <= s1(n))))
IMPLIES convergence(s, 0)
%---------------------------------
% Types of convergent sequences
%---------------------------------
v1, v2 : VAR (convergent?)
u : VAR { s3 | convergent?(s3) }
convergent_nz?(u) : bool = limit(u) /= 0
v3 : VAR (convergent_nz?)
%--------------
% Judgements
%--------------
constant_seq1: JUDGEMENT const_fun(a) HAS_TYPE (convergent?)
constant_seq2: JUDGEMENT const_fun(b: nzreal) HAS_TYPE (convergent_nz?)
conv_seq_plus: JUDGEMENT +(v1, v2) HAS_TYPE (convergent?)
conv_seq_minus: JUDGEMENT -(v1, v2) HAS_TYPE (convergent?)
conv_seq_times: JUDGEMENT *(v1, v2) HAS_TYPE (convergent?)
conv_seq_scal: JUDGEMENT *(a, v1) HAS_TYPE (convergent?)
conv_seq_neg: JUDGEMENT -(v1) HAS_TYPE (convergent?)
conv_seq_abs: JUDGEMENT abs(v1) HAS_TYPE (convergent?)
conv_seq_div1: JUDGEMENT /(v1, v3) HAS_TYPE (convergent?)
conv_seq_div2: JUDGEMENT /(a, v3) HAS_TYPE (convergent?)
%-----------------------------
% Combinations of sequences
%-----------------------------
limit_sum : LEMMA limit(v1 + v2) = limit(v1) + limit(v2)
limit_neg : LEMMA limit(- v1) = - limit(v1)
limit_diff : LEMMA limit(v1 - v2) = limit(v1) - limit(v2)
limit_prod : LEMMA limit(v1 * v2) = limit(v1) * limit(v2)
limit_inv : LEMMA limit(1 / v3) = 1 / limit(v3)
limit_div : LEMMA limit(v1 / v3) = limit(v1) / limit(v3)
limit_const : LEMMA limit(const_fun(a)) = a
limit_scal : LEMMA limit(a * v1) = a * limit(v1)
limit_abs : LEMMA limit(abs(v1)) = abs(limit(v1))
%---------------------------------------------------
% Expansion of convergence (for computing limits)
%---------------------------------------------------
limit_equiv : LEMMA
convergence(s, l) IFF convergent?(s) AND limit(s) = l
limit_order : PROPOSITION
convergence(s1, l1) AND convergence(s2, l2)
AND (FORALL n : s1(n) <= s2(n))
=> l1 <= l2
%----------------------------------------------------------------------------
% NOTE: See "convergence_special" in lnexp library for convergence of
% sequences involving x^a where a is real
%
% NOTE: See "series" in series library for convergence of |x|^n and x^n
%----------------------------------------------------------------------------
END convergence_ops
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
