Theorems · Theorem · number theory

EisensteinSeries.E_qExpansion_coeff

∀ {k : ℕ} (hk : 3 ≤ k),
  Even k →
    ∀ (m : ℕ),
      (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑(ModularForm.E hk)) =
        if m = 0 then 1 else -(2 * ↑k / ↑(bernoulli k)) * ↑((ArithmeticFunction.sigma (k - 1)) m)

The q-expansion coefficients of the normalised Eisenstein series E k: the constant term is 1 and for m ≥ 1 the m-th coefficient is -(2k / B_k) * σ_{k-1}(m) where B_k is the k-th Bernoulli number.

Defined in

Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Cited by

3 results in Mathlib

Foundations

Depth 310 from the axioms · uses propext, Classical.choice, Quot.sound