(* ========================================================================= *)
(* Complex analysis.                                                         *)
(*                                                                           *)
(*              (c) Copyright, John Harrison 1998-2008                       *)
(* (c) Copyright, Marco Maggesi, Graziano Gentili and Gianni Ciolli, 2008.   *)
(*              (c) Copyright, Valentina Bruno 2010                          *)
(* ========================================================================= *)

needs "Library/floor.ml";;
needs "Library/iter.ml";;
needs "Multivariate/complexes.ml";;

prioritize_complex();;

(* ------------------------------------------------------------------------- *)
(* Some toplogical facts formulated for the complex numbers.                 *)
(* ------------------------------------------------------------------------- *)


let CLOSED_HALFSPACE_RE_GE = 
prove
 (`!b. closed {z | Re(z) >= b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CLOSED_HALFSPACE_GE) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[RE_CX; IM_CX; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CLOSED_HALFSPACE_RE_LE = 
prove
 (`!b. closed {z | Re(z) <= b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CLOSED_HALFSPACE_LE) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[RE_CX; IM_CX; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CLOSED_HALFSPACE_RE_EQ = 
prove
 (`!b. closed {z | Re(z) = b}`,

  GEN_TAC THEN REWRITE_TAC[REAL_ARITH `x = y <=> x >= y /\ x <= y`] THEN
  REWRITE_TAC[SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN
  SIMP_TAC[CLOSED_INTER; CLOSED_HALFSPACE_RE_GE; CLOSED_HALFSPACE_RE_LE]);;


let OPEN_HALFSPACE_RE_GT = 
prove
 (`!b. open {z | Re(z) > b}`,

  REWRITE_TAC[OPEN_CLOSED; CLOSED_HALFSPACE_RE_LE;
              REAL_ARITH `x > y <=> ~(x <= y)`;
              SET_RULE `UNIV DIFF {x | ~p x} = {x | p x}`]);;


let OPEN_HALFSPACE_RE_LT = 
prove
 (`!b. open {z | Re(z) < b}`,

  REWRITE_TAC[OPEN_CLOSED; CLOSED_HALFSPACE_RE_GE;
              REAL_ARITH `x < y <=> ~(x >= y)`;
              SET_RULE `UNIV DIFF {x | ~p x} = {x | p x}`]);;


let CLOSED_HALFSPACE_IM_GE = 
prove
 (`!b. closed {z | Im(z) >= b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CLOSED_HALFSPACE_GE) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CLOSED_HALFSPACE_IM_LE = 
prove
 (`!b. closed {z | Im(z) <= b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CLOSED_HALFSPACE_LE) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CLOSED_HALFSPACE_IM_EQ = 
prove
 (`!b. closed {z | Im(z) = b}`,

  GEN_TAC THEN REWRITE_TAC[REAL_ARITH `x = y <=> x >= y /\ x <= y`] THEN
  REWRITE_TAC[SET_RULE `{x | P x /\ Q x} = {x | P x} INTER {x | Q x}`] THEN
  SIMP_TAC[CLOSED_INTER; CLOSED_HALFSPACE_IM_GE; CLOSED_HALFSPACE_IM_LE]);;


let OPEN_HALFSPACE_IM_GT = 
prove
 (`!b. open {z | Im(z) > b}`,

  REWRITE_TAC[OPEN_CLOSED; CLOSED_HALFSPACE_IM_LE;
              REAL_ARITH `x > y <=> ~(x <= y)`;
              SET_RULE `UNIV DIFF {x | ~p x} = {x | p x}`]);;


let OPEN_HALFSPACE_IM_LT = 
prove
 (`!b. open {z | Im(z) < b}`,

  REWRITE_TAC[OPEN_CLOSED; CLOSED_HALFSPACE_IM_GE;
              REAL_ARITH `x < y <=> ~(x >= y)`;
              SET_RULE `UNIV DIFF {x | ~p x} = {x | p x}`]);;


let CONVEX_HALFSPACE_RE_GE = 
prove
 (`!b. convex {z | Re(z) >= b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CONVEX_HALFSPACE_GE) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CONVEX_HALFSPACE_RE_GT = 
prove
 (`!b. convex {z | Re(z) > b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CONVEX_HALFSPACE_GT) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CONVEX_HALFSPACE_RE_LE = 
prove
 (`!b. convex {z | Re(z) <= b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CONVEX_HALFSPACE_LE) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CONVEX_HALFSPACE_RE_LT = 
prove
 (`!b. convex {z | Re(z) < b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`Cx(&1)`; `b:real`] CONVEX_HALFSPACE_LT) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CONVEX_HALFSPACE_IM_GE = 
prove
 (`!b. convex {z | Im(z) >= b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CONVEX_HALFSPACE_GE) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CONVEX_HALFSPACE_IM_GT = 
prove
 (`!b. convex {z | Im(z) > b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CONVEX_HALFSPACE_GT) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CONVEX_HALFSPACE_IM_LE = 
prove
 (`!b. convex {z | Im(z) <= b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CONVEX_HALFSPACE_LE) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let CONVEX_HALFSPACE_IM_LT = 
prove
 (`!b. convex {z | Im(z) < b}`,

  GEN_TAC THEN MP_TAC(ISPECL [`ii`; `b:real`] CONVEX_HALFSPACE_LT) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
  REWRITE_TAC[EXTENSION; dot; SUM_2; DIMINDEX_2; GSYM RE_DEF; GSYM IM_DEF] THEN
  REWRITE_TAC[ii; RE_CX; IM_CX; RE; IM; IN_ELIM_THM] THEN REAL_ARITH_TAC);;


let COMPLEX_IN_BALL_0 = 
prove
 (`!v r. v IN ball(Cx(&0),r) <=> norm v < r`,

  REWRITE_TAC [GSYM COMPLEX_VEC_0; IN_BALL_0]);;


let COMPLEX_IN_CBALL_0 = 
prove
 (`!v r. v IN cball(Cx(&0),r) <=> norm v <= r`,

  REWRITE_TAC [GSYM COMPLEX_VEC_0; IN_CBALL_0]);;


let COMPLEX_IN_SPHERE_0 = 
prove
 (`!v r. v IN sphere(Cx(&0),r) <=> norm v = r`,

  REWRITE_TAC [GSYM COMPLEX_VEC_0; IN_SPHERE_0]);;


let IN_BALL_RE = 
prove
 (`!x z e. x IN ball(z,e) ==> abs(Re(x) - Re(z)) < e`,

  REPEAT GEN_TAC THEN REWRITE_TAC[IN_BALL; dist] THEN
  MP_TAC(SPEC `z - x:complex` COMPLEX_NORM_GE_RE_IM) THEN
  REWRITE_TAC[RE_SUB] THEN REAL_ARITH_TAC);;


let IN_BALL_IM = 
prove
 (`!x z e. x IN ball(z,e) ==> abs(Im(x) - Im(z)) < e`,

  REPEAT GEN_TAC THEN REWRITE_TAC[IN_BALL; dist] THEN
  MP_TAC(SPEC `z - x:complex` COMPLEX_NORM_GE_RE_IM) THEN
  REWRITE_TAC[IM_SUB] THEN REAL_ARITH_TAC);;


let IN_CBALL_RE = 
prove
 (`!x z e. x IN cball(z,e) ==> abs(Re(x) - Re(z)) <= e`,

  REPEAT GEN_TAC THEN REWRITE_TAC[IN_CBALL; dist] THEN
  MP_TAC(SPEC `z - x:complex` COMPLEX_NORM_GE_RE_IM) THEN
  REWRITE_TAC[RE_SUB] THEN REAL_ARITH_TAC);;


let IN_CBALL_IM = 
prove
 (`!x z e. x IN cball(z,e) ==> abs(Im(x) - Im(z)) <= e`,

  REPEAT GEN_TAC THEN REWRITE_TAC[IN_CBALL; dist] THEN
  MP_TAC(SPEC `z - x:complex` COMPLEX_NORM_GE_RE_IM) THEN
  REWRITE_TAC[IM_SUB] THEN REAL_ARITH_TAC);;


let CLOSED_REAL_SET = 
prove
 (`closed {z | real z}`,

  REWRITE_TAC[CLOSED_HALFSPACE_IM_EQ; real]);;


let CLOSED_REAL = 
prove
 (`closed real`,

  GEN_REWRITE_TAC RAND_CONV [SET_RULE `s = {x | s x}`] THEN
  REWRITE_TAC[CLOSED_REAL_SET]);;

(* ------------------------------------------------------------------------- *)
(* Complex-specific uniform limit composition theorems.                      *)
(* ------------------------------------------------------------------------- *)


let UNIFORM_LIM_COMPLEX_MUL = 
prove
 (`!net:(A)net P f g l m b1 b2.
        eventually (\x. !n. P n ==> norm(l n) <= b1) net /\
        eventually (\x. !n. P n ==> norm(m n) <= b2) net /\
        (!e. &0 < e
             ==> eventually (\x. !n:B. P n ==> norm(f n x - l n) < e) net) /\
        (!e. &0 < e
             ==> eventually (\x. !n. P n ==> norm(g n x - m n) < e) net)
        ==> !e. &0 < e
                ==> eventually
                     (\x. !n. P n
                              ==> norm(f n x * g n x - l n * m n) < e)
                     net`,

  REPEAT GEN_TAC THEN
  DISCH_THEN(MP_TAC o CONJ BILINEAR_COMPLEX_MUL) THEN
  REWRITE_TAC[UNIFORM_LIM_BILINEAR]);;


let UNIFORM_LIM_COMPLEX_INV = 
prove
 (`!net:(A)net P f l b.
        (!e. &0 < e
             ==> eventually (\x. !n:B. P n ==> norm(f n x - l n) < e) net) /\
        &0 < b /\ eventually (\x. !n. P n ==> b <= norm(l n)) net
        ==> !e. &0 < e
                ==> eventually
                    (\x. !n. P n ==> norm(inv(f n x) - inv(l n)) < e) net`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC EVENTUALLY_MONO THEN
  EXISTS_TAC
   `\x. !n. P n ==> b <= norm(l n) /\
                    b / &2 <= norm((f:B->A->complex) n x) /\
                    norm(f n x - l n) < e * b pow 2 / &2` THEN
  REWRITE_TAC[TAUT `(p ==> q /\ r) <=> (p ==> q) /\ (p ==> r)`] THEN
  REWRITE_TAC[FORALL_AND_THM] THEN CONJ_TAC THENL
   [X_GEN_TAC `x:A` THEN STRIP_TAC THEN X_GEN_TAC `n:B` THEN DISCH_TAC THEN
    REPEAT(FIRST_X_ASSUM(MP_TAC o SPEC `n:B`) THEN ASM_REWRITE_TAC[]) THEN
    REPEAT DISCH_TAC THEN
    SUBGOAL_THEN `~((f:B->A->complex) n x = Cx(&0)) /\ ~(l n = Cx(&0))`
    STRIP_ASSUME_TAC THENL
     [CONJ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN
      RULE_ASSUM_TAC(REWRITE_RULE[COMPLEX_NORM_CX]) THEN ASM_REAL_ARITH_TAC;
      ALL_TAC] THEN
    ASM_SIMP_TAC[COMPLEX_FIELD
     `~(x = Cx(&0)) /\ ~(y = Cx(&0))
      ==> inv x - inv y = (y - x) / (x * y)`] THEN
    ASM_SIMP_TAC[COMPLEX_NORM_DIV; REAL_LT_LDIV_EQ; COMPLEX_NORM_NZ;
                 COMPLEX_ENTIRE] THEN
    ONCE_REWRITE_TAC[NORM_SUB] THEN
    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
        REAL_LTE_TRANS)) THEN
    ASM_SIMP_TAC[REAL_LE_LMUL_EQ; REAL_ARITH `b pow 2 / &2 = b / &2 * b`] THEN
    REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
    ASM_REAL_ARITH_TAC;
    ASM_REWRITE_TAC[EVENTUALLY_AND] THEN CONJ_TAC THENL
     [FIRST_X_ASSUM(MP_TAC o SPEC `b / &2`) THEN
      ASM_REWRITE_TAC[REAL_HALF] THEN
      FIRST_X_ASSUM(fun th -> MP_TAC th THEN REWRITE_TAC[IMP_IMP] THEN
        GEN_REWRITE_TAC LAND_CONV [GSYM EVENTUALLY_AND]) THEN
      MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
      REWRITE_TAC[] THEN
      ASM_MESON_TAC[NORM_ARITH
       `b <= norm l /\ norm(f - l) < b / &2 ==> b / &2 <= norm f`];
      FIRST_X_ASSUM MATCH_MP_TAC THEN
      ASM_SIMP_TAC[REAL_HALF; REAL_POW_LT; REAL_LT_MUL]]]);;


let UNIFORM_LIM_COMPLEX_DIV = 
prove
 (`!net:(A)net P f g l m b1 b2.
        eventually (\x. !n. P n ==> norm(l n) <= b1) net /\
        &0 < b2 /\ eventually (\x. !n. P n ==> b2 <= norm(m n)) net /\
        (!e. &0 < e
             ==> eventually (\x. !n:B. P n ==> norm(f n x - l n) < e) net) /\
        (!e. &0 < e
             ==> eventually (\x. !n. P n ==> norm(g n x - m n) < e) net)
        ==> !e. &0 < e
                ==> eventually
                     (\x. !n. P n
                              ==> norm(f n x / g n x - l n / m n) < e)
                     net`,

  REPEAT GEN_TAC THEN DISCH_TAC THEN
  REWRITE_TAC[complex_div] THEN MATCH_MP_TAC UNIFORM_LIM_COMPLEX_MUL THEN
  MAP_EVERY EXISTS_TAC [`b1:real`; `inv(b2):real`] THEN
  ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
   [FIRST_X_ASSUM(CONJUNCTS_THEN2 ASSUME_TAC
     (MP_TAC o CONJUNCT1) o CONJUNCT2) THEN
    MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
    GEN_TAC THEN REWRITE_TAC[] THEN MATCH_MP_TAC MONO_FORALL THEN
    REPEAT STRIP_TAC THEN REWRITE_TAC[COMPLEX_NORM_INV] THEN
    MATCH_MP_TAC REAL_LE_INV2 THEN ASM_SIMP_TAC[];
    MATCH_MP_TAC UNIFORM_LIM_COMPLEX_INV THEN
    EXISTS_TAC `b2:real` THEN ASM_REWRITE_TAC[]]);;

(* ------------------------------------------------------------------------- *)
(* The usual non-uniform versions.                                           *)
(* ------------------------------------------------------------------------- *)


let LIM_COMPLEX_MUL = 
prove
 (`!net:(A)net f g l m.
         (f --> l) net /\ (g --> m) net ==> ((\x. f x * g x) --> l * m) net`,


let LIM_COMPLEX_INV = 
prove
 (`!net:(A)net f g l m.
         (f --> l) net /\ ~(l = Cx(&0)) ==> ((\x. inv(f x)) --> inv(l)) net`,

  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL
   [`net:(A)net`; `\x:one. T`;
    `\n:one. (f:A->complex)`;
    `\n:one. (l:complex)`;
    `norm(l:complex)`] UNIFORM_LIM_COMPLEX_INV) THEN
  ASM_REWRITE_TAC[REAL_LE_REFL; EVENTUALLY_TRUE] THEN
  ASM_REWRITE_TAC[GSYM dist; GSYM tendsto; COMPLEX_NORM_NZ]);;


let LIM_COMPLEX_DIV = 
prove
 (`!net:(A)net f g l m.
         (f --> l) net /\ (g --> m) net /\ ~(m = Cx(&0))
         ==> ((\x. f x / g x) --> l / m) net`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[complex_div] THEN
  MATCH_MP_TAC LIM_COMPLEX_MUL THEN ASM_SIMP_TAC[LIM_COMPLEX_INV]);;


let LIM_COMPLEX_POW = 
prove
 (`!net:(A)net f l n.
         (f --> l) net ==> ((\x. f(x) pow n) --> l pow n) net`,

  REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
  INDUCT_TAC THEN ASM_SIMP_TAC[LIM_COMPLEX_MUL; complex_pow; LIM_CONST]);;


let LIM_COMPLEX_LMUL = 
prove
 (`!f l c. (f --> l) net ==> ((\x. c * f x) --> c * l) net`,

  SIMP_TAC[LIM_COMPLEX_MUL; LIM_CONST]);;


let LIM_COMPLEX_RMUL = 
prove
 (`!f l c. (f --> l) net ==> ((\x. f x * c) --> l * c) net`,

  SIMP_TAC[LIM_COMPLEX_MUL; LIM_CONST]);;

(* ------------------------------------------------------------------------- *)
(* Special cases of null limits.                                             *)
(* ------------------------------------------------------------------------- *)


let LIM_NULL_COMPLEX_NEG = 
prove
 (`!net f. (f --> Cx(&0)) net ==> ((\x. --(f x)) --> Cx(&0)) net`,

  REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_NEG) THEN
  REWRITE_TAC[COMPLEX_NEG_0]);;


let LIM_NULL_COMPLEX_ADD = 
prove
 (`!net f g. (f --> Cx(&0)) net /\ (g --> Cx(&0)) net
             ==> ((\x. f x + g x) --> Cx(&0)) net`,

  REPEAT GEN_TAC THEN
  DISCH_THEN(MP_TAC o MATCH_MP LIM_ADD) THEN
  REWRITE_TAC[COMPLEX_ADD_LID]);;


let LIM_NULL_COMPLEX_SUB = 
prove
 (`!net f g. (f --> Cx(&0)) net /\ (g --> Cx(&0)) net
             ==> ((\x. f x - g x) --> Cx(&0)) net`,

  REPEAT GEN_TAC THEN
  DISCH_THEN(MP_TAC o MATCH_MP LIM_SUB) THEN
  REWRITE_TAC[COMPLEX_SUB_REFL]);;


let LIM_NULL_COMPLEX_MUL = 
prove
 (`!net f g. (f --> Cx(&0)) net /\ (g --> Cx(&0)) net
             ==> ((\x. f x * g x) --> Cx(&0)) net`,

  REPEAT GEN_TAC THEN
  DISCH_THEN(MP_TAC o MATCH_MP LIM_COMPLEX_MUL) THEN
  REWRITE_TAC[COMPLEX_MUL_LZERO]);;


let LIM_NULL_COMPLEX_LMUL = 
prove
 (`!net f c. (f --> Cx(&0)) net ==> ((\x. c * f x) --> Cx(&0)) net`,

  REPEAT STRIP_TAC THEN SUBST1_TAC(COMPLEX_RING `Cx(&0) = c * Cx(&0)`) THEN
  ASM_SIMP_TAC[LIM_COMPLEX_LMUL]);;


let LIM_NULL_COMPLEX_RMUL = 
prove
 (`!net f c. (f --> Cx(&0)) net ==> ((\x. f x * c) --> Cx(&0)) net`,

  REPEAT STRIP_TAC THEN SUBST1_TAC(COMPLEX_RING `Cx(&0) = Cx(&0) * c`) THEN
  ASM_SIMP_TAC[LIM_COMPLEX_RMUL]);;


let LIM_NULL_COMPLEX_POW = 
prove
 (`!net f n. (f --> Cx(&0)) net /\ ~(n = 0)
             ==> ((\x. (f x) pow n) --> Cx(&0)) net`,

  REPEAT STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `n:num` o MATCH_MP LIM_COMPLEX_POW) THEN
  ASM_REWRITE_TAC[COMPLEX_POW_ZERO]);;


let LIM_NULL_COMPLEX_BOUND = 
prove
 (`!f g. eventually (\n. norm (f n) <= norm (g n)) net /\ (g --> Cx(&0)) net
         ==> (f --> Cx(&0)) net`,

  REWRITE_TAC[GSYM COMPLEX_VEC_0; LIM_TRANSFORM_BOUND]);;


let SUMS_COMPLEX_0 = 
prove
 (`!f s. (!n. n IN s ==> f n = Cx(&0)) ==> (f sums Cx(&0)) s`,

  REWRITE_TAC[GSYM COMPLEX_VEC_0; SUMS_0]);;


let LIM_NULL_COMPLEX_RMUL_BOUNDED = 
prove
 (`!f g. (f --> Cx(&0)) net /\
         eventually (\a. f a = Cx(&0) \/ norm(g a) <= B) net
         ==> ((\z. f(z) * g(z)) --> Cx(&0)) net`,

  REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN
  ONCE_REWRITE_TAC[LIM_NULL_NORM] THEN
  REWRITE_TAC[LIFT_CMUL; COMPLEX_NORM_MUL] THEN
  REPEAT STRIP_TAC THEN MATCH_MP_TAC LIM_NULL_VMUL_BOUNDED THEN
  EXISTS_TAC `B:real` THEN
  ASM_REWRITE_TAC[o_DEF; NORM_LIFT; REAL_ABS_NORM; NORM_EQ_0]);;


let LIM_NULL_COMPLEX_LMUL_BOUNDED = 
prove
 (`!f g. eventually (\a. norm(f a) <= B \/ g a = Cx(&0)) net /\
         (g --> Cx(&0)) net
         ==> ((\z. f(z) * g(z)) --> Cx(&0)) net`,

  ONCE_REWRITE_TAC[DISJ_SYM; COMPLEX_MUL_SYM] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC LIM_NULL_COMPLEX_RMUL_BOUNDED THEN ASM_REWRITE_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Bound results for real and imaginary components of limits.                *)
(* ------------------------------------------------------------------------- *)


let LIM_RE_UBOUND = 
prove
 (`!net:(A)net f l b.
        ~(trivial_limit net) /\ (f --> l) net /\
        eventually (\x. Re(f x) <= b) net
        ==> Re(l) <= b`,

  REWRITE_TAC[RE_DEF] THEN REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`net:(A)net`; `f:A->complex`; `l:complex`; `b:real`; `1`]
                LIM_COMPONENT_UBOUND) THEN
  ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;


let LIM_RE_LBOUND = 
prove
 (`!net:(A)net f l b.
        ~(trivial_limit net) /\ (f --> l) net /\
        eventually (\x. b <= Re(f x)) net
        ==> b <= Re(l)`,

  REWRITE_TAC[RE_DEF] THEN REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`net:(A)net`; `f:A->complex`; `l:complex`; `b:real`; `1`]
                LIM_COMPONENT_LBOUND) THEN
  ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;


let LIM_IM_UBOUND = 
prove
 (`!net:(A)net f l b.
        ~(trivial_limit net) /\ (f --> l) net /\
        eventually (\x. Im(f x) <= b) net
        ==> Im(l) <= b`,

  REWRITE_TAC[IM_DEF] THEN REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`net:(A)net`; `f:A->complex`; `l:complex`; `b:real`; `2`]
                LIM_COMPONENT_UBOUND) THEN
  ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;


let LIM_IM_LBOUND = 
prove
 (`!net:(A)net f l b.
        ~(trivial_limit net) /\ (f --> l) net /\
        eventually (\x. b <= Im(f x)) net
        ==> b <= Im(l)`,

  REWRITE_TAC[IM_DEF] THEN REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`net:(A)net`; `f:A->complex`; `l:complex`; `b:real`; `2`]
                LIM_COMPONENT_LBOUND) THEN
  ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;

(* ------------------------------------------------------------------------- *)
(* Left and right multiplication of series.                                  *)
(* ------------------------------------------------------------------------- *)


let SERIES_COMPLEX_LMUL = 
prove
 (`!f l c s. (f sums l) s ==> ((\x. c * f x) sums c * l) s`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC SERIES_LINEAR THEN
  ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC RAND_CONV [GSYM ETA_AX] THEN
  REWRITE_TAC[LINEAR_COMPLEX_MUL]);;


let SERIES_COMPLEX_RMUL = 
prove
 (`!f l c s. (f sums l) s ==> ((\x. f x * c) sums l * c) s`,

  ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN REWRITE_TAC[SERIES_COMPLEX_LMUL]);;


let SERIES_COMPLEX_DIV = 
prove
 (`!f l c s. (f sums l) s ==> ((\x. f x / c) sums (l / c)) s`,


let SUMMABLE_COMPLEX_LMUL = 
prove
 (`!f c s. summable s f ==> summable s (\x. c * f x)`,

  REWRITE_TAC[summable] THEN MESON_TAC[SERIES_COMPLEX_LMUL]);;


let SUMMABLE_COMPLEX_RMUL = 
prove
 (`!f c s. summable s f ==> summable s (\x. f x * c)`,

  REWRITE_TAC[summable] THEN MESON_TAC[SERIES_COMPLEX_RMUL]);;


let SUMMABLE_COMPLEX_DIV = 
prove
 (`!f c s. summable s f ==> summable s (\x. f x / c)`,

  REWRITE_TAC[summable] THEN MESON_TAC[SERIES_COMPLEX_DIV]);;

(* ------------------------------------------------------------------------- *)
(* Complex-specific continuity closures.                                     *)
(* ------------------------------------------------------------------------- *)


let CONTINUOUS_COMPLEX_MUL = 
prove
 (`!net f g.
    f continuous net /\ g continuous net ==> (\x. f(x) * g(x)) continuous net`,

  SIMP_TAC[continuous; LIM_COMPLEX_MUL]);;


let CONTINUOUS_COMPLEX_INV = 
prove
 (`!net f.
    f continuous net /\ ~(f(netlimit net) = Cx(&0))
    ==> (\x. inv(f x)) continuous net`,

  SIMP_TAC[continuous; LIM_COMPLEX_INV]);;


let CONTINUOUS_COMPLEX_DIV = 
prove
 (`!net f g.
    f continuous net /\ g continuous net /\ ~(g(netlimit net) = Cx(&0))
    ==> (\x. f(x) / g(x)) continuous net`,

  SIMP_TAC[continuous; LIM_COMPLEX_DIV]);;


let CONTINUOUS_COMPLEX_POW = 
prove
 (`!net f n. f continuous net ==> (\x. f(x) pow n) continuous net`,

  SIMP_TAC[continuous; LIM_COMPLEX_POW]);;

(* ------------------------------------------------------------------------- *)
(* Write away the netlimit, which is otherwise a bit tedious.                *)
(* ------------------------------------------------------------------------- *)


let CONTINUOUS_COMPLEX_INV_WITHIN = 
prove
 (`!f s a.
    f continuous (at a within s) /\ ~(f a = Cx(&0))
    ==> (\x. inv(f x)) continuous (at a within s)`,


let CONTINUOUS_COMPLEX_INV_AT = 
prove
 (`!f a.
    f continuous (at a) /\ ~(f a = Cx(&0))
    ==> (\x. inv(f x)) continuous (at a)`,


let CONTINUOUS_COMPLEX_DIV_WITHIN = 
prove
 (`!f g s a.
    f continuous (at a within s) /\ g continuous (at a within s) /\
    ~(g a = Cx(&0))
    ==> (\x. f x / g x) continuous (at a within s)`,


let CONTINUOUS_COMPLEX_DIV_AT = 
prove
 (`!f g a.
    f continuous at a /\ g continuous at a /\ ~(g a = Cx(&0))
    ==> (\x. f x / g x) continuous at a`,

(* ------------------------------------------------------------------------- *)
(* Also prove "on" variants as needed.                                       *)
(* ------------------------------------------------------------------------- *)


let CONTINUOUS_ON_COMPLEX_MUL = 
prove
 (`!f g s. f continuous_on s /\ g continuous_on s
           ==> (\x. f(x) * g(x)) continuous_on s`,


let CONTINUOUS_ON_COMPLEX_LMUL = 
prove
 (`!f:real^N->complex s. f continuous_on s ==> (\x. c * f(x)) continuous_on s`,

  REWRITE_TAC[CONTINUOUS_ON] THEN SIMP_TAC[LIM_COMPLEX_MUL; LIM_CONST]);;


let CONTINUOUS_ON_COMPLEX_RMUL = 
prove
 (`!f:real^N->complex s. f continuous_on s ==> (\x. f(x) * c) continuous_on s`,

  REWRITE_TAC[CONTINUOUS_ON] THEN SIMP_TAC[LIM_COMPLEX_MUL; LIM_CONST]);;


let CONTINUOUS_ON_COMPLEX_INV = 
prove
 (`!f:real^N->complex.
        f continuous_on s /\
        (!x. x IN s ==> ~(f x = Cx(&0)))
        ==> (\x. inv(f x)) continuous_on s`,


let CONTINUOUS_ON_COMPLEX_DIV = 
prove
 (`!f g s. f continuous_on s /\ g continuous_on s /\
           (!x. x IN s ==> ~(g x = Cx(&0)))
           ==> (\x. f(x) / g(x)) continuous_on s`,


let CONTINUOUS_ON_COMPLEX_POW = 
prove
 (`!f n s. f continuous_on s ==> (\x. f(x) pow n) continuous_on s`,

(* ------------------------------------------------------------------------- *)
(* And also uniform versions.                                                *)
(* ------------------------------------------------------------------------- *)


let UNIFORMLY_CONTINUOUS_ON_COMPLEX_MUL = 
prove
 (`!f g s:real^N->bool.
        f uniformly_continuous_on s /\ g uniformly_continuous_on s /\
        bounded(IMAGE f s) /\ bounded(IMAGE g s)
        ==> (\x. f(x) * g(x)) uniformly_continuous_on s`,

  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL
   [`f:real^N->complex`; `g:real^N->complex`;
    `( * ):complex->complex->complex`; `s:real^N->bool`]
    BILINEAR_UNIFORMLY_CONTINUOUS_ON_COMPOSE) THEN
  ASM_REWRITE_TAC[BILINEAR_COMPLEX_MUL]);;


let UNIFORMLY_CONTINUOUS_ON_COMPLEX_LMUL = 
prove
 (`!f c s:real^N->bool.
      f uniformly_continuous_on s ==> (\x. c * f x) uniformly_continuous_on s`,

  REPEAT GEN_TAC THEN
  DISCH_THEN(MP_TAC o ISPEC `\x:complex. c * x` o MATCH_MP
   (REWRITE_RULE[IMP_CONJ] UNIFORMLY_CONTINUOUS_ON_COMPOSE)) THEN
  ASM_SIMP_TAC[o_DEF; LINEAR_COMPLEX_MUL; LINEAR_UNIFORMLY_CONTINUOUS_ON]);;


let UNIFORMLY_CONTINUOUS_ON_COMPLEX_RMUL = 
prove
 (`!f c s:real^N->bool.
      f uniformly_continuous_on s ==> (\x. f x * c) uniformly_continuous_on s`,

  ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
  REWRITE_TAC[UNIFORMLY_CONTINUOUS_ON_COMPLEX_LMUL]);;

(* ------------------------------------------------------------------------- *)
(* Continuity prover (not just for complex numbers but with more for them).  *)
(* ------------------------------------------------------------------------- *)

let CONTINUOUS_TAC =
  
let ETA_THM = 
prove
   (`f continuous net <=> (\x. f x) continuous net`,

    REWRITE_TAC[ETA_AX]) in
  let ETA_TWEAK =
    GEN_REWRITE_RULE (LAND_CONV o ONCE_DEPTH_CONV) [ETA_THM] o SPEC_ALL in
  let tac_base =
    MATCH_ACCEPT_TAC CONTINUOUS_CONST ORELSE
    MATCH_ACCEPT_TAC CONTINUOUS_AT_ID ORELSE
    MATCH_ACCEPT_TAC CONTINUOUS_WITHIN_ID
  and tac_1 =
    MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_CMUL) ORELSE
    MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_NEG) ORELSE
    MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_COMPLEX_POW)
  and tac_2 =
    MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_ADD) ORELSE
    MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_SUB) ORELSE
    MATCH_MP_TAC(ETA_TWEAK CONTINUOUS_COMPLEX_MUL)
  and tac_1' = MATCH_MP_TAC (ETA_TWEAK CONTINUOUS_COMPLEX_INV)
  and tac_2' = MATCH_MP_TAC (ETA_TWEAK CONTINUOUS_COMPLEX_DIV) in
  let rec CONTINUOUS_TAC gl =
   (tac_base ORELSE
    (tac_1 THEN CONTINUOUS_TAC) ORELSE
    (tac_2 THEN CONJ_TAC THEN CONTINUOUS_TAC) ORELSE
    (tac_1' THEN CONJ_TAC THENL
     [CONTINUOUS_TAC; REWRITE_TAC[NETLIMIT_AT; NETLIMIT_WITHIN]]) ORELSE
    (tac_2' THEN REPEAT CONJ_TAC THENL
     [CONTINUOUS_TAC; CONTINUOUS_TAC;
      REWRITE_TAC[NETLIMIT_AT; NETLIMIT_WITHIN]]) ORELSE
    ALL_TAC) gl in
  CONTINUOUS_TAC;;

(* ------------------------------------------------------------------------- *)
(* Hence a limit calculator                                                  *)
(* ------------------------------------------------------------------------- *)


let LIM_CONTINUOUS = 
prove
 (`!net f l. f continuous net /\ f(netlimit net) = l ==> (f --> l) net`,

  MESON_TAC[continuous]);;

let LIM_TAC =
  MATCH_MP_TAC LIM_CONTINUOUS THEN CONJ_TAC THENL
   [CONTINUOUS_TAC; REWRITE_TAC[NETLIMIT_AT; NETLIMIT_WITHIN]];;

(* ------------------------------------------------------------------------- *)
(* Continuity of the norm.                                                   *)
(* ------------------------------------------------------------------------- *)


let CONTINUOUS_AT_CX_NORM = 
prove
 (`!z:real^N. (\z. Cx(norm z)) continuous at z`,

  REWRITE_TAC[continuous_at; dist; GSYM CX_SUB; COMPLEX_NORM_CX] THEN
  MESON_TAC[NORM_ARITH `norm(a - b:real^N) < d ==> abs(norm a - norm b) < d`]);;


let CONTINUOUS_WITHIN_CX_NORM = 
prove
 (`!z:real^N s. (\z. Cx(norm z)) continuous (at z within s)`,


let CONTINUOUS_ON_CX_NORM = 
prove
 (`!s. (\z. Cx(norm z)) continuous_on s`,


let CONTINUOUS_AT_CX_DOT = 
prove
 (`!c z:real^N. (\z. Cx(c dot z)) continuous at z`,

  REPEAT GEN_TAC THEN MATCH_MP_TAC LINEAR_CONTINUOUS_AT THEN
  REWRITE_TAC[linear; DOT_RADD; DOT_RMUL; CX_ADD; COMPLEX_CMUL; CX_MUL]);;


let CONTINUOUS_WITHIN_CX_DOT = 
prove
 (`!c z:real^N s. (\z. Cx(c dot z)) continuous (at z within s)`,


let CONTINUOUS_ON_CX_DOT = 
prove
 (`!s c:real^N. (\z. Cx(c dot z)) continuous_on s`,

(* ------------------------------------------------------------------------- *)
(* Continuity switching range between complex and real^1                     *)
(* ------------------------------------------------------------------------- *)


let CONTINUOUS_CX_DROP = 
prove
 (`!net f. f continuous net ==> (\x. Cx(drop(f x))) continuous net`,

  REWRITE_TAC[continuous; tendsto] THEN
  REWRITE_TAC[dist; GSYM CX_SUB; COMPLEX_NORM_CX; GSYM DROP_SUB] THEN
  REWRITE_TAC[GSYM ABS_DROP]);;


let CONTINUOUS_ON_CX_DROP = 
prove
 (`!f s. f continuous_on s ==> (\x. Cx(drop(f x))) continuous_on s`,


let CONTINUOUS_CX_LIFT = 
prove
 (`!f. (\x. Cx(f x)) continuous net <=> (\x. lift(f x)) continuous net`,

  REWRITE_TAC[continuous; LIM; dist; GSYM CX_SUB; GSYM LIFT_SUB] THEN
  REWRITE_TAC[COMPLEX_NORM_CX; NORM_LIFT]);;


let CONTINUOUS_ON_CX_LIFT = 
prove
 (`!f s. (\x. Cx(f x)) continuous_on s <=> (\x. lift(f x)) continuous_on s`,

(* ------------------------------------------------------------------------- *)
(* Linearity and continuity of the components.                               *)
(* ------------------------------------------------------------------------- *)


let LINEAR_CX_RE = 
prove
 (`linear(Cx o Re)`,

  SIMP_TAC[linear; o_THM; COMPLEX_CMUL; RE_ADD; RE_MUL_CX; CX_MUL; CX_ADD]);;


let CONTINUOUS_AT_CX_RE = 
prove
 (`!z. (Cx o Re) continuous at z`,


let CONTINUOUS_ON_CX_RE = 
prove
 (`!s. (Cx o Re) continuous_on s`,


let LINEAR_CX_IM = 
prove
 (`linear(Cx o Im)`,

  SIMP_TAC[linear; o_THM; COMPLEX_CMUL; IM_ADD; IM_MUL_CX; CX_MUL; CX_ADD]);;


let CONTINUOUS_AT_CX_IM = 
prove
 (`!z. (Cx o Im) continuous at z`,


let CONTINUOUS_ON_CX_IM = 
prove
 (`!s. (Cx o Im) continuous_on s`,

(* ------------------------------------------------------------------------- *)
(* Complex differentiability.                                                *)
(* ------------------------------------------------------------------------- *)

parse_as_infix ("has_complex_derivative",(12,"right"));;
parse_as_infix ("complex_differentiable",(12,"right"));;
parse_as_infix ("holomorphic_on",(12,"right"));;


let has_complex_derivative = new_definition
 `(f has_complex_derivative f') net <=> (f has_derivative (\x. f' * x)) net`;;


let complex_differentiable = new_definition
 `f complex_differentiable net <=> ?f'. (f has_complex_derivative f') net`;;


let complex_derivative = new_definition
 `complex_derivative f x = @f'. (f has_complex_derivative f') (at x)`;;


let higher_complex_derivative = define
 `higher_complex_derivative 0 f = f /\
  (!n. higher_complex_derivative (SUC n) f =
                complex_derivative (higher_complex_derivative n f))`;;


let holomorphic_on = new_definition
 `f holomorphic_on s <=>
     !x. x IN s ==> ?f'. (f has_complex_derivative f') (at x within s)`;;


let HOLOMORPHIC_ON_DIFFERENTIABLE = 
prove
 (`!f s. f holomorphic_on s <=>
         !x. x IN s ==> f complex_differentiable (at x within s)`,


let HOLOMORPHIC_ON_OPEN = 
prove
 (`!f s. open s
         ==> (f holomorphic_on s <=>
              !x. x IN s ==> ?f'. (f has_complex_derivative f') (at x))`,


let HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_WITHIN = 
prove
 (`!f s x. f holomorphic_on s /\ x IN s
           ==> f complex_differentiable (at x within s)`,


let HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT = 
prove
 (`!f s x. f holomorphic_on s /\ open s /\ x IN s
           ==> f complex_differentiable (at x)`,


let HAS_COMPLEX_DERIVATIVE_IMP_CONTINUOUS_AT = 
prove
 (`!f f' x. (f has_complex_derivative f') (at x) ==> f continuous at x`,

  REWRITE_TAC[has_complex_derivative] THEN
  MESON_TAC[differentiable; DIFFERENTIABLE_IMP_CONTINUOUS_AT]);;


let HAS_COMPLEX_DERIVATIVE_IMP_CONTINUOUS_WITHIN = 
prove
 (`!f f' x s. (f has_complex_derivative f') (at x within s)
              ==> f continuous (at x within s)`,

  REWRITE_TAC[has_complex_derivative] THEN
  MESON_TAC[differentiable; DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN]);;


let COMPLEX_DIFFERENTIABLE_IMP_CONTINUOUS_AT = 
prove
 (`!f x. f complex_differentiable at x ==> f continuous at x`,


let HOLOMORPHIC_ON_IMP_CONTINUOUS_ON = 
prove
 (`!f s. f holomorphic_on s ==> f continuous_on s`,

  REWRITE_TAC[holomorphic_on; CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
  REWRITE_TAC[has_complex_derivative] THEN
  MESON_TAC[DIFFERENTIABLE_IMP_CONTINUOUS_WITHIN; differentiable]);;


let HOLOMORPHIC_ON_SUBSET = 
prove
 (`!f s t. f holomorphic_on s /\ t SUBSET s ==> f holomorphic_on t`,


let HAS_COMPLEX_DERIVATIVE_WITHIN_SUBSET = 
prove
 (`!f s t x. (f has_complex_derivative f') (at x within s) /\ t SUBSET s
             ==> (f has_complex_derivative f') (at x within t)`,


let COMPLEX_DIFFERENTIABLE_WITHIN_SUBSET = 
prove
 (`!f s t. f complex_differentiable (at x within s) /\ t SUBSET s
           ==> f complex_differentiable (at x within t)`,


let HAS_COMPLEX_DERIVATIVE_AT_WITHIN = 
prove
 (`!f f' x s. (f has_complex_derivative f') (at x)
              ==> (f has_complex_derivative f') (at x within s)`,


let HAS_COMPLEX_DERIVATIVE_WITHIN_OPEN = 
prove
 (`!f f' a s.
         a IN s /\ open s
         ==> ((f has_complex_derivative f') (at a within s) <=>
              (f has_complex_derivative f') (at a))`,


let COMPLEX_DIFFERENTIABLE_AT_WITHIN = 
prove
 (`!f s z. f complex_differentiable (at z)
           ==> f complex_differentiable (at z within s)`,


let HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN = 
prove
 (`!f f' g x s d.
       &0 < d /\ x IN s /\
       (!x'. x' IN s /\ dist (x',x) < d ==> f x' = g x') /\
       (f has_complex_derivative f') (at x within s)
       ==> (g has_complex_derivative f') (at x within s)`,


let HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN = 
prove
  (`!f g f' s z. open s /\ z IN s /\ (!w. w IN s ==> f w = g w) /\
                 (f has_complex_derivative f') (at z)
                 ==> (g has_complex_derivative f') (at z)`,

   REWRITE_TAC [has_complex_derivative] THEN
   ASM_MESON_TAC [HAS_DERIVATIVE_TRANSFORM_WITHIN_OPEN]);;


let HAS_COMPLEX_DERIVATIVE_TRANSFORM_AT = 
prove
 (`!f f' g x d.
       &0 < d /\ (!x'. dist (x',x) < d ==> f x' = g x') /\
       (f has_complex_derivative f') (at x)
       ==> (g has_complex_derivative f') (at x)`,

  ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_TRANSFORM_WITHIN; IN_UNIV]);;


let HAS_COMPLEX_DERIVATIVE_ZERO_CONSTANT = 
prove
 (`!f s.
        convex s /\
        (!x. x IN s ==> (f has_complex_derivative Cx(&0)) (at x within s))
        ==> ?c. !x. x IN s ==> f(x) = c`,


let HAS_COMPLEX_DERIVATIVE_ZERO_UNIQUE = 
prove
 (`!f s c a.
        convex s /\ a IN s /\ f a = c /\
        (!x. x IN s ==> (f has_complex_derivative Cx(&0)) (at x within s))
        ==> !x. x IN s ==> f(x) = c`,


let HAS_COMPLEX_DERIVATIVE_ZERO_CONNECTED_CONSTANT = 
prove
 (`!f s.
        open s /\ connected s /\
        (!x. x IN s ==> (f has_complex_derivative Cx(&0)) (at x))
        ==> ?c. !x. x IN s ==> f(x) = c`,


let HAS_COMPLEX_DERIVATIVE_ZERO_CONNECTED_UNIQUE = 
prove
 (`!f s c a.
        open s /\ connected s /\ a IN s /\ f a = c /\
        (!x. x IN s ==> (f has_complex_derivative Cx(&0)) (at x))
        ==> !x. x IN s ==> f(x) = c`,


let COMPLEX_DIFF_CHAIN_WITHIN = 
prove
 (`!f g f' g' x s.
        (f has_complex_derivative f') (at x within s) /\
        (g has_complex_derivative g') (at (f x) within (IMAGE f s))
        ==> ((g o f) has_complex_derivative (g' * f'))(at x within s)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[has_complex_derivative] THEN
  DISCH_THEN(MP_TAC o MATCH_MP DIFF_CHAIN_WITHIN) THEN
  REWRITE_TAC[o_DEF; COMPLEX_MUL_ASSOC]);;


let COMPLEX_DIFF_CHAIN_AT = 
prove
 (`!f g f' g' x.
        (f has_complex_derivative f') (at x) /\
        (g has_complex_derivative g') (at (f x))
        ==> ((g o f) has_complex_derivative (g' * f')) (at x)`,


let HAS_COMPLEX_DERIVATIVE_CHAIN = 
prove
 (`!P f g.
        (!x. P x ==> (g has_complex_derivative g'(x)) (at x))
        ==> (!x s. (f has_complex_derivative f') (at x within s) /\ P(f x)
                   ==> ((\x. g(f x)) has_complex_derivative f' * g'(f x))
                       (at x within s)) /\
            (!x. (f has_complex_derivative f') (at x) /\ P(f x)
                 ==> ((\x. g(f x)) has_complex_derivative f' * g'(f x))
                     (at x))`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM o_DEF] THEN
  ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
  ASM_MESON_TAC[COMPLEX_DIFF_CHAIN_WITHIN; COMPLEX_DIFF_CHAIN_AT;
                HAS_COMPLEX_DERIVATIVE_AT_WITHIN]);;


let HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV = 
prove
 (`!f g. (!x. (g has_complex_derivative g'(x)) (at x))
         ==> (!x s. (f has_complex_derivative f') (at x within s)
                    ==> ((\x. g(f x)) has_complex_derivative f' * g'(f x))
                        (at x within s)) /\
             (!x. (f has_complex_derivative f') (at x)
                  ==> ((\x. g(f x)) has_complex_derivative f' * g'(f x))
                      (at x))`,

  MP_TAC(SPEC `\x:complex. T` HAS_COMPLEX_DERIVATIVE_CHAIN) THEN SIMP_TAC[]);;


let COMPLEX_DERIVATIVE_UNIQUE_AT = 
prove
 (`!f z f' f''.
        (f has_complex_derivative f') (at z) /\
        (f has_complex_derivative f'') (at z)
        ==> f' = f''`,

  REPEAT GEN_TAC THEN REWRITE_TAC[has_complex_derivative] THEN
  DISCH_THEN(MP_TAC o MATCH_MP FRECHET_DERIVATIVE_UNIQUE_AT) THEN
  DISCH_THEN(MP_TAC o C AP_THM `Cx(&1)`) THEN
  REWRITE_TAC[COMPLEX_MUL_RID]);;


let HIGHER_COMPLEX_DERIVATIVE_1 = 
prove
 (`!f z. higher_complex_derivative 1 f z = complex_derivative f z`,

  REWRITE_TAC[num_CONV `1`; higher_complex_derivative]);;

(* ------------------------------------------------------------------------- *)
(* A more direct characterization.                                           *)
(* ------------------------------------------------------------------------- *)


let HAS_COMPLEX_DERIVATIVE_WITHIN = 
prove
 (`!f s a. (f has_complex_derivative f') (at a within s) <=>
           ((\x. (f(x) - f(a)) / (x - a)) --> f') (at a within s)`,

  REWRITE_TAC[has_complex_derivative; has_derivative_within] THEN
  REPEAT GEN_TAC THEN REWRITE_TAC[LINEAR_COMPLEX_MUL] THEN
  GEN_REWRITE_TAC RAND_CONV [LIM_NULL] THEN
  REWRITE_TAC[LIM_WITHIN; dist; VECTOR_SUB_RZERO; NORM_MUL] THEN
  REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ] THEN SIMP_TAC[COMPLEX_FIELD
  `~(x:complex = a) ==> y / (x - a) - z = inv(x - a) * (y - z * (x - a))`] THEN
  REWRITE_TAC[REAL_ABS_INV; COMPLEX_NORM_MUL; REAL_ABS_NORM;
         COMPLEX_NORM_INV; VECTOR_ARITH `a:complex - (b + c) = a - b - c`]);;


let HAS_COMPLEX_DERIVATIVE_AT = 
prove
 (`!f a. (f has_complex_derivative f') (at a) <=>
         ((\x. (f(x) - f(a)) / (x - a)) --> f') (at a)`,

  ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
  REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_WITHIN]);;

(* ------------------------------------------------------------------------- *)
(* Arithmetical combining theorems.                                          *)
(* ------------------------------------------------------------------------- *)


let HAS_DERIVATIVE_COMPLEX_CMUL = 
prove
 (`!net c. ((\x. c * x) has_derivative (\x. c * x)) net`,

  REPEAT GEN_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
  REWRITE_TAC[LINEAR_COMPLEX_MUL]);;


let HAS_COMPLEX_DERIVATIVE_LINEAR = 
prove
 (`!net c. ((\x. c * x) has_complex_derivative c) net`,

  REPEAT GEN_TAC THEN REWRITE_TAC[has_complex_derivative] THEN
  MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
  REWRITE_TAC[linear; COMPLEX_CMUL] THEN CONV_TAC COMPLEX_RING);;


let HAS_COMPLEX_DERIVATIVE_LMUL_WITHIN = 
prove
 (`!f f' c x s.
        (f has_complex_derivative f') (at x within s)
        ==> ((\x. c * f(x)) has_complex_derivative (c * f')) (at x within s)`,

  REPEAT GEN_TAC THEN
  MP_TAC(ISPECL [`at ((f:complex->complex) x) within (IMAGE f s)`; `c:complex`]
    HAS_COMPLEX_DERIVATIVE_LINEAR) THEN
  ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b /\ a ==> c`] THEN
  DISCH_THEN(MP_TAC o MATCH_MP COMPLEX_DIFF_CHAIN_WITHIN) THEN
  REWRITE_TAC[o_DEF]);;


let HAS_COMPLEX_DERIVATIVE_LMUL_AT = 
prove
 (`!f f' c x.
        (f has_complex_derivative f') (at x)
        ==> ((\x. c * f(x)) has_complex_derivative (c * f')) (at x)`,

  ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
  REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_LMUL_WITHIN]);;


let HAS_COMPLEX_DERIVATIVE_RMUL_WITHIN = 
prove
 (`!f f' c x s.
        (f has_complex_derivative f') (at x within s)
        ==> ((\x. f(x) * c) has_complex_derivative (f' * c)) (at x within s)`,

  ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
  REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_LMUL_WITHIN]);;


let HAS_COMPLEX_DERIVATIVE_RMUL_AT = 
prove
 (`!f f' c x.
        (f has_complex_derivative f') (at x)
        ==> ((\x. f(x) * c) has_complex_derivative (f' * c)) (at x)`,

  ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
  REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_LMUL_AT]);;


let HAS_COMPLEX_DERIVATIVE_CDIV_WITHIN = 
prove
 (`!f f' c x s.
        (f has_complex_derivative f') (at x within s)
        ==> ((\x. f(x) / c) has_complex_derivative (f' / c)) (at x within s)`,


let HAS_COMPLEX_DERIVATIVE_CDIV_AT = 
prove
 (`!f f' c x s.
        (f has_complex_derivative f') (at x)
        ==> ((\x. f(x) / c) has_complex_derivative (f' / c)) (at x)`,


let HAS_COMPLEX_DERIVATIVE_ID = 
prove
 (`!net. ((\x. x) has_complex_derivative Cx(&1)) net`,


let HAS_COMPLEX_DERIVATIVE_CONST = 
prove
 (`!c net. ((\x. c) has_complex_derivative Cx(&0)) net`,


let HAS_COMPLEX_DERIVATIVE_NEG = 
prove
 (`!f f' net. (f has_complex_derivative f') net
            ==> ((\x. --(f(x))) has_complex_derivative (--f')) net`,


let HAS_COMPLEX_DERIVATIVE_ADD = 
prove
 (`!f f' g g' net.
        (f has_complex_derivative f') net /\ (g has_complex_derivative g') net
        ==> ((\x. f(x) + g(x)) has_complex_derivative (f' + g')) net`,


let HAS_COMPLEX_DERIVATIVE_SUB = 
prove
 (`!f f' g g' net.
        (f has_complex_derivative f') net /\ (g has_complex_derivative g') net
        ==> ((\x. f(x) - g(x)) has_complex_derivative (f' - g')) net`,


let HAS_COMPLEX_DERIVATIVE_MUL_WITHIN = 
prove
 (`!f f' g g' x s.
        (f has_complex_derivative f') (at x within s) /\
        (g has_complex_derivative g') (at x within s)
        ==> ((\x. f(x) * g(x)) has_complex_derivative
             (f(x) * g' + f' * g(x))) (at x within s)`,

  REPEAT GEN_TAC THEN SIMP_TAC[has_complex_derivative] THEN
  DISCH_THEN(MP_TAC o C CONJ BILINEAR_COMPLEX_MUL) THEN
  REWRITE_TAC[GSYM CONJ_ASSOC] THEN
  DISCH_THEN(MP_TAC o MATCH_MP HAS_DERIVATIVE_BILINEAR_WITHIN) THEN
  MATCH_MP_TAC EQ_IMP THEN
  AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
  CONV_TAC COMPLEX_RING);;


let HAS_COMPLEX_DERIVATIVE_MUL_AT = 
prove
 (`!f f' g g' x.
        (f has_complex_derivative f') (at x) /\
        (g has_complex_derivative g') (at x)
        ==> ((\x. f(x) * g(x)) has_complex_derivative
             (f(x) * g' + f' * g(x))) (at x)`,

  ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
  REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_MUL_WITHIN]);;


let HAS_COMPLEX_DERIVATIVE_POW_WITHIN = 
prove
 (`!f f' x s n. (f has_complex_derivative f') (at x within s)
                ==> ((\x. f(x) pow n) has_complex_derivative
                     (Cx(&n) * f(x) pow (n - 1) * f')) (at x within s)`,

  REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN DISCH_TAC THEN
  INDUCT_TAC THEN REWRITE_TAC[complex_pow] THEN
  REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_CONST; COMPLEX_MUL_LZERO] THEN
  POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
  DISCH_THEN(MP_TAC o MATCH_MP HAS_COMPLEX_DERIVATIVE_MUL_WITHIN) THEN
  REWRITE_TAC[SUC_SUB1] THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
  BINOP_TAC THEN REWRITE_TAC[COMPLEX_MUL_AC; GSYM REAL_OF_NUM_SUC] THEN
  SPEC_TAC(`n:num`,`n:num`) THEN REWRITE_TAC[CX_ADD] THEN INDUCT_TAC THEN
  CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[SUC_SUB1; complex_pow] THEN
  CONV_TAC COMPLEX_FIELD);;


let HAS_COMPLEX_DERIVATIVE_POW_AT = 
prove
 (`!f f' x n. (f has_complex_derivative f') (at x)
              ==> ((\x. f(x) pow n) has_complex_derivative
                   (Cx(&n) * f(x) pow (n - 1) * f')) (at x)`,

  ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
  REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_POW_WITHIN]);;


let HAS_COMPLEX_DERIVATIVE_INV_BASIC = 
prove
 (`!x. ~(x = Cx(&0))
         ==> ((inv) has_complex_derivative (--inv(x pow 2))) (at x)`,

  REPEAT STRIP_TAC THEN
  REWRITE_TAC[has_complex_derivative; has_derivative_at] THEN
  REWRITE_TAC[LINEAR_COMPLEX_MUL; COMPLEX_VEC_0] THEN
  MATCH_MP_TAC LIM_TRANSFORM_AWAY_AT THEN
  MAP_EVERY EXISTS_TAC
   [`\y. inv(norm(y - x)) % inv(x pow 2 * y) * (y - x) pow 2`; `Cx(&0)`] THEN
  ASM_REWRITE_TAC[COMPLEX_CMUL] THEN CONJ_TAC THENL
   [POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD; ALL_TAC] THEN
  SUBGOAL_THEN `((\y. inv(x pow 2 * y) * (y - x)) --> Cx(&0)) (at x)`
  MP_TAC THENL
   [LIM_TAC THEN POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD; ALL_TAC] THEN
  MATCH_MP_TAC EQ_IMP THEN REWRITE_TAC[LIM_AT] THEN
  REWRITE_TAC[dist; COMPLEX_SUB_RZERO] THEN
  REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_INV; COMPLEX_NORM_POW] THEN
  REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_INV; REAL_ABS_NORM] THEN
  REPLICATE_TAC 2 (AP_TERM_TAC THEN ABS_TAC THEN AP_TERM_TAC) THEN
  AP_TERM_TAC THEN ABS_TAC THEN
  MATCH_MP_TAC(MESON[]
   `(p ==> x = y) ==> ((p ==> x < e) <=> (p ==> y < e))`) THEN
  MAP_EVERY ABBREV_TAC
   [`n = norm(x' - x:complex)`;
    `m = inv (norm(x:complex) pow 2 * norm(x':complex))`] THEN
  CONV_TAC REAL_FIELD);;


let HAS_COMPLEX_DERIVATIVE_INV_WITHIN = 
prove
 (`!f f' x s. (f has_complex_derivative f') (at x within s) /\
              ~(f x = Cx(&0))
              ==> ((\x. inv(f(x))) has_complex_derivative (--f' / f(x) pow 2))
                  (at x within s)`,

  REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM o_DEF] THEN
  ASM_SIMP_TAC[COMPLEX_FIELD
   `~(g = Cx(&0)) ==> --f / g pow 2 = --inv(g pow 2) * f`] THEN
  MATCH_MP_TAC COMPLEX_DIFF_CHAIN_WITHIN THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_AT_WITHIN THEN
  ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_INV_BASIC]);;


let HAS_COMPLEX_DERIVATIVE_INV_AT = 
prove
 (`!f f' x. (f has_complex_derivative f') (at x) /\
            ~(f x = Cx(&0))
            ==> ((\x. inv(f(x))) has_complex_derivative (--f' / f(x) pow 2))
                (at x)`,

  ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
  REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_INV_WITHIN]);;


let HAS_COMPLEX_DERIVATIVE_DIV_WITHIN = 
prove
 (`!f f' g g' x s.
        (f has_complex_derivative f') (at x within s) /\
        (g has_complex_derivative g') (at x within s) /\
        ~(g(x) = Cx(&0))
        ==> ((\x. f(x) / g(x)) has_complex_derivative
             (f' * g(x) - f(x) * g') / g(x) pow 2) (at x within s)`,

  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  DISCH_THEN(fun th -> ASSUME_TAC(CONJUNCT2 th) THEN MP_TAC th) THEN
  DISCH_THEN(MP_TAC o MATCH_MP HAS_COMPLEX_DERIVATIVE_INV_WITHIN) THEN
  UNDISCH_TAC `(f has_complex_derivative f') (at x within s)` THEN
  REWRITE_TAC[IMP_IMP] THEN
  DISCH_THEN(MP_TAC o MATCH_MP HAS_COMPLEX_DERIVATIVE_MUL_WITHIN) THEN
  REWRITE_TAC[GSYM complex_div] THEN MATCH_MP_TAC EQ_IMP THEN
  AP_THM_TAC THEN AP_TERM_TAC THEN
  POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD);;


let HAS_COMPLEX_DERIVATIVE_DIV_AT = 
prove
 (`!f f' g g' x.
        (f has_complex_derivative f') (at x) /\
        (g has_complex_derivative g') (at x) /\
        ~(g(x) = Cx(&0))
        ==> ((\x. f(x) / g(x)) has_complex_derivative
             (f' * g(x) - f(x) * g') / g(x) pow 2) (at x)`,

  ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
  REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_DIV_WITHIN]);;


let HAS_COMPLEX_DERIVATIVE_VSUM = 
prove
 (`!f net s.
         FINITE s /\ (!a. a IN s ==> (f a has_complex_derivative f' a) net)
         ==> ((\x. vsum s (\a. f a x)) has_complex_derivative (vsum s f'))
             net`,

  SIMP_TAC[GSYM VSUM_COMPLEX_RMUL; has_complex_derivative] THEN
  REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP HAS_DERIVATIVE_VSUM) THEN
  REWRITE_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Same thing just for complex differentiability.                            *)
(* ------------------------------------------------------------------------- *)


let COMPLEX_DIFFERENTIABLE_LINEAR = 
prove
 (`(\z. c * z) complex_differentiable p`,

  REWRITE_TAC [complex_differentiable] THEN
  MESON_TAC [HAS_COMPLEX_DERIVATIVE_LINEAR]);;


let COMPLEX_DIFFERENTIABLE_CONST = 
prove
 (`!c net. (\z. c) complex_differentiable net`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_CONST]);;


let COMPLEX_DIFFERENTIABLE_ID = 
prove
 (`!net. (\z. z) complex_differentiable net`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_ID]);;


let COMPLEX_DIFFERENTIABLE_NEG = 
prove
 (`!f net.
        f complex_differentiable net
        ==> (\z. --(f z)) complex_differentiable net`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_NEG]);;


let COMPLEX_DIFFERENTIABLE_ADD = 
prove
 (`!f g net.
        f complex_differentiable net /\
        g complex_differentiable net
        ==> (\z. f z + g z) complex_differentiable net`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_ADD]);;


let COMPLEX_DIFFERENTIABLE_SUB = 
prove
 (`!f g net.
        f complex_differentiable net /\
        g complex_differentiable net
        ==> (\z. f z - g z) complex_differentiable net`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_SUB]);;


let COMPLEX_DIFFERENTIABLE_INV_WITHIN = 
prove
 (`!f z s.
        f complex_differentiable (at z within s) /\ ~(f z = Cx(&0))
        ==> (\z. inv(f z)) complex_differentiable (at z within s)`,


let COMPLEX_DIFFERENTIABLE_MUL_WITHIN = 
prove
 (`!f g z s.
        f complex_differentiable (at z within s) /\
        g complex_differentiable (at z within s)
        ==> (\z. f z * g z) complex_differentiable (at z within s)`,


let COMPLEX_DIFFERENTIABLE_DIV_WITHIN = 
prove
 (`!f g z s.
        f complex_differentiable (at z within s) /\
        g complex_differentiable (at z within s) /\
        ~(g z = Cx(&0))
        ==> (\z. f z / g z) complex_differentiable (at z within s)`,


let COMPLEX_DIFFERENTIABLE_POW_WITHIN = 
prove
 (`!f n z s.
        f complex_differentiable (at z within s)
        ==> (\z. f z pow n) complex_differentiable (at z within s)`,


let COMPLEX_DIFFERENTIABLE_TRANSFORM_WITHIN = 
prove
 (`!f g x s d.
        &0 < d /\
        x IN s /\
        (!x'. x' IN s /\ dist (x',x) < d ==> f x' = g x') /\
        f complex_differentiable (at x within s)
        ==> g complex_differentiable (at x within s)`,


let HOLOMORPHIC_TRANSFORM = 
prove
 (`!f g s. (!x. x IN s ==> f x = g x) /\ f holomorphic_on s
           ==> g holomorphic_on s`,

  REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  REWRITE_TAC[holomorphic_on; GSYM complex_differentiable] THEN
  MATCH_MP_TAC MONO_FORALL THEN GEN_TAC THEN
  DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
  ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
  MATCH_MP_TAC COMPLEX_DIFFERENTIABLE_TRANSFORM_WITHIN THEN
  MAP_EVERY EXISTS_TAC [`f:complex->complex`; `&1`] THEN
  ASM_SIMP_TAC[REAL_LT_01]);;


let HOLOMORPHIC_EQ = 
prove
 (`!f g s. (!x. x IN s ==> f x = g x)
           ==> (f holomorphic_on s <=> g holomorphic_on s)`,

  MESON_TAC[HOLOMORPHIC_TRANSFORM]);;


let COMPLEX_DIFFERENTIABLE_INV_AT = 
prove
 (`!f z.
        f complex_differentiable at z /\ ~(f z = Cx(&0))
        ==> (\z. inv(f z)) complex_differentiable at z`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_INV_AT]);;


let COMPLEX_DIFFERENTIABLE_MUL_AT = 
prove
 (`!f g z.
        f complex_differentiable at z /\
        g complex_differentiable at z
        ==> (\z. f z * g z) complex_differentiable at z`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_MUL_AT]);;


let COMPLEX_DIFFERENTIABLE_DIV_AT = 
prove
 (`!f g z.
        f complex_differentiable at z /\
        g complex_differentiable at z /\
        ~(g z = Cx(&0))
        ==> (\z. f z / g z) complex_differentiable at z`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_DIV_AT]);;


let COMPLEX_DIFFERENTIABLE_POW_AT = 
prove
 (`!f n z.
        f complex_differentiable at z
        ==> (\z. f z pow n) complex_differentiable at z`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[HAS_COMPLEX_DERIVATIVE_POW_AT]);;


let COMPLEX_DIFFERENTIABLE_TRANSFORM_AT = 
prove
 (`!f g x d.
        &0 < d /\
        (!x'. dist (x',x) < d ==> f x' = g x') /\
        f complex_differentiable at x
        ==> g complex_differentiable at x`,


let COMPLEX_DIFFERENTIABLE_COMPOSE_WITHIN = 
prove
 (`!f g x s.
         f complex_differentiable (at x within s) /\
         g complex_differentiable (at (f x) within IMAGE f s)
         ==> (g o f) complex_differentiable (at x within s)`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[COMPLEX_DIFF_CHAIN_WITHIN]);;


let COMPLEX_DIFFERENTIABLE_COMPOSE_AT = 
prove
 (`!f g x s.
         f complex_differentiable (at x) /\
         g complex_differentiable (at (f x))
         ==> (g o f) complex_differentiable (at x)`,

  REWRITE_TAC[complex_differentiable] THEN
  MESON_TAC[COMPLEX_DIFF_CHAIN_AT]);;


let COMPLEX_DIFFERENTIABLE_WITHIN_OPEN = 
prove
 (`!f a s.
        a IN s /\ open s
        ==> (f complex_differentiable at a within s <=>
             f complex_differentiable at a)`,

(* ------------------------------------------------------------------------- *)
(* Same again for being holomorphic on a set.                                *)
(* ------------------------------------------------------------------------- *)


let HOLOMORPHIC_ON_LINEAR = 
prove
 (`!s c. (\w. c * w) holomorphic_on s`,

  REWRITE_TAC [holomorphic_on] THEN
  MESON_TAC [HAS_COMPLEX_DERIVATIVE_LINEAR]);;


let HOLOMORPHIC_ON_CONST = 
prove
 (`!c s. (\z. c) holomorphic_on s`,


let HOLOMORPHIC_ON_ID = 
prove
 (`!s. (\z. z) holomorphic_on s`,


let HOLOMORPHIC_ON_COMPOSE = 
prove
 (`!f g s. f holomorphic_on s /\ g holomorphic_on (IMAGE f s)
           ==> (g o f) holomorphic_on s`,


let HOLOMORPHIC_ON_NEG = 
prove
 (`!f s. f holomorphic_on s ==> (\z. --(f z)) holomorphic_on s`,


let HOLOMORPHIC_ON_ADD = 
prove
 (`!f g s.
        f holomorphic_on s /\ g holomorphic_on s
        ==> (\z. f z + g z) holomorphic_on s`,


let HOLOMORPHIC_ON_SUB = 
prove
 (`!f g s.
        f holomorphic_on s /\ g holomorphic_on s
        ==> (\z. f z - g z) holomorphic_on s`,


let HOLOMORPHIC_ON_MUL = 
prove
 (`!f g s.
        f holomorphic_on s /\ g holomorphic_on s
        ==> (\z. f z * g z) holomorphic_on s`,


let HOLOMORPHIC_ON_INV = 
prove
 (`!f s. f holomorphic_on s /\ (!z. z IN s ==> ~(f z = Cx(&0)))
         ==> (\z. inv(f z)) holomorphic_on s`,


let HOLOMORPHIC_ON_DIV = 
prove
 (`!f g s.
        f holomorphic_on s /\ g holomorphic_on s /\
        (!z. z IN s ==> ~(g z = Cx(&0)))
        ==> (\z. f z / g z) holomorphic_on s`,


let HOLOMORPHIC_ON_POW = 
prove
 (`!f s n. f holomorphic_on s ==> (\z. (f z) pow n) holomorphic_on s`,


let HOLOMORPHIC_ON_VSUM = 
prove
 (`!f s k. FINITE k /\ (!a. a IN k ==> (f a) holomorphic_on s)
           ==> (\x. vsum k (\a. f a x)) holomorphic_on s`,

  GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN SIMP_TAC[VSUM_CLAUSES] THEN
  SIMP_TAC[HOLOMORPHIC_ON_CONST; IN_INSERT; NOT_IN_EMPTY] THEN
  REPEAT STRIP_TAC THEN MATCH_MP_TAC HOLOMORPHIC_ON_ADD THEN
  ASM_SIMP_TAC[ETA_AX]);;


let HOLOMORPHIC_ON_COMPOSE_GEN = 
prove
 (`!f g s t. f holomorphic_on s /\ g holomorphic_on t /\
             (!z. z IN s ==> f z IN t)
             ==>  g o f holomorphic_on s`,

  REWRITE_TAC [holomorphic_on] THEN REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `IMAGE (f:complex->complex) s SUBSET t` MP_TAC THENL
   [ASM SET_TAC []; ASM_MESON_TAC [HAS_COMPLEX_DERIVATIVE_WITHIN_SUBSET;
                                   COMPLEX_DIFF_CHAIN_WITHIN]]);;

(* ------------------------------------------------------------------------- *)
(* Same again for the actual derivative function.                            *)
(* ------------------------------------------------------------------------- *)


let HAS_COMPLEX_DERIVATIVE_DERIVATIVE = 
prove
 (`!f f' x. (f has_complex_derivative f') (at x)
                ==> complex_derivative f x = f'`,

  REWRITE_TAC[complex_derivative] THEN
  MESON_TAC[COMPLEX_DERIVATIVE_UNIQUE_AT]);;


let HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE = 
prove
 (`!f x. (f has_complex_derivative (complex_derivative f x)) (at x) <=>
         f complex_differentiable at x`,

  REWRITE_TAC[complex_differentiable; complex_derivative] THEN MESON_TAC[]);;


let COMPLEX_DIFFERENTIABLE_COMPOSE = 
prove
 (`!f g z. f complex_differentiable at z /\ g complex_differentiable at (f z)
          ==> (g o f) complex_differentiable at z`,

  REWRITE_TAC [complex_differentiable] THEN
  MESON_TAC [COMPLEX_DIFF_CHAIN_AT]);;


let COMPLEX_DERIVATIVE_CHAIN = 
prove
 (`!f g z. f complex_differentiable at z /\ g complex_differentiable at (f z)
           ==> complex_derivative (g o f) z =
               complex_derivative g (f z) * complex_derivative f z`,


let COMPLEX_DERIVATIVE_LINEAR = 
prove
 (`!c. complex_derivative (\w. c * w) = \z. c`,

  REWRITE_TAC [FUN_EQ_THM] THEN REPEAT GEN_TAC THEN
  MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_DERIVATIVE THEN
  REWRITE_TAC [HAS_COMPLEX_DERIVATIVE_LINEAR]);;


let COMPLEX_DERIVATIVE_ID = 
prove
 (`complex_derivative (\w.w) = \z. Cx(&1)`,


let COMPLEX_DERIVATIVE_CONST = 
prove
 (`!c. complex_derivative (\w.c) = \z. Cx(&0)`,


let COMPLEX_DERIVATIVE_ADD = 
prove
 (`!f g z. f complex_differentiable at z /\ g complex_differentiable at z
           ==> complex_derivative (\w. f w + g w) z =
               complex_derivative f z + complex_derivative g z`,


let COMPLEX_DERIVATIVE_SUB = 
prove
 (`!f g z. f complex_differentiable at z /\ g complex_differentiable at z
           ==> complex_derivative (\w. f w - g w) z =
               complex_derivative f z - complex_derivative g z`,


let COMPLEX_DERIVATIVE_MUL = 
prove
 (`!f g z. f complex_differentiable at z /\ g complex_differentiable at z
           ==> complex_derivative (\w. f w * g w) z =
               f z * complex_derivative g z + complex_derivative f z * g z`,


let COMPLEX_DERIVATIVE_LMUL = 
prove
 (`!f c z. f complex_differentiable at z
             ==> complex_derivative (\w. c * f w) z =
                 c * complex_derivative f z`,


let COMPLEX_DERIVATIVE_RMUL = 
prove
 (`!f c z. f complex_differentiable at z
           ==> complex_derivative (\w. f w * c) z =
               complex_derivative f z * c`,


let COMPLEX_DERIVATIVE_TRANSFORM_WITHIN_OPEN = 
prove
 (`!f g s z. open s /\ f holomorphic_on s /\ g holomorphic_on s /\ z IN s /\
             (!w. w IN s ==> f w = g w)
             ==> complex_derivative f z = complex_derivative g z`,


let COMPLEX_DERIVATIVE_COMPOSE_LINEAR = 
prove
 (`!f c z. f complex_differentiable at (c * z)
           ==> complex_derivative (\w. f (c * w)) z =
               c * complex_derivative f (c * z)`,

(* ------------------------------------------------------------------------- *)
(* Caratheodory characterization.                                            *)
(* ------------------------------------------------------------------------- *)


let HAS_COMPLEX_DERIVATIVE_CARATHEODORY_AT = 
prove
 (`!f f' z.
        (f has_complex_derivative f') (at z) <=>
        ?g. (!w. f(w) - f(z) = g(w) * (w - z)) /\
            g continuous at z /\ g(z) = f'`,

  REPEAT GEN_TAC THEN
  REWRITE_TAC[COMPLEX_RING `w' - z':complex = a <=> w' = z' + a`] THEN
  SIMP_TAC[GSYM FUN_EQ_THM; HAS_COMPLEX_DERIVATIVE_AT; CONTINUOUS_AT] THEN
  EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
   [EXISTS_TAC `\w. if w = z then f':complex else (f(w) - f(z)) / (w - z)` THEN
    ASM_SIMP_TAC[FUN_EQ_THM; COND_RAND; COND_RATOR; COMPLEX_SUB_REFL] THEN
    CONV_TAC COMPLEX_FIELD;
    FIRST_X_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN
    ASM_SIMP_TAC[COMPLEX_RING `(z + a) - (z + b * (w - w)):complex = a`] THEN
    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
      LIM_TRANSFORM)) THEN
    SIMP_TAC[LIM_CONST; COMPLEX_VEC_0; COMPLEX_FIELD
     `~(w = z) ==> x - (x * (w - z)) / (w - z) = Cx(&0)`]]);;


let HAS_COMPLEX_DERIVATIVE_CARATHEODORY_WITHIN = 
prove
 (`!f f' z s.
        (f has_complex_derivative f') (at z within s) <=>
        ?g. (!w. f(w) - f(z) = g(w) * (w - z)) /\
            g continuous (at z within s) /\ g(z) = f'`,

  REPEAT GEN_TAC THEN
  REWRITE_TAC[COMPLEX_RING `w' - z':complex = a <=> w' = z' + a`] THEN
  SIMP_TAC[GSYM FUN_EQ_THM; HAS_COMPLEX_DERIVATIVE_WITHIN;
           CONTINUOUS_WITHIN] THEN
  EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
   [EXISTS_TAC `\w. if w = z then f':complex else (f(w) - f(z)) / (w - z)` THEN
    ASM_SIMP_TAC[FUN_EQ_THM; COND_RAND; COND_RATOR; COMPLEX_SUB_REFL] THEN
    CONV_TAC COMPLEX_FIELD;
    FIRST_X_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM SUBST1_TAC THEN
    ASM_SIMP_TAC[COMPLEX_RING `(z + a) - (z + b * (w - w)):complex = a`] THEN
    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
      LIM_TRANSFORM)) THEN
    SIMP_TAC[LIM_CONST; COMPLEX_VEC_0; COMPLEX_FIELD
     `~(w = z) ==> x - (x * (w - z)) / (w - z) = Cx(&0)`]]);;


let COMPLEX_DIFFERENTIABLE_CARATHEODORY_AT = 
prove
 (`!f z. f complex_differentiable at z <=>
         ?g. (!w. f(w) - f(z) = g(w) * (w - z)) /\ g continuous at z`,


let COMPLEX_DIFFERENTIABLE_CARATHEODORY_WITHIN = 
prove
 (`!f z s.
      f complex_differentiable (at z within s) <=>
      ?g. (!w. f(w) - f(z) = g(w) * (w - z)) /\ g continuous (at z within s)`,

(* ------------------------------------------------------------------------- *)
(* A slightly stronger, more traditional notion of analyticity on a set.     *)
(* ------------------------------------------------------------------------- *)

parse_as_infix ("analytic_on",(12,"right"));;


let analytic_on = new_definition
 `f analytic_on s <=>
      !x. x IN s ==> ?e. &0 < e /\ f holomorphic_on ball(x,e)`;;


let ANALYTIC_IMP_HOLOMORPHIC = 
prove
 (`!f s. f analytic_on s ==> f holomorphic_on s`,


let ANALYTIC_ON_OPEN = 
prove
 (`!f s. open s ==> (f analytic_on s <=> f holomorphic_on s)`,

  REPEAT STRIP_TAC THEN EQ_TAC THEN REWRITE_TAC[ANALYTIC_IMP_HOLOMORPHIC] THEN
  REWRITE_TAC[analytic_on; holomorphic_on] THEN
  ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_WITHIN_OPEN; OPEN_BALL] THEN
  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [OPEN_CONTAINS_BALL]) THEN
  REWRITE_TAC[SUBSET] THEN MESON_TAC[CENTRE_IN_BALL]);;


let ANALYTIC_ON_IMP_DIFFERENTIABLE_AT = 
prove
 (`!f s x. f analytic_on s /\ x IN s ==> f complex_differentiable (at x)`,


let ANALYTIC_ON_SUBSET = 
prove
 (`!f s t. f analytic_on s /\ t SUBSET s ==> f analytic_on t`,

  REWRITE_TAC[analytic_on; SUBSET] THEN MESON_TAC[]);;


let ANALYTIC_ON_UNION = 
prove
 (`!f s t. f analytic_on (s UNION t) <=> f analytic_on s /\ f analytic_on t`,

  REWRITE_TAC [analytic_on; IN_UNION] THEN MESON_TAC[]);;


let ANALYTIC_ON_UNIONS = 
prove
 (`!f s. f analytic_on (UNIONS s) <=> (!t. t IN s ==> f analytic_on t)`,

  REWRITE_TAC [analytic_on; IN_UNIONS] THEN MESON_TAC[]);;


let ANALYTIC_ON_HOLOMORPHIC = 
prove
 (`!f s. f analytic_on s <=> ?t. open t /\ s SUBSET t /\ f holomorphic_on t`,

  REPEAT GEN_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
  EXISTS_TAC `?t. open t /\ s SUBSET t /\ f analytic_on t` THEN CONJ_TAC THENL
   [EQ_TAC THENL
    [DISCH_TAC THEN EXISTS_TAC `UNIONS {u | open u /\ f analytic_on u}` THEN
     SIMP_TAC [IN_ELIM_THM; OPEN_UNIONS; ANALYTIC_ON_UNIONS] THEN
     REWRITE_TAC [SUBSET; IN_UNIONS; IN_ELIM_THM] THEN
     ASM_MESON_TAC [analytic_on; ANALYTIC_ON_OPEN; OPEN_BALL; CENTRE_IN_BALL];
     MESON_TAC [ANALYTIC_ON_SUBSET]];
    MESON_TAC [ANALYTIC_ON_OPEN]]);;


let ANALYTIC_ON_LINEAR = 
prove
 (`!s c. (\w. c * w) analytic_on s`,

  REPEAT GEN_TAC THEN
  REWRITE_TAC [ANALYTIC_ON_HOLOMORPHIC; HOLOMORPHIC_ON_LINEAR] THEN
  EXISTS_TAC `(:complex)` THEN REWRITE_TAC [OPEN_UNIV; SUBSET_UNIV]);;


let ANALYTIC_ON_CONST = 
prove
 (`!c s. (\z. c) analytic_on s`,

  REWRITE_TAC[analytic_on; HOLOMORPHIC_ON_CONST] THEN MESON_TAC[REAL_LT_01]);;


let ANALYTIC_ON_ID = 
prove
 (`!s. (\z. z) analytic_on s`,

  REWRITE_TAC[analytic_on; HOLOMORPHIC_ON_ID] THEN MESON_TAC[REAL_LT_01]);;


let ANALYTIC_ON_COMPOSE = 
prove
 (`!f g s. f analytic_on s /\ g analytic_on (IMAGE f s)
           ==> (g o f) analytic_on s`,

  REWRITE_TAC[analytic_on; FORALL_IN_IMAGE] THEN REPEAT GEN_TAC THEN
  DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "f") (LABEL_TAC "g")) THEN
  X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
  REMOVE_THEN "f" (MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP HOLOMORPHIC_ON_IMP_CONTINUOUS_ON) THEN
  SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_AT; OPEN_BALL] THEN
  DISCH_THEN(MP_TAC o SPEC `z:complex`) THEN
  ASM_REWRITE_TAC[CENTRE_IN_BALL; CONTINUOUS_AT_BALL] THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
  DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `k:real` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `min (d:real) k` THEN ASM_REWRITE_TAC[REAL_LT_MIN] THEN
  MATCH_MP_TAC HOLOMORPHIC_ON_COMPOSE THEN
  CONJ_TAC THEN MATCH_MP_TAC HOLOMORPHIC_ON_SUBSET THENL
   [EXISTS_TAC `ball(z:complex,d)`;
    EXISTS_TAC `ball((f:complex->complex) z,e)`] THEN
  ASM_REWRITE_TAC[BALL_MIN_INTER; INTER_SUBSET] THEN ASM SET_TAC[]);;


let ANALYTIC_ON_COMPOSE_GEN = 
prove
 (`!f g s t. f analytic_on s /\ g analytic_on t /\ (!z. z IN s ==> f z IN t)
             ==> g o f analytic_on s`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC ANALYTIC_ON_COMPOSE THEN
  ASM_REWRITE_TAC[] THEN MATCH_MP_TAC ANALYTIC_ON_SUBSET THEN ASM SET_TAC[]);;


let ANALYTIC_ON_NEG = 
prove
 (`!f s. f analytic_on s ==> (\z. --(f z)) analytic_on s`,

  SIMP_TAC[analytic_on] THEN MESON_TAC[HOLOMORPHIC_ON_NEG]);;


let ANALYTIC_ON_ADD = 
prove
 (`!f g s.
        f analytic_on s /\ g analytic_on s ==> (\z. f z + g z) analytic_on s`,

  REPEAT GEN_TAC THEN REWRITE_TAC[analytic_on] THEN
  REWRITE_TAC[AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
  GEN_TAC THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2
   (X_CHOOSE_TAC `d:real`) (X_CHOOSE_TAC `e:real`)) THEN
  EXISTS_TAC `min (d:real) e` THEN
  ASM_REWRITE_TAC[REAL_LT_MIN; BALL_MIN_INTER; IN_INTER] THEN
  MATCH_MP_TAC HOLOMORPHIC_ON_ADD THEN
  ASM_MESON_TAC[HOLOMORPHIC_ON_SUBSET; INTER_SUBSET]);;


let ANALYTIC_ON_SUB = 
prove
 (`!f g s.
        f analytic_on s /\ g analytic_on s ==> (\z. f z - g z) analytic_on s`,


let ANALYTIC_ON_MUL = 
prove
 (`!f g s.
        f analytic_on s /\ g analytic_on s ==> (\z. f z * g z) analytic_on s`,

  REPEAT GEN_TAC THEN REWRITE_TAC[analytic_on] THEN
  REWRITE_TAC[AND_FORALL_THM] THEN MATCH_MP_TAC MONO_FORALL THEN
  GEN_TAC THEN DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
  ASM_REWRITE_TAC[] THEN DISCH_THEN(CONJUNCTS_THEN2
   (X_CHOOSE_TAC `d:real`) (X_CHOOSE_TAC `e:real`)) THEN
  EXISTS_TAC `min (d:real) e` THEN
  ASM_REWRITE_TAC[REAL_LT_MIN; BALL_MIN_INTER; IN_INTER] THEN
  MATCH_MP_TAC HOLOMORPHIC_ON_MUL THEN
  ASM_MESON_TAC[HOLOMORPHIC_ON_SUBSET; INTER_SUBSET]);;


let ANALYTIC_ON_INV = 
prove
 (`!f s. f analytic_on s /\ (!z. z IN s ==> ~(f z = Cx(&0)))
         ==> (\z. inv(f z)) analytic_on s`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[analytic_on] THEN
  X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [analytic_on]) THEN
  DISCH_THEN(MP_TAC o SPEC `z:complex`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
  SUBGOAL_THEN `?e. &0 < e /\ !y:complex. dist(z,y) < e ==> ~(f y = Cx(&0))`
  MP_TAC THENL
   [MATCH_MP_TAC CONTINUOUS_ON_OPEN_AVOID THEN
    EXISTS_TAC `ball(z:complex,d)` THEN
    ASM_SIMP_TAC[HOLOMORPHIC_ON_IMP_CONTINUOUS_ON; CENTRE_IN_BALL; OPEN_BALL];
    REWRITE_TAC[GSYM IN_BALL] THEN
    DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `min (d:real) e` THEN ASM_REWRITE_TAC[REAL_LT_MIN] THEN
    MATCH_MP_TAC HOLOMORPHIC_ON_INV THEN
    ASM_SIMP_TAC[BALL_MIN_INTER; IN_INTER] THEN
    ASM_MESON_TAC[HOLOMORPHIC_ON_SUBSET; INTER_SUBSET]]);;


let ANALYTIC_ON_DIV = 
prove
 (`!f g s.
        f analytic_on s /\ g analytic_on s /\
        (!z. z IN s ==> ~(g z = Cx(&0)))
        ==> (\z. f z / g z) analytic_on s`,


let ANALYTIC_ON_POW = 
prove
 (`!f s n. f analytic_on s ==> (\z. (f z) pow n) analytic_on s`,

  REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN
  DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[complex_pow] THEN
  ASM_SIMP_TAC[ANALYTIC_ON_CONST; ANALYTIC_ON_MUL]);;


let ANALYTIC_ON_VSUM = 
prove
 (`!f s k. FINITE k /\ (!a. a IN k ==> (f a) analytic_on s)
           ==> (\x. vsum k (\a. f a x)) analytic_on s`,

  GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[IMP_CONJ] THEN
  MATCH_MP_TAC FINITE_INDUCT_STRONG THEN SIMP_TAC[VSUM_CLAUSES] THEN
  SIMP_TAC[ANALYTIC_ON_CONST; IN_INSERT; NOT_IN_EMPTY] THEN
  REPEAT STRIP_TAC THEN MATCH_MP_TAC ANALYTIC_ON_ADD THEN
  ASM_SIMP_TAC[ETA_AX]);;

(* ------------------------------------------------------------------------- *)
(* The case of analyticity at a point.                                       *)
(* ------------------------------------------------------------------------- *)


let ANALYTIC_AT_BALL = 
prove
 (`!f z. f analytic_on {z} <=> ?e. &0<e /\ f holomorphic_on ball (z,e)`,

  REWRITE_TAC [analytic_on; IN_SING] THEN MESON_TAC []);;


let ANALYTIC_AT = 
prove
 (`!f z. f analytic_on {z} <=> ?s. open s /\ z IN s /\ f holomorphic_on s`,


let ANALYTIC_ON_ANALYTIC_AT = 
prove
 (`!f s. f analytic_on s <=> !z. z IN s ==> f analytic_on {z}`,

  REWRITE_TAC [ANALYTIC_AT_BALL; analytic_on]);;


let ANALYTIC_AT_TWO = 
prove
 (`!f g z. f analytic_on {z} /\ g analytic_on {z} <=>
    ?s. open s /\ z IN s /\ f holomorphic_on s /\ g holomorphic_on s`,

  REWRITE_TAC [ANALYTIC_AT] THEN
  MESON_TAC [HOLOMORPHIC_ON_SUBSET; OPEN_INTER; INTER_SUBSET; IN_INTER]);;


let ANALYTIC_AT_ADD = 
prove
 (`!f g z. f analytic_on {z} /\ g analytic_on {z}
     ==> (\w. f w + g w) analytic_on {z}`,

  REWRITE_TAC [ANALYTIC_AT_TWO] THEN REWRITE_TAC [ANALYTIC_AT] THEN
  MESON_TAC [HOLOMORPHIC_ON_ADD]);;


let ANALYTIC_AT_SUB = 
prove
 (`!f g z. f analytic_on {z} /\ g analytic_on {z}
     ==> (\w. f w - g w) analytic_on {z}`,

  REWRITE_TAC [ANALYTIC_AT_TWO] THEN REWRITE_TAC [ANALYTIC_AT] THEN
  MESON_TAC [HOLOMORPHIC_ON_SUB]);;


let ANALYTIC_AT_MUL = 
prove
 (`!f g z. f analytic_on {z} /\ g analytic_on {z}

     ==> (\w. f w * g w) analytic_on {z}`,

  REWRITE_TAC [ANALYTIC_AT_TWO] THEN REWRITE_TAC [ANALYTIC_AT] THEN
  MESON_TAC [HOLOMORPHIC_ON_MUL]);;


let ANALYTIC_AT_POW = 
prove
 (`!f n z. f analytic_on {z}
     ==> (\w. f w pow n) analytic_on {z}`,

  REWRITE_TAC [ANALYTIC_AT] THEN MESON_TAC [HOLOMORPHIC_ON_POW]);;

(* ------------------------------------------------------------------------- *)
(* Combining theorems for derivative with analytic_at {z} hypotheses.        *)
(* ------------------------------------------------------------------------- *)


let COMPLEX_DERIVATIVE_ADD_AT = 
prove
 (`!f g z. f analytic_on {z} /\ g analytic_on {z}
     ==> complex_derivative (\w. f w + g w) z =
           complex_derivative f z + complex_derivative g z`,

  REWRITE_TAC [ANALYTIC_AT_TWO] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC COMPLEX_DERIVATIVE_ADD THEN
  ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;


let COMPLEX_DERIVATIVE_SUB_AT = 
prove
 (`!f g z. f analytic_on {z} /\ g analytic_on {z}
     ==> complex_derivative (\w. f w - g w) z =
           complex_derivative f z - complex_derivative g z`,

  REWRITE_TAC [ANALYTIC_AT_TWO] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC COMPLEX_DERIVATIVE_SUB THEN
  ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;


let COMPLEX_DERIVATIVE_MUL_AT = 
prove
 (`!f g z. f analytic_on {z} /\ g analytic_on {z}
     ==> complex_derivative (\w. f w * g w) z =
           f z * complex_derivative g z + complex_derivative f z * g z`,

  REWRITE_TAC [ANALYTIC_AT_TWO] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC COMPLEX_DERIVATIVE_MUL THEN
  ASM_MESON_TAC [HOLOMORPHIC_ON_IMP_DIFFERENTIABLE_AT]);;


let COMPLEX_DERIVATIVE_LMUL_AT = 
prove
 (`!f c z. f analytic_on {z}
    ==> complex_derivative (\w. c * f w) z = c * complex_derivative f z`,


let COMPLEX_DERIVATIVE_RMUL_AT = 
prove
 (`!f c z. f analytic_on {z}
    ==> complex_derivative (\w. f w * c) z = complex_derivative f z * c`,

(* ------------------------------------------------------------------------- *)
(* A composition lemma for functions of mixed type.                          *)
(* ------------------------------------------------------------------------- *)


let HAS_VECTOR_DERIVATIVE_REAL_COMPLEX = 
prove
 (`(f has_complex_derivative f') (at(Cx(drop a)))
   ==> ((\x. f(Cx(drop x))) has_vector_derivative f') (at a)`,

  REWRITE_TAC[has_complex_derivative; has_vector_derivative] THEN
  REWRITE_TAC[COMPLEX_CMUL] THEN MP_TAC(ISPECL
   [`\x. Cx(drop x)`; `f:complex->complex`;
    `\x. Cx(drop x)`; `\x:complex. f' * x`; `a:real^1`] DIFF_CHAIN_AT) THEN
  REWRITE_TAC[o_DEF; COMPLEX_MUL_SYM; IMP_CONJ] THEN
  DISCH_THEN MATCH_MP_TAC THEN MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
  REWRITE_TAC[linear; DROP_ADD; DROP_CMUL; CX_ADD; CX_MUL; COMPLEX_CMUL]);;

(* ------------------------------------------------------------------------- *)
(* Complex differentiation of sequences and series.                          *)
(* ------------------------------------------------------------------------- *)


let HAS_COMPLEX_DERIVATIVE_SEQUENCE = 
prove
 (`!s f f' g'.
         convex s /\
         (!n x. x IN s
                ==> (f n has_complex_derivative f' n x) (at x within s)) /\
         (!e. &0 < e
              ==> ?N. !n x. n >= N /\ x IN s ==> norm (f' n x - g' x) <= e) /\
         (?x l. x IN s /\ ((\n. f n x) --> l) sequentially)
         ==> ?g. !x. x IN s
                     ==> ((\n. f n x) --> g x) sequentially /\
                         (g has_complex_derivative g' x) (at x within s)`,

  REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC HAS_DERIVATIVE_SEQUENCE THEN
  EXISTS_TAC `\n x h:complex. (f':num->complex->complex) n x * h` THEN
  ASM_SIMP_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
  REWRITE_TAC[GSYM COMPLEX_SUB_RDISTRIB; COMPLEX_NORM_MUL] THEN
  ASM_MESON_TAC[REAL_LE_RMUL; NORM_POS_LE]);;


let HAS_COMPLEX_DERIVATIVE_SERIES = 
prove
 (`!s f f' g' k.
         convex s /\
         (!n x. x IN s
                ==> (f n has_complex_derivative f' n x) (at x within s)) /\
         (!e. &0 < e
              ==> ?N. !n x. n >= N /\ x IN s
                            ==> norm(vsum (k INTER (0..n)) (\i. f' i x) - g' x)
                                    <= e) /\
         (?x l. x IN s /\ ((\n. f n x) sums l) k)
         ==> ?g. !x. x IN s
                     ==> ((\n. f n x) sums g x) k /\
                         (g has_complex_derivative g' x) (at x within s)`,

  REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC HAS_DERIVATIVE_SERIES THEN
  EXISTS_TAC `\n x h:complex. (f':num->complex->complex) n x * h` THEN
  ASM_SIMP_TAC[] THEN CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
  SIMP_TAC[GSYM COMPLEX_SUB_RDISTRIB; VSUM_COMPLEX_RMUL; FINITE_NUMSEG;
           FINITE_INTER; COMPLEX_NORM_MUL] THEN
  ASM_MESON_TAC[REAL_LE_RMUL; NORM_POS_LE]);;

(* ------------------------------------------------------------------------- *)
(* Bound theorem.                                                            *)
(* ------------------------------------------------------------------------- *)


let COMPLEX_DIFFERENTIABLE_BOUND = 
prove
 (`!f f' s B.
        convex s /\
        (!x. x IN s ==> (f has_complex_derivative f'(x)) (at x within s) /\
                        norm(f' x) <= B)
        ==> !x y. x IN s /\ y IN s ==> norm(f x - f y) <= B * norm(x - y)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[has_complex_derivative] THEN
  STRIP_TAC THEN MATCH_MP_TAC DIFFERENTIABLE_BOUND THEN
  EXISTS_TAC `\x:complex h. f' x * h` THEN ASM_SIMP_TAC[] THEN
  REPEAT STRIP_TAC THEN
  MP_TAC(ISPEC `\h. (f':complex->complex) x * h` ONORM) THEN
  REWRITE_TAC[LINEAR_COMPLEX_MUL] THEN
  DISCH_THEN(MATCH_MP_TAC o CONJUNCT2) THEN
  GEN_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN
  ASM_MESON_TAC[REAL_LE_RMUL; NORM_POS_LE]);;

(* ------------------------------------------------------------------------- *)
(* Inverse function theorem for complex derivatives.                         *)
(* ------------------------------------------------------------------------- *)


let HAS_COMPLEX_DERIVATIVE_INVERSE_BASIC = 
prove
 (`!f g f' t y.
        (f has_complex_derivative f') (at (g y)) /\
        ~(f' = Cx(&0)) /\
        g continuous at y /\
        open t /\
        y IN t /\
        (!z. z IN t ==> f (g z) = z)
        ==> (g has_complex_derivative inv(f')) (at y)`,

  REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_BASIC THEN
  MAP_EVERY EXISTS_TAC
   [`f:complex->complex`; `\x:complex. f' * x`; `t:complex->bool`] THEN
  ASM_REWRITE_TAC[LINEAR_COMPLEX_MUL; FUN_EQ_THM; o_THM; I_THM] THEN
  UNDISCH_TAC `~(f' = Cx(&0))` THEN CONV_TAC COMPLEX_FIELD);;


let HAS_COMPLEX_DERIVATIVE_INVERSE_STRONG = 
prove
 (`!f g f' s x.
         open s /\
         x IN s /\
         f continuous_on s /\
         (!x. x IN s ==> g (f x) = x) /\
         (f has_complex_derivative f') (at x) /\
         ~(f' = Cx(&0))
         ==> (g has_complex_derivative inv(f')) (at (f x))`,

  REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_STRONG THEN
  MAP_EVERY EXISTS_TAC [`\x:complex. f' * x`; `s:complex->bool`] THEN
  ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
  UNDISCH_TAC `~(f' = Cx(&0))` THEN CONV_TAC COMPLEX_FIELD);;


let HAS_COMPLEX_DERIVATIVE_INVERSE_STRONG_X = 
prove
 (`!f g f' s y.
        open s /\ (g y) IN s /\ f continuous_on s /\
        (!x. x IN s ==> (g(f(x)) = x)) /\
        (f has_complex_derivative f') (at (g y)) /\ ~(f' = Cx(&0)) /\
        f(g y) = y
        ==> (g has_complex_derivative inv(f')) (at y)`,

  REWRITE_TAC[has_complex_derivative] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC HAS_DERIVATIVE_INVERSE_STRONG_X THEN MAP_EVERY EXISTS_TAC
   [`f:complex->complex`; `\x:complex. f' * x`; `s:complex->bool`] THEN
  ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
  UNDISCH_TAC `~(f' = Cx(&0))` THEN CONV_TAC COMPLEX_FIELD);;

(* ------------------------------------------------------------------------- *)
(* Cauchy-Riemann condition and relation to conformal.                       *)
(* ------------------------------------------------------------------------- *)


let COMPLEX_BASIS = 
prove
 (`basis 1 = Cx(&1) /\ basis 2 = ii`,

  SIMP_TAC[CART_EQ; FORALL_2; BASIS_COMPONENT; DIMINDEX_2; ARITH] THEN
  REWRITE_TAC[GSYM RE_DEF; GSYM IM_DEF; RE_CX; IM_CX] THEN
  REWRITE_TAC[ii] THEN SIMPLE_COMPLEX_ARITH_TAC);;


let COMPLEX_DIFFERENTIABLE_IMP_DIFFERENTIABLE = 
prove
 (`!net f. f complex_differentiable net ==> f differentiable net`,

  SIMP_TAC[complex_differentiable; differentiable; has_complex_derivative] THEN
  MESON_TAC[]);;


let CAUCHY_RIEMANN = 
prove
 (`!f z. f complex_differentiable at z <=>
         f differentiable at z  /\
         (jacobian f (at z))$1$1 = (jacobian f (at z))$2$2 /\
         (jacobian f (at z))$1$2 = --((jacobian f (at z))$2$1)`,

  REPEAT GEN_TAC THEN REWRITE_TAC[complex_differentiable] THEN EQ_TAC THENL
   [REWRITE_TAC[has_complex_derivative] THEN
    DISCH_THEN(X_CHOOSE_THEN `f':complex` ASSUME_TAC) THEN
    CONJ_TAC THENL [ASM_MESON_TAC[differentiable]; ALL_TAC] THEN
    REWRITE_TAC[jacobian] THEN
    FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP FRECHET_DERIVATIVE_AT) THEN
    SIMP_TAC[matrix; LAMBDA_BETA; DIMINDEX_2; ARITH] THEN
    REWRITE_TAC[COMPLEX_BASIS; GSYM RE_DEF; GSYM IM_DEF; ii] THEN
    SIMPLE_COMPLEX_ARITH_TAC;
    STRIP_TAC THEN EXISTS_TAC
     `complex(jacobian (f:complex->complex) (at z)$1$1,
              jacobian f (at z)$2$1)` THEN
    REWRITE_TAC[has_complex_derivative] THEN
    FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [JACOBIAN_WORKS]) THEN
    MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
    ASM_SIMP_TAC[CART_EQ; matrix_vector_mul; DIMINDEX_2; SUM_2; ARITH;
                 FORALL_2; FUN_EQ_THM; LAMBDA_BETA] THEN
    REWRITE_TAC[GSYM RE_DEF; GSYM IM_DEF; IM; RE; complex_mul] THEN
    REAL_ARITH_TAC]);;


let COMPLEX_DERIVATIVE_JACOBIAN = 
prove
 (`!f z.
        f complex_differentiable (at z)
        ==> complex_derivative f z =
            complex(jacobian f (at z)$1$1,jacobian f (at z)$2$1)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC COMPLEX_DERIVATIVE_UNIQUE_AT THEN
  MAP_EVERY EXISTS_TAC [`f:complex->complex`; `z:complex`] THEN
  ASM_REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_DIFFERENTIABLE] THEN
  REWRITE_TAC[has_complex_derivative] THEN
  FIRST_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [CAUCHY_RIEMANN]) THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [JACOBIAN_WORKS]) THEN
  MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
  ASM_SIMP_TAC[CART_EQ; matrix_vector_mul; DIMINDEX_2; SUM_2; ARITH;
               FORALL_2; FUN_EQ_THM; LAMBDA_BETA] THEN
  REWRITE_TAC[GSYM RE_DEF; GSYM IM_DEF; IM; RE; complex_mul] THEN
  REAL_ARITH_TAC);;


let COMPLEX_DIFFERENTIABLE_EQ_CONFORMAL = 
prove
 (`!f z.
      f complex_differentiable at z /\ ~(complex_derivative f z = Cx(&0)) <=>
      f differentiable at z  /\
      ?a. ~(a = &0) /\ rotation_matrix (a %% jacobian f (at z))`,

  REPEAT GEN_TAC THEN EQ_TAC THENL
   [DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
    ASM_SIMP_TAC[COMPLEX_DIFFERENTIABLE_IMP_DIFFERENTIABLE;
                 COMPLEX_DERIVATIVE_JACOBIAN] THEN
    REWRITE_TAC[GSYM COMPLEX_VEC_0; GSYM DOT_EQ_0] THEN
    REWRITE_TAC[DOT_2; GSYM RE_DEF; GSYM IM_DEF; RE; IM; GSYM REAL_POW_2] THEN
    REWRITE_TAC[RE_DEF; IM_DEF; ROTATION_MATRIX_2] THEN
    RULE_ASSUM_TAC(REWRITE_RULE[CAUCHY_RIEMANN]) THEN
    ASM_REWRITE_TAC[MATRIX_CMUL_COMPONENT] THEN DISCH_TAC THEN
    REWRITE_TAC[REAL_MUL_RNEG; GSYM REAL_ADD_LDISTRIB;
                REAL_ARITH `(a * x:real) pow 2 = a pow 2 * x pow 2`] THEN
    EXISTS_TAC
     `inv(sqrt(jacobian (f:complex->complex) (at z)$2$2 pow 2 +
               jacobian f (at z)$2$1 pow 2))` THEN
    MATCH_MP_TAC(REAL_FIELD
     `x pow 2 = y /\ ~(y = &0)
      ==> ~(inv x = &0) /\ inv(x) pow 2 * y = &1`) THEN
    ASM_SIMP_TAC[SQRT_POW_2; REAL_LE_ADD; REAL_LE_POW_2];
    REWRITE_TAC[ROTATION_MATRIX_2; MATRIX_CMUL_COMPONENT] THEN
    DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
    DISCH_THEN(X_CHOOSE_THEN `a:real` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
    ASM_REWRITE_TAC[GSYM REAL_MUL_RNEG; REAL_EQ_MUL_LCANCEL] THEN
    STRIP_TAC THEN MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN
    CONJ_TAC THENL [ASM_REWRITE_TAC[CAUCHY_RIEMANN]; DISCH_TAC] THEN
    ASM_SIMP_TAC[COMPLEX_DERIVATIVE_JACOBIAN] THEN
    REWRITE_TAC[GSYM COMPLEX_VEC_0; GSYM DOT_EQ_0] THEN
    REWRITE_TAC[DOT_2; GSYM RE_DEF; GSYM IM_DEF; RE; IM; GSYM REAL_POW_2] THEN
    FIRST_X_ASSUM(MP_TAC o MATCH_MP
     (REAL_RING `(a * x) pow 2 + (a * y) pow 2 = &1
                 ==> ~(x pow 2 + y pow 2 = &0)`)) THEN
    ASM_REWRITE_TAC[RE_DEF; IM_DEF]]);;

(* ------------------------------------------------------------------------- *)
(* Differentiation conversion.                                               *)
(* ------------------------------------------------------------------------- *)

let complex_differentiation_theorems = ref [];;

let add_complex_differentiation_theorems =
  
let ETA_THM = 
prove
   (`(f has_complex_derivative f') net <=>
     ((\x. f x) has_complex_derivative f') net`,

    REWRITE_TAC[ETA_AX]) in
  let ETA_TWEAK =
    PURE_REWRITE_RULE [IMP_CONJ] o
    GEN_REWRITE_RULE (LAND_CONV o ONCE_DEPTH_CONV) [ETA_THM] o
    SPEC_ALL in
  fun l -> complex_differentiation_theorems :=
              !complex_differentiation_theorems @ map ETA_TWEAK l;;

add_complex_differentiation_theorems
 [HAS_COMPLEX_DERIVATIVE_LMUL_WITHIN; HAS_COMPLEX_DERIVATIVE_LMUL_AT;
  HAS_COMPLEX_DERIVATIVE_RMUL_WITHIN; HAS_COMPLEX_DERIVATIVE_RMUL_AT;
  HAS_COMPLEX_DERIVATIVE_CDIV_WITHIN; HAS_COMPLEX_DERIVATIVE_CDIV_AT;
  HAS_COMPLEX_DERIVATIVE_ID;
  HAS_COMPLEX_DERIVATIVE_CONST;
  HAS_COMPLEX_DERIVATIVE_NEG;
  HAS_COMPLEX_DERIVATIVE_ADD;
  HAS_COMPLEX_DERIVATIVE_SUB;
  HAS_COMPLEX_DERIVATIVE_MUL_WITHIN; HAS_COMPLEX_DERIVATIVE_MUL_AT;
  HAS_COMPLEX_DERIVATIVE_DIV_WITHIN; HAS_COMPLEX_DERIVATIVE_DIV_AT;
  HAS_COMPLEX_DERIVATIVE_POW_WITHIN; HAS_COMPLEX_DERIVATIVE_POW_AT;
  HAS_COMPLEX_DERIVATIVE_INV_WITHIN; HAS_COMPLEX_DERIVATIVE_INV_AT];;

let rec COMPLEX_DIFF_CONV =
  let partfn tm = let l,r = dest_comb tm in mk_pair(lhand l,r)
  and is_deriv = can (term_match [] `(f has_complex_derivative f') net`) in
  let rec COMPLEX_DIFF_CONV tm =
    try tryfind (fun th -> PART_MATCH partfn th (partfn tm))
                (!complex_differentiation_theorems)
    with Failure _ ->
        let ith = tryfind (fun th ->
         PART_MATCH (partfn o repeat (snd o dest_imp)) th (partfn tm))
                    (!complex_differentiation_theorems) in
        COMPLEX_DIFF_ELIM ith
  and COMPLEX_DIFF_ELIM th =
    let tm = concl th in
    if not(is_imp tm) then th else
    let t = lhand tm in
    if not(is_deriv t) then UNDISCH th
    else COMPLEX_DIFF_ELIM (MATCH_MP th (COMPLEX_DIFF_CONV t)) in
  COMPLEX_DIFF_CONV;;

(* ------------------------------------------------------------------------- *)
(* Hence a tactic.                                                           *)
(* ------------------------------------------------------------------------- *)

let COMPLEX_DIFF_TAC =
  let pth = MESON[]
   `(f has_complex_derivative f') net
    ==> f' = g'
        ==> (f has_complex_derivative g') net` in
  W(fun (asl,w) -> let th = MATCH_MP pth (COMPLEX_DIFF_CONV w) in
       MATCH_MP_TAC(repeat (GEN_REWRITE_RULE I [IMP_IMP]) (DISCH_ALL th)));;

let COMPLEX_DIFFERENTIABLE_TAC =
  let DISCH_FIRST th = DISCH (hd(hyp th)) th in
  GEN_REWRITE_TAC I [complex_differentiable] THEN
  W(fun (asl,w) ->
        let th = COMPLEX_DIFF_CONV(snd(dest_exists w)) in
        let f' = rand(rator(concl th)) in
        EXISTS_TAC f' THEN
        (if hyp th = [] then MATCH_ACCEPT_TAC th else
         let th' = repeat (GEN_REWRITE_RULE I [IMP_IMP] o DISCH_FIRST)
                          (DISCH_FIRST th) in
         MATCH_MP_TAC th'));;

(* ------------------------------------------------------------------------- *)
(* A kind of complex Taylor theorem.                                         *)
(* ------------------------------------------------------------------------- *)


let COMPLEX_TAYLOR = 
prove
 (`!f n s B.
    convex s /\
    (!i x. x IN s /\ i <= n
           ==> ((f i) has_complex_derivative f (i + 1) x) (at x within s)) /\
    (!x. x IN s ==> norm(f (n + 1) x) <= B)
    ==> !w z. w IN s /\ z IN s
              ==> norm(f 0 z -
                       vsum (0..n) (\i. f i w * (z - w) pow i / Cx(&(FACT i))))
                  <= B * norm(z - w) pow (n + 1) / &(FACT n)`,

  
let lemma = prove
   (`!f:num->real^N.
          vsum (0..n) f = f 0 - f (n + 1) + vsum (0..n) (\i. f (i + 1))`,
    REWRITE_TAC[GSYM(REWRITE_CONV[o_DEF] `(f:num->real^N) o (\i. i + 1)`)] THEN
    ASM_SIMP_TAC[GSYM VSUM_IMAGE; EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
    REWRITE_TAC[GSYM NUMSEG_OFFSET_IMAGE] THEN
    SIMP_TAC[VSUM_CLAUSES_LEFT; LE_0] THEN
    REWRITE_TAC[VSUM_CLAUSES_NUMSEG; GSYM ADD1] THEN
    REWRITE_TAC[ARITH; ARITH_RULE `1 <= SUC n`] THEN VECTOR_ARITH_TAC) in
  REPEAT STRIP_TAC THEN MP_TAC(SPECL
   [`(\w. vsum (0..n) (\i. f i w * (z - w) pow i / Cx(&(FACT i))))`;
    `\w. (f:num->complex->complex) (n + 1) w *
         (z - w) pow n / Cx(&(FACT n))`; `segment[w:complex,z]`;
    `B * norm(z - w:complex) pow n / &(FACT n)`]
   COMPLEX_DIFFERENTIABLE_BOUND) THEN
  ANTS_TAC THENL
   [ASM_REWRITE_TAC[CONVEX_SEGMENT] THEN X_GEN_TAC `u:complex` THEN
    DISCH_TAC THEN SUBGOAL_THEN `(u:complex) IN s` ASSUME_TAC THENL
     [ASM_MESON_TAC[CONVEX_CONTAINS_SEGMENT; SUBSET]; ALL_TAC] THEN
    CONJ_TAC THENL
     [ALL_TAC;
      REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_DIV; COMPLEX_NORM_CX;
                  COMPLEX_NORM_POW; REAL_ABS_NUM] THEN
      MATCH_MP_TAC REAL_LE_MUL2 THEN
      ASM_SIMP_TAC[REAL_LE_DIV; NORM_POS_LE; REAL_POS; REAL_POW_LE] THEN
      ASM_SIMP_TAC[REAL_LE_DIV2_EQ; REAL_OF_NUM_LT; FACT_LT] THEN
      MATCH_MP_TAC REAL_POW_LE2 THEN REWRITE_TAC[NORM_POS_LE] THEN
      ASM_MESON_TAC[SEGMENT_BOUND; NORM_SUB]] THEN
    MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_WITHIN_SUBSET THEN
    EXISTS_TAC `s:complex->bool` THEN CONJ_TAC THENL
     [ALL_TAC; ASM_MESON_TAC[CONVEX_CONTAINS_SEGMENT]] THEN
    SUBGOAL_THEN
     `((\u. vsum (0..n) (\i. f i u * (z - u) pow i / Cx (&(FACT i))))
       has_complex_derivative
       vsum (0..n) (\i. f i u * (-- Cx(&i) * (z - u) pow (i - 1)) /
                                Cx(&(FACT i)) +
                        f (i + 1) u * (z - u) pow i / Cx (&(FACT i))))
      (at u within s)`
    MP_TAC THENL
     [MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_VSUM THEN
      REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
      MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_MUL_WITHIN THEN
      ASM_SIMP_TAC[ETA_AX] THEN W(MP_TAC o COMPLEX_DIFF_CONV o snd) THEN
      MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
      REWRITE_TAC[complex_div] THEN CONV_TAC COMPLEX_RING;
      ALL_TAC] THEN
    ASM_SIMP_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
    AP_TERM_TAC THEN REWRITE_TAC[VSUM_ADD_NUMSEG] THEN
    GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [lemma] THEN
    REWRITE_TAC[GSYM VSUM_ADD_NUMSEG; GSYM COMPLEX_ADD_ASSOC] THEN
    REWRITE_TAC[ADD_SUB] THEN REWRITE_TAC[GSYM ADD1; FACT] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_MUL; CX_MUL] THEN
    REWRITE_TAC[complex_div; COMPLEX_INV_MUL; GSYM COMPLEX_MUL_ASSOC] THEN
    REWRITE_TAC[COMPLEX_RING
      `--a * b * inv a * c:complex = --(a * inv a) * b * c`] THEN
    SIMP_TAC[COMPLEX_MUL_RINV; CX_INJ; REAL_ARITH `~(&n + &1 = &0)`] THEN
    REWRITE_TAC[COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; COMPLEX_MUL_LID] THEN
    REWRITE_TAC[COMPLEX_ADD_LINV; GSYM COMPLEX_VEC_0; VSUM_0] THEN
    REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_ADD_RID] THEN
    REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO; COMPLEX_NEG_0] THEN
    CONV_TAC COMPLEX_RING;
    ALL_TAC] THEN
  DISCH_THEN(MP_TAC o SPECL [`z:complex`; `w:complex`]) THEN ANTS_TAC THEN
  ASM_REWRITE_TAC[ENDS_IN_SEGMENT] THEN MATCH_MP_TAC EQ_IMP THEN
  BINOP_TAC THENL
   [ALL_TAC;
    REWRITE_TAC[REAL_POW_ADD; real_div; REAL_POW_1] THEN REAL_ARITH_TAC] THEN
  AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
  SIMP_TAC[VSUM_CLAUSES_LEFT; LE_0; complex_pow; FACT; COMPLEX_DIV_1] THEN
  REWRITE_TAC[SIMPLE_COMPLEX_ARITH `x * Cx(&1) + y = x <=> y = Cx(&0)`] THEN
  REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN MATCH_MP_TAC VSUM_EQ_0 THEN
  INDUCT_TAC THEN
  ASM_REWRITE_TAC[complex_pow; complex_div; COMPLEX_MUL_LZERO;
                  COMPLEX_MUL_RZERO; COMPLEX_SUB_REFL; COMPLEX_VEC_0] THEN
  REWRITE_TAC[IN_NUMSEG] THEN ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* The simplest special case.                                                *)
(* ------------------------------------------------------------------------- *)


let COMPLEX_MVT = 
prove
 (`!f f' s B.
        convex s /\
        (!z. z IN s ==> (f has_complex_derivative f' z) (at z within s)) /\
        (!z. z IN s ==> norm (f' z) <= B)
        ==> !w z. w IN s /\ z IN s ==> norm (f z - f w) <= B * norm (z - w)`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPECL [`(\n. if n = 0 then f else f'):num->complex->complex`;
                `0`; `s:complex->bool`; `B:real`] COMPLEX_TAYLOR) THEN
  SIMP_TAC[NUMSEG_SING; VSUM_SING; LE; ARITH] THEN
  REWRITE_TAC[complex_pow; REAL_POW_1; FACT; REAL_DIV_1] THEN
  ASM_SIMP_TAC[COMPLEX_DIV_1; COMPLEX_MUL_RID]);;

(* ------------------------------------------------------------------------- *)
(* Something more like the traditional MVT for real components.              *)
(* Could, perhaps should, sharpen this to derivatives inside the segment.    *)
(* ------------------------------------------------------------------------- *)


let COMPLEX_MVT_LINE = 
prove
 (`!f f' w z.
        (!u. u IN segment[w,z]
             ==> (f has_complex_derivative f'(u)) (at u))
        ==> ?u. u IN segment[w,z] /\ Re(f z) - Re(f w) = Re(f'(u) * (z - w))`,

  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL
   [`(lift o Re) o (f:complex->complex) o
     (\t. (&1 - drop t) % w + drop t % z)`;
    `\u. (lift o Re) o
         (\h. (f':complex->complex)((&1 - drop u) % w + drop u % z) * h) o
         (\t. drop t % (z - w))`;
    `vec 0:real^1`; `vec 1:real^1`]
        MVT_VERY_SIMPLE) THEN
  ANTS_TAC THENL
   [REWRITE_TAC[DROP_VEC; REAL_POS] THEN
    X_GEN_TAC `t:real^1` THEN STRIP_TAC THEN
    MATCH_MP_TAC HAS_DERIVATIVE_AT_WITHIN THEN
    MATCH_MP_TAC DIFF_CHAIN_AT THEN CONJ_TAC THENL
     [ALL_TAC;
      MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
      REWRITE_TAC[linear; LIFT_ADD; RE_ADD; LIFT_CMUL; RE_CMUL; o_DEF]] THEN
    MATCH_MP_TAC DIFF_CHAIN_AT THEN CONJ_TAC THENL
     [REWRITE_TAC[VECTOR_ARITH `(&1 - t) % w + t % z = w + t % (z - w)`] THEN
      GEN_REWRITE_TAC (RATOR_CONV o RAND_CONV o ABS_CONV)
        [GSYM VECTOR_ADD_LID] THEN
      MATCH_MP_TAC HAS_DERIVATIVE_ADD THEN
      REWRITE_TAC[HAS_DERIVATIVE_CONST] THEN
      MATCH_MP_TAC HAS_DERIVATIVE_LINEAR THEN
      REWRITE_TAC[linear; DROP_ADD; DROP_CMUL] THEN
      CONJ_TAC THEN VECTOR_ARITH_TAC;
      ALL_TAC] THEN
    REWRITE_TAC[GSYM has_complex_derivative] THEN
    FIRST_X_ASSUM MATCH_MP_TAC;
    REWRITE_TAC[o_THM; GSYM LIFT_SUB; LIFT_EQ; DROP_VEC; VECTOR_SUB_RZERO] THEN
    CONV_TAC REAL_RAT_REDUCE_CONV THEN
    REWRITE_TAC[VECTOR_MUL_LID; VECTOR_MUL_LZERO] THEN
    REWRITE_TAC[VECTOR_ADD_LID; VECTOR_ADD_RID] THEN
    DISCH_THEN(X_CHOOSE_THEN `t:real^1` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `(&1 - drop t) % w + drop t % z:complex`] THEN
  ASM_REWRITE_TAC[segment; IN_ELIM_THM] THEN
  EXISTS_TAC `drop t` THEN ASM_REWRITE_TAC[] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_INTERVAL_1]) THEN
  REWRITE_TAC[DROP_VEC]);;


let COMPLEX_TAYLOR_MVT = 
prove
 (`!f w z n.
    (!i x. x IN segment[w,z] /\ i <= n
           ==> ((f i) has_complex_derivative f (i + 1) x) (at x))
    ==> ?u. u IN segment[w,z] /\
            Re(f 0 z) =
            Re(vsum (0..n) (\i. f i w * (z - w) pow i / Cx(&(FACT i))) +
               (f (n + 1) u * (z - u) pow n / Cx (&(FACT n))) * (z - w))`,

  
let lemma = prove
   (`!f:num->real^N.
          vsum (0..n) f = f 0 - f (n + 1) + vsum (0..n) (\i. f (i + 1))`,
    REWRITE_TAC[GSYM(REWRITE_CONV[o_DEF] `(f:num->real^N) o (\i. i + 1)`)] THEN
    ASM_SIMP_TAC[GSYM VSUM_IMAGE; EQ_ADD_RCANCEL; FINITE_NUMSEG] THEN
    REWRITE_TAC[GSYM NUMSEG_OFFSET_IMAGE] THEN
    SIMP_TAC[VSUM_CLAUSES_LEFT; LE_0] THEN
    REWRITE_TAC[VSUM_CLAUSES_NUMSEG; GSYM ADD1] THEN
    REWRITE_TAC[ARITH; ARITH_RULE `1 <= SUC n`] THEN VECTOR_ARITH_TAC) in
  REPEAT STRIP_TAC THEN MP_TAC(SPECL
   [`(\w. vsum (0..n) (\i. f i w * (z - w) pow i / Cx(&(FACT i))))`;
    `\w. (f:num->complex->complex) (n + 1) w *
         (z - w) pow n / Cx(&(FACT n))`;
    `w:complex`; `z:complex`]
    COMPLEX_MVT_LINE) THEN
  ANTS_TAC THENL
   [ASM_REWRITE_TAC[CONVEX_SEGMENT] THEN X_GEN_TAC `u:complex` THEN
    DISCH_TAC THEN
    SUBGOAL_THEN
     `((\u. vsum (0..n) (\i. f i u * (z - u) pow i / Cx (&(FACT i))))
       has_complex_derivative
       vsum (0..n) (\i. f i u * (-- Cx(&i) * (z - u) pow (i - 1)) /
                                Cx(&(FACT i)) +
                        f (i + 1) u * (z - u) pow i / Cx (&(FACT i))))
      (at u)`
    MP_TAC THENL
     [MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_VSUM THEN
      REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN REPEAT STRIP_TAC THEN
      MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_MUL_AT THEN
      ASM_SIMP_TAC[ETA_AX] THEN W(MP_TAC o COMPLEX_DIFF_CONV o snd) THEN
      MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN AP_TERM_TAC THEN
      REWRITE_TAC[complex_div] THEN CONV_TAC COMPLEX_RING;
      ALL_TAC] THEN
    ASM_SIMP_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
    AP_TERM_TAC THEN REWRITE_TAC[VSUM_ADD_NUMSEG] THEN
    GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [lemma] THEN
    REWRITE_TAC[GSYM VSUM_ADD_NUMSEG; GSYM COMPLEX_ADD_ASSOC] THEN
    REWRITE_TAC[ADD_SUB] THEN REWRITE_TAC[GSYM ADD1; FACT] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_SUC; GSYM REAL_OF_NUM_MUL; CX_MUL] THEN
    REWRITE_TAC[complex_div; COMPLEX_INV_MUL; GSYM COMPLEX_MUL_ASSOC] THEN
    REWRITE_TAC[COMPLEX_RING
      `--a * b * inv a * c:complex = --(a * inv a) * b * c`] THEN
    SIMP_TAC[COMPLEX_MUL_RINV; CX_INJ; REAL_ARITH `~(&n + &1 = &0)`] THEN
    REWRITE_TAC[COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; COMPLEX_MUL_LID] THEN
    REWRITE_TAC[COMPLEX_ADD_LINV; GSYM COMPLEX_VEC_0; VSUM_0] THEN
    REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_ADD_RID] THEN
    REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO; COMPLEX_NEG_0] THEN
    CONV_TAC COMPLEX_RING;
    ALL_TAC] THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `u:complex` THEN
  MATCH_MP_TAC MONO_AND THEN REWRITE_TAC[RE_ADD] THEN
  REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_EQ_SUB_RADD] THEN
  DISCH_THEN(SUBST1_TAC o SYM) THEN
  SIMP_TAC[VSUM_CLAUSES_LEFT; LE_0; complex_pow; FACT; COMPLEX_DIV_1] THEN
  REWRITE_TAC[COMPLEX_MUL_RID; RE_ADD] THEN
  MATCH_MP_TAC(REAL_ARITH `Re x = &0 ==> y = y + Re x`) THEN
  SIMP_TAC[RE_VSUM; FINITE_NUMSEG] THEN
  MATCH_MP_TAC SUM_EQ_0_NUMSEG THEN
  INDUCT_TAC THEN REWRITE_TAC[ARITH] THEN
  REWRITE_TAC[COMPLEX_SUB_REFL; complex_pow; complex_div] THEN
  REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_MUL_RZERO; RE_CX]);;

(* ------------------------------------------------------------------------- *)
(* Further useful properties of complex conjugation.                         *)
(* ------------------------------------------------------------------------- *)


let LIM_CNJ = 
prove
 (`!net f l. ((\x. cnj(f x)) --> cnj l) net <=> (f --> l) net`,

  REWRITE_TAC[LIM; dist; GSYM CNJ_SUB; COMPLEX_NORM_CNJ]);;


let SUMS_CNJ = 
prove
 (`!net f l. ((\x. cnj(f x)) sums cnj l) net <=> (f sums l) net`,

  SIMP_TAC[sums; LIM_CNJ; GSYM CNJ_VSUM; FINITE_INTER_NUMSEG]);;


let CONTINUOUS_WITHIN_CNJ = 
prove
 (`!s z. cnj continuous (at z within s)`,


let CONTINUOUS_AT_CNJ = 
prove
 (`!z. cnj continuous (at z)`,


let CONTINUOUS_ON_CNJ = 
prove
 (`!s. cnj continuous_on s`,

(* ------------------------------------------------------------------------- *)
(* Some limit theorems about real part of real series etc.                   *)
(* ------------------------------------------------------------------------- *)


let REAL_LIM = 
prove
 (`!net:(A)net f l.
        (f --> l) net /\ ~(trivial_limit net) /\
        (?b. (?a. netord net a b) /\ !a. netord net a b ==> real(f a))
        ==> real l`,

  REWRITE_TAC[IM_DEF; real] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC LIM_COMPONENT_EQ THEN
  REWRITE_TAC[eventually; DIMINDEX_2; ARITH] THEN ASM_MESON_TAC[]);;


let REAL_LIM_SEQUENTIALLY = 
prove
 (`!f l. (f --> l) sequentially /\ (?N. !n. n >= N ==> real(f n))
         ==> real l`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC(ISPEC `sequentially` REAL_LIM) THEN
  REWRITE_TAC[SEQUENTIALLY; TRIVIAL_LIMIT_SEQUENTIALLY] THEN
  ASM_MESON_TAC[GE_REFL]);;


let REAL_SERIES = 
prove
 (`!f l s. (f sums l) s /\ (!n. real(f n)) ==> real l`,

  REWRITE_TAC[sums] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC REAL_LIM_SEQUENTIALLY THEN
  EXISTS_TAC `\n. vsum(s INTER (0..n)) f :complex` THEN
  ASM_SIMP_TAC[REAL_VSUM; FINITE_INTER; FINITE_NUMSEG]);;

(* ------------------------------------------------------------------------- *)
(* Often convenient to use comparison with real limit of complex type.       *)
(* ------------------------------------------------------------------------- *)


let LIM_NULL_COMPARISON_COMPLEX = 
prove
 (`!net:(A)net f g.
        eventually (\x. norm(f x) <= norm(g x)) net /\
        (g --> Cx(&0)) net
        ==> (f --> Cx(&0)) net`,

  REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN REPEAT STRIP_TAC THEN
  MATCH_MP_TAC(ISPEC `net:(A)net` LIM_NULL_COMPARISON) THEN
  EXISTS_TAC `norm o (g:A->complex)` THEN
  ASM_REWRITE_TAC[o_THM; GSYM LIM_NULL_NORM]);;


let LIM_NULL_COMPARISON_COMPLEX_RE = 
prove
 (`!net:(A)net f g.
        eventually (\x. norm(f x) <= Re(g x)) net /\
        (g --> Cx(&0)) net
        ==> (f --> Cx(&0)) net`,

  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC(ISPEC `net:(A)net` LIM_NULL_COMPARISON_COMPLEX) THEN
  EXISTS_TAC `g:A->complex` THEN ASM_REWRITE_TAC[] THEN
  FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP
   (REWRITE_RULE[IMP_CONJ_ALT] EVENTUALLY_MONO)) THEN
  REWRITE_TAC[] THEN
  MESON_TAC[COMPLEX_NORM_GE_RE_IM; REAL_ABS_LE; REAL_LE_TRANS]);;


let SERIES_COMPARISON_COMPLEX = 
prove
 (`!f:num->real^N g s.
        summable s g /\
        (!n. n IN s ==> real(g n) /\ &0 <= Re(g n)) /\
        (?N. !n. n >= N /\ n IN s ==> norm(f n) <= norm(g n))
        ==> summable s f`,

  REPEAT GEN_TAC THEN REWRITE_TAC[summable] THEN
  DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  MATCH_MP_TAC SERIES_COMPARISON THEN
  EXISTS_TAC `\n. norm((g:num->complex) n)` THEN ASM_REWRITE_TAC[] THEN
  FIRST_X_ASSUM(X_CHOOSE_THEN `l:complex` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `lift(Re l)` THEN MATCH_MP_TAC SUMS_EQ THEN
  EXISTS_TAC `\i:num. lift(Re(g i))` THEN
  ASM_SIMP_TAC[REAL_NORM_POS; o_DEF] THEN
  REWRITE_TAC[RE_DEF] THEN MATCH_MP_TAC SERIES_COMPONENT THEN
  ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;


let SERIES_COMPARISON_UNIFORM_COMPLEX = 
prove
 (`!f:A->num->real^N g P s.
        summable s g /\
        (!n. n IN s ==> real(g n) /\ &0 <= Re(g n)) /\
        (?N. !n x. N <= n /\ n IN s /\ P x ==> norm(f x n) <= norm(g n))
        ==> ?l. !e. &0 < e
                    ==> ?N. !n x. N <= n /\ P x
                                  ==> dist(vsum(s INTER (0..n)) (f x),l x) <
                                       e`,

  REPEAT GEN_TAC THEN REWRITE_TAC[summable] THEN
  DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
  MATCH_MP_TAC SERIES_COMPARISON_UNIFORM THEN
  EXISTS_TAC `\n. norm((g:num->complex) n)` THEN ASM_REWRITE_TAC[] THEN
  FIRST_X_ASSUM(X_CHOOSE_THEN `l:complex` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `lift(Re l)` THEN MATCH_MP_TAC SUMS_EQ THEN
  EXISTS_TAC `\i:num. lift(Re(g i))` THEN
  ASM_SIMP_TAC[REAL_NORM_POS; o_DEF] THEN
  REWRITE_TAC[RE_DEF] THEN MATCH_MP_TAC SERIES_COMPONENT THEN
  ASM_REWRITE_TAC[DIMINDEX_2; ARITH]);;


let SUMMABLE_SUBSET_COMPLEX = 
prove
 (`!x s t. (!n. n IN s ==> real(x n) /\ &0 <= Re(x n)) /\
           summable s x /\ t SUBSET s
           ==> summable t x`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC SUMMABLE_SUBSET THEN
  EXISTS_TAC `s:num->bool` THEN ASM_REWRITE_TAC[] THEN
  MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
  EXISTS_TAC `x:num->complex` THEN ASM_REWRITE_TAC[] THEN
  MESON_TAC[REAL_LE_REFL; NORM_0; NORM_POS_LE]);;


let SERIES_ABSCONV_IMP_CONV = 
prove
 (`!x:num->real^N k. summable k (\n. Cx(norm(x n))) ==> summable k x`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
  EXISTS_TAC `\n:num. Cx(norm(x n:real^N))` THEN
  ASM_REWRITE_TAC[REAL_CX; RE_CX; NORM_POS_LE; COMPLEX_NORM_CX] THEN
  REWRITE_TAC[REAL_ABS_NORM; REAL_LE_REFL]);;

(* ------------------------------------------------------------------------- *)
(* Complex-valued geometric series.                                          *)
(* ------------------------------------------------------------------------- *)


let SUMS_GP = 
prove
 (`!n z. norm(z) < &1
         ==> ((\k. z pow k) sums (z pow n / (Cx(&1) - z))) (from n)`,

  REPEAT STRIP_TAC THEN REWRITE_TAC[SERIES_FROM; VSUM_GP] THEN
  ASM_CASES_TAC `z = Cx(&1)` THENL
   [ASM_MESON_TAC[COMPLEX_NORM_NUM; REAL_LT_REFL]; ALL_TAC] THEN
  MATCH_MP_TAC LIM_TRANSFORM_EVENTUALLY THEN
  EXISTS_TAC `\m. (z pow n - z pow SUC m) / (Cx (&1) - z)` THEN CONJ_TAC THENL
   [ASM_REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN
    EXISTS_TAC `n:num` THEN SIMP_TAC[GSYM NOT_LE];
    MATCH_MP_TAC LIM_COMPLEX_DIV THEN
    ASM_REWRITE_TAC[COMPLEX_SUB_0; LIM_CONST] THEN
    GEN_REWRITE_TAC (RATOR_CONV o RAND_CONV) [GSYM COMPLEX_SUB_RZERO] THEN
    MATCH_MP_TAC LIM_SUB THEN REWRITE_TAC[LIM_CONST] THEN
    REWRITE_TAC[LIM_SEQUENTIALLY; GSYM COMPLEX_VEC_0] THEN
    REWRITE_TAC[NORM_ARITH `dist(x,vec 0) = norm x`] THEN
    X_GEN_TAC `e:real` THEN DISCH_TAC THEN
    MP_TAC(SPECL [`norm(z:complex)`; `e:real`] REAL_ARCH_POW_INV) THEN
    ASM_REWRITE_TAC[] THEN MATCH_MP_TAC MONO_EXISTS THEN
    X_GEN_TAC `n:num` THEN DISCH_TAC THEN X_GEN_TAC `m:num` THEN DISCH_TAC THEN
    FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
     `x < e ==> y <= x ==> y < e`)) THEN
    REWRITE_TAC[COMPLEX_NORM_POW] THEN MATCH_MP_TAC REAL_POW_MONO_INV THEN
    ASM_SIMP_TAC[NORM_POS_LE; REAL_LT_IMP_LE] THEN
    UNDISCH_TAC `n:num <= m` THEN ARITH_TAC]);;


let SUMMABLE_GP = 
prove
 (`!z k. norm(z) < &1 ==> summable k (\n. z pow n)`,

  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC SUMMABLE_SUBSET THEN EXISTS_TAC `(:num)` THEN
  REWRITE_TAC[SUBSET_UNIV] THEN
  MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
  EXISTS_TAC `\n. Cx(norm(z:complex) pow n)` THEN
  REWRITE_TAC[REAL_CX; RE_CX; COMPLEX_NORM_CX] THEN
  SIMP_TAC[REAL_POW_LE; NORM_POS_LE] THEN CONJ_TAC THENL
   [REWRITE_TAC[summable; GSYM FROM_0; CX_POW] THEN
    EXISTS_TAC `Cx(norm z) pow 0 / (Cx(&1) - Cx(norm(z:complex)))` THEN
    MATCH_MP_TAC SUMS_GP THEN
    ASM_REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NORM];
    EXISTS_TAC `0` THEN REPEAT STRIP_TAC THEN
    COND_CASES_TAC THEN
    ASM_SIMP_TAC[REAL_ABS_POW; REAL_ABS_NORM; REAL_LE_REFL; NORM_POS_LE;
                 COMPLEX_NORM_POW; NORM_0; REAL_ABS_POS; REAL_POW_LE]]);;

(* ------------------------------------------------------------------------- *)
(* Complex version (the usual one) of Dirichlet convergence test.            *)
(* ------------------------------------------------------------------------- *)


let SERIES_DIRICHLET_COMPLEX_GEN = 
prove
 (`!f g N k m p l.
        bounded {vsum (m..n) f | n IN (:num)} /\
        summable (from p) (\n. Cx(norm(g(n + 1) - g(n)))) /\
        ((\n. vsum(1..n) f * g(n + 1)) --> l) sequentially
        ==> summable (from k) (\n. f(n) * g(n))`,

  REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
  MATCH_MP_TAC SERIES_DIRICHLET_BILINEAR THEN
  MAP_EVERY EXISTS_TAC [`m:num`; `p:num`; `l:complex`] THEN
  ASM_REWRITE_TAC[BILINEAR_COMPLEX_MUL] THEN
  ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN ASM_REWRITE_TAC[] THEN
  FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [summable]) THEN
  REWRITE_TAC[summable; SERIES_CAUCHY] THEN
  SIMP_TAC[GSYM(REWRITE_RULE[o_DEF] LIFT_SUM); FINITE_NUMSEG; FINITE_INTER;
           VSUM_CX; NORM_LIFT; COMPLEX_NORM_CX]);;


let SERIES_DIRICHLET_COMPLEX = 
prove
 (`!f g N k m.
        bounded {vsum (m..n) f | n IN (:num)} /\
        (!n. real(g n)) /\
        (!n. N <= n ==> Re(g(n + 1)) <= Re(g n)) /\
        (g --> Cx(&0)) sequentially
        ==> summable (from k) (\n. f(n) * g(n))`,

  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`f:num->complex`; `\n:num. Re(g n)`; `N:num`; `k:num`;
                 `m:num`] SERIES_DIRICHLET) THEN
  ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
   [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [LIM_SEQUENTIALLY]) THEN
    REWRITE_TAC[LIM_SEQUENTIALLY; o_THM; dist; VECTOR_SUB_RZERO] THEN
    REWRITE_TAC[COMPLEX_SUB_RZERO; NORM_LIFT] THEN
    MESON_TAC[COMPLEX_NORM_GE_RE_IM; REAL_LET_TRANS];
    MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC THEN
    REWRITE_TAC[COMPLEX_CMUL; FUN_EQ_THM] THEN
    ASM_MESON_TAC[REAL; COMPLEX_MUL_SYM]]);;

(* ------------------------------------------------------------------------- *)
(* Versions with explicit bounds are sometimes useful.                       *)
(* ------------------------------------------------------------------------- *)


let SERIES_DIRICHLET_COMPLEX_VERY_EXPLICIT = 
prove
 (`!f g B p.
        &0 < B /\ 1 <= p /\
        (!m n. p <= m ==> norm(vsum(m..n) f) <= B) /\
        (!n. p <= n ==> real(g n) /\ &0 <= Re(g n)) /\
        (!n. p <= n ==> Re(g(n + 1)) <= Re(g n))
        ==> !m n. p <= m
                  ==> norm(vsum(m..n) (\k. f k * g k)) <= &2 * B * norm(g m)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC
   `norm(vsum(m..n) (\k. (vsum(p..k) f - vsum(p..(k-1)) f) * g k))` THEN
  CONJ_TAC THENL
   [MATCH_MP_TAC REAL_EQ_IMP_LE THEN AP_TERM_TAC THEN
    MATCH_MP_TAC VSUM_EQ_NUMSEG THEN X_GEN_TAC `k:num` THEN STRIP_TAC THEN
    REWRITE_TAC[] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
    SUBGOAL_THEN `p:num <= k`
     (fun th -> SIMP_TAC[GSYM(MATCH_MP NUMSEG_RREC th)])
    THENL [ASM_ARITH_TAC; ALL_TAC] THEN
    SIMP_TAC[VSUM_CLAUSES; FINITE_NUMSEG; IN_NUMSEG] THEN
    COND_CASES_TAC THENL [ASM_ARITH_TAC; VECTOR_ARITH_TAC];
    ALL_TAC] THEN
  ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
  REWRITE_TAC[MATCH_MP BILINEAR_VSUM_PARTIAL_PRE BILINEAR_COMPLEX_MUL] THEN
  COND_CASES_TAC THEN
  ASM_SIMP_TAC[NORM_0; REAL_LE_MUL; REAL_POS; REAL_LT_IMP_LE; NORM_POS_LE] THEN
  MATCH_MP_TAC(NORM_ARITH
   `norm(c) <= e - norm(a) - norm(b) ==> norm(a - b - c) <= e`) THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC `sum (m..n) (\k. norm(g(k + 1) - g(k)) * B)` THEN CONJ_TAC THENL
   [MATCH_MP_TAC VSUM_NORM_LE THEN REWRITE_TAC[IN_NUMSEG; FINITE_NUMSEG] THEN
    X_GEN_TAC `k:num` THEN STRIP_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN
    MATCH_MP_TAC REAL_LE_MUL2 THEN
    ASM_SIMP_TAC[REAL_LE_REFL; LE_REFL; NORM_POS_LE];
    ALL_TAC] THEN
  MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC `sum(m..n) (\k. Re(g(k)) - Re(g(k + 1))) * B` THEN CONJ_TAC THENL
   [ASM_SIMP_TAC[SUM_RMUL; REAL_LE_RMUL_EQ] THEN
    MATCH_MP_TAC REAL_EQ_IMP_LE THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN
    X_GEN_TAC `i:num` THEN STRIP_TAC THEN
    SUBGOAL_THEN `p <= i /\ p <= i + 1` ASSUME_TAC THENL
     [ASM_ARITH_TAC; ALL_TAC] THEN
    ASM_SIMP_TAC[REAL_NORM; REAL_SUB; RE_SUB] THEN
    ASM_SIMP_TAC[REAL_ARITH `abs(x - y) = y - x <=> x <= y`];
    ALL_TAC] THEN
  ASM_REWRITE_TAC[SUM_DIFFS; COMPLEX_NORM_MUL] THEN
  MATCH_MP_TAC(REAL_ARITH
   `w * n1 <= w * B /\ z * n2 <= z * B /\ &0 <= B * (&2 * y - (x + w + z))
    ==> x * B <= &2 * B * y - w * n1 - z * n2`) THEN
  REPEAT(CONJ_TAC THENL
   [MATCH_MP_TAC REAL_LE_LMUL THEN
    ASM_SIMP_TAC[NORM_POS_LE; LE_REFL]; ALL_TAC]) THEN
  MATCH_MP_TAC REAL_LE_MUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN
  SUBGOAL_THEN
   `p <= m /\ p <= m + 1 /\ p <= n /\ p <= n + 1`
  STRIP_ASSUME_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
  ASM_SIMP_TAC[REAL_NORM; real_abs] THEN REAL_ARITH_TAC);;


let SERIES_DIRICHLET_COMPLEX_EXPLICIT = 
prove
 (`!f g p q.
           1 <= p /\
           bounded {vsum (q..n) f | n IN (:num)} /\
           (!n. p <= n ==> real(g n) /\ &0 <= Re(g n)) /\
           (!n. p <= n ==> Re(g(n + 1)) <= Re(g n))
           ==> ?B. &0 < B /\
                   !m n. p <= m
                         ==> norm(vsum(m..n) (\k. f k * g k))
                                 <= B * norm(g m)`,

  REWRITE_TAC[FORALL_AND_THM] THEN REPEAT STRIP_TAC THEN
  FIRST_X_ASSUM(MP_TAC o MATCH_MP BOUNDED_PARTIAL_SUMS) THEN
  SIMP_TAC[BOUNDED_POS; IN_ELIM_THM; IN_UNIV; LEFT_IMP_EXISTS_THM] THEN
  REWRITE_TAC[MESON[] `(!x a b. x = f a b ==> p a b) <=> (!a b. p a b)`] THEN
  X_GEN_TAC `B:real` THEN STRIP_TAC THEN EXISTS_TAC `&2 * B` THEN
  ASM_SIMP_TAC[GSYM REAL_MUL_ASSOC; REAL_LT_MUL; REAL_OF_NUM_LT; ARITH] THEN
  MATCH_MP_TAC SERIES_DIRICHLET_COMPLEX_VERY_EXPLICIT THEN
  ASM_SIMP_TAC[]);;

(* ------------------------------------------------------------------------- *)
(* Relations among convergence and absolute convergence for power series.    *)
(* ------------------------------------------------------------------------- *)


let ABEL_LEMMA = 
prove
 (`!a M r r0.
        &0 <= r /\ r < r0 /\
        (!n. n IN k ==> norm(a n) * r0 pow n <= M)
        ==> summable k (\n. Cx(norm(a(n)) * r pow n))`,

  REPEAT STRIP_TAC THEN
  SUBGOAL_THEN `&0 < r0` ASSUME_TAC THENL
   [ASM_REAL_ARITH_TAC; ALL_TAC] THEN
  ASM_CASES_TAC `k:num->bool = {}` THEN ASM_REWRITE_TAC[SUMMABLE_TRIVIAL] THEN
  SUBGOAL_THEN `&0 <= M` ASSUME_TAC THENL
   [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM MEMBER_NOT_EMPTY]) THEN
    DISCH_THEN(X_CHOOSE_TAC `i:num`) THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `i:num`) THEN ASM_REWRITE_TAC[] THEN
    MATCH_MP_TAC(REAL_ARITH `&0 <= x ==> x <= y ==> &0 <= y`) THEN
    MATCH_MP_TAC REAL_LE_MUL THEN
    ASM_SIMP_TAC[NORM_POS_LE; REAL_POW_LE; REAL_LT_IMP_LE];
    ALL_TAC] THEN
  MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
  EXISTS_TAC `\n. Cx(M * (r / r0) pow n)` THEN REPEAT CONJ_TAC THENL
   [REWRITE_TAC[CX_MUL; CX_POW] THEN MATCH_MP_TAC SUMMABLE_COMPLEX_LMUL THEN
    MATCH_MP_TAC SUMMABLE_GP THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN
    ASM_SIMP_TAC[REAL_ABS_DIV; real_abs; REAL_LT_IMP_LE] THEN
    ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_MUL_LID];
    REWRITE_TAC[REAL_CX; RE_CX] THEN
    REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN
    ASM_SIMP_TAC[REAL_LE_DIV; REAL_POW_LE; REAL_LT_IMP_LE];
    EXISTS_TAC `0` THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN REPEAT STRIP_TAC THEN
    REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NORM; REAL_ABS_DIV] THEN
    ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE; REAL_POW_DIV] THEN
    REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN
    ASM_SIMP_TAC[GSYM real_div; REAL_LE_RDIV_EQ; REAL_POW_LT] THEN
    ONCE_REWRITE_TAC[REAL_ARITH `(a * b) * c:real = (a * c) * b`] THEN
    ASM_SIMP_TAC[REAL_LE_RMUL; REAL_POW_LE; REAL_LT_IMP_LE]]);;


let POWER_SERIES_CONV_IMP_ABSCONV = 
prove
 (`!a k w z.
        summable k (\n. a(n) * z pow n) /\ norm(w) < norm(z)
        ==> summable k (\n. Cx(norm(a(n) * w pow n)))`,

  REPEAT STRIP_TAC THEN
  REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN
  MATCH_MP_TAC ABEL_LEMMA THEN
  FIRST_ASSUM(MP_TAC o MATCH_MP SUMMABLE_IMP_BOUNDED) THEN
  REWRITE_TAC[BOUNDED_POS; FORALL_IN_IMAGE] THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `B:real` THEN STRIP_TAC THEN
  EXISTS_TAC `norm(z:complex)` THEN REWRITE_TAC[NORM_POS_LE] THEN
  ASM_REWRITE_TAC[GSYM COMPLEX_NORM_POW; GSYM COMPLEX_NORM_MUL]);;


let POWER_SERIES_CONV_IMP_ABSCONV_WEAK = 
prove
 (`!a k w z.
        summable k (\n. a(n) * z pow n) /\ norm(w) < norm(z)
        ==> summable k (\n. Cx(norm(a(n))) * w pow n)`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC SERIES_COMPARISON_COMPLEX THEN
  EXISTS_TAC `\n. Cx(norm(a(n) * w pow n))` THEN CONJ_TAC THENL
   [MATCH_MP_TAC POWER_SERIES_CONV_IMP_ABSCONV THEN
    EXISTS_TAC `z:complex` THEN ASM_REWRITE_TAC[];
    ALL_TAC] THEN
  REWRITE_TAC[REAL_CX; RE_CX; NORM_POS_LE] THEN
  REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_CX; REAL_ABS_NORM;
              REAL_ABS_MUL; REAL_LE_REFL]);;

(* ------------------------------------------------------------------------- *)
(* Comparing sums and "integrals" via complex antiderivatives.               *)
(* ------------------------------------------------------------------------- *)


let SUM_INTEGRAL_UBOUND_INCREASING = 
prove
 (`!f g m n.
      m <= n /\
      (!x. x IN segment[Cx(&m),Cx(&n + &1)]
           ==> (g has_complex_derivative f(x)) (at x)) /\
      (!x y. &m <= x /\ x <= y /\ y <= &n + &1 ==> Re(f(Cx x)) <= Re(f(Cx y)))
      ==> sum(m..n) (\k. Re(f(Cx(&k)))) <= Re(g(Cx(&n + &1)) - g(Cx(&m)))`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN
  EXISTS_TAC `--sum(m..n) (\k. Re(g(Cx(&k))) - Re(g(Cx(&(k + 1)))))` THEN
  CONJ_TAC THENL
   [ALL_TAC;
    ASM_REWRITE_TAC[SUM_DIFFS; RE_SUB; REAL_NEG_SUB; REAL_OF_NUM_ADD] THEN
    REWRITE_TAC[REAL_LE_REFL]] THEN
  REWRITE_TAC[GSYM SUM_NEG] THEN MATCH_MP_TAC SUM_LE_NUMSEG THEN
  REWRITE_TAC[REAL_NEG_SUB] THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
  MP_TAC(ISPECL [`g:complex->complex`; `f:complex->complex`;
                 `Cx(&r)`; `Cx(&r + &1)`] COMPLEX_MVT_LINE) THEN
  ANTS_TAC THENL
   [X_GEN_TAC `u:complex` THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
    UNDISCH_TAC `u IN segment[Cx(&r),Cx(&r + &1)]` THEN
    REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
    SPEC_TAC(`u:complex`,`u:complex`) THEN REWRITE_TAC[GSYM SUBSET] THEN
    MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
    REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY; GSYM SEGMENT_CONVEX_HULL] THEN
    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[IN_SEGMENT_CX] THEN
    REWRITE_TAC[REAL_OF_NUM_ADD; REAL_OF_NUM_LE] THEN
    ASM_ARITH_TAC;
    REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN DISCH_THEN(X_CHOOSE_THEN `u:complex`
     (CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
    REWRITE_TAC[CX_ADD; COMPLEX_RING `y * ((x + Cx(&1)) - x) = y`] THEN
    SUBGOAL_THEN `?y. u = Cx y` (CHOOSE_THEN SUBST_ALL_TAC) THENL
     [ASM_MESON_TAC[REAL_SEGMENT; REAL_CX; REAL]; ALL_TAC] THEN
    FIRST_X_ASSUM MATCH_MP_TAC THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_SEGMENT_CX]) THEN
    REPEAT(FIRST_X_ASSUM
     (MP_TAC o GEN_REWRITE_RULE I [GSYM REAL_OF_NUM_LE])) THEN
    REAL_ARITH_TAC]);;


let SUM_INTEGRAL_UBOUND_DECREASING = 
prove
 (`!f g m n.
      m <= n /\
      (!x. x IN segment[Cx(&m - &1),Cx(&n)]
           ==> (g has_complex_derivative f(x)) (at x)) /\
      (!x y. &m - &1 <= x /\ x <= y /\ y <= &n ==> Re(f(Cx y)) <= Re(f(Cx x)))
      ==> sum(m..n) (\k. Re(f(Cx(&k)))) <= Re(g(Cx(&n)) - g(Cx(&m - &1)))`,

  REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC
   `--sum(m..n) (\k. Re(g(Cx(&(k) - &1))) - Re(g(Cx(&(k+1) - &1))))` THEN
  CONJ_TAC THENL
   [ALL_TAC;
    ASM_REWRITE_TAC[SUM_DIFFS; REAL_NEG_SUB] THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_SUB] THEN
    REWRITE_TAC[RE_SUB; REAL_ARITH `(x + &1) - &1 = x`; REAL_LE_REFL]] THEN
  REWRITE_TAC[GSYM SUM_NEG] THEN MATCH_MP_TAC SUM_LE_NUMSEG THEN
  REWRITE_TAC[REAL_NEG_SUB] THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ARITH `(x + &1) - &1 = x`] THEN
  MP_TAC(ISPECL [`g:complex->complex`; `f:complex->complex`;
                 `Cx(&r - &1)`; `Cx(&r)`] COMPLEX_MVT_LINE) THEN
  ANTS_TAC THENL
   [X_GEN_TAC `u:complex` THEN STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
    UNDISCH_TAC `u IN segment[Cx(&r - &1),Cx(&r)]` THEN
    REWRITE_TAC[SEGMENT_CONVEX_HULL] THEN
    SPEC_TAC(`u:complex`,`u:complex`) THEN REWRITE_TAC[GSYM SUBSET] THEN
    MATCH_MP_TAC HULL_MINIMAL THEN REWRITE_TAC[CONVEX_CONVEX_HULL] THEN
    REWRITE_TAC[SUBSET; IN_INSERT; NOT_IN_EMPTY; GSYM SEGMENT_CONVEX_HULL] THEN
    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[IN_SEGMENT_CX] THEN
    REPEAT(POP_ASSUM MP_TAC) THEN
    REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN REAL_ARITH_TAC;
    REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN DISCH_THEN(X_CHOOSE_THEN `u:complex`
     (CONJUNCTS_THEN2 ASSUME_TAC SUBST1_TAC)) THEN
    REWRITE_TAC[CX_SUB; COMPLEX_RING `y * (x - (x - Cx(&1))) = y`] THEN
    SUBGOAL_THEN `?y. u = Cx y` (CHOOSE_THEN SUBST_ALL_TAC) THENL
     [ASM_MESON_TAC[REAL_SEGMENT; REAL_CX; REAL]; ALL_TAC] THEN
    FIRST_X_ASSUM MATCH_MP_TAC THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [IN_SEGMENT_CX]) THEN
    REPEAT(FIRST_X_ASSUM
     (MP_TAC o GEN_REWRITE_RULE I [GSYM REAL_OF_NUM_LE])) THEN
    REAL_ARITH_TAC]);;


let SUM_INTEGRAL_LBOUND_INCREASING = 
prove
 (`!f g m n.
      m <= n /\
      (!x. x IN segment[Cx(&m - &1),Cx(&n)]
           ==> (g has_complex_derivative f(x)) (at x)) /\
      (!x y. &m - &1 <= x /\ x <= y /\ y <= &n ==> Re(f(Cx x)) <= Re(f(Cx y)))
      ==> Re(g(Cx(&n)) - g(Cx(&m - &1))) <= sum(m..n) (\k. Re(f(Cx(&k))))`,

  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`\z. --((f:complex->complex) z)`;
                 `\z. --((g:complex->complex) z)`;
                 `m:num`; `n:num`] SUM_INTEGRAL_UBOUND_DECREASING) THEN
  REWRITE_TAC[RE_NEG; RE_SUB; SUM_NEG; REAL_LE_NEG2;
              REAL_ARITH `--x - --y:real = --(x - y)`] THEN
  ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_NEG]);;


let SUM_INTEGRAL_LBOUND_DECREASING = 
prove
 (`!f g m n.
      m <= n /\
      (!x. x IN segment[Cx(&m),Cx(&n + &1)]
           ==> (g has_complex_derivative f(x)) (at x)) /\
      (!x y. &m <= x /\ x <= y /\ y <= &n + &1 ==> Re(f(Cx y)) <= Re(f(Cx x)))
      ==> Re(g(Cx(&n + &1)) - g(Cx(&m))) <= sum(m..n) (\k. Re(f(Cx(&k))))`,

  REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`\z. --((f:complex->complex) z)`;
                 `\z. --((g:complex->complex) z)`;
                 `m:num`; `n:num`] SUM_INTEGRAL_UBOUND_INCREASING) THEN
  REWRITE_TAC[RE_NEG; RE_SUB; SUM_NEG; REAL_LE_NEG2;
              REAL_ARITH `--x - --y:real = --(x - y)`] THEN
  ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_NEG]);;


let SUM_INTEGRAL_BOUNDS_INCREASING = 
prove
 (`!f g m n.
         m <= n /\
         (!x. x IN segment[Cx(&m - &1),Cx (&n + &1)]
              ==> (g has_complex_derivative f x) (at x)) /\
         (!x y.
              &m - &1 <= x /\ x <= y /\ y <= &n + &1
              ==> Re(f(Cx x)) <= Re(f(Cx y)))
         ==> Re(g(Cx(&n)) - g(Cx(&m - &1))) <= sum(m..n) (\k. Re(f(Cx(&k)))) /\
             sum (m..n) (\k. Re(f(Cx(&k)))) <= Re(g(Cx(&n + &1)) - g(Cx(&m)))`,

  REPEAT STRIP_TAC THENL
   [MATCH_MP_TAC SUM_INTEGRAL_LBOUND_INCREASING;
    MATCH_MP_TAC SUM_INTEGRAL_UBOUND_INCREASING] THEN
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  FIRST_X_ASSUM MATCH_MP_TAC THEN
  RULE_ASSUM_TAC(REWRITE_RULE[IN_SEGMENT_CX_GEN; GSYM REAL_OF_NUM_LE]) THEN
  REWRITE_TAC[IN_SEGMENT_CX_GEN] THEN ASM_REAL_ARITH_TAC);;


let SUM_INTEGRAL_BOUNDS_DECREASING = 
prove
 (`!f g m n.
      m <= n /\
      (!x. x IN segment[Cx(&m - &1),Cx(&n + &1)]
           ==> (g has_complex_derivative f(x)) (at x)) /\
      (!x y. &m - &1 <= x /\ x <= y /\ y <= &n + &1
             ==> Re(f(Cx y)) <= Re(f(Cx x)))
      ==> Re(g(Cx(&n + &1)) - g(Cx(&m))) <= sum(m..n) (\k. Re(f(Cx(&k)))) /\
          sum(m..n) (\k. Re(f(Cx(&k)))) <= Re(g(Cx(&n)) - g(Cx(&m - &1)))`,

  REPEAT STRIP_TAC THENL
   [MATCH_MP_TAC SUM_INTEGRAL_LBOUND_DECREASING;
    MATCH_MP_TAC SUM_INTEGRAL_UBOUND_DECREASING] THEN
  REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
  FIRST_X_ASSUM MATCH_MP_TAC THEN
  RULE_ASSUM_TAC(REWRITE_RULE[IN_SEGMENT_CX_GEN; GSYM REAL_OF_NUM_LE]) THEN
  REWRITE_TAC[IN_SEGMENT_CX_GEN] THEN ASM_REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Relating different kinds of complex limits.                               *)
(* ------------------------------------------------------------------------- *)


let LIM_INFINITY_SEQUENTIALLY_COMPLEX = 
prove
 (`!f l. (f --> l) at_infinity ==> ((\n. f(Cx(&n))) --> l) sequentially`,

  REPEAT GEN_TAC THEN REWRITE_TAC[LIM_AT_INFINITY; LIM_SEQUENTIALLY] THEN
  DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(X_CHOOSE_TAC `B:real`) THEN
  MP_TAC(ISPEC `B:real` REAL_ARCH_SIMPLE) THEN
  MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
  REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
  REWRITE_TAC[COMPLEX_NORM_CX] THEN
  REPEAT(POP_ASSUM MP_TAC) THEN
  REWRITE_TAC[GSYM REAL_OF_NUM_LE] THEN REAL_ARITH_TAC);;


let LIM_ZERO_INFINITY_COMPLEX = 
prove
 (`!f l. ((\x. f(Cx(&1) / x)) --> l) (at (Cx(&0))) ==> (f --> l) at_infinity`,

  REPEAT GEN_TAC THEN REWRITE_TAC[LIM_AT; LIM_AT_INFINITY] THEN
  DISCH_TAC THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN
  REWRITE_TAC[dist; COMPLEX_SUB_RZERO; real_ge] THEN
  DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
  EXISTS_TAC `&2 / d` THEN X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `inv(z):complex`) THEN
  REWRITE_TAC[complex_div; COMPLEX_MUL_LINV; COMPLEX_INV_INV] THEN
  REWRITE_TAC[COMPLEX_MUL_LID] THEN DISCH_THEN MATCH_MP_TAC THEN
  ASM_REWRITE_TAC[COMPLEX_NORM_INV; REAL_LT_INV_EQ] THEN CONJ_TAC THENL
   [UNDISCH_TAC `&2 / d <= norm(z:complex)` THEN
    ASM_CASES_TAC `z = Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_NORM_NZ] THEN
    REWRITE_TAC[COMPLEX_NORM_0; REAL_NOT_LE] THEN
    ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH];
    GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_INV] THEN
    MATCH_MP_TAC REAL_LT_INV2 THEN ASM_REWRITE_TAC[REAL_LT_INV_EQ] THEN
    MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 / d` THEN
    ASM_REWRITE_TAC[] THEN REWRITE_TAC[real_div] THEN
    ASM_REWRITE_TAC[REAL_LT_INV_EQ; REAL_ARITH `x < &2 * x <=> &0 < x`]]);;

(* ------------------------------------------------------------------------- *)
(* Transforming complex limits to real ones.                                 *)
(* ------------------------------------------------------------------------- *)


let LIM_COMPLEX_REAL = 
prove
 (`!f g l m.
         eventually (\n. Re(g n) = f n) sequentially /\
         Re m = l /\
         (g --> m) sequentially
         ==> !e. &0 < e ==> ?N. !n. N <= n ==> abs(f n - l) < e`,

  REPEAT GEN_TAC THEN
  REWRITE_TAC[EVENTUALLY_SEQUENTIALLY; LIM_SEQUENTIALLY] THEN
  DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `N1:num`)
   (CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC)) THEN
  X_GEN_TAC `e:real` THEN DISCH_TAC THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[dist] THEN
  DISCH_THEN(X_CHOOSE_TAC `N0:num`) THEN EXISTS_TAC `N0 + N1:num` THEN
  X_GEN_TAC `n:num` THEN DISCH_THEN(STRIP_ASSUME_TAC o MATCH_MP (ARITH_RULE
   `N0 + N1:num <= n ==> N0 <= n /\ N1 <= n`)) THEN
  UNDISCH_THEN `!n. N0 <= n ==> norm ((g:num->complex) n - m) < e`
   (MP_TAC o SPEC `n:num`) THEN
  FIRST_X_ASSUM(MP_TAC o SPEC `n:num`) THEN ASM_REWRITE_TAC[] THEN
  DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[GSYM RE_SUB] THEN
  MATCH_MP_TAC(REAL_ARITH `x <= y ==> y < e ==> x < e`) THEN
  REWRITE_TAC[COMPLEX_NORM_GE_RE_IM]);;


let LIM_COMPLEX_REAL_0 = 
prove
 (`!f g. eventually (\n. Re(g n) = f n) sequentially /\
         (g --> Cx(&0)) sequentially
         ==> !e. &0 < e ==> ?N. !n. N <= n ==> abs(f n) < e`,

  MP_TAC LIM_COMPLEX_REAL THEN
  REPLICATE_TAC 2 (MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
  DISCH_THEN(MP_TAC o SPECL [`&0`; `Cx(&0)`]) THEN
  REWRITE_TAC[RE_CX; REAL_SUB_RZERO]);;

(* ------------------------------------------------------------------------- *)
(* Uniform convergence of power series in a "Stolz angle".                   *)
(* ------------------------------------------------------------------------- *)


let POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ_1 = 
prove
 (`!M a s e.
        summable s a /\ &0 < M /\ &0 < e
        ==> eventually
             (\n. !z. norm(Cx(&1) - z) <= M * (&1 - norm z)
                      ==> norm(vsum (s INTER (0..n)) (\i. a i * z pow i) -
                               infsum s (\i. a i * z pow i)) < e)
             sequentially`,

  
let lemma = prove
   (`!M w z. &0 < M /\ norm(w - z) <= M * (norm w - norm z) /\ ~(z = w)
             ==> norm(z) < norm(w)`,
    REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN CONJ_TAC THENL
     [ASM_MESON_TAC[REAL_LE_MUL_EQ; REAL_SUB_LE; NORM_POS_LE; REAL_LE_TRANS];
      DISCH_THEN SUBST_ALL_TAC THEN
      ASM_MESON_TAC[REAL_SUB_REFL; REAL_MUL_RZERO;NORM_LE_0; VECTOR_SUB_EQ]])
  and lemma1 = prove
   (`!m n. m < n
           ==> vsum (m..n) (\i. a i * z pow i) =
               (Cx(&1) - z) * vsum(m..n-1) (\i. vsum (m..i) a * z pow i) +
               vsum(m..n) a * z pow n`,
    GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; SUC_SUB1] THEN
    SIMP_TAC[VSUM_CLAUSES_NUMSEG; LT; LT_IMP_LE] THEN STRIP_TAC THENL
     [ASM_REWRITE_TAC[VSUM_SING_NUMSEG; complex_pow] THEN CONV_TAC COMPLEX_RING;
      ASM_SIMP_TAC[] THEN UNDISCH_TAC `m:num < n` THEN
      POP_ASSUM(K ALL_TAC)] THEN
    SPEC_TAC(`n:num`,`n:num`) THEN
    INDUCT_TAC THEN REWRITE_TAC[CONJUNCT1 LT] THEN POP_ASSUM(K ALL_TAC) THEN
    SIMP_TAC[SUC_SUB1; VSUM_CLAUSES_NUMSEG; LT_IMP_LE] THEN
    ASM_REWRITE_TAC[VSUM_SING_NUMSEG; complex_pow] THEN
    CONV_TAC COMPLEX_RING) in
  SUBGOAL_THEN
   `!M a e.
        summable (:num) a /\ &0 < M /\ &0 < e
        ==> eventually
             (\n. !z. norm(Cx(&1) - z) <= M * (&1 - norm z)
                      ==> norm(vsum (0..n) (\i. a i * z pow i) -
                               infsum (:num) (\i. a i * z pow i)) < e)
             sequentially`
  ASSUME_TAC THENL
   [ALL_TAC;
    REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o ISPECL
     [`M:real`; `\i:num. if i IN s then a i else Cx(&0)`; `e:real`]) THEN
    REWRITE_TAC[COND_RAND; COND_RATOR; COMPLEX_MUL_LZERO] THEN
    ASM_REWRITE_TAC[GSYM COMPLEX_VEC_0; GSYM VSUM_RESTRICT_SET;
                    INFSUM_RESTRICT; SUMMABLE_RESTRICT] THEN
    REWRITE_TAC[SET_RULE `{i | i IN t /\ i IN s} = s INTER t`]] THEN
  REPEAT STRIP_TAC THEN
  ONCE_REWRITE_TAC[MESON[]
   `(!z. P z) <=> P (Cx(&1)) /\ (!z. ~(z = Cx(&1)) ==> P z)`] THEN
  REWRITE_TAC[EVENTUALLY_AND] THEN CONJ_TAC THENL
   [REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM; COMPLEX_SUB_REFL;
                REAL_SUB_REFL; REAL_MUL_RZERO; REAL_LE_REFL] THEN
    UNDISCH_TAC `&0 < e` THEN SPEC_TAC(`e:real`,`e:real`) THEN
    REWRITE_TAC[GSYM tendsto; COMPLEX_POW_ONE; COMPLEX_MUL_RID; GSYM dist;
                ETA_AX] THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM SUMS_INFSUM]) THEN
    REWRITE_TAC[sums; INTER_UNIV];
    ALL_TAC] THEN
  REWRITE_TAC[IMP_IMP; EVENTUALLY_SEQUENTIALLY] THEN
  REWRITE_TAC[RIGHT_IMP_FORALL_THM; IMP_IMP; GSYM dist] THEN
  UNDISCH_TAC `&0 < e` THEN SPEC_TAC(`e:real`,`e:real`) THEN
  MATCH_MP_TAC UNIFORMLY_CAUCHY_IMP_UNIFORMLY_CONVERGENT THEN
  REWRITE_TAC[GSYM LIM_SEQUENTIALLY] THEN CONJ_TAC THENL
   [X_GEN_TAC `e:real` THEN DISCH_TAC THEN
    REWRITE_TAC[MESON[] `(!m n z. P m /\ P n /\ Q z ==> R m n z) <=>
                         (!z. Q z ==> !m n. P m /\ P n ==> R m n z)`] THEN
    FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM SUMS_INFSUM]) THEN
    REWRITE_TAC[sums] THEN
    DISCH_THEN(MP_TAC o MATCH_MP CONVERGENT_IMP_CAUCHY) THEN
    REWRITE_TAC[cauchy; GSYM dist] THEN
    DISCH_THEN(MP_TAC o SPEC `min (e / &2) (e / &2 / M)`) THEN
    ASM_SIMP_TAC[REAL_LT_MIN; REAL_LT_DIV; REAL_HALF; GE; INTER_UNIV] THEN
    REWRITE_TAC[GSYM REAL_LT_MIN] THEN
    ONCE_REWRITE_TAC[SEQUENCE_CAUCHY_WLOG] THEN
    SUBGOAL_THEN
     `!f:num->complex m n. m <= n
              ==> dist(vsum (0..m) f,vsum (0..n) f) = norm(vsum (m+1..n) f)`
     (fun th -> SIMP_TAC[th])
    THENL
     [REPEAT STRIP_TAC THEN
      MATCH_MP_TAC(NORM_ARITH `a + c = b ==> dist(a,b) = norm c`) THEN
      MATCH_MP_TAC VSUM_COMBINE_R THEN ASM_ARITH_TAC;
      ALL_TAC] THEN
    MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `N:num` THEN
    REWRITE_TAC[REAL_LT_MIN] THEN STRIP_TAC THEN
    X_GEN_TAC `z:complex` THEN REWRITE_TAC[dist] THEN STRIP_TAC THEN
    SUBGOAL_THEN `norm(z:complex) < &1` ASSUME_TAC THENL
     [UNDISCH_TAC `~(z = Cx(&1))` THEN
      ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
      REWRITE_TAC[NORM_POS_LT; VECTOR_SUB_EQ] THEN DISCH_TAC THEN
      FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (NORM_ARITH
       `norm(a - b) <= M ==> &0 <= --M ==> b = a`)) THEN
      REWRITE_TAC[GSYM REAL_MUL_RNEG; REAL_NEG_SUB] THEN
      MATCH_MP_TAC REAL_LE_MUL THEN ASM_REAL_ARITH_TAC;
      ALL_TAC] THEN
    MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
    ASM_CASES_TAC `m + 1 < n` THENL
     [ASM_SIMP_TAC[lemma1] THEN
      MATCH_MP_TAC(NORM_ARITH
       `norm(a) < e / &2 /\ norm(b) < e / &2 ==> norm(a + b) < e`) THEN
      REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN CONJ_TAC THENL
       [MATCH_MP_TAC REAL_LET_TRANS THEN
        EXISTS_TAC `(M * (&1 - norm(z:complex))) *
                    sum (m+1..n-1) (\i. e / &2 / M * norm(z) pow i)` THEN
        CONJ_TAC THENL
         [MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[NORM_POS_LE] THEN
          MATCH_MP_TAC VSUM_NORM_LE THEN
          REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
          X_GEN_TAC `p:num` THEN STRIP_TAC THEN
          ASM_SIMP_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN
          MATCH_MP_TAC REAL_LE_RMUL THEN
          SIMP_TAC[REAL_POW_LE; NORM_POS_LE] THEN
          MATCH_MP_TAC(REAL_ARITH
            `x < e / &2 /\ x < e / &2 / M ==> x <= e / &2 / M`) THEN
          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
          REWRITE_TAC[SUM_LMUL] THEN
          REWRITE_TAC[REAL_ARITH
           `(M * z1) * e / &2 / M * s < e / &2 <=>
            e * (M / M) * s * z1 < e * &1`] THEN
          ASM_SIMP_TAC[REAL_LT_LMUL_EQ] THEN
          ASM_SIMP_TAC[REAL_DIV_REFL; REAL_LT_IMP_NZ; REAL_MUL_LID] THEN
          ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_SUB_LT] THEN
          REWRITE_TAC[SUM_GP] THEN
          COND_CASES_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
          COND_CASES_TAC THENL
           [UNDISCH_TAC `norm(Cx(&1) - z) <= M * (&1 - norm z)` THEN
            ASM_REWRITE_TAC[REAL_SUB_REFL; REAL_MUL_RZERO] THEN
            ASM_REWRITE_TAC[NORM_ARITH `norm(x - y:complex) <= &0 <=> x = y`];
            ALL_TAC] THEN
          ASM_SIMP_TAC[REAL_LT_DIV2_EQ; REAL_SUB_LT] THEN
          MATCH_MP_TAC(REAL_ARITH
           `&0 <= y /\ x < &1 ==> x - y < &1`) THEN
          ASM_SIMP_TAC[REAL_POW_LE; NORM_POS_LE] THEN
          MATCH_MP_TAC REAL_POW_1_LT THEN
          ASM_REWRITE_TAC[NORM_POS_LE] THEN ARITH_TAC];
        GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
        MATCH_MP_TAC REAL_LT_MUL2 THEN SIMP_TAC[NORM_POS_LE; REAL_POW_LE] THEN
        CONJ_TAC THENL
         [MATCH_MP_TAC(REAL_ARITH
            `x < e / &2 /\ x < e / &2 / M ==> x < e / &2`) THEN
          FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC;
          MATCH_MP_TAC REAL_POW_1_LT THEN
          ASM_REWRITE_TAC[NORM_POS_LE] THEN ASM_ARITH_TAC]];
      ASM_CASES_TAC `(m+1)..n = {}` THENL
       [ASM_REWRITE_TAC[VSUM_CLAUSES; NORM_0]; ALL_TAC] THEN
      RULE_ASSUM_TAC(REWRITE_RULE[NUMSEG_EMPTY]) THEN
      SUBGOAL_THEN `m + 1 = n` SUBST1_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
      REWRITE_TAC[VSUM_SING_NUMSEG] THEN
      REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_POW] THEN
      GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
      MATCH_MP_TAC REAL_LT_MUL2 THEN SIMP_TAC[NORM_POS_LE; REAL_POW_LE] THEN
      CONJ_TAC THENL
       [FIRST_X_ASSUM(MP_TAC o SPECL [`m:num`; `n:num`]) THEN
        SUBGOAL_THEN `m + 1 = n` SUBST1_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
        ANTS_TAC THENL [ASM_ARITH_TAC; REWRITE_TAC[VSUM_SING_NUMSEG]] THEN
        ASM_REAL_ARITH_TAC;
        MATCH_MP_TAC REAL_POW_1_LT THEN
        ASM_REWRITE_TAC[NORM_POS_LE] THEN ASM_ARITH_TAC]];
    X_GEN_TAC `z:complex` THEN REWRITE_TAC[dist] THEN STRIP_TAC THEN
    MP_TAC(ISPECL [`M:real`; `Cx(&1)`; `z:complex`] lemma) THEN
    ASM_REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM] THEN DISCH_TAC THEN
    SUBGOAL_THEN `summable (:num) (\i. a i * z pow i)` MP_TAC THENL
     [MATCH_MP_TAC SERIES_ABSCONV_IMP_CONV THEN
      REWRITE_TAC[] THEN MATCH_MP_TAC POWER_SERIES_CONV_IMP_ABSCONV THEN
      EXISTS_TAC `Cx(&1)` THEN
      REWRITE_TAC[COMPLEX_POW_ONE; COMPLEX_NORM_CX] THEN
      ASM_REWRITE_TAC[REAL_ABS_NUM; COMPLEX_MUL_RID; ETA_AX];
      REWRITE_TAC[GSYM SUMS_INFSUM] THEN
      REWRITE_TAC[sums; INTER_UNIV]]]);;


let POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ = 
prove
 (`!M a w s e.
        summable s (\i. a i * w pow i) /\ &0 < M /\ &0 < e
        ==> eventually
             (\n. !z. norm(w - z) <= M * (norm w - norm z)
                      ==> norm(vsum (s INTER (0..n)) (\i. a i * z pow i) -
                               infsum s (\i. a i * z pow i)) < e)
             sequentially`,

  REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `w = Cx(&0)` THENL
   [ASM_REWRITE_TAC[COMPLEX_SUB_LZERO; REAL_SUB_LZERO; COMPLEX_NORM_0] THEN
    REWRITE_TAC[NORM_NEG; REAL_ARITH
      `n <= M * --n <=> &0 <= --n * (&1 + M)`] THEN
    ASM_SIMP_TAC[REAL_LE_MUL_EQ; REAL_ARITH `&0 < M ==> &0 < &1 + M`] THEN
    REWRITE_TAC[NORM_ARITH `&0 <= --norm z <=> z = vec 0`] THEN
    REWRITE_TAC[EVENTUALLY_SEQUENTIALLY; FORALL_UNWIND_THM2] THEN
    EXISTS_TAC `1` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
    REWRITE_TAC[COMPLEX_VEC_0; COMPLEX_POW_ZERO] THEN
    REWRITE_TAC[COND_RATOR; COND_RAND; COMPLEX_MUL_RZERO; COMPLEX_MUL_RID] THEN
    MATCH_MP_TAC(NORM_ARITH `x = y /\ &0 < e ==> norm(y - x) < e`) THEN
    ASM_REWRITE_TAC[] THEN MATCH_MP_TAC INFSUM_UNIQUE THEN
    REWRITE_TAC[sums] THEN MATCH_MP_TAC LIM_EVENTUALLY THEN
    REWRITE_TAC[EVENTUALLY_SEQUENTIALLY] THEN EXISTS_TAC `1` THEN
    X_GEN_TAC `m:num` THEN DISCH_TAC THEN
    SIMP_TAC[GSYM COMPLEX_VEC_0; VSUM_DELTA] THEN
    REWRITE_TAC[IN_INTER; LE_0; IN_NUMSEG];
    FIRST_ASSUM(MP_TAC o MATCH_MP POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ_1) THEN
    MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
    X_GEN_TAC `n:num` THEN REWRITE_TAC[] THEN DISCH_TAC THEN
    X_GEN_TAC `z:complex` THEN STRIP_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPEC `z / w:complex`) THEN
    ASM_SIMP_TAC[GSYM COMPLEX_MUL_ASSOC; GSYM COMPLEX_POW_MUL] THEN
    ASM_SIMP_TAC[COMPLEX_DIV_LMUL] THEN DISCH_THEN MATCH_MP_TAC THEN
    MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `norm(w:complex)` THEN
    ASM_REWRITE_TAC[COMPLEX_NORM_NZ; GSYM COMPLEX_NORM_MUL] THEN
    ASM_SIMP_TAC[COMPLEX_FIELD
     `~(w = Cx(&0)) ==> (Cx(&1) - z / w) * w = w - z`] THEN
    REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_SUB_RDISTRIB] THEN
    REWRITE_TAC[GSYM COMPLEX_NORM_MUL; REAL_MUL_LID] THEN
    ASM_SIMP_TAC[COMPLEX_DIV_RMUL]]);;

(* ------------------------------------------------------------------------- *)
(* Hence continuity and the Abel limit theorem.                              *)
(* ------------------------------------------------------------------------- *)


let ABEL_POWER_SERIES_CONTINUOUS = 
prove
 (`!M s a.
        summable s a /\ &0 < M
        ==> (\z. infsum s (\i. a i * z pow i)) continuous_on
            {z | norm(Cx(&1) - z) <= M * (&1 - norm z)}`,

  REPEAT STRIP_TAC THEN
  MATCH_MP_TAC(ISPEC `sequentially` CONTINUOUS_UNIFORM_LIMIT) THEN
  EXISTS_TAC `\n z. vsum (s INTER (0..n)) (\i. a i * z pow i)` THEN
  ASM_SIMP_TAC[POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ_1; IN_ELIM_THM;
               TRIVIAL_LIMIT_SEQUENTIALLY] THEN
  MATCH_MP_TAC ALWAYS_EVENTUALLY THEN X_GEN_TAC `n:num` THEN
  REWRITE_TAC[] THEN MATCH_MP_TAC CONTINUOUS_ON_VSUM THEN
  SIMP_TAC[CONTINUOUS_ON_COMPLEX_MUL; CONTINUOUS_ON_COMPLEX_POW;
           CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST; FINITE_INTER;
           FINITE_NUMSEG]);;


let ABEL_LIMIT_THEOREM = 
prove
 (`!M s a.
        summable s a /\ &0 < M
        ==> (!z. norm(z) < &1 ==> summable s (\i. a i * z pow i)) /\
            ((\z. infsum s (\i. a i * z pow i)) --> infsum s a)
            (at (Cx(&1)) within {z | norm(Cx(&1) - z) <= M * (&1 - norm z)})`,

  GEN_TAC THEN ASM_CASES_TAC `&0 < M` THEN ASM_REWRITE_TAC[] THEN
  SUBGOAL_THEN
   `!a. summable (:num) a
        ==> (!z. norm(z) < &1 ==> summable (:num) (\i. a i * z pow i)) /\
            ((\z. infsum (:num) (\i. a i * z pow i))
              --> infsum (:num) a)
            (at (Cx(&1)) within {z | norm(Cx(&1) - z) <= M * (&1 - norm z)})`
  ASSUME_TAC THENL
   [ALL_TAC;
    REPEAT GEN_TAC THEN STRIP_TAC THEN
    FIRST_X_ASSUM(MP_TAC o SPEC
     `(\n. if n IN s then a n else vec 0):num->complex`) THEN
    REWRITE_TAC[COND_RAND; COND_RATOR; COMPLEX_VEC_0; COMPLEX_MUL_LZERO] THEN
    REWRITE_TAC[GSYM COMPLEX_VEC_0] THEN
    ASM_REWRITE_TAC[SUMMABLE_RESTRICT; INFSUM_RESTRICT]] THEN
  GEN_TAC THEN STRIP_TAC THEN CONJ_TAC THENL
   [X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
    MATCH_MP_TAC SERIES_ABSCONV_IMP_CONV THEN
    REWRITE_TAC[] THEN MATCH_MP_TAC POWER_SERIES_CONV_IMP_ABSCONV THEN
    EXISTS_TAC `Cx(&1)` THEN REWRITE_TAC[COMPLEX_POW_ONE; COMPLEX_NORM_CX] THEN
    ASM_REWRITE_TAC[REAL_ABS_NUM; COMPLEX_MUL_RID; ETA_AX];
    MP_TAC(ISPECL [`M:real`; `(:num)`; `a:num->complex`]
       ABEL_POWER_SERIES_CONTINUOUS) THEN
    ASM_REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN] THEN
    DISCH_THEN(MP_TAC o SPEC `Cx(&1)`) THEN
    REWRITE_TAC[IN_ELIM_THM; CONTINUOUS_WITHIN] THEN
    REWRITE_TAC[COMPLEX_SUB_REFL; COMPLEX_NORM_CX; COMPLEX_POW_ONE;
                COMPLEX_MUL_RID; ETA_AX; REAL_ABS_NUM; REAL_SUB_REFL;
                REAL_LE_REFL; REAL_MUL_RZERO]]);;