| products/Sources/formale Sprachen/PVS/examples/ (Beweissystem der NASA Version 6.0.9©) Datei vom 6.10.2014 mit Größe 2 kB |
|
SSL double_nn_sequence.pvs
Interaktion und |
|||||||||
|
%-------------------------------------------------------------------------
% 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 ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.13Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤*Eine klare Vorstellung vom Zielzustand |
|
2026-03-28