Theory HOL-Complex_Analysis.Weierstrass_Factorization
section ‹The Weierstra\ss\ Factorisation Theorem›
theory Weierstrass_Factorization
imports Meromorphic
begin
no_notation Infinite_Set_Sum.abs_summable_on (infix ‹abs'_summable'_on› 50)
subsection ‹The elementary factors›
text ‹
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.
›
definition weierstrass_factor :: "nat ⇒ complex ⇒ complex" where
"weierstrass_factor n z = (1 - z) * exp (∑k=1..n. z ^ k / of_nat k)"
lemma weierstrass_factor_continuous_on [continuous_intros]:
"continuous_on A f ⟹ continuous_on A (λ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 ⟹ (λ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 ⟹ (λ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 ⟷ z = 1"
by (simp add: weierstrass_factor_def)
lemma zorder_weierstrass_factor [simp]: "zorder (weierstrass_factor n) 1 = 1"
proof (rule zorder_eqI)
show "(λz. -exp (∑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 has_zorder_weierstrass_factor [zorder_intros]: "has_zorder (weierstrass_factor n) 1 1"
by (rule has_zorderI)
(auto intro!: analytic_on_imp_meromorphic_on analytic_intros eventually_neq_at_within)
lemma has_field_derivative_weierstrass_factor:
assumes "(f has_field_derivative f') (at z within A)"
assumes "f z ≠ 1"
shows "((λz. weierstrass_factor n (f z)) has_field_derivative
(f' * weierstrass_factor n (f z) * f z ^ n / (f z - 1)))
(at z within A)"
proof -
define W where "W = weierstrass_factor n (f z)"
have "((λz. weierstrass_factor n (f z)) has_field_derivative
(f' * ((∑n=1..n. f z ^ (n - 1)) * W - exp (∑k=1..n. f z ^ k / of_nat k)))) (at z within A)"
unfolding weierstrass_factor_def W_def
by (auto intro!: derivative_eq_intros assms(1) simp: algebra_simps
simp flip: sum_distrib_left sum_distrib_right)
also have "exp (∑k=1..n. f z ^ k / of_nat k) = W / (1 - f z)"
using ‹f z ≠ 1› by (auto simp: weierstrass_factor_def W_def)
also have "(∑n=1..n. f z ^ (n - 1)) = (∑k<n. f z ^ k)"
by (rule sum.reindex_bij_witness[of _ "λn. n+1" "λn. n-1"]) auto
also have "… = (f z ^ n - 1) / (f z - 1)"
by (subst geometric_sum) (use ‹f z ≠ 1› in auto)
also have "(f z ^ n - 1) / (f z - 1) * W - W / (1 - f z) = W * f z ^ n / (f z - 1)"
using ‹f z ≠ 1› by (auto simp: divide_simps) (auto simp: algebra_simps)?
finally show ?thesis
unfolding W_def by (simp add: mult_ac)
qed
lemma weierstrass_factor_bound:
assumes "norm z ≤ 1 / 2"
shows "norm (weierstrass_factor n z - 1) ≤ 3 * norm z ^ Suc n"
proof (cases "n = 0 ∨ 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 ≠ 1" "n > 0" "z ≠ 0"
by auto
have "summable (λ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 ⟷ summable (λk. norm z ^ Suc n * (norm z ^ k / real (k + Suc n)))"
by (simp add: power_add mult_ac)
also have "… ⟷ summable (λk. norm z ^ k / real (k + Suc n))"
by (subst summable_cmult_iff) (use ‹z ≠ 0› in auto)
finally have summable: "summable (λk. norm z ^ k / real (k + Suc n))" .
have "(λ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 "(λk. z ^ (k + Suc n) / of_nat (k + Suc n)) sums (- Ln (1 - z) - (∑k<Suc n. z ^ k / of_nat k))"
by (intro sums_split_initial_segment)
also have "(∑k<Suc n. z ^ k / of_nat k) = (∑k=1..n. z ^ k / of_nat k)"
by (intro sum.mono_neutral_right) auto
finally have "norm (ln (1 - z) + (∑k=1..n. z ^ k / of_nat k)) =
norm (∑k. z ^ (k + Suc n) / of_nat (k + Suc n))"
by (simp add: sums_iff norm_uminus_minus)
also have "… ≤ (∑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 "… = (∑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 "… = norm z ^ Suc n * (∑k. norm z ^ k / real (k + Suc n))"
by (intro suminf_mult summable)
also have "… ≤ norm z ^ Suc n * (1 / (1 - norm z))"
proof (intro mult_left_mono[OF sums_le])
show "(λk. norm z ^ k / real (k + Suc n)) sums (∑k. norm z ^ k / real (k + Suc n))"
using summable by blast
show "(λ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)) ≤ 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 "… = 2 * norm z ^ Suc n"
by simp
finally have norm_le: "norm (ln (1 - z) + (∑k=1..n. z ^ k / of_nat k)) ≤ 2 * norm z ^ Suc n" .
also have "… ≤ 2 * norm z ^ 2"
using ‹n > 0› assms by (intro mult_left_mono power_decreasing) auto
also have "… ≤ 2 * (1 / 2) ^ 2"
by (intro mult_left_mono assms power_mono) auto
finally have norm_le': "norm (ln (1 - z) + (∑k=1..n. z ^ k / of_nat k)) ≤ 1 / 2"
by (simp add: power2_eq_square)
have "weierstrass_factor n z = exp (ln (1 - z) + (∑k=1..n. z ^ k / of_nat k))"
using ‹z ≠ 1› by (simp add: exp_add weierstrass_factor_def)
also have "norm (… - 1) ≤ (3 / 2) * norm (ln (1 - z) + (∑k=1..n. z ^ k / of_nat k))"
by (intro norm_exp_bounds norm_le')
also have "… ≤ (3 / 2) * (2 * norm z ^ Suc n)"
by (intro mult_left_mono norm_le) auto
finally show ?thesis
by simp
qed
subsection ‹Infinite products of elementary factors›
text ‹
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).
›
locale weierstrass_product =
fixes a :: "'a ⇒ complex"
fixes p :: "'a ⇒ nat"
fixes I :: "'a set"
assumes a_nonzero: "⋀x. x ∈ I ⟹ a x ≠ 0"
assumes filterlim_a: "filterlim a at_infinity (inf cofinite (principal I))"
assumes summable_a_p: "⋀r. r > 0 ⟹ (λx. (r / norm (a x)) ^ Suc (p x)) summable_on I"
begin
text ‹
Due to the assumptions on \<^term>‹a›, every point can only occur a finite number of times.
Moreover, the range of \<^term>‹a› is a sparse set (i.e.\ it has no limit points) and is therefore
in particular a closed set.
›
lemma finite_occs_a: "finite (a -` {z} ∩ I)"
proof -
have "eventually (λn. norm (a n) > norm z) (inf cofinite (principal I))"
using filterlim_a by (metis filterlim_at_infinity_imp_norm_at_top filterlim_at_top_dense)
hence "finite {x ∈ I. norm (a x) ≤ norm z}"
by (auto simp: eventually_inf_principal eventually_cofinite not_less)
thus ?thesis
by (rule finite_subset [rotated]) auto
qed
lemma not_islimpt_range_a: "¬z islimpt a ` I"
proof -
define r where "r = norm z + 1"
define U where "U = ball (0::complex) r"
have "finite (U ∩ a ` I)"
proof -
have "eventually (λn. norm (a n) ≥ r) (inf cofinite (principal I))"
using filterlim_a by (metis filterlim_at_infinity_imp_norm_at_top filterlim_at_top)
hence "finite {x ∈ I. norm (a x) < r}"
by (auto simp: eventually_inf_principal eventually_cofinite not_le)
also have "{x∈I. norm (a x) < r} = a -` U ∩ I"
by (auto simp: U_def)
finally have "finite (a -` U ∩ I)" .
hence "finite (a ` (a -` U ∩ I))"
by (rule finite_imageI)
also have "a ` (a -` U ∩ I) = U ∩ a ` I"
by auto
finally show ?thesis .
qed
moreover have "open U" "z ∈ U"
by (auto simp: U_def r_def)
ultimately show ?thesis
unfolding islimpt_eq_acc_point by blast
qed
lemma closed_range_a: "closed (a ` I)"
using not_islimpt_range_a unfolding closed_limpt by blast
text ‹
We construct the product by multiplying the Weierstra\ss\ factors with the appropriate weight.
›
definition f :: "complex ⇒ complex" where
"f z = (∏⇩∞x∈I. weierstrass_factor (p x) (z / a x))"
text ‹
The product converges absolutely.
›
lemma abs_multipliable: "(λx. weierstrass_factor (p x) (z / a x)) abs_multipliable_on I"
unfolding abs_multipliable_on_iff_summable_on
proof -
define I1 where "I1 = {x∈I. norm (z / a x) ≤ 1 / 2}"
define I2 where "I2 = {x∈I. norm (z / a x) > 1 / 2}"
have "finite I2"
proof -
have "eventually (λx. norm (a x) ≥ 2 * norm z) (inf cofinite (principal I))"
using filterlim_a unfolding filterlim_at_infinity_conv_norm_at_top filterlim_at_top
by blast
hence "finite {x ∈ I. norm (a x) < 2 * norm z}"
by (auto simp: eventually_inf_principal eventually_cofinite not_le)
thus "finite I2"
by (rule finite_subset [rotated]) (auto simp: I2_def norm_divide divide_simps)
qed
have "(λn. weierstrass_factor (p n) (z / a n) - 1) abs_summable_on (I1 ∪ I2)"
proof (rule summable_on_Un_disjoint)
show "(λx. weierstrass_factor (p x) (z / a x) - 1) abs_summable_on I2"
by (rule summable_on_finite) fact
next
show "(λx. weierstrass_factor (p x) (z / a x) - 1) abs_summable_on I1"
proof (rule summable_on_comparison_test)
have "(λx. 3 * norm (z / a x) ^ Suc (p x)) summable_on I"
using summable_on_cmult_right[OF summable_a_p[of "norm z"], of 3]
by (cases "z = 0") (auto simp: norm_divide)
thus "(λx. 3 * norm (z / a x) ^ Suc (p x)) summable_on I1"
by (rule summable_on_subset) (auto simp: I1_def)
next
fix x assume x: "x ∈ I1"
hence "norm (z / a x) ≤ 1 / 2"
by (auto simp: norm_divide I1_def)
thus "norm (weierstrass_factor (p x) (z / a x) - 1) ≤ 3 * cmod (z / a x) ^ Suc (p x)"
by (rule weierstrass_factor_bound)
qed auto
qed (auto simp: I1_def I2_def)
also have "I1 ∪ I2 = I"
by (auto simp: I1_def I2_def)
finally show "(λn. weierstrass_factor (p n) (z / a n) - 1) abs_summable_on I" .
qed
lemma multipliable: "(λx. weierstrass_factor (p x) (z / a x)) multipliable_on I"
using abs_multipliable by (rule abs_multipliable_multipliable)
lemma has_setprod: "((λx. weierstrass_factor (p x) (z / a x)) has_setprod f z) I"
using multipliable[of z] unfolding f_def by auto
text ‹
On compact sets, it converges uniformly.
›
context
fixes P
defines "P ≡ (λJ z. ∏x∈J. weierstrass_factor (p x) (z / a x))"
begin
lemma uniform_limit:
assumes "compact K"
shows "uniform_limit K P f (finite_subsets_at_top I)"
proof -
have *: "uniform_limit (cball 0 R) P f (finite_subsets_at_top I)" if "R > 0" for R
proof -
define I1 where "I1 = {x∈I. R ≤ norm (a x) / 2}"
show ?thesis
unfolding P_def f_def
proof (rule uniform_limit_infprod_M_test_strong)
show "finite (I - I1)"
proof -
have "eventually (λx. norm (a x) ≥ 2 * R) (inf cofinite (principal I))"
using filterlim_a unfolding filterlim_at_infinity_conv_norm_at_top filterlim_at_top
by blast
hence "finite {x ∈ I. norm (a x) < 2 * R}"
by (auto simp: eventually_inf_principal eventually_cofinite not_le)
thus "finite (I - I1)"
by (rule finite_subset [rotated]) (auto simp: I1_def norm_divide divide_simps)
qed
next
fix x z assume x: "x ∈ I1" and z: "z ∈ cball (0::complex) R"
from x z have "norm (weierstrass_factor (p x) (z / a x) - 1) ≤ 3 * (norm (z / a x)) ^ Suc (p x)"
by (intro weierstrass_factor_bound) (auto simp: norm_divide divide_simps I1_def)
also have "… = 3 * (norm z / norm (a x)) ^ Suc (p x)"
by (simp add: norm_divide)
also have "… ≤ 3 * (R / norm (a x)) ^ Suc (p x)"
by (intro mult_left_mono power_mono divide_right_mono) (use z in auto)
finally show "norm (weierstrass_factor (p x) (z / a x) - 1) ≤
3 * (R / norm (a x)) ^ Suc (p x)" by simp
next
show "(λx. 3 * (R / norm (a x)) ^ Suc (p x)) summable_on I1"
by (rule summable_on_cmult_right, rule summable_on_subset, rule summable_a_p)
(auto simp: I1_def ‹R > 0›)
next
fix x assume x: "x ∈ I - I1"
have "compact ((λz. weierstrass_factor (p x) (z / a x) - 1) ` cball 0 R)"
by (intro compact_continuous_image continuous_intros) (use x in ‹auto simp: a_nonzero›)
thus "bounded ((λz. weierstrass_factor (p x) (z / a x) - 1) ` cball 0 R)"
by (rule compact_imp_bounded)
qed
qed
from assms have "bounded K"
by (rule compact_imp_bounded)
then obtain R where R: "K ⊆ cball 0 R"
by (auto simp: bounded_iff cball_def)
show ?thesis
by (rule uniform_limit_on_subset[OF *[of "max R 1"]]) (use R in auto)
qed
text ‹
Since the factors are entire, so is the product.
›
lemma analytic [analytic_intros]: "f analytic_on A"
proof -
have "f analytic_on {z}" for z
proof -
define r where "r = norm z + 1"
have r: "r > 0"
by (auto simp: r_def add_nonneg_pos)
have "∀⇩F J in finite_subsets_at_top I. finite J ∧ J ⊆ I"
by (rule eventually_finite_subsets_at_top_weakI) auto
hence *: "∀⇩F J in finite_subsets_at_top I. continuous_on (cball 0 r) (P J) ∧ P J holomorphic_on ball 0 r"
by eventually_elim (auto simp: P_def a_nonzero intro!: continuous_intros holomorphic_intros)
have "f holomorphic_on ball 0 r" using r holomorphic_uniform_limit[OF * uniform_limit]
by auto
hence "f analytic_on ball 0 r"
by (simp add: analytic_on_open)
thus "f analytic_on {z}"
by (rule analytic_on_subset) (auto simp: r_def)
qed
thus "f analytic_on A"
by (metis analytic_on_analytic_at)
qed
lemma holomorphic [holomorphic_intros]: "f holomorphic_on A"
using analytic by (rule analytic_imp_holomorphic)
end
text ‹
The zeros of the product are precisely the numbers in the range of \<^term>‹a›.
›
lemma zero: "f z = 0 ⟷ z ∈ a ` I"
proof -
have *: "(λx. weierstrass_factor (p x) (z / a x)) strongly_multipliable_on I"
using abs_multipliable by (rule abs_multipliable_on_imp_strongly_multipliable_on)
show ?thesis
using has_setprod_eq_0_iff[OF * has_setprod] a_nonzero by auto
qed
lemma isolated_zero:
assumes "z ∈ a ` I"
shows "isolated_zero f z"
proof -
have "eventually (λz. f z ≠ 0) (at z)"
using not_islimpt_range_a[of z] by (auto simp: islimpt_iff_eventually zero)
moreover have "f ─z→ f z"
by (intro isContD analytic_at_imp_isCont analytic)
hence "f ─z→ 0"
using assms zero[of z] by auto
ultimately show ?thesis
by (auto simp: isolated_zero_def)
qed
text ‹
The multiplicity of each zero is the number of times it appears in the range of \<^term>‹a›.
›
theorem has_zorder: "has_zorder f z (card (a -` {z} ∩ I))"
proof -
define g where "g = (λz x. weierstrass_factor (p x) (z / a x))"
define I1 where "I1 = {x∈I. a x ≠ z}"
define I2 where "I2 = a -` {z} ∩ I"
have "finite I2"
using finite_occs_a[of z] unfolding I2_def .
hence prod2: "(g w has_setprod (∏x∈I2. g w x)) I2" for w
by (rule has_setprod_finite)
have "has_zorder (λw. ∏x∈I2. g w x) z (∑x∈I2. 1)"
proof (intro zorder_intros)
fix x assume x: "x ∈ I2"
have [simp]: "a x ≠ 0"
using a_nonzero[of x] x by (auto simp: I2_def)
have "has_zorder (λz. weierstrass_factor (p x) z) 1 1"
by (rule zorder_intros)
hence *: "has_zorder (λz. weierstrass_factor (p x) z) (1 / a x * z) 1"
using x by (auto simp: I2_def)
show "has_zorder (λz. g z x) z 1"
using has_zorder_compose_scale[OF *] by (simp add: g_def)
qed
hence zorder2: "has_zorder (λw. ∏x∈I2. g w x) z (card I2)"
by simp
have abs_mult1: "g w abs_multipliable_on I1" for w
by (rule abs_multipliable_on_subset[of _ I])
(use abs_multipliable in ‹auto simp: g_def I1_def›)
hence prod1: "(g w has_setprod (∏⇩∞x∈I1. g w x)) I1" for w
by (intro has_setprod_infprod abs_multipliable_multipliable)
have zorder1: "has_zorder (λw. ∏⇩∞x∈I1. g w x) z 0"
proof (rule analytic_imp_has_zorder_0)
show "(λw. infprod (g w) I1) analytic_on {z}"
proof -
interpret I1: weierstrass_product a p I1
proof
show "filterlim a at_infinity (inf cofinite (principal I1))"
by (intro filterlim_mono[OF filterlim_a] inf_mono) (auto simp: I1_def)
next
fix r :: real assume r: "r > 0"
show "(λx. (r / cmod (a x)) ^ Suc (p x)) summable_on I1"
by (rule summable_on_subset [OF summable_a_p[OF r]]) (auto simp: I1_def)
qed (auto simp: a_nonzero I1_def)
show ?thesis
using I1.analytic[of "{z}"] by (simp add: I1.f_def [abs_def] g_def)
qed
next
have "(∏⇩∞x∈I1. g z x) = 0 ⟷ (∃x∈I1. g z x = 0)"
by (rule has_setprod_eq_0_iff)
(use prod1 abs_mult1 in ‹auto intro: abs_multipliable_on_imp_strongly_multipliable_on›)
thus "infprod (g z) I1 ≠ 0"
by (auto simp: g_def I1_def)
qed
have "has_zorder (λw. (∏⇩∞x∈I1. g w x) * (∏x∈I2. g w x)) z (card I2)"
using has_zorder_mult[OF zorder1 zorder2 refl] by simp
also have "(λw. (∏⇩∞x∈I1. g w x) * (∏x∈I2. g w x)) = f"
proof
fix w :: complex
have "((λx. g w x) has_setprod ((∏⇩∞x∈I1. g w x) * (∏x∈I2. g w x))) (I1 ∪ I2)"
by (intro has_setprod_Un_disjoint prod1 prod2) (auto simp: I1_def I2_def)
also have "I1 ∪ I2 = I"
by (auto simp: I1_def I2_def)
finally show "(∏⇩∞x∈I1. g w x) * (∏x∈I2. g w x) = f w"
using has_setprod_unique[OF _ has_setprod[of w]] unfolding g_def by blast
qed
finally show ?thesis
by (simp add: I2_def)
qed
lemma zorder: "zorder f z = card (a -` {z} ∩ I)"
using has_zorder by (simp add: has_zorder_def)
text ‹
We also derive a nice form for the logarithmic derivative, which is a uniformly convergent sum.
›
lemma uniform_limit_logderiv:
assumes K: "compact K" "K ∩ a ` I = {}"
shows "uniform_limit K (λJ z. ∑x∈J. (z / a x) ^ p x / (z - a x)) (λz. deriv f z / f z)
(finite_subsets_at_top I)"
proof -
define g where "g = (λx z. weierstrass_factor (p x) (z / a x))"
have "uniform_limit K (λJ z. ∑x∈J. deriv (g x) z / g x z) (λz. deriv f z / f z)
(finite_subsets_at_top I)"
proof (rule logderiv_infprod_uniform_limit)
show "K ⊆ -(a ` I)"
using K by auto
show "compact K"
by fact
show "open (-a ` I)"
using closed_range_a by blast
show "g x holomorphic_on - a ` I" if "x ∈ I" for x
by (auto simp: g_def intro!: holomorphic_intros)
show "f z ≠ 0" if "z ∈ -a ` I" for z
using that by (auto simp: zero)
show "uniform_limit L (λJ x. ∏xa∈J. g xa x) f (finite_subsets_at_top I)" if "compact L" for L
unfolding g_def by (rule uniform_limit) fact
qed
also have "?this ⟷ uniform_limit K (λJ z. ∑x∈J. (z / a x) ^ p x / (z - a x)) (λz. deriv f z / f z)
(finite_subsets_at_top I)"
proof (rule uniform_limit_cong)
have "∀⇩F J in finite_subsets_at_top I. finite J ∧ J ⊆ I"
by (rule eventually_finite_subsets_at_top_weakI) auto
show "∀⇩F J in finite_subsets_at_top I.
∀z∈K. (∑x∈J. deriv (g x) z / g x z) = (∑x∈J. (z / a x) ^ p x / (z - a x))"
proof (intro eventually_finite_subsets_at_top_weakI ballI sum.cong refl)
fix J z x
assume J: "finite J" "J ⊆ I" and z: "z ∈ K" and x: "x ∈ J"
have neq: "z ≠ a x"
using J z x K by auto
have [simp]: "a x ≠ 0"
by (rule a_nonzero) (use J x in auto)
note [derivative_intros] = has_field_derivative_weierstrass_factor
have "((λz. g x z) has_field_derivative (g x z * (z / a x) ^ p x / (a x * (z / a x - 1)))) (at z)"
unfolding g_def using neq by (auto intro!: derivative_eq_intros simp: a_nonzero)
also have "(a x * (z / a x - 1)) = z - a x"
using neq by (simp add: field_simps)
finally have "deriv (g x) z = g x z * (z / a x) ^ p x / (z - a x)"
by (rule DERIV_imp_deriv)
also have "… / g x z = (z / a x) ^ p x / (z - a x)"
by (simp add: g_def)
finally show "deriv (g x) z / g x z = (z / a x) ^ p x / (z - a x)" .
qed
qed auto
finally show ?thesis .
qed
lemma has_sum_logderiv:
assumes "z ∉ a ` I"
shows "((λx. (z / a x) ^ p x / (z - a x)) has_sum (deriv f z / f z)) I"
proof -
have "uniform_limit {z} (λJ z. ∑x∈J. (z / a x) ^ p x / (z - a x)) (λz. deriv f z / f z)
(finite_subsets_at_top I)"
by (rule uniform_limit_logderiv) (use assms in auto)
thus ?thesis
by (simp add: has_sum_def)
qed
theorem logderiv_eq:
assumes "z ∉ a ` I"
shows "deriv f z / f z = (∑⇩∞x∈I. (z / a x) ^ p x / (z - a x))"
using has_sum_logderiv[OF assms] by (simp add: has_sum_iff)
end
text ‹
The following locale is the case where we take the product over a sequence of points
$(a_n)_{n\geq 0}$ with $|a_n|\to\infty$ and we choose $p(n) = n$, which is guaranteed to work.
›
locale weierstrass_product' =
fixes a :: "nat ⇒ complex"
assumes a_nonzero': "⋀n. a n ≠ 0"
assumes filterlim_a': "filterlim a at_infinity at_top"
begin
sublocale weierstrass_product a "λn. n" UNIV
proof
show "a n ≠ 0" for n :: nat
using a_nonzero' by auto
next
show "filterlim a at_infinity (inf cofinite (principal UNIV))"
using filterlim_a' by (simp add: cofinite_eq_sequentially)
next
fix r :: real assume r: "r > 0"
have "summable (λn. (r / norm (a n)) ^ Suc n)"
proof (rule summable_comparison_test_ev)
have "eventually (λ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 (λn. norm ((r / norm (a n)) ^ Suc n) ≤ (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 ‹r > 0› by (simp add: abs_mult)
also have "… ≤ (1 / 2) ^ Suc n"
using ‹r > 0› elim by (intro power_mono) (auto simp: divide_simps)
finally show ?case .
qed
next
show "summable (λn. (1 / 2) ^ Suc n :: real)"
unfolding summable_Suc_iff by (intro summable_geometric) auto
qed
thus "(λx. (r / norm (a x)) ^ Suc x) summable_on UNIV"
by (rule summable_nonneg_imp_summable_on) (use r in auto)
qed
end
subsection ‹Writing a quotient as an exponential›
text ‹
If two holomorphic functions ‹f› and ‹g› 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)$.
›
lemma holomorphic_zorder_factorization:
assumes "g holomorphic_on A" "open A" "connected A"
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ f z = 0 ⟷ g z = 0"
"⋀z. z ∈ A ⟹ zorder f z = zorder g z"
obtains h where "h holomorphic_on A" "⋀z. z ∈ A ⟹ h z ≠ 0" "⋀z. z ∈ A ⟹ g z = h z * f z"
proof (cases "∃z∈A. g z ≠ 0")
case False
show ?thesis
by (rule that[of "λ_. 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 = (λz. fps_nth (G z) (subdegree (G z)) / fps_nth (F z) (subdegree (F z)))"
define h where "h = (λz. if f z = 0 then c z else g z / f z)"
have ev_nonzero: "eventually (λw. g w ≠ 0 ∧ w ∈ A) (at z)" if "z ∈ A" for z
proof -
from True obtain z0 where z0: "z0 ∈ A" "g z0 ≠ 0"
by auto
show ?thesis
by (rule non_zero_neighbour_alt[where ?β = z0])
(use assms that z0 in ‹auto intro: simply_connected_imp_connected›)
qed
have g_ana: "g analytic_on {z}" if "z ∈ A" for z
using assms ‹open A› analytic_at that by blast
have f_ana: "f analytic_on {z}" if "z ∈ A" for z
using assms ‹open A› analytic_at that by blast
have F: "(λw. f (z + w)) has_fps_expansion F z" if "z ∈ A" for z
unfolding F_def by (rule analytic_at_imp_has_fps_expansion[OF f_ana[OF that]])
have G: "(λw. g (z + w)) has_fps_expansion G z" if "z ∈ A" for z
unfolding G_def by (rule analytic_at_imp_has_fps_expansion[OF g_ana[OF that]])
have [simp]: "G z ≠ 0" if "z ∈ A" for z
proof
assume "G z = 0"
hence "eventually (λ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 (λ_. 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 ≠ 0" if "z ∈ A" for z
proof
assume "F z = 0"
hence "eventually (λ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 (λ_. 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 ≠ 0" if "z ∈ A" for z
using that by (simp add: c_def)
have h: "h analytic_on {z} ∧ h z ≠ 0" if "z ∈ A" for z
proof -
show ?thesis
proof (cases "f z = 0")
case False
from False that have "(λz. g z / f z) analytic_on {z}"
by (intro analytic_intros g_ana f_ana) auto
also have "?this ⟷ h analytic_on {z}"
proof (rule analytic_at_cong)
have "eventually (λw. f w ≠ 0) (nhds z)"
using ev_nonzero[OF ‹z ∈ A›] unfolding eventually_at_filter
by eventually_elim (use False ‹z ∈ A› assms in auto)
thus "eventually (λ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 ≠ 0"
using that assms by (simp add: h_def)
ultimately show ?thesis by blast
next
case True
with that have z: "z ∈ 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 "(λ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 ⟷ (λw. h (z + w)) has_fps_expansion G z / F z"
proof (intro has_fps_expansion_cong)
have "eventually (λw. w ≠ z ⟶ f w ≠ 0) (nhds z)"
using ev_nonzero[OF ‹z ∈ A›] unfolding eventually_at_filter
by eventually_elim (use ‹z ∈ A› assms in auto)
hence "eventually (λw. w ≠ 0 ⟶ f (z + w) ≠ 0) (nhds 0)"
by (simp add: nhds_to_0' eventually_filtermap)
thus "eventually (λ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 ‹auto simp: c_def h_def›)
qed auto
finally have "h analytic_on {z}"
using has_fps_expansion_imp_analytic by blast
moreover have "h z ≠ 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: "∀z∈A. h z ≠ 0"
using analytic_on_analytic_at by blast+
moreover have "g z = h z * f z" if "z ∈ A" for z
using assms that by (auto simp: h_def)
ultimately show ?thesis
using ‹open A› by (intro that[of h]) (auto simp: analytic_on_open)
qed
subsection ‹Constructing the sequence of zeros›
text ‹
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 ‹A› 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 ‹f›
enumerating the values of ‹A› in ascending order by absolute value, and ‹f› tends to infinity
for ‹n → ∞›.
›
lemma sequence_of_sparse_set_exists:
fixes A :: "complex set"
assumes "infinite A" "closed A" "⋀r. r ≥ 0 ⟹ finite (A ∩ cball 0 r)"
obtains f :: "nat ⇒ complex"
where "mono (norm ∘ f)" "inj f" "range f = A" "filterlim f at_infinity at_top"
proof -
have "∃f::nat ⇒ complex. ∀n.
f n ∈ A ∧
f n ∉ f ` {..<n} ∧
{z∈A. norm z < norm (f n)} ⊆ f ` {..<n} ∧
(∀k<n. norm (f k) ≤ 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 ∈ A" "{z ∈ A. norm z < norm (f k)} ⊆ f ` {..<k}" "∀k'<k. cmod (f k') ≤ 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 ∈ A - f ` {..<n}"
by (meson finite.intros(1) finite_subset subsetI)
have "finite (A ∩ cball 0 (norm z0))"
by (intro assms(3)) auto
hence "finite (A ∩ cball 0 (norm z0) - f ` {..<n})"
using finite_subset by blast
moreover from z0 have "A ∩ cball 0 (norm z0) - f ` {..<n} ≠ {}"
by auto
ultimately obtain z where "is_arg_min norm (λz. z ∈ A ∩ cball 0 (norm z0) - f ` {..<n}) z"
using ex_is_arg_min_if_finite by blast
hence z: "z ∈ A" "norm z ≤ norm z0" "z ∉ f ` {..<n}"
"⋀w. w ∈ A ⟹ norm w ≤ norm z0 ⟹ w ∉ f ` {..<n} ⟹ norm w ≥ norm z"
by (auto simp: is_arg_min_def)
show ?case
proof (rule exI[of _ z], safe)
fix w assume w: "w ∈ A" "norm w < norm z"
with z(4)[of w] z w show "w ∈ f ` {..<n}"
by linarith
next
fix k assume k: "k < n"
show "norm (f k) ≤ norm z"
using f(2)[of k] z(1,3) k by auto
qed (use z in auto)
qed
then obtain f :: "nat ⇒ complex" where f:
"⋀n. f n ∈ A"
"⋀n. f n ∉ f ` {..<n}"
"⋀n. {z∈A. norm z < norm (f n)} ⊆ f ` {..<n}"
"⋀k n. k < n ⟹ norm (f k) ≤ norm (f n)"
by meson
from f(2) have f_neq: "f n ≠ 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 ∈ A"
show "z ∈ range f"
proof (rule ccontr)
assume "z ∉ range f"
hence "norm (f n) ≤ norm z" for n
using f(3)[of n] z by auto
hence "range f ⊆ A ∩ cball 0 (norm z)"
using f(1) by auto
moreover have "finite (A ∩ 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 ∘ f)"
proof (rule monoI, unfold o_def)
fix m n :: nat
assume "m ≤ n"
thus "norm (f m) ≤ norm (f n)"
using f(4)[of m n] by (cases "m < n") auto
qed
have "¬bounded A"
proof
assume "bounded A"
hence "bdd_above (norm ` A)"
by (meson bdd_above_norm)
hence "norm z ≤ Sup (norm ` A)" if "z ∈ A" for z
using that by (meson cSUP_upper)
hence "A ⊆ cball 0 (Sup (norm ` A))"
by auto
also have "… ⊆ cball 0 (max 1 (Sup (norm ` A)))"
by auto
finally have "A ⊆ A ∩ cball 0 (max 1 (Sup (norm ` A)))"
by blast
moreover have "finite (A ∩ 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 ‹¬bounded A› obtain z where "z ∈ A" "norm z > C"
unfolding bounded_iff by (auto simp: not_le)
obtain n where [simp]: "z = f n"
using range ‹z ∈ A› by auto
show "eventually (λn. norm (f n) ≥ C) at_top"
using eventually_ge_at_top[of n]
proof eventually_elim
case (elim k)
have "C ≤ norm (f n)"
using ‹norm z > C› by simp
also have "… ≤ norm (f k)"
using monoD[OF ‹mono (norm ∘ f)›, of n k] elim by auto
finally show ?case .
qed
qed
show ?thesis
by (intro that[of f] inj range mono lim)
qed
lemma strict_mono_sequence_partition:
assumes "strict_mono (f :: nat ⇒ 'a :: {linorder, no_top})"
assumes "x ≥ f 0"
assumes "filterlim f at_top at_top"
shows "∃k. x ∈ {f k..<f (Suc k)}"
proof -
define k where "k = (LEAST k. f (Suc k) > x)"
{
obtain n where "x ≤ 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 "∃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 ≤ x"
proof (cases k)
case (Suc k')
have "k ≤ k'" if "f (Suc k') > x"
using that unfolding k_def by (rule Least_le)
with Suc show "f k ≤ x" by (cases "f k ≤ x") (auto simp: not_le)
qed (use assms in auto)
ultimately show ?thesis by auto
qed
lemma strict_mono_sequence_partition':
assumes "strict_mono (f :: nat ⇒ 'a :: {linorder, no_top})"
assumes "x ≥ f 0"
assumes "filterlim f at_top at_top"
shows "∃!k. x ∈ {f k..<f (Suc k)}"
proof (rule ex_ex1I)
show "∃k. x ∈ {f k..<f (Suc k)}"
using strict_mono_sequence_partition[OF assms] .
fix k1 k2 assume "x ∈ {f k1..<f (Suc k1)}" "x ∈ {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 ⇒ nat"
assumes "infinite A" "closed A" "⋀r. r ≥ 0 ⟹ finite (A ∩ cball 0 r)"
assumes c_pos: "⋀x. x ∈ A ⟹ c x > 0"
obtains f :: "nat ⇒ complex" where
"mono (norm ∘ f)" "range f = A" "filterlim f at_infinity at_top"
"⋀z. z ∈ A ⟹ finite (f -` {z}) ∧ card (f -` {z}) = c z"
proof -
obtain f :: "nat ⇒ complex" where f:
"mono (norm ∘ 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 ⟷ m = n" for m n
using ‹inj f› by (auto simp: inj_def)
define h :: "nat ⇒ nat" where "h = (λn. ∑k<n. c (f k))"
have [simp]: "h 0 = 0"
by (simp add: h_def)
have h_ge: "h n ≥ n" for n
proof -
have "h n ≥ (∑k<n. 1)"
unfolding h_def by (intro sum_mono) (use c_pos f in ‹auto simp: Suc_le_eq›)
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: "∃!k. n ∈ {h k..<h (Suc k)}" for n
by (intro strict_mono_sequence_partition') auto
define g :: "nat ⇒ nat" where "g = (λn. THE k. n ∈ {h k..<h (Suc k)})"
have g: "n ∈ {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 ∈ {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 ‹strict_mono h›])
have "mono g"
unfolding incseq_Suc_iff
proof safe
fix n :: nat
have "h (g n) + 1 ≤ 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 ≤ g (Suc n)"
by (metis ‹strict_mono h› 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 (λm. g m ≥ n) at_top"
using eventually_ge_at_top[of "h n"]
proof eventually_elim
case (elim m)
have "n ≤ g (h n)"
by (simp add: g_h)
also have "g (h n) ≤ g m"
by (intro monoD[OF ‹mono g›] elim)
finally show ?case .
qed
qed
have vimage: "(f ∘ g) -` {f n} = {h n..<h (Suc n)}" for n
using g by (auto intro!: g_eqI)
show ?thesis
proof (rule that[of "f ∘ g"])
have "incseq (λn. (norm ∘ f) (g n))"
by (intro monoI monoD[OF f(1)] monoD[OF ‹incseq g›])
thus "incseq (norm ∘ (f ∘ g))"
by (simp add: o_def)
next
have "range (f ∘ g) ⊆ A"
using f(3) by auto
moreover have "A ⊆ range (f ∘ g)"
proof
fix z assume "z ∈ A"
then obtain n where [simp]: "z = f n"
using f(3) by auto
have "f (g (h n)) ∈ range (f ∘ g)"
unfolding o_def by blast
thus "z ∈ range (f ∘ g)"
by (simp add: g_h)
qed
ultimately show "range (f ∘ g) = A" by blast
next
fix z assume "z ∈ 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 ∘ g) -` {z}) ∧ card ((f ∘ g) -` {z}) = c z"
using vimage[of n] by simp
next
show "filterlim (f ∘ g) at_infinity at_top"
unfolding o_def by (rule filterlim_compose[OF f(4) ‹filterlim g at_top at_top›])
qed
qed
subsection ‹The factorisation theorem for holomorphic functions›
text ‹
If ‹g› is a holomorphic function on an open connected domain whose zeros do not
have an accumulation point on the frontier of ‹A›, then we can write ‹g› as a product
of a function ‹h› holomorphic on ‹A› and an entire function ‹f› such that ‹h› is non-zero
everywhere in ‹A› and the zeros of ‹f› are precisely the zeros of ‹A› with the same multiplicity.
In other words, we can get rid of all the zeros of ‹g› by dividing it with a suitable
entire function ‹f›.
›
theorem weierstrass_factorization:
assumes "g holomorphic_on A" "open A" "connected A"
assumes "⋀z. z ∈ frontier A ⟹ ¬z islimpt {w∈A. g w = 0}"
obtains h f where
"h holomorphic_on A" "f holomorphic_on UNIV"
"∀z. f z = 0 ⟷ (∀z∈A. g z = 0) ∨ (z ∈ A ∧ g z = 0)"
"∀z∈A. zorder f z = zorder g z"
"∀z∈A. h z ≠ 0"
"∀z∈A. g z = h z * f z"
proof (cases "∀z∈A. g z = 0")
case True
show ?thesis
proof (rule that[of "λ_. 1" "λ_. 0"]; (intro ballI allI impI)?)
fix z assume z: "z ∈ A"
have ev: "eventually (λw. w ∈ A) (at z)"
using z assms by (intro eventually_at_in_open') auto
show "zorder (λ_::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∈A. g z = 0}"
have freq_nz: "frequently (λz. g z ≠ 0) (at z)" if "z ∈ A" for z
proof -
have "∀⇩F w in at z. g w ≠ 0 ∧ w ∈ A"
using non_zero_neighbour_alt[OF assms(1,2,3) that(1)] not_identically_zero by auto
hence "∀⇩F w in at z. g w ≠ 0"
by eventually_elim auto
thus ?thesis
using eventually_frequently by force
qed
have zorder_pos_iff: "zorder g z > 0 ⟷ g z = 0" if "z ∈ 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 = (λz. ∏w∈Z. (z - w) powi (zorder g w))"
have eq_zero_iff: "f z = 0 ⟷ z ∈ A ∧ 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 ∈ 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 ≥ 0"
using that by (intro zorder_ge_0 freq_nz) auto
define f' where "f' = (λz'. (∏w∈Z-{z}. (z' - w) powi (zorder g w)))"
have "zorder (λ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 ∈ UNIV"
using local.zorder_pos_iff
by (fastforce intro!: holomorphic_intros simp: f'_def Z_def)+
show "f' z ≠ 0"
using True unfolding f'_def by (subst prod_zero_iff) auto
qed (use ‹zorder g z ≥ 0› in ‹auto simp: powr_of_int›)
also have "(λ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 "(∏w∈…. (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 ⇒ complex" where h:
"h holomorphic_on A" "⋀z. z ∈ A ⟹ h z ≠ 0" "⋀z. z ∈ A ⟹ 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 ⟷ g z = 0" if "z ∈ A" for z
using that by (subst eq_zero_iff) auto
show "zorder f z = zorder g z" if "z ∈ 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 ‹auto simp: eq_zero_iff zorder_eq h(2) h(3)[symmetric]›)
next
case False
note infinite_zeroes = not_identically_zero False
define c where "c = (λz. nat (zorder g z))"
have ev_nz: "eventually (λw. g w ≠ 0) (at z)" if "z ∈ A" for z
proof -
from infinite_zeroes(1) obtain z0 where z0: "z0 ∈ A" "g z0 ≠ 0"
by auto
have "eventually (λw. g w ≠ 0 ∧ w ∈ A) (at z)"
by (rule non_zero_neighbour_alt[where ?β = z0]) (use assms z0 that in auto)
thus ?thesis
by eventually_elim auto
qed
have no_limpt_Z: "¬z islimpt Z" for z
proof
assume "z islimpt Z"
show False
proof (cases "z ∈ A")
case False
have "z islimpt A"
by (rule islimpt_subset[OF ‹z islimpt Z›]) (auto simp: Z_def)
hence "z ∈ closure A"
by (simp add: closure_def)
with ‹z ∉ A› have "z ∈ frontier A"
by (simp add: closure_Un_frontier)
with assms and ‹z islimpt Z› show False
by (auto simp: Z_def)
next
case True
from True have "eventually (λw. g w ≠ 0) (at z)"
using ev_nz by blast
hence "¬z islimpt Z"
by (auto simp: islimpt_iff_eventually Z_def elim!: eventually_mono)
with ‹z islimpt Z› show False by blast
qed
qed
have "closed Z"
using no_limpt_Z unfolding closed_limpt by blast
obtain a where a:
"incseq (norm ∘ a)" "range a = Z - {0}"
"⋀z. z ∈ Z - {0} ⟹ finite (a -` {z}) ∧ 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}) ∩ cball 0 R)" if "R ≥ 0" for R
proof (rule ccontr)
assume *: "infinite ((Z - {0}) ∩ cball 0 R)"
have "∃z∈cball 0 R. z islimpt ((Z - {0}) ∩ cball 0 R)"
by (rule Heine_Borel_imp_Bolzano_Weierstrass) (use * in auto)
then obtain z where "z islimpt ((Z - {0}) ∩ 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 ∈ 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 ≠ 0" for n
using a(2) by auto
qed fact+
define m where "m = (if 0 ∈ A then nat (zorder g 0) else 0)"
have zorder_eq: "zorder (λz. z ^ m * f.f z) z = zorder g z" if "z ∈ A" for z
proof (cases "g z = 0")
case False
have "g analytic_on {z}"
using ‹z ∈ A› analytic_at assms by blast
hence "zorder g z = 0"
by (intro zorder_eq_0I False)
have "z ∉ range a"
using False Z_def a(2) by blast
hence "zorder (λz. z ^ m * f.f z) z = 0"
using False ‹zorder g z = 0›
by (intro zorder_eq_0I analytic_intros) (auto simp: f.zero m_def)
with ‹zorder g z = 0› show ?thesis
by simp
next
case True
define F where "F = fps_expansion f.f z"
have "frequently (λw. g w ≠ 0) (at z)"
using ev_nz[OF that] eventually_frequently by force
hence "zorder g z ≥ 0"
by (intro zorder_ge_0) (use assms that in ‹auto simp: analytic_at›)
have ev: "eventually (λz. z ∈ A) (nhds z)"
using that assms by (intro eventually_nhds_in_open) auto
have exp1: "(λ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: "(λ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 ≠ 0"
proof
assume "F = 0"
hence "eventually (λz. f.f z = 0) (nhds z)"
using exp1 by (auto simp: has_fps_expansion_def nhds_to_0' eventually_filtermap)
hence "eventually (λz. g z = 0) (at z)"
by (auto simp: f.zero a Z_def eventually_at_filter elim!: eventually_mono)
hence "eventually (λz::complex. False) (at z)"
using ev_nz[OF ‹z ∈ A›] by eventually_elim auto
thus False by simp
qed
have "zorder (λ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 "… = 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 "… = int (card (a -` {z}))"
using f.zorder by simp
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 ‹auto simp: Z_def›)
qed
also have "int … + (if z = 0 then m else 0) = zorder g z"
using ‹zorder g z ≥ 0› that by (auto simp: c_def m_def)
finally show ?thesis .
qed
have eq_zero_iff: "z ^ m * f.f z = 0 ⟷ g z = 0" if "z ∈ A" for z
using that by (auto simp add: f.zero a m_def zorder_pos_iff Z_def)
obtain h :: "complex ⇒ complex" where h:
"h holomorphic_on A" "⋀z. z ∈ A ⟹ h z ≠ 0" "⋀z. z ∈ A ⟹ g z = h z * (z ^ m * f.f z)"
proof (rule holomorphic_zorder_factorization[OF assms(1-3)])
show "(λz. z ^ m * f.f z) holomorphic_on A"
by (intro holomorphic_intros)
show "z ^ m * f.f z = 0 ⟷ g z = 0" if "z ∈ A" for z
by (rule eq_zero_iff) fact+
show "zorder (λz. z ^ m * f.f z) z = zorder g z" if "z ∈ A" for z
by (rule zorder_eq) fact+
qed metis
show ?thesis
proof (rule that[of h "λz. z ^ m * f.f z"]; (intro ballI allI impI)?)
show "h holomorphic_on A"
by fact
show "(λz. z ^ m * f.f z) holomorphic_on UNIV"
by (intro holomorphic_intros)
next
fix z :: complex
show "(z ^ m * f.f z = 0) = ((∀z∈A. g z = 0) ∨ z ∈ A ∧ 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 ‹
The following is a simpler version for entire functions.
›
theorem weierstrass_factorization_UNIV:
assumes "g holomorphic_on UNIV"
obtains h f where
"h holomorphic_on UNIV" "f holomorphic_on UNIV"
"∀z. f z = 0 ⟷ g z = 0"
"∀z. zorder f z = zorder g z"
"∀z. h z ≠ 0"
"∀z. g z = h z * f z"
using assms by (rule weierstrass_factorization, goal_cases) auto
subsection ‹The factorisation theorem for meromorphic functions›
text ‹
Let ‹g› be a meromorphic function on a connected open domain ‹A›. Assume that the poles and
zeros of ‹g› have no accumulation point on the border of ‹A›. Then ‹g› can be written in the
form $g(z) = h(z) f_1(z) / f_2(z)$ where $h$ is holomorphic on ‹A› 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).
›
theorem weierstrass_factorization_meromorphic:
assumes mero: "g nicely_meromorphic_on A" and A: "open A" "connected A"
assumes no_limpt: "⋀z. z ∈ frontier A ⟹ ¬z islimpt {w∈A. g w = 0 ∨ is_pole g w}"
obtains h f1 f2 where
"h holomorphic_on A" "f1 holomorphic_on UNIV" "f2 holomorphic_on UNIV"
"∀z∈A. f1 z = 0 ⟷ ¬is_pole g z ∧ g z = 0"
"∀z∈A. f2 z = 0 ⟷ is_pole g z"
"∀z∈A. ¬is_pole g z ⟶ zorder f1 z = zorder g z"
"∀z∈A. is_pole g z ⟶ zorder f2 z = -zorder g z"
"∀z∈A. h z ≠ 0"
"∀z∈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∈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' ⊆ pts" for pts'
proof (rule open_diff_sparse_pts)
show "pts' sparse_in A"
using ‹pts sparse_in A› by (rule sparse_in_subset2) fact
qed (use ‹open A› in auto)
have ev: "eventually (λw. w ∈ A - pts) (at z)" if "z ∈ A" for z
proof (cases "z ∈ pts")
case False
thus ?thesis
using that open_diff_pts[of "pts"] by (intro eventually_at_in_open') auto
next
case True
have "eventually (λw. w ∈ (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 "∀z∈A-pts. g z = 0")
case True
have no_poles: "¬is_pole g z" if "z ∈ A" for z
proof -
have "is_pole g z ⟷ is_pole (λ_::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 (λ_::complex. 0 :: complex) z" if "z ∈ A" for z
by (intro zorder_cong[OF eventually_mono[OF ev]]) (use True that in auto)
show ?thesis
by (rule that[of "λ_. 1" "λ_. 0" "λ_. 1"]) (use True in ‹auto simp: no_poles›)
next
case False
have is_pole_iff: "is_pole g z ⟷ z ∈ pts" if "z ∈ 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"
"∀z. f1 z = 0 ⟷ (∀z∈A-pts. g z = 0) ∨ (z ∈ A - pts ∧ g z = 0)"
"∀z∈A-pts. zorder f1 z = zorder g z"
"∀z∈A-pts. h z ≠ 0"
"∀z∈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 ‹auto simp: pts_def dest: nicely_meromorphic_on_subset›)
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 ‹pts sparse_in A› in auto)
show "¬ z islimpt {w ∈ A - pts. g w = 0}" if "z ∈ frontier (A - pts)" for z
proof -
from that have "z ∈ frontier A - pts ∪ pts"
using ‹open (A - pts)› ‹open A› closure_mono[of "A - pts" A]
by (auto simp: frontier_def interior_open)
thus ?thesis
proof
assume "z ∈ pts"
hence "is_pole g z"
by (auto simp: pts_def)
hence "eventually (λz. g z ≠ 0) (at z)"
using non_zero_neighbour_pole by blast
hence "¬z islimpt {w. g w = 0}"
by (auto simp: islimpt_iff_eventually)
thus ?thesis
using islimpt_subset[of z "{w∈A-pts. g w = 0}" "{w. g w = 0}"] by blast
next
assume z: "z ∈ frontier A - pts"
show "¬ z islimpt {w ∈ A - pts. g w = 0}"
proof
assume "z islimpt {w ∈ A - pts. g w = 0}"
hence "z islimpt {w ∈ A. g w = 0 ∨ 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 ⟷ (z ∈ A - pts ∧ g z = 0)" for z
using h_f1(3) False by auto
define h' where "h' = (λz. if z ∈ pts then 0 else inverse (h z))"
have isolated_h: "isolated_singularity_at h z" if "z ∈ pts" for z
proof -
have "open (A - (pts - {z}))"
by (rule open_diff_pts) auto
moreover have "z ∈ (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 ∈ 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 (λw. g w ≠ 0) (at z)"
using ‹is_pole g z› non_zero_neighbour_pole by blast
with ev[OF that(1)] have ev': "eventually (λw. g w * f1 w ≠ 0) (at z)"
by eventually_elim (use h_f1(3) in auto)
have "is_pole (λ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 (λw. g w * f1 w ≠ 0) (at z)"
using ev' by (rule eventually_frequently[rotated]) auto
from freq have freq': "frequently (λw. f1 w ≠ 0) (at z)"
using frequently_elim1 by fastforce
have "zorder g z < 0"
using ‹is_pole g z› ‹isolated_singularity_at g z› isolated_pole_imp_neg_zorder by auto
also have "0 ≤ zorder f1 z"
by (rule zorder_ge_0[OF f1 freq'])
finally show "zorder g z < zorder f1 z" .
qed
also have "?this ⟷ 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 ∈ A - pts ∧ g w * f1 w ≠ 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 ∈ A" for z
proof (cases "z ∈ pts")
case False
moreover have "open (A - pts)"
by (rule open_diff_pts) auto
ultimately have "(λz. inverse (h z)) analytic_on {z}"
using that h_f1(1,2,5) ‹open (A - pts)› analytic_at False
by (intro analytic_intros) (auto simp: f1_eq_0_iff)
also have "eventually (λz. z ∈ A - pts) (nhds z)"
using that False ‹open (A - pts)› by (intro eventually_nhds_in_open) auto
hence "(λz. inverse (h z)) analytic_on {z} ⟷ h' analytic_on {z}"
by (intro analytic_at_cong) (auto elim!: eventually_mono simp: h'_def)
finally show ?thesis .
next
case True
have "(λ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 "∀w∈A-(pts-{z})-{z}. h w ≠ 0"
using h_f1(5) by auto
qed
also have "?this ⟷ h' holomorphic_on A - (pts - {z})"
proof (intro holomorphic_cong refl)
fix w assume w: "w ∈ 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 ∈ 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 ⟷ is_pole g w" if "w ∈ 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"
"∀z. f2 z = 0 ⟷ (∀z∈A. h' z = 0) ∨ (z ∈ A ∧ h' z = 0)"
"∀z∈A. h' z = 0 ⟶ zorder f2 z = zorder h' z"
"∀z∈A. h'' z ≠ 0" "∀z∈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 A› by (simp add: analytic_on_open)
show "¬z islimpt {w∈A. h' w = 0}" if "z ∈ frontier A" for z
proof
assume "z islimpt {w∈A. h' w = 0}"
also have "{w∈A. h' w = 0} = pts"
by (auto simp: h'_eq_0_iff pts_def)
finally have "z islimpt {w ∈ A. g w = 0 ∨ 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 "λw. inverse (h'' w)" f1 f2]; (intro ballI allI impI)?)
show "(λ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 ⟷ ¬ is_pole g z ∧ g z = 0" if "z ∈ A" for z
using that by (subst f1_eq_0_iff) (auto simp: pts_def)
next
show "f2 z = 0 ⟷ is_pole g z" if "z ∈ A" for z
proof -
have "¬(∀z∈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 ⟷ h' z = 0"
using h''_f2(3) that by auto
also have "… ⟷ 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 ∈ A" "¬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 ∈ 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 "… = zorder (λw. inverse (h w)) z"
using that by (intro zorder_cong eventually_mono[OF ev]) (auto simp: h'_def)
also have "… = -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 (λw. h w ≠ 0) (at z)"
using non_zero_neighbour_pole[OF ‹is_pole h z›] eventually_frequently by force
qed (use that in ‹auto intro!: isolated_h simp: pts_def›)
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 ≠ 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 "… = zorder (λ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 ∈ A"
using that by auto
have "eventually (λw. g w ≠ 0) (at z)"
using non_zero_neighbour_pole[of g z] that by auto
hence "eventually (λw. f1 w * h w ≠ 0) (at z)"
using ev[OF ‹z ∈ A›] by eventually_elim (use h_f1(6) in auto)
thus "frequently (λw. f1 w * h w ≠ 0) (at z)"
using eventually_frequently by force
qed
also have "… = zorder g z"
proof (rule zorder_cong)
have "eventually (λw. w ∈ A - pts) (at z)"
using ev[of z] that by auto
thus "eventually (λ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) ≠ 0" if "z ∈ A" for z
using h''_f2(5) that by auto
next
show "g z = inverse (h'' z) * f1 z / f2 z" if z: "z ∈ 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 ≠ 0" "h z ≠ 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 "… = 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 "¬g ─z→ 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 ‹
Again, we derive an easier version for functions meromorphic on the entire complex plane.
›
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"
"∀z. f1 z = 0 ⟷ ¬is_pole g z ∧ g z = 0"
"∀z. f2 z = 0 ⟷ is_pole g z"
"∀z. ¬is_pole g z ⟶ zorder f1 z = zorder g z"
"∀z. is_pole g z ⟶ zorder f2 z = -zorder g z"
"∀z. h z ≠ 0"
"∀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 "¬ z islimpt {w ∈ UNIV. g w = 0 ∨ is_pole g w}" if "z ∈ frontier UNIV" for z
using that by simp
show "open (UNIV :: complex set)"
by simp
qed auto
end