limScript.sml
1(*===========================================================================*)
2(* Theory of limits, continuity and differentiation of real->real functions *)
3(*===========================================================================*)
4
5Theory lim
6Ancestors
7 pair arithmetic num prim_rec real metric nets combin pred_set
8 topology real_topology derivative seq
9Libs
10 numLib reduceLib pairLib jrhUtils realLib mesonLib hurdUtils
11
12val _ = ParseExtras.temp_loose_equality()
13
14val _ = Parse.reveal "B";
15
16val tendsto = netsTheory.tendsto; (* conflict with real_topologyTheory.tendsto *)
17val EXACT_CONV = jrhUtils.EXACT_CONV; (* there's one also in hurdUtils *)
18
19(*---------------------------------------------------------------------------*)
20(* Specialize nets theorems to the pointwise limit of real->real functions *)
21(*---------------------------------------------------------------------------*)
22
23Definition tends_real_real :
24 (tends_real_real f l)(x0) =
25 (f tends l)(mtop(mr1),tendsto(mr1,x0))
26End
27
28val _ = add_infix("->", 250, HOLgrammars.RIGHT)
29Overload "->" = ``tends_real_real``
30
31Theorem LIM:
32 !f y0 x0. (f -> y0)(x0) =
33 !e. &0 < e ==>
34 ?d. &0 < d /\ !x. &0 < abs(x - x0) /\ abs(x - x0) < d ==>
35 abs(f(x) - y0) < e
36Proof
37 REPEAT GEN_TAC THEN
38 REWRITE_TAC[tends_real_real, MATCH_MP LIM_TENDS2 (SPEC “x0:real” MR1_LIMPT)]
39 THEN REWRITE_TAC[MR1_DEF] THEN
40 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ABS_SUB] THEN
41 REFL_TAC
42QED
43
44(* connection to real_topologyTheory *)
45Theorem LIM_AT_LIM :
46 !f l a. (f --> l) (at a) <=> (f -> l)(a)
47Proof
48 REWRITE_TAC [LIM_AT, LIM, dist]
49QED
50
51Theorem LIM_CONST :
52 !k x. ((\x. k) -> k)(x)
53Proof
54 rw [GSYM LIM_AT_LIM, real_topologyTheory.LIM_CONST]
55QED
56
57Theorem LIM_ADD :
58 !f g l m x. (f -> l)(x) /\ (g -> m)(x) ==>
59 ((\x. f(x) + g(x)) -> (l + m))(x)
60Proof
61 rw [GSYM LIM_AT_LIM, real_topologyTheory.LIM_ADD]
62QED
63
64Theorem LIM_MUL :
65 !f g l m x. (f -> l)(x) /\ (g -> m)(x) ==>
66 ((\x. f(x) * g(x)) -> (l * m))(x)
67Proof
68 rw [GSYM LIM_AT_LIM, real_topologyTheory.LIM_MUL]
69QED
70
71Theorem LIM_NEG :
72 !f l x. (f -> l)(x) = ((\x. ~(f(x))) -> ~l)(x)
73Proof
74 REPEAT GEN_TAC THEN REWRITE_TAC[tends_real_real] THEN
75 MATCH_MP_TAC NET_NEG THEN MATCH_ACCEPT_TAC DORDER_TENDSTO
76QED
77
78Theorem LIM_INV :
79 !f l x. (f -> l)(x) /\ ~(l = &0) ==>
80 ((\x. inv(f(x))) -> inv l)(x)
81Proof
82 rw [GSYM LIM_AT_LIM,
83 REWRITE_RULE [o_DEF] real_topologyTheory.LIM_INV]
84QED
85
86Theorem LIM_SUB :
87 !f g l m x. (f -> l)(x) /\ (g -> m)(x) ==>
88 ((\x. f(x) - g(x)) -> (l - m))(x)
89Proof
90 rw [GSYM LIM_AT_LIM, real_topologyTheory.LIM_SUB]
91QED
92
93Theorem LIM_DIV :
94 !f g l m x. (f -> l)(x) /\ (g -> m)(x) /\ ~(m = &0) ==>
95 ((\x. f(x) / g(x)) -> (l / m))(x)
96Proof
97 REPEAT GEN_TAC THEN REWRITE_TAC[tends_real_real] THEN
98 MATCH_MP_TAC NET_DIV THEN MATCH_ACCEPT_TAC DORDER_TENDSTO
99QED
100
101Theorem LIM_NULL :
102 !f l x. (f -> l)(x) = ((\x. f(x) - l) -> &0)(x)
103Proof
104 rw [GSYM LIM_AT_LIM, Once real_topologyTheory.LIM_NULL]
105QED
106
107(*---------------------------------------------------------------------------*)
108(* One extra theorem is handy *)
109(*---------------------------------------------------------------------------*)
110
111Theorem LIM_X:
112 !x0. ((\x. x) -> x0)(x0)
113Proof
114 GEN_TAC THEN REWRITE_TAC[LIM] THEN X_GEN_TAC “e:real” THEN
115 DISCH_TAC THEN EXISTS_TAC “e:real” THEN ASM_REWRITE_TAC[] THEN
116 BETA_TAC THEN GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[]
117QED
118
119(*---------------------------------------------------------------------------*)
120(* Uniqueness of limit *)
121(*---------------------------------------------------------------------------*)
122
123Theorem LIM_UNIQ:
124 !f l m x. (f -> l)(x) /\ (f -> m)(x) ==> (l = m)
125Proof
126 REPEAT GEN_TAC THEN REWRITE_TAC[tends_real_real] THEN
127 MATCH_MP_TAC MTOP_TENDS_UNIQ THEN
128 MATCH_ACCEPT_TAC DORDER_TENDSTO
129QED
130
131(*---------------------------------------------------------------------------*)
132(* Show that limits are equal when functions are equal except at limit point *)
133(*---------------------------------------------------------------------------*)
134
135Theorem LIM_EQUAL :
136 !f g l x0. (!x. ~(x = x0) ==> (f x = g x)) ==> ((f -> l)(x0) = (g -> l)(x0))
137Proof
138 rw [GSYM LIM_AT_LIM]
139 >> MATCH_MP_TAC (SIMP_RULE std_ss [ETA_THM] LIM_CONG_AT)
140 >> rw []
141QED
142
143(*---------------------------------------------------------------------------*)
144(* A more general theorem about rearranging the body of a limit *)
145(*---------------------------------------------------------------------------*)
146
147Theorem LIM_TRANSFORM :
148 !f g x0 l. ((\x. f(x) - g(x)) -> &0)(x0) /\ (g -> l)(x0)
149 ==> (f -> l)(x0)
150Proof
151 rw [GSYM LIM_AT_LIM]
152 >> Know ‘(f --> l) (at x0) <=> (g --> l) (at x0)’
153 >- (MATCH_MP_TAC LIM_TRANSFORM_EQ >> art [])
154 >> rw []
155QED
156
157(*---------------------------------------------------------------------------*)
158(* Define differentiation and continuity *)
159(*---------------------------------------------------------------------------*)
160
161val diffl = new_infixr_definition("diffl",
162“($diffl f l)(x) = ((\h. (f(x + h) - f(x)) / h) -> l)(&0)”,
163 750);
164
165(* connection with derivativeTheory, added by Chun Tian *)
166Theorem diffl_has_vector_derivative :
167 !f l x. ($diffl f l)(x) <=> (f has_vector_derivative l) (at x)
168Proof
169 rpt GEN_TAC
170 >> RW_TAC std_ss [diffl, has_vector_derivative, has_derivative_at, LIM_AT_LIM]
171 >> ASSUME_TAC (Q.SPEC ‘l’ (ONCE_REWRITE_RULE [REAL_MUL_COMM] LINEAR_SCALING))
172 >> EQ_TAC >> RW_TAC real_ss [LIM] (* 2 subgoals *)
173 >| [ (* goal 1 (of 2) *)
174 Q.PAT_X_ASSUM ‘!e. 0 < e ==> P’ (MP_TAC o (Q.SPEC ‘e’)) \\
175 RW_TAC std_ss [] \\
176 Q.EXISTS_TAC ‘d’ >> RW_TAC std_ss [] \\
177 Q.PAT_X_ASSUM ‘!h. 0 < abs h /\ abs h < d ==> P’
178 (MP_TAC o (Q.SPEC ‘y - x’)) \\
179 RW_TAC real_ss [] \\
180 ‘y - x <> 0’ by (CCONTR_TAC >> fs []) \\
181 ‘inv (abs (y - x)) = abs (inv (y - x))’ by PROVE_TAC [ABS_INV] >> POP_ORW \\
182 Know ‘abs (abs (inv (y - x)) * (f y - (f x + (y - x) * l))) =
183 abs (inv (y - x) * (f y - (f x + (y - x) * l)))’
184 >- (RW_TAC real_ss [ABS_MUL, ABS_ABS]) >> Rewr' \\
185 Suff ‘inv (y - x) * (f y - (f x + (y - x) * l)) = (f y - f x) / (y - x) - l’
186 >- RW_TAC std_ss [] \\
187 ONCE_REWRITE_TAC [REAL_MUL_COMM] \\
188 ‘f y - (f x + (y - x) * l) = (f y - f x) - l * (y - x)’ by REAL_ARITH_TAC \\
189 POP_ORW >> REWRITE_TAC [real_div] \\
190 GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites
191 [REAL_SUB_RDISTRIB] >> rw [],
192 (* goal 2 (of 2) *)
193 Q.PAT_X_ASSUM ‘!e. 0 < e ==> P’ (MP_TAC o (Q.SPEC ‘e’)) \\
194 RW_TAC std_ss [] \\
195 Q.EXISTS_TAC ‘d’ >> RW_TAC std_ss [] \\
196 Q.PAT_X_ASSUM ‘!y. 0 < abs (y - x) /\ abs (y - x) < d ==> P’
197 (MP_TAC o (Q.SPEC ‘x + h’)) >> RW_TAC real_ss [] \\
198 ‘h <> 0’ by PROVE_TAC [ABS_NZ] \\
199 ‘inv (abs h) = abs (inv h)’ by PROVE_TAC [ABS_INV] \\
200 POP_ASSUM (FULL_SIMP_TAC std_ss o wrap) \\
201 Know ‘abs (abs (inv h) * (f (x + h) - (f x + h * l))) =
202 abs (inv h * (f (x + h) - (f x + h * l)))’
203 >- (RW_TAC real_ss [ABS_MUL, ABS_ABS]) \\
204 DISCH_THEN (FULL_SIMP_TAC std_ss o wrap) \\
205 Suff ‘(f (x + h) - f x) / h - l = inv h * (f (x + h) - (f x + h * l))’
206 >- RW_TAC std_ss [] \\
207 ONCE_REWRITE_TAC [REAL_MUL_COMM] \\
208 ‘f (x + h) - (f x + h * l) = f (x + h) - f x - l * h’ by REAL_ARITH_TAC \\
209 POP_ORW >> REWRITE_TAC [real_div] \\
210 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) empty_rewrites
211 [REAL_SUB_RDISTRIB] >> rw [] ]
212QED
213
214(* |- !f l x.
215 (f has_vector_derivative l) (at x) <=>
216 ((\h. (f (x + h) - f x) / h) --> l) (at 0)
217 *)
218Theorem HAS_VECTOR_DERIVATIVE_ALT =
219 REWRITE_RULE [diffl, GSYM LIM_AT_LIM] (GSYM diffl_has_vector_derivative)
220
221(* |- !f l x. (f diffl l) x <=> (f has_derivative (\x. x * l)) (at x) *)
222Theorem diffl_has_derivative =
223 REWRITE_RULE [has_vector_derivative] diffl_has_vector_derivative
224
225Theorem diffl_has_derivative' :
226 !f l x. (f diffl l) x <=> (f has_derivative ($* l)) (at x)
227Proof
228 rw [diffl_has_derivative]
229 >> Suff ‘(\x. l * x) = $* l’ >- rw []
230 >> rw [FUN_EQ_THM, Once REAL_MUL_COMM]
231QED
232
233val contl = new_infixr_definition("contl",
234 “$contl f x = ((\h. f(x + h)) -> f(x))(&0)”, 750);
235
236(* connection with real_topologyTheory *)
237Theorem contl_eq_continuous_at :
238 !f x. f contl x <=> f continuous (at x)
239Proof
240 RW_TAC real_ss [contl, CONTINUOUS_AT, LIM_AT_LIM, LIM]
241 >> EQ_TAC >> RW_TAC std_ss []
242 >| [ (* goal 1 (of 2) *)
243 Q.PAT_X_ASSUM ‘!e. 0 < e ==> P’ (MP_TAC o (Q.SPEC ‘e’)) \\
244 RW_TAC std_ss [] \\
245 Q.EXISTS_TAC ‘d’ >> RW_TAC std_ss [] \\
246 Q.PAT_X_ASSUM ‘!h. 0 < abs h /\ abs h < d ==> P’
247 (MP_TAC o (Q.SPEC ‘x' - x’)) \\
248 RW_TAC real_ss [],
249 (* goal 2 (of 2) *)
250 Q.PAT_X_ASSUM ‘!e. 0 < e ==> P’ (MP_TAC o (Q.SPEC ‘e’)) \\
251 RW_TAC std_ss [] \\
252 Q.EXISTS_TAC ‘d’ >> RW_TAC std_ss [] \\
253 Q.PAT_X_ASSUM ‘!x'. 0 < abs (x' - x) /\ abs (x' - x) < d ==> P’
254 (MP_TAC o (Q.SPEC ‘x + h’)) \\
255 RW_TAC real_ss [] ]
256QED
257
258val _ = hide "differentiable";
259
260(* cf. derivativeTheory.differentiable *)
261val differentiable = new_infixr_definition("differentiable",
262 “$differentiable f x = ?l. (f diffl l)(x)”, 750);
263
264Theorem differentiable_has_vector_derivative :
265 !f x. f differentiable x <=> ?l. (f has_vector_derivative l) (at x)
266Proof
267 rw [differentiable, diffl_has_vector_derivative]
268QED
269
270(* The equivalence between ‘differentiable’ and ‘derivative$differentiable’ *)
271Theorem differentiable_alt :
272 !f x. f differentiable x <=> derivative$differentiable f (at x)
273Proof
274 rw [differentiable, diffl_has_derivative, derivativeTheory.differentiable]
275 >> EQ_TAC
276 >- (STRIP_TAC \\
277 Q.EXISTS_TAC ‘\x. l * x’ >> rw [])
278 >> DISCH_THEN (Q.X_CHOOSE_THEN ‘g’ ASSUME_TAC)
279 >> ‘linear g’ by PROVE_TAC [has_derivative]
280 >> ‘?l. g = \x. l * x’ by METIS_TAC [linear_repr]
281 >> Q.EXISTS_TAC ‘l’ >> rw []
282QED
283
284(*---------------------------------------------------------------------------*)
285(* Derivative is unique *)
286(*---------------------------------------------------------------------------*)
287
288Theorem DIFF_UNIQ:
289 !f l m x. (f diffl l)(x) /\ (f diffl m)(x) ==> (l = m)
290Proof
291 REPEAT GEN_TAC THEN REWRITE_TAC[diffl] THEN
292 MATCH_ACCEPT_TAC LIM_UNIQ
293QED
294
295(*---------------------------------------------------------------------------*)
296(* Differentiability implies continuity *)
297(*---------------------------------------------------------------------------*)
298
299Theorem DIFF_CONT :
300 !f l x. ($diffl f l)(x) ==> $contl f x
301Proof
302 rw [contl_eq_continuous_at, diffl_has_derivative]
303 >> MATCH_MP_TAC DIFFERENTIABLE_IMP_CONTINUOUS_AT
304 >> rw [derivativeTheory.differentiable]
305 >> Q.EXISTS_TAC ‘\x. l * x’ >> art []
306QED
307
308(*---------------------------------------------------------------------------*)
309(* Alternative definition of continuity *)
310(*---------------------------------------------------------------------------*)
311
312Theorem CONTL_LIM :
313 !f x. f contl x = (f -> f(x))(x)
314Proof
315 rw [contl_eq_continuous_at, CONTINUOUS_AT, LIM_AT_LIM]
316QED
317
318(*---------------------------------------------------------------------------*)
319(* Alternative (Carathe'odory) definition of derivative *)
320(*---------------------------------------------------------------------------*)
321
322Theorem DIFF_CARAT:
323 !f l x. (f diffl l)(x) =
324 ?g. (!z. f(z) - f(x) = g(z) * (z - x)) /\ g contl x /\ (g(x) = l)
325Proof
326 REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
327 [EXISTS_TAC “\z. if (z = x) then l
328 else (f(z) - f(x)) / (z - x)” THEN
329 BETA_TAC THEN REWRITE_TAC[] THEN CONJ_TAC THENL
330 [X_GEN_TAC “z:real” THEN COND_CASES_TAC THEN
331 ASM_REWRITE_TAC[REAL_SUB_REFL, REAL_MUL_RZERO] THEN
332 CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_RMUL THEN
333 ASM_REWRITE_TAC[REAL_SUB_0],
334 POP_ASSUM MP_TAC THEN MATCH_MP_TAC(TAUT_CONV “(a = b) ==> a ==> b”) THEN
335 REWRITE_TAC[diffl, contl] THEN BETA_TAC THEN REWRITE_TAC[] THEN
336 MATCH_MP_TAC LIM_EQUAL THEN GEN_TAC THEN DISCH_TAC THEN BETA_TAC THEN
337 ASM_REWRITE_TAC[REAL_ADD_RID_UNIQ, REAL_ADD_SUB]],
338 POP_ASSUM(X_CHOOSE_THEN “g:real->real” STRIP_ASSUME_TAC) THEN
339 FIRST_ASSUM(UNDISCH_TAC o assert is_eq o concl) THEN
340 DISCH_THEN(SUBST1_TAC o SYM) THEN UNDISCH_TAC “g contl x” THEN
341 ASM_REWRITE_TAC[contl, diffl, REAL_ADD_SUB] THEN
342 MATCH_MP_TAC(TAUT_CONV “(a = b) ==> a ==> b”) THEN
343 MATCH_MP_TAC LIM_EQUAL THEN GEN_TAC THEN DISCH_TAC THEN BETA_TAC THEN
344 REWRITE_TAC[real_div, GSYM REAL_MUL_ASSOC] THEN
345 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_RINV th]) THEN
346 REWRITE_TAC[REAL_MUL_RID]]
347QED
348
349(*---------------------------------------------------------------------------*)
350(* Simple combining theorems for continuity, including composition *)
351(*---------------------------------------------------------------------------*)
352
353Theorem CONT_CONST:
354 !k x. $contl (\x. k) x
355Proof
356 REPEAT GEN_TAC THEN REWRITE_TAC[CONTL_LIM] THEN
357 MATCH_ACCEPT_TAC LIM_CONST
358QED
359
360Theorem CONT_ADD:
361 !f g x. $contl f x /\ $contl g x ==> $contl (\x. f(x) + g(x)) x
362Proof
363 REPEAT GEN_TAC THEN REWRITE_TAC[CONTL_LIM] THEN BETA_TAC THEN
364 MATCH_ACCEPT_TAC LIM_ADD
365QED
366
367Theorem CONT_MUL:
368 !f g x. $contl f x /\ $contl g x ==> $contl (\x. f(x) * g(x)) x
369Proof
370 REPEAT GEN_TAC THEN REWRITE_TAC[CONTL_LIM] THEN BETA_TAC THEN
371 MATCH_ACCEPT_TAC LIM_MUL
372QED
373
374Theorem CONT_NEG:
375 !f x. $contl f x ==> $contl (\x. ~(f(x))) x
376Proof
377 REPEAT GEN_TAC THEN REWRITE_TAC[CONTL_LIM] THEN BETA_TAC THEN
378 REWRITE_TAC[GSYM LIM_NEG]
379QED
380
381Theorem CONT_INV:
382 !f x. $contl f x /\ ~(f x = &0) ==> $contl (\x. inv(f(x))) x
383Proof
384 REPEAT GEN_TAC THEN REWRITE_TAC[CONTL_LIM] THEN BETA_TAC THEN
385 MATCH_ACCEPT_TAC LIM_INV
386QED
387
388Theorem CONT_SUB:
389 !f g x. $contl f x /\ $contl g x ==> $contl (\x. f(x) - g(x)) x
390Proof
391 REPEAT GEN_TAC THEN REWRITE_TAC[CONTL_LIM] THEN BETA_TAC THEN
392 MATCH_ACCEPT_TAC LIM_SUB
393QED
394
395Theorem CONT_DIV:
396 !f g x. $contl f x /\ $contl g x /\ ~(g x = &0) ==>
397 $contl (\x. f(x) / g(x)) x
398Proof
399 REPEAT GEN_TAC THEN REWRITE_TAC[CONTL_LIM] THEN BETA_TAC THEN
400 MATCH_ACCEPT_TAC LIM_DIV
401QED
402
403(* ------------------------------------------------------------------------- *)
404(* Composition of continuous functions is continuous. *)
405(* ------------------------------------------------------------------------- *)
406
407Theorem CONT_COMPOSE :
408 !f g x. f contl x /\ g contl (f x) ==> (\x. g(f x)) contl x
409Proof
410 rw [contl_eq_continuous_at]
411 >> MATCH_MP_TAC (REWRITE_RULE [o_DEF] CONTINUOUS_AT_COMPOSE) >> art []
412QED
413
414(*---------------------------------------------------------------------------*)
415(* Intermediate Value Theorem (we prove contrapositive by bisection) *)
416(*---------------------------------------------------------------------------*)
417
418Theorem IVT :
419 !f a b y. a <= b /\ (f(a) <= y /\ y <= f(b)) /\
420 (!x. a <= x /\ x <= b ==> f contl x)
421 ==> (?x. a <= x /\ x <= b /\ (f(x) = y))
422Proof
423 rw [contl_eq_continuous_at]
424 >> fs [CONJ_ASSOC, GSYM IN_INTERVAL]
425 >> ‘f continuous_on interval [a,b]’
426 by (MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON >> rw [])
427 >> MATCH_MP_TAC CONTINUOUS_ON_IVT >> art []
428QED
429
430(*---------------------------------------------------------------------------*)
431(* Intermediate value theorem where value at the left end is bigger *)
432(*---------------------------------------------------------------------------*)
433
434Theorem IVT2:
435 !f a b y. a <= b /\ (f(b) <= y /\ y <= f(a)) /\
436 (!x. a <= x /\ x <= b ==> $contl f x) ==>
437 ?x. a <= x /\ x <= b /\ (f(x) = y)
438Proof
439 REPEAT GEN_TAC THEN STRIP_TAC THEN
440 MP_TAC(Q.SPECL [‘\x:real. ~(f x)’, ‘a’, ‘b:real’, ‘-y’] IVT)
441 THEN BETA_TAC THEN ASM_REWRITE_TAC[REAL_LE_NEG, REAL_EQ_NEG, REAL_NEGNEG]
442 THEN DISCH_THEN MATCH_MP_TAC THEN GEN_TAC THEN DISCH_TAC THEN
443 MATCH_MP_TAC CONT_NEG THEN FIRST_ASSUM MATCH_MP_TAC THEN
444 ASM_REWRITE_TAC[]
445QED
446
447(*---------------------------------------------------------------------------*)
448(* Prove the simple combining theorems for differentiation *)
449(*---------------------------------------------------------------------------*)
450
451Theorem DIFF_CONST:
452 !k x. ((\x. k) diffl &0)(x)
453Proof
454 REPEAT GEN_TAC THEN REWRITE_TAC[diffl] THEN
455 REWRITE_TAC[REAL_SUB_REFL, real_div, REAL_MUL_LZERO] THEN
456 MATCH_ACCEPT_TAC LIM_CONST
457QED
458
459Theorem DIFF_ADD:
460 !f g l m x. (f diffl l)(x) /\ (g diffl m)(x) ==>
461 ((\x. f(x) + g(x)) diffl (l + m))(x)
462Proof
463 REPEAT GEN_TAC THEN REWRITE_TAC[diffl] THEN
464 DISCH_TAC THEN BETA_TAC THEN
465 REWRITE_TAC[REAL_ADD2_SUB2] THEN
466 REWRITE_TAC[real_div, REAL_RDISTRIB] THEN
467 REWRITE_TAC[GSYM real_div] THEN
468 CONV_TAC(EXACT_CONV[X_BETA_CONV “h:real” “(f(x + h) - f(x)) / h”]) THEN
469 CONV_TAC(EXACT_CONV[X_BETA_CONV “h:real” “(g(x + h) - g(x)) / h”]) THEN
470 MATCH_MP_TAC LIM_ADD THEN ASM_REWRITE_TAC[]
471QED
472
473Theorem DIFF_MUL:
474 !f g l m x. (f diffl l)(x) /\ (g diffl m)(x) ==>
475 ((\x. f(x) * g(x)) diffl ((l * g(x)) + (m * f(x))))(x)
476Proof
477 REPEAT GEN_TAC THEN REWRITE_TAC[diffl] THEN
478 DISCH_TAC THEN BETA_TAC THEN SUBGOAL_THEN
479 “!a b c d. (a * b) - (c * d) = ((a * b) - (a * d)) + ((a * d) - (c * d))”
480 (fn th => ONCE_REWRITE_TAC[hol88Lib.GEN_ALL th]) THENL
481 [REWRITE_TAC[real_sub] THEN
482 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM)
483 “(a + b) + (c + d) = (b + c) + (a + d)”] THEN
484 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID], ALL_TAC] THEN
485 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB, GSYM REAL_SUB_RDISTRIB] THEN SUBGOAL_THEN
486 “!a b c d e. ((a * b) + (c * d)) / e = ((b / e) * a) + ((c / e) * d)”
487 (fn th => ONCE_REWRITE_TAC[th]) THENL
488 [REPEAT GEN_TAC THEN REWRITE_TAC[real_div] THEN
489 REWRITE_TAC[REAL_RDISTRIB] THEN BINOP_TAC THEN
490 CONV_TAC(AC_CONV(REAL_MUL_ASSOC,REAL_MUL_SYM)), ALL_TAC] THEN
491 GEN_REWR_TAC LAND_CONV [REAL_ADD_SYM] THEN
492 CONV_TAC(EXACT_CONV(map (X_BETA_CONV “h:real”)
493 [“((g(x + h) - g(x)) / h) * f(x + h)”,
494 “((f(x + h) - f(x)) / h) * g(x)”])) THEN
495 MATCH_MP_TAC LIM_ADD THEN
496 CONV_TAC(EXACT_CONV(map (X_BETA_CONV “h:real”)
497 [“(g(x + h) - g(x)) / h”, “f(x + h):real”,
498 “(f(x + h) - f(x)) / h”, “g(x:real):real”])) THEN
499 CONJ_TAC THEN MATCH_MP_TAC LIM_MUL THEN
500 BETA_TAC THEN ASM_REWRITE_TAC[LIM_CONST] THEN
501 REWRITE_TAC[GSYM contl] THEN
502 MATCH_MP_TAC DIFF_CONT THEN EXISTS_TAC “l:real” THEN
503 ASM_REWRITE_TAC[diffl]
504QED
505
506Theorem DIFF_CMUL:
507 !f c l x. (f diffl l)(x) ==> ((\x. c * f(x)) diffl (c * l))(x)
508Proof
509 REPEAT GEN_TAC THEN
510 DISCH_THEN(MP_TAC o CONJ (SPECL [“c:real”, “x:real”] DIFF_CONST)) THEN
511 DISCH_THEN(MP_TAC o MATCH_MP DIFF_MUL) THEN BETA_TAC THEN
512 REWRITE_TAC[REAL_MUL_LZERO, REAL_ADD_LID] THEN
513 MATCH_MP_TAC(TAUT_CONV(“(a = b) ==> a ==> b”)) THEN AP_THM_TAC THEN
514 GEN_REWR_TAC (RAND_CONV o RAND_CONV) [REAL_MUL_SYM] THEN
515 REWRITE_TAC[]
516QED
517
518Theorem DIFF_NEG:
519 !f l x. (f diffl l)(x) ==> ((\x. ~(f x)) diffl ~l)(x)
520Proof
521 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_NEG_MINUS1] THEN
522 MATCH_ACCEPT_TAC DIFF_CMUL
523QED
524
525Theorem DIFF_SUB:
526 !f g l m x. (f diffl l)(x) /\ (g diffl m)(x) ==>
527 ((\x. f(x) - g(x)) diffl (l - m))(x)
528Proof
529 REPEAT GEN_TAC THEN
530 DISCH_THEN(MP_TAC o MATCH_MP DIFF_ADD o (uncurry CONJ) o
531 (I ## MATCH_MP DIFF_NEG) o CONJ_PAIR) THEN
532 BETA_TAC THEN REWRITE_TAC[real_sub]
533QED
534
535(*---------------------------------------------------------------------------*)
536(* Now the chain rule *)
537(*---------------------------------------------------------------------------*)
538
539Theorem DIFF_CHAIN:
540 !f g l m x.
541 (f diffl l)(g x) /\ (g diffl m)(x) ==> ((\x. f(g x)) diffl (l * m))(x)
542Proof
543 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN MP_TAC) THEN
544 DISCH_THEN(fn th => MP_TAC th THEN ASSUME_TAC(MATCH_MP DIFF_CONT th)) THEN
545 REWRITE_TAC[DIFF_CARAT] THEN
546 DISCH_THEN(X_CHOOSE_THEN “g':real->real” STRIP_ASSUME_TAC) THEN
547 DISCH_THEN(X_CHOOSE_THEN “f':real->real” STRIP_ASSUME_TAC) THEN
548 EXISTS_TAC “\z. if (z = x) then l * m
549 else (f(g(z):real) - f(g(x))) / (z - x)” THEN
550 BETA_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
551 [GEN_TAC THEN COND_CASES_TAC THEN
552 ASM_REWRITE_TAC[REAL_SUB_REFL, REAL_MUL_RZERO] THEN
553 CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_RMUL THEN
554 ASM_REWRITE_TAC[REAL_SUB_0],
555 MP_TAC(CONJ (ASSUME “g contl x”) (ASSUME “f' contl (g(x:real))”)) THEN
556 DISCH_THEN(MP_TAC o MATCH_MP CONT_COMPOSE) THEN
557 DISCH_THEN(MP_TAC o C CONJ (ASSUME “g' contl x”)) THEN
558 DISCH_THEN(MP_TAC o MATCH_MP CONT_MUL) THEN BETA_TAC THEN
559 ASM_REWRITE_TAC[contl] THEN BETA_TAC THEN ASM_REWRITE_TAC[] THEN
560 MATCH_MP_TAC(TAUT_CONV “(a = b) ==> a ==> b”) THEN
561 MATCH_MP_TAC LIM_EQUAL THEN X_GEN_TAC “z:real” THEN
562 DISCH_TAC THEN BETA_TAC THEN ASM_REWRITE_TAC[REAL_ADD_RID_UNIQ] THEN
563 REWRITE_TAC[real_div, GSYM REAL_MUL_ASSOC, REAL_ADD_SUB] THEN
564 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_RINV th]) THEN
565 REWRITE_TAC[REAL_MUL_RID]]
566QED
567
568(*---------------------------------------------------------------------------*)
569(* Differentiation of natural number powers *)
570(*---------------------------------------------------------------------------*)
571
572Theorem DIFF_X:
573 !x. ((\x. x) diffl &1)(x)
574Proof
575 GEN_TAC THEN REWRITE_TAC[diffl] THEN BETA_TAC THEN
576 REWRITE_TAC[REAL_ADD_SUB] THEN REWRITE_TAC[LIM, REAL_SUB_RZERO] THEN
577 BETA_TAC THEN X_GEN_TAC “e:real” THEN DISCH_TAC THEN
578 EXISTS_TAC “&1” THEN REWRITE_TAC[REAL_LT_01] THEN
579 GEN_TAC THEN DISCH_THEN(MP_TAC o CONJUNCT1) THEN
580 REWRITE_TAC[GSYM ABS_NZ] THEN
581 DISCH_THEN(fn th => REWRITE_TAC[MATCH_MP REAL_DIV_REFL th]) THEN
582 ASM_REWRITE_TAC[REAL_SUB_REFL, ABS_0]
583QED
584
585Theorem DIFF_POW:
586 !n x. ((\x. x pow n) diffl (&n * (x pow (n - 1))))(x)
587Proof
588 INDUCT_TAC THEN REWRITE_TAC[pow, DIFF_CONST, REAL_MUL_LZERO] THEN
589 X_GEN_TAC “x:real” THEN
590 POP_ASSUM(MP_TAC o CONJ(SPEC “x:real” DIFF_X) o SPEC “x:real”) THEN
591 DISCH_THEN(MP_TAC o MATCH_MP DIFF_MUL) THEN BETA_TAC THEN
592 MATCH_MP_TAC(TAUT_CONV “(a = b) ==> a ==> b”) THEN
593 AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[REAL_MUL_LID] THEN
594 REWRITE_TAC[REAL, REAL_RDISTRIB, REAL_MUL_LID] THEN
595 GEN_REWR_TAC RAND_CONV [REAL_ADD_SYM] THEN BINOP_TAC THENL
596 [REWRITE_TAC[ADD1, ADD_SUB],
597 STRUCT_CASES_TAC (SPEC “n:num” num_CASES) THEN
598 REWRITE_TAC[REAL_MUL_LZERO] THEN
599 REWRITE_TAC[ADD1, ADD_SUB, POW_ADD] THEN
600 REWRITE_TAC[REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
601 REWRITE_TAC[ONE, pow] THEN
602 REWRITE_TAC[SYM ONE, REAL_MUL_RID]]
603QED
604
605val lemma = REWRITE_RULE [diffl_has_derivative, Once REAL_MUL_COMM] DIFF_POW;
606
607Theorem HAS_DERIVATIVE_POW' :
608 !n x. ((\x. x pow n) has_derivative (\y. &n * x pow (n - 1) * y)) (at x)
609Proof
610 REWRITE_TAC [lemma]
611QED
612
613(* !n x. ((\x. x pow n) has_vector_derivative &n * x pow (n - 1)) (at x) *)
614Theorem HAS_VECTOR_DERIVATIVE_POW =
615 REWRITE_RULE [diffl_has_vector_derivative] DIFF_POW
616
617(*---------------------------------------------------------------------------*)
618(* Now power of -1 (then differentiation of inverses follows from chain rule)*)
619(*---------------------------------------------------------------------------*)
620
621Theorem DIFF_XM1:
622 !x. x <> 0 ==> ((\x. inv(x)) diffl (-(inv(x) pow 2)))(x)
623Proof
624 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[diffl] THEN BETA_TAC THEN
625 MATCH_MP_TAC LIM_TRANSFORM THEN
626 EXISTS_TAC “\h. ~(inv(x + h) * inv(x))” THEN
627 BETA_TAC THEN CONJ_TAC THENL
628 [REWRITE_TAC[LIM] THEN X_GEN_TAC “e:real” THEN DISCH_TAC THEN
629 EXISTS_TAC “abs(x)” THEN
630 EVERY_ASSUM(fn th => REWRITE_TAC[REWRITE_RULE[ABS_NZ] th]) THEN
631 X_GEN_TAC “h:real” THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
632 DISCH_THEN STRIP_ASSUME_TAC THEN BETA_TAC THEN
633 W(C SUBGOAL_THEN SUBST1_TAC o C (curry mk_eq) “&0” o
634 rand o rator o snd) THEN ASM_REWRITE_TAC[] THEN
635 REWRITE_TAC[ABS_ZERO, REAL_SUB_0] THEN
636 SUBGOAL_THEN “~(x + h = &0)” ASSUME_TAC THENL
637 [REWRITE_TAC[REAL_LNEG_UNIQ] THEN DISCH_THEN SUBST_ALL_TAC THEN
638 UNDISCH_TAC “abs(h) < abs(~h)” THEN
639 REWRITE_TAC[ABS_NEG, REAL_LT_REFL], ALL_TAC] THEN
640 W(fn (asl,w) => MP_TAC(SPECL [“x * (x + h)”, lhs w, rhs w]
641 REAL_EQ_LMUL)) THEN
642 ASM_REWRITE_TAC[REAL_ENTIRE] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN
643 REWRITE_TAC[GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL] THEN
644 REWRITE_TAC[real_div, REAL_SUB_LDISTRIB, REAL_SUB_RDISTRIB] THEN
645 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
646 “(a * b) * (c * d) = (c * b) * (d * a)”] THEN
647 REWRITE_TAC(map (MATCH_MP REAL_MUL_LINV o ASSUME)
648 [“~(x = &0)”, “~(x + h = &0)”]) THEN REWRITE_TAC[REAL_MUL_LID] THEN
649 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM)
650 “(a * b) * (c * d) = (a * d) * (c * b)”] THEN
651 REWRITE_TAC[MATCH_MP REAL_MUL_LINV (ASSUME “~(x = &0)”)] THEN
652 REWRITE_TAC[REAL_MUL_LID, GSYM REAL_SUB_LDISTRIB] THEN
653 REWRITE_TAC[REWRITE_RULE[REAL_NEG_SUB]
654 (AP_TERM “$real_neg” (SPEC_ALL REAL_ADD_SUB))] THEN
655 REWRITE_TAC[GSYM REAL_NEG_RMUL] THEN AP_TERM_TAC THEN
656 MATCH_MP_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[ABS_NZ],
657
658 REWRITE_TAC[POW_2] THEN
659 CONV_TAC(EXACT_CONV[X_BETA_CONV “h:real” “inv(x + h) * inv(x)”]) THEN
660 REWRITE_TAC[GSYM LIM_NEG] THEN
661 CONV_TAC(EXACT_CONV(map (X_BETA_CONV “h:real”) [“inv(x + h)”, “inv(x)”]))
662 THEN MATCH_MP_TAC LIM_MUL THEN BETA_TAC THEN
663 REWRITE_TAC[LIM_CONST] THEN
664 CONV_TAC(EXACT_CONV[X_BETA_CONV “h:real” “x + h”]) THEN
665 MATCH_MP_TAC LIM_INV THEN ASM_REWRITE_TAC[] THEN
666 GEN_REWR_TAC LAND_CONV [GSYM REAL_ADD_RID] THEN
667 CONV_TAC(EXACT_CONV(map (X_BETA_CONV “h:real”) [“x:real”, “h:real”])) THEN
668 MATCH_MP_TAC LIM_ADD THEN BETA_TAC THEN REWRITE_TAC[LIM_CONST] THEN
669 MATCH_ACCEPT_TAC LIM_X]
670QED
671
672(*---------------------------------------------------------------------------*)
673(* Now differentiation of inverse and quotient *)
674(*---------------------------------------------------------------------------*)
675
676Theorem DIFF_INV:
677 !f l x. (f diffl l)(x) /\ ~(f(x) = &0) ==>
678 ((\x. inv(f x)) diffl ~(l / (f(x) pow 2)))(x)
679Proof
680 REPEAT GEN_TAC THEN REWRITE_TAC[real_div, REAL_NEG_RMUL] THEN
681 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN DISCH_TAC THEN
682 MATCH_MP_TAC DIFF_CHAIN THEN ASM_REWRITE_TAC[] THEN
683 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP POW_INV (CONJUNCT2 th)]) THEN
684 MATCH_MP_TAC(CONV_RULE(ONCE_DEPTH_CONV ETA_CONV) DIFF_XM1) THEN
685 ASM_REWRITE_TAC[]
686QED
687
688Theorem DIFF_DIV:
689 !f g l m x. (f diffl l)(x) /\ (g diffl m)(x) /\ ~(g(x) = &0) ==>
690 ((\x. f(x) / g(x)) diffl (((l * g(x)) - (m * f(x))) / (g(x) pow 2)))(x)
691Proof
692 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
693 REWRITE_TAC[real_div] THEN
694 MP_TAC(SPECL [“g:real->real”, “m:real”, “x:real”] DIFF_INV) THEN
695 ASM_REWRITE_TAC[] THEN
696 DISCH_THEN(MP_TAC o CONJ(ASSUME “(f diffl l)(x)”)) THEN
697 DISCH_THEN(MP_TAC o MATCH_MP DIFF_MUL) THEN BETA_TAC THEN
698 W(C SUBGOAL_THEN SUBST1_TAC o mk_eq o
699 ((rand o rator) ## (rand o rator)) o dest_imp o snd) THEN
700 REWRITE_TAC[] THEN REWRITE_TAC[real_sub] THEN
701 REWRITE_TAC[REAL_LDISTRIB, REAL_RDISTRIB] THEN BINOP_TAC THENL
702 [REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN AP_TERM_TAC THEN
703 REWRITE_TAC[POW_2] THEN
704 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_INV_MUL (W CONJ th)]) THEN
705 REWRITE_TAC[REAL_MUL_ASSOC] THEN
706 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_RINV th]) THEN
707 REWRITE_TAC[REAL_MUL_LID],
708 REWRITE_TAC[real_div, GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL] THEN
709 AP_TERM_TAC THEN CONV_TAC(AC_CONV(REAL_MUL_ASSOC,REAL_MUL_SYM))]
710QED
711
712(*---------------------------------------------------------------------------*)
713(* Differentiation of finite sum *)
714(*---------------------------------------------------------------------------*)
715
716Theorem DIFF_SUM:
717 !f f' m n x. (!r:num. m <= r /\ r < (m + n)
718 ==> ((\x. f r x) diffl (f' r x))(x))
719 ==> ((\x. sum(m,n)(\n. f n x)) diffl (sum(m,n) (\r. f' r x)))(x)
720Proof
721 REPEAT GEN_TAC THEN SPEC_TAC(“n:num”,“n:num”) THEN
722 INDUCT_TAC THEN REWRITE_TAC[sum, DIFF_CONST] THEN DISCH_TAC THEN
723 CONV_TAC(ONCE_DEPTH_CONV HABS_CONV) THEN MATCH_MP_TAC DIFF_ADD THEN
724 BETA_TAC THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THENL
725 [GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
726 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC LESS_TRANS THEN
727 EXISTS_TAC “m + n:num” THEN ASM_REWRITE_TAC[ADD_CLAUSES, LESS_SUC_REFL],
728 REWRITE_TAC[LESS_EQ_ADD, ADD_CLAUSES, LESS_SUC_REFL]]
729QED
730
731(*---------------------------------------------------------------------------*)
732(* By bisection, function continuous on closed interval is bounded above *)
733(*---------------------------------------------------------------------------*)
734
735Theorem CONT_BOUNDED:
736 !f a b. (a <= b /\ !x. a <= x /\ x <= b ==> $contl f x)
737 ==> ?M. !x. a <= x /\ x <= b ==> f(x) <= M
738Proof
739 REPEAT STRIP_TAC THEN
740 (MP_TAC o C SPEC BOLZANO_LEMMA)
741 “\(u,v). a <= u /\ u <= v /\ v <= b ==>
742 ?M. !x. u <= x /\ x <= v ==> f x <= M” THEN
743 CONV_TAC(ONCE_DEPTH_CONV PAIRED_BETA_CONV) THEN
744 W(C SUBGOAL_THEN (fn t => REWRITE_TAC[t]) o funpow 2(fst o dest_imp) o snd) THENL
745 [ALL_TAC,
746 DISCH_THEN(MP_TAC o SPECL [“a:real”, “b:real”]) THEN
747 ASM_REWRITE_TAC[REAL_LE_REFL]] THEN
748 CONJ_TAC THENL
749 [MAP_EVERY X_GEN_TAC [“u:real”, “v:real”, “w:real”] THEN
750 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
751 DISCH_TAC THEN
752 REPEAT(FIRST_ASSUM(UNDISCH_TAC o assert is_imp o concl)) THEN
753 ASM_REWRITE_TAC[] THEN
754 SUBGOAL_THEN “v <= b” ASSUME_TAC THENL
755 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “w:real” THEN
756 ASM_REWRITE_TAC[], ALL_TAC] THEN
757 SUBGOAL_THEN “a <= v” ASSUME_TAC THENL
758 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “u:real” THEN
759 ASM_REWRITE_TAC[], ALL_TAC] THEN
760 ASM_REWRITE_TAC[] THEN
761 DISCH_THEN(X_CHOOSE_TAC “M1:real”) THEN
762 DISCH_THEN(X_CHOOSE_TAC “M2:real”) THEN
763 DISJ_CASES_TAC(SPECL [“M1:real”, “M2:real”] REAL_LE_TOTAL) THENL
764 [EXISTS_TAC “M2:real” THEN X_GEN_TAC “x:real” THEN STRIP_TAC THEN
765 DISJ_CASES_TAC(SPECL [“x:real”, “v:real”] REAL_LE_TOTAL) THENL
766 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “M1:real” THEN
767 ASM_REWRITE_TAC[], ALL_TAC] THEN
768 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[],
769 EXISTS_TAC “M1:real” THEN X_GEN_TAC “x:real” THEN STRIP_TAC THEN
770 DISJ_CASES_TAC(SPECL [“x:real”, “v:real”] REAL_LE_TOTAL) THENL
771 [ALL_TAC, MATCH_MP_TAC REAL_LE_TRANS THEN
772 EXISTS_TAC “M2:real” THEN ASM_REWRITE_TAC[]] THEN
773 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]],
774 ALL_TAC] THEN
775 X_GEN_TAC “x:real” THEN ASM_CASES_TAC “a <= x /\ x <= b” THENL
776 [ALL_TAC,
777 EXISTS_TAC “&1” THEN REWRITE_TAC[REAL_LT_01] THEN
778 MAP_EVERY X_GEN_TAC [“u:real”, “v:real”] THEN
779 REPEAT STRIP_TAC THEN UNDISCH_TAC “~(a <= x /\ x <= b)” THEN
780 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
781 REWRITE_TAC[] THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THENL
782 [EXISTS_TAC “u:real”, EXISTS_TAC “v:real”] THEN
783 ASM_REWRITE_TAC[]] THEN
784 UNDISCH_TAC “!x. a <= x /\ x <= b ==> f contl x” THEN
785 DISCH_THEN(MP_TAC o SPEC “x:real”) THEN ASM_REWRITE_TAC[] THEN
786 REWRITE_TAC[contl, LIM] THEN
787 DISCH_THEN(MP_TAC o SPEC “&1”) THEN REWRITE_TAC[REAL_LT_01] THEN
788 ASM_REWRITE_TAC[REAL_SUB_RZERO] THEN BETA_TAC THEN
789 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
790 EXISTS_TAC “d:real” THEN ASM_REWRITE_TAC[] THEN
791 MAP_EVERY X_GEN_TAC [“u:real”, “v:real”] THEN REPEAT STRIP_TAC THEN
792 EXISTS_TAC “abs(f(x:real)) + &1” THEN
793 X_GEN_TAC “z:real” THEN STRIP_TAC THEN
794 FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
795 DISCH_THEN(MP_TAC o SPEC “z - x”) THEN
796 GEN_REWR_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_ADD_SYM] THEN
797 REWRITE_TAC[REAL_SUB_ADD] THEN DISCH_TAC THEN
798 MP_TAC(SPECL [“f(z:real) - f(x)”, “(f:real->real) x”] ABS_TRIANGLE) THEN
799 REWRITE_TAC[REAL_SUB_ADD] THEN
800 DISCH_THEN(ASSUME_TAC o ONCE_REWRITE_RULE[REAL_ADD_SYM]) THEN
801 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “abs(f(z:real))” THEN
802 REWRITE_TAC[ABS_LE] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
803 EXISTS_TAC “abs(f(x:real)) + (abs(f(z) - f(x)))” THEN
804 ASM_REWRITE_TAC[REAL_LE_LADD] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN
805 ASM_CASES_TAC “z:real = x” THENL
806 [ASM_REWRITE_TAC[REAL_SUB_REFL, ABS_0, REAL_LT_01],
807 FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[GSYM ABS_NZ] THEN
808 ASM_REWRITE_TAC[REAL_SUB_0, abs, REAL_SUB_LE] THEN
809 REWRITE_TAC[REAL_NEG_SUB] THEN COND_CASES_TAC THEN
810 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “v - u” THEN
811 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THENL
812 [EXISTS_TAC “v - x”, EXISTS_TAC “v - z”] THEN
813 ASM_REWRITE_TAC[real_sub, REAL_LE_RADD, REAL_LE_LADD, REAL_LE_NEG]]
814QED
815
816(*---------------------------------------------------------------------------*)
817(* Refine the above to existence of least upper bound *)
818(*---------------------------------------------------------------------------*)
819
820Theorem CONT_HASSUP:
821 !f a b. (a <= b /\ !x. a <= x /\ x <= b ==> $contl f x)
822 ==> ?M. (!x. a <= x /\ x <= b ==> f(x) <= M) /\
823 (!N. N < M ==> ?x. a <= x /\ x <= b /\ N < f(x))
824Proof
825 let val tm = “\y:real. ?x. a <= x /\ x <= b /\ (y = f(x))” in
826 REPEAT GEN_TAC THEN DISCH_TAC THEN MP_TAC(SPEC tm REAL_SUP_LE) THEN
827 BETA_TAC THEN
828 W(C SUBGOAL_THEN (fn t => REWRITE_TAC[t]) o funpow 2 (fst o dest_imp) o snd)
829 THENL
830 [CONJ_TAC THENL
831 [MAP_EVERY EXISTS_TAC [“(f:real->real) a”, “a:real”] THEN
832 ASM_REWRITE_TAC[REAL_LE_REFL, REAL_LE_LT],
833 POP_ASSUM(X_CHOOSE_TAC “M:real” o MATCH_MP CONT_BOUNDED) THEN
834 EXISTS_TAC “M:real” THEN X_GEN_TAC “y:real” THEN
835 DISCH_THEN(X_CHOOSE_THEN “x:real” MP_TAC) THEN
836 REWRITE_TAC[CONJ_ASSOC] THEN
837 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC SUBST1_TAC) THEN
838 POP_ASSUM MATCH_ACCEPT_TAC],
839 DISCH_TAC THEN EXISTS_TAC “sup ^tm” THEN CONJ_TAC THENL
840 [X_GEN_TAC “x:real” THEN DISCH_TAC THEN
841 FIRST_ASSUM(MP_TAC o SPEC “sup ^tm”) THEN
842 REWRITE_TAC[REAL_LT_REFL] THEN
843 CONV_TAC(ONCE_DEPTH_CONV NOT_EXISTS_CONV) THEN
844 DISCH_THEN(MP_TAC o SPEC “(f:real->real) x”) THEN
845 REWRITE_TAC[DE_MORGAN_THM, REAL_NOT_LT] THEN
846 CONV_TAC(ONCE_DEPTH_CONV NOT_EXISTS_CONV) THEN
847 DISCH_THEN(DISJ_CASES_THEN MP_TAC) THEN REWRITE_TAC[] THEN
848 DISCH_THEN(MP_TAC o SPEC “x:real”) THEN ASM_REWRITE_TAC[],
849 GEN_TAC THEN FIRST_ASSUM(SUBST1_TAC o SYM o SPEC “N:real”) THEN
850 DISCH_THEN(X_CHOOSE_THEN “y:real” MP_TAC) THEN
851 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
852 DISCH_THEN(X_CHOOSE_THEN “x:real” MP_TAC) THEN
853 REWRITE_TAC[CONJ_ASSOC] THEN
854 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC SUBST_ALL_TAC) THEN
855 DISCH_TAC THEN EXISTS_TAC “x:real” THEN ASM_REWRITE_TAC[]]] end
856QED
857
858(*---------------------------------------------------------------------------*)
859(* Now show that it attains its upper bound *)
860(*---------------------------------------------------------------------------*)
861
862Theorem CONT_ATTAINS:
863 !f a b. (a <= b /\ !x. a <= x /\ x <= b ==> $contl f x)
864 ==> ?M. (!x. a <= x /\ x <= b ==> f(x) <= M) /\
865 (?x. a <= x /\ x <= b /\ (f(x) = M))
866Proof
867 REPEAT GEN_TAC THEN DISCH_TAC THEN
868 FIRST_ASSUM(X_CHOOSE_THEN “M:real” STRIP_ASSUME_TAC o MATCH_MP CONT_HASSUP)
869 THEN EXISTS_TAC “M:real” THEN ASM_REWRITE_TAC[] THEN
870 GEN_REWR_TAC I [TAUT_CONV “a:bool = ~~a”] THEN
871 CONV_TAC(RAND_CONV NOT_EXISTS_CONV) THEN
872 REWRITE_TAC[TAUT_CONV “~(a /\ b /\ c) = a /\ b ==> ~c”] THEN
873 DISCH_TAC THEN
874 SUBGOAL_THEN “!x. a <= x /\ x <= b ==> f(x) < M” MP_TAC THENL
875 [GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN
876 CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
877 FIRST_ASSUM ACCEPT_TAC, ALL_TAC] THEN
878 PURE_ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN DISCH_TAC THEN
879 SUBGOAL_THEN “!x. a <= x /\ x <= b ==> $contl (\x. inv(M - f(x))) x”
880 ASSUME_TAC THENL
881 [GEN_TAC THEN DISCH_TAC THEN
882 CONV_TAC(ONCE_DEPTH_CONV HABS_CONV) THEN
883 MATCH_MP_TAC CONT_INV THEN BETA_TAC THEN
884 REWRITE_TAC[REAL_SUB_0] THEN CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
885 CONJ_TAC THENL
886 [ALL_TAC,
887 MATCH_MP_TAC REAL_LT_IMP_NE THEN
888 ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN
889 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]] THEN
890 CONV_TAC(ONCE_DEPTH_CONV HABS_CONV) THEN
891 MATCH_MP_TAC CONT_SUB THEN BETA_TAC THEN
892 REWRITE_TAC[CONT_CONST] THEN
893 CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN
894 FIRST_ASSUM(MATCH_MP_TAC o CONJUNCT2) THEN
895 ASM_REWRITE_TAC[], ALL_TAC] THEN
896 SUBGOAL_THEN “?k. !x. a <= x /\ x <= b ==> (\x. inv(M - (f x))) x <= k”
897 MP_TAC THENL
898 [MATCH_MP_TAC CONT_BOUNDED THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
899 BETA_TAC THEN DISCH_THEN(X_CHOOSE_TAC “k:real”) THEN
900 SUBGOAL_THEN “!x. a <= x /\ x <= b ==> &0 < inv(M - f(x))” ASSUME_TAC THENL
901 [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_INV_POS THEN
902 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
903 SUBGOAL_THEN “!x. a <= x /\ x <= b ==> (\x. inv(M - (f x))) x < (k + &1)”
904 ASSUME_TAC THENL
905 [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
906 EXISTS_TAC “k:real” THEN REWRITE_TAC[REAL_LT_ADDR, REAL_LT_01] THEN
907 BETA_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
908 ASM_REWRITE_TAC[], ALL_TAC] THEN
909 SUBGOAL_THEN “!x. a <= x /\ x <= b ==>
910 inv(k + &1) < inv((\x. inv(M - (f x))) x)” MP_TAC THENL
911 [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LT_INV THEN
912 CONJ_TAC THENL
913 [BETA_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[],
914 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]], ALL_TAC] THEN
915 BETA_TAC THEN DISCH_TAC THEN
916 SUBGOAL_THEN “!x. a <= x /\ x <= b ==> inv(k + &1) < (M - (f x))”
917 MP_TAC THENL
918 [GEN_TAC THEN DISCH_TAC THEN
919 SUBGOAL_THEN “~(M - f(x:real) = &0)”
920 (SUBST1_TAC o SYM o MATCH_MP REAL_INVINV) THENL
921 [CONV_TAC(RAND_CONV SYM_CONV) THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN
922 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[],
923 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]], ALL_TAC] THEN
924 REWRITE_TAC[REAL_LT_SUB_LADD] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
925 ONCE_REWRITE_TAC[GSYM REAL_LT_SUB_LADD] THEN DISCH_TAC THEN
926 UNDISCH_TAC “!N. N < M ==> (?x. a <= x /\ x <= b /\ N < (f x))” THEN
927 DISCH_THEN(MP_TAC o SPEC “M - inv(k + &1)”) THEN
928 REWRITE_TAC[REAL_LT_SUB_RADD, REAL_LT_ADDR] THEN
929 REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
930 [MATCH_MP_TAC REAL_INV_POS THEN MATCH_MP_TAC REAL_LT_TRANS THEN
931 EXISTS_TAC “k:real” THEN REWRITE_TAC[REAL_LT_ADDR, REAL_LT_01] THEN
932 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC “inv(M - f(a:real))” THEN
933 CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
934 ASM_REWRITE_TAC[REAL_LE_REFL],
935 DISCH_THEN(X_CHOOSE_THEN “x:real” MP_TAC) THEN REWRITE_TAC[CONJ_ASSOC] THEN
936 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
937 REWRITE_TAC[REAL_NOT_LT] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN
938 ONCE_REWRITE_TAC[GSYM REAL_LT_SUB_LADD] THEN
939 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]
940QED
941
942(*---------------------------------------------------------------------------*)
943(* Same theorem for lower bound *)
944(*---------------------------------------------------------------------------*)
945
946Theorem CONT_ATTAINS2:
947 !f a b. (a <= b /\ !x. a <= x /\ x <= b ==> $contl f x)
948 ==> ?M. (!x. a <= x /\ x <= b ==> M <= f(x)) /\
949 (?x. a <= x /\ x <= b /\ (f(x) = M))
950Proof
951 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN
952 SUBGOAL_THEN “!x. a <= x /\ x <= b ==> (\x. ~(f x)) contl x” MP_TAC THENL
953 [GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC CONT_NEG THEN
954 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
955 DISCH_THEN(MP_TAC o CONJ (ASSUME “a <= b”)) THEN
956 DISCH_THEN(X_CHOOSE_THEN “M:real” MP_TAC o MATCH_MP CONT_ATTAINS) THEN
957 BETA_TAC THEN DISCH_TAC THEN Q.EXISTS_TAC ‘~M’ THEN CONJ_TAC THENL
958 [GEN_TAC THEN GEN_REWR_TAC RAND_CONV [GSYM REAL_LE_NEG] THEN
959 ASM_REWRITE_TAC[REAL_NEGNEG],
960 ASM_REWRITE_TAC[GSYM REAL_NEG_EQ]]
961QED
962
963(*---------------------------------------------------------------------------*)
964(* Show it attains *all* values in its range *)
965(*---------------------------------------------------------------------------*)
966
967Theorem CONT_ATTAINS_ALL:
968 !f a b. a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==>
969 ?L M. L <= M /\
970 (!y. L <= y /\ y <= M ==> ?x. a <= x /\ x <= b /\ (f(x) = y)) /\
971 (!x. a <= x /\ x <= b ==> L <= f(x) /\ f(x) <= M)
972Proof
973 REPEAT GEN_TAC THEN DISCH_TAC THEN
974 FIRST_ASSUM(X_CHOOSE_THEN “M:real” MP_TAC o MATCH_MP CONT_ATTAINS) THEN
975 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_TAC “xm:real”)) THEN
976 FIRST_ASSUM(X_CHOOSE_THEN “L:real” MP_TAC o MATCH_MP CONT_ATTAINS2) THEN
977 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_TAC “xl:real”)) THEN
978 MAP_EVERY EXISTS_TAC [“L:real”, “M:real”] THEN REPEAT CONJ_TAC THENL
979 [REPEAT(FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
980 DISCH_THEN(MP_TAC o SPEC “a:real”)) THEN ASM_REWRITE_TAC[REAL_LE_REFL] THEN
981 REPEAT DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
982 EXISTS_TAC “(f:real->real)(a)” THEN ASM_REWRITE_TAC[],
983 X_GEN_TAC “y:real” THEN STRIP_TAC THEN
984 DISJ_CASES_TAC(SPECL [“xl:real”, “xm:real”] REAL_LE_TOTAL) THENL
985 [MP_TAC(SPECL [“f:real->real”, “xl:real”, “xm:real”, “y:real”] IVT),
986 MP_TAC(SPECL [“f:real->real”, “xm:real”, “xl:real”, “y:real”] IVT2)] THEN
987 ASM_REWRITE_TAC[] THEN
988 (W(C SUBGOAL_THEN ASSUME_TAC o funpow 2 (fst o dest_imp) o snd) THENL
989 [X_GEN_TAC “x:real” THEN STRIP_TAC THEN
990 FIRST_ASSUM(MATCH_MP_TAC o CONJUNCT2),
991 ASM_REWRITE_TAC[] THEN
992 DISCH_THEN(X_CHOOSE_THEN “x:real” STRIP_ASSUME_TAC) THEN
993 EXISTS_TAC “x:real” THEN ASM_REWRITE_TAC[]] THEN
994 (CONJ_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
995 FIRST [EXISTS_TAC “xl:real” THEN ASM_REWRITE_TAC[] THEN NO_TAC,
996 EXISTS_TAC “xm:real” THEN ASM_REWRITE_TAC[] THEN NO_TAC])),
997 GEN_TAC THEN DISCH_TAC THEN CONJ_TAC THEN
998 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]
999QED
1000
1001(*---------------------------------------------------------------------------*)
1002(* If f'(x) real_gt 0 then x is locally strictly increasing at the right *)
1003(*---------------------------------------------------------------------------*)
1004
1005Theorem DIFF_LINC:
1006 !f x l. (f diffl l)(x) /\ &0 < l ==>
1007 ?d. &0 < d /\ !h. &0 < h /\ h < d ==> f(x) < f(x + h)
1008Proof
1009 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1010 REWRITE_TAC[diffl, LIM, REAL_SUB_RZERO] THEN
1011 DISCH_THEN(MP_TAC o SPEC “l:real”) THEN ASM_REWRITE_TAC[] THEN BETA_TAC THEN
1012 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
1013 EXISTS_TAC “d:real” THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN
1014 DISCH_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN
1015 FIRST_ASSUM(MP_TAC o MATCH_MP REAL_INV_POS o CONJUNCT1) THEN
1016 DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM(MATCH_MP REAL_LT_RMUL th)]) THEN
1017 REWRITE_TAC[REAL_MUL_LZERO] THEN REWRITE_TAC[GSYM real_div] THEN
1018 MATCH_MP_TAC ABS_SIGN THEN EXISTS_TAC “l:real” THEN
1019 FIRST_ASSUM MATCH_MP_TAC THEN
1020 FIRST_ASSUM(ASSUME_TAC o MATCH_MP REAL_LT_IMP_LE o CONJUNCT1) THEN
1021 ASM_REWRITE_TAC[abs]
1022QED
1023
1024(*---------------------------------------------------------------------------*)
1025(* If f'(x) < 0 then x is locally strictly increasing at the left *)
1026(*---------------------------------------------------------------------------*)
1027
1028Theorem DIFF_LDEC:
1029 !f x l. (f diffl l)(x) /\ l < &0 ==>
1030 ?d. &0 < d /\ !h. &0 < h /\ h < d ==> f(x) < f(x - h)
1031Proof
1032 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN
1033 REWRITE_TAC[diffl, LIM, REAL_SUB_RZERO] THEN
1034 DISCH_THEN(Q.SPEC_THEN ‘~l’ MP_TAC) THEN
1035 ONCE_REWRITE_TAC[GSYM REAL_NEG_LT0] THEN ASM_REWRITE_TAC[REAL_NEGNEG] THEN
1036 REWRITE_TAC[REAL_NEG_LT0] THEN BETA_TAC THEN
1037 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
1038 EXISTS_TAC “d:real” THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN
1039 DISCH_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN
1040 FIRST_ASSUM(MP_TAC o MATCH_MP REAL_INV_POS o CONJUNCT1) THEN
1041 DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM(MATCH_MP REAL_LT_RMUL th)]) THEN
1042 REWRITE_TAC[REAL_MUL_LZERO] THEN
1043 REWRITE_TAC[GSYM REAL_NEG_LT0, REAL_NEG_RMUL] THEN
1044 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_NEG_INV
1045 (GSYM (MATCH_MP REAL_LT_IMP_NE (CONJUNCT1 th)))]) THEN
1046 MATCH_MP_TAC ABS_SIGN2 THEN EXISTS_TAC “l:real” THEN
1047 REWRITE_TAC[GSYM real_div] THEN
1048 GEN_REWR_TAC (LAND_CONV o RAND_CONV o funpow 3 LAND_CONV o RAND_CONV)
1049 [real_sub] THEN
1050 FIRST_ASSUM MATCH_MP_TAC THEN
1051 FIRST_ASSUM(ASSUME_TAC o MATCH_MP REAL_LT_IMP_LE o CONJUNCT1) THEN
1052 REWRITE_TAC[abs, GSYM REAL_NEG_LE0, REAL_NEGNEG] THEN
1053 ASM_REWRITE_TAC[GSYM REAL_NOT_LT]
1054QED
1055
1056(*---------------------------------------------------------------------------*)
1057(* If f is differentiable at a local maximum x, f'(x) = 0 *)
1058(*---------------------------------------------------------------------------*)
1059
1060Theorem DIFF_LMAX:
1061 !f x l. ($diffl f l)(x) /\
1062 (?d. &0 < d /\ (!y. abs(x - y) < d ==> f(y) <= f(x))) ==> (l = &0)
1063Proof
1064 REPEAT GEN_TAC THEN DISCH_THEN
1065 (CONJUNCTS_THEN2 MP_TAC (X_CHOOSE_THEN “k:real” STRIP_ASSUME_TAC)) THEN
1066 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
1067 (SPECL [“l:real”, “&0”] REAL_LT_TOTAL) THEN
1068 ASM_REWRITE_TAC[] THENL
1069 [DISCH_THEN(MP_TAC o C CONJ(ASSUME “l < &0”)) THEN
1070 DISCH_THEN(MP_TAC o MATCH_MP DIFF_LDEC) THEN
1071 DISCH_THEN(X_CHOOSE_THEN “e:real” MP_TAC) THEN
1072 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1073 MP_TAC(SPECL [“k:real”, “e:real”] REAL_DOWN2) THEN
1074 ASM_REWRITE_TAC[] THEN
1075 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
1076 DISCH_THEN(MP_TAC o SPEC “d:real”) THEN ASM_REWRITE_TAC[] THEN
1077 DISCH_TAC THEN FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
1078 DISCH_THEN(MP_TAC o SPEC “x - d”) THEN REWRITE_TAC[REAL_SUB_SUB2] THEN
1079 SUBGOAL_THEN “&0 <= d” ASSUME_TAC THENL
1080 [MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
1081 ASM_REWRITE_TAC[abs] THEN ASM_REWRITE_TAC[GSYM REAL_NOT_LT],
1082 DISCH_THEN(MP_TAC o C CONJ(ASSUME “&0 < l”)) THEN
1083 DISCH_THEN(MP_TAC o MATCH_MP DIFF_LINC) THEN
1084 DISCH_THEN(X_CHOOSE_THEN “e:real” MP_TAC) THEN
1085 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1086 MP_TAC(SPECL [“k:real”, “e:real”] REAL_DOWN2) THEN
1087 ASM_REWRITE_TAC[] THEN
1088 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
1089 DISCH_THEN(MP_TAC o SPEC “d:real”) THEN ASM_REWRITE_TAC[] THEN
1090 DISCH_TAC THEN FIRST_ASSUM(UNDISCH_TAC o assert is_forall o concl) THEN
1091 DISCH_THEN(MP_TAC o SPEC “x + d”) THEN REWRITE_TAC[REAL_ADD_SUB2] THEN
1092 SUBGOAL_THEN “&0 <= d” ASSUME_TAC THENL
1093 [MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
1094 REWRITE_TAC[ABS_NEG] THEN
1095 ASM_REWRITE_TAC[abs] THEN ASM_REWRITE_TAC[GSYM REAL_NOT_LT]]
1096QED
1097
1098(*---------------------------------------------------------------------------*)
1099(* Similar theorem for a local minimum *)
1100(*---------------------------------------------------------------------------*)
1101
1102Theorem DIFF_LMIN:
1103 !f x l. ($diffl f l)(x) /\
1104 (?d. &0 < d /\ (!y. abs(x - y) < d ==> f(x) <= f(y))) ==> (l = &0)
1105Proof
1106 REPEAT GEN_TAC THEN DISCH_TAC THEN
1107 MP_TAC(Q.SPECL [‘\x:real. ~(f x)’, ‘x:real’, ‘~l’] DIFF_LMAX) THEN
1108 BETA_TAC THEN REWRITE_TAC[REAL_LE_NEG, REAL_NEG_EQ0] THEN
1109 DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1110 MATCH_MP_TAC DIFF_NEG THEN ASM_REWRITE_TAC[]
1111QED
1112
1113(*---------------------------------------------------------------------------*)
1114(* In particular if a function is locally flat *)
1115(*---------------------------------------------------------------------------*)
1116
1117Theorem DIFF_LCONST:
1118 !f x l. ($diffl f l)(x) /\
1119 (?d. &0 < d /\ (!y. abs(x - y) < d ==> (f(y) = f(x)))) ==> (l = &0)
1120Proof
1121 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1122 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
1123 MATCH_MP_TAC DIFF_LMAX THEN
1124 MAP_EVERY EXISTS_TAC [“f:real->real”, “x:real”] THEN ASM_REWRITE_TAC[] THEN
1125 EXISTS_TAC “d:real” THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN
1126 DISCH_THEN(fn th => FIRST_ASSUM(SUBST1_TAC o C MATCH_MP th)) THEN
1127 MATCH_ACCEPT_TAC REAL_LE_REFL
1128QED
1129
1130(*---------------------------------------------------------------------------*)
1131(* Lemma about introducing open ball in open interval *)
1132(*---------------------------------------------------------------------------*)
1133
1134Theorem INTERVAL_LEMMA_LT :
1135 !a b x. a < x /\ x < b ==>
1136 ?d. &0 < d /\ !y. abs(x - y) < d ==> a < y /\ y < b
1137Proof
1138 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM ABS_BETWEEN] THEN
1139 DISJ_CASES_TAC(Q.SPECL [`x - a`, `b - x`] REAL_LE_TOTAL) THENL
1140 [ Q.EXISTS_TAC `x - a`, Q.EXISTS_TAC `b - x` ] THEN
1141 ASM_REWRITE_TAC[REAL_SUB_LT] THEN GEN_TAC THEN
1142 REWRITE_TAC[REAL_LT_SUB_LADD, REAL_LT_SUB_RADD] THEN
1143 REWRITE_TAC[real_sub, REAL_ADD_ASSOC] THEN
1144 REWRITE_TAC[GSYM real_sub, REAL_LT_SUB_LADD, REAL_LT_SUB_RADD] THEN
1145 FREEZE_THEN(fn th => ONCE_REWRITE_TAC[th]) (Q.SPEC `x` REAL_ADD_SYM) THEN
1146 REWRITE_TAC[REAL_LT_RADD] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1147 (MATCH_MP_TAC o hol88Lib.GEN_ALL o fst o EQ_IMP_RULE o SPEC_ALL) REAL_LT_RADD THENL
1148 [ (* goal 1 (of 2) *)
1149 Q.EXISTS_TAC `a:real` THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
1150 Q.EXISTS_TAC `x + x` THEN ASM_REWRITE_TAC[] THEN
1151 Q.UNDISCH_TAC `(x - a) <= (b - x)`,
1152 (* goal 2 (of 2) *)
1153 Q.EXISTS_TAC `b:real` THEN MATCH_MP_TAC REAL_LET_TRANS THEN
1154 Q.EXISTS_TAC `x + x` THEN ASM_REWRITE_TAC[] THEN
1155 Q.UNDISCH_TAC `(b - x) <= (x - a)`] THEN
1156 REWRITE_TAC[REAL_LE_SUB_LADD, GSYM REAL_LE_SUB_RADD] THEN
1157 MATCH_MP_TAC(TAUT_CONV ``(a = b) ==> a ==> b``) THEN
1158 AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[real_sub] THEN
1159 REAL_ARITH_TAC
1160QED
1161
1162Theorem INTERVAL_LEMMA :
1163 !a b x. a < x /\ x < b ==>
1164 ?d. &0 < d /\ !y. abs(x - y) < d ==> a <= y /\ y <= b
1165Proof
1166 REPEAT GEN_TAC THEN
1167 DISCH_THEN(Q.X_CHOOSE_TAC `d` o MATCH_MP INTERVAL_LEMMA_LT) THEN
1168 Q.EXISTS_TAC `d` THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN
1169 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th o CONJUNCT2)) THEN
1170 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]
1171QED
1172
1173(*---------------------------------------------------------------------------*)
1174(* Now Rolle's theorem *)
1175(*---------------------------------------------------------------------------*)
1176
1177(* cf. derivativeTheory.ROLLE *)
1178Theorem ROLLE :
1179 !f a b. a < b /\
1180 (f(a) = f(b)) /\
1181 (!x. a <= x /\ x <= b ==> f contl x) /\
1182 (!x. a < x /\ x < b ==> f differentiable x)
1183 ==> ?z. a < z /\ z < b /\ (f diffl &0)(z)
1184Proof
1185 rw [differentiable, diffl_has_derivative', contl_eq_continuous_at]
1186 >> fs [GSYM IN_INTERVAL, EXT_SKOLEM_THM]
1187 >> MP_TAC (Q.SPECL [‘f’, ‘$* o f'’, ‘a’, ‘b’] derivativeTheory.ROLLE)
1188 >> Know ‘f continuous_on interval [a,b]’
1189 >- (MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON >> rw [])
1190 >> rw [o_DEF, FUN_EQ_THM]
1191 >> Q.PAT_X_ASSUM ‘!x. x IN interval (a,b) ==> P’ (MP_TAC o (Q.SPEC ‘x’))
1192 >> RW_TAC std_ss []
1193 >> Q.EXISTS_TAC ‘x’
1194 >> fs [IN_INTERVAL] >> METIS_TAC []
1195QED
1196
1197(*---------------------------------------------------------------------------*)
1198(* Mean value theorem *)
1199(*---------------------------------------------------------------------------*)
1200
1201val gfn = “\x. f(x) - (((f(b) - f(a)) / (b - a)) * x)”;
1202
1203Theorem MVT_LEMMA:
1204 !(f:real->real) a b. ^gfn(a) = ^gfn(b)
1205Proof
1206 REPEAT GEN_TAC THEN BETA_TAC THEN
1207 ASM_CASES_TAC “b:real = a” THEN ASM_REWRITE_TAC[] THEN
1208 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1209 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[GSYM REAL_SUB_0]) THEN
1210 MP_TAC(GENL [“x:real”, “y:real”]
1211 (SPECL [“x:real”, “y:real”, “b - a”] REAL_EQ_RMUL)) THEN
1212 ASM_REWRITE_TAC[] THEN
1213 DISCH_THEN(fn th => GEN_REWR_TAC I [GSYM th]) THEN
1214 REWRITE_TAC[REAL_SUB_RDISTRIB, GSYM REAL_MUL_ASSOC] THEN
1215 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_DIV_RMUL th]) THEN
1216 GEN_REWR_TAC (RAND_CONV o RAND_CONV) [REAL_MUL_SYM] THEN
1217 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [REAL_MUL_SYM] THEN
1218 REWRITE_TAC[real_sub, REAL_LDISTRIB, REAL_RDISTRIB] THEN
1219 REWRITE_TAC[GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL,
1220 REAL_NEG_ADD, REAL_NEGNEG] THEN
1221 REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
1222 REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM)
1223 “w + (x + (y + z)) = (y + w) + (x + z)”,
1224 REAL_ADD_LINV, REAL_ADD_LID] THEN
1225 REWRITE_TAC[REAL_ADD_RID]
1226QED
1227
1228(* cf. derivativeTheory.MVT (One-dimensional mean value theorem) *)
1229Theorem MVT :
1230 !f a b. a < b /\
1231 (!x. a <= x /\ x <= b ==> f contl x) /\
1232 (!x. a < x /\ x < b ==> f differentiable x)
1233 ==> ?l z. a < z /\ z < b /\ (f diffl l)(z) /\
1234 (f(b) - f(a) = (b - a) * l)
1235Proof
1236 rw [differentiable, diffl_has_derivative', contl_eq_continuous_at]
1237 >> fs [GSYM IN_INTERVAL, EXT_SKOLEM_THM]
1238 >> MP_TAC (Q.SPECL [‘f’, ‘$* o f'’, ‘a’, ‘b’] derivativeTheory.MVT)
1239 >> Know ‘f continuous_on interval [a,b]’
1240 >- (MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON >> rw [])
1241 >> rw [o_DEF, FUN_EQ_THM]
1242 >> fs [IN_INTERVAL]
1243 >> qexistsl_tac [‘f' x’, ‘x’] >> rw []
1244QED
1245
1246(*---------------------------------------------------------------------------*)
1247(* Theorem that function is constant if its derivative is 0 over an interval.*)
1248(* *)
1249(* We could have proved this directly by bisection; consider instantiating *)
1250(* BOLZANO_LEMMA with *)
1251(* *)
1252(* fn (x,y) => f(y) - f(x) <= C * (y - x) *)
1253(* *)
1254(* However the Rolle and Mean Value theorems are useful to have anyway *)
1255(*---------------------------------------------------------------------------*)
1256
1257Theorem DIFF_ISCONST_END:
1258 !f a b. a < b /\
1259 (!x. a <= x /\ x <= b ==> f contl x) /\
1260 (!x. a < x /\ x < b ==> (f diffl &0)(x))
1261 ==> (f b = f a)
1262Proof
1263 REPEAT GEN_TAC THEN STRIP_TAC THEN
1264 MP_TAC(SPECL [“f:real->real”, “a:real”, “b:real”] MVT) THEN
1265 ASM_REWRITE_TAC[] THEN
1266 W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
1267 [GEN_TAC THEN REWRITE_TAC[differentiable] THEN
1268 DISCH_THEN(curry op THEN (EXISTS_TAC “&0”) o MP_TAC) THEN
1269 ASM_REWRITE_TAC[],
1270 DISCH_THEN(fn th => REWRITE_TAC[th])] THEN
1271 DISCH_THEN(X_CHOOSE_THEN “l:real” (X_CHOOSE_THEN “x:real” MP_TAC)) THEN
1272 ONCE_REWRITE_TAC[TAUT_CONV “a /\ b /\ c /\ d = (a /\ b) /\ (c /\ d)”] THEN
1273 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
1274 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
1275 DISCH_THEN(MP_TAC o CONJ (ASSUME “(f diffl l)(x)”)) THEN
1276 DISCH_THEN(SUBST_ALL_TAC o MATCH_MP DIFF_UNIQ) THEN
1277 RULE_ASSUM_TAC(REWRITE_RULE[REAL_MUL_RZERO, REAL_SUB_0]) THEN
1278 FIRST_ASSUM ACCEPT_TAC
1279QED
1280
1281Theorem DIFF_ISCONST:
1282 !f a b. a < b /\
1283 (!x. a <= x /\ x <= b ==> f contl x) /\
1284 (!x. a < x /\ x < b ==> (f diffl &0)(x))
1285 ==> !x. a <= x /\ x <= b ==> (f x = f a)
1286Proof
1287 REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN STRIP_TAC THEN
1288 MP_TAC(SPECL [“f:real->real”, “a:real”, “x:real”] DIFF_ISCONST_END) THEN
1289 DISJ_CASES_THEN MP_TAC (REWRITE_RULE[REAL_LE_LT] (ASSUME “a <= x”)) THENL
1290 [DISCH_TAC THEN ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
1291 CONJ_TAC THEN X_GEN_TAC “z:real” THEN STRIP_TAC THEN
1292 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THENL
1293 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “x:real”,
1294 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC “x:real”] THEN
1295 ASM_REWRITE_TAC[],
1296 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[]]
1297QED
1298
1299Theorem DIFF_ISCONST_ALL:
1300 !f. (!x. (f diffl &0)(x)) ==> (!x y. f(x) = f(y))
1301Proof
1302 GEN_TAC THEN DISCH_TAC THEN
1303 SUBGOAL_THEN “!x. f contl x” ASSUME_TAC THENL
1304 [GEN_TAC THEN MATCH_MP_TAC DIFF_CONT THEN
1305 EXISTS_TAC “&0” THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
1306 REPEAT GEN_TAC THEN REPEAT_TCL DISJ_CASES_THEN MP_TAC
1307 (SPECL [“x:real”, “y:real”] REAL_LT_TOTAL) THENL
1308 [DISCH_THEN SUBST1_TAC THEN REFL_TAC,
1309 CONV_TAC(RAND_CONV SYM_CONV),
1310 ALL_TAC] THEN
1311 DISCH_TAC THEN MATCH_MP_TAC DIFF_ISCONST_END THEN
1312 ASM_REWRITE_TAC[]
1313QED
1314
1315(*---------------------------------------------------------------------------*)
1316(* Boring lemma about distances *)
1317(*---------------------------------------------------------------------------*)
1318
1319Theorem INTERVAL_ABS:
1320 !x z d. (x - d) <= z /\ z <= (x + d) = abs(z - x) <= d
1321Proof
1322 REPEAT GEN_TAC THEN REWRITE_TAC[abs, REAL_LE_SUB_RADD] THEN EQ_TAC THENL
1323 [STRIP_TAC THEN COND_CASES_TAC THEN
1324 REWRITE_TAC[REAL_LE_SUB_RADD, REAL_NEG_SUB] THEN
1325 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN ASM_REWRITE_TAC[],
1326 REWRITE_TAC[REAL_SUB_LE] THEN COND_CASES_TAC THEN
1327 REWRITE_TAC[REAL_NEG_SUB, REAL_LE_SUB_RADD] THENL
1328 [ALL_TAC,
1329 RULE_ASSUM_TAC(MATCH_MP REAL_LT_IMP_LE o REWRITE_RULE[REAL_NOT_LE])] THEN
1330 DISCH_THEN(ASSUME_TAC o ONCE_REWRITE_RULE[REAL_ADD_SYM]) THEN
1331 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THENL
1332 [EXISTS_TAC “x + d”, EXISTS_TAC “z + d”] THEN
1333 ASM_REWRITE_TAC[REAL_LE_RADD] THEN
1334 MATCH_MP_TAC REAL_LE_TRANS THENL
1335 [EXISTS_TAC “z:real”, EXISTS_TAC “x:real”] THEN
1336 ASM_REWRITE_TAC[]]
1337QED
1338
1339(*---------------------------------------------------------------------------*)
1340(* Continuous injection on an interval can't have a maximum in the middle *)
1341(*---------------------------------------------------------------------------*)
1342
1343Theorem CONT_INJ_LEMMA:
1344 !f g x d. &0 < d /\
1345 (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
1346 (!z. abs(z - x) <= d ==> f contl z) ==>
1347 ~(!z. abs(z - x) <= d ==> f(z) <= f(x))
1348Proof
1349 REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_TAC REAL_LT_IMP_LE THEN
1350 DISCH_THEN(fn th => MAP_EVERY (MP_TAC o C SPEC th) [“x - d”, “x + d”]) THEN
1351 REWRITE_TAC[REAL_ADD_SUB, REAL_SUB_SUB, ABS_NEG] THEN
1352 ASM_REWRITE_TAC[abs, REAL_LE_REFL] THEN
1353 DISCH_TAC THEN DISCH_TAC THEN DISJ_CASES_TAC
1354 (SPECL [“f(x - d):real”, “f(x + d):real”] REAL_LE_TOTAL) THENL
1355 [MP_TAC(SPECL [“f:real->real”, “x - d”, “x:real”, “f(x + d):real”] IVT) THEN
1356 ASM_REWRITE_TAC[REAL_LE_SUB_RADD, REAL_LE_ADDR] THEN
1357 W(C SUBGOAL_THEN MP_TAC o fst o dest_imp o dest_neg o snd) THENL
1358 [X_GEN_TAC “z:real” THEN STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1359 ONCE_REWRITE_TAC[GSYM ABS_NEG] THEN
1360 REWRITE_TAC[abs, REAL_SUB_LE] THEN
1361 ASM_REWRITE_TAC[REAL_NEG_SUB, REAL_SUB_LE, REAL_LE_SUB_RADD] THEN
1362 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN ASM_REWRITE_TAC[],
1363 DISCH_THEN(fn th => REWRITE_TAC[th]) THEN
1364 DISCH_THEN(X_CHOOSE_THEN “z:real” STRIP_ASSUME_TAC) THEN
1365 FIRST_ASSUM(MP_TAC o AP_TERM “g:real->real”) THEN
1366 SUBGOAL_THEN “g((f:real->real) z) = z” SUBST1_TAC THENL
1367 [FIRST_ASSUM MATCH_MP_TAC THEN
1368 ONCE_REWRITE_TAC[GSYM ABS_NEG] THEN
1369 REWRITE_TAC[abs, REAL_SUB_LE] THEN
1370 ASM_REWRITE_TAC[REAL_NEG_SUB, REAL_SUB_LE, REAL_LE_SUB_RADD] THEN
1371 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
1372 SUBGOAL_THEN “g(f(x + d):real) = x + d” SUBST1_TAC THENL
1373 [FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[REAL_ADD_SUB] THEN
1374 ASM_REWRITE_TAC[abs, REAL_LE_REFL], ALL_TAC] THEN
1375 REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN
1376 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “x:real” THEN
1377 ASM_REWRITE_TAC[REAL_LT_ADDR]],
1378 MP_TAC(SPECL [“f:real->real”, “x:real”, “x + d”, “f(x - d):real”] IVT2) THEN
1379 ASM_REWRITE_TAC[REAL_LE_SUB_RADD, REAL_LE_ADDR] THEN
1380 W(C SUBGOAL_THEN MP_TAC o fst o dest_imp o dest_neg o snd) THENL
1381 [X_GEN_TAC “z:real” THEN STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1382 ASM_REWRITE_TAC[abs, REAL_SUB_LE, REAL_LE_SUB_RADD] THEN
1383 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN ASM_REWRITE_TAC[],
1384 DISCH_THEN(fn th => REWRITE_TAC[th]) THEN
1385 DISCH_THEN(X_CHOOSE_THEN “z:real” STRIP_ASSUME_TAC) THEN
1386 FIRST_ASSUM(MP_TAC o AP_TERM “g:real->real”) THEN
1387 SUBGOAL_THEN “g((f:real->real) z) = z” SUBST1_TAC THENL
1388 [FIRST_ASSUM MATCH_MP_TAC THEN
1389 ASM_REWRITE_TAC[abs, REAL_SUB_LE, REAL_LE_SUB_RADD] THEN
1390 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
1391 SUBGOAL_THEN “g(f(x - d):real) = x - d” SUBST1_TAC THENL
1392 [FIRST_ASSUM MATCH_MP_TAC THEN
1393 REWRITE_TAC[REAL_SUB_SUB, ABS_NEG] THEN
1394 ASM_REWRITE_TAC[abs, REAL_LE_REFL], ALL_TAC] THEN
1395 REWRITE_TAC[] THEN CONV_TAC(RAND_CONV SYM_CONV) THEN
1396 MATCH_MP_TAC REAL_LT_IMP_NE THEN
1397 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC “x:real” THEN
1398 ASM_REWRITE_TAC[REAL_LT_SUB_RADD, REAL_LT_ADDR]]]
1399QED
1400
1401(*---------------------------------------------------------------------------*)
1402(* Similar version for lower bound *)
1403(*---------------------------------------------------------------------------*)
1404
1405Theorem CONT_INJ_LEMMA2:
1406 !f g x d. &0 < d /\
1407 (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
1408 (!z. abs(z - x) <= d ==> f contl z) ==>
1409 ~(!z. abs(z - x) <= d ==> f(x) <= f(z))
1410Proof
1411 REPEAT GEN_TAC THEN STRIP_TAC THEN
1412 MP_TAC(Q.SPECL [‘\x:real. ~(f x)’, ‘\y. (g(~y):real)’, ‘x:real’, ‘d:real’]
1413 CONT_INJ_LEMMA) THEN
1414 BETA_TAC THEN ASM_REWRITE_TAC[REAL_NEGNEG, REAL_LE_NEG] THEN
1415 DISCH_THEN MATCH_MP_TAC THEN
1416 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC CONT_NEG THEN
1417 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC
1418QED
1419
1420(*---------------------------------------------------------------------------*)
1421(* Show there's an interval surrounding f(x) in f[[x - d, x + d]] *)
1422(*---------------------------------------------------------------------------*)
1423
1424Theorem CONT_INJ_RANGE:
1425 !f g x d. &0 < d /\
1426 (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
1427 (!z. abs(z - x) <= d ==> f contl z) ==>
1428 ?e. &0 < e /\
1429 (!y. abs(y - f(x)) <= e ==> ?z. abs(z - x) <= d /\ (f z = y))
1430Proof
1431 REPEAT GEN_TAC THEN STRIP_TAC THEN IMP_RES_TAC REAL_LT_IMP_LE THEN
1432 MP_TAC(SPECL [“f:real->real”, “x - d”, “x + d”] CONT_ATTAINS_ALL) THEN
1433 ASM_REWRITE_TAC[INTERVAL_ABS, REAL_LE_SUB_RADD] THEN
1434 ASM_REWRITE_TAC[GSYM REAL_ADD_ASSOC, REAL_LE_ADDR, REAL_LE_DOUBLE] THEN
1435 DISCH_THEN(X_CHOOSE_THEN “L:real” (X_CHOOSE_THEN “M:real” MP_TAC)) THEN
1436 STRIP_TAC THEN
1437 SUBGOAL_THEN “L <= f(x:real) /\ f(x) <= M” STRIP_ASSUME_TAC THENL
1438 [FIRST_ASSUM MATCH_MP_TAC THEN
1439 ASM_REWRITE_TAC[REAL_SUB_REFL, ABS_0], ALL_TAC] THEN
1440 SUBGOAL_THEN “L < f(x:real) /\ f(x:real) < M” STRIP_ASSUME_TAC THENL
1441 [CONJ_TAC THEN ASM_REWRITE_TAC[REAL_LT_LE] THENL
1442 [DISCH_THEN SUBST_ALL_TAC THEN (MP_TAC o C SPECL CONT_INJ_LEMMA2)
1443 [“f:real->real”, “g:real->real”, “x:real”, “d:real”],
1444 DISCH_THEN(SUBST_ALL_TAC o SYM) THEN (MP_TAC o C SPECL CONT_INJ_LEMMA)
1445 [“f:real->real”, “g:real->real”, “x:real”, “d:real”]] THEN
1446 ASM_REWRITE_TAC[] THEN GEN_TAC THEN
1447 DISCH_THEN(fn t => FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP th t] THEN NO_TAC)),
1448 MP_TAC(SPECL [“f(x:real) - L”, “M - f(x:real)”] REAL_DOWN2) THEN
1449 ASM_REWRITE_TAC[REAL_SUB_LT] THEN
1450 DISCH_THEN(X_CHOOSE_THEN “e:real” STRIP_ASSUME_TAC) THEN
1451 EXISTS_TAC “e:real” THEN ASM_REWRITE_TAC[] THEN
1452 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[GSYM INTERVAL_ABS] THEN
1453 REWRITE_TAC[REAL_LE_SUB_RADD] THEN ONCE_REWRITE_TAC[GSYM CONJ_ASSOC] THEN
1454 FIRST_ASSUM MATCH_MP_TAC THEN UNDISCH_TAC “abs(y - f(x:real)) <= e” THEN
1455 REWRITE_TAC[GSYM INTERVAL_ABS] THEN STRIP_TAC THEN CONJ_TAC THENL
1456 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “f(x:real) - e” THEN
1457 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[REAL_LE_SUB_LADD] THEN
1458 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1459 REWRITE_TAC[GSYM REAL_LE_SUB_LADD],
1460 MATCH_MP_TAC REAL_LE_TRANS THEN
1461 EXISTS_TAC “f(x:real) + (M - f(x))” THEN CONJ_TAC THENL
1462 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “f(x:real) + e” THEN
1463 ASM_REWRITE_TAC[REAL_LE_LADD],
1464 REWRITE_TAC[REAL_SUB_ADD2, REAL_LE_REFL]]] THEN
1465 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]]
1466QED
1467
1468(*---------------------------------------------------------------------------*)
1469(* Continuity of inverse function *)
1470(*---------------------------------------------------------------------------*)
1471
1472Theorem CONT_INVERSE:
1473 !f g x d. &0 < d /\
1474 (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
1475 (!z. abs(z - x) <= d ==> f contl z)
1476 ==> g contl (f x)
1477Proof
1478 REPEAT STRIP_TAC THEN REWRITE_TAC[contl, LIM] THEN
1479 X_GEN_TAC “a:real” THEN DISCH_TAC THEN
1480 MP_TAC(SPECL [“a:real”, “d:real”] REAL_DOWN2) THEN ASM_REWRITE_TAC[] THEN
1481 DISCH_THEN(X_CHOOSE_THEN “e:real” STRIP_ASSUME_TAC) THEN
1482 IMP_RES_TAC REAL_LT_IMP_LE THEN
1483 SUBGOAL_THEN “!z. abs(z - x) <= e ==> (g(f z :real) = z)” ASSUME_TAC THENL
1484 [X_GEN_TAC “z:real” THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1485 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “e:real” THEN ASM_REWRITE_TAC[],
1486 ALL_TAC] THEN
1487 SUBGOAL_THEN “!z. abs(z - x) <= e ==> (f contl z)” ASSUME_TAC THENL
1488 [X_GEN_TAC “z:real” THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1489 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC “e:real” THEN ASM_REWRITE_TAC[],
1490 ALL_TAC] THEN
1491 UNDISCH_TAC “!z. abs(z - x) <= d ==> (g(f z :real) = z)” THEN
1492 UNDISCH_TAC “!z. abs(z - x) <= d ==> (f contl z)” THEN
1493 DISCH_THEN(K ALL_TAC) THEN DISCH_THEN(K ALL_TAC) THEN
1494 (MP_TAC o C SPECL CONT_INJ_RANGE)
1495 [“f:real->real”, “g:real->real”, “x:real”, “e:real”] THEN
1496 ASM_REWRITE_TAC[] THEN
1497 DISCH_THEN(X_CHOOSE_THEN “k:real” STRIP_ASSUME_TAC) THEN
1498 EXISTS_TAC “k:real” THEN ASM_REWRITE_TAC[] THEN
1499 X_GEN_TAC “h:real” THEN BETA_TAC THEN REWRITE_TAC[REAL_SUB_RZERO] THEN
1500 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (ASSUME_TAC o MATCH_MP REAL_LT_IMP_LE)) THEN
1501 REWRITE_TAC[GSYM ABS_NZ] THEN DISCH_TAC THEN
1502 FIRST_ASSUM(fn th => MP_TAC(SPEC “f(x:real) + h” th) THEN
1503 REWRITE_TAC[REAL_ADD_SUB, ASSUME “abs(h) <= k”] THEN
1504 DISCH_THEN(X_CHOOSE_THEN “z:real” STRIP_ASSUME_TAC)) THEN
1505 FIRST_ASSUM(UNDISCH_TAC o assert is_eq o concl) THEN
1506 DISCH_THEN(SUBST1_TAC o SYM) THEN
1507 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “e:real” THEN
1508 SUBGOAL_THEN “(g((f:real->real)(z)) = z) /\ (g(f(x)) = x)”
1509 (fn t => ASM_REWRITE_TAC[t]) THEN CONJ_TAC THEN
1510 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[REAL_SUB_REFL, ABS_0]
1511QED
1512
1513(*---------------------------------------------------------------------------*)
1514(* Differentiability of inverse function *)
1515(*---------------------------------------------------------------------------*)
1516
1517Theorem DIFF_INVERSE:
1518 !f g l x d. &0 < d /\
1519 (!z. abs(z - x) <= d ==> (g(f(z)) = z)) /\
1520 (!z. abs(z - x) <= d ==> f contl z) /\
1521 (f diffl l)(x) /\
1522 ~(l = &0)
1523 ==> (g diffl (inv l))(f x)
1524Proof
1525 REPEAT STRIP_TAC THEN UNDISCH_TAC “(f diffl l)(x)” THEN
1526 DISCH_THEN(fn th => ASSUME_TAC(MATCH_MP DIFF_CONT th) THEN MP_TAC th) THEN
1527 REWRITE_TAC[DIFF_CARAT] THEN
1528 DISCH_THEN(X_CHOOSE_THEN “h:real->real” STRIP_ASSUME_TAC) THEN
1529 EXISTS_TAC “\y. if (y = f(x)) then inv(h(g y))
1530 else (g(y) - g(f(x:real))) / (y - f(x))” THEN
1531 BETA_TAC THEN ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
1532 [X_GEN_TAC “z:real” THEN COND_CASES_TAC THEN
1533 ASM_REWRITE_TAC[REAL_SUB_REFL, REAL_MUL_RZERO] THEN
1534 CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_RMUL THEN
1535 ASM_REWRITE_TAC[REAL_SUB_0],
1536 ALL_TAC,
1537 FIRST_ASSUM(SUBST1_TAC o SYM) THEN REPEAT AP_TERM_TAC THEN
1538 FIRST_ASSUM MATCH_MP_TAC THEN
1539 REWRITE_TAC[REAL_SUB_REFL, ABS_0] THEN
1540 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]] THEN
1541 REWRITE_TAC[CONTL_LIM] THEN BETA_TAC THEN REWRITE_TAC[] THEN
1542 SUBGOAL_THEN “g((f:real->real)(x)) = x” ASSUME_TAC THENL
1543 [FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[REAL_SUB_REFL, ABS_0] THEN
1544 MATCH_MP_TAC REAL_LT_IMP_LE, ALL_TAC] THEN ASM_REWRITE_TAC[] THEN
1545 MATCH_MP_TAC LIM_TRANSFORM THEN
1546 EXISTS_TAC “\y:real. inv(h(g(y):real))” THEN
1547 BETA_TAC THEN CONJ_TAC THENL
1548 [ALL_TAC,
1549 (SUBST1_TAC o SYM o ONCE_DEPTH_CONV BETA_CONV)
1550 “\y. inv((\y:real. h(g(y):real)) y)” THEN
1551 MATCH_MP_TAC LIM_INV THEN ASM_REWRITE_TAC[] THEN
1552 SUBGOAL_THEN “(\y:real. h(g(y):real)) contl (f(x:real))” MP_TAC THENL
1553 [MATCH_MP_TAC CONT_COMPOSE THEN ASM_REWRITE_TAC[] THEN
1554 MATCH_MP_TAC CONT_INVERSE THEN EXISTS_TAC “d:real”,
1555 REWRITE_TAC[CONTL_LIM] THEN BETA_TAC] THEN
1556 ASM_REWRITE_TAC[]] THEN
1557 SUBGOAL_THEN “?e. &0 < e /\
1558 !y. &0 < abs(y - f(x:real)) /\
1559 abs(y - f(x:real)) < e ==>
1560 (f(g(y)) = y) /\ ~(h(g(y)) = &0)”
1561 STRIP_ASSUME_TAC THENL
1562 [ALL_TAC,
1563 REWRITE_TAC[LIM] THEN X_GEN_TAC “k:real” THEN DISCH_TAC THEN
1564 EXISTS_TAC “e:real” THEN ASM_REWRITE_TAC[] THEN
1565 X_GEN_TAC “y:real” THEN
1566 DISCH_THEN(fn th => FIRST_ASSUM(STRIP_ASSUME_TAC o C MATCH_MP th) THEN
1567 ASSUME_TAC(REWRITE_RULE[GSYM ABS_NZ, REAL_SUB_0] (CONJUNCT1 th))) THEN
1568 BETA_TAC THEN ASM_REWRITE_TAC[REAL_SUB_RZERO] THEN
1569 SUBGOAL_THEN “y - f(x) = h(g(y)) * (g(y) - x)”
1570 SUBST1_TAC
1571 THENL
1572 [FIRST_ASSUM(fn th => GEN_REWR_TAC RAND_CONV [GSYM th]) THEN
1573 REWRITE_TAC[ASSUME “f((g:real->real)(y)) = y”],
1574 UNDISCH_TAC “&0 < k” THEN
1575 MATCH_MP_TAC(TAUT_CONV “(a = b) ==> a ==> b”) THEN
1576 AP_THM_TAC THEN AP_TERM_TAC THEN
1577 CONV_TAC SYM_CONV THEN REWRITE_TAC[ABS_ZERO, REAL_SUB_0]] THEN
1578 SUBGOAL_THEN “~(g(y:real) - x = &0)” ASSUME_TAC THENL
1579 [REWRITE_TAC[REAL_SUB_0] THEN
1580 DISCH_THEN(MP_TAC o AP_TERM “f:real->real”) THEN
1581 ASM_REWRITE_TAC[], REWRITE_TAC[real_div]] THEN
1582 SUBGOAL_THEN “inv((h(g(y))) * (g(y:real) - x)) =
1583 inv(h(g(y))) * inv(g(y) - x)” SUBST1_TAC THENL
1584 [MATCH_MP_TAC REAL_INV_MUL THEN ASM_REWRITE_TAC[],
1585 REWRITE_TAC[REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1586 REWRITE_TAC[REAL_MUL_ASSOC] THEN
1587 GEN_REWR_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
1588 AP_THM_TAC THEN AP_TERM_TAC THEN
1589 MATCH_MP_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[]]] THEN
1590 SUBGOAL_THEN
1591 “?e. &0 < e /\
1592 !y. &0 < abs(y - f(x:real)) /\
1593 abs(y - f(x)) < e ==> (f(g(y)) = y)”
1594 (X_CHOOSE_THEN “c:real” STRIP_ASSUME_TAC) THENL
1595 [MP_TAC(SPECL [“f:real->real”, “g:real->real”,
1596 “x:real”, “d:real”] CONT_INJ_RANGE) THEN
1597 ASM_REWRITE_TAC[] THEN
1598 DISCH_THEN(X_CHOOSE_THEN “e:real” STRIP_ASSUME_TAC) THEN
1599 EXISTS_TAC “e:real” THEN ASM_REWRITE_TAC[] THEN
1600 X_GEN_TAC “y:real” THEN DISCH_THEN(MP_TAC o CONJUNCT2) THEN
1601 DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_IMP_LE) THEN
1602 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
1603 DISCH_THEN(X_CHOOSE_THEN “z:real” STRIP_ASSUME_TAC) THEN
1604 UNDISCH_TAC “(f:real->real)(z) = y” THEN
1605 DISCH_THEN(SUBST1_TAC o SYM) THEN AP_TERM_TAC THEN
1606 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[], ALL_TAC] THEN
1607 SUBGOAL_THEN
1608 “?e. &0 < e /\
1609 !y. &0 < abs(y - f(x:real)) /\
1610 abs(y - f(x)) < e
1611 ==> ~((h:real->real)(g(y)) = &0)”
1612 (X_CHOOSE_THEN “b:real” STRIP_ASSUME_TAC) THENL
1613 [ALL_TAC,
1614 MP_TAC(SPECL [“b:real”, “c:real”] REAL_DOWN2) THEN
1615 ASM_REWRITE_TAC[] THEN
1616 DISCH_THEN(X_CHOOSE_THEN “e:real” STRIP_ASSUME_TAC) THEN
1617 EXISTS_TAC “e:real” THEN ASM_REWRITE_TAC[] THEN
1618 X_GEN_TAC “y:real” THEN STRIP_TAC THEN CONJ_TAC THEN
1619 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1620 MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC “e:real” THEN
1621 ASM_REWRITE_TAC[]] THEN
1622 SUBGOAL_THEN “(\y. h(g(y:real):real)) contl (f(x:real))” MP_TAC THENL
1623 [MATCH_MP_TAC CONT_COMPOSE THEN ASM_REWRITE_TAC[] THEN
1624 MATCH_MP_TAC CONT_INVERSE THEN EXISTS_TAC “d:real” THEN
1625 ASM_REWRITE_TAC[], ALL_TAC] THEN
1626 REWRITE_TAC[CONTL_LIM, LIM] THEN
1627 DISCH_THEN(MP_TAC o SPEC “abs(l)”) THEN
1628 ASM_REWRITE_TAC[GSYM ABS_NZ] THEN
1629 (****begin new*****)
1630 REWRITE_TAC[ABS_NZ] THEN
1631 (****end new******)
1632 BETA_TAC THEN ASM_REWRITE_TAC[] THEN
1633 DISCH_THEN(X_CHOOSE_THEN “e:real” STRIP_ASSUME_TAC) THEN
1634 EXISTS_TAC “e:real” THEN ASM_REWRITE_TAC[ABS_NZ] THEN
1635 X_GEN_TAC “y:real” THEN
1636 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
1637 REWRITE_TAC[GSYM ABS_NZ] THEN
1638 CONV_TAC CONTRAPOS_CONV THEN ASM_REWRITE_TAC[] THEN
1639 DISCH_THEN SUBST1_TAC THEN
1640 REWRITE_TAC[REAL_SUB_LZERO, ABS_NEG, REAL_LT_REFL]
1641QED
1642
1643
1644Theorem DIFF_INVERSE_LT:
1645 !f g l x d. &0 < d /\
1646 (!z. abs(z - x) < d ==> (g(f(z)) = z)) /\
1647 (!z. abs(z - x) < d ==> f contl z) /\
1648 (f diffl l)(x) /\
1649 ~(l = &0)
1650 ==> (g diffl (inv l))(f x)
1651Proof
1652 REPEAT STRIP_TAC THEN MATCH_MP_TAC DIFF_INVERSE THEN
1653 EXISTS_TAC (Term `d / &2`) THEN ASM_REWRITE_TAC[REAL_LT_HALF1] THEN
1654 REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1655 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC (Term `d / &2`) THEN
1656 ASM_REWRITE_TAC[REAL_LT_HALF2]
1657QED
1658
1659(*---------------------------------------------------------------------------*)
1660(* Lemma about introducing a closed ball in an open interval *)
1661(*---------------------------------------------------------------------------*)
1662
1663Theorem INTERVAL_CLEMMA:
1664 !a b x. a < x /\ x < b ==>
1665 ?d. &0 < d /\ !y. abs(y - x) <= d ==> a < y /\ y < b
1666Proof
1667 REPEAT GEN_TAC THEN STRIP_TAC THEN
1668 MP_TAC(SPECL [“x - a”, “b - x”] REAL_DOWN2) THEN
1669 ASM_REWRITE_TAC[REAL_SUB_LT] THEN ASM_REWRITE_TAC[REAL_LT_SUB_LADD] THEN
1670 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
1671 EXISTS_TAC “d:real” THEN
1672 ASM_REWRITE_TAC[GSYM INTERVAL_ABS, REAL_LE_SUB_RADD] THEN
1673 X_GEN_TAC “y:real” THEN STRIP_TAC THEN CONJ_TAC THENL
1674 [SUBGOAL_THEN “(d + a) < d + y” MP_TAC THENL
1675 [GEN_REWR_TAC RAND_CONV [REAL_ADD_SYM] THEN
1676 MATCH_MP_TAC REAL_LTE_TRANS THEN
1677 EXISTS_TAC “x:real” THEN ASM_REWRITE_TAC[],
1678 REWRITE_TAC[REAL_LT_LADD]],
1679 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC “x + d” THEN
1680 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1681 ASM_REWRITE_TAC[]]
1682QED
1683
1684(*---------------------------------------------------------------------------*)
1685(* Alternative version of inverse function theorem *)
1686(*---------------------------------------------------------------------------*)
1687
1688Theorem DIFF_INVERSE_OPEN:
1689 !f g l a x b.
1690 a < x /\
1691 x < b /\
1692 (!z. a < z /\ z < b ==> (g(f(z)) = z) /\ f contl z) /\
1693 (f diffl l)(x) /\
1694 ~(l = &0)
1695 ==> (g diffl (inv l))(f x)
1696Proof
1697 REPEAT GEN_TAC THEN STRIP_TAC THEN
1698 MATCH_MP_TAC DIFF_INVERSE THEN
1699 MP_TAC(SPECL [“a:real”, “b:real”,
1700 “x:real”] INTERVAL_CLEMMA) THEN
1701 ASM_REWRITE_TAC[] THEN
1702 DISCH_THEN(X_CHOOSE_THEN “d:real” STRIP_ASSUME_TAC) THEN
1703 EXISTS_TAC “d:real” THEN ASM_REWRITE_TAC[] THEN
1704 CONJ_TAC THEN GEN_TAC THEN
1705 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
1706 DISCH_THEN(fn th => FIRST_ASSUM(fn t => REWRITE_TAC[MATCH_MP t th]))
1707QED
1708
1709(* ------------------------------------------------------------------------- *)
1710(* Every derivative is Darboux continuous. *)
1711(* ------------------------------------------------------------------------- *)
1712
1713Theorem IVT_DERIVATIVE_0 :
1714 !f f' a b.
1715 a <= b /\
1716 (!x. a <= x /\ x <= b ==> (f diffl f'(x))(x)) /\
1717 f'(a) > &0 /\ f'(b) < &0
1718 ==> ?z. a < z /\ z < b /\ (f'(z) = &0)
1719Proof
1720 REPEAT GEN_TAC THEN REWRITE_TAC[real_gt] THEN
1721 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) empty_rewrites [REAL_LE_LT] THEN
1722 STRIP_TAC THENL [ALL_TAC, ASM_MESON_TAC[REAL_LT_ANTISYM]] THEN
1723 Q.SUBGOAL_THEN `?w. (!x. a <= x /\ x <= b ==> f x <= w) /\
1724 (?x. a <= x /\ x <= b /\ (f x = w))`
1725 MP_TAC THENL
1726 [ MATCH_MP_TAC CONT_ATTAINS THEN
1727 ASM_MESON_TAC[REAL_LT_IMP_LE, DIFF_CONT], ALL_TAC] THEN
1728 DISCH_THEN(CHOOSE_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1729 DISCH_THEN(Q.X_CHOOSE_THEN `z:real` STRIP_ASSUME_TAC) THEN
1730
1731 Q.EXISTS_TAC `z:real` >> Cases_on `z:real = a` >-
1732 ( Q.UNDISCH_THEN `z:real = a` SUBST_ALL_TAC THEN
1733 MP_TAC(Q.SPECL[`f:real->real`, `a:real`, `(f':real->real) a`] DIFF_LINC) THEN
1734 ASM_SIMP_TAC std_ss [REAL_LE_REFL, REAL_LT_IMP_LE] THEN
1735 DISCH_THEN(Q.X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
1736 MP_TAC(Q.SPECL [`d:real`, `b - a`] REAL_DOWN2) THEN
1737 ASM_REWRITE_TAC[REAL_LT_SUB_LADD, REAL_ADD_LID] THEN
1738 DISCH_THEN(Q.X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
1739 Q.UNDISCH_TAC `!h. &0 < h /\ h < d ==> w < f (a + h)` THEN
1740 DISCH_THEN(MP_TAC o Q.SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
1741 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
1742 REWRITE_TAC[REAL_NOT_LT] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1743 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1744 ASM_SIMP_TAC std_ss [REAL_LE_ADDL, REAL_LT_IMP_LE] ) \\
1745
1746 Cases_on `z:real = b` >-
1747 ( Q.UNDISCH_THEN `z:real = b` SUBST_ALL_TAC THEN
1748 MP_TAC(Q.SPECL[`f:real->real`, `b:real`, `(f':real->real) b`] DIFF_LDEC) THEN
1749 ASM_SIMP_TAC std_ss [REAL_LE_REFL, REAL_LT_IMP_LE] THEN
1750 DISCH_THEN(Q.X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
1751 MP_TAC(Q.SPECL [`d:real`, `b - a`] REAL_DOWN2) THEN
1752 ASM_REWRITE_TAC[REAL_LT_SUB_LADD, REAL_ADD_LID] THEN
1753 DISCH_THEN(Q.X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
1754 Q.UNDISCH_TAC `!h. &0 < h /\ h < d ==> w < f (b - h)` THEN
1755 DISCH_THEN(MP_TAC o Q.SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
1756 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
1757 REWRITE_TAC[REAL_NOT_LT] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1758 REWRITE_TAC[REAL_LE_SUB_LADD, REAL_LE_SUB_RADD] THEN
1759 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1760 ASM_SIMP_TAC std_ss [REAL_LE_ADDL, REAL_LT_IMP_LE] ) \\
1761 Q.SUBGOAL_THEN `a < z /\ z < b` STRIP_ASSUME_TAC THENL
1762 [ ASM_SIMP_TAC std_ss [REAL_LT_LE], ALL_TAC ] THEN
1763 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIFF_LMAX THEN
1764 MP_TAC(Q.SPECL [`z - a`, `b - z`] REAL_DOWN2) THEN
1765 ASM_REWRITE_TAC[REAL_LT_SUB_LADD, REAL_ADD_LID] THEN
1766 DISCH_THEN(Q.X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
1767 qexistsl_tac [`f:real->real`, `z:real`] THEN
1768 ASM_SIMP_TAC std_ss [REAL_LT_IMP_LE] THEN
1769 Q.EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN
1770 DISCH_THEN(fn th => FIRST_ASSUM MATCH_MP_TAC THEN MP_TAC th) THEN
1771 MAP_EVERY Q.UNDISCH_TAC [`e + z < b`, `e + a < z`] THEN
1772 REAL_ARITH_TAC
1773QED
1774
1775Theorem IVT_DERIVATIVE_POS :
1776 !f f' a b y.
1777 a <= b /\
1778 (!x. a <= x /\ x <= b ==> (f diffl f'(x))(x)) /\
1779 f'(a) > y /\ f'(b) < y
1780 ==> ?z. a < z /\ z < b /\ (f'(z) = y)
1781Proof
1782 REWRITE_TAC[real_gt] THEN REPEAT STRIP_TAC THEN
1783 MP_TAC(Q.SPECL [`\x. f(x) - y * x`, `\x:real. f'(x) - y`,
1784 `a:real`, `b:real`] IVT_DERIVATIVE_0) THEN
1785 ASM_SIMP_TAC std_ss [real_gt] THEN
1786 ASM_REWRITE_TAC[REAL_LT_SUB_LADD, REAL_LT_SUB_RADD] THEN
1787 ASM_REWRITE_TAC[REAL_EQ_SUB_RADD, REAL_ADD_LID] THEN
1788 GEN_REWRITE_TAC (funpow 2 LAND_CONV o BINDER_CONV o RAND_CONV o
1789 LAND_CONV o RAND_CONV) empty_rewrites [GSYM REAL_MUL_RID] THEN
1790 ASM_SIMP_TAC std_ss [DIFF_SUB, DIFF_X, DIFF_CMUL]
1791QED
1792
1793Theorem IVT_DERIVATIVE_NEG :
1794 !f f' a b y.
1795 a <= b /\
1796 (!x. a <= x /\ x <= b ==> (f diffl f'(x))(x)) /\
1797 f'(a) < y /\ f'(b) > y
1798 ==> ?z. a < z /\ z < b /\ (f'(z) = y)
1799Proof
1800 REWRITE_TAC[real_gt] THEN REPEAT STRIP_TAC THEN
1801 MP_TAC(Q.SPECL [`\x:real. ~(f x)`, `\x:real. ~(f' x)`,
1802 `a:real`, `b:real`, `~y`] IVT_DERIVATIVE_POS) THEN
1803 ASM_SIMP_TAC std_ss [real_gt, REAL_LT_NEG, REAL_EQ_NEG] THEN
1804 ASM_SIMP_TAC std_ss [DIFF_NEG]
1805QED
1806
1807(*---------------------------------------------------------------------------*)
1808(* Miscellaneous Results (for use in hyperbolic trigonemtry library) *)
1809(*---------------------------------------------------------------------------*)
1810
1811Theorem DIFF_CONG:
1812 !f g l m x y. (?a b. a < y /\ y < b /\ !z. a < z /\ z < b ==> (f z = g z)) /\
1813 (l = m) /\ (x = y) ==> ((f diffl l) x <=> (g diffl m) y)
1814Proof
1815 simp[] >>
1816 ‘!f g m y. (?a b. a < y /\ y < b /\ !z. a < z /\ z < b ==> (f z = g z)) /\
1817 (f diffl m) y ==> (g diffl m) y’ suffices_by metis_tac[] >>
1818 rw[] >> pop_assum mp_tac >> simp[diffl,LIM] >> rw[] >>
1819 first_x_assum $ drule_then assume_tac >> gs[] >>
1820 qexists ‘min d (min (y - a) (b - y))’ >> simp[REAL_LT_MIN,REAL_SUB_LT] >> rw[] >>
1821 first_x_assum $ drule_all_then mp_tac >>
1822 ‘f (y + h) = g (y + h)’ suffices_by simp[] >> first_x_assum irule >>
1823 gs[ABS_BOUNDS_LT,REAL_NEG_SUB,REAL_LT_SUB_LADD,REAL_LT_SUB_RADD] >>
1824 simp[REAL_ADD_COMM]
1825QED
1826
1827Theorem DIFF_CONG_IMP :
1828 !f g y x. (!x. f x = g x) /\ (g diffl y) x ==> (f diffl y) x
1829Proof
1830 rw [diffl]
1831QED
1832
1833Theorem DIFF_POS_MONO_LT_INTERVAL:
1834 !f s. is_interval s /\ (!z. z IN s ==> f contl z) /\
1835 (!z. z IN interior s ==> ?l. 0 < l /\ (f diffl l) z) ==>
1836 !x y. x IN s /\ y IN s /\ x < y ==> f x < f y
1837Proof
1838 rw[] >>
1839 ‘!z. x < z /\ z < y ==> z IN interior s’ by (
1840 rw[interior] >> qexists ‘interval (x,y)’ >> simp[OPEN_INTERVAL] >>
1841 gs[SUBSET_DEF,OPEN_interval,IS_INTERVAL] >> metis_tac[REAL_LE_LT]) >>
1842 qspecl_then [‘f’,‘x’,‘y’] mp_tac MVT >> impl_tac
1843 >- (gs[IS_INTERVAL] >> metis_tac[differentiable]) >>
1844 rw[] >> pop_assum mp_tac >> simp[REAL_EQ_SUB_RADD] >> disch_then kall_tac >>
1845 irule REAL_LT_MUL >> simp[REAL_SUB_LT] >>
1846 ntac 2 $ first_x_assum $ dxrule_all_then assume_tac >> metis_tac[DIFF_UNIQ]
1847QED
1848
1849Theorem DIFF_NEG_ANTIMONO_LT_INTERVAL:
1850 !f s. is_interval s /\ (!z. z IN s ==> f contl z) /\
1851 (!z. z IN interior s ==> ?l. l < 0 /\ (f diffl l) z) ==>
1852 !x y. x IN s /\ y IN s /\ x < y ==> f y < f x
1853Proof
1854 rw[] >> qspecl_then [‘λw. -f w’,‘s’] mp_tac DIFF_POS_MONO_LT_INTERVAL >>
1855 simp[] >> disch_then irule >> simp[CONT_NEG] >> rw[] >>
1856 first_x_assum $ dxrule_then assume_tac >> gs[] >>
1857 qexists ‘-l’ >> simp[DIFF_NEG]
1858QED
1859
1860Theorem DIFF_POS_MONO_LT_UU:
1861 !f. (!z. ?l. 0 < l /\ (f diffl l) z) ==>
1862 !x y. x < y ==> f x < f y
1863Proof
1864 rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1865 qexists ‘univ(:real)’ >> simp[IS_INTERVAL_POSSIBILITIES] >>
1866 metis_tac[DIFF_CONT]
1867QED
1868
1869Theorem DIFF_POS_MONO_LT_OU:
1870 !f a. (!z. a < z ==> ?l. 0 < l /\ (f diffl l) z) ==>
1871 !x y. a < x /\ x < y ==> f x < f y
1872Proof
1873 rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1874 qexists ‘{x | a < x}’ >>
1875 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1876 metis_tac[DIFF_CONT]
1877QED
1878
1879Theorem DIFF_POS_MONO_LT_UO:
1880 !f b. (!z. z < b ==> ?l. 0 < l /\ (f diffl l) z) ==>
1881 !x y. y < b /\ x < y ==> f x < f y
1882Proof
1883 rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1884 qexists ‘{x | x < b}’ >>
1885 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1886 metis_tac[DIFF_CONT]
1887QED
1888
1889Theorem DIFF_POS_MONO_LT_CU:
1890 !f a. f contl a /\ (!z. a < z ==> ?l. 0 < l /\ (f diffl l) z) ==>
1891 !x y. a <= x /\ x < y ==> f x < f y
1892Proof
1893 rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1894 qexists ‘{x | a <= x}’ >>
1895 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_IMP_LE,REAL_LET_TRANS,SF SFY_ss] >>
1896 metis_tac[DIFF_CONT,REAL_LE_LT]
1897QED
1898
1899Theorem DIFF_POS_MONO_LT_UC:
1900 !f b. f contl b /\ (!z. z < b ==> ?l. 0 < l /\ (f diffl l) z) ==>
1901 !x y. y <= b /\ x < y ==> f x < f y
1902Proof
1903 rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1904 qexists ‘{x | x <= b}’ >>
1905 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_IMP_LE,REAL_LTE_TRANS,SF SFY_ss] >>
1906 metis_tac[DIFF_CONT,REAL_LE_LT]
1907QED
1908
1909Theorem DIFF_POS_MONO_LT_OO:
1910 !f a b. (!z. a < z /\ z < b ==> ?l. 0 < l /\ (f diffl l) z) ==>
1911 !x y. a < x /\ y < b /\ x < y ==> f x < f y
1912Proof
1913 rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1914 qexists ‘{x | a < x /\ x < b}’ >>
1915 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1916 metis_tac[DIFF_CONT]
1917QED
1918
1919Theorem DIFF_POS_MONO_LT_CO:
1920 !f a b. f contl a /\ (!z. a < z /\ z < b ==> ?l. 0 < l /\ (f diffl l) z) ==>
1921 !x y. a <= x /\ y < b /\ x < y ==> f x < f y
1922Proof
1923 rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1924 qexists ‘{x | a <= x /\ x < b}’ >>
1925 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
1926 REAL_LT_TRANS,REAL_LT_IMP_LE,REAL_LET_TRANS,SF SFY_ss] >>
1927 metis_tac[DIFF_CONT,REAL_LE_LT]
1928QED
1929
1930Theorem DIFF_POS_MONO_LT_OC:
1931 !f a b. f contl b /\ (!z. a < z /\ z < b ==> ?l. 0 < l /\ (f diffl l) z) ==>
1932 !x y. a < x /\ y <= b /\ x < y ==> f x < f y
1933Proof
1934 rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1935 qexists ‘{x | a < x /\ x <= b}’ >>
1936 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
1937 REAL_LT_TRANS,REAL_LT_IMP_LE,REAL_LTE_TRANS,SF SFY_ss] >>
1938 metis_tac[DIFF_CONT,REAL_LE_LT]
1939QED
1940
1941Theorem DIFF_POS_MONO_LT_CC:
1942 !f a b. f contl a /\ f contl b /\
1943 (!z. a < z /\ z < b ==> ?l. 0 < l /\ (f diffl l) z) ==>
1944 !x y. a <= x /\ y <= b /\ x < y ==> f x < f y
1945Proof
1946 rw[] >> irule DIFF_POS_MONO_LT_INTERVAL >> simp[] >>
1947 qexists ‘{x | a <= x /\ x <= b}’ >>
1948 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
1949 REAL_LT_IMP_LE,REAL_LET_TRANS,REAL_LTE_TRANS,SF SFY_ss] >>
1950 metis_tac[DIFF_CONT,REAL_LE_LT]
1951QED
1952
1953Theorem DIFF_NEG_ANTIMONO_LT_UU:
1954 !f. (!z. ?l. l < 0 /\ (f diffl l) z) ==>
1955 !x y. x < y ==> f y < f x
1956Proof
1957 rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1958 qexists ‘univ(:real)’ >> simp[IS_INTERVAL_POSSIBILITIES] >>
1959 metis_tac[DIFF_CONT]
1960QED
1961
1962Theorem DIFF_NEG_ANTIMONO_LT_OU:
1963 !f a. (!z. a < z ==> ?l. l < 0 /\ (f diffl l) z) ==>
1964 !x y. a < x /\ x < y ==> f y < f x
1965Proof
1966 rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1967 qexists ‘{x | a < x}’ >>
1968 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1969 metis_tac[DIFF_CONT]
1970QED
1971
1972Theorem DIFF_NEG_ANTIMONO_LT_UO:
1973 !f b. (!z. z < b ==> ?l. l < 0 /\ (f diffl l) z) ==>
1974 !x y. y < b /\ x < y ==> f y < f x
1975Proof
1976 rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1977 qexists ‘{x | x < b}’ >>
1978 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
1979 metis_tac[DIFF_CONT]
1980QED
1981
1982Theorem DIFF_NEG_ANTIMONO_LT_CU:
1983 !f a. f contl a /\ (!z. a < z ==> ?l. l < 0 /\ (f diffl l) z) ==>
1984 !x y. a <= x /\ x < y ==> f y < f x
1985Proof
1986 rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1987 qexists ‘{x | a <= x}’ >>
1988 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_IMP_LE,REAL_LET_TRANS,SF SFY_ss] >>
1989 metis_tac[DIFF_CONT,REAL_LE_LT]
1990QED
1991
1992Theorem DIFF_NEG_ANTIMONO_LT_UC:
1993 !f b. f contl b /\ (!z. z < b ==> ?l. l < 0 /\ (f diffl l) z) ==>
1994 !x y. y <= b /\ x < y ==> f y < f x
1995Proof
1996 rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
1997 qexists ‘{x | x <= b}’ >>
1998 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_IMP_LE,REAL_LTE_TRANS,SF SFY_ss] >>
1999 metis_tac[DIFF_CONT,REAL_LE_LT]
2000QED
2001
2002Theorem DIFF_NEG_ANTIMONO_LT_OO:
2003 !f a b. (!z. a < z /\ z < b ==> ?l. l < 0 /\ (f diffl l) z) ==>
2004 !x y. a < x /\ y < b /\ x < y ==> f y < f x
2005Proof
2006 rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
2007 qexists ‘{x | a < x /\ x < b}’ >>
2008 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,REAL_LT_TRANS,SF SFY_ss] >>
2009 metis_tac[DIFF_CONT]
2010QED
2011
2012Theorem DIFF_NEG_ANTIMONO_LT_CO:
2013 !f a b. f contl a /\ (!z. a < z /\ z < b ==> ?l. l < 0 /\ (f diffl l) z) ==>
2014 !x y. a <= x /\ y < b /\ x < y ==> f y < f x
2015Proof
2016 rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
2017 qexists ‘{x | a <= x /\ x < b}’ >>
2018 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
2019 REAL_LT_TRANS,REAL_LT_IMP_LE,REAL_LET_TRANS,SF SFY_ss] >>
2020 metis_tac[DIFF_CONT,REAL_LE_LT]
2021QED
2022
2023Theorem DIFF_NEG_ANTIMONO_LT_OC:
2024 !f a b. f contl b /\ (!z. a < z /\ z < b ==> ?l. l < 0 /\ (f diffl l) z) ==>
2025 !x y. a < x /\ y <= b /\ x < y ==> f y < f x
2026Proof
2027 rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
2028 qexists ‘{x | a < x /\ x <= b}’ >>
2029 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
2030 REAL_LT_TRANS,REAL_LT_IMP_LE,REAL_LTE_TRANS,SF SFY_ss] >>
2031 metis_tac[DIFF_CONT,REAL_LE_LT]
2032QED
2033
2034Theorem DIFF_NEG_ANTIMONO_LT_CC:
2035 !f a b. f contl a /\ f contl b /\
2036 (!z. a < z /\ z < b ==> ?l. l < 0 /\ (f diffl l) z) ==>
2037 !x y. a <= x /\ y <= b /\ x < y ==> f y < f x
2038Proof
2039 rw[] >> irule DIFF_NEG_ANTIMONO_LT_INTERVAL >> simp[] >>
2040 qexists ‘{x | a <= x /\ x <= b}’ >>
2041 simp[INTERIOR_INTERVAL_CASES,IS_INTERVAL_POSSIBILITIES,
2042 REAL_LT_IMP_LE,REAL_LET_TRANS,REAL_LTE_TRANS,SF SFY_ss] >>
2043 metis_tac[DIFF_CONT,REAL_LE_LT]
2044QED
2045
2046Theorem DIFF_EQ_FUN_EQ:
2047 !f g s. is_interval s /\ (!z. z IN s ==> f contl z) /\ (!z. z IN s ==> g contl z) /\
2048 (!z. z IN interior s ==> ?l. (f diffl l) z /\ (g diffl l) z) ==>
2049 ?c. !x. x IN s ==> (f x = g x + c)
2050Proof
2051 rw[] >> Cases_on ‘s = {} ’ >- simp[] >>
2052 gs[GSYM MEMBER_NOT_EMPTY] >> rename [‘w IN s’] >>
2053 qexists ‘f w - g w’ >> rw[] >>
2054 ‘f x - g x = f w - g w’ suffices_by (
2055 simp[REAL_EQ_SUB_RADD,real_sub,REAL_ADD_ASSOC] >>
2056 disch_then kall_tac >> metis_tac[REAL_ADD_COMM,REAL_ADD_ASSOC]) >>
2057 Cases_on ‘x = w’ >- simp[] >> wlog_tac ‘w < x’ [‘x’,‘w’]
2058 >- (first_x_assum $ qspecl_then [‘w’,‘x’] mp_tac >> simp[] >>
2059 ‘x < w’ suffices_by simp[] >> gs[REAL_NOT_LT,REAL_LE_LT]) >>
2060 ‘!z. z IN s ==> (λx. f x - g x) contl z’ by simp[CONT_SUB] >>
2061 ‘!z. z IN interior s ==> ((λx. f x - g x) diffl 0) z’ by (
2062 rw[] >> qpat_x_assum ‘!z. z IN interior s ==> _’ $ dxrule_then assume_tac >>
2063 gs[] >> qspecl_then [‘f’,‘g’,‘l’,‘l’,‘z’] mp_tac DIFF_SUB >> simp[]) >>
2064 ‘!z. w < z /\ z < x ==> z IN interior s’ by (rw[interior] >>
2065 qexists ‘interval (w,x)’ >> simp[OPEN_INTERVAL,OPEN_interval,SUBSET_DEF] >>
2066 metis_tac[REAL_LE_LT,IS_INTERVAL]) >>
2067 qspecl_then [‘λx. f x - g x’,‘w’,‘x’] mp_tac MVT >> simp[] >> impl_tac
2068 >- (conj_tac >- metis_tac[IS_INTERVAL] >> qx_gen_tac ‘y’ >> strip_tac >>
2069 simp[differentiable] >> first_x_assum $ irule_at Any >> simp[]) >>
2070 rw[] >> ntac 2 $ first_x_assum $ dxrule_all_then assume_tac >>
2071 dxrule_all_then assume_tac DIFF_UNIQ >> rw[] >> gs[REAL_MUL_LZERO]
2072QED
2073
2074(*---------------------------------------------------------------------------*)
2075(* Higher Order Derivatives and Differentiability (Kai Phan and Chun Tian) *)
2076(*---------------------------------------------------------------------------*)
2077(*
2078 NOTE: This work is inspired by the anntecedents of transcTheory.MCLAURIN :
2079
2080 (diff(0) = f) /\
2081 (!m t. m < n /\ &0 <= t /\ t <= h ==>
2082 (diff(m) diffl diff(SUC m)(t)) (t))
2083
2084 When eliminating the SELECT operator, by DIFF_UNIQ we have:
2085
2086 ((diffn m f) diffl y) (x) /\
2087 ((diffn m f) diffl (diffn (SUC m) t)) (x)) ==> y = diffn (SUC m) t)
2088
2089 NOTE: It's named "diffn" instead of “diff” because: 1) “diff ”is already a
2090 constant defined in polyTheory; 2) “diff” looks like a common symbol used in
2091 unknown user code as either variables or user-defined constants.
2092 *)
2093Definition diffn_def :
2094 (diffn 0 f x = f x) /\
2095 (diffn (SUC m) f x = @y. ((diffn m f) diffl y)(x))
2096End
2097
2098(* NOTE: It's recommended for users to copy this overload to their theories:
2099Overload D[local] = “diffn”
2100 *)
2101Overload diff1 = “diffn 1”
2102
2103Theorem diffn_thm :
2104 !f. (!m t. ?x. (diffn m f diffl x) t) ==>
2105 (diffn 0 f = f) /\
2106 (!m t. ((diffn m f) diffl (diffn (SUC m) f t))(t))
2107Proof
2108 rw [diffn_def, FUN_EQ_THM]
2109 >> SELECT_ELIM_TAC >> simp []
2110QED
2111
2112Theorem diffn_0[simp] :
2113 diffn 0 f = f
2114Proof
2115 rw [FUN_EQ_THM, diffn_def]
2116QED
2117
2118Theorem diffn_1 :
2119 !f x. diffn 1 f x = @y. (f diffl y) x
2120Proof
2121 EVAL_TAC >> simp []
2122QED
2123
2124(* |- !f x. diff1 f x = @y. (f diffl y) x *)
2125Theorem diff1_def = diffn_1
2126
2127(* |- !f x. diff1 f x = @y. (f has_vector_derivative y) (at x) *)
2128Theorem diff1_alt =
2129 diffn_1 |> REWRITE_RULE [diffl_has_vector_derivative]
2130
2131Theorem diffl_imp_diff1 :
2132 !f x y. (f diffl y) x ==> (diff1 f x = y)
2133Proof
2134 RW_TAC std_ss [diff1_def]
2135 >> SELECT_ELIM_TAC
2136 >> CONJ_TAC >- (Q.EXISTS_TAC ‘y’ >> art [])
2137 >> Q.X_GEN_TAC ‘z’ >> DISCH_TAC
2138 >> PROVE_TAC [DIFF_UNIQ]
2139QED
2140
2141(* |- !f x y. (f has_vector_derivative y) (at x) ==> diff1 f x = y *)
2142Theorem has_vector_derivative_imp_diff1 =
2143 REWRITE_RULE [diffl_has_vector_derivative] diffl_imp_diff1
2144
2145Theorem SELECT_EQ_THM[local] :
2146 !P Q. (!x. P x <=> Q x) ==> ((@x. P x) = (@x. Q x))
2147Proof
2148 rw []
2149QED
2150
2151Theorem diffn_cong :
2152 !n f g x. (!x. f x = g x) ==> (diffn n f x = diffn n g x)
2153Proof
2154 Induct_on ‘n’ >- gs []
2155 >> rw [diffn_def]
2156 >> HO_MATCH_MP_TAC SELECT_EQ_THM
2157 >> rw [] >> EQ_TAC >> rw []
2158 >> METIS_TAC []
2159QED
2160
2161Definition higher_differentiable_def :
2162 (higher_differentiable 0 f x <=> T) /\
2163 (higher_differentiable (SUC m) f x <=> (?y. (diffn m f diffl y) x) /\
2164 higher_differentiable m f x)
2165End
2166
2167Theorem higher_differentiable_thm :
2168 !f. (diffn 0 f = f) /\
2169 (!m t. (higher_differentiable (SUC m) f t ==>
2170 (diffn m f diffl (diffn (SUC m) f t)) t))
2171Proof
2172 rw [higher_differentiable_def, diffn_def, FUN_EQ_THM]
2173 >> SELECT_ELIM_TAC >> simp []
2174 >> qexists ‘y’ >> simp []
2175QED
2176
2177Theorem higher_differentiable_mono :
2178 !f n m t. m <= n /\ higher_differentiable n f t ==>
2179 higher_differentiable m f t
2180Proof
2181 rpt STRIP_TAC
2182 >> Cases_on ‘m = n’ >- fs []
2183 >> Induct_on ‘n’ >- rw [higher_differentiable_def]
2184 >> rw []
2185 >> Cases_on ‘m’
2186 >- simp [higher_differentiable_def]
2187 >> ‘n < SUC n’ by rw [LESS_SUC_REFL]
2188 >> ‘n < SUC n ==> higher_differentiable (SUC n) f t ==>
2189 higher_differentiable n f t’ by METIS_TAC [higher_differentiable_def]
2190 >> rw []
2191 >> Cases_on ‘SUC n' = n’ >- (rw [])
2192 >> Suff ‘SUC n' < n’ >- (fs [])
2193 >> MATCH_MP_TAC LESS_NOT_SUC >> simp []
2194QED
2195
2196Theorem higher_differentiable_1:
2197 !f x. higher_differentiable 1 f x <=> ?y. (f diffl y) x
2198Proof
2199 rpt STRIP_TAC
2200 >> MP_TAC ( Q.SPECL [‘0’, ‘f’, ‘x’] (cj 2 higher_differentiable_def))
2201 >> simp [cj 1 higher_differentiable_def]
2202QED
2203
2204Theorem higher_differentiable_imp_continuous:
2205 !f x. higher_differentiable 1 f x ==> f continuous (at x)
2206Proof
2207 rw [higher_differentiable_1, GSYM contl_eq_continuous_at]
2208 >> METIS_TAC [DIFF_CONT]
2209QED
2210
2211Theorem higher_differentiable_imp_continuous' :
2212 !n f x. higher_differentiable n f x /\ 1 <= n ==> f continuous (at x)
2213Proof
2214 rpt STRIP_TAC
2215 >> MATCH_MP_TAC higher_differentiable_imp_continuous
2216 >> MATCH_MP_TAC higher_differentiable_mono
2217 >> Q.EXISTS_TAC ‘n’ >> art []
2218QED
2219
2220Theorem higher_differentiable_1_eq_differentiable:
2221 !f x. higher_differentiable 1 f x <=> derivative$differentiable f (at x)
2222Proof
2223 rpt GEN_TAC
2224 >> fs [higher_differentiable_1, diffl_has_vector_derivative,
2225 GSYM differentiable_alt, differentiable_has_vector_derivative]
2226QED
2227
2228Theorem higher_differentiable_1_eq_differentiable_on:
2229 !f. (!x. higher_differentiable 1 f x) <=> f differentiable_on univ(:real)
2230Proof
2231 rw [higher_differentiable_1_eq_differentiable, differentiable_on]
2232 >> METIS_TAC [netsTheory.WITHIN_UNIV]
2233QED
2234
2235Theorem higher_differentiable_1_eq_differentiable_on':
2236 !f s. open s ==>
2237 ((!x. x IN s ==> higher_differentiable 1 f x) <=>
2238 f differentiable_on s)
2239Proof
2240 rw [higher_differentiable_1_eq_differentiable, differentiable_on]
2241 >> METIS_TAC [DIFFERENTIABLE_WITHIN_OPEN]
2242QED
2243
2244Theorem diffn_SUC :
2245 !m f. (!x. higher_differentiable (SUC m) f x) ==>
2246 (diffn m (diffn 1 f) = diffn (SUC m) f)
2247Proof
2248 Induct_on ‘m’ >- gs []
2249 >> rw [diffn_def, FUN_EQ_THM]
2250 >> HO_MATCH_MP_TAC SELECT_EQ_THM
2251 >> rw [] >> EQ_TAC >> rw []
2252 >> (Know ‘!x. higher_differentiable (SUC m) f x’
2253 >- (Q.X_GEN_TAC ‘z’ \\
2254 MATCH_MP_TAC higher_differentiable_mono \\
2255 qexists ‘SUC (SUC m)’ \\
2256 simp [LESS_EQ_SUC_REFL]) \\
2257 Q.PAT_X_ASSUM ‘!f. _ ==> _’ (STRIP_ASSUME_TAC o Q.SPEC ‘f’) \\
2258 DISCH_THEN (fs o wrap))
2259QED
2260
2261Theorem diffn_SUC' :
2262 !m f. (!x. higher_differentiable (SUC m) f x) ==>
2263 (diffn 1 (diffn m f) = diffn (SUC m) f)
2264Proof
2265 rpt STRIP_TAC
2266 >> ‘1 = SUC 0’ by simp[] >> POP_ORW
2267 >> rw [diffn_def, FUN_EQ_THM]
2268QED
2269
2270Theorem higher_differentiable_imp_11 :
2271 !n f x. 1 < n /\ higher_differentiable n f x ==>
2272 higher_differentiable 1 (diffn 1 f) x
2273Proof
2274 Induct_on ‘n’ >- gs []
2275 >> rw [higher_differentiable_def]
2276 >> FIRST_X_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [‘f’, ‘x’])
2277 >> fs [LESS_THM] >> gs []
2278 >> ‘1 = SUC 0’ by simp []
2279 >> POP_ORW
2280 >> rw [higher_differentiable_def] >> qexists ‘y’ >> simp []
2281QED
2282
2283Theorem higher_differentiable_imp_n1 :
2284 !n f. (!x. higher_differentiable (SUC n) f x) ==>
2285 (!x. higher_differentiable n (diffn 1 f) x)
2286Proof
2287 STRIP_TAC
2288 >> Induct_on ‘n’ >> fs [higher_differentiable_def]
2289 >> rw []
2290 >> MP_TAC (Q.SPECL [‘n’, ‘f’] diffn_SUC)
2291 >> impl_tac
2292 >- (rw [higher_differentiable_def] \\
2293 POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2294 qexists ‘y'’ >> simp [])
2295 >> Rewr
2296 >> Know ‘!x. ?y. (diffn n f diffl y) x /\ higher_differentiable n f x’
2297 >- (rw [] \\
2298 POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2299 qexists ‘y'’ >> simp [])
2300 >> DISCH_THEN (fs o wrap)
2301QED
2302
2303Theorem higher_differentiable_imp_1n :
2304 !n f. (!x. higher_differentiable (SUC n) f x) ==>
2305 (!x. higher_differentiable 1 (diffn n f) x)
2306Proof
2307 STRIP_TAC
2308 >> Induct_on ‘n’
2309 >- (‘1 = SUC 0’ by simp [] >> POP_ORW >> fs [])
2310 >> rw []
2311 >> MP_TAC (Q.SPECL [‘n’, ‘f’] diffn_SUC)
2312 >> impl_tac >- (rw [] \\
2313 MATCH_MP_TAC higher_differentiable_mono \\
2314 qexists ‘SUC (SUC n)’ >> fs [])
2315 >> DISCH_THEN (rw o wrap o SYM)
2316 >> Q.PAT_X_ASSUM ‘!f. (!x. _) ==> _’ (STRIP_ASSUME_TAC o Q.SPEC ‘diffn 1 f’)
2317 >> Know ‘!x. higher_differentiable (SUC n) (diffn 1 f) x’
2318 >- (rw [] \\
2319 MATCH_MP_TAC higher_differentiable_imp_n1 >> fs [])
2320 >> gs []
2321QED
2322
2323Theorem higher_differentiable_imp_mn :
2324 !m n f. (!x. higher_differentiable (m + n) f x) ==>
2325 (!x. higher_differentiable m (diffn n f) x)
2326Proof
2327 Q.X_GEN_TAC ‘m’
2328 >> Induct_on ‘n’ >- simp []
2329 >> rpt STRIP_TAC
2330 >> Know ‘diffn (SUC n) f = diffn n (diff1 f)’
2331 >- (SYM_TAC >> MATCH_MP_TAC diffn_SUC \\
2332 Q.X_GEN_TAC ‘x’ \\
2333 MATCH_MP_TAC higher_differentiable_mono \\
2334 qexists ‘m + SUC n’ >> simp [])
2335 >> Rewr'
2336 >> FIRST_X_ASSUM MATCH_MP_TAC
2337 >> MATCH_MP_TAC higher_differentiable_imp_n1
2338 >> ‘SUC (m + n) = m + SUC n’ by ARITH_TAC
2339 >> simp []
2340QED
2341
2342(* NOTE: cf. diffn_add (for additivity of diff1) *)
2343Theorem diffn_ADD :
2344 !m n f. (!x. higher_differentiable (m + n) f x) ==>
2345 (diffn m (diffn n f) = diffn (m + n) f)
2346Proof
2347 Q.X_GEN_TAC ‘m’
2348 >> Induct_on ‘n’ >- simp []
2349 >> rpt STRIP_TAC
2350 >> Know ‘diffn (SUC n) f = diffn n (diff1 f)’
2351 >- (SYM_TAC >> MATCH_MP_TAC diffn_SUC \\
2352 Q.X_GEN_TAC ‘x’ \\
2353 MATCH_MP_TAC higher_differentiable_mono \\
2354 qexists ‘m + SUC n’ >> simp [])
2355 >> Rewr'
2356 >> ‘m + SUC n = SUC (m + n)’ by simp [] >> POP_ORW
2357 >> Know ‘diffn (SUC (m + n)) f = diffn (m + n) (diff1 f)’
2358 >- (SYM_TAC >> MATCH_MP_TAC diffn_SUC \\
2359 simp [ARITH_PROVE “SUC (m + n) = m + SUC n”])
2360 >> Rewr'
2361 >> FIRST_X_ASSUM MATCH_MP_TAC
2362 >> MATCH_MP_TAC higher_differentiable_imp_n1
2363 >> simp [ARITH_PROVE “SUC (m + n) = m + SUC n”]
2364QED
2365
2366Theorem diffn_chain :
2367 !f g. (!t. higher_differentiable 1 f t) /\ (!t. higher_differentiable 1 g t) ==>
2368 (diffn 1 (λx. f (g x)) = λx. diffn 1 f (g x) * diffn 1 g x)
2369Proof
2370 rpt STRIP_TAC
2371 >> ‘1 = SUC 0’ by simp [] >> POP_ORW
2372 >> fs [diffn_def, higher_differentiable_1, FUN_EQ_THM] >> rw []
2373 >> SELECT_ELIM_TAC
2374 >> STRONG_CONJ_TAC
2375 >- (POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2376 FIRST_X_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘g (x :real)’) \\
2377 rename1 ‘(f diffl z) (g x)’ \\
2378 qexists ‘z * y’ \\
2379 MATCH_MP_TAC DIFF_CHAIN >> simp [])
2380 >> DISCH_THEN (Q.X_CHOOSE_THEN ‘y’ ASSUME_TAC)
2381 >> Q.X_GEN_TAC ‘z’
2382 >> DISCH_TAC
2383 >> ‘y = z’ by METIS_TAC [DIFF_UNIQ]
2384 >> NTAC 2 (SELECT_ELIM_TAC >> rw [] >> fs [])
2385 >> rename1 ‘y = l * m’
2386 >> MP_TAC (Q.SPECL [‘f’, ‘g’, ‘l’, ‘m’, ‘(x :real)’] DIFF_CHAIN)
2387 >> simp []
2388 >> METIS_TAC [DIFF_UNIQ]
2389QED
2390
2391Theorem diffn_const :
2392 !k. diffn 1 (λx. k) = λx. 0
2393Proof
2394 rw [diffn_1, FUN_EQ_THM]
2395 >> SELECT_ELIM_TAC >> rw []
2396 >- (qexists ‘0’ >> irule DIFF_CONST)
2397 >> MP_TAC (Q.SPECL [‘k’, ‘x’] DIFF_CONST)
2398 >> METIS_TAC [DIFF_UNIQ]
2399QED
2400
2401Theorem diffn_cmul :
2402 !f c. (!x. higher_differentiable 1 f x) ==>
2403 (diffn 1 (λx. c * f x) = λx. c * diffn 1 f x)
2404Proof
2405 rw [diffn_1, higher_differentiable_1, FUN_EQ_THM]
2406 >> SELECT_ELIM_TAC >> rw []
2407 >- (POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2408 qexists ‘c * y’ >> METIS_TAC [DIFF_CMUL])
2409 >> SELECT_ELIM_TAC >> rw [] >> fs []
2410 >> rename1 ‘y = c * z’
2411 >> MP_TAC (Q.SPECL [‘f’, ‘c’, ‘z’, ‘x’] DIFF_CMUL)
2412 >> simp []
2413 >> METIS_TAC [DIFF_UNIQ]
2414QED
2415
2416(* |- !f c x.
2417 (!x. higher_differentiable 1 f x) ==>
2418 diff1 (\x. c * f x) x = c * diff1 f x
2419 *)
2420Theorem diff1_cmul = diffn_cmul |> SRULE [FUN_EQ_THM, PULL_FORALL]
2421
2422Theorem diffl_imp_diffn :
2423 !m f x y. (diffn m f diffl y) x ==> (diffn (SUC m) f x = y)
2424Proof
2425 rw [diffn_def]
2426 >> SELECT_ELIM_TAC >> rw []
2427 >- (qexists ‘y’ >> fs [])
2428 >> irule DIFF_UNIQ
2429 >> qexistsl [‘diffn m f’, ‘x’] >> fs []
2430QED
2431
2432Theorem diffn_imp_diffl :
2433 !f x y n. higher_differentiable (SUC n) f x /\ (diffn (SUC n) f x = y) ==>
2434 (diffn n f diffl y) x
2435Proof
2436 rpt STRIP_TAC
2437 >> MP_TAC (Q.SPECL [‘f’] higher_differentiable_thm)
2438 >> rw []
2439QED
2440
2441Theorem diff1_imp_diffl :
2442 !f x y. higher_differentiable 1 f x /\ (diff1 f x = y) ==> (f diffl y) x
2443Proof
2444 rpt STRIP_TAC
2445 >> ‘f = diffn 0 f’ by simp [] >> POP_ORW
2446 >> MATCH_MP_TAC diffn_imp_diffl >> simp []
2447QED
2448
2449Theorem diffn_mul :
2450 !f g. (!t. higher_differentiable 1 f t) /\ (!t. higher_differentiable 1 g t) ==>
2451 (diffn 1 (λx. f x * g x) = (λx. diffn 1 f x * g x + diffn 1 g x * f x))
2452Proof
2453 rw [FUN_EQ_THM, diffn_1]
2454 >> SELECT_ELIM_TAC
2455 >> STRONG_CONJ_TAC
2456 >- (fs [higher_differentiable_1] \\
2457 POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2458 FIRST_X_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2459 rename1 ‘(f diffl l) x’ >> rename1 ‘(g diffl m) x’ \\
2460 qexists ‘l * g x + m * f x’ \\
2461 MATCH_MP_TAC DIFF_MUL >> simp [])
2462 >> DISCH_THEN (Q.X_CHOOSE_THEN ‘y’ ASSUME_TAC)
2463 >> Q.X_GEN_TAC ‘z’
2464 >> DISCH_TAC
2465 >> ‘y = z’ by METIS_TAC [DIFF_UNIQ]
2466 >> SELECT_ELIM_TAC >> rw []
2467 >- (Q.PAT_X_ASSUM ‘!t. higher_differentiable 1 f t’
2468 (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2469 fs [higher_differentiable_1] \\
2470 qexists ‘y'’ >> fs [])
2471 >> SELECT_ELIM_TAC >> rw []
2472 >- (Q.PAT_X_ASSUM ‘!t. higher_differentiable 1 g t’
2473 (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2474 fs [higher_differentiable_1] \\
2475 qexists ‘y'’ >> fs [])
2476 >> qmatch_abbrev_tac ‘y = l * g x + m * f x’
2477 >> MP_TAC (Q.SPECL [‘f’, ‘g’, ‘l’, ‘m’, ‘x’] DIFF_MUL) >> rw []
2478 >> METIS_TAC [DIFF_UNIQ]
2479QED
2480
2481Theorem diffn_add :
2482 !f g. (!t. higher_differentiable 1 f t) /\ (!t. higher_differentiable 1 g t) ==>
2483 (diffn 1 (λx. f x + g x) = (λx. diffn 1 f x + diffn 1 g x))
2484Proof
2485 rw [FUN_EQ_THM, diffn_1]
2486 >> SELECT_ELIM_TAC
2487 >> STRONG_CONJ_TAC
2488 >- (fs [higher_differentiable_1] \\
2489 POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2490 FIRST_X_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2491 rename1 ‘(f diffl l) x’ >> rename1 ‘(g diffl m) x’ \\
2492 qexists ‘l + m’ \\
2493 MATCH_MP_TAC DIFF_ADD >> simp [])
2494 >> DISCH_THEN (Q.X_CHOOSE_THEN ‘y’ ASSUME_TAC)
2495 >> Q.X_GEN_TAC ‘z’
2496 >> DISCH_TAC
2497 >> ‘y = z’ by METIS_TAC [DIFF_UNIQ]
2498 >> SELECT_ELIM_TAC >> rw []
2499 >- (Q.PAT_X_ASSUM ‘!t. higher_differentiable 1 f t’
2500 (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2501 fs [higher_differentiable_1] \\
2502 qexists ‘y'’ >> fs [])
2503 >> SELECT_ELIM_TAC >> rw []
2504 >- (Q.PAT_X_ASSUM ‘!t. higher_differentiable 1 g t’
2505 (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2506 fs [higher_differentiable_1] \\
2507 qexists ‘y'’ >> fs [])
2508 >> qmatch_abbrev_tac ‘y = l + m’
2509 >> MP_TAC (Q.SPECL [‘f’, ‘g’, ‘l’, ‘m’, ‘x’] DIFF_ADD) >> rw []
2510 >> METIS_TAC [DIFF_UNIQ]
2511QED
2512
2513Theorem diffn_sub :
2514 !f g. (!t. higher_differentiable 1 f t) /\ (!t. higher_differentiable 1 g t) ==>
2515 (diffn 1 (λx. f x - g x) = (λx. diffn 1 f x - diffn 1 g x))
2516Proof
2517 rw [FUN_EQ_THM, diffn_1]
2518 >> SELECT_ELIM_TAC
2519 >> STRONG_CONJ_TAC
2520 >- (fs [higher_differentiable_1] \\
2521 POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2522 FIRST_X_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2523 rename1 ‘(f diffl l) x’ >> rename1 ‘(g diffl m) x’ \\
2524 qexists ‘l - m’ \\
2525 MATCH_MP_TAC DIFF_SUB >> simp [])
2526 >> DISCH_THEN (Q.X_CHOOSE_THEN ‘y’ ASSUME_TAC)
2527 >> Q.X_GEN_TAC ‘z’
2528 >> DISCH_TAC
2529 >> ‘y = z’ by METIS_TAC [DIFF_UNIQ]
2530 >> SELECT_ELIM_TAC >> rw []
2531 >- (Q.PAT_X_ASSUM ‘!t. higher_differentiable 1 f t’
2532 (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2533 fs [higher_differentiable_1] \\
2534 qexists ‘y'’ >> fs [])
2535 >> SELECT_ELIM_TAC >> rw []
2536 >- (Q.PAT_X_ASSUM ‘!t. higher_differentiable 1 g t’
2537 (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2538 fs [higher_differentiable_1] \\
2539 qexists ‘y'’ >> fs [])
2540 >> qmatch_abbrev_tac ‘y = l - m’
2541 >> MP_TAC (Q.SPECL [‘f’, ‘g’, ‘l’, ‘m’, ‘x’] DIFF_SUB) >> rw []
2542 >> METIS_TAC [DIFF_UNIQ]
2543QED
2544
2545Theorem diff1_add :
2546 !f g x. (!t. higher_differentiable 1 f t) /\
2547 (!t. higher_differentiable 1 g t) ==>
2548 (diff1 (\t. f t + g t) x = diff1 f x + diff1 g x)
2549Proof
2550 rpt STRIP_TAC
2551 >> MP_TAC (Q.SPECL [‘f’, ‘g’] diffn_add) >> rw [FUN_EQ_THM]
2552QED
2553
2554Theorem diff1_sub :
2555 !f g x. (!t. higher_differentiable 1 f t) /\
2556 (!t. higher_differentiable 1 g t) ==>
2557 (diff1 (\t. f t - g t) x = diff1 f x - diff1 g x)
2558Proof
2559 rpt STRIP_TAC
2560 >> MP_TAC (Q.SPECL [‘f’, ‘g’] diffn_sub) >> rw [FUN_EQ_THM]
2561QED
2562
2563Theorem diff1_mul :
2564 !f g x. (!t. higher_differentiable 1 f t) /\
2565 (!t. higher_differentiable 1 g t) ==>
2566 (diffn 1 (\t. f t * g t) x = diffn 1 f x * g x + f x * diffn 1 g x)
2567Proof
2568 rpt STRIP_TAC
2569 >> ‘f x * diff1 g x = diff1 g x * f x’ by simp [Once REAL_MUL_COMM]
2570 >> POP_ORW
2571 >> MP_TAC (Q.SPECL [‘f’, ‘g’] diffn_mul) >> rw [FUN_EQ_THM]
2572QED
2573
2574val higher_differentiable_n_imp_1_tactic =
2575 rw []
2576 >- (Q.PAT_X_ASSUM ‘!x. higher_differentiable (SUC n') f x’
2577 (STRIP_ASSUME_TAC o Q.SPEC ‘t’) \\
2578 MATCH_MP_TAC higher_differentiable_mono \\
2579 qexists ‘SUC n'’ >> simp []) \\
2580 Q.PAT_X_ASSUM ‘!x. higher_differentiable (SUC n') g x’
2581 (STRIP_ASSUME_TAC o Q.SPEC ‘t’) \\
2582 MATCH_MP_TAC higher_differentiable_mono \\
2583 qexists ‘SUC n'’ >> simp [];
2584
2585Theorem higher_differentiable_add :
2586 !f g n. (!x. higher_differentiable n f x) /\
2587 (!x. higher_differentiable n g x) ==>
2588 (!x. higher_differentiable n (λx. f x + g x) x)
2589Proof
2590 Induct_on ‘n’ >- gs [higher_differentiable_def]
2591 >> rw [higher_differentiable_def, FORALL_AND_THM]
2592 >> Cases_on ‘n’
2593 >- (fs [diffn_0] \\
2594 Q.PAT_X_ASSUM ‘!x. ?y. (g diffl y) x’ (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2595 Q.PAT_X_ASSUM ‘!x. ?y. (f diffl y) (x :real)’ (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2596 rename1 ‘(f diffl l) x’ >> rename1 ‘(g diffl m) x’ \\
2597 qexists ‘l + m’ \\
2598 MATCH_MP_TAC DIFF_ADD >> simp [])
2599 >> gs [GSYM diffn_SUC]
2600 >> MP_TAC (Q.SPECL [‘f’, ‘g’] diffn_add)
2601 >> impl_tac >- higher_differentiable_n_imp_1_tactic >> Rewr
2602 >> Q.ABBREV_TAC ‘df = diffn 1 f’
2603 >> Q.ABBREV_TAC ‘dg = diffn 1 g’
2604 >> Q.PAT_X_ASSUM ‘!f g. _’ (STRIP_ASSUME_TAC o Q.SPECL [‘df’, ‘dg’])
2605 >> rename1 ‘?y. (diffn m (\x. df x + dg x) diffl y) x’
2606 >> Know ‘(!x. higher_differentiable (SUC m) df x) /\
2607 (!x. higher_differentiable (SUC m) dg x)’
2608 >- (rw [Abbr ‘df’, Abbr ‘dg’, higher_differentiable_def] \\
2609 MATCH_MP_TAC higher_differentiable_imp_n1 >> gs [])
2610 >> DISCH_THEN (fs o wrap)
2611 >> fs [higher_differentiable_def]
2612QED
2613
2614Theorem higher_differentiable_sub :
2615 !f g n. (!x. higher_differentiable n f x) /\
2616 (!x. higher_differentiable n g x) ==>
2617 (!x. higher_differentiable n (λx. f x - g x) x)
2618Proof
2619 Induct_on ‘n’ >- gs [higher_differentiable_def]
2620 >> rw [higher_differentiable_def, FORALL_AND_THM]
2621 >> Cases_on ‘n’
2622 >- (fs [diffn_0] \\
2623 Q.PAT_X_ASSUM ‘!x. ?y. (g diffl y) x’ (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2624 Q.PAT_X_ASSUM ‘!x. ?y. (f diffl y) (x :real)’ (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2625 rename1 ‘(f diffl l) x’ \\
2626 rename1 ‘(g diffl m) x’ \\
2627 qexists ‘l - m’ \\
2628 MATCH_MP_TAC DIFF_SUB >> simp [])
2629 >> gs [GSYM diffn_SUC]
2630 >> MP_TAC (Q.SPECL [‘f’, ‘g’] diffn_sub)
2631 >> impl_tac >- higher_differentiable_n_imp_1_tactic >> Rewr
2632 >> Q.ABBREV_TAC ‘df = diffn 1 f’
2633 >> Q.ABBREV_TAC ‘dg = diffn 1 g’
2634 >> Q.PAT_X_ASSUM ‘!f g. _’ (STRIP_ASSUME_TAC o Q.SPECL [‘df’, ‘dg’])
2635 >> rename1 ‘?y. (diffn m (\x. df x - dg x) diffl y) x’
2636 >> Know ‘(!x. higher_differentiable (SUC m) df x) /\
2637 (!x. higher_differentiable (SUC m) dg x)’
2638 >- (rw [Abbr ‘df’, Abbr ‘dg’, higher_differentiable_def] \\
2639 MATCH_MP_TAC higher_differentiable_imp_n1 >> gs [])
2640 >> DISCH_THEN (fs o wrap)
2641 >> fs [higher_differentiable_def]
2642QED
2643
2644Theorem higher_differentiable_mul :
2645 !f g n. (!x. higher_differentiable n f x) /\
2646 (!x. higher_differentiable n g x) ==>
2647 (!x. higher_differentiable n (λx. f x * g x) x)
2648Proof
2649 Induct_on ‘n’ >- (gs [higher_differentiable_def])
2650 >> rw [higher_differentiable_def, FORALL_AND_THM]
2651 >> Cases_on ‘n’
2652 >- (fs [diffn_0] \\
2653 Q.PAT_X_ASSUM ‘!x. ?y. (g diffl y) x’ (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2654 Q.PAT_X_ASSUM ‘!x. ?y. (f diffl y) (x :real)’ (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2655 rename1 ‘(f diffl l) x’ >> rename1 ‘(g diffl m) x’ \\
2656 qexists ‘l * g x + m * f x’ \\
2657 MATCH_MP_TAC DIFF_MUL >> simp [])
2658 >> gs [GSYM diffn_SUC]
2659 >> MP_TAC (Q.SPECL [‘f’, ‘g’] diffn_mul)
2660 >> impl_tac >- higher_differentiable_n_imp_1_tactic >> Rewr
2661 >> Q.ABBREV_TAC ‘df = diffn 1 f’
2662 >> Q.ABBREV_TAC ‘dg = diffn 1 g’
2663 >> rename1 ‘!x. ?y. (diffn m df diffl y) x’
2664 >> Know ‘!x. higher_differentiable (SUC m) (λx. df x * g x) x’
2665 >- (Q.PAT_X_ASSUM ‘!f g. _’ (MP_TAC o Q.SPECL [‘df’, ‘g’]) \\
2666 Know ‘(!x. higher_differentiable (SUC m) df x) /\
2667 (!x. higher_differentiable (SUC m) g x)’
2668 >- (rw [Abbr ‘df’, higher_differentiable_def] \\
2669 MATCH_MP_TAC higher_differentiable_imp_n1 >> gs []) >> Rewr)
2670 >> DISCH_TAC
2671 >> Know ‘!x. higher_differentiable (SUC m) (λx. f x * dg x) x’
2672 >- (Q.PAT_X_ASSUM ‘!f g. _’ (MP_TAC o Q.SPECL [‘f’, ‘dg’]) \\
2673 Know ‘(!x. higher_differentiable (SUC m) f x) /\
2674 (!x. higher_differentiable (SUC m) dg x)’
2675 >- (rw [Abbr ‘dg’, higher_differentiable_def] \\
2676 MATCH_MP_TAC higher_differentiable_imp_n1 >> gs []) >> Rewr)
2677 >> DISCH_TAC
2678 >> MP_TAC (Q.SPECL [‘λx. df x * g x’, ‘λx. dg x * f x’, ‘SUC m’]
2679 higher_differentiable_add)
2680 >> Suff ‘(!x. higher_differentiable (SUC m) (λx. df x * g x) x) /\
2681 (!x. higher_differentiable (SUC m) (λx. dg x * f x) x)’
2682 >- (rw [higher_differentiable_def])
2683 >> rw [Abbr ‘df’, Abbr ‘dg’]
2684QED
2685
2686Theorem higher_differentiable_chain :
2687 !n f g. (!x. higher_differentiable n f x) /\
2688 (!x. higher_differentiable n g x) ==>
2689 (!x. higher_differentiable n (λx. f (g x)) x)
2690Proof
2691 Induct_on ‘n’ >- gs [higher_differentiable_def]
2692 >> rw [higher_differentiable_def, FORALL_AND_THM]
2693 >> Cases_on ‘n’
2694 >- (fs [diffn_0] \\
2695 Q.PAT_X_ASSUM ‘!x. ?y. (g diffl y) x’ (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2696 Q.PAT_X_ASSUM ‘!x. ?y. (f diffl y) (x :real)’
2697 (STRIP_ASSUME_TAC o Q.SPEC ‘g (x :real)’) \\
2698 rename1 ‘(f diffl z) (g x)’ \\
2699 qexists ‘z * y’ \\
2700 MATCH_MP_TAC DIFF_CHAIN >> simp [])
2701 >> gs [GSYM diffn_SUC]
2702 >> rename1 ‘?y. (diffn m (diffn 1 (\x. f (g x))) diffl y) x’
2703 >> Know ‘diffn 1 (λx. f (g x)) = λx. diffn 1 f (g x) * diffn 1 g x’
2704 >- (MATCH_MP_TAC diffn_chain >> rw [] \\
2705 Q.PAT_X_ASSUM ‘!x. higher_differentiable (SUC m) f x’
2706 (STRIP_ASSUME_TAC o Q.SPEC ‘t’) \\
2707 MATCH_MP_TAC higher_differentiable_mono \\
2708 qexists ‘SUC m’ >> simp [])
2709 >> Rewr
2710 >> Q.ABBREV_TAC ‘df = diffn 1 f’
2711 >> Q.ABBREV_TAC ‘dg = diffn 1 g’
2712 >> Q.ABBREV_TAC ‘dfg = λx. df (g x)’ >> simp []
2713 >> MP_TAC (Q.SPECL [‘dfg’, ‘dg’, ‘SUC m’] higher_differentiable_mul)
2714 >> impl_tac
2715 >- (rw [Abbr ‘dfg’, Abbr ‘dg’, higher_differentiable_def] \\
2716 Q.PAT_X_ASSUM ‘!f g. _’ (MP_TAC o Q.SPECL [‘df’, ‘g’]) \\
2717 simp [] \\
2718 Suff ‘(!x. higher_differentiable (SUC m) df x)’
2719 >- (rw [higher_differentiable_def]) \\
2720 rw [Abbr ‘df’, higher_differentiable_def] \\
2721 MATCH_MP_TAC higher_differentiable_imp_n1 >> gs [])
2722 >> rw [higher_differentiable_def]
2723QED
2724
2725Theorem higher_differentiable_compose :
2726 !n f g. (!x. higher_differentiable n f x) /\
2727 (!x. higher_differentiable n g x) ==>
2728 (!x. higher_differentiable n (f o g) x)
2729Proof
2730 rw [o_DEF]
2731 >> MATCH_MP_TAC higher_differentiable_chain >> art []
2732QED
2733
2734Theorem diffn_linear :
2735 !a b. diffn 1 (λx. a * x + b) = λx. a
2736Proof
2737 rw [diffn_1, FUN_EQ_THM]
2738 >> SELECT_ELIM_TAC >> rw []
2739 >- (qexists ‘a’ \\
2740 MP_TAC (Q.SPECL [‘λx. a * x’, ‘λx. b’, ‘a’, ‘0’, ‘x’] DIFF_ADD) \\
2741 impl_tac
2742 >- (reverse CONJ_TAC >- (METIS_TAC [DIFF_CONST]) \\
2743 MP_TAC (Q.SPECL [‘λx. x’, ‘a’, ‘1’, ‘x’] DIFF_CMUL) \\
2744 impl_tac >- (METIS_TAC [DIFF_X]) >> gs []) \\
2745 gs [])
2746 >> rename1 ‘y = a’
2747 >> MP_TAC (Q.SPECL [‘λx. a * x’, ‘λx. b’, ‘a’, ‘0’, ‘x’] DIFF_ADD)
2748 >> impl_tac
2749 >- (reverse CONJ_TAC >- (METIS_TAC [DIFF_CONST]) \\
2750 MP_TAC (Q.SPECL [‘λx. x’, ‘a’, ‘1’, ‘x’] DIFF_CMUL) \\
2751 impl_tac >- (METIS_TAC [DIFF_X]) >> gs [])
2752 >> rw []
2753 >> METIS_TAC [DIFF_UNIQ]
2754QED
2755
2756(* |- diff1 (\x. x) = (\x. 1) *)
2757Theorem diff1_I = SRULE [] (Q.SPECL [‘1’, ‘0’] diffn_linear)
2758
2759Theorem diffn_linear' :
2760 !a b n. 2 <= n /\ (!t. higher_differentiable n (λx. a * x + b) t) ==>
2761 (diffn n (λx. a * x + b) = λx. 0)
2762Proof
2763 Induct_on ‘n’ >- gs [diffn_def]
2764 >> rw [diffn_def, FUN_EQ_THM]
2765 >> SELECT_ELIM_TAC >> rw []
2766 >- (Cases_on ‘n = 0’ >- (gs [diffn_def]) \\
2767 Cases_on ‘n = 1’ >- (gs [diffn_1, diffn_linear] \\
2768 qexists ‘0’ >> simp [DIFF_CONST]) \\
2769 Q.PAT_X_ASSUM ‘!a b. _’ (MP_TAC o Q.SPECL [‘a’, ‘b’]) \\
2770 Suff ‘2 <= n /\ (!t. higher_differentiable n (λx. a * x + b) t)’
2771 >- (rw [] >> qexists ‘0’ >> simp [DIFF_CONST]) \\
2772 rw [] \\
2773 FIRST_X_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘t’) \\
2774 MATCH_MP_TAC higher_differentiable_mono \\
2775 qexists ‘SUC n’ >> gs [])
2776 >> Cases_on ‘n = 0’ >- (gs [diffn_def])
2777 >> Cases_on ‘n = 1’ >- (gs [diffn_1, diffn_linear] \\
2778 METIS_TAC [DIFF_CONST, DIFF_UNIQ])
2779 >> Q.PAT_X_ASSUM ‘!a b. _’ (MP_TAC o Q.SPECL [‘a’, ‘b’])
2780 >> Suff ‘2 <= n /\ (!t. higher_differentiable n (λx. a * x + b) t)’
2781 >- (rw [] >> gs [] \\
2782 METIS_TAC [DIFF_CONST, DIFF_UNIQ])
2783 >> rw []
2784 >> FIRST_X_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘t’)
2785 >> MATCH_MP_TAC higher_differentiable_mono
2786 >> qexists ‘SUC n’ >> gs []
2787QED
2788
2789Theorem higher_differentiable_sub_linear :
2790 !a k x. higher_differentiable k (λx. a - x) x
2791Proof
2792 STRIP_TAC
2793 >> Induct_on ‘k’ >- gs [higher_differentiable_def]
2794 >> rw [higher_differentiable_def]
2795 >> Know ‘!x. ((λx. a - x) diffl -1) x’
2796 >- (rw [diffl] \\
2797 ‘!h. a - (x + h) - (a - x) = -h’ by REAL_ARITH_TAC >> POP_ORW \\
2798 MP_TAC (Q.SPECL [‘λh. -h / h’, ‘λx. -1’, ‘-1’, ‘0’] LIM_EQUAL) \\
2799 rw [] \\
2800 METIS_TAC [LIM_CONST])
2801 >> DISCH_TAC
2802 >> MP_TAC (Q.SPECL [‘-1’, ‘a’, ‘k’] diffn_linear') >> rw []
2803 >> ‘!x. -x + a = a - x’ by (rw [] >> REAL_ARITH_TAC)
2804 >> POP_ASSUM (fs o wrap)
2805 >> Cases_on ‘k = 0’
2806 >- (qexists ‘-1’ \\
2807 rw [diffl] \\
2808 ‘!h. a - (x + h) - (a - x) = -h’ by REAL_ARITH_TAC \\
2809 POP_ORW \\
2810 MP_TAC (Q.SPECL [‘λh. -h / h’, ‘λx. -1’, ‘-1’, ‘0’] LIM_EQUAL) \\
2811 rw [] \\
2812 METIS_TAC [LIM_CONST])
2813 >> Cases_on ‘k = 1’
2814 >- (qexists ‘0’ >> gs [] \\
2815 MP_TAC (Q.SPECL [‘λx. a’, ‘λx. x’, ‘0’, ‘1’, ‘x’] DIFF_SUB) \\
2816 impl_tac >- (METIS_TAC [DIFF_CONST, DIFF_X]) \\
2817 rw [] \\
2818 Know ‘diffn 1 (λx. a - x) = λx. -1’
2819 >- (rw [FUN_EQ_THM] \\
2820 POP_ASSUM (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2821 ‘1 = SUC 0’ by simp [] >> POP_ORW \\
2822 irule diffl_imp_diffn >> fs [diffn_def]) >> Rewr \\
2823 METIS_TAC [DIFF_CONST])
2824 >> gs []
2825 >> qexists ‘0’
2826 >> METIS_TAC [DIFF_CONST]
2827QED
2828
2829(* |- !k x. higher_differentiable k (\x. -x) x *)
2830Theorem higher_differentiable_ainv =
2831 higher_differentiable_sub_linear |> Q.SPEC ‘0’ |> SRULE []
2832
2833Theorem higher_differentiable_I :
2834 !k x. higher_differentiable k (\x. x) x
2835Proof
2836 rpt GEN_TAC
2837 >> qabbrev_tac ‘f = \x. -(x :real)’
2838 >> ‘(\x. x) = \x. f (f x)’
2839 by rw [FUN_EQ_THM, REAL_NEG_NEG, Abbr ‘f’] >> POP_ORW
2840 >> MATCH_MP_TAC higher_differentiable_chain
2841 >> simp [higher_differentiable_ainv, Abbr ‘f’]
2842QED
2843
2844Theorem pow_neg_1[local] :
2845 -(1 :real) pow 1 = -1
2846Proof
2847 REAL_ARITH_TAC
2848QED
2849
2850Theorem diffn_neg_sub :
2851 !n f a. (!x. higher_differentiable n f x) ==>
2852 (diffn n (λx. f (a - x)) = λx. (-1) pow n * diffn n f (a - x))
2853Proof
2854 Induct_on ‘n’ >- gs [diffn_def]
2855 >> rw [FUN_EQ_THM]
2856 >> Q.ABBREV_TAC ‘g = λx. f (a - x)’
2857 >> MP_TAC (Q.SPECL [‘n’, ‘g’] diffn_SUC')
2858 >> impl_tac
2859 >- (rw [Abbr ‘g’] \\
2860 irule higher_differentiable_chain >> simp [] \\
2861 METIS_TAC [higher_differentiable_sub_linear])
2862 >> DISCH_THEN (rw o wrap o SYM)
2863 >> Q.PAT_X_ASSUM ‘!f a. _’ (STRIP_ASSUME_TAC o Q.SPECL [‘f’, ‘a’])
2864 >> Know ‘!x. higher_differentiable n f x’
2865 >- (rw [] \\
2866 MATCH_MP_TAC higher_differentiable_mono \\
2867 qexists ‘SUC n’ >> gs [])
2868 >> DISCH_THEN (fs o wrap) >> gs []
2869 >> POP_ORW
2870 >> rw [Abbr ‘g’]
2871 >> Know ‘!x. higher_differentiable 1 f x’
2872 >- (rw [] \\
2873 MATCH_MP_TAC higher_differentiable_mono \\
2874 qexists ‘SUC n’ >> fs [])
2875 >> DISCH_TAC
2876 >> Q.ABBREV_TAC ‘g = λx. diffn n f (a - x)’
2877 >> Know ‘!x. higher_differentiable 1 g x’
2878 >- (rw [Abbr ‘g’] \\
2879 irule higher_differentiable_chain >> rw []
2880 >- (METIS_TAC [higher_differentiable_imp_1n]) \\
2881 METIS_TAC [higher_differentiable_sub_linear])
2882 >> DISCH_TAC
2883 >> ASM_SIMP_TAC std_ss [diffn_cmul]
2884 >> ‘-(1 :real) pow SUC n = -1 pow n * -1’ by rw [ADD1, POW_ADD, pow_neg_1]
2885 >> POP_ORW
2886 >> rw [REAL_MUL_COMM, Abbr ‘g’]
2887 >> Q.ABBREV_TAC ‘dfn = diffn n f’
2888 >> MP_TAC (Q.SPECL [‘dfn’, ‘λx. a - x’] diffn_chain)
2889 >> impl_tac >- (rw [Abbr ‘dfn’]
2890 >- (METIS_TAC [higher_differentiable_imp_1n]) \\
2891 METIS_TAC [higher_differentiable_sub_linear])
2892 >> rw []
2893 >> Know ‘diffn 1 (λx. a - x) x = -1’
2894 >- (MP_TAC (Q.SPECL [‘-1’, ‘a’] diffn_linear) \\
2895 ‘!x. a - x = -x + a’ by (rw [] >> REAL_ARITH_TAC) \\
2896 rw [FUN_EQ_THM])
2897 >> Rewr
2898 >> rw [Abbr ‘dfn’, REAL_MUL_COMM]
2899 >> METIS_TAC [diffn_SUC']
2900QED
2901
2902Theorem higher_differentiable_continuous_on :
2903 !m n f. (!x. higher_differentiable n f x) /\ m < n /\ 0 < n ==>
2904 diffn m f continuous_on univ(:real)
2905Proof
2906 Induct_on ‘m’
2907 >- (rw [] \\
2908 ‘1 <= n’ by fs [] \\
2909 MP_TAC (Q.SPECL [‘f’, ‘n’, ‘1’] higher_differentiable_mono) >> fs [] \\
2910 STRIP_TAC \\
2911 MP_TAC (Q.SPECL [‘f’] higher_differentiable_imp_continuous) >> gs [] \\
2912 fs [continuous_at, continuous_on, IN_UNIV])
2913 >> rpt STRIP_TAC
2914 >> Know ‘!x. higher_differentiable (SUC m) f x’
2915 >- (rw [] \\
2916 HO_MATCH_MP_TAC higher_differentiable_mono \\
2917 qexists ‘n’ \\
2918 METIS_TAC [LT_IMP_LE])
2919 >> DISCH_TAC
2920 >> Q.ABBREV_TAC ‘g = diffn 1 f’
2921 >> Know ‘diffn m g = diffn (SUC m) f’
2922 >- (rw [Abbr ‘g’] \\
2923 HO_MATCH_MP_TAC diffn_SUC \\
2924 simp [])
2925 >> DISCH_TAC >> gs []
2926 >> Cases_on ‘m = 0’
2927 >- (rw [diffn_0, Abbr ‘g’, continuous_on_def] \\
2928 MATCH_MP_TAC CONTINUOUS_AT_WITHIN \\
2929 MATCH_MP_TAC higher_differentiable_imp_continuous \\
2930 HO_MATCH_MP_TAC higher_differentiable_imp_11 \\
2931 qexists ‘n’ >> gs [])
2932 >> Cases_on ‘n’ >> fs []
2933 >> Q.PAT_X_ASSUM ‘diffn m g = _’ (rw o wrap o SYM)
2934 >> FIRST_X_ASSUM (MATCH_MP_TAC)
2935 >> qexists ‘n'’ >> rw [Abbr ‘g’]
2936 >> MATCH_MP_TAC higher_differentiable_imp_n1 >> simp []
2937QED
2938
2939Theorem higher_differentiable_0 :
2940 !n x. higher_differentiable n (λx. 0) x
2941Proof
2942 Induct_on ‘n’ >- (gs [higher_differentiable_def])
2943 >> rw [higher_differentiable_def, FORALL_AND_THM]
2944 >> qexists ‘0’ >> rw []
2945 >> Induct_on ‘n’ >- (gs [higher_differentiable_def, DIFF_CONST])
2946 >> rw [GSYM diffn_SUC, diffn_const]
2947 >> ‘!x. higher_differentiable n (λx. 0) x’
2948 by (rw [] >> MATCH_MP_TAC higher_differentiable_mono >> qexists ‘SUC n’ >> gs [])
2949 >> gs [higher_differentiable_def]
2950QED
2951
2952Theorem diffn_const_0 :
2953 !n x. (diffn n (λx. 0) diffl 0) x
2954Proof
2955 Induct_on ‘n’ >> rw [DIFF_CONST]
2956 >> MATCH_MP_TAC diffn_imp_diffl
2957 >> MP_TAC (Q.SPECL [‘SUC (SUC n)’] higher_differentiable_0) >> rw []
2958 >> MP_TAC (Q.SPECL [‘SUC n’] higher_differentiable_0) >> rw []
2959 >> MP_TAC (Q.SPECL [‘n’, ‘λx. 0’] diffl_imp_diffn) >> rw []
2960 >> rw [diffn_def] >> SELECT_ELIM_TAC
2961 >> CONJ_TAC >- (fs [higher_differentiable_def])
2962 >> ‘diffn (SUC n) (λx. 0) = λx. 0’ by METIS_TAC [FUN_EQ_THM, ETA_AX]
2963 >> POP_ORW >> rw []
2964 >> MP_TAC (Q.SPECL [‘0’, ‘x’] DIFF_CONST) >> rw []
2965 >> METIS_TAC [DIFF_UNIQ]
2966QED
2967
2968Theorem higher_differentiable_const :
2969 !n k x. higher_differentiable n (λx. k) x
2970Proof
2971 Induct_on ‘n’ >- (gs [higher_differentiable_def])
2972 >> rw [higher_differentiable_def, FORALL_AND_THM]
2973 >> qexists ‘0’ >> rw []
2974 >> Induct_on ‘n’ >- (gs [higher_differentiable_def, DIFF_CONST])
2975 >> rw [GSYM diffn_SUC, diffn_const]
2976 >> METIS_TAC [diffn_const_0]
2977QED
2978
2979Theorem higher_differentiable_neg_sub :
2980 !a n f.
2981 (!x. higher_differentiable n f x) ==>
2982 !x. higher_differentiable n (λx. f (a - x)) x
2983Proof
2984 Induct_on ‘n’ >- (gs [higher_differentiable_def])
2985 >> rw [FORALL_AND_THM]
2986 >> MATCH_MP_TAC higher_differentiable_chain
2987 >> rw [higher_differentiable_def]
2988 >- (Cases_on ‘n = 0’ >> gs []
2989 >- (qexists ‘-1’ >> rw [diffl] \\
2990 ‘!h. a - (x + h) - (a - x) = -h’ by REAL_ARITH_TAC >> POP_ORW \\
2991 MP_TAC (Q.SPECL [‘λh. -h / h’, ‘λx. -1’, ‘-1’, ‘0’] LIM_EQUAL) \\
2992 rw [] >> METIS_TAC [LIM_CONST]) \\
2993 MP_TAC (Q.SPECL [‘a’, ‘SUC n’] higher_differentiable_sub_linear) >> rw [] \\
2994 fs [higher_differentiable_def, FORALL_AND_THM] \\
2995 Q.PAT_X_ASSUM ‘!x. ?y. (diffn n (λx. a - x) diffl y) x’
2996 (STRIP_ASSUME_TAC o Q.SPEC ‘x’) \\
2997 qexists ‘y’ >> METIS_TAC [])
2998 >> METIS_TAC [higher_differentiable_sub_linear]
2999QED
3000
3001Theorem higher_differentiable_neg :
3002 !n f. (!x. higher_differentiable n f x) ==>
3003 !x. higher_differentiable n (\x. -f x) x
3004Proof
3005 rpt GEN_TAC >> DISCH_TAC
3006 >> qabbrev_tac ‘g = \x. -(x :real)’
3007 >> ‘!x. -f x = g (f x)’ by rw [Abbr ‘g’] >> POP_ORW
3008 >> MATCH_MP_TAC higher_differentiable_chain
3009 >> simp [higher_differentiable_ainv, Abbr ‘g’]
3010QED
3011
3012(* |- !n f.
3013 (!x. higher_differentiable n f x) ==>
3014 !x. higher_differentiable n (\x. f (-x)) x
3015 *)
3016Theorem higher_differentiable_neg' =
3017 higher_differentiable_neg_sub |> Q.SPEC ‘0’ |> SRULE []
3018
3019Theorem higher_differentiable_cmul :
3020 !f c n. (!x. higher_differentiable n f x) ==>
3021 (!x. higher_differentiable n (\x. c * f x) x)
3022Proof
3023 rpt GEN_TAC >> DISCH_TAC
3024 >> HO_MATCH_MP_TAC higher_differentiable_mul
3025 >> simp [higher_differentiable_const]
3026QED
3027
3028Theorem higher_differentiable_cmul_eq :
3029 !f c n. c <> 0 ==>
3030 ((!x. higher_differentiable n (\x. c * f x) x) <=>
3031 (!x. higher_differentiable n f x))
3032Proof
3033 rpt STRIP_TAC
3034 >> reverse EQ_TAC
3035 >- (DISCH_TAC \\
3036 MATCH_MP_TAC higher_differentiable_cmul >> art [])
3037 >> DISCH_TAC
3038 >> qabbrev_tac ‘g = \x. c * f x’
3039 >> MP_TAC (Q.SPECL [‘g’, ‘inv c’, ‘n’] higher_differentiable_cmul) >> art []
3040 >> simp [Abbr ‘g’, REAL_MUL_LINV, SF ETA_ss]
3041QED
3042
3043Theorem higher_differentiable_affine :
3044 !a b n f. (!x. higher_differentiable n f x) ==>
3045 !x. higher_differentiable n (λx. f (a * x + b)) x
3046Proof
3047 rpt GEN_TAC >> DISCH_TAC
3048 >> HO_MATCH_MP_TAC higher_differentiable_chain >> art []
3049 >> HO_MATCH_MP_TAC higher_differentiable_add
3050 >> simp [higher_differentiable_const]
3051 >> HO_MATCH_MP_TAC higher_differentiable_cmul
3052 >> simp [higher_differentiable_I]
3053QED
3054
3055Theorem higher_differentiable_linear :
3056 !a b n x. higher_differentiable n (\x. a * x + b) x
3057Proof
3058 rpt GEN_TAC
3059 >> MP_TAC (Q.SPECL [‘a’, ‘b’, ‘n’, ‘\x. x’] higher_differentiable_affine)
3060 >> rw [higher_differentiable_I]
3061QED
3062
3063Theorem diffn_cmul_general :
3064 !c f n. (!x. higher_differentiable n f x) ==>
3065 !x. diffn n (\t. c * f t) x = c * diffn n f x
3066Proof
3067 NTAC 2 GEN_TAC
3068 >> Induct_on ‘n’ >- rw [diffn_0]
3069 >> rw [diffn_def]
3070 >> Know ‘!x. higher_differentiable n f x’
3071 >- (Q.X_GEN_TAC ‘x’ \\
3072 MATCH_MP_TAC higher_differentiable_mono \\
3073 Q.EXISTS_TAC ‘SUC n’ >> simp [])
3074 >> DISCH_TAC
3075 >> gs []
3076 >> qabbrev_tac ‘g = diffn n f’
3077 >> ‘diffn n (\t. c * f t) = \x. c * g x’ by rw [FUN_EQ_THM]
3078 >> POP_ORW
3079 (* applying higher_differentiable_imp_1n *)
3080 >> Know ‘!x. higher_differentiable 1 g x’
3081 >- (qunabbrev_tac ‘g’ \\
3082 MATCH_MP_TAC higher_differentiable_imp_1n >> art [])
3083 >> DISCH_THEN (MP_TAC o Q.SPEC ‘x’)
3084 >> RW_TAC std_ss [higher_differentiable_1]
3085 >> Know ‘(@y. (g diffl y) x) = y’
3086 >- (SELECT_ELIM_TAC \\
3087 CONJ_TAC >- (Q.EXISTS_TAC ‘y’ >> art []) \\
3088 Q.X_GEN_TAC ‘z’ >> DISCH_TAC \\
3089 MATCH_MP_TAC DIFF_UNIQ \\
3090 qexistsl_tac [‘g’, ‘x’] >> art [])
3091 >> Rewr'
3092 >> MP_TAC (Q.SPECL [‘g’, ‘c’, ‘y’, ‘x’] DIFF_CMUL) >> rw []
3093 >> SELECT_ELIM_TAC
3094 >> CONJ_TAC >- (Q.EXISTS_TAC ‘c * y’ >> art [])
3095 >> Q.X_GEN_TAC ‘z’ >> DISCH_TAC
3096 >> MATCH_MP_TAC DIFF_UNIQ
3097 >> qexistsl_tac [‘\x. c * g x’, ‘x’] >> art []
3098QED
3099
3100Theorem diffn_linear_general :
3101 !a b f n. (!x. higher_differentiable n f x) ==>
3102 (diffn n (\x. f (a * x + b)) =
3103 \x. a pow n * diffn n f (a * x + b))
3104Proof
3105 NTAC 3 GEN_TAC
3106 >> Induct_on ‘n’ >- rw []
3107 >> rw [FUN_EQ_THM]
3108 >> Know ‘!x. higher_differentiable n f x’
3109 >- (Q.X_GEN_TAC ‘x’ \\
3110 MATCH_MP_TAC higher_differentiable_mono \\
3111 Q.EXISTS_TAC ‘SUC n’ >> simp [])
3112 >> DISCH_TAC
3113 >> qabbrev_tac ‘g = \x. a * x + b’ >> fs []
3114 >> ‘!x. higher_differentiable (SUC n) g x’
3115 by simp [Abbr ‘g’, higher_differentiable_linear]
3116 >> ‘!x. higher_differentiable (SUC n) (\x. f (g x)) x’
3117 by simp [higher_differentiable_chain]
3118 >> Know ‘diffn (SUC n) (\x. f (g x)) = diff1 (diffn n (\x. f (g x)))’
3119 >- (SYM_TAC >> MATCH_MP_TAC diffn_SUC' >> art [])
3120 >> Rewr'
3121 >> simp []
3122 >> Know ‘diff1 (\x. a pow n * diffn n f (g x)) =
3123 \x. a pow n * diff1 (\x. diffn n f (g x)) x’
3124 >- (HO_MATCH_MP_TAC diffn_cmul \\
3125 HO_MATCH_MP_TAC higher_differentiable_chain \\
3126 reverse CONJ_TAC
3127 >- (Q.X_GEN_TAC ‘x’ \\
3128 MATCH_MP_TAC higher_differentiable_mono \\
3129 Q.EXISTS_TAC ‘SUC n’ >> simp []) \\
3130 MATCH_MP_TAC higher_differentiable_imp_1n >> art [])
3131 >> Rewr'
3132 >> simp []
3133 >> Know ‘diff1 (\x. diffn n f (g x)) =
3134 \x. diff1 (diffn n f) (g x) * diff1 g x’
3135 >- (MATCH_MP_TAC diffn_chain \\
3136 reverse CONJ_TAC
3137 >- (Q.X_GEN_TAC ‘x’ \\
3138 MATCH_MP_TAC higher_differentiable_mono \\
3139 Q.EXISTS_TAC ‘SUC n’ >> simp []) \\
3140 MATCH_MP_TAC higher_differentiable_imp_1n >> art [])
3141 >> Rewr'
3142 >> simp []
3143 >> Know ‘diff1 (diffn n f) = diffn (SUC n) f’
3144 >- (MATCH_MP_TAC diffn_SUC' >> art [])
3145 >> Rewr'
3146 >> simp [Abbr ‘g’, diffn_linear, pow]
3147QED
3148
3149(* Temporarily re-enable printing of numeral bits for help documents *)
3150val _ = temp_remove_user_printer ("num.numeral_computations", “n:num”);
3151
3152(* END *)