The Weierstrass ζ function

For a pair of periods L with lattice Λ, the Weierstrass ζ function is ζ(z) = 1 / z + ∑_{l ∈ Λ, l ≠ 0} (1 / (z - l) + 1 / l + z / l²) (PeriodPair.weierstrassZeta), the series converging absolutely and locally uniformly in z, since its terms are z² / (l² (z - l)) = O(|l|⁻³). It is holomorphic away from Λ with ζ' = -℘, and it is odd.

Unlike ℘, the function ζ is not periodic: it is quasi-periodic. Since ζ(z + l) - ζ(z) has derivative ℘(z) - ℘(z + l) = 0 on the connected open set ℂ ∖ Λ, it is a constant η(l), the quasi-period of l (PeriodPair.quasiPeriod), and η : Λ → ℂ is additive. At a lattice point l, a pole of ζ, the defining series takes the value η(l), so the quasi-periodicity holds at every z, and, as ζ is odd, η(l) = 2 ζ(l / 2) for every l ∈ Λ.

The values of ζ at the N-division points of ℤ z + ℤ, corrected by the quasi-periods so as to depend only on the division point modulo the lattice, are the building blocks of the weight-one Eisenstein series of level Γ(N), as the values of ℘ are in weight two.

Main definitions

• PeriodPair.weierstrassZeta: the Weierstrass ζ function of L.
• PeriodPair.quasiPeriod: the quasi-periods η : Λ →+ ℂ of ζ.

Main results

• PeriodPair.weierstrassZeta_bound: the terms of the series are O(|l|⁻³) on balls.
• PeriodPair.hasSumLocallyUniformly_weierstrassZeta, PeriodPair.hasSum_weierstrassZeta: the series converges locally uniformly to ζ.
• PeriodPair.hasDerivAt_weierstrassZeta: ζ' = -℘ away from Λ.
• PeriodPair.differentiableOn_weierstrassZeta: ζ is holomorphic away from Λ.
• PeriodPair.weierstrassZeta_neg: ζ is odd.
• PeriodPair.weierstrassZeta_coe: the junk value ζ(l) = η(l) at a lattice point.
• PeriodPair.weierstrassZeta_add_coe: the quasi-periodicity ζ(z + l) = ζ(z) + η(l).
• PeriodPair.quasiPeriod_eq_intCast_mul_add: η(m ω₁ + n ω₂) = m η(ω₁) + n η(ω₂).
• PeriodPair.quasiPeriod_eq_two_mul_weierstrassZeta: η(l) = 2 ζ(l / 2).

References

• M. Abramowitz and I. A. Stegun, Handbook of mathematical functions, Chapter 18.
• NIST Digital Library of Mathematical Functions, §23.2.
• The convergence and differentiability arguments follow those for Mathlib's PeriodPair.weierstrassP (Andrew Yang).

noncomputable def PeriodPair.weierstrassZeta (L : PeriodPair) (z : ℂ) : ℂ

The Weierstrass ζ function of the lattice Λ of L, ζ(z) = 1 / z + ∑_{l ∈ Λ, l ≠ 0} (1 / (z - l) + 1 / l + z / l²). With the convention 1 / 0 = 0, the term l = 0 of the series below is 1 / z. At the points of Λ the value is junk.

theorem PeriodPair.weierstrassZeta_bound {r : ℝ} {s : ℂ} (hs : ‖s‖ < r) {l : ℂ} (h : 2 * r ≤ ‖l‖) : ‖1 / (s - l) + 1 / l + s / l ^ 2‖ ≤ 2 * r ^ 2 * ‖l‖ ^ (-3)

The terms 1 / (s - l) + 1 / l + s / l² = s² / (l² (s - l)) of the series of ζ are O(|l|⁻³), uniformly for s in a ball.

theorem PeriodPair.hasSumLocallyUniformly_weierstrassZeta (L : PeriodPair) : HasSumLocallyUniformly (fun (l : ↥L.lattice) (z : ℂ) => 1 / (z - ↑l) + 1 / ↑l + z / ↑l ^ 2) L.weierstrassZeta

The series of ζ converges locally uniformly on ℂ.

theorem PeriodPair.hasSum_weierstrassZeta (L : PeriodPair) (z : ℂ) : HasSum (fun (l : ↥L.lattice) => 1 / (z - ↑l) + 1 / ↑l + z / ↑l ^ 2) (L.weierstrassZeta z)

The series of ζ converges to ζ.

theorem PeriodPair.hasDerivAt_weierstrassZeta (L : PeriodPair) {z : ℂ} (hz : z ∉ L.lattice) : HasDerivAt L.weierstrassZeta (-L.weierstrassP z) z

ζ' = -℘ away from the lattice.

theorem PeriodPair.differentiableOn_weierstrassZeta (L : PeriodPair) : DifferentiableOn ℂ L.weierstrassZeta (↑L.lattice)ᶜ

ζ is holomorphic away from the lattice.

@[simp]

theorem PeriodPair.weierstrassZeta_neg (L : PeriodPair) (z : ℂ) : L.weierstrassZeta (-z) = -L.weierstrassZeta z

ζ is odd.

@[simp]

theorem PeriodPair.weierstrassZeta_zero (L : PeriodPair) : L.weierstrassZeta 0 = 0

ζ(0) = 0, as ζ is odd.

noncomputable def PeriodPair.quasiPeriod (L : PeriodPair) : ↥L.lattice →+ ℂ

The quasi-periods of the Weierstrass ζ function: η(l) is the constant value of ζ(z + l) - ζ(z) (PeriodPair.weierstrassZeta_add_coe). It is additive in l.

@[simp]

theorem PeriodPair.weierstrassZeta_coe (L : PeriodPair) (l : ↥L.lattice) : L.weierstrassZeta ↑l = L.quasiPeriod l

The value of ζ at a lattice point is the quasi-period: ζ(l) = η(l). The lattice points are the poles of ζ, so this is a junk value (compare PeriodPair.weierstrassP_coe); it is the constant term of the Laurent expansion of ζ at l.

@[simp]

theorem PeriodPair.weierstrassZeta_add_coe (L : PeriodPair) (z : ℂ) (l : ↥L.lattice) : L.weierstrassZeta (z + ↑l) = L.weierstrassZeta z + L.quasiPeriod l

The quasi-periodicity of ζ: ζ(z + l) = ζ(z) + η(l) for every z and l ∈ Λ.

@[simp]

theorem PeriodPair.weierstrassZeta_sub_coe (L : PeriodPair) (z : ℂ) (l : ↥L.lattice) : L.weierstrassZeta (z - ↑l) = L.weierstrassZeta z - L.quasiPeriod l

ζ(z - l) = ζ(z) - η(l) for every z and l ∈ Λ.

theorem PeriodPair.quasiPeriod_eq_intCast_mul_add (L : PeriodPair) (l : ↥L.lattice) {m n : ℤ} (h : ↑m * L.ω₁ + ↑n * L.ω₂ = ↑l) : L.quasiPeriod l = ↑m * L.quasiPeriod ⟨L.ω₁, ⋯⟩ + ↑n * L.quasiPeriod ⟨L.ω₂, ⋯⟩

The quasi-periods are determined by those of the two periods: if l = m ω₁ + n ω₂, then η(l) = m η(ω₁) + n η(ω₂).

theorem PeriodPair.quasiPeriod_eq_two_mul_weierstrassZeta (L : PeriodPair) (l : ↥L.lattice) : L.quasiPeriod l = 2 * L.weierstrassZeta (↑l / 2)

Since ζ is odd, η(l) = 2 ζ(l / 2) for every l ∈ Λ.