Dedekind eta function #
Main definitions #
- We define the Dedekind eta function as the infinite product
η(z) = q ^ 1/24 * ∏' (1 - q ^ (n + 1))
whereq = e ^ (2πiz)
andz
is in the upper half-plane. The product is taken over all non-negative integersn
. 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][diamondshurman2005], section 1.2
@[reducible, inline]
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)
Instances For
theorem
ModularForm.one_sub_eta_q_ne_zero
(n : ℕ)
{z : ℂ}
(hz : z ∈ UpperHalfPlane.upperHalfPlaneSet)
:
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)
Instances For
theorem
ModularForm.multipliableLocallyUniformlyOn_eta :
MultipliableLocallyUniformlyOn (fun (n : ℕ) (a : ℂ) => 1 - eta_q n a) UpperHalfPlane.upperHalfPlaneSet
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.differentiableAt_eta_of_mem_upperHalfPlaneSet
{z : ℂ}
(hz : z ∈ UpperHalfPlane.upperHalfPlaneSet)
: