# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1743023464 0
# Node ID 882b80bd10c8d992f9adefdb02ccb1fe3c12ae8e
# Parent  00b59ba22c01ad48c4fa94cf526f9c64cded5f6d
More from Theta_Functions_Library

diff -r 00b59ba22c01 -r 882b80bd10c8 src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Mar 25 21:34:36 2025 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Wed Mar 26 21:11:04 2025 +0000
@@ -41,6 +41,9 @@
   "(\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e) \<Longrightarrow> uniform_limit S f l F"
   by (simp add: uniform_limit_iff)
 
+lemma uniform_limit_singleton [simp]: "uniform_limit {x} f g F \<longleftrightarrow> ((\<lambda>n. f n x) \<longlongrightarrow> g x) F"
+  by (simp add: uniform_limit_iff tendsto_iff)
+
 lemma uniform_limit_sequentially_iff:
   "uniform_limit S f l sequentially \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> S. dist (f n x) (l x) < e)"
   unfolding uniform_limit_iff eventually_sequentially ..
@@ -71,6 +74,19 @@
     by eventually_elim (use \<delta> l in blast)
 qed
 
+lemma uniform_limit_compose':
+  assumes "uniform_limit A f g F" and "h \<in> B \<rightarrow> A"
+  shows   "uniform_limit B (\<lambda>n x. f n (h x)) (\<lambda>x. g (h x)) F"
+  unfolding uniform_limit_iff
+proof (intro strip)
+  fix e :: real
+  assume e: "e > 0"
+  with assms(1) have "\<forall>\<^sub>F n in F. \<forall>x\<in>A. dist (f n x) (g x) < e"
+    by (auto simp: uniform_limit_iff)
+  thus "\<forall>\<^sub>F n in F. \<forall>x\<in>B. dist (f n (h x)) (g (h x)) < e"
+    by eventually_elim (use assms(2) in blast)
+qed
+
 lemma metric_uniform_limit_imp_uniform_limit:
   assumes f: "uniform_limit S f a F"
   assumes le: "eventually (\<lambda>x. \<forall>y\<in>S. dist (g x y) (b y) \<le> dist (f x y) (a y)) F"
@@ -982,7 +998,7 @@
   shows "continuous_on (cball \<xi> r) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i))"
 apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
 apply (rule eventuallyI continuous_intros assms)+
-apply (simp add:)
+apply auto
 done
 
 lemma powser_continuous_sums:
diff -r 00b59ba22c01 -r 882b80bd10c8 src/HOL/Complex_Analysis/Great_Picard.thy
--- a/src/HOL/Complex_Analysis/Great_Picard.thy	Tue Mar 25 21:34:36 2025 +0000
+++ b/src/HOL/Complex_Analysis/Great_Picard.thy	Wed Mar 26 21:11:04 2025 +0000
@@ -1178,8 +1178,7 @@
     have "(\<lambda>z. g z - g z1) holomorphic_on S"
       by (intro holomorphic_intros holg)
     then obtain r where "0 < r" "ball z2 r \<subseteq> S" "\<And>z. dist z2 z < r \<and> z \<noteq> z2 \<Longrightarrow> g z \<noteq> g z1"
-      apply (rule isolated_zeros [of "\<lambda>z. g z - g z1" S z2 z0])
-      using S \<open>z0 \<in> S\<close> z0 z12 by auto
+      using isolated_zeros [of "\<lambda>z. g z - g z1" S z2 z0] S \<open>z0 \<in> S\<close> z0 z12 by auto
     have "g z2 - g z1 \<noteq> 0"
     proof (rule Hurwitz_no_zeros [of "S - {z1}" "\<lambda>n z. \<F> n z - \<F> n z1" "\<lambda>z. g z - g z1"])
       show "open (S - {z1})"
@@ -1200,13 +1199,13 @@
         then have K: "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> K. dist (\<F> n x) (g x) < e/2"
           using \<open>0 < e\<close> by (force simp: intro!: uniform_limitD)
         have "uniform_limit {z1} \<F> g sequentially"
-          by (simp add: ul_g z12)
+          by (intro ul_g) (auto simp: z12)
         then have "\<forall>\<^sub>F n in sequentially. \<forall>x \<in> {z1}. dist (\<F> n x) (g x) < e/2"
           using \<open>0 < e\<close> by (force simp: intro!: uniform_limitD)
         then have z1: "\<forall>\<^sub>F n in sequentially. dist (\<F> n z1) (g z1) < e/2"
           by simp
         show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e" 
-          apply (rule eventually_mono [OF  eventually_conj [OF K z1]])
+          apply (intro eventually_mono [OF  eventually_conj [OF K z1]])
           by (metis (no_types, opaque_lifting) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half)
       qed
       show "\<not> (\<lambda>z. g z - g z1) constant_on S - {z1}"