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 Δ : PowerSeries ℤ

Equations

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

noncomputable def τ (n : ℕ) : ℤ

Equations

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

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

theorem τ_zero : τ 0 = 0

theorem τ_one : τ 1 = 1

theorem τ_two : τ 2 = -24

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

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