--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Tue Jan 03 19:55:35 2023 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Wed Jan 04 10:27:19 2023 +0000
@@ -536,15 +536,16 @@
qed
moreover have ?thesis when "fn+gn<0"
proof -
- have "LIM w (at z). fp w * gp w / (w-z)^nat (-(fn+gn)) :> at_infinity"
- apply (rule filterlim_divide_at_infinity)
- apply (insert that, auto intro!:tendsto_eq_intros filterlim_atI)
- using eventually_at_topological by blast
+ have "LIM x at z. (x - z) ^ nat (- (fn + gn)) :> at 0"
+ using eventually_at_topological that
+ by (force intro!: tendsto_eq_intros filterlim_atI)
+ moreover have "\<exists>c. (\<lambda>c. fp c * gp c) \<midarrow>z\<rightarrow> c \<and> 0 \<noteq> c"
+ using \<open>fp \<midarrow>z\<rightarrow> fp z\<close> \<open>gp \<midarrow>z\<rightarrow> gp z\<close> tendsto_mult by fastforce
+ ultimately have "LIM w (at z). fp w * gp w / (w-z)^nat (-(fn+gn)) :> at_infinity"
+ using filterlim_divide_at_infinity by blast
then have "is_pole fg z" unfolding is_pole_def
- apply (elim filterlim_transform_within[OF _ _ \<open>r1>0\<close>],simp)
- apply (subst fg_times,simp add:dist_commute)
- apply (subst powr_of_int)
- using that by (auto simp add:field_split_simps)
+ apply (elim filterlim_transform_within[OF _ _ \<open>r1>0\<close>])
+ by (simp_all add: dist_commute fg_times of_int_of_nat powr_minus_divide that)
then show ?thesis unfolding not_essential_def fg_def by auto
qed
ultimately show ?thesis unfolding not_essential_def fg_def by fastforce
@@ -628,12 +629,12 @@
using f_iso unfolding isolated_singularity_at_def by auto
define d3 where "d3=min d1 d2"
have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto
- moreover have "vf analytic_on ball z d3 - {z}"
+ moreover
+ have "f analytic_on ball z d3 - {z}"
+ by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
+ then have "vf analytic_on ball z d3 - {z}"
unfolding vf_def
- apply (rule analytic_on_inverse)
- subgoal using d2 unfolding d3_def by (elim analytic_on_subset) auto
- subgoal for w using d1 unfolding d3_def by (auto simp add:dist_commute)
- done
+ by (intro analytic_on_inverse; simp add: d1(2) d3_def dist_commute)
ultimately show ?thesis unfolding isolated_singularity_at_def vf_def by auto
qed
ultimately show ?thesis by auto
@@ -645,8 +646,7 @@
shows "not_essential (\<lambda>w. f w / g w) z"
proof -
have "not_essential (\<lambda>w. f w * inverse (g w)) z"
- apply (rule not_essential_times[where g="\<lambda>w. inverse (g w)"])
- using assms by (auto intro: isolated_singularity_at_inverse not_essential_inverse)
+ by (simp add: f_iso f_ness g_iso g_ness isolated_singularity_at_inverse not_essential_inverse not_essential_times)
then show ?thesis by (simp add:field_simps)
qed
@@ -664,14 +664,16 @@
define d3 where "d3=min d1 d2"
have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto
+ have fan: "f analytic_on ball z d3 - {z}"
+ by (smt (verit, best) Diff_iff analytic_on_analytic_at d1 d3_def mem_ball)
+ have gan: "g analytic_on ball z d3 - {z}"
+ by (smt (verit, best) Diff_iff analytic_on_analytic_at d2 d3_def mem_ball)
have "(\<lambda>w. f w * g w) analytic_on ball z d3 - {z}"
- apply (rule analytic_on_mult)
- using d1 d2 unfolding d3_def by (auto elim:analytic_on_subset)
+ using analytic_on_mult fan gan by blast
then show "isolated_singularity_at (\<lambda>w. f w * g w) z"
using \<open>d3>0\<close> unfolding isolated_singularity_at_def by auto
have "(\<lambda>w. f w + g w) analytic_on ball z d3 - {z}"
- apply (rule analytic_on_add)
- using d1 d2 unfolding d3_def by (auto elim:analytic_on_subset)
+ using analytic_on_add fan gan by blast
then show "isolated_singularity_at (\<lambda>w. f w + g w) z"
using \<open>d3>0\<close> unfolding isolated_singularity_at_def by auto
qed
@@ -768,7 +770,7 @@
using zorder_exist[OF f_iso f_ness f_nconst,folded fn_def fp_def]
by auto
have fr_inverse: "vf w = (inverse (fp w)) * (w - z) powr (of_int (-fn))"
- and fr_nz: "inverse (fp w)\<noteq>0"
+ and fr_nz: "inverse (fp w) \<noteq> 0"
when "w\<in>ball z fr - {z}" for w
proof -
have "f w = fp w * (w - z) powr of_int fn" "fp w\<noteq>0"
@@ -792,22 +794,20 @@
define r1 where "r1 = min fr vfr"
have "r1>0" using \<open>fr>0\<close> \<open>vfr>0\<close> unfolding r1_def by simp
show "vfn = - fn"
- apply (rule holomorphic_factor_unique[of r1 vfp z "\<lambda>w. inverse (fp w)" vf])
- subgoal using \<open>r1>0\<close> by simp
- subgoal by simp
- subgoal by simp
- subgoal
- proof (rule ballI)
- fix w assume "w \<in> ball z r1 - {z}"
- then have "w \<in> ball z fr - {z}" "w \<in> cball z vfr - {z}" unfolding r1_def by auto
- from fr_inverse[OF this(1)] fr_nz[OF this(1)] vfr(2)[rule_format,OF this(2)]
- show "vf w = vfp w * (w - z) powr of_int vfn \<and> vfp w \<noteq> 0
- \<and> vf w = inverse (fp w) * (w - z) powr of_int (- fn) \<and> inverse (fp w) \<noteq> 0" by auto
- qed
- subgoal using vfr(1) unfolding r1_def by (auto intro!:holomorphic_intros)
- subgoal using fr unfolding r1_def by (auto intro!:holomorphic_intros)
- done
-
+ proof (rule holomorphic_factor_unique)
+ have \<section>: "\<And>w. \<lbrakk>fp w = 0; dist z w < fr\<rbrakk> \<Longrightarrow> False"
+ using fr_nz by force
+ then show "\<forall>w\<in>ball z r1 - {z}.
+ vf w = vfp w * (w - z) powr complex_of_int vfn \<and>
+ vfp w \<noteq> 0 \<and> vf w = inverse (fp w) * (w - z) powr complex_of_int (- fn) \<and>
+ inverse (fp w) \<noteq> 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 "(\<lambda>w. inverse (fp w)) holomorphic_on ball z r1"
+ by (metis \<section> ball_subset_cball fr(1) holomorphic_on_inverse holomorphic_on_subset mem_ball min.cobounded2 min.commute r1_def subset_ball)
+ qed (use \<open>r1>0\<close> in auto)
have "vfp w = inverse (fp w)" when "w\<in>ball z r1-{z}" for w
proof -
have "w \<in> ball z fr - {z}" "w \<in> cball z vfr - {z}" "w\<noteq>z" using that unfolding r1_def by auto
@@ -816,8 +816,7 @@
qed
then show "\<forall>\<^sub>Fw in (at z). vfp w = inverse (fp w)"
unfolding eventually_at using \<open>r1>0\<close>
- 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 "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>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] \<open>g z\<noteq>0\<close> by auto
qed
+ have fz_lim: "f\<midarrow> z \<rightarrow> f z"
+ by (metis assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on)
+ have gz_lim: "g \<midarrow>z\<rightarrow>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\<midarrow> z \<rightarrow> f z"
- by (metis assms(4,6,7) at_within_open continuous_on holo holomorphic_on_imp_continuous_on)
- then have "(\<lambda>w. g w * (w - z) powr of_int n) \<midarrow>z\<rightarrow> f z"
- apply (elim Lim_transform_within_open[where s="ball z r"])
- using r by auto
- moreover have "g \<midarrow>z\<rightarrow>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 "(\<lambda>w. (g w * (w - z) powr of_int n) / g w) \<midarrow>z\<rightarrow> f z/g z"
- apply (rule_tac tendsto_divide)
- using \<open>g z\<noteq>0\<close> by auto
+ have "(\<lambda>w. g w * (w - z) powr of_int n) \<midarrow>z\<rightarrow> f z"
+ using fz_lim Lim_transform_within_open[where s="ball z r"] r by fastforce
+ then have "(\<lambda>w. (g w * (w - z) powr of_int n) / g w) \<midarrow>z\<rightarrow> f z/g z"
+ using gz_lim \<open>g z \<noteq> 0\<close> tendsto_divide by blast
then have powr_tendsto:"(\<lambda>w. (w - z) powr of_int n) \<midarrow>z\<rightarrow> 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\<ge>0" "f z=0"
proof -
have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
- using powr_tendsto
- apply (elim Lim_transform_within[where d=r])
- by (auto simp add: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>)
+ using powr_tendsto Lim_transform_within[where d=r]
+ by (fastforce simp: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>)
then have *:"(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 0" using \<open>f z=0\<close> by simp
moreover have False when "n=0"
proof -
@@ -1015,9 +1009,8 @@
have False when "n>0"
proof -
have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z"
- using powr_tendsto
- apply (elim Lim_transform_within[where d=r])
- by (auto simp add: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>)
+ using powr_tendsto Lim_transform_within[where d=r]
+ by (fastforce simp add: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>)
moreover have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 0"
using \<open>n>0\<close> by (auto intro!:tendsto_eq_intros)
ultimately show False using \<open>f z\<noteq>0\<close> \<open>g z\<noteq>0\<close> using LIM_unique divide_eq_0_iff by blast
@@ -1028,10 +1021,8 @@
proof -
have "(\<lambda>w. inverse ((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> f z/g z"
"(\<lambda>w.((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> 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 "(\<lambda>x. inverse ((x - z) ^ nat (- n)) * (x - z) ^ nat (- n)) \<midarrow>z\<rightarrow> 0" .
then have "(\<lambda>x. 1::complex) \<midarrow>z\<rightarrow> 0"
@@ -1044,7 +1035,7 @@
proof (cases "w=z")
case True
then have "f \<midarrow>z\<rightarrow>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 "(\<lambda>w. g w * (w-z) ^ nat n) \<midarrow>z\<rightarrow>f w"
proof (elim Lim_transform_within[OF _ \<open>r>0\<close>])
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 \<open>x\<noteq>z\<close> by (auto split:if_splits)
+ by (smt (verit) \<open>x \<noteq> z\<close> if_0 powr_of_int right_minus_eq)
finally show "f x = g x * (x - z) ^ nat n" .
qed
moreover have "(\<lambda>w. g w * (w-z) ^ nat n) \<midarrow>z\<rightarrow> 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 \<open>g z\<noteq>0\<close> 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 \<open>\<not> n < 0\<close> by auto
- moreover have "(\<lambda>x. g x * (x - z) ^ nat n) \<midarrow>z\<rightarrow>c"
+ moreover have "(\<lambda>x. g x * (x - z) ^ nat n) \<midarrow>z\<rightarrow> c"
proof (cases "n=0")
case True
then show ?thesis unfolding c_def by simp