erdos_886_variants_rosenfeld_bound

Erdős and Rosenfeld [ErRo97] proved that, for any constant $C>0$, all large $n$ have at most $1+C^2$ many divisors in $[n^{1/2}, n^{1/2}+Cn^{1/4}]$.

theorem erdos_886_variants_rosenfeld_bound :
    ∀ C > 0, ∀ᶠ (n : ℕ) in atTop,
    ((divisors n).filter (fun (d : ℕ) =>
      (n : ℝ) ^ (1 / 2 : ℝ) ≤ (d : ℝ) ∧ (d : ℝ) ≤ (n : ℝ) ^ (1 / 2 : ℝ) + C * (n : ℝ) ^ (1 / 4 : ℝ))).card
      ≤ 1 + C ^ 2

Recent Submissions

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