Erdős Problem 459

References:

• erdosproblems.com/459
• [ErGr80] P. Erdős and R. L. Graham, Old and new problems and results in combinatorial number theory, Monographies de L'Enseignement Mathématique 28 (1980), p.91.
• OEIS A289280

noncomputable def Erdos459.f (u : ℕ) : ℕ

The function from the problem, in its equivalent form: f u is the smallest v > u all of whose prime factors divide u. (Equivalently, f u is the largest v such that no m ∈ (u, v) is composed entirely of primes dividing u * v.)

Equations

• Erdos459.f u = sInf {v : ℕ | u < v ∧ v.primeFactors ⊆ u.primeFactors}

theorem Erdos459.erdos_459 {u : ℕ} (hu : 2 ≤ u) : u + 2 ≤ f u ∧ f u ≤ u ^ 2

Let $f(u)$ be the largest $v$ such that no $m\in (u,v)$ is composed entirely of primes dividing $uv$. Estimate $f(u)$.

The estimate $u + 2 \le f(u) \le u^2$ holds for every $u \ge 2$. The upper bound is attained when $u$ is prime, and the lower bound when $u = 2^k - 2$ with $k \ge 2$; Cambie further showed that $f(n) = (1 + o(1))n$ for almost all $n$.

theorem Erdos459.erdos_459.variants.upper_tight {p : ℕ} (hp : Nat.Prime p) : f p = p ^ 2

The upper bound $f u ≤ u ^ 2$ is attained exactly when u is prime: $f p = p ^ 2$.