Erdős Problem 975

References:

• erdosproblems.com/975
• [Va39] van der Corput, J. G., Une in'egalit'e{} relative au nombre des diviseurs. Nederl. Akad. Wetensch., Proc. (1939), 547--553.
• [Er52b] Erd"os, P., On the sum {$\sum^x_{k=1} d(f(k))$}. J. London Math. Soc. (1952), 7--15.
• [Ho63] Hooley, Christopher, On the number of divisors of a quadratic polynomial. Acta Math. (1963), 97--114.
• [Mc95] McKee, James, On the average number of divisors of quadratic polynomials. Math. Proc. Cambridge Philos. Soc. (1995), 389--392.
• [Mc97] McKee, James, A note on the number of divisors of quadratic polynomials. (1997), 275--281.
• [Mc99] McKee, James, The average number of divisors of an irreducible quadratic polynomial. Math. Proc. Cambridge Philos. Soc. (1999), 17--22.
• [T] T. Tao, Erdos' divisor bound, https://terrytao.wordpress.com/2011/07/23/erdos-divisor-bound/

noncomputable def Erdos975.Erdos975Sum (f : Polynomial ℤ) (x : ℝ) : ℝ

Sum of $\tau(f(n))$ from 0 to ⌊x⌋ for a polynomial $f \in \mathbb{Z}[X]$.

Here $\tau$ is the divisor counting function, which is σ 0 in mathlib. Also, for simplicity, we use Nat.floor to convert rational values to natural numbers, instead of dealing with negative values.

Equations

• Erdos975.Erdos975Sum f x = ∑ n ∈ Finset.Iic ⌊x⌋₊, ↑((ArithmeticFunction.sigma 0) ⌊Polynomial.eval (↑n) f⌋₊)

theorem Erdos975.erdos_975 : sorry ↔ ∀ (f : Polynomial ℤ), f.natDegree ≠ 0 → Irreducible f → (∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) → ∃ c > 0, Filter.Tendsto (fun (x : ℝ) => Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)

For an irreducible polynomial $f \in \mathbb{Z}[x]$ with $f(n) \ge 1$ for sufficiently large $n$, does there exists a constant $c = c(f) > 0$ such that $\sum_{n \le x} \tau(f(n)) \approx c \cdot x \log x$?

Note that it is unclear whether the polynomial should have integer coefficients or merely be integer-valued. We assume the former.

theorem Erdos975.erdos_975.variant.upper_bound (f : Polynomial ℤ) (hf : Irreducible f) (hf_pos : ∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) : Erdos975Sum f =O[Filter.atTop] fun (x : ℝ) => x * Real.log x

The correctness of the growth rate is shown in [Va39] (lower bound) and [Er52b] (upper bound).

theorem Erdos975.erdos_975.variant.lower_bound (f : Polynomial ℤ) (hf : Irreducible f) (hfdeg : f.natDegree ≠ 0) (hf_pos : ∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) : (fun (x : ℝ) => x * Real.log x) =O[Filter.atTop] Erdos975Sum f

theorem Erdos975.erdos_975.variant.quadratic (f : Polynomial ℤ) (hf : Irreducible f) (hf_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ Polynomial.eval (↑n) f) (hf_degree : f.degree = 2) (c : ℝ) : c = sorry → 0 < c ∧ Filter.Tendsto (fun (x : ℝ) => Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)

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 Erdos975.erdos_975.variant.n2_plus_1_strong : (fun (x : ℝ) => Erdos975Sum (Polynomial.X ^ 2 + 1) x - 3 / Real.pi * x * Real.log x) =O[Filter.atTop] id

More concrete example for $f(n) = n^2 + 1$, where the asymptote is $\sum_{n \le x} \tau(n^2 + 1) \sim \frac{3}{\pi} x \log x + O(x)$. See Tao's blog [T].

theorem Erdos975.erdos_975.variant.n2_plus_1 : ∃ c > 0, Filter.Tendsto (fun (x : ℝ) => Erdos975Sum (Polynomial.X ^ 2 + 1) x / (x * Real.log x)) Filter.atTop (nhds c)