powserScript.sml
1(*===========================================================================*)
2(* Properties of power series. *)
3(*===========================================================================*)
4Theory powser
5Ancestors
6 pair arithmetic num prim_rec real metric nets seq lim
7Libs
8 hol88Lib numLib reduceLib pairLib jrhUtils
9
10
11(*---------------------------------------------------------------------------*)
12(* More theorems about rearranging finite sums *)
13(*---------------------------------------------------------------------------*)
14
15Theorem POWDIFF_LEMMA:
16 !n x y. sum(0,SUC n)(\p. (x pow p) * y pow ((SUC n) - p)) =
17 y * sum(0,SUC n)(\p. (x pow p) * (y pow (n - p)))
18Proof
19 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM SUM_CMUL] THEN
20 MATCH_MP_TAC SUM_SUBST THEN X_GEN_TAC “p:num” THEN DISCH_TAC THEN
21 BETA_TAC THEN GEN_REWR_TAC RAND_CONV [REAL_MUL_SYM] THEN
22 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
23 SUBGOAL_THEN “~(n:num < p)” ASSUME_TAC THENL
24 [POP_ASSUM(MP_TAC o CONJUNCT2) THEN REWRITE_TAC[ADD_CLAUSES] THEN
25 REWRITE_TAC[NOT_LESS, LESS_THM] THEN
26 DISCH_THEN(DISJ_CASES_THEN2 SUBST1_TAC MP_TAC) THEN
27 REWRITE_TAC[LESS_EQ_REFL, LESS_IMP_LESS_OR_EQ],
28 ASM_REWRITE_TAC[SUB] THEN REWRITE_TAC[pow] THEN
29 MATCH_ACCEPT_TAC REAL_MUL_SYM]
30QED
31
32Theorem POWDIFF:
33 !n x y.
34 (x pow (SUC n)) - (y pow (SUC n))
35 =
36 (x - y) * sum(0,SUC n) (\p. (x pow p) * (y pow (n-p)))
37Proof
38 INDUCT_TAC THENL
39 [REPEAT GEN_TAC THEN REWRITE_TAC[sum] THEN
40 REWRITE_TAC[REAL_ADD_LID, ADD_CLAUSES, SUB_0] THEN
41 BETA_TAC THEN REWRITE_TAC[pow] THEN
42 REWRITE_TAC[REAL_MUL_RID],
43 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[sum] THEN
44 REWRITE_TAC[ADD_CLAUSES] THEN BETA_TAC THEN
45 REWRITE_TAC[POWDIFF_LEMMA] THEN REWRITE_TAC[REAL_LDISTRIB] THEN
46 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
47 “a * (b * c) = b * (a * c)”] THEN
48 POP_ASSUM(fn th => ONCE_REWRITE_TAC[GSYM th]) THEN
49 REWRITE_TAC[SUB_EQUAL_0] THEN
50 SPEC_TAC(“SUC n”,“n:num”) THEN GEN_TAC THEN
51 REWRITE_TAC[pow, REAL_MUL_RID] THEN
52 REWRITE_TAC[REAL_LDISTRIB, REAL_SUB_LDISTRIB] THEN
53 REWRITE_TAC[real_sub] THEN
54 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM)
55 “(a + b) + (c + d) = (d + a) + (c + b)”] THEN
56 GEN_REWR_TAC (funpow 2 LAND_CONV) [REAL_MUL_SYM] THEN
57 CONV_TAC SYM_CONV THEN REWRITE_TAC[REAL_ADD_LID_UNIQ] THEN
58 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [REAL_MUL_SYM] THEN
59 REWRITE_TAC[REAL_ADD_LINV]]
60QED
61
62Theorem POWREV:
63 !n x y. sum(0,SUC n)(\p. (x pow p) * (y pow (n - p))) =
64 sum(0,SUC n)(\p. (x pow (n - p)) * (y pow p))
65Proof
66 let val REAL_EQ_LMUL2' = CONV_RULE(REDEPTH_CONV FORALL_IMP_CONV) REAL_EQ_LMUL2 in
67 REPEAT GEN_TAC THEN ASM_CASES_TAC “x:real = y” THENL
68 [ASM_REWRITE_TAC[GSYM POW_ADD] THEN
69 MATCH_MP_TAC SUM_SUBST THEN X_GEN_TAC “p:num” THEN
70 BETA_TAC THEN DISCH_TAC THEN AP_TERM_TAC THEN
71 MATCH_ACCEPT_TAC ADD_SYM,
72 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
73 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[GSYM REAL_SUB_0]) THEN
74 FIRST_ASSUM(fn th => GEN_REWR_TAC I [MATCH_MP REAL_EQ_LMUL2' th]) THEN
75 GEN_REWR_TAC RAND_CONV [GSYM REAL_NEGNEG] THEN
76 ONCE_REWRITE_TAC[REAL_NEG_LMUL] THEN
77 ONCE_REWRITE_TAC[REAL_NEG_SUB] THEN
78 REWRITE_TAC[GSYM POWDIFF] THEN REWRITE_TAC[REAL_NEG_SUB]] end
79QED
80
81(*---------------------------------------------------------------------------*)
82(* Show (essentially) that a power series has a "circle" of convergence, i.e.*)
83(* if it sums for x, then it sums absolutely for z with |z| < |x| *)
84(*---------------------------------------------------------------------------*)
85
86Theorem POWSER_INSIDEA:
87 !f x z. summable (\n. f(n) * (x pow n)) /\ abs(z) < abs(x)
88 ==> summable (\n. abs(f(n)) * (z pow n))
89Proof
90 let val th = (GEN_ALL o CONV_RULE LEFT_IMP_EXISTS_CONV o snd o
91 EQ_IMP_RULE o SPEC_ALL) convergent in
92 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
93 DISCH_THEN(MP_TAC o MATCH_MP SER_ZERO) THEN
94 DISCH_THEN(MP_TAC o MATCH_MP th) THEN REWRITE_TAC[GSYM SEQ_CAUCHY] THEN
95 DISCH_THEN(MP_TAC o MATCH_MP SEQ_CBOUNDED) THEN
96 REWRITE_TAC[SEQ_BOUNDED] THEN BETA_TAC THEN
97 DISCH_THEN(X_CHOOSE_TAC “k':real”) THEN MATCH_MP_TAC SER_COMPAR THEN
98 EXISTS_TAC “\n. (k' * abs(z pow n)) / abs(x pow n)” THEN CONJ_TAC THENL
99 [EXISTS_TAC “0:num” THEN X_GEN_TAC “n:num” THEN DISCH_THEN(K ALL_TAC) THEN
100 BETA_TAC THEN MATCH_MP_TAC REAL_LE_RDIV THEN CONJ_TAC THENL
101 [REWRITE_TAC[GSYM ABS_NZ] THEN MATCH_MP_TAC POW_NZ THEN
102 REWRITE_TAC[ABS_NZ] THEN MATCH_MP_TAC REAL_LET_TRANS THEN
103 EXISTS_TAC “abs(z)” THEN ASM_REWRITE_TAC[ABS_POS],
104 REWRITE_TAC[ABS_MUL, ABS_ABS, GSYM REAL_MUL_ASSOC] THEN
105 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
106 “a * (b * c) = (a * c) * b”] THEN
107 DISJ_CASES_TAC(SPEC “z pow n” ABS_CASES) THEN
108 ASM_REWRITE_TAC[ABS_0, REAL_MUL_RZERO, REAL_LE_REFL] THEN
109 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_LE_RMUL th]) THEN
110 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[GSYM ABS_MUL]],
111 REWRITE_TAC[summable] THEN
112 EXISTS_TAC “k' * inv(&1 - (abs(z) / abs(x)))” THEN
113 REWRITE_TAC[real_div, GSYM REAL_MUL_ASSOC] THEN
114 CONV_TAC(ONCE_DEPTH_CONV HABS_CONV) THEN REWRITE_TAC[] THEN
115 MATCH_MP_TAC SER_CMUL THEN
116 GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [GSYM real_div] THEN
117 SUBGOAL_THEN “!n. abs(z pow n) / abs(x pow n) =
118 (abs(z) / abs(x)) pow n”
119 (fn th => ONCE_REWRITE_TAC[th]) THENL
120 [ALL_TAC, REWRITE_TAC[GSYM real_div] THEN
121 MATCH_MP_TAC GP THEN REWRITE_TAC[real_div, ABS_MUL] THEN
122 SUBGOAL_THEN “~(abs(x) = &0)” (SUBST1_TAC o MATCH_MP ABS_INV) THENL
123 [DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC “abs(z) < &0” THEN
124 REWRITE_TAC[REAL_NOT_LT, ABS_POS],
125 REWRITE_TAC[ABS_ABS, GSYM real_div] THEN
126 MATCH_MP_TAC REAL_LT_1 THEN ASM_REWRITE_TAC[ABS_POS]]] THEN
127 REWRITE_TAC[GSYM POW_ABS] THEN X_GEN_TAC “n:num” THEN
128 REWRITE_TAC[real_div, POW_MUL] THEN AP_TERM_TAC THEN
129 MATCH_MP_TAC POW_INV THEN CONV_TAC(RAND_CONV SYM_CONV) THEN
130 MATCH_MP_TAC REAL_LT_IMP_NE THEN
131 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “abs(z)” THEN
132 ASM_REWRITE_TAC[ABS_POS]] end
133QED
134
135(*---------------------------------------------------------------------------*)
136(* Weaker but more commonly useful form for non-absolute convergence *)
137(*---------------------------------------------------------------------------*)
138
139Theorem POWSER_INSIDE:
140 !f x z. summable (\n. f(n) * (x pow n)) /\ abs(z) < abs(x)
141 ==> summable (\n. f(n) * (z pow n))
142Proof
143 REPEAT GEN_TAC THEN
144 SUBST1_TAC(SYM(SPEC “z:real” ABS_ABS)) THEN
145 DISCH_THEN(MP_TAC o MATCH_MP POWSER_INSIDEA) THEN
146 REWRITE_TAC[POW_ABS, GSYM ABS_MUL] THEN
147 DISCH_THEN(curry op THEN (MATCH_MP_TAC SER_ACONV) o MP_TAC) THEN
148 BETA_TAC THEN DISCH_THEN ACCEPT_TAC
149QED
150
151(*---------------------------------------------------------------------------*)
152(* Define formal differentiation of power series *)
153(*---------------------------------------------------------------------------*)
154
155Definition diffs[nocompute]:
156 diffs c = (\n. &(SUC n) * c(SUC n))
157End
158
159(*---------------------------------------------------------------------------*)
160(* Lemma about distributing negation over it *)
161(*---------------------------------------------------------------------------*)
162
163Theorem DIFFS_NEG:
164 !c. diffs(\n. ~(c n)) = \n. ~((diffs c) n)
165Proof
166 GEN_TAC THEN REWRITE_TAC[diffs] THEN BETA_TAC THEN
167 REWRITE_TAC[REAL_NEG_RMUL]
168QED
169
170(*---------------------------------------------------------------------------*)
171(* Show that we can shift the terms down one *)
172(*---------------------------------------------------------------------------*)
173
174Theorem DIFFS_LEMMA:
175 !n c x. sum(0,n) (\n. (diffs c)(n) * (x pow n)) =
176 sum(0,n) (\n. &n * (c(n) * (x pow (n - 1)))) +
177 (&n * (c(n) * x pow (n - 1)))
178Proof
179 INDUCT_TAC THEN ASM_REWRITE_TAC[sum, REAL_MUL_LZERO, REAL_ADD_LID] THEN
180 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
181 AP_TERM_TAC THEN BETA_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN
182 AP_TERM_TAC THEN REWRITE_TAC[diffs] THEN BETA_TAC THEN
183 REWRITE_TAC[SUC_SUB1, REAL_MUL_ASSOC]
184QED
185
186Theorem DIFFS_LEMMA2:
187 !n c x. sum(0,n) (\n. &n * (c(n) * (x pow (n - 1)))) =
188 sum(0,n) (\n. (diffs c)(n) * (x pow n)) -
189 (&n * (c(n) * x pow (n - 1)))
190Proof
191 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_EQ_SUB_LADD, DIFFS_LEMMA]
192QED
193
194Theorem DIFFS_EQUIV:
195 !c x. summable(\n. (diffs c)(n) * (x pow n)) ==>
196 (\n. &n * (c(n) * (x pow (n - 1)))) sums
197 (suminf(\n. (diffs c)(n) * (x pow n)))
198Proof
199 REPEAT GEN_TAC THEN DISCH_TAC THEN
200 FIRST_ASSUM(MP_TAC o REWRITE_RULE[diffs] o MATCH_MP SER_ZERO) THEN
201 BETA_TAC THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN DISCH_TAC THEN
202 SUBGOAL_THEN “(\n. &n * (c(n) * (x pow (n - 1)))) --> &0”
203 MP_TAC THENL
204 [ONCE_REWRITE_TAC[SEQ_SUC] THEN BETA_TAC THEN
205 ASM_REWRITE_TAC[SUC_SUB1], ALL_TAC] THEN
206 DISCH_THEN(MP_TAC o CONJ (MATCH_MP SUMMABLE_SUM
207 (ASSUME “summable(\n. (diffs c)(n) * (x pow n))”))) THEN
208 REWRITE_TAC[sums] THEN DISCH_THEN(MP_TAC o MATCH_MP SEQ_SUB) THEN
209 BETA_TAC THEN REWRITE_TAC[GSYM DIFFS_LEMMA2] THEN
210 REWRITE_TAC[REAL_SUB_RZERO]
211QED
212
213(*===========================================================================*)
214(* Show term-by-term differentiability of power series *)
215(* (NB we hypothesize convergence of first two derivatives; we could prove *)
216(* they all have the same radius of convergence, but we don't need to.) *)
217(*===========================================================================*)
218
219Theorem TERMDIFF_LEMMA1:
220 !m z h.
221 sum(0,m)(\p. (((z + h) pow (m - p)) * (z pow p)) - (z pow m)) =
222 sum(0,m)(\p. (z pow p) *
223 (((z + h) pow (m - p)) - (z pow (m - p))))
224Proof
225 REPEAT GEN_TAC THEN MATCH_MP_TAC SUM_SUBST THEN
226 X_GEN_TAC “p:num” THEN DISCH_TAC THEN BETA_TAC THEN
227 REWRITE_TAC[REAL_SUB_LDISTRIB, GSYM POW_ADD] THEN BINOP_TAC THENL
228 [MATCH_ACCEPT_TAC REAL_MUL_SYM,
229 AP_TERM_TAC THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
230 CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUB_ADD THEN
231 MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN
232 POP_ASSUM(MP_TAC o CONJUNCT2) THEN REWRITE_TAC[ADD_CLAUSES]]
233QED
234
235Theorem TERMDIFF_LEMMA2:
236 !z h n. ~(h = &0) ==>
237 (((((z + h) pow n) - (z pow n)) / h) - (&n * (z pow (n - 1))) =
238 h * sum(0,n - 1)(\p. (z pow p) *
239 sum(0,(n - 1) - p)
240 (\q. ((z + h) pow q) *
241 (z pow (((n - 2) - p) - q)))))
242Proof
243 REPEAT GEN_TAC THEN DISCH_TAC THEN
244 FIRST_ASSUM(fn th => GEN_REWR_TAC I [MATCH_MP REAL_EQ_LMUL2 th]) THEN
245 REWRITE_TAC[REAL_SUB_LDISTRIB] THEN
246 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_DIV_LMUL th]) THEN
247 DISJ_CASES_THEN2 SUBST1_TAC (X_CHOOSE_THEN “m:num” SUBST1_TAC)
248 (SPEC “n:num” num_CASES) THENL
249 [REWRITE_TAC[pow, REAL_MUL_LZERO, REAL_MUL_RZERO, REAL_SUB_REFL] THEN
250 REWRITE_TAC[SUB_0, sum, REAL_MUL_RZERO], ALL_TAC] THEN
251 REWRITE_TAC[POWDIFF, REAL_ADD_SUB] THEN
252 ASM_REWRITE_TAC[GSYM REAL_SUB_LDISTRIB, REAL_EQ_LMUL] THEN
253 REWRITE_TAC[SUC_SUB1] THEN
254 GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [POWREV] THEN
255 REWRITE_TAC[sum] THEN REWRITE_TAC[ADD_CLAUSES] THEN BETA_TAC THEN
256 REWRITE_TAC[SUB_EQUAL_0] THEN REWRITE_TAC[REAL, pow] THEN
257 REWRITE_TAC[REAL_MUL_LID, REAL_MUL_RID, REAL_RDISTRIB] THEN
258 REWRITE_TAC[REAL_ADD2_SUB2, REAL_SUB_REFL, REAL_ADD_RID] THEN
259 REWRITE_TAC[SUM_NSUB] THEN BETA_TAC THEN
260 REWRITE_TAC[TERMDIFF_LEMMA1] THEN
261 ONCE_REWRITE_TAC[GSYM SUM_CMUL] THEN BETA_TAC THEN
262 MATCH_MP_TAC SUM_SUBST THEN X_GEN_TAC “p:num” THEN
263 REWRITE_TAC[ADD_CLAUSES] THEN DISCH_TAC THEN BETA_TAC THEN
264 GEN_REWR_TAC RAND_CONV [REAL_MUL_SYM] THEN
265 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
266 FIRST_ASSUM(MP_TAC o CONJUNCT2) THEN
267 DISCH_THEN(X_CHOOSE_THEN “d:num” SUBST_ALL_TAC o MATCH_MP LESS_ADD_1) THEN
268 REWRITE_TAC[GSYM ADD1] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
269 REWRITE_TAC[ADD_SUB] THEN REWRITE_TAC[POWDIFF, REAL_ADD_SUB] THEN
270 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
271 AP_TERM_TAC THEN MATCH_MP_TAC SUM_SUBST THEN X_GEN_TAC “q:num” THEN
272 REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC THEN BETA_TAC THEN
273 AP_TERM_TAC THEN AP_TERM_TAC THEN CONV_TAC(TOP_DEPTH_CONV num_CONV) THEN
274 REWRITE_TAC[SUB_MONO_EQ, SUB_0, ADD_SUB]
275QED
276
277Theorem TERMDIFF_LEMMA3:
278 !z h n k'. ~(h = &0) /\ abs(z) <= k' /\ abs(z + h) <= k' ==>
279 abs(((((z + h) pow n) - (z pow n)) / h) - (&n * (z pow (n - 1))))
280 <= &n * (&(n - 1) * ((k' pow (n - 2)) * abs(h)))
281Proof
282 let val tac = W(curry op THEN (MATCH_MP_TAC REAL_LE_TRANS) o
283 EXISTS_TAC o rand o concl o PART_MATCH (rand o rator) ABS_SUM o
284 rand o rator o snd) THEN REWRITE_TAC[ABS_SUM] in
285 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
286 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP TERMDIFF_LEMMA2 th]) THEN
287 REWRITE_TAC[ABS_MUL] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN
288 GEN_REWR_TAC RAND_CONV [REAL_MUL_SYM] THEN
289 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
290 FIRST_ASSUM(ASSUME_TAC o CONV_RULE(REWR_CONV ABS_NZ)) THEN
291 FIRST_ASSUM(fn th => GEN_REWR_TAC I [MATCH_MP REAL_LE_LMUL th]) THEN
292 tac THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
293 GEN_REWR_TAC RAND_CONV [REAL_MUL_SYM] THEN
294 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
295 MATCH_MP_TAC SUM_BOUND THEN X_GEN_TAC “p:num” THEN
296 REWRITE_TAC[ADD_CLAUSES] THEN DISCH_THEN STRIP_ASSUME_TAC THEN
297 BETA_TAC THEN REWRITE_TAC[ABS_MUL] THEN
298 DISJ_CASES_THEN2 SUBST1_TAC (X_CHOOSE_THEN “r:num” SUBST_ALL_TAC)
299 (SPEC “n:num” num_CASES) THENL
300 [REWRITE_TAC[SUB_0, sum, ABS_0, REAL_MUL_RZERO, REAL_LE_REFL],
301 ALL_TAC] THEN
302 REWRITE_TAC[SUC_SUB1, TWO, SUB_MONO_EQ] THEN
303 RULE_ASSUM_TAC(REWRITE_RULE[SUC_SUB1]) THEN MP_TAC(ASSUME “p:num < r”) THEN
304 DISCH_THEN(X_CHOOSE_THEN “d:num” SUBST_ALL_TAC o MATCH_MP LESS_ADD_1) THEN
305 REWRITE_TAC[GSYM ADD1] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
306 REWRITE_TAC[ADD_SUB] THEN REWRITE_TAC[ADD_CLAUSES, SUC_SUB1, ADD_SUB] THEN
307 REWRITE_TAC[POW_ADD] THEN GEN_REWR_TAC RAND_CONV
308 [AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
309 “(a * b) * c = b * (c * a)”] THEN
310 MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[ABS_POS] THEN CONJ_TAC THENL
311 [REWRITE_TAC[GSYM POW_ABS] THEN MATCH_MP_TAC POW_LE THEN
312 ASM_REWRITE_TAC[ABS_POS], ALL_TAC] THEN
313 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “&(SUC d) * (k' pow d)” THEN
314 CONJ_TAC THENL
315 [ALL_TAC, SUBGOAL_THEN “&0 <= k'” MP_TAC THENL
316 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “abs z” THEN
317 ASM_REWRITE_TAC[ABS_POS],
318 DISCH_THEN(MP_TAC o SPEC “d:num” o MATCH_MP POW_POS) THEN
319 DISCH_THEN(DISJ_CASES_THEN MP_TAC o REWRITE_RULE[REAL_LE_LT]) THENL
320 [DISCH_THEN(fn th => REWRITE_TAC[MATCH_MP REAL_LE_RMUL th]) THEN
321 REWRITE_TAC[REAL_LE, LESS_EQ_MONO] THEN
322 MATCH_MP_TAC LESS_EQ_TRANS THEN EXISTS_TAC “SUC d” THEN
323 REWRITE_TAC[LESS_EQ_MONO, LESS_EQ_ADD] THEN
324 MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN REWRITE_TAC[LESS_SUC_REFL],
325 DISCH_THEN(SUBST1_TAC o SYM) THEN
326 REWRITE_TAC[REAL_MUL_RZERO, REAL_LE_REFL]]]] THEN
327 tac THEN MATCH_MP_TAC SUM_BOUND THEN X_GEN_TAC “q:num” THEN
328 REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC THEN BETA_TAC THEN
329 UNDISCH_TAC “q < SUC d” THEN
330 DISCH_THEN(X_CHOOSE_THEN “e:num” MP_TAC o MATCH_MP LESS_ADD_1) THEN
331 REWRITE_TAC[GSYM ADD1, ADD_CLAUSES, INV_SUC_EQ] THEN
332 DISCH_THEN SUBST_ALL_TAC THEN REWRITE_TAC[POW_ADD] THEN
333 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[ADD_SUB] THEN
334 REWRITE_TAC[ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
335 REWRITE_TAC[ABS_POS, GSYM POW_ABS] THEN
336 CONJ_TAC THEN MATCH_MP_TAC POW_LE THEN ASM_REWRITE_TAC[ABS_POS] end
337QED
338
339Theorem TERMDIFF_LEMMA4:
340 !f k' k. &0 < k /\
341 (!h. &0 < abs(h) /\ abs(h) < k ==> abs(f h) <= k' * abs(h))
342 ==> (f -> &0)(&0)
343Proof
344 REPEAT GEN_TAC THEN STRIP_TAC THEN
345 REWRITE_TAC[LIM, REAL_SUB_RZERO] THEN
346 SUBGOAL_THEN “&0 <= k'” MP_TAC THENL
347 [FIRST_ASSUM(MP_TAC o SPEC “k / &2”) THEN
348 MP_TAC(ONCE_REWRITE_RULE[GSYM REAL_LT_HALF1] (ASSUME “&0 < k”)) THEN
349 DISCH_THEN(fn th => ASSUME_TAC th THEN MP_TAC th) THEN
350 DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_IMP_LE) THEN
351 DISCH_THEN(fn th => REWRITE_TAC[th, abs]) THEN
352 REWRITE_TAC[GSYM abs] THEN
353 ASM_REWRITE_TAC[REAL_LT_HALF1, REAL_LT_HALF2] THEN DISCH_TAC THEN
354 MP_TAC(GEN_ALL(MATCH_MP REAL_LE_RMUL (ASSUME “&0 < k / &2”))) THEN
355 DISCH_THEN(fn th => GEN_REWR_TAC I [GSYM th]) THEN
356 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “abs(f(k / &2))” THEN
357 ASM_REWRITE_TAC[REAL_MUL_LZERO, ABS_POS], ALL_TAC] THEN
358 DISCH_THEN(DISJ_CASES_TAC o REWRITE_RULE[REAL_LE_LT]) THEN
359 X_GEN_TAC “e:real” THEN DISCH_TAC THENL
360 [ALL_TAC, EXISTS_TAC “k:real” THEN REWRITE_TAC[ASSUME “&0 < k”] THEN
361 GEN_TAC THEN DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
362 FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[REAL_MUL_LZERO] THEN
363 DISCH_THEN(MP_TAC o C CONJ(SPEC “(f:real->real) x” ABS_POS)) THEN
364 REWRITE_TAC[REAL_LE_ANTISYM] THEN DISCH_THEN SUBST1_TAC THEN
365 FIRST_ASSUM ACCEPT_TAC] THEN
366 SUBGOAL_THEN “&0 < (e / k') / &2” ASSUME_TAC THENL
367 [REWRITE_TAC[real_div] THEN
368 REPEAT(MATCH_MP_TAC REAL_LT_MUL THEN CONJ_TAC) THEN
369 TRY(MATCH_MP_TAC REAL_INV_POS) THEN ASM_REWRITE_TAC[] THEN
370 REWRITE_TAC[REAL_LT, TWO, LESS_0], ALL_TAC] THEN
371 MP_TAC(SPECL [“(e / k') / &2”, “k:real”] REAL_DOWN2) THEN
372 ASM_REWRITE_TAC[] THEN
373 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
374 EXISTS_TAC “d:real” THEN ASM_REWRITE_TAC[] THEN
375 X_GEN_TAC “h:real” THEN DISCH_TAC THEN
376 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “k' * abs(h)” THEN CONJ_TAC THENL
377 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
378 MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC “d:real” THEN
379 ASM_REWRITE_TAC[],
380 MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC “k' * d” THEN
381 ASM_REWRITE_TAC[MATCH_MP REAL_LT_LMUL (ASSUME “&0 < k'”)] THEN
382 ONCE_REWRITE_TAC[GSYM(MATCH_MP REAL_LT_RDIV (ASSUME “&0 < k'”))] THEN
383 REWRITE_TAC[real_div] THEN
384 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
385 “(a * b) * c = (c * a) * b”] THEN
386 ASSUME_TAC(GSYM(MATCH_MP REAL_LT_IMP_NE (ASSUME “&0 < k'”))) THEN
387 REWRITE_TAC[MATCH_MP REAL_MUL_LINV (ASSUME “~(k' = &0)”)] THEN
388 REWRITE_TAC[REAL_MUL_LID] THEN
389 MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC “(e / k') / &2” THEN
390 ASM_REWRITE_TAC[GSYM real_div] THEN REWRITE_TAC[REAL_LT_HALF2] THEN
391 ONCE_REWRITE_TAC[GSYM REAL_LT_HALF1] THEN ASM_REWRITE_TAC[]]
392QED
393
394Theorem TERMDIFF_LEMMA5:
395 !f g k.
396 &0 < k /\
397 summable(f) /\
398 (!h. &0 < abs(h) /\ abs(h) < k
399 ==> !n. abs(g(h) n) <= (f(n) * abs(h)))
400 ==> ((\h. suminf(g h)) -> &0)(&0)
401Proof
402 REPEAT GEN_TAC THEN
403 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
404 DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o MATCH_MP SUMMABLE_SUM) MP_TAC) THEN
405 ASSUME_TAC((GEN “h:real” o SPEC “abs(h)” o
406 MATCH_MP SER_CMUL) (ASSUME “f sums (suminf f)”)) THEN
407 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[REAL_MUL_SYM]) THEN
408 FIRST_ASSUM(ASSUME_TAC o GEN “h:real” o
409 MATCH_MP SUM_UNIQ o SPEC “h:real”) THEN DISCH_TAC THEN
410 C SUBGOAL_THEN ASSUME_TAC “!h. &0 < abs(h) /\ abs(h) < k ==>
411 abs(suminf(g h)) <= (suminf(f) * abs(h))” THENL
412 [GEN_TAC THEN DISCH_THEN(fn th => ASSUME_TAC th THEN
413 FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN DISCH_TAC THEN
414 SUBGOAL_THEN “summable(\n. f(n) * abs(h))” ASSUME_TAC THENL
415 [MATCH_MP_TAC SUM_SUMMABLE THEN
416 EXISTS_TAC “suminf(f) * abs(h)” THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
417 SUBGOAL_THEN “summable(\n. abs(g(h:real)(n:num)))” ASSUME_TAC THENL
418 [MATCH_MP_TAC SER_COMPAR THEN
419 EXISTS_TAC “\n:num. f(n) * abs(h)” THEN ASM_REWRITE_TAC[] THEN
420 EXISTS_TAC “0:num” THEN X_GEN_TAC “n:num” THEN
421 DISCH_THEN(K ALL_TAC) THEN BETA_TAC THEN
422 REWRITE_TAC[ABS_ABS] THEN FIRST_ASSUM MATCH_MP_TAC THEN
423 ASM_REWRITE_TAC[], ALL_TAC] THEN
424 MATCH_MP_TAC REAL_LE_TRANS THEN
425 EXISTS_TAC “suminf(\n. abs(g(h:real)(n:num)))” THEN CONJ_TAC THENL
426 [MATCH_MP_TAC SER_ABS THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
427 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SER_LE THEN
428 REPEAT CONJ_TAC THEN TRY(FIRST_ASSUM ACCEPT_TAC) THEN
429 GEN_TAC THEN BETA_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
430 ASM_REWRITE_TAC[], ALL_TAC] THEN
431 MATCH_MP_TAC TERMDIFF_LEMMA4 THEN
432 MAP_EVERY EXISTS_TAC [“suminf(f)”, “k:real”] THEN
433 BETA_TAC THEN ASM_REWRITE_TAC[]
434QED
435
436Theorem TERMDIFF:
437 !c k' x.
438 summable(\n. c(n) * (k' pow n)) /\
439 summable(\n. (diffs c)(n) * (k' pow n)) /\
440 summable(\n. (diffs(diffs c))(n) * (k' pow n)) /\
441 abs(x) < abs(k')
442 ==> ((\x. suminf (\n. c(n) * (x pow n)))
443 diffl
444 (suminf (\n. (diffs c)(n) * (x pow n)))) (x)
445Proof
446 REPEAT GEN_TAC THEN STRIP_TAC THEN
447 REWRITE_TAC[diffl] THEN BETA_TAC THEN
448 MATCH_MP_TAC LIM_TRANSFORM THEN
449 EXISTS_TAC
450 “\h. suminf(\n. ((c(n) * ((x + h) pow n)) -
451 (c(n) * (x pow n))) / h)” THEN CONJ_TAC
452 THENL
453 [BETA_TAC THEN REWRITE_TAC[LIM] THEN BETA_TAC THEN
454 REWRITE_TAC[REAL_SUB_RZERO] THEN X_GEN_TAC “e:real” THEN
455 DISCH_TAC THEN EXISTS_TAC “abs(k') - abs(x)” THEN
456 REWRITE_TAC[REAL_SUB_LT] THEN
457 ASM_REWRITE_TAC[] THEN X_GEN_TAC “h:real” THEN
458 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
459 DISCH_THEN(ASSUME_TAC o MATCH_MP ABS_CIRCLE) THEN
460 W(fn (asl,w) => SUBGOAL_THEN (mk_eq(rand(rator w),“&0”)) SUBST1_TAC)
461 THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ABS_ZERO] THEN
462 REWRITE_TAC[REAL_SUB_0] THEN C SUBGOAL_THEN MP_TAC
463 “(\n. (c n) * (x pow n)) sums
464 (suminf(\n. (c n) * (x pow n))) /\
465 (\n. (c n) * ((x + h) pow n)) sums
466 (suminf(\n. (c n) * ((x + h) pow n)))”
467 THENL
468 [CONJ_TAC THEN MATCH_MP_TAC SUMMABLE_SUM THEN
469 MATCH_MP_TAC POWSER_INSIDE THEN EXISTS_TAC “k':real” THEN
470 ASM_REWRITE_TAC[], ALL_TAC] THEN
471 ONCE_REWRITE_TAC[CONJ_SYM] THEN
472 DISCH_THEN(MP_TAC o MATCH_MP SER_SUB) THEN BETA_TAC THEN
473 DISCH_THEN(MP_TAC o SPEC “h:real” o MATCH_MP SER_CDIV) THEN
474 BETA_TAC THEN DISCH_THEN(ACCEPT_TAC o MATCH_MP SUM_UNIQ), ALL_TAC]
475 THEN
476 ONCE_REWRITE_TAC[LIM_NULL] THEN BETA_TAC THEN
477 MATCH_MP_TAC LIM_TRANSFORM THEN EXISTS_TAC
478 “\h. suminf
479 (\n. c(n) *
480 (((((x + h) pow n) - (x pow n)) / h)
481 - (&n * (x pow (n - 1)))))” THEN
482 BETA_TAC THEN CONJ_TAC
483 THENL
484 [REWRITE_TAC[LIM] THEN X_GEN_TAC “e:real” THEN DISCH_TAC THEN
485 EXISTS_TAC “abs(k') - abs(x)” THEN
486 REWRITE_TAC[REAL_SUB_LT] THEN
487 ASM_REWRITE_TAC[] THEN X_GEN_TAC “h:real” THEN
488 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
489 DISCH_THEN(ASSUME_TAC o MATCH_MP ABS_CIRCLE) THEN
490 W(fn (asl,w) => SUBGOAL_THEN (mk_eq(rand(rator w),“&0”)) SUBST1_TAC)
491 THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_SUB_RZERO, ABS_ZERO] THEN
492 BETA_TAC THEN REWRITE_TAC[REAL_SUB_0] THEN
493 SUBGOAL_THEN “summable(\n. (diffs c)(n) * (x pow n))” MP_TAC
494 THENL
495 [MATCH_MP_TAC POWSER_INSIDE THEN EXISTS_TAC “k':real” THEN
496 ASM_REWRITE_TAC[], ALL_TAC] THEN
497 DISCH_THEN(fn th => ASSUME_TAC th THEN MP_TAC (MATCH_MP DIFFS_EQUIV th))
498 THEN DISCH_THEN(fn th => SUBST1_TAC (MATCH_MP SUM_UNIQ th) THEN MP_TAC th)
499 THEN RULE_ASSUM_TAC(REWRITE_RULE[REAL_SUB_RZERO]) THEN
500 C SUBGOAL_THEN MP_TAC
501 “(\n. (c n) * (x pow n)) sums
502 (suminf(\n. (c n) * (x pow n))) /\
503 (\n. (c n) * ((x + h) pow n)) sums
504 (suminf(\n. (c n) * ((x + h) pow n)))”
505 THENL
506 [CONJ_TAC THEN MATCH_MP_TAC SUMMABLE_SUM THEN
507 MATCH_MP_TAC POWSER_INSIDE THEN EXISTS_TAC “k':real” THEN
508 ASM_REWRITE_TAC[], ALL_TAC] THEN
509 ONCE_REWRITE_TAC[CONJ_SYM] THEN
510 DISCH_THEN(MP_TAC o MATCH_MP SER_SUB) THEN BETA_TAC THEN
511 DISCH_THEN(MP_TAC o SPEC “h:real” o MATCH_MP SER_CDIV) THEN
512 DISCH_THEN(MP_TAC o MATCH_MP SUMMABLE_SUM o MATCH_MP SUM_SUMMABLE) THEN
513 BETA_TAC THEN DISCH_THEN(fn th => DISCH_THEN (MP_TAC o
514 MATCH_MP SUMMABLE_SUM o MATCH_MP SUM_SUMMABLE) THEN MP_TAC th) THEN
515 DISCH_THEN(fn th1 => DISCH_THEN(fn th2 => MP_TAC(CONJ th1 th2))) THEN
516 DISCH_THEN(MP_TAC o MATCH_MP SER_SUB) THEN BETA_TAC THEN
517 DISCH_THEN(SUBST1_TAC o MATCH_MP SUM_UNIQ) THEN AP_TERM_TAC THEN
518 ABS_TAC THEN REWRITE_TAC[real_div] THEN
519 REWRITE_TAC[REAL_SUB_LDISTRIB, REAL_SUB_RDISTRIB] THEN
520 REWRITE_TAC[REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
521 AP_THM_TAC THEN AP_TERM_TAC THEN (* break *)
522 MATCH_ACCEPT_TAC REAL_MUL_SYM,
523 ALL_TAC] THEN
524 MP_TAC(SPECL [“abs(x)”, “abs(k')”] REAL_MEAN) THEN
525 ASM_REWRITE_TAC[] THEN
526 DISCH_THEN(X_CHOOSE_THEN “R:real” STRIP_ASSUME_TAC) THEN
527 MP_TAC(SPECL
528 [“\n. abs(c n) * (&n * (&(n - 1) * (R pow (n - 2))))”,
529 “\h n. c(n) * (((((x + h) pow n) - (x pow n)) / h)
530 -
531 (&n * (x pow (n - 1))))”,
532 “R - abs(x)”] TERMDIFF_LEMMA5) THEN
533 BETA_TAC THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN
534 DISCH_THEN MATCH_MP_TAC THEN REPEAT CONJ_TAC
535 THENL
536 [ASM_REWRITE_TAC[REAL_SUB_LT],
537 SUBGOAL_THEN “summable(\n. abs(diffs(diffs c) n) * (R pow n))”
538 MP_TAC
539 THENL
540 [MATCH_MP_TAC POWSER_INSIDEA THEN
541 EXISTS_TAC “k':real” THEN ASM_REWRITE_TAC[] THEN
542 SUBGOAL_THEN “abs(R) = R” (fn th => ASM_REWRITE_TAC[th]) THEN
543 REWRITE_TAC[ABS_REFL] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
544 EXISTS_TAC “abs(x)” THEN REWRITE_TAC[ABS_POS] THEN
545 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
546 REWRITE_TAC[diffs] THEN BETA_TAC THEN REWRITE_TAC[ABS_MUL] THEN
547 REWRITE_TAC[ABS_N] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
548 C SUBGOAL_THEN (fn th => ONCE_REWRITE_TAC[GSYM th])
549 “!n. diffs(diffs (\n. abs(c n))) n * (R pow n) =
550 &(SUC n) * (&(SUC(SUC n)) * (abs(c(SUC(SUC n)))
551 * (R pow n)))”
552 THENL
553 [GEN_TAC THEN REWRITE_TAC[diffs] THEN BETA_TAC THEN
554 REWRITE_TAC[REAL_MUL_ASSOC], ALL_TAC] THEN
555 DISCH_THEN(MP_TAC o MATCH_MP DIFFS_EQUIV) THEN
556 DISCH_THEN(MP_TAC o MATCH_MP SUM_SUMMABLE) THEN
557 REWRITE_TAC[diffs] THEN BETA_TAC THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
558 SUBGOAL_THEN “(\n. &n * (&(SUC n) * (abs(c(SUC n))
559 * (R pow (n - 1))))) =
560 \n. diffs(\m. &(m - 1) * (abs(c m) / R)) n * (R pow n)”
561 SUBST1_TAC
562 THENL
563 [REWRITE_TAC[diffs] THEN BETA_TAC THEN REWRITE_TAC[SUC_SUB1] THEN
564 ABS_TAC THEN
565 DISJ_CASES_THEN2 (SUBST1_TAC) (X_CHOOSE_THEN “m:num” SUBST1_TAC)
566 (SPEC “n:num” num_CASES) THEN
567 REWRITE_TAC[REAL_MUL_LZERO, REAL_MUL_RZERO, SUC_SUB1] THEN
568 REWRITE_TAC[ADD1, POW_ADD] THEN REWRITE_TAC[GSYM ADD1, POW_1] THEN
569 REWRITE_TAC[GSYM REAL_MUL_ASSOC, real_div] THEN
570 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
571 “a * (b * (c * (d * (e * f)))) =
572 b * (a * (c * (e * (d * f))))”] THEN
573 REPEAT AP_TERM_TAC THEN SUBGOAL_THEN “inv(R) * R = &1”
574 SUBST1_TAC
575 THENL
576 [MATCH_MP_TAC REAL_MUL_LINV THEN REWRITE_TAC[ABS_NZ] THEN
577 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “abs(x)” THEN
578 ASM_REWRITE_TAC[ABS_POS] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
579 EXISTS_TAC “R:real” THEN ASM_REWRITE_TAC[ABS_LE],
580 REWRITE_TAC[REAL_MUL_RID]], ALL_TAC]
581 THEN
582 DISCH_THEN(MP_TAC o MATCH_MP DIFFS_EQUIV) THEN BETA_TAC THEN
583 DISCH_THEN(MP_TAC o MATCH_MP SUM_SUMMABLE) THEN
584 MATCH_MP_TAC (TAUT_CONV “(a = b) ==> a ==> b”) THEN AP_TERM_TAC THEN
585 CONV_TAC(X_FUN_EQ_CONV “n:num”) THEN BETA_TAC THEN GEN_TAC THEN
586 REWRITE_TAC[real_div, GSYM REAL_MUL_ASSOC] THEN
587 GEN_REWR_TAC RAND_CONV
588 [AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
589 “a * (b * (c * d)) = b * (c * (a * d))”] THEN
590 DISJ_CASES_THEN2 SUBST1_TAC (X_CHOOSE_THEN “m:num” SUBST1_TAC)
591 (SPEC “n:num” num_CASES) THEN REWRITE_TAC[REAL_MUL_LZERO] THEN
592 REWRITE_TAC[TWO, SUC_SUB1, SUB_MONO_EQ] THEN
593 AP_TERM_TAC THEN
594 DISJ_CASES_THEN2 SUBST1_TAC (X_CHOOSE_THEN “n:num” SUBST1_TAC)
595 (SPEC “m:num” num_CASES) THEN REWRITE_TAC[REAL_MUL_LZERO] THEN
596 REPEAT AP_TERM_TAC THEN REWRITE_TAC[SUC_SUB1] THEN
597 REWRITE_TAC[ADD1, POW_ADD, POW_1] THEN
598 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
599 SUBGOAL_THEN “R * inv(R) = &1”
600 (fn th => REWRITE_TAC[th, REAL_MUL_RID]) THEN
601 MATCH_MP_TAC REAL_MUL_RINV THEN CONV_TAC(RAND_CONV SYM_CONV) THEN
602 MATCH_MP_TAC REAL_LT_IMP_NE THEN MATCH_MP_TAC REAL_LET_TRANS THEN
603 EXISTS_TAC “abs(x)” THEN ASM_REWRITE_TAC[ABS_POS],
604
605 X_GEN_TAC “h:real” THEN DISCH_TAC THEN X_GEN_TAC “n:num” THEN
606 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[ABS_MUL] THEN
607 MATCH_MP_TAC REAL_LE_LMUL_IMP THEN REWRITE_TAC[ABS_POS] THEN
608 MATCH_MP_TAC TERMDIFF_LEMMA3 THEN ASM_REWRITE_TAC[ABS_NZ] THEN
609 CONJ_TAC THENL
610 [MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[],
611 MATCH_MP_TAC REAL_LE_TRANS THEN
612 EXISTS_TAC “abs(x) + abs(h)” THEN
613 REWRITE_TAC[ABS_TRIANGLE] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN
614 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
615 ASM_REWRITE_TAC[GSYM REAL_LT_SUB_LADD]]]
616QED
617