erdos_920.variants.lower_bound

A positive answer to this question would follow from [erdosproblems.com/986]. The known bounds for that problem imply $f_k(n) \gg \frac{n^{1-\frac{2}{k+1}}}{(\log n)^{c_k}}.$

theorem erdos_920.variants.lower_bound (k : ℕ) (hk : k ≥ 3) :
    ∃ c > 0, (fun n ↦ f k n) ≫ (fun (n : ℕ) ↦
    (n : ℝ) ^ (1 - 2 / ((k : ℝ) + 1)) / (log n) ^ c)

Recent Submissions

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