New complex analysis material
authorpaulson <lp15@cam.ac.uk>
Tue Dec 15 14:40:36 2015 +0000 (2015-12-15 ago)
changeset 618489250e546ab23
parent 61846 2c79790d270d
child 61849 f8741f200f91
New complex analysis material
NEWS
src/HOL/Complex.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/NEWS	Mon Dec 14 14:05:31 2015 +0100
     1.2 +++ b/NEWS	Tue Dec 15 14:40:36 2015 +0000
     1.3 @@ -594,8 +594,8 @@
     1.4  fixpoint theorem for increasing functions in chain-complete partial
     1.5  orders.
     1.6  
     1.7 -* Multivariate_Analysis/Cauchy_Integral_Thm: Complex path integrals, Cauchy's
     1.8 -integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
     1.9 +* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals),
    1.10 +Cauchy's integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
    1.11  
    1.12  * Multivariate_Analysis: Added topological concepts such as connected components,
    1.13  homotopic paths and the inside or outside of a set.
     2.1 --- a/src/HOL/Complex.thy	Mon Dec 14 14:05:31 2015 +0100
     2.2 +++ b/src/HOL/Complex.thy	Tue Dec 15 14:40:36 2015 +0000
     2.3 @@ -784,7 +784,10 @@
     2.4    apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
     2.5    done
     2.6  
     2.7 -lemma exp_two_pi_i [simp]: "exp(2 * complex_of_real pi * ii) = 1"
     2.8 +lemma exp_pi_i [simp]: "exp(of_real pi * ii) = -1"
     2.9 +  by (metis cis_conv_exp cis_pi mult.commute)
    2.10 +
    2.11 +lemma exp_two_pi_i [simp]: "exp(2 * of_real pi * ii) = 1"
    2.12    by (simp add: exp_eq_polar complex_eq_iff)
    2.13  
    2.14  subsubsection \<open>Complex argument\<close>
     3.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Dec 14 14:05:31 2015 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Dec 15 14:40:36 2015 +0000
     3.3 @@ -2674,7 +2674,7 @@
     3.4      done
     3.5  qed
     3.6  
     3.7 -lemma pathintegral_convex_primitive:
     3.8 +lemma contour_integral_convex_primitive:
     3.9    "\<lbrakk>convex s; continuous_on s f;
    3.10      \<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>
    3.11           \<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
    3.12 @@ -2687,7 +2687,7 @@
    3.13    "\<lbrakk>convex s; finite k; continuous_on s f;
    3.14      \<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x\<rbrakk>
    3.15     \<Longrightarrow> \<exists>g. \<forall>x \<in> s. (g has_field_derivative f x) (at x within s)"
    3.16 -apply (rule pathintegral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite])
    3.17 +apply (rule contour_integral_convex_primitive [OF _ _ Cauchy_theorem_triangle_cofinite])
    3.18  prefer 3
    3.19  apply (erule continuous_on_subset)
    3.20  apply (simp add: subset_hull continuous_on_subset, assumption+)
    3.21 @@ -5029,6 +5029,35 @@
    3.22  lemma pathfinish_circlepath [simp]: "pathfinish (circlepath z r) = z + r"
    3.23    by (simp add: circlepath_def) (metis exp_two_pi_i mult.commute)
    3.24  
    3.25 +lemma circlepath_minus: "circlepath z (-r) x = circlepath z r (x + 1/2)"
    3.26 +proof -
    3.27 +  have "z + of_real r * exp (2 * pi * \<i> * (x + 1 / 2)) =
    3.28 +        z + of_real r * exp (2 * pi * \<i> * x + pi * \<i>)"
    3.29 +    by (simp add: divide_simps) (simp add: algebra_simps)
    3.30 +  also have "... = z - r * exp (2 * pi * \<i> * x)"
    3.31 +    by (simp add: exp_add)
    3.32 +  finally show ?thesis
    3.33 +    by (simp add: circlepath path_image_def sphere_def dist_norm)
    3.34 +qed
    3.35 +
    3.36 +lemma circlepath_add1: "circlepath z r (x+1) = circlepath z r x"
    3.37 +  using circlepath_minus [of z r "x+1/2"] circlepath_minus [of z "-r" x]
    3.38 +  by (simp add: add.commute)
    3.39 +
    3.40 +lemma circlepath_add_half: "circlepath z r (x + 1/2) = circlepath z r (x - 1/2)"
    3.41 +  using circlepath_add1 [of z r "x-1/2"]
    3.42 +  by (simp add: add.commute)
    3.43 +
    3.44 +lemma path_image_circlepath_minus_subset:
    3.45 +     "path_image (circlepath z (-r)) \<subseteq> path_image (circlepath z r)"
    3.46 +  apply (simp add: path_image_def image_def circlepath_minus, clarify)
    3.47 +  apply (case_tac "xa \<le> 1/2", force)
    3.48 +  apply (force simp add: circlepath_add_half)+
    3.49 +  done
    3.50 +
    3.51 +lemma path_image_circlepath_minus: "path_image (circlepath z (-r)) = path_image (circlepath z r)"
    3.52 +  using path_image_circlepath_minus_subset by fastforce
    3.53 +
    3.54  proposition has_vector_derivative_circlepath [derivative_intros]:
    3.55   "((circlepath z r) has_vector_derivative (2 * pi * ii * r * exp (2 * of_real pi * ii * of_real x)))
    3.56     (at x within X)"
    3.57 @@ -5055,7 +5084,7 @@
    3.58  lemma path_circlepath [simp]: "path (circlepath z r)"
    3.59    by (simp add: valid_path_imp_path)
    3.60  
    3.61 -proposition path_image_circlepath [simp]:
    3.62 +lemma path_image_circlepath_nonneg:
    3.63    assumes "0 \<le> r" shows "path_image (circlepath z r) = sphere z r"
    3.64  proof -
    3.65    have *: "x \<in> (\<lambda>u. z + (cmod (x - z)) * exp (\<i> * (of_real u * (of_real pi * 2)))) ` {0..1}" for x
    3.66 @@ -5081,6 +5110,11 @@
    3.67      by (force simp: assms algebra_simps norm_mult norm_minus_commute intro: *)
    3.68  qed
    3.69  
    3.70 +proposition path_image_circlepath [simp]:
    3.71 +    "path_image (circlepath z r) = sphere z (abs r)"
    3.72 +  using path_image_circlepath_minus
    3.73 +  by (force simp add: path_image_circlepath_nonneg abs_if)
    3.74 +
    3.75  lemma has_contour_integral_bound_circlepath_strong:
    3.76        "\<lbrakk>(f has_contour_integral i) (circlepath z r);
    3.77          finite k; 0 \<le> B; 0 < r;
    3.78 @@ -5104,10 +5138,7 @@
    3.79    by (simp add: circlepath_def simple_path_part_circlepath)
    3.80  
    3.81  lemma notin_path_image_circlepath [simp]: "cmod (w - z) < r \<Longrightarrow> w \<notin> path_image (circlepath z r)"
    3.82 -  apply (subst path_image_circlepath)
    3.83 -  apply (meson le_cases less_le_trans norm_not_less_zero)
    3.84 -  apply (simp add: sphere_def dist_norm norm_minus_commute)
    3.85 -  done
    3.86 +  by (simp add: sphere_def dist_norm norm_minus_commute)
    3.87  
    3.88  proposition contour_integral_circlepath:
    3.89       "0 < r \<Longrightarrow> contour_integral (circlepath z r) (\<lambda>w. 1 / (w - z)) = 2 * complex_of_real pi * \<i>"
    3.90 @@ -5195,4 +5226,803 @@
    3.91  apply (rule no_bounded_connected_component_imp_winding_number_zero [OF g])
    3.92  by (simp add: bounded_subset nb path_component_subset_connected_component)
    3.93  
    3.94 +
    3.95 +subsection\<open> Uniform convergence of path integral\<close>
    3.96 +
    3.97 +text\<open>Uniform convergence when the derivative of the path is bounded, and in particular for the special case of a circle.\<close>
    3.98 +
    3.99 +proposition contour_integral_uniform_limit:
   3.100 +  assumes ev_fint: "eventually (\<lambda>n::'a. (f n) contour_integrable_on \<gamma>) F"
   3.101 +      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"
   3.102 +      and noleB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
   3.103 +      and \<gamma>: "valid_path \<gamma>"
   3.104 +      and [simp]: "~ (trivial_limit F)"
   3.105 +  shows "l contour_integrable_on \<gamma>" "((\<lambda>n. contour_integral \<gamma> (f n)) ---> contour_integral \<gamma> l) F"
   3.106 +proof -
   3.107 +  have "0 \<le> B" by (meson noleB [of 0] atLeastAtMost_iff norm_ge_zero order_refl order_trans zero_le_one)
   3.108 +  { fix e::real
   3.109 +    assume "0 < e"
   3.110 +    then have eB: "0 < e / (\<bar>B\<bar> + 1)" by simp
   3.111 +    obtain a where fga: "\<And>x. x \<in> {0..1} \<Longrightarrow> cmod (f a (\<gamma> x) - l (\<gamma> x)) < e / (\<bar>B\<bar> + 1)"
   3.112 +               and inta: "(\<lambda>t. f a (\<gamma> t) * vector_derivative \<gamma> (at t)) integrable_on {0..1}"
   3.113 +      using eventually_happens [OF eventually_conj [OF ev_no [OF eB] ev_fint]]
   3.114 +      by (fastforce simp: contour_integrable_on path_image_def)
   3.115 +    have Ble: "B * e / (\<bar>B\<bar> + 1) \<le> e"
   3.116 +      using \<open>0 \<le> B\<close>  \<open>0 < e\<close> by (simp add: divide_simps)
   3.117 +    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}"
   3.118 +      apply (rule_tac x="\<lambda>x. f (a::'a) (\<gamma> x) * vector_derivative \<gamma> (at x)" in exI)
   3.119 +      apply (intro inta conjI ballI)
   3.120 +      apply (rule order_trans [OF _ Ble])
   3.121 +      apply (frule noleB)
   3.122 +      apply (frule fga)
   3.123 +      using \<open>0 \<le> B\<close>  \<open>0 < e\<close>
   3.124 +      apply (simp add: norm_mult left_diff_distrib [symmetric] norm_minus_commute divide_simps)
   3.125 +      apply (drule (1) mult_mono [OF less_imp_le])
   3.126 +      apply (simp_all add: mult_ac)
   3.127 +      done
   3.128 +  }
   3.129 +  then show lintg: "l contour_integrable_on \<gamma>"
   3.130 +    apply (simp add: contour_integrable_on)
   3.131 +    apply (blast intro: integrable_uniform_limit_real)
   3.132 +    done
   3.133 +  { fix e::real
   3.134 +    def B' \<equiv> "B+1"
   3.135 +    have B': "B' > 0" "B' > B" using  \<open>0 \<le> B\<close> by (auto simp: B'_def)
   3.136 +    assume "0 < e"
   3.137 +    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'"
   3.138 +      using ev_no [of "e / B' / 2"] B' by (simp add: field_simps)
   3.139 +    have ie: "integral {0..1::real} (\<lambda>x. e / 2) < e" using \<open>0 < e\<close> by simp
   3.140 +    have *: "cmod (f x (\<gamma> t) * vector_derivative \<gamma> (at t) - l (\<gamma> t) * vector_derivative \<gamma> (at t)) \<le> e / 2"
   3.141 +             if t: "t\<in>{0..1}" and leB': "2 * cmod (f x (\<gamma> t) - l (\<gamma> t)) < e / B'" for x t
   3.142 +    proof -
   3.143 +      have "2 * cmod (f x (\<gamma> t) - l (\<gamma> t)) * cmod (vector_derivative \<gamma> (at t)) \<le> e * (B/ B')"
   3.144 +        using mult_mono [OF less_imp_le [OF leB'] noleB] B' \<open>0 < e\<close> t by auto
   3.145 +      also have "... < e"
   3.146 +        by (simp add: B' \<open>0 < e\<close> mult_imp_div_pos_less)
   3.147 +      finally have "2 * cmod (f x (\<gamma> t) - l (\<gamma> t)) * cmod (vector_derivative \<gamma> (at t)) < e" .
   3.148 +      then show ?thesis
   3.149 +        by (simp add: left_diff_distrib [symmetric] norm_mult)
   3.150 +    qed
   3.151 +    have "\<forall>\<^sub>F x in F. dist (contour_integral \<gamma> (f x)) (contour_integral \<gamma> l) < e"
   3.152 +      apply (rule eventually_mono [OF eventually_conj [OF ev_no' ev_fint]])
   3.153 +      apply (simp add: dist_norm contour_integrable_on path_image_def contour_integral_integral)
   3.154 +      apply (simp add: lintg integral_diff [symmetric] contour_integrable_on [symmetric], clarify)
   3.155 +      apply (rule le_less_trans [OF integral_norm_bound_integral ie])
   3.156 +      apply (simp add: lintg integrable_diff contour_integrable_on [symmetric])
   3.157 +      apply (blast intro: *)+
   3.158 +      done
   3.159 +  }
   3.160 +  then show "((\<lambda>n. contour_integral \<gamma> (f n)) ---> contour_integral \<gamma> l) F"
   3.161 +    by (rule tendstoI)
   3.162 +qed
   3.163 +
   3.164 +proposition contour_integral_uniform_limit_circlepath:
   3.165 +  assumes ev_fint: "eventually (\<lambda>n::'a. (f n) contour_integrable_on (circlepath z r)) F"
   3.166 +      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"
   3.167 +      and [simp]: "~ (trivial_limit F)" "0 < r"
   3.168 +  shows "l contour_integrable_on (circlepath z r)" "((\<lambda>n. contour_integral (circlepath z r) (f n)) ---> contour_integral (circlepath z r) l) F"
   3.169 +by (auto simp: vector_derivative_circlepath norm_mult intro: contour_integral_uniform_limit assms)
   3.170 +
   3.171 +
   3.172 +subsection\<open> General stepping result for derivative formulas.\<close>
   3.173 +
   3.174 +lemma sum_sqs_eq:
   3.175 +  fixes x::"'a::idom" shows "x * x + y * y = x * (y * 2) \<Longrightarrow> y = x"
   3.176 +  by algebra
   3.177 +
   3.178 +proposition Cauchy_next_derivative:
   3.179 +  assumes "continuous_on (path_image \<gamma>) f'"
   3.180 +      and leB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
   3.181 +      and int: "\<And>w. w \<in> s - path_image \<gamma> \<Longrightarrow> ((\<lambda>u. f' u / (u - w)^k) has_contour_integral f w) \<gamma>"
   3.182 +      and k: "k \<noteq> 0"
   3.183 +      and "open s"
   3.184 +      and \<gamma>: "valid_path \<gamma>"
   3.185 +      and w: "w \<in> s - path_image \<gamma>"
   3.186 +    shows "(\<lambda>u. f' u / (u - w)^(Suc k)) contour_integrable_on \<gamma>"
   3.187 +      and "(f has_field_derivative (k * contour_integral \<gamma> (\<lambda>u. f' u/(u - w)^(Suc k))))
   3.188 +           (at w)"  (is "?thes2")
   3.189 +proof -
   3.190 +  have "open (s - path_image \<gamma>)" using \<open>open s\<close> closed_valid_path_image \<gamma> by blast
   3.191 +  then obtain d where "d>0" and d: "ball w d \<subseteq> s - path_image \<gamma>" using w
   3.192 +    using open_contains_ball by blast
   3.193 +  have [simp]: "\<And>n. cmod (1 + of_nat n) = 1 + of_nat n"
   3.194 +    by (metis norm_of_nat of_nat_Suc)
   3.195 +  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)
   3.196 +                         contour_integrable_on \<gamma>"
   3.197 +    apply (simp add: eventually_at)
   3.198 +    apply (rule_tac x=d in exI)
   3.199 +    apply (simp add: \<open>d > 0\<close> dist_norm field_simps, clarify)
   3.200 +    apply (rule contour_integrable_div [OF contour_integrable_diff])
   3.201 +    using int w d
   3.202 +    apply (force simp:  dist_norm norm_minus_commute intro!: has_contour_integral_integrable)+
   3.203 +    done
   3.204 +  have bim_g: "bounded (image f' (path_image \<gamma>))"
   3.205 +    by (simp add: compact_imp_bounded compact_continuous_image compact_valid_path_image assms)
   3.206 +  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"
   3.207 +    by (force simp: bounded_pos path_image_def)
   3.208 +  have twom: "\<forall>\<^sub>F n in at w.
   3.209 +               \<forall>x\<in>path_image \<gamma>.
   3.210 +                cmod ((inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / k - inverse (x - w) ^ Suc k) < e"
   3.211 +         if "0 < e" for e
   3.212 +  proof -
   3.213 +    have *: "cmod ((inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k) - inverse (x - w) ^ Suc k)   < e"
   3.214 +            if x: "x \<in> path_image \<gamma>" and "u \<noteq> w" and uwd: "cmod (u - w) < d/2"
   3.215 +                and uw_less: "cmod (u - w) < e * (d / 2) ^ (k+2) / (1 + real k)"
   3.216 +            for u x
   3.217 +    proof -
   3.218 +      def ff \<equiv> "\<lambda>n::nat. \<lambda>w. if n = 0 then inverse(x - w)^k
   3.219 +                              else if n = 1 then k / (x - w)^(Suc k)
   3.220 +                              else (k * of_real(Suc k)) / (x - w)^(k + 2)"
   3.221 +      have km1: "\<And>z::complex. z \<noteq> 0 \<Longrightarrow> z ^ (k - Suc 0) = z ^ k / z"
   3.222 +        by (simp add: field_simps) (metis Suc_pred \<open>k \<noteq> 0\<close> neq0_conv power_Suc)
   3.223 +      have ff1: "(ff i has_field_derivative ff (Suc i) z) (at z within ball w (d / 2))"
   3.224 +              if "z \<in> ball w (d / 2)" "i \<le> 1" for i z
   3.225 +      proof -
   3.226 +        have "z \<notin> path_image \<gamma>"
   3.227 +          using \<open>x \<in> path_image \<gamma>\<close> d that ball_divide_subset_numeral by blast
   3.228 +        then have xz[simp]: "x \<noteq> z" using \<open>x \<in> path_image \<gamma>\<close> by blast
   3.229 +        then have neq: "x * x + z * z \<noteq> x * (z * 2)"
   3.230 +          by (blast intro: dest!: sum_sqs_eq)
   3.231 +        with xz have "\<And>v. v \<noteq> 0 \<Longrightarrow> (x * x + z * z) * v \<noteq> (x * (z * 2) * v)" by auto
   3.232 +        then have neqq: "\<And>v. v \<noteq> 0 \<Longrightarrow> x * (x * v) + z * (z * v) \<noteq> x * (z * (2 * v))"
   3.233 +          by (simp add: algebra_simps)
   3.234 +        show ?thesis using \<open>i \<le> 1\<close>
   3.235 +          apply (simp add: ff_def dist_norm Nat.le_Suc_eq km1, safe)
   3.236 +          apply (rule derivative_eq_intros | simp add: km1 | simp add: field_simps neq neqq)+
   3.237 +          done
   3.238 +      qed
   3.239 +      { fix a::real and b::real assume ab: "a > 0" "b > 0"
   3.240 +        then have "k * (1 + real k) * (1 / a) \<le> k * (1 + real k) * (4 / b) \<longleftrightarrow> b \<le> 4 * a"
   3.241 +          apply (subst mult_le_cancel_left_pos)
   3.242 +          using \<open>k \<noteq> 0\<close>
   3.243 +          apply (auto simp: divide_simps)
   3.244 +          done
   3.245 +        with ab have "real k * (1 + real k) / a \<le> (real k * 4 + real k * real k * 4) / b \<longleftrightarrow> b \<le> 4 * a"
   3.246 +          by (simp add: field_simps)
   3.247 +      } note canc = this
   3.248 +      have ff2: "cmod (ff (Suc 1) v) \<le> real (k * (k + 1)) / (d / 2) ^ (k + 2)"
   3.249 +                if "v \<in> ball w (d / 2)" for v
   3.250 +      proof -
   3.251 +        have "d/2 \<le> cmod (x - v)" using d x that
   3.252 +          apply (simp add: dist_norm path_image_def ball_def not_less [symmetric] del: divide_const_simps, clarify)
   3.253 +          apply (drule subsetD)
   3.254 +           prefer 2 apply blast
   3.255 +          apply (metis norm_minus_commute norm_triangle_half_r CollectI)
   3.256 +          done
   3.257 +        then have "d \<le> cmod (x - v) * 2"
   3.258 +          by (simp add: divide_simps)
   3.259 +        then have dpow_le: "d ^ (k+2) \<le> (cmod (x - v) * 2) ^ (k+2)"
   3.260 +          using \<open>0 < d\<close> order_less_imp_le power_mono by blast
   3.261 +        have "x \<noteq> v" using that
   3.262 +          using \<open>x \<in> path_image \<gamma>\<close> ball_divide_subset_numeral d by fastforce
   3.263 +        then show ?thesis
   3.264 +        using \<open>d > 0\<close>
   3.265 +        apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc)
   3.266 +        using dpow_le
   3.267 +        apply (simp add: algebra_simps divide_simps mult_less_0_iff)
   3.268 +        done
   3.269 +      qed
   3.270 +      have ub: "u \<in> ball w (d / 2)"
   3.271 +        using uwd by (simp add: dist_commute dist_norm)
   3.272 +      have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
   3.273 +                  \<le> (real k * 4 + real k * real k * 4) * (cmod (u - w) * cmod (u - w)) / (d * (d * (d / 2) ^ k))"
   3.274 +        using complex_taylor [OF _ ff1 ff2 _ ub, of w, simplified]
   3.275 +        by (simp add: ff_def \<open>0 < d\<close>)
   3.276 +      then have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
   3.277 +                  \<le> (cmod (u - w) * real k) * (1 + real k) * cmod (u - w) / (d / 2) ^ (k+2)"
   3.278 +        by (simp add: field_simps)
   3.279 +      then have "cmod (inverse (x - u) ^ k - (inverse (x - w) ^ k + of_nat k * (u - w) / ((x - w) * (x - w) ^ k)))
   3.280 +                 / (cmod (u - w) * real k)
   3.281 +                  \<le> (1 + real k) * cmod (u - w) / (d / 2) ^ (k+2)"
   3.282 +        using \<open>k \<noteq> 0\<close> \<open>u \<noteq> w\<close> by (simp add: mult_ac zero_less_mult_iff pos_divide_le_eq)
   3.283 +      also have "... < e"
   3.284 +        using uw_less \<open>0 < d\<close> by (simp add: mult_ac divide_simps)
   3.285 +      finally have e: "cmod (inverse (x-u)^k - (inverse (x-w)^k + of_nat k * (u-w) / ((x-w) * (x-w)^k)))
   3.286 +                        / cmod ((u - w) * real k)   <   e"
   3.287 +        by (simp add: norm_mult)
   3.288 +      have "x \<noteq> u"
   3.289 +        using uwd \<open>0 < d\<close> x d by (force simp: dist_norm ball_def norm_minus_commute)
   3.290 +      show ?thesis
   3.291 +        apply (rule le_less_trans [OF _ e])
   3.292 +        using \<open>k \<noteq> 0\<close> \<open>x \<noteq> u\<close>  \<open>u \<noteq> w\<close>
   3.293 +        apply (simp add: field_simps norm_divide [symmetric])
   3.294 +        done
   3.295 +    qed
   3.296 +    show ?thesis
   3.297 +      unfolding eventually_at
   3.298 +      apply (rule_tac x = "min (d/2) ((e*(d/2)^(k + 2))/(Suc k))" in exI)
   3.299 +      apply (force simp: \<open>d > 0\<close> dist_norm that simp del: power_Suc intro: *)
   3.300 +      done
   3.301 +  qed
   3.302 +  have 2: "\<forall>\<^sub>F n in at w.
   3.303 +              \<forall>x\<in>path_image \<gamma>.
   3.304 +               cmod (f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / of_nat k - f' x / (x - w) ^ Suc k) < e"
   3.305 +          if "0 < e" for e
   3.306 +  proof -
   3.307 +    have *: "cmod (f' (\<gamma> x) * (inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
   3.308 +                        f' (\<gamma> x) / ((\<gamma> x - w) * (\<gamma> x - w) ^ k)) < e"
   3.309 +              if ec: "cmod ((inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
   3.310 +                      inverse (\<gamma> x - w) * inverse (\<gamma> x - w) ^ k) < e / C"
   3.311 +                 and x: "0 \<le> x" "x \<le> 1"
   3.312 +              for u x
   3.313 +    proof (cases "(f' (\<gamma> x)) = 0")
   3.314 +      case True then show ?thesis by (simp add: \<open>0 < e\<close>)
   3.315 +    next
   3.316 +      case False
   3.317 +      have "cmod (f' (\<gamma> x) * (inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
   3.318 +                        f' (\<gamma> x) / ((\<gamma> x - w) * (\<gamma> x - w) ^ k)) =
   3.319 +            cmod (f' (\<gamma> x) * ((inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
   3.320 +                             inverse (\<gamma> x - w) * inverse (\<gamma> x - w) ^ k))"
   3.321 +        by (simp add: field_simps)
   3.322 +      also have "... = cmod (f' (\<gamma> x)) *
   3.323 +                       cmod ((inverse (\<gamma> x - u) ^ k - inverse (\<gamma> x - w) ^ k) / ((u - w) * k) -
   3.324 +                             inverse (\<gamma> x - w) * inverse (\<gamma> x - w) ^ k)"
   3.325 +        by (simp add: norm_mult)
   3.326 +      also have "... < cmod (f' (\<gamma> x)) * (e/C)"
   3.327 +        apply (rule mult_strict_left_mono [OF ec])
   3.328 +        using False by simp
   3.329 +      also have "... \<le> e" using C
   3.330 +        by (metis False \<open>0 < e\<close> frac_le less_eq_real_def mult.commute pos_le_divide_eq x zero_less_norm_iff)
   3.331 +      finally show ?thesis .
   3.332 +    qed
   3.333 +    show ?thesis
   3.334 +      using twom [OF divide_pos_pos [OF that \<open>C > 0\<close>]]   unfolding path_image_def
   3.335 +      by (force intro: * elim: eventually_mono)
   3.336 +  qed
   3.337 +  show "(\<lambda>u. f' u / (u - w) ^ (Suc k)) contour_integrable_on \<gamma>"
   3.338 +    by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
   3.339 +  have *: "(\<lambda>n. contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / k))
   3.340 +           --w--> contour_integral \<gamma> (\<lambda>u. f' u / (u - w) ^ (Suc k))"
   3.341 +    by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
   3.342 +  have **: "contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k)) =
   3.343 +              (f u - f w) / (u - w) / k"
   3.344 +           if "dist u w < d" for u
   3.345 +    apply (rule contour_integral_unique)
   3.346 +    apply (simp add: diff_divide_distrib algebra_simps)
   3.347 +    apply (rule has_contour_integral_diff; rule has_contour_integral_div; simp add: field_simps; rule int)
   3.348 +    apply (metis contra_subsetD d dist_commute mem_ball that)
   3.349 +    apply (rule w)
   3.350 +    done
   3.351 +  show ?thes2
   3.352 +    apply (simp add: DERIV_within_iff del: power_Suc)
   3.353 +    apply (rule Lim_transform_at [OF \<open>0 < d\<close> _ tendsto_mult_left [OF *]])
   3.354 +    apply (simp add: \<open>k \<noteq> 0\<close> **)
   3.355 +    done
   3.356 +qed
   3.357 +
   3.358 +corollary Cauchy_next_derivative_circlepath:
   3.359 +  assumes contf: "continuous_on (path_image (circlepath z r)) f"
   3.360 +      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)"
   3.361 +      and k: "k \<noteq> 0"
   3.362 +      and w: "w \<in> ball z r"
   3.363 +    shows "(\<lambda>u. f u / (u - w)^(Suc k)) contour_integrable_on (circlepath z r)"
   3.364 +           (is "?thes1")
   3.365 +      and "(g has_field_derivative (k * contour_integral (circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k)))) (at w)"
   3.366 +           (is "?thes2")
   3.367 +proof -
   3.368 +  have "r > 0" using w
   3.369 +    using ball_eq_empty by fastforce
   3.370 +  have wim: "w \<in> ball z r - path_image (circlepath z r)"
   3.371 +    using w by (auto simp: dist_norm)
   3.372 +  show ?thes1 ?thes2
   3.373 +    by (rule Cauchy_next_derivative [OF contf _ int k open_ball valid_path_circlepath wim, where B = "2 * pi * \<bar>r\<bar>"];
   3.374 +        auto simp: vector_derivative_circlepath norm_mult)+
   3.375 +qed
   3.376 +
   3.377 +
   3.378 +text\<open> In particular, the first derivative formula.\<close>
   3.379 +
   3.380 +proposition Cauchy_derivative_integral_circlepath:
   3.381 +  assumes contf: "continuous_on (cball z r) f"
   3.382 +      and holf: "f holomorphic_on ball z r"
   3.383 +      and w: "w \<in> ball z r"
   3.384 +    shows "(\<lambda>u. f u/(u - w)^2) contour_integrable_on (circlepath z r)"
   3.385 +           (is "?thes1")
   3.386 +      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)"
   3.387 +           (is "?thes2")
   3.388 +proof -
   3.389 +  have [simp]: "r \<ge> 0" using w
   3.390 +    using ball_eq_empty by fastforce
   3.391 +  have f: "continuous_on (path_image (circlepath z r)) f"
   3.392 +    by (rule continuous_on_subset [OF contf]) (force simp add: cball_def sphere_def)
   3.393 +  have int: "\<And>w. dist z w < r \<Longrightarrow>
   3.394 +                 ((\<lambda>u. f u / (u - w)) has_contour_integral (\<lambda>x. 2 * of_real pi * ii * f x) w) (circlepath z r)"
   3.395 +    by (rule Cauchy_integral_circlepath [OF contf holf]) (simp add: dist_norm norm_minus_commute)
   3.396 +  show ?thes1
   3.397 +    apply (simp add: power2_eq_square)
   3.398 +    apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1, simplified])
   3.399 +    apply (blast intro: int)
   3.400 +    done
   3.401 +  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)"
   3.402 +    apply (simp add: power2_eq_square)
   3.403 +    apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "\<lambda>x. 2 * of_real pi * ii * f x", simplified])
   3.404 +    apply (blast intro: int)
   3.405 +    done
   3.406 +  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)"
   3.407 +    by (rule DERIV_cdivide [where f = "\<lambda>x. 2 * of_real pi * \<i> * f x" and c = "2 * of_real pi * \<i>", simplified])
   3.408 +  show ?thes2
   3.409 +    by simp (rule fder)
   3.410 +qed
   3.411 +
   3.412 +subsection\<open> Existence of all higher derivatives.\<close>
   3.413 +
   3.414 +proposition derivative_is_holomorphic:
   3.415 +  assumes "open s"
   3.416 +      and fder: "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z)"
   3.417 +    shows "f' holomorphic_on s"
   3.418 +proof -
   3.419 +  have *: "\<exists>h. (f' has_field_derivative h) (at z)" if "z \<in> s" for z
   3.420 +  proof -
   3.421 +    obtain r where "r > 0" and r: "cball z r \<subseteq> s"
   3.422 +      using open_contains_cball \<open>z \<in> s\<close> \<open>open s\<close> by blast
   3.423 +    then have holf_cball: "f holomorphic_on cball z r"
   3.424 +      apply (simp add: holomorphic_on_def)
   3.425 +      using complex_differentiable_at_within complex_differentiable_def fder by blast
   3.426 +    then have "continuous_on (path_image (circlepath z r)) f"
   3.427 +      using \<open>r > 0\<close> by (force elim: holomorphic_on_subset [THEN holomorphic_on_imp_continuous_on])
   3.428 +    then have contfpi: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1/(2 * of_real pi*ii) * f x)"
   3.429 +      by (auto intro: continuous_intros)+
   3.430 +    have contf_cball: "continuous_on (cball z r) f" using holf_cball
   3.431 +      by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_subset)
   3.432 +    have holf_ball: "f holomorphic_on ball z r" using holf_cball
   3.433 +      using ball_subset_cball holomorphic_on_subset by blast
   3.434 +    { fix w  assume w: "w \<in> ball z r"  
   3.435 +      have intf: "(\<lambda>u. f u / (u - w)\<^sup>2) contour_integrable_on circlepath z r"
   3.436 +        by (blast intro: w Cauchy_derivative_integral_circlepath [OF contf_cball holf_ball])
   3.437 +      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))
   3.438 +                  (at w)"
   3.439 +        by (blast intro: w Cauchy_derivative_integral_circlepath [OF contf_cball holf_ball])
   3.440 +      have f'_eq: "f' w = contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2) / (2 * of_real pi * \<i>)"
   3.441 +        using fder' ball_subset_cball r w by (force intro: DERIV_unique [OF fder])
   3.442 +      have "((\<lambda>u. f u / (u - w)\<^sup>2 / (2 * of_real pi * \<i>)) has_contour_integral
   3.443 +                contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2) / (2 * of_real pi * \<i>))
   3.444 +                (circlepath z r)"
   3.445 +        by (rule Cauchy_Integral_Thm.has_contour_integral_div [OF has_contour_integral_integral [OF intf]])
   3.446 +      then have "((\<lambda>u. f u / (2 * of_real pi * \<i> * (u - w)\<^sup>2)) has_contour_integral
   3.447 +                contour_integral (circlepath z r) (\<lambda>u. f u / (u - w)\<^sup>2) / (2 * of_real pi * \<i>))
   3.448 +                (circlepath z r)"
   3.449 +        by (simp add: algebra_simps)
   3.450 +      then have "((\<lambda>u. f u / (2 * of_real pi * \<i> * (u - w)\<^sup>2)) has_contour_integral f' w) (circlepath z r)"
   3.451 +        by (simp add: f'_eq)
   3.452 +    } note * = this
   3.453 +    show ?thesis
   3.454 +      apply (rule exI)
   3.455 +      apply (rule Cauchy_next_derivative_circlepath [OF contfpi, of 2 f', simplified])
   3.456 +      apply (simp_all add: \<open>0 < r\<close> * dist_norm)
   3.457 +      done
   3.458 +  qed
   3.459 +  show ?thesis
   3.460 +    by (simp add: holomorphic_on_open [OF \<open>open s\<close>] *)
   3.461 +qed
   3.462 +
   3.463 +lemma holomorphic_deriv [holomorphic_intros]: 
   3.464 +    "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv f) holomorphic_on s"
   3.465 +by (metis DERIV_deriv_iff_complex_differentiable at_within_open derivative_is_holomorphic holomorphic_on_def)
   3.466 +
   3.467 +lemma analytic_deriv: "f analytic_on s \<Longrightarrow> (deriv f) analytic_on s"
   3.468 +  using analytic_on_holomorphic holomorphic_deriv by auto
   3.469 +
   3.470 +lemma holomorphic_higher_deriv [holomorphic_intros]: "\<lbrakk>f holomorphic_on s; open s\<rbrakk> \<Longrightarrow> (deriv ^^ n) f holomorphic_on s"
   3.471 +  by (induction n) (auto simp: holomorphic_deriv)
   3.472 +
   3.473 +lemma analytic_higher_deriv: "f analytic_on s \<Longrightarrow> (deriv ^^ n) f analytic_on s"
   3.474 +  unfolding analytic_on_def using holomorphic_higher_deriv by blast
   3.475 +
   3.476 +lemma has_field_derivative_higher_deriv: 
   3.477 +     "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> 
   3.478 +      \<Longrightarrow> ((deriv ^^ n) f has_field_derivative (deriv ^^ (Suc n)) f x) (at x)"
   3.479 +by (metis (no_types, hide_lams) DERIV_deriv_iff_complex_differentiable at_within_open comp_apply 
   3.480 +         funpow.simps(2) holomorphic_higher_deriv holomorphic_on_def)
   3.481 +
   3.482 +
   3.483 +subsection\<open> Morera's theorem.\<close>
   3.484 +
   3.485 +lemma Morera_local_triangle_ball:
   3.486 +  assumes "\<And>z. z \<in> s
   3.487 +          \<Longrightarrow> \<exists>e a. 0 < e \<and> z \<in> ball a e \<and> continuous_on (ball a e) f \<and>
   3.488 +                    (\<forall>b c. closed_segment b c \<subseteq> ball a e
   3.489 +                           \<longrightarrow> contour_integral (linepath a b) f +
   3.490 +                               contour_integral (linepath b c) f +
   3.491 +                               contour_integral (linepath c a) f = 0)"
   3.492 +  shows "f analytic_on s"
   3.493 +proof -
   3.494 +  { fix z  assume "z \<in> s"
   3.495 +    with assms obtain e a where 
   3.496 +            "0 < e" and z: "z \<in> ball a e" and contf: "continuous_on (ball a e) f"
   3.497 +        and 0: "\<And>b c. closed_segment b c \<subseteq> ball a e
   3.498 +                      \<Longrightarrow> contour_integral (linepath a b) f +
   3.499 +                          contour_integral (linepath b c) f +
   3.500 +                          contour_integral (linepath c a) f = 0"
   3.501 +      by fastforce
   3.502 +    have az: "dist a z < e" using mem_ball z by blast
   3.503 +    have sb_ball: "ball z (e - dist a z) \<subseteq> ball a e"
   3.504 +      by (simp add: dist_commute ball_subset_ball_iff)
   3.505 +    have "\<exists>e>0. f holomorphic_on ball z e"
   3.506 +      apply (rule_tac x="e - dist a z" in exI)
   3.507 +      apply (simp add: az)
   3.508 +      apply (rule holomorphic_on_subset [OF _ sb_ball])
   3.509 +      apply (rule derivative_is_holomorphic[OF open_ball])
   3.510 +      apply (rule triangle_contour_integrals_starlike_primitive [OF contf _ open_ball, of a])
   3.511 +         apply (simp_all add: 0 \<open>0 < e\<close>)
   3.512 +      apply (meson \<open>0 < e\<close> centre_in_ball convex_ball convex_contains_segment mem_ball)
   3.513 +      done
   3.514 +  }
   3.515 +  then show ?thesis
   3.516 +    by (simp add: analytic_on_def)
   3.517 +qed
   3.518 +
   3.519 +lemma Morera_local_triangle:
   3.520 +  assumes "\<And>z. z \<in> s
   3.521 +          \<Longrightarrow> \<exists>t. open t \<and> z \<in> t \<and> continuous_on t f \<and>
   3.522 +                  (\<forall>a b c. convex hull {a,b,c} \<subseteq> t
   3.523 +                              \<longrightarrow> contour_integral (linepath a b) f +
   3.524 +                                  contour_integral (linepath b c) f +
   3.525 +                                  contour_integral (linepath c a) f = 0)"
   3.526 +  shows "f analytic_on s"
   3.527 +proof -
   3.528 +  { fix z  assume "z \<in> s"
   3.529 +    with assms obtain t where 
   3.530 +            "open t" and z: "z \<in> t" and contf: "continuous_on t f"
   3.531 +        and 0: "\<And>a b c. convex hull {a,b,c} \<subseteq> t
   3.532 +                      \<Longrightarrow> contour_integral (linepath a b) f +
   3.533 +                          contour_integral (linepath b c) f +
   3.534 +                          contour_integral (linepath c a) f = 0"
   3.535 +      by force
   3.536 +    then obtain e where "e>0" and e: "ball z e \<subseteq> t" 
   3.537 +      using open_contains_ball by blast
   3.538 +    have [simp]: "continuous_on (ball z e) f" using contf
   3.539 +      using continuous_on_subset e by blast
   3.540 +    have "\<exists>e a. 0 < e \<and>
   3.541 +               z \<in> ball a e \<and>
   3.542 +               continuous_on (ball a e) f \<and>
   3.543 +               (\<forall>b c. closed_segment b c \<subseteq> ball a e \<longrightarrow>
   3.544 +                      contour_integral (linepath a b) f + contour_integral (linepath b c) f + contour_integral (linepath c a) f = 0)"
   3.545 +      apply (rule_tac x=e in exI)
   3.546 +      apply (rule_tac x=z in exI)
   3.547 +      apply (simp add: \<open>e > 0\<close>, clarify)
   3.548 +      apply (rule 0)
   3.549 +      apply (meson z \<open>0 < e\<close> centre_in_ball closed_segment_subset convex_ball dual_order.trans e starlike_convex_subset)
   3.550 +      done
   3.551 +  }
   3.552 +  then show ?thesis
   3.553 +    by (simp add: Morera_local_triangle_ball)
   3.554 +qed
   3.555 +
   3.556 +proposition Morera_triangle:
   3.557 +    "\<lbrakk>continuous_on s f; open s; 
   3.558 +      \<And>a b c. convex hull {a,b,c} \<subseteq> s
   3.559 +              \<longrightarrow> contour_integral (linepath a b) f +
   3.560 +                  contour_integral (linepath b c) f +
   3.561 +                  contour_integral (linepath c a) f = 0\<rbrakk>
   3.562 +     \<Longrightarrow> f analytic_on s"
   3.563 +  using Morera_local_triangle by blast
   3.564 +
   3.565 +
   3.566 +
   3.567 +subsection\<open> Combining theorems for higher derivatives including Leibniz rule.\<close>
   3.568 +
   3.569 +lemma higher_deriv_linear [simp]: 
   3.570 +    "(deriv ^^ n) (\<lambda>w. c*w) = (\<lambda>z. if n = 0 then c*z else if n = 1 then c else 0)"
   3.571 +  by (induction n) (auto simp: deriv_const deriv_linear)
   3.572 +
   3.573 +lemma higher_deriv_const [simp]: "(deriv ^^ n) (\<lambda>w. c) = (\<lambda>w. if n=0 then c else 0)"
   3.574 +  by (induction n) (auto simp: deriv_const)
   3.575 +
   3.576 +lemma higher_deriv_ident [simp]:
   3.577 +     "(deriv ^^ n) (\<lambda>w. w) z = (if n = 0 then z else if n = 1 then 1 else 0)"
   3.578 +  apply (induction n)
   3.579 +  apply (simp_all add: deriv_ident funpow_Suc_right del: funpow.simps, simp)
   3.580 +  done
   3.581 +
   3.582 +corollary higher_deriv_id [simp]:
   3.583 +     "(deriv ^^ n) id z = (if n = 0 then z else if n = 1 then 1 else 0)"
   3.584 +  by (simp add: id_def)
   3.585 +
   3.586 +lemma has_complex_derivative_funpow_1: 
   3.587 +     "\<lbrakk>(f has_field_derivative 1) (at z); f z = z\<rbrakk> \<Longrightarrow> (f^^n has_field_derivative 1) (at z)"
   3.588 +  apply (induction n)
   3.589 +  apply auto
   3.590 +  apply (metis DERIV_ident DERIV_transform_at id_apply zero_less_one)
   3.591 +  by (metis DERIV_chain comp_funpow comp_id funpow_swap1 mult.right_neutral)
   3.592 +
   3.593 +proposition higher_deriv_uminus: 
   3.594 +  assumes "f holomorphic_on s" "open s" and z: "z \<in> s"
   3.595 +    shows "(deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
   3.596 +using z
   3.597 +proof (induction n arbitrary: z)
   3.598 +  case 0 then show ?case by simp
   3.599 +next
   3.600 +  case (Suc n z) 
   3.601 +  have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
   3.602 +    using Suc.prems assms has_field_derivative_higher_deriv by auto
   3.603 +  show ?case
   3.604 +    apply simp
   3.605 +    apply (rule DERIV_imp_deriv)
   3.606 +    apply (rule DERIV_transform_within_open [of "\<lambda>w. -((deriv ^^ n) f w)"])
   3.607 +    apply (rule derivative_eq_intros | rule * refl assms Suc)+
   3.608 +    apply (simp add: Suc)
   3.609 +    done
   3.610 +qed
   3.611 +
   3.612 +proposition higher_deriv_add: 
   3.613 +  fixes z::complex
   3.614 +  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
   3.615 +    shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
   3.616 +using z
   3.617 +proof (induction n arbitrary: z)
   3.618 +  case 0 then show ?case by simp
   3.619 +next
   3.620 +  case (Suc n z) 
   3.621 +  have *: "((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
   3.622 +          "((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
   3.623 +    using Suc.prems assms has_field_derivative_higher_deriv by auto
   3.624 +  show ?case
   3.625 +    apply simp
   3.626 +    apply (rule DERIV_imp_deriv)
   3.627 +    apply (rule DERIV_transform_within_open [of "\<lambda>w. (deriv ^^ n) f w + (deriv ^^ n) g w"])
   3.628 +    apply (rule derivative_eq_intros | rule * refl assms Suc)+
   3.629 +    apply (simp add: Suc)
   3.630 +    done
   3.631 +qed
   3.632 +
   3.633 +corollary higher_deriv_diff: 
   3.634 +  fixes z::complex
   3.635 +  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
   3.636 +    shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
   3.637 +  apply (simp only: Groups.group_add_class.diff_conv_add_uminus higher_deriv_add)
   3.638 +  apply (subst higher_deriv_add)
   3.639 +  using assms holomorphic_on_minus apply (auto simp: higher_deriv_uminus)
   3.640 +  done
   3.641 +
   3.642 +
   3.643 +lemma bb: "Suc n choose k = (n choose k) + (if k = 0 then 0 else (n choose (k - 1)))"
   3.644 +  by (simp add: Binomial.binomial.simps)
   3.645 +
   3.646 +proposition higher_deriv_mult:
   3.647 +  fixes z::complex
   3.648 +  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
   3.649 +    shows "(deriv ^^ n) (\<lambda>w. f w * g w) z = 
   3.650 +           (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
   3.651 +using z
   3.652 +proof (induction n arbitrary: z)
   3.653 +  case 0 then show ?case by simp
   3.654 +next
   3.655 +  case (Suc n z) 
   3.656 +  have *: "\<And>n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) z) (at z)"
   3.657 +          "\<And>n. ((deriv ^^ n) g has_field_derivative deriv ((deriv ^^ n) g) z) (at z)"
   3.658 +    using Suc.prems assms has_field_derivative_higher_deriv by auto
   3.659 +  have sumeq: "(\<Sum>i = 0..n.
   3.660 +               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)) =
   3.661 +            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))"
   3.662 +    apply (simp add: bb distrib_right algebra_simps setsum.distrib)
   3.663 +    apply (subst (4) setsum_Suc_reindex)
   3.664 +    apply (auto simp: algebra_simps Suc_diff_le intro: setsum.cong)
   3.665 +    done
   3.666 +  show ?case
   3.667 +    apply (simp only: funpow.simps o_apply)
   3.668 +    apply (rule DERIV_imp_deriv)
   3.669 +    apply (rule DERIV_transform_within_open 
   3.670 +             [of "\<lambda>w. (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f w * (deriv ^^ (n - i)) g w)"])
   3.671 +    apply (simp add: algebra_simps)
   3.672 +    apply (rule DERIV_cong [OF DERIV_setsum])
   3.673 +    apply (rule DERIV_cmult)
   3.674 +    apply (auto simp: intro: DERIV_mult * sumeq \<open>open s\<close> Suc.prems Suc.IH [symmetric])
   3.675 +    done
   3.676 +qed
   3.677 +
   3.678 +
   3.679 +proposition higher_deriv_transform_within_open:
   3.680 +  fixes z::complex
   3.681 +  assumes "f holomorphic_on s" "g holomorphic_on s" "open s" and z: "z \<in> s"
   3.682 +      and fg: "\<And>w. w \<in> s \<Longrightarrow> f w = g w"
   3.683 +    shows "(deriv ^^ i) f z = (deriv ^^ i) g z"
   3.684 +using z
   3.685 +by (induction i arbitrary: z) 
   3.686 +   (auto simp: fg intro: complex_derivative_transform_within_open holomorphic_higher_deriv assms)
   3.687 +
   3.688 +proposition higher_deriv_compose_linear:
   3.689 +  fixes z::complex
   3.690 +  assumes f: "f holomorphic_on t" and s: "open s" and t: "open t" and z: "z \<in> s"
   3.691 +      and fg: "\<And>w. w \<in> s \<Longrightarrow> u * w \<in> t"
   3.692 +    shows "(deriv ^^ n) (\<lambda>w. f (u * w)) z = u^n * (deriv ^^ n) f (u * z)"
   3.693 +using z
   3.694 +proof (induction n arbitrary: z)
   3.695 +  case 0 then show ?case by simp
   3.696 +next
   3.697 +  case (Suc n z) 
   3.698 +  have holo0: "f holomorphic_on op * u ` s"
   3.699 +    by (meson fg f holomorphic_on_subset image_subset_iff)
   3.700 +  have holo1: "(\<lambda>w. f (u * w)) holomorphic_on s"
   3.701 +    apply (rule holomorphic_on_compose [where g=f, unfolded o_def])
   3.702 +    apply (rule holo0 holomorphic_intros)+
   3.703 +    done
   3.704 +  have holo2: "(\<lambda>z. u ^ n * (deriv ^^ n) f (u * z)) holomorphic_on s"
   3.705 +    apply (rule holomorphic_intros)+
   3.706 +    apply (rule holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def])
   3.707 +    apply (rule holomorphic_intros)
   3.708 +    apply (rule holomorphic_on_subset [where s=t])
   3.709 +    apply (rule holomorphic_intros assms)+
   3.710 +    apply (blast intro: fg)
   3.711 +    done
   3.712 +  have "deriv ((deriv ^^ n) (\<lambda>w. f (u * w))) z = deriv (\<lambda>z. u^n * (deriv ^^ n) f (u*z)) z"
   3.713 +    apply (rule complex_derivative_transform_within_open [OF _ holo2 s Suc.prems])
   3.714 +    apply (rule holomorphic_higher_deriv [OF holo1 s])
   3.715 +    apply (simp add: Suc.IH)
   3.716 +    done
   3.717 +  also have "... = u^n * deriv (\<lambda>z. (deriv ^^ n) f (u * z)) z"
   3.718 +    apply (rule complex_derivative_cmult)
   3.719 +    apply (rule analytic_on_imp_differentiable_at [OF _ Suc.prems])
   3.720 +    apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and t=t, unfolded o_def])
   3.721 +    apply (simp add: analytic_on_linear)
   3.722 +    apply (simp add: analytic_on_open f holomorphic_higher_deriv t)
   3.723 +    apply (blast intro: fg)
   3.724 +    done
   3.725 +  also have "... = u * u ^ n * deriv ((deriv ^^ n) f) (u * z)"
   3.726 +      apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "op*u", unfolded o_def])
   3.727 +      apply (rule derivative_intros)
   3.728 +      using Suc.prems complex_differentiable_def f fg has_field_derivative_higher_deriv t apply blast
   3.729 +      apply (simp add: deriv_linear)
   3.730 +      done
   3.731 +  finally show ?case
   3.732 +    by simp
   3.733 +qed
   3.734 +
   3.735 +lemma higher_deriv_add_at: 
   3.736 +  assumes "f analytic_on {z}" "g analytic_on {z}"
   3.737 +    shows "(deriv ^^ n) (\<lambda>w. f w + g w) z = (deriv ^^ n) f z + (deriv ^^ n) g z"
   3.738 +proof -
   3.739 +  have "f analytic_on {z} \<and> g analytic_on {z}"
   3.740 +    using assms by blast
   3.741 +  with higher_deriv_add show ?thesis
   3.742 +    by (auto simp: analytic_at_two)
   3.743 +qed
   3.744 +
   3.745 +lemma higher_deriv_diff_at: 
   3.746 +  assumes "f analytic_on {z}" "g analytic_on {z}"
   3.747 +    shows "(deriv ^^ n) (\<lambda>w. f w - g w) z = (deriv ^^ n) f z - (deriv ^^ n) g z"
   3.748 +proof -
   3.749 +  have "f analytic_on {z} \<and> g analytic_on {z}"
   3.750 +    using assms by blast
   3.751 +  with higher_deriv_diff show ?thesis
   3.752 +    by (auto simp: analytic_at_two)
   3.753 +qed
   3.754 +
   3.755 +lemma higher_deriv_uminus_at: 
   3.756 +   "f analytic_on {z}  \<Longrightarrow> (deriv ^^ n) (\<lambda>w. -(f w)) z = - ((deriv ^^ n) f z)"
   3.757 +  using higher_deriv_uminus
   3.758 +    by (auto simp: analytic_at)
   3.759 +
   3.760 +lemma higher_deriv_mult_at: 
   3.761 +  assumes "f analytic_on {z}" "g analytic_on {z}"
   3.762 +    shows "(deriv ^^ n) (\<lambda>w. f w * g w) z = 
   3.763 +           (\<Sum>i = 0..n. of_nat (n choose i) * (deriv ^^ i) f z * (deriv ^^ (n - i)) g z)"
   3.764 +proof -
   3.765 +  have "f analytic_on {z} \<and> g analytic_on {z}"
   3.766 +    using assms by blast
   3.767 +  with higher_deriv_mult show ?thesis
   3.768 +    by (auto simp: analytic_at_two)
   3.769 +qed
   3.770 +
   3.771 +
   3.772 +text\<open> Nonexistence of isolated singularities and a stronger integral formula.\<close>
   3.773 +
   3.774 +proposition no_isolated_singularity:
   3.775 +  fixes z::complex
   3.776 +  assumes f: "continuous_on s f" and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k"
   3.777 +    shows "f holomorphic_on s"
   3.778 +proof -
   3.779 +  { fix z 
   3.780 +    assume "z \<in> s" and cdf: "\<And>x. x\<in>s - k \<Longrightarrow> f complex_differentiable at x"
   3.781 +    have "f complex_differentiable at z"
   3.782 +    proof (cases "z \<in> k")
   3.783 +      case False then show ?thesis by (blast intro: cdf \<open>z \<in> s\<close>)
   3.784 +    next
   3.785 +      case True
   3.786 +      with finite_set_avoid [OF k, of z] 
   3.787 +      obtain d where "d>0" and d: "\<And>x. \<lbrakk>x\<in>k; x \<noteq> z\<rbrakk> \<Longrightarrow> d \<le> dist z x"
   3.788 +        by blast
   3.789 +      obtain e where "e>0" and e: "ball z e \<subseteq> s" 
   3.790 +        using  s \<open>z \<in> s\<close> by (force simp add: open_contains_ball)
   3.791 +      have fde: "continuous_on (ball z (min d e)) f"
   3.792 +        by (metis Int_iff ball_min_Int continuous_on_subset e f subsetI)
   3.793 +      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))"
   3.794 +        apply (rule contour_integral_convex_primitive [OF convex_ball fde])
   3.795 +        apply (rule Cauchy_theorem_triangle_cofinite [OF _ k])
   3.796 +         apply (metis continuous_on_subset [OF fde] closed_segment_subset convex_ball starlike_convex_subset)
   3.797 +        apply (rule cdf)
   3.798 +        apply (metis Diff_iff Int_iff ball_min_Int bot_least contra_subsetD convex_ball e insert_subset 
   3.799 +               interior_mono interior_subset subset_hull)
   3.800 +        done
   3.801 +      then have "f holomorphic_on ball z (min d e)"
   3.802 +        by (metis open_ball at_within_open derivative_is_holomorphic)
   3.803 +      then show ?thesis
   3.804 +        unfolding holomorphic_on_def
   3.805 +        by (metis open_ball \<open>0 < d\<close> \<open>0 < e\<close> at_within_open centre_in_ball min_less_iff_conj)
   3.806 +    qed
   3.807 +  }
   3.808 +  with holf s k show ?thesis
   3.809 +    by (simp add: holomorphic_on_open open_Diff finite_imp_closed complex_differentiable_def [symmetric])
   3.810 +qed
   3.811 +
   3.812 +proposition Cauchy_integral_formula_convex:
   3.813 +    assumes s: "convex s" and k: "finite k" and contf: "continuous_on s f"
   3.814 +        and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f complex_differentiable at x)"
   3.815 +        and z: "z \<in> interior s" and vpg: "valid_path \<gamma>"
   3.816 +        and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
   3.817 +      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
   3.818 +  apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf])
   3.819 +  apply (simp add: holomorphic_on_open [symmetric] complex_differentiable_def)
   3.820 +  using no_isolated_singularity [where s = "interior s"] 
   3.821 +  apply (metis k contf fcd holomorphic_on_open complex_differentiable_def continuous_on_subset 
   3.822 +               has_field_derivative_at_within holomorphic_on_def interior_subset open_interior)
   3.823 +  using assms
   3.824 +  apply auto
   3.825 +  done
   3.826 +
   3.827 +
   3.828 +text\<open> Formula for higher derivatives.\<close>
   3.829 +
   3.830 +proposition Cauchy_has_contour_integral_higher_derivative_circlepath:
   3.831 +  assumes contf: "continuous_on (cball z r) f"
   3.832 +      and holf: "f holomorphic_on ball z r"
   3.833 +      and w: "w \<in> ball z r"
   3.834 +    shows "((\<lambda>u. f u / (u - w) ^ (Suc k))
   3.835 +             has_contour_integral ((2 * pi * ii) / of_real(fact k) * (deriv ^^ k) f w))
   3.836 +           (circlepath z r)"
   3.837 +using w
   3.838 +proof (induction k arbitrary: w)
   3.839 +  case 0 then show ?case
   3.840 +    using assms by (auto simp: Cauchy_integral_circlepath dist_commute dist_norm)
   3.841 +next
   3.842 +  case (Suc k)
   3.843 +  have [simp]: "r > 0" using w
   3.844 +    using ball_eq_empty by fastforce
   3.845 +  have f: "continuous_on (path_image (circlepath z r)) f"
   3.846 +    by (rule continuous_on_subset [OF contf]) (force simp add: cball_def sphere_def less_imp_le)
   3.847 +  obtain X where X: "((\<lambda>u. f u / (u - w) ^ Suc (Suc k)) has_contour_integral X) (circlepath z r)"
   3.848 +    using Cauchy_next_derivative_circlepath(1) [OF f Suc.IH _ Suc.prems]
   3.849 +    by (auto simp: contour_integrable_on_def)
   3.850 +  then have con: "contour_integral (circlepath z r) ((\<lambda>u. f u / (u - w) ^ Suc (Suc k))) = X"
   3.851 +    by (rule contour_integral_unique)
   3.852 +  have "\<And>n. ((deriv ^^ n) f has_field_derivative deriv ((deriv ^^ n) f) w) (at w)"
   3.853 +    using Suc.prems assms has_field_derivative_higher_deriv by auto
   3.854 +  then have dnf_diff: "\<And>n. (deriv ^^ n) f complex_differentiable (at w)"
   3.855 +    by (force simp add: complex_differentiable_def)
   3.856 +  have "deriv (\<lambda>w. complex_of_real (2 * pi) * \<i> / complex_of_real (fact k) * (deriv ^^ k) f w) w =
   3.857 +          of_nat (Suc k) * contour_integral (circlepath z r) (\<lambda>u. f u / (u - w) ^ Suc (Suc k))"
   3.858 +    apply (rule DERIV_imp_deriv)
   3.859 +    apply (rule Cauchy_next_derivative_circlepath [OF f Suc.IH _ Suc.prems])
   3.860 +    apply auto
   3.861 +    done
   3.862 +  also have "... = of_nat (Suc k) * X"
   3.863 +    by (simp only: con)
   3.864 +  finally have "deriv (\<lambda>w. ((2 * pi) * \<i> / of_real (fact k)) * (deriv ^^ k) f w) w = of_nat (Suc k) * X" .
   3.865 +  then have "((2 * pi) * \<i> / of_real (fact k)) * deriv (\<lambda>w. (deriv ^^ k) f w) w = of_nat (Suc k) * X"
   3.866 +    by (metis complex_derivative_cmult dnf_diff)
   3.867 +  then have "deriv (\<lambda>w. (deriv ^^ k) f w) w = of_nat (Suc k) * X / ((2 * pi) * \<i> / of_real (fact k))"
   3.868 +    by (simp add: field_simps)
   3.869 +  then show ?case
   3.870 +  using of_nat_eq_0_iff X by fastforce
   3.871 +qed
   3.872 +
   3.873 +proposition Cauchy_higher_derivative_integral_circlepath:
   3.874 +  assumes contf: "continuous_on (cball z r) f"
   3.875 +      and holf: "f holomorphic_on ball z r"
   3.876 +      and w: "w \<in> ball z r"
   3.877 +    shows "(\<lambda>u. f u / (u - w)^(Suc k)) contour_integrable_on (circlepath z r)"
   3.878 +           (is "?thes1")
   3.879 +      and "(deriv ^^ k) f w =
   3.880 +             of_real(fact k) / (2 * pi * ii) * contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k))"
   3.881 +           (is "?thes2")
   3.882 +proof -
   3.883 +  have *: "((\<lambda>u. f u / (u - w) ^ Suc k) has_contour_integral (2 * pi) * \<i> / (fact k) * (deriv ^^ k) f w)
   3.884 +           (circlepath z r)"
   3.885 +    using Cauchy_has_contour_integral_higher_derivative_circlepath [OF assms]
   3.886 +    by simp
   3.887 +  show ?thes1 using *
   3.888 +    using contour_integrable_on_def by blast
   3.889 +  show ?thes2 
   3.890 +    unfolding contour_integral_unique [OF *] by (simp add: divide_simps)
   3.891 +qed
   3.892 +
   3.893  end
     4.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Dec 14 14:05:31 2015 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue Dec 15 14:40:36 2015 +0000
     4.3 @@ -261,6 +261,7 @@
     4.4  
     4.5  subsection\<open>Holomorphic functions\<close>
     4.6  
     4.7 +text{*Could be generalized to real normed fields, but in practice that would only include the reals*}
     4.8  definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
     4.9             (infixr "(complex'_differentiable)" 50)
    4.10    where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
    4.11 @@ -481,13 +482,13 @@
    4.12      \<Longrightarrow> deriv (g o f) x = deriv g (f x) * deriv f x"
    4.13    by (metis DERIV_deriv_iff_complex_differentiable DERIV_chain DERIV_imp_deriv)
    4.14  
    4.15 -lemma complex_derivative_linear: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
    4.16 +lemma deriv_linear: "deriv (\<lambda>w. c * w) = (\<lambda>z. c)"
    4.17    by (metis DERIV_imp_deriv DERIV_cmult_Id)
    4.18  
    4.19 -lemma complex_derivative_ident: "deriv (\<lambda>w. w) = (\<lambda>z. 1)"
    4.20 +lemma deriv_ident: "deriv (\<lambda>w. w) = (\<lambda>z. 1)"
    4.21    by (metis DERIV_imp_deriv DERIV_ident)
    4.22  
    4.23 -lemma complex_derivative_const: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
    4.24 +lemma deriv_const: "deriv (\<lambda>w. c) = (\<lambda>z. 0)"
    4.25    by (metis DERIV_imp_deriv DERIV_const)
    4.26  
    4.27  lemma complex_derivative_add:
    4.28 @@ -797,11 +798,11 @@
    4.29  
    4.30  lemma complex_derivative_cmult_at:
    4.31    "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. c * f w) z = c * deriv f z"
    4.32 -by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const)
    4.33 +by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
    4.34  
    4.35  lemma complex_derivative_cmult_right_at:
    4.36    "f analytic_on {z} \<Longrightarrow>  deriv (\<lambda>w. f w * c) z = deriv f z * c"
    4.37 -by (auto simp: complex_derivative_mult_at complex_derivative_const analytic_on_const)
    4.38 +by (auto simp: complex_derivative_mult_at deriv_const analytic_on_const)
    4.39  
    4.40  subsection\<open>Complex differentiation of sequences and series\<close>
    4.41  
     5.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 14 14:05:31 2015 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Dec 15 14:40:36 2015 +0000
     5.3 @@ -6359,6 +6359,9 @@
     5.4    "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"
     5.5    unfolding convex_alt closed_segment_def by auto
     5.6  
     5.7 +lemma closed_segment_subset: "\<lbrakk>x \<in> s; y \<in> s; convex s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> s"
     5.8 +  by (simp add: convex_contains_segment)
     5.9 +
    5.10  lemma closed_segment_subset_convex_hull:
    5.11      "\<lbrakk>x \<in> convex hull s; y \<in> convex hull s\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull s"
    5.12    using convex_contains_segment by blast
     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 14 14:05:31 2015 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 15 14:40:36 2015 +0000
     6.3 @@ -826,6 +826,9 @@
     6.4  lemma mem_cball [simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e"
     6.5    by (simp add: cball_def)
     6.6  
     6.7 +lemma mem_sphere [simp]: "y \<in> sphere x e \<longleftrightarrow> dist x y = e"
     6.8 +  by (simp add: sphere_def)
     6.9 +
    6.10  lemma ball_trivial [simp]: "ball x 0 = {}"
    6.11    by (simp add: ball_def)
    6.12