--- 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)
--- 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"
--- 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>
--- 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