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