Erdős Problem 325

Reference: erdosproblems.com/325

def Erdos325.IsSumThreePower (k n : ℕ) : Prop

A predicate for $n$ to be the sum of three $k$th powers.

Equations

• Erdos325.IsSumThreePower k n = ∃ (a : ℕ) (b : ℕ) (c : ℕ), a ^ k + b ^ k + c ^ k = n

noncomputable def Erdos325.cardIsSumThreePowerBelow (k x : ℕ) : ℕ

The number of integers $\leq x$ which are the sum of three $k$th powers.

Equations

• Erdos325.cardIsSumThreePowerBelow k x = {n : ℕ | n ∈ Set.Iic x ∧ Erdos325.IsSumThreePower k n}.ncard

theorem Erdos325.erdos_325 : (∀ (k : ℕ), 3 ≤ k → (fun (x : ℕ) => ↑x ^ (3 / ↑k)) =O[Filter.atTop] fun (x : ℕ) => ↑(cardIsSumThreePowerBelow k x)) ↔ sorry

Writing $f_{k, 3}(x)$ for the number of integers $\leq x$ which are the sum of three $k$th powers, is it true that $f_{k, 3}(x) \gg x ^ (3 / k)$?

theorem Erdos325.erdos_325.variants.weaker : (∀ ε > 0, ∀ (k : ℕ), 3 ≤ k → (fun (x : ℕ) => ↑x ^ (3 / ↑k - ε)) =O[Filter.atTop] fun (x : ℕ) => ↑(cardIsSumThreePowerBelow k x)) ↔ sorry

Writing $f_{k, 3}(x)$ for the number of integers $\leq x$ which are the sum of three $k$th powers, is it even true that $f_{k, 3}(x) \gg_\epsilon x ^ (3 / k - \epsilon)$?

theorem Erdos325.erdos_325.variants.wooley : (fun (x : ℕ) => ↑x ^ 0.917) =O[Filter.atTop] fun (x : ℕ) => ↑(cardIsSumThreePowerBelow 3 x)

For $k = 3$, the best known is due to Wooley [Wo15] [Wo15] Wooley, Trevor D., Sums of three cubes, II. Acta Arith. (2015), 73-100.