--- 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:
--- 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}"