|
%-------------------------------------------------------------------------
% Convergence properties of doubly-indexed sequences of nnreals
%
% Author: David Lester, Manchester University
%
% Version 1.0 04/05/09 Initial (DRL)
%-------------------------------------------------------------------------
double_nn_sequence: THEORY
BEGIN
IMPORTING analysis@real_fun_supinf[nnreal],
double_index[nnreal],
series@series_aux,
sigma_set@absconv_series_aux
u: VAR [[nat,nat]->nnreal]
v: VAR [nat->nnreal]
l: VAR nnreal
i,j,n: VAR nat
z: VAR real
nn_series_increasing: LEMMA increasing?(series(v))
nn_index_scaf1: LEMMA
series(single_index(u))(double_index_n(0,n)) =
sigma(0, n, LAMBDA i: sigma(0,n-i,lambda j: u(i,j)))
nn_double_index_incr: LEMMA double_index_n(i,j) = double_index_n(0,i+j)-i
nn_index_scaf2: LEMMA
sigma(0,n, LAMBDA i: sigma(0,n,lambda j: u(i,j))) <=
series(single_index(u))(double_index_n(0,2*n))
nn_index_scaf3: LEMMA EXISTS n:
sigma(0,i, LAMBDA i: sigma(0,j,lambda j: u(i,j))) <=
series(single_index(u))(n)
nn_index_scaf4: LEMMA EXISTS i,j:
series(single_index(u))(n) <=
sigma(0,i, LAMBDA i: sigma(0,j,lambda j: u(i,j)))
nn_convegent_bounded: LEMMA convergent?(series(v)) <=>
bounded_above?(Im(series(v)))
nn_limit_lub: LEMMA convergent?(series(v)) =>
limit(series(v)) = lub(Im(series(v)))
nn_convergence_least_upper_bound: LEMMA increasing?(v) =>
(convergence(v,l) <=> least_upper_bound?(l,Im(v)))
double_series: LEMMA
series(LAMBDA i: series(LAMBDA j: u(i,j))(j))(i) =
series(LAMBDA j: series(lambda i: u(i,j))(i))(j)
double_subseq_convergent: LEMMA convergent?(series(single_index(u))) =>
convergent?(series(LAMBDA j: u(i,j)))
double_subseq_bounded: LEMMA
bounded_above?(Im(series(single_index(u)))) =>
bounded_above?(Im(series(LAMBDA j: u(i,j))))
series_limit_def: LEMMA
(FORALL i: convergent?(LAMBDA j: u(i,j))) =>
series(lambda i: limit(lambda j: u(i,j)))(i) =
limit(lambda j: series(lambda i: u(i,j))(i))
double_approx: LEMMA
(FORALL i: convergent?(series(LAMBDA j: u(i,j)))) =>
series(lambda i: limit(series(lambda j: u(i,j))))(i)
= limit(series(lambda j: series(lambda i: u(i,j))(i)))
double_approx1: LEMMA convergence(series(single_index(u)),l) <=>
least_upper_bound?(l,{z | exists i,j:
series(lambda j: series(lambda i: u(i,j))(i))(j) =z})
double_approx2: LEMMA (FORALL i: convergent?(series(LAMBDA j: u(i,j)))) =>
(convergence(series(lambda i: limit(series(lambda j: u(i,j)))),l) <=>
least_upper_bound?(l,{z | exists i,j:
series(lambda j: series(lambda i: u(i,j))(i))(j) =z}))
double_left_convergence: LEMMA
convergence(series(single_index(u)),l) <=>
(FORALL i: convergent?(series(LAMBDA j: u(i,j)))) AND
convergence(series(lambda i: limit(series(lambda j: u(i,j)))),l)
double_left_convergent: LEMMA
convergent?(series(single_index(u))) <=>
(FORALL i: convergent?(series(LAMBDA j: u(i,j)))) AND
convergent?(series(lambda i: limit(series(lambda j: u(i,j)))))
double_left_limit: LEMMA convergent?(series(single_index(u))) =>
limit(series(single_index(u)))
= limit(series(lambda i: limit(series(lambda j: u(i,j)))))
double_right_convergence: LEMMA
convergence(series(single_index(u)),l) <=>
convergence(series(single_index(lambda j,i: u(i,j))),l)
double_right_convergent: LEMMA
convergent?(series(single_index(u))) <=>
convergent?(series(single_index(lambda j,i: u(i,j))))
double_right_limit: LEMMA convergent?(series(single_index(u))) =>
limit(series(single_index(u)))
= limit(series(single_index(lambda j,i: u(i,j))))
END double_nn_sequence
¤ Dauer der Verarbeitung: 0.13 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.
|
