# HG changeset patch
# User desharna
# Date 1743146647 -3600
# Node ID 7fee9141da5e5cc6e9bbe874a7c1eec658fc8f95
# Parent  5af097d05e99a6726217e6c6612b039e3ebc11a4# Parent  35a219e372b02f8c9e37a1f88db6b164a27bba3f
merged

diff -r 5af097d05e99 -r 7fee9141da5e src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Thu Mar 27 16:35:41 2025 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy	Fri Mar 28 08:24:07 2025 +0100
@@ -211,6 +211,74 @@
     by (metis \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff norm_zero)
 qed
 
+lemma raw_has_prod_imp_nonzero:
+  assumes "raw_has_prod f N P" "n \<ge> N"
+  shows   "f n \<noteq> 0"
+proof
+  assume "f n = 0"
+  from assms(1) have lim: "(\<lambda>m. (\<Prod>k\<le>m. f (k + N))) \<longlonglongrightarrow> P" and "P \<noteq> 0"
+    unfolding raw_has_prod_def by blast+
+  have "eventually (\<lambda>m. m \<ge> n - N) at_top"
+    by (rule eventually_ge_at_top)
+  hence "eventually (\<lambda>m. (\<Prod>k\<le>m. f (k + N)) = 0) at_top"
+  proof eventually_elim
+    case (elim m)
+    have "f ((n - N) + N) = 0" "n - N \<in> {..m}" "finite {..m}"
+      using \<open>n \<ge> N\<close> \<open>f n = 0\<close> elim by auto
+    thus "(\<Prod>k\<le>m. f (k + N)) = 0"
+      using prod_zero[of "{..m}" "\<lambda>k. f (k + N)"] by blast
+  qed
+  with lim have "P = 0"
+    by (simp add: LIMSEQ_const_iff tendsto_cong)
+  thus False
+    using \<open>P \<noteq> 0\<close> by contradiction
+qed
+
+lemma has_prod_imp_tendsto:
+  fixes f :: "nat \<Rightarrow> 'a :: {semidom, t2_space}"
+  assumes "f has_prod P"
+  shows   "(\<lambda>n. \<Prod>k\<le>n. f k) \<longlonglongrightarrow> P"
+proof (cases "P = 0")
+  case False
+  with assms show ?thesis
+    by (auto simp: has_prod_def raw_has_prod_def)
+next
+  case True
+  with assms obtain N P' where "f N = 0" "raw_has_prod f (Suc N) P'"
+    by (auto simp: has_prod_def)
+  thus ?thesis
+    using LIMSEQ_prod_0 True \<open>f N = 0\<close> by blast
+qed
+
+lemma has_prod_imp_tendsto':
+  fixes f :: "nat \<Rightarrow> 'a :: {semidom, t2_space}"
+  assumes "f has_prod P"
+  shows   "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> P"
+  using has_prod_imp_tendsto[OF assms] LIMSEQ_lessThan_iff_atMost by blast
+
+lemma has_prod_nonneg:
+  assumes "f has_prod P" "\<And>n. f n \<ge> (0::real)"
+  shows   "P \<ge> 0"
+proof (rule tendsto_le)
+  show "((\<lambda>n. \<Prod>i\<le>n. f i)) \<longlonglongrightarrow> P"
+    using assms(1) by (rule has_prod_imp_tendsto)
+  show "(\<lambda>n. 0::real) \<longlonglongrightarrow> 0"
+    by auto
+qed (use assms in \<open>auto intro!: always_eventually prod_nonneg\<close>)
+
+lemma has_prod_pos:
+  assumes "f has_prod P" "\<And>n. f n > (0::real)"
+  shows   "P > 0"
+proof -
+  have "P \<ge> 0"
+    by (rule has_prod_nonneg[OF assms(1)]) (auto intro!: less_imp_le assms(2))
+  moreover have "f n \<noteq> 0" for n
+    using assms(2)[of n] by auto
+  hence "P \<noteq> 0"
+    using has_prod_0_iff[of f] assms by auto
+  ultimately show ?thesis
+    by linarith
+qed
 
 subsection\<open>Absolutely convergent products\<close>
 
@@ -986,6 +1054,11 @@
   shows "prodinf f = (\<Prod>n\<in>N. f n)"
   using has_prod_finite[OF assms, THEN has_prod_unique] by simp
 
+lemma convergent_prod_tendsto_imp_has_prod:
+  assumes "convergent_prod f" "(\<lambda>n. (\<Prod>i\<le>n. f i)) \<longlonglongrightarrow> P"
+  shows   "f has_prod P"
+  using assms by (metis convergent_prod_imp_has_prod has_prod_imp_tendsto limI)
+    
 end
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Infinite products on ordered topological monoids\<close>
@@ -1520,6 +1593,61 @@
 
 end
 
+lemma prod_ge_prodinf: 
+  fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}"
+  assumes "f has_prod a" "\<And>i. 0 \<le> f i" "\<And>i. i \<ge> n \<Longrightarrow> f i \<le> 1"
+  shows "prod f {..<n} \<ge> prodinf f"
+proof (rule has_prod_le; (intro conjI)?)
+  show "f has_prod prodinf f"
+    using assms(1) has_prod_unique by blast
+  show "(\<lambda>r. if r \<in> {..<n} then f r else 1) has_prod prod f {..<n}"
+    by (rule has_prod_If_finite_set) auto
+next
+  fix i 
+  show "f i \<ge> 0"
+    by (rule assms)
+  show "f i \<le> (if i \<in> {..<n} then f i else 1)"
+    using assms(3)[of i] by auto
+qed
+
+lemma has_prod_less:
+  fixes F G :: real
+  assumes less: "f m < g m"
+  assumes f: "f has_prod F" and g: "g has_prod G"
+  assumes pos: "\<And>n. 0 < f n" and le: "\<And>n. f n \<le> g n"
+  shows   "F < G"
+proof -
+  define F' G' where "F' = (\<Prod>n<Suc m. f n)" and "G' = (\<Prod>n<Suc m. g n)"
+  have [simp]: "f n \<noteq> 0" "g n \<noteq> 0" for n
+    using pos[of n] le[of n] by auto
+  have [simp]: "F' \<noteq> 0" "G' \<noteq> 0"
+    by (auto simp: F'_def G'_def)
+  have f': "(\<lambda>n. f (n + Suc m)) has_prod (F / F')"
+    unfolding F'_def using f
+    by (intro has_prod_split_initial_segment) auto
+  have g': "(\<lambda>n. g (n + Suc m)) has_prod (G / G')"
+    unfolding G'_def using g
+    by (intro has_prod_split_initial_segment) auto
+  have "F' * (F / F') < G' * (F / F')"
+  proof (rule mult_strict_right_mono)
+    show "F' < G'"
+      unfolding F'_def G'_def
+      by (rule prod_mono_strict[of m])
+         (auto intro: le less_imp_le[OF pos] less_le_trans[OF pos le] less)
+    show "F / F' > 0"
+      using f' by (rule has_prod_pos) (use pos in auto)
+  qed
+  also have "\<dots> \<le> G' * (G / G')"
+  proof (rule mult_left_mono)
+    show "F / F' \<le> G / G'"
+      using f' g' by (rule has_prod_le) (auto intro: less_imp_le[OF pos] le)
+    show "G' \<ge> 0"
+      unfolding G'_def by (intro prod_nonneg order.trans[OF less_imp_le[OF pos] le])
+  qed
+  finally show ?thesis
+    by simp
+qed
+
 
 subsection\<open>Exponentials and logarithms\<close>
 
@@ -1905,4 +2033,364 @@
     by (fastforce simp: prod_defs simp flip: of_real_prod)
 qed
 
+subsection \<open>Convergence criteria: especially uniform convergence of infinite products\<close>
+
+text \<open>
+  Cauchy's criterion for the convergence of infinite products, adapted to proving
+  uniform convergence: let $f_k(x)$ be a sequence of functions such that
+
+    \<^enum> $f_k(x)$ has uniformly bounded partial products, i.e.\ there exists a constant \<open>C\<close>
+      such that $\prod_{k=0}^m f_k(x) \leq C$ for all $m$ and $x\in A$.
+
+    \<^enum> For any $\varepsilon > 0$ there exists a number $M \in \mathbb{N}$ such that, for any
+      $m, n \geq M$ and all $x\in A$ we have $|(\prod_{k=m}^n f_k(x)) - 1| < \varepsilon$
+
+  Then $\prod_{k=0}^n f_k(x)$ converges to $\prod_{k=0}^\infty f_k(x)$ uniformly for all
+  $x \in A$.
+\<close>
+lemma uniformly_convergent_prod_Cauchy:
+  fixes f :: "nat \<Rightarrow> 'a :: topological_space \<Rightarrow> 'b :: {real_normed_div_algebra, comm_ring_1, banach}"
+  assumes C: "\<And>x m. x \<in> A \<Longrightarrow> norm (\<Prod>k<m. f k x) \<le> C"
+  assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>x\<in>A. \<forall>m\<ge>M. \<forall>n\<ge>m. dist (\<Prod>k=m..n. f k x) 1 < e"
+  shows   "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. f n x)"
+proof (rule Cauchy_uniformly_convergent, rule uniformly_Cauchy_onI')
+  fix \<epsilon> :: real assume \<epsilon>: "\<epsilon> > 0"
+  define C' where "C' = max C 1"
+  have C': "C' > 0"
+    by (auto simp: C'_def)
+  define \<delta> where "\<delta> = Min {2 / 3 * \<epsilon> / C', 1 / 2}"
+  from \<epsilon> have "\<delta> > 0"
+    using \<open>C' > 0\<close> by (auto simp: \<delta>_def)
+  obtain M where M: "\<And>x m n. x \<in> A \<Longrightarrow> m \<ge> M \<Longrightarrow> n \<ge> m \<Longrightarrow> dist (\<Prod>k=m..n. f k x) 1 < \<delta>"
+    using \<open>\<delta> > 0\<close> assms by fast
+
+  show "\<exists>M. \<forall>x\<in>A. \<forall>m\<ge>M. \<forall>n>m. dist (\<Prod>k<m. f k x) (\<Prod>k<n. f k x) < \<epsilon>"
+  proof (rule exI, intro ballI allI impI)
+    fix x m n
+    assume x: "x \<in> A" and mn: "M + 1 \<le> m" "m < n"
+    show "dist (\<Prod>k<m. f k x) (\<Prod>k<n. f k x) < \<epsilon>"
+    proof (cases "\<exists>k<m. f k x = 0")
+      case True
+      hence "(\<Prod>k<m. f k x) = 0" and "(\<Prod>k<n. f k x) = 0"
+        using mn x by (auto intro!: prod_zero)
+      thus ?thesis
+        using \<epsilon> by simp
+    next
+      case False
+      have *: "{..<n} = {..<m} \<union> {m..n-1}"
+        using mn by auto
+      have "dist (\<Prod>k<m. f k x) (\<Prod>k<n. f k x) = norm ((\<Prod>k<m. f k x) * ((\<Prod>k=m..n-1. f k x) - 1))"
+        unfolding * by (subst prod.union_disjoint)
+                       (use mn in \<open>auto simp: dist_norm algebra_simps norm_minus_commute\<close>)
+      also have "\<dots> = (\<Prod>k<m. norm (f k x)) * dist (\<Prod>k=m..n-1. f k x) 1"
+        by (simp add: norm_mult dist_norm prod_norm)
+      also have "\<dots> < (\<Prod>k<m. norm (f k x)) * (2 / 3 * \<epsilon> / C')"
+      proof (rule mult_strict_left_mono)
+        show "dist (\<Prod>k = m..n - 1. f k x) 1 < 2 / 3 * \<epsilon> / C'"
+          using M[of x m "n-1"] x mn unfolding \<delta>_def by fastforce
+      qed (use False in \<open>auto intro!: prod_pos\<close>)
+      also have "(\<Prod>k<m. norm (f k x)) = (\<Prod>k<M. norm (f k x)) * norm (\<Prod>k=M..<m. (f k x))"
+      proof -
+        have *: "{..<m} = {..<M} \<union> {M..<m}"
+          using mn by auto
+        show ?thesis
+          unfolding * using mn by (subst prod.union_disjoint) (auto simp: prod_norm)
+      qed
+      also have "norm (\<Prod>k=M..<m. (f k x)) \<le> 3 / 2"
+      proof -
+        have "dist (\<Prod>k=M..m-1. f k x) 1 < \<delta>"
+          using M[of x M "m-1"] x mn \<open>\<delta> > 0\<close> by auto
+        also have "\<dots> \<le> 1 / 2"
+          by (simp add: \<delta>_def)
+        also have "{M..m-1} = {M..<m}"
+          using mn by auto
+        finally have "norm (\<Prod>k=M..<m. f k x) \<le> norm (1 :: 'b) + 1 / 2"
+          by norm
+        thus ?thesis
+          by simp
+      qed
+      hence "(\<Prod>k<M. norm (f k x)) * norm (\<Prod>k = M..<m. f k x) * (2 / 3 * \<epsilon> / C') \<le>
+             (\<Prod>k<M. norm (f k x)) * (3 / 2) * (2 / 3 * \<epsilon> / C')"
+        using \<epsilon> C' by (intro mult_left_mono mult_right_mono prod_nonneg) auto
+      also have "\<dots> \<le> C' * (3 / 2) * (2 / 3 * \<epsilon> / C')"
+      proof (intro mult_right_mono)
+        have "(\<Prod>k<M. norm (f k x)) \<le> C"
+          using C[of x M] x by (simp add: prod_norm)
+        also have "\<dots> \<le> C'"
+          by (simp add: C'_def)
+        finally show "(\<Prod>k<M. norm (f k x)) \<le> C'" .
+      qed (use \<epsilon> C' in auto)
+      finally show "dist (\<Prod>k<m. f k x) (\<Prod>k<n. f k x) < \<epsilon>"
+        using \<open>C' > 0\<close> by (simp add: field_simps)
+    qed
+  qed
+qed
+
+text \<open>
+  By instantiating the set $A$ in this result with a singleton set, we obtain the ``normal''
+  Cauchy criterion for infinite products:
+\<close>
+lemma convergent_prod_Cauchy_sufficient:
+  fixes f :: "nat \<Rightarrow> 'b :: {real_normed_div_algebra, comm_ring_1, banach}"
+  assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>m n. M \<le> m \<longrightarrow> m \<le> n \<longrightarrow> dist (\<Prod>k=m..n. f k) 1 < e"
+  shows   "convergent_prod f"
+proof -
+  obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> m \<Longrightarrow> dist (prod f {m..n}) 1 < 1 / 2"
+    using assms(1)[of "1 / 2"] by auto
+  have nz: "f m \<noteq> 0" if "m \<ge> M" for m
+    using M[of m m] that by auto
+
+  have M': "dist (prod (\<lambda>k. f (k + M)) {m..<n}) 1 < 1 / 2" for m n
+  proof (cases "m < n")
+    case True
+    have "dist (prod f {m+M..n-1+M}) 1 < 1 / 2"
+      by (rule M) (use True in auto)
+    also have "prod f {m+M..n-1+M} = prod (\<lambda>k. f (k + M)) {m..<n}"
+      by (rule prod.reindex_bij_witness[of _ "\<lambda>k. k + M" "\<lambda>k. k - M"]) (use True in auto)
+    finally show ?thesis .
+  qed auto 
+
+  have "uniformly_convergent_on {0::'b} (\<lambda>N x. \<Prod>n<N. f (n + M))"
+  proof (rule uniformly_convergent_prod_Cauchy)
+    fix m :: nat
+    have "norm (\<Prod>k=0..<m. f (k + M)) < norm (1 :: 'b) + 1 / 2"
+      using M'[of 0 m] by norm
+    thus "norm (\<Prod>k<m. f (k + M)) \<le> 3 / 2"
+      by (simp add: atLeast0LessThan)
+  next
+    fix e :: real assume e: "e > 0"
+    obtain M' where M': "\<And>m n. M' \<le> m \<longrightarrow> m \<le> n \<longrightarrow> dist (\<Prod>k=m..n. f k) 1 < e"
+      using assms e by blast
+    show "\<exists>M'. \<forall>x\<in>{0}. \<forall>m\<ge>M'. \<forall>n\<ge>m. dist (\<Prod>k=m..n. f (k + M)) 1 < e"
+    proof (rule exI[of _ M'], intro ballI impI allI)
+      fix m n :: nat assume "M' \<le> m" "m \<le> n"
+      thus "dist (\<Prod>k=m..n. f (k + M)) 1 < e"
+        using M' by (metis add.commute add_left_mono prod.shift_bounds_cl_nat_ivl trans_le_add1)
+    qed
+  qed
+  hence "convergent (\<lambda>N. \<Prod>n<N. f (n + M))"
+    by (rule uniformly_convergent_imp_convergent[of _ _ 0]) auto
+  then obtain L where L: "(\<lambda>N. \<Prod>n<N. f (n + M)) \<longlonglongrightarrow> L"
+    unfolding convergent_def by blast
+
+  show ?thesis
+    unfolding convergent_prod_altdef
+  proof (rule exI[of _ M], rule exI[of _ L], intro conjI)
+    show "\<forall>n\<ge>M. f n \<noteq> 0"
+      using nz by auto
+  next
+    show "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> L"
+      using LIMSEQ_Suc[OF L] by (subst (asm) lessThan_Suc_atMost)
+  next
+    have "norm L \<ge> 1 / 2"
+    proof (rule tendsto_lowerbound)
+      show "(\<lambda>n. norm (\<Prod>i<n. f (i + M))) \<longlonglongrightarrow> norm L"
+        by (intro tendsto_intros L)
+      show "\<forall>\<^sub>F n in sequentially. 1 / 2 \<le> norm (\<Prod>i<n. f (i + M))"
+      proof (intro always_eventually allI)
+        fix m :: nat
+        have "norm (\<Prod>k=0..<m. f (k + M)) \<ge> norm (1 :: 'b) - 1 / 2"
+          using M'[of 0 m] by norm
+        thus "norm (\<Prod>k<m. f (k + M)) \<ge> 1 / 2"
+          by (simp add: atLeast0LessThan)
+      qed
+    qed auto
+    thus "L \<noteq> 0"
+      by auto
+  qed
+qed
+
+
+text \<open>
+  We now prove that the Cauchy criterion for pointwise convergence is both necessary
+  and sufficient.
+\<close>
+lemma convergent_prod_Cauchy_necessary:
+  fixes f :: "nat \<Rightarrow> 'b :: {real_normed_field, banach}"
+  assumes "convergent_prod f" "e > 0"
+  shows   "\<exists>M. \<forall>m n. M \<le> m \<longrightarrow> m \<le> n \<longrightarrow> dist (\<Prod>k=m..n. f k) 1 < e"
+proof -
+  have *: "\<exists>M. \<forall>m n. M \<le> m \<longrightarrow> m \<le> n \<longrightarrow> dist (\<Prod>k=m..n. f k) 1 < e"
+    if f: "convergent_prod f" "0 \<notin> range f" and e: "e > 0"
+    for f :: "nat \<Rightarrow> 'b" and e :: real
+  proof -
+    have *: "(\<lambda>n. norm (\<Prod>k<n. f k)) \<longlonglongrightarrow> norm (\<Prod>k. f k)"
+      using has_prod_imp_tendsto' f(1) by (intro tendsto_norm) blast
+    from f(1,2) have [simp]: "(\<Prod>k. f k) \<noteq> 0"
+      using prodinf_nonzero by fastforce
+    obtain M' where M': "norm (\<Prod>k<m. f k) > norm (\<Prod>k. f k) / 2" if "m \<ge> M'" for m
+      using order_tendstoD(1)[OF *, of "norm (\<Prod>k. f k) / 2"]
+      by (auto simp: eventually_at_top_linorder)
+    define M where "M = Min (insert (norm (\<Prod>k. f k) / 2) ((\<lambda>m. norm (\<Prod>k<m. f k)) ` {..<M'}))"
+    have "M > 0"
+      unfolding M_def using f(2) by (subst Min_gr_iff) auto
+    have norm_ge: "norm (\<Prod>k<m. f k) \<ge> M" for m
+    proof (cases "m \<ge> M'")
+      case True
+      have "M \<le> norm (\<Prod>k. f k) / 2"
+        unfolding M_def by (intro Min.coboundedI) auto
+      also from True have "norm (\<Prod>k<m. f k) > norm (\<Prod>k. f k) / 2"
+        by (intro M')
+      finally show ?thesis by linarith
+    next
+      case False
+      thus ?thesis
+        unfolding M_def
+        by (intro Min.coboundedI) auto
+    qed
+
+    have "convergent (\<lambda>n. \<Prod>k<n. f k)"
+      using f(1) convergent_def has_prod_imp_tendsto' by blast
+    hence "Cauchy (\<lambda>n. \<Prod>k<n. f k)"
+      by (rule convergent_Cauchy)
+    moreover have "e * M > 0"
+      using e \<open>M > 0\<close> by auto
+    ultimately obtain N where N: "dist (\<Prod>k<m. f k) (\<Prod>k<n. f k) < e * M" if "m \<ge> N" "n \<ge> N" for m n
+      unfolding Cauchy_def by fast
+
+    show "\<exists>M. \<forall>m n. M \<le> m \<longrightarrow> m \<le> n \<longrightarrow> dist (prod f {m..n}) 1 < e"
+    proof (rule exI[of _ N], intro allI impI, goal_cases)
+      case (1 m n)
+      have "dist (\<Prod>k<m. f k) (\<Prod>k<Suc n. f k) < e * M"
+        by (rule N) (use 1 in auto)
+      also have "dist (\<Prod>k<m. f k) (\<Prod>k<Suc n. f k) = norm ((\<Prod>k<Suc n. f k) - (\<Prod>k<m. f k))"
+        by (simp add: dist_norm norm_minus_commute)
+      also have "(\<Prod>k<Suc n. f k) = (\<Prod>k\<in>{..<m}\<union>{m..n}. f k)"
+        using 1 by (intro prod.cong) auto
+      also have "\<dots> = (\<Prod>k\<in>{..<m}. f k) * (\<Prod>k\<in>{m..n}. f k)"
+        by (subst prod.union_disjoint) auto
+      also have "\<dots> - (\<Prod>k<m. f k) = (\<Prod>k<m. f k) * ((\<Prod>k\<in>{m..n}. f k) - 1)"
+        by (simp add: algebra_simps)
+      finally have "norm (prod f {m..n} - 1) < e * M / norm (prod f {..<m})"
+        using f(2) by (auto simp add: norm_mult divide_simps mult_ac)
+      also have "\<dots> \<le> e * M / M"
+        using e \<open>M > 0\<close> f(2) by (intro divide_left_mono norm_ge mult_pos_pos) auto
+      also have "\<dots> = e"
+        using \<open>M > 0\<close> by simp
+      finally show ?case
+        by (simp add: dist_norm)
+    qed
+  qed
+
+  obtain M where M: "f m \<noteq> 0" if "m \<ge> M" for m
+    using convergent_prod_imp_ev_nonzero[OF assms(1)]
+    by (auto simp: eventually_at_top_linorder)
+
+  have "\<exists>M'. \<forall>m n. M' \<le> m \<longrightarrow> m \<le> n \<longrightarrow> dist (\<Prod>k=m..n. f (k + M)) 1 < e"
+    by (rule *) (use assms M in auto)
+  then obtain M' where M': "dist (\<Prod>k=m..n. f (k + M)) 1 < e" if "M' \<le> m" "m \<le> n" for m n
+    by blast
+
+  show "\<exists>M. \<forall>m n. M \<le> m \<longrightarrow> m \<le> n \<longrightarrow> dist (prod f {m..n}) 1 < e"
+  proof (rule exI[of _ "M + M'"], safe, goal_cases)
+    case (1 m n)
+    have "dist (\<Prod>k=m-M..n-M. f (k + M)) 1 < e"
+      by (rule M') (use 1 in auto)
+    also have "(\<Prod>k=m-M..n-M. f (k + M)) = (\<Prod>k=m..n. f k)"
+      using 1 by (intro prod.reindex_bij_witness[of _ "\<lambda>k. k - M" "\<lambda>k. k + M"]) auto
+    finally show ?case .
+  qed
+qed
+
+lemma convergent_prod_Cauchy_iff:
+  fixes f :: "nat \<Rightarrow> 'b :: {real_normed_field, banach}"
+  shows "convergent_prod f \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m n. M \<le> m \<longrightarrow> m \<le> n \<longrightarrow> dist (\<Prod>k=m..n. f k) 1 < e)"
+  using convergent_prod_Cauchy_necessary[of f] convergent_prod_Cauchy_sufficient[of f]
+  by blast
+
+lemma uniformly_convergent_on_prod:
+  fixes f :: "nat \<Rightarrow> 'a :: topological_space \<Rightarrow> 'b :: {real_normed_div_algebra, comm_ring_1, banach}"
+  assumes cont: "\<And>n. continuous_on A (f n)"
+  assumes A: "compact A"
+  assumes conv_sum: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. norm (f n x))"
+  shows   "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f n x)"
+proof -
+  have lim: "uniform_limit A (\<lambda>n x. \<Sum>k<n. norm (f k x)) (\<lambda>x. \<Sum>k. norm (f k x)) sequentially"
+    by (rule uniform_limit_suminf) fact
+  have cont': "\<forall>\<^sub>F n in sequentially. continuous_on A (\<lambda>x. \<Sum>k<n. norm (f k x))"
+    using cont by (auto intro!: continuous_intros always_eventually cont)
+  have "continuous_on A (\<lambda>x. \<Sum>k. norm (f k x))"
+    by (rule uniform_limit_theorem[OF cont' lim]) auto
+  hence "compact ((\<lambda>x. \<Sum>k. norm (f k x)) ` A)"
+    by (intro compact_continuous_image A)
+  hence "bounded ((\<lambda>x. \<Sum>k. norm (f k x)) ` A)"
+    by (rule compact_imp_bounded)
+  then obtain C where C: "norm (\<Sum>k. norm (f k x)) \<le> C" if "x \<in> A" for x
+    unfolding bounded_iff by blast
+  show ?thesis
+  proof (rule uniformly_convergent_prod_Cauchy)
+    fix x :: 'a and m :: nat
+    assume x: "x \<in> A"
+    have "norm (\<Prod>k<m. 1 + f k x) = (\<Prod>k<m. norm (1 + f k x))"
+      by (simp add: prod_norm)
+    also have "\<dots> \<le> (\<Prod>k<m. norm (1 :: 'b) + norm (f k x))"
+      by (intro prod_mono) norm
+    also have "\<dots> = (\<Prod>k<m. 1 + norm (f k x))"
+      by simp
+    also have "\<dots> \<le> exp (\<Sum>k<m. norm (f k x))"
+      by (rule prod_le_exp_sum) auto
+    also have "(\<Sum>k<m. norm (f k x)) \<le> (\<Sum>k. norm (f k x))"
+    proof (rule sum_le_suminf)
+      have "(\<lambda>n. \<Sum>k<n. norm (f k x)) \<longlonglongrightarrow> (\<Sum>k. norm (f k x))"
+        by (rule tendsto_uniform_limitI[OF lim]) fact
+      thus "summable (\<lambda>k. norm (f k x))"
+        using sums_def sums_iff by blast
+    qed auto
+    also have "exp (\<Sum>k. norm (f k x)) \<le> exp (norm (\<Sum>k. norm (f k x)))"
+      by simp
+    also have "norm (\<Sum>k. norm (f k x)) \<le> C"
+      by (rule C) fact
+    finally show "norm (\<Prod>k<m. 1 + f k x) \<le> exp C"
+      by - simp_all
+  next
+    fix \<epsilon> :: real assume \<epsilon>: "\<epsilon> > 0"
+    have "uniformly_Cauchy_on A (\<lambda>N x. \<Sum>n<N. norm (f n x))"
+      by (rule uniformly_convergent_Cauchy) fact
+    moreover have "ln (1 + \<epsilon>) > 0"
+      using \<epsilon> by simp
+    ultimately obtain M where M: "\<And>m n x. x \<in> A \<Longrightarrow> M \<le> m \<Longrightarrow> M \<le> n \<Longrightarrow>
+        dist (\<Sum>k<m. norm (f k x)) (\<Sum>k<n. norm (f k x)) < ln (1 + \<epsilon>)"
+      using \<epsilon> unfolding uniformly_Cauchy_on_def by metis
+  
+    show "\<exists>M. \<forall>x\<in>A. \<forall>m\<ge>M. \<forall>n\<ge>m. dist (\<Prod>k = m..n. 1 + f k x) 1 < \<epsilon>"
+    proof (rule exI, intro ballI allI impI)
+      fix x m n
+      assume x: "x \<in> A" and mn: "M \<le> m" "m \<le> n"
+      have "dist (\<Sum>k<m. norm (f k x)) (\<Sum>k<Suc n. norm (f k x)) < ln (1 + \<epsilon>)"
+        by (rule M) (use x mn in auto)
+      also have "dist (\<Sum>k<m. norm (f k x)) (\<Sum>k<Suc n. norm (f k x)) =
+                 \<bar>\<Sum>k\<in>{..<Suc n}-{..<m}. norm (f k x)\<bar>"
+        using mn by (subst sum_diff) (auto simp: dist_norm)
+      also have "{..<Suc n}-{..<m} = {m..n}"
+        using mn by auto
+      also have "\<bar>\<Sum>k=m..n. norm (f k x)\<bar> = (\<Sum>k=m..n. norm (f k x))"
+        by (intro abs_of_nonneg sum_nonneg) auto
+      finally have *: "(\<Sum>k=m..n. norm (f k x)) < ln (1 + \<epsilon>)" .
+  
+      have "dist (\<Prod>k=m..n. 1 + f k x) 1 = norm ((\<Prod>k=m..n. 1 + f k x) - 1)"
+        by (simp add: dist_norm)
+      also have "norm ((\<Prod>k=m..n. 1 + f k x) - 1) \<le> (\<Prod>n=m..n. 1 + norm (f n x)) - 1"
+        by (rule norm_prod_minus1_le_prod_minus1)
+      also have "(\<Prod>n=m..n. 1 + norm (f n x)) \<le> exp (\<Sum>k=m..n. norm (f k x))"
+        by (rule prod_le_exp_sum) auto
+      also note *
+      finally show "dist (\<Prod>k = m..n. 1 + f k x) 1 < \<epsilon>"
+        using \<epsilon> by - simp_all
+    qed
+  qed
+qed
+
+lemma uniformly_convergent_on_prod':
+  fixes f :: "nat \<Rightarrow> 'a :: topological_space \<Rightarrow> 'b :: {real_normed_div_algebra, comm_ring_1, banach}"
+  assumes cont: "\<And>n. continuous_on A (f n)"
+  assumes A: "compact A"
+  assumes conv_sum: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. norm (f n x - 1))"
+  shows "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. f n x)"
+proof -
+  have "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + (f n x - 1))"
+    by (rule uniformly_convergent_on_prod) (use assms in \<open>auto intro!: continuous_intros\<close>)
+  thus ?thesis
+    by simp
+qed
+
 end
diff -r 5af097d05e99 -r 7fee9141da5e src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Thu Mar 27 16:35:41 2025 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Fri Mar 28 08:24:07 2025 +0100
@@ -41,6 +41,22 @@
   "(\<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_on_subset:
+  "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
+  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
+
+lemma uniformly_convergent_on_subset:
+  assumes "uniformly_convergent_on A f" "B \<subseteq> A"
+  shows   "uniformly_convergent_on B f"
+  using assms by (meson uniform_limit_on_subset uniformly_convergent_on_def)
+
+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 uniformly_convergent_on_singleton:
+  "uniformly_convergent_on {x} f \<longleftrightarrow> convergent (\<lambda>n. f n x)"
+  by (auto simp: uniformly_convergent_on_def convergent_def)
+
 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 +87,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"
@@ -378,7 +407,7 @@
 qed (metis uniformly_convergent_on_sum_E)
 
 lemma uniform_limit_suminf:
-  fixes f:: "nat \<Rightarrow> 'a::{metric_space, comm_monoid_add} \<Rightarrow> 'a"
+  fixes f:: "nat \<Rightarrow> 'a :: topological_space \<Rightarrow> 'b::{metric_space, comm_monoid_add}"
   assumes "uniformly_convergent_on X (\<lambda>n x. \<Sum>k<n. f k x)" 
   shows "uniform_limit X (\<lambda>n x. \<Sum>k<n. f k x) (\<lambda>x. \<Sum>k. f k x) sequentially"
 proof -
@@ -913,10 +942,6 @@
   shows "uniform_limit (Union I) f g F"
   by (metis SUP_identity_eq assms uniform_limit_on_UNION)
 
-lemma uniform_limit_on_subset:
-  "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
-  by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
-
 lemma uniform_limit_bounded:
   fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::metric_space"
   assumes l: "uniform_limit S f l F"
@@ -982,7 +1007,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 5af097d05e99 -r 7fee9141da5e src/HOL/Complex_Analysis/Great_Picard.thy
--- a/src/HOL/Complex_Analysis/Great_Picard.thy	Thu Mar 27 16:35:41 2025 +0100
+++ b/src/HOL/Complex_Analysis/Great_Picard.thy	Fri Mar 28 08:24:07 2025 +0100
@@ -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}"
diff -r 5af097d05e99 -r 7fee9141da5e src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Thu Mar 27 16:35:41 2025 +0100
+++ b/src/Pure/Build/build_manager.scala	Fri Mar 28 08:24:07 2025 +0100
@@ -871,7 +871,10 @@
     val rsync_context = Rsync.Context()
 
     private def sync(repository: Mercurial.Repository, rev: String, target: Path): String = {
-      repository.pull()
+      val pull_result = Exn.capture(repository.pull())
+      if (Exn.is_exn(pull_result)) {
+        echo_error_message("Could not read from repository: " + Exn.the_exn(pull_result).getMessage)
+      }
 
       if (rev.nonEmpty) repository.sync(rsync_context, target, rev = rev)