Quasiperiods and the Legendre relation

Statements from chapter 2 of Milla (arXiv:1809.00533v6, file 070_Quasiperiods.tex):

• PeriodPair.eta₁, PeriodPair.eta₂ : the basic quasiperiods η₁ = 2ζ(ω₁/2) and η₂ = 2ζ(ω₂/2) (paper Def. defetak; by oddness of ζ, 2ζ(ω_k/2) equals ζ(z+ω_k) - ζ(z) for any z ∉ L);
• quasi-periodicity of ζ (paper eta, defetak);
• the Legendre relation η₁ω₂ - η₂ω₁ = 2πi (paper legendre) — the paper's residue computation implicitly uses a positively oriented basis, so we state it under the orientation hypothesis 0 < Im(ω₂/ω₁), which holds for L = Lτ τ;
• the bridge η₁(L_τ) = G₂(τ) to Mathlib's Eisenstein series EisensteinSeries.G2 (the Eisenstein summation of η₁; with G₂ = 2ζ(2)E₂ and ζ(2) = π²/6 this is the paper's η₁ = π²E₂/3 from Thm. fouriertheorem, proved in Fourier.lean).

All statements in this file are fully proved.

noncomputable def PeriodPair.eta₁ (L : PeriodPair) : ℂ

The first basic quasiperiod η₁(L) = 2ζ(ω₁/2) (paper Def. defetak; this equals ζ(z+ω₁) - ζ(z) for every z ∉ L, see weierstrassZeta_add_ω₁).

Equations

• L.eta₁ = 2 * L.weierstrassZeta (L.ω₁ / 2)

noncomputable def PeriodPair.eta₂ (L : PeriodPair) : ℂ

The second basic quasiperiod η₂(L) = 2ζ(ω₂/2) (paper Def. defetak; this equals ζ(z+ω₂) - ζ(z) for every z ∉ L, see weierstrassZeta_add_ω₂).

Equations

• L.eta₂ = 2 * L.weierstrassZeta (L.ω₂ / 2)

theorem PeriodPair.weierstrassZeta_add_ω₁ (L : PeriodPair) (z : ℂ) (hz : z ∉ L.lattice) : L.weierstrassZeta (z + L.ω₁) = L.weierstrassZeta z + L.eta₁

Quasi-periodicity of ζ in the direction ω₁: ζ(z+ω₁) = ζ(z) + η₁ for z ∉ L (paper eta and Def. defetak).

theorem PeriodPair.weierstrassZeta_add_ω₂ (L : PeriodPair) (z : ℂ) (hz : z ∉ L.lattice) : L.weierstrassZeta (z + L.ω₂) = L.weierstrassZeta z + L.eta₂

Quasi-periodicity of ζ in the direction ω₂: ζ(z+ω₂) = ζ(z) + η₂ for z ∉ L (paper eta and Def. defetak).

A local copy of the scaling action a • L

The scaling action a • L and its transformation laws live in Lattices.lean, which imports this file, so they are not available here. We replicate the small part we need as private helpers.

theorem PeriodPair.legendre_relation (L : PeriodPair) (h : 0 < (L.ω₂ / L.ω₁).im) : L.eta₁ * L.ω₂ - L.eta₂ * L.ω₁ = 2 * ↑Real.pi * Complex.I

Legendre's relation (paper legendre): η₁ω₂ - η₂ω₁ = 2πi for a positively oriented basis (0 < Im(ω₂/ω₁); for the opposite orientation the right-hand side is -2πi).

theorem Chudnovsky.legendre_Lτ (τ : UpperHalfPlane) : (Lτ τ).eta₁ * ↑τ - (Lτ τ).eta₂ = 2 * ↑Real.pi * Complex.I

Legendre's relation for the lattice L_τ = ℤ + ℤτ: η₁τ - η₂ = 2πi (paper legendre with ω₁ = 1, ω₂ = τ).

theorem Chudnovsky.eta₁_Lτ_eq_G2 (τ : UpperHalfPlane) : (Lτ τ).eta₁ = EisensteinSeries.G2 τ

The first quasiperiod of L_τ is the weight-2 Eisenstein series G₂ in its Eisenstein summation order (Mathlib's EisensteinSeries.G2, summed over symmetric intervals). Together with G₂ = 2ζ(2)·E₂ and ζ(2) = π²/6, this is the paper's η₁(L_τ) = π²E₂(τ)/3 from Thm. fouriertheorem (see Fourier.lean).