Documentation

Mathlib.NumberTheory.ModularForms.DedekindEta

Dedekind eta function #

Main definitions #

References #

@[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
Instances For
    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)
    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
    Instances For

      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)