Quellcode-Bibliothek double_nn_sequence.pvs   Sprache: unbekannt

%-------------------------------------------------------------------------
% 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