# HG changeset patch
# User paulson
# Date 1671575076 0
# Node ID 6969d0ffc576cf5edbb819c46fa3ead6e4881830
# Parent  5364cdc3ec0ed2b5562f989a4150d073b75fa588# Parent  b1d57dd345e1b4395ee003d2ff03573a3a5df312
merged

diff -r 5364cdc3ec0e -r 6969d0ffc576 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Dec 20 22:24:36 2022 +0000
@@ -1526,6 +1526,47 @@
 qed
 
 
+lemma norm_Ln_le:
+  fixes z :: complex
+  assumes "norm z < 1/2"
+  shows   "norm (Ln(1+z)) \<le> 2 * norm z"
+proof -
+  have sums: "(\<lambda>n. - ((- z) ^ n) / of_nat n) sums ln (1 + z)"
+    by (intro Ln_series') (use assms in auto)
+  have summable: "summable (\<lambda>n. norm (- ((- z) ^ n / of_nat n)))"
+    using ln_series'[of "-norm z"] assms
+    by (simp add: sums_iff summable_minus_iff norm_power norm_divide)
+
+  have "norm (ln (1 + z)) = norm (\<Sum>n. -((-z) ^ n / of_nat n))"
+    using sums by (simp add: sums_iff)
+  also have "\<dots> \<le> (\<Sum>n. norm (-((-z) ^ n / of_nat n)))"
+    using summable by (rule summable_norm)
+  also have "\<dots> = (\<Sum>n. norm (-((-z) ^ Suc n / of_nat (Suc n))))"
+    using summable by (subst suminf_split_head) auto
+  also have "\<dots> \<le> (\<Sum>n. norm z * (1 / 2) ^ n)"
+  proof (rule suminf_le)
+    show "summable (\<lambda>n. norm z * (1 / 2) ^ n)"
+      by (intro summable_mult summable_geometric) auto
+  next
+    show "summable (\<lambda>n. norm (- ((- z) ^ Suc n / of_nat (Suc n))))"
+      using summable by (subst summable_Suc_iff)
+  next
+    fix n
+    have "norm (-((-z) ^ Suc n / of_nat (Suc n))) = norm z * (norm z ^ n / real (Suc n))"
+      by (simp add: norm_power norm_divide norm_mult del: of_nat_Suc)
+    also have "\<dots> \<le> norm z * ((1 / 2) ^ n / 1)"
+      using assms by (intro mult_left_mono frac_le power_mono) auto
+    finally show "norm (- ((- z) ^ Suc n / of_nat (Suc n))) \<le> norm z * (1 / 2) ^ n"
+      by simp
+  qed
+  also have "\<dots> = norm z * (\<Sum>n. (1 / 2) ^ n)"
+    by (subst suminf_mult) (auto intro: summable_geometric)
+  also have "(\<Sum>n. (1 / 2 :: real) ^ n) = 2"
+    using geometric_sums[of "1 / 2 :: real"] by (simp add: sums_iff)
+  finally show ?thesis
+    by (simp add: mult_ac)
+qed
+
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Quadrant-type results for Ln\<close>
 
 lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
@@ -1796,6 +1837,218 @@
   finally show ?thesis .
 qed
 
+lemma norm_Ln_times_le:
+  assumes "w \<noteq> 0" "z \<noteq> 0"
+  shows  "cmod (Ln(w * z)) \<le> cmod (Ln(w) + Ln(z))"
+proof (cases "- pi < Im(Ln w + Ln z) \<and> Im(Ln w + Ln z) \<le> pi")
+  case True
+  then show ?thesis
+    by (simp add: Ln_times_simple assms)
+next
+  case False
+  then show ?thesis
+    by (smt (verit) Im_Ln_le_pi assms cmod_Im_le_iff exp_Ln exp_add ln_unique mpi_less_Im_Ln mult_eq_0_iff norm_exp_eq_Re)
+qed
+
+corollary norm_Ln_prod_le:
+  fixes f :: "'a \<Rightarrow> complex"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+  shows "cmod (Ln (prod f A)) \<le> (\<Sum>x \<in> A. cmod (Ln (f x)))"
+  using assms
+proof (induction A rule: infinite_finite_induct)
+  case (insert x A)
+  then show ?case
+    by simp (smt (verit) norm_Ln_times_le norm_triangle_ineq prod_zero_iff)
+qed auto
+
+lemma norm_Ln_exp_le: "norm (Ln (exp z)) \<le> norm z"
+  by (smt (verit) Im_Ln_le_pi Ln_exp Re_Ln cmod_Im_le_iff exp_not_eq_zero ln_exp mpi_less_Im_Ln norm_exp_eq_Re)
+
+subsection\<^marker>\<open>tag unimportant\<close>\<open>Uniform convergence and products\<close>
+
+(* TODO: could be generalised perhaps, but then one would have to do without the ln *)
+lemma uniformly_convergent_on_prod_aux:
+  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+  assumes norm_f: "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) < 1"
+  assumes cont: "\<And>n. continuous_on A (f n)"
+  assumes conv: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. ln (1 + f n x))"
+  assumes A: "compact A"
+  shows "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f n x)"
+proof -
+  from conv obtain S where S: "uniform_limit A (\<lambda>N x. \<Sum>n<N. ln (1 + f n x)) S sequentially"
+    by (auto simp: uniformly_convergent_on_def)
+  have cont': "continuous_on A S"
+  proof (rule uniform_limit_theorem[OF _ S])
+    have "f n x + 1 \<notin> \<real>\<^sub>\<le>\<^sub>0" if "x \<in> A" for n x
+    proof
+      assume "f n x + 1 \<in> \<real>\<^sub>\<le>\<^sub>0"
+      then obtain t where t: "t \<le> 0" "f n x + 1 = of_real t"
+        by (auto elim!: nonpos_Reals_cases)
+      hence "f n x = of_real (t - 1)"
+        by (simp add: algebra_simps)
+      also have "norm \<dots> \<ge> 1"
+        using t by (subst norm_of_real) auto
+      finally show False
+        using norm_f[of x n] that by auto
+    qed
+    thus "\<forall>\<^sub>F n in sequentially. continuous_on A (\<lambda>x. \<Sum>n<n. Ln (1 + f n x))"
+      by (auto intro!: always_eventually continuous_intros cont simp: add_ac)
+  qed auto
+
+  define B where "B = {x + y |x y. x \<in> S ` A \<and> y \<in> cball 0 1}"
+  have "compact B"
+    unfolding B_def by (intro compact_sums compact_continuous_image cont' A) auto
+
+  have "uniformly_convergent_on A (\<lambda>N x. exp ((\<Sum>n<N. ln (1 + f n x))))"
+    using conv
+  proof (rule uniformly_convergent_on_compose_uniformly_continuous_on)
+    show "closed B"
+      using \<open>compact B\<close> by (auto dest: compact_imp_closed)
+    show "uniformly_continuous_on B exp"
+      by (intro compact_uniformly_continuous continuous_intros \<open>compact B\<close>)
+
+    have "eventually (\<lambda>N. \<forall>x\<in>A. dist (\<Sum>n<N. Ln (1 + f n x)) (S x) < 1) sequentially"
+      using S unfolding uniform_limit_iff by simp
+    thus "eventually (\<lambda>N. \<forall>x\<in>A. (\<Sum>n<N. Ln (1 + f n x)) \<in> B) sequentially"
+    proof eventually_elim
+      case (elim N)
+      show "\<forall>x\<in>A. (\<Sum>n<N. Ln (1 + f n x)) \<in> B"
+      proof safe
+        fix x assume x: "x \<in> A"
+        have "(\<Sum>n<N. Ln (1 + f n x)) = S x + ((\<Sum>n<N. Ln (1 + f n x)) - S x)"
+          by auto
+        moreover have "((\<Sum>n<N. Ln (1 + f n x)) - S x) \<in> ball 0 1"
+          using elim x by (auto simp: dist_norm norm_minus_commute)
+        ultimately show "(\<Sum>n<N. Ln (1 + f n x)) \<in> B"
+          unfolding B_def using x by fastforce
+      qed
+    qed
+  qed
+  also have "?this \<longleftrightarrow> uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f n x)"
+  proof (intro uniformly_convergent_cong refl always_eventually allI ballI)
+    fix N :: nat and x assume x: "x \<in> A"
+    have "exp (\<Sum>n<N. ln (1 + f n x)) = (\<Prod>n<N. exp (ln (1 + f n x)))"
+      by (simp add: exp_sum)
+    also have "\<dots> = (\<Prod>n<N. 1 + f n x)"
+    proof (rule prod.cong)
+      fix n assume "n \<in> {..<N}"
+      have "f n x \<noteq> -1"
+        using norm_f[of x n] x by auto
+      thus "exp (ln (1 + f n x)) = 1 + f n x"
+        by (simp add: add_eq_0_iff)
+    qed auto
+    finally show "exp (\<Sum>n<N. ln (1 + f n x)) = (\<Prod>n<N. 1 + f n x)" .
+  qed
+  finally show ?thesis .
+qed
+
+(* Theorem 17.6 by Bak & Newman, roughly *)
+lemma uniformly_convergent_on_prod:
+  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+  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 -
+  obtain M where M: "\<And>n x. n \<ge> M \<Longrightarrow> x \<in> A \<Longrightarrow> norm (f n x) < 1 / 2"
+  proof -
+    from conv_sum have "uniformly_Cauchy_on A (\<lambda>N x. \<Sum>n<N. norm (f n x))"
+      using uniformly_convergent_Cauchy by blast
+    moreover have "(1 / 2 :: real) > 0"
+      by simp
+    ultimately obtain M where M:
+      "\<And>x m n. x \<in> A \<Longrightarrow> m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (\<Sum>k<m. norm (f k x)) (\<Sum>k<n. norm (f k x)) < 1 / 2"
+      unfolding uniformly_Cauchy_on_def by fast
+    show ?thesis
+    proof (rule that[of M])
+      fix n x assume nx: "n \<ge> M" "x \<in> A"
+      have "dist (\<Sum>k<Suc n. norm (f k x)) (\<Sum>k<n. norm (f k x)) < 1 / 2"
+        by (rule M) (use nx in auto)
+      also have "dist (\<Sum>k<Suc n. norm (f k x)) (\<Sum>k<n. norm (f k x)) = norm (f n x)"
+        by (simp add: dist_norm)
+      finally show "norm (f n x) < 1 / 2" .
+    qed
+  qed
+
+  have conv: "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. ln (1 + f (n + M) x))"
+  proof (rule uniformly_summable_comparison_test)
+    show "norm (ln (1 + f (n + M) x)) \<le> 2 * norm (f (n + M) x)" if "x \<in> A" for n x
+      by (rule norm_Ln_le) (use M[of "n + M" x] that in auto)
+    have *: "filterlim (\<lambda>n. n + M) at_top at_top"
+      by (rule filterlim_add_const_nat_at_top)
+    have "uniformly_convergent_on A (\<lambda>N x. 2 * ((\<Sum>n<N+M. norm (f n x)) - (\<Sum>n<M. norm (f n x))))"
+      by (intro uniformly_convergent_mult uniformly_convergent_minus
+                uniformly_convergent_on_compose[OF conv_sum *] uniformly_convergent_on_const)
+    also have "(\<lambda>N x. 2 * ((\<Sum>n<N+M. norm (f n x)) - (\<Sum>n<M. norm (f n x)))) =
+               (\<lambda>N x. \<Sum>n<N. 2 * norm (f (n + M) x))" (is "?lhs = ?rhs")
+    proof (intro ext)
+      fix N x
+      have "(\<Sum>n<N+M. norm (f n x)) - (\<Sum>n<M. norm (f n x)) = (\<Sum>n\<in>{..<N+M}-{..<M}. norm (f n x))"
+        by (subst sum_diff) auto
+      also have "\<dots> = (\<Sum>n<N. norm (f (n + M) x))"
+        by (intro sum.reindex_bij_witness[of _ "\<lambda>n. n + M" "\<lambda>n. n - M"]) auto
+      finally show "?lhs N x = ?rhs N x"
+        by (simp add: sum_distrib_left)
+    qed
+    finally show "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. 2 * cmod (f (n + M) x))" .
+  qed
+
+  have conv': "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<N. 1 + f (n + M) x)"
+  proof (rule uniformly_convergent_on_prod_aux)
+    show "norm (f (n + M) x) < 1" if "x \<in> A" for n x
+      using M[of "n + M" x] that by simp
+  qed (use M assms conv in auto)
+
+  then obtain S where S: "uniform_limit A (\<lambda>N x. \<Prod>n<N. 1 + f (n + M) x) S sequentially"
+    by (auto simp: uniformly_convergent_on_def)
+  have cont':  "continuous_on A S"
+    by (intro uniform_limit_theorem[OF _ S] always_eventually ballI allI continuous_intros cont) auto
+
+  have "uniform_limit A (\<lambda>N x. (\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x)) (\<lambda>x. (\<Prod>n<M. 1 + f n x) * S x) sequentially"
+  proof (rule uniform_lim_mult[OF uniform_limit_const S])
+    show "bounded (S ` A)"
+      by (intro compact_imp_bounded compact_continuous_image A cont')
+    show "bounded ((\<lambda>x. \<Prod>n<M. 1 + f n x) ` A)"
+      by (intro compact_imp_bounded compact_continuous_image A continuous_intros cont)
+  qed
+  hence "uniformly_convergent_on A (\<lambda>N x. (\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x))"
+    by (auto simp: uniformly_convergent_on_def)
+  also have "(\<lambda>N x. (\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x)) = (\<lambda>N x. (\<Prod>n<M+N. 1 + f n x))"
+  proof (intro ext)
+    fix N :: nat and x :: complex
+    have "(\<Prod>n<N. 1 + f (n + M) x) = (\<Prod>n\<in>{M..<M+N}. 1 + f n x)"
+      by (intro prod.reindex_bij_witness[of _ "\<lambda>n. n - M" "\<lambda>n. n + M"]) auto
+    also have "(\<Prod>n<M. 1 + f n x) * \<dots> = (\<Prod>n\<in>{..<M}\<union>{M..<M+N}. 1 + f n x)"
+      by (subst prod.union_disjoint) auto
+    also have "{..<M} \<union> {M..<M+N} = {..<M+N}"
+      by auto
+    finally show "(\<Prod>n<M. 1 + f n x) * (\<Prod>n<N. 1 + f (n + M) x) = (\<Prod>n<M+N. 1 + f n x)" .
+  qed
+  finally have "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<M + N. 1 + f n x)"
+    by simp
+  hence "uniformly_convergent_on A (\<lambda>N x. \<Prod>n<M + (N - M). 1 + f n x)"
+    by (rule uniformly_convergent_on_compose) (rule filterlim_minus_const_nat_at_top)
+  also have "?this \<longleftrightarrow> ?thesis"
+  proof (rule uniformly_convergent_cong)
+    show "eventually (\<lambda>x. \<forall>y\<in>A. (\<Prod>n<M + (x - M). 1 + f n y) = (\<Prod>n<x. 1 + f n y)) at_top"
+      using eventually_ge_at_top[of M] by eventually_elim auto
+  qed auto
+  finally show ?thesis .
+qed
+
+lemma uniformly_convergent_on_prod':
+  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+  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
+
 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>
@@ -2623,7 +2876,6 @@
   qed
 qed
 
-
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Some Limits involving Logarithms\<close>
 
 lemma lim_Ln_over_power:
diff -r 5364cdc3ec0e -r 6969d0ffc576 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy	Tue Dec 20 22:24:36 2022 +0000
@@ -118,6 +118,48 @@
   shows "f has_prod s \<Longrightarrow> s = prodinf f"
   by (simp add: has_prod_unique2 prodinf_def the_equality)
 
+lemma has_prod_eq_0_iff:
+  fixes f :: "nat \<Rightarrow> 'a :: {semidom, comm_semiring_1, t2_space}"
+  assumes "f has_prod P"
+  shows   "P = 0 \<longleftrightarrow> 0 \<in> range f"
+proof
+  assume "0 \<in> range f"
+  then obtain N where N: "f N = 0"
+    by auto
+  have "eventually (\<lambda>n. n > N) at_top"
+    by (rule eventually_gt_at_top)
+  hence "eventually (\<lambda>n. (\<Prod>k<n. f k) = 0) at_top"
+    by eventually_elim (use N in auto)
+  hence "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> 0"
+    by (simp add: tendsto_eventually)
+  moreover have "(\<lambda>n. \<Prod>k<n. f k) \<longlonglongrightarrow> P"
+    using assms by (metis N calculation prod_defs(2) raw_has_prod_eq_0 zero_le)
+  ultimately show "P = 0"
+    using tendsto_unique by force
+qed (use assms in \<open>auto simp: has_prod_def\<close>)
+
+lemma has_prod_0D:
+  fixes f :: "nat \<Rightarrow> 'a :: {semidom, comm_semiring_1, t2_space}"
+  shows "f has_prod 0 \<Longrightarrow> 0 \<in> range f"
+  using has_prod_eq_0_iff[of f 0] by auto
+
+lemma has_prod_zeroI:
+  fixes f :: "nat \<Rightarrow> 'a :: {semidom, comm_semiring_1, t2_space}"
+  assumes "f has_prod P" "f n = 0"
+  shows   "P = 0"
+  using assms by (auto simp: has_prod_eq_0_iff)  
+
+lemma raw_has_prod_in_Reals:
+  assumes "raw_has_prod (complex_of_real \<circ> z) M p"
+  shows "p \<in> \<real>"
+  using assms by (auto simp: raw_has_prod_def real_lim_sequentially)
+
+lemma raw_has_prod_of_real_iff: "raw_has_prod (complex_of_real \<circ> z) M (of_real p) \<longleftrightarrow> raw_has_prod z M p"
+  by (auto simp: raw_has_prod_def tendsto_of_real_iff simp flip: of_real_prod)
+
+lemma convergent_prod_of_real_iff: "convergent_prod (complex_of_real \<circ> z) \<longleftrightarrow> convergent_prod z"
+  by (smt (verit, best) Reals_cases convergent_prod_def raw_has_prod_in_Reals raw_has_prod_of_real_iff)
+
 lemma convergent_prod_altdef:
   fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
   shows "convergent_prod f \<longleftrightarrow> (\<exists>M L. (\<forall>n\<ge>M. f n \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"
@@ -1394,6 +1436,25 @@
   shows "(\<Prod>n. f (Suc n)) = prodinf f / f 0"
   using prodinf_split_initial_segment[of 1] assms by simp
 
+lemma has_prod_ignore_initial_segment':
+  assumes "convergent_prod f"
+  shows   "f has_prod ((\<Prod>k<n. f k) * (\<Prod>k. f (k + n)))"
+proof (cases "\<exists>k<n. f k = 0")
+  case True
+  hence [simp]: "(\<Prod>k<n. f k) = 0"
+    by (meson finite_lessThan lessThan_iff prod_zero)
+  thus ?thesis using True assms
+    by (metis convergent_prod_has_prod_iff has_prod_zeroI mult_not_zero)
+next
+  case False
+  hence "(\<lambda>i. f (i + n)) has_prod (prodinf f / prod f {..<n})"
+    using assms by (intro has_prod_split_initial_segment) (auto simp: convergent_prod_has_prod_iff)
+  hence "prodinf f = prod f {..<n} * (\<Prod>k. f (k + n))"
+    using False by (simp add: has_prod_iff divide_simps mult_ac)
+  thus ?thesis
+    using assms by (simp add: convergent_prod_has_prod_iff)
+qed
+
 end
 
 context 
@@ -1745,53 +1806,29 @@
   assumes z: "summable (\<lambda>k. norm (z k))" and non0: "\<And>k. z k \<noteq> -1"
   shows "convergent_prod (\<lambda>k. 1 + z k)" 
 proof -
-  note if_cong [cong] power_Suc [simp del]
-  obtain N where N: "\<And>k. k\<ge>N \<Longrightarrow> norm (z k) < 1/2"
+  obtain N where "\<And>k. k\<ge>N \<Longrightarrow> norm (z k) < 1/2"
     using summable_LIMSEQ_zero [OF z]
     by (metis diff_zero dist_norm half_gt_zero_iff less_numeral_extra(1) lim_sequentially tendsto_norm_zero_iff)
-  have "norm (Ln (1 + z k)) \<le> 2 * norm (z k)" if "k \<ge> N" for k
-  proof (cases "z k = 0")
-    case False
-    let ?f = "\<lambda>i. cmod ((- 1) ^ i * z k ^ i / of_nat (Suc i))"
-    have normf: "norm (?f n) \<le> (1 / 2) ^ n" for n
-    proof -
-      have "norm (?f n) = cmod (z k) ^ n / cmod (1 + of_nat n)"
-        by (auto simp: norm_divide norm_mult norm_power)
-      also have "\<dots> \<le> cmod (z k) ^ n"
-        by (auto simp: field_split_simps mult_le_cancel_left1 in_Reals_norm)
-      also have "\<dots> \<le> (1 / 2) ^ n"
-        using N [OF that] by (simp add: power_mono)
-      finally show "norm (?f n) \<le> (1 / 2) ^ n" .
-    qed
-    have summablef: "summable ?f"
-      by (intro normf summable_comparison_test' [OF summable_geometric [of "1/2"]]) auto
-    have "(\<lambda>n. (- 1) ^ Suc n / of_nat n * z k ^ n) sums Ln (1 + z k)"
-      using Ln_series [of "z k"] N that by fastforce
-    then have *: "(\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))) sums Ln (1 + z k)"
-      using sums_split_initial_segment [where n= 1]  by (force simp: power_Suc mult_ac)
-    then have "norm (Ln (1 + z k)) = norm (suminf (\<lambda>i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))))"
-      using sums_unique by force
-    also have "\<dots> = norm (z k * suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))"
-      apply (subst suminf_mult)
-      using * False
-      by (auto simp: sums_summable intro: summable_mult_D [of "z k"])
-    also have "\<dots> = norm (z k) * norm (suminf (\<lambda>i. ((- 1) ^ i * z k ^ i) / (Suc i)))"
-      by (simp add: norm_mult)
-    also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. norm (((- 1) ^ i * z k ^ i) / (Suc i)))"
-      by (intro mult_left_mono summable_norm summablef) auto
-    also have "\<dots> \<le> norm (z k) * suminf (\<lambda>i. (1/2) ^ i)"
-      by (intro mult_left_mono suminf_le) (use summable_geometric [of "1/2"] summablef normf in auto)
-    also have "\<dots> \<le> norm (z k) * 2"
-      using suminf_geometric [of "1/2::real"] by simp
-    finally show ?thesis
-      by (simp add: mult_ac)
-  qed simp
   then have "summable (\<lambda>k. Ln (1 + z k))"
-    by (metis summable_comparison_test summable_mult z)
+    by (metis norm_Ln_le summable_comparison_test summable_mult z)
   with non0 show ?thesis
     by (simp add: add_eq_0_iff convergent_prod_iff_summable_complex)
 qed
 
+corollary summable_imp_convergent_prod_real:
+  fixes z :: "nat \<Rightarrow> real"
+  assumes z: "summable (\<lambda>k. \<bar>z k\<bar>)" and non0: "\<And>k. z k \<noteq> -1"
+  shows "convergent_prod (\<lambda>k. 1 + z k)" 
+proof -
+  have "\<And>k. (complex_of_real \<circ> z) k \<noteq> - 1"
+    by (metis non0 o_apply of_real_1 of_real_eq_iff of_real_minus)
+  with z 
+  have "convergent_prod (\<lambda>k. 1 + (complex_of_real \<circ> z) k)"
+    by (auto intro: summable_imp_convergent_prod_complex)
+  then show ?thesis 
+    using convergent_prod_of_real_iff [of "\<lambda>k. 1 + z k"] by (simp add: o_def)
+qed
+
 lemma summable_Ln_complex:
   fixes z :: "nat \<Rightarrow> complex"
   assumes "convergent_prod z" "\<And>k. z k \<noteq> 0"
diff -r 5364cdc3ec0e -r 6969d0ffc576 src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Tue Dec 20 22:24:36 2022 +0000
@@ -198,6 +198,19 @@
   unfolding uniformly_convergent_on_def assms(2) [symmetric]
   by (intro iff_exI uniform_limit_cong eventually_mono [OF assms(1)]) auto
 
+lemma uniformly_convergent_on_compose:
+  assumes "uniformly_convergent_on A f"
+  assumes "filterlim g sequentially sequentially"
+  shows   "uniformly_convergent_on A (\<lambda>n. f (g n))"
+proof -
+  from assms(1) obtain f' where "uniform_limit A f f' sequentially"
+    by (auto simp: uniformly_convergent_on_def)
+  hence "uniform_limit A (\<lambda>n. f (g n)) f' sequentially"
+    by (rule filterlim_compose) fact
+  thus ?thesis
+    by (auto simp: uniformly_convergent_on_def)
+qed    
+
 lemma uniformly_convergent_uniform_limit_iff:
   "uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
 proof
@@ -308,6 +321,46 @@
   ultimately show ?thesis by auto
 qed
 
+lemma uniformly_convergent_on_sum_E:
+  fixes \<epsilon>::real and f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_space,real_normed_vector}"
+  assumes uconv: "uniformly_convergent_on K (\<lambda>n z. \<Sum>k<n. f k z)" and "\<epsilon>>0"
+  obtains N where "\<And>m n z. \<lbrakk>N \<le> m; m \<le> n; z\<in>K\<rbrakk> \<Longrightarrow> norm(\<Sum>k=m..<n. f k z) < \<epsilon>"
+proof -
+  obtain N where N: "\<And>m n z. \<lbrakk>N \<le> m; N \<le> n; z\<in>K\<rbrakk> \<Longrightarrow> dist (\<Sum>k<m. f k z) (\<Sum>k<n. f k z) < \<epsilon>"
+    using uconv \<open>\<epsilon>>0\<close> unfolding uniformly_Cauchy_on_def uniformly_convergent_eq_Cauchy by meson
+  show thesis
+  proof
+    fix m n z
+    assume "N \<le> m" "m \<le> n" "z \<in> K"
+    moreover have "(\<Sum>k = m..<n. f k z) = (\<Sum>k<n. f k z) - (\<Sum>k<m. f k z)"
+      by (metis atLeast0LessThan le0 sum_diff_nat_ivl \<open>m \<le> n\<close>)
+    ultimately show "norm(\<Sum>k = m..<n. f k z) < \<epsilon>"
+      using N  by (simp add: dist_norm)
+  qed
+qed
+
+lemma uniformly_convergent_on_sum_iff:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_space,real_normed_vector}"
+  shows "uniformly_convergent_on K (\<lambda>n z. \<Sum>k<n. f k z) 
+     \<longleftrightarrow> (\<forall>\<epsilon>>0. \<exists>N. \<forall>m n z. N\<le>m \<longrightarrow> m\<le>n \<longrightarrow> z\<in>K \<longrightarrow> norm (\<Sum>k=m..<n. f k z) < \<epsilon>)" (is "?lhs=?rhs")
+proof
+  assume R: ?rhs
+  show ?lhs
+    unfolding uniformly_Cauchy_on_def uniformly_convergent_eq_Cauchy
+  proof (intro strip)
+    fix \<epsilon>::real
+    assume "\<epsilon>>0"
+    then obtain N where "\<And>m n z. \<lbrakk>N \<le> m; m \<le> n; z\<in>K\<rbrakk> \<Longrightarrow> norm(\<Sum>k = m..<n. f k z) < \<epsilon>"
+      using R by blast
+    then have "\<forall>x\<in>K. \<forall>m\<ge>N. \<forall>n\<ge>m. norm ((\<Sum>k<m. f k x) - (\<Sum>k<n. f k x)) < \<epsilon>"
+      by (metis atLeast0LessThan le0 sum_diff_nat_ivl norm_minus_commute)
+    then have "\<forall>x\<in>K. \<forall>m\<ge>N. \<forall>n\<ge>N. norm ((\<Sum>k<m. f k x) - (\<Sum>k<n. f k x)) < \<epsilon>"
+      by (metis linorder_le_cases norm_minus_commute)
+    then show "\<exists>M. \<forall>x\<in>K. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) < \<epsilon>"
+      by (metis dist_norm)
+  qed
+qed (metis uniformly_convergent_on_sum_E)
+
 text \<open>TODO: remove explicit formulations
   @{thm uniformly_convergent_eq_cauchy uniformly_cauchy_imp_uniformly_convergent}?!\<close>
 
@@ -316,6 +369,102 @@
   unfolding uniformly_convergent_on_def convergent_def
   by (auto dest: tendsto_uniform_limitI)
 
+subsection \<open>Comparison Test\<close>
+
+lemma uniformly_summable_comparison_test:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: banach"
+  assumes "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. g n x)"
+  assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> g n x"
+  shows   "uniformly_convergent_on A (\<lambda>N x. \<Sum>n<N. f n x)"
+proof -
+  have "uniformly_Cauchy_on A (\<lambda>N x. \<Sum>n<N. f n x)"
+  proof (rule uniformly_Cauchy_onI')
+    fix e :: real assume e: "e > 0"
+    obtain M where M: "\<And>x m n. x \<in> A \<Longrightarrow> m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (\<Sum>k<m. g k x) (\<Sum>k<n. g k x) < e"
+      using assms(1) e unfolding uniformly_convergent_eq_Cauchy uniformly_Cauchy_on_def by metis
+    show "\<exists>M. \<forall>x\<in>A. \<forall>m\<ge>M. \<forall>n>m. dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) < e"
+    proof (rule exI[of _ M], safe)
+      fix x m n assume xmn: "x \<in> A" "m \<ge> M" "m < n"
+      have nonneg: "g k x \<ge> 0" for k
+        by (rule order.trans[OF _ assms(2)]) (use xmn in auto)
+      have "dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) = norm (\<Sum>k\<in>{..<n}-{..<m}. f k x)"
+        using xmn by (subst sum_diff) (auto simp: dist_norm norm_minus_commute)
+      also have "{..<n}-{..<m} = {m..<n}"
+        by auto
+      also have "norm (\<Sum>k\<in>{m..<n}. f k x) \<le> (\<Sum>k\<in>{m..<n}. norm (f k x))"
+        using norm_sum by blast
+      also have "\<dots> \<le> (\<Sum>k\<in>{m..<n}. g k x)"
+        by (intro sum_mono assms xmn)
+      also have "\<dots> = \<bar>\<Sum>k\<in>{m..<n}. g k x\<bar>"
+        by (subst abs_of_nonneg) (auto simp: nonneg intro!: sum_nonneg)
+      also have "{m..<n} = {..<n} - {..<m}"
+        by auto
+      also have "\<bar>\<Sum>k\<in>\<dots>. g k x\<bar> = dist (\<Sum>k<m. g k x) (\<Sum>k<n. g k x)"
+        using xmn by (subst sum_diff) (auto simp: abs_minus_commute dist_norm)
+      also have "\<dots> < e"
+        by (rule M) (use xmn in auto)
+      finally show "dist (\<Sum>k<m. f k x) (\<Sum>k<n. f k x) < e" .
+    qed
+  qed
+  thus ?thesis
+    unfolding uniformly_convergent_eq_Cauchy .
+qed
+
+lemma uniform_limit_compose_uniformly_continuous_on:
+  fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
+  assumes lim: "uniform_limit A g g' F"
+  assumes cont: "uniformly_continuous_on B f"
+  assumes ev: "eventually (\<lambda>x. \<forall>y\<in>A. g x y \<in> B) F" and "closed B"
+  shows   "uniform_limit A (\<lambda>x y. f (g x y)) (\<lambda>y. f (g' y)) F"
+proof (cases "F = bot")
+  case [simp]: False
+  show ?thesis
+    unfolding uniform_limit_iff
+  proof safe
+    fix e :: real assume e: "e > 0"
+
+    have g'_in_B: "g' y \<in> B" if "y \<in> A" for y
+    proof (rule Lim_in_closed_set)
+      show "eventually (\<lambda>x. g x y \<in> B) F"
+        using ev by eventually_elim (use that in auto)
+      show "((\<lambda>x. g x y) \<longlongrightarrow> g' y) F"
+        using lim that by (metis tendsto_uniform_limitI)
+    qed (use \<open>closed B\<close> in auto)
+  
+    obtain d where d: "d > 0" "\<And>x y. x \<in> B \<Longrightarrow> y \<in> B \<Longrightarrow> dist x y < d \<Longrightarrow> dist (f x) (f y) < e"
+      using e cont unfolding uniformly_continuous_on_def by metis
+    from lim have "eventually (\<lambda>x. \<forall>y\<in>A. dist (g x y) (g' y) < d) F"
+      unfolding uniform_limit_iff using \<open>d > 0\<close>  by meson
+    thus "eventually (\<lambda>x. \<forall>y\<in>A. dist (f (g x y)) (f (g' y)) < e) F"
+      using assms(3)
+    proof eventually_elim
+      case (elim x)
+      show "\<forall>y\<in>A. dist (f (g x y)) (f (g' y)) < e"
+      proof safe
+        fix y assume y: "y \<in> A"
+        show "dist (f (g x y)) (f (g' y)) < e"
+        proof (rule d)
+          show "dist (g x y) (g' y) < d"
+            using elim y by blast
+        qed (use y elim g'_in_B in auto)
+      qed
+    qed
+  qed
+qed (auto simp: filterlim_def)
+
+lemma uniformly_convergent_on_compose_uniformly_continuous_on:
+  fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
+  assumes lim: "uniformly_convergent_on A g"
+  assumes cont: "uniformly_continuous_on B f"
+  assumes ev: "eventually (\<lambda>x. \<forall>y\<in>A. g x y \<in> B) sequentially" and "closed B"
+  shows   "uniformly_convergent_on A (\<lambda>x y. f (g x y))"
+proof -
+  from lim obtain g' where g': "uniform_limit A g g' sequentially"
+    by (auto simp: uniformly_convergent_on_def)
+  thus ?thesis
+    using uniform_limit_compose_uniformly_continuous_on[OF g' cont ev \<open>closed B\<close>]
+    by (auto simp: uniformly_convergent_on_def)
+qed
 
 subsection \<open>Weierstrass M-Test\<close>
 
diff -r 5364cdc3ec0e -r 6969d0ffc576 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Complex.thy	Tue Dec 20 22:24:36 2022 +0000
@@ -6,7 +6,7 @@
 section \<open>Complex Numbers: Rectangular and Polar Representations\<close>
 
 theory Complex
-imports Transcendental
+imports Transcendental Real_Vector_Spaces
 begin
 
 text \<open>
@@ -196,6 +196,12 @@
 lemma Im_divide_of_nat [simp]: "Im (z / of_nat n) = Im z / of_nat n"
   by (cases n) (simp_all add: Im_divide field_split_simps power2_eq_square del: of_nat_Suc)
 
+lemma Re_inverse [simp]: "r \<in> \<real> \<Longrightarrow> Re (inverse r) = inverse (Re r)"
+  by (metis Re_complex_of_real Reals_cases of_real_inverse)
+
+lemma Im_inverse [simp]: "r \<in> \<real> \<Longrightarrow> Im (inverse r) = 0"
+  by (metis Im_complex_of_real Reals_cases of_real_inverse)
+
 lemma of_real_Re [simp]: "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
   by (auto simp: Reals_def)
 
diff -r 5364cdc3ec0e -r 6969d0ffc576 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Filter.thy	Tue Dec 20 22:24:36 2022 +0000
@@ -1519,6 +1519,24 @@
     by eventually_elim (insert n, auto)
 qed
 
+lemma filterlim_minus_const_nat_at_top:
+  "filterlim (\<lambda>n. n - c) sequentially sequentially"
+  unfolding filterlim_at_top
+proof
+  fix a :: nat
+  show "eventually (\<lambda>n. n - c \<ge> a) at_top"
+    using eventually_ge_at_top[of "a + c"] by eventually_elim auto
+qed
+
+lemma filterlim_add_const_nat_at_top:
+  "filterlim (\<lambda>n. n + c) sequentially sequentially"
+  unfolding filterlim_at_top
+proof
+  fix a :: nat
+  show "eventually (\<lambda>n. n + c \<ge> a) at_top"
+    using eventually_ge_at_top[of a] by eventually_elim auto
+qed
+
 subsection \<open>Setup \<^typ>\<open>'a filter\<close> for lifting and transfer\<close>
 
 lemma filtermap_id [simp, id_simps]: "filtermap id = id"
diff -r 5364cdc3ec0e -r 6969d0ffc576 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Dec 20 19:43:55 2022 +0100
+++ b/src/HOL/Fun.thy	Tue Dec 20 22:24:36 2022 +0000
@@ -300,11 +300,17 @@
     using lin [of x y] ne by (force simp: dual_order.order_iff_strict)
 qed
 
+lemma linorder_inj_onI':
+  fixes A :: "'a :: linorder set"
+  assumes "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i < j \<Longrightarrow> f i \<noteq> f j"
+  shows   "inj_on f A"
+  by (intro linorder_inj_onI) (auto simp add: assms)
+
 lemma linorder_injI:
   assumes "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
   shows "inj f"
     \<comment> \<open>Courtesy of Stephan Merz\<close>
-using assms by (auto intro: linorder_inj_onI linear)
+using assms by (simp add: linorder_inj_onI')
 
 lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
   unfolding Pow_def inj_on_def by blast