Ramanujan-Petersson: rename to Ramanujan & update informal proof

LeanEval/NumberTheory/RamanujanTau.lean

@@ -6,14 +6,15 @@ namespace NumberTheory
 namespace RamanujanTauProblem
 
 /-!
-# The Ramanujan–Petersson conjecture for the τ-function (Deligne's theorem)
+# Ramanujan's conjecture for the τ-function (Deligne's theorem)
 
 The Ramanujan τ-function is defined by the Fourier expansion
 `Δ = ∑_{n ≥ 1} τ(n) qⁿ` of the modular discriminant
 `Δ(z) = η(z)²⁴ = q ∏_{n ≥ 1} (1 - qⁿ)²⁴`, the normalised cusp form of weight
 `12` and level `1`. Ramanujan (1916) conjectured that `|τ(p)| ≤ 2 p^(11/2)`
-for every prime `p`; Petersson generalised the conjecture to all cusp forms,
-and Deligne proved it in 1974 as a consequence of the Weil conjectures.
+for every prime `p`, and Deligne proved it in 1974 using his proof of the Weil
+conjectures. This bound is due to Ramanujan alone; the Ramanujan–Petersson
+conjecture is Petersson's generalisation to all cuspidal Hecke eigenforms.
 
 Here `τ n` is the `n`-th `q`-expansion coefficient of mathlib's
 `ModularForm.discriminant`. The coefficients are a priori complex, so the
@@ -29,8 +30,8 @@ noncomputable def τ (n : ℕ) : ℂ := (qExpansion 1 discriminant).coeff n
 /-- Normalisation check: `τ 1 = 1`. -/
 theorem τ_one : τ 1 = 1 := discriminant_qExpansion_coeff_one
 
-/-- **The Ramanujan–Petersson conjecture for `τ`** (Ramanujan 1916; proved by
-Deligne in 1974). For every prime `p`, `|τ(p)| ≤ 2 p^(11/2)`. -/
+/-- **Ramanujan's conjecture for `τ`** (Ramanujan 1916; proved by Deligne in
+1974). For every prime `p`, `|τ(p)| ≤ 2 p^(11/2)`. -/
 @[eval_problem]
 theorem ramanujan_petersson :
     ∀ p : ℕ, Prime p → ‖τ p‖ ≤ 2 * (p : ℝ) ^ ((11 : ℝ) / 2) := by

manifests/problems/ramanujan_petersson.toml

@@ -1,5 +1,5 @@
 id = "ramanujan_petersson"
-title = "Ramanujan–Petersson conjecture for the τ-function (Deligne's theorem)"
+title = "Ramanujan's conjecture for the τ-function (Deligne's theorem)"
 group = "formalization-evaluation"
 status = "active"
 visible = true
@@ -8,9 +8,9 @@ tags = []
 module = "LeanEval.NumberTheory.RamanujanTau"
 holes = ["ramanujan_petersson"]
 submitter = "Seewoo Lee"
-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)‖."
-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"
-informal_solution = "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)."
+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 (1971) used the Eichler–Shimura isomorphism to reduce the Ramanujan–Petersson conjecture to the Weil conjectures that he later proved (1974). The coefficients are a priori complex (integrality is classical but not needed to state the bound), so the statement bounds the complex norm ‖τ(p)‖."
+source = "S. Ramanujan, 'On certain arithmetical functions', Trans. Cambridge Philos. Soc. 22 (1916) 159–184. P. Deligne, 'Formes modulaires et représentations ℓ-adiques', Séminaire Bourbaki 1968/69, Exposé 355, Lecture Notes in Math. 179, Springer (1971) 139–172. P. Deligne, 'La conjecture de Weil. I', Publ. Math. IHÉS 43 (1974) 273–307. P. Deligne, 'La conjecture de Weil. II', Publ. Math. IHÉS 52 (1980) 137–252. E. Freitag and R. Kiehl, 'Étale Cohomology and the Weil Conjecture', Ergebnisse der Mathematik und ihrer Grenzgebiete (3) 13, Springer (1988). Background: https://en.wikipedia.org/wiki/Ramanujan_tau_function"
+informal_solution = "Deligne's proof. Δ is a normalised Hecke eigenform, so Tₚ Δ = τ(p) Δ. Fix N ≥ 4 prime to p and a prime ℓ ≠ p, let ℳ be the modular curve over ℤ[1/N] classifying elliptic curves with a point of order N (a fine moduli scheme), and let f : ℰ → ℳ be the universal elliptic curve. τ(p) does not come from the cohomology of ℰ itself: Hecke eigenvalues of forms of weight k appear in the cohomology of the base ℳ with coefficients in the lisse sheaf Symᵏ⁻² R¹f_*ℚ_ℓ, and through it in Hᵏ⁻¹ of the (k−2)-fold fibre power ℰ ×_ℳ ⋯ ×_ℳ ℰ. For Δ (k = 12) the sheaf is V = Sym¹⁰ R¹f_*ℚ_ℓ. Shimura's form of the Eichler–Shimura isomorphism identifies the parabolic cohomology H¹_!(ℳ(ℂ), Sym¹⁰ R¹f_*ℤ) ⊗ ℂ (the image of compactly supported cohomology in ordinary cohomology) with S₁₂(Γ₁(N)) ⊕ conj(S₁₂(Γ₁(N))), compatibly with the Hecke operators. By the comparison theorem the ℓ-adic group H¹_!(ℳ_Q̄, V) has the same Hecke eigenvalues, and it also carries an action of Gal(Q̄/ℚ) that is unramified at p. The Eichler–Shimura congruence relation Tₚ = Frobₚ + p¹¹⟨p⟩ Frobₚ⁻¹ then shows that on the non-zero Δ-isotypic part of H¹_!(ℳ_Q̄, V), on which ⟨p⟩ acts trivially, Frobenius at p satisfies X² − τ(p)X + p¹¹ = 0. So Frobenius has an eigenvalue α there that is a root of this polynomial, and with β = p¹¹/α we get τ(p) = α + β. Purity gives |α| = p^(11/2) for every complex embedding, in either of two ways: Deligne (Bourbaki 1969) realises H¹_!(ℳ_Q̄, V) as a direct summand of H¹¹ of a smooth projective compactification of the Kuga–Sato variety ℰ ×_ℳ ⋯ ×_ℳ ℰ (10 factors), which has good reduction at p, so Weil I (1974) applies; or Weil II (1980), applied to V, which is pure of weight 10, shows directly that H¹_! is pure of weight 11 without taking the fibre power, as in Freitag–Kiehl. Then |β| = p¹¹/|α| = p^(11/2), hence |τ(p)| = |α + β| ≤ 2 p^(11/2)."
 
 [[status_history]]
 status = "active"