1 (* ========================================================================= *)
2 (* Multivariate calculus in Euclidean space. *)
4 (* (c) Copyright, John Harrison 1998-2008 *)
5 (* ========================================================================= *)
7 needs "Multivariate/dimension.ml";;
9 (* ------------------------------------------------------------------------- *)
10 (* Derivatives. The definition is slightly tricky since we make it work over *)
11 (* nets of a particular form. This lets us prove theorems generally and use *)
12 (* "at a" or "at a within s" for restriction to a set (1-sided on R etc.) *)
13 (* ------------------------------------------------------------------------- *)
15 parse_as_infix ("has_derivative",(12,"right"));;
17 let has_derivative = new_definition
18 `(f has_derivative f') net <=>
20 ((\y. inv(norm(y - netlimit net)) %
22 (f(netlimit net) + f'(y - netlimit net)))) --> vec 0) net`;;
24 (* ------------------------------------------------------------------------- *)
25 (* These are the only cases we'll care about, probably. *)
26 (* ------------------------------------------------------------------------- *)
28 let has_derivative_within = prove
29 (`!f:real^M->real^N f' x s.
30 (f has_derivative f') (at x within s) <=>
32 ((\y. inv(norm(y - x)) % (f(y) - (f(x) + f'(y - x)))) --> vec 0)
34 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative] THEN AP_TERM_TAC THEN
35 ASM_CASES_TAC `trivial_limit(at (x:real^M) within s)` THENL
36 [ASM_REWRITE_TAC[LIM]; ASM_SIMP_TAC[NETLIMIT_WITHIN]]);;
38 let has_derivative_at = prove
39 (`!f:real^M->real^N f' x.
40 (f has_derivative f') (at x) <=>
42 ((\y. inv(norm(y - x)) % (f(y) - (f(x) + f'(y - x)))) --> vec 0)
44 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
45 REWRITE_TAC[has_derivative_within]);;
47 (* ------------------------------------------------------------------------- *)
48 (* More explicit epsilon-delta forms. *)
49 (* ------------------------------------------------------------------------- *)
51 let HAS_DERIVATIVE_WITHIN = prove
52 (`(f has_derivative f')(at x within s) <=>
57 &0 < norm(x' - x) /\ norm(x' - x) < d
58 ==> norm(f(x') - f(x) - f'(x' - x)) /
60 SIMP_TAC[has_derivative_within; LIM_WITHIN] THEN AP_TERM_TAC THEN
61 REWRITE_TAC[dist; VECTOR_ARITH `(x' - (x + d)) = x' - x - d:real^N`] THEN
62 REWRITE_TAC[real_div; VECTOR_SUB_RZERO; NORM_MUL] THEN
63 REWRITE_TAC[REAL_MUL_AC; REAL_ABS_INV; REAL_ABS_NORM]);;
65 let HAS_DERIVATIVE_AT = prove
66 (`(f has_derivative f')(at x) <=>
70 !x'. &0 < norm(x' - x) /\ norm(x' - x) < d
71 ==> norm(f(x') - f(x) - f'(x' - x)) /
73 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
74 REWRITE_TAC[HAS_DERIVATIVE_WITHIN; IN_UNIV]);;
76 let HAS_DERIVATIVE_AT_WITHIN = prove
77 (`!f x s. (f has_derivative f') (at x)
78 ==> (f has_derivative f') (at x within s)`,
79 REWRITE_TAC[HAS_DERIVATIVE_WITHIN; HAS_DERIVATIVE_AT] THEN MESON_TAC[]);;
81 let HAS_DERIVATIVE_WITHIN_OPEN = prove
84 ==> ((f has_derivative f') (at a within s) <=>
85 (f has_derivative f') (at a))`,
86 SIMP_TAC[has_derivative_within; has_derivative_at; LIM_WITHIN_OPEN]);;
88 (* ------------------------------------------------------------------------- *)
89 (* Combining theorems. *)
90 (* ------------------------------------------------------------------------- *)
92 let HAS_DERIVATIVE_LINEAR = prove
93 (`!f net. linear f ==> (f has_derivative f) net`,
94 REWRITE_TAC[has_derivative; linear] THEN
95 SIMP_TAC[VECTOR_ARITH `x - y = x + --(&1) % y`] THEN
96 REWRITE_TAC[VECTOR_ARITH `x + --(&1) % (y + x + --(&1) % y) = vec 0`] THEN
97 REWRITE_TAC[VECTOR_MUL_RZERO; LIM_CONST]);;
99 let HAS_DERIVATIVE_ID = prove
100 (`!net. ((\x. x) has_derivative (\h. h)) net`,
101 SIMP_TAC[HAS_DERIVATIVE_LINEAR; LINEAR_ID]);;
103 let HAS_DERIVATIVE_CONST = prove
104 (`!c net. ((\x. c) has_derivative (\h. vec 0)) net`,
105 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative; linear] THEN
106 REWRITE_TAC[VECTOR_ADD_RID; VECTOR_SUB_REFL; VECTOR_MUL_RZERO; LIM_CONST]);;
108 let HAS_DERIVATIVE_LIFT_COMPONENT = prove
109 (`!net:(real^N)net. ((\x. lift(x$i)) has_derivative (\x. lift(x$i))) net`,
110 GEN_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
111 REWRITE_TAC[linear; VECTOR_MUL_COMPONENT; VECTOR_ADD_COMPONENT] THEN
112 REWRITE_TAC[LIFT_ADD; LIFT_CMUL]);;
114 let HAS_DERIVATIVE_CMUL = prove
115 (`!f f' net c. (f has_derivative f') net
116 ==> ((\x. c % f(x)) has_derivative (\h. c % f'(h))) net`,
117 REPEAT GEN_TAC THEN SIMP_TAC[has_derivative; LINEAR_COMPOSE_CMUL] THEN
118 DISCH_THEN(MP_TAC o SPEC `c:real` o MATCH_MP LIM_CMUL o CONJUNCT2) THEN
119 REWRITE_TAC[VECTOR_MUL_RZERO] THEN
120 MATCH_MP_TAC EQ_IMP THEN
121 AP_THM_TAC THEN AP_THM_TAC THEN
122 AP_TERM_TAC THEN ABS_TAC THEN VECTOR_ARITH_TAC);;
124 let HAS_DERIVATIVE_CMUL_EQ = prove
127 ==> (((\x. c % f(x)) has_derivative (\h. c % f'(h))) net <=>
128 (f has_derivative f') net)`,
129 REPEAT STRIP_TAC THEN EQ_TAC THEN
130 DISCH_THEN(MP_TAC o MATCH_MP HAS_DERIVATIVE_CMUL) THENL
131 [DISCH_THEN(MP_TAC o SPEC `inv(c):real`);
132 DISCH_THEN(MP_TAC o SPEC `c:real`)] THEN
133 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID; ETA_AX]);;
135 let HAS_DERIVATIVE_NEG = prove
136 (`!f f' net. (f has_derivative f') net
137 ==> ((\x. --(f(x))) has_derivative (\h. --(f'(h)))) net`,
138 ONCE_REWRITE_TAC[VECTOR_NEG_MINUS1] THEN
139 SIMP_TAC[HAS_DERIVATIVE_CMUL]);;
141 let HAS_DERIVATIVE_NEG_EQ = prove
142 (`!f f' net. ((\x. --(f(x))) has_derivative (\h. --(f'(h)))) net <=>
143 (f has_derivative f') net`,
144 REPEAT GEN_TAC THEN EQ_TAC THEN
145 DISCH_THEN(MP_TAC o MATCH_MP HAS_DERIVATIVE_NEG) THEN
146 REWRITE_TAC[VECTOR_NEG_NEG; ETA_AX]);;
148 let HAS_DERIVATIVE_ADD = prove
150 (f has_derivative f') net /\ (g has_derivative g') net
151 ==> ((\x. f(x) + g(x)) has_derivative (\h. f'(h) + g'(h))) net`,
152 REPEAT GEN_TAC THEN SIMP_TAC[has_derivative; LINEAR_COMPOSE_ADD] THEN
153 DISCH_THEN(MP_TAC o MATCH_MP (TAUT `(a /\ b) /\ (c /\ d) ==> b /\ d`)) THEN
154 DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN REWRITE_TAC[VECTOR_ADD_LID] THEN
155 MATCH_MP_TAC EQ_IMP THEN
156 AP_THM_TAC THEN AP_THM_TAC THEN
157 AP_TERM_TAC THEN ABS_TAC THEN VECTOR_ARITH_TAC);;
159 let HAS_DERIVATIVE_SUB = prove
161 (f has_derivative f') net /\ (g has_derivative g') net
162 ==> ((\x. f(x) - g(x)) has_derivative (\h. f'(h) - g'(h))) net`,
163 SIMP_TAC[VECTOR_SUB; HAS_DERIVATIVE_ADD; HAS_DERIVATIVE_NEG]);;
165 let HAS_DERIVATIVE_VSUM = prove
168 (!a. a IN s ==> ((f a) has_derivative (f' a)) net)
169 ==> ((\x. vsum s (\a. f a x)) has_derivative (\h. vsum s (\a. f' a h)))
171 GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
172 MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
173 SIMP_TAC[VSUM_CLAUSES; HAS_DERIVATIVE_CONST] THEN
174 REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN
175 REWRITE_TAC[ETA_AX] THEN ASM_SIMP_TAC[IN_INSERT]);;
177 let HAS_DERIVATIVE_VSUM_NUMSEG = prove
179 (!i. m <= i /\ i <= n ==> ((f i) has_derivative (f' i)) net)
180 ==> ((\x. vsum (m..n) (\i. f i x)) has_derivative
181 (\h. vsum (m..n) (\i. f' i h))) net`,
182 REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_VSUM THEN
183 ASM_REWRITE_TAC[IN_NUMSEG; FINITE_NUMSEG]);;
185 let HAS_DERIVATIVE_COMPONENTWISE_WITHIN = prove
186 (`!f:real^M->real^N f' a s.
187 (f has_derivative f') (at a within s) <=>
188 !i. 1 <= i /\ i <= dimindex(:N)
189 ==> ((\x. lift(f(x)$i)) has_derivative (\x. lift(f'(x)$i)))
191 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[has_derivative_within] THEN
192 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
193 [LINEAR_COMPONENTWISE; LIM_COMPONENTWISE_LIFT] THEN
194 SIMP_TAC[AND_FORALL_THM; TAUT `(p ==> q) /\ (p ==> r) <=> p ==> q /\ r`] THEN
195 REWRITE_TAC[GSYM LIFT_ADD; GSYM LIFT_CMUL; GSYM LIFT_SUB] THEN
196 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT; VEC_COMPONENT;
197 VECTOR_SUB_COMPONENT; LIFT_NUM]);;
199 let HAS_DERIVATIVE_COMPONENTWISE_AT = prove
200 (`!f:real^M->real^N f' a.
201 (f has_derivative f') (at a) <=>
202 !i. 1 <= i /\ i <= dimindex(:N)
203 ==> ((\x. lift(f(x)$i)) has_derivative (\x. lift(f'(x)$i))) (at a)`,
204 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
205 MATCH_ACCEPT_TAC HAS_DERIVATIVE_COMPONENTWISE_WITHIN);;
207 (* ------------------------------------------------------------------------- *)
208 (* Somewhat different results for derivative of scalar multiplier. *)
209 (* ------------------------------------------------------------------------- *)
211 let HAS_DERIVATIVE_VMUL_COMPONENT = prove
212 (`!c:real^M->real^N c' k v:real^P.
213 1 <= k /\ k <= dimindex(:N) /\ (c has_derivative c') net
214 ==> ((\x. c(x)$k % v) has_derivative (\x. c'(x)$k % v)) net`,
215 SIMP_TAC[has_derivative; LINEAR_VMUL_COMPONENT] THEN
216 REPEAT STRIP_TAC THEN
217 REWRITE_TAC[GSYM VECTOR_ADD_RDISTRIB; GSYM VECTOR_SUB_RDISTRIB] THEN
218 SUBST1_TAC(VECTOR_ARITH `vec 0 = &0 % (v:real^P)`) THEN
219 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN MATCH_MP_TAC LIM_VMUL THEN
220 ASM_SIMP_TAC[GSYM VECTOR_SUB_COMPONENT; GSYM VECTOR_ADD_COMPONENT] THEN
221 ASM_SIMP_TAC[GSYM VECTOR_MUL_COMPONENT] THEN
222 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM]) THEN REWRITE_TAC[LIM] THEN
223 REWRITE_TAC[dist; LIFT_NUM; VECTOR_SUB_RZERO; o_THM; NORM_LIFT] THEN
224 ASM_SIMP_TAC[VECTOR_MUL_COMPONENT; REAL_ABS_MUL; NORM_MUL] THEN
225 ASM_MESON_TAC[REAL_LET_TRANS; COMPONENT_LE_NORM;
226 REAL_LE_LMUL; REAL_ABS_POS]);;
228 let HAS_DERIVATIVE_VMUL_DROP = prove
229 (`!c c' v. (c has_derivative c') net
230 ==> ((\x. drop(c(x)) % v) has_derivative (\x. drop(c'(x)) % v)) net`,
231 SIMP_TAC[drop; LE_REFL; DIMINDEX_1; HAS_DERIVATIVE_VMUL_COMPONENT]);;
233 let HAS_DERIVATIVE_LIFT_DOT = prove
234 (`!f:real^M->real^N f'.
235 (f has_derivative f') net
236 ==> ((\x. lift(v dot f(x))) has_derivative (\t. lift(v dot (f' t)))) net`,
237 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative] THEN
238 REWRITE_TAC[GSYM LIFT_SUB; GSYM LIFT_ADD; GSYM LIFT_CMUL] THEN
239 REWRITE_TAC[GSYM DOT_RADD; GSYM DOT_RSUB; GSYM DOT_RMUL] THEN
241 `(\t. lift (v dot (f':real^M->real^N) t)) = (\y. lift(v dot y)) o f'`
242 SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
243 SIMP_TAC[LINEAR_COMPOSE; LINEAR_LIFT_DOT] THEN
244 DISCH_THEN(MP_TAC o MATCH_MP LIM_LIFT_DOT o CONJUNCT2) THEN
245 SIMP_TAC[o_DEF; DOT_RZERO; LIFT_NUM]);;
247 (* ------------------------------------------------------------------------- *)
248 (* Limit transformation for derivatives. *)
249 (* ------------------------------------------------------------------------- *)
251 let HAS_DERIVATIVE_TRANSFORM_WITHIN = prove
254 (!x'. x' IN s /\ dist (x',x) < d ==> f x' = g x') /\
255 (f has_derivative f') (at x within s)
256 ==> (g has_derivative f') (at x within s)`,
257 REPEAT GEN_TAC THEN SIMP_TAC[has_derivative_within; IMP_CONJ] THEN
258 REPLICATE_TAC 4 DISCH_TAC THEN
259 MATCH_MP_TAC(REWRITE_RULE[TAUT `a /\ b /\ c ==> d <=> a /\ b ==> c ==> d`]
260 LIM_TRANSFORM_WITHIN) THEN
261 EXISTS_TAC `d:real` THEN ASM_SIMP_TAC[DIST_REFL]);;
263 let HAS_DERIVATIVE_TRANSFORM_AT = prove
265 &0 < d /\ (!x'. dist (x',x) < d ==> f x' = g x') /\
266 (f has_derivative f') (at x)
267 ==> (g has_derivative f') (at x)`,
268 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
269 MESON_TAC[HAS_DERIVATIVE_TRANSFORM_WITHIN; IN_UNIV]);;
271 let HAS_DERIVATIVE_TRANSFORM_WITHIN_OPEN = prove
272 (`!f g:real^M->real^N s x.
274 (!y. y IN s ==> f y = g y) /\
275 (f has_derivative f') (at x)
276 ==> (g has_derivative f') (at x)`,
277 REPEAT GEN_TAC THEN SIMP_TAC[has_derivative_at; IMP_CONJ] THEN
278 REPLICATE_TAC 4 DISCH_TAC THEN
279 MATCH_MP_TAC(REWRITE_RULE
280 [TAUT `a /\ b /\ c /\ d ==> e <=> a /\ b /\ c ==> d ==> e`]
281 LIM_TRANSFORM_WITHIN_OPEN) THEN
282 EXISTS_TAC `s:real^M->bool` THEN ASM_SIMP_TAC[]);;
284 (* ------------------------------------------------------------------------- *)
285 (* Differentiability. *)
286 (* ------------------------------------------------------------------------- *)
288 parse_as_infix ("differentiable",(12,"right"));;
289 parse_as_infix ("differentiable_on",(12,"right"));;
291 let differentiable = new_definition
292 `f differentiable net <=> ?f'. (f has_derivative f') net`;;
294 let differentiable_on = new_definition
295 `f differentiable_on s <=> !x. x IN s ==> f differentiable (at x within s)`;;
297 let HAS_DERIVATIVE_IMP_DIFFERENTIABLE = prove
298 (`!f f' net. (f has_derivative f') net ==> f differentiable net`,
299 REWRITE_TAC[differentiable] THEN MESON_TAC[]);;
301 let DIFFERENTIABLE_AT_WITHIN = prove
302 (`!f s x. f differentiable (at x)
303 ==> f differentiable (at x within s)`,
304 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_AT_WITHIN]);;
306 let DIFFERENTIABLE_WITHIN_OPEN = prove
309 ==> (f differentiable (at a within s) <=> (f differentiable (at a)))`,
310 SIMP_TAC[differentiable; HAS_DERIVATIVE_WITHIN_OPEN]);;
312 let DIFFERENTIABLE_AT_IMP_DIFFERENTIABLE_ON = prove
313 (`!f s. (!x. x IN s ==> f differentiable at x) ==> f differentiable_on s`,
314 REWRITE_TAC[differentiable_on] THEN MESON_TAC[DIFFERENTIABLE_AT_WITHIN]);;
316 let DIFFERENTIABLE_ON_EQ_DIFFERENTIABLE_AT = prove
317 (`!f s. open s ==> (f differentiable_on s <=>
318 !x. x IN s ==> f differentiable at x)`,
319 SIMP_TAC[differentiable_on; DIFFERENTIABLE_WITHIN_OPEN]);;
321 let DIFFERENTIABLE_TRANSFORM_WITHIN = prove
324 (!x'. x' IN s /\ dist (x',x) < d ==> f x' = g x') /\
325 f differentiable (at x within s)
326 ==> g differentiable (at x within s)`,
327 REWRITE_TAC[differentiable] THEN
328 MESON_TAC[HAS_DERIVATIVE_TRANSFORM_WITHIN]);;
330 let DIFFERENTIABLE_TRANSFORM_AT = prove
333 (!x'. dist (x',x) < d ==> f x' = g x') /\
334 f differentiable at x
335 ==> g differentiable at x`,
336 REWRITE_TAC[differentiable] THEN
337 MESON_TAC[HAS_DERIVATIVE_TRANSFORM_AT]);;
339 (* ------------------------------------------------------------------------- *)
340 (* Frechet derivative and Jacobian matrix. *)
341 (* ------------------------------------------------------------------------- *)
343 let frechet_derivative = new_definition
344 `frechet_derivative f net = @f'. (f has_derivative f') net`;;
346 let FRECHET_DERIVATIVE_WORKS = prove
347 (`!f net. f differentiable net <=>
348 (f has_derivative (frechet_derivative f net)) net`,
349 REPEAT GEN_TAC THEN REWRITE_TAC[frechet_derivative] THEN
350 CONV_TAC(RAND_CONV SELECT_CONV) THEN REWRITE_TAC[differentiable]);;
352 let LINEAR_FRECHET_DERIVATIVE = prove
353 (`!f net. f differentiable net ==> linear(frechet_derivative f net)`,
354 SIMP_TAC[FRECHET_DERIVATIVE_WORKS; has_derivative]);;
356 let jacobian = new_definition
357 `jacobian f net = matrix(frechet_derivative f net)`;;
359 let JACOBIAN_WORKS = prove
360 (`!f net. f differentiable net <=>
361 (f has_derivative (\h. jacobian f net ** h)) net`,
362 REPEAT GEN_TAC THEN EQ_TAC THENL [ALL_TAC; MESON_TAC[differentiable]] THEN
363 REWRITE_TAC[FRECHET_DERIVATIVE_WORKS] THEN
364 SIMP_TAC[jacobian; MATRIX_WORKS; has_derivative] THEN SIMP_TAC[ETA_AX]);;
366 (* ------------------------------------------------------------------------- *)
367 (* Differentiability implies continuity. *)
368 (* ------------------------------------------------------------------------- *)
370 let LIM_MUL_NORM_WITHIN = prove
371 (`!f a s. (f --> vec 0) (at a within s)
372 ==> ((\x. norm(x - a) % f(x)) --> vec 0) (at a within s)`,
373 REPEAT GEN_TAC THEN REWRITE_TAC[LIM_WITHIN] THEN
374 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `e:real` THEN
375 ASM_CASES_TAC `&0 < e` THEN ASM_REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN
376 DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
377 EXISTS_TAC `min d (&1)` THEN ASM_REWRITE_TAC[REAL_LT_MIN; REAL_LT_01] THEN
378 REPEAT STRIP_TAC THEN REWRITE_TAC[NORM_MUL; REAL_ABS_NORM] THEN
379 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
380 ASM_SIMP_TAC[REAL_LT_MUL2; NORM_POS_LE]);;
382 let DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN = prove
383 (`!f:real^M->real^N s.
384 f differentiable (at x within s) ==> f continuous (at x within s)`,
385 REWRITE_TAC[differentiable; has_derivative_within; CONTINUOUS_WITHIN] THEN
387 DISCH_THEN(X_CHOOSE_THEN `f':real^M->real^N` MP_TAC) THEN
388 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP LIM_MUL_NORM_WITHIN) THEN
390 `((f':real^M->real^N) o (\y. y - x)) continuous (at x within s)`
392 [MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN
393 ASM_SIMP_TAC[LINEAR_CONTINUOUS_WITHIN] THEN
394 SIMP_TAC[CONTINUOUS_SUB; CONTINUOUS_CONST; CONTINUOUS_WITHIN_ID];
396 REWRITE_TAC[CONTINUOUS_WITHIN; o_DEF] THEN
397 ASM_REWRITE_TAC[VECTOR_MUL_ASSOC; IMP_IMP; IN_UNIV] THEN
398 DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN
399 SIMP_TAC[LIM_WITHIN; GSYM DIST_NZ; REAL_MUL_RINV; NORM_EQ_0;
400 VECTOR_ARITH `(x - y = vec 0) <=> (x = y)`;
401 VECTOR_MUL_LID; VECTOR_SUB_REFL] THEN
402 FIRST_ASSUM(SUBST1_TAC o MATCH_MP LINEAR_0) THEN
403 REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN
404 REWRITE_TAC[VECTOR_ARITH `(a + b - (c + a)) - (vec 0 + vec 0) = b - c`]);;
406 let DIFFERENTIABLE_IMP_CONTINUOUS_AT = prove
407 (`!f:real^M->real^N x. f differentiable (at x) ==> f continuous (at x)`,
408 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
409 REWRITE_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]);;
411 let DIFFERENTIABLE_IMP_CONTINUOUS_ON = prove
412 (`!f:real^M->real^N s. f differentiable_on s ==> f continuous_on s`,
413 SIMP_TAC[differentiable_on; CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN;
414 DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]);;
416 let HAS_DERIVATIVE_WITHIN_SUBSET = prove
417 (`!f s t x. (f has_derivative f') (at x within s) /\ t SUBSET s
418 ==> (f has_derivative f') (at x within t)`,
419 REWRITE_TAC[has_derivative_within] THEN MESON_TAC[LIM_WITHIN_SUBSET]);;
421 let DIFFERENTIABLE_WITHIN_SUBSET = prove
422 (`!f:real^M->real^N s t.
423 f differentiable (at x within t) /\ s SUBSET t
424 ==> f differentiable (at x within s)`,
425 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_WITHIN_SUBSET]);;
427 let DIFFERENTIABLE_ON_SUBSET = prove
428 (`!f:real^M->real^N s t.
429 f differentiable_on t /\ s SUBSET t ==> f differentiable_on s`,
430 REWRITE_TAC[differentiable_on] THEN
431 MESON_TAC[SUBSET; DIFFERENTIABLE_WITHIN_SUBSET]);;
433 let DIFFERENTIABLE_ON_EMPTY = prove
434 (`!f. f differentiable_on {}`,
435 REWRITE_TAC[differentiable_on; NOT_IN_EMPTY]);;
437 (* ------------------------------------------------------------------------- *)
438 (* Several results are easier using a "multiplied-out" variant. *)
439 (* (I got this idea from Dieudonne's proof of the chain rule). *)
440 (* ------------------------------------------------------------------------- *)
442 let HAS_DERIVATIVE_WITHIN_ALT = prove
443 (`!f:real^M->real^N f' s x.
444 (f has_derivative f') (at x within s) <=>
448 !y. y IN s /\ norm(y - x) < d
449 ==> norm(f(y) - f(x) - f'(y - x)) <=
451 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative_within; LIM_WITHIN] THEN
452 ASM_REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN
453 ASM_CASES_TAC `linear(f':real^M->real^N)` THEN
454 ASM_REWRITE_TAC[NORM_MUL; REAL_ABS_INV; REAL_ABS_NORM] THEN
455 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN
456 SIMP_TAC[GSYM real_div; REAL_LT_LDIV_EQ] THEN
457 REWRITE_TAC[VECTOR_ARITH `a - (b + c) = a - b - c :real^M`] THEN
458 EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THENL
459 [FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
460 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real` THEN STRIP_TAC THEN
461 ASM_REWRITE_TAC[] THEN X_GEN_TAC `y:real^M` THEN DISCH_TAC THEN
462 ASM_CASES_TAC `&0 < norm(y - x :real^M)` THENL
463 [ASM_SIMP_TAC[REAL_LT_IMP_LE]; ALL_TAC] THEN
464 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [NORM_POS_LT]) THEN
465 ASM_SIMP_TAC[VECTOR_SUB_EQ; VECTOR_SUB_REFL; NORM_0; REAL_MUL_RZERO;
466 VECTOR_ARITH `vec 0 - x = --x`; NORM_NEG] THEN
467 ASM_MESON_TAC[LINEAR_0; NORM_0; REAL_LE_REFL];
468 FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
469 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
470 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real` THEN STRIP_TAC THEN
471 ASM_REWRITE_TAC[] THEN X_GEN_TAC `y:real^M` THEN STRIP_TAC THEN
472 MATCH_MP_TAC REAL_LET_TRANS THEN
473 EXISTS_TAC `e / &2 * norm(y - x :real^M)` THEN
474 ASM_SIMP_TAC[REAL_LT_RMUL_EQ; REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN
475 UNDISCH_TAC `&0 < e` THEN REAL_ARITH_TAC]);;
477 let HAS_DERIVATIVE_AT_ALT = prove
478 (`!f:real^M->real^N f' x.
479 (f has_derivative f') (at x) <=>
484 ==> norm(f(y) - f(x) - f'(y - x)) <= e * norm(y - x)`,
485 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
486 REWRITE_TAC[HAS_DERIVATIVE_WITHIN_ALT; IN_UNIV]);;
488 (* ------------------------------------------------------------------------- *)
489 (* The chain rule. *)
490 (* ------------------------------------------------------------------------- *)
492 let DIFF_CHAIN_WITHIN = prove
493 (`!f:real^M->real^N g:real^N->real^P f' g' x s.
494 (f has_derivative f') (at x within s) /\
495 (g has_derivative g') (at (f x) within (IMAGE f s))
496 ==> ((g o f) has_derivative (g' o f'))(at x within s)`,
497 REPEAT GEN_TAC THEN SIMP_TAC[HAS_DERIVATIVE_WITHIN_ALT; LINEAR_COMPOSE] THEN
498 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
499 FIRST_ASSUM(X_CHOOSE_TAC `B1:real` o MATCH_MP LINEAR_BOUNDED_POS) THEN
500 DISCH_THEN(fun th -> X_GEN_TAC `e:real` THEN DISCH_TAC THEN MP_TAC th) THEN
501 DISCH_THEN(CONJUNCTS_THEN2
502 (fun th -> ASSUME_TAC th THEN X_CHOOSE_TAC `B2:real` (MATCH_MP
503 LINEAR_BOUNDED_POS th)) MP_TAC) THEN
504 FIRST_X_ASSUM(fun th -> MP_TAC th THEN MP_TAC(SPEC `e / &2 / B2` th)) THEN
505 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
506 DISCH_THEN(X_CHOOSE_THEN `d1:real` STRIP_ASSUME_TAC) THEN DISCH_TAC THEN
507 DISCH_THEN(MP_TAC o SPEC `e / &2 / (&1 + B1)`) THEN
508 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH; REAL_LT_ADD] THEN
509 DISCH_THEN(X_CHOOSE_THEN `de:real` STRIP_ASSUME_TAC) THEN
510 FIRST_X_ASSUM(MP_TAC o SPEC `&1`) THEN
511 REWRITE_TAC[REAL_LT_01; REAL_MUL_LID] THEN
512 DISCH_THEN(X_CHOOSE_THEN `d2:real` STRIP_ASSUME_TAC) THEN
513 MP_TAC(SPECL [`d1:real`; `d2:real`] REAL_DOWN2) THEN
514 ASM_SIMP_TAC[REAL_LT_DIV; REAL_LT_ADD; REAL_LT_01] THEN
515 DISCH_THEN(X_CHOOSE_THEN `d0:real` STRIP_ASSUME_TAC) THEN
516 MP_TAC(SPECL [`d0:real`; `de / (B1 + &1)`] REAL_DOWN2) THEN
517 ASM_SIMP_TAC[REAL_LT_DIV; REAL_LT_ADD; REAL_LT_01] THEN
518 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real` THEN
519 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `y:real^M` THEN
520 DISCH_TAC THEN UNDISCH_TAC
521 `!y. y IN s /\ norm(y - x) < d2
522 ==> norm ((f:real^M->real^N) y - f x - f'(y - x)) <= norm(y - x)` THEN
523 DISCH_THEN(MP_TAC o SPEC `y:real^M`) THEN ANTS_TAC THENL
524 [ASM_MESON_TAC[REAL_LT_TRANS]; DISCH_TAC] THEN
525 FIRST_X_ASSUM(MP_TAC o SPEC `y:real^M`) THEN ANTS_TAC THENL
526 [ASM_MESON_TAC[REAL_LT_TRANS]; DISCH_TAC] THEN
527 FIRST_X_ASSUM(MP_TAC o SPEC `(f:real^M->real^N) y`) THEN ANTS_TAC THENL
528 [CONJ_TAC THENL [ASM_MESON_TAC[IN_IMAGE]; ALL_TAC] THEN
529 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC
530 `norm(f'(y - x)) + norm((f:real^M->real^N) y - f x - f'(y - x))` THEN
531 REWRITE_TAC[NORM_TRIANGLE_SUB] THEN
532 MATCH_MP_TAC REAL_LET_TRANS THEN
533 EXISTS_TAC `B1 * norm(y - x) + norm(y - x :real^M)` THEN
534 ASM_SIMP_TAC[REAL_LE_ADD2] THEN
535 REWRITE_TAC[REAL_ARITH `a * x + x = x * (a + &1)`] THEN
536 ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_LT_ADD; REAL_LT_01] THEN
537 ASM_MESON_TAC[REAL_LT_TRANS];
539 REWRITE_TAC[o_THM] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
540 EXISTS_TAC `norm((g:real^N->real^P)(f(y:real^M)) - g(f x) - g'(f y - f x)) +
541 norm((g(f y) - g(f x) - g'(f'(y - x))) -
542 (g(f y) - g(f x) - g'(f y - f x)))` THEN
543 REWRITE_TAC[NORM_TRIANGLE_SUB] THEN
544 REWRITE_TAC[VECTOR_ARITH `(a - b - c1) - (a - b - c2) = c2 - c1:real^M`] THEN
545 ASM_SIMP_TAC[GSYM LINEAR_SUB] THEN
546 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
547 `a <= d ==> b <= ee - d ==> a + b <= ee`)) THEN
548 MATCH_MP_TAC REAL_LE_TRANS THEN
549 EXISTS_TAC `B2 * norm((f:real^M->real^N) y - f x - f'(y - x))` THEN
550 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
551 EXISTS_TAC `B2 * e / &2 / B2 * norm(y - x :real^M)` THEN
552 ASM_SIMP_TAC[REAL_LE_LMUL; REAL_LT_IMP_LE] THEN REWRITE_TAC[real_div] THEN
553 ONCE_REWRITE_TAC[REAL_ARITH
554 `b * ((e * h) * b') * x <= e * x - d <=>
555 d <= e * (&1 - h * b' * b) * x`] THEN
556 ASM_SIMP_TAC[REAL_MUL_LINV; REAL_LT_IMP_NZ] THEN
557 CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
558 ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
559 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN
560 ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LT_ADD; REAL_LT_01] THEN
561 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
562 `norm(f'(y - x)) + norm((f:real^M->real^N) y - f x - f'(y - x))` THEN
563 REWRITE_TAC[NORM_TRIANGLE_SUB] THEN MATCH_MP_TAC(REAL_ARITH
564 `u <= x * b /\ v <= b ==> u + v <= b * (&1 + x)`) THEN
567 let DIFF_CHAIN_AT = prove
568 (`!f:real^M->real^N g:real^N->real^P f' g' x.
569 (f has_derivative f') (at x) /\
570 (g has_derivative g') (at (f x))
571 ==> ((g o f) has_derivative (g' o f')) (at x)`,
572 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
573 ASM_MESON_TAC[DIFF_CHAIN_WITHIN; LIM_WITHIN_SUBSET; SUBSET_UNIV;
574 HAS_DERIVATIVE_WITHIN_SUBSET]);;
576 (* ------------------------------------------------------------------------- *)
577 (* Composition rules stated just for differentiability. *)
578 (* ------------------------------------------------------------------------- *)
580 let DIFFERENTIABLE_LINEAR = prove
581 (`!net f:real^M->real^N. linear f ==> f differentiable net`,
582 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_LINEAR]);;
584 let DIFFERENTIABLE_CONST = prove
585 (`!c net. (\z. c) differentiable net`,
586 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_CONST]);;
588 let DIFFERENTIABLE_ID = prove
589 (`!net. (\z. z) differentiable net`,
590 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_ID]);;
592 let DIFFERENTIABLE_LIFT_COMPONENT = prove
593 (`!net:(real^N)net. (\x. lift(x$i)) differentiable net`,
594 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_LIFT_COMPONENT]);;
596 let DIFFERENTIABLE_CMUL = prove
597 (`!net f c. f differentiable net ==> (\x. c % f(x)) differentiable net`,
598 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_CMUL]);;
600 let DIFFERENTIABLE_NEG = prove
601 (`!f net. f differentiable net ==> (\z. --(f z)) differentiable net`,
602 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_NEG]);;
604 let DIFFERENTIABLE_ADD = prove
606 f differentiable net /\
608 ==> (\z. f z + g z) differentiable net`,
609 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_ADD]);;
611 let DIFFERENTIABLE_SUB = prove
613 f differentiable net /\
615 ==> (\z. f z - g z) differentiable net`,
616 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_SUB]);;
618 let DIFFERENTIABLE_VSUM = prove
621 (!a. a IN s ==> (f a) differentiable net)
622 ==> (\x. vsum s (\a. f a x)) differentiable net`,
623 REPEAT GEN_TAC THEN REWRITE_TAC[differentiable] THEN
624 GEN_REWRITE_TAC (LAND_CONV o TOP_DEPTH_CONV)
625 [RIGHT_IMP_EXISTS_THM; SKOLEM_THM; RIGHT_AND_EXISTS_THM] THEN
626 DISCH_THEN(CHOOSE_THEN (MP_TAC o MATCH_MP HAS_DERIVATIVE_VSUM)) THEN
629 let DIFFERENTIABLE_VSUM_NUMSEG = prove
632 (!i. m <= i /\ i <= n ==> (f i) differentiable net)
633 ==> (\x. vsum (m..n) (\a. f a x)) differentiable net`,
634 SIMP_TAC[DIFFERENTIABLE_VSUM; FINITE_NUMSEG; IN_NUMSEG]);;
636 let DIFFERENTIABLE_CHAIN_AT = prove
638 f differentiable (at x) /\
639 g differentiable (at(f x))
640 ==> (g o f) differentiable (at x)`,
641 REWRITE_TAC[differentiable] THEN MESON_TAC[DIFF_CHAIN_AT]);;
643 let DIFFERENTIABLE_CHAIN_WITHIN = prove
645 f differentiable (at x within s) /\
646 g differentiable (at(f x) within IMAGE f s)
647 ==> (g o f) differentiable (at x within s)`,
648 REWRITE_TAC[differentiable] THEN MESON_TAC[DIFF_CHAIN_WITHIN]);;
650 let DIFFERENTIABLE_COMPONENTWISE_WITHIN = prove
651 (`!f:real^M->real^N a s.
652 f differentiable (at a within s) <=>
653 !i. 1 <= i /\ i <= dimindex(:N)
654 ==> (\x. lift(f(x)$i)) differentiable (at a within s)`,
655 REPEAT GEN_TAC THEN REWRITE_TAC[differentiable] THEN
656 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)
657 [HAS_DERIVATIVE_COMPONENTWISE_WITHIN] THEN
658 REWRITE_TAC[RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN EQ_TAC THENL
659 [DISCH_THEN(X_CHOOSE_TAC `g':real^M->real^N`) THEN
660 EXISTS_TAC `\i x. lift((g':real^M->real^N) x$i)` THEN ASM_REWRITE_TAC[];
661 DISCH_THEN(X_CHOOSE_TAC `g':num->real^M->real^1`) THEN
662 EXISTS_TAC `(\x. lambda i. drop((g':num->real^M->real^1) i x))
663 :real^M->real^N` THEN
664 ASM_SIMP_TAC[LAMBDA_BETA; LIFT_DROP; ETA_AX]]);;
666 let DIFFERENTIABLE_COMPONENTWISE_AT = prove
667 (`!f:real^M->real^N a.
668 f differentiable (at a) <=>
669 !i. 1 <= i /\ i <= dimindex(:N)
670 ==> (\x. lift(f(x)$i)) differentiable (at a)`,
671 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
672 MATCH_ACCEPT_TAC DIFFERENTIABLE_COMPONENTWISE_WITHIN);;
674 (* ------------------------------------------------------------------------- *)
675 (* Similarly for "differentiable_on". *)
676 (* ------------------------------------------------------------------------- *)
678 let DIFFERENTIABLE_ON_LINEAR = prove
679 (`!f:real^M->real^N s. linear f ==> f differentiable_on s`,
680 SIMP_TAC[differentiable_on; DIFFERENTIABLE_LINEAR]);;
682 let DIFFERENTIABLE_ON_CONST = prove
683 (`!s c. (\z. c) differentiable_on s`,
684 REWRITE_TAC[differentiable_on; DIFFERENTIABLE_CONST]);;
686 let DIFFERENTIABLE_ON_ID = prove
687 (`!s. (\z. z) differentiable_on s`,
688 REWRITE_TAC[differentiable_on; DIFFERENTIABLE_ID]);;
690 let DIFFERENTIABLE_ON_COMPOSE = prove
691 (`!f g s. f differentiable_on s /\ g differentiable_on (IMAGE f s)
692 ==> (g o f) differentiable_on s`,
693 SIMP_TAC[differentiable_on; FORALL_IN_IMAGE] THEN
694 MESON_TAC[DIFFERENTIABLE_CHAIN_WITHIN]);;
696 let DIFFERENTIABLE_ON_NEG = prove
697 (`!f s. f differentiable_on s ==> (\z. --(f z)) differentiable_on s`,
698 SIMP_TAC[differentiable_on; DIFFERENTIABLE_NEG]);;
700 let DIFFERENTIABLE_ON_ADD = prove
702 f differentiable_on s /\ g differentiable_on s
703 ==> (\z. f z + g z) differentiable_on s`,
704 SIMP_TAC[differentiable_on; DIFFERENTIABLE_ADD]);;
706 let DIFFERENTIABLE_ON_SUB = prove
708 f differentiable_on s /\ g differentiable_on s
709 ==> (\z. f z - g z) differentiable_on s`,
710 SIMP_TAC[differentiable_on; DIFFERENTIABLE_SUB]);;
712 (* ------------------------------------------------------------------------- *)
713 (* Uniqueness of derivative. *)
715 (* The general result is a bit messy because we need approachability of the *)
716 (* limit point from any direction. But OK for nontrivial intervals etc. *)
717 (* ------------------------------------------------------------------------- *)
719 let FRECHET_DERIVATIVE_UNIQUE_WITHIN = prove
720 (`!f:real^M->real^N f' f'' x s.
721 (f has_derivative f') (at x within s) /\
722 (f has_derivative f'') (at x within s) /\
723 (!i e. 1 <= i /\ i <= dimindex(:M) /\ &0 < e
724 ==> ?d. &0 < abs(d) /\ abs(d) < e /\ (x + d % basis i) IN s)
726 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative] THEN
727 ONCE_REWRITE_TAC[CONJ_ASSOC] THEN
728 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC) THEN
729 SUBGOAL_THEN `(x:real^M) limit_point_of s` ASSUME_TAC THENL
730 [REWRITE_TAC[LIMPT_APPROACHABLE] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
731 FIRST_X_ASSUM(MP_TAC o SPECL [`1`; `e:real`]) THEN
732 ASM_REWRITE_TAC[DIMINDEX_GE_1; LE_REFL] THEN
733 DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
734 EXISTS_TAC `(x:real^M) + d % basis 1` THEN
735 ASM_REWRITE_TAC[dist] THEN ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
736 ASM_SIMP_TAC[VECTOR_ADD_SUB; NORM_MUL; NORM_BASIS; DIMINDEX_GE_1; LE_REFL;
737 VECTOR_MUL_EQ_0; REAL_MUL_RID; DE_MORGAN_THM; REAL_ABS_NZ;
740 DISCH_THEN(CONJUNCTS_THEN (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
741 REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_SUB) THEN
742 SUBGOAL_THEN `netlimit(at x within s) = x:real^M` SUBST_ALL_TAC THENL
743 [ASM_MESON_TAC[NETLIMIT_WITHIN; TRIVIAL_LIMIT_WITHIN]; ALL_TAC] THEN
744 REWRITE_TAC[GSYM VECTOR_SUB_LDISTRIB; NORM_MUL] THEN
745 REWRITE_TAC[VECTOR_ARITH
746 `fx - (fa + f'') - (fx - (fa + f')):real^M = f' - f''`] THEN
747 DISCH_TAC THEN MATCH_MP_TAC LINEAR_EQ_STDBASIS THEN ASM_REWRITE_TAC[] THEN
748 X_GEN_TAC `i:num` THEN STRIP_TAC THEN
749 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
750 GEN_REWRITE_TAC I [TAUT `p = ~ ~p`] THEN
751 PURE_REWRITE_TAC[GSYM NORM_POS_LT] THEN DISCH_TAC THEN ABBREV_TAC
752 `e = norm((f':real^M->real^N) (basis i) - f''(basis i :real^M))` THEN
753 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_WITHIN]) THEN
754 DISCH_THEN(MP_TAC o SPEC `e:real`) THEN
755 ASM_REWRITE_TAC[dist; VECTOR_SUB_RZERO] THEN
756 DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
757 FIRST_X_ASSUM(MP_TAC o SPECL [`i:num`; `d:real`]) THEN ASM_REWRITE_TAC[] THEN
758 DISCH_THEN(X_CHOOSE_THEN `c:real` STRIP_ASSUME_TAC) THEN
759 FIRST_X_ASSUM(MP_TAC o SPEC `(x:real^M) + c % basis i`) THEN
760 ASM_REWRITE_TAC[VECTOR_ADD_SUB; NORM_MUL] THEN
761 ASM_SIMP_TAC[NORM_BASIS; REAL_MUL_RID] THEN
762 ASM_SIMP_TAC[LINEAR_CMUL; GSYM VECTOR_SUB_LDISTRIB; NORM_MUL] THEN
763 REWRITE_TAC[REAL_ABS_INV; REAL_ABS_ABS] THEN
764 ASM_SIMP_TAC[REAL_MUL_LINV; REAL_LT_IMP_NZ; REAL_MUL_ASSOC] THEN
765 REWRITE_TAC[REAL_MUL_LID; REAL_LT_REFL]);;
767 let FRECHET_DERIVATIVE_UNIQUE_AT = prove
768 (`!f:real^M->real^N f' f'' x.
769 (f has_derivative f') (at x) /\ (f has_derivative f'') (at x)
771 REPEAT STRIP_TAC THEN MATCH_MP_TAC FRECHET_DERIVATIVE_UNIQUE_WITHIN THEN
773 [`f:real^M->real^N`; `x:real^M`; `(:real^M)`] THEN
774 ASM_REWRITE_TAC[IN_UNIV; WITHIN_UNIV] THEN
775 MESON_TAC[REAL_ARITH `&0 < e ==> &0 < abs(e / &2) /\ abs(e / &2) < e`]);;
777 let HAS_FRECHET_DERIVATIVE_UNIQUE_AT = prove
778 (`!f:real^M->real^N f' x.
779 (f has_derivative f') (at x)
780 ==> frechet_derivative f (at x) = f'`,
781 REPEAT STRIP_TAC THEN MATCH_MP_TAC FRECHET_DERIVATIVE_UNIQUE_AT THEN
782 MAP_EVERY EXISTS_TAC [`f:real^M->real^N`; `x:real^M`] THEN
783 ASM_REWRITE_TAC[frechet_derivative] THEN CONV_TAC SELECT_CONV THEN
786 let FRECHET_DERIVATIVE_CONST_AT = prove
787 (`!c:real^N a:real^M. frechet_derivative (\x. c) (at a) = \h. vec 0`,
788 REPEAT GEN_TAC THEN MATCH_MP_TAC HAS_FRECHET_DERIVATIVE_UNIQUE_AT THEN
789 REWRITE_TAC[HAS_DERIVATIVE_CONST]);;
791 let FRECHET_DERIVATIVE_UNIQUE_WITHIN_CLOSED_INTERVAL = prove
792 (`!f:real^M->real^N f' f'' x a b.
793 (!i. 1 <= i /\ i <= dimindex(:M) ==> a$i < b$i) /\
794 x IN interval[a,b] /\
795 (f has_derivative f') (at x within interval[a,b]) /\
796 (f has_derivative f'') (at x within interval[a,b])
798 REPEAT STRIP_TAC THEN MATCH_MP_TAC FRECHET_DERIVATIVE_UNIQUE_WITHIN THEN
800 [`f:real^M->real^N`; `x:real^M`; `interval[a:real^M,b]`] THEN
801 ASM_REWRITE_TAC[] THEN
802 MAP_EVERY X_GEN_TAC [`i:num`; `e:real`] THEN STRIP_TAC THEN
803 MATCH_MP_TAC(MESON[] `(?a. P a \/ P(--a)) ==> (?a:real. P a)`) THEN
804 EXISTS_TAC `(min ((b:real^M)$i - (a:real^M)$i) e) / &2` THEN
805 REWRITE_TAC[REAL_ABS_NEG; GSYM LEFT_OR_DISTRIB] THEN
806 REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
807 [UNDISCH_TAC `&0 < e` THEN FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN
808 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
810 UNDISCH_TAC `(x:real^M) IN interval[a,b]` THEN REWRITE_TAC[IN_INTERVAL] THEN
812 ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
813 BASIS_COMPONENT] THEN
815 `!P. (!j. 1 <= j /\ j <= dimindex(:M) ==> P j) <=>
817 (!j. 1 <= j /\ j <= dimindex(:M) /\ ~(j = i) ==> P j)`
818 (fun th -> ONCE_REWRITE_TAC[th])
819 THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
820 ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_ADD_RID; REAL_MUL_RID] THEN
821 REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
822 UNDISCH_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
824 let FRECHET_DERIVATIVE_UNIQUE_WITHIN_OPEN_INTERVAL = prove
825 (`!f:real^M->real^N f' f'' x a b.
826 x IN interval(a,b) /\
827 (f has_derivative f') (at x within interval(a,b)) /\
828 (f has_derivative f'') (at x within interval(a,b))
830 REPEAT STRIP_TAC THEN MATCH_MP_TAC FRECHET_DERIVATIVE_UNIQUE_WITHIN THEN
832 [`f:real^M->real^N`; `x:real^M`; `interval(a:real^M,b)`] THEN
833 ASM_REWRITE_TAC[] THEN
834 MAP_EVERY X_GEN_TAC [`i:num`; `e:real`] THEN STRIP_TAC THEN
835 MATCH_MP_TAC(MESON[] `(?a. P a \/ P(--a)) ==> (?a:real. P a)`) THEN
836 EXISTS_TAC `(min ((b:real^M)$i - (a:real^M)$i) e) / &3` THEN
837 REWRITE_TAC[REAL_ABS_NEG; GSYM LEFT_OR_DISTRIB] THEN
838 REWRITE_TAC[CONJ_ASSOC] THEN CONJ_TAC THENL
839 [UNDISCH_TAC `&0 < e` THEN
840 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_INTERVAL]) THEN
841 DISCH_THEN(MP_TAC o SPEC `i:num`) THEN
842 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
844 UNDISCH_TAC `(x:real^M) IN interval(a,b)` THEN REWRITE_TAC[IN_INTERVAL] THEN
846 ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
847 BASIS_COMPONENT] THEN
849 `!P. (!j. 1 <= j /\ j <= dimindex(:M) ==> P j) <=>
851 (!j. 1 <= j /\ j <= dimindex(:M) /\ ~(j = i) ==> P j)`
852 (fun th -> ONCE_REWRITE_TAC[th])
853 THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
854 ASM_SIMP_TAC[REAL_MUL_RZERO; REAL_ADD_RID; REAL_MUL_RID] THEN
855 REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `i:num`)) THEN
856 UNDISCH_TAC `&0 < e` THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
858 let FRECHET_DERIVATIVE_AT = prove
859 (`!f:real^M->real^N f' x.
860 (f has_derivative f') (at x) ==> (f' = frechet_derivative f (at x))`,
861 MESON_TAC[has_derivative; FRECHET_DERIVATIVE_WORKS;
862 differentiable; FRECHET_DERIVATIVE_UNIQUE_AT]);;
864 let FRECHET_DERIVATIVE_WITHIN_CLOSED_INTERVAL = prove
865 (`!f:real^M->real^N f' x a b.
866 (!i. 1 <= i /\ i <= dimindex(:M) ==> a$i < b$i) /\
867 x IN interval[a,b] /\
868 (f has_derivative f') (at x within interval[a,b])
869 ==> frechet_derivative f (at x within interval[a,b]) = f'`,
870 ASM_MESON_TAC[has_derivative; FRECHET_DERIVATIVE_WORKS;
871 differentiable; FRECHET_DERIVATIVE_UNIQUE_WITHIN_CLOSED_INTERVAL]);;
873 (* ------------------------------------------------------------------------- *)
874 (* Component of the differential must be zero if it exists at a local *)
875 (* maximum or minimum for that corresponding component. Start with slightly *)
876 (* sharper forms that fix the sign of the derivative on the boundary. *)
877 (* ------------------------------------------------------------------------- *)
879 let DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM = prove
880 (`!f:real^M->real^N f' x s k e.
881 1 <= k /\ k <= dimindex(:N) /\
882 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\
883 &0 < e /\ (!w. w IN s INTER ball(x,e) ==> (f x)$k <= (f w)$k)
884 ==> !y. y IN s ==> &0 <= (f'(y - x))$k`,
885 REWRITE_TAC[has_derivative_within] THEN REPEAT STRIP_TAC THEN
886 ASM_CASES_TAC `y:real^M = x` THENL
887 [ASM_MESON_TAC[VECTOR_SUB_REFL; LINEAR_0; VEC_COMPONENT; REAL_LE_REFL];
889 ONCE_REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN
890 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_WITHIN]) THEN
891 DISCH_THEN(MP_TAC o SPEC
892 `--((f':real^M->real^N)(y - x)$k) / norm(y - x)`) THEN
893 ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ;
894 NOT_EXISTS_THM; REAL_ARITH `&0 < --x <=> x < &0`] THEN
895 X_GEN_TAC `d:real` THEN
896 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
897 ABBREV_TAC `de = min (&1) ((min d e) / &2 / norm(y - x:real^M))` THEN
898 DISCH_THEN(MP_TAC o SPEC `x + de % (y - x):real^M`) THEN
899 REWRITE_TAC[dist; VECTOR_ADD_SUB; NOT_IMP; GSYM CONJ_ASSOC] THEN
900 SUBGOAL_THEN `norm(de % (y - x):real^M) < min d e` MP_TAC THENL
901 [ASM_SIMP_TAC[NORM_MUL; GSYM REAL_LT_RDIV_EQ;
902 NORM_POS_LT; VECTOR_SUB_EQ] THEN
903 EXPAND_TAC "de" THEN MATCH_MP_TAC(REAL_ARITH
904 `&0 < de / x ==> abs(min (&1) (de / &2 / x)) < de / x`) THEN
905 ASM_SIMP_TAC[REAL_LT_DIV; REAL_LT_MIN; NORM_POS_LT; VECTOR_SUB_EQ];
906 REWRITE_TAC[REAL_LT_MIN] THEN STRIP_TAC] THEN
907 SUBGOAL_THEN `&0 < de /\ de <= &1` STRIP_ASSUME_TAC THENL
908 [EXPAND_TAC "de" THEN CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
909 ASM_SIMP_TAC[REAL_LT_MIN; REAL_LT_01; REAL_HALF; REAL_LT_DIV;
910 NORM_POS_LT; VECTOR_SUB_EQ];
912 MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
913 [REWRITE_TAC[VECTOR_ARITH
914 `x + a % (y - x):real^N = (&1 - a) % x + a % y`] THEN
915 MATCH_MP_TAC IN_CONVEX_SET THEN ASM_SIMP_TAC[REAL_LT_IMP_LE];
917 ASM_REWRITE_TAC[] THEN REWRITE_TAC[NORM_MUL] THEN
918 ASM_SIMP_TAC[REAL_LT_MUL; REAL_ARITH `&0 < x ==> &0 < abs x`;
919 NORM_POS_LT; VECTOR_SUB_EQ; VECTOR_SUB_RZERO] THEN
920 MATCH_MP_TAC(NORM_ARITH
921 `abs(y$k) <= norm(y) /\ ~(abs(y$k) < e) ==> ~(norm y < e)`) THEN
922 ASM_SIMP_TAC[COMPONENT_LE_NORM] THEN REWRITE_TAC[VECTOR_MUL_COMPONENT] THEN
923 REWRITE_TAC[REAL_ABS_INV; REAL_ABS_MUL; REAL_ABS_NORM; REAL_ABS_ABS] THEN
924 REWRITE_TAC[REAL_NOT_LT; REAL_INV_MUL; REAL_ARITH
925 `d <= (a * inv b) * c <=> d <= (c * a) / b`] THEN
926 ASM_SIMP_TAC[REAL_LE_DIV2_EQ; NORM_POS_LT; VECTOR_SUB_EQ] THEN
927 ASM_SIMP_TAC[GSYM real_div; REAL_LE_RDIV_EQ; VECTOR_SUB_COMPONENT;
928 VECTOR_ADD_COMPONENT; REAL_ARITH `&0 < x ==> &0 < abs x`] THEN
929 MATCH_MP_TAC(REAL_ARITH
930 `fx <= fy /\ a = --b /\ b < &0 ==> a <= abs(fy - (fx + b))`) THEN
931 FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP LINEAR_CMUL th]) THEN
932 ASM_SIMP_TAC[real_abs; VECTOR_MUL_COMPONENT; REAL_LT_IMP_LE] THEN
933 ONCE_REWRITE_TAC[REAL_ARITH `x * y < &0 <=> &0 < x * --y`] THEN
934 ASM_SIMP_TAC[REAL_LT_MUL_EQ] THEN
935 CONJ_TAC THENL [FIRST_X_ASSUM MATCH_MP_TAC; ASM_REAL_ARITH_TAC] THEN
936 ASM_REWRITE_TAC[IN_INTER; IN_BALL; NORM_ARITH
937 `dist(x:real^M,x + e) = norm e`]);;
939 let DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM = prove
940 (`!f:real^M->real^N f' x s k e.
941 1 <= k /\ k <= dimindex(:N) /\
942 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\
943 &0 < e /\ (!w. w IN s INTER ball(x,e) ==> (f w)$k <= (f x)$k)
944 ==> !y. y IN s ==> (f'(y - x))$k <= &0`,
945 REPEAT STRIP_TAC THEN
947 [`\x. --((f:real^M->real^N) x)`; `\x. --((f':real^M->real^N) x)`;
948 `x:real^M`; `s:real^M->bool`; `k:num`; `e:real`]
949 DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM) THEN
950 ASM_SIMP_TAC[HAS_DERIVATIVE_NEG] THEN
951 ASM_SIMP_TAC[REAL_LE_NEG2; VECTOR_NEG_COMPONENT; REAL_NEG_GE0]);;
953 let DROP_DIFFERENTIAL_POS_AT_MINIMUM = prove
954 (`!f:real^N->real^1 f' x s e.
955 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\
956 &0 < e /\ (!w. w IN s INTER ball(x,e) ==> drop(f x) <= drop(f w))
957 ==> !y. y IN s ==> &0 <= drop(f'(y - x))`,
958 REPEAT GEN_TAC THEN REWRITE_TAC[drop] THEN STRIP_TAC THEN
959 MATCH_MP_TAC DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM THEN
960 MAP_EVERY EXISTS_TAC [`f:real^N->real^1`; `e:real`] THEN
961 ASM_REWRITE_TAC[DIMINDEX_1; LE_REFL]);;
963 let DROP_DIFFERENTIAL_NEG_AT_MAXIMUM = prove
964 (`!f:real^N->real^1 f' x s e.
965 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\
966 &0 < e /\ (!w. w IN s INTER ball(x,e) ==> drop(f w) <= drop(f x))
967 ==> !y. y IN s ==> drop(f'(y - x)) <= &0`,
968 REPEAT GEN_TAC THEN REWRITE_TAC[drop] THEN STRIP_TAC THEN
969 MATCH_MP_TAC DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM THEN
970 MAP_EVERY EXISTS_TAC [`f:real^N->real^1`; `e:real`] THEN
971 ASM_REWRITE_TAC[DIMINDEX_1; LE_REFL]);;
973 let DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN = prove
974 (`!f:real^M->real^N f' x s k.
975 1 <= k /\ k <= dimindex(:N) /\
976 x IN s /\ open s /\ (f has_derivative f') (at x) /\
977 ((!w. w IN s ==> (f w)$k <= (f x)$k) \/
978 (!w. w IN s ==> (f x)$k <= (f w)$k))
979 ==> !h. (f' h)$k = &0`,
981 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
982 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [OPEN_CONTAINS_CBALL]) THEN
983 DISCH_THEN(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[SUBSET] THEN
984 DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
985 FIRST_X_ASSUM DISJ_CASES_TAC THENL
986 [MP_TAC(ISPECL [`f:real^M->real^N`; `f':real^M->real^N`;
987 `x:real^M`; `cball(x:real^M,e)`; `k:num`; `e:real`]
988 DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM);
989 MP_TAC(ISPECL [`f:real^M->real^N`; `f':real^M->real^N`;
990 `x:real^M`; `cball(x:real^M,e)`; `k:num`; `e:real`]
991 DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM)] THEN
992 ASM_SIMP_TAC[HAS_DERIVATIVE_AT_WITHIN; CENTRE_IN_CBALL;
993 CONVEX_CBALL; REAL_LT_IMP_LE; IN_INTER] THEN
994 DISCH_THEN(LABEL_TAC "*") THEN X_GEN_TAC `h:real^M` THEN
995 FIRST_X_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [has_derivative_at]) THEN
996 (ASM_CASES_TAC `h:real^M = vec 0` THENL
997 [ASM_MESON_TAC[LINEAR_0; VEC_COMPONENT]; ALL_TAC]) THEN
998 REMOVE_THEN "*" (fun th ->
999 MP_TAC(SPEC `x + e / norm h % h:real^M` th) THEN
1000 MP_TAC(SPEC `x - e / norm h % h:real^M` th)) THEN
1001 REWRITE_TAC[IN_CBALL; NORM_ARITH
1002 `dist(x:real^N,x - e) = norm e /\ dist(x:real^N,x + e) = norm e`] THEN
1003 REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
1004 ASM_SIMP_TAC[real_abs; REAL_DIV_RMUL; NORM_EQ_0; REAL_LT_IMP_LE;
1006 REWRITE_TAC[VECTOR_ARITH `x - e - x:real^N = --e /\ (x + e) - x = e`] THEN
1007 FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP LINEAR_NEG th]) THEN
1008 REWRITE_TAC[IMP_IMP; REAL_ARITH `&0 <= --x /\ &0 <= x <=> x = &0`;
1009 VECTOR_NEG_COMPONENT; REAL_ARITH `--x <= &0 /\ x <= &0 <=> x = &0`] THEN
1010 DISCH_THEN(MP_TAC o AP_TERM `(*) (norm(h:real^M) / e)`) THEN
1011 REWRITE_TAC[GSYM VECTOR_MUL_COMPONENT] THEN
1012 FIRST_ASSUM(fun th -> REWRITE_TAC[GSYM(MATCH_MP LINEAR_CMUL th)]) THEN
1013 REWRITE_TAC[REAL_MUL_RZERO; VECTOR_MUL_ASSOC] THEN
1014 ASM_SIMP_TAC[REAL_FIELD `~(x = &0) /\ ~(y = &0) ==> x / y * y / x = &1`;
1015 NORM_EQ_0; REAL_LT_IMP_NZ; VECTOR_MUL_LID]);;
1017 let DIFFERENTIAL_ZERO_MAXMIN_COMPONENT = prove
1018 (`!f:real^M->real^N x e k.
1019 1 <= k /\ k <= dimindex(:N) /\ &0 < e /\
1020 ((!y. y IN ball(x,e) ==> (f y)$k <= (f x)$k) \/
1021 (!y. y IN ball(x,e) ==> (f x)$k <= (f y)$k)) /\
1022 f differentiable (at x)
1023 ==> (jacobian f (at x) $ k = vec 0)`,
1024 REWRITE_TAC[JACOBIAN_WORKS] THEN REPEAT STRIP_TAC THEN
1026 [`f:real^M->real^N`; `\h. jacobian (f:real^M->real^N) (at x) ** h`;
1027 `x:real^M`; `ball(x:real^M,e)`; `k:num`]
1028 DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN) THEN
1029 ASM_REWRITE_TAC[CENTRE_IN_BALL; OPEN_BALL] THEN
1030 ASM_SIMP_TAC[MATRIX_VECTOR_MUL_COMPONENT; FORALL_DOT_EQ_0]);;
1032 let DIFFERENTIAL_ZERO_MAXMIN = prove
1033 (`!f:real^N->real^1 f' x s.
1034 x IN s /\ open s /\ (f has_derivative f') (at x) /\
1035 ((!y. y IN s ==> drop(f y) <= drop(f x)) \/
1036 (!y. y IN s ==> drop(f x) <= drop(f y)))
1037 ==> (f' = \v. vec 0)`,
1038 REPEAT STRIP_TAC THEN
1039 MP_TAC(ISPECL [`f:real^N->real^1`; `f':real^N->real^1`;
1040 `x:real^N`; `s:real^N->bool`; `1:num`]
1041 DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN) THEN
1042 ASM_REWRITE_TAC[GSYM drop; DIMINDEX_1; LE_REFL] THEN
1043 REWRITE_TAC[GSYM LIFT_EQ; LIFT_NUM; FUN_EQ_THM; LIFT_DROP]);;
1045 (* ------------------------------------------------------------------------- *)
1046 (* The traditional Rolle theorem in one dimension. *)
1047 (* ------------------------------------------------------------------------- *)
1050 (`!f:real^1->real^1 f' a b.
1051 drop a < drop b /\ (f a = f b) /\
1052 f continuous_on interval[a,b] /\
1053 (!x. x IN interval(a,b) ==> (f has_derivative f'(x)) (at x))
1054 ==> ?x. x IN interval(a,b) /\ (f'(x) = \v. vec 0)`,
1055 REPEAT STRIP_TAC THEN
1056 MP_TAC(ISPECL [`f:real^1->real^1`; `a:real^1`; `b:real^1`]
1057 CONTINUOUS_IVT_LOCAL_EXTREMUM) THEN
1058 ASM_SIMP_TAC[SEGMENT_1; REAL_LT_IMP_LE] THEN
1059 ANTS_TAC THENL [ASM_MESON_TAC[REAL_LT_REFL]; MATCH_MP_TAC MONO_EXISTS] THEN
1060 X_GEN_TAC `c:real^1` THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1061 MATCH_MP_TAC DIFFERENTIAL_ZERO_MAXMIN THEN MAP_EVERY EXISTS_TAC
1062 [`f:real^1->real^1`; `c:real^1`; `interval(a:real^1,b)`] THEN
1063 ASM_MESON_TAC[INTERVAL_OPEN_SUBSET_CLOSED; SUBSET; OPEN_INTERVAL]);;
1065 (* ------------------------------------------------------------------------- *)
1066 (* One-dimensional mean value theorem. *)
1067 (* ------------------------------------------------------------------------- *)
1070 (`!f:real^1->real^1 f' a b.
1072 f continuous_on interval[a,b] /\
1073 (!x. x IN interval(a,b) ==> (f has_derivative f'(x)) (at x))
1074 ==> ?x. x IN interval(a,b) /\ (f(b) - f(a) = f'(x) (b - a))`,
1075 REPEAT STRIP_TAC THEN
1076 MP_TAC(SPECL [`\x. f(x) - (drop(f b - f a) / drop(b - a)) % x`;
1077 `\k:real^1 x:real^1.
1078 f'(k)(x) - (drop(f b - f a) / drop(b - a)) % x`;
1079 `a:real^1`; `b:real^1`]
1081 REWRITE_TAC[] THEN ANTS_TAC THENL
1082 [ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_CMUL; CONTINUOUS_ON_ID] THEN
1084 [REWRITE_TAC[VECTOR_ARITH
1085 `(fa - k % a = fb - k % b) <=> (fb - fa = k % (b - a))`];
1086 REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_SUB THEN
1087 ASM_SIMP_TAC[HAS_DERIVATIVE_CMUL; HAS_DERIVATIVE_ID; ETA_AX]];
1088 MATCH_MP_TAC MONO_EXISTS THEN SIMP_TAC[FUN_EQ_THM] THEN
1089 X_GEN_TAC `x:real^1` THEN
1090 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `b - a:real^1`))] THEN
1091 SIMP_TAC[VECTOR_SUB_EQ; GSYM DROP_EQ; DROP_SUB; DROP_CMUL] THEN
1092 ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_SUB_LT; REAL_LT_IMP_NZ]);;
1094 let MVT_SIMPLE = prove
1095 (`!f:real^1->real^1 f' a b.
1097 (!x. x IN interval[a,b]
1098 ==> (f has_derivative f'(x)) (at x within interval[a,b]))
1099 ==> ?x. x IN interval(a,b) /\ (f(b) - f(a) = f'(x) (b - a))`,
1101 REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
1102 REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1104 [MATCH_MP_TAC DIFFERENTIABLE_IMP_CONTINUOUS_ON THEN
1105 ASM_MESON_TAC[differentiable_on; differentiable];
1106 ASM_MESON_TAC[HAS_DERIVATIVE_WITHIN_OPEN; OPEN_INTERVAL;
1107 HAS_DERIVATIVE_WITHIN_SUBSET; INTERVAL_OPEN_SUBSET_CLOSED;
1110 let MVT_VERY_SIMPLE = prove
1111 (`!f:real^1->real^1 f' a b.
1113 (!x. x IN interval[a,b]
1114 ==> (f has_derivative f'(x)) (at x within interval[a,b]))
1115 ==> ?x. x IN interval[a,b] /\ (f(b) - f(a) = f'(x) (b - a))`,
1116 REPEAT GEN_TAC THEN ASM_CASES_TAC `b:real^1 = a` THENL
1117 [ASM_REWRITE_TAC[VECTOR_SUB_REFL] THEN REPEAT STRIP_TAC THEN
1118 FIRST_X_ASSUM(MP_TAC o SPEC `a:real^1`) THEN
1119 REWRITE_TAC[INTERVAL_SING; IN_SING; has_derivative; UNWIND_THM2] THEN
1120 MESON_TAC[LINEAR_0];
1121 ASM_REWRITE_TAC[REAL_LE_LT; DROP_EQ] THEN
1122 DISCH_THEN(MP_TAC o MATCH_MP MVT_SIMPLE) THEN
1123 MATCH_MP_TAC MONO_EXISTS THEN
1124 SIMP_TAC[REWRITE_RULE[SUBSET] INTERVAL_OPEN_SUBSET_CLOSED]]);;
1126 (* ------------------------------------------------------------------------- *)
1127 (* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *)
1128 (* ------------------------------------------------------------------------- *)
1130 let MVT_GENERAL = prove
1131 (`!f:real^1->real^N f' a b.
1133 f continuous_on interval[a,b] /\
1134 (!x. x IN interval(a,b) ==> (f has_derivative f'(x)) (at x))
1135 ==> ?x. x IN interval(a,b) /\
1136 norm(f(b) - f(a)) <= norm(f'(x) (b - a))`,
1137 REPEAT STRIP_TAC THEN
1138 MP_TAC(SPECL [`(lift o (\y. (f(b) - f(a)) dot y)) o (f:real^1->real^N)`;
1139 `\x t. lift((f(b:real^1) - f(a)) dot
1140 ((f':real^1->real^1->real^N) x t))`;
1141 `a:real^1`; `b:real^1`] MVT) THEN
1143 [ASM_SIMP_TAC[CONTINUOUS_ON_LIFT_DOT; CONTINUOUS_ON_COMPOSE] THEN
1144 REPEAT STRIP_TAC THEN REWRITE_TAC[o_DEF] THEN
1145 MATCH_MP_TAC HAS_DERIVATIVE_LIFT_DOT THEN ASM_SIMP_TAC[ETA_AX];
1147 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `x:real^1` THEN
1148 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1149 ASM_REWRITE_TAC[o_THM; GSYM LIFT_SUB; GSYM DOT_RSUB; LIFT_EQ] THEN
1150 DISCH_TAC THEN ASM_CASES_TAC `(f:real^1->real^N) b = f a` THENL
1151 [ASM_REWRITE_TAC[VECTOR_SUB_REFL; NORM_0; NORM_POS_LE]; ALL_TAC] THEN
1152 MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN
1153 EXISTS_TAC `norm((f:real^1->real^N) b - f a)` THEN
1154 ASM_REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ; GSYM REAL_POW_2] THEN
1155 ASM_REWRITE_TAC[NORM_POW_2; NORM_CAUCHY_SCHWARZ]);;
1157 (* ------------------------------------------------------------------------- *)
1158 (* Still more general bound theorem. *)
1159 (* ------------------------------------------------------------------------- *)
1161 let DIFFERENTIABLE_BOUND = prove
1162 (`!f:real^M->real^N f' s B.
1164 (!x. x IN s ==> (f has_derivative f'(x)) (at x within s)) /\
1165 (!x. x IN s ==> onorm(f'(x)) <= B)
1166 ==> !x y. x IN s /\ y IN s ==> norm(f(x) - f(y)) <= B * norm(x - y)`,
1167 ONCE_REWRITE_TAC[NORM_SUB] THEN REPEAT STRIP_TAC THEN
1169 `!x y. x IN s ==> norm((f':real^M->real^M->real^N)(x) y) <= B * norm(y)`
1171 [ASM_MESON_TAC[ONORM; has_derivative; REAL_LE_TRANS; NORM_POS_LE;
1172 REAL_LE_RMUL]; ALL_TAC] THEN
1174 `!u. u IN interval[vec 0,vec 1] ==> (x + drop u % (y - x) :real^M) IN s`
1176 [REWRITE_TAC[IN_INTERVAL; FORALL_DIMINDEX_1; drop] THEN
1177 SIMP_TAC[VEC_COMPONENT; LE_REFL; DIMINDEX_1] THEN
1178 REWRITE_TAC[VECTOR_ARITH `x + u % (y - x) = (&1 - u) % x + u % y`] THEN
1179 ASM_MESON_TAC[CONVEX_ALT];
1182 `!u. u IN interval(vec 0,vec 1) ==> (x + drop u % (y - x) :real^M) IN s`
1184 [ASM_MESON_TAC[SUBSET; INTERVAL_OPEN_SUBSET_CLOSED]; ALL_TAC] THEN
1186 [`(f:real^M->real^N) o (\u. x + drop u % (y - x))`;
1187 `\u. (f':real^M->real^M->real^N) (x + drop u % (y - x)) o
1188 (\u. vec 0 + drop u % (y - x))`;
1189 `vec 0:real^1`; `vec 1:real^1`] MVT_GENERAL) THEN
1190 REWRITE_TAC[o_THM; DROP_VEC; VECTOR_ARITH `x + &1 % (y - x) = y`;
1191 VECTOR_MUL_LZERO; VECTOR_SUB_RZERO; VECTOR_ADD_RID] THEN
1192 REWRITE_TAC[VECTOR_MUL_LID] THEN ANTS_TAC THENL
1193 [ALL_TAC; ASM_MESON_TAC[VECTOR_ADD_LID; REAL_LE_TRANS]] THEN
1194 REWRITE_TAC[REAL_LT_01] THEN CONJ_TAC THENL
1195 [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1196 SIMP_TAC[CONTINUOUS_ON_ADD; CONTINUOUS_ON_CONST; CONTINUOUS_ON_VMUL;
1197 o_DEF; LIFT_DROP; CONTINUOUS_ON_ID] THEN
1198 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN EXISTS_TAC `s:real^M->bool` THEN
1199 ASM_REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
1200 ASM_MESON_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN; differentiable;
1201 CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN];
1203 X_GEN_TAC `a:real^1` THEN DISCH_TAC THEN
1204 SUBGOAL_THEN `a IN interval(vec 0:real^1,vec 1) /\
1205 open(interval(vec 0:real^1,vec 1))`
1206 MP_TAC THENL [ASM_MESON_TAC[OPEN_INTERVAL]; ALL_TAC] THEN
1207 DISCH_THEN(fun th -> ONCE_REWRITE_TAC[GSYM(MATCH_MP
1208 HAS_DERIVATIVE_WITHIN_OPEN th)]) THEN
1209 MATCH_MP_TAC DIFF_CHAIN_WITHIN THEN
1210 ASM_SIMP_TAC[HAS_DERIVATIVE_ADD; HAS_DERIVATIVE_CONST;
1211 HAS_DERIVATIVE_VMUL_DROP; HAS_DERIVATIVE_ID] THEN
1212 MATCH_MP_TAC HAS_DERIVATIVE_WITHIN_SUBSET THEN
1213 EXISTS_TAC `s:real^M->bool` THEN
1214 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN
1215 ASM_MESON_TAC[INTERVAL_OPEN_SUBSET_CLOSED; SUBSET]);;
1217 (* ------------------------------------------------------------------------- *)
1218 (* In particular. *)
1219 (* ------------------------------------------------------------------------- *)
1221 let HAS_DERIVATIVE_ZERO_CONSTANT = prove
1222 (`!f:real^M->real^N s.
1224 (!x. x IN s ==> (f has_derivative (\h. vec 0)) (at x within s))
1225 ==> ?c. !x. x IN s ==> f(x) = c`,
1226 REPEAT STRIP_TAC THEN
1227 MP_TAC(ISPECL [`f:real^M->real^N`; `(\x h. vec 0):real^M->real^M->real^N`;
1228 `s:real^M->bool`; `&0`] DIFFERENTIABLE_BOUND) THEN
1229 ASM_REWRITE_TAC[REAL_MUL_LZERO; ONORM_CONST; NORM_0; REAL_LE_REFL] THEN
1230 SIMP_TAC[NORM_LE_0; VECTOR_SUB_EQ] THEN MESON_TAC[]);;
1232 let HAS_DERIVATIVE_ZERO_UNIQUE = prove
1233 (`!f s a c. convex s /\ a IN s /\ f a = c /\
1234 (!x. x IN s ==> (f has_derivative (\h. vec 0)) (at x within s))
1235 ==> !x. x IN s ==> f x = c`,
1236 MESON_TAC[HAS_DERIVATIVE_ZERO_CONSTANT]);;
1238 let HAS_DERIVATIVE_ZERO_CONNECTED_CONSTANT = prove
1239 (`!f:real^M->real^N s.
1240 open s /\ connected s /\
1241 (!x. x IN s ==> (f has_derivative (\h. vec 0)) (at x))
1242 ==> ?c. !x. x IN s ==> f(x) = c`,
1243 REPEAT STRIP_TAC THEN
1244 ASM_CASES_TAC `s:real^M->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
1245 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
1246 DISCH_THEN(X_CHOOSE_TAC `a:real^M`) THEN
1247 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [CONNECTED_CLOPEN]) THEN
1248 DISCH_THEN(MP_TAC o SPEC `{x | x IN s /\ (f:real^M->real^N) x = f a}`) THEN
1249 ANTS_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN CONJ_TAC THENL
1250 [SIMP_TAC[open_in; SUBSET; IN_ELIM_THM] THEN
1251 X_GEN_TAC `x:real^M` THEN STRIP_TAC THEN
1252 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [OPEN_CONTAINS_BALL]) THEN
1253 DISCH_THEN(MP_TAC o SPEC `x:real^M`) THEN ASM_REWRITE_TAC[] THEN
1254 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `e:real` THEN
1255 REWRITE_TAC[SUBSET; IN_BALL] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1256 MP_TAC(ISPECL [`f:real^M->real^N`; `ball(x:real^M,e)`]
1257 HAS_DERIVATIVE_ZERO_CONSTANT) THEN
1258 REWRITE_TAC[IN_BALL; CONVEX_BALL] THEN
1259 ASM_MESON_TAC[HAS_DERIVATIVE_AT_WITHIN; DIST_SYM; DIST_REFL];
1260 MATCH_MP_TAC CONTINUOUS_CLOSED_IN_PREIMAGE_CONSTANT THEN
1261 MATCH_MP_TAC DIFFERENTIABLE_IMP_CONTINUOUS_ON THEN
1262 ASM_SIMP_TAC[DIFFERENTIABLE_ON_EQ_DIFFERENTIABLE_AT] THEN
1263 ASM_MESON_TAC[differentiable]]);;
1265 let HAS_DERIVATIVE_ZERO_CONNECTED_UNIQUE = prove
1266 (`!f s a c. open s /\ connected s /\ a IN s /\ f a = c /\
1267 (!x. x IN s ==> (f has_derivative (\h. vec 0)) (at x))
1268 ==> !x. x IN s ==> f x = c`,
1269 MESON_TAC[HAS_DERIVATIVE_ZERO_CONNECTED_CONSTANT]);;
1271 (* ------------------------------------------------------------------------- *)
1272 (* Differentiability of inverse function (most basic form). *)
1273 (* ------------------------------------------------------------------------- *)
1275 let HAS_DERIVATIVE_INVERSE_BASIC = prove
1276 (`!f:real^M->real^N g f' g' t y.
1277 (f has_derivative f') (at (g y)) /\ linear g' /\ (g' o f' = I) /\
1278 g continuous (at y) /\
1279 open t /\ y IN t /\ (!z. z IN t ==> (f(g(z)) = z))
1280 ==> (g has_derivative g') (at y)`,
1281 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN REPEAT STRIP_TAC THEN
1282 FIRST_ASSUM(X_CHOOSE_TAC `C:real` o MATCH_MP LINEAR_BOUNDED_POS) THEN
1284 `!e. &0 < e ==> ?d. &0 < d /\
1286 ==> norm((g:real^N->real^M)(z) - g(y) - g'(z - y))
1287 <= e * norm(g(z) - g(y))`
1289 [X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1290 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [HAS_DERIVATIVE_AT_ALT]) THEN
1291 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `e / C`)) THEN
1292 ASM_SIMP_TAC[REAL_LT_DIV] THEN
1293 DISCH_THEN(X_CHOOSE_THEN `d0:real`
1294 (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1295 DISCH_THEN(ASSUME_TAC o GEN `z:real^N` o SPEC `(g:real^N->real^M) z`) THEN
1296 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [continuous_at]) THEN
1297 DISCH_THEN(MP_TAC o SPEC `d0:real`) THEN ASM_REWRITE_TAC[dist] THEN
1298 DISCH_THEN(X_CHOOSE_THEN `d1:real` STRIP_ASSUME_TAC) THEN
1299 FIRST_X_ASSUM(MP_TAC o SPEC `y:real^N` o
1300 GEN_REWRITE_RULE I [open_def]) THEN
1301 ASM_REWRITE_TAC[dist] THEN
1302 DISCH_THEN(X_CHOOSE_THEN `d2:real` STRIP_ASSUME_TAC) THEN
1303 MP_TAC(SPECL [`d1:real`; `d2:real`] REAL_DOWN2) THEN
1304 ASM_REWRITE_TAC[] THEN
1305 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real` THEN STRIP_TAC THEN
1306 ASM_REWRITE_TAC[] THEN
1307 X_GEN_TAC `z:real^N` THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1308 EXISTS_TAC `C * (e / C) * norm((g:real^N->real^M) z - g y)` THEN
1311 ASM_SIMP_TAC[REAL_MUL_ASSOC; REAL_LE_RMUL; REAL_DIV_LMUL;
1312 REAL_EQ_IMP_LE; REAL_LT_IMP_NZ; NORM_POS_LE]] THEN
1313 MATCH_MP_TAC REAL_LE_TRANS THEN
1314 EXISTS_TAC `C * norm(f((g:real^N->real^M) z) - y - f'(g z - g y))` THEN
1315 CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[REAL_LT_TRANS; REAL_LE_LMUL_EQ]] THEN
1316 MATCH_MP_TAC REAL_LE_TRANS THEN
1318 `norm(g'(f((g:real^N->real^M) z) - y - f'(g z - g y)):real^M)` THEN
1319 ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[LINEAR_SUB] THEN
1320 GEN_REWRITE_TAC LAND_CONV [GSYM NORM_NEG] THEN
1321 REWRITE_TAC[VECTOR_ARITH
1322 `--(gz:real^N - gy - (z - y)) = z - y - (gz - gy)`] THEN
1323 ASM_MESON_TAC[REAL_LE_REFL; REAL_LT_TRANS];
1326 `?B d. &0 < B /\ &0 < d /\
1328 ==> norm((g:real^N->real^M)(z) - g(y)) <= B * norm(z - y)`
1329 STRIP_ASSUME_TAC THENL
1330 [EXISTS_TAC `&2 * C` THEN
1331 FIRST_X_ASSUM(MP_TAC o SPEC `&1 / &2`) THEN
1332 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1333 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real` THEN
1334 ASM_SIMP_TAC[REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
1335 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1336 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `z:real^N` THEN
1337 MATCH_MP_TAC MONO_IMP THEN REWRITE_TAC[] THEN
1338 MATCH_MP_TAC(REAL_ARITH
1339 `norm(dg) <= norm(dg') + norm(dg - dg') /\
1340 ((&2 * (&1 - h)) * norm(dg) = &1 * norm(dg)) /\
1341 norm(dg') <= c * norm(d)
1342 ==> norm(dg - dg') <= h * norm(dg)
1343 ==> norm(dg) <= (&2 * c) * norm(d)`) THEN
1344 CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_REWRITE_TAC[NORM_TRIANGLE_SUB];
1346 REWRITE_TAC[HAS_DERIVATIVE_AT_ALT] THEN ASM_REWRITE_TAC[] THEN
1347 X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1348 FIRST_X_ASSUM(MP_TAC o SPEC `e / B`) THEN
1349 ASM_SIMP_TAC[REAL_LT_DIV] THEN
1350 DISCH_THEN(X_CHOOSE_THEN `d':real` STRIP_ASSUME_TAC) THEN
1351 MP_TAC(SPECL [`d:real`; `d':real`] REAL_DOWN2) THEN ASM_REWRITE_TAC[] THEN
1352 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `k:real` THEN
1353 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `z:real^N` THEN
1354 DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1355 EXISTS_TAC `e / B * norm ((g:real^N->real^M) z - g y)` THEN
1356 CONJ_TAC THENL [ASM_MESON_TAC[REAL_LT_TRANS]; ALL_TAC] THEN
1357 ASM_SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_LE_LMUL_EQ] THEN
1358 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1359 ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ] THEN
1360 ASM_MESON_TAC[REAL_MUL_SYM; REAL_LT_TRANS]);;
1362 (* ------------------------------------------------------------------------- *)
1363 (* Simply rewrite that based on the domain point x. *)
1364 (* ------------------------------------------------------------------------- *)
1366 let HAS_DERIVATIVE_INVERSE_BASIC_X = prove
1367 (`!f:real^M->real^N g f' g' t x.
1368 (f has_derivative f') (at x) /\ linear g' /\ (g' o f' = I) /\
1369 g continuous (at (f(x))) /\ (g(f(x)) = x) /\
1370 open t /\ f(x) IN t /\ (!y. y IN t ==> (f(g(y)) = y))
1371 ==> (g has_derivative g') (at (f(x)))`,
1372 MESON_TAC[HAS_DERIVATIVE_INVERSE_BASIC]);;
1374 (* ------------------------------------------------------------------------- *)
1375 (* This is the version in Dieudonne', assuming continuity of f and g. *)
1376 (* ------------------------------------------------------------------------- *)
1378 let HAS_DERIVATIVE_INVERSE_DIEUDONNE = prove
1379 (`!f:real^M->real^N g s.
1380 open s /\ open (IMAGE f s) /\
1381 f continuous_on s /\ g continuous_on (IMAGE f s) /\
1382 (!x. x IN s ==> (g(f(x)) = x))
1383 ==> !f' g' x. x IN s /\ (f has_derivative f') (at x) /\
1384 linear g' /\ (g' o f' = I)
1385 ==> (g has_derivative g') (at (f(x)))`,
1386 REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_BASIC_X THEN
1387 EXISTS_TAC `f':real^M->real^N` THEN
1388 EXISTS_TAC `IMAGE (f:real^M->real^N) s` THEN
1389 ASM_MESON_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_AT; IN_IMAGE]);;
1391 (* ------------------------------------------------------------------------- *)
1392 (* Here's the simplest way of not assuming much about g. *)
1393 (* ------------------------------------------------------------------------- *)
1395 let HAS_DERIVATIVE_INVERSE = prove
1396 (`!f:real^M->real^N g f' g' s x.
1397 compact s /\ x IN s /\ f(x) IN interior(IMAGE f s) /\
1398 f continuous_on s /\ (!x. x IN s ==> (g(f(x)) = x)) /\
1399 (f has_derivative f') (at x) /\ linear g' /\ (g' o f' = I)
1400 ==> (g has_derivative g') (at (f(x)))`,
1401 REPEAT STRIP_TAC THEN
1402 MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_BASIC_X THEN
1403 EXISTS_TAC `f':real^M->real^N` THEN
1404 EXISTS_TAC `interior(IMAGE (f:real^M->real^N) s)` THEN
1405 ASM_MESON_TAC[CONTINUOUS_ON_INTERIOR; CONTINUOUS_ON_INVERSE;
1406 OPEN_INTERIOR; IN_IMAGE; INTERIOR_SUBSET; SUBSET]);;
1408 (* ------------------------------------------------------------------------- *)
1409 (* Proving surjectivity via Brouwer fixpoint theorem. *)
1410 (* ------------------------------------------------------------------------- *)
1412 let BROUWER_SURJECTIVE = prove
1413 (`!f:real^N->real^N s t.
1414 compact t /\ convex t /\ ~(t = {}) /\ f continuous_on t /\
1415 (!x y. x IN s /\ y IN t ==> x + (y - f(y)) IN t)
1416 ==> !x. x IN s ==> ?y. y IN t /\ (f(y) = x)`,
1417 REPEAT STRIP_TAC THEN
1418 ONCE_REWRITE_TAC[VECTOR_ARITH
1419 `((f:real^N->real^N)(y) = x) <=> (x + (y - f(y)) = y)`] THEN
1420 ASM_SIMP_TAC[CONTINUOUS_ON_ADD; CONTINUOUS_ON_CONST; CONTINUOUS_ON_SUB;
1421 BROUWER; SUBSET; FORALL_IN_IMAGE; CONTINUOUS_ON_ID]);;
1423 let BROUWER_SURJECTIVE_CBALL = prove
1424 (`!f:real^N->real^N s a e.
1426 f continuous_on cball(a,e) /\
1427 (!x y. x IN s /\ y IN cball(a,e) ==> x + (y - f(y)) IN cball(a,e))
1428 ==> !x. x IN s ==> ?y. y IN cball(a,e) /\ (f(y) = x)`,
1429 REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC BROUWER_SURJECTIVE THEN
1430 ASM_REWRITE_TAC[COMPACT_CBALL; CONVEX_CBALL] THEN
1431 ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT]);;
1433 (* ------------------------------------------------------------------------- *)
1434 (* See Sussmann: "Multidifferential calculus", Theorem 2.1.1 *)
1435 (* ------------------------------------------------------------------------- *)
1437 let SUSSMANN_OPEN_MAPPING = prove
1438 (`!f:real^M->real^N f' g' s x.
1439 open s /\ f continuous_on s /\
1440 x IN s /\ (f has_derivative f') (at x) /\ linear g' /\ (f' o g' = I)
1441 ==> !t. t SUBSET s /\ x IN interior(t)
1442 ==> f(x) IN interior(IMAGE f t)`,
1443 REWRITE_TAC[HAS_DERIVATIVE_AT_ALT] THEN
1444 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN REPEAT STRIP_TAC THEN
1445 MP_TAC(MATCH_MP LINEAR_BOUNDED_POS (ASSUME `linear(g':real^N->real^M)`)) THEN
1446 DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
1447 FIRST_X_ASSUM(MP_TAC o SPEC `&1 / (&2 * B)`) THEN
1448 ASM_SIMP_TAC[REAL_LT_MUL; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1449 DISCH_THEN(X_CHOOSE_THEN `e0:real` STRIP_ASSUME_TAC) THEN
1450 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_INTERIOR_CBALL]) THEN
1451 DISCH_THEN(X_CHOOSE_THEN `e1:real` STRIP_ASSUME_TAC) THEN
1452 MP_TAC(SPECL [`e0 / B`; `e1 / B`] REAL_DOWN2) THEN
1453 ASM_SIMP_TAC[REAL_LT_DIV] THEN
1454 DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
1456 [`\y. (f:real^M->real^N)(x + g'(y - f(x)))`;
1457 `cball((f:real^M->real^N) x,e / &2)`; `(f:real^M->real^N) x`; `e:real`]
1458 BROUWER_SURJECTIVE_CBALL) THEN
1459 REWRITE_TAC[] THEN ANTS_TAC THENL
1460 [ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
1461 [ONCE_REWRITE_TAC[GSYM o_DEF] THEN
1462 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
1463 [MATCH_MP_TAC CONTINUOUS_ON_ADD THEN
1464 REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
1465 ONCE_REWRITE_TAC[GSYM o_DEF] THEN
1466 MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1467 ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_CONST;
1468 CONTINUOUS_ON_ID; LINEAR_CONTINUOUS_ON];
1470 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
1471 EXISTS_TAC `cball(x:real^M,e1)` THEN CONJ_TAC THENL
1472 [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_TRANS]; ALL_TAC] THEN
1473 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN X_GEN_TAC `y:real^N` THEN
1474 REWRITE_TAC[IN_CBALL; dist] THEN
1475 REWRITE_TAC[VECTOR_ARITH `x - (x + y) = --y:real^N`] THEN
1476 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [NORM_SUB] THEN
1477 DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
1478 EXISTS_TAC `B * norm(y - (f:real^M->real^N) x)` THEN
1479 ASM_REWRITE_TAC[NORM_NEG] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1480 ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN
1481 ASM_MESON_TAC[REAL_LE_TRANS; REAL_LT_IMP_LE];
1483 MAP_EVERY X_GEN_TAC [`y:real^N`; `z:real^N`] THEN STRIP_TAC THEN
1484 FIRST_X_ASSUM(MP_TAC o SPEC `x + g'(z - (f:real^M->real^N) x)`) THEN
1485 ASM_REWRITE_TAC[VECTOR_ADD_SUB] THEN ANTS_TAC THENL
1486 [MATCH_MP_TAC REAL_LET_TRANS THEN
1487 EXISTS_TAC `B * norm(z - (f:real^M->real^N) x)` THEN
1488 ASM_REWRITE_TAC[NORM_NEG] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1489 ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ] THEN
1490 ASM_MESON_TAC[IN_CBALL; dist; NORM_SUB; REAL_LET_TRANS];
1492 REWRITE_TAC[VECTOR_ARITH `a - b - (c - b) = a - c:real^N`] THEN
1493 DISCH_TAC THEN REWRITE_TAC[IN_CBALL; dist] THEN
1494 ONCE_REWRITE_TAC[VECTOR_ARITH
1495 `f0 - (y + z - f1) = (f1 - z) + (f0 - y):real^N`] THEN
1496 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
1497 `norm(f(x + g'(z - (f:real^M->real^N) x)) - z) + norm(f x - y)` THEN
1498 REWRITE_TAC[NORM_TRIANGLE] THEN
1499 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
1500 `x <= a ==> y <= b - a ==> x + y <= b`)) THEN
1501 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `e / &2` THEN CONJ_TAC THENL
1502 [ASM_MESON_TAC[IN_CBALL; dist]; ALL_TAC] THEN
1503 REWRITE_TAC[REAL_ARITH `e / &2 <= e - x <=> x <= e / &2`] THEN
1504 REWRITE_TAC[real_div; REAL_INV_MUL; REAL_MUL_ASSOC] THEN
1505 CONV_TAC REAL_RAT_REDUCE_CONV THEN
1506 SIMP_TAC[REAL_ARITH `(&1 / &2 * b) * x <= e * &1 / &2 <=> x * b <= e`] THEN
1507 ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ] THEN
1508 MATCH_MP_TAC REAL_LE_TRANS THEN
1509 EXISTS_TAC `B * norm(z - (f:real^M->real^N) x)` THEN
1510 ASM_REWRITE_TAC[] THEN
1511 ASM_MESON_TAC[REAL_LE_LMUL_EQ; REAL_MUL_SYM; IN_CBALL; dist; DIST_SYM];
1513 REWRITE_TAC[IN_INTERIOR] THEN
1514 DISCH_THEN(fun th -> EXISTS_TAC `e / &2` THEN MP_TAC th) THEN
1515 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH; SUBSET] THEN
1516 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `y:real^N` THEN
1517 MATCH_MP_TAC MONO_IMP THEN
1518 REWRITE_TAC[REWRITE_RULE[SUBSET] BALL_SUBSET_CBALL] THEN
1519 DISCH_THEN(X_CHOOSE_THEN `z:real^N` (STRIP_ASSUME_TAC o GSYM)) THEN
1520 ASM_REWRITE_TAC[IN_IMAGE] THEN
1521 EXISTS_TAC `x + g'(z - (f:real^M->real^N) x)` THEN REWRITE_TAC[] THEN
1522 FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[SUBSET]) THEN
1523 REWRITE_TAC[IN_CBALL; dist; VECTOR_ARITH `x - (x + y) = --y:real^N`] THEN
1524 MATCH_MP_TAC REAL_LE_TRANS THEN
1525 EXISTS_TAC `B * norm(z - (f:real^M->real^N) x)` THEN
1526 ASM_REWRITE_TAC[NORM_NEG] THEN
1527 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1528 ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN
1529 ASM_MESON_TAC[IN_CBALL; dist; NORM_SUB; REAL_LT_IMP_LE; REAL_LE_TRANS]);;
1531 (* ------------------------------------------------------------------------- *)
1532 (* Hence the following eccentric variant of the inverse function theorem. *)
1533 (* This has no continuity assumptions, but we do need the inverse function. *)
1534 (* We could put f' o g = I but this happens to fit with the minimal linear *)
1535 (* algebra theory I've set up so far. *)
1536 (* ------------------------------------------------------------------------- *)
1538 let HAS_DERIVATIVE_INVERSE_STRONG = prove
1539 (`!f:real^N->real^N g f' g' s x.
1540 open s /\ x IN s /\ f continuous_on s /\
1541 (!x. x IN s ==> (g(f(x)) = x)) /\
1542 (f has_derivative f') (at x) /\ (f' o g' = I)
1543 ==> (g has_derivative g') (at (f(x)))`,
1544 REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_BASIC_X THEN
1545 SUBGOAL_THEN `linear (g':real^N->real^N) /\ (g' o f' = I)`
1546 STRIP_ASSUME_TAC THENL
1547 [ASM_MESON_TAC[has_derivative; RIGHT_INVERSE_LINEAR; LINEAR_INVERSE_LEFT];
1549 EXISTS_TAC `f':real^N->real^N` THEN
1550 EXISTS_TAC `interior (IMAGE (f:real^N->real^N) s)` THEN
1551 ASM_REWRITE_TAC[] THEN REPEAT CONJ_TAC THENL
1554 REWRITE_TAC[OPEN_INTERIOR];
1555 ASM_MESON_TAC[INTERIOR_OPEN; SUSSMANN_OPEN_MAPPING; LINEAR_INVERSE_LEFT;
1556 SUBSET_REFL; has_derivative];
1557 ASM_MESON_TAC[IN_IMAGE; SUBSET; INTERIOR_SUBSET]] THEN
1558 REWRITE_TAC[continuous_at] THEN
1559 X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1561 `!t. t SUBSET s /\ x IN interior(t)
1562 ==> (f:real^N->real^N)(x) IN interior(IMAGE f t)`
1564 [ASM_MESON_TAC[SUSSMANN_OPEN_MAPPING; LINEAR_INVERSE_LEFT; has_derivative];
1566 DISCH_THEN(MP_TAC o SPEC `ball(x:real^N,e) INTER s`) THEN ANTS_TAC THENL
1567 [ASM_SIMP_TAC[IN_INTER; OPEN_BALL; INTERIOR_OPEN; OPEN_INTER;
1568 INTER_SUBSET; CENTRE_IN_BALL];
1570 REWRITE_TAC[IN_INTERIOR] THEN
1571 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real` THEN
1572 ASM_CASES_TAC `&0 < d` THEN ASM_REWRITE_TAC[] THEN
1573 REWRITE_TAC[SUBSET; IN_BALL; IN_IMAGE; IN_INTER] THEN
1574 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `y:real^N` THEN
1575 REWRITE_TAC[DIST_SYM] THEN MATCH_MP_TAC MONO_IMP THEN
1576 ASM_MESON_TAC[DIST_SYM]);;
1578 (* ------------------------------------------------------------------------- *)
1579 (* A rewrite based on the other domain. *)
1580 (* ------------------------------------------------------------------------- *)
1582 let HAS_DERIVATIVE_INVERSE_STRONG_X = prove
1583 (`!f:real^N->real^N g f' g' s y.
1584 open s /\ (g y) IN s /\ f continuous_on s /\
1585 (!x. x IN s ==> (g(f(x)) = x)) /\
1586 (f has_derivative f') (at (g y)) /\ (f' o g' = I) /\
1588 ==> (g has_derivative g') (at y)`,
1589 REPEAT STRIP_TAC THEN
1590 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [SYM th]) THEN
1591 MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_STRONG THEN
1592 MAP_EVERY EXISTS_TAC [`f':real^N->real^N`; `s:real^N->bool`] THEN
1593 ASM_REWRITE_TAC[]);;
1595 (* ------------------------------------------------------------------------- *)
1597 (* ------------------------------------------------------------------------- *)
1599 let HAS_DERIVATIVE_INVERSE_ON = prove
1600 (`!f:real^N->real^N s.
1602 (!x. x IN s ==> (f has_derivative f'(x)) (at x) /\ (g(f(x)) = x) /\
1603 (f'(x) o g'(x) = I))
1604 ==> !x. x IN s ==> (g has_derivative g'(x)) (at (f(x)))`,
1605 REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_STRONG THEN
1606 EXISTS_TAC `(f':real^N->real^N->real^N) x` THEN
1607 EXISTS_TAC `s:real^N->bool` THEN
1608 ASM_MESON_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_AT;
1609 DIFFERENTIABLE_IMP_CONTINUOUS_AT; differentiable]);;
1611 (* ------------------------------------------------------------------------- *)
1612 (* Invertible derivative continous at a point implies local injectivity. *)
1613 (* It's only for this we need continuity of the derivative, except of course *)
1614 (* if we want the fact that the inverse derivative is also continuous. So if *)
1615 (* we know for some other reason that the inverse function exists, it's OK. *)
1616 (* ------------------------------------------------------------------------- *)
1618 let HAS_DERIVATIVE_LOCALLY_INJECTIVE = prove
1619 (`!f:real^M->real^N f' g' s a.
1620 a IN s /\ open s /\ linear g' /\ (g' o f'(a) = I) /\
1621 (!x. x IN s ==> (f has_derivative f'(x)) (at x)) /\
1624 !x. dist(a,x) < d ==> onorm(\v. f'(x) v - f'(a) v) < e)
1625 ==> ?t. a IN t /\ open t /\
1626 !x x'. x IN t /\ x' IN t /\ (f x' = f x) ==> (x' = x)`,
1627 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN REPEAT STRIP_TAC THEN
1628 SUBGOAL_THEN `&0 < onorm(g':real^N->real^M)` ASSUME_TAC THENL
1629 [ASM_SIMP_TAC[ONORM_POS_LT] THEN ASM_MESON_TAC[VEC_EQ; ARITH_EQ];
1631 ABBREV_TAC `k = &1 / onorm(g':real^N->real^M) / &2` THEN
1633 `?d. &0 < d /\ ball(a,d) SUBSET s /\
1635 ==> onorm(\v. (f':real^M->real^M->real^N)(x) v - f'(a) v) < k`
1636 STRIP_ASSUME_TAC THENL
1637 [FIRST_X_ASSUM(MP_TAC o SPEC `k:real`) THEN EXPAND_TAC "k" THEN
1638 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1639 DISCH_THEN(X_CHOOSE_THEN `d1:real` STRIP_ASSUME_TAC) THEN
1640 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [OPEN_CONTAINS_BALL]) THEN
1641 DISCH_THEN(MP_TAC o SPEC `a:real^M`) THEN ASM_REWRITE_TAC[] THEN
1642 REWRITE_TAC[SUBSET; IN_BALL] THEN DISCH_THEN(X_CHOOSE_TAC `d2:real`) THEN
1643 EXISTS_TAC `min d1 d2` THEN ASM_REWRITE_TAC[REAL_LT_MIN; IN_BALL] THEN
1644 ASM_MESON_TAC[REAL_LT_TRANS];
1646 EXISTS_TAC `ball(a:real^M,d)` THEN
1647 ASM_SIMP_TAC[OPEN_BALL; CENTRE_IN_BALL] THEN
1648 MAP_EVERY X_GEN_TAC [`x:real^M`; `x':real^M`] THEN STRIP_TAC THEN
1649 ABBREV_TAC `ph = \w. w - g'(f(w) - (f:real^M->real^N)(x))` THEN
1650 SUBGOAL_THEN `norm((ph:real^M->real^M) x' - ph x) <= norm(x' - x) / &2`
1653 EXPAND_TAC "ph" THEN ASM_REWRITE_TAC[VECTOR_SUB_REFL] THEN
1654 FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP LINEAR_0 th]) THEN
1655 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
1656 REWRITE_TAC[VECTOR_SUB_RZERO; GSYM NORM_LE_0] THEN REAL_ARITH_TAC] THEN
1658 `!u v:real^M. u IN ball(a,d) /\ v IN ball(a,d)
1659 ==> norm(ph u - ph v :real^M) <= norm(u - v) / &2`
1660 (fun th -> ASM_SIMP_TAC[th]) THEN
1661 REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN
1662 MATCH_MP_TAC DIFFERENTIABLE_BOUND THEN
1663 REWRITE_TAC[CONVEX_BALL; OPEN_BALL] THEN
1664 EXISTS_TAC `\x v. v - g'((f':real^M->real^M->real^N) x v)` THEN
1665 CONJ_TAC THEN X_GEN_TAC `u:real^M` THEN DISCH_TAC THEN REWRITE_TAC[] THENL
1666 [EXPAND_TAC "ph" THEN
1667 MATCH_MP_TAC HAS_DERIVATIVE_SUB THEN REWRITE_TAC[HAS_DERIVATIVE_ID] THEN
1668 FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP LINEAR_SUB th]) THEN
1669 GEN_REWRITE_TAC (RATOR_CONV o BINDER_CONV) [GSYM VECTOR_SUB_RZERO] THEN
1670 MATCH_MP_TAC HAS_DERIVATIVE_SUB THEN REWRITE_TAC[HAS_DERIVATIVE_CONST] THEN
1671 ONCE_REWRITE_TAC[GSYM o_DEF] THEN MATCH_MP_TAC DIFF_CHAIN_WITHIN THEN
1672 ONCE_REWRITE_TAC[ETA_AX] THEN
1673 ASM_MESON_TAC[HAS_DERIVATIVE_LINEAR; SUBSET; HAS_DERIVATIVE_AT_WITHIN];
1676 `(\w. w - g'((f':real^M->real^M->real^N) u w)) =
1677 g' o (\w. f' a w - f' u w)`
1679 [REWRITE_TAC[FUN_EQ_THM; o_THM] THEN ASM_MESON_TAC[LINEAR_SUB];
1681 SUBGOAL_THEN `linear(\w. f' a w - (f':real^M->real^M->real^N) u w)`
1683 [MATCH_MP_TAC LINEAR_COMPOSE_SUB THEN ONCE_REWRITE_TAC[ETA_AX] THEN
1684 ASM_MESON_TAC[has_derivative; SUBSET; CENTRE_IN_BALL];
1686 MATCH_MP_TAC REAL_LE_TRANS THEN
1688 `onorm(g':real^N->real^M) *
1689 onorm(\w. f' a w - (f':real^M->real^M->real^N) u w)` THEN
1690 ASM_SIMP_TAC[ONORM_COMPOSE] THEN
1691 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_SIMP_TAC[GSYM REAL_LE_RDIV_EQ] THEN
1692 REWRITE_TAC[real_div; REAL_ARITH `inv(&2) * x = (&1 * x) * inv(&2)`] THEN
1693 ASM_REWRITE_TAC[GSYM real_div] THEN
1694 SUBGOAL_THEN `onorm(\w. (f':real^M->real^M->real^N) a w - f' u w) =
1695 onorm(\w. f' u w - f' a w)`
1696 (fun th -> ASM_SIMP_TAC[th; REAL_LT_IMP_LE]) THEN
1697 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM VECTOR_NEG_SUB] THEN
1698 MATCH_MP_TAC ONORM_NEG THEN ONCE_REWRITE_TAC[GSYM VECTOR_NEG_SUB] THEN
1699 ASM_SIMP_TAC[LINEAR_COMPOSE_NEG]);;
1701 (* ------------------------------------------------------------------------- *)
1702 (* More conventional "C1" version of inverse function theorem. *)
1703 (* ------------------------------------------------------------------------- *)
1705 let INVERSE_FUNCTION_C1 = prove
1706 (`!f:real^N->real^N f' a s.
1708 (!x. x IN s ==> (f has_derivative f'(x)) (at x)) /\
1711 !x. dist(a,x) < d ==> onorm(\v. f'(x) v - f'(a) v) < e) /\
1712 ~(det(matrix(f' a)) = &0)
1713 ==> ?t u g. open t /\ a IN t /\ open u /\ f(a) IN u /\
1714 (!x. x IN t ==> g(f(x)) = x) /\
1715 (!y. y IN u ==> f(g(y)) = y) /\
1716 g differentiable_on u`,
1717 REPEAT STRIP_TAC THEN
1719 `(\x:real^N. lift(det(matrix(f' x:real^N->real^N)))) continuous at a`
1721 [MATCH_MP_TAC CONTINUOUS_LIFT_DET THEN
1722 REPEAT STRIP_TAC THEN REWRITE_TAC[continuous_at; DIST_LIFT] THEN
1723 X_GEN_TAC `e:real` THEN STRIP_TAC THEN
1724 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [open_def]) THEN
1725 DISCH_THEN(MP_TAC o SPEC `a:real^N`) THEN ASM_REWRITE_TAC[] THEN
1726 DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
1727 FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
1728 DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
1729 EXISTS_TAC `min d k:real` THEN ASM_REWRITE_TAC[REAL_LT_MIN] THEN
1730 X_GEN_TAC `x:real^N` THEN STRIP_TAC THEN
1731 FIRST_X_ASSUM(MP_TAC o SPEC `x:real^N`) THEN
1732 ANTS_TAC THENL [ASM_MESON_TAC[DIST_SYM]; ALL_TAC] THEN
1733 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] REAL_LET_TRANS) THEN
1734 REWRITE_TAC[GSYM MATRIX_SUB_COMPONENT] THEN
1735 W(MP_TAC o PART_MATCH lhand MATRIX_COMPONENT_LE_ONORM o lhand o snd) THEN
1736 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ_ALT] REAL_LE_TRANS) THEN
1737 MATCH_MP_TAC REAL_EQ_IMP_LE THEN AP_TERM_TAC THEN ABS_TAC THEN
1738 REWRITE_TAC[MATRIX_VECTOR_MUL_SUB_RDISTRIB] THEN BINOP_TAC THEN
1739 MATCH_MP_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM] MATRIX_WORKS) THEN
1740 RULE_ASSUM_TAC(REWRITE_RULE[has_derivative]) THEN
1744 `?u. a IN u /\ open u /\
1745 !x:real^N. x IN u ==> ~(det(matrix(f' x:real^N->real^N)) = &0)`
1746 STRIP_ASSUME_TAC THENL
1747 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [continuous_at]) THEN
1748 DISCH_THEN(MP_TAC o SPEC
1749 `abs(det(matrix((f':real^N->real^N->real^N) a)))`) THEN
1750 ASM_REWRITE_TAC[REAL_ARITH `&0 < abs x <=> ~(x = &0)`] THEN
1751 REWRITE_TAC[DIST_LIFT; LEFT_IMP_EXISTS_THM] THEN
1752 X_GEN_TAC `d:real` THEN STRIP_TAC THEN
1753 EXISTS_TAC `ball(a:real^N,d)` THEN
1754 ASM_REWRITE_TAC[DIST_REFL; OPEN_BALL; IN_BALL] THEN
1755 ASM_MESON_TAC[DIST_SYM; REAL_ARITH `abs(x - y) < abs y ==> ~(x = &0)`];
1757 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM INVERTIBLE_DET_NZ]) THEN
1758 SUBGOAL_THEN `!x. x IN s ==> linear((f':real^N->real^N->real^N) x)`
1759 ASSUME_TAC THENL [ASM_MESON_TAC[has_derivative]; ALL_TAC] THEN
1760 ASM_SIMP_TAC[MATRIX_INVERTIBLE] THEN
1761 DISCH_THEN(X_CHOOSE_THEN `g'a:real^N->real^N` STRIP_ASSUME_TAC) THEN
1762 MP_TAC(ISPECL [`f:real^N->real^N`; `f':real^N->real^N->real^N`;
1763 `g'a:real^N->real^N`; `s:real^N->bool`; `a:real^N`]
1764 HAS_DERIVATIVE_LOCALLY_INJECTIVE) THEN
1765 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN
1766 X_GEN_TAC `t:real^N->bool` THEN STRIP_TAC THEN
1767 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
1768 MP_TAC(ISPECL [`f:real^N->real^N`; `t:real^N->bool`]
1769 INJECTIVE_ON_LEFT_INVERSE) THEN
1770 MATCH_MP_TAC(TAUT `p /\ (q ==> r) ==> (p <=> q) ==> r`) THEN
1771 CONJ_TAC THENL [ASM_MESON_TAC[]; MATCH_MP_TAC MONO_EXISTS] THEN
1772 X_GEN_TAC `g:real^N->real^N` THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1775 ==> ?g. linear g /\ (f':real^N->real^N->real^N) x o g = I /\
1778 [ASM_SIMP_TAC[IN_INTER; GSYM MATRIX_INVERTIBLE; INVERTIBLE_DET_NZ];
1779 GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [RIGHT_IMP_EXISTS_THM] THEN
1780 REWRITE_TAC[SKOLEM_THM; LEFT_IMP_EXISTS_THM]] THEN
1781 X_GEN_TAC `g':real^N->real^N->real^N` THEN STRIP_TAC THEN
1782 EXISTS_TAC `interior (IMAGE (f:real^N->real^N) (s INTER t INTER u))` THEN
1783 SIMP_TAC[OPEN_INTERIOR; DIFFERENTIABLE_ON_EQ_DIFFERENTIABLE_AT] THEN
1785 [MP_TAC(ISPECL [`f:real^N->real^N`; `(f':real^N->real^N->real^N) a`;
1786 `g'a:real^N->real^N`; `s INTER t INTER u:real^N->bool`;
1788 SUSSMANN_OPEN_MAPPING) THEN
1789 ASM_SIMP_TAC[OPEN_INTER; IN_INTER] THEN ANTS_TAC THENL
1790 [ASM_MESON_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_AT;
1791 CONTINUOUS_ON_EQ_CONTINUOUS_AT; OPEN_INTER;
1792 differentiable; SUBSET; IN_INTER];
1793 DISCH_THEN MATCH_MP_TAC THEN CONJ_TAC THENL [SET_TAC[]; ALL_TAC] THEN
1794 ASM_SIMP_TAC[INTERIOR_OPEN; OPEN_INTER; IN_INTER]];
1796 ONCE_REWRITE_TAC[MESON[SUBSET; INTERIOR_SUBSET]
1797 `(!x. x IN interior s ==> P x) <=>
1798 (!x. x IN s ==> x IN interior s ==> P x)`] THEN
1799 REWRITE_TAC[FORALL_IN_IMAGE] THEN
1800 CONJ_TAC THENL [ASM_MESON_TAC[IN_INTER]; ALL_TAC] THEN
1801 X_GEN_TAC `x:real^N` THEN REWRITE_TAC[IN_INTER] THEN REPEAT STRIP_TAC THEN
1802 REWRITE_TAC[differentiable] THEN
1803 EXISTS_TAC `(g':real^N->real^N->real^N) x` THEN
1804 MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_STRONG THEN
1805 EXISTS_TAC `(f':real^N->real^N->real^N) x` THEN
1806 EXISTS_TAC `s INTER t INTER u:real^N->bool` THEN
1807 RULE_ASSUM_TAC(REWRITE_RULE[IN_INTER]) THEN
1808 ASM_SIMP_TAC[IN_INTER; OPEN_INTER] THEN
1809 ASM_MESON_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_AT;
1810 CONTINUOUS_ON_EQ_CONTINUOUS_AT; OPEN_INTER;
1811 differentiable; SUBSET; IN_INTER]);;
1813 (* ------------------------------------------------------------------------- *)
1814 (* Uniformly convergent sequence of derivatives. *)
1815 (* ------------------------------------------------------------------------- *)
1817 let HAS_DERIVATIVE_SEQUENCE_LIPSCHITZ = prove
1818 (`!s f:num->real^M->real^N f' g'.
1820 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\
1822 ==> ?N. !n x h. n >= N /\ x IN s
1823 ==> norm(f' n x h - g' x h) <= e * norm(h))
1825 ==> ?N. !m n x y. m >= N /\ n >= N /\ x IN s /\ y IN s
1826 ==> norm((f m x - f n x) - (f m y - f n y))
1827 <= e * norm(x - y)`,
1828 REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
1829 ASM_REWRITE_TAC[REAL_HALF] THEN MATCH_MP_TAC MONO_EXISTS THEN
1830 X_GEN_TAC `N:num` THEN DISCH_TAC THEN
1831 MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN
1832 ASM_CASES_TAC `m:num >= N` THEN ASM_REWRITE_TAC[] THEN
1833 ASM_CASES_TAC `n:num >= N` THEN ASM_REWRITE_TAC[] THEN
1834 MATCH_MP_TAC DIFFERENTIABLE_BOUND THEN
1835 EXISTS_TAC `\x h. (f':num->real^M->real^M->real^N) m x h - f' n x h` THEN
1836 ASM_SIMP_TAC[HAS_DERIVATIVE_SUB; ETA_AX] THEN
1837 X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN
1839 `!h. norm((f':num->real^M->real^M->real^N) m x h - f' n x h) <= e * norm(h)`
1840 MP_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[HAS_DERIVATIVE_WITHIN_ALT]) THEN
1841 ASM_SIMP_TAC[ONORM; LINEAR_COMPOSE_SUB; ETA_AX] THEN
1842 X_GEN_TAC `h:real^M` THEN SUBST1_TAC(VECTOR_ARITH
1843 `(f':num->real^M->real^M->real^N) m x h - f' n x h =
1844 (f' m x h - g' x h) + --(f' n x h - g' x h)`) THEN
1845 MATCH_MP_TAC NORM_TRIANGLE_LE THEN
1846 ASM_SIMP_TAC[NORM_NEG; REAL_ARITH
1847 `a <= e / &2 * h /\ b <= e / &2 * h ==> a + b <= e * h`]);;
1849 let HAS_DERIVATIVE_SEQUENCE = prove
1850 (`!s f:num->real^M->real^N f' g'.
1852 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\
1854 ==> ?N. !n x h. n >= N /\ x IN s
1855 ==> norm(f' n x h - g' x h) <= e * norm(h)) /\
1856 (?x l. x IN s /\ ((\n. f n x) --> l) sequentially)
1858 ==> ((\n. f n x) --> g x) sequentially /\
1859 (g has_derivative g'(x)) (at x within s)`,
1861 REPLICATE_TAC 2 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
1862 DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "O") MP_TAC) THEN
1863 DISCH_THEN(X_CHOOSE_THEN `x0:real^M` STRIP_ASSUME_TAC) THEN
1866 ==> ?N. !m n x y. m >= N /\ n >= N /\ x IN s /\ y IN s
1867 ==> norm(((f:num->real^M->real^N) m x - f n x) -
1870 [MATCH_MP_TAC HAS_DERIVATIVE_SEQUENCE_LIPSCHITZ THEN
1871 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[]] THEN
1873 `?g:real^M->real^N. !x. x IN s ==> ((\n. f n x) --> g x) sequentially`
1875 [REWRITE_TAC[GSYM SKOLEM_THM; RIGHT_EXISTS_IMP_THM] THEN
1876 X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN
1877 GEN_REWRITE_TAC I [CONVERGENT_EQ_CAUCHY] THEN
1878 FIRST_X_ASSUM(MP_TAC o MATCH_MP CONVERGENT_IMP_CAUCHY) THEN
1879 REWRITE_TAC[cauchy; dist] THEN DISCH_THEN(LABEL_TAC "B") THEN
1880 X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1881 ASM_CASES_TAC `x:real^M = x0` THEN ASM_SIMP_TAC[] THEN
1882 REMOVE_THEN "B" (MP_TAC o SPEC `e / &2`) THEN
1883 ASM_REWRITE_TAC[REAL_HALF] THEN
1884 DISCH_THEN(X_CHOOSE_THEN `N1:num` STRIP_ASSUME_TAC) THEN
1885 REMOVE_THEN "A" (MP_TAC o SPEC `e / &2 / norm(x - x0:real^M)`) THEN
1886 ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; REAL_HALF; VECTOR_SUB_EQ] THEN
1887 DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN
1888 EXISTS_TAC `N1 + N2:num` THEN REPEAT GEN_TAC THEN
1889 DISCH_THEN(CONJUNCTS_THEN (STRIP_ASSUME_TAC o MATCH_MP
1890 (ARITH_RULE `m >= N1 + N2:num ==> m >= N1 /\ m >= N2`))) THEN
1891 SUBST1_TAC(VECTOR_ARITH
1892 `(f:num->real^M->real^N) m x - f n x =
1893 (f m x - f n x - (f m x0 - f n x0)) + (f m x0 - f n x0)`) THEN
1894 MATCH_MP_TAC NORM_TRIANGLE_LT THEN
1895 FIRST_X_ASSUM(MP_TAC o SPECL
1896 [`m:num`; `n:num`; `x:real^M`; `x0:real^M`]) THEN
1897 FIRST_X_ASSUM(MP_TAC o SPECL [`m:num`; `n:num`]) THEN
1898 ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN REAL_ARITH_TAC;
1900 MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN SIMP_TAC[] THEN
1901 DISCH_THEN(LABEL_TAC "B") THEN X_GEN_TAC `x:real^M` THEN DISCH_TAC THEN
1902 REWRITE_TAC[HAS_DERIVATIVE_WITHIN_ALT] THEN
1905 ==> ?N. !n x y. n >= N /\ x IN s /\ y IN s
1906 ==> norm(((f:num->real^M->real^N) n x - f n y) -
1909 [X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1910 REMOVE_THEN "A" (MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
1911 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
1912 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `n:num` THEN
1913 DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`u:real^M`; `v:real^M`] THEN
1914 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN `m:num` o SPECL
1915 [`m:num`; `u:real^M`; `v:real^M`]) THEN
1916 DISCH_TAC THEN MATCH_MP_TAC(ISPEC `sequentially` LIM_NORM_UBOUND) THEN
1918 `\m. ((f:num->real^M->real^N) n u - f n v) - (f m u - f m v)` THEN
1919 REWRITE_TAC[eventually; TRIVIAL_LIMIT_SEQUENTIALLY] THEN
1920 ASM_SIMP_TAC[SEQUENTIALLY; LIM_SUB; LIM_CONST] THEN EXISTS_TAC `N:num` THEN
1921 ONCE_REWRITE_TAC[VECTOR_ARITH
1922 `(x - y) - (u - v) = (x - u) - (y - v):real^N`] THEN
1923 ASM_MESON_TAC[GE_REFL]] THEN
1926 `!u. ((\n. (f':num->real^M->real^M->real^N) n x u) --> g' x u) sequentially`
1927 [REWRITE_TAC[LIM_SEQUENTIALLY; dist] THEN REPEAT STRIP_TAC THEN
1928 ASM_CASES_TAC `u = vec 0:real^M` THENL
1929 [REMOVE_THEN "O" (MP_TAC o SPEC `e:real`);
1930 REMOVE_THEN "O" (MP_TAC o SPEC `e / &2 / norm(u:real^M)`)] THEN
1931 ASM_SIMP_TAC[NORM_POS_LT; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1932 MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
1933 MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
1934 DISCH_THEN(MP_TAC o SPECL [`x:real^M`; `u:real^M`]) THEN
1935 DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
1936 ASM_SIMP_TAC[GE; NORM_0; REAL_MUL_RZERO; NORM_LE_0] THEN
1937 ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0] THEN
1938 UNDISCH_TAC `&0 < e` THEN REAL_ARITH_TAC] THEN
1939 REWRITE_TAC[linear] THEN ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN
1941 [MAP_EVERY X_GEN_TAC [`u:real^M`; `v:real^M`];
1942 MAP_EVERY X_GEN_TAC [`c:real`; `u:real^M`]] THEN
1943 MATCH_MP_TAC(ISPEC `sequentially` LIM_UNIQUE) THENL
1945 `\n. (f':num->real^M->real^M->real^N) n x (u + v) -
1946 (f' n x u + f' n x v)`;
1948 `\n. (f':num->real^M->real^M->real^N) n x (c % u) -
1950 ASM_SIMP_TAC[TRIVIAL_LIMIT_SEQUENTIALLY; LIM_SUB; LIM_ADD; LIM_CMUL] THEN
1951 RULE_ASSUM_TAC(REWRITE_RULE[has_derivative_within; linear]) THEN
1952 ASM_SIMP_TAC[VECTOR_SUB_REFL; LIM_CONST];
1954 X_GEN_TAC `e:real` THEN DISCH_TAC THEN
1955 MAP_EVERY (fun s -> REMOVE_THEN s (MP_TAC o SPEC `e / &3`)) ["C"; "O"] THEN
1956 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1957 DISCH_THEN(X_CHOOSE_THEN `N1:num` (LABEL_TAC "C")) THEN
1958 DISCH_THEN(X_CHOOSE_THEN `N2:num` (LABEL_TAC "A")) THEN
1959 REMOVE_THEN "C" (MP_TAC o GEN `y:real^M` o
1960 SPECL [`N1 + N2:num`; `x:real^M`; `y - x:real^M`]) THEN
1961 REMOVE_THEN "A" (MP_TAC o GEN `y:real^M` o
1962 SPECL [`N1 + N2:num`; `y:real^M`; `x:real^M`]) THEN
1963 FIRST_X_ASSUM(MP_TAC o SPECL [`N1 + N2:num`; `x:real^M`]) THEN
1964 ASM_REWRITE_TAC[ARITH_RULE `m + n >= m:num /\ m + n >= n`] THEN
1965 REWRITE_TAC[HAS_DERIVATIVE_WITHIN_ALT] THEN
1966 DISCH_THEN(MP_TAC o SPEC `e / &3` o CONJUNCT2) THEN
1967 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
1968 DISCH_THEN(X_CHOOSE_THEN `d1:real` STRIP_ASSUME_TAC) THEN
1969 DISCH_THEN(LABEL_TAC "D1") THEN DISCH_THEN(LABEL_TAC "D2") THEN
1970 EXISTS_TAC `d1:real` THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `y:real^M` THEN
1971 DISCH_TAC THEN REMOVE_THEN "D2" (MP_TAC o SPEC `y:real^M`) THEN
1972 REMOVE_THEN "D1" (MP_TAC o SPEC `y:real^M`) THEN ANTS_TAC THENL
1973 [ASM_MESON_TAC[REAL_LT_TRANS; NORM_SUB]; ALL_TAC] THEN
1974 FIRST_X_ASSUM(MP_TAC o SPEC `y:real^M`) THEN ANTS_TAC THENL
1975 [ASM_MESON_TAC[REAL_LT_TRANS; NORM_SUB]; ALL_TAC] THEN
1976 MATCH_MP_TAC(REAL_ARITH
1978 ==> a <= e / &3 * n ==> b <= e / &3 * n ==> c <= e / &3 * n
1979 ==> d <= e * n`) THEN
1980 GEN_REWRITE_TAC (funpow 2 RAND_CONV o LAND_CONV) [NORM_SUB] THEN
1981 MATCH_MP_TAC(REAL_ARITH
1982 `(norm(x + y + z) = norm(a)) /\
1983 norm(x + y + z) <= norm(x) + norm(y + z) /\
1984 norm(y + z) <= norm(y) + norm(z)
1985 ==> norm(a) <= norm(x) + norm(y) + norm(z)`) THEN
1986 REWRITE_TAC[NORM_TRIANGLE] THEN AP_TERM_TAC THEN VECTOR_ARITH_TAC);;
1988 (* ------------------------------------------------------------------------- *)
1989 (* Can choose to line up antiderivatives if we want. *)
1990 (* ------------------------------------------------------------------------- *)
1992 let HAS_ANTIDERIVATIVE_SEQUENCE = prove
1993 (`!s f:num->real^M->real^N f' g'.
1995 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\
1997 ==> ?N. !n x h. n >= N /\ x IN s
1998 ==> norm(f' n x h - g' x h) <= e * norm(h))
1999 ==> ?g. !x. x IN s ==> (g has_derivative g'(x)) (at x within s)`,
2000 REPEAT STRIP_TAC THEN ASM_CASES_TAC `(s:real^M->bool) = {}` THEN
2001 ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
2002 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
2003 DISCH_THEN(X_CHOOSE_TAC `a:real^M`) THEN
2006 `\n x. (f:num->real^M->real^N) n x + (f 0 a - f n a)`;
2007 `f':num->real^M->real^M->real^N`;
2008 `g':real^M->real^M->real^N`]
2009 HAS_DERIVATIVE_SEQUENCE) THEN
2010 ASM_REWRITE_TAC[] THEN ANTS_TAC THENL [ALL_TAC; MESON_TAC[]] THEN
2012 [REPEAT STRIP_TAC THEN
2013 SUBGOAL_THEN `(f':num->real^M->real^M->real^N) n x =
2014 \h. f' n x h + vec 0`
2015 SUBST1_TAC THENL [SIMP_TAC[FUN_EQ_THM] THEN VECTOR_ARITH_TAC; ALL_TAC] THEN
2016 MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN
2017 ASM_SIMP_TAC[HAS_DERIVATIVE_CONST; ETA_AX];
2018 MAP_EVERY EXISTS_TAC [`a:real^M`; `f 0 (a:real^M) :real^N`] THEN
2019 ASM_REWRITE_TAC[VECTOR_ARITH `a + b - a = b:real^N`; LIM_CONST]]);;
2021 let HAS_ANTIDERIVATIVE_LIMIT = prove
2022 (`!s g':real^M->real^M->real^N.
2025 ==> ?f f'. !x. x IN s
2026 ==> (f has_derivative (f' x)) (at x within s) /\
2027 (!h. norm(f' x h - g' x h) <= e * norm(h)))
2028 ==> ?g. !x. x IN s ==> (g has_derivative g'(x)) (at x within s)`,
2029 REPEAT STRIP_TAC THEN
2030 FIRST_X_ASSUM(MP_TAC o GEN `n:num` o SPEC `inv(&n + &1)`) THEN
2031 REWRITE_TAC[REAL_LT_INV_EQ; REAL_ARITH `&0 < &n + &1`] THEN
2032 REWRITE_TAC[SKOLEM_THM] THEN DISCH_TAC THEN
2033 MATCH_MP_TAC HAS_ANTIDERIVATIVE_SEQUENCE THEN
2034 UNDISCH_TAC `convex(s:real^M->bool)` THEN SIMP_TAC[] THEN
2035 DISCH_THEN(K ALL_TAC) THEN POP_ASSUM MP_TAC THEN
2036 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `f:num->real^M->real^N` THEN
2037 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `f':num->real^M->real^M->real^N` THEN
2038 REPEAT STRIP_TAC THEN ASM_SIMP_TAC[] THEN
2039 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [REAL_ARCH_INV]) THEN
2040 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN STRIP_TAC THEN
2041 X_GEN_TAC `n:num` THEN REWRITE_TAC[GE] THEN
2042 MAP_EVERY X_GEN_TAC [`x:real^M`; `h:real^M`] THEN STRIP_TAC THEN
2043 MATCH_MP_TAC REAL_LE_TRANS THEN
2044 EXISTS_TAC `inv(&n + &1) * norm(h:real^M)` THEN
2045 ASM_SIMP_TAC[] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
2046 REWRITE_TAC[NORM_POS_LE] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
2047 EXISTS_TAC `inv(&N)` THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2048 MATCH_MP_TAC REAL_LE_INV2 THEN
2049 REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE; REAL_OF_NUM_LT] THEN
2052 (* ------------------------------------------------------------------------- *)
2053 (* Differentiation of a series. *)
2054 (* ------------------------------------------------------------------------- *)
2056 let HAS_DERIVATIVE_SERIES = prove
2057 (`!s f:num->real^M->real^N f' g' k.
2059 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\
2061 ==> ?N. !n x h. n >= N /\ x IN s
2062 ==> norm(vsum(k INTER (0..n)) (\i. f' i x h) -
2063 g' x h) <= e * norm(h)) /\
2064 (?x l. x IN s /\ ((\n. f n x) sums l) k)
2065 ==> ?g. !x. x IN s ==> ((\n. f n x) sums (g x)) k /\
2066 (g has_derivative g'(x)) (at x within s)`,
2067 REPEAT GEN_TAC THEN REWRITE_TAC[sums] THEN
2068 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
2069 MATCH_MP_TAC HAS_DERIVATIVE_SEQUENCE THEN EXISTS_TAC
2070 `\n:num x:real^M h:real^M. vsum(k INTER (0..n)) (\n. f' n x h):real^N` THEN
2071 ASM_SIMP_TAC[ETA_AX; FINITE_INTER_NUMSEG; HAS_DERIVATIVE_VSUM]);;
2073 (* ------------------------------------------------------------------------- *)
2074 (* Derivative with composed bilinear function. *)
2075 (* ------------------------------------------------------------------------- *)
2077 let HAS_DERIVATIVE_BILINEAR_WITHIN = prove
2078 (`!h:real^M->real^N->real^P f g f' g' x:real^Q s.
2079 (f has_derivative f') (at x within s) /\
2080 (g has_derivative g') (at x within s) /\
2082 ==> ((\x. h (f x) (g x)) has_derivative
2083 (\d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)`,
2084 REPEAT STRIP_TAC THEN
2085 SUBGOAL_TAC "contg" `((g:real^Q->real^N) --> g(x)) (at x within s)`
2086 [REWRITE_TAC[GSYM CONTINUOUS_WITHIN] THEN
2087 ASM_MESON_TAC[differentiable; DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]] THEN
2088 UNDISCH_TAC `((f:real^Q->real^M) has_derivative f') (at x within s)` THEN
2089 REWRITE_TAC[has_derivative_within] THEN
2090 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "df")) THEN
2092 `((\y. (f:real^Q->real^M)(x) + f'(y - x)) --> f(x)) (at x within s)`
2093 [GEN_REWRITE_TAC LAND_CONV [GSYM VECTOR_ADD_RID] THEN
2094 MATCH_MP_TAC LIM_ADD THEN REWRITE_TAC[LIM_CONST] THEN
2095 SUBGOAL_THEN `vec 0 = (f':real^Q->real^M)(x - x)` SUBST1_TAC THENL
2096 [ASM_MESON_TAC[LINEAR_0; VECTOR_SUB_REFL]; ALL_TAC] THEN
2097 ASM_SIMP_TAC[LIM_LINEAR; LIM_SUB; LIM_CONST; LIM_WITHIN_ID]] THEN
2098 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [has_derivative_within]) THEN
2099 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (LABEL_TAC "dg")) THEN
2101 [FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [bilinear]) THEN
2102 RULE_ASSUM_TAC(REWRITE_RULE[linear]) THEN ASM_REWRITE_TAC[linear] THEN
2103 REPEAT STRIP_TAC THEN VECTOR_ARITH_TAC;
2105 MP_TAC(ISPECL [`at (x:real^Q) within s`; `h:real^M->real^N->real^P`]
2107 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2108 REMOVE_THEN "contg" MP_TAC THEN REMOVE_THEN "df" MP_TAC THEN
2109 REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
2110 REMOVE_THEN "dg" MP_TAC THEN REMOVE_THEN "contf" MP_TAC THEN
2111 ONCE_REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
2112 REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN
2114 `((\y:real^Q. inv(norm(y - x)) %
2115 (h:real^M->real^N->real^P) (f'(y - x)) (g'(y - x)))
2116 --> vec 0) (at x within s)`
2118 [FIRST_ASSUM(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC o MATCH_MP
2119 BILINEAR_BOUNDED_POS) THEN
2120 X_CHOOSE_THEN `C:real` STRIP_ASSUME_TAC
2121 (MATCH_MP LINEAR_BOUNDED_POS (ASSUME `linear (f':real^Q->real^M)`)) THEN
2122 X_CHOOSE_THEN `D:real` STRIP_ASSUME_TAC
2123 (MATCH_MP LINEAR_BOUNDED_POS (ASSUME `linear (g':real^Q->real^N)`)) THEN
2124 REWRITE_TAC[LIM_WITHIN; dist; VECTOR_SUB_RZERO] THEN
2125 X_GEN_TAC `e:real` THEN STRIP_TAC THEN EXISTS_TAC `e / (B * C * D)` THEN
2126 ASM_SIMP_TAC[REAL_LT_DIV; NORM_MUL; REAL_LT_MUL] THEN
2127 X_GEN_TAC `x':real^Q` THEN
2128 REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NORM; REAL_ABS_INV] THEN
2129 STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN
2130 EXISTS_TAC `inv(norm(x' - x :real^Q)) *
2131 B * (C * norm(x' - x)) * (D * norm(x' - x))` THEN
2133 [MATCH_MP_TAC REAL_LE_LMUL THEN SIMP_TAC[REAL_LE_INV_EQ; NORM_POS_LE] THEN
2134 ASM_MESON_TAC[REAL_LE_LMUL; REAL_LT_IMP_LE; REAL_LE_MUL2; NORM_POS_LE;
2136 ONCE_REWRITE_TAC[AC REAL_MUL_AC
2137 `i * b * (c * x) * (d * x) = (i * x) * x * (b * c * d)`] THEN
2138 ASM_SIMP_TAC[REAL_MUL_LINV; REAL_LT_IMP_NZ; REAL_MUL_LID] THEN
2139 ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_LT_MUL]];
2140 REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN
2141 REWRITE_TAC (map (C MATCH_MP (ASSUME `bilinear(h:real^M->real^N->real^P)`))
2142 [BILINEAR_RZERO; BILINEAR_LZERO; BILINEAR_LADD; BILINEAR_RADD;
2143 BILINEAR_LMUL; BILINEAR_RMUL; BILINEAR_LSUB; BILINEAR_RSUB]) THEN
2144 MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
2145 BINOP_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN VECTOR_ARITH_TAC]);;
2147 let HAS_DERIVATIVE_BILINEAR_AT = prove
2148 (`!h:real^M->real^N->real^P f g f' g' x:real^Q.
2149 (f has_derivative f') (at x) /\
2150 (g has_derivative g') (at x) /\
2152 ==> ((\x. h (f x) (g x)) has_derivative
2153 (\d. h (f x) (g' d) + h (f' d) (g x))) (at x)`,
2154 REWRITE_TAC[has_derivative_at] THEN
2155 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
2156 REWRITE_TAC[GSYM has_derivative_within; HAS_DERIVATIVE_BILINEAR_WITHIN]);;
2158 let BILINEAR_DIFFERENTIABLE_AT_COMPOSE = prove
2159 (`!f:real^M->real^N g:real^M->real^P h:real^N->real^P->real^Q a.
2160 f differentiable at a /\ g differentiable at a /\ bilinear h
2161 ==> (\x. h (f x) (g x)) differentiable at a`,
2162 REPEAT GEN_TAC THEN REWRITE_TAC[FRECHET_DERIVATIVE_WORKS] THEN
2163 DISCH_THEN(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_AT) THEN
2164 REWRITE_TAC[GSYM FRECHET_DERIVATIVE_WORKS; differentiable] THEN
2167 let BILINEAR_DIFFERENTIABLE_WITHIN_COMPOSE = prove
2168 (`!f:real^M->real^N g:real^M->real^P h:real^N->real^P->real^Q x s.
2169 f differentiable at x within s /\ g differentiable at x within s /\
2171 ==> (\x. h (f x) (g x)) differentiable at x within s`,
2172 REPEAT GEN_TAC THEN REWRITE_TAC[FRECHET_DERIVATIVE_WORKS] THEN
2173 DISCH_THEN(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_WITHIN) THEN
2174 REWRITE_TAC[GSYM FRECHET_DERIVATIVE_WORKS; differentiable] THEN
2177 let BILINEAR_DIFFERENTIABLE_ON_COMPOSE = prove
2178 (`!f:real^M->real^N g:real^M->real^P h:real^N->real^P->real^Q s.
2179 f differentiable_on s /\ g differentiable_on s /\ bilinear h
2180 ==> (\x. h (f x) (g x)) differentiable_on s`,
2181 REWRITE_TAC[differentiable_on] THEN
2182 MESON_TAC[BILINEAR_DIFFERENTIABLE_WITHIN_COMPOSE]);;
2184 let DIFFERENTIABLE_AT_LIFT_DOT2 = prove
2185 (`!f:real^M->real^N g x.
2186 f differentiable at x /\ g differentiable at x
2187 ==> (\x. lift(f x dot g x)) differentiable at x`,
2188 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (MATCH_MP (REWRITE_RULE
2189 [TAUT `p /\ q /\ r ==> s <=> r ==> p /\ q ==> s`]
2190 BILINEAR_DIFFERENTIABLE_AT_COMPOSE) BILINEAR_DOT)) THEN REWRITE_TAC[]);;
2192 let DIFFERENTIABLE_WITHIN_LIFT_DOT2 = prove
2193 (`!f:real^M->real^N g x s.
2194 f differentiable (at x within s) /\ g differentiable (at x within s)
2195 ==> (\x. lift(f x dot g x)) differentiable (at x within s)`,
2196 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (MATCH_MP (REWRITE_RULE
2197 [TAUT `p /\ q /\ r ==> s <=> r ==> p /\ q ==> s`]
2198 BILINEAR_DIFFERENTIABLE_WITHIN_COMPOSE) BILINEAR_DOT)) THEN REWRITE_TAC[]);;
2200 let DIFFERENTIABLE_ON_LIFT_DOT2 = prove
2201 (`!f:real^M->real^N g s.
2202 f differentiable_on s /\ g differentiable_on s
2203 ==> (\x. lift(f x dot g x)) differentiable_on s`,
2204 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP (MATCH_MP (REWRITE_RULE
2205 [TAUT `p /\ q /\ r ==> s <=> r ==> p /\ q ==> s`]
2206 BILINEAR_DIFFERENTIABLE_ON_COMPOSE) BILINEAR_DOT)) THEN REWRITE_TAC[]);;
2208 let HAS_DERIVATIVE_MUL_WITHIN = prove
2209 (`!f f' g:real^M->real^N g' a s.
2210 ((lift o f) has_derivative (lift o f')) (at a within s) /\
2211 (g has_derivative g') (at a within s)
2212 ==> ((\x. f x % g x) has_derivative
2213 (\h. f a % g' h + f' h % g a)) (at a within s)`,
2215 DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[BILINEAR_DROP_MUL]
2216 (ISPEC `\x y:real^M. drop x % y` HAS_DERIVATIVE_BILINEAR_WITHIN))) THEN
2217 REWRITE_TAC[o_DEF; DROP_CMUL; LIFT_DROP]);;
2219 let HAS_DERIVATIVE_MUL_AT = prove
2220 (`!f f' g:real^M->real^N g' a.
2221 ((lift o f) has_derivative (lift o f')) (at a) /\
2222 (g has_derivative g') (at a)
2223 ==> ((\x. f x % g x) has_derivative
2224 (\h. f a % g' h + f' h % g a)) (at a)`,
2225 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
2226 REWRITE_TAC[HAS_DERIVATIVE_MUL_WITHIN]);;
2228 let HAS_DERIVATIVE_SQNORM_AT = prove
2230 ((\x. lift(norm x pow 2)) has_derivative (\x. &2 % lift(a dot x))) (at a)`,
2231 GEN_TAC THEN MP_TAC(ISPECL
2232 [`\x y:real^N. lift(x dot y)`;
2233 `\x:real^N. x`; `\x:real^N. x`; `\x:real^N. x`; `\x:real^N. x`;
2234 `a:real^N`] HAS_DERIVATIVE_BILINEAR_AT) THEN
2235 REWRITE_TAC[HAS_DERIVATIVE_ID; BILINEAR_DOT; NORM_POW_2] THEN
2236 MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2237 REWRITE_TAC[FUN_EQ_THM; DOT_SYM] THEN VECTOR_ARITH_TAC);;
2239 let DIFFERENTIABLE_MUL_WITHIN = prove
2240 (`!f g:real^M->real^N a s.
2241 (lift o f) differentiable (at a within s) /\
2242 g differentiable (at a within s)
2243 ==> (\x. f x % g x) differentiable (at a within s)`,
2244 REPEAT GEN_TAC THEN MP_TAC(ISPECL
2245 [`lift o (f:real^M->real)`; `g:real^M->real^N`; `\x y:real^N. drop x % y`;
2246 `a:real^M`; `s:real^M->bool`] BILINEAR_DIFFERENTIABLE_WITHIN_COMPOSE) THEN
2247 REWRITE_TAC[o_DEF; LIFT_DROP; BILINEAR_DROP_MUL]);;
2249 let DIFFERENTIABLE_MUL_AT = prove
2250 (`!f g:real^M->real^N a.
2251 (lift o f) differentiable (at a) /\ g differentiable (at a)
2252 ==> (\x. f x % g x) differentiable (at a)`,
2253 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
2254 REWRITE_TAC[DIFFERENTIABLE_MUL_WITHIN]);;
2256 let DIFFERENTIABLE_SQNORM_AT = prove
2257 (`!a:real^N. (\x. lift(norm x pow 2)) differentiable (at a)`,
2258 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_SQNORM_AT]);;
2260 let DIFFERENTIABLE_ON_MUL = prove
2261 (`!f g:real^M->real^N s.
2262 (lift o f) differentiable_on s /\ g differentiable_on s
2263 ==> (\x. f x % g x) differentiable_on s`,
2264 REPEAT GEN_TAC THEN MP_TAC(ISPECL
2265 [`lift o (f:real^M->real)`; `g:real^M->real^N`; `\x y:real^N. drop x % y`;
2266 `s:real^M->bool`] BILINEAR_DIFFERENTIABLE_ON_COMPOSE) THEN
2267 REWRITE_TAC[o_DEF; LIFT_DROP; BILINEAR_DROP_MUL]);;
2269 let DIFFERENTIABLE_ON_SQNORM = prove
2270 (`!s:real^N->bool. (\x. lift(norm x pow 2)) differentiable_on s`,
2271 SIMP_TAC[DIFFERENTIABLE_AT_IMP_DIFFERENTIABLE_ON;
2272 DIFFERENTIABLE_SQNORM_AT]);;
2274 (* ------------------------------------------------------------------------- *)
2275 (* Considering derivative R(^1)->R^n as a vector. *)
2276 (* ------------------------------------------------------------------------- *)
2278 parse_as_infix ("has_vector_derivative",(12,"right"));;
2280 let has_vector_derivative = new_definition
2281 `(f has_vector_derivative f') net <=>
2282 (f has_derivative (\x. drop(x) % f')) net`;;
2284 let vector_derivative = new_definition
2285 `vector_derivative (f:real^1->real^N) net =
2286 @f'. (f has_vector_derivative f') net`;;
2288 let VECTOR_DERIVATIVE_WORKS = prove
2289 (`!net f:real^1->real^N.
2290 f differentiable net <=>
2291 (f has_vector_derivative (vector_derivative f net)) net`,
2292 REPEAT GEN_TAC THEN REWRITE_TAC[vector_derivative] THEN
2293 CONV_TAC(RAND_CONV SELECT_CONV) THEN
2294 SIMP_TAC[FRECHET_DERIVATIVE_WORKS; has_vector_derivative] THEN EQ_TAC THENL
2295 [ALL_TAC; MESON_TAC[FRECHET_DERIVATIVE_WORKS; differentiable]] THEN
2296 DISCH_TAC THEN EXISTS_TAC `column 1 (jacobian (f:real^1->real^N) net)` THEN
2297 FIRST_ASSUM MP_TAC THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
2298 AP_TERM_TAC THEN REWRITE_TAC[jacobian] THEN
2299 MATCH_MP_TAC LINEAR_FROM_REALS THEN
2300 RULE_ASSUM_TAC(REWRITE_RULE[has_derivative]) THEN ASM_REWRITE_TAC[]);;
2302 let VECTOR_DERIVATIVE_UNIQUE_AT = prove
2303 (`!f:real^1->real^N x f' f''.
2304 (f has_vector_derivative f') (at x) /\
2305 (f has_vector_derivative f'') (at x)
2307 REWRITE_TAC[has_vector_derivative; drop] THEN REPEAT STRIP_TAC THEN
2308 MP_TAC(ISPECL [`f:real^1->real^N`;
2309 `\x. drop x % (f':real^N)`; `\x. drop x % (f'':real^N)`;
2310 `x:real^1`] FRECHET_DERIVATIVE_UNIQUE_AT) THEN
2311 ASM_SIMP_TAC[DIMINDEX_1; LE_ANTISYM; drop] THEN
2312 REWRITE_TAC[FUN_EQ_THM] THEN DISCH_THEN(MP_TAC o SPEC `vec 1:real^1`) THEN
2313 SIMP_TAC[VEC_COMPONENT; DIMINDEX_1; ARITH; VECTOR_MUL_LID]);;
2315 let HAS_VECTOR_DERIVATIVE_UNIQUE_AT = prove
2316 (`!f:real^1->real^N f' x.
2317 (f has_vector_derivative f') (at x)
2318 ==> vector_derivative f (at x) = f'`,
2319 REPEAT STRIP_TAC THEN MATCH_MP_TAC VECTOR_DERIVATIVE_UNIQUE_AT THEN
2320 MAP_EVERY EXISTS_TAC [`f:real^1->real^N`; `x:real^1`] THEN
2321 ASM_REWRITE_TAC[vector_derivative] THEN CONV_TAC SELECT_CONV THEN
2324 let VECTOR_DERIVATIVE_UNIQUE_WITHIN_CLOSED_INTERVAL = prove
2325 (`!f:real^1->real^N a b x f' f''.
2327 x IN interval [a,b] /\
2328 (f has_vector_derivative f') (at x within interval [a,b]) /\
2329 (f has_vector_derivative f'') (at x within interval [a,b])
2331 REWRITE_TAC[has_vector_derivative; drop] THEN REPEAT STRIP_TAC THEN
2332 MP_TAC(ISPECL [`f:real^1->real^N`;
2333 `\x. drop x % (f':real^N)`; `\x. drop x % (f'':real^N)`;
2334 `x:real^1`; `a:real^1`; `b:real^1`]
2335 FRECHET_DERIVATIVE_UNIQUE_WITHIN_CLOSED_INTERVAL) THEN
2336 ASM_SIMP_TAC[DIMINDEX_1; LE_ANTISYM; drop] THEN
2337 ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN REWRITE_TAC[FUN_EQ_THM] THEN
2338 DISCH_THEN(MP_TAC o SPEC `vec 1:real^1`) THEN
2339 SIMP_TAC[VEC_COMPONENT; DIMINDEX_1; ARITH; VECTOR_MUL_LID]);;
2341 let VECTOR_DERIVATIVE_AT = prove
2342 (`(f has_vector_derivative f') (at x) ==> vector_derivative f (at x) = f'`,
2343 ASM_MESON_TAC[VECTOR_DERIVATIVE_UNIQUE_AT;
2344 VECTOR_DERIVATIVE_WORKS; differentiable; has_vector_derivative]);;
2346 let VECTOR_DERIVATIVE_WITHIN_CLOSED_INTERVAL = prove
2347 (`!f:real^1->real^N f' x a b.
2348 drop a < drop b /\ x IN interval[a,b] /\
2349 (f has_vector_derivative f') (at x within interval [a,b])
2350 ==> vector_derivative f (at x within interval [a,b]) = f'`,
2351 ASM_MESON_TAC[VECTOR_DERIVATIVE_UNIQUE_WITHIN_CLOSED_INTERVAL;
2352 VECTOR_DERIVATIVE_WORKS; differentiable; has_vector_derivative]);;
2354 let HAS_VECTOR_DERIVATIVE_WITHIN_SUBSET = prove
2355 (`!f s t x. (f has_vector_derivative f') (at x within s) /\ t SUBSET s
2356 ==> (f has_vector_derivative f') (at x within t)`,
2357 REWRITE_TAC[has_vector_derivative; HAS_DERIVATIVE_WITHIN_SUBSET]);;
2359 let HAS_VECTOR_DERIVATIVE_CONST = prove
2360 (`!c net. ((\x. c) has_vector_derivative vec 0) net`,
2361 REWRITE_TAC[has_vector_derivative] THEN
2362 REWRITE_TAC[VECTOR_MUL_RZERO; HAS_DERIVATIVE_CONST]);;
2364 let VECTOR_DERIVATIVE_CONST_AT = prove
2365 (`!c:real^N a. vector_derivative (\x. c) (at a) = vec 0`,
2366 REPEAT GEN_TAC THEN MATCH_MP_TAC HAS_VECTOR_DERIVATIVE_UNIQUE_AT THEN
2367 REWRITE_TAC[HAS_VECTOR_DERIVATIVE_CONST]);;
2369 let HAS_VECTOR_DERIVATIVE_ID = prove
2370 (`!net. ((\x. x) has_vector_derivative (vec 1)) net`,
2371 REWRITE_TAC[has_vector_derivative] THEN
2372 SUBGOAL_THEN `(\x. drop x % vec 1) = (\x. x)`
2373 (fun th -> REWRITE_TAC[HAS_DERIVATIVE_ID; th]) THEN
2374 REWRITE_TAC[FUN_EQ_THM; GSYM DROP_EQ; DROP_CMUL; DROP_VEC] THEN
2377 let HAS_VECTOR_DERIVATIVE_CMUL = prove
2378 (`!f f' net c. (f has_vector_derivative f') net
2379 ==> ((\x. c % f(x)) has_vector_derivative (c % f')) net`,
2380 SIMP_TAC[has_vector_derivative] THEN
2381 ONCE_REWRITE_TAC[VECTOR_ARITH `a % b % x = b % a % x`] THEN
2382 SIMP_TAC[HAS_DERIVATIVE_CMUL]);;
2384 let HAS_VECTOR_DERIVATIVE_CMUL_EQ = prove
2387 ==> (((\x. c % f(x)) has_vector_derivative (c % f')) net <=>
2388 (f has_vector_derivative f') net)`,
2389 REPEAT STRIP_TAC THEN EQ_TAC THEN
2390 DISCH_THEN(MP_TAC o MATCH_MP HAS_VECTOR_DERIVATIVE_CMUL) THENL
2391 [DISCH_THEN(MP_TAC o SPEC `inv(c):real`);
2392 DISCH_THEN(MP_TAC o SPEC `c:real`)] THEN
2393 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; VECTOR_MUL_LID; ETA_AX]);;
2395 let HAS_VECTOR_DERIVATIVE_NEG = prove
2396 (`!f f' net. (f has_vector_derivative f') net
2397 ==> ((\x. --(f(x))) has_vector_derivative (--f')) net`,
2398 SIMP_TAC[has_vector_derivative; VECTOR_MUL_RNEG; HAS_DERIVATIVE_NEG]);;
2400 let HAS_VECTOR_DERIVATIVE_NEG_EQ = prove
2401 (`!f f' net. ((\x. --(f(x))) has_vector_derivative --f') net <=>
2402 (f has_vector_derivative f') net`,
2403 SIMP_TAC[has_vector_derivative; HAS_DERIVATIVE_NEG_EQ; VECTOR_MUL_RNEG]);;
2405 let HAS_VECTOR_DERIVATIVE_ADD = prove
2407 (f has_vector_derivative f') net /\ (g has_vector_derivative g') net
2408 ==> ((\x. f(x) + g(x)) has_vector_derivative (f' + g')) net`,
2409 SIMP_TAC[has_vector_derivative; VECTOR_ADD_LDISTRIB; HAS_DERIVATIVE_ADD]);;
2411 let HAS_VECTOR_DERIVATIVE_SUB = prove
2413 (f has_vector_derivative f') net /\ (g has_vector_derivative g') net
2414 ==> ((\x. f(x) - g(x)) has_vector_derivative (f' - g')) net`,
2415 SIMP_TAC[has_vector_derivative; VECTOR_SUB_LDISTRIB; HAS_DERIVATIVE_SUB]);;
2417 let HAS_VECTOR_DERIVATIVE_BILINEAR_WITHIN = prove
2418 (`!h:real^M->real^N->real^P f g f' g' x s.
2419 (f has_vector_derivative f') (at x within s) /\
2420 (g has_vector_derivative g') (at x within s) /\
2422 ==> ((\x. h (f x) (g x)) has_vector_derivative
2423 (h (f x) g' + h f' (g x))) (at x within s)`,
2424 REPEAT GEN_TAC THEN REWRITE_TAC[has_vector_derivative] THEN
2426 FIRST_ASSUM(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_WITHIN) THEN
2427 RULE_ASSUM_TAC(REWRITE_RULE[bilinear; linear]) THEN
2428 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB]);;
2430 let HAS_VECTOR_DERIVATIVE_BILINEAR_AT = prove
2431 (`!h:real^M->real^N->real^P f g f' g' x.
2432 (f has_vector_derivative f') (at x) /\
2433 (g has_vector_derivative g') (at x) /\
2435 ==> ((\x. h (f x) (g x)) has_vector_derivative
2436 (h (f x) g' + h f' (g x))) (at x)`,
2437 REPEAT GEN_TAC THEN REWRITE_TAC[has_vector_derivative] THEN
2439 FIRST_ASSUM(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_AT) THEN
2440 RULE_ASSUM_TAC(REWRITE_RULE[bilinear; linear]) THEN
2441 ASM_REWRITE_TAC[VECTOR_ADD_LDISTRIB]);;
2443 let HAS_VECTOR_DERIVATIVE_AT_WITHIN = prove
2444 (`!f x s. (f has_vector_derivative f') (at x)
2445 ==> (f has_vector_derivative f') (at x within s)`,
2446 SIMP_TAC[has_vector_derivative; HAS_DERIVATIVE_AT_WITHIN]);;
2448 let HAS_VECTOR_DERIVATIVE_TRANSFORM_WITHIN = prove
2451 (!x'. x' IN s /\ dist (x',x) < d ==> f x' = g x') /\
2452 (f has_vector_derivative f') (at x within s)
2453 ==> (g has_vector_derivative f') (at x within s)`,
2454 REWRITE_TAC[has_vector_derivative; HAS_DERIVATIVE_TRANSFORM_WITHIN]);;
2456 let HAS_VECTOR_DERIVATIVE_TRANSFORM_AT = prove
2458 &0 < d /\ (!x'. dist (x',x) < d ==> f x' = g x') /\
2459 (f has_vector_derivative f') (at x)
2460 ==> (g has_vector_derivative f') (at x)`,
2461 REWRITE_TAC[has_vector_derivative; HAS_DERIVATIVE_TRANSFORM_AT]);;
2463 let HAS_VECTOR_DERIVATIVE_TRANSFORM_WITHIN_OPEN = prove
2466 (!y. y IN s ==> f y = g y) /\
2467 (f has_vector_derivative f') (at x)
2468 ==> (g has_vector_derivative f') (at x)`,
2469 REWRITE_TAC[has_vector_derivative; HAS_DERIVATIVE_TRANSFORM_WITHIN_OPEN]);;
2471 let VECTOR_DIFF_CHAIN_AT = prove
2473 (f has_vector_derivative f') (at x) /\
2474 (g has_vector_derivative g') (at (f x))
2475 ==> ((g o f) has_vector_derivative (drop f' % g')) (at x)`,
2476 REPEAT GEN_TAC THEN REWRITE_TAC[has_vector_derivative] THEN
2477 DISCH_THEN(MP_TAC o MATCH_MP DIFF_CHAIN_AT) THEN
2478 REWRITE_TAC[o_DEF; DROP_CMUL; GSYM VECTOR_MUL_ASSOC]);;
2480 let VECTOR_DIFF_CHAIN_WITHIN = prove
2482 (f has_vector_derivative f') (at x within s) /\
2483 (g has_vector_derivative g') (at (f x) within IMAGE f s)
2484 ==> ((g o f) has_vector_derivative (drop f' % g')) (at x within s)`,
2485 REPEAT GEN_TAC THEN REWRITE_TAC[has_vector_derivative] THEN
2486 DISCH_THEN(MP_TAC o MATCH_MP DIFF_CHAIN_WITHIN) THEN
2487 REWRITE_TAC[o_DEF; DROP_CMUL; GSYM VECTOR_MUL_ASSOC]);;
2489 (* ------------------------------------------------------------------------- *)
2490 (* Various versions of Kachurovskii's theorem. *)
2491 (* ------------------------------------------------------------------------- *)
2493 let CONVEX_ON_DERIVATIVE_SECANT_IMP = prove
2494 (`!f f' s x y:real^N.
2495 f convex_on s /\ segment[x,y] SUBSET s /\
2496 ((lift o f) has_derivative (lift o f')) (at x within s)
2497 ==> f'(y - x) <= f y - f x`,
2498 REPEAT STRIP_TAC THEN
2499 SUBGOAL_THEN `(x:real^N) IN s /\ (y:real^N) IN s` ASSUME_TAC THENL
2500 [ASM_MESON_TAC[SUBSET; ENDS_IN_SEGMENT]; ALL_TAC] THEN
2501 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [has_derivative_within]) THEN
2502 REWRITE_TAC[LIM_WITHIN; DIST_0; o_THM] THEN
2503 REWRITE_TAC[GSYM LIFT_ADD; GSYM LIFT_SUB; GSYM LIFT_CMUL; NORM_LIFT] THEN
2504 STRIP_TAC THEN ASM_CASES_TAC `y:real^N = x` THENL
2505 [FIRST_X_ASSUM(MP_TAC o MATCH_MP LINEAR_0) THEN
2506 REWRITE_TAC[o_THM; VECTOR_SUB_REFL; GSYM DROP_EQ; DROP_VEC; LIFT_DROP] THEN
2507 ASM_SIMP_TAC[REAL_SUB_REFL; REAL_LE_REFL; VECTOR_SUB_REFL];
2509 ABBREV_TAC `e = (f':real^N->real)(y - x) - (f y - f x)` THEN
2510 ASM_CASES_TAC `&0 < e` THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
2511 FIRST_X_ASSUM(MP_TAC o SPEC `e / &2 / norm(y - x:real^N)`) THEN
2512 ASM_SIMP_TAC[REAL_LT_DIV; REAL_HALF; NORM_POS_LT; VECTOR_SUB_EQ] THEN
2513 DISCH_THEN(X_CHOOSE_THEN `d:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
2514 ABBREV_TAC `u = min (&1 / &2) (d / &2 / norm (y - x:real^N))` THEN
2515 SUBGOAL_THEN `&0 < u /\ u < &1` STRIP_ASSUME_TAC THENL
2516 [EXPAND_TAC "u" THEN REWRITE_TAC[REAL_LT_MIN; REAL_MIN_LT] THEN
2517 ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; REAL_HALF; VECTOR_SUB_EQ] THEN
2518 CONV_TAC REAL_RAT_REDUCE_CONV;
2520 ABBREV_TAC `z:real^N = (&1 - u) % x + u % y` THEN
2521 SUBGOAL_THEN `(z:real^N) IN segment(x,y)` MP_TAC THENL
2522 [ASM_MESON_TAC[IN_SEGMENT]; ALL_TAC] THEN
2523 SIMP_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY; DE_MORGAN_THM] THEN
2524 STRIP_TAC THEN DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN
2525 SUBGOAL_THEN `(z:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
2527 [ASM_SIMP_TAC[DIST_POS_LT] THEN
2528 EXPAND_TAC "z" THEN REWRITE_TAC[dist; NORM_MUL; VECTOR_ARITH
2529 `((&1 - u) % x + u % y) - x:real^N = u % (y - x)`] THEN
2530 ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; NORM_POS_LT; VECTOR_SUB_EQ] THEN
2533 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [CONVEX_ON_LEFT_SECANT]) THEN
2534 DISCH_THEN(MP_TAC o SPECL [`x:real^N`; `y:real^N`; `z:real^N`]) THEN
2535 ASM_REWRITE_TAC[open_segment; IN_DIFF; IN_INSERT; NOT_IN_EMPTY] THEN
2536 SIMP_TAC[REAL_ARITH `inv y * (z - (x + d)):real = (z - x) / y - d / y`] THEN
2537 REWRITE_TAC[IMP_IMP] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
2538 `z <= y / n /\ abs(z - d) < e / n ==> d <= (y + e) / n`)) THEN
2540 `(f':real^N->real)(z - x) / norm(z - x) = f'(y - x) / norm(y - x)`
2542 [EXPAND_TAC "z" THEN
2543 REWRITE_TAC[VECTOR_ARITH
2544 `((&1 - u) % x + u % y) - x:real^N = u % (y - x)`] THEN
2545 FIRST_ASSUM(MP_TAC o MATCH_MP LINEAR_CMUL) THEN
2546 DISCH_THEN(MP_TAC o SPECL [`u:real`; `y - x:real^N`]) THEN
2547 ASM_REWRITE_TAC[GSYM LIFT_CMUL; o_THM; LIFT_EQ] THEN
2548 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[NORM_MUL] THEN
2549 ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE] THEN
2550 REWRITE_TAC[real_div; REAL_INV_MUL; REAL_MUL_ASSOC] THEN
2551 AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN
2552 REWRITE_TAC[GSYM real_div] THEN MATCH_MP_TAC REAL_DIV_LMUL THEN
2554 ASM_SIMP_TAC[REAL_LE_DIV2_EQ; NORM_POS_LT; VECTOR_SUB_EQ] THEN
2555 ASM_REAL_ARITH_TAC]);;
2557 let CONVEX_ON_SECANT_DERIVATIVE_IMP = prove
2558 (`!f f' s x y:real^N.
2559 f convex_on s /\ segment[x,y] SUBSET s /\
2560 ((lift o f) has_derivative (lift o f')) (at y within s)
2561 ==> f y - f x <= f'(y - x)`,
2562 ONCE_REWRITE_TAC[SEGMENT_SYM] THEN REPEAT STRIP_TAC THEN
2564 [`f:real^N->real`; `f':real^N->real`; `s:real^N->bool`;
2565 `y:real^N`; `x:real^N`] CONVEX_ON_DERIVATIVE_SECANT_IMP) THEN
2566 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SEGMENT_SYM] THEN
2567 MATCH_MP_TAC(REAL_ARITH
2568 `f' = --f'' ==> f' <= x - y ==> y - x <= f''`) THEN
2569 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM VECTOR_NEG_SUB] THEN
2570 GEN_REWRITE_TAC I [GSYM LIFT_EQ] THEN REWRITE_TAC[LIFT_NEG] THEN
2571 SPEC_TAC(`y - x:real^N`,`z:real^N`) THEN
2572 MATCH_MP_TAC(REWRITE_RULE[RIGHT_FORALL_IMP_THM] LINEAR_NEG) THEN
2573 REWRITE_TAC[GSYM o_DEF] THEN ASM_MESON_TAC[has_derivative]);;
2575 let CONVEX_ON_DERIVATIVES_IMP = prove
2576 (`!f f'x f'y s x y:real^N.
2577 f convex_on s /\ segment[x,y] SUBSET s /\
2578 ((lift o f) has_derivative (lift o f'x)) (at x within s) /\
2579 ((lift o f) has_derivative (lift o f'y)) (at y within s)
2580 ==> f'x(y - x) <= f'y(y - x)`,
2581 ASM_MESON_TAC[CONVEX_ON_DERIVATIVE_SECANT_IMP;
2582 CONVEX_ON_SECANT_DERIVATIVE_IMP;
2583 SEGMENT_SYM; REAL_LE_TRANS]);;
2585 let CONVEX_ON_DERIVATIVE_SECANT,CONVEX_ON_DERIVATIVES =
2587 (`(!f f' s:real^N->bool.
2589 (!x. x IN s ==> ((lift o f) has_derivative (lift o f'(x)))
2591 ==> (f convex_on s <=>
2592 !x y. x IN s /\ y IN s ==> f'(x)(y - x) <= f y - f x)) /\
2593 (!f f' s:real^N->bool.
2595 (!x. x IN s ==> ((lift o f) has_derivative (lift o f'(x)))
2597 ==> (f convex_on s <=>
2598 !x y. x IN s /\ y IN s ==> f'(x)(y - x) <= f'(y)(y - x)))`,
2599 REWRITE_TAC[AND_FORALL_THM] THEN REPEAT GEN_TAC THEN
2600 REWRITE_TAC[TAUT `(a ==> b) /\ (a ==> c) <=> a ==> b /\ c`] THEN
2601 STRIP_TAC THEN MATCH_MP_TAC(TAUT
2602 `(a ==> b) /\ (b ==> c) /\ (c ==> a) ==> (a <=> b) /\ (a <=> c)`) THEN
2603 REPEAT CONJ_TAC THENL
2604 [REPEAT STRIP_TAC THEN MATCH_MP_TAC CONVEX_ON_DERIVATIVE_SECANT_IMP THEN
2605 EXISTS_TAC `s:real^N->bool` THEN ASM_SIMP_TAC[ETA_AX] THEN
2606 ASM_MESON_TAC[CONVEX_CONTAINS_SEGMENT];
2607 DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
2608 STRIP_TAC THEN FIRST_X_ASSUM(fun th ->
2609 MP_TAC(ISPECL [`x:real^N`; `y:real^N`] th) THEN
2610 MP_TAC(ISPECL [`y:real^N`; `x:real^N`] th)) THEN
2611 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC(REAL_ARITH
2612 `f''' = --f'' ==> f''' <= x - y ==> f' <= y - x ==> f' <= f''`) THEN
2613 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM VECTOR_NEG_SUB] THEN
2614 GEN_REWRITE_TAC I [GSYM LIFT_EQ] THEN REWRITE_TAC[LIFT_NEG] THEN
2615 SPEC_TAC(`y - x:real^N`,`z:real^N`) THEN
2616 MATCH_MP_TAC(REWRITE_RULE[RIGHT_FORALL_IMP_THM] LINEAR_NEG) THEN
2617 REWRITE_TAC[GSYM o_DEF] THEN REWRITE_TAC[GSYM I_DEF; I_O_ID] THEN
2618 ASM_MESON_TAC[has_derivative];
2620 DISCH_TAC THEN REWRITE_TAC[convex_on] THEN
2621 MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN
2622 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
2623 REWRITE_TAC[TAUT `a /\ b /\ c /\ d /\ e <=> e /\ a /\ b /\ c /\ d`] THEN
2624 REWRITE_TAC[IMP_CONJ; REAL_ARITH `u + v = &1 <=> u = &1 - v`] THEN
2625 REWRITE_TAC[FORALL_UNWIND_THM2; REAL_SUB_LE] THEN X_GEN_TAC `u:real` THEN
2626 REPEAT STRIP_TAC THEN
2627 ASM_CASES_TAC `u = &0` THEN
2628 ASM_SIMP_TAC[REAL_SUB_RZERO; VECTOR_MUL_LZERO; VECTOR_MUL_LID; REAL_LE_REFL;
2629 REAL_MUL_LZERO; REAL_MUL_LID; VECTOR_ADD_RID; REAL_ADD_RID] THEN
2630 ASM_CASES_TAC `u = &1` THEN
2631 ASM_SIMP_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_MUL_LID; REAL_LE_REFL;
2632 REAL_MUL_LZERO; REAL_MUL_LID; VECTOR_ADD_LID; REAL_ADD_LID] THEN
2633 SUBGOAL_THEN `&0 < u /\ u < &1` STRIP_ASSUME_TAC THENL
2634 [ASM_REWRITE_TAC[REAL_LT_LE]; ALL_TAC] THEN
2636 [`lift o (f:real^N->real) o (\u. (&1 - drop u) % a + drop u % b)`;
2637 `\x:real^1. lift o f'((&1 - drop x) % a + drop x % b) o
2638 (\u. --(drop u) % a + drop u % b:real^N)`] MVT_VERY_SIMPLE) THEN
2639 DISCH_THEN(fun th ->
2640 MP_TAC(ISPECL [`vec 0:real^1`; `lift u`] th) THEN
2641 MP_TAC(ISPECL [`lift u`; `vec 1:real^1`] th)) THEN
2642 ASM_REWRITE_TAC[LIFT_DROP; o_THM] THEN
2643 ASM_SIMP_TAC[DROP_VEC; VECTOR_MUL_LZERO; REAL_SUB_RZERO; REAL_LT_IMP_LE;
2644 VECTOR_ADD_RID; VECTOR_MUL_LID; VECTOR_SUB_RZERO] THEN
2646 `(a1 /\ a2) /\ (b1 ==> b2 ==> c) ==> (a1 ==> b1) ==> (a2 ==> b2) ==> c`) THEN
2648 [CONJ_TAC THEN X_GEN_TAC `v:real^1` THEN DISCH_TAC THEN
2649 (REWRITE_TAC[o_ASSOC] THEN MATCH_MP_TAC DIFF_CHAIN_WITHIN THEN
2650 REWRITE_TAC[] THEN CONJ_TAC THENL
2651 [MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN CONJ_TAC THENL
2652 [ONCE_REWRITE_TAC[VECTOR_ARITH `(&1 - a) % x:real^N = x + --a % x`;
2653 VECTOR_ARITH `--u % a:real^N = vec 0 + --u % a`] THEN
2654 MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN
2655 REWRITE_TAC[HAS_DERIVATIVE_CONST];
2657 MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
2658 REWRITE_TAC[linear; DROP_ADD; DROP_CMUL] THEN VECTOR_ARITH_TAC;
2659 MATCH_MP_TAC HAS_DERIVATIVE_WITHIN_SUBSET THEN
2660 EXISTS_TAC `s:real^N->bool` THEN CONJ_TAC THENL
2661 [FIRST_X_ASSUM MATCH_MP_TAC;
2662 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE] THEN GEN_TAC THEN DISCH_TAC] THEN
2663 FIRST_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [CONVEX_ALT]) THEN
2664 RULE_ASSUM_TAC(REWRITE_RULE[IN_INTERVAL_1; LIFT_DROP; DROP_VEC]) THEN
2665 ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC]);
2666 REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_ADD_LID] THEN
2667 REWRITE_TAC[EXISTS_LIFT; LIFT_DROP; IN_INTERVAL_1; DROP_VEC] THEN
2668 REWRITE_TAC[GSYM LIFT_SUB; LIFT_EQ] THEN
2669 REWRITE_TAC[DROP_SUB; DROP_VEC; LIFT_DROP] THEN
2670 REWRITE_TAC[VECTOR_ARITH `--u % a + u % b:real^N = u % (b - a)`] THEN
2671 REWRITE_TAC[LEFT_IMP_EXISTS_THM; RIGHT_IMP_FORALL_THM] THEN
2672 MAP_EVERY X_GEN_TAC [`w:real`; `v:real`] THEN
2673 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
2674 ONCE_REWRITE_TAC[TAUT `a ==> b /\ c ==> d <=> b ==> a ==> c ==> d`] THEN
2675 STRIP_TAC THEN REWRITE_TAC[IMP_IMP] THEN
2676 DISCH_THEN(CONJUNCTS_THEN2 (MP_TAC o AP_TERM `(*) (u:real)`)
2677 (MP_TAC o AP_TERM `(*) (&1 - u:real)`)) THEN
2678 MATCH_MP_TAC(REAL_ARITH
2679 `f1 <= f2 /\ (xa <= xb ==> a <= b)
2680 ==> xa = f1 ==> xb = f2 ==> a <= b`) THEN
2681 CONJ_TAC THENL [ALL_TAC; REAL_ARITH_TAC] THEN
2683 `((&1 - v) % a + v % b:real^N) IN s /\
2684 ((&1 - w) % a + w % b:real^N) IN s`
2685 STRIP_ASSUME_TAC THENL
2687 FIRST_X_ASSUM(MATCH_MP_TAC o GEN_REWRITE_RULE I [CONVEX_ALT]) THEN
2688 ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC;
2691 `linear(lift o (f'((&1 - v) % a + v % b:real^N):real^N->real)) /\
2692 linear(lift o (f'((&1 - w) % a + w % b:real^N):real^N->real))`
2693 MP_TAC THENL [ASM_MESON_TAC[has_derivative]; ALL_TAC] THEN
2694 DISCH_THEN(CONJUNCTS_THEN(MP_TAC o MATCH_MP LINEAR_CMUL)) THEN
2695 ASM_REWRITE_TAC[o_THM; GSYM LIFT_NEG; GSYM LIFT_CMUL; LIFT_EQ] THEN
2696 REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
2697 ONCE_REWRITE_TAC[REAL_ARITH `(&1 - u) * u * x = u * (&1 - u) * x`] THEN
2698 REPEAT(MATCH_MP_TAC REAL_LE_LMUL THEN
2699 CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
2700 FIRST_X_ASSUM(MP_TAC o SPECL
2701 [`(&1 - v) % a + v % b:real^N`; `(&1 - w) % a + w % b:real^N`]) THEN
2702 ASM_REWRITE_TAC[VECTOR_ARITH
2703 `((&1 - v) % a + v % b) - ((&1 - w) % a + w % b):real^N =
2704 (v - w) % (b - a)`] THEN
2705 ASM_CASES_TAC `v:real = w` THEN ASM_SIMP_TAC[REAL_LE_REFL] THEN
2706 SUBGOAL_THEN `&0 < w - v` (fun th -> SIMP_TAC[th; REAL_LE_LMUL_EQ]) THEN
2707 ASM_REAL_ARITH_TAC]);;
2709 let CONVEX_ON_SECANT_DERIVATIVE = prove
2710 (`!f f' s:real^N->bool.
2712 (!x. x IN s ==> ((lift o f) has_derivative (lift o f'(x)))
2714 ==> (f convex_on s <=>
2715 !x y. x IN s /\ y IN s ==> f y - f x <= f'(y)(y - x))`,
2716 REPEAT GEN_TAC THEN DISCH_TAC THEN
2717 FIRST_ASSUM(SUBST1_TAC o MATCH_MP CONVEX_ON_DERIVATIVE_SECANT) THEN
2718 GEN_REWRITE_TAC RAND_CONV [SWAP_FORALL_THM] THEN
2719 AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
2720 X_GEN_TAC `x:real^N` THEN REWRITE_TAC[] THEN
2721 AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
2722 X_GEN_TAC `y:real^N` THEN REWRITE_TAC[] THEN
2723 MAP_EVERY ASM_CASES_TAC [`(x:real^N) IN s`; `(y:real^N) IN s`] THEN
2724 ASM_REWRITE_TAC[] THEN
2725 MATCH_MP_TAC(REAL_ARITH
2726 `f' = --f'' ==> (f' <= y - x <=> x - y <= f'')`) THEN
2727 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM VECTOR_NEG_SUB] THEN
2728 GEN_REWRITE_TAC I [GSYM LIFT_EQ] THEN REWRITE_TAC[LIFT_NEG] THEN
2729 SPEC_TAC(`x - y:real^N`,`z:real^N`) THEN
2730 MATCH_MP_TAC(REWRITE_RULE[RIGHT_FORALL_IMP_THM] LINEAR_NEG) THEN
2731 REWRITE_TAC[GSYM o_DEF] THEN
2732 REWRITE_TAC[GSYM I_DEF; I_O_ID] THEN ASM_MESON_TAC[has_derivative]);;