lang_trotter_conjecture
Disprovedl-functionsnumber-theory
Lang-Trotter conjecture (1976): For a fixed integer a and Weil-bounded sequence τ(p), the number of primes p ≤ x with τ(p) = a grows like C·√x/log x. Proved on average over curves; individual cases open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem lang_trotter_conjecture (a b : ℤ) (hdisc : 4 * a ^ 3 + 27 * b ^ 2 ≠ 0)
(tau : ℕ → ℤ) (htau : ∀ p : ℕ, Nat.Prime p → |tau p| ≤ 2 * Nat.sqrt p)
(target : ℤ) :
∃ (C : ℝ), 0 < C ∧
Filter.Tendsto (fun x : ℝ =>
(∑ p ∈ (Finset.range (Nat.floor x)).filter Nat.Prime,
if tau p = target then (1 : ℝ) else 0) /
(Real.sqrt x / Real.log x))
Filter.atTop (nhds C) := by
sorrySource