Erdős Problem 413

References:

• erdosproblems.com/413
• OEIS A005236

Erdős called a natural number n a barrier for ω, the number of distinct prime divisors, if m + ω(m) ≤ n for all m < n. He believed there should be infinitely many such barriers, and even posed a relaxed variant asking whether there is some ε > 0 for which infinitely many n satisfy m + ε · ω(m) ≤ n for every m < n.

def Erdos413.IsBarrier (f : ℕ → ℝ) (n : ℕ) : Prop

IsBarrier f n means n is a barrier for the real-valued function f, i.e. (m : ℝ) + f m ≤ (n : ℝ) for all m < n.

Equations

• Erdos413.IsBarrier f n = ∀ m < n, ↑m + f m ≤ ↑n

theorem Erdos413.erdos_413 : sorry ↔ {n : ℕ | IsBarrier (fun (m : ℕ) => ↑(ArithmeticFunction.cardDistinctFactors m)) n}.Infinite

Are there infinitely many barriers for ω?

def Erdos413.expProd (n : ℕ) : ℕ

expProd n is ∏ kᵢ when n = ∏ pᵢ ^ kᵢ, i.e. the product of the prime exponents of n.

Equations

• Erdos413.expProd n = n.factorization.prod fun (x e : ℕ) => e

theorem Erdos413.erdos_413_hasPosDensity_barrier_expProd : {n : ℕ | IsBarrier (fun (m : ℕ) => ↑(expProd m)) n}.HasPosDensity

Erdős proved that the barrier set for expProd is infinite and even has positive density.

theorem Erdos413.erdos_413_bigOmega : sorry ↔ {n : ℕ | IsBarrier (fun (m : ℕ) => ↑(ArithmeticFunction.cardFactors m)) n}.Infinite

Erdős believed there should be infinitely many barriers for Ω, the total prime multiplicity.

theorem Erdos413.erdos_413_bigOmega_largest_barrier_lt_100k : IsGreatest {n : ℕ | n < 10 ^ 5 ∧ IsBarrier (fun (m : ℕ) => ↑(ArithmeticFunction.cardFactors m)) n} 99840

Selfridge computed that the largest Ω-barrier below 10^5 is 99840.

theorem Erdos413.erdos_413_epsilon : sorry ↔ ∃ ε > 0, {n : ℕ | IsBarrier (fun (n : ℕ) => ε * ↑(ArithmeticFunction.cardDistinctFactors n)) n}.Infinite

Does there exist some ε > 0 such that there are infinitely many ε-barriers for ω?