erdos_1004.variants.le_of_isDistinctTotientRun

Erdős, Pomerance, and Sárközy [EPS87] proved that if φ(n+k) are all distinct for 1 ≤ k ≤ K then K ≤ n / exp(c (log n)^{1/3}) for some constant c > 0. Here we state the existence of such a constant c.

theorem erdos_1004.variants.le_of_isDistinctTotientRun :
    answer(True) ↔ ∃ (c : ℝ) (hc : c > 0),
      ∀ᶠ n in atTop, ∀ (K : ℕ), IsDistinctTotientRun n K →
        (K : ℝ) ≤ (n : ℝ) / Real.exp (c * (Real.log n) ^ (1/3 : ℝ))

Recent Submissions

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