Dedekind eta function

Main definitions

• We define the Dedekind eta function as the infinite product η(z) = q ^ 1/24 * ∏' (1 - q ^ (n + 1)) where q = e ^ (2πiz) and z is in the upper half-plane. The product is taken over all non-negative integers n. We then show it is non-vanishing and differentiable on the upper half-plane.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, section 1.2

@[reducible, inline]

noncomputable abbrev ModularForm.eta_q (n : ℕ) (z : ℂ) : ℂ

The q term inside the product defining the eta function. It is defined as eta_q n z = e ^ (2 π i (n + 1) z).

Equations

• ModularForm.eta_q n z = Function.Periodic.qParam 1 z ^ (n + 1)

theorem ModularForm.eta_q_eq_cexp (n : ℕ) (z : ℂ) : eta_q n z = Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * z)

theorem ModularForm.eta_q_eq_pow (n : ℕ) (z : ℂ) : eta_q n z = Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ (n + 1)

theorem ModularForm.one_sub_eta_q_ne_zero (n : ℕ) {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : 1 - eta_q n z ≠ 0

noncomputable def ModularForm.eta (z : ℂ) : ℂ

The eta function, whose value at z is q^ 1 / 24 * ∏' 1 - q ^ (n + 1) for q = e ^ 2 π i z.

Equations

• ModularForm.eta z = Function.Periodic.qParam 24 z * ∏' (n : ℕ), (1 - ModularForm.eta_q n z)

theorem ModularForm.summable_eta_q (z : UpperHalfPlane) : Summable fun (n : ℕ) => ‖-eta_q n ↑z‖

theorem ModularForm.multipliableLocallyUniformlyOn_eta : MultipliableLocallyUniformlyOn (fun (n : ℕ) (a : ℂ) => 1 - eta_q n a) UpperHalfPlane.upperHalfPlaneSet

theorem ModularForm.eta_ne_zero {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : eta z ≠ 0

Eta is non-vanishing on the upper half plane.

theorem ModularForm.logDeriv_one_sub_cexp (r : ℂ) : (logDeriv fun (z : ℂ) => 1 - r * Complex.exp z) = fun (z : ℂ) => -r * Complex.exp z / (1 - r * Complex.exp z)

theorem ModularForm.logDeriv_one_sub_mul_cexp_comp (r : ℂ) {g : ℂ → ℂ} (hg : Differentiable ℂ g) : logDeriv ((fun (z : ℂ) => 1 - r * Complex.exp z) ∘ g) = fun (z : ℂ) => -r * deriv g z * Complex.exp (g z) / (1 - r * Complex.exp (g z))

theorem ModularForm.tsum_logDeriv_eta_q (z : ℂ) : ∑' (n : ℕ), logDeriv (fun (x : ℂ) => 1 - eta_q n x) z = 2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), (↑n + 1) * -eta_q n z / (1 - eta_q n z)

theorem ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : DifferentiableAt ℂ eta z