Linnik's theorem (L = 5.5)

linnik

Submitter: Bolton Bailey/Project Numina.

Notes: Linnik's theorem with the explicit constant `L = 5.5` due to Heath-Brown (1992): for `a` coprime to `d` with `0 < a < d`, the least prime `p(a, d)` in the progression `a mod d` satisfies `p(a, d) ≤ c · d ^ 5.5` for some absolute constant `c`.

Source: Heath-Brown, D.R. (1992), Zero-Free Regions for Dirichlet L-Functions, and the Least Prime in an Arithmetic Progression. Proceedings of the London Mathematical Society, s3-64: 265-338. https://doi.org/10.1112/plms/s3-64.2.265

Informal solution: Heath-Brown's proof rests on three principles: a quantitative zero-free region for Dirichlet L-functions, the Deuring-Heilbronn phenomenon, and the log-free zero-density estimate. Heath-Brown combines strong versions of these estimates to obtain an exponent of 5.5.

theorem declaration uses `sorry`linnik : ∃ c : ℝ, ∀ ⦃a d : ℕ⦄,
    0 < a → a < d → a.Coprime d → p a d ≤ c * d ^ (5.5 : ℝ) := by⊢ ∃ c, ∀ ⦃a d : ℕ⦄, 0 < a → a < d → a.Coprime d → ↑(p a d) ≤ c * ↑d ^ 5.5
  sorryAll goals completed! 🐙

Solved by

Not yet solved.