Erdős Problem 890

Reference:

• erdosproblems.com/890
• [ErSe67] Erdős, P. and Selfridge, J. L., Some problems on the prime factors of consecutive integers. Illinois J. Math. (1967), 428--430.

def Erdos890.omegaGt (k n : ℕ) : ℕ

omegaGt k n counts the number of distinct prime factors of n that are strictly greater than k.

Equations

• Erdos890.omegaGt k n = {x ∈ n.primeFactors | x > k}.card

theorem Erdos890.erdos_890.parts.a : True ↔ ∀ k ≥ 1, Filter.liminf (fun (n : ℕ) => ∑ i ∈ Finset.range k, ↑(omegaGt k (n + i))) Filter.atTop ≤ ↑k

If $\omega_k(n)$ counts the number of distinct prime factors of $n$ which are $>k$, then is it true that, for every $k\geq 1$, $$\liminf_{n\to \infty}\sum_{0\leq i < k}\omega_k(n+i)\leq k?$$

theorem Erdos890.erdos_890.parts.b : True ↔ ∀ k ≥ 1, Filter.limsup (fun (n : ℕ) => (∑ i ∈ Finset.range k, ↑(ArithmeticFunction.cardDistinctFactors (n + i))) * (↑(Real.log (Real.log ↑n)) / ↑(Real.log ↑n))) Filter.atTop = 1

Is it true that $$\limsup_{n\to \infty}\left(\sum_{0\leq i < k}\omega(n+i)\right) \frac{\log\log n}{\log n}=1,$$ where $\omega$ counts the number of distinct prime factors without restriction?

theorem Erdos890.erdos_890.variants.liminf_lower_bound (k : ℕ) : Filter.liminf (fun (n : ℕ) => ∑ i ∈ Finset.range k, ↑(ArithmeticFunction.cardDistinctFactors (n + i))) Filter.atTop ≥ ↑k + ↑k.primeCounting - 1

A question of Erdős and Selfridge [ErSe67], who observe that $\liminf_{n\to \infty}\sum_{0\leq i < k}\omega(n+i)\geq k+\pi(k)-1$ for every $k$. This follows from Pólya's theorem that the set of $k$-smooth integers has unbounded gaps - indeed, $n(n+1)\cdots (n+k-1)$ is divisible by all primes $\leq k$ and, provided $n$ is large, all but at most one of $n,n+1,\ldots,n+k-1$ has a prime factor $>k$ by Pólya's theorem.

theorem Erdos890.erdos_890.variants.omega_limsup : Filter.limsup (fun (n : ℕ) => ↑(ArithmeticFunction.cardDistinctFactors n) * (↑(Real.log (Real.log ↑n)) / ↑(Real.log ↑n))) Filter.atTop = 1

It is a classical fact that $\limsup_{n\to \infty}\omega(n)\frac{\log\log n}{\log n}=1.$