Erdős Problem 304

Reference: erdosproblems.com/304

def unitFractionExpressible (a b : ℕ) : Set ℕ

The set of k for which a / b can be expressed as a sum of k distinct unit fractions.

Equations

• unitFractionExpressible a b = {k : ℕ | ∃ (s : Finset ℕ), s.card = k ∧ (∀ n ∈ s, n > 1) ∧ ↑a / ↑b = ∑ n ∈ s, (↑n)⁻¹}

@[simp]

theorem zero_mem_unitFractionExpressible_iff {a b : ℕ} : 0 ∈ unitFractionExpressible a b ↔ a = 0 ∨ b = 0

theorem unitFractionExpressible_of_zero {a b : ℕ} (h : a = 0 ∨ b = 0) : unitFractionExpressible a b = {0}

theorem unitFractionExpressible_zero_left {b : ℕ} : unitFractionExpressible 0 b = {0}

theorem unitFractionExpressible_zero_right {a : ℕ} : unitFractionExpressible a 0 = {0}

theorem zero_notMem_unitFractionExpressible {a b : ℕ} : 0 ∉ unitFractionExpressible a b ↔ a ≠ 0 ∧ b ≠ 0

theorem eq_inv_of_one_mem_unitFractionExpressible {a b : ℕ} (h : 1 ∈ unitFractionExpressible a b) : ∃ (m : ℕ), 1 < m ∧ ↑a / ↑b = (↑m)⁻¹

theorem dvd_of_one_mem_unitFractionExpressible {a b : ℕ} (h : 1 ∈ unitFractionExpressible a b) : a ∣ b

noncomputable def smallestCollection (a b : ℕ) : ℕ

Let $$N(a, b)$$, denoted here by smallestCollection a b be the minimal k such that there exist integers $1 < n_1 < n_2 < ... < n_k$ with $$\frac{a}{b} = \sum_{i=1}^k \frac{1}{n_i}$$

Equations

• smallestCollection a b = sInf (unitFractionExpressible a b)

theorem smallestCollection_pos {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : (unitFractionExpressible a b).Nonempty) : 0 < smallestCollection a b

theorem smallestCollection_left_one (b : ℕ) (hb : 1 < b) : smallestCollection 1 b = 1

theorem eq_one_of_smallestCollection_eq_one {a b : ℕ} (h : smallestCollection a b = 1) : ∃ (m : ℕ), 1 < m ∧ ↑a / ↑b = (↑m)⁻¹

theorem dvd_of_smallestCollection_eq_one {a b : ℕ} (h : smallestCollection a b = 1) : a ∣ b

theorem smallestCollection_two_fifteen : smallestCollection 2 15 = 2

noncomputable def smallestCollectionTo (b : ℕ) : ℕ

Write $$N(b) = max_{1 \leq a < b} N(a, b)$$.

Equations

• smallestCollectionTo b = sSup {x : ℕ | ∃ a ∈ Finset.Ico 1 b, smallestCollection a b = x}

theorem erdos_304.variants.upper_1950 : (fun (b : ℕ) => ↑(smallestCollectionTo b)) =O[Filter.atTop] fun (b : ℕ) => Real.log ↑b / Real.log (Real.log ↑b)

In 1950, Erdős [Er50c] proved the upper bound $$N(b) \ll \log b / \log \log b$$. [Er50c] Erdős, P., Az ${1}/{x_1} + {1}/{x_2} + \ldots + {1}/{x_n} =A/B$ egyenlet eg'{E}sz sz'{A}m'{u} megold'{A}sairól. Mat. Lapok (1950), 192-210.

theorem erdos_304.variants.lower_1950 : (fun (b : ℕ) => Real.log (Real.log ↑b)) =O[Filter.atTop] fun (b : ℕ) => ↑(smallestCollectionTo b)

In 1950, Erdős [Er50c] proved the lower bound $$\log \log b \ll N(b)$$. [Er50c] Erdős, P., Az ${1}/{x_1} + {1}/{x_2} + \ldots + {1}/{x_n} =A/B$ egyenlet eg'{E}sz sz'{A}m'{u} megold'{A}sairól. Mat. Lapok (1950), 192-210.

theorem erdos_304.variants.upper_1985 : (fun (b : ℕ) => ↑(smallestCollectionTo b)) =O[Filter.atTop] fun (b : ℕ) => √(Real.log ↑b)

In 1985 Vose [Vo85] proved the upper bound $$N(b) \ll \sqrt{\log b}$$. [Vo85] Vose, Michael D., Egyptian fractions. Bull. London Math. Soc. (1985), 21-24.

theorem upper_bound : ((fun (b : ℕ) => ↑(smallestCollectionTo b)) =O[Filter.atTop] fun (b : ℕ) => Real.log (Real.log ↑b)) ↔ sorry

Is it true that $$N(b) \ll \log \log b$$?