diff -r 8331063570d6 -r 954ee5acaae0 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Nov 27 16:54:33 2019 +0000
+++ b/src/HOL/Analysis/Gamma_Function.thy	Sat Nov 30 13:47:33 2019 +0100
@@ -6,7 +6,6 @@
 
 theory Gamma_Function
   imports
-  Conformal_Mappings
   Equivalence_Lebesgue_Henstock_Integration
   Summation_Tests
   Harmonic_Numbers
@@ -2065,7 +2064,208 @@
     by (simp add: field_split_simps Gamma_eq_zero_iff ring_distribs exp_diff exp_of_real ac_simps)
 qed
 
-theorem Gamma_reflection_complex:
+text \<open>
+  The following lemma is somewhat annoying. With a little bit of complex analysis
+  (Cauchy's integral theorem, to be exact), this would be completely trivial. However,
+  we want to avoid depending on the complex analysis session at this point, so we prove it
+  the hard way.
+\<close>
+private lemma Gamma_reflection_aux:
+  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)"
+proof -
+  define f where "f n = a * of_real (cos_coeff (n+1) - sin_coeff (n+2))" for n
+  define F where "F z = (if z = 0 then 0 else (cos (a*z) - sin (a*z)/(a*z)) / z)" for z
+  define g where "g n = complex_of_real (sin_coeff (n+1))" for n
+  define G where "G z = (if z = 0 then 1 else sin (a*z)/(a*z))" for 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)"
+    if "abs (Re z) < 1" for z
+  proof (cases "z = 0"; rule conjI)
+    assume "z \<noteq> 0"
+    note z = this that
+
+    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]
+      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))"
+      by (simp add: mult_ac scaleR_conv_of_real ring_distribs f_def g_def)
+    from sums_mult[OF this, of "inverse z"] z assms
+      show "(\<lambda>n. f n * (a*z)^n) sums (F z)" by (simp add: divide_simps mult_ac f_def F_def)
+  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)"
+      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)"
+      by (simp add: g_def G_def sin_coeff_def cos_coeff_def)
+  qed
+  note sums = conjunct1[OF this] conjunct2[OF this]
+
+  define h2 where [abs_def]:
+    "h2 z = (\<Sum>n. f n * (a*z)^n) / (\<Sum>n. g n * (a*z)^n) + Digamma (1 + z) - Digamma (1 - z)" for z
+  define POWSER where [abs_def]: "POWSER f z = (\<Sum>n. f n * (z^n :: complex))" for f z
+  define POWSER' where [abs_def]: "POWSER' f z = (\<Sum>n. diffs f n * (z^n))" for f and z :: complex
+  define h2' where [abs_def]:
+    "h2' 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)" for 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)"
+      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)
+    also have "\<dots> = (\<Sum>n. f n * (a*t)^n) / (\<Sum>n. g n * (a*t)^n)"
+      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}"
+  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)
+  have summable_g: "summable (\<lambda>n. g 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)
+  have summable_fg': "summable (\<lambda>n. diffs f n * z^n)" "summable (\<lambda>n. diffs g n * z^n)" for z
+    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
+    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"
+    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]
+
+  {
+    fix z :: complex assume z: "abs (Re z) < 1"
+    define d where "d = \<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
+      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)
+    have no_int: "1 + z \<in> \<int> \<longleftrightarrow> z = 0" using z Ints_diff[of "1+z" 1] A
+      by (auto elim!: nonpos_Ints_cases)
+    have no_int': "1 - z \<in> \<int> \<longleftrightarrow> z = 0" using z Ints_diff[of 1 "1-z"] A
+      by (auto elim!: nonpos_Ints_cases)
+    from no_int no_int' have no_int: "1 - z \<notin> \<int>\<^sub>\<le>\<^sub>0" "1 + z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
+    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)"
+      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
+            continuous_on_compose2[OF _ continuous_on_Polygamma[of "{z. Re z > 0}"]]) auto
+    note deriv and this
+  } note A = this
+
+  interpret h: periodic_fun_simple' h
+  proof
+    fix z :: complex
+    show "h (z + 1) = h z"
+    proof (cases "z \<in> \<int>")
+      assume z: "z \<notin> \<int>"
+      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"
+        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)"
+      by (rule DERIV_cong, rule DERIV_chain'[OF _ A(1)])
+         (insert z, auto intro!: derivative_eq_intros)
+    hence "(h has_field_derivative h2' (z - 1)) (at z)" by (subst (asm) h.minus_1)
+    moreover from z have "(h has_field_derivative h2' z) (at z)" by (intro A) simp_all
+    ultimately show "h2' (z - 1) = h2' z" by (rule DERIV_unique)
+  qed
+
+  define h2'' where "h2'' z = h2' (z - of_int \<lfloor>Re z\<rfloor>)" for z
+  have deriv: "(h has_field_derivative h2'' z) (at z)" for z
+  proof -
+    fix z :: complex
+    have B: "\<bar>Re z - real_of_int \<lfloor>Re z\<rfloor>\<bar> < 1" by linarith
+    have "((\<lambda>t. h (t - of_int \<lfloor>Re z\<rfloor>)) has_field_derivative h2'' z) (at z)"
+      unfolding h2''_def by (rule DERIV_cong, rule DERIV_chain'[OF _ A(1)])
+                            (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
+    define r where "r = \<lfloor>Re z\<rfloor>"
+    define A where "A = {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)
+         (simp_all add: abs_real_def)
+    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)
+      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
+      case False
+      from t have t: "of_int r - 1 < Re t" "Re t < of_int r + 1" by (simp_all add: A_def)
+      with False have t': "\<lfloor>Re t\<rfloor> = \<lfloor>Re z\<rfloor> - 1" unfolding r_def by linarith
+      moreover from t False have "h2' (t - of_int r + 1 - 1) = h2' (t - of_int r + 1)"
+        by (intro h2'_eq) simp_all
+      ultimately show ?thesis by (auto simp: r_def h2''_def algebra_simps t')
+    qed
+    ultimately have "continuous_on A h2''" by (subst continuous_on_cong[OF refl])
+    moreover {
+      have "open ({t. of_int r - 1 < Re t} \<inter> {t. of_int r + 1 > Re t})"
+        by (intro open_Int open_halfspace_Re_gt open_halfspace_Re_lt)
+      also have "{t. of_int r - 1 < Re t} \<inter> {t. of_int r + 1 > Re t} = A"
+        unfolding A_def by blast
+      finally have "open A" .
+    }
+    ultimately have C: "isCont h2'' t" if "t \<in> A" for t using that
+      by (subst (asm) continuous_on_eq_continuous_at) auto
+    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:
   fixes z :: complex
   shows "Gamma z * Gamma (1 - z) = of_real pi / sin (of_real pi * z)"
 proof -
@@ -2074,7 +2274,7 @@
   let ?h = "\<lambda>z::complex. (of_real pi * cot (of_real pi*z) + Digamma z - Digamma (1 - z))"
   define h where [abs_def]: "h z = (if z \<in> \<int> then 0 else ?h z)" for z :: complex
 
-  \<comment> \<open>\<^term>\<open>g\<close> is periodic with period 1.\<close>
+  \<comment> \<open>@{term g} is periodic with period 1.\<close>
   interpret g: periodic_fun_simple' g
   proof
     fix z :: complex
@@ -2094,8 +2294,8 @@
     qed (simp add: g_def)
   qed
 
-  \<comment> \<open>\<^term>\<open>g\<close> is entire.\<close>
-  have g_g' [derivative_intros]: "(g has_field_derivative (h z * g z)) (at z)" for z :: complex
+  \<comment> \<open>@{term g} is entire.\<close>
+  have g_g': "(g has_field_derivative (h z * g z)) (at z)" for z :: complex
   proof (cases "z \<in> \<int>")
     let ?h' = "\<lambda>z. Beta z (1 - z) * ((Digamma z - Digamma (1 - z)) * sin (z * of_real pi) +
                      of_real pi * cos (z * of_real pi))"
@@ -2144,10 +2344,6 @@
     finally show "(g has_field_derivative (h z * g z)) (at z)" by (simp add: z h_def)
   qed
 
-  have g_holo [holomorphic_intros]: "g holomorphic_on A" for A
-    by (rule holomorphic_on_subset[of _ UNIV])
-       (force simp: holomorphic_on_open intro!: derivative_intros)+
-
   have g_eq: "g (z/2) * g ((z+1)/2) = Gamma (1/2)^2 * g z" if "Re z > -1" "Re z < 2" for z
   proof (cases "z \<in> \<int>")
     case True
@@ -2208,9 +2404,6 @@
   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_altdef: "h z = deriv g z / g z" for z :: complex
-    using DERIV_imp_deriv[OF g_g', of z] by simp
-
   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
@@ -2230,16 +2423,9 @@
     thus "h z = (h (z/2) + h ((z+1)/2)) / 2" by simp
   qed
 
-  have h_holo [holomorphic_intros]: "h holomorphic_on A" for A
-    unfolding h_altdef [abs_def]
-    by (rule holomorphic_on_subset[of _ UNIV]) (auto intro!: holomorphic_intros)
-  define h' where "h' = deriv h"
-  have h_h': "(h has_field_derivative h' z) (at z)" for z unfolding h'_def
-    by (auto intro!: holomorphic_derivI[of _ UNIV] holomorphic_intros)
-  have h'_holo [holomorphic_intros]: "h' holomorphic_on A" for A unfolding h'_def
-    by (rule holomorphic_on_subset[of _ UNIV]) (auto intro!: holomorphic_intros)
-  have h'_cont: "continuous_on UNIV h'"
-    by (intro holomorphic_on_imp_continuous_on holomorphic_intros)
+  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)
 
   have h'_eq: "h' z = (h' (z/2) + h' ((z+1)/2)) / 4" for z
   proof -
@@ -2307,13 +2493,16 @@
     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
+    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
   have "\<exists>u. u \<in> closed_segment 0 1 \<and> Re (g 1) - Re (g 0) = Re (h u * g u * (1 - 0))"
     by (intro complex_mvt_line g_g')
-  then guess u by (elim exE conjE) note u = this
+  then obtain u where u: "u \<in> closed_segment 0 1" "Re (g 1) - Re (g 0) = Re (h u * g u)"
+    by auto
   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)
@@ -2330,7 +2519,7 @@
   show ?thesis
   proof (cases "z \<in> \<int>")
     case False
-    with \<open>g z = pi\<close> show ?thesis by (auto simp: g_def field_split_simps)
+    with \<open>g z = pi\<close> show ?thesis by (auto simp: g_def divide_simps)
   next
     case True
     then obtain n where n: "z = of_int n" by (elim Ints_cases)
@@ -2446,20 +2635,6 @@
   finally show "(\<lambda>z. inverse (rGamma z / (z + of_nat n))) \<midarrow> (- of_nat n) \<rightarrow> ?c" .
 qed
 
-lemma is_pole_Gamma: "is_pole Gamma (- of_nat n)"
-  unfolding is_pole_def using Gamma_poles .
-
-lemma Gamme_residue:
-  "residue Gamma (- of_nat n) = (-1) ^ n / fact n"
-proof (rule residue_simple')
-  show "open (- (\<int>\<^sub>\<le>\<^sub>0 - {-of_nat n}) :: complex set)"
-    by (intro open_Compl closed_subset_Ints) auto
-  show "Gamma holomorphic_on (- (\<int>\<^sub>\<le>\<^sub>0 - {-of_nat n}) - {- of_nat n})"
-    by (rule holomorphic_Gamma) auto
-  show "(\<lambda>w. Gamma w * (w - - of_nat n)) \<midarrow>- of_nat n \<rightarrow> (- 1) ^ n / fact n"
-    using Gamma_residues[of n] by simp
-qed auto
-
 
 subsection \<open>Alternative definitions\<close>