helm/software/matita/contribs/dama/dama_didactic/sequences.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "reals.ma".
  18
  19 axiom continuo: (R → R) → Prop.
  20 axiom tends_to: (nat → R) → R → Prop.
  21 axiom tends_to_inf: (nat → R) → Prop.
  22
  23 definition monotone_not_increasing ≝
  24  λ alpha:nat→R.
  25  ∀n:nat.alpha (S n) ≤ alpha n.
  26
  27 definition inf_bounded ≝
  28  λ alpha:nat → R.
  29  ∃ m. ∀ n:nat. m ≤ alpha n.
  30
  31 axiom converge: ∀ alpha.
  32  monotone_not_increasing alpha →
  33  inf_bounded alpha →
  34  ∃ l. tends_to alpha l.
  35
  36 definition punto_fisso :=
  37  λ F:R→R. λ x. x = F x.
  38
  39 let rec successione F x (n:nat) on n : R ≝
  40  match n with
  41   [ O ⇒ x
  42   | S n ⇒ F (successione F x n)
  43   ].
  44
  45 axiom lim_punto_fisso:
  46 ∀ F: R → R. ∀b:R. continuo F →
  47  let alpha := successione F b in
  48   ∀ l. tends_to alpha l →
  49     punto_fisso F l.
  50
  51 definition monotone_not_decreasing ≝
  52  λ alpha:nat→R.
  53  ∀n:nat.alpha n ≤ alpha (S n).
  54
  55 definition sup_bounded ≝
  56  λ alpha:nat → R.
  57  ∃ m. ∀ n:nat. alpha n ≤ m.