erdos_89.variants.n_dvd_log_n

Guth and Katz [GuKa15] proved that there are always $\gg \frac{n}{\log n}$ many distinct distances. [GuKa15] Guth, Larry and Katz, Nets Hawk, On the Erdős distinct distances problem in the plane. Ann. of Math. (2) (2015), 155-190.

theorem erdos_89.variants.n_dvd_log_n :
    (fun (n : ℕ) => n/(n : ℝ).log) =O[atTop] (fun n => (minimalDistinctDistances n : ℝ))

Recent Submissions

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