def Erdos1004.IsDistinctTotientRun (n K : ℕ) : Prop

IsDistinctTotientRun n K means that the values φ(n+1), φ(n+2), ..., φ(n+K) are all distinct.

Equations

• Erdos1004.IsDistinctTotientRun n K = Set.InjOn Nat.totient (Set.Icc (n + 1) (n + K))

theorem Erdos1004.erdos_1004 : sorry ↔ ∀ c > 0, ∀ᶠ (x : ℕ) in Filter.atTop, ∃ n ≤ x, IsDistinctTotientRun n ⌊Real.log ↑x ^ c⌋₊

For any fixed c > 0, if x is sufficiently large then there exists n ≤ x such that the values of φ(n+k) are all distinct for 1 ≤ k ≤ (log x)^c. This is an open problem.

theorem Erdos1004.erdos_1004.EPS87_theorem : True ↔ ∃ (c : ℝ) (_ : c > 0), ∀ (n K : ℕ), n > 0 → IsDistinctTotientRun n K → ↑K ≤ ↑n / Real.exp (c * Real.log ↑n ^ (1 / 3))

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.