|
%------------------------------------------------------------------------------
% Metric Convergence Properties
%
% Author: David Lester, Manchester University
%
% Version 1.0 17/08/07 Initial Version
%------------------------------------------------------------------------------
convergence_aux: THEORY
BEGIN
IMPORTING metric_space_def[real,(LAMBDA (x,y:real): abs(x-y))],
metric_space[real,(LAMBDA (x,y:real): abs(x-y))],
reals@bounded_reals[real],
reals@real_fun_ops_aux[nat],
reals@real_fun_preds[nat]
u,v: VAR sequence[real]
x,y: VAR real
n,i: VAR nat
r: VAR posreal
nnc: VAR nnreal
ua: VAR (real_fun_preds.bounded_above?)
ub: VAR (real_fun_preds.bounded_below?)
% bounded_above?(u):bool = bounded_above?(image[nat,real](u,fullset[nat]))
% bounded_below?(u):bool = bounded_below?(image[nat,real](u,fullset[nat]))
bounded_seq?(u) :bool = bounded?(image[nat,real](u,fullset[nat]))
bounded_seq_def: LEMMA bounded_seq?(u) <=>
(bounded_above?(u) AND bounded_below?(u))
upper_bound?(u):[real->bool] = upper_bound?(image[nat,real](u,fullset[nat]))
lower_bound?(u):[real->bool] = lower_bound?(image[nat,real](u,fullset[nat]))
lub(ua):real = lub(image[nat,real](ua,fullset[nat]))
glb(ub):real = glb(image[nat,real](ub,fullset[nat]))
% following should be in real_topology, but is it even needed?
% cauchy_convergent: LEMMA cauchy?(u) <=> metric_convergent?(u)
converges_upto?(u,x):bool = convergence?(u,x) AND increasing?(u)
convergent_upto?(u):bool = EXISTS x: converges_upto?(u,x)
converges_upto_bounded_above: LEMMA converges_upto?(u,x) =>
bounded_above?(u)
converges_upto_le: LEMMA converges_upto?(u,x) => (FORALL n: u(n) <= x)
converges_upto_def: LEMMA
converges_upto?(u,x) <=>
increasing?(u) AND
(FORALL n: u(n) <= x) AND
(FORALL r: EXISTS n: FORALL i: i >= n => x-u(i) < r)
converges_upto_is_lub: LEMMA
converges_upto?(u,x) <=>
(bounded_above?(u) AND increasing?(u) AND
least_upper_bound?(x,image[nat,real](u,fullset[nat])))
bounded_above_is_convergent:
LEMMA bounded_above?(u) AND increasing?(u) => convergent_upto?(u)
converges_upto_add: LEMMA converges_upto?(u,x) AND converges_upto?(v,y)
=> converges_upto?(u+v,x+y)
converges_upto_scal: LEMMA converges_upto?(u,x) =>
converges_upto?(nnc*u,nnc*x)
converges_downto?(u,x):bool = convergence?(u,x) AND decreasing?(u)
convergent_downto?(u):bool = EXISTS x: converges_downto?(u,x)
converges_downto_bounded_below: LEMMA converges_downto?(u,x) =>
bounded_below?(u)
converges_downto_ge: LEMMA converges_downto?(u,x) => FORALL n: x<=u(n)
converges_downto_def: LEMMA
converges_downto?(u,x) <=>
decreasing?(u) AND
(FORALL n: x <= u(n)) AND
(FORALL r: EXISTS n: FORALL i: i >= n => u(i)-x < r)
converges_downto_is_glb: LEMMA
converges_downto?(u,x) <=>
(bounded_below?(u) AND decreasing?(u) AND
greatest_lower_bound?(x,image[nat,real](u,fullset[nat])))
bounded_below_is_convergent:
LEMMA bounded_below?(u) AND decreasing?(u) => convergent_downto?(u)
converges_downto_add: LEMMA converges_downto?(u,x) AND converges_downto?(v,y)
=> converges_downto?(u+v,x+y)
converges_downto_scal:LEMMA converges_downto?(u,x) =>
converges_downto?(nnc*u,nnc*x)
monotonic_converges?(u,x):bool
= convergence?(u,x) AND (increasing?(u) OR decreasing?(u))
monotonic_convergent?(u):bool = EXISTS x: monotonic_converges?(u,x)
END convergence_aux
¤ Dauer der Verarbeitung: 0.0 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.
|
