# HG changeset patch
# User desharna
# Date 1710963936 -3600
# Node ID b5cb8d56339f958e1f129e3705d84050329a31ad
# Parent  7793e3161d2bec551b2513a2a0f0e48a51c06ef3# Parent  eb753708e85b9c786d1330cdf1bd1fb69db3b94d
merged

diff -r 7793e3161d2b -r b5cb8d56339f CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Mar 20 12:26:52 2024 +0100
+++ b/CONTRIBUTORS	Wed Mar 20 20:45:36 2024 +0100
@@ -6,6 +6,12 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* March 2024: Manuel Eberl
+  Weierstraß Factorization Theorem in HOL-Complex_Analysis
+
+* March 2024: Anthony Bordg, Manuel Eberl, Wenda Li, Larry Paulson
+  New and more general definition of meromorphicity in HOL-Complex_Analysis
+
 * 2023/2024: Makarius Wenzel and Fabian Huch
   More robust and scalable support for distributed build clusters.
 
diff -r 7793e3161d2b -r b5cb8d56339f NEWS
--- a/NEWS	Wed Mar 20 12:26:52 2024 +0100
+++ b/NEWS	Wed Mar 20 20:45:36 2024 +0100
@@ -137,6 +137,8 @@
 * HOL-Analysis: corrected the definition of convex function (convex_on)
 to require the underlying set to be convex. INCOMPATIBILITY.
 
+* HOL-Complex_Analysis: new, more general definition of meromorphicity.
+INCOMPATIBILITY.
 
 *** Pure ***
 
diff -r 7793e3161d2b -r b5cb8d56339f src/HOL/Complex_Analysis/Complex_Analysis.thy
--- a/src/HOL/Complex_Analysis/Complex_Analysis.thy	Wed Mar 20 12:26:52 2024 +0100
+++ b/src/HOL/Complex_Analysis/Complex_Analysis.thy	Wed Mar 20 20:45:36 2024 +0100
@@ -2,7 +2,7 @@
   imports
   Riemann_Mapping
   Residue_Theorem
-  Meromorphic
+  Weierstrass_Factorization
 begin
 
 end
diff -r 7793e3161d2b -r b5cb8d56339f src/HOL/Complex_Analysis/Meromorphic.thy
--- a/src/HOL/Complex_Analysis/Meromorphic.thy	Wed Mar 20 12:26:52 2024 +0100
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy	Wed Mar 20 20:45:36 2024 +0100
@@ -1,5 +1,6 @@
 theory Meromorphic imports
-  "Laurent_Convergence"
+  Laurent_Convergence
+  Cauchy_Integral_Formula
   "HOL-Analysis.Sparse_In"
 begin
 
@@ -616,6 +617,10 @@
     where "f nicely_meromorphic_on A \<longleftrightarrow> f meromorphic_on A 
         \<and> (\<forall>z\<in>A. (is_pole f z \<and> f z=0) \<or> f \<midarrow>z\<rightarrow> f z)"
 
+lemma nicely_meromorphic_on_subset:
+  "f nicely_meromorphic_on A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> f nicely_meromorphic_on B"
+  using meromorphic_on_subset unfolding nicely_meromorphic_on_def by blast
+
 lemma constant_on_imp_nicely_meromorphic_on:
   assumes "f constant_on A" "open A"
   shows "f nicely_meromorphic_on A"
diff -r 7793e3161d2b -r b5cb8d56339f src/HOL/Complex_Analysis/Weierstrass_Factorization.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Complex_Analysis/Weierstrass_Factorization.thy	Wed Mar 20 20:45:36 2024 +0100
@@ -0,0 +1,1595 @@
+section \<open>The Weierstra\ss\ Factorisation Theorem\<close>
+theory Weierstrass_Factorization
+  imports Meromorphic
+begin 
+                
+subsection \<open>The elementary factors\<close>
+
+text \<open>
+  The Weierstra\ss\ elementary factors are the family of entire functions
+  \[E_n(z) = (1-z) \exp\bigg(z + \frac{z^2}{2} + \ldots + \frac{z^n}{n}\bigg)\]
+  with the key properties that they have a single zero at $z = 1$ and 
+  satisfy $E_n(z) = 1 + O(z^{n+1})$ around the origin.
+\<close>
+definition weierstrass_factor :: "nat \<Rightarrow> complex \<Rightarrow> complex" where
+  "weierstrass_factor n z = (1 - z) * exp (\<Sum>k=1..n. z ^ k / of_nat k)"
+
+lemma weierstrass_factor_continuous_on [continuous_intros]:
+  "continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>z. weierstrass_factor n (f z))"
+  by (auto simp: weierstrass_factor_def intro!: continuous_intros)
+
+lemma weierstrass_factor_holomorphic [holomorphic_intros]:
+  "f holomorphic_on A \<Longrightarrow> (\<lambda>z. weierstrass_factor n (f z)) holomorphic_on A"
+  by (auto simp: weierstrass_factor_def intro!: holomorphic_intros)
+
+lemma weierstrass_factor_analytic [analytic_intros]:
+  "f analytic_on A \<Longrightarrow> (\<lambda>z. weierstrass_factor n (f z)) analytic_on A"
+  by (auto simp: weierstrass_factor_def intro!: analytic_intros)
+
+lemma weierstrass_factor_0 [simp]: "weierstrass_factor n 0 = 1"
+  by (auto simp: weierstrass_factor_def power_0_left)
+
+lemma weierstrass_factor_1 [simp]: "weierstrass_factor n 1 = 0"
+  by (simp add: weierstrass_factor_def)
+
+lemma weierstrass_factor_eq_0_iff [simp]: "weierstrass_factor n z = 0 \<longleftrightarrow> z = 1"
+  by (simp add: weierstrass_factor_def)
+
+lemma zorder_weierstrass_factor [simp]: "zorder (weierstrass_factor n) 1 = 1"
+proof (rule zorder_eqI)
+  show "(\<lambda>z. -exp (\<Sum>k=1..n. z ^ k / of_nat k)) holomorphic_on UNIV"
+    by (intro holomorphic_intros) auto
+qed (auto simp: weierstrass_factor_def algebra_simps)  
+
+lemma
+  fixes z :: "'a :: {banach, real_normed_field}"
+  assumes "norm z \<le> 1 / 2"
+  shows   norm_exp_bounds_lemma: "norm (exp z - 1 - z) \<le> norm z / 2"
+    and   norm_exp_bounds: "norm (exp z - 1) \<ge> 1 / 2 * norm z"
+                           "norm (exp z - 1) \<le> 3 / 2 * norm z"
+proof -
+  show *: "norm (exp z - 1 - z) \<le> norm z / 2"
+  proof (cases "z = 0")
+    case False
+    have sums: "(\<lambda>k. z ^ (k + 2) /\<^sub>R fact (k + 2)) sums (exp z - (\<Sum>k<2. z ^ k /\<^sub>R fact k))"
+      by (intro sums_split_initial_segment exp_converges)
+  
+    have "summable (\<lambda>k. norm z ^ (k + 2) /\<^sub>R fact (k + 2))"
+      using summable_norm_exp[of z]
+      by (intro summable_norm summable_ignore_initial_segment)
+         (auto simp: norm_power norm_divide divide_simps)
+    also have "?this \<longleftrightarrow> summable (\<lambda>k. norm z ^ 2 * (norm z ^ k / fact (k +2)))"
+      by (simp add: power_add mult_ac divide_simps power2_eq_square del: of_nat_Suc of_nat_add)
+    also have "\<dots> \<longleftrightarrow> summable (\<lambda>k. norm z ^ k / fact (k + 2))"
+      by (subst summable_cmult_iff) (use \<open>z \<noteq> 0\<close> in auto)
+    finally have summable: "summable (\<lambda>k. norm z ^ k / fact (k + 2))" .
+  
+    have "exp z - 1 - z = (\<Sum>k. z ^ (k + 2) / fact (k + 2))"
+      using sums by (simp add: sums_iff scaleR_conv_of_real divide_simps eval_nat_numeral)
+    also have "norm \<dots> \<le> (\<Sum>k. norm (z ^ (k + 2) / fact (k + 2)))"
+      using summable_norm_exp[of z]
+      by (intro summable_norm summable_ignore_initial_segment)
+         (auto simp: norm_power norm_divide divide_simps)
+    also have "\<dots> = (\<Sum>k. norm z ^ 2 * (norm z ^ k / fact (k + 2)))"
+      by (simp add: power_add norm_power norm_divide mult_ac norm_mult power2_eq_square del: of_nat_Suc)
+    also have "\<dots> = norm z ^ 2 * (\<Sum>k. norm z ^ k / fact (k + 2))"
+      using summable by (rule suminf_mult)
+    also have "\<dots> \<le> norm z ^ 2 * (1 / (1 - norm z) / 2)"
+    proof (intro mult_left_mono, rule sums_le)
+      show "(\<lambda>k. norm z ^ k / fact (k + 2)) sums (\<Sum>k. norm z ^ k / fact (k + 2))"
+        using summable by blast
+      show "(\<lambda>k. norm z ^ k / 2) sums (1 / (1 - norm z) / 2)"
+        using assms by (intro geometric_sums sums_divide) auto
+    next
+      fix k :: nat
+      have "norm z ^ k / fact (k + 2) \<le> norm z ^ k / fact 2"
+        by (intro divide_left_mono fact_mono) auto
+      thus "norm z ^ k / fact (k + 2) \<le> norm z ^ k / 2"
+        by simp
+    qed (auto simp: divide_simps)
+    also have "\<dots> = norm z * (norm z / (1 - norm z)) / 2"
+      by (simp add: power2_eq_square)
+    also have "\<dots> \<le> norm z * ((1 / 2) / (1 - (1 / 2))) / 2"
+      using assms by (intro mult_mono frac_le diff_mono) auto
+    also have "\<dots> = norm z / 2"
+      by simp
+    finally show "norm (exp z - 1 - z) \<le> norm z / 2" .
+  qed auto
+
+  have "norm (exp z - 1) \<le> norm z + norm (exp z - 1 - z)"
+    by (rule norm_triangle_sub)
+  with * show "norm (exp z - 1) \<le> 3 / 2 * norm z"
+    by simp
+
+  have "norm z - norm (exp z - 1 - z) \<le> norm (exp z - 1)"
+    using norm_triangle_ineq3[of "exp z - 1 - z" "-z"] by simp
+  with * show "norm (exp z - 1) \<ge> 1 / 2 * norm z"
+    by simp
+qed 
+
+lemma weierstrass_factor_bound:
+  assumes "norm z \<le> 1 / 2"
+  shows   "norm (weierstrass_factor n z - 1) \<le> 3 * norm z ^ Suc n"
+proof (cases "n = 0 \<or> z = 0")
+  case True
+  thus ?thesis
+  proof
+    assume "n = 0"
+    thus ?thesis by (auto simp: weierstrass_factor_def)
+  qed auto
+next
+  case False
+  with assms have "z \<noteq> 1" "n > 0" "z \<noteq> 0"
+    by auto
+
+  have "summable (\<lambda>k. cmod z ^ (k + Suc n) / real (k + Suc n))"
+    using ln_series'[of "-norm z"] assms
+    by (intro summable_norm summable_ignore_initial_segment)
+       (simp_all add: sums_iff summable_minus_iff power_minus' norm_divide norm_power)
+  also have "?this \<longleftrightarrow> summable (\<lambda>k. norm z ^ Suc n * (norm z ^ k / real (k + Suc n)))"
+    by (simp add: power_add mult_ac)
+  also have "\<dots> \<longleftrightarrow> summable (\<lambda>k. norm z ^ k / real (k + Suc n))"
+    by (subst summable_cmult_iff) (use \<open>z \<noteq> 0\<close> in auto)
+  finally have summable: "summable (\<lambda>k. norm z ^ k / real (k + Suc n))" .
+
+  have "(\<lambda>k. z ^ k / of_nat k) sums - Ln (1 - z)"
+    using sums_minus[OF Ln_series[of "-z"]] assms by (simp add: power_minus')
+  hence "(\<lambda>k. z ^ (k + Suc n) / of_nat (k + Suc n)) sums (- Ln (1 - z) - (\<Sum>k<Suc n. z ^ k / of_nat k))"
+    by (intro sums_split_initial_segment)
+  also have "(\<Sum>k<Suc n. z ^ k / of_nat k) = (\<Sum>k=1..n. z ^ k / of_nat k)"
+    by (intro sum.mono_neutral_right) auto
+  finally have "norm (ln (1 - z) + (\<Sum>k=1..n. z ^ k / of_nat k)) =
+                norm (\<Sum>k. z ^ (k + Suc n) / of_nat (k + Suc n))"
+    by (simp add: sums_iff norm_uminus_minus)
+
+  also have "\<dots> \<le> (\<Sum>k. norm (z ^ (k + Suc n) / of_nat (k + Suc n)))"
+    using ln_series'[of "-norm z"] assms
+    by (intro summable_norm summable_ignore_initial_segment)
+       (simp_all add: sums_iff summable_minus_iff power_minus' norm_divide norm_power)
+  also have "\<dots> = (\<Sum>k. norm z ^ Suc n * (norm z ^ k / real (k + Suc n)))"
+    by (simp add: algebra_simps norm_mult norm_power norm_divide power_add del: of_nat_add of_nat_Suc)
+  also have "\<dots> = norm z ^ Suc n * (\<Sum>k. norm z ^ k / real (k + Suc n))"
+    by (intro suminf_mult summable)
+  also have "\<dots> \<le> norm z ^ Suc n * (1 / (1 - norm z))"
+  proof (intro mult_left_mono[OF sums_le])
+    show "(\<lambda>k. norm z ^ k / real (k + Suc n)) sums (\<Sum>k. norm z ^ k / real (k + Suc n))"
+      using summable by blast
+    show "(\<lambda>k. norm z ^ k) sums (1 / (1 - norm z))"
+      by (rule geometric_sums) (use assms in auto)
+  qed (auto simp: field_simps)
+  also have "norm z ^ Suc n * (1 / (1 - norm z)) \<le> norm z ^ Suc n * (1 / (1 - (1 / 2)))"
+    using assms by (intro mult_mono power_mono divide_left_mono diff_mono mult_pos_pos) auto
+  also have "\<dots> = 2 * norm z ^ Suc n"
+    by simp
+  finally have norm_le: "norm (ln (1 - z) + (\<Sum>k=1..n. z ^ k / of_nat k)) \<le> 2 * norm z ^ Suc n" .
+
+  also have "\<dots> \<le> 2 * norm z ^ 2"
+    using \<open>n > 0\<close> assms by (intro mult_left_mono power_decreasing) auto
+  also have "\<dots> \<le> 2 * (1 / 2) ^ 2"
+    by (intro mult_left_mono assms power_mono) auto
+  finally have norm_le': "norm (ln (1 - z) + (\<Sum>k=1..n. z ^ k / of_nat k)) \<le> 1 / 2"
+    by (simp add: power2_eq_square)
+
+  have "weierstrass_factor n z = exp (ln (1 - z) + (\<Sum>k=1..n. z ^ k / of_nat k))"
+    using \<open>z \<noteq> 1\<close> by (simp add: exp_add weierstrass_factor_def)
+  also have "norm (\<dots> - 1) \<le> (3 / 2) * norm (ln (1 - z) + (\<Sum>k=1..n. z ^ k / of_nat k))"
+    by (intro norm_exp_bounds norm_le')
+  also have "\<dots> \<le> (3 / 2) * (2 * norm z ^ Suc n)"
+    by (intro mult_left_mono norm_le) auto
+  finally show ?thesis
+    by simp
+qed
+
+
+subsection \<open>Infinite products of elementary factors\<close>
+
+text \<open>
+  We now show that the elementary factors can be used to construct an entire function
+  with its zeros at a certain set of points (given by a sequence of non-zero numbers $a_n$ with no
+  accumulation point).
+\<close>
+
+locale weierstrass_product =
+  fixes a :: "nat \<Rightarrow> complex"
+  fixes p :: "nat \<Rightarrow> nat"
+  assumes a_nonzero: "\<And>n. a n \<noteq> 0"
+  assumes filterlim_a: "filterlim a at_infinity at_top"
+  assumes summable_a_p: "\<And>r. r > 0 \<Longrightarrow> summable (\<lambda>n. (r / norm (a n)) ^ Suc (p n))"
+begin
+
+definition f :: "complex \<Rightarrow> complex" where
+  "f z = (\<Prod>n. weierstrass_factor (p n) (z / a n))"
+
+lemma abs_convergent: "abs_convergent_prod (\<lambda>n. weierstrass_factor (p n) (z / a n))"
+  unfolding abs_convergent_prod_conv_summable
+proof (rule summable_comparison_test_ev)
+  have "eventually (\<lambda>n. norm (a n) > 2 * norm z) at_top"
+    using filterlim_a by (metis filterlim_at_infinity_imp_norm_at_top filterlim_at_top_dense)
+  thus "eventually (\<lambda>n. norm (norm (weierstrass_factor (p n) (z / a n) - 1)) \<le>
+          3 * norm (z / a n) ^ Suc (p n)) at_top"
+  proof eventually_elim
+    case (elim n)
+    hence "norm (z / a n) \<le> 1 / 2"
+      by (auto simp: norm_divide divide_simps)
+    thus ?case using weierstrass_factor_bound[of "z / a n" "p n"]
+      by simp
+  qed
+next
+  show "summable (\<lambda>n. 3 * norm (z / a n) ^ Suc (p n))"
+    using summable_mult[OF summable_a_p[of "norm z"], of 3]
+    by (cases "z = 0") (auto simp: norm_divide)
+qed
+
+lemma convergent: "convergent_prod (\<lambda>n. weierstrass_factor (p n) (z / a n))"
+  using abs_convergent[of z] abs_convergent_prod_imp_convergent_prod by blast
+
+lemma has_prod: "(\<lambda>n. weierstrass_factor (p n) (z / a n)) has_prod f z"
+  using convergent[of z] unfolding f_def by auto
+
+lemma finite_occs_a: "finite (a -` {z})"
+proof -
+  have "eventually (\<lambda>n. norm (a n) > norm z) at_top"
+    using filterlim_a by (metis filterlim_at_infinity_imp_norm_at_top filterlim_at_top_dense)
+  then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (a n) > norm z"
+    by (auto simp: eventually_at_top_linorder)
+  have "n < N" if "n \<in> a -` {z}" for n
+    using N[of n] that by (cases "n < N") auto
+  hence "a -` {z} \<subseteq> {..<N}" "finite {..<N}"
+    by auto
+  thus ?thesis
+    using finite_subset by blast
+qed
+
+context
+  fixes P
+  defines "P \<equiv> (\<lambda>N z. \<Prod>n<N. weierstrass_factor (p n) (z / a n))"
+begin 
+
+lemma uniformly_convergent:
+  assumes "R > 0"
+  shows   "uniformly_convergent_on (cball 0 R) P"
+  unfolding P_def
+proof (rule uniformly_convergent_on_prod')
+  show "uniformly_convergent_on (cball 0 R) (\<lambda>N z. \<Sum>n<N. norm (weierstrass_factor (p n) (z / a n) - 1))"
+  proof (rule Weierstrass_m_test'_ev)
+    have "eventually (\<lambda>n. norm (a n) \<ge> 2 * R) sequentially"
+      using filterlim_a by (metis filterlim_at_infinity_imp_norm_at_top filterlim_at_top)
+    thus "\<forall>\<^sub>F n in sequentially. \<forall>z\<in>cball 0 R. norm (norm (weierstrass_factor (p n) (z / a n) - 1)) \<le>
+            3 * (R / norm (a n)) ^ Suc (p n)"
+    proof eventually_elim
+      case (elim n)
+      show ?case
+      proof safe
+        fix z :: complex assume z: "z \<in> cball 0 R"
+        have "2 * norm z \<le> 2 * R"
+          using z by auto
+        also have "\<dots> \<le> norm (a n)"
+          using elim by simp
+        finally have "norm (a n) \<ge> 2 * norm z" .
+        hence "norm (weierstrass_factor (p n) (z / a n) - 1) \<le> 3 * norm (z / a n) ^ Suc (p n)"
+          by (intro weierstrass_factor_bound) (auto simp: norm_divide divide_simps)
+        also have "\<dots> = 3 * (norm z / norm (a n)) ^ Suc (p n)"
+          by (simp add: norm_divide)
+        also have "\<dots> \<le> 3 * (R / norm (a n)) ^ Suc (p n)"
+          by (intro mult_left_mono power_mono divide_right_mono) (use z in auto)
+        finally show "norm (norm (weierstrass_factor (p n) (z / a n) - 1)) \<le>
+                        3 * (R / norm (a n)) ^ Suc (p n)" by simp
+      qed
+    qed
+  next
+    show "summable (\<lambda>n. 3 * (R / norm (a n)) ^ Suc (p n))"
+      by (intro summable_mult summable_a_p assms)
+  qed
+qed (auto intro!: continuous_intros simp: a_nonzero)
+
+lemma uniform_limit:
+  assumes "R > 0"
+  shows   "uniform_limit (cball 0 R) P f at_top"
+proof -
+  obtain g where g: "uniform_limit (cball 0 R) P g at_top"
+    using uniformly_convergent[OF assms] by (auto simp: uniformly_convergent_on_def)
+  also have "?this \<longleftrightarrow> uniform_limit (cball 0 R) P f at_top"
+  proof (intro uniform_limit_cong)
+    fix z :: complex assume "z \<in> cball 0 R"
+    with g have "(\<lambda>n. P (Suc n) z) \<longlonglongrightarrow> g z"
+      by (metis tendsto_uniform_limitI filterlim_sequentially_Suc)
+    moreover have "(\<lambda>n. P (Suc n) z) \<longlonglongrightarrow> f z"
+      using convergent_prod_LIMSEQ[OF convergent[of z]] unfolding P_def lessThan_Suc_atMost
+      by (simp add: f_def)
+    ultimately show "g z = f z"
+      using tendsto_unique by force
+  qed auto
+  finally show ?thesis .
+qed
+
+lemma holomorphic [holomorphic_intros]: "f holomorphic_on A"
+proof (rule holomorphic_on_subset)
+  show "f holomorphic_on UNIV"
+  proof (rule holomorphic_uniform_sequence)
+    fix z :: complex
+    have *: "uniform_limit (cball 0 (norm z + 1)) P f sequentially"
+      by (rule uniform_limit) (auto intro: add_nonneg_pos)
+    hence "uniform_limit (cball z 1) P f sequentially"
+      by (rule uniform_limit_on_subset) (simp add: cball_subset_cball_iff)
+    thus "\<exists>d>0. cball z d \<subseteq> UNIV \<and> uniform_limit (cball z d) P f sequentially"
+      by (intro exI[of _ 1]) auto
+  qed (auto intro!: holomorphic_intros simp: P_def)
+qed auto
+
+lemma analytic [analytic_intros]: "f analytic_on A"
+  using holomorphic[of UNIV] analytic_on_holomorphic by blast
+
+end
+
+
+lemma zero: "f z = 0 \<longleftrightarrow> z \<in> range a"
+  using has_prod_eq_0_iff[OF has_prod, of z] by (auto simp: a_nonzero)  
+
+lemma not_islimpt_range_a: "\<not>z islimpt (range a)"
+proof
+  assume "z islimpt (range a)"
+  then obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "(a \<circ> r) \<longlonglongrightarrow> z"
+    using islimpt_range_imp_convergent_subsequence by metis
+  moreover have "filterlim (a \<circ> r) at_infinity sequentially"
+    unfolding o_def by (rule filterlim_compose[OF filterlim_a filterlim_subseq[OF r(1)]])
+  ultimately show False
+    by (meson not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially)
+qed
+
+lemma isolated_zero:
+  assumes "z \<in> range a"
+  shows   "isolated_zero f z"
+  using not_islimpt_range_a[of z] assms
+    by (auto simp: isolated_zero_altdef zero)
+
+lemma zorder: "zorder f z = card (a -` {z})"
+proof -
+  obtain N where N: "a -` {z} \<subseteq> {..N}"
+    using finite_occs_a[of z] by (meson finite_nat_iff_bounded_le)
+  define g where "g = (\<lambda>z n. weierstrass_factor (p n) (z / a n))"
+  define h1 where "h1 = (\<lambda>w. (\<Prod>n\<in>{..N} - a-`{z}. g w n) * (\<Prod>n. g w (n + Suc N)))"
+  define h2 where "h2 = (\<lambda>w. (\<Prod>n\<in>{..N} \<inter> a-`{z}. g w n))"
+
+  have has_prod_h1': "(\<lambda>n. g w (n + Suc N)) has_prod (\<Prod>n. g w (n + Suc N))" for w
+    unfolding g_def
+    by (intro convergent_prod_has_prod convergent_prod_ignore_initial_segment convergent)
+
+  have f_eq: "f w = h1 w * h2 w" for w
+  proof -
+    have "f w = (\<Prod>n<Suc N. g w n) * (\<Prod>n. g w (n + Suc N))"
+    proof (rule has_prod_unique2)
+      show "(\<lambda>n. g w n) has_prod ((\<Prod>n<Suc N. g w n) * (\<Prod>n. g w (n + Suc N)))"
+        unfolding g_def by (intro has_prod_ignore_initial_segment' convergent)
+      show "g w has_prod f w"
+        unfolding g_def by (rule has_prod)
+    qed 
+    also have "{..<Suc N} = ({..N} - a-`{z}) \<union> ({..N} \<inter> a-`{z})"
+      by auto
+    also have "(\<Prod>k\<in>\<dots>. g w k) = (\<Prod>k\<in>{..N} - a-`{z}. g w k) * (\<Prod>k\<in>{..N} \<inter> a-`{z}. g w k)"
+      by (intro prod.union_disjoint) auto
+    finally show ?thesis
+      by (simp add: h1_def h2_def mult_ac)
+  qed    
+
+  have ana_h1: "h1 analytic_on {z}"
+  proof -
+    interpret h1: weierstrass_product "\<lambda>n. a (n + Suc N)" "\<lambda>n. p (n + Suc N)"
+    proof
+      have "filterlim (\<lambda>n. n + Suc N) at_top at_top"
+        by (rule filterlim_add_const_nat_at_top)
+      thus "filterlim (\<lambda>n. a (n + Suc N)) at_infinity at_top"
+        by (intro filterlim_compose[OF filterlim_a])
+      show "summable (\<lambda>n. (r / cmod (a (n + Suc N))) ^ Suc (p (n + Suc N)))" if "r > 0" for r
+        by (intro summable_ignore_initial_segment summable_a_p that)
+    qed (auto simp: a_nonzero)
+
+    show ?thesis using h1.analytic
+      unfolding h1_def g_def h1.f_def by (intro analytic_intros) (auto simp: a_nonzero)
+  qed
+
+  have ana_h2: "h2 analytic_on {z}"
+    unfolding h2_def g_def by (intro analytic_intros) (auto simp: a_nonzero)
+
+  have "zorder f z = zorder (\<lambda>w. h1 w * h2 w) z"
+    by (simp add: f_eq [abs_def])
+  also have "\<dots> = zorder h1 z + zorder h2 z"
+  proof (rule zorder_times_analytic)
+    have "eventually (\<lambda>w. f w \<noteq> 0) (at z)"
+      using not_islimpt_range_a[of z] by (auto simp: islimpt_conv_frequently_at frequently_def zero)
+    thus "eventually (\<lambda>w. h1 w * h2 w \<noteq> 0) (at z)"
+      by (simp add: f_eq)
+  qed fact+
+  also have "zorder h2 z = (\<Sum>n\<in>{..N} \<inter> a -` {z}. zorder (\<lambda>w. g w n) z)"
+    unfolding h2_def
+    by (intro zorder_prod_analytic)
+       (auto simp: a_nonzero g_def eventually_at_filter intro!: analytic_intros)
+  also have "h1 z \<noteq> 0" using N has_prod_eq_0_iff[OF has_prod_h1'[of z]]
+    by (auto simp: h1_def g_def)
+  hence "zorder h1 z = 0"
+    by (intro zorder_eq_0I ana_h1)
+  also have "(\<Sum>n\<in>{..N} \<inter> a -` {z}. zorder (\<lambda>w. g w n) z) = (\<Sum>n\<in>{..N} \<inter> a -` {z}. 1)"
+  proof (intro sum.cong refl)
+    fix n :: nat
+    assume n: "n \<in> {..N} \<inter> a -` {z}"
+    have "zorder (\<lambda>w. weierstrass_factor (p n) (1 / a n * w)) z =
+          zorder (weierstrass_factor (p n)) (1 / a n * z)"
+      using a_nonzero[of n] eventually_neq_at_within[of 1 "z / a n" UNIV]
+      by (intro zorder_scale analytic_intros) auto
+    hence "zorder (\<lambda>w. g w n) z = zorder (weierstrass_factor (p n)) 1"
+      using n a_nonzero[of n] by (auto simp: g_def)
+    thus "zorder (\<lambda>w. g w n) z = 1"
+      by simp
+  qed
+  also have "\<dots> = card ({..N} \<inter> a -` {z})"
+    by simp
+  also have "{..N} \<inter> a -` {z} = a -` {z}"
+    using N by blast
+  finally show ?thesis
+    by simp
+qed
+
+end (* weierstrass_product *)
+
+
+text \<open>
+  The following locale is the most common case of $p(n) = n$.
+\<close>
+locale weierstrass_product' =
+  fixes a :: "nat \<Rightarrow> complex"
+  assumes a_nonzero: "\<And>n. a n \<noteq> 0"
+  assumes filterlim_a: "filterlim a at_infinity at_top"
+  assumes finite_occs_a': "\<And>z. z \<in> range a \<Longrightarrow> finite (a -` {z})"
+begin
+
+lemma finite_occs_a: "finite (a -` {z})"
+proof (cases "z \<in> range a")
+  case False
+  hence "a -` {z} = {}"
+    by auto
+  thus ?thesis by simp
+qed (use finite_occs_a'[of z] in auto)
+
+sublocale weierstrass_product a "\<lambda>n. n"
+proof
+  fix r :: real assume r: "r > 0"
+  show "summable (\<lambda>n. (r / norm (a n)) ^ Suc n)"
+  proof (rule summable_comparison_test_ev)
+    have "eventually (\<lambda>n. norm (a n) > 2 * r) at_top"
+      using filterlim_a by (metis filterlim_at_infinity_imp_norm_at_top filterlim_at_top_dense)
+    thus "eventually (\<lambda>n. norm ((r / norm (a n)) ^ Suc n) \<le> (1 / 2) ^ Suc n) at_top"
+    proof eventually_elim
+      case (elim n)
+      have "norm ((r / norm (a n)) ^ Suc n) = (r / norm (a n)) ^ Suc n"
+        using \<open>r > 0\<close> by (simp add: abs_mult)
+      also have "\<dots> \<le> (1 / 2) ^ Suc n"
+        using \<open>r > 0\<close> elim by (intro power_mono) (auto simp: divide_simps)
+      finally show ?case .
+    qed
+  next
+    show "summable (\<lambda>n. (1 / 2) ^ Suc n :: real)"
+      unfolding summable_Suc_iff by (intro summable_geometric) auto
+  qed
+qed (use a_nonzero filterlim_a finite_occs_a in auto)
+
+end (* weierstrass_product' *)
+
+
+
+subsection \<open>Writing a quotient as an exponential\<close>
+
+text \<open>
+  If two holomorphic functions \<open>f\<close> and \<open>g\<close> on a simply connected domain have the same zeros with
+  the same multiplicities, they can be written as $g(x) = e^{h(x)} f(x)$ for some holomorphic
+  function $h(x)$.
+\<close>
+lemma holomorphic_zorder_factorization:
+  assumes "g holomorphic_on A" "open A" "connected A"
+  assumes "f holomorphic_on A" "\<And>z. z \<in> A \<Longrightarrow> f z = 0 \<longleftrightarrow> g z = 0"
+          "\<And>z. z \<in> A \<Longrightarrow> zorder f z = zorder g z"
+  obtains h where "h holomorphic_on A" "\<And>z. z \<in> A \<Longrightarrow> h z \<noteq> 0" "\<And>z. z \<in> A \<Longrightarrow> g z = h z * f z"
+proof (cases "\<exists>z\<in>A. g z \<noteq> 0")
+  case False
+  show ?thesis
+    by (rule that[of "\<lambda>_. 1"]) (use False assms in auto)
+next
+  case True
+  define F where "F = fps_expansion f"
+  define G where "G = fps_expansion g"
+  define c where "c = (\<lambda>z. fps_nth (G z) (subdegree (G z)) / fps_nth (F z) (subdegree (F z)))"
+  define h where "h = (\<lambda>z. if f z = 0 then c z else g z / f z)"
+
+  have ev_nonzero: "eventually (\<lambda>w. g w \<noteq> 0 \<and> w \<in> A) (at z)" if "z \<in> A" for z
+  proof -
+    from True obtain z0 where z0: "z0 \<in> A" "g z0 \<noteq> 0"
+      by auto
+    show ?thesis
+      by (rule non_zero_neighbour_alt[where ?\<beta> = z0])
+         (use assms that z0 in \<open>auto intro: simply_connected_imp_connected\<close>)
+  qed
+
+  have g_ana: "g analytic_on {z}" if "z \<in> A" for z
+    using assms \<open>open A\<close> analytic_at that by blast
+  have f_ana: "f analytic_on {z}" if "z \<in> A" for z
+    using assms \<open>open A\<close> analytic_at that by blast
+
+  have F: "(\<lambda>w. f (z + w)) has_fps_expansion F z" if "z \<in> A" for z
+    unfolding F_def by (rule analytic_at_imp_has_fps_expansion[OF f_ana[OF that]])
+  have G: "(\<lambda>w. g (z + w)) has_fps_expansion G z" if "z \<in> A" for z
+    unfolding G_def by (rule analytic_at_imp_has_fps_expansion[OF g_ana[OF that]])
+
+  have [simp]: "G z \<noteq> 0" if "z \<in> A" for z
+  proof
+    assume "G z = 0"
+    hence "eventually (\<lambda>w. g w = 0) (at z)" using G[OF that]
+      by (auto simp: has_fps_expansion_0_iff at_to_0' eventually_filtermap add_ac
+                     eventually_at_filter nhds_to_0' elim: eventually_mono)
+    hence "eventually (\<lambda>_. False) (at z)"
+      using ev_nonzero[OF that] unfolding eventually_at_filter by eventually_elim auto
+    thus False
+      by simp
+  qed
+  have [simp]: "F z \<noteq> 0" if "z \<in> A" for z
+  proof
+    assume "F z = 0"
+    hence "eventually (\<lambda>w. f w = 0) (at z)" using F[of z] that
+      by (auto simp: has_fps_expansion_0_iff at_to_0' eventually_filtermap add_ac
+                     eventually_at_filter nhds_to_0' elim: eventually_mono)
+    hence "eventually (\<lambda>_. False) (at z)"
+      using ev_nonzero[OF that] unfolding eventually_at_filter
+      by eventually_elim (use assms in auto)
+    thus False
+      by simp
+  qed
+  have [simp]: "c z \<noteq> 0" if "z \<in> A" for z
+    using that by (simp add: c_def)
+
+  have h: "h analytic_on {z} \<and> h z \<noteq> 0" if "z \<in> A" for z
+  proof -
+    show ?thesis
+    proof (cases "f z = 0")
+      case False
+      from False that have "(\<lambda>z. g z / f z) analytic_on {z}"
+        by (intro analytic_intros g_ana f_ana) auto
+      also have "?this \<longleftrightarrow> h analytic_on {z}"
+      proof (rule analytic_at_cong)
+        have "eventually (\<lambda>w. f w \<noteq> 0) (nhds z)"
+          using ev_nonzero[OF \<open>z \<in> A\<close>] unfolding eventually_at_filter
+          by eventually_elim (use False \<open>z \<in> A\<close> assms in auto)
+        thus "eventually (\<lambda>z. g z / f z = h z) (nhds z)"
+          by eventually_elim (auto simp: h_def)
+      qed auto
+      finally have "h analytic_on {z}" .
+      moreover have "h z \<noteq> 0"
+        using that assms by (simp add: h_def)
+      ultimately show ?thesis by blast
+    next
+      case True
+      with that have z: "z \<in> A" "f z = 0"
+        by auto
+      have "zorder f z = int (subdegree (F z))"
+        using F by (rule has_fps_expansion_zorder) (use z in auto)
+      also have "zorder f z = zorder g z"
+        using z assms by auto
+      also have "zorder g z = subdegree (G z)"
+        using G by (rule has_fps_expansion_zorder) (use z in auto)
+      finally have subdegree_eq: "subdegree (F z) = subdegree (G z)"
+        by simp
+  
+      have "(\<lambda>w. if w = 0 then c z else g (z + w) / f (z + w)) has_fps_expansion G z / F z" (is ?P)
+        using subdegree_eq z by (intro has_fps_expansion_divide F G) (auto simp: c_def)
+      also have "?this \<longleftrightarrow> (\<lambda>w. h (z + w)) has_fps_expansion G z / F z"
+      proof (intro has_fps_expansion_cong)
+        have "eventually (\<lambda>w. w \<noteq> z \<longrightarrow> f w \<noteq> 0) (nhds z)"
+          using ev_nonzero[OF \<open>z \<in> A\<close>] unfolding eventually_at_filter
+          by eventually_elim (use \<open>z \<in> A\<close> assms in auto)
+        hence "eventually (\<lambda>w. w \<noteq> 0 \<longrightarrow> f (z + w) \<noteq> 0) (nhds 0)"
+          by (simp add: nhds_to_0' eventually_filtermap)
+        thus "eventually (\<lambda>w. (if w = 0 then c z else g (z + w) / f (z + w)) = h (z + w)) (nhds 0)"
+          unfolding h_def by eventually_elim (use z in \<open>auto simp: c_def h_def\<close>)
+      qed auto
+      finally have "h analytic_on {z}"
+        using has_fps_expansion_imp_analytic by blast
+      moreover have "h z \<noteq> 0"
+        using that z by (auto simp: h_def c_def)
+      ultimately show ?thesis by blast
+    qed
+  qed
+
+  from h have h_ana: "h analytic_on A" and h_nz: "\<forall>z\<in>A. h z \<noteq> 0"
+    using analytic_on_analytic_at by blast+
+  moreover have "g z = h z * f z" if "z \<in> A" for z
+    using assms that by (auto simp: h_def)
+  ultimately show ?thesis
+    using \<open>open A\<close> by (intro that[of h]) (auto simp: analytic_on_open)
+qed
+
+
+subsection \<open>Constructing the sequence of zeros\<close>
+
+text \<open>
+  The form of the Weierstra\ss\ Factorisation Theorem that we derived above requires
+  an explicit sequence of the zeros that tends to infinity. We will now show that under
+  mild conditions, such a sequence always exists.
+
+  More precisely: if \<open>A\<close> is an infinite closed set that is sparse in the sense that its
+  intersection with any compact set is finite, then there exists an injective sequence \<open>f\<close>
+  enumerating the values of \<open>A\<close> in ascending order by absolute value, and \<open>f\<close> tends to infinity
+  for \<open>n \<rightarrow> \<infinity>\<close>.
+\<close>
+lemma sequence_of_sparse_set_exists:
+  fixes A :: "complex set"
+  assumes "infinite A" "closed A" "\<And>r. r \<ge> 0 \<Longrightarrow> finite (A \<inter> cball 0 r)"
+  obtains f :: "nat \<Rightarrow> complex"
+    where "mono (norm \<circ> f)" "inj f" "range f = A" "filterlim f at_infinity at_top"
+proof -
+  have "\<exists>f::nat \<Rightarrow> complex. \<forall>n.
+         f n \<in> A \<and>
+         f n \<notin> f ` {..<n} \<and>
+         {z\<in>A. norm z < norm (f n)} \<subseteq> f ` {..<n} \<and>
+         (\<forall>k<n. norm (f k) \<le> norm (f n))"
+  proof (rule dependent_wf_choice[OF wf], goal_cases)
+    case (1 f g n r)
+    thus ?case by auto
+  next
+    case (2 n f)
+    have f: "f k \<in> A" "{z \<in> A. norm z < norm (f k)} \<subseteq> f ` {..<k}" "\<forall>k'<k. cmod (f k') \<le> cmod (f k)"
+      if "k < n" for k
+      using 2[of k] that by simp_all
+  
+    have "infinite (A - f ` {..<n})"
+      using assms(1) by (intro Diff_infinite_finite) auto
+    then obtain z0 where z0: "z0 \<in> A - f ` {..<n}"
+      by (meson finite.intros(1) finite_subset subsetI)
+    have "finite (A \<inter> cball 0 (norm z0))"
+      by (intro assms(3)) auto
+    hence "finite (A \<inter> cball 0 (norm z0) - f ` {..<n})"
+      using finite_subset by blast
+    moreover from z0 have "A \<inter> cball 0 (norm z0) - f ` {..<n} \<noteq> {}"
+      by auto
+    ultimately obtain z where "is_arg_min norm (\<lambda>z. z \<in> A \<inter> cball 0 (norm z0) - f ` {..<n}) z"
+      using ex_is_arg_min_if_finite by blast
+    hence z: "z \<in> A" "norm z \<le> norm z0" "z \<notin> f ` {..<n}"
+             "\<And>w. w \<in> A \<Longrightarrow> norm w \<le> norm z0 \<Longrightarrow> w \<notin> f ` {..<n} \<Longrightarrow> norm w \<ge> norm z"
+      by (auto simp: is_arg_min_def)
+  
+    show ?case
+    proof (rule exI[of _ z], safe)
+      fix w assume w: "w \<in> A" "norm w < norm z"
+      with z(4)[of w] z w show "w \<in> f ` {..<n}"
+        by linarith
+    next
+      fix k assume k: "k < n"
+      show "norm (f k) \<le> norm z"
+        using f(2)[of k] z(1,3) k by auto
+    qed (use z in auto)
+  qed
+  then obtain f :: "nat \<Rightarrow> complex" where f:
+    "\<And>n. f n \<in> A"
+    "\<And>n. f n \<notin> f ` {..<n}"
+    "\<And>n. {z\<in>A. norm z < norm (f n)} \<subseteq> f ` {..<n}"
+    "\<And>k n. k < n \<Longrightarrow> norm (f k) \<le> norm (f n)"
+    by meson
+  from f(2) have f_neq: "f n \<noteq> f k" if "k < n" for k n
+    using that by blast
+
+  have inj: "inj f"
+  proof (rule injI)
+    fix m n :: nat
+    assume "f m = f n"
+    thus "m = n"
+      using f_neq[of m n] f_neq[of n m] by (cases m n rule: linorder_cases) auto
+  qed      
+
+  have range: "range f = A"
+  proof safe
+    fix z assume z: "z \<in> A"
+    show "z \<in> range f"
+    proof (rule ccontr)
+      assume "z \<notin> range f"
+      hence "norm (f n) \<le> norm z" for n
+        using f(3)[of n] z by auto
+      hence "range f \<subseteq> A \<inter> cball 0 (norm z)"
+        using f(1) by auto
+      moreover have "finite (A \<inter> cball 0 (norm z))"
+        by (intro assms) auto
+      ultimately have "finite (range f)"
+        using finite_subset by blast
+      moreover have "infinite (range f)"
+        using inj by (subst finite_image_iff) auto
+      ultimately show False by contradiction
+    qed
+  qed (use f(1) in auto)
+
+  have mono: "mono (norm \<circ> f)"
+  proof (rule monoI, unfold o_def)
+    fix m n :: nat
+    assume "m \<le> n"
+    thus "norm (f m) \<le> norm (f n)"
+      using f(4)[of m n] by (cases "m < n") auto
+  qed
+
+  have "\<not>bounded A"
+  proof
+    assume "bounded A"
+    hence "bdd_above (norm ` A)"
+      by (meson bdd_above_norm)
+    hence "norm z \<le> Sup (norm ` A)" if "z \<in> A" for z
+      using that by (meson cSUP_upper)
+    hence "A \<subseteq> cball 0 (Sup (norm ` A))"
+      by auto
+    also have "\<dots> \<subseteq> cball 0 (max 1 (Sup (norm ` A)))"
+      by auto
+    finally have "A \<subseteq> A \<inter> cball 0 (max 1 (Sup (norm ` A)))"
+      by blast
+    moreover have "finite (A \<inter> cball 0 (max 1 (Sup (norm ` A))))"
+      by (intro assms) auto
+    ultimately have "finite A"
+      using finite_subset by blast
+    hence "finite (range f)"
+      by (simp add: range)
+    thus False
+      using inj by (subst (asm) finite_image_iff) auto
+  qed
+
+  have lim: "filterlim f at_infinity at_top"
+    unfolding filterlim_at_infinity_conv_norm_at_top filterlim_at_top
+  proof
+    fix C :: real
+    from \<open>\<not>bounded A\<close> obtain z where "z \<in> A" "norm z > C"
+      unfolding bounded_iff by (auto simp: not_le)
+    obtain n where [simp]: "z = f n"
+      using range \<open>z \<in> A\<close> by auto
+    show "eventually (\<lambda>n. norm (f n) \<ge> C) at_top"
+      using eventually_ge_at_top[of n]
+    proof eventually_elim
+      case (elim k)
+      have "C \<le> norm (f n)"
+        using \<open>norm z > C\<close> by simp
+      also have "\<dots> \<le> norm (f k)"
+        using monoD[OF \<open>mono (norm \<circ> f)\<close>, of n k] elim by auto
+      finally show ?case .
+    qed
+  qed
+
+  show ?thesis
+    by (intro that[of f] inj range mono lim)
+qed
+
+(* TODO: of general interest? *)
+lemma strict_mono_sequence_partition:
+  assumes "strict_mono (f :: nat \<Rightarrow> 'a :: {linorder, no_top})"
+  assumes "x \<ge> f 0"
+  assumes "filterlim f at_top at_top"
+  shows   "\<exists>k. x \<in> {f k..<f (Suc k)}"
+proof -
+  define k where "k = (LEAST k. f (Suc k) > x)"
+  {
+    obtain n where "x \<le> f n"
+      using assms by (auto simp: filterlim_at_top eventually_at_top_linorder)
+    also have "f n < f (Suc n)"
+      using assms by (auto simp: strict_mono_Suc_iff)
+    finally have "\<exists>n. f (Suc n) > x" by auto
+  }
+  from LeastI_ex[OF this] have "x < f (Suc k)"
+    by (simp add: k_def)
+  moreover have "f k \<le> x"
+  proof (cases k)
+    case (Suc k')
+    have "k \<le> k'" if "f (Suc k') > x"
+      using that unfolding k_def by (rule Least_le)
+    with Suc show "f k \<le> x" by (cases "f k \<le> x") (auto simp: not_le)
+  qed (use assms in auto)
+  ultimately show ?thesis by auto
+qed
+
+(* TODO: of general interest? *)
+lemma strict_mono_sequence_partition':
+  assumes "strict_mono (f :: nat \<Rightarrow> 'a :: {linorder, no_top})"
+  assumes "x \<ge> f 0"
+  assumes "filterlim f at_top at_top"
+  shows   "\<exists>!k. x \<in> {f k..<f (Suc k)}"
+proof (rule ex_ex1I)
+  show "\<exists>k. x \<in> {f k..<f (Suc k)}"
+    using strict_mono_sequence_partition[OF assms] .
+  fix k1 k2 assume "x \<in> {f k1..<f (Suc k1)}" "x \<in> {f k2..<f (Suc k2)}"
+  thus "k1 = k2"
+  proof (induction k1 k2 rule: linorder_wlog)
+    case (le k1 k2)
+    hence "f k2 < f (Suc k1)"
+      by auto
+    hence "k2 < Suc k1"
+      using assms(1) strict_mono_less by blast
+    with le show "k1 = k2"
+      by linarith
+  qed auto
+qed
+
+lemma sequence_of_sparse_set_exists':
+  fixes A :: "complex set" and c :: "complex \<Rightarrow> nat"
+  assumes "infinite A" "closed A" "\<And>r. r \<ge> 0 \<Longrightarrow> finite (A \<inter> cball 0 r)"
+  assumes c_pos: "\<And>x. x \<in> A \<Longrightarrow> c x > 0"
+  obtains f :: "nat \<Rightarrow> complex" where
+    "mono (norm \<circ> f)" "range f = A" "filterlim f at_infinity at_top"
+    "\<And>z. z \<in> A \<Longrightarrow> finite (f -` {z}) \<and> card (f -` {z}) = c z"
+proof -
+  obtain f :: "nat \<Rightarrow> complex" where f:
+    "mono (norm \<circ> f)" "inj f" "range f = A" "filterlim f at_infinity at_top"
+    using assms sequence_of_sparse_set_exists by blast
+  have f_eq_iff [simp]: "f m = f n \<longleftrightarrow> m = n" for m n
+    using \<open>inj f\<close> by (auto simp: inj_def)
+
+  define h :: "nat \<Rightarrow> nat" where "h = (\<lambda>n. \<Sum>k<n. c (f k))"
+
+  have [simp]: "h 0 = 0"
+    by (simp add: h_def)
+  have h_ge: "h n \<ge> n" for n
+  proof -
+    have "h n \<ge> (\<Sum>k<n. 1)"
+      unfolding h_def by (intro sum_mono) (use c_pos f in \<open>auto simp: Suc_le_eq\<close>)
+    thus ?thesis by simp
+  qed
+
+  have "strict_mono h"
+    unfolding strict_mono_Suc_iff using f by (auto simp: h_def c_pos)
+  moreover from this have "filterlim h at_top at_top"
+    using filterlim_subseq by blast
+  ultimately have Ex1: "\<exists>!k. n \<in> {h k..<h (Suc k)}" for n
+    by (intro strict_mono_sequence_partition') auto
+
+  define g :: "nat \<Rightarrow> nat" where "g = (\<lambda>n. THE k. n \<in> {h k..<h (Suc k)})"
+  have g: "n \<in> {h (g n)..<h (Suc (g n))}" for n
+    using theI'[OF Ex1[of n]] by (simp add: g_def)
+  have g_eqI: "g n = k" if "n \<in> {h k..<h (Suc k)}" for n k
+    using the1_equality[OF Ex1 that] by (simp add: g_def)
+  have g_h: "g (h n) = n" for n
+    by (rule g_eqI) (auto intro: strict_monoD[OF \<open>strict_mono h\<close>])
+
+  have "mono g"
+    unfolding incseq_Suc_iff
+  proof safe
+    fix n :: nat
+    have "h (g n) + 1 \<le> Suc n"
+      using g[of n] by auto
+    also have "Suc n < h (Suc (g (Suc n)))"
+      using g[of "Suc n"] by auto
+    finally show "g n \<le> g (Suc n)"
+      by (metis \<open>strict_mono h\<close> add_lessD1 less_Suc_eq_le strict_mono_less)
+  qed
+
+  have "filterlim g at_top at_top"
+    unfolding filterlim_at_top
+  proof
+    fix n :: nat
+    show "eventually (\<lambda>m. g m \<ge> n) at_top"
+      using eventually_ge_at_top[of "h n"]
+    proof eventually_elim
+      case (elim m)
+      have "n \<le> g (h n)"
+        by (simp add: g_h)
+      also have "g (h n) \<le> g m"
+        by (intro monoD[OF \<open>mono g\<close>] elim)
+      finally show ?case .
+    qed
+  qed
+
+  have vimage: "(f \<circ> g) -` {f n} = {h n..<h (Suc n)}" for n
+    using g by (auto intro!: g_eqI)
+
+  show ?thesis
+  proof (rule that[of "f \<circ> g"])
+    have "incseq (\<lambda>n. (norm \<circ> f) (g n))"
+      by (intro monoI monoD[OF f(1)] monoD[OF \<open>incseq g\<close>])
+    thus "incseq (norm \<circ> (f \<circ> g))"
+      by (simp add: o_def)
+  next
+    have "range (f \<circ> g) \<subseteq> A"
+      using f(3) by auto
+    moreover have "A \<subseteq> range (f \<circ> g)"
+    proof
+      fix z assume "z \<in> A"
+      then obtain n where [simp]: "z = f n"
+        using f(3) by auto
+      have "f (g (h n)) \<in> range (f \<circ> g)"
+        unfolding o_def by blast
+      thus "z \<in> range (f \<circ> g)"
+        by (simp add: g_h)
+    qed
+    ultimately show "range (f \<circ> g) = A" by blast
+  next
+    fix z assume "z \<in> A"
+    then obtain n where [simp]: "z = f n"
+      using f(3) by auto
+    have "finite {h n..<h (Suc n)}"
+      by auto
+    moreover have "card {h n..<h (Suc n)} = c z"
+      by (simp add: h_def)
+    ultimately show "finite ((f \<circ> g) -` {z}) \<and> card ((f \<circ> g) -` {z}) = c z"
+      using vimage[of n] by simp
+  next
+    show "filterlim (f \<circ> g) at_infinity at_top"
+      unfolding o_def by (rule filterlim_compose[OF f(4) \<open>filterlim g at_top at_top\<close>])
+  qed
+qed
+
+subsection \<open>The factorisation theorem for holomorphic functions\<close>
+
+text \<open>
+  If \<open>g\<close> is a holomorphic function on an open connected domain whose zeros do not
+  have an accumulation point on the frontier of \<open>A\<close>, then we can write \<open>g\<close> as a product
+  of a function \<open>h\<close> holomorphic on \<open>A\<close> and an entire function \<open>f\<close> such that \<open>h\<close> is non-zero
+  everywhere in \<open>A\<close> and the zeros of \<open>f\<close> are precisely the zeros of \<open>A\<close> with the same multiplicity.
+
+  In other words, we can get rid of all the zeros of \<open>g\<close> by dividing it with a suitable
+  entire function \<open>f\<close>.
+\<close>
+theorem weierstrass_factorization:
+  assumes "g holomorphic_on A" "open A" "connected A" 
+  assumes "\<And>z. z \<in> frontier A \<Longrightarrow> \<not>z islimpt {w\<in>A. g w = 0}"
+  obtains h f where
+    "h holomorphic_on A" "f holomorphic_on UNIV"
+    "\<forall>z. f z = 0 \<longleftrightarrow> (\<forall>z\<in>A. g z = 0) \<or> (z \<in> A \<and> g z = 0)"
+    "\<forall>z\<in>A. zorder f z = zorder g z"
+    "\<forall>z\<in>A. h z \<noteq> 0"
+    "\<forall>z\<in>A. g z = h z * f z"
+proof (cases "\<forall>z\<in>A. g z = 0")
+  case True
+  show ?thesis
+  proof (rule that[of "\<lambda>_. 1" "\<lambda>_. 0"]; (intro ballI allI impI)?)
+    fix z assume z: "z \<in> A"
+    have ev: "eventually (\<lambda>w. w \<in> A) (at z)"
+      using z assms by (intro eventually_at_in_open') auto
+    show "zorder (\<lambda>_::complex. 0 :: complex) z = zorder g z"
+      by (intro zorder_cong eventually_mono[OF ev] refl) (use True in auto)
+  qed (use assms True in auto)
+next
+  case not_identically_zero: False
+  define Z where "Z = {z\<in>A. g z = 0}"
+  have freq_nz: "frequently (\<lambda>z. g z \<noteq> 0) (at z)" if "z \<in> A" for z
+  proof -
+    have "\<forall>\<^sub>F w in at z. g w \<noteq> 0 \<and> w \<in> A"
+      using non_zero_neighbour_alt[OF assms(1,2,3) that(1)] not_identically_zero by auto
+    hence  "\<forall>\<^sub>F w in at z. g w \<noteq> 0"
+      by eventually_elim auto
+    thus ?thesis
+      using eventually_frequently by force
+  qed
+
+  have zorder_pos_iff: "zorder g z > 0 \<longleftrightarrow> g z = 0" if "z \<in> A" for z
+    by (subst zorder_pos_iff[OF assms(1,2) that]) (use freq_nz[of z] that in auto)
+
+  show ?thesis
+  proof (cases "finite Z")
+    case True
+    define f where "f = (\<lambda>z. \<Prod>w\<in>Z. (z - w) powi (zorder g w))"
+
+    have eq_zero_iff: "f z = 0 \<longleftrightarrow> z \<in> A \<and> g z = 0" for z
+      using True local.zorder_pos_iff
+      unfolding f_def Z_def by fastforce
+    have zorder_eq: "zorder f z = zorder g z" if "z \<in> A" for z
+    proof (cases "g z = 0")
+      case False
+      have "g analytic_on {z}"
+        using that assms analytic_at by blast
+      hence [simp]: "zorder g z = 0"
+        using False by (intro zorder_eq_0I) auto
+      moreover have "f analytic_on {z}"
+        unfolding f_def by (auto intro!: analytic_intros)
+      hence "zorder f z = 0"
+        using False by (intro zorder_eq_0I) (auto simp: eq_zero_iff)
+      ultimately show ?thesis
+        by simp
+    next
+      case zero: True
+      have "g analytic_on {z}"
+        using that assms(1,2) analytic_at by blast
+      hence "zorder g z \<ge> 0"
+        using that by (intro zorder_ge_0 freq_nz) auto
+      define f' where "f' = (\<lambda>z'. (\<Prod>w\<in>Z-{z}. (z' - w) powi (zorder g w)))"
+      have "zorder (\<lambda>z'. (z' - z) powi (zorder g z) * f' z') z = zorder g z"
+      proof (rule zorder_eqI)
+        show "open (UNIV :: complex set)" "f' holomorphic_on UNIV" "z \<in> UNIV"
+          using local.zorder_pos_iff
+          by (fastforce intro!: holomorphic_intros simp: f'_def Z_def)+
+        show "f' z \<noteq> 0"
+          using True unfolding f'_def by (subst prod_zero_iff) auto
+      qed (use \<open>zorder g z \<ge> 0\<close> in \<open>auto simp: powr_of_int\<close>)
+      also have "(\<lambda>z'. (z' - z) powi (zorder g z) * f' z') = f"
+      proof
+        fix z' :: complex
+        have "Z = insert z (Z - {z})"
+          using that zero by (auto simp: Z_def)
+        also have "(\<Prod>w\<in>\<dots>. (z' - w) powi (zorder g w)) = (z' - z) powi (zorder g z) * f' z'"
+          using True by (subst prod.insert) (auto simp: f'_def)
+        finally show "(z' - z) powi (zorder g z) * f' z' = f z'"
+          by (simp add: f_def)
+      qed
+      finally show ?thesis .
+    qed
+
+    obtain h :: "complex \<Rightarrow> complex" where h:
+       "h holomorphic_on A" "\<And>z. z \<in> A \<Longrightarrow> h z \<noteq> 0" "\<And>z. z \<in> A \<Longrightarrow> g z = h z * f z"
+    proof (rule holomorphic_zorder_factorization[OF assms(1-3)])
+      show "f holomorphic_on A"
+        using local.zorder_pos_iff
+        unfolding f_def Z_def by (fastforce intro: holomorphic_intros)
+      show "f z = 0 \<longleftrightarrow> g z = 0" if "z \<in> A" for z
+        using that by (subst eq_zero_iff) auto
+      show "zorder f z = zorder g z" if "z \<in> A" for z
+        by (rule zorder_eq) fact
+    qed metis
+
+    show ?thesis
+    proof (rule that[of h f]; (intro ballI)?)
+      show "h holomorphic_on A"
+        by fact
+      show "f holomorphic_on UNIV"
+        using local.zorder_pos_iff
+        unfolding f_def Z_def by (fastforce intro: holomorphic_intros)
+    qed (use True not_identically_zero in \<open>auto simp: eq_zero_iff zorder_eq h(2) h(3)[symmetric]\<close>)
+
+  next
+    case False
+    note infinite_zeroes = not_identically_zero False
+    define c where "c = (\<lambda>z. nat (zorder g z))"
+
+    have ev_nz: "eventually (\<lambda>w. g w \<noteq> 0) (at z)" if "z \<in> A" for z
+    proof -
+      from infinite_zeroes(1) obtain z0 where z0: "z0 \<in> A" "g z0 \<noteq> 0"
+        by auto
+      have "eventually (\<lambda>w. g w \<noteq> 0 \<and> w \<in> A) (at z)"
+        by (rule non_zero_neighbour_alt[where ?\<beta> = z0]) (use assms z0 that in auto)
+      thus ?thesis
+        by eventually_elim auto
+    qed
+
+    have no_limpt_Z: "\<not>z islimpt Z" for z
+    proof
+      assume "z islimpt Z"
+      show False
+      proof (cases "z \<in> A")
+        case False
+        have "z islimpt A"
+          by (rule islimpt_subset[OF \<open>z islimpt Z\<close>]) (auto simp: Z_def)
+        hence "z \<in> closure A"
+          by (simp add: closure_def)
+        with \<open>z \<notin> A\<close> have "z \<in> frontier A"
+          by (simp add: closure_Un_frontier)
+        with assms and \<open>z islimpt Z\<close> show False
+          by (auto simp: Z_def)
+      next
+        case True
+        from True have "eventually (\<lambda>w. g w \<noteq> 0) (at z)"
+          using ev_nz by blast
+        hence "\<not>z islimpt Z"
+          by (auto simp: islimpt_iff_eventually Z_def elim!: eventually_mono)
+        with \<open>z islimpt Z\<close> show False by blast        
+      qed
+    qed
+    have "closed Z"
+      using no_limpt_Z unfolding closed_limpt by blast
+   
+    obtain a where a:
+        "incseq (norm \<circ> a)" "range a = Z - {0}"
+        "\<And>z. z \<in> Z - {0} \<Longrightarrow> finite (a -` {z}) \<and> card (a -` {z}) = c z"
+        "filterlim a at_infinity at_top"
+    proof (rule sequence_of_sparse_set_exists')
+      show "infinite (Z - {0})"
+        using infinite_zeroes(2) by auto
+    next
+      show "closed (Z - {0})" 
+        unfolding closed_limpt using no_limpt_Z islimpt_subset by blast
+    next
+      show "finite ((Z - {0}) \<inter> cball 0 R)" if "R \<ge> 0" for R
+      proof (rule ccontr)
+        assume *: "infinite ((Z - {0}) \<inter> cball 0 R)"
+        have "\<exists>z\<in>cball 0 R. z islimpt ((Z - {0}) \<inter> cball 0 R)"
+          by (rule Heine_Borel_imp_Bolzano_Weierstrass) (use * in auto)
+        then obtain z where "z islimpt ((Z - {0}) \<inter> cball 0 R)"
+          by blast
+        hence "z islimpt Z"
+          using islimpt_subset by blast
+        thus False
+          using no_limpt_Z by blast
+      qed
+    next
+      show "c z > 0" if "z \<in> Z - {0}" for z
+        using zorder_pos_iff[of z] that by (auto simp: c_def Z_def)
+    qed metis 
+
+    interpret f: weierstrass_product' a
+    proof
+      show "a n \<noteq> 0" for n
+        using a(2) by auto
+      show "finite (a -` {z})" if "z \<in> range a" for z
+        using a(3)[of z] a(2) that by simp
+    qed fact+
+
+    define m where "m = (if 0 \<in> A then nat (zorder g 0) else  0)"
+
+    have zorder_eq: "zorder (\<lambda>z. z ^ m * f.f z) z = zorder g z" if "z \<in> A" for z
+    proof (cases "g z = 0")
+      case False
+      have "g analytic_on {z}"
+        using \<open>z \<in> A\<close> analytic_at assms by blast
+      hence "zorder g z = 0"
+        by (intro zorder_eq_0I False)
+      have "z \<notin> range a"
+        using False Z_def a(2) by blast
+      hence "zorder (\<lambda>z. z ^ m * f.f z) z = 0"
+        using False \<open>zorder g z = 0\<close>
+        by (intro zorder_eq_0I analytic_intros) (auto simp: f.zero m_def)
+      with \<open>zorder g z = 0\<close> show ?thesis
+        by simp
+    next
+      case True
+      define F where "F = fps_expansion f.f z"
+      have "frequently (\<lambda>w. g w \<noteq> 0) (at z)"
+        using ev_nz[OF that] eventually_frequently by force
+      hence "zorder g z \<ge> 0"
+        by (intro zorder_ge_0) (use assms that in \<open>auto simp: analytic_at\<close>)
+      
+      have ev: "eventually (\<lambda>z. z \<in> A) (nhds z)"
+        using that assms by (intro eventually_nhds_in_open) auto
+      have exp1: "(\<lambda>w. f.f (z + w)) has_fps_expansion F"
+        unfolding F_def by (intro analytic_at_imp_has_fps_expansion[OF f.analytic])
+      have exp2: "(\<lambda>w. (z + w) ^ m * f.f (z + w)) has_fps_expansion (fps_const z + fps_X) ^ m * F"
+        by (intro fps_expansion_intros exp1)
+      have [simp]: "F \<noteq> 0"
+      proof
+        assume "F = 0"
+        hence "eventually (\<lambda>z. f.f z = 0) (nhds z)"
+          using exp1 by (auto simp: has_fps_expansion_def nhds_to_0' eventually_filtermap)
+        hence "eventually (\<lambda>z. g z = 0) (at z)"
+          by (auto simp: f.zero a Z_def eventually_at_filter elim!: eventually_mono)
+        hence "eventually (\<lambda>z::complex. False) (at z)"
+          using ev_nz[OF \<open>z \<in> A\<close>] by eventually_elim auto
+        thus False by simp
+      qed
+      
+      have "zorder (\<lambda>w. w ^ m * f.f w) z = int (subdegree ((fps_const z + fps_X) ^ m * F))"
+        using has_fps_expansion_zorder[OF exp2] by simp
+      also have "\<dots> = int (subdegree F) + (if z = 0 then m else 0)"
+        by auto
+      also have "int (subdegree F) = zorder f.f z"
+        using has_fps_expansion_zorder[OF exp1] by simp
+      also have "\<dots> = int (card (a -` {z}))"
+        by (rule f.zorder)
+      also have "card (a -` {z}) = (if z = 0 then 0 else c z)"
+      proof (cases "z = 0")
+        case True
+        hence "a -` {z} = {}"
+          using a(2) by auto
+        thus ?thesis using True by simp
+      next
+        case False
+        thus ?thesis
+          by (subst a(3)) (use True that in \<open>auto simp: Z_def\<close>)
+      qed
+      also have "int \<dots> + (if z = 0 then m else 0) = zorder g z"
+        using \<open>zorder g z \<ge> 0\<close> that by (auto simp: c_def m_def)
+      finally show ?thesis .
+    qed 
+
+    have eq_zero_iff: "z ^ m * f.f z = 0 \<longleftrightarrow> g z = 0" if "z \<in> A" for z
+      using that by (auto simp add: f.zero a m_def zorder_pos_iff Z_def)
+
+    obtain h :: "complex \<Rightarrow> complex" where h:
+       "h holomorphic_on A" "\<And>z. z \<in> A \<Longrightarrow> h z \<noteq> 0" "\<And>z. z \<in> A \<Longrightarrow> g z = h z * (z ^ m * f.f z)"
+    proof (rule holomorphic_zorder_factorization[OF assms(1-3)])
+      show "(\<lambda>z. z ^ m * f.f z) holomorphic_on A"
+        by (intro holomorphic_intros)
+      show "z ^ m * f.f z = 0 \<longleftrightarrow> g z = 0" if "z \<in> A" for z
+        by (rule eq_zero_iff) fact+
+      show "zorder (\<lambda>z. z ^ m * f.f z) z = zorder g z" if "z \<in> A" for z
+        by (rule zorder_eq) fact+
+    qed metis
+
+    show ?thesis
+    proof (rule that[of h "\<lambda>z. z ^ m * f.f z"]; (intro ballI allI impI)?)
+      show "h holomorphic_on A"
+        by fact
+      show "(\<lambda>z. z ^ m * f.f z) holomorphic_on UNIV"
+        by (intro holomorphic_intros)
+    next
+      fix z :: complex
+      show "(z ^ m * f.f z = 0) = ((\<forall>z\<in>A. g z = 0) \<or> z \<in> A \<and> g z = 0)"
+        using infinite_zeroes(1) a(2)
+        by (auto simp: m_def zorder_eq eq_zero_iff zorder_pos_iff Z_def f.zero)
+    qed (use zorder_eq eq_zero_iff h in auto)
+  qed
+qed
+
+text \<open>
+  The following is a simpler version for entire functions.
+\<close>
+theorem weierstrass_factorization_UNIV:
+  assumes "g holomorphic_on UNIV" 
+  obtains h f where
+    "h holomorphic_on UNIV" "f holomorphic_on UNIV"
+    "\<forall>z. f z = 0 \<longleftrightarrow> g z = 0"
+    "\<forall>z. zorder f z = zorder g z"
+    "\<forall>z. h z \<noteq> 0"
+    "\<forall>z. g z = h z * f z"
+  using assms by (rule weierstrass_factorization, goal_cases) auto
+
+
+
+subsection \<open>The factorisation theorem for meromorphic functions\<close>
+
+text \<open>
+  Let \<open>g\<close> be a meromorphic function on a connected open domain \<open>A\<close>. Assume that the poles and
+  zeros of \<open>g\<close> have no accumulation point on the border of \<open>A\<close>. Then \<open>g\<close> can be written in the
+  form $g(z) = h(z) f_1(z) / f_2(z)$ where $h$ is holomorphic on \<open>A\<close> with no zeroes and $f_1$ and
+  $f_2$ are entire.
+  
+  Moreover, as direct consequences of that, the zeroes of $f_1$ are precisely the zeroes of $g$
+  and the zeros of $f_2$ are precisely the poles of $g$ (with the corresponding multiplicity).
+\<close>
+theorem weierstrass_factorization_meromorphic:
+  assumes mero: "g nicely_meromorphic_on A" and A: "open A" "connected A"
+  assumes no_limpt: "\<And>z. z \<in> frontier A \<Longrightarrow> \<not>z islimpt {w\<in>A. g w = 0 \<or> is_pole g w}"
+  obtains h f1 f2 where
+    "h holomorphic_on A" "f1 holomorphic_on UNIV" "f2 holomorphic_on UNIV"
+    "\<forall>z\<in>A. f1 z = 0 \<longleftrightarrow> \<not>is_pole g z \<and> g z = 0"
+    "\<forall>z\<in>A. f2 z = 0 \<longleftrightarrow> is_pole g z"
+    "\<forall>z\<in>A. \<not>is_pole g z \<longrightarrow> zorder f1 z = zorder g z"
+    "\<forall>z\<in>A. is_pole g z \<longrightarrow> zorder f2 z = -zorder g z"
+    "\<forall>z\<in>A. h z \<noteq> 0"
+    "\<forall>z\<in>A. g z = h z * f1 z / f2 z"
+proof -
+  have mero': "g meromorphic_on A"
+    using mero unfolding nicely_meromorphic_on_def by auto
+  define pts where "pts = {z\<in>A. is_pole g z}"
+  have "{z. is_pole g z} sparse_in A"
+    using meromorphic_on_imp_not_pole_cosparse[OF mero']
+    by (auto simp: eventually_cosparse)
+  hence "pts sparse_in A"
+    unfolding pts_def by (rule sparse_in_subset2) auto
+  have open_diff_pts: "open (A - pts')" if "pts' \<subseteq> pts" for pts'
+  proof (rule open_diff_sparse_pts)
+    show "pts' sparse_in A"
+      using \<open>pts sparse_in A\<close> by (rule sparse_in_subset2) fact
+  qed (use \<open>open A\<close> in auto)
+  
+  have ev: "eventually (\<lambda>w. w \<in> A - pts) (at z)" if "z \<in> A" for z
+  proof (cases "z \<in> pts")
+    case False
+    thus ?thesis
+      using that open_diff_pts[of "pts"] by (intro eventually_at_in_open') auto
+  next
+    case True
+    have "eventually (\<lambda>w. w \<in> (A - (pts - {z})) - {z}) (at z)"
+      using that by (intro eventually_at_in_open open_diff_pts) auto
+    also have "A - (pts - {z}) - {z} = A - pts"
+      using True by auto
+    finally show ?thesis .
+  qed
+
+  show ?thesis
+  proof (cases "\<forall>z\<in>A-pts. g z = 0")
+    case True
+    have no_poles: "\<not>is_pole g z" if "z \<in> A" for z
+    proof -
+      have "is_pole g z \<longleftrightarrow> is_pole (\<lambda>_::complex. 0 :: complex) z"
+        by (intro is_pole_cong[OF eventually_mono[OF ev]]) (use that True in auto)
+      thus ?thesis
+        by simp
+    qed
+    hence [simp]: "pts = {}"
+      by (auto simp: pts_def)
+    have [simp]: "zorder g z = zorder (\<lambda>_::complex. 0 :: complex) z" if "z \<in> A" for z
+      by (intro zorder_cong[OF eventually_mono[OF ev]]) (use True that in auto)
+    show ?thesis
+      by (rule that[of "\<lambda>_. 1" "\<lambda>_. 0" "\<lambda>_. 1"]) (use True in \<open>auto simp: no_poles\<close>)
+  
+  next
+  
+    case False
+    have is_pole_iff: "is_pole g z \<longleftrightarrow> z \<in> pts" if "z \<in> A" for z
+      using that by (auto simp: pts_def)
+  
+    obtain h f1 where h_f1:
+      "h holomorphic_on A - pts" "f1 holomorphic_on UNIV"
+      "\<forall>z. f1 z = 0 \<longleftrightarrow> (\<forall>z\<in>A-pts. g z = 0) \<or> (z \<in> A - pts \<and> g z = 0)"
+      "\<forall>z\<in>A-pts. zorder f1 z = zorder g z"
+      "\<forall>z\<in>A-pts. h z \<noteq> 0"
+      "\<forall>z\<in>A-pts. g z = h z * f1 z"
+    proof (rule weierstrass_factorization)
+      have "g analytic_on A - pts"
+        by (rule nicely_meromorphic_without_singularities)
+           (use mero in \<open>auto simp: pts_def dest: nicely_meromorphic_on_subset\<close>)
+      thus holo: "g holomorphic_on A - pts"
+        by (rule analytic_imp_holomorphic)
+      show "open (A - pts)"
+        by (rule open_diff_pts) auto
+      show "connected (A - pts)"
+        by (rule sparse_imp_connected) (use A \<open>pts sparse_in A\<close> in auto)
+      show "\<not> z islimpt {w \<in> A - pts. g w = 0}" if "z \<in> frontier (A - pts)" for z
+      proof -
+        from that have "z \<in> frontier A - pts \<union> pts"
+          using \<open>open (A - pts)\<close> \<open>open A\<close> closure_mono[of "A - pts" A]
+          by (auto simp: frontier_def interior_open)
+        thus ?thesis
+        proof
+          assume "z \<in> pts"
+          hence "is_pole g z"
+            by (auto simp: pts_def)
+          hence "eventually (\<lambda>z. g z \<noteq> 0) (at z)"
+            using non_zero_neighbour_pole by blast
+          hence "\<not>z islimpt {w. g w = 0}"
+            by (auto simp: islimpt_iff_eventually)
+          thus ?thesis
+            using islimpt_subset[of z "{w\<in>A-pts. g w = 0}" "{w. g w = 0}"] by blast
+        next
+          assume z: "z \<in> frontier A - pts"
+          show "\<not> z islimpt {w \<in> A - pts. g w = 0}"
+          proof
+            assume "z islimpt {w \<in> A - pts. g w = 0}"
+            hence "z islimpt {w \<in> A. g w = 0 \<or> is_pole g w}"
+              by (rule islimpt_subset) (auto simp: pts_def)
+            thus False using no_limpt z by blast
+          qed
+        qed
+      qed
+    qed
+  
+    have f1_eq_0_iff: "f1 z = 0 \<longleftrightarrow> (z \<in> A - pts \<and> g z = 0)" for z
+      using h_f1(3) False by auto
+  
+    define h' where "h' = (\<lambda>z. if z \<in> pts then 0 else inverse (h z))"
+
+    have isolated_h: "isolated_singularity_at h z" if "z \<in> pts" for z
+    proof -
+      have "open (A - (pts - {z}))"
+        by (rule open_diff_pts) auto
+      moreover have "z \<in> (A - (pts - {z}))"
+        using that by (auto simp: pts_def)
+      moreover have "h holomorphic_on (A - (pts - {z})) - {z}"
+        by (rule holomorphic_on_subset[OF h_f1(1)]) (use that in auto)
+      ultimately show "isolated_singularity_at h z"
+        using isolated_singularity_at_holomorphic by blast
+    qed
+
+    have is_pole_h: "is_pole h z" if "z \<in> A" "is_pole g z" for z
+    proof -
+      have f1: "f1 analytic_on {z}"
+        by (meson analytic_on_holomorphic h_f1(2) open_UNIV top_greatest)
+      have "eventually (\<lambda>w. g w \<noteq> 0) (at z)"
+        using \<open>is_pole g z\<close> non_zero_neighbour_pole by blast
+      with ev[OF that(1)] have ev': "eventually (\<lambda>w. g w * f1 w \<noteq> 0) (at z)"
+        by eventually_elim (use h_f1(3) in auto)
+
+      have "is_pole (\<lambda>w. g w / f1 w) z"
+      proof (rule is_pole_divide_zorder)
+        show "isolated_singularity_at f1 z" "not_essential f1 z"
+          using f1 by (simp_all add: isolated_singularity_at_analytic not_essential_analytic)
+        show "isolated_singularity_at g z" "not_essential g z"
+          using mero' that unfolding meromorphic_on_altdef by blast+
+        show freq: "frequently (\<lambda>w. g w * f1 w \<noteq> 0) (at z)"
+          using ev' by (rule eventually_frequently[rotated]) auto
+        from freq have freq': "frequently (\<lambda>w. f1 w \<noteq> 0) (at z)"
+          using frequently_elim1 by fastforce
+        have "zorder g z < 0"
+          using \<open>is_pole g z\<close> \<open>isolated_singularity_at g z\<close> isolated_pole_imp_neg_zorder by auto
+        also have "0 \<le> zorder f1 z"
+          by (rule zorder_ge_0[OF f1 freq'])
+        finally show "zorder g z < zorder f1 z" .
+      qed
+      also have "?this \<longleftrightarrow> is_pole h z"
+      proof (intro is_pole_cong refl eventually_mono[OF eventually_conj[OF ev[OF that(1)] ev']])
+        fix w assume "w \<in> A - pts \<and> g w * f1 w \<noteq> 0"
+        thus "g w / f1 w = h w" using h_f1(6)
+          by (auto simp: divide_simps)
+      qed
+      finally show "is_pole h z" .
+    qed
+
+    have "h' analytic_on {z}" if "z \<in> A" for z
+    proof (cases "z \<in> pts")
+      case False
+      moreover have "open (A - pts)"
+        by (rule open_diff_pts) auto
+      ultimately have "(\<lambda>z. inverse (h z)) analytic_on {z}"
+        using that h_f1(1,2,5) \<open>open (A - pts)\<close> analytic_at False
+        by (intro analytic_intros) (auto simp: f1_eq_0_iff)
+      also have "eventually (\<lambda>z. z \<in> A - pts) (nhds z)"
+        using that False \<open>open (A - pts)\<close> by (intro eventually_nhds_in_open) auto
+      hence "(\<lambda>z. inverse (h z)) analytic_on {z} \<longleftrightarrow> h' analytic_on {z}"
+        by (intro analytic_at_cong) (auto elim!: eventually_mono simp: h'_def)
+      finally show ?thesis .
+    next
+      case True
+      have "(\<lambda>w. if w = z then 0 else inverse (h w)) holomorphic_on (A - (pts - {z}))"
+      proof (rule is_pole_inverse_holomorphic)
+        from True have "A - (pts - {z}) - {z} = A - pts"
+          by auto
+        thus "h holomorphic_on A - (pts - {z}) - {z}"
+          using h_f1(1) by simp
+      next
+        show "open (A - (pts - {z}))"
+          by (rule open_diff_pts) auto
+      next
+        have "is_pole g z"
+          using True that by (simp add: is_pole_iff)
+        thus "is_pole h z"
+          using is_pole_h that by auto
+      next
+        show "\<forall>w\<in>A-(pts-{z})-{z}. h w \<noteq> 0"
+          using h_f1(5) by auto
+      qed
+      also have "?this \<longleftrightarrow> h' holomorphic_on A - (pts - {z})"
+      proof (intro holomorphic_cong refl)
+        fix w assume w: "w \<in> A - (pts - {z})"
+        show "(if w = z then 0 else inverse (h w)) = h' w"
+          using True w by (cases "w = z") (auto simp: h'_def)
+      qed
+      finally have "h' holomorphic_on A - (pts - {z})" .
+      moreover have "z \<in> A - (pts - {z})" "open (A - (pts - {z}))"
+        using True that by (auto intro!: open_diff_pts)
+      ultimately show "h' analytic_on {z}"
+        using analytic_at by blast
+    qed
+    hence h': "h' analytic_on A"
+      using analytic_on_analytic_at by blast
+  
+    have h'_eq_0_iff: "h' w = 0 \<longleftrightarrow> is_pole g w" if "w \<in> A" for w
+      using that h_f1(5) is_pole_iff[of w] by (auto simp: h'_def)
+ 
+    obtain h'' f2 where h''_f2:
+       "h'' holomorphic_on A" "f2 holomorphic_on UNIV"
+       "\<forall>z. f2 z = 0 \<longleftrightarrow> (\<forall>z\<in>A. h' z = 0) \<or> (z \<in> A \<and> h' z = 0)"
+       "\<forall>z\<in>A. h' z = 0 \<longrightarrow> zorder f2 z = zorder h' z"
+       "\<forall>z\<in>A. h'' z \<noteq> 0" "\<forall>z\<in>A. h' z = h'' z * f2 z"
+    proof (rule weierstrass_factorization[of h' A])
+      show "open A" "connected A"
+        by fact+
+      show "h' holomorphic_on A"
+        using h' \<open>open A\<close> by (simp add: analytic_on_open)
+      show "\<not>z islimpt {w\<in>A. h' w = 0}" if "z \<in> frontier A" for z
+      proof
+        assume "z islimpt {w\<in>A. h' w = 0}"
+        also have "{w\<in>A. h' w = 0} = pts"
+          by (auto simp: h'_eq_0_iff pts_def)
+        finally have "z islimpt {w \<in> A. g w = 0 \<or> is_pole g w}"
+          by (rule islimpt_subset) (auto simp: pts_def)
+        thus False using no_limpt[of z] that
+          by blast
+      qed
+    qed blast
+  
+    show ?thesis
+    proof (rule that[of "\<lambda>w. inverse (h'' w)" f1 f2]; (intro ballI allI impI)?)
+      show "(\<lambda>w. inverse (h'' w)) holomorphic_on A"
+        using h''_f2(1,2,5) by (intro holomorphic_intros) auto
+    next
+      show "f1 holomorphic_on UNIV" "f2 holomorphic_on UNIV"
+        by fact+
+    next
+      show "f1 z = 0 \<longleftrightarrow> \<not> is_pole g z \<and> g z = 0" if "z \<in> A" for z
+        using that by (subst f1_eq_0_iff) (auto simp: pts_def)
+    next
+      show "f2 z = 0 \<longleftrightarrow> is_pole g z" if "z \<in> A" for z
+      proof -
+        have "\<not>(\<forall>z\<in>A. h' z = 0)"
+          using False h''_f2(6) h_f1(6) h'_eq_0_iff is_pole_iff by auto
+        hence "f2 z = 0 \<longleftrightarrow> h' z = 0"
+          using h''_f2(3) that by auto
+        also have "\<dots> \<longleftrightarrow> is_pole g z"
+          using that by (simp add: is_pole_iff h'_eq_0_iff)
+        finally show ?thesis .
+      qed
+    next
+      show "zorder f1 z = zorder g z" if "z \<in> A" "\<not>is_pole g z" for z
+        using h_f1(4) that by (auto simp: pts_def)
+    next
+      show "zorder f2 z = -zorder g z" if "z \<in> A" "is_pole g z" for z
+      proof -
+        have "zorder f2 z = zorder h' z"
+          using h''_f2(4) that h'_eq_0_iff[of z] is_pole_iff[of z] by auto
+        also have "\<dots> = zorder (\<lambda>w. inverse (h w)) z"
+          using that by (intro zorder_cong eventually_mono[OF ev]) (auto simp: h'_def)
+        also have "\<dots> = -zorder h z"
+        proof (intro zorder_inverse)
+          have "is_pole h z"
+            using that is_pole_iff[of z] is_pole_h[of z] by auto
+          thus "not_essential h z"
+            by force
+          show "frequently (\<lambda>w. h w \<noteq> 0) (at z)"
+            using non_zero_neighbour_pole[OF \<open>is_pole h z\<close>] eventually_frequently by force
+        qed (use that in \<open>auto intro!: isolated_h simp: pts_def\<close>)
+        also have "zorder f1 z = 0"
+        proof (rule zorder_eq_0I)
+          show "f1 analytic_on {z}"
+            using that h_f1(2) holomorphic_on_imp_analytic_at by blast
+          show "f1 z \<noteq> 0"
+            using that h_f1(3) False by (auto simp: pts_def)
+        qed
+        hence "zorder h z = zorder f1 z + zorder h z"
+          by simp
+        also have "\<dots> = zorder (\<lambda>w. f1 w * h w) z"
+        proof (rule zorder_times [symmetric])
+          have "f1 analytic_on {z}"
+            using that h_f1(2) holomorphic_on_imp_analytic_at by blast
+          thus "isolated_singularity_at f1 z" "not_essential f1 z"
+            using isolated_singularity_at_analytic not_essential_analytic by blast+
+          show "isolated_singularity_at h z"
+            using that by (intro isolated_h) (auto simp: pts_def)
+          have "is_pole h z"
+            using is_pole_iff[of z] that by (intro is_pole_h) auto
+          thus "not_essential h z"
+            by force
+          have "z \<in> A"
+            using that by auto
+          have "eventually (\<lambda>w. g w \<noteq> 0) (at z)"
+            using non_zero_neighbour_pole[of g z] that by auto
+          hence "eventually (\<lambda>w. f1 w * h w \<noteq> 0) (at z)"
+            using ev[OF \<open>z \<in> A\<close>]  by eventually_elim (use h_f1(6) in auto)
+          thus "frequently (\<lambda>w. f1 w * h w \<noteq> 0) (at z)"
+            using eventually_frequently by force
+        qed
+        also have "\<dots> = zorder g z"
+        proof (rule zorder_cong)
+          have "eventually (\<lambda>w. w \<in> A - pts) (at z)"
+            using ev[of z] that by auto
+          thus "eventually (\<lambda>w. f1 w * h w = g w) (at z)"
+            by eventually_elim (use h_f1(6) in auto)
+        qed auto
+        finally show ?thesis .
+      qed
+    next
+      show "inverse (h'' z) \<noteq> 0" if "z \<in> A" for z
+        using h''_f2(5) that by auto
+    next
+      show "g z = inverse (h'' z) * f1 z / f2 z" if z: "z \<in> A" for z
+      proof (cases "is_pole g z")
+        case False
+        have *: "g z = h z * f1 z" "h' z = h'' z * f2 z" "h'' z \<noteq> 0" "h z \<noteq> 0"
+          using that h''_f2(5,6) h_f1(5,6) False unfolding pts_def by blast+
+        have "g z = h z * f1 z"
+          by fact
+        also have "\<dots> = f1 z / h' z"
+          using * that False by (simp add: h'_def field_simps pts_def)
+        also have "h' z = h'' z * f2 z"
+          by fact
+        also have "f1 z / (h'' z * f2 z) = inverse (h'' z) * f1 z / f2 z"
+          by (simp add: divide_inverse_commute)
+        finally show ?thesis .
+      next
+        case True
+        have "\<not>g \<midarrow>z\<rightarrow> g z"
+          using True at_neq_bot is_pole_def not_tendsto_and_filterlim_at_infinity by blast
+        with mero and z and True have "g z = 0"
+          by (auto simp: nicely_meromorphic_on_def)
+        moreover have "f2 z = 0"
+          using True z by (simp add: h''_f2(3) h'_eq_0_iff)
+        ultimately show ?thesis by simp
+      qed
+    qed
+  qed
+qed
+
+text \<open>
+  Again, we derive an easier version for functions meromorphic on the entire complex plane.
+\<close>
+theorem weierstrass_factorization_meromorphic_UNIV:
+  assumes "g nicely_meromorphic_on UNIV" 
+  obtains h f1 f2 where
+    "h holomorphic_on UNIV" "f1 holomorphic_on UNIV" "f2 holomorphic_on UNIV"
+    "\<forall>z. f1 z = 0 \<longleftrightarrow> \<not>is_pole g z \<and> g z = 0"
+    "\<forall>z. f2 z = 0 \<longleftrightarrow> is_pole g z"
+    "\<forall>z. \<not>is_pole g z \<longrightarrow> zorder f1 z = zorder g z"
+    "\<forall>z. is_pole g z \<longrightarrow> zorder f2 z = -zorder g z"
+    "\<forall>z. h z \<noteq> 0"
+    "\<forall>z. g z = h z * f1 z / f2 z"
+proof (rule weierstrass_factorization_meromorphic)
+  show "g nicely_meromorphic_on UNIV"
+    by fact
+  show "connected (UNIV :: complex set)"
+    by (simp add: Convex.connected_UNIV)
+  show "\<not> z islimpt {w \<in> UNIV. g w = 0 \<or> is_pole g w}" if "z \<in> frontier UNIV" for z
+    using that by simp
+  show "open (UNIV :: complex set)"
+    by simp
+qed auto
+
+end
diff -r 7793e3161d2b -r b5cb8d56339f src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Mar 20 12:26:52 2024 +0100
+++ b/src/HOL/Library/Library.thy	Wed Mar 20 20:45:36 2024 +0100
@@ -78,6 +78,7 @@
   Quotient_Syntax
   Quotient_Type
   Ramsey
+  Real_Mod
   Reflection
   Rewrite
   Saturated
diff -r 7793e3161d2b -r b5cb8d56339f src/HOL/Library/Real_Mod.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Real_Mod.thy	Wed Mar 20 20:45:36 2024 +0100
@@ -0,0 +1,238 @@
+(*
+  File:     HOL/Library/Real_Mod.thy
+  Authors:  Manuel Eberl, University of Innsbruck
+*)
+section \<open>Modulo and congruence on the reals\<close>
+theory Real_Mod
+  imports Complex_Main
+begin
+
+definition rmod :: "real \<Rightarrow> real \<Rightarrow> real" (infixl "rmod" 70) where
+  "x rmod y = x - \<bar>y\<bar> * of_int \<lfloor>x / \<bar>y\<bar>\<rfloor>"
+
+lemma rmod_conv_frac: "y \<noteq> 0 \<Longrightarrow> x rmod y = frac (x / \<bar>y\<bar>) * \<bar>y\<bar>"
+  by (simp add: rmod_def frac_def algebra_simps)
+
+lemma rmod_conv_frac': "x rmod y = (if y = 0 then x else frac (x / \<bar>y\<bar>) * \<bar>y\<bar>)"
+  by (simp add: rmod_def frac_def algebra_simps)
+
+lemma rmod_rmod [simp]: "(x rmod y) rmod y = x rmod y"
+  by (simp add: rmod_conv_frac')
+
+lemma rmod_0_right [simp]: "x rmod 0 = x"
+  by (simp add: rmod_def)
+
+lemma rmod_less: "m > 0 \<Longrightarrow> x rmod m < m"
+  by (simp add: rmod_conv_frac' frac_lt_1)
+
+lemma rmod_less_abs: "m \<noteq> 0 \<Longrightarrow> x rmod m < \<bar>m\<bar>"
+  by (simp add: rmod_conv_frac' frac_lt_1)
+
+lemma rmod_le: "m > 0 \<Longrightarrow> x rmod m \<le> m"
+  by (intro less_imp_le rmod_less)
+
+lemma rmod_nonneg: "m \<noteq> 0 \<Longrightarrow> x rmod m \<ge> 0"
+  unfolding rmod_def
+  by (metis abs_le_zero_iff diff_ge_0_iff_ge floor_divide_lower linorder_not_le mult.commute)
+
+lemma rmod_unique:
+  assumes "z \<in> {0..<\<bar>y\<bar>}" "x = z + of_int n * y"
+  shows   "x rmod y = z"
+proof -
+  have "(x - z) / y = of_int n"
+    using assms by auto
+  hence "(x - z) / \<bar>y\<bar> = of_int ((if y > 0 then 1 else -1) * n)"
+    using assms(1) by (cases y "0 :: real" rule: linorder_cases) (auto split: if_splits)
+  also have "\<dots> \<in> \<int>"
+    by auto
+  finally have "frac (x / \<bar>y\<bar>) = z / \<bar>y\<bar>"
+    using assms(1) by (subst frac_unique_iff) (auto simp: field_simps)
+  thus ?thesis
+    using assms(1) by (auto simp: rmod_conv_frac')
+qed
+
+lemma rmod_0 [simp]: "0 rmod z = 0"
+  by (simp add: rmod_def)
+
+lemma rmod_add: "(x rmod z + y rmod z) rmod z = (x + y) rmod z"
+proof (cases "z = 0")
+  case [simp]: False
+  show ?thesis
+  proof (rule sym, rule rmod_unique)
+    define n where "n = (if z > 0 then 1 else -1) * (\<lfloor>x / \<bar>z\<bar>\<rfloor> + \<lfloor>y / \<bar>z\<bar>\<rfloor> +
+       \<lfloor>(x + y - (\<bar>z\<bar> * real_of_int \<lfloor>x / \<bar>z\<bar>\<rfloor> + \<bar>z\<bar> * real_of_int \<lfloor>y / \<bar>z\<bar>\<rfloor>)) / \<bar>z\<bar>\<rfloor>)"
+    show "x + y = (x rmod z + y rmod z) rmod z + real_of_int n * z"
+      by (simp add: rmod_def algebra_simps n_def)
+  qed (auto simp: rmod_less_abs rmod_nonneg)
+qed auto
+
+lemma rmod_diff: "(x rmod z - y rmod z) rmod z = (x - y) rmod z"
+proof (cases "z = 0")
+  case [simp]: False
+  show ?thesis
+  proof (rule sym, rule rmod_unique)
+    define n where "n = (if z > 0 then 1 else -1) * (\<lfloor>x / \<bar>z\<bar>\<rfloor> +
+      \<lfloor>(x + \<bar>z\<bar> * real_of_int \<lfloor>y / \<bar>z\<bar>\<rfloor> - (y + \<bar>z\<bar> * real_of_int \<lfloor>x / \<bar>z\<bar>\<rfloor>)) / \<bar>z\<bar>\<rfloor> - \<lfloor>y / \<bar>z\<bar>\<rfloor>)"
+    show "x - y = (x rmod z - y rmod z) rmod z + real_of_int n * z"
+      by (simp add: rmod_def algebra_simps n_def)
+  qed (auto simp: rmod_less_abs rmod_nonneg)
+qed auto
+
+lemma rmod_self [simp]: "x rmod x = 0"
+  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)
+
+lemma rmod_self_multiple_int [simp]: "(of_int n * x) rmod x = 0"
+  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)
+
+lemma rmod_self_multiple_nat [simp]: "(of_nat n * x) rmod x = 0"
+  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)
+
+lemma rmod_self_multiple_numeral [simp]: "(numeral n * x) rmod x = 0"
+  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)
+
+lemma rmod_self_multiple_int' [simp]: "(x * of_int n) rmod x = 0"
+  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)
+
+lemma rmod_self_multiple_nat' [simp]: "(x * of_nat n) rmod x = 0"
+  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)
+
+lemma rmod_self_multiple_numeral' [simp]: "(x * numeral n) rmod x = 0"
+  by (cases x "0 :: real" rule: linorder_cases) (auto simp: rmod_conv_frac)
+
+lemma rmod_idem [simp]: "x \<in> {0..<\<bar>y\<bar>} \<Longrightarrow> x rmod y = x"
+  by (rule rmod_unique[of _ _ _ 0]) auto
+
+
+
+definition rcong :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" (\<open>(1[_ = _] '(' rmod _'))\<close>) where
+  "[x = y] (rmod m) \<longleftrightarrow> x rmod m = y rmod m"
+
+named_theorems rcong_intros
+
+lemma rcong_0_right [simp]: "[x = y] (rmod 0) \<longleftrightarrow> x = y"
+  by (simp add: rcong_def)
+
+lemma rcong_0_iff: "[x = 0] (rmod m) \<longleftrightarrow> x rmod m = 0"
+  and rcong_0_iff': "[0 = x] (rmod m) \<longleftrightarrow> x rmod m = 0"
+  by (simp_all add: rcong_def)
+
+lemma rcong_refl [simp, intro!, rcong_intros]: "[x = x] (rmod m)"
+  by (simp add: rcong_def)
+
+lemma rcong_sym: "[y = x] (rmod m) \<Longrightarrow> [x = y] (rmod m)"
+  by (simp add: rcong_def)
+
+lemma rcong_sym_iff: "[y = x] (rmod m) \<longleftrightarrow> [x = y] (rmod m)"
+  unfolding rcong_def by (simp add: eq_commute del: rmod_idem)
+
+lemma rcong_trans [trans]: "[x = y] (rmod m) \<Longrightarrow> [y = z] (rmod m) \<Longrightarrow> [x = z] (rmod m)"
+  by (simp add: rcong_def)
+
+lemma rcong_add [rcong_intros]:
+  "[a = b] (rmod m) \<Longrightarrow> [c = d] (rmod m) \<Longrightarrow> [a + c = b + d] (rmod m)"
+  unfolding rcong_def using rmod_add by metis
+
+lemma rcong_diff [rcong_intros]:
+  "[a = b] (rmod m) \<Longrightarrow> [c = d] (rmod m) \<Longrightarrow> [a - c = b - d] (rmod m)"
+  unfolding rcong_def using rmod_diff by metis
+
+lemma rcong_uminus [rcong_intros]:
+  "[a = b] (rmod m) \<Longrightarrow> [-a = -b] (rmod m)"
+  using rcong_diff[of 0 0 m a b] by simp
+
+lemma rcong_uminus_uminus_iff [simp]: "[-x = -y] (rmod m) \<longleftrightarrow> [x = y] (rmod m)"
+  using rcong_uminus minus_minus by metis
+
+lemma rcong_uminus_left_iff: "[-x = y] (rmod m) \<longleftrightarrow> [x = -y] (rmod m)"
+  using rcong_uminus minus_minus by metis
+
+lemma rcong_add_right_cancel [simp]: "[a + c = b + c] (rmod m) \<longleftrightarrow> [a = b] (rmod m)"
+  using rcong_add[of a b m c c] rcong_add[of "a + c" "b + c" m "-c" "-c"] by auto
+
+lemma rcong_add_left_cancel [simp]: "[c + a = c + b] (rmod m) \<longleftrightarrow> [a = b] (rmod m)"
+  by (subst (1 2) add.commute) simp
+
+lemma rcong_diff_right_cancel [simp]: "[a - c = b - c] (rmod m) \<longleftrightarrow> [a = b] (rmod m)"
+  by (metis rcong_add_left_cancel uminus_add_conv_diff)
+
+lemma rcong_diff_left_cancel [simp]: "[c - a = c - b] (rmod m) \<longleftrightarrow> [a = b] (rmod m)"
+  by (metis minus_diff_eq rcong_diff_right_cancel rcong_uminus_uminus_iff)
+
+lemma rcong_rmod_right_iff [simp]: "[a = (b rmod m)] (rmod m) \<longleftrightarrow> [a = b] (rmod m)"
+  and rcong_rmod_left_iff [simp]: "[(a rmod m) = b] (rmod m) \<longleftrightarrow> [a = b] (rmod m)"
+  by (simp_all add: rcong_def)
+
+lemma rcong_rmod_left [rcong_intros]: "[a = b] (rmod m) \<Longrightarrow> [(a rmod m) = b] (rmod m)"
+  and rcong_rmod_right [rcong_intros]: "[a = b] (rmod m) \<Longrightarrow> [a = (b rmod m)] (rmod m)"
+  by simp_all
+
+lemma rcong_mult_of_int_0_left_left [rcong_intros]: "[0 = of_int n * m] (rmod m)"
+  and rcong_mult_of_int_0_right_left [rcong_intros]: "[0 = m * of_int n] (rmod m)"
+  and rcong_mult_of_int_0_left_right [rcong_intros]: "[of_int n * m = 0] (rmod m)"
+  and rcong_mult_of_int_0_right_right [rcong_intros]: "[m * of_int n = 0] (rmod m)"
+  by (simp_all add: rcong_def)
+
+lemma rcong_altdef: "[a = b] (rmod m) \<longleftrightarrow> (\<exists>n. b = a + of_int n * m)"
+proof (cases "m = 0")
+  case False
+  show ?thesis
+  proof
+    assume "[a = b] (rmod m)"
+    hence "[a - b = b - b] (rmod m)"
+      by (intro rcong_intros)
+    hence "(a - b) rmod m = 0"
+      by (simp add: rcong_def)
+    then obtain n where "of_int n = (a - b) / \<bar>m\<bar>"
+      using False by (auto simp: rmod_conv_frac elim!: Ints_cases)
+    thus "\<exists>n. b = a + of_int n * m" using False
+      by (intro exI[of _ "if m > 0 then -n else n"]) (auto simp: field_simps)
+  next
+    assume "\<exists>n. b = a + of_int n * m"
+    then obtain n where n: "b = a + of_int n * m"
+      by auto
+    have "[a + 0 = a + of_int n * m] (rmod m)"
+      by (intro rcong_intros)
+    with n show "[a = b] (rmod m)"
+      by simp
+  qed
+qed auto
+
+lemma rcong_conv_diff_rmod_eq_0: "[x = y] (rmod m) \<longleftrightarrow> (x - y) rmod m = 0"
+  by (metis cancel_comm_monoid_add_class.diff_cancel rcong_0_iff rcong_diff_right_cancel)
+
+lemma rcong_imp_eq:
+  assumes "[x = y] (rmod m)" "\<bar>x - y\<bar> < \<bar>m\<bar>"
+  shows   "x = y"
+proof -
+  from assms obtain n where n: "y = x + of_int n * m"
+    unfolding rcong_altdef by blast
+  have "of_int \<bar>n\<bar> * \<bar>m\<bar> = \<bar>x - y\<bar>"
+    by (simp add: n abs_mult)
+  also have "\<dots> < 1 * \<bar>m\<bar>"
+    using assms(2) by simp
+  finally have "n = 0"
+    by (subst (asm) mult_less_cancel_right) auto
+  with n show ?thesis
+    by simp
+qed
+
+lemma rcong_mult_modulus:
+  assumes "[a = b] (rmod (m / c))" "c \<noteq> 0"
+  shows   "[a * c = b * c] (rmod m)"
+proof -
+  from assms obtain k where k: "b = a + of_int k * (m / c)"
+    by (auto simp: rcong_altdef)
+  have "b * c = (a + of_int k * (m / c)) * c"
+    by (simp only: k)
+  also have "\<dots> = a * c + of_int k * m"
+    using assms(2) by (auto simp: divide_simps)
+  finally show ?thesis
+    unfolding rcong_altdef by blast
+qed
+
+lemma rcong_divide_modulus:
+  assumes "[a = b] (rmod (m * c))" "c \<noteq> 0"
+  shows   "[a / c = b / c] (rmod m)"
+  using rcong_mult_modulus[of a b m "1 / c"] assms by (auto simp: field_simps)
+
+end
\ No newline at end of file
diff -r 7793e3161d2b -r b5cb8d56339f src/Pure/Build/build_benchmark.scala
--- a/src/Pure/Build/build_benchmark.scala	Wed Mar 20 12:26:52 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala	Wed Mar 20 20:45:36 2024 +0100
@@ -18,9 +18,10 @@
     ssh: SSH.System = SSH.Local,
     isabelle_home: Path = Path.current,
   ): String = {
-    val options = Options.Spec.eq("build_hostname", host.name) :: host.options
+    val benchmark_options =
+      List(Options.Spec.eq("build_hostname", host.name), Options.Spec("build_database_server"))
     ssh.bash_path(Isabelle_Tool.exe(isabelle_home)) + " build_benchmark" +
-      Options.Spec.bash_strings(options, bg = true)
+      Options.Spec.bash_strings(benchmark_options ::: host.options, bg = true)
   }
 
   def benchmark_requirements(options: Options, progress: Progress = new Progress): Unit = {
diff -r 7793e3161d2b -r b5cb8d56339f src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Wed Mar 20 12:26:52 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Wed Mar 20 20:45:36 2024 +0100
@@ -576,6 +576,7 @@
       val next_nodes =
         for {
           task <- state.next_ready
+          if graph.defined(task.name)
           node = graph.get_node(task.name)
           if hostname == node.node_info.hostname
         } yield node
@@ -1010,8 +1011,8 @@
 
     /* global resources with common close() operation */
 
-    private final lazy val _log_store: Build_Log.Store = Build_Log.store(build_options)
-    private final lazy val _log_database: SQL.Database =
+    private final val _log_store: Build_Log.Store = Build_Log.store(build_options)
+    private final val _log_database: SQL.Database =
       try {
         val db = _log_store.open_database(server = this.server)
         _log_store.init_database(db)
@@ -1149,7 +1150,9 @@
           val elapsed = Time.now() - start
 
           val timing_msg = if (elapsed.is_relevant) " (took " + elapsed.message + ")" else ""
-          progress.echo_if(_schedule.deviation(schedule).minutes > 1, schedule.message + timing_msg)
+          progress.echo_if(
+            _schedule.deviation(schedule).minutes > 1 && schedule.duration >= Time.seconds(1),
+            schedule.message + timing_msg)
 
           _schedule = schedule
           _schedule.next(hostname, state)