Ramanujan–Petersson conjecture for the τ-function (Deligne's theorem)

ramanujan_petersson — a formalization challenge from the lean-eval benchmark.

Notes

τ(n) is the n-th q-expansion coefficient of mathlib's modular discriminant ModularForm.discriminant = η²⁴, the normalised cusp form of weight 12 and level 1; the module proves τ(1) = 1 as a sanity check. Ramanujan (1916) conjectured |τ(p)| ≤ 2 p^(11/2) for every prime p; Petersson generalised it to all cusp forms, and Deligne proved it in 1974 from the Weil conjectures. The coefficients are a priori complex (integrality is classical but not needed to state the bound), so the statement bounds the complex norm ‖τ(p)‖.

Formal statement

/-- **The Ramanujan–Petersson conjecture for `τ`** (Ramanujan 1916; proved by
Deligne in 1974). For every prime `p`, `|τ(p)| ≤ 2 p^(11/2)`. -/
theorem ramanujan_petersson :
    ∀ p : ℕ, Prime p → ‖τ p‖ ≤ 2 * (p : ℝ) ^ ((11 : ℝ) / 2) := by
  sorry

Informal solution sketch

Deligne's proof: the ℓ-adic Galois representation attached to Δ (Eichler–Shimura, Deligne) realises τ(p) as the trace of Frobenius on a weight-11 piece of the étale cohomology of the universal elliptic curve over the modular curve, and Deligne's proof of the Weil conjectures (1974) gives Frobenius eigenvalues α, β with αβ = p¹¹ and |α| = |β| = p^(11/2), hence |τ(p)| = |α + β| ≤ 2 p^(11/2).

Source

S. Ramanujan, 'On certain arithmetical functions', Trans. Cambridge Philos. Soc. 22 (1916) 159–184. H. Petersson, 'Theorie der automorphen Formen beliebiger reeller Dimension und ihre Darstellung durch eine neue Art Poincaréscher Reihen', Math. Ann. 103 (1930) 369–436. P. Deligne, 'Formes modulaires et représentations ℓ-adiques', Séminaire Bourbaki 1968/69: Exposés 347–363, Lecture Notes in Math. 179, Springer (1971). P. Deligne, 'La conjecture de Weil. I', Publ. Math. IHÉS 43 (1974) 273–307. Background: https://en.wikipedia.org/wiki/Ramanujan%E2%80%93Petersson_conjecture

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: ramanujan_petersson
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Seewoo Lee.