--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Feb 09 08:35:50 2023 +0000
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy Thu Feb 09 16:29:53 2023 +0000
@@ -417,14 +417,24 @@
(metis centre_in_ball field_differentiable_at_within)
lemma analytic_on_open: "open S \<Longrightarrow> f analytic_on S \<longleftrightarrow> f holomorphic_on S"
-apply (auto simp: analytic_imp_holomorphic)
-apply (auto simp: analytic_on_def holomorphic_on_def)
-by (metis holomorphic_on_def holomorphic_on_subset open_contains_ball)
+ by (meson analytic_imp_holomorphic analytic_on_def holomorphic_on_subset openE)
lemma analytic_on_imp_differentiable_at:
"f analytic_on S \<Longrightarrow> x \<in> S \<Longrightarrow> f field_differentiable (at x)"
- apply (auto simp: analytic_on_def holomorphic_on_def)
-by (metis open_ball centre_in_ball field_differentiable_within_open)
+ using analytic_on_def holomorphic_on_imp_differentiable_at by auto
+
+lemma analytic_at_imp_isCont:
+ assumes "f analytic_on {z}"
+ shows "isCont f z"
+ using assms by (meson analytic_on_imp_differentiable_at field_differentiable_imp_continuous_at insertI1)
+
+lemma analytic_at_neq_imp_eventually_neq:
+ assumes "f analytic_on {x}" "f x \<noteq> c"
+ shows "eventually (\<lambda>y. f y \<noteq> c) (at x)"
+proof (intro tendsto_imp_eventually_ne)
+ show "f \<midarrow>x\<rightarrow> f x"
+ using assms by (simp add: analytic_at_imp_isCont isContD)
+qed (use assms in auto)
lemma analytic_on_subset: "f analytic_on S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> f analytic_on T"
by (auto simp: analytic_on_def)
@@ -652,15 +662,20 @@
lemma analytic_at_ball:
"f analytic_on {z} \<longleftrightarrow> (\<exists>e. 0<e \<and> f holomorphic_on ball z e)"
-by (metis analytic_on_def singleton_iff)
+ by (metis analytic_on_def singleton_iff)
lemma analytic_at:
- "f analytic_on {z} \<longleftrightarrow> (\<exists>s. open s \<and> z \<in> s \<and> f holomorphic_on s)"
-by (metis analytic_on_holomorphic empty_subsetI insert_subset)
+ "f analytic_on {z} \<longleftrightarrow> (\<exists>s. open s \<and> z \<in> s \<and> f holomorphic_on s)"
+ by (metis analytic_on_holomorphic empty_subsetI insert_subset)
+
+lemma holomorphic_on_imp_analytic_at:
+ assumes "f holomorphic_on A" "open A" "z \<in> A"
+ shows "f analytic_on {z}"
+ using assms by (meson analytic_at)
lemma analytic_on_analytic_at:
- "f analytic_on s \<longleftrightarrow> (\<forall>z \<in> s. f analytic_on {z})"
-by (metis analytic_at_ball analytic_on_def)
+ "f analytic_on s \<longleftrightarrow> (\<forall>z \<in> s. f analytic_on {z})"
+ by (metis analytic_at_ball analytic_on_def)
lemma analytic_at_two:
"f analytic_on {z} \<and> g analytic_on {z} \<longleftrightarrow>
--- a/src/HOL/Analysis/Isolated.thy Thu Feb 09 08:35:50 2023 +0000
+++ b/src/HOL/Analysis/Isolated.thy Thu Feb 09 16:29:53 2023 +0000
@@ -14,6 +14,12 @@
definition (in metric_space) uniform_discrete :: "'a set \<Rightarrow> bool" where
"uniform_discrete S \<longleftrightarrow> (\<exists>e>0. \<forall>x\<in>S. \<forall>y\<in>S. dist x y < e \<longrightarrow> x = y)"
+lemma discreteI: "(\<And>x. x \<in> X \<Longrightarrow> x isolated_in X ) \<Longrightarrow> discrete X"
+ unfolding discrete_def by auto
+
+lemma discreteD: "discrete X \<Longrightarrow> x \<in> X \<Longrightarrow> x isolated_in X "
+ unfolding discrete_def by auto
+
lemma uniformI1:
assumes "e>0" "\<And>x y. \<lbrakk>x\<in>S;y\<in>S;dist x y<e\<rbrakk> \<Longrightarrow> x =y "
shows "uniform_discrete S"
@@ -43,6 +49,54 @@
shows "x isolated_in (insert a S) \<longleftrightarrow> x isolated_in S \<or> (x=a \<and> \<not> (x islimpt S))"
by (meson insert_iff islimpt_insert isolated_in_islimpt_iff)
+lemma isolated_inI:
+ assumes "x\<in>S" "open T" "T \<inter> S = {x}"
+ shows "x isolated_in S"
+ using assms unfolding isolated_in_def by auto
+
+lemma isolated_inE:
+ assumes "x isolated_in S"
+ obtains T where "x \<in> S" "open T" "T \<inter> S = {x}"
+ using assms that unfolding isolated_in_def by force
+
+lemma isolated_inE_dist:
+ assumes "x isolated_in S"
+ obtains d where "d > 0" "\<And>y. y \<in> S \<Longrightarrow> dist x y < d \<Longrightarrow> y = x"
+ by (meson assms isolated_in_dist_Ex_iff)
+
+lemma isolated_in_altdef:
+ "x isolated_in S \<longleftrightarrow> (x\<in>S \<and> eventually (\<lambda>y. y \<notin> S) (at x))"
+proof
+ assume "x isolated_in S"
+ from isolated_inE[OF this]
+ obtain T where "x \<in> S" and T:"open T" "T \<inter> S = {x}"
+ by metis
+ have "\<forall>\<^sub>F y in nhds x. y \<in> T"
+ apply (rule eventually_nhds_in_open)
+ using T by auto
+ then have "eventually (\<lambda>y. y \<in> T - {x}) (at x)"
+ unfolding eventually_at_filter by eventually_elim auto
+ then have "eventually (\<lambda>y. y \<notin> S) (at x)"
+ by eventually_elim (use T in auto)
+ then show " x \<in> S \<and> (\<forall>\<^sub>F y in at x. y \<notin> S)" using \<open>x \<in> S\<close> by auto
+next
+ assume "x \<in> S \<and> (\<forall>\<^sub>F y in at x. y \<notin> S)"
+ then have "\<forall>\<^sub>F y in at x. y \<notin> S" "x\<in>S" by auto
+ from this(1) have "eventually (\<lambda>y. y \<notin> S \<or> y = x) (nhds x)"
+ unfolding eventually_at_filter by eventually_elim auto
+ then obtain T where T:"open T" "x \<in> T" "(\<forall>y\<in>T. y \<notin> S \<or> y = x)"
+ unfolding eventually_nhds by auto
+ with \<open>x \<in> S\<close> have "T \<inter> S = {x}"
+ by fastforce
+ with \<open>x\<in>S\<close> \<open>open T\<close>
+ show "x isolated_in S"
+ unfolding isolated_in_def by auto
+qed
+
+lemma discrete_altdef:
+ "discrete S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>\<^sub>F y in at x. y \<notin> S)"
+ unfolding discrete_def isolated_in_altdef by auto
+
(*
TODO.
Other than
@@ -194,4 +248,80 @@
ultimately show ?thesis by fastforce
qed
+definition sparse :: "real \<Rightarrow> 'a :: metric_space set \<Rightarrow> bool"
+ where "sparse \<epsilon> X \<longleftrightarrow> (\<forall>x\<in>X. \<forall>y\<in>X-{x}. dist x y > \<epsilon>)"
+
+lemma sparse_empty [simp, intro]: "sparse \<epsilon> {}"
+ by (auto simp: sparse_def)
+
+lemma sparseI [intro?]:
+ "(\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> x \<noteq> y \<Longrightarrow> dist x y > \<epsilon>) \<Longrightarrow> sparse \<epsilon> X"
+ unfolding sparse_def by auto
+
+lemma sparseD:
+ "sparse \<epsilon> X \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> x \<noteq> y \<Longrightarrow> dist x y > \<epsilon>"
+ unfolding sparse_def by auto
+
+lemma sparseD':
+ "sparse \<epsilon> X \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist x y \<le> \<epsilon> \<Longrightarrow> x = y"
+ unfolding sparse_def by force
+
+lemma sparse_singleton [simp, intro]: "sparse \<epsilon> {x}"
+ by (auto simp: sparse_def)
+
+definition setdist_gt where "setdist_gt \<epsilon> X Y \<longleftrightarrow> (\<forall>x\<in>X. \<forall>y\<in>Y. dist x y > \<epsilon>)"
+
+lemma setdist_gt_empty [simp]: "setdist_gt \<epsilon> {} Y" "setdist_gt \<epsilon> X {}"
+ by (auto simp: setdist_gt_def)
+
+lemma setdist_gtI: "(\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> dist x y > \<epsilon>) \<Longrightarrow> setdist_gt \<epsilon> X Y"
+ unfolding setdist_gt_def by auto
+
+lemma setdist_gtD: "setdist_gt \<epsilon> X Y \<Longrightarrow> x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> dist x y > \<epsilon>"
+ unfolding setdist_gt_def by auto
+
+lemma setdist_gt_setdist: "\<epsilon> < setdist A B \<Longrightarrow> setdist_gt \<epsilon> A B"
+ unfolding setdist_gt_def using setdist_le_dist by fastforce
+
+lemma setdist_gt_mono: "setdist_gt \<epsilon>' A B \<Longrightarrow> \<epsilon> \<le> \<epsilon>' \<Longrightarrow> A' \<subseteq> A \<Longrightarrow> B' \<subseteq> B \<Longrightarrow> setdist_gt \<epsilon> A' B'"
+ by (force simp: setdist_gt_def)
+
+lemma setdist_gt_Un_left: "setdist_gt \<epsilon> (A \<union> B) C \<longleftrightarrow> setdist_gt \<epsilon> A C \<and> setdist_gt \<epsilon> B C"
+ by (auto simp: setdist_gt_def)
+
+lemma setdist_gt_Un_right: "setdist_gt \<epsilon> C (A \<union> B) \<longleftrightarrow> setdist_gt \<epsilon> C A \<and> setdist_gt \<epsilon> C B"
+ by (auto simp: setdist_gt_def)
+
+lemma compact_closed_imp_eventually_setdist_gt_at_right_0:
+ assumes "compact A" "closed B" "A \<inter> B = {}"
+ shows "eventually (\<lambda>\<epsilon>. setdist_gt \<epsilon> A B) (at_right 0)"
+proof (cases "A = {} \<or> B = {}")
+ case False
+ hence "setdist A B > 0"
+ by (metis IntI assms empty_iff in_closed_iff_infdist_zero order_less_le setdist_attains_inf setdist_pos_le setdist_sym)
+ hence "eventually (\<lambda>\<epsilon>. \<epsilon> < setdist A B) (at_right 0)"
+ using eventually_at_right_field by blast
+ thus ?thesis
+ by eventually_elim (auto intro: setdist_gt_setdist)
+qed auto
+
+lemma setdist_gt_symI: "setdist_gt \<epsilon> A B \<Longrightarrow> setdist_gt \<epsilon> B A"
+ by (force simp: setdist_gt_def dist_commute)
+
+lemma setdist_gt_sym: "setdist_gt \<epsilon> A B \<longleftrightarrow> setdist_gt \<epsilon> B A"
+ by (force simp: setdist_gt_def dist_commute)
+
+lemma eventually_setdist_gt_at_right_0_mult_iff:
+ assumes "c > 0"
+ shows "eventually (\<lambda>\<epsilon>. setdist_gt (c * \<epsilon>) A B) (at_right 0) \<longleftrightarrow>
+ eventually (\<lambda>\<epsilon>. setdist_gt \<epsilon> A B) (at_right 0)"
+proof -
+ have "eventually (\<lambda>\<epsilon>. setdist_gt (c * \<epsilon>) A B) (at_right 0) \<longleftrightarrow>
+ eventually (\<lambda>\<epsilon>. setdist_gt \<epsilon> A B) (filtermap ((*) c) (at_right 0))"
+ by (simp add: eventually_filtermap)
+ also have "filtermap ((*) c) (at_right 0) = at_right 0"
+ by (subst filtermap_times_pos_at_right) (use assms in auto)
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/Analysis/Product_Vector.thy Thu Feb 09 08:35:50 2023 +0000
+++ b/src/HOL/Analysis/Product_Vector.thy Thu Feb 09 16:29:53 2023 +0000
@@ -131,7 +131,10 @@
instance..
end
-instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniform_space, uniform_space) uniform_space begin
+subsubsection \<open>Uniform spaces\<close>
+
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniform_space, uniform_space) uniform_space
+begin
instance
proof standard
fix U :: \<open>('a \<times> 'b) set\<close>
@@ -216,6 +219,133 @@
qed
end
+
+lemma (in uniform_space) nhds_eq_comap_uniformity: "nhds x = filtercomap (\<lambda>y. (x, y)) uniformity"
+proof -
+ have *: "eventually P (filtercomap (\<lambda>y. (x, y)) F) \<longleftrightarrow>
+ eventually (\<lambda>z. fst z = x \<longrightarrow> P (snd z)) F" for P :: "'a \<Rightarrow> bool" and F
+ unfolding eventually_filtercomap
+ by (smt (verit) eventually_elim2 fst_conv prod.collapse snd_conv)
+ thus ?thesis
+ unfolding filter_eq_iff
+ by (subst *) (auto simp: eventually_nhds_uniformity case_prod_unfold)
+qed
+
+lemma uniformity_of_uniform_continuous_invariant:
+ fixes f :: "'a :: uniform_space \<Rightarrow> 'a \<Rightarrow> 'a"
+ assumes "filterlim (\<lambda>((a,b),(c,d)). (f a c, f b d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+ assumes "eventually P uniformity"
+ obtains Q where "eventually Q uniformity" "\<And>a b c. Q (a, b) \<Longrightarrow> P (f a c, f b c)"
+ using eventually_compose_filterlim[OF assms(2,1)] uniformity_refl
+ by (fastforce simp: case_prod_unfold eventually_filtercomap eventually_prod_same)
+
+class uniform_topological_monoid_add = topological_monoid_add + uniform_space +
+ assumes uniformly_continuous_add':
+ "filterlim (\<lambda>((a,b), (c,d)). (a + c, b + d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+
+lemma uniformly_continuous_add:
+ "uniformly_continuous_on UNIV (\<lambda>(x :: 'a :: uniform_topological_monoid_add,y). x + y)"
+ using uniformly_continuous_add'[where ?'a = 'a]
+ by (simp add: uniformly_continuous_on_uniformity case_prod_unfold uniformity_prod_def filterlim_filtermap)
+
+lemma filterlim_fst: "filterlim fst F (F \<times>\<^sub>F G)"
+ by (simp add: filterlim_def filtermap_fst_prod_filter)
+
+lemma filterlim_snd: "filterlim snd G (F \<times>\<^sub>F G)"
+ by (simp add: filterlim_def filtermap_snd_prod_filter)
+
+class uniform_topological_group_add = topological_group_add + uniform_topological_monoid_add +
+ assumes uniformly_continuous_uminus': "filterlim (\<lambda>(a, b). (-a, -b)) uniformity uniformity"
+begin
+
+lemma uniformly_continuous_minus':
+ "filterlim (\<lambda>((a,b), (c,d)). (a - c, b - d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+proof -
+ have "filterlim ((\<lambda>((a,b), (c,d)). (a + c, b + d)) \<circ> (\<lambda>((a,b), (c,d)). ((a, b), (-c, -d))))
+ uniformity (uniformity \<times>\<^sub>F uniformity)"
+ unfolding o_def using uniformly_continuous_uminus'
+ by (intro filterlim_compose[OF uniformly_continuous_add'])
+ (auto simp: case_prod_unfold intro!: filterlim_Pair
+ filterlim_fst filterlim_compose[OF _ filterlim_snd])
+ thus ?thesis
+ by (simp add: o_def case_prod_unfold)
+qed
+
+end
+
+lemma uniformly_continuous_uminus:
+ "uniformly_continuous_on UNIV (\<lambda>x :: 'a :: uniform_topological_group_add. -x)"
+ using uniformly_continuous_uminus'[where ?'a = 'a]
+ by (simp add: uniformly_continuous_on_uniformity)
+
+lemma uniformly_continuous_minus:
+ "uniformly_continuous_on UNIV (\<lambda>(x :: 'a :: uniform_topological_group_add,y). x - y)"
+ using uniformly_continuous_minus'[where ?'a = 'a]
+ by (simp add: uniformly_continuous_on_uniformity case_prod_unfold uniformity_prod_def filterlim_filtermap)
+
+
+
+lemma real_normed_vector_is_uniform_topological_group_add [Pure.intro]:
+ "OFCLASS('a :: real_normed_vector, uniform_topological_group_add_class)"
+proof
+ show "filterlim (\<lambda>((a::'a,b), (c,d)). (a + c, b + d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+ unfolding filterlim_def le_filter_def eventually_filtermap case_prod_unfold
+ proof safe
+ fix P :: "'a \<times> 'a \<Rightarrow> bool"
+ assume "eventually P uniformity"
+ then obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "\<And>x y. dist x y < \<epsilon> \<Longrightarrow> P (x, y)"
+ by (auto simp: eventually_uniformity_metric)
+ define Q where "Q = (\<lambda>(x::'a,y). dist x y < \<epsilon> / 2)"
+ have Q: "eventually Q uniformity"
+ unfolding eventually_uniformity_metric Q_def using \<open>\<epsilon> > 0\<close>
+ by (meson case_prodI divide_pos_pos zero_less_numeral)
+ have "P (a + c, b + d)" if "Q (a, b)" "Q (c, d)" for a b c d
+ proof -
+ have "dist (a + c) (b + d) \<le> dist a b + dist c d"
+ by (simp add: dist_norm norm_diff_triangle_ineq)
+ also have "\<dots> < \<epsilon>"
+ using that by (auto simp: Q_def)
+ finally show ?thesis
+ by (intro \<epsilon>)
+ qed
+ thus "\<forall>\<^sub>F x in uniformity \<times>\<^sub>F uniformity. P (fst (fst x) + fst (snd x), snd (fst x) + snd (snd x))"
+ unfolding eventually_prod_filter by (intro exI[of _ Q] conjI Q) auto
+ qed
+next
+ show "filterlim (\<lambda>((a::'a), b). (-a, -b)) uniformity uniformity"
+ unfolding filterlim_def le_filter_def eventually_filtermap
+ proof safe
+ fix P :: "'a \<times> 'a \<Rightarrow> bool"
+ assume "eventually P uniformity"
+ then obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "\<And>x y. dist x y < \<epsilon> \<Longrightarrow> P (x, y)"
+ by (auto simp: eventually_uniformity_metric)
+ show "\<forall>\<^sub>F x in uniformity. P (case x of (a, b) \<Rightarrow> (- a, - b))"
+ unfolding eventually_uniformity_metric
+ by (intro exI[of _ \<epsilon>]) (auto intro!: \<epsilon> simp: dist_norm norm_minus_commute)
+ qed
+qed
+
+instance real :: uniform_topological_group_add ..
+instance complex :: uniform_topological_group_add ..
+
+lemma cauchy_seq_finset_iff_vanishing:
+ "uniformity = filtercomap (\<lambda>(x,y). y - x :: 'a :: uniform_topological_group_add) (nhds 0)"
+proof -
+ have "filtercomap (\<lambda>x. (0, case x of (x, y) \<Rightarrow> y - (x :: 'a))) uniformity \<le> uniformity"
+ apply (simp add: le_filter_def eventually_filtercomap)
+ using uniformity_of_uniform_continuous_invariant[OF uniformly_continuous_add']
+ by (metis diff_self eq_diff_eq)
+ moreover
+ have "uniformity \<le> filtercomap (\<lambda>x. (0, case x of (x, y) \<Rightarrow> y - (x :: 'a))) uniformity"
+ apply (simp add: le_filter_def eventually_filtercomap)
+ using uniformity_of_uniform_continuous_invariant[OF uniformly_continuous_minus']
+ by (metis (mono_tags) diff_self eventually_mono surjective_pairing)
+ ultimately show ?thesis
+ by (simp add: nhds_eq_comap_uniformity filtercomap_filtercomap)
+qed
+
+subsubsection \<open>Metric spaces\<close>
+
instantiation\<^marker>\<open>tag unimportant\<close> prod :: (metric_space, metric_space) uniformity_dist begin
instance
proof
@@ -422,7 +552,7 @@
using uniformly_continuous_on_prod_metric[of UNIV UNIV]
by auto
-text \<open>This logically belong with the real vector spaces by we only have the necessary lemmas now.\<close>
+text \<open>This logically belong with the real vector spaces but we only have the necessary lemmas now.\<close>
lemma isUCont_plus[simp]:
shows \<open>isUCont (\<lambda>(x::'a::real_normed_vector,y). x+y)\<close>
proof (rule isUCont_prod_metric[THEN iffD2], intro allI impI, simp)
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Thu Feb 09 08:35:50 2023 +0000
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy Thu Feb 09 16:29:53 2023 +0000
@@ -2567,6 +2567,11 @@
definition\<^marker>\<open>tag important\<close> fps_expansion :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> complex fps" where
"fps_expansion f z0 = Abs_fps (\<lambda>n. (deriv ^^ n) f z0 / fact n)"
+lemma fps_expansion_cong:
+ assumes "\<forall>\<^sub>F w in nhds x. f w =g w"
+ shows "fps_expansion f x = fps_expansion g x"
+ unfolding fps_expansion_def using assms higher_deriv_cong_ev by fastforce
+
lemma
fixes r :: ereal
assumes "f holomorphic_on eball z0 r"
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Thu Feb 09 08:35:50 2023 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Thu Feb 09 16:29:53 2023 +0000
@@ -39,6 +39,11 @@
shows "NO_MATCH 0 z \<Longrightarrow> is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f (z + x)) 0"
by (metis is_pole_shift_0)
+lemma is_pole_compose_iff:
+ assumes "filtermap g (at x) = (at y)"
+ shows "is_pole (f \<circ> g) x \<longleftrightarrow> is_pole f y"
+ unfolding is_pole_def filterlim_def filtermap_compose assms ..
+
lemma is_pole_inverse_holomorphic:
assumes "open s"
and f_holo:"f holomorphic_on (s-{z})"
@@ -130,7 +135,106 @@
shows "is_pole (\<lambda>w. f w / w ^ n) 0"
using is_pole_basic[of f A 0] assms by simp
-text \<open>The proposition
+lemma is_pole_compose:
+ assumes "is_pole f w" "g \<midarrow>z\<rightarrow> w" "eventually (\<lambda>z. g z \<noteq> w) (at z)"
+ shows "is_pole (\<lambda>x. f (g x)) z"
+ using assms(1) unfolding is_pole_def
+ by (rule filterlim_compose) (use assms in \<open>auto simp: filterlim_at\<close>)
+
+lemma is_pole_plus_const_iff:
+ "is_pole f z \<longleftrightarrow> is_pole (\<lambda>x. f x + c) z"
+proof
+ assume "is_pole f z"
+ then have "filterlim f at_infinity (at z)" unfolding is_pole_def .
+ moreover have "((\<lambda>_. c) \<longlongrightarrow> c) (at z)" by auto
+ ultimately have " LIM x (at z). f x + c :> at_infinity"
+ using tendsto_add_filterlim_at_infinity'[of f "at z"] by auto
+ then show "is_pole (\<lambda>x. f x + c) z" unfolding is_pole_def .
+next
+ assume "is_pole (\<lambda>x. f x + c) z"
+ then have "filterlim (\<lambda>x. f x + c) at_infinity (at z)"
+ unfolding is_pole_def .
+ moreover have "((\<lambda>_. -c) \<longlongrightarrow> -c) (at z)" by auto
+ ultimately have " LIM x (at z). f x :> at_infinity"
+ using tendsto_add_filterlim_at_infinity'[of "(\<lambda>x. f x + c)"
+ "at z" "(\<lambda>_. - c)" "-c"]
+ by auto
+ then show "is_pole f z" unfolding is_pole_def .
+qed
+
+lemma is_pole_minus_const_iff:
+ "is_pole (\<lambda>x. f x - c) z \<longleftrightarrow> is_pole f z"
+ using is_pole_plus_const_iff [of f z "-c"] by simp
+
+lemma is_pole_alt:
+ "is_pole f x = (\<forall>B>0. \<exists>U. open U \<and> x\<in>U \<and> (\<forall>y\<in>U. y\<noteq>x \<longrightarrow> norm (f y)\<ge>B))"
+ unfolding is_pole_def
+ unfolding filterlim_at_infinity[of 0,simplified] eventually_at_topological
+ by auto
+
+lemma is_pole_mult_analytic_nonzero1:
+ assumes "is_pole g x" "f analytic_on {x}" "f x \<noteq> 0"
+ shows "is_pole (\<lambda>x. f x * g x) x"
+ unfolding is_pole_def
+proof (rule tendsto_mult_filterlim_at_infinity)
+ show "f \<midarrow>x\<rightarrow> f x"
+ using assms by (simp add: analytic_at_imp_isCont isContD)
+qed (use assms in \<open>auto simp: is_pole_def\<close>)
+
+lemma is_pole_mult_analytic_nonzero2:
+ assumes "is_pole f x" "g analytic_on {x}" "g x \<noteq> 0"
+ shows "is_pole (\<lambda>x. f x * g x) x"
+ by (subst mult.commute, rule is_pole_mult_analytic_nonzero1) (use assms in auto)
+
+lemma is_pole_mult_analytic_nonzero1_iff:
+ assumes "f analytic_on {x}" "f x \<noteq> 0"
+ shows "is_pole (\<lambda>x. f x * g x) x \<longleftrightarrow> is_pole g x"
+proof
+ assume "is_pole g x"
+ thus "is_pole (\<lambda>x. f x * g x) x"
+ by (intro is_pole_mult_analytic_nonzero1 assms)
+next
+ assume "is_pole (\<lambda>x. f x * g x) x"
+ hence "is_pole (\<lambda>x. inverse (f x) * (f x * g x)) x"
+ by (rule is_pole_mult_analytic_nonzero1)
+ (use assms in \<open>auto intro!: analytic_intros\<close>)
+ also have "?this \<longleftrightarrow> is_pole g x"
+ proof (rule is_pole_cong)
+ have "eventually (\<lambda>x. f x \<noteq> 0) (at x)"
+ using assms by (simp add: analytic_at_neq_imp_eventually_neq)
+ thus "eventually (\<lambda>x. inverse (f x) * (f x * g x) = g x) (at x)"
+ by eventually_elim auto
+ qed auto
+ finally show "is_pole g x" .
+qed
+
+lemma is_pole_mult_analytic_nonzero2_iff:
+ assumes "g analytic_on {x}" "g x \<noteq> 0"
+ shows "is_pole (\<lambda>x. f x * g x) x \<longleftrightarrow> is_pole f x"
+ by (subst mult.commute, rule is_pole_mult_analytic_nonzero1_iff) (fact assms)+
+
+lemma frequently_const_imp_not_is_pole:
+ fixes z :: "'a::first_countable_topology"
+ assumes "frequently (\<lambda>w. f w = c) (at z)"
+ shows "\<not> is_pole f z"
+proof
+ assume "is_pole f z"
+ from assms have "z islimpt {w. f w = c}"
+ by (simp add: islimpt_conv_frequently_at)
+ then obtain g where g: "\<And>n. g n \<in> {w. f w = c} - {z}" "g \<longlonglongrightarrow> z"
+ unfolding islimpt_sequential by blast
+ then have "(f \<circ> g) \<longlonglongrightarrow> c"
+ by (simp add: tendsto_eventually)
+ moreover have *: "filterlim g (at z) sequentially"
+ using g by (auto simp: filterlim_at)
+ have "filterlim (f \<circ> g) at_infinity sequentially"
+ unfolding o_def by (rule filterlim_compose [OF _ *])
+ (use \<open>is_pole f z\<close> in \<open>simp add: is_pole_def\<close>)
+ ultimately show False
+ using not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially by blast
+qed
+
+ text \<open>The proposition
\<^term>\<open>\<exists>x. ((f::complex\<Rightarrow>complex) \<longlongrightarrow> x) (at z) \<or> is_pole f z\<close>
can be interpreted as the complex function \<^term>\<open>f\<close> has a non-essential singularity at \<^term>\<open>z\<close>
(i.e. the singularity is either removable or a pole).\<close>
@@ -140,6 +244,39 @@
definition isolated_singularity_at::"[complex \<Rightarrow> complex, complex] \<Rightarrow> bool" where
"isolated_singularity_at f z = (\<exists>r>0. f analytic_on ball z r-{z})"
+lemma not_essential_cong:
+ assumes "eventually (\<lambda>x. f x = g x) (at z)" "z = z'"
+ shows "not_essential f z \<longleftrightarrow> not_essential g z'"
+ unfolding not_essential_def using assms filterlim_cong is_pole_cong by fastforce
+
+lemma isolated_singularity_at_cong:
+ assumes "eventually (\<lambda>x. f x = g x) (at z)" "z = z'"
+ shows "isolated_singularity_at f z \<longleftrightarrow> isolated_singularity_at g z'"
+proof -
+ have "isolated_singularity_at g z"
+ if "isolated_singularity_at f z" "eventually (\<lambda>x. f x = g x) (at z)" for f g
+ proof -
+ from that(1) obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
+ by (auto simp: isolated_singularity_at_def)
+ from that(2) obtain r' where r': "r' > 0" "\<forall>x\<in>ball z r'-{z}. f x = g x"
+ unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_commute)
+
+ have "f holomorphic_on ball z r - {z}"
+ using r(2) by (subst (asm) analytic_on_open) auto
+ hence "f holomorphic_on ball z (min r r') - {z}"
+ by (rule holomorphic_on_subset) auto
+ also have "?this \<longleftrightarrow> g holomorphic_on ball z (min r r') - {z}"
+ using r' by (intro holomorphic_cong) auto
+ also have "\<dots> \<longleftrightarrow> g analytic_on ball z (min r r') - {z}"
+ by (subst analytic_on_open) auto
+ finally show ?thesis
+ unfolding isolated_singularity_at_def
+ by (intro exI[of _ "min r r'"]) (use \<open>r > 0\<close> \<open>r' > 0\<close> in auto)
+ qed
+ from this[of f g] this[of g f] assms show ?thesis
+ by (auto simp: eq_commute)
+qed
+
lemma removable_singularity:
assumes "f holomorphic_on A - {x}" "open A"
assumes "f \<midarrow>x\<rightarrow> c"
@@ -795,6 +932,24 @@
using assms unfolding isolated_singularity_at_def
by (metis analytic_on_holomorphic centre_in_ball insert_Diff openE open_delete subset_insert_iff)
+lemma isolated_singularity_at_altdef:
+ "isolated_singularity_at f z \<longleftrightarrow> eventually (\<lambda>z. f analytic_on {z}) (at z)"
+proof
+ assume "isolated_singularity_at f z"
+ then obtain r where r: "r > 0" "f analytic_on ball z r - {z}"
+ unfolding isolated_singularity_at_def by blast
+ have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
+ using r(1) by (intro eventually_at_in_open) auto
+ thus "eventually (\<lambda>z. f analytic_on {z}) (at z)"
+ by eventually_elim (use r analytic_on_subset in auto)
+next
+ assume "eventually (\<lambda>z. f analytic_on {z}) (at z)"
+ then obtain A where A: "open A" "z \<in> A" "\<And>w. w \<in> A - {z} \<Longrightarrow> f analytic_on {w}"
+ unfolding eventually_at_topological by blast
+ then show "isolated_singularity_at f z"
+ by (meson analytic_imp_holomorphic analytic_on_analytic_at isolated_singularity_at_holomorphic)
+qed
+
lemma isolated_singularity_at_shift:
assumes "isolated_singularity_at (\<lambda>x. f (x + w)) z"
shows "isolated_singularity_at f (z + w)"
@@ -863,6 +1018,20 @@
by (auto simp: not_essential_def)
qed
+lemma not_essential_analytic:
+ assumes "f analytic_on {z}"
+ shows "not_essential f z"
+ using analytic_at assms not_essential_holomorphic by blast
+
+lemma not_essential_id [singularity_intros]: "not_essential (\<lambda>w. w) z"
+ by (simp add: not_essential_analytic)
+
+lemma is_pole_imp_not_essential [intro]: "is_pole f z \<Longrightarrow> not_essential f z"
+ by (auto simp: not_essential_def)
+
+lemma tendsto_imp_not_essential [intro]: "f \<midarrow>z\<rightarrow> c \<Longrightarrow> not_essential f z"
+ by (auto simp: not_essential_def)
+
lemma eventually_not_pole:
assumes "isolated_singularity_at f z"
shows "eventually (\<lambda>w. \<not>is_pole f w) (at z)"
@@ -901,7 +1070,18 @@
thus ?thesis by simp
qed
-subsubsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
+lemma isolated_singularity_at_analytic:
+ assumes "f analytic_on {z}"
+ shows "isolated_singularity_at f z"
+proof -
+ from assms obtain r where r: "r > 0" "f holomorphic_on ball z r"
+ by (auto simp: analytic_on_def)
+ show ?thesis
+ by (rule isolated_singularity_at_holomorphic[of f "ball z r"])
+ (use \<open>r > 0\<close> in \<open>auto intro!: holomorphic_on_subset[OF r(2)]\<close>)
+qed
+
+subsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
definition\<^marker>\<open>tag important\<close> zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
"zorder f z = (THE n. (\<exists>h r. r>0 \<and> h holomorphic_on cball z r \<and> h z\<noteq>0
@@ -1658,6 +1838,33 @@
using \<open>z=z'\<close> unfolding P_def zorder_def zor_poly_def by auto
qed
+lemma zorder_times_analytic':
+ assumes "isolated_singularity_at f z" "not_essential f z"
+ assumes "g analytic_on {z}" "frequently (\<lambda>z. f z * g z \<noteq> 0) (at z)"
+ shows "zorder (\<lambda>x. f x * g x) z = zorder f z + zorder g z"
+proof (rule zorder_times)
+ show "isolated_singularity_at g z" "not_essential g z"
+ by (intro isolated_singularity_at_analytic not_essential_analytic assms)+
+qed (use assms in auto)
+
+lemma zorder_cmult:
+ assumes "c \<noteq> 0"
+ shows "zorder (\<lambda>z. c * f z) z = zorder f z"
+proof -
+ define P where
+ "P = (\<lambda>f n h r. 0 < r \<and> h holomorphic_on cball z r \<and>
+ h z \<noteq> 0 \<and> (\<forall>w\<in>cball z r - {z}. f w = h w * (w - z) powr of_int n \<and> h w \<noteq> 0))"
+ have *: "P (\<lambda>x. c * f x) n (\<lambda>x. c * h x) r" if "P f n h r" "c \<noteq> 0" for f n h r c
+ using that unfolding P_def by (auto intro!: holomorphic_intros)
+ have "(\<exists>h r. P (\<lambda>x. c * f x) n h r) \<longleftrightarrow> (\<exists>h r. P f n h r)" for n
+ using *[of f n _ _ c] *[of "\<lambda>x. c * f x" n _ _ "inverse c"] \<open>c \<noteq> 0\<close>
+ by (fastforce simp: field_simps)
+ hence "(THE n. \<exists>h r. P (\<lambda>x. c * f x) n h r) = (THE n. \<exists>h r. P f n h r)"
+ by simp
+ thus ?thesis
+ by (simp add: zorder_def P_def)
+qed
+
lemma zorder_nonzero_div_power:
assumes sz: "open s" "z \<in> s" "f holomorphic_on s" "f z \<noteq> 0" and "n > 0"
shows "zorder (\<lambda>w. f w / (w - z) ^ n) z = - n"
@@ -2269,4 +2476,263 @@
qed
qed
+
+lemma deriv_divide_is_pole: \<comment>\<open>Generalises @{thm zorder_deriv}\<close>
+ fixes f g::"complex \<Rightarrow> complex" and z::complex
+ assumes f_iso:"isolated_singularity_at f z"
+ and f_ness:"not_essential f z"
+ and fg_nconst: "\<exists>\<^sub>Fw in (at z). deriv f w * f w \<noteq> 0"
+ and f_ord:"zorder f z \<noteq>0"
+ shows "is_pole (\<lambda>z. deriv f z / f z) z"
+proof (rule neg_zorder_imp_is_pole)
+ define ff where "ff=(\<lambda>w. deriv f w / f w)"
+ show "isolated_singularity_at ff z"
+ using f_iso f_ness unfolding ff_def
+ by (auto intro:singularity_intros)
+ show "not_essential ff z"
+ unfolding ff_def using f_ness f_iso
+ by (auto intro:singularity_intros)
+
+ have "zorder ff z = zorder (deriv f) z - zorder f z"
+ unfolding ff_def using f_iso f_ness fg_nconst
+ apply (rule_tac zorder_divide)
+ by (auto intro:singularity_intros)
+ moreover have "zorder (deriv f) z = zorder f z - 1"
+ proof (rule zorder_deriv_minus_1)
+ show " \<exists>\<^sub>F w in at z. f w \<noteq> 0"
+ using fg_nconst frequently_elim1 by fastforce
+ qed (use f_iso f_ness f_ord in auto)
+ ultimately show "zorder ff z < 0" by auto
+
+ show "\<exists>\<^sub>F w in at z. ff w \<noteq> 0"
+ unfolding ff_def using fg_nconst by auto
+qed
+
+lemma is_pole_deriv_divide_is_pole:
+ fixes f g::"complex \<Rightarrow> complex" and z::complex
+ assumes f_iso:"isolated_singularity_at f z"
+ and "is_pole f z"
+ shows "is_pole (\<lambda>z. deriv f z / f z) z"
+proof (rule deriv_divide_is_pole[OF f_iso])
+ show "not_essential f z"
+ using \<open>is_pole f z\<close> unfolding not_essential_def by auto
+ show "\<exists>\<^sub>F w in at z. deriv f w * f w \<noteq> 0"
+ apply (rule isolated_pole_imp_nzero_times)
+ using assms by auto
+ show "zorder f z \<noteq> 0"
+ using isolated_pole_imp_neg_zorder assms by fastforce
+qed
+
+subsection \<open>Isolated zeroes\<close>
+
+definition isolated_zero :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> bool" where
+ "isolated_zero f z \<longleftrightarrow> f z = 0 \<and> eventually (\<lambda>z. f z \<noteq> 0) (at z)"
+
+lemma isolated_zero_altdef: "isolated_zero f z \<longleftrightarrow> f z = 0 \<and> \<not>z islimpt {z. f z = 0}"
+ unfolding isolated_zero_def eventually_at_filter eventually_nhds islimpt_def by blast
+
+lemma isolated_zero_mult1:
+ assumes "isolated_zero f x" "isolated_zero g x"
+ shows "isolated_zero (\<lambda>x. f x * g x) x"
+proof -
+ have "eventually (\<lambda>x. f x \<noteq> 0) (at x)" "eventually (\<lambda>x. g x \<noteq> 0) (at x)"
+ using assms unfolding isolated_zero_def by auto
+ hence "eventually (\<lambda>x. f x * g x \<noteq> 0) (at x)"
+ by eventually_elim auto
+ with assms show ?thesis
+ by (auto simp: isolated_zero_def)
+qed
+
+lemma isolated_zero_mult2:
+ assumes "isolated_zero f x" "g x \<noteq> 0" "g analytic_on {x}"
+ shows "isolated_zero (\<lambda>x. f x * g x) x"
+proof -
+ have "eventually (\<lambda>x. f x \<noteq> 0) (at x)"
+ using assms unfolding isolated_zero_def by auto
+ moreover have "eventually (\<lambda>x. g x \<noteq> 0) (at x)"
+ using analytic_at_neq_imp_eventually_neq[of g x 0] assms by auto
+ ultimately have "eventually (\<lambda>x. f x * g x \<noteq> 0) (at x)"
+ by eventually_elim auto
+ thus ?thesis
+ using assms(1) by (auto simp: isolated_zero_def)
+qed
+
+lemma isolated_zero_mult3:
+ assumes "isolated_zero f x" "g x \<noteq> 0" "g analytic_on {x}"
+ shows "isolated_zero (\<lambda>x. g x * f x) x"
+ using isolated_zero_mult2[OF assms] by (simp add: mult_ac)
+
+lemma isolated_zero_prod:
+ assumes "\<And>x. x \<in> I \<Longrightarrow> isolated_zero (f x) z" "I \<noteq> {}" "finite I"
+ shows "isolated_zero (\<lambda>y. \<Prod>x\<in>I. f x y) z"
+ using assms(3,2,1) by (induction rule: finite_ne_induct) (auto intro: isolated_zero_mult1)
+
+lemma non_isolated_zero':
+ assumes "isolated_singularity_at f z" "not_essential f z" "f z = 0" "\<not>isolated_zero f z"
+ shows "eventually (\<lambda>z. f z = 0) (at z)"
+proof (rule not_essential_frequently_0_imp_eventually_0)
+ from assms show "frequently (\<lambda>z. f z = 0) (at z)"
+ by (auto simp: frequently_def isolated_zero_def)
+qed fact+
+
+lemma non_isolated_zero:
+ assumes "\<not>isolated_zero f z" "f analytic_on {z}" "f z = 0"
+ shows "eventually (\<lambda>z. f z = 0) (nhds z)"
+proof -
+ have "eventually (\<lambda>z. f z = 0) (at z)"
+ by (rule non_isolated_zero')
+ (use assms in \<open>auto intro: not_essential_analytic isolated_singularity_at_analytic\<close>)
+ with \<open>f z = 0\<close> show ?thesis
+ unfolding eventually_at_filter by (auto elim!: eventually_mono)
+qed
+
+lemma not_essential_compose:
+ assumes "not_essential f (g z)" "g analytic_on {z}"
+ shows "not_essential (\<lambda>x. f (g x)) z"
+proof (cases "isolated_zero (\<lambda>w. g w - g z) z")
+ case False
+ hence "eventually (\<lambda>w. g w - g z = 0) (nhds z)"
+ by (rule non_isolated_zero) (use assms in \<open>auto intro!: analytic_intros\<close>)
+ hence "not_essential (\<lambda>x. f (g x)) z \<longleftrightarrow> not_essential (\<lambda>_. f (g z)) z"
+ by (intro not_essential_cong refl)
+ (auto elim!: eventually_mono simp: eventually_at_filter)
+ thus ?thesis
+ by (simp add: not_essential_const)
+next
+ case True
+ hence ev: "eventually (\<lambda>w. g w \<noteq> g z) (at z)"
+ by (auto simp: isolated_zero_def)
+ from assms consider c where "f \<midarrow>g z\<rightarrow> c" | "is_pole f (g z)"
+ by (auto simp: not_essential_def)
+ have "isCont g z"
+ by (rule analytic_at_imp_isCont) fact
+ hence lim: "g \<midarrow>z\<rightarrow> g z"
+ using isContD by blast
+
+ from assms(1) consider c where "f \<midarrow>g z\<rightarrow> c" | "is_pole f (g z)"
+ unfolding not_essential_def by blast
+ thus ?thesis
+ proof cases
+ fix c assume "f \<midarrow>g z\<rightarrow> c"
+ hence "(\<lambda>x. f (g x)) \<midarrow>z\<rightarrow> c"
+ by (rule filterlim_compose) (use lim ev in \<open>auto simp: filterlim_at\<close>)
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ next
+ assume "is_pole f (g z)"
+ hence "is_pole (\<lambda>x. f (g x)) z"
+ by (rule is_pole_compose) fact+
+ thus ?thesis
+ by (auto simp: not_essential_def)
+ qed
+qed
+
+subsection \<open>Isolated points\<close>
+
+definition isolated_points_of :: "complex set \<Rightarrow> complex set" where
+ "isolated_points_of A = {z\<in>A. eventually (\<lambda>w. w \<notin> A) (at z)}"
+
+lemma isolated_points_of_altdef: "isolated_points_of A = {z\<in>A. \<not>z islimpt A}"
+ unfolding isolated_points_of_def islimpt_def eventually_at_filter eventually_nhds by blast
+
+lemma isolated_points_of_empty [simp]: "isolated_points_of {} = {}"
+ and isolated_points_of_UNIV [simp]: "isolated_points_of UNIV = {}"
+ by (auto simp: isolated_points_of_def)
+
+lemma isolated_points_of_open_is_empty [simp]: "open A \<Longrightarrow> isolated_points_of A = {}"
+ unfolding isolated_points_of_altdef
+ by (simp add: interior_limit_point interior_open)
+
+lemma isolated_points_of_subset: "isolated_points_of A \<subseteq> A"
+ by (auto simp: isolated_points_of_def)
+
+lemma isolated_points_of_discrete:
+ assumes "discrete A"
+ shows "isolated_points_of A = A"
+ using assms by (auto simp: isolated_points_of_def discrete_altdef)
+
+lemmas uniform_discreteI1 = uniformI1
+lemmas uniform_discreteI2 = uniformI2
+
+lemma isolated_singularity_at_compose:
+ assumes "isolated_singularity_at f (g z)" "g analytic_on {z}"
+ shows "isolated_singularity_at (\<lambda>x. f (g x)) z"
+proof (cases "isolated_zero (\<lambda>w. g w - g z) z")
+ case False
+ hence "eventually (\<lambda>w. g w - g z = 0) (nhds z)"
+ by (rule non_isolated_zero) (use assms in \<open>auto intro!: analytic_intros\<close>)
+ hence "isolated_singularity_at (\<lambda>x. f (g x)) z \<longleftrightarrow> isolated_singularity_at (\<lambda>_. f (g z)) z"
+ by (intro isolated_singularity_at_cong refl)
+ (auto elim!: eventually_mono simp: eventually_at_filter)
+ thus ?thesis
+ by (simp add: isolated_singularity_at_const)
+next
+ case True
+ from assms(1) obtain r where r: "r > 0" "f analytic_on ball (g z) r - {g z}"
+ by (auto simp: isolated_singularity_at_def)
+ hence holo_f: "f holomorphic_on ball (g z) r - {g z}"
+ by (subst (asm) analytic_on_open) auto
+ from assms(2) obtain r' where r': "r' > 0" "g holomorphic_on ball z r'"
+ by (auto simp: analytic_on_def)
+
+ have "continuous_on (ball z r') g"
+ using holomorphic_on_imp_continuous_on r' by blast
+ hence "isCont g z"
+ using r' by (subst (asm) continuous_on_eq_continuous_at) auto
+ hence "g \<midarrow>z\<rightarrow> g z"
+ using isContD by blast
+ hence "eventually (\<lambda>w. g w \<in> ball (g z) r) (at z)"
+ using \<open>r > 0\<close> unfolding tendsto_def by force
+ moreover have "eventually (\<lambda>w. g w \<noteq> g z) (at z)" using True
+ by (auto simp: isolated_zero_def elim!: eventually_mono)
+ ultimately have "eventually (\<lambda>w. g w \<in> ball (g z) r - {g z}) (at z)"
+ by eventually_elim auto
+ then obtain r'' where r'': "r'' > 0" "\<forall>w\<in>ball z r''-{z}. g w \<in> ball (g z) r - {g z}"
+ unfolding eventually_at_filter eventually_nhds_metric ball_def
+ by (auto simp: dist_commute)
+ have "f \<circ> g holomorphic_on ball z (min r' r'') - {z}"
+ proof (rule holomorphic_on_compose_gen)
+ show "g holomorphic_on ball z (min r' r'') - {z}"
+ by (rule holomorphic_on_subset[OF r'(2)]) auto
+ show "f holomorphic_on ball (g z) r - {g z}"
+ by fact
+ show "g ` (ball z (min r' r'') - {z}) \<subseteq> ball (g z) r - {g z}"
+ using r'' by force
+ qed
+ hence "f \<circ> g analytic_on ball z (min r' r'') - {z}"
+ by (subst analytic_on_open) auto
+ thus ?thesis using \<open>r' > 0\<close> \<open>r'' > 0\<close>
+ by (auto simp: isolated_singularity_at_def o_def intro!: exI[of _ "min r' r''"])
+qed
+
+lemma is_pole_power_int_0:
+ assumes "f analytic_on {x}" "isolated_zero f x" "n < 0"
+ shows "is_pole (\<lambda>x. f x powi n) x"
+proof -
+ have "f \<midarrow>x\<rightarrow> f x"
+ using assms(1) by (simp add: analytic_at_imp_isCont isContD)
+ with assms show ?thesis
+ unfolding is_pole_def
+ by (intro filterlim_power_int_neg_at_infinity) (auto simp: isolated_zero_def)
+qed
+
+lemma isolated_zero_imp_not_constant_on:
+ assumes "isolated_zero f x" "x \<in> A" "open A"
+ shows "\<not>f constant_on A"
+proof
+ assume "f constant_on A"
+ then obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x = c"
+ by (auto simp: constant_on_def)
+ from assms and c[of x] have [simp]: "c = 0"
+ by (auto simp: isolated_zero_def)
+ have "eventually (\<lambda>x. f x \<noteq> 0) (at x)"
+ using assms by (auto simp: isolated_zero_def)
+ moreover have "eventually (\<lambda>x. x \<in> A) (at x)"
+ using assms by (intro eventually_at_in_open') auto
+ ultimately have "eventually (\<lambda>x. False) (at x)"
+ by eventually_elim (use c in auto)
+ thus False
+ by simp
+qed
+
end
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy Thu Feb 09 08:35:50 2023 +0000
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy Thu Feb 09 16:29:53 2023 +0000
@@ -1079,7 +1079,7 @@
qed
qed
-text\<open>Hence a nice clean inverse function theorem\<close>
+subsubsection \<open>Hence a nice clean inverse function theorem\<close>
lemma has_field_derivative_inverse_strong:
fixes f :: "'a::{euclidean_space,real_normed_field} \<Rightarrow> 'a"
@@ -1140,6 +1140,78 @@
qed
qed
+subsubsection \<open> Holomorphism of covering maps and lifts.\<close>
+
+lemma covering_space_lift_is_holomorphic:
+ assumes cov: "covering_space C p S"
+ and C: "open C" "p holomorphic_on C"
+ and holf: "f holomorphic_on U" and fim: "f ` U \<subseteq> S" and gim: "g ` U \<subseteq> C"
+ and contg: "continuous_on U g" and pg_f: "\<And>x. x \<in> U \<Longrightarrow> p(g x) = f x"
+ shows "g holomorphic_on U"
+ unfolding holomorphic_on_def
+proof (intro strip)
+ fix z
+ assume "z \<in> U"
+ with fim have "f z \<in> S" by blast
+ then obtain T \<V> where "f z \<in> T" and opeT: "openin (top_of_set S) T"
+ and UV: "\<Union>\<V> = C \<inter> p -` T"
+ and "\<And>W. W \<in> \<V> \<Longrightarrow> openin (top_of_set C) W"
+ and disV: "pairwise disjnt \<V>" and homeV: "\<And>W. W \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism W T p q"
+ using cov fim unfolding covering_space_def by meson
+ then have "\<And>W. W \<in> \<V> \<Longrightarrow> open W \<and> W \<subseteq> C"
+ by (metis \<open>open C\<close> inf_le1 open_Int openin_open)
+ then obtain V where "V \<in> \<V>" "g z \<in> V" "open V" "V \<subseteq> C"
+ by (metis IntI UnionE image_subset_iff vimageI UV \<open>f z \<in> T\<close> \<open>z \<in> U\<close> gim pg_f)
+ have holp: "p holomorphic_on V"
+ using \<open>V \<subseteq> C\<close> \<open>p holomorphic_on C\<close> holomorphic_on_subset by blast
+ moreover have injp: "inj_on p V"
+ by (metis \<open>V \<in> \<V>\<close> homeV homeomorphism_def inj_on_inverseI)
+ ultimately
+ obtain p' where holp': "p' holomorphic_on (p ` V)" and pp': "\<And>z. z \<in> V \<Longrightarrow> p'(p z) = z"
+ using \<open>open V\<close> holomorphic_has_inverse by metis
+ have "z \<in> U \<inter> g -` V"
+ using \<open>g z \<in> V\<close> \<open>z \<in> U\<close> by blast
+ moreover have "openin (top_of_set U) (U \<inter> g -` V)"
+ using continuous_openin_preimage [OF contg gim]
+ by (meson \<open>open V\<close> contg continuous_openin_preimage_eq)
+ ultimately obtain \<epsilon> where "\<epsilon>>0" and e: "ball z \<epsilon> \<inter> U \<subseteq> g -` V"
+ by (force simp add: openin_contains_ball)
+ show "g field_differentiable at z within U"
+ proof (rule field_differentiable_transform_within)
+ show "(0::real) < \<epsilon>"
+ by (simp add: \<open>0 < \<epsilon>\<close>)
+ show "z \<in> U"
+ by (simp add: \<open>z \<in> U\<close>)
+ show "(p' o f) x' = g x'" if "x' \<in> U" "dist x' z < \<epsilon>" for x'
+ using that
+ by (metis Int_iff comp_apply dist_commute e mem_ball pg_f pp' subsetD vimage_eq)
+ have "open (p ` V)"
+ using \<open>open V\<close> holp injp open_mapping_thm3 by force
+ moreover have "f z \<in> p ` V"
+ by (metis \<open>z \<in> U\<close> image_iff pg_f \<open>g z \<in> V\<close>)
+ ultimately have "p' field_differentiable at (f z)"
+ using holomorphic_on_imp_differentiable_at holp' by blast
+ moreover have "f field_differentiable at z within U"
+ by (metis (no_types) \<open>z \<in> U\<close> holf holomorphic_on_def)
+ ultimately show "(p' o f) field_differentiable at z within U"
+ by (metis (no_types) field_differentiable_at_within field_differentiable_compose_within)
+ qed
+qed
+
+lemma covering_space_lift_holomorphic:
+ assumes cov: "covering_space C p S"
+ and C: "open C" "p holomorphic_on C"
+ and f: "f holomorphic_on U" "f ` U \<subseteq> S"
+ and U: "simply_connected U" "locally path_connected U"
+ obtains g where "g holomorphic_on U" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+proof -
+ obtain g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
+ using covering_space_lift [OF cov U]
+ using f holomorphic_on_imp_continuous_on by blast
+ then show ?thesis
+ by (metis C cov covering_space_lift_is_holomorphic f that)
+qed
+
subsection\<open>The Schwarz Lemma\<close>
lemma Schwarz1:
@@ -1923,8 +1995,7 @@
qed
show ?thesis
apply (rule Bloch_unit [OF 1 2])
- apply (rule_tac b="(C * of_real r) * b" in that)
- using image_mono sb1 sb2 by fastforce
+ using image_mono sb1 sb2 that by fastforce
qed
corollary Bloch_general:
@@ -1954,10 +2025,7 @@
then have 1: "f holomorphic_on ball a t"
using holf using holomorphic_on_subset by blast
show ?thesis
- apply (rule Bloch [OF 1 \<open>t > 0\<close> rle])
- apply (rule_tac b=b in that)
- using * apply force
- done
+ using Bloch [OF 1 \<open>t > 0\<close> rle] * by (metis image_mono order_trans that)
qed
qed
qed