36 |
36 |
37 lemma is_pole_shift_0': |
37 lemma is_pole_shift_0': |
38 fixes f :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector)" |
38 fixes f :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector)" |
39 shows "NO_MATCH 0 z \<Longrightarrow> is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f (z + x)) 0" |
39 shows "NO_MATCH 0 z \<Longrightarrow> is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f (z + x)) 0" |
40 by (metis is_pole_shift_0) |
40 by (metis is_pole_shift_0) |
|
41 |
|
42 lemma is_pole_compose_iff: |
|
43 assumes "filtermap g (at x) = (at y)" |
|
44 shows "is_pole (f \<circ> g) x \<longleftrightarrow> is_pole f y" |
|
45 unfolding is_pole_def filterlim_def filtermap_compose assms .. |
41 |
46 |
42 lemma is_pole_inverse_holomorphic: |
47 lemma is_pole_inverse_holomorphic: |
43 assumes "open s" |
48 assumes "open s" |
44 and f_holo:"f holomorphic_on (s-{z})" |
49 and f_holo:"f holomorphic_on (s-{z})" |
45 and pole:"is_pole f z" |
50 and pole:"is_pole f z" |
206 lemma is_pole_mult_analytic_nonzero2_iff: |
211 lemma is_pole_mult_analytic_nonzero2_iff: |
207 assumes "g analytic_on {x}" "g x \<noteq> 0" |
212 assumes "g analytic_on {x}" "g x \<noteq> 0" |
208 shows "is_pole (\<lambda>x. f x * g x) x \<longleftrightarrow> is_pole f x" |
213 shows "is_pole (\<lambda>x. f x * g x) x \<longleftrightarrow> is_pole f x" |
209 by (subst mult.commute, rule is_pole_mult_analytic_nonzero1_iff) (fact assms)+ |
214 by (subst mult.commute, rule is_pole_mult_analytic_nonzero1_iff) (fact assms)+ |
210 |
215 |
211 text \<open>The proposition |
216 lemma frequently_const_imp_not_is_pole: |
|
217 fixes z :: "'a::first_countable_topology" |
|
218 assumes "frequently (\<lambda>w. f w = c) (at z)" |
|
219 shows "\<not> is_pole f z" |
|
220 proof |
|
221 assume "is_pole f z" |
|
222 from assms have "z islimpt {w. f w = c}" |
|
223 by (simp add: islimpt_conv_frequently_at) |
|
224 then obtain g where g: "\<And>n. g n \<in> {w. f w = c} - {z}" "g \<longlonglongrightarrow> z" |
|
225 unfolding islimpt_sequential by blast |
|
226 then have "(f \<circ> g) \<longlonglongrightarrow> c" |
|
227 by (simp add: tendsto_eventually) |
|
228 moreover have *: "filterlim g (at z) sequentially" |
|
229 using g by (auto simp: filterlim_at) |
|
230 have "filterlim (f \<circ> g) at_infinity sequentially" |
|
231 unfolding o_def by (rule filterlim_compose [OF _ *]) |
|
232 (use \<open>is_pole f z\<close> in \<open>simp add: is_pole_def\<close>) |
|
233 ultimately show False |
|
234 using not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially by blast |
|
235 qed |
|
236 |
|
237 text \<open>The proposition |
212 \<^term>\<open>\<exists>x. ((f::complex\<Rightarrow>complex) \<longlongrightarrow> x) (at z) \<or> is_pole f z\<close> |
238 \<^term>\<open>\<exists>x. ((f::complex\<Rightarrow>complex) \<longlongrightarrow> x) (at z) \<or> is_pole f z\<close> |
213 can be interpreted as the complex function \<^term>\<open>f\<close> has a non-essential singularity at \<^term>\<open>z\<close> |
239 can be interpreted as the complex function \<^term>\<open>f\<close> has a non-essential singularity at \<^term>\<open>z\<close> |
214 (i.e. the singularity is either removable or a pole).\<close> |
240 (i.e. the singularity is either removable or a pole).\<close> |
215 definition not_essential::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where |
241 definition not_essential::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where |
216 "not_essential f z = (\<exists>x. f\<midarrow>z\<rightarrow>x \<or> is_pole f z)" |
242 "not_essential f z = (\<exists>x. f\<midarrow>z\<rightarrow>x \<or> is_pole f z)" |