theorem ComplexLattice.periodic_int_mul {f : ℂ → ℂ} {ω : ℂ} (h : ∀ (w : ℂ), f (w + ω) = f w) (n : ℤ) (w : ℂ) : f (w + ↑n * ω) = f w

If f : ℂ → ℂ is periodic with period ω, then it is periodic with period n * ω for every integer n. Inductive consequence of additive periodicity.

def ComplexLattice.IsLatticePeriodic (L : ComplexLattice) (f : ℂ → ℂ) : Prop

A function f : ℂ → ℂ is L-periodic if f(z + ω) = f(z) for every z ∈ ℂ and every lattice element ω ∈ L.

structure ComplexLattice.IsEllipticFunction (L : ComplexLattice) (f : ℂ → ℂ) : Prop

Definition 14.8: an elliptic function for L is a meromorphic function on ℂ that is L-periodic.

• meromorphic : Meromorphic f
• periodic : L.IsLatticePeriodic f

theorem ComplexLattice.isLatticePeriodic_const {L : ComplexLattice} (c : ℂ) : L.IsLatticePeriodic fun (x : ℂ) => c

Constant functions are L-periodic for any lattice L.

noncomputable def ComplexLattice.poleMultiplicity (f : ℂ → ℂ) (z : ℂ) : ℕ

The order of a pole of f at z: n if f has a pole of order n at z, and 0 if f is holomorphic or has a zero at z. Extracted from meromorphicOrderAt by negating and clamping to ℕ.

def ComplexLattice.IsPoleAt (f : ℂ → ℂ) (z : ℂ) : Prop

f has a pole at z iff its meromorphic order is strictly negative.

def ComplexLattice.polesInFundParallelogram (L : ComplexLattice) (f : ℂ → ℂ) (α : ℂ) : Set ℂ

The set of poles of f lying in the fundamental parallelogram with corner α.

theorem ComplexLattice.polesInFundParallelogram_finite {L : ComplexLattice} {f : ℂ → ℂ} (hf : L.IsEllipticFunction f) (α : ℂ) : (L.polesInFundParallelogram f α).Finite

The poles of an elliptic function in any fundamental parallelogram form a finite set, because they are a discrete subset of a bounded region (the closure of the parallelogram is compact).

noncomputable def ComplexLattice.ellipticOrder (L : ComplexLattice) (f : ℂ → ℂ) (hf : L.IsEllipticFunction f) : ℕ

Definition 14.9: the order of an elliptic function f for L, computed as the sum of pole multiplicities in the fundamental parallelogram with corner 0.

theorem ComplexLattice.ellipticOrder_independent {L : ComplexLattice} {f : ℂ → ℂ} (hf : L.IsEllipticFunction f) (α : ℂ) : ∑ z ∈ ⋯.toFinset, poleMultiplicity f z = L.ellipticOrder f hf

The order of an elliptic function is independent of the choice of fundamental parallelogram.

def ComplexLattice.IsNonzeroElliptic (L : ComplexLattice) (f : ℂ → ℂ) : Prop

f is a nonzero elliptic function for L if it is elliptic and not identically zero.

def ComplexLattice.zerosAndPolesInFundParallelogram (L : ComplexLattice) (f : ℂ → ℂ) (α : ℂ) : Set ℂ

The set of points in the fundamental parallelogram with corner α where f has a nonzero ord (i.e., a zero or a pole).

theorem ComplexLattice.zerosAndPolesInFundParallelogram_finite {L : ComplexLattice} {f : ℂ → ℂ} (hf : L.IsNonzeroElliptic f) (α : ℂ) : (L.zerosAndPolesInFundParallelogram f α).Finite

The zeros and poles of a nonzero elliptic function in any fundamental parallelogram form a finite set.

theorem ComplexLattice.ord_ne_top_of_nonzeroElliptic {L : ComplexLattice} {f : ℂ → ℂ} (hf : L.IsNonzeroElliptic f) (z : ℂ) : ord z f ≠ ⊤

For a nonzero elliptic function f, the order ord_z(f) is finite (never ⊤).

noncomputable def ComplexLattice.ordInt {L : ComplexLattice} {f : ℂ → ℂ} (hf : L.IsNonzeroElliptic f) (z : ℂ) : ℤ

The integer-valued order ord_z(f) ∈ ℤ for a nonzero elliptic function, extracted by removing the ⊤ case.

theorem ComplexLattice.exists_fundParallelogram_boundary {L : ComplexLattice} {f : ℂ → ℂ} (hf : L.IsNonzeroElliptic f) (α : ℂ) : ∃ (γ : PiecewiseSmoothCurve) (Ω : Set ℂ) (N : ℕ) (pts : Fin N → ℂ) (ords : Fin N → ℤ), IsOpen Ω ∧ γ.IsClosed ∧ γ.IsSimple ∧ γ.IsPositivelyOriented ∧ (∀ (i : Fin γ.n), ∀ t ∈ Set.Icc (γ.pieces i).a (γ.pieces i).b, (γ.pieces i).toFun t ∈ Ω) ∧ γ.image ∪ γ.interiorRegion ⊆ Ω ∧ IsMeromorphicOn f Ω ∧ (∀ (k : Fin N), pts k ∈ γ.interiorRegion) ∧ (∀ (k : Fin N), ord (pts k) f = ↑(ords k)) ∧ (∀ z ∈ Ω, (∀ (k : Fin N), z ≠ pts k) → AnalyticAt ℂ f z ∧ f z ≠ 0) ∧ (∀ (i : Fin γ.n), ∀ t ∈ Set.Icc (γ.pieces i).a (γ.pieces i).b, AnalyticAt ℂ f ((γ.pieces i).toFun t) ∧ f ((γ.pieces i).toFun t) ≠ 0) ∧ ∑ z ∈ ⋯.toFinset, ordInt hf z = ∑ k : Fin N, ords k

For any nonzero elliptic function and any corner α, there exists a piecewise smooth boundary curve γ of (a perturbation of) the fundamental parallelogram such that f is meromorphic on an enclosing open set Ω, the zeros/poles of f lie in the interior of γ, and the sum of ord values matches the sum along the boundary. This packages the data needed to apply the argument principle.

theorem ComplexLattice.contour_integral_f'_over_f_vanishes {L : ComplexLattice} {f : ℂ → ℂ} (hf : L.IsNonzeroElliptic f) (γ : PiecewiseSmoothCurve) : PiecewiseSmoothCurve.contourIntegral (fun (z : ℂ) => deriv f z / f z) γ = 0

The contour integral of f'/f around the boundary γ of a fundamental parallelogram vanishes, because periodic boundary identifications make opposite sides cancel.

theorem ComplexLattice.sum_ord_eq_zero_of_nonzeroElliptic {L : ComplexLattice} {f : ℂ → ℂ} (hf : L.IsNonzeroElliptic f) (α : ℂ) : ∑ z ∈ ⋯.toFinset, ordInt hf z = 0

Theorem 14.18: for any nonzero elliptic function f, the number of zeros equals the number of poles in any fundamental parallelogram (counted with multiplicity). Equivalently, the sum of ord over zeros and poles is zero. Proof combines the argument principle (Theorem 14.17) with vanishing of the boundary contour integral.