diff -r 6969d0ffc576 -r 7ff71bdcf731 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Dec 20 22:24:36 2022 +0000
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Dec 21 12:30:48 2022 +0000
@@ -2049,6 +2049,48 @@
     by simp
 qed
 
+text\<open>Prop 17.6 of Bak and Newman, Complex Analysis, p. 243. 
+     Only this version is for the reals. Can the two proofs be consolidated?\<close>
+lemma uniformly_convergent_on_prod_real:
+  fixes u :: "nat \<Rightarrow> real \<Rightarrow> real"
+  assumes contu: "\<And>k. continuous_on K (u k)" 
+     and uconv: "uniformly_convergent_on K (\<lambda>n x. \<Sum>k<n. \<bar>u k x\<bar>)"
+     and K: "compact K"
+   shows "uniformly_convergent_on K (\<lambda>n x. \<Prod>k<n. 1 + u k x)"
+proof -
+  define f where "f \<equiv> \<lambda>k. complex_of_real \<circ> u k \<circ> Re"
+  define L where "L \<equiv> complex_of_real ` K"
+  have "compact L"
+    by (simp add: \<open>compact K\<close> L_def compact_continuous_image)
+  have "Re ` complex_of_real ` X = X" for X
+    by (auto simp: image_iff)
+  with contu have contf: "\<And>k. continuous_on L (f k)"
+    unfolding f_def L_def by (intro continuous_intros) auto
+  obtain S where S: "\<And>\<epsilon>. \<epsilon>>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<Sum>k<n. \<bar>u k x\<bar>) (S x) < \<epsilon>"
+    using uconv unfolding uniformly_convergent_on_def uniform_limit_iff by presburger 
+  have "\<forall>\<^sub>F n in sequentially. \<forall>z\<in>L. dist (\<Sum>k<n. cmod (f k z)) ((of_real \<circ> S \<circ> Re) z) < \<epsilon>" 
+    if "\<epsilon>>0" for \<epsilon>
+    using S [OF that] by eventually_elim (simp add: L_def f_def)
+  then have uconvf: "uniformly_convergent_on L (\<lambda>n z. \<Sum>k<n. norm (f k z))"
+    unfolding uniformly_convergent_on_def uniform_limit_iff by blast
+  obtain P where P: "\<And>\<epsilon>. \<epsilon>>0 \<Longrightarrow> \<forall>\<^sub>F n in sequentially. \<forall>z\<in>L. dist (\<Prod>k<n. 1 + f k z) (P z) < \<epsilon>"
+    using uniformly_convergent_on_prod [OF contf \<open>compact L\<close> uconvf]
+    unfolding uniformly_convergent_on_def uniform_limit_iff by blast
+  have \<section>: "\<bar>(\<Prod>k<n. 1 + u k x) - Re (P x)\<bar> \<le> cmod ((\<Prod>k<n. 1 + of_real (u k x)) - P x)" for n x
+  proof -
+    have "(\<Prod>k\<in>N. of_real (1 + u k x)) = (\<Prod>k\<in>N. 1 + of_real (u k x))" for N
+      by force
+    then show ?thesis
+      by (metis Re_complex_of_real abs_Re_le_cmod minus_complex.sel(1) of_real_prod)
+  qed
+  have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<Prod>k<n. 1 + u k x) ((Re \<circ> P \<circ> of_real) x) < \<epsilon>" 
+    if "\<epsilon>>0" for \<epsilon>
+    using P [OF that] by eventually_elim (simp add: L_def f_def dist_norm le_less_trans [OF \<section>])
+  then show ?thesis
+    unfolding uniformly_convergent_on_def uniform_limit_iff by blast 
+qed
+
+
 subsection\<open>The Argument of a Complex Number\<close>
 
 text\<open>Unlike in HOL Light, it's defined for the same interval as the complex logarithm: \<open>(-\<pi>,\<pi>]\<close>.\<close>