diff -r 6969d0ffc576 -r 7ff71bdcf731 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Tue Dec 20 22:24:36 2022 +0000
+++ b/src/HOL/Analysis/Infinite_Products.thy	Wed Dec 21 12:30:48 2022 +0000
@@ -710,6 +710,24 @@
   using assms convergent_prod_offset_0 [OF assms]
   by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff)
 
+lemma prodinf_eq_lim':
+  fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
+  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
+  shows "prodinf f = lim (\<lambda>n. \<Prod>i<n. f i)"
+  by (metis assms prodinf_eq_lim LIMSEQ_lessThan_iff_atMost convergent_prod_iff_nz_lim limI)
+
+lemma prodinf_eq_prod_lim:
+  fixes a:: "'a :: {topological_semigroup_mult,t2_space,idom}"
+  assumes "(\<lambda>n. \<Prod>k\<le>n. f k) \<longlonglongrightarrow> a" "a \<noteq> 0"
+  shows"(\<Prod>k. f k) = a"
+  by (metis LIMSEQ_prod_0 LIMSEQ_unique assms convergent_prod_iff_nz_lim limI prodinf_eq_lim)
+
+lemma prodinf_eq_prod_lim':
+  fixes a:: "'a :: {topological_semigroup_mult,t2_space,idom}"
+  assumes "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> a" "a \<noteq> 0"
+  shows"(\<Prod>k. f k) = a"
+  using LIMSEQ_lessThan_iff_atMost assms prodinf_eq_prod_lim by blast
+
 lemma has_prod_one[simp, intro]: "(\<lambda>n. 1) has_prod 1"
   unfolding prod_defs by auto
 
@@ -875,6 +893,34 @@
   shows "(\<lambda>r. if r = i then f r else 1) has_prod f i"
   using has_prod_If_finite[of "\<lambda>r. r = i"] by simp
 
+text \<open>The ge1 assumption can probably be weakened, at the expense of extra work\<close>
+lemma uniform_limit_prodinf:
+  fixes f:: "nat \<Rightarrow> real \<Rightarrow> real"
+  assumes "uniformly_convergent_on X (\<lambda>n x. \<Prod>k<n. f k x)" 
+    and ge1: "\<And>x k . x \<in> X \<Longrightarrow> f k x \<ge> 1"
+  shows "uniform_limit X (\<lambda>n x. \<Prod>k<n. f k x) (\<lambda>x. \<Prod>k. f k x) sequentially"
+proof -
+  have ul: "uniform_limit X (\<lambda>n x. \<Prod>k<n. f k x) (\<lambda>x. lim (\<lambda>n. \<Prod>k<n. f k x)) sequentially"
+    using assms uniformly_convergent_uniform_limit_iff by blast
+  moreover have "(\<Prod>k. f k x) = lim (\<lambda>n. \<Prod>k<n. f k x)" if "x \<in> X" for x
+  proof (intro prodinf_eq_lim')
+    have tends: "(\<lambda>n. \<Prod>k<n. f k x) \<longlonglongrightarrow> lim (\<lambda>n. \<Prod>k<n. f k x)"
+      using tendsto_uniform_limitI [OF ul] that by metis
+    moreover have "(\<Prod>k<n. f k x) \<ge> 1" for n
+      using ge1 by (simp add: prod_ge_1 that)
+    ultimately have "lim (\<lambda>n. \<Prod>k<n. f k x) \<ge> 1"
+      by (meson LIMSEQ_le_const)
+    then have "raw_has_prod (\<lambda>k. f k x) 0 (lim (\<lambda>n. \<Prod>k<n. f k x))"
+      using LIMSEQ_lessThan_iff_atMost tends by (auto simp: raw_has_prod_def)
+    then show "convergent_prod (\<lambda>k. f k x)"
+      unfolding convergent_prod_def by blast
+    show "\<And>k. f k x \<noteq> 0"
+      by (smt (verit) ge1 that)
+  qed
+  ultimately show ?thesis
+    by (metis (mono_tags, lifting) uniform_limit_cong')
+qed
+
 context
   fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
 begin
@@ -944,29 +990,15 @@
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Infinite products on ordered topological monoids\<close>
 
-lemma LIMSEQ_prod_0: 
-  fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}"
-  assumes "f i = 0"
-  shows "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"
-proof (subst tendsto_cong)
-  show "\<forall>\<^sub>F n in sequentially. prod f {..n} = 0"
-  proof
-    show "prod f {..n} = 0" if "n \<ge> i" for n
-      using that assms by auto
-  qed
-qed auto
-
-lemma LIMSEQ_prod_nonneg: 
-  fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"
-  assumes 0: "\<And>n. 0 \<le> f n" and a: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> a"
-  shows "a \<ge> 0"
-  by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a])
-
-
 context
   fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}"
 begin
 
+lemma has_prod_nonzero:
+  assumes "f has_prod a" "a \<noteq> 0"
+  shows "f k \<noteq> 0"
+  using assms by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0 LIMSEQ_unique)
+
 lemma has_prod_le:
   assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n"
   shows "a \<le> b"
@@ -1024,9 +1056,9 @@
 
 lemma prodinf_le_const:
   fixes f :: "nat \<Rightarrow> real"
-  assumes "convergent_prod f" "\<And>n. prod f {..<n} \<le> x" 
+  assumes "convergent_prod f" "\<And>n. n \<ge> N \<Longrightarrow> prod f {..<n} \<le> x" 
   shows "prodinf f \<le> x"
-  by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2)
+  by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2 atMost_iff lessThan_iff less_le)
 
 lemma prodinf_eq_one_iff [simp]: 
   fixes f :: "nat \<Rightarrow> real"