erdos_394_lower_bound

Since $t_2(p)=p-1$ for prime $p$ it is trivial that $\sum_{n\leq x}t_2(n)\gg \frac{x^2}{\log x}$.

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

Recent Submissions

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