Erdős Problem 445

References:

• erdosproblems.com/445
• [He00] Heath-Brown, D. R., Arithmetic applications of {K}loosterman sums. Nieuw Arch. Wiskd. (5) (2000), 380--384.
• MathOverflow

def Erdos445.Erdos445Prop (c : ℝ) (p n : ℕ) : Prop

The property that there exist $a,b\in(n,n+p^c)$ such that $ab\equiv 1\pmod{p}$.

Equations

• Erdos445.Erdos445Prop c p n = ∃ (a : ℕ) (b : ℕ), n < a ∧ ↑a < ↑n + ↑p ^ c ∧ n < b ∧ ↑b < ↑n + ↑p ^ c ∧ a * b ≡ 1 [MOD p]

theorem Erdos445.erdos_445 : True ↔ ∀ c > 1 / 2, ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∀ (n : ℕ), Erdos445Prop c p n

Is it true that, for any $c>1/2$, if $p$ is a sufficiently large prime then, for any $n\geq 0$, there exist $a,b\in(n,n+p^c)$ such that $ab\equiv 1\pmod{p}$?

This is discussed in this MathOverflow question [MathOverflow].

theorem Erdos445.erdos_445.variants.heilbronn : ∃ c₀ < 1, ∀ c > c₀, ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∀ (n : ℕ), Erdos445Prop c p n

Heilbronn (unpublished) proved this for $c$ sufficiently close to $1$.

theorem Erdos445.erdos_445.variants.heath_brown (c : ℝ) : c > 3 / 4 → ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∀ (n : ℕ), Erdos445Prop c p n

Heath-Brown [He00] used Kloosterman sums to prove this for all $c>3/4$.

theorem Erdos445.erdos_445.test.small_example : Erdos445Prop 1 5 1

Small example: for $p=5$, $c=1$, $n=0$, the pair $(2,3) \in (0,5)$ satisfies $2 \cdot 3 = 6 \equiv 1 \pmod{5}$.