# HG changeset patch # User paulson # Date 1464190715 -3600 # Node ID 82df5181d69988f3df7987cff1104ba7e112dd16 # Parent 6a131df8e3d944580b7856c9744ccb9c46cf0293 updated proof of Residue Theorem (form Wenda Li) diff -r 6a131df8e3d9 -r 82df5181d699 src/HOL/Multivariate_Analysis/Conformal_Mappings.thy --- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Wed May 25 13:13:35 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Wed May 25 16:38:35 2016 +0100 @@ -9,6 +9,33 @@ begin +lemma finite_ball_avoid: + assumes "open S" "finite X" "p \ S" + shows "\e>0. \w\ball p e. w\S \ (w\p \ w\X)" +proof - + obtain e1 where "0 < e1" and e1_b:"ball p e1 \ S" + using open_contains_ball_eq[OF \open S\] assms by auto + obtain e2 where "0x\X. x \ p \ e2 \ dist p x" + using finite_set_avoid[OF \finite X\,of p] by auto + hence "\w\ball p (min e1 e2). w\S \ (w\p \ w\X)" using e1_b by auto + thus "\e>0. \w\ball p e. w \ S \ (w \ p \ w \ X)" using \e2>0\ \e1>0\ + apply (rule_tac x="min e1 e2" in exI) + by auto +qed + +lemma finite_cball_avoid: + fixes S :: "'a :: euclidean_space set" + assumes "open S" "finite X" "p \ S" + shows "\e>0. \w\cball p e. w\S \ (w\p \ w\X)" +proof - + obtain e1 where "e1>0" and e1: "\w\ball p e1. w\S \ (w\p \ w\X)" + using finite_ball_avoid[OF assms] by auto + define e2 where "e2 \ e1/2" + have "e2>0" and "e2e1>0\ by auto + then have "cball p e2 \ ball p e1" by (subst cball_subset_ball_iff,auto) + then show "\e>0. \w\cball p e. w \ S \ (w \ p \ w \ X)" using \e2>0\ e1 by auto +qed + subsection\Cauchy's inequality and more versions of Liouville\ lemma Cauchy_higher_deriv_bound: @@ -2134,159 +2161,282 @@ qed qed -subsection \Cauchy's residue theorem\ +subsection \Foundations of Cauchy's residue theorem\ -text\Wenda Li (2016)\ +text\Wenda Li and LC Paulson (2016). A Formal Proof of Cauchy's Residue Theorem. + Interactive Theorem Proving\ -declare valid_path_imp_path [simp] +definition residue :: "(complex \ complex) \ complex \ complex" where + "residue f z = (SOME int. \e>0. \\>0. \ (f has_contour_integral 2*pi* ii *int) (circlepath z \))" -lemma holomorphic_factor_zero_unique: - fixes f::"complex \ complex" and z::complex and r::real - assumes "r>0" - and asm:"\w\ball z r. f w = (w-z)^n * g w \ g w\0 \ f w = (w - z)^m * h w \ h w\0" - and g_holo:"g holomorphic_on ball z r" and h_holo:"h holomorphic_on ball z r" - shows "n=m" +lemma contour_integral_circlepath_eq: + assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0e2" + and e2_cball:"cball z e2 \ s" + shows + "f contour_integrable_on circlepath z e1" + "f contour_integrable_on circlepath z e2" + "contour_integral (circlepath z e2) f = contour_integral (circlepath z e1) f" proof - - have "n>m \ False" + define l where "l \ linepath (z+e2) (z+e1)" + have [simp]:"valid_path l" "pathstart l=z+e2" "pathfinish l=z+e1" unfolding l_def by auto + have "e2>0" using \e1>0\ \e1\e2\ by auto + have zl_img:"z\path_image l" + proof + assume "z \ path_image l" + then have "e2 \ cmod (e2 - e1)" + using segment_furthest_le[of z "z+e2" "z+e1" "z+e2",simplified] \e1>0\ \e2>0\ unfolding l_def + by (auto simp add:closed_segment_commute) + thus False using \e2>0\ \e1>0\ \e1\e2\ + apply (subst (asm) norm_of_real) + by auto + qed + define g where "g \ circlepath z e2 +++ l +++ reversepath (circlepath z e1) +++ reversepath l" + show [simp]: "f contour_integrable_on circlepath z e2" "f contour_integrable_on (circlepath z e1)" proof - - assume "n>m" - have "(h \ 0) (at z within ball z r)" - proof (rule Lim_transform_within[OF _ \r>0\, where f="\w. (w - z) ^ (n - m) * g w"]) - have "\w\ball z r. w\z \ h w = (w-z)^(n-m) * g w" using \n>m\ asm - by (auto simp add:field_simps power_diff) - then show "\x' \ ball z r; 0 < dist x' z;dist x' z < r\ - \ (x' - z) ^ (n - m) * g x' = h x'" for x' by auto - next - define F where "F = at z within ball z r" - define f' where [abs_def]: "f' x = (x - z) ^ (n-m)" for x - have "f' z=0" using \n>m\ unfolding f'_def by auto - moreover have "continuous F f'" unfolding f'_def F_def - by (intro continuous_intros) - ultimately have "(f' \ 0) F" unfolding F_def - by (simp add: continuous_within) - moreover have "(g \ g z) F" - using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] \r>0\ - unfolding F_def by auto - ultimately show " ((\w. f' w * g w) \ 0) F" using tendsto_mult by fastforce + show "f contour_integrable_on circlepath z e2" + apply (intro contour_integrable_continuous_circlepath[OF + continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]]) + using \e2>0\ e2_cball by auto + show "f contour_integrable_on (circlepath z e1)" + apply (intro contour_integrable_continuous_circlepath[OF + continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]]) + using \e1>0\ \e1\e2\ e2_cball by auto + qed + have [simp]:"f contour_integrable_on l" + proof - + have "closed_segment (z + e2) (z + e1) \ cball z e2" using \e2>0\ \e1>0\ \e1\e2\ + by (intro closed_segment_subset,auto simp add:dist_norm) + hence "closed_segment (z + e2) (z + e1) \ s - {z}" using zl_img e2_cball unfolding l_def + by auto + then show "f contour_integrable_on l" unfolding l_def + apply (intro contour_integrable_continuous_linepath[OF + continuous_on_subset[OF holomorphic_on_imp_continuous_on[OF f_holo]]]) + by auto + qed + let ?ig="\g. contour_integral g f" + have "(f has_contour_integral 0) g" + proof (rule Cauchy_theorem_global[OF _ f_holo]) + show "open (s - {z})" using \open s\ by auto + show "valid_path g" unfolding g_def l_def by auto + show "pathfinish g = pathstart g" unfolding g_def l_def by auto + next + have path_img:"path_image g \ cball z e2" + proof - + have "closed_segment (z + e2) (z + e1) \ cball z e2" using \e2>0\ \e1>0\ \e1\e2\ + by (intro closed_segment_subset,auto simp add:dist_norm) + moreover have "sphere z \e1\ \ cball z e2" using \e2>0\ \e1\e2\ \e1>0\ by auto + ultimately show ?thesis unfolding g_def l_def using \e2>0\ + by (simp add: path_image_join closed_segment_commute) qed - moreover have "(h \ h z) (at z within ball z r)" - using holomorphic_on_imp_continuous_on[OF h_holo] - by (auto simp add:continuous_on_def \r>0\) - moreover have "at z within ball z r \ bot" using \r>0\ - by (auto simp add:trivial_limit_within islimpt_ball) - ultimately have "h z=0" by (auto intro: tendsto_unique) - thus False using asm \r>0\ by auto - qed - moreover have "m>n \ False" - proof - - assume "m>n" - have "(g \ 0) (at z within ball z r)" - proof (rule Lim_transform_within[OF _ \r>0\, where f="\w. (w - z) ^ (m - n) * h w"]) - have "\w\ball z r. w\z \ g w = (w-z)^(m-n) * h w" using \m>n\ asm - by (auto simp add:field_simps power_diff) - then show "\x' \ ball z r; 0 < dist x' z;dist x' z < r\ - \ (x' - z) ^ (m - n) * h x' = g x'" for x' by auto - next - define F where "F = at z within ball z r" - define f' where [abs_def]: "f' x = (x - z) ^ (m-n)" for x - have "f' z=0" using \m>n\ unfolding f'_def by auto - moreover have "continuous F f'" unfolding f'_def F_def - by (intro continuous_intros) - ultimately have "(f' \ 0) F" unfolding F_def - by (simp add: continuous_within) - moreover have "(h \ h z) F" - using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] \r>0\ - unfolding F_def by auto - ultimately show " ((\w. f' w * h w) \ 0) F" using tendsto_mult by fastforce + show "path_image g \ s - {z}" + proof - + have "z\path_image g" using zl_img + unfolding g_def l_def by (auto simp add: path_image_join closed_segment_commute) + moreover note \cball z e2 \ s\ and path_img + ultimately show ?thesis by auto qed - moreover have "(g \ g z) (at z within ball z r)" - using holomorphic_on_imp_continuous_on[OF g_holo] - by (auto simp add:continuous_on_def \r>0\) - moreover have "at z within ball z r \ bot" using \r>0\ - by (auto simp add:trivial_limit_within islimpt_ball) - ultimately have "g z=0" by (auto intro: tendsto_unique) - thus False using asm \r>0\ by auto - qed - ultimately show "n=m" by fastforce + show "winding_number g w = 0" when"w \ s - {z}" for w + proof - + have "winding_number g w = 0" when "w\s" using that e2_cball + apply (intro winding_number_zero_outside[OF _ _ _ _ path_img]) + by (auto simp add:g_def l_def) + moreover have "winding_number g z=0" + proof - + let ?Wz="\g. winding_number g z" + have "?Wz g = ?Wz (circlepath z e2) + ?Wz l + ?Wz (reversepath (circlepath z e1)) + + ?Wz (reversepath l)" + using \e2>0\ \e1>0\ zl_img unfolding g_def l_def + by (subst winding_number_join,auto simp add:path_image_join closed_segment_commute)+ + also have "... = ?Wz (circlepath z e2) + ?Wz (reversepath (circlepath z e1))" + using zl_img + apply (subst (2) winding_number_reversepath) + by (auto simp add:l_def closed_segment_commute) + also have "... = 0" + proof - + have "?Wz (circlepath z e2) = 1" using \e2>0\ + by (auto intro: winding_number_circlepath_centre) + moreover have "?Wz (reversepath (circlepath z e1)) = -1" using \e1>0\ + apply (subst winding_number_reversepath) + by (auto intro: winding_number_circlepath_centre) + ultimately show ?thesis by auto + qed + finally show ?thesis . + qed + ultimately show ?thesis using that by auto + qed + qed + then have "0 = ?ig g" using contour_integral_unique by simp + also have "... = ?ig (circlepath z e2) + ?ig l + ?ig (reversepath (circlepath z e1)) + + ?ig (reversepath l)" + unfolding g_def + by (auto simp add:contour_integrable_reversepath_eq) + also have "... = ?ig (circlepath z e2) - ?ig (circlepath z e1)" + by (auto simp add:contour_integral_reversepath) + finally show "contour_integral (circlepath z e2) f = contour_integral (circlepath z e1) f" + by simp qed -lemma holomorphic_factor_zero_Ex1: - assumes "open s" "connected s" "z \ s" and - holo:"f holomorphic_on s" - and "f z = 0" and "\w\s. f w \ 0" - shows "\!n. \g r. 0 < n \ 0 < r \ - g holomorphic_on cball z r - \ (\w\cball z r. f w = (w-z)^n * g w \ g w\0)" -proof (rule ex_ex1I) - obtain g r n where "0 < n" "0 < r" "ball z r \ s" and - g:"g holomorphic_on ball z r" - "\w. w \ ball z r \ f w = (w - z) ^ n * g w" - "\w. w \ ball z r \ g w \ 0" - using holomorphic_factor_zero_nonconstant[OF holo \open s\ \connected s\ \z\s\ \f z=0\] - by (metis assms(3) assms(5) assms(6)) - define r' where "r' = r/2" - have "cball z r' \ ball z r" unfolding r'_def by (simp add: \0 < r\ cball_subset_ball_iff) - hence "cball z r' \ s" "g holomorphic_on cball z r'" - "(\w\cball z r'. f w = (w - z) ^ n * g w \ g w \ 0)" - using g \ball z r \ s\ by auto - moreover have "r'>0" unfolding r'_def using \0 by auto - ultimately show "\n g r. 0 < n \ 0 < r \ g holomorphic_on cball z r - \ (\w\cball z r. f w = (w - z) ^ n * g w \ g w \ 0)" - apply (intro exI[of _ n] exI[of _ g] exI[of _ r']) - by (simp add:\0 < n\) -next - fix m n - define fac where "fac n g r \ (\w\cball z r. f w = (w - z) ^ n * g w \ g w \ 0)" for n g r - assume n_asm:"\g r1. 0 < n \ 0 < r1 \ g holomorphic_on cball z r1 \ fac n g r1" - and m_asm:"\h r2. 0 < m \ 0 < r2 \ h holomorphic_on cball z r2 \ fac m h r2" - obtain g r1 where "0 < n" "0 < r1" and g_holo: "g holomorphic_on cball z r1" - and "fac n g r1" using n_asm by auto - obtain h r2 where "0 < m" "0 < r2" and h_holo: "h holomorphic_on cball z r2" - and "fac m h r2" using m_asm by auto - define r where "r = min r1 r2" - have "r>0" using \r1>0\ \r2>0\ unfolding r_def by auto - moreover have "\w\ball z r. f w = (w-z)^n * g w \ g w\0 \ f w = (w - z)^m * h w \ h w\0" - using \fac m h r2\ \fac n g r1\ unfolding fac_def r_def - by fastforce - ultimately show "m=n" using g_holo h_holo - apply (elim holomorphic_factor_zero_unique[of r z f n g m h,symmetric,rotated]) - by (auto simp add:r_def) +lemma base_residue: + assumes "open s" "z\s" "r>0" and f_holo:"f holomorphic_on (s - {z})" + and r_cball:"cball z r \ s" + shows "(f has_contour_integral 2*pi*ii* (residue f z)) (circlepath z r)" +proof - + obtain e where "e>0" and e_cball:"cball z e \ s" + using open_contains_cball[of s] \open s\ \z\s\ by auto + define c where "c \ 2*pi*ii" + define i where "i \ contour_integral (circlepath z e) f / c" + have "(f has_contour_integral c*i) (circlepath z \)" when "\>0" "\ + proof - + have "contour_integral (circlepath z e) f = contour_integral (circlepath z \) f" + "f contour_integrable_on circlepath z \" + "f contour_integrable_on circlepath z e" + using \\ + by (intro contour_integral_circlepath_eq[OF \open s\ f_holo \\>0\ _ e_cball],auto)+ + then show ?thesis unfolding i_def c_def + by (auto intro:has_contour_integral_integral) + qed + then have "\e>0. \\>0. \ (f has_contour_integral c * (residue f z)) (circlepath z \)" + unfolding residue_def c_def + apply (rule_tac someI[of _ i],intro exI[where x=e]) + by (auto simp add:\e>0\ c_def) + then obtain e' where "e'>0" + and e'_def:"\\>0. \ (f has_contour_integral c * (residue f z)) (circlepath z \)" + by auto + let ?int="\e. contour_integral (circlepath z e) f" + def \\"Min {r,e'} / 2" + have "\>0" "\\r" "\r>0\ \e'>0\ unfolding \_def by auto + have "(f has_contour_integral c * (residue f z)) (circlepath z \)" + using e'_def[rule_format,OF \\>0\ \\] . + then show ?thesis unfolding c_def + using contour_integral_circlepath_eq[OF \open s\ f_holo \\>0\ \\\r\ r_cball] + by (auto elim: has_contour_integral_eqpath[of _ _ "circlepath z \" "circlepath z r"]) +qed + + +lemma residue_holo: + assumes "open s" "z \ s" and f_holo: "f holomorphic_on s" + shows "residue f z = 0" +proof - + define c where "c \ 2 * pi * \" + obtain e where "e>0" and e_cball:"cball z e \ s" using \open s\ \z\s\ + using open_contains_cball_eq by blast + have "(f has_contour_integral c*residue f z) (circlepath z e)" + using f_holo + by (auto intro: base_residue[OF \open s\ \z\s\ \e>0\ _ e_cball,folded c_def]) + moreover have "(f has_contour_integral 0) (circlepath z e)" + using f_holo e_cball \e>0\ + by (auto intro: Cauchy_theorem_convex_simple[of _ "cball z e"]) + ultimately have "c*residue f z =0" + using has_contour_integral_unique by blast + thus ?thesis unfolding c_def by auto qed -lemma finite_ball_avoid: - assumes "open s" "finite pts" - shows "\p\s. \e>0. \w\ball p e. w\s \ (w\p \ w\pts)" -proof - fix p assume "p\s" - then obtain e1 where "0 < e1" and e1_b:"ball p e1 \ s" - using open_contains_ball_eq[OF \open s\] by auto - obtain e2 where "0x\pts. x \ p \ e2 \ dist p x" - using finite_set_avoid[OF \finite pts\,of p] by auto - hence "\w\ball p (min e1 e2). w\s \ (w\p \ w\pts)" using e1_b by auto - thus "\e>0. \w\ball p e. w \ s \ (w \ p \ w \ pts)" using \e2>0\ \e1>0\ - apply (rule_tac x="min e1 e2" in exI) - by auto + +lemma residue_const:"residue (\_. c) z = 0" + by (intro residue_holo[of "UNIV::complex set"],auto intro:holomorphic_intros) + + +lemma residue_add: + assumes "open s" "z \ s" and f_holo: "f holomorphic_on s - {z}" + and g_holo:"g holomorphic_on s - {z}" + shows "residue (\z. f z + g z) z= residue f z + residue g z" +proof - + define c where "c \ 2 * pi * \" + define fg where "fg \ (\z. f z+g z)" + obtain e where "e>0" and e_cball:"cball z e \ s" using \open s\ \z\s\ + using open_contains_cball_eq by blast + have "(fg has_contour_integral c * residue fg z) (circlepath z e)" + unfolding fg_def using f_holo g_holo + apply (intro base_residue[OF \open s\ \z\s\ \e>0\ _ e_cball,folded c_def]) + by (auto intro:holomorphic_intros) + moreover have "(fg has_contour_integral c*residue f z + c* residue g z) (circlepath z e)" + unfolding fg_def using f_holo g_holo + by (auto intro: has_contour_integral_add base_residue[OF \open s\ \z\s\ \e>0\ _ e_cball,folded c_def]) + ultimately have "c*(residue f z + residue g z) = c * residue fg z" + using has_contour_integral_unique by (auto simp add:distrib_left) + thus ?thesis unfolding fg_def + by (auto simp add:c_def) qed -lemma finite_cball_avoid: - fixes s :: "'a :: euclidean_space set" - assumes "open s" "finite pts" - shows "\p\s. \e>0. \w\cball p e. w\s \ (w\p \ w\pts)" -proof - fix p assume "p\s" - then obtain e1 where "e1>0" and e1: "\w\ball p e1. w\s \ (w\p \ w\pts)" - using finite_ball_avoid[OF assms] by auto - define e2 where "e2 = e1/2" - have "e2>0" and "e2e1>0\ by auto - then have "cball p e2 \ ball p e1" by (subst cball_subset_ball_iff,auto) - then show "\e>0. \w\cball p e. w \ s \ (w \ p \ w \ pts)" using \e2>0\ e1 by auto + +lemma residue_lmul: + assumes "open s" "z \ s" and f_holo: "f holomorphic_on s - {z}" + shows "residue (\z. c * (f z)) z= c * residue f z" +proof (cases "c=0") + case True + thus ?thesis using residue_const by auto +next + case False + def c'\"2 * pi * \" + def f'\"(\z. c * (f z))" + obtain e where "e>0" and e_cball:"cball z e \ s" using \open s\ \z\s\ + using open_contains_cball_eq by blast + have "(f' has_contour_integral c' * residue f' z) (circlepath z e)" + unfolding f'_def using f_holo + apply (intro base_residue[OF \open s\ \z\s\ \e>0\ _ e_cball,folded c'_def]) + by (auto intro:holomorphic_intros) + moreover have "(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)" + unfolding f'_def using f_holo + by (auto intro: has_contour_integral_lmul + base_residue[OF \open s\ \z\s\ \e>0\ _ e_cball,folded c'_def]) + ultimately have "c' * residue f' z = c * (c' * residue f z)" + using has_contour_integral_unique by auto + thus ?thesis unfolding f'_def c'_def using False + by (auto simp add:field_simps) qed +lemma residue_rmul: + assumes "open s" "z \ s" and f_holo: "f holomorphic_on s - {z}" + shows "residue (\z. (f z) * c) z= residue f z * c" +using residue_lmul[OF assms,of c] by (auto simp add:algebra_simps) + +lemma residue_div: + assumes "open s" "z \ s" and f_holo: "f holomorphic_on s - {z}" + shows "residue (\z. (f z) / c) z= residue f z / c " +using residue_lmul[OF assms,of "1/c"] by (auto simp add:algebra_simps) + +lemma residue_neg: + assumes "open s" "z \ s" and f_holo: "f holomorphic_on s - {z}" + shows "residue (\z. - (f z)) z= - residue f z" +using residue_lmul[OF assms,of "-1"] by auto + +lemma residue_diff: + assumes "open s" "z \ s" and f_holo: "f holomorphic_on s - {z}" + and g_holo:"g holomorphic_on s - {z}" + shows "residue (\z. f z - g z) z= residue f z - residue g z" +using residue_add[OF assms(1,2,3),of "\z. - g z"] residue_neg[OF assms(1,2,4)] +by (auto intro:holomorphic_intros g_holo) + +lemma residue_simple: + assumes "open s" "z\s" and f_holo:"f holomorphic_on s" + shows "residue (\w. f w / (w - z)) z = f z" +proof - + define c where "c \ 2 * pi * \" + def f'\"\w. f w / (w - z)" + obtain e where "e>0" and e_cball:"cball z e \ s" using \open s\ \z\s\ + using open_contains_cball_eq by blast + have "(f' has_contour_integral c * f z) (circlepath z e)" + unfolding f'_def c_def using \e>0\ f_holo e_cball + by (auto intro!: Cauchy_integral_circlepath_simple holomorphic_intros) + moreover have "(f' has_contour_integral c * residue f' z) (circlepath z e)" + unfolding f'_def using f_holo + apply (intro base_residue[OF \open s\ \z\s\ \e>0\ _ e_cball,folded c_def]) + by (auto intro!:holomorphic_intros) + ultimately have "c * f z = c * residue f' z" + using has_contour_integral_unique by blast + thus ?thesis unfolding c_def f'_def by auto +qed + + + +subsubsection \Cauchy's residue theorem\ + lemma get_integrable_path: assumes "open s" "connected (s-pts)" "finite pts" "f holomorphic_on (s-pts) " "a\s-pts" "b\s-pts" obtains g where "valid_path g" "pathstart g = a" "pathfinish g = b" "path_image g \ s-pts" "f contour_integrable_on g" using assms -proof (induct arbitrary:s thesis a rule:finite_induct[OF \finite pts\]) print_cases +proof (induct arbitrary:s thesis a rule:finite_induct[OF \finite pts\]) case 1 obtain g where "valid_path g" "path_image g \ s" "pathstart g = a" "pathfinish g = b" using connected_open_polynomial_connected[OF \open s\,of a b ] \connected (s - {})\ @@ -2299,42 +2449,42 @@ next case idt:(2 p pts) obtain e where "e>0" and e:"\w\ball a e. w \ s \ (w \ a \ w \ insert p pts)" - using finite_ball_avoid[OF \open s\ \finite (insert p pts)\,rule_format,of a] + using finite_ball_avoid[OF \open s\ \finite (insert p pts)\, of a] \a \ s - insert p pts\ by auto - define a' where "a' = a+e/2" + define a' where "a' \ a+e/2" have "a'\s-{p} -pts" using e[rule_format,of "a+e/2"] \e>0\ by (auto simp add:dist_complex_def a'_def) then obtain g' where g'[simp]:"valid_path g'" "pathstart g' = a'" "pathfinish g' = b" "path_image g' \ s - {p} - pts" "f contour_integrable_on g'" using idt.hyps(3)[of a' "s-{p}"] idt.prems idt.hyps(1) by (metis Diff_insert2 open_delete) - define g where "g = linepath a a' +++ g'" + define g where "g \ linepath a a' +++ g'" have "valid_path g" unfolding g_def by (auto intro: valid_path_join) moreover have "pathstart g = a" and "pathfinish g = b" unfolding g_def by auto moreover have "path_image g \ s - insert p pts" unfolding g_def - proof (rule subset_path_image_join) - have "closed_segment a a' \ ball a e" using \e>0\ - by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute) - then show "path_image (linepath a a') \ s - insert p pts" using e idt(9) - by auto - next - show "path_image g' \ s - insert p pts" using g'(4) by blast - qed + proof (rule subset_path_image_join) + have "closed_segment a a' \ ball a e" using \e>0\ + by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute) + then show "path_image (linepath a a') \ s - insert p pts" using e idt(9) + by auto + next + show "path_image g' \ s - insert p pts" using g'(4) by blast + qed moreover have "f contour_integrable_on g" - proof - - have "closed_segment a a' \ ball a e" using \e>0\ - by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute) - then have "continuous_on (closed_segment a a') f" - using e idt.prems(6) holomorphic_on_imp_continuous_on[OF idt.prems(5)] - apply (elim continuous_on_subset) - by auto - then have "f contour_integrable_on linepath a a'" - using contour_integrable_continuous_linepath by auto - then show ?thesis unfolding g_def - apply (rule contour_integrable_joinI) - by (auto simp add: \e>0\) - qed + proof - + have "closed_segment a a' \ ball a e" using \e>0\ + by (auto dest!:segment_bound1 simp:a'_def dist_complex_def norm_minus_commute) + then have "continuous_on (closed_segment a a') f" + using e idt.prems(6) holomorphic_on_imp_continuous_on[OF idt.prems(5)] + apply (elim continuous_on_subset) + by auto + then have "f contour_integrable_on linepath a a'" + using contour_integrable_continuous_linepath by auto + then show ?thesis unfolding g_def + apply (rule contour_integrable_joinI) + by (auto simp add: \e>0\) + qed ultimately show ?case using idt.prems(1)[of g] by auto qed @@ -2376,10 +2526,10 @@ obtain n::int where "n=winding_number g p" using integer_winding_number[OF _ g_loop,of p] valid path_img by (metis DiffD2 Ints_cases insertI1 subset_eq valid_path_imp_path) - define p_circ where "p_circ = circlepath p (h p)" - define p_circ_pt where "p_circ_pt = linepath (p+h p) (p+h p)" - define n_circ where "n_circ n = (op +++ p_circ ^^ n) p_circ_pt" for n - define cp where "cp = (if n\0 then reversepath (n_circ (nat n)) else n_circ (nat (- n)))" + define p_circ where "p_circ \ circlepath p (h p)" + define p_circ_pt where "p_circ_pt \ linepath (p+h p) (p+h p)" + define n_circ where "n_circ \ \n. (op +++ p_circ ^^ n) p_circ_pt" + define cp where "cp \ if n\0 then reversepath (n_circ (nat n)) else n_circ (nat (- n))" have n_circ:"valid_path (n_circ k)" "winding_number (n_circ k) p = k" "pathstart (n_circ k) = p + h p" "pathfinish (n_circ k) = p + h p" @@ -2467,7 +2617,7 @@ ultimately show ?thesis unfolding n_Suc apply (subst winding_number_join) - by (auto simp: pcirc Suc that not_in_path_image_join Suc.hyps(7)[OF that]) + by (auto simp: valid_path_imp_path pcirc Suc that not_in_path_image_join Suc.hyps(7)[OF that]) qed show "f contour_integrable_on (n_circ (Suc k))" unfolding n_Suc @@ -2495,13 +2645,14 @@ using n_circ(5) by auto next show "winding_number cp p = - n" - unfolding cp_def using winding_number_reversepath n_circ \h p>0\ by auto + unfolding cp_def using winding_number_reversepath n_circ \h p>0\ + by (auto simp: valid_path_imp_path) next show "winding_number cp p'=0 \ p' \ path_image cp" when "p'\s - pts" for p' unfolding cp_def apply (auto) apply (subst winding_number_reversepath) - by (auto simp add: n_circ(7)[OF that] n_circ(1)) + by (auto simp add: valid_path_imp_path n_circ(7)[OF that] n_circ(1)) next show "f contour_integrable_on cp" unfolding cp_def using contour_integrable_reversepath_eq n_circ(1,8) by auto @@ -2510,7 +2661,7 @@ unfolding cp_def using contour_integral_reversepath[OF n_circ(1)] n_circ(9) by auto qed - define g' where "g' = g +++ pg +++ cp +++ (reversepath pg)" + def g'\"g +++ pg +++ cp +++ (reversepath pg)" have "contour_integral g' f = (\p\pts. winding_number g' p * contour_integral (circlepath p (h p)) f)" proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ \finite pts\ ]) show "connected (s - {p} - pts)" using connected by (metis Diff_insert2) @@ -2524,8 +2675,8 @@ unfolding g'_def cp_def using pg(2) by simp show "path_image g' \ s - {p} - pts" proof - - define s' where "s' = s - {p} - pts" - have s': "s' = s-insert p pts " unfolding s'_def by auto + def s'\"s - {p} - pts" + have s':"s' = s-insert p pts " unfolding s'_def by auto then show ?thesis using path_img pg(4) cp(4) unfolding g'_def apply (fold s'_def s') @@ -2539,9 +2690,10 @@ have "winding_number (g +++ pg +++ cp +++ reversepath pg) z = winding_number g z + winding_number (pg +++ cp +++ (reversepath pg)) z" proof (rule winding_number_join) - show "path g" using \valid_path g\ by simp + show "path g" using \valid_path g\ by (simp add: valid_path_imp_path) show "z \ path_image g" using z path_img by auto - show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp by auto + show "path (pg +++ cp +++ reversepath pg)" using pg(3) cp + by (simp add: valid_path_imp_path) next have "path_image (pg +++ cp +++ reversepath pg) \ s - insert p pts" using pg(4) cp(4) by (auto simp:subset_path_image_join) @@ -2553,7 +2705,8 @@ + winding_number (cp +++ (reversepath pg)) z)" proof (subst add_left_cancel,rule winding_number_join) show "path pg" and "path (cp +++ reversepath pg)" - and "pathfinish pg = pathstart (cp +++ reversepath pg)" by auto + and "pathfinish pg = pathstart (cp +++ reversepath pg)" + by (auto simp add: valid_path_imp_path) show "z \ path_image pg" using pg(4) z by blast show "z \ path_image (cp +++ reversepath pg)" using z by (metis Diff_iff \z \ path_image pg\ contra_subsetD cp(4) insertI1 @@ -2561,12 +2714,12 @@ qed also have "... = winding_number g z + (winding_number pg z + (winding_number cp z + winding_number (reversepath pg) z))" - apply (auto intro!:winding_number_join ) + apply (auto intro!:winding_number_join simp: valid_path_imp_path) apply (metis Diff_iff contra_subsetD cp(4) insertI1 singletonD z) by (metis Diff_insert2 Diff_subset contra_subsetD pg(4) z) also have "... = winding_number g z + winding_number cp z" apply (subst winding_number_reversepath) - apply auto + apply (auto simp: valid_path_imp_path) by (metis Diff_iff contra_subsetD insertI1 pg(4) singletonD z) finally have "winding_number g' z = winding_number g z + winding_number cp z" unfolding g'_def . @@ -2612,22 +2765,22 @@ have "winding_number g' p' = winding_number g p' + winding_number (pg +++ cp +++ reversepath pg) p'" unfolding g'_def apply (subst winding_number_join) - apply simp_all + apply (simp_all add: valid_path_imp_path) apply (intro not_in_path_image_join) by auto also have "... = winding_number g p' + winding_number pg p' + winding_number (cp +++ reversepath pg) p'" apply (subst winding_number_join) - apply simp_all + apply (simp_all add: valid_path_imp_path) apply (intro not_in_path_image_join) by auto also have "... = winding_number g p' + winding_number pg p'+ winding_number cp p' + winding_number (reversepath pg) p'" apply (subst winding_number_join) - by simp_all + by (simp_all add: valid_path_imp_path) also have "... = winding_number g p' + winding_number cp p'" apply (subst winding_number_reversepath) - by auto + by (simp_all add: valid_path_imp_path) also have "... = winding_number g p'" using that by auto finally show ?thesis . qed @@ -2637,9 +2790,8 @@ by (auto simp add:setsum.insert[OF \finite pts\ \p\pts\] algebra_simps) qed - lemma Cauchy_theorem_singularities: - assumes "open s" "connected (s-pts)" "finite pts" and + assumes "open s" "connected s" "finite pts" and holo:"f holomorphic_on s-pts" and "valid_path g" and loop:"pathfinish g = pathstart g" and @@ -2649,15 +2801,17 @@ shows "contour_integral g f = (\p\pts. winding_number g p * contour_integral (circlepath p (h p)) f)" (is "?L=?R") proof - - define circ - where [abs_def]: "circ p = winding_number g p * contour_integral (circlepath p (h p)) f" for p - define pts1 where "pts1 = pts \ s" - define pts2 where "pts2 = pts - pts1" + define circ where "circ \ \p. winding_number g p * contour_integral (circlepath p (h p)) f" + define pts1 where "pts1 \ pts \ s" + define pts2 where "pts2 \ pts - pts1" have "pts=pts1 \ pts2" "pts1 \ pts2 = {}" "pts2 \ s={}" "pts1\s" unfolding pts1_def pts2_def by auto have "contour_integral g f = (\p\pts1. circ p)" unfolding circ_def proof (rule Cauchy_theorem_aux[OF \open s\ _ _ \pts1\s\ _ \valid_path g\ loop _ homo]) - show "connected (s - pts1)" by (metis Diff_Int2 Int_absorb assms(2) pts1_def) + have "finite pts1" unfolding pts1_def using \finite pts\ by auto + then show "connected (s - pts1)" + using \open s\ \connected s\ connected_open_delete_finite[of s] by auto + next show "finite pts1" using \pts = pts1 \ pts2\ assms(3) by auto show "f holomorphic_on s - pts1" by (metis Diff_Int2 Int_absorb holo pts1_def) show "path_image g \ s - pts1" using assms(7) pts1_def by auto @@ -2681,6 +2835,88 @@ by auto qed +lemma Residue_theorem: + fixes s pts::"complex set" and f::"complex \ complex" + and g::"real \ complex" + assumes "open s" "connected s" "finite pts" and + holo:"f holomorphic_on s-pts" and + "valid_path g" and + loop:"pathfinish g = pathstart g" and + "path_image g \ s-pts" and + homo:"\z. (z \ s) \ winding_number g z = 0" + shows "contour_integral g f = 2 * pi * \ *(\p\pts. winding_number g p * residue f p)" +proof - + define c where "c \ 2 * pi * \" + obtain h where avoid:"\p\s. h p>0 \ (\w\cball p (h p). w\s \ (w\p \ w \ pts))" + using finite_cball_avoid[OF \open s\ \finite pts\] by metis + have "contour_integral g f + = (\p\pts. winding_number g p * contour_integral (circlepath p (h p)) f)" + using Cauchy_theorem_singularities[OF assms avoid] . + also have "... = (\p\pts. c * winding_number g p * residue f p)" + proof (intro setsum.cong) + show "pts = pts" by simp + next + fix x assume "x \ pts" + show "winding_number g x * contour_integral (circlepath x (h x)) f + = c * winding_number g x * residue f x" + proof (cases "x\s") + case False + then have "winding_number g x=0" using homo by auto + thus ?thesis by auto + next + case True + have "contour_integral (circlepath x (h x)) f = c* residue f x" + using \x\pts\ \finite pts\ avoid[rule_format,OF True] + apply (intro base_residue[of "s-(pts-{x})",THEN contour_integral_unique,folded c_def]) + by (auto intro:holomorphic_on_subset[OF holo] open_Diff[OF \open s\ finite_imp_closed]) + then show ?thesis by auto + qed + qed + also have "... = c * (\p\pts. winding_number g p * residue f p)" + by (simp add: setsum_right_distrib algebra_simps) + finally show ?thesis unfolding c_def . +qed + +subsection \The argument principle\ + +definition is_pole :: "('a::topological_space \ 'b::real_normed_vector) \ 'a \ bool" where + "is_pole f a = (LIM x (at a). f x :> at_infinity)" + +lemma is_pole_tendsto: + fixes f::"('a::topological_space \ 'b::real_normed_div_algebra)" + shows "is_pole f x \ ((inverse o f) \ 0) (at x)" +unfolding is_pole_def +by (auto simp add:filterlim_inverse_at_iff[symmetric] comp_def filterlim_at) + +lemma is_pole_inverse_holomorphic: + assumes "open s" + and f_holo:"f holomorphic_on (s-{z})" + and pole:"is_pole f z" + and non_z:"\x\s-{z}. f x\0" + shows "(\x. if x=z then 0 else inverse (f x)) holomorphic_on s" +proof - + define g where "g \ \x. if x=z then 0 else inverse (f x)" + have "isCont g z" unfolding isCont_def using is_pole_tendsto[OF pole] + apply (subst Lim_cong_at[where b=z and y=0 and g="inverse \ f"]) + by (simp_all add:g_def) + moreover have "continuous_on (s-{z}) f" using f_holo holomorphic_on_imp_continuous_on by auto + hence "continuous_on (s-{z}) (inverse o f)" unfolding comp_def + by (auto elim!:continuous_on_inverse simp add:non_z) + hence "continuous_on (s-{z}) g" unfolding g_def + apply (subst continuous_on_cong[where t="s-{z}" and g="inverse o f"]) + by auto + ultimately have "continuous_on s g" using open_delete[OF \open s\] \open s\ + by (auto simp add:continuous_on_eq_continuous_at) + moreover have "(inverse o f) holomorphic_on (s-{z})" + unfolding comp_def using f_holo + by (auto elim!:holomorphic_on_inverse simp add:non_z) + hence "g holomorphic_on (s-{z})" + apply (subst holomorphic_cong[where t="s-{z}" and g="inverse o f"]) + by (auto simp add:g_def) + ultimately show ?thesis unfolding g_def using \open s\ + by (auto elim!: no_isolated_singularity) +qed + (*order of the zero of f at z*) definition zorder::"(complex \ complex) \ complex \ nat" where @@ -2693,17 +2929,126 @@ (*order of the pole of f at z*) definition porder::"(complex \ complex) \ complex \ nat" where - "porder f z = zorder (inverse o f) z" + "porder f z = (let f'=(\x. if x=z then 0 else inverse (f x)) in zorder f' z)" definition pol_poly::"[complex \ complex,complex]\complex \ complex" where - "pol_poly f z = inverse o zer_poly (inverse o f) z" + "pol_poly f z = (let f'=(\ x. if x=z then 0 else inverse (f x)) + in inverse o zer_poly f' z)" + -definition residue::"(complex \ complex) \ complex \ complex" where - "residue f z = (let n=porder f z;h=pol_poly f z in (deriv ^^ (n - 1)) h z / fact (n-1))" +lemma holomorphic_factor_zero_unique: + fixes f::"complex \ complex" and z::complex and r::real + assumes "r>0" + and asm:"\w\ball z r. f w = (w-z)^n * g w \ g w\0 \ f w = (w - z)^m * h w \ h w\0" + and g_holo:"g holomorphic_on ball z r" and h_holo:"h holomorphic_on ball z r" + shows "n=m" +proof - + have "n>m \ False" + proof - + assume "n>m" + have "(h \ 0) (at z within ball z r)" + proof (rule Lim_transform_within[OF _ \r>0\, where f="\w. (w - z) ^ (n - m) * g w"]) + have "\w\ball z r. w\z \ h w = (w-z)^(n-m) * g w" using \n>m\ asm + by (auto simp add:field_simps power_diff) + then show "\x' \ ball z r; 0 < dist x' z;dist x' z < r\ + \ (x' - z) ^ (n - m) * g x' = h x'" for x' by auto + next + define F where "F \ at z within ball z r" + define f' where "f' \ \x. (x - z) ^ (n-m)" + have "f' z=0" using \n>m\ unfolding f'_def by auto + moreover have "continuous F f'" unfolding f'_def F_def + by (intro continuous_intros) + ultimately have "(f' \ 0) F" unfolding F_def + by (simp add: continuous_within) + moreover have "(g \ g z) F" + using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] \r>0\ + unfolding F_def by auto + ultimately show " ((\w. f' w * g w) \ 0) F" using tendsto_mult by fastforce + qed + moreover have "(h \ h z) (at z within ball z r)" + using holomorphic_on_imp_continuous_on[OF h_holo] + by (auto simp add:continuous_on_def \r>0\) + moreover have "at z within ball z r \ bot" using \r>0\ + by (auto simp add:trivial_limit_within islimpt_ball) + ultimately have "h z=0" by (auto intro: tendsto_unique) + thus False using asm \r>0\ by auto + qed + moreover have "m>n \ False" + proof - + assume "m>n" + have "(g \ 0) (at z within ball z r)" + proof (rule Lim_transform_within[OF _ \r>0\, where f="\w. (w - z) ^ (m - n) * h w"]) + have "\w\ball z r. w\z \ g w = (w-z)^(m-n) * h w" using \m>n\ asm + by (auto simp add:field_simps power_diff) + then show "\x' \ ball z r; 0 < dist x' z;dist x' z < r\ + \ (x' - z) ^ (m - n) * h x' = g x'" for x' by auto + next + define F where "F \ at z within ball z r" + define f' where "f' \\x. (x - z) ^ (m-n)" + have "f' z=0" using \m>n\ unfolding f'_def by auto + moreover have "continuous F f'" unfolding f'_def F_def + by (intro continuous_intros) + ultimately have "(f' \ 0) F" unfolding F_def + by (simp add: continuous_within) + moreover have "(h \ h z) F" + using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] \r>0\ + unfolding F_def by auto + ultimately show " ((\w. f' w * h w) \ 0) F" using tendsto_mult by fastforce + qed + moreover have "(g \ g z) (at z within ball z r)" + using holomorphic_on_imp_continuous_on[OF g_holo] + by (auto simp add:continuous_on_def \r>0\) + moreover have "at z within ball z r \ bot" using \r>0\ + by (auto simp add:trivial_limit_within islimpt_ball) + ultimately have "g z=0" by (auto intro: tendsto_unique) + thus False using asm \r>0\ by auto + qed + ultimately show "n=m" by fastforce +qed -definition is_pole:: "(complex \ complex) \ complex \bool" where - "is_pole f p \ isCont (inverse o f) p \ f p = 0" +lemma holomorphic_factor_zero_Ex1: + assumes "open s" "connected s" "z \ s" and + holo:"f holomorphic_on s" + and "f z = 0" and "\w\s. f w \ 0" + shows "\!n. \g r. 0 < n \ 0 < r \ + g holomorphic_on cball z r + \ (\w\cball z r. f w = (w-z)^n * g w \ g w\0)" +proof (rule ex_ex1I) + obtain g r n where "0 < n" "0 < r" "ball z r \ s" and + g:"g holomorphic_on ball z r" + "\w. w \ ball z r \ f w = (w - z) ^ n * g w" + "\w. w \ ball z r \ g w \ 0" + using holomorphic_factor_zero_nonconstant[OF holo \open s\ \connected s\ \z\s\ \f z=0\] + by (metis assms(3) assms(5) assms(6)) + def r'\"r/2" + have "cball z r' \ ball z r" unfolding r'_def by (simp add: \0 < r\ cball_subset_ball_iff) + hence "cball z r' \ s" "g holomorphic_on cball z r'" + "(\w\cball z r'. f w = (w - z) ^ n * g w \ g w \ 0)" + using g \ball z r \ s\ by auto + moreover have "r'>0" unfolding r'_def using \0 by auto + ultimately show "\n g r. 0 < n \ 0 < r \ g holomorphic_on cball z r + \ (\w\cball z r. f w = (w - z) ^ n * g w \ g w \ 0)" + apply (intro exI[of _ n] exI[of _ g] exI[of _ r']) + by (simp add:\0 < n\) +next + fix m n + define fac where "fac \ \n g r. \w\cball z r. f w = (w - z) ^ n * g w \ g w \ 0" + assume n_asm:"\g r1. 0 < n \ 0 < r1 \ g holomorphic_on cball z r1 \ fac n g r1" + and m_asm:"\h r2. 0 < m \ 0 < r2 \ h holomorphic_on cball z r2 \ fac m h r2" + obtain g r1 where "0 < n" "0 < r1" and g_holo: "g holomorphic_on cball z r1" + and "fac n g r1" using n_asm by auto + obtain h r2 where "0 < m" "0 < r2" and h_holo: "h holomorphic_on cball z r2" + and "fac m h r2" using m_asm by auto + define r where "r \ min r1 r2" + have "r>0" using \r1>0\ \r2>0\ unfolding r_def by auto + moreover have "\w\ball z r. f w = (w-z)^n * g w \ g w\0 \ f w = (w - z)^m * h w \ h w\0" + using \fac m h r2\ \fac n g r1\ unfolding fac_def r_def + by fastforce + ultimately show "m=n" using g_holo h_holo + apply (elim holomorphic_factor_zero_unique[of r z f n g m h,symmetric,rotated]) + by (auto simp add:r_def) +qed lemma zorder_exist: fixes f::"complex \ complex" and z::complex @@ -2714,8 +3059,8 @@ shows "\r. n>0 \ r>0 \ cball z r \ s \ h holomorphic_on cball z r \ (\w\cball z r. f w = h w * (w-z)^n \ h w \0) " proof - - define P where "P h r n \ r>0 \ h holomorphic_on cball z r - \ (\w\cball z r. ( f w = h w * (w-z)^n) \ h w \0)" for h r n + define P where "P \ \h r n. r>0 \ h holomorphic_on cball z r + \ (\w\cball z r. ( f w = h w * (w-z)^n) \ h w \0)" have "(\!n. n>0 \ (\ h r. P h r n))" proof - have "\!n. \h r. n>0 \ P h r n" @@ -2739,7 +3084,7 @@ then obtain r1 where "P h r1 n" by auto obtain r2 where "r2>0" "cball z r2 \ s" using assms(3) assms(5) open_contains_cball_eq by blast - define r3 where "r3 = min r1 r2" + define r3 where "r3 \ min r1 r2" have "P h r3 n" using \P h r1 n\ \r2>0\ unfolding P_def r3_def by auto moreover have "cball z r3 \ s" using \cball z r2 \ s\ unfolding r3_def by auto @@ -2748,279 +3093,185 @@ lemma porder_exist: fixes f::"complex \ complex" and z::complex - defines "n\porder f z" and "h\pol_poly f z" - assumes "open s" "connected s" "z\s" - and holo:"(inverse o f) holomorphic_on s" - and "f z=0" "\w\s. f w\0" + defines "n \ porder f z" and "h \ pol_poly f z" + assumes "open s" "z \ s" + and holo:"f holomorphic_on s-{z}" + and "is_pole f z" shows "\r. n>0 \ r>0 \ cball z r \ s \ h holomorphic_on cball z r - \ (\w\cball z r. f w = h w / (w-z)^n \ h w \0)" + \ (\w\cball z r. (w\z \ f w = h w / (w-z)^n) \ h w \0)" proof - - define zo where "zo = zorder (inverse \ f) z" - define zp where "zp = zer_poly (inverse \ f) z" - obtain r where "0 < zo" "0 < r" "cball z r \ s" and zp_holo: "zp holomorphic_on cball z r" and - zp_fac: "\w\cball z r. (inverse \ f) w = zp w * (w - z) ^ zo \ zp w \ 0" - using zorder_exist[OF \open s\ \connected s\ \z\s\ holo,folded zo_def zp_def] - \f z=0\ \\w\s. f w\0\ + obtain e where "e>0" and e_ball:"ball z e \ s"and e_def: "\x\ball z e-{z}. f x\0" + proof - + have "\\<^sub>F z in at z. f z \ 0" + using \is_pole f z\ filterlim_at_infinity_imp_eventually_ne unfolding is_pole_def + by auto + then obtain e1 where "e1>0" and e1_def: "\x. x \ z \ dist x z < e1 \ f x \ 0" + using eventually_at[of "\x. f x\0" z,simplified] by auto + obtain e2 where "e2>0" and "ball z e2 \s" using \open s\ \z\s\ openE by auto + define e where "e \ min e1 e2" + have "e>0" using \e1>0\ \e2>0\ unfolding e_def by auto + moreover have "ball z e \ s" unfolding e_def using \ball z e2 \ s\ by auto + moreover have "\x\ball z e-{z}. f x\0" using e1_def \e1>0\ \e2>0\ unfolding e_def + by (simp add: DiffD1 DiffD2 dist_commute singletonI) + ultimately show ?thesis using that by auto + qed + define g where "g \ \x. if x=z then 0 else inverse (f x)" + define zo where "zo \ zorder g z" + define zp where "zp \ zer_poly g z" + have "\w\ball z e. g w \ 0" + proof - + obtain w where w:"w\ball z e-{z}" using \0 < e\ + by (metis open_ball all_not_in_conv centre_in_ball insert_Diff_single + insert_absorb not_open_singleton) + hence "w\z" "f w\0" using e_def[rule_format,of w] mem_ball + by (auto simp add:dist_commute) + then show ?thesis unfolding g_def using w by auto + qed + moreover have "g holomorphic_on ball z e" + apply (intro is_pole_inverse_holomorphic[of "ball z e",OF _ _ \is_pole f z\ e_def,folded g_def]) + using holo e_ball by auto + moreover have "g z=0" unfolding g_def by auto + ultimately obtain r where "0 < zo" "0 < r" "cball z r \ ball z e" + and zp_holo: "zp holomorphic_on cball z r" and + zp_fac: "\w\cball z r. g w = zp w * (w - z) ^ zo \ zp w \ 0" + using zorder_exist[of "ball z e" z g,simplified,folded zo_def zp_def] \e>0\ by auto have n:"n=zo" and h:"h=inverse o zp" - unfolding n_def zo_def porder_def h_def zp_def pol_poly_def by simp_all + unfolding n_def zo_def porder_def h_def zp_def pol_poly_def g_def by simp_all have "h holomorphic_on cball z r" using zp_holo zp_fac holomorphic_on_inverse unfolding h comp_def by blast - moreover have "\w\cball z r. f w = h w / (w-z)^n \ h w \0" - using zp_fac unfolding h n comp_def + moreover have "\w\cball z r. (w\z \ f w = h w / (w-z)^n) \ h w \0" + using zp_fac unfolding h n comp_def g_def by (metis divide_inverse_commute field_class.field_inverse_zero inverse_inverse_eq inverse_mult_distrib mult.commute) moreover have "0 < n" unfolding n using \zo>0\ by simp - ultimately show ?thesis using \0 < r\ \cball z r \ s\ by auto -qed - -lemma base_residue: - fixes f::"complex \ complex" and z::complex - assumes "open s" "connected s" "z\s" - and holo: "(inverse o f) holomorphic_on s" - and "f z=0" - and non_c:"\w\s. f w\0" - shows "\r>0. cball z r \ s - \ (f has_contour_integral complex_of_real (2 * pi) * \ * residue f z) (circlepath z r)" -proof - - define n where "n = porder f z" - define h where "h = pol_poly f z" - obtain r where "n>0" "0 < r" and - r_b:"cball z r \ s" and - h_holo:"h holomorphic_on cball z r" - and h:"(\w\cball z r. f w = h w / (w - z) ^ n \ h w \ 0)" - using porder_exist[OF \open s\ \connected s\ \z\s\ holo \f z=0\ non_c] - unfolding n_def h_def by auto - define c where "c = complex_of_real (2 * pi) * \" - have "residue f z = (deriv ^^ (n - 1)) h z / fact (n-1)" - unfolding residue_def - apply (fold n_def h_def) - by simp - then have "((\u. h u / (u - z) ^ n) has_contour_integral c * residue f z) - (circlepath z r)" - using Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n -1" - ,unfolded Suc_diff_1[OF \n>0\],folded c_def] h_holo r_b - by (auto simp add:\r>0\ holomorphic_on_imp_continuous_on holomorphic_on_subset) - then have "(f has_contour_integral c * residue f z) (circlepath z r)" - proof (elim has_contour_integral_eq) - fix x assume "x \ path_image (circlepath z r)" - hence "x\cball z r" using \0 < r\ by auto - then show "h x / (x - z) ^ n = f x" using h by auto - qed - then show ?thesis using \r>0\ \cball z r \ s\ unfolding c_def by auto + ultimately show ?thesis using \0 < r\ \cball z r \ ball z e\ e_ball by auto qed -theorem residue_theorem: - assumes "open s" "connected (s-poles)" and - holo:"f holomorphic_on s-poles" and - "valid_path \" and - loop:"pathfinish \ = pathstart \" and - "path_image \ \ s-poles" and - homo:"\z. (z \ s) \ winding_number \ z = 0" and - "finite {p. f p=0}" and - poles:"\p\poles. is_pole f p" - shows "contour_integral \ f = 2 * pi * \ *(\p\poles. winding_number \ p * residue f p)" +lemma residue_porder: + fixes f::"complex \ complex" and z::complex + defines "n \ porder f z" and "h \ pol_poly f z" + assumes "open s" "z \ s" + and holo:"f holomorphic_on s - {z}" + and pole:"is_pole f z" + shows "residue f z = ((deriv ^^ (n - 1)) h z / fact (n-1))" proof - - define pts where "pts = {p. f p=0}" - define c where "c = 2 * complex_of_real pi * \ " - define contour - where "contour p e = (f has_contour_integral c * residue f p) (circlepath p e)" for p e - define avoid where "avoid p e \ (\w\cball p e. w \ s \ (w \ p \ w \ pts))" for p e - have "poles \ pts" and "finite pts" - using poles \finite {p. f p=0}\ unfolding pts_def is_pole_def by auto - have "\e>0. avoid p e \ (p\poles \ contour p e)" - when "p\s" for p - proof - - obtain e1 where e:"e1>0" and e:"avoid p e1" - using finite_cball_avoid[OF \open s\ \finite pts\] \p\s\ unfolding avoid_def by auto - have "\e2>0. cball p e2 \ ball p e1 \ contour p e2" - when "p\poles" unfolding c_def contour_def - proof (rule base_residue[of "ball p e1" p f,simplified,OF \e1>0\]) - show "inverse \ f holomorphic_on ball p e1" - proof - - define f' where "f' = inverse o f" - have "f holomorphic_on ball p e1 - {p}" - using holo e \poles \ pts\ unfolding avoid_def - apply (elim holomorphic_on_subset) - by auto - then have f'_holo:"f' holomorphic_on ball p e1 - {p}" unfolding f'_def comp_def - apply (elim holomorphic_on_inverse) - using e pts_def ball_subset_cball unfolding avoid_def by blast - moreover have "isCont f' p" using \p\poles\ poles unfolding f'_def is_pole_def by auto - ultimately show "f' holomorphic_on ball p e1" - apply (elim no_isolated_singularity[rotated]) - apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified]) - using field_differentiable_imp_continuous_at f'_holo - holomorphic_on_imp_differentiable_at by fastforce - qed - next - show "f p = 0" using \p\poles\ poles unfolding is_pole_def by auto - next - define p' where "p' = p+e1/2" - have "p'\ball p e1" and "p'\p" using \e1>0\ unfolding p'_def by (auto simp add:dist_norm) - then show "\w\ball p e1. f w \ 0" using e unfolding avoid_def - apply (rule_tac x=p' in bexI) - by (auto simp add:pts_def) - qed - then obtain e2 where e2:"p\poles \ e2>0 \ cball p e2 \ ball p e1 \ contour p e2" by auto - define e3 where "e3 = (if p\poles then e2 else e1)" - have "avoid p e3" - using e2 e that avoid_def e3_def by auto - moreover have "e3>0" using \e1>0\ e2 unfolding e3_def by auto - moreover have " p\poles \ contour p e3" using e2 unfolding e3_def by auto - ultimately show ?thesis by auto - qed - then obtain h where h:"\p\s. h p>0 \ (avoid p (h p) \ (p\poles \ contour p (h p)))" - by metis - define cont where "cont p = contour_integral (circlepath p (h p)) f" for p - have "contour_integral \ f = (\p\poles. winding_number \ p * cont p)" - unfolding cont_def - proof (rule Cauchy_theorem_singularities[OF \open s\ \connected (s-poles)\ _ holo \valid_path \\ - loop \path_image \ \ s-poles\ homo]) - show "finite poles" using \poles \ pts\ and \finite pts\ by (simp add: finite_subset) - next - show "\p\s. 0 < h p \ (\w\cball p (h p). w \ s \ (w \ p \ w \ poles))" - using \poles \ pts\ h unfolding avoid_def by blast - qed - also have "... = (\p\poles. c * (winding_number \ p * residue f p))" - proof (rule setsum.cong[of poles poles,simplified]) - fix p assume "p \ poles" - show "winding_number \ p * cont p = c * (winding_number \ p * residue f p)" - proof (cases "p\s") - assume "p \ s" - then have "cont p=c*residue f p" - unfolding cont_def - apply (intro contour_integral_unique) - using h[unfolded contour_def] \p \ poles\ by blast - then show ?thesis by auto - next - assume "p\s" - then have "winding_number \ p=0" using homo by auto - then show ?thesis by auto + define g where "g \ \x. if x=z then 0 else inverse (f x)" + obtain r where "0 < n" "0 < r" and r_cball:"cball z r \ s" and h_holo: "h holomorphic_on cball z r" + and h_divide:"(\w\cball z r. (w\z \ f w = h w / (w - z) ^ n) \ h w \ 0)" + using porder_exist[OF \open s\ \z \ s\ holo pole, folded n_def h_def] by blast + have r_nonzero:"\w. w \ ball z r - {z} \ f w \ 0" + using h_divide by simp + define c where "c \ 2 * pi * \" + define der_f where "der_f \ ((deriv ^^ (n - 1)) h z / fact (n-1))" + def h'\"\u. h u / (u - z) ^ n" + have "(h' has_contour_integral c / fact (n - 1) * (deriv ^^ (n - 1)) h z) (circlepath z r)" + unfolding h'_def + proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n-1", + folded c_def Suc_pred'[OF \n>0\]]) + show "continuous_on (cball z r) h" using holomorphic_on_imp_continuous_on h_holo by simp + show "h holomorphic_on ball z r" using h_holo by auto + show " z \ ball z r" using \r>0\ by auto qed - qed - also have "... = c * (\p\poles. winding_number \ p * residue f p)" - apply (subst setsum_right_distrib) - by simp - finally show ?thesis unfolding c_def by auto -qed + then have "(h' has_contour_integral c * der_f) (circlepath z r)" unfolding der_f_def by auto + then have "(f has_contour_integral c * der_f) (circlepath z r)" + proof (elim has_contour_integral_eq) + fix x assume "x \ path_image (circlepath z r)" + hence "x\cball z r - {z}" using \r>0\ by auto + then show "h' x = f x" using h_divide unfolding h'_def by auto + qed + moreover have "(f has_contour_integral c * residue f z) (circlepath z r)" + using base_residue[OF \open s\ \z\s\ \r>0\ holo r_cball,folded c_def] . + ultimately have "c * der_f = c * residue f z" using has_contour_integral_unique by blast + hence "der_f = residue f z" unfolding c_def by auto + thus ?thesis unfolding der_f_def by auto +qed theorem argument_principle: fixes f::"complex \ complex" and poles s:: "complex set" - defines "pts\{p. f p=0}" - defines "zeros\pts - poles" + defines "zeros\{p. f p=0} - poles" assumes "open s" and - connected:"connected (s- pts)" and + "connected s" and f_holo:"f holomorphic_on s-poles" and h_holo:"h holomorphic_on s" and "valid_path g" and loop:"pathfinish g = pathstart g" and - path_img:"path_image g \ s - pts" and + path_img:"path_image g \ s - (zeros \ poles)" and homo:"\z. (z \ s) \ winding_number g z = 0" and - finite:"finite pts" and + finite:"finite (zeros \ poles)" and poles:"\p\poles. is_pole f p" shows "contour_integral g (\x. deriv f x * h x / f x) = 2 * pi * \ * ((\p\zeros. winding_number g p * h p * zorder f p) - (\p\poles. winding_number g p * h p * porder f p))" (is "?L=?R") proof - - define c where "c = 2 * complex_of_real pi * \ " - define ff where [abs_def]: "ff x = deriv f x * h x / f x" for x - define cont_pole where "cont_pole ff p e \ - (ff has_contour_integral - c * porder f p * h p) (circlepath p e)" for ff p e - define cont_zero where "cont_zero ff p e \ - (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)" for ff p e - define avoid where "avoid p e \ (\w\cball p e. w \ s \ (w \ p \ w \ pts))" for p e - have "poles \ pts" and "zeros \ pts" and "finite zeros" and "pts=zeros \ poles" - using poles \finite pts\ unfolding pts_def zeros_def is_pole_def by auto + define c where "c \ 2 * complex_of_real pi * \ " + define ff where "ff \ (\x. deriv f x * h x / f x)" + define cont_pole where "cont_pole \ \ff p e. (ff has_contour_integral - c * porder f p * h p) (circlepath p e)" + define cont_zero where "cont_zero \ \ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)" + define avoid where "avoid \ \p e. \w\cball p e. w \ s \ (w \ p \ w \ zeros \ poles)" have "\e>0. avoid p e \ (p\poles \ cont_pole ff p e) \ (p\zeros \ cont_zero ff p e)" when "p\s" for p proof - - obtain e1 where e:"e1>0" and e:"avoid p e1" - using finite_cball_avoid[OF \open s\ \finite pts\] \p\s\ unfolding avoid_def by auto + obtain e1 where "e1>0" and e1_avoid:"avoid p e1" + using finite_cball_avoid[OF \open s\ finite] \p\s\ unfolding avoid_def by auto have "\e2>0. cball p e2 \ ball p e1 \ cont_pole ff p e2" when "p\poles" proof - - define po where "po = porder f p" - define pp where "pp = pol_poly f p" - define f' where [abs_def]: "f' w = pp w / (w - p) ^ po" for w - define ff' where [abs_def]: "ff' x = deriv f' x * h x / f' x" for x - have "inverse \ f holomorphic_on ball p e1" - proof - - have "f holomorphic_on ball p e1 - {p}" - using f_holo e \poles \ pts\ unfolding avoid_def - apply (elim holomorphic_on_subset) - by auto - then have inv_holo:"(inverse o f) holomorphic_on ball p e1 - {p}" - unfolding comp_def - apply (elim holomorphic_on_inverse) - using e pts_def ball_subset_cball unfolding avoid_def by blast - moreover have "isCont (inverse o f) p" - using \p\poles\ poles unfolding is_pole_def by auto - ultimately show "(inverse o f) holomorphic_on ball p e1" - apply (elim no_isolated_singularity[rotated]) - apply (auto simp add:continuous_on_eq_continuous_at[of "ball p e1",simplified]) - using field_differentiable_imp_continuous_at inv_holo - holomorphic_on_imp_differentiable_at unfolding comp_def - by fastforce - qed - moreover have "f p = 0" using \p\poles\ poles unfolding is_pole_def by auto - moreover have "\w\ball p e1. f w \ 0" - proof - - define p' where "p' = p+e1/2" - have "p'\ball p e1" and "p'\p" using \e1>0\ unfolding p'_def by (auto simp add:dist_norm) - then show "\w\ball p e1. f w \ 0" using e unfolding avoid_def - apply (rule_tac x=p' in bexI) - by (auto simp add:pts_def) - qed - ultimately obtain r where + define po where "po \ porder f p" + define pp where "pp \ pol_poly f p" + def f'\"\w. pp w / (w - p) ^ po" + def ff'\"(\x. deriv f' x * h x / f' x)" + have "f holomorphic_on ball p e1 - {p}" + apply (intro holomorphic_on_subset[OF f_holo]) + using e1_avoid \p\poles\ unfolding avoid_def by auto + then obtain r where "0 < po" "r>0" "cball p r \ ball p e1" and pp_holo:"pp holomorphic_on cball p r" and - pp_po:"(\w\cball p r. f w = pp w / (w - p) ^ po \ pp w \ 0)" - using porder_exist[of "ball p e1" p f,simplified,OF \e1>0\] unfolding po_def pp_def + pp_po:"(\w\cball p r. (w\p \ f w = pp w / (w - p) ^ po) \ pp w \ 0)" + using porder_exist[of "ball p e1" p f,simplified,OF \e1>0\] poles \p\poles\ + unfolding po_def pp_def by auto - define e2 where "e2 = r/2" + define e2 where "e2 \ r/2" have "e2>0" using \r>0\ unfolding e2_def by auto - define anal where [abs_def]: "anal w = deriv pp w * h w / pp w" for w - define prin where [abs_def]: "prin w = - of_nat po * h w / (w - p)" for w + define anal where "anal \ \w. deriv pp w * h w / pp w" + define prin where "prin \ \w. - of_nat po * h w / (w - p)" have "((\w. prin w + anal w) has_contour_integral - c * po * h p) (circlepath p e2)" - proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified]) - have "ball p r \ s" - using \cball p r \ ball p e1\ avoid_def ball_subset_cball e by blast - then have "cball p e2 \ s" - using \r>0\ unfolding e2_def by auto - then have "(\w. - of_nat po * h w) holomorphic_on cball p e2" - using h_holo - by (auto intro!: holomorphic_intros) - then show "(prin has_contour_integral - c * of_nat po * h p ) (circlepath p e2)" - using Cauchy_integral_circlepath_simple[folded c_def, of "\w. - of_nat po * h w"] - \e2>0\ - unfolding prin_def - by (auto simp add: mult.assoc) - have "anal holomorphic_on ball p r" unfolding anal_def - using pp_holo h_holo pp_po \ball p r \ s\ - by (auto intro!: holomorphic_intros) - then show "(anal has_contour_integral 0) (circlepath p e2)" - using e2_def \r>0\ - by (auto elim!: Cauchy_theorem_disc_simple) - qed + proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified]) + have "ball p r \ s" + using \cball p r \ ball p e1\ avoid_def ball_subset_cball e1_avoid by blast + then have "cball p e2 \ s" + using \r>0\ unfolding e2_def by auto + then have "(\w. - of_nat po * h w) holomorphic_on cball p e2" + using h_holo + by (auto intro!: holomorphic_intros) + then show "(prin has_contour_integral - c * of_nat po * h p ) (circlepath p e2)" + using Cauchy_integral_circlepath_simple[folded c_def, of "\w. - of_nat po * h w"] + \e2>0\ + unfolding prin_def + by (auto simp add: mult.assoc) + have "anal holomorphic_on ball p r" unfolding anal_def + using pp_holo h_holo pp_po \ball p r \ s\ + by (auto intro!: holomorphic_intros) + then show "(anal has_contour_integral 0) (circlepath p e2)" + using e2_def \r>0\ + by (auto elim!: Cauchy_theorem_disc_simple) + qed then have "cont_pole ff' p e2" unfolding cont_pole_def po_def proof (elim has_contour_integral_eq) fix w assume "w \ path_image (circlepath p e2)" then have "w\ball p r" and "w\p" unfolding e2_def using \r>0\ by auto - define wp where "wp = w-p" + define wp where "wp \ w-p" have "wp\0" and "pp w \0" unfolding wp_def using \w\p\ \w\ball p r\ pp_po by auto moreover have der_f':"deriv f' w = - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po" proof (rule DERIV_imp_deriv) - define der where "der = - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po" + define der where "der \ - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po" have po:"po = Suc (po - Suc 0) " using \po>0\ by auto have "(pp has_field_derivative (deriv pp w)) (at w)" - using DERIV_deriv_iff_field_differentiable \w\ball p r\ - holomorphic_on_imp_differentiable_at[of _ "ball p r"] - holomorphic_on_subset [OF pp_holo ball_subset_cball] - by (metis open_ball) + using DERIV_deriv_iff_has_field_derivative pp_holo \w\p\ + by (meson open_ball \w \ ball p r\ ball_subset_cball holomorphic_derivI holomorphic_on_subset) then show "(f' has_field_derivative der) (at w)" using \w\p\ \po>0\ unfolding der_def f'_def apply (auto intro!: derivative_eq_intros simp add:field_simps) @@ -3040,27 +3291,29 @@ fix w assume "w \ path_image (circlepath p e2)" then have "w\ball p r" and "w\p" unfolding e2_def using \r>0\ by auto have "deriv f' w = deriv f w" - proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"]) - show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo - by (auto intro!: holomorphic_intros) - next - have "ball p e1 - {p} \ s - poles" - using avoid_def ball_subset_cball e \poles \ pts\ by auto - then have "ball p r - {p} \ s - poles" using \cball p r \ ball p e1\ - using ball_subset_cball by blast - then show "f holomorphic_on ball p r - {p}" using f_holo - by auto - next - show "open (ball p r - {p})" by auto - next - show "w \ ball p r - {p}" using \w\ball p r\ \w\p\ by auto - next - fix x assume "x \ ball p r - {p}" - then show "f' x = f x" - using pp_po unfolding f'_def by auto - qed + proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"]) + show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo + by (auto intro!: holomorphic_intros) + next + have "ball p e1 - {p} \ s - poles" + using avoid_def ball_subset_cball e1_avoid + by auto + then have "ball p r - {p} \ s - poles" using \cball p r \ ball p e1\ + using ball_subset_cball by blast + then show "f holomorphic_on ball p r - {p}" using f_holo + by auto + next + show "open (ball p r - {p})" by auto + next + show "w \ ball p r - {p}" using \w\ball p r\ \w\p\ by auto + next + fix x assume "x \ ball p r - {p}" + then show "f' x = f x" + using pp_po unfolding f'_def by auto + qed moreover have " f' w = f w " - using \w \ ball p r\ ball_subset_cball subset_iff pp_po unfolding f'_def by auto + using \w \ ball p r\ ball_subset_cball subset_iff pp_po \w\p\ + unfolding f'_def by auto ultimately show "ff' w = ff w" unfolding ff'_def ff_def by simp qed @@ -3073,27 +3326,26 @@ have "\e3>0. cball p e3 \ ball p e1 \ cont_zero ff p e3" when "p\zeros" proof - - define zo where "zo = zorder f p" - define zp where "zp = zer_poly f p" - define f' where [abs_def]: "f' w = zp w * (w - p) ^ zo" for w - define ff' where [abs_def]: "ff' x = deriv f' x * h x / f' x" for x + define zo where "zo \ zorder f p" + define zp where "zp \ zer_poly f p" + def f'\"\w. zp w * (w - p) ^ zo" + def ff'\"(\x. deriv f' x * h x / f' x)" have "f holomorphic_on ball p e1" - proof - - have "ball p e1 \ s - poles" - using \poles \ pts\ avoid_def ball_subset_cball e that zeros_def by fastforce - thus ?thesis using f_holo by auto - qed + proof - + have "ball p e1 \ s - poles" + using avoid_def ball_subset_cball e1_avoid that zeros_def by fastforce + thus ?thesis using f_holo by auto + qed moreover have "f p = 0" using \p\zeros\ - using DiffD1 mem_Collect_eq pts_def zeros_def by blast + using DiffD1 mem_Collect_eq zeros_def by blast moreover have "\w\ball p e1. f w \ 0" - proof - - define p' where "p' = p+e1/2" - have "p'\ball p e1" and "p'\p" - using \e1>0\ unfolding p'_def by (auto simp add:dist_norm) - then show "\w\ball p e1. f w \ 0" using e unfolding avoid_def - apply (rule_tac x=p' in bexI) - by (auto simp add:pts_def) - qed + proof - + def p'\"p+e1/2" + have "p'\ball p e1" and "p'\p" using \e1>0\ unfolding p'_def by (auto simp add:dist_norm) + then show "\w\ball p e1. f w \ 0" using e1_avoid unfolding avoid_def + apply (rule_tac x=p' in bexI) + by (auto simp add:zeros_def) + qed ultimately obtain r where "0 < zo" "r>0" "cball p r \ ball p e1" and @@ -3101,59 +3353,57 @@ pp_po:"(\w\cball p r. f w = zp w * (w - p) ^ zo \ zp w \ 0)" using zorder_exist[of "ball p e1" p f,simplified,OF \e1>0\] unfolding zo_def zp_def by auto - define e2 where "e2 = r/2" + define e2 where "e2 \ r/2" have "e2>0" using \r>0\ unfolding e2_def by auto - define anal where [abs_def]: "anal w = deriv zp w * h w / zp w" for w - define prin where [abs_def]: "prin w = of_nat zo * h w / (w - p)" for w + define anal where "anal \ \w. deriv zp w * h w / zp w" + define prin where "prin \ \w. of_nat zo * h w / (w - p)" have "((\w. prin w + anal w) has_contour_integral c * zo * h p) (circlepath p e2)" - proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified]) - have "ball p r \ s" - using \cball p r \ ball p e1\ avoid_def ball_subset_cball e by blast - then have "cball p e2 \ s" - using \r>0\ unfolding e2_def by auto - then have "(\w. of_nat zo * h w) holomorphic_on cball p e2" - using h_holo - by (auto intro!: holomorphic_intros) - then show "(prin has_contour_integral c * of_nat zo * h p ) (circlepath p e2)" - using Cauchy_integral_circlepath_simple[folded c_def, of "\w. of_nat zo * h w"] - \e2>0\ - unfolding prin_def - by (auto simp add: mult.assoc) - have "anal holomorphic_on ball p r" unfolding anal_def - using pp_holo h_holo pp_po \ball p r \ s\ - by (auto intro!: holomorphic_intros) - then show "(anal has_contour_integral 0) (circlepath p e2)" - using e2_def \r>0\ - by (auto elim!: Cauchy_theorem_disc_simple) - qed + proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified]) + have "ball p r \ s" + using \cball p r \ ball p e1\ avoid_def ball_subset_cball e1_avoid by blast + then have "cball p e2 \ s" + using \r>0\ unfolding e2_def by auto + then have "(\w. of_nat zo * h w) holomorphic_on cball p e2" + using h_holo + by (auto intro!: holomorphic_intros) + then show "(prin has_contour_integral c * of_nat zo * h p ) (circlepath p e2)" + using Cauchy_integral_circlepath_simple[folded c_def, of "\w. of_nat zo * h w"] + \e2>0\ + unfolding prin_def + by (auto simp add: mult.assoc) + have "anal holomorphic_on ball p r" unfolding anal_def + using pp_holo h_holo pp_po \ball p r \ s\ + by (auto intro!: holomorphic_intros) + then show "(anal has_contour_integral 0) (circlepath p e2)" + using e2_def \r>0\ + by (auto elim!: Cauchy_theorem_disc_simple) + qed then have "cont_zero ff' p e2" unfolding cont_zero_def zo_def - proof (elim has_contour_integral_eq) - fix w assume "w \ path_image (circlepath p e2)" - then have "w\ball p r" and "w\p" unfolding e2_def using \r>0\ by auto - define wp where "wp = w-p" - have "wp\0" and "zp w \0" - unfolding wp_def using \w\p\ \w\ball p r\ pp_po by auto - moreover have der_f':"deriv f' w = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" - proof (rule DERIV_imp_deriv) - define der where "der = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" - have po:"zo = Suc (zo - Suc 0) " using \zo>0\ by auto - have "(zp has_field_derivative (deriv zp w)) (at w)" - using DERIV_deriv_iff_field_differentiable \w\ball p r\ - holomorphic_on_imp_differentiable_at[of _ "ball p r"] - holomorphic_on_subset [OF pp_holo ball_subset_cball] - by (metis open_ball) - then show "(f' has_field_derivative der) (at w)" - using \w\p\ \zo>0\ unfolding der_def f'_def - by (auto intro!: derivative_eq_intros simp add:field_simps) - qed - ultimately show "prin w + anal w = ff' w" - unfolding ff'_def prin_def anal_def - apply simp - apply (unfold f'_def) - apply (fold wp_def) - apply (auto simp add:field_simps) - by (metis Suc_diff_Suc minus_nat.diff_0 power_Suc) - qed + proof (elim has_contour_integral_eq) + fix w assume "w \ path_image (circlepath p e2)" + then have "w\ball p r" and "w\p" unfolding e2_def using \r>0\ by auto + define wp where "wp \ w-p" + have "wp\0" and "zp w \0" + unfolding wp_def using \w\p\ \w\ball p r\ pp_po by auto + moreover have der_f':"deriv f' w = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" + proof (rule DERIV_imp_deriv) + define der where "der \ zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" + have po:"zo = Suc (zo - Suc 0) " using \zo>0\ by auto + have "(zp has_field_derivative (deriv zp w)) (at w)" + using DERIV_deriv_iff_has_field_derivative pp_holo + by (meson Topology_Euclidean_Space.open_ball \w \ ball p r\ ball_subset_cball holomorphic_derivI holomorphic_on_subset) + then show "(f' has_field_derivative der) (at w)" + using \w\p\ \zo>0\ unfolding der_def f'_def + by (auto intro!: derivative_eq_intros simp add:field_simps) + qed + ultimately show "prin w + anal w = ff' w" + unfolding ff'_def prin_def anal_def + apply simp + apply (unfold f'_def) + apply (fold wp_def) + apply (auto simp add:field_simps) + by (metis Suc_diff_Suc minus_nat.diff_0 power_Suc) + qed then have "cont_zero ff p e2" unfolding cont_zero_def proof (elim has_contour_integral_eq) fix w assume "w \ path_image (circlepath p e2)" @@ -3164,7 +3414,7 @@ by (auto intro!: holomorphic_intros) next have "ball p e1 - {p} \ s - poles" - using avoid_def ball_subset_cball e \poles \ pts\ by auto + using avoid_def ball_subset_cball e1_avoid by auto then have "ball p r - {p} \ s - poles" using \cball p r \ ball p e1\ using ball_subset_cball by blast then show "f holomorphic_on ball p r - {p}" using f_holo @@ -3189,31 +3439,31 @@ qed then obtain e3 where e3:"p\zeros \ e3>0 \ cball p e3 \ ball p e1 \ cont_zero ff p e3" by auto - define e4 where "e4 = (if p\poles then e2 else if p\zeros then e3 else e1)" + define e4 where "e4 \ if p\poles then e2 else if p\zeros then e3 else e1" have "e4>0" using e2 e3 \e1>0\ unfolding e4_def by auto - moreover have "avoid p e4" using e2 e3 \e1>0\ e unfolding e4_def avoid_def by auto + moreover have "avoid p e4" using e2 e3 \e1>0\ e1_avoid unfolding e4_def avoid_def by auto moreover have "p\poles \ cont_pole ff p e4" and "p\zeros \ cont_zero ff p e4" - by (auto simp add: e2 e3 e4_def pts_def zeros_def) + by (auto simp add: e2 e3 e4_def zeros_def) ultimately show ?thesis by auto qed then obtain get_e where get_e:"\p\s. get_e p>0 \ avoid p (get_e p) \ (p\poles \ cont_pole ff p (get_e p)) \ (p\zeros \ cont_zero ff p (get_e p))" by metis - define cont where "cont p = contour_integral (circlepath p (get_e p)) ff" for p - define w where "w p = winding_number g p" for p - have "contour_integral g ff = (\p\pts. w p * cont p)" + define cont where "cont \ \p. contour_integral (circlepath p (get_e p)) ff" + define w where "w \ \p. winding_number g p" + have "contour_integral g ff = (\p\zeros \ poles. w p * cont p)" unfolding cont_def w_def - proof (rule Cauchy_theorem_singularities[OF \open s\ connected finite _ \valid_path g\ loop - path_img homo]) - have "open (s - pts)" using open_Diff[OF _ finite_imp_closed[OF finite]] \open s\ by auto - then show "ff holomorphic_on s - pts" unfolding ff_def using f_holo \poles \ pts\ h_holo - by (auto intro!: holomorphic_intros simp add:pts_def) - next - show "\p\s. 0 < get_e p \ (\w\cball p (get_e p). w \ s \ (w \ p \ w \ pts))" - using get_e using avoid_def by blast - qed + proof (rule Cauchy_theorem_singularities[OF \open s\ \connected s\ finite _ \valid_path g\ loop + path_img homo]) + have "open (s - (zeros \ poles))" using open_Diff[OF _ finite_imp_closed[OF finite]] \open s\ by auto + then show "ff holomorphic_on s - (zeros \ poles)" unfolding ff_def using f_holo h_holo + by (auto intro!: holomorphic_intros simp add:zeros_def) + next + show "\p\s. 0 < get_e p \ (\w\cball p (get_e p). w \ s \ (w \ p \ w \ zeros \ poles))" + using get_e using avoid_def by blast + qed also have "... = (\p\zeros. w p * cont p) + (\p\poles. w p * cont p)" - using \finite pts\ unfolding \pts=zeros \ poles\ + using finite apply (subst setsum.union_disjoint) by (auto simp add:zeros_def) also have "... = c * ((\p\zeros. w p * h p * zorder f p) - (\p\poles. w p * h p * porder f p))" @@ -3263,27 +3513,14 @@ finally show ?thesis unfolding w_def ff_def c_def by auto qed -lemma holomorphic_imp_diff_on: - assumes f_holo:"f holomorphic_on s" and "open s" - shows "f differentiable_on s" -proof (rule differentiable_at_imp_differentiable_on) - fix x assume "x\s" - obtain f' where "(f has_field_derivative f') (at x) " - using holomorphic_on_imp_differentiable_at[OF f_holo \open s\ \x\s\] - unfolding field_differentiable_def by auto - then have " (f has_derivative op * f') (at x)" - using has_field_derivative_imp_has_derivative[of f f' "at x"] by auto - then show "f differentiable at x" using differentiableI by auto -qed +subsection \Rouche's theorem \ theorem Rouche_theorem: fixes f g::"complex \ complex" and s:: "complex set" defines "fg\(\p. f p+ g p)" defines "zeros_fg\{p. fg p =0}" and "zeros_f\{p. f p=0}" assumes - "open s" and - connected_fg:"connected (s- zeros_fg)" and - connected_f:"connected (s- zeros_f)" and + "open s" and "connected s" and "finite zeros_fg" and "finite zeros_f" and f_holo:"f holomorphic_on s" and @@ -3317,9 +3554,9 @@ qed then show ?thesis unfolding zeros_f_def using path_img by auto qed - define w where "w p = winding_number \ p" for p - define c where "c = 2 * complex_of_real pi * \" - define h where [abs_def]: "h p = g p / f p + 1" for p + define w where "w \ \p. winding_number \ p" + define c where "c \ 2 * complex_of_real pi * \" + define h where "h \ \p. g p / f p + 1" obtain spikes where "finite spikes" and spikes: "\x\{0..1} - spikes. \ differentiable at x" using \valid_path \\ @@ -3339,9 +3576,7 @@ by (simp add: image_subset_iff path_image_compose) moreover have " (0::complex) \ ball 1 1" by (simp add: dist_norm) ultimately show "?thesis" - using convex_in_outside[of "ball 1 1" "0::complex"] - apply (drule_tac outside_mono) - by auto + using convex_in_outside[of "ball 1 1" 0] outside_mono by blast qed have valid_h:"valid_path (h \ \)" proof (rule valid_path_compose_holomorphic[OF \valid_path \\ _ _ path_f]) @@ -3362,7 +3597,7 @@ proof - have "0 \ outside (path_image (h \ \))" using outside_img . moreover have "path (h o \)" - using valid_h by auto + using valid_h by (simp add: valid_path_imp_path) moreover have "pathfinish (h o \) = pathstart (h o \)" by (simp add: loop pathfinish_compose pathstart_compose) ultimately show ?thesis using winding_number_zero_in_outside by auto @@ -3374,17 +3609,15 @@ proof (rule vector_derivative_chain_at_general) show "\ differentiable at x" using that \valid_path \\ spikes by auto next - define der where "der p = (deriv g p * f p - g p * deriv f p)/(f p * f p)" for p - define t where "t = \ x" + define der where "der \ \p. (deriv g p * f p - g p * deriv f p)/(f p * f p)" + define t where "t \ \ x" have "f t\0" unfolding zeros_f_def t_def by (metis DiffD1 image_eqI norm_not_less_zero norm_zero path_defs(4) path_less that) moreover have "t\s" using contra_subsetD path_image_def path_fg t_def that by fastforce ultimately have "(h has_field_derivative der t) (at t)" - unfolding h_def der_def using g_holo f_holo - apply (auto intro!: derivative_eq_intros) - by (auto simp add: DERIV_deriv_iff_field_differentiable - holomorphic_on_imp_differentiable_at[OF _ \open s\]) + unfolding h_def der_def using g_holo f_holo \open s\ + by (auto intro!: holomorphic_derivI derivative_eq_intros ) then show "\g'. (h has_field_derivative g') (at (\ x))" unfolding t_def by auto qed then have " (op / 1 has_contour_integral 0) (h \ \) @@ -3420,29 +3653,27 @@ have "fg p\0" and "f p\0" using path_f path_fg that unfolding zeros_f_def zeros_fg_def by auto have "h p\0" - proof (rule ccontr) - assume "\ h p \ 0" - then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2) - then have "cmod (g p/f p) = 1" by auto - moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that] - apply (cases "cmod (f p) = 0") - by (auto simp add: norm_divide) - ultimately show False by auto - qed + proof (rule ccontr) + assume "\ h p \ 0" + then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2) + then have "cmod (g p/f p) = 1" by auto + moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that] + apply (cases "cmod (f p) = 0") + by (auto simp add: norm_divide) + ultimately show False by auto + qed have der_fg:"deriv fg p = deriv f p + deriv g p" unfolding fg_def using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _ \open s\] path_img that - by (auto intro!: deriv_add) + by auto have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)" - proof - - define der where "der p = (deriv g p * f p - g p * deriv f p)/(f p * f p)" for p - have "p\s" using path_img that by auto - then have "(h has_field_derivative der p) (at p)" - unfolding h_def der_def using g_holo f_holo \f p\0\ - apply (auto intro!: derivative_eq_intros) - by (auto simp add: DERIV_deriv_iff_field_differentiable - holomorphic_on_imp_differentiable_at[OF _ \open s\]) - then show ?thesis unfolding der_def using DERIV_imp_deriv by auto - qed + proof - + define der where "der \ \p. (deriv g p * f p - g p * deriv f p)/(f p * f p)" + have "p\s" using path_img that by auto + then have "(h has_field_derivative der p) (at p)" + unfolding h_def der_def using g_holo f_holo \open s\ \f p\0\ + by (auto intro!: derivative_eq_intros holomorphic_derivI) + then show ?thesis unfolding der_def using DERIV_imp_deriv by auto + qed show ?thesis apply (simp only:der_fg der_h) apply (auto simp add:field_simps \h p\0\ \f p\0\ \fg p\0\) @@ -3455,21 +3686,21 @@ qed moreover have "contour_integral \ (\x. deriv fg x / fg x) = c * (\p\zeros_fg. w p * zorder fg p)" unfolding c_def zeros_fg_def w_def - proof (rule argument_principle[OF \open s\ _ _ _ \valid_path \\ loop _ homo, of _ "{}" "\_. 1",simplified]) - show "connected (s - {p. fg p = 0})" using connected_fg unfolding zeros_fg_def . + proof (rule argument_principle[OF \open s\ \connected s\ _ _ \valid_path \\ loop _ homo + , of _ "{}" "\_. 1",simplified]) show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto show "path_image \ \ s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def . show " finite {p. fg p = 0}" using \finite zeros_fg\ unfolding zeros_fg_def . qed moreover have "contour_integral \ (\x. deriv f x / f x) = c * (\p\zeros_f. w p * zorder f p)" unfolding c_def zeros_f_def w_def - proof (rule argument_principle[OF \open s\ _ _ _ \valid_path \\ loop _ homo, of _ "{}" "\_. 1",simplified]) - show "connected (s - {p. f p = 0})" using connected_f unfolding zeros_f_def . + proof (rule argument_principle[OF \open s\ \connected s\ _ _ \valid_path \\ loop _ homo + , of _ "{}" "\_. 1",simplified]) show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto show "path_image \ \ s - {p. f p = 0}" using path_f unfolding zeros_f_def . - show "finite {p. f p = 0}" using \finite zeros_f\ unfolding zeros_f_def . + show " finite {p. f p = 0}" using \finite zeros_f\ unfolding zeros_f_def . qed - ultimately have "c * (\p\zeros_fg. w p * (zorder fg p)) = c* (\p\zeros_f. w p * (zorder f p))" + ultimately have " c* (\p\zeros_fg. w p * (zorder fg p)) = c* (\p\zeros_f. w p * (zorder f p))" by auto then show ?thesis unfolding c_def using w_def by auto qed diff -r 6a131df8e3d9 -r 82df5181d699 src/HOL/Multivariate_Analysis/Path_Connected.thy --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Wed May 25 13:13:35 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Wed May 25 16:38:35 2016 +0100 @@ -2073,10 +2073,26 @@ "2 \ DIM('N::euclidean_space) \ path_connected(ball a r - {a::'N})" by (simp add: path_connected_open_delete) -lemma connected_punctured_ball: +corollary connected_punctured_ball: "2 \ DIM('N::euclidean_space) \ connected(ball a r - {a::'N})" by (simp add: connected_open_delete) +corollary connected_open_delete_finite: + fixes S T::"'a::euclidean_space set" + assumes S: "open S" "connected S" and 2: "2 \ DIM('a)" and "finite T" + shows "connected(S - T)" + using \finite T\ S +proof (induct T) + case empty + show ?case using \connected S\ by simp +next + case (insert x F) + then have "connected (S-F)" by auto + moreover have "open (S - F)" using finite_imp_closed[OF \finite F\] \open S\ by auto + ultimately have "connected (S - F - {x})" using connected_open_delete[OF _ _ 2] by auto + thus ?case by (metis Diff_insert) +qed + subsection\Relations between components and path components\ lemma open_connected_component: diff -r 6a131df8e3d9 -r 82df5181d699 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed May 25 13:13:35 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed May 25 16:38:35 2016 +0100 @@ -9253,6 +9253,34 @@ shows "cball x d = ball y e \ d < 0 \ e \ 0" using ball_eq_cball_iff by blast +lemma finite_ball_avoid: + fixes S :: "'a :: euclidean_space set" + assumes "open S" "finite X" "p \ S" + shows "\e>0. \w\ball p e. w\S \ (w\p \ w\X)" +proof - + obtain e1 where "0 < e1" and e1_b:"ball p e1 \ S" + using open_contains_ball_eq[OF \open S\] assms by auto + obtain e2 where "0 < e2" and "\x\X. x \ p \ e2 \ dist p x" + using finite_set_avoid[OF \finite X\,of p] by auto + hence "\w\ball p (min e1 e2). w\S \ (w\p \ w\X)" using e1_b by auto + thus "\e>0. \w\ball p e. w \ S \ (w \ p \ w \ X)" using \e2>0\ \e1>0\ + apply (rule_tac x="min e1 e2" in exI) + by auto +qed + +lemma finite_cball_avoid: + fixes S :: "'a :: euclidean_space set" + assumes "open S" "finite X" "p \ S" + shows "\e>0. \w\cball p e. w\S \ (w\p \ w\X)" +proof - + obtain e1 where "e1>0" and e1: "\w\ball p e1. w\S \ (w\p \ w\X)" + using finite_ball_avoid[OF assms] by auto + define e2 where "e2 \ e1/2" + have "e2>0" and "e2 < e1" unfolding e2_def using \e1>0\ by auto + then have "cball p e2 \ ball p e1" by (subst cball_subset_ball_iff,auto) + then show "\e>0. \w\cball p e. w \ S \ (w \ p \ w \ X)" using \e2>0\ e1 by auto +qed + no_notation eucl_less (infix "