Elliptic functions and the Liouville theorems

Statements from chapter 1 of Milla (arXiv:1809.00533v6, file 060_ElliptFunct.tex):

• PeriodPair.IsEllipticWith : an elliptic function for a lattice L — a meromorphic function on ℂ that is L-periodic;
• PeriodPair.fundamentalParallelogram : the fundamental parallelogram 𝒫 (paper Def. fund);
• Chudnovsky.residue : the residue of a function at a point, defined as the limit of circle integrals (2πi)⁻¹ ∮_{|z-c|=r} f as r → 0⁺;
• the three Liouville theorems (paper liouville1, liouville2, liouville3) and the "workhorse" lemma: two elliptic functions with the same zeros and poles (with orders) agree up to a nonzero constant factor.

All statements in this file are fully proved (no sorrys). The second Liouville theorem is proved via a self-contained parallelogram residue theorem built from Mathlib's rectangle Cauchy--Goursat primitives.

noncomputable def Chudnovsky.residue (f : ℂ → ℂ) (c : ℂ) : ℂ

The residue of f : ℂ → ℂ at a point c, defined as the limit of the circle integrals (2πi)⁻¹ ∮_{|z-c|=r} f(z) dz as r → 0⁺. For a function meromorphic at c these integrals are eventually constant in r, so the limit exists and is the usual residue; for other functions the value is junk.

Equations

• Chudnovsky.residue f c = (nhdsWithin 0 (Set.Ioi 0)).limUnder fun (r : ℝ) => (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(c, r), f z

theorem Chudnovsky.residue_eq_of_eventuallyEq {f : ℂ → ℂ} {c a : ℂ} (h : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(c, r), f z = a) : residue f c = a

If the normalised circle integrals defining the residue are eventually equal to a constant a as the radius r → 0⁺, then residue f c = a. This is the basic tool for computing residues: the integrals need only be known for all small r.

theorem Chudnovsky.residue_congr {f₁ f₂ : ℂ → ℂ} {c : ℂ} (h : f₁ =ᶠ[nhdsWithin c {c}ᶜ] f₂) : residue f₁ c = residue f₂ c

The residue depends only on the germ of f on a punctured neighbourhood of c.

theorem Chudnovsky.residue_sub_center_inv (c : ℂ) : residue (fun (z : ℂ) => (z - c)⁻¹) c = 1

The residue of (z - c)⁻¹ at c is 1.

theorem Chudnovsky.residue_add_of_periodic {f : ℂ → ℂ} {c ω : ℂ} (h : ∀ (z : ℂ), f (z + ω) = f z) : residue f (c + ω) = residue f c

Translation invariance of the residue. If f has period ω (f (z + ω) = f z), then its residues at c and at c + ω agree. This lets one transport a residue count from a fundamental parallelogram to any lattice translate of it.

theorem Chudnovsky.residue_eq_zero_of_analyticAt {f : ℂ → ℂ} {c : ℂ} (hf : AnalyticAt ℂ f c) : residue f c = 0

A function analytic at c has residue 0 there.

theorem Chudnovsky.residue_simplePole_add_analytic {c a : ℂ} {w : ℂ → ℂ} (hw : AnalyticAt ℂ w c) : residue (fun (z : ℂ) => a * (z - c)⁻¹ + w z) c = a

The residue of a simple pole a·(z-c)⁻¹ plus an analytic part is the coefficient a.

theorem Chudnovsky.residue_logDeriv_eq_order {f : ℂ → ℂ} {c : ℂ} (hf : MeromorphicAt f c) (hord : meromorphicOrderAt f c ≠ ⊤) : residue (logDeriv f) c = ↑(meromorphicOrderAt f c).untop₀

Residue of the logarithmic derivative equals the order. For a function f meromorphic at c with finite order there, the residue of f'/f = logDeriv f at c equals the order of f at c (a simple pole with integer residue). This is the local computation behind the third Liouville theorem.

def PeriodPair.IsEllipticWith (L : PeriodPair) (f : ℂ → ℂ) : Prop

An elliptic function for the lattice of the period pair L: a meromorphic function ℂ → ℂ which is periodic with respect to every lattice point (paper Def. of "elliptic function", ch. 1).

Equations

• L.IsEllipticWith f = (Meromorphic f ∧ ∀ (z : ℂ) (l : ↥L.lattice), f (z + ↑l) = f z)

def PeriodPair.fundamentalParallelogram (L : PeriodPair) : Set ℂ

The fundamental parallelogram 𝒫 = {s·ω₁ + t·ω₂ | 0 ≤ s, t < 1} (paper Def. fund). Every z : ℂ is equivalent modulo L.lattice to exactly one point of 𝒫.

Equations

• L.fundamentalParallelogram = {z : ℂ | ∃ s ∈ Set.Ico 0 1, ∃ t ∈ Set.Ico 0 1, z = s • L.ω₁ + t • L.ω₂}

theorem PeriodPair.isEllipticWith_weierstrassP (L : PeriodPair) : L.IsEllipticWith L.weierstrassP

℘ is an elliptic function.

theorem PeriodPair.isEllipticWith_derivWeierstrassP (L : PeriodPair) : L.IsEllipticWith L.derivWeierstrassP

℘' is an elliptic function.

theorem PeriodPair.exists_sub_mem_lattice_of_mem_fundamentalParallelogram (L : PeriodPair) (z : ℂ) : ∃ w ∈ L.fundamentalParallelogram, z - w ∈ L.lattice

Every z : ℂ differs by a lattice point from a point of the fundamental parallelogram.

theorem PeriodPair.IsEllipticWith.exists_eq_const_of_differentiable {L : PeriodPair} {f : ℂ → ℂ} (hf : L.IsEllipticWith f) (hd : Differentiable ℂ f) : ∃ (c : ℂ), f = fun (x : ℂ) => c

First Liouville theorem (paper liouville1): an elliptic function without poles (i.e. entire) is constant.

theorem PeriodPair.IsEllipticWith.finite_nonAnalytic {L : PeriodPair} {f : ℂ → ℂ} (hf : L.IsEllipticWith f) : {z : ℂ | z ∈ L.fundamentalParallelogram ∧ ¬AnalyticAt ℂ f z}.Finite

An elliptic function has only finitely many singularities in the (bounded) fundamental parallelogram. Part of the second Liouville theorem (paper liouville2).

noncomputable def PeriodPair.boundaryIntegral (L : PeriodPair) (f : ℂ → ℂ) (v : ℂ) : ℂ

The integral of f along the (positively oriented) boundary of the parallelogram with base point v and sides ω₁, ω₂, parametrised over t ∈ [0,1]. The four terms are the bottom, right, top (reversed) and left (reversed) edges; this is the contour used in the residue-theorem proof of the second Liouville theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem PeriodPair.IsEllipticWith.boundaryIntegral_eq_zero {L : PeriodPair} {f : ℂ → ℂ} (hf : L.IsEllipticWith f) (v : ℂ) : L.boundaryIntegral f v = 0

Boundary integral of an elliptic function vanishes (paper liouville2, the cancellation of opposite edges). By double periodicity the top edge repeats the bottom edge and the right edge repeats the left edge, so with the orientation above the four contributions cancel in pairs. This is the analysis-free half of the second Liouville theorem: combined with a parallelogram residue theorem (boundaryIntegral f v = 2πi · Σ residues inside, still open) it yields sum_residue_eq_zero.

def PeriodPair.boundarySet (L : PeriodPair) (v : ℂ) : Set ℂ

The boundary of the parallelogram with base point v: the union of its four edges.

Equations

• One or more equations did not get rendered due to their size.

theorem PeriodPair.IsEllipticWith.sum_residue_eq_zero {L : PeriodPair} {f : ℂ → ℂ} (hf : L.IsEllipticWith f) : ∑ z ∈ ⋯.toFinset, Chudnovsky.residue f z = 0

Second Liouville theorem (paper liouville2): the residues of an elliptic function over a fundamental parallelogram sum to 0.

The paper sums over the poles of f in a shifted parallelogram 𝒫 + v; since every point of ℂ is equivalent mod L to exactly one point of 𝒫 and residues of an elliptic function are invariant under lattice translation (Chudnovsky.residue_add_of_periodic), summing over the singular points inside 𝒫 itself is an equivalent formulation. The proof chooses a base point v' = -ε₁ω₁ - ε₂ω₂ so that every singularity class has a unique representative strictly inside the shifted parallelogram, then applies the parallelogram residue theorem (sum_residue_eq_zero_of_boundaryIntegral_eq_zero) together with the vanishing of the boundary integral by double periodicity (boundaryIntegral_eq_zero).

theorem PeriodPair.IsEllipticWith.finite_order_ne_zero {L : PeriodPair} {f : ℂ → ℂ} (hf : L.IsEllipticWith f) (h0 : ∃ (z : ℂ), meromorphicOrderAt f z ≠ ⊤) : {z : ℂ | z ∈ L.fundamentalParallelogram ∧ meromorphicOrderAt f z ≠ 0}.Finite

A not-identically-vanishing elliptic function has only finitely many zeros and poles in the fundamental parallelogram.

theorem PeriodPair.isEllipticWith_logDeriv {L : PeriodPair} {f : ℂ → ℂ} (hf : L.IsEllipticWith f) : L.IsEllipticWith (logDeriv f)

The logarithmic derivative f'/f of an elliptic function is again elliptic.

theorem PeriodPair.IsEllipticWith.sum_meromorphicOrderAt_eq_zero {L : PeriodPair} {f : ℂ → ℂ} (hf : L.IsEllipticWith f) (h0 : ∃ (z : ℂ), meromorphicOrderAt f z ≠ ⊤) : ∑ z ∈ ⋯.toFinset, (meromorphicOrderAt f z).untop₀ = 0

Third Liouville theorem (paper liouville3): an elliptic function which does not vanish identically has, modulo L, as many zeros as poles, counted with multiplicity — equivalently, the sum of the orders ord_z f over a fundamental parallelogram is 0.

The proof reduces the statement to the second Liouville theorem: logDeriv f = f'/f is again elliptic (IsEllipticWith.logDeriv), its residue at every point equals the order of f there (Chudnovsky.residue_logDeriv_eq_order), and f has a zero/pole exactly where logDeriv f fails to be analytic; so the residue sum of logDeriv f is the order sum of f.

theorem PeriodPair.IsEllipticWith.exists_const_mul_of_meromorphicOrderAt_eq {L : PeriodPair} {f g : ℂ → ℂ} (hf : L.IsEllipticWith f) (hg : L.IsEllipticWith g) (h : ∀ (z : ℂ), meromorphicOrderAt f z = meromorphicOrderAt g z) : ∃ (c : ℂ), c ≠ 0 ∧ f =ᶠ[Filter.codiscrete ℂ] fun (z : ℂ) => c * g z

Workhorse lemma (used throughout the paper, e.g. in pstrichprod, fouriersigma, and Appendix A): two elliptic functions with the same zeros and poles, counted with orders, agree up to a nonzero constant factor away from a discrete set (namely, away from their poles and points of non-normality).