merged

--- a/src/HOL/Library/Nonpos_Ints.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Library/Nonpos_Ints.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -2,12 +2,13 @@
     Author:   Manuel Eberl, TU München
 *)
 
-section \<open>Non-positive integers\<close>
+section \<open>Non-negative, non-positive integers and reals\<close>
 
 theory Nonpos_Ints
 imports Complex_Main
 begin
 
+subsection\<open>Non-positive integers\<close>
 text \<open>
   The set of non-positive integers on a ring. (in analogy to the set of non-negative
   integers @{term "\<nat>"}) This is useful e.g. for the Gamma function.
@@ -30,7 +31,6 @@
 lemma numeral_notin_nonpos_Ints [simp]: "(numeral n :: 'a :: ring_char_0) \<notin> \<int>\<^sub>\<le>\<^sub>0"
   by (auto simp: nonpos_Ints_def)
 
-
 lemma minus_of_nat_in_nonpos_Ints [simp, intro]: "- of_nat n \<in> \<int>\<^sub>\<le>\<^sub>0"
 proof -
   have "- of_nat n = of_int (-int n)" by simp
@@ -140,4 +140,165 @@
   show "z \<in> \<int>\<^sub>\<le>\<^sub>0" by (subst A) simp
 qed
 
+
+subsection\<open>Non-negative reals\<close>
+
+definition nonneg_Reals :: "'a::real_algebra_1 set"  ("\<real>\<^sub>\<ge>\<^sub>0")
+  where "\<real>\<^sub>\<ge>\<^sub>0 = {of_real r | r. r \<ge> 0}"
+
+lemma nonneg_Reals_of_real_iff [simp]: "of_real r \<in> \<real>\<^sub>\<ge>\<^sub>0 \<longleftrightarrow> r \<ge> 0"
+  by (force simp add: nonneg_Reals_def)
+
+lemma nonneg_Reals_subset_Reals: "\<real>\<^sub>\<ge>\<^sub>0 \<subseteq> \<real>"
+  unfolding nonneg_Reals_def Reals_def by blast
+
+lemma nonneg_Reals_Real [dest]: "x \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> x \<in> \<real>"
+  unfolding nonneg_Reals_def Reals_def by blast
+
+lemma nonneg_Reals_of_nat_I [simp]: "of_nat n \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  by (metis nonneg_Reals_of_real_iff of_nat_0_le_iff of_real_of_nat_eq)
+
+lemma nonneg_Reals_cases:
+  assumes "x \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  obtains r where "x = of_real r" "r \<ge> 0"
+  using assms unfolding nonneg_Reals_def by (auto elim!: Reals_cases)
+
+lemma nonneg_Reals_zero_I [simp]: "0 \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  unfolding nonneg_Reals_def by auto
+
+lemma nonneg_Reals_one_I [simp]: "1 \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  by (metis (mono_tags, lifting) nonneg_Reals_of_nat_I of_nat_1)
+
+lemma nonneg_Reals_minus_one_I [simp]: "-1 \<notin> \<real>\<^sub>\<ge>\<^sub>0"
+  by (metis nonneg_Reals_of_real_iff le_minus_one_simps(3) of_real_1 of_real_def real_vector.scale_minus_left)
+
+lemma nonneg_Reals_numeral_I [simp]: "numeral w \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  by (metis (no_types) nonneg_Reals_of_nat_I of_nat_numeral)
+
+lemma nonneg_Reals_minus_numeral_I [simp]: "- numeral w \<notin> \<real>\<^sub>\<ge>\<^sub>0"
+  using nonneg_Reals_of_real_iff not_zero_le_neg_numeral by fastforce
+
+lemma nonneg_Reals_add_I [simp]: "\<lbrakk>a \<in> \<real>\<^sub>\<ge>\<^sub>0; b \<in> \<real>\<^sub>\<ge>\<^sub>0\<rbrakk> \<Longrightarrow> a + b \<in> \<real>\<^sub>\<ge>\<^sub>0"
+apply (simp add: nonneg_Reals_def)
+apply clarify
+apply (rename_tac r s)
+apply (rule_tac x="r+s" in exI, auto)
+done
+
+lemma nonneg_Reals_mult_I [simp]: "\<lbrakk>a \<in> \<real>\<^sub>\<ge>\<^sub>0; b \<in> \<real>\<^sub>\<ge>\<^sub>0\<rbrakk> \<Longrightarrow> a * b \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  unfolding nonneg_Reals_def  by (auto simp: of_real_def)
+
+lemma nonneg_Reals_inverse_I [simp]:
+  fixes a :: "'a::real_div_algebra"
+  shows "a \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> inverse a \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  by (simp add: nonneg_Reals_def image_iff) (metis inverse_nonnegative_iff_nonnegative of_real_inverse)
+
+lemma nonneg_Reals_divide_I [simp]:
+  fixes a :: "'a::real_div_algebra"
+  shows "\<lbrakk>a \<in> \<real>\<^sub>\<ge>\<^sub>0; b \<in> \<real>\<^sub>\<ge>\<^sub>0\<rbrakk> \<Longrightarrow> a / b \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  by (simp add: divide_inverse)
+
+lemma nonneg_Reals_pow_I [simp]: "a \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> a^n \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  by (induction n) auto
+
+lemma complex_nonneg_Reals_iff: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<longleftrightarrow> Re z \<ge> 0 \<and> Im z = 0"
+  by (auto simp: nonneg_Reals_def) (metis complex_of_real_def complex_surj)
+
+lemma ii_not_nonneg_Reals [iff]: "\<i> \<notin> \<real>\<^sub>\<ge>\<^sub>0"
+  by (simp add: complex_nonneg_Reals_iff)
+
+
+subsection\<open>Non-positive reals\<close>
+
+definition nonpos_Reals :: "'a::real_algebra_1 set"  ("\<real>\<^sub>\<le>\<^sub>0")
+  where "\<real>\<^sub>\<le>\<^sub>0 = {of_real r | r. r \<le> 0}"
+
+lemma nonpos_Reals_of_real_iff [simp]: "of_real r \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> r \<le> 0"
+  by (force simp add: nonpos_Reals_def)
+
+lemma nonpos_Reals_subset_Reals: "\<real>\<^sub>\<le>\<^sub>0 \<subseteq> \<real>"
+  unfolding nonpos_Reals_def Reals_def by blast
+
+lemma nonpos_Ints_subset_nonpos_Reals: "\<int>\<^sub>\<le>\<^sub>0 \<subseteq> \<real>\<^sub>\<le>\<^sub>0"
+  by (metis nonpos_Ints_cases nonpos_Ints_nonpos nonpos_Ints_of_int 
+    nonpos_Reals_of_real_iff of_real_of_int_eq subsetI)
+
+lemma nonpos_Reals_of_nat_iff [simp]: "of_nat n \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n=0"
+  by (metis nonpos_Reals_of_real_iff of_nat_le_0_iff of_real_of_nat_eq)
+
+lemma nonpos_Reals_Real [dest]: "x \<in> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> x \<in> \<real>"
+  unfolding nonpos_Reals_def Reals_def by blast
+
+lemma nonpos_Reals_cases:
+  assumes "x \<in> \<real>\<^sub>\<le>\<^sub>0"
+  obtains r where "x = of_real r" "r \<le> 0"
+  using assms unfolding nonpos_Reals_def by (auto elim!: Reals_cases)
+
+lemma uminus_nonneg_Reals_iff [simp]: "-x \<in> \<real>\<^sub>\<ge>\<^sub>0 \<longleftrightarrow> x \<in> \<real>\<^sub>\<le>\<^sub>0"
+  apply (auto simp: nonpos_Reals_def nonneg_Reals_def)
+  apply (metis nonpos_Reals_of_real_iff minus_minus neg_le_0_iff_le of_real_minus)
+  apply (metis neg_0_le_iff_le of_real_minus)
+  done
+
+lemma uminus_nonpos_Reals_iff [simp]: "-x \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> x \<in> \<real>\<^sub>\<ge>\<^sub>0"
+  by (metis (no_types) minus_minus uminus_nonneg_Reals_iff)
+
+lemma nonpos_Reals_zero_I [simp]: "0 \<in> \<real>\<^sub>\<le>\<^sub>0"
+  unfolding nonpos_Reals_def by force
+
+lemma nonpos_Reals_one_I [simp]: "1 \<notin> \<real>\<^sub>\<le>\<^sub>0"
+  using nonneg_Reals_minus_one_I uminus_nonneg_Reals_iff by blast
+
+lemma nonpos_Reals_numeral_I [simp]: "numeral w \<notin> \<real>\<^sub>\<le>\<^sub>0"
+  using nonneg_Reals_minus_numeral_I uminus_nonneg_Reals_iff by blast
+
+lemma nonpos_Reals_add_I [simp]: "\<lbrakk>a \<in> \<real>\<^sub>\<le>\<^sub>0; b \<in> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> a + b \<in> \<real>\<^sub>\<le>\<^sub>0"
+  by (metis nonneg_Reals_add_I add_uminus_conv_diff minus_diff_eq minus_minus uminus_nonpos_Reals_iff)
+
+lemma nonpos_Reals_mult_I1: "\<lbrakk>a \<in> \<real>\<^sub>\<ge>\<^sub>0; b \<in> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> a * b \<in> \<real>\<^sub>\<le>\<^sub>0"
+  by (metis nonneg_Reals_mult_I mult_minus_right uminus_nonneg_Reals_iff)
+
+lemma nonpos_Reals_mult_I2: "\<lbrakk>a \<in> \<real>\<^sub>\<le>\<^sub>0; b \<in> \<real>\<^sub>\<ge>\<^sub>0\<rbrakk> \<Longrightarrow> a * b \<in> \<real>\<^sub>\<le>\<^sub>0"
+  by (metis nonneg_Reals_mult_I mult_minus_left uminus_nonneg_Reals_iff)
+
+lemma nonpos_Reals_mult_of_nat_iff:
+  fixes a:: "'a :: real_div_algebra" shows "a * of_nat n \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> a \<in> \<real>\<^sub>\<le>\<^sub>0 \<or> n=0"
+  apply (auto intro: nonpos_Reals_mult_I2)
+  apply (auto simp: nonpos_Reals_def)
+  apply (rule_tac x="r/n" in exI)
+  apply (auto simp: divide_simps)
+  done
+
+lemma nonpos_Reals_inverse_I:
+    fixes a :: "'a::real_div_algebra"
+    shows "a \<in> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> inverse a \<in> \<real>\<^sub>\<le>\<^sub>0"
+  using nonneg_Reals_inverse_I uminus_nonneg_Reals_iff by fastforce
+
+lemma nonpos_Reals_divide_I1:
+    fixes a :: "'a::real_div_algebra"
+    shows "\<lbrakk>a \<in> \<real>\<^sub>\<ge>\<^sub>0; b \<in> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> a / b \<in> \<real>\<^sub>\<le>\<^sub>0"
+  by (simp add: nonpos_Reals_inverse_I nonpos_Reals_mult_I1 divide_inverse)
+
+lemma nonpos_Reals_divide_I2:
+    fixes a :: "'a::real_div_algebra"
+    shows "\<lbrakk>a \<in> \<real>\<^sub>\<le>\<^sub>0; b \<in> \<real>\<^sub>\<ge>\<^sub>0\<rbrakk> \<Longrightarrow> a / b \<in> \<real>\<^sub>\<le>\<^sub>0"
+  by (metis nonneg_Reals_divide_I minus_divide_left uminus_nonneg_Reals_iff)
+
+lemma nonpos_Reals_divide_of_nat_iff:
+  fixes a:: "'a :: real_div_algebra" shows "a / of_nat n \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> a \<in> \<real>\<^sub>\<le>\<^sub>0 \<or> n=0"
+  apply (auto intro: nonpos_Reals_divide_I2)
+  apply (auto simp: nonpos_Reals_def)
+  apply (rule_tac x="r*n" in exI)
+  apply (auto simp: divide_simps mult_le_0_iff)
+  done
+
+lemma nonpos_Reals_pow_I: "\<lbrakk>a \<in> \<real>\<^sub>\<le>\<^sub>0; odd n\<rbrakk> \<Longrightarrow> a^n \<in> \<real>\<^sub>\<le>\<^sub>0"
+  by (metis nonneg_Reals_pow_I power_minus_odd uminus_nonneg_Reals_iff)
+
+lemma complex_nonpos_Reals_iff: "z \<in> \<real>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> Re z \<le> 0 \<and> Im z = 0"
+   using complex_is_Real_iff by (force simp add: nonpos_Reals_def)
+
+lemma ii_not_nonpos_Reals [iff]: "\<i> \<notin> \<real>\<^sub>\<le>\<^sub>0"
+  by (simp add: complex_nonpos_Reals_iff)
+
 end
\ No newline at end of file

--- a/src/HOL/Library/Product_Vector.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -574,5 +574,13 @@
     and norm_Pair2 [simp]: "norm (x,0) = norm x"
 by (auto simp: norm_Pair)
 
+lemma norm_commute: "norm (x,y) = norm (y,x)"
+  by (simp add: norm_Pair)
+
+lemma norm_fst_le: "norm x \<le> norm (x,y)"
+  by (metis dist_fst_le fst_conv fst_zero norm_conv_dist)
+
+lemma norm_snd_le: "norm y \<le> norm (x,y)"
+  by (metis dist_snd_le snd_conv snd_zero norm_conv_dist)
 
 end

--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -572,6 +572,12 @@
 lemma contour_integral_unique: "(f has_contour_integral i)  g \<Longrightarrow> contour_integral g f = i"
   by (auto simp: contour_integral_def has_contour_integral_def integral_def [symmetric])
 
+corollary has_contour_integral_eqpath:
+     "\<lbrakk>(f has_contour_integral y) p; f contour_integrable_on \<gamma>; 
+       contour_integral p f = contour_integral \<gamma> f\<rbrakk>
+      \<Longrightarrow> (f has_contour_integral y) \<gamma>"
+using contour_integrable_on_def contour_integral_unique by auto
+
 lemma has_contour_integral_integral:
     "f contour_integrable_on i \<Longrightarrow> (f has_contour_integral (contour_integral i f)) i"
   by (metis contour_integral_unique contour_integrable_on_def)
@@ -2826,12 +2832,12 @@
 qed
 
 lemma contour_integrable_holomorphic_simple:
-  assumes contf: "continuous_on s f"
+  assumes fh: "f holomorphic_on s"
       and os: "open s"
       and g: "valid_path g" "path_image g \<subseteq> s"
-      and fh: "f holomorphic_on s"
     shows "f contour_integrable_on g"
-  apply (rule contour_integrable_holomorphic [OF contf os Finite_Set.finite.emptyI g])
+  apply (rule contour_integrable_holomorphic [OF _ os Finite_Set.finite.emptyI g])
+  apply (simp add: fh holomorphic_on_imp_continuous_on)
   using fh  by (simp add: complex_differentiable_def holomorphic_on_open os)
 
 lemma continuous_on_inversediff:
@@ -2840,7 +2846,7 @@
 
 corollary contour_integrable_inversediff:
     "\<lbrakk>valid_path g; z \<notin> path_image g\<rbrakk> \<Longrightarrow> (\<lambda>w. 1 / (w-z)) contour_integrable_on g"
-apply (rule contour_integrable_holomorphic_simple [of "UNIV-{z}", OF continuous_on_inversediff])
+apply (rule contour_integrable_holomorphic_simple [of _ "UNIV-{z}"])
 apply (auto simp: holomorphic_on_open open_delete intro!: derivative_eq_intros)
 done
 
@@ -5972,8 +5978,7 @@
   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))
+    shows "((\<lambda>u. f u / (u - w) ^ (Suc k)) has_contour_integral ((2 * pi * ii) / (fact k) * (deriv ^^ k) f w))
            (circlepath z r)"
 using w
 proof (induction k arbitrary: w)
@@ -5994,18 +5999,15 @@
     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 =
+  have "deriv (\<lambda>w. complex_of_real (2 * pi) * \<i> / (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
+    by (force intro!: DERIV_imp_deriv Cauchy_next_derivative_circlepath [OF f Suc.IH _ Suc.prems])
   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"
+  finally have "deriv (\<lambda>w. ((2 * pi) * \<i> / (fact k)) * (deriv ^^ k) f w) w = of_nat (Suc k) * X" .
+  then have "((2 * pi) * \<i> / (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))"
+  then have "deriv (\<lambda>w. (deriv ^^ k) f w) w = of_nat (Suc k) * X / ((2 * pi) * \<i> / (fact k))"
     by (simp add: field_simps)
   then show ?case
   using of_nat_eq_0_iff X by fastforce
@@ -6017,8 +6019,7 @@
       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))"
+      and "(deriv ^^ k) f w = (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)
@@ -6033,7 +6034,7 @@
 
 corollary Cauchy_contour_integral_circlepath:
   assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \<in> ball z r"
-    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)"
+    shows "contour_integral(circlepath z r) (\<lambda>u. f u/(u - w)^(Suc k)) = (2 * pi * ii) * (deriv ^^ k) f w / (fact k)"
 by (simp add: Cauchy_higher_derivative_integral_circlepath [OF assms])
 
 corollary Cauchy_contour_integral_circlepath_2:
@@ -6048,14 +6049,14 @@
 theorem holomorphic_power_series:
   assumes holf: "f holomorphic_on ball z r"
       and w: "w \<in> ball z r"
-    shows "((\<lambda>n. (deriv ^^ n) f z / of_real(fact n) * (w - z)^n) sums f w)"
+    shows "((\<lambda>n. (deriv ^^ n) f z / (fact n) * (w - z)^n) sums f w)"
 proof -
   have fh': "f holomorphic_on cball z ((r + dist w z) / 2)"
      apply (rule holomorphic_on_subset [OF holf])
      apply (clarsimp simp del: divide_const_simps)
      apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w)
      done
-  \<comment>\<open>Replacing @{term r} and the original (weak) premises\<close>
+  --\<open>Replacing @{term r} and the original (weak) premises\<close>
   obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
     apply (rule that [of "(r + dist w z) / 2"])
       apply (simp_all add: fh')
@@ -6102,7 +6103,7 @@
         apply (auto simp: geometric_sum [OF wzu_not1])
         apply (simp add: field_simps norm_mult [symmetric])
         done
-      also have "... = norm ((u - z) ^ N * (w - u) - ((w - z) ^ N - (u - z) ^ N) * (u - w)) / (r ^ N * norm (u - w)) * norm (f u)"
+      also have "... = norm ((u-z) ^ N * (w - u) - ((w - z) ^ N - (u-z) ^ N) * (u-w)) / (r ^ N * norm (u-w)) * norm (f u)"
         using \<open>0 < r\<close> r by (simp add: divide_simps norm_mult norm_divide norm_power dist_norm norm_minus_commute)
       also have "... = norm ((w - z) ^ N * (w - u)) / (r ^ N * norm (u - w)) * norm (f u)"
         by (simp add: algebra_simps)
@@ -6148,7 +6149,7 @@
     using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]])
   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)))
             sums ((2 * of_real pi * ii * f w) / (\<i> * (complex_of_real pi * 2)))"
-    by (rule Series.sums_divide)
+    by (rule sums_divide)
   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)))
             sums f w"
     by (simp add: field_simps)
@@ -6381,4 +6382,1024 @@
     using that by blast
 qed
 
+
+subsection\<open>Some more simple/convenient versions for applications.\<close>
+
+lemma holomorphic_uniform_sequence:
+  assumes s: "open s"
+      and hol_fn: "\<And>n. (f n) holomorphic_on s"
+      and to_g: "\<And>x. x \<in> s
+                     \<Longrightarrow> \<exists>d. 0 < d \<and> cball x d \<subseteq> s \<and>
+                             (\<forall>e. 0 < e \<longrightarrow> eventually (\<lambda>n. \<forall>y \<in> cball x d. norm(f n y - g y) < e) sequentially)"
+  shows "g holomorphic_on s"
+proof -
+  have "\<exists>f'. (g has_field_derivative f') (at z)" if "z \<in> s" for z
+  proof -
+    obtain r where "0 < r" and r: "cball z r \<subseteq> s"
+               and fg: "\<forall>e. 0 < e \<longrightarrow> eventually (\<lambda>n. \<forall>y \<in> cball z r. norm(f n y - g y) < e) sequentially"
+      using to_g [OF \<open>z \<in> s\<close>] by blast
+    have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and> f n holomorphic_on ball z r"
+      apply (intro eventuallyI conjI)
+      using hol_fn holomorphic_on_imp_continuous_on holomorphic_on_subset r apply blast
+      apply (metis hol_fn holomorphic_on_subset interior_cball interior_subset r)
+      done
+    show ?thesis
+      apply (rule holomorphic_uniform_limit [OF *])
+      using \<open>0 < r\<close> centre_in_ball fg
+      apply (auto simp: holomorphic_on_open)
+      done
+  qed
+  with s show ?thesis
+    by (simp add: holomorphic_on_open)
+qed
+
+lemma has_complex_derivative_uniform_sequence:
+  fixes s :: "complex set"
+  assumes s: "open s"
+      and hfd: "\<And>n x. x \<in> s \<Longrightarrow> ((f n) has_field_derivative f' n x) (at x)"
+      and to_g: "\<And>x. x \<in> s
+             \<Longrightarrow> \<exists>d. 0 < d \<and> cball x d \<subseteq> s \<and>
+                     (\<forall>e. 0 < e \<longrightarrow> eventually (\<lambda>n. \<forall>y \<in> cball x d. norm(f n y - g y) < e) sequentially)"
+  shows "\<exists>g'. \<forall>x \<in> s. (g has_field_derivative g' x) (at x) \<and> ((\<lambda>n. f' n x) \<longlongrightarrow> g' x) sequentially"
+proof -
+  have y: "\<exists>y. (g has_field_derivative y) (at z) \<and> (\<lambda>n. f' n z) \<longlonglongrightarrow> y" if "z \<in> s" for z
+  proof -
+    obtain r where "0 < r" and r: "cball z r \<subseteq> s"
+               and fg: "\<forall>e. 0 < e \<longrightarrow> eventually (\<lambda>n. \<forall>y \<in> cball z r. norm(f n y - g y) < e) sequentially"
+      using to_g [OF \<open>z \<in> s\<close>] by blast
+    have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and>
+                                   (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))"
+      apply (intro eventuallyI conjI)
+      apply (meson hfd holomorphic_on_imp_continuous_on holomorphic_on_open holomorphic_on_subset r s)
+      using ball_subset_cball hfd r apply blast
+      done
+    show ?thesis
+      apply (rule has_complex_derivative_uniform_limit [OF *, of g])
+      using \<open>0 < r\<close> centre_in_ball fg
+      apply force+
+      done
+  qed
+  show ?thesis
+    by (rule bchoice) (blast intro: y)
+qed
+
+
+subsection\<open>On analytic functions defined by a series.\<close>
+
+lemma series_and_derivative_comparison:
+  fixes s :: "complex set"
+  assumes s: "open s"
+      and h: "summable h"
+      and hfd: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+      and to_g: "\<And>n x. \<lbrakk>N \<le> n; x \<in> s\<rbrakk> \<Longrightarrow> norm(f n x) \<le> h n"
+  obtains g g' where "\<forall>x \<in> s. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
+proof -
+  obtain g where g: "\<And>e. e>0 \<Longrightarrow> \<exists>N. \<forall>n x. N \<le> n \<and> x \<in> s \<longrightarrow> dist (\<Sum>n<n. f n x) (g x) < e"
+    using series_comparison_uniform [OF h to_g, of N s] by force
+  have *: "\<exists>d>0. cball x d \<subseteq> s \<and> (\<forall>e>0. \<forall>\<^sub>F n in sequentially. \<forall>y\<in>cball x d. cmod ((\<Sum>a<n. f a y) - g y) < e)"
+         if "x \<in> s" for x
+  proof -
+    obtain d where "d>0" and d: "cball x d \<subseteq> s"
+      using open_contains_cball [of "s"] \<open>x \<in> s\<close> s by blast
+    then show ?thesis
+      apply (rule_tac x=d in exI)
+      apply (auto simp: dist_norm eventually_sequentially)
+      apply (metis g contra_subsetD dist_norm)
+      done
+  qed
+  have "(\<forall>x\<in>s. (\<lambda>n. \<Sum>i<n. f i x) \<longlonglongrightarrow> g x)"
+    using g by (force simp add: lim_sequentially)
+  moreover have "\<exists>g'. \<forall>x\<in>s. (g has_field_derivative g' x) (at x) \<and> (\<lambda>n. \<Sum>i<n. f' i x) \<longlonglongrightarrow> g' x"
+    by (rule has_complex_derivative_uniform_sequence [OF s]) (auto intro: * hfd DERIV_setsum)+
+  ultimately show ?thesis
+    by (force simp add: sums_def  conj_commute intro: that)
+qed
+
+text\<open>A version where we only have local uniform/comparative convergence.\<close>
+
+lemma series_and_derivative_comparison_local:
+  fixes s :: "complex set"
+  assumes s: "open s"
+      and hfd: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+      and to_g: "\<And>x. x \<in> s \<Longrightarrow>
+                      \<exists>d h N. 0 < d \<and> summable h \<and> (\<forall>n y. N \<le> n \<and> y \<in> ball x d \<longrightarrow> norm(f n y) \<le> h n)"
+  shows "\<exists>g g'. \<forall>x \<in> s. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
+proof -
+  have "\<exists>y. (\<lambda>n. f n z) sums (\<Sum>n. f n z) \<and> (\<lambda>n. f' n z) sums y \<and> ((\<lambda>x. \<Sum>n. f n x) has_field_derivative y) (at z)"
+       if "z \<in> s" for z
+  proof -
+    obtain d h N where "0 < d" "summable h" and le_h: "\<And>n y. \<lbrakk>N \<le> n; y \<in> ball z d\<rbrakk> \<Longrightarrow> norm(f n y) \<le> h n"
+      using to_g \<open>z \<in> s\<close> by blast
+    then obtain r where "r>0" and r: "ball z r \<subseteq> ball z d \<inter> s" using \<open>z \<in> s\<close> s
+      by (metis Int_iff open_ball centre_in_ball open_Int open_contains_ball_eq)
+    have 1: "open (ball z d \<inter> s)"
+      by (simp add: open_Int s)
+    have 2: "\<And>n x. x \<in> ball z d \<inter> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+      by (auto simp: hfd)
+    obtain g g' where gg': "\<forall>x \<in> ball z d \<inter> s. ((\<lambda>n. f n x) sums g x) \<and>
+                                    ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
+      by (auto intro: le_h series_and_derivative_comparison [OF 1 \<open>summable h\<close> hfd])
+    then have "(\<lambda>n. f' n z) sums g' z"
+      by (meson \<open>0 < r\<close> centre_in_ball contra_subsetD r)
+    moreover have "(\<lambda>n. f n z) sums (\<Sum>n. f n z)"
+      by (metis summable_comparison_test' summable_sums centre_in_ball \<open>0 < d\<close> \<open>summable h\<close> le_h)
+    moreover have "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' z) (at z)"
+      apply (rule_tac f=g in DERIV_transform_at [OF _ \<open>0 < r\<close>])
+      apply (simp add: gg' \<open>z \<in> s\<close> \<open>0 < d\<close>)
+      apply (metis (full_types) contra_subsetD dist_commute gg' mem_ball r sums_unique)
+      done
+    ultimately show ?thesis by auto
+  qed
+  then show ?thesis
+    by (rule_tac x="\<lambda>x. suminf  (\<lambda>n. f n x)" in exI) meson
+qed
+
+
+text\<open>Sometimes convenient to compare with a complex series of positive reals. (?)\<close>
+
+lemma series_and_derivative_comparison_complex:
+  fixes s :: "complex set"
+  assumes s: "open s"
+      and hfd: "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+      and to_g: "\<And>x. x \<in> s \<Longrightarrow>
+                      \<exists>d h N. 0 < d \<and> summable h \<and> range h \<subseteq> nonneg_Reals \<and> (\<forall>n y. N \<le> n \<and> y \<in> ball x d \<longrightarrow> cmod(f n y) \<le> cmod (h n))"
+  shows "\<exists>g g'. \<forall>x \<in> s. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. f' n x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
+apply (rule series_and_derivative_comparison_local [OF s hfd], assumption)
+apply (frule to_g)
+apply (erule ex_forward)
+apply (erule exE)
+apply (rule_tac x="Re o h" in exI)
+apply (erule ex_forward)
+apply (simp add: summable_Re o_def )
+apply (elim conjE all_forward)
+apply (simp add: nonneg_Reals_cmod_eq_Re image_subset_iff)
+done
+
+
+text\<open>In particular, a power series is analytic inside circle of convergence.\<close>
+
+lemma power_series_and_derivative_0:
+  fixes a :: "nat \<Rightarrow> complex" and r::real
+  assumes "summable (\<lambda>n. a n * r^n)"
+    shows "\<exists>g g'. \<forall>z. cmod z < r \<longrightarrow>
+             ((\<lambda>n. a n * z^n) sums g z) \<and> ((\<lambda>n. of_nat n * a n * z^(n - 1)) sums g' z) \<and> (g has_field_derivative g' z) (at z)"
+proof (cases "0 < r")
+  case True
+    have der: "\<And>n z. ((\<lambda>x. a n * x ^ n) has_field_derivative of_nat n * a n * z ^ (n - 1)) (at z)"
+      by (rule derivative_eq_intros | simp)+
+    have y_le: "\<lbrakk>cmod (z - y) * 2 < r - cmod z\<rbrakk> \<Longrightarrow> cmod y \<le> cmod (of_real r + of_real (cmod z)) / 2" for z y
+      using \<open>r > 0\<close>
+      apply (auto simp: algebra_simps norm_mult norm_divide norm_power of_real_add [symmetric] simp del: of_real_add)
+      using norm_triangle_ineq2 [of y z]
+      apply (simp only: diff_le_eq norm_minus_commute mult_2)
+      done
+    have "summable (\<lambda>n. a n * complex_of_real r ^ n)"
+      using assms \<open>r > 0\<close> by simp
+    moreover have "\<And>z. cmod z < r \<Longrightarrow> cmod ((of_real r + of_real (cmod z)) / 2) < cmod (of_real r)"
+      using \<open>r > 0\<close>
+      by (simp add: of_real_add [symmetric] del: of_real_add)
+    ultimately have sum: "\<And>z. cmod z < r \<Longrightarrow> summable (\<lambda>n. of_real (cmod (a n)) * ((of_real r + complex_of_real (cmod z)) / 2) ^ n)"
+      by (rule power_series_conv_imp_absconv_weak)
+    have "\<exists>g g'. \<forall>z \<in> ball 0 r. (\<lambda>n.  (a n) * z ^ n) sums g z \<and>
+               (\<lambda>n. of_nat n * (a n) * z ^ (n - 1)) sums g' z \<and> (g has_field_derivative g' z) (at z)"
+      apply (rule series_and_derivative_comparison_complex [OF open_ball der])
+      apply (rule_tac x="(r - norm z)/2" in exI)
+      apply (simp add: dist_norm)
+      apply (rule_tac x="\<lambda>n. of_real(norm(a n)*((r + norm z)/2)^n)" in exI)
+      using \<open>r > 0\<close>
+      apply (auto simp: sum nonneg_Reals_divide_I)
+      apply (rule_tac x=0 in exI)
+      apply (force simp: norm_mult norm_divide norm_power intro!: mult_left_mono power_mono y_le)
+      done
+  then show ?thesis
+    by (simp add: dist_0_norm ball_def)
+next
+  case False then show ?thesis
+    apply (simp add: not_less)
+    using less_le_trans norm_not_less_zero by blast
+qed
+
+proposition power_series_and_derivative:
+  fixes a :: "nat \<Rightarrow> complex" and r::real
+  assumes "summable (\<lambda>n. a n * r^n)"
+    obtains g g' where "\<forall>z \<in> ball w r.
+             ((\<lambda>n. a n * (z - w) ^ n) sums g z) \<and> ((\<lambda>n. of_nat n * a n * (z - w) ^ (n - 1)) sums g' z) \<and>
+              (g has_field_derivative g' z) (at z)"
+  using power_series_and_derivative_0 [OF assms]
+  apply clarify
+  apply (rule_tac g="(\<lambda>z. g(z - w))" in that)
+  using DERIV_shift [where z="-w"] 
+  apply (auto simp: norm_minus_commute Ball_def dist_norm)
+  done
+
+proposition power_series_holomorphic:
+  assumes "\<And>w. w \<in> ball z r \<Longrightarrow> ((\<lambda>n. a n*(w - z)^n) sums f w)"
+    shows "f holomorphic_on ball z r"
+proof -
+  have "\<exists>f'. (f has_field_derivative f') (at w)" if w: "dist z w < r" for w
+  proof -
+    have inb: "z + complex_of_real ((dist z w + r) / 2) \<in> ball z r"
+    proof -
+      have wz: "cmod (w - z) < r" using w
+        by (auto simp: divide_simps dist_norm norm_minus_commute)
+      then have "0 \<le> r"
+        by (meson less_eq_real_def norm_ge_zero order_trans)
+      show ?thesis
+        using w by (simp add: dist_norm \<open>0\<le>r\<close> of_real_add [symmetric] del: of_real_add)
+    qed
+    have sum: "summable (\<lambda>n. a n * of_real (((cmod (z - w) + r) / 2) ^ n))"
+      using assms [OF inb] by (force simp add: summable_def dist_norm)
+    obtain g g' where gg': "\<And>u. u \<in> ball z ((cmod (z - w) + r) / 2) \<Longrightarrow>
+                               (\<lambda>n. a n * (u - z) ^ n) sums g u \<and>
+                               (\<lambda>n. of_nat n * a n * (u - z) ^ (n - 1)) sums g' u \<and> (g has_field_derivative g' u) (at u)"
+      by (rule power_series_and_derivative [OF sum, of z]) fastforce
+    have [simp]: "g u = f u" if "cmod (u - w) < (r - cmod (z - w)) / 2" for u
+    proof -
+      have less: "cmod (z - u) * 2 < cmod (z - w) + r"
+        using that dist_triangle2 [of z u w]
+        by (simp add: dist_norm [symmetric] algebra_simps)
+      show ?thesis
+        apply (rule sums_unique2 [of "\<lambda>n. a n*(u - z)^n"])
+        using gg' [of u] less w
+        apply (auto simp: assms dist_norm)
+        done
+    qed
+    show ?thesis
+      apply (rule_tac x="g' w" in exI)
+      apply (rule DERIV_transform_at [where f=g and d="(r - norm(z - w))/2"])
+      using w gg' [of w]
+      apply (auto simp: dist_norm)
+      done
+  qed
+  then show ?thesis by (simp add: holomorphic_on_open)
+qed
+
+corollary holomorphic_iff_power_series:
+     "f holomorphic_on ball z r \<longleftrightarrow>
+      (\<forall>w \<in> ball z r. (\<lambda>n. (deriv ^^ n) f z / (fact n) * (w - z)^n) sums f w)"
+  apply (intro iffI ballI)
+   using holomorphic_power_series  apply force
+  apply (rule power_series_holomorphic [where a = "\<lambda>n. (deriv ^^ n) f z / (fact n)"])
+  apply force
+  done
+
+corollary power_series_analytic:
+     "(\<And>w. w \<in> ball z r \<Longrightarrow> (\<lambda>n. a n*(w - z)^n) sums f w) \<Longrightarrow> f analytic_on ball z r"
+  by (force simp add: analytic_on_open intro!: power_series_holomorphic)
+
+corollary analytic_iff_power_series:
+     "f analytic_on ball z r \<longleftrightarrow>
+      (\<forall>w \<in> ball z r. (\<lambda>n. (deriv ^^ n) f z / (fact n) * (w - z)^n) sums f w)"
+  by (simp add: analytic_on_open holomorphic_iff_power_series)
+
+
+subsection\<open>Equality between holomorphic functions, on open ball then connected set.\<close>
+
+lemma holomorphic_fun_eq_on_ball:
+   "\<lbrakk>f holomorphic_on ball z r; g holomorphic_on ball z r;
+     w \<in> ball z r;
+     \<And>n. (deriv ^^ n) f z = (deriv ^^ n) g z\<rbrakk>
+     \<Longrightarrow> f w = g w"
+  apply (rule sums_unique2 [of "\<lambda>n. (deriv ^^ n) f z / (fact n) * (w - z)^n"])
+  apply (auto simp: holomorphic_iff_power_series)
+  done
+
+lemma holomorphic_fun_eq_0_on_ball:
+   "\<lbrakk>f holomorphic_on ball z r;  w \<in> ball z r;
+     \<And>n. (deriv ^^ n) f z = 0\<rbrakk>
+     \<Longrightarrow> f w = 0"
+  apply (rule sums_unique2 [of "\<lambda>n. (deriv ^^ n) f z / (fact n) * (w - z)^n"])
+  apply (auto simp: holomorphic_iff_power_series)
+  done
+
+lemma holomorphic_fun_eq_0_on_connected:
+  assumes holf: "f holomorphic_on s" and "open s"
+      and cons: "connected s"
+      and der: "\<And>n. (deriv ^^ n) f z = 0"
+      and "z \<in> s" "w \<in> s"
+    shows "f w = 0"
+proof -
+  have *: "\<And>x e. \<lbrakk> \<forall>xa. (deriv ^^ xa) f x = 0;  ball x e \<subseteq> s\<rbrakk>
+           \<Longrightarrow> ball x e \<subseteq> (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
+    apply auto
+    apply (rule holomorphic_fun_eq_0_on_ball [OF holomorphic_higher_deriv])
+    apply (rule holomorphic_on_subset [OF holf], simp_all)
+    by (metis funpow_add o_apply)
+  have 1: "openin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
+    apply (rule open_subset, force)
+    using \<open>open s\<close>
+    apply (simp add: open_contains_ball Ball_def)
+    apply (erule all_forward)
+    using "*" by blast
+  have 2: "closedin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
+    using assms
+    by (auto intro: continuous_closed_in_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv)
+  obtain e where "e>0" and e: "ball w e \<subseteq> s" using openE [OF \<open>open s\<close> \<open>w \<in> s\<close>] .
+  then have holfb: "f holomorphic_on ball w e"
+    using holf holomorphic_on_subset by blast
+  have 3: "(\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0}) = s \<Longrightarrow> f w = 0"
+    using \<open>e>0\<close> e by (force intro: holomorphic_fun_eq_0_on_ball [OF holfb])
+  show ?thesis
+    using cons der \<open>z \<in> s\<close>
+    apply (simp add: connected_clopen)
+    apply (drule_tac x="\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0}" in spec)
+    apply (auto simp: 1 2 3)
+    done
+qed
+
+lemma holomorphic_fun_eq_on_connected:
+  assumes "f holomorphic_on s" "g holomorphic_on s" and "open s"  "connected s"
+      and "\<And>n. (deriv ^^ n) f z = (deriv ^^ n) g z"
+      and "z \<in> s" "w \<in> s"
+    shows "f w = g w"
+  apply (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>x. f x - g x" s z, simplified])
+  apply (intro assms holomorphic_intros)
+  using assms apply simp_all
+  apply (subst higher_deriv_diff, auto)
+  done
+
+lemma holomorphic_fun_eq_const_on_connected:
+  assumes holf: "f holomorphic_on s" and "open s"
+      and cons: "connected s"
+      and der: "\<And>n. 0 < n \<Longrightarrow> (deriv ^^ n) f z = 0"
+      and "z \<in> s" "w \<in> s"
+    shows "f w = f z"
+  apply (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>w. f w - f z" s z, simplified])
+  apply (intro assms holomorphic_intros)
+  using assms apply simp_all
+  apply (subst higher_deriv_diff)
+  apply (intro holomorphic_intros | simp)+
+  done
+
+
+subsection\<open>Some basic lemmas about poles/singularities.\<close>
+
+lemma pole_lemma:
+  assumes holf: "f holomorphic_on s" and a: "a \<in> interior s"
+    shows "(\<lambda>z. if z = a then deriv f a
+                 else (f z - f a) / (z - a)) holomorphic_on s" (is "?F holomorphic_on s")
+proof -
+  have F1: "?F complex_differentiable (at u within s)" if "u \<in> s" "u \<noteq> a" for u
+  proof -
+    have fcd: "f complex_differentiable at u within s"
+      using holf holomorphic_on_def by (simp add: \<open>u \<in> s\<close>)
+    have cd: "(\<lambda>z. (f z - f a) / (z - a)) complex_differentiable at u within s"
+      by (rule fcd derivative_intros | simp add: that)+
+    have "0 < dist a u" using that dist_nz by blast
+    then show ?thesis
+      by (rule complex_differentiable_transform_within [OF _ _ _ cd]) (auto simp: \<open>u \<in> s\<close>)
+  qed
+  have F2: "?F complex_differentiable at a" if "0 < e" "ball a e \<subseteq> s" for e
+  proof -
+    have holfb: "f holomorphic_on ball a e"
+      by (rule holomorphic_on_subset [OF holf \<open>ball a e \<subseteq> s\<close>])
+    have 2: "?F holomorphic_on ball a e - {a}"
+      apply (rule holomorphic_on_subset [where s = "s - {a}"])
+      apply (simp add: holomorphic_on_def complex_differentiable_def [symmetric])
+      using mem_ball that
+      apply (auto intro: F1 complex_differentiable_within_subset)
+      done
+    have "isCont (\<lambda>z. if z = a then deriv f a else (f z - f a) / (z - a)) x"
+            if "dist a x < e" for x
+    proof (cases "x=a")
+      case True then show ?thesis
+      using holfb \<open>0 < e\<close>
+      apply (simp add: holomorphic_on_open complex_differentiable_def [symmetric])
+      apply (drule_tac x=a in bspec)
+      apply (auto simp: DERIV_deriv_iff_complex_differentiable [symmetric] continuous_at DERIV_iff2
+                elim: rev_iffD1 [OF _ LIM_equal])
+      done
+    next
+      case False with 2 that show ?thesis
+        by (force simp: holomorphic_on_open open_Diff complex_differentiable_def [symmetric] complex_differentiable_imp_continuous_at)
+    qed
+    then have 1: "continuous_on (ball a e) ?F"
+      by (clarsimp simp:  continuous_on_eq_continuous_at)
+    have "?F holomorphic_on ball a e"
+      by (auto intro: no_isolated_singularity [OF 1 2])
+    with that show ?thesis
+      by (simp add: holomorphic_on_open complex_differentiable_def [symmetric]
+                    complex_differentiable_at_within)
+  qed
+  show ?thesis
+  proof
+    fix x assume "x \<in> s" show "?F complex_differentiable at x within s"
+    proof (cases "x=a")
+      case True then show ?thesis
+      using a by (auto simp: mem_interior intro: complex_differentiable_at_within F2)
+    next
+      case False with F1 \<open>x \<in> s\<close>
+      show ?thesis by blast
+    qed
+  qed
+qed
+
+proposition pole_theorem:
+  assumes holg: "g holomorphic_on s" and a: "a \<in> interior s"
+      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
+    shows "(\<lambda>z. if z = a then deriv g a
+                 else f z - g a/(z - a)) holomorphic_on s"
+  using pole_lemma [OF holg a]
+  by (rule holomorphic_transform) (simp add: eq divide_simps)
+
+lemma pole_lemma_open:
+  assumes "f holomorphic_on s" "open s"
+    shows "(\<lambda>z. if z = a then deriv f a else (f z - f a)/(z - a)) holomorphic_on s"
+proof (cases "a \<in> s")
+  case True with assms interior_eq pole_lemma
+    show ?thesis by fastforce
+next
+  case False with assms show ?thesis
+    apply (simp add: holomorphic_on_def complex_differentiable_def [symmetric], clarify)
+    apply (rule complex_differentiable_transform_within [where f = "\<lambda>z. (f z - f a)/(z - a)" and d = 1])
+    apply (rule derivative_intros | force)+
+    done
+qed
+
+proposition pole_theorem_open:
+  assumes holg: "g holomorphic_on s" and s: "open s"
+      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
+    shows "(\<lambda>z. if z = a then deriv g a
+                 else f z - g a/(z - a)) holomorphic_on s"
+  using pole_lemma_open [OF holg s]
+  by (rule holomorphic_transform) (auto simp: eq divide_simps)
+
+proposition pole_theorem_0:
+  assumes holg: "g holomorphic_on s" and a: "a \<in> interior s"
+      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
+      and [simp]: "f a = deriv g a" "g a = 0"
+    shows "f holomorphic_on s"
+  using pole_theorem [OF holg a eq]
+  by (rule holomorphic_transform) (auto simp: eq divide_simps)
+
+proposition pole_theorem_open_0:
+  assumes holg: "g holomorphic_on s" and s: "open s"
+      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
+      and [simp]: "f a = deriv g a" "g a = 0"
+    shows "f holomorphic_on s"
+  using pole_theorem_open [OF holg s eq]
+  by (rule holomorphic_transform) (auto simp: eq divide_simps)
+
+lemma pole_theorem_analytic:
+  assumes g: "g analytic_on s"
+      and eq: "\<And>z. z \<in> s
+             \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
+    shows "(\<lambda>z. if z = a then deriv g a
+                 else f z - g a/(z - a)) analytic_on s"
+using g
+apply (simp add: analytic_on_def Ball_def)
+apply (safe elim!: all_forward dest!: eq)
+apply (rule_tac x="min d e" in exI, simp)
+apply (rule pole_theorem_open)
+apply (auto simp: holomorphic_on_subset subset_ball)
+done
+
+lemma pole_theorem_analytic_0:
+  assumes g: "g analytic_on s"
+      and eq: "\<And>z. z \<in> s \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
+      and [simp]: "f a = deriv g a" "g a = 0"
+    shows "f analytic_on s"
+proof -
+  have [simp]: "(\<lambda>z. if z = a then deriv g a else f z - g a / (z - a)) = f"
+    by auto
+  show ?thesis
+    using pole_theorem_analytic [OF g eq] by simp
+qed
+
+lemma pole_theorem_analytic_open_superset:
+  assumes g: "g analytic_on s" and "s \<subseteq> t" "open t"
+      and eq: "\<And>z. z \<in> t - {a} \<Longrightarrow> g z = (z - a) * f z"
+    shows "(\<lambda>z. if z = a then deriv g a
+                 else f z - g a/(z - a)) analytic_on s"
+  apply (rule pole_theorem_analytic [OF g])
+  apply (rule openE [OF \<open>open t\<close>])
+  using assms eq by auto
+
+lemma pole_theorem_analytic_open_superset_0:
+  assumes g: "g analytic_on s" "s \<subseteq> t" "open t" "\<And>z. z \<in> t - {a} \<Longrightarrow> g z = (z - a) * f z"
+      and [simp]: "f a = deriv g a" "g a = 0"
+    shows "f analytic_on s"
+proof -
+  have [simp]: "(\<lambda>z. if z = a then deriv g a else f z - g a / (z - a)) = f"
+    by auto
+  have "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on s"
+    by (rule pole_theorem_analytic_open_superset [OF g])
+  then show ?thesis by simp
+qed
+
+
+
+subsection\<open>General, homology form of Cauchy's theorem.\<close>
+
+text\<open>Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\<close>
+
+text\<open>This version has @{term"polynomial_function \<gamma>"} as an additional assumption.\<close>
+lemma Cauchy_integral_formula_global_weak:
+    assumes u: "open u" and holf: "f holomorphic_on u"
+        and z: "z \<in> u" and \<gamma>: "polynomial_function \<gamma>"
+        and pasz: "path_image \<gamma> \<subseteq> u - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+        and zero: "\<And>w. w \<notin> u \<Longrightarrow> winding_number \<gamma> w = 0"
+      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+proof -
+  obtain \<gamma>' where pf\<gamma>': "polynomial_function \<gamma>'" and \<gamma>': "\<And>x. (\<gamma> has_vector_derivative (\<gamma>' x)) (at x)"
+    using has_vector_derivative_polynomial_function [OF \<gamma>] by blast
+  then have "bounded(path_image \<gamma>')"
+    by (simp add: path_image_def compact_imp_bounded compact_continuous_image continuous_on_polymonial_function)
+  then obtain B where "B>0" and B: "\<And>x. x \<in> path_image \<gamma>' \<Longrightarrow> norm x \<le> B"
+    using bounded_pos by force
+  def d \<equiv> "\<lambda>z w. if w = z then deriv f z else (f w - f z)/(w - z)"
+  def v \<equiv> "{w. w \<notin> path_image \<gamma> \<and> winding_number \<gamma> w = 0}"
+  have "path \<gamma>" "valid_path \<gamma>" using \<gamma>
+    by (auto simp: path_polynomial_function valid_path_polynomial_function)
+  then have ov: "open v"
+    by (simp add: v_def open_winding_number_levelsets loop)
+  have uv_Un: "u \<union> v = UNIV"
+    using pasz zero by (auto simp: v_def)
+  have conf: "continuous_on u f"
+    by (metis holf holomorphic_on_imp_continuous_on)
+  have hol_d: "(d y) holomorphic_on u" if "y \<in> u" for y
+  proof -
+    have *: "(\<lambda>c. if c = y then deriv f y else (f c - f y) / (c - y)) holomorphic_on u"
+      by (simp add: holf pole_lemma_open u)
+    then have "isCont (\<lambda>x. if x = y then deriv f y else (f x - f y) / (x - y)) y"
+      using at_within_open complex_differentiable_imp_continuous_at holomorphic_on_def that u by fastforce
+    then have "continuous_on u (d y)"
+      apply (simp add: d_def continuous_on_eq_continuous_at u, clarify)
+      using * holomorphic_on_def
+      by (meson complex_differentiable_within_open complex_differentiable_imp_continuous_at u)
+    moreover have "d y holomorphic_on u - {y}"
+      apply (simp add: d_def holomorphic_on_open u open_delete complex_differentiable_def [symmetric])
+      apply (intro ballI)
+      apply (rename_tac w)
+      apply (rule_tac d="dist w y" and f = "\<lambda>w. (f w - f y)/(w - y)" in complex_differentiable_transform_within)
+      apply (auto simp: dist_pos_lt dist_commute intro!: derivative_intros)
+      using analytic_on_imp_differentiable_at analytic_on_open holf u apply blast
+      done
+    ultimately show ?thesis
+      by (rule no_isolated_singularity) (auto simp: u)
+  qed
+  have cint_fxy: "(\<lambda>x. (f x - f y) / (x - y)) contour_integrable_on \<gamma>" if "y \<notin> path_image \<gamma>" for y
+    apply (rule contour_integrable_holomorphic_simple [where s = "u-{y}"])
+    using \<open>valid_path \<gamma>\<close> pasz
+    apply (auto simp: u open_delete)
+    apply (rule continuous_intros holomorphic_intros continuous_on_subset [OF conf] holomorphic_on_subset [OF holf] |
+                force simp add: that)+
+    done
+  def h \<equiv> "\<lambda>z. if z \<in> u then contour_integral \<gamma> (d z) else contour_integral \<gamma> (\<lambda>w. f w/(w - z))"
+  have U: "\<And>z. z \<in> u \<Longrightarrow> ((d z) has_contour_integral h z) \<gamma>"
+    apply (simp add: h_def)
+    apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where s=u]])
+    using u pasz \<open>valid_path \<gamma>\<close>
+    apply (auto intro: holomorphic_on_imp_continuous_on hol_d)
+    done
+  have V: "((\<lambda>w. f w / (w - z)) has_contour_integral h z) \<gamma>" if z: "z \<in> v" for z
+  proof -
+    have 0: "0 = (f z) * 2 * of_real (2 * pi) * \<i> * winding_number \<gamma> z"
+      using v_def z by auto
+    then have "((\<lambda>x. 1 / (x - z)) has_contour_integral 0) \<gamma>"
+     using z v_def  has_contour_integral_winding_number [OF \<open>valid_path \<gamma>\<close>] by fastforce
+    then have "((\<lambda>x. f z * (1 / (x - z))) has_contour_integral 0) \<gamma>"
+      using has_contour_integral_lmul by fastforce
+    then have "((\<lambda>x. f z / (x - z)) has_contour_integral 0) \<gamma>"
+      by (simp add: divide_simps)
+    moreover have "((\<lambda>x. (f x - f z) / (x - z)) has_contour_integral contour_integral \<gamma> (d z)) \<gamma>"
+      using z
+      apply (auto simp: v_def)
+      apply (metis (no_types, lifting) contour_integrable_eq d_def has_contour_integral_eq has_contour_integral_integral cint_fxy)
+      done
+    ultimately have *: "((\<lambda>x. f z / (x - z) + (f x - f z) / (x - z)) has_contour_integral (0 + contour_integral \<gamma> (d z))) \<gamma>"
+      by (rule has_contour_integral_add)
+    have "((\<lambda>w. f w / (w - z)) has_contour_integral contour_integral \<gamma> (d z)) \<gamma>"
+            if  "z \<in> u"
+      using * by (auto simp: divide_simps has_contour_integral_eq)
+    moreover have "((\<lambda>w. f w / (w - z)) has_contour_integral contour_integral \<gamma> (\<lambda>w. f w / (w - z))) \<gamma>"
+            if "z \<notin> u"
+      apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where s=u]])
+      using u pasz \<open>valid_path \<gamma>\<close> that
+      apply (auto intro: holomorphic_on_imp_continuous_on hol_d)
+      apply (rule continuous_intros conf holomorphic_intros holf | force)+
+      done
+    ultimately show ?thesis
+      using z by (simp add: h_def)
+  qed
+  have znot: "z \<notin> path_image \<gamma>"
+    using pasz by blast
+  obtain d0 where "d0>0" and d0: "\<And>x y. x \<in> path_image \<gamma> \<Longrightarrow> y \<in> - u \<Longrightarrow> d0 \<le> dist x y"
+    using separate_compact_closed [of "path_image \<gamma>" "-u"] pasz u
+    by (fastforce simp add: \<open>path \<gamma>\<close> compact_path_image)
+  obtain dd where "0 < dd" and dd: "{y + k | y k. y \<in> path_image \<gamma> \<and> k \<in> ball 0 dd} \<subseteq> u"
+    apply (rule that [of "d0/2"])
+    using \<open>0 < d0\<close>
+    apply (auto simp: dist_norm dest: d0)
+    done
+  have "\<And>x x'. \<lbrakk>x \<in> path_image \<gamma>; dist x x' * 2 < dd\<rbrakk> \<Longrightarrow> \<exists>y k. x' = y + k \<and> y \<in> path_image \<gamma> \<and> dist 0 k * 2 \<le> dd"
+    apply (rule_tac x=x in exI)
+    apply (rule_tac x="x'-x" in exI)
+    apply (force simp add: dist_norm)
+    done
+  then have 1: "path_image \<gamma> \<subseteq> interior {y + k |y k. y \<in> path_image \<gamma> \<and> k \<in> cball 0 (dd / 2)}"
+    apply (clarsimp simp add: mem_interior)
+    using \<open>0 < dd\<close>
+    apply (rule_tac x="dd/2" in exI, auto)
+    done
+  obtain t where "compact t" and subt: "path_image \<gamma> \<subseteq> interior t" and t: "t \<subseteq> u"
+    apply (rule that [OF _ 1])
+    apply (fastforce simp add: \<open>valid_path \<gamma>\<close> compact_valid_path_image intro!: compact_sums)
+    apply (rule order_trans [OF _ dd])
+    using \<open>0 < dd\<close> by fastforce
+  obtain L where "L>0"
+           and L: "\<And>f B. \<lbrakk>f holomorphic_on interior t; \<And>z. z\<in>interior t \<Longrightarrow> cmod (f z) \<le> B\<rbrakk> \<Longrightarrow>
+                         cmod (contour_integral \<gamma> f) \<le> L * B"
+      using contour_integral_bound_exists [OF open_interior \<open>valid_path \<gamma>\<close> subt]
+      by blast
+  have "bounded(f ` t)"
+    by (meson \<open>compact t\<close> compact_continuous_image compact_imp_bounded conf continuous_on_subset t)
+  then obtain D where "D>0" and D: "\<And>x. x \<in> t \<Longrightarrow> norm (f x) \<le> D"
+    by (auto simp: bounded_pos)
+  obtain C where "C>0" and C: "\<And>x. x \<in> t \<Longrightarrow> norm x \<le> C"
+    using \<open>compact t\<close> bounded_pos compact_imp_bounded by force
+  have "dist (h y) 0 \<le> e" if "0 < e" and le: "D * L / e + C \<le> cmod y" for e y
+  proof -
+    have "D * L / e > 0"  using \<open>D>0\<close> \<open>L>0\<close> \<open>e>0\<close> by simp
+    with le have ybig: "norm y > C" by force
+    with C have "y \<notin> t"  by force
+    then have ynot: "y \<notin> path_image \<gamma>"
+      using subt interior_subset by blast
+    have [simp]: "winding_number \<gamma> y = 0"
+      apply (rule winding_number_zero_outside [of _ "cball 0 C"])
+      using ybig interior_subset subt
+      apply (force simp add: loop \<open>path \<gamma>\<close> dist_norm intro!: C)+
+      done
+    have [simp]: "h y = contour_integral \<gamma> (\<lambda>w. f w/(w - y))"
+      by (rule contour_integral_unique [symmetric]) (simp add: v_def ynot V)
+    have holint: "(\<lambda>w. f w / (w - y)) holomorphic_on interior t"
+      apply (rule holomorphic_on_divide)
+      using holf holomorphic_on_subset interior_subset t apply blast
+      apply (rule holomorphic_intros)+
+      using \<open>y \<notin> t\<close> interior_subset by auto
+    have leD: "cmod (f z / (z - y)) \<le> D * (e / L / D)" if z: "z \<in> interior t" for z
+    proof -
+      have "D * L / e + cmod z \<le> cmod y"
+        using le C [of z] z using interior_subset by force
+      then have DL2: "D * L / e \<le> cmod (z - y)"
+        using norm_triangle_ineq2 [of y z] by (simp add: norm_minus_commute)
+      have "cmod (f z / (z - y)) = cmod (f z) * inverse (cmod (z - y))"
+        by (simp add: norm_mult norm_inverse Fields.field_class.field_divide_inverse)
+      also have "... \<le> D * (e / L / D)"
+        apply (rule mult_mono)
+        using that D interior_subset apply blast
+        using \<open>L>0\<close> \<open>e>0\<close> \<open>D>0\<close> DL2
+        apply (auto simp: norm_divide divide_simps algebra_simps)
+        done
+      finally show ?thesis .
+    qed
+    have "dist (h y) 0 = cmod (contour_integral \<gamma> (\<lambda>w. f w / (w - y)))"
+      by (simp add: dist_norm)
+    also have "... \<le> L * (D * (e / L / D))"
+      by (rule L [OF holint leD])
+    also have "... = e"
+      using  \<open>L>0\<close> \<open>0 < D\<close> by auto
+    finally show ?thesis .
+  qed
+  then have "(h \<longlongrightarrow> 0) at_infinity"
+    by (meson Lim_at_infinityI)
+  moreover have "h holomorphic_on UNIV"
+  proof -
+    have con_ff: "continuous (at (x,z)) (\<lambda>y. (f(snd y) - f(fst y)) / (snd y - fst y))"
+                 if "x \<in> u" "z \<in> u" "x \<noteq> z" for x z
+      using that conf
+      apply (simp add: continuous_on_eq_continuous_at u)
+      apply (simp | rule continuous_intros continuous_within_compose2 [where g=f])+
+      done
+    have con_fstsnd: "continuous_on UNIV (\<lambda>x. (fst x - snd x) ::complex)"
+      by (rule continuous_intros)+
+    have open_uu_Id: "open (u \<times> u - Id)"
+      apply (rule open_Diff)
+      apply (simp add: open_Times u)
+      using continuous_closed_preimage_constant [OF con_fstsnd closed_UNIV, of 0]
+      apply (auto simp: Id_fstsnd_eq algebra_simps)
+      done
+    have con_derf: "continuous (at z) (deriv f)" if "z \<in> u" for z
+      apply (rule continuous_on_interior [of u])
+      apply (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on u)
+      by (simp add: interior_open that u)
+    have tendsto_f': "((\<lambda>x. if snd x = fst x then deriv f (fst x)
+                                    else (f (snd x) - f (fst x)) / (snd x - fst x)) \<longlongrightarrow> deriv f x)
+                      (at (x, x) within u \<times> u)" if "x \<in> u" for x
+    proof (rule Lim_withinI)
+      fix e::real assume "0 < e"
+      obtain k1 where "k1>0" and k1: "\<And>x'. norm (x' - x) \<le> k1 \<Longrightarrow> norm (deriv f x' - deriv f x) < e"
+        using \<open>0 < e\<close> continuous_within_E [OF con_derf [OF \<open>x \<in> u\<close>]]
+        by (metis UNIV_I dist_norm)
+      obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> u" by (blast intro: openE [OF u] \<open>x \<in> u\<close>)
+      have neq: "norm ((f z' - f x') / (z' - x') - deriv f x) \<le> e"
+                    if "z' \<noteq> x'" and less_k1: "norm (x'-x, z'-x) < k1" and less_k2: "norm (x'-x, z'-x) < k2"
+                 for x' z'
+      proof -
+        have cs_less: "w \<in> closed_segment x' z' \<Longrightarrow> cmod (w - x) \<le> norm (x'-x, z'-x)" for w
+          apply (drule segment_furthest_le [where y=x])
+          by (metis (no_types) dist_commute dist_norm norm_fst_le norm_snd_le order_trans)
+        have derf_le: "w \<in> closed_segment x' z' \<Longrightarrow> z' \<noteq> x' \<Longrightarrow> cmod (deriv f w - deriv f x) \<le> e" for w
+          by (blast intro: cs_less less_k1 k1 [unfolded divide_const_simps dist_norm] less_imp_le le_less_trans)
+        have f_has_der: "\<And>x. x \<in> u \<Longrightarrow> (f has_field_derivative deriv f x) (at x within u)"
+          by (metis DERIV_deriv_iff_complex_differentiable at_within_open holf holomorphic_on_def u)
+        have "closed_segment x' z' \<subseteq> u"
+          by (rule order_trans [OF _ k2]) (simp add: cs_less  le_less_trans [OF _ less_k2] dist_complex_def norm_minus_commute subset_iff)
+        then have cint_derf: "(deriv f has_contour_integral f z' - f x') (linepath x' z')"
+          using contour_integral_primitive [OF f_has_der valid_path_linepath] pasz  by simp
+        then have *: "((\<lambda>x. deriv f x / (z' - x')) has_contour_integral (f z' - f x') / (z' - x')) (linepath x' z')"
+          by (rule has_contour_integral_div)
+        have "norm ((f z' - f x') / (z' - x') - deriv f x) \<le> e/norm(z' - x') * norm(z' - x')"
+          apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_diff [OF *]])
+          using has_contour_integral_div [where c = "z' - x'", OF has_contour_integral_const_linepath [of "deriv f x" z' x']]
+                 \<open>e > 0\<close>  \<open>z' \<noteq> x'\<close>
+          apply (auto simp: norm_divide divide_simps derf_le)
+          done
+        also have "... \<le> e" using \<open>0 < e\<close> by simp
+        finally show ?thesis .
+      qed
+      show "\<exists>d>0. \<forall>xa\<in>u \<times> u.
+                  0 < dist xa (x, x) \<and> dist xa (x, x) < d \<longrightarrow>
+                  dist (if snd xa = fst xa then deriv f (fst xa) else (f (snd xa) - f (fst xa)) / (snd xa - fst xa))
+                       (deriv f x)  \<le>  e"
+        apply (rule_tac x="min k1 k2" in exI)
+        using \<open>k1>0\<close> \<open>k2>0\<close> \<open>e>0\<close>
+        apply (force simp: dist_norm neq intro: dual_order.strict_trans2 k1 less_imp_le norm_fst_le)
+        done
+    qed
+    have con_pa_f: "continuous_on (path_image \<gamma>) f"
+      by (meson holf holomorphic_on_imp_continuous_on holomorphic_on_subset interior_subset subt t)
+    have le_B: "\<And>t. t \<in> {0..1} \<Longrightarrow> cmod (vector_derivative \<gamma> (at t)) \<le> B"
+      apply (rule B)
+      using \<gamma>' using path_image_def vector_derivative_at by fastforce
+    have f_has_cint: "\<And>w. w \<in> v - path_image \<gamma> \<Longrightarrow> ((\<lambda>u. f u / (u - w) ^ 1) has_contour_integral h w) \<gamma>"
+      by (simp add: V)
+    have cond_uu: "continuous_on (u \<times> u) (\<lambda>y. d (fst y) (snd y))"
+      apply (simp add: continuous_on_eq_continuous_within d_def continuous_within tendsto_f')
+      apply (simp add: Lim_within_open_NO_MATCH open_Times u, clarify)
+      apply (rule Lim_transform_within_open [OF _ open_uu_Id, where f = "(\<lambda>x. (f (snd x) - f (fst x)) / (snd x - fst x))"])
+      using con_ff
+      apply (auto simp: continuous_within)
+      done
+    have hol_dw: "(\<lambda>z. d z w) holomorphic_on u" if "w \<in> u" for w
+    proof -
+      have "continuous_on u ((\<lambda>y. d (fst y) (snd y)) o (\<lambda>z. (w,z)))"
+        by (rule continuous_on_compose continuous_intros continuous_on_subset [OF cond_uu] | force intro: that)+
+      then have *: "continuous_on u (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z))"
+        by (rule rev_iffD1 [OF _ continuous_on_cong [OF refl]]) (simp add: d_def field_simps)
+      have **: "\<And>x. \<lbrakk>x \<in> u; x \<noteq> w\<rbrakk> \<Longrightarrow> (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z)) complex_differentiable at x"
+        apply (rule_tac f = "\<lambda>x. (f w - f x)/(w - x)" and d = "dist x w" in complex_differentiable_transform_within)
+        apply (rule u derivative_intros holomorphic_on_imp_differentiable_at [OF holf] | force simp add: dist_commute)+
+        done
+      show ?thesis
+        unfolding d_def
+        apply (rule no_isolated_singularity [OF * _ u, where k = "{w}"])
+        apply (auto simp: complex_differentiable_def [symmetric] holomorphic_on_open open_Diff u **)
+        done
+    qed
+    { fix a b
+      assume abu: "closed_segment a b \<subseteq> u"
+      then have cont_dw: "\<And>w. w \<in> u \<Longrightarrow> (\<lambda>z. d z w) contour_integrable_on (linepath a b)"
+        by (metis hol_dw continuous_on_subset contour_integrable_continuous_linepath holomorphic_on_imp_continuous_on)
+      have *: "\<exists>da>0. \<forall>x'\<in>u. dist x' w < da \<longrightarrow>
+                             dist (contour_integral (linepath a b) (\<lambda>z. d z x'))
+                                  (contour_integral (linepath a b) (\<lambda>z. d z w)) \<le> ee"
+              if "w \<in> u" "0 < ee" "a \<noteq> b" for w ee
+      proof -
+        obtain dd where "dd>0" and dd: "cball w dd \<subseteq> u" using open_contains_cball u \<open>w \<in> u\<close> by force
+        let ?abdd = "{(z,t) |z t. z \<in> closed_segment a b \<and> t \<in> cball w dd}"
+        have "uniformly_continuous_on ?abdd (\<lambda>y. d (fst y) (snd y))"
+          apply (rule compact_uniformly_continuous)
+          apply (rule continuous_on_subset[OF cond_uu])
+          using abu dd
+          apply (auto simp: compact_Times simp del: mem_cball)
+          done
+        then obtain kk where "kk>0"
+            and kk: "\<And>x x'. \<lbrakk>x\<in>?abdd; x'\<in>?abdd; dist x' x < kk\<rbrakk> \<Longrightarrow>
+                             dist ((\<lambda>y. d (fst y) (snd y)) x') ((\<lambda>y. d (fst y) (snd y)) x) < ee/norm(b - a)"
+          apply (rule uniformly_continuous_onE [where e = "ee/norm(b - a)"])
+          using \<open>0 < ee\<close> \<open>a \<noteq> b\<close> by auto
+        have kk: "\<lbrakk>x1 \<in> closed_segment a b; norm (w - x2) \<le> dd;
+                   x1' \<in> closed_segment a b; norm (w - x2') \<le> dd; norm ((x1', x2') - (x1, x2)) < kk\<rbrakk>
+                  \<Longrightarrow> norm (d x1' x2' - d x1 x2) \<le> ee / cmod (b - a)"
+                 for x1 x2 x1' x2'
+          using kk [of "(x1,x2)" "(x1',x2')"] by (force simp add: dist_norm)
+        have le_ee: "cmod (contour_integral (linepath a b) (\<lambda>x. d x x' - d x w)) \<le> ee"
+                    if "x' \<in> u" "cmod (x' - w) < dd" "cmod (x' - w) < kk"  for x'
+        proof -
+          have "cmod (contour_integral (linepath a b) (\<lambda>x. d x x' - d x w)) \<le> ee/norm(b - a) * norm(b - a)"
+            apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_integral _ kk])
+            apply (rule contour_integrable_diff [OF cont_dw cont_dw])
+            using \<open>0 < ee\<close> \<open>a \<noteq> b\<close> \<open>0 < dd\<close> \<open>w \<in> u\<close> that
+            apply (auto simp: norm_minus_commute)
+            done
+          also have "... = ee" using \<open>a \<noteq> b\<close> by simp
+          finally show ?thesis .
+        qed
+        show ?thesis
+          apply (rule_tac x="min dd kk" in exI)
+          using \<open>0 < dd\<close> \<open>0 < kk\<close>
+          apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> u\<close> intro: le_ee)
+          done
+      qed
+      have cont_cint_d: "continuous_on u (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
+        apply (rule continuous_onI)
+        apply (cases "a=b")
+        apply (auto intro: *)
+        done
+      have cont_cint_d\<gamma>: "continuous_on {0..1} ((\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w)) o \<gamma>)"
+        apply (rule continuous_on_compose)
+        using \<open>path \<gamma>\<close> path_def pasz
+        apply (auto intro!: continuous_on_subset [OF cont_cint_d])
+        apply (force simp add: path_image_def)
+        done
+      have cint_cint: "(\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w)) contour_integrable_on \<gamma>"
+        apply (simp add: contour_integrable_on)
+        apply (rule integrable_continuous_real)
+        apply (rule continuous_on_mult [OF cont_cint_d\<gamma> [unfolded o_def]])
+        using pf\<gamma>'
+        by (simp add: continuous_on_polymonial_function vector_derivative_at [OF \<gamma>'])
+      have "contour_integral (linepath a b) h = contour_integral (linepath a b) (\<lambda>z. contour_integral \<gamma> (d z))"
+        using abu  by (force simp add: h_def intro: contour_integral_eq)
+      also have "... =  contour_integral \<gamma> (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
+        apply (rule contour_integral_swap)
+        apply (simp add: split_def)
+        apply (rule continuous_on_subset [OF cond_uu])
+        using abu pasz \<open>valid_path \<gamma>\<close>
+        apply (auto intro!: continuous_intros)
+        by (metis \<gamma>' continuous_on_eq path_def path_polynomial_function pf\<gamma>' vector_derivative_at)
+      finally have cint_h_eq:
+          "contour_integral (linepath a b) h =
+                    contour_integral \<gamma> (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))" .
+      note cint_cint cint_h_eq
+    } note cint_h = this
+    have conthu: "continuous_on u h"
+    proof (simp add: continuous_on_sequentially, clarify)
+      fix a x
+      assume x: "x \<in> u" and au: "\<forall>n. a n \<in> u" and ax: "a \<longlonglongrightarrow> x"
+      then have A1: "\<forall>\<^sub>F n in sequentially. d (a n) contour_integrable_on \<gamma>"
+        by (meson U contour_integrable_on_def eventuallyI)
+      obtain dd where "dd>0" and dd: "cball x dd \<subseteq> u" using open_contains_cball u x by force
+      have A2: "\<forall>\<^sub>F n in sequentially. \<forall>xa\<in>path_image \<gamma>. cmod (d (a n) xa - d x xa) < ee" if "0 < ee" for ee
+      proof -
+        let ?ddpa = "{(w,z) |w z. w \<in> cball x dd \<and> z \<in> path_image \<gamma>}"
+        have "uniformly_continuous_on ?ddpa (\<lambda>y. d (fst y) (snd y))"
+          apply (rule compact_uniformly_continuous [OF continuous_on_subset[OF cond_uu]])
+          using dd pasz \<open>valid_path \<gamma>\<close>
+          apply (auto simp: compact_Times compact_valid_path_image simp del: mem_cball)
+          done
+        then obtain kk where "kk>0"
+            and kk: "\<And>x x'. \<lbrakk>x\<in>?ddpa; x'\<in>?ddpa; dist x' x < kk\<rbrakk> \<Longrightarrow>
+                             dist ((\<lambda>y. d (fst y) (snd y)) x') ((\<lambda>y. d (fst y) (snd y)) x) < ee"
+          apply (rule uniformly_continuous_onE [where e = ee])
+          using \<open>0 < ee\<close> by auto
+
+        have kk: "\<lbrakk>norm (w - x) \<le> dd; z \<in> path_image \<gamma>; norm ((w, z) - (x, z)) < kk\<rbrakk> \<Longrightarrow> norm (d w z - d x z) < ee"
+                 for  w z
+          using \<open>dd>0\<close> kk [of "(x,z)" "(w,z)"] by (force simp add: norm_minus_commute dist_norm)
+        show ?thesis
+          using ax unfolding lim_sequentially eventually_sequentially
+          apply (drule_tac x="min dd kk" in spec)
+          using \<open>dd > 0\<close> \<open>kk > 0\<close>
+          apply (fastforce simp: kk dist_norm)
+          done
+      qed
+      have tendsto_hx: "(\<lambda>n. contour_integral \<gamma> (d (a n))) \<longlonglongrightarrow> h x"
+        apply (simp add: contour_integral_unique [OF U, symmetric] x)
+        apply (rule contour_integral_uniform_limit [OF A1 A2 le_B])
+        apply (auto simp: \<open>valid_path \<gamma>\<close>)
+        done
+      then show "(h \<circ> a) \<longlonglongrightarrow> h x"
+        by (simp add: h_def x au o_def)
+    qed
+    show ?thesis
+    proof (simp add: holomorphic_on_open complex_differentiable_def [symmetric], clarify)
+      fix z0
+      consider "z0 \<in> v" | "z0 \<in> u" using uv_Un by blast
+      then show "h complex_differentiable at z0"
+      proof cases
+        assume "z0 \<in> v" then show ?thesis
+          using Cauchy_next_derivative [OF con_pa_f le_B f_has_cint _ ov] V f_has_cint \<open>valid_path \<gamma>\<close>
+          by (auto simp: complex_differentiable_def v_def)
+      next
+        assume "z0 \<in> u" then
+        obtain e where "e>0" and e: "ball z0 e \<subseteq> u" by (blast intro: openE [OF u])
+        have *: "contour_integral (linepath a b) h + contour_integral (linepath b c) h + contour_integral (linepath c a) h = 0"
+                if abc_subset: "convex hull {a, b, c} \<subseteq> ball z0 e"  for a b c
+        proof -
+          have *: "\<And>x1 x2 z. z \<in> u \<Longrightarrow> closed_segment x1 x2 \<subseteq> u \<Longrightarrow> (\<lambda>w. d w z) contour_integrable_on linepath x1 x2"
+            using  hol_dw holomorphic_on_imp_continuous_on u
+            by (auto intro!: contour_integrable_holomorphic_simple)
+          have abc: "closed_segment a b \<subseteq> u"  "closed_segment b c \<subseteq> u"  "closed_segment c a \<subseteq> u"
+            using that e segments_subset_convex_hull by fastforce+
+          have eq0: "\<And>w. w \<in> u \<Longrightarrow> contour_integral (linepath a b +++ linepath b c +++ linepath c a) (\<lambda>z. d z w) = 0"
+            apply (rule contour_integral_unique [OF Cauchy_theorem_triangle])
+            apply (rule holomorphic_on_subset [OF hol_dw])
+            using e abc_subset by auto
+          have "contour_integral \<gamma>
+                   (\<lambda>x. contour_integral (linepath a b) (\<lambda>z. d z x) +
+                        (contour_integral (linepath b c) (\<lambda>z. d z x) +
+                         contour_integral (linepath c a) (\<lambda>z. d z x)))  =  0"
+            apply (rule contour_integral_eq_0)
+            using abc pasz u
+            apply (subst contour_integral_join [symmetric], auto intro: eq0 *)+
+            done
+          then show ?thesis
+            by (simp add: cint_h abc contour_integrable_add contour_integral_add [symmetric] add_ac)
+        qed
+        show ?thesis
+          using e \<open>e > 0\<close>
+          by (auto intro!: holomorphic_on_imp_differentiable_at [OF _ open_ball] analytic_imp_holomorphic
+                           Morera_triangle continuous_on_subset [OF conthu] *)
+      qed
+    qed
+  qed
+  ultimately have [simp]: "h z = 0" for z
+    by (meson Liouville_weak)
+  have "((\<lambda>w. 1 / (w - z)) has_contour_integral complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z) \<gamma>"
+    by (rule has_contour_integral_winding_number [OF \<open>valid_path \<gamma>\<close> znot])
+  then have "((\<lambda>w. f z * (1 / (w - z))) has_contour_integral complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z * f z) \<gamma>"
+    by (metis mult.commute has_contour_integral_lmul)
+  then have 1: "((\<lambda>w. f z / (w - z)) has_contour_integral complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z * f z) \<gamma>"
+    by (simp add: divide_simps)
+  moreover have 2: "((\<lambda>w. (f w - f z) / (w - z)) has_contour_integral 0) \<gamma>"
+    using U [OF z] pasz d_def by (force elim: has_contour_integral_eq [where g = "\<lambda>w. (f w - f z)/(w - z)"])
+  show ?thesis
+    using has_contour_integral_add [OF 1 2]  by (simp add: diff_divide_distrib)
+qed
+
+
+theorem Cauchy_integral_formula_global:
+    assumes s: "open s" and holf: "f holomorphic_on s"
+        and z: "z \<in> s" and vpg: "valid_path \<gamma>"
+        and pasz: "path_image \<gamma> \<subseteq> s - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+        and zero: "\<And>w. w \<notin> s \<Longrightarrow> winding_number \<gamma> w = 0"
+      shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \<gamma> z * f z)) \<gamma>"
+proof -
+  have "path \<gamma>" using vpg by (blast intro: valid_path_imp_path)
+  have hols: "(\<lambda>w. f w / (w - z)) holomorphic_on s - {z}" "(\<lambda>w. 1 / (w - z)) holomorphic_on s - {z}"
+    by (rule holomorphic_intros holomorphic_on_subset [OF holf] | force)+
+  then have cint_fw: "(\<lambda>w. f w / (w - z)) contour_integrable_on \<gamma>"
+    by (meson contour_integrable_holomorphic_simple holomorphic_on_imp_continuous_on open_delete s vpg pasz)
+  obtain d where "d>0"
+      and d: "\<And>g h. \<lbrakk>valid_path g; valid_path h; \<forall>t\<in>{0..1}. cmod (g t - \<gamma> t) < d \<and> cmod (h t - \<gamma> t) < d;
+                     pathstart h = pathstart g \<and> pathfinish h = pathfinish g\<rbrakk>
+                     \<Longrightarrow> path_image h \<subseteq> s - {z} \<and> (\<forall>f. f holomorphic_on s - {z} \<longrightarrow> contour_integral h f = contour_integral g f)"
+    using contour_integral_nearby_ends [OF _ \<open>path \<gamma>\<close> pasz] s by (simp add: open_Diff) metis
+  obtain p where polyp: "polynomial_function p"
+             and ps: "pathstart p = pathstart \<gamma>" and pf: "pathfinish p = pathfinish \<gamma>" and led: "\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < d"
+    using path_approx_polynomial_function [OF \<open>path \<gamma>\<close> \<open>d > 0\<close>] by blast
+  then have ploop: "pathfinish p = pathstart p" using loop by auto
+  have vpp: "valid_path p"  using polyp valid_path_polynomial_function by blast
+  have [simp]: "z \<notin> path_image \<gamma>" using pasz by blast
+  have paps: "path_image p \<subseteq> s - {z}" and cint_eq: "(\<And>f. f holomorphic_on s - {z} \<Longrightarrow> contour_integral p f = contour_integral \<gamma> f)"
+    using pf ps led d [OF vpg vpp] \<open>d > 0\<close> by auto
+  have wn_eq: "winding_number p z = winding_number \<gamma> z"
+    using vpp paps
+    by (simp add: subset_Diff_insert vpg valid_path_polynomial_function winding_number_valid_path cint_eq hols)
+  have "winding_number p w = winding_number \<gamma> w" if "w \<notin> s" for w
+  proof -
+    have hol: "(\<lambda>v. 1 / (v - w)) holomorphic_on s - {z}"
+      using that by (force intro: holomorphic_intros holomorphic_on_subset [OF holf])
+   have "w \<notin> path_image p" "w \<notin> path_image \<gamma>" using paps pasz that by auto
+   then show ?thesis
+    using vpp vpg by (simp add: subset_Diff_insert valid_path_polynomial_function winding_number_valid_path cint_eq [OF hol])
+  qed
+  then have wn0: "\<And>w. w \<notin> s \<Longrightarrow> winding_number p w = 0"
+    by (simp add: zero)
+  show ?thesis
+    using Cauchy_integral_formula_global_weak [OF s holf z polyp paps ploop wn0] hols
+    by (metis wn_eq cint_eq has_contour_integral_eqpath cint_fw cint_eq)
+qed
+
+theorem Cauchy_theorem_global:
+    assumes s: "open s" and holf: "f holomorphic_on s"
+        and vpg: "valid_path \<gamma>" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+        and pas: "path_image \<gamma> \<subseteq> s"
+        and zero: "\<And>w. w \<notin> s \<Longrightarrow> winding_number \<gamma> w = 0"
+      shows "(f has_contour_integral 0) \<gamma>"
+proof -
+  obtain z where "z \<in> s" and znot: "z \<notin> path_image \<gamma>"
+  proof -
+    have "compact (path_image \<gamma>)"
+      using compact_valid_path_image vpg by blast
+    then have "path_image \<gamma> \<noteq> s"
+      by (metis (no_types) compact_open path_image_nonempty s)
+    with pas show ?thesis by (blast intro: that)
+  qed
+  then have pasz: "path_image \<gamma> \<subseteq> s - {z}" using pas by blast
+  have hol: "(\<lambda>w. (w - z) * f w) holomorphic_on s"
+    by (rule holomorphic_intros holf)+
+  show ?thesis
+    using Cauchy_integral_formula_global [OF s hol \<open>z \<in> s\<close> vpg pasz loop zero]
+    by (auto simp: znot elim!: has_contour_integral_eq)
+qed
+
+corollary Cauchy_theorem_global_outside:
+    assumes "open s" "f holomorphic_on s" "valid_path \<gamma>"  "pathfinish \<gamma> = pathstart \<gamma>" "path_image \<gamma> \<subseteq> s"
+            "\<And>w. w \<notin> s \<Longrightarrow> w \<in> outside(path_image \<gamma>)"
+      shows "(f has_contour_integral 0) \<gamma>"
+by (metis Cauchy_theorem_global assms winding_number_zero_in_outside valid_path_imp_path)
+
+
 end

--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -5,14 +5,14 @@
 section \<open>Complex Analysis Basics\<close>
 
 theory Complex_Analysis_Basics
-imports Cartesian_Euclidean_Space
+imports Cartesian_Euclidean_Space "~~/src/HOL/Library/Nonpos_Ints"
 begin
 
 
-lemma cmod_fact [simp]: "cmod (fact n) = fact n"
-  by (metis norm_of_nat of_nat_fact)
+subsection\<open>General lemmas\<close>
 
-subsection\<open>General lemmas\<close>
+lemma nonneg_Reals_cmod_eq_Re: "z \<in> \<real>\<^sub>\<ge>\<^sub>0 \<Longrightarrow> norm z = Re z"
+  by (simp add: complex_nonneg_Reals_iff cmod_eq_Re)
 
 lemma has_derivative_mult_right:
   fixes c:: "'a :: real_normed_algebra"
@@ -223,10 +223,26 @@
 lemma closed_Real_halfspace_Re_le: "closed (\<real> \<inter> {w. Re w \<le> x})"
   by (simp add: closed_Int closed_complex_Reals closed_halfspace_Re_le)
 
+corollary closed_nonpos_Reals_complex [simp]: "closed (\<real>\<^sub>\<le>\<^sub>0 :: complex set)"
+proof -
+  have "\<real>\<^sub>\<le>\<^sub>0 = \<real> \<inter> {z. Re(z) \<le> 0}"
+    using complex_nonpos_Reals_iff complex_is_Real_iff by auto
+  then show ?thesis
+    by (metis closed_Real_halfspace_Re_le)
+qed
+
 lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
   using closed_halfspace_Re_ge
   by (simp add: closed_Int closed_complex_Reals)
 
+corollary closed_nonneg_Reals_complex [simp]: "closed (\<real>\<^sub>\<ge>\<^sub>0 :: complex set)"
+proof -
+  have "\<real>\<^sub>\<ge>\<^sub>0 = \<real> \<inter> {z. Re(z) \<ge> 0}"
+    using complex_nonneg_Reals_iff complex_is_Real_iff by auto
+  then show ?thesis
+    by (metis closed_Real_halfspace_Re_ge)
+qed
+
 lemma closed_real_abs_le: "closed {w \<in> \<real>. \<bar>Re w\<bar> \<le> r}"
 proof -
   have "{w \<in> \<real>. \<bar>Re w\<bar> \<le> r} = (\<real> \<inter> {w. Re w \<le> r}) \<inter> (\<real> \<inter> {w. Re w \<ge> -r})"
@@ -399,6 +415,16 @@
 
 named_theorems holomorphic_intros "structural introduction rules for holomorphic_on"
 
+lemma holomorphic_onI [intro?]: "(\<And>x. x \<in> s \<Longrightarrow> f complex_differentiable (at x within s)) \<Longrightarrow> f holomorphic_on s"
+  by (simp add: holomorphic_on_def)
+
+lemma holomorphic_onD [dest?]: "\<lbrakk>f holomorphic_on s; x \<in> s\<rbrakk> \<Longrightarrow> f complex_differentiable (at x within s)"
+  by (simp add: holomorphic_on_def)
+
+lemma holomorphic_on_imp_differentiable_at:
+   "\<lbrakk>f holomorphic_on s; open s; x \<in> s\<rbrakk> \<Longrightarrow> f complex_differentiable (at x)"
+using at_within_open holomorphic_on_def by fastforce
+
 lemma holomorphic_on_empty [holomorphic_intros]: "f holomorphic_on {}"
   by (simp add: holomorphic_on_def)
 

--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -27,8 +27,6 @@
   using assms moebius_inverse[of d a "-b" "-c" z]
   by (auto simp: algebra_simps)
 
-
-
 lemma cmod_add_real_less:
   assumes "Im z \<noteq> 0" "r\<noteq>0"
     shows "cmod (z + r) < cmod z + \<bar>r\<bar>"
@@ -1025,14 +1023,16 @@
 subsection\<open>Derivative of Ln away from the branch cut\<close>
 
 lemma
-  assumes "Im(z) = 0 \<Longrightarrow> 0 < Re(z)"
+  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
     shows has_field_derivative_Ln: "(Ln has_field_derivative inverse(z)) (at z)"
       and Im_Ln_less_pi:           "Im (Ln z) < pi"
 proof -
   have znz: "z \<noteq> 0"
     using assms by auto
-  then show *: "Im (Ln z) < pi" using assms
-    by (metis exp_Ln Im_Ln_le_pi Im_exp Re_exp abs_of_nonneg cmod_eq_Re cos_pi mult.right_neutral mult_minus_right mult_zero_right neg_less_0_iff_less norm_exp_eq_Re not_less not_less_iff_gr_or_eq sin_pi)
+  then have "Im (Ln z) \<noteq> pi"
+    by (metis (no_types) Im_exp Ln_in_Reals assms complex_nonpos_Reals_iff complex_is_Real_iff exp_Ln mult_zero_right not_less pi_neq_zero sin_pi znz)
+  then show *: "Im (Ln z) < pi" using assms Im_Ln_le_pi
+    by (simp add: le_neq_trans znz)
   show "(Ln has_field_derivative inverse(z)) (at z)"
     apply (rule has_complex_derivative_inverse_strong_x
               [where f = exp and s = "{w. -pi < Im(w) & Im(w) < pi}"])
@@ -1046,27 +1046,27 @@
 declare has_field_derivative_Ln [derivative_intros]
 declare has_field_derivative_Ln [THEN DERIV_chain2, derivative_intros]
 
-lemma complex_differentiable_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln complex_differentiable at z"
+lemma complex_differentiable_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln complex_differentiable at z"
   using complex_differentiable_def has_field_derivative_Ln by blast
 
-lemma complex_differentiable_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z))
+lemma complex_differentiable_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0
          \<Longrightarrow> Ln complex_differentiable (at z within s)"
   using complex_differentiable_at_Ln complex_differentiable_within_subset by blast
 
-lemma continuous_at_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) Ln"
+lemma continuous_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) Ln"
   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_Ln)
 
 lemma isCont_Ln' [simp]:
-   "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
+   "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
   by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
 
-lemma continuous_within_Ln: "(Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) Ln"
+lemma continuous_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) Ln"
   using continuous_at_Ln continuous_at_imp_continuous_within by blast
 
-lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s Ln"
+lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s Ln"
   by (simp add: continuous_at_imp_continuous_on continuous_within_Ln)
 
-lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> Im(z) = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> Ln holomorphic_on s"
+lemma holomorphic_on_Ln: "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> Ln holomorphic_on s"
   by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
 
 
@@ -1161,31 +1161,33 @@
 lemma Im_Ln_pos_lt_imp: "0 < Im(z) \<Longrightarrow> 0 < Im(Ln z) \<and> Im(Ln z) < pi"
   by (metis Im_Ln_pos_lt not_le order_refl zero_complex.simps(2))
 
+text\<open>A reference to the set of positive real numbers\<close>
 lemma Im_Ln_eq_0: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = 0 \<longleftrightarrow> 0 < Re(z) \<and> Im(z) = 0)"
-  by (metis exp_Ln Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt Re_complex_of_real add.commute add.left_neutral
-       complex_eq exp_of_real le_less mult_zero_right norm_exp_eq_Re norm_le_zero_iff not_le of_real_0)
+by (metis Im_complex_of_real Im_exp Ln_in_Reals Re_Ln_pos_lt Re_Ln_pos_lt_imp 
+          Re_complex_of_real complex_is_Real_iff exp_Ln exp_of_real pi_gt_zero)
 
 lemma Im_Ln_eq_pi: "z \<noteq> 0 \<Longrightarrow> (Im(Ln z) = pi \<longleftrightarrow> Re(z) < 0 \<and> Im(z) = 0)"
-  by (metis Im_Ln_eq_0 Im_Ln_less_pi Im_Ln_pos_le Im_Ln_pos_lt add.right_neutral complex_eq mult_zero_right not_less not_less_iff_gr_or_eq of_real_0)
+by (metis Im_Ln_eq_0 Im_Ln_pos_le Im_Ln_pos_lt add.left_neutral complex_eq less_eq_real_def 
+    mult_zero_right not_less_iff_gr_or_eq pi_ge_zero pi_neq_zero rcis_zero_arg rcis_zero_mod)
 
 
 subsection\<open>More Properties of Ln\<close>
 
-lemma cnj_Ln: "(Im z = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
+lemma cnj_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> cnj(Ln z) = Ln(cnj z)"
   apply (cases "z=0", auto)
   apply (rule exp_complex_eqI)
   apply (auto simp: abs_if split: split_if_asm)
-  apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps mult_2 neg_equal_0_iff_equal)
-  apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff mpi_less_Im_Ln mult.commute mult_2_right)
+  using Im_Ln_less_pi Im_Ln_le_pi apply force
+  apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff 
+          mpi_less_Im_Ln mult.commute mult_2_right)
   by (metis exp_Ln exp_cnj)
 
-lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
+lemma Ln_inverse: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln(inverse z) = -(Ln z)"
   apply (cases "z=0", auto)
   apply (rule exp_complex_eqI)
   using mpi_less_Im_Ln [of z] mpi_less_Im_Ln [of "inverse z"]
   apply (auto simp: abs_if exp_minus split: split_if_asm)
-  apply (metis Im_Ln_less_pi Im_Ln_pos_le add_less_cancel_left add_strict_mono
-               inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
+  apply (metis Im_Ln_less_pi Im_Ln_le_pi add.commute add_mono_thms_linordered_field(3) inverse_nonzero_iff_nonzero mult_2)
   done
 
 lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
@@ -1201,12 +1203,9 @@
 
 lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)"
 proof -
-  have  "Ln(-ii) = Ln(1/ii)"
-    by simp
-  also have "... = - (Ln ii)"
-    by (metis Ln_inverse ii.sel(2) inverse_eq_divide zero_neq_one)
-  also have "... = - (ii * pi/2)"
-    by simp
+  have  "Ln(-ii) = Ln(inverse ii)"    by simp
+  also have "... = - (Ln ii)"         using Ln_inverse by blast
+  also have "... = - (ii * pi/2)"     by simp
   finally show ?thesis .
 qed
 
@@ -1220,7 +1219,7 @@
                 else Ln(w) + Ln(z))"
   using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z]
   using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z]
-  by (auto simp: of_real_numeral exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
+  by (auto simp: exp_add exp_diff sin_double cos_double exp_Euler intro!: Ln_unique)
 
 corollary Ln_times_simple:
     "\<lbrakk>w \<noteq> 0; z \<noteq> 0; -pi < Im(Ln w) + Im(Ln z); Im(Ln w) + Im(Ln z) \<le> pi\<rbrakk>
@@ -1245,23 +1244,20 @@
                      else Ln(z) - ii * pi)" (is "_ = ?rhs")
   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z]
-    by (auto simp: of_real_numeral exp_add exp_diff exp_Euler intro!: Ln_unique)
+    by (fastforce simp: exp_add exp_diff exp_Euler intro!: Ln_unique)
 
 lemma Ln_inverse_if:
   assumes "z \<noteq> 0"
-    shows "Ln (inverse z) =
-            (if (Im(z) = 0 \<longrightarrow> 0 < Re z)
-             then -(Ln z)
-             else -(Ln z) + \<i> * 2 * complex_of_real pi)"
-proof (cases "(Im(z) = 0 \<longrightarrow> 0 < Re z)")
-  case True then show ?thesis
+    shows "Ln (inverse z) = (if z \<in> \<real>\<^sub>\<le>\<^sub>0 then -(Ln z) + \<i> * 2 * complex_of_real pi else -(Ln z))"
+proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
+  case False then show ?thesis
     by (simp add: Ln_inverse)
 next
-  case False
+  case True
   then have z: "Im z = 0" "Re z < 0"
     using assms
-    apply auto
-    by (metis cnj.code complex_cnj_cnj not_less_iff_gr_or_eq zero_complex.simps(1) zero_complex.simps(2))
+    apply (auto simp: complex_nonpos_Reals_iff)
+    by (metis complex_is_Real_iff le_imp_less_or_eq of_real_0 of_real_Re)
   have "Ln(inverse z) = Ln(- (inverse (-z)))"
     by simp
   also have "... = Ln (inverse (-z)) + \<i> * complex_of_real pi"
@@ -1271,15 +1267,13 @@
     done
   also have "... = - Ln (- z) + \<i> * complex_of_real pi"
     apply (subst Ln_inverse)
-    using z assms by auto
+    using z by (auto simp add: complex_nonneg_Reals_iff) 
   also have "... = - (Ln z) + \<i> * 2 * complex_of_real pi"
     apply (subst Ln_minus [OF assms])
     using assms z
     apply simp
     done
-  finally show ?thesis
-    using assms z
-    by simp
+  finally show ?thesis by (simp add: True)
 qed
 
 lemma Ln_times_ii:
@@ -1289,7 +1283,7 @@
                           else Ln(z) - ii * of_real(3 * pi/2))"
   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
-  by (auto simp: of_real_numeral Ln_times)
+  by (auto simp: Ln_times)
 
 lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
   by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
@@ -1338,17 +1332,23 @@
 qed
 
 lemma continuous_at_Arg:
-  assumes "z \<in> \<real> \<Longrightarrow> Re z < 0"
+  assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0"
     shows "continuous (at z) Arg"
 proof -
   have *: "isCont (\<lambda>z. Im (Ln (- z)) + pi) z"
     by (rule Complex.isCont_Im isCont_Ln' continuous_intros | simp add: assms complex_is_Real_iff)+
-  then show ?thesis
-    apply (simp add: continuous_at)
-    apply (rule Lim_transform_within_open [where s= "-{z. z \<in> \<real> & 0 \<le> Re z}" and f = "\<lambda>z. Im(Ln(-z)) + pi"])
-    apply (simp_all add: assms not_le Arg_Ln [OF Arg_gt_0])
-    apply (simp add: closed_def [symmetric] closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge)
-    done
+  have [simp]: "\<And>x. \<lbrakk>Im x \<noteq> 0\<rbrakk> \<Longrightarrow> Im (Ln (- x)) + pi = Arg x"
+      using Arg_Ln Arg_gt_0 complex_is_Real_iff by auto
+  consider "Re z < 0" | "Im z \<noteq> 0" using assms
+    using complex_nonneg_Reals_iff not_le by blast 
+  then have [simp]: "(\<lambda>z. Im (Ln (- z)) + pi) \<midarrow>z\<rightarrow> Arg z"
+      using "*"  by (simp add: isCont_def) (metis Arg_Ln Arg_gt_0 complex_is_Real_iff)
+  show ?thesis
+      apply (simp add: continuous_at)
+      apply (rule Lim_transform_within_open [where s= "-\<real>\<^sub>\<ge>\<^sub>0" and f = "\<lambda>z. Im(Ln(-z)) + pi"])
+      apply (auto simp add: not_le Arg_Ln [OF Arg_gt_0] complex_nonneg_Reals_iff closed_def [symmetric])
+      using assms apply (force simp add: complex_nonneg_Reals_iff)
+      done
 qed
 
 lemma Ln_series:
@@ -1372,7 +1372,7 @@
     have "Re (-z) \<le> norm (-z)" by (rule complex_Re_le_cmod)
     also from z have "... < 1" by simp
     finally have "((\<lambda>z. ln (1 + z)) has_field_derivative inverse (1+z)) (at z)"
-      by (auto intro!: derivative_eq_intros)
+      by (auto intro!: derivative_eq_intros simp: complex_nonpos_Reals_iff)
     moreover have "(?F has_field_derivative ?F' z) (at z)" using t r
       by (intro termdiffs_strong[of _ t] summable_in_conv_radius) simp_all
     ultimately have "((\<lambda>z. ln (1 + z) - ?F z) has_field_derivative (inverse (1 + z) - ?F' z)) 
@@ -1447,7 +1447,7 @@
     using False assms arctan [of "Re z / Im z"] pi_ge_two pi_half_less_two
     apply (auto simp: exp_Euler cos_diff sin_diff)
     using norm_complex_def [of z, symmetric]
-    apply (simp add: of_real_numeral sin_of_real cos_of_real sin_arctan cos_arctan field_simps real_sqrt_divide)
+    apply (simp add: sin_of_real cos_of_real sin_arctan cos_arctan field_simps real_sqrt_divide)
     apply (metis complex_eq mult.assoc ring_class.ring_distribs(2))
     done
 qed
@@ -1472,13 +1472,13 @@
 lemma continuous_within_upperhalf_Arg:
   assumes "z \<noteq> 0"
     shows "continuous (at z within {z. 0 \<le> Im z}) Arg"
-proof (cases "z \<in> \<real> & 0 \<le> Re z")
+proof (cases "z \<in> \<real>\<^sub>\<ge>\<^sub>0")
   case False then show ?thesis
     using continuous_at_Arg continuous_at_imp_continuous_within by auto
 next
   case True
   then have z: "z \<in> \<real>" "0 < Re z"
-    using assms  by (auto simp: complex_is_Real_iff complex_neq_0)
+    using assms  by (auto simp: complex_nonneg_Reals_iff complex_is_Real_iff complex_neq_0)
   then have [simp]: "Arg z = 0" "Im (Ln z) = 0"
     by (auto simp: Arg_eq_0 Im_Ln_eq_0 assms complex_is_Real_iff)
   show ?thesis
@@ -1486,7 +1486,7 @@
     fix e::real
     assume "0 < e"
     moreover have "continuous (at z) (\<lambda>x. Im (Ln x))"
-      using z  by (rule continuous_intros | simp)
+      using z by (simp add: continuous_at_Ln complex_nonpos_Reals_iff)
     ultimately
     obtain d where d: "d>0" "\<And>x. x \<noteq> z \<Longrightarrow> cmod (x - z) < d \<Longrightarrow> \<bar>Im (Ln x)\<bar> < e"
       by (auto simp: continuous_within Lim_within dist_norm)
@@ -1513,17 +1513,15 @@
   assumes "0 \<le> s" "t \<le> 2*pi"
     shows "open ({y. s < Arg y} \<inter> {y. Arg y < t})"
 proof -
-  have 1: "continuous_on (UNIV - {z \<in> \<real>. 0 \<le> Re z}) Arg"
+  have 1: "continuous_on (UNIV - \<real>\<^sub>\<ge>\<^sub>0) Arg"
     using continuous_at_Arg continuous_at_imp_continuous_within
-    by (auto simp: continuous_on_eq_continuous_within set_diff_eq)
-  have 2: "open (UNIV - {z \<in> \<real>. 0 \<le> Re z})"
-    by (simp add: closed_Collect_conj closed_complex_Reals closed_halfspace_Re_ge open_Diff)
+    by (auto simp: continuous_on_eq_continuous_within)
+  have 2: "open (UNIV - \<real>\<^sub>\<ge>\<^sub>0 :: complex set)"  by (simp add: open_Diff)
   have "open ({z. s < z} \<inter> {z. z < t})"
     using open_lessThan [of t] open_greaterThan [of s]
     by (metis greaterThan_def lessThan_def open_Int)
-  moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - {z \<in> \<real>. 0 \<le> Re z}"
-    using assms
-    by (auto simp: Arg_real)
+  moreover have "{y. s < Arg y} \<inter> {y. Arg y < t} \<subseteq> - \<real>\<^sub>\<ge>\<^sub>0"
+    using assms by (auto simp: Arg_real complex_nonneg_Reals_iff complex_is_Real_iff)
   ultimately show ?thesis
     using continuous_imp_open_vimage [OF 1 2, of  "{z. Re z > s} \<inter> {z. Re z < t}"]
     by auto
@@ -1576,7 +1574,7 @@
   shows   "cnj (a powr b) = cnj a powr cnj b"
 proof (cases "a = 0")
   case False
-  with assms have "Im a = 0 \<Longrightarrow> Re a > 0" by (auto simp: complex_eq_iff)
+  with assms have "a \<notin> \<real>\<^sub>\<le>\<^sub>0" by (auto simp: complex_eq_iff complex_nonpos_Reals_iff)
   with False show ?thesis by (simp add: powr_def exp_cnj cnj_Ln)
 qed simp
 
@@ -1615,8 +1613,8 @@
 qed simp_all
 
 lemma has_field_derivative_powr:
-    "(Im z = 0 \<Longrightarrow> 0 < Re z)
-     \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
+  fixes z :: complex
+  shows "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
   apply (cases "z=0", auto)
   apply (simp add: powr_def)
   apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
@@ -1625,23 +1623,7 @@
   apply (simp add: field_simps exp_diff)
   done
 
-lemma has_field_derivative_powr_complex':
-  assumes "Im z \<noteq> 0 \<or> Re z > 0"
-  shows "((\<lambda>z. z powr r :: complex) has_field_derivative r * z powr (r - 1)) (at z)"
-proof (subst DERIV_cong_ev[OF refl _ refl])
-  from assms have "eventually (\<lambda>z. z \<noteq> 0) (nhds z)" by (intro t1_space_nhds) auto
-  thus "eventually (\<lambda>z. z powr r = exp (r * Ln z)) (nhds z)"
-    unfolding powr_def by eventually_elim simp
-
-  have "((\<lambda>z. exp (r * Ln z)) has_field_derivative exp (r * Ln z) * (inverse z * r)) (at z)"
-    using assms by (auto intro!: derivative_eq_intros has_field_derivative_powr)
-  also have "exp (r * Ln z) * (inverse z * r) = r * z powr (r - 1)"
-    unfolding powr_def by (simp add: assms exp_diff field_simps)
-  finally show "((\<lambda>z. exp (r * Ln z)) has_field_derivative r * z powr (r - 1)) (at z)"
-    by simp
-qed
-
-declare has_field_derivative_powr_complex'[THEN DERIV_chain2, derivative_intros]
+declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
 
 
 lemma has_field_derivative_powr_right:
@@ -1815,71 +1797,72 @@
 qed
 
 lemma csqrt_inverse:
-  assumes "Im(z) = 0 \<Longrightarrow> 0 < Re z"
+  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
     shows "csqrt (inverse z) = inverse (csqrt z)"
 proof (cases "z=0", simp)
-  assume "z \<noteq> 0 "
+  assume "z \<noteq> 0"
   then show ?thesis
-    using assms
+    using assms csqrt_exp_Ln Ln_inverse exp_minus
     by (simp add: csqrt_exp_Ln Ln_inverse exp_minus)
 qed
 
 lemma cnj_csqrt:
-  assumes "Im z = 0 \<Longrightarrow> 0 \<le> Re(z)"
+  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
     shows "cnj(csqrt z) = csqrt(cnj z)"
 proof (cases "z=0", simp)
-  assume z: "z \<noteq> 0"
-  then have "Im z = 0 \<Longrightarrow> 0 < Re(z)"
-    using assms cnj.code complex_cnj_zero_iff by fastforce
+  assume "z \<noteq> 0"
   then show ?thesis
-   using z by (simp add: csqrt_exp_Ln cnj_Ln exp_cnj)
+     by (simp add: assms cnj_Ln csqrt_exp_Ln exp_cnj) 
 qed
 
 lemma has_field_derivative_csqrt:
-  assumes "Im z = 0 \<Longrightarrow> 0 < Re(z)"
+  assumes "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
     shows "(csqrt has_field_derivative inverse(2 * csqrt z)) (at z)"
 proof -
   have z: "z \<noteq> 0"
     using assms by auto
   then have *: "inverse z = inverse (2*z) * 2"
     by (simp add: divide_simps)
-  show ?thesis
-    apply (rule DERIV_transform_at [where f = "\<lambda>z. exp(Ln(z) / 2)" and d = "norm z"])
-    apply (intro derivative_eq_intros | simp add: assms)+
-    apply (rule *)
+  have [simp]: "exp (Ln z / 2) * inverse z = inverse (csqrt z)"
+    by (simp add: z field_simps csqrt_exp_Ln [symmetric]) (metis power2_csqrt power2_eq_square)
+  have "Im z = 0 \<Longrightarrow> 0 < Re z"
+    using assms complex_nonpos_Reals_iff not_less by blast
+  with z have "((\<lambda>z. exp (Ln z / 2)) has_field_derivative inverse (2 * csqrt z)) (at z)"
+    by (force intro: derivative_eq_intros * simp add: assms)
+  then show ?thesis
+    apply (rule DERIV_transform_at[where d = "norm z"])
+    apply (intro z derivative_eq_intros | simp add: assms)+
     using z
-    apply (auto simp: field_simps csqrt_exp_Ln [symmetric])
-    apply (metis power2_csqrt power2_eq_square)
     apply (metis csqrt_exp_Ln dist_0_norm less_irrefl)
     done
 qed
 
 lemma complex_differentiable_at_csqrt:
-    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable at z"
+    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt complex_differentiable at z"
   using complex_differentiable_def has_field_derivative_csqrt by blast
 
 lemma complex_differentiable_within_csqrt:
-    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt complex_differentiable (at z within s)"
+    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt complex_differentiable (at z within s)"
   using complex_differentiable_at_csqrt complex_differentiable_within_subset by blast
 
 lemma continuous_at_csqrt:
-    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z) csqrt"
+    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) csqrt"
   by (simp add: complex_differentiable_within_csqrt complex_differentiable_imp_continuous_at)
 
 corollary isCont_csqrt' [simp]:
-   "\<lbrakk>isCont f z; Im(f z) = 0 \<Longrightarrow> 0 < Re(f z)\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
+   "\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. csqrt (f x)) z"
   by (blast intro: isCont_o2 [OF _ continuous_at_csqrt])
 
 lemma continuous_within_csqrt:
-    "(Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous (at z within s) csqrt"
+    "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within s) csqrt"
   by (simp add: complex_differentiable_imp_continuous_at complex_differentiable_within_csqrt)
 
 lemma continuous_on_csqrt [continuous_intros]:
-    "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> continuous_on s csqrt"
+    "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on s csqrt"
   by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
 
 lemma holomorphic_on_csqrt:
-    "(\<And>z. z \<in> s \<and> Im z = 0 \<Longrightarrow> 0 < Re(z)) \<Longrightarrow> csqrt holomorphic_on s"
+    "(\<And>z. z \<in> s \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> csqrt holomorphic_on s"
   by (simp add: complex_differentiable_within_csqrt holomorphic_on_def)
 
 lemma continuous_within_closed_nontrivial:
@@ -1889,24 +1872,24 @@
 
 lemma continuous_within_csqrt_posreal:
     "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
-proof (cases "Im z = 0 --> 0 < Re(z)")
-  case True then show ?thesis
-    by (blast intro: continuous_within_csqrt)
-next
-  case False
+proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
+  case True 
   then have "Im z = 0" "Re z < 0 \<or> z = 0"
-    using False cnj.code complex_cnj_zero_iff by auto force
+    using cnj.code complex_cnj_zero_iff  by (auto simp: complex_nonpos_Reals_iff) fastforce
   then show ?thesis
     apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
     apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
     apply (rule_tac x="e^2" in exI)
     apply (auto simp: Reals_def)
-by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
+    by (metis linear not_less real_sqrt_less_iff real_sqrt_pow2_iff real_sqrt_power)
+next
+  case False
+    then show ?thesis   by (blast intro: continuous_within_csqrt)
 qed
 
 subsection\<open>Complex arctangent\<close>
 
-text\<open>branch cut gives standard bounds in real case.\<close>
+text\<open>The branch cut gives standard bounds in the real case.\<close>
 
 definition Arctan :: "complex \<Rightarrow> complex" where
     "Arctan \<equiv> \<lambda>z. (\<i>/2) * Ln((1 - \<i>*z) / (1 + \<i>*z))"
@@ -2005,16 +1988,19 @@
               less_irrefl mult_zero_right zero_complex.simps(1) zero_complex.simps(2))
   have nzi: "((1 - \<i>*z) * inverse (1 + \<i>*z)) \<noteq> 0"
     using nz1 nz2 by auto
-  have *: "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))"
+  have "Im ((1 - \<i>*z) / (1 + \<i>*z)) = 0 \<Longrightarrow> 0 < Re ((1 - \<i>*z) / (1 + \<i>*z))"
     apply (simp add: divide_complex_def)
     apply (simp add: divide_simps split: split_if_asm)
     using assms
     apply (auto simp: algebra_simps abs_square_less_1 [unfolded power2_eq_square])
     done
+  then have *: "((1 - \<i>*z) / (1 + \<i>*z)) \<notin> \<real>\<^sub>\<le>\<^sub>0"
+    by (auto simp add: complex_nonpos_Reals_iff)
   show "\<bar>Re(Arctan z)\<bar> < pi/2"
     unfolding Arctan_def divide_complex_def
     using mpi_less_Im_Ln [OF nzi]
-    by (auto simp: abs_if intro: Im_Ln_less_pi * [unfolded divide_complex_def])
+    apply (auto simp: abs_if intro!: Im_Ln_less_pi * [unfolded divide_complex_def])
+    done
   show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
     unfolding Arctan_def scaleR_conv_of_real
     apply (rule DERIV_cong)
@@ -2178,7 +2164,7 @@
   show "- (pi / 2) < Re (Arctan (complex_of_real x))"
     apply (simp add: Arctan_def)
     apply (rule Im_Ln_less_pi)
-    apply (auto simp: Im_complex_div_lemma)
+    apply (auto simp: Im_complex_div_lemma complex_nonpos_Reals_iff)
     done
 next
   have *: " (1 - \<i>*x) / (1 + \<i>*x) \<noteq> 0"
@@ -2312,24 +2298,54 @@
 lemma Im_Arcsin: "Im(Arcsin z) = - ln (cmod (\<i> * z + csqrt (1 - z\<^sup>2)))"
   by (simp add: Arcsin_def Arcsin_body_lemma)
 
+lemma one_minus_z2_notin_nonpos_Reals:
+  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+  shows "1 - z\<^sup>2 \<notin> \<real>\<^sub>\<le>\<^sub>0"
+    using assms  
+    apply (auto simp: complex_nonpos_Reals_iff Re_power2 Im_power2)
+    using power2_less_0 [of "Im z"] apply force
+    using abs_square_less_1 not_le by blast
+
+lemma isCont_Arcsin_lemma:
+  assumes le0: "Re (\<i> * z + csqrt (1 - z\<^sup>2)) \<le> 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
+    shows False
+proof (cases "Im z = 0")
+  case True
+  then show ?thesis
+    using assms by (fastforce simp: cmod_def abs_square_less_1 [symmetric])
+next
+  case False
+  have neq: "(cmod z)\<^sup>2 \<noteq> 1 + cmod (1 - z\<^sup>2)"
+  proof (clarsimp simp add: cmod_def)
+    assume "(Re z)\<^sup>2 + (Im z)\<^sup>2 = 1 + sqrt ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
+    then have "((Re z)\<^sup>2 + (Im z)\<^sup>2 - 1)\<^sup>2 = ((1 - Re (z\<^sup>2))\<^sup>2 + (Im (z\<^sup>2))\<^sup>2)"
+      by simp
+    then show False using False
+      by (simp add: power2_eq_square algebra_simps)
+  qed
+  moreover have 2: "(Im z)\<^sup>2 = (1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2"
+    using le0
+    apply simp
+    apply (drule sqrt_le_D)
+    using cmod_power2 [of z] norm_triangle_ineq2 [of "z^2" 1]
+    apply (simp add: norm_power Re_power2 norm_minus_commute [of 1])
+    done
+  ultimately show False
+    by (simp add: Re_power2 Im_power2 cmod_power2)
+qed
+
 lemma isCont_Arcsin:
   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
     shows "isCont Arcsin z"
 proof -
-  have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 0 < Re (1 - z\<^sup>2)"
-    using assms
-    by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps)
-  have cmz: "(cmod z)\<^sup>2 < 1 + cmod (1 - z\<^sup>2)"
-    by (blast intro: assms cmod_square_less_1_plus)
+  have *: "\<i> * z + csqrt (1 - z\<^sup>2) \<notin> \<real>\<^sub>\<le>\<^sub>0"
+    by (metis isCont_Arcsin_lemma assms complex_nonpos_Reals_iff)
   show ?thesis
     using assms
     apply (simp add: Arcsin_def)
     apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
-    apply (erule rez)
-    apply (auto simp: Re_power2 Im_power2 abs_square_less_1 [symmetric] real_less_rsqrt algebra_simps split: split_if_asm)
-    apply (simp add: norm_complex_def)
-    using cmod_power2 [of z, symmetric] cmz
-    apply (simp add: real_less_rsqrt)
+    apply (simp add: one_minus_z2_notin_nonpos_Reals assms)
+    apply (rule *)
     done
 qed
 
@@ -2464,18 +2480,17 @@
   by (simp add: Arccos_def Arccos_body_lemma)
 
 text\<open>A very tricky argument to find!\<close>
-lemma abs_Re_less_1_preserve:
-  assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"  "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0"
-    shows "0 < Re (z + \<i> * csqrt (1 - z\<^sup>2))"
+lemma isCont_Arccos_lemma:
+  assumes eq0: "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0" and "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)" 
+    shows False
 proof (cases "Im z = 0")
   case True
   then show ?thesis
-    using assms
-    by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric])
+    using assms by (fastforce simp add: cmod_def abs_square_less_1 [symmetric])
 next
   case False
   have Imz: "Im z = - sqrt ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
-    using assms abs_Re_le_cmod [of "1-z\<^sup>2"]
+    using eq0 abs_Re_le_cmod [of "1-z\<^sup>2"]
     by (simp add: Re_power2 algebra_simps)
   have "(cmod z)\<^sup>2 - 1 \<noteq> cmod (1 - z\<^sup>2)"
   proof (clarsimp simp add: cmod_def)
@@ -2486,28 +2501,24 @@
       by (simp add: power2_eq_square algebra_simps)
   qed
   moreover have "(Im z)\<^sup>2 = ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
-    apply (subst Imz, simp)
-    apply (subst real_sqrt_pow2)
+    apply (subst Imz)
     using abs_Re_le_cmod [of "1-z\<^sup>2"]
-    apply (auto simp: Re_power2 field_simps)
+    apply (simp add: Re_power2)
     done
-  ultimately show ?thesis
-    by (simp add: Re_power2 Im_power2 cmod_power2)
+  ultimately show False
+    by (simp add: cmod_power2)
 qed
 
 lemma isCont_Arccos:
   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"
     shows "isCont Arccos z"
 proof -
-  have rez: "Im (1 - z\<^sup>2) = 0 \<Longrightarrow> 0 < Re (1 - z\<^sup>2)"
-    using assms
-    by (auto simp: Re_power2 Im_power2 abs_square_less_1 add_pos_nonneg algebra_simps)
-  show ?thesis
-    using assms
+  have "z + \<i> * csqrt (1 - z\<^sup>2) \<notin> \<real>\<^sub>\<le>\<^sub>0"
+    by (metis complex_nonpos_Reals_iff isCont_Arccos_lemma assms)
+  with assms show ?thesis
     apply (simp add: Arccos_def)
     apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+
-    apply (erule rez)
-    apply (blast intro: abs_Re_less_1_preserve)
+    apply (simp_all add: one_minus_z2_notin_nonpos_Reals assms)
     done
 qed
 

--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -1346,6 +1346,19 @@
 corollary connected_UNIV[intro]: "connected (UNIV :: 'a::real_normed_vector set)"
   by(simp add: convex_connected)
 
+proposition clopen:
+  fixes s :: "'a :: real_normed_vector set"
+  shows "closed s \<and> open s \<longleftrightarrow> s = {} \<or> s = UNIV"
+apply (rule iffI)
+ apply (rule connected_UNIV [unfolded connected_clopen, rule_format])
+ apply (force simp add: open_openin closed_closedin, force)
+done
+
+corollary compact_open:
+  fixes s :: "'a :: euclidean_space set"
+  shows "compact s \<and> open s \<longleftrightarrow> s = {}"
+  by (auto simp: compact_eq_bounded_closed clopen)
+
 text \<open>Balls, being convex, are connected.\<close>
 
 lemma convex_prod:

--- a/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -5,7 +5,7 @@
 section \<open>The Gamma Function\<close>
 
 theory Gamma
-imports 
+imports
   Complex_Transcendental
   Summation
   Harmonic_Numbers
@@ -14,22 +14,22 @@
 begin
 
 text \<open>
-  Several equivalent definitions of the Gamma function and its 
+  Several equivalent definitions of the Gamma function and its
   most important properties. Also contains the definition and some properties
   of the log-Gamma function and the Digamma function and the other Polygamma functions.
-  
+
   Based on the Gamma function, we also prove the Weierstraß product form of the
-  sin function and, based on this, the solution of the Basel problem (the 
+  sin function and, based on this, the solution of the Basel problem (the
   sum over all @{term "1 / (n::nat)^2"}.
-\<close>  
+\<close>
 
-lemma pochhammer_eq_0_imp_nonpos_Int: 
+lemma pochhammer_eq_0_imp_nonpos_Int:
   "pochhammer (x::'a::field_char_0) n = 0 \<Longrightarrow> x \<in> \<int>\<^sub>\<le>\<^sub>0"
   by (auto simp: pochhammer_eq_0_iff)
-  
+
 lemma closed_nonpos_Ints [simp]: "closed (\<int>\<^sub>\<le>\<^sub>0 :: 'a :: real_normed_algebra_1 set)"
 proof -
-  have "\<int>\<^sub>\<le>\<^sub>0 = (of_int ` {n. n \<le> 0} :: 'a set)" 
+  have "\<int>\<^sub>\<le>\<^sub>0 = (of_int ` {n. n \<le> 0} :: 'a set)"
     by (auto elim!: nonpos_Ints_cases intro!: nonpos_Ints_of_int)
   also have "closed \<dots>" by (rule closed_of_int_image)
   finally show ?thesis .
@@ -65,7 +65,7 @@
 lemma sin_series: "(\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z"
 proof -
   from sin_converges[of z] have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z" .
-  also have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z \<longleftrightarrow> 
+  also have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z \<longleftrightarrow>
                  (\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z"
     by (subst sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
        (auto simp: sin_coeff_def subseq_def ac_simps elim!: oddE)
@@ -75,7 +75,7 @@
 lemma cos_series: "(\<lambda>n. ((-1)^n / fact (2*n)) *\<^sub>R z^(2*n)) sums cos z"
 proof -
   from cos_converges[of z] have "(\<lambda>n. cos_coeff n *\<^sub>R z^n) sums cos z" .
-  also have "(\<lambda>n. cos_coeff n *\<^sub>R z^n) sums cos z \<longleftrightarrow> 
+  also have "(\<lambda>n. cos_coeff n *\<^sub>R z^n) sums cos z \<longleftrightarrow>
                  (\<lambda>n. ((-1)^n / fact (2*n)) *\<^sub>R z^(2*n)) sums cos z"
     by (subst sums_mono_reindex[of "\<lambda>n. 2*n", symmetric])
        (auto simp: cos_coeff_def subseq_def ac_simps elim!: evenE)
@@ -98,7 +98,7 @@
   assumes "z \<noteq> 0"
   shows   "(\<lambda>n. sin_coeff (n+1) *\<^sub>R z^n) sums (sin z / z)"
 proof -
-  from sums_split_initial_segment[OF sin_converges[of z], of 1] 
+  from sums_split_initial_segment[OF sin_converges[of z], of 1]
     have "(\<lambda>n. z * (sin_coeff (n+1) *\<^sub>R z ^ n)) sums sin z" by simp
   from sums_mult[OF this, of "inverse z"] assms show ?thesis by (simp add: field_simps)
 qed
@@ -108,7 +108,7 @@
   shows "((\<lambda>z. if z = 0 then 1 else sin z / z) has_field_derivative 0) (at 0 within A)"
       (is "(?f has_field_derivative ?f') _")
 proof (rule has_field_derivative_at_within)
-  have "((\<lambda>z::'a. \<Sum>n. of_real (sin_coeff (n+1)) * z^n) 
+  have "((\<lambda>z::'a. \<Sum>n. of_real (sin_coeff (n+1)) * z^n)
             has_field_derivative (\<Sum>n. diffs (\<lambda>n. of_real (sin_coeff (n+1))) n * 0^n)) (at 0)"
   proof (rule termdiffs_strong)
     from summable_ignore_initial_segment[OF sums_summable[OF sin_converges[of "1::'a"]], of 1]
@@ -118,19 +118,15 @@
   proof
     fix z
     show "(\<Sum>n. of_real (sin_coeff (n+1)) * z^n)  = ?f z"
-      by (cases "z = 0") (insert sin_z_over_z_series'[of z], 
+      by (cases "z = 0") (insert sin_z_over_z_series'[of z],
             simp_all add: scaleR_conv_of_real sums_iff powser_zero sin_coeff_def)
   qed
-  also have "(\<Sum>n. diffs (\<lambda>n. of_real (sin_coeff (n + 1))) n * (0::'a) ^ n) = 
+  also have "(\<Sum>n. diffs (\<lambda>n. of_real (sin_coeff (n + 1))) n * (0::'a) ^ n) =
                  diffs (\<lambda>n. of_real (sin_coeff (Suc n))) 0" by (simp add: powser_zero)
   also have "\<dots> = 0" by (simp add: sin_coeff_def diffs_def)
   finally show "((\<lambda>z::'a. if z = 0 then 1 else sin z / z) has_field_derivative 0) (at 0)" .
 qed
 
- 
-lemma tendsto_complex_of_real_iff: "((\<lambda>x. complex_of_real (f x)) \<longlongrightarrow> of_real c) F = (f \<longlongrightarrow> c) F"
-  by (rule tendsto_of_real_iff)
-
 lemma round_Re_minimises_norm:
   "norm ((z::complex) - of_int m) \<ge> norm (z - of_int (round (Re z)))"
 proof -
@@ -158,7 +154,7 @@
   shows   "t \<notin> \<int>\<^sub>\<le>\<^sub>0"
   using Re_pos_in_ball[OF assms] by (force elim!: nonpos_Ints_cases)
 
-lemma no_nonpos_Int_in_ball: 
+lemma no_nonpos_Int_in_ball:
   assumes "t \<in> ball z (dist z (round (Re z)))"
   shows   "t \<notin> \<int>\<^sub>\<le>\<^sub>0"
 proof
@@ -182,37 +178,37 @@
   thus "t \<notin> \<int>\<^sub>\<le>\<^sub>0" using setdist_le_dist[of z "{z}" t "\<int>\<^sub>\<le>\<^sub>0"] by force
 qed
 
-lemma Re_pos_or_Im_nz_in_ball:
-  assumes "Re z > 0 \<or> Im z \<noteq> 0" "t \<in> ball z (if Im z = 0 then Re z / 2 else abs (Im z) / 2)"
-  shows   "Re t > 0 \<or> Im t \<noteq> 0"
-using assms(1)
+lemma no_nonpos_Real_in_ball:
+  assumes z: "z \<notin> \<real>\<^sub>\<le>\<^sub>0" and t: "t \<in> ball z (if Im z = 0 then Re z / 2 else abs (Im z) / 2)"
+  shows   "t \<notin> \<real>\<^sub>\<le>\<^sub>0"
+using z
 proof (cases "Im z = 0")
   assume A: "Im z = 0"
-  with assms(1) have "Re z > 0" by blast
-  with assms(2) A Re_pos_in_ball[of z t] show ?thesis by simp
+  with z have "Re z > 0" by (force simp add: complex_nonpos_Reals_iff)
+  with t A Re_pos_in_ball[of z t] show ?thesis by (force simp add: complex_nonpos_Reals_iff)
 next
   assume A: "Im z \<noteq> 0"
   have "abs (Im z) - abs (Im t) \<le> abs (Im z - Im t)" by linarith
   also have "\<dots> = abs (Im (z - t))" by simp
   also have "\<dots> \<le> norm (z - t)" by (rule abs_Im_le_cmod)
-  also from A assms(2) have "\<dots> \<le> abs (Im z) / 2" by (simp add: dist_complex_def)
+  also from A t have "\<dots> \<le> abs (Im z) / 2" by (simp add: dist_complex_def)
   finally have "abs (Im t) > 0" using A by simp
-  thus ?thesis by force
+  thus ?thesis by (force simp add: complex_nonpos_Reals_iff)
 qed
 
 
 subsection \<open>Definitions\<close>
 
 text \<open>
-  We define the Gamma function by first defining its multiplicative inverse @{term "Gamma_inv"}. 
-  This is more convenient because @{term "Gamma_inv"} is entire, which makes proofs of its 
+  We define the Gamma function by first defining its multiplicative inverse @{term "Gamma_inv"}.
+  This is more convenient because @{term "Gamma_inv"} is entire, which makes proofs of its
   properties more convenient because one does not have to watch out for discontinuities.
   (e.g. @{term "Gamma_inv"} fulfils @{term "rGamma z = z * rGamma (z + 1)"} everywhere,
   whereas @{term "Gamma"} does not fulfil the analogous equation on the non-positive integers)
-  
-  We define the Gamma function (resp. its inverse) in the Euler form. This form has the advantage 
-  that it is a relatively simple limit that converges everywhere. The limit at the poles is 0 
-  (due to division by 0). The functional equation @{term "Gamma (z + 1) = z * Gamma z"} follows 
+
+  We define the Gamma function (resp. its inverse) in the Euler form. This form has the advantage
+  that it is a relatively simple limit that converges everywhere. The limit at the poles is 0
+  (due to division by 0). The functional equation @{term "Gamma (z + 1) = z * Gamma z"} follows
   immediately from the definition.
 \<close>
 
@@ -228,22 +224,22 @@
 lemma Gamma_series_altdef: "Gamma_series z n = inverse (rGamma_series z n)"
   and rGamma_series_altdef: "rGamma_series z n = inverse (Gamma_series z n)"
   unfolding Gamma_series_def rGamma_series_def by simp_all
-  
+
 lemma rGamma_series_minus_of_nat:
   "eventually (\<lambda>n. rGamma_series (- of_nat k) n = 0) sequentially"
   using eventually_ge_at_top[of k]
-  by eventually_elim (auto simp: rGamma_series_def pochhammer_of_nat_eq_0_iff)  
+  by eventually_elim (auto simp: rGamma_series_def pochhammer_of_nat_eq_0_iff)
 
 lemma Gamma_series_minus_of_nat:
   "eventually (\<lambda>n. Gamma_series (- of_nat k) n = 0) sequentially"
   using eventually_ge_at_top[of k]
-  by eventually_elim (auto simp: Gamma_series_def pochhammer_of_nat_eq_0_iff)  
+  by eventually_elim (auto simp: Gamma_series_def pochhammer_of_nat_eq_0_iff)
 
 lemma Gamma_series'_minus_of_nat:
   "eventually (\<lambda>n. Gamma_series' (- of_nat k) n = 0) sequentially"
   using eventually_gt_at_top[of k]
   by eventually_elim (auto simp: Gamma_series'_def pochhammer_of_nat_eq_0_iff)
-  
+
 lemma rGamma_series_nonpos_Ints_LIMSEQ: "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma_series z \<longlonglongrightarrow> 0"
   by (elim nonpos_Ints_cases', hypsubst, subst tendsto_cong, rule rGamma_series_minus_of_nat, simp)
 
@@ -252,8 +248,8 @@
 
 lemma Gamma_series'_nonpos_Ints_LIMSEQ: "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Gamma_series' z \<longlonglongrightarrow> 0"
   by (elim nonpos_Ints_cases', hypsubst, subst tendsto_cong, rule Gamma_series'_minus_of_nat, simp)
-  
-lemma Gamma_series_Gamma_series': 
+
+lemma Gamma_series_Gamma_series':
   assumes z: "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "(\<lambda>n. Gamma_series' z n / Gamma_series z n) \<longlonglongrightarrow> 1"
 proof (rule Lim_transform_eventually)
@@ -270,7 +266,7 @@
   qed
   have "(\<lambda>x. z / of_nat x) \<longlonglongrightarrow> 0"
     by (rule tendsto_norm_zero_cancel)
-       (insert tendsto_mult[OF tendsto_const[of "norm z"] lim_inverse_n], 
+       (insert tendsto_mult[OF tendsto_const[of "norm z"] lim_inverse_n],
         simp add:  norm_divide inverse_eq_divide)
   from tendsto_add[OF this tendsto_const[of 1]] show "(\<lambda>n. z / of_nat n + 1) \<longlonglongrightarrow> 1" by simp
 qed
@@ -279,15 +275,15 @@
 subsection \<open>Convergence of the Euler series form\<close>
 
 text \<open>
-  We now show that the series that defines the Gamma function in the Euler form converges 
-  and that the function defined by it is continuous on the complex halfspace with positive 
+  We now show that the series that defines the Gamma function in the Euler form converges
+  and that the function defined by it is continuous on the complex halfspace with positive
   real part.
-  
-  We do this by showing that the logarithm of the Euler series is continuous and converges 
-  locally uniformly, which means that the log-Gamma function defined by its limit is also 
+
+  We do this by showing that the logarithm of the Euler series is continuous and converges
+  locally uniformly, which means that the log-Gamma function defined by its limit is also
   continuous.
-  
-  This will later allow us to lift holomorphicity and continuity from the log-Gamma 
+
+  This will later allow us to lift holomorphicity and continuity from the log-Gamma
   function to the inverse of the Gamma function, and from that to the Gamma function itself.
 \<close>
 
@@ -303,7 +299,7 @@
 
 
 text \<open>
-  We now show that the log-Gamma series converges locally uniformly for all complex numbers except 
+  We now show that the log-Gamma series converges locally uniformly for all complex numbers except
   the non-positive integers. We do this by proving that the series is locally Cauchy, adapting this
   proof:
   http://math.stackexchange.com/questions/887158/convergence-of-gammaz-lim-n-to-infty-fracnzn-prod-m-0nzm
@@ -324,7 +320,7 @@
     by (subst norm_mult [symmetric], rule norm_triangle_ineq)
   also have "norm (Ln (1 + -1/?k) - (-1/?k)) \<le> (norm (-1/?k))\<^sup>2 / (1 - norm(-1/?k))"
     using k by (intro Ln_approx_linear) (simp add: norm_divide)
-  hence "?z * norm (ln (1-1/?k) + 1/?k) \<le> ?z * ((norm (1/?k))^2 / (1 - norm (1/?k)))" 
+  hence "?z * norm (ln (1-1/?k) + 1/?k) \<le> ?z * ((norm (1/?k))^2 / (1 - norm (1/?k)))"
     by (intro mult_left_mono) simp_all
   also have "... \<le> (?z * (of_nat k / (of_nat k - 1))) / of_nat k^2" using k
     by (simp add: field_simps power2_eq_square norm_divide)
@@ -332,7 +328,7 @@
     by (intro divide_right_mono mult_left_mono) (simp_all add: field_simps)
   also have "norm (ln (1+z/?k) - z/?k) \<le> norm (z/?k)^2 / (1 - norm (z/?k))" using k
     by (intro Ln_approx_linear) (simp add: norm_divide)
-  hence "norm (ln (1+z/?k) - z/?k) \<le> ?z^2 / of_nat k^2 / (1 - ?z / of_nat k)" 
+  hence "norm (ln (1+z/?k) - z/?k) \<le> ?z^2 / of_nat k^2 / (1 - ?z / of_nat k)"
     by (simp add: field_simps norm_divide)
   also have "... \<le> (?z^2 * (of_nat k / (of_nat k - ?z))) / of_nat k^2" using k
     by (simp add: field_simps power2_eq_square)
@@ -359,7 +355,7 @@
     by (subst less_cSUP_iff) (auto intro!: add_pos_nonneg bexI[of _ z])
   have e'': "norm t + norm t^2 \<le> e''" if "t \<in> ball z d" for t unfolding e''_def using that
     by (rule cSUP_upper[OF _ bdd])
-  from e z e''_pos have e': "e' > 0" unfolding e'_def 
+  from e z e''_pos have e': "e' > 0" unfolding e'_def
     by (intro divide_pos_pos mult_pos_pos add_pos_pos) (simp_all add: field_simps)
 
   have "summable (\<lambda>k. inverse ((real_of_nat k)^2))"
@@ -368,11 +364,11 @@
 
   def N \<equiv> "max 2 (max (nat \<lceil>2 * (norm z + d)\<rceil>) M)"
   {
-    from d have "\<lceil>2 * (cmod z + d)\<rceil> \<ge> \<lceil>0::real\<rceil>" 
+    from d have "\<lceil>2 * (cmod z + d)\<rceil> \<ge> \<lceil>0::real\<rceil>"
       by (intro ceiling_mono mult_nonneg_nonneg add_nonneg_nonneg) simp_all
     hence "2 * (norm z + d) \<le> of_nat (nat \<lceil>2 * (norm z + d)\<rceil>)" unfolding N_def
       by (simp_all add: le_of_int_ceiling)
-    also have "... \<le> of_nat N" unfolding N_def 
+    also have "... \<le> of_nat N" unfolding N_def
       by (subst of_nat_le_iff) (rule max.coboundedI2, rule max.cobounded1)
     finally have "of_nat N \<ge> 2 * (norm z + d)" .
     moreover have "N \<ge> 2" "N \<ge> M" unfolding N_def by simp_all
@@ -397,7 +393,7 @@
     also have "N \<le> m" by (rule mn)
     finally have norm_t: "2 * norm t < of_nat m" by simp
 
-    have "ln_Gamma_series t m - ln_Gamma_series t n = 
+    have "ln_Gamma_series t m - ln_Gamma_series t n =
               (-(t * Ln (of_nat n)) - (-(t * Ln (of_nat m)))) +
               ((\<Sum>k=1..n. Ln (t / of_nat k + 1)) - (\<Sum>k=1..m. Ln (t / of_nat k + 1)))"
       by (simp add: ln_Gamma_series_def algebra_simps)
@@ -405,7 +401,7 @@
                  (\<Sum>k\<in>{1..n}-{1..m}. Ln (t / of_nat k + 1))" using mn
       by (simp add: setsum_diff)
     also from mn have "{1..n}-{1..m} = {Suc m..n}" by fastforce
-    also have "-(t * Ln (of_nat n)) - (-(t * Ln (of_nat m))) = 
+    also have "-(t * Ln (of_nat n)) - (-(t * Ln (of_nat m))) =
                    (\<Sum>k = Suc m..n. t * Ln (of_nat (k - 1)) - t * Ln (of_nat k))" using mn
       by (subst setsum_telescope'' [symmetric]) simp_all
     also have "... = (\<Sum>k = Suc m..n. t * Ln (of_nat (k - 1) / of_nat k))" using mn N
@@ -417,16 +413,16 @@
              (\<Sum>k = Suc m..n. t * Ln (1 - 1 / of_nat k))" using mn N
       by (intro setsum.cong) simp_all
     also note setsum.distrib [symmetric]
-    also have "norm (\<Sum>k=Suc m..n. t * Ln (1 - 1/of_nat k) + Ln (t/of_nat k + 1)) \<le> 
+    also have "norm (\<Sum>k=Suc m..n. t * Ln (1 - 1/of_nat k) + Ln (t/of_nat k + 1)) \<le>
       (\<Sum>k=Suc m..n. 2 * (norm t + (norm t)\<^sup>2) / (real_of_nat k)\<^sup>2)" using t_nz N(2) mn norm_t
       by (intro order.trans[OF norm_setsum setsum_mono[OF ln_Gamma_series_complex_converges_aux]]) simp_all
     also have "... \<le> 2 * (norm t + norm t^2) * (\<Sum>k=Suc m..n. 1 / (of_nat k)\<^sup>2)"
       by (simp add: setsum_right_distrib)
     also have "... < 2 * (norm t + norm t^2) * e'" using mn z t_nz
       by (intro mult_strict_left_mono N mult_pos_pos add_pos_pos) simp_all
-    also from e''_pos have "... = e * ((cmod t + (cmod t)\<^sup>2) / e'')" 
+    also from e''_pos have "... = e * ((cmod t + (cmod t)\<^sup>2) / e'')"
       by (simp add: e'_def field_simps power2_eq_square)
-    also from e''[OF t] e''_pos e 
+    also from e''[OF t] e''_pos e
       have "\<dots> \<le> e * 1" by (intro mult_left_mono) (simp_all add: field_simps)
     finally show "norm (ln_Gamma_series t m - ln_Gamma_series t n) < e" by simp
   qed
@@ -454,7 +450,7 @@
     finally show ?thesis .
   next
     case False
-    with assms nonpos_Ints_of_int[of "round (Re z)"] 
+    with assms nonpos_Ints_of_int[of "round (Re z)"]
       have "z \<noteq> of_int (round d')" by (auto simp: not_less)
     with False have "d < norm (z - of_int (round d'))" by (simp add: d_def d'_def)
     also have "\<dots> \<le> norm (z - of_int n)" unfolding d'_def by (rule round_Re_minimises_norm)
@@ -476,7 +472,7 @@
   shows   "exp (ln_Gamma_series z n :: complex) = Gamma_series z n"
 proof -
   from assms have "z \<noteq> 0" by (intro notI) auto
-  with assms have "exp (ln_Gamma_series z n) = 
+  with assms have "exp (ln_Gamma_series z n) =
           (of_nat n) powr z / (z * (\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))))"
     unfolding ln_Gamma_series_def powr_def by (simp add: exp_diff exp_setsum)
   also from assms have "(\<Prod>k=1..n. exp (Ln (z / of_nat k + 1))) = (\<Prod>k=1..n. z / of_nat k + 1)"
@@ -494,12 +490,12 @@
 
 lemma ln_Gamma_series'_aux:
   assumes "(z::complex) \<notin> \<int>\<^sub>\<le>\<^sub>0"
-  shows   "(\<lambda>k. z / of_nat (Suc k) - ln (1 + z / of_nat (Suc k))) sums 
+  shows   "(\<lambda>k. z / of_nat (Suc k) - ln (1 + z / of_nat (Suc k))) sums
               (ln_Gamma z + euler_mascheroni * z + ln z)" (is "?f sums ?s")
 unfolding sums_def
 proof (rule Lim_transform)
   show "(\<lambda>n. ln_Gamma_series z n + of_real (harm n - ln (of_nat n)) * z + ln z) \<longlonglongrightarrow> ?s"
-    (is "?g \<longlonglongrightarrow> _") 
+    (is "?g \<longlonglongrightarrow> _")
     by (intro tendsto_intros ln_Gamma_complex_LIMSEQ euler_mascheroni_LIMSEQ_of_real assms)
 
   have A: "eventually (\<lambda>n. (\<Sum>k<n. ?f k) - ?g n = 0) sequentially"
@@ -512,7 +508,7 @@
     also have "\<dots> = z * of_real (harm n) - (\<Sum>k=1..n. ln (1 + z / of_nat k))"
       by (simp add: harm_def setsum_subtractf setsum_right_distrib divide_inverse)
     also from n have "\<dots> - ?g n = 0"
-      by (simp add: ln_Gamma_series_def setsum_subtractf algebra_simps Ln_of_nat) 
+      by (simp add: ln_Gamma_series_def setsum_subtractf algebra_simps Ln_of_nat)
     finally show "(\<Sum>k<n. ?f k) - ?g n = 0" .
   qed
   show "(\<lambda>n. (\<Sum>k<n. ?f k) - ?g n) \<longlonglongrightarrow> 0" by (subst tendsto_cong[OF A]) simp_all
@@ -531,7 +527,7 @@
     have "norm (t + (z - t)) \<le> norm t + norm (z - t)" by (rule norm_triangle_ineq)
     also from t d have "norm (z - t) < norm z / 2" by (simp add: dist_norm)
     finally have A: "norm t > norm z / 2" using z by (simp add: field_simps)
-    
+
     have "norm t = norm (z + (t - z))" by simp
     also have "\<dots> \<le> norm z + norm (t - z)" by (rule norm_triangle_ineq)
     also from t d have "norm (t - z) \<le> norm z / 2" by (simp add: dist_norm norm_minus_commute)
@@ -559,16 +555,16 @@
     also {
       from z t_nz ball[OF t] have "of_nat (Suc n) / (4 * norm z) \<le> of_nat (Suc n) / (2 * norm t)"
         by (intro divide_left_mono mult_pos_pos) simp_all
-      also have "\<dots> < norm (of_nat (Suc n) / t) - norm (1 :: 'a)" 
+      also have "\<dots> < norm (of_nat (Suc n) / t) - norm (1 :: 'a)"
         using t_nz n by (simp add: field_simps norm_divide del: of_nat_Suc)
       also have "\<dots> \<le> norm (of_nat (Suc n)/t + 1)" by (rule norm_diff_ineq)
       finally have "inverse (norm (of_nat (Suc n)/t + 1)) \<le> 4 * norm z / of_nat (Suc n)"
         using z by (simp add: divide_simps norm_divide mult_ac del: of_nat_Suc)
     }
     also have "inverse (real_of_nat (Suc n)) * (4 * norm z / real_of_nat (Suc n)) =
-                 4 * norm z * inverse (of_nat (Suc n)^2)" 
+                 4 * norm z * inverse (of_nat (Suc n)^2)"
                  by (simp add: divide_simps power2_eq_square del: of_nat_Suc)
-    finally show "norm (?f n t) \<le> 4 * norm z * inverse (of_nat (Suc n)^2)" 
+    finally show "norm (?f n t) \<le> 4 * norm z * inverse (of_nat (Suc n)^2)"
       by (simp del: of_nat_Suc)
   qed
 next
@@ -577,31 +573,31 @@
 qed
 
 lemma summable_deriv_ln_Gamma:
-  "z \<noteq> (0 :: 'a :: {real_normed_field,banach}) \<Longrightarrow> 
+  "z \<noteq> (0 :: 'a :: {real_normed_field,banach}) \<Longrightarrow>
      summable (\<lambda>n. inverse (of_nat (Suc n)) - inverse (z + of_nat (Suc n)))"
   unfolding summable_iff_convergent
-  by (rule uniformly_convergent_imp_convergent, 
+  by (rule uniformly_convergent_imp_convergent,
       rule uniformly_summable_deriv_ln_Gamma[of z "norm z/2"]) simp_all
 
 
 definition Polygamma :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
-  "Polygamma n z = (if n = 0 then 
-      (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) - euler_mascheroni else 
+  "Polygamma n z = (if n = 0 then
+      (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) - euler_mascheroni else
       (-1)^Suc n * fact n * (\<Sum>k. inverse ((z + of_nat k)^Suc n)))"
 
 abbreviation Digamma :: "('a :: {real_normed_field,banach}) \<Rightarrow> 'a" where
   "Digamma \<equiv> Polygamma 0"
 
-lemma Digamma_def: 
+lemma Digamma_def:
   "Digamma z = (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) - euler_mascheroni"
   by (simp add: Polygamma_def)
 
 
-lemma summable_Digamma: 
+lemma summable_Digamma:
   assumes "(z :: 'a :: {real_normed_field,banach}) \<noteq> 0"
   shows   "summable (\<lambda>n. inverse (of_nat (Suc n)) - inverse (z + of_nat n))"
 proof -
-  have sums: "(\<lambda>n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n)) sums 
+  have sums: "(\<lambda>n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n)) sums
                        (0 - inverse (z + of_nat 0))"
     by (intro telescope_sums filterlim_compose[OF tendsto_inverse_0]
               tendsto_add_filterlim_at_infinity[OF tendsto_const] tendsto_of_nat)
@@ -614,13 +610,13 @@
   shows   "summable f"
 proof -
   from assms have "convergent (\<lambda>m. \<Sum>n<m. f (n + k))" by (simp add: summable_iff_convergent)
-  hence "convergent (\<lambda>m. (\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)))" 
+  hence "convergent (\<lambda>m. (\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)))"
     by (intro convergent_add convergent_const)
   also have "(\<lambda>m. (\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k))) = (\<lambda>m. \<Sum>n<m+k. f n)"
   proof
     fix m :: nat
     have "{..<m+k} = {..<k} \<union> {k..<m+k}" by auto
-    also have "(\<Sum>n\<in>\<dots>. f n) = (\<Sum>n<k. f n) + (\<Sum>n=k..<m+k. f n)" 
+    also have "(\<Sum>n\<in>\<dots>. f n) = (\<Sum>n<k. f n) + (\<Sum>n=k..<m+k. f n)"
       by (rule setsum.union_disjoint) auto
     also have "(\<Sum>n=k..<m+k. f n) = (\<Sum>n=0..<m+k-k. f (n + k))"
       by (intro setsum.reindex_cong[of "\<lambda>n. n + k"])
@@ -646,14 +642,14 @@
     also from t have "norm (t - z) < d" by (simp add: dist_norm norm_minus_commute)
     finally have "norm t < norm z * e" using z by (simp add: divide_simps e_def)
   } note ball = this
-  
-  show "eventually (\<lambda>k. \<forall>t\<in>ball z d. norm (inverse ((t + of_nat k)^n)) \<le> 
+
+  show "eventually (\<lambda>k. \<forall>t\<in>ball z d. norm (inverse ((t + of_nat k)^n)) \<le>
             inverse (of_nat (k - m)^n)) sequentially"
     using eventually_gt_at_top[of m] apply eventually_elim
   proof (intro ballI)
     fix k :: nat and t :: 'a assume k: "k > m" and t: "t \<in> ball z d"
     from k have "real_of_nat (k - m) = of_nat k - of_nat m" by (simp add: of_nat_diff)
-    also have "\<dots> \<le> norm (of_nat k :: 'a) - norm z * e" 
+    also have "\<dots> \<le> norm (of_nat k :: 'a) - norm z * e"
       unfolding m_def by (subst norm_of_nat) linarith
     also from ball[OF t] have "\<dots> \<le> norm (of_nat k :: 'a) - norm t" by simp
     also have "\<dots> \<le> norm (of_nat k + t)" by (rule norm_diff_ineq)
@@ -662,8 +658,8 @@
     thus "norm (inverse ((t + of_nat k)^n)) \<le> inverse (of_nat (k - m)^n)"
       by (simp add: norm_inverse norm_power power_inverse)
   qed
-  
-  have "summable (\<lambda>k. inverse ((real_of_nat k)^n))" 
+
+  have "summable (\<lambda>k. inverse ((real_of_nat k)^n))"
     using inverse_power_summable[of n] n by simp
   hence "summable (\<lambda>k. inverse ((real_of_nat (k + m - m))^n))" by simp
   thus "summable (\<lambda>k. inverse ((real_of_nat (k - m))^n))" by (rule summable_offset)
@@ -677,47 +673,51 @@
   by (simp add: summable_iff_convergent)
 
 lemma has_field_derivative_ln_Gamma_complex [derivative_intros]:
-  assumes z: "Re z > 0 \<or> Im z \<noteq> 0"
+  fixes z :: complex
+  assumes z: "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
   shows   "(ln_Gamma has_field_derivative Digamma z) (at z)"
 proof -
-  have not_nonpos_Int [simp]: "t \<notin> \<int>\<^sub>\<le>\<^sub>0" if "Re t > 0" for t 
+  have not_nonpos_Int [simp]: "t \<notin> \<int>\<^sub>\<le>\<^sub>0" if "Re t > 0" for t
     using that by (auto elim!: nonpos_Ints_cases')
-  from z have z': "z \<notin> \<int>\<^sub>\<le>\<^sub>0" and z'': "z \<noteq> 0" by (auto elim!: nonpos_Ints_cases)
+  from z have z': "z \<notin> \<int>\<^sub>\<le>\<^sub>0" and z'': "z \<noteq> 0" using nonpos_Ints_subset_nonpos_Reals nonpos_Reals_zero_I
+     by blast+
   let ?f' = "\<lambda>z k. inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))"
   let ?f = "\<lambda>z k. z / of_nat (Suc k) - ln (1 + z / of_nat (Suc k))" and ?F' = "\<lambda>z. \<Sum>n. ?f' z n"
   def d \<equiv> "min (norm z/2) (if Im z = 0 then Re z / 2 else abs (Im z) / 2)"
-  from z have d: "d > 0" "norm z/2 \<ge> d" by (auto simp add: d_def)
-  have ball: "Im t = 0 \<longrightarrow> Re t > 0" if "dist z t < d" for t 
-    using Re_pos_or_Im_nz_in_ball[OF z, of t] that unfolding d_def by auto
-  have sums: "(\<lambda>n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n)) sums 
+  from z have d: "d > 0" "norm z/2 \<ge> d" by (auto simp add: complex_nonpos_Reals_iff d_def)
+  have ball: "Im t = 0 \<longrightarrow> Re t > 0" if "dist z t < d" for t
+    using no_nonpos_Real_in_ball[OF z, of t] that unfolding d_def by (force simp add: complex_nonpos_Reals_iff)
+  have sums: "(\<lambda>n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n)) sums
                        (0 - inverse (z + of_nat 0))"
     by (intro telescope_sums filterlim_compose[OF tendsto_inverse_0]
               tendsto_add_filterlim_at_infinity[OF tendsto_const] tendsto_of_nat)
 
   have "((\<lambda>z. \<Sum>n. ?f z n) has_field_derivative ?F' z) (at z)"
     using d z ln_Gamma_series'_aux[OF z']
-    by (intro has_field_derivative_series'(2)[of "ball z d" _ _ z] uniformly_summable_deriv_ln_Gamma)
-       (auto intro!: derivative_eq_intros add_pos_pos mult_pos_pos dest!: ball
-             simp: field_simps Re_complex_div_gt_0 sums_iff Im_divide_of_nat
+    apply (intro has_field_derivative_series'(2)[of "ball z d" _ _ z] uniformly_summable_deriv_ln_Gamma)
+    apply (auto intro!: derivative_eq_intros add_pos_pos mult_pos_pos dest!: ball
+             simp: field_simps sums_iff nonpos_Reals_divide_of_nat_iff
              simp del: of_nat_Suc)
-  with z have "((\<lambda>z. (\<Sum>k. ?f z k) - euler_mascheroni * z - Ln z) has_field_derivative 
-                   ?F' z - euler_mascheroni - inverse z) (at z)" 
+    apply (auto simp add: complex_nonpos_Reals_iff)
+    done
+  with z have "((\<lambda>z. (\<Sum>k. ?f z k) - euler_mascheroni * z - Ln z) has_field_derivative
+                   ?F' z - euler_mascheroni - inverse z) (at z)"
     by (force intro!: derivative_eq_intros simp: Digamma_def)
   also have "?F' z - euler_mascheroni - inverse z = (?F' z + -inverse z) - euler_mascheroni" by simp
   also from sums have "-inverse z = (\<Sum>n. inverse (z + of_nat (Suc n)) - inverse (z + of_nat n))"
     by (simp add: sums_iff)
-  also from sums summable_deriv_ln_Gamma[OF z''] 
+  also from sums summable_deriv_ln_Gamma[OF z'']
     have "?F' z + \<dots> =  (\<Sum>n. inverse (of_nat (Suc n)) - inverse (z + of_nat n))"
     by (subst suminf_add) (simp_all add: add_ac sums_iff)
   also have "\<dots> - euler_mascheroni = Digamma z" by (simp add: Digamma_def)
-  finally have "((\<lambda>z. (\<Sum>k. ?f z k) - euler_mascheroni * z - Ln z) 
+  finally have "((\<lambda>z. (\<Sum>k. ?f z k) - euler_mascheroni * z - Ln z)
                     has_field_derivative Digamma z) (at z)" .
   moreover from eventually_nhds_ball[OF d(1), of z]
     have "eventually (\<lambda>z. ln_Gamma z = (\<Sum>k. ?f z k) - euler_mascheroni * z - Ln z) (nhds z)"
   proof eventually_elim
     fix t assume "t \<in> ball z d"
     hence "t \<notin> \<int>\<^sub>\<le>\<^sub>0" by (auto dest!: ball elim!: nonpos_Ints_cases)
-    from ln_Gamma_series'_aux[OF this] 
+    from ln_Gamma_series'_aux[OF this]
       show "ln_Gamma t = (\<Sum>k. ?f t k) - euler_mascheroni * t - Ln t" by (simp add: sums_iff)
   qed
   ultimately show ?thesis by (subst DERIV_cong_ev[OF refl _ refl])
@@ -728,16 +728,16 @@
 
 lemma Digamma_1 [simp]: "Digamma (1 :: 'a :: {real_normed_field,banach}) = - euler_mascheroni"
   by (simp add: Digamma_def)
-  
+
 lemma Digamma_plus1:
   assumes "z \<noteq> 0"
   shows   "Digamma (z+1) = Digamma z + 1/z"
 proof -
-  have sums: "(\<lambda>k. inverse (z + of_nat k) - inverse (z + of_nat (Suc k))) 
+  have sums: "(\<lambda>k. inverse (z + of_nat k) - inverse (z + of_nat (Suc k)))
                   sums (inverse (z + of_nat 0) - 0)"
     by (intro telescope_sums'[OF filterlim_compose[OF tendsto_inverse_0]]
               tendsto_add_filterlim_at_infinity[OF tendsto_const] tendsto_of_nat)
-  have "Digamma (z+1) = (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) - 
+  have "Digamma (z+1) = (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) -
           euler_mascheroni" (is "_ = suminf ?f - _") by (simp add: Digamma_def add_ac)
   also have "suminf ?f = (\<Sum>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) +
                          (\<Sum>k. inverse (z + of_nat k) - inverse (z + of_nat (Suc k)))"
@@ -759,18 +759,18 @@
     using Polygamma_converges'[OF assms, of "Suc n"] n
     by (subst suminf_split_initial_segment [symmetric]) simp_all
   hence "(\<Sum>k. ?f (k+1)) = (\<Sum>k. ?f k) - inverse (z ^ Suc n)" by (simp add: algebra_simps)
-  also have "(-1) ^ Suc n * fact n * ((\<Sum>k. ?f k) - inverse (z ^ Suc n)) = 
+  also have "(-1) ^ Suc n * fact n * ((\<Sum>k. ?f k) - inverse (z ^ Suc n)) =
                Polygamma n z + (-1)^n * fact n / (z ^ Suc n)" using n
     by (simp add: inverse_eq_divide algebra_simps Polygamma_def)
   finally show ?thesis .
 qed (insert assms, simp add: Digamma_plus1 inverse_eq_divide)
 
-lemma Digamma_of_nat: 
+lemma Digamma_of_nat:
   "Digamma (of_nat (Suc n) :: 'a :: {real_normed_field,banach}) = harm n - euler_mascheroni"
 proof (induction n)
   case (Suc n)
   have "Digamma (of_nat (Suc (Suc n)) :: 'a) = Digamma (of_nat (Suc n) + 1)" by simp
-  also have "\<dots> = Digamma (of_nat (Suc n)) + inverse (of_nat (Suc n))" 
+  also have "\<dots> = Digamma (of_nat (Suc n)) + inverse (of_nat (Suc n))"
     by (subst Digamma_plus1) (simp_all add: inverse_eq_divide del: of_nat_Suc)
   also have "Digamma (of_nat (Suc n) :: 'a) = harm n - euler_mascheroni " by (rule Suc)
   also have "\<dots> + inverse (of_nat (Suc n)) = harm (Suc n) - euler_mascheroni"
@@ -789,13 +789,13 @@
   by (elim Reals_cases, hypsubst, subst Polygamma_of_real) simp_all
 
 lemma Digamma_half_integer:
-  "Digamma (of_nat n + 1/2 :: 'a :: {real_normed_field,banach}) = 
+  "Digamma (of_nat n + 1/2 :: 'a :: {real_normed_field,banach}) =
       (\<Sum>k<n. 2 / (of_nat (2*k+1))) - euler_mascheroni - of_real (2 * ln 2)"
 proof (induction n)
   case 0
   have "Digamma (1/2 :: 'a) = of_real (Digamma (1/2))" by (simp add: Polygamma_of_real [symmetric])
-  also have "Digamma (1/2::real) = 
-               (\<Sum>k. inverse (of_nat (Suc k)) - inverse (of_nat k + 1/2)) - euler_mascheroni" 
+  also have "Digamma (1/2::real) =
+               (\<Sum>k. inverse (of_nat (Suc k)) - inverse (of_nat k + 1/2)) - euler_mascheroni"
     by (simp add: Digamma_def add_ac)
   also have "(\<Sum>k. inverse (of_nat (Suc k) :: real) - inverse (of_nat k + 1/2)) =
              (\<Sum>k. inverse (1/2) * (inverse (2 * of_nat (Suc k)) - inverse (2 * of_nat k + 1)))"
@@ -849,8 +849,8 @@
   have "(?F has_field_derivative (\<Sum>k. ?f' k z)) (at z)"
   proof (rule has_field_derivative_series'[of "ball z d" _ _ z])
     fix k :: nat and t :: 'a assume t: "t \<in> ball z d"
-    from t d(2)[of t] show "((\<lambda>z. ?f k z) has_field_derivative ?f' k t) (at t within ball z d)" 
-      by (auto intro!: derivative_eq_intros simp: power2_eq_square simp del: of_nat_Suc 
+    from t d(2)[of t] show "((\<lambda>z. ?f k z) has_field_derivative ?f' k t) (at t within ball z d)"
+      by (auto intro!: derivative_eq_intros simp: power2_eq_square simp del: of_nat_Suc
                dest!: plus_of_nat_eq_0_imp elim!: nonpos_Ints_cases)
   qed (insert d(1) summable conv, (assumption|simp)+)
   with z show "(Polygamma n has_field_derivative Polygamma (Suc n) z) (at z)"
@@ -871,10 +871,10 @@
                 - of_nat n' * inverse ((t + of_nat k) ^ (n'+1))) (at t within ball z d)" using t'
       by (fastforce intro!: derivative_eq_intros simp: divide_simps power_diff dest: plus_of_nat_eq_0_imp)
   next
-    have "uniformly_convergent_on (ball z d) 
-              (\<lambda>k z. (- of_nat n' :: 'a) * (\<Sum>i<k. inverse ((z + of_nat i) ^ (n'+1))))" 
+    have "uniformly_convergent_on (ball z d)
+              (\<lambda>k z. (- of_nat n' :: 'a) * (\<Sum>i<k. inverse ((z + of_nat i) ^ (n'+1))))"
       using z' n by (intro uniformly_convergent_mult Polygamma_converges) (simp_all add: n'_def)
-    thus "uniformly_convergent_on (ball z d) 
+    thus "uniformly_convergent_on (ball z d)
               (\<lambda>k z. \<Sum>i<k. - of_nat n' * inverse ((z + of_nat i :: 'a) ^ (n'+1)))"
       by (subst (asm) setsum_right_distrib) simp
   qed (insert Polygamma_converges'[OF z' n'] d, simp_all)
@@ -890,49 +890,50 @@
 
 declare has_field_derivative_Polygamma[THEN DERIV_chain2, derivative_intros]
 
-lemma isCont_Polygamma [continuous_intros]: 
+lemma isCont_Polygamma [continuous_intros]:
   fixes f :: "_ \<Rightarrow> 'a :: {real_normed_field,euclidean_space}"
   shows "isCont f z \<Longrightarrow> f z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> isCont (\<lambda>x. Polygamma n (f x)) z"
   by (rule isCont_o2[OF _  DERIV_isCont[OF has_field_derivative_Polygamma]])
 
-lemma continuous_on_Polygamma: 
+lemma continuous_on_Polygamma:
   "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> continuous_on A (Polygamma n :: _ \<Rightarrow> 'a :: {real_normed_field,euclidean_space})"
   by (intro continuous_at_imp_continuous_on isCont_Polygamma[OF continuous_ident] ballI) blast
 
-lemma isCont_ln_Gamma_complex [continuous_intros]: 
-  "isCont f z \<Longrightarrow> Re (f z) > 0 \<or> Im (f z) \<noteq> 0 \<Longrightarrow> isCont (\<lambda>z. ln_Gamma (f z)) z"
+lemma isCont_ln_Gamma_complex [continuous_intros]:
+  fixes f :: "'a::t2_space \<Rightarrow> complex"
+  shows "isCont f z \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> isCont (\<lambda>z. ln_Gamma (f z)) z"
   by (rule isCont_o2[OF _  DERIV_isCont[OF has_field_derivative_ln_Gamma_complex]])
 
 lemma continuous_on_ln_Gamma_complex [continuous_intros]:
-   "A \<inter> {z. Re z \<le> 0 \<and> Im z = 0} = {} \<Longrightarrow> continuous_on A ln_Gamma"
-  by (intro continuous_at_imp_continuous_on ballI isCont_ln_Gamma_complex[OF continuous_ident]) 
+  fixes A :: "complex set"
+  shows "A \<inter> \<real>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> continuous_on A ln_Gamma"
+  by (intro continuous_at_imp_continuous_on ballI isCont_ln_Gamma_complex[OF continuous_ident])
      fastforce
 
-
 text \<open>
-  We define a type class that captures all the fundamental properties of the inverse of the Gamma function 
-  and defines the Gamma function upon that. This allows us to instantiate the type class both for 
-  the reals and for the complex numbers with a minimal amount of proof duplication. 
+  We define a type class that captures all the fundamental properties of the inverse of the Gamma function
+  and defines the Gamma function upon that. This allows us to instantiate the type class both for
+  the reals and for the complex numbers with a minimal amount of proof duplication.
 \<close>
 
 class Gamma = real_normed_field + complete_space +
   fixes rGamma :: "'a \<Rightarrow> 'a"
   assumes rGamma_eq_zero_iff_aux: "rGamma z = 0 \<longleftrightarrow> (\<exists>n. z = - of_nat n)"
-  assumes differentiable_rGamma_aux1: 
+  assumes differentiable_rGamma_aux1:
     "(\<And>n. z \<noteq> - of_nat n) \<Longrightarrow>
-     let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (z + of_nat k)) 
+     let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (z + of_nat k))
                \<longlonglongrightarrow> d) - scaleR euler_mascheroni 1
-     in  filterlim (\<lambda>y. (rGamma y - rGamma z + rGamma z * d * (y - z)) /\<^sub>R 
+     in  filterlim (\<lambda>y. (rGamma y - rGamma z + rGamma z * d * (y - z)) /\<^sub>R
                         norm (y - z)) (nhds 0) (at z)"
-  assumes differentiable_rGamma_aux2: 
+  assumes differentiable_rGamma_aux2:
     "let z = - of_nat n
-     in  filterlim (\<lambda>y. (rGamma y - rGamma z - (-1)^n * (setprod of_nat {1..n}) * (y - z)) /\<^sub>R 
+     in  filterlim (\<lambda>y. (rGamma y - rGamma z - (-1)^n * (setprod of_nat {1..n}) * (y - z)) /\<^sub>R
                         norm (y - z)) (nhds 0) (at z)"
-  assumes rGamma_series_aux: "(\<And>n. z \<noteq> - of_nat n) \<Longrightarrow> 
+  assumes rGamma_series_aux: "(\<And>n. z \<noteq> - of_nat n) \<Longrightarrow>
              let fact' = (\<lambda>n. setprod of_nat {1..n});
                  exp = (\<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x^k /\<^sub>R fact k) \<longlonglongrightarrow> e);
                  pochhammer' = (\<lambda>a n. (\<Prod>n = 0..n. a + of_nat n))
-             in  filterlim (\<lambda>n. pochhammer' z n / (fact' n * exp (z * (ln (of_nat n) *\<^sub>R 1)))) 
+             in  filterlim (\<lambda>n. pochhammer' z n / (fact' n * exp (z * (ln (of_nat n) *\<^sub>R 1))))
                      (nhds (rGamma z)) sequentially"
 begin
 subclass banach ..
@@ -951,7 +952,7 @@
   and rGamma_nonzero: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> rGamma z \<noteq> 0"
   using rGamma_eq_zero_iff_aux[of z] unfolding Gamma_def by (auto elim!: nonpos_Ints_cases')
 
-lemma Gamma_eq_zero_iff: "Gamma z = 0 \<longleftrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0" 
+lemma Gamma_eq_zero_iff: "Gamma z = 0 \<longleftrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0"
   and rGamma_eq_zero_iff: "rGamma z = 0 \<longleftrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0"
   using rGamma_eq_zero_iff_aux[of z] unfolding Gamma_def by (auto elim!: nonpos_Ints_cases')
 
@@ -968,13 +969,13 @@
                   exp_def of_real_def[symmetric] suminf_def sums_def[abs_def])
 qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
 
-lemma Gamma_series_LIMSEQ [tendsto_intros]: 
+lemma Gamma_series_LIMSEQ [tendsto_intros]:
   "Gamma_series z \<longlonglongrightarrow> Gamma z"
 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
   case False
   hence "(\<lambda>n. inverse (rGamma_series z n)) \<longlonglongrightarrow> inverse (rGamma z)"
     by (intro tendsto_intros) (simp_all add: rGamma_eq_zero_iff)
-  also have "(\<lambda>n. inverse (rGamma_series z n)) = Gamma_series z" 
+  also have "(\<lambda>n. inverse (rGamma_series z n)) = Gamma_series z"
     by (simp add: rGamma_series_def Gamma_series_def[abs_def])
   finally show ?thesis by (simp add: Gamma_def)
 qed (insert Gamma_eq_zero_iff[of z], simp_all add: Gamma_series_nonpos_Ints_LIMSEQ)
@@ -986,7 +987,7 @@
 proof -
   have A: "eventually (\<lambda>n. rGamma_series 1 n = of_nat (Suc n) / of_nat n) sequentially"
     using eventually_gt_at_top[of "0::nat"]
-    by (force elim!: eventually_mono simp: rGamma_series_def exp_of_real pochhammer_fact 
+    by (force elim!: eventually_mono simp: rGamma_series_def exp_of_real pochhammer_fact
                     divide_simps pochhammer_rec' dest!: pochhammer_eq_0_imp_nonpos_Int)
   have "rGamma_series 1 \<longlonglongrightarrow> 1" by (subst tendsto_cong[OF A]) (rule LIMSEQ_Suc_n_over_n)
   moreover have "rGamma_series 1 \<longlonglongrightarrow> rGamma 1" by (rule tendsto_intros)
@@ -1030,10 +1031,10 @@
   using rGamma_plus1[of z] by (simp add: rGamma_inverse_Gamma field_simps Gamma_eq_zero_iff)
 
 lemma pochhammer_Gamma: "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> pochhammer z n = Gamma (z + of_nat n) / Gamma z"
-  using pochhammer_rGamma[of z] 
+  using pochhammer_rGamma[of z]
   by (simp add: rGamma_inverse_Gamma Gamma_eq_zero_iff field_simps)
 
-lemma Gamma_0 [simp]: "Gamma 0 = 0" 
+lemma Gamma_0 [simp]: "Gamma 0 = 0"
   and rGamma_0 [simp]: "rGamma 0 = 0"
   and Gamma_neg_1 [simp]: "Gamma (- 1) = 0"
   and rGamma_neg_1 [simp]: "rGamma (- 1) = 0"
@@ -1066,7 +1067,7 @@
   shows   "g \<longlonglongrightarrow> Gamma z"
 proof (rule Lim_transform_eventually)
   have "1/2 > (0::real)" by simp
-  from tendstoD[OF assms, OF this] 
+  from tendstoD[OF assms, OF this]
     show "eventually (\<lambda>n. g n / Gamma_series z n * Gamma_series z n = g n) sequentially"
     by (force elim!: eventually_mono simp: dist_real_def dist_0_norm)
   from assms have "(\<lambda>n. g n / Gamma_series z n * Gamma_series z n) \<longlonglongrightarrow> 1 * Gamma z"
@@ -1089,32 +1090,32 @@
 qed
 
 lemma Gamma_series'_LIMSEQ: "Gamma_series' z \<longlonglongrightarrow> Gamma z"
-  by (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0") (simp_all add: Gamma_nonpos_Int Gamma_seriesI[OF Gamma_series_Gamma_series'] 
+  by (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0") (simp_all add: Gamma_nonpos_Int Gamma_seriesI[OF Gamma_series_Gamma_series']
                                       Gamma_series'_nonpos_Ints_LIMSEQ[of z])
 
 
 subsection \<open>Differentiability\<close>
 
-lemma has_field_derivative_rGamma_no_nonpos_int: 
+lemma has_field_derivative_rGamma_no_nonpos_int:
   assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "(rGamma has_field_derivative -rGamma z * Digamma z) (at z within A)"
 proof (rule has_field_derivative_at_within)
   from assms have "z \<noteq> - of_nat n" for n by auto
-  from differentiable_rGamma_aux1[OF this] 
+  from differentiable_rGamma_aux1[OF this]
     show "(rGamma has_field_derivative -rGamma z * Digamma z) (at z)"
          unfolding Digamma_def suminf_def sums_def[abs_def]
                    has_field_derivative_def has_derivative_def netlimit_at
     by (simp add: Let_def bounded_linear_mult_right mult_ac of_real_def [symmetric])
 qed
 
-lemma has_field_derivative_rGamma_nonpos_int: 
-  "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n) within A)" 
+lemma has_field_derivative_rGamma_nonpos_int:
+  "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n) within A)"
   apply (rule has_field_derivative_at_within)
   using differentiable_rGamma_aux2[of n]
   unfolding Let_def has_field_derivative_def has_derivative_def netlimit_at
   by (simp only: bounded_linear_mult_right mult_ac of_real_def [symmetric] fact_altdef)
 
-lemma has_field_derivative_rGamma [derivative_intros]: 
+lemma has_field_derivative_rGamma [derivative_intros]:
   "(rGamma has_field_derivative (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>norm z\<rfloor>) * fact (nat \<lfloor>norm z\<rfloor>)
       else -rGamma z * Digamma z)) (at z within A)"
 using has_field_derivative_rGamma_no_nonpos_int[of z A]
@@ -1128,7 +1129,7 @@
 declare has_field_derivative_rGamma [derivative_intros]
 
 
-lemma has_field_derivative_Gamma [derivative_intros]: 
+lemma has_field_derivative_Gamma [derivative_intros]:
   "z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> (Gamma has_field_derivative Gamma z * Digamma z) (at z within A)"
   unfolding Gamma_def [abs_def]
   by (fastforce intro!: derivative_eq_intros simp: rGamma_eq_zero_iff)
@@ -1152,11 +1153,11 @@
 lemma continuous_on_Gamma [continuous_intros]: "A \<inter> \<int>\<^sub>\<le>\<^sub>0 = {} \<Longrightarrow> continuous_on A Gamma"
   by (rule DERIV_continuous_on has_field_derivative_Gamma)+ blast
 
-lemma isCont_rGamma [continuous_intros]: 
+lemma isCont_rGamma [continuous_intros]:
   "isCont f z \<Longrightarrow> isCont (\<lambda>x. rGamma (f x)) z"
   by (rule isCont_o2[OF _  DERIV_isCont[OF has_field_derivative_rGamma]])
 
-lemma isCont_Gamma [continuous_intros]: 
+lemma isCont_Gamma [continuous_intros]:
   "isCont f z \<Longrightarrow> f z \<notin> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> isCont (\<lambda>x. Gamma (f x)) z"
   by (rule isCont_o2[OF _  DERIV_isCont[OF has_field_derivative_Gamma]])
 
@@ -1170,7 +1171,7 @@
 definition rGamma_complex :: "complex \<Rightarrow> complex" where
   "rGamma_complex z = lim (rGamma_series z)"
 
-lemma rGamma_series_complex_converges: 
+lemma rGamma_series_complex_converges:
         "convergent (rGamma_series (z :: complex))" (is "?thesis1")
   and rGamma_complex_altdef:
         "rGamma z = (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then 0 else exp (-ln_Gamma z))" (is "?thesis2")
@@ -1181,7 +1182,7 @@
     have "rGamma_series z \<longlonglongrightarrow> exp (- ln_Gamma z)"
     proof (rule Lim_transform_eventually)
       from ln_Gamma_series_complex_converges'[OF False] guess d by (elim exE conjE)
-      from this(1) uniformly_convergent_imp_convergent[OF this(2), of z] 
+      from this(1) uniformly_convergent_imp_convergent[OF this(2), of z]
         have "ln_Gamma_series z \<longlonglongrightarrow> lim (ln_Gamma_series z)" by (simp add: convergent_LIMSEQ_iff)
       thus "(\<lambda>n. exp (-ln_Gamma_series z n)) \<longlonglongrightarrow> exp (- ln_Gamma z)"
         unfolding convergent_def ln_Gamma_def by (intro tendsto_exp tendsto_minus)
@@ -1222,13 +1223,13 @@
   qed
   moreover have "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> ((z+1) * 0 + 1) * rGamma z"
     using rGamma_series_complex_converges
-    by (intro tendsto_intros lim_inverse_n) 
+    by (intro tendsto_intros lim_inverse_n)
        (simp_all add: convergent_LIMSEQ_iff rGamma_complex_def)
   hence "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> rGamma z" by simp
   ultimately have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> rGamma z"
     by (rule Lim_transform_eventually)
   moreover have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> z * rGamma (z + 1)"
-    using rGamma_series_complex_converges 
+    using rGamma_series_complex_converges
     by (auto intro!: tendsto_mult simp: rGamma_complex_def convergent_LIMSEQ_iff)
   ultimately show "z * rGamma (z + 1) = rGamma z" using LIMSEQ_unique by blast
 qed
@@ -1237,19 +1238,19 @@
   assumes "(z :: complex) \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "(rGamma has_field_derivative - rGamma z * Digamma z) (at z)"
 proof -
-  have diff: "(rGamma has_field_derivative - rGamma z * Digamma z) (at z)" if "Re z > 0" for z 
+  have diff: "(rGamma has_field_derivative - rGamma z * Digamma z) (at z)" if "Re z > 0" for z
   proof (subst DERIV_cong_ev[OF refl _ refl])
-    from that have "eventually (\<lambda>t. t \<in> ball z (Re z/2)) (nhds z)" 
+    from that have "eventually (\<lambda>t. t \<in> ball z (Re z/2)) (nhds z)"
       by (intro eventually_nhds_in_nhd) simp_all
     thus "eventually (\<lambda>t. rGamma t = exp (- ln_Gamma t)) (nhds z)"
       using no_nonpos_Int_in_ball_complex[OF that]
       by (auto elim!: eventually_mono simp: rGamma_complex_altdef)
   next
-    show "((\<lambda>t. exp (- ln_Gamma t)) has_field_derivative (-rGamma z * Digamma z)) (at z)"
-      using that by (force elim!: nonpos_Ints_cases intro!: derivative_eq_intros 
-                           simp: rGamma_complex_altdef)
+    have "z \<notin> \<real>\<^sub>\<le>\<^sub>0" using that by (simp add: complex_nonpos_Reals_iff)
+    with that show "((\<lambda>t. exp (- ln_Gamma t)) has_field_derivative (-rGamma z * Digamma z)) (at z)"
+     by (force elim!: nonpos_Ints_cases intro!: derivative_eq_intros simp: rGamma_complex_altdef)
   qed
-  
+
   from assms show "(rGamma has_field_derivative - rGamma z * Digamma z) (at z)"
   proof (induction "nat \<lfloor>1 - Re z\<rfloor>" arbitrary: z)
     case (Suc n z)
@@ -1257,11 +1258,11 @@
     from Suc.hyps have "n = nat \<lfloor>- Re z\<rfloor>" by linarith
     hence A: "n = nat \<lfloor>1 - Re (z + 1)\<rfloor>" by simp
     from Suc.prems have B: "z + 1 \<notin> \<int>\<^sub>\<le>\<^sub>0" by (force dest: plus_one_in_nonpos_Ints_imp)
-    
-    have "((\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1)) z) has_field_derivative 
+
+    have "((\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1)) z) has_field_derivative
       -rGamma (z + 1) * (Digamma (z + 1) * z - 1)) (at z)"
       by (rule derivative_eq_intros DERIV_chain Suc refl A B)+ (simp add: algebra_simps)
-    also have "(\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1 :: complex)) z) = rGamma" 
+    also have "(\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1 :: complex)) z) = rGamma"
       by (simp add: rGamma_complex_plus1)
     also from z have "Digamma (z + 1) * z - 1 = z * Digamma z"
       by (subst Digamma_plus1) (simp_all add: field_simps)
@@ -1275,7 +1276,7 @@
 proof -
   have A: "eventually (\<lambda>n. rGamma_series 1 n = of_nat (Suc n) / of_nat n) sequentially"
     using eventually_gt_at_top[of "0::nat"]
-    by (force elim!: eventually_mono simp: rGamma_series_def exp_of_real pochhammer_fact 
+    by (force elim!: eventually_mono simp: rGamma_series_def exp_of_real pochhammer_fact
                     divide_simps pochhammer_rec' dest!: pochhammer_eq_0_imp_nonpos_Int)
   have "rGamma_series 1 \<longlonglongrightarrow> 1" by (subst tendsto_cong[OF A]) (rule LIMSEQ_Suc_n_over_n)
   thus "rGamma 1 = (1 :: complex)" unfolding rGamma_complex_def by (rule limI)
@@ -1292,11 +1293,11 @@
     thus ?case by (simp add: rGamma_complex_plus1)
 next
   case (Suc n)
-  hence A: "(rGamma has_field_derivative (-1)^n * fact n)  
+  hence A: "(rGamma has_field_derivative (-1)^n * fact n)
                 (at (- of_nat (Suc n) + 1 :: complex))" by simp
-   have "((\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1 :: complex)) z) has_field_derivative 
+   have "((\<lambda>z. z * (rGamma \<circ> (\<lambda>z. z + 1 :: complex)) z) has_field_derivative
              (- 1) ^ Suc n * fact (Suc n)) (at (- of_nat (Suc n)))"
-     by (rule derivative_eq_intros refl A DERIV_chain)+ 
+     by (rule derivative_eq_intros refl A DERIV_chain)+
         (simp add: algebra_simps rGamma_complex_altdef)
   thus ?case by (simp add: rGamma_complex_plus1)
 qed
@@ -1309,7 +1310,7 @@
   hence "z \<notin> \<int>\<^sub>\<le>\<^sub>0" by (auto elim!: nonpos_Ints_cases')
   from has_field_derivative_rGamma_complex_no_nonpos_Int[OF this]
     show "let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (z + of_nat k))
-                       \<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in  (\<lambda>y. (rGamma y - rGamma z + 
+                       \<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in  (\<lambda>y. (rGamma y - rGamma z +
               rGamma z * d * (y - z)) /\<^sub>R  cmod (y - z)) \<midarrow>z\<rightarrow> 0"
       by (simp add: has_field_derivative_def has_derivative_def Digamma_def sums_def [abs_def]
                     netlimit_at of_real_def[symmetric] suminf_def)
@@ -1323,7 +1324,7 @@
   fix z :: complex
   from rGamma_series_complex_converges[of z] have "rGamma_series z \<longlonglongrightarrow> rGamma z"
     by (simp add: convergent_LIMSEQ_iff rGamma_complex_def)
-  thus "let fact' = \<lambda>n. setprod of_nat {1..n}; 
+  thus "let fact' = \<lambda>n. setprod of_nat {1..n};
             exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e;
             pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
         in  (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma z"
@@ -1335,7 +1336,7 @@
 end
 
 
-lemma Gamma_complex_altdef: 
+lemma Gamma_complex_altdef:
   "Gamma z = (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then 0 else exp (ln_Gamma (z :: complex)))"
   unfolding Gamma_def rGamma_complex_altdef by (simp add: exp_minus)
 
@@ -1349,8 +1350,8 @@
 
 lemma cnj_Gamma: "cnj (Gamma z) = Gamma (cnj z)"
   unfolding Gamma_def by (simp add: cnj_rGamma)
-  
-lemma Gamma_complex_real: 
+
+lemma Gamma_complex_real:
   "z \<in> \<real> \<Longrightarrow> Gamma z \<in> (\<real> :: complex set)" and rGamma_complex_real: "z \<in> \<real> \<Longrightarrow> rGamma z \<in> \<real>"
   by (simp_all add: Reals_cnj_iff cnj_Gamma cnj_rGamma)
 
@@ -1375,7 +1376,7 @@
      (auto intro!: holomorphic_on_Gamma)
 
 lemma has_field_derivative_rGamma_complex' [derivative_intros]:
-  "(rGamma has_field_derivative (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>-Re z\<rfloor>) * fact (nat \<lfloor>-Re z\<rfloor>) else 
+  "(rGamma has_field_derivative (if z \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>-Re z\<rfloor>) * fact (nat \<lfloor>-Re z\<rfloor>) else
         -rGamma z * Digamma z)) (at z within A)"
   using has_field_derivative_rGamma[of z] by (auto elim!: nonpos_Ints_cases')
 
@@ -1428,21 +1429,21 @@
   finally show "(rGamma x) = 0 \<longleftrightarrow> (\<exists>n. x = - real_of_nat n)" by simp
 next
   fix x :: real assume "\<And>n. x \<noteq> - of_nat n"
-  hence "complex_of_real x \<notin> \<int>\<^sub>\<le>\<^sub>0" 
+  hence "complex_of_real x \<notin> \<int>\<^sub>\<le>\<^sub>0"
     by (subst of_real_in_nonpos_Ints_iff) (auto elim!: nonpos_Ints_cases')
   moreover from this have "x \<noteq> 0" by auto
   ultimately have "(rGamma has_field_derivative - rGamma x * Digamma x) (at x)"
-    by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex 
+    by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex
                   simp: Polygamma_of_real rGamma_real_def [abs_def])
   thus "let d = (THE d. (\<lambda>n. \<Sum>k<n. inverse (of_nat (Suc k)) - inverse (x + of_nat k))
-                       \<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in  (\<lambda>y. (rGamma y - rGamma x + 
+                       \<longlonglongrightarrow> d) - euler_mascheroni *\<^sub>R 1 in  (\<lambda>y. (rGamma y - rGamma x +
               rGamma x * d * (y - x)) /\<^sub>R  norm (y - x)) \<midarrow>x\<rightarrow> 0"
       by (simp add: has_field_derivative_def has_derivative_def Digamma_def sums_def [abs_def]
                     netlimit_at of_real_def[symmetric] suminf_def)
 next
   fix n :: nat
   have "(rGamma has_field_derivative (-1)^n * fact n) (at (- of_nat n :: real))"
-    by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex 
+    by (fastforce intro!: derivative_eq_intros has_vector_derivative_real_complex
                   simp: Polygamma_of_real rGamma_real_def [abs_def])
   thus "let x = - of_nat n in (\<lambda>y. (rGamma y - rGamma x - (- 1) ^ n * setprod of_nat {1..n} *
                   (y - x)) /\<^sub>R norm (y - x)) \<midarrow>x::real\<rightarrow> 0"
@@ -1454,7 +1455,7 @@
     show "(\<lambda>n. Re (rGamma_series (of_real x) n)) \<longlonglongrightarrow> rGamma x" unfolding rGamma_real_def
       by (intro tendsto_intros)
   qed (insert rGamma_series_real, simp add: eq_commute)
-  thus "let fact' = \<lambda>n. setprod of_nat {1..n}; 
+  thus "let fact' = \<lambda>n. setprod of_nat {1..n};
             exp = \<lambda>x. THE e. (\<lambda>n. \<Sum>k<n. x ^ k /\<^sub>R fact k) \<longlonglongrightarrow> e;
             pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
         in  (\<lambda>n. pochhammer' x n / (fact' n * exp (x * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma x"
@@ -1479,10 +1480,10 @@
 
 lemma Gamma_real_altdef2: "Gamma x = Re (Gamma (of_real x))"
   using rGamma_complex_real[OF Reals_of_real[of x]]
-  by (elim Reals_cases) 
+  by (elim Reals_cases)
      (simp only: Gamma_def rGamma_real_def of_real_inverse[symmetric] Re_complex_of_real)
 
-lemma ln_Gamma_series_complex_of_real: 
+lemma ln_Gamma_series_complex_of_real:
   "x > 0 \<Longrightarrow> n > 0 \<Longrightarrow> ln_Gamma_series (complex_of_real x) n = of_real (ln_Gamma_series x n)"
 proof -
   assume xn: "x > 0" "n > 0"
@@ -1491,15 +1492,15 @@
   with xn show ?thesis by (simp add: ln_Gamma_series_def Ln_of_nat Ln_of_real)
 qed
 
-lemma ln_Gamma_real_converges: 
-  assumes "(x::real) > 0" 
+lemma ln_Gamma_real_converges:
+  assumes "(x::real) > 0"
   shows   "convergent (ln_Gamma_series x)"
 proof -
   have "(\<lambda>n. ln_Gamma_series (complex_of_real x) n) \<longlonglongrightarrow> ln_Gamma (of_real x)" using assms
     by (intro ln_Gamma_complex_LIMSEQ) (auto simp: of_real_in_nonpos_Ints_iff)
   moreover from eventually_gt_at_top[of "0::nat"]
-    have "eventually (\<lambda>n. complex_of_real (ln_Gamma_series x n) = 
-            ln_Gamma_series (complex_of_real x) n) sequentially" 
+    have "eventually (\<lambda>n. complex_of_real (ln_Gamma_series x n) =
+            ln_Gamma_series (complex_of_real x) n) sequentially"
     by eventually_elim (simp add: ln_Gamma_series_complex_of_real assms)
   ultimately have "(\<lambda>n. complex_of_real (ln_Gamma_series x n)) \<longlonglongrightarrow> ln_Gamma (of_real x)"
     by (subst tendsto_cong) assumption+
@@ -1512,14 +1513,14 @@
 lemma ln_Gamma_complex_of_real: "x > 0 \<Longrightarrow> ln_Gamma (complex_of_real x) = of_real (ln_Gamma x)"
 proof (unfold ln_Gamma_def, rule limI, rule Lim_transform_eventually)
   assume x: "x > 0"
-  show "eventually (\<lambda>n. of_real (ln_Gamma_series x n) = 
-            ln_Gamma_series (complex_of_real x) n) sequentially" 
-    using eventually_gt_at_top[of "0::nat"] 
+  show "eventually (\<lambda>n. of_real (ln_Gamma_series x n) =
+            ln_Gamma_series (complex_of_real x) n) sequentially"
+    using eventually_gt_at_top[of "0::nat"]
     by eventually_elim (simp add: ln_Gamma_series_complex_of_real x)
 qed (intro tendsto_of_real, insert ln_Gamma_real_LIMSEQ[of x], simp add: ln_Gamma_def)
-     
+
 lemma Gamma_real_pos_exp: "x > (0 :: real) \<Longrightarrow> Gamma x = exp (ln_Gamma x)"
-  by (auto simp: Gamma_real_altdef2 Gamma_complex_altdef of_real_in_nonpos_Ints_iff 
+  by (auto simp: Gamma_real_altdef2 Gamma_complex_altdef of_real_in_nonpos_Ints_iff
                  ln_Gamma_complex_of_real exp_of_real)
 
 lemma ln_Gamma_real_pos: "x > 0 \<Longrightarrow> ln_Gamma x = ln (Gamma x :: real)"
@@ -1527,7 +1528,7 @@
 
 lemma Gamma_real_pos: "x > (0::real) \<Longrightarrow> Gamma x > 0"
   by (simp add: Gamma_real_pos_exp)
-  
+
 lemma has_field_derivative_ln_Gamma_real [derivative_intros]:
   assumes x: "x > (0::real)"
   shows "(ln_Gamma has_field_derivative Digamma x) (at x)"
@@ -1544,7 +1545,7 @@
 
 
 lemma has_field_derivative_rGamma_real' [derivative_intros]:
-  "(rGamma has_field_derivative (if x \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>-x\<rfloor>) * fact (nat \<lfloor>-x\<rfloor>) else 
+  "(rGamma has_field_derivative (if x \<in> \<int>\<^sub>\<le>\<^sub>0 then (-1)^(nat \<lfloor>-x\<rfloor>) * fact (nat \<lfloor>-x\<rfloor>) else
         -rGamma x * Digamma x)) (at x within A)"
   using has_field_derivative_rGamma[of x] by (force elim!: nonpos_Ints_cases')
 
@@ -1557,7 +1558,7 @@
   from assms have "x \<noteq> 0" by auto
   with assms show ?thesis
     unfolding Polygamma_def using Polygamma_converges'[of x "Suc n"]
-    by (auto simp: zero_less_power_eq simp del: power_Suc 
+    by (auto simp: zero_less_power_eq simp del: power_Suc
              dest: plus_of_nat_eq_0_imp intro!: mult_pos_pos suminf_pos)
 qed
 
@@ -1566,7 +1567,7 @@
   shows   "Polygamma n x < 0"
   using assms unfolding Polygamma_def using Polygamma_converges'[of x "Suc n"]
   by (auto intro!: mult_pos_pos suminf_pos)
-  
+
 lemma Polygamma_real_strict_mono:
   assumes "x > 0" "x < (y::real)" "even n"
   shows   "Polygamma n x < Polygamma n y"
@@ -1575,7 +1576,7 @@
     using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases)
   then guess \<xi> by (elim exE conjE) note \<xi> = this
   note \<xi>(3)
-  also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> > 0" 
+  also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> > 0"
     by (intro mult_pos_pos Polygamma_real_odd_pos) (auto elim!: nonpos_Ints_cases)
   finally show ?thesis by simp
 qed
@@ -1588,7 +1589,7 @@
     using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases)
   then guess \<xi> by (elim exE conjE) note \<xi> = this
   note \<xi>(3)
-  also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> < 0" 
+  also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> < 0"
     by (intro mult_pos_neg Polygamma_real_even_neg) simp_all
   finally show ?thesis by simp
 qed
@@ -1596,7 +1597,7 @@
 lemma Polygamma_real_mono:
   assumes "x > 0" "x \<le> (y::real)" "even n"
   shows   "Polygamma n x \<le> Polygamma n y"
-  using Polygamma_real_strict_mono[OF assms(1) _ assms(3), of y] assms(2) 
+  using Polygamma_real_strict_mono[OF assms(1) _ assms(3), of y] assms(2)
   by (cases "x = y") simp_all
 
 lemma Digamma_real_ge_three_halves_pos:
@@ -1616,11 +1617,11 @@
     using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases)
   then guess \<xi> by (elim exE conjE) note \<xi> = this
   note \<xi>(3)
-  also from \<xi>(1,2) assms have "(y - x) * Digamma \<xi> > 0" 
+  also from \<xi>(1,2) assms have "(y - x) * Digamma \<xi> > 0"
     by (intro mult_pos_pos Digamma_real_ge_three_halves_pos) simp_all
   finally show ?thesis by simp
-qed  
-  
+qed
+
 lemma Gamma_real_strict_mono:
   assumes "x \<ge> 3/2" "x < y"
   shows   "Gamma (x :: real) < Gamma y"
@@ -1633,7 +1634,7 @@
 
 lemma log_convex_Gamma_real: "convex_on {0<..} (ln \<circ> Gamma :: real \<Rightarrow> real)"
   by (rule convex_on_realI[of _ _ Digamma])
-     (auto intro!: derivative_eq_intros Polygamma_real_mono Gamma_real_pos 
+     (auto intro!: derivative_eq_intros Polygamma_real_mono Gamma_real_pos
            simp: o_def Gamma_eq_zero_iff elim!: nonpos_Ints_cases')
 
 
@@ -1649,21 +1650,21 @@
 
 lemma has_field_derivative_Beta1 [derivative_intros]:
   assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "x + y \<notin> \<int>\<^sub>\<le>\<^sub>0"
-  shows   "((\<lambda>x. Beta x y) has_field_derivative (Beta x y * (Digamma x - Digamma (x + y)))) 
+  shows   "((\<lambda>x. Beta x y) has_field_derivative (Beta x y * (Digamma x - Digamma (x + y))))
                (at x within A)" unfolding Beta_altdef
   by (rule DERIV_cong, (rule derivative_intros assms)+) (simp add: algebra_simps)
 
 lemma has_field_derivative_Beta2 [derivative_intros]:
   assumes "y \<notin> \<int>\<^sub>\<le>\<^sub>0" "x + y \<notin> \<int>\<^sub>\<le>\<^sub>0"
-  shows   "((\<lambda>y. Beta x y) has_field_derivative (Beta x y * (Digamma y - Digamma (x + y)))) 
+  shows   "((\<lambda>y. Beta x y) has_field_derivative (Beta x y * (Digamma y - Digamma (x + y))))
                (at y within A)"
   using has_field_derivative_Beta1[of y x A] assms by (simp add: Beta_commute add_ac)
 
-lemma Beta_plus1_plus1: 
-  assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0" 
+lemma Beta_plus1_plus1:
+  assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "Beta (x + 1) y + Beta x (y + 1) = Beta x y"
 proof -
-  have "Beta (x + 1) y + Beta x (y + 1) = 
+  have "Beta (x + 1) y + Beta x (y + 1) =
             (Gamma (x + 1) * Gamma y + Gamma x * Gamma (y + 1)) * rGamma ((x + y) + 1)"
     by (simp add: Beta_altdef add_divide_distrib algebra_simps)
   also have "\<dots> = (Gamma x * Gamma y) * ((x + y) * rGamma ((x + y) + 1))"
@@ -1672,7 +1673,7 @@
   finally show ?thesis .
 qed
 
-lemma Beta_plus1_left: 
+lemma Beta_plus1_left:
   assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "(x + y) * Beta (x + 1) y = x * Beta x y"
 proof -
@@ -1683,7 +1684,7 @@
   finally show ?thesis .
 qed
 
-lemma Beta_plus1_right: 
+lemma Beta_plus1_right:
   assumes "x \<notin> \<int>\<^sub>\<le>\<^sub>0" "y \<notin> \<int>\<^sub>\<le>\<^sub>0"
   shows   "(x + y) * Beta x (y + 1) = y * Beta x y"
   using Beta_plus1_left[of y x] assms by (simp add: Beta_commute add.commute)
@@ -1707,11 +1708,11 @@
   shows "Gamma z * Gamma (z + 1/2) = exp ((1 - 2*z) * of_real (ln 2)) * Gamma (1/2) * Gamma (2*z)"
 proof -
   let ?powr = "\<lambda>b a. exp (a * of_real (ln (of_nat b)))"
-  let ?h = "\<lambda>n. (fact (n-1))\<^sup>2 / fact (2*n-1) * of_nat (2^(2*n)) * 
+  let ?h = "\<lambda>n. (fact (n-1))\<^sup>2 / fact (2*n-1) * of_nat (2^(2*n)) *
                 exp (1/2 * of_real (ln (real_of_nat n)))"
   {
     fix z :: 'a assume z: "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z + 1/2 \<notin> \<int>\<^sub>\<le>\<^sub>0"
-    let ?g = "\<lambda>n. ?powr 2 (2*z) * Gamma_series' z n * Gamma_series' (z + 1/2) n / 
+    let ?g = "\<lambda>n. ?powr 2 (2*z) * Gamma_series' z n * Gamma_series' (z + 1/2) n /
                       Gamma_series' (2*z) (2*n)"
     have "eventually (\<lambda>n. ?g n = ?h n) sequentially" using eventually_gt_at_top
     proof eventually_elim
@@ -1721,21 +1722,21 @@
       have A: "Gamma_series' z n * Gamma_series' (z + 1/2) n = ?f^2 * ?powr n (2*z + 1/2) /
                 (pochhammer z n * pochhammer (z + 1/2) n)"
         by (simp add: Gamma_series'_def exp_add ring_distribs power2_eq_square A mult_ac)
-      have B: "Gamma_series' (2*z) (2*n) = 
-                       ?f' * ?powr 2 (2*z) * ?powr n (2*z) / 
+      have B: "Gamma_series' (2*z) (2*n) =
+                       ?f' * ?powr 2 (2*z) * ?powr n (2*z) /
                        (of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n)" using n
         by (simp add: Gamma_series'_def ln_mult exp_add ring_distribs pochhammer_double)
       from z have "pochhammer z n \<noteq> 0" by (auto dest: pochhammer_eq_0_imp_nonpos_Int)
       moreover from z have "pochhammer (z + 1/2) n \<noteq> 0" by (auto dest: pochhammer_eq_0_imp_nonpos_Int)
-      ultimately have "?powr 2 (2*z) * (Gamma_series' z n * Gamma_series' (z + 1/2) n) / Gamma_series' (2*z) (2*n) = 
+      ultimately have "?powr 2 (2*z) * (Gamma_series' z n * Gamma_series' (z + 1/2) n) / Gamma_series' (2*z) (2*n) =
          ?f^2 / ?f' * of_nat (2^(2*n)) * (?powr n ((4*z + 1)/2) * ?powr n (-2*z))"
         using n unfolding A B by (simp add: divide_simps exp_minus)
       also have "?powr n ((4*z + 1)/2) * ?powr n (-2*z) = ?powr n (1/2)"
         by (simp add: algebra_simps exp_add[symmetric] add_divide_distrib)
       finally show "?g n = ?h n" by (simp only: mult_ac)
     qed
-    
-    moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto     
+
+    moreover from z double_in_nonpos_Ints_imp[of z] have "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
     hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
       using lim_subseq[of "op * 2", OF _ Gamma_series'_LIMSEQ, of "2*z"]
       by (intro tendsto_intros Gamma_series'_LIMSEQ)
@@ -1743,8 +1744,8 @@
     ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
       by (rule Lim_transform_eventually)
   } note lim = this
-  
-  from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto  
+
+  from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
   from fraction_not_in_ints[of 2 1] have "(1/2 :: 'a) \<notin> \<int>\<^sub>\<le>\<^sub>0"
     by (intro not_in_Ints_imp_not_in_nonpos_Ints) simp_all
   with lim[of "1/2 :: 'a"] have "?h \<longlonglongrightarrow> 2 * Gamma (1 / 2 :: 'a)" by (simp add: exp_of_real)
@@ -1752,10 +1753,10 @@
     by (simp add: divide_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps)
 qed
 
-(* TODO: perhaps this is unnecessary once we have the fact that a holomorphic function is 
+(* TODO: perhaps this is unnecessary once we have the fact that a holomorphic function is
    infinitely differentiable *)
 private lemma Gamma_reflection_aux:
-  defines "h \<equiv> \<lambda>z::complex. if z \<in> \<int> then 0 else 
+  defines "h \<equiv> \<lambda>z::complex. if z \<in> \<int> then 0 else
                  (of_real pi * cot (of_real pi*z) + Digamma z - Digamma (1 - z))"
   defines "a \<equiv> complex_of_real pi"
   obtains h' where "continuous_on UNIV h'" "\<And>z. (h has_field_derivative (h' z)) (at z)"
@@ -1766,7 +1767,7 @@
   def G \<equiv> "\<lambda>z. if z = 0 then 1 else sin (a*z)/(a*z)"
   have a_nz: "a \<noteq> 0" unfolding a_def by simp
 
-  have "(\<lambda>n. f n * (a*z)^n) sums (F z) \<and> (\<lambda>n. g n * (a*z)^n) sums (G z)" 
+  have "(\<lambda>n. f n * (a*z)^n) sums (F z) \<and> (\<lambda>n. g n * (a*z)^n) sums (G z)"
     if "abs (Re z) < 1" for z
   proof (cases "z = 0"; rule conjI)
     assume "z \<noteq> 0"
@@ -1775,14 +1776,14 @@
     from z have sin_nz: "sin (a*z) \<noteq> 0" unfolding a_def by (auto simp: sin_eq_0)
     have "(\<lambda>n. of_real (sin_coeff n) * (a*z)^n) sums (sin (a*z))" using sin_converges[of "a*z"]
       by (simp add: scaleR_conv_of_real)
-    from sums_split_initial_segment[OF this, of 1] 
+    from sums_split_initial_segment[OF this, of 1]
       have "(\<lambda>n. (a*z) * of_real (sin_coeff (n+1)) * (a*z)^n) sums (sin (a*z))" by (simp add: mult_ac)
     from sums_mult[OF this, of "inverse (a*z)"] z a_nz
       have A: "(\<lambda>n. g n * (a*z)^n) sums (sin (a*z)/(a*z))"
       by (simp add: field_simps g_def)
     with z show "(\<lambda>n. g n * (a*z)^n) sums (G z)" by (simp add: G_def)
     from A z a_nz sin_nz have g_nz: "(\<Sum>n. g n * (a*z)^n) \<noteq> 0" by (simp add: sums_iff g_def)
-  
+
     have [simp]: "sin_coeff (Suc 0) = 1" by (simp add: sin_coeff_def)
     from sums_split_initial_segment[OF sums_diff[OF cos_converges[of "a*z"] A], of 1]
     have "(\<lambda>n. z * f n * (a*z)^n) sums (cos (a*z) - sin (a*z) / (a*z))"
@@ -1792,26 +1793,26 @@
   next
     assume z: "z = 0"
     have "(\<lambda>n. f n * (a * z) ^ n) sums f 0" using powser_sums_zero[of f] z by simp
-    with z show "(\<lambda>n. f n * (a * z) ^ n) sums (F z)" 
+    with z show "(\<lambda>n. f n * (a * z) ^ n) sums (F z)"
       by (simp add: f_def F_def sin_coeff_def cos_coeff_def)
     have "(\<lambda>n. g n * (a * z) ^ n) sums g 0" using powser_sums_zero[of g] z by simp
-    with z show "(\<lambda>n. g n * (a * z) ^ n) sums (G z)" 
+    with z show "(\<lambda>n. g n * (a * z) ^ n) sums (G z)"
       by (simp add: g_def G_def sin_coeff_def cos_coeff_def)
   qed
   note sums = conjunct1[OF this] conjunct2[OF this]
-  
-  def h2 \<equiv> "\<lambda>z. (\<Sum>n. f n * (a*z)^n) / (\<Sum>n. g n * (a*z)^n) + 
+
+  def h2 \<equiv> "\<lambda>z. (\<Sum>n. f n * (a*z)^n) / (\<Sum>n. g n * (a*z)^n) +
             Digamma (1 + z) - Digamma (1 - z)"
   def POWSER \<equiv> "\<lambda>f z. (\<Sum>n. f n * (z^n :: complex))"
   def POWSER' \<equiv> "\<lambda>f z. (\<Sum>n. diffs f n * (z^n :: complex))"
 
-  def h2' \<equiv> "\<lambda>z. a * (POWSER g (a*z) * POWSER' f (a*z) - POWSER f (a*z) * POWSER' g (a*z)) / 
-                     (POWSER g (a*z))^2 + Polygamma 1 (1 + z) + Polygamma 1 (1 - z)" 
-  
+  def h2' \<equiv> "\<lambda>z. a * (POWSER g (a*z) * POWSER' f (a*z) - POWSER f (a*z) * POWSER' g (a*z)) /
+                     (POWSER g (a*z))^2 + Polygamma 1 (1 + z) + Polygamma 1 (1 - z)"
+
   have h_eq: "h t = h2 t" if "abs (Re t) < 1" for t
   proof -
     from that have t: "t \<in> \<int> \<longleftrightarrow> t = 0" by (auto elim!: Ints_cases simp: dist_0_norm)
-    hence "h t = a*cot (a*t) - 1/t + Digamma (1 + t) - Digamma (1 - t)" 
+    hence "h t = a*cot (a*t) - 1/t + Digamma (1 + t) - Digamma (1 - t)"
       unfolding h_def using Digamma_plus1[of t] by (force simp: field_simps a_def)
     also have "a*cot (a*t) - 1/t = (F t) / (G t)"
       using t by (auto simp add: divide_simps sin_eq_0 cot_def a_def F_def G_def)
@@ -1819,14 +1820,14 @@
       using sums[of t] that by (simp add: sums_iff dist_0_norm)
     finally show "h t = h2 t" by (simp only: h2_def)
   qed
-  
-  let ?A = "{z. abs (Re z) < 1}"  
+
+  let ?A = "{z. abs (Re z) < 1}"
   have "open ({z. Re z < 1} \<inter> {z. Re z > -1})"
     using open_halfspace_Re_gt open_halfspace_Re_lt by auto
   also have "({z. Re z < 1} \<inter> {z. Re z > -1}) = {z. abs (Re z) < 1}" by auto
   finally have open_A: "open ?A" .
   hence [simp]: "interior ?A = ?A" by (simp add: interior_open)
-  
+
   have summable_f: "summable (\<lambda>n. f n * z^n)" for z
     by (rule powser_inside, rule sums_summable, rule sums[of "\<i> * of_real (norm z + 1) / a"])
        (simp_all add: norm_mult a_def del: of_real_add)
@@ -1837,10 +1838,10 @@
     by (intro termdiff_converges_all summable_f summable_g)+
   have "(POWSER f has_field_derivative (POWSER' f z)) (at z)"
                "(POWSER g has_field_derivative (POWSER' g z)) (at z)" for z
-    unfolding POWSER_def POWSER'_def 
+    unfolding POWSER_def POWSER'_def
     by (intro termdiffs_strong_converges_everywhere summable_f summable_g)+
   note derivs = this[THEN DERIV_chain2[OF _ DERIV_cmult[OF DERIV_ident]], unfolded POWSER_def]
-  have "isCont (POWSER f) z" "isCont (POWSER g) z" "isCont (POWSER' f) z" "isCont (POWSER' g) z" 
+  have "isCont (POWSER f) z" "isCont (POWSER g) z" "isCont (POWSER' f) z" "isCont (POWSER' g) z"
     for z unfolding POWSER_def POWSER'_def
     by (intro isCont_powser_converges_everywhere summable_f summable_g summable_fg')+
   note cont = this[THEN isCont_o2[rotated], unfolded POWSER_def POWSER'_def]
@@ -1850,9 +1851,9 @@
     def d \<equiv> "\<i> * of_real (norm z + 1)"
     have d: "abs (Re d) < 1" "norm z < norm d" by (simp_all add: d_def norm_mult del: of_real_add)
     have "eventually (\<lambda>z. h z = h2 z) (nhds z)"
-      using eventually_nhds_in_nhd[of z ?A] using h_eq z 
+      using eventually_nhds_in_nhd[of z ?A] using h_eq z
       by (auto elim!: eventually_mono simp: dist_0_norm)
-    
+
     moreover from sums(2)[OF z] z have nz: "(\<Sum>n. g n * (a * z) ^ n) \<noteq> 0"
       unfolding G_def by (auto simp: sums_iff sin_eq_0 a_def)
     have A: "z \<in> \<int> \<longleftrightarrow> z = 0" using z by (auto elim!: Ints_cases)
@@ -1864,13 +1865,13 @@
     have "(h2 has_field_derivative h2' z) (at z)" unfolding h2_def
       by (rule DERIV_cong, (rule derivative_intros refl derivs[unfolded POWSER_def] nz no_int)+)
          (auto simp: h2'_def POWSER_def field_simps power2_eq_square)
-    ultimately have deriv: "(h has_field_derivative h2' z) (at z)" 
+    ultimately have deriv: "(h has_field_derivative h2' z) (at z)"
       by (subst DERIV_cong_ev[OF refl _ refl])
-    
+
     from sums(2)[OF z] z have "(\<Sum>n. g n * (a * z) ^ n) \<noteq> 0"
       unfolding G_def by (auto simp: sums_iff a_def sin_eq_0)
     hence "isCont h2' z" using no_int unfolding h2'_def[abs_def] POWSER_def POWSER'_def
-      by (intro continuous_intros cont 
+      by (intro continuous_intros cont
             continuous_on_compose2[OF _ continuous_on_Polygamma[of "{z. Re z > 0}"]]) auto
     note deriv and this
   } note A = this
@@ -1884,11 +1885,11 @@
       hence A: "z + 1 \<notin> \<int>" "z \<noteq> 0" using Ints_diff[of "z+1" 1] by auto
       hence "Digamma (z + 1) - Digamma (-z) = Digamma z - Digamma (-z + 1)"
         by (subst (1 2) Digamma_plus1) simp_all
-      with A z show "h (z + 1) = h z" 
+      with A z show "h (z + 1) = h z"
         by (simp add: h_def sin_plus_pi cos_plus_pi ring_distribs cot_def)
     qed (simp add: h_def)
   qed
-  
+
   have h2'_eq: "h2' (z - 1) = h2' z" if z: "Re z > 0" "Re z < 1" for z
   proof -
     have "((\<lambda>z. h (z - 1)) has_field_derivative h2' (z - 1)) (at z)"
@@ -1909,11 +1910,11 @@
                             (insert B, auto intro!: derivative_intros)
     thus "(h has_field_derivative h2'' z) (at z)" by (simp add: h.minus_of_int)
   qed
-  
+
   have cont: "continuous_on UNIV h2''"
   proof (intro continuous_at_imp_continuous_on ballI)
     fix z :: complex
-    def r \<equiv> "\<lfloor>Re z\<rfloor>" 
+    def r \<equiv> "\<lfloor>Re z\<rfloor>"
     def A \<equiv> "{t. of_int r - 1 < Re t \<and> Re t < of_int r + 1}"
     have "continuous_on A (\<lambda>t. h2' (t - of_int r))" unfolding A_def
       by (intro continuous_at_imp_continuous_on isCont_o2[OF _ A(2)] ballI continuous_intros)
@@ -1921,7 +1922,7 @@
     moreover have "h2'' t = h2' (t - of_int r)" if t: "t \<in> A" for t
     proof (cases "Re t \<ge> of_int r")
       case True
-      from t have "of_int r - 1 < Re t" "Re t < of_int r + 1" by (simp_all add: A_def) 
+      from t have "of_int r - 1 < Re t" "Re t < of_int r + 1" by (simp_all add: A_def)
       with True have "\<lfloor>Re t\<rfloor> = \<lfloor>Re z\<rfloor>" unfolding r_def by linarith
       thus ?thesis by (auto simp: r_def h2''_def)
     next
@@ -1945,11 +1946,11 @@
     have "of_int r - 1 < Re z" "Re z  < of_int r + 1" unfolding r_def by linarith+
     thus "isCont h2'' z" by (intro C) (simp_all add: A_def)
   qed
-  
+
   from that[OF cont deriv] show ?thesis .
 qed
 
-lemma Gamma_reflection_complex: 
+lemma Gamma_reflection_complex:
   fixes z :: complex
   shows "Gamma z * Gamma (1 - z) = of_real pi / sin (of_real pi * z)"
 proof -
@@ -1966,13 +1967,13 @@
     proof (cases "z \<in> \<int>")
       case False
       hence "z * g z = z * Beta z (- z + 1) * sin (of_real pi * z)" by (simp add: g_def Beta_def)
-      also have "z * Beta z (- z + 1) = (z + 1 + -z) * Beta (z + 1) (- z + 1)" 
+      also have "z * Beta z (- z + 1) = (z + 1 + -z) * Beta (z + 1) (- z + 1)"
         using False Ints_diff[of 1 "1 - z"] nonpos_Ints_subset_Ints
         by (subst Beta_plus1_left [symmetric]) auto
       also have "\<dots> * sin (of_real pi * z) = z * (Beta (z + 1) (-z) * sin (of_real pi * (z + 1)))"
         using False Ints_diff[of "z+1" 1] Ints_minus[of "-z"] nonpos_Ints_subset_Ints
         by (subst Beta_plus1_right) (auto simp: ring_distribs sin_plus_pi)
-      also from False have "Beta (z + 1) (-z) * sin (of_real pi * (z + 1)) = g (z + 1)" 
+      also from False have "Beta (z + 1) (-z) * sin (of_real pi * (z + 1)) = g (z + 1)"
         using Ints_diff[of "z+1" 1] by (auto simp: g_def Beta_def)
       finally show "g (z + 1) = g z" using False by (subst (asm) mult_left_cancel) auto
     qed (simp add: g_def)
@@ -1988,7 +1989,7 @@
       by (intro eventually_nhds_in_open) (auto simp: open_Diff)
     hence "eventually (\<lambda>t. g t = ?g t) (nhds z)" by eventually_elim (simp add: g_def)
     moreover {
-      from False Ints_diff[of 1 "1-z"] have "1 - z \<notin> \<int>" by auto 
+      from False Ints_diff[of 1 "1-z"] have "1 - z \<notin> \<int>" by auto
       hence "(?g has_field_derivative ?h' z) (at z)" using nonpos_Ints_subset_Ints
         by (auto intro!: derivative_eq_intros simp: algebra_simps Beta_def)
       also from False have "sin (of_real pi * z) \<noteq> 0" by (subst sin_eq_0) auto
@@ -2016,12 +2017,12 @@
         qed (simp add: g_def)
       qed
       have "(?t has_field_derivative (0 * of_real pi)) (at 0)"
-        using has_field_derivative_sin_z_over_z[of "UNIV :: complex set"] 
+        using has_field_derivative_sin_z_over_z[of "UNIV :: complex set"]
         by (intro DERIV_chain) simp_all
       thus "((\<lambda>z. of_real pi * Gamma (1 + z) * Gamma (1 - z) * ?t z) has_field_derivative 0) (at 0)"
         by (auto intro!: derivative_eq_intros simp: o_def)
     qed
-    
+
     have "((g \<circ> (\<lambda>x. x - of_int n)) has_field_derivative 0 * 1) (at (of_int n))"
       using deriv_0 by (intro DERIV_chain) (auto intro!: derivative_eq_intros)
     also have "g \<circ> (\<lambda>x. x - of_int n) = g" by (intro ext) (simp add: g.minus_of_int)
@@ -2042,18 +2043,18 @@
     case False
     hence z: "z/2 \<notin> \<int>" "(z+1)/2 \<notin> \<int>" using Ints_diff[of "z+1" 1] by (auto elim!: Ints_cases)
     hence z': "z/2 \<notin> \<int>\<^sub>\<le>\<^sub>0" "(z+1)/2 \<notin> \<int>\<^sub>\<le>\<^sub>0" by (auto elim!: nonpos_Ints_cases)
-    from z have "1-z/2 \<notin> \<int>" "1-((z+1)/2) \<notin> \<int>" 
+    from z have "1-z/2 \<notin> \<int>" "1-((z+1)/2) \<notin> \<int>"
       using Ints_diff[of 1 "1-z/2"] Ints_diff[of 1 "1-((z+1)/2)"] by auto
     hence z'': "1-z/2 \<notin> \<int>\<^sub>\<le>\<^sub>0" "1-((z+1)/2) \<notin> \<int>\<^sub>\<le>\<^sub>0" by (auto elim!: nonpos_Ints_cases)
-    from z have "g (z/2) * g ((z+1)/2) = 
+    from z have "g (z/2) * g ((z+1)/2) =
       (Gamma (z/2) * Gamma ((z+1)/2)) * (Gamma (1-z/2) * Gamma (1-((z+1)/2))) *
       (sin (of_real pi * z/2) * sin (of_real pi * (z+1)/2))"
       by (simp add: g_def)
-    also from z' Gamma_legendre_duplication_aux[of "z/2"] 
+    also from z' Gamma_legendre_duplication_aux[of "z/2"]
       have "Gamma (z/2) * Gamma ((z+1)/2) = exp ((1-z) * of_real (ln 2)) * Gamma (1/2) * Gamma z"
       by (simp add: add_divide_distrib)
     also from z'' Gamma_legendre_duplication_aux[of "1-(z+1)/2"]
-      have "Gamma (1-z/2) * Gamma (1-(z+1)/2) = 
+      have "Gamma (1-z/2) * Gamma (1-(z+1)/2) =
               Gamma (1-z) * Gamma (1/2) * exp (z * of_real (ln 2))"
       by (simp add: add_divide_distrib ac_simps)
     finally have "g (z/2) * g ((z+1)/2) = Gamma (1/2)^2 * (Gamma z * Gamma (1-z) *
@@ -2074,8 +2075,8 @@
     have "Gamma (1/2)^2 * g z = Gamma (1/2)^2 * g (z - of_int (2*r))" by (simp only: g.minus_of_int)
     also have "of_int (2*r) = 2 * of_int r" by simp
     also have "Re z - 2 * of_int r > -1" "Re z - 2 * of_int r < 2" unfolding r_def by linarith+
-    hence "Gamma (1/2)^2 * g (z - 2 * of_int r) = 
-                   g ((z - 2 * of_int r)/2) * g ((z - 2 * of_int r + 1)/2)" 
+    hence "Gamma (1/2)^2 * g (z - 2 * of_int r) =
+                   g ((z - 2 * of_int r)/2) * g ((z - 2 * of_int r + 1)/2)"
       unfolding r_def by (intro g_eq[symmetric]) simp_all
     also have "(z - 2 * of_int r) / 2 = z/2 - of_int r" by simp
     also have "g \<dots> = g (z/2)" by (rule g.minus_of_int)
@@ -2083,11 +2084,11 @@
     also have "g \<dots> = g ((z+1)/2)" by (rule g.minus_of_int)
     finally show ?thesis ..
   qed
-    
+
   have g_nz [simp]: "g z \<noteq> 0" for z :: complex
   unfolding g_def using Ints_diff[of 1 "1 - z"]
     by (auto simp: Gamma_eq_zero_iff sin_eq_0 dest!: nonpos_Ints_Int)
-  
+
   have h_eq: "h z = (h (z/2) + h ((z+1)/2)) / 2" for z
   proof -
     have "((\<lambda>t. g (t/2) * g ((t+1)/2)) has_field_derivative
@@ -2106,28 +2107,28 @@
       by (intro DERIV_unique)
     thus "h z = (h (z/2) + h ((z+1)/2)) / 2" by simp
   qed
-  
+
   obtain h' where h'_cont: "continuous_on UNIV h'" and
                   h_h': "\<And>z. (h has_field_derivative h' z) (at z)"
-     unfolding h_def by (erule Gamma_reflection_aux) 
-  
+     unfolding h_def by (erule Gamma_reflection_aux)
+
   have h'_eq: "h' z = (h' (z/2) + h' ((z+1)/2)) / 4" for z
   proof -
     have "((\<lambda>t. (h (t/2) + h ((t+1)/2)) / 2) has_field_derivative
-                       ((h' (z/2) + h' ((z+1)/2)) / 4)) (at z)" 
+                       ((h' (z/2) + h' ((z+1)/2)) / 4)) (at z)"
       by (fastforce intro!: derivative_eq_intros h_h'[THEN DERIV_chain2])
     hence "(h has_field_derivative ((h' (z/2) + h' ((z+1)/2))/4)) (at z)"
       by (subst (asm) h_eq[symmetric])
     from h_h' and this show "h' z = (h' (z/2) + h' ((z+1)/2)) / 4" by (rule DERIV_unique)
   qed
-  
+
   have h'_zero: "h' z = 0" for z
   proof -
     def m \<equiv> "max 1 \<bar>Re z\<bar>"
     def B \<equiv> "{t. abs (Re t) \<le> m \<and> abs (Im t) \<le> abs (Im z)}"
-    have "closed ({t. Re t \<ge> -m} \<inter> {t. Re t \<le> m} \<inter> 
+    have "closed ({t. Re t \<ge> -m} \<inter> {t. Re t \<le> m} \<inter>
                   {t. Im t \<ge> -\<bar>Im z\<bar>} \<inter> {t. Im t \<le> \<bar>Im z\<bar>})"
-      (is "closed ?B") by (intro closed_Int closed_halfspace_Re_ge closed_halfspace_Re_le 
+      (is "closed ?B") by (intro closed_Int closed_halfspace_Re_ge closed_halfspace_Re_le
                                  closed_halfspace_Im_ge closed_halfspace_Im_le)
     also have "?B = B" unfolding B_def by fastforce
     finally have "closed B" .
@@ -2140,7 +2141,7 @@
       finally show "norm t \<le> m + \<bar>Im z\<bar>" by - simp
     qed
     ultimately have compact: "compact B" by (subst compact_eq_bounded_closed) blast
-    
+
     def M \<equiv> "SUP z:B. norm (h' z)"
     have "compact (h' ` B)"
       by (intro compact_continuous_image continuous_on_subset[OF h'_cont] compact) blast+
@@ -2160,8 +2161,8 @@
         also have "norm (h' (t/2) + h' ((t+1)/2)) \<le> norm (h' (t/2)) + norm (h' ((t+1)/2))"
           by (rule norm_triangle_ineq)
         also from t have "abs (Re ((t + 1)/2)) \<le> m" unfolding m_def B_def by auto
-        with t have "t/2 \<in> B" "(t+1)/2 \<in> B" unfolding B_def by auto        
-        hence "norm (h' (t/2)) + norm (h' ((t+1)/2)) \<le> M + M" unfolding M_def 
+        with t have "t/2 \<in> B" "(t+1)/2 \<in> B" unfolding B_def by auto
+        hence "norm (h' (t/2)) + norm (h' ((t+1)/2)) \<le> M + M" unfolding M_def
           by (intro add_mono cSUP_upper bdd) (auto simp: B_def)
         also have "(M + M) / 4 = M / 2" by simp
         finally show "norm (h' t) \<le> M/2" by - simp_all
@@ -2172,14 +2173,14 @@
   qed
   have h_h'_2: "(h has_field_derivative 0) (at z)" for z
     using h_h'[of z] h'_zero[of z] by simp
-  
+
   have g_real: "g z \<in> \<real>" if "z \<in> \<real>" for z
     unfolding g_def using that by (auto intro!: Reals_mult Gamma_complex_real)
   have h_real: "h z \<in> \<real>" if "z \<in> \<real>" for z
     unfolding h_def using that by (auto intro!: Reals_mult Reals_add Reals_diff Polygamma_Real)
   have g_nz: "g z \<noteq> 0" for z unfolding g_def using Ints_diff[of 1 "1-z"]
     by (auto simp: Gamma_eq_zero_iff sin_eq_0)
-  
+
   from h'_zero h_h'_2 have "\<exists>c. \<forall>z\<in>UNIV. h z = c"
     by (intro has_field_derivative_zero_constant) (simp_all add: dist_0_norm)
   then obtain c where c: "\<And>z. h z = c" by auto
@@ -2187,7 +2188,7 @@
     by (intro complex_mvt_line g_g')
     find_theorems name:deriv Reals
   then guess u by (elim exE conjE) note u = this
-  from u(1) have u': "u \<in> \<real>" unfolding closed_segment_def 
+  from u(1) have u': "u \<in> \<real>" unfolding closed_segment_def
     by (auto simp: scaleR_conv_of_real)
   from u' g_real[of u] g_nz[of u] have "Re (g u) \<noteq> 0" by (auto elim!: Reals_cases)
   with u(2) c[of u] g_real[of u] g_nz[of u] u'
@@ -2199,7 +2200,7 @@
   then obtain c' where c: "\<And>z. g z = c'" by (force simp: dist_0_norm)
   moreover from this[of 0] have "c' = pi" unfolding g_def by simp
   ultimately have "g z = pi" by simp
-  
+
   show ?thesis
   proof (cases "z \<in> \<int>")
     case False
@@ -2214,12 +2215,12 @@
   qed
 qed
 
-lemma rGamma_reflection_complex: 
+lemma rGamma_reflection_complex:
   "rGamma z * rGamma (1 - z :: complex) = sin (of_real pi * z) / of_real pi"
   using Gamma_reflection_complex[of z]
     by (simp add: Gamma_def divide_simps split: split_if_asm)
 
-lemma rGamma_reflection_complex': 
+lemma rGamma_reflection_complex':
   "rGamma z * rGamma (- z :: complex) = -z * sin (of_real pi * z) / of_real pi"
 proof -
   have "rGamma z * rGamma (-z) = -z * (rGamma z * rGamma (1 - z))"
@@ -2229,7 +2230,7 @@
   finally show ?thesis by simp
 qed
 
-lemma Gamma_reflection_complex': 
+lemma Gamma_reflection_complex':
   "Gamma z * Gamma (- z :: complex) = - of_real pi / (z * sin (of_real pi * z))"
   using rGamma_reflection_complex'[of z] by (force simp add: Gamma_def divide_simps mult_ac)
 
@@ -2256,7 +2257,7 @@
 lemma Gamma_legendre_duplication:
   fixes z :: complex
   assumes "z \<notin> \<int>\<^sub>\<le>\<^sub>0" "z + 1/2 \<notin> \<int>\<^sub>\<le>\<^sub>0"
-  shows "Gamma z * Gamma (z + 1/2) = 
+  shows "Gamma z * Gamma (z + 1/2) =
              exp ((1 - 2*z) * of_real (ln 2)) * of_real (sqrt pi) * Gamma (2*z)"
   using Gamma_legendre_duplication_aux[OF assms] by (simp add: Gamma_one_half_complex)
 
@@ -2269,12 +2270,12 @@
   The inverse of the Gamma function has simple zeros:
 \<close>
 
-lemma rGamma_zeros: 
+lemma rGamma_zeros:
   "(\<lambda>z. rGamma z / (z + of_nat n)) \<midarrow> (- of_nat n) \<rightarrow> ((-1)^n * fact n :: 'a :: Gamma)"
 proof (subst tendsto_cong)
   let ?f = "\<lambda>z. pochhammer z n * rGamma (z + of_nat (Suc n)) :: 'a"
   from eventually_at_ball'[OF zero_less_one, of "- of_nat n :: 'a" UNIV]
-    show "eventually (\<lambda>z. rGamma z / (z + of_nat n) = ?f z) (at (- of_nat n))" 
+    show "eventually (\<lambda>z. rGamma z / (z + of_nat n) = ?f z) (at (- of_nat n))"
     by (subst pochhammer_rGamma[of _ "Suc n"])
        (auto elim!: eventually_mono simp: divide_simps pochhammer_rec' eq_neg_iff_add_eq_0)
   have "isCont ?f (- of_nat n)" by (intro continuous_intros)
@@ -2284,7 +2285,7 @@
 
 
 text \<open>
-  The simple zeros of the inverse of the Gamma function correspond to simple poles of the Gamma function, 
+  The simple zeros of the inverse of the Gamma function correspond to simple poles of the Gamma function,
   and their residues can easily be computed from the limit we have just proven:
 \<close>
 
@@ -2294,27 +2295,27 @@
     have "eventually (\<lambda>z. rGamma z \<noteq> (0 :: 'a)) (at (- of_nat n))"
     by (auto elim!: eventually_mono nonpos_Ints_cases'
              simp: rGamma_eq_zero_iff dist_of_nat dist_minus)
-  with isCont_rGamma[of "- of_nat n :: 'a", OF continuous_ident] 
+  with isCont_rGamma[of "- of_nat n :: 'a", OF continuous_ident]
     have "filterlim (\<lambda>z. inverse (rGamma z) :: 'a) at_infinity (at (- of_nat n))"
     unfolding isCont_def by (intro filterlim_compose[OF filterlim_inverse_at_infinity])
                             (simp_all add: filterlim_at)
-  moreover have "(\<lambda>z. inverse (rGamma z) :: 'a) = Gamma" 
+  moreover have "(\<lambda>z. inverse (rGamma z) :: 'a) = Gamma"
     by (intro ext) (simp add: rGamma_inverse_Gamma)
   ultimately show ?thesis by (simp only: )
 qed
 
-lemma Gamma_residues: 
+lemma Gamma_residues:
   "(\<lambda>z. Gamma z * (z + of_nat n)) \<midarrow> (- of_nat n) \<rightarrow> ((-1)^n / fact n :: 'a :: Gamma)"
 proof (subst tendsto_cong)
   let ?c = "(- 1) ^ n / fact n :: 'a"
   from eventually_at_ball'[OF zero_less_one, of "- of_nat n :: 'a" UNIV]
-    show "eventually (\<lambda>z. Gamma z * (z + of_nat n) = inverse (rGamma z / (z + of_nat n))) 
-            (at (- of_nat n))" 
+    show "eventually (\<lambda>z. Gamma z * (z + of_nat n) = inverse (rGamma z / (z + of_nat n)))
+            (at (- of_nat n))"
     by (auto elim!: eventually_mono simp: divide_simps rGamma_inverse_Gamma)
-  have "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow> 
+  have "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow>
           inverse ((- 1) ^ n * fact n :: 'a)"
     by (intro tendsto_intros rGamma_zeros) simp_all
-  also have "inverse ((- 1) ^ n * fact n) = ?c" 
+  also have "inverse ((- 1) ^ n * fact n) = ?c"
     by (simp_all add: field_simps power_mult_distrib [symmetric] del: power_mult_distrib)
   finally show "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow> ?c" .
 qed
@@ -2328,7 +2329,7 @@
 
 
 definition Gamma_series_euler' where
-  "Gamma_series_euler' z n = 
+  "Gamma_series_euler' z n =
      inverse z * (\<Prod>k=1..n. exp (z * of_real (ln (1 + inverse (of_nat k)))) / (1 + z / of_nat k))"
 
 context
@@ -2338,7 +2339,7 @@
   assumes n: "n > 0"
   shows "exp (z * of_real (ln (of_nat n + 1))) = (\<Prod>k=1..n. exp (z * of_real (ln (1 + 1 / of_nat k))))"
 proof -
-  have "(\<Prod>k=1..n. exp (z * of_real (ln (1 + 1 / of_nat k)))) = 
+  have "(\<Prod>k=1..n. exp (z * of_real (ln (1 + 1 / of_nat k)))) =
           exp (z * of_real (\<Sum>k = 1..n. ln (1 + 1 / real_of_nat k)))"
     by (subst exp_setsum [symmetric]) (simp_all add: setsum_right_distrib)
   also have "(\<Sum>k=1..n. ln (1 + 1 / of_nat k) :: real) = ln (\<Prod>k=1..n. 1 + 1 / real_of_nat k)"
@@ -2365,18 +2366,18 @@
   moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))"
     by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all
   ultimately show "?r \<longlonglongrightarrow> 1" by (force dest!: Lim_transform_eventually)
-  
+
   from eventually_gt_at_top[of "0::nat"]
     show "eventually (\<lambda>n. ?r n = Gamma_series_euler' z n / Gamma_series z n) sequentially"
   proof eventually_elim
     fix n :: nat assume n: "n > 0"
-    from n z' have "Gamma_series_euler' z n = 
+    from n z' have "Gamma_series_euler' z n =
       exp (z * of_real (ln (of_nat n + 1))) / (z * (\<Prod>k=1..n. (1 + z / of_nat k)))"
-      by (subst Gamma_euler'_aux1) 
-         (simp_all add: Gamma_series_euler'_def setprod.distrib 
+      by (subst Gamma_euler'_aux1)
+         (simp_all add: Gamma_series_euler'_def setprod.distrib
                         setprod_inversef[symmetric] divide_inverse)
     also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n"
-      by (cases n) (simp_all add: pochhammer_def fact_altdef setprod_shift_bounds_cl_Suc_ivl 
+      by (cases n) (simp_all add: pochhammer_def fact_altdef setprod_shift_bounds_cl_Suc_ivl
                                   setprod_dividef[symmetric] divide_simps add_ac)
     also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec)
     finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp
@@ -2390,11 +2391,11 @@
 subsubsection \<open>Weierstrass form\<close>
 
 definition Gamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
-  "Gamma_series_weierstrass z n = 
+  "Gamma_series_weierstrass z n =
      exp (-euler_mascheroni * z) / z * (\<Prod>k=1..n. exp (z / of_nat k) / (1 + z / of_nat k))"
 
 definition rGamma_series_weierstrass :: "'a :: {banach,real_normed_field} \<Rightarrow> nat \<Rightarrow> 'a" where
-  "rGamma_series_weierstrass z n = 
+  "rGamma_series_weierstrass z n =
      exp (euler_mascheroni * z) * z * (\<Prod>k=1..n. (1 + z / of_nat k) * exp (-z / of_nat k))"
 
 lemma Gamma_series_weierstrass_nonpos_Ints:
@@ -2404,7 +2405,7 @@
 lemma rGamma_series_weierstrass_nonpos_Ints:
   "eventually (\<lambda>k. rGamma_series_weierstrass (- of_nat n) k = 0) sequentially"
   using eventually_ge_at_top[of n] by eventually_elim (auto simp: rGamma_series_weierstrass_def)
-  
+
 lemma Gamma_weierstrass_complex: "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma (z :: complex)"
 proof (cases "z \<in> \<int>\<^sub>\<le>\<^sub>0")
   case True
@@ -2420,15 +2421,18 @@
     using False that by (subst exp_Ln) (auto simp: field_simps dest!: plus_of_nat_eq_0_imp)
   have "(\<lambda>n. \<Sum>k=1..n. z / of_nat k - ln (1 + z / of_nat k)) \<longlonglongrightarrow> ln_Gamma z + euler_mascheroni * z + ln z"
     using ln_Gamma_series'_aux[OF False]
-    by (simp only: atLeastLessThanSuc_atLeastAtMost [symmetric] One_nat_def 
+    by (simp only: atLeastLessThanSuc_atLeastAtMost [symmetric] One_nat_def
                    setsum_shift_bounds_Suc_ivl sums_def atLeast0LessThan)
   from tendsto_exp[OF this] False z have "?f \<longlonglongrightarrow> z * exp (euler_mascheroni * z) * Gamma z"
     by (simp add: exp_add exp_setsum exp_diff mult_ac Gamma_complex_altdef A)
   from tendsto_mult[OF tendsto_const[of "exp (-euler_mascheroni * z) / z"] this] z
-    show "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma z" 
+    show "Gamma_series_weierstrass z \<longlonglongrightarrow> Gamma z"
     by (simp add: exp_minus divide_simps Gamma_series_weierstrass_def [abs_def])
 qed
 
+lemma tendsto_complex_of_real_iff: "((\<lambda>x. complex_of_real (f x)) \<longlongrightarrow> of_real c) F = (f \<longlongrightarrow> c) F"
+  by (rule tendsto_of_real_iff)
+
 lemma Gamma_weierstrass_real: "Gamma_series_weierstrass x \<longlonglongrightarrow> Gamma (x :: real)"
   using Gamma_weierstrass_complex[of "of_real x"] unfolding Gamma_series_weierstrass_def[abs_def]
   by (subst tendsto_complex_of_real_iff [symmetric])
@@ -2444,7 +2448,7 @@
 next
   case False
   have "rGamma_series_weierstrass z = (\<lambda>n. inverse (Gamma_series_weierstrass z n))"
-    by (simp add: rGamma_series_weierstrass_def[abs_def] Gamma_series_weierstrass_def 
+    by (simp add: rGamma_series_weierstrass_def[abs_def] Gamma_series_weierstrass_def
                   exp_minus divide_inverse setprod_inversef[symmetric] mult_ac)
   also from False have "\<dots> \<longlonglongrightarrow> inverse (Gamma z)"
     by (intro tendsto_intros Gamma_weierstrass_complex) (simp add: Gamma_eq_zero_iff)
@@ -2460,7 +2464,7 @@
   show ?thesis
   proof (rule Lim_transform_eventually)
     let ?powr = "\<lambda>a b. exp (b * of_real (ln (of_nat a)))"
-    show "eventually (\<lambda>n. rGamma_series z n / z = 
+    show "eventually (\<lambda>n. rGamma_series z n / z =
             ((z + of_nat n) gchoose n) * ?powr n (-z)) sequentially"
     proof (intro always_eventually allI)
       fix n :: nat
@@ -2470,20 +2474,20 @@
         by (simp add: rGamma_series_def divide_simps exp_minus)
       finally show "rGamma_series z n / z = ((z + of_nat n) gchoose n) * ?powr n (-z)" ..
     qed
-  
+
     from False have "(\<lambda>n. rGamma_series z n / z) \<longlonglongrightarrow> rGamma z / z" by (intro tendsto_intros)
-    also from False have "rGamma z / z = rGamma (z + 1)" using rGamma_plus1[of z] 
+    also from False have "rGamma z / z = rGamma (z + 1)" using rGamma_plus1[of z]
       by (simp add: field_simps)
     finally show "(\<lambda>n. rGamma_series z n / z) \<longlonglongrightarrow> rGamma (z+1)" .
   qed
 qed (simp_all add: binomial_gbinomial [symmetric])
 
-lemma fact_binomial_limit: 
+lemma fact_binomial_limit:
   "(\<lambda>n. of_nat ((k + n) choose n) / of_nat (n ^ k) :: 'a :: Gamma) \<longlonglongrightarrow> 1 / fact k"
 proof (rule Lim_transform_eventually)
   have "(\<lambda>n. of_nat ((k + n) choose n) / of_real (exp (of_nat k * ln (real_of_nat n))))
             \<longlonglongrightarrow> 1 / Gamma (of_nat (Suc k) :: 'a)" (is "?f \<longlonglongrightarrow> _")
-    using Gamma_binomial[of "of_nat k :: 'a"] 
+    using Gamma_binomial[of "of_nat k :: 'a"]
     by (simp add: binomial_gbinomial add_ac Gamma_def divide_simps exp_of_real [symmetric] exp_minus)
   also have "Gamma (of_nat (Suc k)) = fact k" by (rule Gamma_fact)
   finally show "?f \<longlonglongrightarrow> 1 / fact k" .
@@ -2498,7 +2502,7 @@
   qed
 qed
 
-lemma binomial_asymptotic: 
+lemma binomial_asymptotic:
   "(\<lambda>n. of_nat ((k + n) choose n) / (of_nat (n ^ k) / fact k) :: 'a :: Gamma) \<longlonglongrightarrow> 1"
   using tendsto_mult[OF fact_binomial_limit[of k] tendsto_const[of "fact k :: 'a"]] by simp
 
@@ -2517,14 +2521,14 @@
                     (\<lambda>n. of_real pi * z * (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2))"
   proof
     fix n :: nat
-    have "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) = 
+    have "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) =
               of_real pi * z * (\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2)"
       by (simp add: rGamma_series_weierstrass_def mult_ac exp_minus
                     divide_simps setprod.distrib[symmetric] power2_eq_square)
     also have "(\<Prod>k=1..n. (of_nat k - z) * (of_nat k + z) / of_nat k ^ 2) =
                  (\<Prod>k=1..n. 1 - z^2 / of_nat k ^ 2)"
       by (intro setprod.cong) (simp_all add: power2_eq_square field_simps)
-    finally show "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) = of_real pi * z * \<dots>" 
+    finally show "(- of_real pi * inverse z) * (?f z n * ?f (-z) n) = of_real pi * z * \<dots>"
       by (simp add: divide_simps)
   qed
   also have "(- of_real pi * inverse z) * (rGamma z * rGamma (- z)) = sin (of_real pi * z)"
@@ -2545,7 +2549,7 @@
 
 lemma sin_product_formula_real':
   assumes "x \<noteq> (0::real)"
-  shows   "(\<lambda>n. (\<Prod>k=1..n. 1 - x^2 / of_nat k^2)) \<longlonglongrightarrow> sin (pi * x) / (pi * x)" 
+  shows   "(\<lambda>n. (\<Prod>k=1..n. 1 - x^2 / of_nat k^2)) \<longlonglongrightarrow> sin (pi * x) / (pi * x)"
   using tendsto_divide[OF sin_product_formula_real[of x] tendsto_const[of "pi * x"]] assms
   by simp
 
@@ -2558,7 +2562,7 @@
   def K \<equiv> "\<Sum>n. inverse (real_of_nat (Suc n))^2"
   def f \<equiv> "\<lambda>x. \<Sum>n. P x n / of_nat (Suc n)^2"
   def g \<equiv> "\<lambda>x. (1 - sin (pi * x) / (pi * x))"
-  
+
   have sums: "(\<lambda>n. P x n / of_nat (Suc n)^2) sums (if x = 0 then K else g x / x^2)" for x
   proof (cases "x = 0")
     assume x: "x = 0"
@@ -2575,7 +2579,7 @@
     finally have "(\<lambda>n. x\<^sup>2 / (of_nat (Suc n))\<^sup>2 * P x n) sums (1 - sin (pi * x) / (pi * x))" .
     from sums_divide[OF this, of "x^2"] x show ?thesis unfolding g_def by simp
   qed
-  
+
   have "continuous_on (ball 0 1) f"
   proof (rule uniform_limit_theorem; (intro always_eventually allI)?)
     show "uniform_limit (ball 0 1) (\<lambda>n x. \<Sum>k<n. P x k / of_nat (Suc k)^2) f sequentially"
@@ -2585,7 +2589,7 @@
         fix k :: nat assume k: "k \<ge> 1"
         from x have "x^2 < 1" by (auto simp: dist_0_norm abs_square_less_1)
         also from k have "\<dots> \<le> of_nat k^2" by simp
-        finally have "(1 - x^2 / of_nat k^2) \<in> {0..1}" using k 
+        finally have "(1 - x^2 / of_nat k^2) \<in> {0..1}" using k
           by (simp_all add: field_simps del: of_nat_Suc)
       }
       hence "(\<Prod>k=1..n. abs (1 - x^2 / of_nat k^2)) \<le> (\<Prod>k=1..n. 1)" by (intro setprod_mono) simp
@@ -2596,12 +2600,12 @@
   hence "isCont f 0" by (subst (asm) continuous_on_eq_continuous_at) simp_all
   hence "(f \<midarrow> 0 \<rightarrow> f 0)" by (simp add: isCont_def)
   also have "f 0 = K" unfolding f_def P_def K_def by (simp add: inverse_eq_divide power_divide)
-  finally have "f \<midarrow> 0 \<rightarrow> K" . 
-  
+  finally have "f \<midarrow> 0 \<rightarrow> K" .
+
   moreover have "f \<midarrow> 0 \<rightarrow> pi^2 / 6"
   proof (rule Lim_transform_eventually)
     def f' \<equiv> "\<lambda>x. \<Sum>n. - sin_coeff (n+3) * pi ^ (n+2) * x^n"
-    have "eventually (\<lambda>x. x \<noteq> (0::real)) (at 0)" 
+    have "eventually (\<lambda>x. x \<noteq> (0::real)) (at 0)"
       by (auto simp add: eventually_at intro!: exI[of _ 1])
     thus "eventually (\<lambda>x. f' x = f x) (at 0)"
     proof eventually_elim
@@ -2619,28 +2623,28 @@
       also have "\<dots> = f x" using sums[of x] x by (simp add: sums_iff g_def f_def)
       finally show "f' x = f x" .
     qed
-    
+
     have "isCont f' 0" unfolding f'_def
-    proof (intro isCont_powser_converges_everywhere) 
+    proof (intro isCont_powser_converges_everywhere)
       fix x :: real show "summable (\<lambda>n. -sin_coeff (n+3) * pi^(n+2) * x^n)"
       proof (cases "x = 0")
         assume x: "x \<noteq> 0"
-        from summable_divide[OF sums_summable[OF sums_split_initial_segment[OF 
+        from summable_divide[OF sums_summable[OF sums_split_initial_segment[OF
                sin_converges[of "pi*x"]], of 3], of "-pi*x^3"] x
           show ?thesis by (simp add: mult_ac power_mult_distrib divide_simps eval_nat_numeral)
       qed (simp only: summable_0_powser)
     qed
     hence "f' \<midarrow> 0 \<rightarrow> f' 0" by (simp add: isCont_def)
-    also have "f' 0 = pi * pi / fact 3" unfolding f'_def 
+    also have "f' 0 = pi * pi / fact 3" unfolding f'_def
       by (subst powser_zero) (simp add: sin_coeff_def)
     finally show "f' \<midarrow> 0 \<rightarrow> pi^2 / 6" by (simp add: eval_nat_numeral)
   qed
-  
+
   ultimately have "K = pi^2 / 6" by (rule LIM_unique)
   moreover from inverse_power_summable[of 2]
     have "summable (\<lambda>n. (inverse (real_of_nat (Suc n)))\<^sup>2)"
     by (subst summable_Suc_iff) (simp add: power_inverse)
-  ultimately show ?thesis unfolding K_def 
+  ultimately show ?thesis unfolding K_def
     by (auto simp add: sums_iff power_divide inverse_eq_divide)
 qed
 

--- a/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -121,7 +121,7 @@
     hence z: "norm z < K" by (simp add: dist_0_norm)
     with K have nz: "1 + z \<noteq> 0" by (auto dest!: minus_unique)
     from z K have "norm z < 1" by simp
-    hence "Im (1 + z) \<noteq> 0 \<or> Re (1 + z) > 0" by (cases z) auto
+    hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: complex_nonpos_Reals_iff)
     hence "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative 
               f' z * (1 + z) powr (-a) - a * f z * (1 + z) powr (-a-1)) (at z)" using z
       by (auto intro!: derivative_eq_intros)

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -525,10 +525,19 @@
 
 lemma closedin_Inter[intro]:
   assumes Ke: "K \<noteq> {}"
-    and Kc: "\<forall>S \<in>K. closedin U S"
+    and Kc: "\<And>S. S \<in>K \<Longrightarrow> closedin U S"
   shows "closedin U (\<Inter>K)"
   using Ke Kc unfolding closedin_def Diff_Inter by auto
 
+lemma closedin_INT[intro]:
+  assumes "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> closedin U (B x)"
+  shows "closedin U (\<Inter>x\<in>A. B x)"
+  unfolding Inter_image_eq [symmetric]
+  apply (rule closedin_Inter)
+  using assms
+  apply auto
+  done
+
 lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
   using closedin_Inter[of "{S,T}" U] by auto
 
@@ -2322,6 +2331,13 @@
     (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a  < d \<longrightarrow> dist (f x) l < e)"
   by (auto simp add: tendsto_iff eventually_at)
 
+corollary Lim_withinI [intro?]:
+  assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l \<le> e"
+  shows "(f \<longlongrightarrow> l) (at a within S)"
+apply (simp add: Lim_within, clarify)
+apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
+done
+
 lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
     (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
   by (auto simp add: tendsto_iff eventually_at2)
@@ -2330,6 +2346,13 @@
   "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
   by (auto simp add: tendsto_iff eventually_at_infinity)
 
+corollary Lim_at_infinityI [intro?]:
+  assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>B. \<forall>x. norm x \<ge> B \<longrightarrow> dist (f x) l \<le> e"
+  shows "(f \<longlongrightarrow> l) at_infinity"
+apply (simp add: Lim_at_infinity, clarify)
+apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
+done
+
 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net"
   by (rule topological_tendstoI, auto elim: eventually_mono)
 
@@ -4911,6 +4934,33 @@
   using frontier_subset_closed compact_eq_bounded_closed
   by blast
 
+subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
+
+lemma summable_imp_bounded:
+  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
+  shows "summable f \<Longrightarrow> bounded (range f)"
+by (frule summable_LIMSEQ_zero) (simp add: convergent_imp_bounded)
+
+lemma summable_imp_sums_bounded:
+   "summable f \<Longrightarrow> bounded (range (\<lambda>n. setsum f {..<n}))"
+by (auto simp: summable_def sums_def dest: convergent_imp_bounded)
+
+lemma power_series_conv_imp_absconv_weak:
+  fixes a:: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}" and w :: 'a
+  assumes sum: "summable (\<lambda>n. a n * z ^ n)" and no: "norm w < norm z"
+    shows "summable (\<lambda>n. of_real(norm(a n)) * w ^ n)"
+proof -
+  obtain M where M: "\<And>x. norm (a x * z ^ x) \<le> M"
+    using summable_imp_bounded [OF sum] by (force simp add: bounded_iff)
+  then have *: "summable (\<lambda>n. norm (a n) * norm w ^ n)"
+    by (rule_tac M=M in Abel_lemma) (auto simp: norm_mult norm_power intro: no)
+  show ?thesis
+    apply (rule series_comparison_complex [of "(\<lambda>n. of_real(norm(a n) * norm w ^ n))"])
+    apply (simp only: summable_complex_of_real *)
+    apply (auto simp: norm_mult norm_power)
+    done
+qed
+
 subsection \<open>Bounded closed nest property (proof does not use Heine-Borel)\<close>
 
 lemma bounded_closed_nest:
@@ -5133,7 +5183,7 @@
   apply blast
   done
 
-lemma continuous_at_eps_delta:
+corollary continuous_at_eps_delta:
   "continuous (at x) f \<longleftrightarrow> (\<forall>e > 0. \<exists>d > 0. \<forall>x'. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
   using continuous_within_eps_delta [of x UNIV f] by simp
 
@@ -5240,6 +5290,21 @@
   unfolding continuous_on_def Lim_within
   by (metis dist_pos_lt dist_self)
 
+lemma continuous_within_E:
+  assumes "continuous (at x within s) f" "e>0"
+  obtains d where "d>0"  "\<And>x'. \<lbrakk>x'\<in> s; dist x' x \<le> d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
+  using assms apply (simp add: continuous_within_eps_delta)
+  apply (drule spec [of _ e], clarify)
+  apply (rule_tac d="d/2" in that, auto)
+  done
+
+lemma continuous_onI [intro?]:
+  assumes "\<And>x e. \<lbrakk>e > 0; x \<in> s\<rbrakk> \<Longrightarrow> \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) \<le> e"
+  shows "continuous_on s f"
+apply (simp add: continuous_on_iff, clarify)
+apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
+done
+
 lemma uniformly_continuous_on_def:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   shows "uniformly_continuous_on s f \<longleftrightarrow>

--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -272,20 +272,34 @@
   qed
 qed
 
-lemma weierstrass_m_test:
-fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
-assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
-assumes "summable M"
-shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
+text{*Alternative version, formulated as in HOL Light*}
+corollary series_comparison_uniform:
+  fixes f :: "_ \<Rightarrow> nat \<Rightarrow> _ :: banach"
+  assumes g: "summable g" and le: "\<And>n x. N \<le> n \<and> x \<in> A \<Longrightarrow> norm(f x n) \<le> g n"
+    shows "\<exists>l. \<forall>e. 0 < e \<longrightarrow> (\<exists>N. \<forall>n x. N \<le> n \<and> x \<in> A \<longrightarrow> dist(setsum (f x) {..<n}) (l x) < e)"
+proof -
+  have 1: "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. norm (f x n) \<le> g n"
+    using le eventually_sequentially by auto
+  show ?thesis
+    apply (rule_tac x="(\<lambda>x. \<Sum>i. f x i)" in exI)
+    apply (metis (no_types, lifting) eventually_sequentially uniform_limitD [OF weierstrass_m_test_ev [OF 1 g]])
+    done
+qed
+
+corollary weierstrass_m_test:
+  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
+  assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
+  assumes "summable M"
+  shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
   using assms by (intro weierstrass_m_test_ev always_eventually) auto
-  
-lemma weierstrass_m_test'_ev:
+    
+corollary weierstrass_m_test'_ev:
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M" 
   shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
   unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
 
-lemma weierstrass_m_test':
+corollary weierstrass_m_test':
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
   assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M" 
   shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"

--- a/src/HOL/NthRoot.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/NthRoot.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -425,6 +425,9 @@
 lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
   using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
 
+lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y^2"
+  by (meson not_le real_less_rsqrt)
+
 lemma sqrt_even_pow2:
   assumes n: "even n"
   shows "sqrt (2 ^ n) = 2 ^ (n div 2)"

--- a/src/HOL/Real_Vector_Spaces.thy	Mon Jan 11 20:51:13 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jan 11 22:14:42 2016 +0000
@@ -313,8 +313,7 @@
 by (simp add: divide_inverse nonzero_of_real_inverse)
 
 lemma of_real_divide [simp]:
-  "of_real (x / y) =
-   (of_real x / of_real y :: 'a::{real_field, field})"
+  "of_real (x / y) = (of_real x / of_real y :: 'a::real_div_algebra)"
 by (simp add: divide_inverse)
 
 lemma of_real_power [simp]: