1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 include "sequences.ma".
20 ESERCIZI SULLE SUCCESSIONI
22 Dimostrare che la successione alpha converge a 0
25 definition F ≝ λ x:R.Rdiv x (S (S O)).
27 definition alpha ≝ successione F R1.
29 axiom cont: continuo F.
31 lemma l1: monotone_not_increasing alpha.
32 we need to prove (monotone_not_increasing alpha)
33 or equivalently (∀n:nat. alpha (S n) ≤ alpha n).
35 we need to prove (alpha (S n) ≤ alpha n)
36 or equivalently (Rdiv (alpha n) (S (S O)) ≤ alpha n).
40 lemma l2: inf_bounded alpha.
41 we need to prove (inf_bounded alpha)
42 or equivalently (∃m. ∀n:nat. m ≤ alpha n).
43 (* da trovare il modo giusto *)
44 cut (∀n:nat.R0 ≤ alpha n).by (ex_intro ? ? R0 Hcut) done.
46 we need to prove (∀n:nat. R0 ≤ alpha n).
48 we proceed by induction on n to prove (R0 ≤ alpha n).
51 the thesis becomes (R0 ≤ alpha O)
52 or equivalently (R0 ≤ R1).
54 (* approssimiamo con questo *)
55 we need to prove (R0 ≤ alpha O)
56 or equivalently (R0 ≤ R1).
59 by induction hypothesis we know (R0 ≤ alpha m) (H).
60 we need to prove (R0 ≤ alpha (S m))
61 or equivalently (R0 ≤ Rdiv (alpha m) (S (S O))).
66 ∀ F: R → R. ∀b:R. continuo F →
67 ∀ l. tends_to (successione F b) l →
70 theorem dimostrazione: tends_to alpha O.
71 let l:R such that (tends_to alpha l) (H).
73 change in match alpha in H with (successione F O).
74 check(xxx' F cont l H).*)
75 (* end auto($Revision: 8612 $) proof: TIME=0.01 SIZE=100 DEPTH=100 *)
76 using (lim_punto_fisso F R1 cont l H) we proved (punto_fisso F l) (H2)
77 that is equivalent to (l = (Rdiv l (S (S O)))).
78 we proved (tends_to alpha l = tends_to alpha O) (H4).
83 (******************************************************************************)
85 (* Dimostrare che la successione alpha2 diverge *)
87 definition F2 ≝ λ x:R. Rmult x x.
89 definition alpha2 ≝ successione F2 (S (S O)).
91 lemma uno: ∀n. alpha2 n ≥ R1.
92 we need to prove (∀n. alpha2 n ≥ R1).
94 we proceed by induction on n to prove (alpha2 n ≥ R1).
96 alias num (instance 0) = "natural number".
97 we need to prove (alpha2 0 ≥ R1)
98 or equivalently ((S (S O)) ≥ R1).
101 by induction hypothesis we know (alpha2 m ≥ R1) (H).
102 we need to prove (alpha2 (S m) ≥ R1)
103 or equivalently (Rmult (alpha2 m) (alpha2 m) ≥ R1).letin xxx := (n ≤ n);
104 we proved (R1 · R1 ≤ alpha2 m · alpha2 m) (H1).
105 we proved (R1 · R1 = R1) (H2).
110 lemma mono1: monotone_not_decreasing alpha2.
111 we need to prove (monotone_not_decreasing alpha2)
112 or equivalently (∀n:nat. alpha2 n ≤ alpha2 (S n)).
114 we need to prove (alpha2 n ≤ alpha2 (S n))
115 or equivalently (alpha2 n ≤ Rmult (alpha2 n) (alpha2 n)).
120 lemma due: ∀n. Relev (alpha2 0) n ≥ R0.
121 we need to prove (∀n. Relev (alpha2 0) n ≥ R0)
122 or equivalently (∀n. Relev (S (S O)) n ≥ R0).
126 lemma tre: ∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n).
127 we need to prove (∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n)).
129 we proceed by induction on n to prove (alpha2 (S n) ≥ Relev (alpha2 0) (S n)).
131 we need to prove (alpha2 1 ≥ Relev (alpha2 0) R1)
132 or equivalently (Rmult R2 R2 ≥ R2).
135 by induction hypothesis we know (alpha2 (S m) ≥ Relev (alpha2 0) (S m)) (H).
136 we need to prove (alpha2 (S (S m)) ≥ Relev (alpha2 0) (S (S m)))
140 theorem dim2: tends_to_inf alpha2.
145 (******************************************************************************)
147 (* Dimostrare che la successione alpha3 converge a 0 *)
149 definition alpha3 ≝ successione F2 (Rdiv (S 0) (S (S 0))).
151 lemma quattro: ∀n. alpha3 n ≤ R1.
153 we need to prove (∀n. alpha3 n ≤ R1).
154 we proceed by induction on n to prove (alpha3 n ≤ R1).
156 we need to prove (alpha3 0 ≤ R1).
159 by induction hypothesis we know (alpha3 m ≤ R1) (H).
160 we need to prove (alpha3 (S m) ≤ R1)
161 or equivalently (Rmult (alpha3 m) (alpha3 m) ≤ R1).
165 lemma mono3: monotone_not_increasing alpha3.
166 we need to prove (monotone_not_increasing alpha3)
167 or equivalently (∀n:nat. alpha (S n) ≤ alpha n).
169 we need to prove (alpha (S n) ≤ alpha n)
170 or equivalently (Rmult (alpha3 n) (alpha3 n) ≤ alpha3 n).
174 lemma bound3: inf_bounded alpha3.
175 we need to prove (inf_bounded alpha3)
176 or equivalently (∃m. ∀n:nat. m ≤ alpha3 n).
177 (* da trovare il modo giusto *)
178 cut (∀n:nat.R0 ≤ alpha3 n).by (ex_intro ? ? R0 Hcut) done.
180 we need to prove (∀n:nat. R0 ≤ alpha3 n).
182 we proceed by induction on n to prove (R0 ≤ alpha3 n).
185 the thesis becomes (R0 ≤ alpha O)
186 or equivalently (R0 ≤ R1).
188 (* approssimiamo con questo *)
189 we need to prove (R0 ≤ alpha3 O)
190 or equivalently (R0 ≤ Rdiv (S 0) (S (S 0))).
193 by induction hypothesis we know (R0 ≤ alpha3 m) (H).
194 we need to prove (R0 ≤ alpha3 (S m))
195 or equivalently (R0 ≤ Rmult (alpha3 m) (alpha3 m)).
199 theorem dim3: tends_to alpha3 O.