--- 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)"
--- 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>
--- 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>
--- 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>