|
series_lems: THEORY
%------------------------------------------------------------------------------
% Extra properties of series. To be added to series@series
%
% Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING series,
orders@well_nat % proof only
i: VAR int
n,m,N: VAR nat
pn: VAR posnat
x,l1,l2,c: VAR real
nnx: VAR nnreal
a,b: VAR sequence[real]
nna: VAR sequence[nnreal]
phi: VAR (bijective?[nat,nat])
zero_tail_series_conv: LEMMA (FORALL m: n < m => a(m) = 0) =>
convergent?(series(a))
zero_tail_series_limit: LEMMA (FORALL m: n < m => a(m) = 0) =>
limit(series(a)) = series(a)(n)
zero_tail_series: LEMMA (FORALL m: n < m => a(m) = 0) =>
convergence(series(a), series(a)(n))
single_nz_series_conv: LEMMA (FORALL m: n /= m => a(m) = 0) =>
convergent?(series(a))
single_nz_series_limit: LEMMA (FORALL m: n /= m => a(m) = 0) =>
limit(series(a)) = a(n)
single_nz_series: LEMMA (FORALL m: n /= m => a(m) = 0) =>
convergence(series(a), a(n))
limit_nonneg: LEMMA convergent?(nna) => limit(nna) >= 0
convergence_nonneg: LEMMA convergence(series(nna),nnx) =>
FORALL n: series(nna)(n) <= nnx
nonneg_series_bij: LEMMA convergence(series(nna),nnx) =>
convergence(series(nna o phi),nnx)
nonneg_series_bij_conv: LEMMA convergent?(series(nna)) =>
convergent?(series(nna o phi))
nonneg_series_bij_limit:LEMMA convergent?(series(nna)) =>
limit(series(nna)) = limit(series(nna o phi))
abs_series_bij: LEMMA convergent?(series(abs(a))) AND
convergence(series(a),x) =>
convergence(series(a o phi),x)
abs_series_bij_conv: LEMMA convergent?(series(abs(a))) =>
convergent?(series(a o phi))
abs_series_bij_limit: LEMMA convergent?(series(abs(a))) =>
limit(series(a)) = limit(series(a o phi))
END series_lems
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
