# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1646147127 0
# Node ID ff60b4acd6ddf22d187162fa0cc79e72e49b7f72
# Parent  0a300751fdf564ef0a2ac9153127ad0253d2f048
Added some theorems (from Wetzel)

diff -r 0a300751fdf5 -r ff60b4acd6dd src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Feb 28 13:10:22 2022 +0100
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Mar 01 15:05:27 2022 +0000
@@ -532,6 +532,10 @@
   "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on S) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) analytic_on S"
   by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_add)
 
+lemma analytic_on_prod [analytic_intros]:
+  "(\<And>i. i \<in> I \<Longrightarrow> (f i) analytic_on S) \<Longrightarrow> (\<lambda>x. prod (\<lambda>i. f i x) I) analytic_on S"
+  by (induct I rule: infinite_finite_induct) (auto simp: analytic_on_mult)
+
 lemma deriv_left_inverse:
   assumes "f holomorphic_on S" and "g holomorphic_on T"
       and "open S" and "open T"
diff -r 0a300751fdf5 -r ff60b4acd6dd src/HOL/Complex_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Mon Feb 28 13:10:22 2022 +0100
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Tue Mar 01 15:05:27 2022 +0000
@@ -114,6 +114,45 @@
     by blast
 qed
 
+lemma holomorphic_countable_zeros:
+  assumes S: "f holomorphic_on S" "open S" "connected S" and "fsigma S"
+      and "\<not> f constant_on S"
+    shows "countable {z\<in>S. f z = 0}"
+proof -
+  obtain F::"nat \<Rightarrow> complex set" 
+      where F: "range F \<subseteq> Collect compact" and Seq: "S = (\<Union>i. F i)"
+    using \<open>fsigma S\<close> by (meson fsigma_Union_compact)
+  have fin: "finite {z \<in> F i. f z = 0}" for i
+    using holomorphic_compact_finite_zeros assms F Seq Union_iff by blast
+  have "{z \<in> S. f z = 0} = (\<Union>i. {z \<in> F i. f z = 0})"
+    using Seq by auto
+  with fin show ?thesis
+    by (simp add: countable_finite)
+qed
+
+lemma holomorphic_countable_equal:
+  assumes "f holomorphic_on S" "g holomorphic_on S" "open S" "connected S" and "fsigma S"
+    and eq: "uncountable {z\<in>S. f z = g z}"
+  shows "S \<subseteq> {z\<in>S. f z = g z}"
+proof -
+  obtain z where z: "z\<in>S" "f z = g z"
+    using eq not_finite_existsD uncountable_infinite by blast
+  have "(\<lambda>x. f x - g x) holomorphic_on S"
+    by (simp add: assms holomorphic_on_diff)
+  then have "(\<lambda>x. f x - g x) constant_on S"
+    using holomorphic_countable_zeros assms by force
+  with z have "\<And>x. x\<in>S \<Longrightarrow> f x - g x = 0"
+    unfolding constant_on_def by force
+  then show ?thesis
+    by auto
+qed
+
+lemma holomorphic_countable_equal_UNIV:
+  assumes fg: "f holomorphic_on UNIV" "g holomorphic_on UNIV"
+    and eq: "uncountable {z. f z = g z}"
+  shows "f=g"
+  using holomorphic_countable_equal [OF fg] eq by fastforce
+
 subsection\<open>Open mapping theorem\<close>
 
 lemma holomorphic_contract_to_zero: