Fourier expansions: the lattice ↔ modular-forms bridge

Statements from chapter 4 of Milla (arXiv:1809.00533v6, file 090_Fourier.tex):

• the σ product formula (paper fouriersigma) σ(z; L_τ) = (2πi)⁻¹·e^{η₁z²/2}·(q_z^{1/2} - q_z^{-1/2})·∏_{n≥1} (1-q^n q_z)(1-q^n/q_z)/(1-q^n)² with q_z^{±1/2} written branch-free as e^{±πiz};
• the bridge to normalized Eisenstein series (paper Thm. fouriertheorem): η₁(L_τ) = π²E₂(τ)/3, g₂(L_τ) = (4/3)π⁴E₄(τ), g₃(L_τ) = (8/27)π⁶E₆(τ), Δ(L_τ) = (2π)¹²/1728·(E₄³-E₆²), and J(L_τ) = E₄³/(E₄³-E₆²) = Chudnovsky.J τ.

Note the sign trap in the paper's satzphi (its displayed transformation φ(z+τ) = -e^{2πiz}φ(z) should read φ(z+τ) = -e^{-2πiz}φ(z), as in its proof); the final product formula fouriersigma stated here is unaffected.

All statements in this file are fully proved.

Helpers for the lattice ↔ Eisenstein-series bridge

theorem Chudnovsky.eta₁_Lτ (τ : UpperHalfPlane) : (Lτ τ).eta₁ = ↑Real.pi ^ 2 / 3 * EisensteinSeries.E2 τ

η₁(L_τ) = π²·E₂(τ)/3 (paper Thm. fouriertheorem). Together with eta₁_Lτ_eq_G2 this is Mathlib's G₂ = 2ζ(2)·E₂ with ζ(2) = π²/6.

theorem Chudnovsky.g₂_Lτ (τ : UpperHalfPlane) : (Lτ τ).g₂ = 4 / 3 * ↑Real.pi ^ 4 * ModularForm.E₄ τ

g₂(L_τ) = (4/3)·π⁴·E₄(τ) (paper Thm. fouriertheorem).

theorem Chudnovsky.g₃_Lτ (τ : UpperHalfPlane) : (Lτ τ).g₃ = 8 / 27 * ↑Real.pi ^ 6 * ModularForm.E₆ τ

g₃(L_τ) = (8/27)·π⁶·E₆(τ) (paper Thm. fouriertheorem).

theorem Chudnovsky.discr_Lτ (τ : UpperHalfPlane) : (Lτ τ).discr = (2 * ↑Real.pi) ^ 12 / 1728 * (ModularForm.E₄ τ ^ 3 - ModularForm.E₆ τ ^ 2)

Δ(L_τ) = (2π)¹²/1728·(E₄(τ)³ - E₆(τ)²) (paper Thm. fouriertheorem).

theorem Chudnovsky.J_eq_J_Lτ (τ : UpperHalfPlane) : J τ = (Lτ τ).J

Klein's absolute invariant of the lattice L_τ agrees with the modular J-function J = E₄³/(E₄³ - E₆²) of Basic.lean, i.e. J(τ) = g₂³/(g₂³ - 27g₃²) evaluated at L_τ (paper Thm. fouriertheorem and Def. defijdelta).

The σ transformation law (paper trafosigma)

σ(z + ω) = -exp(η_ω·(z + ω/2))·σ(z) for a basic period ω of the lattice. This is derived by the log-derivative constancy argument: σ(z+ω)/(exp(η(z+ω/2))·σ(z)) has zero derivative on the connected set Lᶜ, hence is constant, and the constant is -1 by oddness of σ.

The basic q-product Q(v) = ∏'_{n≥1} (1 - qⁿ·v)

All the infinite products in the σ-product formula are values of this single entire function Q, which satisfies the functional equation Q(v) = (1 - q·v)·Q(q·v).

Milla's φ and g functions and their transformation laws (paper satzphi)

φ(z) = exp(-η₁/2·z² + πiz)·σ(z) and g(z) = (q_z - 1)/(2πi)·Q(q_z)·Q(q_z⁻¹)/Q(1)² transform identically under z ↦ z+1 (invariant) and z ↦ z+τ (factor -e^{-2πiz}, the corrected sign of the paper's satzphi).

Entireness and non-vanishing of φ and g

φ = g via the first Liouville theorem, and the product formula

theorem Chudnovsky.weierstrassSigma_Lτ (τ : UpperHalfPlane) (z : ℂ) : (Lτ τ).weierstrassSigma z = (2 * ↑Real.pi * Complex.I)⁻¹ * Complex.exp ((Lτ τ).eta₁ * z ^ 2 / 2) * (Complex.exp (↑Real.pi * Complex.I * z) - Complex.exp (-(↑Real.pi * Complex.I * z))) * ∏' (n : ℕ+), (1 - q τ ^ ↑n * Complex.exp (2 * ↑Real.pi * Complex.I * z)) * (1 - q τ ^ ↑n / Complex.exp (2 * ↑Real.pi * Complex.I * z)) / (1 - q τ ^ ↑n) ^ 2

The σ product formula (paper fouriersigma): with q = e^{2πiτ} and q_z = e^{2πiz},

σ(z; L_τ) = (2πi)⁻¹·e^{η₁z²/2}·(e^{πiz} - e^{-πiz})·∏_{n≥1} (1-qⁿq_z)(1-qⁿ/q_z)/(1-qⁿ)².

The half-integral powers q_z^{±1/2} of the paper are written branch-free as e^{±πiz}.