Erdős Problem 323

Reference: erdosproblems.com/323

noncomputable def Erdos323.f (k m x : ℕ) : ℕ

Let $1\leq m\leq k$ and $f_{k,m}(x)$ denote the number of integers $\leq x$ which are the sum of $m$ many nonnegative $k$th powers.

Equations

• Erdos323.f k m x = {n : ℕ | n ≤ x ∧ ∃ (v : Fin m → ℕ), n = ∑ i : Fin m, v i ^ k}.ncard

theorem Erdos323.erdos_323.parts.i : True ↔ ∀ k ≥ 1, ∀ ε > 0, (fun (x : ℕ) => ↑x ^ (1 - ε)) =O[Filter.atTop] fun (x : ℕ) => ↑(f k k x)

Is it true that $f_{k,k}(x) \gg_\epsilon x^{1-\epsilon}$ for all $\epsilon>0$?

This would have significant applications to Waring's problem. Erdős and Graham describe this as 'unattackable by the methods at our disposal'.

theorem Erdos323.erdos_323.parts.ii : True ↔ ∀ (k m : ℕ), 1 ≤ m → m < k → (fun (x : ℕ) => ↑x ^ (↑m / ↑k)) =O[Filter.atTop] fun (x : ℕ) => ↑(f k m x)

Is it true that if $m < k$ then $f_{k,m}(x) \gg x^{m/k}$ for sufficiently large $x$?

theorem Erdos323.erdos_323.variants.k_eq_2 : ∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun (x : ℕ) => ↑(f 2 2 x)) fun (x : ℕ) => c * ↑x / √(Real.log ↑x)

The case $k=2$ was resolved by Landau, who showed $f_{2,2}(x) \sim \frac{cx}{\sqrt{\log x}}$ for some constant $c>0$.

theorem Erdos323.erdos_323.variants.k_gt_2 : True ↔ ∀ k > 2, (fun (x : ℕ) => ↑(f k k x)) =o[Filter.atTop] fun (x : ℕ) => ↑x

For $k>2$ it is not known if $f_{k,k}(x)=o(x)$.