Erdős Problem 400

Reference: erdosproblems.com/400

noncomputable def Erdos400.g (k n : ℕ) : ℕ

For any $k\geq 2$ let $g_k(n)$ denote the maximum value of $(a_1+\cdots+a_k)-n$ where $a_1,\ldots,a_k$ are integers such that $a_1!\cdots a_k! \mid n!$.

Equations

• Erdos400.g k n = sSup {x : ℕ | ∃ (a : Fin k → ℕ) (_ : ∏ i : Fin k, (a i).factorial ∣ n.factorial), ∑ i : Fin k, a i - n = x}

theorem Erdos400.erdos_400.parts.i : True ↔ ∀ k ≥ 2, ∃ (c : ℝ), Asymptotics.IsEquivalent Filter.atTop (fun (x : ℕ) => ∑ n ∈ Finset.Icc 1 x, ↑(g k n)) fun (x : ℕ) => c * ↑x * Real.log ↑x

Can one show that $\sum_{n\leq x}g_k(n) \sim c_k x\log x$ for some constant $c_k$?

theorem Erdos400.erdos_400.parts.ii : True ↔ ∀ k ≥ 2, ∃ (c : ℝ), ∀ ε > 0, Filter.Tendsto (fun (x : ℕ) => ↑{n ∈ Finset.Icc 1 x | |↑(g k n) - c * Real.log ↑x| ≤ ε * Real.log ↑x}.card / ↑x) Filter.atTop (nhds 1)

Is it true that there is a constant $c_k$ such that for almost all $n < x$ we have $g_k(n)=c_k\log x+o(\log x)$?

theorem Erdos400.erdos_400.variants.upper_bound (k : ℕ) (hk : k ≥ 2) : (fun (n : ℕ) => ↑(g k n)) =O[Filter.atTop] fun (n : ℕ) => Real.log ↑n

Erdős and Graham write that it is easy to show that $g_k(n) \ll_k \log n$ always, but the best possible constant is unknown.

theorem Erdos400.erdos_400.variants.g_pos (k n : ℕ) (h : k ≥ 2) : 0 < g k n

For $k \ge 2$, $g_k(n) > 0$. We show this by choosing $a = (n, 1, 0, \ldots, 0)$.