Erdős Problem 282

Reference: erdosproblems.com/282

noncomputable def Erdos282.greedyUnitFractionRem (A : Set ℕ) (x : ℚ) : ℕ → ℚ

Let $A\subseteq \mathbb{N}$ be an infinite set and consider the following greedy algorithm for a rational $x$: choose the minimal $n\in A$ such that $n\geq 1/x$ and repeat with $x$ replaced by $x-\frac{1}{n}$.

This process of subtracting unit fractions is modelled in greedyUnitFractionRem. At each step t : ℕ, the function greedyUnitFractionRem A x t returns the remainder of x with respect to the first t + 1 unit fractions, with denominators taken from A. If this process ever reaches 0 then it terminates. This corresponds to producing a representation of x as the sum of distinct unit fractions with denominators from A, however this function does not return this representation.

Equations

• One or more equations did not get rendered due to their size.
• Erdos282.greedyUnitFractionRem A x 0 = x - 1 / ↑(sInf {n : ℕ | n ∈ A ∧ 1 / x ≤ ↑n})

theorem Erdos282.greedyUnitFractionRem_zero (n : ℕ) : greedyUnitFractionRem Set.univ (1 / ↑n) 0 = 0

theorem Erdos282.greedyUnitFractionRem_one (n : ℕ) : greedyUnitFractionRem Set.univ (1 / ↑n) 1 = 0

theorem Erdos282.erdos_282 {x : ℚ} (hx : x ∈ Set.Ioo 0 1) (hx_den : Odd x.den) : greedyUnitFractionRem {n : ℕ | Odd n} x =ᶠ[Filter.atTop] 0

Let $A\subseteq \mathbb{N}$ be an infinite set and consider the following greedy algorithm for a rational $x\in (0,1)$: choose the minimal $n\in A$ such that $n\geq 1/x$ and repeat with $x$ replaced by $x-\frac{1}{n}$. If this terminates after finitely many steps then this produces a representation of $x$ as the sum of distinct unit fractions with denominators from $A$.

Does this process always terminate if $x$ has odd denominator and $A$ is the set of odd numbers?

theorem Erdos282.erdos_282.variants.general (x : ℚ) (A : Set ℕ) : greedyUnitFractionRem A x =ᶠ[Filter.atTop] 0 ↔ (x, A) ∈ sorry

More generally, for which pairs $x$ and $A$ does this process terminate?

theorem Erdos282.erdos_282.variants.fibonacci {x : ℚ} (hx : x ∈ Set.Ioo 0 1) : greedyUnitFractionRem Set.univ x =ᶠ[Filter.atTop] 0

In 1202 Fibonacci observed that this process terminates for any $x$ when $A=\mathbb{N}$.

theorem Erdos282.erdos_282.variants.graham {x : ℚ} (hx : x ∈ Set.Ioo 0 1) {a d : ℕ} (hd : 1 < d) (h : (x.den / x.den.gcd (a.gcd d)).gcd (d / a.gcd d) = 1) : greedyUnitFractionRem {n : ℕ | n ≡ a [MOD d]} x =ᶠ[Filter.atTop] 0 ↔ True

Graham has shown that $\frac{m}{n}$ is the sum of distinct unit fractions with denominators $\equiv a\pmod{d}$ if and only if $$\left(\frac{n}{(n,a,d)},\frac{d}{(a,d)}\right)=1.$$ Does the greedy algorithm always terminate in such cases?

theorem Erdos282.greedyUnitFractionRem_sq_one : greedyUnitFractionRem {n : ℕ | IsSquare n} 1 0 = 0

theorem Erdos282.erdos_282.variants.sq : True ↔ ∀ (x : ℚ), ↑x ∈ Set.Ico 0 (Real.pi ^ 2 / 6 - 1) ∪ Set.Ico 1 (Real.pi ^ 2 / 6) → greedyUnitFractionRem {n : ℕ | IsSquare n} x =ᶠ[Filter.atTop] 0

Graham has also shown that $x$ is the sum of distinct unit fractions with square denominators if and only if $x\in [0,\pi^2/6-1)\cup [1,\pi^2/6)$. Does the greedy algorithm for this always terminate? Erdős and Graham believe not - indeed, perhaps it fails to terminate almost always.