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. Lastly, we compute its logarithmic derivative and show that it is a multiple of the Eisenstein series E2.

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)

def ModularForm.termη : Lean.ParserDescr

Notation for the Dedekind eta function.

Equations

• ModularForm.termη = Lean.ParserDescr.node `ModularForm.termη 1024 (Lean.ParserDescr.symbol "η")

theorem ModularForm.multipliable_one_sub_pow {q : ℂ} (hq : ‖q‖ < 1) : Multipliable fun (n : ℕ) => 1 - q ^ (n + 1)

For ‖q‖ < 1, the infinite product ∏ (1 - q^(n+1)) is multipliable.

theorem ModularForm.multipliableLocallyUniformlyOn_one_sub_pow : MultipliableLocallyUniformlyOn (fun (n : ℕ) (q : ℂ) => 1 - q ^ (n + 1)) (Metric.ball 0 1)

The infinite product ∏ (1 - q^(n+1)) converges locally uniformly on the open unit disc, with limit q ↦ ∏' n, (1 - q^(n+1)).

theorem ModularForm.differentiableOn_tprod_one_sub_pow : DifferentiableOn ℂ (fun (q : ℂ) => ∏' (n : ℕ), (1 - q ^ (n + 1))) (Metric.ball 0 1)

The infinite product q ↦ ∏' n, (1 - q^(n+1)) is differentiable on the open unit disc.

theorem ModularForm.differentiableOn_tprod_one_sub_pow_pow (k : ℕ) : DifferentiableOn ℂ (fun (q : ℂ) => ∏' (n : ℕ), (1 - q ^ (n + 1)) ^ k) (Metric.ball 0 1)

For any k, the function q ↦ ∏' n, (1 - q^(n+1))^k is differentiable on the open unit disc.

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_tprod_ne_zero {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : ∏' (n : ℕ), (1 - eta_q n z) ≠ 0

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_tprod {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : DifferentiableAt ℂ (fun (x : ℂ) => ∏' (n : ℕ), (1 - eta_q n x)) z

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

theorem ModularForm.logDeriv_qParam (h : ℝ) (z : ℂ) : logDeriv (Function.Periodic.qParam h) z = 2 * ↑Real.pi * Complex.I / ↑h

theorem ModularForm.summable_logDeriv_one_sub_eta_q {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : Summable fun (i : ℕ) => logDeriv (fun (x : ℂ) => 1 - eta_q i x) z

theorem ModularForm.logDeriv_eta_eq_E2 (z : UpperHalfPlane) : logDeriv eta ↑z = ↑Real.pi * Complex.I / 12 * EisensteinSeries.E2 z