Erdős Problem 1054

Reference: erdosproblems.com/1054

noncomputable def Erdos1054.f (n : ℕ) : ℕ

Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest divisors of $m$ for some $k\geq 1$.

Equations

• Erdos1054.f n = if h : ∃ (m : ℕ), ∃ k ≥ 1, n = ∑ i ∈ Finset.Iio k, Nat.nth (fun (x : ℕ) => x ∈ m.divisors) i then Nat.find h else 0

theorem Erdos1054.erdos_1054.parts.i : ((fun (n : ℕ) => ↑(f n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) ↔ sorry

Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest divisors of $m$ for some $k\geq 1$. Is it true that $f(n)=o(n)$?

theorem Erdos1054.erdos_1054.parts.ii : (∃ (A : Set ℕ), A.HasDensity 1 ∧ (fun (n : ↑A) => ↑(f ↑n)) =o[Filter.atTop] fun (n : ↑A) => ↑↑n) ↔ sorry

Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest divisors of $m$ for some $k\geq 1$. Is it true that $f(n)=o(n)$ for almost all $n$?

theorem Erdos1054.erdos_1054.parts.iii : (∃ (A : Set ℕ), A.HasDensity 1 ∧ Filter.limsup (fun (n : ℕ) => ↑(f n) / ↑n = ⊤) Filter.atTop) ↔ sorry

Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest divisors of $m$ for some $k\geq 1$. Is it true that $\limsup f(n)/n=\infty$?

theorem Erdos1054.f_undefined_at_2 : f 2 = 0

Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest divisors of $m$ for some $k\geq 1$. Show that $f$ is undefined at $n=2$, i.e. we get the junk value $0$.

theorem Erdos1054.f_undefined_at_3 : f 5 = 0

Let $f(n)$ be the minimal integer $m$ such that $n$ is the sum of the $k$ smallest divisors of $m$ for some $k\geq 1$. Show that $f$ is undefined at $n=5$, i.e. we get the junk value $0$.