78 by (intro interior_limit_point) (auto simp: interior_open) |
78 by (intro interior_limit_point) (auto simp: interior_open) |
79 have "f z - g z = 0" |
79 have "f z - g z = 0" |
80 by (rule analytic_continuation[of "\<lambda>z. f z - g z" s' s \<xi>]) |
80 by (rule analytic_continuation[of "\<lambda>z. f z - g z" s' s \<xi>]) |
81 (insert assms \<open>\<xi> \<in> s\<close> \<xi>, auto intro: holomorphic_intros) |
81 (insert assms \<open>\<xi> \<in> s\<close> \<xi>, auto intro: holomorphic_intros) |
82 thus ?thesis by simp |
82 thus ?thesis by simp |
|
83 qed |
|
84 |
|
85 corollary analytic_continuation': |
|
86 assumes "f holomorphic_on S" "open S" "connected S" |
|
87 and "U \<subseteq> S" "\<xi> \<in> S" "\<xi> islimpt U" |
|
88 and "f constant_on U" |
|
89 shows "f constant_on S" |
|
90 proof - |
|
91 obtain c where c: "\<And>x. x \<in> U \<Longrightarrow> f x - c = 0" |
|
92 by (metis \<open>f constant_on U\<close> constant_on_def diff_self) |
|
93 have "(\<lambda>z. f z - c) holomorphic_on S" |
|
94 using assms by (intro holomorphic_intros) |
|
95 with c analytic_continuation assms have "\<And>x. x \<in> S \<Longrightarrow> f x - c = 0" |
|
96 by blast |
|
97 then show ?thesis |
|
98 unfolding constant_on_def by force |
|
99 qed |
|
100 |
|
101 lemma holomorphic_compact_finite_zeros: |
|
102 assumes S: "f holomorphic_on S" "open S" "connected S" |
|
103 and "compact K" "K \<subseteq> S" |
|
104 and "\<not> f constant_on S" |
|
105 shows "finite {z\<in>K. f z = 0}" |
|
106 proof (rule ccontr) |
|
107 assume "infinite {z\<in>K. f z = 0}" |
|
108 then obtain z where "z \<in> K" and z: "z islimpt {z\<in>K. f z = 0}" |
|
109 using \<open>compact K\<close> by (auto simp: compact_eq_Bolzano_Weierstrass) |
|
110 moreover have "{z\<in>K. f z = 0} \<subseteq> S" |
|
111 using \<open>K \<subseteq> S\<close> by blast |
|
112 ultimately show False |
|
113 using assms analytic_continuation [OF S] unfolding constant_on_def |
|
114 by blast |
83 qed |
115 qed |
84 |
116 |
85 subsection\<open>Open mapping theorem\<close> |
117 subsection\<open>Open mapping theorem\<close> |
86 |
118 |
87 lemma holomorphic_contract_to_zero: |
119 lemma holomorphic_contract_to_zero: |