Multivariate/canal.ml

   1 (* ========================================================================= *)
   2 (* Complex analysis.                                                         *)
   3 (*                                                                           *)
   4 (*              (c) Copyright, John Harrison 1998-2008                       *)
   5 (* (c) Copyright, Marco Maggesi, Graziano Gentili and Gianni Ciolli, 2008.   *)
   6 (*              (c) Copyright, Valentina Bruno 2010                          *)
   7 (* ========================================================================= *)
   8
   9 needs "Library/floor.ml";;
  10 needs "Library/iter.ml";;
  11 needs "Multivariate/complexes.ml";;
  12
  13 prioritize_complex();;
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (* Some toplogical facts formulated for the complex numbers.                 *)
  17 (* ------------------------------------------------------------------------- *)
  18
  19 let CLOSED_HALFSPACE_RE_GE = prove
  20  (`!b. closed {z | Re(z) >= b}`,
  21   GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CLOSED_HALFSPACE_GE) THEN
  22   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  23   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  24   REWRITE_TAC[RE_CX; IM_CX; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
  25
  26 let CLOSED_HALFSPACE_RE_LE = prove
  27  (`!b. closed {z | Re(z) <= b}`,
  28   GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CLOSED_HALFSPACE_LE) THEN
  29   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  30   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  31   REWRITE_TAC[RE_CX; IM_CX; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
  32
  33 let CLOSED_HALFSPACE_RE_EQ = prove
  34  (`!b. closed {z | Re(z) = b}`,
  35   GEN_TAC THEN REWRITE_TAC[REAL_ARITH `x = y <=> x >= y /\ x <= y`] THEN
  36   REWRITE_TAC[SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN
  37   SIMP_TAC[CLOSED_INTER; CLOSED_HALFSPACE_RE_GE; CLOSED_HALFSPACE_RE_LE]);;
  38
  39 let OPEN_HALFSPACE_RE_GT = prove
  40  (`!b. open {z | Re(z) > b}`,
  41   REWRITE_TAC[OPEN_CLOSED; CLOSED_HALFSPACE_RE_LE;
  42               REAL_ARITH `x > y <=> ~(x <= y)`;
  43               SET_RULE `UNIV DIFF {x | ~p x} = {x | p x}`]);;
  44
  45 let OPEN_HALFSPACE_RE_LT = prove
  46  (`!b. open {z | Re(z) < b}`,
  47   REWRITE_TAC[OPEN_CLOSED; CLOSED_HALFSPACE_RE_GE;
  48               REAL_ARITH `x < y <=> ~(x >= y)`;
  49               SET_RULE `UNIV DIFF {x | ~p x} = {x | p x}`]);;
  50
  51 let CLOSED_HALFSPACE_IM_GE = prove
  52  (`!b. closed {z | Im(z) >= b}`,
  53   GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CLOSED_HALFSPACE_GE) THEN
  54   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  55   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  56   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
  57
  58 let CLOSED_HALFSPACE_IM_LE = prove
  59  (`!b. closed {z | Im(z) <= b}`,
  60   GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CLOSED_HALFSPACE_LE) THEN
  61   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  62   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  63   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
  64
  65 let CLOSED_HALFSPACE_IM_EQ = prove
  66  (`!b. closed {z | Im(z) = b}`,
  67   GEN_TAC THEN REWRITE_TAC[REAL_ARITH `x = y <=> x >= y /\ x <= y`] THEN
  68   REWRITE_TAC[SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN
  69   SIMP_TAC[CLOSED_INTER; CLOSED_HALFSPACE_IM_GE; CLOSED_HALFSPACE_IM_LE]);;
  70
  71 let OPEN_HALFSPACE_IM_GT = prove
  72  (`!b. open {z | Im(z) > b}`,
  73   REWRITE_TAC[OPEN_CLOSED; CLOSED_HALFSPACE_IM_LE;
  74               REAL_ARITH `x > y <=> ~(x <= y)`;
  75               SET_RULE `UNIV DIFF {x | ~p x} = {x | p x}`]);;
  76
  77 let OPEN_HALFSPACE_IM_LT = prove
  78  (`!b. open {z | Im(z) < b}`,
  79   REWRITE_TAC[OPEN_CLOSED; CLOSED_HALFSPACE_IM_GE;
  80               REAL_ARITH `x < y <=> ~(x >= y)`;
  81               SET_RULE `UNIV DIFF {x | ~p x} = {x | p x}`]);;
  82
  83 let CONVEX_HALFSPACE_RE_GE = prove
  84  (`!b. convex {z | Re(z) >= b}`,
  85   GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CONVEX_HALFSPACE_GE) THEN
  86   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  87   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  88   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
  89
  90 let CONVEX_HALFSPACE_RE_GT = prove
  91  (`!b. convex {z | Re(z) > b}`,
  92   GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CONVEX_HALFSPACE_GT) THEN
  93   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  94   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  95   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
  96
  97 let CONVEX_HALFSPACE_RE_LE = prove
  98  (`!b. convex {z | Re(z) <= b}`,
  99   GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CONVEX_HALFSPACE_LE) THEN
 100   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
 101   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
 102   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
 103
 104 let CONVEX_HALFSPACE_RE_LT = prove
 105  (`!b. convex {z | Re(z) < b}`,
 106   GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CONVEX_HALFSPACE_LT) THEN
 107   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
 108   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
 109   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
 110
 111 let CONVEX_HALFSPACE_IM_GE = prove
 112  (`!b. convex {z | Im(z) >= b}`,
 113   GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CONVEX_HALFSPACE_GE) THEN
 114   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
 115   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
 116   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
 117
 118 let CONVEX_HALFSPACE_IM_GT = prove
 119  (`!b. convex {z | Im(z) > b}`,
 120   GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CONVEX_HALFSPACE_GT) THEN
 121   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
 122   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
 123   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
 124
 125 let CONVEX_HALFSPACE_IM_LE = prove
 126  (`!b. convex {z | Im(z) <= b}`,
 127   GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CONVEX_HALFSPACE_LE) THEN
 128   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
 129   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
 130   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
 131
 132 let CONVEX_HALFSPACE_IM_LT = prove
 133  (`!b. convex {z | Im(z) < b}`,
 134   GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CONVEX_HALFSPACE_LT) THEN
 135   MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
 136   REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
 137   REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;
 138
 139 let COMPLEX_IN_BALL_0 = prove
 140  (`!v r. v IN ball(Cx(&0),r) <=> norm v < r`,
 141   REWRITE_TAC [GSYM COMPLEX_VEC_0; IN_BALL_0]);;
 142
 143 let COMPLEX_IN_CBALL_0 = prove
 144  (`!v r. v IN cball(Cx(&0),r) <=> norm v <= r`,
 145   REWRITE_TAC [GSYM COMPLEX_VEC_0; IN_CBALL_0]);;
 146
 147 let COMPLEX_IN_SPHERE_0 = prove
 148  (`!v r. v IN sphere(Cx(&0),r) <=> norm v = r`,
 149   REWRITE_TAC [GSYM COMPLEX_VEC_0; IN_SPHERE_0]);;
 150
 151 let IN_BALL_RE = prove
 152  (`!x z e. x IN ball(z,e) ==> abs(Re(x) - Re(z)) < e`,
 153   REPEAT GEN_TAC THEN REWRITE_TAC[IN_BALL; dist] THEN
 154   MP_TAC(SPEC `z - x:complex` COMPLEX_NORM_GE_RE_IM) THEN
 155   REWRITE_TAC[RE_SUB] THEN REAL_ARITH_TAC);;
 156
 157 let IN_BALL_IM = prove
 158  (`!x z e. x IN ball(z,e) ==> abs(Im(x) - Im(z)) < e`,
 159   REPEAT GEN_TAC THEN REWRITE_TAC[IN_BALL; dist] THEN
 160   MP_TAC(SPEC `z - x:complex` COMPLEX_NORM_GE_RE_IM) THEN
 161   REWRITE_TAC[IM_SUB] THEN REAL_ARITH_TAC);;
 162
 163 let IN_CBALL_RE = prove
 164  (`!x z e. x IN cball(z,e) ==> abs(Re(x) - Re(z)) <= e`,
 165   REPEAT GEN_TAC THEN REWRITE_TAC[IN_CBALL; dist] THEN
 166   MP_TAC(SPEC `z - x:complex` COMPLEX_NORM_GE_RE_IM) THEN
 167   REWRITE_TAC[RE_SUB] THEN REAL_ARITH_TAC);;
 168
 169 let IN_CBALL_IM = prove
 170  (`!x z e. x IN cball(z,e) ==> abs(Im(x) - Im(z)) <= e`,
 171   REPEAT GEN_TAC THEN REWRITE_TAC[IN_CBALL; dist] THEN
 172   MP_TAC(SPEC `z - x:complex` COMPLEX_NORM_GE_RE_IM) THEN
 173   REWRITE_TAC[IM_SUB] THEN REAL_ARITH_TAC);;
 174
 175 let CLOSED_REAL_SET = prove
 176  (`closed {z | real z}`,
 177   REWRITE_TAC[CLOSED_HALFSPACE_IM_EQ; real]);;
 178
 179 let CLOSED_REAL = prove
 180  (`closed real`,
 181   GEN_REWRITE_TAC RAND_CONV [SET_RULE `s = {x | s x}`] THEN
 182   REWRITE_TAC[CLOSED_REAL_SET]);;
 183
 184 let UNBOUNDED_REAL = prove
 185  (`~(bounded real)`,
 186   REWRITE_TAC[bounded; IN; REAL_EXISTS; LEFT_IMP_EXISTS_THM] THEN
 187   MESON_TAC[COMPLEX_NORM_CX; REAL_ARITH `~(abs(abs B + &1) <= B)`]);;
 188
 189 let CONNECTED_REAL = prove
 190  (`connected real`,
 191   SIMP_TAC[CONVEX_REAL; CONVEX_CONNECTED]);;
 192
 193 let PATH_CONNECTED_REAL = prove
 194  (`path_connected real`,
 195   SIMP_TAC[CONVEX_REAL; CONVEX_IMP_PATH_CONNECTED]);;
 196
 197 let TRIVIAL_LIMIT_WITHIN_REAL = prove
 198  (`!z. trivial_limit (at z within real) <=> ~(real z)`,
 199   GEN_TAC THEN REWRITE_TAC[TRIVIAL_LIMIT_WITHIN] THEN
 200   AP_TERM_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM IN] THEN
 201   MATCH_MP_TAC CONNECTED_IMP_PERFECT_CLOSED THEN
 202   REWRITE_TAC[CONNECTED_REAL; CLOSED_REAL] THEN
 203   MESON_TAC[UNBOUNDED_REAL; BOUNDED_SING]);;
 204
 205 (* ------------------------------------------------------------------------- *)
 206 (* Complex-specific uniform limit composition theorems.                      *)
 207 (* ------------------------------------------------------------------------- *)
 208
 209 let UNIFORM_LIM_COMPLEX_MUL = prove
 210  (`!net:(A)net P f g l m b1 b2.
 211         eventually (\x. !n. P n ==> norm(l n) <= b1) net /\
 212         eventually (\x. !n. P n ==> norm(m n) <= b2) net /\
 213         (!e. &0 < e
 214              ==> eventually (\x. !n:B. P n ==> norm(f n x - l n) < e) net) /\
 215         (!e. &0 < e
 216              ==> eventually (\x. !n. P n ==> norm(g n x - m n) < e) net)
 217         ==> !e. &0 < e
 218                 ==> eventually
 219                      (\x. !n. P n
 220                               ==> norm(f n x * g n x - l n * m n) < e)
 221                      net`,
 222   REPEAT GEN_TAC THEN
 223   DISCH_THEN(MP_TAC o CONJ BILINEAR_COMPLEX_MUL) THEN
 224   REWRITE_TAC[UNIFORM_LIM_BILINEAR]);;
 225
 226 let UNIFORM_LIM_COMPLEX_INV = prove
 227  (`!net:(A)net P f l b.
 228         (!e. &0 < e
 229              ==> eventually (\x. !n:B. P n ==> norm(f n x - l n) < e) net) /\
 230         &0 < b /\ eventually (\x. !n. P n ==> b <= norm(l n)) net
 231         ==> !e. &0 < e
 232                 ==> eventually
 233                     (\x. !n. P n ==> norm(inv(f n x) - inv(l n)) < e) net`,
 234   REPEAT STRIP_TAC THEN MATCH_MP_TAC EVENTUALLY_MONO THEN
 235   EXISTS_TAC
 236    `\x. !n. P n ==> b <= norm(l n) /\
 237                     b / &2 <= norm((f:B->A->complex) n x) /\
 238                     norm(f n x - l n) < e * b pow 2 / &2` THEN
 239   REWRITE_TAC[TAUT `(p ==> q /\ r) <=> (p ==> q) /\ (p ==> r)`] THEN
 240   REWRITE_TAC[FORALL_AND_THM] THEN CONJ_TAC THENL
 241    [X_GEN_TAC `x:A` THEN STRIP_TAC THEN X_GEN_TAC `n:B` THEN DISCH_TAC THEN
 242     REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `n:B`) THEN ASM_REWRITE_TAC[]) THEN
 243     REPEAT DISCH_TAC THEN
 244     SUBGOAL_THEN `~((f:B->A->complex) n x = Cx(&0)) /\ ~(l n = Cx(&0))`
 245     STRIP_ASSUME_TAC THENL
 246      [CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
 247       RULE_ASSUM_TAC(REWRITE_RULE[COMPLEX_NORM_CX]) THEN ASM_REAL_ARITH_TAC;
 248       ALL_TAC] THEN
 249     ASM_SIMP_TAC[COMPLEX_FIELD
 250      `~(x = Cx(&0)) /\ ~(y = Cx(&0))
 251       ==> inv x - inv y = (y - x) / (x * y)`] THEN
 252     ASM_SIMP_TAC[COMPLEX_NORM_DIV; REAL_LT_LDIV_EQ; COMPLEX_NORM_NZ;
 253                  COMPLEX_ENTIRE] THEN
 254     ONCE_REWRITE_TAC[NORM_SUB] THEN
 255     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
 256         REAL_LTE_TRANS)) THEN
 257     ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_ARITH `b pow 2 / &2 = b / &2 * b`] THEN
 258     REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
 259     ASM_REAL_ARITH_TAC;
 260     ASM_REWRITE_TAC[EVENTUALLY_AND] THEN CONJ_TAC THENL
 261      [FIRST_X_ASSUM(MP_TAC o SPEC `b / &2`) THEN
 262       ASM_REWRITE_TAC[REAL_HALF] THEN
 263       FIRST_X_ASSUM(fun th -> MP_TAC th THEN REWRITE_TAC[IMP_IMP] THEN
 264         GEN_REWRITE_TAC LAND_CONV [GSYM EVENTUALLY_AND]) THEN
 265       MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
 266       REWRITE_TAC[] THEN
 267       ASM_MESON_TAC[NORM_ARITH
 268        `b <= norm l /\ norm(f - l) < b / &2 ==> b / &2 <= norm f`];
 269       FIRST_X_ASSUM MATCH_MP_TAC THEN
 270       ASM_SIMP_TAC[REAL_HALF; REAL_POW_LT; REAL_LT_MUL]]]);;
 271
 272 let UNIFORM_LIM_COMPLEX_DIV = prove
 273  (`!net:(A)net P f g l m b1 b2.
 274         eventually (\x. !n. P n ==> norm(l n) <= b1) net /\
 275         &0 < b2 /\ eventually (\x. !n. P n ==> b2 <= norm(m n)) net /\
 276         (!e. &0 < e
 277              ==> eventually (\x. !n:B. P n ==> norm(f n x - l n) < e) net) /\
 278         (!e. &0 < e
 279              ==> eventually (\x. !n. P n ==> norm(g n x - m n) < e) net)
 280         ==> !e. &0 < e
 281                 ==> eventually
 282                      (\x. !n. P n
 283                               ==> norm(f n x / g n x - l n / m n) < e)
 284                      net`,
 285   REPEAT GEN_TAC THEN DISCH_TAC THEN
 286   REWRITE_TAC[complex_div] THEN MATCH_MP_TAC UNIFORM_LIM_COMPLEX_MUL THEN
 287   MAP_EVERY EXISTS_TAC [`b1:real`; `inv(b2):real`] THEN
 288   ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 289    [FIRST_X_ASSUM(CONJUNCTS_THEN2 ASSUME_TAC
 290      (MP_TAC o CONJUNCT1) o CONJUNCT2) THEN
 291     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
 292     GEN_TAC THEN REWRITE_TAC[] THEN MATCH_MP_TAC MONO_FORALL THEN
 293     REPEAT STRIP_TAC THEN REWRITE_TAC[COMPLEX_NORM_INV] THEN
 294     MATCH_MP_TAC REAL_LE_INV2 THEN ASM_SIMP_TAC[];
 295     MATCH_MP_TAC UNIFORM_LIM_COMPLEX_INV THEN
 296     EXISTS_TAC `b2:real` THEN ASM_REWRITE_TAC[]]);;
 297
 298 (* ------------------------------------------------------------------------- *)
 299 (* The usual non-uniform versions.                                           *)
 300 (* ------------------------------------------------------------------------- *)
 301
 302 let LIM_COMPLEX_MUL = prove
 303  (`!net:(A)net f g l m.
 304          (f --> l) net /\ (g --> m) net ==> ((\x. f x * g x) --> l * m) net`,
 305   SIMP_TAC[LIM_BILINEAR; BILINEAR_COMPLEX_MUL]);;
 306
 307 let LIM_COMPLEX_INV = prove
 308  (`!net:(A)net f g l m.
 309          (f --> l) net /\ ~(l = Cx(&0)) ==> ((\x. inv(f x)) --> inv(l)) net`,
 310   REPEAT STRIP_TAC THEN
 311   MP_TAC(ISPECL
 312    [`net:(A)net`; `\x:one. T`;
 313     `\n:one. (f:A->complex)`;
 314     `\n:one. (l:complex)`;
 315     `norm(l:complex)`] UNIFORM_LIM_COMPLEX_INV) THEN
 316   ASM_REWRITE_TAC[REAL_LE_REFL; EVENTUALLY_TRUE] THEN
 317   ASM_REWRITE_TAC[GSYM dist; GSYM tendsto; COMPLEX_NORM_NZ]);;
 318
 319 let LIM_COMPLEX_DIV = prove
 320  (`!net:(A)net f g l m.
 321          (f --> l) net /\ (g --> m) net /\ ~(m = Cx(&0))
 322          ==> ((\x. f x / g x) --> l / m) net`,
 323   REPEAT STRIP_TAC THEN REWRITE_TAC[complex_div] THEN
 324   MATCH_MP_TAC LIM_COMPLEX_MUL THEN ASM_SIMP_TAC[LIM_COMPLEX_INV]);;
 325
 326 let LIM_COMPLEX_POW = prove
 327  (`!net:(A)net f l n.
 328          (f --> l) net ==> ((\x. f(x) pow n) --> l pow n) net`,
 329   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
 330   INDUCT_TAC THEN ASM_SIMP_TAC[LIM_COMPLEX_MUL; complex_pow; LIM_CONST]);;
 331
 332 let LIM_COMPLEX_LMUL = prove
 333  (`!f l c. (f --> l) net ==> ((\x. c * f x) --> c * l) net`,
 334   SIMP_TAC[LIM_COMPLEX_MUL; LIM_CONST]);;
 335
 336 let LIM_COMPLEX_RMUL = prove
 337  (`!f l c. (f --> l) net ==> ((\x. f x * c) --> l * c) net`,
 338   SIMP_TAC[LIM_COMPLEX_MUL; LIM_CONST]);;
 339
 340 (* ------------------------------------------------------------------------- *)
 341 (* Mapping real limits between C and R^1.                                    *)
 342 (* ------------------------------------------------------------------------- *)
 343
 344 let LIM_CX_LIFT = prove
 345  (`!net f l.
 346      ((\x. Cx(f x)) --> Cx l) net <=> ((\x. lift(f x)) --> lift l) net`,
 347   REWRITE_TAC[LIM; DIST_LIFT; DIST_CX]);;
 348
 349 let SERIES_CX_LIFT = prove
 350  (`!f s x.
 351      ((\x. Cx(f x)) sums (Cx x)) s <=> ((\x. lift(f x)) sums (lift x)) s`,
 352   SIMP_TAC[sums; LIM_CX_LIFT; VSUM_CX; FINITE_INTER; FINITE_NUMSEG] THEN
 353   REWRITE_TAC[REWRITE_RULE[o_DEF] (GSYM LIFT_SUM)]);;
 354
 355 let LIM_INFINITY_POSINFINITY_CX = prove
 356  (`!f l:real^N. (f --> l) at_infinity ==> ((f o Cx) --> l) at_posinfinity`,
 357   REWRITE_TAC[LIM_AT_INFINITY; LIM_AT_POSINFINITY; o_THM] THEN
 358   MESON_TAC[COMPLEX_NORM_CX; REAL_ARITH `x >= b ==> abs(x) >= b`]);;
 359
 360 (* ------------------------------------------------------------------------- *)
 361 (* Special cases of null limits.                                             *)
 362 (* ------------------------------------------------------------------------- *)
 363
 364 let LIM_NULL_COMPLEX = prove
 365  (`!net f. (f --> l) net <=> ((\x. f x - l) --> Cx(&0)) net`,
 366   REWRITE_TAC[GSYM COMPLEX_VEC_0; GSYM LIM_NULL]);;
 367
 368 let LIM_NULL_COMPLEX_NORM = prove
 369  (`!net f. (f --> Cx(&0)) net <=> ((\x. Cx(norm(f x))) --> Cx(&0)) net`,
 370   REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN
 371   ONCE_REWRITE_TAC[LIM_NULL_NORM] THEN
 372   REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NORM]);;
 373
 374 let LIM_NULL_COMPLEX_NEG = prove
 375  (`!net f. (f --> Cx(&0)) net ==> ((\x. --(f x)) --> Cx(&0)) net`,
 376   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_NEG) THEN
 377   REWRITE_TAC[COMPLEX_NEG_0]);;
 378
 379 let LIM_NULL_COMPLEX_ADD = prove
 380  (`!net f g. (f --> Cx(&0)) net /\ (g --> Cx(&0)) net
 381              ==> ((\x. f x + g x) --> Cx(&0)) net`,
 382   REPEAT GEN_TAC THEN
 383   DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN
 384   REWRITE_TAC[COMPLEX_ADD_LID]);;
 385
 386 let LIM_NULL_COMPLEX_SUB = prove
 387  (`!net f g. (f --> Cx(&0)) net /\ (g --> Cx(&0)) net
 388              ==> ((\x. f x - g x) --> Cx(&0)) net`,
 389   REPEAT GEN_TAC THEN
 390   DISCH_THEN(MP_TAC o MATCH_MP LIM_SUB) THEN
 391   REWRITE_TAC[COMPLEX_SUB_REFL]);;
 392
 393 let LIM_NULL_COMPLEX_MUL = prove
 394  (`!net f g. (f --> Cx(&0)) net /\ (g --> Cx(&0)) net
 395              ==> ((\x. f x * g x) --> Cx(&0)) net`,
 396   REPEAT GEN_TAC THEN
 397   DISCH_THEN(MP_TAC o MATCH_MP LIM_COMPLEX_MUL) THEN
 398   REWRITE_TAC[COMPLEX_MUL_LZERO]);;
 399
 400 let LIM_NULL_COMPLEX_LMUL = prove
 401  (`!net f c. (f --> Cx(&0)) net ==> ((\x. c * f x) --> Cx(&0)) net`,
 402   REPEAT STRIP_TAC THEN SUBST1_TAC(COMPLEX_RING `Cx(&0) = c * Cx(&0)`) THEN
 403   ASM_SIMP_TAC[LIM_COMPLEX_LMUL]);;
 404
 405 let LIM_NULL_COMPLEX_RMUL = prove
 406  (`!net f c. (f --> Cx(&0)) net ==> ((\x. f x * c) --> Cx(&0)) net`,
 407   REPEAT STRIP_TAC THEN SUBST1_TAC(COMPLEX_RING `Cx(&0) = Cx(&0) * c`) THEN
 408   ASM_SIMP_TAC[LIM_COMPLEX_RMUL]);;
 409
 410 let LIM_NULL_COMPLEX_POW = prove
 411  (`!net f n. (f --> Cx(&0)) net /\ ~(n = 0)
 412              ==> ((\x. (f x) pow n) --> Cx(&0)) net`,
 413   REPEAT STRIP_TAC THEN
 414   FIRST_X_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP LIM_COMPLEX_POW) THEN
 415   ASM_REWRITE_TAC[COMPLEX_POW_ZERO]);;
 416
 417 let LIM_NULL_COMPLEX_BOUND = prove
 418  (`!f g. eventually (\n. norm (f n) <= norm (g n)) net /\ (g --> Cx(&0)) net
 419          ==> (f --> Cx(&0)) net`,
 420   REWRITE_TAC[GSYM COMPLEX_VEC_0; LIM_TRANSFORM_BOUND]);;
 421
 422 let SUMS_COMPLEX_0 = prove
 423  (`!f s. (!n. n IN s ==> f n = Cx(&0)) ==> (f sums Cx(&0)) s`,
 424   REWRITE_TAC[GSYM COMPLEX_VEC_0; SUMS_0]);;
 425
 426 let LIM_NULL_COMPLEX_RMUL_BOUNDED = prove
 427  (`!net f g B.
 428         (f --> Cx(&0)) net /\
 429         eventually (\a. f a = Cx(&0) \/ norm(g a) <= B) net
 430         ==> ((\z. f(z) * g(z)) --> Cx(&0)) net`,
 431   REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN
 432   ONCE_REWRITE_TAC[LIM_NULL_NORM] THEN
 433   REWRITE_TAC[LIFT_CMUL; COMPLEX_NORM_MUL] THEN
 434   REPEAT STRIP_TAC THEN MATCH_MP_TAC LIM_NULL_VMUL_BOUNDED THEN
 435   EXISTS_TAC `B:real` THEN
 436   ASM_REWRITE_TAC[o_DEF; NORM_LIFT; REAL_ABS_NORM; NORM_EQ_0]);;
 437
 438 let LIM_NULL_COMPLEX_LMUL_BOUNDED = prove
 439  (`!net f g B.
 440         eventually (\a. norm(f a) <= B \/ g a = Cx(&0)) net /\
 441         (g --> Cx(&0)) net
 442         ==> ((\z. f(z) * g(z)) --> Cx(&0)) net`,
 443   ONCE_REWRITE_TAC[DISJ_SYM; COMPLEX_MUL_SYM] THEN REPEAT STRIP_TAC THEN
 444   MATCH_MP_TAC LIM_NULL_COMPLEX_RMUL_BOUNDED THEN
 445   ASM_MESON_TAC[]);;
 446
 447 (* ------------------------------------------------------------------------- *)
 448 (* Bound results for real and imaginary components of limits.                *)
 449 (* ------------------------------------------------------------------------- *)
 450
 451 let LIM_RE_UBOUND = prove
 452  (`!net:(A)net f l b.
 453         ~(trivial_limit net) /\ (f --> l) net /\
 454         eventually (\x. Re(f x) <= b) net
 455         ==> Re(l) <= b`,
 456   REWRITE_TAC[RE_DEF] THEN REPEAT STRIP_TAC THEN
 457   MP_TAC(ISPECL [`net:(A)net`; `f:A->complex`; `l:complex`; `b:real`; `1`]
 458                 LIM_COMPONENT_UBOUND) THEN
 459   ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;
 460
 461 let LIM_RE_LBOUND = prove
 462  (`!net:(A)net f l b.
 463         ~(trivial_limit net) /\ (f --> l) net /\
 464         eventually (\x. b <= Re(f x)) net
 465         ==> b <= Re(l)`,
 466   REWRITE_TAC[RE_DEF] THEN REPEAT STRIP_TAC THEN
 467   MP_TAC(ISPECL [`net:(A)net`; `f:A->complex`; `l:complex`; `b:real`; `1`]
 468                 LIM_COMPONENT_LBOUND) THEN
 469   ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;
 470
 471 let LIM_IM_UBOUND = prove
 472  (`!net:(A)net f l b.
 473         ~(trivial_limit net) /\ (f --> l) net /\
 474         eventually (\x. Im(f x) <= b) net
 475         ==> Im(l) <= b`,
 476   REWRITE_TAC[IM_DEF] THEN REPEAT STRIP_TAC THEN
 477   MP_TAC(ISPECL [`net:(A)net`; `f:A->complex`; `l:complex`; `b:real`; `2`]
 478                 LIM_COMPONENT_UBOUND) THEN
 479   ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;
 480
 481 let LIM_IM_LBOUND = prove
 482  (`!net:(A)net f l b.
 483         ~(trivial_limit net) /\ (f --> l) net /\
 484         eventually (\x. b <= Im(f x)) net
 485         ==> b <= Im(l)`,
 486   REWRITE_TAC[IM_DEF] THEN REPEAT STRIP_TAC THEN
 487   MP_TAC(ISPECL [`net:(A)net`; `f:A->complex`; `l:complex`; `b:real`; `2`]
 488                 LIM_COMPONENT_LBOUND) THEN
 489   ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;
 490
 491 (* ------------------------------------------------------------------------- *)
 492 (* Case analysis for limit of reciprocal of a function. This can be true     *)
 493 (* degenerately, and it's a bit tiresome to show otherwise that it means     *)
 494 (* what you expect.                                                          *)
 495 (* ------------------------------------------------------------------------- *)
 496
 497 let LIM_COMPLEX_INV_NONDEGENERATE = prove
 498  (`!f:real^N->complex s a l.
 499         2 <= dimindex(:N) /\
 500         a IN s /\ open s /\
 501         f continuous_on (s DELETE a) /\
 502         ((inv o f) --> l) (at a)
 503         ==> ?t. open t /\ t SUBSET s /\
 504                 ((!x. x IN t DELETE a ==> f x = Cx(&0)) /\ l = Cx(&0) \/
 505                  (!x. x IN t DELETE a ==> ~(f x = Cx(&0))))`,
 506   REPEAT STRIP_TAC THEN ASM_CASES_TAC
 507    `!e. &0 < e ==> ?z:real^N. norm(z - a) < e /\ ~(z = a) /\ f(z) = Cx(&0)`
 508   THENL
 509    [ALL_TAC;
 510     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_FORALL_THM]) THEN
 511     REWRITE_TAC[NOT_IMP; NOT_EXISTS_THM; LEFT_IMP_EXISTS_THM] THEN
 512     REWRITE_TAC[TAUT `~(a /\ b) <=> a ==> ~b`] THEN
 513     X_GEN_TAC `e:real` THEN STRIP_TAC THEN
 514     EXISTS_TAC `s INTER ball(a:real^N,e)` THEN
 515     ASM_SIMP_TAC[INTER_SUBSET; OPEN_INTER; OPEN_BALL] THEN DISJ2_TAC THEN
 516     REWRITE_TAC[IN_DELETE; IN_INTER; IN_BALL; dist] THEN
 517     ASM_MESON_TAC[NORM_SUB]] THEN
 518   SUBGOAL_THEN `l = Cx(&0)` SUBST_ALL_TAC THENL
 519    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_AT]) THEN
 520     ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN DISCH_TAC THEN
 521     DISCH_THEN(MP_TAC o SPEC `norm(l:complex)`) THEN
 522     ASM_SIMP_TAC[COMPLEX_NORM_NZ; dist] THEN
 523     DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
 524     FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[] THEN
 525     DISCH_THEN(X_CHOOSE_THEN `z:real^N` STRIP_ASSUME_TAC) THEN
 526     FIRST_X_ASSUM(MP_TAC o SPEC `z:real^N`) THEN
 527     ASM_REWRITE_TAC[NORM_POS_LT; o_THM; VECTOR_SUB_EQ; COMPLEX_INV_0] THEN
 528     REWRITE_TAC[COMPLEX_SUB_LZERO; NORM_NEG; REAL_LT_REFL];
 529     REWRITE_TAC[]] THEN
 530   SUBGOAL_THEN
 531    `?e. &0 < e /\
 532         !z:real^N. norm(z - a) < e /\ ~(z = a)
 533                    ==> z IN s /\ (f z = Cx(&0) \/ norm(f z) >= &1)`
 534   STRIP_ASSUME_TAC THENL
 535    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_AT]) THEN
 536     DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[REAL_LT_01] THEN
 537     REWRITE_TAC[o_THM; VECTOR_SUB_EQ; dist; COMPLEX_SUB_RZERO] THEN
 538     DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
 539     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [open_def]) THEN
 540     DISCH_THEN(MP_TAC o SPEC `a:real^N`) THEN ASM_REWRITE_TAC[dist] THEN
 541     DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
 542     EXISTS_TAC `min d e:real` THEN ASM_SIMP_TAC[REAL_LT_MIN] THEN
 543     X_GEN_TAC `z:real^N` THEN DISCH_TAC THEN
 544     REWRITE_TAC[TAUT `p \/ q <=> ~p ==> q`] THEN STRIP_TAC THEN
 545     REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `z:real^N`)) THEN
 546     ASM_REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ] THEN REPEAT DISCH_TAC THEN
 547     SUBST1_TAC(REAL_ARITH `&1 = inv(&1)`) THEN REWRITE_TAC[real_ge] THEN
 548     GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_INV] THEN
 549     MATCH_MP_TAC REAL_LE_INV2 THEN
 550     ASM_SIMP_TAC[GSYM COMPLEX_NORM_INV; REAL_LT_IMP_LE] THEN
 551     ASM_REWRITE_TAC[NORM_POS_LT; COMPLEX_INV_EQ_0; COMPLEX_VEC_0];
 552     ALL_TAC] THEN
 553   EXISTS_TAC `ball(a:real^N,e)` THEN
 554   ASM_REWRITE_TAC[OPEN_BALL; SUBSET; IN_DELETE; IN_BALL; dist] THEN
 555   CONJ_TAC THENL [ASM_MESON_TAC[NORM_SUB]; DISJ1_TAC] THEN
 556   X_GEN_TAC `z:real^N` THEN STRIP_TAC THEN
 557   ASM_CASES_TAC `f(z:real^N) = Cx(&0)` THEN ASM_REWRITE_TAC[] THEN
 558   FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
 559   DISCH_THEN(X_CHOOSE_THEN `w:real^N` STRIP_ASSUME_TAC) THEN
 560   SUBGOAL_THEN
 561    `connected (IMAGE (lift o norm o (f:real^N->complex)) (ball(a,e) DELETE a))`
 562   MP_TAC THENL
 563    [MATCH_MP_TAC CONNECTED_CONTINUOUS_IMAGE THEN
 564     ASM_SIMP_TAC[CONNECTED_PUNCTURED_BALL; o_DEF] THEN
 565     MATCH_MP_TAC CONTINUOUS_ON_LIFT_NORM_COMPOSE THEN
 566     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
 567       CONTINUOUS_ON_SUBSET)) THEN
 568     REWRITE_TAC[SUBSET; IN_DELETE; IN_BALL; dist] THEN
 569     ASM_MESON_TAC[NORM_SUB];
 570     REWRITE_TAC[GSYM IS_INTERVAL_CONNECTED_1]] THEN
 571   REWRITE_TAC[IS_INTERVAL_1; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 572   REWRITE_TAC[FORALL_IN_IMAGE; IN_DELETE; IN_BALL; dist] THEN
 573   DISCH_THEN(MP_TAC o SPEC `w:real^N`) THEN
 574   ANTS_TAC THENL [ASM_MESON_TAC[NORM_SUB]; ALL_TAC] THEN
 575   DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN
 576   ASM_REWRITE_TAC[o_THM; LIFT_DROP; COMPLEX_NORM_0] THEN
 577   DISCH_THEN(MP_TAC o SPEC `lift(&1 / &2)`) THEN
 578   ASM_REWRITE_TAC[LIFT_DROP; NOT_IMP] THEN
 579   CONV_TAC REAL_RAT_REDUCE_CONV THEN CONJ_TAC THENL
 580    [MATCH_MP_TAC(REAL_ARITH `x >= &1 ==> &1 / &2 <= x`) THEN
 581     ASM_MESON_TAC[NORM_SUB];
 582     REWRITE_TAC[IN_IMAGE; o_THM; LIFT_EQ; IN_BALL; IN_DELETE; dist] THEN
 583     DISCH_THEN(X_CHOOSE_THEN `x:real^N` (STRIP_ASSUME_TAC o GSYM)) THEN
 584     FIRST_X_ASSUM(MP_TAC o SPEC `x:real^N`) THEN
 585     ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[NORM_SUB] THEN
 586     CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_REWRITE_TAC[] THEN
 587     DISCH_THEN(SUBST_ALL_TAC o CONJUNCT2) THEN
 588     RULE_ASSUM_TAC(REWRITE_RULE[COMPLEX_NORM_0]) THEN ASM_REAL_ARITH_TAC]);;
 589
 590 (* ------------------------------------------------------------------------- *)
 591 (* Left and right multiplication of series.                                  *)
 592 (* ------------------------------------------------------------------------- *)
 593
 594 let SERIES_COMPLEX_LMUL = prove
 595  (`!f l c s. (f sums l) s ==> ((\x. c * f x) sums c * l) s`,
 596   REPEAT STRIP_TAC THEN MATCH_MP_TAC SERIES_LINEAR THEN
 597   ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC RAND_CONV [GSYM ETA_AX] THEN
 598   REWRITE_TAC[LINEAR_COMPLEX_MUL]);;
 599
 600 let SERIES_COMPLEX_RMUL = prove
 601  (`!f l c s. (f sums l) s ==> ((\x. f x * c) sums l * c) s`,
 602   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN REWRITE_TAC[SERIES_COMPLEX_LMUL]);;
 603
 604 let SERIES_COMPLEX_DIV = prove
 605  (`!f l c s. (f sums l) s ==> ((\x. f x / c) sums (l / c)) s`,
 606   REWRITE_TAC[complex_div; SERIES_COMPLEX_RMUL]);;
 607
 608 let SUMMABLE_COMPLEX_LMUL = prove
 609  (`!f c s. summable s f ==> summable s (\x. c * f x)`,
 610   REWRITE_TAC[summable] THEN MESON_TAC[SERIES_COMPLEX_LMUL]);;
 611
 612 let SUMMABLE_COMPLEX_RMUL = prove
 613  (`!f c s. summable s f ==> summable s (\x. f x * c)`,
 614   REWRITE_TAC[summable] THEN MESON_TAC[SERIES_COMPLEX_RMUL]);;
 615
 616 let SUMMABLE_COMPLEX_DIV = prove
 617  (`!f c s. summable s f ==> summable s (\x. f x / c)`,
 618   REWRITE_TAC[summable] THEN MESON_TAC[SERIES_COMPLEX_DIV]);;
 619
 620 (* ------------------------------------------------------------------------- *)
 621 (* Complex-specific continuity closures.                                     *)
 622 (* ------------------------------------------------------------------------- *)
 623
 624 let CONTINUOUS_COMPLEX_MUL = prove
 625  (`!net f g.
 626     f continuous net /\ g continuous net ==> (\x. f(x) * g(x)) continuous net`,
 627   SIMP_TAC[continuous; LIM_COMPLEX_MUL]);;
 628
 629 let CONTINUOUS_COMPLEX_LMUL = prove
 630  (`!c f net. f continuous net ==> (\x. c * f x) continuous net`,
 631   SIMP_TAC[CONTINUOUS_COMPLEX_MUL; CONTINUOUS_CONST]);;
 632
 633 let CONTINUOUS_COMPLEX_RMUL = prove
 634  (`!c f net. f continuous net ==> (\x. f x * c) continuous net`,
 635   SIMP_TAC[CONTINUOUS_COMPLEX_MUL; CONTINUOUS_CONST]);;
 636
 637 let CONTINUOUS_COMPLEX_INV = prove
 638  (`!net f.
 639     f continuous net /\ ~(f(netlimit net) = Cx(&0))
 640     ==> (\x. inv(f x)) continuous net`,
 641   SIMP_TAC[continuous; LIM_COMPLEX_INV]);;
 642
 643 let CONTINUOUS_COMPLEX_DIV = prove
 644  (`!net f g.
 645     f continuous net /\ g continuous net /\ ~(g(netlimit net) = Cx(&0))
 646     ==> (\x. f(x) / g(x)) continuous net`,
 647   SIMP_TAC[continuous; LIM_COMPLEX_DIV]);;
 648
 649 let CONTINUOUS_COMPLEX_POW = prove
 650  (`!net f n. f continuous net ==> (\x. f(x) pow n) continuous net`,
 651   SIMP_TAC[continuous; LIM_COMPLEX_POW]);;
 652
 653 (* ------------------------------------------------------------------------- *)
 654 (* Write away the netlimit, which is otherwise a bit tedious.                *)
 655 (* ------------------------------------------------------------------------- *)
 656
 657 let CONTINUOUS_COMPLEX_INV_WITHIN = prove
 658  (`!f s a.
 659     f continuous (at a within s) /\ ~(f a = Cx(&0))
 660     ==> (\x. inv(f x)) continuous (at a within s)`,
 661   MESON_TAC[CONTINUOUS_COMPLEX_INV; CONTINUOUS_TRIVIAL_LIMIT;
 662             NETLIMIT_WITHIN]);;
 663
 664 let CONTINUOUS_COMPLEX_INV_AT = prove
 665  (`!f a.
 666     f continuous (at a) /\ ~(f a = Cx(&0))
 667     ==> (\x. inv(f x)) continuous (at a)`,
 668   SIMP_TAC[CONTINUOUS_COMPLEX_INV; NETLIMIT_AT]);;
 669
 670 let CONTINUOUS_COMPLEX_DIV_WITHIN = prove
 671  (`!f g s a.
 672     f continuous (at a within s) /\ g continuous (at a within s) /\
 673     ~(g a = Cx(&0))
 674     ==> (\x. f x / g x) continuous (at a within s)`,
 675   MESON_TAC[CONTINUOUS_COMPLEX_DIV; CONTINUOUS_TRIVIAL_LIMIT;
 676             NETLIMIT_WITHIN]);;
 677
 678 let CONTINUOUS_COMPLEX_DIV_AT = prove
 679  (`!f g a.
 680     f continuous at a /\ g continuous at a /\ ~(g a = Cx(&0))
 681     ==> (\x. f x / g x) continuous at a`,
 682   SIMP_TAC[CONTINUOUS_COMPLEX_DIV; NETLIMIT_AT]);;
 683
 684 (* ------------------------------------------------------------------------- *)
 685 (* Also prove "on" variants as needed.                                       *)
 686 (* ------------------------------------------------------------------------- *)
 687
 688 let CONTINUOUS_ON_COMPLEX_MUL = prove
 689  (`!f g s. f continuous_on s /\ g continuous_on s
 690            ==> (\x. f(x) * g(x)) continuous_on s`,
 691   REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
 692   SIMP_TAC[CONTINUOUS_COMPLEX_MUL]);;
 693
 694 let CONTINUOUS_ON_COMPLEX_LMUL = prove
 695  (`!f:real^N->complex s. f continuous_on s ==> (\x. c * f(x)) continuous_on s`,
 696   REWRITE_TAC[CONTINUOUS_ON] THEN SIMP_TAC[LIM_COMPLEX_MUL; LIM_CONST]);;
 697
 698 let CONTINUOUS_ON_COMPLEX_RMUL = prove
 699  (`!f:real^N->complex s. f continuous_on s ==> (\x. f(x) * c) continuous_on s`,
 700   REWRITE_TAC[CONTINUOUS_ON] THEN SIMP_TAC[LIM_COMPLEX_MUL; LIM_CONST]);;
 701
 702 let CONTINUOUS_ON_COMPLEX_INV = prove
 703  (`!f:real^N->complex.
 704         f continuous_on s /\
 705         (!x. x IN s ==> ~(f x = Cx(&0)))
 706         ==> (\x. inv(f x)) continuous_on s`,
 707   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN;
 708            CONTINUOUS_COMPLEX_INV_WITHIN]);;
 709
 710 let CONTINUOUS_ON_COMPLEX_DIV = prove
 711  (`!f g s. f continuous_on s /\ g continuous_on s /\
 712            (!x. x IN s ==> ~(g x = Cx(&0)))
 713            ==> (\x. f(x) / g(x)) continuous_on s`,
 714   REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
 715   SIMP_TAC[CONTINUOUS_COMPLEX_DIV_WITHIN]);;
 716
 717 let CONTINUOUS_ON_COMPLEX_POW = prove
 718  (`!f n s. f continuous_on s ==> (\x. f(x) pow n) continuous_on s`,
 719   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN; CONTINUOUS_COMPLEX_POW]);;
 720
 721 (* ------------------------------------------------------------------------- *)
 722 (* And also uniform versions.                                                *)
 723 (* ------------------------------------------------------------------------- *)
 724
 725 let UNIFORMLY_CONTINUOUS_ON_COMPLEX_MUL = prove
 726  (`!f g s:real^N->bool.
 727         f uniformly_continuous_on s /\ g uniformly_continuous_on s /\
 728         bounded(IMAGE f s) /\ bounded(IMAGE g s)
 729         ==> (\x. f(x) * g(x)) uniformly_continuous_on s`,
 730   REPEAT STRIP_TAC THEN
 731   MP_TAC(ISPECL
 732    [`f:real^N->complex`; `g:real^N->complex`;
 733     `( * ):complex->complex->complex`; `s:real^N->bool`]
 734     BILINEAR_UNIFORMLY_CONTINUOUS_ON_COMPOSE) THEN
 735   ASM_REWRITE_TAC[BILINEAR_COMPLEX_MUL]);;
 736
 737 let UNIFORMLY_CONTINUOUS_ON_COMPLEX_LMUL = prove
 738  (`!f c s:real^N->bool.
 739       f uniformly_continuous_on s ==> (\x. c * f x) uniformly_continuous_on s`,
 740   REPEAT GEN_TAC THEN
 741   DISCH_THEN(MP_TAC o ISPEC `\x:complex. c * x` o MATCH_MP
 742    (REWRITE_RULE[IMP_CONJ] UNIFORMLY_CONTINUOUS_ON_COMPOSE)) THEN
 743   ASM_SIMP_TAC[o_DEF; LINEAR_COMPLEX_MUL; LINEAR_UNIFORMLY_CONTINUOUS_ON]);;
 744
 745 let UNIFORMLY_CONTINUOUS_ON_COMPLEX_RMUL = prove
 746  (`!f c s:real^N->bool.
 747       f uniformly_continuous_on s ==> (\x. f x * c) uniformly_continuous_on s`,
 748   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
 749   REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_COMPLEX_LMUL]);;
 750
 751 (* ------------------------------------------------------------------------- *)
 752 (* Continuity prover (not just for complex numbers but with more for them).  *)
 753 (* ------------------------------------------------------------------------- *)
 754
 755 let CONTINUOUS_TAC =
 756   let ETA_THM = prove
 757    (`f continuous net <=> (\x. f x) continuous net`,
 758     REWRITE_TAC[ETA_AX]) in
 759   let ETA_TWEAK =
 760     GEN_REWRITE_RULE (LAND_CONV o ONCE_DEPTH_CONV) [ETA_THM] o SPEC_ALL in
 761   let tac_base =
 762     MATCH_ACCEPT_TAC CONTINUOUS_CONST ORELSE
 763     MATCH_ACCEPT_TAC CONTINUOUS_AT_ID ORELSE
 764     MATCH_ACCEPT_TAC CONTINUOUS_WITHIN_ID
 765   and tac_1 =
 766     MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_CMUL) ORELSE
 767     MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_NEG) ORELSE
 768     MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_COMPLEX_POW)
 769   and tac_2 =
 770     MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_ADD) ORELSE
 771     MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_SUB) ORELSE
 772     MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_COMPLEX_MUL)
 773   and tac_1' = MATCH_MP_TAC (ETA_TWEAK CONTINUOUS_COMPLEX_INV)
 774   and tac_2' = MATCH_MP_TAC (ETA_TWEAK CONTINUOUS_COMPLEX_DIV) in
 775   let rec CONTINUOUS_TAC gl =
 776    (tac_base ORELSE
 777     (tac_1 THEN CONTINUOUS_TAC) ORELSE
 778     (tac_2 THEN CONJ_TAC THEN CONTINUOUS_TAC) ORELSE
 779     (tac_1' THEN CONJ_TAC THENL
 780      [CONTINUOUS_TAC; REWRITE_TAC[NETLIMIT_AT; NETLIMIT_WITHIN]]) ORELSE
 781     (tac_2' THEN REPEAT CONJ_TAC THENL
 782      [CONTINUOUS_TAC; CONTINUOUS_TAC;
 783       REWRITE_TAC[NETLIMIT_AT; NETLIMIT_WITHIN]]) ORELSE
 784     ALL_TAC) gl in
 785   CONTINUOUS_TAC;;
 786
 787 (* ------------------------------------------------------------------------- *)
 788 (* Hence a limit calculator                                                  *)
 789 (* ------------------------------------------------------------------------- *)
 790
 791 let LIM_CONTINUOUS = prove
 792  (`!net f l. f continuous net /\ f(netlimit net) = l ==> (f --> l) net`,
 793   MESON_TAC[continuous]);;
 794
 795 let LIM_TAC =
 796   MATCH_MP_TAC LIM_CONTINUOUS THEN CONJ_TAC THENL
 797    [CONTINUOUS_TAC; REWRITE_TAC[NETLIMIT_AT; NETLIMIT_WITHIN]];;
 798
 799 (* ------------------------------------------------------------------------- *)
 800 (* Continuity of the norm.                                                   *)
 801 (* ------------------------------------------------------------------------- *)
 802
 803 let CONTINUOUS_AT_CX_NORM = prove
 804  (`!z:real^N. (\z. Cx(norm z)) continuous at z`,
 805   REWRITE_TAC[continuous_at; dist; GSYM CX_SUB; COMPLEX_NORM_CX] THEN
 806   MESON_TAC[NORM_ARITH `norm(a - b:real^N) < d ==> abs(norm a - norm b) < d`]);;
 807
 808 let CONTINUOUS_WITHIN_CX_NORM = prove
 809  (`!z:real^N s. (\z. Cx(norm z)) continuous (at z within s)`,
 810   SIMP_TAC[CONTINUOUS_AT_CX_NORM; CONTINUOUS_AT_WITHIN]);;
 811
 812 let CONTINUOUS_ON_CX_NORM = prove
 813  (`!s. (\z. Cx(norm z)) continuous_on s`,
 814   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN; CONTINUOUS_WITHIN_CX_NORM]);;
 815
 816 let CONTINUOUS_AT_CX_DOT = prove
 817  (`!c z:real^N. (\z. Cx(c dot z)) continuous at z`,
 818   REPEAT GEN_TAC THEN MATCH_MP_TAC LINEAR_CONTINUOUS_AT THEN
 819   REWRITE_TAC[linear; DOT_RADD; DOT_RMUL; CX_ADD; COMPLEX_CMUL; CX_MUL]);;
 820
 821 let CONTINUOUS_WITHIN_CX_DOT = prove
 822  (`!c z:real^N s. (\z. Cx(c dot z)) continuous (at z within s)`,
 823   SIMP_TAC[CONTINUOUS_AT_CX_DOT; CONTINUOUS_AT_WITHIN]);;
 824
 825 let CONTINUOUS_ON_CX_DOT = prove
 826  (`!s c:real^N. (\z. Cx(c dot z)) continuous_on s`,
 827   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN; CONTINUOUS_WITHIN_CX_DOT]);;
 828
 829 (* ------------------------------------------------------------------------- *)
 830 (* Continuity switching range between complex and real^1                     *)
 831 (* ------------------------------------------------------------------------- *)
 832
 833 let CONTINUOUS_CX_DROP = prove
 834  (`!net f. f continuous net ==> (\x. Cx(drop(f x))) continuous net`,
 835   REWRITE_TAC[continuous; tendsto] THEN
 836   REWRITE_TAC[dist; GSYM CX_SUB; COMPLEX_NORM_CX; GSYM DROP_SUB] THEN
 837   REWRITE_TAC[GSYM ABS_DROP]);;
 838
 839 let CONTINUOUS_ON_CX_DROP = prove
 840  (`!f s. f continuous_on s ==> (\x. Cx(drop(f x))) continuous_on s`,
 841   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN; CONTINUOUS_CX_DROP]);;
 842
 843 let CONTINUOUS_CX_LIFT = prove
 844  (`!f. (\x. Cx(f x)) continuous net <=> (\x. lift(f x)) continuous net`,
 845   REWRITE_TAC[continuous; LIM; dist; GSYM CX_SUB; GSYM LIFT_SUB] THEN
 846   REWRITE_TAC[COMPLEX_NORM_CX; NORM_LIFT]);;
 847
 848 let CONTINUOUS_ON_CX_LIFT = prove
 849  (`!f s. (\x. Cx(f x)) continuous_on s <=> (\x. lift(f x)) continuous_on s`,
 850   REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN; CONTINUOUS_CX_LIFT]);;
 851
 852 (* ------------------------------------------------------------------------- *)
 853 (* Linearity and continuity of the components.                               *)
 854 (* ------------------------------------------------------------------------- *)
 855
 856 let LINEAR_CX_RE = prove
 857  (`linear(Cx o Re)`,
 858   SIMP_TAC[linear; o_THM; COMPLEX_CMUL; RE_ADD; RE_MUL_CX; CX_MUL; CX_ADD]);;
 859
 860 let CONTINUOUS_AT_CX_RE = prove
 861  (`!z. (Cx o Re) continuous at z`,
 862   SIMP_TAC[LINEAR_CONTINUOUS_AT; LINEAR_CX_RE]);;
 863
 864 let CONTINUOUS_ON_CX_RE = prove
 865  (`!s. (Cx o Re) continuous_on s`,
 866   SIMP_TAC[LINEAR_CONTINUOUS_ON; LINEAR_CX_RE]);;
 867
 868 let LINEAR_CX_IM = prove
 869  (`linear(Cx o Im)`,
 870   SIMP_TAC[linear; o_THM; COMPLEX_CMUL; IM_ADD; IM_MUL_CX; CX_MUL; CX_ADD]);;
 871
 872 let CONTINUOUS_AT_CX_IM = prove
 873  (`!z. (Cx o Im) continuous at z`,
 874   SIMP_TAC[LINEAR_CONTINUOUS_AT; LINEAR_CX_IM]);;
 875
 876 let CONTINUOUS_ON_CX_IM = prove
 877  (`!s. (Cx o Im) continuous_on s`,
 878   SIMP_TAC[LINEAR_CONTINUOUS_ON; LINEAR_CX_IM]);;
 879
 880 (* ------------------------------------------------------------------------- *)
 881 (* Complex differentiability.                                                *)
 882 (* ------------------------------------------------------------------------- *)
 883
 884 parse_as_infix ("has_complex_derivative",(12,"right"));;
 885 parse_as_infix ("complex_differentiable",(12,"right"));;
 886 parse_as_infix ("holomorphic_on",(12,"right"));;
 887
 888 let has_complex_derivative = new_definition
 889  `(f has_complex_derivative f') net <=> (f has_derivative (\x. f' * x)) net`;;
 890
 891 let complex_differentiable = new_definition
 892  `f complex_differentiable net <=> ?f'. (f has_complex_derivative f') net`;;
 893
 894 let complex_derivative = new_definition
 895  `complex_derivative f x = @f'. (f has_complex_derivative f') (at x)`;;
 896
 897 let higher_complex_derivative = define
 898  `higher_complex_derivative 0 f = f /\
 899   (!n. higher_complex_derivative (SUC n) f =
 900                 complex_derivative (higher_complex_derivative n f))`;;
 901
 902 let holomorphic_on = new_definition
 903  `f holomorphic_on s <=>
 904      !x. x IN s ==> ?f'. (f has_complex_derivative f') (at x within s)`;;
 905
 906 let HOLOMORPHIC_ON_EMPTY = prove
 907  (`!f. f holomorphic_on {}`,
 908   REWRITE_TAC[holomorphic_on; NOT_IN_EMPTY]);;
 909
 910 let HOLOMORPHIC_ON_DIFFERENTIABLE = prove
 911  (`!f s. f holomorphic_on s <=>
 912          !x. x IN s ==> f complex_differentiable (at x within s)`,
 913   REWRITE_TAC[holomorphic_on; complex_differentiable]);;
 914
 915 let HOLOMORPHIC_ON_OPEN = prove
 916  (`!f s. open s
 917          ==> (f holomorphic_on s <=>
 918               !x. x IN s ==> ?f'. (f has_complex_derivative f') (at x))`,
 919   REWRITE_TAC[holomorphic_on; has_complex_derivative] THEN
 920   REWRITE_TAC[has_derivative_at; has_derivative_within] THEN
 921   SIMP_TAC[LIM_WITHIN_OPEN]);;
 922
 923 let HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_WITHIN = prove
 924  (`!f s x. f holomorphic_on s /\ x IN s
 925            ==> f complex_differentiable (at x within s)`,
 926   MESON_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE]);;
 927
 928 let HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT = prove
 929  (`!f s x. f holomorphic_on s /\ open s /\ x IN s
 930            ==> f complex_differentiable (at x)`,
 931   MESON_TAC[HOLOMORPHIC_ON_OPEN; complex_differentiable]);;
 932
 933 let HAS_COMPLEX_DERIVATIVE_IMP_CONTINUOUS_AT = prove
 934  (`!f f' x. (f has_complex_derivative f') (at x) ==> f continuous at x`,
 935   REWRITE_TAC[has_complex_derivative] THEN
 936   MESON_TAC[differentiable; DIFFERENTIABLE_IMP_CONTINUOUS_AT]);;
 937
 938 let HAS_COMPLEX_DERIVATIVE_IMP_CONTINUOUS_WITHIN = prove
 939  (`!f f' x s. (f has_complex_derivative f') (at x within s)
 940               ==> f continuous (at x within s)`,
 941   REWRITE_TAC[has_complex_derivative] THEN
 942   MESON_TAC[differentiable; DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]);;
 943
 944 let COMPLEX_DIFFERENTIABLE_IMP_DIFFERENTIABLE = prove
 945  (`!net f. f complex_differentiable net ==> f differentiable net`,
 946   SIMP_TAC[complex_differentiable; differentiable; has_complex_derivative] THEN
 947   MESON_TAC[]);;
 948
 949 let COMPLEX_DIFFERENTIABLE_IMP_CONTINUOUS_AT = prove
 950  (`!f x. f complex_differentiable at x ==> f continuous at x`,
 951   MESON_TAC[HAS_COMPLEX_DERIVATIVE_IMP_CONTINUOUS_AT; complex_differentiable]);;
 952
 953 let COMPLEX_DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN = prove
 954  (`!f x s. f complex_differentiable (at x within s)
 955            ==> f continuous (at x within s)`,
 956   MESON_TAC[COMPLEX_DIFFERENTIABLE_IMP_DIFFERENTIABLE;
 957             DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]);;
 958
 959 let HOLOMORPHIC_ON_IMP_CONTINUOUS_ON = prove
 960  (`!f s. f holomorphic_on s ==> f continuous_on s`,
 961   REWRITE_TAC[holomorphic_on; CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
 962   REWRITE_TAC[has_complex_derivative] THEN
 963   MESON_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN; differentiable]);;
 964
 965 let HOLOMORPHIC_ON_SUBSET = prove
 966  (`!f s t. f holomorphic_on s /\ t SUBSET s ==> f holomorphic_on t`,
 967   REWRITE_TAC[holomorphic_on; has_complex_derivative] THEN
 968   MESON_TAC[SUBSET; HAS_DERIVATIVE_WITHIN_SUBSET]);;
 969
 970 let HAS_COMPLEX_DERIVATIVE_WITHIN_SUBSET = prove
 971  (`!f s t x. (f has_complex_derivative f') (at x within s) /\ t SUBSET s
 972              ==> (f has_complex_derivative f') (at x within t)`,
 973   REWRITE_TAC[has_complex_derivative; HAS_DERIVATIVE_WITHIN_SUBSET]);;
 974
 975 let COMPLEX_DIFFERENTIABLE_WITHIN_SUBSET = prove
 976  (`!f s t. f complex_differentiable (at x within s) /\ t SUBSET s
 977            ==> f complex_differentiable (at x within t)`,
 978   REWRITE_TAC[complex_differentiable] THEN
 979   MESON_TAC[HAS_COMPLEX_DERIVATIVE_WITHIN_SUBSET]);;
 980
 981 let HAS_COMPLEX_DERIVATIVE_AT_WITHIN = prove
 982  (`!f f' x s. (f has_complex_derivative f') (at x)
 983               ==> (f has_complex_derivative f') (at x within s)`,
 984   REWRITE_TAC[has_complex_derivative; HAS_DERIVATIVE_AT_WITHIN]);;
 985
 986 let HAS_COMPLEX_DERIVATIVE_WITHIN_OPEN = prove
 987  (`!f f' a s.
 988          a IN s /\ open s
 989          ==> ((f has_complex_derivative f') (at a within s) <=>
 990               (f has_complex_derivative f') (at a))`,
 991   REWRITE_TAC[has_complex_derivative; HAS_DERIVATIVE_WITHIN_OPEN]);;
 992
 993 let COMPLEX_DIFFERENTIABLE_AT_WITHIN = prove
 994  (`!f s z. f complex_differentiable (at z)
 995            ==> f complex_differentiable (at z within s)`,
 996   REWRITE_TAC[complex_differentiable] THEN
 997   MESON_TAC[HAS_COMPLEX_DERIVATIVE_AT_WITHIN]);;
 998
 999 let HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN = prove
1000  (`!f f' g x s d.
1001        &0 < d /\ x IN s /\
1002        (!x'. x' IN s /\ dist (x',x) < d ==> f x' = g x') /\
1003        (f has_complex_derivative f') (at x within s)
1004        ==> (g has_complex_derivative f') (at x within s)`,
1005   REWRITE_TAC[has_complex_derivative] THEN
1006   MESON_TAC[HAS_DERIVATIVE_TRANSFORM_WITHIN]);;
1007
1008 let HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN = prove
1009   (`!f g f' s z. open s /\ z IN s /\ (!w. w IN s ==> f w = g w) /\
1010                  (f has_complex_derivative f') (at z)
1011                  ==> (g has_complex_derivative f') (at z)`,
1012    REWRITE_TAC [has_complex_derivative] THEN
1013    ASM_MESON_TAC [HAS_DERIVATIVE_TRANSFORM_WITHIN_OPEN]);;
1014
1015 let HAS_COMPLEX_DERIVATIVE_TRANSFORM_AT = prove
1016  (`!f f' g x d.
1017        &0 < d /\ (!x'. dist (x',x) < d ==> f x' = g x') /\
1018        (f has_complex_derivative f') (at x)
1019        ==> (g has_complex_derivative f') (at x)`,
1020   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
1021   MESON_TAC[HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN; IN_UNIV]);;
1022
1023 let HAS_COMPLEX_DERIVATIVE_ZERO_CONSTANT = prove
1024  (`!f s.
1025         convex s /\
1026         (!x. x IN s ==> (f has_complex_derivative Cx(&0)) (at x within s))
1027         ==> ?c. !x. x IN s ==> f(x) = c`,
1028   REWRITE_TAC[has_complex_derivative; COMPLEX_MUL_LZERO] THEN
1029   REWRITE_TAC[GSYM COMPLEX_VEC_0; HAS_DERIVATIVE_ZERO_CONSTANT]);;
1030
1031 let HAS_COMPLEX_DERIVATIVE_ZERO_UNIQUE = prove
1032  (`!f s c a.
1033         convex s /\ a IN s /\ f a = c /\
1034         (!x. x IN s ==> (f has_complex_derivative Cx(&0)) (at x within s))
1035         ==> !x. x IN s ==> f(x) = c`,
1036   REWRITE_TAC[has_complex_derivative; COMPLEX_MUL_LZERO] THEN
1037   REWRITE_TAC[GSYM COMPLEX_VEC_0; HAS_DERIVATIVE_ZERO_UNIQUE]);;
1038
1039 let HAS_COMPLEX_DERIVATIVE_ZERO_CONNECTED_CONSTANT = prove
1040  (`!f s.
1041         open s /\ connected s /\
1042         (!x. x IN s ==> (f has_complex_derivative Cx(&0)) (at x))
1043         ==> ?c. !x. x IN s ==> f(x) = c`,
1044   REWRITE_TAC[has_complex_derivative; COMPLEX_MUL_LZERO] THEN
1045   REWRITE_TAC[GSYM COMPLEX_VEC_0; HAS_DERIVATIVE_ZERO_CONNECTED_CONSTANT]);;
1046
1047 let HAS_COMPLEX_DERIVATIVE_ZERO_CONNECTED_UNIQUE = prove
1048  (`!f s c a.
1049         open s /\ connected s /\ a IN s /\ f a = c /\
1050         (!x. x IN s ==> (f has_complex_derivative Cx(&0)) (at x))
1051         ==> !x. x IN s ==> f(x) = c`,
1052   REWRITE_TAC[has_complex_derivative; COMPLEX_MUL_LZERO] THEN
1053   REWRITE_TAC[GSYM COMPLEX_VEC_0; HAS_DERIVATIVE_ZERO_CONNECTED_UNIQUE]);;
1054
1055 let COMPLEX_DIFF_CHAIN_WITHIN = prove
1056  (`!f g f' g' x s.
1057         (f has_complex_derivative f') (at x within s) /\
1058         (g has_complex_derivative g') (at (f x) within (IMAGE f s))
1059         ==> ((g o f) has_complex_derivative (g' * f'))(at x within s)`,
1060   REPEAT GEN_TAC THEN REWRITE_TAC[has_complex_derivative] THEN
1061   DISCH_THEN(MP_TAC o MATCH_MP DIFF_CHAIN_WITHIN) THEN
1062   REWRITE_TAC[o_DEF; COMPLEX_MUL_ASSOC]);;
1063
1064 let COMPLEX_DIFF_CHAIN_AT = prove
1065  (`!f g f' g' x.
1066         (f has_complex_derivative f') (at x) /\
1067         (g has_complex_derivative g') (at (f x))
1068         ==> ((g o f) has_complex_derivative (g' * f')) (at x)`,
1069   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
1070   ASM_MESON_TAC[COMPLEX_DIFF_CHAIN_WITHIN; SUBSET_UNIV;
1071                 HAS_COMPLEX_DERIVATIVE_WITHIN_SUBSET]);;
1072
1073 let HAS_COMPLEX_DERIVATIVE_CHAIN = prove
1074  (`!P f g.
1075         (!x. P x ==> (g has_complex_derivative g'(x)) (at x))
1076         ==> (!x s. (f has_complex_derivative f') (at x within s) /\ P(f x)
1077                    ==> ((\x. g(f x)) has_complex_derivative f' * g'(f x))
1078                        (at x within s)) /\
1079             (!x. (f has_complex_derivative f') (at x) /\ P(f x)
1080                  ==> ((\x. g(f x)) has_complex_derivative f' * g'(f x))
1081                      (at x))`,
1082   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM o_DEF] THEN
1083   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
1084   ASM_MESON_TAC[COMPLEX_DIFF_CHAIN_WITHIN; COMPLEX_DIFF_CHAIN_AT;
1085                 HAS_COMPLEX_DERIVATIVE_AT_WITHIN]);;
1086
1087 let HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV = prove
1088  (`!f g. (!x. (g has_complex_derivative g'(x)) (at x))
1089          ==> (!x s. (f has_complex_derivative f') (at x within s)
1090                     ==> ((\x. g(f x)) has_complex_derivative f' * g'(f x))
1091                         (at x within s)) /\
1092              (!x. (f has_complex_derivative f') (at x)
1093                   ==> ((\x. g(f x)) has_complex_derivative f' * g'(f x))
1094                       (at x))`,
1095   MP_TAC(SPEC `\x:complex. T` HAS_COMPLEX_DERIVATIVE_CHAIN) THEN SIMP_TAC[]);;
1096
1097 let COMPLEX_DERIVATIVE_UNIQUE_AT = prove
1098  (`!f z f' f''.
1099         (f has_complex_derivative f') (at z) /\
1100         (f has_complex_derivative f'') (at z)
1101         ==> f' = f''`,
1102   REPEAT GEN_TAC THEN REWRITE_TAC[has_complex_derivative] THEN
1103   DISCH_THEN(MP_TAC o MATCH_MP FRECHET_DERIVATIVE_UNIQUE_AT) THEN
1104   DISCH_THEN(MP_TAC o C AP_THM `Cx(&1)`) THEN
1105   REWRITE_TAC[COMPLEX_MUL_RID]);;
1106
1107 let HIGHER_COMPLEX_DERIVATIVE_1 = prove
1108  (`!f z. higher_complex_derivative 1 f z = complex_derivative f z`,
1109   REWRITE_TAC[num_CONV `1`; higher_complex_derivative]);;
1110
1111 (* ------------------------------------------------------------------------- *)
1112 (* A more direct characterization.                                           *)
1113 (* ------------------------------------------------------------------------- *)
1114
1115 let HAS_COMPLEX_DERIVATIVE_WITHIN = prove
1116  (`!f s a. (f has_complex_derivative f') (at a within s) <=>
1117            ((\x. (f(x) - f(a)) / (x - a)) --> f') (at a within s)`,
1118   REWRITE_TAC[has_complex_derivative; has_derivative_within] THEN
1119   REPEAT GEN_TAC THEN REWRITE_TAC[LINEAR_COMPLEX_MUL] THEN
1120   GEN_REWRITE_TAC RAND_CONV [LIM_NULL] THEN
1121   REWRITE_TAC[LIM_WITHIN; dist; VECTOR_SUB_RZERO; NORM_MUL] THEN
1122   REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ] THEN SIMP_TAC[COMPLEX_FIELD
1123   `~(x:complex = a) ==> y / (x - a) - z = inv(x - a) * (y - z * (x - a))`] THEN
1124   REWRITE_TAC[REAL_ABS_INV; COMPLEX_NORM_MUL; REAL_ABS_NORM;
1125          COMPLEX_NORM_INV; VECTOR_ARITH `a:complex - (b + c) = a - b - c`]);;
1126
1127 let HAS_COMPLEX_DERIVATIVE_AT = prove
1128  (`!f a. (f has_complex_derivative f') (at a) <=>
1129          ((\x. (f(x) - f(a)) / (x - a)) --> f') (at a)`,
1130   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
1131   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_WITHIN]);;
1132
1133 (* ------------------------------------------------------------------------- *)
1134 (* Arithmetical combining theorems.                                          *)
1135 (* ------------------------------------------------------------------------- *)
1136
1137 let HAS_DERIVATIVE_COMPLEX_CMUL = prove
1138  (`!net c. ((\x. c * x) has_derivative (\x. c * x)) net`,
1139   REPEAT GEN_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
1140   REWRITE_TAC[LINEAR_COMPLEX_MUL]);;
1141
1142 let HAS_COMPLEX_DERIVATIVE_LINEAR = prove
1143  (`!net c. ((\x. c * x) has_complex_derivative c) net`,
1144   REPEAT GEN_TAC THEN REWRITE_TAC[has_complex_derivative] THEN
1145   MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
1146   REWRITE_TAC[linear; COMPLEX_CMUL] THEN CONV_TAC COMPLEX_RING);;
1147
1148 let HAS_COMPLEX_DERIVATIVE_LMUL_WITHIN = prove
1149  (`!f f' c x s.
1150         (f has_complex_derivative f') (at x within s)
1151         ==> ((\x. c * f(x)) has_complex_derivative (c * f')) (at x within s)`,
1152   REPEAT GEN_TAC THEN
1153   MP_TAC(ISPECL [`at ((f:complex->complex) x) within (IMAGE f s)`; `c:complex`]
1154     HAS_COMPLEX_DERIVATIVE_LINEAR) THEN
1155   ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
1156   DISCH_THEN(MP_TAC o MATCH_MP COMPLEX_DIFF_CHAIN_WITHIN) THEN
1157   REWRITE_TAC[o_DEF]);;
1158
1159 let HAS_COMPLEX_DERIVATIVE_LMUL_AT = prove
1160  (`!f f' c x.
1161         (f has_complex_derivative f') (at x)
1162         ==> ((\x. c * f(x)) has_complex_derivative (c * f')) (at x)`,
1163   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
1164   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_LMUL_WITHIN]);;
1165
1166 let HAS_COMPLEX_DERIVATIVE_RMUL_WITHIN = prove
1167  (`!f f' c x s.
1168         (f has_complex_derivative f') (at x within s)
1169         ==> ((\x. f(x) * c) has_complex_derivative (f' * c)) (at x within s)`,
1170   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
1171   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_LMUL_WITHIN]);;
1172
1173 let HAS_COMPLEX_DERIVATIVE_RMUL_AT = prove
1174  (`!f f' c x.
1175         (f has_complex_derivative f') (at x)
1176         ==> ((\x. f(x) * c) has_complex_derivative (f' * c)) (at x)`,
1177   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
1178   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_LMUL_AT]);;
1179
1180 let HAS_COMPLEX_DERIVATIVE_CDIV_WITHIN = prove
1181  (`!f f' c x s.
1182         (f has_complex_derivative f') (at x within s)
1183         ==> ((\x. f(x) / c) has_complex_derivative (f' / c)) (at x within s)`,
1184   SIMP_TAC[complex_div; HAS_COMPLEX_DERIVATIVE_RMUL_WITHIN]);;
1185
1186 let HAS_COMPLEX_DERIVATIVE_CDIV_AT = prove
1187  (`!f f' c x s.
1188         (f has_complex_derivative f') (at x)
1189         ==> ((\x. f(x) / c) has_complex_derivative (f' / c)) (at x)`,
1190   SIMP_TAC[complex_div; HAS_COMPLEX_DERIVATIVE_RMUL_AT]);;
1191
1192 let HAS_COMPLEX_DERIVATIVE_ID = prove
1193  (`!net. ((\x. x) has_complex_derivative Cx(&1)) net`,
1194   REWRITE_TAC[has_complex_derivative; HAS_DERIVATIVE_ID; COMPLEX_MUL_LID]);;
1195
1196 let HAS_COMPLEX_DERIVATIVE_CONST = prove
1197  (`!c net. ((\x. c) has_complex_derivative Cx(&0)) net`,
1198   REWRITE_TAC[has_complex_derivative; COMPLEX_MUL_LZERO] THEN
1199   REWRITE_TAC[GSYM COMPLEX_VEC_0; HAS_DERIVATIVE_CONST]);;
1200
1201 let HAS_COMPLEX_DERIVATIVE_NEG = prove
1202  (`!f f' net. (f has_complex_derivative f') net
1203             ==> ((\x. --(f(x))) has_complex_derivative (--f')) net`,
1204   SIMP_TAC[has_complex_derivative; COMPLEX_MUL_LNEG; HAS_DERIVATIVE_NEG]);;
1205
1206 let HAS_COMPLEX_DERIVATIVE_ADD = prove
1207  (`!f f' g g' net.
1208         (f has_complex_derivative f') net /\ (g has_complex_derivative g') net
1209         ==> ((\x. f(x) + g(x)) has_complex_derivative (f' + g')) net`,
1210   SIMP_TAC[has_complex_derivative; COMPLEX_ADD_RDISTRIB; HAS_DERIVATIVE_ADD]);;
1211
1212 let HAS_COMPLEX_DERIVATIVE_SUB = prove
1213  (`!f f' g g' net.
1214         (f has_complex_derivative f') net /\ (g has_complex_derivative g') net
1215         ==> ((\x. f(x) - g(x)) has_complex_derivative (f' - g')) net`,
1216   SIMP_TAC[has_complex_derivative; COMPLEX_SUB_RDISTRIB; HAS_DERIVATIVE_SUB]);;
1217
1218 let HAS_COMPLEX_DERIVATIVE_MUL_WITHIN = prove
1219  (`!f f' g g' x s.
1220         (f has_complex_derivative f') (at x within s) /\
1221         (g has_complex_derivative g') (at x within s)
1222         ==> ((\x. f(x) * g(x)) has_complex_derivative
1223              (f(x) * g' + f' * g(x))) (at x within s)`,
1224   REPEAT GEN_TAC THEN SIMP_TAC[has_complex_derivative] THEN
1225   DISCH_THEN(MP_TAC o C CONJ BILINEAR_COMPLEX_MUL) THEN
1226   REWRITE_TAC[GSYM CONJ_ASSOC] THEN
1227   DISCH_THEN(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_WITHIN) THEN
1228   MATCH_MP_TAC EQ_IMP THEN
1229   AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
1230   CONV_TAC COMPLEX_RING);;
1231
1232 let HAS_COMPLEX_DERIVATIVE_MUL_AT = prove
1233  (`!f f' g g' x.
1234         (f has_complex_derivative f') (at x) /\
1235         (g has_complex_derivative g') (at x)
1236         ==> ((\x. f(x) * g(x)) has_complex_derivative
1237              (f(x) * g' + f' * g(x))) (at x)`,
1238   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
1239   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_MUL_WITHIN]);;
1240
1241 let HAS_COMPLEX_DERIVATIVE_POW_WITHIN = prove
1242  (`!f f' x s n. (f has_complex_derivative f') (at x within s)
1243                 ==> ((\x. f(x) pow n) has_complex_derivative
1244                      (Cx(&n) * f(x) pow (n - 1) * f')) (at x within s)`,
1245   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
1246   INDUCT_TAC THEN REWRITE_TAC[complex_pow] THEN
1247   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_CONST; COMPLEX_MUL_LZERO] THEN
1248   POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
1249   DISCH_THEN(MP_TAC o MATCH_MP HAS_COMPLEX_DERIVATIVE_MUL_WITHIN) THEN
1250   REWRITE_TAC[SUC_SUB1] THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
1251   BINOP_TAC THEN REWRITE_TAC[COMPLEX_MUL_AC; GSYM REAL_OF_NUM_SUC] THEN
1252   SPEC_TAC(`n:num`,`n:num`) THEN REWRITE_TAC[CX_ADD] THEN INDUCT_TAC THEN
1253   CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[SUC_SUB1; complex_pow] THEN
1254   CONV_TAC COMPLEX_FIELD);;
1255
1256 let HAS_COMPLEX_DERIVATIVE_POW_AT = prove
1257  (`!f f' x n. (f has_complex_derivative f') (at x)
1258               ==> ((\x. f(x) pow n) has_complex_derivative
1259                    (Cx(&n) * f(x) pow (n - 1) * f')) (at x)`,
1260   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
1261   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_POW_WITHIN]);;
1262
1263 let HAS_COMPLEX_DERIVATIVE_INV_BASIC = prove
1264  (`!x. ~(x = Cx(&0))
1265          ==> ((inv) has_complex_derivative (--inv(x pow 2))) (at x)`,
1266   REPEAT STRIP_TAC THEN
1267   REWRITE_TAC[has_complex_derivative; has_derivative_at] THEN
1268   REWRITE_TAC[LINEAR_COMPLEX_MUL; COMPLEX_VEC_0] THEN
1269   MATCH_MP_TAC LIM_TRANSFORM_AWAY_AT THEN
1270   MAP_EVERY EXISTS_TAC
1271    [`\y. inv(norm(y - x)) % inv(x pow 2 * y) * (y - x) pow 2`; `Cx(&0)`] THEN
1272   ASM_REWRITE_TAC[COMPLEX_CMUL] THEN CONJ_TAC THENL
1273    [POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD; ALL_TAC] THEN
1274   SUBGOAL_THEN `((\y. inv(x pow 2 * y) * (y - x)) --> Cx(&0)) (at x)`
1275   MP_TAC THENL
1276    [LIM_TAC THEN POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD; ALL_TAC] THEN
1277   MATCH_MP_TAC EQ_IMP THEN REWRITE_TAC[LIM_AT] THEN
1278   REWRITE_TAC[dist; COMPLEX_SUB_RZERO] THEN
1279   REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_INV; COMPLEX_NORM_POW] THEN
1280   REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_INV; REAL_ABS_NORM] THEN
1281   REPLICATE_TAC 2 (AP_TERM_TAC THEN ABS_TAC THEN AP_TERM_TAC) THEN
1282   AP_TERM_TAC THEN ABS_TAC THEN
1283   MATCH_MP_TAC(MESON[]
1284    `(p ==> x = y) ==> ((p ==> x < e) <=> (p ==> y < e))`) THEN
1285   MAP_EVERY ABBREV_TAC
1286    [`n = norm(x' - x:complex)`;
1287     `m = inv (norm(x:complex) pow 2 * norm(x':complex))`] THEN
1288   CONV_TAC REAL_FIELD);;
1289
1290 let HAS_COMPLEX_DERIVATIVE_INV_WITHIN = prove
1291  (`!f f' x s. (f has_complex_derivative f') (at x within s) /\
1292               ~(f x = Cx(&0))
1293               ==> ((\x. inv(f(x))) has_complex_derivative (--f' / f(x) pow 2))
1294                   (at x within s)`,
1295   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM o_DEF] THEN
1296   ASM_SIMP_TAC[COMPLEX_FIELD
1297    `~(g = Cx(&0)) ==> --f / g pow 2 = --inv(g pow 2) * f`] THEN
1298   MATCH_MP_TAC COMPLEX_DIFF_CHAIN_WITHIN THEN ASM_REWRITE_TAC[] THEN
1299   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_AT_WITHIN THEN
1300   ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_INV_BASIC]);;
1301
1302 let HAS_COMPLEX_DERIVATIVE_INV_AT = prove
1303  (`!f f' x. (f has_complex_derivative f') (at x) /\
1304             ~(f x = Cx(&0))
1305             ==> ((\x. inv(f(x))) has_complex_derivative (--f' / f(x) pow 2))
1306                 (at x)`,
1307   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
1308   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_INV_WITHIN]);;
1309
1310 let HAS_COMPLEX_DERIVATIVE_DIV_WITHIN = prove
1311  (`!f f' g g' x s.
1312         (f has_complex_derivative f') (at x within s) /\
1313         (g has_complex_derivative g') (at x within s) /\
1314         ~(g(x) = Cx(&0))
1315         ==> ((\x. f(x) / g(x)) has_complex_derivative
1316              (f' * g(x) - f(x) * g') / g(x) pow 2) (at x within s)`,
1317   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1318   DISCH_THEN(fun th -> ASSUME_TAC(CONJUNCT2 th) THEN MP_TAC th) THEN
1319   DISCH_THEN(MP_TAC o MATCH_MP HAS_COMPLEX_DERIVATIVE_INV_WITHIN) THEN
1320   UNDISCH_TAC `(f has_complex_derivative f') (at x within s)` THEN
1321   REWRITE_TAC[IMP_IMP] THEN
1322   DISCH_THEN(MP_TAC o MATCH_MP HAS_COMPLEX_DERIVATIVE_MUL_WITHIN) THEN
1323   REWRITE_TAC[GSYM complex_div] THEN MATCH_MP_TAC EQ_IMP THEN
1324   AP_THM_TAC THEN AP_TERM_TAC THEN
1325   POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD);;
1326
1327 let HAS_COMPLEX_DERIVATIVE_DIV_AT = prove
1328  (`!f f' g g' x.
1329         (f has_complex_derivative f') (at x) /\
1330         (g has_complex_derivative g') (at x) /\
1331         ~(g(x) = Cx(&0))
1332         ==> ((\x. f(x) / g(x)) has_complex_derivative
1333              (f' * g(x) - f(x) * g') / g(x) pow 2) (at x)`,
1334   ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
1335   REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_DIV_WITHIN]);;
1336
1337 let HAS_COMPLEX_DERIVATIVE_VSUM = prove
1338  (`!f net s.
1339          FINITE s /\ (!a. a IN s ==> (f a has_complex_derivative f' a) net)
1340          ==> ((\x. vsum s (\a. f a x)) has_complex_derivative (vsum s f'))
1341              net`,
1342   SIMP_TAC[GSYM VSUM_COMPLEX_RMUL; has_complex_derivative] THEN
1343   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP HAS_DERIVATIVE_VSUM) THEN
1344   REWRITE_TAC[]);;
1345
1346 (* ------------------------------------------------------------------------- *)
1347 (* Same thing just for complex differentiability.                            *)
1348 (* ------------------------------------------------------------------------- *)
1349
1350 let COMPLEX_DIFFERENTIABLE_LINEAR = prove
1351  (`(\z. c * z) complex_differentiable p`,
1352   REWRITE_TAC [complex_differentiable] THEN
1353   MESON_TAC [HAS_COMPLEX_DERIVATIVE_LINEAR]);;
1354
1355 let COMPLEX_DIFFERENTIABLE_CONST = prove
1356  (`!c net. (\z. c) complex_differentiable net`,
1357   REWRITE_TAC[complex_differentiable] THEN
1358   MESON_TAC[HAS_COMPLEX_DERIVATIVE_CONST]);;
1359
1360 let COMPLEX_DIFFERENTIABLE_ID = prove
1361  (`!net. (\z. z) complex_differentiable net`,
1362   REWRITE_TAC[complex_differentiable] THEN
1363   MESON_TAC[HAS_COMPLEX_DERIVATIVE_ID]);;
1364
1365 let COMPLEX_DIFFERENTIABLE_NEG = prove
1366  (`!f net.
1367         f complex_differentiable net
1368         ==> (\z. --(f z)) complex_differentiable net`,
1369   REWRITE_TAC[complex_differentiable] THEN
1370   MESON_TAC[HAS_COMPLEX_DERIVATIVE_NEG]);;
1371
1372 let COMPLEX_DIFFERENTIABLE_ADD = prove
1373  (`!f g net.
1374         f complex_differentiable net /\
1375         g complex_differentiable net
1376         ==> (\z. f z + g z) complex_differentiable net`,
1377   REWRITE_TAC[complex_differentiable] THEN
1378   MESON_TAC[HAS_COMPLEX_DERIVATIVE_ADD]);;
1379
1380 let COMPLEX_DIFFERENTIABLE_SUB = prove
1381  (`!f g net.
1382         f complex_differentiable net /\
1383         g complex_differentiable net
1384         ==> (\z. f z - g z) complex_differentiable net`,
1385   REWRITE_TAC[complex_differentiable] THEN
1386   MESON_TAC[HAS_COMPLEX_DERIVATIVE_SUB]);;
1387
1388 let COMPLEX_DIFFERENTIABLE_INV_WITHIN = prove
1389  (`!f z s.
1390         f complex_differentiable (at z within s) /\ ~(f z = Cx(&0))
1391         ==> (\z. inv(f z)) complex_differentiable (at z within s)`,
1392   REWRITE_TAC[complex_differentiable] THEN
1393   MESON_TAC[HAS_COMPLEX_DERIVATIVE_INV_WITHIN]);;
1394
1395 let COMPLEX_DIFFERENTIABLE_MUL_WITHIN = prove
1396  (`!f g z s.
1397         f complex_differentiable (at z within s) /\
1398         g complex_differentiable (at z within s)
1399         ==> (\z. f z * g z) complex_differentiable (at z within s)`,
1400   REWRITE_TAC[complex_differentiable] THEN
1401   MESON_TAC[HAS_COMPLEX_DERIVATIVE_MUL_WITHIN]);;
1402
1403 let COMPLEX_DIFFERENTIABLE_DIV_WITHIN = prove
1404  (`!f g z s.
1405         f complex_differentiable (at z within s) /\
1406         g complex_differentiable (at z within s) /\
1407         ~(g z = Cx(&0))
1408         ==> (\z. f z / g z) complex_differentiable (at z within s)`,
1409   REWRITE_TAC[complex_differentiable] THEN
1410   MESON_TAC[HAS_COMPLEX_DERIVATIVE_DIV_WITHIN]);;
1411
1412 let COMPLEX_DIFFERENTIABLE_POW_WITHIN = prove
1413  (`!f n z s.
1414         f complex_differentiable (at z within s)
1415         ==> (\z. f z pow n) complex_differentiable (at z within s)`,
1416   REWRITE_TAC[complex_differentiable] THEN
1417   MESON_TAC[HAS_COMPLEX_DERIVATIVE_POW_WITHIN]);;
1418
1419 let COMPLEX_DIFFERENTIABLE_CPRODUCT_WITHIN = prove
1420  (`!f k:A->bool z s.
1421         FINITE k /\
1422         (!i. i IN k ==> f i complex_differentiable (at z within s))
1423         ==> (\z. cproduct k (\i. f i z)) complex_differentiable
1424             (at z within s)`,
1425   GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
1426   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1427   SIMP_TAC[CPRODUCT_CLAUSES; COMPLEX_DIFFERENTIABLE_CONST; FORALL_IN_INSERT;
1428            ETA_AX; COMPLEX_DIFFERENTIABLE_MUL_WITHIN]);;
1429
1430 let COMPLEX_DIFFERENTIABLE_TRANSFORM_WITHIN = prove
1431  (`!f g x s d.
1432         &0 < d /\
1433         x IN s /\
1434         (!x'. x' IN s /\ dist (x',x) < d ==> f x' = g x') /\
1435         f complex_differentiable (at x within s)
1436         ==> g complex_differentiable (at x within s)`,
1437   REWRITE_TAC[complex_differentiable] THEN
1438   MESON_TAC[HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN]);;
1439
1440 let HOLOMORPHIC_TRANSFORM = prove
1441  (`!f g s. (!x. x IN s ==> f x = g x) /\ f holomorphic_on s
1442            ==> g holomorphic_on s`,
1443   REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1444   REWRITE_TAC[holomorphic_on; GSYM complex_differentiable] THEN
1445   MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
1446   DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
1447   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1448   MATCH_MP_TAC COMPLEX_DIFFERENTIABLE_TRANSFORM_WITHIN THEN
1449   MAP_EVERY EXISTS_TAC [`f:complex->complex`; `&1`] THEN
1450   ASM_SIMP_TAC[REAL_LT_01]);;
1451
1452 let HOLOMORPHIC_EQ = prove
1453  (`!f g s. (!x. x IN s ==> f x = g x)
1454            ==> (f holomorphic_on s <=> g holomorphic_on s)`,
1455   MESON_TAC[HOLOMORPHIC_TRANSFORM]);;
1456
1457 let COMPLEX_DIFFERENTIABLE_INV_AT = prove
1458  (`!f z.
1459         f complex_differentiable at z /\ ~(f z = Cx(&0))
1460         ==> (\z. inv(f z)) complex_differentiable at z`,
1461   REWRITE_TAC[complex_differentiable] THEN
1462   MESON_TAC[HAS_COMPLEX_DERIVATIVE_INV_AT]);;
1463
1464 let COMPLEX_DIFFERENTIABLE_MUL_AT = prove
1465  (`!f g z.
1466         f complex_differentiable at z /\
1467         g complex_differentiable at z
1468         ==> (\z. f z * g z) complex_differentiable at z`,
1469   REWRITE_TAC[complex_differentiable] THEN
1470   MESON_TAC[HAS_COMPLEX_DERIVATIVE_MUL_AT]);;
1471
1472 let COMPLEX_DIFFERENTIABLE_DIV_AT = prove
1473  (`!f g z.
1474         f complex_differentiable at z /\
1475         g complex_differentiable at z /\
1476         ~(g z = Cx(&0))
1477         ==> (\z. f z / g z) complex_differentiable at z`,
1478   REWRITE_TAC[complex_differentiable] THEN
1479   MESON_TAC[HAS_COMPLEX_DERIVATIVE_DIV_AT]);;
1480
1481 let COMPLEX_DIFFERENTIABLE_POW_AT = prove
1482  (`!f n z.
1483         f complex_differentiable at z
1484         ==> (\z. f z pow n) complex_differentiable at z`,
1485   REWRITE_TAC[complex_differentiable] THEN
1486   MESON_TAC[HAS_COMPLEX_DERIVATIVE_POW_AT]);;
1487
1488 let COMPLEX_DIFFERENTIABLE_CPRODUCT_AT = prove
1489  (`!f k:A->bool z.
1490         FINITE k /\
1491         (!i. i IN k ==> f i complex_differentiable (at z))
1492         ==> (\z. cproduct k (\i. f i z)) complex_differentiable (at z)`,
1493   GEN_TAC THEN REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
1494   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
1495   SIMP_TAC[CPRODUCT_CLAUSES; COMPLEX_DIFFERENTIABLE_CONST; FORALL_IN_INSERT;
1496            ETA_AX; COMPLEX_DIFFERENTIABLE_MUL_AT]);;
1497
1498 let COMPLEX_DIFFERENTIABLE_TRANSFORM_AT = prove
1499  (`!f g x d.
1500         &0 < d /\
1501         (!x'. dist (x',x) < d ==> f x' = g x') /\
1502         f complex_differentiable at x
1503         ==> g complex_differentiable at x`,
1504   REWRITE_TAC[complex_differentiable] THEN
1505   MESON_TAC[HAS_COMPLEX_DERIVATIVE_TRANSFORM_AT]);;
1506
1507 let COMPLEX_DIFFERENTIABLE_COMPOSE_WITHIN = prove
1508  (`!f g x s.
1509          f complex_differentiable (at x within s) /\
1510          g complex_differentiable (at (f x) within IMAGE f s)
1511          ==> (g o f) complex_differentiable (at x within s)`,
1512   REWRITE_TAC[complex_differentiable] THEN
1513   MESON_TAC[COMPLEX_DIFF_CHAIN_WITHIN]);;
1514
1515 let COMPLEX_DIFFERENTIABLE_COMPOSE_AT = prove
1516  (`!f g x s.
1517          f complex_differentiable (at x) /\
1518          g complex_differentiable (at (f x))
1519          ==> (g o f) complex_differentiable (at x)`,
1520   REWRITE_TAC[complex_differentiable] THEN
1521   MESON_TAC[COMPLEX_DIFF_CHAIN_AT]);;
1522
1523 let COMPLEX_DIFFERENTIABLE_WITHIN_OPEN = prove
1524  (`!f a s.
1525         a IN s /\ open s
1526         ==> (f complex_differentiable at a within s <=>
1527              f complex_differentiable at a)`,
1528   SIMP_TAC[complex_differentiable; HAS_COMPLEX_DERIVATIVE_WITHIN_OPEN]);;
1529
1530 (* ------------------------------------------------------------------------- *)
1531 (* Same again for being holomorphic on a set.                                *)
1532 (* ------------------------------------------------------------------------- *)
1533
1534 let HOLOMORPHIC_ON_LINEAR = prove
1535  (`!s c. (\w. c * w) holomorphic_on s`,
1536   REWRITE_TAC [holomorphic_on] THEN
1537   MESON_TAC [HAS_COMPLEX_DERIVATIVE_LINEAR]);;
1538
1539 let HOLOMORPHIC_ON_CONST = prove
1540  (`!c s. (\z. c) holomorphic_on s`,
1541   REWRITE_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE; COMPLEX_DIFFERENTIABLE_CONST]);;
1542
1543 let HOLOMORPHIC_ON_ID = prove
1544  (`!s. (\z. z) holomorphic_on s`,
1545   REWRITE_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE; COMPLEX_DIFFERENTIABLE_ID]);;
1546
1547 let HOLOMORPHIC_ON_COMPOSE = prove
1548  (`!f g s. f holomorphic_on s /\ g holomorphic_on (IMAGE f s)
1549            ==> (g o f) holomorphic_on s`,
1550   SIMP_TAC[holomorphic_on; GSYM complex_differentiable; FORALL_IN_IMAGE] THEN
1551   MESON_TAC[COMPLEX_DIFFERENTIABLE_COMPOSE_WITHIN]);;
1552
1553 let HOLOMORPHIC_ON_NEG = prove
1554  (`!f s. f holomorphic_on s ==> (\z. --(f z)) holomorphic_on s`,
1555   SIMP_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE; COMPLEX_DIFFERENTIABLE_NEG]);;
1556
1557 let HOLOMORPHIC_ON_ADD = prove
1558  (`!f g s.
1559         f holomorphic_on s /\ g holomorphic_on s
1560         ==> (\z. f z + g z) holomorphic_on s`,
1561   SIMP_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE; COMPLEX_DIFFERENTIABLE_ADD]);;
1562
1563 let HOLOMORPHIC_ON_SUB = prove
1564  (`!f g s.
1565         f holomorphic_on s /\ g holomorphic_on s
1566         ==> (\z. f z - g z) holomorphic_on s`,
1567   SIMP_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE; COMPLEX_DIFFERENTIABLE_SUB]);;
1568
1569 let HOLOMORPHIC_ON_MUL = prove
1570  (`!f g s.
1571         f holomorphic_on s /\ g holomorphic_on s
1572         ==> (\z. f z * g z) holomorphic_on s`,
1573   SIMP_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE; COMPLEX_DIFFERENTIABLE_MUL_WITHIN]);;
1574
1575 let HOLOMORPHIC_ON_LMUL = prove
1576  (`!f c s. f holomorphic_on s ==> (\x. c * f x) holomorphic_on s`,
1577   SIMP_TAC[HOLOMORPHIC_ON_MUL; HOLOMORPHIC_ON_CONST]);;
1578
1579 let HOLOMORPHIC_ON_RMUL = prove
1580  (`!f c s. f holomorphic_on s ==> (\x. f x * c) holomorphic_on s`,
1581   SIMP_TAC[HOLOMORPHIC_ON_MUL; HOLOMORPHIC_ON_CONST]);;
1582
1583 let HOLOMORPHIC_ON_INV = prove
1584  (`!f s. f holomorphic_on s /\ (!z. z IN s ==> ~(f z = Cx(&0)))
1585          ==> (\z. inv(f z)) holomorphic_on s`,
1586   SIMP_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE; COMPLEX_DIFFERENTIABLE_INV_WITHIN]);;
1587
1588 let HOLOMORPHIC_ON_DIV = prove
1589  (`!f g s.
1590         f holomorphic_on s /\ g holomorphic_on s /\
1591         (!z. z IN s ==> ~(g z = Cx(&0)))
1592         ==> (\z. f z / g z) holomorphic_on s`,
1593   SIMP_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE; COMPLEX_DIFFERENTIABLE_DIV_WITHIN]);;
1594
1595 let HOLOMORPHIC_ON_POW = prove
1596  (`!f s n. f holomorphic_on s ==> (\z. (f z) pow n) holomorphic_on s`,
1597   SIMP_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE; COMPLEX_DIFFERENTIABLE_POW_WITHIN]);;
1598
1599 let HOLOMORPHIC_ON_VSUM = prove
1600  (`!f s k. FINITE k /\ (!a. a IN k ==> (f a) holomorphic_on s)
1601            ==> (\x. vsum k (\a. f a x)) holomorphic_on s`,
1602   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
1603   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN SIMP_TAC[VSUM_CLAUSES] THEN
1604   SIMP_TAC[HOLOMORPHIC_ON_CONST; IN_INSERT; NOT_IN_EMPTY] THEN
1605   REPEAT STRIP_TAC THEN MATCH_MP_TAC HOLOMORPHIC_ON_ADD THEN
1606   ASM_SIMP_TAC[ETA_AX]);;
1607
1608 let HOLOMORPHIC_ON_CPRODUCT = prove
1609  (`!f k:A->bool s.
1610         FINITE k /\
1611         (!i. i IN k ==> f i holomorphic_on s)
1612         ==> (\z. cproduct k (\i. f i z)) holomorphic_on s`,
1613   SIMP_TAC[HOLOMORPHIC_ON_DIFFERENTIABLE;
1614            COMPLEX_DIFFERENTIABLE_CPRODUCT_WITHIN]);;
1615
1616 let HOLOMORPHIC_ON_COMPOSE_GEN = prove
1617  (`!f g s t. f holomorphic_on s /\ g holomorphic_on t /\
1618              (!z. z IN s ==> f z IN t)
1619              ==>  g o f holomorphic_on s`,
1620   REWRITE_TAC [holomorphic_on] THEN REPEAT STRIP_TAC THEN
1621   SUBGOAL_THEN `IMAGE (f:complex->complex) s SUBSET t` MP_TAC THENL
1622    [ASM SET_TAC []; ASM_MESON_TAC [HAS_COMPLEX_DERIVATIVE_WITHIN_SUBSET;
1623                                    COMPLEX_DIFF_CHAIN_WITHIN]]);;
1624
1625 (* ------------------------------------------------------------------------- *)
1626 (* Same again for the actual derivative function.                            *)
1627 (* ------------------------------------------------------------------------- *)
1628
1629 let HAS_COMPLEX_DERIVATIVE_DERIVATIVE = prove
1630  (`!f f' x. (f has_complex_derivative f') (at x)
1631                 ==> complex_derivative f x = f'`,
1632   REWRITE_TAC[complex_derivative] THEN
1633   MESON_TAC[COMPLEX_DERIVATIVE_UNIQUE_AT]);;
1634
1635 let HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE = prove
1636  (`!f x. (f has_complex_derivative (complex_derivative f x)) (at x) <=>
1637          f complex_differentiable at x`,
1638   REWRITE_TAC[complex_differentiable; complex_derivative] THEN MESON_TAC[]);;
1639
1640 let COMPLEX_DIFFERENTIABLE_COMPOSE = prove
1641  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at (f z)
1642           ==> (g o f) complex_differentiable at z`,
1643   REWRITE_TAC [complex_differentiable] THEN
1644   MESON_TAC [COMPLEX_DIFF_CHAIN_AT]);;
1645
1646 let COMPLEX_DERIVATIVE_CHAIN = prove
1647  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at (f z)
1648            ==> complex_derivative (g o f) z =
1649                complex_derivative g (f z) * complex_derivative f z`,
1650   MESON_TAC [HAS_COMPLEX_DERIVATIVE_DERIVATIVE; COMPLEX_DIFF_CHAIN_AT;
1651              HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;
1652
1653 let COMPLEX_DERIVATIVE_LINEAR = prove
1654  (`!c. complex_derivative (\w. c * w) = \z. c`,
1655   REWRITE_TAC [FUN_EQ_THM] THEN REPEAT GEN_TAC THEN
1656   MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
1657   REWRITE_TAC [HAS_COMPLEX_DERIVATIVE_LINEAR]);;
1658
1659 let COMPLEX_DERIVATIVE_ID = prove
1660  (`complex_derivative (\w.w) = \z. Cx(&1)`,
1661   REWRITE_TAC [FUN_EQ_THM] THEN
1662   MESON_TAC [HAS_COMPLEX_DERIVATIVE_DERIVATIVE; HAS_COMPLEX_DERIVATIVE_ID]);;
1663
1664 let COMPLEX_DERIVATIVE_CONST = prove
1665  (`!c. complex_derivative (\w.c) = \z. Cx(&0)`,
1666   REWRITE_TAC [FUN_EQ_THM] THEN
1667   MESON_TAC [HAS_COMPLEX_DERIVATIVE_DERIVATIVE;
1668              HAS_COMPLEX_DERIVATIVE_CONST]);;
1669
1670 let COMPLEX_DERIVATIVE_ADD = prove
1671  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at z
1672            ==> complex_derivative (\w. f w + g w) z =
1673                complex_derivative f z + complex_derivative g z`,
1674   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
1675   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_ADD;
1676                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;
1677
1678 let COMPLEX_DERIVATIVE_SUB = prove
1679  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at z
1680            ==> complex_derivative (\w. f w - g w) z =
1681                complex_derivative f z - complex_derivative g z`,
1682   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
1683   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_SUB;
1684                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;
1685
1686 let COMPLEX_DERIVATIVE_MUL = prove
1687  (`!f g z. f complex_differentiable at z /\ g complex_differentiable at z
1688            ==> complex_derivative (\w. f w * g w) z =
1689                f z * complex_derivative g z + complex_derivative f z * g z`,
1690   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
1691   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_MUL_AT;
1692                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;
1693
1694 let COMPLEX_DERIVATIVE_LMUL = prove
1695  (`!f c z. f complex_differentiable at z
1696              ==> complex_derivative (\w. c * f w) z =
1697                  c * complex_derivative f z`,
1698   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
1699   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_LMUL_AT;
1700                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;
1701
1702 let COMPLEX_DERIVATIVE_RMUL = prove
1703  (`!f c z. f complex_differentiable at z
1704            ==> complex_derivative (\w. f w * c) z =
1705                complex_derivative f z * c`,
1706   REPEAT STRIP_TAC THEN MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
1707   ASM_SIMP_TAC [HAS_COMPLEX_DERIVATIVE_RMUL_AT;
1708                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;
1709
1710 let COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN = prove
1711  (`!f g s z. open s /\ f holomorphic_on s /\ g holomorphic_on s /\ z IN s /\
1712              (!w. w IN s ==> f w = g w)
1713              ==> complex_derivative f z = complex_derivative g z`,
1714   REPEAT STRIP_TAC THEN MATCH_MP_TAC COMPLEX_DERIVATIVE_UNIQUE_AT THEN
1715   ASM_MESON_TAC[HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN;
1716                 HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT;
1717                 HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE]);;
1718
1719 let COMPLEX_DERIVATIVE_COMPOSE_LINEAR = prove
1720  (`!f c z. f complex_differentiable at (c * z)
1721            ==> complex_derivative (\w. f (c * w)) z =
1722                c * complex_derivative f (c * z)`,
1723   SIMP_TAC
1724     [COMPLEX_MUL_SYM; REWRITE_RULE [o_DEF; COMPLEX_DIFFERENTIABLE_ID;
1725                    COMPLEX_DIFFERENTIABLE_LINEAR;
1726                    COMPLEX_DERIVATIVE_LINEAR]
1727      (SPECL [`\w:complex. c * w`] COMPLEX_DERIVATIVE_CHAIN)]);;
1728
1729 (* ------------------------------------------------------------------------- *)
1730 (* Caratheodory characterization.                                            *)
1731 (* ------------------------------------------------------------------------- *)
1732
1733 let HAS_COMPLEX_DERIVATIVE_CARATHEODORY_AT = prove
1734  (`!f f' z.
1735         (f has_complex_derivative f') (at z) <=>
1736         ?g. (!w. f(w) - f(z) = g(w) * (w - z)) /\
1737             g continuous at z /\ g(z) = f'`,
1738   REPEAT GEN_TAC THEN
1739   REWRITE_TAC[COMPLEX_RING `w' - z':complex = a <=> w' = z' + a`] THEN
1740   SIMP_TAC[GSYM FUN_EQ_THM; HAS_COMPLEX_DERIVATIVE_AT; CONTINUOUS_AT] THEN
1741   EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
1742    [EXISTS_TAC `\w. if w = z then f':complex else (f(w) - f(z)) / (w - z)` THEN
1743     ASM_SIMP_TAC[FUN_EQ_THM; COND_RAND; COND_RATOR; COMPLEX_SUB_REFL] THEN
1744     CONV_TAC COMPLEX_FIELD;
1745     FIRST_X_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN
1746     ASM_SIMP_TAC[COMPLEX_RING `(z + a) - (z + b * (w - w)):complex = a`] THEN
1747     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
1748       LIM_TRANSFORM)) THEN
1749     SIMP_TAC[LIM_CONST; COMPLEX_VEC_0; COMPLEX_FIELD
1750      `~(w = z) ==> x - (x * (w - z)) / (w - z) = Cx(&0)`]]);;
1751
1752 let HAS_COMPLEX_DERIVATIVE_CARATHEODORY_WITHIN = prove
1753  (`!f f' z s.
1754         (f has_complex_derivative f') (at z within s) <=>
1755         ?g. (!w. f(w) - f(z) = g(w) * (w - z)) /\
1756             g continuous (at z within s) /\ g(z) = f'`,
1757   REPEAT GEN_TAC THEN
1758   REWRITE_TAC[COMPLEX_RING `w' - z':complex = a <=> w' = z' + a`] THEN
1759   SIMP_TAC[GSYM FUN_EQ_THM; HAS_COMPLEX_DERIVATIVE_WITHIN;
1760            CONTINUOUS_WITHIN] THEN
1761   EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
1762    [EXISTS_TAC `\w. if w = z then f':complex else (f(w) - f(z)) / (w - z)` THEN
1763     ASM_SIMP_TAC[FUN_EQ_THM; COND_RAND; COND_RATOR; COMPLEX_SUB_REFL] THEN
1764     CONV_TAC COMPLEX_FIELD;
1765     FIRST_X_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN
1766     ASM_SIMP_TAC[COMPLEX_RING `(z + a) - (z + b * (w - w)):complex = a`] THEN
1767     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
1768       LIM_TRANSFORM)) THEN
1769     SIMP_TAC[LIM_CONST; COMPLEX_VEC_0; COMPLEX_FIELD
1770      `~(w = z) ==> x - (x * (w - z)) / (w - z) = Cx(&0)`]]);;
1771
1772 let COMPLEX_DIFFERENTIABLE_CARATHEODORY_AT = prove
1773  (`!f z. f complex_differentiable at z <=>
1774          ?g. (!w. f(w) - f(z) = g(w) * (w - z)) /\ g continuous at z`,
1775   SIMP_TAC[complex_differentiable; HAS_COMPLEX_DERIVATIVE_CARATHEODORY_AT] THEN
1776   MESON_TAC[]);;
1777
1778 let COMPLEX_DIFFERENTIABLE_CARATHEODORY_WITHIN = prove
1779  (`!f z s.
1780       f complex_differentiable (at z within s) <=>
1781       ?g. (!w. f(w) - f(z) = g(w) * (w - z)) /\ g continuous (at z within s)`,
1782   SIMP_TAC[complex_differentiable;
1783            HAS_COMPLEX_DERIVATIVE_CARATHEODORY_WITHIN] THEN
1784   MESON_TAC[]);;
1785
1786 (* ------------------------------------------------------------------------- *)
1787 (* A slightly stronger, more traditional notion of analyticity on a set.     *)
1788 (* ------------------------------------------------------------------------- *)
1789
1790 parse_as_infix ("analytic_on",(12,"right"));;
1791
1792 let analytic_on = new_definition
1793  `f analytic_on s <=>
1794       !x. x IN s ==> ?e. &0 < e /\ f holomorphic_on ball(x,e)`;;
1795
1796 let ANALYTIC_IMP_HOLOMORPHIC = prove
1797  (`!f s. f analytic_on s ==> f holomorphic_on s`,
1798   REWRITE_TAC[analytic_on; holomorphic_on] THEN
1799   SIMP_TAC[HAS_COMPLEX_DERIVATIVE_WITHIN_OPEN; OPEN_BALL] THEN
1800   MESON_TAC[HAS_COMPLEX_DERIVATIVE_AT_WITHIN; CENTRE_IN_BALL]);;
1801
1802 let ANALYTIC_ON_OPEN = prove
1803  (`!f s. open s ==> (f analytic_on s <=> f holomorphic_on s)`,
1804   REPEAT STRIP_TAC THEN EQ_TAC THEN REWRITE_TAC[ANALYTIC_IMP_HOLOMORPHIC] THEN
1805   REWRITE_TAC[analytic_on; holomorphic_on] THEN
1806   ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_WITHIN_OPEN; OPEN_BALL] THEN
1807   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [OPEN_CONTAINS_BALL]) THEN
1808   REWRITE_TAC[SUBSET] THEN MESON_TAC[CENTRE_IN_BALL]);;
1809
1810 let ANALYTIC_ON_IMP_DIFFERENTIABLE_AT = prove
1811  (`!f s x. f analytic_on s /\ x IN s ==> f complex_differentiable (at x)`,
1812   SIMP_TAC[analytic_on; HOLOMORPHIC_ON_OPEN; OPEN_BALL;
1813            complex_differentiable] THEN
1814   MESON_TAC[CENTRE_IN_BALL]);;
1815
1816 let ANALYTIC_ON_SUBSET = prove
1817  (`!f s t. f analytic_on s /\ t SUBSET s ==> f analytic_on t`,
1818   REWRITE_TAC[analytic_on; SUBSET] THEN MESON_TAC[]);;
1819
1820 let ANALYTIC_ON_UNION = prove
1821  (`!f s t. f analytic_on (s UNION t) <=> f analytic_on s /\ f analytic_on t`,
1822   REWRITE_TAC [analytic_on; IN_UNION] THEN MESON_TAC[]);;
1823
1824 let ANALYTIC_ON_UNIONS = prove
1825  (`!f s. f analytic_on (UNIONS s) <=> (!t. t IN s ==> f analytic_on t)`,
1826   REWRITE_TAC [analytic_on; IN_UNIONS] THEN MESON_TAC[]);;
1827
1828 let ANALYTIC_ON_HOLOMORPHIC = prove
1829  (`!f s. f analytic_on s <=> ?t. open t /\ s SUBSET t /\ f holomorphic_on t`,
1830   REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1831   EXISTS_TAC `?t. open t /\ s SUBSET t /\ f analytic_on t` THEN CONJ_TAC THENL
1832    [EQ_TAC THENL
1833     [DISCH_TAC THEN EXISTS_TAC `UNIONS {u | open u /\ f analytic_on u}` THEN
1834      SIMP_TAC [IN_ELIM_THM; OPEN_UNIONS; ANALYTIC_ON_UNIONS] THEN
1835      REWRITE_TAC [SUBSET; IN_UNIONS; IN_ELIM_THM] THEN
1836      ASM_MESON_TAC [analytic_on; ANALYTIC_ON_OPEN; OPEN_BALL; CENTRE_IN_BALL];
1837      MESON_TAC [ANALYTIC_ON_SUBSET]];
1838     MESON_TAC [ANALYTIC_ON_OPEN]]);;
1839
1840 let ANALYTIC_ON_LINEAR = prove
1841  (`!s c. (\w. c * w) analytic_on s`,
1842   REPEAT GEN_TAC THEN
1843   REWRITE_TAC [ANALYTIC_ON_HOLOMORPHIC; HOLOMORPHIC_ON_LINEAR] THEN
1844   EXISTS_TAC `(:complex)` THEN REWRITE_TAC [OPEN_UNIV; SUBSET_UNIV]);;
1845
1846 let ANALYTIC_ON_CONST = prove
1847  (`!c s. (\z. c) analytic_on s`,
1848   REWRITE_TAC[analytic_on; HOLOMORPHIC_ON_CONST] THEN MESON_TAC[REAL_LT_01]);;
1849
1850 let ANALYTIC_ON_ID = prove
1851  (`!s. (\z. z) analytic_on s`,
1852   REWRITE_TAC[analytic_on; HOLOMORPHIC_ON_ID] THEN MESON_TAC[REAL_LT_01]);;
1853
1854 let ANALYTIC_ON_COMPOSE = prove
1855  (`!f g s. f analytic_on s /\ g analytic_on (IMAGE f s)
1856            ==> (g o f) analytic_on s`,
1857   REWRITE_TAC[analytic_on; FORALL_IN_IMAGE] THEN REPEAT GEN_TAC THEN
1858   DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "f") (LABEL_TAC "g")) THEN
1859   X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
1860   REMOVE_THEN "f" (MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
1861   DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
1862   FIRST_ASSUM(MP_TAC o MATCH_MP HOLOMORPHIC_ON_IMP_CONTINUOUS_ON) THEN
1863   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_AT; OPEN_BALL] THEN
1864   DISCH_THEN(MP_TAC o SPEC `z:complex`) THEN
1865   ASM_REWRITE_TAC[CENTRE_IN_BALL; CONTINUOUS_AT_BALL] THEN
1866   FIRST_X_ASSUM(MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
1867   DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
1868   DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
1869   DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
1870   EXISTS_TAC `min (d:real) k` THEN ASM_REWRITE_TAC[REAL_LT_MIN] THEN
1871   MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE THEN
1872   CONJ_TAC THEN MATCH_MP_TAC HOLOMORPHIC_ON_SUBSET THENL
1873    [EXISTS_TAC `ball(z:complex,d)`;
1874     EXISTS_TAC `ball((f:complex->complex) z,e)`] THEN
1875   ASM_REWRITE_TAC[BALL_MIN_INTER; INTER_SUBSET] THEN ASM SET_TAC[]);;
1876
1877 let ANALYTIC_ON_COMPOSE_GEN = prove
1878  (`!f g s t. f analytic_on s /\ g analytic_on t /\ (!z. z IN s ==> f z IN t)
1879              ==> g o f analytic_on s`,
1880   REPEAT STRIP_TAC THEN MATCH_MP_TAC ANALYTIC_ON_COMPOSE THEN
1881   ASM_REWRITE_TAC[] THEN MATCH_MP_TAC ANALYTIC_ON_SUBSET THEN ASM SET_TAC[]);;
1882
1883 let ANALYTIC_ON_NEG = prove
1884  (`!f s. f analytic_on s ==> (\z. --(f z)) analytic_on s`,
1885   SIMP_TAC[analytic_on] THEN MESON_TAC[HOLOMORPHIC_ON_NEG]);;
1886
1887 let ANALYTIC_ON_ADD = prove
1888  (`!f g s.
1889         f analytic_on s /\ g analytic_on s ==> (\z. f z + g z) analytic_on s`,
1890   REPEAT GEN_TAC THEN REWRITE_TAC[analytic_on] THEN
1891   REWRITE_TAC[AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
1892   GEN_TAC THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
1893   ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2
1894    (X_CHOOSE_TAC `d:real`) (X_CHOOSE_TAC `e:real`)) THEN
1895   EXISTS_TAC `min (d:real) e` THEN
1896   ASM_REWRITE_TAC[REAL_LT_MIN; BALL_MIN_INTER; IN_INTER] THEN
1897   MATCH_MP_TAC HOLOMORPHIC_ON_ADD THEN
1898   ASM_MESON_TAC[HOLOMORPHIC_ON_SUBSET; INTER_SUBSET]);;
1899
1900 let ANALYTIC_ON_SUB = prove
1901  (`!f g s.
1902         f analytic_on s /\ g analytic_on s ==> (\z. f z - g z) analytic_on s`,
1903   SIMP_TAC[complex_sub; ANALYTIC_ON_ADD; ANALYTIC_ON_NEG]);;
1904
1905 let ANALYTIC_ON_MUL = prove
1906  (`!f g s.
1907         f analytic_on s /\ g analytic_on s ==> (\z. f z * g z) analytic_on s`,
1908   REPEAT GEN_TAC THEN REWRITE_TAC[analytic_on] THEN
1909   REWRITE_TAC[AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
1910   GEN_TAC THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
1911   ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2
1912    (X_CHOOSE_TAC `d:real`) (X_CHOOSE_TAC `e:real`)) THEN
1913   EXISTS_TAC `min (d:real) e` THEN
1914   ASM_REWRITE_TAC[REAL_LT_MIN; BALL_MIN_INTER; IN_INTER] THEN
1915   MATCH_MP_TAC HOLOMORPHIC_ON_MUL THEN
1916   ASM_MESON_TAC[HOLOMORPHIC_ON_SUBSET; INTER_SUBSET]);;
1917
1918 let ANALYTIC_ON_INV = prove
1919  (`!f s. f analytic_on s /\ (!z. z IN s ==> ~(f z = Cx(&0)))
1920          ==> (\z. inv(f z)) analytic_on s`,
1921   REPEAT STRIP_TAC THEN REWRITE_TAC[analytic_on] THEN
1922   X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
1923   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [analytic_on]) THEN
1924   DISCH_THEN(MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
1925   DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
1926   SUBGOAL_THEN `?e. &0 < e /\ !y:complex. dist(z,y) < e ==> ~(f y = Cx(&0))`
1927   MP_TAC THENL
1928    [MATCH_MP_TAC CONTINUOUS_ON_OPEN_AVOID THEN
1929     EXISTS_TAC `ball(z:complex,d)` THEN
1930     ASM_SIMP_TAC[HOLOMORPHIC_ON_IMP_CONTINUOUS_ON; CENTRE_IN_BALL; OPEN_BALL];
1931     REWRITE_TAC[GSYM IN_BALL] THEN
1932     DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
1933     EXISTS_TAC `min (d:real) e` THEN ASM_REWRITE_TAC[REAL_LT_MIN] THEN
1934     MATCH_MP_TAC HOLOMORPHIC_ON_INV THEN
1935     ASM_SIMP_TAC[BALL_MIN_INTER; IN_INTER] THEN
1936     ASM_MESON_TAC[HOLOMORPHIC_ON_SUBSET; INTER_SUBSET]]);;
1937
1938 let ANALYTIC_ON_DIV = prove
1939  (`!f g s.
1940         f analytic_on s /\ g analytic_on s /\
1941         (!z. z IN s ==> ~(g z = Cx(&0)))
1942         ==> (\z. f z / g z) analytic_on s`,
1943   SIMP_TAC[complex_div; ANALYTIC_ON_MUL; ANALYTIC_ON_INV]);;
1944
1945 let ANALYTIC_ON_POW = prove
1946  (`!f s n. f analytic_on s ==> (\z. (f z) pow n) analytic_on s`,
1947   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN
1948   DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[complex_pow] THEN
1949   ASM_SIMP_TAC[ANALYTIC_ON_CONST; ANALYTIC_ON_MUL]);;
1950
1951 let ANALYTIC_ON_VSUM = prove
1952  (`!f s k. FINITE k /\ (!a. a IN k ==> (f a) analytic_on s)
1953            ==> (\x. vsum k (\a. f a x)) analytic_on s`,
1954   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
1955   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN SIMP_TAC[VSUM_CLAUSES] THEN
1956   SIMP_TAC[ANALYTIC_ON_CONST; IN_INSERT; NOT_IN_EMPTY] THEN
1957   REPEAT STRIP_TAC THEN MATCH_MP_TAC ANALYTIC_ON_ADD THEN
1958   ASM_SIMP_TAC[ETA_AX]);;
1959
1960 (* ------------------------------------------------------------------------- *)
1961 (* The case of analyticity at a point.                                       *)
1962 (* ------------------------------------------------------------------------- *)
1963
1964 let ANALYTIC_AT_BALL = prove
1965  (`!f z. f analytic_on {z} <=> ?e. &0<e /\ f holomorphic_on ball (z,e)`,
1966   REWRITE_TAC [analytic_on; IN_SING] THEN MESON_TAC []);;
1967
1968 let ANALYTIC_AT = prove
1969  (`!f z. f analytic_on {z} <=> ?s. open s /\ z IN s /\ f holomorphic_on s`,
1970   REWRITE_TAC [ANALYTIC_ON_HOLOMORPHIC; SING_SUBSET]);;
1971
1972 let ANALYTIC_ON_ANALYTIC_AT = prove
1973  (`!f s. f analytic_on s <=> !z. z IN s ==> f analytic_on {z}`,
1974   REWRITE_TAC [ANALYTIC_AT_BALL; analytic_on]);;
1975
1976 let ANALYTIC_AT_TWO = prove
1977  (`!f g z. f analytic_on {z} /\ g analytic_on {z} <=>
1978     ?s. open s /\ z IN s /\ f holomorphic_on s /\ g holomorphic_on s`,
1979   REWRITE_TAC [ANALYTIC_AT] THEN
1980   MESON_TAC [HOLOMORPHIC_ON_SUBSET; OPEN_INTER; INTER_SUBSET; IN_INTER]);;
1981
1982 let ANALYTIC_AT_ADD = prove
1983  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
1984      ==> (\w. f w + g w) analytic_on {z}`,
1985   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REWRITE_TAC [ANALYTIC_AT] THEN
1986   MESON_TAC [HOLOMORPHIC_ON_ADD]);;
1987
1988 let ANALYTIC_AT_SUB = prove
1989  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
1990      ==> (\w. f w - g w) analytic_on {z}`,
1991   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REWRITE_TAC [ANALYTIC_AT] THEN
1992   MESON_TAC [HOLOMORPHIC_ON_SUB]);;
1993
1994 let ANALYTIC_AT_MUL = prove
1995  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
1996
1997      ==> (\w. f w * g w) analytic_on {z}`,
1998   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REWRITE_TAC [ANALYTIC_AT] THEN
1999   MESON_TAC [HOLOMORPHIC_ON_MUL]);;
2000
2001 let ANALYTIC_AT_POW = prove
2002  (`!f n z. f analytic_on {z}
2003      ==> (\w. f w pow n) analytic_on {z}`,
2004   REWRITE_TAC [ANALYTIC_AT] THEN MESON_TAC [HOLOMORPHIC_ON_POW]);;
2005
2006 (* ------------------------------------------------------------------------- *)
2007 (* Combining theorems for derivative with analytic_at {z} hypotheses.        *)
2008 (* ------------------------------------------------------------------------- *)
2009
2010 let COMPLEX_DERIVATIVE_ADD_AT = prove
2011  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
2012      ==> complex_derivative (\w. f w + g w) z =
2013            complex_derivative f z + complex_derivative g z`,
2014   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REPEAT STRIP_TAC THEN
2015   MATCH_MP_TAC COMPLEX_DERIVATIVE_ADD THEN
2016   ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;
2017
2018 let COMPLEX_DERIVATIVE_SUB_AT = prove
2019  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
2020      ==> complex_derivative (\w. f w - g w) z =
2021            complex_derivative f z - complex_derivative g z`,
2022   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REPEAT STRIP_TAC THEN
2023   MATCH_MP_TAC COMPLEX_DERIVATIVE_SUB THEN
2024   ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;
2025
2026 let COMPLEX_DERIVATIVE_MUL_AT = prove
2027  (`!f g z. f analytic_on {z} /\ g analytic_on {z}
2028      ==> complex_derivative (\w. f w * g w) z =
2029            f z * complex_derivative g z + complex_derivative f z * g z`,
2030   REWRITE_TAC [ANALYTIC_AT_TWO] THEN REPEAT STRIP_TAC THEN
2031   MATCH_MP_TAC COMPLEX_DERIVATIVE_MUL THEN
2032   ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;
2033
2034 let COMPLEX_DERIVATIVE_LMUL_AT = prove
2035  (`!f c z. f analytic_on {z}
2036     ==> complex_derivative (\w. c * f w) z = c * complex_derivative f z`,
2037   REWRITE_TAC [ANALYTIC_AT] THEN
2038   MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT; COMPLEX_DERIVATIVE_LMUL]);;
2039
2040 let COMPLEX_DERIVATIVE_RMUL_AT = prove
2041  (`!f c z. f analytic_on {z}
2042     ==> complex_derivative (\w. f w * c) z = complex_derivative f z * c`,
2043   REWRITE_TAC [ANALYTIC_AT] THEN
2044   MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT; COMPLEX_DERIVATIVE_RMUL]);;
2045
2046 (* ------------------------------------------------------------------------- *)
2047 (* A composition lemma for functions of mixed type.                          *)
2048 (* ------------------------------------------------------------------------- *)
2049
2050 let HAS_VECTOR_DERIVATIVE_REAL_COMPLEX = prove
2051  (`(f has_complex_derivative f') (at(Cx(drop a)))
2052    ==> ((\x. f(Cx(drop x))) has_vector_derivative f') (at a)`,
2053   REWRITE_TAC[has_complex_derivative; has_vector_derivative] THEN
2054   REWRITE_TAC[COMPLEX_CMUL] THEN MP_TAC(ISPECL
2055    [`\x. Cx(drop x)`; `f:complex->complex`;
2056     `\x. Cx(drop x)`; `\x:complex. f' * x`; `a:real^1`] DIFF_CHAIN_AT) THEN
2057   REWRITE_TAC[o_DEF; COMPLEX_MUL_SYM; IMP_CONJ] THEN
2058   DISCH_THEN MATCH_MP_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
2059   REWRITE_TAC[linear; DROP_ADD; DROP_CMUL; CX_ADD; CX_MUL; COMPLEX_CMUL]);;
2060
2061 let DIFFERENTIABLE_REAL_COMPLEX = prove
2062  (`!f a. f complex_differentiable at (Cx(drop a))
2063          ==> (\x. f(Cx(drop x))) differentiable at a`,
2064   REWRITE_TAC[complex_differentiable; VECTOR_DERIVATIVE_WORKS] THEN
2065   REPEAT STRIP_TAC THEN REWRITE_TAC[vector_derivative] THEN
2066   ASM_MESON_TAC[HAS_VECTOR_DERIVATIVE_REAL_COMPLEX]);;
2067
2068 (* ------------------------------------------------------------------------- *)
2069 (* Complex differentiation of sequences and series.                          *)
2070 (* ------------------------------------------------------------------------- *)
2071
2072 let HAS_COMPLEX_DERIVATIVE_SEQUENCE = prove
2073  (`!s f f' g'.
2074          convex s /\
2075          (!n x. x IN s
2076                 ==> (f n has_complex_derivative f' n x) (at x within s)) /\
2077          (!e. &0 < e
2078               ==> ?N. !n x. n >= N /\ x IN s ==> norm (f' n x - g' x) <= e) /\
2079          (?x l. x IN s /\ ((\n. f n x) --> l) sequentially)
2080          ==> ?g. !x. x IN s
2081                      ==> ((\n. f n x) --> g x) sequentially /\
2082                          (g has_complex_derivative g' x) (at x within s)`,
2083   REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
2084   MATCH_MP_TAC HAS_DERIVATIVE_SEQUENCE THEN
2085   EXISTS_TAC `\n x h:complex. (f':num->complex->complex) n x * h` THEN
2086   ASM_SIMP_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
2087   REWRITE_TAC[GSYM COMPLEX_SUB_RDISTRIB; COMPLEX_NORM_MUL] THEN
2088   ASM_MESON_TAC[REAL_LE_RMUL; NORM_POS_LE]);;
2089
2090 let HAS_COMPLEX_DERIVATIVE_SERIES = prove
2091  (`!s f f' g' k.
2092          convex s /\
2093          (!n x. x IN s
2094                 ==> (f n has_complex_derivative f' n x) (at x within s)) /\
2095          (!e. &0 < e
2096               ==> ?N. !n x. n >= N /\ x IN s
2097                             ==> norm(vsum (k INTER (0..n)) (\i. f' i x) - g' x)
2098                                     <= e) /\
2099          (?x l. x IN s /\ ((\n. f n x) sums l) k)
2100          ==> ?g. !x. x IN s
2101                      ==> ((\n. f n x) sums g x) k /\
2102                          (g has_complex_derivative g' x) (at x within s)`,
2103   REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
2104   MATCH_MP_TAC HAS_DERIVATIVE_SERIES THEN
2105   EXISTS_TAC `\n x h:complex. (f':num->complex->complex) n x * h` THEN
2106   ASM_SIMP_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
2107   SIMP_TAC[GSYM COMPLEX_SUB_RDISTRIB; VSUM_COMPLEX_RMUL; FINITE_NUMSEG;
2108            FINITE_INTER; COMPLEX_NORM_MUL] THEN
2109   ASM_MESON_TAC[REAL_LE_RMUL; NORM_POS_LE]);;
2110
2111 (* ------------------------------------------------------------------------- *)
2112 (* Bound theorem.                                                            *)
2113 (* ------------------------------------------------------------------------- *)
2114
2115 let COMPLEX_DIFFERENTIABLE_BOUND = prove
2116  (`!f f' s B.
2117         convex s /\
2118         (!x. x IN s ==> (f has_complex_derivative f'(x)) (at x within s) /\
2119                         norm(f' x) <= B)
2120         ==> !x y. x IN s /\ y IN s ==> norm(f x - f y) <= B * norm(x - y)`,
2121   REPEAT GEN_TAC THEN REWRITE_TAC[has_complex_derivative] THEN
2122   STRIP_TAC THEN MATCH_MP_TAC DIFFERENTIABLE_BOUND THEN
2123   EXISTS_TAC `\x:complex h. f' x * h` THEN ASM_SIMP_TAC[] THEN
2124   REPEAT STRIP_TAC THEN
2125   MP_TAC(ISPEC `\h. (f':complex->complex) x * h` ONORM) THEN
2126   REWRITE_TAC[LINEAR_COMPLEX_MUL] THEN
2127   DISCH_THEN(MATCH_MP_TAC o CONJUNCT2) THEN
2128   GEN_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN
2129   ASM_MESON_TAC[REAL_LE_RMUL; NORM_POS_LE]);;
2130
2131 (* ------------------------------------------------------------------------- *)
2132 (* Inverse function theorem for complex derivatives.                         *)
2133 (* ------------------------------------------------------------------------- *)
2134
2135 let HAS_COMPLEX_DERIVATIVE_INVERSE_BASIC = prove
2136  (`!f g f' t y.
2137         (f has_complex_derivative f') (at (g y)) /\
2138         ~(f' = Cx(&0)) /\
2139         g continuous at y /\
2140         open t /\
2141         y IN t /\
2142         (!z. z IN t ==> f (g z) = z)
2143         ==> (g has_complex_derivative inv(f')) (at y)`,
2144   REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
2145   MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_BASIC THEN
2146   MAP_EVERY EXISTS_TAC
2147    [`f:complex->complex`; `\x:complex. f' * x`; `t:complex->bool`] THEN
2148   ASM_REWRITE_TAC[LINEAR_COMPLEX_MUL; FUN_EQ_THM; o_THM; I_THM] THEN
2149   UNDISCH_TAC `~(f' = Cx(&0))` THEN CONV_TAC COMPLEX_FIELD);;
2150
2151 let HAS_COMPLEX_DERIVATIVE_INVERSE_STRONG = prove
2152  (`!f g f' s x.
2153          open s /\
2154          x IN s /\
2155          f continuous_on s /\
2156          (!x. x IN s ==> g (f x) = x) /\
2157          (f has_complex_derivative f') (at x) /\
2158          ~(f' = Cx(&0))
2159          ==> (g has_complex_derivative inv(f')) (at (f x))`,
2160   REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
2161   MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_STRONG THEN
2162   MAP_EVERY EXISTS_TAC [`\x:complex. f' * x`; `s:complex->bool`] THEN
2163   ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
2164   UNDISCH_TAC `~(f' = Cx(&0))` THEN CONV_TAC COMPLEX_FIELD);;
2165
2166 let HAS_COMPLEX_DERIVATIVE_INVERSE_STRONG_X = prove
2167  (`!f g f' s y.
2168         open s /\ (g y) IN s /\ f continuous_on s /\
2169         (!x. x IN s ==> (g(f(x)) = x)) /\
2170         (f has_complex_derivative f') (at (g y)) /\ ~(f' = Cx(&0)) /\
2171         f(g y) = y
2172         ==> (g has_complex_derivative inv(f')) (at y)`,
2173   REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
2174   MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_STRONG_X THEN MAP_EVERY EXISTS_TAC
2175    [`f:complex->complex`; `\x:complex. f' * x`; `s:complex->bool`] THEN
2176   ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
2177   UNDISCH_TAC `~(f' = Cx(&0))` THEN CONV_TAC COMPLEX_FIELD);;
2178
2179 (* ------------------------------------------------------------------------- *)
2180 (* Cauchy-Riemann condition and relation to conformal.                       *)
2181 (* ------------------------------------------------------------------------- *)
2182
2183 let COMPLEX_BASIS = prove
2184  (`basis 1 = Cx(&1) /\ basis 2 = ii`,
2185   SIMP_TAC[CART_EQ; FORALL_2; BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
2186   REWRITE_TAC[GSYM RE_DEF; GSYM IM_DEF; RE_CX; IM_CX] THEN
2187   REWRITE_TAC[ii] THEN SIMPLE_COMPLEX_ARITH_TAC);;
2188
2189 let CAUCHY_RIEMANN = prove
2190  (`!f z. f complex_differentiable at z <=>
2191          f differentiable at z  /\
2192          (jacobian f (at z))$1$1 = (jacobian f (at z))$2$2 /\
2193          (jacobian f (at z))$1$2 = --((jacobian f (at z))$2$1)`,
2194   REPEAT GEN_TAC THEN REWRITE_TAC[complex_differentiable] THEN EQ_TAC THENL
2195    [REWRITE_TAC[has_complex_derivative] THEN
2196     DISCH_THEN(X_CHOOSE_THEN `f':complex` ASSUME_TAC) THEN
2197     CONJ_TAC THENL [ASM_MESON_TAC[differentiable]; ALL_TAC] THEN
2198     REWRITE_TAC[jacobian] THEN
2199     FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP FRECHET_DERIVATIVE_AT) THEN
2200     SIMP_TAC[matrix; LAMBDA_BETA; DIMINDEX_2; ARITH] THEN
2201     REWRITE_TAC[COMPLEX_BASIS; GSYM RE_DEF; GSYM IM_DEF; ii] THEN
2202     SIMPLE_COMPLEX_ARITH_TAC;
2203     STRIP_TAC THEN EXISTS_TAC
2204      `complex(jacobian (f:complex->complex) (at z)$1$1,
2205               jacobian f (at z)$2$1)` THEN
2206     REWRITE_TAC[has_complex_derivative] THEN
2207     FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [JACOBIAN_WORKS]) THEN
2208     MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2209     ASM_SIMP_TAC[CART_EQ; matrix_vector_mul; DIMINDEX_2; SUM_2; ARITH;
2210                  FORALL_2; FUN_EQ_THM; LAMBDA_BETA] THEN
2211     REWRITE_TAC[GSYM RE_DEF; GSYM IM_DEF; IM; RE; complex_mul] THEN
2212     REAL_ARITH_TAC]);;
2213
2214 let COMPLEX_DERIVATIVE_JACOBIAN = prove
2215  (`!f z.
2216         f complex_differentiable (at z)
2217         ==> complex_derivative f z =
2218             complex(jacobian f (at z)$1$1,jacobian f (at z)$2$1)`,
2219   REPEAT STRIP_TAC THEN MATCH_MP_TAC COMPLEX_DERIVATIVE_UNIQUE_AT THEN
2220   MAP_EVERY EXISTS_TAC [`f:complex->complex`; `z:complex`] THEN
2221   ASM_REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE] THEN
2222   REWRITE_TAC[has_complex_derivative] THEN
2223   FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [CAUCHY_RIEMANN]) THEN
2224   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [JACOBIAN_WORKS]) THEN
2225   MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2226   ASM_SIMP_TAC[CART_EQ; matrix_vector_mul; DIMINDEX_2; SUM_2; ARITH;
2227                FORALL_2; FUN_EQ_THM; LAMBDA_BETA] THEN
2228   REWRITE_TAC[GSYM RE_DEF; GSYM IM_DEF; IM; RE; complex_mul] THEN
2229   REAL_ARITH_TAC);;
2230
2231 let COMPLEX_DIFFERENTIABLE_EQ_CONFORMAL = prove
2232  (`!f z.
2233       f complex_differentiable at z /\ ~(complex_derivative f z = Cx(&0)) <=>
2234       f differentiable at z  /\
2235       ?a. ~(a = &0) /\ rotation_matrix (a %% jacobian f (at z))`,
2236   REPEAT GEN_TAC THEN EQ_TAC THENL
2237    [DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2238     ASM_SIMP_TAC[COMPLEX_DIFFERENTIABLE_IMP_DIFFERENTIABLE;
2239                  COMPLEX_DERIVATIVE_JACOBIAN] THEN
2240     REWRITE_TAC[GSYM COMPLEX_VEC_0; GSYM DOT_EQ_0] THEN
2241     REWRITE_TAC[DOT_2; GSYM RE_DEF; GSYM IM_DEF; RE; IM; GSYM REAL_POW_2] THEN
2242     REWRITE_TAC[RE_DEF; IM_DEF; ROTATION_MATRIX_2] THEN
2243     RULE_ASSUM_TAC(REWRITE_RULE[CAUCHY_RIEMANN]) THEN
2244     ASM_REWRITE_TAC[MATRIX_CMUL_COMPONENT] THEN DISCH_TAC THEN
2245     REWRITE_TAC[REAL_MUL_RNEG; GSYM REAL_ADD_LDISTRIB;
2246                 REAL_ARITH `(a * x:real) pow 2 = a pow 2 * x pow 2`] THEN
2247     EXISTS_TAC
2248      `inv(sqrt(jacobian (f:complex->complex) (at z)$2$2 pow 2 +
2249                jacobian f (at z)$2$1 pow 2))` THEN
2250     MATCH_MP_TAC(REAL_FIELD
2251      `x pow 2 = y /\ ~(y = &0)
2252       ==> ~(inv x = &0) /\ inv(x) pow 2 * y = &1`) THEN
2253     ASM_SIMP_TAC[SQRT_POW_2; REAL_LE_ADD; REAL_LE_POW_2];
2254     REWRITE_TAC[ROTATION_MATRIX_2; MATRIX_CMUL_COMPONENT] THEN
2255     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
2256     DISCH_THEN(X_CHOOSE_THEN `a:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
2257     ASM_REWRITE_TAC[GSYM REAL_MUL_RNEG; REAL_EQ_MUL_LCANCEL] THEN
2258     STRIP_TAC THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
2259     CONJ_TAC THENL [ASM_REWRITE_TAC[CAUCHY_RIEMANN]; DISCH_TAC] THEN
2260     ASM_SIMP_TAC[COMPLEX_DERIVATIVE_JACOBIAN] THEN
2261     REWRITE_TAC[GSYM COMPLEX_VEC_0; GSYM DOT_EQ_0] THEN
2262     REWRITE_TAC[DOT_2; GSYM RE_DEF; GSYM IM_DEF; RE; IM; GSYM REAL_POW_2] THEN
2263     FIRST_X_ASSUM(MP_TAC o MATCH_MP
2264      (REAL_RING `(a * x) pow 2 + (a * y) pow 2 = &1
2265                  ==> ~(x pow 2 + y pow 2 = &0)`)) THEN
2266     ASM_REWRITE_TAC[RE_DEF; IM_DEF]]);;
2267
2268 (* ------------------------------------------------------------------------- *)
2269 (* Differentiation conversion.                                               *)
2270 (* ------------------------------------------------------------------------- *)
2271
2272 let complex_differentiation_theorems = ref [];;
2273
2274 let add_complex_differentiation_theorems =
2275   let ETA_THM = prove
2276    (`(f has_complex_derivative f') net <=>
2277      ((\x. f x) has_complex_derivative f') net`,
2278     REWRITE_TAC[ETA_AX]) in
2279   let ETA_TWEAK =
2280     PURE_REWRITE_RULE [IMP_CONJ] o
2281     GEN_REWRITE_RULE (LAND_CONV o ONCE_DEPTH_CONV) [ETA_THM] o
2282     SPEC_ALL in
2283   fun l -> complex_differentiation_theorems :=
2284               !complex_differentiation_theorems @ map ETA_TWEAK l;;
2285
2286 add_complex_differentiation_theorems
2287  [HAS_COMPLEX_DERIVATIVE_LMUL_WITHIN; HAS_COMPLEX_DERIVATIVE_LMUL_AT;
2288   HAS_COMPLEX_DERIVATIVE_RMUL_WITHIN; HAS_COMPLEX_DERIVATIVE_RMUL_AT;
2289   HAS_COMPLEX_DERIVATIVE_CDIV_WITHIN; HAS_COMPLEX_DERIVATIVE_CDIV_AT;
2290   HAS_COMPLEX_DERIVATIVE_ID;
2291   HAS_COMPLEX_DERIVATIVE_CONST;
2292   HAS_COMPLEX_DERIVATIVE_NEG;
2293   HAS_COMPLEX_DERIVATIVE_ADD;
2294   HAS_COMPLEX_DERIVATIVE_SUB;
2295   HAS_COMPLEX_DERIVATIVE_MUL_WITHIN; HAS_COMPLEX_DERIVATIVE_MUL_AT;
2296   HAS_COMPLEX_DERIVATIVE_DIV_WITHIN; HAS_COMPLEX_DERIVATIVE_DIV_AT;
2297   HAS_COMPLEX_DERIVATIVE_POW_WITHIN; HAS_COMPLEX_DERIVATIVE_POW_AT;
2298   HAS_COMPLEX_DERIVATIVE_INV_WITHIN; HAS_COMPLEX_DERIVATIVE_INV_AT];;
2299
2300 let GEN_COMPLEX_DIFF_CONV ths =
2301   let partfn tm = let l,r = dest_comb tm in mk_pair(lhand l,r)
2302   and is_deriv = can (term_match [] `(f has_complex_derivative f') net`)
2303   and ths' =
2304    unions(mapfilter (CONJUNCTS o REWRITE_RULE[FORALL_AND_THM] o
2305                      MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV) ths) in
2306   let rec COMPLEX_DIFF_CONV tm =
2307     try tryfind (fun th -> PART_MATCH partfn th (partfn tm))
2308                 (!complex_differentiation_theorems @ ths')
2309     with Failure _ ->
2310         let ith = tryfind (fun th ->
2311          PART_MATCH (partfn o repeat (snd o dest_imp)) th (partfn tm))
2312                     (!complex_differentiation_theorems @ ths') in
2313         COMPLEX_DIFF_ELIM ith
2314   and COMPLEX_DIFF_ELIM th =
2315     let tm = concl th in
2316     if not(is_imp tm) then th else
2317     let t = lhand tm in
2318     if not(is_deriv t) then UNDISCH th
2319     else COMPLEX_DIFF_ELIM (MATCH_MP th (COMPLEX_DIFF_CONV t)) in
2320   COMPLEX_DIFF_CONV;;
2321
2322 let COMPLEX_DIFF_CONV = GEN_COMPLEX_DIFF_CONV [];;
2323
2324 (* ------------------------------------------------------------------------- *)
2325 (* Hence a tactic.                                                           *)
2326 (* ------------------------------------------------------------------------- *)
2327
2328 let GEN_COMPLEX_DIFF_TAC ths =
2329   let pth = MESON[]
2330    `(f has_complex_derivative f') net
2331     ==> f' = g'
2332         ==> (f has_complex_derivative g') net` in
2333   W(fun (asl,w) -> let th = MATCH_MP pth (GEN_COMPLEX_DIFF_CONV ths w) in
2334        MATCH_MP_TAC(repeat (GEN_REWRITE_RULE I [IMP_IMP]) (DISCH_ALL th)));;
2335
2336 let COMPLEX_DIFF_TAC = GEN_COMPLEX_DIFF_TAC [];;
2337
2338 let COMPLEX_DIFFERENTIABLE_TAC =
2339   let DISCH_FIRST th = DISCH (hd(hyp th)) th in
2340   GEN_REWRITE_TAC I [complex_differentiable] THEN
2341   W(fun (asl,w) ->
2342         let th = COMPLEX_DIFF_CONV(snd(dest_exists w)) in
2343         let f' = rand(rator(concl th)) in
2344         EXISTS_TAC f' THEN
2345         (if hyp th = [] then MATCH_ACCEPT_TAC th else
2346          let th' = repeat (GEN_REWRITE_RULE I [IMP_IMP] o DISCH_FIRST)
2347                           (DISCH_FIRST th) in
2348          MATCH_MP_TAC th'));;
2349
2350 (* ------------------------------------------------------------------------- *)
2351 (* A kind of complex Taylor theorem.                                         *)
2352 (* ------------------------------------------------------------------------- *)
2353
2354 let COMPLEX_TAYLOR = prove
2355  (`!f n s B.
2356     convex s /\
2357     (!i x. x IN s /\ i <= n
2358            ==> ((f i) has_complex_derivative f (i + 1) x) (at x within s)) /\
2359     (!x. x IN s ==> norm(f (n + 1) x) <= B)
2360     ==> !w z. w IN s /\ z IN s
2361               ==> norm(f 0 z -
2362                        vsum (0..n) (\i. f i w * (z - w) pow i / Cx(&(FACT i))))
2363                   <= B * norm(z - w) pow (n + 1) / &(FACT n)`,
2364   let lemma = prove
2365    (`!f:num->real^N.
2366           vsum (0..n) f = f 0 - f (n + 1) + vsum (0..n) (\i. f (i + 1))`,
2367     REWRITE_TAC[GSYM(REWRITE_CONV[o_DEF] `(f:num->real^N) o (\i. i + 1)`)] THEN
2368     ASM_SIMP_TAC[GSYM VSUM_IMAGE; EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
2369     REWRITE_TAC[GSYM NUMSEG_OFFSET_IMAGE] THEN
2370     SIMP_TAC[VSUM_CLAUSES_LEFT; LE_0] THEN
2371     REWRITE_TAC[VSUM_CLAUSES_NUMSEG; GSYM ADD1] THEN
2372     REWRITE_TAC[ARITH; ARITH_RULE `1 <= SUC n`] THEN VECTOR_ARITH_TAC) in
2373   REPEAT STRIP_TAC THEN MP_TAC(SPECL
2374    [`(\w. vsum (0..n) (\i. f i w * (z - w) pow i / Cx(&(FACT i))))`;
2375     `\w. (f:num->complex->complex) (n + 1) w *
2376          (z - w) pow n / Cx(&(FACT n))`; `segment[w:complex,z]`;
2377     `B * norm(z - w:complex) pow n / &(FACT n)`]
2378    COMPLEX_DIFFERENTIABLE_BOUND) THEN
2379   ANTS_TAC THENL
2380    [ASM_REWRITE_TAC[CONVEX_SEGMENT] THEN X_GEN_TAC `u:complex` THEN
2381     DISCH_TAC THEN SUBGOAL_THEN `(u:complex) IN s` ASSUME_TAC THENL
2382      [ASM_MESON_TAC[CONVEX_CONTAINS_SEGMENT; SUBSET]; ALL_TAC] THEN
2383     CONJ_TAC THENL
2384      [ALL_TAC;
2385       REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_DIV; COMPLEX_NORM_CX;
2386                   COMPLEX_NORM_POW; REAL_ABS_NUM] THEN
2387       MATCH_MP_TAC REAL_LE_MUL2 THEN
2388       ASM_SIMP_TAC[REAL_LE_DIV; NORM_POS_LE; REAL_POS; REAL_POW_LE] THEN
2389       ASM_SIMP_TAC[REAL_LE_DIV2_EQ; REAL_OF_NUM_LT; FACT_LT] THEN
2390       MATCH_MP_TAC REAL_POW_LE2 THEN REWRITE_TAC[NORM_POS_LE] THEN
2391       ASM_MESON_TAC[SEGMENT_BOUND; NORM_SUB]] THEN
2392     MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_WITHIN_SUBSET THEN
2393     EXISTS_TAC `s:complex->bool` THEN CONJ_TAC THENL
2394      [ALL_TAC; ASM_MESON_TAC[CONVEX_CONTAINS_SEGMENT]] THEN
2395     SUBGOAL_THEN
2396      `((\u. vsum (0..n) (\i. f i u * (z - u) pow i / Cx (&(FACT i))))
2397        has_complex_derivative
2398        vsum (0..n) (\i. f i u * (-- Cx(&i) * (z - u) pow (i - 1)) /
2399                                 Cx(&(FACT i)) +
2400                         f (i + 1) u * (z - u) pow i / Cx (&(FACT i))))
2401       (at u within s)`
2402     MP_TAC THENL
2403      [MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_VSUM THEN
2404       REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
2405       MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_MUL_WITHIN THEN
2406       ASM_SIMP_TAC[ETA_AX] THEN W(MP_TAC o COMPLEX_DIFF_CONV o snd) THEN
2407       MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2408       REWRITE_TAC[complex_div] THEN CONV_TAC COMPLEX_RING;
2409       ALL_TAC] THEN
2410     ASM_SIMP_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
2411     AP_TERM_TAC THEN REWRITE_TAC[VSUM_ADD_NUMSEG] THEN
2412     GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [lemma] THEN
2413     REWRITE_TAC[GSYM VSUM_ADD_NUMSEG; GSYM COMPLEX_ADD_ASSOC] THEN
2414     REWRITE_TAC[ADD_SUB] THEN REWRITE_TAC[GSYM ADD1; FACT] THEN
2415     REWRITE_TAC[GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_MUL; CX_MUL] THEN
2416     REWRITE_TAC[complex_div; COMPLEX_INV_MUL; GSYM COMPLEX_MUL_ASSOC] THEN
2417     REWRITE_TAC[COMPLEX_RING
2418       `--a * b * inv a * c:complex = --(a * inv a) * b * c`] THEN
2419     SIMP_TAC[COMPLEX_MUL_RINV; CX_INJ; REAL_ARITH `~(&n + &1 = &0)`] THEN
2420     REWRITE_TAC[COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; COMPLEX_MUL_LID] THEN
2421     REWRITE_TAC[COMPLEX_ADD_LINV; GSYM COMPLEX_VEC_0; VSUM_0] THEN
2422     REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_ADD_RID] THEN
2423     REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO; COMPLEX_NEG_0] THEN
2424     CONV_TAC COMPLEX_RING;
2425     ALL_TAC] THEN
2426   DISCH_THEN(MP_TAC o SPECL [`z:complex`; `w:complex`]) THEN ANTS_TAC THEN
2427   ASM_REWRITE_TAC[ENDS_IN_SEGMENT] THEN MATCH_MP_TAC EQ_IMP THEN
2428   BINOP_TAC THENL
2429    [ALL_TAC;
2430     REWRITE_TAC[REAL_POW_ADD; real_div; REAL_POW_1] THEN REAL_ARITH_TAC] THEN
2431   AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2432   SIMP_TAC[VSUM_CLAUSES_LEFT; LE_0; complex_pow; FACT; COMPLEX_DIV_1] THEN
2433   REWRITE_TAC[SIMPLE_COMPLEX_ARITH `x * Cx(&1) + y = x <=> y = Cx(&0)`] THEN
2434   REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN MATCH_MP_TAC VSUM_EQ_0 THEN
2435   INDUCT_TAC THEN
2436   ASM_REWRITE_TAC[complex_pow; complex_div; COMPLEX_MUL_LZERO;
2437                   COMPLEX_MUL_RZERO; COMPLEX_SUB_REFL; COMPLEX_VEC_0] THEN
2438   REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);;
2439
2440 (* ------------------------------------------------------------------------- *)
2441 (* The simplest special case.                                                *)
2442 (* ------------------------------------------------------------------------- *)
2443
2444 let COMPLEX_MVT = prove
2445  (`!f f' s B.
2446         convex s /\
2447         (!z. z IN s ==> (f has_complex_derivative f' z) (at z within s)) /\
2448         (!z. z IN s ==> norm (f' z) <= B)
2449         ==> !w z. w IN s /\ z IN s ==> norm (f z - f w) <= B * norm (z - w)`,
2450   REPEAT STRIP_TAC THEN
2451   MP_TAC(SPECL [`(\n. if n = 0 then f else f'):num->complex->complex`;
2452                 `0`; `s:complex->bool`; `B:real`] COMPLEX_TAYLOR) THEN
2453   SIMP_TAC[NUMSEG_SING; VSUM_SING; LE; ARITH] THEN
2454   REWRITE_TAC[complex_pow; REAL_POW_1; FACT; REAL_DIV_1] THEN
2455   ASM_SIMP_TAC[COMPLEX_DIV_1; COMPLEX_MUL_RID]);;
2456
2457 (* ------------------------------------------------------------------------- *)
2458 (* Something more like the traditional MVT for real components.              *)
2459 (* Could, perhaps should, sharpen this to derivatives inside the segment.    *)
2460 (* ------------------------------------------------------------------------- *)
2461
2462 let COMPLEX_MVT_LINE = prove
2463  (`!f f' w z.
2464         (!u. u IN segment[w,z]
2465              ==> (f has_complex_derivative f'(u)) (at u))
2466         ==> ?u. u IN segment[w,z] /\ Re(f z) - Re(f w) = Re(f'(u) * (z - w))`,
2467   REPEAT STRIP_TAC THEN
2468   MP_TAC(ISPECL
2469    [`(lift o Re) o (f:complex->complex) o
2470      (\t. (&1 - drop t) % w + drop t % z)`;
2471     `\u. (lift o Re) o
2472          (\h. (f':complex->complex)((&1 - drop u) % w + drop u % z) * h) o
2473          (\t. drop t % (z - w))`;
2474     `vec 0:real^1`; `vec 1:real^1`]
2475         MVT_VERY_SIMPLE) THEN
2476   ANTS_TAC THENL
2477    [REWRITE_TAC[DROP_VEC; REAL_POS] THEN
2478     X_GEN_TAC `t:real^1` THEN STRIP_TAC THEN
2479     MATCH_MP_TAC HAS_DERIVATIVE_AT_WITHIN THEN
2480     MATCH_MP_TAC DIFF_CHAIN_AT THEN CONJ_TAC THENL
2481      [ALL_TAC;
2482       MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
2483       REWRITE_TAC[linear; LIFT_ADD; RE_ADD; LIFT_CMUL; RE_CMUL; o_DEF]] THEN
2484     MATCH_MP_TAC DIFF_CHAIN_AT THEN CONJ_TAC THENL
2485      [REWRITE_TAC[VECTOR_ARITH `(&1 - t) % w + t % z = w + t % (z - w)`] THEN
2486       GEN_REWRITE_TAC (RATOR_CONV o RAND_CONV o ABS_CONV)
2487         [GSYM VECTOR_ADD_LID] THEN
2488       MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN
2489       REWRITE_TAC[HAS_DERIVATIVE_CONST] THEN
2490       MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
2491       REWRITE_TAC[linear; DROP_ADD; DROP_CMUL] THEN
2492       CONJ_TAC THEN VECTOR_ARITH_TAC;
2493       ALL_TAC] THEN
2494     REWRITE_TAC[GSYM has_complex_derivative] THEN
2495     FIRST_X_ASSUM MATCH_MP_TAC;
2496     REWRITE_TAC[o_THM; GSYM LIFT_SUB; LIFT_EQ; DROP_VEC; VECTOR_SUB_RZERO] THEN
2497     CONV_TAC REAL_RAT_REDUCE_CONV THEN
2498     REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO] THEN
2499     REWRITE_TAC[VECTOR_ADD_LID; VECTOR_ADD_RID] THEN
2500     DISCH_THEN(X_CHOOSE_THEN `t:real^1` STRIP_ASSUME_TAC) THEN
2501     EXISTS_TAC `(&1 - drop t) % w + drop t % z:complex`] THEN
2502   ASM_REWRITE_TAC[segment; IN_ELIM_THM] THEN
2503   EXISTS_TAC `drop t` THEN ASM_REWRITE_TAC[] THEN
2504   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_INTERVAL_1]) THEN
2505   REWRITE_TAC[DROP_VEC]);;
2506
2507 let COMPLEX_TAYLOR_MVT = prove
2508  (`!f w z n.
2509     (!i x. x IN segment[w,z] /\ i <= n
2510            ==> ((f i) has_complex_derivative f (i + 1) x) (at x))
2511     ==> ?u. u IN segment[w,z] /\
2512             Re(f 0 z) =
2513             Re(vsum (0..n) (\i. f i w * (z - w) pow i / Cx(&(FACT i))) +
2514                (f (n + 1) u * (z - u) pow n / Cx (&(FACT n))) * (z - w))`,
2515   let lemma = prove
2516    (`!f:num->real^N.
2517           vsum (0..n) f = f 0 - f (n + 1) + vsum (0..n) (\i. f (i + 1))`,
2518     REWRITE_TAC[GSYM(REWRITE_CONV[o_DEF] `(f:num->real^N) o (\i. i + 1)`)] THEN
2519     ASM_SIMP_TAC[GSYM VSUM_IMAGE; EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
2520     REWRITE_TAC[GSYM NUMSEG_OFFSET_IMAGE] THEN
2521     SIMP_TAC[VSUM_CLAUSES_LEFT; LE_0] THEN
2522     REWRITE_TAC[VSUM_CLAUSES_NUMSEG; GSYM ADD1] THEN
2523     REWRITE_TAC[ARITH; ARITH_RULE `1 <= SUC n`] THEN VECTOR_ARITH_TAC) in
2524   REPEAT STRIP_TAC THEN MP_TAC(SPECL
2525    [`(\w. vsum (0..n) (\i. f i w * (z - w) pow i / Cx(&(FACT i))))`;
2526     `\w. (f:num->complex->complex) (n + 1) w *
2527          (z - w) pow n / Cx(&(FACT n))`;
2528     `w:complex`; `z:complex`]
2529     COMPLEX_MVT_LINE) THEN
2530   ANTS_TAC THENL
2531    [ASM_REWRITE_TAC[CONVEX_SEGMENT] THEN X_GEN_TAC `u:complex` THEN
2532     DISCH_TAC THEN
2533     SUBGOAL_THEN
2534      `((\u. vsum (0..n) (\i. f i u * (z - u) pow i / Cx (&(FACT i))))
2535        has_complex_derivative
2536        vsum (0..n) (\i. f i u * (-- Cx(&i) * (z - u) pow (i - 1)) /
2537                                 Cx(&(FACT i)) +
2538                         f (i + 1) u * (z - u) pow i / Cx (&(FACT i))))
2539       (at u)`
2540     MP_TAC THENL
2541      [MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_VSUM THEN
2542       REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
2543       MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_MUL_AT THEN
2544       ASM_SIMP_TAC[ETA_AX] THEN W(MP_TAC o COMPLEX_DIFF_CONV o snd) THEN
2545       MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2546       REWRITE_TAC[complex_div] THEN CONV_TAC COMPLEX_RING;
2547       ALL_TAC] THEN
2548     ASM_SIMP_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
2549     AP_TERM_TAC THEN REWRITE_TAC[VSUM_ADD_NUMSEG] THEN
2550     GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [lemma] THEN
2551     REWRITE_TAC[GSYM VSUM_ADD_NUMSEG; GSYM COMPLEX_ADD_ASSOC] THEN
2552     REWRITE_TAC[ADD_SUB] THEN REWRITE_TAC[GSYM ADD1; FACT] THEN
2553     REWRITE_TAC[GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_MUL; CX_MUL] THEN
2554     REWRITE_TAC[complex_div; COMPLEX_INV_MUL; GSYM COMPLEX_MUL_ASSOC] THEN
2555     REWRITE_TAC[COMPLEX_RING
2556       `--a * b * inv a * c:complex = --(a * inv a) * b * c`] THEN
2557     SIMP_TAC[COMPLEX_MUL_RINV; CX_INJ; REAL_ARITH `~(&n + &1 = &0)`] THEN
2558     REWRITE_TAC[COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; COMPLEX_MUL_LID] THEN
2559     REWRITE_TAC[COMPLEX_ADD_LINV; GSYM COMPLEX_VEC_0; VSUM_0] THEN
2560     REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_ADD_RID] THEN
2561     REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO; COMPLEX_NEG_0] THEN
2562     CONV_TAC COMPLEX_RING;
2563     ALL_TAC] THEN
2564   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:complex` THEN
2565   MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[RE_ADD] THEN
2566   REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_EQ_SUB_RADD] THEN
2567   DISCH_THEN(SUBST1_TAC o SYM) THEN
2568   SIMP_TAC[VSUM_CLAUSES_LEFT; LE_0; complex_pow; FACT; COMPLEX_DIV_1] THEN
2569   REWRITE_TAC[COMPLEX_MUL_RID; RE_ADD] THEN
2570   MATCH_MP_TAC(REAL_ARITH `Re x = &0 ==> y = y + Re x`) THEN
2571   SIMP_TAC[RE_VSUM; FINITE_NUMSEG] THEN
2572   MATCH_MP_TAC SUM_EQ_0_NUMSEG THEN
2573   INDUCT_TAC THEN REWRITE_TAC[ARITH] THEN
2574   REWRITE_TAC[COMPLEX_SUB_REFL; complex_pow; complex_div] THEN
2575   REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO; RE_CX]);;
2576
2577 (* ------------------------------------------------------------------------- *)
2578 (* Further useful properties of complex conjugation.                         *)
2579 (* ------------------------------------------------------------------------- *)
2580
2581 let LIM_CNJ = prove
2582  (`!net f l. ((\x. cnj(f x)) --> cnj l) net <=> (f --> l) net`,
2583   REWRITE_TAC[LIM; dist; GSYM CNJ_SUB; COMPLEX_NORM_CNJ]);;
2584
2585 let SUMS_CNJ = prove
2586  (`!net f l. ((\x. cnj(f x)) sums cnj l) net <=> (f sums l) net`,
2587   SIMP_TAC[sums; LIM_CNJ; GSYM CNJ_VSUM; FINITE_INTER_NUMSEG]);;
2588
2589 let CONTINUOUS_WITHIN_CNJ = prove
2590  (`!s z. cnj continuous (at z within s)`,
2591   SIMP_TAC[LINEAR_CONTINUOUS_WITHIN; LINEAR_CNJ]);;
2592
2593 let CONTINUOUS_AT_CNJ = prove
2594  (`!z. cnj continuous (at z)`,
2595   SIMP_TAC[LINEAR_CONTINUOUS_AT; LINEAR_CNJ]);;
2596
2597 let CONTINUOUS_ON_CNJ = prove
2598  (`!s. cnj continuous_on s`,
2599   SIMP_TAC[LINEAR_CONTINUOUS_ON; LINEAR_CNJ]);;
2600
2601 (* ------------------------------------------------------------------------- *)
2602 (* Some limit theorems about real part of real series etc.                   *)
2603 (* ------------------------------------------------------------------------- *)
2604
2605 let REAL_LIM = prove
2606  (`!net:(A)net f l.
2607         (f --> l) net /\ ~(trivial_limit net) /\
2608         (?b. (?a. netord net a b) /\ !a. netord net a b ==> real(f a))
2609         ==> real l`,
2610   REWRITE_TAC[IM_DEF; real] THEN REPEAT STRIP_TAC THEN
2611   MATCH_MP_TAC LIM_COMPONENT_EQ THEN
2612   REWRITE_TAC[eventually; DIMINDEX_2; ARITH] THEN ASM_MESON_TAC[]);;
2613
2614 let REAL_LIM_SEQUENTIALLY = prove
2615  (`!f l. (f --> l) sequentially /\ (?N. !n. n >= N ==> real(f n))
2616          ==> real l`,
2617   REPEAT STRIP_TAC THEN MATCH_MP_TAC(ISPEC `sequentially` REAL_LIM) THEN
2618   REWRITE_TAC[SEQUENTIALLY; TRIVIAL_LIMIT_SEQUENTIALLY] THEN
2619   ASM_MESON_TAC[GE_REFL]);;
2620
2621 let REAL_SERIES = prove
2622  (`!f l s. (f sums l) s /\ (!n. real(f n)) ==> real l`,
2623   REWRITE_TAC[sums] THEN REPEAT STRIP_TAC THEN
2624   MATCH_MP_TAC REAL_LIM_SEQUENTIALLY THEN
2625   EXISTS_TAC `\n. vsum(s INTER (0..n)) f :complex` THEN
2626   ASM_SIMP_TAC[REAL_VSUM; FINITE_INTER; FINITE_NUMSEG]);;
2627
2628 (* ------------------------------------------------------------------------- *)
2629 (* Often convenient to use comparison with real limit of complex type.       *)
2630 (* ------------------------------------------------------------------------- *)
2631
2632 let LIM_NULL_COMPARISON_COMPLEX = prove
2633  (`!net:(A)net f g.
2634         eventually (\x. norm(f x) <= norm(g x)) net /\
2635         (g --> Cx(&0)) net
2636         ==> (f --> Cx(&0)) net`,
2637   REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN REPEAT STRIP_TAC THEN
2638   MATCH_MP_TAC(ISPEC `net:(A)net` LIM_NULL_COMPARISON) THEN
2639   EXISTS_TAC `norm o (g:A->complex)` THEN
2640   ASM_REWRITE_TAC[o_THM; GSYM LIM_NULL_NORM]);;
2641
2642 let LIM_NULL_COMPARISON_COMPLEX_RE = prove
2643  (`!net:(A)net f g.
2644         eventually (\x. norm(f x) <= Re(g x)) net /\
2645         (g --> Cx(&0)) net
2646         ==> (f --> Cx(&0)) net`,
2647   REPEAT STRIP_TAC THEN
2648   MATCH_MP_TAC(ISPEC `net:(A)net` LIM_NULL_COMPARISON_COMPLEX) THEN
2649   EXISTS_TAC `g:A->complex` THEN ASM_REWRITE_TAC[] THEN
2650   FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP
2651    (REWRITE_RULE[IMP_CONJ_ALT] EVENTUALLY_MONO)) THEN
2652   REWRITE_TAC[] THEN
2653   MESON_TAC[COMPLEX_NORM_GE_RE_IM; REAL_ABS_LE; REAL_LE_TRANS]);;
2654
2655 let SERIES_COMPARISON_COMPLEX = prove
2656  (`!f:num->real^N g s.
2657         summable s g /\
2658         (!n. n IN s ==> real(g n) /\ &0 <= Re(g n)) /\
2659         (?N. !n. n >= N /\ n IN s ==> norm(f n) <= norm(g n))
2660         ==> summable s f`,
2661   REPEAT GEN_TAC THEN REWRITE_TAC[summable] THEN
2662   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
2663   MATCH_MP_TAC SERIES_COMPARISON THEN
2664   EXISTS_TAC `\n. norm((g:num->complex) n)` THEN ASM_REWRITE_TAC[] THEN
2665   FIRST_X_ASSUM(X_CHOOSE_THEN `l:complex` STRIP_ASSUME_TAC) THEN
2666   EXISTS_TAC `lift(Re l)` THEN MATCH_MP_TAC SUMS_EQ THEN
2667   EXISTS_TAC `\i:num. lift(Re(g i))` THEN
2668   ASM_SIMP_TAC[REAL_NORM_POS; o_DEF] THEN
2669   REWRITE_TAC[RE_DEF] THEN MATCH_MP_TAC SERIES_COMPONENT THEN
2670   ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;
2671
2672 let SERIES_COMPARISON_UNIFORM_COMPLEX = prove
2673  (`!f:A->num->real^N g P s.
2674         summable s g /\
2675         (!n. n IN s ==> real(g n) /\ &0 <= Re(g n)) /\
2676         (?N. !n x. N <= n /\ n IN s /\ P x ==> norm(f x n) <= norm(g n))
2677         ==> ?l. !e. &0 < e
2678                     ==> ?N. !n x. N <= n /\ P x
2679                                   ==> dist(vsum(s INTER (0..n)) (f x),l x) <
2680                                        e`,
2681   REPEAT GEN_TAC THEN REWRITE_TAC[summable] THEN
2682   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
2683   MATCH_MP_TAC SERIES_COMPARISON_UNIFORM THEN
2684   EXISTS_TAC `\n. norm((g:num->complex) n)` THEN ASM_REWRITE_TAC[] THEN
2685   FIRST_X_ASSUM(X_CHOOSE_THEN `l:complex` STRIP_ASSUME_TAC) THEN
2686   EXISTS_TAC `lift(Re l)` THEN MATCH_MP_TAC SUMS_EQ THEN
2687   EXISTS_TAC `\i:num. lift(Re(g i))` THEN
2688   ASM_SIMP_TAC[REAL_NORM_POS; o_DEF] THEN
2689   REWRITE_TAC[RE_DEF] THEN MATCH_MP_TAC SERIES_COMPONENT THEN
2690   ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;
2691
2692 let SUMMABLE_SUBSET_COMPLEX = prove
2693  (`!x s t. (!n. n IN s ==> real(x n) /\ &0 <= Re(x n)) /\
2694            summable s x /\ t SUBSET s
2695            ==> summable t x`,
2696   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUMMABLE_SUBSET THEN
2697   EXISTS_TAC `s:num->bool` THEN ASM_REWRITE_TAC[] THEN
2698   MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
2699   EXISTS_TAC `x:num->complex` THEN ASM_REWRITE_TAC[] THEN
2700   MESON_TAC[REAL_LE_REFL; NORM_0; NORM_POS_LE]);;
2701
2702 let SERIES_ABSCONV_IMP_CONV = prove
2703  (`!x:num->real^N k. summable k (\n. Cx(norm(x n))) ==> summable k x`,
2704   REPEAT STRIP_TAC THEN MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
2705   EXISTS_TAC `\n:num. Cx(norm(x n:real^N))` THEN
2706   ASM_REWRITE_TAC[REAL_CX; RE_CX; NORM_POS_LE; COMPLEX_NORM_CX] THEN
2707   REWRITE_TAC[REAL_ABS_NORM; REAL_LE_REFL]);;
2708
2709 (* ------------------------------------------------------------------------- *)
2710 (* Complex-valued geometric series.                                          *)
2711 (* ------------------------------------------------------------------------- *)
2712
2713 let SUMS_GP = prove
2714  (`!n z. norm(z) < &1
2715          ==> ((\k. z pow k) sums (z pow n / (Cx(&1) - z))) (from n)`,
2716   REPEAT STRIP_TAC THEN REWRITE_TAC[SERIES_FROM; VSUM_GP] THEN
2717   ASM_CASES_TAC `z = Cx(&1)` THENL
2718    [ASM_MESON_TAC[COMPLEX_NORM_NUM; REAL_LT_REFL]; ALL_TAC] THEN
2719   MATCH_MP_TAC LIM_TRANSFORM_EVENTUALLY THEN
2720   EXISTS_TAC `\m. (z pow n - z pow SUC m) / (Cx (&1) - z)` THEN CONJ_TAC THENL
2721    [ASM_REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN
2722     EXISTS_TAC `n:num` THEN SIMP_TAC[GSYM NOT_LE];
2723     MATCH_MP_TAC LIM_COMPLEX_DIV THEN
2724     ASM_REWRITE_TAC[COMPLEX_SUB_0; LIM_CONST] THEN
2725     GEN_REWRITE_TAC (RATOR_CONV o RAND_CONV) [GSYM COMPLEX_SUB_RZERO] THEN
2726     MATCH_MP_TAC LIM_SUB THEN REWRITE_TAC[LIM_CONST] THEN
2727     REWRITE_TAC[LIM_SEQUENTIALLY; GSYM COMPLEX_VEC_0] THEN
2728     REWRITE_TAC[NORM_ARITH `dist(x,vec 0) = norm x`] THEN
2729     X_GEN_TAC `e:real` THEN DISCH_TAC THEN
2730     MP_TAC(SPECL [`norm(z:complex)`; `e:real`] REAL_ARCH_POW_INV) THEN
2731     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN
2732     X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `m:num` THEN DISCH_TAC THEN
2733     FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
2734      `x < e ==> y <= x ==> y < e`)) THEN
2735     REWRITE_TAC[COMPLEX_NORM_POW] THEN MATCH_MP_TAC REAL_POW_MONO_INV THEN
2736     ASM_SIMP_TAC[NORM_POS_LE; REAL_LT_IMP_LE] THEN
2737     UNDISCH_TAC `n:num <= m` THEN ARITH_TAC]);;
2738
2739 let SUMMABLE_GP = prove
2740  (`!z k. norm(z) < &1 ==> summable k (\n. z pow n)`,
2741   REPEAT STRIP_TAC THEN
2742   MATCH_MP_TAC SUMMABLE_SUBSET THEN EXISTS_TAC `(:num)` THEN
2743   REWRITE_TAC[SUBSET_UNIV] THEN
2744   MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
2745   EXISTS_TAC `\n. Cx(norm(z:complex) pow n)` THEN
2746   REWRITE_TAC[REAL_CX; RE_CX; COMPLEX_NORM_CX] THEN
2747   SIMP_TAC[REAL_POW_LE; NORM_POS_LE] THEN CONJ_TAC THENL
2748    [REWRITE_TAC[summable; GSYM FROM_0; CX_POW] THEN
2749     EXISTS_TAC `Cx(norm z) pow 0 / (Cx(&1) - Cx(norm(z:complex)))` THEN
2750     MATCH_MP_TAC SUMS_GP THEN
2751     ASM_REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NORM];
2752     EXISTS_TAC `0` THEN REPEAT STRIP_TAC THEN
2753     COND_CASES_TAC THEN
2754     ASM_SIMP_TAC[REAL_ABS_POW; REAL_ABS_NORM; REAL_LE_REFL; NORM_POS_LE;
2755                  COMPLEX_NORM_POW; NORM_0; REAL_ABS_POS; REAL_POW_LE]]);;
2756
2757 (* ------------------------------------------------------------------------- *)
2758 (* Convergence of 1/n^k for n >= 2.                                          *)
2759 (* ------------------------------------------------------------------------- *)
2760
2761 let SUMMABLE_ZETA_INTEGER = prove
2762  (`!n m. 2 <= m ==> summable (from n) (\k. inv(Cx(&k) pow m))`,
2763   REPEAT STRIP_TAC THEN MATCH_MP_TAC SUMMABLE_FROM_ELSEWHERE THEN
2764   EXISTS_TAC `1` THEN
2765   REWRITE_TAC[summable; GSYM CX_INV; GSYM CX_POW] THEN
2766   MATCH_MP_TAC(MESON[] `(?x. P(Cx x)) ==> ?x. P x`) THEN
2767   REWRITE_TAC[SERIES_CX_LIFT] THEN
2768   REWRITE_TAC[sums; FROM_INTER_NUMSEG; LIM_SEQUENTIALLY; DIST_REAL] THEN
2769   REWRITE_TAC[EXISTS_LIFT; LIFT_DROP; GSYM drop] THEN
2770   MATCH_MP_TAC CONVERGENT_BOUNDED_MONOTONE THEN
2771   EXISTS_TAC `&2 pow m / (&1 - (&1 / &2) pow (m - 1))` THEN CONJ_TAC THENL
2772    [ALL_TAC;
2773     DISJ1_TAC THEN MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN
2774     DISCH_TAC THEN REWRITE_TAC[DROP_VSUM; o_DEF; LIFT_DROP] THEN
2775     MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN
2776     SIMP_TAC[REAL_LE_INV_EQ; REAL_POW_LE; REAL_POS] THEN
2777     REWRITE_TAC[FINITE_NUMSEG; SUBSET_NUMSEG] THEN ASM_ARITH_TAC] THEN
2778   X_GEN_TAC `n:num` THEN REWRITE_TAC[DROP_VSUM; o_DEF; LIFT_DROP] THEN
2779   SIMP_TAC[real_abs; SUM_POS_LE_NUMSEG; REAL_LE_INV_EQ;
2780            REAL_POW_LE; REAL_POS] THEN
2781   TRANS_TAC REAL_LE_TRANS `sum(1..2 EXP n) (\x. inv(&x pow m))` THEN
2782   CONJ_TAC THENL
2783    [MATCH_MP_TAC SUM_SUBSET_SIMPLE THEN
2784     SIMP_TAC[REAL_LE_INV_EQ; REAL_POW_LE; REAL_POS] THEN
2785     SIMP_TAC[FINITE_NUMSEG; SUBSET_NUMSEG; LE_REFL;
2786              LT_POW2_REFL; LT_IMP_LE];
2787     ALL_TAC] THEN
2788   TRANS_TAC REAL_LE_TRANS
2789    `sum(0..n) (\k. &2 pow m / &2 pow (k * (m - 1)))` THEN
2790   CONJ_TAC THENL
2791    [SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
2792     SIMP_TAC[EXP; SUM_SING_NUMSEG; REAL_POW_ONE; MULT_CLAUSES; real_pow] THEN
2793     REWRITE_TAC[REAL_DIV_1; REAL_INV_1; REAL_LE_POW2] THEN
2794     MP_TAC(ISPECL
2795      [`\k. inv(&k pow m)`; `1`; `2 EXP n`; `2 EXP n`]
2796         SUM_ADD_SPLIT) THEN
2797     ANTS_TAC THENL [ARITH_TAC; REWRITE_TAC[MULT_2]] THEN
2798     DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[SUM_CLAUSES_NUMSEG; LE_0] THEN
2799     MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
2800     TRANS_TAC REAL_LE_TRANS
2801      `sum (2 EXP n + 1..2 EXP n + 2 EXP n) (\k. inv(&2 pow n pow m))` THEN
2802     CONJ_TAC THENL
2803      [MATCH_MP_TAC SUM_LE_NUMSEG THEN REPEAT STRIP_TAC THEN
2804       REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
2805       ASM_SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH] THEN
2806       MATCH_MP_TAC REAL_POW_LE2 THEN
2807       REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LE; LE_0] THEN ASM_ARITH_TAC;
2808       REWRITE_TAC[SUM_CONST_NUMSEG; ARITH_RULE `((n + n) + 1) - (n + 1) = n`;
2809                   GSYM REAL_OF_NUM_POW; REAL_INV_POW; REAL_POW_2] THEN
2810       REWRITE_TAC[REAL_POW_POW; REAL_POW_INV] THEN
2811       REWRITE_TAC[GSYM real_div] THEN
2812       ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_POW2] THEN
2813       REWRITE_TAC[REAL_ARITH `a / b * c:real = (a * c) / b`] THEN
2814       ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LT_POW2] THEN
2815       REWRITE_TAC[GSYM(CONJUNCT2 real_pow); GSYM REAL_POW_ADD] THEN
2816       MATCH_MP_TAC REAL_POW_MONO THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
2817       UNDISCH_TAC `2 <= m` THEN SPEC_TAC(`m:num`,`m:num`) THEN
2818       INDUCT_TAC THEN REWRITE_TAC[ARITH; SUC_SUB1] THEN ARITH_TAC];
2819     ONCE_REWRITE_TAC[MULT_SYM] THEN
2820     REWRITE_TAC[GSYM REAL_POW_POW; real_div] THEN
2821     REWRITE_TAC[REAL_INV_POW; SUM_LMUL] THEN REWRITE_TAC[SUM_GP] THEN
2822     REWRITE_TAC[REAL_INV_EQ_1; REAL_POW_EQ_1; LT] THEN
2823     CONV_TAC REAL_RAT_REDUCE_CONV THEN
2824     ASM_SIMP_TAC[ARITH_RULE `2 <= m ==> ~(m - 1 = 0)`] THEN
2825     REWRITE_TAC[CONJUNCT1 real_pow] THEN
2826     MATCH_MP_TAC REAL_LE_LMUL THEN SIMP_TAC[REAL_POW_LE; REAL_POS] THEN
2827     REWRITE_TAC[REAL_ARITH `a / b <= inv b <=> a * inv b <= &1 * inv b`] THEN
2828     MATCH_MP_TAC REAL_LE_RMUL THEN
2829     REWRITE_TAC[REAL_ARITH `&1 - x <= &1 <=> &0 <= x`; REAL_LE_INV_EQ] THEN
2830     SIMP_TAC[REAL_POW_LE; REAL_LE_DIV; REAL_POS; REAL_SUB_LE] THEN
2831     MATCH_MP_TAC REAL_POW_1_LE THEN CONV_TAC REAL_RAT_REDUCE_CONV]);;
2832
2833 (* ------------------------------------------------------------------------- *)
2834 (* Complex version (the usual one) of Dirichlet convergence test.            *)
2835 (* ------------------------------------------------------------------------- *)
2836
2837 let SERIES_DIRICHLET_COMPLEX_GEN = prove
2838  (`!f g N k m p l.
2839         bounded {vsum (m..n) f | n IN (:num)} /\
2840         summable (from p) (\n. Cx(norm(g(n + 1) - g(n)))) /\
2841         ((\n. vsum(1..n) f * g(n + 1)) --> l) sequentially
2842         ==> summable (from k) (\n. f(n) * g(n))`,
2843   REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
2844   MATCH_MP_TAC SERIES_DIRICHLET_BILINEAR THEN
2845   MAP_EVERY EXISTS_TAC [`m:num`; `p:num`; `l:complex`] THEN
2846   ASM_REWRITE_TAC[BILINEAR_COMPLEX_MUL] THEN
2847   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN ASM_REWRITE_TAC[] THEN
2848   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [summable]) THEN
2849   REWRITE_TAC[summable; SERIES_CAUCHY] THEN
2850   SIMP_TAC[GSYM(REWRITE_RULE[o_DEF] LIFT_SUM); FINITE_NUMSEG; FINITE_INTER;
2851            VSUM_CX; NORM_LIFT; COMPLEX_NORM_CX]);;
2852
2853 let SERIES_DIRICHLET_COMPLEX = prove
2854  (`!f g N k m.
2855         bounded {vsum (m..n) f | n IN (:num)} /\
2856         (!n. real(g n)) /\
2857         (!n. N <= n ==> Re(g(n + 1)) <= Re(g n)) /\
2858         (g --> Cx(&0)) sequentially
2859         ==> summable (from k) (\n. f(n) * g(n))`,
2860   REPEAT STRIP_TAC THEN
2861   MP_TAC(ISPECL [`f:num->complex`; `\n:num. Re(g n)`; `N:num`; `k:num`;
2862                  `m:num`] SERIES_DIRICHLET) THEN
2863   ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
2864    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_SEQUENTIALLY]) THEN
2865     REWRITE_TAC[LIM_SEQUENTIALLY; o_THM; dist; VECTOR_SUB_RZERO] THEN
2866     REWRITE_TAC[COMPLEX_SUB_RZERO; NORM_LIFT] THEN
2867     MESON_TAC[COMPLEX_NORM_GE_RE_IM; REAL_LET_TRANS];
2868     MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
2869     REWRITE_TAC[COMPLEX_CMUL; FUN_EQ_THM] THEN
2870     ASM_MESON_TAC[REAL; COMPLEX_MUL_SYM]]);;
2871
2872 (* ------------------------------------------------------------------------- *)
2873 (* Versions with explicit bounds are sometimes useful.                       *)
2874 (* ------------------------------------------------------------------------- *)
2875
2876 let SERIES_DIRICHLET_COMPLEX_VERY_EXPLICIT = prove
2877  (`!f g B p.
2878         &0 < B /\ 1 <= p /\
2879         (!m n. p <= m ==> norm(vsum(m..n) f) <= B) /\
2880         (!n. p <= n ==> real(g n) /\ &0 <= Re(g n)) /\
2881         (!n. p <= n ==> Re(g(n + 1)) <= Re(g n))
2882         ==> !m n. p <= m
2883                   ==> norm(vsum(m..n) (\k. f k * g k)) <= &2 * B * norm(g m)`,
2884   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
2885   EXISTS_TAC
2886    `norm(vsum(m..n) (\k. (vsum(p..k) f - vsum(p..(k-1)) f) * g k))` THEN
2887   CONJ_TAC THENL
2888    [MATCH_MP_TAC REAL_EQ_IMP_LE THEN AP_TERM_TAC THEN
2889     MATCH_MP_TAC VSUM_EQ_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
2890     REWRITE_TAC[] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
2891     SUBGOAL_THEN `p:num <= k`
2892      (fun th -> SIMP_TAC[GSYM(MATCH_MP NUMSEG_RREC th)])
2893     THENL [ASM_ARITH_TAC; ALL_TAC] THEN
2894     SIMP_TAC[VSUM_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
2895     COND_CASES_TAC THENL [ASM_ARITH_TAC; VECTOR_ARITH_TAC];
2896     ALL_TAC] THEN
2897   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
2898   REWRITE_TAC[MATCH_MP BILINEAR_VSUM_PARTIAL_PRE BILINEAR_COMPLEX_MUL] THEN
2899   COND_CASES_TAC THEN
2900   ASM_SIMP_TAC[NORM_0; REAL_LE_MUL; REAL_POS; REAL_LT_IMP_LE; NORM_POS_LE] THEN
2901   MATCH_MP_TAC(NORM_ARITH
2902    `norm(c) <= e - norm(a) - norm(b) ==> norm(a - b - c) <= e`) THEN
2903   MATCH_MP_TAC REAL_LE_TRANS THEN
2904   EXISTS_TAC `sum (m..n) (\k. norm(g(k + 1) - g(k)) * B)` THEN CONJ_TAC THENL
2905    [MATCH_MP_TAC VSUM_NORM_LE THEN REWRITE_TAC[IN_NUMSEG; FINITE_NUMSEG] THEN
2906     X_GEN_TAC `k:num` THEN STRIP_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN
2907     MATCH_MP_TAC REAL_LE_MUL2 THEN
2908     ASM_SIMP_TAC[REAL_LE_REFL; LE_REFL; NORM_POS_LE];
2909     ALL_TAC] THEN
2910   MATCH_MP_TAC REAL_LE_TRANS THEN
2911   EXISTS_TAC `sum(m..n) (\k. Re(g(k)) - Re(g(k + 1))) * B` THEN CONJ_TAC THENL
2912    [ASM_SIMP_TAC[SUM_RMUL; REAL_LE_RMUL_EQ] THEN
2913     MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN
2914     X_GEN_TAC `i:num` THEN STRIP_TAC THEN
2915     SUBGOAL_THEN `p <= i /\ p <= i + 1` ASSUME_TAC THENL
2916      [ASM_ARITH_TAC; ALL_TAC] THEN
2917     ASM_SIMP_TAC[REAL_NORM; REAL_SUB; RE_SUB] THEN
2918     ASM_SIMP_TAC[REAL_ARITH `abs(x - y) = y - x <=> x <= y`];
2919     ALL_TAC] THEN
2920   ASM_REWRITE_TAC[SUM_DIFFS; COMPLEX_NORM_MUL] THEN
2921   MATCH_MP_TAC(REAL_ARITH
2922    `w * n1 <= w * B /\ z * n2 <= z * B /\ &0 <= B * (&2 * y - (x + w + z))
2923     ==> x * B <= &2 * B * y - w * n1 - z * n2`) THEN
2924   REPEAT(CONJ_TAC THENL
2925    [MATCH_MP_TAC REAL_LE_LMUL THEN
2926     ASM_SIMP_TAC[NORM_POS_LE; LE_REFL]; ALL_TAC]) THEN
2927   MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
2928   SUBGOAL_THEN
2929    `p <= m /\ p <= m + 1 /\ p <= n /\ p <= n + 1`
2930   STRIP_ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
2931   ASM_SIMP_TAC[REAL_NORM; real_abs] THEN REAL_ARITH_TAC);;
2932
2933 let SERIES_DIRICHLET_COMPLEX_EXPLICIT = prove
2934  (`!f g p q.
2935            1 <= p /\
2936            bounded {vsum (q..n) f | n IN (:num)} /\
2937            (!n. p <= n ==> real(g n) /\ &0 <= Re(g n)) /\
2938            (!n. p <= n ==> Re(g(n + 1)) <= Re(g n))
2939            ==> ?B. &0 < B /\
2940                    !m n. p <= m
2941                          ==> norm(vsum(m..n) (\k. f k * g k))
2942                                  <= B * norm(g m)`,
2943   REWRITE_TAC[FORALL_AND_THM] THEN REPEAT STRIP_TAC THEN
2944   FIRST_X_ASSUM(MP_TAC o MATCH_MP BOUNDED_PARTIAL_SUMS) THEN
2945   SIMP_TAC[BOUNDED_POS; IN_ELIM_THM; IN_UNIV; LEFT_IMP_EXISTS_THM] THEN
2946   REWRITE_TAC[MESON[] `(!x a b. x = f a b ==> p a b) <=> (!a b. p a b)`] THEN
2947   X_GEN_TAC `B:real` THEN STRIP_TAC THEN EXISTS_TAC `&2 * B` THEN
2948   ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
2949   MATCH_MP_TAC SERIES_DIRICHLET_COMPLEX_VERY_EXPLICIT THEN
2950   ASM_SIMP_TAC[]);;
2951
2952 (* ------------------------------------------------------------------------- *)
2953 (* Integrals and complex multiplication.                                     *)
2954 (* ------------------------------------------------------------------------- *)
2955
2956 let HAS_INTEGRAL_COMPLEX_LMUL = prove
2957  (`!f y i c. (f has_integral y) i ==> ((\x. c * f(x)) has_integral (c * y)) i`,
2958   REPEAT STRIP_TAC THEN MATCH_MP_TAC
2959    (REWRITE_RULE[o_DEF] HAS_INTEGRAL_LINEAR) THEN
2960   ASM_REWRITE_TAC[linear; COMPLEX_CMUL] THEN CONV_TAC COMPLEX_RING);;
2961
2962 let HAS_INTEGRAL_COMPLEX_RMUL = prove
2963  (`!f y i c. (f has_integral y) i ==> ((\x. f(x) * c) has_integral (y * c)) i`,
2964   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
2965   REWRITE_TAC[HAS_INTEGRAL_COMPLEX_LMUL]);;
2966
2967 let HAS_INTEGRAL_COMPLEX_0 = prove
2968  (`!s. ((\x. Cx(&0)) has_integral Cx(&0)) s`,
2969   REWRITE_TAC[GSYM COMPLEX_VEC_0; HAS_INTEGRAL_0]);;
2970
2971 let INTEGRABLE_COMPLEX_LMUL = prove
2972  (`!f:real^N->complex s c.
2973         f integrable_on s ==> (\x. c * f x) integrable_on s`,
2974   REWRITE_TAC[integrable_on] THEN MESON_TAC[HAS_INTEGRAL_COMPLEX_LMUL]);;
2975
2976 let INTEGRABLE_COMPLEX_RMUL = prove
2977  (`!f:real^N->complex s c.
2978         f integrable_on s ==> (\x. f x * c) integrable_on s`,
2979   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
2980   REWRITE_TAC[INTEGRABLE_COMPLEX_LMUL]);;
2981
2982 let INTEGRABLE_COMPLEX_0 = prove
2983  (`!s. (\x. Cx(&0)) integrable_on s`,
2984   REWRITE_TAC[integrable_on] THEN MESON_TAC[HAS_INTEGRAL_COMPLEX_0]);;
2985
2986 let INTEGRABLE_COMPLEX_LMUL_EQ = prove
2987  (`!f:real^N->complex s c.
2988         (\x. c * f x) integrable_on s <=> c = Cx(&0) \/ f integrable_on s`,
2989   REPEAT(STRIP_TAC ORELSE EQ_TAC) THEN
2990   ASM_SIMP_TAC[INTEGRABLE_COMPLEX_LMUL; COMPLEX_MUL_LZERO] THEN
2991   REWRITE_TAC[INTEGRABLE_COMPLEX_0] THEN
2992   ASM_CASES_TAC `c = Cx(&0)` THEN ASM_REWRITE_TAC[] THEN
2993   FIRST_X_ASSUM(MP_TAC o SPEC `inv c:complex` o
2994     MATCH_MP INTEGRABLE_COMPLEX_LMUL) THEN
2995   ASM_SIMP_TAC[COMPLEX_MUL_ASSOC; COMPLEX_MUL_LID; COMPLEX_MUL_LINV; ETA_AX]);;
2996
2997 let INTEGRABLE_COMPLEX_RMUL_EQ = prove
2998  (`!f:real^N->complex s c.
2999         (\x. f x * c) integrable_on s <=> c = Cx(&0) \/ f integrable_on s`,
3000   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
3001   REWRITE_TAC[INTEGRABLE_COMPLEX_LMUL_EQ]);;
3002
3003 let INTEGRAL_COMPLEX_LMUL = prove
3004  (`!f:real^N->complex s c.
3005         f integrable_on s ==> integral s (\x. c * f x) = c * integral s f`,
3006   REPEAT STRIP_TAC THEN MATCH_MP_TAC INTEGRAL_UNIQUE THEN
3007   MATCH_MP_TAC HAS_INTEGRAL_COMPLEX_LMUL THEN
3008   ASM_SIMP_TAC[INTEGRABLE_INTEGRAL]);;
3009
3010 let INTEGRAL_COMPLEX_RMUL = prove
3011  (`!f:real^N->complex s c.
3012         f integrable_on s ==> integral s (\x. f x * c) = integral s f * c`,
3013   ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
3014   REWRITE_TAC[INTEGRAL_COMPLEX_LMUL]);;
3015
3016 let REAL_COMPLEX_INTEGRAL = prove
3017  (`!f:real^N->complex s.
3018      f integrable_on s /\ (!x. x IN s ==> real(f x)) ==> real(integral s f)`,
3019   REWRITE_TAC[real; IM_DEF] THEN SIMP_TAC[INTEGRAL_COMPONENT] THEN
3020   REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM LIFT_EQ; LIFT_DROP; LIFT_NUM] THEN
3021   MATCH_MP_TAC INTEGRAL_EQ_0 THEN
3022   ASM_REWRITE_TAC[GSYM LIFT_NUM; LIFT_EQ]);;
3023
3024 (* ------------------------------------------------------------------------- *)
3025 (* Relations among convergence and absolute convergence for power series.    *)
3026 (* ------------------------------------------------------------------------- *)
3027
3028 let ABEL_LEMMA = prove
3029  (`!a M r r0.
3030         &0 <= r /\ r < r0 /\
3031         (!n. n IN k ==> norm(a n) * r0 pow n <= M)
3032         ==> summable k (\n. Cx(norm(a(n)) * r pow n))`,
3033   REPEAT STRIP_TAC THEN
3034   SUBGOAL_THEN `&0 < r0` ASSUME_TAC THENL
3035    [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
3036   ASM_CASES_TAC `k:num->bool = {}` THEN ASM_REWRITE_TAC[SUMMABLE_TRIVIAL] THEN
3037   SUBGOAL_THEN `&0 <= M` ASSUME_TAC THENL
3038    [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
3039     DISCH_THEN(X_CHOOSE_TAC `i:num`) THEN
3040     FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
3041     MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> x <= y ==> &0 <= y`) THEN
3042     MATCH_MP_TAC REAL_LE_MUL THEN
3043     ASM_SIMP_TAC[NORM_POS_LE; REAL_POW_LE; REAL_LT_IMP_LE];
3044     ALL_TAC] THEN
3045   MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
3046   EXISTS_TAC `\n. Cx(M * (r / r0) pow n)` THEN REPEAT CONJ_TAC THENL
3047    [REWRITE_TAC[CX_MUL; CX_POW] THEN MATCH_MP_TAC SUMMABLE_COMPLEX_LMUL THEN
3048     MATCH_MP_TAC SUMMABLE_GP THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN
3049     ASM_SIMP_TAC[REAL_ABS_DIV; real_abs; REAL_LT_IMP_LE] THEN
3050     ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_MUL_LID];
3051     REWRITE_TAC[REAL_CX; RE_CX] THEN
3052     REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
3053     ASM_SIMP_TAC[REAL_LE_DIV; REAL_POW_LE; REAL_LT_IMP_LE];
3054     EXISTS_TAC `0` THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN REPEAT STRIP_TAC THEN
3055     REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NORM; REAL_ABS_DIV] THEN
3056     ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE; REAL_POW_DIV] THEN
3057     REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN
3058     ASM_SIMP_TAC[GSYM real_div; REAL_LE_RDIV_EQ; REAL_POW_LT] THEN
3059     ONCE_REWRITE_TAC[REAL_ARITH `(a * b) * c:real = (a * c) * b`] THEN
3060     ASM_SIMP_TAC[REAL_LE_RMUL; REAL_POW_LE; REAL_LT_IMP_LE]]);;
3061
3062 let POWER_SERIES_CONV_IMP_ABSCONV = prove
3063  (`!a k w z.
3064         summable k (\n. a(n) * z pow n) /\ norm(w) < norm(z)
3065         ==> summable k (\n. Cx(norm(a(n) * w pow n)))`,
3066   REPEAT STRIP_TAC THEN
3067   REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN
3068   MATCH_MP_TAC ABEL_LEMMA THEN
3069   FIRST_ASSUM(MP_TAC o MATCH_MP SUMMABLE_IMP_BOUNDED) THEN
3070   REWRITE_TAC[BOUNDED_POS; FORALL_IN_IMAGE] THEN
3071   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `B:real` THEN STRIP_TAC THEN
3072   EXISTS_TAC `norm(z:complex)` THEN REWRITE_TAC[NORM_POS_LE] THEN
3073   ASM_REWRITE_TAC[GSYM COMPLEX_NORM_POW; GSYM COMPLEX_NORM_MUL]);;
3074
3075 let POWER_SERIES_CONV_IMP_ABSCONV_WEAK = prove
3076  (`!a k w z.
3077         summable k (\n. a(n) * z pow n) /\ norm(w) < norm(z)
3078         ==> summable k (\n. Cx(norm(a(n))) * w pow n)`,
3079   REPEAT STRIP_TAC THEN MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
3080   EXISTS_TAC `\n. Cx(norm(a(n) * w pow n))` THEN CONJ_TAC THENL
3081    [MATCH_MP_TAC POWER_SERIES_CONV_IMP_ABSCONV THEN
3082     EXISTS_TAC `z:complex` THEN ASM_REWRITE_TAC[];
3083     ALL_TAC] THEN
3084   REWRITE_TAC[REAL_CX; RE_CX; NORM_POS_LE] THEN
3085   REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_CX; REAL_ABS_NORM;
3086               REAL_ABS_MUL; REAL_LE_REFL]);;
3087
3088 (* ------------------------------------------------------------------------- *)
3089 (* Comparing sums and "integrals" via complex antiderivatives.               *)
3090 (* ------------------------------------------------------------------------- *)
3091
3092 let SUM_INTEGRAL_UBOUND_INCREASING = prove
3093  (`!f g m n.
3094       m <= n /\
3095       (!x. x IN segment[Cx(&m),Cx(&n + &1)]
3096            ==> (g has_complex_derivative f(x)) (at x)) /\
3097       (!x y. &m <= x /\ x <= y /\ y <= &n + &1 ==> Re(f(Cx x)) <= Re(f(Cx y)))
3098       ==> sum(m..n) (\k. Re(f(Cx(&k)))) <= Re(g(Cx(&n + &1)) - g(Cx(&m)))`,
3099   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
3100   EXISTS_TAC `--sum(m..n) (\k. Re(g(Cx(&k))) - Re(g(Cx(&(k + 1)))))` THEN
3101   CONJ_TAC THENL
3102    [ALL_TAC;
3103     ASM_REWRITE_TAC[SUM_DIFFS; RE_SUB; REAL_NEG_SUB; REAL_OF_NUM_ADD] THEN
3104     REWRITE_TAC[REAL_LE_REFL]] THEN
3105   REWRITE_TAC[GSYM SUM_NEG] THEN MATCH_MP_TAC SUM_LE_NUMSEG THEN
3106   REWRITE_TAC[REAL_NEG_SUB] THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
3107   MP_TAC(ISPECL [`g:complex->complex`; `f:complex->complex`;
3108                  `Cx(&r)`; `Cx(&r + &1)`] COMPLEX_MVT_LINE) THEN
3109   ANTS_TAC THENL
3110    [X_GEN_TAC `u:complex` THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
3111     UNDISCH_TAC `u IN segment[Cx(&r),Cx(&r + &1)]` THEN
3112     REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
3113     SPEC_TAC(`u:complex`,`u:complex`) THEN REWRITE_TAC[GSYM SUBSET] THEN
3114     MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
3115     REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY; GSYM SEGMENT_CONVEX_HULL] THEN
3116     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[IN_SEGMENT_CX] THEN
3117     REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE] THEN
3118     ASM_ARITH_TAC;
3119     REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN DISCH_THEN(X_CHOOSE_THEN `u:complex`
3120      (CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
3121     REWRITE_TAC[CX_ADD; COMPLEX_RING `y * ((x + Cx(&1)) - x) = y`] THEN
3122     SUBGOAL_THEN `?y. u = Cx y` (CHOOSE_THEN SUBST_ALL_TAC) THENL
3123      [ASM_MESON_TAC[REAL_SEGMENT; REAL_CX; REAL]; ALL_TAC] THEN
3124     FIRST_X_ASSUM MATCH_MP_TAC THEN
3125     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_SEGMENT_CX]) THEN
3126     REPEAT(FIRST_X_ASSUM
3127      (MP_TAC o GEN_REWRITE_RULE I [GSYM REAL_OF_NUM_LE])) THEN
3128     REAL_ARITH_TAC]);;
3129
3130 let SUM_INTEGRAL_UBOUND_DECREASING = prove
3131  (`!f g m n.
3132       m <= n /\
3133       (!x. x IN segment[Cx(&m - &1),Cx(&n)]
3134            ==> (g has_complex_derivative f(x)) (at x)) /\
3135       (!x y. &m - &1 <= x /\ x <= y /\ y <= &n ==> Re(f(Cx y)) <= Re(f(Cx x)))
3136       ==> sum(m..n) (\k. Re(f(Cx(&k)))) <= Re(g(Cx(&n)) - g(Cx(&m - &1)))`,
3137   REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
3138    `--sum(m..n) (\k. Re(g(Cx(&(k) - &1))) - Re(g(Cx(&(k+1) - &1))))` THEN
3139   CONJ_TAC THENL
3140    [ALL_TAC;
3141     ASM_REWRITE_TAC[SUM_DIFFS; REAL_NEG_SUB] THEN
3142     REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_SUB] THEN
3143     REWRITE_TAC[RE_SUB; REAL_ARITH `(x + &1) - &1 = x`; REAL_LE_REFL]] THEN
3144   REWRITE_TAC[GSYM SUM_NEG] THEN MATCH_MP_TAC SUM_LE_NUMSEG THEN
3145   REWRITE_TAC[REAL_NEG_SUB] THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
3146   REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ARITH `(x + &1) - &1 = x`] THEN
3147   MP_TAC(ISPECL [`g:complex->complex`; `f:complex->complex`;
3148                  `Cx(&r - &1)`; `Cx(&r)`] COMPLEX_MVT_LINE) THEN
3149   ANTS_TAC THENL
3150    [X_GEN_TAC `u:complex` THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
3151     UNDISCH_TAC `u IN segment[Cx(&r - &1),Cx(&r)]` THEN
3152     REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
3153     SPEC_TAC(`u:complex`,`u:complex`) THEN REWRITE_TAC[GSYM SUBSET] THEN
3154     MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
3155     REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY; GSYM SEGMENT_CONVEX_HULL] THEN
3156     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[IN_SEGMENT_CX] THEN
3157     REPEAT(POP_ASSUM MP_TAC) THEN
3158     REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN REAL_ARITH_TAC;
3159     REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN DISCH_THEN(X_CHOOSE_THEN `u:complex`
3160      (CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
3161     REWRITE_TAC[CX_SUB; COMPLEX_RING `y * (x - (x - Cx(&1))) = y`] THEN
3162     SUBGOAL_THEN `?y. u = Cx y` (CHOOSE_THEN SUBST_ALL_TAC) THENL
3163      [ASM_MESON_TAC[REAL_SEGMENT; REAL_CX; REAL]; ALL_TAC] THEN
3164     FIRST_X_ASSUM MATCH_MP_TAC THEN
3165     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_SEGMENT_CX]) THEN
3166     REPEAT(FIRST_X_ASSUM
3167      (MP_TAC o GEN_REWRITE_RULE I [GSYM REAL_OF_NUM_LE])) THEN
3168     REAL_ARITH_TAC]);;
3169
3170 let SUM_INTEGRAL_LBOUND_INCREASING = prove
3171  (`!f g m n.
3172       m <= n /\
3173       (!x. x IN segment[Cx(&m - &1),Cx(&n)]
3174            ==> (g has_complex_derivative f(x)) (at x)) /\
3175       (!x y. &m - &1 <= x /\ x <= y /\ y <= &n ==> Re(f(Cx x)) <= Re(f(Cx y)))
3176       ==> Re(g(Cx(&n)) - g(Cx(&m - &1))) <= sum(m..n) (\k. Re(f(Cx(&k))))`,
3177   REPEAT STRIP_TAC THEN
3178   MP_TAC(ISPECL [`\z. --((f:complex->complex) z)`;
3179                  `\z. --((g:complex->complex) z)`;
3180                  `m:num`; `n:num`] SUM_INTEGRAL_UBOUND_DECREASING) THEN
3181   REWRITE_TAC[RE_NEG; RE_SUB; SUM_NEG; REAL_LE_NEG2;
3182               REAL_ARITH `--x - --y:real = --(x - y)`] THEN
3183   ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_NEG]);;
3184
3185 let SUM_INTEGRAL_LBOUND_DECREASING = prove
3186  (`!f g m n.
3187       m <= n /\
3188       (!x. x IN segment[Cx(&m),Cx(&n + &1)]
3189            ==> (g has_complex_derivative f(x)) (at x)) /\
3190       (!x y. &m <= x /\ x <= y /\ y <= &n + &1 ==> Re(f(Cx y)) <= Re(f(Cx x)))
3191       ==> Re(g(Cx(&n + &1)) - g(Cx(&m))) <= sum(m..n) (\k. Re(f(Cx(&k))))`,
3192   REPEAT STRIP_TAC THEN
3193   MP_TAC(ISPECL [`\z. --((f:complex->complex) z)`;
3194                  `\z. --((g:complex->complex) z)`;
3195                  `m:num`; `n:num`] SUM_INTEGRAL_UBOUND_INCREASING) THEN
3196   REWRITE_TAC[RE_NEG; RE_SUB; SUM_NEG; REAL_LE_NEG2;
3197               REAL_ARITH `--x - --y:real = --(x - y)`] THEN
3198   ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_NEG]);;
3199
3200 let SUM_INTEGRAL_BOUNDS_INCREASING = prove
3201  (`!f g m n.
3202          m <= n /\
3203          (!x. x IN segment[Cx(&m - &1),Cx (&n + &1)]
3204               ==> (g has_complex_derivative f x) (at x)) /\
3205          (!x y.
3206               &m - &1 <= x /\ x <= y /\ y <= &n + &1
3207               ==> Re(f(Cx x)) <= Re(f(Cx y)))
3208          ==> Re(g(Cx(&n)) - g(Cx(&m - &1))) <= sum(m..n) (\k. Re(f(Cx(&k)))) /\
3209              sum (m..n) (\k. Re(f(Cx(&k)))) <= Re(g(Cx(&n + &1)) - g(Cx(&m)))`,
3210   REPEAT STRIP_TAC THENL
3211    [MATCH_MP_TAC SUM_INTEGRAL_LBOUND_INCREASING;
3212     MATCH_MP_TAC SUM_INTEGRAL_UBOUND_INCREASING] THEN
3213   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
3214   FIRST_X_ASSUM MATCH_MP_TAC THEN
3215   RULE_ASSUM_TAC(REWRITE_RULE[IN_SEGMENT_CX_GEN; GSYM REAL_OF_NUM_LE]) THEN
3216   REWRITE_TAC[IN_SEGMENT_CX_GEN] THEN ASM_REAL_ARITH_TAC);;
3217
3218 let SUM_INTEGRAL_BOUNDS_DECREASING = prove
3219  (`!f g m n.
3220       m <= n /\
3221       (!x. x IN segment[Cx(&m - &1),Cx(&n + &1)]
3222            ==> (g has_complex_derivative f(x)) (at x)) /\
3223       (!x y. &m - &1 <= x /\ x <= y /\ y <= &n + &1
3224              ==> Re(f(Cx y)) <= Re(f(Cx x)))
3225       ==> Re(g(Cx(&n + &1)) - g(Cx(&m))) <= sum(m..n) (\k. Re(f(Cx(&k)))) /\
3226           sum(m..n) (\k. Re(f(Cx(&k)))) <= Re(g(Cx(&n)) - g(Cx(&m - &1)))`,
3227   REPEAT STRIP_TAC THENL
3228    [MATCH_MP_TAC SUM_INTEGRAL_LBOUND_DECREASING;
3229     MATCH_MP_TAC SUM_INTEGRAL_UBOUND_DECREASING] THEN
3230   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
3231   FIRST_X_ASSUM MATCH_MP_TAC THEN
3232   RULE_ASSUM_TAC(REWRITE_RULE[IN_SEGMENT_CX_GEN; GSYM REAL_OF_NUM_LE]) THEN
3233   REWRITE_TAC[IN_SEGMENT_CX_GEN] THEN ASM_REAL_ARITH_TAC);;
3234
3235 (* ------------------------------------------------------------------------- *)
3236 (* Relating different kinds of complex limits.                               *)
3237 (* ------------------------------------------------------------------------- *)
3238
3239 let LIM_INFINITY_SEQUENTIALLY_COMPLEX = prove
3240  (`!f l. (f --> l) at_infinity ==> ((\n. f(Cx(&n))) --> l) sequentially`,
3241   REPEAT GEN_TAC THEN REWRITE_TAC[LIM_AT_INFINITY; LIM_SEQUENTIALLY] THEN
3242   DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
3243   FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
3244   DISCH_THEN(X_CHOOSE_TAC `B:real`) THEN
3245   MP_TAC(ISPEC `B:real` REAL_ARCH_SIMPLE) THEN
3246   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
3247   REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
3248   REWRITE_TAC[COMPLEX_NORM_CX] THEN
3249   REPEAT(POP_ASSUM MP_TAC) THEN
3250   REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN REAL_ARITH_TAC);;
3251
3252 let LIM_AT_INFINITY_COMPLEX_0 = prove
3253  (`!f l:real^N.
3254         (f --> l) at_infinity <=> ((f o inv) --> l) (at(Cx(&0)))`,
3255   REPEAT GEN_TAC THEN REWRITE_TAC[LIM_AT_LE; LIM_AT_INFINITY_POS; o_DEF] THEN
3256   REWRITE_TAC[GSYM DIST_NZ; real_ge] THEN
3257   REWRITE_TAC[dist; COMPLEX_SUB_RZERO] THEN EQ_TAC THEN DISCH_TAC THEN
3258   X_GEN_TAC `e:real` THEN DISCH_TAC THEN
3259   FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[real_ge] THEN
3260   DISCH_THEN(X_CHOOSE_THEN `b:real` STRIP_ASSUME_TAC) THEN
3261   EXISTS_TAC `inv(b:real)` THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ] THEN
3262   X_GEN_TAC `z:complex` THEN STRIP_TAC THENL
3263    [ALL_TAC; SUBST1_TAC(SYM(SPEC `z:complex` COMPLEX_INV_INV))] THEN
3264   FIRST_X_ASSUM MATCH_MP_TAC THENL
3265    [GEN_REWRITE_TAC LAND_CONV [GSYM REAL_INV_INV] THEN
3266     REWRITE_TAC[COMPLEX_NORM_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
3267     ASM_REWRITE_TAC[COMPLEX_NORM_NZ];
3268     ASM_REWRITE_TAC[COMPLEX_INV_EQ_0] THEN CONJ_TAC THENL
3269      [REWRITE_TAC[GSYM COMPLEX_NORM_NZ] THEN
3270       TRANS_TAC REAL_LTE_TRANS `inv(b:real)` THEN
3271       ASM_REWRITE_TAC[REAL_LT_INV_EQ];
3272       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_INV] THEN
3273       REWRITE_TAC[COMPLEX_NORM_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
3274       ASM_REWRITE_TAC[REAL_LT_INV_EQ]]]);;
3275
3276 let LIM_ZERO_INFINITY_COMPLEX = prove
3277  (`!f l:real^N.
3278      ((\x. f(Cx(&1) / x)) --> l) (at (Cx(&0))) ==> (f --> l) at_infinity`,
3279   REWRITE_TAC[LIM_AT_INFINITY_COMPLEX_0; o_DEF; complex_div] THEN
3280   REWRITE_TAC[COMPLEX_MUL_LID]);;
3281
3282 (* ------------------------------------------------------------------------- *)
3283 (* Transforming complex limits to real ones.                                 *)
3284 (* ------------------------------------------------------------------------- *)
3285
3286 let LIM_COMPLEX_REAL = prove
3287  (`!f g l m.
3288          eventually (\n. Re(g n) = f n) sequentially /\
3289          Re m = l /\
3290          (g --> m) sequentially
3291          ==> !e. &0 < e ==> ?N. !n. N <= n ==> abs(f n - l) < e`,
3292   REPEAT GEN_TAC THEN
3293   REWRITE_TAC[EVENTUALLY_SEQUENTIALLY; LIM_SEQUENTIALLY] THEN
3294   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `N1:num`)
3295    (CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC)) THEN
3296   X_GEN_TAC `e:real` THEN DISCH_TAC THEN
3297   FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[dist] THEN
3298   DISCH_THEN(X_CHOOSE_TAC `N0:num`) THEN EXISTS_TAC `N0 + N1:num` THEN
3299   X_GEN_TAC `n:num` THEN DISCH_THEN(STRIP_ASSUME_TAC o MATCH_MP (ARITH_RULE
3300    `N0 + N1:num <= n ==> N0 <= n /\ N1 <= n`)) THEN
3301   UNDISCH_THEN `!n. N0 <= n ==> norm ((g:num->complex) n - m) < e`
3302    (MP_TAC o SPEC `n:num`) THEN
3303   FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN ASM_REWRITE_TAC[] THEN
3304   DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[GSYM RE_SUB] THEN
3305   MATCH_MP_TAC(REAL_ARITH `x <= y ==> y < e ==> x < e`) THEN
3306   REWRITE_TAC[COMPLEX_NORM_GE_RE_IM]);;
3307
3308 let LIM_COMPLEX_REAL_0 = prove
3309  (`!f g. eventually (\n. Re(g n) = f n) sequentially /\
3310          (g --> Cx(&0)) sequentially
3311          ==> !e. &0 < e ==> ?N. !n. N <= n ==> abs(f n) < e`,
3312   MP_TAC LIM_COMPLEX_REAL THEN
3313   REPLICATE_TAC 2 (MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
3314   DISCH_THEN(MP_TAC o SPECL [`&0`; `Cx(&0)`]) THEN
3315   REWRITE_TAC[RE_CX; REAL_SUB_RZERO]);;
3316
3317 (* ------------------------------------------------------------------------- *)
3318 (* Uniform convergence of power series in a "Stolz angle".                   *)
3319 (* ------------------------------------------------------------------------- *)
3320
3321 let POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ_1 = prove
3322  (`!M a s e.
3323         summable s a /\ &0 < M /\ &0 < e
3324         ==> eventually
3325              (\n. !z. norm(Cx(&1) - z) <= M * (&1 - norm z)
3326                       ==> norm(vsum (s INTER (0..n)) (\i. a i * z pow i) -
3327                                infsum s (\i. a i * z pow i)) < e)
3328              sequentially`,
3329   let lemma = prove
3330    (`!M w z. &0 < M /\ norm(w - z) <= M * (norm w - norm z) /\ ~(z = w)
3331              ==> norm(z) < norm(w)`,
3332     REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN CONJ_TAC THENL
3333      [ASM_MESON_TAC[REAL_LE_MUL_EQ; REAL_SUB_LE; NORM_POS_LE; REAL_LE_TRANS];
3334       DISCH_THEN SUBST_ALL_TAC THEN
3335       ASM_MESON_TAC[REAL_SUB_REFL; REAL_MUL_RZERO;NORM_LE_0; VECTOR_SUB_EQ]])
3336   and lemma1 = prove
3337    (`!m n. m < n
3338            ==> vsum (m..n) (\i. a i * z pow i) =
3339                (Cx(&1) - z) * vsum(m..n-1) (\i. vsum (m..i) a * z pow i) +
3340                vsum(m..n) a * z pow n`,
3341     GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; SUC_SUB1] THEN
3342     SIMP_TAC[VSUM_CLAUSES_NUMSEG; LT; LT_IMP_LE] THEN STRIP_TAC THENL
3343      [ASM_REWRITE_TAC[VSUM_SING_NUMSEG; complex_pow] THEN CONV_TAC COMPLEX_RING;
3344       ASM_SIMP_TAC[] THEN UNDISCH_TAC `m:num < n` THEN
3345       POP_ASSUM(K ALL_TAC)] THEN
3346     SPEC_TAC(`n:num`,`n:num`) THEN
3347     INDUCT_TAC THEN REWRITE_TAC[CONJUNCT1 LT] THEN POP_ASSUM(K ALL_TAC) THEN
3348     SIMP_TAC[SUC_SUB1; VSUM_CLAUSES_NUMSEG; LT_IMP_LE] THEN
3349     ASM_REWRITE_TAC[VSUM_SING_NUMSEG; complex_pow] THEN
3350     CONV_TAC COMPLEX_RING) in
3351   SUBGOAL_THEN
3352    `!M a e.
3353         summable (:num) a /\ &0 < M /\ &0 < e
3354         ==> eventually
3355              (\n. !z. norm(Cx(&1) - z) <= M * (&1 - norm z)
3356                       ==> norm(vsum (0..n) (\i. a i * z pow i) -
3357                                infsum (:num) (\i. a i * z pow i)) < e)
3358              sequentially`
3359   ASSUME_TAC THENL
3360    [ALL_TAC;
3361     REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o ISPECL
3362      [`M:real`; `\i:num. if i IN s then a i else Cx(&0)`; `e:real`]) THEN
3363     REWRITE_TAC[COND_RAND; COND_RATOR; COMPLEX_MUL_LZERO] THEN
3364     ASM_REWRITE_TAC[GSYM COMPLEX_VEC_0; GSYM VSUM_RESTRICT_SET;
3365                     INFSUM_RESTRICT; SUMMABLE_RESTRICT] THEN
3366     REWRITE_TAC[SET_RULE `{i | i IN t /\ i IN s} = s INTER t`]] THEN
3367   REPEAT STRIP_TAC THEN
3368   ONCE_REWRITE_TAC[MESON[]
3369    `(!z. P z) <=> P (Cx(&1)) /\ (!z. ~(z = Cx(&1)) ==> P z)`] THEN
3370   REWRITE_TAC[EVENTUALLY_AND] THEN CONJ_TAC THENL
3371    [REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM; COMPLEX_SUB_REFL;
3372                 REAL_SUB_REFL; REAL_MUL_RZERO; REAL_LE_REFL] THEN
3373     UNDISCH_TAC `&0 < e` THEN SPEC_TAC(`e:real`,`e:real`) THEN
3374     REWRITE_TAC[GSYM tendsto; COMPLEX_POW_ONE; COMPLEX_MUL_RID; GSYM dist;
3375                 ETA_AX] THEN
3376     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM SUMS_INFSUM]) THEN
3377     REWRITE_TAC[sums; INTER_UNIV];
3378     ALL_TAC] THEN
3379   REWRITE_TAC[IMP_IMP; EVENTUALLY_SEQUENTIALLY] THEN
3380   REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM dist] THEN
3381   UNDISCH_TAC `&0 < e` THEN SPEC_TAC(`e:real`,`e:real`) THEN
3382   MATCH_MP_TAC UNIFORMLY_CAUCHY_IMP_UNIFORMLY_CONVERGENT THEN
3383   REWRITE_TAC[GSYM LIM_SEQUENTIALLY] THEN CONJ_TAC THENL
3384    [X_GEN_TAC `e:real` THEN DISCH_TAC THEN
3385     REWRITE_TAC[MESON[] `(!m n z. P m /\ P n /\ Q z ==> R m n z) <=>
3386                          (!z. Q z ==> !m n. P m /\ P n ==> R m n z)`] THEN
3387     FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM SUMS_INFSUM]) THEN
3388     REWRITE_TAC[sums] THEN
3389     DISCH_THEN(MP_TAC o MATCH_MP CONVERGENT_IMP_CAUCHY) THEN
3390     REWRITE_TAC[cauchy; GSYM dist] THEN
3391     DISCH_THEN(MP_TAC o SPEC `min (e / &2) (e / &2 / M)`) THEN
3392     ASM_SIMP_TAC[REAL_LT_MIN; REAL_LT_DIV; REAL_HALF; GE; INTER_UNIV] THEN
3393     REWRITE_TAC[GSYM REAL_LT_MIN] THEN
3394     ONCE_REWRITE_TAC[SEQUENCE_CAUCHY_WLOG] THEN
3395     SUBGOAL_THEN
3396      `!f:num->complex m n. m <= n
3397               ==> dist(vsum (0..m) f,vsum (0..n) f) = norm(vsum (m+1..n) f)`
3398      (fun th -> SIMP_TAC[th])
3399     THENL
3400      [REPEAT STRIP_TAC THEN
3401       MATCH_MP_TAC(NORM_ARITH `a + c = b ==> dist(a,b) = norm c`) THEN
3402       MATCH_MP_TAC VSUM_COMBINE_R THEN ASM_ARITH_TAC;
3403       ALL_TAC] THEN
3404     MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
3405     REWRITE_TAC[REAL_LT_MIN] THEN STRIP_TAC THEN
3406     X_GEN_TAC `z:complex` THEN REWRITE_TAC[dist] THEN STRIP_TAC THEN
3407     SUBGOAL_THEN `norm(z:complex) < &1` ASSUME_TAC THENL
3408      [UNDISCH_TAC `~(z = Cx(&1))` THEN
3409       ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
3410       REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ] THEN DISCH_TAC THEN
3411       FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (NORM_ARITH
3412        `norm(a - b) <= M ==> &0 <= --M ==> b = a`)) THEN
3413       REWRITE_TAC[GSYM REAL_MUL_RNEG; REAL_NEG_SUB] THEN
3414       MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC;
3415       ALL_TAC] THEN
3416     MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
3417     ASM_CASES_TAC `m + 1 < n` THENL
3418      [ASM_SIMP_TAC[lemma1] THEN
3419       MATCH_MP_TAC(NORM_ARITH
3420        `norm(a) < e / &2 /\ norm(b) < e / &2 ==> norm(a + b) < e`) THEN
3421       REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN CONJ_TAC THENL
3422        [MATCH_MP_TAC REAL_LET_TRANS THEN
3423         EXISTS_TAC `(M * (&1 - norm(z:complex))) *
3424                     sum (m+1..n-1) (\i. e / &2 / M * norm(z) pow i)` THEN
3425         CONJ_TAC THENL
3426          [MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN
3427           MATCH_MP_TAC VSUM_NORM_LE THEN
3428           REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
3429           X_GEN_TAC `p:num` THEN STRIP_TAC THEN
3430           ASM_SIMP_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN
3431           MATCH_MP_TAC REAL_LE_RMUL THEN
3432           SIMP_TAC[REAL_POW_LE; NORM_POS_LE] THEN
3433           MATCH_MP_TAC(REAL_ARITH
3434             `x < e / &2 /\ x < e / &2 / M ==> x <= e / &2 / M`) THEN
3435           FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
3436           REWRITE_TAC[SUM_LMUL] THEN
3437           REWRITE_TAC[REAL_ARITH
3438            `(M * z1) * e / &2 / M * s < e / &2 <=>
3439             e * (M / M) * s * z1 < e * &1`] THEN
3440           ASM_SIMP_TAC[REAL_LT_LMUL_EQ] THEN
3441           ASM_SIMP_TAC[REAL_DIV_REFL; REAL_LT_IMP_NZ; REAL_MUL_LID] THEN
3442           ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_SUB_LT] THEN
3443           REWRITE_TAC[SUM_GP] THEN
3444           COND_CASES_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
3445           COND_CASES_TAC THENL
3446            [UNDISCH_TAC `norm(Cx(&1) - z) <= M * (&1 - norm z)` THEN
3447             ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO] THEN
3448             ASM_REWRITE_TAC[NORM_ARITH `norm(x - y:complex) <= &0 <=> x = y`];
3449             ALL_TAC] THEN
3450           ASM_SIMP_TAC[REAL_LT_DIV2_EQ; REAL_SUB_LT] THEN
3451           MATCH_MP_TAC(REAL_ARITH
3452            `&0 <= y /\ x < &1 ==> x - y < &1`) THEN
3453           ASM_SIMP_TAC[REAL_POW_LE; NORM_POS_LE] THEN
3454           MATCH_MP_TAC REAL_POW_1_LT THEN
3455           ASM_REWRITE_TAC[NORM_POS_LE] THEN ARITH_TAC];
3456         GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
3457         MATCH_MP_TAC REAL_LT_MUL2 THEN SIMP_TAC[NORM_POS_LE; REAL_POW_LE] THEN
3458         CONJ_TAC THENL
3459          [MATCH_MP_TAC(REAL_ARITH
3460             `x < e / &2 /\ x < e / &2 / M ==> x < e / &2`) THEN
3461           FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
3462           MATCH_MP_TAC REAL_POW_1_LT THEN
3463           ASM_REWRITE_TAC[NORM_POS_LE] THEN ASM_ARITH_TAC]];
3464       ASM_CASES_TAC `(m+1)..n = {}` THENL
3465        [ASM_REWRITE_TAC[VSUM_CLAUSES; NORM_0]; ALL_TAC] THEN
3466       RULE_ASSUM_TAC(REWRITE_RULE[NUMSEG_EMPTY]) THEN
3467       SUBGOAL_THEN `m + 1 = n` SUBST1_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
3468       REWRITE_TAC[VSUM_SING_NUMSEG] THEN
3469       REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN
3470       GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
3471       MATCH_MP_TAC REAL_LT_MUL2 THEN SIMP_TAC[NORM_POS_LE; REAL_POW_LE] THEN
3472       CONJ_TAC THENL
3473        [FIRST_X_ASSUM(MP_TAC o SPECL [`m:num`; `n:num`]) THEN
3474         SUBGOAL_THEN `m + 1 = n` SUBST1_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
3475         ANTS_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[VSUM_SING_NUMSEG]] THEN
3476         ASM_REAL_ARITH_TAC;
3477         MATCH_MP_TAC REAL_POW_1_LT THEN
3478         ASM_REWRITE_TAC[NORM_POS_LE] THEN ASM_ARITH_TAC]];
3479     X_GEN_TAC `z:complex` THEN REWRITE_TAC[dist] THEN STRIP_TAC THEN
3480     MP_TAC(ISPECL [`M:real`; `Cx(&1)`; `z:complex`] lemma) THEN
3481     ASM_REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM] THEN DISCH_TAC THEN
3482     SUBGOAL_THEN `summable (:num) (\i. a i * z pow i)` MP_TAC THENL
3483      [MATCH_MP_TAC SERIES_ABSCONV_IMP_CONV THEN
3484       REWRITE_TAC[] THEN MATCH_MP_TAC POWER_SERIES_CONV_IMP_ABSCONV THEN
3485       EXISTS_TAC `Cx(&1)` THEN
3486       REWRITE_TAC[COMPLEX_POW_ONE; COMPLEX_NORM_CX] THEN
3487       ASM_REWRITE_TAC[REAL_ABS_NUM; COMPLEX_MUL_RID; ETA_AX];
3488       REWRITE_TAC[GSYM SUMS_INFSUM] THEN
3489       REWRITE_TAC[sums; INTER_UNIV]]]);;
3490
3491 let POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ = prove
3492  (`!M a w s e.
3493         summable s (\i. a i * w pow i) /\ &0 < M /\ &0 < e
3494         ==> eventually
3495              (\n. !z. norm(w - z) <= M * (norm w - norm z)
3496                       ==> norm(vsum (s INTER (0..n)) (\i. a i * z pow i) -
3497                                infsum s (\i. a i * z pow i)) < e)
3498              sequentially`,
3499   REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `w = Cx(&0)` THENL
3500    [ASM_REWRITE_TAC[COMPLEX_SUB_LZERO; REAL_SUB_LZERO; COMPLEX_NORM_0] THEN
3501     REWRITE_TAC[NORM_NEG; REAL_ARITH
3502       `n <= M * --n <=> &0 <= --n * (&1 + M)`] THEN
3503     ASM_SIMP_TAC[REAL_LE_MUL_EQ; REAL_ARITH `&0 < M ==> &0 < &1 + M`] THEN
3504     REWRITE_TAC[NORM_ARITH `&0 <= --norm z <=> z = vec 0`] THEN
3505     REWRITE_TAC[EVENTUALLY_SEQUENTIALLY; FORALL_UNWIND_THM2] THEN
3506     EXISTS_TAC `1` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
3507     REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_POW_ZERO] THEN
3508     REWRITE_TAC[COND_RATOR; COND_RAND; COMPLEX_MUL_RZERO; COMPLEX_MUL_RID] THEN
3509     MATCH_MP_TAC(NORM_ARITH `x = y /\ &0 < e ==> norm(y - x) < e`) THEN
3510     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INFSUM_UNIQUE THEN
3511     REWRITE_TAC[sums] THEN MATCH_MP_TAC LIM_EVENTUALLY THEN
3512     REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN EXISTS_TAC `1` THEN
3513     X_GEN_TAC `m:num` THEN DISCH_TAC THEN
3514     SIMP_TAC[GSYM COMPLEX_VEC_0; VSUM_DELTA] THEN
3515     REWRITE_TAC[IN_INTER; LE_0; IN_NUMSEG];
3516     FIRST_ASSUM(MP_TAC o MATCH_MP POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ_1) THEN
3517     MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
3518     X_GEN_TAC `n:num` THEN REWRITE_TAC[] THEN DISCH_TAC THEN
3519     X_GEN_TAC `z:complex` THEN STRIP_TAC THEN
3520     FIRST_X_ASSUM(MP_TAC o SPEC `z / w:complex`) THEN
3521     ASM_SIMP_TAC[GSYM COMPLEX_MUL_ASSOC; GSYM COMPLEX_POW_MUL] THEN
3522     ASM_SIMP_TAC[COMPLEX_DIV_LMUL] THEN DISCH_THEN MATCH_MP_TAC THEN
3523     MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `norm(w:complex)` THEN
3524     ASM_REWRITE_TAC[COMPLEX_NORM_NZ; GSYM COMPLEX_NORM_MUL] THEN
3525     ASM_SIMP_TAC[COMPLEX_FIELD
3526      `~(w = Cx(&0)) ==> (Cx(&1) - z / w) * w = w - z`] THEN
3527     REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_SUB_RDISTRIB] THEN
3528     REWRITE_TAC[GSYM COMPLEX_NORM_MUL; REAL_MUL_LID] THEN
3529     ASM_SIMP_TAC[COMPLEX_DIV_RMUL]]);;
3530
3531 (* ------------------------------------------------------------------------- *)
3532 (* Hence continuity and the Abel limit theorem.                              *)
3533 (* ------------------------------------------------------------------------- *)
3534
3535 let ABEL_POWER_SERIES_CONTINUOUS = prove
3536  (`!M s a.
3537         summable s a /\ &0 < M
3538         ==> (\z. infsum s (\i. a i * z pow i)) continuous_on
3539             {z | norm(Cx(&1) - z) <= M * (&1 - norm z)}`,
3540   REPEAT STRIP_TAC THEN
3541   MATCH_MP_TAC(ISPEC `sequentially` CONTINUOUS_UNIFORM_LIMIT) THEN
3542   EXISTS_TAC `\n z. vsum (s INTER (0..n)) (\i. a i * z pow i)` THEN
3543   ASM_SIMP_TAC[POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ_1; IN_ELIM_THM;
3544                TRIVIAL_LIMIT_SEQUENTIALLY] THEN
3545   MATCH_MP_TAC ALWAYS_EVENTUALLY THEN X_GEN_TAC `n:num` THEN
3546   REWRITE_TAC[] THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM THEN
3547   SIMP_TAC[CONTINUOUS_ON_COMPLEX_MUL; CONTINUOUS_ON_COMPLEX_POW;
3548            CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST; FINITE_INTER;
3549            FINITE_NUMSEG]);;
3550
3551 let ABEL_LIMIT_THEOREM = prove
3552  (`!M s a.
3553         summable s a /\ &0 < M
3554         ==> (!z. norm(z) < &1 ==> summable s (\i. a i * z pow i)) /\
3555             ((\z. infsum s (\i. a i * z pow i)) --> infsum s a)
3556             (at (Cx(&1)) within {z | norm(Cx(&1) - z) <= M * (&1 - norm z)})`,
3557   GEN_TAC THEN ASM_CASES_TAC `&0 < M` THEN ASM_REWRITE_TAC[] THEN
3558   SUBGOAL_THEN
3559    `!a. summable (:num) a
3560         ==> (!z. norm(z) < &1 ==> summable (:num) (\i. a i * z pow i)) /\
3561             ((\z. infsum (:num) (\i. a i * z pow i))
3562               --> infsum (:num) a)
3563             (at (Cx(&1)) within {z | norm(Cx(&1) - z) <= M * (&1 - norm z)})`
3564   ASSUME_TAC THENL
3565    [ALL_TAC;
3566     REPEAT GEN_TAC THEN STRIP_TAC THEN
3567     FIRST_X_ASSUM(MP_TAC o SPEC
3568      `(\n. if n IN s then a n else vec 0):num->complex`) THEN
3569     REWRITE_TAC[COND_RAND; COND_RATOR; COMPLEX_VEC_0; COMPLEX_MUL_LZERO] THEN
3570     REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN
3571     ASM_REWRITE_TAC[SUMMABLE_RESTRICT; INFSUM_RESTRICT]] THEN
3572   GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
3573    [X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
3574     MATCH_MP_TAC SERIES_ABSCONV_IMP_CONV THEN
3575     REWRITE_TAC[] THEN MATCH_MP_TAC POWER_SERIES_CONV_IMP_ABSCONV THEN
3576     EXISTS_TAC `Cx(&1)` THEN REWRITE_TAC[COMPLEX_POW_ONE; COMPLEX_NORM_CX] THEN
3577     ASM_REWRITE_TAC[REAL_ABS_NUM; COMPLEX_MUL_RID; ETA_AX];
3578     MP_TAC(ISPECL [`M:real`; `(:num)`; `a:num->complex`]
3579        ABEL_POWER_SERIES_CONTINUOUS) THEN
3580     ASM_REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
3581     DISCH_THEN(MP_TAC o SPEC `Cx(&1)`) THEN
3582     REWRITE_TAC[IN_ELIM_THM; CONTINUOUS_WITHIN] THEN
3583     REWRITE_TAC[COMPLEX_SUB_REFL; COMPLEX_NORM_CX; COMPLEX_POW_ONE;
3584                 COMPLEX_MUL_RID; ETA_AX; REAL_ABS_NUM; REAL_SUB_REFL;
3585                 REAL_LE_REFL; REAL_MUL_RZERO]]);;
3586
3587 (* ------------------------------------------------------------------------- *)
3588 (* Continuity and uniqueness of power series. These would drop easily out    *)
3589 (* of later developments, but it seems nice to prove them without all the    *)
3590 (* machinery of Cauchy's theorem etc.                                        *)
3591 (* ------------------------------------------------------------------------- *)
3592
3593 let POWER_SERIES_CONTINUOUS = prove
3594  (`!a k f z r.
3595         (!w. w IN ball(z,r) ==> ((\n. a n * (w - z) pow n) sums f w) k)
3596         ==> f continuous_on ball(z,r)`,
3597   REWRITE_TAC[IN_BALL] THEN REPEAT STRIP_TAC THEN
3598   SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_AT; OPEN_BALL] THEN
3599   X_GEN_TAC `w:complex` THEN REWRITE_TAC[IN_BALL] THEN DISCH_TAC THEN
3600   ABBREV_TAC `R = (r + dist(z,w:complex)) / &2` THEN
3601   MATCH_MP_TAC CONTINUOUS_ON_INTERIOR THEN
3602   EXISTS_TAC `cball(z:complex,R)` THEN
3603   REWRITE_TAC[INTERIOR_CBALL; IN_BALL] THEN CONJ_TAC THENL
3604    [ALL_TAC;
3605     EXPAND_TAC "R" THEN UNDISCH_TAC `dist(z:complex,w) < r` THEN
3606     CONV_TAC NORM_ARITH] THEN
3607   MATCH_MP_TAC(ISPEC `sequentially` CONTINUOUS_UNIFORM_LIMIT) THEN
3608   EXISTS_TAC
3609    `\n w. vsum(k INTER (0..n)) (\i. (a:num->complex) i * (w - z) pow i)` THEN
3610   REWRITE_TAC[TRIVIAL_LIMIT_SEQUENTIALLY] THEN CONJ_TAC THENL
3611    [REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN EXISTS_TAC `1` THEN
3612     REPEAT STRIP_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM THEN
3613     SIMP_TAC[FINITE_INTER; FINITE_NUMSEG; IN_INTER; IN_NUMSEG] THEN
3614     X_GEN_TAC `i:num` THEN STRIP_TAC THEN
3615     MATCH_MP_TAC CONTINUOUS_ON_COMPLEX_LMUL THEN
3616     MATCH_MP_TAC CONTINUOUS_ON_COMPLEX_POW THEN
3617     MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
3618     REWRITE_TAC[CONTINUOUS_ON_CONST; CONTINUOUS_ON_ID];
3619     ALL_TAC] THEN
3620   MP_TAC(ISPECL
3621    [`\w n. (a:num->complex) n * (w - z) pow n`;
3622     `\n. Cx (norm (a n * Cx R pow n))`;
3623     `\x:complex. x IN cball(z,R)`;
3624     `k:num->bool`] SERIES_COMPARISON_UNIFORM_COMPLEX) THEN
3625   REWRITE_TAC[EVENTUALLY_SEQUENTIALLY; dist] THEN ANTS_TAC THENL
3626    [REWRITE_TAC[RE_CX; NORM_POS_LE; REAL_CX] THEN CONJ_TAC THENL
3627      [MATCH_MP_TAC POWER_SERIES_CONV_IMP_ABSCONV THEN
3628       EXISTS_TAC `Cx((r + R) / &2)` THEN CONJ_TAC THENL
3629        [FIRST_X_ASSUM(MP_TAC o SPEC `z + Cx((r + R) / &2)`) THEN
3630         ANTS_TAC THENL
3631          [REWRITE_TAC[NORM_ARITH `dist(z,z + r) = norm r`];
3632           REWRITE_TAC[summable; COMPLEX_RING `(z + r) - z:complex = r`] THEN
3633           MESON_TAC[]];
3634         ALL_TAC] THEN
3635       REWRITE_TAC[COMPLEX_NORM_CX] THEN
3636       EXPAND_TAC "R" THEN UNDISCH_TAC `dist(z:complex,w) < r` THEN
3637       CONV_TAC NORM_ARITH;
3638       EXISTS_TAC `1` THEN REWRITE_TAC[IN_CBALL; dist] THEN
3639       REPEAT STRIP_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN
3640       REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_MUL; REAL_ABS_NORM] THEN
3641       MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[NORM_POS_LE] THEN
3642       REWRITE_TAC[COMPLEX_NORM_POW] THEN MATCH_MP_TAC REAL_POW_LE2 THEN
3643       REWRITE_TAC[NORM_POS_LE; COMPLEX_NORM_CX] THEN
3644       UNDISCH_TAC `norm(z - x:complex) <= R` THEN CONV_TAC NORM_ARITH];
3645     DISCH_THEN(X_CHOOSE_TAC `g:complex->complex`) THEN
3646     SUBGOAL_THEN `!x. x IN cball(z,R) ==> (f:complex->complex) x = g x`
3647     MP_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
3648     X_GEN_TAC `y:complex` THEN REWRITE_TAC[IN_CBALL] THEN DISCH_TAC THEN
3649     MATCH_MP_TAC SERIES_UNIQUE THEN
3650     EXISTS_TAC `\n. (a:num->complex) n * (y - z) pow n` THEN
3651     EXISTS_TAC `k:num->bool` THEN REWRITE_TAC[] THEN CONJ_TAC THENL
3652      [FIRST_X_ASSUM MATCH_MP_TAC THEN
3653       FIRST_X_ASSUM(K ALL_TAC o SPEC `&0`) THEN
3654       REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC NORM_ARITH;
3655       REWRITE_TAC[sums; LIM_SEQUENTIALLY; dist] THEN
3656       RULE_ASSUM_TAC(REWRITE_RULE[IN_CBALL]) THEN ASM_MESON_TAC[]]]);;
3657
3658 let POWER_SERIES_LIMIT_POINT_OF_ZEROS = prove
3659  (`!f k r s.
3660         &0 < r /\
3661         (!w. dist(w,z) < r ==> ((\i. c i * (w - z) pow i) sums f(w)) k) /\
3662         (!w. w IN s ==> f(w) = Cx(&0)) /\ z limit_point_of s
3663         ==> !i. i IN k ==> c(i) = Cx(&0)`,
3664   REPEAT GEN_TAC THEN STRIP_TAC THEN
3665   ONCE_REWRITE_TAC[MESON[] `(!x. P x ==> Q x) <=> ~(?x. P x /\ ~Q x)`] THEN
3666   GEN_REWRITE_TAC RAND_CONV [num_WOP] THEN
3667   REWRITE_TAC[TAUT `(p ==> ~(q /\ ~r)) <=> q /\ p ==> r`] THEN
3668   DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN
3669   SUBGOAL_THEN
3670    `!w. w IN ball(z,r) /\ ~(w = z)
3671         ==> ((\i. c(m + i) * (w - z) pow i) sums f(w) / (w - z) pow m)
3672             {i | m + i IN k}`
3673   ASSUME_TAC THENL
3674    [REPEAT STRIP_TAC THEN MATCH_MP_TAC SUMS_EQ THEN
3675     EXISTS_TAC `\i. (c(m + i) * (w - z) pow (m + i)) / (w - z) pow m` THEN
3676     REWRITE_TAC[IN_ELIM_THM] THEN CONJ_TAC THENL
3677      [REPEAT STRIP_TAC THEN
3678       REWRITE_TAC[complex_div; GSYM COMPLEX_MUL_ASSOC] THEN
3679       AP_TERM_TAC THEN REWRITE_TAC[GSYM complex_div] THEN
3680       ASM_SIMP_TAC[COMPLEX_DIV_POW2; COMPLEX_SUB_0; LE_ADD] THEN
3681       AP_TERM_TAC THEN ARITH_TAC;
3682       REWRITE_TAC[complex_div] THEN
3683       MATCH_MP_TAC SERIES_COMPLEX_RMUL THEN
3684       MP_TAC(ISPECL [`m:num`; `\i. (c:num->complex) i * (w - z) pow i`;
3685                      `(f:complex->complex) w`; `{i:num | m + i IN k}`]
3686         (ONCE_REWRITE_RULE[ADD_SYM] SUMS_REINDEX_GEN)) THEN
3687       REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
3688       REWRITE_TAC[IMAGE; IN_ELIM_THM] THEN
3689       SUBGOAL_THEN `((\i. c i * (w - z) pow i) sums (f:complex->complex) w) k`
3690       MP_TAC THENL [ASM_MESON_TAC[IN_BALL; DIST_SYM]; ALL_TAC] THEN
3691       ONCE_REWRITE_TAC[GSYM SERIES_RESTRICT] THEN
3692       MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] SUMS_EQ) THEN
3693       X_GEN_TAC `i:num` THEN REWRITE_TAC[IN_UNIV; IN_ELIM_THM] THEN
3694       REWRITE_TAC[GSYM LE_EXISTS; MESON[]
3695         `(?x. f x IN k /\ y = f x) <=> y IN k /\ (?x. y = f x)`] THEN
3696       ASM_CASES_TAC `(i:num) IN k` THEN ASM_REWRITE_TAC[] THEN
3697       COND_CASES_TAC THEN ASM_REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_ENTIRE] THEN
3698       ASM_MESON_TAC[NOT_LE]];
3699     ALL_TAC] THEN
3700   SUBGOAL_THEN
3701    `((\i. c(m + i) * (z - z) pow i) sums
3702      vsum {0} (\i. c(m + i) * (z - z) pow i))
3703     {i | m + i IN k}`
3704   MP_TAC THENL
3705    [MATCH_MP_TAC SERIES_VSUM THEN EXISTS_TAC `{0}` THEN
3706     REWRITE_TAC[FINITE_SING; SING_SUBSET; IN_ELIM_THM; IN_SING] THEN
3707     ASM_REWRITE_TAC[ADD_CLAUSES; COMPLEX_VEC_0; COMPLEX_ENTIRE] THEN
3708     SIMP_TAC[COMPLEX_SUB_REFL; COMPLEX_POW_EQ_0];
3709     REWRITE_TAC[VSUM_SING; complex_pow; ADD_CLAUSES; COMPLEX_MUL_RID] THEN
3710     DISCH_TAC] THEN
3711   SUBGOAL_THEN
3712    `!w. w IN ball(z,r)
3713         ==> summable {i | m + i IN k} (\i. c(m + i) * (w - z) pow i)`
3714   MP_TAC THENL
3715    [X_GEN_TAC `w:complex` THEN DISCH_TAC THEN REWRITE_TAC[summable] THEN
3716     ASM_CASES_TAC `w:complex = z` THEN ASM_MESON_TAC[];
3717     REWRITE_TAC[summable; RIGHT_IMP_EXISTS_THM; SKOLEM_THM] THEN
3718     DISCH_THEN(X_CHOOSE_TAC `g:complex->complex`)] THEN
3719   SUBGOAL_THEN `(g:complex->complex) continuous_on ball(z,r)`
3720   ASSUME_TAC THENL
3721    [MATCH_MP_TAC POWER_SERIES_CONTINUOUS THEN ASM_MESON_TAC[];
3722     ALL_TAC] THEN
3723   SUBGOAL_THEN
3724    `!x. x IN closure((s INTER cball(z,r / &2)) DELETE z)
3725         ==> (g:complex->complex) x IN {Cx(&0)}`
3726   MP_TAC THENL
3727    [MATCH_MP_TAC FORALL_IN_CLOSURE THEN REWRITE_TAC[CLOSED_SING; IN_SING] THEN
3728     CONJ_TAC THENL
3729      [FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
3730         CONTINUOUS_ON_SUBSET)) THEN
3731       TRANS_TAC SUBSET_TRANS `closure(cball(z:complex,r / &2))` THEN
3732       SIMP_TAC[SUBSET_CLOSURE; INTER_SUBSET;
3733                SET_RULE `s SUBSET t ==> (s DELETE z) SUBSET t`] THEN
3734       SIMP_TAC[CLOSURE_CLOSED; CLOSED_CBALL; SUBSET_BALLS; DIST_REFL] THEN
3735       ASM_REAL_ARITH_TAC;
3736       X_GEN_TAC `w:complex` THEN REWRITE_TAC[IN_INTER; IN_DELETE] THEN
3737       STRIP_TAC THEN
3738       SUBGOAL_THEN `(g:complex->complex) w = f w / (w - z) pow m`
3739        (fun th -> ASM_SIMP_TAC[COMPLEX_DIV_EQ_0; th]) THEN
3740       MATCH_MP_TAC SERIES_UNIQUE THEN
3741       EXISTS_TAC `\i. (c:num->complex) (m + i) * (w - z) pow i` THEN
3742       EXISTS_TAC `{i:num | m + i IN k}` THEN
3743       REWRITE_TAC[] THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
3744       ASM_REWRITE_TAC[] THEN UNDISCH_TAC `w IN cball(z:complex,r / &2)` THEN
3745       REWRITE_TAC[IN_CBALL; IN_BALL] THEN ASM_REAL_ARITH_TAC];
3746     DISCH_THEN(MP_TAC o SPEC `z:complex`) THEN
3747     REWRITE_TAC[IN_CLOSURE_DELETE; NOT_IMP; IN_SING] THEN CONJ_TAC THENL
3748      [UNDISCH_TAC `(z:complex) limit_point_of s` THEN
3749       REWRITE_TAC[LIMPT_INFINITE_CBALL; INTER_ASSOC] THEN
3750       REWRITE_TAC[GSYM CBALL_MIN_INTER] THEN
3751       DISCH_THEN(fun th -> X_GEN_TAC `e:real` THEN
3752         MP_TAC(SPEC `min (r / &2) e` th)) THEN
3753       ASM_REWRITE_TAC[REAL_HALF; REAL_LT_MIN];
3754       SUBGOAL_THEN `(g:complex->complex) z = c(m:num)`
3755        (fun th -> ASM_REWRITE_TAC[th]) THEN
3756       MATCH_MP_TAC SERIES_UNIQUE THEN
3757       EXISTS_TAC `\i. (c:num->complex) (m + i) * (z - z) pow i` THEN
3758       EXISTS_TAC `{i:num | m + i IN k}` THEN
3759       ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
3760       ASM_REWRITE_TAC[CENTRE_IN_BALL]]]);;