Liouville theorem, Fundamental Theorem of Algebra, etc.
authorpaulson <lp15@cam.ac.uk>
Tue Dec 22 14:33:34 2015 +0000 (2015-12-22)
changeset 61907f0c894ab18c9
parent 61897 bc0fc5499085
child 61908 a759f69db1f6
Liouville theorem, Fundamental Theorem of Algebra, etc.
NEWS
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/NEWS	Mon Dec 21 19:08:26 2015 +0100
     1.2 +++ b/NEWS	Tue Dec 22 14:33:34 2015 +0000
     1.3 @@ -596,7 +596,8 @@
     1.4  orders.
     1.5  
     1.6  * Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (= complex path integrals),
     1.7 -Cauchy's integral theorem, winding numbers and Cauchy's integral formula, ported from HOL Light
     1.8 +Cauchy's integral theorem, winding numbers and Cauchy's integral formula, Liouville theorem,
     1.9 +Fundamental Theorem of Algebra. Ported from HOL Light
    1.10  
    1.11  * Multivariate_Analysis: Added topological concepts such as connected components,
    1.12  homotopic paths and the inside or outside of a set.
     2.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Dec 21 19:08:26 2015 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Dec 22 14:33:34 2015 +0000
     2.3 @@ -6025,4 +6025,354 @@
     2.4      unfolding contour_integral_unique [OF *] by (simp add: divide_simps)
     2.5  qed
     2.6  
     2.7 +corollary Cauchy_contour_integral_circlepath:
     2.8 +  assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \<in> ball z r"
     2.9 +    shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k)) = (2 * pi * ii) * (deriv ^^ k) f w / of_real(fact k)"
    2.10 +by (simp add: Cauchy_higher_derivative_integral_circlepath [OF assms])
    2.11 +
    2.12 +corollary Cauchy_contour_integral_circlepath_2:
    2.13 +  assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \<in> ball z r"
    2.14 +    shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^2) = (2 * pi * ii) * deriv f w"
    2.15 +  using Cauchy_contour_integral_circlepath [OF assms, of 1]
    2.16 +  by (simp add: power2_eq_square)
    2.17 +
    2.18 +
    2.19 +subsection\<open>A holomorphic function is analytic, i.e. has local power series.\<close>
    2.20 +
    2.21 +theorem holomorphic_power_series:
    2.22 +  assumes holf: "f holomorphic_on ball z r"
    2.23 +      and w: "w \<in> ball z r"
    2.24 +    shows "((\<lambda>n. (deriv ^^ n) f z / of_real(fact n) * (w - z)^n) sums f w)"
    2.25 +proof -
    2.26 +  have fh': "f holomorphic_on cball z ((r + dist w z) / 2)"
    2.27 +     apply (rule holomorphic_on_subset [OF holf])
    2.28 +     apply (clarsimp simp del: divide_const_simps)
    2.29 +     apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w)
    2.30 +     done
    2.31 +  --\<open>Replacing @{term r} and the original (weak) premises\<close>
    2.32 +  obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
    2.33 +    apply (rule that [of "(r + dist w z) / 2"])
    2.34 +      apply (simp_all add: fh')
    2.35 +     apply (metis add_0_iff ball_eq_empty dist_nz dist_self empty_iff not_less pos_add_strict w)
    2.36 +    apply (metis add_less_cancel_right dist_commute mem_ball mult_2_right w)
    2.37 +    done
    2.38 +  then have holf: "f holomorphic_on ball z r" and contf: "continuous_on (cball z r) f"
    2.39 +    using ball_subset_cball holomorphic_on_subset apply blast
    2.40 +    by (simp add: holfc holomorphic_on_imp_continuous_on)
    2.41 +  have cint: "\<And>k. (\<lambda>u. f u / (u - z) ^ Suc k) contour_integrable_on circlepath z r"
    2.42 +    apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf])
    2.43 +    apply (simp add: \<open>0 < r\<close>)
    2.44 +    done
    2.45 +  obtain B where "0 < B" and B: "\<And>u. u \<in> cball z r \<Longrightarrow> norm(f u) \<le> B"
    2.46 +    by (metis (no_types) bounded_pos compact_cball compact_continuous_image compact_imp_bounded contf image_eqI)
    2.47 +  obtain k where k: "0 < k" "k \<le> r" and wz_eq: "norm(w - z) = r - k" 
    2.48 +             and kle: "\<And>u. norm(u - z) = r \<Longrightarrow> k \<le> norm(u - w)"
    2.49 +    apply (rule_tac k = "r - dist z w" in that)
    2.50 +    using w
    2.51 +    apply (auto simp: dist_norm norm_minus_commute)
    2.52 +    by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
    2.53 +  have *: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>path_image (circlepath z r). 
    2.54 +                norm ((\<Sum>k<n. (w - z) ^ k * (f x / (x - z) ^ Suc k)) - f x / (x - w)) < e"
    2.55 +          if "0 < e" for e
    2.56 +  proof -
    2.57 +    have rr: "0 \<le> (r - k) / r" "(r - k) / r < 1" using  k by auto
    2.58 +    obtain n where n: "((r - k) / r) ^ n < e / B * k"
    2.59 +      using real_arch_pow_inv [of "e/B*k" "(r - k)/r"] \<open>0 < e\<close> \<open>0 < B\<close> k by force
    2.60 +    have "norm ((\<Sum>k<N. (w - z) ^ k * f u / (u - z) ^ Suc k) - f u / (u - w)) < e"
    2.61 +         if "n \<le> N" and r: "r = dist z u"  for N u
    2.62 +    proof -
    2.63 +      have N: "((r - k) / r) ^ N < e / B * k"
    2.64 +        apply (rule le_less_trans [OF power_decreasing n])
    2.65 +        using  \<open>n \<le> N\<close> k by auto
    2.66 +      have u [simp]: "(u \<noteq> z) \<and> (u \<noteq> w)"
    2.67 +        using \<open>0 < r\<close> r w by auto
    2.68 +      have wzu_not1: "(w - z) / (u - z) \<noteq> 1"
    2.69 +        by (metis (no_types) dist_norm divide_eq_1_iff less_irrefl mem_ball norm_minus_commute r w)
    2.70 +      have "norm ((\<Sum>k<N. (w - z) ^ k * f u / (u - z) ^ Suc k) * (u - w) - f u)
    2.71 +            = norm ((\<Sum>k<N. (((w - z) / (u - z)) ^ k)) * f u * (u - w) / (u - z) - f u)"
    2.72 +        unfolding setsum_left_distrib setsum_divide_distrib power_divide by (simp add: algebra_simps)
    2.73 +      also have "... = norm ((((w - z) / (u - z)) ^ N - 1) * (u - w) / (((w - z) / (u - z) - 1) * (u - z)) - 1) * norm (f u)"
    2.74 +        using \<open>0 < B\<close>
    2.75 +        apply (auto simp: geometric_sum [OF wzu_not1])
    2.76 +        apply (simp add: field_simps norm_mult [symmetric])
    2.77 +        done
    2.78 +      also have "... = norm ((u - z) ^ N * (w - u) - ((w - z) ^ N - (u - z) ^ N) * (u - w)) / (r ^ N * norm (u - w)) * norm (f u)"
    2.79 +        using \<open>0 < r\<close> r by (simp add: divide_simps norm_mult norm_divide norm_power dist_norm norm_minus_commute)
    2.80 +      also have "... = norm ((w - z) ^ N * (w - u)) / (r ^ N * norm (u - w)) * norm (f u)"
    2.81 +        by (simp add: algebra_simps)
    2.82 +      also have "... = norm (w - z) ^ N * norm (f u) / r ^ N"
    2.83 +        by (simp add: norm_mult norm_power norm_minus_commute)
    2.84 +      also have "... \<le> (((r - k)/r)^N) * B"
    2.85 +        using \<open>0 < r\<close> w k
    2.86 +        apply (simp add: divide_simps)
    2.87 +        apply (rule mult_mono [OF power_mono])
    2.88 +        apply (auto simp: norm_divide wz_eq norm_power dist_norm norm_minus_commute B r)
    2.89 +        done
    2.90 +      also have "... < e * k"
    2.91 +        using \<open>0 < B\<close> N by (simp add: divide_simps)
    2.92 +      also have "... \<le> e * norm (u - w)"
    2.93 +        using r kle \<open>0 < e\<close> by (simp add: dist_commute dist_norm) 
    2.94 +      finally show ?thesis
    2.95 +        by (simp add: divide_simps norm_divide del: power_Suc)
    2.96 +    qed
    2.97 +    with \<open>0 < r\<close> show ?thesis
    2.98 +      by (auto simp: mult_ac less_imp_le eventually_sequentially Ball_def)
    2.99 +  qed
   2.100 +  have eq: "\<forall>\<^sub>F x in sequentially.
   2.101 +             contour_integral (circlepath z r) (\<lambda>u. \<Sum>k<x. (w - z) ^ k * (f u / (u - z) ^ Suc k)) =
   2.102 +             (\<Sum>k<x. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z) ^ k)"
   2.103 +    apply (rule eventuallyI)
   2.104 +    apply (subst contour_integral_setsum, simp)
   2.105 +    using contour_integrable_lmul [OF cint, of "(w - z) ^ a" for a] apply (simp add: field_simps)
   2.106 +    apply (simp only: contour_integral_lmul cint algebra_simps)
   2.107 +    done
   2.108 +  have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
   2.109 +        sums contour_integral (circlepath z r) (\<lambda>u. f u/(u - w))"
   2.110 +    unfolding sums_def
   2.111 +    apply (rule Lim_transform_eventually [OF eq])
   2.112 +    apply (rule contour_integral_uniform_limit_circlepath [OF eventuallyI *])
   2.113 +    apply (rule contour_integrable_setsum, simp)
   2.114 +    apply (rule contour_integrable_lmul)
   2.115 +    apply (rule Cauchy_higher_derivative_integral_circlepath [OF contf holf])
   2.116 +    using \<open>0 < r\<close>
   2.117 +    apply auto
   2.118 +    done
   2.119 +  then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
   2.120 +             sums (2 * of_real pi * ii * f w)"
   2.121 +    using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]])
   2.122 +  then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc k) * (w - z)^k / (\<i> * (of_real pi * 2))) 
   2.123 +            sums ((2 * of_real pi * ii * f w) / (\<i> * (complex_of_real pi * 2)))"
   2.124 +    by (rule Series.sums_divide)
   2.125 +  then have "(\<lambda>n. (w - z) ^ n * contour_integral (circlepath z r) (\<lambda>u. f u / (u - z) ^ Suc n) / (\<i> * (of_real pi * 2))) 
   2.126 +            sums f w"
   2.127 +    by (simp add: field_simps)
   2.128 +  then show ?thesis
   2.129 +    by (simp add: field_simps \<open>0 < r\<close> Cauchy_higher_derivative_integral_circlepath [OF contf holf])
   2.130 +qed
   2.131 +
   2.132 +
   2.133 +subsection\<open>The Liouville theorem and the Fundamental Theorem of Algebra.\<close>
   2.134 +
   2.135 +text\<open> These weak Liouville versions don't even need the derivative formula.\<close>
   2.136 +
   2.137 +lemma Liouville_weak_0: 
   2.138 +  assumes holf: "f holomorphic_on UNIV" and inf: "(f ---> 0) at_infinity"
   2.139 +    shows "f z = 0"
   2.140 +proof (rule ccontr)
   2.141 +  assume fz: "f z \<noteq> 0"
   2.142 +  with inf [unfolded Lim_at_infinity, rule_format, of "norm(f z)/2"]
   2.143 +  obtain B where B: "\<And>x. B \<le> cmod x \<Longrightarrow> norm (f x) * 2 < cmod (f z)"
   2.144 +    by (auto simp: dist_norm)
   2.145 +  def R \<equiv> "1 + abs B + norm z"
   2.146 +  have "R > 0" unfolding R_def by (meson abs_add_one_gt_zero le_less_trans less_add_same_cancel2 norm_ge_zero)
   2.147 +  have *: "((\<lambda>u. f u / (u - z)) has_contour_integral 2 * complex_of_real pi * \<i> * f z) (circlepath z R)"
   2.148 +    apply (rule Cauchy_integral_circlepath)
   2.149 +    using \<open>R > 0\<close> apply (auto intro: holomorphic_on_subset [OF holf] holomorphic_on_imp_continuous_on)+
   2.150 +    done
   2.151 +  have "cmod (x - z) = R \<Longrightarrow> cmod (f x) * 2 \<le> cmod (f z)" for x
   2.152 +    apply (simp add: R_def)
   2.153 +    apply (rule less_imp_le)
   2.154 +    apply (rule B)
   2.155 +    using norm_triangle_ineq4 [of x z]
   2.156 +    apply (auto simp:)
   2.157 +    done
   2.158 +  with  \<open>R > 0\<close> fz show False
   2.159 +    using has_contour_integral_bound_circlepath [OF *, of "norm(f z)/2/R"]
   2.160 +    by (auto simp: norm_mult norm_divide divide_simps)
   2.161 +qed
   2.162 +
   2.163 +proposition Liouville_weak: 
   2.164 +  assumes "f holomorphic_on UNIV" and "(f ---> l) at_infinity"
   2.165 +    shows "f z = l"
   2.166 +  using Liouville_weak_0 [of "\<lambda>z. f z - l"]
   2.167 +  by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero)
   2.168 +
   2.169 +
   2.170 +proposition Liouville_weak_inverse: 
   2.171 +  assumes "f holomorphic_on UNIV" and unbounded: "\<And>B. eventually (\<lambda>x. norm (f x) \<ge> B) at_infinity"
   2.172 +    obtains z where "f z = 0"
   2.173 +proof -
   2.174 +  { assume f: "\<And>z. f z \<noteq> 0"
   2.175 +    have 1: "(\<lambda>x. 1 / f x) holomorphic_on UNIV"
   2.176 +      by (simp add: holomorphic_on_divide holomorphic_on_const assms f)
   2.177 +    have 2: "((\<lambda>x. 1 / f x) ---> 0) at_infinity"
   2.178 +      apply (rule tendstoI [OF eventually_mono])
   2.179 +      apply (rule_tac B="2/e" in unbounded)
   2.180 +      apply (simp add: dist_norm norm_divide divide_simps mult_ac)
   2.181 +      done
   2.182 +    have False
   2.183 +      using Liouville_weak_0 [OF 1 2] f by simp
   2.184 +  }
   2.185 +  then show ?thesis
   2.186 +    using that by blast
   2.187 +qed
   2.188 +
   2.189 +
   2.190 +text\<open> In particular we get the Fundamental Theorem of Algebra.\<close>
   2.191 +
   2.192 +theorem fundamental_theorem_of_algebra: 
   2.193 +    fixes a :: "nat \<Rightarrow> complex"
   2.194 +  assumes "a 0 = 0 \<or> (\<exists>i \<in> {1..n}. a i \<noteq> 0)"
   2.195 +  obtains z where "(\<Sum>i\<le>n. a i * z^i) = 0"
   2.196 +using assms
   2.197 +proof (elim disjE bexE)
   2.198 +  assume "a 0 = 0" then show ?thesis
   2.199 +    by (auto simp: that [of 0])
   2.200 +next
   2.201 +  fix i
   2.202 +  assume i: "i \<in> {1..n}" and nz: "a i \<noteq> 0"
   2.203 +  have 1: "(\<lambda>z. \<Sum>i\<le>n. a i * z^i) holomorphic_on UNIV"
   2.204 +    by (rule holomorphic_intros)+
   2.205 +  show ?thesis
   2.206 +    apply (rule Liouville_weak_inverse [OF 1])
   2.207 +    apply (rule polyfun_extremal)
   2.208 +    apply (rule nz)
   2.209 +    using i that
   2.210 +    apply (auto simp:)
   2.211 +    done
   2.212 +qed
   2.213 +
   2.214 +
   2.215 +subsection\<open> Weierstrass convergence theorem.\<close>
   2.216 +
   2.217 +proposition holomorphic_uniform_limit:
   2.218 +  assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and> (f n) holomorphic_on ball z r) F"
   2.219 +      and lim: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> cball z r. norm(f n x - g x) < e) F"
   2.220 +      and F:  "~ trivial_limit F"
   2.221 +  obtains "continuous_on (cball z r) g" "g holomorphic_on ball z r"
   2.222 +proof (cases r "0::real" rule: linorder_cases)
   2.223 +  case less then show ?thesis by (force simp add: ball_empty less_imp_le continuous_on_def holomorphic_on_def intro: that)
   2.224 +next
   2.225 +  case equal then show ?thesis
   2.226 +    by (force simp add: holomorphic_on_def continuous_on_sing intro: that)
   2.227 +next
   2.228 +  case greater
   2.229 +  have contg: "continuous_on (cball z r) g"
   2.230 +    using cont
   2.231 +    by (fastforce simp: eventually_conj_iff dist_norm intro: eventually_mono [OF lim] continuous_uniform_limit [OF F])
   2.232 +  have 1: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1 / (2 * complex_of_real pi * \<i>) * g x)"
   2.233 +    apply (rule continuous_intros continuous_on_subset [OF contg])+
   2.234 +    using \<open>0 < r\<close> by auto
   2.235 +  have 2: "((\<lambda>u. 1 / (2 * of_real pi * \<i>) * g u / (u - w) ^ 1) has_contour_integral g w) (circlepath z r)"
   2.236 +       if w: "w \<in> ball z r" for w
   2.237 +  proof -
   2.238 +    def d \<equiv> "(r - norm(w - z))"
   2.239 +    have "0 < d"  "d \<le> r" using w by (auto simp: norm_minus_commute d_def dist_norm) 
   2.240 +    have dle: "\<And>u. cmod (z - u) = r \<Longrightarrow> d \<le> cmod (u - w)"
   2.241 +      unfolding d_def by (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
   2.242 +    have ev_int: "\<forall>\<^sub>F n in F. (\<lambda>u. f n u / (u - w)) contour_integrable_on circlepath z r"
   2.243 +      apply (rule eventually_mono [OF cont])
   2.244 +      using w
   2.245 +      apply (auto intro: Cauchy_higher_derivative_integral_circlepath [where k=0, simplified])
   2.246 +      done
   2.247 +    have ev_less: "\<forall>\<^sub>F n in F. \<forall>x\<in>path_image (circlepath z r). cmod (f n x / (x - w) - g x / (x - w)) < e"
   2.248 +         if "e > 0" for e
   2.249 +      using greater \<open>0 < d\<close> \<open>0 < e\<close>
   2.250 +      apply (simp add: norm_divide diff_divide_distrib [symmetric] divide_simps)
   2.251 +      apply (rule_tac e1="e * d" in eventually_mono [OF lim])
   2.252 +      apply (force simp: dist_norm intro: dle mult_left_mono less_le_trans)+
   2.253 +      done
   2.254 +    have g_cint: "(\<lambda>u. g u/(u - w)) contour_integrable_on circlepath z r"
   2.255 +      by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
   2.256 +    have cif_tends_cig: "((\<lambda>n. contour_integral(circlepath z r) (\<lambda>u. f n u / (u - w))) ---> contour_integral(circlepath z r) (\<lambda>u. g u/(u - w))) F"
   2.257 +      by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
   2.258 +    have f_tends_cig: "((\<lambda>n. 2 * of_real pi * ii * f n w) ---> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
   2.259 +      apply (rule Lim_transform_eventually [where f = "\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. f n u/(u - w))"])
   2.260 +      apply (rule eventually_mono [OF cont])
   2.261 +      apply (rule contour_integral_unique [OF Cauchy_integral_circlepath])
   2.262 +      using w
   2.263 +      apply (auto simp: norm_minus_commute dist_norm cif_tends_cig)
   2.264 +      done
   2.265 +    have "((\<lambda>n. 2 * of_real pi * \<i> * f n w) ---> 2 * of_real pi * \<i> * g w) F"
   2.266 +      apply (rule tendsto_mult_left [OF tendstoI])
   2.267 +      apply (rule eventually_mono [OF lim], assumption)
   2.268 +      using w
   2.269 +      apply (force simp add: dist_norm)
   2.270 +      done
   2.271 +    then have "((\<lambda>u. g u / (u - w)) has_contour_integral 2 * of_real pi * \<i> * g w) (circlepath z r)"
   2.272 +      using has_contour_integral_integral [OF g_cint] tendsto_unique [OF F f_tends_cig] w
   2.273 +      by (force simp add: dist_norm)
   2.274 +    then have "((\<lambda>u. g u / (2 * of_real pi * \<i> * (u - w))) has_contour_integral g w) (circlepath z r)"
   2.275 +      using has_contour_integral_div [where c = "2 * of_real pi * \<i>"]
   2.276 +      by (force simp add: field_simps)
   2.277 +    then show ?thesis
   2.278 +      by (simp add: dist_norm)
   2.279 +  qed
   2.280 +  show ?thesis
   2.281 +    using Cauchy_next_derivative_circlepath(2) [OF 1 2, simplified]
   2.282 +    by (fastforce simp add: holomorphic_on_open contg intro: that)
   2.283 +qed
   2.284 +
   2.285 +
   2.286 +text\<open> Version showing that the limit is the limit of the derivatives.\<close>
   2.287 +
   2.288 +proposition has_complex_derivative_uniform_limit:
   2.289 +  fixes z::complex
   2.290 +  assumes cont: "eventually (\<lambda>n. continuous_on (cball z r) (f n) \<and> 
   2.291 +                               (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F"
   2.292 +      and lim: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> cball z r. norm(f n x - g x) < e) F"
   2.293 +      and F:  "~ trivial_limit F" and "0 < r"
   2.294 +  obtains g' where
   2.295 +      "continuous_on (cball z r) g" 
   2.296 +      "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) ---> g' w) F"
   2.297 +proof -
   2.298 +  let ?conint = "contour_integral (circlepath z r)"
   2.299 +  have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r"
   2.300 +    by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F]; 
   2.301 +             auto simp: holomorphic_on_open complex_differentiable_def)+
   2.302 +  then obtain g' where g': "\<And>x. x \<in> ball z r \<Longrightarrow> (g has_field_derivative g' x) (at x)"
   2.303 +    using DERIV_deriv_iff_has_field_derivative
   2.304 +    by (fastforce simp add: holomorphic_on_open)
   2.305 +  then have derg: "\<And>x. x \<in> ball z r \<Longrightarrow> deriv g x = g' x"
   2.306 +    by (simp add: DERIV_imp_deriv)
   2.307 +  have tends_f'n_g': "((\<lambda>n. f' n w) ---> g' w) F" if w: "w \<in> ball z r" for w
   2.308 +  proof -
   2.309 +    have eq_f': "?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \<i>)" 
   2.310 +             if cont_fn: "continuous_on (cball z r) (f n)" 
   2.311 +             and fnd: "\<And>w. w \<in> ball z r \<Longrightarrow> (f n has_field_derivative f' n w) (at w)" for n
   2.312 +    proof -
   2.313 +      have hol_fn: "f n holomorphic_on ball z r"
   2.314 +        using fnd by (force simp add: holomorphic_on_open)
   2.315 +      have "(f n has_field_derivative 1 / (2 * of_real pi * \<i>) * ?conint (\<lambda>u. f n u / (u - w)\<^sup>2)) (at w)"
   2.316 +        by (rule Cauchy_derivative_integral_circlepath [OF cont_fn hol_fn w])
   2.317 +      then have f': "f' n w = 1 / (2 * of_real pi * \<i>) * ?conint (\<lambda>u. f n u / (u - w)\<^sup>2)"
   2.318 +        using DERIV_unique [OF fnd] w by blast 
   2.319 +      show ?thesis
   2.320 +        by (simp add: f' Cauchy_contour_integral_circlepath_2 [OF g w] derg [OF w] divide_simps)
   2.321 +    qed
   2.322 +    def d \<equiv> "(r - norm(w - z))^2"
   2.323 +    have "d > 0"
   2.324 +      using w by (simp add: dist_commute dist_norm d_def)
   2.325 +    have dle: "\<And>y. r = cmod (z - y) \<Longrightarrow> d \<le> cmod ((y - w)\<^sup>2)"
   2.326 +      apply (simp add: d_def norm_power)
   2.327 +      apply (rule power_mono)
   2.328 +      apply (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
   2.329 +      apply (metis diff_ge_0_iff_ge dist_commute dist_norm less_eq_real_def mem_ball w)
   2.330 +      done
   2.331 +    have 1: "\<forall>\<^sub>F n in F. (\<lambda>x. f n x / (x - w)\<^sup>2) contour_integrable_on circlepath z r"
   2.332 +      by (force simp add: holomorphic_on_open intro: w Cauchy_derivative_integral_circlepath eventually_mono [OF cont])
   2.333 +    have 2: "0 < e \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x \<in> path_image (circlepath z r). cmod (f n x / (x - w)\<^sup>2 - g x / (x - w)\<^sup>2) < e" for e
   2.334 +      using \<open>r > 0\<close>
   2.335 +      apply (simp add: diff_divide_distrib [symmetric] norm_divide divide_simps sphere_def)
   2.336 +      apply (rule eventually_mono [OF lim, of "e*d"])
   2.337 +      apply (simp add: \<open>0 < d\<close>)
   2.338 +      apply (force simp add: dist_norm dle intro: less_le_trans)
   2.339 +      done
   2.340 +    have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2)) 
   2.341 +             ---> contour_integral (circlepath z r) ((\<lambda>x. g x / (x - w)\<^sup>2))) F"
   2.342 +      by (rule Cauchy_Integral_Thm.contour_integral_uniform_limit_circlepath [OF 1 2 F \<open>0 < r\<close>])
   2.343 +    then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) ---> 0) F"
   2.344 +      using Lim_null by (force intro!: tendsto_mult_right_zero)
   2.345 +    have "((\<lambda>n. f' n w - g' w) ---> 0) F"
   2.346 +      apply (rule Lim_transform_eventually [OF _ tendsto_0])
   2.347 +      apply (force simp add: divide_simps intro: eq_f' eventually_mono [OF cont])
   2.348 +      done
   2.349 +    then show ?thesis using Lim_null by blast
   2.350 +  qed
   2.351 +  obtain g' where "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) ---> g' w) F"
   2.352 +      by (blast intro: tends_f'n_g' g' )
   2.353 +  then show ?thesis using g
   2.354 +    using that by blast
   2.355 +qed
   2.356 +
   2.357  end
     3.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Dec 21 19:08:26 2015 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 22 14:33:34 2015 +0000
     3.3 @@ -2356,6 +2356,10 @@
     3.4  lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
     3.5    unfolding deriv_def by (metis some_equality DERIV_unique)
     3.6  
     3.7 +lemma DERIV_deriv_iff_has_field_derivative:
     3.8 +  "DERIV f x :> deriv f x \<longleftrightarrow> (\<exists>f'. (f has_field_derivative f') (at x))"
     3.9 +  by (auto simp: has_field_derivative_def DERIV_imp_deriv)
    3.10 +  
    3.11  lemma DERIV_deriv_iff_real_differentiable:
    3.12    fixes x :: real
    3.13    shows "DERIV f x :> deriv f x \<longleftrightarrow> f differentiable at x"
     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 21 19:08:26 2015 +0100
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 22 14:33:34 2015 +0000
     4.3 @@ -855,6 +855,9 @@
     4.4  lemma ball_subset_cball [simp,intro]: "ball x e \<subseteq> cball x e"
     4.5    by (simp add: subset_eq)
     4.6  
     4.7 +lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
     4.8 +  by force
     4.9 +
    4.10  lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
    4.11    by (simp add: subset_eq)
    4.12  
     5.1 --- a/src/HOL/Topological_Spaces.thy	Mon Dec 21 19:08:26 2015 +0100
     5.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Dec 22 14:33:34 2015 +0000
     5.3 @@ -1449,6 +1449,12 @@
     5.4    shows "closed (f -` s)"
     5.5    using closed_vimage_Int [OF assms] by simp
     5.6  
     5.7 +lemma continuous_on_empty: "continuous_on {} f"
     5.8 +  by (simp add: continuous_on_def)
     5.9 +
    5.10 +lemma continuous_on_sing: "continuous_on {x} f"
    5.11 +  by (simp add: continuous_on_def at_within_def)
    5.12 +
    5.13  lemma continuous_on_open_Union:
    5.14    "(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"
    5.15    unfolding continuous_on_def by safe (metis open_Union at_within_open UnionI)