Theory HOL-Complex_Analysis.Weierstrass_Factorization
section ‹The Weierstra\ss\ Factorisation Theorem›
theory Weierstrass_Factorization
imports Meromorphic
begin
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
fixes z :: "'a :: {banach, real_normed_field}"
assumes "norm z ≤ 1 / 2"
shows norm_exp_bounds_lemma: "norm (exp z - 1 - z) ≤ norm z / 2"
and norm_exp_bounds: "norm (exp z - 1) ≥ 1 / 2 * norm z"
"norm (exp z - 1) ≤ 3 / 2 * norm z"
proof -
show *: "norm (exp z - 1 - z) ≤ norm z / 2"
proof (cases "z = 0")
case False
have sums: "(λk. z ^ (k + 2) /⇩R fact (k + 2)) sums (exp z - (∑k<2. z ^ k /⇩R fact k))"
by (intro sums_split_initial_segment exp_converges)
have "summable (λk. norm z ^ (k + 2) /⇩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 ⟷ summable (λ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 "… ⟷ summable (λk. norm z ^ k / fact (k + 2))"
by (subst summable_cmult_iff) (use ‹z ≠ 0› in auto)
finally have summable: "summable (λk. norm z ^ k / fact (k + 2))" .
have "exp z - 1 - z = (∑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 … ≤ (∑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 "… = (∑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 "… = norm z ^ 2 * (∑k. norm z ^ k / fact (k + 2))"
using summable by (rule suminf_mult)
also have "… ≤ norm z ^ 2 * (1 / (1 - norm z) / 2)"
proof (intro mult_left_mono, rule sums_le)
show "(λk. norm z ^ k / fact (k + 2)) sums (∑k. norm z ^ k / fact (k + 2))"
using summable by blast
show "(λ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) ≤ norm z ^ k / fact 2"
by (intro divide_left_mono fact_mono) auto
thus "norm z ^ k / fact (k + 2) ≤ norm z ^ k / 2"
by simp
qed (auto simp: divide_simps)
also have "… = norm z * (norm z / (1 - norm z)) / 2"
by (simp add: power2_eq_square)
also have "… ≤ norm z * ((1 / 2) / (1 - (1 / 2))) / 2"
using assms by (intro mult_mono frac_le diff_mono) auto
also have "… = norm z / 2"
by simp
finally show "norm (exp z - 1 - z) ≤ norm z / 2" .
qed auto
have "norm (exp z - 1) ≤ norm z + norm (exp z - 1 - z)"
by (rule norm_triangle_sub)
with * show "norm (exp z - 1) ≤ 3 / 2 * norm z"
by simp
have "norm z - norm (exp z - 1 - z) ≤ norm (exp z - 1)"
using norm_triangle_ineq3[of "exp z - 1 - z" "-z"] by simp
with * show "norm (exp z - 1) ≥ 1 / 2 * norm z"
by simp
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 :: "nat ⇒ complex"
fixes p :: "nat ⇒ nat"
assumes a_nonzero: "⋀n. a n ≠ 0"
assumes filterlim_a: "filterlim a at_infinity at_top"
assumes summable_a_p: "⋀r. r > 0 ⟹ summable (λn. (r / norm (a n)) ^ Suc (p n))"
begin
definition f :: "complex ⇒ complex" where
"f z = (∏n. weierstrass_factor (p n) (z / a n))"
lemma abs_convergent: "abs_convergent_prod (λn. weierstrass_factor (p n) (z / a n))"
unfolding abs_convergent_prod_conv_summable
proof (rule summable_comparison_test_ev)
have "eventually (λ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 (λn. norm (norm (weierstrass_factor (p n) (z / a n) - 1)) ≤
3 * norm (z / a n) ^ Suc (p n)) at_top"
proof eventually_elim
case (elim n)
hence "norm (z / a n) ≤ 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 (λ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 (λn. weierstrass_factor (p n) (z / a n))"
using abs_convergent[of z] abs_convergent_prod_imp_convergent_prod by blast
lemma has_prod: "(λ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 (λ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: "⋀n. n ≥ N ⟹ norm (a n) > norm z"
by (auto simp: eventually_at_top_linorder)
have "n < N" if "n ∈ a -` {z}" for n
using N[of n] that by (cases "n < N") auto
hence "a -` {z} ⊆ {..<N}" "finite {..<N}"
by auto
thus ?thesis
using finite_subset by blast
qed
context
fixes P
defines "P ≡ (λN z. ∏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) (λN z. ∑n<N. norm (weierstrass_factor (p n) (z / a n) - 1))"
proof (rule Weierstrass_m_test'_ev)
have "eventually (λn. norm (a n) ≥ 2 * R) sequentially"
using filterlim_a by (metis filterlim_at_infinity_imp_norm_at_top filterlim_at_top)
thus "∀⇩F n in sequentially. ∀z∈cball 0 R. norm (norm (weierstrass_factor (p n) (z / a n) - 1)) ≤
3 * (R / norm (a n)) ^ Suc (p n)"
proof eventually_elim
case (elim n)
show ?case
proof safe
fix z :: complex assume z: "z ∈ cball 0 R"
have "2 * norm z ≤ 2 * R"
using z by auto
also have "… ≤ norm (a n)"
using elim by simp
finally have "norm (a n) ≥ 2 * norm z" .
hence "norm (weierstrass_factor (p n) (z / a n) - 1) ≤ 3 * norm (z / a n) ^ Suc (p n)"
by (intro weierstrass_factor_bound) (auto simp: norm_divide divide_simps)
also have "… = 3 * (norm z / norm (a n)) ^ Suc (p n)"
by (simp add: norm_divide)
also have "… ≤ 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)) ≤
3 * (R / norm (a n)) ^ Suc (p n)" by simp
qed
qed
next
show "summable (λ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 ⟷ uniform_limit (cball 0 R) P f at_top"
proof (intro uniform_limit_cong)
fix z :: complex assume "z ∈ cball 0 R"
with g have "(λn. P (Suc n) z) ⇢ g z"
by (metis tendsto_uniform_limitI filterlim_sequentially_Suc)
moreover have "(λn. P (Suc n) z) ⇢ 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 "∃d>0. cball z d ⊆ UNIV ∧ 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 ⟷ z ∈ range a"
using has_prod_eq_0_iff[OF has_prod, of z] by (auto simp: a_nonzero)
lemma not_islimpt_range_a: "¬z islimpt (range a)"
proof
assume "z islimpt (range a)"
then obtain r :: "nat ⇒ nat" where r: "strict_mono r" "(a ∘ r) ⇢ z"
using islimpt_range_imp_convergent_subsequence by metis
moreover have "filterlim (a ∘ 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 ∈ 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} ⊆ {..N}"
using finite_occs_a[of z] by (meson finite_nat_iff_bounded_le)
define g where "g = (λz n. weierstrass_factor (p n) (z / a n))"
define h1 where "h1 = (λw. (∏n∈{..N} - a-`{z}. g w n) * (∏n. g w (n + Suc N)))"
define h2 where "h2 = (λw. (∏n∈{..N} ∩ a-`{z}. g w n))"
have has_prod_h1': "(λn. g w (n + Suc N)) has_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 = (∏n<Suc N. g w n) * (∏n. g w (n + Suc N))"
proof (rule has_prod_unique2)
show "(λn. g w n) has_prod ((∏n<Suc N. g w n) * (∏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}) ∪ ({..N} ∩ a-`{z})"
by auto
also have "(∏k∈…. g w k) = (∏k∈{..N} - a-`{z}. g w k) * (∏k∈{..N} ∩ 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 "λn. a (n + Suc N)" "λn. p (n + Suc N)"
proof
have "filterlim (λn. n + Suc N) at_top at_top"
by (rule filterlim_add_const_nat_at_top)
thus "filterlim (λn. a (n + Suc N)) at_infinity at_top"
by (intro filterlim_compose[OF filterlim_a])
show "summable (λ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 (λw. h1 w * h2 w) z"
by (simp add: f_eq [abs_def])
also have "… = zorder h1 z + zorder h2 z"
proof (rule zorder_times_analytic)
have "eventually (λw. f w ≠ 0) (at z)"
using not_islimpt_range_a[of z] by (auto simp: islimpt_conv_frequently_at frequently_def zero)
thus "eventually (λw. h1 w * h2 w ≠ 0) (at z)"
by (simp add: f_eq)
qed fact+
also have "zorder h2 z = (∑n∈{..N} ∩ a -` {z}. zorder (λ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 ≠ 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 "(∑n∈{..N} ∩ a -` {z}. zorder (λw. g w n) z) = (∑n∈{..N} ∩ a -` {z}. 1)"
proof (intro sum.cong refl)
fix n :: nat
assume n: "n ∈ {..N} ∩ a -` {z}"
have "zorder (λ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 (λw. g w n) z = zorder (weierstrass_factor (p n)) 1"
using n a_nonzero[of n] by (auto simp: g_def)
thus "zorder (λw. g w n) z = 1"
by simp
qed
also have "… = card ({..N} ∩ a -` {z})"
by simp
also have "{..N} ∩ a -` {z} = a -` {z}"
using N by blast
finally show ?thesis
by simp
qed
end
text ‹
The following locale is the most common case of $p(n) = n$.
›
locale weierstrass_product' =
fixes a :: "nat ⇒ complex"
assumes a_nonzero: "⋀n. a n ≠ 0"
assumes filterlim_a: "filterlim a at_infinity at_top"
assumes finite_occs_a': "⋀z. z ∈ range a ⟹ finite (a -` {z})"
begin
lemma finite_occs_a: "finite (a -` {z})"
proof (cases "z ∈ 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 "λn. n"
proof
fix r :: real assume r: "r > 0"
show "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
qed (use a_nonzero filterlim_a finite_occs_a in auto)
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
show "finite (a -` {z})" if "z ∈ range a" for z
using a(3)[of z] a(2) that by simp
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}))"
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 ‹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