noncomputable def ComplexLattice.weierstrassPFun (L : ComplexLattice) (z : ℂ) : ℂ

The Weierstrass ℘-function associated to the complex lattice L, packaged as a function ℂ → ℂ.

theorem ComplexLattice.weierstrassPFun_differentiableOn (L : ComplexLattice) : DifferentiableOn ℂ L.weierstrassPFun (↑(PeriodPair.lattice L))ᶜ

The Weierstrass ℘-function is differentiable on the complement of the lattice.

theorem ComplexLattice.weierstrassPFun_differentiableAt (L : ComplexLattice) {z₀ : ℂ} (hz₀ : z₀ ∉ ↑(PeriodPair.lattice L)) : DifferentiableAt ℂ L.weierstrassPFun z₀

The Weierstrass ℘-function is differentiable at any point not in the lattice.

theorem ComplexLattice.weierstrassPFun_analyticOnNhd (L : ComplexLattice) : AnalyticOnNhd ℂ L.weierstrassPFun (↑(PeriodPair.lattice L))ᶜ

The Weierstrass ℘-function is analytic on neighborhoods of points off the lattice.

theorem ComplexLattice.weierstrassPFun_meromorphic (L : ComplexLattice) : Meromorphic L.weierstrassPFun

The Weierstrass ℘-function is a meromorphic function on ℂ.

theorem ComplexLattice.weierstrassPFun_order (L : ComplexLattice) (l₀ : ℂ) (h : l₀ ∈ PeriodPair.lattice L) : meromorphicOrderAt L.weierstrassPFun l₀ = -2

At every lattice point l₀, the Weierstrass ℘-function has a pole of order 2.

@[simp]

theorem ComplexLattice.weierstrassPFun_even (L : ComplexLattice) (z : ℂ) : L.weierstrassPFun (-z) = L.weierstrassPFun z

The Weierstrass ℘-function is an even function: ℘(-z) = ℘(z).

theorem ComplexLattice.weierstrassPFun_laurentExpansion (L : ComplexLattice) (z : ℂ) (hz : ∀ (l : ↥(PeriodPair.lattice L)), ↑l ≠ 0 → ‖z‖ < ‖↑l‖) : HasSum (fun (n : ℕ) => (2 * ↑n + 3) * L.eisensteinSeries (2 * n + 4) * z ^ (2 * n + 2)) (L.weierstrassPFun z - 1 / z ^ 2)

The Laurent expansion of ℘(z) - 1/z² near 0: the coefficients are expressed in terms of the Eisenstein series of weight 2n + 4.

noncomputable def ComplexLattice.derivWeierstrassPFun (L : ComplexLattice) (z : ℂ) : ℂ

The derivative ℘' of the Weierstrass ℘-function as a function ℂ → ℂ.

theorem ComplexLattice.derivWeierstrassPFun_meromorphic (L : ComplexLattice) : Meromorphic L.derivWeierstrassPFun

The derivative of the Weierstrass ℘-function is meromorphic on ℂ.

@[simp]

theorem ComplexLattice.derivWeierstrassPFun_odd (L : ComplexLattice) (z : ℂ) : L.derivWeierstrassPFun (-z) = -L.derivWeierstrassPFun z

The derivative of the Weierstrass ℘-function is an odd function: ℘'(-z) = -℘'(z).

theorem ComplexLattice.derivWeierstrassPFun_analyticOnNhd (L : ComplexLattice) : AnalyticOnNhd ℂ L.derivWeierstrassPFun (↑(PeriodPair.lattice L))ᶜ

The derivative ℘' is analytic on neighborhoods of points off the lattice.

theorem ComplexLattice.derivWeierstrassPFun_order (L : ComplexLattice) (l₀ : ℂ) (h : l₀ ∈ PeriodPair.lattice L) : meromorphicOrderAt L.derivWeierstrassPFun l₀ = -3

At every lattice point l₀, the derivative ℘' has a pole of order 3.

theorem ComplexLattice.weierstrassPFun_add_lattice (L : ComplexLattice) (z ω : ℂ) (hω : ω ∈ PeriodPair.lattice L) : L.weierstrassPFun (z + ω) = L.weierstrassPFun z

℘ is doubly periodic: adding any lattice vector to the argument leaves the value unchanged.

theorem ComplexLattice.derivWeierstrassPFun_add_lattice (L : ComplexLattice) (z ω : ℂ) (hω : ω ∈ PeriodPair.lattice L) : L.derivWeierstrassPFun (z + ω) = L.derivWeierstrassPFun z

℘' is doubly periodic: adding any lattice vector to the argument leaves the value unchanged.

noncomputable def ComplexLattice.g₂Fun (L : ComplexLattice) : ℂ

The invariant g₂ of the lattice, defined as 60 times the Eisenstein series of weight 4.

noncomputable def ComplexLattice.g₃Fun (L : ComplexLattice) : ℂ

The invariant g₃ of the lattice, defined as 140 times the Eisenstein series of weight 6.

@[simp]

theorem ComplexLattice.g₂Fun_eq (L : ComplexLattice) : L.g₂Fun = PeriodPair.g₂ L

g₂Fun agrees definitionally with the field g₂ of the lattice.

@[simp]

theorem ComplexLattice.g₃Fun_eq (L : ComplexLattice) : L.g₃Fun = PeriodPair.g₃ L

g₃Fun agrees definitionally with the field g₃ of the lattice.

theorem ComplexLattice.weierstrassPFun_differentialEquation (L : ComplexLattice) (z : ℂ) (hz : z ∉ ↑(PeriodPair.lattice L)) : L.derivWeierstrassPFun z ^ 2 = 4 * L.weierstrassPFun z ^ 3 - L.g₂Fun * L.weierstrassPFun z - L.g₃Fun

The differential equation satisfied by the Weierstrass ℘-function: (℘'(z))² = 4 ℘(z)³ - g₂ ℘(z) - g₃, for z not in the lattice.