1(* ========================================================================= *) 2(* *) 3(* Univariate Derivative Theory in R^1 *) 4(* *) 5(* (c) Copyright, John Harrison 1998-2008 *) 6(* (c) Copyright, Marco Maggesi 2014 *) 7(* (c) Copyright 2015, *) 8(* Muhammad Qasim, *) 9(* Osman Hasan, *) 10(* Hardware Verification Group, *) 11(* Concordia University *) 12(* Contact: <m_qasi@ece.concordia.ca> *) 13(* *) 14(* Note: This theory was ported from HOL Light *) 15(* *) 16(* ========================================================================= *) 17 18open HolKernel Parse boolLib bossLib; 19 20open numTheory numLib unwindLib tautLib Arith prim_recTheory pairTheory 21 combinTheory quotientTheory arithmeticTheory pred_setTheory realTheory 22 realLib jrhUtils seqTheory limTheory transcTheory listTheory mesonLib 23 topologyTheory optionTheory RealArith pred_setLib cardinalTheory; 24 25open hurdUtils iterateTheory productTheory real_topologyTheory; 26 27val _ = new_theory "derivative"; 28 29fun MESON ths tm = prove(tm,MESON_TAC ths); 30fun METIS ths tm = prove(tm,METIS_TAC ths); 31 32val DISC_RW_KILL = DISCH_TAC THEN ONCE_ASM_REWRITE_TAC [] THEN 33 POP_ASSUM K_TAC; 34 35fun ASSERT_TAC tm = SUBGOAL_THEN tm STRIP_ASSUME_TAC; 36val ASM_ARITH_TAC = REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC; 37 38(* Minimal hol-light compatibility layer *) 39val ASM_REAL_ARITH_TAC = REAL_ASM_ARITH_TAC; (* RealArith *) 40val IMP_CONJ = CONJ_EQ_IMP; (* cardinalTheory *) 41val FINITE_SUBSET = SUBSET_FINITE_I; (* pred_setTheory *) 42val LE_0 = ZERO_LESS_EQ; (* arithmeticTheory *) 43 44(* ------------------------------------------------------------------------- *) 45(* convex *) 46(* ------------------------------------------------------------------------- *) 47 48val convex = new_definition ("convex", 49 ``convex (s:real->bool) <=> 50 !x y u v. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ (u + v = &1) 51 ==> ((u * x) + (v * y)) IN s``); 52 53Theorem CONVEX_ALT : 54 !s. convex s <=> !x y u. x IN s /\ y IN s /\ &0 <= u /\ u <= &1 55 ==> ((&1 - u) * x + u * y) IN s 56Proof 57 GEN_TAC >> REWRITE_TAC [convex] THEN 58 MESON_TAC [REAL_ARITH ``&0:real <= u /\ &0 <= v /\ (u + v = &1) 59 ==> v <= &1 /\ (u = &1 - v)``, 60 REAL_ARITH ``u <= &1 ==> &0:real <= &1 - u /\ ((&1 - u) + u = &1)``] 61QED 62 63val IN_CONVEX_SET = store_thm ("IN_CONVEX_SET", 64 ``!s a b u. 65 convex s /\ a IN s /\ b IN s /\ &0 <= u /\ u <= &1 66 ==> ((&1 - u) * a + u * b) IN s``, 67 MESON_TAC[CONVEX_ALT]); 68 69val LIMPT_APPROACHABLE = store_thm ("LIMPT_APPROACHABLE", 70 ``!x s. x limit_point_of s <=> 71 !e. &0 < e ==> ?x'. x' IN s /\ ~(x' = x) /\ dist(x',x) < e``, 72 REPEAT GEN_TAC THEN REWRITE_TAC[limit_point_of] THEN 73 MESON_TAC[open_def, DIST_SYM, OPEN_BALL, CENTRE_IN_BALL, IN_BALL]); 74 75Theorem LIMPT_OF_CONVEX : 76 !s x:real. convex s /\ x IN s ==> (x limit_point_of s <=> ~(s = {x})) 77Proof 78 rpt STRIP_TAC 79 >> ASM_CASES_TAC ``s = {x:real}`` >> art [LIMPT_SING] 80 >> `?y:real. y IN s /\ ~(y = x)` by ASM_SET_TAC [] 81 >> REWRITE_TAC [LIMPT_APPROACHABLE] 82 >> Q.X_GEN_TAC `e` >> DISCH_TAC 83 >> Q.ABBREV_TAC `u = min (&1 / &2) (e / &2 / abs(y - x:real))` 84 >> Know `&0 < u /\ u < &1:real` 85 >- (Q.UNABBREV_TAC `u` >> REWRITE_TAC [REAL_LT_MIN, REAL_MIN_LT] \\ 86 SIMP_TAC std_ss [REAL_HALF_BETWEEN] \\ 87 ASM_SIMP_TAC real_ss [REAL_HALF, REAL_LT_DIV, GSYM ABS_NZ, REAL_SUB_0]) 88 >> DISCH_TAC 89 >> Q.EXISTS_TAC `(&1 - u) * x + u * y:real` 90 >> rpt CONJ_TAC (* 3 subgoals *) 91 >| [ (* goal 1 (of 3) *) 92 FIRST_X_ASSUM (MATCH_MP_TAC o REWRITE_RULE [CONVEX_ALT]) \\ 93 ASM_SIMP_TAC real_ss [REAL_LT_IMP_LE], 94 (* goal 2 (of 3) *) 95 ASM_SIMP_TAC std_ss [REAL_ENTIRE, REAL_SUB_0, REAL_ARITH 96 ``((&1 - u) * x + u * y:real = x) <=> (u * (y - x) = 0)``] \\ 97 ASM_REAL_ARITH_TAC, 98 (* goal 3 (of 3) *) 99 REWRITE_TAC [dist, ABS_MUL, REAL_ARITH 100 ``((&1 - u) * x + u * y) - x:real = u * (y - x)``] \\ 101 ASM_SIMP_TAC std_ss [REAL_ARITH ``&0 < u ==> (abs u = u:real)``] \\ 102 MATCH_MP_TAC (REAL_ARITH ``x * 2 <= e /\ &0 < e ==> x < e:real``) \\ 103 ASM_SIMP_TAC real_ss [GSYM REAL_LE_RDIV_EQ, GSYM ABS_NZ, REAL_SUB_0] \\ 104 Q.UNABBREV_TAC `u` >> FULL_SIMP_TAC real_ss [min_def] ] 105QED 106 107val TRIVIAL_LIMIT_WITHIN_CONVEX = store_thm ("TRIVIAL_LIMIT_WITHIN_CONVEX", 108 ``!s x:real. 109 convex s /\ x IN s ==> (trivial_limit(at x within s) <=> (s = {x}))``, 110 SIMP_TAC std_ss [TRIVIAL_LIMIT_WITHIN, LIMPT_OF_CONVEX]); 111 112(* ------------------------------------------------------------------------- *) 113(* A general lemma. *) 114(* ------------------------------------------------------------------------- *) 115 116val CONVEX_CONNECTED = store_thm ("CONVEX_CONNECTED", 117 ``!s:real->bool. convex s ==> connected s``, 118 SIMP_TAC std_ss [CONVEX_ALT, connected, SUBSET_DEF, EXTENSION, IN_INTER, 119 IN_UNION, NOT_IN_EMPTY, NOT_FORALL_THM, NOT_EXISTS_THM] THEN 120 GEN_TAC THEN DISCH_TAC THEN REPEAT GEN_TAC THEN 121 CCONTR_TAC THEN FULL_SIMP_TAC std_ss [] THEN 122 MP_TAC(ISPECL [``\u. (&1 - u) * x + u * (x':real)``, 123 ``&0:real``, ``&1:real``, ``e1:real->bool``, ``e2:real->bool``] 124 (SIMP_RULE std_ss [GSYM open_def] CONNECTED_REAL_LEMMA)) THEN 125 ASM_SIMP_TAC real_ss [NOT_IMP, REAL_SUB_RZERO, REAL_MUL_LID, REAL_MUL_LZERO, 126 REAL_SUB_REFL, REAL_ADD_RID, REAL_ADD_LID, REAL_POS] THEN 127 REPEAT(CONJ_TAC THENL [ALL_TAC, ASM_MESON_TAC[]]) THEN 128 REPEAT STRIP_TAC THEN REWRITE_TAC[dist] THEN 129 SIMP_TAC real_ss [ABS_MUL, REAL_ARITH 130 ``((&1 - a) * x + a * y) - ((&1 - b) * x + b * y) = (a - b) * (y - x:real)``] THEN 131 MP_TAC(ISPEC ``(x' - x):real`` ABS_POS) THEN 132 REWRITE_TAC[REAL_LE_LT] THEN STRIP_TAC THENL 133 [ALL_TAC, METIS_TAC[REAL_MUL_RZERO, REAL_LT_01]] THEN 134 EXISTS_TAC ``e / abs((x' - x):real)`` THEN 135 ASM_SIMP_TAC real_ss [REAL_LT_RDIV_EQ, REAL_LT_DIV]); 136 137(* ------------------------------------------------------------------------- *) 138(* Explicit expressions for convexity in terms of arbitrary sums. *) 139(* ------------------------------------------------------------------------- *) 140 141Theorem CONVEX_SUM : 142 !s k u x:'a->real. 143 FINITE k /\ convex s /\ (sum k u = &1) /\ 144 (!i. i IN k ==> &0 <= u i /\ x i IN s) 145 ==> sum k (\i. u i * x i) IN s 146Proof 147 GEN_TAC THEN ASM_CASES_TAC ``convex(s:real->bool)`` THEN 148 ASM_SIMP_TAC std_ss [IMP_CONJ, RIGHT_FORALL_IMP_THM] THEN 149 ONCE_REWRITE_TAC [METIS [] 150 ``!k. (!u. (sum k u = 1) ==> 151 !x. (!i. i IN k ==> 0 <= u i /\ x i IN s) ==> 152 sum k (\i. u i * x i) IN s) = 153 (\k. !u. (sum k u = 1) ==> 154 !x. (!i. i IN k ==> 0 <= u i /\ x i IN s) ==> 155 sum k (\i. u i * x i) IN s) k``] THEN 156 MATCH_MP_TAC FINITE_INDUCT THEN BETA_TAC THEN 157 SIMP_TAC real_ss [SUM_CLAUSES, FORALL_IN_INSERT] THEN 158 SIMP_TAC std_ss [GSYM RIGHT_FORALL_IMP_THM] THEN 159 MAP_EVERY X_GEN_TAC [``k:'a->bool``, ``i:'a``, ``u:'a->real``, ``x:'a->real``] THEN 160 REWRITE_TAC[AND_IMP_INTRO] THEN STRIP_TAC THEN 161 ASM_CASES_TAC ``(u:'a->real) i = &1`` THENL 162 [ASM_REWRITE_TAC[REAL_ARITH ``(&1 + a = &1) <=> (a = &0:real)``] THEN 163 SUBGOAL_THEN ``sum k (\i:'a. u i * x(i):real) = 0`` 164 (fn th => ASM_SIMP_TAC std_ss [th, REAL_ADD_RID, REAL_MUL_LID]) THEN 165 MATCH_MP_TAC SUM_EQ_0 THEN SIMP_TAC std_ss [REAL_ENTIRE] THEN 166 REPEAT STRIP_TAC THEN DISJ1_TAC THEN 167 POP_ASSUM MP_TAC THEN SPEC_TAC (``x':'a``,``x':'a``) THEN 168 MATCH_MP_TAC SUM_POS_EQ_0 THEN ASM_SIMP_TAC std_ss [] THEN 169 POP_ASSUM MP_TAC THEN UNDISCH_TAC ``(u:'a->real) i + sum k u = 1`` THEN 170 REAL_ARITH_TAC, 171 FIRST_X_ASSUM(MP_TAC o SPEC ``(\j. (u:'a->real)(j) / (&1 - u(i)))``) THEN 172 ASM_REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 173 ASM_SIMP_TAC std_ss [SUM_LMUL, GSYM REAL_MUL_ASSOC] THEN 174 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN 175 REWRITE_TAC [real_div] THEN ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN 176 REWRITE_TAC [REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN 177 ASM_SIMP_TAC std_ss [SUM_LMUL] THEN 178 SUBGOAL_THEN ``&0:real < &1 - u(i:'a)`` ASSUME_TAC THENL 179 [ASM_MESON_TAC[SUM_POS_LE, REAL_ADD_SYM, REAL_ARITH 180 ``&0 <= a /\ &0 <= b /\ (b + a = &1) /\ ~(a = &1) ==> &0 < &1 - a:real``], 181 ALL_TAC] THEN 182 REWRITE_TAC[GSYM real_div] THEN 183 ASM_SIMP_TAC real_ss [REAL_LE_DIV, REAL_LT_IMP_LE] THEN 184 ASM_SIMP_TAC real_ss [REAL_EQ_LDIV_EQ, REAL_MUL_LID, REAL_EQ_SUB_LADD] THEN 185 DISCH_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 186 UNDISCH_TAC ``convex s`` THEN DISCH_TAC THEN 187 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [convex]) THEN 188 DISCH_THEN(MP_TAC o SPECL 189 [``sum k (\j. (u j / (&1 - u(i:'a))) * x(j) :real)``, 190 ``x(i:'a):real``, ``&1 - u(i:'a):real``, ``u(i:'a):real``]) THEN 191 REWRITE_TAC[real_div, REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 192 REWRITE_TAC[real_div, REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 193 ASM_SIMP_TAC std_ss [GSYM REAL_MUL_ASSOC, SUM_LMUL] THEN 194 REWRITE_TAC [REAL_MUL_ASSOC] THEN 195 SIMP_TAC real_ss [REAL_ARITH ``a * inv (1 - (u:'a->real) i) * b = 196 inv (1 - (u:'a->real) i) * a * b``] THEN 197 ASM_SIMP_TAC std_ss [GSYM REAL_MUL_ASSOC, SUM_LMUL] THEN 198 ASM_SIMP_TAC real_ss [REAL_MUL_ASSOC, REAL_MUL_RINV, REAL_LT_IMP_NE] THEN 199 REWRITE_TAC[REAL_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN 200 ASM_SIMP_TAC real_ss [REAL_LT_IMP_LE, SUM_LMUL] THEN 201 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[REAL_ADD_SYM]]); 202 203val CONVEX_INDEXED = store_thm ("CONVEX_INDEXED", 204 ``!s:real->bool. 205 convex s <=> 206 !k u x. (!i:num. 1 <= i /\ i <= k ==> &0 <= u(i) /\ x(i) IN s) /\ 207 (sum ((1:num)..k) u = &1) 208 ==> sum ((1:num)..k) (\i. u(i) * x(i)) IN s``, 209 REPEAT GEN_TAC THEN EQ_TAC THENL 210 [REPEAT STRIP_TAC THEN MATCH_MP_TAC CONVEX_SUM THEN 211 ASM_SIMP_TAC std_ss [IN_NUMSEG, FINITE_NUMSEG], 212 DISCH_TAC THEN REWRITE_TAC[convex] THEN 213 MAP_EVERY X_GEN_TAC [``x:real``, ``y:real``, ``u:real``, ``v:real``] THEN 214 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPEC ``2:num``) THEN 215 DISCH_THEN(MP_TAC o SPEC ``\n:num. if n = 1 then u else v:real``) THEN 216 DISCH_THEN(MP_TAC o SPEC ``\n:num. if n = 1 then x else y:real``) THEN 217 REWRITE_TAC [TWO, SUM_CLAUSES_NUMSEG, NUMSEG_SING, SUM_SING] THEN 218 SIMP_TAC arith_ss [] THEN METIS_TAC[]]); 219 220(* ------------------------------------------------------------------------- *) 221(* Convexity of general and special intervals. *) 222(* ------------------------------------------------------------------------- *) 223 224val IS_INTERVAL_CONVEX = store_thm ("IS_INTERVAL_CONVEX", 225 ``!s:real->bool. is_interval s ==> convex s``, 226 REWRITE_TAC[is_interval, convex] THEN 227 REPEAT STRIP_TAC THEN 228 KNOW_TAC ``x IN (s:real->bool) /\ y IN s ==> 229 x <= (u * x + v * y) /\ (u * x + v * y) <= y \/ 230 y <= (u * x + v * y) /\ (u * x + v * y) <= x`` THENL 231 [ALL_TAC, METIS_TAC []] THEN 232 ASM_SIMP_TAC std_ss [] THEN 233 DISJ_CASES_TAC(SPECL [``(x:real)``, ``(y:real)``] REAL_LE_TOTAL) THENL 234 [DISJ1_TAC, DISJ2_TAC] THEN 235 MATCH_MP_TAC(REAL_ARITH 236 ``&1 * a <= b /\ b <= &1 * c ==> a <= b /\ b <= c:real``) THEN 237 FIRST_X_ASSUM(SUBST1_TAC o SYM) THEN 238 ASM_SIMP_TAC real_ss [REAL_ADD_RDISTRIB] THEN 239 ASM_SIMP_TAC real_ss [REAL_LE_LMUL, REAL_LE_LADD, REAL_LE_RADD] THEN 240 CONJ_TAC THEN MATCH_MP_TAC REAL_LE_LMUL_IMP THEN ASM_REWRITE_TAC []); 241 242val IS_INTERVAL_CONNECTED = store_thm ("IS_INTERVAL_CONNECTED", 243 ``!s:real->bool. is_interval s ==> connected s``, 244 MESON_TAC[IS_INTERVAL_CONVEX, CONVEX_CONNECTED]); 245 246val IS_INTERVAL_CONNECTED_1 = store_thm ("IS_INTERVAL_CONNECTED_1", 247 ``!s:real->bool. is_interval s <=> connected s``, 248 GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[IS_INTERVAL_CONNECTED] THEN 249 ONCE_REWRITE_TAC[MONO_NOT_EQ] THEN 250 SIMP_TAC std_ss [IS_INTERVAL, connected, NOT_FORALL_THM, 251 LEFT_IMP_EXISTS_THM, NOT_IMP] THEN 252 MAP_EVERY X_GEN_TAC [``a:real``, ``b:real``, ``x:real``] THEN STRIP_TAC THEN 253 MAP_EVERY EXISTS_TAC [``{z:real | 1 * z < x}``, ``{z:real | 1 * z > x}``] THEN 254 REWRITE_TAC[OPEN_HALFSPACE_LT, OPEN_HALFSPACE_GT] THEN 255 SIMP_TAC arith_ss [SUBSET_DEF, EXTENSION, IN_UNION, IN_INTER, NOT_FORALL_THM, 256 real_gt, NOT_IN_EMPTY, GSPECIFICATION] THEN 257 SIMP_TAC real_ss [] THEN 258 REPEAT CONJ_TAC THENL [METIS_TAC[REAL_LT_TOTAL], 259 REAL_ARITH_TAC, EXISTS_TAC ``a:real``, EXISTS_TAC ``b:real``] THEN 260 ASM_REWRITE_TAC[REAL_LT_LE] THEN ASM_MESON_TAC[]); 261 262val CONVEX_INTERVAL = store_thm ("CONVEX_INTERVAL", 263 ``!a b:real. convex(interval [a,b]) /\ convex(interval (a,b))``, 264 METIS_TAC [IS_INTERVAL_CONVEX, IS_INTERVAL_INTERVAL]); 265 266 267(* ------------------------------------------------------------------------- *) 268(* On real, is_interval, convex and connected are all equivalent. *) 269(* ------------------------------------------------------------------------- *) 270 271val IS_INTERVAL_CONVEX_1 = store_thm ("IS_INTERVAL_CONVEX_1", 272 ``!s:real->bool. is_interval s <=> convex s``, 273 MESON_TAC[IS_INTERVAL_CONVEX, CONVEX_CONNECTED, IS_INTERVAL_CONNECTED_1]); 274 275(* ------------------------------------------------------------------------- *) 276(* *) 277(* ------------------------------------------------------------------------- *) 278 279val CONNECTED_COMPACT_INTERVAL_1 = store_thm ("CONNECTED_COMPACT_INTERVAL_1", 280 ``!s:real->bool. connected s /\ compact s <=> ?a b. s = interval[a,b]``, 281 REWRITE_TAC[GSYM IS_INTERVAL_CONNECTED_1, IS_INTERVAL_COMPACT]); 282 283(* ------------------------------------------------------------------------- *) 284(* *) 285(* ------------------------------------------------------------------------- *) 286 287val _ = set_fixity "convex_on" (Infix(NONASSOC, 450)); 288 289val convex_on = new_definition ("convex_on", 290 ``f convex_on s <=> 291 !x y u v:real. x IN s /\ y IN s /\ &0 <= u /\ &0 <= v /\ (u + v = &1) 292 ==> f(u * x + v * y) <= u * f(x) + v * f(y)``); 293 294Theorem REAL_CONVEX_BOUND2_LT : 295 !x y a b u v:real. x < a /\ y < b /\ &0 <= u /\ &0 <= v /\ (u + v = &1) 296 ==> u * x + v * y < u * a + v * b 297Proof 298 REPEAT GEN_TAC THEN ASM_CASES_TAC ``u = &0:real`` THENL 299 [ASM_REWRITE_TAC[REAL_MUL_LZERO, REAL_ADD_LID] THEN REPEAT STRIP_TAC, 300 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_ADD2 THEN 301 ASM_SIMP_TAC real_ss [REAL_LE_LMUL_IMP, REAL_LT_IMP_LE]] THEN 302 MATCH_MP_TAC REAL_LT_LMUL_IMP THEN ASM_REAL_ARITH_TAC 303QED 304 305val REAL_CONVEX_BOUND_LT = store_thm ("REAL_CONVEX_BOUND_LT", 306 ``!x y a u v:real. x < a /\ y < a /\ &0 <= u /\ &0 <= v /\ (u + v = &1) 307 ==> u * x + v * y < a``, 308 REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN 309 Q.EXISTS_TAC `u * a + v * a:real` THEN CONJ_TAC THENL 310 [ASM_SIMP_TAC real_ss [REAL_CONVEX_BOUND2_LT], 311 ALL_TAC] THEN 312 MATCH_MP_TAC REAL_EQ_IMP_LE THEN 313 UNDISCH_TAC ``u + v = &1:real`` THEN 314 SIMP_TAC real_ss [GSYM REAL_ADD_RDISTRIB]); 315 316val CONVEX_DISTANCE = store_thm ("CONVEX_DISTANCE", 317 ``!s a. (\x. dist(a,x)) convex_on s``, 318 SIMP_TAC std_ss [convex_on, dist] THEN REPEAT STRIP_TAC THEN 319 GEN_REWR_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [GSYM REAL_MUL_LID] THEN 320 FIRST_ASSUM(SUBST1_TAC o SYM) THEN 321 REWRITE_TAC[REAL_ARITH 322 ``(u + v) * z - (u * x + v * y) = u * (z - x) + v * (z - y:real)``] THEN 323 ASM_MESON_TAC[ABS_TRIANGLE, ABS_MUL, ABS_REFL]); 324 325val lemma = REWRITE_RULE[convex_on, IN_UNIV] 326 (ISPEC ``univ(:real)`` CONVEX_DISTANCE); 327 328val CONVEX_BALL = store_thm ("CONVEX_BALL", 329 ``!x:real e. convex(ball(x,e))``, 330 SIMP_TAC std_ss [convex, IN_BALL] THEN REPEAT STRIP_TAC THEN 331 ASM_MESON_TAC[REAL_LET_TRANS, REAL_CONVEX_BOUND_LT, lemma]); 332 333(* ------------------------------------------------------------------------- *) 334(* Derivatives. The definition is slightly tricky since we make it work over *) 335(* nets of a particular form. This lets us prove theorems generally and use *) 336(* "at a" or "at a within s" for restriction to a set (1-sided on R etc.) *) 337(* ------------------------------------------------------------------------- *) 338 339val _ = set_fixity "has_derivative" (Infix(NONASSOC, 450)); 340 341val has_derivative = new_definition ("has_derivative", 342 ``(f has_derivative f') net <=> 343 linear f' /\ 344 ((\y. inv(abs(y - netlimit net)) * 345 (f(y) - 346 (f(netlimit net) + f'(y - netlimit net)))) --> 0) net``); 347 348(* ------------------------------------------------------------------------- *) 349(* These are the only cases we'll care about, probably. *) 350(* ------------------------------------------------------------------------- *) 351 352val has_derivative_within = store_thm ("has_derivative_within", 353 ``!f:real->real f' x s. 354 (f has_derivative f') (at x within s) <=> 355 linear f' /\ 356 ((\y. inv(abs(y - x)) * (f(y) - (f(x) + f'(y - x)))) --> 0) 357 (at x within s)``, 358 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative] THEN AP_TERM_TAC THEN 359 ASM_CASES_TAC ``trivial_limit(at (x:real) within s)`` THENL 360 [ASM_REWRITE_TAC[LIM], ASM_SIMP_TAC std_ss [NETLIMIT_WITHIN]]); 361 362val has_derivative_at = store_thm ("has_derivative_at", 363 ``!f:real->real f' x. 364 (f has_derivative f') (at x) <=> 365 linear f' /\ 366 ((\y. inv(abs(y - x)) * (f(y) - (f(x) + f'(y - x)))) --> 0) 367 (at x)``, 368 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN 369 REWRITE_TAC[has_derivative_within]); 370 371(* ------------------------------------------------------------------------- *) 372(* More explicit epsilon-delta forms. *) 373(* ------------------------------------------------------------------------- *) 374 375Theorem HAS_DERIVATIVE_WITHIN : 376 !f f' x s. (f has_derivative f')(at x within s) <=> 377 linear f' /\ 378 !e. &0 < e 379 ==> ?d. &0 < d /\ 380 !x'. x' IN s /\ 381 &0 < abs(x' - x) /\ abs(x' - x) < d 382 ==> abs(f(x') - f(x) - f'(x' - x)) / 383 abs(x' - x) < e 384Proof 385 rpt GEN_TAC 386 >> SIMP_TAC std_ss [has_derivative_within, LIM_WITHIN] THEN AP_TERM_TAC 387 >> SIMP_TAC std_ss [dist, REAL_ARITH ``(x' - (x + d)) = x' - x - d:real``] 388 >> SIMP_TAC std_ss [real_div, REAL_SUB_RZERO, ABS_MUL] 389 >> SIMP_TAC std_ss [REAL_MUL_ASSOC, REAL_MUL_SYM, ABS_INV, ABS_ABS, REAL_LT_IMP_NE] 390QED 391 392Theorem HAS_DERIVATIVE_AT : 393 !f f' x. (f has_derivative f')(at x) <=> 394 linear f' /\ 395 !e. &0 < e 396 ==> ?d. &0 < d /\ 397 !x'. &0 < abs(x' - x) /\ abs(x' - x) < d 398 ==> abs(f(x') - f(x) - f'(x' - x)) / 399 abs(x' - x) < e 400Proof 401 ONCE_REWRITE_TAC [GSYM WITHIN_UNIV] 402 >> REWRITE_TAC [HAS_DERIVATIVE_WITHIN, IN_UNIV] 403QED 404 405Theorem HAS_DERIVATIVE_AT_WITHIN : 406 !f f' x s. (f has_derivative f') (at x) 407 ==> (f has_derivative f') (at x within s) 408Proof 409 REWRITE_TAC [HAS_DERIVATIVE_WITHIN, HAS_DERIVATIVE_AT] 410 >> MESON_TAC [] 411QED 412 413val HAS_DERIVATIVE_WITHIN_OPEN = store_thm ("HAS_DERIVATIVE_WITHIN_OPEN", 414 ``!f f' a s. 415 a IN s /\ open s 416 ==> ((f has_derivative f') (at a within s) <=> 417 (f has_derivative f') (at a))``, 418 SIMP_TAC std_ss [has_derivative_within, has_derivative_at, LIM_WITHIN_OPEN]); 419 420(* ------------------------------------------------------------------------- *) 421(* Combining theorems. *) 422(* ------------------------------------------------------------------------- *) 423 424val HAS_DERIVATIVE_LINEAR = store_thm ("HAS_DERIVATIVE_LINEAR", 425 ``!f net. linear f ==> (f has_derivative f) net``, 426 RW_TAC real_ss [has_derivative, real_sub] THEN 427 ASM_SIMP_TAC real_ss [GSYM LINEAR_ADD, GSYM LINEAR_CMUL, GSYM LINEAR_NEG] THEN 428 ASM_SIMP_TAC real_ss [REAL_ARITH ``a + -(b + (a + -b)) = 0:real``] THEN 429 ASM_SIMP_TAC real_ss [LINEAR_0, LIM_CONST]); 430 431val HAS_DERIVATIVE_ID = store_thm ("HAS_DERIVATIVE_ID", 432 ``!net. ((\x. x) has_derivative (\h. h)) net``, 433 SIMP_TAC real_ss [HAS_DERIVATIVE_LINEAR, LINEAR_ID]); 434 435val HAS_DERIVATIVE_CONST = store_thm ("HAS_DERIVATIVE_CONST", 436 ``!c net. ((\x. c) has_derivative (\h. 0)) net``, 437 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative, linear] THEN 438 SIMP_TAC real_ss [REAL_ADD_RID, REAL_SUB_REFL, REAL_MUL_RZERO, LIM_CONST]); 439 440val HAS_DERIVATIVE_CMUL = store_thm ("HAS_DERIVATIVE_CMUL", 441 ``!f f' net c. (f has_derivative f') net 442 ==> ((\x. c * f(x)) has_derivative (\h. c * f'(h))) net``, 443 REPEAT GEN_TAC THEN SIMP_TAC real_ss [has_derivative, LINEAR_COMPOSE_CMUL] THEN 444 DISCH_THEN(MP_TAC o SPEC ``c:real`` o MATCH_MP LIM_CMUL o CONJUNCT2) THEN 445 SIMP_TAC real_ss [REAL_MUL_RZERO] THEN MATCH_MP_TAC EQ_IMPLIES THEN 446 AP_THM_TAC THEN AP_THM_TAC THEN 447 AP_TERM_TAC THEN ABS_TAC THEN REAL_ARITH_TAC); 448 449val HAS_DERIVATIVE_NEG = store_thm ("HAS_DERIVATIVE_NEG", 450 ``!f f' net. (f has_derivative f') net 451 ==> ((\x. -(f(x))) has_derivative (\h. -(f'(h)))) net``, 452 ONCE_REWRITE_TAC[REAL_NEG_MINUS1] THEN 453 SIMP_TAC real_ss [HAS_DERIVATIVE_CMUL]); 454 455val HAS_DERIVATIVE_ADD = store_thm ("HAS_DERIVATIVE_ADD", 456 ``!f f' g g' net. 457 (f has_derivative f') net /\ (g has_derivative g') net 458 ==> ((\x. f(x) + g(x)) has_derivative (\h. f'(h) + g'(h))) net``, 459 REPEAT GEN_TAC THEN SIMP_TAC std_ss [has_derivative, LINEAR_COMPOSE_ADD] THEN 460 DISCH_THEN(MP_TAC o MATCH_MP (TAUT `(a /\ b) /\ (c /\ d) ==> b /\ d`)) THEN 461 DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN REWRITE_TAC[REAL_ADD_LID] THEN 462 MATCH_MP_TAC EQ_IMPLIES THEN SIMP_TAC std_ss [] THEN 463 AP_THM_TAC THEN AP_THM_TAC THEN 464 AP_TERM_TAC THEN ABS_TAC THEN REAL_ARITH_TAC); 465 466val HAS_DERIVATIVE_SUB = store_thm ("HAS_DERIVATIVE_SUB", 467 ``!f f' g g' net. 468 (f has_derivative f') net /\ (g has_derivative g') net 469 ==> ((\x. f(x) - g(x)) has_derivative (\h. f'(h) - g'(h))) net``, 470 SIMP_TAC real_ss [real_sub, HAS_DERIVATIVE_ADD, HAS_DERIVATIVE_NEG]); 471 472Theorem HAS_DERIVATIVE_SUM : 473 !f f' net s. FINITE s /\ (!a. a IN s ==> ((f a) has_derivative (f' a)) net) 474 ==> ((\x. sum s (\a. f a x)) has_derivative (\h. sum s (\a. f' a h))) net 475Proof 476 NTAC 3 GEN_TAC >> REWRITE_TAC [IMP_CONJ] 477 >> SET_INDUCT_TAC 478 >> ASM_SIMP_TAC std_ss [SUM_CLAUSES, HAS_DERIVATIVE_CONST] 479 >> rpt STRIP_TAC 480 >> ONCE_REWRITE_TAC [METIS [] ``sum s (\a. f a x) = (\x. sum s (\a. f a x)) x``] 481 >> MATCH_MP_TAC HAS_DERIVATIVE_ADD 482 >> SIMP_TAC std_ss [ETA_AX] >> ASM_SIMP_TAC std_ss [IN_INSERT] 483QED 484 485(* ------------------------------------------------------------------------- *) 486(* Limit transformation for derivatives. *) 487(* ------------------------------------------------------------------------- *) 488 489val HAS_DERIVATIVE_TRANSFORM_WITHIN = store_thm ("HAS_DERIVATIVE_TRANSFORM_WITHIN", 490 ``!f f' g x s d. 491 &0 < d /\ x IN s /\ 492 (!x'. x' IN s /\ dist (x',x) < d ==> (f x' = g x')) /\ 493 (f has_derivative f') (at x within s) 494 ==> (g has_derivative f') (at x within s)``, 495 REPEAT GEN_TAC THEN SIMP_TAC std_ss [has_derivative_within, IMP_CONJ] THEN 496 DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN DISCH_TAC THEN 497 MATCH_MP_TAC(REWRITE_RULE[TAUT `a /\ b /\ c ==> d <=> a /\ b ==> c ==> d`] 498 LIM_TRANSFORM_WITHIN) THEN 499 Q.EXISTS_TAC `d:real` THEN ASM_SIMP_TAC std_ss [DIST_REFL]); 500 501val HAS_DERIVATIVE_TRANSFORM_AT = store_thm ("HAS_DERIVATIVE_TRANSFORM_AT", 502 ``!f f' g x d. 503 &0 < d /\ (!x'. dist (x',x) < d ==> (f x' = g x')) /\ 504 (f has_derivative f') (at x) 505 ==> (g has_derivative f') (at x)``, 506 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN 507 MESON_TAC[HAS_DERIVATIVE_TRANSFORM_WITHIN, IN_UNIV]); 508 509(* ------------------------------------------------------------------------- *) 510(* Differentiability. *) 511(* ------------------------------------------------------------------------- *) 512 513val _ = set_fixity "differentiable" (Infix(NONASSOC, 450)); 514val _ = set_fixity "differentiable_on" (Infix(NONASSOC, 450)); 515 516val _ = hide "differentiable"; 517 518val differentiable = new_definition ("differentiable", 519 ``f differentiable net <=> ?f'. ((f has_derivative f') net)``); 520 521val differentiable_on = new_definition ("differentiable_on", 522 ``f differentiable_on s <=> !x. x IN s ==> f differentiable (at x within s)``); 523 524(* ------------------------------------------------------------------------- *) 525(* Frechet derivative and Jacobian matrix. *) 526(* ------------------------------------------------------------------------- *) 527 528val frechet_derivative = new_definition ("frechet_derivative", 529 ``frechet_derivative f net = @f'. (f has_derivative f') net``); 530 531val FRECHET_DERIVATIVE_WORKS = store_thm ("FRECHET_DERIVATIVE_WORKS", 532 ``!f net. f differentiable net <=> 533 (f has_derivative (frechet_derivative f net)) net``, 534 REPEAT GEN_TAC THEN REWRITE_TAC[frechet_derivative] THEN 535 CONV_TAC(RAND_CONV SELECT_CONV) THEN REWRITE_TAC[differentiable]); 536 537val LINEAR_FRECHET_DERIVATIVE = store_thm ("LINEAR_FRECHET_DERIVATIVE", 538 ``!f net. f differentiable net ==> linear(frechet_derivative f net)``, 539 SIMP_TAC std_ss [FRECHET_DERIVATIVE_WORKS, has_derivative]); 540 541(* ------------------------------------------------------------------------- *) 542(* Differentiability implies continuity. 377 *) 543(* ------------------------------------------------------------------------- *) 544 545val LIM_MUL_ABS_WITHIN = store_thm ("LIM_MUL_ABS_WITHIN", 546 ``!f a s. (f --> 0) (at a within s) 547 ==> ((\x. abs(x - a) * f(x)) --> 0) (at a within s)``, 548 REPEAT GEN_TAC THEN REWRITE_TAC[LIM_WITHIN] THEN 549 DISCH_TAC THEN GEN_TAC THEN POP_ASSUM (MP_TAC o Q.SPEC `e:real`) THEN 550 ASM_CASES_TAC ``&0 < e:real`` THEN ASM_REWRITE_TAC[dist, REAL_SUB_RZERO] THEN 551 DISCH_THEN(X_CHOOSE_THEN ``d:real`` STRIP_ASSUME_TAC) THEN 552 EXISTS_TAC ``min d (&1:real)`` THEN ASM_REWRITE_TAC[REAL_LT_MIN, REAL_LT_01] THEN 553 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [ABS_MUL, ABS_ABS] THEN 554 GEN_REWR_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN 555 ASM_SIMP_TAC std_ss [REAL_LT_MUL2, ABS_POS]); 556 557Theorem DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN : 558 !f:real->real x s. 559 f differentiable (at x within s) ==> f continuous (at x within s) 560Proof 561 REWRITE_TAC[differentiable, has_derivative_within, CONTINUOUS_WITHIN] THEN 562 REPEAT GEN_TAC THEN 563 DISCH_THEN(X_CHOOSE_THEN ``f':real->real`` MP_TAC) THEN 564 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o MATCH_MP LIM_MUL_ABS_WITHIN) THEN 565 SUBGOAL_THEN 566 ``((f':real->real) o (\y. y - x)) continuous (at x within s)`` 567 MP_TAC THENL 568 [MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN 569 ASM_SIMP_TAC std_ss [LINEAR_CONTINUOUS_WITHIN] THEN 570 SIMP_TAC std_ss [CONTINUOUS_SUB, CONTINUOUS_CONST, CONTINUOUS_WITHIN_ID], 571 ALL_TAC] THEN 572 SIMP_TAC std_ss [CONTINUOUS_WITHIN, o_DEF] THEN 573 ASM_REWRITE_TAC[REAL_MUL_ASSOC, AND_IMP_INTRO, IN_UNIV] THEN 574 DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN 575 SIMP_TAC std_ss [LIM_WITHIN, GSYM DIST_NZ, REAL_MUL_RINV, ABS_ZERO, 576 REAL_ARITH ``(x - y = 0) <=> (x = y:real)``, 577 REAL_MUL_LID, REAL_SUB_REFL] THEN 578 FIRST_ASSUM(SUBST1_TAC o MATCH_MP LINEAR_0) THEN 579 REWRITE_TAC[dist, REAL_SUB_RZERO, REAL_ADD_ASSOC] THEN 580 SIMP_TAC std_ss [REAL_ARITH ``(a + (b - (c + a))) - (0 + 0) = b - c:real``] 581QED 582 583val DIFFERENTIABLE_IMP_CONTINUOUS_AT = store_thm ("DIFFERENTIABLE_IMP_CONTINUOUS_AT", 584 ``!f:real->real x. f differentiable (at x) ==> f continuous (at x)``, 585 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN 586 REWRITE_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]); 587 588val DIFFERENTIABLE_IMP_CONTINUOUS_ON = store_thm ("DIFFERENTIABLE_IMP_CONTINUOUS_ON", 589 ``!f:real->real s. f differentiable_on s ==> f continuous_on s``, 590 SIMP_TAC std_ss [differentiable_on, CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN, 591 DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]); 592 593Theorem HAS_DERIVATIVE_WITHIN_SUBSET : 594 !f f' s t x. (f has_derivative f') (at x within s) /\ t SUBSET s 595 ==> (f has_derivative f') (at x within t) 596Proof 597 REWRITE_TAC[has_derivative_within] THEN MESON_TAC[LIM_WITHIN_SUBSET] 598QED 599 600Theorem DIFFERENTIABLE_WITHIN_SUBSET : 601 !f:real->real s t x. 602 f differentiable (at x within t) /\ s SUBSET t 603 ==> f differentiable (at x within s) 604Proof 605 REWRITE_TAC[differentiable] THEN MESON_TAC[HAS_DERIVATIVE_WITHIN_SUBSET] 606QED 607 608val DIFFERENTIABLE_ON_SUBSET = store_thm ("DIFFERENTIABLE_ON_SUBSET", 609 ``!f:real->real s t. 610 f differentiable_on t /\ s SUBSET t ==> f differentiable_on s``, 611 REWRITE_TAC[differentiable_on] THEN 612 MESON_TAC[SUBSET_DEF, DIFFERENTIABLE_WITHIN_SUBSET]); 613 614val DIFFERENTIABLE_ON_EMPTY = store_thm ("DIFFERENTIABLE_ON_EMPTY", 615 ``!f. f differentiable_on {}``, 616 REWRITE_TAC[differentiable_on, NOT_IN_EMPTY]); 617 618(* ------------------------------------------------------------------------- *) 619(* Several results are easier using a "multiplied-out" variant. *) 620(* (I got this idea from Dieudonne's proof of the chain rule). *) 621(* ------------------------------------------------------------------------- *) 622 623val HAS_DERIVATIVE_WITHIN_ALT = store_thm ("HAS_DERIVATIVE_WITHIN_ALT", 624 ``!f:real->real f' s x. 625 (f has_derivative f') (at x within s) <=> 626 linear f' /\ 627 !e. &0 < e 628 ==> ?d. &0 < d /\ 629 !y. y IN s /\ abs(y - x) < d 630 ==> abs(f(y) - f(x) - f'(y - x)) <= 631 e * abs(y - x)``, 632 REPEAT GEN_TAC THEN REWRITE_TAC[has_derivative_within, LIM_WITHIN] THEN 633 ASM_REWRITE_TAC[dist, REAL_SUB_RZERO] THEN 634 ASM_CASES_TAC ``linear(f':real->real)`` THEN 635 ASM_REWRITE_TAC [ABS_MUL, ABS_INV, ABS_ABS] THEN 636 GEN_REWR_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_SYM] THEN 637 SIMP_TAC std_ss [GSYM real_div, REAL_LT_LDIV_EQ] THEN 638 REWRITE_TAC[REAL_ARITH ``a - (b + c) = a - b - c :real``] THEN 639 EQ_TAC THEN DISCH_TAC THEN X_GEN_TAC ``e:real`` THEN DISCH_TAC THENL 640 [FIRST_X_ASSUM(MP_TAC o SPEC ``e:real``) THEN ASM_REWRITE_TAC[] THEN 641 STRIP_TAC THEN EXISTS_TAC ``d:real`` THEN 642 ASM_REWRITE_TAC[] THEN X_GEN_TAC ``y:real`` THEN DISCH_TAC THEN 643 ASM_CASES_TAC ``&0 < abs(y - x :real)`` THENL 644 [ASM_SIMP_TAC std_ss [GSYM REAL_LE_LDIV_EQ] THEN 645 FULL_SIMP_TAC std_ss [REAL_LT_IMP_NE, REAL_LE_LT, ABS_DIV, ABS_ABS], 646 ALL_TAC] THEN 647 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [GSYM ABS_NZ]) THEN 648 ASM_SIMP_TAC std_ss [REAL_SUB_0, REAL_SUB_REFL, ABS_0, REAL_MUL_RZERO, 649 REAL_ARITH ``0 - x = -x:real``, ABS_NEG] THEN 650 ASM_MESON_TAC[LINEAR_0, ABS_0, REAL_LE_REFL], 651 FIRST_X_ASSUM(MP_TAC o SPEC ``e / &2:real``) THEN 652 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT] THEN 653 STRIP_TAC THEN EXISTS_TAC ``d:real`` THEN 654 ASM_REWRITE_TAC[] THEN X_GEN_TAC ``y:real`` THEN STRIP_TAC THEN 655 ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE, ABS_DIV, ABS_ABS, REAL_LT_LDIV_EQ] THEN 656 MATCH_MP_TAC REAL_LET_TRANS THEN 657 EXISTS_TAC ``e / &2 * abs(y - x :real)`` THEN 658 ASM_SIMP_TAC arith_ss [REAL_LT_RMUL, REAL_LT_LDIV_EQ, REAL_LT] THEN 659 UNDISCH_TAC ``&0 < e:real`` THEN REAL_ARITH_TAC]); 660 661val HAS_DERIVATIVE_AT_ALT = store_thm ("HAS_DERIVATIVE_AT_ALT", 662 ``!f:real->real f' x. 663 (f has_derivative f') (at x) <=> 664 linear f' /\ 665 !e. &0 < e 666 ==> ?d. &0 < d /\ 667 !y. abs(y - x) < d 668 ==> abs(f(y) - f(x) - f'(y - x)) <= e * abs(y - x)``, 669 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN 670 REWRITE_TAC[HAS_DERIVATIVE_WITHIN_ALT, IN_UNIV]); 671 672(* ------------------------------------------------------------------------- *) 673(* The chain rule. 499 *) 674(* ------------------------------------------------------------------------- *) 675 676val DIFF_CHAIN_WITHIN = store_thm ("DIFF_CHAIN_WITHIN", 677 ``!f:real->real g:real->real f' g' x s. 678 (f has_derivative f') (at x within s) /\ 679 (g has_derivative g') (at (f x) within (IMAGE f s)) 680 ==> ((g o f) has_derivative (g' o f'))(at x within s)``, 681 REPEAT GEN_TAC THEN SIMP_TAC std_ss [HAS_DERIVATIVE_WITHIN_ALT, LINEAR_COMPOSE] THEN 682 DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN 683 FIRST_ASSUM(X_CHOOSE_TAC ``B1:real`` o MATCH_MP LINEAR_BOUNDED_POS) THEN 684 DISCH_THEN(fn th => X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN MP_TAC th) THEN 685 DISCH_THEN(CONJUNCTS_THEN2 686 (fn th => ASSUME_TAC th THEN X_CHOOSE_TAC ``B2:real`` (MATCH_MP 687 LINEAR_BOUNDED_POS th)) MP_TAC) THEN 688 FIRST_X_ASSUM(fn th => MP_TAC th THEN MP_TAC(Q.SPEC `e / &2 / B2` th)) THEN 689 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT] THEN 690 DISCH_THEN(X_CHOOSE_THEN ``d1:real`` STRIP_ASSUME_TAC) THEN DISCH_TAC THEN 691 DISCH_THEN(MP_TAC o Q.SPEC `e / &2 / (&1 + B1)`) THEN 692 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT, REAL_LT_ADD] THEN 693 DISCH_THEN(X_CHOOSE_THEN ``de:real`` STRIP_ASSUME_TAC) THEN 694 UNDISCH_TAC ``!e:real. 0 < e ==> 695 ?d. 0 < d /\ 696 !y. y IN s /\ abs (y - x) < d ==> 697 abs (f y - f x - f' (y - x)) <= e * abs (y - x)`` THEN 698 DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o Q.SPEC `&1`) THEN 699 REWRITE_TAC[REAL_LT_01, REAL_MUL_LID] THEN 700 DISCH_THEN(X_CHOOSE_THEN ``d2:real`` STRIP_ASSUME_TAC) THEN 701 MP_TAC(SPECL [``d1:real``, ``d2:real``] REAL_DOWN2) THEN 702 ASM_SIMP_TAC std_ss [REAL_LT_DIV, REAL_LT_ADD, REAL_LT_01] THEN 703 DISCH_THEN(X_CHOOSE_THEN ``d0:real`` STRIP_ASSUME_TAC) THEN 704 MP_TAC(SPECL [``d0:real``, ``de / (B1 + &1:real)``] REAL_DOWN2) THEN 705 ASM_SIMP_TAC std_ss [REAL_LT_DIV, REAL_LT_ADD, REAL_LT_01] THEN 706 DISCH_THEN (X_CHOOSE_TAC ``d:real``) THEN Q.EXISTS_TAC `d` THEN 707 POP_ASSUM MP_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 708 X_GEN_TAC ``y:real`` THEN DISCH_TAC THEN UNDISCH_TAC 709 ``!y. y IN s /\ abs(y - x) < d2 710 ==> abs((f:real->real) y - f x - f'(y - x)) <= abs(y - x)`` THEN 711 DISCH_THEN(MP_TAC o SPEC ``y:real``) THEN 712 Q_TAC SUFF_TAC `y IN s /\ abs (y - x) < d2` THENL 713 [DISCH_TAC, ASM_MESON_TAC[REAL_LT_TRANS]] THEN 714 ASM_REWRITE_TAC [] THEN DISCH_TAC THEN 715 UNDISCH_TAC ``!y. y IN s /\ abs (y - x) < d1 ==> 716 abs (f y - f x - f' (y - x)) <= e / 2 / B2 * abs (y - x:real)`` THEN 717 DISCH_THEN(MP_TAC o SPEC ``y:real``) THEN 718 Q_TAC SUFF_TAC `y IN s /\ abs (y - x) < d1` THENL 719 [DISCH_TAC, ASM_MESON_TAC[REAL_LT_TRANS]] THEN 720 ASM_REWRITE_TAC [] THEN DISCH_TAC THEN 721 FIRST_X_ASSUM(MP_TAC o SPEC ``(f:real->real) y``) THEN 722 ASM_SIMP_TAC std_ss [] THEN 723 Q_TAC SUFF_TAC `f y IN IMAGE f s /\ abs (f y - f x) < de` THENL 724 [DISCH_TAC, 725 CONJ_TAC THENL [ASM_MESON_TAC[IN_IMAGE], ALL_TAC] THEN 726 MATCH_MP_TAC REAL_LET_TRANS THEN Q.EXISTS_TAC 727 `abs(f'(y - x)) + abs((f:real->real) y - f x - f'(y - x))` THEN 728 REWRITE_TAC[ABS_TRIANGLE_SUB] THEN 729 MATCH_MP_TAC REAL_LET_TRANS THEN 730 EXISTS_TAC ``B1 * abs(y - x) + abs(y - x :real)`` THEN 731 ASM_SIMP_TAC real_ss [REAL_LE_ADD2] THEN 732 REWRITE_TAC[REAL_ARITH ``a * x + x = x * (a + &1:real)``] THEN 733 ASM_SIMP_TAC real_ss [GSYM REAL_LT_RDIV_EQ, REAL_LT_ADD, REAL_LT_01] THEN 734 ASM_MESON_TAC[REAL_LT_TRANS]] THEN 735 ASM_REWRITE_TAC [] THEN DISCH_TAC THEN 736 REWRITE_TAC[o_THM] THEN MATCH_MP_TAC REAL_LE_TRANS THEN 737 Q.EXISTS_TAC `abs((g:real->real)(f(y:real)) - g(f x) - g'(f y - f x)) + 738 abs((g(f y) - g(f x) - g'(f'(y - x))) - 739 (g(f y) - g(f x) - g'(f y - f x)))` THEN 740 REWRITE_TAC[ABS_TRIANGLE_SUB] THEN 741 REWRITE_TAC[REAL_ARITH ``(a - b - c1) - (a - b - c2) = c2 - c1:real``] THEN 742 ASM_SIMP_TAC std_ss [GSYM LINEAR_SUB] THEN 743 FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH 744 ``a <= d ==> b <= ee - d ==> a + b <= ee:real``)) THEN 745 MATCH_MP_TAC REAL_LE_TRANS THEN 746 Q.EXISTS_TAC `B2 * abs((f:real->real) y - f x - f'(y - x))` THEN 747 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN 748 Q.EXISTS_TAC `B2 * e / &2 / B2 * abs(y - x :real)` THEN 749 CONJ_TAC THENL 750 [SIMP_TAC std_ss [real_div] THEN 751 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d * e = a * ((b * c * d) * e:real)``] THEN 752 MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_SIMP_TAC std_ss [GSYM real_div, REAL_LE_REFL] THEN 753 ASM_SIMP_TAC std_ss [REAL_LT_IMP_LE, ABS_POS], 754 ALL_TAC] THEN 755 ASM_SIMP_TAC real_ss [REAL_LE_LMUL, REAL_LT_IMP_LE] THEN REWRITE_TAC[real_div] THEN 756 ONCE_REWRITE_TAC[REAL_ARITH 757 ``b * e * h * b' * x <= e * x - d <=> 758 d <= e * (&1 - h * (b' * b)) * x:real``] THEN 759 ASM_SIMP_TAC real_ss [REAL_MUL_LINV, REAL_LT_IMP_NE] THEN 760 SIMP_TAC real_ss [ONE_MINUS_HALF, REAL_INV_1OVER] THEN 761 REWRITE_TAC[GSYM REAL_MUL_ASSOC, GSYM REAL_INV_1OVER] THEN 762 ASM_SIMP_TAC arith_ss [REAL_LE_LMUL, REAL_LT_DIV, REAL_LT] THEN 763 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN 764 ASM_SIMP_TAC real_ss [REAL_LE_LDIV_EQ, REAL_LT_ADD, REAL_LT_01] THEN 765 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[GSYM real_div] THEN 766 ASM_SIMP_TAC real_ss [REAL_LE_LDIV_EQ, REAL_LT_ADD, REAL_LT_01] THEN 767 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC 768 ``abs(f'(y - x)) + abs((f:real->real) y - f x - f'(y - x))`` THEN 769 REWRITE_TAC[ABS_TRIANGLE_SUB] THEN SIMP_TAC real_ss [real_div, REAL_MUL_ASSOC] THEN 770 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = (c * a) * b * d:real``] THEN 771 SIMP_TAC real_ss [REAL_MUL_LINV] THEN MATCH_MP_TAC(REAL_ARITH 772 ``u <= x * b /\ v <= b ==> u + v <= b * (&1 + x:real)``) THEN 773 ASM_REWRITE_TAC[]); 774 775(* ------------------------------------------------------------------------- *) 776(* Component of the differential must be zero if it exists at a local *) 777(* maximum or minimum for that corresponding component. Start with slightly *) 778(* sharper forms that fix the sign of the derivative on the boundary. *) 779(* ------------------------------------------------------------------------- *) 780 781Theorem DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM : 782 !f:real->real f' x s e. 783 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\ 784 &0 < e /\ (!w. w IN s INTER ball(x,e) ==> (f x) <= (f w)) 785 ==> !y. y IN s ==> &0 <= (f'(y - x)) 786Proof 787 REWRITE_TAC[has_derivative_within] THEN REPEAT STRIP_TAC THEN 788 ASM_CASES_TAC ``y:real = x`` THENL 789 [ASM_MESON_TAC[REAL_SUB_REFL, LINEAR_0, REAL_LE_REFL], 790 ALL_TAC] THEN 791 ONCE_REWRITE_TAC[GSYM REAL_NOT_LT] THEN DISCH_TAC THEN 792 UNDISCH_TAC ``((\y. inv (abs (y - x)) * (f y - (f x + f' (y - x)))) --> 0) 793 (at x within s)`` THEN REWRITE_TAC [LIM_WITHIN] THEN 794 DISCH_THEN(MP_TAC o Q.SPEC `-((f':real->real)(y - x)) / abs(y - x)`) THEN 795 ASM_SIMP_TAC real_ss [REAL_LT_DIV, GSYM ABS_NZ, real_sub, 796 NOT_EXISTS_THM, REAL_ARITH ``&0 < -x <=> x < &0:real``] THEN 797 CONJ_TAC THENL 798 [ONCE_REWRITE_TAC [GSYM REAL_LT_NEG] THEN SIMP_TAC real_ss [REAL_NEG_0, real_div] THEN 799 SIMP_TAC std_ss [GSYM real_sub, GSYM real_div] THEN 800 Q_TAC SUFF_TAC `0 < abs (y - x:real)` THENL 801 [DISCH_TAC, 802 REWRITE_TAC [GSYM ABS_NZ] THEN POP_ASSUM MP_TAC THEN 803 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC] THEN 804 ASM_SIMP_TAC real_ss [REAL_LT_LDIV_EQ], 805 ALL_TAC] THEN 806 X_GEN_TAC ``d:real`` THEN CCONTR_TAC THEN FULL_SIMP_TAC std_ss [] THEN 807 Q.ABBREV_TAC `de = min (&1) ((min d e) / &2 / abs(y - x:real))` THEN 808 FIRST_X_ASSUM (MP_TAC o Q.SPEC `x + de * (y - x):real`) THEN 809 SIMP_TAC real_ss [dist, REAL_ADD_SUB, NOT_IMP, GSYM CONJ_ASSOC] THEN 810 SUBGOAL_THEN ``abs(de * (y - x):real) < min d e`` MP_TAC THENL 811 [ASM_SIMP_TAC real_ss [ABS_MUL, GSYM REAL_LT_RDIV_EQ, 812 ABS_POS, real_sub] THEN 813 Q.UNABBREV_TAC `de` THEN SIMP_TAC real_ss [real_div, REAL_MUL_ASSOC] THEN 814 SIMP_TAC std_ss [min_def] THEN REPEAT COND_CASES_TAC THENL 815 [FULL_SIMP_TAC real_ss [GSYM real_sub] THEN MATCH_MP_TAC REAL_LET_TRANS THEN 816 Q.EXISTS_TAC `d / 2` THEN ASM_SIMP_TAC std_ss [REAL_LT_HALF2] THEN 817 Q_TAC SUFF_TAC `0 < abs (y - x:real)` THENL 818 [DISCH_TAC, REWRITE_TAC [GSYM ABS_NZ] THEN 819 UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC] THEN 820 GEN_REWR_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN 821 ASM_SIMP_TAC real_ss [GSYM REAL_LE_RDIV_EQ, real_div], 822 FULL_SIMP_TAC real_ss [GSYM real_sub] THEN MATCH_MP_TAC REAL_LET_TRANS THEN 823 Q.EXISTS_TAC `e / 2` THEN ASM_SIMP_TAC std_ss [REAL_LT_HALF2] THEN 824 Q_TAC SUFF_TAC `0 < abs (y - x:real)` THENL 825 [DISCH_TAC, REWRITE_TAC [GSYM ABS_NZ] THEN 826 UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC] THEN 827 GEN_REWR_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN 828 ASM_SIMP_TAC real_ss [GSYM REAL_LE_RDIV_EQ, real_div], 829 SIMP_TAC real_ss [ABS_MUL] THEN 830 `y - x <> 0` by (UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC) THEN 831 ASM_SIMP_TAC std_ss [GSYM ABS_INV, ABS_ABS] THEN 832 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = (a * b) * (c * d:real)``] THEN 833 ASM_SIMP_TAC real_ss [GSYM ABS_MUL, REAL_MUL_LINV, GSYM real_sub] THEN 834 SIMP_TAC real_ss [GSYM real_div] THEN Q_TAC SUFF_TAC `abs (d / 2) = d / 2` THENL 835 [ASM_SIMP_TAC real_ss [REAL_LT_HALF2], ALL_TAC] THEN 836 ASM_SIMP_TAC real_ss [ABS_REFL, REAL_LE_RDIV_EQ, REAL_LE_LT], 837 ALL_TAC] THEN 838 SIMP_TAC real_ss [ABS_MUL] THEN 839 `y - x <> 0` by (UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC) THEN 840 ASM_SIMP_TAC std_ss [GSYM ABS_INV, ABS_ABS] THEN 841 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = (a * b) * (c * d:real)``] THEN 842 ASM_SIMP_TAC real_ss [GSYM ABS_MUL, REAL_MUL_LINV, GSYM real_sub] THEN 843 SIMP_TAC std_ss [GSYM real_div] THEN Q_TAC SUFF_TAC `abs (e / 2) = e / 2` THENL 844 [ASM_SIMP_TAC real_ss [REAL_LT_HALF2], ALL_TAC] THEN 845 ASM_SIMP_TAC real_ss [ABS_REFL, REAL_LE_RDIV_EQ, REAL_LE_LT], 846 ALL_TAC] THEN 847 REWRITE_TAC[REAL_LT_MIN] THEN STRIP_TAC THEN 848 SUBGOAL_THEN ``&0 < de /\ de <= &1:real`` STRIP_ASSUME_TAC THENL 849 [Q.UNABBREV_TAC `de` THEN CONJ_TAC THENL [ALL_TAC, SIMP_TAC std_ss [REAL_MIN_LE1]] THEN 850 ASM_SIMP_TAC real_ss [REAL_LT_MIN, REAL_LT_01, REAL_HALF, REAL_LT_DIV, ABS_NZ, real_sub] THEN 851 SIMP_TAC real_ss [real_div, min_def] THEN 852 Q_TAC SUFF_TAC `0 < abs (y - x:real)` THENL 853 [DISCH_TAC, REWRITE_TAC [GSYM ABS_NZ] THEN 854 UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC] THEN COND_CASES_TAC THENL 855 [ASM_SIMP_TAC std_ss [REAL_LT_RDIV_EQ, GSYM real_div, GSYM real_sub] THEN 856 ASM_SIMP_TAC real_ss [REAL_LT_HALF2], 857 ALL_TAC] THEN 858 ASM_SIMP_TAC std_ss [REAL_LT_RDIV_EQ, GSYM real_div, GSYM real_sub] THEN 859 ASM_SIMP_TAC real_ss [REAL_LT_HALF2], 860 ALL_TAC] THEN 861 MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL 862 [REWRITE_TAC[REAL_ARITH 863 ``x + a * (y - x):real = (&1 - a) * x + a * y``] THEN 864 MATCH_MP_TAC IN_CONVEX_SET THEN ASM_SIMP_TAC real_ss [REAL_LT_IMP_LE], 865 DISCH_TAC] THEN 866 CONJ_TAC THENL 867 [SIMP_TAC std_ss [ABS_MUL] THEN MATCH_MP_TAC REAL_LT_MUL THEN 868 UNDISCH_TAC ``0 < de:real`` THEN UNDISCH_TAC ``y <> x:real`` THEN 869 REAL_ARITH_TAC, ALL_TAC] THEN ASM_REWRITE_TAC[] THEN 870 SIMP_TAC std_ss [REAL_NOT_LT, ABS_MUL] THEN 871 ONCE_REWRITE_TAC [REAL_ARITH ``a + b + -a = b:real``] THEN 872 Q_TAC SUFF_TAC `abs (de * (y - x)) <> 0` THENL 873 [DISCH_TAC, SIMP_TAC std_ss [ABS_MUL] THEN 874 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN 875 MATCH_MP_TAC REAL_LT_MUL THEN ASM_SIMP_TAC real_ss [GSYM ABS_NZ] THEN 876 ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE] THEN UNDISCH_TAC ``y <> x:real`` THEN 877 REAL_ARITH_TAC] THEN 878 ASM_SIMP_TAC std_ss [ABS_INV, ABS_ABS] THEN 879 `y - x <> 0` by (UNDISCH_TAC ``y <> x:real`` THEN REAL_ARITH_TAC) THEN 880 `0 < abs (y - x)` by (ASM_SIMP_TAC std_ss [GSYM ABS_NZ]) THEN 881 ASM_SIMP_TAC std_ss [REAL_LE_LDIV_EQ, GSYM real_sub] THEN 882 `abs (y - x) <> 0` by ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE] THEN 883 `de <> 0` by (ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE]) THEN 884 `0 < abs (de)` by (ASM_SIMP_TAC std_ss [GSYM ABS_NZ]) THEN 885 `abs (de) <> 0` by ASM_SIMP_TAC std_ss [REAL_LT_IMP_NE] THEN 886 ASM_SIMP_TAC real_ss [REAL_INV_MUL, ABS_MUL] THEN 887 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = (a * c) * (b * d:real)``] THEN 888 ASM_SIMP_TAC real_ss [REAL_MUL_LINV] THEN 889 Q_TAC SUFF_TAC `x + de * (y - x) IN ball (x,e)` THENL 890 [DISCH_TAC, SIMP_TAC real_ss [IN_BALL, dist] THEN 891 UNDISCH_TAC ``abs (de * (y - x)) < e:real`` THEN REAL_ARITH_TAC] THEN 892 `f x <= f (x + de * (y - x))` by METIS_TAC [IN_INTER] THEN 893 Q_TAC SUFF_TAC `abs (f (x + de * (y - x)) - (f x + f' (de * (y - x)))) = 894 (f (x + de * (y - x)) - (f x + f' (de * (y - x))))` THENL 895 [DISC_RW_KILL, 896 REWRITE_TAC [ABS_REFL] THEN 897 ONCE_REWRITE_TAC [REAL_ARITH ``a - (b + c) = (a - b) + -c:real``] THEN 898 MATCH_MP_TAC REAL_LE_ADD THEN 899 ASM_SIMP_TAC real_ss [REAL_ARITH ``a <= b ==> 0 <= b - a:real``] THEN 900 ASM_SIMP_TAC real_ss [LINEAR_CMUL] THEN 901 ONCE_REWRITE_TAC [REAL_ARITH ``-(a * b) = a * -b:real``] THEN 902 MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC std_ss [REAL_LE_LT] THEN 903 ONCE_REWRITE_TAC [GSYM REAL_LT_NEG] THEN ASM_SIMP_TAC real_ss []] THEN 904 ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN REWRITE_TAC [GSYM real_div] THEN 905 ASM_SIMP_TAC real_ss [REAL_LE_RDIV_EQ] THEN ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN 906 `0 <= de` by ASM_SIMP_TAC real_ss [REAL_LE_LT] THEN 907 POP_ASSUM (ASSUME_TAC o REWRITE_RULE [GSYM ABS_REFL]) THEN 908 ASM_SIMP_TAC real_ss [GSYM LINEAR_CMUL] THEN 909 GEN_REWR_TAC (LAND_CONV o ONCE_DEPTH_CONV) [REAL_MUL_COMM] THEN 910 ONCE_REWRITE_TAC [REAL_ARITH ``-a <= b - (c + a) <=> c <= b:real``] THEN 911 METIS_TAC [REAL_MUL_COMM] 912QED 913 914val DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM = store_thm ("DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM", 915 ``!f:real->real f' x s e. 916 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\ 917 &0 < e /\ (!w. w IN s INTER ball(x,e) ==> (f w) <= (f x)) 918 ==> !y. y IN s ==> (f'(y - x)) <= &0``, 919 REPEAT STRIP_TAC THEN 920 MP_TAC(ISPECL [ 921 ``\x. -((f:real->real) x)``, ``\x. -((f':real->real) x)``, 922 ``x:real``, ``s:real->bool``, ``e:real``] 923 DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM) THEN 924 ASM_SIMP_TAC real_ss [HAS_DERIVATIVE_NEG] THEN 925 ASM_SIMP_TAC real_ss [REAL_LE_NEG2, REAL_NEG_GE0]); 926 927val CONVEX_CBALL = store_thm ("CONVEX_CBALL", 928 ``!x:real e. convex(cball(x,e))``, 929 REWRITE_TAC[convex, IN_CBALL, dist] THEN MAP_EVERY X_GEN_TAC 930 [``x:real``, ``e:real``, ``y:real``, ``z:real``, ``u:real``, ``v:real``] THEN 931 STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH ``a - b = &1 * a - b:real``] THEN 932 FIRST_ASSUM(SUBST1_TAC o SYM) THEN 933 REWRITE_TAC[REAL_ARITH 934 ``(a + b) * x - (a * y + b * z) = a * (x - y) + b * (x - z:real)``] THEN 935 MATCH_MP_TAC REAL_LE_TRANS THEN 936 EXISTS_TAC ``abs(u * (x - y)) + abs(v * (x - z):real)`` THEN 937 REWRITE_TAC[ABS_TRIANGLE, ABS_MUL] THEN 938 MATCH_MP_TAC REAL_CONVEX_BOUND_LE THEN ASM_REWRITE_TAC[REAL_ABS_POS] THEN 939 ASM_SIMP_TAC real_ss [REAL_ARITH 940 ``&0 <= u /\ &0 <= v /\ (u + v = &1) ==> (abs(u) + abs(v) = &1:real)``]); 941 942Theorem DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN : 943 !f:real->real f' x s. 944 x IN s /\ open s /\ (f has_derivative f') (at x) /\ 945 ((!w. w IN s ==> (f w) <= (f x)) \/ 946 (!w. w IN s ==> (f x) <= (f w))) ==> !h. (f' h) = &0 947Proof 948 rpt GEN_TAC 949 >> DISCH_THEN (REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) 950 >> Q.PAT_ASSUM `open s` 951 (MP_TAC o ONCE_REWRITE_RULE [OPEN_CONTAINS_CBALL]) 952 >> DISCH_THEN(MP_TAC o Q.SPEC `x:real`) >> art [SUBSET_DEF] 953 >> DISCH_THEN(X_CHOOSE_THEN ``e:real`` STRIP_ASSUME_TAC) 954 >> FIRST_X_ASSUM DISJ_CASES_TAC (* 2 subgoals, shared tactics *) 955 >| [ MP_TAC (Q.SPECL [`f`, `f'`, `x`, `cball(x:real,e)`, `e`] 956 DIFFERENTIAL_COMPONENT_NEG_AT_MAXIMUM), 957 MP_TAC (Q.SPECL [`f`, `f'`, `x`, `cball(x:real,e)`, `e`] 958 DIFFERENTIAL_COMPONENT_POS_AT_MINIMUM) ] (* 2 subgoals *) 959 >> ASM_SIMP_TAC real_ss [HAS_DERIVATIVE_AT_WITHIN, CENTRE_IN_CBALL, 960 CONVEX_CBALL, REAL_LT_IMP_LE, IN_INTER] 961 >> DISCH_TAC THEN X_GEN_TAC ``h:real`` 962 >> Q.PAT_X_ASSUM `(f has_derivative f') (at x)` 963 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [has_derivative_at])) 964 >> (Cases_on `h:real = 0` >- ASM_MESON_TAC [LINEAR_0]) 965 >> Q.PAT_X_ASSUM `!y. y IN cball (x,e) ==> _` 966 (fn th => MP_TAC (Q.SPEC `x + e / abs h * h:real` th) \\ 967 MP_TAC (Q.SPEC `x - e / abs h * h:real` th)) 968 >> SIMP_TAC real_ss [IN_CBALL, dist, REAL_ARITH 969 ``(abs(x:real - (x - e)) = abs e) /\ (abs(x:real - (x + e)) = abs e)``, 970 REAL_ARITH ``x - e / abs h * h - x = -(e / abs h * h):real``] 971 >> FIRST_ASSUM (fn th => REWRITE_TAC [MATCH_MP LINEAR_NEG th]) 972 >| [ ONCE_REWRITE_TAC [METIS [REAL_LE_NEG] ``-e <= 0 <=> -0 <= --e:real``], 973 ONCE_REWRITE_TAC [METIS [REAL_LE_NEG] ``0 <= -e <=> --e <= -0:real``] ] 974 >> SIMP_TAC std_ss [REAL_NEG_NEG, REAL_NEG_0] 975 (* stage work, right-associative from now on *) 976 >> (Know `abs (e / abs h * h) <= e` 977 >- (Cases_on `0 <= h` (* 2 subgoals, same tactics *) 978 >- (REWRITE_TAC [real_div, REAL_ARITH ``a * b * c = a * (b * c:real)``] \\ 979 FULL_SIMP_TAC real_ss [abs, REAL_MUL_LINV, GSYM REAL_NEG_INV, 980 REAL_ARITH ``-a * b = -(a * b:real)``] \\ 981 `0 <= e` by PROVE_TAC [REAL_LT_IMP_LE] >> rw []) \\ 982 REWRITE_TAC [real_div, REAL_ARITH ``a * b * c = a * (b * c:real)``] \\ 983 FULL_SIMP_TAC real_ss [abs, REAL_MUL_LINV, GSYM REAL_NEG_INV, 984 REAL_ARITH ``-a * b = -(a * b:real)``] \\ 985 ONCE_REWRITE_TAC [METIS [REAL_LE_NEG] ``0 <= -e <=> --e <= -0:real``] \\ 986 SIMP_TAC std_ss [REAL_NEG_NEG, REAL_NEG_0] \\ 987 `~(e <= 0)` by PROVE_TAC [real_lte] >> rw []) \\ 988 RW_TAC std_ss [] \\ 989 `f' (e / abs h * h) = 0` by METIS_TAC [REAL_LE_ANTISYM] \\ 990 POP_ASSUM MP_TAC >> ASM_SIMP_TAC std_ss [LINEAR_CMUL] \\ 991 ASM_SIMP_TAC std_ss [REAL_ENTIRE] \\ 992 Suff `e / abs h <> 0` >- rw [] \\ 993 ONCE_REWRITE_TAC [EQ_SYM_EQ] \\ 994 MATCH_MP_TAC REAL_LT_IMP_NE \\ 995 MATCH_MP_TAC REAL_LT_DIV \\ 996 ASM_SIMP_TAC std_ss [GSYM ABS_NZ]) 997QED 998 999Theorem DIFFERENTIAL_ZERO_MAXMIN : 1000 !f:real->real f' x s. 1001 x IN s /\ open s /\ (f has_derivative f') (at x) /\ 1002 ((!y. y IN s ==> (f y) <= (f x)) \/ 1003 (!y. y IN s ==> (f x) <= (f y))) 1004 ==> (f' = \v. 0) 1005Proof 1006 rpt STRIP_TAC 1007 >> MP_TAC (ISPECL [``f:real->real``, ``f':real->real``, 1008 ``x:real``, ``s:real->bool``] 1009 DIFFERENTIAL_COMPONENT_ZERO_AT_MAXMIN) 1010 >> ASM_SIMP_TAC real_ss [FUN_EQ_THM, REAL_LE_REFL] 1011QED 1012 1013(* ------------------------------------------------------------------------- *) 1014(* The traditional Rolle theorem in one dimension. 1056 *) 1015(* ------------------------------------------------------------------------- *) 1016 1017val ROLLE = store_thm ("ROLLE", 1018 ``!f:real->real f' a b. 1019 a < b /\ (f a = f b) /\ 1020 f continuous_on interval[a,b] /\ 1021 (!x. x IN interval(a,b) ==> (f has_derivative f'(x)) (at x)) 1022 ==> ?x. x IN interval(a,b) /\ (f'(x) = \v. 0)``, 1023 REPEAT STRIP_TAC THEN 1024 SUBGOAL_THEN 1025 ``?x. x:real IN interval(a,b) /\ 1026 ((!y. y IN interval(a,b) ==> (f x):real <= (f y)) \/ 1027 (!y. y IN interval(a,b) ==> (f y):real <= (f x)))`` 1028 MP_TAC THENL 1029 [ALL_TAC, METIS_TAC[DIFFERENTIAL_ZERO_MAXMIN, OPEN_INTERVAL]] THEN 1030 MAP_EVERY (MP_TAC o ISPECL 1031 [``(f:real->real)``, ``interval[a:real,b]``]) 1032 [CONTINUOUS_ATTAINS_SUP, CONTINUOUS_ATTAINS_INF] THEN 1033 REWRITE_TAC[COMPACT_INTERVAL, o_ASSOC] THEN 1034 ASM_SIMP_TAC real_ss [CONTINUOUS_ON_COMPOSE, CONTINUOUS_ON_ID, o_DEF] THEN 1035 REWRITE_TAC[GSYM INTERVAL_EQ_EMPTY, CONJ_ASSOC, REAL_LE_ANTISYM] THEN 1036 ASM_SIMP_TAC real_ss [UNWIND_THM1, REAL_NOT_LT, REAL_LT_IMP_LE] THEN 1037 DISCH_THEN(X_CHOOSE_THEN ``d:real`` STRIP_ASSUME_TAC) THEN 1038 ASM_CASES_TAC ``(d:real) IN interval(a,b)`` THENL 1039 [ASM_MESON_TAC[SUBSET_DEF, INTERVAL_OPEN_SUBSET_CLOSED], ALL_TAC] THEN 1040 DISCH_THEN(X_CHOOSE_THEN ``c:real`` STRIP_ASSUME_TAC) THEN 1041 ASM_CASES_TAC ``(c:real) IN interval(a,b)`` THENL 1042 [ASM_MESON_TAC[SUBSET_DEF, INTERVAL_OPEN_SUBSET_CLOSED], ALL_TAC] THEN 1043 SUBGOAL_THEN ``?x:real. x IN interval(a,b)`` MP_TAC THENL 1044 [REWRITE_TAC[MEMBER_NOT_EMPTY, GSYM INTERVAL_EQ_EMPTY] THEN 1045 ASM_MESON_TAC[REAL_LE_ANTISYM, REAL_NOT_LE], 1046 ALL_TAC] THEN 1047 STRIP_TAC THEN Q.EXISTS_TAC `x` THEN 1048 REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP INTERVAL_CASES)) THEN 1049 ASM_REWRITE_TAC[] THEN REPEAT(DISCH_THEN(DISJ_CASES_THEN SUBST_ALL_TAC)) THEN 1050 ASM_MESON_TAC[REAL_LE_ANTISYM, SUBSET_DEF, INTERVAL_OPEN_SUBSET_CLOSED]); 1051 1052(* ------------------------------------------------------------------------- *) 1053(* One-dimensional mean value theorem. 1076 *) 1054(* ------------------------------------------------------------------------- *) 1055 1056val MVT = store_thm ("MVT", 1057 ``!f:real->real f' a b. 1058 a < b /\ f continuous_on interval[a,b] /\ 1059 (!x. x IN interval(a,b) ==> (f has_derivative f'(x)) (at x)) 1060 ==> ?x. x IN interval(a,b) /\ (f(b) - f(a) = f'(x) (b - a))``, 1061 REPEAT STRIP_TAC THEN 1062 MP_TAC(SPECL [``\x. f(x) - ((f b - f a) / (b - a)) * x:real``, 1063 ``\k:real x:real. 1064 f'(k)(x) - ((f b - f a) / (b - a)) * x:real``, 1065 ``a:real``, ``b:real``] 1066 ROLLE) THEN 1067 REWRITE_TAC[] THEN 1068 Q_TAC SUFF_TAC `(a < b /\ 1069 ((\x. f x - (f b - f a) / (b - a) * x) a = 1070 (\x. f x - (f b - f a) / (b - a) * x) b)) /\ 1071 (\x. f x - (f b - f a) / (b - a) * x) continuous_on interval [(a,b)] /\ 1072 (!x. x IN interval (a,b) ==> 1073 ((\x. f x - (f b - f a) / (b - a) * x) has_derivative 1074 (\k x. f' k x - (f b - f a) / (b - a) * x) x) (at x))` THENL 1075 [DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN 1076 STRIP_TAC THEN Q.EXISTS_TAC `x` THEN POP_ASSUM MP_TAC THEN 1077 ASM_SIMP_TAC std_ss [FUN_EQ_THM] THEN DISCH_THEN (MP_TAC o SPEC ``b - a:real``), 1078 ASM_SIMP_TAC real_ss [CONTINUOUS_ON_SUB, CONTINUOUS_ON_CMUL, CONTINUOUS_ON_ID] THEN 1079 CONJ_TAC THENL 1080 [REWRITE_TAC[REAL_ARITH 1081 ``(fa - k * a = fb - k * b) <=> (fb - fa = k * (b - a:real))``] THEN 1082 SIMP_TAC real_ss [real_div, REAL_ARITH ``a * b * c = a * (b * c:real)``] THEN 1083 `b - a <> 0` by (UNDISCH_TAC ``a < b:real`` THEN REAL_ARITH_TAC) THEN 1084 ASM_SIMP_TAC real_ss [REAL_MUL_LINV], 1085 REPEAT STRIP_TAC THEN 1086 ONCE_REWRITE_TAC [METIS [] ``(f b - f a) / (b - a) * x = 1087 (\x. (f b - f a) / (b - a) * x) x:real``] THEN 1088 MATCH_MP_TAC HAS_DERIVATIVE_SUB THEN 1089 ASM_SIMP_TAC real_ss [HAS_DERIVATIVE_CMUL, HAS_DERIVATIVE_ID, ETA_AX]]] THEN 1090 `b - a <> 0` by (UNDISCH_TAC ``a < b:real`` THEN REAL_ARITH_TAC) THEN 1091 ASM_SIMP_TAC real_ss [REAL_DIV_RMUL] THEN REAL_ARITH_TAC); 1092 1093(* ------------------------------------------------------------------------- *) 1094(* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *) 1095(* ------------------------------------------------------------------------- *) 1096 1097val MVT_GENERAL = store_thm ("MVT_GENERAL", 1098 ``!f:real->real f' a b. 1099 a < b /\ f continuous_on interval[a,b] /\ 1100 (!x. x IN interval(a,b) ==> (f has_derivative f'(x)) (at x)) 1101 ==> ?x. x IN interval(a,b) /\ 1102 abs(f(b) - f(a)) <= abs(f'(x) (b - a))``, 1103 REPEAT STRIP_TAC THEN 1104 MP_TAC(SPECL [``((\y. (f(b) - f(a)) * y)) o (f:real->real)``, 1105 ``\x t. ((f(b:real) - f(a)) * 1106 ((f':real->real->real) x t))``, 1107 ``a:real``, ``b:real``] MVT) THEN 1108 Q_TAC SUFF_TAC `a < b /\ (\y. (f b - f a) * y) o 1109 f continuous_on interval [(a,b)] /\ 1110 (!x. x IN interval (a,b) ==> 1111 ((\y. (f b - f a) * y) o f has_derivative 1112 (\x t. (f b - f a) * f' x t) x) (at x))` THENL 1113 [ALL_TAC, 1114 ASM_SIMP_TAC real_ss [] THEN CONJ_TAC THENL 1115 [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN 1116 ASM_SIMP_TAC std_ss [CONTINUOUS_ON_ID, CONTINUOUS_ON_CONST, CONTINUOUS_ON_MUL], 1117 ALL_TAC] THEN 1118 REPEAT STRIP_TAC THEN SIMP_TAC std_ss [o_DEF] THEN 1119 MATCH_MP_TAC HAS_DERIVATIVE_CMUL THEN METIS_TAC []] THEN 1120 DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN 1121 STRIP_TAC THEN Q.EXISTS_TAC `x` THEN POP_ASSUM MP_TAC THEN 1122 ASM_SIMP_TAC real_ss [GSYM REAL_SUB_LDISTRIB, o_THM] THEN 1123 DISCH_TAC THEN ASM_CASES_TAC ``(f:real->real) b = f a`` THENL 1124 [ASM_SIMP_TAC std_ss [REAL_SUB_REFL, ABS_0, ABS_POS], ALL_TAC] THEN 1125 REWRITE_TAC [REAL_LE_LT] THEN DISJ2_TAC THEN 1126 MATCH_MP_TAC REAL_EQ_LMUL_IMP THEN 1127 Q.EXISTS_TAC `abs((f:real->real) b - f a)` THEN 1128 ASM_SIMP_TAC real_ss [GSYM ABS_MUL] THEN 1129 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN 1130 POP_ASSUM MP_TAC THEN REAL_ARITH_TAC); 1131 1132(* ------------------------------------------------------------------------- *) 1133(* Operator norm. *) 1134(* ------------------------------------------------------------------------- *) 1135 1136val oabs = new_definition ("oabs", 1137 ``oabs (f:real->real) = sup { abs(f x) | abs(x) = &1 }``); 1138 1139val ABS_BOUND_GENERALIZE = store_thm ("ABS_BOUND_GENERALIZE", 1140 ``!f:real->real b. 1141 linear f 1142 ==> ((!x. (abs(x) = &1) ==> abs(f x) <= b) <=> 1143 (!x. abs(f x) <= b * abs(x)))``, 1144 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THENL 1145 [ALL_TAC, ASM_MESON_TAC[REAL_MUL_RID]] THEN 1146 X_GEN_TAC ``x:real`` THEN ASM_CASES_TAC ``x:real = 0`` THENL 1147 [ASM_REWRITE_TAC[ABS_0, REAL_MUL_RZERO] THEN 1148 ASM_MESON_TAC[LINEAR_0, ABS_0, REAL_LE_REFL], 1149 ALL_TAC] THEN 1150 `0 < abs x` by (ASM_SIMP_TAC std_ss [GSYM ABS_NZ]) THEN 1151 ASM_SIMP_TAC real_ss [GSYM REAL_LE_LDIV_EQ, ABS_NZ, real_div] THEN 1152 MATCH_MP_TAC(REAL_ARITH ``abs(a * b) <= c ==> b * a <= c:real``) THEN 1153 ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN ASM_SIMP_TAC std_ss [ABS_ABS, GSYM ABS_INV] THEN 1154 REWRITE_TAC [GSYM ABS_MUL] THEN 1155 FIRST_ASSUM(fn th => REWRITE_TAC[GSYM(MATCH_MP LINEAR_CMUL th)]) THEN 1156 ASM_SIMP_TAC real_ss [ABS_MUL, ABS_INV, ABS_ABS, REAL_MUL_LINV, ABS_0]); 1157 1158val OABS = store_thm ("OABS", 1159 ``!f:real->real. 1160 linear f 1161 ==> (!x. abs(f x) <= oabs f * abs(x)) /\ 1162 (!b. (!x. abs(f x) <= b * abs(x)) ==> oabs f <= b)``, 1163 GEN_TAC THEN DISCH_TAC THEN 1164 MP_TAC(Q.SPEC `{ abs((f:real->real) x) | abs(x) = &1 }` SUP) THEN 1165 SIMP_TAC std_ss [GSPECIFICATION, LEFT_IMP_EXISTS_THM] THEN 1166 SIMP_TAC std_ss [LEFT_FORALL_IMP_THM, RIGHT_EXISTS_AND_THM, EXISTS_REFL] THEN 1167 ASM_SIMP_TAC std_ss [ABS_BOUND_GENERALIZE, GSYM oabs, GSYM MEMBER_NOT_EMPTY] THEN 1168 DISCH_THEN MATCH_MP_TAC THEN SIMP_TAC std_ss [GSPECIFICATION] THEN 1169 ASM_MESON_TAC[REAL_CHOOSE_SIZE, LINEAR_BOUNDED, REAL_POS]); 1170 1171(* ------------------------------------------------------------------------- *) 1172(* Still more general bound theorem. 1168 *) 1173(* ------------------------------------------------------------------------- *) 1174 1175val DIFFERENTIABLE_BOUND = store_thm ("DIFFERENTIABLE_BOUND", 1176 ``!f:real->real f' s B. 1177 convex s /\ 1178 (!x. x IN s ==> (f has_derivative f'(x)) (at x within s)) /\ 1179 (!x. x IN s ==> oabs(f'(x)) <= B) 1180 ==> !x y. x IN s /\ y IN s ==> abs(f(x) - f(y)) <= B * abs(x - y)``, 1181 ONCE_REWRITE_TAC[ABS_SUB] THEN REPEAT STRIP_TAC THEN 1182 SUBGOAL_THEN 1183 ``!x y. x IN s ==> abs((f':real->real->real)(x) y) <= B * abs(y)`` 1184 ASSUME_TAC THENL 1185 [FULL_SIMP_TAC std_ss [has_derivative] THEN RW_TAC std_ss [] THEN 1186 FIRST_X_ASSUM (MP_TAC o Q.SPEC `x'`) THEN 1187 FIRST_X_ASSUM (MP_TAC o Q.SPEC `x'`) THEN 1188 ASM_REWRITE_TAC [] THEN RW_TAC std_ss [] THEN 1189 FIRST_X_ASSUM (MP_TAC o MATCH_MP OABS) THEN RW_TAC std_ss [] THEN 1190 MATCH_MP_TAC REAL_LE_TRANS THEN Q.EXISTS_TAC `oabs (f' x') * abs y'` THEN 1191 ASM_SIMP_TAC std_ss [] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN 1192 ASM_SIMP_TAC std_ss [REAL_LE_REFL, ABS_POS] THEN 1193 SIMP_TAC std_ss [oabs] THEN MATCH_MP_TAC REAL_LE_SUP THEN 1194 SIMP_TAC std_ss [GSPECIFICATION] THEN Q.EXISTS_TAC `oabs (f' x') * abs 1` THEN 1195 Q.EXISTS_TAC `abs (f' x' 1)` THEN METIS_TAC [ABS_POS, ABS_1], 1196 ALL_TAC] THEN 1197 SUBGOAL_THEN 1198 ``!u. u IN interval[0,1] ==> (x + u * (y - x) :real) IN s`` 1199 ASSUME_TAC THENL 1200 [REWRITE_TAC[IN_INTERVAL] THEN SIMP_TAC std_ss [REAL_LE_REFL] THEN 1201 REWRITE_TAC[REAL_ARITH ``x + u * (y - x) = (&1 - u) * x + u * y:real``] THEN 1202 ASM_MESON_TAC[CONVEX_ALT], 1203 ALL_TAC] THEN 1204 SUBGOAL_THEN 1205 ``!u. u IN interval(0,1) ==> (x + u * (y - x) :real) IN s`` 1206 ASSUME_TAC THENL 1207 [ASM_MESON_TAC[SUBSET_DEF, INTERVAL_OPEN_SUBSET_CLOSED], ALL_TAC] THEN 1208 MP_TAC(SPECL 1209 [``(f:real->real) o (\u. x + u * (y - x))``, 1210 ``(\u. (f':real->real->real) (x + u * (y - x)) o 1211 (\u. 0 + u * (y - x)))``, 1212 ``0:real``, ``1:real``] MVT_GENERAL) THEN 1213 SIMP_TAC real_ss [o_DEF, REAL_ARITH ``x + &1 * (y - x) = y:real``, 1214 REAL_MUL_LZERO, REAL_SUB_RZERO, REAL_ADD_RID] THEN 1215 SIMP_TAC real_ss [REAL_MUL_LID] THEN 1216 Q_TAC SUFF_TAC `(\u. f (x + u * (y - x))) continuous_on interval [(0,1)] /\ 1217 (!x'. x' IN interval (0,1) ==> 1218 ((\u. f (x + u * (y - x))) has_derivative 1219 (\u. f' (x + x' * (y - x)) (u * (y - x)))) (at x'))` THENL 1220 [DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN 1221 ASM_MESON_TAC[REAL_ADD_LID, REAL_LE_TRANS], 1222 ALL_TAC] THEN CONJ_TAC THENL 1223 [ONCE_REWRITE_TAC [METIS [] ``(x + u * (y - x)) = (\u. x + u * (y - x)) u:real``] THEN 1224 MATCH_MP_TAC (SIMP_RULE std_ss [o_DEF] CONTINUOUS_ON_COMPOSE) THEN 1225 SIMP_TAC real_ss [CONTINUOUS_ON_ADD, CONTINUOUS_ON_CONST, CONTINUOUS_ON_MUL, 1226 o_DEF, CONTINUOUS_ON_ID] THEN 1227 MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN EXISTS_TAC ``s:real->bool`` THEN 1228 ASM_SIMP_TAC real_ss [SUBSET_DEF, FORALL_IN_IMAGE] THEN 1229 ASM_MESON_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN, differentiable, 1230 CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN], 1231 ALL_TAC] THEN 1232 X_GEN_TAC ``a:real`` THEN DISCH_TAC THEN 1233 SUBGOAL_THEN ``a IN interval(0:real,1) /\ open(interval(0:real,1))`` 1234 MP_TAC THENL [ASM_MESON_TAC[OPEN_INTERVAL], ALL_TAC] THEN 1235 DISCH_THEN(fn th => ONCE_REWRITE_TAC[GSYM(MATCH_MP 1236 HAS_DERIVATIVE_WITHIN_OPEN th)]) THEN 1237 ONCE_REWRITE_TAC [METIS [] ``(x + u * (y - x) = (\u. x + u * (y - x)) u) /\ 1238 (u * (y - x) = (\u. u * (y - x)) u:real)``] THEN 1239 MATCH_MP_TAC (SIMP_RULE std_ss [o_DEF] DIFF_CHAIN_WITHIN) THEN 1240 CONJ_TAC THENL 1241 [ALL_TAC, 1242 MATCH_MP_TAC HAS_DERIVATIVE_WITHIN_SUBSET THEN 1243 EXISTS_TAC ``s:real->bool`` THEN 1244 ASM_SIMP_TAC real_ss [SUBSET_DEF, FORALL_IN_IMAGE]] THEN 1245 Q_TAC SUFF_TAC `((\u. x + u * (y - x)) has_derivative (\u. u * (y - x))) = 1246 ((\u. (\u. x) u + (\u. u * (y - x)) u) has_derivative 1247 (\u. (\u:real. 0:real) u + (\u. u * (y - x)) u))` THENL 1248 [DISC_RW_KILL, SIMP_TAC real_ss []] THEN 1249 MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN REWRITE_TAC [HAS_DERIVATIVE_CONST] THEN 1250 ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN 1251 ONCE_REWRITE_TAC [METIS [] ``(\u. (y - x) * u) = (\u. (y - x) * (\u. u) u:real)``] THEN 1252 MATCH_MP_TAC HAS_DERIVATIVE_CMUL THEN SIMP_TAC std_ss [HAS_DERIVATIVE_ID]); 1253 1254(* ------------------------------------------------------------------------- *) 1255(* Uniformly convergent sequence of derivatives. 1948 *) 1256(* ------------------------------------------------------------------------- *) 1257 1258val HAS_DERIVATIVE_SEQUENCE_LIPSCHITZ = store_thm ("HAS_DERIVATIVE_SEQUENCE_LIPSCHITZ", 1259 ``!s f:num->real->real f' g'. 1260 convex s /\ 1261 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\ 1262 (!e. &0 < e 1263 ==> ?N. !n x h. n >= N /\ x IN s 1264 ==> abs(f' n x h - g' x h) <= e * abs(h)) 1265 ==> !e. &0 < e 1266 ==> ?N. !m n x y. m >= N /\ n >= N /\ x IN s /\ y IN s 1267 ==> abs((f m x - f n x) - (f m y - f n y)) 1268 <= e * abs(x - y)``, 1269 REPEAT STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o Q.SPEC `e / &2`) THEN 1270 ASM_REWRITE_TAC[REAL_HALF] THEN 1271 Q_TAC SUFF_TAC `!N. (!n x h. n >= N /\ x IN s ==> 1272 abs (f' n x h - g' x h) <= e / 2 * abs h) ==> 1273 !m n x y. m >= N /\ n >= N /\ x IN s /\ y IN s ==> 1274 abs (f m x - f n x - (f m y - f n y)) <= e * abs (x - y)` THENL 1275 [METIS_TAC [MONO_EXISTS], ALL_TAC] THEN 1276 X_GEN_TAC ``N:num`` THEN DISCH_TAC THEN 1277 MAP_EVERY X_GEN_TAC [``m:num``, ``n:num``] THEN 1278 ASM_CASES_TAC ``m:num >= N`` THEN ASM_REWRITE_TAC[] THEN 1279 ASM_CASES_TAC ``n:num >= N`` THEN ASM_REWRITE_TAC[] THEN 1280 ONCE_REWRITE_TAC [METIS [] ``(f m x - f n x - (f m y - f n y)) = 1281 ((\x. f m x - f n x) x - (\y. (f:num->real->real) m y - f n y) y)``] THEN 1282 MATCH_MP_TAC DIFFERENTIABLE_BOUND THEN 1283 Q.EXISTS_TAC `\x h. (f':num->real->real->real) m x h - f' n x h` THEN 1284 ASM_SIMP_TAC std_ss [] THEN CONJ_TAC THENL 1285 [METIS_TAC [HAS_DERIVATIVE_SUB], ALL_TAC] THEN 1286 X_GEN_TAC ``x:real`` THEN DISCH_TAC THEN 1287 SUBGOAL_THEN 1288 ``!h. abs((f':num->real->real->real) m x h - f' n x h) <= e * abs(h)`` 1289 MP_TAC THEN RULE_ASSUM_TAC(REWRITE_RULE[HAS_DERIVATIVE_WITHIN_ALT]) THENL 1290 [ALL_TAC, 1291 Q_TAC SUFF_TAC `linear (\h. f' m x h - f' n x h)` THENL 1292 [ALL_TAC, MATCH_MP_TAC LINEAR_COMPOSE_SUB THEN METIS_TAC []] THEN 1293 DISCH_THEN (MP_TAC o MATCH_MP OABS) THEN RW_TAC std_ss []] THEN 1294 X_GEN_TAC ``h:real`` THEN SUBST1_TAC(REAL_ARITH 1295 ``(f':num->real->real->real) m x h - f' n x h = 1296 (f' m x h - g' x h) + -(f' n x h - g' x h)``) THEN 1297 MATCH_MP_TAC ABS_TRIANGLE_LE THEN 1298 Q_TAC SUFF_TAC `!a b h. a <= e / &2 * h /\ b <= e / &2 * h ==> a + b <= e * h:real` THENL 1299 [DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC real_ss [ABS_NEG], ALL_TAC] THEN 1300 ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN SIMP_TAC real_ss [real_div] THEN 1301 ONCE_REWRITE_TAC [REAL_ARITH ``a * (b * c) = (a * b) * c:real``] THEN 1302 SIMP_TAC real_ss [GSYM real_div, REAL_LE_RDIV_EQ] THEN REAL_ARITH_TAC); 1303 1304val HAS_DERIVATIVE_SEQUENCE = store_thm ("HAS_DERIVATIVE_SEQUENCE", 1305 ``!s f:num->real->real f' g'. 1306 convex s /\ 1307 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\ 1308 (!e. &0 < e 1309 ==> ?N. !n x h. n >= N /\ x IN s 1310 ==> abs(f' n x h - g' x h) <= e * abs(h)) /\ 1311 (?x l. x IN s /\ ((\n. f n x) --> l) sequentially) 1312 ==> ?g. !x. x IN s 1313 ==> ((\n. f n x) --> g x) sequentially /\ 1314 (g has_derivative g'(x)) (at x within s)``, 1315 1316 REPEAT GEN_TAC THEN 1317 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1318 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1319 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN (* O *) 1320 DISCH_THEN(X_CHOOSE_THEN ``x0:real`` STRIP_ASSUME_TAC) THEN 1321 SUBGOAL_THEN ``!e. &0 < e 1322 ==> ?N. !m n x y. m >= N /\ n >= N /\ x IN s /\ y IN s 1323 ==> abs(((f:num->real->real) m x - f n x) - (f m y - f n y)) 1324 <= e * abs(x - y)`` ASSUME_TAC THENL 1325 [MATCH_MP_TAC HAS_DERIVATIVE_SEQUENCE_LIPSCHITZ THEN 1326 ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[], ALL_TAC] THEN 1327 SUBGOAL_THEN 1328 ``?g:real->real. !x. x IN s ==> ((\n. f n x) --> g x) sequentially`` 1329 MP_TAC THENL 1330 [SIMP_TAC std_ss [GSYM SKOLEM_THM, RIGHT_EXISTS_IMP_THM] THEN 1331 X_GEN_TAC ``x:real`` THEN DISCH_TAC THEN 1332 GEN_REWR_TAC I [CONVERGENT_EQ_CAUCHY] THEN 1333 FIRST_X_ASSUM(MP_TAC o MATCH_MP CONVERGENT_IMP_CAUCHY) THEN 1334 SIMP_TAC std_ss [cauchy, dist] THEN DISCH_TAC THEN 1335 X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1336 ASM_CASES_TAC ``x:real = x0`` THEN ASM_SIMP_TAC std_ss [] THEN 1337 FIRST_X_ASSUM (MP_TAC o Q.SPEC `e / &2`) THEN 1338 ASM_REWRITE_TAC[REAL_HALF] THEN 1339 DISCH_THEN(X_CHOOSE_THEN ``N1:num`` STRIP_ASSUME_TAC) THEN 1340 `0 < abs(x - x0)` by (UNDISCH_TAC ``x <> x0:real`` THEN REAL_ARITH_TAC) THEN 1341 FIRST_X_ASSUM (MP_TAC o Q.SPEC `e / &2 / abs(x - x0:real)`) THEN 1342 ASM_SIMP_TAC real_ss [REAL_LT_DIV, ABS_NZ, REAL_HALF] THEN 1343 DISCH_THEN(X_CHOOSE_TAC ``N2:num``) THEN 1344 EXISTS_TAC ``N1 + N2:num`` THEN X_GEN_TAC ``m:num`` THEN X_GEN_TAC ``n:num`` THEN 1345 DISCH_THEN(CONJUNCTS_THEN (STRIP_ASSUME_TAC o MATCH_MP 1346 (ARITH_PROVE ``m >= N1 + N2:num ==> m >= N1 /\ m >= N2``))) THEN 1347 SUBST1_TAC(REAL_ARITH 1348 ``(f:num->real->real) m x - f n x = 1349 (f m x - f n x - (f m x0 - f n x0)) + (f m x0 - f n x0)``) THEN 1350 MATCH_MP_TAC ABS_TRIANGLE_LT THEN 1351 FIRST_X_ASSUM(MP_TAC o SPECL 1352 [``m:num``, ``n:num``, ``x:real``, ``x0:real``]) THEN 1353 FIRST_X_ASSUM(MP_TAC o SPECL [``m:num``, ``n:num``]) THEN 1354 SIMP_TAC real_ss [real_div] THEN 1355 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = a * b * (c * d:real)``] THEN 1356 ASM_SIMP_TAC real_ss [REAL_LT_IMP_NE, REAL_MUL_LINV] THEN 1357 ASM_SIMP_TAC real_ss [GSYM real_div, real_sub] THEN 1358 SIMP_TAC real_ss [REAL_LT_RDIV_EQ, REAL_LE_RDIV_EQ] THEN REAL_ARITH_TAC, 1359 ALL_TAC] THEN 1360 STRIP_TAC THEN Q.EXISTS_TAC `g` THEN ASM_SIMP_TAC std_ss [] THEN 1361 X_GEN_TAC ``x:real`` THEN DISCH_TAC THEN 1362 REWRITE_TAC[HAS_DERIVATIVE_WITHIN_ALT] THEN 1363 SUBGOAL_THEN ``!e. &0 < e 1364 ==> ?N. !n x y. n >= N /\ x IN s /\ y IN s 1365 ==> abs(((f:num->real->real) n x - f n y) - (g x - g y)) 1366 <= e * abs(x - y)`` ASSUME_TAC THENL 1367 [X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1368 UNDISCH_TAC ``!e:real. 0 < e ==> 1369 ?N. !m:num n:num x:real y:real. 1370 m >= N /\ n >= N /\ x IN s /\ y IN s ==> 1371 abs (f m x - f n x - (f m y - f n y)) <= e * abs (x - y)`` THEN 1372 DISCH_THEN (MP_TAC o SPEC ``e:real``) THEN ASM_REWRITE_TAC[] THEN 1373 STRIP_TAC THEN Q.EXISTS_TAC `N` THEN GEN_TAC THEN 1374 POP_ASSUM (MP_TAC o Q.SPEC `n`) THEN DISCH_TAC THEN 1375 MAP_EVERY X_GEN_TAC [``u:real``, ``v:real``] THEN 1376 STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o GEN ``m:num`` o SPECL 1377 [``m:num``, ``u:real``, ``v:real``]) THEN 1378 DISCH_TAC THEN MATCH_MP_TAC(ISPEC ``sequentially`` LIM_ABS_UBOUND) THEN 1379 Q.EXISTS_TAC 1380 `\m. ((f:num->real->real) n u - f n v) - (f m u - f m v)` THEN 1381 REWRITE_TAC[eventually, TRIVIAL_LIMIT_SEQUENTIALLY] THEN 1382 ASM_SIMP_TAC std_ss [SEQUENTIALLY, LIM_SUB, LIM_CONST] THEN EXISTS_TAC ``N:num`` THEN 1383 ONCE_REWRITE_TAC[REAL_ARITH 1384 ``(x - y) - (u - v) = (x - u) - (y - v):real``] THEN 1385 ASM_MESON_TAC[GREATER_EQ_REFL], ALL_TAC] THEN 1386 CONJ_TAC THENL 1387 [SUBGOAL_THEN 1388 ``!u. ((\n. (f':num->real->real->real) n x u) --> g' x u) sequentially`` 1389 ASSUME_TAC THENL 1390 [REWRITE_TAC[LIM_SEQUENTIALLY, dist] THEN REPEAT STRIP_TAC THEN 1391 UNDISCH_TAC ``!e:real. 0 < e ==> 1392 ?N:num. !n x:real h:real. n >= N /\ x IN s ==> 1393 abs (f' n x h - g' x h) <= e * abs h`` THEN 1394 DISCH_TAC THEN ASM_CASES_TAC ``u = 0:real`` THENL 1395 [FIRST_X_ASSUM (MP_TAC o SPEC ``e:real``), 1396 FIRST_X_ASSUM (MP_TAC o SPEC ``e / &2 / abs(u:real)``)] THENL 1397 [ALL_TAC, 1398 `0 < abs u` by (UNDISCH_TAC ``u <> 0:real`` THEN REAL_ARITH_TAC)] THEN 1399 ASM_SIMP_TAC arith_ss [ABS_NZ, REAL_LT_DIV, REAL_LT] THEN 1400 STRIP_TAC THEN Q.EXISTS_TAC `N` THEN GEN_TAC THEN 1401 POP_ASSUM (MP_TAC o Q.SPEC `n`) THEN 1402 DISCH_THEN(MP_TAC o SPECL [``x:real``, ``u:real``]) THEN 1403 DISCH_THEN(fn th => DISCH_TAC THEN MP_TAC th) THEN 1404 ASM_SIMP_TAC real_ss [GE, ABS_0, REAL_MUL_RZERO, ABS_POS] THEN 1405 ASM_SIMP_TAC real_ss [REAL_DIV_RMUL, ABS_0] THENL 1406 [UNDISCH_TAC ``&0 < e:real`` THEN REAL_ARITH_TAC, ALL_TAC] THEN 1407 SIMP_TAC std_ss [real_div] THEN 1408 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = a * b * (c * d:real)``] THEN 1409 ASM_SIMP_TAC real_ss [REAL_LT_IMP_NE, REAL_MUL_LINV] THEN 1410 ASM_SIMP_TAC real_ss [GSYM real_div, REAL_LE_RDIV_EQ] THEN 1411 UNDISCH_TAC ``&0 < e:real`` THEN REAL_ARITH_TAC, ALL_TAC] THEN 1412 REWRITE_TAC[linear] THEN CONJ_TAC THENL 1413 [MAP_EVERY X_GEN_TAC [``u:real``, ``v:real``], 1414 MAP_EVERY X_GEN_TAC [``c:real``, ``u:real``]] THEN 1415 MATCH_MP_TAC(ISPEC ``sequentially`` LIM_UNIQUE) THENL 1416 [Q.EXISTS_TAC 1417 `\n. (f':num->real->real->real) n x (u + v)`, 1418 Q.EXISTS_TAC 1419 `\n. (f':num->real->real->real) n x (c * u)`] THEN 1420 ASM_SIMP_TAC real_ss [TRIVIAL_LIMIT_SEQUENTIALLY, LIM_SUB, LIM_ADD, LIM_CMUL] THEN 1421 RULE_ASSUM_TAC(REWRITE_RULE[has_derivative_within, linear]) THEN 1422 ASM_SIMP_TAC real_ss [REAL_SUB_REFL, LIM_CONST] THEN 1423 METIS_TAC [LIM_ADD, LIM_CMUL], ALL_TAC] THEN 1424 X_GEN_TAC ``e:real`` THEN DISCH_TAC THEN 1425 FIRST_X_ASSUM (MP_TAC o Q.SPEC `e / &3`) THEN 1426 UNDISCH_TAC ``!e:real. 0 < e ==> 1427 ?N:num. !n x:real h:real. n >= N /\ x IN s ==> 1428 abs (f' n x h - g' x h) <= e * abs h`` THEN 1429 DISCH_THEN (MP_TAC o Q.SPEC `e / &3`) THEN 1430 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT] THEN 1431 DISCH_THEN(X_CHOOSE_THEN ``N1:num`` ASSUME_TAC) THEN 1432 DISCH_THEN(X_CHOOSE_THEN ``N2:num`` ASSUME_TAC) THEN 1433 UNDISCH_TAC ``!n:num x:real h:real. n >= N1 /\ x IN s ==> 1434 abs (f' n x h - g' x h) <= e / 3 * abs h`` THEN DISCH_TAC THEN 1435 FIRST_X_ASSUM (MP_TAC o GEN ``y:real`` o 1436 Q.SPECL [`N1 + N2:num`, `x:real`, `y - x:real`]) THEN 1437 FIRST_X_ASSUM (MP_TAC o GEN ``y:real`` o 1438 Q.SPECL [`N1 + N2:num`, `y:real`, `x:real`]) THEN 1439 FIRST_X_ASSUM(MP_TAC o Q.SPECL [`N1 + N2:num`, `x:real`]) THEN 1440 ASM_REWRITE_TAC[ARITH_PROVE ``m + n >= m:num /\ m + n >= n``] THEN 1441 REWRITE_TAC[HAS_DERIVATIVE_WITHIN_ALT] THEN 1442 DISCH_THEN(MP_TAC o Q.SPEC `e / &3` o CONJUNCT2) THEN 1443 ASM_SIMP_TAC arith_ss [REAL_LT_DIV, REAL_LT] THEN 1444 DISCH_THEN(X_CHOOSE_THEN ``d1:real`` STRIP_ASSUME_TAC) THEN 1445 DISCH_TAC THEN DISCH_TAC THEN 1446 Q.EXISTS_TAC `d1:real` THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC ``y:real`` THEN 1447 DISCH_TAC THEN FIRST_X_ASSUM (MP_TAC o Q.SPEC `y:real`) THEN 1448 FIRST_X_ASSUM (MP_TAC o Q.SPEC `y:real`) THEN 1449 FIRST_X_ASSUM(MP_TAC o Q.SPEC `y:real`) THEN 1450 Q_TAC SUFF_TAC `!a b c d n. d <= a + b + c 1451 ==> a <= e / &3 * n ==> b <= e / &3 * n ==> c <= e / &3 * n 1452 ==> d <= e * n` THENL 1453 [ALL_TAC, 1454 ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN SIMP_TAC real_ss [real_div] THEN 1455 ONCE_REWRITE_TAC [REAL_ARITH ``a * (b * c) = (a * b) * c:real``] THEN 1456 SIMP_TAC real_ss [GSYM real_div, REAL_LE_RDIV_EQ] THEN REAL_ARITH_TAC] THEN 1457 ASM_SIMP_TAC real_ss [] THEN DISCH_THEN MATCH_MP_TAC THEN 1458 Q_TAC SUFF_TAC `abs (f (N1 + N2) y - f (N1 + N2) x - (g y - g x)) = 1459 abs ((g y - g x) - (f (N1 + N2) y - f (N1 + N2) x))` THENL 1460 [DISC_RW_KILL, SIMP_TAC real_ss [ABS_SUB]] THEN 1461 MATCH_MP_TAC(REAL_ARITH 1462 ``(abs(x + y + z) = abs(a)) /\ 1463 abs(x + y + z) <= abs(x) + abs(y + z) /\ 1464 abs(y + z) <= abs(y) + abs(z) 1465 ==> abs(a) <= abs(x) + abs(y) + abs(z:real)``) THEN 1466 ONCE_REWRITE_TAC [REAL_ARITH ``a + b + c = a + (b + c:real)``] THEN 1467 SIMP_TAC std_ss [ABS_TRIANGLE] THEN AP_TERM_TAC THEN REAL_ARITH_TAC); 1468 1469(* ------------------------------------------------------------------------- *) 1470(* Differentiation of a series. HAS_DERIVATIVE_SEQUENCE 2187 *) 1471(* ------------------------------------------------------------------------- *) 1472 1473val HAS_DERIVATIVE_SERIES = store_thm ("HAS_DERIVATIVE_SERIES", 1474 ``!s f:num->real->real f' g' k. 1475 convex s /\ 1476 (!n x. x IN s ==> ((f n) has_derivative (f' n x)) (at x within s)) /\ 1477 (!e. &0 < e 1478 ==> ?N. !n x h. n >= N /\ x IN s 1479 ==> abs(sum(k INTER {x | 0 <= x /\ x <= n}) (\i. f' i x h) - 1480 g' x h) <= e * abs(h)) /\ 1481 (?x l. x IN s /\ ((\n. f n x) sums l) k) 1482 ==> ?g. !x. x IN s ==> ((\n. f n x) sums (g x)) k /\ 1483 (g has_derivative g'(x)) (at x within s)``, 1484 REPEAT GEN_TAC THEN REWRITE_TAC[sums, GSYM numseg] THEN 1485 DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN 1486 ONCE_REWRITE_TAC [METIS [] ``sum (k INTER (0 .. n)) (\n. f n x) = 1487 (\n x. sum (k INTER (0 .. n)) (\n. f n x)) n x``] THEN 1488 MATCH_MP_TAC HAS_DERIVATIVE_SEQUENCE THEN Q.EXISTS_TAC 1489 `(\n:num x:real h:real. sum(k INTER ((0:num) .. n)) (\n. f' n x h):real)` THEN 1490 ASM_SIMP_TAC real_ss [FINITE_INTER_NUMSEG] THEN RW_TAC std_ss [] THEN 1491 ONCE_REWRITE_TAC [METIS [] ``(\n. f' n x h) = (\n. (\n h. f' n x h) n h)``] THEN 1492 MATCH_MP_TAC HAS_DERIVATIVE_SUM THEN METIS_TAC [FINITE_INTER_NUMSEG, ETA_AX]); 1493 1494val HAS_DERIVATIVE_SERIES' = store_thm ("HAS_DERIVATIVE_SERIES'", 1495 ``!s f f' g' k. 1496 convex s /\ 1497 (!n x. x IN s 1498 ==> (f n has_derivative (\y. f' n x * y)) (at x within s)) /\ 1499 (!e. &0 < e 1500 ==> ?N. !n x. n >= N /\ x IN s 1501 ==> abs(sum (k INTER ((0:num)..n)) (\i. f' i x) - g' x) <= e) /\ 1502 (?x l. x IN s /\ ((\n. f n x) sums l) k) 1503 ==> ?g. !x. x IN s 1504 ==> ((\n. f n x) sums g x) k /\ 1505 (g has_derivative (\y. g' x * y)) (at x within s)``, 1506 REPEAT STRIP_TAC THEN 1507 ONCE_REWRITE_TAC [METIS [] ``(\y. g' x * y) = (\x y. (g':real->real) x * y) x``] THEN 1508 MATCH_MP_TAC HAS_DERIVATIVE_SERIES THEN 1509 Q.EXISTS_TAC `\n x h. (f':num->real->real) n x * h` THEN 1510 ASM_SIMP_TAC std_ss [] THEN CONJ_TAC THENL [ALL_TAC, METIS_TAC[]] THEN 1511 ONCE_REWRITE_TAC [METIS [] ``(\i. (f':num->real->real) i x' * h) = 1512 (\i. (\i. f' i x') i * h)``] THEN 1513 SIMP_TAC std_ss [SUM_RMUL, GSYM REAL_SUB_RDISTRIB, ABS_MUL] THEN 1514 Q_TAC SUFF_TAC `!n. {x | x <= n} = ((0:num) .. n)` THENL 1515 [METIS_TAC[REAL_LE_RMUL_IMP, ABS_POS], ALL_TAC] THEN 1516 RW_TAC arith_ss [EXTENSION, GSPECIFICATION, IN_NUMSEG]); 1517 1518(* ------------------------------------------------------------------------- *) 1519(* Derivative with composed bilinear function. *) 1520(* ------------------------------------------------------------------------- *) 1521 1522val HAS_DERIVATIVE_BILINEAR_WITHIN = store_thm ("HAS_DERIVATIVE_BILINEAR_WITHIN", 1523 ``!h:real->real->real f g f' g' x:real s. 1524 (f has_derivative f') (at x within s) /\ 1525 (g has_derivative g') (at x within s) /\ 1526 bilinear h 1527 ==> ((\x. h (f x) (g x)) has_derivative 1528 (\d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)``, 1529 REPEAT STRIP_TAC THEN 1530 SUBGOAL_THEN ``((g:real->real) --> g(x)) (at x within s)`` ASSUME_TAC THENL 1531 [REWRITE_TAC[GSYM CONTINUOUS_WITHIN] THEN 1532 ASM_MESON_TAC[differentiable, DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN], 1533 ALL_TAC] THEN 1534 UNDISCH_TAC ``((f:real->real) has_derivative f') (at x within s)`` THEN 1535 REWRITE_TAC[has_derivative_within] THEN 1536 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC ASSUME_TAC) THEN 1537 SUBGOAL_THEN 1538 ``((\y. (f:real->real)(x) + f'(y - x)) --> f(x)) (at x within s)`` 1539 ASSUME_TAC THENL 1540 [GEN_REWR_TAC LAND_CONV [GSYM REAL_ADD_RID] THEN 1541 Q_TAC SUFF_TAC `((\y. (\y. f x) y + (\y. f' (y - x)) y) 1542 --> (f x + 0)) (at x within s)` THENL 1543 [SIMP_TAC std_ss [], ALL_TAC] THEN 1544 MATCH_MP_TAC LIM_ADD THEN REWRITE_TAC[LIM_CONST] THEN 1545 SUBGOAL_THEN ``0 = (f':real->real)(x - x)`` SUBST1_TAC THENL 1546 [ASM_MESON_TAC[LINEAR_0, REAL_SUB_REFL], ALL_TAC] THEN 1547 ASM_SIMP_TAC std_ss [LIM_LINEAR, LIM_SUB, LIM_CONST, LIM_WITHIN_ID], 1548 ALL_TAC] THEN 1549 UNDISCH_TAC ``(g has_derivative g') (at x within s)`` THEN 1550 ONCE_REWRITE_TAC [has_derivative_within] THEN 1551 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC ASSUME_TAC) THEN 1552 CONJ_TAC THENL 1553 [UNDISCH_TAC ``bilinear h`` THEN ONCE_REWRITE_TAC [bilinear] THEN 1554 STRIP_TAC THEN 1555 RULE_ASSUM_TAC(REWRITE_RULE[linear]) THEN ASM_REWRITE_TAC[linear] THEN 1556 FULL_SIMP_TAC real_ss [] THEN REPEAT STRIP_TAC THEN REAL_ARITH_TAC, 1557 ALL_TAC] THEN 1558 MP_TAC(Q.ISPECL [`at (x:real) within s`, `h:real->real->real`] 1559 LIM_BILINEAR) THEN 1560 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN 1561 UNDISCH_TAC ``(g --> g x) (at x within s)`` THEN 1562 UNDISCH_TAC ``((\y. inv (abs (y - x)) * (f y - (f x + f' (y - x)))) --> 0) 1563 (at x within s)`` THEN 1564 REWRITE_TAC[AND_IMP_INTRO] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN 1565 UNDISCH_TAC ``((\y. inv (abs (y - x)) * (g y - (g x + g' (y - x)))) --> 0) 1566 (at x within s)`` THEN 1567 UNDISCH_TAC ``((\y. f x + f' (y - x)) --> f x) (at x within s)`` THEN 1568 ONCE_REWRITE_TAC[AND_IMP_INTRO] THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN 1569 REWRITE_TAC[AND_IMP_INTRO] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN 1570 SUBGOAL_THEN 1571 ``((\y:real. inv(abs(y - x)) * (h:real->real->real) (f'(y - x)) (g'(y - x))) 1572 --> 0) (at x within s)`` 1573 MP_TAC THENL 1574 [FIRST_ASSUM(X_CHOOSE_THEN ``B:real`` STRIP_ASSUME_TAC o MATCH_MP 1575 BILINEAR_BOUNDED_POS) THEN 1576 X_CHOOSE_THEN ``C:real`` STRIP_ASSUME_TAC 1577 (MATCH_MP LINEAR_BOUNDED_POS (ASSUME ``linear (f':real->real)``)) THEN 1578 X_CHOOSE_THEN ``D:real`` STRIP_ASSUME_TAC 1579 (MATCH_MP LINEAR_BOUNDED_POS (ASSUME ``linear (g':real->real)``)) THEN 1580 REWRITE_TAC[LIM_WITHIN, dist, REAL_SUB_RZERO] THEN 1581 X_GEN_TAC ``e:real`` THEN STRIP_TAC THEN Q.EXISTS_TAC `e / (B * C * D)` THEN 1582 ASM_SIMP_TAC real_ss [REAL_LT_DIV, ABS_MUL, REAL_LT_MUL] THEN 1583 X_GEN_TAC ``x':real`` THEN STRIP_TAC THEN 1584 ASM_SIMP_TAC real_ss [ABS_MUL, ABS_ABS, ABS_INV, REAL_LT_IMP_NE] THEN 1585 MATCH_MP_TAC REAL_LET_TRANS THEN 1586 Q.EXISTS_TAC `inv(abs(x' - x :real)) * 1587 B * (C * abs(x' - x)) * (D * abs(x' - x))` THEN 1588 CONJ_TAC THENL 1589 [ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c * d = a * (b * c * d:real)``] THEN 1590 MATCH_MP_TAC REAL_LE_LMUL_IMP THEN SIMP_TAC real_ss [REAL_LE_INV_EQ, ABS_POS] THEN 1591 MATCH_MP_TAC REAL_LE_TRANS THEN 1592 Q.EXISTS_TAC `B * abs (f' (x' - x)) * abs (g' (x' - x))` THEN 1593 ASM_SIMP_TAC std_ss [] THEN REWRITE_TAC [GSYM REAL_MUL_ASSOC] THEN 1594 MATCH_MP_TAC REAL_LE_LMUL_IMP THEN ASM_SIMP_TAC std_ss [REAL_LT_IMP_LE] THEN 1595 ONCE_REWRITE_TAC [REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN 1596 ASM_SIMP_TAC real_ss [ABS_POS], 1597 ONCE_REWRITE_TAC[REAL_ARITH 1598 ``i * b * (c * x) * (d * x) = (i * x) * x * (b * c * d:real)``] THEN 1599 ASM_SIMP_TAC real_ss [REAL_MUL_LINV, REAL_LT_IMP_NE, REAL_MUL_LID] THEN 1600 ASM_SIMP_TAC real_ss [GSYM REAL_LT_RDIV_EQ, REAL_LT_MUL]], 1601 REWRITE_TAC[AND_IMP_INTRO] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN 1602 SIMP_TAC std_ss (map (C MATCH_MP (ASSUME ``bilinear(h:real->real->real)``)) 1603 [BILINEAR_RZERO, BILINEAR_LZERO, BILINEAR_LADD, BILINEAR_RADD, 1604 BILINEAR_LMUL, BILINEAR_RMUL, BILINEAR_LSUB, BILINEAR_RSUB]) THEN 1605 MATCH_MP_TAC EQ_IMPLIES THEN AP_THM_TAC THEN 1606 BINOP_TAC THEN SIMP_TAC real_ss [FUN_EQ_THM] THEN REAL_ARITH_TAC]); 1607 1608val HAS_DERIVATIVE_BILINEAR_AT = store_thm ("HAS_DERIVATIVE_BILINEAR_AT", 1609 ``!h:real->real->real f g f' g' x:real. 1610 (f has_derivative f') (at x) /\ 1611 (g has_derivative g') (at x) /\ 1612 bilinear h 1613 ==> ((\x. h (f x) (g x)) has_derivative 1614 (\d. h (f x) (g' d) + h (f' d) (g x))) (at x)``, 1615 REWRITE_TAC[has_derivative_at] THEN 1616 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN 1617 REWRITE_TAC[GSYM has_derivative_within, HAS_DERIVATIVE_BILINEAR_WITHIN]); 1618 1619val HAS_DERIVATIVE_MUL_WITHIN = store_thm ("HAS_DERIVATIVE_MUL_WITHIN", 1620 ``!f f' g:real->real g' a s. 1621 ((f) has_derivative (f')) (at a within s) /\ 1622 (g has_derivative g') (at a within s) 1623 ==> ((\x. f x * g x) has_derivative 1624 (\h. f a * g' h + f' h * g a)) (at a within s)``, 1625 REPEAT GEN_TAC THEN 1626 DISCH_THEN(MP_TAC o MATCH_MP (REWRITE_RULE[BILINEAR_DOT] 1627 (Q.ISPEC `\x y:real. x * y` HAS_DERIVATIVE_BILINEAR_WITHIN))) THEN 1628 SIMP_TAC std_ss [o_DEF]); 1629 1630val HAS_DERIVATIVE_MUL_AT = store_thm ("HAS_DERIVATIVE_MUL_AT", 1631 ``!f f' g:real->real g' a. 1632 ((f) has_derivative (f')) (at a) /\ 1633 (g has_derivative g') (at a) 1634 ==> ((\x. f x * g x) has_derivative 1635 (\h. f a * g' h + f' h * g a)) (at a)``, 1636 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN 1637 REWRITE_TAC[HAS_DERIVATIVE_MUL_WITHIN]); 1638 1639(* ------------------------------------------------------------------------- *) 1640(* Considering derivative R->R as a vector. *) 1641(* ------------------------------------------------------------------------- *) 1642 1643val _ = set_fixity "has_vector_derivative" (Infix(NONASSOC, 450)); 1644 1645val has_vector_derivative = new_definition ("has_vector_derivative", 1646 ``(f has_vector_derivative f') net <=> 1647 (f has_derivative (\x. (x) * f')) net``); 1648 1649val vector_derivative = new_definition ("vector_derivative", 1650 ``vector_derivative (f:real->real) net = 1651 @f'. (f has_vector_derivative f') net``); 1652 1653Theorem HAS_VECTOR_DERIVATIVE_WITHIN_SUBSET : 1654 !f f' s t x. (f has_vector_derivative f') (at x within s) /\ t SUBSET s 1655 ==> (f has_vector_derivative f') (at x within t) 1656Proof 1657 REWRITE_TAC [has_vector_derivative, HAS_DERIVATIVE_WITHIN_SUBSET] 1658QED 1659 1660val HAS_VECTOR_DERIVATIVE_BILINEAR_WITHIN = store_thm ("HAS_VECTOR_DERIVATIVE_BILINEAR_WITHIN", 1661 ``!h:real->real->real f g f' g' x s. 1662 (f has_vector_derivative f') (at x within s) /\ 1663 (g has_vector_derivative g') (at x within s) /\ 1664 bilinear h 1665 ==> ((\x. h (f x) (g x)) has_vector_derivative 1666 (h (f x) g' + h f' (g x))) (at x within s)``, 1667 REPEAT GEN_TAC THEN SIMP_TAC std_ss [has_vector_derivative] THEN 1668 DISCH_TAC THEN 1669 FIRST_ASSUM(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_WITHIN) THEN 1670 RULE_ASSUM_TAC(REWRITE_RULE[bilinear, linear]) THEN 1671 FULL_SIMP_TAC real_ss [REAL_ADD_LDISTRIB]); 1672 1673val HAS_VECTOR_DERIVATIVE_BILINEAR_AT = store_thm ("HAS_VECTOR_DERIVATIVE_BILINEAR_AT", 1674 ``!h:real->real->real f g f' g' x. 1675 (f has_vector_derivative f') (at x) /\ 1676 (g has_vector_derivative g') (at x) /\ 1677 bilinear h 1678 ==> ((\x. h (f x) (g x)) has_vector_derivative 1679 (h (f x) g' + h f' (g x))) (at x)``, 1680 REPEAT GEN_TAC THEN SIMP_TAC real_ss [has_vector_derivative] THEN 1681 DISCH_TAC THEN 1682 FIRST_ASSUM(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_AT) THEN 1683 RULE_ASSUM_TAC(REWRITE_RULE[bilinear, linear]) THEN 1684 FULL_SIMP_TAC real_ss [REAL_ADD_LDISTRIB]); 1685 1686Theorem HAS_VECTOR_DERIVATIVE_AT_WITHIN : 1687 !f f' x s. (f has_vector_derivative f') (at x) 1688 ==> (f has_vector_derivative f') (at x within s) 1689Proof 1690 SIMP_TAC std_ss [has_vector_derivative, HAS_DERIVATIVE_AT_WITHIN] 1691QED 1692 1693(* ------------------------------------------------------------------------- *) 1694(* CONTINUOUS_ON_EXP *) 1695(* ------------------------------------------------------------------------- *) 1696 1697val HAS_DERIVATIVE_POW = store_thm ("HAS_DERIVATIVE_POW", 1698 ``!q0 n. 1699 ((\q. q pow n) has_derivative 1700 (\q. sum ((1:num)..n) (\i. q0 pow (n - i) * q * q0 pow (i - 1)))) 1701 (at q0)``, 1702 GEN_TAC THEN INDUCT_TAC THENL 1703 [`0 < 1:num` by SIMP_TAC arith_ss [] THEN 1704 FULL_SIMP_TAC real_ss [GSYM NUMSEG_EMPTY, SUM_CLAUSES, pow] THEN 1705 MATCH_ACCEPT_TAC HAS_DERIVATIVE_CONST, ALL_TAC] THEN 1706 REWRITE_TAC[pow, SUM_CLAUSES_NUMSEG, ARITH_PROVE ``1 <= SUC n``, 1707 REAL_SUB_REFL, REAL_MUL_LID, ARITH_PROVE ``SUC n - 1 = n``] THEN 1708 SUBGOAL_THEN 1709 ``!q. sum ((1:num)..n) (\i. q0 pow (SUC n - i) * q * q0 pow (i - 1)) = 1710 q0 * sum ((1:num)..n) (\i. q0 pow (n - i) * q * q0 pow (i - 1))`` 1711 (fn th => REWRITE_TAC[th]) THENL 1712 [GEN_TAC THEN SIMP_TAC std_ss [FINITE_NUMSEG, GSYM SUM_LMUL] THEN 1713 MATCH_MP_TAC SUM_EQ THEN 1714 REWRITE_TAC [IN_NUMSEG, FUN_EQ_THM] THEN REPEAT STRIP_TAC THEN 1715 ASM_SIMP_TAC std_ss [ARITH_PROVE ``x <= n ==> (SUC n - x = SUC (n - x))``, 1716 pow, GSYM REAL_MUL_ASSOC], ALL_TAC] THEN 1717 MP_TAC (Q.ISPEC `(at (q0:real))` HAS_DERIVATIVE_ID) THEN DISCH_TAC THEN 1718 FULL_SIMP_TAC real_ss [] THEN 1719 Q_TAC SUFF_TAC `((\q. (\q. q) q * (\q. q pow n) q) has_derivative 1720 (\q. (\q. q) q0 * (\q. sum (1 .. n) (\i. q0 pow (n - i) * q * q0 pow (i - 1))) q + 1721 (\q. q) q * (\q. q pow n) q0)) (at q0)` THENL 1722 [SIMP_TAC std_ss [], ALL_TAC] THEN MATCH_MP_TAC HAS_DERIVATIVE_MUL_AT THEN 1723 ASM_SIMP_TAC std_ss [HAS_DERIVATIVE_ID]); 1724 1725val EXP_CONVERGES_UNIFORMLY_CAUCHY = store_thm ("EXP_CONVERGES_UNIFORMLY_CAUCHY", 1726 ``!R e. &0 < e /\ &0 < R 1727 ==> ?N. !m n z. m >= N /\ abs(z) <= R 1728 ==> abs(sum(m..n) (\i. z pow i / (&(FACT i)))) < e``, 1729 REPEAT STRIP_TAC THEN 1730 MP_TAC(Q.ISPECL [`&1 / &2:real`, `\i. R pow i / (&(FACT i):real)`, 1731 `from 0`] SERIES_RATIO) THEN 1732 SIMP_TAC real_ss [SERIES_CAUCHY, LEFT_FORALL_IMP_THM] THEN 1733 MP_TAC(Q.SPEC `&2 * abs(R)` SIMP_REAL_ARCH) THEN 1734 MATCH_MP_TAC(TAUT `(a ==> b) /\ (c ==> d) ==> a ==> (b ==> c) ==> d`) THEN 1735 CONJ_TAC THENL 1736 [DISCH_THEN (X_CHOOSE_TAC ``N:num``) THEN Q.EXISTS_TAC `N:num` THEN 1737 X_GEN_TAC ``n:num`` THEN REWRITE_TAC[GE] THEN DISCH_TAC THEN 1738 SIMP_TAC real_ss [FACT, pow, real_div] THEN 1739 `inv (&(FACT n * SUC n)) = inv (&(FACT n):real) * inv (&(SUC n))` by 1740 (ONCE_REWRITE_TAC [GSYM REAL_OF_NUM_MUL] THEN MATCH_MP_TAC REAL_INV_MUL THEN 1741 SIMP_TAC real_ss [] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN MATCH_MP_TAC LESS_NOT_EQ THEN 1742 SIMP_TAC arith_ss [FACT_LESS]) THEN 1743 POP_ASSUM (fn th => SIMP_TAC real_ss [th]) THEN SIMP_TAC real_ss [ABS_MUL] THEN 1744 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * (c * d) = (a * d) * (b * c:real)``] THEN 1745 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC real_ss [REAL_LE_REFL] THEN 1746 SIMP_TAC real_ss [REAL_LE_MUL, ABS_POS, ABS_INV, REAL_INV_1OVER] THEN 1747 SIMP_TAC real_ss [REAL_LE_RDIV_EQ, REAL_ARITH ``a * b * c = (a * c) * b:real``] THEN 1748 REWRITE_TAC [GSYM real_div, GSYM REAL_INV_1OVER] THEN 1749 `0:real < abs (&SUC n)` by SIMP_TAC real_ss [GSYM ABS_NZ] THEN 1750 ASM_SIMP_TAC real_ss [REAL_LE_LDIV_EQ] THEN ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN 1751 MATCH_MP_TAC REAL_LE_TRANS THEN Q.EXISTS_TAC `&N` THEN ASM_SIMP_TAC real_ss [] THEN 1752 MATCH_MP_TAC REAL_LE_TRANS THEN Q.EXISTS_TAC `&n` THEN 1753 ASM_SIMP_TAC real_ss [REAL_OF_NUM_LE, ADD1] THEN 1754 REWRITE_TAC [GSYM REAL_OF_NUM_ADD] THEN REAL_ARITH_TAC, ALL_TAC] THEN 1755 DISCH_THEN(MP_TAC o Q.SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN 1756 STRIP_TAC THEN Q.EXISTS_TAC `N` THEN POP_ASSUM MP_TAC THEN 1757 REWRITE_TAC[FROM_0, INTER_UNIV] THEN DISCH_TAC THEN GEN_TAC THEN 1758 GEN_TAC THEN POP_ASSUM (MP_TAC o Q.SPECL [`m`,`n`]) THEN 1759 DISCH_THEN(fn th => REPEAT STRIP_TAC THEN MP_TAC th) THEN 1760 ASM_REWRITE_TAC [] THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN 1761 Q.EXISTS_TAC `abs (sum (m .. n) (\i. R pow i / &FACT i))` THEN 1762 ASM_REWRITE_TAC [] THEN MATCH_MP_TAC REAL_LE_TRANS THEN 1763 Q.EXISTS_TAC `sum (m .. n) (\i. R pow i / &FACT i)` THEN 1764 SIMP_TAC std_ss [ABS_LE] THEN MATCH_MP_TAC SUM_ABS_LE THEN 1765 RW_TAC std_ss [FINITE_NUMSEG, ABS_MUL, real_div] THEN 1766 MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC std_ss [ABS_POS] THEN 1767 CONJ_TAC THENL 1768 [REWRITE_TAC [GSYM POW_ABS] THEN MATCH_MP_TAC POW_LE THEN 1769 ASM_SIMP_TAC std_ss [ABS_POS], ALL_TAC] THEN 1770 SIMP_TAC std_ss [REAL_LE_LT] THEN DISJ2_TAC THEN 1771 REWRITE_TAC [ABS_REFL] THEN MATCH_MP_TAC REAL_LE_INV THEN 1772 SIMP_TAC std_ss [REAL_LE_LT] THEN DISJ1_TAC THEN 1773 SIMP_TAC std_ss [FACT_LESS, REAL_LT]); 1774 1775val REAL_MUL_NZ = store_thm ("REAL_MUL_NZ", 1776 ``!a b:real. a <> 0 /\ b <> 0 ==> a * b <> 0``, 1777 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [MONO_NOT_EQ] THEN 1778 SIMP_TAC real_ss [REAL_ENTIRE]); 1779 1780(* `sum (0, SUC n)` is defined by realTheory.sum 1781 `sum (0 .. n)` is defined by iterateTheory.sum_def 1782 1783 TODO: re-prove this lemma once `iterate` is re-defined by `pred_set$ITSET` 1784 *) 1785val lemma_sum_eq = prove ( 1786 ``!n x:real. sum (0, SUC n) (\n. (\n. inv(&(FACT n))) n * (x pow n)) = 1787 sum (0 .. n) (\n. (\n. inv(&(FACT n))) n * (x pow n))``, 1788 NTAC 2 GEN_TAC 1789 >> SIMP_TAC std_ss [sum_def, iterate, support] 1790 >> Know `FINITE {n' | n' IN 0 .. n /\ inv (&FACT n') * x pow n' <> neutral $+}` 1791 >- (MATCH_MP_TAC FINITE_SUBSET \\ 1792 Q.EXISTS_TAC `(0 .. n)` \\ 1793 SIMP_TAC std_ss [FINITE_NUMSEG] >> SET_TAC []) 1794 >> DISCH_TAC 1795 >> ASM_SIMP_TAC std_ss [] 1796 >> Know `neutral $+ = 0:real` 1797 >- (SIMP_TAC std_ss [neutral] >> MATCH_MP_TAC SELECT_UNIQUE \\ 1798 RW_TAC real_ss [] \\ 1799 reverse EQ_TAC >- REAL_ARITH_TAC \\ 1800 DISCH_THEN (MP_TAC o Q.SPEC `1`) >> REAL_ARITH_TAC) 1801 >> DISCH_THEN ((FULL_SIMP_TAC std_ss) o wrap) 1802 >> SIMP_TAC std_ss [ITSET'] >> SELECT_ELIM_TAC 1803 >> CONJ_TAC 1804 >- (Q.EXISTS_TAC `(\s. sum s (\n. (\n. inv(&(FACT n))) n * (x pow n)))` \\ 1805 SIMP_TAC std_ss [SUM_CLAUSES]) 1806 THEN RW_TAC std_ss [] THEN ASM_CASES_TAC ``x = 0:real`` THENL 1807 [ASM_SIMP_TAC real_ss [ADD1] THEN ONCE_REWRITE_TAC [ADD_COMM] THEN 1808 SIMP_TAC std_ss [GSYM SUM_TWO] THEN 1809 Q_TAC SUFF_TAC `{n' | n' IN 0 .. n /\ inv (&FACT n') * (0:real) pow n' <> 0} = {0}` THENL 1810 [DISCH_TAC, 1811 SIMP_TAC std_ss [EXTENSION, GSPECIFICATION, IN_SING, IN_NUMSEG] THEN 1812 GEN_TAC THEN EQ_TAC THENL 1813 [STRIP_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC [MONO_NOT_EQ] THEN 1814 RW_TAC arith_ss [] THEN `0 < x''` by METIS_TAC [LESS_0_CASES] THEN 1815 FULL_SIMP_TAC std_ss [SUC_PRE] THEN 1816 POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN 1817 ONCE_ASM_REWRITE_TAC [] THEN SIMP_TAC arith_ss [POW_0] THEN 1818 REAL_ARITH_TAC, ALL_TAC] THEN 1819 DISC_RW_KILL THEN SIMP_TAC real_ss [FACT, pow] THEN 1820 SIMP_TAC real_ss [REAL_INV_1OVER]] THEN 1821 ASM_REWRITE_TAC [] THEN FIRST_X_ASSUM (MP_TAC o Q.SPECL [`0`,`{}`]) THEN 1822 ASM_SIMP_TAC real_ss [FINITE_EMPTY, NOT_IN_EMPTY, FACT, pow, REAL_INV_1OVER] THEN 1823 DISCH_TAC THEN SIMP_TAC real_ss [SUM_1, FACT, pow, REAL_ADD_RID_UNIQ] THEN 1824 Q_TAC SUFF_TAC `(!n:num. n >= 1 ==> ((\n'. 1 / &FACT n' * 0 pow n') n = 0:real))` THENL 1825 [DISCH_THEN (MP_TAC o MATCH_MP SUM_ZERO) THEN DISCH_THEN (MATCH_MP_TAC) THEN 1826 ARITH_TAC, ALL_TAC] THEN 1827 RW_TAC arith_ss [GE] THEN `0 < n'` by (ASM_SIMP_TAC arith_ss []) THEN 1828 FULL_SIMP_TAC std_ss [SUC_PRE] THEN 1829 POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN 1830 ONCE_ASM_REWRITE_TAC [] THEN SIMP_TAC real_ss [POW_0], 1831 ALL_TAC] THEN 1832 Q_TAC SUFF_TAC `!n. inv (&FACT n) * x pow n <> 0` THENL 1833 [DISCH_TAC, 1834 GEN_TAC THEN MATCH_MP_TAC REAL_MUL_NZ THEN ASM_SIMP_TAC std_ss [POW_NZ] THEN 1835 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN 1836 MATCH_MP_TAC REAL_INV_POS THEN SIMP_TAC arith_ss [REAL_LT, FACT_LESS]] THEN 1837 ASM_SIMP_TAC real_ss [] THEN 1838 Q_TAC SUFF_TAC `(\p v. 1839 (!n s. FINITE s ==> (x' (n INSERT s) = if n IN s then x' s else v n + x' s)) ==> 1840 (sum (FST p, SUC (SND p) - FST p) v = x' {n' | n' IN (FST p) .. (SND p)})) 1841 (0, n) (\n. inv (&FACT n) * x pow n)` THENL 1842 [ASM_SIMP_TAC arith_ss [], ALL_TAC] THEN MATCH_MP_TAC sum_ind THEN RW_TAC std_ss [] THENL 1843 [SIMP_TAC arith_ss [SUM_1, IN_NUMSEG] THEN 1844 ASM_CASES_TAC ``n' = 0:num`` THENL 1845 [ASM_SIMP_TAC arith_ss [SUM_1] THEN 1846 ONCE_REWRITE_TAC [SET_RULE ``{n'':num | n'' = 0} = {0}``] THEN 1847 FIRST_X_ASSUM (MP_TAC o Q.SPECL [`0`,`{}`]) THEN 1848 ASM_SIMP_TAC real_ss [FINITE_EMPTY, NOT_IN_EMPTY, FACT, pow, REAL_INV_1OVER] THEN 1849 DISCH_THEN (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN 1850 ASM_SIMP_TAC real_ss [], ALL_TAC] THEN 1851 `1 - n' = 0` by (ASM_SIMP_TAC arith_ss []) THEN 1852 Q_TAC SUFF_TAC `{n'' | n' <= n'' /\ (n'' = 0)} = {}` THENL 1853 [DISC_RW_KILL, ASM_SIMP_TAC arith_ss [EXTENSION, NOT_IN_EMPTY, GSPECIFICATION]] THEN 1854 ASM_SIMP_TAC real_ss [sum], ALL_TAC] THEN 1855 FULL_SIMP_TAC std_ss [] THEN 1856 ONCE_REWRITE_TAC [SET_RULE ``{n'' | n'' IN n' .. SUC m} = (n' .. SUC m)``] THEN 1857 ASM_CASES_TAC ``SUC m < n'`` THENL 1858 [`(n' .. SUC m) = {}` by METIS_TAC [NUMSEG_EMPTY] THEN 1859 `SUC (SUC m) - n' = 0` by ASM_SIMP_TAC arith_ss [] THEN 1860 ASM_SIMP_TAC std_ss [sum], ALL_TAC] THEN 1861 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN 1862 POP_ASSUM (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN 1863 FIRST_X_ASSUM (MP_TAC o Q.SPECL [`SUC (m)`,`(n' .. m)`]) THEN 1864 RW_TAC arith_ss [FINITE_NUMSEG, IN_NUMSEG] THEN 1865 Q_TAC SUFF_TAC `(SUC m INSERT (n' .. m)) = (n' .. m + 1)` THENL 1866 [DISCH_TAC THEN FULL_SIMP_TAC arith_ss [GSYM ADD1], 1867 ASM_SIMP_TAC arith_ss [EXTENSION, IN_NUMSEG, IN_INSERT, ADD1]] THEN 1868 `{n'' | n'' IN n' .. m} = (n' .. m)` by SET_TAC [] THEN 1869 FULL_SIMP_TAC std_ss [] THEN 1870 `SUC (SUC m) - n' = SUC (SUC m - n')` by ASM_SIMP_TAC arith_ss [] THEN 1871 ASM_SIMP_TAC std_ss [] THEN ONCE_REWRITE_TAC [sum] THEN 1872 ASM_SIMP_TAC arith_ss [REAL_ADD_COMM]); 1873 1874val lemma_sums_eq = prove ( 1875 ``!l x. (seq$sums (\n. ((\n. inv(&(FACT n)))) n * (x pow n)) l) = 1876 ((\n. ((\n. inv(&(FACT n)))) n * (x pow n)) sums l) UNIV``, 1877 RW_TAC std_ss [sums, seqTheory.sums, LIM_SEQUENTIALLY, SEQ, GE] THEN 1878 EQ_TAC THEN RW_TAC std_ss [INTER_UNIV] THEN 1879 FIRST_X_ASSUM (MP_TAC o Q.SPEC `e`) THEN 1880 ASM_REWRITE_TAC [] THEN STRIP_TAC THENL 1881 [Q.EXISTS_TAC `N` THEN RW_TAC std_ss [] THEN 1882 FIRST_X_ASSUM (MP_TAC o Q.SPEC `SUC n`) THEN 1883 ASM_SIMP_TAC arith_ss [dist] THEN 1884 REWRITE_TAC [SIMP_RULE std_ss [] lemma_sum_eq], 1885 ALL_TAC] THEN 1886 Q.EXISTS_TAC `SUC N` THEN RW_TAC std_ss [] THEN 1887 FIRST_X_ASSUM (MP_TAC o Q.SPEC `PRE n`) THEN 1888 ASM_SIMP_TAC arith_ss [dist] THEN 1889 `?m. PRE n = m` by ASM_SIMP_TAC arith_ss [] THEN 1890 `n = SUC m` by ASM_SIMP_TAC arith_ss [] THEN 1891 ASM_REWRITE_TAC [SIMP_RULE std_ss [] lemma_sum_eq]); 1892 1893val EXP_CONVERGES = store_thm ("EXP_CONVERGES", 1894 ``!z. ((\n. z pow n / (&(FACT n))) sums exp(z)) (from 0)``, 1895 SIMP_TAC std_ss [exp] THEN 1896 Q_TAC SUFF_TAC `!z. suminf (\n. inv (&FACT n) * z pow n) = 1897 infsum UNIV (\n. inv (&FACT n) * z pow n)` THENL 1898 [DISC_RW_KILL, 1899 SIMP_TAC std_ss [suminf, infsum] THEN 1900 SIMP_TAC std_ss [FROM_0, SIMP_RULE std_ss [] (GSYM lemma_sums_eq)]] THEN 1901 ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN REWRITE_TAC [GSYM real_div, FROM_0] THEN 1902 GEN_TAC THEN SIMP_TAC std_ss [SUMS_INFSUM, summable, SERIES_CAUCHY] THEN 1903 REWRITE_TAC[INTER_UNIV] THEN 1904 MP_TAC(Q.SPEC `abs(z) + &1` EXP_CONVERGES_UNIFORMLY_CAUCHY) THEN 1905 SIMP_TAC std_ss [REAL_ARITH ``&0 <= x ==> &0 < x + &1:real``, ABS_POS] THEN 1906 METIS_TAC [REAL_ARITH ``x:real <= x + &1``]); 1907 1908val EXP_CONVERGES_UNIQUE = store_thm ("EXP_CONVERGES_UNIQUE", 1909 ``!w z. ((\n. z pow n / (&(FACT n))) sums w) (from 0) <=> (w = exp(z))``, 1910 REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC std_ss [EXP_CONVERGES] THEN 1911 DISCH_THEN(MP_TAC o C CONJ (Q.SPEC `z` EXP_CONVERGES)) THEN 1912 REWRITE_TAC[SERIES_UNIQUE]); 1913 1914val EXP_CONVERGES_UNIFORMLY = store_thm ("EXP_CONVERGES_UNIFORMLY", 1915 ``!R e. &0 < R /\ &0 < e 1916 ==> ?N. !n z. n >= N /\ abs(z) < R 1917 ==> abs(sum((0:num)..n) (\i. z pow i / (&(FACT i))) - exp(z)) <= e``, 1918 REPEAT STRIP_TAC THEN 1919 MP_TAC(Q.SPECL [`R:real`, `e / &2`] EXP_CONVERGES_UNIFORMLY_CAUCHY) THEN 1920 ASM_REWRITE_TAC[REAL_HALF] THEN STRIP_TAC THEN Q.EXISTS_TAC `N` THEN 1921 MAP_EVERY X_GEN_TAC [``n:num``, ``z:real``] THEN STRIP_TAC THEN 1922 MP_TAC(Q.SPEC `z` EXP_CONVERGES) THEN 1923 SIMP_TAC std_ss [sums, LIM_SEQUENTIALLY, FROM_0, INTER_UNIV, dist] THEN 1924 DISCH_THEN(MP_TAC o Q.SPEC `e / &2`) THEN ASM_REWRITE_TAC[REAL_HALF] THEN 1925 DISCH_THEN(X_CHOOSE_THEN ``M:num`` (MP_TAC o Q.SPEC `n + M + 1`)) THEN 1926 FIRST_X_ASSUM(MP_TAC o Q.SPECL [`n + 1`, `n + M + 1`, `z`]) THEN 1927 ASM_SIMP_TAC std_ss [ARITH_PROVE ``(n >= N ==> n + 1 >= N) /\ M <= n + M + 1:num``] THEN 1928 ASM_SIMP_TAC std_ss [REAL_LT_IMP_LE, LE_0] THEN 1929 Q.ABBREV_TAC `f = (\i. z pow i / &FACT i)` THEN 1930 `0 <= n + 1` by ASM_SIMP_TAC arith_ss [] THEN 1931 ONCE_REWRITE_TAC [ARITH_PROVE ``n + M + 1 = n + (M + 1:num)``] THEN 1932 FIRST_X_ASSUM (MP_TAC o MATCH_MP SUM_ADD_SPLIT) THEN 1933 DISCH_THEN (ASSUME_TAC o Q.SPECL [`f`,`M + 1`]) THEN 1934 ONCE_ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN 1935 GEN_REWR_TAC (RAND_CONV o RAND_CONV o RAND_CONV) [GSYM REAL_HALF] THEN 1936 REAL_ARITH_TAC); 1937 1938val HAS_DERIVATIVE_EXP = store_thm ("HAS_DERIVATIVE_EXP", 1939 ``!z. (exp has_derivative (\y. exp z * y)) (at z)``, 1940 REPEAT GEN_TAC THEN MP_TAC(Q.ISPECL 1941 [`ball((&0),abs(z:real) + &1)`, 1942 `\n z. z pow n / (&(FACT n):real)`, 1943 `\n z:real. if n = 0 then (&0) else z pow (n-1) / (&(FACT(n-1)))`, 1944 `exp:real->real`, `from (0)`] 1945 HAS_DERIVATIVE_SERIES') THEN 1946 SIMP_TAC real_ss [CONVEX_BALL, OPEN_BALL, IN_BALL, dist] THEN 1947 SIMP_TAC real_ss [HAS_DERIVATIVE_WITHIN_OPEN, OPEN_BALL, IN_BALL, 1948 dist, REAL_SUB_LZERO, REAL_SUB_RZERO, ABS_NEG] THEN 1949 Q_TAC SUFF_TAC `(!n x. 1950 abs x < abs z + 1 ==> 1951 ((\z. z pow n / &FACT n) has_derivative 1952 (\y. (if n = 0 then 0 else x pow (n - 1) / &FACT (n - 1)) * y)) 1953 (at x)) /\ 1954 (!e. 0 < e ==> 1955 ?N. !n x. n >= N /\ abs x < abs z + 1 ==> 1956 abs (sum (from 0 INTER (0 .. n)) 1957 (\i. if i = 0 then 0 else x pow (i - 1) / &FACT (i - 1)) - 1958 exp x) <= e) /\ 1959 (?x l. abs x < abs z + 1 /\ ((\n. x pow n / &FACT n) sums l) (from 0))` THENL 1960 [DISCH_TAC THEN ASM_REWRITE_TAC [] THEN POP_ASSUM K_TAC THEN 1961 DISCH_THEN(X_CHOOSE_THEN ``g:real->real`` MP_TAC) THEN 1962 REWRITE_TAC[EXP_CONVERGES_UNIQUE] THEN STRIP_TAC THEN 1963 MATCH_MP_TAC HAS_DERIVATIVE_TRANSFORM_AT THEN 1964 MAP_EVERY Q.EXISTS_TAC [`g`, `&1`] THEN 1965 REWRITE_TAC[REAL_LT_01] THEN CONJ_TAC THENL 1966 [ALL_TAC, 1967 FIRST_X_ASSUM(MP_TAC o Q.SPEC `z`) THEN 1968 Q_TAC SUFF_TAC `abs z < abs z + 1` THENL 1969 [METIS_TAC [ETA_AX], REAL_ARITH_TAC]] THEN 1970 GEN_TAC THEN POP_ASSUM (MP_TAC o Q.SPEC `x'`) THEN 1971 MATCH_MP_TAC MONO_IMP THEN SIMP_TAC std_ss [dist] THEN 1972 REAL_ARITH_TAC, ALL_TAC] THEN 1973 REPEAT CONJ_TAC THENL 1974 [ALL_TAC, 1975 REPEAT STRIP_TAC THEN 1976 MP_TAC(Q.SPECL [`abs(z) + &1`, `e`] EXP_CONVERGES_UNIFORMLY) THEN 1977 ASM_SIMP_TAC std_ss [ABS_POS, REAL_ARITH ``&0 <= x ==> &0 < x + &1:real``] THEN 1978 DISCH_THEN(X_CHOOSE_TAC ``N:num``) THEN Q.EXISTS_TAC `N + 1` THEN 1979 MAP_EVERY X_GEN_TAC [``n:num``, ``w:real``] THEN STRIP_TAC THEN 1980 FIRST_X_ASSUM(MP_TAC o Q.SPECL [`n - 1`, `w`]) THEN 1981 ASM_SIMP_TAC std_ss [ARITH_PROVE ``n >= m + 1 ==> n - 1 >= m:num``] THEN 1982 REWRITE_TAC[FROM_0, INTER_UNIV] THEN MATCH_MP_TAC EQ_IMPLIES THEN 1983 AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN 1984 AP_THM_TAC THEN AP_TERM_TAC THEN 1985 SUBGOAL_THEN ``((0:num)..n) = 0 INSERT (IMAGE SUC ((0:num)..n-1))`` SUBST1_TAC THENL 1986 [REWRITE_TAC[EXTENSION, IN_INSERT, IN_IMAGE, IN_NUMSEG] THEN 1987 INDUCT_TAC THEN SIMP_TAC arith_ss [] THEN 1988 UNDISCH_TAC ``n >= N + 1:num`` THEN ARITH_TAC, 1989 ALL_TAC] THEN 1990 SIMP_TAC std_ss [SUM_CLAUSES, IMAGE_FINITE, FINITE_NUMSEG] THEN 1991 SIMP_TAC real_ss [IN_IMAGE, NOT_SUC, SUC_NOT, REAL_ADD_LID] THEN 1992 SIMP_TAC std_ss [SUM_IMAGE, FINITE_NUMSEG] THEN 1993 MATCH_MP_TAC SUM_EQ THEN SIMP_TAC real_ss [IN_NUMSEG, NOT_SUC, o_THM, SUC_SUB1], 1994 MAP_EVERY Q.EXISTS_TAC [`(&0)`, `exp((&0))`] THEN 1995 REWRITE_TAC[EXP_CONVERGES, ABS_0] THEN 1996 SIMP_TAC std_ss [REAL_ARITH ``&0 <= z ==> &0 < z + &1:real``, ABS_POS]] THEN 1997 X_GEN_TAC ``n:num`` THEN REPEAT STRIP_TAC THEN 1998 ASM_CASES_TAC ``n = 0:num`` THEN ASM_REWRITE_TAC [] THENL 1999 [SIMP_TAC real_ss [pow, FACT, HAS_DERIVATIVE_CONST], ALL_TAC] THEN 2000 SIMP_TAC std_ss [real_div] THEN ONCE_REWRITE_TAC [REAL_MUL_COMM] THEN 2001 ONCE_REWRITE_TAC [REAL_ARITH ``a * (b * c) = c * b * a:real``] THEN 2002 Q_TAC SUFF_TAC `!y. inv (&FACT (n - 1)) * x pow (n - 1) * y = 2003 inv (&FACT n) * (&n * x pow (n - 1) * y)` THENL 2004 [DISC_RW_KILL, 2005 RW_TAC real_ss [REAL_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN 2006 AP_THM_TAC THEN AP_TERM_TAC THEN `0 < n` by ASM_SIMP_TAC arith_ss [] THEN 2007 `?m. n = SUC m` by (Q.EXISTS_TAC `PRE n` THEN ASM_SIMP_TAC arith_ss [SUC_PRE]) THEN 2008 ASM_SIMP_TAC std_ss [SUC_SUB1, FACT, GSYM REAL_OF_NUM_MUL] THEN 2009 `~(&SUC m = &0:real)` by ASM_SIMP_TAC arith_ss [NOT_SUC, REAL_OF_NUM_EQ] THEN 2010 ASM_SIMP_TAC real_ss [REAL_FACT_NZ, REAL_INV_MUL] THEN 2011 ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c = a * c * b:real``] THEN 2012 ASM_SIMP_TAC real_ss [REAL_MUL_LINV]] THEN 2013 Q_TAC SUFF_TAC `((\z. inv (&FACT n) * (\z. z pow n) z) has_derivative 2014 (\y. inv (&FACT n) * (\y. (&n * x pow (n - 1) * y)) y)) (at x)` THENL 2015 [SIMP_TAC std_ss [], ALL_TAC] THEN 2016 MATCH_MP_TAC HAS_DERIVATIVE_CMUL THEN 2017 Q_TAC SUFF_TAC `(\y. &n * x pow (n - 1) * y) = 2018 (\y. sum (1 .. n) (\i. x pow (n - i) * y * x pow (i - 1)))` THENL 2019 [DISC_RW_KILL THEN SIMP_TAC std_ss [HAS_DERIVATIVE_POW], ALL_TAC] THEN 2020 `FINITE (1 .. n)` by SIMP_TAC std_ss [FINITE_NUMSEG] THEN 2021 POP_ASSUM (MP_TAC o MATCH_MP SUM_CONST) THEN 2022 DISCH_THEN (MP_TAC o Q.SPEC `x pow (n - 1)`) THEN SIMP_TAC arith_ss [CARD_NUMSEG] THEN 2023 DISCH_THEN (ASSUME_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) THEN 2024 ASM_REWRITE_TAC [] THEN ONCE_REWRITE_TAC [REAL_ARITH ``a * b * c = (a * c) * b:real``] THEN 2025 ABS_TAC THEN SIMP_TAC std_ss [SUM_RMUL] THEN AP_THM_TAC THEN AP_TERM_TAC THEN 2026 MATCH_MP_TAC SUM_EQ THEN SIMP_TAC arith_ss [GSYM POW_ADD, IN_NUMSEG]); 2027 2028val HAS_DERIVATIVE_IMP_CONTINUOUS_AT = store_thm ("HAS_DERIVATIVE_IMP_CONTINUOUS_AT", 2029 ``!f f' x. (f has_derivative f') (at x) ==> f continuous at x``, 2030 RW_TAC std_ss [] THEN MATCH_MP_TAC DIFFERENTIABLE_IMP_CONTINUOUS_AT THEN 2031 METIS_TAC[differentiable]); 2032 2033val CONTINUOUS_AT_EXP = store_thm ("CONTINUOUS_AT_EXP", 2034 ``!z. exp continuous at z``, 2035 METIS_TAC[HAS_DERIVATIVE_EXP, HAS_DERIVATIVE_IMP_CONTINUOUS_AT]); 2036 2037val CONTINUOUS_WITHIN_EXP = store_thm ("CONTINUOUS_WITHIN_EXP", 2038 ``!s z. exp continuous (at z within s)``, 2039 METIS_TAC[CONTINUOUS_AT_WITHIN, CONTINUOUS_AT_EXP]); 2040 2041val CONTINUOUS_ON_EXP = store_thm ("CONTINUOUS_ON_EXP", 2042 ``!s. exp continuous_on s``, 2043 METIS_TAC[CONTINUOUS_AT_IMP_CONTINUOUS_ON, CONTINUOUS_AT_EXP]); 2044 2045val _ = export_theory(); 2046