Ramanujan τ-function

There are two conjectures related to the Ramanujan τ-function:

• Ramanujan-Petersson conjecture: For every prime p, the absolute value of the Ramanujan τ-function at p is bounded by 2 * p^(11/2).
• Lehmer's conjecture: The Ramanujan τ-function is never zero for any positive integer n.

References:

• Ramanujan-Petersson conjecture
• Lehmer's conjecture

noncomputable def RamanujanTau.Δ : PowerSeries ℤ

Equations

• RamanujanTau.Δ = PowerSeries.X * ∏' (n : ℕ+), (1 - PowerSeries.X ^ ↑n) ^ 24

noncomputable def RamanujanTau.τ (n : ℕ) : ℤ

Equations

• RamanujanTau.τ n = (PowerSeries.coeff ℤ n) RamanujanTau.Δ

theorem RamanujanTau.multipliable : Multipliable fun (n : ℕ+) => (1 - PowerSeries.X ^ ↑n) ^ 24

theorem RamanujanTau.τ_zero : τ 0 = 0

theorem RamanujanTau.τ_one : τ 1 = 1

theorem RamanujanTau.τ_two : τ 2 = -24

theorem RamanujanTau.ramanujan_petersson (p : ℕ) : Prime p → ↑|τ p| ≤ 2 * ↑p ^ (11 / 2)

theorem RamanujanTau.lehmer_ramanujan_tau (n : ℕ) : n > 0 → τ n ≠ 0