Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Further_Topology.thy Sprache: PVS

Original von: PVS^©

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Definition and properties of      %
%  convergent sequences of reals     %
%  -> limit of a sequence,           %
%  -> point of accumulation          %
%  -> cauchy criterion      %
%  -> Bolzano-Weierstrass theorem    %
%  -> completeness of the reals      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

convergence_sequences : THEORY

  BEGIN

  IMPORTING sequence_props, reals@abs_lems,  monotone_subsequence

  u, u1, u2 : VAR sequence[real]

  l, l1, l2 : VAR real

  a, b, c, x : VAR real

  epsilon : VAR posreal

  i, j, n, m : VAR nat

  %--------------------
  %  Convergence to l
  %--------------------

  convergence(u, l) : bool =
FORALL epsilon : EXISTS n :
     FORALL i : i >= n IMPLIES abs(u(i) - l) < epsilon

  %-------------------------
  %  Point of accumulation
  %-------------------------

  accumulation(u, a) : bool =
FORALL epsilon, n : EXISTS i : i >= n AND abs(u(i) - a) < epsilon

  %--------------------
  %  Cauchy sequence
  %--------------------

  cauchy(u) : bool =
FORALL epsilon : EXISTS n :
     FORALL i, j : i >= n AND j >= n IMPLIES abs(u(i) - u(j)) < epsilon

  %-----------------------
  %  The limit is unique
  %-----------------------

  unique_limit : LEMMA
convergence(u, l1) AND convergence(u, l2) IMPLIES l1 = l2

  %---------------------------------
  %  Limit of convergent sequences
  %---------------------------------

  convergent?(u) : bool = EXISTS l : convergence(u, l)

  convergent_seq?(u): MACRO bool = convergent?(u)

  v : VAR (convergent?)

  limit(v) : real = epsilon(LAMBDA l : convergence(v, l))

  limit_lemma : LEMMA convergence(v, limit(v))

  limit_def : LEMMA  limit(v) = l IFF convergence(v, l)

  %--------------------------------------------------------
  %  A subsequence of a convergent sequence is convergent
  %--------------------------------------------------------

  convergence_subsequence : LEMMA
convergence(u1, l) AND subseq(u2, u1) IMPLIES convergence(u2, l)



  %----------------------------------------
  %  The limit is a point of accumulation
  %----------------------------------------

  limit_accumulation : LEMMA
convergence(u, l) IMPLIES accumulation(u, l)

  %------------------------------------------------------------------
  %  a is a point of accumulation iff a sub-sequence converges to a
  %------------------------------------------------------------------

  %--- extraction ---%

  g(u, a)(n) : RECURSIVE nat =
IF n = 0 THEN 0
ELSE  epsilon! i : g(u, a)(n - 1) < i AND abs(u(i) - a) < 1/n
ENDIF
      MEASURE n

  %--- property of g when a is an accumulation point of a ---%

  g_prop : LEMMA accumulation(u, a) IMPLIES
FORALL n : g(u, a)(n) < g(u, a)(n+1) AND abs(u(g(u, a)(n + 1)) - a) < 1/(n + 1)

  g_increasing : COROLLARY
accumulation(u, a) IMPLIES strict_increasing?(g(u, a))

  g_convergence : COROLLARY
accumulation(u, a) IMPLIES FORALL n : abs(u(g(u, a)(n + 1)) - a) < 1/(n + 1)

  %--- main theorem ---%

  accumulation_subsequence : THEOREM
accumulation(u, a) IFF EXISTS u1 : subseq(u1, u) AND convergence(u1, a)

  %-------------------------------------------------------------
  %  a point of accumulation of a Cauchy sequence is its limit
  %-------------------------------------------------------------

  cauchy_accumulation : THEOREM
cauchy(u) AND accumulation(u, a) IMPLIES convergence(u, a)

  cauchy_subsequence : COROLLARY
cauchy(u) AND subseq(u1, u) AND convergence(u1, l)
     IMPLIES convergence(u, l)

  %----------------------------------------------
  %  Monotone, bounded sequences are convergent
  %----------------------------------------------

  v1 : VAR { u | bounded_above?(u) }

  v2 : VAR { u | bounded_below?(u) }

  increasing_bounded_convergence : LEMMA
increasing?(v1) IMPLIES convergence(v1, sup(v1))

  decreasing_bounded_convergence : LEMMA
decreasing(v2) IMPLIES convergence(v2, inf(v2))

  %--------------------------------------------------
  %  Bolzano-Weierstrass theorem:
  %  a bounded sequence has a point of accumulation
  %--------------------------------------------------

  %--- bounded sequence ---%

  w : VAR { u | bounded_above?(u) AND bounded_below?(u) }


  %--- Bolzano/Weirstrass theorem ---%

  bolzano_weierstrass1 : COROLLARY
EXISTS a : inf(w) <= a AND a <= sup(w) AND accumulation(w, a)

  bolzano_weierstrass2 : COROLLARY  EXISTS a : accumulation(w, a)

  bolzano_weierstrass3 : COROLLARY
EXISTS u : subseq(u, w) AND convergent?(u)

  bolzano_weierstrass4 : COROLLARY
(FORALL i : a <= u(i) AND u(i) <= b) IMPLIES
     (EXISTS c : a <= c AND c <= b AND accumulation(u, c))

  %--------------------------------
  %  A Cauchy sequence is bounded
  %--------------------------------

  prefix_bounded1 : LEMMA
EXISTS a : FORALL i : i <= n IMPLIES u(i) <= a

  prefix_bounded2 : LEMMA
EXISTS a : FORALL i : i <= n IMPLIES a <= u(i)

  cauchy_bounded : LEMMA
cauchy(u) IMPLIES bounded_above?(u) AND bounded_below?(u)

  %--------------------------------------------------
  %  Completeness : a Cauchy sequence is convergent
  %--------------------------------------------------

  convergence_cauchy1 : LEMMA convergent?(u) IMPLIES cauchy(u)

  convergence_cauchy2 : LEMMA cauchy(u) IMPLIES convergent?(u)

  convergence_cauchy : THEOREM  convergent?(u) IFF cauchy(u)

  END convergence_sequences

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.