3000 hence "f \<midarrow>x\<rightarrow> f x" by (simp add: isCont_def) |
3030 hence "f \<midarrow>x\<rightarrow> f x" by (simp add: isCont_def) |
3001 thus "\<not>is_pole f x" unfolding is_pole_def |
3031 thus "\<not>is_pole f x" unfolding is_pole_def |
3002 using not_tendsto_and_filterlim_at_infinity[of "at x" f "f x"] by auto |
3032 using not_tendsto_and_filterlim_at_infinity[of "at x" f "f x"] by auto |
3003 qed |
3033 qed |
3004 |
3034 |
3005 |
3035 lemma is_pole_inverse_power: "n > 0 \<Longrightarrow> is_pole (\<lambda>z::complex. 1 / (z - a) ^ n) a" |
3006 (*order of the zero of f at z*) |
3036 unfolding is_pole_def inverse_eq_divide [symmetric] |
3007 definition zorder::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> nat" where |
3037 by (intro filterlim_compose[OF filterlim_inverse_at_infinity] tendsto_intros) |
3008 "zorder f z = (THE n. n>0 \<and> (\<exists>h r. r>0 \<and> h holomorphic_on cball z r |
3038 (auto simp: filterlim_at eventually_at intro!: exI[of _ 1] tendsto_eq_intros) |
3009 \<and> (\<forall>w\<in>cball z r. f w = h w * (w-z)^n \<and> h w \<noteq>0)))" |
3039 |
3010 |
3040 lemma is_pole_inverse: "is_pole (\<lambda>z::complex. 1 / (z - a)) a" |
3011 definition zer_poly::"[complex \<Rightarrow> complex,complex]\<Rightarrow>complex \<Rightarrow> complex" where |
3041 using is_pole_inverse_power[of 1 a] by simp |
3012 "zer_poly f z = (SOME h. \<exists>r . r>0 \<and> h holomorphic_on cball z r |
3042 |
3013 \<and> (\<forall>w\<in>cball z r. f w = h w * (w-z)^(zorder f z) \<and> h w \<noteq>0))" |
3043 lemma is_pole_divide: |
3014 |
3044 fixes f :: "'a :: t2_space \<Rightarrow> 'b :: real_normed_field" |
3015 (*order of the pole of f at z*) |
3045 assumes "isCont f z" "filterlim g (at 0) (at z)" "f z \<noteq> 0" |
3016 definition porder::"(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> nat" where |
3046 shows "is_pole (\<lambda>z. f z / g z) z" |
3017 "porder f z = (let f'=(\<lambda>x. if x=z then 0 else inverse (f x)) in zorder f' z)" |
3047 proof - |
3018 |
3048 have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)" |
3019 definition pol_poly::"[complex \<Rightarrow> complex,complex]\<Rightarrow>complex \<Rightarrow> complex" where |
3049 by (intro tendsto_mult_filterlim_at_infinity[of _ "f z"] |
3020 "pol_poly f z = (let f'=(\<lambda> x. if x=z then 0 else inverse (f x)) |
3050 filterlim_compose[OF filterlim_inverse_at_infinity])+ |
3021 in inverse o zer_poly f' z)" |
3051 (insert assms, auto simp: isCont_def) |
3022 |
3052 thus ?thesis by (simp add: divide_simps is_pole_def) |
3023 |
3053 qed |
3024 lemma holomorphic_factor_zero_unique: |
3054 |
3025 fixes f::"complex \<Rightarrow> complex" and z::complex and r::real |
3055 lemma is_pole_basic: |
3026 assumes "r>0" |
3056 assumes "f holomorphic_on A" "open A" "z \<in> A" "f z \<noteq> 0" "n > 0" |
3027 and asm:"\<forall>w\<in>ball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0 \<and> f w = (w - z)^m * h w \<and> h w\<noteq>0" |
3057 shows "is_pole (\<lambda>w. f w / (w - z) ^ n) z" |
|
3058 proof (rule is_pole_divide) |
|
3059 have "continuous_on A f" by (rule holomorphic_on_imp_continuous_on) fact |
|
3060 with assms show "isCont f z" by (auto simp: continuous_on_eq_continuous_at) |
|
3061 have "filterlim (\<lambda>w. (w - z) ^ n) (nhds 0) (at z)" |
|
3062 using assms by (auto intro!: tendsto_eq_intros) |
|
3063 thus "filterlim (\<lambda>w. (w - z) ^ n) (at 0) (at z)" |
|
3064 by (intro filterlim_atI tendsto_eq_intros) |
|
3065 (insert assms, auto simp: eventually_at_filter) |
|
3066 qed fact+ |
|
3067 |
|
3068 lemma is_pole_basic': |
|
3069 assumes "f holomorphic_on A" "open A" "0 \<in> A" "f 0 \<noteq> 0" "n > 0" |
|
3070 shows "is_pole (\<lambda>w. f w / w ^ n) 0" |
|
3071 using is_pole_basic[of f A 0] assms by simp |
|
3072 |
|
3073 text \<open>The proposition |
|
3074 @{term "\<exists>x. ((f::complex\<Rightarrow>complex) \<longlongrightarrow> x) (at z) \<or> is_pole f z"} |
|
3075 can be interpreted as the complex function @{term f} has a non-essential singularity at @{term z} |
|
3076 (i.e. the singularity is either removable or a pole).\<close> |
|
3077 definition not_essential::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where |
|
3078 "not_essential f z = (\<exists>x. f\<midarrow>z\<rightarrow>x \<or> is_pole f z)" |
|
3079 |
|
3080 definition isolated_singularity_at::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where |
|
3081 "isolated_singularity_at f z = (\<exists>r>0. f analytic_on ball z r-{z})" |
|
3082 |
|
3083 named_theorems singularity_intros "introduction rules for singularities" |
|
3084 |
|
3085 lemma holomorphic_factor_unique: |
|
3086 fixes f::"complex \<Rightarrow> complex" and z::complex and r::real and m n::int |
|
3087 assumes "r>0" "g z\<noteq>0" "h z\<noteq>0" |
|
3088 and asm:"\<forall>w\<in>ball z r-{z}. f w = g w * (w-z) powr n \<and> g w\<noteq>0 \<and> f w = h w * (w - z) powr m \<and> h w\<noteq>0" |
3028 and g_holo:"g holomorphic_on ball z r" and h_holo:"h holomorphic_on ball z r" |
3089 and g_holo:"g holomorphic_on ball z r" and h_holo:"h holomorphic_on ball z r" |
3029 shows "n=m" |
3090 shows "n=m" |
3030 proof - |
3091 proof - |
3031 have "n>m \<Longrightarrow> False" |
3092 have [simp]:"at z within ball z r \<noteq> bot" using \<open>r>0\<close> |
|
3093 by (auto simp add:at_within_ball_bot_iff) |
|
3094 have False when "n>m" |
|
3095 proof - |
|
3096 have "(h \<longlongrightarrow> 0) (at z within ball z r)" |
|
3097 proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powr (n - m) * g w"]) |
|
3098 have "\<forall>w\<in>ball z r-{z}. h w = (w-z)powr(n-m) * g w" |
|
3099 using \<open>n>m\<close> asm \<open>r>0\<close> |
|
3100 apply (auto simp add:field_simps powr_diff) |
|
3101 by force |
|
3102 then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> |
|
3103 \<Longrightarrow> (x' - z) powr (n - m) * g x' = h x'" for x' by auto |
|
3104 next |
|
3105 define F where "F \<equiv> at z within ball z r" |
|
3106 define f' where "f' \<equiv> \<lambda>x. (x - z) powr (n-m)" |
|
3107 have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto |
|
3108 moreover have "continuous F f'" unfolding f'_def F_def continuous_def |
|
3109 apply (subst netlimit_within) |
|
3110 using \<open>n>m\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros) |
|
3111 ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def |
|
3112 by (simp add: continuous_within) |
|
3113 moreover have "(g \<longlongrightarrow> g z) F" |
|
3114 using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] \<open>r>0\<close> |
|
3115 unfolding F_def by auto |
|
3116 ultimately show " ((\<lambda>w. f' w * g w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce |
|
3117 qed |
|
3118 moreover have "(h \<longlongrightarrow> h z) (at z within ball z r)" |
|
3119 using holomorphic_on_imp_continuous_on[OF h_holo] |
|
3120 by (auto simp add:continuous_on_def \<open>r>0\<close>) |
|
3121 ultimately have "h z=0" by (auto intro!: tendsto_unique) |
|
3122 thus False using \<open>h z\<noteq>0\<close> by auto |
|
3123 qed |
|
3124 moreover have False when "m>n" |
|
3125 proof - |
|
3126 have "(g \<longlongrightarrow> 0) (at z within ball z r)" |
|
3127 proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) powr (m - n) * h w"]) |
|
3128 have "\<forall>w\<in>ball z r -{z}. g w = (w-z) powr (m-n) * h w" using \<open>m>n\<close> asm |
|
3129 apply (auto simp add:field_simps powr_diff) |
|
3130 by force |
|
3131 then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> |
|
3132 \<Longrightarrow> (x' - z) powr (m - n) * h x' = g x'" for x' by auto |
|
3133 next |
|
3134 define F where "F \<equiv> at z within ball z r" |
|
3135 define f' where "f' \<equiv>\<lambda>x. (x - z) powr (m-n)" |
|
3136 have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto |
|
3137 moreover have "continuous F f'" unfolding f'_def F_def continuous_def |
|
3138 apply (subst netlimit_within) |
|
3139 using \<open>m>n\<close> by (auto intro!:tendsto_powr_complex_0 tendsto_eq_intros) |
|
3140 ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def |
|
3141 by (simp add: continuous_within) |
|
3142 moreover have "(h \<longlongrightarrow> h z) F" |
|
3143 using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] \<open>r>0\<close> |
|
3144 unfolding F_def by auto |
|
3145 ultimately show " ((\<lambda>w. f' w * h w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce |
|
3146 qed |
|
3147 moreover have "(g \<longlongrightarrow> g z) (at z within ball z r)" |
|
3148 using holomorphic_on_imp_continuous_on[OF g_holo] |
|
3149 by (auto simp add:continuous_on_def \<open>r>0\<close>) |
|
3150 ultimately have "g z=0" by (auto intro!: tendsto_unique) |
|
3151 thus False using \<open>g z\<noteq>0\<close> by auto |
|
3152 qed |
|
3153 ultimately show "n=m" by fastforce |
|
3154 qed |
|
3155 |
|
3156 lemma holomorphic_factor_puncture: |
|
3157 assumes f_iso:"isolated_singularity_at f z" |
|
3158 and "not_essential f z" \<comment> \<open>@{term f} has either a removable singularity or a pole at @{term z}\<close> |
|
3159 and non_zero:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" \<comment> \<open>@{term f} will not be constantly zero in a neighbour of @{term z}\<close> |
|
3160 shows "\<exists>!n::int. \<exists>g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0 |
|
3161 \<and> (\<forall>w\<in>cball z r-{z}. f w = g w * (w-z) powr n \<and> g w\<noteq>0)" |
|
3162 proof - |
|
3163 define P where "P = (\<lambda>f n g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0 |
|
3164 \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powr (of_int n) \<and> g w\<noteq>0))" |
|
3165 have imp_unique:"\<exists>!n::int. \<exists>g r. P f n g r" when "\<exists>n g r. P f n g r" |
|
3166 proof (rule ex_ex1I[OF that]) |
|
3167 fix n1 n2 :: int |
|
3168 assume g1_asm:"\<exists>g1 r1. P f n1 g1 r1" and g2_asm:"\<exists>g2 r2. P f n2 g2 r2" |
|
3169 define fac where "fac \<equiv> \<lambda>n g r. \<forall>w\<in>cball z r-{z}. f w = g w * (w - z) powr (of_int n) \<and> g w \<noteq> 0" |
|
3170 obtain g1 r1 where "0 < r1" and g1_holo: "g1 holomorphic_on cball z r1" and "g1 z\<noteq>0" |
|
3171 and "fac n1 g1 r1" using g1_asm unfolding P_def fac_def by auto |
|
3172 obtain g2 r2 where "0 < r2" and g2_holo: "g2 holomorphic_on cball z r2" and "g2 z\<noteq>0" |
|
3173 and "fac n2 g2 r2" using g2_asm unfolding P_def fac_def by auto |
|
3174 define r where "r \<equiv> min r1 r2" |
|
3175 have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto |
|
3176 moreover have "\<forall>w\<in>ball z r-{z}. f w = g1 w * (w-z) powr n1 \<and> g1 w\<noteq>0 |
|
3177 \<and> f w = g2 w * (w - z) powr n2 \<and> g2 w\<noteq>0" |
|
3178 using \<open>fac n1 g1 r1\<close> \<open>fac n2 g2 r2\<close> unfolding fac_def r_def |
|
3179 by fastforce |
|
3180 ultimately show "n1=n2" using g1_holo g2_holo \<open>g1 z\<noteq>0\<close> \<open>g2 z\<noteq>0\<close> |
|
3181 apply (elim holomorphic_factor_unique) |
|
3182 by (auto simp add:r_def) |
|
3183 qed |
|
3184 |
|
3185 have P_exist:"\<exists> n g r. P h n g r" when |
|
3186 "\<exists>z'. (h \<longlongrightarrow> z') (at z)" "isolated_singularity_at h z" "\<exists>\<^sub>Fw in (at z). h w\<noteq>0" |
|
3187 for h |
|
3188 proof - |
|
3189 from that(2) obtain r where "r>0" "h analytic_on ball z r - {z}" |
|
3190 unfolding isolated_singularity_at_def by auto |
|
3191 obtain z' where "(h \<longlongrightarrow> z') (at z)" using \<open>\<exists>z'. (h \<longlongrightarrow> z') (at z)\<close> by auto |
|
3192 define h' where "h'=(\<lambda>x. if x=z then z' else h x)" |
|
3193 have "h' holomorphic_on ball z r" |
|
3194 apply (rule no_isolated_singularity'[of "{z}"]) |
|
3195 subgoal by (metis LIM_equal Lim_at_imp_Lim_at_within \<open>h \<midarrow>z\<rightarrow> z'\<close> empty_iff h'_def insert_iff) |
|
3196 subgoal using \<open>h analytic_on ball z r - {z}\<close> analytic_imp_holomorphic h'_def holomorphic_transform |
|
3197 by fastforce |
|
3198 by auto |
|
3199 have ?thesis when "z'=0" |
|
3200 proof - |
|
3201 have "h' z=0" using that unfolding h'_def by auto |
|
3202 moreover have "\<not> h' constant_on ball z r" |
|
3203 using \<open>\<exists>\<^sub>Fw in (at z). h w\<noteq>0\<close> unfolding constant_on_def frequently_def eventually_at h'_def |
|
3204 apply simp |
|
3205 by (metis \<open>0 < r\<close> centre_in_ball dist_commute mem_ball that) |
|
3206 moreover note \<open>h' holomorphic_on ball z r\<close> |
|
3207 ultimately obtain g r1 n where "0 < n" "0 < r1" "ball z r1 \<subseteq> ball z r" and |
|
3208 g:"g holomorphic_on ball z r1" |
|
3209 "\<And>w. w \<in> ball z r1 \<Longrightarrow> h' w = (w - z) ^ n * g w" |
|
3210 "\<And>w. w \<in> ball z r1 \<Longrightarrow> g w \<noteq> 0" |
|
3211 using holomorphic_factor_zero_nonconstant[of _ "ball z r" z thesis,simplified, |
|
3212 OF \<open>h' holomorphic_on ball z r\<close> \<open>r>0\<close> \<open>h' z=0\<close> \<open>\<not> h' constant_on ball z r\<close>] |
|
3213 by (auto simp add:dist_commute) |
|
3214 define rr where "rr=r1/2" |
|
3215 have "P h' n g rr" |
|
3216 unfolding P_def rr_def |
|
3217 using \<open>n>0\<close> \<open>r1>0\<close> g by (auto simp add:powr_nat) |
|
3218 then have "P h n g rr" |
|
3219 unfolding h'_def P_def by auto |
|
3220 then show ?thesis unfolding P_def by blast |
|
3221 qed |
|
3222 moreover have ?thesis when "z'\<noteq>0" |
3032 proof - |
3223 proof - |
3033 assume "n>m" |
3224 have "h' z\<noteq>0" using that unfolding h'_def by auto |
3034 have "(h \<longlongrightarrow> 0) (at z within ball z r)" |
3225 obtain r1 where "r1>0" "cball z r1 \<subseteq> ball z r" "\<forall>x\<in>cball z r1. h' x\<noteq>0" |
3035 proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) ^ (n - m) * g w"]) |
3226 proof - |
3036 have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> h w = (w-z)^(n-m) * g w" using \<open>n>m\<close> asm |
3227 have "isCont h' z" "h' z\<noteq>0" |
3037 by (auto simp add:field_simps power_diff) |
3228 by (auto simp add: Lim_cong_within \<open>h \<midarrow>z\<rightarrow> z'\<close> \<open>z'\<noteq>0\<close> continuous_at h'_def) |
3038 then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> |
3229 then obtain r2 where r2:"r2>0" "\<forall>x\<in>ball z r2. h' x\<noteq>0" |
3039 \<Longrightarrow> (x' - z) ^ (n - m) * g x' = h x'" for x' by auto |
3230 using continuous_at_avoid[of z h' 0 ] unfolding ball_def by auto |
3040 next |
3231 define r1 where "r1=min r2 r / 2" |
3041 define F where "F \<equiv> at z within ball z r" |
3232 have "0 < r1" "cball z r1 \<subseteq> ball z r" |
3042 define f' where "f' \<equiv> \<lambda>x. (x - z) ^ (n-m)" |
3233 using \<open>r2>0\<close> \<open>r>0\<close> unfolding r1_def by auto |
3043 have "f' z=0" using \<open>n>m\<close> unfolding f'_def by auto |
3234 moreover have "\<forall>x\<in>cball z r1. h' x \<noteq> 0" |
3044 moreover have "continuous F f'" unfolding f'_def F_def |
3235 using r2 unfolding r1_def by simp |
3045 by (intro continuous_intros) |
3236 ultimately show ?thesis using that by auto |
3046 ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def |
3237 qed |
3047 by (simp add: continuous_within) |
3238 then have "P h' 0 h' r1" using \<open>h' holomorphic_on ball z r\<close> unfolding P_def by auto |
3048 moreover have "(g \<longlongrightarrow> g z) F" |
3239 then have "P h 0 h' r1" unfolding P_def h'_def by auto |
3049 using holomorphic_on_imp_continuous_on[OF g_holo,unfolded continuous_on_def] \<open>r>0\<close> |
3240 then show ?thesis unfolding P_def by blast |
3050 unfolding F_def by auto |
3241 qed |
3051 ultimately show " ((\<lambda>w. f' w * g w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce |
3242 ultimately show ?thesis by auto |
3052 qed |
3243 qed |
3053 moreover have "(h \<longlongrightarrow> h z) (at z within ball z r)" |
3244 |
3054 using holomorphic_on_imp_continuous_on[OF h_holo] |
3245 have ?thesis when "\<exists>x. (f \<longlongrightarrow> x) (at z)" |
3055 by (auto simp add:continuous_on_def \<open>r>0\<close>) |
3246 apply (rule_tac imp_unique[unfolded P_def]) |
3056 moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close> |
3247 using P_exist[OF that(1) f_iso non_zero] unfolding P_def . |
3057 by (auto simp add:trivial_limit_within islimpt_ball) |
3248 moreover have ?thesis when "is_pole f z" |
3058 ultimately have "h z=0" by (auto intro: tendsto_unique) |
3249 proof (rule imp_unique[unfolded P_def]) |
3059 thus False using asm \<open>r>0\<close> by auto |
3250 obtain e where [simp]:"e>0" and e_holo:"f holomorphic_on ball z e - {z}" and e_nz: "\<forall>x\<in>ball z e-{z}. f x\<noteq>0" |
3060 qed |
|
3061 moreover have "m>n \<Longrightarrow> False" |
|
3062 proof - |
3251 proof - |
3063 assume "m>n" |
3252 have "\<forall>\<^sub>F z in at z. f z \<noteq> 0" |
3064 have "(g \<longlongrightarrow> 0) (at z within ball z r)" |
3253 using \<open>is_pole f z\<close> filterlim_at_infinity_imp_eventually_ne unfolding is_pole_def |
3065 proof (rule Lim_transform_within[OF _ \<open>r>0\<close>, where f="\<lambda>w. (w - z) ^ (m - n) * h w"]) |
3254 by auto |
3066 have "\<forall>w\<in>ball z r. w\<noteq>z \<longrightarrow> g w = (w-z)^(m-n) * h w" using \<open>m>n\<close> asm |
3255 then obtain e1 where e1:"e1>0" "\<forall>x\<in>ball z e1-{z}. f x\<noteq>0" |
3067 by (auto simp add:field_simps power_diff) |
3256 using that eventually_at[of "\<lambda>x. f x\<noteq>0" z UNIV,simplified] by (auto simp add:dist_commute) |
3068 then show "\<lbrakk>x' \<in> ball z r; 0 < dist x' z;dist x' z < r\<rbrakk> |
3257 obtain e2 where e2:"e2>0" "f holomorphic_on ball z e2 - {z}" |
3069 \<Longrightarrow> (x' - z) ^ (m - n) * h x' = g x'" for x' by auto |
3258 using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by auto |
3070 next |
3259 define e where "e=min e1 e2" |
3071 define F where "F \<equiv> at z within ball z r" |
3260 show ?thesis |
3072 define f' where "f' \<equiv>\<lambda>x. (x - z) ^ (m-n)" |
3261 apply (rule that[of e]) |
3073 have "f' z=0" using \<open>m>n\<close> unfolding f'_def by auto |
3262 using e1 e2 unfolding e_def by auto |
3074 moreover have "continuous F f'" unfolding f'_def F_def |
3263 qed |
3075 by (intro continuous_intros) |
3264 |
3076 ultimately have "(f' \<longlongrightarrow> 0) F" unfolding F_def |
3265 define h where "h \<equiv> \<lambda>x. inverse (f x)" |
3077 by (simp add: continuous_within) |
3266 |
3078 moreover have "(h \<longlongrightarrow> h z) F" |
3267 have "\<exists>n g r. P h n g r" |
3079 using holomorphic_on_imp_continuous_on[OF h_holo,unfolded continuous_on_def] \<open>r>0\<close> |
3268 proof - |
3080 unfolding F_def by auto |
3269 have "h \<midarrow>z\<rightarrow> 0" |
3081 ultimately show " ((\<lambda>w. f' w * h w) \<longlongrightarrow> 0) F" using tendsto_mult by fastforce |
3270 using Lim_transform_within_open assms(2) h_def is_pole_tendsto that by fastforce |
3082 qed |
3271 moreover have "\<exists>\<^sub>Fw in (at z). h w\<noteq>0" |
3083 moreover have "(g \<longlongrightarrow> g z) (at z within ball z r)" |
3272 using non_zero |
3084 using holomorphic_on_imp_continuous_on[OF g_holo] |
3273 apply (elim frequently_rev_mp) |
3085 by (auto simp add:continuous_on_def \<open>r>0\<close>) |
3274 unfolding h_def eventually_at by (auto intro:exI[where x=1]) |
3086 moreover have "at z within ball z r \<noteq> bot" using \<open>r>0\<close> |
3275 moreover have "isolated_singularity_at h z" |
3087 by (auto simp add:trivial_limit_within islimpt_ball) |
3276 unfolding isolated_singularity_at_def h_def |
3088 ultimately have "g z=0" by (auto intro: tendsto_unique) |
3277 apply (rule exI[where x=e]) |
3089 thus False using asm \<open>r>0\<close> by auto |
3278 using e_holo e_nz \<open>e>0\<close> by (metis Topology_Euclidean_Space.open_ball analytic_on_open |
3090 qed |
3279 holomorphic_on_inverse open_delete) |
3091 ultimately show "n=m" by fastforce |
3280 ultimately show ?thesis |
3092 qed |
3281 using P_exist[of h] by auto |
3093 |
3282 qed |
3094 |
3283 then obtain n g r |
3095 lemma holomorphic_factor_zero_Ex1: |
3284 where "0 < r" and |
3096 assumes "open s" "connected s" "z \<in> s" and |
3285 g_holo:"g holomorphic_on cball z r" and "g z\<noteq>0" and |
3097 holf: "f holomorphic_on s" |
3286 g_fac:"(\<forall>w\<in>cball z r-{z}. h w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0)" |
3098 and f: "f z = 0" "\<exists>w\<in>s. f w \<noteq> 0" |
3287 unfolding P_def by auto |
3099 shows "\<exists>!n. \<exists>g r. 0 < n \<and> 0 < r \<and> |
3288 have "P f (-n) (inverse o g) r" |
3100 g holomorphic_on cball z r |
3289 proof - |
3101 \<and> (\<forall>w\<in>cball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0)" |
3290 have "f w = inverse (g w) * (w - z) powr of_int (- n)" when "w\<in>cball z r - {z}" for w |
3102 proof (rule ex_ex1I) |
3291 using g_fac[rule_format,of w] that unfolding h_def |
3103 have "\<not> f constant_on s" |
3292 apply (auto simp add:powr_minus ) |
3104 by (metis \<open>z\<in>s\<close> constant_on_def f) |
3293 by (metis inverse_inverse_eq inverse_mult_distrib) |
3105 then obtain g r n where "0 < n" "0 < r" "ball z r \<subseteq> s" and |
3294 then show ?thesis |
3106 g:"g holomorphic_on ball z r" |
3295 unfolding P_def comp_def |
3107 "\<And>w. w \<in> ball z r \<Longrightarrow> f w = (w - z) ^ n * g w" |
3296 using \<open>r>0\<close> g_holo g_fac \<open>g z\<noteq>0\<close> by (auto intro:holomorphic_intros) |
3108 "\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0" |
3297 qed |
3109 by (blast intro: holomorphic_factor_zero_nonconstant[OF holf \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>]) |
3298 then show "\<exists>x g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z \<noteq> 0 |
3110 define r' where "r' \<equiv> r/2" |
3299 \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powr of_int x \<and> g w \<noteq> 0)" |
3111 have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff) |
3300 unfolding P_def by blast |
3112 hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'" |
3301 qed |
3113 "(\<forall>w\<in>cball z r'. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)" |
3302 ultimately show ?thesis using \<open>not_essential f z\<close> unfolding not_essential_def by presburger |
3114 using g \<open>ball z r \<subseteq> s\<close> by auto |
3303 qed |
3115 moreover have "r'>0" unfolding r'_def using \<open>0<r\<close> by auto |
3304 |
3116 ultimately show "\<exists>n g r. 0 < n \<and> 0 < r \<and> g holomorphic_on cball z r |
3305 lemma not_essential_transform: |
3117 \<and> (\<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)" |
3306 assumes "not_essential g z" |
3118 apply (intro exI[of _ n] exI[of _ g] exI[of _ r']) |
3307 assumes "\<forall>\<^sub>F w in (at z). g w = f w" |
3119 by (simp add:\<open>0 < n\<close>) |
3308 shows "not_essential f z" |
|
3309 using assms unfolding not_essential_def |
|
3310 by (simp add: filterlim_cong is_pole_cong) |
|
3311 |
|
3312 lemma isolated_singularity_at_transform: |
|
3313 assumes "isolated_singularity_at g z" |
|
3314 assumes "\<forall>\<^sub>F w in (at z). g w = f w" |
|
3315 shows "isolated_singularity_at f z" |
|
3316 proof - |
|
3317 obtain r1 where "r1>0" and r1:"g analytic_on ball z r1 - {z}" |
|
3318 using assms(1) unfolding isolated_singularity_at_def by auto |
|
3319 obtain r2 where "r2>0" and r2:" \<forall>x. x \<noteq> z \<and> dist x z < r2 \<longrightarrow> g x = f x" |
|
3320 using assms(2) unfolding eventually_at by auto |
|
3321 define r3 where "r3=min r1 r2" |
|
3322 have "r3>0" unfolding r3_def using \<open>r1>0\<close> \<open>r2>0\<close> by auto |
|
3323 moreover have "f analytic_on ball z r3 - {z}" |
|
3324 proof - |
|
3325 have "g holomorphic_on ball z r3 - {z}" |
|
3326 using r1 unfolding r3_def by (subst (asm) analytic_on_open,auto) |
|
3327 then have "f holomorphic_on ball z r3 - {z}" |
|
3328 using r2 unfolding r3_def |
|
3329 by (auto simp add:dist_commute elim!:holomorphic_transform) |
|
3330 then show ?thesis by (subst analytic_on_open,auto) |
|
3331 qed |
|
3332 ultimately show ?thesis unfolding isolated_singularity_at_def by auto |
|
3333 qed |
|
3334 |
|
3335 lemma not_essential_powr[singularity_intros]: |
|
3336 assumes "LIM w (at z). f w :> (at x)" |
|
3337 shows "not_essential (\<lambda>w. (f w) powr (of_int n)) z" |
|
3338 proof - |
|
3339 define fp where "fp=(\<lambda>w. (f w) powr (of_int n))" |
|
3340 have ?thesis when "n>0" |
|
3341 proof - |
|
3342 have "(\<lambda>w. (f w) ^ (nat n)) \<midarrow>z\<rightarrow> x ^ nat n" |
|
3343 using that assms unfolding filterlim_at by (auto intro!:tendsto_eq_intros) |
|
3344 then have "fp \<midarrow>z\<rightarrow> x ^ nat n" unfolding fp_def |
|
3345 apply (elim Lim_transform_within[where d=1],simp) |
|
3346 by (metis less_le powr_0 powr_of_int that zero_less_nat_eq zero_power) |
|
3347 then show ?thesis unfolding not_essential_def fp_def by auto |
|
3348 qed |
|
3349 moreover have ?thesis when "n=0" |
|
3350 proof - |
|
3351 have "fp \<midarrow>z\<rightarrow> 1 " |
|
3352 apply (subst tendsto_cong[where g="\<lambda>_.1"]) |
|
3353 using that filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def by auto |
|
3354 then show ?thesis unfolding fp_def not_essential_def by auto |
|
3355 qed |
|
3356 moreover have ?thesis when "n<0" |
|
3357 proof (cases "x=0") |
|
3358 case True |
|
3359 have "LIM w (at z). inverse ((f w) ^ (nat (-n))) :> at_infinity" |
|
3360 apply (subst filterlim_inverse_at_iff[symmetric],simp) |
|
3361 apply (rule filterlim_atI) |
|
3362 subgoal using assms True that unfolding filterlim_at by (auto intro!:tendsto_eq_intros) |
|
3363 subgoal using filterlim_at_within_not_equal[OF assms,of 0] |
|
3364 by (eventually_elim,insert that,auto) |
|
3365 done |
|
3366 then have "LIM w (at z). fp w :> at_infinity" |
|
3367 proof (elim filterlim_mono_eventually) |
|
3368 show "\<forall>\<^sub>F x in at z. inverse (f x ^ nat (- n)) = fp x" |
|
3369 using filterlim_at_within_not_equal[OF assms,of 0] unfolding fp_def |
|
3370 apply eventually_elim |
|
3371 using powr_of_int that by auto |
|
3372 qed auto |
|
3373 then show ?thesis unfolding fp_def not_essential_def is_pole_def by auto |
|
3374 next |
|
3375 case False |
|
3376 let ?xx= "inverse (x ^ (nat (-n)))" |
|
3377 have "(\<lambda>w. inverse ((f w) ^ (nat (-n)))) \<midarrow>z\<rightarrow>?xx" |
|
3378 using assms False unfolding filterlim_at by (auto intro!:tendsto_eq_intros) |
|
3379 then have "fp \<midarrow>z\<rightarrow>?xx" |
|
3380 apply (elim Lim_transform_within[where d=1],simp) |
|
3381 unfolding fp_def by (metis inverse_zero nat_mono_iff nat_zero_as_int neg_0_less_iff_less |
|
3382 not_le power_eq_0_iff powr_0 powr_of_int that) |
|
3383 then show ?thesis unfolding fp_def not_essential_def by auto |
|
3384 qed |
|
3385 ultimately show ?thesis by linarith |
|
3386 qed |
|
3387 |
|
3388 lemma isolated_singularity_at_powr[singularity_intros]: |
|
3389 assumes "isolated_singularity_at f z" "\<forall>\<^sub>F w in (at z). f w\<noteq>0" |
|
3390 shows "isolated_singularity_at (\<lambda>w. (f w) powr (of_int n)) z" |
|
3391 proof - |
|
3392 obtain r1 where "r1>0" "f analytic_on ball z r1 - {z}" |
|
3393 using assms(1) unfolding isolated_singularity_at_def by auto |
|
3394 then have r1:"f holomorphic_on ball z r1 - {z}" |
|
3395 using analytic_on_open[of "ball z r1-{z}" f] by blast |
|
3396 obtain r2 where "r2>0" and r2:"\<forall>w. w \<noteq> z \<and> dist w z < r2 \<longrightarrow> f w \<noteq> 0" |
|
3397 using assms(2) unfolding eventually_at by auto |
|
3398 define r3 where "r3=min r1 r2" |
|
3399 have "(\<lambda>w. (f w) powr of_int n) holomorphic_on ball z r3 - {z}" |
|
3400 apply (rule holomorphic_on_powr_of_int) |
|
3401 subgoal unfolding r3_def using r1 by auto |
|
3402 subgoal unfolding r3_def using r2 by (auto simp add:dist_commute) |
|
3403 done |
|
3404 moreover have "r3>0" unfolding r3_def using \<open>0 < r1\<close> \<open>0 < r2\<close> by linarith |
|
3405 ultimately show ?thesis unfolding isolated_singularity_at_def |
|
3406 apply (subst (asm) analytic_on_open[symmetric]) |
|
3407 by auto |
|
3408 qed |
|
3409 |
|
3410 lemma non_zero_neighbour: |
|
3411 assumes f_iso:"isolated_singularity_at f z" |
|
3412 and f_ness:"not_essential f z" |
|
3413 and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" |
|
3414 shows "\<forall>\<^sub>F w in (at z). f w\<noteq>0" |
|
3415 proof - |
|
3416 obtain fn fp fr where [simp]:"fp z \<noteq> 0" and "fr > 0" |
|
3417 and fr: "fp holomorphic_on cball z fr" |
|
3418 "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powr of_int fn \<and> fp w \<noteq> 0" |
|
3419 using holomorphic_factor_puncture[OF f_iso f_ness f_nconst,THEN ex1_implies_ex] by auto |
|
3420 have "f w \<noteq> 0" when " w \<noteq> z" "dist w z < fr" for w |
|
3421 proof - |
|
3422 have "f w = fp w * (w - z) powr of_int fn" "fp w \<noteq> 0" |
|
3423 using fr(2)[rule_format, of w] using that by (auto simp add:dist_commute) |
|
3424 moreover have "(w - z) powr of_int fn \<noteq>0" |
|
3425 unfolding powr_eq_0_iff using \<open>w\<noteq>z\<close> by auto |
|
3426 ultimately show ?thesis by auto |
|
3427 qed |
|
3428 then show ?thesis using \<open>fr>0\<close> unfolding eventually_at by auto |
|
3429 qed |
|
3430 |
|
3431 lemma non_zero_neighbour_pole: |
|
3432 assumes "is_pole f z" |
|
3433 shows "\<forall>\<^sub>F w in (at z). f w\<noteq>0" |
|
3434 using assms filterlim_at_infinity_imp_eventually_ne[of f "at z" 0] |
|
3435 unfolding is_pole_def by auto |
|
3436 |
|
3437 lemma non_zero_neighbour_alt: |
|
3438 assumes holo: "f holomorphic_on S" |
|
3439 and "open S" "connected S" "z \<in> S" "\<beta> \<in> S" "f \<beta> \<noteq> 0" |
|
3440 shows "\<forall>\<^sub>F w in (at z). f w\<noteq>0 \<and> w\<in>S" |
|
3441 proof (cases "f z = 0") |
|
3442 case True |
|
3443 from isolated_zeros[OF holo \<open>open S\<close> \<open>connected S\<close> \<open>z \<in> S\<close> True \<open>\<beta> \<in> S\<close> \<open>f \<beta> \<noteq> 0\<close>] |
|
3444 obtain r where "0 < r" "ball z r \<subseteq> S" "\<forall>w \<in> ball z r - {z}.f w \<noteq> 0" by metis |
|
3445 then show ?thesis unfolding eventually_at |
|
3446 apply (rule_tac x=r in exI) |
|
3447 by (auto simp add:dist_commute) |
3120 next |
3448 next |
3121 fix m n |
3449 case False |
3122 define fac where "fac \<equiv> \<lambda>n g r. \<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0" |
3450 obtain r1 where r1:"r1>0" "\<forall>y. dist z y < r1 \<longrightarrow> f y \<noteq> 0" |
3123 assume n_asm:"\<exists>g r1. 0 < n \<and> 0 < r1 \<and> g holomorphic_on cball z r1 \<and> fac n g r1" |
3451 using continuous_at_avoid[of z f, OF _ False] assms(2,4) continuous_on_eq_continuous_at |
3124 and m_asm:"\<exists>h r2. 0 < m \<and> 0 < r2 \<and> h holomorphic_on cball z r2 \<and> fac m h r2" |
3452 holo holomorphic_on_imp_continuous_on by blast |
3125 obtain g r1 where "0 < n" "0 < r1" and g_holo: "g holomorphic_on cball z r1" |
3453 obtain r2 where r2:"r2>0" "ball z r2 \<subseteq> S" |
3126 and "fac n g r1" using n_asm by auto |
3454 using assms(2) assms(4) openE by blast |
3127 obtain h r2 where "0 < m" "0 < r2" and h_holo: "h holomorphic_on cball z r2" |
3455 show ?thesis unfolding eventually_at |
3128 and "fac m h r2" using m_asm by auto |
3456 apply (rule_tac x="min r1 r2" in exI) |
3129 define r where "r \<equiv> min r1 r2" |
3457 using r1 r2 by (auto simp add:dist_commute) |
3130 have "r>0" using \<open>r1>0\<close> \<open>r2>0\<close> unfolding r_def by auto |
3458 qed |
3131 moreover have "\<forall>w\<in>ball z r. f w = (w-z)^n * g w \<and> g w\<noteq>0 \<and> f w = (w - z)^m * h w \<and> h w\<noteq>0" |
3459 |
3132 using \<open>fac m h r2\<close> \<open>fac n g r1\<close> unfolding fac_def r_def |
3460 lemma not_essential_times[singularity_intros]: |
3133 by fastforce |
3461 assumes f_ness:"not_essential f z" and g_ness:"not_essential g z" |
3134 ultimately show "m=n" using g_holo h_holo |
3462 assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z" |
3135 apply (elim holomorphic_factor_zero_unique[of r z f n g m h,symmetric,rotated]) |
3463 shows "not_essential (\<lambda>w. f w * g w) z" |
3136 by (auto simp add:r_def) |
3464 proof - |
3137 qed |
3465 define fg where "fg = (\<lambda>w. f w * g w)" |
|
3466 have ?thesis when "\<not> ((\<exists>\<^sub>Fw in (at z). f w\<noteq>0) \<and> (\<exists>\<^sub>Fw in (at z). g w\<noteq>0))" |
|
3467 proof - |
|
3468 have "\<forall>\<^sub>Fw in (at z). fg w=0" |
|
3469 using that[unfolded frequently_def, simplified] unfolding fg_def |
|
3470 by (auto elim: eventually_rev_mp) |
|
3471 from tendsto_cong[OF this] have "fg \<midarrow>z\<rightarrow>0" by auto |
|
3472 then show ?thesis unfolding not_essential_def fg_def by auto |
|
3473 qed |
|
3474 moreover have ?thesis when f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" and g_nconst:"\<exists>\<^sub>Fw in (at z). g w\<noteq>0" |
|
3475 proof - |
|
3476 obtain fn fp fr where [simp]:"fp z \<noteq> 0" and "fr > 0" |
|
3477 and fr: "fp holomorphic_on cball z fr" |
|
3478 "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powr of_int fn \<and> fp w \<noteq> 0" |
|
3479 using holomorphic_factor_puncture[OF f_iso f_ness f_nconst,THEN ex1_implies_ex] by auto |
|
3480 obtain gn gp gr where [simp]:"gp z \<noteq> 0" and "gr > 0" |
|
3481 and gr: "gp holomorphic_on cball z gr" |
|
3482 "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w - z) powr of_int gn \<and> gp w \<noteq> 0" |
|
3483 using holomorphic_factor_puncture[OF g_iso g_ness g_nconst,THEN ex1_implies_ex] by auto |
|
3484 |
|
3485 define r1 where "r1=(min fr gr)" |
|
3486 have "r1>0" unfolding r1_def using \<open>fr>0\<close> \<open>gr>0\<close> by auto |
|
3487 have fg_times:"fg w = (fp w * gp w) * (w - z) powr (of_int (fn+gn))" and fgp_nz:"fp w*gp w\<noteq>0" |
|
3488 when "w\<in>ball z r1 - {z}" for w |
|
3489 proof - |
|
3490 have "f w = fp w * (w - z) powr of_int fn" "fp w\<noteq>0" |
|
3491 using fr(2)[rule_format,of w] that unfolding r1_def by auto |
|
3492 moreover have "g w = gp w * (w - z) powr of_int gn" "gp w \<noteq> 0" |
|
3493 using gr(2)[rule_format, of w] that unfolding r1_def by auto |
|
3494 ultimately show "fg w = (fp w * gp w) * (w - z) powr (of_int (fn+gn))" "fp w*gp w\<noteq>0" |
|
3495 unfolding fg_def by (auto simp add:powr_add) |
|
3496 qed |
|
3497 |
|
3498 have [intro]: "fp \<midarrow>z\<rightarrow>fp z" "gp \<midarrow>z\<rightarrow>gp z" |
|
3499 using fr(1) \<open>fr>0\<close> gr(1) \<open>gr>0\<close> |
|
3500 by (meson Topology_Euclidean_Space.open_ball ball_subset_cball centre_in_ball |
|
3501 continuous_on_eq_continuous_at continuous_within holomorphic_on_imp_continuous_on |
|
3502 holomorphic_on_subset)+ |
|
3503 have ?thesis when "fn+gn>0" |
|
3504 proof - |
|
3505 have "(\<lambda>w. (fp w * gp w) * (w - z) ^ (nat (fn+gn))) \<midarrow>z\<rightarrow>0" |
|
3506 using that by (auto intro!:tendsto_eq_intros) |
|
3507 then have "fg \<midarrow>z\<rightarrow> 0" |
|
3508 apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>]) |
|
3509 by (metis (no_types, hide_lams) Diff_iff cball_trivial dist_commute dist_self |
|
3510 eq_iff_diff_eq_0 fg_times less_le linorder_not_le mem_ball mem_cball powr_of_int |
|
3511 that) |
|
3512 then show ?thesis unfolding not_essential_def fg_def by auto |
|
3513 qed |
|
3514 moreover have ?thesis when "fn+gn=0" |
|
3515 proof - |
|
3516 have "(\<lambda>w. fp w * gp w) \<midarrow>z\<rightarrow>fp z*gp z" |
|
3517 using that by (auto intro!:tendsto_eq_intros) |
|
3518 then have "fg \<midarrow>z\<rightarrow> fp z*gp z" |
|
3519 apply (elim Lim_transform_within[OF _ \<open>r1>0\<close>]) |
|
3520 apply (subst fg_times) |
|
3521 by (auto simp add:dist_commute that) |
|
3522 then show ?thesis unfolding not_essential_def fg_def by auto |
|
3523 qed |
|
3524 moreover have ?thesis when "fn+gn<0" |
|
3525 proof - |
|
3526 have "LIM w (at z). fp w * gp w / (w-z)^nat (-(fn+gn)) :> at_infinity" |
|
3527 apply (rule filterlim_divide_at_infinity) |
|
3528 apply (insert that, auto intro!:tendsto_eq_intros filterlim_atI) |
|
3529 using eventually_at_topological by blast |
|
3530 then have "is_pole fg z" unfolding is_pole_def |
|
3531 apply (elim filterlim_transform_within[OF _ _ \<open>r1>0\<close>],simp) |
|
3532 apply (subst fg_times,simp add:dist_commute) |
|
3533 apply (subst powr_of_int) |
|
3534 using that by (auto simp add:divide_simps) |
|
3535 then show ?thesis unfolding not_essential_def fg_def by auto |
|
3536 qed |
|
3537 ultimately show ?thesis unfolding not_essential_def fg_def by fastforce |
|
3538 qed |
|
3539 ultimately show ?thesis by auto |
|
3540 qed |
|
3541 |
|
3542 lemma not_essential_inverse[singularity_intros]: |
|
3543 assumes f_ness:"not_essential f z" |
|
3544 assumes f_iso:"isolated_singularity_at f z" |
|
3545 shows "not_essential (\<lambda>w. inverse (f w)) z" |
|
3546 proof - |
|
3547 define vf where "vf = (\<lambda>w. inverse (f w))" |
|
3548 have ?thesis when "\<not>(\<exists>\<^sub>Fw in (at z). f w\<noteq>0)" |
|
3549 proof - |
|
3550 have "\<forall>\<^sub>Fw in (at z). f w=0" |
|
3551 using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp) |
|
3552 then have "\<forall>\<^sub>Fw in (at z). vf w=0" |
|
3553 unfolding vf_def by auto |
|
3554 from tendsto_cong[OF this] have "vf \<midarrow>z\<rightarrow>0" unfolding vf_def by auto |
|
3555 then show ?thesis unfolding not_essential_def vf_def by auto |
|
3556 qed |
|
3557 moreover have ?thesis when "is_pole f z" |
|
3558 proof - |
|
3559 have "vf \<midarrow>z\<rightarrow>0" |
|
3560 using that filterlim_at filterlim_inverse_at_iff unfolding is_pole_def vf_def by blast |
|
3561 then show ?thesis unfolding not_essential_def vf_def by auto |
|
3562 qed |
|
3563 moreover have ?thesis when "\<exists>x. f\<midarrow>z\<rightarrow>x " and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" |
|
3564 proof - |
|
3565 from that obtain fz where fz:"f\<midarrow>z\<rightarrow>fz" by auto |
|
3566 have ?thesis when "fz=0" |
|
3567 proof - |
|
3568 have "(\<lambda>w. inverse (vf w)) \<midarrow>z\<rightarrow>0" |
|
3569 using fz that unfolding vf_def by auto |
|
3570 moreover have "\<forall>\<^sub>F w in at z. inverse (vf w) \<noteq> 0" |
|
3571 using non_zero_neighbour[OF f_iso f_ness f_nconst] |
|
3572 unfolding vf_def by auto |
|
3573 ultimately have "is_pole vf z" |
|
3574 using filterlim_inverse_at_iff[of vf "at z"] unfolding filterlim_at is_pole_def by auto |
|
3575 then show ?thesis unfolding not_essential_def vf_def by auto |
|
3576 qed |
|
3577 moreover have ?thesis when "fz\<noteq>0" |
|
3578 proof - |
|
3579 have "vf \<midarrow>z\<rightarrow>inverse fz" |
|
3580 using fz that unfolding vf_def by (auto intro:tendsto_eq_intros) |
|
3581 then show ?thesis unfolding not_essential_def vf_def by auto |
|
3582 qed |
|
3583 ultimately show ?thesis by auto |
|
3584 qed |
|
3585 ultimately show ?thesis using f_ness unfolding not_essential_def by auto |
|
3586 qed |
|
3587 |
|
3588 lemma isolated_singularity_at_inverse[singularity_intros]: |
|
3589 assumes f_iso:"isolated_singularity_at f z" |
|
3590 and f_ness:"not_essential f z" |
|
3591 shows "isolated_singularity_at (\<lambda>w. inverse (f w)) z" |
|
3592 proof - |
|
3593 define vf where "vf = (\<lambda>w. inverse (f w))" |
|
3594 have ?thesis when "\<not>(\<exists>\<^sub>Fw in (at z). f w\<noteq>0)" |
|
3595 proof - |
|
3596 have "\<forall>\<^sub>Fw in (at z). f w=0" |
|
3597 using that[unfolded frequently_def, simplified] by (auto elim: eventually_rev_mp) |
|
3598 then have "\<forall>\<^sub>Fw in (at z). vf w=0" |
|
3599 unfolding vf_def by auto |
|
3600 then obtain d1 where "d1>0" and d1:"\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> vf x = 0" |
|
3601 unfolding eventually_at by auto |
|
3602 then have "vf holomorphic_on ball z d1-{z}" |
|
3603 apply (rule_tac holomorphic_transform[of "\<lambda>_. 0"]) |
|
3604 by (auto simp add:dist_commute) |
|
3605 then have "vf analytic_on ball z d1 - {z}" |
|
3606 by (simp add: analytic_on_open open_delete) |
|
3607 then show ?thesis using \<open>d1>0\<close> unfolding isolated_singularity_at_def vf_def by auto |
|
3608 qed |
|
3609 moreover have ?thesis when f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" |
|
3610 proof - |
|
3611 have "\<forall>\<^sub>F w in at z. f w \<noteq> 0" using non_zero_neighbour[OF f_iso f_ness f_nconst] . |
|
3612 then obtain d1 where d1:"d1>0" "\<forall>x. x \<noteq> z \<and> dist x z < d1 \<longrightarrow> f x \<noteq> 0" |
|
3613 unfolding eventually_at by auto |
|
3614 obtain d2 where "d2>0" and d2:"f analytic_on ball z d2 - {z}" |
|
3615 using f_iso unfolding isolated_singularity_at_def by auto |
|
3616 define d3 where "d3=min d1 d2" |
|
3617 have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto |
|
3618 moreover have "vf analytic_on ball z d3 - {z}" |
|
3619 unfolding vf_def |
|
3620 apply (rule analytic_on_inverse) |
|
3621 subgoal using d2 unfolding d3_def by (elim analytic_on_subset) auto |
|
3622 subgoal for w using d1 unfolding d3_def by (auto simp add:dist_commute) |
|
3623 done |
|
3624 ultimately show ?thesis unfolding isolated_singularity_at_def vf_def by auto |
|
3625 qed |
|
3626 ultimately show ?thesis by auto |
|
3627 qed |
|
3628 |
|
3629 lemma not_essential_divide[singularity_intros]: |
|
3630 assumes f_ness:"not_essential f z" and g_ness:"not_essential g z" |
|
3631 assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z" |
|
3632 shows "not_essential (\<lambda>w. f w / g w) z" |
|
3633 proof - |
|
3634 have "not_essential (\<lambda>w. f w * inverse (g w)) z" |
|
3635 apply (rule not_essential_times[where g="\<lambda>w. inverse (g w)"]) |
|
3636 using assms by (auto intro: isolated_singularity_at_inverse not_essential_inverse) |
|
3637 then show ?thesis by (simp add:field_simps) |
|
3638 qed |
|
3639 |
|
3640 lemma |
|
3641 assumes f_iso:"isolated_singularity_at f z" |
|
3642 and g_iso:"isolated_singularity_at g z" |
|
3643 shows isolated_singularity_at_times[singularity_intros]: |
|
3644 "isolated_singularity_at (\<lambda>w. f w * g w) z" and |
|
3645 isolated_singularity_at_add[singularity_intros]: |
|
3646 "isolated_singularity_at (\<lambda>w. f w + g w) z" |
|
3647 proof - |
|
3648 obtain d1 d2 where "d1>0" "d2>0" |
|
3649 and d1:"f analytic_on ball z d1 - {z}" and d2:"g analytic_on ball z d2 - {z}" |
|
3650 using f_iso g_iso unfolding isolated_singularity_at_def by auto |
|
3651 define d3 where "d3=min d1 d2" |
|
3652 have "d3>0" unfolding d3_def using \<open>d1>0\<close> \<open>d2>0\<close> by auto |
|
3653 |
|
3654 have "(\<lambda>w. f w * g w) analytic_on ball z d3 - {z}" |
|
3655 apply (rule analytic_on_mult) |
|
3656 using d1 d2 unfolding d3_def by (auto elim:analytic_on_subset) |
|
3657 then show "isolated_singularity_at (\<lambda>w. f w * g w) z" |
|
3658 using \<open>d3>0\<close> unfolding isolated_singularity_at_def by auto |
|
3659 have "(\<lambda>w. f w + g w) analytic_on ball z d3 - {z}" |
|
3660 apply (rule analytic_on_add) |
|
3661 using d1 d2 unfolding d3_def by (auto elim:analytic_on_subset) |
|
3662 then show "isolated_singularity_at (\<lambda>w. f w + g w) z" |
|
3663 using \<open>d3>0\<close> unfolding isolated_singularity_at_def by auto |
|
3664 qed |
|
3665 |
|
3666 lemma isolated_singularity_at_uminus[singularity_intros]: |
|
3667 assumes f_iso:"isolated_singularity_at f z" |
|
3668 shows "isolated_singularity_at (\<lambda>w. - f w) z" |
|
3669 using assms unfolding isolated_singularity_at_def using analytic_on_neg by blast |
|
3670 |
|
3671 lemma isolated_singularity_at_id[singularity_intros]: |
|
3672 "isolated_singularity_at (\<lambda>w. w) z" |
|
3673 unfolding isolated_singularity_at_def by (simp add: gt_ex) |
|
3674 |
|
3675 lemma isolated_singularity_at_minus[singularity_intros]: |
|
3676 assumes f_iso:"isolated_singularity_at f z" |
|
3677 and g_iso:"isolated_singularity_at g z" |
|
3678 shows "isolated_singularity_at (\<lambda>w. f w - g w) z" |
|
3679 using isolated_singularity_at_uminus[THEN isolated_singularity_at_add[OF f_iso,of "\<lambda>w. - g w"] |
|
3680 ,OF g_iso] by simp |
|
3681 |
|
3682 lemma isolated_singularity_at_divide[singularity_intros]: |
|
3683 assumes f_iso:"isolated_singularity_at f z" |
|
3684 and g_iso:"isolated_singularity_at g z" |
|
3685 and g_ness:"not_essential g z" |
|
3686 shows "isolated_singularity_at (\<lambda>w. f w / g w) z" |
|
3687 using isolated_singularity_at_inverse[THEN isolated_singularity_at_times[OF f_iso, |
|
3688 of "\<lambda>w. inverse (g w)"],OF g_iso g_ness] by (simp add:field_simps) |
|
3689 |
|
3690 lemma isolated_singularity_at_const[singularity_intros]: |
|
3691 "isolated_singularity_at (\<lambda>w. c) z" |
|
3692 unfolding isolated_singularity_at_def by (simp add: gt_ex) |
|
3693 |
|
3694 lemma isolated_singularity_at_holomorphic: |
|
3695 assumes "f holomorphic_on s-{z}" "open s" "z\<in>s" |
|
3696 shows "isolated_singularity_at f z" |
|
3697 using assms unfolding isolated_singularity_at_def |
|
3698 by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff) |
|
3699 |
|
3700 subsubsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close> |
|
3701 |
|
3702 definition zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where |
|
3703 "zorder f z = (THE n. (\<exists>h r. r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0 |
|
3704 \<and> (\<forall>w\<in>cball z r - {z}. f w = h w * (w-z) powr (of_int n) \<and> h w \<noteq>0)))" |
|
3705 |
|
3706 definition zor_poly::"[complex \<Rightarrow> complex,complex]\<Rightarrow>complex \<Rightarrow> complex" where |
|
3707 "zor_poly f z = (SOME h. \<exists>r . r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0 |
|
3708 \<and> (\<forall>w\<in>cball z r-{z}. f w = h w * (w-z) powr (zorder f z) \<and> h w \<noteq>0))" |
3138 |
3709 |
3139 lemma zorder_exist: |
3710 lemma zorder_exist: |
3140 fixes f::"complex \<Rightarrow> complex" and z::complex |
3711 fixes f::"complex \<Rightarrow> complex" and z::complex |
3141 defines "n\<equiv>zorder f z" and "h\<equiv>zer_poly f z" |
3712 defines "n\<equiv>zorder f z" and "g\<equiv>zor_poly f z" |
3142 assumes "open s" "connected s" "z\<in>s" |
3713 assumes f_iso:"isolated_singularity_at f z" |
3143 and holo: "f holomorphic_on s" |
3714 and f_ness:"not_essential f z" |
3144 and "f z=0" "\<exists>w\<in>s. f w\<noteq>0" |
3715 and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" |
3145 shows "\<exists>r. n>0 \<and> r>0 \<and> cball z r \<subseteq> s \<and> h holomorphic_on cball z r |
3716 shows "g z\<noteq>0 \<and> (\<exists>r. r>0 \<and> g holomorphic_on cball z r |
3146 \<and> (\<forall>w\<in>cball z r. f w = h w * (w-z)^n \<and> h w \<noteq>0) " |
3717 \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powr n \<and> g w \<noteq>0))" |
3147 proof - |
3718 proof - |
3148 define P where "P \<equiv> \<lambda>h r n. r>0 \<and> h holomorphic_on cball z r |
3719 define P where "P = (\<lambda>n g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0 |
3149 \<and> (\<forall>w\<in>cball z r. ( f w = h w * (w-z)^n) \<and> h w \<noteq>0)" |
3720 \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powr (of_int n) \<and> g w\<noteq>0))" |
3150 have "(\<exists>!n. n>0 \<and> (\<exists> h r. P h r n))" |
3721 have "\<exists>!n. \<exists>g r. P n g r" |
|
3722 using holomorphic_factor_puncture[OF assms(3-)] unfolding P_def by auto |
|
3723 then have "\<exists>g r. P n g r" |
|
3724 unfolding n_def P_def zorder_def |
|
3725 by (drule_tac theI',argo) |
|
3726 then have "\<exists>r. P n g r" |
|
3727 unfolding P_def zor_poly_def g_def n_def |
|
3728 by (drule_tac someI_ex,argo) |
|
3729 then obtain r1 where "P n g r1" by auto |
|
3730 then show ?thesis unfolding P_def by auto |
|
3731 qed |
|
3732 |
|
3733 lemma |
|
3734 fixes f::"complex \<Rightarrow> complex" and z::complex |
|
3735 assumes f_iso:"isolated_singularity_at f z" |
|
3736 and f_ness:"not_essential f z" |
|
3737 and f_nconst:"\<exists>\<^sub>Fw in (at z). f w\<noteq>0" |
|
3738 shows zorder_inverse: "zorder (\<lambda>w. inverse (f w)) z = - zorder f z" |
|
3739 and zor_poly_inverse: "\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. inverse (f w)) z w |
|
3740 = inverse (zor_poly f z w)" |
|
3741 proof - |
|
3742 define vf where "vf = (\<lambda>w. inverse (f w))" |
|
3743 define fn vfn where |
|
3744 "fn = zorder f z" and "vfn = zorder vf z" |
|
3745 define fp vfp where |
|
3746 "fp = zor_poly f z" and "vfp = zor_poly vf z" |
|
3747 |
|
3748 obtain fr where [simp]:"fp z \<noteq> 0" and "fr > 0" |
|
3749 and fr: "fp holomorphic_on cball z fr" |
|
3750 "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powr of_int fn \<and> fp w \<noteq> 0" |
|
3751 using zorder_exist[OF f_iso f_ness f_nconst,folded fn_def fp_def] |
|
3752 by auto |
|
3753 have fr_inverse: "vf w = (inverse (fp w)) * (w - z) powr (of_int (-fn))" |
|
3754 and fr_nz: "inverse (fp w)\<noteq>0" |
|
3755 when "w\<in>ball z fr - {z}" for w |
|
3756 proof - |
|
3757 have "f w = fp w * (w - z) powr of_int fn" "fp w\<noteq>0" |
|
3758 using fr(2)[rule_format,of w] that by auto |
|
3759 then show "vf w = (inverse (fp w)) * (w - z) powr (of_int (-fn))" "inverse (fp w)\<noteq>0" |
|
3760 unfolding vf_def by (auto simp add:powr_minus) |
|
3761 qed |
|
3762 obtain vfr where [simp]:"vfp z \<noteq> 0" and "vfr>0" and vfr:"vfp holomorphic_on cball z vfr" |
|
3763 "(\<forall>w\<in>cball z vfr - {z}. vf w = vfp w * (w - z) powr of_int vfn \<and> vfp w \<noteq> 0)" |
|
3764 proof - |
|
3765 have "isolated_singularity_at vf z" |
|
3766 using isolated_singularity_at_inverse[OF f_iso f_ness] unfolding vf_def . |
|
3767 moreover have "not_essential vf z" |
|
3768 using not_essential_inverse[OF f_ness f_iso] unfolding vf_def . |
|
3769 moreover have "\<exists>\<^sub>F w in at z. vf w \<noteq> 0" |
|
3770 using f_nconst unfolding vf_def by (auto elim:frequently_elim1) |
|
3771 ultimately show ?thesis using zorder_exist[of vf z, folded vfn_def vfp_def] that by auto |
|
3772 qed |
|
3773 |
|
3774 |
|
3775 define r1 where "r1 = min fr vfr" |
|
3776 have "r1>0" using \<open>fr>0\<close> \<open>vfr>0\<close> unfolding r1_def by simp |
|
3777 show "vfn = - fn" |
|
3778 apply (rule holomorphic_factor_unique[of r1 vfp z "\<lambda>w. inverse (fp w)" vf]) |
|
3779 subgoal using \<open>r1>0\<close> by simp |
|
3780 subgoal by simp |
|
3781 subgoal by simp |
|
3782 subgoal |
|
3783 proof (rule ballI) |
|
3784 fix w assume "w \<in> ball z r1 - {z}" |
|
3785 then have "w \<in> ball z fr - {z}" "w \<in> cball z vfr - {z}" unfolding r1_def by auto |
|
3786 from fr_inverse[OF this(1)] fr_nz[OF this(1)] vfr(2)[rule_format,OF this(2)] |
|
3787 show "vf w = vfp w * (w - z) powr of_int vfn \<and> vfp w \<noteq> 0 |
|
3788 \<and> vf w = inverse (fp w) * (w - z) powr of_int (- fn) \<and> inverse (fp w) \<noteq> 0" by auto |
|
3789 qed |
|
3790 subgoal using vfr(1) unfolding r1_def by (auto intro!:holomorphic_intros) |
|
3791 subgoal using fr unfolding r1_def by (auto intro!:holomorphic_intros) |
|
3792 done |
|
3793 |
|
3794 have "vfp w = inverse (fp w)" when "w\<in>ball z r1-{z}" for w |
|
3795 proof - |
|
3796 have "w \<in> ball z fr - {z}" "w \<in> cball z vfr - {z}" "w\<noteq>z" using that unfolding r1_def by auto |
|
3797 from fr_inverse[OF this(1)] fr_nz[OF this(1)] vfr(2)[rule_format,OF this(2)] \<open>vfn = - fn\<close> \<open>w\<noteq>z\<close> |
|
3798 show ?thesis by auto |
|
3799 qed |
|
3800 then show "\<forall>\<^sub>Fw in (at z). vfp w = inverse (fp w)" |
|
3801 unfolding eventually_at using \<open>r1>0\<close> |
|
3802 apply (rule_tac x=r1 in exI) |
|
3803 by (auto simp add:dist_commute) |
|
3804 qed |
|
3805 |
|
3806 |
|
3807 lemma |
|
3808 fixes f g::"complex \<Rightarrow> complex" and z::complex |
|
3809 assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z" |
|
3810 and f_ness:"not_essential f z" and g_ness:"not_essential g z" |
|
3811 and fg_nconst: "\<exists>\<^sub>Fw in (at z). f w * g w\<noteq> 0" |
|
3812 shows zorder_times:"zorder (\<lambda>w. f w * g w) z = zorder f z + zorder g z" and |
|
3813 zor_poly_times:"\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w * g w) z w |
|
3814 = zor_poly f z w *zor_poly g z w" |
|
3815 proof - |
|
3816 define fg where "fg = (\<lambda>w. f w * g w)" |
|
3817 define fn gn fgn where |
|
3818 "fn = zorder f z" and "gn = zorder g z" and "fgn = zorder fg z" |
|
3819 define fp gp fgp where |
|
3820 "fp = zor_poly f z" and "gp = zor_poly g z" and "fgp = zor_poly fg z" |
|
3821 have f_nconst:"\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst:"\<exists>\<^sub>Fw in (at z).g w\<noteq> 0" |
|
3822 using fg_nconst by (auto elim!:frequently_elim1) |
|
3823 obtain fr where [simp]:"fp z \<noteq> 0" and "fr > 0" |
|
3824 and fr: "fp holomorphic_on cball z fr" |
|
3825 "\<forall>w\<in>cball z fr - {z}. f w = fp w * (w - z) powr of_int fn \<and> fp w \<noteq> 0" |
|
3826 using zorder_exist[OF f_iso f_ness f_nconst,folded fp_def fn_def] by auto |
|
3827 obtain gr where [simp]:"gp z \<noteq> 0" and "gr > 0" |
|
3828 and gr: "gp holomorphic_on cball z gr" |
|
3829 "\<forall>w\<in>cball z gr - {z}. g w = gp w * (w - z) powr of_int gn \<and> gp w \<noteq> 0" |
|
3830 using zorder_exist[OF g_iso g_ness g_nconst,folded gn_def gp_def] by auto |
|
3831 define r1 where "r1=min fr gr" |
|
3832 have "r1>0" unfolding r1_def using \<open>fr>0\<close> \<open>gr>0\<close> by auto |
|
3833 have fg_times:"fg w = (fp w * gp w) * (w - z) powr (of_int (fn+gn))" and fgp_nz:"fp w*gp w\<noteq>0" |
|
3834 when "w\<in>ball z r1 - {z}" for w |
|
3835 proof - |
|
3836 have "f w = fp w * (w - z) powr of_int fn" "fp w\<noteq>0" |
|
3837 using fr(2)[rule_format,of w] that unfolding r1_def by auto |
|
3838 moreover have "g w = gp w * (w - z) powr of_int gn" "gp w \<noteq> 0" |
|
3839 using gr(2)[rule_format, of w] that unfolding r1_def by auto |
|
3840 ultimately show "fg w = (fp w * gp w) * (w - z) powr (of_int (fn+gn))" "fp w*gp w\<noteq>0" |
|
3841 unfolding fg_def by (auto simp add:powr_add) |
|
3842 qed |
|
3843 |
|
3844 obtain fgr where [simp]:"fgp z \<noteq> 0" and "fgr > 0" |
|
3845 and fgr: "fgp holomorphic_on cball z fgr" |
|
3846 "\<forall>w\<in>cball z fgr - {z}. fg w = fgp w * (w - z) powr of_int fgn \<and> fgp w \<noteq> 0" |
|
3847 proof - |
|
3848 have "fgp z \<noteq> 0 \<and> (\<exists>r>0. fgp holomorphic_on cball z r |
|
3849 \<and> (\<forall>w\<in>cball z r - {z}. fg w = fgp w * (w - z) powr of_int fgn \<and> fgp w \<noteq> 0))" |
|
3850 apply (rule zorder_exist[of fg z, folded fgn_def fgp_def]) |
|
3851 subgoal unfolding fg_def using isolated_singularity_at_times[OF f_iso g_iso] . |
|
3852 subgoal unfolding fg_def using not_essential_times[OF f_ness g_ness f_iso g_iso] . |
|
3853 subgoal unfolding fg_def using fg_nconst . |
|
3854 done |
|
3855 then show ?thesis using that by blast |
|
3856 qed |
|
3857 define r2 where "r2 = min fgr r1" |
|
3858 have "r2>0" using \<open>r1>0\<close> \<open>fgr>0\<close> unfolding r2_def by simp |
|
3859 show "fgn = fn + gn " |
|
3860 apply (rule holomorphic_factor_unique[of r2 fgp z "\<lambda>w. fp w * gp w" fg]) |
|
3861 subgoal using \<open>r2>0\<close> by simp |
|
3862 subgoal by simp |
|
3863 subgoal by simp |
|
3864 subgoal |
|
3865 proof (rule ballI) |
|
3866 fix w assume "w \<in> ball z r2 - {z}" |
|
3867 then have "w \<in> ball z r1 - {z}" "w \<in> cball z fgr - {z}" unfolding r2_def by auto |
|
3868 from fg_times[OF this(1)] fgp_nz[OF this(1)] fgr(2)[rule_format,OF this(2)] |
|
3869 show "fg w = fgp w * (w - z) powr of_int fgn \<and> fgp w \<noteq> 0 |
|
3870 \<and> fg w = fp w * gp w * (w - z) powr of_int (fn + gn) \<and> fp w * gp w \<noteq> 0" by auto |
|
3871 qed |
|
3872 subgoal using fgr(1) unfolding r2_def r1_def by (auto intro!:holomorphic_intros) |
|
3873 subgoal using fr(1) gr(1) unfolding r2_def r1_def by (auto intro!:holomorphic_intros) |
|
3874 done |
|
3875 |
|
3876 have "fgp w = fp w *gp w" when "w\<in>ball z r2-{z}" for w |
|
3877 proof - |
|
3878 have "w \<in> ball z r1 - {z}" "w \<in> cball z fgr - {z}" "w\<noteq>z" using that unfolding r2_def by auto |
|
3879 from fg_times[OF this(1)] fgp_nz[OF this(1)] fgr(2)[rule_format,OF this(2)] \<open>fgn = fn + gn\<close> \<open>w\<noteq>z\<close> |
|
3880 show ?thesis by auto |
|
3881 qed |
|
3882 then show "\<forall>\<^sub>Fw in (at z). fgp w = fp w * gp w" |
|
3883 using \<open>r2>0\<close> unfolding eventually_at by (auto simp add:dist_commute) |
|
3884 qed |
|
3885 |
|
3886 lemma |
|
3887 fixes f g::"complex \<Rightarrow> complex" and z::complex |
|
3888 assumes f_iso:"isolated_singularity_at f z" and g_iso:"isolated_singularity_at g z" |
|
3889 and f_ness:"not_essential f z" and g_ness:"not_essential g z" |
|
3890 and fg_nconst: "\<exists>\<^sub>Fw in (at z). f w * g w\<noteq> 0" |
|
3891 shows zorder_divide:"zorder (\<lambda>w. f w / g w) z = zorder f z - zorder g z" and |
|
3892 zor_poly_divide:"\<forall>\<^sub>Fw in (at z). zor_poly (\<lambda>w. f w / g w) z w |
|
3893 = zor_poly f z w / zor_poly g z w" |
|
3894 proof - |
|
3895 have f_nconst:"\<exists>\<^sub>Fw in (at z). f w \<noteq> 0" and g_nconst:"\<exists>\<^sub>Fw in (at z).g w\<noteq> 0" |
|
3896 using fg_nconst by (auto elim!:frequently_elim1) |
|
3897 define vg where "vg=(\<lambda>w. inverse (g w))" |
|
3898 have "zorder (\<lambda>w. f w * vg w) z = zorder f z + zorder vg z" |
|
3899 apply (rule zorder_times[OF f_iso _ f_ness,of vg]) |
|
3900 subgoal unfolding vg_def using isolated_singularity_at_inverse[OF g_iso g_ness] . |
|
3901 subgoal unfolding vg_def using not_essential_inverse[OF g_ness g_iso] . |
|
3902 subgoal unfolding vg_def using fg_nconst by (auto elim!:frequently_elim1) |
|
3903 done |
|
3904 then show "zorder (\<lambda>w. f w / g w) z = zorder f z - zorder g z" |
|
3905 using zorder_inverse[OF g_iso g_ness g_nconst,folded vg_def] unfolding vg_def |
|
3906 by (auto simp add:field_simps) |
|
3907 |
|
3908 have "\<forall>\<^sub>F w in at z. zor_poly (\<lambda>w. f w * vg w) z w = zor_poly f z w * zor_poly vg z w" |
|
3909 apply (rule zor_poly_times[OF f_iso _ f_ness,of vg]) |
|
3910 subgoal unfolding vg_def using isolated_singularity_at_inverse[OF g_iso g_ness] . |
|
3911 subgoal unfolding vg_def using not_essential_inverse[OF g_ness g_iso] . |
|
3912 subgoal unfolding vg_def using fg_nconst by (auto elim!:frequently_elim1) |
|
3913 done |
|
3914 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" |
|
3915 using zor_poly_inverse[OF g_iso g_ness g_nconst,folded vg_def] unfolding vg_def |
|
3916 apply eventually_elim |
|
3917 by (auto simp add:field_simps) |
|
3918 qed |
|
3919 |
|
3920 lemma zorder_exist_zero: |
|
3921 fixes f::"complex \<Rightarrow> complex" and z::complex |
|
3922 defines "n\<equiv>zorder f z" and "g\<equiv>zor_poly f z" |
|
3923 assumes holo: "f holomorphic_on s" and |
|
3924 "open s" "connected s" "z\<in>s" |
|
3925 and non_const: "\<exists>w\<in>s. f w \<noteq> 0" |
|
3926 shows "(if f z=0 then n > 0 else n=0) \<and> (\<exists>r. r>0 \<and> cball z r \<subseteq> s \<and> g holomorphic_on cball z r |
|
3927 \<and> (\<forall>w\<in>cball z r. f w = g w * (w-z) ^ nat n \<and> g w \<noteq>0))" |
|
3928 proof - |
|
3929 obtain r where "g z \<noteq> 0" and r: "r>0" "cball z r \<subseteq> s" "g holomorphic_on cball z r" |
|
3930 "(\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0)" |
|
3931 proof - |
|
3932 have "g z \<noteq> 0 \<and> (\<exists>r>0. g holomorphic_on cball z r |
|
3933 \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0))" |
|
3934 proof (rule zorder_exist[of f z,folded g_def n_def]) |
|
3935 show "isolated_singularity_at f z" unfolding isolated_singularity_at_def |
|
3936 using holo assms(4,6) |
|
3937 by (meson Diff_subset open_ball analytic_on_holomorphic holomorphic_on_subset openE) |
|
3938 show "not_essential f z" unfolding not_essential_def |
|
3939 using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on |
|
3940 by fastforce |
|
3941 have "\<forall>\<^sub>F w in at z. f w \<noteq> 0 \<and> w\<in>s" |
|
3942 proof - |
|
3943 obtain w where "w\<in>s" "f w\<noteq>0" using non_const by auto |
|
3944 then show ?thesis |
|
3945 by (rule non_zero_neighbour_alt[OF holo \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close>]) |
|
3946 qed |
|
3947 then show "\<exists>\<^sub>F w in at z. f w \<noteq> 0" |
|
3948 apply (elim eventually_frequentlyE) |
|
3949 by auto |
|
3950 qed |
|
3951 then obtain r1 where "g z \<noteq> 0" "r1>0" and r1:"g holomorphic_on cball z r1" |
|
3952 "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0)" |
|
3953 by auto |
|
3954 obtain r2 where r2: "r2>0" "cball z r2 \<subseteq> s" |
|
3955 using assms(4,6) open_contains_cball_eq by blast |
|
3956 define r3 where "r3=min r1 r2" |
|
3957 have "r3>0" "cball z r3 \<subseteq> s" using \<open>r1>0\<close> r2 unfolding r3_def by auto |
|
3958 moreover have "g holomorphic_on cball z r3" |
|
3959 using r1(1) unfolding r3_def by auto |
|
3960 moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0)" |
|
3961 using r1(2) unfolding r3_def by auto |
|
3962 ultimately show ?thesis using that[of r3] \<open>g z\<noteq>0\<close> by auto |
|
3963 qed |
|
3964 |
|
3965 have if_0:"if f z=0 then n > 0 else n=0" |
|
3966 proof - |
|
3967 have "f\<midarrow> z \<rightarrow> f z" |
|
3968 by (metis assms(4,6,7) at_within_open continuous_on holo holomorphic_on_imp_continuous_on) |
|
3969 then have "(\<lambda>w. g w * (w - z) powr of_int n) \<midarrow>z\<rightarrow> f z" |
|
3970 apply (elim Lim_transform_within_open[where s="ball z r"]) |
|
3971 using r by auto |
|
3972 moreover have "g \<midarrow>z\<rightarrow>g z" |
|
3973 by (metis (mono_tags, lifting) Topology_Euclidean_Space.open_ball at_within_open_subset |
|
3974 ball_subset_cball centre_in_ball continuous_on holomorphic_on_imp_continuous_on r(1,3) subsetCE) |
|
3975 ultimately have "(\<lambda>w. (g w * (w - z) powr of_int n) / g w) \<midarrow>z\<rightarrow> f z/g z" |
|
3976 apply (rule_tac tendsto_divide) |
|
3977 using \<open>g z\<noteq>0\<close> by auto |
|
3978 then have powr_tendsto:"(\<lambda>w. (w - z) powr of_int n) \<midarrow>z\<rightarrow> f z/g z" |
|
3979 apply (elim Lim_transform_within_open[where s="ball z r"]) |
|
3980 using r by auto |
|
3981 |
|
3982 have ?thesis when "n\<ge>0" "f z=0" |
3151 proof - |
3983 proof - |
3152 have "\<exists>!n. \<exists>h r. n>0 \<and> P h r n" |
3984 have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z" |
3153 using holomorphic_factor_zero_Ex1[OF \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> holo \<open>f z=0\<close> |
3985 using powr_tendsto |
3154 \<open>\<exists>w\<in>s. f w\<noteq>0\<close>] unfolding P_def |
3986 apply (elim Lim_transform_within[where d=r]) |
3155 apply (subst mult.commute) |
3987 by (auto simp add: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>) |
|
3988 then have *:"(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 0" using \<open>f z=0\<close> by simp |
|
3989 moreover have False when "n=0" |
|
3990 proof - |
|
3991 have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 1" |
|
3992 using \<open>n=0\<close> by auto |
|
3993 then show False using * using LIM_unique zero_neq_one by blast |
|
3994 qed |
|
3995 ultimately show ?thesis using that by fastforce |
|
3996 qed |
|
3997 moreover have ?thesis when "n\<ge>0" "f z\<noteq>0" |
|
3998 proof - |
|
3999 have False when "n>0" |
|
4000 proof - |
|
4001 have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> f z/g z" |
|
4002 using powr_tendsto |
|
4003 apply (elim Lim_transform_within[where d=r]) |
|
4004 by (auto simp add: powr_of_int \<open>n\<ge>0\<close> \<open>r>0\<close>) |
|
4005 moreover have "(\<lambda>w. (w - z) ^ nat n) \<midarrow>z\<rightarrow> 0" |
|
4006 using \<open>n>0\<close> by (auto intro!:tendsto_eq_intros) |
|
4007 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 |
|
4008 qed |
|
4009 then show ?thesis using that by force |
|
4010 qed |
|
4011 moreover have False when "n<0" |
|
4012 proof - |
|
4013 have "(\<lambda>w. inverse ((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> f z/g z" |
|
4014 "(\<lambda>w.((w - z) ^ nat (- n))) \<midarrow>z\<rightarrow> 0" |
|
4015 subgoal using powr_tendsto powr_of_int that |
|
4016 by (elim Lim_transform_within_open[where s=UNIV],auto) |
|
4017 subgoal using that by (auto intro!:tendsto_eq_intros) |
|
4018 done |
|
4019 from tendsto_mult[OF this,simplified] |
|
4020 have "(\<lambda>x. inverse ((x - z) ^ nat (- n)) * (x - z) ^ nat (- n)) \<midarrow>z\<rightarrow> 0" . |
|
4021 then have "(\<lambda>x. 1::complex) \<midarrow>z\<rightarrow> 0" |
|
4022 by (elim Lim_transform_within_open[where s=UNIV],auto) |
|
4023 then show False using LIM_const_eq by fastforce |
|
4024 qed |
|
4025 ultimately show ?thesis by fastforce |
|
4026 qed |
|
4027 moreover have "f w = g w * (w-z) ^ nat n \<and> g w \<noteq>0" when "w\<in>cball z r" for w |
|
4028 proof (cases "w=z") |
|
4029 case True |
|
4030 then have "f \<midarrow>z\<rightarrow>f w" |
|
4031 using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on by fastforce |
|
4032 then have "(\<lambda>w. g w * (w-z) ^ nat n) \<midarrow>z\<rightarrow>f w" |
|
4033 proof (elim Lim_transform_within[OF _ \<open>r>0\<close>]) |
|
4034 fix x assume "0 < dist x z" "dist x z < r" |
|
4035 then have "x \<in> cball z r - {z}" "x\<noteq>z" |
|
4036 unfolding cball_def by (auto simp add: dist_commute) |
|
4037 then have "f x = g x * (x - z) powr of_int n" |
|
4038 using r(4)[rule_format,of x] by simp |
|
4039 also have "... = g x * (x - z) ^ nat n" |
|
4040 apply (subst powr_of_int) |
|
4041 using if_0 \<open>x\<noteq>z\<close> by (auto split:if_splits) |
|
4042 finally show "f x = g x * (x - z) ^ nat n" . |
|
4043 qed |
|
4044 moreover have "(\<lambda>w. g w * (w-z) ^ nat n) \<midarrow>z\<rightarrow> g w * (w-z) ^ nat n" |
|
4045 using True apply (auto intro!:tendsto_eq_intros) |
|
4046 by (metis open_ball at_within_open_subset ball_subset_cball centre_in_ball |
|
4047 continuous_on holomorphic_on_imp_continuous_on r(1) r(3) that) |
|
4048 ultimately have "f w = g w * (w-z) ^ nat n" using LIM_unique by blast |
|
4049 then show ?thesis using \<open>g z\<noteq>0\<close> True by auto |
|
4050 next |
|
4051 case False |
|
4052 then have "f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0" |
|
4053 using r(4) that by auto |
|
4054 then show ?thesis using False if_0 powr_of_int by (auto split:if_splits) |
|
4055 qed |
|
4056 ultimately show ?thesis using r by auto |
|
4057 qed |
|
4058 |
|
4059 lemma zorder_exist_pole: |
|
4060 fixes f::"complex \<Rightarrow> complex" and z::complex |
|
4061 defines "n\<equiv>zorder f z" and "g\<equiv>zor_poly f z" |
|
4062 assumes holo: "f holomorphic_on s-{z}" and |
|
4063 "open s" "z\<in>s" |
|
4064 and "is_pole f z" |
|
4065 shows "n < 0 \<and> g z\<noteq>0 \<and> (\<exists>r. r>0 \<and> cball z r \<subseteq> s \<and> g holomorphic_on cball z r |
|
4066 \<and> (\<forall>w\<in>cball z r - {z}. f w = g w / (w-z) ^ nat (- n) \<and> g w \<noteq>0))" |
|
4067 proof - |
|
4068 obtain r where "g z \<noteq> 0" and r: "r>0" "cball z r \<subseteq> s" "g holomorphic_on cball z r" |
|
4069 "(\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0)" |
|
4070 proof - |
|
4071 have "g z \<noteq> 0 \<and> (\<exists>r>0. g holomorphic_on cball z r |
|
4072 \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0))" |
|
4073 proof (rule zorder_exist[of f z,folded g_def n_def]) |
|
4074 show "isolated_singularity_at f z" unfolding isolated_singularity_at_def |
|
4075 using holo assms(4,5) |
|
4076 by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff) |
|
4077 show "not_essential f z" unfolding not_essential_def |
|
4078 using assms(4,6) at_within_open continuous_on holo holomorphic_on_imp_continuous_on |
|
4079 by fastforce |
|
4080 from non_zero_neighbour_pole[OF \<open>is_pole f z\<close>] show "\<exists>\<^sub>F w in at z. f w \<noteq> 0" |
|
4081 apply (elim eventually_frequentlyE) |
3156 by auto |
4082 by auto |
3157 thus ?thesis by auto |
4083 qed |
3158 qed |
4084 then obtain r1 where "g z \<noteq> 0" "r1>0" and r1:"g holomorphic_on cball z r1" |
3159 moreover have n:"n=(THE n. n>0 \<and> (\<exists>h r. P h r n))" |
4085 "(\<forall>w\<in>cball z r1 - {z}. f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0)" |
3160 unfolding n_def zorder_def P_def by simp |
4086 by auto |
3161 ultimately have "n>0 \<and> (\<exists>h r. P h r n)" |
4087 obtain r2 where r2: "r2>0" "cball z r2 \<subseteq> s" |
3162 apply (drule_tac theI') |
4088 using assms(4,5) open_contains_cball_eq by metis |
3163 by simp |
4089 define r3 where "r3=min r1 r2" |
3164 then have "n>0" and "\<exists>h r. P h r n" by auto |
4090 have "r3>0" "cball z r3 \<subseteq> s" using \<open>r1>0\<close> r2 unfolding r3_def by auto |
3165 moreover have "h=(SOME h. \<exists>r. P h r n)" |
4091 moreover have "g holomorphic_on cball z r3" |
3166 unfolding h_def P_def zer_poly_def[of f z,folded n_def P_def] by simp |
4092 using r1(1) unfolding r3_def by auto |
3167 ultimately have "\<exists>r. P h r n" |
4093 moreover have "(\<forall>w\<in>cball z r3 - {z}. f w = g w * (w - z) powr of_int n \<and> g w \<noteq> 0)" |
3168 apply (drule_tac someI_ex) |
4094 using r1(2) unfolding r3_def by auto |
3169 by simp |
4095 ultimately show ?thesis using that[of r3] \<open>g z\<noteq>0\<close> by auto |
3170 then obtain r1 where "P h r1 n" by auto |
4096 qed |
3171 obtain r2 where "r2>0" "cball z r2 \<subseteq> s" |
4097 |
3172 using assms(3) assms(5) open_contains_cball_eq by blast |
4098 have "n<0" |
3173 define r3 where "r3 \<equiv> min r1 r2" |
4099 proof (rule ccontr) |
3174 have "P h r3 n" using \<open>P h r1 n\<close> \<open>r2>0\<close> unfolding P_def r3_def |
4100 assume " \<not> n < 0" |
3175 by auto |
4101 define c where "c=(if n=0 then g z else 0)" |
3176 moreover have "cball z r3 \<subseteq> s" using \<open>cball z r2 \<subseteq> s\<close> unfolding r3_def by auto |
4102 have [simp]:"g \<midarrow>z\<rightarrow> g z" |
3177 ultimately show ?thesis using \<open>n>0\<close> unfolding P_def by auto |
4103 by (metis Topology_Euclidean_Space.open_ball at_within_open ball_subset_cball centre_in_ball |
|
4104 continuous_on holomorphic_on_imp_continuous_on holomorphic_on_subset r(1) r(3) ) |
|
4105 have "\<forall>\<^sub>F x in at z. f x = g x * (x - z) ^ nat n" |
|
4106 unfolding eventually_at_topological |
|
4107 apply (rule_tac exI[where x="ball z r"]) |
|
4108 using r powr_of_int \<open>\<not> n < 0\<close> by auto |
|
4109 moreover have "(\<lambda>x. g x * (x - z) ^ nat n) \<midarrow>z\<rightarrow>c" |
|
4110 proof (cases "n=0") |
|
4111 case True |
|
4112 then show ?thesis unfolding c_def by simp |
|
4113 next |
|
4114 case False |
|
4115 then have "(\<lambda>x. (x - z) ^ nat n) \<midarrow>z\<rightarrow> 0" using \<open>\<not> n < 0\<close> |
|
4116 by (auto intro!:tendsto_eq_intros) |
|
4117 from tendsto_mult[OF _ this,of g "g z",simplified] |
|
4118 show ?thesis unfolding c_def using False by simp |
|
4119 qed |
|
4120 ultimately have "f \<midarrow>z\<rightarrow>c" using tendsto_cong by fast |
|
4121 then show False using \<open>is_pole f z\<close> at_neq_bot not_tendsto_and_filterlim_at_infinity |
|
4122 unfolding is_pole_def by blast |
|
4123 qed |
|
4124 moreover have "\<forall>w\<in>cball z r - {z}. f w = g w / (w-z) ^ nat (- n) \<and> g w \<noteq>0" |
|
4125 using r(4) \<open>n<0\<close> powr_of_int |
|
4126 by (metis Diff_iff divide_inverse eq_iff_diff_eq_0 insert_iff linorder_not_le) |
|
4127 ultimately show ?thesis using r(1-3) \<open>g z\<noteq>0\<close> by auto |
3178 qed |
4128 qed |
3179 |
4129 |
3180 lemma zorder_eqI: |
4130 lemma zorder_eqI: |
3181 assumes "open s" "z \<in> s" "g holomorphic_on s" "g z \<noteq> 0" "n > 0" |
4131 assumes "open s" "z \<in> s" "g holomorphic_on s" "g z \<noteq> 0" |
3182 assumes "\<And>w. w \<in> s \<Longrightarrow> f w = g w * (w - z) ^ n" |
4132 assumes fg_eq:"\<And>w. \<lbrakk>w \<in> s;w\<noteq>z\<rbrakk> \<Longrightarrow> f w = g w * (w - z) powr n" |
3183 shows "zorder f z = n" |
4133 shows "zorder f z = n" |
3184 proof - |
4134 proof - |
3185 have "continuous_on s g" by (rule holomorphic_on_imp_continuous_on) fact |
4135 have "continuous_on s g" by (rule holomorphic_on_imp_continuous_on) fact |
3186 moreover have "open (-{0::complex})" by auto |
4136 moreover have "open (-{0::complex})" by auto |
3187 ultimately have "open ((g -` (-{0})) \<inter> s)" |
4137 ultimately have "open ((g -` (-{0})) \<inter> s)" |
3188 unfolding continuous_on_open_vimage[OF \<open>open s\<close>] by blast |
4138 unfolding continuous_on_open_vimage[OF \<open>open s\<close>] by blast |
3189 moreover from assms have "z \<in> (g -` (-{0})) \<inter> s" by auto |
4139 moreover from assms have "z \<in> (g -` (-{0})) \<inter> s" by auto |
3190 ultimately obtain r where r: "r > 0" "cball z r \<subseteq> (g -` (-{0})) \<inter> s" |
4140 ultimately obtain r where r: "r > 0" "cball z r \<subseteq> s \<inter> (g -` (-{0}))" |
3191 unfolding open_contains_cball by blast |
4141 unfolding open_contains_cball by blast |
3192 |
4142 |
3193 have "n > 0 \<and> r > 0 \<and> g holomorphic_on cball z r \<and> |
4143 let ?gg= "(\<lambda>w. g w * (w - z) powr n)" |
3194 (\<forall>w\<in>cball z r. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)" (is "?P g r n") |
4144 define P where "P = (\<lambda>n g r. 0 < r \<and> g holomorphic_on cball z r \<and> g z\<noteq>0 |
3195 using r assms(3,5,6) by auto |
4145 \<and> (\<forall>w\<in>cball z r - {z}. f w = g w * (w-z) powr (of_int n) \<and> g w\<noteq>0))" |
3196 hence ex: "\<exists>g r. ?P g r n" by blast |
4146 have "P n g r" |
3197 have unique: "\<exists>!n. \<exists>g r. ?P g r n" |
4147 unfolding P_def using r assms(3,4,5) by auto |
3198 proof (rule holomorphic_factor_zero_Ex1) |
4148 then have "\<exists>g r. P n g r" by auto |
3199 from r have "(\<lambda>w. g w * (w - z) ^ n) holomorphic_on ball z r" |
4149 moreover have unique: "\<exists>!n. \<exists>g r. P n g r" unfolding P_def |
3200 by (intro holomorphic_intros holomorphic_on_subset[OF assms(3)]) auto |
4150 proof (rule holomorphic_factor_puncture) |
3201 also have "?this \<longleftrightarrow> f holomorphic_on ball z r" |
4151 have "ball z r-{z} \<subseteq> s" using r using ball_subset_cball by blast |
3202 using r assms by (intro holomorphic_cong refl) (auto simp: cball_def subset_iff) |
4152 then have "?gg holomorphic_on ball z r-{z}" |
3203 finally show \<dots> . |
4153 using \<open>g holomorphic_on s\<close> r by (auto intro!: holomorphic_intros) |
|
4154 then have "f holomorphic_on ball z r - {z}" |
|
4155 apply (elim holomorphic_transform) |
|
4156 using fg_eq \<open>ball z r-{z} \<subseteq> s\<close> by auto |
|
4157 then show "isolated_singularity_at f z" unfolding isolated_singularity_at_def |
|
4158 using analytic_on_open open_delete r(1) by blast |
3204 next |
4159 next |
3205 let ?w = "z + of_real r / 2" |
4160 have "not_essential ?gg z" |
3206 have "?w \<in> ball z r" |
4161 proof (intro singularity_intros) |
3207 using r by (auto simp: dist_norm) |
4162 show "not_essential g z" |
3208 moreover from this and r have "g ?w \<noteq> 0" and "?w \<in> s" |
4163 by (meson \<open>continuous_on s g\<close> assms(1) assms(2) continuous_on_eq_continuous_at |
3209 by (auto simp: cball_def ball_def subset_iff) |
4164 isCont_def not_essential_def) |
3210 with assms have "f ?w \<noteq> 0" using \<open>r > 0\<close> by auto |
4165 show " \<forall>\<^sub>F w in at z. w - z \<noteq> 0" by (simp add: eventually_at_filter) |
3211 ultimately show "\<exists>w\<in>ball z r. f w \<noteq> 0" by blast |
4166 then show "LIM w at z. w - z :> at 0" |
3212 qed (insert assms r, auto) |
4167 unfolding filterlim_at by (auto intro:tendsto_eq_intros) |
3213 from unique and ex have "(THE n. \<exists>g r. ?P g r n) = n" |
4168 show "isolated_singularity_at g z" |
3214 by (rule the1_equality) |
4169 by (meson Diff_subset Topology_Euclidean_Space.open_ball analytic_on_holomorphic |
3215 also have "(THE n. \<exists>g r. ?P g r n) = zorder f z" |
4170 assms(1,2,3) holomorphic_on_subset isolated_singularity_at_def openE) |
3216 by (simp add: zorder_def mult.commute) |
4171 qed |
3217 finally show ?thesis . |
4172 then show "not_essential f z" |
|
4173 apply (elim not_essential_transform) |
|
4174 unfolding eventually_at using assms(1,2) assms(5)[symmetric] |
|
4175 by (metis dist_commute mem_ball openE subsetCE) |
|
4176 show "\<exists>\<^sub>F w in at z. f w \<noteq> 0" unfolding frequently_at |
|
4177 proof (rule,rule) |
|
4178 fix d::real assume "0 < d" |
|
4179 define z' where "z'=z+min d r / 2" |
|
4180 have "z' \<noteq> z" " dist z' z < d " |
|
4181 unfolding z'_def using \<open>d>0\<close> \<open>r>0\<close> |
|
4182 by (auto simp add:dist_norm) |
|
4183 moreover have "f z' \<noteq> 0" |
|
4184 proof (subst fg_eq[OF _ \<open>z'\<noteq>z\<close>]) |
|
4185 have "z' \<in> cball z r" unfolding z'_def using \<open>r>0\<close> \<open>d>0\<close> by (auto simp add:dist_norm) |
|
4186 then show " z' \<in> s" using r(2) by blast |
|
4187 show "g z' * (z' - z) powr of_int n \<noteq> 0" |
|
4188 using P_def \<open>P n g r\<close> \<open>z' \<in> cball z r\<close> calculation(1) by auto |
|
4189 qed |
|
4190 ultimately show "\<exists>x\<in>UNIV. x \<noteq> z \<and> dist x z < d \<and> f x \<noteq> 0" by auto |
|
4191 qed |
|
4192 qed |
|
4193 ultimately have "(THE n. \<exists>g r. P n g r) = n" |
|
4194 by (rule_tac the1_equality) |
|
4195 then show ?thesis unfolding zorder_def P_def by blast |
|
4196 qed |
|
4197 |
|
4198 lemma residue_pole_order: |
|
4199 fixes f::"complex \<Rightarrow> complex" and z::complex |
|
4200 defines "n \<equiv> nat (- zorder f z)" and "h \<equiv> zor_poly f z" |
|
4201 assumes f_iso:"isolated_singularity_at f z" |
|
4202 and pole:"is_pole f z" |
|
4203 shows "residue f z = ((deriv ^^ (n - 1)) h z / fact (n-1))" |
|
4204 proof - |
|
4205 define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)" |
|
4206 obtain e where [simp]:"e>0" and f_holo:"f holomorphic_on ball z e - {z}" |
|
4207 using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by blast |
|
4208 obtain r where "0 < n" "0 < r" and r_cball:"cball z r \<subseteq> ball z e" and h_holo: "h holomorphic_on cball z r" |
|
4209 and h_divide:"(\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w = h w / (w - z) ^ n) \<and> h w \<noteq> 0)" |
|
4210 proof - |
|
4211 obtain r where r:"zorder f z < 0" "h z \<noteq> 0" "r>0" "cball z r \<subseteq> ball z e" "h holomorphic_on cball z r" |
|
4212 "(\<forall>w\<in>cball z r - {z}. f w = h w / (w - z) ^ n \<and> h w \<noteq> 0)" |
|
4213 using zorder_exist_pole[OF f_holo,simplified,OF \<open>is_pole f z\<close>,folded n_def h_def] by auto |
|
4214 have "n>0" using \<open>zorder f z < 0\<close> unfolding n_def by simp |
|
4215 moreover have "(\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w = h w / (w - z) ^ n) \<and> h w \<noteq> 0)" |
|
4216 using \<open>h z\<noteq>0\<close> r(6) by blast |
|
4217 ultimately show ?thesis using r(3,4,5) that by blast |
|
4218 qed |
|
4219 have r_nonzero:"\<And>w. w \<in> ball z r - {z} \<Longrightarrow> f w \<noteq> 0" |
|
4220 using h_divide by simp |
|
4221 define c where "c \<equiv> 2 * pi * \<i>" |
|
4222 define der_f where "der_f \<equiv> ((deriv ^^ (n - 1)) h z / fact (n-1))" |
|
4223 define h' where "h' \<equiv> \<lambda>u. h u / (u - z) ^ n" |
|
4224 have "(h' has_contour_integral c / fact (n - 1) * (deriv ^^ (n - 1)) h z) (circlepath z r)" |
|
4225 unfolding h'_def |
|
4226 proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n-1", |
|
4227 folded c_def Suc_pred'[OF \<open>n>0\<close>]]) |
|
4228 show "continuous_on (cball z r) h" using holomorphic_on_imp_continuous_on h_holo by simp |
|
4229 show "h holomorphic_on ball z r" using h_holo by auto |
|
4230 show " z \<in> ball z r" using \<open>r>0\<close> by auto |
|
4231 qed |
|
4232 then have "(h' has_contour_integral c * der_f) (circlepath z r)" unfolding der_f_def by auto |
|
4233 then have "(f has_contour_integral c * der_f) (circlepath z r)" |
|
4234 proof (elim has_contour_integral_eq) |
|
4235 fix x assume "x \<in> path_image (circlepath z r)" |
|
4236 hence "x\<in>cball z r - {z}" using \<open>r>0\<close> by auto |
|
4237 then show "h' x = f x" using h_divide unfolding h'_def by auto |
|
4238 qed |
|
4239 moreover have "(f has_contour_integral c * residue f z) (circlepath z r)" |
|
4240 using base_residue[of \<open>ball z e\<close> z,simplified,OF \<open>r>0\<close> f_holo r_cball,folded c_def] |
|
4241 unfolding c_def by simp |
|
4242 ultimately have "c * der_f = c * residue f z" using has_contour_integral_unique by blast |
|
4243 hence "der_f = residue f z" unfolding c_def by auto |
|
4244 thus ?thesis unfolding der_f_def by auto |
3218 qed |
4245 qed |
3219 |
4246 |
3220 lemma simple_zeroI: |
4247 lemma simple_zeroI: |
3221 assumes "open s" "z \<in> s" "g holomorphic_on s" "g z \<noteq> 0" |
4248 assumes "open s" "z \<in> s" "g holomorphic_on s" "g z \<noteq> 0" |
3222 assumes "\<And>w. w \<in> s \<Longrightarrow> f w = g w * (w - z)" |
4249 assumes "\<And>w. w \<in> s \<Longrightarrow> f w = g w * (w - z)" |
3249 by (rule DERIV_imp_deriv) |
4276 by (rule DERIV_imp_deriv) |
3250 } |
4277 } |
3251 finally show ?case . |
4278 finally show ?case . |
3252 qed |
4279 qed |
3253 |
4280 |
3254 lemma zorder_eqI': |
4281 lemma zorder_zero_eqI: |
3255 assumes "open s" "connected s" "z \<in> s" "f holomorphic_on s" |
4282 assumes f_holo:"f holomorphic_on s" and "open s" "z \<in> s" |
3256 assumes zero: "\<And>i. i < n' \<Longrightarrow> (deriv ^^ i) f z = 0" |
4283 assumes zero: "\<And>i. i < nat n \<Longrightarrow> (deriv ^^ i) f z = 0" |
3257 assumes nz: "(deriv ^^ n') f z \<noteq> 0" and n: "n' > 0" |
4284 assumes nz: "(deriv ^^ nat n) f z \<noteq> 0" and "n\<ge>0" |
3258 shows "zorder f z = n'" |
4285 shows "zorder f z = n" |
3259 proof - |
4286 proof - |
3260 { |
4287 obtain r where [simp]:"r>0" and "ball z r \<subseteq> s" |
3261 assume *: "\<And>w. w \<in> s \<Longrightarrow> f w = 0" |
4288 using \<open>open s\<close> \<open>z\<in>s\<close> openE by blast |
3262 hence "eventually (\<lambda>u. u \<in> s) (nhds z)" |
4289 have nz':"\<exists>w\<in>ball z r. f w \<noteq> 0" |
3263 using assms by (intro eventually_nhds_in_open) auto |
4290 proof (rule ccontr) |
3264 hence "eventually (\<lambda>u. f u = 0) (nhds z)" |
4291 assume "\<not> (\<exists>w\<in>ball z r. f w \<noteq> 0)" |
3265 by eventually_elim (simp_all add: *) |
4292 then have "eventually (\<lambda>u. f u = 0) (nhds z)" |
3266 hence "(deriv ^^ n') f z = (deriv ^^ n') (\<lambda>_. 0) z" |
4293 using \<open>r>0\<close> unfolding eventually_nhds |
|
4294 apply (rule_tac x="ball z r" in exI) |
|
4295 by auto |
|
4296 then have "(deriv ^^ nat n) f z = (deriv ^^ nat n) (\<lambda>_. 0) z" |
3267 by (intro higher_deriv_cong_ev) auto |
4297 by (intro higher_deriv_cong_ev) auto |
3268 also have "(deriv ^^ n') (\<lambda>_. 0) z = 0" |
4298 also have "(deriv ^^ nat n) (\<lambda>_. 0) z = 0" |
3269 by (induction n') simp_all |
4299 by (induction n) simp_all |
3270 finally have False using nz by contradiction |
4300 finally show False using nz by contradiction |
3271 } |
4301 qed |
3272 hence nz': "\<exists>w\<in>s. f w \<noteq> 0" by blast |
4302 |
3273 |
4303 define zn g where "zn = zorder f z" and "g = zor_poly f z" |
3274 from zero[of 0] and n have [simp]: "f z = 0" by simp |
4304 obtain e where e_if:"if f z = 0 then 0 < zn else zn = 0" and |
3275 |
4305 [simp]:"e>0" and "cball z e \<subseteq> ball z r" and |
3276 define n g where "n = zorder f z" and "g = zer_poly f z" |
4306 g_holo:"g holomorphic_on cball z e" and |
3277 from zorder_exist[OF assms(1-4) \<open>f z = 0\<close> nz'] |
4307 e_fac:"(\<forall>w\<in>cball z e. f w = g w * (w - z) ^ nat zn \<and> g w \<noteq> 0)" |
3278 obtain r where r: "n > 0" "r > 0" "cball z r \<subseteq> s" "g holomorphic_on cball z r" |
4308 proof - |
3279 "\<forall>w\<in>cball z r. f w = g w * (w - z) ^ n \<and> g w \<noteq> 0" |
4309 have "f holomorphic_on ball z r" |
3280 unfolding n_def g_def by blast |
4310 using f_holo \<open>ball z r \<subseteq> s\<close> by auto |
3281 |
4311 from that zorder_exist_zero[of f "ball z r" z,simplified,OF this nz',folded zn_def g_def] |
3282 define A where "A = (\<lambda>i. of_nat (i choose n) * fact n * (deriv ^^ (i - n)) g z)" |
4312 show ?thesis by blast |
3283 { |
4313 qed |
3284 fix i :: nat |
4314 from this(1,2,5) have "zn\<ge>0" "g z\<noteq>0" |
3285 have "eventually (\<lambda>w. w \<in> ball z r) (nhds z)" |
4315 subgoal by (auto split:if_splits) |
3286 using r by (intro eventually_nhds_in_open) auto |
4316 subgoal using \<open>0 < e\<close> ball_subset_cball centre_in_ball e_fac by blast |
3287 hence "eventually (\<lambda>w. f w = (w - z) ^ n * g w) (nhds z)" |
4317 done |
3288 by eventually_elim (use r in auto) |
4318 |
3289 hence "(deriv ^^ i) f z = (deriv ^^ i) (\<lambda>w. (w - z) ^ n * g w) z" |
4319 define A where "A = (\<lambda>i. of_nat (i choose (nat zn)) * fact (nat zn) * (deriv ^^ (i - nat zn)) g z)" |
|
4320 have deriv_A:"(deriv ^^ i) f z = (if zn \<le> int i then A i else 0)" for i |
|
4321 proof - |
|
4322 have "eventually (\<lambda>w. w \<in> ball z e) (nhds z)" |
|
4323 using \<open>cball z e \<subseteq> ball z r\<close> \<open>e>0\<close> by (intro eventually_nhds_in_open) auto |
|
4324 hence "eventually (\<lambda>w. f w = (w - z) ^ (nat zn) * g w) (nhds z)" |
|
4325 apply eventually_elim |
|
4326 by (use e_fac in auto) |
|
4327 hence "(deriv ^^ i) f z = (deriv ^^ i) (\<lambda>w. (w - z) ^ nat zn * g w) z" |
3290 by (intro higher_deriv_cong_ev) auto |
4328 by (intro higher_deriv_cong_ev) auto |
3291 also have "\<dots> = (\<Sum>j=0..i. of_nat (i choose j) * |
4329 also have "\<dots> = (\<Sum>j=0..i. of_nat (i choose j) * |
3292 (deriv ^^ j) (\<lambda>w. (w - z) ^ n) z * (deriv ^^ (i - j)) g z)" |
4330 (deriv ^^ j) (\<lambda>w. (w - z) ^ nat zn) z * (deriv ^^ (i - j)) g z)" |
3293 using r by (intro higher_deriv_mult[of _ "ball z r"]) (auto intro!: holomorphic_intros) |
4331 using g_holo \<open>e>0\<close> |
3294 also have "\<dots> = (\<Sum>j=0..i. if j = n then of_nat (i choose n) * fact n * (deriv ^^ (i - n)) g z |
4332 by (intro higher_deriv_mult[of _ "ball z e"]) (auto intro!: holomorphic_intros) |
3295 else 0)" |
4333 also have "\<dots> = (\<Sum>j=0..i. if j = nat zn then |
|
4334 of_nat (i choose nat zn) * fact (nat zn) * (deriv ^^ (i - nat zn)) g z else 0)" |
3296 proof (intro sum.cong refl, goal_cases) |
4335 proof (intro sum.cong refl, goal_cases) |
3297 case (1 j) |
4336 case (1 j) |
3298 have "(deriv ^^ j) (\<lambda>w. (w - z) ^ n) z = |
4337 have "(deriv ^^ j) (\<lambda>w. (w - z) ^ nat zn) z = |
3299 pochhammer (of_nat (Suc n - j)) j * 0 ^ (n - j)" |
4338 pochhammer (of_nat (Suc (nat zn) - j)) j * 0 ^ (nat zn - j)" |
3300 by (subst higher_deriv_power) auto |
4339 by (subst higher_deriv_power) auto |
3301 also have "\<dots> = (if j = n then fact j else 0)" |
4340 also have "\<dots> = (if j = nat zn then fact j else 0)" |
3302 by (auto simp: not_less pochhammer_0_left pochhammer_fact) |
4341 by (auto simp: not_less pochhammer_0_left pochhammer_fact) |
3303 also have "of_nat (i choose j) * \<dots> * (deriv ^^ (i - j)) g z = |
4342 also have "of_nat (i choose j) * \<dots> * (deriv ^^ (i - j)) g z = |
3304 (if j = n then of_nat (i choose n) * fact n * (deriv ^^ (i - n)) g z else 0)" |
4343 (if j = nat zn then of_nat (i choose (nat zn)) * fact (nat zn) |
|
4344 * (deriv ^^ (i - nat zn)) g z else 0)" |
3305 by simp |
4345 by simp |
3306 finally show ?case . |
4346 finally show ?case . |
3307 qed |
4347 qed |
3308 also have "\<dots> = (if i \<ge> n then A i else 0)" |
4348 also have "\<dots> = (if i \<ge> zn then A i else 0)" |
3309 by (auto simp: A_def) |
4349 by (auto simp: A_def) |
3310 finally have "(deriv ^^ i) f z = \<dots>" . |
4350 finally show "(deriv ^^ i) f z = \<dots>" . |
3311 } note * = this |
4351 qed |
3312 |
4352 |
3313 from *[of n] and r have "(deriv ^^ n) f z \<noteq> 0" |
4353 have False when "n<zn" |
3314 by (simp add: A_def) |
4354 proof - |
3315 with zero[of n] have "n \<ge> n'" by (cases "n \<ge> n'") auto |
4355 have "(deriv ^^ nat n) f z = 0" |
3316 with nz show "n = n'" |
4356 using deriv_A[of "nat n"] that \<open>n\<ge>0\<close> by auto |
3317 by (auto simp: * split: if_splits) |
4357 with nz show False by auto |
3318 qed |
4358 qed |
3319 |
4359 moreover have "n\<le>zn" |
3320 lemma simple_zeroI': |
4360 proof - |
3321 assumes "open s" "connected s" "z \<in> s" |
4361 have "g z \<noteq> 0" using e_fac[rule_format,of z] \<open>e>0\<close> by simp |
3322 assumes "\<And>z. z \<in> s \<Longrightarrow> (f has_field_derivative f' z) (at z)" |
4362 then have "(deriv ^^ nat zn) f z \<noteq> 0" |
3323 assumes "f z = 0" "f' z \<noteq> 0" |
4363 using deriv_A[of "nat zn"] by(auto simp add:A_def) |
3324 shows "zorder f z = 1" |
4364 then have "nat zn \<ge> nat n" using zero[of "nat zn"] by linarith |
3325 proof - |
4365 moreover have "zn\<ge>0" using e_if by (auto split:if_splits) |
3326 have "deriv f z = f' z" if "z \<in> s" for z |
4366 ultimately show ?thesis using nat_le_eq_zle by blast |
3327 using that by (intro DERIV_imp_deriv assms) auto |
4367 qed |
3328 moreover from assms have "f holomorphic_on s" |
4368 ultimately show ?thesis unfolding zn_def by fastforce |
3329 by (subst holomorphic_on_open) auto |
4369 qed |
3330 ultimately show ?thesis using assms |
4370 |
3331 by (intro zorder_eqI'[of s]) auto |
4371 lemma |
3332 qed |
4372 assumes "eventually (\<lambda>z. f z = g z) (at z)" "z = z'" |
3333 |
4373 shows zorder_cong:"zorder f z = zorder g z'" and zor_poly_cong:"zor_poly f z = zor_poly g z'" |
3334 lemma porder_exist: |
4374 proof - |
3335 fixes f::"complex \<Rightarrow> complex" and z::complex |
4375 define P where "P = (\<lambda>ff n h r. 0 < r \<and> h holomorphic_on cball z r \<and> h z\<noteq>0 |
3336 defines "n \<equiv> porder f z" and "h \<equiv> pol_poly f z" |
4376 \<and> (\<forall>w\<in>cball z r - {z}. ff w = h w * (w-z) powr (of_int n) \<and> h w\<noteq>0))" |
3337 assumes "open s" "z \<in> s" |
4377 have "(\<exists>r. P f n h r) = (\<exists>r. P g n h r)" for n h |
3338 and holo:"f holomorphic_on s-{z}" |
4378 proof - |
3339 and "is_pole f z" |
4379 have *: "\<exists>r. P g n h r" if "\<exists>r. P f n h r" and "eventually (\<lambda>x. f x = g x) (at z)" for f g |
3340 shows "\<exists>r. n>0 \<and> r>0 \<and> cball z r \<subseteq> s \<and> h holomorphic_on cball z r |
|
3341 \<and> (\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w = h w / (w-z)^n) \<and> h w \<noteq>0)" |
|
3342 proof - |
|
3343 obtain e where "e>0" and e_ball:"ball z e \<subseteq> s"and e_def: "\<forall>x\<in>ball z e-{z}. f x\<noteq>0" |
|
3344 proof - |
4380 proof - |
3345 have "\<forall>\<^sub>F z in at z. f z \<noteq> 0" |
4381 from that(1) obtain r1 where r1_P:"P f n h r1" by auto |
3346 using \<open>is_pole f z\<close> filterlim_at_infinity_imp_eventually_ne unfolding is_pole_def |
4382 from that(2) obtain r2 where "r2>0" and r2_dist:"\<forall>x. x \<noteq> z \<and> dist x z \<le> r2 \<longrightarrow> f x = g x" |
|
4383 unfolding eventually_at_le by auto |
|
4384 define r where "r=min r1 r2" |
|
4385 have "r>0" "h z\<noteq>0" using r1_P \<open>r2>0\<close> unfolding r_def P_def by auto |
|
4386 moreover have "h holomorphic_on cball z r" |
|
4387 using r1_P unfolding P_def r_def by auto |
|
4388 moreover have "g w = h w * (w - z) powr of_int n \<and> h w \<noteq> 0" when "w\<in>cball z r - {z}" for w |
|
4389 proof - |
|
4390 have "f w = h w * (w - z) powr of_int n \<and> h w \<noteq> 0" |
|
4391 using r1_P that unfolding P_def r_def by auto |
|
4392 moreover have "f w=g w" using r2_dist[rule_format,of w] that unfolding r_def |
|
4393 by (simp add: dist_commute) |
|
4394 ultimately show ?thesis by simp |
|
4395 qed |
|
4396 ultimately show ?thesis unfolding P_def by auto |
|
4397 qed |
|
4398 from assms have eq': "eventually (\<lambda>z. g z = f z) (at z)" |
|
4399 by (simp add: eq_commute) |
|
4400 show ?thesis |
|
4401 by (rule iffI[OF *[OF _ assms(1)] *[OF _ eq']]) |
|
4402 qed |
|
4403 then show "zorder f z = zorder g z'" "zor_poly f z = zor_poly g z'" |
|
4404 using \<open>z=z'\<close> unfolding P_def zorder_def zor_poly_def by auto |
|
4405 qed |
|
4406 |
|
4407 lemma zorder_nonzero_div_power: |
|
4408 assumes "open s" "z \<in> s" "f holomorphic_on s" "f z \<noteq> 0" "n > 0" |
|
4409 shows "zorder (\<lambda>w. f w / (w - z) ^ n) z = - n" |
|
4410 apply (rule zorder_eqI[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>f holomorphic_on s\<close> \<open>f z\<noteq>0\<close>]) |
|
4411 apply (subst powr_of_int) |
|
4412 using \<open>n>0\<close> by (auto simp add:field_simps) |
|
4413 |
|
4414 lemma zor_poly_eq: |
|
4415 assumes "isolated_singularity_at f z" "not_essential f z" "\<exists>\<^sub>F w in at z. f w \<noteq> 0" |
|
4416 shows "eventually (\<lambda>w. zor_poly f z w = f w * (w - z) powr - zorder f z) (at z)" |
|
4417 proof - |
|
4418 obtain r where r:"r>0" |
|
4419 "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w * (w - z) powr of_int (zorder f z))" |
|
4420 using zorder_exist[OF assms] by blast |
|
4421 then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w * (w - z) powr - zorder f z" |
|
4422 by (auto simp: field_simps powr_minus) |
|
4423 have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)" |
|
4424 using r eventually_at_ball'[of r z UNIV] by auto |
|
4425 thus ?thesis by eventually_elim (insert *, auto) |
|
4426 qed |
|
4427 |
|
4428 lemma zor_poly_zero_eq: |
|
4429 assumes "f holomorphic_on s" "open s" "connected s" "z \<in> s" "\<exists>w\<in>s. f w \<noteq> 0" |
|
4430 shows "eventually (\<lambda>w. zor_poly f z w = f w / (w - z) ^ nat (zorder f z)) (at z)" |
|
4431 proof - |
|
4432 obtain r where r:"r>0" |
|
4433 "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w * (w - z) ^ nat (zorder f z))" |
|
4434 using zorder_exist_zero[OF assms] by auto |
|
4435 then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w / (w - z) ^ nat (zorder f z)" |
|
4436 by (auto simp: field_simps powr_minus) |
|
4437 have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)" |
|
4438 using r eventually_at_ball'[of r z UNIV] by auto |
|
4439 thus ?thesis by eventually_elim (insert *, auto) |
|
4440 qed |
|
4441 |
|
4442 lemma zor_poly_pole_eq: |
|
4443 assumes f_iso:"isolated_singularity_at f z" "is_pole f z" |
|
4444 shows "eventually (\<lambda>w. zor_poly f z w = f w * (w - z) ^ nat (- zorder f z)) (at z)" |
|
4445 proof - |
|
4446 obtain e where [simp]:"e>0" and f_holo:"f holomorphic_on ball z e - {z}" |
|
4447 using f_iso analytic_imp_holomorphic unfolding isolated_singularity_at_def by blast |
|
4448 obtain r where r:"r>0" |
|
4449 "(\<forall>w\<in>cball z r - {z}. f w = zor_poly f z w / (w - z) ^ nat (- zorder f z))" |
|
4450 using zorder_exist_pole[OF f_holo,simplified,OF \<open>is_pole f z\<close>] by auto |
|
4451 then have *: "\<forall>w\<in>ball z r - {z}. zor_poly f z w = f w * (w - z) ^ nat (- zorder f z)" |
|
4452 by (auto simp: field_simps) |
|
4453 have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)" |
|
4454 using r eventually_at_ball'[of r z UNIV] by auto |
|
4455 thus ?thesis by eventually_elim (insert *, auto) |
|
4456 qed |
|
4457 |
|
4458 lemma zor_poly_eqI: |
|
4459 fixes f :: "complex \<Rightarrow> complex" and z0 :: complex |
|
4460 defines "n \<equiv> zorder f z0" |
|
4461 assumes "isolated_singularity_at f z0" "not_essential f z0" "\<exists>\<^sub>F w in at z0. f w \<noteq> 0" |
|
4462 assumes lim: "((\<lambda>x. f (g x) * (g x - z0) powr - n) \<longlongrightarrow> c) F" |
|
4463 assumes g: "filterlim g (at z0) F" and "F \<noteq> bot" |
|
4464 shows "zor_poly f z0 z0 = c" |
|
4465 proof - |
|
4466 from zorder_exist[OF assms(2-4)] obtain r where |
|
4467 r: "r > 0" "zor_poly f z0 holomorphic_on cball z0 r" |
|
4468 "\<And>w. w \<in> cball z0 r - {z0} \<Longrightarrow> f w = zor_poly f z0 w * (w - z0) powr n" |
|
4469 unfolding n_def by blast |
|
4470 from r(1) have "eventually (\<lambda>w. w \<in> ball z0 r \<and> w \<noteq> z0) (at z0)" |
|
4471 using eventually_at_ball'[of r z0 UNIV] by auto |
|
4472 hence "eventually (\<lambda>w. zor_poly f z0 w = f w * (w - z0) powr - n) (at z0)" |
|
4473 by eventually_elim (insert r, auto simp: field_simps powr_minus) |
|
4474 moreover have "continuous_on (ball z0 r) (zor_poly f z0)" |
|
4475 using r by (intro holomorphic_on_imp_continuous_on) auto |
|
4476 with r(1,2) have "isCont (zor_poly f z0) z0" |
|
4477 by (auto simp: continuous_on_eq_continuous_at) |
|
4478 hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)" |
|
4479 unfolding isCont_def . |
|
4480 ultimately have "((\<lambda>w. f w * (w - z0) powr - n) \<longlongrightarrow> zor_poly f z0 z0) (at z0)" |
|
4481 by (rule Lim_transform_eventually) |
|
4482 hence "((\<lambda>x. f (g x) * (g x - z0) powr - n) \<longlongrightarrow> zor_poly f z0 z0) F" |
|
4483 by (rule filterlim_compose[OF _ g]) |
|
4484 from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis . |
|
4485 qed |
|
4486 |
|
4487 lemma zor_poly_zero_eqI: |
|
4488 fixes f :: "complex \<Rightarrow> complex" and z0 :: complex |
|
4489 defines "n \<equiv> zorder f z0" |
|
4490 assumes "f holomorphic_on A" "open A" "connected A" "z0 \<in> A" "\<exists>z\<in>A. f z \<noteq> 0" |
|
4491 assumes lim: "((\<lambda>x. f (g x) / (g x - z0) ^ nat n) \<longlongrightarrow> c) F" |
|
4492 assumes g: "filterlim g (at z0) F" and "F \<noteq> bot" |
|
4493 shows "zor_poly f z0 z0 = c" |
|
4494 proof - |
|
4495 from zorder_exist_zero[OF assms(2-6)] obtain r where |
|
4496 r: "r > 0" "cball z0 r \<subseteq> A" "zor_poly f z0 holomorphic_on cball z0 r" |
|
4497 "\<And>w. w \<in> cball z0 r \<Longrightarrow> f w = zor_poly f z0 w * (w - z0) ^ nat n" |
|
4498 unfolding n_def by blast |
|
4499 from r(1) have "eventually (\<lambda>w. w \<in> ball z0 r \<and> w \<noteq> z0) (at z0)" |
|
4500 using eventually_at_ball'[of r z0 UNIV] by auto |
|
4501 hence "eventually (\<lambda>w. zor_poly f z0 w = f w / (w - z0) ^ nat n) (at z0)" |
|
4502 by eventually_elim (insert r, auto simp: field_simps) |
|
4503 moreover have "continuous_on (ball z0 r) (zor_poly f z0)" |
|
4504 using r by (intro holomorphic_on_imp_continuous_on) auto |
|
4505 with r(1,2) have "isCont (zor_poly f z0) z0" |
|
4506 by (auto simp: continuous_on_eq_continuous_at) |
|
4507 hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)" |
|
4508 unfolding isCont_def . |
|
4509 ultimately have "((\<lambda>w. f w / (w - z0) ^ nat n) \<longlongrightarrow> zor_poly f z0 z0) (at z0)" |
|
4510 by (rule Lim_transform_eventually) |
|
4511 hence "((\<lambda>x. f (g x) / (g x - z0) ^ nat n) \<longlongrightarrow> zor_poly f z0 z0) F" |
|
4512 by (rule filterlim_compose[OF _ g]) |
|
4513 from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis . |
|
4514 qed |
|
4515 |
|
4516 lemma zor_poly_pole_eqI: |
|
4517 fixes f :: "complex \<Rightarrow> complex" and z0 :: complex |
|
4518 defines "n \<equiv> zorder f z0" |
|
4519 assumes f_iso:"isolated_singularity_at f z0" and "is_pole f z0" |
|
4520 assumes lim: "((\<lambda>x. f (g x) * (g x - z0) ^ nat (-n)) \<longlongrightarrow> c) F" |
|
4521 assumes g: "filterlim g (at z0) F" and "F \<noteq> bot" |
|
4522 shows "zor_poly f z0 z0 = c" |
|
4523 proof - |
|
4524 obtain r where r: "r > 0" "zor_poly f z0 holomorphic_on cball z0 r" |
|
4525 proof - |
|
4526 have "\<exists>\<^sub>F w in at z0. f w \<noteq> 0" |
|
4527 using non_zero_neighbour_pole[OF \<open>is_pole f z0\<close>] by (auto elim:eventually_frequentlyE) |
|
4528 moreover have "not_essential f z0" unfolding not_essential_def using \<open>is_pole f z0\<close> by simp |
|
4529 ultimately show ?thesis using that zorder_exist[OF f_iso,folded n_def] by auto |
|
4530 qed |
|
4531 from r(1) have "eventually (\<lambda>w. w \<in> ball z0 r \<and> w \<noteq> z0) (at z0)" |
|
4532 using eventually_at_ball'[of r z0 UNIV] by auto |
|
4533 have "eventually (\<lambda>w. zor_poly f z0 w = f w * (w - z0) ^ nat (-n)) (at z0)" |
|
4534 using zor_poly_pole_eq[OF f_iso \<open>is_pole f z0\<close>] unfolding n_def . |
|
4535 moreover have "continuous_on (ball z0 r) (zor_poly f z0)" |
|
4536 using r by (intro holomorphic_on_imp_continuous_on) auto |
|
4537 with r(1,2) have "isCont (zor_poly f z0) z0" |
|
4538 by (auto simp: continuous_on_eq_continuous_at) |
|
4539 hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)" |
|
4540 unfolding isCont_def . |
|
4541 ultimately have "((\<lambda>w. f w * (w - z0) ^ nat (-n)) \<longlongrightarrow> zor_poly f z0 z0) (at z0)" |
|
4542 by (rule Lim_transform_eventually) |
|
4543 hence "((\<lambda>x. f (g x) * (g x - z0) ^ nat (-n)) \<longlongrightarrow> zor_poly f z0 z0) F" |
|
4544 by (rule filterlim_compose[OF _ g]) |
|
4545 from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis . |
|
4546 qed |
|
4547 |
|
4548 lemma residue_simple_pole: |
|
4549 assumes "isolated_singularity_at f z0" |
|
4550 assumes "is_pole f z0" "zorder f z0 = - 1" |
|
4551 shows "residue f z0 = zor_poly f z0 z0" |
|
4552 using assms by (subst residue_pole_order) simp_all |
|
4553 |
|
4554 lemma residue_simple_pole_limit: |
|
4555 assumes "isolated_singularity_at f z0" |
|
4556 assumes "is_pole f z0" "zorder f z0 = - 1" |
|
4557 assumes "((\<lambda>x. f (g x) * (g x - z0)) \<longlongrightarrow> c) F" |
|
4558 assumes "filterlim g (at z0) F" "F \<noteq> bot" |
|
4559 shows "residue f z0 = c" |
|
4560 proof - |
|
4561 have "residue f z0 = zor_poly f z0 z0" |
|
4562 by (rule residue_simple_pole assms)+ |
|
4563 also have "\<dots> = c" |
|
4564 apply (rule zor_poly_pole_eqI) |
|
4565 using assms by auto |
|
4566 finally show ?thesis . |
|
4567 qed |
|
4568 |
|
4569 lemma lhopital_complex_simple: |
|
4570 assumes "(f has_field_derivative f') (at z)" |
|
4571 assumes "(g has_field_derivative g') (at z)" |
|
4572 assumes "f z = 0" "g z = 0" "g' \<noteq> 0" "f' / g' = c" |
|
4573 shows "((\<lambda>w. f w / g w) \<longlongrightarrow> c) (at z)" |
|
4574 proof - |
|
4575 have "eventually (\<lambda>w. w \<noteq> z) (at z)" |
|
4576 by (auto simp: eventually_at_filter) |
|
4577 hence "eventually (\<lambda>w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z)) = f w / g w) (at z)" |
|
4578 by eventually_elim (simp add: assms divide_simps) |
|
4579 moreover have "((\<lambda>w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z))) \<longlongrightarrow> f' / g') (at z)" |
|
4580 by (intro tendsto_divide has_field_derivativeD assms) |
|
4581 ultimately have "((\<lambda>w. f w / g w) \<longlongrightarrow> f' / g') (at z)" |
|
4582 by (rule Lim_transform_eventually) |
|
4583 with assms show ?thesis by simp |
|
4584 qed |
|
4585 |
|
4586 lemma |
|
4587 assumes f_holo:"f holomorphic_on s" and g_holo:"g holomorphic_on s" |
|
4588 and "open s" "connected s" "z \<in> s" |
|
4589 assumes g_deriv:"(g has_field_derivative g') (at z)" |
|
4590 assumes "f z \<noteq> 0" "g z = 0" "g' \<noteq> 0" |
|
4591 shows porder_simple_pole_deriv: "zorder (\<lambda>w. f w / g w) z = - 1" |
|
4592 and residue_simple_pole_deriv: "residue (\<lambda>w. f w / g w) z = f z / g'" |
|
4593 proof - |
|
4594 have [simp]:"isolated_singularity_at f z" "isolated_singularity_at g z" |
|
4595 using isolated_singularity_at_holomorphic[OF _ \<open>open s\<close> \<open>z\<in>s\<close>] f_holo g_holo |
|
4596 by (meson Diff_subset holomorphic_on_subset)+ |
|
4597 have [simp]:"not_essential f z" "not_essential g z" |
|
4598 unfolding not_essential_def using f_holo g_holo assms(3,5) |
|
4599 by (meson continuous_on_eq_continuous_at continuous_within holomorphic_on_imp_continuous_on)+ |
|
4600 have g_nconst:"\<exists>\<^sub>F w in at z. g w \<noteq>0 " |
|
4601 proof (rule ccontr) |
|
4602 assume "\<not> (\<exists>\<^sub>F w in at z. g w \<noteq> 0)" |
|
4603 then have "\<forall>\<^sub>F w in nhds z. g w = 0" |
|
4604 unfolding eventually_at eventually_nhds frequently_at using \<open>g z = 0\<close> |
|
4605 by (metis Topology_Euclidean_Space.open_ball UNIV_I centre_in_ball dist_commute mem_ball) |
|
4606 then have "deriv g z = deriv (\<lambda>_. 0) z" |
|
4607 by (intro deriv_cong_ev) auto |
|
4608 then have "deriv g z = 0" by auto |
|
4609 then have "g' = 0" using g_deriv DERIV_imp_deriv by blast |
|
4610 then show False using \<open>g'\<noteq>0\<close> by auto |
|
4611 qed |
|
4612 |
|
4613 have "zorder (\<lambda>w. f w / g w) z = zorder f z - zorder g z" |
|
4614 proof - |
|
4615 have "\<forall>\<^sub>F w in at z. f w \<noteq>0 \<and> w\<in>s" |
|
4616 apply (rule non_zero_neighbour_alt) |
|
4617 using assms by auto |
|
4618 with g_nconst have "\<exists>\<^sub>F w in at z. f w * g w \<noteq> 0" |
|
4619 by (elim frequently_rev_mp eventually_rev_mp,auto) |
|
4620 then show ?thesis using zorder_divide[of f z g] by auto |
|
4621 qed |
|
4622 moreover have "zorder f z=0" |
|
4623 apply (rule zorder_zero_eqI[OF f_holo \<open>open s\<close> \<open>z\<in>s\<close>]) |
|
4624 using \<open>f z\<noteq>0\<close> by auto |
|
4625 moreover have "zorder g z=1" |
|
4626 apply (rule zorder_zero_eqI[OF g_holo \<open>open s\<close> \<open>z\<in>s\<close>]) |
|
4627 subgoal using assms(8) by auto |
|
4628 subgoal using DERIV_imp_deriv assms(9) g_deriv by auto |
|
4629 subgoal by simp |
|
4630 done |
|
4631 ultimately show "zorder (\<lambda>w. f w / g w) z = - 1" by auto |
|
4632 |
|
4633 show "residue (\<lambda>w. f w / g w) z = f z / g'" |
|
4634 proof (rule residue_simple_pole_limit[where g=id and F="at z",simplified]) |
|
4635 show "zorder (\<lambda>w. f w / g w) z = - 1" by fact |
|
4636 show "isolated_singularity_at (\<lambda>w. f w / g w) z" |
|
4637 by (auto intro: singularity_intros) |
|
4638 show "is_pole (\<lambda>w. f w / g w) z" |
|
4639 proof (rule is_pole_divide) |
|
4640 have "\<forall>\<^sub>F x in at z. g x \<noteq> 0" |
|
4641 apply (rule non_zero_neighbour) |
|
4642 using g_nconst by auto |
|
4643 moreover have "g \<midarrow>z\<rightarrow> 0" |
|
4644 using DERIV_isCont assms(8) continuous_at g_deriv by force |
|
4645 ultimately show "filterlim g (at 0) (at z)" unfolding filterlim_at by simp |
|
4646 show "isCont f z" |
|
4647 using assms(3,5) continuous_on_eq_continuous_at f_holo holomorphic_on_imp_continuous_on |
3347 by auto |
4648 by auto |
3348 then obtain e1 where "e1>0" and e1_def: "\<forall>x. x \<noteq> z \<and> dist x z < e1 \<longrightarrow> f x \<noteq> 0" |
4649 show "f z \<noteq> 0" by fact |
3349 using eventually_at[of "\<lambda>x. f x\<noteq>0" z,simplified] by auto |
4650 qed |
3350 obtain e2 where "e2>0" and "ball z e2 \<subseteq>s" using \<open>open s\<close> \<open>z\<in>s\<close> openE by auto |
4651 show "filterlim id (at z) (at z)" by (simp add: filterlim_iff) |
3351 define e where "e \<equiv> min e1 e2" |
4652 have "((\<lambda>w. (f w * (w - z)) / g w) \<longlongrightarrow> f z / g') (at z)" |
3352 have "e>0" using \<open>e1>0\<close> \<open>e2>0\<close> unfolding e_def by auto |
4653 proof (rule lhopital_complex_simple) |
3353 moreover have "ball z e \<subseteq> s" unfolding e_def using \<open>ball z e2 \<subseteq> s\<close> by auto |
4654 show "((\<lambda>w. f w * (w - z)) has_field_derivative f z) (at z)" |
3354 moreover have "\<forall>x\<in>ball z e-{z}. f x\<noteq>0" using e1_def \<open>e1>0\<close> \<open>e2>0\<close> unfolding e_def |
4655 using assms by (auto intro!: derivative_eq_intros holomorphic_derivI[OF f_holo]) |
3355 by (simp add: DiffD1 DiffD2 dist_commute singletonI) |
4656 show "(g has_field_derivative g') (at z)" by fact |
3356 ultimately show ?thesis using that by auto |
4657 qed (insert assms, auto) |
3357 qed |
4658 then show "((\<lambda>w. (f w / g w) * (w - z)) \<longlongrightarrow> f z / g') (at z)" |
3358 define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)" |
4659 by (simp add: divide_simps) |
3359 define zo where "zo \<equiv> zorder g z" |
4660 qed |
3360 define zp where "zp \<equiv> zer_poly g z" |
4661 qed |
3361 have "\<exists>w\<in>ball z e. g w \<noteq> 0" |
4662 |
3362 proof - |
4663 subsection \<open>The argument principle\<close> |
3363 obtain w where w:"w\<in>ball z e-{z}" using \<open>0 < e\<close> |
|
3364 by (metis open_ball all_not_in_conv centre_in_ball insert_Diff_single |
|
3365 insert_absorb not_open_singleton) |
|
3366 hence "w\<noteq>z" "f w\<noteq>0" using e_def[rule_format,of w] mem_ball |
|
3367 by (auto simp add:dist_commute) |
|
3368 then show ?thesis unfolding g_def using w by auto |
|
3369 qed |
|
3370 moreover have "g holomorphic_on ball z e" |
|
3371 apply (intro is_pole_inverse_holomorphic[of "ball z e",OF _ _ \<open>is_pole f z\<close> e_def,folded g_def]) |
|
3372 using holo e_ball by auto |
|
3373 moreover have "g z=0" unfolding g_def by auto |
|
3374 ultimately obtain r where "0 < zo" "0 < r" "cball z r \<subseteq> ball z e" |
|
3375 and zp_holo: "zp holomorphic_on cball z r" and |
|
3376 zp_fac: "\<forall>w\<in>cball z r. g w = zp w * (w - z) ^ zo \<and> zp w \<noteq> 0" |
|
3377 using zorder_exist[of "ball z e" z g,simplified,folded zo_def zp_def] \<open>e>0\<close> |
|
3378 by auto |
|
3379 have n:"n=zo" and h:"h=inverse o zp" |
|
3380 unfolding n_def zo_def porder_def h_def zp_def pol_poly_def g_def by simp_all |
|
3381 have "h holomorphic_on cball z r" |
|
3382 using zp_holo zp_fac holomorphic_on_inverse unfolding h comp_def by blast |
|
3383 moreover have "\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w = h w / (w-z)^n) \<and> h w \<noteq>0" |
|
3384 using zp_fac unfolding h n comp_def g_def |
|
3385 by (metis divide_inverse_commute field_class.field_inverse_zero inverse_inverse_eq |
|
3386 inverse_mult_distrib mult.commute) |
|
3387 moreover have "0 < n" unfolding n using \<open>zo>0\<close> by simp |
|
3388 ultimately show ?thesis using \<open>0 < r\<close> \<open>cball z r \<subseteq> ball z e\<close> e_ball by auto |
|
3389 qed |
|
3390 |
|
3391 lemma residue_porder: |
|
3392 fixes f::"complex \<Rightarrow> complex" and z::complex |
|
3393 defines "n \<equiv> porder f z" and "h \<equiv> pol_poly f z" |
|
3394 assumes "open s" "z \<in> s" |
|
3395 and holo:"f holomorphic_on s - {z}" |
|
3396 and pole:"is_pole f z" |
|
3397 shows "residue f z = ((deriv ^^ (n - 1)) h z / fact (n-1))" |
|
3398 proof - |
|
3399 define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)" |
|
3400 obtain r where "0 < n" "0 < r" and r_cball:"cball z r \<subseteq> s" and h_holo: "h holomorphic_on cball z r" |
|
3401 and h_divide:"(\<forall>w\<in>cball z r. (w\<noteq>z \<longrightarrow> f w = h w / (w - z) ^ n) \<and> h w \<noteq> 0)" |
|
3402 using porder_exist[OF \<open>open s\<close> \<open>z \<in> s\<close> holo pole, folded n_def h_def] by blast |
|
3403 have r_nonzero:"\<And>w. w \<in> ball z r - {z} \<Longrightarrow> f w \<noteq> 0" |
|
3404 using h_divide by simp |
|
3405 define c where "c \<equiv> 2 * pi * \<i>" |
|
3406 define der_f where "der_f \<equiv> ((deriv ^^ (n - 1)) h z / fact (n-1))" |
|
3407 define h' where "h' \<equiv> \<lambda>u. h u / (u - z) ^ n" |
|
3408 have "(h' has_contour_integral c / fact (n - 1) * (deriv ^^ (n - 1)) h z) (circlepath z r)" |
|
3409 unfolding h'_def |
|
3410 proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n-1", |
|
3411 folded c_def Suc_pred'[OF \<open>n>0\<close>]]) |
|
3412 show "continuous_on (cball z r) h" using holomorphic_on_imp_continuous_on h_holo by simp |
|
3413 show "h holomorphic_on ball z r" using h_holo by auto |
|
3414 show " z \<in> ball z r" using \<open>r>0\<close> by auto |
|
3415 qed |
|
3416 then have "(h' has_contour_integral c * der_f) (circlepath z r)" unfolding der_f_def by auto |
|
3417 then have "(f has_contour_integral c * der_f) (circlepath z r)" |
|
3418 proof (elim has_contour_integral_eq) |
|
3419 fix x assume "x \<in> path_image (circlepath z r)" |
|
3420 hence "x\<in>cball z r - {z}" using \<open>r>0\<close> by auto |
|
3421 then show "h' x = f x" using h_divide unfolding h'_def by auto |
|
3422 qed |
|
3423 moreover have "(f has_contour_integral c * residue f z) (circlepath z r)" |
|
3424 using base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>r>0\<close> holo r_cball,folded c_def] . |
|
3425 ultimately have "c * der_f = c * residue f z" using has_contour_integral_unique by blast |
|
3426 hence "der_f = residue f z" unfolding c_def by auto |
|
3427 thus ?thesis unfolding der_f_def by auto |
|
3428 qed |
|
3429 |
4664 |
3430 theorem argument_principle: |
4665 theorem argument_principle: |
3431 fixes f::"complex \<Rightarrow> complex" and poles s:: "complex set" |
4666 fixes f::"complex \<Rightarrow> complex" and poles s:: "complex set" |
3432 defines "zeros\<equiv>{p. f p=0} - poles" |
4667 defines "pz \<equiv> {w. f w = 0 \<or> w \<in> poles}" \<comment> \<open>@{term "pz"} is the set of poles and zeros\<close> |
3433 assumes "open s" and |
4668 assumes "open s" and |
3434 "connected s" and |
4669 "connected s" and |
3435 f_holo:"f holomorphic_on s-poles" and |
4670 f_holo:"f holomorphic_on s-poles" and |
3436 h_holo:"h holomorphic_on s" and |
4671 h_holo:"h holomorphic_on s" and |
3437 "valid_path g" and |
4672 "valid_path g" and |
3438 loop:"pathfinish g = pathstart g" and |
4673 loop:"pathfinish g = pathstart g" and |
3439 path_img:"path_image g \<subseteq> s - (zeros \<union> poles)" and |
4674 path_img:"path_image g \<subseteq> s - pz" and |
3440 homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and |
4675 homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number g z = 0" and |
3441 finite:"finite (zeros \<union> poles)" and |
4676 finite:"finite pz" and |
3442 poles:"\<forall>p\<in>poles. is_pole f p" |
4677 poles:"\<forall>p\<in>poles. is_pole f p" |
3443 shows "contour_integral g (\<lambda>x. deriv f x * h x / f x) = 2 * pi * \<i> * |
4678 shows "contour_integral g (\<lambda>x. deriv f x * h x / f x) = 2 * pi * \<i> * |
3444 ((\<Sum>p\<in>zeros. winding_number g p * h p * zorder f p) |
4679 (\<Sum>p\<in>pz. winding_number g p * h p * zorder f p)" |
3445 - (\<Sum>p\<in>poles. winding_number g p * h p * porder f p))" |
|
3446 (is "?L=?R") |
4680 (is "?L=?R") |
3447 proof - |
4681 proof - |
3448 define c where "c \<equiv> 2 * complex_of_real pi * \<i> " |
4682 define c where "c \<equiv> 2 * complex_of_real pi * \<i> " |
3449 define ff where "ff \<equiv> (\<lambda>x. deriv f x * h x / f x)" |
4683 define ff where "ff \<equiv> (\<lambda>x. deriv f x * h x / f x)" |
3450 define cont_pole where "cont_pole \<equiv> \<lambda>ff p e. (ff has_contour_integral - c * porder f p * h p) (circlepath p e)" |
4684 define cont where "cont \<equiv> \<lambda>ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)" |
3451 define cont_zero where "cont_zero \<equiv> \<lambda>ff p e. (ff has_contour_integral c * zorder f p * h p ) (circlepath p e)" |
4685 define avoid where "avoid \<equiv> \<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pz)" |
3452 define avoid where "avoid \<equiv> \<lambda>p e. \<forall>w\<in>cball p e. w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> zeros \<union> poles)" |
4686 |
3453 have "\<exists>e>0. avoid p e \<and> (p\<in>poles \<longrightarrow> cont_pole ff p e) \<and> (p\<in>zeros \<longrightarrow> cont_zero ff p e)" |
4687 have "\<exists>e>0. avoid p e \<and> (p\<in>pz \<longrightarrow> cont ff p e)" when "p\<in>s" for p |
3454 when "p\<in>s" for p |
4688 proof - |
|
4689 obtain e1 where "e1>0" and e1_avoid:"avoid p e1" |
|
4690 using finite_cball_avoid[OF \<open>open s\<close> finite] \<open>p\<in>s\<close> unfolding avoid_def by auto |
|
4691 have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> cont ff p e2" when "p\<in>pz" |
3455 proof - |
4692 proof - |
3456 obtain e1 where "e1>0" and e1_avoid:"avoid p e1" |
4693 define po where "po \<equiv> zorder f p" |
3457 using finite_cball_avoid[OF \<open>open s\<close> finite] \<open>p\<in>s\<close> unfolding avoid_def by auto |
4694 define pp where "pp \<equiv> zor_poly f p" |
3458 have "\<exists>e2>0. cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2" |
4695 define f' where "f' \<equiv> \<lambda>w. pp w * (w - p) powr po" |
3459 when "p\<in>poles" |
4696 define ff' where "ff' \<equiv> (\<lambda>x. deriv f' x * h x / f' x)" |
|
4697 obtain r where "pp p\<noteq>0" "r>0" and |
|
4698 "r<e1" and |
|
4699 pp_holo:"pp holomorphic_on cball p r" and |
|
4700 pp_po:"(\<forall>w\<in>cball p r-{p}. f w = pp w * (w - p) powr po \<and> pp w \<noteq> 0)" |
|
4701 proof - |
|
4702 have "isolated_singularity_at f p" |
3460 proof - |
4703 proof - |
3461 define po where "po \<equiv> porder f p" |
|
3462 define pp where "pp \<equiv> pol_poly f p" |
|
3463 define f' where "f' \<equiv> \<lambda>w. pp w / (w - p) ^ po" |
|
3464 define ff' where "ff' \<equiv> (\<lambda>x. deriv f' x * h x / f' x)" |
|
3465 have "f holomorphic_on ball p e1 - {p}" |
4704 have "f holomorphic_on ball p e1 - {p}" |
3466 apply (intro holomorphic_on_subset[OF f_holo]) |
4705 apply (intro holomorphic_on_subset[OF f_holo]) |
3467 using e1_avoid \<open>p\<in>poles\<close> unfolding avoid_def by auto |
4706 using e1_avoid \<open>p\<in>pz\<close> unfolding avoid_def pz_def by force |
3468 then obtain r where |
4707 then show ?thesis unfolding isolated_singularity_at_def |
3469 "0 < po" "r>0" |
4708 using \<open>e1>0\<close> analytic_on_open open_delete by blast |
3470 "cball p r \<subseteq> ball p e1" and |
4709 qed |
3471 pp_holo:"pp holomorphic_on cball p r" and |
4710 moreover have "not_essential f p" |
3472 pp_po:"(\<forall>w\<in>cball p r. (w\<noteq>p \<longrightarrow> f w = pp w / (w - p) ^ po) \<and> pp w \<noteq> 0)" |
4711 proof (cases "is_pole f p") |
3473 using porder_exist[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>] poles \<open>p\<in>poles\<close> |
4712 case True |
3474 unfolding po_def pp_def |
4713 then show ?thesis unfolding not_essential_def by auto |
|
4714 next |
|
4715 case False |
|
4716 then have "p\<in>s-poles" using \<open>p\<in>s\<close> poles unfolding pz_def by auto |
|
4717 moreover have "open (s-poles)" |
|
4718 using \<open>open s\<close> |
|
4719 apply (elim open_Diff) |
|
4720 apply (rule finite_imp_closed) |
|
4721 using finite unfolding pz_def by simp |
|
4722 ultimately have "isCont f p" |
|
4723 using holomorphic_on_imp_continuous_on[OF f_holo] continuous_on_eq_continuous_at |
3475 by auto |
4724 by auto |
3476 define e2 where "e2 \<equiv> r/2" |
4725 then show ?thesis unfolding isCont_def not_essential_def by auto |
3477 have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto |
4726 qed |
3478 define anal where "anal \<equiv> \<lambda>w. deriv pp w * h w / pp w" |
4727 moreover have "\<exists>\<^sub>F w in at p. f w \<noteq> 0 " |
3479 define prin where "prin \<equiv> \<lambda>w. - of_nat po * h w / (w - p)" |
4728 proof (rule ccontr) |
3480 have "((\<lambda>w. prin w + anal w) has_contour_integral - c * po * h p) (circlepath p e2)" |
4729 assume "\<not> (\<exists>\<^sub>F w in at p. f w \<noteq> 0)" |
3481 proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified]) |
4730 then have "\<forall>\<^sub>F w in at p. f w= 0" unfolding frequently_def by auto |
3482 have "ball p r \<subseteq> s" |
4731 then obtain rr where "rr>0" "\<forall>w\<in>ball p rr - {p}. f w =0" |
3483 using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e1_avoid by blast |
4732 unfolding eventually_at by (auto simp add:dist_commute) |
3484 then have "cball p e2 \<subseteq> s" |
4733 then have "ball p rr - {p} \<subseteq> {w\<in>ball p rr-{p}. f w=0}" by blast |
3485 using \<open>r>0\<close> unfolding e2_def by auto |
4734 moreover have "infinite (ball p rr - {p})" using \<open>rr>0\<close> using finite_imp_not_open by fastforce |
3486 then have "(\<lambda>w. - of_nat po * h w) holomorphic_on cball p e2" |
4735 ultimately have "infinite {w\<in>ball p rr-{p}. f w=0}" using infinite_super by blast |
3487 using h_holo |
4736 then have "infinite pz" |
3488 by (auto intro!: holomorphic_intros) |
4737 unfolding pz_def infinite_super by auto |
3489 then show "(prin has_contour_integral - c * of_nat po * h p ) (circlepath p e2)" |
4738 then show False using \<open>finite pz\<close> by auto |
3490 using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. - of_nat po * h w"] |
|
3491 \<open>e2>0\<close> |
|
3492 unfolding prin_def |
|
3493 by (auto simp add: mult.assoc) |
|
3494 have "anal holomorphic_on ball p r" unfolding anal_def |
|
3495 using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close> |
|
3496 by (auto intro!: holomorphic_intros) |
|
3497 then show "(anal has_contour_integral 0) (circlepath p e2)" |
|
3498 using e2_def \<open>r>0\<close> |
|
3499 by (auto elim!: Cauchy_theorem_disc_simple) |
|
3500 qed |
|
3501 then have "cont_pole ff' p e2" unfolding cont_pole_def po_def |
|
3502 proof (elim has_contour_integral_eq) |
|
3503 fix w assume "w \<in> path_image (circlepath p e2)" |
|
3504 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto |
|
3505 define wp where "wp \<equiv> w-p" |
|
3506 have "wp\<noteq>0" and "pp w \<noteq>0" |
|
3507 unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto |
|
3508 moreover have der_f':"deriv f' w = - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po" |
|
3509 proof (rule DERIV_imp_deriv) |
|
3510 define der where "der \<equiv> - po * pp w / (w-p)^(po+1) + deriv pp w / (w-p)^po" |
|
3511 have po:"po = Suc (po - Suc 0) " using \<open>po>0\<close> by auto |
|
3512 have "(pp has_field_derivative (deriv pp w)) (at w)" |
|
3513 using DERIV_deriv_iff_has_field_derivative pp_holo \<open>w\<noteq>p\<close> |
|
3514 by (meson open_ball \<open>w \<in> ball p r\<close> ball_subset_cball holomorphic_derivI holomorphic_on_subset) |
|
3515 then show "(f' has_field_derivative der) (at w)" |
|
3516 using \<open>w\<noteq>p\<close> \<open>po>0\<close> unfolding der_def f'_def |
|
3517 apply (auto intro!: derivative_eq_intros simp add:field_simps) |
|
3518 apply (subst (4) po) |
|
3519 apply (subst power_Suc) |
|
3520 by (auto simp add:field_simps) |
|
3521 qed |
|
3522 ultimately show "prin w + anal w = ff' w" |
|
3523 unfolding ff'_def prin_def anal_def |
|
3524 apply simp |
|
3525 apply (unfold f'_def) |
|
3526 apply (fold wp_def) |
|
3527 by (auto simp add:field_simps) |
|
3528 qed |
|
3529 then have "cont_pole ff p e2" unfolding cont_pole_def |
|
3530 proof (elim has_contour_integral_eq) |
|
3531 fix w assume "w \<in> path_image (circlepath p e2)" |
|
3532 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto |
|
3533 have "deriv f' w = deriv f w" |
|
3534 proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"]) |
|
3535 show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo |
|
3536 by (auto intro!: holomorphic_intros) |
|
3537 next |
|
3538 have "ball p e1 - {p} \<subseteq> s - poles" |
|
3539 using avoid_def ball_subset_cball e1_avoid |
|
3540 by auto |
|
3541 then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close> |
|
3542 using ball_subset_cball by blast |
|
3543 then show "f holomorphic_on ball p r - {p}" using f_holo |
|
3544 by auto |
|
3545 next |
|
3546 show "open (ball p r - {p})" by auto |
|
3547 next |
|
3548 show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto |
|
3549 next |
|
3550 fix x assume "x \<in> ball p r - {p}" |
|
3551 then show "f' x = f x" |
|
3552 using pp_po unfolding f'_def by auto |
|
3553 qed |
|
3554 moreover have " f' w = f w " |
|
3555 using \<open>w \<in> ball p r\<close> ball_subset_cball subset_iff pp_po \<open>w\<noteq>p\<close> |
|
3556 unfolding f'_def by auto |
|
3557 ultimately show "ff' w = ff w" |
|
3558 unfolding ff'_def ff_def by simp |
|
3559 qed |
|
3560 moreover have "cball p e2 \<subseteq> ball p e1" |
|
3561 using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto |
|
3562 ultimately show ?thesis using \<open>e2>0\<close> by auto |
|
3563 qed |
4739 qed |
3564 then obtain e2 where e2:"p\<in>poles \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> cont_pole ff p e2" |
4740 ultimately obtain r where "pp p \<noteq> 0" and r:"r>0" "pp holomorphic_on cball p r" |
3565 by auto |
4741 "(\<forall>w\<in>cball p r - {p}. f w = pp w * (w - p) powr of_int po \<and> pp w \<noteq> 0)" |
3566 have "\<exists>e3>0. cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3" |
4742 using zorder_exist[of f p,folded po_def pp_def] by auto |
3567 when "p\<in>zeros" |
4743 define r1 where "r1=min r e1 / 2" |
3568 proof - |
4744 have "r1<e1" unfolding r1_def using \<open>e1>0\<close> \<open>r>0\<close> by auto |
3569 define zo where "zo \<equiv> zorder f p" |
4745 moreover have "r1>0" "pp holomorphic_on cball p r1" |
3570 define zp where "zp \<equiv> zer_poly f p" |
4746 "(\<forall>w\<in>cball p r1 - {p}. f w = pp w * (w - p) powr of_int po \<and> pp w \<noteq> 0)" |
3571 define f' where "f' \<equiv> \<lambda>w. zp w * (w - p) ^ zo" |
4747 unfolding r1_def using \<open>e1>0\<close> r by auto |
3572 define ff' where "ff' \<equiv> (\<lambda>x. deriv f' x * h x / f' x)" |
4748 ultimately show ?thesis using that \<open>pp p\<noteq>0\<close> by auto |
3573 have "f holomorphic_on ball p e1" |
4749 qed |
3574 proof - |
4750 |
3575 have "ball p e1 \<subseteq> s - poles" |
4751 define e2 where "e2 \<equiv> r/2" |
3576 using avoid_def ball_subset_cball e1_avoid that zeros_def by fastforce |
4752 have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto |
3577 thus ?thesis using f_holo by auto |
4753 define anal where "anal \<equiv> \<lambda>w. deriv pp w * h w / pp w" |
3578 qed |
4754 define prin where "prin \<equiv> \<lambda>w. po * h w / (w - p)" |
3579 moreover have "f p = 0" using \<open>p\<in>zeros\<close> |
4755 have "((\<lambda>w. prin w + anal w) has_contour_integral c * po * h p) (circlepath p e2)" |
3580 using DiffD1 mem_Collect_eq zeros_def by blast |
4756 proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified]) |
3581 moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0" |
4757 have "ball p r \<subseteq> s" |
3582 proof - |
4758 using \<open>r<e1\<close> avoid_def ball_subset_cball e1_avoid by (simp add: subset_eq) |
3583 define p' where "p' \<equiv> p+e1/2" |
4759 then have "cball p e2 \<subseteq> s" |
3584 have "p' \<in> ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm) |
4760 using \<open>r>0\<close> unfolding e2_def by auto |
3585 then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e1_avoid unfolding avoid_def |
4761 then have "(\<lambda>w. po * h w) holomorphic_on cball p e2" |
3586 apply (rule_tac x=p' in bexI) |
4762 using h_holo by (auto intro!: holomorphic_intros) |
3587 by (auto simp add:zeros_def) |
4763 then show "(prin has_contour_integral c * po * h p ) (circlepath p e2)" |
3588 qed |
4764 using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. po * h w"] \<open>e2>0\<close> |
3589 ultimately obtain r where |
4765 unfolding prin_def by (auto simp add: mult.assoc) |
3590 "0 < zo" "r>0" |
4766 have "anal holomorphic_on ball p r" unfolding anal_def |
3591 "cball p r \<subseteq> ball p e1" and |
4767 using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close> \<open>pp p\<noteq>0\<close> |
3592 pp_holo:"zp holomorphic_on cball p r" and |
4768 by (auto intro!: holomorphic_intros) |
3593 pp_po:"(\<forall>w\<in>cball p r. f w = zp w * (w - p) ^ zo \<and> zp w \<noteq> 0)" |
4769 then show "(anal has_contour_integral 0) (circlepath p e2)" |
3594 using zorder_exist[of "ball p e1" p f,simplified,OF \<open>e1>0\<close>] unfolding zo_def zp_def |
4770 using e2_def \<open>r>0\<close> |
|
4771 by (auto elim!: Cauchy_theorem_disc_simple) |
|
4772 qed |
|
4773 then have "cont ff' p e2" unfolding cont_def po_def |
|
4774 proof (elim has_contour_integral_eq) |
|
4775 fix w assume "w \<in> path_image (circlepath p e2)" |
|
4776 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto |
|
4777 define wp where "wp \<equiv> w-p" |
|
4778 have "wp\<noteq>0" and "pp w \<noteq>0" |
|
4779 unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto |
|
4780 moreover have der_f':"deriv f' w = po * pp w * (w-p) powr (po - 1) + deriv pp w * (w-p) powr po" |
|
4781 proof (rule DERIV_imp_deriv) |
|
4782 have "(pp has_field_derivative (deriv pp w)) (at w)" |
|
4783 using DERIV_deriv_iff_has_field_derivative pp_holo \<open>w\<noteq>p\<close> |
|
4784 by (meson open_ball \<open>w \<in> ball p r\<close> ball_subset_cball holomorphic_derivI holomorphic_on_subset) |
|
4785 then show " (f' has_field_derivative of_int po * pp w * (w - p) powr of_int (po - 1) |
|
4786 + deriv pp w * (w - p) powr of_int po) (at w)" |
|
4787 unfolding f'_def using \<open>w\<noteq>p\<close> |
|
4788 apply (auto intro!: derivative_eq_intros(35) DERIV_cong[OF has_field_derivative_powr_of_int]) |
|
4789 by (auto intro: derivative_eq_intros) |
|
4790 qed |
|
4791 ultimately show "prin w + anal w = ff' w" |
|
4792 unfolding ff'_def prin_def anal_def |
|
4793 apply simp |
|
4794 apply (unfold f'_def) |
|
4795 apply (fold wp_def) |
|
4796 apply (auto simp add:field_simps) |
|
4797 by (metis (no_types, lifting) diff_add_cancel mult.commute powr_add powr_to_1) |
|
4798 qed |
|
4799 then have "cont ff p e2" unfolding cont_def |
|
4800 proof (elim has_contour_integral_eq) |
|
4801 fix w assume "w \<in> path_image (circlepath p e2)" |
|
4802 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto |
|
4803 have "deriv f' w = deriv f w" |
|
4804 proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"]) |
|
4805 show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo |
|
4806 by (auto intro!: holomorphic_intros) |
|
4807 next |
|
4808 have "ball p e1 - {p} \<subseteq> s - poles" |
|
4809 using ball_subset_cball e1_avoid[unfolded avoid_def] unfolding pz_def |
3595 by auto |
4810 by auto |
3596 define e2 where "e2 \<equiv> r/2" |
4811 then have "ball p r - {p} \<subseteq> s - poles" |
3597 have "e2>0" using \<open>r>0\<close> unfolding e2_def by auto |
4812 apply (elim dual_order.trans) |
3598 define anal where "anal \<equiv> \<lambda>w. deriv zp w * h w / zp w" |
4813 using \<open>r<e1\<close> by auto |
3599 define prin where "prin \<equiv> \<lambda>w. of_nat zo * h w / (w - p)" |
4814 then show "f holomorphic_on ball p r - {p}" using f_holo |
3600 have "((\<lambda>w. prin w + anal w) has_contour_integral c * zo * h p) (circlepath p e2)" |
4815 by auto |
3601 proof (rule has_contour_integral_add[of _ _ _ _ 0,simplified]) |
4816 next |
3602 have "ball p r \<subseteq> s" |
4817 show "open (ball p r - {p})" by auto |
3603 using \<open>cball p r \<subseteq> ball p e1\<close> avoid_def ball_subset_cball e1_avoid by blast |
4818 show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto |
3604 then have "cball p e2 \<subseteq> s" |
4819 next |
3605 using \<open>r>0\<close> unfolding e2_def by auto |
4820 fix x assume "x \<in> ball p r - {p}" |
3606 then have "(\<lambda>w. of_nat zo * h w) holomorphic_on cball p e2" |
4821 then show "f' x = f x" |
3607 using h_holo |
4822 using pp_po unfolding f'_def by auto |
3608 by (auto intro!: holomorphic_intros) |
|
3609 then show "(prin has_contour_integral c * of_nat zo * h p ) (circlepath p e2)" |
|
3610 using Cauchy_integral_circlepath_simple[folded c_def, of "\<lambda>w. of_nat zo * h w"] |
|
3611 \<open>e2>0\<close> |
|
3612 unfolding prin_def |
|
3613 by (auto simp add: mult.assoc) |
|
3614 have "anal holomorphic_on ball p r" unfolding anal_def |
|
3615 using pp_holo h_holo pp_po \<open>ball p r \<subseteq> s\<close> |
|
3616 by (auto intro!: holomorphic_intros) |
|
3617 then show "(anal has_contour_integral 0) (circlepath p e2)" |
|
3618 using e2_def \<open>r>0\<close> |
|
3619 by (auto elim!: Cauchy_theorem_disc_simple) |
|
3620 qed |
|
3621 then have "cont_zero ff' p e2" unfolding cont_zero_def zo_def |
|
3622 proof (elim has_contour_integral_eq) |
|
3623 fix w assume "w \<in> path_image (circlepath p e2)" |
|
3624 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto |
|
3625 define wp where "wp \<equiv> w-p" |
|
3626 have "wp\<noteq>0" and "zp w \<noteq>0" |
|
3627 unfolding wp_def using \<open>w\<noteq>p\<close> \<open>w\<in>ball p r\<close> pp_po by auto |
|
3628 moreover have der_f':"deriv f' w = zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" |
|
3629 proof (rule DERIV_imp_deriv) |
|
3630 define der where "der \<equiv> zo * zp w * (w-p)^(zo-1) + deriv zp w * (w-p)^zo" |
|
3631 have po:"zo = Suc (zo - Suc 0) " using \<open>zo>0\<close> by auto |
|
3632 have "(zp has_field_derivative (deriv zp w)) (at w)" |
|
3633 using DERIV_deriv_iff_has_field_derivative pp_holo |
|
3634 by (meson open_ball \<open>w \<in> ball p r\<close> ball_subset_cball holomorphic_derivI holomorphic_on_subset) |
|
3635 then show "(f' has_field_derivative der) (at w)" |
|
3636 using \<open>w\<noteq>p\<close> \<open>zo>0\<close> unfolding der_def f'_def |
|
3637 by (auto intro!: derivative_eq_intros simp add:field_simps) |
|
3638 qed |
|
3639 ultimately show "prin w + anal w = ff' w" |
|
3640 unfolding ff'_def prin_def anal_def |
|
3641 apply simp |
|
3642 apply (unfold f'_def) |
|
3643 apply (fold wp_def) |
|
3644 apply (auto simp add:field_simps) |
|
3645 by (metis Suc_diff_Suc minus_nat.diff_0 power_Suc) |
|
3646 qed |
|
3647 then have "cont_zero ff p e2" unfolding cont_zero_def |
|
3648 proof (elim has_contour_integral_eq) |
|
3649 fix w assume "w \<in> path_image (circlepath p e2)" |
|
3650 then have "w\<in>ball p r" and "w\<noteq>p" unfolding e2_def using \<open>r>0\<close> by auto |
|
3651 have "deriv f' w = deriv f w" |
|
3652 proof (rule complex_derivative_transform_within_open[where s="ball p r - {p}"]) |
|
3653 show "f' holomorphic_on ball p r - {p}" unfolding f'_def using pp_holo |
|
3654 by (auto intro!: holomorphic_intros) |
|
3655 next |
|
3656 have "ball p e1 - {p} \<subseteq> s - poles" |
|
3657 using avoid_def ball_subset_cball e1_avoid by auto |
|
3658 then have "ball p r - {p} \<subseteq> s - poles" using \<open>cball p r \<subseteq> ball p e1\<close> |
|
3659 using ball_subset_cball by blast |
|
3660 then show "f holomorphic_on ball p r - {p}" using f_holo |
|
3661 by auto |
|
3662 next |
|
3663 show "open (ball p r - {p})" by auto |
|
3664 next |
|
3665 show "w \<in> ball p r - {p}" using \<open>w\<in>ball p r\<close> \<open>w\<noteq>p\<close> by auto |
|
3666 next |
|
3667 fix x assume "x \<in> ball p r - {p}" |
|
3668 then show "f' x = f x" |
|
3669 using pp_po unfolding f'_def by auto |
|
3670 qed |
|
3671 moreover have " f' w = f w " |
|
3672 using \<open>w \<in> ball p r\<close> ball_subset_cball subset_iff pp_po unfolding f'_def by auto |
|
3673 ultimately show "ff' w = ff w" |
|
3674 unfolding ff'_def ff_def by simp |
|
3675 qed |
|
3676 moreover have "cball p e2 \<subseteq> ball p e1" |
|
3677 using \<open>0 < r\<close> \<open>cball p r \<subseteq> ball p e1\<close> e2_def by auto |
|
3678 ultimately show ?thesis using \<open>e2>0\<close> by auto |
|
3679 qed |
4823 qed |
3680 then obtain e3 where e3:"p\<in>zeros \<longrightarrow> e3>0 \<and> cball p e3 \<subseteq> ball p e1 \<and> cont_zero ff p e3" |
4824 moreover have " f' w = f w " |
3681 by auto |
4825 using \<open>w \<in> ball p r\<close> ball_subset_cball subset_iff pp_po \<open>w\<noteq>p\<close> |
3682 define e4 where "e4 \<equiv> if p\<in>poles then e2 else if p\<in>zeros then e3 else e1" |
4826 unfolding f'_def by auto |
3683 have "e4>0" using e2 e3 \<open>e1>0\<close> unfolding e4_def by auto |
4827 ultimately show "ff' w = ff w" |
3684 moreover have "avoid p e4" using e2 e3 \<open>e1>0\<close> e1_avoid unfolding e4_def avoid_def by auto |
4828 unfolding ff'_def ff_def by simp |
3685 moreover have "p\<in>poles \<longrightarrow> cont_pole ff p e4" and "p\<in>zeros \<longrightarrow> cont_zero ff p e4" |
4829 qed |
3686 by (auto simp add: e2 e3 e4_def zeros_def) |
4830 moreover have "cball p e2 \<subseteq> ball p e1" |
3687 ultimately show ?thesis by auto |
4831 using \<open>0 < r\<close> \<open>r<e1\<close> e2_def by auto |
3688 qed |
4832 ultimately show ?thesis using \<open>e2>0\<close> by auto |
|
4833 qed |
|
4834 then obtain e2 where e2:"p\<in>pz \<longrightarrow> e2>0 \<and> cball p e2 \<subseteq> ball p e1 \<and> cont ff p e2" |
|
4835 by auto |
|
4836 define e4 where "e4 \<equiv> if p\<in>pz then e2 else e1" |
|
4837 have "e4>0" using e2 \<open>e1>0\<close> unfolding e4_def by auto |
|
4838 moreover have "avoid p e4" using e2 \<open>e1>0\<close> e1_avoid unfolding e4_def avoid_def by auto |
|
4839 moreover have "p\<in>pz \<longrightarrow> cont ff p e4" |
|
4840 by (auto simp add: e2 e4_def) |
|
4841 ultimately show ?thesis by auto |
|
4842 qed |
3689 then obtain get_e where get_e:"\<forall>p\<in>s. get_e p>0 \<and> avoid p (get_e p) |
4843 then obtain get_e where get_e:"\<forall>p\<in>s. get_e p>0 \<and> avoid p (get_e p) |
3690 \<and> (p\<in>poles \<longrightarrow> cont_pole ff p (get_e p)) \<and> (p\<in>zeros \<longrightarrow> cont_zero ff p (get_e p))" |
4844 \<and> (p\<in>pz \<longrightarrow> cont ff p (get_e p))" |
3691 by metis |
4845 by metis |
3692 define cont where "cont \<equiv> \<lambda>p. contour_integral (circlepath p (get_e p)) ff" |
4846 define ci where "ci \<equiv> \<lambda>p. contour_integral (circlepath p (get_e p)) ff" |
3693 define w where "w \<equiv> \<lambda>p. winding_number g p" |
4847 define w where "w \<equiv> \<lambda>p. winding_number g p" |
3694 have "contour_integral g ff = (\<Sum>p\<in>zeros \<union> poles. w p * cont p)" |
4848 have "contour_integral g ff = (\<Sum>p\<in>pz. w p * ci p)" unfolding ci_def w_def |
3695 unfolding cont_def w_def |
4849 proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> \<open>connected s\<close> finite _ \<open>valid_path g\<close> loop |
3696 proof (rule Cauchy_theorem_singularities[OF \<open>open s\<close> \<open>connected s\<close> finite _ \<open>valid_path g\<close> loop |
|
3697 path_img homo]) |
4850 path_img homo]) |
3698 have "open (s - (zeros \<union> poles))" using open_Diff[OF _ finite_imp_closed[OF finite]] \<open>open s\<close> by auto |
4851 have "open (s - pz)" using open_Diff[OF _ finite_imp_closed[OF finite]] \<open>open s\<close> by auto |
3699 then show "ff holomorphic_on s - (zeros \<union> poles)" unfolding ff_def using f_holo h_holo |
4852 then show "ff holomorphic_on s - pz" unfolding ff_def using f_holo h_holo |
3700 by (auto intro!: holomorphic_intros simp add:zeros_def) |
4853 by (auto intro!: holomorphic_intros simp add:pz_def) |
|
4854 next |
|
4855 show "\<forall>p\<in>s. 0 < get_e p \<and> (\<forall>w\<in>cball p (get_e p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> pz))" |
|
4856 using get_e using avoid_def by blast |
|
4857 qed |
|
4858 also have "... = (\<Sum>p\<in>pz. c * w p * h p * zorder f p)" |
|
4859 proof (rule sum.cong[of pz pz,simplified]) |
|
4860 fix p assume "p \<in> pz" |
|
4861 show "w p * ci p = c * w p * h p * (zorder f p)" |
|
4862 proof (cases "p\<in>s") |
|
4863 assume "p \<in> s" |
|
4864 have "ci p = c * h p * (zorder f p)" unfolding ci_def |
|
4865 apply (rule contour_integral_unique) |
|
4866 using get_e \<open>p\<in>s\<close> \<open>p\<in>pz\<close> unfolding cont_def by (metis mult.assoc mult.commute) |
|
4867 thus ?thesis by auto |
3701 next |
4868 next |
3702 show "\<forall>p\<in>s. 0 < get_e p \<and> (\<forall>w\<in>cball p (get_e p). w \<in> s \<and> (w \<noteq> p \<longrightarrow> w \<notin> zeros \<union> poles))" |
4869 assume "p\<notin>s" |
3703 using get_e using avoid_def by blast |
4870 then have "w p=0" using homo unfolding w_def by auto |
3704 qed |
4871 then show ?thesis by auto |
3705 also have "... = (\<Sum>p\<in>zeros. w p * cont p) + (\<Sum>p\<in>poles. w p * cont p)" |
4872 qed |
3706 using finite |
4873 qed |
3707 apply (subst sum.union_disjoint) |
4874 also have "... = c*(\<Sum>p\<in>pz. w p * h p * zorder f p)" |
3708 by (auto simp add:zeros_def) |
4875 unfolding sum_distrib_left by (simp add:algebra_simps) |
3709 also have "... = c * ((\<Sum>p\<in>zeros. w p * h p * zorder f p) - (\<Sum>p\<in>poles. w p * h p * porder f p))" |
4876 finally have "contour_integral g ff = c * (\<Sum>p\<in>pz. w p * h p * of_int (zorder f p))" . |
3710 proof - |
4877 then show ?thesis unfolding ff_def c_def w_def by simp |
3711 have "(\<Sum>p\<in>zeros. w p * cont p) = (\<Sum>p\<in>zeros. c * w p * h p * zorder f p)" |
|
3712 proof (rule sum.cong[of zeros zeros,simplified]) |
|
3713 fix p assume "p \<in> zeros" |
|
3714 show "w p * cont p = c * w p * h p * (zorder f p)" |
|
3715 proof (cases "p\<in>s") |
|
3716 assume "p \<in> s" |
|
3717 have "cont p = c * h p * (zorder f p)" unfolding cont_def |
|
3718 apply (rule contour_integral_unique) |
|
3719 using get_e \<open>p\<in>s\<close> \<open>p\<in>zeros\<close> unfolding cont_zero_def |
|
3720 by (metis mult.assoc mult.commute) |
|
3721 thus ?thesis by auto |
|
3722 next |
|
3723 assume "p\<notin>s" |
|
3724 then have "w p=0" using homo unfolding w_def by auto |
|
3725 then show ?thesis by auto |
|
3726 qed |
|
3727 qed |
|
3728 then have "(\<Sum>p\<in>zeros. w p * cont p) = c * (\<Sum>p\<in>zeros. w p * h p * zorder f p)" |
|
3729 apply (subst sum_distrib_left) |
|
3730 by (simp add:algebra_simps) |
|
3731 moreover have "(\<Sum>p\<in>poles. w p * cont p) = (\<Sum>p\<in>poles. - c * w p * h p * porder f p)" |
|
3732 proof (rule sum.cong[of poles poles,simplified]) |
|
3733 fix p assume "p \<in> poles" |
|
3734 show "w p * cont p = - c * w p * h p * (porder f p)" |
|
3735 proof (cases "p\<in>s") |
|
3736 assume "p \<in> s" |
|
3737 have "cont p = - c * h p * (porder f p)" unfolding cont_def |
|
3738 apply (rule contour_integral_unique) |
|
3739 using get_e \<open>p\<in>s\<close> \<open>p\<in>poles\<close> unfolding cont_pole_def |
|
3740 by (metis mult.assoc mult.commute) |
|
3741 thus ?thesis by auto |
|
3742 next |
|
3743 assume "p\<notin>s" |
|
3744 then have "w p=0" using homo unfolding w_def by auto |
|
3745 then show ?thesis by auto |
|
3746 qed |
|
3747 qed |
|
3748 then have "(\<Sum>p\<in>poles. w p * cont p) = - c * (\<Sum>p\<in>poles. w p * h p * porder f p)" |
|
3749 apply (subst sum_distrib_left) |
|
3750 by (simp add:algebra_simps) |
|
3751 ultimately show ?thesis by (simp add: right_diff_distrib) |
|
3752 qed |
|
3753 finally show ?thesis unfolding w_def ff_def c_def by auto |
|
3754 qed |
4878 qed |
3755 |
4879 |
3756 subsection \<open>Rouche's theorem \<close> |
4880 subsection \<open>Rouche's theorem \<close> |
3757 |
4881 |
3758 theorem Rouche_theorem: |
4882 theorem Rouche_theorem: |
3772 homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number \<gamma> z = 0" |
4896 homo:"\<forall>z. (z \<notin> s) \<longrightarrow> winding_number \<gamma> z = 0" |
3773 shows "(\<Sum>p\<in>zeros_fg. winding_number \<gamma> p * zorder fg p) |
4897 shows "(\<Sum>p\<in>zeros_fg. winding_number \<gamma> p * zorder fg p) |
3774 = (\<Sum>p\<in>zeros_f. winding_number \<gamma> p * zorder f p)" |
4898 = (\<Sum>p\<in>zeros_f. winding_number \<gamma> p * zorder f p)" |
3775 proof - |
4899 proof - |
3776 have path_fg:"path_image \<gamma> \<subseteq> s - zeros_fg" |
4900 have path_fg:"path_image \<gamma> \<subseteq> s - zeros_fg" |
|
4901 proof - |
|
4902 have False when "z\<in>path_image \<gamma>" and "f z + g z=0" for z |
3777 proof - |
4903 proof - |
3778 have False when "z\<in>path_image \<gamma>" and "f z + g z=0" for z |
4904 have "cmod (f z) > cmod (g z)" using \<open>z\<in>path_image \<gamma>\<close> path_less by auto |
3779 proof - |
4905 moreover have "f z = - g z" using \<open>f z + g z =0\<close> by (simp add: eq_neg_iff_add_eq_0) |
3780 have "cmod (f z) > cmod (g z)" using \<open>z\<in>path_image \<gamma>\<close> path_less by auto |
4906 then have "cmod (f z) = cmod (g z)" by auto |
3781 moreover have "f z = - g z" using \<open>f z + g z =0\<close> by (simp add: eq_neg_iff_add_eq_0) |
4907 ultimately show False by auto |
3782 then have "cmod (f z) = cmod (g z)" by auto |
4908 qed |
3783 ultimately show False by auto |
4909 then show ?thesis unfolding zeros_fg_def fg_def using path_img by auto |
3784 qed |
4910 qed |
3785 then show ?thesis unfolding zeros_fg_def fg_def using path_img by auto |
|
3786 qed |
|
3787 have path_f:"path_image \<gamma> \<subseteq> s - zeros_f" |
4911 have path_f:"path_image \<gamma> \<subseteq> s - zeros_f" |
|
4912 proof - |
|
4913 have False when "z\<in>path_image \<gamma>" and "f z =0" for z |
3788 proof - |
4914 proof - |
3789 have False when "z\<in>path_image \<gamma>" and "f z =0" for z |
4915 have "cmod (g z) < cmod (f z) " using \<open>z\<in>path_image \<gamma>\<close> path_less by auto |
3790 proof - |
4916 then have "cmod (g z) < 0" using \<open>f z=0\<close> by auto |
3791 have "cmod (g z) < cmod (f z) " using \<open>z\<in>path_image \<gamma>\<close> path_less by auto |
4917 then show False by auto |
3792 then have "cmod (g z) < 0" using \<open>f z=0\<close> by auto |
4918 qed |
3793 then show False by auto |
4919 then show ?thesis unfolding zeros_f_def using path_img by auto |
3794 qed |
4920 qed |
3795 then show ?thesis unfolding zeros_f_def using path_img by auto |
|
3796 qed |
|
3797 define w where "w \<equiv> \<lambda>p. winding_number \<gamma> p" |
4921 define w where "w \<equiv> \<lambda>p. winding_number \<gamma> p" |
3798 define c where "c \<equiv> 2 * complex_of_real pi * \<i>" |
4922 define c where "c \<equiv> 2 * complex_of_real pi * \<i>" |
3799 define h where "h \<equiv> \<lambda>p. g p / f p + 1" |
4923 define h where "h \<equiv> \<lambda>p. g p / f p + 1" |
3800 obtain spikes |
4924 obtain spikes |
3801 where "finite spikes" and spikes: "\<forall>x\<in>{0..1} - spikes. \<gamma> differentiable at x" |
4925 where "finite spikes" and spikes: "\<forall>x\<in>{0..1} - spikes. \<gamma> differentiable at x" |
3802 using \<open>valid_path \<gamma>\<close> |
4926 using \<open>valid_path \<gamma>\<close> |
3803 by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
4927 by (auto simp: valid_path_def piecewise_C1_differentiable_on_def C1_differentiable_on_eq) |
3804 have h_contour:"((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" |
4928 have h_contour:"((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" |
|
4929 proof - |
|
4930 have outside_img:"0 \<in> outside (path_image (h o \<gamma>))" |
3805 proof - |
4931 proof - |
3806 have outside_img:"0 \<in> outside (path_image (h o \<gamma>))" |
4932 have "h p \<in> ball 1 1" when "p\<in>path_image \<gamma>" for p |
3807 proof - |
4933 proof - |
3808 have "h p \<in> ball 1 1" when "p\<in>path_image \<gamma>" for p |
4934 have "cmod (g p/f p) <1" using path_less[rule_format,OF that] |
3809 proof - |
4935 apply (cases "cmod (f p) = 0") |
3810 have "cmod (g p/f p) <1" using path_less[rule_format,OF that] |
4936 by (auto simp add: norm_divide) |
3811 apply (cases "cmod (f p) = 0") |
4937 then show ?thesis unfolding h_def by (auto simp add:dist_complex_def) |
3812 by (auto simp add: norm_divide) |
4938 qed |
3813 then show ?thesis unfolding h_def by (auto simp add:dist_complex_def) |
4939 then have "path_image (h o \<gamma>) \<subseteq> ball 1 1" |
3814 qed |
4940 by (simp add: image_subset_iff path_image_compose) |
3815 then have "path_image (h o \<gamma>) \<subseteq> ball 1 1" |
4941 moreover have " (0::complex) \<notin> ball 1 1" by (simp add: dist_norm) |
3816 by (simp add: image_subset_iff path_image_compose) |
4942 ultimately show "?thesis" |
3817 moreover have " (0::complex) \<notin> ball 1 1" by (simp add: dist_norm) |
4943 using convex_in_outside[of "ball 1 1" 0] outside_mono by blast |
3818 ultimately show "?thesis" |
4944 qed |
3819 using convex_in_outside[of "ball 1 1" 0] outside_mono by blast |
4945 have valid_h:"valid_path (h \<circ> \<gamma>)" |
3820 qed |
4946 proof (rule valid_path_compose_holomorphic[OF \<open>valid_path \<gamma>\<close> _ _ path_f]) |
3821 have valid_h:"valid_path (h \<circ> \<gamma>)" |
4947 show "h holomorphic_on s - zeros_f" |
3822 proof (rule valid_path_compose_holomorphic[OF \<open>valid_path \<gamma>\<close> _ _ path_f]) |
4948 unfolding h_def using f_holo g_holo |
3823 show "h holomorphic_on s - zeros_f" |
4949 by (auto intro!: holomorphic_intros simp add:zeros_f_def) |
3824 unfolding h_def using f_holo g_holo |
4950 next |
3825 by (auto intro!: holomorphic_intros simp add:zeros_f_def) |
4951 show "open (s - zeros_f)" using \<open>finite zeros_f\<close> \<open>open s\<close> finite_imp_closed |
3826 next |
|
3827 show "open (s - zeros_f)" using \<open>finite zeros_f\<close> \<open>open s\<close> finite_imp_closed |
|
3828 by auto |
|
3829 qed |
|
3830 have "((\<lambda>z. 1/z) has_contour_integral 0) (h \<circ> \<gamma>)" |
|
3831 proof - |
|
3832 have "0 \<notin> path_image (h \<circ> \<gamma>)" using outside_img by (simp add: outside_def) |
|
3833 then have "((\<lambda>z. 1/z) has_contour_integral c * winding_number (h \<circ> \<gamma>) 0) (h \<circ> \<gamma>)" |
|
3834 using has_contour_integral_winding_number[of "h o \<gamma>" 0,simplified] valid_h |
|
3835 unfolding c_def by auto |
|
3836 moreover have "winding_number (h o \<gamma>) 0 = 0" |
|
3837 proof - |
|
3838 have "0 \<in> outside (path_image (h \<circ> \<gamma>))" using outside_img . |
|
3839 moreover have "path (h o \<gamma>)" |
|
3840 using valid_h by (simp add: valid_path_imp_path) |
|
3841 moreover have "pathfinish (h o \<gamma>) = pathstart (h o \<gamma>)" |
|
3842 by (simp add: loop pathfinish_compose pathstart_compose) |
|
3843 ultimately show ?thesis using winding_number_zero_in_outside by auto |
|
3844 qed |
|
3845 ultimately show ?thesis by auto |
|
3846 qed |
|
3847 moreover have "vector_derivative (h \<circ> \<gamma>) (at x) = vector_derivative \<gamma> (at x) * deriv h (\<gamma> x)" |
|
3848 when "x\<in>{0..1} - spikes" for x |
|
3849 proof (rule vector_derivative_chain_at_general) |
|
3850 show "\<gamma> differentiable at x" using that \<open>valid_path \<gamma>\<close> spikes by auto |
|
3851 next |
|
3852 define der where "der \<equiv> \<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)" |
|
3853 define t where "t \<equiv> \<gamma> x" |
|
3854 have "f t\<noteq>0" unfolding zeros_f_def t_def |
|
3855 by (metis DiffD1 image_eqI norm_not_less_zero norm_zero path_defs(4) path_less that) |
|
3856 moreover have "t\<in>s" |
|
3857 using contra_subsetD path_image_def path_fg t_def that by fastforce |
|
3858 ultimately have "(h has_field_derivative der t) (at t)" |
|
3859 unfolding h_def der_def using g_holo f_holo \<open>open s\<close> |
|
3860 by (auto intro!: holomorphic_derivI derivative_eq_intros) |
|
3861 then show "h field_differentiable at (\<gamma> x)" |
|
3862 unfolding t_def field_differentiable_def by blast |
|
3863 qed |
|
3864 then have " ((/) 1 has_contour_integral 0) (h \<circ> \<gamma>) |
|
3865 = ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" |
|
3866 unfolding has_contour_integral |
|
3867 apply (intro has_integral_spike_eq[OF negligible_finite, OF \<open>finite spikes\<close>]) |
|
3868 by auto |
4952 by auto |
|
4953 qed |
|
4954 have "((\<lambda>z. 1/z) has_contour_integral 0) (h \<circ> \<gamma>)" |
|
4955 proof - |
|
4956 have "0 \<notin> path_image (h \<circ> \<gamma>)" using outside_img by (simp add: outside_def) |
|
4957 then have "((\<lambda>z. 1/z) has_contour_integral c * winding_number (h \<circ> \<gamma>) 0) (h \<circ> \<gamma>)" |
|
4958 using has_contour_integral_winding_number[of "h o \<gamma>" 0,simplified] valid_h |
|
4959 unfolding c_def by auto |
|
4960 moreover have "winding_number (h o \<gamma>) 0 = 0" |
|
4961 proof - |
|
4962 have "0 \<in> outside (path_image (h \<circ> \<gamma>))" using outside_img . |
|
4963 moreover have "path (h o \<gamma>)" |
|
4964 using valid_h by (simp add: valid_path_imp_path) |
|
4965 moreover have "pathfinish (h o \<gamma>) = pathstart (h o \<gamma>)" |
|
4966 by (simp add: loop pathfinish_compose pathstart_compose) |
|
4967 ultimately show ?thesis using winding_number_zero_in_outside by auto |
|
4968 qed |
3869 ultimately show ?thesis by auto |
4969 ultimately show ?thesis by auto |
3870 qed |
4970 qed |
|
4971 moreover have "vector_derivative (h \<circ> \<gamma>) (at x) = vector_derivative \<gamma> (at x) * deriv h (\<gamma> x)" |
|
4972 when "x\<in>{0..1} - spikes" for x |
|
4973 proof (rule vector_derivative_chain_at_general) |
|
4974 show "\<gamma> differentiable at x" using that \<open>valid_path \<gamma>\<close> spikes by auto |
|
4975 next |
|
4976 define der where "der \<equiv> \<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)" |
|
4977 define t where "t \<equiv> \<gamma> x" |
|
4978 have "f t\<noteq>0" unfolding zeros_f_def t_def |
|
4979 by (metis DiffD1 image_eqI norm_not_less_zero norm_zero path_defs(4) path_less that) |
|
4980 moreover have "t\<in>s" |
|
4981 using contra_subsetD path_image_def path_fg t_def that by fastforce |
|
4982 ultimately have "(h has_field_derivative der t) (at t)" |
|
4983 unfolding h_def der_def using g_holo f_holo \<open>open s\<close> |
|
4984 by (auto intro!: holomorphic_derivI derivative_eq_intros) |
|
4985 then show "h field_differentiable at (\<gamma> x)" |
|
4986 unfolding t_def field_differentiable_def by blast |
|
4987 qed |
|
4988 then have " ((/) 1 has_contour_integral 0) (h \<circ> \<gamma>) |
|
4989 = ((\<lambda>x. deriv h x / h x) has_contour_integral 0) \<gamma>" |
|
4990 unfolding has_contour_integral |
|
4991 apply (intro has_integral_spike_eq[OF negligible_finite, OF \<open>finite spikes\<close>]) |
|
4992 by auto |
|
4993 ultimately show ?thesis by auto |
|
4994 qed |
3871 then have "contour_integral \<gamma> (\<lambda>x. deriv h x / h x) = 0" |
4995 then have "contour_integral \<gamma> (\<lambda>x. deriv h x / h x) = 0" |
3872 using contour_integral_unique by simp |
4996 using contour_integral_unique by simp |
3873 moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = contour_integral \<gamma> (\<lambda>x. deriv f x / f x) |
4997 moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = contour_integral \<gamma> (\<lambda>x. deriv f x / f x) |
3874 + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)" |
4998 + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)" |
|
4999 proof - |
|
5000 have "(\<lambda>p. deriv f p / f p) contour_integrable_on \<gamma>" |
|
5001 proof (rule contour_integrable_holomorphic_simple[OF _ _ \<open>valid_path \<gamma>\<close> path_f]) |
|
5002 show "open (s - zeros_f)" using finite_imp_closed[OF \<open>finite zeros_f\<close>] \<open>open s\<close> |
|
5003 by auto |
|
5004 then show "(\<lambda>p. deriv f p / f p) holomorphic_on s - zeros_f" |
|
5005 using f_holo |
|
5006 by (auto intro!: holomorphic_intros simp add:zeros_f_def) |
|
5007 qed |
|
5008 moreover have "(\<lambda>p. deriv h p / h p) contour_integrable_on \<gamma>" |
|
5009 using h_contour |
|
5010 by (simp add: has_contour_integral_integrable) |
|
5011 ultimately have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x + deriv h x / h x) = |
|
5012 contour_integral \<gamma> (\<lambda>p. deriv f p / f p) + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)" |
|
5013 using contour_integral_add[of "(\<lambda>p. deriv f p / f p)" \<gamma> "(\<lambda>p. deriv h p / h p)" ] |
|
5014 by auto |
|
5015 moreover have "deriv fg p / fg p = deriv f p / f p + deriv h p / h p" |
|
5016 when "p\<in> path_image \<gamma>" for p |
3875 proof - |
5017 proof - |
3876 have "(\<lambda>p. deriv f p / f p) contour_integrable_on \<gamma>" |
5018 have "fg p\<noteq>0" and "f p\<noteq>0" using path_f path_fg that unfolding zeros_f_def zeros_fg_def |
3877 proof (rule contour_integrable_holomorphic_simple[OF _ _ \<open>valid_path \<gamma>\<close> path_f]) |
|
3878 show "open (s - zeros_f)" using finite_imp_closed[OF \<open>finite zeros_f\<close>] \<open>open s\<close> |
|
3879 by auto |
|
3880 then show "(\<lambda>p. deriv f p / f p) holomorphic_on s - zeros_f" |
|
3881 using f_holo |
|
3882 by (auto intro!: holomorphic_intros simp add:zeros_f_def) |
|
3883 qed |
|
3884 moreover have "(\<lambda>p. deriv h p / h p) contour_integrable_on \<gamma>" |
|
3885 using h_contour |
|
3886 by (simp add: has_contour_integral_integrable) |
|
3887 ultimately have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x + deriv h x / h x) = |
|
3888 contour_integral \<gamma> (\<lambda>p. deriv f p / f p) + contour_integral \<gamma> (\<lambda>p. deriv h p / h p)" |
|
3889 using contour_integral_add[of "(\<lambda>p. deriv f p / f p)" \<gamma> "(\<lambda>p. deriv h p / h p)" ] |
|
3890 by auto |
5019 by auto |
3891 moreover have "deriv fg p / fg p = deriv f p / f p + deriv h p / h p" |
5020 have "h p\<noteq>0" |
3892 when "p\<in> path_image \<gamma>" for p |
5021 proof (rule ccontr) |
3893 proof - |
5022 assume "\<not> h p \<noteq> 0" |
3894 have "fg p\<noteq>0" and "f p\<noteq>0" using path_f path_fg that unfolding zeros_f_def zeros_fg_def |
5023 then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2) |
3895 by auto |
5024 then have "cmod (g p/f p) = 1" by auto |
3896 have "h p\<noteq>0" |
5025 moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that] |
3897 proof (rule ccontr) |
5026 apply (cases "cmod (f p) = 0") |
3898 assume "\<not> h p \<noteq> 0" |
5027 by (auto simp add: norm_divide) |
3899 then have "g p / f p= -1" unfolding h_def by (simp add: add_eq_0_iff2) |
5028 ultimately show False by auto |
3900 then have "cmod (g p/f p) = 1" by auto |
5029 qed |
3901 moreover have "cmod (g p/f p) <1" using path_less[rule_format,OF that] |
5030 have der_fg:"deriv fg p = deriv f p + deriv g p" unfolding fg_def |
3902 apply (cases "cmod (f p) = 0") |
5031 using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>] path_img that |
3903 by (auto simp add: norm_divide) |
5032 by auto |
3904 ultimately show False by auto |
5033 have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)" |
3905 qed |
5034 proof - |
3906 have der_fg:"deriv fg p = deriv f p + deriv g p" unfolding fg_def |
5035 define der where "der \<equiv> \<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)" |
3907 using f_holo g_holo holomorphic_on_imp_differentiable_at[OF _ \<open>open s\<close>] path_img that |
5036 have "p\<in>s" using path_img that by auto |
3908 by auto |
5037 then have "(h has_field_derivative der p) (at p)" |
3909 have der_h:"deriv h p = (deriv g p * f p - g p * deriv f p)/(f p * f p)" |
5038 unfolding h_def der_def using g_holo f_holo \<open>open s\<close> \<open>f p\<noteq>0\<close> |
3910 proof - |
5039 by (auto intro!: derivative_eq_intros holomorphic_derivI) |
3911 define der where "der \<equiv> \<lambda>p. (deriv g p * f p - g p * deriv f p)/(f p * f p)" |
5040 then show ?thesis unfolding der_def using DERIV_imp_deriv by auto |
3912 have "p\<in>s" using path_img that by auto |
5041 qed |
3913 then have "(h has_field_derivative der p) (at p)" |
5042 show ?thesis |
3914 unfolding h_def der_def using g_holo f_holo \<open>open s\<close> \<open>f p\<noteq>0\<close> |
5043 apply (simp only:der_fg der_h) |
3915 by (auto intro!: derivative_eq_intros holomorphic_derivI) |
5044 apply (auto simp add:field_simps \<open>h p\<noteq>0\<close> \<open>f p\<noteq>0\<close> \<open>fg p\<noteq>0\<close>) |
3916 then show ?thesis unfolding der_def using DERIV_imp_deriv by auto |
5045 by (auto simp add:field_simps h_def \<open>f p\<noteq>0\<close> fg_def) |
3917 qed |
5046 qed |
3918 show ?thesis |
5047 then have "contour_integral \<gamma> (\<lambda>p. deriv fg p / fg p) |
3919 apply (simp only:der_fg der_h) |
5048 = contour_integral \<gamma> (\<lambda>p. deriv f p / f p + deriv h p / h p)" |
3920 apply (auto simp add:field_simps \<open>h p\<noteq>0\<close> \<open>f p\<noteq>0\<close> \<open>fg p\<noteq>0\<close>) |
5049 by (elim contour_integral_eq) |
3921 by (auto simp add:field_simps h_def \<open>f p\<noteq>0\<close> fg_def) |
5050 ultimately show ?thesis by auto |
3922 qed |
5051 qed |
3923 then have "contour_integral \<gamma> (\<lambda>p. deriv fg p / fg p) |
|
3924 = contour_integral \<gamma> (\<lambda>p. deriv f p / f p + deriv h p / h p)" |
|
3925 by (elim contour_integral_eq) |
|
3926 ultimately show ?thesis by auto |
|
3927 qed |
|
3928 moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)" |
5052 moreover have "contour_integral \<gamma> (\<lambda>x. deriv fg x / fg x) = c * (\<Sum>p\<in>zeros_fg. w p * zorder fg p)" |
3929 unfolding c_def zeros_fg_def w_def |
5053 unfolding c_def zeros_fg_def w_def |
3930 proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo |
5054 proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo |
3931 , of _ "{}" "\<lambda>_. 1",simplified]) |
5055 , of _ "{}" "\<lambda>_. 1",simplified]) |
3932 show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto |
5056 show "fg holomorphic_on s" unfolding fg_def using f_holo g_holo holomorphic_on_add by auto |
3933 show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def . |
5057 show "path_image \<gamma> \<subseteq> s - {p. fg p = 0}" using path_fg unfolding zeros_fg_def . |
3934 show " finite {p. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def . |
5058 show " finite {p. fg p = 0}" using \<open>finite zeros_fg\<close> unfolding zeros_fg_def . |
3935 qed |
5059 qed |
3936 moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)" |
5060 moreover have "contour_integral \<gamma> (\<lambda>x. deriv f x / f x) = c * (\<Sum>p\<in>zeros_f. w p * zorder f p)" |
3937 unfolding c_def zeros_f_def w_def |
5061 unfolding c_def zeros_f_def w_def |
3938 proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo |
5062 proof (rule argument_principle[OF \<open>open s\<close> \<open>connected s\<close> _ _ \<open>valid_path \<gamma>\<close> loop _ homo |
3939 , of _ "{}" "\<lambda>_. 1",simplified]) |
5063 , of _ "{}" "\<lambda>_. 1",simplified]) |
3940 show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto |
5064 show "f holomorphic_on s" using f_holo g_holo holomorphic_on_add by auto |
3941 show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def . |
5065 show "path_image \<gamma> \<subseteq> s - {p. f p = 0}" using path_f unfolding zeros_f_def . |
3942 show " finite {p. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def . |
5066 show " finite {p. f p = 0}" using \<open>finite zeros_f\<close> unfolding zeros_f_def . |
3943 qed |
5067 qed |
3944 ultimately have " c* (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))" |
5068 ultimately have " c* (\<Sum>p\<in>zeros_fg. w p * (zorder fg p)) = c* (\<Sum>p\<in>zeros_f. w p * (zorder f p))" |
3945 by auto |
5069 by auto |
3946 then show ?thesis unfolding c_def using w_def by auto |
5070 then show ?thesis unfolding c_def using w_def by auto |
3947 qed |
5071 qed |
3948 |
5072 |
3949 |
|
3950 subsection \<open>More facts about poles and residues\<close> |
|
3951 |
|
3952 lemma zorder_cong: |
|
3953 assumes "eventually (\<lambda>z. f z = g z) (nhds z)" "z = z'" |
|
3954 shows "zorder f z = zorder g z'" |
|
3955 proof - |
|
3956 let ?P = "(\<lambda>f n h r. 0 < r \<and> h holomorphic_on cball z r \<and> |
|
3957 (\<forall>w\<in>cball z r. f w = h w * (w - z) ^ n \<and> h w \<noteq> 0))" |
|
3958 have "(\<lambda>n. n > 0 \<and> (\<exists>h r. ?P f n h r)) = (\<lambda>n. n > 0 \<and> (\<exists>h r. ?P g n h r))" |
|
3959 proof (intro ext conj_cong refl iff_exI[where ?'a = "complex \<Rightarrow> complex"], goal_cases) |
|
3960 case (1 n h) |
|
3961 have *: "\<exists>r. ?P g n h r" if "\<exists>r. ?P f n h r" and "eventually (\<lambda>x. f x = g x) (nhds z)" for f g |
|
3962 proof - |
|
3963 from that(1) obtain r where "?P f n h r" by blast |
|
3964 moreover from that(2) obtain r' where "r' > 0" "\<And>w. dist w z < r' \<Longrightarrow> f w = g w" |
|
3965 by (auto simp: eventually_nhds_metric) |
|
3966 hence "\<forall>w\<in>cball z (r'/2). f w = g w" by (auto simp: dist_commute) |
|
3967 ultimately show ?thesis using \<open>r' > 0\<close> |
|
3968 by (intro exI[of _ "min r (r'/2)"]) (auto simp: cball_def) |
|
3969 qed |
|
3970 from assms have eq': "eventually (\<lambda>z. g z = f z) (nhds z)" |
|
3971 by (simp add: eq_commute) |
|
3972 show ?case |
|
3973 by (rule iffI[OF *[OF _ assms(1)] *[OF _ eq']]) |
|
3974 qed |
|
3975 with assms(2) show ?thesis unfolding zorder_def by simp |
|
3976 qed |
|
3977 |
|
3978 lemma porder_cong: |
|
3979 assumes "eventually (\<lambda>z. f z = g z) (at z)" "z = z'" |
|
3980 shows "porder f z = porder g z'" |
|
3981 proof - |
|
3982 from assms(1) have *: "eventually (\<lambda>w. w \<noteq> z \<longrightarrow> f w = g w) (nhds z)" |
|
3983 by (auto simp: eventually_at_filter) |
|
3984 from assms(2) show ?thesis |
|
3985 unfolding porder_def Let_def |
|
3986 by (intro zorder_cong eventually_mono [OF *]) auto |
|
3987 qed |
|
3988 |
|
3989 lemma zer_poly_cong: |
|
3990 assumes "eventually (\<lambda>z. f z = g z) (nhds z)" "z = z'" |
|
3991 shows "zer_poly f z = zer_poly g z'" |
|
3992 unfolding zer_poly_def |
|
3993 proof (rule Eps_cong, goal_cases) |
|
3994 case (1 h) |
|
3995 let ?P = "\<lambda>w f. f w = h w * (w - z) ^ zorder f z \<and> h w \<noteq> 0" |
|
3996 from assms have eq': "eventually (\<lambda>z. g z = f z) (nhds z)" |
|
3997 by (simp add: eq_commute) |
|
3998 have "\<exists>r>0. h holomorphic_on cball z r \<and> (\<forall>w\<in>cball z r. ?P w g)" |
|
3999 if "r > 0" "h holomorphic_on cball z r" "\<And>w. w \<in> cball z r \<Longrightarrow> ?P w f" |
|
4000 "eventually (\<lambda>z. f z = g z) (nhds z)" for f g r |
|
4001 proof - |
|
4002 from that have [simp]: "zorder f z = zorder g z" |
|
4003 by (intro zorder_cong) auto |
|
4004 from that(4) obtain r' where r': "r' > 0" "\<And>w. w \<in> ball z r' \<Longrightarrow> g w = f w" |
|
4005 by (auto simp: eventually_nhds_metric ball_def dist_commute) |
|
4006 define R where "R = min r (r' / 2)" |
|
4007 have "R > 0" "cball z R \<subseteq> cball z r" "cball z R \<subseteq> ball z r'" |
|
4008 using that(1) r' by (auto simp: R_def) |
|
4009 with that(1,2,3) r' |
|
4010 have "R > 0" "h holomorphic_on cball z R" "\<forall>w\<in>cball z R. ?P w g" |
|
4011 by force+ |
|
4012 thus ?thesis by blast |
|
4013 qed |
|
4014 from this[of _ f g] and this[of _ g f] and assms and eq' |
|
4015 show ?case by blast |
|
4016 qed |
|
4017 |
|
4018 lemma pol_poly_cong: |
|
4019 assumes "eventually (\<lambda>z. f z = g z) (at z)" "z = z'" |
|
4020 shows "pol_poly f z = pol_poly g z'" |
|
4021 proof - |
|
4022 from assms have *: "eventually (\<lambda>w. w \<noteq> z \<longrightarrow> f w = g w) (nhds z)" |
|
4023 by (auto simp: eventually_at_filter) |
|
4024 have "zer_poly (\<lambda>x. if x = z then 0 else inverse (f x)) z = |
|
4025 zer_poly (\<lambda>x. if x = z' then 0 else inverse (g x)) z" |
|
4026 by (intro zer_poly_cong eventually_mono[OF *] refl) (auto simp: assms(2)) |
|
4027 thus "pol_poly f z = pol_poly g z'" |
|
4028 by (simp add: pol_poly_def Let_def o_def fun_eq_iff assms(2)) |
|
4029 qed |
|
4030 |
|
4031 lemma porder_nonzero_div_power: |
|
4032 assumes "open s" "z \<in> s" "f holomorphic_on s" "f z \<noteq> 0" "n > 0" |
|
4033 shows "porder (\<lambda>w. f w / (w - z) ^ n) z = n" |
|
4034 proof - |
|
4035 let ?s' = "(f -` (-{0}) \<inter> s)" |
|
4036 have "continuous_on s f" |
|
4037 by (rule holomorphic_on_imp_continuous_on) fact |
|
4038 moreover have "open (-{0::complex})" by auto |
|
4039 ultimately have s': "open ?s'" |
|
4040 unfolding continuous_on_open_vimage[OF \<open>open s\<close>] by blast |
|
4041 show ?thesis unfolding Let_def porder_def |
|
4042 proof (rule zorder_eqI) |
|
4043 show "(\<lambda>x. inverse (f x)) holomorphic_on ?s'" |
|
4044 using assms by (auto intro!: holomorphic_intros) |
|
4045 qed (insert assms s', auto simp: field_simps) |
|
4046 qed |
|
4047 |
|
4048 lemma is_pole_inverse_power: "n > 0 \<Longrightarrow> is_pole (\<lambda>z::complex. 1 / (z - a) ^ n) a" |
|
4049 unfolding is_pole_def inverse_eq_divide [symmetric] |
|
4050 by (intro filterlim_compose[OF filterlim_inverse_at_infinity] tendsto_intros) |
|
4051 (auto simp: filterlim_at eventually_at intro!: exI[of _ 1] tendsto_eq_intros) |
|
4052 |
|
4053 lemma is_pole_inverse: "is_pole (\<lambda>z::complex. 1 / (z - a)) a" |
|
4054 using is_pole_inverse_power[of 1 a] by simp |
|
4055 |
|
4056 lemma is_pole_divide: |
|
4057 fixes f :: "'a :: t2_space \<Rightarrow> 'b :: real_normed_field" |
|
4058 assumes "isCont f z" "filterlim g (at 0) (at z)" "f z \<noteq> 0" |
|
4059 shows "is_pole (\<lambda>z. f z / g z) z" |
|
4060 proof - |
|
4061 have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)" |
|
4062 by (intro tendsto_mult_filterlim_at_infinity[of _ "f z"] |
|
4063 filterlim_compose[OF filterlim_inverse_at_infinity])+ |
|
4064 (insert assms, auto simp: isCont_def) |
|
4065 thus ?thesis by (simp add: divide_simps is_pole_def) |
|
4066 qed |
|
4067 |
|
4068 lemma is_pole_basic: |
|
4069 assumes "f holomorphic_on A" "open A" "z \<in> A" "f z \<noteq> 0" "n > 0" |
|
4070 shows "is_pole (\<lambda>w. f w / (w - z) ^ n) z" |
|
4071 proof (rule is_pole_divide) |
|
4072 have "continuous_on A f" by (rule holomorphic_on_imp_continuous_on) fact |
|
4073 with assms show "isCont f z" by (auto simp: continuous_on_eq_continuous_at) |
|
4074 have "filterlim (\<lambda>w. (w - z) ^ n) (nhds 0) (at z)" |
|
4075 using assms by (auto intro!: tendsto_eq_intros) |
|
4076 thus "filterlim (\<lambda>w. (w - z) ^ n) (at 0) (at z)" |
|
4077 by (intro filterlim_atI tendsto_eq_intros) |
|
4078 (insert assms, auto simp: eventually_at_filter) |
|
4079 qed fact+ |
|
4080 |
|
4081 lemma is_pole_basic': |
|
4082 assumes "f holomorphic_on A" "open A" "0 \<in> A" "f 0 \<noteq> 0" "n > 0" |
|
4083 shows "is_pole (\<lambda>w. f w / w ^ n) 0" |
|
4084 using is_pole_basic[of f A 0] assms by simp |
|
4085 |
|
4086 lemma zer_poly_eq: |
|
4087 assumes "open s" "connected s" "z \<in> s" "f holomorphic_on s" "f z = 0" "\<exists>w\<in>s. f w \<noteq> 0" |
|
4088 shows "eventually (\<lambda>w. zer_poly f z w = f w / (w - z) ^ zorder f z) (at z)" |
|
4089 proof - |
|
4090 from zorder_exist [OF assms] obtain r where r: "r > 0" |
|
4091 and "\<forall>w\<in>cball z r. f w = zer_poly f z w * (w - z) ^ zorder f z" by blast |
|
4092 hence *: "\<forall>w\<in>ball z r - {z}. zer_poly f z w = f w / (w - z) ^ zorder f z" |
|
4093 by (auto simp: field_simps) |
|
4094 have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)" |
|
4095 using r eventually_at_ball'[of r z UNIV] by auto |
|
4096 thus ?thesis by eventually_elim (insert *, auto) |
|
4097 qed |
|
4098 |
|
4099 lemma pol_poly_eq: |
|
4100 assumes "open s" "z \<in> s" "f holomorphic_on s - {z}" "is_pole f z" "\<exists>w\<in>s. f w \<noteq> 0" |
|
4101 shows "eventually (\<lambda>w. pol_poly f z w = f w * (w - z) ^ porder f z) (at z)" |
|
4102 proof - |
|
4103 from porder_exist[OF assms(1-4)] obtain r where r: "r > 0" |
|
4104 and "\<forall>w\<in>cball z r. w \<noteq> z \<longrightarrow> f w = pol_poly f z w / (w - z) ^ porder f z" by blast |
|
4105 hence *: "\<forall>w\<in>ball z r - {z}. pol_poly f z w = f w * (w - z) ^ porder f z" |
|
4106 by (auto simp: field_simps) |
|
4107 have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)" |
|
4108 using r eventually_at_ball'[of r z UNIV] by auto |
|
4109 thus ?thesis by eventually_elim (insert *, auto) |
|
4110 qed |
|
4111 |
|
4112 lemma lhopital_complex_simple: |
|
4113 assumes "(f has_field_derivative f') (at z)" |
|
4114 assumes "(g has_field_derivative g') (at z)" |
|
4115 assumes "f z = 0" "g z = 0" "g' \<noteq> 0" "f' / g' = c" |
|
4116 shows "((\<lambda>w. f w / g w) \<longlongrightarrow> c) (at z)" |
|
4117 proof - |
|
4118 have "eventually (\<lambda>w. w \<noteq> z) (at z)" |
|
4119 by (auto simp: eventually_at_filter) |
|
4120 hence "eventually (\<lambda>w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z)) = f w / g w) (at z)" |
|
4121 by eventually_elim (simp add: assms divide_simps) |
|
4122 moreover have "((\<lambda>w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z))) \<longlongrightarrow> f' / g') (at z)" |
|
4123 by (intro tendsto_divide has_field_derivativeD assms) |
|
4124 ultimately have "((\<lambda>w. f w / g w) \<longlongrightarrow> f' / g') (at z)" |
|
4125 by (rule Lim_transform_eventually) |
|
4126 with assms show ?thesis by simp |
|
4127 qed |
|
4128 |
|
4129 lemma porder_eqI: |
|
4130 assumes "open s" "z \<in> s" "g holomorphic_on s" "g z \<noteq> 0" "n > 0" |
|
4131 assumes "\<And>w. w \<in> s - {z} \<Longrightarrow> f w = g w / (w - z) ^ n" |
|
4132 shows "porder f z = n" |
|
4133 proof - |
|
4134 define f' where "f' = (\<lambda>x. if x = z then 0 else inverse (f x))" |
|
4135 define g' where "g' = (\<lambda>x. inverse (g x))" |
|
4136 define s' where "s' = (g -` (-{0}) \<inter> s)" |
|
4137 have "continuous_on s g" |
|
4138 by (intro holomorphic_on_imp_continuous_on) fact |
|
4139 hence "open s'" |
|
4140 unfolding s'_def using assms by (subst (asm) continuous_on_open_vimage) blast+ |
|
4141 have s': "z \<in> s'" "g' holomorphic_on s'" "g' z \<noteq> 0" using assms |
|
4142 by (auto simp: s'_def g'_def intro!: holomorphic_intros) |
|
4143 have f'_g': "f' w = g' w * (w - z) ^ n" if "w \<in> s'" for w |
|
4144 unfolding f'_def g'_def using that \<open>n > 0\<close> |
|
4145 by (auto simp: assms(6) field_simps s'_def) |
|
4146 have "porder f z = zorder f' z" |
|
4147 by (simp add: porder_def f'_def) |
|
4148 also have "\<dots> = n" using assms f'_g' |
|
4149 by (intro zorder_eqI[OF \<open>open s'\<close> s']) (auto simp: f'_def g'_def field_simps s'_def) |
|
4150 finally show ?thesis . |
|
4151 qed |
|
4152 |
|
4153 lemma simple_poleI': |
|
4154 assumes "open s" "connected s" "z \<in> s" |
|
4155 assumes "\<And>w. w \<in> s - {z} \<Longrightarrow> |
|
4156 ((\<lambda>w. inverse (f w)) has_field_derivative f' w) (at w)" |
|
4157 assumes "f holomorphic_on s - {z}" "f' holomorphic_on s" "is_pole f z" "f' z \<noteq> 0" |
|
4158 shows "porder f z = 1" |
|
4159 proof - |
|
4160 define g where "g = (\<lambda>w. if w = z then 0 else inverse (f w))" |
|
4161 from \<open>is_pole f z\<close> have "eventually (\<lambda>w. f w \<noteq> 0) (at z)" |
|
4162 unfolding is_pole_def using filterlim_at_infinity_imp_eventually_ne by blast |
|
4163 then obtain s'' where s'': "open s''" "z \<in> s''" "\<forall>w\<in>s''-{z}. f w \<noteq> 0" |
|
4164 by (auto simp: eventually_at_topological) |
|
4165 from assms(1) and s''(1) have "open (s \<inter> s'')" by auto |
|
4166 then obtain r where r: "r > 0" "ball z r \<subseteq> s \<inter> s''" |
|
4167 using assms(3) s''(2) by (subst (asm) open_contains_ball) blast |
|
4168 define s' where "s' = ball z r" |
|
4169 hence s': "open s'" "connected s'" "z \<in> s'" "s' \<subseteq> s" "\<forall>w\<in>s'-{z}. f w \<noteq> 0" |
|
4170 using r s'' by (auto simp: s'_def) |
|
4171 have s'_ne: "s' - {z} \<noteq> {}" |
|
4172 using r unfolding s'_def by (intro ball_minus_countable_nonempty) auto |
|
4173 |
|
4174 have "porder f z = zorder g z" |
|
4175 by (simp add: porder_def g_def) |
|
4176 also have "\<dots> = 1" |
|
4177 proof (rule simple_zeroI') |
|
4178 fix w assume w: "w \<in> s'" |
|
4179 have [holomorphic_intros]: "g holomorphic_on s'" unfolding g_def using assms s' |
|
4180 by (intro is_pole_inverse_holomorphic holomorphic_on_subset[OF assms(5)]) auto |
|
4181 hence "(g has_field_derivative deriv g w) (at w)" |
|
4182 using w s' by (intro holomorphic_derivI) |
|
4183 also have deriv_g: "deriv g w = f' w" if "w \<in> s' - {z}" for w |
|
4184 proof - |
|
4185 from that have ne: "eventually (\<lambda>w. w \<noteq> z) (nhds w)" |
|
4186 by (intro t1_space_nhds) auto |
|
4187 have "deriv g w = deriv (\<lambda>w. inverse (f w)) w" |
|
4188 by (intro deriv_cong_ev refl eventually_mono [OF ne]) (auto simp: g_def) |
|
4189 also from assms(4)[of w] that s' have "\<dots> = f' w" |
|
4190 by (auto dest: DERIV_imp_deriv) |
|
4191 finally show ?thesis . |
|
4192 qed |
|
4193 have "deriv g w = f' w" |
|
4194 by (rule analytic_continuation_open[of "s' - {z}" s' "deriv g" f']) |
|
4195 (insert s' assms s'_ne deriv_g w, |
|
4196 auto intro!: holomorphic_intros holomorphic_on_subset[OF assms(6)]) |
|
4197 finally show "(g has_field_derivative f' w) (at w)" . |
|
4198 qed (insert assms s', auto simp: g_def) |
|
4199 finally show ?thesis . |
|
4200 qed |
|
4201 |
|
4202 lemma residue_holomorphic_over_power: |
|
4203 assumes "open A" "z0 \<in> A" "f holomorphic_on A" |
|
4204 shows "residue (\<lambda>z. f z / (z - z0) ^ Suc n) z0 = (deriv ^^ n) f z0 / fact n" |
|
4205 proof - |
|
4206 let ?f = "\<lambda>z. f z / (z - z0) ^ Suc n" |
|
4207 from assms(1,2) obtain r where r: "r > 0" "cball z0 r \<subseteq> A" |
|
4208 by (auto simp: open_contains_cball) |
|
4209 have "(?f has_contour_integral 2 * pi * \<i> * residue ?f z0) (circlepath z0 r)" |
|
4210 using r assms by (intro base_residue[of A]) (auto intro!: holomorphic_intros) |
|
4211 moreover have "(?f has_contour_integral 2 * pi * \<i> / fact n * (deriv ^^ n) f z0) (circlepath z0 r)" |
|
4212 using assms r |
|
4213 by (intro Cauchy_has_contour_integral_higher_derivative_circlepath) |
|
4214 (auto intro!: holomorphic_on_subset[OF assms(3)] holomorphic_on_imp_continuous_on) |
|
4215 ultimately have "2 * pi * \<i> * residue ?f z0 = 2 * pi * \<i> / fact n * (deriv ^^ n) f z0" |
|
4216 by (rule has_contour_integral_unique) |
|
4217 thus ?thesis by (simp add: field_simps) |
|
4218 qed |
|
4219 |
|
4220 lemma residue_holomorphic_over_power': |
|
4221 assumes "open A" "0 \<in> A" "f holomorphic_on A" |
|
4222 shows "residue (\<lambda>z. f z / z ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n" |
|
4223 using residue_holomorphic_over_power[OF assms] by simp |
|
4224 |
|
4225 lemma zer_poly_eqI: |
|
4226 fixes f :: "complex \<Rightarrow> complex" and z0 :: complex |
|
4227 defines "n \<equiv> zorder f z0" |
|
4228 assumes "open A" "connected A" "z0 \<in> A" "f holomorphic_on A" "f z0 = 0" "\<exists>z\<in>A. f z \<noteq> 0" |
|
4229 assumes lim: "((\<lambda>x. f (g x) / (g x - z0) ^ n) \<longlongrightarrow> c) F" |
|
4230 assumes g: "filterlim g (at z0) F" and "F \<noteq> bot" |
|
4231 shows "zer_poly f z0 z0 = c" |
|
4232 proof - |
|
4233 from zorder_exist[OF assms(2-7)] obtain r where |
|
4234 r: "r > 0" "cball z0 r \<subseteq> A" "zer_poly f z0 holomorphic_on cball z0 r" |
|
4235 "\<And>w. w \<in> cball z0 r \<Longrightarrow> f w = zer_poly f z0 w * (w - z0) ^ n" |
|
4236 unfolding n_def by blast |
|
4237 from r(1) have "eventually (\<lambda>w. w \<in> ball z0 r \<and> w \<noteq> z0) (at z0)" |
|
4238 using eventually_at_ball'[of r z0 UNIV] by auto |
|
4239 hence "eventually (\<lambda>w. zer_poly f z0 w = f w / (w - z0) ^ n) (at z0)" |
|
4240 by eventually_elim (insert r, auto simp: field_simps) |
|
4241 moreover have "continuous_on (ball z0 r) (zer_poly f z0)" |
|
4242 using r by (intro holomorphic_on_imp_continuous_on) auto |
|
4243 with r(1,2) have "isCont (zer_poly f z0) z0" |
|
4244 by (auto simp: continuous_on_eq_continuous_at) |
|
4245 hence "(zer_poly f z0 \<longlongrightarrow> zer_poly f z0 z0) (at z0)" |
|
4246 unfolding isCont_def . |
|
4247 ultimately have "((\<lambda>w. f w / (w - z0) ^ n) \<longlongrightarrow> zer_poly f z0 z0) (at z0)" |
|
4248 by (rule Lim_transform_eventually) |
|
4249 hence "((\<lambda>x. f (g x) / (g x - z0) ^ n) \<longlongrightarrow> zer_poly f z0 z0) F" |
|
4250 by (rule filterlim_compose[OF _ g]) |
|
4251 from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis . |
|
4252 qed |
|
4253 |
|
4254 lemma pol_poly_eqI: |
|
4255 fixes f :: "complex \<Rightarrow> complex" and z0 :: complex |
|
4256 defines "n \<equiv> porder f z0" |
|
4257 assumes "open A" "z0 \<in> A" "f holomorphic_on A-{z0}" "is_pole f z0" |
|
4258 assumes lim: "((\<lambda>x. f (g x) * (g x - z0) ^ n) \<longlongrightarrow> c) F" |
|
4259 assumes g: "filterlim g (at z0) F" and "F \<noteq> bot" |
|
4260 shows "pol_poly f z0 z0 = c" |
|
4261 proof - |
|
4262 from porder_exist[OF assms(2-5)] obtain r where |
|
4263 r: "r > 0" "cball z0 r \<subseteq> A" "pol_poly f z0 holomorphic_on cball z0 r" |
|
4264 "\<And>w. w \<in> cball z0 r - {z0} \<Longrightarrow> f w = pol_poly f z0 w / (w - z0) ^ n" |
|
4265 unfolding n_def by blast |
|
4266 from r(1) have "eventually (\<lambda>w. w \<in> ball z0 r \<and> w \<noteq> z0) (at z0)" |
|
4267 using eventually_at_ball'[of r z0 UNIV] by auto |
|
4268 hence "eventually (\<lambda>w. pol_poly f z0 w = f w * (w - z0) ^ n) (at z0)" |
|
4269 by eventually_elim (insert r, auto simp: field_simps) |
|
4270 moreover have "continuous_on (ball z0 r) (pol_poly f z0)" |
|
4271 using r by (intro holomorphic_on_imp_continuous_on) auto |
|
4272 with r(1,2) have "isCont (pol_poly f z0) z0" |
|
4273 by (auto simp: continuous_on_eq_continuous_at) |
|
4274 hence "(pol_poly f z0 \<longlongrightarrow> pol_poly f z0 z0) (at z0)" |
|
4275 unfolding isCont_def . |
|
4276 ultimately have "((\<lambda>w. f w * (w - z0) ^ n) \<longlongrightarrow> pol_poly f z0 z0) (at z0)" |
|
4277 by (rule Lim_transform_eventually) |
|
4278 hence "((\<lambda>x. f (g x) * (g x - z0) ^ n) \<longlongrightarrow> pol_poly f z0 z0) F" |
|
4279 by (rule filterlim_compose[OF _ g]) |
|
4280 from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis . |
|
4281 qed |
|
4282 |
|
4283 lemma residue_simple_pole: |
|
4284 assumes "open A" "z0 \<in> A" "f holomorphic_on A - {z0}" |
|
4285 assumes "is_pole f z0" "porder f z0 = 1" |
|
4286 shows "residue f z0 = pol_poly f z0 z0" |
|
4287 using assms by (subst residue_porder[of A]) simp_all |
|
4288 |
|
4289 lemma residue_simple_pole_limit: |
|
4290 assumes "open A" "z0 \<in> A" "f holomorphic_on A - {z0}" |
|
4291 assumes "is_pole f z0" "porder f z0 = 1" |
|
4292 assumes "((\<lambda>x. f (g x) * (g x - z0)) \<longlongrightarrow> c) F" |
|
4293 assumes "filterlim g (at z0) F" "F \<noteq> bot" |
|
4294 shows "residue f z0 = c" |
|
4295 proof - |
|
4296 have "residue f z0 = pol_poly f z0 z0" |
|
4297 by (rule residue_simple_pole assms)+ |
|
4298 also have "\<dots> = c" |
|
4299 using assms by (intro pol_poly_eqI[of A z0 f g c F]) auto |
|
4300 finally show ?thesis . |
|
4301 qed |
|
4302 |
|
4303 (* TODO: This is a mess and could be done much more easily if we had |
|
4304 a nice compositional theory of poles and zeros *) |
|
4305 lemma |
|
4306 assumes "open s" "connected s" "z \<in> s" "f holomorphic_on s" "g holomorphic_on s" |
|
4307 assumes "(g has_field_derivative g') (at z)" |
|
4308 assumes "f z \<noteq> 0" "g z = 0" "g' \<noteq> 0" |
|
4309 shows porder_simple_pole_deriv: "porder (\<lambda>w. f w / g w) z = 1" |
|
4310 and residue_simple_pole_deriv: "residue (\<lambda>w. f w / g w) z = f z / g'" |
|
4311 proof - |
|
4312 have "\<exists>w\<in>s. g w \<noteq> 0" |
|
4313 proof (rule ccontr) |
|
4314 assume *: "\<not>(\<exists>w\<in>s. g w \<noteq> 0)" |
|
4315 have **: "eventually (\<lambda>w. w \<in> s) (nhds z)" |
|
4316 by (intro eventually_nhds_in_open assms) |
|
4317 from * have "deriv g z = deriv (\<lambda>_. 0) z" |
|
4318 by (intro deriv_cong_ev eventually_mono [OF **]) auto |
|
4319 also have "\<dots> = 0" by simp |
|
4320 also from assms have "deriv g z = g'" by (auto dest: DERIV_imp_deriv) |
|
4321 finally show False using \<open>g' \<noteq> 0\<close> by contradiction |
|
4322 qed |
|
4323 then obtain w where w: "w \<in> s" "g w \<noteq> 0" by blast |
|
4324 from isolated_zeros[OF assms(5) assms(1-3,8) w] |
|
4325 obtain r where r: "r > 0" "ball z r \<subseteq> s" "\<And>w. w \<in> ball z r - {z} \<Longrightarrow> g w \<noteq> 0" |
|
4326 by blast |
|
4327 from assms r have holo: "(\<lambda>w. f w / g w) holomorphic_on ball z r - {z}" |
|
4328 by (auto intro!: holomorphic_intros) |
|
4329 |
|
4330 have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)" |
|
4331 using eventually_at_ball'[OF r(1), of z UNIV] by auto |
|
4332 hence "eventually (\<lambda>w. g w \<noteq> 0) (at z)" |
|
4333 by eventually_elim (use r in auto) |
|
4334 moreover have "continuous_on s g" |
|
4335 by (intro holomorphic_on_imp_continuous_on) fact |
|
4336 with assms have "isCont g z" |
|
4337 by (auto simp: continuous_on_eq_continuous_at) |
|
4338 ultimately have "filterlim g (at 0) (at z)" |
|
4339 using \<open>g z = 0\<close> by (auto simp: filterlim_at isCont_def) |
|
4340 moreover have "continuous_on s f" by (intro holomorphic_on_imp_continuous_on) fact |
|
4341 with assms have "isCont f z" |
|
4342 by (auto simp: continuous_on_eq_continuous_at) |
|
4343 ultimately have pole: "is_pole (\<lambda>w. f w / g w) z" |
|
4344 unfolding is_pole_def using \<open>f z \<noteq> 0\<close> |
|
4345 by (intro filterlim_divide_at_infinity[of _ "f z"]) (auto simp: isCont_def) |
|
4346 |
|
4347 have "continuous_on s f" by (intro holomorphic_on_imp_continuous_on) fact |
|
4348 moreover have "open (-{0::complex})" by auto |
|
4349 ultimately have "open (f -` (-{0}) \<inter> s)" using \<open>open s\<close> |
|
4350 by (subst (asm) continuous_on_open_vimage) blast+ |
|
4351 moreover have "z \<in> f -` (-{0}) \<inter> s" using assms by auto |
|
4352 ultimately obtain r' where r': "r' > 0" "ball z r' \<subseteq> f -` (-{0}) \<inter> s" |
|
4353 unfolding open_contains_ball by blast |
|
4354 |
|
4355 let ?D = "\<lambda>w. (f w * deriv g w - g w * deriv f w) / f w ^ 2" |
|
4356 show "porder (\<lambda>w. f w / g w) z = 1" |
|
4357 proof (rule simple_poleI') |
|
4358 show "open (ball z (min r r'))" "connected (ball z (min r r'))" "z \<in> ball z (min r r')" |
|
4359 using r'(1) r(1) by auto |
|
4360 next |
|
4361 fix w assume "w \<in> ball z (min r r') - {z}" |
|
4362 with r' have "w \<in> s" "f w \<noteq> 0" by auto |
|
4363 have "((\<lambda>w. g w / f w) has_field_derivative ?D w) (at w)" |
|
4364 by (rule derivative_eq_intros holomorphic_derivI[OF assms(4)] |
|
4365 holomorphic_derivI[OF assms(5)] | fact)+ |
|
4366 (simp_all add: algebra_simps power2_eq_square) |
|
4367 thus "((\<lambda>w. inverse (f w / g w)) has_field_derivative ?D w) (at w)" |
|
4368 by (simp add: divide_simps) |
|
4369 next |
|
4370 from r' show "?D holomorphic_on ball z (min r r')" |
|
4371 by (intro holomorphic_intros holomorphic_on_subset[OF assms(4)] |
|
4372 holomorphic_on_subset[OF assms(5)]) auto |
|
4373 next |
|
4374 from assms have "deriv g z = g'" |
|
4375 by (auto dest: DERIV_imp_deriv) |
|
4376 with assms r' show "(f z * deriv g z - g z * deriv f z) / (f z)\<^sup>2 \<noteq> 0" |
|
4377 by simp |
|
4378 qed (insert pole holo, auto) |
|
4379 |
|
4380 show "residue (\<lambda>w. f w / g w) z = f z / g'" |
|
4381 proof (rule residue_simple_pole_limit) |
|
4382 show "porder (\<lambda>w. f w / g w) z = 1" by fact |
|
4383 from r show "open (ball z r)" "z \<in> ball z r" by auto |
|
4384 |
|
4385 have "((\<lambda>w. (f w * (w - z)) / g w) \<longlongrightarrow> f z / g') (at z)" |
|
4386 proof (rule lhopital_complex_simple) |
|
4387 show "((\<lambda>w. f w * (w - z)) has_field_derivative f z) (at z)" |
|
4388 using assms by (auto intro!: derivative_eq_intros holomorphic_derivI[OF assms(4)]) |
|
4389 show "(g has_field_derivative g') (at z)" by fact |
|
4390 qed (insert assms, auto) |
|
4391 thus "((\<lambda>w. (f w / g w) * (w - z)) \<longlongrightarrow> f z / g') (at z)" |
|
4392 by (simp add: divide_simps) |
|
4393 qed (insert holo pole, auto simp: filterlim_ident) |
|
4394 qed |
|
4395 |
|
4396 end |
5073 end |