# HG changeset patch # User paulson # Date 1675949785 0 # Node ID 69956724ad4f59b4eb9d5e28e35621f08beee64e # Parent 607e1e345e8f6dd139f8ad298c50a05177d65b86 More material for Analysis and Complex_Analysis diff -r 607e1e345e8f -r 69956724ad4f src/HOL/Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Wed Feb 08 15:05:24 2023 +0000 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Feb 09 13:36:25 2023 +0000 @@ -417,14 +417,24 @@ (metis centre_in_ball field_differentiable_at_within) lemma analytic_on_open: "open S \ f analytic_on S \ f holomorphic_on S" -apply (auto simp: analytic_imp_holomorphic) -apply (auto simp: analytic_on_def holomorphic_on_def) -by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball) + by (meson analytic_imp_holomorphic analytic_on_def holomorphic_on_subset openE) lemma analytic_on_imp_differentiable_at: "f analytic_on S \ x \ S \ f field_differentiable (at x)" - apply (auto simp: analytic_on_def holomorphic_on_def) -by (metis open_ball centre_in_ball field_differentiable_within_open) + using analytic_on_def holomorphic_on_imp_differentiable_at by auto + +lemma analytic_at_imp_isCont: + assumes "f analytic_on {z}" + shows "isCont f z" + using assms by (meson analytic_on_imp_differentiable_at field_differentiable_imp_continuous_at insertI1) + +lemma analytic_at_neq_imp_eventually_neq: + assumes "f analytic_on {x}" "f x \ c" + shows "eventually (\y. f y \ c) (at x)" +proof (intro tendsto_imp_eventually_ne) + show "f \x\ f x" + using assms by (simp add: analytic_at_imp_isCont isContD) +qed (use assms in auto) lemma analytic_on_subset: "f analytic_on S \ T \ S \ f analytic_on T" by (auto simp: analytic_on_def) @@ -652,15 +662,20 @@ lemma analytic_at_ball: "f analytic_on {z} \ (\e. 0 f holomorphic_on ball z e)" -by (metis analytic_on_def singleton_iff) + by (metis analytic_on_def singleton_iff) lemma analytic_at: - "f analytic_on {z} \ (\s. open s \ z \ s \ f holomorphic_on s)" -by (metis analytic_on_holomorphic empty_subsetI insert_subset) + "f analytic_on {z} \ (\s. open s \ z \ s \ f holomorphic_on s)" + by (metis analytic_on_holomorphic empty_subsetI insert_subset) + +lemma holomorphic_on_imp_analytic_at: + assumes "f holomorphic_on A" "open A" "z \ A" + shows "f analytic_on {z}" + using assms by (meson analytic_at) lemma analytic_on_analytic_at: - "f analytic_on s \ (\z \ s. f analytic_on {z})" -by (metis analytic_at_ball analytic_on_def) + "f analytic_on s \ (\z \ s. f analytic_on {z})" + by (metis analytic_at_ball analytic_on_def) lemma analytic_at_two: "f analytic_on {z} \ g analytic_on {z} \ diff -r 607e1e345e8f -r 69956724ad4f src/HOL/Analysis/Isolated.thy --- a/src/HOL/Analysis/Isolated.thy Wed Feb 08 15:05:24 2023 +0000 +++ b/src/HOL/Analysis/Isolated.thy Thu Feb 09 13:36:25 2023 +0000 @@ -14,6 +14,12 @@ definition (in metric_space) uniform_discrete :: "'a set \ bool" where "uniform_discrete S \ (\e>0. \x\S. \y\S. dist x y < e \ x = y)" +lemma discreteI: "(\x. x \ X \ x isolated_in X ) \ discrete X" + unfolding discrete_def by auto + +lemma discreteD: "discrete X \ x \ X \ x isolated_in X " + unfolding discrete_def by auto + lemma uniformI1: assumes "e>0" "\x y. \x\S;y\S;dist x y \ x =y " shows "uniform_discrete S" @@ -43,6 +49,54 @@ shows "x isolated_in (insert a S) \ x isolated_in S \ (x=a \ \ (x islimpt S))" by (meson insert_iff islimpt_insert isolated_in_islimpt_iff) +lemma isolated_inI: + assumes "x\S" "open T" "T \ S = {x}" + shows "x isolated_in S" + using assms unfolding isolated_in_def by auto + +lemma isolated_inE: + assumes "x isolated_in S" + obtains T where "x \ S" "open T" "T \ S = {x}" + using assms that unfolding isolated_in_def by force + +lemma isolated_inE_dist: + assumes "x isolated_in S" + obtains d where "d > 0" "\y. y \ S \ dist x y < d \ y = x" + by (meson assms isolated_in_dist_Ex_iff) + +lemma isolated_in_altdef: + "x isolated_in S \ (x\S \ eventually (\y. y \ S) (at x))" +proof + assume "x isolated_in S" + from isolated_inE[OF this] + obtain T where "x \ S" and T:"open T" "T \ S = {x}" + by metis + have "\\<^sub>F y in nhds x. y \ T" + apply (rule eventually_nhds_in_open) + using T by auto + then have "eventually (\y. y \ T - {x}) (at x)" + unfolding eventually_at_filter by eventually_elim auto + then have "eventually (\y. y \ S) (at x)" + by eventually_elim (use T in auto) + then show " x \ S \ (\\<^sub>F y in at x. y \ S)" using \x \ S\ by auto +next + assume "x \ S \ (\\<^sub>F y in at x. y \ S)" + then have "\\<^sub>F y in at x. y \ S" "x\S" by auto + from this(1) have "eventually (\y. y \ S \ y = x) (nhds x)" + unfolding eventually_at_filter by eventually_elim auto + then obtain T where T:"open T" "x \ T" "(\y\T. y \ S \ y = x)" + unfolding eventually_nhds by auto + with \x \ S\ have "T \ S = {x}" + by fastforce + with \x\S\ \open T\ + show "x isolated_in S" + unfolding isolated_in_def by auto +qed + +lemma discrete_altdef: + "discrete S \ (\x\S. \\<^sub>F y in at x. y \ S)" + unfolding discrete_def isolated_in_altdef by auto + (* TODO. Other than @@ -194,4 +248,80 @@ ultimately show ?thesis by fastforce qed +definition sparse :: "real \ 'a :: metric_space set \ bool" + where "sparse \ X \ (\x\X. \y\X-{x}. dist x y > \)" + +lemma sparse_empty [simp, intro]: "sparse \ {}" + by (auto simp: sparse_def) + +lemma sparseI [intro?]: + "(\x y. x \ X \ y \ X \ x \ y \ dist x y > \) \ sparse \ X" + unfolding sparse_def by auto + +lemma sparseD: + "sparse \ X \ x \ X \ y \ X \ x \ y \ dist x y > \" + unfolding sparse_def by auto + +lemma sparseD': + "sparse \ X \ x \ X \ y \ X \ dist x y \ \ \ x = y" + unfolding sparse_def by force + +lemma sparse_singleton [simp, intro]: "sparse \ {x}" + by (auto simp: sparse_def) + +definition setdist_gt where "setdist_gt \ X Y \ (\x\X. \y\Y. dist x y > \)" + +lemma setdist_gt_empty [simp]: "setdist_gt \ {} Y" "setdist_gt \ X {}" + by (auto simp: setdist_gt_def) + +lemma setdist_gtI: "(\x y. x \ X \ y \ Y \ dist x y > \) \ setdist_gt \ X Y" + unfolding setdist_gt_def by auto + +lemma setdist_gtD: "setdist_gt \ X Y \ x \ X \ y \ Y \ dist x y > \" + unfolding setdist_gt_def by auto + +lemma setdist_gt_setdist: "\ < setdist A B \ setdist_gt \ A B" + unfolding setdist_gt_def using setdist_le_dist by fastforce + +lemma setdist_gt_mono: "setdist_gt \' A B \ \ \ \' \ A' \ A \ B' \ B \ setdist_gt \ A' B'" + by (force simp: setdist_gt_def) + +lemma setdist_gt_Un_left: "setdist_gt \ (A \ B) C \ setdist_gt \ A C \ setdist_gt \ B C" + by (auto simp: setdist_gt_def) + +lemma setdist_gt_Un_right: "setdist_gt \ C (A \ B) \ setdist_gt \ C A \ setdist_gt \ C B" + by (auto simp: setdist_gt_def) + +lemma compact_closed_imp_eventually_setdist_gt_at_right_0: + assumes "compact A" "closed B" "A \ B = {}" + shows "eventually (\\. setdist_gt \ A B) (at_right 0)" +proof (cases "A = {} \ B = {}") + case False + hence "setdist A B > 0" + by (metis IntI assms empty_iff in_closed_iff_infdist_zero order_less_le setdist_attains_inf setdist_pos_le setdist_sym) + hence "eventually (\\. \ < setdist A B) (at_right 0)" + using eventually_at_right_field by blast + thus ?thesis + by eventually_elim (auto intro: setdist_gt_setdist) +qed auto + +lemma setdist_gt_symI: "setdist_gt \ A B \ setdist_gt \ B A" + by (force simp: setdist_gt_def dist_commute) + +lemma setdist_gt_sym: "setdist_gt \ A B \ setdist_gt \ B A" + by (force simp: setdist_gt_def dist_commute) + +lemma eventually_setdist_gt_at_right_0_mult_iff: + assumes "c > 0" + shows "eventually (\\. setdist_gt (c * \) A B) (at_right 0) \ + eventually (\\. setdist_gt \ A B) (at_right 0)" +proof - + have "eventually (\\. setdist_gt (c * \) A B) (at_right 0) \ + eventually (\\. setdist_gt \ A B) (filtermap ((*) c) (at_right 0))" + by (simp add: eventually_filtermap) + also have "filtermap ((*) c) (at_right 0) = at_right 0" + by (subst filtermap_times_pos_at_right) (use assms in auto) + finally show ?thesis . +qed + end diff -r 607e1e345e8f -r 69956724ad4f src/HOL/Complex_Analysis/Complex_Singularities.thy --- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Wed Feb 08 15:05:24 2023 +0000 +++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Thu Feb 09 13:36:25 2023 +0000 @@ -130,6 +130,84 @@ shows "is_pole (\w. f w / w ^ n) 0" using is_pole_basic[of f A 0] assms by simp +lemma is_pole_compose: + assumes "is_pole f w" "g \z\ w" "eventually (\z. g z \ w) (at z)" + shows "is_pole (\x. f (g x)) z" + using assms(1) unfolding is_pole_def + by (rule filterlim_compose) (use assms in \auto simp: filterlim_at\) + +lemma is_pole_plus_const_iff: + "is_pole f z \ is_pole (\x. f x + c) z" +proof + assume "is_pole f z" + then have "filterlim f at_infinity (at z)" unfolding is_pole_def . + moreover have "((\_. c) \ c) (at z)" by auto + ultimately have " LIM x (at z). f x + c :> at_infinity" + using tendsto_add_filterlim_at_infinity'[of f "at z"] by auto + then show "is_pole (\x. f x + c) z" unfolding is_pole_def . +next + assume "is_pole (\x. f x + c) z" + then have "filterlim (\x. f x + c) at_infinity (at z)" + unfolding is_pole_def . + moreover have "((\_. -c) \ -c) (at z)" by auto + ultimately have " LIM x (at z). f x :> at_infinity" + using tendsto_add_filterlim_at_infinity'[of "(\x. f x + c)" + "at z" "(\_. - c)" "-c"] + by auto + then show "is_pole f z" unfolding is_pole_def . +qed + +lemma is_pole_minus_const_iff: + "is_pole (\x. f x - c) z \ is_pole f z" + using is_pole_plus_const_iff [of f z "-c"] by simp + +lemma is_pole_alt: + "is_pole f x = (\B>0. \U. open U \ x\U \ (\y\U. y\x \ norm (f y)\B))" + unfolding is_pole_def + unfolding filterlim_at_infinity[of 0,simplified] eventually_at_topological + by auto + +lemma is_pole_mult_analytic_nonzero1: + assumes "is_pole g x" "f analytic_on {x}" "f x \ 0" + shows "is_pole (\x. f x * g x) x" + unfolding is_pole_def +proof (rule tendsto_mult_filterlim_at_infinity) + show "f \x\ f x" + using assms by (simp add: analytic_at_imp_isCont isContD) +qed (use assms in \auto simp: is_pole_def\) + +lemma is_pole_mult_analytic_nonzero2: + assumes "is_pole f x" "g analytic_on {x}" "g x \ 0" + shows "is_pole (\x. f x * g x) x" + by (subst mult.commute, rule is_pole_mult_analytic_nonzero1) (use assms in auto) + +lemma is_pole_mult_analytic_nonzero1_iff: + assumes "f analytic_on {x}" "f x \ 0" + shows "is_pole (\x. f x * g x) x \ is_pole g x" +proof + assume "is_pole g x" + thus "is_pole (\x. f x * g x) x" + by (intro is_pole_mult_analytic_nonzero1 assms) +next + assume "is_pole (\x. f x * g x) x" + hence "is_pole (\x. inverse (f x) * (f x * g x)) x" + by (rule is_pole_mult_analytic_nonzero1) + (use assms in \auto intro!: analytic_intros\) + also have "?this \ is_pole g x" + proof (rule is_pole_cong) + have "eventually (\x. f x \ 0) (at x)" + using assms by (simp add: analytic_at_neq_imp_eventually_neq) + thus "eventually (\x. inverse (f x) * (f x * g x) = g x) (at x)" + by eventually_elim auto + qed auto + finally show "is_pole g x" . +qed + +lemma is_pole_mult_analytic_nonzero2_iff: + assumes "g analytic_on {x}" "g x \ 0" + shows "is_pole (\x. f x * g x) x \ is_pole f x" + by (subst mult.commute, rule is_pole_mult_analytic_nonzero1_iff) (fact assms)+ + text \The proposition \<^term>\\x. ((f::complex\complex) \ x) (at z) \ is_pole f z\ can be interpreted as the complex function \<^term>\f\ has a non-essential singularity at \<^term>\z\ @@ -140,6 +218,39 @@ definition isolated_singularity_at::"[complex \ complex, complex] \ bool" where "isolated_singularity_at f z = (\r>0. f analytic_on ball z r-{z})" +lemma not_essential_cong: + assumes "eventually (\x. f x = g x) (at z)" "z = z'" + shows "not_essential f z \ not_essential g z'" + unfolding not_essential_def using assms filterlim_cong is_pole_cong by fastforce + +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'" +proof - + have "isolated_singularity_at g z" + if "isolated_singularity_at f z" "eventually (\x. f x = g x) (at z)" for f g + proof - + from that(1) obtain r where r: "r > 0" "f analytic_on ball z r - {z}" + by (auto simp: isolated_singularity_at_def) + from that(2) obtain r' where r': "r' > 0" "\x\ball z r'-{z}. f x = g x" + unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_commute) + + have "f holomorphic_on ball z r - {z}" + using r(2) by (subst (asm) analytic_on_open) auto + hence "f holomorphic_on ball z (min r r') - {z}" + by (rule holomorphic_on_subset) auto + also have "?this \ g holomorphic_on ball z (min r r') - {z}" + using r' by (intro holomorphic_cong) auto + also have "\ \ g analytic_on ball z (min r r') - {z}" + by (subst analytic_on_open) auto + finally show ?thesis + unfolding isolated_singularity_at_def + by (intro exI[of _ "min r r'"]) (use \r > 0\ \r' > 0\ in auto) + qed + from this[of f g] this[of g f] assms show ?thesis + by (auto simp: eq_commute) +qed + lemma removable_singularity: assumes "f holomorphic_on A - {x}" "open A" assumes "f \x\ c" @@ -795,6 +906,24 @@ using assms unfolding isolated_singularity_at_def by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff) +lemma isolated_singularity_at_altdef: + "isolated_singularity_at f z \ eventually (\z. f analytic_on {z}) (at z)" +proof + assume "isolated_singularity_at f z" + then obtain r where r: "r > 0" "f analytic_on ball z r - {z}" + unfolding isolated_singularity_at_def by blast + have "eventually (\w. w \ ball z r - {z}) (at z)" + using r(1) by (intro eventually_at_in_open) auto + thus "eventually (\z. f analytic_on {z}) (at z)" + by eventually_elim (use r analytic_on_subset in auto) +next + assume "eventually (\z. f analytic_on {z}) (at z)" + then obtain A where A: "open A" "z \ A" "\w. w \ A - {z} \ f analytic_on {w}" + unfolding eventually_at_topological by blast + then show "isolated_singularity_at f z" + by (meson analytic_imp_holomorphic analytic_on_analytic_at isolated_singularity_at_holomorphic) +qed + lemma isolated_singularity_at_shift: assumes "isolated_singularity_at (\x. f (x + w)) z" shows "isolated_singularity_at f (z + w)" @@ -863,6 +992,20 @@ by (auto simp: not_essential_def) qed +lemma not_essential_analytic: + assumes "f analytic_on {z}" + shows "not_essential f z" + using analytic_at assms not_essential_holomorphic by blast + +lemma not_essential_id [singularity_intros]: "not_essential (\w. w) z" + by (simp add: not_essential_analytic) + +lemma is_pole_imp_not_essential [intro]: "is_pole f z \ not_essential f z" + by (auto simp: not_essential_def) + +lemma tendsto_imp_not_essential [intro]: "f \z\ c \ not_essential f z" + by (auto simp: not_essential_def) + lemma eventually_not_pole: assumes "isolated_singularity_at f z" shows "eventually (\w. \is_pole f w) (at z)" @@ -901,7 +1044,18 @@ thus ?thesis by simp qed -subsubsection \The order of non-essential singularities (i.e. removable singularities or poles)\ +lemma isolated_singularity_at_analytic: + assumes "f analytic_on {z}" + shows "isolated_singularity_at f z" +proof - + from assms obtain r where r: "r > 0" "f holomorphic_on ball z r" + by (auto simp: analytic_on_def) + show ?thesis + by (rule isolated_singularity_at_holomorphic[of f "ball z r"]) + (use \r > 0\ in \auto intro!: holomorphic_on_subset[OF r(2)]\) +qed + +subsection \The order of non-essential singularities (i.e. removable singularities or poles)\ definition\<^marker>\tag important\ zorder :: "(complex \ complex) \ complex \ int" where "zorder f z = (THE n. (\h r. r>0 \ h holomorphic_on cball z r \ h z\0 @@ -1658,6 +1812,33 @@ using \z=z'\ unfolding P_def zorder_def zor_poly_def by auto qed +lemma zorder_times_analytic': + assumes "isolated_singularity_at f z" "not_essential f z" + assumes "g analytic_on {z}" "frequently (\z. f z * g z \ 0) (at z)" + shows "zorder (\x. f x * g x) z = zorder f z + zorder g z" +proof (rule zorder_times) + show "isolated_singularity_at g z" "not_essential g z" + by (intro isolated_singularity_at_analytic not_essential_analytic assms)+ +qed (use assms in auto) + +lemma zorder_cmult: + assumes "c \ 0" + shows "zorder (\z. c * f z) z = zorder f z" +proof - + define P where + "P = (\f n h r. 0 < r \ h holomorphic_on cball z r \ + h z \ 0 \ (\w\cball z r - {z}. f w = h w * (w - z) powr of_int n \ h w \ 0))" + have *: "P (\x. c * f x) n (\x. c * h x) r" if "P f n h r" "c \ 0" for f n h r c + using that unfolding P_def by (auto intro!: holomorphic_intros) + have "(\h r. P (\x. c * f x) n h r) \ (\h r. P f n h r)" for n + using *[of f n _ _ c] *[of "\x. c * f x" n _ _ "inverse c"] \c \ 0\ + by (fastforce simp: field_simps) + hence "(THE n. \h r. P (\x. c * f x) n h r) = (THE n. \h r. P f n h r)" + by simp + thus ?thesis + by (simp add: zorder_def P_def) +qed + lemma zorder_nonzero_div_power: assumes sz: "open s" "z \ s" "f holomorphic_on s" "f z \ 0" and "n > 0" shows "zorder (\w. f w / (w - z) ^ n) z = - n" @@ -2269,4 +2450,263 @@ qed qed + +lemma deriv_divide_is_pole: \\Generalises @{thm zorder_deriv}\ + fixes f g::"complex \ complex" and z::complex + assumes f_iso:"isolated_singularity_at f z" + and f_ness:"not_essential f z" + and fg_nconst: "\\<^sub>Fw in (at z). deriv f w * f w \ 0" + and f_ord:"zorder f z \0" + shows "is_pole (\z. deriv f z / f z) z" +proof (rule neg_zorder_imp_is_pole) + define ff where "ff=(\w. deriv f w / f w)" + show "isolated_singularity_at ff z" + using f_iso f_ness unfolding ff_def + by (auto intro:singularity_intros) + show "not_essential ff z" + unfolding ff_def using f_ness f_iso + by (auto intro:singularity_intros) + + have "zorder ff z = zorder (deriv f) z - zorder f z" + unfolding ff_def using f_iso f_ness fg_nconst + apply (rule_tac zorder_divide) + by (auto intro:singularity_intros) + moreover have "zorder (deriv f) z = zorder f z - 1" + proof (rule zorder_deriv_minus_1) + show " \\<^sub>F w in at z. f w \ 0" + using fg_nconst frequently_elim1 by fastforce + qed (use f_iso f_ness f_ord in auto) + ultimately show "zorder ff z < 0" by auto + + show "\\<^sub>F w in at z. ff w \ 0" + unfolding ff_def using fg_nconst by auto +qed + +lemma is_pole_deriv_divide_is_pole: + fixes f g::"complex \ complex" and z::complex + assumes f_iso:"isolated_singularity_at f z" + and "is_pole f z" + shows "is_pole (\z. deriv f z / f z) z" +proof (rule deriv_divide_is_pole[OF f_iso]) + show "not_essential f z" + using \is_pole f z\ unfolding not_essential_def by auto + show "\\<^sub>F w in at z. deriv f w * f w \ 0" + apply (rule isolated_pole_imp_nzero_times) + using assms by auto + show "zorder f z \ 0" + using isolated_pole_imp_neg_zorder assms by fastforce +qed + +subsection \Isolated zeroes\ + +definition isolated_zero :: "(complex \ complex) \ complex \ bool" where + "isolated_zero f z \ f z = 0 \ eventually (\z. f z \ 0) (at z)" + +lemma isolated_zero_altdef: "isolated_zero f z \ f z = 0 \ \z islimpt {z. f z = 0}" + unfolding isolated_zero_def eventually_at_filter eventually_nhds islimpt_def by blast + +lemma isolated_zero_mult1: + assumes "isolated_zero f x" "isolated_zero g x" + shows "isolated_zero (\x. f x * g x) x" +proof - + have "eventually (\x. f x \ 0) (at x)" "eventually (\x. g x \ 0) (at x)" + using assms unfolding isolated_zero_def by auto + hence "eventually (\x. f x * g x \ 0) (at x)" + by eventually_elim auto + with assms show ?thesis + by (auto simp: isolated_zero_def) +qed + +lemma isolated_zero_mult2: + assumes "isolated_zero f x" "g x \ 0" "g analytic_on {x}" + shows "isolated_zero (\x. f x * g x) x" +proof - + have "eventually (\x. f x \ 0) (at x)" + using assms unfolding isolated_zero_def by auto + moreover have "eventually (\x. g x \ 0) (at x)" + using analytic_at_neq_imp_eventually_neq[of g x 0] assms by auto + ultimately have "eventually (\x. f x * g x \ 0) (at x)" + by eventually_elim auto + thus ?thesis + using assms(1) by (auto simp: isolated_zero_def) +qed + +lemma isolated_zero_mult3: + assumes "isolated_zero f x" "g x \ 0" "g analytic_on {x}" + shows "isolated_zero (\x. g x * f x) x" + using isolated_zero_mult2[OF assms] by (simp add: mult_ac) + +lemma isolated_zero_prod: + assumes "\x. x \ I \ isolated_zero (f x) z" "I \ {}" "finite I" + shows "isolated_zero (\y. \x\I. f x y) z" + using assms(3,2,1) by (induction rule: finite_ne_induct) (auto intro: isolated_zero_mult1) + +lemma non_isolated_zero': + assumes "isolated_singularity_at f z" "not_essential f z" "f z = 0" "\isolated_zero f z" + shows "eventually (\z. f z = 0) (at z)" +proof (rule not_essential_frequently_0_imp_eventually_0) + from assms show "frequently (\z. f z = 0) (at z)" + by (auto simp: frequently_def isolated_zero_def) +qed fact+ + +lemma non_isolated_zero: + assumes "\isolated_zero f z" "f analytic_on {z}" "f z = 0" + shows "eventually (\z. f z = 0) (nhds z)" +proof - + have "eventually (\z. f z = 0) (at z)" + by (rule non_isolated_zero') + (use assms in \auto intro: not_essential_analytic isolated_singularity_at_analytic\) + with \f z = 0\ show ?thesis + unfolding eventually_at_filter by (auto elim!: eventually_mono) +qed + +lemma not_essential_compose: + assumes "not_essential f (g z)" "g analytic_on {z}" + shows "not_essential (\x. f (g x)) z" +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) (use assms in \auto intro!: analytic_intros\) + hence "not_essential (\x. f (g x)) z \ not_essential (\_. f (g z)) z" + by (intro not_essential_cong refl) + (auto elim!: eventually_mono simp: eventually_at_filter) + thus ?thesis + by (simp add: not_essential_const) +next + case True + hence ev: "eventually (\w. g w \ g z) (at z)" + by (auto simp: isolated_zero_def) + from assms consider c where "f \g z\ c" | "is_pole f (g z)" + by (auto simp: not_essential_def) + have "isCont g z" + by (rule analytic_at_imp_isCont) fact + hence lim: "g \z\ g z" + using isContD by blast + + from assms(1) consider c where "f \g z\ c" | "is_pole f (g z)" + unfolding not_essential_def by blast + thus ?thesis + proof cases + fix c assume "f \g z\ c" + hence "(\x. f (g x)) \z\ c" + by (rule filterlim_compose) (use lim ev in \auto simp: filterlim_at\) + thus ?thesis + by (auto simp: not_essential_def) + next + assume "is_pole f (g z)" + hence "is_pole (\x. f (g x)) z" + by (rule is_pole_compose) fact+ + thus ?thesis + by (auto simp: not_essential_def) + qed +qed + +subsection \Isolated points\ + +definition isolated_points_of :: "complex set \ complex set" where + "isolated_points_of A = {z\A. eventually (\w. w \ A) (at z)}" + +lemma isolated_points_of_altdef: "isolated_points_of A = {z\A. \z islimpt A}" + unfolding isolated_points_of_def islimpt_def eventually_at_filter eventually_nhds by blast + +lemma isolated_points_of_empty [simp]: "isolated_points_of {} = {}" + and isolated_points_of_UNIV [simp]: "isolated_points_of UNIV = {}" + by (auto simp: isolated_points_of_def) + +lemma isolated_points_of_open_is_empty [simp]: "open A \ isolated_points_of A = {}" + unfolding isolated_points_of_altdef + by (simp add: interior_limit_point interior_open) + +lemma isolated_points_of_subset: "isolated_points_of A \ A" + by (auto simp: isolated_points_of_def) + +lemma isolated_points_of_discrete: + assumes "discrete A" + shows "isolated_points_of A = A" + using assms by (auto simp: isolated_points_of_def discrete_altdef) + +lemmas uniform_discreteI1 = uniformI1 +lemmas uniform_discreteI2 = uniformI2 + +lemma isolated_singularity_at_compose: + assumes "isolated_singularity_at f (g z)" "g analytic_on {z}" + shows "isolated_singularity_at (\x. f (g x)) z" +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) (use assms in \auto intro!: analytic_intros\) + hence "isolated_singularity_at (\x. f (g x)) z \ isolated_singularity_at (\_. f (g z)) z" + by (intro isolated_singularity_at_cong refl) + (auto elim!: eventually_mono simp: eventually_at_filter) + thus ?thesis + by (simp add: isolated_singularity_at_const) +next + case True + from assms(1) obtain r where r: "r > 0" "f analytic_on ball (g z) r - {g z}" + by (auto simp: isolated_singularity_at_def) + hence holo_f: "f holomorphic_on ball (g z) r - {g z}" + by (subst (asm) analytic_on_open) auto + from assms(2) obtain r' where r': "r' > 0" "g holomorphic_on ball z r'" + by (auto simp: analytic_on_def) + + have "continuous_on (ball z r') g" + using holomorphic_on_imp_continuous_on r' by blast + hence "isCont g z" + using r' by (subst (asm) continuous_on_eq_continuous_at) auto + hence "g \z\ g z" + using isContD by blast + hence "eventually (\w. g w \ ball (g z) r) (at z)" + using \r > 0\ unfolding tendsto_def by force + moreover have "eventually (\w. g w \ g z) (at z)" using True + by (auto simp: isolated_zero_def elim!: eventually_mono) + ultimately have "eventually (\w. g w \ ball (g z) r - {g z}) (at z)" + by eventually_elim auto + then obtain r'' where r'': "r'' > 0" "\w\ball z r''-{z}. g w \ ball (g z) r - {g z}" + unfolding eventually_at_filter eventually_nhds_metric ball_def + by (auto simp: dist_commute) + have "f \ g holomorphic_on ball z (min r' r'') - {z}" + proof (rule holomorphic_on_compose_gen) + show "g holomorphic_on ball z (min r' r'') - {z}" + by (rule holomorphic_on_subset[OF r'(2)]) auto + show "f holomorphic_on ball (g z) r - {g z}" + by fact + show "g ` (ball z (min r' r'') - {z}) \ ball (g z) r - {g z}" + using r'' by force + qed + hence "f \ g analytic_on ball z (min r' r'') - {z}" + by (subst analytic_on_open) auto + thus ?thesis using \r' > 0\ \r'' > 0\ + by (auto simp: isolated_singularity_at_def o_def intro!: exI[of _ "min r' r''"]) +qed + +lemma is_pole_power_int_0: + assumes "f analytic_on {x}" "isolated_zero f x" "n < 0" + shows "is_pole (\x. f x powi n) x" +proof - + have "f \x\ f x" + using assms(1) by (simp add: analytic_at_imp_isCont isContD) + with assms show ?thesis + unfolding is_pole_def + by (intro filterlim_power_int_neg_at_infinity) (auto simp: isolated_zero_def) +qed + +lemma isolated_zero_imp_not_constant_on: + assumes "isolated_zero f x" "x \ A" "open A" + shows "\f constant_on A" +proof + assume "f constant_on A" + then obtain c where c: "\x. x \ A \ f x = c" + by (auto simp: constant_on_def) + from assms and c[of x] have [simp]: "c = 0" + by (auto simp: isolated_zero_def) + have "eventually (\x. f x \ 0) (at x)" + using assms by (auto simp: isolated_zero_def) + moreover have "eventually (\x. x \ A) (at x)" + using assms by (intro eventually_at_in_open') auto + ultimately have "eventually (\x. False) (at x)" + by eventually_elim (use c in auto) + thus False + by simp +qed + end