theorem ComplexLattice.weierstrassPFun_periodic (L : ComplexLattice) : L.IsLatticePeriodic L.weierstrassPFun

The Weierstrass ℘-function for a lattice L is periodic with respect to L: shifting the input by any lattice element leaves the value unchanged.

theorem ComplexLattice.derivWeierstrassPFun_periodic (L : ComplexLattice) : L.IsLatticePeriodic L.derivWeierstrassPFun

The derivative ℘' of the Weierstrass ℘-function is also L-periodic.

theorem ComplexLattice.weierstrassPFun_isElliptic (L : ComplexLattice) : L.IsEllipticFunction L.weierstrassPFun

The Weierstrass ℘-function is an elliptic function: meromorphic on ℂ and L-periodic.

theorem ComplexLattice.derivWeierstrassPFun_isElliptic (L : ComplexLattice) : L.IsEllipticFunction L.derivWeierstrassPFun

The derivative ℘' is an elliptic function: meromorphic on ℂ and L-periodic.

theorem ComplexLattice.lattice_mem_fundamentalDomain_eq_zero (L : ComplexLattice) (z : ℂ) (hz_lat : z ∈ PeriodPair.lattice L) (hz_fd : z ∈ ZSpan.fundamentalDomain (PeriodPair.basis L)) : z = 0

The only lattice point inside the fundamental parallelogram of L (as a ZSpan-style fundamental domain) is the origin.

theorem ComplexLattice.poleMultiplicity_weierstrassP_zero (L : ComplexLattice) : poleMultiplicity L.weierstrassPFun 0 = 2

The Weierstrass ℘-function has a pole of multiplicity exactly 2 at the origin.

theorem ComplexLattice.poleMultiplicity_derivWeierstrassP_zero (L : ComplexLattice) : poleMultiplicity L.derivWeierstrassPFun 0 = 3

The derivative ℘' has a pole of multiplicity exactly 3 at the origin.

theorem ComplexLattice.polesInFundParallelogram_weierstrassP_eq (L : ComplexLattice) : L.polesInFundParallelogram L.weierstrassPFun 0 = {0}

The set of poles of the Weierstrass ℘-function inside the fundamental parallelogram (anchored at 0) consists of just the origin.

theorem ComplexLattice.polesInFundParallelogram_derivWeierstrassP_eq (L : ComplexLattice) : L.polesInFundParallelogram L.derivWeierstrassPFun 0 = {0}

The set of poles of ℘' inside the fundamental parallelogram (anchored at 0) consists of just the origin.

theorem ComplexLattice.weierstrassPFun_ellipticOrder (L : ComplexLattice) : L.ellipticOrder L.weierstrassPFun ⋯ = 2

The Weierstrass ℘-function has elliptic order 2: the sum of pole multiplicities in a fundamental parallelogram equals 2.

theorem ComplexLattice.weierstrassPFun_sub_const_isElliptic (L : ComplexLattice) (c : ℂ) : L.IsEllipticFunction fun (z : ℂ) => L.weierstrassPFun z - c

For any constant c, the shifted function z ↦ ℘(z) - c is also an elliptic function.

theorem ComplexLattice.weierstrassPFun_sub_const_order_zero (L : ComplexLattice) (c : ℂ) : meromorphicOrderAt (fun (z : ℂ) => L.weierstrassPFun z - c) 0 = ↑(-2)

Subtracting a constant from ℘ does not change its order at the origin: z ↦ ℘(z) - c still has meromorphic order -2 at 0.

theorem ComplexLattice.poleMultiplicity_weierstrassP_sub_const_zero (L : ComplexLattice) (c : ℂ) : poleMultiplicity (fun (z : ℂ) => L.weierstrassPFun z - c) 0 = 2

For any constant c, the function z ↦ ℘(z) - c has a pole of multiplicity 2 at the origin.

theorem ComplexLattice.polesInFundParallelogram_weierstrassP_sub_const_eq (L : ComplexLattice) (c : ℂ) : L.polesInFundParallelogram (fun (z : ℂ) => L.weierstrassPFun z - c) 0 = {0}

The poles of z ↦ ℘(z) - c in the fundamental parallelogram (anchored at 0) are exactly the origin, just as for ℘ itself.

theorem ComplexLattice.weierstrassPFun_sub_const_ellipticOrder (L : ComplexLattice) (c : ℂ) : L.ellipticOrder (fun (z : ℂ) => L.weierstrassPFun z - c) ⋯ = 2

The elliptic order of z ↦ ℘(z) - c is 2 for any constant c: as a corollary, every value of ℘ is attained exactly twice (with multiplicity) in each fundamental parallelogram.