# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1450190436 0
# Node ID 9250e546ab23f5c69895fa58833579ca2fb6cad8
# Parent  2c79790d270db445ca55a203a3a1ffb2a6ced565
New complex analysis material

diff -r 2c79790d270d -r 9250e546ab23 NEWS
--- a/NEWS	Mon Dec 14 14:05:31 2015 +0100
+++ b/NEWS	Tue Dec 15 14:40:36 2015 +0000
@@ -594,8 +594,8 @@
 fixpoint theorem for increasing functions in chain-complete partial
 orders.
 
-* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's
-integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
+* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals),
+Cauchy's integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
 
 * Multivariate_Analysis: Added topological concepts such as connected components,
 homotopic paths and the inside or outside of a set.
diff -r 2c79790d270d -r 9250e546ab23 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Dec 14 14:05:31 2015 +0100
+++ b/src/HOL/Complex.thy	Tue Dec 15 14:40:36 2015 +0000
@@ -784,7 +784,10 @@
   apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
   done
 
-lemma exp_two_pi_i [simp]: "exp(2 * complex_of_real pi * ii) = 1"
+lemma exp_pi_i [simp]: "exp(of_real pi * ii) = -1"
+  by (metis cis_conv_exp cis_pi mult.commute)
+
+lemma exp_two_pi_i [simp]: "exp(2 * of_real pi * ii) = 1"
   by (simp add: exp_eq_polar complex_eq_iff)
 
 subsubsection \<open>Complex argument\<close>
diff -r 2c79790d270d -r 9250e546ab23 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Dec 14 14:05:31 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Dec 15 14:40:36 2015 +0000
@@ -2674,7 +2674,7 @@
     done
 qed
 
-lemma pathintegral_convex_primitive:
+lemma contour_integral_convex_primitive:
   "\<lbrakk>convex s; continuous_on s f;
     \<And>a b c. \<lbrakk>a \<in> s; b \<in> s; c \<in> s\<rbrakk> \<Longrightarrow> (f has_contour_integral 0) (linepath a b +++ linepath b c +++ linepath c a)\<rbrakk>
          \<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
@@ -2687,7 +2687,7 @@
   "\<lbrakk>convex s; finite k; continuous_on s f;
     \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x\<rbrakk>
    \<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
-apply (rule pathintegral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite])
+apply (rule contour_integral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite])
 prefer 3
 apply (erule continuous_on_subset)
 apply (simp add: subset_hull continuous_on_subset, assumption+)
@@ -5029,6 +5029,35 @@
 lemma pathfinish_circlepath [simp]: "pathfinish (circlepath z r) = z + r"
   by (simp add: circlepath_def) (metis exp_two_pi_i mult.commute)
 
+lemma circlepath_minus: "circlepath z (-r) x = circlepath z r (x + 1/2)"
+proof -
+  have "z + of_real r * exp (2 * pi * \<i> * (x + 1 / 2)) =
+        z + of_real r * exp (2 * pi * \<i> * x + pi * \<i>)"
+    by (simp add: divide_simps) (simp add: algebra_simps)
+  also have "... = z - r * exp (2 * pi * \<i> * x)"
+    by (simp add: exp_add)
+  finally show ?thesis
+    by (simp add: circlepath path_image_def sphere_def dist_norm)
+qed
+
+lemma circlepath_add1: "circlepath z r (x+1) = circlepath z r x"
+  using circlepath_minus [of z r "x+1/2"] circlepath_minus [of z "-r" x]
+  by (simp add: add.commute)
+
+lemma circlepath_add_half: "circlepath z r (x + 1/2) = circlepath z r (x - 1/2)"
+  using circlepath_add1 [of z r "x-1/2"]
+  by (simp add: add.commute)
+
+lemma path_image_circlepath_minus_subset:
+     "path_image (circlepath z (-r)) \<subseteq> path_image (circlepath z r)"
+  apply (simp add: path_image_def image_def circlepath_minus, clarify)
+  apply (case_tac "xa \<le> 1/2", force)
+  apply (force simp add: circlepath_add_half)+
+  done
+
+lemma path_image_circlepath_minus: "path_image (circlepath z (-r)) = path_image (circlepath z r)"
+  using path_image_circlepath_minus_subset by fastforce
+
 proposition has_vector_derivative_circlepath [derivative_intros]:
  "((circlepath z r) has_vector_derivative (2 * pi * ii * r * exp (2 * of_real pi * ii * of_real x)))
    (at x within X)"
@@ -5055,7 +5084,7 @@
 lemma path_circlepath [simp]: "path (circlepath z r)"
   by (simp add: valid_path_imp_path)
 
-proposition path_image_circlepath [simp]:
+lemma path_image_circlepath_nonneg:
   assumes "0 \<le> r" shows "path_image (circlepath z r) = sphere z r"
 proof -
   have *: "x \<in> (\<lambda>u. z + (cmod (x - z)) * exp (\<i> * (of_real u * (of_real pi * 2)))) ` {0..1}" for x
@@ -5081,6 +5110,11 @@
     by (force simp: assms algebra_simps norm_mult norm_minus_commute intro: *)
 qed
 
+proposition path_image_circlepath [simp]:
+    "path_image (circlepath z r) = sphere z (abs r)"
+  using path_image_circlepath_minus
+  by (force simp add: path_image_circlepath_nonneg abs_if)
+
 lemma has_contour_integral_bound_circlepath_strong:
       "\<lbrakk>(f has_contour_integral i) (circlepath z r);
         finite k; 0 \<le> B; 0 < r;
@@ -5104,10 +5138,7 @@
   by (simp add: circlepath_def simple_path_part_circlepath)
 
 lemma notin_path_image_circlepath [simp]: "cmod (w - z) < r \<Longrightarrow> w \<notin> path_image (circlepath z r)"
-  apply (subst path_image_circlepath)
-  apply (meson le_cases less_le_trans norm_not_less_zero)
-  apply (simp add: sphere_def dist_norm norm_minus_commute)
-  done
+  by (simp add: sphere_def dist_norm norm_minus_commute)
 
 proposition contour_integral_circlepath:
      "0 < r \<Longrightarrow> contour_integral (circlepath z r) (\<lambda>w. 1 / (w - z)) = 2 * complex_of_real pi * \<i>"
@@ -5195,4 +5226,803 @@
 apply (rule no_bounded_connected_component_imp_winding_number_zero [OF g])
 by (simp add: bounded_subset nb path_component_subset_connected_component)
 
+
+subsection\<open> Uniform convergence of path integral\<close>
+
+text\<open>Uniform convergence when the derivative of the path is bounded, and in particular for the special case of a circle.\<close>
+
+proposition contour_integral_uniform_limit:
+  assumes ev_fint: "eventually (\<lambda>n::'a. (f n) contour_integrable_on \<gamma>) F"
+      and ev_no: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> path_image \<gamma>. norm(f n x - l x) < e) F"
+      and noleB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
+      and \<gamma>: "valid_path \<gamma>"
+      and [simp]: "~ (trivial_limit F)"
+  shows "l contour_integrable_on \<gamma>" "((\<lambda>n. contour_integral \<gamma> (f n)) ---> contour_integral \<gamma> l) F"
+proof -
+  have "0 \<le> B" by (meson noleB [of 0] atLeastAtMost_iff norm_ge_zero order_refl order_trans zero_le_one)
+  { fix e::real
+    assume "0 < e"
+    then have eB: "0 < e / (\<bar>B\<bar> + 1)" by simp
+    obtain a where fga: "\<And>x. x \<in> {0..1} \<Longrightarrow> cmod (f a (\<gamma> x) - l (\<gamma> x)) < e / (\<bar>B\<bar> + 1)"
+               and inta: "(\<lambda>t. f a (\<gamma> t) * vector_derivative \<gamma> (at t)) integrable_on {0..1}"
+      using eventually_happens [OF eventually_conj [OF ev_no [OF eB] ev_fint]]
+      by (fastforce simp: contour_integrable_on path_image_def)
+    have Ble: "B * e / (\<bar>B\<bar> + 1) \<le> e"
+      using \<open>0 \<le> B\<close>  \<open>0 < e\<close> by (simp add: divide_simps)
+    have "\<exists>h. (\<forall>x\<in>{0..1}. cmod (l (\<gamma> x) * vector_derivative \<gamma> (at x) - h x) \<le> e) \<and> h integrable_on {0..1}"
+      apply (rule_tac x="\<lambda>x. f (a::'a) (\<gamma> x) * vector_derivative \<gamma> (at x)" in exI)
+      apply (intro inta conjI ballI)
+      apply (rule order_trans [OF _ Ble])
+      apply (frule noleB)
+      apply (frule fga)
+      using \<open>0 \<le> B\<close>  \<open>0 < e\<close>
+      apply (simp add: norm_mult left_diff_distrib [symmetric] norm_minus_commute divide_simps)
+      apply (drule (1) mult_mono [OF less_imp_le])
+      apply (simp_all add: mult_ac)
+      done
+  }
+  then show lintg: "l contour_integrable_on \<gamma>"
+    apply (simp add: contour_integrable_on)
+    apply (blast intro: integrable_uniform_limit_real)
+    done
+  { fix e::real
+    def B' \<equiv> "B+1"
+    have B': "B' > 0" "B' > B" using  \<open>0 \<le> B\<close> by (auto simp: B'_def)
+    assume "0 < e"
+    then have ev_no': "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image \<gamma>. 2 * cmod (f n x - l x) < e / B'"
+      using ev_no [of "e / B' / 2"] B' by (simp add: field_simps)
+    have ie: "integral {0..1::real} (\<lambda>x. e / 2) < e" using \<open>0 < e\<close> by simp
+    have *: "cmod (f x (\<gamma> t) * vector_derivative \<gamma> (at t) - l (\<gamma> t) * vector_derivative \<gamma> (at t)) \<le> e / 2"
+             if t: "t\<in>{0..1}" and leB': "2 * cmod (f x (\<gamma> t) - l (\<gamma> t)) < e / B'" for x t
+    proof -
+      have "2 * cmod (f x (\<gamma> t) - l (\<gamma> t)) * cmod (vector_derivative \<gamma> (at t)) \<le> e * (B/ B')"
+        using mult_mono [OF less_imp_le [OF leB'] noleB] B' \<open>0 < e\<close> t by auto
+      also have "... < e"
+        by (simp add: B' \<open>0 < e\<close> mult_imp_div_pos_less)
+      finally have "2 * cmod (f x (\<gamma> t) - l (\<gamma> t)) * cmod (vector_derivative \<gamma> (at t)) < e" .
+      then show ?thesis
+        by (simp add: left_diff_distrib [symmetric] norm_mult)
+    qed
+    have "\<forall>\<^sub>F x in F. dist (contour_integral \<gamma> (f x)) (contour_integral \<gamma> l) < e"
+      apply (rule eventually_mono [OF eventually_conj [OF ev_no' ev_fint]])
+      apply (simp add: dist_norm contour_integrable_on path_image_def contour_integral_integral)
+      apply (simp add: lintg integral_diff [symmetric] contour_integrable_on [symmetric], clarify)
+      apply (rule le_less_trans [OF integral_norm_bound_integral ie])
+      apply (simp add: lintg integrable_diff contour_integrable_on [symmetric])
+      apply (blast intro: *)+
+      done
+  }
+  then show "((\<lambda>n. contour_integral \<gamma> (f n)) ---> contour_integral \<gamma> l) F"
+    by (rule tendstoI)
+qed
+
+proposition contour_integral_uniform_limit_circlepath:
+  assumes ev_fint: "eventually (\<lambda>n::'a. (f n) contour_integrable_on (circlepath z r)) F"
+      and ev_no: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> path_image (circlepath z r). norm(f n x - l x) < e) F"
+      and [simp]: "~ (trivial_limit F)" "0 < r"
+  shows "l contour_integrable_on (circlepath z r)" "((\<lambda>n. contour_integral (circlepath z r) (f n)) ---> contour_integral (circlepath z r) l) F"
+by (auto simp: vector_derivative_circlepath norm_mult intro: contour_integral_uniform_limit assms)
+
+
+subsection\<open> General stepping result for derivative formulas.\<close>
+
+lemma sum_sqs_eq:
+  fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \<Longrightarrow> y = x"
+  by algebra
+
+proposition Cauchy_next_derivative:
+  assumes "continuous_on (path_image \<gamma>) f'"
+      and leB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
+      and int: "\<And>w. w \<in> s - path_image \<gamma> \<Longrightarrow> ((\<lambda>u. f' u / (u - w)^k) has_contour_integral f w) \<gamma>"
+      and k: "k \<noteq> 0"
+      and "open s"
+      and \<gamma>: "valid_path \<gamma>"
+      and w: "w \<in> s - path_image \<gamma>"
+    shows "(\<lambda>u. f' u / (u - w)^(Suc k)) contour_integrable_on \<gamma>"
+      and "(f has_field_derivative (k * contour_integral \<gamma> (\<lambda>u. f' u/(u - w)^(Suc k))))
+           (at w)"  (is "?thes2")
+proof -
+  have "open (s - path_image \<gamma>)" using \<open>open s\<close> closed_valid_path_image \<gamma> by blast
+  then obtain d where "d>0" and d: "ball w d \<subseteq> s - path_image \<gamma>" using w
+    using open_contains_ball by blast
+  have [simp]: "\<And>n. cmod (1 + of_nat n) = 1 + of_nat n"
+    by (metis norm_of_nat of_nat_Suc)
+  have 1: "\<forall>\<^sub>F n in at w. (\<lambda>x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k)
+                         contour_integrable_on \<gamma>"
+    apply (simp add: eventually_at)
+    apply (rule_tac x=d in exI)
+    apply (simp add: \<open>d > 0\<close> dist_norm field_simps, clarify)
+    apply (rule contour_integrable_div [OF contour_integrable_diff])
+    using int w d
+    apply (force simp:  dist_norm norm_minus_commute intro!: has_contour_integral_integrable)+
+    done
+  have bim_g: "bounded (image f' (path_image \<gamma>))"
+    by (simp add: compact_imp_bounded compact_continuous_image compact_valid_path_image assms)
+  then obtain C where "C > 0" and C: "\<And>x. \<lbrakk>0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cmod (f' (\<gamma> x)) \<le> C"
+    by (force simp: bounded_pos path_image_def)
+  have twom: "\<forall>\<^sub>F n in at w.
+               \<forall>x\<in>path_image \<gamma>.
+                cmod ((inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / k - inverse (x - w) ^ Suc k) < e"
+         if "0 < e" for e
+  proof -
+    have *: "cmod ((inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k) - inverse (x - w) ^ Suc k)   < e"
+            if x: "x \<in> path_image \<gamma>" and "u \<noteq> w" and uwd: "cmod (u - w) < d/2"
+                and uw_less: "cmod (u - w) < e * (d / 2) ^ (k+2) / (1 + real k)"
+            for u x
+    proof -
+      def ff \<equiv> "\<lambda>n::nat. \<lambda>w. if n = 0 then inverse(x - w)^k
+                              else if n = 1 then k / (x - w)^(Suc k)
+                              else (k * of_real(Suc k)) / (x - w)^(k + 2)"
+      have km1: "\<And>z::complex. z \<noteq> 0 \<Longrightarrow> z ^ (k - Suc 0) = z ^ k / z"
+        by (simp add: field_simps) (metis Suc_pred \<open>k \<noteq> 0\<close> neq0_conv power_Suc)
+      have ff1: "(ff i has_field_derivative ff (Suc i) z) (at z within ball w (d / 2))"
+              if "z \<in> ball w (d / 2)" "i \<le> 1" for i z
+      proof -
+        have "z \<notin> path_image \<gamma>"
+          using \<open>x \<in> path_image \<gamma>\<close> d that ball_divide_subset_numeral by blast
+        then have xz[simp]: "x \<noteq> z" using \<open>x \<in> path_image \<gamma>\<close> by blast
+        then have neq: "x * x + z * z \<noteq> x * (z * 2)"
+          by (blast intro: dest!: sum_sqs_eq)
+        with xz have "\<And>v. v \<noteq> 0 \<Longrightarrow> (x * x + z * z) * v \<noteq> (x * (z * 2) * v)" by auto
+        then have neqq: "\<And>v. v \<noteq> 0 \<Longrightarrow> x * (x * v) + z * (z * v) \<noteq> x * (z * (2 * v))"
+          by (simp add: algebra_simps)
+        show ?thesis using \<open>i \<le> 1\<close>
+          apply (simp add: ff_def dist_norm Nat.le_Suc_eq km1, safe)
+          apply (rule derivative_eq_intros | simp add: km1 | simp add: field_simps neq neqq)+
+          done
+      qed
+      { fix a::real and b::real assume ab: "a > 0" "b > 0"
+        then have "k * (1 + real k) * (1 / a) \<le> k * (1 + real k) * (4 / b) \<longleftrightarrow> b \<le> 4 * a"
+          apply (subst mult_le_cancel_left_pos)
+          using \<open>k \<noteq> 0\<close>
+          apply (auto simp: divide_simps)
+          done
+        with ab have "real k * (1 + real k) / a \<le> (real k * 4 + real k * real k * 4) / b \<longleftrightarrow> b \<le> 4 * a"
+          by (simp add: field_simps)
+      } note canc = this
+      have ff2: "cmod (ff (Suc 1) v) \<le> real (k * (k + 1)) / (d / 2) ^ (k + 2)"
+                if "v \<in> ball w (d / 2)" for v
+      proof -
+        have "d/2 \<le> cmod (x - v)" using d x that
+          apply (simp add: dist_norm path_image_def ball_def not_less [symmetric] del: divide_const_simps, clarify)
+          apply (drule subsetD)
+           prefer 2 apply blast
+          apply (metis norm_minus_commute norm_triangle_half_r CollectI)
+          done
+        then have "d \<le> cmod (x - v) * 2"
+          by (simp add: divide_simps)
+        then have dpow_le: "d ^ (k+2) \<le> (cmod (x - v) * 2) ^ (k+2)"
+          using \<open>0 < d\<close> order_less_imp_le power_mono by blast
+        have "x \<noteq> v" using that
+          using \<open>x \<in> path_image \<gamma>\<close> ball_divide_subset_numeral d by fastforce
+        then show ?thesis
+        using \<open>d > 0\<close>
+        apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc)
+        using dpow_le
+        apply (simp add: algebra_simps divide_simps mult_less_0_iff)
+        done
+      qed
+      have ub: "u \<in> ball w (d / 2)"
+        using uwd by (simp add: dist_commute dist_norm)
+      have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
+                  \<le> (real k * 4 + real k * real k * 4) * (cmod (u - w) * cmod (u - w)) / (d * (d * (d / 2) ^ k))"
+        using complex_taylor [OF _ ff1 ff2 _ ub, of w, simplified]
+        by (simp add: ff_def \<open>0 < d\<close>)
+      then have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
+                  \<le> (cmod (u - w) * real k) * (1 + real k) * cmod (u - w) / (d / 2) ^ (k+2)"
+        by (simp add: field_simps)
+      then have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
+                 / (cmod (u - w) * real k)
+                  \<le> (1 + real k) * cmod (u - w) / (d / 2) ^ (k+2)"
+        using \<open>k \<noteq> 0\<close> \<open>u \<noteq> w\<close> by (simp add: mult_ac zero_less_mult_iff pos_divide_le_eq)
+      also have "... < e"
+        using uw_less \<open>0 < d\<close> by (simp add: mult_ac divide_simps)
+      finally have e: "cmod (inverse (x-u)^k - (inverse (x-w)^k + of_nat k * (u-w) / ((x-w) * (x-w)^k)))
+                        / cmod ((u - w) * real k)   <   e"
+        by (simp add: norm_mult)
+      have "x \<noteq> u"
+        using uwd \<open>0 < d\<close> x d by (force simp: dist_norm ball_def norm_minus_commute)
+      show ?thesis
+        apply (rule le_less_trans [OF _ e])
+        using \<open>k \<noteq> 0\<close> \<open>x \<noteq> u\<close>  \<open>u \<noteq> w\<close>
+        apply (simp add: field_simps norm_divide [symmetric])
+        done
+    qed
+    show ?thesis
+      unfolding eventually_at
+      apply (rule_tac x = "min (d/2) ((e*(d/2)^(k + 2))/(Suc k))" in exI)
+      apply (force simp: \<open>d > 0\<close> dist_norm that simp del: power_Suc intro: *)
+      done
+  qed
+  have 2: "\<forall>\<^sub>F n in at w.
+              \<forall>x\<in>path_image \<gamma>.
+               cmod (f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k - f' x / (x - w) ^ Suc k) < e"
+          if "0 < e" for e
+  proof -
+    have *: "cmod (f' (\<gamma> x) * (inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
+                        f' (\<gamma> x) / ((\<gamma> x - w) * (\<gamma> x - w) ^ k)) < e"
+              if ec: "cmod ((inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
+                      inverse (\<gamma> x - w) * inverse (\<gamma> x - w) ^ k) < e / C"
+                 and x: "0 \<le> x" "x \<le> 1"
+              for u x
+    proof (cases "(f' (\<gamma> x)) = 0")
+      case True then show ?thesis by (simp add: \<open>0 < e\<close>)
+    next
+      case False
+      have "cmod (f' (\<gamma> x) * (inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
+                        f' (\<gamma> x) / ((\<gamma> x - w) * (\<gamma> x - w) ^ k)) =
+            cmod (f' (\<gamma> x) * ((inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
+                             inverse (\<gamma> x - w) * inverse (\<gamma> x - w) ^ k))"
+        by (simp add: field_simps)
+      also have "... = cmod (f' (\<gamma> x)) *
+                       cmod ((inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
+                             inverse (\<gamma> x - w) * inverse (\<gamma> x - w) ^ k)"
+        by (simp add: norm_mult)
+      also have "... < cmod (f' (\<gamma> x)) * (e/C)"
+        apply (rule mult_strict_left_mono [OF ec])
+        using False by simp
+      also have "... \<le> e" using C
+        by (metis False \<open>0 < e\<close> frac_le less_eq_real_def mult.commute pos_le_divide_eq x zero_less_norm_iff)
+      finally show ?thesis .
+    qed
+    show ?thesis
+      using twom [OF divide_pos_pos [OF that \<open>C > 0\<close>]]   unfolding path_image_def
+      by (force intro: * elim: eventually_mono)
+  qed
+  show "(\<lambda>u. f' u / (u - w) ^ (Suc k)) contour_integrable_on \<gamma>"
+    by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
+  have *: "(\<lambda>n. contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / k))
+           --w--> contour_integral \<gamma> (\<lambda>u. f' u / (u - w) ^ (Suc k))"
+    by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
+  have **: "contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k)) =
+              (f u - f w) / (u - w) / k"
+           if "dist u w < d" for u
+    apply (rule contour_integral_unique)
+    apply (simp add: diff_divide_distrib algebra_simps)
+    apply (rule has_contour_integral_diff; rule has_contour_integral_div; simp add: field_simps; rule int)
+    apply (metis contra_subsetD d dist_commute mem_ball that)
+    apply (rule w)
+    done
+  show ?thes2
+    apply (simp add: DERIV_within_iff del: power_Suc)
+    apply (rule Lim_transform_at [OF \<open>0 < d\<close> _ tendsto_mult_left [OF *]])
+    apply (simp add: \<open>k \<noteq> 0\<close> **)
+    done
+qed
+
+corollary Cauchy_next_derivative_circlepath:
+  assumes contf: "continuous_on (path_image (circlepath z r)) f"
+      and int: "\<And>w. w \<in> ball z r \<Longrightarrow> ((\<lambda>u. f u / (u - w)^k) has_contour_integral g w) (circlepath z r)"
+      and k: "k \<noteq> 0"
+      and w: "w \<in> ball z r"
+    shows "(\<lambda>u. f u / (u - w)^(Suc k)) contour_integrable_on (circlepath z r)"
+           (is "?thes1")
+      and "(g has_field_derivative (k * contour_integral (circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k)))) (at w)"
+           (is "?thes2")
+proof -
+  have "r > 0" using w
+    using ball_eq_empty by fastforce
+  have wim: "w \<in> ball z r - path_image (circlepath z r)"
+    using w by (auto simp: dist_norm)
+  show ?thes1 ?thes2
+    by (rule Cauchy_next_derivative [OF contf _ int k open_ball valid_path_circlepath wim, where B = "2 * pi * \<bar>r\<bar>"];
+        auto simp: vector_derivative_circlepath norm_mult)+
+qed
+
+
+text\<open> In particular, the first derivative formula.\<close>
+
+proposition Cauchy_derivative_integral_circlepath:
+  assumes contf: "continuous_on (cball z r) f"
+      and holf: "f holomorphic_on ball z r"
+      and w: "w \<in> ball z r"
+    shows "(\<lambda>u. f u/(u - w)^2) contour_integrable_on (circlepath z r)"
+           (is "?thes1")
+      and "(f has_field_derivative (1 / (2 * of_real pi * ii) * contour_integral(circlepath z r) (\<lambda>u. f u / (u - w)^2))) (at w)"
+           (is "?thes2")
+proof -
+  have [simp]: "r \<ge> 0" using w
+    using ball_eq_empty by fastforce
+  have f: "continuous_on (path_image (circlepath z r)) f"
+    by (rule continuous_on_subset [OF contf]) (force simp add: cball_def sphere_def)
+  have int: "\<And>w. dist z w < r \<Longrightarrow>
+                 ((\<lambda>u. f u / (u - w)) has_contour_integral (\<lambda>x. 2 * of_real pi * ii * f x) w) (circlepath z r)"
+    by (rule Cauchy_integral_circlepath [OF contf holf]) (simp add: dist_norm norm_minus_commute)
+  show ?thes1
+    apply (simp add: power2_eq_square)
+    apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1, simplified])
+    apply (blast intro: int)
+    done
+  have "((\<lambda>x. 2 * of_real pi * \<i> * f x) has_field_derivative contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)^2)) (at w)"
+    apply (simp add: power2_eq_square)
+    apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "\<lambda>x. 2 * of_real pi * ii * f x", simplified])
+    apply (blast intro: int)
+    done
+  then have fder: "(f has_field_derivative contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)^2) / (2 * of_real pi * \<i>)) (at w)"
+    by (rule DERIV_cdivide [where f = "\<lambda>x. 2 * of_real pi * \<i> * f x" and c = "2 * of_real pi * \<i>", simplified])
+  show ?thes2
+    by simp (rule fder)
+qed
+
+subsection\<open> Existence of all higher derivatives.\<close>
+
+proposition derivative_is_holomorphic:
+  assumes "open s"
+      and fder: "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z)"
+    shows "f' holomorphic_on s"
+proof -
+  have *: "\<exists>h. (f' has_field_derivative h) (at z)" if "z \<in> s" for z
+  proof -
+    obtain r where "r > 0" and r: "cball z r \<subseteq> s"
+      using open_contains_cball \<open>z \<in> s\<close> \<open>open s\<close> by blast
+    then have holf_cball: "f holomorphic_on cball z r"
+      apply (simp add: holomorphic_on_def)
+      using complex_differentiable_at_within complex_differentiable_def fder by blast
+    then have "continuous_on (path_image (circlepath z r)) f"
+      using \<open>r > 0\<close> by (force elim: holomorphic_on_subset [THEN holomorphic_on_imp_continuous_on])
+    then have contfpi: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1/(2 * of_real pi*ii) * f x)"
+      by (auto intro: continuous_intros)+
+    have contf_cball: "continuous_on (cball z r) f" using holf_cball
+      by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_subset)
+    have holf_ball: "f holomorphic_on ball z r" using holf_cball
+      using ball_subset_cball holomorphic_on_subset by blast
+    { fix w  assume w: "w \<in> ball z r"  
+      have intf: "(\<lambda>u. f u / (u - w)\<^sup>2) contour_integrable_on circlepath z r"
+        by (blast intro: w Cauchy_derivative_integral_circlepath [OF contf_cball holf_ball])
+      have fder': "(f has_field_derivative 1 / (2 * of_real pi * \<i>) * contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2))
+                  (at w)"
+        by (blast intro: w Cauchy_derivative_integral_circlepath [OF contf_cball holf_ball])
+      have f'_eq: "f' w = contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2) / (2 * of_real pi * \<i>)"
+        using fder' ball_subset_cball r w by (force intro: DERIV_unique [OF fder])
+      have "((\<lambda>u. f u / (u - w)\<^sup>2 / (2 * of_real pi * \<i>)) has_contour_integral
+                contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2) / (2 * of_real pi * \<i>))
+                (circlepath z r)"
+        by (rule Cauchy_Integral_Thm.has_contour_integral_div [OF has_contour_integral_integral [OF intf]])
+      then have "((\<lambda>u. f u / (2 * of_real pi * \<i> * (u - w)\<^sup>2)) has_contour_integral
+                contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2) / (2 * of_real pi * \<i>))
+                (circlepath z r)"
+        by (simp add: algebra_simps)
+      then have "((\<lambda>u. f u / (2 * of_real pi * \<i> * (u - w)\<^sup>2)) has_contour_integral f' w) (circlepath z r)"
+        by (simp add: f'_eq)
+    } note * = this
+    show ?thesis
+      apply (rule exI)
+      apply (rule Cauchy_next_derivative_circlepath [OF contfpi, of 2 f', simplified])
+      apply (simp_all add: \<open>0 < r\<close> * dist_norm)
+      done
+  qed
+  show ?thesis
+    by (simp add: holomorphic_on_open [OF \<open>open s\<close>] *)
+qed
+
+lemma holomorphic_deriv [holomorphic_intros]: 
+    "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
+by (metis DERIV_deriv_iff_complex_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
+
+lemma analytic_deriv: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
+  using analytic_on_holomorphic holomorphic_deriv by auto
+
+lemma holomorphic_higher_deriv [holomorphic_intros]: "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv ^^ n) f holomorphic_on s"
+  by (induction n) (auto simp: holomorphic_deriv)
+
+lemma analytic_higher_deriv: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
+  unfolding analytic_on_def using holomorphic_higher_deriv by blast
+
+lemma has_field_derivative_higher_deriv: 
+     "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> 
+      \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
+by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply 
+         funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
+
+
+subsection\<open> Morera's theorem.\<close>
+
+lemma Morera_local_triangle_ball:
+  assumes "\<And>z. z \<in> s
+          \<Longrightarrow> \<exists>e a. 0 < e \<and> z \<in> ball a e \<and> continuous_on (ball a e) f \<and>
+                    (\<forall>b c. closed_segment b c \<subseteq> ball a e
+                           \<longrightarrow> contour_integral (linepath a b) f +
+                               contour_integral (linepath b c) f +
+                               contour_integral (linepath c a) f = 0)"
+  shows "f analytic_on s"
+proof -
+  { fix z  assume "z \<in> s"
+    with assms obtain e a where 
+            "0 < e" and z: "z \<in> ball a e" and contf: "continuous_on (ball a e) f"
+        and 0: "\<And>b c. closed_segment b c \<subseteq> ball a e
+                      \<Longrightarrow> contour_integral (linepath a b) f +
+                          contour_integral (linepath b c) f +
+                          contour_integral (linepath c a) f = 0"
+      by fastforce
+    have az: "dist a z < e" using mem_ball z by blast
+    have sb_ball: "ball z (e - dist a z) \<subseteq> ball a e"
+      by (simp add: dist_commute ball_subset_ball_iff)
+    have "\<exists>e>0. f holomorphic_on ball z e"
+      apply (rule_tac x="e - dist a z" in exI)
+      apply (simp add: az)
+      apply (rule holomorphic_on_subset [OF _ sb_ball])
+      apply (rule derivative_is_holomorphic[OF open_ball])
+      apply (rule triangle_contour_integrals_starlike_primitive [OF contf _ open_ball, of a])
+         apply (simp_all add: 0 \<open>0 < e\<close>)
+      apply (meson \<open>0 < e\<close> centre_in_ball convex_ball convex_contains_segment mem_ball)
+      done
+  }
+  then show ?thesis
+    by (simp add: analytic_on_def)
+qed
+
+lemma Morera_local_triangle:
+  assumes "\<And>z. z \<in> s
+          \<Longrightarrow> \<exists>t. open t \<and> z \<in> t \<and> continuous_on t f \<and>
+                  (\<forall>a b c. convex hull {a,b,c} \<subseteq> t
+                              \<longrightarrow> contour_integral (linepath a b) f +
+                                  contour_integral (linepath b c) f +
+                                  contour_integral (linepath c a) f = 0)"
+  shows "f analytic_on s"
+proof -
+  { fix z  assume "z \<in> s"
+    with assms obtain t where 
+            "open t" and z: "z \<in> t" and contf: "continuous_on t f"
+        and 0: "\<And>a b c. convex hull {a,b,c} \<subseteq> t
+                      \<Longrightarrow> contour_integral (linepath a b) f +
+                          contour_integral (linepath b c) f +
+                          contour_integral (linepath c a) f = 0"
+      by force
+    then obtain e where "e>0" and e: "ball z e \<subseteq> t" 
+      using open_contains_ball by blast
+    have [simp]: "continuous_on (ball z e) f" using contf
+      using continuous_on_subset e by blast
+    have "\<exists>e a. 0 < e \<and>
+               z \<in> ball a e \<and>
+               continuous_on (ball a e) f \<and>
+               (\<forall>b c. closed_segment b c \<subseteq> ball a e \<longrightarrow>
+                      contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0)"
+      apply (rule_tac x=e in exI)
+      apply (rule_tac x=z in exI)
+      apply (simp add: \<open>e > 0\<close>, clarify)
+      apply (rule 0)
+      apply (meson z \<open>0 < e\<close> centre_in_ball closed_segment_subset convex_ball dual_order.trans e starlike_convex_subset)
+      done
+  }
+  then show ?thesis
+    by (simp add: Morera_local_triangle_ball)
+qed
+
+proposition Morera_triangle:
+    "\<lbrakk>continuous_on s f; open s; 
+      \<And>a b c. convex hull {a,b,c} \<subseteq> s
+              \<longrightarrow> contour_integral (linepath a b) f +
+                  contour_integral (linepath b c) f +
+                  contour_integral (linepath c a) f = 0\<rbrakk>
+     \<Longrightarrow> f analytic_on s"
+  using Morera_local_triangle by blast
+
+
+
+subsection\<open> Combining theorems for higher derivatives including Leibniz rule.\<close>
+
+lemma higher_deriv_linear [simp]: 
+    "(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>z. if n = 0 then c*z else if n = 1 then c else 0)"
+  by (induction n) (auto simp: deriv_const deriv_linear)
+
+lemma higher_deriv_const [simp]: "(deriv ^^ n) (\<lambda>w. c) = (\<lambda>w. if n=0 then c else 0)"
+  by (induction n) (auto simp: deriv_const)
+
+lemma higher_deriv_ident [simp]:
+     "(deriv ^^ n) (\<lambda>w. w) z = (if n = 0 then z else if n = 1 then 1 else 0)"
+  apply (induction n)
+  apply (simp_all add: deriv_ident funpow_Suc_right del: funpow.simps, simp)
+  done
+
+corollary higher_deriv_id [simp]:
+     "(deriv ^^ n) id z = (if n = 0 then z else if n = 1 then 1 else 0)"
+  by (simp add: id_def)
+
+lemma has_complex_derivative_funpow_1: 
+     "\<lbrakk>(f has_field_derivative 1) (at z); f z = z\<rbrakk> \<Longrightarrow> (f^^n has_field_derivative 1) (at z)"
+  apply (induction n)
+  apply auto
+  apply (metis DERIV_ident DERIV_transform_at id_apply zero_less_one)
+  by (metis DERIV_chain comp_funpow comp_id funpow_swap1 mult.right_neutral)
+
+proposition higher_deriv_uminus: 
+  assumes "f holomorphic_on s" "open s" and z: "z \<in> s"
+    shows "(deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
+using z
+proof (induction n arbitrary: z)
+  case 0 then show ?case by simp
+next
+  case (Suc n z) 
+  have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
+    using Suc.prems assms has_field_derivative_higher_deriv by auto
+  show ?case
+    apply simp
+    apply (rule DERIV_imp_deriv)
+    apply (rule DERIV_transform_within_open [of "\<lambda>w. -((deriv ^^ n) f w)"])
+    apply (rule derivative_eq_intros | rule * refl assms Suc)+
+    apply (simp add: Suc)
+    done
+qed
+
+proposition higher_deriv_add: 
+  fixes z::complex
+  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
+    shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
+using z
+proof (induction n arbitrary: z)
+  case 0 then show ?case by simp
+next
+  case (Suc n z) 
+  have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
+          "((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
+    using Suc.prems assms has_field_derivative_higher_deriv by auto
+  show ?case
+    apply simp
+    apply (rule DERIV_imp_deriv)
+    apply (rule DERIV_transform_within_open [of "\<lambda>w. (deriv ^^ n) f w + (deriv ^^ n) g w"])
+    apply (rule derivative_eq_intros | rule * refl assms Suc)+
+    apply (simp add: Suc)
+    done
+qed
+
+corollary higher_deriv_diff: 
+  fixes z::complex
+  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
+    shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
+  apply (simp only: Groups.group_add_class.diff_conv_add_uminus higher_deriv_add)
+  apply (subst higher_deriv_add)
+  using assms holomorphic_on_minus apply (auto simp: higher_deriv_uminus)
+  done
+
+
+lemma bb: "Suc n choose k = (n choose k) + (if k = 0 then 0 else (n choose (k - 1)))"
+  by (simp add: Binomial.binomial.simps)
+
+proposition higher_deriv_mult:
+  fixes z::complex
+  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
+    shows "(deriv ^^ n) (\<lambda>w. f w * g w) z = 
+           (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
+using z
+proof (induction n arbitrary: z)
+  case 0 then show ?case by simp
+next
+  case (Suc n z) 
+  have *: "\<And>n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
+          "\<And>n. ((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
+    using Suc.prems assms has_field_derivative_higher_deriv by auto
+  have sumeq: "(\<Sum>i = 0..n.
+               of_nat (n choose i) * (deriv ((deriv ^^ i) f) z * (deriv ^^ (n - i)) g z + deriv ((deriv ^^ (n - i)) g) z * (deriv ^^ i) f z)) =
+            g z * deriv ((deriv ^^ n) f) z + (\<Sum>i = 0..n. (deriv ^^ i) f z * (of_nat (Suc n choose i) * (deriv ^^ (Suc n - i)) g z))"
+    apply (simp add: bb distrib_right algebra_simps setsum.distrib)
+    apply (subst (4) setsum_Suc_reindex)
+    apply (auto simp: algebra_simps Suc_diff_le intro: setsum.cong)
+    done
+  show ?case
+    apply (simp only: funpow.simps o_apply)
+    apply (rule DERIV_imp_deriv)
+    apply (rule DERIV_transform_within_open 
+             [of "\<lambda>w. (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"])
+    apply (simp add: algebra_simps)
+    apply (rule DERIV_cong [OF DERIV_setsum])
+    apply (rule DERIV_cmult)
+    apply (auto simp: intro: DERIV_mult * sumeq \<open>open s\<close> Suc.prems Suc.IH [symmetric])
+    done
+qed
+
+
+proposition higher_deriv_transform_within_open:
+  fixes z::complex
+  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
+      and fg: "\<And>w. w \<in> s \<Longrightarrow> f w = g w"
+    shows "(deriv ^^ i) f z = (deriv ^^ i) g z"
+using z
+by (induction i arbitrary: z) 
+   (auto simp: fg intro: complex_derivative_transform_within_open holomorphic_higher_deriv assms)
+
+proposition higher_deriv_compose_linear:
+  fixes z::complex
+  assumes f: "f holomorphic_on t" and s: "open s" and t: "open t" and z: "z \<in> s"
+      and fg: "\<And>w. w \<in> s \<Longrightarrow> u * w \<in> t"
+    shows "(deriv ^^ n) (\<lambda>w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)"
+using z
+proof (induction n arbitrary: z)
+  case 0 then show ?case by simp
+next
+  case (Suc n z) 
+  have holo0: "f holomorphic_on op * u ` s"
+    by (meson fg f holomorphic_on_subset image_subset_iff)
+  have holo1: "(\<lambda>w. f (u * w)) holomorphic_on s"
+    apply (rule holomorphic_on_compose [where g=f, unfolded o_def])
+    apply (rule holo0 holomorphic_intros)+
+    done
+  have holo2: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on s"
+    apply (rule holomorphic_intros)+
+    apply (rule holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def])
+    apply (rule holomorphic_intros)
+    apply (rule holomorphic_on_subset [where s=t])
+    apply (rule holomorphic_intros assms)+
+    apply (blast intro: fg)
+    done
+  have "deriv ((deriv ^^ n) (\<lambda>w. f (u * w))) z = deriv (\<lambda>z. u^n * (deriv ^^ n) f (u*z)) z"
+    apply (rule complex_derivative_transform_within_open [OF _ holo2 s Suc.prems])
+    apply (rule holomorphic_higher_deriv [OF holo1 s])
+    apply (simp add: Suc.IH)
+    done
+  also have "... = u^n * deriv (\<lambda>z. (deriv ^^ n) f (u * z)) z"
+    apply (rule complex_derivative_cmult)
+    apply (rule analytic_on_imp_differentiable_at [OF _ Suc.prems])
+    apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and t=t, unfolded o_def])
+    apply (simp add: analytic_on_linear)
+    apply (simp add: analytic_on_open f holomorphic_higher_deriv t)
+    apply (blast intro: fg)
+    done
+  also have "... = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
+      apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "op*u", unfolded o_def])
+      apply (rule derivative_intros)
+      using Suc.prems complex_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
+      apply (simp add: deriv_linear)
+      done
+  finally show ?case
+    by simp
+qed
+
+lemma higher_deriv_add_at: 
+  assumes "f analytic_on {z}" "g analytic_on {z}"
+    shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
+proof -
+  have "f analytic_on {z} \<and> g analytic_on {z}"
+    using assms by blast
+  with higher_deriv_add show ?thesis
+    by (auto simp: analytic_at_two)
+qed
+
+lemma higher_deriv_diff_at: 
+  assumes "f analytic_on {z}" "g analytic_on {z}"
+    shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
+proof -
+  have "f analytic_on {z} \<and> g analytic_on {z}"
+    using assms by blast
+  with higher_deriv_diff show ?thesis
+    by (auto simp: analytic_at_two)
+qed
+
+lemma higher_deriv_uminus_at: 
+   "f analytic_on {z}  \<Longrightarrow> (deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
+  using higher_deriv_uminus
+    by (auto simp: analytic_at)
+
+lemma higher_deriv_mult_at: 
+  assumes "f analytic_on {z}" "g analytic_on {z}"
+    shows "(deriv ^^ n) (\<lambda>w. f w * g w) z = 
+           (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
+proof -
+  have "f analytic_on {z} \<and> g analytic_on {z}"
+    using assms by blast
+  with higher_deriv_mult show ?thesis
+    by (auto simp: analytic_at_two)
+qed
+
+
+text\<open> Nonexistence of isolated singularities and a stronger integral formula.\<close>
+
+proposition no_isolated_singularity:
+  fixes z::complex
+  assumes f: "continuous_on s f" and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k"
+    shows "f holomorphic_on s"
+proof -
+  { fix z 
+    assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f complex_differentiable at x"
+    have "f complex_differentiable at z"
+    proof (cases "z \<in> k")
+      case False then show ?thesis by (blast intro: cdf \<open>z \<in> s\<close>)
+    next
+      case True
+      with finite_set_avoid [OF k, of z] 
+      obtain d where "d>0" and d: "\<And>x. \<lbrakk>x\<in>k; x \<noteq> z\<rbrakk> \<Longrightarrow> d \<le> dist z x"
+        by blast
+      obtain e where "e>0" and e: "ball z e \<subseteq> s" 
+        using  s \<open>z \<in> s\<close> by (force simp add: open_contains_ball)
+      have fde: "continuous_on (ball z (min d e)) f"
+        by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI)
+      have "\<exists>g. \<forall>w \<in> ball z (min d e). (g has_field_derivative f w) (at w within ball z (min d e))"
+        apply (rule contour_integral_convex_primitive [OF convex_ball fde])
+        apply (rule Cauchy_theorem_triangle_cofinite [OF _ k])
+         apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset)
+        apply (rule cdf)
+        apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset 
+               interior_mono interior_subset subset_hull)
+        done
+      then have "f holomorphic_on ball z (min d e)"
+        by (metis open_ball at_within_open derivative_is_holomorphic)
+      then show ?thesis
+        unfolding holomorphic_on_def
+        by (metis open_ball \<open>0 < d\<close> \<open>0 < e\<close> at_within_open centre_in_ball min_less_iff_conj)
+    qed
+  }
+  with holf s k show ?thesis
+    by (simp add: holomorphic_on_open open_Diff finite_imp_closed complex_differentiable_def [symmetric])
+qed
+
+proposition Cauchy_integral_formula_convex:
+    assumes s: "convex s" and k: "finite k" and contf: "continuous_on s f"
+        and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x)"
+        and z: "z \<in> interior s" and vpg: "valid_path \<gamma>"
+        and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+  apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf])
+  apply (simp add: holomorphic_on_open [symmetric] complex_differentiable_def)
+  using no_isolated_singularity [where s = "interior s"] 
+  apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset 
+               has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
+  using assms
+  apply auto
+  done
+
+
+text\<open> Formula for higher derivatives.\<close>
+
+proposition Cauchy_has_contour_integral_higher_derivative_circlepath:
+  assumes contf: "continuous_on (cball z r) f"
+      and holf: "f holomorphic_on ball z r"
+      and w: "w \<in> ball z r"
+    shows "((\<lambda>u. f u / (u - w) ^ (Suc k))
+             has_contour_integral ((2 * pi * ii) / of_real(fact k) * (deriv ^^ k) f w))
+           (circlepath z r)"
+using w
+proof (induction k arbitrary: w)
+  case 0 then show ?case
+    using assms by (auto simp: Cauchy_integral_circlepath dist_commute dist_norm)
+next
+  case (Suc k)
+  have [simp]: "r > 0" using w
+    using ball_eq_empty by fastforce
+  have f: "continuous_on (path_image (circlepath z r)) f"
+    by (rule continuous_on_subset [OF contf]) (force simp add: cball_def sphere_def less_imp_le)
+  obtain X where X: "((\<lambda>u. f u / (u - w) ^ Suc (Suc k)) has_contour_integral X) (circlepath z r)"
+    using Cauchy_next_derivative_circlepath(1) [OF f Suc.IH _ Suc.prems]
+    by (auto simp: contour_integrable_on_def)
+  then have con: "contour_integral (circlepath z r) ((\<lambda>u. f u / (u - w) ^ Suc (Suc k))) = X"
+    by (rule contour_integral_unique)
+  have "\<And>n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) w) (at w)"
+    using Suc.prems assms has_field_derivative_higher_deriv by auto
+  then have dnf_diff: "\<And>n. (deriv ^^ n) f complex_differentiable (at w)"
+    by (force simp add: complex_differentiable_def)
+  have "deriv (\<lambda>w. complex_of_real (2 * pi) * \<i> / complex_of_real (fact k) * (deriv ^^ k) f w) w =
+          of_nat (Suc k) * contour_integral (circlepath z r) (\<lambda>u. f u / (u - w) ^ Suc (Suc k))"
+    apply (rule DERIV_imp_deriv)
+    apply (rule Cauchy_next_derivative_circlepath [OF f Suc.IH _ Suc.prems])
+    apply auto
+    done
+  also have "... = of_nat (Suc k) * X"
+    by (simp only: con)
+  finally have "deriv (\<lambda>w. ((2 * pi) * \<i> / of_real (fact k)) * (deriv ^^ k) f w) w = of_nat (Suc k) * X" .
+  then have "((2 * pi) * \<i> / of_real (fact k)) * deriv (\<lambda>w. (deriv ^^ k) f w) w = of_nat (Suc k) * X"
+    by (metis complex_derivative_cmult dnf_diff)
+  then have "deriv (\<lambda>w. (deriv ^^ k) f w) w = of_nat (Suc k) * X / ((2 * pi) * \<i> / of_real (fact k))"
+    by (simp add: field_simps)
+  then show ?case
+  using of_nat_eq_0_iff X by fastforce
+qed
+
+proposition Cauchy_higher_derivative_integral_circlepath:
+  assumes contf: "continuous_on (cball z r) f"
+      and holf: "f holomorphic_on ball z r"
+      and w: "w \<in> ball z r"
+    shows "(\<lambda>u. f u / (u - w)^(Suc k)) contour_integrable_on (circlepath z r)"
+           (is "?thes1")
+      and "(deriv ^^ k) f w =
+             of_real(fact k) / (2 * pi * ii) * contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k))"
+           (is "?thes2")
+proof -
+  have *: "((\<lambda>u. f u / (u - w) ^ Suc k) has_contour_integral (2 * pi) * \<i> / (fact k) * (deriv ^^ k) f w)
+           (circlepath z r)"
+    using Cauchy_has_contour_integral_higher_derivative_circlepath [OF assms]
+    by simp
+  show ?thes1 using *
+    using contour_integrable_on_def by blast
+  show ?thes2 
+    unfolding contour_integral_unique [OF *] by (simp add: divide_simps)
+qed
+
 end
diff -r 2c79790d270d -r 9250e546ab23 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Dec 14 14:05:31 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Dec 15 14:40:36 2015 +0000
@@ -261,6 +261,7 @@
 
 subsection\<open>Holomorphic functions\<close>
 
+text{*Could be generalized to real normed fields, but in practice that would only include the reals*}
 definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
            (infixr "(complex'_differentiable)" 50)
   where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
@@ -481,13 +482,13 @@
     \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
   by (metis DERIV_deriv_iff_complex_differentiable DERIV_chain DERIV_imp_deriv)
 
-lemma complex_derivative_linear: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
+lemma deriv_linear: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
   by (metis DERIV_imp_deriv DERIV_cmult_Id)
 
-lemma complex_derivative_ident: "deriv (\<lambda>w. w) = (\<lambda>z. 1)"
+lemma deriv_ident: "deriv (\<lambda>w. w) = (\<lambda>z. 1)"
   by (metis DERIV_imp_deriv DERIV_ident)
 
-lemma complex_derivative_const: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
+lemma deriv_const: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
   by (metis DERIV_imp_deriv DERIV_const)
 
 lemma complex_derivative_add:
@@ -797,11 +798,11 @@
 
 lemma complex_derivative_cmult_at:
   "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. c * f w) z = c * deriv f z"
-by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const)
+by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
 
 lemma complex_derivative_cmult_right_at:
   "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
-by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const)
+by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
 
 subsection\<open>Complex differentiation of sequences and series\<close>
 
diff -r 2c79790d270d -r 9250e546ab23 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 14 14:05:31 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Dec 15 14:40:36 2015 +0000
@@ -6359,6 +6359,9 @@
   "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"
   unfolding convex_alt closed_segment_def by auto
 
+lemma closed_segment_subset: "\<lbrakk>x \<in> s; y \<in> s; convex s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> s"
+  by (simp add: convex_contains_segment)
+
 lemma closed_segment_subset_convex_hull:
     "\<lbrakk>x \<in> convex hull s; y \<in> convex hull s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull s"
   using convex_contains_segment by blast
diff -r 2c79790d270d -r 9250e546ab23 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 14 14:05:31 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 15 14:40:36 2015 +0000
@@ -826,6 +826,9 @@
 lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"
   by (simp add: cball_def)
 
+lemma mem_sphere [simp]: "y \<in> sphere x e \<longleftrightarrow> dist x y = e"
+  by (simp add: sphere_def)
+
 lemma ball_trivial [simp]: "ball x 0 = {}"
   by (simp add: ball_def)