# HG changeset patch # User paulson # Date 1676550081 0 # Node ID c6b50597abbcb5275da3fb952f4947481657620d # Parent 29032b496f2e6d42c0837f2521a764ecd880ac59 More of Eberl's contributions: memomorphic functions diff -r 29032b496f2e -r c6b50597abbc src/HOL/Complex_Analysis/Complex_Analysis.thy --- a/src/HOL/Complex_Analysis/Complex_Analysis.thy Thu Feb 16 10:42:39 2023 +0000 +++ b/src/HOL/Complex_Analysis/Complex_Analysis.thy Thu Feb 16 12:21:21 2023 +0000 @@ -1,7 +1,7 @@ theory Complex_Analysis imports Residue_Theorem - Riemann_Mapping + Meromorphic begin end diff -r 29032b496f2e -r c6b50597abbc src/HOL/Complex_Analysis/Complex_Singularities.thy --- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Thu Feb 16 10:42:39 2023 +0000 +++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Thu Feb 16 12:21:21 2023 +0000 @@ -249,6 +249,12 @@ shows "not_essential f z \ not_essential g z'" unfolding not_essential_def using assms filterlim_cong is_pole_cong by fastforce +lemma not_essential_compose_iff: + assumes "filtermap g (at z) = at z'" + shows "not_essential (f \ g) z = not_essential f z'" + unfolding not_essential_def filterlim_def filtermap_compose assms is_pole_compose_iff[OF assms] + by blast + lemma isolated_singularity_at_cong: assumes "eventually (\x. f x = g x) (at z)" "z = z'" shows "isolated_singularity_at f z \ isolated_singularity_at g z'" @@ -362,8 +368,8 @@ 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 + unfolding F_def + using \r>0\ centre_in_ball continuous_on_def g_holo holomorphic_on_imp_continuous_on by blast 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)" @@ -1058,7 +1064,7 @@ using analytic_at not_is_pole_holomorphic by blast lemma not_essential_const [singularity_intros]: "not_essential (\_. c) z" - unfolding not_essential_def by (rule exI[of _ c]) auto + by blast lemma not_essential_uminus [singularity_intros]: assumes f_ness: "not_essential f z" diff -r 29032b496f2e -r c6b50597abbc src/HOL/Complex_Analysis/Laurent_Convergence.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Thu Feb 16 12:21:21 2023 +0000 @@ -0,0 +1,2917 @@ +theory Laurent_Convergence + imports "HOL-Computational_Algebra.Formal_Laurent_Series" "HOL-Library.Landau_Symbols" + Residue_Theorem + +begin + +(* TODO: Move *) +text \TODO: Better than @{thm deriv_compose_linear}?\ +lemma deriv_compose_linear': + assumes "f field_differentiable at (c * z+a)" + shows "deriv (\w. f (c * w+a)) z = c * deriv f (c * z+a)" + apply (subst deriv_chain[where f="\w. c * w+a",unfolded comp_def]) + using assms by (auto intro:derivative_intros) + +text \TODO: Better than @{thm higher_deriv_compose_linear}?\ +lemma higher_deriv_compose_linear': + fixes z::complex + assumes f: "f holomorphic_on T" and S: "open S" and T: "open T" and z: "z \ S" + and fg: "\w. w \ S \ u * w+c \ T" + shows "(deriv ^^ n) (\w. f (u * w+c)) z = u^n * (deriv ^^ n) f (u * z+c)" +using z +proof (induction n arbitrary: z) + case 0 then show ?case by simp +next + case (Suc n z) + have holo0: "f holomorphic_on (\w. u * w+c) ` S" + by (meson fg f holomorphic_on_subset image_subset_iff) + have holo2: "(deriv ^^ n) f holomorphic_on (\w. u * w+c) ` S" + by (meson f fg holomorphic_higher_deriv holomorphic_on_subset image_subset_iff T) + have holo3: "(\z. u ^ n * (deriv ^^ n) f (u * z+c)) holomorphic_on S" + by (intro holo2 holomorphic_on_compose [where g="(deriv ^^ n) f", unfolded o_def] holomorphic_intros) + have "(\w. u * w+c) holomorphic_on S" "f holomorphic_on (\w. u * w+c) ` S" + by (rule holo0 holomorphic_intros)+ + then have holo1: "(\w. f (u * w+c)) holomorphic_on S" + by (rule holomorphic_on_compose [where g=f, unfolded o_def]) + have "deriv ((deriv ^^ n) (\w. f (u * w+c))) z = deriv (\z. u^n * (deriv ^^ n) f (u*z+c)) z" + proof (rule complex_derivative_transform_within_open [OF _ holo3 S Suc.prems]) + show "(deriv ^^ n) (\w. f (u * w+c)) holomorphic_on S" + by (rule holomorphic_higher_deriv [OF holo1 S]) + qed (simp add: Suc.IH) + also have "\ = u^n * deriv (\z. (deriv ^^ n) f (u * z+c)) z" + proof - + have "(deriv ^^ n) f analytic_on T" + by (simp add: analytic_on_open f holomorphic_higher_deriv T) + then have "(\w. (deriv ^^ n) f (u * w+c)) analytic_on S" + proof - + have "(deriv ^^ n) f \ (\w. u * w+c) holomorphic_on S" + using holomorphic_on_compose[OF _ holo2] \(\w. u * w+c) holomorphic_on S\ + by simp + then show ?thesis + by (simp add: S analytic_on_open o_def) + qed + then show ?thesis + by (intro deriv_cmult analytic_on_imp_differentiable_at [OF _ Suc.prems]) + qed + also have "\ = u * u ^ n * deriv ((deriv ^^ n) f) (u * z+c)" + proof - + have "(deriv ^^ n) f field_differentiable at (u * z+c)" + using Suc.prems T f fg holomorphic_higher_deriv holomorphic_on_imp_differentiable_at by blast + then show ?thesis + by (simp add: deriv_compose_linear') + qed + finally show ?case + by simp +qed + +lemma fps_to_fls_numeral [simp]: "fps_to_fls (numeral n) = numeral n" + by (metis fps_to_fls_of_nat of_nat_numeral) + +lemma fls_const_power: "fls_const (a ^ b) = fls_const a ^ b" + by (induction b) (auto simp flip: fls_const_mult_const) + +lemma fls_deriv_numeral [simp]: "fls_deriv (numeral n) = 0" + by (metis fls_deriv_of_int of_int_numeral) + +lemma fls_const_numeral [simp]: "fls_const (numeral n) = numeral n" + by (metis fls_of_nat of_nat_numeral) + +lemma fls_mult_of_int_nth [simp]: + shows "fls_nth (numeral k * f) n = numeral k * fls_nth f n" + and "fls_nth (f * numeral k) n = fls_nth f n * numeral k" + by (metis fls_const_numeral fls_mult_const_nth)+ + +lemma fls_nth_numeral' [simp]: + "fls_nth (numeral n) 0 = numeral n" "k \ 0 \ fls_nth (numeral n) k = 0" + by (subst fls_const_numeral [symmetric], subst fls_const_nth, simp)+ + +lemma fls_subdegree_prod: + fixes F :: "'a \ 'b :: field_char_0 fls" + assumes "\x. x \ I \ F x \ 0" + shows "fls_subdegree (\x\I. F x) = (\x\I. fls_subdegree (F x))" + using assms by (induction I rule: infinite_finite_induct) auto + +lemma fls_subdegree_prod': + fixes F :: "'a \ 'b :: field_char_0 fls" + assumes "\x. x \ I \ fls_subdegree (F x) \ 0" + shows "fls_subdegree (\x\I. F x) = (\x\I. fls_subdegree (F x))" +proof (intro fls_subdegree_prod) + show "F x \ 0" if "x \ I" for x + using assms[OF that] by auto +qed + +instance fps :: (semiring_char_0) semiring_char_0 +proof + show "inj (of_nat :: nat \ 'a fps)" + proof + fix m n :: nat + assume "of_nat m = (of_nat n :: 'a fps)" + hence "fps_nth (of_nat m) 0 = (fps_nth (of_nat n) 0 :: 'a)" + by (simp only: ) + thus "m = n" + by simp + qed +qed + +instance fls :: (semiring_char_0) semiring_char_0 +proof + show "inj (of_nat :: nat \ 'a fls)" + proof + fix m n :: nat + assume "of_nat m = (of_nat n :: 'a fls)" + hence "fls_nth (of_nat m) 0 = (fls_nth (of_nat n) 0 :: 'a)" + by (simp only: ) + thus "m = n" + by (simp add: fls_of_nat_nth) + qed +qed + +lemma fls_const_eq_0_iff [simp]: "fls_const c = 0 \ c = 0" + using fls_const_0 fls_const_nonzero by blast + +lemma fls_subdegree_add_eq1: + assumes "f \ 0" "fls_subdegree f < fls_subdegree g" + shows "fls_subdegree (f + g) = fls_subdegree f" +proof (intro antisym) + from assms have *: "fls_nth (f + g) (fls_subdegree f) \ 0" + by auto + from * show "fls_subdegree (f + g) \ fls_subdegree f" + by (rule fls_subdegree_leI) + from * have "f + g \ 0" + using fls_nonzeroI by blast + thus "fls_subdegree f \ fls_subdegree (f + g)" + using assms(2) fls_plus_subdegree by force +qed + +lemma fls_subdegree_add_eq2: + assumes "g \ 0" "fls_subdegree g < fls_subdegree f" + shows "fls_subdegree (f + g) = fls_subdegree g" +proof (intro antisym) + from assms have *: "fls_nth (f + g) (fls_subdegree g) \ 0" + by auto + from * show "fls_subdegree (f + g) \ fls_subdegree g" + by (rule fls_subdegree_leI) + from * have "f + g \ 0" + using fls_nonzeroI by blast + thus "fls_subdegree g \ fls_subdegree (f + g)" + using assms(2) fls_plus_subdegree by force +qed + +lemma fls_subdegree_diff_eq1: + assumes "f \ 0" "fls_subdegree f < fls_subdegree g" + shows "fls_subdegree (f - g) = fls_subdegree f" + using fls_subdegree_add_eq1[of f "-g"] assms by simp + +lemma fls_subdegree_diff_eq2: + assumes "g \ 0" "fls_subdegree g < fls_subdegree f" + shows "fls_subdegree (f - g) = fls_subdegree g" + using fls_subdegree_add_eq2[of "-g" f] assms by simp + +lemma nat_minus_fls_subdegree_plus_const_eq: + "nat (-fls_subdegree (F + fls_const c)) = nat (-fls_subdegree F)" +proof (cases "fls_subdegree F < 0") + case True + hence "fls_subdegree (F + fls_const c) = fls_subdegree F" + by (intro fls_subdegree_add_eq1) auto + thus ?thesis + by simp +next + case False + thus ?thesis + by (auto simp: fls_subdegree_ge0I) +qed + +lemma at_to_0': "NO_MATCH 0 z \ at z = filtermap (\x. x + z) (at 0)" + for z :: "'a::real_normed_vector" + by (rule at_to_0) + +lemma nhds_to_0: "nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)" +proof - + have "(\xa. xa - - x) = (+) x" + by auto + thus ?thesis + using filtermap_nhds_shift[of "-x" 0] by simp +qed + +lemma nhds_to_0': "NO_MATCH 0 x \ nhds (x :: 'a :: real_normed_vector) = filtermap ((+) x) (nhds 0)" + by (rule nhds_to_0) + + +definition%important fls_conv_radius :: "complex fls \ ereal" where + "fls_conv_radius f = fps_conv_radius (fls_regpart f)" + +definition%important eval_fls :: "complex fls \ complex \ complex" where + "eval_fls F z = eval_fps (fls_base_factor_to_fps F) z * z powi fls_subdegree F" + +definition\<^marker>\tag important\ + has_laurent_expansion :: "(complex \ complex) \ complex fls \ bool" + (infixl "has'_laurent'_expansion" 60) + where "(f has_laurent_expansion F) \ + fls_conv_radius F > 0 \ eventually (\z. eval_fls F z = f z) (at 0)" + +lemma has_laurent_expansion_schematicI: + "f has_laurent_expansion F \ F = G \ f has_laurent_expansion G" + by simp + +lemma has_laurent_expansion_cong: + assumes "eventually (\x. f x = g x) (at 0)" "F = G" + shows "(f has_laurent_expansion F) \ (g has_laurent_expansion G)" +proof - + have "eventually (\z. eval_fls F z = g z) (at 0)" + if "eventually (\z. eval_fls F z = f z) (at 0)" "eventually (\x. f x = g x) (at 0)" for f g + using that by eventually_elim auto + from this[of f g] this[of g f] show ?thesis + using assms by (auto simp: eq_commute has_laurent_expansion_def) +qed + +lemma has_laurent_expansion_cong': + assumes "eventually (\x. f x = g x) (at z)" "F = G" "z = z'" + shows "((\x. f (z + x)) has_laurent_expansion F) \ ((\x. g (z' + x)) has_laurent_expansion G)" + by (intro has_laurent_expansion_cong) + (use assms in \auto simp: at_to_0' eventually_filtermap add_ac\) + +lemma fls_conv_radius_altdef: + "fls_conv_radius F = fps_conv_radius (fls_base_factor_to_fps F)" +proof - + have "conv_radius (\n. fls_nth F (int n)) = conv_radius (\n. fls_nth F (int n + fls_subdegree F))" + proof (cases "fls_subdegree F \ 0") + case True + hence "conv_radius (\n. fls_nth F (int n + fls_subdegree F)) = + conv_radius (\n. fls_nth F (int (n + nat (fls_subdegree F))))" + by auto + thus ?thesis + by (subst (asm) conv_radius_shift) auto + next + case False + hence "conv_radius (\n. fls_nth F (int n)) = + conv_radius (\n. fls_nth F (fls_subdegree F + int (n + nat (-fls_subdegree F))))" + by auto + thus ?thesis + by (subst (asm) conv_radius_shift) (auto simp: add_ac) + qed + thus ?thesis + by (simp add: fls_conv_radius_def fps_conv_radius_def) +qed + +lemma eval_fps_of_nat [simp]: "eval_fps (of_nat n) z = of_nat n" + and eval_fps_of_int [simp]: "eval_fps (of_int m) z = of_int m" + by (simp_all flip: fps_of_nat fps_of_int) + +lemma fls_subdegree_numeral [simp]: "fls_subdegree (numeral n) = 0" + by (metis fls_subdegree_of_nat of_nat_numeral) + +lemma fls_regpart_numeral [simp]: "fls_regpart (numeral n) = numeral n" + by (metis fls_regpart_of_nat of_nat_numeral) + +lemma fps_conv_radius_of_nat [simp]: "fps_conv_radius (of_nat n) = \" + and fps_conv_radius_of_int [simp]: "fps_conv_radius (of_int m) = \" + by (simp_all flip: fps_of_nat fps_of_int) + +lemma fps_conv_radius_fls_regpart: "fps_conv_radius (fls_regpart F) = fls_conv_radius F" + by (simp add: fls_conv_radius_def) + +lemma fls_conv_radius_0 [simp]: "fls_conv_radius 0 = \" + and fls_conv_radius_1 [simp]: "fls_conv_radius 1 = \" + and fls_conv_radius_const [simp]: "fls_conv_radius (fls_const c) = \" + and fls_conv_radius_numeral [simp]: "fls_conv_radius (numeral num) = \" + and fls_conv_radius_of_nat [simp]: "fls_conv_radius (of_nat n) = \" + and fls_conv_radius_of_int [simp]: "fls_conv_radius (of_int m) = \" + and fls_conv_radius_X [simp]: "fls_conv_radius fls_X = \" + and fls_conv_radius_X_inv [simp]: "fls_conv_radius fls_X_inv = \" + and fls_conv_radius_X_intpow [simp]: "fls_conv_radius (fls_X_intpow m) = \" + by (simp_all add: fls_conv_radius_def fls_X_intpow_regpart) + +lemma fls_conv_radius_shift [simp]: "fls_conv_radius (fls_shift n F) = fls_conv_radius F" + unfolding fls_conv_radius_altdef by (subst fls_base_factor_to_fps_shift) (rule refl) + +lemma fls_conv_radius_fps_to_fls [simp]: "fls_conv_radius (fps_to_fls F) = fps_conv_radius F" + by (simp add: fls_conv_radius_def) + +lemma fls_conv_radius_deriv [simp]: "fls_conv_radius (fls_deriv F) \ fls_conv_radius F" +proof - + have "fls_conv_radius (fls_deriv F) = fps_conv_radius (fls_regpart (fls_deriv F))" + by (simp add: fls_conv_radius_def) + also have "fls_regpart (fls_deriv F) = fps_deriv (fls_regpart F)" + by (intro fps_ext) (auto simp: add_ac) + also have "fps_conv_radius \ \ fls_conv_radius F" + by (simp add: fls_conv_radius_def fps_conv_radius_deriv) + finally show ?thesis . +qed + +lemma fls_conv_radius_uminus [simp]: "fls_conv_radius (-F) = fls_conv_radius F" + by (simp add: fls_conv_radius_def) + +lemma fls_conv_radius_add: "fls_conv_radius (F + G) \ min (fls_conv_radius F) (fls_conv_radius G)" + by (simp add: fls_conv_radius_def fps_conv_radius_add) + +lemma fls_conv_radius_diff: "fls_conv_radius (F - G) \ min (fls_conv_radius F) (fls_conv_radius G)" + by (simp add: fls_conv_radius_def fps_conv_radius_diff) + +lemma fls_conv_radius_mult: "fls_conv_radius (F * G) \ min (fls_conv_radius F) (fls_conv_radius G)" +proof (cases "F = 0 \ G = 0") + case False + hence [simp]: "F \ 0" "G \ 0" + by auto + have "fls_conv_radius (F * G) = fps_conv_radius (fls_regpart (fls_shift (fls_subdegree F + fls_subdegree G) (F * G)))" + by (simp add: fls_conv_radius_altdef) + also have "fls_regpart (fls_shift (fls_subdegree F + fls_subdegree G) (F * G)) = + fls_base_factor_to_fps F * fls_base_factor_to_fps G" + by (simp add: fls_times_def) + also have "fps_conv_radius \ \ min (fls_conv_radius F) (fls_conv_radius G)" + unfolding fls_conv_radius_altdef by (rule fps_conv_radius_mult) + finally show ?thesis . +qed auto + +lemma fps_conv_radius_add_ge: + "fps_conv_radius F \ r \ fps_conv_radius G \ r \ fps_conv_radius (F + G) \ r" + using fps_conv_radius_add[of F G] by (simp add: min_def split: if_splits) + +lemma fps_conv_radius_diff_ge: + "fps_conv_radius F \ r \ fps_conv_radius G \ r \ fps_conv_radius (F - G) \ r" + using fps_conv_radius_diff[of F G] by (simp add: min_def split: if_splits) + +lemma fps_conv_radius_mult_ge: + "fps_conv_radius F \ r \ fps_conv_radius G \ r \ fps_conv_radius (F * G) \ r" + using fps_conv_radius_mult[of F G] by (simp add: min_def split: if_splits) + +lemma fls_conv_radius_add_ge: + "fls_conv_radius F \ r \ fls_conv_radius G \ r \ fls_conv_radius (F + G) \ r" + using fls_conv_radius_add[of F G] by (simp add: min_def split: if_splits) + +lemma fls_conv_radius_diff_ge: + "fls_conv_radius F \ r \ fls_conv_radius G \ r \ fls_conv_radius (F - G) \ r" + using fls_conv_radius_diff[of F G] by (simp add: min_def split: if_splits) + +lemma fls_conv_radius_mult_ge: + "fls_conv_radius F \ r \ fls_conv_radius G \ r \ fls_conv_radius (F * G) \ r" + using fls_conv_radius_mult[of F G] by (simp add: min_def split: if_splits) + +lemma fls_conv_radius_power: "fls_conv_radius (F ^ n) \ fls_conv_radius F" + by (induction n) (auto intro!: fls_conv_radius_mult_ge) + +lemma eval_fls_0 [simp]: "eval_fls 0 z = 0" + and eval_fls_1 [simp]: "eval_fls 1 z = 1" + and eval_fls_const [simp]: "eval_fls (fls_const c) z = c" + and eval_fls_numeral [simp]: "eval_fls (numeral num) z = numeral num" + and eval_fls_of_nat [simp]: "eval_fls (of_nat n) z = of_nat n" + and eval_fls_of_int [simp]: "eval_fls (of_int m) z = of_int m" + and eval_fls_X [simp]: "eval_fls fls_X z = z" + and eval_fls_X_intpow [simp]: "eval_fls (fls_X_intpow m) z = z powi m" + by (simp_all add: eval_fls_def) + +lemma eval_fls_at_0: "eval_fls F 0 = (if fls_subdegree F \ 0 then fls_nth F 0 else 0)" + by (cases "fls_subdegree F = 0") + (simp_all add: eval_fls_def fls_regpart_def eval_fps_at_0) + +lemma eval_fps_to_fls: + assumes "norm z < fps_conv_radius F" + shows "eval_fls (fps_to_fls F) z = eval_fps F z" +proof (cases "F = 0") + case [simp]: False + have "eval_fps F z = eval_fps (unit_factor F * normalize F) z" + by (metis unit_factor_mult_normalize) + also have "\ = eval_fps (unit_factor F * fps_X ^ subdegree F) z" + by simp + also have "\ = eval_fps (unit_factor F) z * z ^ subdegree F" + using assms by (subst eval_fps_mult) auto + also have "\ = eval_fls (fps_to_fls F) z" + unfolding eval_fls_def fls_base_factor_to_fps_to_fls fls_subdegree_fls_to_fps + power_int_of_nat .. + finally show ?thesis .. +qed auto + +lemma eval_fls_shift: + assumes [simp]: "z \ 0" + shows "eval_fls (fls_shift n F) z = eval_fls F z * z powi -n" +proof (cases "F = 0") + case [simp]: False + show ?thesis + unfolding eval_fls_def + by (subst fls_base_factor_to_fps_shift, subst fls_shift_subdegree[OF \F \ 0\], subst power_int_diff) + (auto simp: power_int_minus divide_simps) +qed auto + +lemma eval_fls_add: + assumes "ereal (norm z) < fls_conv_radius F" "ereal (norm z) < fls_conv_radius G" "z \ 0" + shows "eval_fls (F + G) z = eval_fls F z + eval_fls G z" + using assms +proof (induction "fls_subdegree F" "fls_subdegree G" arbitrary: F G rule: linorder_wlog) + case (sym F G) + show ?case + using sym(1)[of G F] sym(2-) by (simp add: add_ac) +next + case (le F G) + show ?case + proof (cases "F = 0 \ G = 0") + case False + hence [simp]: "F \ 0" "G \ 0" + by auto + note [simp] = \z \ 0\ + define F' G' where "F' = fls_base_factor_to_fps F" "G' = fls_base_factor_to_fps G" + define m n where "m = fls_subdegree F" "n = fls_subdegree G" + have "m \ n" + using le by (auto simp: m_n_def) + have conv1: "ereal (cmod z) < fps_conv_radius F'" "ereal (cmod z) < fps_conv_radius G'" + using assms le by (simp_all add: F'_G'_def fls_conv_radius_altdef) + have conv2: "ereal (cmod z) < fps_conv_radius (G' * fps_X ^ nat (n - m))" + using conv1 by (intro less_le_trans[OF _ fps_conv_radius_mult]) auto + have conv3: "ereal (cmod z) < fps_conv_radius (F' + G' * fps_X ^ nat (n - m))" + using conv1 conv2 by (intro less_le_trans[OF _ fps_conv_radius_add]) auto + + have "eval_fls F z + eval_fls G z = eval_fps F' z * z powi m + eval_fps G' z * z powi n" + unfolding eval_fls_def m_n_def[symmetric] F'_G'_def[symmetric] + by (simp add: power_int_add algebra_simps) + also have "\ = (eval_fps F' z + eval_fps G' z * z powi (n - m)) * z powi m" + by (simp add: algebra_simps power_int_diff) + also have "eval_fps G' z * z powi (n - m) = eval_fps (G' * fps_X ^ nat (n - m)) z" + using assms \m \ n\ conv1 by (subst eval_fps_mult) (auto simp: power_int_def) + also have "eval_fps F' z + \ = eval_fps (F' + G' * fps_X ^ nat (n - m)) z" + using conv1 conv2 by (subst eval_fps_add) auto + also have "\ = eval_fls (fps_to_fls (F' + G' * fps_X ^ nat (n - m))) z" + using conv3 by (subst eval_fps_to_fls) auto + also have "\ * z powi m = eval_fls (fls_shift (-m) (fps_to_fls (F' + G' * fps_X ^ nat (n - m)))) z" + by (subst eval_fls_shift) auto + also have "fls_shift (-m) (fps_to_fls (F' + G' * fps_X ^ nat (n - m))) = F + G" + using \m \ n\ + by (simp add: fls_times_fps_to_fls fps_to_fls_power fls_X_power_conv_shift_1 + fls_shifted_times_simps F'_G'_def m_n_def) + finally show ?thesis .. + qed auto +qed + +lemma eval_fls_minus: + assumes "ereal (norm z) < fls_conv_radius F" + shows "eval_fls (-F) z = -eval_fls F z" + using assms by (simp add: eval_fls_def eval_fps_minus fls_conv_radius_altdef) + +lemma eval_fls_diff: + assumes "ereal (norm z) < fls_conv_radius F" "ereal (norm z) < fls_conv_radius G" + and [simp]: "z \ 0" + shows "eval_fls (F - G) z = eval_fls F z - eval_fls G z" +proof - + have "eval_fls (F + (-G)) z = eval_fls F z - eval_fls G z" + using assms by (subst eval_fls_add) (auto simp: eval_fls_minus) + thus ?thesis + by simp +qed + +lemma eval_fls_mult: + assumes "ereal (norm z) < fls_conv_radius F" "ereal (norm z) < fls_conv_radius G" "z \ 0" + shows "eval_fls (F * G) z = eval_fls F z * eval_fls G z" +proof (cases "F = 0 \ G = 0") + case False + hence [simp]: "F \ 0" "G \ 0" + by auto + note [simp] = \z \ 0\ + define F' G' where "F' = fls_base_factor_to_fps F" "G' = fls_base_factor_to_fps G" + define m n where "m = fls_subdegree F" "n = fls_subdegree G" + have "eval_fls F z * eval_fls G z = (eval_fps F' z * eval_fps G' z) * z powi (m + n)" + unfolding eval_fls_def m_n_def[symmetric] F'_G'_def[symmetric] + by (simp add: power_int_add algebra_simps) + also have "\ = eval_fps (F' * G') z * z powi (m + n)" + using assms by (subst eval_fps_mult) (auto simp: F'_G'_def fls_conv_radius_altdef) + also have "\ = eval_fls (F * G) z" + by (simp add: eval_fls_def F'_G'_def m_n_def) (simp add: fls_times_def) + finally show ?thesis .. +qed auto + +lemma eval_fls_power: + assumes "ereal (norm z) < fls_conv_radius F" "z \ 0" + shows "eval_fls (F ^ n) z = eval_fls F z ^ n" +proof (induction n) + case (Suc n) + have "eval_fls (F ^ Suc n) z = eval_fls (F * F ^ n) z" + by simp + also have "\ = eval_fls F z * eval_fls (F ^ n) z" + using assms by (subst eval_fls_mult) (auto intro!: less_le_trans[OF _ fls_conv_radius_power]) + finally show ?case + using Suc by simp +qed auto + +lemma norm_summable_fls: + "norm z < fls_conv_radius f \ summable (\n. norm (fls_nth f n * z ^ n))" + using norm_summable_fps[of z "fls_regpart f"] by (simp add: fls_conv_radius_def) + +lemma norm_summable_fls': + "norm z < fls_conv_radius f \ summable (\n. norm (fls_nth f (n + fls_subdegree f) * z ^ n))" + using norm_summable_fps[of z "fls_base_factor_to_fps f"] by (simp add: fls_conv_radius_altdef) + +lemma summable_fls: + "norm z < fls_conv_radius f \ summable (\n. fls_nth f n * z ^ n)" + by (rule summable_norm_cancel[OF norm_summable_fls]) + +theorem sums_eval_fls: + fixes f + defines "n \ fls_subdegree f" + assumes "norm z < fls_conv_radius f" and "z \ 0 \ n \ 0" + shows "(\k. fls_nth f (int k + n) * z powi (int k + n)) sums eval_fls f z" +proof (cases "z = 0") + case [simp]: False + have "(\k. fps_nth (fls_base_factor_to_fps f) k * z ^ k * z powi n) sums + (eval_fps (fls_base_factor_to_fps f) z * z powi n)" + using assms(2) by (intro sums_eval_fps sums_mult2) (auto simp: fls_conv_radius_altdef) + thus ?thesis + by (simp add: power_int_add n_def eval_fls_def mult_ac) +next + case [simp]: True + with assms have "n \ 0" + by auto + have "(\k. fls_nth f (int k + n) * z powi (int k + n)) sums + (\k\(if n \ 0 then {nat (-n)} else {}). fls_nth f (int k + n) * z powi (int k + n))" + by (intro sums_finite) (auto split: if_splits) + also have "\ = eval_fls f z" + using \n \ 0\ by (auto simp: eval_fls_at_0 n_def not_le) + finally show ?thesis . +qed + +lemma holomorphic_on_eval_fls: + fixes f + defines "n \ fls_subdegree f" + assumes "A \ eball 0 (fls_conv_radius f) - (if n \ 0 then {} else {0})" + shows "eval_fls f holomorphic_on A" +proof (cases "n \ 0") + case True + have "eval_fls f = (\z. eval_fps (fls_base_factor_to_fps f) z * z ^ nat n)" + using True by (simp add: fun_eq_iff eval_fls_def power_int_def n_def) + moreover have "\ holomorphic_on A" + using True assms(2) by (intro holomorphic_intros) (auto simp: fls_conv_radius_altdef) + ultimately show ?thesis + by simp +next + case False + show ?thesis using assms + unfolding eval_fls_def by (intro holomorphic_intros) (auto simp: fls_conv_radius_altdef) +qed + +lemma holomorphic_on_eval_fls' [holomorphic_intros]: + assumes "g holomorphic_on A" + assumes "g ` A \ eball 0 (fls_conv_radius f) - (if fls_subdegree f \ 0 then {} else {0})" + shows "(\x. eval_fls f (g x)) holomorphic_on A" +proof - + have "eval_fls f \ g holomorphic_on A" + by (intro holomorphic_on_compose[OF assms(1) holomorphic_on_eval_fls]) (use assms in auto) + thus ?thesis + by (simp add: o_def) +qed + +lemma continuous_on_eval_fls: + fixes f + defines "n \ fls_subdegree f" + assumes "A \ eball 0 (fls_conv_radius f) - (if n \ 0 then {} else {0})" + shows "continuous_on A (eval_fls f)" + by (intro holomorphic_on_imp_continuous_on holomorphic_on_eval_fls) + (use assms in auto) + +lemma continuous_on_eval_fls' [continuous_intros]: + fixes f + defines "n \ fls_subdegree f" + assumes "g ` A \ eball 0 (fls_conv_radius f) - (if n \ 0 then {} else {0})" + assumes "continuous_on A g" + shows "continuous_on A (\x. eval_fls f (g x))" + using assms(3) + by (intro continuous_on_compose2[OF continuous_on_eval_fls _ assms(2)]) + (auto simp: n_def) + +lemmas has_field_derivative_eval_fps' [derivative_intros] = + DERIV_chain2[OF has_field_derivative_eval_fps] + +lemma fps_deriv_fls_regpart: "fps_deriv (fls_regpart F) = fls_regpart (fls_deriv F)" + by (intro fps_ext) (auto simp: add_ac) + +(* TODO: generalise for nonneg subdegree *) +lemma has_field_derivative_eval_fls: + assumes "z \ eball 0 (fls_conv_radius f) - {0}" + shows "(eval_fls f has_field_derivative eval_fls (fls_deriv f) z) (at z within A)" +proof - + define g where "g = fls_base_factor_to_fps f" + define n where "n = fls_subdegree f" + have [simp]: "fps_conv_radius g = fls_conv_radius f" + by (simp add: fls_conv_radius_altdef g_def) + have conv1: "fps_conv_radius (fps_deriv g * fps_X) \ fls_conv_radius f" + by (intro fps_conv_radius_mult_ge order.trans[OF _ fps_conv_radius_deriv]) auto + have conv2: "fps_conv_radius (of_int n * g) \ fls_conv_radius f" + by (intro fps_conv_radius_mult_ge) auto + have conv3: "fps_conv_radius (fps_deriv g * fps_X + of_int n * g) \ fls_conv_radius f" + by (intro fps_conv_radius_add_ge conv1 conv2) + + have [simp]: "fps_conv_radius g = fls_conv_radius f" + by (simp add: g_def fls_conv_radius_altdef) + have "((\z. eval_fps g z * z powi fls_subdegree f) has_field_derivative + (eval_fps (fps_deriv g) z * z powi n + of_int n * z powi (n - 1) * eval_fps g z)) + (at z within A)" + using assms by (auto intro!: derivative_eq_intros simp: n_def) + also have "(\z. eval_fps g z * z powi fls_subdegree f) = eval_fls f" + by (simp add: eval_fls_def g_def fun_eq_iff) + also have "eval_fps (fps_deriv g) z * z powi n + of_int n * z powi (n - 1) * eval_fps g z = + (z * eval_fps (fps_deriv g) z + of_int n * eval_fps g z) * z powi (n - 1)" + using assms by (auto simp: power_int_diff field_simps) + also have "(z * eval_fps (fps_deriv g) z + of_int n * eval_fps g z) = + eval_fps (fps_deriv g * fps_X + of_int n * g) z" + using conv1 conv2 assms fps_conv_radius_deriv[of g] + by (subst eval_fps_add) (auto simp: eval_fps_mult) + also have "\ = eval_fls (fps_to_fls (fps_deriv g * fps_X + of_int n * g)) z" + using conv3 assms by (subst eval_fps_to_fls) auto + also have "\ * z powi (n - 1) = eval_fls (fls_shift (1 - n) (fps_to_fls (fps_deriv g * fps_X + of_int n * g))) z" + using assms by (subst eval_fls_shift) auto + also have "fls_shift (1 - n) (fps_to_fls (fps_deriv g * fps_X + of_int n * g)) = fls_deriv f" + by (intro fls_eqI) (auto simp: g_def n_def algebra_simps eq_commute[of _ "fls_subdegree f"]) + finally show ?thesis . +qed + +lemma eval_fls_deriv: + assumes "z \ eball 0 (fls_conv_radius F) - {0}" + shows "eval_fls (fls_deriv F) z = deriv (eval_fls F) z" + by (rule sym, rule DERIV_imp_deriv, rule has_field_derivative_eval_fls, rule assms) + +lemma analytic_on_eval_fls: + assumes "A \ eball 0 (fls_conv_radius f) - (if fls_subdegree f \ 0 then {} else {0})" + shows "eval_fls f analytic_on A" +proof (rule analytic_on_subset [OF _ assms]) + show "eval_fls f analytic_on eball 0 (fls_conv_radius f) - (if fls_subdegree f \ 0 then {} else {0})" + using holomorphic_on_eval_fls[OF order.refl] + by (subst analytic_on_open) auto +qed + +lemma analytic_on_eval_fls' [analytic_intros]: + assumes "g analytic_on A" + assumes "g ` A \ eball 0 (fls_conv_radius f) - (if fls_subdegree f \ 0 then {} else {0})" + shows "(\x. eval_fls f (g x)) analytic_on A" +proof - + have "eval_fls f \ g analytic_on A" + by (intro analytic_on_compose[OF assms(1) analytic_on_eval_fls]) (use assms in auto) + thus ?thesis + by (simp add: o_def) +qed + +lemma continuous_eval_fls [continuous_intros]: + assumes "z \ eball 0 (fls_conv_radius F) - (if fls_subdegree F \ 0 then {} else {0})" + shows "continuous (at z within A) (eval_fls F)" +proof - + have "isCont (eval_fls F) z" + using continuous_on_eval_fls[OF order.refl] assms + by (subst (asm) continuous_on_eq_continuous_at) auto + thus ?thesis + using continuous_at_imp_continuous_at_within by blast +qed + + + + +named_theorems laurent_expansion_intros + +lemma has_laurent_expansion_imp_asymp_equiv_0: + assumes F: "f has_laurent_expansion F" + defines "n \ fls_subdegree F" + shows "f \[at 0] (\z. fls_nth F n * z powi n)" +proof (cases "F = 0") + case True + thus ?thesis using assms + by (auto simp: has_laurent_expansion_def) +next + case [simp]: False + define G where "G = fls_base_factor_to_fps F" + have "fls_conv_radius F > 0" + using F by (auto simp: has_laurent_expansion_def) + hence "isCont (eval_fps G) 0" + by (intro continuous_intros) (auto simp: G_def fps_conv_radius_fls_regpart zero_ereal_def) + hence lim: "eval_fps G \0\ eval_fps G 0" + by (meson isContD) + have [simp]: "fps_nth G 0 \ 0" + by (auto simp: G_def) + + have "f \[at 0] eval_fls F" + using F by (intro asymp_equiv_refl_ev) (auto simp: has_laurent_expansion_def eq_commute) + also have "\ = (\z. eval_fps G z * z powi n)" + by (intro ext) (simp_all add: eval_fls_def G_def n_def) + also have "\ \[at 0] (\z. fps_nth G 0 * z powi n)" using lim + by (intro asymp_equiv_intros tendsto_imp_asymp_equiv_const) (auto simp: eval_fps_at_0) + also have "fps_nth G 0 = fls_nth F n" + by (simp add: G_def n_def) + finally show ?thesis + by simp +qed + +lemma has_laurent_expansion_imp_asymp_equiv: + assumes F: "(\w. f (z + w)) has_laurent_expansion F" + defines "n \ fls_subdegree F" + shows "f \[at z] (\w. fls_nth F n * (w - z) powi n)" + using has_laurent_expansion_imp_asymp_equiv_0[OF assms(1)] unfolding n_def + by (simp add: at_to_0[of z] asymp_equiv_filtermap_iff add_ac) + + +lemmas [tendsto_intros del] = tendsto_power_int + +lemma has_laurent_expansion_imp_tendsto_0: + assumes F: "f has_laurent_expansion F" and "fls_subdegree F \ 0" + shows "f \0\ fls_nth F 0" +proof (rule asymp_equiv_tendsto_transfer) + show "(\z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) \[at 0] f" + by (rule asymp_equiv_symI, rule has_laurent_expansion_imp_asymp_equiv_0) fact + show "(\z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) \0\ fls_nth F 0" + by (rule tendsto_eq_intros refl | use assms(2) in simp)+ + (use assms(2) in \auto simp: power_int_0_left_If\) +qed + +lemma has_laurent_expansion_imp_tendsto: + assumes F: "(\w. f (z + w)) has_laurent_expansion F" and "fls_subdegree F \ 0" + shows "f \z\ fls_nth F 0" + using has_laurent_expansion_imp_tendsto_0[OF assms] + by (simp add: at_to_0[of z] filterlim_filtermap add_ac) + +lemma has_laurent_expansion_imp_filterlim_infinity_0: + assumes F: "f has_laurent_expansion F" and "fls_subdegree F < 0" + shows "filterlim f at_infinity (at 0)" +proof (rule asymp_equiv_at_infinity_transfer) + have [simp]: "F \ 0" + using assms(2) by auto + show "(\z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) \[at 0] f" + by (rule asymp_equiv_symI, rule has_laurent_expansion_imp_asymp_equiv_0) fact + show "filterlim (\z. fls_nth F (fls_subdegree F) * z powi fls_subdegree F) at_infinity (at 0)" + by (rule tendsto_mult_filterlim_at_infinity tendsto_const + filterlim_power_int_neg_at_infinity | use assms(2) in simp)+ + (auto simp: eventually_at_filter) +qed + +lemma has_laurent_expansion_imp_neg_fls_subdegree: + assumes F: "f has_laurent_expansion F" + and infy:"filterlim f at_infinity (at 0)" + shows "fls_subdegree F < 0" +proof (rule ccontr) + assume asm:"\ fls_subdegree F < 0" + define ff where "ff=(\z. fls_nth F (fls_subdegree F) + * z powi fls_subdegree F)" + + have "(ff \ (if fls_subdegree F =0 then fls_nth F 0 else 0)) (at 0)" + using asm unfolding ff_def + by (auto intro!: tendsto_eq_intros) + moreover have "filterlim ff at_infinity (at 0)" + proof (rule asymp_equiv_at_infinity_transfer) + show "f \[at 0] ff" unfolding ff_def + using has_laurent_expansion_imp_asymp_equiv_0[OF F] unfolding ff_def . + show "filterlim f at_infinity (at 0)" by fact + qed + ultimately show False + using not_tendsto_and_filterlim_at_infinity[of "at (0::complex)"] by auto +qed + +lemma has_laurent_expansion_imp_filterlim_infinity: + assumes F: "(\w. f (z + w)) has_laurent_expansion F" and "fls_subdegree F < 0" + shows "filterlim f at_infinity (at z)" + using has_laurent_expansion_imp_filterlim_infinity_0[OF assms] + by (simp add: at_to_0[of z] filterlim_filtermap add_ac) + +lemma has_laurent_expansion_imp_is_pole_0: + assumes F: "f has_laurent_expansion F" and "fls_subdegree F < 0" + shows "is_pole f 0" + using has_laurent_expansion_imp_filterlim_infinity_0[OF assms] + by (simp add: is_pole_def) + +lemma is_pole_0_imp_neg_fls_subdegree: + assumes F: "f has_laurent_expansion F" and "is_pole f 0" + shows "fls_subdegree F < 0" + using F assms(2) has_laurent_expansion_imp_neg_fls_subdegree is_pole_def + by blast + +lemma has_laurent_expansion_imp_is_pole: + assumes F: "(\x. f (z + x)) has_laurent_expansion F" and "fls_subdegree F < 0" + shows "is_pole f z" + using has_laurent_expansion_imp_is_pole_0[OF assms] + by (simp add: is_pole_shift_0') + +lemma is_pole_imp_neg_fls_subdegree: + assumes F: "(\x. f (z + x)) has_laurent_expansion F" and "is_pole f z" + shows "fls_subdegree F < 0" + apply (rule is_pole_0_imp_neg_fls_subdegree[OF F]) + using assms(2) is_pole_shift_0 by blast + +lemma is_pole_fls_subdegree_iff: + assumes "(\x. f (z + x)) has_laurent_expansion F" + shows "is_pole f z \ fls_subdegree F < 0" + using assms is_pole_imp_neg_fls_subdegree has_laurent_expansion_imp_is_pole + by auto + +lemma + assumes "f has_laurent_expansion F" + shows has_laurent_expansion_isolated_0: "isolated_singularity_at f 0" + and has_laurent_expansion_not_essential_0: "not_essential f 0" +proof - + from assms have "eventually (\z. eval_fls F z = f z) (at 0)" + by (auto simp: has_laurent_expansion_def) + then obtain r where r: "r > 0" "\z. z \ ball 0 r - {0} \ eval_fls F z = f z" + by (auto simp: eventually_at_filter ball_def eventually_nhds_metric) + + have "fls_conv_radius F > 0" + using assms by (auto simp: has_laurent_expansion_def) + then obtain R :: real where R: "R > 0" "R \ min r (fls_conv_radius F)" + using \r > 0\ by (metis dual_order.strict_implies_order ereal_dense2 ereal_less(2) min_def) + + have "eval_fls F holomorphic_on ball 0 R - {0}" + using r R by (intro holomorphic_intros ball_eball_mono Diff_mono) (auto simp: ereal_le_less) + also have "?this \ f holomorphic_on ball 0 R - {0}" + using r R by (intro holomorphic_cong) auto + also have "\ \ f analytic_on ball 0 R - {0}" + by (subst analytic_on_open) auto + finally show "isolated_singularity_at f 0" + unfolding isolated_singularity_at_def using \R > 0\ by blast + + show "not_essential f 0" + proof (cases "fls_subdegree F \ 0") + case True + hence "f \0\ fls_nth F 0" + by (intro has_laurent_expansion_imp_tendsto_0[OF assms]) + thus ?thesis + by (auto simp: not_essential_def) + next + case False + hence "is_pole f 0" + by (intro has_laurent_expansion_imp_is_pole_0[OF assms]) auto + thus ?thesis + by (auto simp: not_essential_def) + qed +qed + +lemma + assumes "(\w. f (z + w)) has_laurent_expansion F" + shows has_laurent_expansion_isolated: "isolated_singularity_at f z" + and has_laurent_expansion_not_essential: "not_essential f z" + using has_laurent_expansion_isolated_0[OF assms] has_laurent_expansion_not_essential_0[OF assms] + by (simp_all add: isolated_singularity_at_shift_0 not_essential_shift_0) + +lemma has_laurent_expansion_fps: + assumes "f has_fps_expansion F" + shows "f has_laurent_expansion fps_to_fls F" +proof - + from assms have radius: "0 < fps_conv_radius F" and eval: "\\<^sub>F z in nhds 0. eval_fps F z = f z" + by (auto simp: has_fps_expansion_def) + from eval have eval': "\\<^sub>F z in at 0. eval_fps F z = f z" + using eventually_at_filter eventually_mono by fastforce + moreover have "eventually (\z. z \ eball 0 (fps_conv_radius F) - {0}) (at 0)" + using radius by (intro eventually_at_in_open) (auto simp: zero_ereal_def) + ultimately have "eventually (\z. eval_fls (fps_to_fls F) z = f z) (at 0)" + by eventually_elim (auto simp: eval_fps_to_fls) + thus ?thesis using radius + by (auto simp: has_laurent_expansion_def) +qed + +lemma has_laurent_expansion_const [simp, intro, laurent_expansion_intros]: + "(\_. c) has_laurent_expansion fls_const c" + by (auto simp: has_laurent_expansion_def) + +lemma has_laurent_expansion_0 [simp, intro, laurent_expansion_intros]: + "(\_. 0) has_laurent_expansion 0" + by (auto simp: has_laurent_expansion_def) + +lemma has_fps_expansion_0_iff: "f has_fps_expansion 0 \ eventually (\z. f z = 0) (nhds 0)" + by (auto simp: has_fps_expansion_def) + +lemma has_laurent_expansion_1 [simp, intro, laurent_expansion_intros]: + "(\_. 1) has_laurent_expansion 1" + by (auto simp: has_laurent_expansion_def) + +lemma has_laurent_expansion_numeral [simp, intro, laurent_expansion_intros]: + "(\_. numeral n) has_laurent_expansion numeral n" + by (auto simp: has_laurent_expansion_def) + +lemma has_laurent_expansion_fps_X_power [laurent_expansion_intros]: + "(\x. x ^ n) has_laurent_expansion (fls_X_intpow n)" + by (auto simp: has_laurent_expansion_def) + +lemma has_laurent_expansion_fps_X_power_int [laurent_expansion_intros]: + "(\x. x powi n) has_laurent_expansion (fls_X_intpow n)" + by (auto simp: has_laurent_expansion_def) + +lemma has_laurent_expansion_fps_X [laurent_expansion_intros]: + "(\x. x) has_laurent_expansion fls_X" + by (auto simp: has_laurent_expansion_def) + +lemma has_laurent_expansion_cmult_left [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" + shows "(\x. c * f x) has_laurent_expansion fls_const c * F" +proof - + from assms have "eventually (\z. z \ eball 0 (fls_conv_radius F) - {0}) (at 0)" + by (intro eventually_at_in_open) (auto simp: has_laurent_expansion_def zero_ereal_def) + moreover from assms have "eventually (\z. eval_fls F z = f z) (at 0)" + by (auto simp: has_laurent_expansion_def) + ultimately have "eventually (\z. eval_fls (fls_const c * F) z = c * f z) (at 0)" + by eventually_elim (simp_all add: eval_fls_mult) + with assms show ?thesis + by (auto simp: has_laurent_expansion_def intro!: less_le_trans[OF _ fls_conv_radius_mult]) +qed + +lemma has_laurent_expansion_cmult_right [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" + shows "(\x. f x * c) has_laurent_expansion F * fls_const c" +proof - + have "F * fls_const c = fls_const c * F" + by (intro fls_eqI) (auto simp: mult.commute) + with has_laurent_expansion_cmult_left [OF assms] show ?thesis + by (simp add: mult.commute) +qed + +lemma has_fps_expansion_scaleR [fps_expansion_intros]: + fixes F :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps" + shows "f has_fps_expansion F \ (\x. c *\<^sub>R f x) has_fps_expansion fps_const (of_real c) * F" + unfolding scaleR_conv_of_real by (intro fps_expansion_intros) + +lemma has_laurent_expansion_scaleR [laurent_expansion_intros]: + "f has_laurent_expansion F \ (\x. c *\<^sub>R f x) has_laurent_expansion fls_const (of_real c) * F" + unfolding scaleR_conv_of_real by (intro laurent_expansion_intros) + +lemma has_laurent_expansion_minus [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" + shows "(\x. - f x) has_laurent_expansion -F" +proof - + from assms have "eventually (\x. x \ eball 0 (fls_conv_radius F) - {0}) (at 0)" + by (intro eventually_at_in_open) (auto simp: has_laurent_expansion_def zero_ereal_def) + moreover from assms have "eventually (\x. eval_fls F x = f x) (at 0)" + by (auto simp: has_laurent_expansion_def) + ultimately have "eventually (\x. eval_fls (-F) x = -f x) (at 0)" + by eventually_elim (auto simp: eval_fls_minus) + thus ?thesis using assms by (auto simp: has_laurent_expansion_def) +qed + +lemma has_laurent_expansion_add [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" "g has_laurent_expansion G" + shows "(\x. f x + g x) has_laurent_expansion F + G" +proof - + from assms have "0 < min (fls_conv_radius F) (fls_conv_radius G)" + by (auto simp: has_laurent_expansion_def) + also have "\ \ fls_conv_radius (F + G)" + by (rule fls_conv_radius_add) + finally have radius: "\ > 0" . + + from assms have "eventually (\x. x \ eball 0 (fls_conv_radius F) - {0}) (at 0)" + "eventually (\x. x \ eball 0 (fls_conv_radius G) - {0}) (at 0)" + by (intro eventually_at_in_open; force simp: has_laurent_expansion_def zero_ereal_def)+ + moreover have "eventually (\x. eval_fls F x = f x) (at 0)" + and "eventually (\x. eval_fls G x = g x) (at 0)" + using assms by (auto simp: has_laurent_expansion_def) + ultimately have "eventually (\x. eval_fls (F + G) x = f x + g x) (at 0)" + by eventually_elim (auto simp: eval_fls_add) + with radius show ?thesis by (auto simp: has_laurent_expansion_def) +qed + +lemma has_laurent_expansion_diff [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" "g has_laurent_expansion G" + shows "(\x. f x - g x) has_laurent_expansion F - G" + using has_laurent_expansion_add[of f F "\x. - g x" "-G"] assms + by (simp add: has_laurent_expansion_minus) + +lemma has_laurent_expansion_mult [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" "g has_laurent_expansion G" + shows "(\x. f x * g x) has_laurent_expansion F * G" +proof - + from assms have "0 < min (fls_conv_radius F) (fls_conv_radius G)" + by (auto simp: has_laurent_expansion_def) + also have "\ \ fls_conv_radius (F * G)" + by (rule fls_conv_radius_mult) + finally have radius: "\ > 0" . + + from assms have "eventually (\x. x \ eball 0 (fls_conv_radius F) - {0}) (at 0)" + "eventually (\x. x \ eball 0 (fls_conv_radius G) - {0}) (at 0)" + by (intro eventually_at_in_open; force simp: has_laurent_expansion_def zero_ereal_def)+ + moreover have "eventually (\x. eval_fls F x = f x) (at 0)" + and "eventually (\x. eval_fls G x = g x) (at 0)" + using assms by (auto simp: has_laurent_expansion_def) + ultimately have "eventually (\x. eval_fls (F * G) x = f x * g x) (at 0)" + by eventually_elim (auto simp: eval_fls_mult) + with radius show ?thesis by (auto simp: has_laurent_expansion_def) +qed + +lemma has_fps_expansion_power [fps_expansion_intros]: + fixes F :: "'a :: {banach, real_normed_div_algebra, comm_ring_1} fps" + shows "f has_fps_expansion F \ (\x. f x ^ m) has_fps_expansion F ^ m" + by (induction m) (auto intro!: fps_expansion_intros) + +lemma has_laurent_expansion_power [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" + shows "(\x. f x ^ n) has_laurent_expansion F ^ n" + by (induction n) (auto intro!: laurent_expansion_intros assms) + +lemma has_laurent_expansion_sum [laurent_expansion_intros]: + assumes "\x. x \ I \ f x has_laurent_expansion F x" + shows "(\y. \x\I. f x y) has_laurent_expansion (\x\I. F x)" + using assms by (induction I rule: infinite_finite_induct) (auto intro!: laurent_expansion_intros) + +lemma has_laurent_expansion_prod [laurent_expansion_intros]: + assumes "\x. x \ I \ f x has_laurent_expansion F x" + shows "(\y. \x\I. f x y) has_laurent_expansion (\x\I. F x)" + using assms by (induction I rule: infinite_finite_induct) (auto intro!: laurent_expansion_intros) + +lemma has_laurent_expansion_deriv [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" + shows "deriv f has_laurent_expansion fls_deriv F" +proof - + have "eventually (\z. z \ eball 0 (fls_conv_radius F) - {0}) (at 0)" + using assms by (intro eventually_at_in_open) + (auto simp: has_laurent_expansion_def zero_ereal_def) + moreover from assms have "eventually (\z. eval_fls F z = f z) (at 0)" + by (auto simp: has_laurent_expansion_def) + then obtain s where "open s" "0 \ s" and s: "\w. w \ s - {0} \ eval_fls F w = f w" + by (auto simp: eventually_nhds eventually_at_filter) + hence "eventually (\w. w \ s - {0}) (at 0)" + by (intro eventually_at_in_open) auto + ultimately have "eventually (\z. eval_fls (fls_deriv F) z = deriv f z) (at 0)" + proof eventually_elim + case (elim z) + hence "eval_fls (fls_deriv F) z = deriv (eval_fls F) z" + by (simp add: eval_fls_deriv) + also have "eventually (\w. w \ s - {0}) (nhds z)" + using elim and \open s\ by (intro eventually_nhds_in_open) auto + hence "eventually (\w. eval_fls F w = f w) (nhds z)" + by eventually_elim (use s in auto) + hence "deriv (eval_fls F) z = deriv f z" + by (intro deriv_cong_ev refl) + finally show ?case . + qed + with assms show ?thesis + by (auto simp: has_laurent_expansion_def intro!: less_le_trans[OF _ fls_conv_radius_deriv]) +qed + +lemma has_laurent_expansion_shift [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" + shows "(\x. f x * x powi n) has_laurent_expansion (fls_shift (-n) F)" +proof - + have "eventually (\x. x \ eball 0 (fls_conv_radius F) - {0}) (at 0)" + using assms by (intro eventually_at_in_open) (auto simp: has_laurent_expansion_def zero_ereal_def) + moreover have "eventually (\x. eval_fls F x = f x) (at 0)" + using assms by (auto simp: has_laurent_expansion_def) + ultimately have "eventually (\x. eval_fls (fls_shift (-n) F) x = f x * x powi n) (at 0)" + by eventually_elim (auto simp: eval_fls_shift assms) + with assms show ?thesis by (auto simp: has_laurent_expansion_def) +qed + +lemma has_laurent_expansion_shift' [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" + shows "(\x. f x * x powi (-n)) has_laurent_expansion (fls_shift n F)" + using has_laurent_expansion_shift[OF assms, of "-n"] by simp + + +lemma has_laurent_expansion_deriv': + assumes "f has_laurent_expansion F" + assumes "open A" "0 \ A" "\x. x \ A - {0} \ (f has_field_derivative f' x) (at x)" + shows "f' has_laurent_expansion fls_deriv F" +proof - + have "deriv f has_laurent_expansion fls_deriv F" + by (intro laurent_expansion_intros assms) + also have "?this \ ?thesis" + proof (intro has_laurent_expansion_cong refl) + have "eventually (\z. z \ A - {0}) (at 0)" + by (intro eventually_at_in_open assms) + thus "eventually (\z. deriv f z = f' z) (at 0)" + by eventually_elim (auto intro!: DERIV_imp_deriv assms) + qed + finally show ?thesis . +qed + +definition laurent_expansion :: "(complex \ complex) \ complex \ complex fls" where + "laurent_expansion f z = + (if eventually (\z. f z = 0) (at z) then 0 + else fls_shift (-zorder f z) (fps_to_fls (fps_expansion (zor_poly f z) z)))" + +lemma laurent_expansion_cong: + assumes "eventually (\w. f w = g w) (at z)" "z = z'" + shows "laurent_expansion f z = laurent_expansion g z'" + unfolding laurent_expansion_def + using zor_poly_cong[OF assms(1,2)] zorder_cong[OF assms] assms + by (intro if_cong refl) (auto elim: eventually_elim2) + +theorem not_essential_has_laurent_expansion_0: + assumes "isolated_singularity_at f 0" "not_essential f 0" + shows "f has_laurent_expansion laurent_expansion f 0" +proof (cases "\\<^sub>F w in at 0. f w \ 0") + case False + have "(\_. 0) has_laurent_expansion 0" + by simp + also have "?this \ f has_laurent_expansion 0" + using False by (intro has_laurent_expansion_cong) (auto simp: frequently_def) + finally show ?thesis + using False by (simp add: laurent_expansion_def frequently_def) +next + case True + define n where "n = zorder f 0" + obtain r where r: "zor_poly f 0 0 \ 0" "zor_poly f 0 holomorphic_on cball 0 r" "r > 0" + "\w\cball 0 r - {0}. f w = zor_poly f 0 w * w powr of_int n \ + zor_poly f 0 w \ 0" + using zorder_exist[OF assms True] unfolding n_def by auto + have holo: "zor_poly f 0 holomorphic_on ball 0 r" + by (rule holomorphic_on_subset[OF r(2)]) auto + + define F where "F = fps_expansion (zor_poly f 0) 0" + have F: "zor_poly f 0 has_fps_expansion F" + unfolding F_def by (rule has_fps_expansion_fps_expansion[OF _ _ holo]) (use \r > 0\ in auto) + have "(\z. zor_poly f 0 z * z powi n) has_laurent_expansion fls_shift (-n) (fps_to_fls F)" + by (intro laurent_expansion_intros has_laurent_expansion_fps[OF F]) + also have "?this \ f has_laurent_expansion fls_shift (-n) (fps_to_fls F)" + by (intro has_laurent_expansion_cong refl eventually_mono[OF eventually_at_in_open[of "ball 0 r"]]) + (use r in \auto simp: complex_powr_of_int\) + finally show ?thesis using True + by (simp add: laurent_expansion_def F_def n_def frequently_def) +qed + +lemma not_essential_has_laurent_expansion: + assumes "isolated_singularity_at f z" "not_essential f z" + shows "(\x. f (z + x)) has_laurent_expansion laurent_expansion f z" +proof - + from assms(1) have iso:"isolated_singularity_at (\x. f (z + x)) 0" + by (simp add: isolated_singularity_at_shift_0) + moreover from assms(2) have ness:"not_essential (\x. f (z + x)) 0" + by (simp add: not_essential_shift_0) + ultimately have "(\x. f (z + x)) has_laurent_expansion laurent_expansion (\x. f (z + x)) 0" + by (rule not_essential_has_laurent_expansion_0) + + also have "\ = laurent_expansion f z" + proof (cases "\\<^sub>F w in at z. f w \ 0") + case False + then have "\\<^sub>F w in at z. f w = 0" using not_frequently by force + then have "laurent_expansion (\x. f (z + x)) 0 = 0" + by (smt (verit, best) add.commute eventually_at_to_0 eventually_mono + laurent_expansion_def) + moreover have "laurent_expansion f z = 0" + using \\\<^sub>F w in at z. f w = 0\ unfolding laurent_expansion_def by auto + ultimately show ?thesis by auto + next + case True + define df where "df=zor_poly (\x. f (z + x)) 0" + define g where "g=(\u. u-z)" + + have "fps_expansion df 0 + = fps_expansion (df o g) z" + proof - + have "\\<^sub>F w in at 0. f (z + w) \ 0" using True + by (smt (verit, best) add.commute eventually_at_to_0 + eventually_mono not_frequently) + from zorder_exist[OF iso ness this,folded df_def] + obtain r where "r>0" and df_holo:"df holomorphic_on cball 0 r" and "df 0 \ 0" + "\w\cball 0 r - {0}. + f (z + w) = df w * w powr of_int (zorder (\w. f (z + w)) 0) \ + df w \ 0" + by auto + then have df_nz:"\w\ball 0 r. df w\0" by auto + + have "(deriv ^^ n) df 0 = (deriv ^^ n) (df \ g) z" for n + unfolding comp_def g_def + proof (subst higher_deriv_compose_linear'[where u=1 and c="-z",simplified]) + show "df holomorphic_on ball 0 r" + using df_holo by auto + show "open (ball z r)" "open (ball 0 r)" "z \ ball z r" + using \r>0\ by auto + show " \w. w \ ball z r \ w - z \ ball 0 r" + by (simp add: dist_norm) + qed auto + then show ?thesis + unfolding fps_expansion_def by auto + qed + also have "... = fps_expansion (zor_poly f z) z" + proof (rule fps_expansion_cong) + have "\\<^sub>F w in nhds z. zor_poly f z w + = zor_poly (\u. f (z + u)) 0 (w - z)" + apply (rule zor_poly_shift) + using True assms by auto + then show "\\<^sub>F w in nhds z. (df \ g) w = zor_poly f z w" + unfolding df_def g_def comp_def + by (auto elim:eventually_mono) + qed + finally show ?thesis unfolding df_def + by (auto simp: laurent_expansion_def at_to_0[of z] + eventually_filtermap add_ac zorder_shift') + qed + finally show ?thesis . +qed + +lemma has_fps_expansion_to_laurent: + "f has_fps_expansion F \ f has_laurent_expansion fps_to_fls F \ f 0 = fps_nth F 0" +proof safe + assume *: "f has_laurent_expansion fps_to_fls F" "f 0 = fps_nth F 0" + have "eventually (\z. z \ eball 0 (fps_conv_radius F)) (nhds 0)" + using * by (intro eventually_nhds_in_open) (auto simp: has_laurent_expansion_def zero_ereal_def) + moreover have "eventually (\z. z \ 0 \ eval_fls (fps_to_fls F) z = f z) (nhds 0)" + using * by (auto simp: has_laurent_expansion_def eventually_at_filter) + ultimately have "eventually (\z. f z = eval_fps F z) (nhds 0)" + by eventually_elim + (auto simp: has_laurent_expansion_def eventually_at_filter eval_fps_at_0 eval_fps_to_fls *(2)) + thus "f has_fps_expansion F" + using * by (auto simp: has_fps_expansion_def has_laurent_expansion_def eq_commute) +next + assume "f has_fps_expansion F" + thus "f 0 = fps_nth F 0" + by (metis eval_fps_at_0 has_fps_expansion_imp_holomorphic) +qed (auto intro: has_laurent_expansion_fps) + +lemma eval_fps_fls_base_factor [simp]: + assumes "z \ 0" + shows "eval_fps (fls_base_factor_to_fps F) z = eval_fls F z * z powi -fls_subdegree F" + using assms unfolding eval_fls_def by (simp add: power_int_minus field_simps) + +lemma has_fps_expansion_imp_analytic_0: + assumes "f has_fps_expansion F" + shows "f analytic_on {0}" + by (meson analytic_at_two assms has_fps_expansion_imp_holomorphic) + +lemma has_fps_expansion_imp_analytic: + assumes "(\x. f (z + x)) has_fps_expansion F" + shows "f analytic_on {z}" +proof - + have "(\x. f (z + x)) analytic_on {0}" + by (rule has_fps_expansion_imp_analytic_0) fact + hence "(\x. f (z + x)) \ (\x. x - z) analytic_on {z}" + by (intro analytic_on_compose_gen analytic_intros) auto + thus ?thesis + by (simp add: o_def) +qed + +lemma is_pole_cong_asymp_equiv: + assumes "f \[at z] g" "z = z'" + shows "is_pole f z = is_pole g z'" + using asymp_equiv_at_infinity_transfer[OF assms(1)] + asymp_equiv_at_infinity_transfer[OF asymp_equiv_symI[OF assms(1)]] assms(2) + unfolding is_pole_def by auto + +lemma not_is_pole_const [simp]: "\is_pole (\_::'a::perfect_space. c :: complex) z" + using not_tendsto_and_filterlim_at_infinity[of "at z" "\_::'a. c" c] by (auto simp: is_pole_def) + +lemma has_laurent_expansion_imp_is_pole_iff: + assumes F: "(\x. f (z + x)) has_laurent_expansion F" + shows "is_pole f z \ fls_subdegree F < 0" +proof + assume pole: "is_pole f z" + have [simp]: "F \ 0" + proof + assume "F = 0" + hence "is_pole f z \ is_pole (\_. 0 :: complex) z" using assms + by (intro is_pole_cong) + (auto simp: has_laurent_expansion_def at_to_0[of z] eventually_filtermap add_ac) + with pole show False + by simp + qed + + note pole + also have "is_pole f z \ + is_pole (\w. fls_nth F (fls_subdegree F) * (w - z) powi fls_subdegree F) z" + using has_laurent_expansion_imp_asymp_equiv[OF F] by (intro is_pole_cong_asymp_equiv refl) + also have "\ \ is_pole (\w. (w - z) powi fls_subdegree F) z" + by simp + finally have pole': \ . + + have False if "fls_subdegree F \ 0" + proof - + have "(\w. (w - z) powi fls_subdegree F) holomorphic_on UNIV" + using that by (intro holomorphic_intros) auto + hence "\is_pole (\w. (w - z) powi fls_subdegree F) z" + by (meson UNIV_I not_is_pole_holomorphic open_UNIV) + with pole' show False + by simp + qed + thus "fls_subdegree F < 0" + by force +qed (use has_laurent_expansion_imp_is_pole[OF assms] in auto) + +lemma analytic_at_imp_has_fps_expansion_0: + assumes "f analytic_on {0}" + shows "f has_fps_expansion fps_expansion f 0" + using assms has_fps_expansion_fps_expansion analytic_at by fast + +lemma deriv_shift_0: "deriv f z = deriv (f \ (\x. z + x)) 0" +proof - + have *: "(f \ (+) z has_field_derivative D) (at z')" + if "(f has_field_derivative D) (at (z + z'))" for D z z' and f :: "'a \ 'a" + proof - + have "(f \ (+) z has_field_derivative D * 1) (at z')" + by (rule DERIV_chain that derivative_eq_intros refl)+ auto + thus ?thesis by simp + qed + have "(\D. (f has_field_derivative D) (at z)) = (\ D. (f \ (+) z has_field_derivative D) (at 0))" + using *[of f _ z 0] *[of "f \ (+) z" _ "-z" z] by (intro ext iffI) (auto simp: o_def) + thus ?thesis + by (simp add: deriv_def) +qed + +lemma deriv_shift_0': "NO_MATCH 0 z \ deriv f z = deriv (f \ (\x. z + x)) 0" + by (rule deriv_shift_0) + +lemma higher_deriv_shift_0: "(deriv ^^ n) f z = (deriv ^^ n) (f \ (\x. z + x)) 0" +proof (induction n arbitrary: f) + case (Suc n) + have "(deriv ^^ Suc n) f z = (deriv ^^ n) (deriv f) z" + by (subst funpow_Suc_right) auto + also have "\ = (deriv ^^ n) (\x. deriv f (z + x)) 0" + by (subst Suc) (auto simp: o_def) + also have "\ = (deriv ^^ n) (\x. deriv (\xa. f (z + x + xa)) 0) 0" + by (subst deriv_shift_0) (auto simp: o_def) + also have "(\x. deriv (\xa. f (z + x + xa)) 0) = deriv (\x. f (z + x))" + by (rule ext) (simp add: deriv_shift_0' o_def add_ac) + also have "(deriv ^^ n) \ 0 = (deriv ^^ Suc n) (f \ (\x. z + x)) 0" + by (subst funpow_Suc_right) (auto simp: o_def) + finally show ?case . +qed auto + +lemma higher_deriv_shift_0': "NO_MATCH 0 z \ (deriv ^^ n) f z = (deriv ^^ n) (f \ (\x. z + x)) 0" + by (rule higher_deriv_shift_0) + +lemma analytic_at_imp_has_fps_expansion: + assumes "f analytic_on {z}" + shows "(\x. f (z + x)) has_fps_expansion fps_expansion f z" +proof - + have "f \ (\x. z + x) analytic_on {0}" + by (intro analytic_on_compose_gen[OF _ assms] analytic_intros) auto + hence "(f \ (\x. z + x)) has_fps_expansion fps_expansion (f \ (\x. z + x)) 0" + unfolding o_def by (intro analytic_at_imp_has_fps_expansion_0) auto + also have "\ = fps_expansion f z" + by (simp add: fps_expansion_def higher_deriv_shift_0') + finally show ?thesis by (simp add: add_ac) +qed + +lemma has_laurent_expansion_zorder_0: + assumes "f has_laurent_expansion F" "F \ 0" + shows "zorder f 0 = fls_subdegree F" +proof - + define G where "G = fls_base_factor_to_fps F" + from assms obtain A where A: "0 \ A" "open A" "\x. x \ A - {0} \ eval_fls F x = f x" + unfolding has_laurent_expansion_def eventually_at_filter eventually_nhds + by blast + + show ?thesis + proof (rule zorder_eqI) + show "open (A \ eball 0 (fls_conv_radius F))" "0 \ A \ eball 0 (fls_conv_radius F)" + using assms A by (auto simp: has_laurent_expansion_def zero_ereal_def) + show "eval_fps G holomorphic_on A \ eball 0 (fls_conv_radius F)" + by (intro holomorphic_intros) (auto simp: fls_conv_radius_altdef G_def) + show "eval_fps G 0 \ 0" using \F \ 0\ + by (auto simp: eval_fps_at_0 G_def) + next + fix w :: complex assume "w \ A \ eball 0 (fls_conv_radius F)" "w \ 0" + thus "f w = eval_fps G w * (w - 0) powr of_int (fls_subdegree F)" + using A unfolding G_def + by (subst eval_fps_fls_base_factor) + (auto simp: complex_powr_of_int power_int_minus field_simps) + qed +qed + +lemma has_laurent_expansion_zorder: + assumes "(\w. f (z + w)) has_laurent_expansion F" "F \ 0" + shows "zorder f z = fls_subdegree F" + using has_laurent_expansion_zorder_0[OF assms] by (simp add: zorder_shift' add_ac) + +lemma has_fps_expansion_zorder_0: + assumes "f has_fps_expansion F" "F \ 0" + shows "zorder f 0 = int (subdegree F)" + using assms has_laurent_expansion_zorder_0[of f "fps_to_fls F"] + by (auto simp: has_fps_expansion_to_laurent fls_subdegree_fls_to_fps) + +lemma has_fps_expansion_zorder: + assumes "(\w. f (z + w)) has_fps_expansion F" "F \ 0" + shows "zorder f z = int (subdegree F)" + using has_fps_expansion_zorder_0[OF assms] + by (simp add: zorder_shift' add_ac) + +lemma has_fps_expansion_fls_base_factor_to_fps: + assumes "f has_laurent_expansion F" + defines "n \ fls_subdegree F" + defines "c \ fps_nth (fls_base_factor_to_fps F) 0" + shows "(\z. if z = 0 then c else f z * z powi -n) has_fps_expansion fls_base_factor_to_fps F" +proof - + have "(\z. f z * z powi -n) has_laurent_expansion fls_shift (-(-n)) F" + by (intro laurent_expansion_intros assms) + also have "fls_shift (-(-n)) F = fps_to_fls (fls_base_factor_to_fps F)" + by (simp add: n_def fls_shift_nonneg_subdegree) + also have "(\z. f z * z powi - n) has_laurent_expansion fps_to_fls (fls_base_factor_to_fps F) \ + (\z. if z = 0 then c else f z * z powi -n) has_laurent_expansion fps_to_fls (fls_base_factor_to_fps F)" + by (intro has_laurent_expansion_cong) (auto simp: eventually_at_filter) + also have "\ \ (\z. if z = 0 then c else f z * z powi -n) has_fps_expansion fls_base_factor_to_fps F" + by (subst has_fps_expansion_to_laurent) (auto simp: c_def) + finally show ?thesis . +qed + +lemma zero_has_laurent_expansion_imp_eq_0: + assumes "(\_. 0) has_laurent_expansion F" + shows "F = 0" +proof - + have "at (0 :: complex) \ bot" + by auto + moreover have "(\z. if z = 0 then fls_nth F (fls_subdegree F) else 0) has_fps_expansion + fls_base_factor_to_fps F" (is "?f has_fps_expansion _") + using has_fps_expansion_fls_base_factor_to_fps[OF assms] by (simp cong: if_cong) + hence "isCont ?f 0" + using has_fps_expansion_imp_continuous by blast + hence "?f \0\ fls_nth F (fls_subdegree F)" + by (auto simp: isCont_def) + moreover have "?f \0\ 0 \ (\_::complex. 0 :: complex) \0\ 0" + by (intro filterlim_cong) (auto simp: eventually_at_filter) + hence "?f \0\ 0" + by simp + ultimately have "fls_nth F (fls_subdegree F) = 0" + by (rule tendsto_unique) + thus ?thesis + by (meson nth_fls_subdegree_nonzero) +qed + +lemma has_laurent_expansion_unique: + assumes "f has_laurent_expansion F" "f has_laurent_expansion G" + shows "F = G" +proof - + from assms have "(\x. f x - f x) has_laurent_expansion F - G" + by (intro laurent_expansion_intros) + hence "(\_. 0) has_laurent_expansion F - G" + by simp + hence "F - G = 0" + by (rule zero_has_laurent_expansion_imp_eq_0) + thus ?thesis + by simp +qed + +lemma laurent_expansion_eqI: + assumes "(\x. f (z + x)) has_laurent_expansion F" + shows "laurent_expansion f z = F" + using assms has_laurent_expansion_isolated has_laurent_expansion_not_essential + has_laurent_expansion_unique not_essential_has_laurent_expansion by blast + +lemma laurent_expansion_0_eqI: + assumes "f has_laurent_expansion F" + shows "laurent_expansion f 0 = F" + using assms laurent_expansion_eqI[of f 0] by simp + +lemma has_laurent_expansion_nonzero_imp_eventually_nonzero: + assumes "f has_laurent_expansion F" "F \ 0" + shows "eventually (\x. f x \ 0) (at 0)" +proof (rule ccontr) + assume "\eventually (\x. f x \ 0) (at 0)" + with assms have "eventually (\x. f x = 0) (at 0)" + by (intro not_essential_frequently_0_imp_eventually_0 has_laurent_expansion_isolated + has_laurent_expansion_not_essential) + (auto simp: frequently_def) + hence "(f has_laurent_expansion 0) \ ((\_. 0) has_laurent_expansion 0)" + by (intro has_laurent_expansion_cong) auto + hence "f has_laurent_expansion 0" + by simp + with assms(1) have "F = 0" + using has_laurent_expansion_unique by blast + with \F \ 0\ show False + by contradiction +qed + +lemma has_laurent_expansion_eventually_nonzero_iff': + assumes "f has_laurent_expansion F" + shows "eventually (\x. f x \ 0) (at 0) \ F \ 0 " +proof + assume "\\<^sub>F x in at 0. f x \ 0" + moreover have "\ (\\<^sub>F x in at 0. f x \ 0)" if "F=0" + proof - + have "\\<^sub>F x in at 0. f x = 0" + using assms that unfolding has_laurent_expansion_def by simp + then show ?thesis unfolding not_eventually + by (auto elim:eventually_frequentlyE) + qed + ultimately show "F \ 0" by auto +qed (simp add:has_laurent_expansion_nonzero_imp_eventually_nonzero[OF assms]) + +lemma has_laurent_expansion_eventually_nonzero_iff: + assumes "(\w. f (z+w)) has_laurent_expansion F" + shows "eventually (\x. f x \ 0) (at z) \ F \ 0" + apply (subst eventually_at_to_0) + apply (rule has_laurent_expansion_eventually_nonzero_iff') + using assms by (simp add:add.commute) + +lemma has_laurent_expansion_inverse [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" + shows "(\x. inverse (f x)) has_laurent_expansion inverse F" +proof (cases "F = 0") + case True + thus ?thesis using assms + by (auto simp: has_laurent_expansion_def) +next + case False + define G where "G = laurent_expansion (\x. inverse (f x)) 0" + from False have ev: "eventually (\z. f z \ 0) (at 0)" + by (intro has_laurent_expansion_nonzero_imp_eventually_nonzero[OF assms]) + + have *: "(\x. inverse (f x)) has_laurent_expansion G" unfolding G_def + by (intro not_essential_has_laurent_expansion_0 isolated_singularity_at_inverse not_essential_inverse + has_laurent_expansion_isolated_0[OF assms] has_laurent_expansion_not_essential_0[OF assms]) + have "(\x. f x * inverse (f x)) has_laurent_expansion F * G" + by (intro laurent_expansion_intros assms *) + also have "?this \ (\x. 1) has_laurent_expansion F * G" + by (intro has_laurent_expansion_cong refl eventually_mono[OF ev]) auto + finally have "(\_. 1) has_laurent_expansion F * G" . + moreover have "(\_. 1) has_laurent_expansion 1" + by simp + ultimately have "F * G = 1" + using has_laurent_expansion_unique by blast + hence "G = inverse F" + using inverse_unique by blast + with * show ?thesis + by simp +qed + +lemma has_laurent_expansion_power_int [laurent_expansion_intros]: + "f has_laurent_expansion F \ (\x. f x powi n) has_laurent_expansion (F powi n)" + by (auto simp: power_int_def intro!: laurent_expansion_intros) + + +lemma has_fps_expansion_0_analytic_continuation: + assumes "f has_fps_expansion 0" "f holomorphic_on A" + assumes "open A" "connected A" "0 \ A" "x \ A" + shows "f x = 0" +proof - + have "eventually (\z. z \ A \ f z = 0) (nhds 0)" using assms + by (intro eventually_conj eventually_nhds_in_open) (auto simp: has_fps_expansion_def) + then obtain B where B: "open B" "0 \ B" "\z\B. z \ A \ f z = 0" + unfolding eventually_nhds by blast + show ?thesis + proof (rule analytic_continuation_open[where f = f and g = "\_. 0"]) + show "B \ {}" + using \open B\ B by auto + show "connected A" + using assms by auto + qed (use assms B in auto) +qed + +lemma has_laurent_expansion_0_analytic_continuation: + assumes "f has_laurent_expansion 0" "f holomorphic_on A - {0}" + assumes "open A" "connected A" "0 \ A" "x \ A - {0}" + shows "f x = 0" +proof - + have "eventually (\z. z \ A - {0} \ f z = 0) (at 0)" using assms + by (intro eventually_conj eventually_at_in_open) (auto simp: has_laurent_expansion_def) + then obtain B where B: "open B" "0 \ B" "\z\B - {0}. z \ A - {0} \ f z = 0" + unfolding eventually_at_filter eventually_nhds by blast + show ?thesis + proof (rule analytic_continuation_open[where f = f and g = "\_. 0"]) + show "B - {0} \ {}" + using \open B\ \0 \ B\ by (metis insert_Diff not_open_singleton) + show "connected (A - {0})" + using assms by (intro connected_open_delete) auto + qed (use assms B in auto) +qed + +lemma has_fps_expansion_cong: + assumes "eventually (\x. f x = g x) (nhds 0)" "F = G" + shows "f has_fps_expansion F \ g has_fps_expansion G" + using assms(2) by (auto simp: has_fps_expansion_def elim!: eventually_elim2[OF assms(1)]) + +lemma zor_poly_has_fps_expansion: + assumes "f has_laurent_expansion F" "F \ 0" + shows "zor_poly f 0 has_fps_expansion fls_base_factor_to_fps F" +proof - + note [simp] = \F \ 0\ + have "eventually (\z. f z \ 0) (at 0)" + by (rule has_laurent_expansion_nonzero_imp_eventually_nonzero[OF assms]) + hence freq: "frequently (\z. f z \ 0) (at 0)" + by (rule eventually_frequently[rotated]) auto + + have *: "isolated_singularity_at f 0" "not_essential f 0" + using has_laurent_expansion_isolated_0[OF assms(1)] has_laurent_expansion_not_essential_0[OF assms(1)] + by auto + + define G where "G = fls_base_factor_to_fps F" + define n where "n = zorder f 0" + have n_altdef: "n = fls_subdegree F" + using has_laurent_expansion_zorder_0 [OF assms(1)] by (simp add: n_def) + obtain r where r: "zor_poly f 0 0 \ 0" "zor_poly f 0 holomorphic_on cball 0 r" "r > 0" + "\w\cball 0 r - {0}. f w = zor_poly f 0 w * w powr of_int n \ + zor_poly f 0 w \ 0" + using zorder_exist[OF * freq] unfolding n_def by auto + obtain r' where r': "r' > 0" "\x\ball 0 r'-{0}. eval_fls F x = f x" + using assms(1) unfolding has_laurent_expansion_def eventually_at_filter eventually_nhds_metric ball_def + by (auto simp: dist_commute) + have holo: "zor_poly f 0 holomorphic_on ball 0 r" + by (rule holomorphic_on_subset[OF r(2)]) auto + + have "(\z. if z = 0 then fps_nth G 0 else f z * z powi -n) has_fps_expansion G" + unfolding G_def n_altdef by (intro has_fps_expansion_fls_base_factor_to_fps assms) + also have "?this \ zor_poly f 0 has_fps_expansion G" + proof (intro has_fps_expansion_cong) + have "eventually (\z. z \ ball 0 (min r r')) (nhds 0)" + using \r > 0\ \r' > 0\ by (intro eventually_nhds_in_open) auto + thus "\\<^sub>F x in nhds 0. (if x = 0 then G $ 0 else f x * x powi - n) = zor_poly f 0 x" + proof eventually_elim + case (elim w) + have w: "w \ ball 0 r" "w \ ball 0 r'" + using elim by auto + show ?case + proof (cases "w = 0") + case False + hence "f w = zor_poly f 0 w * w powr of_int n" + using r w by auto + thus ?thesis using False + by (simp add: powr_minus complex_powr_of_int power_int_minus) + next + case [simp]: True + obtain R where R: "R > 0" "R \ r" "R \ r'" "R \ fls_conv_radius F" + using \r > 0\ \r' > 0\ assms(1) unfolding has_laurent_expansion_def + by (smt (verit, ccfv_SIG) ereal_dense2 ereal_less(2) less_ereal.simps(1) order.strict_implies_order order_trans) + have "eval_fps G 0 = zor_poly f 0 0" + proof (rule analytic_continuation_open[where f = "eval_fps G" and g = "zor_poly f 0"]) + show "connected (ball 0 R :: complex set)" + by auto + have "of_real R / 2 \ ball 0 R - {0 :: complex}" + using R by auto + thus "ball 0 R - {0 :: complex} \ {}" + by blast + show "eval_fps G holomorphic_on ball 0 R" + using R less_le_trans[OF _ R(4)] unfolding G_def + by (intro holomorphic_intros) (auto simp: fls_conv_radius_altdef) + show "zor_poly f 0 holomorphic_on ball 0 R" + by (rule holomorphic_on_subset[OF holo]) (use R in auto) + show "eval_fps G z = zor_poly f 0 z" if "z \ ball 0 R - {0}" for z + using that r r' R n_altdef unfolding G_def + by (subst eval_fps_fls_base_factor) + (auto simp: complex_powr_of_int field_simps power_int_minus n_def) + qed (use R in auto) + hence "zor_poly f 0 0 = fps_nth G 0" + by (simp add: eval_fps_at_0) + thus ?thesis by simp + qed + qed + qed (use r' in auto) + finally show ?thesis + by (simp add: G_def) +qed + +lemma zorder_geI_0: + assumes "f analytic_on {0}" "f holomorphic_on A" "open A" "connected A" "0 \ A" "z \ A" "f z \ 0" + assumes "\k. k < n \ (deriv ^^ k) f 0 = 0" + shows "zorder f 0 \ n" +proof - + define F where "F = fps_expansion f 0" + from assms have "f has_fps_expansion F" + unfolding F_def using analytic_at_imp_has_fps_expansion_0 by blast + hence laurent: "f has_laurent_expansion fps_to_fls F" and [simp]: "f 0 = fps_nth F 0" + by (simp_all add: has_fps_expansion_to_laurent) + + have [simp]: "F \ 0" + proof + assume [simp]: "F = 0" + hence "f z = 0" + proof (cases "z = 0") + case False + have "f has_laurent_expansion 0" + using laurent by simp + thus ?thesis + proof (rule has_laurent_expansion_0_analytic_continuation) + show "f holomorphic_on A - {0}" + using assms(2) by (rule holomorphic_on_subset) auto + qed (use assms False in auto) + qed auto + with \f z \ 0\ show False by contradiction + qed + + have "zorder f 0 = int (subdegree F)" + using has_laurent_expansion_zorder_0[OF laurent] by (simp add: fls_subdegree_fls_to_fps) + also have "subdegree F \ n" + using assms by (intro subdegree_geI \F \ 0\) (auto simp: F_def fps_expansion_def) + hence "int (subdegree F) \ int n" + by simp + finally show ?thesis . +qed + +lemma zorder_geI: + assumes "f analytic_on {x}" "f holomorphic_on A" "open A" "connected A" "x \ A" "z \ A" "f z \ 0" + assumes "\k. k < n \ (deriv ^^ k) f x = 0" + shows "zorder f x \ n" +proof - + have "zorder f x = zorder (f \ (\u. u + x)) 0" + by (subst zorder_shift) (auto simp: o_def) + also have "\ \ n" + proof (rule zorder_geI_0) + show "(f \ (\u. u + x)) analytic_on {0}" + by (intro analytic_on_compose_gen[OF _ assms(1)] analytic_intros) auto + show "f \ (\u. u + x) holomorphic_on ((+) (-x)) ` A" + by (intro holomorphic_on_compose_gen[OF _ assms(2)] holomorphic_intros) auto + show "connected ((+) (- x) ` A)" + by (intro connected_continuous_image continuous_intros assms) + show "open ((+) (- x) ` A)" + by (intro open_translation assms) + show "z - x \ (+) (- x) ` A" + using \z \ A\ by auto + show "0 \ (+) (- x) ` A" + using \x \ A\ by auto + show "(f \ (\u. u + x)) (z - x) \ 0" + using \f z \ 0\ by auto + next + fix k :: nat assume "k < n" + hence "(deriv ^^ k) f x = 0" + using assms by simp + also have "(deriv ^^ k) f x = (deriv ^^ k) (f \ (+) x) 0" + by (subst higher_deriv_shift_0) auto + finally show "(deriv ^^ k) (f \ (\u. u + x)) 0 = 0" + by (subst add.commute) auto + qed + finally show ?thesis . +qed + +lemma has_laurent_expansion_divide [laurent_expansion_intros]: + assumes "f has_laurent_expansion F" and "g has_laurent_expansion G" + shows "(\x. f x / g x) has_laurent_expansion (F / G)" +proof - + have "(\x. f x * inverse (g x)) has_laurent_expansion (F * inverse G)" + by (intro laurent_expansion_intros assms) + thus ?thesis + by (simp add: field_simps) +qed + +lemma vector_derivative_translate [simp]: + "vector_derivative ((+) z \ g) (at x within A) = vector_derivative g (at x within A)" +proof - + have "(((+) z \ g) has_vector_derivative g') (at x within A)" + if "(g has_vector_derivative g') (at x within A)" for g :: "real \ 'a" and z g' + unfolding o_def using that by (auto intro!: derivative_eq_intros) + from this[of g _ z] this[of "\x. z + g x" _ "-z"] show ?thesis + unfolding vector_derivative_def + by (intro arg_cong[where f = Eps] ext) (auto simp: o_def algebra_simps) +qed + +lemma has_contour_integral_translate: + "(f has_contour_integral I) ((+) z \ g) \ ((\x. f (x + z)) has_contour_integral I) g" + by (simp add: has_contour_integral_def add_ac) + +lemma contour_integrable_translate: + "f contour_integrable_on ((+) z \ g) \ (\x. f (x + z)) contour_integrable_on g" + by (simp add: contour_integrable_on_def has_contour_integral_translate) + +lemma contour_integral_translate: + "contour_integral ((+) z \ g) f = contour_integral g (\x. f (x + z))" + by (simp add: contour_integral_def contour_integrable_translate has_contour_integral_translate) + +lemma residue_shift_0: "residue f z = residue (\x. f (z + x)) 0" +proof - + define Q where + "Q = (\r f z \. (f has_contour_integral complex_of_real (2 * pi) * \ * r) (circlepath z \))" + define P where + "P = (\r f z. \e>0. \\>0. \ < e \ Q r f z \)" + have path_eq: "circlepath (z - w) \ = (+) (-w) \ circlepath z \" for z w \ + by (simp add: circlepath_def o_def part_circlepath_def algebra_simps) + have *: "P r f z" if "P r (\x. f (x + w)) (z - w)" for r w f z + using that by (auto simp: P_def Q_def path_eq has_contour_integral_translate) + have "(SOME r. P r f z) = (SOME r. P r (\x. f (z + x)) 0)" + using *[of _ f z z] *[of _ "\x. f (z + x)" "-z"] + by (intro arg_cong[where f = Eps] ext iffI) (simp_all add: add_ac) + thus ?thesis + by (simp add: residue_def P_def Q_def) +qed + +lemma residue_shift_0': "NO_MATCH 0 z \ residue f z = residue (\x. f (z + x)) 0" + by (rule residue_shift_0) + +lemma has_laurent_expansion_residue_0: + assumes "f has_laurent_expansion F" + shows "residue f 0 = fls_residue F" +proof (cases "fls_subdegree F \ 0") + case True + have "residue f 0 = residue (eval_fls F) 0" + using assms by (intro residue_cong) (auto simp: has_laurent_expansion_def eq_commute) + also have "\ = 0" + by (rule residue_holo[OF _ _ holomorphic_on_eval_fls[OF order.refl]]) + (use True assms in \auto simp: has_laurent_expansion_def zero_ereal_def\) + also have "\ = fls_residue F" + using True by simp + finally show ?thesis . +next + case False + hence "F \ 0" + by auto + have *: "zor_poly f 0 has_fps_expansion fls_base_factor_to_fps F" + by (intro zor_poly_has_fps_expansion False assms \F \ 0\) + + have "residue f 0 = (deriv ^^ (nat (-zorder f 0) - 1)) (zor_poly f 0) 0 / fact (nat (- zorder f 0) - 1)" + by (intro residue_pole_order has_laurent_expansion_isolated_0[OF assms] + has_laurent_expansion_imp_is_pole_0[OF assms]) (use False in auto) + also have "\ = fls_residue F" + using has_laurent_expansion_zorder_0[OF assms \F \ 0\] False + by (subst fps_nth_fps_expansion [OF *, symmetric]) (auto simp: of_nat_diff) + finally show ?thesis . +qed + +lemma has_laurent_expansion_residue: + assumes "(\x. f (z + x)) has_laurent_expansion F" + shows "residue f z = fls_residue F" + using has_laurent_expansion_residue_0[OF assms] by (simp add: residue_shift_0') + +lemma eval_fls_has_laurent_expansion [laurent_expansion_intros]: + assumes "fls_conv_radius F > 0" + shows "eval_fls F has_laurent_expansion F" + using assms by (auto simp: has_laurent_expansion_def) + +lemma fps_expansion_unique_complex: + fixes F G :: "complex fps" + assumes "f has_fps_expansion F" "f has_fps_expansion G" + shows "F = G" + using assms unfolding fps_eq_iff by (auto simp: fps_eq_iff fps_nth_fps_expansion) + +lemma fps_expansion_eqI: + assumes "f has_fps_expansion F" + shows "fps_expansion f 0 = F" + using assms unfolding fps_eq_iff + by (auto simp: fps_eq_iff fps_nth_fps_expansion fps_expansion_def) + +lemma has_fps_expansion_imp_eval_fps_eq: + assumes "f has_fps_expansion F" "norm z < r" + assumes "f holomorphic_on ball 0 r" + shows "eval_fps F z = f z" +proof - + have [simp]: "fps_expansion f 0 = F" + by (rule fps_expansion_eqI) fact + have *: "f holomorphic_on eball 0 (ereal r)" + using assms by simp + from conv_radius_fps_expansion[OF *] have "fps_conv_radius F \ ereal r" + by simp + have "eval_fps (fps_expansion f 0) z = f (0 + z)" + by (rule eval_fps_expansion'[OF *]) (use assms in auto) + thus ?thesis + by simp +qed + +lemma fls_conv_radius_ge: + assumes "f has_laurent_expansion F" + assumes "f holomorphic_on eball 0 r - {0}" + shows "fls_conv_radius F \ r" +proof - + define n where "n = fls_subdegree F" + define G where "G = fls_base_factor_to_fps F" + define g where "g = (\z. if z = 0 then fps_nth G 0 else f z * z powi -n)" + have G: "g has_fps_expansion G" + unfolding G_def g_def n_def + by (intro has_fps_expansion_fls_base_factor_to_fps assms) + have "(\z. f z * z powi -n) holomorphic_on eball 0 r - {0}" + by (intro holomorphic_intros assms) auto + also have "?this \ g holomorphic_on eball 0 r - {0}" + by (intro holomorphic_cong) (auto simp: g_def) + finally have "g analytic_on eball 0 r - {0}" + by (subst analytic_on_open) auto + moreover have "g analytic_on {0}" + using G has_fps_expansion_imp_analytic_0 by auto + ultimately have "g analytic_on (eball 0 r - {0} \ {0})" + by (subst analytic_on_Un) auto + hence "g analytic_on eball 0 r" + by (rule analytic_on_subset) auto + hence "g holomorphic_on eball 0 r" + by (subst (asm) analytic_on_open) auto + hence "fps_conv_radius (fps_expansion g 0) \ r" + by (intro conv_radius_fps_expansion) + also have "fps_expansion g 0 = G" + using G by (intro fps_expansion_eqI) + finally show ?thesis + by (simp add: fls_conv_radius_altdef G_def) +qed + +lemma connected_eball [intro]: "connected (eball (z :: 'a :: real_normed_vector) r)" + by (cases r) auto + +lemma eval_fls_eqI: + assumes "f has_laurent_expansion F" "f holomorphic_on eball 0 r - {0}" + assumes "z \ eball 0 r - {0}" + shows "eval_fls F z = f z" +proof - + have conv: "fls_conv_radius F \ r" + by (intro fls_conv_radius_ge[OF assms(1,2)]) + have "(\z. eval_fls F z - f z) has_laurent_expansion F - F" + using assms by (intro laurent_expansion_intros assms) (auto simp: has_laurent_expansion_def) + hence "(\z. eval_fls F z - f z) has_laurent_expansion 0" + by simp + hence "eval_fls F z - f z = 0" + proof (rule has_laurent_expansion_0_analytic_continuation) + have "ereal 0 \ ereal (norm z)" + by simp + also have "norm z < r" + using assms by auto + finally have "r > 0" + by (simp add: zero_ereal_def) + thus "open (eball 0 r :: complex set)" "connected (eball 0 r :: complex set)" + "0 \ eball 0 r" "z \ eball 0 r - {0}" + using assms by (auto simp: zero_ereal_def) + qed (auto intro!: holomorphic_intros assms less_le_trans[OF _ conv] split: if_splits) + thus ?thesis by simp +qed + +lemma fls_nth_as_contour_integral: + assumes F: "f has_laurent_expansion F" + assumes holo: "f holomorphic_on ball 0 r - {0}" + assumes R: "0 < R" "R < r" + shows "((\z. f z * z powi (-(n+1))) has_contour_integral + complex_of_real (2 * pi) * \ * fls_nth F n) (circlepath 0 R)" +proof - + define I where "I = (\z. f z * z powi (-(n+1)))" + have "(I has_contour_integral complex_of_real (2 * pi) * \ * residue I 0) (circlepath 0 R)" + proof (rule base_residue) + show "open (ball (0::complex) r)" "0 \ ball (0::complex) r" + using R F by (auto simp: has_laurent_expansion_def zero_ereal_def) + qed (use R in \auto intro!: holomorphic_intros holomorphic_on_subset[OF holo] + simp: I_def split: if_splits\) + also have "residue I 0 = fls_residue (fls_shift (n + 1) F)" + unfolding I_def by (intro has_laurent_expansion_residue_0 laurent_expansion_intros F) + also have "\ = fls_nth F n" + by simp + finally show ?thesis + by (simp add: I_def) +qed + +lemma tendsto_0_subdegree_iff_0: + assumes F:"f has_laurent_expansion F" and "F\0" + shows "(f \0\0) \ fls_subdegree F > 0" +proof - + have ?thesis if "is_pole f 0" + proof - + have "fls_subdegree F <0" + using is_pole_0_imp_neg_fls_subdegree[OF F that] . + moreover then have "\ f \0\0" + using \is_pole f 0\ F at_neq_bot + has_laurent_expansion_imp_filterlim_infinity_0 + not_tendsto_and_filterlim_at_infinity that + by blast + ultimately show ?thesis by auto + qed + moreover have ?thesis if "\is_pole f 0" "\x. f \0\x" + proof - + have "fls_subdegree F \0" + using has_laurent_expansion_imp_is_pole_0[OF F] that(1) + by linarith + have "f \0\0" if "fls_subdegree F > 0" + using fls_eq0_below_subdegree[OF that] + by (metis F \0 \ fls_subdegree F\ has_laurent_expansion_imp_tendsto_0) + moreover have "fls_subdegree F > 0" if "f \0\0" + proof - + have False if "fls_subdegree F = 0" + proof - + have "f \0\ fls_nth F 0" + using has_laurent_expansion_imp_tendsto_0 + [OF F \fls_subdegree F \0\] . + then have "fls_nth F 0 = 0" using \f \0\0\ + using LIM_unique by blast + then have "F = 0" + using nth_fls_subdegree_zero_iff \fls_subdegree F = 0\ + by metis + with \F\0\ show False by auto + qed + with \fls_subdegree F \0\ + show ?thesis by fastforce + qed + ultimately show ?thesis by auto + qed + moreover have "is_pole f 0 \ (\x. f \0\x)" + proof - + have "not_essential f 0" + using F has_laurent_expansion_not_essential_0 by auto + then show ?thesis unfolding not_essential_def + by auto + qed + ultimately show ?thesis by auto +qed + +lemma tendsto_0_subdegree_iff: + assumes F:"(\w. f (z+w)) has_laurent_expansion F" and "F\0" + shows "(f \z\0) \ fls_subdegree F > 0" + apply (subst Lim_at_zero) + apply (rule tendsto_0_subdegree_iff_0) + using assms by auto + +lemma is_pole_0_deriv_divide_iff: + assumes F:"f has_laurent_expansion F" and "F\0" + shows "is_pole (\x. deriv f x / f x) 0 \ is_pole f 0 \ (f \0\0)" +proof - + have "(\x. deriv f x / f x) has_laurent_expansion fls_deriv F / F" + using F by (auto intro:laurent_expansion_intros) + + have "is_pole (\x. deriv f x / f x) 0 \ + fls_subdegree (fls_deriv F / F) < 0" + apply (rule is_pole_fls_subdegree_iff) + using F by (auto intro:laurent_expansion_intros) + also have "... \ is_pole f 0 \ (f \0\0)" + proof (cases "fls_subdegree F = 0") + case True + then have "fls_subdegree (fls_deriv F / F) \ 0" + by (metis diff_zero div_0 \F\0\ fls_deriv_subdegree0 + fls_divide_subdegree) + moreover then have "\ is_pole f 0" + by (metis F True is_pole_0_imp_neg_fls_subdegree less_le) + moreover have "\ (f \0\0)" + using tendsto_0_subdegree_iff_0[OF F \F\0\] True by auto + ultimately show ?thesis by auto + next + case False + then have "fls_deriv F \ 0" + by (metis fls_const_subdegree fls_deriv_eq_0_iff) + then have "fls_subdegree (fls_deriv F / F) = + fls_subdegree (fls_deriv F) - fls_subdegree F" + by (rule fls_divide_subdegree[OF _ \F\0\]) + moreover have "fls_subdegree (fls_deriv F) = fls_subdegree F - 1" + using fls_subdegree_deriv[OF False] . + ultimately have "fls_subdegree (fls_deriv F / F) < 0" by auto + moreover have "f \0\ 0 = (0 < fls_subdegree F)" + using tendsto_0_subdegree_iff_0[OF F \F \ 0\] . + moreover have "is_pole f 0 = (fls_subdegree F < 0)" + using is_pole_fls_subdegree_iff F by auto + ultimately show ?thesis using False by auto + qed + finally show ?thesis . +qed + +lemma is_pole_deriv_divide_iff: + assumes F:"(\w. f (z+w)) has_laurent_expansion F" and "F\0" + shows "is_pole (\x. deriv f x / f x) z \ is_pole f z \ (f \z\0)" +proof - + define ff df where "ff=(\w. f (z+w))" and "df=(\w. deriv f (z + w))" + have "is_pole (\x. deriv f x / f x) z + \ is_pole (\x. deriv ff x / ff x) 0" + unfolding ff_def df_def + by (simp add:deriv_shift_0' is_pole_shift_0' comp_def algebra_simps) + moreover have "is_pole f z \ is_pole ff 0" + unfolding ff_def by (auto simp:is_pole_shift_0') + moreover have "(f \z\0) \ (ff \0\0)" + unfolding ff_def by (simp add: LIM_offset_zero_iff) + moreover have "is_pole (\x. deriv ff x / ff x) 0 = (is_pole ff 0 \ ff \0\ 0)" + apply (rule is_pole_0_deriv_divide_iff) + using F ff_def \F\0\ by blast+ + ultimately show ?thesis by auto +qed + +lemma subdegree_imp_eventually_deriv_nzero_0: + assumes F:"f has_laurent_expansion F" and "fls_subdegree F\0" + shows "eventually (\z. deriv f z \ 0) (at 0)" +proof - + have "deriv f has_laurent_expansion fls_deriv F" + using has_laurent_expansion_deriv[OF F] . + moreover have "fls_deriv F\0" + using \fls_subdegree F\0\ + by (metis fls_const_subdegree fls_deriv_eq_0_iff) + ultimately show ?thesis + using has_laurent_expansion_eventually_nonzero_iff' by blast +qed + +lemma subdegree_imp_eventually_deriv_nzero: + assumes F:"(\w. f (z+w)) has_laurent_expansion F" + and "fls_subdegree F\0" + shows "eventually (\w. deriv f w \ 0) (at z)" +proof - + have "\\<^sub>F x in at 0. deriv (\w. f (z + w)) x \ 0" + using subdegree_imp_eventually_deriv_nzero_0 assms by auto + then show ?thesis + apply (subst eventually_at_to_0) + by (simp add:deriv_shift_0' comp_def algebra_simps) +qed + +lemma has_fps_expansion_imp_asymp_equiv_0: + fixes f :: "complex \ complex" + assumes F: "f has_fps_expansion F" + defines "n \ subdegree F" + shows "f \[nhds 0] (\z. fps_nth F n * z ^ n)" +proof - + have F': "f has_laurent_expansion fps_to_fls F" + using F has_laurent_expansion_fps by blast + + have "f \[at 0] (\z. fps_nth F n * z ^ n)" + using has_laurent_expansion_imp_asymp_equiv_0[OF F'] + by (simp add: fls_subdegree_fls_to_fps n_def) + moreover have "f 0 = fps_nth F n * 0 ^ n" + using F by (auto simp: n_def has_fps_expansion_to_laurent power_0_left) + ultimately show ?thesis + by (auto simp: asymp_equiv_nhds_iff) +qed + +lemma has_fps_expansion_imp_tendsto_0: + fixes f :: "complex \ complex" + assumes "f has_fps_expansion F" + shows "(f \ fps_nth F 0) (nhds 0)" +proof (rule asymp_equiv_tendsto_transfer) + show "(\z. fps_nth F (subdegree F) * z ^ subdegree F) \[nhds 0] f" + by (rule asymp_equiv_symI, rule has_fps_expansion_imp_asymp_equiv_0) fact + have "((\z. F $ subdegree F * z ^ subdegree F) \ F $ 0) (at 0)" + by (rule tendsto_eq_intros refl | simp)+ (auto simp: power_0_left) + thus "((\z. F $ subdegree F * z ^ subdegree F) \ F $ 0) (nhds 0)" + by (auto simp: tendsto_nhds_iff power_0_left) +qed + +lemma has_fps_expansion_imp_0_eq_fps_nth_0: + assumes "f has_fps_expansion F" + shows "f 0 = fps_nth F 0" +proof - + have "eventually (\x. f x = eval_fps F x) (nhds 0)" + using assms by (auto simp: has_fps_expansion_def eq_commute) + then obtain A where "open A" "0 \ A" "\x\A. f x = eval_fps F x" + unfolding eventually_nhds by blast + hence "f 0 = eval_fps F 0" + by blast + thus ?thesis + by (simp add: eval_fps_at_0) +qed + +lemma fls_nth_compose_aux: + assumes "f has_fps_expansion F" + assumes G: "g has_fps_expansion G" "fps_nth G 0 = 0" "fps_deriv G \ 0" + assumes "(f \ g) has_laurent_expansion H" + shows "fls_nth H (int n) = fps_nth (fps_compose F G) n" + using assms(1,5) +proof (induction n arbitrary: f F H rule: less_induct) + case (less n f F H) + have [simp]: "g 0 = 0" + using has_fps_expansion_imp_0_eq_fps_nth_0[OF G(1)] G(2) by simp + have ana_f: "f analytic_on {0}" + using less.prems by (meson has_fps_expansion_imp_analytic_0) + have ana_g: "g analytic_on {0}" + using G by (meson has_fps_expansion_imp_analytic_0) + have "(f \ g) has_laurent_expansion fps_to_fls (fps_expansion (f \ g) 0)" + by (rule analytic_at_imp_has_fps_expansion_0 analytic_intros has_laurent_expansion_fps + analytic_on_compose_gen ana_f ana_g)+ auto + with less.prems have "H = fps_to_fls (fps_expansion (f \ g) 0)" + using has_laurent_expansion_unique by blast + also have "fls_subdegree \ \ 0" + by (simp add: fls_subdegree_fls_to_fps) + finally have subdeg: "fls_subdegree H \ 0" . + + show ?case + proof (cases "n = 0") + case [simp]: True + have lim_g: "g \0\ 0" + using has_laurent_expansion_imp_tendsto_0[of g "fps_to_fls G"] G + by (auto simp: fls_subdegree_fls_to_fps_gt0 has_fps_expansion_to_laurent) + have lim_f: "(f \ fps_nth F 0) (nhds 0)" + by (intro has_fps_expansion_imp_tendsto_0 less.prems) + have "(\x. f (g x)) \0\ fps_nth F 0" + by (rule filterlim_compose[OF lim_f lim_g]) + moreover have "(f \ g) \0\ fls_nth H 0" + by (intro has_laurent_expansion_imp_tendsto_0 less.prems subdeg) + ultimately have "fps_nth F 0 = fls_nth H 0" + using tendsto_unique by (force simp: o_def) + thus ?thesis + by simp + next + case n: False + define GH where "GH = (fls_deriv H / fls_deriv (fps_to_fls G))" + define GH' where "GH' = fls_regpart GH" + + have "(\x. deriv (f \ g) x / deriv g x) has_laurent_expansion + fls_deriv H / fls_deriv (fps_to_fls G)" + by (intro laurent_expansion_intros less.prems has_laurent_expansion_fps[of _ G] G) + also have "?this \ (deriv f \ g) has_laurent_expansion fls_deriv H / fls_deriv (fps_to_fls G)" + proof (rule has_laurent_expansion_cong) + from ana_f obtain r1 where r1: "r1 > 0" "f holomorphic_on ball 0 r1" + unfolding analytic_on_def by blast + from ana_g obtain r2 where r2: "r2 > 0" "g holomorphic_on ball 0 r2" + unfolding analytic_on_def by blast + have lim_g: "g \0\ 0" + using has_laurent_expansion_imp_tendsto_0[of g "fps_to_fls G"] G + by (auto simp: fls_subdegree_fls_to_fps_gt0 has_fps_expansion_to_laurent) + moreover have "open (ball 0 r1)" "0 \ ball 0 r1" + using r1 by auto + ultimately have "eventually (\x. g x \ ball 0 r1) (at 0)" + unfolding tendsto_def by blast + moreover have "eventually (\x. deriv g x \ 0) (at 0)" + using G fps_to_fls_eq_0_iff has_fps_expansion_deriv has_fps_expansion_to_laurent + has_laurent_expansion_nonzero_imp_eventually_nonzero by blast + moreover have "eventually (\x. x \ ball 0 (min r1 r2) - {0}) (at 0)" + by (intro eventually_at_in_open) (use r1 r2 in auto) + ultimately show "eventually (\x. deriv (f \ g) x / deriv g x = (deriv f \ g) x) (at 0)" + proof eventually_elim + case (elim x) + thus ?case using r1 r2 + by (subst deriv_chain) + (auto simp: field_simps holomorphic_on_def at_within_open[of _ "ball _ _"]) + qed + qed auto + finally have GH: "(deriv f \ g) has_laurent_expansion GH" + unfolding GH_def . + + have "(deriv f \ g) has_laurent_expansion fps_to_fls (fps_expansion (deriv f \ g) 0)" + by (rule analytic_at_imp_has_fps_expansion_0 analytic_intros has_laurent_expansion_fps + analytic_on_compose_gen ana_f ana_g)+ auto + with GH have "GH = fps_to_fls (fps_expansion (deriv f \ g) 0)" + using has_laurent_expansion_unique by blast + also have "fls_subdegree \ \ 0" + by (simp add: fls_subdegree_fls_to_fps) + finally have subdeg': "fls_subdegree GH \ 0" . + + have "deriv f has_fps_expansion fps_deriv F" + by (intro fps_expansion_intros less.prems) + from this and GH have IH: "fls_nth GH (int k) = fps_nth (fps_compose (fps_deriv F) G) k" + if "k < n" for k + by (intro less.IH that) + + have "fps_nth (fps_compose (fps_deriv F) G) n = (\i=0..n. of_nat (Suc i) * F $ Suc i * G ^ i $ n)" + by (simp add: fps_compose_nth) + + have "fps_nth (fps_compose F G) n = + fps_nth (fps_deriv (fps_compose F G)) (n - 1) / of_nat n" + using n by (cases n) (auto simp del: of_nat_Suc) + also have "fps_deriv (fps_compose F G) = fps_compose (fps_deriv F) G * fps_deriv G " + using G by (subst fps_compose_deriv) auto + also have "fps_nth \ (n - 1) = (\i=0..n-1. (fps_deriv F oo G) $ i * fps_deriv G $ (n - 1 - i))" + unfolding fps_mult_nth .. + also have "\ = (\i=0..n-1. fps_nth GH' i * of_nat (n - i) * G $ (n - i))" + using n by (intro sum.cong) (auto simp: IH Suc_diff_Suc GH'_def) + also have "\ = (\i=0..n. fps_nth GH' i * of_nat (n - i) * G $ (n - i))" + by (intro sum.mono_neutral_left) auto + also have "\ = fps_nth (GH' * Abs_fps (\i. of_nat i * fps_nth G i)) n" + by (simp add: fps_mult_nth mult_ac) + also have "Abs_fps (\i. of_nat i * fps_nth G i) = fps_X * fps_deriv G" + by (simp add: fps_mult_fps_X_deriv_shift) + also have "fps_nth (GH' * (fps_X * fps_deriv G)) n = + fls_nth (fps_to_fls (GH' * (fps_X * fps_deriv G))) (int n)" + by simp + also have "fps_to_fls (GH' * (fps_X * fps_deriv G)) = + GH * fps_to_fls (fps_deriv G) * fls_X" + using subdeg' by (simp add: mult_ac fls_times_fps_to_fls GH'_def) + also have "GH * fps_to_fls (fps_deriv G) = fls_deriv H" + unfolding GH_def using G by (simp add: fls_deriv_fps_to_fls) + also have "fls_deriv H * fls_X = fls_shift (-1) (fls_deriv H)" + using fls_X_times_conv_shift(2) by blast + finally show ?thesis + using n by simp + qed +qed + +lemma has_fps_expansion_compose [fps_expansion_intros]: + fixes f g :: "complex \ complex" + assumes F: "f has_fps_expansion F" + assumes G: "g has_fps_expansion G" "fps_nth G 0 = 0" + shows "(f \ g) has_fps_expansion fps_compose F G" +proof (cases "fps_deriv G = 0") + case False + have [simp]: "g 0 = 0" + using has_fps_expansion_imp_0_eq_fps_nth_0[OF G(1)] G(2) False by simp + have ana_f: "f analytic_on {0}" + using F by (meson has_fps_expansion_imp_analytic_0) + have ana_g: "g analytic_on {0}" + using G by (meson has_fps_expansion_imp_analytic_0) + have fg: "(f \ g) has_fps_expansion fps_expansion (f \ g) 0" + by (rule analytic_at_imp_has_fps_expansion_0 analytic_intros + analytic_on_compose_gen ana_f ana_g)+ auto + + have "fls_nth (fps_to_fls (fps_expansion (f \ g) 0)) (int n) = fps_nth (fps_compose F G) n" for n + by (rule fls_nth_compose_aux has_laurent_expansion_fps F G False fg)+ + hence "fps_expansion (f \ g) 0 = fps_compose F G" + by (simp add: fps_eq_iff) + thus ?thesis using fg + by simp +next + case True + have [simp]: "f 0 = fps_nth F 0" + using F by (auto dest: has_fps_expansion_imp_0_eq_fps_nth_0) + from True have "fps_nth G n = 0" for n + using G(2) by (cases n) (auto simp del: of_nat_Suc) + hence [simp]: "G = 0" + by (auto simp: fps_eq_iff) + have "(\_. f 0) has_fps_expansion fps_const (f 0)" + by (intro fps_expansion_intros) + also have "eventually (\x. g x = 0) (nhds 0)" + using G by (auto simp: has_fps_expansion_def) + hence "(\_. f 0) has_fps_expansion fps_const (f 0) \ (f \ g) has_fps_expansion fps_const (f 0)" + by (intro has_fps_expansion_cong) (auto elim!: eventually_mono) + thus ?thesis + by simp +qed + +hide_const (open) fls_compose_fps + +definition fls_compose_fps :: "'a :: field fls \ 'a fps \ 'a fls" where + "fls_compose_fps F G = + fps_to_fls (fps_compose (fls_base_factor_to_fps F) G) * fps_to_fls G powi fls_subdegree F" + +lemma fps_compose_of_nat [simp]: "fps_compose (of_nat n :: 'a :: comm_ring_1 fps) H = of_nat n" + and fps_compose_of_int [simp]: "fps_compose (of_int i) H = of_int i" + unfolding fps_of_nat [symmetric] fps_of_int [symmetric] numeral_fps_const + by (rule fps_const_compose)+ + +lemmas [simp] = fps_to_fls_of_nat fps_to_fls_of_int + +lemma fls_compose_fps_0 [simp]: "fls_compose_fps 0 H = 0" + and fls_compose_fps_1 [simp]: "fls_compose_fps 1 H = 1" + and fls_compose_fps_const [simp]: "fls_compose_fps (fls_const c) H = fls_const c" + and fls_compose_fps_of_nat [simp]: "fls_compose_fps (of_nat n) H = of_nat n" + and fls_compose_fps_of_int [simp]: "fls_compose_fps (of_int i) H = of_int i" + and fls_compose_fps_X [simp]: "fls_compose_fps fls_X F = fps_to_fls F" + by (simp_all add: fls_compose_fps_def) + +lemma fls_compose_fps_0_right: + "fls_compose_fps F 0 = (if fls_subdegree F \ 0 then fls_const (fls_nth F 0) else 0)" + by (cases "fls_subdegree F = 0") (simp_all add: fls_compose_fps_def) + +lemma fls_compose_fps_shift: + assumes "H \ 0" + shows "fls_compose_fps (fls_shift n F) H = fls_compose_fps F H * fps_to_fls H powi (-n)" +proof (cases "F = 0") + case False + thus ?thesis + using assms by (simp add: fls_compose_fps_def power_int_diff power_int_minus field_simps) +qed auto + +lemma fls_compose_fps_to_fls [simp]: + assumes [simp]: "G \ 0" "fps_nth G 0 = 0" + shows "fls_compose_fps (fps_to_fls F) G = fps_to_fls (fps_compose F G)" +proof (cases "F = 0") + case False + define n where "n = subdegree F" + define F' where "F' = fps_shift n F" + have [simp]: "F' \ 0" "subdegree F' = 0" + using False by (auto simp: F'_def n_def) + have F_eq: "F = F' * fps_X ^ n" + unfolding F'_def n_def using subdegree_decompose by blast + have "fls_compose_fps (fps_to_fls F) G = + fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F' * fls_X_intpow (int n))) oo G) * fps_to_fls (G ^ n)" + unfolding F_eq fls_compose_fps_def + by (simp add: fls_times_fps_to_fls fls_X_power_conv_shift_1 power_int_add + fls_subdegree_fls_to_fps fps_to_fls_power fls_regpart_shift_conv_fps_shift + flip: fls_times_both_shifted_simp) + also have "fps_to_fls F' * fls_X_intpow (int n) = fps_to_fls F" + by (simp add: F_eq fls_times_fps_to_fls fps_to_fls_power fls_X_power_conv_shift_1) + also have "fps_to_fls (fps_shift n (fls_regpart (fps_to_fls F)) oo G) * fps_to_fls (G ^ n) = + fps_to_fls ((fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n) oo G)" + by (simp add: fls_times_fps_to_fls flip: fps_compose_power add: fps_compose_mult_distrib) + also have "fps_shift n (fls_regpart (fps_to_fls F)) * fps_X ^ n = F" + by (simp add: F_eq) + finally show ?thesis . +qed (auto simp: fls_compose_fps_def) + +lemma fls_compose_fps_mult: + assumes [simp]: "H \ 0" "fps_nth H 0 = 0" + shows "fls_compose_fps (F * G) H = fls_compose_fps F H * fls_compose_fps G H" + using assms +proof (cases "F * G = 0") + case False + hence [simp]: "F \ 0" "G \ 0" + by auto + define n m where "n = fls_subdegree F" "m = fls_subdegree G" + define F' where "F' = fls_regpart (fls_shift n F)" + define G' where "G' = fls_regpart (fls_shift m G)" + have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-m) (fps_to_fls G')" + by (simp_all add: F'_def G'_def n_m_def) + have "fls_compose_fps (F * G) H = fls_compose_fps (fls_shift (-(n + m)) (fps_to_fls (F' * G'))) H" + by (simp add: fls_times_fps_to_fls F_eq G_eq fls_shifted_times_simps) + also have "\ = fps_to_fls ((F' oo H) * (G' oo H)) * fps_to_fls H powi (m + n)" + by (simp add: fls_compose_fps_shift fps_compose_mult_distrib) + also have "\ = fls_compose_fps F H * fls_compose_fps G H" + by (simp add: F_eq G_eq fls_compose_fps_shift fls_times_fps_to_fls power_int_add) + finally show ?thesis . +qed auto + +lemma fls_compose_fps_power: + assumes [simp]: "G \ 0" "fps_nth G 0 = 0" + shows "fls_compose_fps (F ^ n) G = fls_compose_fps F G ^ n" + by (induction n) (auto simp: fls_compose_fps_mult) + +lemma fls_compose_fps_add: + assumes [simp]: "H \ 0" "fps_nth H 0 = 0" + shows "fls_compose_fps (F + G) H = fls_compose_fps F H + fls_compose_fps G H" +proof (cases "F = 0 \ G = 0") + case False + hence [simp]: "F \ 0" "G \ 0" + by auto + define n where "n = min (fls_subdegree F) (fls_subdegree G)" + define F' where "F' = fls_regpart (fls_shift n F)" + define G' where "G' = fls_regpart (fls_shift n G)" + have F_eq: "F = fls_shift (-n) (fps_to_fls F')" and G_eq: "G = fls_shift (-n) (fps_to_fls G')" + unfolding n_def by (simp_all add: F'_def G'_def n_def) + have "F + G = fls_shift (-n) (fps_to_fls (F' + G'))" + by (simp add: F_eq G_eq) + also have "fls_compose_fps \ H = fls_compose_fps (fps_to_fls (F' + G')) H * fps_to_fls H powi n" + by (subst fls_compose_fps_shift) auto + also have "\ = fps_to_fls (fps_compose (F' + G') H) * fps_to_fls H powi n" + by (subst fls_compose_fps_to_fls) auto + also have "\ = fls_compose_fps F H + fls_compose_fps G H" + by (simp add: F_eq G_eq fls_compose_fps_shift fps_compose_add_distrib algebra_simps) + finally show ?thesis . +qed auto + +lemma fls_compose_fps_uminus [simp]: "fls_compose_fps (-F) H = -fls_compose_fps F H" + by (simp add: fls_compose_fps_def fps_compose_uminus) + +lemma fls_compose_fps_diff: + assumes [simp]: "H \ 0" "fps_nth H 0 = 0" + shows "fls_compose_fps (F - G) H = fls_compose_fps F H - fls_compose_fps G H" + using fls_compose_fps_add[of H F "-G"] by simp + +lemma fps_compose_eq_0_iff: + fixes F G :: "'a :: idom fps" + assumes "fps_nth G 0 = 0" + shows "fps_compose F G = 0 \ F = 0 \ (G = 0 \ fps_nth F 0 = 0)" +proof safe + assume *: "fps_compose F G = 0" "F \ 0" + have "fps_nth (fps_compose F G) 0 = fps_nth F 0" + by simp + also have "fps_compose F G = 0" + by (simp add: *) + finally show "fps_nth F 0 = 0" + by simp + show "G = 0" + proof (rule ccontr) + assume "G \ 0" + hence "subdegree G > 0" using assms + using subdegree_eq_0_iff by blast + define N where "N = subdegree F * subdegree G" + have "fps_nth (fps_compose F G) N = (\i = 0..N. fps_nth F i * fps_nth (G ^ i) N)" + unfolding fps_compose_def by (simp add: N_def) + also have "\ = (\i\{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)" + proof (intro sum.mono_neutral_right ballI) + fix i assume i: "i \ {0..N} - {subdegree F}" + show "fps_nth F i * fps_nth (G ^ i) N = 0" + proof (cases i "subdegree F" rule: linorder_cases) + assume "i > subdegree F" + hence "fps_nth (G ^ i) N = 0" + using i \subdegree G > 0\ by (intro fps_pow_nth_below_subdegree) (auto simp: N_def) + thus ?thesis by simp + qed (use i in \auto simp: N_def\) + qed (use \subdegree G > 0\ in \auto simp: N_def\) + also have "\ = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N" + by simp + also have "\ \ 0" + using \G \ 0\ \F \ 0\ by (auto simp: N_def) + finally show False using * by auto + qed +qed auto + +lemma fls_compose_fps_eq_0_iff: + assumes "H \ 0" "fps_nth H 0 = 0" + shows "fls_compose_fps F H = 0 \ F = 0" + using assms fls_base_factor_to_fps_nonzero[of F] + by (cases "F = 0") (auto simp: fls_compose_fps_def fps_compose_eq_0_iff) + +lemma fls_compose_fps_inverse: + assumes [simp]: "H \ 0" "fps_nth H 0 = 0" + shows "fls_compose_fps (inverse F) H = inverse (fls_compose_fps F H)" +proof (cases "F = 0") + case False + have "fls_compose_fps (inverse F) H * fls_compose_fps F H = + fls_compose_fps (inverse F * F) H" + by (subst fls_compose_fps_mult) auto + also have "inverse F * F = 1" + using False by simp + finally show ?thesis + using False by (simp add: field_simps fls_compose_fps_eq_0_iff) +qed auto + +lemma fls_compose_fps_divide: + assumes [simp]: "H \ 0" "fps_nth H 0 = 0" + shows "fls_compose_fps (F / G) H = fls_compose_fps F H / fls_compose_fps G H" + using fls_compose_fps_mult[of H F "inverse G"] fls_compose_fps_inverse[of H G] + by (simp add: field_simps) + +lemma fls_compose_fps_powi: + assumes [simp]: "H \ 0" "fps_nth H 0 = 0" + shows "fls_compose_fps (F powi n) H = fls_compose_fps F H powi n" + by (simp add: power_int_def fls_compose_fps_power fls_compose_fps_inverse) + +lemma fls_compose_fps_assoc: + assumes [simp]: "G \ 0" "fps_nth G 0 = 0" "H \ 0" "fps_nth H 0 = 0" + shows "fls_compose_fps (fls_compose_fps F G) H = fls_compose_fps F (fps_compose G H)" +proof (cases "F = 0") + case [simp]: False + define n where "n = fls_subdegree F" + define F' where "F' = fls_regpart (fls_shift n F)" + have F_eq: "F = fls_shift (-n) (fps_to_fls F')" + by (simp add: F'_def n_def) + show ?thesis + by (simp add: F_eq fls_compose_fps_shift fls_compose_fps_mult fls_compose_fps_powi + fps_compose_eq_0_iff fps_compose_assoc) +qed auto + +lemma subdegree_pos_iff: "subdegree F > 0 \ F \ 0 \ fps_nth F 0 = 0" + using subdegree_eq_0_iff[of F] by auto + +lemma has_fps_expansion_fps_to_fls: + assumes "f has_laurent_expansion fps_to_fls F" + shows "(\z. if z = 0 then fps_nth F 0 else f z) has_fps_expansion F" + (is "?f' has_fps_expansion _") +proof - + have "f has_laurent_expansion fps_to_fls F \ ?f' has_laurent_expansion fps_to_fls F" + by (intro has_laurent_expansion_cong) (auto simp: eventually_at_filter) + with assms show ?thesis + by (auto simp: has_fps_expansion_to_laurent) +qed + + +lemma has_laurent_expansion_compose [laurent_expansion_intros]: + fixes f g :: "complex \ complex" + assumes F: "f has_laurent_expansion F" + assumes G: "g has_laurent_expansion fps_to_fls G" "fps_nth G 0 = 0" "G \ 0" + shows "(f \ g) has_laurent_expansion fls_compose_fps F G" +proof - + from assms have lim_g: "g \0\ 0" + by (subst tendsto_0_subdegree_iff_0[OF G(1)]) + (auto simp: fls_subdegree_fls_to_fps subdegree_pos_iff) + have ev1: "eventually (\z. g z \ 0) (at 0)" + using \G \ 0\ G(1) fps_to_fls_eq_0_iff has_laurent_expansion_fps + has_laurent_expansion_nonzero_imp_eventually_nonzero by blast + moreover have "eventually (\z. z \ 0) (at (0 :: complex))" + by (auto simp: eventually_at_filter) + ultimately have ev: "eventually (\z. z \ 0 \ g z \ 0) (at 0)" + by eventually_elim blast + from ev1 and lim_g have lim_g': "filterlim g (at 0) (at 0)" + by (auto simp: filterlim_at) + define g' where "g' = (\z. if z = 0 then fps_nth G 0 else g z)" + + show ?thesis + proof (cases "F = 0") + assume [simp]: "F = 0" + have "eventually (\z. f z = 0) (at 0)" + using F by (auto simp: has_laurent_expansion_def) + hence "eventually (\z. f (g z) = 0) (at 0)" + using lim_g' by (rule eventually_compose_filterlim) + thus ?thesis + by (auto simp: has_laurent_expansion_def) + next + assume [simp]: "F \ 0" + define n where "n = fls_subdegree F" + define f' where + "f' = (\z. if z = 0 then fps_nth (fls_base_factor_to_fps F) 0 else f z * z powi -n)" + have "((\z. (f' \ g') z * g z powi n)) has_laurent_expansion fls_compose_fps F G" + unfolding f'_def n_def fls_compose_fps_def g'_def + by (intro fps_expansion_intros laurent_expansion_intros has_fps_expansion_fps_to_fls + has_fps_expansion_fls_base_factor_to_fps assms has_laurent_expansion_fps) + also have "?this \ ?thesis" + by (intro has_laurent_expansion_cong eventually_mono[OF ev]) + (auto simp: f'_def power_int_minus g'_def) + finally show ?thesis . + qed +qed + +lemma has_laurent_expansion_fls_X_inv [laurent_expansion_intros]: + "inverse has_laurent_expansion fls_X_inv" + using has_laurent_expansion_inverse[OF has_laurent_expansion_fps_X] + by (simp add: fls_inverse_X) + +lemma fls_X_power_int [simp]: "fls_X powi n = (fls_X_intpow n :: 'a :: division_ring fls)" + by (auto simp: power_int_def fls_X_power_conv_shift_1 fls_inverse_X fls_inverse_shift + simp flip: fls_inverse_X_power) + +lemma fls_const_power_int: "fls_const (c powi n) = fls_const (c :: 'a :: division_ring) powi n" + by (auto simp: power_int_def fls_const_power fls_inverse_const) + +lemma fls_nth_fls_compose_fps_linear: + fixes c :: "'a :: field" + assumes [simp]: "c \ 0" + shows "fls_nth (fls_compose_fps F (fps_const c * fps_X)) n = fls_nth F n * c powi n" +proof - + { + assume *: "n \ fls_subdegree F" + hence "c ^ nat (n - fls_subdegree F) = c powi int (nat (n - fls_subdegree F))" + by (simp add: power_int_def) + also have "\ * c powi fls_subdegree F = c powi (int (nat (n - fls_subdegree F)) + fls_subdegree F)" + using * by (subst power_int_add) auto + also have "\ = c powi n" + using * by simp + finally have "c ^ nat (n - fls_subdegree F) * c powi fls_subdegree F = c powi n" . + } + thus ?thesis + by (simp add: fls_compose_fps_def fps_compose_linear fls_times_fps_to_fls power_int_mult_distrib + fls_shifted_times_simps + flip: fls_const_power_int) +qed + +lemma zorder_times_analytic: + assumes "f analytic_on {z}" "g analytic_on {z}" + assumes "eventually (\z. f z * g z \ 0) (at z)" + shows "zorder (\z. f z * g z) z = zorder f z + zorder g z" +proof - + have *: "(\w. f (z + w)) has_fps_expansion fps_expansion f z" + "(\w. g (z + w)) has_fps_expansion fps_expansion g z" + "(\w. f (z + w) * g (z + w)) has_fps_expansion fps_expansion f z * fps_expansion g z" + by (intro fps_expansion_intros analytic_at_imp_has_fps_expansion assms)+ + have [simp]: "fps_expansion f z \ 0" + proof + assume "fps_expansion f z = 0" + hence "eventually (\z. f z * g z = 0) (at z)" using *(1) + by (auto simp: has_fps_expansion_0_iff nhds_to_0' eventually_filtermap eventually_at_filter + elim: eventually_mono) + with assms(3) have "eventually (\z. False) (at z)" + by eventually_elim auto + thus False by simp + qed + have [simp]: "fps_expansion g z \ 0" + proof + assume "fps_expansion g z = 0" + hence "eventually (\z. f z * g z = 0) (at z)" using *(2) + by (auto simp: has_fps_expansion_0_iff nhds_to_0' eventually_filtermap eventually_at_filter + elim: eventually_mono) + with assms(3) have "eventually (\z. False) (at z)" + by eventually_elim auto + thus False by simp + qed + from *[THEN has_fps_expansion_zorder] show ?thesis + by auto +qed + +lemma analytic_on_prod [analytic_intros]: + assumes "\x. x \ A \ f x analytic_on B" + shows "(\z. \x\A. f x z) analytic_on B" + using assms by (induction A rule: infinite_finite_induct) (auto intro!: analytic_intros) + +lemma zorder_const [simp]: "c \ 0 \ zorder (\_. c) z = 0" + by (intro zorder_eqI[where s = UNIV]) auto + +lemma zorder_prod_analytic: + assumes "\x. x \ A \ f x analytic_on {z}" + assumes "eventually (\z. (\x\A. f x z) \ 0) (at z)" + shows "zorder (\z. \x\A. f x z) z = (\x\A. zorder (f x) z)" + using assms +proof (induction A rule: infinite_finite_induct) + case (insert x A) + have "zorder (\z. f x z * (\x\A. f x z)) z = zorder (f x) z + zorder (\z. \x\A. f x z) z" + using insert.prems insert.hyps by (intro zorder_times_analytic analytic_intros) auto + also have "zorder (\z. \x\A. f x z) z = (\x\A. zorder (f x) z)" + using insert.prems insert.hyps by (intro insert.IH) (auto elim!: eventually_mono) + finally show ?case using insert + by simp +qed auto + +lemma zorder_eq_0I: + assumes "g analytic_on {z}" "g z \ 0" + shows "zorder g z = 0" +proof - + from assms obtain r where r: "r > 0" "g holomorphic_on ball z r" + unfolding analytic_on_def by blast + thus ?thesis using assms + by (intro zorder_eqI[of "ball z r" _ g]) auto +qed + +lemma zorder_pos_iff: + assumes "f holomorphic_on A" "open A" "z \ A" "frequently (\z. f z \ 0) (at z)" + shows "zorder f z > 0 \ f z = 0" +proof - + have "f analytic_on {z}" + using assms analytic_at by blast + hence *: "(\w. f (z + w)) has_fps_expansion fps_expansion f z" + using analytic_at_imp_has_fps_expansion by blast + have nz: "fps_expansion f z \ 0" + proof + assume "fps_expansion f z = 0" + hence "eventually (\z. f z = 0) (nhds z)" + using * by (auto simp: has_fps_expansion_def nhds_to_0' eventually_filtermap add_ac) + hence "eventually (\z. f z = 0) (at z)" + by (auto simp: eventually_at_filter elim: eventually_mono) + with assms show False + by (auto simp: frequently_def) + qed + from has_fps_expansion_zorder[OF * this] have eq: "zorder f z = int (subdegree (fps_expansion f z))" + by auto + moreover have "subdegree (fps_expansion f z) = 0 \ fps_nth (fps_expansion f z) 0 \ 0" + using nz by (auto simp: subdegree_eq_0_iff) + moreover have "fps_nth (fps_expansion f z) 0 = f z" + by (auto simp: fps_expansion_def) + ultimately show ?thesis + by auto +qed + +lemma zorder_pos_iff': + assumes "f analytic_on {z}" "frequently (\z. f z \ 0) (at z)" + shows "zorder f z > 0 \ f z = 0" +proof - + from assms(1) obtain A where A: "open A" "{z} \ A" "f holomorphic_on A" + unfolding analytic_on_holomorphic by auto + with zorder_pos_iff [OF A(3,1), of z] assms show ?thesis + by auto +qed + +lemma zorder_ge_0: + assumes "f analytic_on {z}" "frequently (\z. f z \ 0) (at z)" + shows "zorder f z \ 0" +proof - + have *: "(\w. f (z + w)) has_laurent_expansion fps_to_fls (fps_expansion f z)" + using assms by (simp add: analytic_at_imp_has_fps_expansion has_laurent_expansion_fps) + from * assms(2) have "fps_to_fls (fps_expansion f z) \ 0" + by (auto simp: has_laurent_expansion_def frequently_def at_to_0' eventually_filtermap add_ac) + with has_laurent_expansion_zorder[OF *] show ?thesis + by (simp add: fls_subdegree_fls_to_fps) +qed + +lemma zorder_eq_0_iff: + assumes "f analytic_on {z}" "frequently (\w. f w \ 0) (at z)" + shows "zorder f z = 0 \ f z \ 0" +proof + assume "f z \ 0" + thus "zorder f z = 0" + using assms zorder_eq_0I by blast +next + assume "zorder f z = 0" + thus "f z \ 0" + using assms zorder_pos_iff' by fastforce +qed + +lemma dist_mult_left: + "dist (a * b) (a * c :: 'a :: real_normed_field) = norm a * dist b c" + unfolding dist_norm right_diff_distrib [symmetric] norm_mult by simp + +lemma dist_mult_right: + "dist (b * a) (c * a :: 'a :: real_normed_field) = norm a * dist b c" + using dist_mult_left[of a b c] by (simp add: mult_ac) + +lemma zorder_scale: + assumes "f analytic_on {a * z}" "eventually (\w. f w \ 0) (at (a * z))" "a \ 0" + shows "zorder (\w. f (a * w)) z = zorder f (a * z)" +proof - + from assms(1) obtain r where r: "r > 0" "f holomorphic_on ball (a * z) r" + by (auto simp: analytic_on_def) + have *: "open (ball (a * z) r)" "connected (ball (a * z) r)" "a * z \ ball (a * z) r" + using r \a \ 0\ by (auto simp: dist_norm) + from assms(2) have "eventually (\w. f w \ 0 \ w \ ball (a * z) r - {a * z}) (at (a * z))" + using \r > 0\ by (intro eventually_conj eventually_at_in_open) auto + then obtain z0 where "f z0 \ 0 \ z0 \ ball (a * z) r - {a * z}" + using eventually_happens[of _ "at (a * z)"] by force + hence **: "\w\ball (a * z) r. f w \ 0" + by blast + + define n where "n = nat (zorder f (a * z))" + obtain r' where r': + "(if f (a * z) = 0 then 0 < zorder f (a * z) else zorder f (a * z) = 0)" + "r' > 0" "cball (a * z) r' \ ball (a * z) r" "zor_poly f (a * z) holomorphic_on cball (a * z) r'" + "\w. w \ cball (a * z) r' \ + f w = zor_poly f (a * z) w * (w - a * z) ^ n \ zor_poly f (a * z) w \ 0" + unfolding n_def using zorder_exist_zero[OF r(2) * **] by blast + + show ?thesis + proof (rule zorder_eqI) + show "open (ball z (r' / norm a))" "z \ ball z (r' / norm a)" + using r \r' > 0\ \a \ 0\ by auto + have "(*) a ` ball z (r' / cmod a) \ cball (a * z) r'" + proof safe + fix w assume "w \ ball z (r' / cmod a)" + thus "a * w \ cball (a * z) r'" + using dist_mult_left[of a z w] \a \ 0\ by (auto simp: divide_simps mult_ac) + qed + thus "(\w. a ^ n * (zor_poly f (a * z) \ (\w. a * w)) w) holomorphic_on ball z (r' / norm a)" + using \a \ 0\ by (intro holomorphic_on_compose_gen[OF _ r'(4)] holomorphic_intros) auto + show "a ^ n * (zor_poly f (a * z) \ (\w. a * w)) z \ 0" + using r' \a \ 0\ by auto + show "f (a * w) = a ^ n * (zor_poly f (a * z) \ (*) a) w * (w - z) powr of_int (zorder f (a * z))" + if "w \ ball z (r' / norm a)" "w \ z" for w + proof - + have "f (a * w) = zor_poly f (a * z) (a * w) * (a * (w - z)) ^ n" + using that r'(5)[of "a * w"] dist_mult_left[of a z w] \a \ 0\ unfolding ring_distribs + by (auto simp: divide_simps mult_ac) + also have "\ = a ^ n * zor_poly f (a * z) (a * w) * (w - z) ^ n" + by (subst power_mult_distrib) (auto simp: mult_ac) + also have "(w - z) ^ n = (w - z) powr of_nat n" + using \w \ z\ by (subst powr_nat') auto + also have "of_nat n = of_int (zorder f (a * z))" + using r'(1) by (auto simp: n_def split: if_splits) + finally show ?thesis + unfolding o_def n_def . + qed + qed +qed + +lemma subdegree_fps_compose [simp]: + fixes F G :: "'a :: idom fps" + assumes [simp]: "fps_nth G 0 = 0" + shows "subdegree (fps_compose F G) = subdegree F * subdegree G" +proof (cases "G = 0"; cases "F = 0") + assume [simp]: "G \ 0" "F \ 0" + define m where "m = subdegree F" + define F' where "F' = fps_shift m F" + have F_eq: "F = F' * fps_X ^ m" + unfolding F'_def by (simp add: fps_shift_times_fps_X_power m_def) + have [simp]: "F' \ 0" + using \F \ 0\ unfolding F_eq by auto + have "subdegree (fps_compose F G) = subdegree (fps_compose F' G) + m * subdegree G" + by (simp add: F_eq fps_compose_mult_distrib fps_compose_eq_0_iff flip: fps_compose_power) + also have "subdegree (fps_compose F' G) = 0" + by (intro subdegree_eq_0) (auto simp: F'_def m_def) + finally show ?thesis by (simp add: m_def) +qed auto + +lemma fls_subdegree_power_int [simp]: + fixes F :: "'a :: field fls" + shows "fls_subdegree (F powi n) = n * fls_subdegree F" + by (auto simp: power_int_def fls_subdegree_pow) + +lemma subdegree_fls_compose_fps [simp]: + fixes G :: "'a :: field fps" + assumes [simp]: "fps_nth G 0 = 0" + shows "fls_subdegree (fls_compose_fps F G) = fls_subdegree F * subdegree G" +proof (cases "F = 0"; cases "G = 0") + assume [simp]: "G \ 0" "F \ 0" + have nz1: "fls_base_factor_to_fps F \ 0" + using \F \ 0\ fls_base_factor_to_fps_nonzero by blast + show ?thesis + unfolding fls_compose_fps_def using nz1 + by (subst fls_subdegree_mult) (simp_all add: fps_compose_eq_0_iff fls_subdegree_fls_to_fps) +qed (auto simp: fls_compose_fps_0_right) + +lemma zorder_compose_aux: + assumes "isolated_singularity_at f 0" "not_essential f 0" + assumes G: "g has_fps_expansion G" "G \ 0" "g 0 = 0" + assumes "eventually (\w. f w \ 0) (at 0)" + shows "zorder (f \ g) 0 = zorder f 0 * subdegree G" +proof - + obtain F where F: "f has_laurent_expansion F" + using not_essential_has_laurent_expansion_0[OF assms(1,2)] by blast + have [simp]: "fps_nth G 0 = 0" + using G \g 0 = 0\ by (simp add: has_fps_expansion_imp_0_eq_fps_nth_0) + note [simp] = \G \ 0\ \g 0 = 0\ + have [simp]: "F \ 0" + using has_laurent_expansion_eventually_nonzero_iff[of f 0 F] F assms by simp + have FG: "(f \ g) has_laurent_expansion fls_compose_fps F G" + by (intro has_laurent_expansion_compose has_laurent_expansion_fps F G) auto + + have "zorder (f \ g) 0 = fls_subdegree (fls_compose_fps F G)" + using has_laurent_expansion_zorder_0 [OF FG] by (auto simp: fls_compose_fps_eq_0_iff) + also have "\ = fls_subdegree F * int (subdegree G)" + by simp + also have "fls_subdegree F = zorder f 0" + using has_laurent_expansion_zorder_0 [OF F] by auto + finally show ?thesis . +qed + +lemma zorder_compose: + assumes "isolated_singularity_at f (g z)" "not_essential f (g z)" + assumes G: "(\x. g (z + x) - g z) has_fps_expansion G" "G \ 0" + assumes "eventually (\w. f w \ 0) (at (g z))" + shows "zorder (f \ g) z = zorder f (g z) * subdegree G" +proof - + define f' where "f' = (\w. f (g z + w))" + define g' where "g' = (\w. g (z + w) - g z)" + have "zorder f (g z) = zorder f' 0" + by (simp add: f'_def zorder_shift' add_ac) + have "zorder (\x. g x - g z) z = zorder g' 0" + by (simp add: g'_def zorder_shift' add_ac) + have "zorder (f \ g) z = zorder (f' \ g') 0" + by (simp add: zorder_shift' f'_def g'_def add_ac o_def) + also have "\ = zorder f' 0 * int (subdegree G)" + proof (rule zorder_compose_aux) + show "isolated_singularity_at f' 0" unfolding f'_def + using assms has_laurent_expansion_isolated_0 not_essential_has_laurent_expansion by blast + show "not_essential f' 0" unfolding f'_def + using assms has_laurent_expansion_not_essential_0 not_essential_has_laurent_expansion by blast + qed (use assms in \auto simp: f'_def g'_def at_to_0' eventually_filtermap add_ac\) + also have "zorder f' 0 = zorder f (g z)" + by (simp add: f'_def zorder_shift' add_ac) + finally show ?thesis . +qed + +lemma fps_to_fls_eq_fls_const_iff [simp]: "fps_to_fls F = fls_const c \ F = fps_const c" +proof + assume "F = fps_const c" + thus "fps_to_fls F = fls_const c" + by simp +next + assume "fps_to_fls F = fls_const c" + thus "F = fps_const c" + by (metis fls_regpart_const fls_regpart_fps_trivial) +qed + +lemma zorder_compose': + assumes "isolated_singularity_at f (g z)" "not_essential f (g z)" + assumes "g analytic_on {z}" + assumes "eventually (\w. f w \ 0) (at (g z))" + assumes "eventually (\w. g w \ g z) (at z)" + shows "zorder (f \ g) z = zorder f (g z) * zorder (\x. g x - g z) z" +proof - + obtain G where G [fps_expansion_intros]: "(\x. g (z + x)) has_fps_expansion G" + using assms analytic_at_imp_has_fps_expansion by blast + have G': "(\x. g (z + x) - g z) has_fps_expansion G - fps_const (g z)" + by (intro fps_expansion_intros) + hence G'': "(\x. g (z + x) - g z) has_laurent_expansion fps_to_fls (G - fps_const (g z))" + using has_laurent_expansion_fps by blast + have nz: "G - fps_const (g z) \ 0" + using has_laurent_expansion_eventually_nonzero_iff[OF G''] assms by auto + have "zorder (f \ g) z = zorder f (g z) * subdegree (G - fps_const (g z))" + proof (rule zorder_compose) + show "(\x. g (z + x) - g z) has_fps_expansion G - fps_const (g z)" + by (intro fps_expansion_intros) + qed (use assms nz in auto) + also have "int (subdegree (G - fps_const (g z))) = fls_subdegree (fps_to_fls G - fls_const (g z))" + by (simp flip: fls_subdegree_fls_to_fps) + also have "\ = zorder (\x. g x - g z) z" + using has_laurent_expansion_zorder [OF G''] nz by auto + finally show ?thesis . +qed + +lemma analytic_at_cong: + assumes "eventually (\x. f x = g x) (nhds x)" "x = y" + shows "f analytic_on {x} \ g analytic_on {y}" +proof - + have "g analytic_on {x}" if "f analytic_on {x}" "eventually (\x. f x = g x) (nhds x)" for f g + proof - + have "(\y. f (x + y)) has_fps_expansion fps_expansion f x" + by (rule analytic_at_imp_has_fps_expansion) fact + also have "?this \ (\y. g (x + y)) has_fps_expansion fps_expansion f x" + using that by (intro has_fps_expansion_cong refl) (auto simp: nhds_to_0' eventually_filtermap) + finally show ?thesis + by (rule has_fps_expansion_imp_analytic) + qed + from this[of f g] this[of g f] show ?thesis using assms + by (auto simp: eq_commute) +qed + + +lemma has_laurent_expansion_sin' [laurent_expansion_intros]: + "sin has_laurent_expansion fps_to_fls (fps_sin 1)" + using has_fps_expansion_sin' has_fps_expansion_to_laurent by blast + +lemma has_laurent_expansion_cos' [laurent_expansion_intros]: + "cos has_laurent_expansion fps_to_fls (fps_cos 1)" + using has_fps_expansion_cos' has_fps_expansion_to_laurent by blast + +lemma has_laurent_expansion_sin [laurent_expansion_intros]: + "(\z. sin (c * z)) has_laurent_expansion fps_to_fls (fps_sin c)" + by (intro has_laurent_expansion_fps has_fps_expansion_sin) + +lemma has_laurent_expansion_cos [laurent_expansion_intros]: + "(\z. cos (c * z)) has_laurent_expansion fps_to_fls (fps_cos c)" + by (intro has_laurent_expansion_fps has_fps_expansion_cos) + +lemma has_laurent_expansion_tan' [laurent_expansion_intros]: + "tan has_laurent_expansion fps_to_fls (fps_tan 1)" + using has_fps_expansion_tan' has_fps_expansion_to_laurent by blast + +lemma has_laurent_expansion_tan [laurent_expansion_intros]: + "(\z. tan (c * z)) has_laurent_expansion fps_to_fls (fps_tan c)" + by (intro has_laurent_expansion_fps has_fps_expansion_tan) + +end diff -r 29032b496f2e -r c6b50597abbc src/HOL/Complex_Analysis/Meromorphic.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Complex_Analysis/Meromorphic.thy Thu Feb 16 12:21:21 2023 +0000 @@ -0,0 +1,2333 @@ +theory Meromorphic + imports Laurent_Convergence Riemann_Mapping +begin + +lemma analytic_at_cong: + assumes "eventually (\x. f x = g x) (nhds x)" "x = y" + shows "f analytic_on {x} \ g analytic_on {y}" +proof - + have "g analytic_on {x}" if "f analytic_on {x}" "eventually (\x. f x = g x) (nhds x)" for f g + proof - + have "(\y. f (x + y)) has_fps_expansion fps_expansion f x" + by (rule analytic_at_imp_has_fps_expansion) fact + also have "?this \ (\y. g (x + y)) has_fps_expansion fps_expansion f x" + using that by (intro has_fps_expansion_cong refl) (auto simp: nhds_to_0' eventually_filtermap) + finally show ?thesis + by (rule has_fps_expansion_imp_analytic) + qed + from this[of f g] this[of g f] show ?thesis using assms + by (auto simp: eq_commute) +qed + +definition remove_sings :: "(complex \ complex) \ complex \ complex" where + "remove_sings f z = (if \c. f \z\ c then Lim (at z) f else 0)" + +lemma remove_sings_eqI [intro]: + assumes "f \z\ c" + shows "remove_sings f z = c" + using assms unfolding remove_sings_def by (auto simp: tendsto_Lim) + +lemma remove_sings_at_analytic [simp]: + assumes "f analytic_on {z}" + shows "remove_sings f z = f z" + using assms by (intro remove_sings_eqI) (simp add: analytic_at_imp_isCont isContD) + +lemma remove_sings_at_pole [simp]: + assumes "is_pole f z" + shows "remove_sings f z = 0" + using assms unfolding remove_sings_def is_pole_def + by (meson at_neq_bot not_tendsto_and_filterlim_at_infinity) + +lemma eventually_remove_sings_eq_at: + assumes "isolated_singularity_at f z" + shows "eventually (\w. remove_sings f w = f w) (at z)" +proof - + from assms obtain r where r: "r > 0" "f analytic_on ball z r - {z}" + by (auto simp: isolated_singularity_at_def) + hence *: "f analytic_on {w}" if "w \ ball z r - {z}" for w + using r that by (auto intro: analytic_on_subset) + have "eventually (\w. w \ ball z r - {z}) (at z)" + using r by (intro eventually_at_in_open) auto + thus ?thesis + by eventually_elim (auto simp: remove_sings_at_analytic *) +qed + +lemma eventually_remove_sings_eq_nhds: + assumes "f analytic_on {z}" + shows "eventually (\w. remove_sings f w = f w) (nhds z)" +proof - + from assms obtain A where A: "open A" "z \ A" "f holomorphic_on A" + by (auto simp: analytic_at) + have "eventually (\z. z \ A) (nhds z)" + by (intro eventually_nhds_in_open A) + thus ?thesis + proof eventually_elim + case (elim w) + from elim have "f analytic_on {w}" + using A analytic_at by blast + thus ?case by auto + qed +qed + +lemma remove_sings_compose: + assumes "filtermap g (at z) = at z'" + shows "remove_sings (f \ g) z = remove_sings f z'" +proof (cases "\c. f \z'\ c") + case True + then obtain c where c: "f \z'\ c" + by auto + from c have "remove_sings f z' = c" + by blast + moreover from c have "remove_sings (f \ g) z = c" + using c by (intro remove_sings_eqI) (auto simp: filterlim_def filtermap_compose assms) + ultimately show ?thesis + by simp +next + case False + hence "\(\c. (f \ g) \z\ c)" + by (auto simp: filterlim_def filtermap_compose assms) + with False show ?thesis + by (auto simp: remove_sings_def) +qed + +lemma remove_sings_cong: + assumes "eventually (\x. f x = g x) (at z)" "z = z'" + shows "remove_sings f z = remove_sings g z'" +proof (cases "\c. f \z\ c") + case True + then obtain c where c: "f \z\ c" by blast + hence "remove_sings f z = c" + by blast + moreover have "f \z\ c \ g \z'\ c" + using assms by (intro filterlim_cong refl) auto + with c have "remove_sings g z' = c" + by (intro remove_sings_eqI) auto + ultimately show ?thesis + by simp +next + case False + have "f \z\ c \ g \z'\ c" for c + using assms by (intro filterlim_cong) auto + with False show ?thesis + by (auto simp: remove_sings_def) +qed + + +lemma deriv_remove_sings_at_analytic [simp]: + assumes "f analytic_on {z}" + shows "deriv (remove_sings f) z = deriv f z" + apply (rule deriv_cong_ev) + apply (rule eventually_remove_sings_eq_nhds) + using assms by auto + +lemma isolated_singularity_at_remove_sings [simp, intro]: + assumes "isolated_singularity_at f z" + shows "isolated_singularity_at (remove_sings f) z" + using isolated_singularity_at_cong[OF eventually_remove_sings_eq_at[OF assms] refl] assms + by simp + +lemma not_essential_remove_sings_iff [simp]: + assumes "isolated_singularity_at f z" + shows "not_essential (remove_sings f) z \ not_essential f z" + using not_essential_cong[OF eventually_remove_sings_eq_at[OF assms(1)] refl] + by simp + +lemma not_essential_remove_sings [intro]: + assumes "isolated_singularity_at f z" "not_essential f z" + shows "not_essential (remove_sings f) z" + by (subst not_essential_remove_sings_iff) (use assms in auto) + +lemma + assumes "isolated_singularity_at f z" + shows is_pole_remove_sings_iff [simp]: + "is_pole (remove_sings f) z \ is_pole f z" + and zorder_remove_sings [simp]: + "zorder (remove_sings f) z = zorder f z" + and zor_poly_remove_sings [simp]: + "zor_poly (remove_sings f) z = zor_poly f z" + and has_laurent_expansion_remove_sings_iff [simp]: + "(\w. remove_sings f (z + w)) has_laurent_expansion F \ + (\w. f (z + w)) has_laurent_expansion F" + and tendsto_remove_sings_iff [simp]: + "remove_sings f \z\ c \ f \z\ c" + by (intro is_pole_cong eventually_remove_sings_eq_at refl zorder_cong + zor_poly_cong has_laurent_expansion_cong' tendsto_cong assms)+ + +lemma get_all_poles_from_remove_sings: + fixes f:: "complex \ complex" + defines "ff\remove_sings f" + assumes f_holo:"f holomorphic_on s - pts" and "finite pts" + "pts\s" "open s" and not_ess:"\x\pts. not_essential f x" + obtains pts' where + "pts' \ pts" "finite pts'" "ff holomorphic_on s - pts'" "\x\pts'. is_pole ff x" +proof - + define pts' where "pts' = {x\pts. is_pole f x}" + + have "pts' \ pts" unfolding pts'_def by auto + then have "finite pts'" using \finite pts\ + using rev_finite_subset by blast + then have "open (s - pts')" using \open s\ + by (simp add: finite_imp_closed open_Diff) + + have isolated:"isolated_singularity_at f z" if "z\pts" for z + proof (rule isolated_singularity_at_holomorphic) + show "f holomorphic_on (s-(pts-{z})) - {z}" + by (metis Diff_insert f_holo insert_Diff that) + show " open (s - (pts - {z}))" + by (meson assms(3) assms(5) finite_Diff finite_imp_closed open_Diff) + show "z \ s - (pts - {z})" + using assms(4) that by auto + qed + + have "ff holomorphic_on s - pts'" + proof (rule no_isolated_singularity') + show "(ff \ ff z) (at z within s - pts')" if "z \ pts-pts'" for z + proof - + have "at z within s - pts' = at z" + apply (rule at_within_open) + using \open (s - pts')\ that \pts\s\ by auto + moreover have "ff \z\ ff z" + unfolding ff_def + proof (subst tendsto_remove_sings_iff) + show "isolated_singularity_at f z" + apply (rule isolated) + using that by auto + have "not_essential f z" + using not_ess that by auto + moreover have "\is_pole f z" + using that unfolding pts'_def by auto + ultimately have "\c. f \z\ c" + unfolding not_essential_def by auto + then show "f \z\ remove_sings f z" + using remove_sings_eqI by blast + qed + ultimately show ?thesis by auto + qed + have "ff holomorphic_on s - pts" + using f_holo + proof (elim holomorphic_transform) + fix x assume "x \ s - pts" + then have "f analytic_on {x}" + using assms(3) assms(5) f_holo + by (meson finite_imp_closed + holomorphic_on_imp_analytic_at open_Diff) + from remove_sings_at_analytic[OF this] + show "f x = ff x" unfolding ff_def by auto + qed + then show "ff holomorphic_on s - pts' - (pts - pts')" + apply (elim holomorphic_on_subset) + by blast + show "open (s - pts')" + by (simp add: \open (s - pts')\) + show "finite (pts - pts')" + by (simp add: assms(3)) + qed + moreover have "\x\pts'. is_pole ff x" + unfolding pts'_def + using ff_def is_pole_remove_sings_iff isolated by blast + moreover note \pts' \ pts\ \finite pts'\ + ultimately show ?thesis using that by auto +qed + +lemma remove_sings_eq_0_iff: + assumes "not_essential f w" + shows "remove_sings f w = 0 \ is_pole f w \ f \w\ 0" +proof (cases "is_pole f w") + case True + then show ?thesis by simp +next + case False + then obtain c where c:"f \w\ c" + using \not_essential f w\ unfolding not_essential_def by auto + then show ?thesis + using False remove_sings_eqI by auto +qed + +definition meromorphic_on:: "[complex \ complex, complex set, complex set] \ bool" + ("_ (meromorphic'_on) _ _" [50,50,50]50) where + "f meromorphic_on D pts \ + open D \ pts \ D \ (\z\pts. isolated_singularity_at f z \ not_essential f z) \ + (\z\D. \(z islimpt pts)) \ (f holomorphic_on D-pts)" + +lemma meromorphic_imp_holomorphic: "f meromorphic_on D pts \ f holomorphic_on (D - pts)" + unfolding meromorphic_on_def by auto + +lemma meromorphic_imp_closedin_pts: + assumes "f meromorphic_on D pts" + shows "closedin (top_of_set D) pts" + by (meson assms closedin_limpt meromorphic_on_def) + +lemma meromorphic_imp_open_diff': + assumes "f meromorphic_on D pts" "pts' \ pts" + shows "open (D - pts')" +proof - + have "D - pts' = D - closure pts'" + proof safe + fix x assume x: "x \ D" "x \ closure pts'" "x \ pts'" + hence "x islimpt pts'" + by (subst islimpt_in_closure) auto + hence "x islimpt pts" + by (rule islimpt_subset) fact + with assms x show False + by (auto simp: meromorphic_on_def) + qed (use closure_subset in auto) + then show ?thesis + using assms meromorphic_on_def by auto +qed + +lemma meromorphic_imp_open_diff: "f meromorphic_on D pts \ open (D - pts)" + by (erule meromorphic_imp_open_diff') auto + +lemma meromorphic_pole_subset: + assumes merf: "f meromorphic_on D pts" + shows "{x\D. is_pole f x} \ pts" + by (smt (verit) Diff_iff assms mem_Collect_eq meromorphic_imp_open_diff + meromorphic_on_def not_is_pole_holomorphic subsetI) + +named_theorems meromorphic_intros + +lemma meromorphic_on_subset: + assumes "f meromorphic_on A pts" "open B" "B \ A" "pts' = pts \ B" + shows "f meromorphic_on B pts'" + unfolding meromorphic_on_def +proof (intro ballI conjI) + fix z assume "z \ B" + show "\z islimpt pts'" + proof + assume "z islimpt pts'" + hence "z islimpt pts" + by (rule islimpt_subset) (use \pts' = _\ in auto) + thus False using \z \ B\ \B \ A\ assms(1) + by (auto simp: meromorphic_on_def) + qed +qed (use assms in \auto simp: meromorphic_on_def\) + +lemma meromorphic_on_superset_pts: + assumes "f meromorphic_on A pts" "pts \ pts'" "pts' \ A" "\x\A. \x islimpt pts'" + shows "f meromorphic_on A pts'" + unfolding meromorphic_on_def +proof (intro conjI ballI impI) + fix z assume "z \ pts'" + from assms(1) have holo: "f holomorphic_on A - pts" and "open A" + unfolding meromorphic_on_def by blast+ + have "open (A - pts)" + by (intro meromorphic_imp_open_diff[OF assms(1)]) + + show "isolated_singularity_at f z" + proof (cases "z \ pts") + case False + thus ?thesis + using \open (A - pts)\ assms \z \ pts'\ + by (intro isolated_singularity_at_holomorphic[of _ "A - pts"] holomorphic_on_subset[OF holo]) + auto + qed (use assms in \auto simp: meromorphic_on_def\) + + show "not_essential f z" + proof (cases "z \ pts") + case False + thus ?thesis + using \open (A - pts)\ assms \z \ pts'\ + by (intro not_essential_holomorphic[of _ "A - pts"] holomorphic_on_subset[OF holo]) + auto + qed (use assms in \auto simp: meromorphic_on_def\) +qed (use assms in \auto simp: meromorphic_on_def\) + +lemma meromorphic_on_no_singularities: "f meromorphic_on A {} \ f holomorphic_on A \ open A" + by (auto simp: meromorphic_on_def) + +lemma holomorphic_on_imp_meromorphic_on: + "f holomorphic_on A \ pts \ A \ open A \ \x\A. \x islimpt pts \ f meromorphic_on A pts" + by (rule meromorphic_on_superset_pts[where pts = "{}"]) + (auto simp: meromorphic_on_no_singularities) + +lemma meromorphic_on_const [meromorphic_intros]: + assumes "open A" "\x\A. \x islimpt pts" "pts \ A" + shows "(\_. c) meromorphic_on A pts" + by (rule holomorphic_on_imp_meromorphic_on) (use assms in auto) + +lemma meromorphic_on_ident [meromorphic_intros]: + assumes "open A" "\x\A. \x islimpt pts" "pts \ A" + shows "(\x. x) meromorphic_on A pts" + by (rule holomorphic_on_imp_meromorphic_on) (use assms in auto) + +lemma meromorphic_on_id [meromorphic_intros]: + assumes "open A" "\x\A. \x islimpt pts" "pts \ A" + shows "id meromorphic_on A pts" + using meromorphic_on_ident assms unfolding id_def . + +lemma not_essential_add [singularity_intros]: + assumes f_ness: "not_essential f z" and g_ness: "not_essential g z" + assumes f_iso: "isolated_singularity_at f z" and g_iso: "isolated_singularity_at g z" + shows "not_essential (\w. f w + g w) z" +proof - + have "(\w. f (z + w) + g (z + w)) has_laurent_expansion laurent_expansion f z + laurent_expansion g z" + by (intro not_essential_has_laurent_expansion laurent_expansion_intros assms) + hence "not_essential (\w. f (z + w) + g (z + w)) 0" + using has_laurent_expansion_not_essential_0 by blast + thus ?thesis + by (simp add: not_essential_shift_0) +qed + +lemma meromorphic_on_uminus [meromorphic_intros]: + assumes "f meromorphic_on A pts" + shows "(\z. -f z) meromorphic_on A pts" + unfolding meromorphic_on_def + by (use assms in \auto simp: meromorphic_on_def intro!: holomorphic_intros singularity_intros\) + +lemma meromorphic_on_add [meromorphic_intros]: + assumes "f meromorphic_on A pts" "g meromorphic_on A pts" + shows "(\z. f z + g z) meromorphic_on A pts" + unfolding meromorphic_on_def + by (use assms in \auto simp: meromorphic_on_def intro!: holomorphic_intros singularity_intros\) + +lemma meromorphic_on_add': + assumes "f meromorphic_on A pts1" "g meromorphic_on A pts2" + shows "(\z. f z + g z) meromorphic_on A (pts1 \ pts2)" +proof (rule meromorphic_intros) + show "f meromorphic_on A (pts1 \ pts2)" + by (rule meromorphic_on_superset_pts[OF assms(1)]) + (use assms in \auto simp: meromorphic_on_def islimpt_Un\) + show "g meromorphic_on A (pts1 \ pts2)" + by (rule meromorphic_on_superset_pts[OF assms(2)]) + (use assms in \auto simp: meromorphic_on_def islimpt_Un\) +qed + +lemma meromorphic_on_add_const [meromorphic_intros]: + assumes "f meromorphic_on A pts" + shows "(\z. f z + c) meromorphic_on A pts" + unfolding meromorphic_on_def + by (use assms in \auto simp: meromorphic_on_def intro!: holomorphic_intros singularity_intros\) + +lemma meromorphic_on_minus_const [meromorphic_intros]: + assumes "f meromorphic_on A pts" + shows "(\z. f z - c) meromorphic_on A pts" + using meromorphic_on_add_const[OF assms,of "-c"] by simp + +lemma meromorphic_on_diff [meromorphic_intros]: + assumes "f meromorphic_on A pts" "g meromorphic_on A pts" + shows "(\z. f z - g z) meromorphic_on A pts" + using meromorphic_on_add[OF assms(1) meromorphic_on_uminus[OF assms(2)]] by simp + +lemma meromorphic_on_diff': + assumes "f meromorphic_on A pts1" "g meromorphic_on A pts2" + shows "(\z. f z - g z) meromorphic_on A (pts1 \ pts2)" +proof (rule meromorphic_intros) + show "f meromorphic_on A (pts1 \ pts2)" + by (rule meromorphic_on_superset_pts[OF assms(1)]) + (use assms in \auto simp: meromorphic_on_def islimpt_Un\) + show "g meromorphic_on A (pts1 \ pts2)" + by (rule meromorphic_on_superset_pts[OF assms(2)]) + (use assms in \auto simp: meromorphic_on_def islimpt_Un\) +qed + +lemma meromorphic_on_mult [meromorphic_intros]: + assumes "f meromorphic_on A pts" "g meromorphic_on A pts" + shows "(\z. f z * g z) meromorphic_on A pts" + unfolding meromorphic_on_def + by (use assms in \auto simp: meromorphic_on_def intro!: holomorphic_intros singularity_intros\) + +lemma meromorphic_on_mult': + assumes "f meromorphic_on A pts1" "g meromorphic_on A pts2" + shows "(\z. f z * g z) meromorphic_on A (pts1 \ pts2)" +proof (rule meromorphic_intros) + show "f meromorphic_on A (pts1 \ pts2)" + by (rule meromorphic_on_superset_pts[OF assms(1)]) + (use assms in \auto simp: meromorphic_on_def islimpt_Un\) + show "g meromorphic_on A (pts1 \ pts2)" + by (rule meromorphic_on_superset_pts[OF assms(2)]) + (use assms in \auto simp: meromorphic_on_def islimpt_Un\) +qed + + + +lemma meromorphic_on_imp_not_essential: + assumes "f meromorphic_on A pts" "z \ A" + shows "not_essential f z" +proof (cases "z \ pts") + case False + thus ?thesis + using not_essential_holomorphic[of f "A - pts" z] meromorphic_imp_open_diff[OF assms(1)] assms + by (auto simp: meromorphic_on_def) +qed (use assms in \auto simp: meromorphic_on_def\) + +lemma meromorphic_imp_analytic: "f meromorphic_on D pts \ f analytic_on (D - pts)" + unfolding meromorphic_on_def + apply (subst analytic_on_open) + using meromorphic_imp_open_diff meromorphic_on_id apply blast + apply auto + done + +lemma not_islimpt_isolated_zeros: + assumes mero: "f meromorphic_on A pts" and "z \ A" + shows "\z islimpt {w\A. isolated_zero f w}" +proof + assume islimpt: "z islimpt {w\A. isolated_zero f w}" + have holo: "f holomorphic_on A - pts" and "open A" + using assms by (auto simp: meromorphic_on_def) + have open': "open (A - (pts - {z}))" + by (intro meromorphic_imp_open_diff'[OF mero]) auto + then obtain r where r: "r > 0" "ball z r \ A - (pts - {z})" + using meromorphic_imp_open_diff[OF mero] \z \ A\ openE by blast + + have "not_essential f z" + using assms by (rule meromorphic_on_imp_not_essential) + then consider c where "f \z\ c" | "is_pole f z" + unfolding not_essential_def by blast + thus False + proof cases + assume "is_pole f z" + hence "eventually (\w. f w \ 0) (at z)" + by (rule non_zero_neighbour_pole) + hence "\z islimpt {w. f w = 0}" + by (simp add: islimpt_conv_frequently_at frequently_def) + moreover have "z islimpt {w. f w = 0}" + using islimpt by (rule islimpt_subset) (auto simp: isolated_zero_def) + ultimately show False by contradiction + next + fix c assume c: "f \z\ c" + define g where "g = (\w. if w = z then c else f w)" + have holo': "g holomorphic_on A - (pts - {z})" unfolding g_def + by (intro removable_singularity holomorphic_on_subset[OF holo] open' c) auto + + have eq_zero: "g w = 0" if "w \ ball z r" for w + proof (rule analytic_continuation[where f = g]) + show "open (ball z r)" "connected (ball z r)" "{w\ball z r. isolated_zero f w} \ ball z r" + by auto + have "z islimpt {w\A. isolated_zero f w} \ ball z r" + using islimpt \r > 0\ by (intro islimpt_Int_eventually eventually_at_in_open') auto + also have "\ = {w\ball z r. isolated_zero f w}" + using r by auto + finally show "z islimpt {w\ball z r. isolated_zero f w}" + by simp + next + fix w assume w: "w \ {w\ball z r. isolated_zero f w}" + show "g w = 0" + proof (cases "w = z") + case False + thus ?thesis using w by (auto simp: g_def isolated_zero_def) + next + case True + have "z islimpt {z. f z = 0}" + using islimpt by (rule islimpt_subset) (auto simp: isolated_zero_def) + thus ?thesis + using w by (simp add: isolated_zero_altdef True) + qed + qed (use r that in \auto intro!: holomorphic_on_subset[OF holo'] simp: isolated_zero_def\) + + have "infinite ({w\A. isolated_zero f w} \ ball z r)" + using islimpt \r > 0\ unfolding islimpt_eq_infinite_ball by blast + hence "{w\A. isolated_zero f w} \ ball z r \ {}" + by force + then obtain z0 where z0: "z0 \ A" "isolated_zero f z0" "z0 \ ball z r" + by blast + have "\\<^sub>F y in at z0. y \ ball z r - (if z = z0 then {} else {z}) - {z0}" + using r z0 by (intro eventually_at_in_open) auto + hence "eventually (\w. f w = 0) (at z0)" + proof eventually_elim + case (elim w) + show ?case + using eq_zero[of w] elim by (auto simp: g_def split: if_splits) + qed + hence "eventually (\w. f w = 0) (at z0)" + by (auto simp: g_def eventually_at_filter elim!: eventually_mono split: if_splits) + moreover from z0 have "eventually (\w. f w \ 0) (at z0)" + by (simp add: isolated_zero_def) + ultimately have "eventually (\_. False) (at z0)" + by eventually_elim auto + thus False + by simp + qed +qed + +lemma closedin_isolated_zeros: + assumes "f meromorphic_on A pts" + shows "closedin (top_of_set A) {z\A. isolated_zero f z}" + unfolding closedin_limpt using not_islimpt_isolated_zeros[OF assms] by auto + +lemma meromorphic_on_deriv': + assumes "f meromorphic_on A pts" "open A" + assumes "\x. x \ A - pts \ (f has_field_derivative f' x) (at x)" + shows "f' meromorphic_on A pts" + unfolding meromorphic_on_def +proof (intro conjI ballI) + have "open (A - pts)" + by (intro meromorphic_imp_open_diff[OF assms(1)]) + thus "f' holomorphic_on A - pts" + by (rule derivative_is_holomorphic) (use assms in auto) +next + fix z assume "z \ pts" + hence "z \ A" + using assms(1) by (auto simp: meromorphic_on_def) + from \z \ pts\ obtain r where r: "r > 0" "f analytic_on ball z r - {z}" + using assms(1) by (auto simp: meromorphic_on_def isolated_singularity_at_def) + + have "open (ball z r \ (A - (pts - {z})))" + by (intro open_Int assms meromorphic_imp_open_diff'[OF assms(1)]) auto + then obtain r' where r': "r' > 0" "ball z r' \ ball z r \ (A - (pts - {z}))" + using r \z \ A\ by (subst (asm) open_contains_ball) fastforce + + have "open (ball z r' - {z})" + by auto + hence "f' holomorphic_on ball z r' - {z}" + by (rule derivative_is_holomorphic[of _ f]) (use r' in \auto intro!: assms(3)\) + moreover have "open (ball z r' - {z})" + by auto + ultimately show "isolated_singularity_at f' z" + unfolding isolated_singularity_at_def using \r' > 0\ + by (auto simp: analytic_on_open intro!: exI[of _ r']) +next + fix z assume z: "z \ pts" + hence z': "not_essential f z" "z \ A" + using assms by (auto simp: meromorphic_on_def) + from z'(1) show "not_essential f' z" + proof (rule not_essential_deriv') + show "z \ A - (pts - {z})" + using \z \ A\ by blast + show "open (A - (pts - {z}))" + by (intro meromorphic_imp_open_diff'[OF assms(1)]) auto + qed (use assms in auto) +qed (use assms in \auto simp: meromorphic_on_def\) + +lemma meromorphic_on_deriv [meromorphic_intros]: + assumes "f meromorphic_on A pts" "open A" + shows "deriv f meromorphic_on A pts" +proof (intro meromorphic_on_deriv'[OF assms(1)]) + have *: "open (A - pts)" + by (intro meromorphic_imp_open_diff[OF assms(1)]) + show "(f has_field_derivative deriv f x) (at x)" if "x \ A - pts" for x + using assms(1) by (intro holomorphic_derivI[OF _ * that]) (auto simp: meromorphic_on_def) +qed fact + +lemma meromorphic_on_imp_analytic_at: + assumes "f meromorphic_on A pts" "z \ A - pts" + shows "f analytic_on {z}" + using assms by (metis analytic_at meromorphic_imp_open_diff meromorphic_on_def) + +lemma meromorphic_compact_finite_pts: + assumes "f meromorphic_on D pts" "compact S" "S \ D" + shows "finite (S \ pts)" +proof - + { assume "infinite (S \ pts)" + then obtain z where "z \ S" and z: "z islimpt (S \ pts)" + using assms by (metis compact_eq_Bolzano_Weierstrass inf_le1) + then have False + using assms by (meson in_mono inf_le2 islimpt_subset meromorphic_on_def) } + then show ?thesis by metis +qed + +lemma meromorphic_imp_countable: + assumes "f meromorphic_on D pts" + shows "countable pts" +proof - + obtain K :: "nat \ complex set" where K: "D = (\n. K n)" "\n. compact (K n)" + using assms unfolding meromorphic_on_def by (metis open_Union_compact_subsets) + then have "pts = (\n. K n \ pts)" + using assms meromorphic_on_def by auto + moreover have "\n. finite (K n \ pts)" + by (metis K(1) K(2) UN_I assms image_iff meromorphic_compact_finite_pts rangeI subset_eq) + ultimately show ?thesis + by (metis countableI_type countable_UN countable_finite) +qed + +lemma meromorphic_imp_connected_diff': + assumes "f meromorphic_on D pts" "connected D" "pts' \ pts" + shows "connected (D - pts')" +proof (rule connected_open_diff_countable) + show "countable pts'" + by (rule countable_subset [OF assms(3)]) (use assms(1) in \auto simp: meromorphic_imp_countable\) +qed (use assms in \auto simp: meromorphic_on_def\) + +lemma meromorphic_imp_connected_diff: + assumes "f meromorphic_on D pts" "connected D" + shows "connected (D - pts)" + using meromorphic_imp_connected_diff'[OF assms order.refl] . + +lemma meromorphic_on_compose [meromorphic_intros]: + assumes f: "f meromorphic_on A pts" and g: "g holomorphic_on B" + assumes "open B" and "g ` B \ A" + shows "(\x. f (g x)) meromorphic_on B (isolated_points_of (g -` pts \ B))" + unfolding meromorphic_on_def +proof (intro ballI conjI) + fix z assume z: "z \ isolated_points_of (g -` pts \ B)" + hence z': "z \ B" "g z \ pts" + using isolated_points_of_subset by blast+ + have g': "g analytic_on {z}" + using g z' \open B\ analytic_at by blast + + show "isolated_singularity_at (\x. f (g x)) z" + by (rule isolated_singularity_at_compose[OF _ g']) (use f z' in \auto simp: meromorphic_on_def\) + show "not_essential (\x. f (g x)) z" + by (rule not_essential_compose[OF _ g']) (use f z' in \auto simp: meromorphic_on_def\) +next + fix z assume z: "z \ B" + hence "g z \ A" + using assms by auto + hence "\g z islimpt pts" + using f by (auto simp: meromorphic_on_def) + hence ev: "eventually (\w. w \ pts) (at (g z))" + by (auto simp: islimpt_conv_frequently_at frequently_def) + have g': "g analytic_on {z}" + by (rule holomorphic_on_imp_analytic_at[OF g]) (use assms z in auto) + + (* TODO: There's probably a useful lemma somewhere in here to extract... *) + have "eventually (\w. w \ isolated_points_of (g -` pts \ B)) (at z)" + proof (cases "isolated_zero (\w. g w - g z) z") + case True + have "eventually (\w. w \ pts) (at (g z))" + using ev by (auto simp: islimpt_conv_frequently_at frequently_def) + moreover have "g \z\ g z" + using analytic_at_imp_isCont[OF g'] isContD by blast + hence lim: "filterlim g (at (g z)) (at z)" + using True by (auto simp: filterlim_at isolated_zero_def) + have "eventually (\w. g w \ pts) (at z)" + using ev lim by (rule eventually_compose_filterlim) + thus ?thesis + by eventually_elim (auto simp: isolated_points_of_def) + next + case False + have "eventually (\w. g w - g z = 0) (nhds z)" + using False by (rule non_isolated_zero) (auto intro!: analytic_intros g') + hence "eventually (\w. g w = g z \ w \ B) (nhds z)" + using eventually_nhds_in_open[OF \open B\ \z \ B\] + by eventually_elim auto + then obtain X where X: "open X" "z \ X" "X \ B" "\x\X. g x = g z" + unfolding eventually_nhds by blast + + have "z0 \ isolated_points_of (g -` pts \ B)" if "z0 \ X" for z0 + proof (cases "g z \ pts") + case False + with that have "g z0 \ pts" + using X by metis + thus ?thesis + by (auto simp: isolated_points_of_def) + next + case True + have "eventually (\w. w \ X) (at z0)" + by (intro eventually_at_in_open') fact+ + hence "eventually (\w. w \ g -` pts \ B) (at z0)" + by eventually_elim (use X True in fastforce) + hence "frequently (\w. w \ g -` pts \ B) (at z0)" + by (meson at_neq_bot eventually_frequently) + thus "z0 \ isolated_points_of (g -` pts \ B)" + unfolding isolated_points_of_def by (auto simp: frequently_def) + qed + moreover have "eventually (\x. x \ X) (at z)" + by (intro eventually_at_in_open') fact+ + ultimately show ?thesis + by (auto elim!: eventually_mono) + qed + thus "\z islimpt isolated_points_of (g -` pts \ B)" + by (auto simp: islimpt_conv_frequently_at frequently_def) +next + have "f \ g analytic_on (\z\B - isolated_points_of (g -` pts \ B). {z})" + unfolding analytic_on_UN + proof + fix z assume z: "z \ B - isolated_points_of (g -` pts \ B)" + hence "z \ B" by blast + have g': "g analytic_on {z}" + by (rule holomorphic_on_imp_analytic_at[OF g]) (use assms z in auto) + show "f \ g analytic_on {z}" + proof (cases "g z \ pts") + case False + show ?thesis + proof (rule analytic_on_compose) + show "f analytic_on g ` {z}" using False z assms + by (auto intro!: meromorphic_on_imp_analytic_at[OF f]) + qed fact + next + case True + show ?thesis + proof (cases "isolated_zero (\w. g w - g z) z") + case False + hence "eventually (\w. g w - g z = 0) (nhds z)" + by (rule non_isolated_zero) (auto intro!: analytic_intros g') + hence "f \ g analytic_on {z} \ (\_. f (g z)) analytic_on {z}" + by (intro analytic_at_cong) (auto elim!: eventually_mono) + thus ?thesis + by simp + next + case True + hence ev: "eventually (\w. g w \ g z) (at z)" + by (auto simp: isolated_zero_def) + + have "\g z islimpt pts" + using \g z \ pts\ f by (auto simp: meromorphic_on_def) + hence "eventually (\w. w \ pts) (at (g z))" + by (auto simp: islimpt_conv_frequently_at frequently_def) + moreover have "g \z\ g z" + using analytic_at_imp_isCont[OF g'] isContD by blast + with ev have "filterlim g (at (g z)) (at z)" + by (auto simp: filterlim_at) + ultimately have "eventually (\w. g w \ pts) (at z)" + using eventually_compose_filterlim by blast + hence "z \ isolated_points_of (g -` pts \ B)" + using \g z \ pts\ \z \ B\ + by (auto simp: isolated_points_of_def elim!: eventually_mono) + with z show ?thesis by simp + qed + qed + qed + also have "\ = B - isolated_points_of (g -` pts \ B)" + by blast + finally show "(\x. f (g x)) holomorphic_on B - isolated_points_of (g -` pts \ B)" + unfolding o_def using analytic_imp_holomorphic by blast +qed (auto simp: isolated_points_of_def \open B\) + +lemma meromorphic_on_compose': + assumes f: "f meromorphic_on A pts" and g: "g holomorphic_on B" + assumes "open B" and "g ` B \ A" and "pts' = (isolated_points_of (g -` pts \ B))" + shows "(\x. f (g x)) meromorphic_on B pts'" + using meromorphic_on_compose[OF assms(1-4)] assms(5) by simp + +lemma meromorphic_on_inverse': "inverse meromorphic_on UNIV 0" + unfolding meromorphic_on_def + by (auto intro!: holomorphic_intros singularity_intros not_essential_inverse + isolated_singularity_at_inverse simp: islimpt_finite) + +lemma meromorphic_on_inverse [meromorphic_intros]: + assumes mero: "f meromorphic_on A pts" + shows "(\z. inverse (f z)) meromorphic_on A (pts \ {z\A. isolated_zero f z})" +proof - + have "open A" + using mero by (auto simp: meromorphic_on_def) + have open': "open (A - pts)" + by (intro meromorphic_imp_open_diff[OF mero]) + have holo: "f holomorphic_on A - pts" + using assms by (auto simp: meromorphic_on_def) + have ana: "f analytic_on A - pts" + using open' holo by (simp add: analytic_on_open) + + show ?thesis + unfolding meromorphic_on_def + proof (intro conjI ballI) + fix z assume z: "z \ pts \ {z\A. isolated_zero f z}" + have "isolated_singularity_at f z \ not_essential f z" + proof (cases "z \ pts") + case False + have "f holomorphic_on A - pts - {z}" + by (intro holomorphic_on_subset[OF holo]) auto + hence "isolated_singularity_at f z" + by (rule isolated_singularity_at_holomorphic) + (use z False in \auto intro!: meromorphic_imp_open_diff[OF mero]\) + moreover have "not_essential f z" + using z False + by (intro not_essential_holomorphic[OF holo] meromorphic_imp_open_diff[OF mero]) auto + ultimately show ?thesis by blast + qed (use assms in \auto simp: meromorphic_on_def\) + thus "isolated_singularity_at (\z. inverse (f z)) z" "not_essential (\z. inverse (f z)) z" + by (auto intro!: isolated_singularity_at_inverse not_essential_inverse) + next + fix z assume "z \ A" + hence "\ z islimpt {z\A. isolated_zero f z}" + by (rule not_islimpt_isolated_zeros[OF mero]) + thus "\ z islimpt pts \ {z \ A. isolated_zero f z}" using \z \ A\ + using mero by (auto simp: islimpt_Un meromorphic_on_def) + next + show "pts \ {z \ A. isolated_zero f z} \ A" + using mero by (auto simp: meromorphic_on_def) + next + have "(\z. inverse (f z)) analytic_on (\w\A - (pts \ {z \ A. isolated_zero f z}) . {w})" + unfolding analytic_on_UN + proof (intro ballI) + fix w assume w: "w \ A - (pts \ {z \ A. isolated_zero f z})" + show "(\z. inverse (f z)) analytic_on {w}" + proof (cases "f w = 0") + case False + thus ?thesis using w + by (intro analytic_intros analytic_on_subset[OF ana]) auto + next + case True + have "eventually (\w. f w = 0) (nhds w)" + using True w by (intro non_isolated_zero analytic_on_subset[OF ana]) auto + hence "(\z. inverse (f z)) analytic_on {w} \ (\_. 0) analytic_on {w}" + using w by (intro analytic_at_cong refl) auto + thus ?thesis + by simp + qed + qed + also have "\ = A - (pts \ {z \ A. isolated_zero f z})" + by blast + finally have "(\z. inverse (f z)) analytic_on \" . + moreover have "open (A - (pts \ {z \ A. isolated_zero f z}))" + using closedin_isolated_zeros[OF mero] open' \open A\ + by (metis (no_types, lifting) Diff_Diff_Int Diff_Un closedin_closed open_Diff open_Int) + ultimately show "(\z. inverse (f z)) holomorphic_on A - (pts \ {z \ A. isolated_zero f z})" + by (subst (asm) analytic_on_open) auto + qed (use assms in \auto simp: meromorphic_on_def islimpt_Un + intro!: holomorphic_intros singularity_intros\) +qed + +lemma meromorphic_on_inverse'' [meromorphic_intros]: + assumes "f meromorphic_on A pts" "{z\A. f z = 0} \ pts" + shows "(\z. inverse (f z)) meromorphic_on A pts" +proof - + have "(\z. inverse (f z)) meromorphic_on A (pts \ {z \ A. isolated_zero f z})" + by (intro meromorphic_on_inverse assms) + also have "(pts \ {z \ A. isolated_zero f z}) = pts" + using assms(2) by (auto simp: isolated_zero_def) + finally show ?thesis . +qed + +lemma meromorphic_on_divide [meromorphic_intros]: + assumes "f meromorphic_on A pts" and "g meromorphic_on A pts" + shows "(\z. f z / g z) meromorphic_on A (pts \ {z\A. isolated_zero g z})" +proof - + have mero1: "(\z. inverse (g z)) meromorphic_on A (pts \ {z\A. isolated_zero g z})" + by (intro meromorphic_intros assms) + have sparse: "\x\A. \ x islimpt pts \ {z\A. isolated_zero g z}" and "pts \ A" + using mero1 by (auto simp: meromorphic_on_def) + have mero2: "f meromorphic_on A (pts \ {z\A. isolated_zero g z})" + by (rule meromorphic_on_superset_pts[OF assms(1)]) (use sparse \pts \ A\ in auto) + have "(\z. f z * inverse (g z)) meromorphic_on A (pts \ {z\A. isolated_zero g z})" + by (intro meromorphic_on_mult mero1 mero2) + thus ?thesis + by (simp add: field_simps) +qed + +lemma meromorphic_on_divide' [meromorphic_intros]: + assumes "f meromorphic_on A pts" "g meromorphic_on A pts" "{z\A. g z = 0} \ pts" + shows "(\z. f z / g z) meromorphic_on A pts" +proof - + have "(\z. f z * inverse (g z)) meromorphic_on A pts" + by (intro meromorphic_intros assms) + thus ?thesis + by (simp add: field_simps) +qed + +lemma meromorphic_on_cmult_left [meromorphic_intros]: + assumes "f meromorphic_on A pts" + shows "(\x. c * f x) meromorphic_on A pts" + using assms by (intro meromorphic_intros) (auto simp: meromorphic_on_def) + +lemma meromorphic_on_cmult_right [meromorphic_intros]: + assumes "f meromorphic_on A pts" + shows "(\x. f x * c) meromorphic_on A pts" + using assms by (intro meromorphic_intros) (auto simp: meromorphic_on_def) + +lemma meromorphic_on_scaleR [meromorphic_intros]: + assumes "f meromorphic_on A pts" + shows "(\x. c *\<^sub>R f x) meromorphic_on A pts" + using assms unfolding scaleR_conv_of_real + by (intro meromorphic_intros) (auto simp: meromorphic_on_def) + +lemma meromorphic_on_sum [meromorphic_intros]: + assumes "\y. y \ I \ f y meromorphic_on A pts" + assumes "I \ {} \ open A \ pts \ A \ (\x\A. \x islimpt pts)" + shows "(\x. \y\I. f y x) meromorphic_on A pts" +proof - + have *: "open A \ pts \ A \ (\x\A. \x islimpt pts)" + using assms(2) + proof + assume "I \ {}" + then obtain x where "x \ I" + by blast + from assms(1)[OF this] show ?thesis + by (auto simp: meromorphic_on_def) + qed auto + show ?thesis + using assms(1) + by (induction I rule: infinite_finite_induct) (use * in \auto intro!: meromorphic_intros\) +qed + +lemma meromorphic_on_prod [meromorphic_intros]: + assumes "\y. y \ I \ f y meromorphic_on A pts" + assumes "I \ {} \ open A \ pts \ A \ (\x\A. \x islimpt pts)" + shows "(\x. \y\I. f y x) meromorphic_on A pts" +proof - + have *: "open A \ pts \ A \ (\x\A. \x islimpt pts)" + using assms(2) + proof + assume "I \ {}" + then obtain x where "x \ I" + by blast + from assms(1)[OF this] show ?thesis + by (auto simp: meromorphic_on_def) + qed auto + show ?thesis + using assms(1) + by (induction I rule: infinite_finite_induct) (use * in \auto intro!: meromorphic_intros\) +qed + +lemma meromorphic_on_power [meromorphic_intros]: + assumes "f meromorphic_on A pts" + shows "(\x. f x ^ n) meromorphic_on A pts" +proof - + have "(\x. \i\{..auto simp: meromorphic_on_def\) + thus ?thesis + by simp +qed + +lemma meromorphic_on_power_int [meromorphic_intros]: + assumes "f meromorphic_on A pts" + shows "(\z. f z powi n) meromorphic_on A (pts \ {z \ A. isolated_zero f z})" +proof - + have inv: "(\x. inverse (f x)) meromorphic_on A (pts \ {z \ A. isolated_zero f z})" + by (intro meromorphic_intros assms) + have *: "f meromorphic_on A (pts \ {z \ A. isolated_zero f z})" + by (intro meromorphic_on_superset_pts [OF assms(1)]) + (use inv in \auto simp: meromorphic_on_def\) + show ?thesis + proof (cases "n \ 0") + case True + have "(\x. f x ^ nat n) meromorphic_on A (pts \ {z \ A. isolated_zero f z})" + by (intro meromorphic_intros *) + thus ?thesis + using True by (simp add: power_int_def) + next + case False + have "(\x. inverse (f x) ^ nat (-n)) meromorphic_on A (pts \ {z \ A. isolated_zero f z})" + by (intro meromorphic_intros assms) + thus ?thesis + using False by (simp add: power_int_def) + qed +qed + +lemma meromorphic_on_power_int' [meromorphic_intros]: + assumes "f meromorphic_on A pts" "n \ 0 \ (\z\A. isolated_zero f z \ z \ pts)" + shows "(\z. f z powi n) meromorphic_on A pts" +proof (cases "n \ 0") + case True + have "(\z. f z ^ nat n) meromorphic_on A pts" + by (intro meromorphic_intros assms) + thus ?thesis + using True by (simp add: power_int_def) +next + case False + have "(\z. f z powi n) meromorphic_on A (pts \ {z\A. isolated_zero f z})" + by (rule meromorphic_on_power_int) fact + also from assms(2) False have "pts \ {z\A. isolated_zero f z} = pts" + by auto + finally show ?thesis . +qed + +lemma has_laurent_expansion_on_imp_meromorphic_on: + assumes "open A" + assumes laurent: "\z. z \ A \ \F. (\w. f (z + w)) has_laurent_expansion F" + shows "f meromorphic_on A {z\A. \f analytic_on {z}}" + unfolding meromorphic_on_def +proof (intro conjI ballI) + fix z assume "z \ {z\A. \f analytic_on {z}}" + then obtain F where F: "(\w. f (z + w)) has_laurent_expansion F" + using laurent[of z] by blast + from F show "not_essential f z" "isolated_singularity_at f z" + using has_laurent_expansion_not_essential has_laurent_expansion_isolated by blast+ +next + fix z assume z: "z \ A" + obtain F where F: "(\w. f (z + w)) has_laurent_expansion F" + using laurent[of z] \z \ A\ by blast + from F have "isolated_singularity_at f z" + using has_laurent_expansion_isolated z by blast + then obtain r where r: "r > 0" "f analytic_on ball z r - {z}" + unfolding isolated_singularity_at_def by blast + have "f analytic_on {w}" if "w \ ball z r - {z}" for w + by (rule analytic_on_subset[OF r(2)]) (use that in auto) + hence "eventually (\w. f analytic_on {w}) (at z)" + using eventually_at_in_open[of "ball z r" z] \r > 0\ by (auto elim!: eventually_mono) + hence "\z islimpt {w. \f analytic_on {w}}" + by (auto simp: islimpt_conv_frequently_at frequently_def) + thus "\z islimpt {w\A. \f analytic_on {w}}" + using islimpt_subset[of z "{w\A. \f analytic_on {w}}" "{w. \f analytic_on {w}}"] by blast +next + have "f analytic_on A - {w\A. \f analytic_on {w}}" + by (subst analytic_on_analytic_at) auto + thus "f holomorphic_on A - {w\A. \f analytic_on {w}}" + by (meson analytic_imp_holomorphic) +qed (use assms in auto) + +lemma meromorphic_on_imp_has_laurent_expansion: + assumes "f meromorphic_on A pts" "z \ A" + shows "(\w. f (z + w)) has_laurent_expansion laurent_expansion f z" +proof (cases "z \ pts") + case True + thus ?thesis + using assms by (intro not_essential_has_laurent_expansion) (auto simp: meromorphic_on_def) +next + case False + have "f holomorphic_on (A - pts)" + using assms by (auto simp: meromorphic_on_def) + moreover have "z \ A - pts" "open (A - pts)" + using assms(2) False by (auto intro!: meromorphic_imp_open_diff[OF assms(1)]) + ultimately have "f analytic_on {z}" + unfolding analytic_at by blast + thus ?thesis + using isolated_singularity_at_analytic not_essential_analytic + not_essential_has_laurent_expansion by blast +qed + +lemma + assumes "isolated_singularity_at f z" "f \z\ c" + shows eventually_remove_sings_eq_nhds': + "eventually (\w. remove_sings f w = (if w = z then c else f w)) (nhds z)" + and remove_sings_analytic_at_singularity: "remove_sings f analytic_on {z}" +proof - + have "eventually (\w. w \ z) (at z)" + by (auto simp: eventually_at_filter) + hence "eventually (\w. remove_sings f w = (if w = z then c else f w)) (at z)" + using eventually_remove_sings_eq_at[OF assms(1)] + by eventually_elim auto + moreover have "remove_sings f z = c" + using assms by auto + ultimately show ev: "eventually (\w. remove_sings f w = (if w = z then c else f w)) (nhds z)" + by (simp add: eventually_at_filter) + + have "(\w. if w = z then c else f w) analytic_on {z}" + by (intro removable_singularity' assms) + also have "?this \ remove_sings f analytic_on {z}" + using ev by (intro analytic_at_cong) (auto simp: eq_commute) + finally show \ . +qed + +lemma remove_sings_meromorphic_on: + assumes "f meromorphic_on A pts" "\z. z \ pts - pts' \ \is_pole f z" "pts' \ pts" + shows "remove_sings f meromorphic_on A pts'" + unfolding meromorphic_on_def +proof safe + have "remove_sings f analytic_on {z}" if "z \ A - pts'" for z + proof (cases "z \ pts") + case False + hence *: "f analytic_on {z}" + using assms meromorphic_imp_open_diff[OF assms(1)] that + by (force simp: meromorphic_on_def analytic_at) + have "remove_sings f analytic_on {z} \ f analytic_on {z}" + by (intro analytic_at_cong eventually_remove_sings_eq_nhds * refl) + thus ?thesis using * by simp + next + case True + have isol: "isolated_singularity_at f z" + using True using assms by (auto simp: meromorphic_on_def) + from assms(1) have "not_essential f z" + using True by (auto simp: meromorphic_on_def) + with assms(2) True that obtain c where "f \z\ c" + by (auto simp: not_essential_def) + thus "remove_sings f analytic_on {z}" + by (intro remove_sings_analytic_at_singularity isol) + qed + hence "remove_sings f analytic_on A - pts'" + by (subst analytic_on_analytic_at) auto + thus "remove_sings f holomorphic_on A - pts'" + using meromorphic_imp_open_diff'[OF assms(1,3)] by (subst (asm) analytic_on_open) +qed (use assms islimpt_subset[OF _ assms(3)] in \auto simp: meromorphic_on_def\) + +lemma remove_sings_holomorphic_on: + assumes "f meromorphic_on A pts" "\z. z \ pts \ \is_pole f z" + shows "remove_sings f holomorphic_on A" + using remove_sings_meromorphic_on[OF assms(1), of "{}"] assms(2) + by (auto simp: meromorphic_on_no_singularities) + +lemma meromorphic_on_Ex_iff: + "(\pts. f meromorphic_on A pts) \ + open A \ (\z\A. \F. (\w. f (z + w)) has_laurent_expansion F)" +proof safe + fix pts assume *: "f meromorphic_on A pts" + from * show "open A" + by (auto simp: meromorphic_on_def) + show "\F. (\w. f (z + w)) has_laurent_expansion F" if "z \ A" for z + using that * + by (intro exI[of _ "laurent_expansion f z"] meromorphic_on_imp_has_laurent_expansion) +qed (blast intro!: has_laurent_expansion_on_imp_meromorphic_on) + +lemma is_pole_inverse_holomorphic_pts: + fixes pts::"complex set" and f::"complex \ complex" + defines "g \ \x. (if x\pts then 0 else inverse (f x))" + assumes mer: "f meromorphic_on D pts" + and non_z: "\z. z \ D - pts \ f z \ 0" + and all_poles:"\x. is_pole f x \ x\pts" + shows "g holomorphic_on D" +proof - + have "open D" and f_holo: "f holomorphic_on (D-pts)" + using mer by (auto simp: meromorphic_on_def) + have "\r. r>0 \ f analytic_on ball z r - {z} + \ (\x \ ball z r - {z}. f x\0)" if "z\pts" for z + proof - + have "isolated_singularity_at f z" "is_pole f z" + using mer meromorphic_on_def that all_poles by blast+ + then obtain r1 where "r1>0" and fan: "f analytic_on ball z r1 - {z}" + by (meson isolated_singularity_at_def) + obtain r2 where "r2>0" "\x \ ball z r2 - {z}. f x\0" + using non_zero_neighbour_pole[OF \is_pole f z\] + unfolding eventually_at by (metis Diff_iff UNIV_I dist_commute insertI1 mem_ball) + define r where "r = min r1 r2" + have "r>0" by (simp add: \0 < r2\ \r1>0\ r_def) + moreover have "f analytic_on ball z r - {z}" + using r_def by (force intro: analytic_on_subset [OF fan]) + moreover have "\x \ ball z r - {z}. f x\0" + by (simp add: \\x\ball z r2 - {z}. f x \ 0\ r_def) + ultimately show ?thesis by auto + qed + then obtain get_r where r_pos:"get_r z>0" + and r_ana:"f analytic_on ball z (get_r z) - {z}" + and r_nz:"\x \ ball z (get_r z) - {z}. f x\0" + if "z\pts" for z + by metis + define p_balls where "p_balls \ \z\pts. ball z (get_r z)" + have g_ball:"g holomorphic_on ball z (get_r z)" if "z\pts" for z + proof - + have "(\x. if x = z then 0 else inverse (f x)) holomorphic_on ball z (get_r z)" + proof (rule is_pole_inverse_holomorphic) + show "f holomorphic_on ball z (get_r z) - {z}" + using analytic_imp_holomorphic r_ana that by blast + show "is_pole f z" + using mer meromorphic_on_def that all_poles by force + show "\x\ball z (get_r z) - {z}. f x \ 0" + using r_nz that by metis + qed auto + then show ?thesis unfolding g_def + by (smt (verit, ccfv_SIG) Diff_iff Elementary_Metric_Spaces.open_ball + all_poles analytic_imp_holomorphic empty_iff + holomorphic_transform insert_iff not_is_pole_holomorphic + open_delete r_ana that) + qed + then have "g holomorphic_on p_balls" + proof - + have "g analytic_on p_balls" + unfolding p_balls_def analytic_on_UN + using g_ball by (simp add: analytic_on_open) + moreover have "open p_balls" using p_balls_def by blast + ultimately show ?thesis + by (simp add: analytic_imp_holomorphic) + qed + moreover have "g holomorphic_on D-pts" + proof - + have "(\z. inverse (f z)) holomorphic_on D - pts" + using f_holo holomorphic_on_inverse non_z by blast + then show ?thesis + by (metis DiffD2 g_def holomorphic_transform) + qed + moreover have "open p_balls" + using p_balls_def by blast + ultimately have "g holomorphic_on (p_balls \ (D-pts))" + by (simp add: holomorphic_on_Un meromorphic_imp_open_diff[OF mer]) + moreover have "D \ p_balls \ (D-pts)" + unfolding p_balls_def using \\z. z \ pts \ 0 < get_r z\ by force + ultimately show "g holomorphic_on D" by (meson holomorphic_on_subset) +qed + +lemma meromorphic_imp_analytic_on: + assumes "f meromorphic_on D pts" + shows "f analytic_on (D - pts)" + by (metis assms analytic_on_open meromorphic_imp_open_diff meromorphic_on_def) + +lemma meromorphic_imp_constant_on: + assumes merf: "f meromorphic_on D pts" + and "f constant_on (D - pts)" + and "\x\pts. is_pole f x" + shows "f constant_on D" +proof - + obtain c where c:"\z. z \ D-pts \ f z = c" + by (meson assms constant_on_def) + + have "f z = c" if "z \ D" for z + proof (cases "is_pole f z") + case True + then obtain r0 where "r0 > 0" and r0: "f analytic_on ball z r0 - {z}" and pol: "is_pole f z" + using merf unfolding meromorphic_on_def isolated_singularity_at_def + by (metis \z \ D\ insert_Diff insert_Diff_if insert_iff merf + meromorphic_imp_open_diff not_is_pole_holomorphic) + have "open D" + using merf meromorphic_on_def by auto + then obtain r where "r > 0" "ball z r \ D" "r \ r0" + by (smt (verit, best) \0 < r0\ \z \ D\ openE order_subst2 subset_ball) + have r: "f analytic_on ball z r - {z}" + by (meson Diff_mono \r \ r0\ analytic_on_subset order_refl r0 subset_ball) + have "ball z r - {z} \ -pts" + using merf r unfolding meromorphic_on_def + by (meson ComplI Elementary_Metric_Spaces.open_ball + analytic_imp_holomorphic assms(3) not_is_pole_holomorphic open_delete subsetI) + with \ball z r \ D\ have "ball z r - {z} \ D-pts" + by fastforce + with c have c': "\u. u \ ball z r - {z} \ f u = c" + by blast + have False if "\\<^sub>F x in at z. cmod c + 1 \ cmod (f x)" + proof - + have "\\<^sub>F x in at z within ball z r - {z}. cmod c + 1 \ cmod (f x)" + by (smt (verit, best) Diff_UNIV Diff_eq_empty_iff eventually_at_topological insert_subset that) + with \r > 0\ show ?thesis + apply (simp add: c' eventually_at_filter topological_space_class.eventually_nhds open_dist) + by (metis dist_commute min_less_iff_conj perfect_choose_dist) + qed + with pol show ?thesis + by (auto simp: is_pole_def filterlim_at_infinity_conv_norm_at_top filterlim_at_top) + next + case False + then show ?thesis by (meson DiffI assms(3) c that) + qed + then show ?thesis + by (simp add: constant_on_def) +qed + + +lemma meromorphic_isolated: + assumes merf: "f meromorphic_on D pts" and "p\pts" + obtains r where "r>0" "ball p r \ D" "ball p r \ pts = {p}" +proof - + have "\z\D. \e>0. finite (pts \ ball z e)" + using merf unfolding meromorphic_on_def islimpt_eq_infinite_ball + by auto + then obtain r0 where r0:"r0>0" "finite (pts \ ball p r0)" + by (metis assms(2) in_mono merf meromorphic_on_def) + moreover define pts' where "pts' = pts \ ball p r0 - {p}" + ultimately have "finite pts'" + by simp + + define r1 where "r1=(if pts'={} then r0 else + min (Min {dist p' p |p'. p'\pts'}/2) r0)" + have "r1>0 \ pts \ ball p r1 - {p} = {}" + proof (cases "pts'={}") + case True + then show ?thesis + using pts'_def r0(1) r1_def by presburger + next + case False + define S where "S={dist p' p |p'. p'\pts'}" + + have nempty:"S \ {}" + using False S_def by blast + have finite:"finite S" + using \finite pts'\ S_def by simp + + have "r1>0" + proof - + have "r1=min (Min S/2) r0" + using False unfolding S_def r1_def by auto + moreover have "Min S\S" + using \S\{}\ \finite S\ Min_in by auto + then have "Min S>0" unfolding S_def + using pts'_def by force + ultimately show ?thesis using \r0>0\ by auto + qed + moreover have "pts \ ball p r1 - {p} = {}" + proof (rule ccontr) + assume "pts \ ball p r1 - {p} \ {}" + then obtain p' where "p'\pts \ ball p r1 - {p}" by blast + moreover have "r1\r0" using r1_def by auto + ultimately have "p'\pts'" unfolding pts'_def + by auto + then have "dist p' p\Min S" + using S_def eq_Min_iff local.finite by blast + moreover have "dist p' p < Min S" + using \p'\pts \ ball p r1 - {p}\ False unfolding r1_def + apply (fold S_def) + by (smt (verit, ccfv_threshold) DiffD1 Int_iff dist_commute + dist_triangle_half_l mem_ball) + ultimately show False by auto + qed + ultimately show ?thesis by auto + qed + then have "r1>0" and r1_pts:"pts \ ball p r1 - {p} = {}" by auto + + obtain r2 where "r2>0" "ball p r2 \ D" + by (metis assms(2) merf meromorphic_on_def openE subset_eq) + define r where "r=min r1 r2" + have "r > 0" unfolding r_def + by (simp add: \0 < r1\ \0 < r2\) + moreover have "ball p r \ D" + using \ball p r2 \ D\ r_def by auto + moreover have "ball p r \ pts = {p}" + using assms(2) \r>0\ r1_pts + unfolding r_def by auto + ultimately show ?thesis using that by auto +qed + +lemma meromorphic_pts_closure: + assumes merf: "f meromorphic_on D pts" + shows "pts \ closure (D - pts)" +proof - + have "p islimpt (D - pts)" if "p\pts" for p + proof - + obtain r where "r>0" "ball p r \ D" "ball p r \ pts = {p}" + using meromorphic_isolated[OF merf \p\pts\] by auto + from \r>0\ + have "p islimpt ball p r - {p}" + by (meson open_ball ball_subset_cball in_mono islimpt_ball + islimpt_punctured le_less open_contains_ball_eq) + moreover have " ball p r - {p} \ D - pts" + using \ball p r \ pts = {p}\ \ball p r \ D\ by fastforce + ultimately show ?thesis + using islimpt_subset by auto + qed + then show ?thesis by (simp add: islimpt_in_closure subset_eq) +qed + +lemma nconst_imp_nzero_neighbour: + assumes merf: "f meromorphic_on D pts" + and f_nconst:"\(\w\D-pts. f w=0)" + and "z\D" and "connected D" + shows "(\\<^sub>F w in at z. f w \ 0 \ w \ D - pts)" +proof - + obtain \ where \:"\ \ D - pts" "f \\0" + using f_nconst by auto + + have ?thesis if "z\pts" + proof - + have "\\<^sub>F w in at z. f w \ 0 \ w \ D - pts" + apply (rule non_zero_neighbour_alt[of f "D-pts" z \]) + subgoal using merf meromorphic_on_def by blast + subgoal using merf meromorphic_imp_open_diff by auto + subgoal using assms(4) merf meromorphic_imp_connected_diff by blast + subgoal by (simp add: assms(3) that) + using \ by auto + then show ?thesis by (auto elim:eventually_mono) + qed + moreover have ?thesis if "z\pts" "\ f \z\ 0" + proof - + have "\\<^sub>F w in at z. w \ D - pts" + using merf[unfolded meromorphic_on_def islimpt_iff_eventually] \z\D\ + using eventually_at_in_open' eventually_elim2 by fastforce + moreover have "\\<^sub>F w in at z. f w \ 0" + proof (cases "is_pole f z") + case True + then show ?thesis using non_zero_neighbour_pole by auto + next + case False + moreover have "not_essential f z" + using merf meromorphic_on_def that(1) by fastforce + ultimately obtain c where "c\0" "f \z\ c" + by (metis \\ f \z\ 0\ not_essential_def) + then show ?thesis + using tendsto_imp_eventually_ne by auto + qed + ultimately show ?thesis by eventually_elim auto + qed + moreover have ?thesis if "z\pts" "f \z\ 0" + proof - + define ff where "ff=(\x. if x=z then 0 else f x)" + define A where "A=D - (pts - {z})" + + have "f holomorphic_on A - {z}" + by (metis A_def Diff_insert analytic_imp_holomorphic + insert_Diff merf meromorphic_imp_analytic_on that(1)) + moreover have "open A" + using A_def merf meromorphic_imp_open_diff' by force + ultimately have "ff holomorphic_on A" + using \f \z\ 0\ unfolding ff_def + by (rule removable_singularity) + moreover have "connected A" + proof - + have "connected (D - pts)" + using assms(4) merf meromorphic_imp_connected_diff by auto + moreover have "D - pts \ A" + unfolding A_def by auto + moreover have "A \ closure (D - pts)" unfolding A_def + by (smt (verit, ccfv_SIG) Diff_empty Diff_insert + closure_subset insert_Diff_single insert_absorb + insert_subset merf meromorphic_pts_closure that(1)) + ultimately show ?thesis using connected_intermediate_closure + by auto + qed + moreover have "z \ A" using A_def assms(3) by blast + moreover have "ff z = 0" unfolding ff_def by auto + moreover have "\ \ A " using A_def \(1) by blast + moreover have "ff \ \ 0" using \(1) \(2) ff_def that(1) by auto + ultimately obtain r where "0 < r" + "ball z r \ A" "\x. x \ ball z r - {z} \ ff x \ 0" + using \open A\ isolated_zeros[of ff A z \] by auto + then show ?thesis unfolding eventually_at ff_def + by (intro exI[of _ r]) (auto simp: A_def dist_commute ball_def) + qed + ultimately show ?thesis by auto +qed + +lemma nconst_imp_nzero_neighbour': + assumes merf: "f meromorphic_on D pts" + and f_nconst:"\(\w\D-pts. f w=0)" + and "z\D" and "connected D" + shows "\\<^sub>F w in at z. f w \ 0" + using nconst_imp_nzero_neighbour[OF assms] + by (auto elim:eventually_mono) + +lemma meromorphic_compact_finite_zeros: + assumes merf:"f meromorphic_on D pts" + and "compact S" "S \ D" "connected D" + and f_nconst:"\(\w\D-pts. f w=0)" + shows "finite ({x\S. f x=0})" +proof - + have "finite ({x\S. f x=0 \ x \ pts})" + proof (rule ccontr) + assume "infinite {x \ S. f x = 0 \ x \ pts}" + then obtain z where "z\S" and z_lim:"z islimpt {x \ S. f x = 0 + \ x \ pts}" + using \compact S\ unfolding compact_eq_Bolzano_Weierstrass + by auto + + from z_lim + have "\\<^sub>F x in at z. f x = 0 \ x \ S \ x \ pts" + unfolding islimpt_iff_eventually not_eventually by simp + moreover have "\\<^sub>F w in at z. f w \ 0 \ w \ D - pts" + using nconst_imp_nzero_neighbour[OF merf f_nconst _ \connected D\] + \z\S\ \S \ D\ + by auto + ultimately have "\\<^sub>F x in at z. False" + by (simp add: eventually_mono frequently_def) + then show False by auto + qed + moreover have "finite (S \ pts)" + using meromorphic_compact_finite_pts[OF merf \compact S\ \S \ D\] . + ultimately have "finite ({x\S. f x=0 \ x \ pts} \ (S \ pts))" + unfolding finite_Un by auto + then show ?thesis by (elim rev_finite_subset) auto +qed + +lemma meromorphic_onI [intro?]: + assumes "open A" "pts \ A" + assumes "f holomorphic_on A - pts" "\z. z \ A \ \z islimpt pts" + assumes "\z. z \ pts \ isolated_singularity_at f z" + assumes "\z. z \ pts \ not_essential f z" + shows "f meromorphic_on A pts" + using assms unfolding meromorphic_on_def by blast + +lemma Polygamma_plus_of_nat: + assumes "\k -of_nat k" + shows "Polygamma n (z + of_nat m) = + Polygamma n z + (-1) ^ n * fact n * (\k = Polygamma n (z + of_nat m) + (-1) ^ n * fact n * (1 / ((z + of_nat m) ^ Suc n))" + using Suc.prems by (subst Polygamma_plus1) (auto simp: add_eq_0_iff2) + also have "Polygamma n (z + of_nat m) = + Polygamma n z + (-1) ^ n * (\k c) F" "c \ \\<^sub>\\<^sub>0" + shows "((\z. Gamma (f z)) \ Gamma c) F" + by (intro isCont_tendsto_compose[OF _ assms(1)] continuous_intros assms) + +lemma tendsto_Polygamma [tendsto_intros]: + fixes f :: "_ \ 'a :: {real_normed_field,euclidean_space}" + assumes "(f \ c) F" "c \ \\<^sub>\\<^sub>0" + shows "((\z. Polygamma n (f z)) \ Polygamma n c) F" + by (intro isCont_tendsto_compose[OF _ assms(1)] continuous_intros assms) + +lemma analytic_on_Gamma' [analytic_intros]: + assumes "f analytic_on A" "\x\A. f x \ \\<^sub>\\<^sub>0" + shows "(\z. Gamma (f z)) analytic_on A" + using analytic_on_compose_gen[OF assms(1) analytic_Gamma[of "f ` A"]] assms(2) + by (auto simp: o_def) + +lemma analytic_on_Polygamma' [analytic_intros]: + assumes "f analytic_on A" "\x\A. f x \ \\<^sub>\\<^sub>0" + shows "(\z. Polygamma n (f z)) analytic_on A" + using analytic_on_compose_gen[OF assms(1) analytic_on_Polygamma[of "f ` A" n]] assms(2) + by (auto simp: o_def) + +lemma + shows is_pole_Polygamma: "is_pole (Polygamma n) (-of_nat m :: complex)" + and zorder_Polygamma: "zorder (Polygamma n) (-of_nat m) = -int (Suc n)" + and residue_Polygamma: "residue (Polygamma n) (-of_nat m) = (if n = 0 then -1 else 0)" +proof - + define g1 :: "complex \ complex" where + "g1 = (\z. Polygamma n (z + of_nat (Suc m)) + + (-1) ^ Suc n * fact n * (\k complex" where + "g = (\z. g1 z + (-1) ^ Suc n * fact n / (z + of_nat m) ^ Suc n)" + define F where "F = fps_to_fls (fps_expansion g1 (-of_nat m)) + fls_const ((-1) ^ Suc n * fact n) / fls_X ^ Suc n" + have F_altdef: "F = fps_to_fls (fps_expansion g1 (-of_nat m)) + fls_shift (n+1) (fls_const ((-1) ^ Suc n * fact n))" + by (simp add: F_def del: power_Suc) + + have "\(-of_nat m) islimpt (\\<^sub>\\<^sub>0 :: complex set)" + by (intro discrete_imp_not_islimpt[where e = 1]) + (auto elim!: nonpos_Ints_cases simp: dist_of_int) + hence "eventually (\z::complex. z \ \\<^sub>\\<^sub>0) (at (-of_nat m))" + by (auto simp: islimpt_conv_frequently_at frequently_def) + hence ev: "eventually (\z. Polygamma n z = g z) (at (-of_nat m))" + proof eventually_elim + case (elim z) + hence *: "\k - of_nat k" + by auto + thus ?case + using Polygamma_plus_of_nat[of "Suc m" z n, OF *] + by (auto simp: g_def g1_def algebra_simps) + qed + + have "(\w. g (-of_nat m + w)) has_laurent_expansion F" + unfolding g_def F_def + by (intro laurent_expansion_intros has_laurent_expansion_fps analytic_at_imp_has_fps_expansion) + (auto simp: g1_def intro!: laurent_expansion_intros analytic_intros) + also have "?this \ (\w. Polygamma n (-of_nat m + w)) has_laurent_expansion F" + using ev by (intro has_laurent_expansion_cong refl) + (simp_all add: eq_commute at_to_0' eventually_filtermap) + finally have *: "(\w. Polygamma n (-of_nat m + w)) has_laurent_expansion F" . + + have subdegree: "fls_subdegree F = -int (Suc n)" unfolding F_def + by (subst fls_subdegree_add_eq2) (simp_all add: fls_subdegree_fls_to_fps fls_divide_subdegree) + have [simp]: "F \ 0" + using subdegree by auto + + show "is_pole (Polygamma n) (-of_nat m :: complex)" + using * by (rule has_laurent_expansion_imp_is_pole) (auto simp: subdegree) + show "zorder (Polygamma n) (-of_nat m :: complex) = -int (Suc n)" + by (subst has_laurent_expansion_zorder[OF *]) (auto simp: subdegree) + show "residue (Polygamma n) (-of_nat m :: complex) = (if n = 0 then -1 else 0)" + by (subst has_laurent_expansion_residue[OF *]) (auto simp: F_altdef) +qed + +lemma Gamma_meromorphic_on [meromorphic_intros]: "Gamma meromorphic_on UNIV \\<^sub>\\<^sub>0" +proof + show "\z islimpt \\<^sub>\\<^sub>0" for z :: complex + by (intro discrete_imp_not_islimpt[of 1]) (auto elim!: nonpos_Ints_cases simp: dist_of_int) +next + fix z :: complex assume z: "z \ \\<^sub>\\<^sub>0" + then obtain n where n: "z = -of_nat n" + by (elim nonpos_Ints_cases') + show "not_essential Gamma z" + by (auto simp: n intro!: is_pole_imp_not_essential is_pole_Gamma) + have *: "open (-(\\<^sub>\\<^sub>0 - {z}))" + by (intro open_Compl discrete_imp_closed[of 1]) (auto elim!: nonpos_Ints_cases simp: dist_of_int) + have "Gamma holomorphic_on -(\\<^sub>\\<^sub>0 - {z}) - {z}" + by (intro holomorphic_intros) auto + thus "isolated_singularity_at Gamma z" + by (rule isolated_singularity_at_holomorphic) (use z * in auto) +qed (auto intro!: holomorphic_intros) + +lemma Polygamma_meromorphic_on [meromorphic_intros]: "Polygamma n meromorphic_on UNIV \\<^sub>\\<^sub>0" +proof + show "\z islimpt \\<^sub>\\<^sub>0" for z :: complex + by (intro discrete_imp_not_islimpt[of 1]) (auto elim!: nonpos_Ints_cases simp: dist_of_int) +next + fix z :: complex assume z: "z \ \\<^sub>\\<^sub>0" + then obtain m where n: "z = -of_nat m" + by (elim nonpos_Ints_cases') + show "not_essential (Polygamma n) z" + by (auto simp: n intro!: is_pole_imp_not_essential is_pole_Polygamma) + have *: "open (-(\\<^sub>\\<^sub>0 - {z}))" + by (intro open_Compl discrete_imp_closed[of 1]) (auto elim!: nonpos_Ints_cases simp: dist_of_int) + have "Polygamma n holomorphic_on -(\\<^sub>\\<^sub>0 - {z}) - {z}" + by (intro holomorphic_intros) auto + thus "isolated_singularity_at (Polygamma n) z" + by (rule isolated_singularity_at_holomorphic) (use z * in auto) +qed (auto intro!: holomorphic_intros) + + +theorem argument_principle': + fixes f::"complex \ complex" and poles s:: "complex set" + \ \\<^term>\pz\ is the set of non-essential singularities and zeros\ + defines "pz \ {w\s. f w = 0 \ w \ poles}" + assumes "open s" 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 - pz" and + homo:"\z. (z \ s) \ winding_number g z = 0" and + finite:"finite pz" and + poles:"\p\s\poles. not_essential f p" + shows "contour_integral g (\x. deriv f x * h x / f x) = 2 * pi * \ * + (\p\pz. winding_number g p * h p * zorder f p)" +proof - + define ff where "ff = remove_sings f" + + have finite':"finite (s \ poles)" + using finite unfolding pz_def by (auto elim:rev_finite_subset) + + have isolated:"isolated_singularity_at f z" if "z\s" for z + proof (rule isolated_singularity_at_holomorphic) + show "f holomorphic_on (s-(poles-{z})) - {z}" + by (metis Diff_empty Diff_insert Diff_insert0 Diff_subset + f_holo holomorphic_on_subset insert_Diff) + show "open (s - (poles - {z}))" + by (metis Diff_Diff_Int Int_Diff assms(2) finite' finite_Diff + finite_imp_closed inf.idem open_Diff) + show "z \ s - (poles - {z})" + using assms(4) that by auto + qed + + have not_ess:"not_essential f w" if "w\s" for w + by (metis Diff_Diff_Int Diff_iff Int_Diff Int_absorb assms(2) + f_holo finite' finite_imp_closed not_essential_holomorphic + open_Diff poles that) + + have nzero:"\\<^sub>F x in at w. f x \ 0" if "w\s" for w + proof (rule ccontr) + assume "\ (\\<^sub>F x in at w. f x \ 0)" + then have "\\<^sub>F x in at w. f x = 0" + unfolding not_eventually by simp + moreover have "\\<^sub>F x in at w. x\s" + by (simp add: assms(2) eventually_at_in_open' that) + ultimately have "\\<^sub>F x in at w. x\{w\s. f w = 0}" + apply (elim frequently_rev_mp) + by (auto elim:eventually_mono) + from frequently_at_imp_islimpt[OF this] + have "w islimpt {w \ s. f w = 0}" . + then have "infinite({w \ s. f w = 0} \ ball w 1)" + unfolding islimpt_eq_infinite_ball by auto + then have "infinite({w \ s. f w = 0})" + by auto + then have "infinite pz" unfolding pz_def + by (smt (verit) Collect_mono_iff rev_finite_subset) + then show False using finite by auto + qed + + obtain pts' where pts':"pts' \ s \ poles" + "finite pts'" "ff holomorphic_on s - pts'" "\x\pts'. is_pole ff x" + apply (elim get_all_poles_from_remove_sings + [of f,folded ff_def,rotated -1]) + subgoal using f_holo by fastforce + using \open s\ poles finite' by auto + + have pts'_sub_pz:"{w \ s. ff w = 0 \ w \ pts'} \ pz" + proof - + have "w\poles" if "w\s" "w\pts'" for w + by (meson in_mono le_infE pts'(1) that(2)) + moreover have "f w=0" if" w\s" "w\poles" "ff w=0" for w + proof - + have "\ is_pole f w" + by (metis DiffI Diff_Diff_Int Diff_subset assms(2) f_holo + finite' finite_imp_closed inf.absorb_iff2 + not_is_pole_holomorphic open_Diff that(1) that(2)) + then have "f \w\ 0" + using remove_sings_eq_0_iff[OF not_ess[OF \w\s\]] \ff w=0\ + unfolding ff_def by auto + moreover have "f analytic_on {w}" + using that(1,2) finite' f_holo assms(2) + by (metis Diff_Diff_Int Diff_empty Diff_iff Diff_subset + double_diff finite_imp_closed + holomorphic_on_imp_analytic_at open_Diff) + ultimately show ?thesis + using ff_def remove_sings_at_analytic that(3) by presburger + qed + ultimately show ?thesis unfolding pz_def by auto + qed + + + have "contour_integral g (\x. deriv f x * h x / f x) + = contour_integral g (\x. deriv ff x * h x / ff x)" + proof (rule contour_integral_eq) + fix x assume "x \ path_image g" + have "f analytic_on {x}" + proof (rule holomorphic_on_imp_analytic_at[of _ "s-poles"]) + from finite' + show "open (s - poles)" + using \open s\ + by (metis Diff_Compl Diff_Diff_Int Diff_eq finite_imp_closed + open_Diff) + show "x \ s - poles" + using path_img \x \ path_image g\ unfolding pz_def by auto + qed (use f_holo in simp) + then show "deriv f x * h x / f x = deriv ff x * h x / ff x" + unfolding ff_def by auto + qed + also have "... = complex_of_real (2 * pi) * \ * + (\p\{w \ s. ff w = 0 \ w \ pts'}. + winding_number g p * h p * of_int (zorder ff p))" + proof (rule argument_principle[OF \open s\ \connected s\, of ff pts' h g]) + show "path_image g \ s - {w \ s. ff w = 0 \ w \ pts'}" + using path_img pts'_sub_pz by auto + show "finite {w \ s. ff w = 0 \ w \ pts'}" + using pts'_sub_pz finite + using rev_finite_subset by blast + qed (use pts' assms in auto) + also have "... = 2 * pi * \ * + (\p\pz. winding_number g p * h p * zorder f p)" + proof - + have "(\p\{w \ s. ff w = 0 \ w \ pts'}. + winding_number g p * h p * of_int (zorder ff p)) = + (\p\pz. winding_number g p * h p * of_int (zorder f p))" + proof (rule sum.mono_neutral_cong_left) + have "zorder f w = 0" + if "w\s" " f w = 0 \ w \ poles" "ff w \ 0" " w \ pts'" + for w + proof - + define F where "F=laurent_expansion f w" + have has_l:"(\x. f (w + x)) has_laurent_expansion F" + unfolding F_def + apply (rule not_essential_has_laurent_expansion) + using isolated not_ess \w\s\ by auto + from has_laurent_expansion_eventually_nonzero_iff[OF this] + have "F \0" + using nzero \w\s\ by auto + from tendsto_0_subdegree_iff[OF has_l this] + have "f \w\ 0 = (0 < fls_subdegree F)" . + moreover have "\ (is_pole f w \ f \w\ 0)" + using remove_sings_eq_0_iff[OF not_ess[OF \w\s\]] \ff w \ 0\ + unfolding ff_def by auto + moreover have "is_pole f w = (fls_subdegree F < 0)" + using is_pole_fls_subdegree_iff[OF has_l] . + ultimately have "fls_subdegree F = 0" by auto + then show ?thesis + using has_laurent_expansion_zorder[OF has_l \F\0\] by auto + qed + then show "\i\pz - {w \ s. ff w = 0 \ w \ pts'}. + winding_number g i * h i * of_int (zorder f i) = 0" + unfolding pz_def by auto + show "\x. x \ {w \ s. ff w = 0 \ w \ pts'} \ + winding_number g x * h x * of_int (zorder ff x) = + winding_number g x * h x * of_int (zorder f x)" + using isolated zorder_remove_sings[of f,folded ff_def] by auto + qed (use pts'_sub_pz finite in auto) + then show ?thesis by auto + qed + finally show ?thesis . +qed + +lemma meromorphic_on_imp_isolated_singularity: + assumes "f meromorphic_on D pts" "z \ D" + shows "isolated_singularity_at f z" + by (meson DiffI assms(1) assms(2) holomorphic_on_imp_analytic_at isolated_singularity_at_analytic + meromorphic_imp_open_diff meromorphic_on_def) + +lemma meromorphic_imp_not_is_pole: + assumes "f meromorphic_on D pts" "z \ D - pts" + shows "\is_pole f z" +proof - + from assms have "f analytic_on {z}" + using meromorphic_on_imp_analytic_at by blast + thus ?thesis + using analytic_at not_is_pole_holomorphic by blast +qed + +lemma meromorphic_all_poles_iff_empty [simp]: "f meromorphic_on pts pts \ pts = {}" + by (auto simp: meromorphic_on_def holomorphic_on_def open_imp_islimpt) + +lemma meromorphic_imp_nonsingular_point_exists: + assumes "f meromorphic_on A pts" "A \ {}" + obtains x where "x \ A - pts" +proof - + have "A \ pts" + using assms by auto + moreover have "pts \ A" + using assms by (auto simp: meromorphic_on_def) + ultimately show ?thesis + using that by blast +qed + +lemma meromorphic_frequently_const_imp_const: + assumes "f meromorphic_on A pts" "connected A" + assumes "frequently (\w. f w = c) (at z)" + assumes "z \ A - pts" + assumes "w \ A - pts" + shows "f w = c" +proof - + have "f w - c = 0" + proof (rule analytic_continuation[where f = "\z. f z - c"]) + show "(\z. f z - c) holomorphic_on (A - pts)" + by (intro holomorphic_intros meromorphic_imp_holomorphic[OF assms(1)]) + show [intro]: "open (A - pts)" + using assms meromorphic_imp_open_diff by blast + show "connected (A - pts)" + using assms meromorphic_imp_connected_diff by blast + show "{z\A-pts. f z = c} \ A - pts" + by blast + have "eventually (\z. z \ A - pts) (at z)" + using assms by (intro eventually_at_in_open') auto + hence "frequently (\z. f z = c \ z \ A - pts) (at z)" + by (intro frequently_eventually_frequently assms) + thus "z islimpt {z\A-pts. f z = c}" + by (simp add: islimpt_conv_frequently_at conj_commute) + qed (use assms in auto) + thus ?thesis + by simp +qed + +lemma meromorphic_imp_eventually_neq: + assumes "f meromorphic_on A pts" "connected A" "\f constant_on A - pts" + assumes "z \ A - pts" + shows "eventually (\z. f z \ c) (at z)" +proof (rule ccontr) + assume "\eventually (\z. f z \ c) (at z)" + hence *: "frequently (\z. f z = c) (at z)" + by (auto simp: frequently_def) + have "\w\A-pts. f w = c" + using meromorphic_frequently_const_imp_const [OF assms(1,2) * assms(4)] by blast + hence "f constant_on A - pts" + by (auto simp: constant_on_def) + thus False + using assms(3) by contradiction +qed + +lemma meromorphic_frequently_const_imp_const': + assumes "f meromorphic_on A pts" "connected A" "\w\pts. is_pole f w" + assumes "frequently (\w. f w = c) (at z)" + assumes "z \ A" + assumes "w \ A" + shows "f w = c" +proof - + have "\is_pole f z" + using frequently_const_imp_not_is_pole[OF assms(4)] . + with assms have z: "z \ A - pts" + by auto + have *: "f w = c" if "w \ A - pts" for w + using that meromorphic_frequently_const_imp_const [OF assms(1,2,4) z] by auto + have "\is_pole f u" if "u \ A" for u + proof - + have "is_pole f u \ is_pole (\_. c) u" + proof (rule is_pole_cong) + have "eventually (\w. w \ A - (pts - {u}) - {u}) (at u)" + by (intro eventually_at_in_open meromorphic_imp_open_diff' [OF assms(1)]) (use that in auto) + thus "eventually (\w. f w = c) (at u)" + by eventually_elim (use * in auto) + qed auto + thus ?thesis + by auto + qed + moreover have "pts \ A" + using assms(1) by (simp add: meromorphic_on_def) + ultimately have "pts = {}" + using assms(3) by auto + with * and \w \ A\ show ?thesis + by blast +qed + +lemma meromorphic_imp_eventually_neq': + assumes "f meromorphic_on A pts" "connected A" "\w\pts. is_pole f w" "\f constant_on A" + assumes "z \ A" + shows "eventually (\z. f z \ c) (at z)" +proof (rule ccontr) + assume "\eventually (\z. f z \ c) (at z)" + hence *: "frequently (\z. f z = c) (at z)" + by (auto simp: frequently_def) + have "\w\A. f w = c" + using meromorphic_frequently_const_imp_const' [OF assms(1,2,3) * assms(5)] by blast + hence "f constant_on A" + by (auto simp: constant_on_def) + thus False + using assms(4) by contradiction +qed + +lemma zorder_eq_0_iff_meromorphic: + assumes "f meromorphic_on A pts" "\z\pts. is_pole f z" "z \ A" + assumes "eventually (\x. f x \ 0) (at z)" + shows "zorder f z = 0 \ \is_pole f z \ f z \ 0" +proof (cases "z \ pts") + case True + from assms obtain F where F: "(\x. f (z + x)) has_laurent_expansion F" + by (metis True meromorphic_on_def not_essential_has_laurent_expansion) (* TODO: better lemmas *) + from F and assms(4) have [simp]: "F \ 0" + using has_laurent_expansion_eventually_nonzero_iff by blast + show ?thesis using True assms(2) + using is_pole_fls_subdegree_iff [OF F] has_laurent_expansion_zorder [OF F] + by auto +next + case False + have ana: "f analytic_on {z}" + using meromorphic_on_imp_analytic_at False assms by blast + hence "\is_pole f z" + using analytic_at not_is_pole_holomorphic by blast + moreover have "frequently (\w. f w \ 0) (at z)" + using assms(4) by (intro eventually_frequently) auto + ultimately show ?thesis using zorder_eq_0_iff[OF ana] False + by auto +qed + +lemma zorder_pos_iff_meromorphic: + assumes "f meromorphic_on A pts" "\z\pts. is_pole f z" "z \ A" + assumes "eventually (\x. f x \ 0) (at z)" + shows "zorder f z > 0 \ \is_pole f z \ f z = 0" +proof (cases "z \ pts") + case True + from assms obtain F where F: "(\x. f (z + x)) has_laurent_expansion F" + by (metis True meromorphic_on_def not_essential_has_laurent_expansion) (* TODO: better lemmas *) + from F and assms(4) have [simp]: "F \ 0" + using has_laurent_expansion_eventually_nonzero_iff by blast + show ?thesis using True assms(2) + using is_pole_fls_subdegree_iff [OF F] has_laurent_expansion_zorder [OF F] + by auto +next + case False + have ana: "f analytic_on {z}" + using meromorphic_on_imp_analytic_at False assms by blast + hence "\is_pole f z" + using analytic_at not_is_pole_holomorphic by blast + moreover have "frequently (\w. f w \ 0) (at z)" + using assms(4) by (intro eventually_frequently) auto + ultimately show ?thesis using zorder_pos_iff'[OF ana] False + by auto +qed + +lemma zorder_neg_iff_meromorphic: + assumes "f meromorphic_on A pts" "\z\pts. is_pole f z" "z \ A" + assumes "eventually (\x. f x \ 0) (at z)" + shows "zorder f z < 0 \ is_pole f z" +proof - + have "frequently (\x. f x \ 0) (at z)" + using assms by (intro eventually_frequently) auto + moreover from assms have "isolated_singularity_at f z" "not_essential f z" + using meromorphic_on_imp_isolated_singularity meromorphic_on_imp_not_essential by blast+ + ultimately show ?thesis + using isolated_pole_imp_neg_zorder neg_zorder_imp_is_pole by blast +qed + +lemma meromorphic_on_imp_discrete: + assumes mero:"f meromorphic_on S pts" and "connected S" + and nconst:"\ (\w\S - pts. f w = c)" + shows "discrete {x\S. f x=c}" +proof - + define g where "g=(\x. f x - c)" + have "\\<^sub>F w in at z. g w \ 0" if "z \ S" for z + proof (rule nconst_imp_nzero_neighbour'[of g S pts z]) + show "g meromorphic_on S pts" using mero unfolding g_def + by (auto intro:meromorphic_intros) + show "\ (\w\S - pts. g w = 0)" using nconst unfolding g_def by auto + qed fact+ + then show ?thesis + unfolding discrete_altdef g_def + using eventually_mono by fastforce +qed + +lemma meromorphic_isolated_in: + assumes merf: "f meromorphic_on D pts" "p\pts" + shows "p isolated_in pts" + by (meson assms isolated_in_islimpt_iff meromorphic_on_def subsetD) + +lemma remove_sings_constant_on: + assumes merf: "f meromorphic_on D pts" and "connected D" + and const:"f constant_on (D - pts)" + shows "(remove_sings f) constant_on D" +proof - + have remove_sings_const: "remove_sings f constant_on D - pts" + using const + by (metis constant_onE merf meromorphic_on_imp_analytic_at remove_sings_at_analytic) + + have ?thesis if "D = {}" + using that unfolding constant_on_def by auto + moreover have ?thesis if "D\{}" "{x\pts. is_pole f x} = {}" + proof - + obtain \ where "\ \ (D - pts)" "\ islimpt (D - pts)" + proof - + have "open (D - pts)" + using meromorphic_imp_open_diff[OF merf] . + moreover have "(D - pts) \ {}" using \D\{}\ + by (metis Diff_empty closure_empty merf + meromorphic_pts_closure subset_empty) + ultimately show ?thesis using open_imp_islimpt that by auto + qed + moreover have "remove_sings f holomorphic_on D" + using remove_sings_holomorphic_on[OF merf] that by auto + moreover note remove_sings_const + moreover have "open D" + using assms(1) meromorphic_on_def by blast + ultimately show ?thesis + using Conformal_Mappings.analytic_continuation' + [of "remove_sings f" D "D-pts" \] \connected D\ + by auto + qed + moreover have ?thesis if "D\{}" "{x\pts. is_pole f x} \ {}" + proof - + define PP where "PP={x\D. is_pole f x}" + have "remove_sings f meromorphic_on D PP" + using merf unfolding PP_def + apply (elim remove_sings_meromorphic_on) + subgoal using assms(1) meromorphic_on_def by force + subgoal using meromorphic_pole_subset merf by auto + done + moreover have "remove_sings f constant_on D - PP" + proof - + obtain \ where "\ \ f ` (D - pts)" + by (metis Diff_empty Diff_eq_empty_iff \D \ {}\ assms(1) + closure_empty ex_in_conv imageI meromorphic_pts_closure) + have \:"\x\D - pts. f x = \" + by (metis \\ \ f ` (D - pts)\ assms(3) constant_on_def image_iff) + + have "remove_sings f x = \" if "x\D - PP" for x + proof (cases "x\pts") + case True + then have"x isolated_in pts" + using meromorphic_isolated_in[OF merf] by auto + then obtain T0 where T0:"open T0" "T0 \ pts = {x}" + unfolding isolated_in_def by auto + obtain T1 where T1:"open T1" "x\T1" "T1 \ D" + using merf unfolding meromorphic_on_def + using True by blast + define T2 where "T2 = T1 \ T0" + have "open T2" "x\T2" "T2 - {x} \ D - pts" + using T0 T1 unfolding T2_def by auto + then have "\w\T2. w\x \ f w =\" + using \ by auto + then have "\\<^sub>F x in at x. f x = \" + unfolding eventually_at_topological + using \open T2\ \x\T2\ by auto + then have "f \x\ \" + using tendsto_eventually by auto + then show ?thesis by blast + next + case False + then show ?thesis + using \\x\D - pts. f x = \\ assms(1) + meromorphic_on_imp_analytic_at that by auto + qed + + then show ?thesis unfolding constant_on_def by auto + qed + + moreover have "is_pole (remove_sings f) x" if "x\PP" for x + proof - + have "isolated_singularity_at f x" + by (metis (mono_tags, lifting) DiffI PP_def assms(1) + isolated_singularity_at_analytic mem_Collect_eq + meromorphic_on_def meromorphic_on_imp_analytic_at that) + then show ?thesis using that unfolding PP_def by simp + qed + ultimately show ?thesis + using meromorphic_imp_constant_on + [of "remove_sings f" D PP] + by auto + qed + ultimately show ?thesis by auto +qed + +lemma meromorphic_eq_meromorphic_extend: + assumes "f meromorphic_on A pts1" "g meromorphic_on A pts1" "\z islimpt pts2" + assumes "\z. z \ A - pts2 \ f z = g z" "pts1 \ pts2" "z \ A - pts1" + shows "f z = g z" +proof - + have "g analytic_on {z}" + using assms by (intro meromorphic_on_imp_analytic_at[OF assms(2)]) auto + hence "g \z\ g z" + using analytic_at_imp_isCont isContD by blast + also have "?this \ f \z\ g z" + proof (intro filterlim_cong) + have "eventually (\w. w \ pts2) (at z)" + using assms by (auto simp: islimpt_conv_frequently_at frequently_def) + moreover have "eventually (\w. w \ A) (at z)" + using assms by (intro eventually_at_in_open') (auto simp: meromorphic_on_def) + ultimately show "\\<^sub>F x in at z. g x = f x" + by eventually_elim (use assms in auto) + qed auto + finally have "f \z\ g z" . + moreover have "f analytic_on {z}" + using assms by (intro meromorphic_on_imp_analytic_at[OF assms(1)]) auto + hence "f \z\ f z" + using analytic_at_imp_isCont isContD by blast + ultimately show ?thesis + using tendsto_unique by force +qed + +lemma meromorphic_constant_on_extend: + assumes "f constant_on A - pts1" "f meromorphic_on A pts1" "f meromorphic_on A pts2" "pts2 \ pts1" + shows "f constant_on A - pts2" +proof - + from assms(1) obtain c where c: "\z. z \ A - pts1 \ f z = c" + unfolding constant_on_def by auto + have "f z = c" if "z \ A - pts2" for z + using assms(3) + proof (rule meromorphic_eq_meromorphic_extend[where z = z]) + show "(\a. c) meromorphic_on A pts2" + by (intro meromorphic_on_const) (use assms in \auto simp: meromorphic_on_def\) + show "\z islimpt pts1" + using that assms by (auto simp: meromorphic_on_def) + qed (use assms c that in auto) + thus ?thesis + by (auto simp: constant_on_def) +qed + +lemma meromorphic_remove_sings_constant_on_imp_constant_on: + assumes "f meromorphic_on A pts" + assumes "remove_sings f constant_on A" + shows "f constant_on A - pts" +proof - + from assms(2) obtain c where c: "\z. z \ A \ remove_sings f z = c" + by (auto simp: constant_on_def) + have "f z = c" if "z \ A - pts" for z + using meromorphic_on_imp_analytic_at[OF assms(1) that] c[of z] that + by auto + thus ?thesis + by (auto simp: constant_on_def) +qed + + + + +definition singularities_on :: "complex set \ (complex \ complex) \ complex set" where + "singularities_on A f = + {z\A. isolated_singularity_at f z \ not_essential f z \ \f analytic_on {z}}" + +lemma singularities_on_subset: "singularities_on A f \ A" + by (auto simp: singularities_on_def) + +lemma pole_in_singularities_on: + assumes "f meromorphic_on A pts" "z \ A" "is_pole f z" + shows "z \ singularities_on A f" + unfolding singularities_on_def not_essential_def using assms + using analytic_at_imp_no_pole meromorphic_on_imp_isolated_singularity by force + + +lemma meromorphic_on_subset_pts: + assumes "f meromorphic_on A pts" "pts' \ pts" "f analytic_on pts - pts'" + shows "f meromorphic_on A pts'" +proof + show "open A" "pts' \ A" + using assms by (auto simp: meromorphic_on_def) + show "isolated_singularity_at f z" "not_essential f z" if "z \ pts'" for z + using assms that by (auto simp: meromorphic_on_def) + show "\z islimpt pts'" if "z \ A" for z + using assms that islimpt_subset unfolding meromorphic_on_def by blast + have "f analytic_on A - pts" + using assms(1) meromorphic_imp_analytic by blast + with assms have "f analytic_on (A - pts) \ (pts - pts')" + by (subst analytic_on_Un) auto + also have "(A - pts) \ (pts - pts') = A - pts'" + using assms by (auto simp: meromorphic_on_def) + finally show "f holomorphic_on A - pts'" + using analytic_imp_holomorphic by blast +qed + +lemma meromorphic_on_imp_superset_singularities_on: + assumes "f meromorphic_on A pts" + shows "singularities_on A f \ pts" +proof + fix z assume "z \ singularities_on A f" + hence "z \ A" "\f analytic_on {z}" + by (auto simp: singularities_on_def) + with assms show "z \ pts" + by (meson DiffI meromorphic_on_imp_analytic_at) +qed + +lemma meromorphic_on_singularities_on: + assumes "f meromorphic_on A pts" + shows "f meromorphic_on A (singularities_on A f)" + using assms meromorphic_on_imp_superset_singularities_on[OF assms] +proof (rule meromorphic_on_subset_pts) + have "f analytic_on {z}" if "z \ pts - singularities_on A f" for z + using that assms by (auto simp: singularities_on_def meromorphic_on_def) + thus "f analytic_on pts - singularities_on A f" + using analytic_on_analytic_at by blast +qed + +theorem Residue_theorem_inside: + assumes f: "f meromorphic_on s pts" + "simply_connected s" + assumes g: "valid_path g" + "pathfinish g = pathstart g" + "path_image g \ s - pts" + defines "pts1 \ pts \ inside (path_image g)" + shows "finite pts1" + and "contour_integral g f = 2 * pi * \ * (\p\pts1. winding_number g p * residue f p)" +proof - + note [dest] = valid_path_imp_path + have cl_g [intro]: "closed (path_image g)" + using g by (auto intro!: closed_path_image) + have "open s" + using f(1) by (auto simp: meromorphic_on_def) + define pts2 where "pts2 = pts - pts1" + + define A where "A = path_image g \ inside (path_image g)" + have "closed A" + unfolding A_def using g by (intro closed_path_image_Un_inside) auto + moreover have "bounded A" + unfolding A_def using g by (auto intro!: bounded_path_image bounded_inside) + ultimately have 1: "compact A" + using compact_eq_bounded_closed by blast + have 2: "open (s - pts2)" + using f by (auto intro!: meromorphic_imp_open_diff' [OF f(1)] simp: pts2_def) + have 3: "A \ s - pts2" + unfolding A_def pts2_def pts1_def + using f(2) g(3) 2 subset_simply_connected_imp_inside_subset[of s "path_image g"] \open s\ + by auto + + obtain \ where \: "\ > 0" "(\x\A. ball x \) \ s - pts2" + using compact_subset_open_imp_ball_epsilon_subset[OF 1 2 3] by blast + define B where "B = (\x\A. ball x \)" + + have "finite (A \ pts)" + using 1 3 by (intro meromorphic_compact_finite_pts[OF f(1)]) auto + also have "A \ pts = pts1" + unfolding pts1_def using g by (auto simp: A_def) + finally show fin: "finite pts1" . + + show "contour_integral g f = 2 * pi * \ * (\p\pts1. winding_number g p * residue f p)" + proof (rule Residue_theorem) + show "open B" + by (auto simp: B_def) + next + have "connected A" + unfolding A_def using g + by (intro connected_with_inside closed_path_image connected_path_image) auto + hence "connected (A \ B)" + unfolding B_def using g \\ > 0\ f(2) + by (intro connected_Un_UN connected_path_image valid_path_imp_path) + (auto simp: simply_connected_imp_connected) + also have "A \ B = B" + using \(1) by (auto simp: B_def) + finally show "connected B" . + next + have "f holomorphic_on (s - pts)" + by (intro meromorphic_imp_holomorphic f) + moreover have "B - pts1 \ s - pts" + using \ unfolding B_def by (auto simp: pts1_def pts2_def) + ultimately show "f holomorphic_on (B - pts1)" + by (rule holomorphic_on_subset) + next + have "path_image g \ A - pts1" + using g unfolding pts1_def by (auto simp: A_def) + also have "\ \ B - pts1" + unfolding B_def using \(1) by auto + finally show "path_image g \ B - pts1" . + next + show "\z. z \ B \ winding_number g z = 0" + proof safe + fix z assume z: "z \ B" + hence "z \ A" + using \(1) by (auto simp: B_def) + hence "z \ outside (path_image g)" + unfolding A_def by (simp add: union_with_inside) + thus "winding_number g z = 0" + using g by (intro winding_number_zero_in_outside) auto + qed + qed (use g fin in auto) +qed + +theorem Residue_theorem': + assumes f: "f meromorphic_on s pts" + "simply_connected s" + assumes g: "valid_path g" + "pathfinish g = pathstart g" + "path_image g \ s - pts" + assumes pts': "finite pts'" + "pts' \ s" + "\z. z \ pts - pts' \ winding_number g z = 0" + shows "contour_integral g f = 2 * pi * \ * (\p\pts'. winding_number g p * residue f p)" +proof - + note [dest] = valid_path_imp_path + define pts1 where "pts1 = pts \ inside (path_image g)" + + have "contour_integral g f = 2 * pi * \ * (\p\pts1. winding_number g p * residue f p)" + unfolding pts1_def by (intro Residue_theorem_inside[OF f g]) + also have "(\p\pts1. winding_number g p * residue f p) = + (\p\pts'. winding_number g p * residue f p)" + proof (intro sum.mono_neutral_cong refl) + show "finite pts1" + unfolding pts1_def by (intro Residue_theorem_inside[OF f g]) + show "finite pts'" + by fact + next + fix z assume z: "z \ pts' - pts1" + show "winding_number g z * residue f z = 0" + proof (cases "z \ pts") + case True + with z have "z \ path_image g \ inside (path_image g)" + using g(3) by (auto simp: pts1_def) + hence "z \ outside (path_image g)" + by (simp add: union_with_inside) + hence "winding_number g z = 0" + using g by (intro winding_number_zero_in_outside) auto + thus ?thesis + by simp + next + case False + with z pts' have "z \ s - pts" + by auto + with f(1) have "f analytic_on {z}" + by (intro meromorphic_on_imp_analytic_at) + hence "residue f z = 0" + using analytic_at residue_holo by blast + thus ?thesis + by simp + qed + next + fix z assume z: "z \ pts1 - pts'" + hence "winding_number g z = 0" + using pts' by (auto simp: pts1_def) + thus "winding_number g z * residue f z = 0" + by simp + qed + finally show ?thesis . +qed + +end \ No newline at end of file diff -r 29032b496f2e -r c6b50597abbc src/HOL/Complex_Analysis/Residue_Theorem.thy --- a/src/HOL/Complex_Analysis/Residue_Theorem.thy Thu Feb 16 10:42:39 2023 +0000 +++ b/src/HOL/Complex_Analysis/Residue_Theorem.thy Thu Feb 16 12:21:21 2023 +0000 @@ -3,6 +3,34 @@ imports Complex_Residues "HOL-Library.Landau_Symbols" begin +text \Could be moved to a previous theory importing both Landau Symbols and Elementary Metric Spaces\ +lemma continuous_bounded_at_infinity_imp_bounded: + fixes f :: "real \ 'a :: real_normed_field" + assumes "f \ O[at_bot](\_. 1)" + assumes "f \ O[at_top](\_. 1)" + assumes "continuous_on UNIV f" + shows "bounded (range f)" +proof - + from assms(1) obtain c1 where "eventually (\x. norm (f x) \ c1) at_bot" + by (auto elim!: landau_o.bigE) + then obtain x1 where x1: "\x. x \ x1 \ norm (f x) \ c1" + by (auto simp: eventually_at_bot_linorder) + from assms(2) obtain c2 where "eventually (\x. norm (f x) \ c2) at_top" + by (auto elim!: landau_o.bigE) + then obtain x2 where x2: "\x. x \ x2 \ norm (f x) \ c2" + by (auto simp: eventually_at_top_linorder) + have "compact (f ` {x1..x2})" + by (intro compact_continuous_image continuous_on_subset[OF assms(3)]) auto + hence "bounded (f ` {x1..x2})" + by (rule compact_imp_bounded) + then obtain c3 where c3: "\x. x \ {x1..x2} \ norm (f x) \ c3" + unfolding bounded_iff by fast + have "norm (f x) \ Max {c1, c2, c3}" for x + by (cases "x \ x1"; cases "x \ x2") (use x1 x2 c3 in \auto simp: le_max_iff_disj\) + thus ?thesis + unfolding bounded_iff by blast +qed + subsection \Cauchy's residue theorem\ lemma get_integrable_path: diff -r 29032b496f2e -r c6b50597abbc src/HOL/Complex_Analysis/Riemann_Mapping.thy --- a/src/HOL/Complex_Analysis/Riemann_Mapping.thy Thu Feb 16 10:42:39 2023 +0000 +++ b/src/HOL/Complex_Analysis/Riemann_Mapping.thy Thu Feb 16 12:21:21 2023 +0000 @@ -1245,21 +1245,9 @@ interpret SC_Chain using assms by (simp add: SC_Chain_def) have "?fp \ ?ucc \ ?ei" -proof - - have *: "\\ \ \; \ \ \; \ \ \; \ \ \\ - \ (\ \ \) \ (\ \ \) \ (\ \ \)" for \ \ \ \ - by blast - show ?thesis - apply (rule *) - using frontier_properties simply_connected_imp_connected apply blast -apply clarify - using unbounded_complement_components simply_connected_imp_connected apply blast - using empty_inside apply blast - using empty_inside_imp_simply_connected apply blast - done -qed + using empty_inside empty_inside_imp_simply_connected frontier_properties unbounded_complement_components winding_number_zero by blast then show ?fp ?ucc ?ei - by safe + by blast+ qed lemma simply_connected_iff_simple: @@ -1270,6 +1258,12 @@ apply (metis DIM_complex assms(2) cobounded_has_bounded_component double_compl order_refl) by (meson assms inside_bounded_complement_connected_empty simply_connected_eq_empty_inside simply_connected_eq_unbounded_complement_components) +lemma subset_simply_connected_imp_inside_subset: + fixes A :: "complex set" + assumes "simply_connected A" "open A" "B \ A" + shows "inside B \ A" +by (metis assms Diff_eq_empty_iff inside_mono subset_empty simply_connected_eq_empty_inside) + subsection\Further equivalences based on continuous logs and sqrts\ context SC_Chain @@ -1299,9 +1293,7 @@ and expg: "\z. z \ ball 0 1 \ (f \ k) z = exp (g z)" proof (rule continuous_logarithm_on_ball) show "continuous_on (ball 0 1) (f \ k)" - apply (rule continuous_on_compose [OF contk]) - using kim continuous_on_subset [OF contf] - by blast + using contf continuous_on_compose contk kim by blast show "\z. z \ ball 0 1 \ (f \ k) z \ 0" using kim nz by auto qed auto @@ -1438,9 +1430,7 @@ lemma Borsukian_eq_simply_connected: fixes S :: "complex set" shows "open S \ Borsukian S \ (\C \ components S. simply_connected C)" -apply (auto simp: Borsukian_componentwise_eq open_imp_locally_connected) - using in_components_connected open_components simply_connected_eq_Borsukian apply blast - using open_components simply_connected_eq_Borsukian by blast + by (meson Borsukian_componentwise_eq in_components_connected open_components open_imp_locally_connected simply_connected_eq_Borsukian) lemma Borsukian_separation_open_closed: fixes S :: "complex set" @@ -1451,7 +1441,7 @@ assume "open S" show ?thesis unfolding Borsukian_eq_simply_connected [OF \open S\] - by (meson \open S\ \bounded S\ bounded_subset in_components_connected in_components_subset nonseparation_by_component_eq open_components simply_connected_iff_simple) + by (metis \open S\ \bounded S\ bounded_subset in_components_maximal nonseparation_by_component_eq open_components simply_connected_iff_simple) next assume "closed S" with \bounded S\ show ?thesis @@ -1659,10 +1649,8 @@ proof assume ?lhs then show ?rhs - apply (auto simp: winding_number_homotopic_loops_null_eq [OF assms]) - apply (rule homotopic_loops_imp_homotopic_paths_null) - apply (simp add: linepath_refl) - done + using homotopic_loops_imp_homotopic_paths_null + by (force simp add: linepath_refl winding_number_homotopic_loops_null_eq [OF assms]) next assume ?rhs then show ?lhs @@ -1701,11 +1689,7 @@ then show ?rhs using homotopic_paths_imp_pathstart assms by (fastforce simp add: dest: homotopic_paths_imp_homotopic_loops homotopic_paths_loop_parts) -next - assume ?rhs - then show ?lhs - by (simp add: winding_number_homotopic_paths) -qed +qed (simp add: winding_number_homotopic_paths) lemma winding_number_homotopic_loops_eq: assumes "path p" and \p: "\ \ path_image p" @@ -1725,17 +1709,20 @@ then have "pathstart r \ \" by blast have "homotopic_loops (- {\}) p (r +++ q +++ reversepath r)" proof (rule homotopic_paths_imp_homotopic_loops) - show "homotopic_paths (- {\}) p (r +++ q +++ reversepath r)" - by (metis (mono_tags, opaque_lifting) \path r\ L \p \q \path p\ \path q\ homotopic_loops_conjugate loops not_in_path_image_join paf pas path_image_reversepath path_imp_reversepath path_join_eq pathfinish_join pathfinish_reversepath pathstart_join pathstart_reversepath rim subset_Compl_singleton winding_number_homotopic_loops winding_number_homotopic_paths_eq) + have "path (r +++ q +++ reversepath r)" + by (simp add: \path r\ \path q\ loops paf) + moreover have "\ \ path_image (r +++ q +++ reversepath r)" + by (metis \q not_in_path_image_join path_image_reversepath rim subset_Compl_singleton) + moreover have "homotopic_loops (- {\}) (r +++ q +++ reversepath r) q" + using \path q\ \path r\ \q homotopic_loops_conjugate loops(2) paf rim by blast + ultimately show "homotopic_paths (- {\}) p (r +++ q +++ reversepath r)" + using loops pathfinish_join pathfinish_reversepath pathstart_join + by (metis L \p \path p\ pas winding_number_homotopic_loops winding_number_homotopic_paths_eq) qed (use loops pas in auto) moreover have "homotopic_loops (- {\}) (r +++ q +++ reversepath r) q" using rim \q by (auto simp: homotopic_loops_conjugate paf \path q\ \path r\ loops) ultimately show ?rhs using homotopic_loops_trans by metis -next - assume ?rhs - then show ?lhs - by (simp add: winding_number_homotopic_loops) -qed +qed (simp add: winding_number_homotopic_loops) end diff -r 29032b496f2e -r c6b50597abbc src/HOL/Complex_Analysis/Winding_Numbers.thy --- a/src/HOL/Complex_Analysis/Winding_Numbers.thy Thu Feb 16 10:42:39 2023 +0000 +++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy Thu Feb 16 12:21:21 2023 +0000 @@ -901,6 +901,16 @@ by metis qed +lemma bounded_winding_number_nz: + assumes "path g" "pathfinish g = pathstart g" + shows "bounded {z. winding_number g z \ 0}" +proof - + obtain B where "\x. norm x \ B \ winding_number g x = 0" + using winding_number_zero_at_infinity[OF assms] by auto + thus ?thesis + unfolding bounded_iff by (intro exI[of _ "B + 1"]) force +qed + lemma winding_number_zero_point: "\path \; convex S; pathfinish \ = pathstart \; open S; path_image \ \ S\ \ \z. z \ S \ winding_number \ z = 0" diff -r 29032b496f2e -r c6b50597abbc src/HOL/Library/Landau_Symbols.thy --- a/src/HOL/Library/Landau_Symbols.thy Thu Feb 16 10:42:39 2023 +0000 +++ b/src/HOL/Library/Landau_Symbols.thy Thu Feb 16 12:21:21 2023 +0000 @@ -1742,6 +1742,10 @@ by (rule Lim_transform_eventually) qed (simp_all add: asymp_equiv_def) +lemma tendsto_imp_asymp_equiv_const: + assumes "(f \ c) F" "c \ 0" + shows "f \[F] (\_. c)" + by (rule asymp_equivI' tendsto_eq_intros assms refl)+ (use assms in auto) lemma asymp_equiv_cong: assumes "eventually (\x. f1 x = f2 x) F" "eventually (\x. g1 x = g2 x) F"