Erdős Problem 18

Reference:

• erdosproblems.com/18
• [ErGr80] Erdős, P. and Graham, R. L. (1980). Old and New Problems and Results in Combinatorial Number Theory. Monographies de L'Enseignement Mathématique, 28. Université de Genève. (See the sections on Egyptian fractions or practical numbers).
• [Vo85] Vose, Michael D., Egyptian fractions. Bull. London Math. Soc. (1985), 21-24.

noncomputable def Erdos18.practicalH (n : ℕ) : ℕ

For a practical number $n$, $h(n)$ is the maximum over all $1 ≤ m ≤ n$ of the minimum number of divisors of $n$ needed to represent $m$ as a sum of distinct divisors.

Equations

• Erdos18.practicalH n = (Finset.Icc 1 n).sup fun (m : ℕ) => sInf {k : ℕ | ∃ D ⊆ n.divisors, D.card = k ∧ m ∈ subsetSums ↑D}

theorem Erdos18.practicalH_one : practicalH 1 = 1

$h(1) = 1$: we need the single divisor {1} to represent 1.

theorem Erdos18.practicalH_two : practicalH 2 = 1

$h(2) = 1$: divisors are {1, 2}, each of m=1,2 needs only 1 divisor.

theorem Erdos18.practicalH_six : practicalH 6 = 2

$h(6) = 2$: divisors are {1, 2, 3, 6}. The hardest m to represent is m=4 or m=5, each requiring 2 divisors: 4=1+3, 5=2+3.

theorem Erdos18.practicalH_twelve : practicalH 12 = 3

$h(12) = 3$: divisors are {1, 2, 3, 4, 6, 12}. The hardest m is m=11, requiring 3 divisors: 11=1+4+6.

theorem Erdos18.practicalH_le_divisors (n : ℕ) (hn : n.IsPractical) : practicalH n ≤ n.divisors.card

For any practical number $n$, $h(n) ≤ number of divisors of $n$.

theorem Erdos18.factorial_isPractical (n : ℕ) : n.factorial.IsPractical

$h(n!)$ is well-defined since $n!$ is practical for $n ≥ 1$.

theorem Erdos18.erdos_18a : True ↔ ∃ (C : ℝ), 0 < C ∧ ∃ᶠ (m : ℕ) in Filter.atTop, m.IsPractical ∧ ↑(practicalH m) < Real.log (Real.log ↑m) ^ C

Conjecture 1. Are there infinitely many practical numbers $m$ such that $h(m) < (\log \log m)^{O(1)}$?

More precisely: does there exist a constant $C > 0$ such that for infinitely many practical numbers $m$, we have $h(m) < (\log \log m)^C$?

theorem Erdos18.erdos_18b : True ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ↑(practicalH n.factorial) < ↑n ^ ε

Conjecture 2. Is it true that $h(n!) < n^{o(1)}$? That is, for all $\varepsilon > 0$, is $h(n!) < n^\varepsilon$ for sufficiently large $n$?

theorem Erdos18.erdos_18c : True ↔ ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(practicalH n.factorial) < Real.log ↑n ^ C

Conjecture 3. Or perhaps even $h(n!) < (\log n)^{O(1)}$?

Erdős offered $250 for a proof or disproof.

theorem Erdos18.erdos_18_upper_bound : ∀ᶠ (n : ℕ) in Filter.atTop, practicalH n.factorial < n

Erdős's Theorem. Erdős proved that $h(n!) < n$ for all $n \ge 1$.

theorem Erdos18.erdos_18_vose : ∃ (C : ℝ), 0 < C ∧ ∃ᶠ (m : ℕ) in Filter.atTop, m.IsPractical ∧ ↑(practicalH m) < C * Real.log ↑m ^ (1 / 2)

Vose's Theorem. Vose proved the existence of infinitely many practical numbers $m$ such that $h(m) \ll (\log m)^{1/2}$. This gives a positive answer to a weaker form of Conjecture 1.