Erdős Problem 295

Reference: erdosproblems.com/295

theorem Erdos295.exists_k (N : ℕ) : ∃ (k : ℕ) (n : Fin k.succ → ℕ), (∀ (i : Fin k.succ), N ≤ n i) ∧ StrictMono n ∧ ∑ i : Fin k.succ, 1 / ↑(n i) = 1

Helper lemma: for each $N$, there exists $k$ and $n_1 < ... < n_k$ such that $N ≤ n_1 < ⋯ < n_k$ with $\frac 1 {n_1} + ... + \frac 1 {n_k} = 1$.

theorem Erdos295.erdos_295 : Filter.Tendsto (fun (N : ℕ) => ↑(Erdos295.k✝ N) - (Real.exp 1 - 1) * ↑N) Filter.atTop Filter.atTop ↔ sorry

Let $k(N)$ denote the smallest $k$ such that there exists $N ≤ n_1 < ⋯ < n_k$ with $\frac 1 {n_1} + ... + \frac 1 {n_k} = 1$

Is it true that $\lim_{N→∞} k(N) - (e - 1)N = ∞$?

theorem Erdos295.erdos_295.variants.erdos_straus : ∃ C > 0, ∃ O > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos295.k✝ N) - (Real.exp 1 - 1) * ↑N ∈ Set.Ioc (-C) (O * ↑N / Real.log ↑N)

Erdős and Straus have proved the existence of some constant $c>0$ such that $-c < k(N)-(e-1)N ≪ \frac N {log N}$