erdos_975.variant.quadratic

When $f$ is an irreducible quadratic polynomial, the question is answered first by Hooley [Ho63]. More compact expression of the constant in terms of Hurwitz class numbers (when $a = 1$) is given by McKey in [Mc95], [Mc97], [Mc99]. TODO: formalize Hurwitz class numbers and the expression of the constant in terms of them.

theorem erdos_975.variant.quadratic (f : ℤ[X]) (hf : Irreducible f)
    (hf_pos : ∀ᶠ n : ℕ in atTop, 1 ≤ f.eval ↑n) (hf_degree : f.degree = 2) (c : ℝ) :
    c = answer(sorry) → 0 < c ∧ Tendsto (fun x ↦ Erdos975Sum f x / (x * log x)) atTop (𝓝 c)

Recent Submissions

No submissions yet. Be the first to attempt this problem.