# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1675956966 0
# Node ID 8c093a4b8ccf9a9628cfd771504963c1944e1c7c
# Parent  6c8c980e777a695e242892dece5787e478b360cd
Even more new material from Eberl and Li

diff -r 6c8c980e777a -r 8c093a4b8ccf src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Thu Feb 09 13:36:53 2023 +0000
+++ b/src/HOL/Analysis/Product_Vector.thy	Thu Feb 09 15:36:06 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)
diff -r 6c8c980e777a -r 8c093a4b8ccf src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Thu Feb 09 13:36:53 2023 +0000
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Thu Feb 09 15:36:06 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"
diff -r 6c8c980e777a -r 8c093a4b8ccf src/HOL/Complex_Analysis/Complex_Singularities.thy
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy	Thu Feb 09 13:36:53 2023 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy	Thu Feb 09 15:36:06 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})"
@@ -208,7 +213,28 @@
   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)+
 
-text \<open>The proposition
+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>
diff -r 6c8c980e777a -r 8c093a4b8ccf src/HOL/Complex_Analysis/Conformal_Mappings.thy
--- a/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Thu Feb 09 13:36:53 2023 +0000
+++ b/src/HOL/Complex_Analysis/Conformal_Mappings.thy	Thu Feb 09 15:36:06 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