seqScript.sml
1(*===========================================================================*)
2(* Theory of sequences and series of real numbers *)
3(*===========================================================================*)
4Theory seq
5Ancestors
6 pair arithmetic num prim_rec real metric nets combin pred_set
7 iterate real_sigma real_topology
8Libs
9 numLib reduceLib pairLib jrhUtils realSimps BasicProvers
10 res_quanTools realSimps realLib hurdUtils
11
12
13val _ = ParseExtras.temp_loose_equality()
14
15val num_EQ_CONV = Arithconv.NEQ_CONV;
16val EXACT_CONV = jrhUtils.EXACT_CONV; (* conflict with hurdUtils.EXACT_CONV *)
17val assert = Lib.assert; (* conflict with hurdUtils.assert *)
18
19val _ = add_implicit_rewrites pairLib.pair_rws;
20
21val S_TAC = rpt (POP_ASSUM MP_TAC) >> rpt RESQ_STRIP_TAC;
22val Strip = S_TAC;
23
24(*---------------------------------------------------------------------------*)
25(* Specialize net theorems to sequences:num->real *)
26(*---------------------------------------------------------------------------*)
27
28val geq = Term `$>= : num->num->bool`;
29
30Definition tends_num_real :
31 tends_num_real x x0 = (x tends x0)(mtop(mr1), ^geq)
32End
33Overload "-->" = “tends_num_real”
34
35Theorem SEQ:
36 !x x0.
37 (x --> x0) =
38 !e. &0 < e
39 ==> ?N. !n. n >= N ==> abs(x(n) - x0) < e
40Proof
41 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real, SEQ_TENDS, MR1_DEF] THEN
42 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ABS_SUB]
43 THEN REFL_TAC
44QED
45
46(* connection to real_topologyTheory *)
47Theorem LIM_SEQUENTIALLY_SEQ :
48 !s l. (s --> l) sequentially <=> (s --> l)
49Proof
50 REWRITE_TAC [LIM_SEQUENTIALLY, SEQ, GREATER_EQ, dist]
51QED
52
53Theorem SEQ_CONST:
54 !k. (\x. k) --> k
55Proof
56 REPEAT GEN_TAC THEN REWRITE_TAC[SEQ, REAL_SUB_REFL, ABS_0] THEN
57 GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
58QED
59
60Theorem SEQ_ADD:
61 !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x(n) + y(n)) --> (x0 + y0)
62Proof
63 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN
64 MATCH_MP_TAC NET_ADD THEN MATCH_ACCEPT_TAC DORDER_NGE
65QED
66
67Theorem SEQ_MUL:
68 !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x(n) * y(n)) --> (x0 * y0)
69Proof
70 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN
71 MATCH_MP_TAC NET_MUL THEN MATCH_ACCEPT_TAC DORDER_NGE
72QED
73
74Theorem SEQ_NEG:
75 !x x0. x --> x0 = (\n. ~(x n)) --> ~x0
76Proof
77 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN
78 MATCH_MP_TAC NET_NEG THEN MATCH_ACCEPT_TAC DORDER_NGE
79QED
80
81Theorem SEQ_INV:
82 !x x0. x --> x0 /\ ~(x0 = &0) ==> (\n. inv(x n)) --> inv x0
83Proof
84 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN
85 MATCH_MP_TAC NET_INV THEN MATCH_ACCEPT_TAC DORDER_NGE
86QED
87
88Theorem SEQ_SUB:
89 !x x0 y y0. x --> x0 /\ y --> y0 ==> (\n. x(n) - y(n)) --> (x0 - y0)
90Proof
91 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN
92 MATCH_MP_TAC NET_SUB THEN MATCH_ACCEPT_TAC DORDER_NGE
93QED
94
95Theorem SEQ_DIV:
96 !x x0 y y0. x --> x0 /\ y --> y0 /\ ~(y0 = &0) ==>
97 (\n. x(n) / y(n)) --> (x0 / y0)
98Proof
99 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN
100 MATCH_MP_TAC NET_DIV THEN MATCH_ACCEPT_TAC DORDER_NGE
101QED
102
103Theorem SEQ_UNIQ:
104 !x x1 x2. x --> x1 /\ x --> x2 ==> (x1 = x2)
105Proof
106 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN
107 MATCH_MP_TAC MTOP_TENDS_UNIQ THEN
108 MATCH_ACCEPT_TAC DORDER_NGE
109QED
110
111(*---------------------------------------------------------------------------*)
112(* Define convergence and Cauchy-ness *)
113(*---------------------------------------------------------------------------*)
114
115Definition convergent[nocompute]:
116 convergent f = ?l. f --> l
117End
118
119(* already defined in real_topologyTheory *)
120Theorem cauchy :
121 !f. cauchy f <=>
122 !e. &0 < e ==> ?N:num. !m n. m >= N /\ n >= N ==> abs(f(m) - f(n)) < e
123Proof
124 rw [cauchy_def, dist]
125QED
126
127Definition lim :
128 limseq f = @l. f --> l
129End
130Overload lim = “limseq”
131
132(* connection to real_topologyTheory *)
133Theorem LIM_SEQUENTIALLY_SEQ' :
134 !f. lim sequentially f = lim f
135Proof
136 REWRITE_TAC [LIM_SEQUENTIALLY_SEQ, reallim, lim]
137QED
138
139Theorem SEQ_LIM :
140 !f. convergent f <=> f --> lim f
141Proof
142 GEN_TAC THEN REWRITE_TAC[convergent] THEN EQ_TAC THENL
143 [DISCH_THEN(MP_TAC o SELECT_RULE) THEN REWRITE_TAC[lim],
144 DISCH_TAC THEN EXISTS_TAC “lim f” THEN POP_ASSUM ACCEPT_TAC]
145QED
146
147(*---------------------------------------------------------------------------*)
148(* Define a subsequence *)
149(*---------------------------------------------------------------------------*)
150
151Definition subseq[nocompute]:
152 subseq f = !m n:num. m < n ==> f m < (f n):num
153End
154
155Theorem SUBSEQ_SUC:
156 !f. subseq f = !n. f(n) < f(SUC n)
157Proof
158 GEN_TAC THEN REWRITE_TAC[subseq] THEN EQ_TAC THEN DISCH_TAC THENL
159 [X_GEN_TAC “n:num” THEN POP_ASSUM MATCH_MP_TAC THEN
160 REWRITE_TAC[LESS_SUC_REFL],
161 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP LESS_ADD_1) THEN
162 REWRITE_TAC[GSYM ADD1] THEN
163 DISCH_THEN(X_CHOOSE_THEN “p:num” SUBST1_TAC) THEN
164 SPEC_TAC(“p:num”,“p:num”) THEN INDUCT_TAC THENL
165 [ALL_TAC,
166 MATCH_MP_TAC LESS_TRANS THEN EXISTS_TAC “f(m + (SUC p)):num”] THEN
167 ASM_REWRITE_TAC[ADD_CLAUSES]]
168QED
169
170(*---------------------------------------------------------------------------*)
171(* Define monotonicity *)
172(*---------------------------------------------------------------------------*)
173
174Definition mono[nocompute]:
175 mono f = (!m n:num. m <= n ==> f(m) <= (f n:real))
176 \/
177 (!m n. m <= n ==> f(m) >= f(n))
178End
179
180Theorem MONO_SUC :
181 !f:num->real. mono f <=> (!n. f(SUC n) >= f n) \/ (!n. f(SUC n) <= f(n))
182Proof
183 GEN_TAC THEN REWRITE_TAC[mono, real_ge] THEN
184 MATCH_MP_TAC(TAUT_CONV “(a = c) /\ (b = d) ==> (a \/ b = c \/ d)”)
185 THEN CONJ_TAC THEN (EQ_TAC THENL
186 [DISCH_THEN(MP_TAC o GEN “n:num” o
187 SPECL [“n:num”, “SUC n”]) THEN
188 REWRITE_TAC[LESS_EQ_SUC_REFL],
189 DISCH_TAC THEN REPEAT GEN_TAC THEN
190 DISCH_THEN(X_CHOOSE_THEN “p:num” SUBST1_TAC
191 o MATCH_MP LESS_EQUAL_ADD) THEN
192 SPEC_TAC(“p:num”,“p:num”) THEN INDUCT_TAC THEN
193 ASM_REWRITE_TAC[ADD_CLAUSES, REAL_LE_REFL] THEN
194 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “f(m + p:num):real” THEN
195 ASM_REWRITE_TAC[]])
196QED
197
198(*---------------------------------------------------------------------------*)
199(* Simpler characterization of bounded sequence *)
200(*---------------------------------------------------------------------------*)
201
202Theorem MAX_LEMMA:
203 !s N. ?k. !n:num. n < N ==> abs(s n) < k
204Proof
205 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[NOT_LESS_0] THEN
206 POP_ASSUM(X_CHOOSE_TAC “k:real”) THEN
207 DISJ_CASES_TAC (SPECL [“k:real”, “abs(s(N:num))”] REAL_LET_TOTAL) THENL
208 [EXISTS_TAC “abs(s(N:num)) + &1”, EXISTS_TAC “k:real”] THEN
209 X_GEN_TAC “n:num” THEN REWRITE_TAC[LESS_THM] THEN
210 DISCH_THEN(DISJ_CASES_THEN2 SUBST1_TAC MP_TAC) THEN
211 TRY(MATCH_MP_TAC REAL_LT_ADD1) THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
212 DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
213 MATCH_MP_TAC REAL_LT_ADD1 THEN
214 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “k:real” THEN
215 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN
216 ASM_REWRITE_TAC[]
217QED
218
219Theorem SEQ_BOUNDED:
220 !s. bounded(mr1, ^geq) s = ?k. !n. abs(s n) < k
221Proof
222 GEN_TAC THEN REWRITE_TAC[MR1_BOUNDED] THEN
223 REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL] THEN EQ_TAC THENL
224 [DISCH_THEN(X_CHOOSE_THEN “k:real” (X_CHOOSE_TAC “N:num”)) THEN
225 MP_TAC(SPECL [“s:num->real”, “N:num”] MAX_LEMMA) THEN
226 DISCH_THEN(X_CHOOSE_TAC “l:real”) THEN
227 DISJ_CASES_TAC (SPECL [“k:real”, “l:real”] REAL_LE_TOTAL) THENL
228 [EXISTS_TAC “l:real”, EXISTS_TAC “k:real”] THEN
229 X_GEN_TAC “n:num” THEN MP_TAC(SPECL [“n:num”, “N:num”] LESS_CASES) THEN
230 DISCH_THEN(DISJ_CASES_THEN(ANTE_RES_THEN ASSUME_TAC)) THEN
231 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
232 FIRST_ASSUM(fn th => EXISTS_TAC(rand(concl th)) THEN
233 ASM_REWRITE_TAC[] THEN NO_TAC),
234 DISCH_THEN(X_CHOOSE_TAC “k:real”) THEN
235 MAP_EVERY EXISTS_TAC [“k:real”, “0:num”] THEN
236 GEN_TAC THEN ASM_REWRITE_TAC[]]
237QED
238
239Theorem SEQ_BOUNDED_2:
240 !f k k'. (!n. k <= f(n) /\ f(n) <= k') ==> bounded(mr1, ^geq) f
241Proof
242 REPEAT STRIP_TAC THEN REWRITE_TAC[SEQ_BOUNDED] THEN
243 EXISTS_TAC “(abs(k) + abs(k')) + &1” THEN GEN_TAC THEN
244 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “abs(k) + abs(k')” THEN
245 REWRITE_TAC[REAL_LT_ADDR, REAL_LT_01] THEN
246 GEN_REWR_TAC LAND_CONV [abs] THEN
247 COND_CASES_TAC THENL
248 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “abs(k')” THEN
249 REWRITE_TAC[REAL_LE_ADDL, ABS_POS] THEN
250 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “k':real” THEN
251 ASM_REWRITE_TAC[ABS_LE],
252 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “abs(k)” THEN
253 REWRITE_TAC[REAL_LE_ADDR, ABS_POS] THEN
254 REWRITE_TAC[abs] THEN
255 COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_LE_NEG] THEN
256 SUBGOAL_THEN “&0 <= f(n:num)” MP_TAC THENL
257 [MATCH_MP_TAC REAL_LE_TRANS THEN
258 EXISTS_TAC “k:real” THEN ASM_REWRITE_TAC[],
259 ASM_REWRITE_TAC[]]]
260QED
261
262(*---------------------------------------------------------------------------*)
263(* Show that every Cauchy sequence is bounded *)
264(*---------------------------------------------------------------------------*)
265
266Theorem SEQ_CBOUNDED:
267 !f. cauchy f ==> bounded(mr1, ^geq) f
268Proof
269 GEN_TAC THEN REWRITE_TAC[bounded, cauchy] THEN
270 DISCH_THEN(MP_TAC o SPEC “&1”) THEN REWRITE_TAC[REAL_LT_01] THEN
271 DISCH_THEN(X_CHOOSE_TAC “N:num”) THEN
272 MAP_EVERY EXISTS_TAC [“&1”, “(f:num->real) N”, “N:num”] THEN
273 REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL] THEN
274 POP_ASSUM(MP_TAC o SPEC “N:num”) THEN
275 REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL, MR1_DEF]
276QED
277
278(*---------------------------------------------------------------------------*)
279(* Show that a bounded and monotonic sequence converges *)
280(*---------------------------------------------------------------------------*)
281
282Theorem SEQ_ICONV:
283 !f. bounded(mr1, ^geq) f /\ (!m n:num. m >= n ==> f(m) >= f(n))
284 ==> convergent f
285Proof
286GEN_TAC THEN DISCH_TAC THEN
287 MP_TAC (SPEC “\x:real. ?n:num. x = f(n)” REAL_SUP) THEN BETA_TAC THEN
288 W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
289 [CONJ_TAC THENL
290 [MAP_EVERY EXISTS_TAC [“f(0:num):real”, “0:num”] THEN REFL_TAC,
291 POP_ASSUM(MP_TAC o REWRITE_RULE[SEQ_BOUNDED] o CONJUNCT1) THEN
292 DISCH_THEN(X_CHOOSE_TAC “k:real”) THEN
293 EXISTS_TAC “k:real” THEN
294 GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN “n:num” SUBST1_TAC) THEN
295 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “abs(f(n:num))” THEN
296 ASM_REWRITE_TAC[ABS_LE]], ALL_TAC] THEN
297 DISCH_THEN(fn th => REWRITE_TAC[th]) THEN DISCH_TAC THEN
298 REWRITE_TAC[convergent] THEN EXISTS_TAC “sup(\x. ?n:num. x = f(n))” THEN
299 REWRITE_TAC[SEQ] THEN X_GEN_TAC “e:real” THEN DISCH_TAC THEN
300 FIRST_ASSUM(MP_TAC o assert(is_forall o concl)) THEN
301 DISCH_THEN(MP_TAC o SPEC “sup(\x. ?n:num. x = f(n)) - e”) THEN
302 REWRITE_TAC[REAL_LT_SUB_RADD, REAL_LT_ADDR] THEN
303 ASM_REWRITE_TAC[] THEN
304 DISCH_THEN(X_CHOOSE_THEN “x:real” MP_TAC) THEN
305 ONCE_REWRITE_TAC[CONJ_SYM] THEN
306 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_THEN “n:num” SUBST1_TAC)) THEN
307 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[GSYM REAL_LT_SUB_RADD] THEN
308 DISCH_TAC THEN SUBGOAL_THEN “!n. f(n) <= sup(\x. ?n:num. x = f(n))”
309 ASSUME_TAC THENL
310 [FIRST_ASSUM(MP_TAC o SPEC “sup(\x. ?n:num. x = f(n))”) THEN
311 REWRITE_TAC[REAL_LT_REFL] THEN
312 CONV_TAC(ONCE_DEPTH_CONV NOT_EXISTS_CONV) THEN
313 REWRITE_TAC[TAUT_CONV “~(a /\ b) = a ==> ~b”] THEN
314 REWRITE_TAC[REAL_NOT_LT] THEN
315 CONV_TAC(ONCE_DEPTH_CONV LEFT_IMP_EXISTS_CONV) THEN
316 DISCH_THEN(MP_TAC o GEN “n:num” o SPECL [“(f:num->real) n”, “n:num”]) THEN
317 REWRITE_TAC[], ALL_TAC] THEN
318 EXISTS_TAC “n:num” THEN X_GEN_TAC “m:num” THEN
319 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN
320 DISCH_THEN(ASSUME_TAC o CONJUNCT2) THEN
321 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
322 RULE_ASSUM_TAC(REWRITE_RULE[REAL_LT_SUB_RADD]) THEN
323 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[REAL_ADD_SYM]) THEN
324 RULE_ASSUM_TAC(REWRITE_RULE[GSYM REAL_LT_SUB_RADD]) THEN
325 REWRITE_TAC[real_ge] THEN DISCH_TAC THEN
326 SUBGOAL_THEN “(sup(\x. ?m:num. x = f(m)) - e) < f(m)” ASSUME_TAC THENL
327 [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC “(f:num->real) n” THEN
328 ASM_REWRITE_TAC[], ALL_TAC] THEN
329 REWRITE_TAC[abs] THEN COND_CASES_TAC THEN
330 ASM_REWRITE_TAC[REAL_NEG_SUB] THENL
331 [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “&0” THEN
332 ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_sub] THEN
333 (SUBST1_TAC o REWRITE_RULE[REAL_ADD_RINV] o C SPECL REAL_LE_RADD)
334 [“(f:num->real) m”, “(sup(\x. ?n:num. x = f(n)))”,
335 “~(sup(\x. ?n:num. x = f(n)))”] THEN
336 ASM_REWRITE_TAC[],
337 REWRITE_TAC[REAL_LT_SUB_RADD] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
338 REWRITE_TAC[GSYM REAL_LT_SUB_RADD] THEN ASM_REWRITE_TAC[]]
339QED
340
341Theorem SEQ_NEG_CONV:
342 !f. convergent f = convergent (\n. ~(f n))
343Proof
344 GEN_TAC THEN REWRITE_TAC[convergent] THEN EQ_TAC THEN
345 DISCH_THEN(X_CHOOSE_TAC “l:real”) THEN
346 Q.EXISTS_TAC ‘~l’ THEN POP_ASSUM MP_TAC THEN
347 SUBST1_TAC(SYM(SPEC “l:real” REAL_NEGNEG)) THEN
348 REWRITE_TAC[GSYM SEQ_NEG] THEN REWRITE_TAC[REAL_NEGNEG]
349QED
350
351Theorem SEQ_NEG_BOUNDED:
352 !f. bounded(mr1, ^geq)(\n. ~(f n)) = bounded(mr1, ^geq) f
353Proof
354 GEN_TAC THEN REWRITE_TAC[SEQ_BOUNDED] THEN BETA_TAC THEN
355 REWRITE_TAC[ABS_NEG]
356QED
357
358Theorem SEQ_BCONV:
359 !f. bounded(mr1, ^geq) f /\ mono f ==> convergent f
360Proof
361 GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
362 REWRITE_TAC[mono] THEN DISCH_THEN DISJ_CASES_TAC THENL
363 [MATCH_MP_TAC SEQ_ICONV THEN ASM_REWRITE_TAC[GREATER_EQ, real_ge],
364 ONCE_REWRITE_TAC[SEQ_NEG_CONV] THEN MATCH_MP_TAC SEQ_ICONV THEN
365 ASM_REWRITE_TAC[SEQ_NEG_BOUNDED] THEN BETA_TAC THEN
366 REWRITE_TAC[GREATER_EQ, real_ge, REAL_LE_NEG] THEN
367 ONCE_REWRITE_TAC[GSYM real_ge] THEN ASM_REWRITE_TAC[]]
368QED
369
370(*---------------------------------------------------------------------------*)
371(* Show that every sequence contains a monotonic subsequence *)
372(*---------------------------------------------------------------------------*)
373
374Theorem SEQ_MONOSUB:
375 !s:num->real. ?f. subseq f /\ mono(\n. s(f n))
376Proof
377 GEN_TAC THEN
378 ASM_CASES_TAC “!n. ?p:num. p>n /\ !m. m >= p ==> s(m) <= s(p)” THENL
379 [(X_CHOOSE_THEN “f:num->num” MP_TAC o EXISTENCE o
380 C ISPECL num_Axiom_old)
381 [“@p:num. p>0 /\ (!m. m >= p ==> (s m) <= (s p))”,
382 “\x. \n:num. @p:num. p > x /\ (!m. m >= p ==> (s m) <= (s p))”] THEN
383 BETA_TAC THEN RULE_ASSUM_TAC
384 (GEN “n:num” o SELECT_RULE o SPEC “n:num”) THEN
385 POP_ASSUM(fn th => DISCH_THEN(ASSUME_TAC o GSYM) THEN
386 MP_TAC(SPEC “0:num” th) THEN
387 MP_TAC(GEN “n:num” (SPEC “(f:num->num) n” th))) THEN
388 ASM_REWRITE_TAC[] THEN POP_ASSUM(K ALL_TAC) THEN REPEAT STRIP_TAC THEN
389 EXISTS_TAC “f:num->num” THEN ASM_REWRITE_TAC[SUBSEQ_SUC, GSYM GREATER_DEF] THEN
390 SUBGOAL_THEN “!(p:num) q. p >= (f q) ==> s(p) <= s(f(q:num))” MP_TAC THENL
391 [REPEAT GEN_TAC THEN STRUCT_CASES_TAC(SPEC “q:num” num_CASES) THEN
392 ASM_REWRITE_TAC[], ALL_TAC] THEN
393 DISCH_THEN(MP_TAC o GEN “q:num” o SPECL [“f(SUC q):num”, “q:num”]) THEN
394 SUBGOAL_THEN “!q. f(SUC q) >= f(q):num” (fn th => REWRITE_TAC[th]) THENL
395 [GEN_TAC THEN REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_IMP_LESS_OR_EQ
396 THEN ASM_REWRITE_TAC[GSYM GREATER_DEF], ALL_TAC] THEN
397 DISCH_TAC THEN REWRITE_TAC[MONO_SUC] THEN DISJ2_TAC THEN
398 BETA_TAC THEN ASM_REWRITE_TAC[],
399 POP_ASSUM(X_CHOOSE_TAC “N:num” o CONV_RULE NOT_FORALL_CONV) THEN
400 POP_ASSUM(MP_TAC o CONV_RULE NOT_EXISTS_CONV) THEN
401 REWRITE_TAC[TAUT_CONV “~(a /\ b) = a ==> ~b”] THEN
402 CONV_TAC(ONCE_DEPTH_CONV NOT_FORALL_CONV) THEN
403 REWRITE_TAC[NOT_IMP, REAL_NOT_LE] THEN DISCH_TAC THEN
404 SUBGOAL_THEN “!p. p >= SUC N ==> (?m. m > p /\ s(p) < s(m))”
405 MP_TAC THENL
406 [GEN_TAC THEN REWRITE_TAC[GREATER_EQ, GSYM LESS_EQ] THEN
407 REWRITE_TAC[GSYM GREATER_DEF] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
408 REWRITE_TAC[GREATER_EQ, LESS_OR_EQ, RIGHT_AND_OVER_OR, GREATER_DEF] THEN
409 DISCH_THEN(X_CHOOSE_THEN “m:num” DISJ_CASES_TAC) THENL
410 [EXISTS_TAC “m:num” THEN ASM_REWRITE_TAC[],
411 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN
412 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
413 ASM_REWRITE_TAC[REAL_LT_REFL]], ALL_TAC] THEN
414 POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN
415 (X_CHOOSE_THEN “f:num->num” MP_TAC o EXISTENCE o
416 C ISPECL num_Axiom_old)
417 [“@m. m > SUC N /\ s(SUC N) < s(m)”,
418 “\x:num. \n:num. @m. m > x /\ s(x) < s(m)”] THEN
419 BETA_TAC THEN DISCH_THEN ASSUME_TAC THEN SUBGOAL_THEN
420 “!n. f(n) >= SUC N /\
421 f(SUC n) > f(n) /\ s(f n) < s(f(SUC n))” MP_TAC THENL
422 [INDUCT_TAC THENL
423 [SUBGOAL_THEN “f(0:num) >= SUC N” MP_TAC THENL
424 [FIRST_ASSUM(MP_TAC o SPEC “SUC N”) THEN
425 REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL] THEN
426 DISCH_THEN(MP_TAC o SELECT_RULE) THEN ASM_REWRITE_TAC[] THEN
427 DISCH_THEN(ASSUME_TAC o CONJUNCT1) THEN
428 MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN
429 ASM_REWRITE_TAC[GSYM GREATER_DEF], ALL_TAC] THEN
430 DISCH_THEN(fn th => ASSUME_TAC th THEN REWRITE_TAC[th]) THEN
431 FIRST_ASSUM(fn th => REWRITE_TAC[CONJUNCT2 th]) THEN
432 CONV_TAC SELECT_CONV THEN FIRST_ASSUM MATCH_MP_TAC THEN
433 FIRST_ASSUM ACCEPT_TAC,
434 FIRST_ASSUM(UNDISCH_TAC o
435 assert(curry op =3 o length o strip_conj) o concl) THEN
436 DISCH_THEN STRIP_ASSUME_TAC THEN CONJ_TAC THENL
437 [REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_EQ_TRANS THEN
438 EXISTS_TAC “(f:num->num) n” THEN REWRITE_TAC[GSYM GREATER_EQ] THEN
439 CONJ_TAC THEN TRY(FIRST_ASSUM ACCEPT_TAC) THEN
440 REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN
441 REWRITE_TAC[GSYM GREATER_DEF] THEN FIRST_ASSUM ACCEPT_TAC,
442 FIRST_ASSUM(SUBST1_TAC o SPEC “SUC n” o CONJUNCT2) THEN
443 CONV_TAC SELECT_CONV THEN FIRST_ASSUM MATCH_MP_TAC THEN
444 REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_EQ_TRANS THEN
445 EXISTS_TAC “(f:num->num) n” THEN
446 REWRITE_TAC[GSYM GREATER_EQ] THEN CONJ_TAC THEN
447 TRY(FIRST_ASSUM ACCEPT_TAC) THEN
448 REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN
449 REWRITE_TAC[GSYM GREATER_DEF] THEN
450 FIRST_ASSUM ACCEPT_TAC]], ALL_TAC] THEN
451 POP_ASSUM_LIST(K ALL_TAC) THEN DISCH_TAC THEN
452 EXISTS_TAC “f:num->num” THEN REWRITE_TAC[SUBSEQ_SUC, MONO_SUC] THEN
453 ASM_REWRITE_TAC[GSYM GREATER_DEF] THEN DISJ1_TAC THEN BETA_TAC THEN
454 GEN_TAC THEN REWRITE_TAC[real_ge] THEN
455 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]]
456QED
457
458(*---------------------------------------------------------------------------*)
459(* Show that a subsequence of a bounded sequence is bounded *)
460(*---------------------------------------------------------------------------*)
461
462Theorem SEQ_SBOUNDED:
463 !s f. bounded(mr1,^geq) s ==> bounded(mr1,^geq) (\n. s(f n))
464Proof
465 REPEAT GEN_TAC THEN REWRITE_TAC[SEQ_BOUNDED] THEN
466 DISCH_THEN(X_CHOOSE_TAC “k:real”) THEN EXISTS_TAC “k:real” THEN
467 GEN_TAC THEN BETA_TAC THEN ASM_REWRITE_TAC[]
468QED
469
470(*---------------------------------------------------------------------------*)
471(* Show we can take subsequential terms arbitrarily far up a sequence *)
472(*---------------------------------------------------------------------------*)
473
474Theorem SEQ_SUBLE:
475 !f. subseq f ==> !n. n <= f(n)
476Proof
477 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
478 [REWRITE_TAC[GSYM NOT_LESS, NOT_LESS_0],
479 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC “SUC(f(n:num))” THEN
480 ASM_REWRITE_TAC[LESS_EQ_MONO] THEN REWRITE_TAC[GSYM LESS_EQ] THEN
481 UNDISCH_TAC “subseq f” THEN REWRITE_TAC[SUBSEQ_SUC] THEN
482 DISCH_THEN MATCH_ACCEPT_TAC]
483QED
484
485Theorem SEQ_DIRECT:
486 !f. subseq f ==> !N1 N2. ?n. n >= N1 /\ f(n) >= N2
487Proof
488 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
489 DISJ_CASES_TAC (SPECL [“N1:num”, “N2:num”] LESS_EQ_CASES) THENL
490 [EXISTS_TAC “N2:num” THEN ASM_REWRITE_TAC[GREATER_EQ] THEN
491 MATCH_MP_TAC SEQ_SUBLE THEN FIRST_ASSUM ACCEPT_TAC,
492 EXISTS_TAC “N1:num” THEN REWRITE_TAC[GREATER_EQ, LESS_EQ_REFL] THEN
493 REWRITE_TAC[GREATER_EQ] THEN MATCH_MP_TAC LESS_EQ_TRANS THEN
494 EXISTS_TAC “N1:num” THEN ASM_REWRITE_TAC[] THEN
495 MATCH_MP_TAC SEQ_SUBLE THEN FIRST_ASSUM ACCEPT_TAC]
496QED
497
498(*---------------------------------------------------------------------------*)
499(* Now show that every Cauchy sequence converges *)
500(*---------------------------------------------------------------------------*)
501
502Theorem SEQ_CAUCHY:
503 !f. cauchy f = convergent f
504Proof
505 GEN_TAC THEN EQ_TAC THENL
506 [DISCH_TAC THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP SEQ_CBOUNDED) THEN
507 MP_TAC(SPEC “f:num->real” SEQ_MONOSUB) THEN
508 DISCH_THEN(X_CHOOSE_THEN “g:num->num” STRIP_ASSUME_TAC) THEN
509 SUBGOAL_THEN “bounded(mr1, ^geq)(\n. f(g(n):num))” ASSUME_TAC THENL
510 [MATCH_MP_TAC SEQ_SBOUNDED THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
511 SUBGOAL_THEN “convergent (\n. f(g(n):num))” MP_TAC THENL
512 [MATCH_MP_TAC SEQ_BCONV THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
513 REWRITE_TAC[convergent] THEN DISCH_THEN(X_CHOOSE_TAC “l:real”) THEN
514 EXISTS_TAC “l:real” THEN REWRITE_TAC[SEQ] THEN
515 X_GEN_TAC “e:real” THEN DISCH_TAC THEN
516 UNDISCH_TAC “(\n. f(g(n):num)) --> l” THEN REWRITE_TAC[SEQ] THEN
517 DISCH_THEN(MP_TAC o SPEC “e / &2”) THEN
518 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN BETA_TAC THEN
519 DISCH_THEN(X_CHOOSE_TAC “N1:num”) THEN
520 UNDISCH_TAC “cauchy f” THEN REWRITE_TAC[cauchy] THEN
521 DISCH_THEN(MP_TAC o SPEC “e / &2”) THEN
522 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN
523 DISCH_THEN(X_CHOOSE_THEN “N2:num” ASSUME_TAC) THEN
524 FIRST_ASSUM(MP_TAC o MATCH_MP SEQ_DIRECT) THEN
525 DISCH_THEN(MP_TAC o SPECL [“N1:num”, “N2:num”]) THEN
526 DISCH_THEN(X_CHOOSE_THEN “n:num” STRIP_ASSUME_TAC) THEN
527 EXISTS_TAC “N2:num” THEN X_GEN_TAC “m:num” THEN DISCH_TAC THEN
528 UNDISCH_TAC “!n:num. n >= N1 ==> abs(f(g n:num) - l) < (e / &2)” THEN
529 DISCH_THEN(MP_TAC o SPEC “n:num”) THEN ASM_REWRITE_TAC[] THEN
530 DISCH_TAC THEN FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
531 DISCH_THEN(MP_TAC o SPECL [“g(n:num):num”, “m:num”]) THEN
532 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
533 MATCH_MP_TAC REAL_LET_TRANS THEN
534 SUBGOAL_THEN “f(m:num) - l = (f(m) - f(g(n:num))) + (f(g n) - l)”
535 SUBST1_TAC THENL [REWRITE_TAC[REAL_SUB_TRIANGLE], ALL_TAC] THEN
536 EXISTS_TAC “abs(f(m:num) - f(g(n:num))) + abs(f(g n) - l)” THEN
537 REWRITE_TAC[ABS_TRIANGLE] THEN
538 SUBST1_TAC(SYM(SPEC “e:real” REAL_HALF_DOUBLE)) THEN
539 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[] THEN
540 ONCE_REWRITE_TAC[ABS_SUB] THEN ASM_REWRITE_TAC[],
541
542 REWRITE_TAC[convergent] THEN
543 DISCH_THEN(X_CHOOSE_THEN “l:real” MP_TAC) THEN
544 REWRITE_TAC[SEQ, cauchy] THEN DISCH_TAC THEN
545 X_GEN_TAC “e:real” THEN DISCH_TAC THEN
546 FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
547 DISCH_THEN(MP_TAC o SPEC “e / &2”) THEN
548 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN
549 DISCH_THEN(X_CHOOSE_TAC “N:num”) THEN
550 EXISTS_TAC “N:num” THEN REPEAT GEN_TAC THEN
551 DISCH_THEN(CONJUNCTS_THEN (ANTE_RES_THEN ASSUME_TAC)) THEN
552 MATCH_MP_TAC REAL_LET_TRANS THEN
553 SUBGOAL_THEN “f(m:num) - f(n) = (f(m) - l) + (l - f(n))”
554 SUBST1_TAC THENL [REWRITE_TAC[REAL_SUB_TRIANGLE], ALL_TAC] THEN
555 EXISTS_TAC “abs(f(m:num) - l) + abs(l - f(n))” THEN
556 REWRITE_TAC[ABS_TRIANGLE] THEN
557 SUBST1_TAC(SYM(SPEC “e:real” REAL_HALF_DOUBLE)) THEN
558 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[] THEN
559 ONCE_REWRITE_TAC[ABS_SUB] THEN ASM_REWRITE_TAC[]]
560QED
561
562(*---------------------------------------------------------------------------*)
563(* The limit comparison property for sequences *)
564(*---------------------------------------------------------------------------*)
565
566Theorem SEQ_LE:
567 !f g l m. f --> l /\ g --> m /\ (?N. !n. n >= N ==> f(n) <= g(n))
568 ==> l <= m
569Proof
570 REPEAT GEN_TAC THEN
571 MP_TAC(ISPEC geq NET_LE) THEN
572 REWRITE_TAC[DORDER_NGE, tends_num_real, GREATER_EQ, LESS_EQ_REFL] THEN
573 DISCH_THEN MATCH_ACCEPT_TAC
574QED
575
576(*---------------------------------------------------------------------------*)
577(* We can displace a convergent series by 1 *)
578(*---------------------------------------------------------------------------*)
579
580Theorem SEQ_SUC:
581 !f l. f --> l = (\n. f(SUC n)) --> l
582Proof
583 REPEAT GEN_TAC THEN REWRITE_TAC[SEQ, GREATER_EQ] THEN EQ_TAC THEN
584 DISCH_THEN(fn th => X_GEN_TAC “e:real” THEN
585 DISCH_THEN(MP_TAC o MATCH_MP th)) THEN BETA_TAC THEN
586 DISCH_THEN(X_CHOOSE_TAC “N:num”) THENL
587 [EXISTS_TAC “N:num” THEN X_GEN_TAC “n:num” THEN DISCH_TAC THEN
588 FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC LESS_EQ_TRANS THEN
589 EXISTS_TAC “SUC N” THEN ASM_REWRITE_TAC[LESS_EQ_MONO, LESS_EQ_SUC_REFL],
590 EXISTS_TAC “SUC N” THEN X_GEN_TAC “n:num” THEN
591 STRUCT_CASES_TAC (SPEC “n:num” num_CASES) THENL
592 [REWRITE_TAC[GSYM NOT_LESS, LESS_0],
593 REWRITE_TAC[LESS_EQ_MONO] THEN DISCH_TAC THEN
594 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]]
595QED
596
597(*---------------------------------------------------------------------------*)
598(* Prove a sequence tends to zero iff its abs does *)
599(*---------------------------------------------------------------------------*)
600
601Theorem SEQ_ABS:
602 !f. (\n. abs(f n)) --> &0 = f --> &0
603Proof
604 GEN_TAC THEN REWRITE_TAC[SEQ] THEN
605 BETA_TAC THEN REWRITE_TAC[REAL_SUB_RZERO, ABS_ABS]
606QED
607
608(*---------------------------------------------------------------------------*)
609(* Half this is true for a general limit *)
610(*---------------------------------------------------------------------------*)
611
612Theorem SEQ_ABS_IMP:
613 !f l. f --> l ==> (\n. abs(f n)) --> abs(l)
614Proof
615 REPEAT GEN_TAC THEN REWRITE_TAC[tends_num_real] THEN
616 MATCH_ACCEPT_TAC NET_ABS
617QED
618
619(*---------------------------------------------------------------------------*)
620(* Prove that an unbounded sequence's inverse tends to 0 *)
621(*---------------------------------------------------------------------------*)
622
623Theorem SEQ_INV0:
624 !f. (!y. ?N. !n. n >= N ==> f(n) > y)
625 ==>
626 (\n. inv(f n)) --> &0
627Proof
628 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[SEQ, REAL_SUB_RZERO] THEN
629 X_GEN_TAC “e:real” THEN DISCH_TAC THEN
630 FIRST_ASSUM(X_CHOOSE_TAC “N:num” o SPEC “inv e”) THEN
631 EXISTS_TAC “N:num” THEN X_GEN_TAC “n:num” THEN
632 DISCH_THEN(fn th => ASSUME_TAC th THEN ANTE_RES_THEN MP_TAC th) THEN
633 REWRITE_TAC[real_gt] THEN BETA_TAC THEN IMP_RES_TAC REAL_INV_POS THEN
634 SUBGOAL_THEN “&0 < f(n:num)” ASSUME_TAC THENL
635 [MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC “inv e” THEN
636 ASM_REWRITE_TAC[] THEN REWRITE_TAC[GSYM real_gt] THEN
637 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
638 SUBGOAL_THEN “&0 < inv(f(n:num))” ASSUME_TAC THENL
639 [MATCH_MP_TAC REAL_INV_POS THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
640 SUBGOAL_THEN “~(f(n:num) = &0)” ASSUME_TAC THENL
641 [CONV_TAC(RAND_CONV SYM_CONV) THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN
642 ASM_REWRITE_TAC[], ALL_TAC] THEN DISCH_TAC THEN
643 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP ABS_INV th]) THEN
644 SUBGOAL_THEN “e = inv(inv e)” SUBST1_TAC THENL
645 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_INVINV THEN
646 CONV_TAC(RAND_CONV SYM_CONV) THEN
647 MATCH_MP_TAC REAL_LT_IMP_NE THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
648 MATCH_MP_TAC REAL_LT_INV THEN ASM_REWRITE_TAC[] THEN
649 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC “(f:num->real) n” THEN
650 ASM_REWRITE_TAC[ABS_LE]
651QED
652
653(*---------------------------------------------------------------------------*)
654(* Important limit of c^n for |c| < 1 *)
655(*---------------------------------------------------------------------------*)
656
657Theorem SEQ_POWER_ABS:
658 !c. abs(c) < &1 ==> (\n. abs(c) pow n) --> &0
659Proof
660 GEN_TAC THEN DISCH_TAC THEN MP_TAC(SPEC “c:real” ABS_POS) THEN
661 REWRITE_TAC[REAL_LE_LT] THEN DISCH_THEN DISJ_CASES_TAC THENL
662 [SUBGOAL_THEN “!n. abs(c) pow n = inv(inv(abs(c) pow n))”
663 (fn th => ONCE_REWRITE_TAC[th]) THENL
664 [GEN_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_INVINV THEN
665 MATCH_MP_TAC POW_NZ THEN
666 ASM_REWRITE_TAC[ABS_NZ, ABS_ABS], ALL_TAC] THEN
667 CONV_TAC(EXACT_CONV[X_BETA_CONV “n:num” “inv(abs(c) pow n)”]) THEN
668 MATCH_MP_TAC SEQ_INV0 THEN BETA_TAC THEN X_GEN_TAC “y:real” THEN
669 SUBGOAL_THEN “~(abs(c) = &0)” (fn th => REWRITE_TAC[MATCH_MP POW_INV th]) THENL
670 [CONV_TAC(RAND_CONV SYM_CONV) THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN
671 ASM_REWRITE_TAC[], ALL_TAC] THEN REWRITE_TAC[real_gt] THEN
672 SUBGOAL_THEN “&0 < inv(abs c) - &1” ASSUME_TAC THENL
673 [REWRITE_TAC[REAL_LT_SUB_LADD] THEN REWRITE_TAC[REAL_ADD_LID] THEN
674 ONCE_REWRITE_TAC[GSYM REAL_INV1] THEN MATCH_MP_TAC REAL_LT_INV THEN
675 ASM_REWRITE_TAC[], ALL_TAC] THEN
676 MP_TAC(SPEC “inv(abs c) - &1” REAL_ARCH) THEN ASM_REWRITE_TAC[] THEN
677 DISCH_THEN(X_CHOOSE_TAC “N:num” o SPEC “y:real”) THEN
678 EXISTS_TAC “N:num” THEN X_GEN_TAC “n:num” THEN REWRITE_TAC[GREATER_EQ] THEN
679 DISCH_TAC THEN SUBGOAL_THEN “y < (&n * (inv(abs c) - &1))”
680 ASSUME_TAC THENL
681 [MATCH_MP_TAC REAL_LTE_TRANS THEN
682 EXISTS_TAC “&N * (inv(abs c) - &1)” THEN ASM_REWRITE_TAC[] THEN
683 FIRST_ASSUM(fn th => GEN_REWR_TAC I [MATCH_MP REAL_LE_RMUL th]) THEN
684 ASM_REWRITE_TAC[REAL_LE], ALL_TAC] THEN
685 MATCH_MP_TAC REAL_LT_TRANS THEN
686 EXISTS_TAC “&n * (inv(abs c) - &1)” THEN ASM_REWRITE_TAC[] THEN
687 MATCH_MP_TAC REAL_LTE_TRANS THEN
688 EXISTS_TAC “&1 + (&n * (inv(abs c) - &1))” THEN
689 REWRITE_TAC[REAL_LT_ADDL, REAL_LT_01] THEN
690 MATCH_MP_TAC REAL_LE_TRANS THEN
691 EXISTS_TAC “(&1 + (inv(abs c) - &1)) pow n” THEN CONJ_TAC THENL
692 [MATCH_MP_TAC POW_PLUS1 THEN ASM_REWRITE_TAC[],
693 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[REAL_SUB_ADD] THEN
694 REWRITE_TAC[REAL_LE_REFL]],
695 FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[SEQ] THEN
696 GEN_TAC THEN DISCH_TAC THEN EXISTS_TAC “1:num” THEN
697 X_GEN_TAC “n:num” THEN REWRITE_TAC[GREATER_EQ] THEN BETA_TAC THEN
698 STRUCT_CASES_TAC(SPEC “n:num” num_CASES) THENL
699 [REWRITE_TAC[GSYM NOT_LESS, ONE, LESS_0],
700 REWRITE_TAC[POW_0, REAL_SUB_RZERO, ABS_0] THEN
701 REWRITE_TAC[ASSUME “&0 < e”]]]
702QED
703
704(*---------------------------------------------------------------------------*)
705(* Similar version without the abs *)
706(*---------------------------------------------------------------------------*)
707
708Theorem SEQ_POWER:
709 !c. abs(c) < &1 ==> (\n. c pow n) --> &0
710Proof
711 GEN_TAC THEN DISCH_TAC THEN
712 ONCE_REWRITE_TAC[GSYM SEQ_ABS] THEN BETA_TAC THEN
713 REWRITE_TAC[GSYM POW_ABS] THEN
714 POP_ASSUM(ACCEPT_TAC o MATCH_MP SEQ_POWER_ABS)
715QED
716
717(*---------------------------------------------------------------------------*)
718(* Useful lemmas about nested intervals and proof by bisection *)
719(*---------------------------------------------------------------------------*)
720
721Theorem NEST_LEMMA:
722 !f g. (!n. f(SUC n) >= f(n)) /\
723 (!n. g(SUC n) <= g(n)) /\
724 (!n. f(n) <= g(n)) ==>
725 ?l m. l <= m /\ ((!n. f(n) <= l) /\ f --> l) /\
726 ((!n. m <= g(n)) /\ g --> m)
727Proof
728 REPEAT STRIP_TAC THEN MP_TAC(SPEC “f:num->real” MONO_SUC) THEN
729 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
730 MP_TAC(SPEC “g:num->real” MONO_SUC) THEN ASM_REWRITE_TAC[] THEN
731 DISCH_TAC THEN SUBGOAL_THEN “bounded(mr1,^geq) f” ASSUME_TAC THENL
732 [MATCH_MP_TAC SEQ_BOUNDED_2 THEN
733 MAP_EVERY EXISTS_TAC [“(f:num->real) 0”, “(g:num->real) 0”] THEN
734 INDUCT_TAC THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN CONJ_TAC THENL
735 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “(f:num->real) n” THEN
736 RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN ASM_REWRITE_TAC[],
737 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “g(SUC n):real” THEN
738 ASM_REWRITE_TAC[] THEN SPEC_TAC(“SUC n”,“m:num”) THEN
739 INDUCT_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
740 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “g(m:num):real” THEN
741 ASM_REWRITE_TAC[]], ALL_TAC] THEN
742 SUBGOAL_THEN “bounded(mr1, ^geq) g” ASSUME_TAC THENL
743 [MATCH_MP_TAC SEQ_BOUNDED_2 THEN
744 MAP_EVERY EXISTS_TAC [“(f:num->real) 0”, “(g:num->real) 0”] THEN
745 INDUCT_TAC THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN CONJ_TAC THENL
746 [MATCH_MP_TAC REAL_LE_TRANS THEN
747 EXISTS_TAC “(f:num->real) (SUC n)” THEN
748 ASM_REWRITE_TAC[] THEN SPEC_TAC(“SUC n”,“m:num”) THEN
749 INDUCT_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
750 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “(f:num->real) m” THEN
751 RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN ASM_REWRITE_TAC[],
752 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “(g:num->real) n” THEN
753 ASM_REWRITE_TAC[]], ALL_TAC] THEN
754 MP_TAC(SPEC “f:num->real” SEQ_BCONV) THEN ASM_REWRITE_TAC[SEQ_LIM] THEN
755 DISCH_TAC THEN MP_TAC(SPEC “g:num->real” SEQ_BCONV) THEN
756 ASM_REWRITE_TAC[SEQ_LIM] THEN DISCH_TAC THEN
757 MAP_EVERY EXISTS_TAC [“lim f”, “lim g”] THEN
758 ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
759 [MATCH_MP_TAC SEQ_LE THEN
760 MAP_EVERY EXISTS_TAC [“f:num->real”, “g:num->real”] THEN
761 ASM_REWRITE_TAC[],
762 X_GEN_TAC “m:num” THEN
763 GEN_REWR_TAC I [TAUT_CONV “a = ~~a:bool”] THEN
764 PURE_REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN
765 UNDISCH_TAC “f --> lim f” THEN REWRITE_TAC[SEQ] THEN
766 DISCH_THEN(MP_TAC o SPEC “f(m) - lim f”) THEN
767 ASM_REWRITE_TAC[REAL_SUB_LT] THEN
768 DISCH_THEN(X_CHOOSE_THEN “p:num” MP_TAC) THEN
769 DISCH_THEN(MP_TAC o SPEC “p + m:num”) THEN
770 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD] THEN REWRITE_TAC[abs] THEN
771 SUBGOAL_THEN “!p:num. lim f <= f(p + m)” ASSUME_TAC THENL
772 [INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THENL
773 [MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_ASSUM ACCEPT_TAC,
774 MATCH_MP_TAC REAL_LE_TRANS THEN
775 EXISTS_TAC “f(p + m:num):real” THEN
776 RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN ASM_REWRITE_TAC[]],
777 ASM_REWRITE_TAC[REAL_SUB_LE] THEN
778 REWRITE_TAC[REAL_NOT_LT, real_sub, REAL_LE_RADD] THEN
779 SPEC_TAC(“p:num”,“p:num”) THEN INDUCT_TAC THEN
780 REWRITE_TAC[REAL_LE_REFL, ADD_CLAUSES] THEN
781 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “f(p + m:num):real” THEN
782 RULE_ASSUM_TAC(REWRITE_RULE[real_ge]) THEN ASM_REWRITE_TAC[]],
783 X_GEN_TAC “m:num” THEN
784 GEN_REWR_TAC I [TAUT_CONV “a = ~~a:bool”] THEN
785 PURE_REWRITE_TAC[REAL_NOT_LE] THEN DISCH_TAC THEN
786 UNDISCH_TAC “g --> lim g” THEN REWRITE_TAC[SEQ] THEN
787 DISCH_THEN(MP_TAC o SPEC “lim g - g(m)”) THEN
788 ASM_REWRITE_TAC[REAL_SUB_LT] THEN
789 DISCH_THEN(X_CHOOSE_THEN “p:num” MP_TAC) THEN
790 DISCH_THEN(MP_TAC o SPEC “p + m:num”) THEN
791 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD] THEN REWRITE_TAC[abs] THEN
792 SUBGOAL_THEN “!p. g(p + m:num) < lim g” ASSUME_TAC THENL
793 [INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN
794 MATCH_MP_TAC REAL_LET_TRANS THEN
795 EXISTS_TAC “g(p + m:num):real” THEN ASM_REWRITE_TAC[],
796 REWRITE_TAC[REAL_SUB_LE] THEN ASM_REWRITE_TAC[GSYM REAL_NOT_LT] THEN
797 REWRITE_TAC[REAL_NOT_LT, REAL_NEG_SUB] THEN
798 REWRITE_TAC[real_sub, REAL_LE_LADD, REAL_LE_NEG] THEN
799 SPEC_TAC(“p:num”,“p:num”) THEN INDUCT_TAC THEN
800 REWRITE_TAC[REAL_LE_REFL, ADD_CLAUSES] THEN
801 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “g(p + m:num):real” THEN
802 ASM_REWRITE_TAC[]]]
803QED
804
805Theorem NEST_LEMMA_UNIQ:
806 !f g. (!n. f(SUC n) >= f(n)) /\
807 (!n. g(SUC n) <= g(n)) /\
808 (!n. f(n) <= g(n)) /\
809 (\n. f(n) - g(n)) --> &0 ==>
810 ?l. ((!n. f(n) <= l) /\ f --> l) /\
811 ((!n. l <= g(n)) /\ g --> l)
812Proof
813 REPEAT GEN_TAC THEN
814 DISCH_THEN(fn th => STRIP_ASSUME_TAC th THEN MP_TAC th) THEN
815 REWRITE_TAC[CONJ_ASSOC] THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN
816 REWRITE_TAC[GSYM CONJ_ASSOC] THEN
817 DISCH_THEN(MP_TAC o MATCH_MP NEST_LEMMA) THEN
818 DISCH_THEN(X_CHOOSE_THEN “l:real” MP_TAC) THEN
819 DISCH_THEN(X_CHOOSE_THEN “m:real” STRIP_ASSUME_TAC) THEN
820 EXISTS_TAC “l:real” THEN ASM_REWRITE_TAC[] THEN
821 SUBGOAL_THEN “l:real = m” (fn th => ASM_REWRITE_TAC[th]) THEN
822 MP_TAC(SPECL [“f:num->real”, “l:real”, “g:num->real”, “m:real”] SEQ_SUB) THEN
823 ASM_REWRITE_TAC[] THEN
824 DISCH_THEN(MP_TAC o CONJ(ASSUME “(\n. f(n) - g(n)) --> &0”)) THEN
825 DISCH_THEN(MP_TAC o MATCH_MP SEQ_UNIQ) THEN
826 CONV_TAC(LAND_CONV SYM_CONV) THEN
827 REWRITE_TAC[REAL_SUB_0]
828QED
829
830
831Theorem BOLZANO_LEMMA:
832 !P. (!a b c. a <= b /\ b <= c /\ P(a,b) /\ P(b,c) ==> P(a,c)) /\
833 (!x. ?d. &0 < d /\ !a b. a <= x /\ x <= b /\ (b - a) < d ==> P(a,b))
834 ==> !a b. a <= b ==> P(a,b)
835Proof
836 REPEAT STRIP_TAC THEN
837 GEN_REWR_TAC I [TAUT_CONV “a = ~~a:bool”] THEN
838 DISCH_TAC THEN
839 (X_CHOOSE_THEN “f:num->real#real” STRIP_ASSUME_TAC o
840 EXISTENCE o BETA_RULE o C ISPECL num_Axiom_old)
841 [“(a:real,(b:real))”,
842 “\fn (n:num). if P(FST fn,(FST fn + SND fn) / &2)
843 then ((FST fn + SND fn) / &2,SND fn)
844 else (FST fn,(FST fn + SND fn) / &2)”] THEN
845 MP_TAC(SPECL
846 [“\n:num. FST(f(n) :real#real)”, “\n:num. SND(f(n) :real#real)”]
847 NEST_LEMMA_UNIQ) THEN BETA_TAC THEN
848 SUBGOAL_THEN “!n:num. FST(f n) <= SND(f n)” ASSUME_TAC THENL
849 [INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN
850 COND_CASES_TAC THEN REWRITE_TAC[] THENL
851 [MATCH_MP_TAC REAL_MIDDLE2, MATCH_MP_TAC REAL_MIDDLE1] THEN
852 FIRST_ASSUM ACCEPT_TAC, ALL_TAC] THEN REWRITE_TAC[real_ge] THEN
853 SUBGOAL_THEN “!n:num. FST(f n :real#real) <= FST(f(SUC n))”
854 ASSUME_TAC THENL
855 [REWRITE_TAC[real_ge] THEN INDUCT_TAC THEN
856 FIRST_ASSUM(fn th => GEN_REWR_TAC (funpow 2 RAND_CONV) [th]) THEN
857 COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
858 MATCH_MP_TAC REAL_MIDDLE1 THEN FIRST_ASSUM MATCH_ACCEPT_TAC, ALL_TAC] THEN
859 SUBGOAL_THEN “!n. ~P(FST((f:num->real#real) n),SND(f n))” ASSUME_TAC THENL
860 [INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN
861 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
862 UNDISCH_TAC “~P(FST((f:num->real#real) n),SND(f n)):bool” THEN
863 PURE_REWRITE_TAC[IMP_CLAUSES, NOT_CLAUSES] THEN
864 FIRST_ASSUM MATCH_MP_TAC THEN
865 EXISTS_TAC “(FST(f(n:num)) + SND(f(n))) / &2” THEN
866 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
867 [MATCH_MP_TAC REAL_MIDDLE1, MATCH_MP_TAC REAL_MIDDLE2] THEN
868 FIRST_ASSUM MATCH_ACCEPT_TAC, ALL_TAC] THEN
869 SUBGOAL_THEN “!n:num. SND(f(SUC n) :real#real) <= SND(f n)” ASSUME_TAC THENL
870 [BETA_TAC THEN INDUCT_TAC THEN
871 FIRST_ASSUM(fn th => GEN_REWR_TAC (LAND_CONV o RAND_CONV) [th]) THEN
872 COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN
873 MATCH_MP_TAC REAL_MIDDLE2 THEN FIRST_ASSUM MATCH_ACCEPT_TAC, ALL_TAC] THEN
874 SUBGOAL_THEN “!n:num. SND(f n) - FST(f n) = (b - a) / (&2 pow n)”
875 ASSUME_TAC THENL
876 [INDUCT_TAC THENL
877 [ASM_REWRITE_TAC[pow, real_div, REAL_INV1, REAL_MUL_RID], ALL_TAC] THEN
878 ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN
879 MATCH_MP_TAC REAL_EQ_LMUL_IMP THEN EXISTS_TAC “&2” THEN
880 REWRITE_TAC[REAL_SUB_LDISTRIB] THEN
881 (SUBGOAL_THEN “~(&2 = &0)” (fn th => REWRITE_TAC[th] THEN
882 REWRITE_TAC[MATCH_MP REAL_DIV_LMUL th]) THENL
883 [REWRITE_TAC[REAL_INJ] THEN CONV_TAC(RAND_CONV num_EQ_CONV) THEN
884 REWRITE_TAC[], ALL_TAC]) THEN
885 REWRITE_TAC[GSYM REAL_DOUBLE] THEN
886 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [REAL_ADD_SYM]
887 THEN (SUBGOAL_THEN “!x y z:real. (x + y) - (x + z) = y - z”
888 (fn th => REWRITE_TAC[th])
889 THENL
890 [REPEAT GEN_TAC THEN REWRITE_TAC[real_sub, REAL_NEG_ADD] THEN
891 GEN_REWR_TAC RAND_CONV [GSYM REAL_ADD_RID] THEN
892 SUBST1_TAC(SYM(SPEC “x:real” REAL_ADD_LINV)) THEN
893 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM)), ALL_TAC]) THEN
894 ASM_REWRITE_TAC[REAL_DOUBLE] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
895 REWRITE_TAC[real_div, GSYM REAL_MUL_ASSOC] THEN
896 AP_TERM_TAC THEN REWRITE_TAC[pow] THEN
897 (SUBGOAL_THEN “~(&2 = &0) /\ ~(&2 pow n = &0)”
898 (fn th => REWRITE_TAC[MATCH_MP REAL_INV_MUL th]) THENL
899 [CONJ_TAC THENL [ALL_TAC, MATCH_MP_TAC POW_NZ] THEN
900 REWRITE_TAC[REAL_INJ] THEN
901 CONV_TAC(RAND_CONV num_EQ_CONV) THEN REWRITE_TAC[],
902 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN
903 GEN_REWR_TAC (RATOR_CONV o RAND_CONV)
904 [GSYM REAL_MUL_LID] THEN
905 AP_THM_TAC THEN AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN
906 MATCH_MP_TAC REAL_MUL_RINV THEN REWRITE_TAC[REAL_INJ] THEN
907 CONV_TAC(RAND_CONV num_EQ_CONV) THEN REWRITE_TAC[]]),
908 ALL_TAC] THEN
909 FIRST_ASSUM(UNDISCH_TAC o assert (can (find_term is_cond)) o concl) THEN
910 DISCH_THEN(K ALL_TAC) THEN ASM_REWRITE_TAC[] THEN
911 W(C SUBGOAL_THEN (fn t => REWRITE_TAC[t]) o fst o dest_imp o rand o snd) THENL
912 [ONCE_REWRITE_TAC[SEQ_NEG] THEN BETA_TAC THEN
913 ASM_REWRITE_TAC[REAL_NEG_SUB, REAL_NEG_0] THEN
914 REWRITE_TAC[real_div] THEN SUBGOAL_THEN “~(&2 = &0)” ASSUME_TAC THENL
915 [REWRITE_TAC[REAL_INJ] THEN CONV_TAC(RAND_CONV num_EQ_CONV) THEN
916 REWRITE_TAC[], ALL_TAC] THEN
917 (MP_TAC o C SPECL SEQ_MUL)
918 [“\n:num. b - a”, “b - a”, “\n. (inv (&2 pow n))”, “&0”] THEN
919 REWRITE_TAC[SEQ_CONST, REAL_MUL_RZERO] THEN BETA_TAC THEN
920 DISCH_THEN MATCH_MP_TAC THEN
921 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP POW_INV th]) THEN
922 ONCE_REWRITE_TAC[GSYM SEQ_ABS] THEN BETA_TAC THEN
923 REWRITE_TAC[GSYM POW_ABS] THEN MATCH_MP_TAC SEQ_POWER_ABS THEN
924 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP ABS_INV th]) THEN
925 REWRITE_TAC[ABS_N] THEN SUBGOAL_THEN “&0 < &2”
926 (fn th => ONCE_REWRITE_TAC [GSYM (MATCH_MP REAL_LT_RMUL th)]) THENL
927 [REWRITE_TAC[REAL_LT, num_CONV “2:num”, LESS_0], ALL_TAC] THEN
928 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th]) THEN
929 REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[REAL_LT] THEN
930 REWRITE_TAC[num_CONV “2:num”, LESS_SUC_REFL],
931 DISCH_THEN(X_CHOOSE_THEN “l:real” STRIP_ASSUME_TAC) THEN
932 FIRST_ASSUM(X_CHOOSE_THEN “d:real” MP_TAC o SPEC “l:real”) THEN
933 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
934 UNDISCH_TAC “(\n:num. SND(f n :real#real)) --> l” THEN
935 UNDISCH_TAC “(\n:num. FST(f n :real#real)) --> l” THEN
936 REWRITE_TAC[SEQ] THEN DISCH_THEN(MP_TAC o SPEC “d / &2”) THEN
937 ASM_REWRITE_TAC[REAL_LT_HALF1] THEN
938 DISCH_THEN(X_CHOOSE_THEN “N1:num” (ASSUME_TAC o BETA_RULE)) THEN
939 DISCH_THEN(MP_TAC o SPEC “d / &2”) THEN ASM_REWRITE_TAC[REAL_LT_HALF1] THEN
940 DISCH_THEN(X_CHOOSE_THEN “N2:num” (ASSUME_TAC o BETA_RULE)) THEN
941 DISCH_THEN(MP_TAC o
942 SPECL [“FST((f:num->real#real) (N1 + N2))”,
943 “SND((f:num->real#real) (N1 + N2))”]) THEN
944 UNDISCH_TAC “!n:num. (SND(f n)) - (FST(f n)) = (b - a) / ((& 2) pow n)” THEN
945 DISCH_THEN(K ALL_TAC) THEN ASM_REWRITE_TAC[] THEN
946 MATCH_MP_TAC REAL_LET_TRANS THEN
947 EXISTS_TAC “abs(FST(f(N1 + N2:num)) - l) +
948 abs(SND(f(N1 + N2)) - l)” THEN
949 GEN_REWR_TAC (funpow 2 RAND_CONV) [GSYM REAL_HALF_DOUBLE] THEN
950 CONJ_TAC THENL
951 [GEN_REWR_TAC (RAND_CONV o LAND_CONV) [ABS_SUB]
952 THEN ASM_REWRITE_TAC[abs, REAL_SUB_LE] THEN
953 REWRITE_TAC[real_sub, GSYM REAL_ADD_ASSOC] THEN
954 REWRITE_TAC[(EQT_ELIM o AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))
955 “a + (b + (c + d)) = (d + a) + (c + b)”] THEN
956 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID, REAL_LE_REFL],
957 MATCH_MP_TAC REAL_LT_ADD2 THEN
958 CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
959 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD] THEN
960 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[LESS_EQ_ADD]]]
961QED
962
963(* moved here from integralTheory *)
964Theorem BOLZANO_LEMMA_ALT :
965 !P. (!a b c. a <= b /\ b <= c /\ P a b /\ P b c ==> P a c) /\
966 (!x. ?d. &0 < d /\ (!a b. a <= x /\ x <= b /\ b - a < d ==> P a b))
967 ==> !a b. a <= b ==> P a b
968Proof
969 GEN_TAC THEN MP_TAC(SPEC ``\(x:real,y:real). P x y :bool`` BOLZANO_LEMMA) THEN
970 CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN REWRITE_TAC[]
971QED
972
973(*---------------------------------------------------------------------------*)
974(* Define infinite sums *)
975(*---------------------------------------------------------------------------*)
976
977val _ = hide "sums";
978val sums = new_infixr_definition("sums",
979 “$sums f s = (\n. sum(0,n) f) --> s”,750);
980
981val _ = hide "summable";
982Definition summable[nocompute]:
983 summable f = ?s. f sums s
984End
985
986val _ = hide "suminf";
987Definition suminf[nocompute]:
988 suminf f = @s. f sums s
989End
990
991(* connection to real_topologyTheory *)
992Theorem sums_univ :
993 !(f :num -> real) (l :real). real_topology$sums f l univ(:num) <=> f sums l
994Proof
995 RW_TAC std_ss [sums, sums_def, dist, INTER_UNIV,
996 SEQ, LIM_SEQUENTIALLY]
997 >> EQ_TAC >> rpt STRIP_TAC
998 >| [ (* goal 1 (of 2) *)
999 Q.PAT_X_ASSUM `!e. 0 < e ==> P` (MP_TAC o (Q.SPEC `e`)) \\
1000 RW_TAC std_ss [] \\
1001 Q.EXISTS_TAC `SUC N` >> rpt STRIP_TAC \\
1002 Cases_on `n` >- fs [] \\
1003 REWRITE_TAC [GSYM sum_real] \\
1004 FIRST_X_ASSUM MATCH_MP_TAC >> rw [],
1005 (* goal 2 (of 2) *)
1006 Q.PAT_X_ASSUM `!e. 0 < e ==> P` (MP_TAC o (Q.SPEC `e`)) \\
1007 RW_TAC std_ss [] \\
1008 Q.EXISTS_TAC `N` >> rpt STRIP_TAC \\
1009 REWRITE_TAC [sum_real] \\
1010 FIRST_X_ASSUM MATCH_MP_TAC >> rw [] ]
1011QED
1012
1013(* NOTE: this indicates that ‘suminf = infsum univ(:num)’ *)
1014Theorem suminf_univ :
1015 !(f :num -> real). infsum univ(:num) f = seq$suminf f
1016Proof
1017 RW_TAC std_ss [suminf_def, suminf, sums_univ]
1018QED
1019
1020(* NOTE: this indicates that ‘summable = real_topology$summable univ(:num)’ *)
1021Theorem summable_univ :
1022 !(f :num -> real). real_topology$summable univ(:num) f <=> summable f
1023Proof
1024 RW_TAC std_ss [summable_def, summable, sums_univ]
1025QED
1026
1027(*---------------------------------------------------------------------------*)
1028(* If summable then it sums to the sum (!) *)
1029(*---------------------------------------------------------------------------*)
1030
1031Theorem SUM_SUMMABLE:
1032 !f l. f sums l ==> summable f
1033Proof
1034 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[summable] THEN
1035 EXISTS_TAC “l:real” THEN POP_ASSUM ACCEPT_TAC
1036QED
1037
1038Theorem SUMMABLE_SUM:
1039 !f. summable f ==> f sums (suminf f)
1040Proof
1041 GEN_TAC THEN REWRITE_TAC[summable, suminf] THEN
1042 DISCH_THEN(CHOOSE_THEN MP_TAC) THEN
1043 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN
1044 MATCH_ACCEPT_TAC SELECT_AX
1045QED
1046
1047(*---------------------------------------------------------------------------*)
1048(* And the sum is unique *)
1049(*---------------------------------------------------------------------------*)
1050
1051Theorem SUM_UNIQ:
1052 !f x. f sums x ==> (x = suminf f)
1053Proof
1054 REPEAT GEN_TAC THEN DISCH_TAC THEN
1055 SUBGOAL_THEN “summable f” MP_TAC THENL
1056 [REWRITE_TAC[summable] THEN EXISTS_TAC “x:real” THEN ASM_REWRITE_TAC[],
1057 DISCH_THEN(ASSUME_TAC o MATCH_MP SUMMABLE_SUM) THEN
1058 MATCH_MP_TAC SEQ_UNIQ THEN
1059 EXISTS_TAC “\n. sum(0,n) f” THEN ASM_REWRITE_TAC[GSYM sums]]
1060QED
1061
1062(*---------------------------------------------------------------------------*)
1063(* Series which is zero beyond a certain point *)
1064(*---------------------------------------------------------------------------*)
1065
1066Theorem SER_0:
1067 !f n. (!m. n <= m ==> (f(m) = &0)) ==>
1068 f sums (sum(0,n) f)
1069Proof
1070 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[sums, SEQ] THEN
1071 X_GEN_TAC “e:real” THEN DISCH_TAC THEN EXISTS_TAC “n:num” THEN
1072 X_GEN_TAC “m:num” THEN REWRITE_TAC[GREATER_EQ] THEN
1073 DISCH_THEN(X_CHOOSE_THEN “d:num” SUBST1_TAC o MATCH_MP LESS_EQUAL_ADD) THEN
1074 W(C SUBGOAL_THEN SUBST1_TAC o C (curry mk_eq) “&0” o rand o rator o snd) THEN
1075 ASM_REWRITE_TAC[] THEN REWRITE_TAC[ABS_ZERO, REAL_SUB_0] THEN
1076 BETA_TAC THEN REWRITE_TAC[GSYM SUM_TWO, REAL_ADD_RID_UNIQ] THEN
1077 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[GREATER_EQ] SUM_ZERO)) THEN
1078 MATCH_ACCEPT_TAC LESS_EQ_REFL
1079QED
1080
1081(*---------------------------------------------------------------------------*)
1082(* Summable series of positive terms has limit >(=) any partial sum *)
1083(*---------------------------------------------------------------------------*)
1084
1085Theorem SER_POS_LE:
1086 !f n. summable f /\ (!m. n <= m ==> &0 <= f(m))
1087 ==> sum(0,n) f <= suminf f
1088Proof
1089 REPEAT GEN_TAC THEN STRIP_TAC THEN
1090 FIRST_ASSUM(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN REWRITE_TAC[sums] THEN
1091 MP_TAC(SPEC “sum(0,n) f” SEQ_CONST) THEN
1092 GEN_REWR_TAC I [TAUT_CONV “a ==> b ==> c = a /\ b ==> c”] THEN
1093 MATCH_MP_TAC(REWRITE_RULE[TAUT_CONV “a /\ b /\ c ==> d = c ==> a /\ b ==> d”]
1094 SEQ_LE) THEN BETA_TAC THEN
1095 EXISTS_TAC “n:num” THEN X_GEN_TAC “m:num” THEN REWRITE_TAC[GREATER_EQ] THEN
1096 DISCH_THEN(X_CHOOSE_THEN “d:num” SUBST1_TAC o MATCH_MP LESS_EQUAL_ADD) THEN
1097 REWRITE_TAC[GSYM SUM_TWO, REAL_LE_ADDR] THEN
1098 MATCH_MP_TAC SUM_POS_GEN THEN FIRST_ASSUM MATCH_ACCEPT_TAC
1099QED
1100
1101Theorem SER_POS_LT:
1102 !f n. summable f /\ (!m. n <= m ==> &0 < f(m))
1103 ==> sum(0,n) f < suminf f
1104Proof
1105 REPEAT GEN_TAC THEN STRIP_TAC THEN
1106 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC “sum(0,n + 1) f” THEN
1107 CONJ_TAC THENL
1108 [REWRITE_TAC[GSYM SUM_TWO, REAL_LT_ADDR] THEN
1109 REWRITE_TAC[ONE, sum, REAL_ADD_LID, ADD_CLAUSES] THEN
1110 FIRST_ASSUM MATCH_MP_TAC THEN MATCH_ACCEPT_TAC LESS_EQ_REFL,
1111 MATCH_MP_TAC SER_POS_LE THEN ASM_REWRITE_TAC[] THEN
1112 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN
1113 FIRST_ASSUM MATCH_MP_TAC THEN
1114 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC “SUC n” THEN
1115 REWRITE_TAC[LESS_EQ_SUC_REFL] THEN ASM_REWRITE_TAC[ADD1]]
1116QED
1117
1118(*---------------------------------------------------------------------------*)
1119(* Theorems about grouping and offsetting (and *not* permuting) terms *)
1120(*---------------------------------------------------------------------------*)
1121
1122Theorem SER_GROUP:
1123 !f (k:num). summable f /\ 0 < k ==>
1124 (\n. sum(n * k,k) f) sums (suminf f)
1125Proof
1126 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1127 DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN
1128 REWRITE_TAC[sums, SEQ] THEN BETA_TAC THEN
1129 DISCH_THEN(fn t => X_GEN_TAC “e:real” THEN DISCH_THEN(MP_TAC o MATCH_MP t)) THEN
1130 REWRITE_TAC[GREATER_EQ] THEN DISCH_THEN(X_CHOOSE_TAC “N:num”) THEN
1131 REWRITE_TAC[SUM_GROUP] THEN EXISTS_TAC “N:num” THEN
1132 X_GEN_TAC “n:num” THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1133 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC “n:num” THEN
1134 ASM_REWRITE_TAC[] THEN UNDISCH_TAC “0 < k:num” THEN
1135 STRUCT_CASES_TAC(SPEC “k:num” num_CASES) THEN
1136 REWRITE_TAC[MULT_CLAUSES, LESS_EQ_ADD, LESS_EQ_0] THEN
1137 REWRITE_TAC[LESS_REFL]
1138QED
1139
1140Theorem SER_PAIR:
1141 !f. summable f ==> (\n. sum(2 * n,2) f) sums (suminf f)
1142Proof
1143 GEN_TAC THEN DISCH_THEN(MP_TAC o C CONJ (SPEC “1:num” LESS_0)) THEN
1144 REWRITE_TAC[SYM(num_CONV “2:num”)] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
1145 MATCH_ACCEPT_TAC SER_GROUP
1146QED
1147
1148Theorem SER_OFFSET:
1149 !f. summable f ==> !k. (\n. f(n + k)) sums (suminf f - sum(0,k) f)
1150Proof
1151 GEN_TAC THEN DISCH_THEN(curry op THEN GEN_TAC o MP_TAC o MATCH_MP SUMMABLE_SUM) THEN
1152 REWRITE_TAC[sums, SEQ] THEN
1153 DISCH_THEN(fn th => GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP th)) THEN
1154 BETA_TAC THEN REWRITE_TAC[GREATER_EQ] THEN DISCH_THEN(X_CHOOSE_TAC “N:num”) THEN
1155 EXISTS_TAC “N:num” THEN X_GEN_TAC “n:num” THEN DISCH_TAC THEN
1156 REWRITE_TAC[SUM_OFFSET] THEN
1157 REWRITE_TAC[real_sub, REAL_NEG_ADD, REAL_NEGNEG] THEN
1158 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM)
1159 “(a + b) + (c + d) = (b + d) + (a + c)”] THEN
1160 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID] THEN REWRITE_TAC[GSYM real_sub] THEN
1161 FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC LESS_EQ_TRANS THEN
1162 EXISTS_TAC “n:num” THEN ASM_REWRITE_TAC[LESS_EQ_ADD]
1163QED
1164
1165(*---------------------------------------------------------------------------*)
1166(* Similar version for pairing up terms *)
1167(*---------------------------------------------------------------------------*)
1168
1169Theorem SER_POS_LT_PAIR:
1170 !f n. summable f /\
1171 (!d. &0 < (f(n + (2 * d))) + f(n + ((2 * d) + 1)))
1172 ==> sum(0,n) f < suminf f
1173Proof
1174 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1175 DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN
1176 REWRITE_TAC[sums, SEQ] THEN BETA_TAC THEN
1177 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
1178 DISCH_THEN(MP_TAC o SPEC “f(n:num) + f(n + 1)”) THEN
1179 FIRST_ASSUM(MP_TAC o SPEC “0:num”) THEN
1180 REWRITE_TAC[ADD_CLAUSES, MULT_CLAUSES] THEN
1181 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1182 DISCH_THEN(X_CHOOSE_THEN “N:num” MP_TAC) THEN
1183 SUBGOAL_THEN “sum(0,n + 2) f <= sum(0,(2 * (SUC N)) + n) f”
1184 ASSUME_TAC THENL
1185 [SPEC_TAC(“N:num”,“N:num”) THEN INDUCT_TAC THENL
1186 [REWRITE_TAC[MULT_CLAUSES, ADD_CLAUSES] THEN
1187 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ADD_SYM] THEN
1188 MATCH_ACCEPT_TAC REAL_LE_REFL,
1189 ABBREV_TAC “M = SUC N” THEN
1190 REWRITE_TAC[MULT_CLAUSES] THEN
1191 REWRITE_TAC[TWO, ADD_CLAUSES] THEN
1192 REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[ADD_SYM] ADD1)] THEN
1193 REWRITE_TAC[SYM TWO] THEN REWRITE_TAC[ADD_CLAUSES] THEN
1194 GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [ADD1] THEN
1195 (* changed for new term nets.
1196 old: REWRITE_TAC[GSYM ADD_ASSOC, GSYM ADD1, SYM(num_CONV “2”)] *)
1197 REWRITE_TAC[GSYM ADD_ASSOC] THEN
1198 REWRITE_TAC [GSYM ADD1, SYM TWO] THEN
1199 MATCH_MP_TAC REAL_LE_TRANS THEN
1200 EXISTS_TAC “sum(0,(2 * M) + n) f” THEN
1201 ASM_REWRITE_TAC[] THEN REWRITE_TAC[sum] THEN
1202 REWRITE_TAC[GSYM REAL_ADD_ASSOC, REAL_LE_ADDR] THEN
1203 REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[ADD1] THEN
1204 REWRITE_TAC[GSYM ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
1205 REWRITE_TAC[GSYM ADD_ASSOC] THEN
1206 ONCE_REWRITE_TAC[SPEC “1:num” ADD_SYM] THEN
1207 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]],
1208 DISCH_THEN(MP_TAC o SPEC “(2 * SUC N) + n”) THEN
1209 W(C SUBGOAL_THEN (fn th => REWRITE_TAC[th])
1210 o funpow 2(fst o dest_imp) o snd)
1211 THENL
1212 [REWRITE_TAC[TWO, MULT_CLAUSES] THEN
1213 ONCE_REWRITE_TAC[AC(ADD_ASSOC,ADD_SYM)
1214 “(a + (b + c)) + d = b + (a + (c + d:num))”] THEN
1215 REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD], ALL_TAC] THEN
1216 SUBGOAL_THEN “suminf f + (f(n:num) + f(n + 1))
1217 <= sum(0,(2 * (SUC N)) + n) f”
1218 ASSUME_TAC THENL
1219 [MATCH_MP_TAC REAL_LE_TRANS THEN
1220 EXISTS_TAC “sum(0,n + 2) f” THEN ASM_REWRITE_TAC[] THEN
1221 MATCH_MP_TAC REAL_LE_TRANS THEN
1222 EXISTS_TAC “sum(0,n) f + (f(n:num) + f(n + 1))” THEN
1223 ASM_REWRITE_TAC[REAL_LE_RADD] THEN
1224 MATCH_MP_TAC REAL_EQ_IMP_LE THEN
1225 CONV_TAC(REDEPTH_CONV num_CONV) THEN
1226 REWRITE_TAC[ADD_CLAUSES, sum, REAL_ADD_ASSOC], ALL_TAC] THEN
1227 SUBGOAL_THEN “suminf f <= sum(0,(2 * (SUC N)) + n) f”
1228 ASSUME_TAC THENL
1229 [MATCH_MP_TAC REAL_LE_TRANS THEN
1230 EXISTS_TAC “suminf f + (f(n:num) + f(n + 1))” THEN
1231 ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_LE_ADDR] THEN
1232 MATCH_MP_TAC REAL_LT_IMP_LE THEN FIRST_ASSUM ACCEPT_TAC, ALL_TAC] THEN
1233 ASM_REWRITE_TAC[abs, REAL_SUB_LE] THEN
1234 REWRITE_TAC[REAL_LT_SUB_RADD] THEN
1235 GEN_REWR_TAC (funpow 2 RAND_CONV) [REAL_ADD_SYM]
1236 THEN ASM_REWRITE_TAC[REAL_NOT_LT]]
1237QED
1238
1239(*---------------------------------------------------------------------------*)
1240(* Prove a few composition formulas for series *)
1241(*---------------------------------------------------------------------------*)
1242
1243Theorem SER_ADD:
1244 !x x0 y y0. x sums x0 /\ y sums y0 ==> (\n. x(n) + y(n)) sums (x0 + y0)
1245Proof
1246 REPEAT GEN_TAC THEN REWRITE_TAC[sums, SUM_ADD] THEN
1247 CONV_TAC((RAND_CONV o EXACT_CONV)[X_BETA_CONV “n:num” “sum(0,n) x”]) THEN
1248 CONV_TAC((RAND_CONV o EXACT_CONV)[X_BETA_CONV “n:num” “sum(0,n) y”]) THEN
1249 MATCH_ACCEPT_TAC SEQ_ADD
1250QED
1251
1252Theorem SER_CMUL:
1253 !x x0 c. x sums x0 ==> (\n. c * x(n)) sums (c * x0)
1254Proof
1255 REPEAT GEN_TAC THEN REWRITE_TAC[sums, SUM_CMUL] THEN DISCH_TAC THEN
1256 CONV_TAC(EXACT_CONV[X_BETA_CONV “n:num” “sum(0,n) x”]) THEN
1257 CONV_TAC((RATOR_CONV o EXACT_CONV)[X_BETA_CONV “n:num” “c:real”]) THEN
1258 MATCH_MP_TAC SEQ_MUL THEN ASM_REWRITE_TAC[SEQ_CONST]
1259QED
1260
1261Theorem SER_NEG:
1262 !x x0. x sums x0 ==> (\n. ~(x n)) sums ~x0
1263Proof
1264 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_NEG_MINUS1] THEN
1265 MATCH_ACCEPT_TAC SER_CMUL
1266QED
1267
1268Theorem SER_SUB:
1269 !x x0 y y0. x sums x0 /\ y sums y0 ==> (\n. x(n) - y(n)) sums (x0 - y0)
1270Proof
1271 REPEAT GEN_TAC THEN DISCH_THEN(fn th => MP_TAC (MATCH_MP SER_ADD
1272 (CONJ (CONJUNCT1 th) (MATCH_MP SER_NEG (CONJUNCT2 th))))) THEN
1273 BETA_TAC THEN REWRITE_TAC[real_sub]
1274QED
1275
1276Theorem SER_CDIV:
1277 !x x0 c. x sums x0 ==> (\n. x(n) / c) sums (x0 / c)
1278Proof
1279 REPEAT GEN_TAC THEN REWRITE_TAC[real_div] THEN
1280 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1281 MATCH_ACCEPT_TAC SER_CMUL
1282QED
1283
1284(*---------------------------------------------------------------------------*)
1285(* Prove Cauchy-type criterion for convergence of series *)
1286(*---------------------------------------------------------------------------*)
1287
1288Theorem SER_CAUCHY:
1289 !f. summable f =
1290 !e. &0 < e ==> ?N. !m n. m >= N ==> abs(sum(m,n) f) < e
1291Proof
1292 GEN_TAC THEN REWRITE_TAC[summable, sums] THEN
1293 REWRITE_TAC[GSYM convergent] THEN
1294 REWRITE_TAC[GSYM SEQ_CAUCHY] THEN REWRITE_TAC[cauchy] THEN
1295 AP_TERM_TAC THEN ABS_TAC THEN REWRITE_TAC[GREATER_EQ] THEN BETA_TAC THEN
1296 REWRITE_TAC[TAUT_CONV “((a ==> b) = (a ==> c)) = a ==> (b = c)”] THEN
1297 DISCH_TAC THEN EQ_TAC THEN DISCH_THEN(X_CHOOSE_TAC “N:num”) THEN
1298 EXISTS_TAC “N:num” THEN REPEAT GEN_TAC THEN DISCH_TAC THENL
1299 [ONCE_REWRITE_TAC[SUM_DIFF] THEN
1300 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1301 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC “m:num” THEN
1302 ASM_REWRITE_TAC[LESS_EQ_ADD],
1303 DISJ_CASES_THEN MP_TAC (SPECL [“m:num”, “n:num”] LESS_EQ_CASES) THEN
1304 DISCH_THEN(X_CHOOSE_THEN “p:num” SUBST1_TAC o MATCH_MP LESS_EQUAL_ADD) THENL
1305 [ONCE_REWRITE_TAC[ABS_SUB], ALL_TAC] THEN
1306 REWRITE_TAC[GSYM SUM_DIFF] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1307 ASM_REWRITE_TAC[]]
1308QED
1309
1310(*---------------------------------------------------------------------------*)
1311(* Show that if a series converges, the terms tend to 0 *)
1312(*---------------------------------------------------------------------------*)
1313
1314Theorem SER_ZERO:
1315 !f. summable f ==> f --> &0
1316Proof
1317 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[SEQ] THEN
1318 X_GEN_TAC “e:real” THEN DISCH_TAC THEN
1319 UNDISCH_TAC “summable f” THEN REWRITE_TAC[SER_CAUCHY] THEN
1320 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o MATCH_MP th)) THEN
1321 DISCH_THEN(X_CHOOSE_THEN “N:num” MP_TAC) THEN
1322 DISCH_THEN(curry op THEN (EXISTS_TAC “N:num” THEN X_GEN_TAC “n:num” THEN DISCH_TAC)
1323 o MP_TAC) THEN DISCH_THEN(MP_TAC o SPECL [“n:num”, “SUC 0”]) THEN
1324 ASM_REWRITE_TAC[sum, REAL_SUB_RZERO, REAL_ADD_LID, ADD_CLAUSES]
1325QED
1326
1327(*---------------------------------------------------------------------------*)
1328(* Now prove the comparison test *)
1329(*---------------------------------------------------------------------------*)
1330
1331Theorem SER_COMPAR:
1332 !f g. (?N. !n. n >= N ==> abs(f(n)) <= g(n)) /\ summable g ==>
1333 summable f
1334Proof
1335 REPEAT GEN_TAC THEN REWRITE_TAC[SER_CAUCHY, GREATER_EQ] THEN
1336 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC “N1:num”) MP_TAC) THEN
1337 REWRITE_TAC[SER_CAUCHY, GREATER_EQ] THEN DISCH_TAC THEN
1338 X_GEN_TAC “e:real” THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1339 DISCH_THEN(X_CHOOSE_TAC “N2:num”) THEN EXISTS_TAC “N1 + N2:num” THEN
1340 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
1341 EXISTS_TAC “sum(m,n)(\k. abs(f k))” THEN REWRITE_TAC[ABS_SUM] THEN
1342 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “sum(m,n) g” THEN CONJ_TAC THENL
1343 [MATCH_MP_TAC SUM_LE THEN BETA_TAC THEN
1344 X_GEN_TAC “p:num” THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1345 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC “m:num” THEN
1346 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LESS_EQ_TRANS THEN
1347 EXISTS_TAC “N1 + N2:num” THEN ASM_REWRITE_TAC[LESS_EQ_ADD], ALL_TAC] THEN
1348 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “abs(sum(m,n) g)” THEN
1349 REWRITE_TAC[ABS_LE] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1350 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC “N1 + N2:num” THEN
1351 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
1352 REWRITE_TAC[LESS_EQ_ADD]
1353QED
1354
1355(*---------------------------------------------------------------------------*)
1356(* And a similar version for absolute convergence *)
1357(*---------------------------------------------------------------------------*)
1358
1359Theorem SER_COMPARA:
1360 !f g. (?N. !n. n >= N ==> abs(f(n)) <= g(n)) /\ summable g ==>
1361 summable (\k. abs(f k))
1362Proof
1363 REPEAT GEN_TAC THEN SUBGOAL_THEN “!n. abs(f(n)) = abs((\k:num. abs(f k)) n)”
1364 (fn th => GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [th]) THENL
1365 [GEN_TAC THEN BETA_TAC THEN REWRITE_TAC[ABS_ABS],
1366 MATCH_ACCEPT_TAC SER_COMPAR]
1367QED
1368
1369(*---------------------------------------------------------------------------*)
1370(* Limit comparison property for series *)
1371(*---------------------------------------------------------------------------*)
1372
1373Theorem SER_LE:
1374 !f g. (!n. f(n) <= g(n)) /\ summable f /\ summable g
1375 ==> suminf f <= suminf g
1376Proof
1377 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1378 DISCH_THEN(CONJUNCTS_THEN (fn th => ASSUME_TAC th THEN ASSUME_TAC
1379 (REWRITE_RULE[sums] (MATCH_MP SUMMABLE_SUM th)))) THEN
1380 MATCH_MP_TAC SEQ_LE THEN REWRITE_TAC[CONJ_ASSOC] THEN
1381 MAP_EVERY EXISTS_TAC [“\n. sum(0,n) f”, “\n. sum(0,n) g”] THEN CONJ_TAC THENL
1382 [REWRITE_TAC[GSYM sums] THEN CONJ_TAC THEN
1383 MATCH_MP_TAC SUMMABLE_SUM THEN FIRST_ASSUM ACCEPT_TAC,
1384 EXISTS_TAC “0:num” THEN REWRITE_TAC[GREATER_EQ, ZERO_LESS_EQ] THEN
1385 GEN_TAC THEN BETA_TAC THEN MATCH_MP_TAC SUM_LE THEN
1386 GEN_TAC THEN ASM_REWRITE_TAC[ZERO_LESS_EQ]]
1387QED
1388
1389Theorem SER_LE2:
1390 !f g. (!n. abs(f n) <= g(n)) /\ summable g ==>
1391 summable f /\ suminf f <= suminf g
1392Proof
1393 REPEAT GEN_TAC THEN STRIP_TAC THEN
1394 SUBGOAL_THEN “summable f” ASSUME_TAC THENL
1395 [MATCH_MP_TAC SER_COMPAR THEN EXISTS_TAC “g:num->real” THEN
1396 ASM_REWRITE_TAC[], ASM_REWRITE_TAC[]] THEN
1397 MATCH_MP_TAC SER_LE THEN ASM_REWRITE_TAC[] THEN
1398 X_GEN_TAC “n:num” THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1399 EXISTS_TAC “abs(f(n:num))” THEN ASM_REWRITE_TAC[ABS_LE]
1400QED
1401
1402(*---------------------------------------------------------------------------*)
1403(* Show that absolute convergence implies normal convergence *)
1404(*---------------------------------------------------------------------------*)
1405
1406Theorem SER_ACONV:
1407 !f. summable (\n. abs(f n)) ==> summable f
1408Proof
1409 GEN_TAC THEN REWRITE_TAC[SER_CAUCHY] THEN REWRITE_TAC[SUM_ABS] THEN
1410 DISCH_THEN(curry op THEN (X_GEN_TAC “e:real” THEN DISCH_TAC) o MP_TAC) THEN
1411 DISCH_THEN(IMP_RES_THEN (X_CHOOSE_TAC “N:num”)) THEN
1412 EXISTS_TAC “N:num” THEN REPEAT GEN_TAC THEN
1413 DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN MATCH_MP_TAC REAL_LET_TRANS THEN
1414 EXISTS_TAC “sum(m,n)(\m. abs(f m))” THEN ASM_REWRITE_TAC[ABS_SUM]
1415QED
1416
1417(*---------------------------------------------------------------------------*)
1418(* Absolute value of series *)
1419(*---------------------------------------------------------------------------*)
1420
1421Theorem SER_ABS:
1422 !f. summable(\n. abs(f n)) ==> abs(suminf f) <= suminf(\n. abs(f n))
1423Proof
1424 GEN_TAC THEN DISCH_TAC THEN
1425 FIRST_ASSUM(MP_TAC o MATCH_MP SUMMABLE_SUM o MATCH_MP SER_ACONV) THEN
1426 POP_ASSUM(MP_TAC o MATCH_MP SUMMABLE_SUM) THEN
1427 REWRITE_TAC[sums] THEN DISCH_TAC THEN
1428 DISCH_THEN(ASSUME_TAC o BETA_RULE o MATCH_MP SEQ_ABS_IMP) THEN
1429 MATCH_MP_TAC SEQ_LE THEN MAP_EVERY EXISTS_TAC
1430 [“\n. abs(sum(0,n)f)”, “\n. sum(0,n)(\n. abs(f n))”] THEN
1431 ASM_REWRITE_TAC[] THEN EXISTS_TAC “0:num” THEN X_GEN_TAC “n:num” THEN
1432 DISCH_THEN(K ALL_TAC) THEN BETA_TAC THEN MATCH_ACCEPT_TAC SUM_ABS_LE
1433QED
1434
1435(*---------------------------------------------------------------------------*)
1436(* Prove sum of geometric progression (useful for comparison) *)
1437(*---------------------------------------------------------------------------*)
1438
1439Theorem GP_FINITE:
1440 !x. ~(x = &1) ==>
1441 !n. (sum(0,n) (\n. x pow n) = ((x pow n) - &1) / (x - &1))
1442Proof
1443 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THENL
1444 [REWRITE_TAC[sum, pow, REAL_SUB_REFL, REAL_DIV_LZERO],
1445 REWRITE_TAC[sum, pow] THEN BETA_TAC THEN
1446 ASM_REWRITE_TAC[ADD_CLAUSES] THEN
1447 SUBGOAL_THEN “~(x - &1 = &0)” ASSUME_TAC THEN
1448 ASM_REWRITE_TAC[REAL_SUB_0] THEN
1449 MP_TAC(GENL [“p:real”, “q:real”]
1450 (SPECL [“p:real”, “q:real”, “x - &1”] REAL_EQ_RMUL)) THEN
1451 ASM_REWRITE_TAC[] THEN DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM th]) THEN
1452 REWRITE_TAC[REAL_RDISTRIB] THEN SUBGOAL_THEN
1453 “!p. (p / (x - &1)) * (x - &1) = p” (fn th => REWRITE_TAC[th]) THENL
1454 [GEN_TAC THEN MATCH_MP_TAC REAL_DIV_RMUL THEN ASM_REWRITE_TAC[], ALL_TAC]
1455 THEN REWRITE_TAC[REAL_SUB_LDISTRIB] THEN REWRITE_TAC[real_sub] THEN
1456 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM)
1457 “(a + b) + (c + d) = (c + b) + (d + a)”] THEN
1458 REWRITE_TAC[REAL_MUL_RID, REAL_ADD_LINV, REAL_ADD_RID] THEN
1459 AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_MUL_SYM]
1460QED
1461
1462Theorem GP:
1463 !x. abs(x) < &1 ==> (\n. x pow n) sums inv(&1 - x)
1464Proof
1465 GEN_TAC THEN ASM_CASES_TAC “x = &1” THEN
1466 ASM_REWRITE_TAC[ABS_1, REAL_LT_REFL] THEN DISCH_TAC THEN
1467 REWRITE_TAC[sums] THEN
1468 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP GP_FINITE th]) THEN
1469 REWRITE_TAC[REAL_INV_1OVER] THEN REWRITE_TAC[real_div] THEN
1470 GEN_REWR_TAC (LAND_CONV o ABS_CONV) [GSYM REAL_NEG_MUL2] THEN
1471 SUBGOAL_THEN “~(x - &1 = &0)” (fn t =>REWRITE_TAC[MATCH_MP REAL_NEG_INV t]) THENL
1472 [ASM_REWRITE_TAC[REAL_SUB_0], ALL_TAC] THEN
1473 REWRITE_TAC[REAL_NEG_SUB, GSYM real_div] THEN
1474 CONV_TAC(EXACT_CONV[X_BETA_CONV “n:num” “&1 - (x pow n)”]) THEN
1475 CONV_TAC(EXACT_CONV[X_BETA_CONV “n:num” “&1 - x”]) THEN
1476 MATCH_MP_TAC SEQ_DIV THEN BETA_TAC THEN REWRITE_TAC[SEQ_CONST] THEN
1477 REWRITE_TAC[REAL_SUB_0] THEN CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
1478 ASM_REWRITE_TAC[] THEN
1479 GEN_REWR_TAC RAND_CONV [GSYM REAL_SUB_RZERO]
1480 THEN CONV_TAC(EXACT_CONV[X_BETA_CONV “n:num” “x pow n”]) THEN
1481 CONV_TAC(EXACT_CONV[X_BETA_CONV “n:num” “&1”]) THEN
1482 MATCH_MP_TAC SEQ_SUB THEN BETA_TAC THEN REWRITE_TAC[SEQ_CONST] THEN
1483 MATCH_MP_TAC SEQ_POWER THEN FIRST_ASSUM ACCEPT_TAC
1484QED
1485
1486(*---------------------------------------------------------------------------*)
1487(* Now prove the ratio test *)
1488(*---------------------------------------------------------------------------*)
1489
1490Theorem ABS_NEG_LEMMA:
1491 !c. c <= &0 ==> !x y. abs(x) <= c * abs(y) ==> (x = &0)
1492Proof
1493 GEN_TAC THEN REWRITE_TAC[GSYM REAL_NEG_GE0] THEN DISCH_TAC THEN
1494 REPEAT GEN_TAC THEN MP_TAC(Q.SPECL [‘~c’, ‘abs(y)’] REAL_LE_MUL) THEN
1495 ASM_REWRITE_TAC[ABS_POS, GSYM REAL_NEG_LMUL, REAL_NEG_GE0] THEN
1496 DISCH_THEN(fn th => DISCH_THEN(MP_TAC o C CONJ th)) THEN
1497 DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_TRANS) THEN CONV_TAC CONTRAPOS_CONV THEN
1498 REWRITE_TAC[ABS_NZ, REAL_NOT_LE]
1499QED
1500
1501Theorem SER_RATIO:
1502 !f c (N:num).
1503 c < &1 /\ (!n. n >= N ==> abs(f(SUC n)) <= c * abs(f(n)))
1504 ==>
1505 summable f
1506Proof
1507 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
1508 DISJ_CASES_TAC (SPECL [“c:real”, “&0”] REAL_LET_TOTAL) THENL
1509 [REWRITE_TAC[SER_CAUCHY] THEN X_GEN_TAC “e:real” THEN DISCH_TAC THEN
1510 SUBGOAL_THEN “!n. n >= N ==> (f(SUC n) = &0)” ASSUME_TAC THENL
1511 [GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1512 MATCH_MP_TAC ABS_NEG_LEMMA THEN FIRST_ASSUM ACCEPT_TAC, ALL_TAC] THEN
1513 SUBGOAL_THEN “!n. n >= SUC N ==> (f(n) = &0)” ASSUME_TAC THENL
1514 [GEN_TAC THEN STRUCT_CASES_TAC(SPEC “n:num” num_CASES) THENL
1515 [REWRITE_TAC[GREATER_EQ] THEN DISCH_THEN(MP_TAC o MATCH_MP OR_LESS) THEN
1516 REWRITE_TAC[NOT_LESS_0],
1517 REWRITE_TAC[GREATER_EQ, LESS_EQ_MONO] THEN
1518 ASM_REWRITE_TAC[GSYM GREATER_EQ]], ALL_TAC] THEN
1519 EXISTS_TAC “SUC N” THEN FIRST_ASSUM(ASSUME_TAC o MATCH_MP SUM_ZERO) THEN
1520 REPEAT GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN (fn th => REWRITE_TAC[th])) THEN
1521 ASM_REWRITE_TAC[ABS_0],
1522
1523 MATCH_MP_TAC SER_COMPAR THEN
1524 EXISTS_TAC “\n:num. (abs(f N) / c pow N) * (c pow n)” THEN
1525 CONJ_TAC THENL
1526 [EXISTS_TAC “N:num” THEN X_GEN_TAC “n:num” THEN
1527 REWRITE_TAC[GREATER_EQ] THEN
1528 DISCH_THEN(X_CHOOSE_THEN “d:num” SUBST1_TAC o MATCH_MP LESS_EQUAL_ADD)
1529 THEN BETA_TAC THEN REWRITE_TAC[POW_ADD] THEN REWRITE_TAC[real_div] THEN
1530 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
1531 “(a * b) * (c * d) = (a * d) * (b * c)”] THEN
1532 SUBGOAL_THEN “~(c pow N = &0)”
1533 (fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th, REAL_MUL_RID]) THENL
1534 [MATCH_MP_TAC POW_NZ THEN CONV_TAC(RAND_CONV SYM_CONV) THEN
1535 MATCH_MP_TAC REAL_LT_IMP_NE THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
1536 SPEC_TAC(“d:num”,“d:num”) THEN INDUCT_TAC THEN
1537 REWRITE_TAC[pow, ADD_CLAUSES, REAL_MUL_RID, REAL_LE_REFL] THEN
1538 MATCH_MP_TAC REAL_LE_TRANS THEN
1539 EXISTS_TAC “c * abs(f((N:num) + d))” THEN CONJ_TAC THENL
1540 [FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[GREATER_EQ, LESS_EQ_ADD],
1541 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
1542 “a * (b * c) = b * (a * c)”] THEN
1543 FIRST_ASSUM(fn th => ASM_REWRITE_TAC[MATCH_MP REAL_LE_LMUL th])],
1544
1545 REWRITE_TAC[summable] THEN
1546 EXISTS_TAC “(abs(f(N:num)) / (c pow N)) * inv(&1 - c)” THEN
1547 MATCH_MP_TAC SER_CMUL THEN
1548 MATCH_MP_TAC(CONV_RULE(ONCE_DEPTH_CONV ETA_CONV) GP) THEN
1549 ASSUME_TAC(MATCH_MP REAL_LT_IMP_LE (ASSUME “&0 < c”)) THEN
1550 ASM_REWRITE_TAC[abs]]]
1551QED
1552
1553(*---------------------------------------------------------------------------*)
1554(* Useful lemmas for proving inequalities of limits *)
1555(*---------------------------------------------------------------------------*)
1556
1557Theorem LE_SEQ_IMP_LE_LIM:
1558 !x y f. (!n. x <= f n) /\ f --> y ==> x <= y
1559Proof
1560 RW_TAC boolSimps.bool_ss [SEQ]
1561 THEN MATCH_MP_TAC REAL_LE_EPSILON
1562 THEN RW_TAC boolSimps.bool_ss []
1563 THEN Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`)
1564 THEN RW_TAC boolSimps.bool_ss []
1565 THEN POP_ASSUM (MP_TAC o Q.SPEC `N`)
1566 THEN Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`)
1567 THEN RW_TAC boolSimps.bool_ss
1568 [GREATER_EQ, LESS_EQ_REFL, abs, REAL_LE_SUB_LADD, REAL_ADD_LID]
1569 THEN simpLib.FULL_SIMP_TAC boolSimps.bool_ss
1570 [REAL_NOT_LE, REAL_NEG_SUB, REAL_LT_SUB_RADD]
1571 THEN PROVE_TAC [REAL_LET_TRANS, REAL_LT_ADDR, REAL_LTE_TRANS, REAL_LE_TRANS,
1572 REAL_LT_LE, REAL_ADD_SYM]
1573QED
1574
1575Theorem SEQ_LE_IMP_LIM_LE:
1576 !x y f. (!n. f n <= x) /\ f --> y ==> y <= x
1577Proof
1578 RW_TAC boolSimps.bool_ss [SEQ]
1579 THEN MATCH_MP_TAC REAL_LE_EPSILON
1580 THEN RW_TAC boolSimps.bool_ss []
1581 THEN Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`)
1582 THEN RW_TAC boolSimps.bool_ss []
1583 THEN POP_ASSUM (MP_TAC o Q.SPEC `N`)
1584 THEN Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`)
1585 THEN (RW_TAC boolSimps.bool_ss
1586 [GREATER_EQ, LESS_EQ_REFL, abs, REAL_LE_SUB_LADD, REAL_ADD_LID]
1587 THEN simpLib.FULL_SIMP_TAC boolSimps.bool_ss
1588 [REAL_NOT_LE, REAL_NEG_SUB, REAL_LT_SUB_RADD])
1589 THENL [MATCH_MP_TAC REAL_LE_TRANS
1590 THEN Q.EXISTS_TAC `x`
1591 THEN (CONJ_TAC THEN1 PROVE_TAC [REAL_LE_TRANS])
1592 THEN PROVE_TAC [REAL_LE_ADDR, REAL_LT_LE],
1593 MATCH_MP_TAC REAL_LE_TRANS
1594 THEN Q.EXISTS_TAC `f N + e`
1595 THEN (CONJ_TAC THEN1 PROVE_TAC [REAL_LT_LE, REAL_ADD_SYM])
1596 THEN PROVE_TAC [REAL_LE_ADD2, REAL_LE_REFL]]
1597QED
1598
1599Theorem SEQ_MONO_LE:
1600 !f x n. (!n. f n <= f (n + 1)) /\ f --> x ==> f n <= x
1601Proof
1602 RW_TAC boolSimps.bool_ss [SEQ]
1603 THEN MATCH_MP_TAC REAL_LE_EPSILON
1604 THEN RW_TAC boolSimps.bool_ss []
1605 THEN Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`)
1606 THEN RW_TAC boolSimps.bool_ss [GREATER_EQ]
1607 THEN MP_TAC (Q.SPECL [`N`, `n`] LESS_EQ_CASES)
1608 THEN (STRIP_TAC
1609 THEN1 (Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n`)
1610 THEN RW_TAC boolSimps.bool_ss
1611 [abs, REAL_LE_SUB_LADD, REAL_LT_SUB_RADD, REAL_ADD_LID,
1612 REAL_NEG_SUB]
1613 THENL [PROVE_TAC [REAL_LT_LE, REAL_ADD_SYM],
1614 simpLib.FULL_SIMP_TAC boolSimps.bool_ss [REAL_NOT_LE]
1615 THEN MATCH_MP_TAC REAL_LE_TRANS
1616 THEN Q.EXISTS_TAC `x`
1617 THEN PROVE_TAC [REAL_LT_LE, REAL_LE_ADDR]]))
1618 THEN (SUFF_TAC ``!i : num. f (N - i) <= x + (e : real)``
1619 THEN1 PROVE_TAC [LESS_EQUAL_DIFF])
1620 THEN numLib.INDUCT_TAC
1621 THENL [Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`)
1622 THEN RW_TAC boolSimps.bool_ss [abs, LESS_EQ_REFL, SUB_0]
1623 THEN simpLib.FULL_SIMP_TAC boolSimps.bool_ss
1624 [REAL_LT_SUB_RADD, REAL_NEG_SUB, REAL_NOT_LE, REAL_ADD_LID,
1625 REAL_LE_SUB_LADD]
1626 THEN PROVE_TAC
1627 [REAL_LT_LE, REAL_ADD_SYM, REAL_LE_TRANS, REAL_LE_ADDR],
1628 MP_TAC (numLib.ARITH_PROVE
1629 ``(N - i = N - SUC i) \/ (N - i = (N - SUC i) + 1)``)
1630 THEN PROVE_TAC [REAL_LE_REFL, REAL_LE_TRANS]]
1631QED
1632
1633Theorem SEQ_LE_MONO:
1634 !f x n. (!n. f (n + 1) <= f n) /\ f --> x ==> x <= f n
1635Proof
1636 REPEAT GEN_TAC
1637 THEN MP_TAC (Q.SPECL [`\n. ~f n`, `~x`, `n`] SEQ_MONO_LE)
1638 THEN RW_TAC boolSimps.bool_ss [GSYM SEQ_NEG, REAL_LE_NEG]
1639QED
1640
1641(* ****************************************************** *)
1642(* Useful Theorems on Real Sequences from util_probTheory *)
1643(* ****************************************************** *)
1644
1645Definition mono_increasing_def:
1646 mono_increasing (f:num->real) = !m n. m <= n ==> f m <= f n
1647End
1648
1649Theorem mono_increasing_suc: !(f:num->real). mono_increasing f <=> !n. f n <= f (SUC n)
1650Proof
1651 RW_TAC std_ss [mono_increasing_def]
1652 >> EQ_TAC
1653 >- RW_TAC real_ss []
1654 >> RW_TAC std_ss []
1655 >> Know `?d. n = m + d` >- PROVE_TAC [LESS_EQ_EXISTS]
1656 >> RW_TAC std_ss []
1657 >> Induct_on `d` >- RW_TAC real_ss []
1658 >> RW_TAC std_ss []
1659 >> Q.PAT_X_ASSUM `!n. f n <= f (SUC n)` (MP_TAC o Q.SPEC `m + d`)
1660 >> METIS_TAC [REAL_LE_TRANS, ADD_CLAUSES, LESS_EQ_ADD]
1661QED
1662
1663Definition mono_decreasing_def:
1664 mono_decreasing (f:num->real) = !m n. m <= n ==> f n <= f m
1665End
1666
1667Theorem mono_decreasing_suc: !(f:num->real). mono_decreasing f <=> !n. f (SUC n) <= f n
1668Proof
1669 RW_TAC std_ss [mono_decreasing_def]
1670 >> EQ_TAC
1671 >- RW_TAC real_ss []
1672 >> RW_TAC std_ss []
1673 >> Know `?d. n = m + d` >- PROVE_TAC [LESS_EQ_EXISTS]
1674 >> RW_TAC std_ss []
1675 >> Induct_on `d` >- RW_TAC real_ss []
1676 >> RW_TAC std_ss []
1677 >> Q.PAT_X_ASSUM `!n. f (SUC n) <= f n` (MP_TAC o Q.SPEC `m + d`)
1678 >> METIS_TAC [REAL_LE_TRANS, ADD_CLAUSES, LESS_EQ_ADD]
1679QED
1680
1681Theorem mono_increasing_converges_to_sup:
1682 !f r. mono_increasing f /\ f --> r ==>
1683 (r = sup (IMAGE f UNIV))
1684Proof
1685 RW_TAC std_ss [mono_increasing_def]
1686 >> Suff `f --> sup (IMAGE f UNIV)`
1687 >- METIS_TAC [SEQ_UNIQ]
1688 >> RW_TAC std_ss [SEQ]
1689 >> (MP_TAC o Q.ISPECL [`IMAGE (f:num->real) UNIV`,`e:real/2`]) SUP_EPSILON
1690 >> SIMP_TAC std_ss [REAL_LT_HALF1]
1691 >> `!y x z. IMAGE f UNIV x = x IN IMAGE f UNIV` by RW_TAC std_ss [IN_DEF]
1692 >> POP_ORW
1693 >> Know `(?z. !x. x IN IMAGE f UNIV ==> x <= z)`
1694 >- (Q.EXISTS_TAC `r` >> RW_TAC std_ss [IN_IMAGE, IN_UNIV]
1695 >> MATCH_MP_TAC SEQ_MONO_LE
1696 >> RW_TAC std_ss [DECIDE ``!n:num. n <= n + 1``])
1697 >> SIMP_TAC std_ss [] >> STRIP_TAC >> POP_ASSUM (K ALL_TAC)
1698 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV, GSYM ABS_BETWEEN, GREATER_EQ]
1699 >> Q.EXISTS_TAC `x'`
1700 >> RW_TAC std_ss [REAL_LT_SUB_RADD]
1701 >- (MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `f x' + e / 2`
1702 >> RW_TAC std_ss [] >> MATCH_MP_TAC REAL_LET_TRANS
1703 >> Q.EXISTS_TAC `f n + e / 2` >> RW_TAC std_ss [REAL_LE_ADD2, REAL_LE_REFL]
1704 >> MATCH_MP_TAC REAL_LT_IADD >> RW_TAC std_ss [REAL_LT_HALF2])
1705 >> MATCH_MP_TAC REAL_LET_TRANS >> Q.EXISTS_TAC `sup (IMAGE f UNIV)`
1706 >> RW_TAC std_ss [REAL_LT_ADDR]
1707 >> Suff `!y. (\y. y IN IMAGE f UNIV) y ==> y <= sup (IMAGE f UNIV)`
1708 >- METIS_TAC [IN_IMAGE, IN_UNIV]
1709 >> SIMP_TAC std_ss [IN_DEF]
1710 >> MATCH_MP_TAC REAL_SUP_UBOUND_LE
1711 >> `!y x z. IMAGE f UNIV x = x IN IMAGE f UNIV` by RW_TAC std_ss [IN_DEF]
1712 >> POP_ORW
1713 >> RW_TAC std_ss [IN_IMAGE, IN_UNIV]
1714 >> Q.EXISTS_TAC `r`
1715 >> RW_TAC std_ss []
1716 >> MATCH_MP_TAC SEQ_MONO_LE
1717 >> RW_TAC std_ss [DECIDE ``!n:num. n <= n + 1``]
1718QED
1719
1720Theorem INCREASING_SEQ:
1721 !f l.
1722 (!n. f n <= f (SUC n)) /\
1723 (!n. f n <= l) /\
1724 (!e. 0 < e ==> ?n. l < f n + e) ==>
1725 f --> l
1726Proof
1727 RW_TAC std_ss [SEQ, GREATER_EQ]
1728 >> Q.PAT_X_ASSUM `!e. P e` (MP_TAC o Q.SPEC `e`)
1729 >> RW_TAC std_ss []
1730 >> Q.EXISTS_TAC `n`
1731 >> ONCE_REWRITE_TAC [ABS_SUB]
1732 >> REVERSE (RW_TAC std_ss [abs])
1733 >- (Q.PAT_X_ASSUM `~x` MP_TAC
1734 >> Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n'`)
1735 >> REAL_ARITH_TAC)
1736 >> Know `?d. n' = n + d` >- PROVE_TAC [LESS_EQ_EXISTS]
1737 >> RW_TAC std_ss []
1738 >> Suff `l < f (n + d) + e` >- REAL_ARITH_TAC
1739 >> NTAC 2 (POP_ASSUM K_TAC)
1740 >> Induct_on `d` >- RW_TAC arith_ss []
1741 >> RW_TAC std_ss [ADD_CLAUSES]
1742 >> Q.PAT_X_ASSUM `!n. f n <= f (SUC n)` (MP_TAC o Q.SPEC `n + d`)
1743 >> POP_ASSUM MP_TAC
1744 >> REAL_ARITH_TAC
1745QED
1746
1747Theorem X_LE_MAX[local] = cj 1 MAX_LE
1748Theorem MAX_LE_X[local] = cj 2 MAX_LE
1749
1750Theorem SEQ_SANDWICH:
1751 !f g h l.
1752 f --> l /\ h --> l /\ (!n. f n <= g n /\ g n <= h n) ==> g --> l
1753Proof
1754 RW_TAC std_ss [SEQ, GREATER_EQ]
1755 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `e`)
1756 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `e`)
1757 >> RW_TAC std_ss []
1758 >> Q.EXISTS_TAC `MAX N N'`
1759 >> RW_TAC std_ss [MAX_LE_X]
1760 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `n`)
1761 >> Q.PAT_X_ASSUM `!e. P e ==> Q e` (MP_TAC o Q.SPEC `n`)
1762 >> RW_TAC std_ss []
1763 >> REPEAT (POP_ASSUM MP_TAC)
1764 >> DISCH_THEN (MP_TAC o Q.SPEC `n`)
1765 >> RW_TAC std_ss [abs]
1766 >> REPEAT (POP_ASSUM MP_TAC)
1767 >> REAL_ARITH_TAC
1768QED
1769
1770Theorem SER_POS:
1771 !f. summable f /\ (!n. 0 <= f n) ==> 0 <= suminf f
1772Proof
1773 RW_TAC std_ss []
1774 >> MP_TAC (Q.SPECL [`f`, `0`] SER_POS_LE)
1775 >> RW_TAC std_ss [sum]
1776QED
1777
1778Theorem SER_POS_MONO:
1779 !f. (!n. 0 <= f n) ==> mono (\n. sum (0, n) f)
1780Proof
1781 RW_TAC std_ss [mono]
1782 >> DISJ1_TAC
1783 >> HO_MATCH_MP_TAC TRIANGLE_2D_NUM
1784 >> Induct >- RW_TAC arith_ss [REAL_LE_REFL]
1785 >> RW_TAC std_ss [ADD_CLAUSES]
1786 >> MATCH_MP_TAC REAL_LE_TRANS
1787 >> Q.EXISTS_TAC `sum (0, d + n) f`
1788 >> RW_TAC real_ss [sum]
1789 >> Q.PAT_X_ASSUM `!n. 0 <= f n` (MP_TAC o Q.SPEC `d + n`)
1790 >> REAL_ARITH_TAC
1791QED
1792
1793Theorem POS_SUMMABLE:
1794 !f. (!n. 0 <= f n) /\ (?x. !n. sum (0, n) f <= x) ==> summable f
1795Proof
1796 RW_TAC std_ss [summable, sums, GSYM convergent]
1797 >> MATCH_MP_TAC SEQ_BCONV
1798 >> RW_TAC std_ss [SER_POS_MONO, netsTheory.MR1_BOUNDED]
1799 >> Q.EXISTS_TAC `x + 1`
1800 >> Q.EXISTS_TAC `N`
1801 >> RW_TAC arith_ss []
1802 >> RW_TAC std_ss [abs, SUM_POS]
1803 >> Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `n`)
1804 >> REAL_ARITH_TAC
1805QED
1806
1807Theorem SUMMABLE_LE:
1808 !f x. summable f /\ (!n. sum (0, n) f <= x) ==> suminf f <= x
1809Proof
1810 Strip
1811 >> Suff `0 < suminf f - x ==> F` >- REAL_ARITH_TAC
1812 >> Strip
1813 >> Know `(\n. sum (0, n) f) --> suminf f`
1814 >- RW_TAC std_ss [GSYM sums, SUMMABLE_SUM]
1815 >> RW_TAC std_ss [SEQ]
1816 >> Q.EXISTS_TAC `suminf f - x`
1817 >> RW_TAC std_ss []
1818 >> Q.EXISTS_TAC `N`
1819 >> Q.PAT_X_ASSUM `!n. P n` (MP_TAC o Q.SPEC `N`)
1820 >> RW_TAC real_ss []
1821 >> ONCE_REWRITE_TAC [ABS_SUB]
1822 >> Know `0 <= suminf f - sum (0, N) f`
1823 >- (rpt (POP_ASSUM MP_TAC)
1824 >> REAL_ARITH_TAC)
1825 >> RW_TAC std_ss [abs]
1826 >> rpt (POP_ASSUM MP_TAC)
1827 >> REAL_ARITH_TAC
1828QED
1829
1830Theorem SUMS_EQ:
1831 !f x. f sums x = summable f /\ (suminf f = x)
1832Proof
1833 PROVE_TAC [SUM_SUMMABLE, SUM_UNIQ, summable]
1834QED
1835
1836Theorem SUMINF_POS:
1837 !f. (!n. 0 <= f n) /\ summable f ==> 0 <= suminf f
1838Proof
1839 RW_TAC std_ss []
1840 >> Know `0 = sum (0, 0) f` >- RW_TAC std_ss [sum]
1841 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap)
1842 >> MATCH_MP_TAC SER_POS_LE
1843 >> RW_TAC std_ss []
1844QED
1845
1846Theorem SUM_CONST_R:
1847 !n r. sum (0,n) (K r) = &n * r
1848Proof
1849 Induct >- RW_TAC real_ss [sum]
1850 >> RW_TAC bool_ss [sum, ADD1, K_THM, GSYM REAL_ADD, REAL_ADD_RDISTRIB]
1851 >> RW_TAC real_ss []
1852QED
1853
1854Theorem SUMS_ZERO:
1855 (K 0) sums 0
1856Proof
1857 RW_TAC real_ss [sums, SEQ, SUM_CONST_R, abs, REAL_SUB_REFL, REAL_LE_REFL]
1858QED
1859
1860Theorem LT_SUC'[local] = DECIDE “!a b. a < SUC b = a < b \/ (a = b)”
1861
1862Theorem SUMINF_ADD:
1863 !f g.
1864 summable f /\ summable g ==>
1865 summable (\n. f n + g n) /\
1866 (suminf f + suminf g = suminf (\n. f n + g n))
1867Proof
1868 RW_TAC std_ss []
1869 >> ( Know `f sums suminf f /\ g sums suminf g` >- PROVE_TAC [SUMMABLE_SUM]
1870 >> STRIP_TAC
1871 >> Know `(\n. f n + g n) sums (suminf f + suminf g)`
1872 >- RW_TAC std_ss [SER_ADD]
1873 >> RW_TAC std_ss [SUMS_EQ] )
1874QED
1875
1876Theorem SUMINF_2D:
1877 !f g h.
1878 (!m n. 0 <= f m n) /\ (!n. f n sums g n) /\ summable g /\
1879 BIJ h UNIV (UNIV CROSS UNIV) ==>
1880 (UNCURRY f o h) sums suminf g
1881Proof
1882 RW_TAC std_ss []
1883 >> RW_TAC std_ss [sums]
1884 >> Know `g sums suminf g` >- PROVE_TAC [SUMMABLE_SUM]
1885 >> Q.PAT_X_ASSUM `!n. P n` MP_TAC
1886 >> RW_TAC std_ss [SUMS_EQ, FORALL_AND_THM]
1887 >> MATCH_MP_TAC INCREASING_SEQ
1888 >> CONJ_TAC
1889 >- (RW_TAC std_ss [sum, o_THM, ADD_CLAUSES]
1890 >> Cases_on `h n`
1891 >> RW_TAC std_ss [UNCURRY_DEF]
1892 >> Q.PAT_X_ASSUM `!m n. 0 <= f m n` (MP_TAC o Q.SPECL [`q`, `r`])
1893 >> REAL_ARITH_TAC)
1894 >> Know `!m. 0 <= g m`
1895 >- (STRIP_TAC
1896 >> Suff `0 <= suminf (f m)` >- PROVE_TAC []
1897 >> MATCH_MP_TAC SER_POS
1898 >> PROVE_TAC [])
1899 >> STRIP_TAC
1900 >> CONJ_TAC
1901 >- (RW_TAC std_ss []
1902 >> MP_TAC (Q.SPECL [`h`, `n`] NUM_2D_BIJ_BIG_SQUARE)
1903 >> ASM_REWRITE_TAC []
1904 >> STRIP_TAC
1905 >> MATCH_MP_TAC REAL_LE_TRANS
1906 >> Q.EXISTS_TAC `sum (0,k) g`
1907 >> REVERSE CONJ_TAC
1908 >- (MATCH_MP_TAC SER_POS_LE
1909 >> PROVE_TAC [])
1910 >> MATCH_MP_TAC REAL_LE_TRANS
1911 >> Q.EXISTS_TAC `sum (0,k) (\m. sum (0,k) (f m))`
1912 >> REVERSE CONJ_TAC
1913 >- (MATCH_MP_TAC SUM_LE
1914 >> RW_TAC std_ss []
1915 >> Q.PAT_X_ASSUM `!n. suminf (f n) = g n` (REWRITE_TAC o wrap o GSYM)
1916 >> MATCH_MP_TAC SER_POS_LE
1917 >> PROVE_TAC [])
1918 >> Suff
1919 `!j.
1920 j <= n ==>
1921 (sum (0, j) (UNCURRY f o h) =
1922 sum (0, k)
1923 (\m. sum (0, k)
1924 (\n. if (?i. i < j /\ (h i = (m, n))) then f m n else 0)))`
1925 >- (DISCH_THEN (MP_TAC o Q.SPEC `n`)
1926 >> REWRITE_TAC [LESS_EQ_REFL]
1927 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap)
1928 >> MATCH_MP_TAC SUM_LE
1929 >> RW_TAC std_ss []
1930 >> MATCH_MP_TAC SUM_LE
1931 >> RW_TAC std_ss [REAL_LE_REFL])
1932 >> Induct >- RW_TAC arith_ss [sum, SUM_0]
1933 >> RW_TAC std_ss [sum]
1934 >> Q.PAT_X_ASSUM `p ==> q` MP_TAC
1935 >> RW_TAC arith_ss []
1936 >> Know
1937 `!m n.
1938 (?i. i < SUC j /\ (h i = (m,n))) =
1939 (?i. i < j /\ (h i = (m,n))) \/ (h j = (m, n))`
1940 >- (RW_TAC std_ss []
1941 >> Suff `!i. i < SUC j = i < j \/ (i = j)`
1942 >- PROVE_TAC []
1943 >> DECIDE_TAC)
1944 >> DISCH_THEN (REWRITE_TAC o wrap)
1945 >> Know
1946 `!m n.
1947 (if (?i. i < j /\ (h i = (m,n))) \/ (h j = (m,n)) then f m n
1948 else 0) =
1949 (if (?i. i < j /\ (h i = (m,n))) then f m n else 0) +
1950 (if (h j = (m,n)) then f m n else 0)`
1951 >- (Strip
1952 >> Suff `(?i. i < j /\ (h i = (m,n'))) ==> ~(h j = (m,n'))`
1953 >- PROVE_TAC [REAL_ADD_LID, REAL_ADD_RID]
1954 >> RW_TAC std_ss []
1955 >> Q.PAT_X_ASSUM `BIJ a b c` MP_TAC
1956 >> RW_TAC std_ss [BIJ_DEF, INJ_DEF, IN_UNIV, IN_CROSS]
1957 >> PROVE_TAC [prim_recTheory.LESS_REFL])
1958 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap)
1959 >> RW_TAC std_ss [SUM_ADD]
1960 >> POP_ASSUM K_TAC
1961 >> Suff
1962 `(UNCURRY f o h) j =
1963 sum (0,k)
1964 (\m. sum (0,k) (\n. (if h j = (m,n) then f m n else 0)))`
1965 >- (KILL_TAC
1966 >> Q.SPEC_TAC
1967 (`(sum (0,k)
1968 (\m.
1969 sum (0,k)
1970 (\n. if ?i. i < j /\ (h i = (m,n)) then f m n else 0)))`,
1971 `r1`)
1972 >> Q.SPEC_TAC
1973 (`sum (0,k)
1974 (\m. sum (0,k) (\n. (if h j = (m,n) then f m n else 0)))`,
1975 `r2`)
1976 >> RW_TAC std_ss [])
1977 >> Cases_on `h j`
1978 >> RW_TAC std_ss [o_THM, UNCURRY_DEF]
1979 >> Know
1980 `!m n.
1981 (if (q = m) /\ (r = n) then f m n else 0) =
1982 (if (n = r) then if (m = q) then f m n else 0 else 0)`
1983 >- PROVE_TAC []
1984 >> DISCH_THEN (REWRITE_TAC o wrap)
1985 >> Q.PAT_X_ASSUM `a SUBSET b` MP_TAC
1986 >> RW_TAC std_ss [SUBSET_DEF, IN_IMAGE, IN_COUNT, IN_CROSS]
1987 >> Suff `q < k /\ r < k`
1988 >- RW_TAC std_ss [SUM_PICK]
1989 >> POP_ASSUM (MP_TAC o Q.SPEC `h (j:num)`)
1990 >> Suff `j < n`
1991 >- (RW_TAC std_ss []
1992 >> PROVE_TAC [])
1993 >> DECIDE_TAC)
1994 >> RW_TAC std_ss []
1995 >> Know `?M. 0 < M /\ suminf g < sum (0, M) g + e / 2`
1996 >- (Know `g sums suminf g` >- PROVE_TAC [SUMMABLE_SUM]
1997 >> RW_TAC std_ss [sums, SEQ]
1998 >> POP_ASSUM (MP_TAC o Q.SPEC `e / 2`)
1999 >> RW_TAC std_ss [REAL_LT_HALF1, GREATER_EQ]
2000 >> POP_ASSUM (MP_TAC o Q.SPEC `SUC N`)
2001 >> ONCE_REWRITE_TAC [ABS_SUB]
2002 >> Know `sum (0, SUC N) g <= suminf g`
2003 >- (MATCH_MP_TAC SER_POS_LE
2004 >> RW_TAC std_ss [])
2005 >> REVERSE (RW_TAC arith_ss [abs])
2006 >- (Suff `F` >- PROVE_TAC []
2007 >> POP_ASSUM K_TAC
2008 >> POP_ASSUM MP_TAC
2009 >> POP_ASSUM MP_TAC
2010 >> REAL_ARITH_TAC)
2011 >> Q.EXISTS_TAC `SUC N`
2012 >> CONJ_TAC >- DECIDE_TAC
2013 >> POP_ASSUM MP_TAC
2014 >> REAL_ARITH_TAC)
2015 >> RW_TAC std_ss []
2016 >> Suff `?k. sum (0, M) g < sum (0, k) (UNCURRY f o h) + e / 2`
2017 >- (Strip
2018 >> Q.EXISTS_TAC `k`
2019 >> Know
2020 `sum (0, M) g + e / 2 < sum (0, k) (UNCURRY f o h) + (e / 2 + e / 2)`
2021 >- (POP_ASSUM MP_TAC
2022 >> REAL_ARITH_TAC)
2023 >> POP_ASSUM K_TAC
2024 >> POP_ASSUM MP_TAC
2025 >> REWRITE_TAC [REAL_HALF_DOUBLE]
2026 >> REAL_ARITH_TAC)
2027 >> POP_ASSUM K_TAC
2028 >> Know `!m. ?N. g m < sum (0, N) (f m) + (e / 2) / & M`
2029 >- (Know `!m. f m sums g m`
2030 >- RW_TAC std_ss [SUMS_EQ]
2031 >> RW_TAC std_ss [sums, SEQ]
2032 >> POP_ASSUM (MP_TAC o Q.SPECL [`m`, `(e / 2) / & M`])
2033 >> Know `0 < (e / 2) / & M`
2034 >- RW_TAC arith_ss [REAL_LT_DIV, REAL_NZ_IMP_LT]
2035 >> DISCH_THEN (REWRITE_TAC o wrap)
2036 >> RW_TAC std_ss [GREATER_EQ]
2037 >> POP_ASSUM (MP_TAC o Q.SPEC `N`)
2038 >> ONCE_REWRITE_TAC [ABS_SUB]
2039 >> Know `sum (0, N) (f m) <= g m`
2040 >- (Q.PAT_X_ASSUM `!n. P n = Q n` (REWRITE_TAC o wrap o GSYM)
2041 >> MATCH_MP_TAC SER_POS_LE
2042 >> RW_TAC std_ss [])
2043 >> REVERSE (RW_TAC arith_ss [abs])
2044 >- (POP_ASSUM K_TAC
2045 >> Suff `F` >- PROVE_TAC []
2046 >> NTAC 2 (POP_ASSUM MP_TAC)
2047 >> REAL_ARITH_TAC)
2048 >> Q.EXISTS_TAC `N`
2049 >> POP_ASSUM MP_TAC
2050 >> REAL_ARITH_TAC)
2051 >> DISCH_THEN (MP_TAC o CONV_RULE SKOLEM_CONV)
2052 >> RW_TAC std_ss []
2053 >> Know `?c. M <= c /\ !m. m < M ==> N m <= c`
2054 >- (KILL_TAC
2055 >> Induct_on `M` >- RW_TAC arith_ss []
2056 >> Strip
2057 >> Q.EXISTS_TAC `MAX (SUC c) (N M)`
2058 >> RW_TAC arith_ss [X_LE_MAX, LT_SUC']
2059 >> PROVE_TAC [LESS_EQ_REFL, LE])
2060 >> Strip
2061 >> MP_TAC (Q.SPECL [`h`, `c`] NUM_2D_BIJ_SMALL_SQUARE)
2062 >> ASM_REWRITE_TAC []
2063 >> DISCH_THEN (Q.X_CHOOSE_TAC `k`)
2064 >> Q.EXISTS_TAC `k`
2065 >> MATCH_MP_TAC REAL_LTE_TRANS
2066 >> Q.EXISTS_TAC `sum (0, M) (\m. sum (0, N m) (f m) + e / 2 / &M)`
2067 >> CONJ_TAC
2068 >- (MATCH_MP_TAC SUM_LT
2069 >> RW_TAC arith_ss [])
2070 >> RW_TAC std_ss [SUM_ADD, GSYM K_PARTIAL, SUM_CONST_R]
2071 >> Know `!x:real. & M * (x / & M) = x`
2072 >- (RW_TAC std_ss [real_div]
2073 >> Suff `(& M * inv (& M)) * x = x`
2074 >- PROVE_TAC [REAL_MUL_ASSOC, REAL_MUL_SYM]
2075 >> Suff `~(& M = 0:real)` >- RW_TAC std_ss [REAL_MUL_RINV, REAL_MUL_LID]
2076 >> RW_TAC arith_ss [REAL_INJ])
2077 >> DISCH_THEN (REWRITE_TAC o wrap)
2078 >> RW_TAC std_ss [REAL_LE_RADD]
2079 >> Suff
2080 `sum (0,M) (\m. sum (0,N m) (f m)) =
2081 sum (0, k)
2082 (\k.
2083 if ?m n. m < M /\ n < N m /\ (h k = (m, n)) then (UNCURRY f o h) k
2084 else 0)`
2085 >- (RW_TAC std_ss []
2086 >> MATCH_MP_TAC SUM_LE
2087 >> RW_TAC std_ss [o_THM, REAL_LE_REFL]
2088 >> Cases_on `h r`
2089 >> RW_TAC std_ss [UNCURRY_DEF])
2090 >> NTAC 3 (POP_ASSUM MP_TAC)
2091 >> Q.PAT_X_ASSUM `BIJ h a b` MP_TAC
2092 >> KILL_TAC
2093 >> RW_TAC std_ss []
2094 >> Induct_on `M` >- RW_TAC arith_ss [sum, SUM_ZERO]
2095 >> RW_TAC arith_ss [sum, LT_SUC']
2096 >> Q.PAT_X_ASSUM `a ==> b` K_TAC
2097 >> Know
2098 `!k'.
2099 (?m n. (m < M \/ (m = M)) /\ n < N m /\ (h k' = (m, n))) =
2100 (?m n. m < M /\ n < N m /\ (h k' = (m, n))) \/
2101 (?n. n < N M /\ (h k' = (M, n)))`
2102 >- PROVE_TAC []
2103 >> DISCH_THEN (REWRITE_TAC o wrap)
2104 >> Know
2105 `!k'.
2106 (if (?m n. m < M /\ n < N m /\ (h k' = (m,n))) \/
2107 (?n. n < N M /\ (h k' = (M,n)))
2108 then UNCURRY f (h k')
2109 else 0) =
2110 (if (?m n. m < M /\ n < N m /\ (h k' = (m,n))) then UNCURRY f (h k')
2111 else 0) +
2112 (if (?n. n < N M /\ (h k' = (M,n))) then UNCURRY f (h k')
2113 else 0)`
2114 >- (STRIP_TAC
2115 >> Suff
2116 `(?m n. m < M /\ n < N m /\ (h k' = (m,n))) ==>
2117 ~(?n. n < N M /\ (h k' = (M,n)))`
2118 >- PROVE_TAC [REAL_ADD_RID, REAL_ADD_LID]
2119 >> Cases_on `h k'`
2120 >> RW_TAC arith_ss [])
2121 >> DISCH_THEN (REWRITE_TAC o wrap)
2122 >> RW_TAC std_ss [SUM_ADD, REAL_EQ_LADD]
2123 >> Know `N M <= c` >- PROVE_TAC []
2124 >> POP_ASSUM K_TAC
2125 >> Q.SPEC_TAC (`N M`, `l`)
2126 >> Induct >- RW_TAC real_ss [sum, SUM_0]
2127 >> RW_TAC arith_ss [sum, LT_SUC']
2128 >> Q.PAT_X_ASSUM `a ==> b` K_TAC
2129 >> Know
2130 `!k'.
2131 (?n. (n < l \/ (n = l)) /\ (h k' = (M,n))) =
2132 (?n. n < l /\ (h k' = (M,n))) \/ (h k' = (M, l))`
2133 >- PROVE_TAC []
2134 >> DISCH_THEN (REWRITE_TAC o wrap)
2135 >> Know
2136 `!k'.
2137 (if (?n. n < l /\ (h k' = (M,n))) \/ (h k' = (M, l)) then
2138 UNCURRY f (h k')
2139 else 0) =
2140 (if (?n. n < l /\ (h k' = (M,n))) then UNCURRY f (h k') else 0) +
2141 (if (h k' = (M, l)) then UNCURRY f (h k') else 0)`
2142 >- (STRIP_TAC
2143 >> Suff `(?n. n < l /\ (h k' = (M,n))) ==> ~(h k' = (M, l))`
2144 >- PROVE_TAC [REAL_ADD_LID, REAL_ADD_RID]
2145 >> Cases_on `h k'`
2146 >> RW_TAC arith_ss [])
2147 >> DISCH_THEN (REWRITE_TAC o wrap)
2148 >> RW_TAC std_ss [SUM_ADD, REAL_EQ_LADD]
2149 >> Q.PAT_X_ASSUM `a SUBSET b` MP_TAC
2150 >> RW_TAC std_ss [SUBSET_DEF, IN_CROSS, IN_COUNT, IN_IMAGE]
2151 >> POP_ASSUM (MP_TAC o Q.SPEC `(M, l)`)
2152 >> RW_TAC arith_ss []
2153 >> Suff `!k'. (h k' = (M, l)) = (k' = x')`
2154 >- (RW_TAC std_ss [SUM_PICK, o_THM]
2155 >> Q.PAT_X_ASSUM `(M,l) = a` (REWRITE_TAC o wrap o GSYM)
2156 >> RW_TAC std_ss [UNCURRY_DEF])
2157 >> Q.PAT_X_ASSUM `BIJ h a b` MP_TAC
2158 >> RW_TAC std_ss [BIJ_DEF, INJ_DEF, IN_UNIV, IN_CROSS]
2159 >> PROVE_TAC []
2160QED
2161
2162Theorem POW_HALF_SER:
2163 (\n. (1 / 2) pow (n + 1)) sums 1
2164Proof
2165 Know `(\n. (1 / 2) pow n) sums inv (1 - (1 / 2))`
2166 >- (MATCH_MP_TAC GP
2167 >> RW_TAC std_ss [abs, HALF_POS, REAL_LT_IMP_LE, HALF_LT_1])
2168 >> RW_TAC std_ss [ONE_MINUS_HALF, REAL_INV_INV, GSYM REAL_INV_1OVER,
2169 GSYM ADD1, pow]
2170 >> Know `1 = inv 2 * 2:real`
2171 >- RW_TAC arith_ss [REAL_MUL_LINV, REAL_INJ]
2172 >> DISCH_THEN (ONCE_REWRITE_TAC o wrap)
2173 >> HO_MATCH_MP_TAC SER_CMUL
2174 >> RW_TAC std_ss []
2175QED
2176
2177Theorem SER_POS_COMPARE:
2178 !f g.
2179 (!n. 0 <= f n) /\ summable g /\ (!n. f n <= g n) ==>
2180 summable f /\ suminf f <= suminf g
2181Proof
2182 REVERSE (rpt (STRONG_CONJ_TAC ORELSE STRIP_TAC))
2183 >- PROVE_TAC [SER_LE]
2184 >> MATCH_MP_TAC SER_COMPAR
2185 >> Q.EXISTS_TAC `g`
2186 >> RW_TAC std_ss []
2187 >> Q.EXISTS_TAC `0`
2188 >> RW_TAC arith_ss [abs]
2189QED
2190
2191(* moved here from real_sigmaTheory *)
2192Theorem SEQ_REAL_SUM_IMAGE :
2193 !s. FINITE s ==>
2194 !f f'. (!x. x IN s ==> (\n. f n x) --> f' x) ==>
2195 (\n. REAL_SUM_IMAGE (f n) s) --> REAL_SUM_IMAGE f' s
2196Proof
2197 Suff `!s. FINITE s ==>
2198 (\s. !f f'. (!x. x IN s ==> (\n. f n x) --> f' x) ==>
2199 (\n. REAL_SUM_IMAGE (f n) s) -->
2200 REAL_SUM_IMAGE f' s) s`
2201 >- RW_TAC std_ss []
2202 >> MATCH_MP_TAC FINITE_INDUCT
2203 >> RW_TAC std_ss [REAL_SUM_IMAGE_THM, SEQ_CONST, IN_INSERT, DELETE_NON_ELEMENT]
2204 >> `(\n. f n e + REAL_SUM_IMAGE (f n) s) = (\n. (\n. f n e) n + (\n. REAL_SUM_IMAGE (f n) s) n)`
2205 by RW_TAC std_ss []
2206 >> POP_ORW
2207 >> MATCH_MP_TAC SEQ_ADD
2208 >> METIS_TAC []
2209QED
2210
2211Theorem POW_HALF_SMALL :
2212 !e:real. 0 < e ==> ?n. (1 / 2) pow n < e
2213Proof
2214 RW_TAC std_ss []
2215 >> MP_TAC (Q.SPEC `1 / 2` SEQ_POWER)
2216 >> RW_TAC std_ss [abs, HALF_LT_1, HALF_POS, REAL_LT_IMP_LE, SEQ]
2217 >> POP_ASSUM (MP_TAC o Q.SPEC `e`)
2218 >> RW_TAC std_ss [REAL_SUB_RZERO, POW_HALF_POS, REAL_LT_IMP_LE,
2219 GREATER_EQ]
2220 >> PROVE_TAC [LESS_EQ_REFL]
2221QED
2222
2223Theorem POW_HALF_MONO :
2224 !m n. m <= n ==> ((1:real)/2) pow n <= (1/2) pow m
2225Proof
2226 REPEAT STRIP_TAC
2227 >> Induct_on `n`
2228 >- (STRIP_TAC \\
2229 Know `m:num = 0` >- DECIDE_TAC \\
2230 PROVE_TAC [REAL_LE_REFL])
2231 >> Cases_on `m = SUC n` >- PROVE_TAC [REAL_LE_REFL]
2232 >> ONCE_REWRITE_TAC [pow]
2233 >> STRIP_TAC
2234 >> Know `m:num <= n` >- DECIDE_TAC
2235 >> STRIP_TAC
2236 >> Suff `(2:real) * ((1/2) * (1/2) pow n) <= 2 * (1/2) pow m`
2237 >- PROVE_TAC [REAL_ARITH ``0:real < 2``, REAL_LE_LMUL]
2238 >> Suff `((1:real)/2) pow n <= 2 * (1/2) pow m`
2239 >- (KILL_TAC \\
2240 PROVE_TAC [GSYM REAL_MUL_ASSOC, HALF_CANCEL, REAL_MUL_LID])
2241 >> PROVE_TAC [REAL_ARITH ``!x y. 0:real < x /\ x <= y ==> x <= 2 * y``,
2242 POW_HALF_POS]
2243QED
2244
2245Theorem HARMONIC_SERIES_POW_2 : (* was in util_probTheory *)
2246 summable (\n. inv (&(SUC n) pow 2))
2247Proof
2248 MATCH_MP_TAC POS_SUMMABLE
2249 >> CONJ_TAC >- rw []
2250 >> Q.EXISTS_TAC `2`
2251 >> GEN_TAC
2252 >> Cases_on `n` >- rw [sum]
2253 >> rename1 ‘sum (0,SUC m) (\n. inv (&SUC n pow 2)) <= 2’
2254 >> MATCH_MP_TAC REAL_LE_TRANS
2255 >> Q.EXISTS_TAC `1 + sum (1,m) (\n. inv (&n) - inv (&SUC n))`
2256 >> CONJ_TAC
2257 >- (Know `sum (0,SUC m) (\n. inv (&SUC n pow 2)) =
2258 sum (0,1) (\n. inv (&SUC n pow 2)) + sum (1,m) (\n. inv (&SUC n pow 2))`
2259 >- (MATCH_MP_TAC EQ_SYM \\
2260 MP_TAC (Q.SPECL [`\n. inv (&SUC n pow 2)`, `1`, `m`] SUM_TWO) \\
2261 RW_TAC arith_ss [ADD1]) >> Rewr' \\
2262 Know `sum (0,1) (\n. inv (&SUC n pow 2)) = 1`
2263 >- (REWRITE_TAC [sum, ONE] >> rw []) >> Rewr' \\
2264 REWRITE_TAC [REAL_LE_LADD] \\
2265 MATCH_MP_TAC realTheory.SUM_LE \\
2266 RW_TAC real_ss [REAL_INV_1OVER] \\
2267 `&r <> 0` by RW_TAC real_ss [] \\
2268 `&SUC r <> 0` by RW_TAC real_ss [] \\
2269 ASM_SIMP_TAC real_ss [REAL_SUB_RAT] \\
2270 `&SUC r - &r = 1` by METIS_TAC [REAL, REAL_ADD_SUB] >> POP_ORW \\
2271 ASM_SIMP_TAC std_ss [POW_2, GSYM REAL_INV_1OVER] \\
2272 `0 < &SUC r * &SUC r` by rw [] \\
2273 Know `0 < &(r * SUC r)`
2274 >- (rw [] >> `0 = r * 0` by RW_TAC arith_ss [] >> POP_ORW \\
2275 rw [LT_MULT_LCANCEL]) >> DISCH_TAC \\
2276 MATCH_MP_TAC REAL_LT_IMP_LE \\
2277 ASM_SIMP_TAC real_ss [REAL_INV_LT_ANTIMONO] \\
2278 `SUC r ** 2 = SUC r * SUC r` by RW_TAC arith_ss [] >> POP_ORW \\
2279 RW_TAC arith_ss [LT_MULT_RCANCEL])
2280 >> `2 = 1 + (1 :real)` by RW_TAC real_ss [] >> POP_ORW
2281 >> REWRITE_TAC [REAL_LE_LADD]
2282 >> Q.ABBREV_TAC `f = \n. -inv (&n)`
2283 >> Know `!n. inv (&n) - inv (&SUC n) = f (SUC n) - f n`
2284 >- (RW_TAC real_ss [Abbr `f`] \\
2285 REAL_ASM_ARITH_TAC) >> Rewr'
2286 >> REWRITE_TAC [SUM_CANCEL]
2287 >> rw [Abbr `f`, REAL_SUB_NEG2, REAL_LE_SUB_RADD, REAL_LE_ADDR]
2288QED
2289