Suchen Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Haftungshinweis

Bemerkung: zur Agenda Produktseite wechseln Projekt Beratung

Suchen Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 28.9.2014 mit Größe 5 kB

Quelle convergence_sequences.pvs Sprache: 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

quality95%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.