Ramanujan tau function

DefinitionRamanujan τ-function#✓fully proved

For a natural number \(n\), \(\tau(n)\) is the complex number given by the coefficient of \(q^n\) in the \(q\)-expansion of the modular discriminant \(\Delta = \eta^{24}\), where \(\eta\) is the Dedekind eta function and \(q = e^{2\pi i z}\).

noncomputable def τ (n : ℕ) : ℂ := (qExpansion 1 discriminant).coeff n

Used by 2

Used byNormalisation of the Ramanujan τ-function · Ramanujan–Petersson conjecture for τ (Deligne's theorem)

TheoremNormalisation of the Ramanujan τ-function#✓fully proved

The Ramanujan τ-function satisfies \(\tau(1) = 1\): the coefficient of \(q\) in the \(q\)-expansion of the modular discriminant \(\Delta\) is \(1\).

theorem τ_one : τ 1 = 1

Uses 1

Statement usesRamanujan τ-function

TheoremRamanujan–Petersson conjecture for τ (Deligne's theorem)#●ready to prove

For every prime \(p\), the Ramanujan τ-function satisfies \(|\tau(p)| \le 2p^{11/2}\), where \(|\cdot|\) is the absolute value of a complex number.

public theorem_wanted ramanujan_petersson :
    ∀ p : ℕ, Prime p → ‖τ p‖ ≤ 2 * (p : ℝ) ^ ((11 : ℝ) / 2)

Sources

• 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. Problem ramanujan_petersson of the lean-eval benchmark.

Uses 1

Statement usesRamanujan τ-function

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.