Product identities for the Dedekind eta function

Mathlib's Dedekind eta function is η(τ) = q^{1/24} ∏_{n ≥ 1} (1 - qⁿ) with q = e^{2π i τ} and q^{1/24} = e^{2π i τ / 24} (ModularForm.eta). This file compares η at 2τ, τ / 2 and (τ + 1) / 2 with η(τ) by explicit products: with s = e^{π i τ}, so that q = s²,

• η(2τ) = e^{π i τ / 12} η(τ) ∏_{n ≥ 1} (1 + qⁿ);
• η(τ / 2) = e^{-π i τ / 24} η(τ) ∏_{n ≥ 0} (1 - s^{2n+1});
• η((τ + 1) / 2) = e^{π i / 24} e^{-π i τ / 24} η(τ) ∏_{n ≥ 0} (1 + s^{2n+1}).

Up to powers of q, the three products on the right are Weber's modular functions 𝔣₂/√2, 𝔣₁ and 𝔣, so these identities express Weber's functions, and the level-two Siegel functions, as quotients of eta values. The file also records the square of the transformation of η under S : τ ↦ -1/τ, η(-1/τ)² = -i τ η(τ)², which avoids the branch of √τ in Mathlib's ModularForm.eta_comp_eq_csqrt_I_inv, and compares that transformation at τ and at c τ for real c > 0, where the branches of √(c τ) and √τ differ by the factor √c.

Main results

• TauCeti.ModularForm.eta_eq_exp_mul_tprod: η(τ) = e^{2π i τ / 24} ∏_{n ≥ 1} (1 - qⁿ).
• TauCeti.ModularForm.eta_two_mul, TauCeti.ModularForm.eta_div_two, TauCeti.ModularForm.eta_add_one_div_two: the three product identities above.
• TauCeti.ModularForm.eta_neg_one_div_sq: η(-1/τ)² = -i τ η(τ)² on the upper half-plane.
• TauCeti.ModularForm.eta_neg_one_div_ofReal_mul_mul: η(-1/(c τ)) η(τ) = √c η(c τ) η(-1/τ) for real c > 0.

References

• D. A. Cox, Primes of the Form x² + ny², §12 (Weber's functions as eta quotients).

theorem TauCeti.ModularForm.eta_eq_exp_mul_tprod (τ : ℂ) : ModularForm.eta τ = Complex.exp (2 * ↑Real.pi * Complex.I * τ / 24) * ∏' (n : ℕ), (1 - Complex.exp (2 * ↑Real.pi * Complex.I * τ) ^ (n + 1))

Mathlib's Dedekind eta function as an exponential times the Euler product: η(τ) = e^{2π i τ / 24} ∏_{n ≥ 1} (1 - qⁿ) with q = e^{2π i τ}.

theorem TauCeti.ModularForm.eta_two_mul {τ : ℂ} (hτ : 0 < τ.im) : ModularForm.eta (2 * τ) = Complex.exp (↑Real.pi * Complex.I * τ / 12) * ModularForm.eta τ * ∏' (n : ℕ), (1 + Complex.exp (2 * ↑Real.pi * Complex.I * τ) ^ (n + 1))

η(2τ) = e^{π i τ / 12} η(τ) ∏_{n ≥ 1} (1 + qⁿ) on the upper half-plane, where q = e^{2π i τ}.

theorem TauCeti.ModularForm.eta_div_two {τ : ℂ} (hτ : 0 < τ.im) : ModularForm.eta (τ / 2) = Complex.exp (-(↑Real.pi * Complex.I * τ / 24)) * ModularForm.eta τ * ∏' (n : ℕ), (1 - Complex.exp (↑Real.pi * Complex.I * τ) ^ (2 * n + 1))

η(τ / 2) = e^{-π i τ / 24} η(τ) ∏_{n ≥ 0} (1 - s^{2n+1}) on the upper half-plane, where s = e^{π i τ}.

theorem TauCeti.ModularForm.eta_add_one_div_two {τ : ℂ} (hτ : 0 < τ.im) : ModularForm.eta ((τ + 1) / 2) = Complex.exp (↑Real.pi * Complex.I / 24) * Complex.exp (-(↑Real.pi * Complex.I * τ / 24)) * ModularForm.eta τ * ∏' (n : ℕ), (1 + Complex.exp (↑Real.pi * Complex.I * τ) ^ (2 * n + 1))

η((τ + 1) / 2) = e^{π i / 24} e^{-π i τ / 24} η(τ) ∏_{n ≥ 0} (1 + s^{2n+1}) on the upper half-plane, where s = e^{π i τ}.

theorem TauCeti.ModularForm.eta_neg_one_div_sq {τ : ℂ} (hτ : 0 < τ.im) : ModularForm.eta (-1 / τ) ^ 2 = -Complex.I * τ * ModularForm.eta τ ^ 2

The square of the S-transformation of η: η(-1/τ)² = -i τ η(τ)² on the upper half-plane.

theorem TauCeti.ModularForm.eta_neg_one_div_ofReal_mul_mul {c : ℝ} (hc : 0 < c) {τ : ℂ} (hτ : 0 < τ.im) : ModularForm.eta (-1 / (↑c * τ)) * ModularForm.eta τ = ↑√c * ModularForm.eta (↑c * τ) * ModularForm.eta (-1 / τ)

The S-transformation of η at a positive real multiple: for real c > 0, η(-1/(c τ)) η(τ) = √c η(c τ) η(-1/τ) on the upper half-plane. The branch of √(c τ) in Mathlib's ModularForm.eta_comp_eq_csqrt_I_inv is √c √τ, so no sign is lost.