Theorems · Theorem · number theory

UpperHalfPlane.qExpansion_coeff_eq_circleIntegral

∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f →
          ∀ (n : ℕ) {R : ℝ},
            0 < R →
              R < 1 →
                (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h f) =
                  (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), UpperHalfPlane.cuspFunction h f z / z ^ (n + 1)

The q-expansion coefficient can be expressed as a circleIntegral for any radius 0 < R < 1.

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

1 results in Mathlib

Foundations

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