Erdős Problem 968

Let uₙ = pₙ / n, where pₙ is the nth prime. Does the set of n such that uₙ < uₙ₊₁ have positive density?

Erdős and Prachar also proved that ∑_{pₙ < x} |uₙ₊₁ - uₙ| ≍ (log x)^2, and that the set of n such that uₙ > uₙ₊₁ has positive density. Erdős also asked whether there are infinitely many increasing triples uₙ < uₙ₊₁ < uₙ₊₂ or decreasing triples uₙ > uₙ₊₁ > uₙ₊₂.

Reference: erdosproblems.com/968

[ErPr61] Erdős, P. and Prachar, K., Sätze und Probleme über pₖ/k. Abh. Math. Sem. Univ. Hamburg (1961/62), 251–256.

noncomputable def Erdos968.u (n : ℕ) : ℝ

u n is the normalized nth prime, defined as pₙ / (n+1) where pₙ is the nth prime (with 0.nth Nat.Prime = 2).

This corresponds to the classical sequence (p₁/1, p₂/2, p₃/3, ...) while using Nat.nth Prime's 0-based indexing; in particular, the denominator is always positive.

Equations

• Erdos968.u n = ↑(Nat.nth Nat.Prime n) / (↑n + 1)

theorem Erdos968.erdos_968 : sorry ↔ {n : ℕ | u n < u (n + 1)}.HasPosDensity

Does the set {n | u n < u (n+1)} have positive natural density?

theorem Erdos968.erdos_968.variants.sum_abs_diff_isTheta_log_sq : (fun (x : ℕ) => ∑ n ∈ Finset.Iio x.primeCounting', |u (n + 1) - u n|) =Θ[Filter.atTop] fun (x : ℕ) => Real.log ↑x ^ 2

Erdős and Prachar proved ∑_{pₙ < x} |u (n+1) - u n| ≍ (log x)^2 (see [ErPr61]).

We encode ∑_{pₙ < x} as a sum over n < Nat.primeCounting' x (the number of primes < x).

theorem Erdos968.erdos_968.variants.decreasingSteps_hasPosDensity : {n : ℕ | u n > u (n + 1)}.HasPosDensity

Erdős and Prachar proved that the set {n | u n > u (n+1)} has positive natural density (see [ErPr61]).

theorem Erdos968.erdos_968.variants.infinite_increasingTriples : sorry ↔ {n : ℕ | u n < u (n + 1) ∧ u (n + 1) < u (n + 2)}.Infinite

Erdős asked whether there are infinitely many solutions to uₙ < uₙ₊₁ < uₙ₊₂.

theorem Erdos968.erdos_968.variants.infinite_decreasingTriples : sorry ↔ {n : ℕ | u n > u (n + 1) ∧ u (n + 1) > u (n + 2)}.Infinite

Erdős asked whether there are infinitely many solutions to uₙ > uₙ₊₁ > uₙ₊₂.