: "\w. \fp w = 0; dist z w < fr\ \ False" + using fr_nz by force + then show "\w\ball z r1 - {z}. + vf w = vfp w * (w - z) powr complex_of_int vfn \ + vfp w \ 0 \ vf w = inverse (fp w) * (w - z) powr complex_of_int (- fn) \ + inverse (fp w) \ 0" + using fr_inverse r1_def vfr(2) + by (smt (verit) Diff_iff inverse_nonzero_iff_nonzero mem_ball mem_cball) + show "vfp holomorphic_on ball z r1" + using r1_def vfr(1) by auto + show "(\w. inverse (fp w)) holomorphic_on ball z r1" + by (metis \

ball_subset_cball fr(1) holomorphic_on_inverse holomorphic_on_subset mem_ball min.cobounded2 min.commute r1_def subset_ball) + qed (use \r1>0\ in auto) have "vfp w = inverse (fp w)" when "w\ball z r1-{z}" for w proof - have "w \ ball z fr - {z}" "w \ cball z vfr - {z}" "w\z" using that unfolding r1_def by auto @@ -816,8 +816,7 @@ qed then show "\\<^sub>Fw in (at z). vfp w = inverse (fp w)" unfolding eventually_at using \r1>0\ - apply (rule_tac x=r1 in exI) - by (auto simp add:dist_commute) + by (metis DiffI dist_commute mem_ball singletonD) qed lemma @@ -929,8 +928,7 @@ done then show "\\<^sub>Fw in (at z). zor_poly (\w. f w / g w) z w = zor_poly f z w / zor_poly g z w" using zor_poly_inverse[OF g_iso g_ness g_nconst,folded vg_def] unfolding vg_def - apply eventually_elim - by (auto simp add:field_simps) + by eventually_elim (auto simp add:field_simps) qed lemma zorder_exist_zero: @@ -978,29 +976,25 @@ ultimately show ?thesis using that[of r3] \g z\0\ by auto qed + have fz_lim: "f\ z \ f z" + by (metis assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on) + have gz_lim: "g \z\g z" + by (metis r open_ball at_within_open ball_subset_cball centre_in_ball + continuous_on_def continuous_on_subset holomorphic_on_imp_continuous_on) have if_0:"if f z=0 then n > 0 else n=0" proof - - have "f\ z \ f z" - by (metis assms(4,6,7) at_within_open continuous_on holo holomorphic_on_imp_continuous_on) - then have "(\w. g w * (w - z) powr of_int n) \z\ f z" - apply (elim Lim_transform_within_open[where s="ball z r"]) - using r by auto - moreover have "g \z\g z" - by (metis (mono_tags, lifting) open_ball at_within_open_subset - ball_subset_cball centre_in_ball continuous_on holomorphic_on_imp_continuous_on r(1,3) subsetCE) - ultimately have "(\w. (g w * (w - z) powr of_int n) / g w) \z\ f z/g z" - apply (rule_tac tendsto_divide) - using \g z\0\ by auto + have "(\w. g w * (w - z) powr of_int n) \z\ f z" + using fz_lim Lim_transform_within_open[where s="ball z r"] r by fastforce + then have "(\w. (g w * (w - z) powr of_int n) / g w) \z\ f z/g z" + using gz_lim \g z \ 0\ tendsto_divide by blast then have powr_tendsto:"(\w. (w - z) powr of_int n) \z\ f z/g z" - apply (elim Lim_transform_within_open[where s="ball z r"]) - using r by auto + using Lim_transform_within_open[where s="ball z r"] r by fastforce have ?thesis when "n\0" "f z=0" proof - have "(\w. (w - z) ^ nat n) \z\ f z/g z" - using powr_tendsto - apply (elim Lim_transform_within[where d=r]) - by (auto simp add: powr_of_int \n\0\ \r>0\) + using powr_tendsto Lim_transform_within[where d=r] + by (fastforce simp: powr_of_int \n\0\ \r>0\) then have *:"(\w. (w - z) ^ nat n) \z\ 0" using \f z=0\ by simp moreover have False when "n=0" proof - @@ -1015,9 +1009,8 @@ have False when "n>0" proof - have "(\w. (w - z) ^ nat n) \z\ f z/g z" - using powr_tendsto - apply (elim Lim_transform_within[where d=r]) - by (auto simp add: powr_of_int \n\0\ \r>0\) + using powr_tendsto Lim_transform_within[where d=r] + by (fastforce simp add: powr_of_int \n\0\ \r>0\) moreover have "(\w. (w - z) ^ nat n) \z\ 0" using \n>0\ by (auto intro!:tendsto_eq_intros) ultimately show False using \f z\0\ \g z\0\ using LIM_unique divide_eq_0_iff by blast @@ -1028,10 +1021,8 @@ proof - have "(\w. inverse ((w - z) ^ nat (- n))) \z\ f z/g z" "(\w.((w - z) ^ nat (- n))) \z\ 0" - subgoal using powr_tendsto powr_of_int that - by (elim Lim_transform_within_open[where s=UNIV],auto) - subgoal using that by (auto intro!:tendsto_eq_intros) - done + apply (smt (verit, ccfv_SIG) LIM_cong eq_iff_diff_eq_0 powr_of_int powr_tendsto that) + using that by (auto intro!:tendsto_eq_intros) from tendsto_mult[OF this,simplified] have "(\x. inverse ((x - z) ^ nat (- n)) * (x - z) ^ nat (- n)) \z\ 0" . then have "(\x. 1::complex) \z\ 0" @@ -1044,7 +1035,7 @@ proof (cases "w=z") case True then have "f \z\f w" - using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on by fastforce + using fz_lim by blast then have "(\w. g w * (w-z) ^ nat n) \z\f w" proof (elim Lim_transform_within[OF _ \r>0\]) fix x assume "0 < dist x z" "dist x z < r" @@ -1053,14 +1044,11 @@ then have "f x = g x * (x - z) powr of_int n" using r(4)[rule_format,of x] by simp also have "... = g x * (x - z) ^ nat n" - apply (subst powr_of_int) - using if_0 \x\z\ by (auto split:if_splits) + by (smt (verit) \x \ z\ if_0 powr_of_int right_minus_eq) finally show "f x = g x * (x - z) ^ nat n" . qed moreover have "(\w. g w * (w-z) ^ nat n) \z\ g w * (w-z) ^ nat n" - using True apply (auto intro!:tendsto_eq_intros) - by (metis open_ball at_within_open_subset ball_subset_cball centre_in_ball - continuous_on holomorphic_on_imp_continuous_on r(1) r(3) that) + using True by (auto intro!:tendsto_eq_intros gz_lim) ultimately have "f w = g w * (w-z) ^ nat n" using LIM_unique by blast then show ?thesis using \g z\0\ True by auto next @@ -1122,7 +1110,7 @@ unfolding eventually_at_topological apply (rule_tac exI[where x="ball z r"]) using r powr_of_int \\ n < 0\ by auto - moreover have "(\x. g x * (x - z) ^ nat n) \z\c" + moreover have "(\x. g x * (x - z) ^ nat n) \z\ c" proof (cases "n=0") case True then show ?thesis unfolding c_def by simp