Additional new material about infinite products, etc.

--- 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>

--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Tue Dec 20 22:24:36 2022 +0000
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Wed Dec 21 12:30:48 2022 +0000
@@ -1130,6 +1130,12 @@
   using assms uniformly_continuous_on_add [of s f "- g"]
     by (simp add: fun_Compl_def uniformly_continuous_on_minus)
 
+lemma uniformly_continuous_on_sum [continuous_intros]:
+  fixes f :: "'a \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> uniformly_continuous_on S (f i)) \<Longrightarrow> uniformly_continuous_on S (\<lambda>x. \<Sum>i\<in>I. f i x)"
+  by (induction I rule: infinite_finite_induct)
+     (auto simp: uniformly_continuous_on_add uniformly_continuous_on_const)
+
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close>
 

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

--- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Dec 20 22:24:36 2022 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Wed Dec 21 12:30:48 2022 +0000
@@ -361,6 +361,19 @@
   qed
 qed (metis uniformly_convergent_on_sum_E)
 
+lemma uniform_limit_suminf:
+  fixes f:: "nat \<Rightarrow> 'a::{metric_space, comm_monoid_add} \<Rightarrow> 'a"
+  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 -
+  obtain S where S: "uniform_limit X (\<lambda>n x. \<Sum>k<n. f k x) S sequentially"
+    using assms uniformly_convergent_on_def by blast
+  then have "(\<Sum>k. f k x) = S x" if "x \<in> X" for x
+    using that sums_iff sums_def by (blast intro: tendsto_uniform_limitI [OF S])
+  with S show ?thesis
+    by (simp cong: uniform_limit_cong')
+qed
+
 text \<open>TODO: remove explicit formulations
   @{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>
 

--- a/src/HOL/Limits.thy	Tue Dec 20 22:24:36 2022 +0000
+++ b/src/HOL/Limits.thy	Wed Dec 21 12:30:48 2022 +0000
@@ -14,7 +14,7 @@
 text \<open>Lemmas related to shifting/scaling\<close>
 lemma range_add [simp]:
   fixes a::"'a::group_add" shows "range ((+) a) = UNIV"
-  by (metis add_minus_cancel surjI)
+  by simp
 
 lemma range_diff [simp]:
   fixes a::"'a::group_add" shows "range ((-) a) = UNIV"
@@ -1060,6 +1060,21 @@
   shows "((\<lambda>i. prod (f i) I) \<longlongrightarrow> 1) F"
   using tendsto_prod' [of I "\<lambda>x y. f y x" "\<lambda>x. 1"] assms by simp
 
+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"
+    using assms eventually_at_top_linorder by auto
+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])
+
 lemma continuous_prod' [continuous_intros]:
   fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_mult"
   shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>I. f i x)"

--- a/src/HOL/Topological_Spaces.thy	Tue Dec 20 22:24:36 2022 +0000
+++ b/src/HOL/Topological_Spaces.thy	Wed Dec 21 12:30:48 2022 +0000
@@ -3440,7 +3440,7 @@
 lemma uniformly_continuous_on_id[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. x)"
   by (auto simp: uniformly_continuous_on_uniformity filterlim_def)
 
-lemma uniformly_continuous_on_compose[continuous_intros]:
+lemma uniformly_continuous_on_compose:
   "uniformly_continuous_on s g \<Longrightarrow> uniformly_continuous_on (g`s) f \<Longrightarrow>
     uniformly_continuous_on s (\<lambda>x. f (g x))"
   using filterlim_compose[of "\<lambda>(x, y). (f x, f y)" uniformity