The Weierstrass σ- and ζ-functions

Statements from chapter 1 of Milla, A detailed proof of the Chudnovsky formula with means of a basic first year approach (arXiv:1809.00533v6, file 060_ElliptFunct.tex):

• PeriodPair.weierstrassSigma : the Weierstrass σ-function σ(z; L) = z·∏_{ω ∈ L, ω ≠ 0} (1 - z/ω)·exp(z/ω + z²/(2ω²)) (paper Def. defisigma);
• PeriodPair.weierstrassZeta : the Weierstrass ζ-function ζ(z; L) = 1/z + ∑_{ω ∈ L, ω ≠ 0} (1/(z-ω) + 1/ω + z/ω²) (paper Def. defizeta);
• convergence statements (paper Rem. bemsigma), oddness of σ and ζ (paper sigmaodd), the location and simplicity of the zeros of σ (paper Rem. bemsigma), ζ = σ'/σ (paper Def. defizeta) and ζ' = -℘ (paper Def. defiwp).

All nontrivial proofs are sorry-ed for now; this file pins the statements.

noncomputable def PeriodPair.weierstrassSigmaTerm (z w : ℂ) : ℂ

The factor of the Weierstrass σ-product associated to a nonzero lattice point w: (1 - z/w)·exp(z/w + z²/(2w²)).

Equations

• PeriodPair.weierstrassSigmaTerm z w = (1 - z / w) * Complex.exp (z / w + z ^ 2 / (2 * w ^ 2))

noncomputable def PeriodPair.weierstrassZetaTerm (z w : ℂ) : ℂ

The summand of the Weierstrass ζ-series associated to a nonzero lattice point w: 1/(z-w) + 1/w + z/w².

Equations

• PeriodPair.weierstrassZetaTerm z w = 1 / (z - w) + 1 / w + z / w ^ 2

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

The Weierstrass σ-function of the lattice L (paper Def. defisigma): σ(z; L) = z·∏_{ω ∈ L, ω ≠ 0} (1 - z/ω)·exp(z/ω + z²/(2ω²)).

Equations

• L.weierstrassSigma z = z * ∏' (l : { l : ↥L.lattice // l ≠ 0 }), PeriodPair.weierstrassSigmaTerm z ↑↑l

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

The Weierstrass ζ-function of the lattice L (paper Def. defizeta): ζ(z; L) = 1/z + ∑_{ω ∈ L, ω ≠ 0} (1/(z-ω) + 1/ω + z/ω²).

Equations

• L.weierstrassZeta z = 1 / z + ∑' (l : { l : ↥L.lattice // l ≠ 0 }), PeriodPair.weierstrassZetaTerm z ↑↑l

Helper lemmas

Convergence (paper Rem. bemsigma)

theorem PeriodPair.multipliable_weierstrassSigmaTerm (L : PeriodPair) (z : ℂ) : Multipliable fun (l : { l : ↥L.lattice // l ≠ 0 }) => weierstrassSigmaTerm z ↑↑l

The σ-product converges for every z.

theorem PeriodPair.hasProdLocallyUniformly_weierstrassSigmaTerm (L : PeriodPair) : HasProdLocallyUniformly (fun (l : { l : ↥L.lattice // l ≠ 0 }) (z : ℂ) => weierstrassSigmaTerm z ↑↑l) fun (z : ℂ) => ∏' (l : { l : ↥L.lattice // l ≠ 0 }), weierstrassSigmaTerm z ↑↑l

The σ-product converges locally uniformly on ℂ.

theorem PeriodPair.summable_weierstrassZetaTerm (L : PeriodPair) (z : ℂ) (_hz : z ∉ L.lattice) : Summable fun (l : { l : ↥L.lattice // l ≠ 0 }) => weierstrassZetaTerm z ↑↑l

The ζ-series converges away from the lattice.

theorem PeriodPair.hasSumLocallyUniformlyOn_weierstrassZetaTerm (L : PeriodPair) : HasSumLocallyUniformlyOn (fun (l : { l : ↥L.lattice // l ≠ 0 }) (z : ℂ) => weierstrassZetaTerm z ↑↑l) (fun (z : ℂ) => ∑' (l : { l : ↥L.lattice // l ≠ 0 }), weierstrassZetaTerm z ↑↑l) (↑L.lattice)ᶜ

The ζ-series converges locally uniformly away from the lattice.

Basic properties

theorem PeriodPair.differentiable_weierstrassSigma (L : PeriodPair) : Differentiable ℂ L.weierstrassSigma

σ is an entire function.

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

ζ is holomorphic away from the lattice.

theorem PeriodPair.weierstrassSigma_neg (L : PeriodPair) (z : ℂ) : L.weierstrassSigma (-z) = -L.weierstrassSigma z

σ is an odd function (paper Prop. sigmaodd).

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

ζ is an odd function.

Zeros of σ (paper Rem. bemsigma)

theorem PeriodPair.weierstrassSigma_eq_zero_iff (L : PeriodPair) (z : ℂ) : L.weierstrassSigma z = 0 ↔ z ∈ L.lattice

The zeros of σ are exactly the lattice points.

theorem PeriodPair.meromorphicOrderAt_weierstrassSigma (L : PeriodPair) (l : ℂ) (hl : l ∈ L.lattice) : meromorphicOrderAt L.weierstrassSigma l = 1

The zeros of σ at the lattice points are simple (order 1).

The logarithmic derivative and ζ' = -℘

theorem PeriodPair.logDeriv_weierstrassSigma (L : PeriodPair) (z : ℂ) (hz : z ∉ L.lattice) : logDeriv L.weierstrassSigma z = L.weierstrassZeta z

ζ is the logarithmic derivative of σ (paper Def. defizeta).

theorem PeriodPair.deriv_weierstrassZeta (L : PeriodPair) (z : ℂ) (hz : z ∉ L.lattice) : deriv L.weierstrassZeta z = -L.weierstrassP z

℘ is the negative derivative of ζ (paper Def. defiwp).