# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1500370532 -7200
# Node ID 1c977b13414f870224729b3aadcefec6b695c703
# Parent  4d722e3e870e61ce8941051b3c52be54cdafd734
poles and residues of the Gamma function

diff -r 4d722e3e870e -r 1c977b13414f src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jul 18 08:54:49 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jul 18 11:35:32 2017 +0200
@@ -6002,6 +6002,29 @@
     by (simp add: holomorphic_on_open open_Diff finite_imp_closed field_differentiable_def [symmetric])
 qed
 
+lemma no_isolated_singularity':
+  fixes z::complex
+  assumes f: "\<And>z. z \<in> k \<Longrightarrow> (f \<longlongrightarrow> f z) (at z within s)" 
+      and holf: "f holomorphic_on (s - k)" and s: "open s" and k: "finite k"
+    shows "f holomorphic_on s"
+proof (rule no_isolated_singularity[OF _ assms(2-)])
+  show "continuous_on s f" unfolding continuous_on_def
+  proof
+    fix z assume z: "z \<in> s"
+    show "(f \<longlongrightarrow> f z) (at z within s)"
+    proof (cases "z \<in> k")
+      case False
+      from holf have "continuous_on (s - k) f" 
+        by (rule holomorphic_on_imp_continuous_on)
+      with z False have "(f \<longlongrightarrow> f z) (at z within (s - k))" 
+        by (simp add: continuous_on_def)
+      also from z k s False have "at z within (s - k) = at z within s"
+        by (subst (1 2) at_within_open) (auto intro: finite_imp_closed)
+      finally show "(f \<longlongrightarrow> f z) (at z within s)" .
+    qed (insert assms z, simp_all)
+  qed
+qed
+
 proposition Cauchy_integral_formula_convex:
     assumes s: "convex s" and k: "finite k" and contf: "continuous_on s f"
         and fcd: "(\<And>x. x \<in> interior s - k \<Longrightarrow> f field_differentiable at x)"
diff -r 4d722e3e870e -r 1c977b13414f src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Jul 18 08:54:49 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Jul 18 11:35:32 2017 +0200
@@ -2143,6 +2143,52 @@
   "residue f z = (SOME int. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon><e
     \<longrightarrow> (f has_contour_integral 2*pi* \<i> *int) (circlepath z \<epsilon>))"
 
+lemma Eps_cong:
+  assumes "\<And>x. P x = Q x"
+  shows   "Eps P = Eps Q"
+  using ext[of P Q, OF assms] by simp
+
+lemma residue_cong:
+  assumes eq: "eventually (\<lambda>z. f z = g z) (at z)" and "z = z'"
+  shows   "residue f z = residue g z'"
+proof -
+  from assms have eq': "eventually (\<lambda>z. g z = f z) (at z)"
+    by (simp add: eq_commute)
+  let ?P = "\<lambda>f c e. (\<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow>
+   (f has_contour_integral of_real (2 * pi) * \<i> * c) (circlepath z \<epsilon>))"
+  have "residue f z = residue g z" unfolding residue_def
+  proof (rule Eps_cong)
+    fix c :: complex
+    have "\<exists>e>0. ?P g c e" 
+      if "\<exists>e>0. ?P f c e" and "eventually (\<lambda>z. f z = g z) (at z)" for f g 
+    proof -
+      from that(1) obtain e where e: "e > 0" "?P f c e"
+        by blast
+      from that(2) obtain e' where e': "e' > 0" "\<And>z'. z' \<noteq> z \<Longrightarrow> dist z' z < e' \<Longrightarrow> f z' = g z'"
+        unfolding eventually_at by blast
+      have "?P g c (min e e')"
+      proof (intro allI exI impI, goal_cases)
+        case (1 \<epsilon>)
+        hence "(f has_contour_integral of_real (2 * pi) * \<i> * c) (circlepath z \<epsilon>)" 
+          using e(2) by auto
+        thus ?case
+        proof (rule has_contour_integral_eq)
+          fix z' assume "z' \<in> path_image (circlepath z \<epsilon>)"
+          hence "dist z' z < e'" and "z' \<noteq> z"
+            using 1 by (auto simp: dist_commute)
+          with e'(2)[of z'] show "f z' = g z'" by simp
+        qed
+      qed
+      moreover from e and e' have "min e e' > 0" by auto
+      ultimately show ?thesis by blast
+    qed
+    from this[OF _ eq] and this[OF _ eq']
+      show "(\<exists>e>0. ?P f c e) \<longleftrightarrow> (\<exists>e>0. ?P g c e)"
+      by blast
+  qed
+  with assms show ?thesis by simp
+qed
+
 lemma contour_integral_circlepath_eq:
   assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0<e1" "e1\<le>e2"
     and e2_cball:"cball z e2 \<subseteq> s"
@@ -2401,6 +2447,37 @@
   thus ?thesis unfolding c_def f'_def  by auto
 qed
 
+lemma residue_simple':
+  assumes s: "open s" "z \<in> s" and holo: "f holomorphic_on (s - {z})" 
+      and lim: "((\<lambda>w. f w * (w - z)) \<longlongrightarrow> c) (at z)"
+  shows   "residue f z = c"
+proof -
+  define g where "g = (\<lambda>w. if w = z then c else f w * (w - z))"
+  from holo have "(\<lambda>w. f w * (w - z)) holomorphic_on (s - {z})" (is "?P")
+    by (force intro: holomorphic_intros)
+  also have "?P \<longleftrightarrow> g holomorphic_on (s - {z})"
+    by (intro holomorphic_cong refl) (simp_all add: g_def)
+  finally have *: "g holomorphic_on (s - {z})" .
+
+  note lim
+  also have "(\<lambda>w. f w * (w - z)) \<midarrow>z\<rightarrow> c \<longleftrightarrow> g \<midarrow>z\<rightarrow> g z"
+    by (intro filterlim_cong refl) (simp_all add: g_def [abs_def] eventually_at_filter)
+  finally have **: "g \<midarrow>z\<rightarrow> g z" .
+
+  have g_holo: "g holomorphic_on s"
+    by (rule no_isolated_singularity'[where k = "{z}"])
+       (insert assms * **, simp_all add: at_within_open_NO_MATCH)
+  from s and this have "residue (\<lambda>w. g w / (w - z)) z = g z"
+    by (rule residue_simple)
+  also have "\<forall>\<^sub>F za in at z. g za / (za - z) = f za"
+    unfolding eventually_at by (auto intro!: exI[of _ 1] simp: field_simps g_def)
+  hence "residue (\<lambda>w. g w / (w - z)) z = residue f z"
+    by (intro residue_cong refl)
+  finally show ?thesis
+    by (simp add: g_def)
+qed
+
+
 
 
 subsubsection \<open>Cauchy's residue theorem\<close>
diff -r 4d722e3e870e -r 1c977b13414f src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Tue Jul 18 08:54:49 2017 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Tue Jul 18 11:35:32 2017 +0200
@@ -6,7 +6,7 @@
 
 theory Gamma_Function
 imports
-  Cauchy_Integral_Theorem
+  Conformal_Mappings
   Summation_Tests
   Harmonic_Numbers
   "~~/src/HOL/Library/Nonpos_Ints"
@@ -2432,6 +2432,19 @@
   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>
diff -r 4d722e3e870e -r 1c977b13414f src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jul 18 08:54:49 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jul 18 11:35:32 2017 +0200
@@ -2054,6 +2054,17 @@
 lemma closed_Ints [simp]: "closed (\<int> :: 'a :: real_normed_algebra_1 set)"
   unfolding Ints_def by (rule closed_of_int_image)
 
+lemma closed_subset_Ints: 
+  fixes A :: "'a :: real_normed_algebra_1 set"
+  assumes "A \<subseteq> \<int>"
+  shows   "closed A"
+proof (intro discrete_imp_closed[OF zero_less_one] ballI impI, goal_cases)
+  case (1 x y)
+  with assms have "x \<in> \<int>" and "y \<in> \<int>" by auto
+  with \<open>dist y x < 1\<close> show "y = x"
+    by (auto elim!: Ints_cases simp: dist_of_int)
+qed
+
 
 subsection \<open>Interior of a Set\<close>