Theory Weierstrass_Elliptic
section ‹The Weierstra\ss\ ‹℘› Function›
theory Weierstrass_Elliptic
imports
Elliptic_Functions
Modular_Group
begin
text ‹
In this section, we will define the Weierstra\ss\ ‹℘› function, which is in some sense
the simplest and most fundamental elliptic function. All elliptic functions can be expressed
solely in terms of ‹℘› and ‹℘'›.
›
subsection ‹Preliminary convergence results›
text ‹
We first examine the uniform convergence of the series
\[\sum_{\omega\in\Lambda^*} \frac{1}{(z-\omega)^n}\]
and
\[\sum_{\omega\in\Lambda} \frac{1}{(z-\omega)^n}\]
for fixed $n \geq 3$.
The second version is an elliptic function that we call the ∗‹Eisenstein function› because
setting $z = 0$ gives us the Eisenstein series. To our knowledge this function does not have a
name of its own in the literature.
This is perhaps because it is up to a constant factor, equal to the $(n-2)$-nth derivative of
the Weierstra\ss\ $\wp$ function (which we will define a bit afterwards).
›
lemmas [simp del] = div_mult_self1 div_mult_self2 div_mult_self3 div_mult_self4
context complex_lattice
begin
lemma ω_upper:
assumes "ω ∈ lattice_layer k" and "α > 0" and "k > 0"
shows "norm ω powr -α ≤ (k*Inf_para) powr -α"
using lattice_layer_le_norm Inf_para_pos assms powr_mono2' by force
lemma sum_ω_upper:
assumes "α > 0" and "k > 0"
shows "(∑ω ∈ lattice_layer k. norm ω powr -α) ≤ 8 * k powr (1-α) * Inf_para powr -α"
(is "?lhs ≤ ?rhs")
proof -
have "?lhs ≤ (8 * k) * (k*Inf_para) powr -α"
using sum_bounded_above [OF ω_upper] card_lattice_layer [OF ‹k>0›] assms
by fastforce
also have "… = ?rhs"
using Inf_para_pos by (simp add: powr_diff powr_minus powr_mult divide_simps)
finally show ?thesis .
qed
lemma lattice_layer_lower:
assumes "ω ∈ lattice_layer k" and "k > 0"
shows "(k * (if α ≥ 0 then Inf_para else Sup_para)) powr α ≤ norm ω powr α"
proof (cases "α ≥ 0")
case True
have [simp]: "ω ≠ 0"
using assms by auto
show ?thesis
by (rule powr_mono2)
(use True lattice_layer_le_norm[of ω k] Inf_para_pos assms in auto)
next
case False
show ?thesis
by (rule powr_mono2') (use False lattice_layer_ge_norm[of ω k] assms in auto)
qed
lemma sum_lattice_layer_lower:
fixes α :: real
assumes "k > 0"
defines "C ≡ (if α ≥ 0 then Sup_para else Inf_para)"
shows "8 * k powr (1-α) * C powr -α ≤ (∑ω ∈ lattice_layer k. norm ω powr -α)"
(is "?lhs ≤ ?rhs")
proof -
from ‹k > 0› have "?lhs = (∑ω∈lattice_layer k. (k * C) powr -α)"
by (simp add: powr_minus powr_diff field_simps powr_mult card_lattice_layer)
also have "… ≤ ?rhs"
unfolding C_def using lattice_layer_lower[of _ k "-α"] ‹k > 0›
by (cases "α > 0"; intro sum_mono) (auto split: if_splits)
finally show ?thesis .
qed
lemma converges_absolutely_iff_aux1:
fixes α :: real
assumes "α > 2"
shows "summable (λi. ∑ω∈lattice_layer (Suc i). 1 / norm ω powr α)"
proof (rule summable_comparison_test')
show "norm (∑ω∈lattice_layer (Suc n). 1 / norm ω powr α) ≤
8 * real (Suc n) powr (1 - α) * Inf_para powr -α" for n
proof -
have "norm (∑ω∈lattice_layer (Suc n). 1 / norm ω powr α) =
(∑ω∈lattice_layer (Suc n). norm ω powr -α)"
unfolding real_norm_def
by (subst abs_of_nonneg) (auto intro!: sum_nonneg simp: powr_minus field_simps)
also have "… ≤ 8 * real (Suc n) powr (1 - α) * Inf_para powr -α"
using sum_ω_upper[of α "Suc n"] assms by simp
finally show ?thesis .
qed
next
show "summable (λn. 8 * real (Suc n) powr (1 - α) * Inf_para powr -α)"
by (subst summable_Suc_iff, intro summable_mult summable_mult2, subst summable_real_powr_iff)
(use assms in auto)
qed
lemma converges_absolutely_iff_aux2:
fixes α :: real
assumes "summable (λi. ∑ω∈lattice_layer (Suc i). 1 / norm ω powr α)"
shows "α > 2"
proof -
define C where "C = (if α > 0 then Sup_para else Inf_para)"
have "C > 0"
using Sup_para_pos Inf_para_pos by (auto simp: C_def)
have "summable (λn. 8 * real (Suc n) powr (1 - α) * C powr -α)"
proof (rule summable_comparison_test')
show "norm (8 * real (Suc n) powr (1 - α) * C powr -α) ≤
(∑ω∈lattice_layer (Suc n). 1 / norm ω powr α)" for n
proof -
have "norm (8 * real (Suc n) powr (1 - α) * C powr -α) =
8 * real (Suc n) powr (1 - α) * C powr -α"
unfolding real_norm_def by (subst abs_of_nonneg) (auto intro!: sum_nonneg)
also have "… ≤ (∑ω∈lattice_layer (Suc n). 1 / norm ω powr α)"
using sum_lattice_layer_lower[of "Suc n" α]
by (auto simp: powr_minus field_simps C_def split: if_splits)
finally show ?thesis .
qed
qed fact
hence "summable (λn. 8 * C powr -α * real n powr (1 - α))"
by (subst (asm) summable_Suc_iff) (simp add: mult_ac)
hence "summable (λn. real n powr (1 - α))"
using ‹C > 0› by (subst (asm) summable_cmult_iff) auto
thus "α > 2"
by (subst (asm) summable_real_powr_iff) auto
qed
text ‹Apostol's Lemma 1›
lemma converges_absolutely_iff:
fixes α:: real
shows "(λω. 1 / norm ω powr α) summable_on Λ⇧* ⟷ α > 2"
(is "?P ⟷ _")
proof -
have "(λω. 1 / norm ω powr α) summable_on Λ⇧* ⟷
(λω. 1 / norm ω powr α) summable_on (⋃i ∈ {0<..}. lattice_layer i)"
by (simp add: lattice0_conv_layers)
also have "… ⟷ (λi. ∑ω∈lattice_layer i. 1 / norm ω powr α) summable_on {0<..}"
using lattice_layer_disjoint
by (intro summable_on_Union_iff has_sum_finite finite_lattice_layer refl)
(auto simp: disjoint_family_on_def)
also have "{0<..} = Suc ` UNIV"
by (auto simp: image_iff) presburger?
also have "(λi. ∑ω∈lattice_layer i. 1 / norm ω powr α) summable_on Suc ` UNIV ⟷
(λi. ∑ω∈lattice_layer (Suc i). 1 / norm ω powr α) summable_on UNIV"
by (subst summable_on_reindex) (auto simp: o_def)
also have "… ⟷ summable (λi. ∑ω∈lattice_layer (Suc i). 1 / norm ω powr α)"
by (rule summable_on_UNIV_nonneg_real_iff) (auto intro: sum_nonneg)
also have "… ⟷ α > 2"
using converges_absolutely_iff_aux1 converges_absolutely_iff_aux2 by blast
finally show ?thesis .
qed
lemma bounded_lattice_finite:
assumes "bounded B"
shows "finite (Λ ∩ B)"
by (meson not_islimpt_lattice inf.bounded_iff islimpt_subset ‹bounded B›
bounded_infinite_imp_islimpt bounded_subset eq_refl)
lemma closed_subset_lattice: "Λ' ⊆ Λ ⟹ closed Λ'"
unfolding closed_limpt using not_islimpt_lattice islimpt_subset by blast
corollary closed_lattice0: "closed Λ⇧*"
unfolding lattice0_def by (rule closed_subset_lattice) auto
lemma weierstrass_summand_bound:
assumes "α ≥ 1" and "R > 0"
obtains M where
"M > 0"
"⋀ω z. ⟦ω ∈ Λ; cmod ω > R; cmod z ≤ R⟧ ⟹ norm (z - ω) powr -α ≤ M * (norm ω powr -α)"
proof -
obtain m where m: "of_int m > R / norm ω1" "m ≥ 0"
by (metis ex_less_of_int le_less_trans linear not_le of_int_0_le_iff)
obtain W where W: "W ∈ (Λ - cball 0 R) ∩ cball 0 (norm W)"
proof
show "of_int m * ω1 ∈ (Λ - cball 0 R) ∩ cball 0 (norm (of_int m * ω1))"
using m latticeI [of m 0]
by (simp add: field_simps norm_mult)
qed
define PF where "PF ≡ (Λ - cball 0 R) ∩ cball 0 (norm W)"
have "finite PF"
by (simp add: PF_def Diff_Int_distrib2 bounded_lattice_finite)
then have "finite (norm ` PF)"
by blast
then obtain r where "r ∈ norm ` PF" "r ≤ norm W" and r: "⋀x. x ∈ norm ` PF ⟹ r ≤ x"
using PF_def W Min_le Min_in by (metis empty_iff image_eqI)
then obtain ωr where ωr: "ωr ∈ PF" "norm ωr = r"
by blast
with assms have "ωr ∈ Λ" "ωr ≠ 0" "r > 0"
by (auto simp: PF_def)
have minr: "r ≤ cmod ω" if "ω ∈ Λ" "cmod ω > R" for ω
using r ‹r ≤ cmod W› that unfolding PF_def by fastforce
have "R < r"
using ωr by (simp add: PF_def)
with ‹R > 0› have R_iff_r: "cmod ω > R ⟷ cmod ω ≥ r" if "ω ∈ Λ" for ω
using that by (auto simp: minr)
define M where "M ≡ (1 - R/r) powr -α"
have "M > 0"
unfolding M_def using ‹R < r› by auto
moreover
have "cmod (z - ω) powr -α ≤ M * cmod ω powr -α"
if "ω ∈ Λ" "cmod z ≤ R" "R < cmod ω" for z ω
proof -
have "r ≤ cmod ω"
using minr that by blast
then have "ω ≠ 0"
using ‹0 < r› that by force
have "1 - R/r ≤ 1 - norm (z/ω)"
using that ‹0 < r› ‹0 < R› ‹ω ≠ 0› ‹r ≤ cmod ω›
by (simp add: field_simps norm_divide) (metis mult.commute mult_mono norm_ge_zero)
also have "… ≤ norm (1 - z/ω)"
by (metis norm_one norm_triangle_ineq2)
also have "… = norm ((z - ω) / ω)"
by (simp add: ‹ω ≠ 0› norm_minus_commute diff_divide_distrib)
finally have *: "1 - R/r ≤ norm ((z - ω) / ω)" .
have ge_rR: "cmod (z - ω) ≥ r - R"
by (smt (verit) ‹r ≤ cmod ω› norm_minus_commute norm_triangle_ineq2 that(2))
have "1/M ≤ norm ((z - ω) / ω) powr α"
proof -
have "1/M = (1 - R / r) powr α"
by (simp add: M_def powr_minus_divide)
also have "… ≤ norm ((z - ω) / ω) powr α"
using * ‹0 < r› ‹R < r› ‹1 ≤ α› powr_mono2 by force
finally show ?thesis .
qed
then show ?thesis
using ‹R > 0› ‹M > 0› ‹ω ≠ 0›
by (simp add: mult.commute divide_simps powr_divide norm_divide powr_minus)
qed
ultimately show thesis
using that by presburger
qed
text ‹Lemma 2 on Apostol p. 8›
lemma weierstrass_aux_converges_absolutely_in_disk:
assumes "α > 2" and "R > 0" and "z ∈ cball 0 R"
shows "(λω. cmod (z - ω) powr -α) summable_on (Λ - cball 0 R)"
proof -
have Λ: "Λ - cball 0 R ⊆ Λ⇧*"
using assms by force
obtain M where "M > 0" and M: "⋀ω. ⟦ω ∈ Λ; cmod ω > R⟧ ⟹ cmod(z - ω) powr -α ≤ M * (cmod ω powr -α)"
using weierstrass_summand_bound assms
by (smt (verit, del_insts) less_eq_real_def mem_cball_0 one_le_numeral)
have §: "((λω. 1 / cmod ω powr α) summable_on Λ⇧*)"
using ‹α > 2› converges_absolutely_iff by blast
have "(λω. M * norm ω powr -α) summable_on Λ⇧*"
using summable_on_cmult_right [OF §] by (simp add: powr_minus field_class.field_divide_inverse)
with Λ have "(λω. M * norm ω powr -α) summable_on Λ - cball 0 R"
using summable_on_subset_banach by blast
then show ?thesis
by (rule summable_on_comparison_test) (use M in auto)
qed
lemma weierstrass_aux_converges_absolutely_in_disk':
fixes α :: nat and R :: real and z:: complex
assumes "α > 2" and "R > 0" and "z ∈ cball 0 R"
shows "(λω. 1 / norm (z - ω) ^ α) summable_on (Λ - cball 0 R)"
proof -
have "(λω. norm (z - ω) powr -of_nat α) summable_on (Λ - cball 0 R)"
using assms by (intro weierstrass_aux_converges_absolutely_in_disk) auto
also have "?this ⟷ ?thesis"
unfolding powr_minus
by (intro summable_on_cong refl, subst powr_realpow)
(use assms in ‹auto simp: field_simps›)
finally show ?thesis .
qed
lemma weierstrass_aux_converges_in_disk':
fixes α :: nat and R :: real and z:: complex
assumes "α > 2" and "R > 0" and "z ∈ cball 0 R"
shows "(λω. 1 / (z - ω) ^ α) summable_on (Λ - cball 0 R)"
by (rule abs_summable_summable)
(use weierstrass_aux_converges_absolutely_in_disk'[OF assms]
in ‹simp add: norm_divide norm_power›)
lemma weierstrass_aux_converges_absolutely:
fixes α :: real
assumes "α > 2" and "Λ' ⊆ Λ"
shows "(λω. norm (z - ω) powr -α) summable_on Λ'"
proof (cases "z = 0")
case True
hence "(λω. norm (z - ω) powr -α) summable_on Λ⇧*"
using converges_absolutely_iff[of α] assms by (simp add: powr_minus field_simps)
hence "(λω. norm (z - ω) powr -α) summable_on Λ"
by (simp add: lattice_lattice0 summable_on_insert_iff)
thus ?thesis
by (rule summable_on_subset_banach) fact
next
case [simp]: False
define R where "R = norm z"
have "(λω. norm (z - ω) powr -α) summable_on (Λ - cball 0 R)"
using assms by (intro weierstrass_aux_converges_absolutely_in_disk) (auto simp: R_def)
hence "(λω. norm (z - ω) powr -α) summable_on (Λ - cball 0 R) ∪ (Λ ∩ cball 0 R)"
by (intro bounded_lattice_finite summable_on_union[OF _ summable_on_finite]) auto
also have "… = Λ"
by blast
finally show ?thesis
by (rule summable_on_subset) fact
qed
lemma weierstrass_aux_converges_absolutely':
fixes α :: nat
assumes "α > 2" and "Λ' ⊆ Λ"
shows "(λω. 1 / norm (z - ω) ^ α) summable_on Λ'"
using weierstrass_aux_converges_absolutely[of "of_nat α" Λ' z] assms
by (simp add: powr_nat' powr_minus field_simps norm_power norm_divide powr_realpow')
lemma weierstrass_aux_converges:
fixes α :: real
assumes "α > 2" and "Λ' ⊆ Λ"
shows "(λω. (z - ω) powr -α) summable_on Λ'"
by (rule abs_summable_summable)
(use weierstrass_aux_converges_absolutely[OF assms]
in ‹simp add: norm_divide norm_powr_real_powr'›)
lemma weierstrass_aux_converges':
fixes α :: nat
assumes "α > 2" and "Λ' ⊆ Λ"
shows "(λω. 1 / (z - ω) ^ α) summable_on Λ'"
using weierstrass_aux_converges[of "of_nat α" Λ' z] assms
by (simp add: powr_nat' powr_minus field_simps)
lemma
fixes α R :: real
assumes "α > 2" "R > 0"
shows weierstrass_aux_converges_absolutely_uniformly_in_disk:
"uniform_limit (cball 0 R)
(λX z. ∑ω∈X. norm ((z - ω) powr -α))
(λz. ∑⇩∞ω∈Λ-cball 0 R. norm ((z - ω) powr -α))
(finite_subsets_at_top (Λ - cball 0 R))" (is ?th1)
and weierstrass_aux_converges_uniformly_in_disk:
"uniform_limit (cball 0 R)
(λX z. ∑ω∈X. (z - ω) powr -α)
(λz. ∑⇩∞ω∈Λ-cball 0 R. (z - ω) powr -α)
(finite_subsets_at_top (Λ - cball 0 R))" (is ?th2)
proof -
obtain M where M:
"M > 0" "⋀ω z. ⟦ω ∈ Λ; norm ω > R; norm z ≤ R⟧ ⟹ norm (z - ω) powr -α ≤ M * norm ω powr -α"
using weierstrass_summand_bound[of α R] assms by auto
have 1: "(λω. M * norm ω powr -α) summable_on (Λ - cball 0 R)"
proof -
have "(λω. 1 / norm ω powr α) summable_on Λ⇧*"
using assms by (subst converges_absolutely_iff) auto
hence "(λω. M * norm ω powr -α) summable_on Λ⇧*"
by (intro summable_on_cmult_right) (auto simp: powr_minus field_simps)
thus "(λω. M * norm ω powr -α) summable_on (Λ - cball 0 R)"
by (rule summable_on_subset) (use assms in ‹auto simp: lattice0_def›)
qed
have 2: "norm ((z - ω) powr -α) ≤ M * norm ω powr -α"
if "ω ∈ Λ - cball 0 R" "z ∈ cball 0 R" for ω z
proof -
have "norm ((z - ω) powr -α) = norm (z - ω) powr -α"
by (auto simp add: powr_def)
also have "… ≤ M * norm ω powr -α"
using that by (intro M) auto
finally show "norm ((z - ω) powr -α) ≤ M * norm ω powr -α"
by simp
qed
show ?th1 ?th2
by (rule Weierstrass_m_test_general[OF _ 1]; use 2 in simp)+
qed
lemma
fixes n :: nat and R :: real
assumes "n > 2" "R > 0"
shows weierstrass_aux_converges_absolutely_uniformly_in_disk':
"uniform_limit (cball 0 R)
(λX z. ∑ω∈X. norm (1 / (z - ω) ^ n))
(λz. ∑⇩∞ω∈Λ-cball 0 R. norm (1 / (z - ω) ^ n))
(finite_subsets_at_top (Λ - cball 0 R))" (is ?th1)
and weierstrass_aux_converges_uniformly_in_disk':
"uniform_limit (cball 0 R)
(λX z. ∑ω∈X. 1 / (z - ω) powr n)
(λz. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω) ^ n)
(finite_subsets_at_top (Λ - cball 0 R))" (is ?th2)
proof -
have "uniform_limit (cball 0 R)
(λX z. ∑ω∈X. norm ((z - ω) powr -real n))
(λz. ∑⇩∞ω∈Λ-cball 0 R. norm ((z - ω) powr -real n))
(finite_subsets_at_top (Λ - cball 0 R))"
by (rule weierstrass_aux_converges_absolutely_uniformly_in_disk) (use assms in auto)
also have "?this ⟷ ?th1"
by (intro uniform_limit_cong eventually_finite_subsets_at_top_weakI sum.cong ballI)
(auto simp: norm_divide norm_power powr_minus field_simps powr_nat
intro!: infsum_cong)
finally show ?th1 .
next
have "uniform_limit (cball 0 R)
(λX z. ∑ω∈X. (z - ω) powr -of_nat n)
(λz. ∑⇩∞ω∈Λ-cball 0 R. (z - ω) powr -of_nat n)
(finite_subsets_at_top (Λ - cball 0 R))"
using weierstrass_aux_converges_uniformly_in_disk[of "of_nat n" R] assms by auto
also have "?this ⟷ ?th2"
by (intro uniform_limit_cong eventually_finite_subsets_at_top_weakI sum.cong ballI)
(auto simp: norm_divide norm_power powr_minus field_simps powr_nat
intro!: infsum_cong)
finally show ?th2 .
qed
definition eisenstein_fun_aux :: "nat ⇒ complex ⇒ complex" where
"eisenstein_fun_aux n z =
(if n = 0 then 1 else if n < 3 ∨ z ∈ Λ⇧* then 0 else (∑⇩∞ω∈Λ⇧*. 1 / (z - ω) ^ n))"
lemma eisenstein_fun_aux_at_pole_eq_0: "n > 0 ⟹ z ∈ Λ⇧* ⟹ eisenstein_fun_aux n z = 0"
by (simp add: eisenstein_fun_aux_def)
lemma eisenstein_fun_aux_has_sum:
assumes "n ≥ 3" "z ∉ Λ⇧*"
shows "((λω. 1 / (z - ω) ^ n) has_sum eisenstein_fun_aux n z) Λ⇧*"
proof -
have "eisenstein_fun_aux n z = (∑⇩∞ω∈Λ⇧*. 1 / (z - ω) ^ n)"
using assms by (simp add: eisenstein_fun_aux_def)
also have "((λω. 1 / (z - ω) ^ n) has_sum …) Λ⇧*"
using assms by (intro has_sum_infsum weierstrass_aux_converges') (auto simp: lattice0_def)
finally show ?thesis .
qed
lemma eisenstein_fun_aux_minus: "eisenstein_fun_aux n (-z) = (-1) ^ n * eisenstein_fun_aux n z"
proof (cases "n < 3 ∨ z ∈ Λ⇧*")
case False
have "eisenstein_fun_aux n (-z) = (∑⇩∞ω∈Λ⇧*. 1 / (- z - ω) ^ n)"
using False by (auto simp: eisenstein_fun_aux_def lattice0_def uminus_in_lattice_iff)
also have "… = (∑⇩∞ω∈uminus ` Λ⇧*. 1 / (ω - z) ^ n)"
by (subst infsum_reindex) (auto simp: o_def minus_diff_commute inj_on_def)
also have "uminus ` Λ⇧* = Λ⇧*"
by (auto simp: lattice0_def uminus_in_lattice_iff image_def intro: bexI[of _ "-x" for x])
also have "(λω. 1 / (ω - z) ^ n) = (λω. (-1) ^ n * (1 / (z - ω) ^ n))"
proof
fix ω :: complex
have "1 / (ω - z) ^ n = (1 / (ω - z)) ^ n"
by (simp add: power_divide)
also have "1 / (ω - z) = (-1) / (z - ω)"
by (simp add: divide_simps)
also have "… ^ n = (-1) ^ n * (1 / (z - ω) ^ n)"
by (subst power_divide) auto
finally show "1 / (ω - z) ^ n = (-1) ^ n * (1 / (z - ω) ^ n)" .
qed
also have "(∑⇩∞ω∈Λ⇧*. (-1) ^ n * (1 / (z - ω) ^ n)) = (-1) ^ n * eisenstein_fun_aux n z"
using False by (subst infsum_cmult_right') (auto simp: eisenstein_fun_aux_def)
finally show ?thesis .
qed (auto simp: eisenstein_fun_aux_def lattice0_def uminus_in_lattice_iff)
lemma eisenstein_fun_aux_even_minus: "even n ⟹ eisenstein_fun_aux n (-z) = eisenstein_fun_aux n z"
by (simp add: eisenstein_fun_aux_minus)
lemma eisenstein_fun_aux_odd_minus: "odd n ⟹ eisenstein_fun_aux n (-z) = -eisenstein_fun_aux n z"
by (simp add: eisenstein_fun_aux_minus)
lemma eisenstein_fun_aux_has_field_derivative_aux:
fixes α :: nat and R :: real
defines "F ≡ (λα z. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω) ^ α)"
assumes "α > 2" "R > 0" "w ∈ ball 0 R"
shows "(F α has_field_derivative -of_nat α * F (Suc α) w) (at w)"
proof -
define α' where "α' = α - 1"
have α': "α = Suc α'"
using assms by (simp add: α'_def)
have 1: "∀⇩F n in finite_subsets_at_top (Λ - cball 0 R).
continuous_on (cball 0 R) (λz. ∑ω∈n. 1 / (z - ω) ^ α) ∧
(∀z∈ball 0 R. ((λz. ∑ω∈n. 1 / (z - ω) ^ α) has_field_derivative (∑ω∈n. -α / (z - ω) ^ Suc α)) (at z))"
proof (intro eventually_finite_subsets_at_top_weakI conjI continuous_intros derivative_intros ballI)
fix z::complex and X n
assume "finite X" "X ⊆ Λ - cball 0 R"
and "z ∈ ball 0 R" "n ∈ X"
then show "((λz. 1 / (z - n) ^ α) has_field_derivative of_int (- int α) / (z - n) ^ Suc α) (at z)"
apply (auto intro!: derivative_eq_intros simp: divide_simps)
apply (simp add: algebra_simps α')
done
qed auto
have "uniform_limit (cball 0 R)
(λX z. ∑ω∈X. (z - ω) powr of_real (-of_nat α))
(λz. ∑⇩∞ω∈Λ-cball 0 R. (z - ω) powr of_real (-of_nat α))
(finite_subsets_at_top (Λ - cball 0 R))"
using assms by (intro weierstrass_aux_converges_uniformly_in_disk) auto
also have "?this ⟷ uniform_limit (cball 0 R) (λX z. ∑ω∈X. 1 / (z - ω) ^ α) (F α)
(finite_subsets_at_top (Λ - cball 0 R))"
using assms unfolding F_def
by (intro uniform_limit_cong eventually_finite_subsets_at_top_weakI)
(auto simp: powr_minus powr_nat field_simps intro!: sum.cong infsum_cong)
finally have 2: … .
have 3: "finite_subsets_at_top (Λ - cball 0 R) ≠ bot"
by simp
obtain g where g: "continuous_on (cball 0 R) (F α)"
"⋀w. w ∈ ball 0 R ⟹ (F α has_field_derivative g w) (at w) ∧
((λω. -of_nat α / (w - ω) ^ Suc α) has_sum g w) (Λ - cball 0 R)"
unfolding has_sum_def using has_complex_derivative_uniform_limit[OF 1 2 3 ‹R > 0›] by auto
have "((λω. -of_nat α * (1 / (w - ω) ^ Suc α)) has_sum -of_nat α * F (Suc α) w) (Λ - cball 0 R)"
unfolding F_def using assms
by (intro has_sum_cmult_right has_sum_infsum weierstrass_aux_converges') auto
moreover have "((λω. -of_nat α * (1 / (w - ω) ^ Suc α)) has_sum g w) (Λ - cball 0 R)"
using g(2)[of w] assms by simp
ultimately have "g w = -of_nat α * F (Suc α) w"
by (metis infsumI)
thus ?thesis
using g(2)[of w] assms by (simp add: F_def)
qed
lemma eisenstein_fun_aux_has_field_derivative:
assumes z: "z ∉ Λ⇧*" and n: "n ≥ 3"
shows "(eisenstein_fun_aux n has_field_derivative -of_nat n * eisenstein_fun_aux (Suc n) z) (at z)"
proof -
define R where "R = norm z + 1"
have R: "R > 0" "norm z < R"
by (auto simp: R_def add_nonneg_pos)
have "finite (Λ ∩ cball 0 R)"
by (simp add: bounded_lattice_finite)
moreover have "Λ⇧* ∩ cball 0 R ⊆ Λ ∩ cball 0 R"
unfolding lattice0_def by blast
ultimately have fin: "finite (Λ⇧* ∩ cball 0 R)"
using finite_subset by blast
define n' where "n' = n - 1"
from n have n': "n = Suc n'"
by (simp add: n'_def)
define F1 where "F1 = (λn z. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω) ^ n)"
define F2 where "F2 = (λn z. ∑ω∈Λ⇧*∩cball 0 R. 1 / (z - ω) ^ n)"
have "(F1 n has_field_derivative -of_nat n * F1 (Suc n) z) (at z)"
unfolding F1_def
by (rule eisenstein_fun_aux_has_field_derivative_aux) (use n in ‹auto simp: R_def add_nonneg_pos›)
moreover have "(F2 n has_field_derivative -of_nat n * F2 (Suc n) z) (at z)"
unfolding F2_def sum_distrib_left lattice0_def
by (rule derivative_eq_intros refl sum.cong | use R z n in ‹force simp: lattice0_def›)+
(simp add: divide_simps power3_eq_cube power4_eq_xxxx n')
ultimately have "((λz. F1 n z + F2 n z) has_field_derivative
(-of_nat n * F1 (Suc n) z) + (-of_nat n * F2 (Suc n) z)) (at z)"
by (intro derivative_intros)
also have "?this ⟷ (eisenstein_fun_aux n has_field_derivative (-of_nat n * F1 (Suc n) z) + (-of_nat n * F2 (Suc n) z)) (at z)"
proof (intro has_field_derivative_cong_ev refl)
have "eventually (λz'. z' ∈ -Λ⇧*) (nhds z)"
using z by (intro eventually_nhds_in_open) (auto simp: closed_lattice0)
thus "∀⇩F x in nhds z. x ∈ UNIV ⟶ F1 n x + F2 n x = eisenstein_fun_aux n x"
proof eventually_elim
case (elim z)
have "((λω. 1 / (z - ω) ^ n) has_sum (F1 n z + F2 n z)) ((Λ - cball 0 R) ∪ (Λ⇧* ∩ cball 0 R))"
unfolding F1_def F2_def using R fin n
by (intro has_sum_Un_disjoint[OF has_sum_infsum has_sum_finite]
summable_on_subset[OF weierstrass_aux_converges']) auto
also have "(Λ - cball 0 R) ∪ (Λ⇧* ∩ cball 0 R) = Λ⇧*"
using R unfolding lattice0_def by auto
finally show ?case using elim n
unfolding F1_def F2_def by (simp add: infsumI eisenstein_fun_aux_def)
qed
qed auto
also have "(-of_nat n * F1 (Suc n) z) + (-of_nat n * F2 (Suc n) z) = -of_nat n * (F1 (Suc n) z + F2 (Suc n) z)"
by (simp add: algebra_simps)
also have "F1 (Suc n) z + F2 (Suc n) z = eisenstein_fun_aux (Suc n) z"
proof -
have "((λω. 1 / (z - ω) ^ Suc n) has_sum (F1 (Suc n) z + F2 (Suc n) z)) ((Λ - cball 0 R) ∪ (Λ⇧* ∩ cball 0 R))"
unfolding F1_def F2_def using R fin n
by (intro has_sum_Un_disjoint[OF has_sum_infsum has_sum_finite] weierstrass_aux_converges') auto
also have "(Λ - cball 0 R) ∪ (Λ⇧* ∩ cball 0 R) = Λ⇧*"
using R unfolding lattice0_def by auto
finally show ?thesis using n z
unfolding F1_def F2_def eisenstein_fun_aux_def by (simp add: infsumI)
qed
finally show ?thesis .
qed
lemmas eisenstein_fun_aux_has_field_derivative' [derivative_intros] =
DERIV_chain2[OF eisenstein_fun_aux_has_field_derivative]
lemma higher_deriv_eisenstein_fun_aux:
assumes z: "z ∉ Λ⇧*" and n: "n ≥ 3"
shows "(deriv ^^ m) (eisenstein_fun_aux n) z =
(-1) ^ m * pochhammer (of_nat n) m * eisenstein_fun_aux (n + m) z"
using z n
proof (induction m arbitrary: z n)
case 0
thus ?case by simp
next
case (Suc m z n)
have ev: "eventually (λz. z ∈ -Λ⇧*) (nhds z)"
using Suc.prems closed_lattice0 by (intro eventually_nhds_in_open) auto
have "(deriv ^^ Suc m) (eisenstein_fun_aux n) z = deriv ((deriv ^^ m) (eisenstein_fun_aux n)) z"
by simp
also have "… = deriv (λz. (-1)^ m * pochhammer (of_nat n) m * eisenstein_fun_aux (n + m) z) z"
by (intro deriv_cong_ev eventually_mono[OF ev]) (use Suc in auto)
also have "… = (-1) ^ Suc m * pochhammer (of_nat n) (Suc m) * eisenstein_fun_aux (Suc (n + m)) z"
using Suc.prems
by (intro DERIV_imp_deriv)
(auto intro!: derivative_eq_intros simp: pochhammer_Suc algebra_simps)
finally show ?case
by simp
qed
lemma eisenstein_fun_aux_holomorphic: "eisenstein_fun_aux n holomorphic_on -Λ⇧*"
proof (cases "n ≥ 3")
case True
thus ?thesis
using closed_lattice0
by (subst holomorphic_on_open) (auto intro!: eisenstein_fun_aux_has_field_derivative)
next
case False
thus ?thesis
by (cases "n = 0") (auto simp: eisenstein_fun_aux_def [abs_def])
qed
lemma eisenstein_fun_aux_holomorphic' [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ⇧*"
shows "(λz. eisenstein_fun_aux n (f z)) holomorphic_on A"
proof -
have "eisenstein_fun_aux n ∘ f holomorphic_on A"
by (rule holomorphic_on_compose_gen assms eisenstein_fun_aux_holomorphic)+ (use assms in auto)
thus ?thesis by (simp add: o_def)
qed
lemma eisenstein_fun_aux_analytic: "eisenstein_fun_aux n analytic_on -Λ⇧*"
by (simp add: analytic_on_open closed_lattice0 open_Compl eisenstein_fun_aux_holomorphic)
lemma eisenstein_fun_aux_analytic' [analytic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ⇧*"
shows "(λz. eisenstein_fun_aux n (f z)) analytic_on A"
proof -
have "eisenstein_fun_aux n ∘ f analytic_on A"
by (rule analytic_on_compose_gen assms eisenstein_fun_aux_analytic)+ (use assms in auto)
thus ?thesis by (simp add: o_def)
qed
lemma eisenstein_fun_aux_continuous_on: "continuous_on (-Λ⇧*) (eisenstein_fun_aux n)"
using holomorphic_on_imp_continuous_on eisenstein_fun_aux_holomorphic by blast
lemma eisenstein_fun_aux_continuous_on' [continuous_intros]:
assumes "continuous_on A f" "⋀z. z ∈ A ⟹ f z ∉ Λ⇧*"
shows "continuous_on A (λz. eisenstein_fun_aux n (f z))"
by (rule continuous_on_compose2[OF eisenstein_fun_aux_continuous_on assms(1)]) (use assms in auto)
lemma weierstrass_aux_translate:
fixes α :: real
assumes "α > 2"
shows "(∑⇩∞ω∈Λ. (z + w - ω) powr -α) = (∑⇩∞ω∈(+) (-w) ` Λ. (z - ω) powr -α)"
by (subst infsum_reindex) (auto simp: o_def algebra_simps)
lemma weierstrass_aux_holomorphic:
assumes "α > 2" "Λ' ⊆ Λ" "finite (Λ - Λ')"
shows "(λz. ∑⇩∞ω∈Λ'. 1 / (z - ω) ^ α) holomorphic_on -Λ'"
proof -
define M where "M = Max (insert 0 (norm ` (Λ - Λ')))"
have M: "M ≥ 0" "⋀ω. ω ∈ Λ - Λ' ⟹ M ≥ norm ω"
using assms by (auto simp: M_def)
have [simp]: "closed Λ'"
using assms(2) by (rule closed_subset_lattice)
have *: "(λz. ∑⇩∞ω∈Λ'. 1 / (z - ω) ^ α) holomorphic_on ball 0 R - Λ'" if R: "R > M" for R
proof -
define F where "F = (λα z. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω) ^ α)"
define G where "G = (λα z. ∑ω∈Λ'∩cball 0 R. 1 / (z - ω) ^ α)"
have "(F α has_field_derivative -of_nat α * F (Suc α) z) (at z)" if z: "z ∈ ball 0 R" for z
unfolding F_def using assms R M(1) z by (intro eisenstein_fun_aux_has_field_derivative_aux) auto
hence "F α holomorphic_on ball 0 R - Λ'"
using holomorphic_on_open ‹closed Λ'› by blast
hence "(λz. F α z + G α z) holomorphic_on ball 0 R - Λ'"
unfolding G_def using assms M R by (intro holomorphic_intros) auto
also have "(λz. F α z + G α z) = (λz. ∑⇩∞ω∈Λ'. 1 / (z - ω) ^ α)"
proof
fix z :: complex
have "finite (Λ ∩ cball 0 R)"
by (intro bounded_lattice_finite) auto
moreover have "Λ' ∩ cball 0 R ⊆ Λ ∩ cball 0 R"
using assms by blast
ultimately have "finite (Λ' ∩ cball 0 R)"
using finite_subset by blast
hence "((λω. 1 / (z - ω) ^ α) has_sum (F α z + G α z)) ((Λ - cball 0 R) ∪ (Λ' ∩ cball 0 R))"
unfolding F_def G_def using assms
by (intro has_sum_Un_disjoint[OF has_sum_infsum has_sum_finite] weierstrass_aux_converges') auto
also have "(Λ - cball 0 R) ∪ (Λ' ∩ cball 0 R) = Λ'"
using M R assms by (force simp: not_le)
finally show "F α z + G α z = (∑⇩∞ω∈Λ'. 1 / (z - ω) ^ α)"
by (simp add: infsumI)
qed
finally show ?thesis .
qed
have "(λz. ∑⇩∞ω∈Λ'. 1 / (z - ω) ^ α) holomorphic_on (⋃R∈{R. R > M}. ball 0 R - Λ')"
by (rule holomorphic_on_UN_open) (use * ‹closed Λ'› in auto)
also have "… = (⋃R∈{R. R > M}. ball 0 R) - Λ'"
by blast
also have "(⋃R∈{R. R > M}. ball 0 R) = (UNIV :: complex set)"
proof (safe intro!: UN_I)
fix z :: complex
show "norm z + M + 1 > M" "z ∈ ball 0 (norm z + M + 1)"
using M(1) by (auto intro: add_nonneg_pos)
qed auto
finally show ?thesis
by (simp add: Compl_eq_Diff_UNIV)
qed
definition eisenstein_fun :: "nat ⇒ complex ⇒ complex" where
"eisenstein_fun n z = (if n < 3 ∨ z ∈ Λ then 0 else (∑⇩∞ω∈Λ. 1 / (z - ω) ^ n))"
lemma eisenstein_fun_has_sum:
"n ≥ 3 ⟹ z ∉ Λ ⟹ ((λω. 1 / (z - ω) ^ n) has_sum eisenstein_fun n z) Λ"
unfolding eisenstein_fun_def by (auto intro!: has_sum_infsum weierstrass_aux_converges')
lemma eisenstein_fun_at_pole_eq_0: "z ∈ Λ ⟹ eisenstein_fun n z = 0"
by (simp add: eisenstein_fun_def)
lemma eisenstein_fun_conv_eisenstein_fun_aux:
assumes "n ≥ 3" "z ∉ Λ"
shows "eisenstein_fun n z = eisenstein_fun_aux n z + 1 / z ^ n"
proof -
from assms have "eisenstein_fun n z = (∑⇩∞ω∈insert 0 Λ⇧*. 1 / (z - ω) ^ n)"
by (simp add: eisenstein_fun_def lattice_lattice0)
also from assms have "… = (∑⇩∞ω∈Λ⇧*. 1 / (z - ω) ^ n) + 1 / z ^ n"
by (subst infsum_insert) (auto intro!: weierstrass_aux_converges' simp: lattice_lattice0)
also from assms have "… = eisenstein_fun_aux n z + 1 / z ^ n"
by (simp add: eisenstein_fun_aux_def lattice_lattice0)
finally show ?thesis .
qed
lemma eisenstein_fun_altdef:
"eisenstein_fun n z = (if n < 3 ∨ z ∈ Λ then 0 else eisenstein_fun_aux n z + 1 / z ^ n)"
using eisenstein_fun_conv_eisenstein_fun_aux[of n z]
by (auto simp: eisenstein_fun_def eisenstein_fun_aux_def lattice0_def)
lemma eisenstein_fun_minus: "eisenstein_fun n (-z) = (-1) ^ n * eisenstein_fun n z"
by (auto simp: eisenstein_fun_altdef eisenstein_fun_aux_minus lattice0_def uminus_in_lattice_iff
power_minus' divide_simps)
(auto simp: algebra_simps)
lemma eisenstein_fun_even_minus: "even n ⟹ eisenstein_fun n (-z) = eisenstein_fun n z"
by (simp add: eisenstein_fun_minus)
lemma eisenstein_fun_odd_minus: "odd n ⟹ eisenstein_fun n (-z) = -eisenstein_fun n z"
by (simp add: eisenstein_fun_minus)
lemma eisenstein_fun_has_field_derivative:
assumes "n ≥ 3" "z ∉ Λ"
shows "(eisenstein_fun n has_field_derivative -of_nat n * eisenstein_fun (Suc n) z) (at z)"
proof -
define n' where "n' = n - 1"
have n': "n = Suc n'"
using assms by (simp add: n'_def)
have ev: "eventually (λz. z ∈ -Λ) (nhds z)"
using assms closed_lattice by (intro eventually_nhds_in_open) auto
have "((λz. eisenstein_fun_aux n z + 1 / z ^ n) has_field_derivative
-of_nat n * eisenstein_fun (Suc n) z) (at z)"
using assms
apply (auto intro!: derivative_eq_intros)
apply (auto simp: eisenstein_fun_conv_eisenstein_fun_aux lattice_lattice0 field_simps n')
done
also have "?this ⟷ ?thesis"
using assms by (intro has_field_derivative_cong_ev refl eventually_mono[OF ev])
(auto simp: eisenstein_fun_conv_eisenstein_fun_aux)
finally show ?thesis .
qed
lemmas eisenstein_fun_has_field_derivative' [derivative_intros] =
DERIV_chain2[OF eisenstein_fun_has_field_derivative]
lemma eisenstein_fun_holomorphic: "eisenstein_fun n holomorphic_on -Λ"
proof (cases "n ≥ 3")
case True
thus ?thesis using closed_lattice
by (subst holomorphic_on_open) (auto intro!: eisenstein_fun_has_field_derivative)
qed (auto simp: eisenstein_fun_def [abs_def])
lemma higher_deriv_eisenstein_fun:
assumes z: "z ∉ Λ" and n: "n ≥ 3"
shows "(deriv ^^ m) (eisenstein_fun n) z =
(-1) ^ m * pochhammer (of_nat n) m * eisenstein_fun (n + m) z"
using z n
proof (induction m arbitrary: z n)
case 0
thus ?case by simp
next
case (Suc m z n)
have ev: "eventually (λz. z ∈ -Λ) (nhds z)"
using Suc.prems closed_lattice by (intro eventually_nhds_in_open) auto
have "(deriv ^^ Suc m) (eisenstein_fun n) z = deriv ((deriv ^^ m) (eisenstein_fun n)) z"
by simp
also have "… = deriv (λz. (-1)^ m * pochhammer (of_nat n) m * eisenstein_fun (n + m) z) z"
by (intro deriv_cong_ev eventually_mono[OF ev]) (use Suc in auto)
also have "… = (-1) ^ Suc m * pochhammer (of_nat n) (Suc m) * eisenstein_fun (Suc (n + m)) z"
using Suc.prems
by (intro DERIV_imp_deriv)
(auto intro!: derivative_eq_intros simp: pochhammer_Suc algebra_simps)
finally show ?case
by simp
qed
lemma eisenstein_fun_holomorphic' [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ n < 3 ∨ f z ∉ Λ"
shows "(λz. eisenstein_fun n (f z)) holomorphic_on A"
proof (cases "n ≥ 3")
case True
have "eisenstein_fun n ∘ f holomorphic_on A"
by (rule holomorphic_on_compose_gen assms eisenstein_fun_holomorphic)+ (use assms True in auto)
thus ?thesis by (simp add: o_def)
qed (auto simp: eisenstein_fun_def)
lemma eisenstein_fun_analytic: "eisenstein_fun n analytic_on -Λ"
by (simp add: analytic_on_open closed_lattice open_Compl eisenstein_fun_holomorphic)
lemma eisenstein_fun_analytic' [analytic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ n < 3 ∨ f z ∉ Λ"
shows "(λz. eisenstein_fun n (f z)) analytic_on A"
proof (cases "n ≥ 3")
case True
have "eisenstein_fun n ∘ f analytic_on A"
by (rule analytic_on_compose_gen assms True eisenstein_fun_analytic)+ (use assms True in auto)
thus ?thesis by (simp add: o_def)
qed (auto simp: eisenstein_fun_def)
lemma eisenstein_fun_continuous_on: "n ≥ 3 ⟹ continuous_on (-Λ) (eisenstein_fun n)"
using holomorphic_on_imp_continuous_on eisenstein_fun_holomorphic by blast
lemma eisenstein_fun_continuous_on' [continuous_intros]:
assumes "continuous_on A f" "⋀z. z ∈ A ⟹ n < 3 ∨ f z ∉ Λ"
shows "continuous_on A (λz. eisenstein_fun n (f z))"
proof (cases "n ≥ 3")
case True
show ?thesis
by (rule continuous_on_compose2[OF eisenstein_fun_continuous_on assms(1)])
(use assms True in auto)
qed (auto simp: eisenstein_fun_def)
sublocale eisenstein_fun: complex_lattice_periodic ω1 ω2 "eisenstein_fun n"
proof
have *: "eisenstein_fun n (w + z) = eisenstein_fun n w" if "z ∈ Λ" for w z
proof (cases "n ≥ 3 ∧ w ∉ Λ")
case True
show ?thesis
proof (rule has_sum_unique)
show "((λω. 1 / (w - ω) ^ n) has_sum eisenstein_fun n w) Λ"
by (rule eisenstein_fun_has_sum) (use True in auto)
next
have "((λω. 1 / (w + z - ω) ^ n) has_sum eisenstein_fun n (w + z)) Λ"
by (rule eisenstein_fun_has_sum) (use True that in auto)
also have "?this ⟷ ((λω. 1 / (w - ω) ^ n) has_sum eisenstein_fun n (w + z)) Λ"
by (rule has_sum_reindex_bij_witness[of _ "(+) z" "(+) (-z)"])
(use that in ‹auto intro!: lattice_intros simp: algebra_simps›)
finally show "((λω. 1 / (w - ω) ^ n) has_sum eisenstein_fun n (w + z)) Λ" .
qed
qed (use that in ‹auto simp: eisenstein_fun_def›)
show "eisenstein_fun n (z + ω1) = eisenstein_fun n z"
"eisenstein_fun n (z + ω2) = eisenstein_fun n z" for z
by (rule *; simp)+
qed
lemma is_pole_eisenstein_fun:
assumes "n ≥ 3" "z ∈ Λ"
shows "is_pole (eisenstein_fun n) z"
proof -
have "eisenstein_fun_aux n ─0→ eisenstein_fun_aux n 0"
by (rule isContD, rule analytic_at_imp_isCont) (auto intro!: analytic_intros)
moreover have "is_pole (λw. 1 / w ^ n :: complex) 0"
using assms is_pole_inverse_power[of n 0] by simp
ultimately have "is_pole (λw. eisenstein_fun_aux n w + 1 / w ^ n) 0"
unfolding is_pole_def by (rule tendsto_add_filterlim_at_infinity)
also have "eventually (λw. w ∉ Λ) (at 0)"
using not_islimpt_lattice by (auto simp: islimpt_iff_eventually)
hence "eventually (λw. eisenstein_fun_aux n w + 1 / w ^ n = eisenstein_fun n w) (at 0)"
by eventually_elim (use assms in ‹auto simp: eisenstein_fun_altdef›)
hence "is_pole (λw. eisenstein_fun_aux n w + 1 / w ^ n) 0 ⟷ is_pole (eisenstein_fun n) 0"
by (intro is_pole_cong) auto
also have "eisenstein_fun n = eisenstein_fun n ∘ (λw. w + z)"
using assms by (auto simp: fun_eq_iff simp: rel_def uminus_in_lattice_iff eisenstein_fun.lattice_cong)
also have "is_pole … 0 ⟷ is_pole (eisenstein_fun n) z"
by (simp add: is_pole_shift_0' o_def add.commute)
finally show ?thesis .
qed
sublocale eisenstein_fun: nicely_elliptic_function ω1 ω2 "eisenstein_fun n"
proof
show "eisenstein_fun n nicely_meromorphic_on UNIV"
proof (cases "n ≥ 3")
case True
show ?thesis
proof (rule nicely_meromorphic_onI_open)
show "eisenstein_fun n analytic_on UNIV - Λ"
using eisenstein_fun_analytic[of n] by (simp add: Compl_eq_Diff_UNIV)
show "is_pole (eisenstein_fun n) z ∧ eisenstein_fun n z = 0" if "z ∈ Λ" for z
using that by (simp add: True eisenstein_fun_def is_pole_eisenstein_fun)
show "isolated_singularity_at (eisenstein_fun n) z" for z
proof (rule analytic_nhd_imp_isolated_singularity[of _ "-(Λ-{z})"])
show "open (- (Λ - {z}))"
by (intro open_Compl closed_subset_lattice) auto
qed (auto intro!: analytic_intros)
qed simp
qed (auto simp: eisenstein_fun_def [abs_def] intro!: analytic_on_imp_nicely_meromorphic_on)
qed
lemmas [elliptic_function_intros] =
eisenstein_fun.elliptic_function_axioms eisenstein_fun.nicely_elliptic_function_axioms
end
subsection ‹Definition and basic properties›
text ‹
The Weierstra\ss\ ‹℘› function is in a sense the most basic elliptic function, and we will see
later on that all elliptic function can be written as a combination of ‹℘› and ‹℘'›.
Its derivative, as we noted before, is equal to our Eisenstein function for $n = 3$ (up to
a constant factor $-2$). The function ‹℘› itself is somewhat more awkward to define.
›
context complex_lattice begin
lemma minus_lattice_eq: "uminus ` Λ = Λ"
proof -
have "uminus ` Λ ⊆ Λ"
by (auto simp: uminus_in_lattice_iff)
then show ?thesis
using equation_minus_iff by blast
qed
lemma minus_latticemz_eq: "uminus ` Λ⇧* = Λ⇧*"
by (simp add: lattice0_def inj_on_def image_set_diff minus_lattice_eq)
lemma bij_minus_latticemz: "bij_betw uminus Λ⇧* Λ⇧*"
by (simp add: bij_betw_def inj_on_def minus_latticemz_eq)
definition weierstrass_fun_deriv ("℘''") where
"weierstrass_fun_deriv z = -2 * eisenstein_fun 3 z"
sublocale weierstrass_fun_deriv: elliptic_function ω1 ω2 weierstrass_fun_deriv
unfolding weierstrass_fun_deriv_def by (intro elliptic_function_intros)
sublocale weierstrass_fun_deriv: nicely_elliptic_function ω1 ω2 weierstrass_fun_deriv
proof
show "℘' nicely_meromorphic_on UNIV"
using eisenstein_fun.nicely_meromorphic unfolding weierstrass_fun_deriv_def
by (intro nicely_meromorphic_on_uminus nicely_meromorphic_on_cmult_left)
qed
lemmas [elliptic_function_intros] =
weierstrass_fun_deriv.elliptic_function_axioms weierstrass_fun_deriv.nicely_elliptic_function_axioms
lemma weierstrass_fun_deriv_minus [simp]: "℘' (-z) = -℘' z"
by (simp add: weierstrass_fun_deriv_def eisenstein_fun_odd_minus)
lemma weierstrass_fun_deriv_has_field_derivative:
assumes "z ∉ Λ"
shows "(℘' has_field_derivative 6 * eisenstein_fun 4 z) (at z)"
unfolding weierstrass_fun_deriv_def
using assms by (auto intro!: derivative_eq_intros)
lemma weierstrass_fun_deriv_holomorphic: "℘' holomorphic_on -Λ"
unfolding weierstrass_fun_deriv_def by (auto intro!: holomorphic_intros)
lemma weierstrass_fun_deriv_holomorphic' [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ"
shows "(λz. ℘' (f z)) holomorphic_on A"
using assms unfolding weierstrass_fun_deriv_def by (auto intro!: holomorphic_intros)
lemma weierstrass_fun_deriv_analytic: "℘' analytic_on -Λ"
unfolding weierstrass_fun_deriv_def by (auto intro!: analytic_intros)
lemma weierstrass_fun_deriv_analytic' [analytic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ"
shows "(λz. ℘' (f z)) analytic_on A"
using assms unfolding weierstrass_fun_deriv_def by (auto intro!: analytic_intros)
lemma weierstrass_fun_deriv_continuous_on: "continuous_on (-Λ) ℘'"
unfolding weierstrass_fun_deriv_def by (auto intro!: continuous_intros)
lemma weierstrass_fun_deriv_continuous_on' [continuous_intros]:
assumes "continuous_on A f" "⋀z. z ∈ A ⟹ f z ∉ Λ"
shows "continuous_on A (λz. ℘' (f z))"
using assms unfolding weierstrass_fun_deriv_def by (auto intro!: continuous_intros)
lemma tendsto_weierstrass_fun_deriv [tendsto_intros]:
assumes "(f ⤏ c) F" "c ∉ Λ"
shows "((λz. ℘' (f z)) ⤏ ℘' c) F"
proof (rule continuous_on_tendsto_compose[OF _ assms(1)])
show "continuous_on (-Λ) ℘'"
by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto
show "eventually (λz. f z ∈ -Λ) F"
by (rule eventually_compose_filterlim[OF _ assms(1)], rule eventually_nhds_in_open)
(use assms(2) in ‹auto intro: closed_lattice›)
qed (use assms(2) in auto)
text ‹
The following is the Weierstra\ss\ function minus its pole at the origin. By convention, it
returns 0 at all its remaining poles.
›
definition weierstrass_fun_aux :: "complex ⇒ complex" where
"weierstrass_fun_aux z = (if z ∈ Λ⇧* then 0 else (∑⇩∞ ω ∈ Λ⇧*. 1 / (z - ω)⇧2 - 1 / ω⇧2))"
text ‹
This is now the Weierstra\ss\ function. Again, it returns 0 at all its poles.
›
definition weierstrass_fun :: "complex ⇒ complex" ("℘")
where "℘ z = (if z ∈ Λ then 0 else 1 / z⇧2 + weierstrass_fun_aux z)"
lemma weierstrass_fun_aux_0 [simp]: "weierstrass_fun_aux 0 = 0"
by (simp add: weierstrass_fun_aux_def)
lemma weierstrass_fun_at_pole: "ω ∈ Λ ⟹ ℘ ω = 0"
by (simp add: weierstrass_fun_def)
lemma
fixes R :: real
assumes "R > 0"
shows weierstrass_fun_aux_converges_absolutely_uniformly_in_disk:
"uniform_limit (cball 0 R)
(λX z. ∑ω∈X. norm (1 / (z - ω)⇧2 - 1 / ω⇧2))
(λz. ∑⇩∞ω∈Λ-cball 0 R. norm (1 / (z - ω)⇧2 - 1 / ω⇧2))
(finite_subsets_at_top (Λ - cball 0 R))" (is ?th1)
and weierstrass_fun_aux_converges_uniformly_in_disk:
"uniform_limit (cball 0 R)
(λX z. ∑ω∈X. 1 / (z - ω)⇧2 - 1 / ω⇧2)
(λz. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω)⇧2 - 1 / ω⇧2)
(finite_subsets_at_top (Λ - cball 0 R))" (is ?th2)
proof -
obtain M where M:
"M > 0" "⋀ω z. ⟦ω ∈ Λ; norm ω > R; norm z ≤ R⟧ ⟹ norm (z - ω) powr -2 ≤ M * norm ω powr -2"
using weierstrass_summand_bound[of 2 R] assms by auto
have 1: "(λω. 3 * M * R * norm ω powr -3) summable_on (Λ - cball 0 R)"
proof -
have "(λω. 1 / norm ω powr 3) summable_on Λ⇧*"
using assms by (subst converges_absolutely_iff) auto
hence "(λω. 3 * M * R * norm ω powr -3) summable_on Λ⇧*"
by (intro summable_on_cmult_right) (auto simp: powr_minus field_simps)
thus "(λω. 3 * M * R * norm ω powr -3) summable_on (Λ - cball 0 R)"
by (rule summable_on_subset) (use assms in ‹auto simp: lattice0_def›)
qed
have 2: "norm (1 / (z - ω)⇧2 - 1 / ω⇧2) ≤ 3 * M * R * norm ω powr -3"
if "ω ∈ Λ - cball 0 R" "z ∈ cball 0 R" for ω z
proof -
from that have nz: "ω ≠ 0" "ω ≠ z"
using ‹R > 0› by auto
hence "1 / (z - ω)⇧2 - 1 / ω⇧2 = z * (2 * ω - z) / (ω⇧2 * (z - ω)⇧2)"
using that by (auto simp: field_simps) (auto simp: power2_eq_square algebra_simps)
also have "norm … = norm z * norm (2 * ω - z) / norm ω ^ 2 * norm (z - ω) powr - 2"
by (simp add: norm_divide norm_mult norm_power powr_minus divide_simps)
also have "… ≤ R * (2 * norm ω + norm z) / norm ω ^ 2 * (M * norm ω powr -2)"
using assms that
by (intro mult_mono frac_le mult_nonneg_nonneg M order.trans[OF norm_triangle_ineq4]) auto
also have "… = M * R * (2 + norm z / norm ω) / norm ω ^ 3"
using nz by (simp add: field_simps powr_minus power2_eq_square power3_eq_cube)
also have "… ≤ M * R * 3 / norm ω ^ 3"
using nz assms M(1) that by (intro mult_left_mono divide_right_mono) auto
finally show ?thesis
by (simp add: field_simps powr_minus)
qed
show ?th1 ?th2 unfolding weierstrass_fun_aux_def
by (rule Weierstrass_m_test_general[OF _ 1]; use 2 in simp)+
qed
lemma weierstrass_fun_has_field_derivative_aux:
fixes R :: real
defines "F ≡ (λz. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω)⇧2 - 1 / ω⇧2)"
defines "F' ≡ (λz. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω) ^ 3)"
assumes "R > 0" "w ∈ ball 0 R"
shows "(F has_field_derivative -2 * F' w) (at w)"
proof -
have 1: "∀⇩F n in finite_subsets_at_top (Λ - cball 0 R).
continuous_on (cball 0 R) (λz. ∑ω∈n. 1 / (z - ω)⇧2 - 1 / ω⇧2) ∧
(∀z∈ball 0 R. ((λz. ∑ω∈n. 1 / (z - ω)⇧2 - 1 / ω⇧2) has_field_derivative (∑ω∈n. -2 / (z - ω)^3)) (at z))"
apply (intro eventually_finite_subsets_at_top_weakI conjI continuous_intros derivative_intros ballI)
apply force
apply (rule derivative_eq_intros refl | force)+
apply (simp add: divide_simps, simp add: algebra_simps power4_eq_xxxx power3_eq_cube)
done
have "uniform_limit (cball 0 R)
(λX z. ∑ω∈X. 1 / (z - ω)⇧2 - 1 / ω⇧2)
(λz. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω)⇧2 - 1 / ω⇧2)
(finite_subsets_at_top (Λ - cball 0 R))"
using assms by (intro weierstrass_fun_aux_converges_uniformly_in_disk) auto
also have "?this ⟷ uniform_limit (cball 0 R) (λX z. ∑ω∈X. 1 / (z - ω)⇧2 - 1 / ω⇧2) F
(finite_subsets_at_top (Λ - cball 0 R))"
using assms unfolding F_def
by (intro uniform_limit_cong eventually_finite_subsets_at_top_weakI)
(auto simp: powr_minus powr_nat field_simps intro!: sum.cong infsum_cong)
finally have 2: … .
have 3: "finite_subsets_at_top (Λ - cball 0 R) ≠ bot"
by simp
obtain g where g: "continuous_on (cball 0 R) F"
"⋀w. w ∈ ball 0 R ⟹ (F has_field_derivative g w) (at w) ∧
((λω. -2 / (w - ω) ^ 3) has_sum g w) (Λ - cball 0 R)"
unfolding has_sum_def using has_complex_derivative_uniform_limit[OF 1 2 3 ‹R > 0›] by auto
have "((λω. (-2) * (1 / (w - ω) ^ 3)) has_sum (-2) * F' w) (Λ - cball 0 R)"
unfolding F'_def using assms
by (intro has_sum_cmult_right has_sum_infsum weierstrass_aux_converges_in_disk') auto
moreover have "((λω. -2 * (1 / (w - ω) ^ 3)) has_sum g w) (Λ - cball 0 R)"
using g(2)[of w] assms by simp
ultimately have "g w = -2 * F' w"
by (metis infsumI)
thus "(F has_field_derivative -2 * F' w) (at w)"
using g(2)[of w] assms by simp
qed
lemma norm_summable_weierstrass_fun_aux: "(λω. norm (1 / (z - ω)⇧2 - 1 / ω⇧2)) summable_on Λ"
proof -
define R where "R = norm z + 1"
have "(λω. norm (1 / (z - ω)⇧2 - 1 / ω⇧2)) summable_on (Λ - cball 0 R)"
unfolding summable_iff_has_sum_infsum has_sum_def
by (rule tendsto_uniform_limitI[OF weierstrass_fun_aux_converges_absolutely_uniformly_in_disk])
(auto simp: R_def add_nonneg_pos)
hence "(λω. norm (1 / (z - ω)⇧2 - 1 / ω⇧2)) summable_on ((Λ - cball 0 R) ∪ (Λ ∩ cball 0 R))"
by (intro summable_on_union[OF _ summable_on_finite]) (auto simp: bounded_lattice_finite)
also have "… = Λ"
by blast
finally show ?thesis .
qed
lemma summable_weierstrass_fun_aux: "(λω. 1 / (z - ω)⇧2 - 1 / ω⇧2) summable_on Λ"
using norm_summable_weierstrass_fun_aux by (rule abs_summable_summable)
lemma weierstrass_summable: "(λω. 1 / (z - ω)⇧2 - 1 / ω⇧2) summable_on Λ⇧*"
by (rule summable_on_subset[OF summable_weierstrass_fun_aux]) (auto simp: lattice0_def)
lemma weierstrass_fun_aux_has_sum:
"z ∉ Λ⇧* ⟹ ((λω. 1 / (z - ω)⇧2 - 1 / ω⇧2) has_sum weierstrass_fun_aux z) Λ⇧*"
unfolding weierstrass_fun_aux_def by (simp add: weierstrass_summable)
lemma weierstrass_fun_aux_has_field_derivative:
defines "F ≡ weierstrass_fun_aux"
defines "F' ≡ (λz. ∑⇩∞ω∈Λ⇧*. 1 / (z - ω) ^ 3)"
assumes z: "z ∉ Λ⇧*"
shows "(F has_field_derivative -2 * eisenstein_fun_aux 3 z) (at z)"
proof -
define R where "R = norm z + 1"
have R: "R > 0" "norm z < R"
by (auto simp: R_def add_nonneg_pos)
have "finite (Λ ∩ cball 0 R)"
by (simp add: bounded_lattice_finite)
moreover have "Λ⇧* ∩ cball 0 R ⊆ Λ ∩ cball 0 R"
unfolding lattice0_def by blast
ultimately have fin: "finite (Λ⇧* ∩ cball 0 R)"
using finite_subset by blast
define F1 where "F1 = (λz. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω)⇧2 - 1 / ω⇧2)"
define F'1 where "F'1 = (λz. ∑⇩∞ω∈Λ-cball 0 R. 1 / (z - ω) ^ 3)"
define F2 where "F2 = (λz. ∑ω∈Λ⇧*∩cball 0 R. 1 / (z - ω)⇧2 - 1 / ω⇧2)"
define F'2 where "F'2 = (λz. ∑ω∈Λ⇧*∩cball 0 R. 1 / (z - ω) ^ 3)"
have "(F1 has_field_derivative -2 * F'1 z) (at z)"
unfolding F1_def F'1_def
by (rule weierstrass_fun_has_field_derivative_aux) (auto simp: R_def add_nonneg_pos)
moreover have "(F2 has_field_derivative -2 * F'2 z) (at z)"
unfolding F2_def F'2_def sum_distrib_left lattice0_def
by (rule derivative_eq_intros refl sum.cong | use R z in ‹force simp: lattice0_def›)+
(simp add: divide_simps power3_eq_cube power4_eq_xxxx)
ultimately have "((λz. F1 z + F2 z) has_field_derivative (-2 * F'1 z) + (-2 * F'2 z)) (at z)"
by (intro derivative_intros)
also have "?this ⟷ (F has_field_derivative (-2 * F'1 z) + (-2 * F'2 z)) (at z)"
proof (intro has_field_derivative_cong_ev refl)
have "eventually (λz'. z' ∈ -Λ⇧*) (nhds z)"
using z by (intro eventually_nhds_in_open) (auto simp: closed_lattice0)
thus "∀⇩F x in nhds z. x ∈ UNIV ⟶ F1 x + F2 x = F x"
proof eventually_elim
case (elim z)
have "((λω. 1 / (z - ω)^2 - 1 / ω^2) has_sum (F1 z + F2 z)) ((Λ - cball 0 R) ∪ (Λ⇧* ∩ cball 0 R))"
unfolding F1_def F2_def using R fin
by (intro has_sum_Un_disjoint[OF has_sum_infsum has_sum_finite]
summable_on_subset_banach[OF summable_weierstrass_fun_aux]) auto
also have "(Λ - cball 0 R) ∪ (Λ⇧* ∩ cball 0 R) = Λ⇧*"
using R unfolding lattice0_def by auto
finally show ?case using elim
unfolding F1_def F2_def F_def weierstrass_fun_aux_def by (simp add: infsumI)
qed
qed auto
also have "(-2 * F'1 z) + (-2 * F'2 z) = -2 * (F'1 z + F'2 z)"
by (simp add: algebra_simps)
also have "F'1 z + F'2 z = F' z"
proof -
have "((λω. 1 / (z - ω)^3) has_sum (F'1 z + F'2 z)) ((Λ - cball 0 R) ∪ (Λ⇧* ∩ cball 0 R))"
unfolding F'1_def F'2_def using R fin
by (intro has_sum_Un_disjoint [OF has_sum_infsum has_sum_finite] weierstrass_aux_converges') auto
also have "(Λ - cball 0 R) ∪ (Λ⇧* ∩ cball 0 R) = Λ⇧*"
using R unfolding lattice0_def by auto
finally show "F'1 z + F'2 z = F' z"
unfolding F'1_def F'2_def F'_def by (simp add: infsumI)
qed
finally show ?thesis
using assms by (simp add: eisenstein_fun_aux_def)
qed
lemmas weierstrass_fun_aux_has_field_derivative' [derivative_intros] =
weierstrass_fun_aux_has_field_derivative [THEN DERIV_chain2]
lemma weierstrass_fun_aux_holomorphic: "weierstrass_fun_aux holomorphic_on -Λ⇧*"
by (subst holomorphic_on_open)
(auto intro!: weierstrass_fun_aux_has_field_derivative simp: closed_lattice0)
lemma weierstrass_fun_aux_holomorphic' [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ⇧*"
shows "(λz. weierstrass_fun_aux (f z)) holomorphic_on A"
proof -
have "weierstrass_fun_aux ∘ f holomorphic_on A"
by (rule holomorphic_on_compose_gen assms weierstrass_fun_aux_holomorphic)+ (use assms in auto)
thus ?thesis by (simp add: o_def)
qed
lemma weierstrass_fun_aux_continuous_on: "continuous_on (-Λ⇧*) weierstrass_fun_aux"
using holomorphic_on_imp_continuous_on weierstrass_fun_aux_holomorphic by blast
lemma weierstrass_fun_aux_continuous_on' [continuous_intros]:
assumes "continuous_on A f" "⋀z. z ∈ A ⟹ f z ∉ Λ⇧*"
shows "continuous_on A (λz. weierstrass_fun_aux (f z))"
by (rule continuous_on_compose2[OF weierstrass_fun_aux_continuous_on assms(1)]) (use assms in auto)
lemma weierstrass_fun_aux_analytic: "weierstrass_fun_aux analytic_on -Λ⇧*"
by (simp add: analytic_on_open closed_lattice0 open_Compl weierstrass_fun_aux_holomorphic)
lemma weierstrass_fun_aux_analytic' [analytic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ⇧*"
shows "(λz. weierstrass_fun_aux (f z)) analytic_on A"
proof -
have "weierstrass_fun_aux ∘ f analytic_on A"
by (rule analytic_on_compose_gen assms weierstrass_fun_aux_analytic)+ (use assms in auto)
thus ?thesis by (simp add: o_def)
qed
lemma deriv_weierstrass_fun_aux:
"z ∉ Λ⇧* ⟹ deriv weierstrass_fun_aux z = -2 * eisenstein_fun_aux 3 z"
by (rule DERIV_imp_deriv derivative_eq_intros refl | assumption)+ simp
lemma weierstrass_fun_has_field_derivative:
fixes R :: real
assumes z: "z ∉ Λ"
shows "(℘ has_field_derivative ℘' z) (at z)"
proof -
note [derivative_intros] = weierstrass_fun_aux_has_field_derivative
from z have [simp]: "z ≠ 0" "z ∉ Λ⇧*"
by (auto simp: lattice0_def)
define D where "D = -2 / z ^ 3 - 2 * eisenstein_fun_aux 3 z"
have "((λz. 1 / z⇧2 + weierstrass_fun_aux z) has_field_derivative D) (at z)" unfolding D_def
by (rule derivative_eq_intros refl | simp)+ (simp add: divide_simps power3_eq_cube power4_eq_xxxx)
also have "?this ⟷ (weierstrass_fun has_field_derivative D) (at z)"
proof (intro has_field_derivative_cong_ev refl)
have "eventually (λz. z ∈ -Λ) (nhds z)"
using closed_lattice z by (intro eventually_nhds_in_open) auto
thus "eventually (λz. z ∈ UNIV ⟶ 1 / z ^ 2 + weierstrass_fun_aux z = ℘ z) (nhds z)"
by eventually_elim (simp add: weierstrass_fun_def)
qed auto
also have "D = -2 * eisenstein_fun 3 z"
using z by (simp add: eisenstein_fun_conv_eisenstein_fun_aux D_def)
finally show ?thesis by (simp add: weierstrass_fun_deriv_def)
qed
lemmas weierstrass_fun_has_field_derivative' [derivative_intros] =
weierstrass_fun_has_field_derivative [THEN DERIV_chain2]
lemma weierstrass_fun_holomorphic: "℘ holomorphic_on -Λ"
by (subst holomorphic_on_open)
(auto intro!: weierstrass_fun_has_field_derivative simp: closed_lattice)
lemma weierstrass_fun_holomorphic' [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ"
shows "(λz. weierstrass_fun (f z)) holomorphic_on A"
proof -
have "weierstrass_fun ∘ f holomorphic_on A"
by (rule holomorphic_on_compose_gen assms weierstrass_fun_holomorphic)+ (use assms in auto)
thus ?thesis by (simp add: o_def)
qed
lemma weierstrass_fun_analytic: "℘ analytic_on -Λ"
by (simp add: analytic_on_open closed_lattice open_Compl weierstrass_fun_holomorphic)
lemma weierstrass_fun_analytic' [analytic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ f z ∉ Λ"
shows "(λz. ℘ (f z)) analytic_on A"
proof -
have "℘ ∘ f analytic_on A"
by (rule analytic_on_compose_gen assms weierstrass_fun_analytic)+ (use assms in auto)
thus ?thesis by (simp add: o_def)
qed
lemma weierstrass_fun_continuous_on: "continuous_on (-Λ) weierstrass_fun"
using holomorphic_on_imp_continuous_on weierstrass_fun_holomorphic by blast
lemma weierstrass_fun_continuous_on' [continuous_intros]:
assumes "continuous_on A f" "⋀z. z ∈ A ⟹ f z ∉ Λ"
shows "continuous_on A (λz. ℘ (f z))"
by (rule continuous_on_compose2[OF weierstrass_fun_continuous_on assms(1)]) (use assms in auto)
lemma tendsto_weierstrass_fun [tendsto_intros]:
assumes "(f ⤏ c) F" "c ∉ Λ"
shows "((λz. ℘ (f z)) ⤏ ℘ c) F"
proof (rule continuous_on_tendsto_compose[OF _ assms(1)])
show "continuous_on (-Λ) ℘"
by (intro holomorphic_on_imp_continuous_on holomorphic_intros) auto
show "eventually (λz. f z ∈ -Λ) F"
by (rule eventually_compose_filterlim[OF _ assms(1)], rule eventually_nhds_in_open)
(use assms(2) in ‹auto intro: closed_lattice›)
qed (use assms(2) in auto)
lemma deriv_weierstrass_fun:
assumes "z ∉ Λ"
shows "deriv ℘ z = ℘' z"
by (rule DERIV_imp_deriv weierstrass_fun_has_field_derivative refl assms)+
text ‹
The following identity is to be read with care: for ‹ω = 0› we get a division by zero,
so the term ‹1 / ω⇧2› simply gets dropped.
›
lemma weierstrass_fun_eq:
assumes "z ∉ Λ"
shows "℘ z = (∑⇩∞ ω ∈ Λ. (1 / (z - ω) ^ 2) - 1 / ω ^ 2)"
proof -
have *: "((λω. 1 / (z - ω)⇧2 - 1 / ω⇧2) has_sum ℘ z - 1 / z^2) Λ⇧*"
using has_sum_infsum [OF weierstrass_summable, of z] assms
by (simp add: weierstrass_fun_def weierstrass_fun_aux_def lattice0_def)
have "((λω. 1 / (z - ω)⇧2 - 1 / ω⇧2) has_sum ((1 / (z - 0)^2 - 1 / 0⇧2) + (℘ z - 1 / z^2))) Λ"
unfolding lattice_lattice0 by (rule has_sum_insert) (use * in auto)
then show ?thesis
by (simp add: infsumI)
qed
subsection ‹Ellipticity and poles›
text ‹
It can easily be seen from its definition that ‹℘› is an even elliptic function with a
double pole at each lattice point and no other poles. Thus it has order 2.
Its derivative is consequently an odd elliptic function with a triple pole at each lattice point,
no other poles, and order 3.
The results in this section correspond to Apostol's Theorems 1.9 and 1.10.
›
lemma weierstrass_fun_minus: "℘ (-z) = ℘ z"
proof (cases "z ∈ Λ")
case False
have "(∑⇩∞ ω ∈ Λ⇧*. 1 / (- z - ω)⇧2 - 1 / ω⇧2) = (∑⇩∞ ω ∈ Λ⇧*. (1 / (z - ω)⇧2 - 1 / ω⇧2))"
by (rule infsum_reindex_bij_witness[of _ uminus uminus])
(auto intro!: lattice_intros simp: uminus_in_lattice0_iff power2_commute add_ac)
thus ?thesis using False
by (auto simp: weierstrass_fun_def weierstrass_fun_aux_def uminus_in_lattice0_iff lattice_lattice0)
qed (auto simp: weierstrass_fun_at_pole uminus_in_lattice_iff)
sublocale weierstrass_fun: complex_lattice_periodic ω1 ω2 ℘
proof
have *: "℘ (z + ω) = ℘ z" if ω: "ω ∈ {ω1, ω2}" for ω z
proof (cases "z ∈ Λ")
case z: True
thus ?thesis
by (subst (1 2) weierstrass_fun_at_pole) (use ω in ‹auto intro!: lattice_intros›)
next
case z: False
from ω have ω' [simp, intro]: "ω ∈ Λ"
by auto
define f where "f = (λz. ℘ (z + ω) - ℘ z)"
with ‹z ∉ Λ› have "(f has_field_derivative 0) (at z)" if "z ∉ Λ" for z
proof -
from that and ω have "(f has_field_derivative (℘' (z + ω) - ℘' z)) (at z)"
unfolding f_def by (auto intro!: derivative_eq_intros)
also have "℘' (z + ω) = ℘' z"
by (rule weierstrass_fun_deriv.lattice_cong) (auto simp: rel_def)
finally show ?thesis
by simp
qed
hence deriv: "∀x∈UNIV - Λ - {}. (f has_field_derivative 0) (at x)"
by blast
have cont: "continuous_on (UNIV - Λ) f"
by (auto simp: f_def intro!: continuous_intros)
have *: "connected (UNIV - Λ)" "open (UNIV - Λ)" "finite ({} :: complex set)"
by (auto simp: closed_lattice countable_lattice intro!: connected_open_diff_countable)
obtain c where c: "⋀z. z ∈ UNIV - Λ ⟹ f z = c"
using DERIV_zero_connected_constant[OF * cont deriv] by blast
have "ω / 2 ∉ Λ"
using of_ω12_coords_in_lattice_iff ω by (auto simp: in_lattice_conv_ω12_coords)
hence "f (-ω / 2) = c"
by (intro c) (auto simp: uminus_in_lattice_iff)
also have "f (-ω / 2) = 0"
by (simp add: f_def weierstrass_fun_minus)
finally have "f z = 0"
using c that z by auto
thus ?thesis
by (simp add: f_def)
qed
show "℘ (z + ω1) = ℘ z" "℘ (z + ω2) = ℘ z" for z
by (rule *; simp)+
qed
lemma zorder_weierstrass_fun_pole:
assumes "ω ∈ Λ"
shows "zorder ℘ ω = -2"
proof -
define R where "R = Inf_para"
have R: "R > 0"
using Inf_para_pos by (auto simp: R_def)
have R': "ball 0 R ∩ Λ⇧* = {}"
using Inf_para_le_norm by (force simp: R_def)
have "zorder weierstrass_fun ω = zorder (λz. weierstrass_fun (z + ω)) 0"
by (rule zorder_shift)
also have "(λz. weierstrass_fun (z + ω)) = weierstrass_fun"
by (intro ext weierstrass_fun.lattice_cong) (auto simp: rel_def assms)
also have "zorder weierstrass_fun 0 = -2"
proof (rule zorder_eqI)
show "open (ball 0 R :: complex set)" "(0 :: complex) ∈ ball 0 R"
using R by auto
show "(λz. 1 + weierstrass_fun_aux z * z ^ 2) holomorphic_on ball 0 R" using R'
by (intro holomorphic_intros holomorphic_on_subset[OF weierstrass_fun_aux_holomorphic]) auto
show "⋀w. ⟦w ∈ ball 0 R; w ≠ 0⟧
⟹ ℘ w =
(1 + weierstrass_fun_aux w * w⇧2) *
(w - 0) powi - 2"
using R'
by (auto simp: weierstrass_fun_def field_simps power_numeral_reduce powi_minus_numeral_reduce
lattice0_def)
qed auto
finally show ?thesis .
qed
lemma is_pole_weierstrass_fun:
assumes ω: "ω ∈ Λ"
shows "is_pole ℘ ω"
proof -
have "is_pole ℘ 0"
proof -
have "eventually (λz. z ∈ -Λ⇧*) (nhds 0)"
using closed_lattice0 by (intro eventually_nhds_in_open) auto
hence ev: "eventually (λz. z ∉ Λ) (at 0)"
unfolding eventually_at_filter by eventually_elim (auto simp: lattice0_def)
have "Λ - Λ⇧* = {0}" "Λ⇧* ⊆ Λ"
by (auto simp: insert_Diff_if lattice_lattice0)
hence "weierstrass_fun_aux holomorphic_on -Λ⇧*"
by (auto intro!: holomorphic_intros)
hence "continuous_on (-Λ⇧*) weierstrass_fun_aux"
using holomorphic_on_imp_continuous_on by blast
moreover have "0 ∈ -Λ⇧*"
by (auto simp: lattice0_def)
ultimately have "(weierstrass_fun_aux ⤏ weierstrass_fun_aux 0) (at 0)"
using closed_lattice0 by (metis at_within_open closed_open continuous_on_def)
moreover have "filterlim (λz::complex. 1 / z ^ 2) at_infinity (at 0)"
using is_pole_inverse_power[of 2 0] by (simp add: is_pole_def)
ultimately have "filterlim (λz. weierstrass_fun_aux z + 1 / z ^ 2) at_infinity (at 0)"
by (rule tendsto_add_filterlim_at_infinity)
also have "?this ⟷ filterlim weierstrass_fun at_infinity (at 0)"
by (intro filterlim_cong refl eventually_mono[OF ev]) (auto simp: weierstrass_fun_def)
finally show ?thesis
by (simp add: is_pole_def)
qed
also have "℘ = ℘ ∘ (λz. z + ω)"
by (auto simp: fun_eq_iff rel_def assms uminus_in_lattice_iff
intro!: weierstrass_fun.lattice_cong)
also have "is_pole … 0 ⟷ is_pole ℘ ω"
by (simp add: o_def is_pole_shift_0' add_ac)
finally show "is_pole ℘ ω" .
qed
sublocale weierstrass_fun: nicely_elliptic_function ω1 ω2 ℘
proof
show "℘ nicely_meromorphic_on UNIV"
proof (rule nicely_meromorphic_onI_open)
show "℘ analytic_on UNIV - Λ"
by (auto intro!: analytic_intros)
next
fix z assume "z ∈ Λ"
thus "is_pole ℘ z ∧ ℘ z = 0"
by (auto simp: weierstrass_fun_at_pole is_pole_weierstrass_fun)
next
show "isolated_singularity_at ℘ z" for z
proof (rule analytic_nhd_imp_isolated_singularity[of _ "-(Λ-{z})"])
show "open (- (Λ - {z}))"
by (intro open_Compl closed_subset_lattice) auto
qed (auto intro!: analytic_intros)
qed auto
qed
sublocale weierstrass_fun: even_elliptic_function ω1 ω2 ℘
by standard (auto simp: weierstrass_fun_minus)
lemmas [elliptic_function_intros] =
weierstrass_fun.elliptic_function_axioms
weierstrass_fun.nicely_elliptic_function_axioms
lemma is_pole_weierstrass_fun_iff: "is_pole ℘ z ⟷ z ∈ Λ"
by (meson ComplI analytic_on_analytic_at is_pole_weierstrass_fun
nicely_elliptic_function.analytic_at_iff_not_pole
weierstrass_fun.nicely_elliptic_function_axioms weierstrass_fun_analytic)
lemma is_pole_weierstrass_fun_deriv_iff: "is_pole ℘' z ⟷ z ∈ Λ"
proof -
have "eventually (λw. w ∉ Λ) (at z)"
using islimpt_iff_eventually not_islimpt_lattice by auto
hence "eventually (λw. ℘' w = deriv ℘ w) (at z)"
by eventually_elim (simp add: deriv_weierstrass_fun)
hence "is_pole ℘' z ⟷ is_pole (deriv ℘) z"
by (rule is_pole_cong) auto
also have "… ⟷ is_pole ℘ z"
by (rule is_pole_deriv_iff) (auto intro!: meromorphic_intros)
also have "… ⟷ z ∈ Λ"
by (rule is_pole_weierstrass_fun_iff)
finally show ?thesis .
qed
lemma zorder_weierstrass_fun_deriv_pole:
assumes "z ∈ Λ"
shows "zorder ℘' z = -3"
proof -
have "eventually (λw. w ∉ Λ) (at z)"
using islimpt_iff_eventually not_islimpt_lattice by auto
hence "eventually (λw. ℘' w = deriv ℘ w) (at z)"
by eventually_elim (simp add: deriv_weierstrass_fun)
hence "zorder ℘' z = zorder (deriv ℘) z"
by (rule zorder_cong) auto
also have "… = zorder ℘ z - 1"
by (subst zorder_deriv) (auto simp: is_pole_weierstrass_fun_iff assms)
also have "… = -3"
using assms by (simp add: zorder_weierstrass_fun_pole)
finally show ?thesis .
qed
lemma order_weierstrass_fun [simp]: "elliptic_order ℘ = 2"
proof -
have "elliptic_order ℘ = (∑z ∈ period_parallelogram 0 ∩ Λ. nat (-zorder ℘ z))"
unfolding elliptic_order_def by (rule sum.cong) (auto simp: is_pole_weierstrass_fun_iff)
also have "period_parallelogram 0 ∩ Λ = {0}"
by (auto elim!: latticeE simp: period_parallelogram_altdef zero_prod_def)
finally show ?thesis
by (simp add: zorder_weierstrass_fun_pole)
qed
lemma order_weierstrass_fun_deriv [simp]: "elliptic_order ℘' = 3"
proof -
have "elliptic_order ℘' = (∑z ∈ period_parallelogram 0 ∩ Λ. nat (-zorder ℘' z))"
unfolding elliptic_order_def by (rule sum.cong) (auto simp: is_pole_weierstrass_fun_deriv_iff)
also have "period_parallelogram 0 ∩ Λ = {0}"
by (auto elim!: latticeE simp: period_parallelogram_altdef zero_prod_def)
also have "(∑z∈{0}. nat (- zorder ℘' z)) = nat (-zorder ℘' 0)"
by simp
finally show ?thesis
by (simp add: zorder_weierstrass_fun_deriv_pole)
qed
sublocale weierstrass_fun: nonconst_nicely_elliptic_function ω1 ω2 ℘
by standard auto
sublocale weierstrass_fun_deriv: nonconst_nicely_elliptic_function ω1 ω2 "℘'"
by standard auto
subsection ‹The numbers $e_1, e_2, e_3$›
text ‹
The values of ‹℘› at the half-periods $\frac{1}{2}\omega_1$, $\frac{1}{2}\omega_2$, and
$\frac{1}{2}(\omega_1+\omega_2)$ are exactly the roots of the polynomial $4X^3 - g_2X - g_3$.
We call these values $e_1$, $e_2$, $e_3$.
›
definition number_e1:: "complex" ("𝖾⇩1") where
"𝖾⇩1 ≡ ℘ (ω1 / 2)"
definition number_e2:: "complex" ("𝖾⇩2") where
"𝖾⇩2 ≡ ℘ (ω2 / 2)"
definition number_e3:: "complex" ("𝖾⇩3") where
"𝖾⇩3 ≡ ℘ ((ω1 + ω2) / 2)"
lemmas number_e123_defs = number_e1_def number_e2_def number_e3_def
text ‹
The half-lattice points are those that are equivalent to one of the three points
$\frac{\omega_1}{2}$, $\frac{\omega_2}{2}$, and $\frac{\omega_1 + \omega_2}{2}$.
›
lemma to_fund_parallelogram_half_period:
assumes "ω ∉ Λ" "2 * ω ∈ Λ"
shows "to_fund_parallelogram ω ∈ {ω1 / 2, ω2 / 2, (ω1 + ω2) / 2}"
proof -
from assms(2) obtain m n where "2 * ω = of_ω12_coords (of_int m, of_int n)"
by (elim latticeE)
hence mn: "ω = of_ω12_coords (of_int m / 2, of_int n / 2)"
by (auto simp: of_ω12_coords_def field_simps)
have [simp]: "of_ω12_coords (1 / 2, 1 / 2) = (ω1 + ω2) / 2"
by (simp add: of_ω12_coords_def field_simps)
have "odd m ∨ odd n"
using assms(1) unfolding mn by (auto simp: in_lattice_conv_ω12_coords elim!: evenE)
thus ?thesis
by (cases "even m"; cases "even n")
(auto elim!: evenE oddE simp: mn to_fund_parallelogram_def add_divide_distrib)
qed
lemma rel_half_period:
assumes "ω ∉ Λ" "2 * ω ∈ Λ"
shows "∃ω'∈{ω1 / 2, ω2 / 2, (ω1 + ω2) / 2}. rel ω ω'"
proof -
have "rel ω (to_fund_parallelogram ω)"
by auto
with to_fund_parallelogram_half_period[OF assms] show ?thesis
by blast
qed
lemma weierstass_fun_deriv_half_period_eq_0:
assumes "ω ∈ Λ"
shows "℘' (ω / 2) = 0"
using weierstrass_fun_deriv.lattice_cong[of "-ω/2" "ω/2"] ‹ω ∈ Λ›
by (simp add: rel_def uminus_in_lattice_iff)
lemma weierstass_fun_deriv_half_root_eq_0 [simp]:
"℘' (ω1 / 2) = 0" "℘' (ω2 / 2) = 0" "℘' ((ω1 + ω2) / 2) = 0"
by (rule weierstass_fun_deriv_half_period_eq_0; simp)+
lemma weierstrass_fun_at_half_period:
assumes "ω ∈ Λ" "ω / 2 ∉ Λ"
shows "℘ (ω / 2) ∈ {𝖾⇩1, 𝖾⇩2, 𝖾⇩3}"
proof -
have "∃ω'∈{ω1 / 2, ω2 / 2, (ω1 + ω2) / 2}. rel (ω / 2) ω'"
using rel_half_period[of "ω / 2"] assms by auto
thus ?thesis
unfolding number_e123_defs using weierstrass_fun.lattice_cong by blast
qed
lemma weierstrass_fun_at_half_period':
assumes "2 * ω ∈ Λ" "ω ∉ Λ"
shows "℘ ω ∈ {𝖾⇩1, 𝖾⇩2, 𝖾⇩3}"
using weierstrass_fun_at_half_period[of "2 * ω"] assms by simp
text ‹
$\wp'$ has a simple zero at each half-lattice point, and no other zeros.
›
lemma weierstrass_fun_deriv_eq_0_iff:
assumes "z ∉ Λ"
shows "℘' z = 0 ⟷ 2 * z ∈ Λ"
proof
assume "℘' z = 0"
define z' where "z' = to_fund_parallelogram z"
have z': "℘' z' = 0" "z' ∉ Λ" "z' ∈ period_parallelogram 0"
using ‹℘' z = 0› assms by (auto simp: z'_def weierstrass_fun_deriv.eval_to_fund_parallelogram)
have [simp]: "℘' ≠ (λ_. 0)"
using weierstrass_fun_deriv.elliptic_order_eq_0_iff_no_poles by auto
have "{ω1 / 2, ω2 / 2, (ω1 + ω2) / 2, z'} ⊆ {z∈period_parallelogram 0. isolated_zero ℘' z}"
using z' by (auto simp: period_parallelogram_altdef ω12_coords.add
weierstrass_fun_deriv.isolated_zero_iff is_pole_weierstrass_fun_deriv_iff)
hence "card {ω1 / 2, ω2 / 2, (ω1 + ω2) / 2, z'} ≤ card {z∈period_parallelogram 0. isolated_zero ℘' z}"
by (intro card_mono weierstrass_fun_deriv.finite_zeros_in_parallelogram)
also have "… ≤ 3"
using weierstrass_fun_deriv.card_zeros_le_order[of 0] by simp
finally have "2 * z' ∈ {ω1, ω2, ω1 + ω2}"
by (auto simp: card_insert_if split: if_splits)
also have "… ⊆ Λ"
by auto
finally have "2 * z' ∈ Λ" .
thus "2 * z ∈ Λ" unfolding z'_def
by (metis rel_to_fund_parallelogram_right mult_2 rel_add rel_lattice_trans_right)
next
assume "2 * z ∈ Λ"
thus "℘' z = 0"
using assms weierstass_fun_deriv_half_period_eq_0[of "2*z"] by auto
qed
lemma zorder_weierstrass_fun_deriv_zero:
assumes "z ∉ Λ" "2 * z ∈ Λ"
shows "zorder ℘' z = 1"
proof -
have *: "℘' ≠ (λ_. 0)"
using is_pole_weierstrass_fun_deriv_iff[of 0] by auto
note ** [simp] = weierstrass_fun_deriv.isolated_zero_iff[OF *] is_pole_weierstrass_fun_deriv_iff
define w1 w2 w3 where "w1 = ω1 / 2" "w2 = ω2 / 2" "w3 = (ω1 + ω2) / 2"
note w123_defs = this
have [simp]: "w1 ∉ Λ" "w2 ∉ Λ" "w3 ∉ Λ" "2 * w1 ∈ Λ" "2 * w2 ∈ Λ" "2 * w3 ∈ Λ"
and "distinct [w1, w2, w3]"
by (auto simp: w123_defs add_divide_distrib in_lattice_conv_ω12_coords ω12_coords.add)
define A where "A = {w1, w2, w3}"
have [simp, intro]: "finite A" and [simp]: "card A = 3"
using ‹distinct [w1, w2, w3]› by (auto simp: A_def)
have in_parallelogram: "A ⊆ period_parallelogram 0"
unfolding A_def period_parallelogram_altdef by (auto simp: w123_defs ω12_coords.add)
have [simp]: "℘' w = 0" if "w ∈ A" for w
by (subst weierstrass_fun_deriv_eq_0_iff) (use that in ‹auto simp: A_def›)
have [intro]: "isolated_zero ℘' w" if "w ∈ A" for w
using that by (subst **) (auto simp: A_def)
have "(∑w∈A. nat (zorder ℘' w)) ≤ elliptic_order ℘'"
unfolding weierstrass_fun_deriv.zeros_eq_elliptic_order[of 0, symmetric] using in_parallelogram
by (intro sum_mono2 weierstrass_fun_deriv.finite_zeros_in_parallelogram)
(auto simp: A_def)
also have "… = 3"
by simp
finally have le_3: "(∑w∈A. nat (zorder ℘' w)) ≤ 3" .
have pos: "zorder ℘' w > 0" if "w ∈ A" for w
by (rule zorder_isolated_zero_pos) (use that in ‹auto intro!: analytic_intros simp: A_def›)
have zorder_eq_1: "zorder ℘' w = 1" if "w ∈ A" for w
proof (rule ccontr)
assume *: "zorder ℘' w ≠ 1"
have "(∑w∈A. nat (zorder ℘' w)) > (∑w∈A. 1)"
proof (rule sum_strict_mono_strong[of _ w])
show "nat (zorder ℘' w) ≥ 1" if "w ∈ A" for w
using pos[of w] that by auto
qed (use pos[of w] * ‹w ∈ A› in auto)
with le_3 show False
by simp
qed
from assms obtain w where w: "w ∈ A" "rel z w"
using rel_half_period[of z] unfolding A_def w123_defs by metis
with zorder_eq_1[of w] show ?thesis
using weierstrass_fun_deriv.zorder.lattice_cong by metis
qed
end
subsection ‹Injectivity of ‹℘››
context complex_lattice
begin
text ‹
The function ‹℘› is almost injective in the sense that $\wp(u) = \wp(v)$ iff
$u \sim v$ or $u \sim -v$. Another way to phrase this is that it is injective inside
period half-parallelograms.
This is Exercise~1.3(a) in Apostol's book.
›
theorem weierstrass_fun_eq_iff:
assumes "u ∉ Λ" "v ∉ Λ"
shows "℘ u = ℘ v ⟷ rel u v ∨ rel u (-v)"
proof (intro iffI)
assume "rel u v ∨ rel u (-v)"
thus "℘ u = ℘ v"
by (metis weierstrass_fun.lattice_cong weierstrass_fun_minus)
next
assume *: "℘ u = ℘ v"
define c where "c = ℘ u"
define f where "f = (λz. ℘ z - c)"
interpret f: elliptic_function_affine ω1 ω2 ℘ 1 "-c" f
proof -
show "elliptic_function_affine ω1 ω2 ℘ 1"
by standard auto
qed (simp_all add: f_def)
interpret f: even_elliptic_function ω1 ω2 f
by standard (simp_all add: f_def weierstrass_fun_minus)
interpret f: elliptic_function_remove_sings ω1 ω2 f ..
have ana: "f analytic_on {x}" if "x ∉ Λ" for x using that
unfolding f_def by (auto intro!: analytic_intros)
have ana': "remove_sings f analytic_on {x}" if "x ∉ Λ" for x using that
by (auto simp: f.remove_sings.analytic_at_iff_not_pole f.is_pole_affine_iff
is_pole_weierstrass_fun_iff)
have [simp]: "remove_sings f x = f x" if "x ∉ Λ" for x
using ana[OF that] by simp
have [simp]: "f u = 0" "f v = 0"
using * by (auto simp: f_def c_def)
have order: "elliptic_order f = 2"
by (simp add: f.order_affine_eq)
have nz: "remove_sings f ≠ (λ_. 0)"
proof
assume "remove_sings f = (λ_. 0)"
hence "remove_sings f constant_on UNIV"
by (auto simp: constant_on_def)
thus False
using f.remove_sings.elliptic_order_eq_0_iff order by simp
qed
have zero_f_iff [simp]: "isolated_zero f z ⟷ f z = 0" if "z ∉ Λ" for z
using that ana f.affine.isolated_zero_analytic_iff
f.affine.elliptic_order_eq_0_iff_const_cosparse local.order by auto
define u' where "u' = to_half_fund_parallelogram u"
define v' where "v' = to_half_fund_parallelogram v"
define Z where "Z = {z ∈ period_parallelogram 0. z ∉ Λ ∧ f z = 0}"
define Z1 where "Z1 = {z ∈ half_fund_parallelogram. z ∉ Λ ∧ f z = 0}"
define Z2 where "Z2 = to_fund_parallelogram ` uminus ` Z1"
have Z: "(∑z∈Z. nat (zorder f z)) = 2" "finite Z"
proof -
have "(∑z∈{z∈period_parallelogram 0. isolated_zero (remove_sings f) z}.
nat (zorder (remove_sings f) z)) = 2 ∧
finite {z∈period_parallelogram 0. isolated_zero (remove_sings f) z}"
using order f.remove_sings.zeros_eq_elliptic_order[of 0]
f.remove_sings.finite_zeros_in_parallelogram[of 0] by simp
also have "{z∈period_parallelogram 0. isolated_zero (remove_sings f) z} =
{z∈period_parallelogram 0. z ∉ Λ ∧ remove_sings f z = 0}"
by (subst f.remove_sings.isolated_zero_iff)
(use nz f.is_pole_affine_iff is_pole_weierstrass_fun_iff in auto)
also have "… = {z∈period_parallelogram 0. z ∉ Λ ∧ f z = 0}"
by (intro Collect_cong conj_cong) auto
finally show "(∑z∈Z. nat (zorder f z)) = 2" "finite Z"
unfolding Z_def by auto
qed
have "finite Z1"
by (rule finite_subset[OF _ Z(2)])
(use half_fund_parallelogram_subset_period_parallelogram in ‹auto simp: Z_def Z1_def›)
hence "finite Z2"
by (simp_all add: Z2_def)
note finite = ‹finite Z› ‹finite Z1› ‹finite Z2›
have subset: "Z1 ⊆ Z" "Z2 ⊆ Z"
unfolding Z_def Z1_def Z2_def
using half_fund_parallelogram_subset_period_parallelogram
by (auto simp: uminus_in_lattice_iff f.affine.eval_to_fund_parallelogram f.even)
have "card Z1 + card Z2 = card (Z1 ∪ Z2) + card (Z1 ∩ Z2)"
by (rule card_Un_Int) (use finite in auto)
also have "card Z2 = card Z1" unfolding Z2_def image_image
by (intro card_image inj_onI)
(auto simp: Z1_def rel_minus_iff intro: rel_in_half_fund_parallelogram_imp_eq)
also have "card (Z1 ∪ Z2) ≤ card Z"
by (intro card_mono finite) (use subset in auto)
also have "… = (∑z∈Z. 1)"
by simp
also have "card (Z1 ∩ Z2) = (∑z∈Z1 ∩ Z2. 1)"
by simp
also have "… = (∑z∈Z. if z ∈ Z1 ∩ Z2 then 1 else 0)"
by (intro sum.mono_neutral_cong_left) (use finite subset in auto)
also have "(∑z∈Z. 1) + … = (∑z∈Z. if z ∈ Z1 ∩ Z2 then 2 else 1)"
by (subst sum.distrib [symmetric], intro sum.cong) auto
also have "… ≤ (∑z∈Z. nat (zorder f z))"
proof (intro sum_mono)
fix z assume z: "z ∈ Z"
hence "zorder f z > 0"
by (intro zorder_isolated_zero_pos ana) (auto simp: Z_def)
moreover have "zorder f z ≥ 2" if z: "z ∈ Z1 ∩ Z2"
proof -
obtain z' where "to_fund_parallelogram (-z') ∈ half_fund_parallelogram" "z' ∉ Λ"
"z = to_fund_parallelogram (-z')" "z' ∈ half_fund_parallelogram"
using z by (auto simp: Z1_def Z2_def uminus_in_lattice_iff)
hence "2 * z ∈ Λ"
by (metis in_half_fund_parallelogram_imp_half_lattice
rel_in_half_fund_parallelogram_imp_eq rel_to_fund_parallelogram_left)
moreover have "¬(∀⇩≈z. f z = 0)" using nz
using f.affine.elliptic_order_eq_0_iff_const_cosparse local.order by auto
ultimately have "even (zorder f z)"
by (intro f.even_zorder)
with ‹zorder f z > 0› show "zorder f z ≥ 2"
by presburger
qed
ultimately show "(if z ∈ Z1 ∩ Z2 then 2 else 1) ≤ nat (zorder f z)"
by auto
qed
also have "… = 2"
by (fact Z(1))
finally have "card Z1 ≤ 1"
by simp
moreover have "card {u', v'} ≤ card Z1" using assms
by (intro card_mono finite) (auto simp: Z1_def u'_def v'_def f.eval_to_half_fund_parallelogram)
ultimately have "card {u', v'} ≤ 1"
by simp
hence "u' = v'"
by (cases "u' = v'") simp_all
thus "rel u v ∨ rel u (-v)"
unfolding u'_def v'_def by (simp add: to_half_fund_parallelogram_eq_iff)
qed
text ‹
It is also surjective. Together with the fact that it is doubly periodic and even, this means
that it takes on every value exactly once inside its period triangles, or twice within its
period parallelograms. Note however that the multiplicities of the poles on the lattice points
and of the values \<^term>‹𝖾⇩1›, \<^term>‹𝖾⇩2›, \<^term>‹𝖾⇩3› at the half-lattice points are 2.
›
lemma surj_weierstrass_fun:
obtains z where "z ∈ period_parallelogram w - Λ" "℘ z = c"
using weierstrass_fun.surj[of w c]
by (auto simp: is_pole_weierstrass_fun_iff)
lemma surj_weierstrass_fun_deriv:
obtains z where "z ∈ period_parallelogram w - Λ" "℘' z = c"
using weierstrass_fun_deriv.surj[of w c]
by (auto simp: is_pole_weierstrass_fun_deriv_iff)
end
context complex_lattice_swap
begin
lemma weierstrass_fun_aux_swap [simp]: "swap.weierstrass_fun_aux = weierstrass_fun_aux"
unfolding weierstrass_fun_aux_def [abs_def] swap.weierstrass_fun_aux_def [abs_def] by auto
lemma weierstrass_fun_swap [simp]: "swap.weierstrass_fun = weierstrass_fun"
unfolding weierstrass_fun_def [abs_def] swap.weierstrass_fun_def [abs_def] by auto
lemma number_e1_swap [simp]: "swap.number_e1 = number_e2"
and number_e2_swap [simp]: "swap.number_e2 = number_e1"
and number_e3_swap [simp]: "swap.number_e3 = number_e3"
unfolding number_e2_def swap.number_e1_def number_e1_def swap.number_e2_def
number_e3_def swap.number_e3_def by (simp_all add: add_ac)
end
subsection ‹Invariance under lattice transformations›
text ‹
We show how various concepts related to lattices (e.g.\ the Weierstra\ss\ $\wp$
function, the numbers $e_1$, $e_2$, $e_3$) transform under various transformations of the lattice.
Namely: complex conjugation, swapping the generators, stretching/rotation, and unimodular
M\"obius transforms.
›
locale complex_lattice_cnj = complex_lattice
begin
sublocale cnj: complex_lattice "cnj ω1" "cnj ω2"
by unfold_locales (use fundpair in auto)
lemma bij_betw_lattice_cnj: "bij_betw cnj lattice cnj.lattice"
by (rule bij_betwI[of _ _ _ cnj])
(auto elim!: latticeE cnj.latticeE simp: of_ω12_coords_def cnj.of_ω12_coords_def
intro!: lattice_intros cnj.lattice_intros)
lemma bij_betw_lattice0_cnj: "bij_betw cnj lattice0 cnj.lattice0"
unfolding lattice0_def cnj.lattice0_def
by (intro bij_betw_DiffI bij_betw_lattice_cnj) auto
lemma lattice_cnj_eq: "cnj.lattice = cnj ` lattice"
using bij_betw_lattice_cnj by (auto simp: bij_betw_def)
lemma lattice0_cnj_eq: "cnj.lattice0 = cnj ` lattice0"
using bij_betw_lattice0_cnj by (auto simp: bij_betw_def)
lemma eisenstein_fun_aux_cnj: "cnj.eisenstein_fun_aux n z = cnj (eisenstein_fun_aux n (cnj z))"
unfolding eisenstein_fun_aux_def cnj.eisenstein_fun_aux_def
by (subst infsum_reindex_bij_betw[OF bij_betw_lattice0_cnj, symmetric])
(auto simp flip: infsum_cnj simp: lattice0_cnj_eq in_image_cnj_iff)
lemma weierstrass_fun_aux_cnj: "cnj.weierstrass_fun_aux z = cnj (weierstrass_fun_aux (cnj z))"
unfolding weierstrass_fun_aux_def cnj.weierstrass_fun_aux_def
by (subst infsum_reindex_bij_betw[OF bij_betw_lattice0_cnj, symmetric])
(auto simp flip: infsum_cnj simp: lattice0_cnj_eq in_image_cnj_iff)
lemma weierstrass_fun_cnj: "cnj.weierstrass_fun z = cnj (weierstrass_fun (cnj z))"
unfolding weierstrass_fun_def cnj.weierstrass_fun_def
by (auto simp: lattice_cnj_eq in_image_cnj_iff weierstrass_fun_aux_cnj)
lemma number_e1_cnj [simp]: "cnj.number_e1 = cnj number_e1"
and number_e2_cnj [simp]: "cnj.number_e2 = cnj number_e2"
and number_e3_cnj [simp]: "cnj.number_e3 = cnj number_e3"
by (simp_all add: number_e1_def cnj.number_e1_def number_e2_def
cnj.number_e2_def number_e3_def cnj.number_e3_def weierstrass_fun_cnj)
end
locale complex_lattice_stretch = complex_lattice +
fixes c :: complex
assumes stretch_nonzero: "c ≠ 0"
begin
sublocale stretched: complex_lattice "c * ω1" "c * ω2"
by unfold_locales (use fundpair in ‹auto simp: stretch_nonzero fundpair_def›)
lemma stretched_of_ω12_coords: "stretched.of_ω12_coords ab = c * of_ω12_coords ab"
unfolding stretched.of_ω12_coords_def of_ω12_coords_def
by (auto simp: case_prod_unfold algebra_simps)
lemma stretched_ω12_coords: "stretched.ω12_coords ab = ω12_coords (ab / c)"
using stretch_nonzero stretched_of_ω12_coords
by (metis mult.commute nonzero_divide_eq_eq of_ω12_coords_ω12_coords stretched.ω12_coords_eqI)
lemma stretched_ω1_coord: "stretched.ω1_coord ab = ω1_coord (ab / c)"
and stretched_ω2_coord: "stretched.ω2_coord ab = ω2_coord (ab / c)"
using stretched_ω12_coords[of ab] by (simp_all add: stretched.ω12_coords_def ω12_coords_def)
lemma mult_into_stretched_lattice: "(*) c ∈ Λ → stretched.lattice"
by (auto elim!: latticeE simp: stretched.in_lattice_conv_ω12_coords
stretched_ω12_coords zero_prod_def)
lemma mult_into_stretched_lattice': "(*) (inverse c) ∈ stretched.lattice → Λ"
proof -
interpret inv: complex_lattice_stretch "c * ω1" "c * ω2" "inverse c"
by unfold_locales (use stretch_nonzero in auto)
from inv.mult_into_stretched_lattice show ?thesis
by (simp add: inv.stretched.lattice_def stretched.lattice_def field_simps stretch_nonzero)
qed
lemma bij_betw_stretch_lattice: "bij_betw ((*) c) lattice stretched.lattice"
proof (rule bij_betwI[of _ _ _ "(*) (inverse c)"])
show "(*) c ∈ Λ → stretched.lattice"
by (rule mult_into_stretched_lattice)
show "(*) (inverse c) ∈ stretched.lattice → Λ"
by (rule mult_into_stretched_lattice')
qed (auto simp: stretch_nonzero)
lemma bij_betw_stretch_lattice0:
"bij_betw ((*) c) lattice0 stretched.lattice0"
unfolding lattice0_def stretched.lattice0_def
by (intro bij_betw_DiffI bij_betw_stretch_lattice) auto
end
locale unimodular_moebius_transform_lattice = complex_lattice + unimodular_moebius_transform
begin
definition ω1' where "ω1' = of_int c * ω2 + of_int d * ω1"
definition ω2' where "ω2' = of_int a * ω2 + of_int b * ω1"
sublocale transformed: complex_lattice ω1' ω2'
proof unfold_locales
define τ where "τ = ω2 / ω1"
have "Im (φ τ) ≠ 0"
using fundpair Im_transform_zero_iff[of τ] unfolding τ_def
by (auto simp: fundpair_def complex_is_Real_iff)
also have "φ τ = ω2' / ω1'"
by (simp add: φ_def ω1'_def ω2'_def moebius_def τ_def divide_simps)
finally show "fundpair (ω1', ω2')"
by (simp add: φ_def ω1'_def ω2'_def moebius_def τ_def field_simps
fundpair_def complex_is_Real_iff)
qed
lemma transformed_lattice_subset: "transformed.lattice ⊆ lattice"
proof safe
fix z assume "z ∈ transformed.lattice"
then obtain m n where mn: "z = of_int m * ω1' + of_int n * ω2'"
by (elim transformed.latticeE) (auto simp: transformed.of_ω12_coords_def)
also have "of_int m * ω1' + of_int n * ω2' =
of_int (d * m + b * n) * ω1 + of_int (c * m + a * n) * ω2"
by (simp add: algebra_simps ω1'_def ω2'_def)
finally show "z ∈ lattice"
by (auto intro!: lattice_intros simp: ring_distribs mult.assoc)
qed
lemma transformed_lattice_eq: "transformed.lattice = lattice"
proof -
interpret inverse_unimodular_moebius_transform a b c d ..
interpret inv: unimodular_moebius_transform_lattice ω1' ω2' d "-b" "-c" a ..
have [simp]: "inv.ω1' = ω1" "inv.ω2' = ω2"
unfolding inv.ω1'_def inv.ω2'_def unfolding ω1'_def ω2'_def of_int_minus using unimodular
by (simp_all add: algebra_simps flip: of_int_mult)
have "inv.transformed.lattice ⊆ transformed.lattice"
by (rule inv.transformed_lattice_subset)
also have "inv.transformed.lattice = lattice"
unfolding inv.transformed.lattice_def unfolding lattice_def by simp
finally show ?thesis
using transformed_lattice_subset by blast
qed
lemma transformed_lattice0_eq: "transformed.lattice0 = lattice0"
by (simp add: transformed.lattice0_def lattice0_def transformed_lattice_eq)
lemma eisenstein_fun_aux_transformed [simp]: "transformed.eisenstein_fun_aux = eisenstein_fun_aux"
by (intro ext) (simp add: transformed.eisenstein_fun_aux_def eisenstein_fun_aux_def
transformed_lattice0_eq)
lemma weierstrass_fun_aux_transformed [simp]: "transformed.weierstrass_fun_aux = weierstrass_fun_aux"
by (intro ext, unfold weierstrass_fun_aux_def transformed.weierstrass_fun_aux_def
transformed_lattice0_eq) simp_all
lemma weierstrass_fun_transformed [simp]: "transformed.weierstrass_fun = weierstrass_fun"
by (intro ext, simp add: weierstrass_fun_def transformed.weierstrass_fun_def transformed_lattice_eq)
end
locale complex_lattice_apply_modgrp = complex_lattice +
fixes f :: modgrp
begin
sublocale unimodular_moebius_transform_lattice
ω1 ω2 "modgrp_a f" "modgrp_b f" "modgrp_c f" "modgrp_d f"
rewrites "modgrp.as_modgrp = (λx. x)" and "modgrp.φ = apply_modgrp"
by unfold_locales simp_all
end
subsection ‹Construction of arbitrary elliptic functions from ‹℘››
text ‹
In this section we will show that any elliptic function can be written as a combination of
‹℘› and ‹℘'›. The key step is to show that every even elliptic function can be written as a
rational function of ‹℘›.
The first step is to show that if $w \notin \Lambda$, the function $f(z) = \wp(z) - \wp(w)$
has a double zero at $w$ if $w$ is a half-lattice point and simple zeros at $\pm w$ otherwise,
and no other zeros.
›
locale weierstrass_fun_minus_const = complex_lattice +
fixes w :: complex and f :: "complex ⇒ complex"
assumes not_in_lattice: "w ∉ Λ"
defines "f ≡ (λz. ℘ z - ℘ w)"
begin
sublocale elliptic_function_affine ω1 ω2 ℘ 1 "-℘ w" f
unfolding f_def by unfold_locales (auto simp: f_def)
lemmas order_eq = order_affine_eq
lemmas is_pole_iff = is_pole_affine_iff
lemmas zorder_pole_eq = zorder_pole_affine
lemma isolated_zero_iff: "isolated_zero f z ⟷ rel z w ∨ rel z (-w)"
proof (cases "z ∈ Λ")
case False
hence "f analytic_on {z}"
unfolding f_def by (auto intro!: analytic_intros)
moreover have "¬(∀⇩≈z. f z = 0)"
using affine.elliptic_order_eq_0_iff_const_cosparse order_affine_eq by auto
ultimately have "isolated_zero f z ⟷ ℘ z = ℘ w"
by (subst affine.isolated_zero_analytic_iff) (auto simp: f_def)
also have "… ⟷ rel z w ∨ rel z (-w)"
by (rule weierstrass_fun_eq_iff) (use not_in_lattice False in auto)
finally show ?thesis .
next
case True
thus ?thesis
using not_in_lattice is_pole_iff is_pole_weierstrass_fun pole_is_not_zero
pre_complex_lattice.rel_lattice_trans_left uminus_in_lattice_iff by blast
qed
lemma zorder_zero_eq:
assumes "rel z w ∨ rel z (-w)"
shows "zorder f z = (if 2 * w ∈ Λ then 2 else 1)"
proof (cases "2 * w ∈ Λ")
case False
have z: "z ∉ Λ"
using assms not_in_lattice pre_complex_lattice.rel_lattice_trans_left
uminus_in_lattice_iff by blast
have z': "2 * z ∉ Λ"
using assms False z
by (metis minus_zero minus_minus not_in_lattice weierstrass_fun_deriv.lattice_cong
weierstrass_fun_deriv_eq_0_iff weierstrass_fun_deriv_minus z)
have "zorder f z = 1"
proof (rule zorder_zero_eqI')
show "f analytic_on {z}"
using not_in_lattice z by (auto simp: f_def intro!: analytic_intros)
next
show "(deriv ^^ i) f z = 0" if "i < nat 1" for i
using that z not_in_lattice assms by (auto simp: f_def weierstrass_fun_eq_iff)
next
have "deriv f z = ℘' z" unfolding f_def
by (rule DERIV_imp_deriv) (use z in ‹auto intro!: derivative_eq_intros›)
also have "℘' z ≠ 0"
using not_in_lattice False z assms z' by (auto simp: weierstrass_fun_deriv_eq_0_iff)
finally show "(deriv ^^ nat 1) f z ≠ 0"
by simp
qed auto
with False show ?thesis
by simp
next
case True
have z: "z ∉ Λ"
using assms not_in_lattice pre_complex_lattice.rel_lattice_trans_left
uminus_in_lattice_iff by blast
have z': "2 * z ∈ Λ"
using assms True z
by (metis minus_zero minus_minus not_in_lattice weierstrass_fun_deriv.lattice_cong
weierstrass_fun_deriv_eq_0_iff weierstrass_fun_deriv_minus z)
have "eventually (λw. f w ≠ 0) (at 0)"
by (simp add: affine.avoid' order_affine_eq)
moreover have "eventually (λw. w ∉ Λ) (at 0)"
using islimpt_iff_eventually not_islimpt_lattice by auto
ultimately have ev: "eventually (λw. f w ≠ 0 ∧ w ∉ Λ) (at 0)"
by eventually_elim auto
obtain z0 where z0: "z0 ∉ Λ" "f z0 ≠ 0"
using eventually_happens[OF ev] by auto
have "(∑z∈{z}. nat (zorder f z)) ≤
(∑z' | z' ∈ period_parallelogram z ∧ isolated_zero f z'. nat (zorder f z'))"
using assms by (intro sum_mono2 affine.finite_zeros_in_parallelogram) (auto simp: isolated_zero_iff)
also have "… = 2"
using affine.zeros_eq_elliptic_order[of z] order_eq by simp
finally have "zorder f z ≤ 2"
by simp
moreover have "zorder f z ≥ int 2"
proof (rule zorder_geI)
show "f holomorphic_on -Λ"
by (auto intro!: holomorphic_intros simp: f_def)
next
show "z0 ∈ -Λ" "f z0 ≠ 0"
using z0 by auto
next
show "open (-Λ)"
using closed_lattice by auto
next
have "Λ sparse_in UNIV"
using not_islimpt_lattice sparse_in_def by blast
hence "connected (UNIV - Λ)"
by (intro sparse_imp_connected) auto
also have "UNIV - Λ = -Λ"
by auto
finally show "connected (-Λ)" .
next
have "deriv f z = ℘' z"
by (rule DERIV_imp_deriv) (auto simp: f_def intro!: derivative_eq_intros z)
also have "… = 0"
using True z z' weierstrass_fun_deriv_eq_0_iff by blast
finally have "deriv f z = 0" .
moreover have "f z = 0"
using not_in_lattice z z' assms by (simp add: f_def weierstrass_fun_eq_iff)
ultimately show "(deriv ^^ n) f z = 0" if "n < 2" for n
using that by (cases n) auto
qed (use z in ‹auto intro!: analytic_intros simp: f_def›)
ultimately have "zorder f z = 2"
by linarith
thus ?thesis
using True by simp
qed
lemma zorder_zero_eq':
assumes "z ∉ Λ"
shows "zorder f z = (if rel z w ∨ rel z (-w) then if 2 * w ∈ Λ then 2 else 1 else 0)"
proof (cases "rel z w ∨ rel z (-w)")
case True
thus ?thesis
using zorder_zero_eq[OF True] by auto
next
case False
have "f analytic_on {z}"
using assms by (auto simp: f_def intro!: analytic_intros)
moreover have "f z ≠ 0"
using assms not_in_lattice False by (auto simp: f_def weierstrass_fun_eq_iff)
ultimately have "zorder f z = 0"
by (intro zorder_eq_0I) auto
thus ?thesis
using False by simp
qed
end
lemma (in complex_lattice) zorder_weierstrass_fun_minus_const:
assumes "w ∉ Λ" "z ∉ Λ"
shows "zorder (λz. ℘ z - ℘ w) z =
(if rel z w ∨ rel z (-w) then if 2 * w ∈ Λ then 2 else 1 else 0)"
proof -
interpret weierstrass_fun_minus_const ω1 ω2 w "λz. ℘ z - ℘ w"
by unfold_locales (use assms in auto)
show ?thesis
using zorder_zero_eq'[of z] assms by simp
qed
text ‹
We now construct an elliptic function
\[g(z) = \prod_{w\in A} (\wp(z) - \wp(w))^{h(w)}\]
where $A \subseteq \mathbb{C}\setminus\Lambda$ is finite and $h : A \to \mathbb{Z}$.
We will examine what the zeros and poles of this functions are and what their multiplicities are.
This is roughly Exercise~1.3(b) in Apostol's book.
›
locale elliptic_function_construct = complex_lattice +
fixes A :: "complex set" and h :: "complex ⇒ int" and g :: "complex ⇒ complex"
assumes finite [intro]: "finite A" and no_lattice_points: "A ∩ Λ = {}"
defines "g ≡ (λz. (∏w∈A. (℘ z - ℘ w) powi h w))"
begin
sublocale elliptic_function ω1 ω2 g
unfolding g_def by (intro elliptic_function_intros)
sublocale even_elliptic_function ω1 ω2 g
by standard (simp add: g_def weierstrass_fun_minus)
lemma no_lattice_points': "w ∉ Λ" if "w ∈ A" for w
using no_lattice_points that by blast
lemma eq_0_iff: "g z = 0 ⟷ (∃w∈A. h w ≠ 0 ∧ (rel z w ∨ rel z (-w)))" if "z ∉ Λ" for z
using finite that by (auto simp: g_def weierstrass_fun_eq_iff no_lattice_points')
lemma nonzero_almost_everywhere: "eventually (λz. g z ≠ 0) (cosparse UNIV)"
proof -
have "{z. g z = 0} ⊆ Λ ∪ (⋃w∈A. (+) w ` Λ) ∪ (⋃w∈A. (+) (-w) ` Λ)"
using eq_0_iff by (force simp: rel_def)
moreover have "… sparse_in UNIV"
by (intro sparse_in_union' sparse_in_UN_finite finite_imageI
finite sparse_in_translate_UNIV lattice_sparse)
ultimately have "{z. g z = 0} sparse_in UNIV"
using sparse_in_subset2 by blast
thus ?thesis
by (simp add: eventually_cosparse)
qed
lemma eventually_nonzero_at: "eventually (λz. g z ≠ 0) (at z)"
using nonzero_almost_everywhere by (auto simp: eventually_cosparse_open_eq)
lemma zorder_eq:
assumes z: "z ∉ Λ"
shows "zorder g z =
(∑w∈A. if rel z w ∨ rel z (-w) then if 2*w ∈ Λ then 2 * h w else h w else 0)"
proof -
have [simp]: "w ∉ Λ" if "w ∈ A" for w
using no_lattice_points that by blast
have "zorder g z = (∑x∈A. zorder (λz. (℘ z - ℘ x) powi h x) z)"
unfolding g_def
proof (rule zorder_prod)
show "∀⇩F z in at z. (∏x∈A. (℘ z - ℘ x) powi h x) ≠ 0"
using eventually_nonzero_at[of z] by (simp add: g_def)
qed (auto intro!: meromorphic_intros)
also have "… = (∑w∈A. if rel z w ∨ rel z (-w) then if 2*w ∈ Λ then 2 * h w else h w else 0)"
proof (intro sum.cong refl)
fix w assume "w ∈ A"
have "zorder (λz. (℘ z - ℘ w) powi h w) z = h w * zorder (λz. (℘ z - ℘ w)) z"
proof (cases "h w = 0")
case [simp]: False
have "∀⇩F z in at z. ℘ z - ℘ w ≠ 0"
using eventually_nonzero_at[of z]
by eventually_elim (use ‹w ∈ A› finite in ‹auto simp: g_def›)
hence "∃⇩F z in at z. ℘ z - ℘ w ≠ 0"
using eventually_frequently at_neq_bot by blast
thus ?thesis
by (intro zorder_power_int) (auto intro!: meromorphic_intros)
qed auto
also have "zorder (λz. ℘ z - ℘ w) z =
(if rel z w ∨ rel z (-w) then if 2*w ∈ Λ then 2 else 1 else 0)"
using zorder_weierstrass_fun_minus_const[of w z] z ‹w ∈ A› by simp
also have "h w * … = (if rel z w ∨ rel z (-w) then if 2*w ∈ Λ then 2 * h w else h w else 0)"
by auto
finally show "zorder (λz. (℘ z - ℘ w) powi h w) z =
(if rel z w ∨ rel z (-w) then if 2*w ∈ Λ then 2 * h w else h w else 0)" .
qed
finally show "zorder g z = (∑w∈A. if rel z w ∨ rel z (-w) then if 2*w ∈ Λ then 2 * h w else h w else 0)" .
qed
end
lemma (in even_elliptic_function) in_terms_of_weierstrass_fun_even_aux:
assumes nontrivial: "¬eventually (λz. f z = 0) (cosparse UNIV)"
defines "Z ≡ {z∈half_fund_parallelogram - {0}. is_pole f z ∨ isolated_zero f z}"
defines "h ≡ (λz. if z ∈ Z then zorder f z div (if 2 * z ∈ Λ then 2 else 1) else 0)"
obtains c where "eventually (λz. f z = c * (∏w∈Z. (℘ z - ℘ w) powi h w)) (cosparse UNIV)"
proof -
define g where "g = (λz. (∏w∈Z. (℘ z - ℘ w) powi h w))"
have [intro]: "finite Z"
proof (rule finite_subset)
show "Z ⊆ {z∈period_parallelogram 0. is_pole f z} ∪ {z∈period_parallelogram 0. isolated_zero f z}"
using half_fund_parallelogram_subset_period_parallelogram by (auto simp: Z_def)
show "finite ({z∈period_parallelogram 0. is_pole f z} ∪ {z∈period_parallelogram 0. isolated_zero f z})"
by (intro finite_UnI finite_poles_in_parallelogram finite_zeros_in_parallelogram)
qed
have [simp]: "z ∉ Λ" if "z ∈ Z" for z
using that half_fund_parallelogram_in_lattice_iff[of z] unfolding Z_def by auto
interpret g: elliptic_function_construct ω1 ω2 Z h g
by unfold_locales (auto simp: g_def)
have zorder_eq_aux: "zorder g z = zorder f z" if z: "z ∈ half_fund_parallelogram - Λ" for z
proof -
have "zorder g z = (∑w∈Z. if rel z w ∨ rel z (-w) then if 2*w ∈ Λ then 2 * h w else h w else 0)"
by (rule g.zorder_eq) (use z in auto)
also have "… = (∑w∈Z∩{z}. if 2*w ∈ Λ then 2 * h w else h w)"
proof (intro sum.mono_neutral_cong_right ballI)
fix w assume w: "w ∈ Z - Z ∩ {z}"
thus "(if rel z w ∨ rel z (-w) then if 2 * w ∈ Λ then 2 * h w else h w else 0) = 0"
using rel_in_half_fund_parallelogram_imp_eq[of z w] z by (auto simp: Z_def)
qed auto
also have "… = (if 2 * z ∈ Λ then 2 * h z else h z)"
by (auto simp: h_def)
also have "… = (if z ∈ Z then zorder f z else 0)"
using even_zorder[of z] nontrivial by (auto simp: h_def)
also have "… = zorder f z"
proof (cases "z ∈ Z")
case False
hence "¬is_pole f z ∧ ¬isolated_zero f z"
using z by (auto simp: Z_def)
moreover have "frequently (λz. f z ≠ 0) (at z)"
using nontrivial by (metis eventually_eq_imp_almost_everywhere_eq not_eventually)
ultimately have "zorder f z = 0"
by (intro not_pole_not_isolated_zero_imp_zorder_eq_0) (auto intro: meromorphic')
thus ?thesis
by simp
qed auto
finally show ?thesis .
qed
have zorder_eq: "zorder g z = zorder f z" if z: "z ∉ Λ" for z
proof -
have "zorder g z = zorder g (to_half_fund_parallelogram z)"
using g.zorder_to_half_fund_parallelogram by simp
also have "… = zorder f (to_half_fund_parallelogram z)"
by (rule zorder_eq_aux) (use z in auto)
also have "… = zorder f z"
using zorder_to_half_fund_parallelogram by simp
finally show ?thesis .
qed
define h where "h = (λz. f z / g z)"
interpret h: elliptic_function ω1 ω2 h
unfolding h_def by (intro elliptic_function_intros)
have h_nonzero: "eventually (λz. h z ≠ 0) (at z)" for z
proof -
have "eventually (λz. f z ≠ 0) (at z)"
using nontrivial frequently_def frequently_eq_imp_almost_everywhere_eq by blast
thus ?thesis
using g.eventually_nonzero_at by eventually_elim (auto simp: h_def)
qed
have zorder_h: "zorder h z = 0" if z: "z ∉ Λ" for z
unfolding h_def
proof (subst zorder_divide)
show "∃⇩F z in at z. f z ≠ 0"
using nontrivial by (metis eventually_eq_imp_almost_everywhere_eq not_eventually)
show "∃⇩F z in at z. g z ≠ 0"
using eventually_frequently g.eventually_nonzero_at trivial_limit_at by blast
qed (use z zorder_eq[of z] in ‹auto intro!: meromorphic' g.meromorphic'›)
have zorder_h': "zorder h z = 0" if z: "z ∈ period_parallelogram 0" "z ≠ 0" for z
by (rule zorder_h) (use z fund_period_parallelogram_in_lattice_iff[of z] in auto)
have "elliptic_order h = 0"
proof -
have "elliptic_order h = (∑z∈(if is_pole h 0 then {0} else {}). nat (-zorder h z))"
unfolding elliptic_order_def
by (intro sum.mono_neutral_right h.finite_poles_in_parallelogram)
(auto dest: zorder_h')
also have "… = nat (-zorder h 0)"
using zorder_neg_imp_is_pole[OF h.meromorphic', of 0] h_nonzero
linorder_not_less[of "zorder h 0" 0] by auto
finally have *: "elliptic_order h = nat (-zorder h 0)" .
have "elliptic_order h = (∑z∈(if isolated_zero h 0 then {0} else {}). nat (zorder h z))"
unfolding h.zeros_eq_elliptic_order[of 0, symmetric]
by (intro sum.mono_neutral_right h.finite_zeros_in_parallelogram)
(auto dest: zorder_h')
also have "… = nat (zorder h 0)"
using zorder_pos_imp_isolated_zero[OF h.meromorphic', of 0] h_nonzero
linorder_not_less[of 0 "zorder h 0"] by auto
finally have "elliptic_order h = nat (zorder h 0)" .
with * show "elliptic_order h = 0"
by simp
qed
then obtain c where c: "eventually (λz. h z = c) (cosparse UNIV)"
using h.elliptic_order_eq_0_iff_const_cosparse by blast
moreover have "eventually (λz. g z ≠ 0) (cosparse UNIV)"
using g.nonzero_almost_everywhere by blast
ultimately have "eventually (λz. f z = c * g z) (cosparse UNIV)"
by eventually_elim (auto simp: h_def)
thus ?thesis
using that[of c] unfolding g_def by blast
qed
text ‹
Finally, we show that any even elliptic function can be written as a rational function of $\wp$.
This is Exercise~1.4 in Apostol's book.
›
lemma (in even_elliptic_function) in_terms_of_weierstrass_fun_even:
obtains p q :: "complex poly" where "q ≠ 0" "∀⇩≈z. f z = poly p (℘ z) / poly q (℘ z)"
proof (cases "eventually (λz. f z = 0) (cosparse UNIV)")
case True
thus ?thesis
using that[of 1 0] by simp
next
case False
define Z where "Z = {z∈half_fund_parallelogram - {0}. is_pole f z ∨ isolated_zero f z}"
define h where "h = (λz. if z ∈ Z then zorder f z div (if 2 * z ∈ Λ then 2 else 1) else 0)"
obtain c where *: "eventually (λz. f z = c * (∏w∈Z. (℘ z - ℘ w) powi h w)) (cosparse UNIV)"
using False in_terms_of_weierstrass_fun_even_aux unfolding Z_def h_def by metis
define p where "p = Polynomial.smult c (∏w∈{w∈Z. h w ≥ 0}. [:-℘ w, 1:] ^ nat (h w))"
define q where "q = (∏w∈{w∈Z. h w < 0}. [:-℘ w, 1:] ^ nat (-h w))"
have finite: "finite Z"
proof (rule finite_subset)
show "Z ⊆ {z∈period_parallelogram 0. is_pole f z} ∪ {z∈period_parallelogram 0. isolated_zero f z}"
using half_fund_parallelogram_subset_period_parallelogram by (auto simp: Z_def)
show "finite ({z∈period_parallelogram 0. is_pole f z} ∪ {z∈period_parallelogram 0. isolated_zero f z})"
by (intro finite_UnI finite_poles_in_parallelogram finite_zeros_in_parallelogram)
qed
show ?thesis
proof (rule that[of q p])
show "q ≠ 0"
using finite by (auto simp: q_def)
next
show "∀⇩≈z. f z = poly p (℘ z) / poly q (℘ z)"
using *
proof eventually_elim
case (elim z)
have "f z = c * (∏w∈Z. (℘ z - ℘ w) powi h w)"
by (fact elim)
also have "Z = {w∈Z. h w ≥ 0} ∪ {w∈Z. h w < 0}"
by auto
also have "c * (∏w∈…. (℘ z - ℘ w) powi h w) =
c * (∏w∈{w∈Z. h w ≥ 0}. (℘ z - ℘ w) powi h w) *
(∏w∈{w∈Z. h w < 0}. (℘ z - ℘ w) powi h w)"
by (subst prod.union_disjoint) (use finite in auto)
also have "(∏w∈{w∈Z. h w ≥ 0}. (℘ z - ℘ w) powi h w) =
(∏w∈{w∈Z. h w ≥ 0}. poly [:-℘ w, 1:] (℘ z) ^ (nat (h w)))"
by (intro prod.cong) (auto simp: power_int_def)
also have "c * … = poly p (℘ z)"
by (simp add: p_def poly_prod)
also have "(∏w∈{w∈Z. h w < 0}. (℘ z - ℘ w) powi h w) =
(∏w∈{w∈Z. h w < 0}. inverse (poly [:-℘ w, 1:] (℘ z) ^ (nat (-h w))))"
by (intro prod.cong) (auto simp: power_int_def field_simps)
also have "… = inverse (poly q (℘ z))"
unfolding q_def poly_prod by (subst prod_inversef [symmetric]) auto
finally show ?case
by (simp add: field_simps)
qed
qed
qed
text ‹
From this, we now show that any elliptic function $f$ can be written in the form
$f(z) = g(\wp(z)) + \wp'(z) h(\wp(z))$ where $g, h$ are rational functions.
The proof is fairly simple: We can split $f(z)$ into a sum $f(z) = f_1(z) + f_2(z)$ where
$f_1$ is even and $f_2$ is odd by defining $f_1(z) = \frac{1}{2} (f(z) + f(-z))$ and
$f_2(z) = \frac{1}{2} (f(z) - f(-z))$. We can then further define $f_3(z) = f_2(z) / \wp'(z)$ so
that $f_3$ is also even.
By our previous result, we know that $f_1$ and $f_3$ can be written as rational functions of
$\wp$, so by combining everything we get the result we want.
This result is Exercise~1.5 in Apostol's book.
›
theorem (in even_elliptic_function) in_terms_of_weierstrass_fun:
obtains p q r s :: "complex poly" where "q ≠ 0" "s ≠ 0"
"∀⇩≈z. f z = poly p (℘ z) / poly q (℘ z) + ℘' z * poly r (℘ z) / poly s (℘ z)"
proof -
define f1 where "f1 = (λz. (f z + f (-z)) / 2)"
define f2 where "f2 = (λz. (f z - f (-z)) / 2)"
define f2' where "f2' = (λz. f2 z / ℘' z)"
note [elliptic_function_intros] = elliptic_function_compose_uminus[OF elliptic_function_axioms]
interpret f1: elliptic_function ω1 ω2 f1
unfolding f1_def by (intro elliptic_function_intros)
interpret f1: even_elliptic_function ω1 ω2 f1
by standard (auto simp: f1_def)
obtain p q where pq: "q ≠ 0" "∀⇩≈z. f1 z = poly p (℘ z) / poly q (℘ z)"
using f1.in_terms_of_weierstrass_fun_even .
interpret f2': elliptic_function ω1 ω2 f2'
unfolding f2'_def f2_def by (intro elliptic_function_intros)
interpret f2': even_elliptic_function ω1 ω2 f2'
by standard (auto simp: f2'_def f2_def divide_simps)
obtain r s where rs: "s ≠ 0" "∀⇩≈z. f2' z = poly r (℘ z) / poly s (℘ z)"
using f2'.in_terms_of_weierstrass_fun_even .
have "eventually (λz. ℘' z ≠ 0) (cosparse UNIV)"
by (simp add: weierstrass_fun_deriv.avoid)
with pq(2) and rs(2) have "∀⇩≈z. f z = poly p (℘ z) / poly q (℘ z) + ℘' z * poly r (℘ z) / poly s (℘ z)"
proof eventually_elim
case (elim z)
have "poly p (℘ z) / poly q (℘ z) + ℘' z * poly r (℘ z) / poly s (℘ z) =
f1 z + ℘' z * (poly r (℘ z) / poly s (℘ z))"
unfolding elim(1) by (simp add: divide_simps)
also have "poly r (℘ z) / poly s (℘ z) = f2' z"
using elim(2) by simp
also have "℘' z * f2' z = f2 z"
using elim(3) by (simp add: f2'_def)
also have "f1 z + f2 z = f z"
by (simp add: f1_def f2_def field_simps)
finally show ?case ..
qed
thus ?thesis
using that[of q s p r] pq(1) rs(1) by simp
qed
end