Erdős Problem 971

Reference: erdosproblems.com/971

noncomputable def Erdos971.leastCongruentPrime (a d : ℕ) : ℕ

leastCongruentPrime a d is the least prime congruent to a modulo d.

Equations

• Erdos971.leastCongruentPrime a d = sInf {p : ℕ | Nat.Prime p ∧ p ≡ a [MOD d]}

theorem Erdos971.erdos_971 : sorry ↔ ∃ c > 0, ∃ C > 0, ∀ᶠ (d : ℕ) in Filter.atTop, C * ↑d.totient ≤ ↑{a ∈ Finset.Iio d | a.Coprime d ∧ ↑(leastCongruentPrime a d) > (1 + c) * ↑d.totient * Real.log ↑d}.card

Let p(a, d) be the least prime congruent to a (mod d). Does there exist a constant c > 0 such that for all large d, p(a, d) > (1 + c) * φ(d) * log d for ≫ φ(d) many values of a?

theorem Erdos971.erdos_971.variants.infinite_sequence : ∃ c > 0, ∃ C > 0, {d : ℕ | C * ↑d.totient ≤ ↑{a ∈ Finset.Iio d | a.Coprime d ∧ ↑(leastCongruentPrime a d) > (1 + c) * ↑d.totient * Real.log ↑d}.card}.Infinite

Erdős [Er49c] proved that the statement in erdos_971 holds for infinitely many values of d.

[Er49c] Erdős, P., On some applications of Brun's method. Acta Univ. Szeged. Sect. Sci. Math. (1949), 57--63.

theorem Erdos971.erdos_971.variants.many_small (ε : ℝ) : ε > 0 → ∃ C > 0, ∀ᶠ (d : ℕ) in Filter.atTop, C * ↑d.totient ≤ ↑{a ∈ Finset.Iio d | a.Coprime d ∧ ↑(leastCongruentPrime a d) < ε * ↑d.totient * Real.log ↑d}.card

Erdős [Er49c] proved that for any ε > 0 we have p(a, d) < ε * φ(d) * log d for ≫_ε φ(d) many values of a (for all large d).

[Er49c] Erdős, P., On some applications of Brun's method. Acta Univ. Szeged. Sect. Sci. Math. (1949), 57--63.