Theorems · Theorem · number theory

EisensteinSeries.qExpansion_identity

∀ {k : ℕ},
  1 ≤ k →
    ∀ (z : UpperHalfPlane),
      ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
        (-2 * ↑Real.pi * Complex.I) ^ (k + 1) / ↑k.factorial *
          ∑' (n : ℕ), ↑n ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n

This is one key identity relating infinite series to q-expansions which shows that ∑' n, 1 / (z + n) ^ (k + 1) = ((-2 π I) ^ (k + 1) / k !) * ∑' n, n ^ k q ^n where q = cexp (2 π I z).

Defined in

Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Cited by

1 results in Mathlib

Foundations

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