derivativeScript.sml
1(* ========================================================================= *)
2(* *)
3(* Univariate Derivative Theory in R^1 *)
4(* *)
5(* (c) Copyright, John Harrison 1998-2008 *)
6(* (c) Copyright, Marco Maggesi 2014 *)
7(* (c) Copyright 2015, *)
8(* Muhammad Qasim, *)
9(* Osman Hasan, *)
10(* Hardware Verification Group, *)
11(* Concordia University *)
12(* Contact: <m_qasi@ece.concordia.ca> *)
13(* *)
14(* Note: This theory was ported from HOL Light *)
15(* *)
16(* ========================================================================= *)
17
18Theory derivative
19Ancestors
20 num prim_rec pair combin quotient arithmetic pred_set list
21 option iterate real topology cardinal metric nets real_sigma
22 real_topology
23Libs
24 numLib unwindLib tautLib Arith hurdUtils jrhUtils mesonLib
25 pred_setLib realLib
26
27fun METIS ths tm = prove(tm,METIS_TAC ths);
28
29val DISC_RW_KILL = DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN
30 POP_ASSUM K_TAC;
31
32fun ASSERT_TAC tm = SUBGOAL_THEN tm STRIP_ASSUME_TAC;
33val ASM_ARITH_TAC = REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC;
34
35(* Minimal hol-light compatibility layer *)
36val ASM_REAL_ARITH_TAC = REAL_ASM_ARITH_TAC; (* realLib *)
37val IMP_CONJ = CONJ_EQ_IMP; (* cardinalTheory *)
38val FINITE_SUBSET = SUBSET_FINITE_I; (* pred_setTheory *)
39val LIM = LIM_DEF; (* real_topologyTheory *)
40val REAL_SUB_EQ = REAL_SUB_0; (* cf. HOL-Light's VECTOR_SUB_EQ *)
41val ABS_POS_LT = GSYM ABS_NZ; (* cf. HOL-Light's NORM_POS_LT *)
42val REAL_LE_DIV2_EQ = REAL_LE_RDIV_CANCEL;
43
44val set_ss = std_ss ++ PRED_SET_ss;
45
46(* ------------------------------------------------------------------------- *)
47(* definition(s) moved from other theories *)
48(* ------------------------------------------------------------------------- *)
49
50val exp_ser = “\n. inv(&(FACT n))”;
51
52Definition exp_def :
53 exp(x) = infsum UNIV (\n. (^exp_ser) n * (x pow n))
54End
55
56(* ------------------------------------------------------------------------- *)
57(* Convexity (updated by HOL-Light's convex.ml). *)
58(* ------------------------------------------------------------------------- *)
59
60Definition convex[nocompute]:
61 convex (s:real->bool) <=>
62 !x y u v. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
63 ==> ((u * x) + (v * y)) IN s
64End
65
66Theorem CONVEX_ALT :
67 !s. convex s <=> !x y u. x IN s /\ y IN s /\ &0 <= u /\ u <= &1
68 ==> ((&1 - u) * x + u * y) IN s
69Proof
70 GEN_TAC >> REWRITE_TAC [convex] THEN
71 MESON_TAC [REAL_ARITH ``&0:real <= u /\ &0 <= v /\ (u + v = &1)
72 ==> v <= &1 /\ (u = &1 - v)``,
73 REAL_ARITH ``u <= &1 ==> &0:real <= &1 - u /\ ((&1 - u) + u = &1)``]
74QED
75
76Theorem IN_CONVEX_SET:
77 !s a b u.
78 convex s /\ a IN s /\ b IN s /\ &0 <= u /\ u <= &1
79 ==> ((&1 - u) * a + u * b) IN s
80Proof
81 MESON_TAC[CONVEX_ALT]
82QED
83
84Theorem CONVEX_CONTAINS_SEGMENT :
85 !s. convex s <=> !a b. a IN s /\ b IN s ==> segment[a,b] SUBSET s
86Proof
87 RW_TAC set_ss [CONVEX_ALT, segment, SUBSET_DEF]
88 >> METIS_TAC []
89QED
90
91Theorem CONVEX_CONTAINS_OPEN_SEGMENT :
92 !s. convex s <=> !a b. a IN s /\ b IN s ==> segment(a,b) SUBSET s
93Proof
94 ONCE_REWRITE_TAC[segment] THEN REWRITE_TAC[CONVEX_CONTAINS_SEGMENT] THEN
95 SET_TAC[]
96QED
97
98Theorem CONVEX_CONTAINS_SEGMENT_EQ :
99 !s:real->bool.
100 convex s <=> !a b. segment[a,b] SUBSET s <=> a IN s /\ b IN s
101Proof
102 REWRITE_TAC[CONVEX_CONTAINS_SEGMENT, SUBSET_DEF] THEN
103 MESON_TAC[ENDS_IN_SEGMENT]
104QED
105
106Theorem CONVEX_CONTAINS_SEGMENT_IMP :
107 !s a b. convex s ==> (segment[a,b] SUBSET s <=> a IN s /\ b IN s)
108Proof
109 SIMP_TAC std_ss [CONVEX_CONTAINS_SEGMENT_EQ]
110QED
111
112Theorem SEGMENT_SUBSET_CONVEX :
113 !s a b:real.
114 convex s /\ a IN s /\ b IN s ==> segment[a,b] SUBSET s
115Proof
116 MESON_TAC[CONVEX_CONTAINS_SEGMENT]
117QED
118
119Theorem CONVEX_CONTAINS :
120 !s a b x:real.
121 convex s /\ a IN s /\ b IN s /\ x IN segment[a,b] ==> x IN s
122Proof
123 MESON_TAC[SEGMENT_SUBSET_CONVEX, SUBSET_DEF]
124QED
125
126Theorem CONVEX_EMPTY :
127 convex {}
128Proof
129 REWRITE_TAC[convex, NOT_IN_EMPTY]
130QED
131
132Theorem CONVEX_SING :
133 !a. convex {a}
134Proof
135 SIMP_TAC std_ss[convex, IN_SING, GSYM REAL_ADD_RDISTRIB, REAL_MUL_LID]
136QED
137
138Theorem CONVEX_UNIV :
139 convex(UNIV:real->bool)
140Proof
141 REWRITE_TAC[convex, IN_UNIV]
142QED
143
144Theorem CONVEX_INTERS :
145 !f. (!s. s IN f ==> convex s) ==> convex(INTERS f)
146Proof
147 REWRITE_TAC[convex, IN_INTERS] THEN MESON_TAC[]
148QED
149
150Theorem CONVEX_INTER :
151 !s t. convex s /\ convex t ==> convex(s INTER t)
152Proof
153 REWRITE_TAC[convex, IN_INTER] THEN MESON_TAC[]
154QED
155
156Theorem LIMPT_OF_CONVEX :
157 !s x:real. convex s /\ x IN s ==> (x limit_point_of s <=> ~(s = {x}))
158Proof
159 rpt STRIP_TAC
160 >> ASM_CASES_TAC ``s = {x:real}`` >> art [LIMPT_SING]
161 >> `?y:real. y IN s /\ ~(y = x)` by ASM_SET_TAC []
162 >> REWRITE_TAC [LIMPT_APPROACHABLE]
163 >> Q.X_GEN_TAC `e` >> DISCH_TAC
164 >> Q.ABBREV_TAC `u = min (&1 / &2) (e / &2 / abs(y - x:real))`
165 >> Know `&0 < u /\ u < &1:real`
166 >- (Q.UNABBREV_TAC `u` >> REWRITE_TAC [REAL_LT_MIN, REAL_MIN_LT] \\
167 SIMP_TAC std_ss [REAL_HALF_BETWEEN] \\
168 ASM_SIMP_TAC real_ss [REAL_HALF, REAL_LT_DIV, GSYM ABS_NZ, REAL_SUB_0])
169 >> DISCH_TAC
170 >> Q.EXISTS_TAC `(&1 - u) * x + u * y:real`
171 >> rpt CONJ_TAC (* 3 subgoals *)
172 >| [ (* goal 1 (of 3) *)
173 FIRST_X_ASSUM (MATCH_MP_TAC o REWRITE_RULE [CONVEX_ALT]) \\
174 ASM_SIMP_TAC real_ss [REAL_LT_IMP_LE],
175 (* goal 2 (of 3) *)
176 ASM_SIMP_TAC std_ss [REAL_ENTIRE, REAL_SUB_0, REAL_ARITH
177 ``((&1 - u) * x + u * y:real = x) <=> (u * (y - x) = 0)``] \\
178 ASM_REAL_ARITH_TAC,
179 (* goal 3 (of 3) *)
180 REWRITE_TAC [dist, ABS_MUL, REAL_ARITH
181 ``((&1 - u) * x + u * y) - x:real = u * (y - x)``] \\
182 ASM_SIMP_TAC std_ss [REAL_ARITH ``&0 < u ==> (abs u = u:real)``] \\
183 MATCH_MP_TAC (REAL_ARITH ``x * 2 <= e /\ &0 < e ==> x < e:real``) \\
184 ASM_SIMP_TAC real_ss [GSYM REAL_LE_RDIV_EQ, GSYM ABS_NZ, REAL_SUB_0] \\
185 Q.UNABBREV_TAC `u` >> FULL_SIMP_TAC real_ss [min_def] ]
186QED
187
188Theorem TRIVIAL_LIMIT_WITHIN_CONVEX:
189 !s x:real.
190 convex s /\ x IN s ==> (trivial_limit(at x within s) <=> (s = {x}))
191Proof
192 SIMP_TAC std_ss [TRIVIAL_LIMIT_WITHIN, LIMPT_OF_CONVEX]
193QED
194
195(* ------------------------------------------------------------------------- *)
196(* A general lemma. *)
197(* ------------------------------------------------------------------------- *)
198
199Theorem CONVEX_CONNECTED:
200 !s:real->bool. convex s ==> connected s
201Proof
202 SIMP_TAC std_ss [CONVEX_ALT, connected, SUBSET_DEF, EXTENSION, IN_INTER,
203 IN_UNION, NOT_IN_EMPTY, NOT_FORALL_THM, NOT_EXISTS_THM] THEN
204 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
205 CCONTR_TAC THEN FULL_SIMP_TAC std_ss [] THEN
206 MP_TAC(ISPECL [``\u. (&1 - u) * x + u * (x':real)``,
207 ``&0:real``, ``&1:real``, ``e1:real->bool``, ``e2:real->bool``]
208 (SIMP_RULE std_ss [GSYM open_def] CONNECTED_REAL_LEMMA)) THEN
209 ASM_SIMP_TAC real_ss [NOT_IMP, REAL_SUB_RZERO, REAL_MUL_LID, REAL_MUL_LZERO,
210 REAL_SUB_REFL, REAL_ADD_RID, REAL_ADD_LID, REAL_POS] THEN
211 REPEAT(CONJ_TAC THENL [ALL_TAC, ASM_MESON_TAC[]]) THEN
212 REPEAT STRIP_TAC THEN REWRITE_TAC[dist] THEN
213 SIMP_TAC real_ss [ABS_MUL, REAL_ARITH
214 ``((&1 - a) * x + a * y) - ((&1 - b) * x + b * y) = (a - b) * (y - x:real)``] THEN
215 MP_TAC(ISPEC ``(x' - x):real`` ABS_POS) THEN
216 REWRITE_TAC[REAL_LE_LT] THEN STRIP_TAC THENL
217 [ALL_TAC, METIS_TAC[REAL_MUL_RZERO, REAL_LT_01]] THEN
218 EXISTS_TAC ``e / abs((x' - x):real)`` THEN
219 ASM_SIMP_TAC real_ss [REAL_LT_RDIV_EQ, REAL_LT_DIV]
220QED
221
222(* ------------------------------------------------------------------------- *)
223(* Explicit expressions for convexity in terms of arbitrary sums. *)
224(* ------------------------------------------------------------------------- *)
225
226Theorem CONVEX_SUM :
227 !s k u x:'a->real.
228 FINITE k /\ convex s /\ (sum k u = &1) /\
229 (!i. i IN k ==> &0 <= u i /\ x i IN s)
230 ==> sum k (\i. u i * x i) IN s
231Proof
232 GEN_TAC THEN ASM_CASES_TAC ``convex(s:real->bool)`` THEN
233 ASM_SIMP_TAC std_ss [IMP_CONJ, RIGHT_FORALL_IMP_THM] THEN
234 ONCE_REWRITE_TAC [METIS []
235 ``!k. (!u. (sum k u = 1) ==>
236 !x. (!i. i IN k ==> 0 <= u i /\ x i IN s) ==>
237 sum k (\i. u i * x i) IN s) =
238 (\k. !u. (sum k u = 1) ==>
239 !x. (!i. i IN k ==> 0 <= u i /\ x i IN s) ==>
240 sum k (\i. u i * x i) IN s) k``] THEN
241 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN
242 SIMP_TAC real_ss [SUM_CLAUSES, FORALL_IN_INSERT] THEN
243 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN
244 MAP_EVERY X_GEN_TAC [``k:'a->bool``, ``i:'a``, ``u:'a->real``, ``x:'a->real``] THEN
245 REWRITE_TAC[AND_IMP_INTRO] THEN STRIP_TAC THEN
246 ASM_CASES_TAC ``(u:'a->real) i = &1`` THENL
247 [ASM_REWRITE_TAC[REAL_ARITH ``(&1 + a = &1) <=> (a = &0:real)``] THEN
248 SUBGOAL_THEN ``sum k (\i:'a. u i * x(i):real) = 0``
249 (fn th => ASM_SIMP_TAC std_ss [th, REAL_ADD_RID, REAL_MUL_LID]) THEN
250 MATCH_MP_TAC SUM_EQ_0' THEN SIMP_TAC std_ss [REAL_ENTIRE] THEN
251 REPEAT STRIP_TAC THEN DISJ1_TAC THEN
252 POP_ASSUM MP_TAC THEN SPEC_TAC (``x':'a``,``x':'a``) THEN
253 MATCH_MP_TAC SUM_POS_EQ_0 THEN ASM_SIMP_TAC std_ss [] THEN
254 POP_ASSUM MP_TAC THEN UNDISCH_TAC ``(u:'a->real) i + sum k u = 1`` THEN
255 REAL_ARITH_TAC,
256 FIRST_X_ASSUM(MP_TAC o SPEC ``(\j. (u:'a->real)(j) / (&1 - u(i)))``) THEN
257 ASM_REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
258 ASM_SIMP_TAC std_ss [SUM_LMUL, GSYM REAL_MUL_ASSOC] THEN
259 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN
260 REWRITE_TAC [real_div] THEN ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN
261 REWRITE_TAC [REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN
262 ASM_SIMP_TAC std_ss [SUM_LMUL] THEN
263 SUBGOAL_THEN ``&0:real < &1 - u(i:'a)`` ASSUME_TAC THENL
264 [ASM_MESON_TAC[SUM_POS_LE, REAL_ADD_SYM, REAL_ARITH
265 ``&0 <= a /\ &0 <= b /\ (b + a = &1) /\ ~(a = &1) ==> &0 < &1 - a:real``],
266 ALL_TAC] THEN
267 REWRITE_TAC[GSYM real_div] THEN
268 ASM_SIMP_TAC real_ss [REAL_LE_DIV, REAL_LT_IMP_LE] THEN
269 ASM_SIMP_TAC real_ss [REAL_EQ_LDIV_EQ, REAL_MUL_LID, REAL_EQ_SUB_LADD] THEN
270 DISCH_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
271 UNDISCH_TAC ``convex s`` THEN DISCH_TAC THEN
272 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [convex]) THEN
273 DISCH_THEN(MP_TAC o SPECL
274 [``sum k (\j. (u j / (&1 - u(i:'a))) * x(j) :real)``,
275 ``x(i:'a):real``, ``&1 - u(i:'a):real``, ``u(i:'a):real``]) THEN
276 REWRITE_TAC[real_div, REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
277 REWRITE_TAC[real_div, REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
278 ASM_SIMP_TAC std_ss [GSYM REAL_MUL_ASSOC, SUM_LMUL] THEN
279 REWRITE_TAC [REAL_MUL_ASSOC] THEN
280 SIMP_TAC real_ss [REAL_ARITH ``a * inv (1 - (u:'a->real) i) * b =
281 inv (1 - (u:'a->real) i) * a * b``] THEN
282 ASM_SIMP_TAC std_ss [GSYM REAL_MUL_ASSOC, SUM_LMUL] THEN
283 ASM_SIMP_TAC real_ss [REAL_MUL_ASSOC, REAL_MUL_RINV, REAL_LT_IMP_NE] THEN
284 REWRITE_TAC[REAL_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN
285 ASM_SIMP_TAC real_ss [REAL_LT_IMP_LE, SUM_LMUL] THEN
286 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[REAL_ADD_SYM]]
287QED
288
289Theorem CONVEX_INDEXED:
290 !s:real->bool.
291 convex s <=>
292 !k u x. (!i:num. 1 <= i /\ i <= k ==> &0 <= u(i) /\ x(i) IN s) /\
293 (sum { 1n..k} u = &1)
294 ==> sum { 1n..k} (\i. u(i) * x(i)) IN s
295Proof
296 REPEAT GEN_TAC THEN EQ_TAC THENL
297 [REPEAT STRIP_TAC THEN MATCH_MP_TAC CONVEX_SUM THEN
298 ASM_SIMP_TAC std_ss [IN_NUMSEG, FINITE_NUMSEG],
299 DISCH_TAC THEN REWRITE_TAC[convex] THEN
300 MAP_EVERY X_GEN_TAC [``x:real``, ``y:real``, ``u:real``, ``v:real``] THEN
301 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC ``2:num``) THEN
302 DISCH_THEN(MP_TAC o SPEC ``\n:num. if n = 1 then u else v:real``) THEN
303 DISCH_THEN(MP_TAC o SPEC ``\n:num. if n = 1 then x else y:real``) THEN
304 REWRITE_TAC [TWO, SUM_CLAUSES_NUMSEG, NUMSEG_SING, SUM_SING] THEN
305 SIMP_TAC arith_ss [] THEN METIS_TAC[]]
306QED
307
308(* ------------------------------------------------------------------------- *)
309(* Convexity of general and special intervals. *)
310(* ------------------------------------------------------------------------- *)
311
312Theorem IS_INTERVAL_CONVEX:
313 !s:real->bool. is_interval s ==> convex s
314Proof
315 REWRITE_TAC[is_interval, convex] THEN
316 REPEAT STRIP_TAC THEN
317 KNOW_TAC ``x IN (s:real->bool) /\ y IN s ==>
318 x <= (u * x + v * y) /\ (u * x + v * y) <= y \/
319 y <= (u * x + v * y) /\ (u * x + v * y) <= x`` THENL
320 [ALL_TAC, METIS_TAC []] THEN
321 ASM_SIMP_TAC std_ss [] THEN
322 DISJ_CASES_TAC(SPECL [``(x:real)``, ``(y:real)``] REAL_LE_TOTAL) THENL
323 [DISJ1_TAC, DISJ2_TAC] THEN
324 MATCH_MP_TAC(REAL_ARITH
325 ``&1 * a <= b /\ b <= &1 * c ==> a <= b /\ b <= c:real``) THEN
326 FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN
327 ASM_SIMP_TAC real_ss [REAL_ADD_RDISTRIB] THEN
328 ASM_SIMP_TAC real_ss [REAL_LE_LMUL, REAL_LE_LADD, REAL_LE_RADD] THEN
329 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_LMUL_IMP THEN ASM_REWRITE_TAC []
330QED
331
332Theorem IS_INTERVAL_CONNECTED:
333 !s:real->bool. is_interval s ==> connected s
334Proof
335 MESON_TAC[IS_INTERVAL_CONVEX, CONVEX_CONNECTED]
336QED
337
338Theorem IS_INTERVAL_CONNECTED_1:
339 !s:real->bool. is_interval s <=> connected s
340Proof
341 GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[IS_INTERVAL_CONNECTED] THEN
342 ONCE_REWRITE_TAC[MONO_NOT_EQ] THEN
343 SIMP_TAC std_ss [IS_INTERVAL, connected, NOT_FORALL_THM,
344 LEFT_IMP_EXISTS_THM, NOT_IMP] THEN
345 qx_genl_tac [‘a’, ‘b’, ‘x’] THEN STRIP_TAC THEN
346 MAP_EVERY EXISTS_TAC [``{z:real | 1 * z < x}``, ``{z:real | 1 * z > x}``] THEN
347 REWRITE_TAC[OPEN_HALFSPACE_LT, OPEN_HALFSPACE_GT] THEN
348 SIMP_TAC arith_ss [SUBSET_DEF, EXTENSION, IN_UNION, IN_INTER, NOT_FORALL_THM,
349 real_gt, NOT_IN_EMPTY, GSPECIFICATION] THEN
350 SIMP_TAC real_ss [] THEN
351 REPEAT CONJ_TAC THENL [simp[REAL_NOT_LT, REAL_LE_TOTAL],
352 metis_tac[REAL_LT_TOTAL], metis_tac[REAL_LE_LT], metis_tac[REAL_LE_LT]]
353QED
354
355Theorem CONVEX_INTERVAL:
356 !a b:real. convex(interval [a,b]) /\ convex(interval (a,b))
357Proof
358 METIS_TAC [IS_INTERVAL_CONVEX, IS_INTERVAL_INTERVAL]
359QED
360
361
362(* ------------------------------------------------------------------------- *)
363(* On real, is_interval, convex and connected are all equivalent. *)
364(* ------------------------------------------------------------------------- *)
365
366Theorem IS_INTERVAL_CONVEX_1:
367 !s:real->bool. is_interval s <=> convex s
368Proof
369 MESON_TAC[IS_INTERVAL_CONVEX, CONVEX_CONNECTED, IS_INTERVAL_CONNECTED_1]
370QED
371
372(* ------------------------------------------------------------------------- *)
373(* *)
374(* ------------------------------------------------------------------------- *)
375
376Theorem CONNECTED_COMPACT_INTERVAL_1:
377 !s:real->bool. connected s /\ compact s <=> ?a b. s = interval[a,b]
378Proof
379 REWRITE_TAC[GSYM IS_INTERVAL_CONNECTED_1, IS_INTERVAL_COMPACT]
380QED
381
382(* ------------------------------------------------------------------------- *)
383(* Convex functions into the reals (from HOL-Light's convex.ml). *)
384(* ------------------------------------------------------------------------- *)
385
386val _ = set_fixity "convex_on" (Infix(NONASSOC, 450));
387
388Definition convex_on[nocompute]:
389 f convex_on s <=>
390 !x y u v:real. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
391 ==> f(u * x + v * y) <= u * f(x) + v * f(y)
392End
393
394Theorem CONVEX_ON_EMPTY :
395 !f:real->real. f convex_on {}
396Proof
397 REWRITE_TAC[convex_on, NOT_IN_EMPTY]
398QED
399
400Theorem CONVEX_ON_SUBSET :
401 !f s t. f convex_on t /\ s SUBSET t ==> f convex_on s
402Proof
403 REWRITE_TAC[convex_on, SUBSET_DEF] THEN MESON_TAC[]
404QED
405
406Theorem CONVEX_ON_EQ :
407 !f g s. convex s /\ (!x. x IN s ==> f x = g x) /\ f convex_on s
408 ==> g convex_on s
409Proof
410 REWRITE_TAC[convex_on, convex] THEN MESON_TAC[]
411QED
412
413Theorem CONVEX_ON_CONST :
414 !s a. (\x. a) convex_on s
415Proof
416 SIMP_TAC std_ss[convex_on, GSYM REAL_ADD_RDISTRIB, REAL_MUL_LID, REAL_LE_REFL]
417QED
418
419Theorem LINEAR_IMP_CONVEX_ON :
420 !f s:real->bool. linear f ==> f convex_on s
421Proof
422 REWRITE_TAC[linear, convex_on] THEN rw []
423QED
424
425Theorem CONVEX_ON_SING :
426 !f a:real. f convex_on {a}
427Proof
428 REPEAT GEN_TAC THEN MATCH_MP_TAC CONVEX_ON_EQ THEN
429 EXISTS_TAC ``\x:real. (f:real->real) a`` THEN
430 SIMP_TAC std_ss[IN_SING, CONVEX_SING, CONVEX_ON_CONST]
431QED
432
433Theorem CONVEX_ADD :
434 !s f g. f convex_on s /\ g convex_on s ==> (\x. f(x) + g(x)) convex_on s
435Proof
436 SIMP_TAC bool_ss [convex_on, AND_FORALL_THM] THEN
437 REPEAT(HO_MATCH_MP_TAC MONO_FORALL ORELSE GEN_TAC) THEN
438 HO_MATCH_MP_TAC(TAUT
439 `(b /\ c ==> d) ==> (a ==> b) /\ (a ==> c) ==> a ==> d`) THEN
440 REAL_ARITH_TAC
441QED
442
443Theorem CONVEX_ADD_EQ :
444 !a f s:real->bool. (\x. a + f x) convex_on s <=> f convex_on s
445Proof
446 REPEAT STRIP_TAC THEN EQ_TAC THEN
447 SIMP_TAC std_ss [CONVEX_ADD, CONVEX_ON_CONST] THEN
448 DISCH_THEN(MP_TAC o SPEC ``(\x. -a):real->real`` o
449 MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT] CONVEX_ADD)) THEN
450 SIMP_TAC (std_ss ++ ETA_ss) [CONVEX_ON_CONST, REAL_ARITH ``-a + (a + x:real) = x``]
451QED
452
453(* NOTE: HOL-Light's [REAL_LE_LMUL] is HOL4's [REAL_LE_LMUL_IMP]. *)
454Theorem CONVEX_CMUL :
455 !s c f. &0 <= c /\ f convex_on s ==> (\x. c * f(x)) convex_on s
456Proof
457 RW_TAC std_ss [convex_on, REAL_LE_LMUL_IMP,
458 REAL_ARITH ``u * (c * fx) + v * (c * fy) = (c :real) * (u * fx + v * fy)``]
459QED
460
461Theorem CONVEX_MAX :
462 !f g s. f convex_on s /\ g convex_on s
463 ==> (\x. max (f x) (g x)) convex_on s
464Proof
465 SIMP_TAC std_ss[convex_on, REAL_MAX_LE] THEN REPEAT STRIP_TAC THEN
466 FIRST_X_ASSUM(fn th =>
467 W(MP_TAC o PART_MATCH (lhand o rand) th o lhand o snd)) THEN
468 ASM_REWRITE_TAC[] THEN
469 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
470 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THEN
471 MATCH_MP_TAC REAL_LE_LMUL_IMP THEN ASM_REAL_ARITH_TAC
472QED
473
474Theorem REAL_CONVEX_BOUND2_LT :
475 !x y a b u v:real. x < a /\ y < b /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
476 ==> u * x + v * y < u * a + v * b
477Proof
478 REPEAT GEN_TAC THEN ASM_CASES_TAC ``u = &0:real`` THENL
479 [ASM_REWRITE_TAC[REAL_MUL_LZERO, REAL_ADD_LID] THEN REPEAT STRIP_TAC,
480 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_ADD2 THEN
481 ASM_SIMP_TAC real_ss [REAL_LE_LMUL_IMP, REAL_LT_IMP_LE]] THEN
482 MATCH_MP_TAC REAL_LT_LMUL_IMP THEN ASM_REAL_ARITH_TAC
483QED
484
485Theorem REAL_CONVEX_BOUND_LT:
486 !x y a u v:real. x < a /\ y < a /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
487 ==> u * x + v * y < a
488Proof
489 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN
490 Q.EXISTS_TAC `u * a + v * a:real` THEN CONJ_TAC THENL
491 [ASM_SIMP_TAC real_ss [REAL_CONVEX_BOUND2_LT],
492 ALL_TAC] THEN
493 MATCH_MP_TAC REAL_EQ_IMP_LE THEN
494 UNDISCH_TAC ``u + v = &1:real`` THEN
495 SIMP_TAC real_ss [GSYM REAL_ADD_RDISTRIB]
496QED
497
498Theorem CONVEX_DISTANCE:
499 !s a. (\x. dist(a,x)) convex_on s
500Proof
501 SIMP_TAC std_ss [convex_on, dist] THEN REPEAT STRIP_TAC THEN
502 GEN_REWR_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [GSYM REAL_MUL_LID] THEN
503 FIRST_ASSUM(SUBST1_TAC o SYM) THEN
504 REWRITE_TAC[REAL_ARITH
505 ``(u + v) * z - (u * x + v * y) = u * (z - x) + v * (z - y:real)``] THEN
506 ASM_MESON_TAC[ABS_TRIANGLE, ABS_MUL, ABS_REFL]
507QED
508
509val lemma = REWRITE_RULE[convex_on, IN_UNIV]
510 (ISPEC ``univ(:real)`` CONVEX_DISTANCE);
511
512Theorem CONVEX_BALL:
513 !x:real e. convex(ball(x,e))
514Proof
515 SIMP_TAC std_ss [convex, IN_BALL] THEN REPEAT STRIP_TAC THEN
516 ASM_MESON_TAC[REAL_LET_TRANS, REAL_CONVEX_BOUND_LT, lemma]
517QED
518
519(* ------------------------------------------------------------------------- *)
520(* Derivatives. The definition is slightly tricky since we make it work over *)
521(* nets of a particular form. This lets us prove theorems generally and use *)
522(* "at a" or "at a within s" for restriction to a set (1-sided on R etc.) *)
523(* ------------------------------------------------------------------------- *)
524
525val _ = set_fixity "has_derivative" (Infix(NONASSOC, 450));
526
527Definition has_derivative[nocompute]:
528 (f has_derivative f') net <=>
529 linear f' /\
530 ((\y. inv(abs(y - netlimit net)) *
531 (f(y) -
532 (f(netlimit net) + f'(y - netlimit net)))) --> 0) net
533End
534
535(* ------------------------------------------------------------------------- *)
536(* These are the only cases we'll care about, probably. *)
537(* ------------------------------------------------------------------------- *)
538
539Theorem has_derivative_within:
540 !f:real->real f' x s.
541 (f has_derivative f') (at x within s) <=>
542 linear f' /\
543 ((\y. inv(abs(y - x)) * (f(y) - (f(x) + f'(y - x)))) --> 0)
544 (at x within s)
545Proof
546 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative] THEN AP_TERM_TAC THEN
547 ASM_CASES_TAC ``trivial_limit(at (x:real) within s)`` THENL
548 [ASM_REWRITE_TAC[LIM], ASM_SIMP_TAC std_ss [NETLIMIT_WITHIN]]
549QED
550
551Theorem has_derivative_at:
552 !f:real->real f' x.
553 (f has_derivative f') (at x) <=>
554 linear f' /\
555 ((\y. inv(abs(y - x)) * (f(y) - (f(x) + f'(y - x)))) --> 0)
556 (at x)
557Proof
558 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
559 REWRITE_TAC[has_derivative_within]
560QED
561
562(* ------------------------------------------------------------------------- *)
563(* More explicit epsilon-delta forms. *)
564(* ------------------------------------------------------------------------- *)
565
566Theorem HAS_DERIVATIVE_WITHIN :
567 !f f' x s. (f has_derivative f')(at x within s) <=>
568 linear f' /\
569 !e. &0 < e
570 ==> ?d. &0 < d /\
571 !x'. x' IN s /\
572 &0 < abs(x' - x) /\ abs(x' - x) < d
573 ==> abs(f(x') - f(x) - f'(x' - x)) /
574 abs(x' - x) < e
575Proof
576 rpt GEN_TAC
577 >> SIMP_TAC std_ss [has_derivative_within, LIM_WITHIN] THEN AP_TERM_TAC
578 >> SIMP_TAC std_ss [dist, REAL_ARITH ``(x' - (x + d)) = x' - x - d:real``]
579 >> SIMP_TAC std_ss [real_div, REAL_SUB_RZERO, ABS_MUL]
580 >> SIMP_TAC std_ss [REAL_MUL_ASSOC, REAL_MUL_SYM, ABS_INV, ABS_ABS, REAL_LT_IMP_NE]
581QED
582
583Theorem HAS_DERIVATIVE_AT :
584 !f f' x. (f has_derivative f')(at x) <=>
585 linear f' /\
586 !e. &0 < e
587 ==> ?d. &0 < d /\
588 !x'. &0 < abs(x' - x) /\ abs(x' - x) < d
589 ==> abs(f(x') - f(x) - f'(x' - x)) /
590 abs(x' - x) < e
591Proof
592 ONCE_REWRITE_TAC [GSYM WITHIN_UNIV]
593 >> REWRITE_TAC [HAS_DERIVATIVE_WITHIN, IN_UNIV]
594QED
595
596Theorem HAS_DERIVATIVE_AT_WITHIN :
597 !f f' x s. (f has_derivative f') (at x)
598 ==> (f has_derivative f') (at x within s)
599Proof
600 REWRITE_TAC [HAS_DERIVATIVE_WITHIN, HAS_DERIVATIVE_AT]
601 >> MESON_TAC []
602QED
603
604Theorem HAS_DERIVATIVE_WITHIN_OPEN:
605 !f f' a s.
606 a IN s /\ open s
607 ==> ((f has_derivative f') (at a within s) <=>
608 (f has_derivative f') (at a))
609Proof
610 SIMP_TAC std_ss [has_derivative_within, has_derivative_at, LIM_WITHIN_OPEN]
611QED
612
613(* ------------------------------------------------------------------------- *)
614(* Combining theorems. *)
615(* ------------------------------------------------------------------------- *)
616
617Theorem HAS_DERIVATIVE_LINEAR:
618 !f net. linear f ==> (f has_derivative f) net
619Proof
620 RW_TAC real_ss [has_derivative, real_sub] THEN
621 ASM_SIMP_TAC real_ss [GSYM LINEAR_ADD, GSYM LINEAR_CMUL, GSYM LINEAR_NEG] THEN
622 ASM_SIMP_TAC real_ss [REAL_ARITH ``a + -(b + (a + -b)) = 0:real``] THEN
623 ASM_SIMP_TAC real_ss [LINEAR_0, LIM_CONST]
624QED
625
626Theorem HAS_DERIVATIVE_ID:
627 !net. ((\x. x) has_derivative (\h. h)) net
628Proof
629 SIMP_TAC real_ss [HAS_DERIVATIVE_LINEAR, LINEAR_ID]
630QED
631
632Theorem HAS_DERIVATIVE_CONST:
633 !c net. ((\x. c) has_derivative (\h. 0)) net
634Proof
635 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative, linear] THEN
636 SIMP_TAC real_ss [REAL_ADD_RID, REAL_SUB_REFL, REAL_MUL_RZERO, LIM_CONST]
637QED
638
639Theorem HAS_DERIVATIVE_CMUL:
640 !f f' net c. (f has_derivative f') net
641 ==> ((\x. c * f(x)) has_derivative (\h. c * f'(h))) net
642Proof
643 REPEAT GEN_TAC THEN SIMP_TAC real_ss [has_derivative, LINEAR_COMPOSE_CMUL] THEN
644 DISCH_THEN(MP_TAC o SPEC ``c:real`` o MATCH_MP LIM_CMUL o CONJUNCT2) THEN
645 SIMP_TAC real_ss [REAL_MUL_RZERO] THEN MATCH_MP_TAC EQ_IMPLIES THEN
646 AP_THM_TAC THEN AP_THM_TAC THEN
647 AP_TERM_TAC THEN ABS_TAC THEN REAL_ARITH_TAC
648QED
649
650Theorem HAS_DERIVATIVE_NEG:
651 !f f' net. (f has_derivative f') net
652 ==> ((\x. -(f(x))) has_derivative (\h. -(f'(h)))) net
653Proof
654 ONCE_REWRITE_TAC[REAL_NEG_MINUS1] THEN
655 SIMP_TAC real_ss [HAS_DERIVATIVE_CMUL]
656QED
657
658Theorem HAS_DERIVATIVE_ADD:
659 !f f' g g' net.
660 (f has_derivative f') net /\ (g has_derivative g') net
661 ==> ((\x. f(x) + g(x)) has_derivative (\h. f'(h) + g'(h))) net
662Proof
663 REPEAT GEN_TAC THEN SIMP_TAC std_ss [has_derivative, LINEAR_COMPOSE_ADD] THEN
664 DISCH_THEN(MP_TAC o MATCH_MP (TAUT `(a /\ b) /\ (c /\ d) ==> b /\ d`)) THEN
665 DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN REWRITE_TAC[REAL_ADD_LID] THEN
666 MATCH_MP_TAC EQ_IMPLIES THEN SIMP_TAC std_ss [] THEN
667 AP_THM_TAC THEN AP_THM_TAC THEN
668 AP_TERM_TAC THEN ABS_TAC THEN REAL_ARITH_TAC
669QED
670
671Theorem HAS_DERIVATIVE_SUB:
672 !f f' g g' net.
673 (f has_derivative f') net /\ (g has_derivative g') net
674 ==> ((\x. f(x) - g(x)) has_derivative (\h. f'(h) - g'(h))) net
675Proof
676 SIMP_TAC real_ss [real_sub, HAS_DERIVATIVE_ADD, HAS_DERIVATIVE_NEG]
677QED
678
679Theorem HAS_DERIVATIVE_SUM :
680 !f f' net s. FINITE s /\ (!a. a IN s ==> ((f a) has_derivative (f' a)) net)
681 ==> ((\x. sum s (\a. f a x)) has_derivative (\h. sum s (\a. f' a h))) net
682Proof
683 NTAC 3 GEN_TAC >> REWRITE_TAC [IMP_CONJ]
684 >> SET_INDUCT_TAC
685 >> ASM_SIMP_TAC std_ss [SUM_CLAUSES, HAS_DERIVATIVE_CONST]
686 >> rpt STRIP_TAC
687 >> ONCE_REWRITE_TAC [METIS [] ``sum s (\a. f a x) = (\x. sum s (\a. f a x)) x``]
688 >> MATCH_MP_TAC HAS_DERIVATIVE_ADD
689 >> SIMP_TAC std_ss [ETA_AX] >> ASM_SIMP_TAC std_ss [IN_INSERT]
690QED
691
692(* ------------------------------------------------------------------------- *)
693(* Limit transformation for derivatives. *)
694(* ------------------------------------------------------------------------- *)
695
696Theorem HAS_DERIVATIVE_TRANSFORM_WITHIN:
697 !f f' g x s d.
698 &0 < d /\ x IN s /\
699 (!x'. x' IN s /\ dist (x',x) < d ==> (f x' = g x')) /\
700 (f has_derivative f') (at x within s)
701 ==> (g has_derivative f') (at x within s)
702Proof
703 REPEAT GEN_TAC THEN SIMP_TAC std_ss [has_derivative_within, IMP_CONJ] THEN
704 DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN
705 MATCH_MP_TAC(REWRITE_RULE[TAUT `a /\ b /\ c ==> d <=> a /\ b ==> c ==> d`]
706 LIM_TRANSFORM_WITHIN) THEN
707 Q.EXISTS_TAC `d:real` THEN ASM_SIMP_TAC std_ss [DIST_REFL]
708QED
709
710Theorem HAS_DERIVATIVE_TRANSFORM_AT:
711 !f f' g x d.
712 &0 < d /\ (!x'. dist (x',x) < d ==> (f x' = g x')) /\
713 (f has_derivative f') (at x)
714 ==> (g has_derivative f') (at x)
715Proof
716 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
717 MESON_TAC[HAS_DERIVATIVE_TRANSFORM_WITHIN, IN_UNIV]
718QED
719
720Theorem HAS_DERIVATIVE_WITHIN_CONG :
721 !f f' g x s.
722 x IN s /\ (!x'. x' IN s ==> (f x' = g x')) ==>
723 ((f has_derivative f') (at x within s) <=>
724 (g has_derivative f') (at x within s))
725Proof
726 rpt STRIP_TAC
727 >> EQ_TAC >> DISCH_TAC
728 >| [ (* goal 1 (of 2) *)
729 MATCH_MP_TAC HAS_DERIVATIVE_TRANSFORM_WITHIN \\
730 qexistsl_tac [‘f’, ‘1’] >> simp [DIST_REFL],
731 (* goal 2 (of 2) *)
732 MATCH_MP_TAC HAS_DERIVATIVE_TRANSFORM_WITHIN \\
733 qexistsl_tac [‘g’, ‘1’] >> simp [DIST_REFL] ]
734QED
735
736(* ------------------------------------------------------------------------- *)
737(* Differentiability. *)
738(* ------------------------------------------------------------------------- *)
739
740val _ = set_fixity "differentiable" (Infix(NONASSOC, 450));
741val _ = set_fixity "differentiable_on" (Infix(NONASSOC, 450));
742
743val _ = hide "differentiable";
744
745Definition differentiable[nocompute]:
746 f differentiable net <=> ?f'. ((f has_derivative f') net)
747End
748
749Definition differentiable_on[nocompute]:
750 f differentiable_on s <=> !x. x IN s ==> f differentiable (at x within s)
751End
752
753Theorem HAS_DERIVATIVE_IMP_DIFFERENTIABLE :
754 !f f' net. (f has_derivative f') net ==> f differentiable net
755Proof
756 REWRITE_TAC[differentiable] THEN MESON_TAC[]
757QED
758
759Theorem DIFFERENTIABLE_AT_WITHIN :
760 !f s x. f differentiable (at x)
761 ==> f differentiable (at x within s)
762Proof
763 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_AT_WITHIN]
764QED
765
766Theorem DIFFERENTIABLE_WITHIN_OPEN :
767 !f a s.
768 a IN s /\ open s
769 ==> (f differentiable (at a within s) <=> (f differentiable (at a)))
770Proof
771 SIMP_TAC std_ss[differentiable, HAS_DERIVATIVE_WITHIN_OPEN]
772QED
773
774Theorem DIFFERENTIABLE_AT_IMP_DIFFERENTIABLE_ON :
775 !f s. (!x. x IN s ==> f differentiable at x) ==> f differentiable_on s
776Proof
777 REWRITE_TAC[differentiable_on] THEN MESON_TAC[DIFFERENTIABLE_AT_WITHIN]
778QED
779
780Theorem DIFFERENTIABLE_ON_EQ_DIFFERENTIABLE_AT :
781 !f s. open s ==> (f differentiable_on s <=>
782 !x. x IN s ==> f differentiable at x)
783Proof
784 SIMP_TAC std_ss[differentiable_on, DIFFERENTIABLE_WITHIN_OPEN]
785QED
786
787Theorem DIFFERENTIABLE_TRANSFORM_WITHIN :
788 !f g x s d.
789 &0 < d /\ x IN s /\
790 (!x'. x' IN s /\ dist (x',x) < d ==> f x' = g x') /\
791 f differentiable (at x within s)
792 ==> g differentiable (at x within s)
793Proof
794 REWRITE_TAC[differentiable] THEN
795 MESON_TAC[HAS_DERIVATIVE_TRANSFORM_WITHIN]
796QED
797
798Theorem DIFFERENTIABLE_TRANSFORM_AT :
799 !f g x d.
800 &0 < d /\
801 (!x'. dist (x',x) < d ==> f x' = g x') /\
802 f differentiable at x
803 ==> g differentiable at x
804Proof
805 REWRITE_TAC[differentiable] THEN
806 MESON_TAC[HAS_DERIVATIVE_TRANSFORM_AT]
807QED
808
809Theorem DIFFERENTIABLE_ON_EQ :
810 !f g s.
811 (!x. x IN s ==> f x = g x) /\ f differentiable_on s
812 ==> g differentiable_on s
813Proof
814 REPEAT GEN_TAC THEN
815 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
816 REWRITE_TAC[differentiable_on] THEN
817 ASM_MESON_TAC[DIFFERENTIABLE_TRANSFORM_WITHIN, REAL_LT_01]
818QED
819
820(* ------------------------------------------------------------------------- *)
821(* Frechet derivative and Jacobian matrix. *)
822(* ------------------------------------------------------------------------- *)
823
824Definition frechet_derivative[nocompute]:
825 frechet_derivative f net = @f'. (f has_derivative f') net
826End
827
828Theorem FRECHET_DERIVATIVE_WORKS:
829 !f net. f differentiable net <=>
830 (f has_derivative (frechet_derivative f net)) net
831Proof
832 REPEAT GEN_TAC THEN REWRITE_TAC[frechet_derivative] THEN
833 CONV_TAC(RAND_CONV SELECT_CONV) THEN REWRITE_TAC[differentiable]
834QED
835
836Theorem LINEAR_FRECHET_DERIVATIVE:
837 !f net. f differentiable net ==> linear(frechet_derivative f net)
838Proof
839 SIMP_TAC std_ss [FRECHET_DERIVATIVE_WORKS, has_derivative]
840QED
841
842(* ------------------------------------------------------------------------- *)
843(* Differentiability implies continuity. 377 *)
844(* ------------------------------------------------------------------------- *)
845
846Theorem LIM_MUL_ABS_WITHIN:
847 !f a s. (f --> 0) (at a within s)
848 ==> ((\x. abs(x - a) * f(x)) --> 0) (at a within s)
849Proof
850 REPEAT GEN_TAC THEN REWRITE_TAC[LIM_WITHIN] THEN
851 DISCH_TAC THEN GEN_TAC THEN POP_ASSUM (MP_TAC o Q.SPEC `e:real`) THEN
852 ASM_CASES_TAC ``&0 < e:real`` THEN ASM_REWRITE_TAC[dist, REAL_SUB_RZERO] THEN
853 DISCH_THEN(X_CHOOSE_THEN ``d:real`` STRIP_ASSUME_TAC) THEN
854 EXISTS_TAC ``min d (&1:real)`` THEN ASM_REWRITE_TAC[REAL_LT_MIN, REAL_LT_01] THEN
855 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [ABS_MUL, ABS_ABS] THEN
856 GEN_REWR_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
857 ASM_SIMP_TAC std_ss [REAL_LT_MUL2, ABS_POS]
858QED
859
860Theorem DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN :
861 !f:real->real x s.
862 f differentiable (at x within s) ==> f continuous (at x within s)
863Proof
864 REWRITE_TAC[differentiable, has_derivative_within, CONTINUOUS_WITHIN] THEN
865 REPEAT GEN_TAC THEN
866 DISCH_THEN(X_CHOOSE_THEN ``f':real->real`` MP_TAC) THEN
867 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP LIM_MUL_ABS_WITHIN) THEN
868 SUBGOAL_THEN
869 ``((f':real->real) o (\y. y - x)) continuous (at x within s)``
870 MP_TAC THENL
871 [MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN
872 ASM_SIMP_TAC std_ss [LINEAR_CONTINUOUS_WITHIN] THEN
873 SIMP_TAC std_ss [CONTINUOUS_SUB, CONTINUOUS_CONST, CONTINUOUS_WITHIN_ID],
874 ALL_TAC] THEN
875 SIMP_TAC std_ss [CONTINUOUS_WITHIN, o_DEF] THEN
876 ASM_REWRITE_TAC[REAL_MUL_ASSOC, AND_IMP_INTRO, IN_UNIV] THEN
877 DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN
878 SIMP_TAC std_ss [LIM_WITHIN, GSYM DIST_NZ, REAL_MUL_RINV, ABS_ZERO,
879 REAL_ARITH ``(x - y = 0) <=> (x = y:real)``,
880 REAL_MUL_LID, REAL_SUB_REFL] THEN
881 FIRST_ASSUM(SUBST1_TAC o MATCH_MP LINEAR_0) THEN
882 REWRITE_TAC[dist, REAL_SUB_RZERO, REAL_ADD_ASSOC] THEN
883 SIMP_TAC std_ss [REAL_ARITH ``(a + (b - (c + a))) - (0 + 0) = b - c:real``]
884QED
885
886Theorem DIFFERENTIABLE_IMP_CONTINUOUS_AT:
887 !f:real->real x. f differentiable (at x) ==> f continuous (at x)
888Proof
889 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
890 REWRITE_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]
891QED
892
893Theorem DIFFERENTIABLE_IMP_CONTINUOUS_ON:
894 !f:real->real s. f differentiable_on s ==> f continuous_on s
895Proof
896 SIMP_TAC std_ss [differentiable_on, CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN,
897 DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]
898QED
899
900Theorem HAS_DERIVATIVE_WITHIN_SUBSET :
901 !f f' s t x. (f has_derivative f') (at x within s) /\ t SUBSET s
902 ==> (f has_derivative f') (at x within t)
903Proof
904 REWRITE_TAC[has_derivative_within] THEN MESON_TAC[LIM_WITHIN_SUBSET]
905QED
906
907Theorem DIFFERENTIABLE_WITHIN_SUBSET :
908 !f:real->real s t x.
909 f differentiable (at x within t) /\ s SUBSET t
910 ==> f differentiable (at x within s)
911Proof
912 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_WITHIN_SUBSET]
913QED
914
915Theorem DIFFERENTIABLE_ON_SUBSET:
916 !f:real->real s t.
917 f differentiable_on t /\ s SUBSET t ==> f differentiable_on s
918Proof
919 REWRITE_TAC[differentiable_on] THEN
920 MESON_TAC[SUBSET_DEF, DIFFERENTIABLE_WITHIN_SUBSET]
921QED
922
923Theorem DIFFERENTIABLE_ON_EMPTY:
924 !f. f differentiable_on {}
925Proof
926 REWRITE_TAC[differentiable_on, NOT_IN_EMPTY]
927QED
928
929(* ------------------------------------------------------------------------- *)
930(* Several results are easier using a "multiplied-out" variant. *)
931(* (I got this idea from Dieudonne's proof of the chain rule). *)
932(* ------------------------------------------------------------------------- *)
933
934Theorem HAS_DERIVATIVE_WITHIN_ALT:
935 !f:real->real f' s x.
936 (f has_derivative f') (at x within s) <=>
937 linear f' /\
938 !e. &0 < e
939 ==> ?d. &0 < d /\
940 !y. y IN s /\ abs(y - x) < d
941 ==> abs(f(y) - f(x) - f'(y - x)) <=
942 e * abs(y - x)
943Proof
944 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative_within, LIM_WITHIN] THEN
945 ASM_REWRITE_TAC[dist, REAL_SUB_RZERO] THEN
946 ASM_CASES_TAC ``linear(f':real->real)`` THEN
947 ASM_REWRITE_TAC [ABS_MUL, ABS_INV, ABS_ABS] THEN
948 GEN_REWR_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
949 SIMP_TAC std_ss [GSYM real_div, REAL_LT_LDIV_EQ] THEN
950 REWRITE_TAC[REAL_ARITH ``a - (b + c) = a - b - c :real``] THEN
951 EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC ``e:real`` THEN DISCH_TAC THENL
952 [FIRST_X_ASSUM(MP_TAC o SPEC ``e:real``) THEN ASM_REWRITE_TAC[] THEN
953 STRIP_TAC THEN EXISTS_TAC ``d:real`` THEN
954 ASM_REWRITE_TAC[] THEN X_GEN_TAC ``y:real`` THEN DISCH_TAC THEN
955 ASM_CASES_TAC ``&0 < abs(y - x :real)`` THENL
956 [ASM_SIMP_TAC std_ss [GSYM REAL_LE_LDIV_EQ] THEN
957 FULL_SIMP_TAC std_ss [REAL_LT_IMP_NE, REAL_LE_LT, ABS_DIV, ABS_ABS],
958 ALL_TAC] THEN
959 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [GSYM ABS_NZ]) THEN
960 ASM_SIMP_TAC std_ss [REAL_SUB_0, REAL_SUB_REFL, ABS_0, REAL_MUL_RZERO,
961 REAL_ARITH ``0 - x = -x:real``, ABS_NEG] THEN
962 ASM_MESON_TAC[LINEAR_0, ABS_0, REAL_LE_REFL],
963 FIRST_X_ASSUM(MP_TAC o SPEC ``e / &2:real``) THEN
964 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT] THEN
965 STRIP_TAC THEN EXISTS_TAC ``d:real`` THEN
966 ASM_REWRITE_TAC[] THEN X_GEN_TAC ``y:real`` THEN STRIP_TAC THEN
967 ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE, ABS_DIV, ABS_ABS, REAL_LT_LDIV_EQ] THEN
968 MATCH_MP_TAC REAL_LET_TRANS THEN
969 EXISTS_TAC ``e / &2 * abs(y - x :real)`` THEN
970 ASM_SIMP_TAC arith_ss [REAL_LT_RMUL, REAL_LT_LDIV_EQ, REAL_LT] THEN
971 UNDISCH_TAC ``&0 < e:real`` THEN REAL_ARITH_TAC]
972QED
973
974Theorem HAS_DERIVATIVE_AT_ALT:
975 !f:real->real f' x.
976 (f has_derivative f') (at x) <=>
977 linear f' /\
978 !e. &0 < e
979 ==> ?d. &0 < d /\
980 !y. abs(y - x) < d
981 ==> abs(f(y) - f(x) - f'(y - x)) <= e * abs(y - x)
982Proof
983 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
984 REWRITE_TAC[HAS_DERIVATIVE_WITHIN_ALT, IN_UNIV]
985QED
986
987(* ------------------------------------------------------------------------- *)
988(* The chain rule. 499 *)
989(* ------------------------------------------------------------------------- *)
990
991Theorem DIFF_CHAIN_WITHIN:
992 !f:real->real g:real->real f' g' x s.
993 (f has_derivative f') (at x within s) /\
994 (g has_derivative g') (at (f x) within (IMAGE f s))
995 ==> ((g o f) has_derivative (g' o f'))(at x within s)
996Proof
997 REPEAT GEN_TAC THEN SIMP_TAC std_ss [HAS_DERIVATIVE_WITHIN_ALT, LINEAR_COMPOSE] THEN
998 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
999 FIRST_ASSUM(X_CHOOSE_TAC ``B1:real`` o MATCH_MP LINEAR_BOUNDED_POS) THEN
1000 DISCH_THEN(fn th => X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN MP_TAC th) THEN
1001 DISCH_THEN(CONJUNCTS_THEN2
1002 (fn th => ASSUME_TAC th THEN X_CHOOSE_TAC ``B2:real`` (MATCH_MP
1003 LINEAR_BOUNDED_POS th)) MP_TAC) THEN
1004 FIRST_X_ASSUM(fn th => MP_TAC th THEN MP_TAC(Q.SPEC `e / &2 / B2` th)) THEN
1005 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT] THEN
1006 DISCH_THEN(X_CHOOSE_THEN ``d1:real`` STRIP_ASSUME_TAC) THEN DISCH_TAC THEN
1007 DISCH_THEN(MP_TAC o Q.SPEC `e / &2 / (&1 + B1)`) THEN
1008 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT, REAL_LT_ADD] THEN
1009 DISCH_THEN(X_CHOOSE_THEN ``de:real`` STRIP_ASSUME_TAC) THEN
1010 UNDISCH_TAC ``!e:real. 0 < e ==>
1011 ?d. 0 < d /\
1012 !y. y IN s /\ abs (y - x) < d ==>
1013 abs (f y - f x - f' (y - x)) <= e * abs (y - x)`` THEN
1014 DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o Q.SPEC `&1`) THEN
1015 REWRITE_TAC[REAL_LT_01, REAL_MUL_LID] THEN
1016 DISCH_THEN(X_CHOOSE_THEN ``d2:real`` STRIP_ASSUME_TAC) THEN
1017 MP_TAC(SPECL [``d1:real``, ``d2:real``] REAL_DOWN2) THEN
1018 ASM_SIMP_TAC std_ss [REAL_LT_DIV, REAL_LT_ADD, REAL_LT_01] THEN
1019 DISCH_THEN(X_CHOOSE_THEN ``d0:real`` STRIP_ASSUME_TAC) THEN
1020 MP_TAC(SPECL [``d0:real``, ``de / (B1 + &1:real)``] REAL_DOWN2) THEN
1021 ASM_SIMP_TAC std_ss [REAL_LT_DIV, REAL_LT_ADD, REAL_LT_01] THEN
1022 DISCH_THEN (X_CHOOSE_TAC ``d:real``) THEN Q.EXISTS_TAC `d` THEN
1023 POP_ASSUM MP_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1024 X_GEN_TAC ``y:real`` THEN DISCH_TAC THEN UNDISCH_TAC
1025 ``!y. y IN s /\ abs(y - x) < d2
1026 ==> abs((f:real->real) y - f x - f'(y - x)) <= abs(y - x)`` THEN
1027 DISCH_THEN(MP_TAC o SPEC ``y:real``) THEN
1028 Q_TAC SUFF_TAC `y IN s /\ abs (y - x) < d2` THENL
1029 [DISCH_TAC, ASM_MESON_TAC[REAL_LT_TRANS]] THEN
1030 ASM_REWRITE_TAC [] THEN DISCH_TAC THEN
1031 UNDISCH_TAC ``!y. y IN s /\ abs (y - x) < d1 ==>
1032 abs (f y - f x - f' (y - x)) <= e / 2 / B2 * abs (y - x:real)`` THEN
1033 DISCH_THEN(MP_TAC o SPEC ``y:real``) THEN
1034 Q_TAC SUFF_TAC `y IN s /\ abs (y - x) < d1` THENL
1035 [DISCH_TAC, ASM_MESON_TAC[REAL_LT_TRANS]] THEN
1036 ASM_REWRITE_TAC [] THEN DISCH_TAC THEN
1037 FIRST_X_ASSUM(MP_TAC o SPEC ``(f:real->real) y``) THEN
1038 ASM_SIMP_TAC std_ss [] THEN
1039 Q_TAC SUFF_TAC `f y IN IMAGE f s /\ abs (f y - f x) < de` THENL
1040 [DISCH_TAC,
1041 CONJ_TAC THENL [ASM_MESON_TAC[IN_IMAGE], ALL_TAC] THEN
1042 MATCH_MP_TAC REAL_LET_TRANS THEN Q.EXISTS_TAC
1043 `abs(f'(y - x)) + abs((f:real->real) y - f x - f'(y - x))` THEN
1044 REWRITE_TAC[ABS_TRIANGLE_SUB] THEN
1045 MATCH_MP_TAC REAL_LET_TRANS THEN
1046 EXISTS_TAC ``B1 * abs(y - x) + abs(y - x :real)`` THEN
1047 ASM_SIMP_TAC real_ss [REAL_LE_ADD2] THEN
1048 REWRITE_TAC[REAL_ARITH ``a * x + x = x * (a + &1:real)``] THEN
1049 ASM_SIMP_TAC real_ss [GSYM REAL_LT_RDIV_EQ, REAL_LT_ADD, REAL_LT_01] THEN
1050 ASM_MESON_TAC[REAL_LT_TRANS]] THEN
1051 ASM_REWRITE_TAC [] THEN DISCH_TAC THEN
1052 REWRITE_TAC[o_THM] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1053 Q.EXISTS_TAC `abs((g:real->real)(f(y:real)) - g(f x) - g'(f y - f x)) +
1054 abs((g(f y) - g(f x) - g'(f'(y - x))) -
1055 (g(f y) - g(f x) - g'(f y - f x)))` THEN
1056 REWRITE_TAC[ABS_TRIANGLE_SUB] THEN
1057 REWRITE_TAC[REAL_ARITH ``(a - b - c1) - (a - b - c2) = c2 - c1:real``] THEN
1058 ASM_SIMP_TAC std_ss [GSYM LINEAR_SUB] THEN
1059 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
1060 ``a <= d ==> b <= ee - d ==> a + b <= ee:real``)) THEN
1061 MATCH_MP_TAC REAL_LE_TRANS THEN
1062 Q.EXISTS_TAC `B2 * abs((f:real->real) y - f x - f'(y - x))` THEN
1063 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1064 Q.EXISTS_TAC `B2 * e / &2 / B2 * abs(y - x :real)` THEN
1065 CONJ_TAC THENL
1066 [SIMP_TAC std_ss [real_div] THEN
1067 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d * e = a * ((b * c * d) * e:real)``] THEN
1068 MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_SIMP_TAC std_ss [GSYM real_div, REAL_LE_REFL] THEN
1069 ASM_SIMP_TAC std_ss [REAL_LT_IMP_LE, ABS_POS],
1070 ALL_TAC] THEN
1071 ASM_SIMP_TAC real_ss [REAL_LE_LMUL, REAL_LT_IMP_LE] THEN REWRITE_TAC[real_div] THEN
1072 ONCE_REWRITE_TAC[REAL_ARITH
1073 ``b * e * h * b' * x <= e * x - d <=>
1074 d <= e * (&1 - h * (b' * b)) * x:real``] THEN
1075 ASM_SIMP_TAC real_ss [REAL_MUL_LINV, REAL_LT_IMP_NE] THEN
1076 SIMP_TAC real_ss [ONE_MINUS_HALF, REAL_INV_1OVER] THEN
1077 REWRITE_TAC[GSYM REAL_MUL_ASSOC, GSYM REAL_INV_1OVER] THEN
1078 ASM_SIMP_TAC arith_ss [REAL_LE_LMUL, REAL_LT_DIV, REAL_LT] THEN
1079 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN
1080 ASM_SIMP_TAC real_ss [REAL_LE_LDIV_EQ, REAL_LT_ADD, REAL_LT_01] THEN
1081 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN
1082 ASM_SIMP_TAC real_ss [REAL_LE_LDIV_EQ, REAL_LT_ADD, REAL_LT_01] THEN
1083 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
1084 ``abs(f'(y - x)) + abs((f:real->real) y - f x - f'(y - x))`` THEN
1085 REWRITE_TAC[ABS_TRIANGLE_SUB] THEN SIMP_TAC real_ss [real_div, REAL_MUL_ASSOC] THEN
1086 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = (c * a) * b * d:real``] THEN
1087 SIMP_TAC real_ss [REAL_MUL_LINV] THEN MATCH_MP_TAC(REAL_ARITH
1088 ``u <= x * b /\ v <= b ==> u + v <= b * (&1 + x:real)``) THEN
1089 ASM_REWRITE_TAC[]
1090QED
1091
1092(* ------------------------------------------------------------------------- *)
1093(* Component of the differential must be zero if it exists at a local *)
1094(* maximum or minimum for that corresponding component. Start with slightly *)
1095(* sharper forms that fix the sign of the derivative on the boundary. *)
1096(* ------------------------------------------------------------------------- *)
1097
1098Theorem DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM :
1099 !f:real->real f' x s e.
1100 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\
1101 &0 < e /\ (!w. w IN s INTER ball(x,e) ==> (f x) <= (f w))
1102 ==> !y. y IN s ==> &0 <= (f'(y - x))
1103Proof
1104 REWRITE_TAC[has_derivative_within] THEN REPEAT STRIP_TAC THEN
1105 ASM_CASES_TAC ``y:real = x`` THENL
1106 [ASM_MESON_TAC[REAL_SUB_REFL, LINEAR_0, REAL_LE_REFL],
1107 ALL_TAC] THEN
1108 ONCE_REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN
1109 UNDISCH_TAC ``((\y. inv (abs (y - x)) * (f y - (f x + f' (y - x)))) --> 0)
1110 (at x within s)`` THEN REWRITE_TAC [LIM_WITHIN] THEN
1111 DISCH_THEN(MP_TAC o Q.SPEC `-((f':real->real)(y - x)) / abs(y - x)`) THEN
1112 ASM_SIMP_TAC real_ss [REAL_LT_DIV, GSYM ABS_NZ, real_sub,
1113 NOT_EXISTS_THM, REAL_ARITH ``&0 < -x <=> x < &0:real``] THEN
1114 CONJ_TAC THENL
1115 [ONCE_REWRITE_TAC [GSYM REAL_LT_NEG] THEN SIMP_TAC real_ss [REAL_NEG_0, real_div] THEN
1116 SIMP_TAC std_ss [GSYM real_sub, GSYM real_div] THEN
1117 Q_TAC SUFF_TAC `0 < abs (y - x:real)` THENL
1118 [DISCH_TAC,
1119 REWRITE_TAC [GSYM ABS_NZ] THEN POP_ASSUM MP_TAC THEN
1120 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN
1121 ASM_SIMP_TAC real_ss [REAL_LT_LDIV_EQ],
1122 ALL_TAC] THEN
1123 X_GEN_TAC ``d:real`` THEN CCONTR_TAC THEN FULL_SIMP_TAC std_ss [] THEN
1124 Q.ABBREV_TAC `de = min (&1) ((min d e) / &2 / abs(y - x:real))` THEN
1125 FIRST_X_ASSUM (MP_TAC o Q.SPEC `x + de * (y - x):real`) THEN
1126 SIMP_TAC real_ss [dist, REAL_ADD_SUB, NOT_IMP, GSYM CONJ_ASSOC] THEN
1127 SUBGOAL_THEN ``abs(de * (y - x):real) < min d e`` MP_TAC THENL
1128 [ASM_SIMP_TAC real_ss [ABS_MUL, GSYM REAL_LT_RDIV_EQ,
1129 ABS_POS, real_sub] THEN
1130 Q.UNABBREV_TAC `de` THEN SIMP_TAC real_ss [real_div, REAL_MUL_ASSOC] THEN
1131 SIMP_TAC std_ss [min_def] THEN REPEAT COND_CASES_TAC THENL
1132 [FULL_SIMP_TAC real_ss [GSYM real_sub] THEN MATCH_MP_TAC REAL_LET_TRANS THEN
1133 Q.EXISTS_TAC `d / 2` THEN ASM_SIMP_TAC std_ss [REAL_LT_HALF2] THEN
1134 Q_TAC SUFF_TAC `0 < abs (y - x:real)` THENL
1135 [DISCH_TAC, REWRITE_TAC [GSYM ABS_NZ] THEN
1136 UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC] THEN
1137 GEN_REWR_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN
1138 ASM_SIMP_TAC real_ss [GSYM REAL_LE_RDIV_EQ, real_div],
1139 FULL_SIMP_TAC real_ss [GSYM real_sub] THEN MATCH_MP_TAC REAL_LET_TRANS THEN
1140 Q.EXISTS_TAC `e / 2` THEN ASM_SIMP_TAC std_ss [REAL_LT_HALF2] THEN
1141 Q_TAC SUFF_TAC `0 < abs (y - x:real)` THENL
1142 [DISCH_TAC, REWRITE_TAC [GSYM ABS_NZ] THEN
1143 UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC] THEN
1144 GEN_REWR_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN
1145 ASM_SIMP_TAC real_ss [GSYM REAL_LE_RDIV_EQ, real_div],
1146 SIMP_TAC real_ss [ABS_MUL] THEN
1147 `y - x <> 0` by (UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC) THEN
1148 ASM_SIMP_TAC std_ss [GSYM ABS_INV, ABS_ABS] THEN
1149 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = (a * b) * (c * d:real)``] THEN
1150 ASM_SIMP_TAC real_ss [GSYM ABS_MUL, REAL_MUL_LINV, GSYM real_sub] THEN
1151 SIMP_TAC real_ss [GSYM real_div] THEN Q_TAC SUFF_TAC `abs (d / 2) = d / 2` THENL
1152 [ASM_SIMP_TAC real_ss [REAL_LT_HALF2], ALL_TAC] THEN
1153 ASM_SIMP_TAC real_ss [ABS_REFL, REAL_LE_RDIV_EQ, REAL_LE_LT],
1154 ALL_TAC] THEN
1155 SIMP_TAC real_ss [ABS_MUL] THEN
1156 `y - x <> 0` by (UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC) THEN
1157 ASM_SIMP_TAC std_ss [GSYM ABS_INV, ABS_ABS] THEN
1158 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = (a * b) * (c * d:real)``] THEN
1159 ASM_SIMP_TAC real_ss [GSYM ABS_MUL, REAL_MUL_LINV, GSYM real_sub] THEN
1160 SIMP_TAC std_ss [GSYM real_div] THEN Q_TAC SUFF_TAC `abs (e / 2) = e / 2` THENL
1161 [ASM_SIMP_TAC real_ss [REAL_LT_HALF2], ALL_TAC] THEN
1162 ASM_SIMP_TAC real_ss [ABS_REFL, REAL_LE_RDIV_EQ, REAL_LE_LT],
1163 ALL_TAC] THEN
1164 REWRITE_TAC[REAL_LT_MIN] THEN STRIP_TAC THEN
1165 SUBGOAL_THEN ``&0 < de /\ de <= &1:real`` STRIP_ASSUME_TAC THENL
1166 [Q.UNABBREV_TAC `de` THEN CONJ_TAC THENL [ALL_TAC, SIMP_TAC std_ss [REAL_MIN_LE1]] THEN
1167 ASM_SIMP_TAC real_ss [REAL_LT_MIN, REAL_LT_01, REAL_HALF, REAL_LT_DIV, ABS_NZ, real_sub] THEN
1168 SIMP_TAC real_ss [real_div, min_def] THEN
1169 Q_TAC SUFF_TAC `0 < abs (y - x:real)` THENL
1170 [DISCH_TAC, REWRITE_TAC [GSYM ABS_NZ] THEN
1171 UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC] THEN COND_CASES_TAC THENL
1172 [ASM_SIMP_TAC std_ss [REAL_LT_RDIV_EQ, GSYM real_div, GSYM real_sub] THEN
1173 ASM_SIMP_TAC real_ss [REAL_LT_HALF2],
1174 ALL_TAC] THEN
1175 ASM_SIMP_TAC std_ss [REAL_LT_RDIV_EQ, GSYM real_div, GSYM real_sub] THEN
1176 ASM_SIMP_TAC real_ss [REAL_LT_HALF2],
1177 ALL_TAC] THEN
1178 MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
1179 [REWRITE_TAC[REAL_ARITH
1180 ``x + a * (y - x):real = (&1 - a) * x + a * y``] THEN
1181 MATCH_MP_TAC IN_CONVEX_SET THEN ASM_SIMP_TAC real_ss [REAL_LT_IMP_LE],
1182 DISCH_TAC] THEN
1183 CONJ_TAC THENL
1184 [SIMP_TAC std_ss [ABS_MUL] THEN MATCH_MP_TAC REAL_LT_MUL THEN
1185 UNDISCH_TAC ``0 < de:real`` THEN UNDISCH_TAC ``y <> x:real`` THEN
1186 REAL_ARITH_TAC, ALL_TAC] THEN ASM_REWRITE_TAC[] THEN
1187 SIMP_TAC std_ss [REAL_NOT_LT, ABS_MUL] THEN
1188 ONCE_REWRITE_TAC [REAL_ARITH ``a + b + -a = b:real``] THEN
1189 Q_TAC SUFF_TAC `abs (de * (y - x)) <> 0` THENL
1190 [DISCH_TAC, SIMP_TAC std_ss [ABS_MUL] THEN
1191 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN
1192 MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC real_ss [GSYM ABS_NZ] THEN
1193 ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE] THEN UNDISCH_TAC ``y <> x:real`` THEN
1194 REAL_ARITH_TAC] THEN
1195 ASM_SIMP_TAC std_ss [ABS_INV, ABS_ABS] THEN
1196 `y - x <> 0` by (UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC) THEN
1197 `0 < abs (y - x)` by (ASM_SIMP_TAC std_ss [GSYM ABS_NZ]) THEN
1198 ASM_SIMP_TAC std_ss [REAL_LE_LDIV_EQ, GSYM real_sub] THEN
1199 `abs (y - x) <> 0` by ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE] THEN
1200 `de <> 0` by (ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE]) THEN
1201 `0 < abs (de)` by (ASM_SIMP_TAC std_ss [GSYM ABS_NZ]) THEN
1202 `abs (de) <> 0` by ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE] THEN
1203 ASM_SIMP_TAC real_ss [REAL_INV_MUL, ABS_MUL] THEN
1204 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = (a * c) * (b * d:real)``] THEN
1205 ASM_SIMP_TAC real_ss [REAL_MUL_LINV] THEN
1206 Q_TAC SUFF_TAC `x + de * (y - x) IN ball (x,e)` THENL
1207 [DISCH_TAC, SIMP_TAC real_ss [IN_BALL, dist] THEN
1208 UNDISCH_TAC ``abs (de * (y - x)) < e:real`` THEN REAL_ARITH_TAC] THEN
1209 `f x <= f (x + de * (y - x))` by METIS_TAC [IN_INTER] THEN
1210 Q_TAC SUFF_TAC `abs (f (x + de * (y - x)) - (f x + f' (de * (y - x)))) =
1211 (f (x + de * (y - x)) - (f x + f' (de * (y - x))))` THENL
1212 [DISC_RW_KILL,
1213 REWRITE_TAC [ABS_REFL] THEN
1214 ONCE_REWRITE_TAC [REAL_ARITH ``a - (b + c) = (a - b) + -c:real``] THEN
1215 MATCH_MP_TAC REAL_LE_ADD THEN
1216 ASM_SIMP_TAC real_ss [REAL_ARITH ``a <= b ==> 0 <= b - a:real``] THEN
1217 ASM_SIMP_TAC real_ss [LINEAR_CMUL] THEN
1218 ONCE_REWRITE_TAC [REAL_ARITH ``-(a * b) = a * -b:real``] THEN
1219 MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC std_ss [REAL_LE_LT] THEN
1220 ONCE_REWRITE_TAC [GSYM REAL_LT_NEG] THEN ASM_SIMP_TAC real_ss []] THEN
1221 ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN REWRITE_TAC [GSYM real_div] THEN
1222 ASM_SIMP_TAC real_ss [REAL_LE_RDIV_EQ] THEN ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN
1223 `0 <= de` by ASM_SIMP_TAC real_ss [REAL_LE_LT] THEN
1224 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [GSYM ABS_REFL]) THEN
1225 ASM_SIMP_TAC real_ss [GSYM LINEAR_CMUL] THEN
1226 GEN_REWR_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_COMM] THEN
1227 ONCE_REWRITE_TAC [REAL_ARITH ``-a <= b - (c + a) <=> c <= b:real``] THEN
1228 METIS_TAC [REAL_MUL_COMM]
1229QED
1230
1231Theorem DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM:
1232 !f:real->real f' x s e.
1233 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\
1234 &0 < e /\ (!w. w IN s INTER ball(x,e) ==> (f w) <= (f x))
1235 ==> !y. y IN s ==> (f'(y - x)) <= &0
1236Proof
1237 REPEAT STRIP_TAC THEN
1238 MP_TAC(ISPECL [
1239 ``\x. -((f:real->real) x)``, ``\x. -((f':real->real) x)``,
1240 ``x:real``, ``s:real->bool``, ``e:real``]
1241 DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM) THEN
1242 ASM_SIMP_TAC real_ss [HAS_DERIVATIVE_NEG] THEN
1243 ASM_SIMP_TAC real_ss [REAL_LE_NEG2, REAL_NEG_GE0]
1244QED
1245
1246Theorem CONVEX_CBALL:
1247 !x:real e. convex(cball(x,e))
1248Proof
1249 REWRITE_TAC[convex, IN_CBALL, dist] THEN MAP_EVERY X_GEN_TAC
1250 [``x:real``, ``e:real``, ``y:real``, ``z:real``, ``u:real``, ``v:real``] THEN
1251 STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH ``a - b = &1 * a - b:real``] THEN
1252 FIRST_ASSUM(SUBST1_TAC o SYM) THEN
1253 REWRITE_TAC[REAL_ARITH
1254 ``(a + b) * x - (a * y + b * z) = a * (x - y) + b * (x - z:real)``] THEN
1255 MATCH_MP_TAC REAL_LE_TRANS THEN
1256 EXISTS_TAC ``abs(u * (x - y)) + abs(v * (x - z):real)`` THEN
1257 REWRITE_TAC[ABS_TRIANGLE, ABS_MUL] THEN
1258 MATCH_MP_TAC REAL_CONVEX_BOUND_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS] THEN
1259 ASM_SIMP_TAC real_ss [REAL_ARITH
1260 ``&0 <= u /\ &0 <= v /\ (u + v = &1) ==> (abs(u) + abs(v) = &1:real)``]
1261QED
1262
1263Theorem DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN :
1264 !f:real->real f' x s.
1265 x IN s /\ open s /\ (f has_derivative f') (at x) /\
1266 ((!w. w IN s ==> (f w) <= (f x)) \/
1267 (!w. w IN s ==> (f x) <= (f w))) ==> !h. (f' h) = &0
1268Proof
1269 rpt GEN_TAC
1270 >> DISCH_THEN (REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC)
1271 >> Q.PAT_ASSUM `open s`
1272 (MP_TAC o ONCE_REWRITE_RULE [OPEN_CONTAINS_CBALL])
1273 >> DISCH_THEN(MP_TAC o Q.SPEC `x:real`) >> art [SUBSET_DEF]
1274 >> DISCH_THEN(X_CHOOSE_THEN ``e:real`` STRIP_ASSUME_TAC)
1275 >> FIRST_X_ASSUM DISJ_CASES_TAC (* 2 subgoals, shared tactics *)
1276 >| [ MP_TAC (Q.SPECL [`f`, `f'`, `x`, `cball(x:real,e)`, `e`]
1277 DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM),
1278 MP_TAC (Q.SPECL [`f`, `f'`, `x`, `cball(x:real,e)`, `e`]
1279 DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM) ] (* 2 subgoals *)
1280 >> ASM_SIMP_TAC real_ss [HAS_DERIVATIVE_AT_WITHIN, CENTRE_IN_CBALL,
1281 CONVEX_CBALL, REAL_LT_IMP_LE, IN_INTER]
1282 >> DISCH_TAC THEN X_GEN_TAC ``h:real``
1283 >> Q.PAT_X_ASSUM `(f has_derivative f') (at x)`
1284 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [has_derivative_at]))
1285 >> (Cases_on `h:real = 0` >- ASM_MESON_TAC [LINEAR_0])
1286 >> Q.PAT_X_ASSUM `!y. y IN cball (x,e) ==> _`
1287 (fn th => MP_TAC (Q.SPEC `x + e / abs h * h:real` th) \\
1288 MP_TAC (Q.SPEC `x - e / abs h * h:real` th))
1289 >> SIMP_TAC real_ss [IN_CBALL, dist, REAL_ARITH
1290 ``(abs(x:real - (x - e)) = abs e) /\ (abs(x:real - (x + e)) = abs e)``,
1291 REAL_ARITH ``x - e / abs h * h - x = -(e / abs h * h):real``]
1292 >> FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP LINEAR_NEG th])
1293 >| [ ONCE_REWRITE_TAC [METIS [REAL_LE_NEG] ``-e <= 0 <=> -0 <= --e:real``],
1294 ONCE_REWRITE_TAC [METIS [REAL_LE_NEG] ``0 <= -e <=> --e <= -0:real``] ]
1295 >> SIMP_TAC std_ss [REAL_NEG_NEG, REAL_NEG_0]
1296 (* stage work, right-associative from now on *)
1297 >> (Know `abs (e / abs h * h) <= e`
1298 >- (Cases_on `0 <= h` (* 2 subgoals, same tactics *)
1299 >- (REWRITE_TAC [real_div, REAL_ARITH ``a * b * c = a * (b * c:real)``] \\
1300 FULL_SIMP_TAC real_ss [abs, REAL_MUL_LINV, GSYM REAL_NEG_INV,
1301 REAL_ARITH ``-a * b = -(a * b:real)``] \\
1302 `0 <= e` by PROVE_TAC [REAL_LT_IMP_LE] >> rw []) \\
1303 REWRITE_TAC [real_div, REAL_ARITH ``a * b * c = a * (b * c:real)``] \\
1304 FULL_SIMP_TAC real_ss [abs, REAL_MUL_LINV, GSYM REAL_NEG_INV,
1305 REAL_ARITH ``-a * b = -(a * b:real)``] \\
1306 ONCE_REWRITE_TAC [METIS [REAL_LE_NEG] ``0 <= -e <=> --e <= -0:real``] \\
1307 SIMP_TAC std_ss [REAL_NEG_NEG, REAL_NEG_0] \\
1308 `~(e <= 0)` by PROVE_TAC [real_lte] >> rw []) \\
1309 RW_TAC std_ss [] \\
1310 `f' (e / abs h * h) = 0` by METIS_TAC [REAL_LE_ANTISYM] \\
1311 POP_ASSUM MP_TAC >> ASM_SIMP_TAC std_ss [LINEAR_CMUL] \\
1312 ASM_SIMP_TAC std_ss [REAL_ENTIRE] \\
1313 Suff `e / abs h <> 0` >- rw [] \\
1314 ONCE_REWRITE_TAC [EQ_SYM_EQ] \\
1315 MATCH_MP_TAC REAL_LT_IMP_NE \\
1316 MATCH_MP_TAC REAL_LT_DIV \\
1317 ASM_SIMP_TAC std_ss [GSYM ABS_NZ])
1318QED
1319
1320Theorem DIFFERENTIAL_ZERO_MAXMIN :
1321 !f:real->real f' x s.
1322 x IN s /\ open s /\ (f has_derivative f') (at x) /\
1323 ((!y. y IN s ==> (f y) <= (f x)) \/
1324 (!y. y IN s ==> (f x) <= (f y)))
1325 ==> (f' = \v. 0)
1326Proof
1327 rpt STRIP_TAC
1328 >> MP_TAC (ISPECL [``f:real->real``, ``f':real->real``,
1329 ``x:real``, ``s:real->bool``]
1330 DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN)
1331 >> ASM_SIMP_TAC real_ss [FUN_EQ_THM, REAL_LE_REFL]
1332QED
1333
1334(* ------------------------------------------------------------------------- *)
1335(* The traditional Rolle theorem in one dimension. 1056 *)
1336(* ------------------------------------------------------------------------- *)
1337
1338Theorem ROLLE:
1339 !f:real->real f' a b.
1340 a < b /\ (f a = f b) /\
1341 f continuous_on interval[a,b] /\
1342 (!x. x IN interval(a,b) ==> (f has_derivative f'(x)) (at x))
1343 ==> ?x. x IN interval(a,b) /\ (f'(x) = \v. 0)
1344Proof
1345 REPEAT STRIP_TAC THEN
1346 SUBGOAL_THEN
1347 ``?x. x:real IN interval(a,b) /\
1348 ((!y. y IN interval(a,b) ==> (f x):real <= (f y)) \/
1349 (!y. y IN interval(a,b) ==> (f y):real <= (f x)))``
1350 MP_TAC THENL
1351 [ALL_TAC, METIS_TAC[DIFFERENTIAL_ZERO_MAXMIN, OPEN_INTERVAL]] THEN
1352 MAP_EVERY (MP_TAC o ISPECL
1353 [``(f:real->real)``, ``interval[a:real,b]``])
1354 [CONTINUOUS_ATTAINS_SUP, CONTINUOUS_ATTAINS_INF] THEN
1355 REWRITE_TAC[COMPACT_INTERVAL, o_ASSOC] THEN
1356 ASM_SIMP_TAC real_ss [CONTINUOUS_ON_COMPOSE, CONTINUOUS_ON_ID, o_DEF] THEN
1357 REWRITE_TAC[GSYM INTERVAL_EQ_EMPTY, CONJ_ASSOC, REAL_LE_ANTISYM] THEN
1358 ASM_SIMP_TAC real_ss [UNWIND_THM1, REAL_NOT_LT, REAL_LT_IMP_LE] THEN
1359 DISCH_THEN(X_CHOOSE_THEN ``d:real`` STRIP_ASSUME_TAC) THEN
1360 ASM_CASES_TAC ``(d:real) IN interval(a,b)`` THENL
1361 [ASM_MESON_TAC[SUBSET_DEF, INTERVAL_OPEN_SUBSET_CLOSED], ALL_TAC] THEN
1362 DISCH_THEN(X_CHOOSE_THEN ``c:real`` STRIP_ASSUME_TAC) THEN
1363 ASM_CASES_TAC ``(c:real) IN interval(a,b)`` THENL
1364 [ASM_MESON_TAC[SUBSET_DEF, INTERVAL_OPEN_SUBSET_CLOSED], ALL_TAC] THEN
1365 SUBGOAL_THEN ``?x:real. x IN interval(a,b)`` MP_TAC THENL
1366 [REWRITE_TAC[MEMBER_NOT_EMPTY, GSYM INTERVAL_EQ_EMPTY] THEN
1367 ASM_MESON_TAC[REAL_LE_ANTISYM, REAL_NOT_LE],
1368 ALL_TAC] THEN
1369 STRIP_TAC THEN Q.EXISTS_TAC `x` THEN
1370 REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP INTERVAL_CASES)) THEN
1371 ASM_REWRITE_TAC[] THEN REPEAT(DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC)) THEN
1372 ASM_MESON_TAC[REAL_LE_ANTISYM, SUBSET_DEF, INTERVAL_OPEN_SUBSET_CLOSED]
1373QED
1374
1375(* ------------------------------------------------------------------------- *)
1376(* One-dimensional mean value theorem. 1076 *)
1377(* ------------------------------------------------------------------------- *)
1378
1379Theorem MVT:
1380 !f:real->real f' a b.
1381 a < b /\ f continuous_on interval[a,b] /\
1382 (!x. x IN interval(a,b) ==> (f has_derivative f'(x)) (at x))
1383 ==> ?x. x IN interval(a,b) /\ (f(b) - f(a) = f'(x) (b - a))
1384Proof
1385 REPEAT STRIP_TAC THEN
1386 MP_TAC(SPECL [``\x. f(x) - ((f b - f a) / (b - a)) * x:real``,
1387 ``\k:real x:real.
1388 f'(k)(x) - ((f b - f a) / (b - a)) * x:real``,
1389 ``a:real``, ``b:real``]
1390 ROLLE) THEN
1391 REWRITE_TAC[] THEN
1392 Q_TAC SUFF_TAC `(a < b /\
1393 ((\x. f x - (f b - f a) / (b - a) * x) a =
1394 (\x. f x - (f b - f a) / (b - a) * x) b)) /\
1395 (\x. f x - (f b - f a) / (b - a) * x) continuous_on interval [(a,b)] /\
1396 (!x. x IN interval (a,b) ==>
1397 ((\x. f x - (f b - f a) / (b - a) * x) has_derivative
1398 (\k x. f' k x - (f b - f a) / (b - a) * x) x) (at x))` THENL
1399 [DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN
1400 STRIP_TAC THEN Q.EXISTS_TAC `x` THEN POP_ASSUM MP_TAC THEN
1401 ASM_SIMP_TAC std_ss [FUN_EQ_THM] THEN DISCH_THEN (MP_TAC o SPEC ``b - a:real``),
1402 ASM_SIMP_TAC real_ss [CONTINUOUS_ON_SUB, CONTINUOUS_ON_CMUL,
1403 CONTINUOUS_ON_ID] THEN
1404 CONJ_TAC THENL
1405 [REWRITE_TAC[REAL_ARITH
1406 ``(fa - k * a = fb - k * b) <=> (fb - fa = k * (b - a:real))``] THEN
1407 SIMP_TAC real_ss [real_div, REAL_ARITH ``a * b * c = a * (b * c:real)``] THEN
1408 `b - a <> 0` by (UNDISCH_TAC ``a < b:real`` THEN REAL_ARITH_TAC) THEN
1409 ASM_SIMP_TAC real_ss [REAL_MUL_LINV],
1410 REPEAT STRIP_TAC THEN
1411 ONCE_REWRITE_TAC [METIS [] ``(f b - f a) / (b - a) * x =
1412 (\x. (f b - f a) / (b - a) * x) x:real``] THEN
1413 MATCH_MP_TAC HAS_DERIVATIVE_SUB THEN
1414 ASM_SIMP_TAC real_ss [HAS_DERIVATIVE_CMUL, HAS_DERIVATIVE_ID, ETA_AX]]] THEN
1415 `b - a <> 0` by (UNDISCH_TAC ``a < b:real`` THEN REAL_ARITH_TAC) THEN
1416 ASM_SIMP_TAC real_ss [REAL_DIV_RMUL] THEN REAL_ARITH_TAC
1417QED
1418
1419Theorem MVT_SIMPLE :
1420 !f:real->real f' a b.
1421 a < b /\
1422 (!x. x IN interval[a,b]
1423 ==> (f has_derivative f'(x)) (at x within interval[a,b]))
1424 ==> ?x. x IN interval(a,b) /\ (f(b) - f(a) = f'(x) (b - a))
1425Proof
1426 MP_TAC MVT THEN
1427 REPEAT(HO_MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
1428 REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1429 CONJ_TAC THENL
1430 [MATCH_MP_TAC DIFFERENTIABLE_IMP_CONTINUOUS_ON THEN
1431 ASM_MESON_TAC[differentiable_on, differentiable],
1432 ASM_MESON_TAC[HAS_DERIVATIVE_WITHIN_OPEN, OPEN_INTERVAL,
1433 HAS_DERIVATIVE_WITHIN_SUBSET, INTERVAL_OPEN_SUBSET_CLOSED,
1434 SUBSET_DEF]]
1435QED
1436
1437Theorem MVT_VERY_SIMPLE :
1438 !f:real->real f' a b.
1439 a <= b /\
1440 (!x. x IN interval[a,b]
1441 ==> (f has_derivative f'(x)) (at x within interval[a,b]))
1442 ==> ?x. x IN interval[a,b] /\ (f(b) - f(a) = f'(x) (b - a))
1443Proof
1444 REPEAT GEN_TAC THEN ASM_CASES_TAC ``b:real = a`` THENL
1445 [ASM_REWRITE_TAC[REAL_SUB_REFL] THEN REPEAT STRIP_TAC THEN
1446 FIRST_X_ASSUM(MP_TAC o Q.SPEC `a:real`) THEN
1447 SIMP_TAC std_ss[INTERVAL_SING, IN_SING, has_derivative, UNWIND_THM2] THEN
1448 MESON_TAC[LINEAR_0],
1449 ‘a <> b’ by PROVE_TAC [] \\
1450 ASM_REWRITE_TAC[REAL_LE_LT] THEN
1451 DISCH_THEN(MP_TAC o MATCH_MP MVT_SIMPLE) THEN
1452 HO_MATCH_MP_TAC MONO_EXISTS THEN
1453 SIMP_TAC std_ss[REWRITE_RULE[SUBSET_DEF] INTERVAL_OPEN_SUBSET_CLOSED]]
1454QED
1455
1456(* ------------------------------------------------------------------------- *)
1457(* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *)
1458(* ------------------------------------------------------------------------- *)
1459
1460Theorem MVT_GENERAL:
1461 !f:real->real f' a b.
1462 a < b /\ f continuous_on interval[a,b] /\
1463 (!x. x IN interval(a,b) ==> (f has_derivative f'(x)) (at x))
1464 ==> ?x. x IN interval(a,b) /\
1465 abs(f(b) - f(a)) <= abs(f'(x) (b - a))
1466Proof
1467 REPEAT STRIP_TAC THEN
1468 MP_TAC(SPECL [``((\y. (f(b) - f(a)) * y)) o (f:real->real)``,
1469 ``\x t. ((f(b:real) - f(a)) *
1470 ((f':real->real->real) x t))``,
1471 ``a:real``, ``b:real``] MVT) THEN
1472 Q_TAC SUFF_TAC `a < b /\ (\y. (f b - f a) * y) o
1473 f continuous_on interval [(a,b)] /\
1474 (!x. x IN interval (a,b) ==>
1475 ((\y. (f b - f a) * y) o f has_derivative
1476 (\x t. (f b - f a) * f' x t) x) (at x))` THENL
1477 [ALL_TAC,
1478 ASM_SIMP_TAC real_ss [] THEN CONJ_TAC THENL
1479 [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1480 ASM_SIMP_TAC std_ss [CONTINUOUS_ON_ID, CONTINUOUS_ON_CONST, CONTINUOUS_ON_MUL],
1481 ALL_TAC] THEN
1482 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [o_DEF] THEN
1483 MATCH_MP_TAC HAS_DERIVATIVE_CMUL THEN METIS_TAC []] THEN
1484 DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN
1485 STRIP_TAC THEN Q.EXISTS_TAC `x` THEN POP_ASSUM MP_TAC THEN
1486 ASM_SIMP_TAC real_ss [GSYM REAL_SUB_LDISTRIB, o_THM] THEN
1487 DISCH_TAC THEN ASM_CASES_TAC ``(f:real->real) b = f a`` THENL
1488 [ASM_SIMP_TAC std_ss [REAL_SUB_REFL, ABS_0, ABS_POS], ALL_TAC] THEN
1489 REWRITE_TAC [REAL_LE_LT] THEN DISJ2_TAC THEN
1490 MATCH_MP_TAC REAL_EQ_LMUL_IMP THEN
1491 Q.EXISTS_TAC `abs((f:real->real) b - f a)` THEN
1492 ASM_SIMP_TAC real_ss [GSYM ABS_MUL] THEN
1493 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN
1494 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC
1495QED
1496
1497(* ------------------------------------------------------------------------- *)
1498(* Operator norm. *)
1499(* ------------------------------------------------------------------------- *)
1500
1501Definition oabs[nocompute]:
1502 oabs (f:real->real) = sup { abs(f x) | abs(x) = &1 }
1503End
1504
1505Theorem ABS_BOUND_GENERALIZE:
1506 !f:real->real b.
1507 linear f
1508 ==> ((!x. (abs(x) = &1) ==> abs(f x) <= b) <=>
1509 (!x. abs(f x) <= b * abs(x)))
1510Proof
1511 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THENL
1512 [ALL_TAC, ASM_MESON_TAC[REAL_MUL_RID]] THEN
1513 X_GEN_TAC ``x:real`` THEN ASM_CASES_TAC ``x:real = 0`` THENL
1514 [ASM_REWRITE_TAC[ABS_0, REAL_MUL_RZERO] THEN
1515 ASM_MESON_TAC[LINEAR_0, ABS_0, REAL_LE_REFL],
1516 ALL_TAC] THEN
1517 `0 < abs x` by (ASM_SIMP_TAC std_ss [GSYM ABS_NZ]) THEN
1518 ASM_SIMP_TAC real_ss [GSYM REAL_LE_LDIV_EQ, ABS_NZ, real_div] THEN
1519 MATCH_MP_TAC(REAL_ARITH ``abs(a * b) <= c ==> b * a <= c:real``) THEN
1520 ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN ASM_SIMP_TAC std_ss [ABS_ABS, GSYM ABS_INV] THEN
1521 REWRITE_TAC [GSYM ABS_MUL] THEN
1522 FIRST_ASSUM(fn th => REWRITE_TAC[GSYM(MATCH_MP LINEAR_CMUL th)]) THEN
1523 ASM_SIMP_TAC real_ss [ABS_MUL, ABS_INV, ABS_ABS, REAL_MUL_LINV, ABS_0]
1524QED
1525
1526Theorem OABS:
1527 !f:real->real.
1528 linear f
1529 ==> (!x. abs(f x) <= oabs f * abs(x)) /\
1530 (!b. (!x. abs(f x) <= b * abs(x)) ==> oabs f <= b)
1531Proof
1532 GEN_TAC THEN DISCH_TAC THEN
1533 MP_TAC(Q.SPEC `{ abs((f:real->real) x) | abs(x) = &1 }` SUP) THEN
1534 SIMP_TAC std_ss [GSPECIFICATION, LEFT_IMP_EXISTS_THM] THEN
1535 SIMP_TAC std_ss [LEFT_FORALL_IMP_THM, RIGHT_EXISTS_AND_THM, EXISTS_REFL] THEN
1536 ASM_SIMP_TAC std_ss [ABS_BOUND_GENERALIZE, GSYM oabs, GSYM MEMBER_NOT_EMPTY] THEN
1537 DISCH_THEN MATCH_MP_TAC THEN SIMP_TAC std_ss [GSPECIFICATION] THEN
1538 ASM_MESON_TAC[REAL_CHOOSE_SIZE, LINEAR_BOUNDED, REAL_POS]
1539QED
1540
1541(* ------------------------------------------------------------------------- *)
1542(* Still more general bound theorem. 1168 *)
1543(* ------------------------------------------------------------------------- *)
1544
1545Theorem DIFFERENTIABLE_BOUND:
1546 !f:real->real f' s B.
1547 convex s /\
1548 (!x. x IN s ==> (f has_derivative f'(x)) (at x within s)) /\
1549 (!x. x IN s ==> oabs(f'(x)) <= B)
1550 ==> !x y. x IN s /\ y IN s ==> abs(f(x) - f(y)) <= B * abs(x - y)
1551Proof
1552 ONCE_REWRITE_TAC[ABS_SUB] THEN REPEAT STRIP_TAC THEN
1553 SUBGOAL_THEN
1554 ``!x y. x IN s ==> abs((f':real->real->real)(x) y) <= B * abs(y)``
1555 ASSUME_TAC THENL
1556 [FULL_SIMP_TAC std_ss [has_derivative] THEN RW_TAC std_ss [] THEN
1557 FIRST_X_ASSUM (MP_TAC o Q.SPEC `x'`) THEN
1558 FIRST_X_ASSUM (MP_TAC o Q.SPEC `x'`) THEN
1559 ASM_REWRITE_TAC [] THEN RW_TAC std_ss [] THEN
1560 FIRST_X_ASSUM (MP_TAC o MATCH_MP OABS) THEN RW_TAC std_ss [] THEN
1561 MATCH_MP_TAC REAL_LE_TRANS THEN Q.EXISTS_TAC `oabs (f' x') * abs y'` THEN
1562 ASM_SIMP_TAC std_ss [] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
1563 ASM_SIMP_TAC std_ss [REAL_LE_REFL, ABS_POS] THEN
1564 SIMP_TAC std_ss [oabs] THEN MATCH_MP_TAC REAL_LE_SUP2 THEN
1565 SIMP_TAC std_ss [GSPECIFICATION] THEN Q.EXISTS_TAC `oabs (f' x') * abs 1` THEN
1566 Q.EXISTS_TAC `abs (f' x' 1)` THEN METIS_TAC [ABS_POS, ABS_1],
1567 ALL_TAC] THEN
1568 SUBGOAL_THEN
1569 ``!u. u IN interval[0,1] ==> (x + u * (y - x) :real) IN s``
1570 ASSUME_TAC THENL
1571 [REWRITE_TAC[IN_INTERVAL] THEN SIMP_TAC std_ss [REAL_LE_REFL] THEN
1572 REWRITE_TAC[REAL_ARITH ``x + u * (y - x) = (&1 - u) * x + u * y:real``] THEN
1573 ASM_MESON_TAC[CONVEX_ALT],
1574 ALL_TAC] THEN
1575 SUBGOAL_THEN
1576 ``!u. u IN interval(0,1) ==> (x + u * (y - x) :real) IN s``
1577 ASSUME_TAC THENL
1578 [ASM_MESON_TAC[SUBSET_DEF, INTERVAL_OPEN_SUBSET_CLOSED], ALL_TAC] THEN
1579 MP_TAC(SPECL
1580 [``(f:real->real) o (\u. x + u * (y - x))``,
1581 ``(\u. (f':real->real->real) (x + u * (y - x)) o
1582 (\u. 0 + u * (y - x)))``,
1583 ``0:real``, ``1:real``] MVT_GENERAL) THEN
1584 SIMP_TAC real_ss [o_DEF, REAL_ARITH ``x + &1 * (y - x) = y:real``,
1585 REAL_MUL_LZERO, REAL_SUB_RZERO, REAL_ADD_RID] THEN
1586 SIMP_TAC real_ss [REAL_MUL_LID] THEN
1587 Q_TAC SUFF_TAC `(\u. f (x + u * (y - x))) continuous_on interval [(0,1)] /\
1588 (!x'. x' IN interval (0,1) ==>
1589 ((\u. f (x + u * (y - x))) has_derivative
1590 (\u. f' (x + x' * (y - x)) (u * (y - x)))) (at x'))` THENL
1591 [DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN
1592 ASM_MESON_TAC[REAL_ADD_LID, REAL_LE_TRANS],
1593 ALL_TAC] THEN CONJ_TAC THENL
1594 [ONCE_REWRITE_TAC [METIS [] ``(x + u * (y - x)) = (\u. x + u * (y - x)) u:real``] THEN
1595 MATCH_MP_TAC (SIMP_RULE std_ss [o_DEF] CONTINUOUS_ON_COMPOSE) THEN
1596 SIMP_TAC real_ss [CONTINUOUS_ON_ADD, CONTINUOUS_ON_CONST, CONTINUOUS_ON_MUL,
1597 o_DEF, CONTINUOUS_ON_ID] THEN
1598 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN EXISTS_TAC ``s:real->bool`` THEN
1599 ASM_SIMP_TAC real_ss [SUBSET_DEF, FORALL_IN_IMAGE] THEN
1600 ASM_MESON_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN, differentiable,
1601 CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN],
1602 ALL_TAC] THEN
1603 X_GEN_TAC ``a:real`` THEN DISCH_TAC THEN
1604 SUBGOAL_THEN ``a IN interval(0:real,1) /\ open(interval(0:real,1))``
1605 MP_TAC THENL [ASM_MESON_TAC[OPEN_INTERVAL], ALL_TAC] THEN
1606 DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM(MATCH_MP
1607 HAS_DERIVATIVE_WITHIN_OPEN th)]) THEN
1608 ONCE_REWRITE_TAC [METIS [] ``(x + u * (y - x) = (\u. x + u * (y - x)) u) /\
1609 (u * (y - x) = (\u. u * (y - x)) u:real)``] THEN
1610 MATCH_MP_TAC (SIMP_RULE std_ss [o_DEF] DIFF_CHAIN_WITHIN) THEN
1611 CONJ_TAC THENL
1612 [ALL_TAC,
1613 MATCH_MP_TAC HAS_DERIVATIVE_WITHIN_SUBSET THEN
1614 EXISTS_TAC ``s:real->bool`` THEN
1615 ASM_SIMP_TAC real_ss [SUBSET_DEF, FORALL_IN_IMAGE]] THEN
1616 Q_TAC SUFF_TAC `((\u. x + u * (y - x)) has_derivative (\u. u * (y - x))) =
1617 ((\u. (\u. x) u + (\u. u * (y - x)) u) has_derivative
1618 (\u. (\u:real. 0:real) u + (\u. u * (y - x)) u))` THENL
1619 [DISC_RW_KILL, SIMP_TAC real_ss []] THEN
1620 MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN REWRITE_TAC [HAS_DERIVATIVE_CONST] THEN
1621 ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN
1622 ONCE_REWRITE_TAC [METIS [] ``(\u. (y - x) * u) = (\u. (y - x) * (\u. u) u:real)``] THEN
1623 MATCH_MP_TAC HAS_DERIVATIVE_CMUL THEN SIMP_TAC std_ss [HAS_DERIVATIVE_ID]
1624QED
1625
1626(* ------------------------------------------------------------------------- *)
1627(* Uniformly convergent sequence of derivatives. 1948 *)
1628(* ------------------------------------------------------------------------- *)
1629
1630Theorem HAS_DERIVATIVE_SEQUENCE_LIPSCHITZ:
1631 !s f:num->real->real f' g'.
1632 convex s /\
1633 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\
1634 (!e. &0 < e
1635 ==> ?N. !n x h. n >= N /\ x IN s
1636 ==> abs(f' n x h - g' x h) <= e * abs(h))
1637 ==> !e. &0 < e
1638 ==> ?N. !m n x y. m >= N /\ n >= N /\ x IN s /\ y IN s
1639 ==> abs((f m x - f n x) - (f m y - f n y))
1640 <= e * abs(x - y)
1641Proof
1642 REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o Q.SPEC `e / &2`) THEN
1643 ASM_REWRITE_TAC[REAL_HALF] THEN
1644 Q_TAC SUFF_TAC `!N. (!n x h. n >= N /\ x IN s ==>
1645 abs (f' n x h - g' x h) <= e / 2 * abs h) ==>
1646 !m n x y. m >= N /\ n >= N /\ x IN s /\ y IN s ==>
1647 abs (f m x - f n x - (f m y - f n y)) <= e * abs (x - y)` THENL
1648 [METIS_TAC [MONO_EXISTS], ALL_TAC] THEN
1649 X_GEN_TAC ``N:num`` THEN DISCH_TAC THEN
1650 MAP_EVERY X_GEN_TAC [``m:num``, ``n:num``] THEN
1651 ASM_CASES_TAC ``m:num >= N`` THEN ASM_REWRITE_TAC[] THEN
1652 ASM_CASES_TAC ``n:num >= N`` THEN ASM_REWRITE_TAC[] THEN
1653 ONCE_REWRITE_TAC [METIS [] ``(f m x - f n x - (f m y - f n y)) =
1654 ((\x. f m x - f n x) x - (\y. (f:num->real->real) m y - f n y) y)``] THEN
1655 MATCH_MP_TAC DIFFERENTIABLE_BOUND THEN
1656 Q.EXISTS_TAC `\x h. (f':num->real->real->real) m x h - f' n x h` THEN
1657 ASM_SIMP_TAC std_ss [] THEN CONJ_TAC THENL
1658 [METIS_TAC [HAS_DERIVATIVE_SUB], ALL_TAC] THEN
1659 X_GEN_TAC ``x:real`` THEN DISCH_TAC THEN
1660 SUBGOAL_THEN
1661 ``!h. abs((f':num->real->real->real) m x h - f' n x h) <= e * abs(h)``
1662 MP_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[HAS_DERIVATIVE_WITHIN_ALT]) THENL
1663 [ALL_TAC,
1664 Q_TAC SUFF_TAC `linear (\h. f' m x h - f' n x h)` THENL
1665 [ALL_TAC, MATCH_MP_TAC LINEAR_COMPOSE_SUB THEN METIS_TAC []] THEN
1666 DISCH_THEN (MP_TAC o MATCH_MP OABS) THEN RW_TAC std_ss []] THEN
1667 X_GEN_TAC ``h:real`` THEN SUBST1_TAC(REAL_ARITH
1668 ``(f':num->real->real->real) m x h - f' n x h =
1669 (f' m x h - g' x h) + -(f' n x h - g' x h)``) THEN
1670 MATCH_MP_TAC ABS_TRIANGLE_LE THEN
1671 Q_TAC SUFF_TAC `!a b h. a <= e / &2 * h /\ b <= e / &2 * h ==> a + b <= e * h:real` THENL
1672 [DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC real_ss [ABS_NEG], ALL_TAC] THEN
1673 ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN SIMP_TAC real_ss [real_div] THEN
1674 ONCE_REWRITE_TAC [REAL_ARITH ``a * (b * c) = (a * b) * c:real``] THEN
1675 SIMP_TAC real_ss [GSYM real_div, REAL_LE_RDIV_EQ] THEN REAL_ARITH_TAC
1676QED
1677
1678Theorem HAS_DERIVATIVE_SEQUENCE:
1679 !s f:num->real->real f' g'.
1680 convex s /\
1681 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\
1682 (!e. &0 < e
1683 ==> ?N. !n x h. n >= N /\ x IN s
1684 ==> abs(f' n x h - g' x h) <= e * abs(h)) /\
1685 (?x l. x IN s /\ ((\n. f n x) --> l) sequentially)
1686 ==> ?g. !x. x IN s
1687 ==> ((\n. f n x) --> g x) sequentially /\
1688 (g has_derivative g'(x)) (at x within s)
1689Proof
1690
1691 REPEAT GEN_TAC THEN
1692 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1693 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1694 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN (* O *)
1695 DISCH_THEN(X_CHOOSE_THEN ``x0:real`` STRIP_ASSUME_TAC) THEN
1696 SUBGOAL_THEN ``!e. &0 < e
1697 ==> ?N. !m n x y. m >= N /\ n >= N /\ x IN s /\ y IN s
1698 ==> abs(((f:num->real->real) m x - f n x) - (f m y - f n y))
1699 <= e * abs(x - y)`` ASSUME_TAC THENL
1700 [MATCH_MP_TAC HAS_DERIVATIVE_SEQUENCE_LIPSCHITZ THEN
1701 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[], ALL_TAC] THEN
1702 SUBGOAL_THEN
1703 ``?g:real->real. !x. x IN s ==> ((\n. f n x) --> g x) sequentially``
1704 MP_TAC THENL
1705 [SIMP_TAC std_ss [GSYM SKOLEM_THM, RIGHT_EXISTS_IMP_THM] THEN
1706 X_GEN_TAC ``x:real`` THEN DISCH_TAC THEN
1707 GEN_REWR_TAC I [CONVERGENT_EQ_CAUCHY] THEN
1708 FIRST_X_ASSUM(MP_TAC o MATCH_MP CONVERGENT_IMP_CAUCHY) THEN
1709 SIMP_TAC std_ss [cauchy_def, dist] THEN DISCH_TAC THEN
1710 X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN
1711 ASM_CASES_TAC ``x:real = x0`` THEN ASM_SIMP_TAC std_ss [] THEN
1712 FIRST_X_ASSUM (MP_TAC o Q.SPEC `e / &2`) THEN
1713 ASM_REWRITE_TAC[REAL_HALF] THEN
1714 DISCH_THEN(X_CHOOSE_THEN ``N1:num`` STRIP_ASSUME_TAC) THEN
1715 `0 < abs(x - x0)` by (UNDISCH_TAC ``x <> x0:real`` THEN REAL_ARITH_TAC) THEN
1716 FIRST_X_ASSUM (MP_TAC o Q.SPEC `e / &2 / abs(x - x0:real)`) THEN
1717 ASM_SIMP_TAC real_ss [REAL_LT_DIV, ABS_NZ, REAL_HALF] THEN
1718 DISCH_THEN(X_CHOOSE_TAC ``N2:num``) THEN
1719 EXISTS_TAC ``N1 + N2:num`` THEN X_GEN_TAC ``m:num`` THEN X_GEN_TAC ``n:num`` THEN
1720 DISCH_THEN(CONJUNCTS_THEN (STRIP_ASSUME_TAC o MATCH_MP
1721 (ARITH_PROVE ``m >= N1 + N2:num ==> m >= N1 /\ m >= N2``))) THEN
1722 SUBST1_TAC(REAL_ARITH
1723 ``(f:num->real->real) m x - f n x =
1724 (f m x - f n x - (f m x0 - f n x0)) + (f m x0 - f n x0)``) THEN
1725 MATCH_MP_TAC ABS_TRIANGLE_LT THEN
1726 FIRST_X_ASSUM(MP_TAC o SPECL
1727 [``m:num``, ``n:num``, ``x:real``, ``x0:real``]) THEN
1728 FIRST_X_ASSUM(MP_TAC o SPECL [``m:num``, ``n:num``]) THEN
1729 SIMP_TAC real_ss [real_div] THEN
1730 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = a * b * (c * d:real)``] THEN
1731 ASM_SIMP_TAC real_ss [REAL_LT_IMP_NE, REAL_MUL_LINV] THEN
1732 ASM_SIMP_TAC real_ss [GSYM real_div, real_sub] THEN
1733 SIMP_TAC real_ss [REAL_LT_RDIV_EQ, REAL_LE_RDIV_EQ] THEN REAL_ARITH_TAC,
1734 ALL_TAC] THEN
1735 STRIP_TAC THEN Q.EXISTS_TAC `g` THEN ASM_SIMP_TAC std_ss [] THEN
1736 X_GEN_TAC ``x:real`` THEN DISCH_TAC THEN
1737 REWRITE_TAC[HAS_DERIVATIVE_WITHIN_ALT] THEN
1738 SUBGOAL_THEN ``!e. &0 < e
1739 ==> ?N. !n x y. n >= N /\ x IN s /\ y IN s
1740 ==> abs(((f:num->real->real) n x - f n y) - (g x - g y))
1741 <= e * abs(x - y)`` ASSUME_TAC THENL
1742 [X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN
1743 UNDISCH_TAC ``!e:real. 0 < e ==>
1744 ?N. !m:num n:num x:real y:real.
1745 m >= N /\ n >= N /\ x IN s /\ y IN s ==>
1746 abs (f m x - f n x - (f m y - f n y)) <= e * abs (x - y)`` THEN
1747 DISCH_THEN (MP_TAC o SPEC ``e:real``) THEN ASM_REWRITE_TAC[] THEN
1748 STRIP_TAC THEN Q.EXISTS_TAC `N` THEN GEN_TAC THEN
1749 POP_ASSUM (MP_TAC o Q.SPEC `n`) THEN DISCH_TAC THEN
1750 MAP_EVERY X_GEN_TAC [``u:real``, ``v:real``] THEN
1751 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN ``m:num`` o SPECL
1752 [``m:num``, ``u:real``, ``v:real``]) THEN
1753 DISCH_TAC THEN MATCH_MP_TAC(ISPEC ``sequentially`` LIM_ABS_UBOUND) THEN
1754 Q.EXISTS_TAC
1755 `\m. ((f:num->real->real) n u - f n v) - (f m u - f m v)` THEN
1756 REWRITE_TAC[eventually, TRIVIAL_LIMIT_SEQUENTIALLY] THEN
1757 ASM_SIMP_TAC std_ss [SEQUENTIALLY, LIM_SUB, LIM_CONST] THEN EXISTS_TAC ``N:num`` THEN
1758 ONCE_REWRITE_TAC[REAL_ARITH
1759 ``(x - y) - (u - v) = (x - u) - (y - v):real``] THEN
1760 ASM_MESON_TAC[GREATER_EQ_REFL], ALL_TAC] THEN
1761 CONJ_TAC THENL
1762 [SUBGOAL_THEN
1763 ``!u. ((\n. (f':num->real->real->real) n x u) --> g' x u) sequentially``
1764 ASSUME_TAC THENL
1765 [REWRITE_TAC[LIM_SEQUENTIALLY, dist] THEN REPEAT STRIP_TAC THEN
1766 UNDISCH_TAC ``!e:real. 0 < e ==>
1767 ?N:num. !n x:real h:real. n >= N /\ x IN s ==>
1768 abs (f' n x h - g' x h) <= e * abs h`` THEN
1769 DISCH_TAC THEN ASM_CASES_TAC ``u = 0:real`` THENL
1770 [FIRST_X_ASSUM (MP_TAC o SPEC ``e:real``),
1771 FIRST_X_ASSUM (MP_TAC o SPEC ``e / &2 / abs(u:real)``)] THENL
1772 [ALL_TAC,
1773 `0 < abs u` by (UNDISCH_TAC ``u <> 0:real`` THEN REAL_ARITH_TAC)] THEN
1774 ASM_SIMP_TAC arith_ss [ABS_NZ, REAL_LT_DIV, REAL_LT] THEN
1775 STRIP_TAC THEN Q.EXISTS_TAC `N` THEN GEN_TAC THEN
1776 POP_ASSUM (MP_TAC o Q.SPEC `n`) THEN
1777 DISCH_THEN(MP_TAC o SPECL [``x:real``, ``u:real``]) THEN
1778 DISCH_THEN(fn th => DISCH_TAC THEN MP_TAC th) THEN
1779 ASM_SIMP_TAC real_ss [GE, ABS_0, REAL_MUL_RZERO, ABS_POS] THEN
1780 ASM_SIMP_TAC real_ss [REAL_DIV_RMUL, ABS_0] THENL
1781 [UNDISCH_TAC ``&0 < e:real`` THEN REAL_ARITH_TAC, ALL_TAC] THEN
1782 SIMP_TAC std_ss [real_div] THEN
1783 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = a * b * (c * d:real)``] THEN
1784 ASM_SIMP_TAC real_ss [REAL_LT_IMP_NE, REAL_MUL_LINV] THEN
1785 ASM_SIMP_TAC real_ss [GSYM real_div, REAL_LE_RDIV_EQ] THEN
1786 UNDISCH_TAC ``&0 < e:real`` THEN REAL_ARITH_TAC, ALL_TAC] THEN
1787 REWRITE_TAC[linear] THEN CONJ_TAC THENL
1788 [MAP_EVERY X_GEN_TAC [``u:real``, ``v:real``],
1789 MAP_EVERY X_GEN_TAC [``c:real``, ``u:real``]] THEN
1790 MATCH_MP_TAC(ISPEC ``sequentially`` LIM_UNIQUE) THENL
1791 [Q.EXISTS_TAC
1792 `\n. (f':num->real->real->real) n x (u + v)`,
1793 Q.EXISTS_TAC
1794 `\n. (f':num->real->real->real) n x (c * u)`] THEN
1795 ASM_SIMP_TAC real_ss [TRIVIAL_LIMIT_SEQUENTIALLY, LIM_SUB, LIM_ADD, LIM_CMUL] THEN
1796 RULE_ASSUM_TAC(REWRITE_RULE[has_derivative_within, linear]) THEN
1797 ASM_SIMP_TAC real_ss [REAL_SUB_REFL, LIM_CONST] THEN
1798 METIS_TAC [LIM_ADD, LIM_CMUL], ALL_TAC] THEN
1799 X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN
1800 FIRST_X_ASSUM (MP_TAC o Q.SPEC `e / &3`) THEN
1801 UNDISCH_TAC ``!e:real. 0 < e ==>
1802 ?N:num. !n x:real h:real. n >= N /\ x IN s ==>
1803 abs (f' n x h - g' x h) <= e * abs h`` THEN
1804 DISCH_THEN (MP_TAC o Q.SPEC `e / &3`) THEN
1805 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT] THEN
1806 DISCH_THEN(X_CHOOSE_THEN ``N1:num`` ASSUME_TAC) THEN
1807 DISCH_THEN(X_CHOOSE_THEN ``N2:num`` ASSUME_TAC) THEN
1808 UNDISCH_TAC ``!n:num x:real h:real. n >= N1 /\ x IN s ==>
1809 abs (f' n x h - g' x h) <= e / 3 * abs h`` THEN DISCH_TAC THEN
1810 FIRST_X_ASSUM (MP_TAC o GEN ``y:real`` o
1811 Q.SPECL [`N1 + N2:num`, `x:real`, `y - x:real`]) THEN
1812 FIRST_X_ASSUM (MP_TAC o GEN ``y:real`` o
1813 Q.SPECL [`N1 + N2:num`, `y:real`, `x:real`]) THEN
1814 FIRST_X_ASSUM(MP_TAC o Q.SPECL [`N1 + N2:num`, `x:real`]) THEN
1815 ASM_REWRITE_TAC[ARITH_PROVE ``m + n >= m:num /\ m + n >= n``] THEN
1816 REWRITE_TAC[HAS_DERIVATIVE_WITHIN_ALT] THEN
1817 DISCH_THEN(MP_TAC o Q.SPEC `e / &3` o CONJUNCT2) THEN
1818 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT] THEN
1819 DISCH_THEN(X_CHOOSE_THEN ``d1:real`` STRIP_ASSUME_TAC) THEN
1820 DISCH_TAC THEN DISCH_TAC THEN
1821 Q.EXISTS_TAC `d1:real` THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC ``y:real`` THEN
1822 DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o Q.SPEC `y:real`) THEN
1823 FIRST_X_ASSUM (MP_TAC o Q.SPEC `y:real`) THEN
1824 FIRST_X_ASSUM(MP_TAC o Q.SPEC `y:real`) THEN
1825 Q_TAC SUFF_TAC `!a b c d n. d <= a + b + c
1826 ==> a <= e / &3 * n ==> b <= e / &3 * n ==> c <= e / &3 * n
1827 ==> d <= e * n` THENL
1828 [ALL_TAC,
1829 ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN SIMP_TAC real_ss [real_div] THEN
1830 ONCE_REWRITE_TAC [REAL_ARITH ``a * (b * c) = (a * b) * c:real``] THEN
1831 SIMP_TAC real_ss [GSYM real_div, REAL_LE_RDIV_EQ] THEN REAL_ARITH_TAC] THEN
1832 ASM_SIMP_TAC real_ss [] THEN DISCH_THEN MATCH_MP_TAC THEN
1833 Q_TAC SUFF_TAC `abs (f (N1 + N2) y - f (N1 + N2) x - (g y - g x)) =
1834 abs ((g y - g x) - (f (N1 + N2) y - f (N1 + N2) x))` THENL
1835 [DISC_RW_KILL, SIMP_TAC real_ss [ABS_SUB]] THEN
1836 MATCH_MP_TAC(REAL_ARITH
1837 ``(abs(x + y + z) = abs(a)) /\
1838 abs(x + y + z) <= abs(x) + abs(y + z) /\
1839 abs(y + z) <= abs(y) + abs(z)
1840 ==> abs(a) <= abs(x) + abs(y) + abs(z:real)``) THEN
1841 ONCE_REWRITE_TAC [REAL_ARITH ``a + b + c = a + (b + c:real)``] THEN
1842 SIMP_TAC std_ss [ABS_TRIANGLE] THEN AP_TERM_TAC THEN REAL_ARITH_TAC
1843QED
1844
1845(* ------------------------------------------------------------------------- *)
1846(* Differentiation of a series. HAS_DERIVATIVE_SEQUENCE 2187 *)
1847(* ------------------------------------------------------------------------- *)
1848
1849Theorem HAS_DERIVATIVE_SERIES:
1850 !s f:num->real->real f' g' k.
1851 convex s /\
1852 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\
1853 (!e. &0 < e
1854 ==> ?N. !n x h. n >= N /\ x IN s
1855 ==> abs(sum(k INTER {x | 0 <= x /\ x <= n}) (\i. f' i x h) -
1856 g' x h) <= e * abs(h)) /\
1857 (?x l. x IN s /\ ((\n. f n x) sums l) k)
1858 ==> ?g. !x. x IN s ==> ((\n. f n x) sums (g x)) k /\
1859 (g has_derivative g'(x)) (at x within s)
1860Proof
1861 REPEAT GEN_TAC THEN REWRITE_TAC[sums_def, GSYM numseg] THEN
1862 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
1863 ONCE_REWRITE_TAC [METIS [] ``sum (k INTER {0 .. n}) (\n. f n x) =
1864 (\n x. sum (k INTER {0 .. n}) (\n. f n x)) n x``] THEN
1865 MATCH_MP_TAC HAS_DERIVATIVE_SEQUENCE THEN Q.EXISTS_TAC
1866 `(\n:num x:real h:real. sum(k INTER { 0n .. n}) (\n. f' n x h):real)` THEN
1867 ASM_SIMP_TAC real_ss [FINITE_INTER_NUMSEG] THEN RW_TAC std_ss [] THEN
1868 ONCE_REWRITE_TAC [METIS [] ``(\n. f' n x h) = (\n. (\n h. f' n x h) n h)``] THEN
1869 MATCH_MP_TAC HAS_DERIVATIVE_SUM THEN METIS_TAC [FINITE_INTER_NUMSEG, ETA_AX]
1870QED
1871
1872Theorem HAS_DERIVATIVE_SERIES':
1873 !s f f' g' k.
1874 convex s /\
1875 (!n x. x IN s
1876 ==> (f n has_derivative (\y. f' n x * y)) (at x within s)) /\
1877 (!e. &0 < e
1878 ==> ?N. !n x. n >= N /\ x IN s
1879 ==> abs(sum (k INTER { 0n..n}) (\i. f' i x) - g' x) <= e) /\
1880 (?x l. x IN s /\ ((\n. f n x) sums l) k)
1881 ==> ?g. !x. x IN s
1882 ==> ((\n. f n x) sums g x) k /\
1883 (g has_derivative (\y. g' x * y)) (at x within s)
1884Proof
1885 REPEAT STRIP_TAC THEN
1886 ONCE_REWRITE_TAC [METIS [] ``(\y. g' x * y) = (\x y. (g':real->real) x * y) x``] THEN
1887 MATCH_MP_TAC HAS_DERIVATIVE_SERIES THEN
1888 Q.EXISTS_TAC `\n x h. (f':num->real->real) n x * h` THEN
1889 ASM_SIMP_TAC std_ss [] THEN CONJ_TAC THENL [ALL_TAC, METIS_TAC[]] THEN
1890 ONCE_REWRITE_TAC [METIS [] ``(\i. (f':num->real->real) i x' * h) =
1891 (\i. (\i. f' i x') i * h)``] THEN
1892 SIMP_TAC std_ss [SUM_RMUL, GSYM REAL_SUB_RDISTRIB, ABS_MUL] THEN
1893 Q_TAC SUFF_TAC `!n. {x | x <= n} = { 0n .. n}` THENL
1894 [METIS_TAC[REAL_LE_RMUL_IMP, ABS_POS], ALL_TAC] THEN
1895 RW_TAC arith_ss [EXTENSION, GSPECIFICATION, IN_NUMSEG]
1896QED
1897
1898(* ------------------------------------------------------------------------- *)
1899(* Derivative with composed bilinear function. *)
1900(* ------------------------------------------------------------------------- *)
1901
1902Theorem HAS_DERIVATIVE_BILINEAR_WITHIN:
1903 !h:real->real->real f g f' g' x:real s.
1904 (f has_derivative f') (at x within s) /\
1905 (g has_derivative g') (at x within s) /\
1906 bilinear h
1907 ==> ((\x. h (f x) (g x)) has_derivative
1908 (\d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)
1909Proof
1910 REPEAT STRIP_TAC THEN
1911 SUBGOAL_THEN ``((g:real->real) --> g(x)) (at x within s)`` ASSUME_TAC THENL
1912 [REWRITE_TAC[GSYM CONTINUOUS_WITHIN] THEN
1913 ASM_MESON_TAC[differentiable, DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN],
1914 ALL_TAC] THEN
1915 UNDISCH_TAC ``((f:real->real) has_derivative f') (at x within s)`` THEN
1916 REWRITE_TAC[has_derivative_within] THEN
1917 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC ASSUME_TAC) THEN
1918 SUBGOAL_THEN
1919 ``((\y. (f:real->real)(x) + f'(y - x)) --> f(x)) (at x within s)``
1920 ASSUME_TAC THENL
1921 [GEN_REWR_TAC LAND_CONV [GSYM REAL_ADD_RID] THEN
1922 Q_TAC SUFF_TAC `((\y. (\y. f x) y + (\y. f' (y - x)) y)
1923 --> (f x + 0)) (at x within s)` THENL
1924 [SIMP_TAC std_ss [], ALL_TAC] THEN
1925 MATCH_MP_TAC LIM_ADD THEN REWRITE_TAC[LIM_CONST] THEN
1926 SUBGOAL_THEN ``0 = (f':real->real)(x - x)`` SUBST1_TAC THENL
1927 [ASM_MESON_TAC[LINEAR_0, REAL_SUB_REFL], ALL_TAC] THEN
1928 ASM_SIMP_TAC std_ss [LIM_LINEAR, LIM_SUB, LIM_CONST, LIM_WITHIN_ID],
1929 ALL_TAC] THEN
1930 UNDISCH_TAC ``(g has_derivative g') (at x within s)`` THEN
1931 ONCE_REWRITE_TAC [has_derivative_within] THEN
1932 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC ASSUME_TAC) THEN
1933 CONJ_TAC THENL
1934 [UNDISCH_TAC ``bilinear h`` THEN ONCE_REWRITE_TAC [bilinear] THEN
1935 STRIP_TAC THEN
1936 RULE_ASSUM_TAC(REWRITE_RULE[linear]) THEN ASM_REWRITE_TAC[linear] THEN
1937 FULL_SIMP_TAC real_ss [] THEN REPEAT STRIP_TAC THEN REAL_ARITH_TAC,
1938 ALL_TAC] THEN
1939 MP_TAC(Q.ISPECL [`at (x:real) within s`, `h:real->real->real`]
1940 LIM_BILINEAR) THEN
1941 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1942 UNDISCH_TAC ``(g --> g x) (at x within s)`` THEN
1943 UNDISCH_TAC ``((\y. inv (abs (y - x)) * (f y - (f x + f' (y - x)))) --> 0)
1944 (at x within s)`` THEN
1945 REWRITE_TAC[AND_IMP_INTRO] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1946 UNDISCH_TAC ``((\y. inv (abs (y - x)) * (g y - (g x + g' (y - x)))) --> 0)
1947 (at x within s)`` THEN
1948 UNDISCH_TAC ``((\y. f x + f' (y - x)) --> f x) (at x within s)`` THEN
1949 ONCE_REWRITE_TAC[AND_IMP_INTRO] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1950 REWRITE_TAC[AND_IMP_INTRO] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN
1951 SUBGOAL_THEN
1952 ``((\y:real. inv(abs(y - x)) * (h:real->real->real) (f'(y - x)) (g'(y - x)))
1953 --> 0) (at x within s)``
1954 MP_TAC THENL
1955 [FIRST_ASSUM(X_CHOOSE_THEN ``B:real`` STRIP_ASSUME_TAC o MATCH_MP
1956 BILINEAR_BOUNDED_POS) THEN
1957 X_CHOOSE_THEN ``C:real`` STRIP_ASSUME_TAC
1958 (MATCH_MP LINEAR_BOUNDED_POS (ASSUME ``linear (f':real->real)``)) THEN
1959 X_CHOOSE_THEN ``D:real`` STRIP_ASSUME_TAC
1960 (MATCH_MP LINEAR_BOUNDED_POS (ASSUME ``linear (g':real->real)``)) THEN
1961 REWRITE_TAC[LIM_WITHIN, dist, REAL_SUB_RZERO] THEN
1962 X_GEN_TAC ``e:real`` THEN STRIP_TAC THEN Q.EXISTS_TAC `e / (B * C * D)` THEN
1963 ASM_SIMP_TAC real_ss [REAL_LT_DIV, ABS_MUL, REAL_LT_MUL] THEN
1964 X_GEN_TAC ``x':real`` THEN STRIP_TAC THEN
1965 ASM_SIMP_TAC real_ss [ABS_MUL, ABS_ABS, ABS_INV, REAL_LT_IMP_NE] THEN
1966 MATCH_MP_TAC REAL_LET_TRANS THEN
1967 Q.EXISTS_TAC `inv(abs(x' - x :real)) *
1968 B * (C * abs(x' - x)) * (D * abs(x' - x))` THEN
1969 CONJ_TAC THENL
1970 [ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = a * (b * c * d:real)``] THEN
1971 MATCH_MP_TAC REAL_LE_LMUL_IMP THEN SIMP_TAC real_ss [REAL_LE_INV_EQ, ABS_POS] THEN
1972 MATCH_MP_TAC REAL_LE_TRANS THEN
1973 Q.EXISTS_TAC `B * abs (f' (x' - x)) * abs (g' (x' - x))` THEN
1974 ASM_SIMP_TAC std_ss [] THEN REWRITE_TAC [GSYM REAL_MUL_ASSOC] THEN
1975 MATCH_MP_TAC REAL_LE_LMUL_IMP THEN ASM_SIMP_TAC std_ss [REAL_LT_IMP_LE] THEN
1976 ONCE_REWRITE_TAC [REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
1977 ASM_SIMP_TAC real_ss [ABS_POS],
1978 ONCE_REWRITE_TAC[REAL_ARITH
1979 ``i * b * (c * x) * (d * x) = (i * x) * x * (b * c * d:real)``] THEN
1980 ASM_SIMP_TAC real_ss [REAL_MUL_LINV, REAL_LT_IMP_NE, REAL_MUL_LID] THEN
1981 ASM_SIMP_TAC real_ss [GSYM REAL_LT_RDIV_EQ, REAL_LT_MUL]],
1982 REWRITE_TAC[AND_IMP_INTRO] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN
1983 SIMP_TAC std_ss (map (C MATCH_MP (ASSUME ``bilinear(h:real->real->real)``))
1984 [BILINEAR_RZERO, BILINEAR_LZERO, BILINEAR_LADD, BILINEAR_RADD,
1985 BILINEAR_LMUL, BILINEAR_RMUL, BILINEAR_LSUB, BILINEAR_RSUB]) THEN
1986 MATCH_MP_TAC EQ_IMPLIES THEN AP_THM_TAC THEN
1987 BINOP_TAC THEN SIMP_TAC real_ss [FUN_EQ_THM] THEN REAL_ARITH_TAC]
1988QED
1989
1990Theorem HAS_DERIVATIVE_BILINEAR_AT:
1991 !h:real->real->real f g f' g' x:real.
1992 (f has_derivative f') (at x) /\
1993 (g has_derivative g') (at x) /\
1994 bilinear h
1995 ==> ((\x. h (f x) (g x)) has_derivative
1996 (\d. h (f x) (g' d) + h (f' d) (g x))) (at x)
1997Proof
1998 REWRITE_TAC[has_derivative_at] THEN
1999 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
2000 REWRITE_TAC[GSYM has_derivative_within, HAS_DERIVATIVE_BILINEAR_WITHIN]
2001QED
2002
2003Theorem HAS_DERIVATIVE_MUL_WITHIN:
2004 !f f' g:real->real g' a s.
2005 ((f) has_derivative (f')) (at a within s) /\
2006 (g has_derivative g') (at a within s)
2007 ==> ((\x. f x * g x) has_derivative
2008 (\h. f a * g' h + f' h * g a)) (at a within s)
2009Proof
2010 REPEAT GEN_TAC THEN
2011 DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[BILINEAR_DOT]
2012 (Q.ISPEC `\x y:real. x * y` HAS_DERIVATIVE_BILINEAR_WITHIN))) THEN
2013 SIMP_TAC std_ss [o_DEF]
2014QED
2015
2016Theorem HAS_DERIVATIVE_MUL_AT:
2017 !f f' g:real->real g' a.
2018 ((f) has_derivative (f')) (at a) /\
2019 (g has_derivative g') (at a)
2020 ==> ((\x. f x * g x) has_derivative
2021 (\h. f a * g' h + f' h * g a)) (at a)
2022Proof
2023 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
2024 REWRITE_TAC[HAS_DERIVATIVE_MUL_WITHIN]
2025QED
2026
2027(* ------------------------------------------------------------------------- *)
2028(* Considering derivative R->R as a vector. *)
2029(* ------------------------------------------------------------------------- *)
2030
2031val _ = set_fixity "has_vector_derivative" (Infix(NONASSOC, 450));
2032
2033Definition has_vector_derivative[nocompute]:
2034 (f has_vector_derivative f') net <=>
2035 (f has_derivative (\x. (x) * f')) net
2036End
2037
2038Definition vector_derivative[nocompute]:
2039 vector_derivative (f:real->real) net =
2040 @f'. (f has_vector_derivative f') net
2041End
2042
2043(* NOTE: This theorem is NOT from HOL-Light, as it's only possible under one
2044 dimensional case, showing ‘has_derivative’ and ‘has_vector_derivative’ is
2045 inter-changable in HOL4.
2046 *)
2047Theorem has_derivative_iff_has_vector_derivative :
2048 !f net. (?f'. (f has_derivative f') net) <=>
2049 (?l. (f has_vector_derivative l) net)
2050Proof
2051 rpt GEN_TAC
2052 >> reverse EQ_TAC
2053 >- (rw [has_vector_derivative] \\
2054 Q.EXISTS_TAC ‘\x. l * x’ >> art [])
2055 >> rw [has_derivative, has_vector_derivative]
2056 >> gs [linear_repr]
2057 >> Q.EXISTS_TAC ‘l’ >> art []
2058 >> Q.EXISTS_TAC ‘l’ >> rw [FUN_EQ_THM]
2059QED
2060
2061(* |- !f net. f differentiable net <=> ?f'. (f has_vector_derivative f') net *)
2062Theorem differentiable_alt_has_vector_derivative =
2063 REWRITE_RULE [has_derivative_iff_has_vector_derivative] differentiable
2064
2065Theorem has_vector_derivative_within :
2066 !f l x s.
2067 (f has_vector_derivative l) (at x within s) <=>
2068 ((\y. inv(abs(y - x)) * (f(y) - (f(x) + l * (y - x)))) --> 0)
2069 (at x within s)
2070Proof
2071 rw [has_vector_derivative, has_derivative_within, LINEAR_SCALING]
2072QED
2073
2074(* |- !c. linear (\x. x * c) *)
2075Theorem LINEAR_SCALING'[local] =
2076 ONCE_REWRITE_RULE [REAL_MUL_COMM] LINEAR_SCALING
2077
2078(* |- !f f' x s.
2079 (f has_vector_derivative f') (at x within s) <=>
2080 !e. 0 < e ==>
2081 ?d. 0 < d /\
2082 !x'.
2083 x' IN s /\ 0 < abs (x' - x) /\ abs (x' - x) < d ==>
2084 abs (f x' - f x - (x' - x) * f') / abs (x' - x) < e
2085 *)
2086Theorem HAS_VECTOR_DERIVATIVE_WITHIN =
2087 HAS_DERIVATIVE_WITHIN
2088 |> Q.SPECL [‘f’, ‘\x. x * f'’, ‘x’, ‘s’]
2089 |> SIMP_RULE std_ss [GSYM has_vector_derivative, LINEAR_SCALING']
2090 |> Q.GENL [‘f’, ‘f'’, ‘x’, ‘s’]
2091
2092(* |- !f f' x s.
2093 (f has_vector_derivative f') (at s within x) <=>
2094 !e. 0 < e ==>
2095 ?d. 0 < d /\
2096 !y. y IN x /\ abs (y - s) < d ==>
2097 abs (f y - f s - (y - s) * f') <= e * abs (y - s)
2098 *)
2099Theorem HAS_VECTOR_DERIVATIVE_WITHIN_ALT =
2100 HAS_DERIVATIVE_WITHIN_ALT
2101 |> Q.SPECL [‘f’, ‘\x. x * f'’, ‘x’, ‘s’]
2102 |> SIMP_RULE std_ss [GSYM has_vector_derivative, LINEAR_SCALING']
2103 |> Q.GENL [‘f’, ‘f'’, ‘x’, ‘s’]
2104
2105Theorem HAS_VECTOR_DERIVATIVE_WITHIN_OPEN :
2106 !f f' a s.
2107 a IN s /\ open s
2108 ==> ((f has_vector_derivative f') (at a within s) <=>
2109 (f has_vector_derivative f') (at a))
2110Proof
2111 RW_TAC std_ss [has_vector_derivative]
2112 >> MATCH_MP_TAC HAS_DERIVATIVE_WITHIN_OPEN >> art []
2113QED
2114
2115Theorem HAS_VECTOR_DERIVATIVE_WITHIN_SUBSET :
2116 !f f' s t x. (f has_vector_derivative f') (at x within s) /\ t SUBSET s
2117 ==> (f has_vector_derivative f') (at x within t)
2118Proof
2119 REWRITE_TAC [has_vector_derivative, HAS_DERIVATIVE_WITHIN_SUBSET]
2120QED
2121
2122Theorem HAS_VECTOR_DERIVATIVE_BILINEAR_WITHIN:
2123 !h:real->real->real f g f' g' x s.
2124 (f has_vector_derivative f') (at x within s) /\
2125 (g has_vector_derivative g') (at x within s) /\
2126 bilinear h
2127 ==> ((\x. h (f x) (g x)) has_vector_derivative
2128 (h (f x) g' + h f' (g x))) (at x within s)
2129Proof
2130 REPEAT GEN_TAC THEN SIMP_TAC std_ss [has_vector_derivative] THEN
2131 DISCH_TAC THEN
2132 FIRST_ASSUM(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_WITHIN) THEN
2133 RULE_ASSUM_TAC(REWRITE_RULE[bilinear, linear]) THEN
2134 FULL_SIMP_TAC real_ss [REAL_ADD_LDISTRIB]
2135QED
2136
2137Theorem HAS_VECTOR_DERIVATIVE_BILINEAR_AT:
2138 !h:real->real->real f g f' g' x.
2139 (f has_vector_derivative f') (at x) /\
2140 (g has_vector_derivative g') (at x) /\
2141 bilinear h
2142 ==> ((\x. h (f x) (g x)) has_vector_derivative
2143 (h (f x) g' + h f' (g x))) (at x)
2144Proof
2145 REPEAT GEN_TAC THEN SIMP_TAC real_ss [has_vector_derivative] THEN
2146 DISCH_TAC THEN
2147 FIRST_ASSUM(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_AT) THEN
2148 RULE_ASSUM_TAC(REWRITE_RULE[bilinear, linear]) THEN
2149 FULL_SIMP_TAC real_ss [REAL_ADD_LDISTRIB]
2150QED
2151
2152Theorem HAS_VECTOR_DERIVATIVE_AT_WITHIN :
2153 !f f' x s. (f has_vector_derivative f') (at x)
2154 ==> (f has_vector_derivative f') (at x within s)
2155Proof
2156 SIMP_TAC std_ss [has_vector_derivative, HAS_DERIVATIVE_AT_WITHIN]
2157QED
2158
2159Theorem MVT_ALT :
2160 !f f' a b.
2161 a < b /\ f continuous_on interval[a,b] /\
2162 (!x. x IN interval(a,b) ==> (f has_vector_derivative f' x) (at x))
2163 ==> ?x. x IN interval(a,b) /\ (f(b) - f(a) = f' x * (b - a))
2164Proof
2165 rw [has_vector_derivative]
2166 >> qabbrev_tac ‘g = (\x t. t * f' x)’ >> fs []
2167 >> ‘!x. (\t. g x t) = g x’ by rw [FUN_EQ_THM]
2168 >> POP_ASSUM (fs o wrap)
2169 >> ‘!x. f' x * (b - a) = g x (b - a)’ by rw [Abbr ‘g’] >> POP_ORW
2170 >> MATCH_MP_TAC MVT >> art []
2171QED
2172
2173Theorem MVT_GENERAL_ALT :
2174 !f f' a b.
2175 a < b /\ f continuous_on interval[a,b] /\
2176 (!x. x IN interval(a,b) ==> (f has_vector_derivative f' x) (at x))
2177 ==> ?x. x IN interval(a,b) /\ abs (f b - f a) <= abs (f' x * (b - a))
2178Proof
2179 rw [has_vector_derivative]
2180 >> qabbrev_tac ‘g = (\x t. t * f' x)’ >> fs []
2181 >> ‘!x. (\t. g x t) = g x’ by rw [FUN_EQ_THM]
2182 >> POP_ASSUM (fs o wrap)
2183 >> ‘!x. f' x * (b - a) = g x (b - a)’ by rw [Abbr ‘g’] >> POP_ORW
2184 >> MATCH_MP_TAC MVT_GENERAL >> art []
2185QED
2186
2187(* ------------------------------------------------------------------------- *)
2188(* CONTINUOUS_ON_EXP *)
2189(* ------------------------------------------------------------------------- *)
2190
2191(* See limTheory.HAS_DERIVATIVE_POW' for a better version without sum *)
2192Theorem HAS_DERIVATIVE_POW:
2193 !q0 n.
2194 ((\q. q pow n) has_derivative
2195 (\q. sum { 1n..n} (\i. q0 pow (n - i) * q * q0 pow (i - 1))))
2196 (at q0)
2197Proof
2198 GEN_TAC THEN INDUCT_TAC THENL
2199 [`0 < 1:num` by SIMP_TAC arith_ss [] THEN
2200 FULL_SIMP_TAC real_ss [GSYM NUMSEG_EMPTY, SUM_CLAUSES, pow] THEN
2201 MATCH_ACCEPT_TAC HAS_DERIVATIVE_CONST, ALL_TAC] THEN
2202 REWRITE_TAC[pow, SUM_CLAUSES_NUMSEG, ARITH_PROVE ``1 <= SUC n``,
2203 REAL_SUB_REFL, REAL_MUL_LID, ARITH_PROVE ``SUC n - 1 = n``] THEN
2204 SUBGOAL_THEN
2205 ``!q. sum { 1n..n} (\i. q0 pow (SUC n - i) * q * q0 pow (i - 1)) =
2206 q0 * sum { 1n..n} (\i. q0 pow (n - i) * q * q0 pow (i - 1))``
2207 (fn th => REWRITE_TAC[th]) THENL
2208 [GEN_TAC THEN SIMP_TAC std_ss [FINITE_NUMSEG, GSYM SUM_LMUL] THEN
2209 MATCH_MP_TAC SUM_EQ' THEN
2210 REWRITE_TAC [IN_NUMSEG, FUN_EQ_THM] THEN REPEAT STRIP_TAC THEN
2211 ASM_SIMP_TAC std_ss [ARITH_PROVE ``x <= n ==> (SUC n - x = SUC (n - x))``,
2212 pow, GSYM REAL_MUL_ASSOC], ALL_TAC] THEN
2213 MP_TAC (Q.ISPEC `(at (q0:real))` HAS_DERIVATIVE_ID) THEN DISCH_TAC THEN
2214 FULL_SIMP_TAC real_ss [] THEN
2215 Q_TAC SUFF_TAC `((\q. (\q. q) q * (\q. q pow n) q) has_derivative
2216 (\q. (\q. q) q0 * (\q. sum {1 .. n} (\i. q0 pow (n - i) * q * q0 pow (i - 1))) q +
2217 (\q. q) q * (\q. q pow n) q0)) (at q0)` THENL
2218 [SIMP_TAC std_ss [], ALL_TAC] THEN MATCH_MP_TAC HAS_DERIVATIVE_MUL_AT THEN
2219 ASM_SIMP_TAC std_ss [HAS_DERIVATIVE_ID]
2220QED
2221
2222Theorem EXP_CONVERGES_UNIFORMLY_CAUCHY:
2223 !R e. &0 < e /\ &0 < R
2224 ==> ?N. !m n z. m >= N /\ abs(z) <= R
2225 ==> abs(sum{m..n} (\i. z pow i / (&(FACT i)))) < e
2226Proof
2227 REPEAT STRIP_TAC THEN
2228 MP_TAC(Q.ISPECL [`&1 / &2:real`, `\i. R pow i / (&(FACT i):real)`,
2229 `from 0`] SERIES_RATIO) THEN
2230 SIMP_TAC real_ss [SERIES_CAUCHY, LEFT_FORALL_IMP_THM] THEN
2231 MP_TAC(Q.SPEC `&2 * abs(R)` SIMP_REAL_ARCH) THEN
2232 MATCH_MP_TAC(TAUT `(a ==> b) /\ (c ==> d) ==> a ==> (b ==> c) ==> d`) THEN
2233 CONJ_TAC THENL
2234 [DISCH_THEN (X_CHOOSE_TAC ``N:num``) THEN Q.EXISTS_TAC `N:num` THEN
2235 X_GEN_TAC ``n:num`` THEN REWRITE_TAC[GE] THEN DISCH_TAC THEN
2236 SIMP_TAC real_ss [FACT, pow, real_div] THEN
2237 `inv (&(FACT n * SUC n)) = inv (&(FACT n):real) * inv (&(SUC n))` by
2238 (ONCE_REWRITE_TAC [GSYM REAL_OF_NUM_MUL] THEN MATCH_MP_TAC REAL_INV_MUL THEN
2239 SIMP_TAC real_ss [] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN MATCH_MP_TAC LESS_NOT_EQ THEN
2240 SIMP_TAC arith_ss [FACT_LESS]) THEN
2241 POP_ASSUM (fn th => SIMP_TAC real_ss [th]) THEN SIMP_TAC real_ss [ABS_MUL] THEN
2242 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * (c * d) = (a * d) * (b * c:real)``] THEN
2243 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC real_ss [REAL_LE_REFL] THEN
2244 SIMP_TAC real_ss [REAL_LE_MUL, ABS_POS, ABS_INV, REAL_INV_1OVER] THEN
2245 SIMP_TAC real_ss [REAL_LE_RDIV_EQ, REAL_ARITH ``a * b * c = (a * c) * b:real``] THEN
2246 REWRITE_TAC [GSYM real_div, GSYM REAL_INV_1OVER] THEN
2247 `0:real < abs (&SUC n)` by SIMP_TAC real_ss [GSYM ABS_NZ] THEN
2248 ASM_SIMP_TAC real_ss [REAL_LE_LDIV_EQ] THEN ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN
2249 MATCH_MP_TAC REAL_LE_TRANS THEN Q.EXISTS_TAC `&N` THEN ASM_SIMP_TAC real_ss [] THEN
2250 MATCH_MP_TAC REAL_LE_TRANS THEN Q.EXISTS_TAC `&n` THEN
2251 ASM_SIMP_TAC real_ss [REAL_OF_NUM_LE, ADD1] THEN
2252 REWRITE_TAC [GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC, ALL_TAC] THEN
2253 DISCH_THEN(MP_TAC o Q.SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
2254 STRIP_TAC THEN Q.EXISTS_TAC `N` THEN POP_ASSUM MP_TAC THEN
2255 REWRITE_TAC[FROM_0, INTER_UNIV] THEN DISCH_TAC THEN GEN_TAC THEN
2256 GEN_TAC THEN POP_ASSUM (MP_TAC o Q.SPECL [`m`,`n`]) THEN
2257 DISCH_THEN(fn th => REPEAT STRIP_TAC THEN MP_TAC th) THEN
2258 ASM_REWRITE_TAC [] THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
2259 Q.EXISTS_TAC `abs (sum {m .. n} (\i. R pow i / &FACT i))` THEN
2260 ASM_REWRITE_TAC [] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
2261 Q.EXISTS_TAC `sum {m .. n} (\i. R pow i / &FACT i)` THEN
2262 SIMP_TAC std_ss [ABS_LE] THEN MATCH_MP_TAC SUM_ABS_LE' THEN
2263 RW_TAC std_ss [FINITE_NUMSEG, ABS_MUL, real_div] THEN
2264 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC std_ss [ABS_POS] THEN
2265 CONJ_TAC THENL
2266 [REWRITE_TAC [GSYM POW_ABS] THEN MATCH_MP_TAC POW_LE THEN
2267 ASM_SIMP_TAC std_ss [ABS_POS], ALL_TAC] THEN
2268 SIMP_TAC std_ss [REAL_LE_LT] THEN DISJ2_TAC THEN
2269 REWRITE_TAC [ABS_REFL] THEN MATCH_MP_TAC REAL_LE_INV THEN
2270 SIMP_TAC std_ss [REAL_LE_LT] THEN DISJ1_TAC THEN
2271 SIMP_TAC std_ss [FACT_LESS, REAL_LT]
2272QED
2273
2274Theorem REAL_MUL_NZ:
2275 !a b:real. a <> 0 /\ b <> 0 ==> a * b <> 0
2276Proof
2277 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [MONO_NOT_EQ] THEN
2278 SIMP_TAC real_ss [REAL_ENTIRE]
2279QED
2280
2281(* `sum (0, SUC n)` is defined by realTheory.sum
2282 `sum {0 .. n}` is defined by iterateTheory.sum_def
2283 *)
2284Theorem lemma_sum_eq[local] :
2285 !n x:real. sum (0, SUC n) (\n. (\n. inv(&(FACT n))) n * (x pow n)) =
2286 sum {0 .. n} (\n. (\n. inv(&(FACT n))) n * (x pow n))
2287Proof
2288 NTAC 2 GEN_TAC
2289 >> SIMP_TAC std_ss [sum_def, iterate, support]
2290 >> Know `FINITE {n' | n' IN {0 .. n} /\ inv(&FACT n') * x pow n' <> neutral $+}`
2291 >- (MATCH_MP_TAC FINITE_SUBSET \\
2292 Q.EXISTS_TAC `{0 .. n}` \\
2293 SIMP_TAC std_ss [FINITE_NUMSEG] >> SET_TAC [])
2294 >> DISCH_TAC
2295 >> ASM_SIMP_TAC std_ss []
2296 >> Know `neutral $+ = 0:real`
2297 >- (SIMP_TAC std_ss [neutral] >> MATCH_MP_TAC SELECT_UNIQUE \\
2298 RW_TAC real_ss [] \\
2299 reverse EQ_TAC >- REAL_ARITH_TAC \\
2300 DISCH_THEN (MP_TAC o Q.SPEC `1`) >> REAL_ARITH_TAC)
2301 >> DISCH_THEN ((FULL_SIMP_TAC std_ss) o wrap)
2302 (* applying ITSET_alt *)
2303 >> Q.ABBREV_TAC ‘f = (\n a. inv (&FACT n) * x pow n + a)’
2304 >> Q.ABBREV_TAC ‘s = {n' | n' IN {0 .. n} /\ inv (&FACT n') * x pow n' <> 0}’
2305 >> Q.ABBREV_TAC ‘b = 0’
2306 >> Know ‘ITSET f s b =
2307 (@g. g {} = b /\
2308 !x s. FINITE s ==>
2309 g (x INSERT s) = if x IN s then g s else f x (g s)) s’
2310 >- (MATCH_MP_TAC ITSET_alt >> rw [Abbr ‘f’] \\
2311 REAL_ARITH_TAC)
2312 >> Rewr'
2313 >> qunabbrevl_tac [‘f’, ‘s’, ‘b’]
2314 (* end of changes *)
2315 >> SELECT_ELIM_TAC
2316 >> CONJ_TAC
2317 >- (Q.EXISTS_TAC `(\s. sum s (\n. (\n. inv(&(FACT n))) n * (x pow n)))` \\
2318 SIMP_TAC std_ss [SUM_CLAUSES])
2319 >> RW_TAC std_ss [] THEN ASM_CASES_TAC ``x = 0:real`` THENL
2320 [ASM_SIMP_TAC real_ss [ADD1] THEN ONCE_REWRITE_TAC [ADD_COMM] THEN
2321 SIMP_TAC std_ss [GSYM SUM_TWO] THEN
2322 Q_TAC SUFF_TAC `{n' | n' IN {0 .. n} /\ inv (&FACT n') * 0r pow n' <> 0} = {0}` THENL
2323 [DISCH_TAC,
2324 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_SING, IN_NUMSEG] THEN
2325 GEN_TAC THEN EQ_TAC THENL
2326 [STRIP_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC [MONO_NOT_EQ] THEN
2327 RW_TAC arith_ss [] THEN `0 < x''` by METIS_TAC [LESS_0_CASES] THEN
2328 FULL_SIMP_TAC std_ss [SUC_PRE] THEN
2329 POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN
2330 ONCE_ASM_REWRITE_TAC [] THEN SIMP_TAC arith_ss [POW_0] THEN
2331 REAL_ARITH_TAC, ALL_TAC] THEN
2332 DISC_RW_KILL THEN SIMP_TAC real_ss [FACT, pow] THEN
2333 SIMP_TAC real_ss [REAL_INV_1OVER]] THEN
2334 ASM_REWRITE_TAC [] THEN FIRST_X_ASSUM (MP_TAC o Q.SPECL [`0`,`{}`]) THEN
2335 ASM_SIMP_TAC real_ss [FINITE_EMPTY, NOT_IN_EMPTY, FACT, pow, REAL_INV_1OVER] THEN
2336 DISCH_TAC THEN SIMP_TAC real_ss [SUM_1, FACT, pow, REAL_ADD_RID_UNIQ] THEN
2337 Q_TAC SUFF_TAC `(!n:num. n >= 1 ==> ((\n'. 1 / &FACT n' * 0 pow n') n = 0:real))` THENL
2338 [DISCH_THEN (MP_TAC o MATCH_MP SUM_ZERO) THEN DISCH_THEN (MATCH_MP_TAC) THEN
2339 ARITH_TAC, ALL_TAC] THEN
2340 RW_TAC arith_ss [GE] THEN `0 < n'` by (ASM_SIMP_TAC arith_ss []) THEN
2341 FULL_SIMP_TAC std_ss [SUC_PRE] THEN
2342 POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN
2343 ONCE_ASM_REWRITE_TAC [] THEN SIMP_TAC real_ss [POW_0],
2344 ALL_TAC] THEN
2345 Q_TAC SUFF_TAC `!n. inv (&FACT n) * x pow n <> 0` THENL
2346 [DISCH_TAC,
2347 GEN_TAC THEN MATCH_MP_TAC REAL_MUL_NZ THEN ASM_SIMP_TAC std_ss [POW_NZ] THEN
2348 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN
2349 MATCH_MP_TAC REAL_INV_POS THEN SIMP_TAC arith_ss [REAL_LT, FACT_LESS]] THEN
2350 ASM_SIMP_TAC real_ss [] THEN
2351 Q_TAC SUFF_TAC `(\p v.
2352 (!n s. FINITE s ==> (x' (n INSERT s) = if n IN s then x' s else v n + x' s)) ==>
2353 (sum (FST p, SUC (SND p) - FST p) v = x' {n' | n' IN {FST p .. SND p}}))
2354 (0, n) (\n. inv (&FACT n) * x pow n)` THENL
2355 [ASM_SIMP_TAC arith_ss [], ALL_TAC] THEN MATCH_MP_TAC sum_ind THEN RW_TAC std_ss [] THENL
2356 [SIMP_TAC arith_ss [SUM_1, IN_NUMSEG] THEN
2357 ASM_CASES_TAC ``n' = 0:num`` THENL
2358 [ASM_SIMP_TAC arith_ss [SUM_1] THEN
2359 ONCE_REWRITE_TAC [SET_RULE ``{n'':num | n'' = 0} = {0}``] THEN
2360 FIRST_X_ASSUM (MP_TAC o Q.SPECL [`0`,`{}`]) THEN
2361 ASM_SIMP_TAC real_ss [FINITE_EMPTY, NOT_IN_EMPTY, FACT, pow, REAL_INV_1OVER] THEN
2362 DISCH_THEN (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN
2363 ASM_SIMP_TAC real_ss [], ALL_TAC] THEN
2364 `1 - n' = 0` by (ASM_SIMP_TAC arith_ss []) THEN
2365 Q_TAC SUFF_TAC `{n'' | n' <= n'' /\ (n'' = 0)} = {}` THENL
2366 [DISC_RW_KILL, ASM_SIMP_TAC arith_ss [EXTENSION, NOT_IN_EMPTY, GSPECIFICATION]] THEN
2367 ASM_SIMP_TAC real_ss [sum], ALL_TAC] THEN
2368 FULL_SIMP_TAC std_ss [] THEN
2369 ONCE_REWRITE_TAC [SET_RULE “{n'' | n'' IN {n' .. SUC m}} = {n' .. SUC m}”] >>
2370 ASM_CASES_TAC ``SUC m < n'`` THENL
2371 [`{n' .. SUC m} = {}` by METIS_TAC [NUMSEG_EMPTY] THEN
2372 `SUC (SUC m) - n' = 0` by ASM_SIMP_TAC arith_ss [] THEN
2373 ASM_SIMP_TAC std_ss [sum], ALL_TAC] THEN
2374 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
2375 POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN
2376 FIRST_X_ASSUM (MP_TAC o Q.SPECL [`SUC (m)`,`{n' .. m}`]) THEN
2377 RW_TAC arith_ss [FINITE_NUMSEG, IN_NUMSEG] THEN
2378 Q_TAC SUFF_TAC `(SUC m INSERT {n' .. m}) = {n' .. m + 1}` THENL
2379 [DISCH_TAC THEN FULL_SIMP_TAC arith_ss [GSYM ADD1],
2380 ASM_SIMP_TAC arith_ss [EXTENSION, IN_NUMSEG, IN_INSERT, ADD1]] THEN
2381 `{n'' | n'' IN {n' .. m}} = {n' .. m}` by SET_TAC [] THEN
2382 FULL_SIMP_TAC std_ss [] THEN
2383 `SUC (SUC m) - n' = SUC (SUC m - n')` by ASM_SIMP_TAC arith_ss [] THEN
2384 ASM_SIMP_TAC std_ss [] THEN ONCE_REWRITE_TAC [sum] THEN
2385 ASM_SIMP_TAC arith_ss [REAL_ADD_COMM]
2386QED
2387
2388(* cf. transcTheory.EXP_CONVERGES *)
2389Theorem EXP_CONVERGES :
2390 !z. ((\n. z pow n / (&(FACT n))) sums exp(z)) (from 0)
2391Proof
2392 RW_TAC std_ss [exp_def, FROM_0]
2393 >> ONCE_REWRITE_TAC [REAL_MUL_COMM] >> REWRITE_TAC [GSYM real_div]
2394 >> SIMP_TAC std_ss [SUMS_INFSUM, summable_def, SERIES_CAUCHY]
2395 >> REWRITE_TAC[INTER_UNIV]
2396 >> MP_TAC(Q.SPEC `abs(z) + &1` EXP_CONVERGES_UNIFORMLY_CAUCHY)
2397 >> SIMP_TAC std_ss [REAL_ARITH ``&0 <= x ==> &0 < x + &1:real``, ABS_POS]
2398 >> METIS_TAC [REAL_ARITH ``x:real <= x + &1``]
2399QED
2400
2401Theorem EXP_CONVERGES_UNIQUE:
2402 !w z. ((\n. z pow n / (&(FACT n))) sums w) (from 0) <=> (w = exp(z))
2403Proof
2404 REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC std_ss [EXP_CONVERGES] THEN
2405 DISCH_THEN(MP_TAC o C CONJ (Q.SPEC `z` EXP_CONVERGES)) THEN
2406 REWRITE_TAC[SERIES_UNIQUE]
2407QED
2408
2409Theorem EXP_CONVERGES_UNIFORMLY:
2410 !R e. &0 < R /\ &0 < e
2411 ==> ?N. !n z. n >= N /\ abs(z) < R
2412 ==> abs(sum{ 0n..n} (\i. z pow i / (&(FACT i))) - exp(z)) <= e
2413Proof
2414 REPEAT STRIP_TAC THEN
2415 MP_TAC(Q.SPECL [`R:real`, `e / &2`] EXP_CONVERGES_UNIFORMLY_CAUCHY) THEN
2416 ASM_REWRITE_TAC[REAL_HALF] THEN STRIP_TAC THEN Q.EXISTS_TAC `N` THEN
2417 MAP_EVERY X_GEN_TAC [``n:num``, ``z:real``] THEN STRIP_TAC THEN
2418 MP_TAC(Q.SPEC `z` EXP_CONVERGES) THEN
2419 SIMP_TAC std_ss [sums_def, LIM_SEQUENTIALLY, FROM_0, INTER_UNIV, dist] THEN
2420 DISCH_THEN(MP_TAC o Q.SPEC `e / &2`) THEN ASM_REWRITE_TAC[REAL_HALF] THEN
2421 DISCH_THEN(X_CHOOSE_THEN ``M:num`` (MP_TAC o Q.SPEC `n + M + 1`)) THEN
2422 FIRST_X_ASSUM(MP_TAC o Q.SPECL [`n + 1`, `n + M + 1`, `z`]) THEN
2423 ASM_SIMP_TAC std_ss
2424 [ARITH_PROVE ``(n >= N ==> n + 1 >= N) /\ M <= n + M + 1:num``] THEN
2425 ASM_SIMP_TAC std_ss [REAL_LT_IMP_LE, LE_0] THEN
2426 Q.ABBREV_TAC `f = (\i. z pow i / &FACT i)` THEN
2427 `0 <= n + 1` by ASM_SIMP_TAC arith_ss [] THEN
2428 ONCE_REWRITE_TAC [ARITH_PROVE ``n + M + 1 = n + (M + 1:num)``] THEN
2429 FIRST_X_ASSUM (MP_TAC o MATCH_MP SUM_ADD_SPLIT) THEN
2430 DISCH_THEN (ASSUME_TAC o Q.SPECL [`f`,`M + 1`]) THEN
2431 ONCE_ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN
2432 GEN_REWR_TAC (RAND_CONV o RAND_CONV o RAND_CONV) [GSYM REAL_HALF] THEN
2433 REAL_ARITH_TAC
2434QED
2435
2436Theorem HAS_DERIVATIVE_EXP:
2437 !z. (exp has_derivative (\y. exp z * y)) (at z)
2438Proof
2439 REPEAT GEN_TAC THEN MP_TAC(Q.ISPECL
2440 [`ball((&0),abs(z:real) + &1)`,
2441 `\n z. z pow n / (&(FACT n):real)`,
2442 `\n z:real. if n = 0 then (&0) else z pow (n-1) / (&(FACT(n-1)))`,
2443 `exp:real->real`, `from (0)`]
2444 HAS_DERIVATIVE_SERIES') THEN
2445 SIMP_TAC real_ss [CONVEX_BALL, OPEN_BALL, IN_BALL, dist] THEN
2446 SIMP_TAC real_ss [HAS_DERIVATIVE_WITHIN_OPEN, OPEN_BALL, IN_BALL,
2447 dist, REAL_SUB_LZERO, REAL_SUB_RZERO, ABS_NEG] THEN
2448 Q_TAC SUFF_TAC `(!n x.
2449 abs x < abs z + 1 ==>
2450 ((\z. z pow n / &FACT n) has_derivative
2451 (\y. (if n = 0 then 0 else x pow (n - 1) / &FACT (n - 1)) * y))
2452 (at x)) /\
2453 (!e. 0 < e ==>
2454 ?N. !n x. n >= N /\ abs x < abs z + 1 ==>
2455 abs (sum (from 0 INTER {0 .. n})
2456 (\i. if i = 0 then 0 else x pow (i - 1) / &FACT (i - 1)) -
2457 exp x) <= e) /\
2458 (?x l. abs x < abs z + 1 /\ ((\n. x pow n / &FACT n) sums l) (from 0))` THENL
2459 [DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN
2460 DISCH_THEN(X_CHOOSE_THEN ``g:real->real`` MP_TAC) THEN
2461 REWRITE_TAC[EXP_CONVERGES_UNIQUE] THEN STRIP_TAC THEN
2462 MATCH_MP_TAC HAS_DERIVATIVE_TRANSFORM_AT THEN
2463 MAP_EVERY Q.EXISTS_TAC [`g`, `&1`] THEN
2464 REWRITE_TAC[REAL_LT_01] THEN CONJ_TAC THENL
2465 [ALL_TAC,
2466 FIRST_X_ASSUM(MP_TAC o Q.SPEC `z`) THEN
2467 Q_TAC SUFF_TAC `abs z < abs z + 1` THENL
2468 [METIS_TAC [ETA_AX], REAL_ARITH_TAC]] THEN
2469 GEN_TAC THEN POP_ASSUM (MP_TAC o Q.SPEC `x'`) THEN
2470 MATCH_MP_TAC MONO_IMP THEN SIMP_TAC std_ss [dist] THEN
2471 REAL_ARITH_TAC, ALL_TAC] THEN
2472 REPEAT CONJ_TAC THENL
2473 [ALL_TAC,
2474 REPEAT STRIP_TAC THEN
2475 MP_TAC(Q.SPECL [`abs(z) + &1`, `e`] EXP_CONVERGES_UNIFORMLY) THEN
2476 ASM_SIMP_TAC std_ss [ABS_POS, REAL_ARITH ``&0 <= x ==> &0 < x + &1:real``] THEN
2477 DISCH_THEN(X_CHOOSE_TAC ``N:num``) THEN Q.EXISTS_TAC `N + 1` THEN
2478 MAP_EVERY X_GEN_TAC [``n:num``, ``w:real``] THEN STRIP_TAC THEN
2479 FIRST_X_ASSUM(MP_TAC o Q.SPECL [`n - 1`, `w`]) THEN
2480 ASM_SIMP_TAC std_ss [ARITH_PROVE ``n >= m + 1 ==> n - 1 >= m:num``] THEN
2481 REWRITE_TAC[FROM_0, INTER_UNIV] THEN MATCH_MP_TAC EQ_IMPLIES THEN
2482 AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
2483 AP_THM_TAC THEN AP_TERM_TAC THEN
2484 SUBGOAL_THEN ``{ 0n..n} = 0 INSERT (IMAGE SUC { 0n..n-1})`` SUBST1_TAC THENL
2485 [REWRITE_TAC[EXTENSION, IN_INSERT, IN_IMAGE, IN_NUMSEG] THEN
2486 INDUCT_TAC THEN SIMP_TAC arith_ss [] THEN
2487 UNDISCH_TAC ``n >= N + 1:num`` THEN ARITH_TAC,
2488 ALL_TAC] THEN
2489 SIMP_TAC std_ss [SUM_CLAUSES, IMAGE_FINITE, FINITE_NUMSEG] THEN
2490 SIMP_TAC real_ss [IN_IMAGE, NOT_SUC, SUC_NOT, REAL_ADD_LID] THEN
2491 SIMP_TAC std_ss [SUM_IMAGE, FINITE_NUMSEG] THEN
2492 MATCH_MP_TAC SUM_EQ' THEN SIMP_TAC real_ss [IN_NUMSEG, NOT_SUC, o_THM, SUC_SUB1],
2493 MAP_EVERY Q.EXISTS_TAC [`(&0)`, `exp((&0))`] THEN
2494 REWRITE_TAC[EXP_CONVERGES, ABS_0] THEN
2495 SIMP_TAC std_ss [REAL_ARITH ``&0 <= z ==> &0 < z + &1:real``, ABS_POS]] THEN
2496 X_GEN_TAC ``n:num`` THEN REPEAT STRIP_TAC THEN
2497 ASM_CASES_TAC ``n = 0:num`` THEN ASM_REWRITE_TAC [] THENL
2498 [SIMP_TAC real_ss [pow, FACT, HAS_DERIVATIVE_CONST], ALL_TAC] THEN
2499 SIMP_TAC std_ss [real_div] THEN ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN
2500 ONCE_REWRITE_TAC [REAL_ARITH ``a * (b * c) = c * b * a:real``] THEN
2501 Q_TAC SUFF_TAC `!y. inv (&FACT (n - 1)) * x pow (n - 1) * y =
2502 inv (&FACT n) * (&n * x pow (n - 1) * y)` THENL
2503 [DISC_RW_KILL,
2504 RW_TAC real_ss [REAL_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2505 AP_THM_TAC THEN AP_TERM_TAC THEN `0 < n` by ASM_SIMP_TAC arith_ss [] THEN
2506 `?m. n = SUC m` by (Q.EXISTS_TAC `PRE n` THEN ASM_SIMP_TAC arith_ss [SUC_PRE]) THEN
2507 ASM_SIMP_TAC std_ss [SUC_SUB1, FACT, GSYM REAL_OF_NUM_MUL] THEN
2508 `~(&SUC m = &0:real)` by ASM_SIMP_TAC arith_ss [NOT_SUC, REAL_OF_NUM_EQ] THEN
2509 ASM_SIMP_TAC real_ss [REAL_FACT_NZ, REAL_INV_MUL] THEN
2510 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c = a * c * b:real``] THEN
2511 ASM_SIMP_TAC real_ss [REAL_MUL_LINV]] THEN
2512 Q_TAC SUFF_TAC `((\z. inv (&FACT n) * (\z. z pow n) z) has_derivative
2513 (\y. inv (&FACT n) * (\y. (&n * x pow (n - 1) * y)) y)) (at x)` THENL
2514 [SIMP_TAC std_ss [], ALL_TAC] THEN
2515 MATCH_MP_TAC HAS_DERIVATIVE_CMUL THEN
2516 Q_TAC SUFF_TAC `(\y. &n * x pow (n - 1) * y) =
2517 (\y. sum {1 .. n} (\i. x pow (n - i) * y * x pow (i - 1)))` THENL
2518 [DISC_RW_KILL THEN SIMP_TAC std_ss [HAS_DERIVATIVE_POW], ALL_TAC] THEN
2519 `FINITE {1 .. n}` by SIMP_TAC std_ss [FINITE_NUMSEG] THEN
2520 POP_ASSUM (MP_TAC o MATCH_MP SUM_CONST) THEN
2521 DISCH_THEN (MP_TAC o Q.SPEC `x pow (n - 1)`) THEN SIMP_TAC arith_ss [CARD_NUMSEG] THEN
2522 DISCH_THEN (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN
2523 ASM_REWRITE_TAC [] THEN
2524 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c = (a * c) * b:real``] THEN
2525 ABS_TAC THEN SIMP_TAC std_ss [SUM_RMUL] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2526 MATCH_MP_TAC SUM_EQ' THEN SIMP_TAC arith_ss [GSYM POW_ADD, IN_NUMSEG]
2527QED
2528
2529Theorem HAS_DERIVATIVE_IMP_CONTINUOUS_AT:
2530 !f f' x. (f has_derivative f') (at x) ==> f continuous at x
2531Proof
2532 RW_TAC std_ss [] THEN MATCH_MP_TAC DIFFERENTIABLE_IMP_CONTINUOUS_AT THEN
2533 METIS_TAC[differentiable]
2534QED
2535
2536Theorem CONTINUOUS_AT_EXP:
2537 !z. exp continuous at z
2538Proof
2539 METIS_TAC[HAS_DERIVATIVE_EXP, HAS_DERIVATIVE_IMP_CONTINUOUS_AT]
2540QED
2541
2542Theorem CONTINUOUS_WITHIN_EXP:
2543 !s z. exp continuous (at z within s)
2544Proof
2545 METIS_TAC[CONTINUOUS_AT_WITHIN, CONTINUOUS_AT_EXP]
2546QED
2547
2548Theorem CONTINUOUS_ON_EXP:
2549 !s. exp continuous_on s
2550Proof
2551 METIS_TAC[CONTINUOUS_AT_IMP_CONTINUOUS_ON, CONTINUOUS_AT_EXP]
2552QED
2553
2554(* ------------------------------------------------------------------------- *)
2555(* Characterizations of convex functions in terms of secants. *)
2556(* (Ported from HOL-Light's Multivariate/convex.ml) *)
2557(* ------------------------------------------------------------------------- *)
2558
2559Theorem CONVEX_ON_SECANT_MUL_combined[local] :
2560 (!f s:real->bool.
2561 f convex_on s <=>
2562 !a b x. a IN s /\ b IN s /\ x IN segment[a,b]
2563 ==> (f x - f a) * abs(b - a) <= (f b - f a) * abs(x - a)) /\
2564 (!f s:real->bool.
2565 f convex_on s <=>
2566 !a b x. a IN s /\ b IN s /\ x IN segment[a,b]
2567 ==> (f b - f a) * abs(b - x) <= (f b - f x) * abs(b - a)) /\
2568 (!f s:real->bool.
2569 f convex_on s <=>
2570 !a b x. a IN s /\ b IN s /\ x IN segment[a,b]
2571 ==> (f x - f a) * abs(b - x) <= (f b - f x) * abs(x - a))
2572Proof
2573 REPEAT CONJ_TAC THEN (* 3 subgoals, same tactics *)
2574 REPEAT GEN_TAC THEN REWRITE_TAC[convex_on] THEN
2575 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites [FUN_EQ_THM] THEN
2576 Q.X_GEN_TAC `a:real` THEN BETA_TAC THEN
2577 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites [FUN_EQ_THM] THEN
2578 Q.X_GEN_TAC `b:real` THEN BETA_TAC THEN
2579 ASM_CASES_TAC ``(a:real) IN s`` THEN ASM_REWRITE_TAC[] THEN
2580 ASM_CASES_TAC ``(b:real) IN s`` THEN ASM_REWRITE_TAC[] THEN
2581 SIMP_TAC pure_ss[IN_SEGMENT, LEFT_IMP_EXISTS_THM] THEN
2582 Ho_Rewrite.ONCE_REWRITE_TAC [SWAP_FORALL_THM] THEN
2583 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites [FUN_EQ_THM] THEN
2584 Q.X_GEN_TAC `u:real` THEN BETA_TAC THEN
2585 REWRITE_TAC[TAUT `a /\ x = y <=> x = y /\ a`,
2586 TAUT `a /\ x = y /\ b <=> x = y /\ a /\ b`] THEN
2587 REWRITE_TAC[REAL_ARITH ``v + u = &1 <=> v = &1 - u``] THEN
2588 SIMP_TAC bool_ss[FORALL_UNWIND_THM2, IMP_CONJ] THEN
2589 REWRITE_TAC[REAL_SUB_LE] THEN
2590 ASM_CASES_TAC ``&0 <= u`` THEN ASM_REWRITE_TAC[] THEN
2591 ASM_CASES_TAC ``u <= &1`` THEN ASM_REWRITE_TAC[] THEN
2592 REWRITE_TAC[REAL_ARITH ``((&1 - u) * a + u * b) - a:real = u * (b - a)``,
2593 REAL_ARITH ``b - ((&1 - u) * a + u * b):real = (&1 - u) * (b - a)``] THEN
2594 REWRITE_TAC[ABS_MUL, REAL_MUL_ASSOC] THEN
2595 (ASM_CASES_TAC ``b:real = a`` THENL
2596 [ASM_REWRITE_TAC[REAL_SUB_REFL,
2597 REAL_ARITH ``(&1 - u) * a + u * a:real = a``] THEN
2598 REAL_ARITH_TAC,
2599 ‘0 < abs (b - a)’ by simp [GSYM ABS_NZ, REAL_SUB_0] THEN
2600 ASM_SIMP_TAC std_ss[REAL_LE_RMUL] THEN
2601 ASM_SIMP_TAC std_ss[REAL_ARITH
2602 ``&0 <= u /\ u <= &1 ==> abs u = u /\ abs(&1 - u) = &1 - u``] THEN
2603 REAL_ARITH_TAC])
2604QED
2605
2606Theorem CONVEX_ON_LEFT_SECANT_MUL = CONVEX_ON_SECANT_MUL_combined |> cj 1
2607Theorem CONVEX_ON_RIGHT_SECANT_MUL = CONVEX_ON_SECANT_MUL_combined |> cj 2
2608Theorem CONVEX_ON_MID_SECANT_MUL = CONVEX_ON_SECANT_MUL_combined |> cj 3
2609
2610Theorem CONVEX_ON_SECANT_combined[local] :
2611 (!f s:real->bool.
2612 f convex_on s <=>
2613 !a b x. a IN s /\ b IN s /\ x IN segment(a,b)
2614 ==> (f x - f a) / abs(x - a) <= (f b - f a) / abs(b - a)) /\
2615 (!f s:real->bool.
2616 f convex_on s <=>
2617 !a b x. a IN s /\ b IN s /\ x IN segment(a,b)
2618 ==> (f b - f a) / abs(b - a) <= (f b - f x) / abs(b - x)) /\
2619 (!f s:real->bool.
2620 f convex_on s <=>
2621 !a b x. a IN s /\ b IN s /\ x IN segment(a,b)
2622 ==> (f x - f a) / abs(x - a) <= (f b - f x) / abs(b - x))
2623Proof
2624 REPEAT CONJ_TAC THEN REPEAT GEN_TAC THENL
2625 [REWRITE_TAC[CONVEX_ON_LEFT_SECANT_MUL],
2626 REWRITE_TAC[CONVEX_ON_RIGHT_SECANT_MUL],
2627 REWRITE_TAC[CONVEX_ON_MID_SECANT_MUL]] THEN (* 3 subgoals, same tactics *)
2628 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites[FUN_EQ_THM] THEN
2629 Q.X_GEN_TAC `a:real` THEN BETA_TAC THEN
2630 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites[FUN_EQ_THM] THEN
2631 Q.X_GEN_TAC `b:real` THEN BETA_TAC THEN
2632 ASM_CASES_TAC ``(a:real) IN s`` THEN ASM_REWRITE_TAC[] THEN
2633 ASM_CASES_TAC ``(b:real) IN s`` THEN ASM_REWRITE_TAC[] THEN
2634 ASM_CASES_TAC ``a:real = b`` THEN
2635 ASM_REWRITE_TAC[SEGMENT_REFL, NOT_IN_EMPTY, REAL_SUB_REFL, ABS_0,
2636 REAL_MUL_LZERO, REAL_MUL_RZERO, REAL_LE_REFL] THEN
2637 (* only subgoal for ‘a <> b’ is left here *)
2638 SIMP_TAC bool_ss[IN_SING, FORALL_UNWIND_THM2, REAL_LE_REFL] THEN
2639 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites[FUN_EQ_THM] THEN
2640 Q.X_GEN_TAC `x:real` THEN BETA_TAC THEN
2641 REWRITE_TAC[open_segment, IN_DIFF, IN_INSERT, NOT_IN_EMPTY] THEN
2642 MAP_EVERY ASM_CASES_TAC [``x:real = a``, ``x:real = b``] THEN
2643 ASM_REWRITE_TAC[REAL_LE_REFL, REAL_SUB_REFL, ABS_0,
2644 REAL_MUL_LZERO, REAL_MUL_RZERO] THEN (* one goal left *)
2645 ASM_SIMP_TAC std_ss [REAL_LE_RDIV_EQ, GSYM REAL_LE_LDIV_EQ,
2646 GSYM ABS_NZ, REAL_SUB_0] THEN
2647 AP_TERM_TAC THEN REAL_ARITH_TAC
2648QED
2649
2650Theorem CONVEX_ON_LEFT_SECANT = CONVEX_ON_SECANT_combined |> cj 1
2651Theorem CONVEX_ON_RIGHT_SECANT = CONVEX_ON_SECANT_combined |> cj 2
2652Theorem CONVEX_ON_MID_SECANT = CONVEX_ON_SECANT_combined |> cj 3
2653
2654(* ------------------------------------------------------------------------- *)
2655(* Various versions of Kachurovskii's theorem (reduced to R^1). *)
2656(* (Ported from HOL-Light's Multivariate/derivatives.ml) *)
2657(* ------------------------------------------------------------------------- *)
2658
2659Theorem CONVEX_ON_DERIVATIVE_SECANT_IMP :
2660 !f f' s x y:real.
2661 f convex_on s /\ segment[x,y] SUBSET s /\
2662 (f has_derivative f') (at x within s)
2663 ==> f'(y - x) <= f y - f x
2664Proof
2665 REPEAT STRIP_TAC THEN
2666 SUBGOAL_THEN ``(x:real) IN s /\ (y:real) IN s`` ASSUME_TAC THENL
2667 [ASM_MESON_TAC[SUBSET_DEF, ENDS_IN_SEGMENT], ALL_TAC] THEN
2668 FIRST_X_ASSUM
2669 (MP_TAC o GEN_REWRITE_RULE I empty_rewrites[has_derivative_within]) THEN
2670 REWRITE_TAC[LIM_WITHIN, DIST_0, o_THM] THEN
2671 STRIP_TAC THEN ASM_CASES_TAC ``y:real = x`` THENL
2672 [FIRST_X_ASSUM(MP_TAC o MATCH_MP LINEAR_0) THEN
2673 ASM_SIMP_TAC std_ss[REAL_SUB_REFL, REAL_LE_REFL],
2674 ALL_TAC] THEN
2675 (* stage work *)
2676 Q.ABBREV_TAC `e = (f':real->real)(y - x) - (f y - f x)` THEN
2677 ASM_CASES_TAC ``&0 < e`` THENL
2678 [ALL_TAC, qunabbrev_tac ‘e’ >> ASM_REAL_ARITH_TAC] THEN
2679 FIRST_X_ASSUM(MP_TAC o SPEC ``e / &2 / abs(y - x:real)``) THEN
2680 ASM_SIMP_TAC std_ss[REAL_LT_DIV, REAL_HALF, ABS_POS_LT, REAL_SUB_EQ] THEN
2681 DISCH_THEN(X_CHOOSE_THEN ``d:real`` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
2682 Q.ABBREV_TAC `u = min (&1 / &2) (d / &2 / abs (y - x:real))` THEN
2683 SUBGOAL_THEN ``&0 < u /\ u < &1`` STRIP_ASSUME_TAC THENL
2684 [qunabbrev_tac ‘u’ THEN REWRITE_TAC[REAL_LT_MIN, REAL_MIN_LT] THEN
2685 ASM_SIMP_TAC std_ss[REAL_LT_DIV, ABS_POS_LT, REAL_HALF, REAL_SUB_EQ] THEN
2686 simp [],
2687 ALL_TAC] THEN
2688 Q.ABBREV_TAC `z:real = (&1 - u) * x + u * y` THEN
2689 SUBGOAL_THEN ``(z:real) IN segment(x,y)`` MP_TAC THENL
2690 [METIS_TAC [IN_SEGMENT], ALL_TAC] THEN
2691 SIMP_TAC std_ss[open_segment, IN_DIFF, IN_INSERT, NOT_IN_EMPTY, DE_MORGAN_THM] THEN
2692 STRIP_TAC THEN DISCH_THEN(MP_TAC o SPEC ``z:real``) THEN
2693 SUBGOAL_THEN ``(z:real) IN s`` ASSUME_TAC THENL [ASM_SET_TAC[], ALL_TAC] THEN
2694 impl_tac THENL
2695 [ASM_SIMP_TAC std_ss[DIST_POS_LT] THEN
2696 qunabbrev_tac ‘z’ THEN REWRITE_TAC[dist, ABS_MUL, REAL_ARITH
2697 ``((&1 - u) * x + u * y) - x:real = u * (y - x)``] THEN
2698 ASM_SIMP_TAC std_ss[GSYM REAL_LT_RDIV_EQ, ABS_POS_LT, REAL_SUB_EQ] THEN
2699 ‘abs u = u’ by simp [ABS_REDUCE, REAL_LT_IMP_LE] >> POP_ORW \\
2700 simp [Abbr ‘u’, REAL_MIN_LT],
2701 ALL_TAC] THEN
2702 FIRST_ASSUM(MP_TAC o
2703 GEN_REWRITE_RULE I empty_rewrites[CONVEX_ON_LEFT_SECANT]) THEN
2704 DISCH_THEN(MP_TAC o Q.SPECL [`x:real`, `y:real`, `z:real`]) THEN
2705 ASM_REWRITE_TAC[open_segment, IN_DIFF, IN_INSERT, NOT_IN_EMPTY] THEN
2706 SIMP_TAC std_ss
2707 [REAL_ARITH ``inv y * (z - (x + d)):real = (z - x) / y - d / y``] THEN
2708 REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2709 ``z <= y / n /\ abs(z - d) < e / n ==> d <= (y + e) / n``)) THEN
2710 SUBGOAL_THEN
2711 ``(f':real->real)(z - x) / abs(z - x) = f'(y - x) / abs(y - x)``
2712 SUBST1_TAC THENL
2713 [qunabbrev_tac ‘z’ THEN
2714 REWRITE_TAC[REAL_ARITH
2715 ``((&1 - u) * x + u * y) - x:real = u * (y - x)``] THEN
2716 FIRST_ASSUM(MP_TAC o MATCH_MP LINEAR_CMUL) THEN
2717 DISCH_THEN(MP_TAC o Q.SPECL [`u:real`, `y - x:real`]) THEN
2718 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[ABS_MUL] THEN
2719 ‘abs u = u’ by simp [ABS_REDUCE, REAL_LT_IMP_LE] >> POP_ORW THEN
2720 REWRITE_TAC[real_div, REAL_INV_MUL', REAL_MUL_ASSOC] THEN
2721 AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
2722 REWRITE_TAC[GSYM real_div] THEN MATCH_MP_TAC REAL_DIV_LMUL THEN
2723 ASM_REAL_ARITH_TAC,
2724 ASM_SIMP_TAC std_ss[REAL_LE_DIV2_EQ, ABS_POS_LT, REAL_SUB_EQ] THEN
2725 qunabbrev_tac ‘e’ >> REAL_ARITH_TAC]
2726QED
2727
2728Theorem CONVEX_ON_SECANT_DERIVATIVE_IMP :
2729 !f f' s x y:real.
2730 f convex_on s /\ segment[x,y] SUBSET s /\
2731 (f has_derivative f') (at y within s)
2732 ==> f y - f x <= f'(y - x)
2733Proof
2734 ONCE_REWRITE_TAC[SEGMENT_SYM] THEN REPEAT STRIP_TAC THEN
2735 MP_TAC(Q.ISPECL
2736 [`f:real->real`, `f':real->real`, `s:real->bool`,
2737 `y:real`, `x:real`] CONVEX_ON_DERIVATIVE_SECANT_IMP) THEN
2738 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SEGMENT_SYM] THEN
2739 MATCH_MP_TAC(REAL_ARITH
2740 ``f' = -f'' ==> f' <= x - y ==> y - x <= f'' :real``) THEN
2741 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) empty_rewrites[GSYM REAL_NEG_SUB] THEN
2742 Q.SPEC_TAC(`y - x:real`,`z:real`) THEN
2743 MATCH_MP_TAC(REWRITE_RULE[RIGHT_FORALL_IMP_THM] LINEAR_NEG) THEN
2744 ASM_MESON_TAC[has_derivative]
2745QED
2746
2747Theorem CONVEX_ON_DERIVATIVES_IMP :
2748 !f f'x f'y s x y:real.
2749 f convex_on s /\ segment[x,y] SUBSET s /\
2750 (f has_derivative f'x) (at x within s) /\
2751 (f has_derivative f'y) (at y within s)
2752 ==> f'x(y - x) <= f'y(y - x)
2753Proof
2754 ASM_MESON_TAC[CONVEX_ON_DERIVATIVE_SECANT_IMP,
2755 CONVEX_ON_SECANT_DERIVATIVE_IMP,
2756 SEGMENT_SYM, REAL_LE_TRANS]
2757QED
2758
2759Theorem CONVEX_ON_DERIVATIVE_SECANT_combined[local] :
2760 (!f f' s:real->bool.
2761 convex s /\
2762 (!x. x IN s ==> (f has_derivative (f'(x))) (at x within s))
2763 ==> (f convex_on s <=>
2764 !x y. x IN s /\ y IN s ==> f'(x)(y - x) <= f y - f x)) /\
2765 (!f f' s:real->bool.
2766 convex s /\
2767 (!x. x IN s ==> (f has_derivative (f'(x))) (at x within s))
2768 ==> (f convex_on s <=>
2769 !x y. x IN s /\ y IN s ==> f'(x)(y - x) <= f'(y)(y - x)))
2770Proof
2771 SIMP_TAC bool_ss[AND_FORALL_THM] THEN REPEAT GEN_TAC THEN
2772 REWRITE_TAC[TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`] THEN
2773 STRIP_TAC THEN MATCH_MP_TAC(TAUT
2774 `(a ==> b) /\ (b ==> c) /\ (c ==> a) ==> (a <=> b) /\ (a <=> c)`) THEN
2775 REPEAT CONJ_TAC THENL
2776 [ (* goal 1 (of 3) *)
2777 REPEAT STRIP_TAC THEN MATCH_MP_TAC CONVEX_ON_DERIVATIVE_SECANT_IMP THEN
2778 EXISTS_TAC ``s:real->bool`` THEN ASM_SIMP_TAC std_ss[] THEN
2779 ASM_MESON_TAC[CONVEX_CONTAINS_SEGMENT],
2780 (* goal 2 (of 3) *)
2781 DISCH_TAC THEN MAP_EVERY Q.X_GEN_TAC [`x:real`, `y:real`] THEN
2782 STRIP_TAC THEN FIRST_X_ASSUM(fn th =>
2783 MP_TAC(Q.SPECL [`x:real`, `y:real`] th) THEN
2784 MP_TAC(Q.SPECL [`y:real`, `x:real`] th)) THEN
2785 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
2786 ``f''' = -f'' ==> f''' <= x - y ==> f' <= y - x ==> f' <= f''``) THEN
2787 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) empty_rewrites[GSYM REAL_NEG_SUB] THEN
2788 Q.SPEC_TAC(`y - x:real`,`z:real`) THEN
2789 MATCH_MP_TAC(REWRITE_RULE[RIGHT_FORALL_IMP_THM] LINEAR_NEG) THEN
2790 ASM_MESON_TAC[has_derivative],
2791 (* goal 3 (of 3) *)
2792 ALL_TAC] THEN
2793 DISCH_TAC THEN REWRITE_TAC[convex_on] THEN
2794 MAP_EVERY Q.X_GEN_TAC [`a:real`, `b:real`] THEN
2795 ASM_SIMP_TAC bool_ss[Once SWAP_FORALL_THM] THEN
2796 ONCE_REWRITE_TAC[TAUT `a /\ b /\ c /\ d /\ e <=> e /\ a /\ b /\ c /\ d`] THEN
2797 REWRITE_TAC[IMP_CONJ, REAL_ARITH ``u + v = &1 <=> u = &1 - v``] THEN
2798 SIMP_TAC bool_ss[FORALL_UNWIND_THM2, REAL_SUB_LE] THEN
2799 Q.X_GEN_TAC `u:real` THEN
2800 REPEAT STRIP_TAC THEN
2801 ASM_CASES_TAC ``u = &0`` THEN
2802 ASM_SIMP_TAC std_ss [REAL_SUB_RZERO, REAL_MUL_LZERO, REAL_MUL_LID,
2803 REAL_LE_REFL, REAL_ADD_RID] THEN
2804 ASM_CASES_TAC ``u = &1`` THEN
2805 ASM_SIMP_TAC std_ss [REAL_SUB_REFL, REAL_MUL_LZERO, REAL_MUL_LID,
2806 REAL_LE_REFL, REAL_ADD_LID] THEN
2807 SUBGOAL_THEN ``&0 < u /\ u < &1`` STRIP_ASSUME_TAC THENL
2808 [ASM_REWRITE_TAC[REAL_LT_LE] >> PROVE_TAC [], ALL_TAC] THEN
2809 MP_TAC(Q.SPECL
2810 [`(f:real->real) o (\u. (&1 - u) * a + u * b)`,
2811 `\x:real. f'((&1 - x) * a + x * b) o
2812 (\u. -u * a + u * b:real)`] MVT_VERY_SIMPLE) THEN
2813 DISCH_THEN(fn th =>
2814 MP_TAC(Q.SPECL [`0:real`, `u`] th) THEN
2815 MP_TAC(Q.SPECL [`u`, `1:real`] th)) THEN
2816 ASM_SIMP_TAC std_ss[o_THM] THEN
2817 ASM_SIMP_TAC std_ss[REAL_MUL_LZERO, REAL_SUB_RZERO, REAL_LT_IMP_LE,
2818 REAL_ADD_RID, REAL_MUL_LID, REAL_SUB_RZERO] THEN
2819 MATCH_MP_TAC(TAUT
2820 `(a1 /\ a2) /\ (b1 ==> b2 ==> c) ==> (a1 ==> b1) ==> (a2 ==> b2) ==> c`) THEN
2821 CONJ_TAC THENL
2822 [ (* goal 1 (of 2) *)
2823 CONJ_TAC THEN X_GEN_TAC ``v:real`` THEN DISCH_TAC THEN
2824 (* 2 subgoals, same tactics *)
2825 (REWRITE_TAC[o_ASSOC] THEN MATCH_MP_TAC DIFF_CHAIN_WITHIN THEN
2826 REWRITE_TAC[] THEN CONJ_TAC THENL
2827 [ (* goal 1.1 (of 2) *)
2828 HO_MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN CONJ_TAC THENL
2829 [ONCE_REWRITE_TAC[REAL_ARITH ``(&1 - a) * x:real = x + -a * x``,
2830 REAL_ARITH ``-u * a:real = 0 + -u * a``] THEN
2831 HO_MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN
2832 REWRITE_TAC[HAS_DERIVATIVE_CONST],
2833 ALL_TAC] THEN
2834 MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
2835 REWRITE_TAC[linear] THEN REAL_ARITH_TAC,
2836 (* goal 1.2 (of 2) *)
2837 MATCH_MP_TAC HAS_DERIVATIVE_WITHIN_SUBSET THEN
2838 BETA_TAC THEN
2839 EXISTS_TAC ``s:real->bool`` THEN CONJ_TAC THENL
2840 [FIRST_X_ASSUM MATCH_MP_TAC,
2841 SIMP_TAC std_ss[SUBSET_DEF, FORALL_IN_IMAGE] THEN
2842 Q.X_GEN_TAC ‘x’ THEN DISCH_TAC] THEN
2843 FIRST_ASSUM(MATCH_MP_TAC o
2844 GEN_REWRITE_RULE I empty_rewrites[CONVEX_ALT]) THEN
2845 FULL_SIMP_TAC std_ss [IN_INTERVAL] THEN
2846 ASM_REAL_ARITH_TAC ]),
2847 (* goal 2 (of 2) *)
2848 REWRITE_TAC[REAL_SUB_REFL, REAL_MUL_LZERO, REAL_ADD_LID] THEN
2849 SIMP_TAC std_ss [IN_INTERVAL] \\
2850 REWRITE_TAC[REAL_ARITH ``-u * a + u * b:real = u * (b - a)``] THEN
2851 SIMP_TAC std_ss[LEFT_IMP_EXISTS_THM, RIGHT_IMP_FORALL_THM] THEN
2852 MAP_EVERY X_GEN_TAC [``w:real``, ``v:real``] THEN
2853 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
2854 ONCE_REWRITE_TAC[TAUT `a ==> b /\ c ==> d <=> b ==> a ==> c ==> d`] THEN
2855 STRIP_TAC THEN REWRITE_TAC[IMP_IMP] THEN
2856 DISCH_THEN(CONJUNCTS_THEN2 (MP_TAC o AP_TERM ``$* (u:real)``)
2857 (MP_TAC o AP_TERM ``$* (&1 - u:real)``)) THEN
2858 MATCH_MP_TAC(REAL_ARITH
2859 ``f1 <= f2 /\ (xa <= xb ==> a <= b)
2860 ==> xa = f1 ==> xb = f2 ==> a <= b :real``) THEN
2861 CONJ_TAC THENL [ALL_TAC, REAL_ARITH_TAC] THEN
2862 SUBGOAL_THEN
2863 ``((&1 - v) * a + v * b:real) IN s /\
2864 ((&1 - w) * a + w * b:real) IN s``
2865 STRIP_ASSUME_TAC THENL
2866 [CONJ_TAC THEN
2867 FIRST_X_ASSUM
2868 (MATCH_MP_TAC o GEN_REWRITE_RULE I empty_rewrites[CONVEX_ALT]) THEN
2869 ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC,
2870 ALL_TAC] THEN
2871 SUBGOAL_THEN
2872 ``linear((f'((&1 - v) * a + v * b:real):real->real)) /\
2873 linear((f'((&1 - w) * a + w * b:real):real->real))``
2874 MP_TAC THENL [ASM_MESON_TAC[has_derivative], ALL_TAC] THEN
2875 DISCH_THEN(CONJUNCTS_THEN(MP_TAC o MATCH_MP LINEAR_CMUL)) THEN
2876 REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
2877 ONCE_REWRITE_TAC[REAL_ARITH ``(&1 - u) * (u * x) = u * ((&1 - u) * x)``] THEN
2878 REPEAT(MATCH_MP_TAC REAL_LE_LMUL_IMP THEN
2879 CONJ_TAC THENL [ASM_REAL_ARITH_TAC, ALL_TAC]) THEN
2880 LAST_X_ASSUM(MP_TAC o SPECL
2881 [``(&1 - v) * a + v * b:real``, ``(&1 - w) * a + w * b:real``]) THEN
2882 ASM_REWRITE_TAC[REAL_ARITH
2883 ``((&1 - v) * a + v * b) - ((&1 - w) * a + w * b):real =
2884 (v - w) * (b - a)``] THEN
2885 ASM_CASES_TAC ``v:real = w`` THEN ASM_SIMP_TAC std_ss[REAL_LE_REFL] THEN
2886 SUBGOAL_THEN ``&0 < w - v`` (fn th => SIMP_TAC std_ss[th, REAL_LE_LMUL]) THEN
2887 ASM_REAL_ARITH_TAC]
2888QED
2889
2890(* |- !f f' s.
2891 convex s /\ (!x. x IN s ==> (f has_derivative f' x) (at x within s)) ==>
2892 (f convex_on s <=>
2893 !x y. x IN s /\ y IN s ==> f' x (y - x) <= f y - f x)
2894 *)
2895Theorem CONVEX_ON_DERIVATIVE_SECANT =
2896 CONVEX_ON_DERIVATIVE_SECANT_combined |> cj 1
2897
2898(* |- !f f' s.
2899 convex s /\ (!x. x IN s ==> (f has_derivative f' x) (at x within s)) ==>
2900 (f convex_on s <=>
2901 !x y. x IN s /\ y IN s ==> f' x (y - x) <= f' y (y - x))
2902 *)
2903Theorem CONVEX_ON_DERIVATIVES =
2904 CONVEX_ON_DERIVATIVE_SECANT_combined |> cj 2
2905
2906Theorem CONVEX_ON_SECANT_DERIVATIVE :
2907 !f f' s:real->bool.
2908 convex s /\
2909 (!x. x IN s ==> (f has_derivative (f'(x))) (at x within s))
2910 ==> (f convex_on s <=>
2911 !x y. x IN s /\ y IN s ==> f y - f x <= f'(y)(y - x))
2912Proof
2913 REPEAT GEN_TAC THEN DISCH_TAC THEN
2914 FIRST_ASSUM(SUBST1_TAC o MATCH_MP CONVEX_ON_DERIVATIVE_SECANT) THEN
2915 Ho_Rewrite.GEN_REWRITE_TAC RAND_CONV [SWAP_FORALL_THM] THEN
2916 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites[FUN_EQ_THM] THEN
2917 Q.X_GEN_TAC `x:real` THEN BETA_TAC THEN
2918 AP_TERM_TAC THEN GEN_REWRITE_TAC I empty_rewrites[FUN_EQ_THM] THEN
2919 Q.X_GEN_TAC `y:real` THEN BETA_TAC THEN
2920 MAP_EVERY ASM_CASES_TAC [``(x:real) IN s``, ``(y:real) IN s``] THEN
2921 ASM_REWRITE_TAC[] THEN
2922 MATCH_MP_TAC(REAL_ARITH
2923 ``f' = -f'' ==> (f' <= y - x <=> x - y <= f'' :real)``) THEN
2924 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) empty_rewrites[GSYM REAL_NEG_SUB] THEN
2925 Q.SPEC_TAC(`x - y:real`,`z:real`) THEN
2926 MATCH_MP_TAC(REWRITE_RULE[RIGHT_FORALL_IMP_THM] LINEAR_NEG) THEN
2927 ASM_MESON_TAC[has_derivative]
2928QED
2929
2930(* ------------------------------------------------------------------------- *)
2931(* Concave functions *)
2932(* ------------------------------------------------------------------------- *)
2933
2934val _ = set_fixity "concave_on" (Infix(NONASSOC, 450));
2935
2936Definition concave_on_def :
2937 f concave_on s <=> (\x. -f x) convex_on s
2938End
2939
2940Theorem concave_on :
2941 !f s. f concave_on s <=>
2942 !x y u v:real. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ (u + v = &1)
2943 ==> u * f(x) + v * f(y) <= f(u * x + v * y)
2944Proof
2945 rw [concave_on_def, convex_on, REAL_MUL_RNEG, GSYM REAL_NEG_ADD, REAL_LE_NEG]
2946QED
2947
2948Theorem CONCAVE_ON_SECANT_DERIVATIVE :
2949 !f f' s.
2950 convex s /\
2951 (!x. x IN s ==> (f has_derivative (f'(x))) (at x within s))
2952 ==> (f concave_on s <=>
2953 !x y. x IN s /\ y IN s ==> f'(y)(y - x) <= f y - f x)
2954Proof
2955 RW_TAC std_ss [concave_on_def]
2956 >> qabbrev_tac ‘g = \x. -f x’
2957 >> qabbrev_tac ‘g' = \h x. -f' h x’
2958 >> ‘!x y. f' y (y - x) = -g' y (y - x)’
2959 by rw [REAL_NEG_NEG, Abbr ‘g'’] >> POP_ORW
2960 >> ‘!x y. f y - f x = -(g y - g x)’
2961 by rw [Abbr ‘g’, REAL_SUB_NEG2, REAL_NEG_SUB] >> POP_ORW
2962 >> simp [REAL_LE_NEG]
2963 >> MATCH_MP_TAC CONVEX_ON_SECANT_DERIVATIVE
2964 >> rw [Abbr ‘g’, Abbr ‘g'’]
2965 >> HO_MATCH_MP_TAC HAS_DERIVATIVE_NEG
2966 >> simp [SF ETA_ss]
2967QED
2968
2969Theorem CONCAVE_ON_DERIVATIVE_SECANT :
2970 !f f' s.
2971 convex s /\
2972 (!x. x IN s ==> (f has_derivative f' x) (at x within s)) ==>
2973 (f concave_on s <=>
2974 !x y. x IN s /\ y IN s ==> f y - f x <= f' x (y - x))
2975Proof
2976 RW_TAC std_ss [concave_on_def]
2977 >> qabbrev_tac ‘g = \x. -f x’
2978 >> qabbrev_tac ‘g' = \h x. -f' h x’
2979 >> ‘!x y. f' x (y - x) = -g' x (y - x)’
2980 by rw [REAL_NEG_NEG, Abbr ‘g'’] >> POP_ORW
2981 >> ‘!x y. f y - f x = -(g y - g x)’
2982 by rw [Abbr ‘g’, REAL_SUB_NEG2, REAL_NEG_SUB] >> POP_ORW
2983 >> simp [REAL_LE_NEG]
2984 >> MATCH_MP_TAC CONVEX_ON_DERIVATIVE_SECANT
2985 >> rw [Abbr ‘g’, Abbr ‘g'’]
2986 >> HO_MATCH_MP_TAC HAS_DERIVATIVE_NEG
2987 >> simp [SF ETA_ss]
2988QED
2989
2990Theorem CONCAVE_ON_LEFT_SECANT :
2991 !f s.
2992 f concave_on s <=>
2993 !a b x.
2994 a IN s /\ b IN s /\ x IN segment (a,b) ==>
2995 (f b - f a) / abs (b - a) <= (f x - f a) / abs (x - a)
2996Proof
2997 RW_TAC std_ss [concave_on_def]
2998 >> qabbrev_tac ‘g = \x. -f x’
2999 >> ‘!a b. f b - f a = -(g b - g a)’
3000 by rw [Abbr ‘g’, REAL_SUB_NEG2, REAL_NEG_SUB] >> POP_ORW
3001 >> REWRITE_TAC [REAL_DIV_LNEG, REAL_LE_NEG]
3002 >> REWRITE_TAC [CONVEX_ON_LEFT_SECANT]
3003QED
3004
3005Theorem CONCAVE_ON_RIGHT_SECANT :
3006 !f s.
3007 f concave_on s <=>
3008 !a b x.
3009 a IN s /\ b IN s /\ x IN segment (a,b) ==>
3010 (f b - f x) / abs (b - x) <= (f b - f a) / abs (b - a)
3011Proof
3012 RW_TAC std_ss [concave_on_def]
3013 >> qabbrev_tac ‘g = \x. -f x’
3014 >> ‘!a b. f b - f a = -(g b - g a)’
3015 by rw [Abbr ‘g’, REAL_SUB_NEG2, REAL_NEG_SUB] >> POP_ORW
3016 >> REWRITE_TAC [REAL_DIV_LNEG, REAL_LE_NEG]
3017 >> REWRITE_TAC [CONVEX_ON_RIGHT_SECANT]
3018QED
3019
3020Theorem CONCAVE_ON_MID_SECANT :
3021 !f s.
3022 f concave_on s <=>
3023 !a b x.
3024 a IN s /\ b IN s /\ x IN segment (a,b) ==>
3025 (f b - f x) / abs (b - x) <= (f x - f a) / abs (x - a)
3026Proof
3027 RW_TAC std_ss [concave_on_def]
3028 >> qabbrev_tac ‘g = \x. -f x’
3029 >> ‘!a b. f b - f a = -(g b - g a)’
3030 by rw [Abbr ‘g’, REAL_SUB_NEG2, REAL_NEG_SUB] >> POP_ORW
3031 >> REWRITE_TAC [REAL_DIV_LNEG, REAL_LE_NEG]
3032 >> REWRITE_TAC [CONVEX_ON_MID_SECANT]
3033QED
3034
3035(* END *)