erdos_394_hall_bound

In [ErGr80] they mention a conjecture of Erdős that the sum is $o(x^2)$. This was proved by Erdős and Hall [ErHa78], who proved that in fact $\sum_{n\leq x}t_2(n)\ll \frac{\log\log\log x}{\log\log x}x^2.$

theorem erdos_394_hall_bound :
    (fun x ↦ ∑ n ∈ Icc 1 ⌊x⌋₊, (t 2 n : ℝ)) ≪
    (fun x ↦ x ^ 2 * (Real.log (Real.log (Real.log x)) / Real.log (Real.log x)))

Recent Submissions

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