waring_polynomial_problem
Disprovedalgebrageometrygraph-theorynumber-theory
Waring problem for polynomials: Every homogeneous polynomial of degree k in d variables is a sum of k-th powers of linear forms. The minimum number of summands needed (the Waring rank) is not known in general.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem waring_polynomial_problem (k d : ℕ) (hk : 2 ≤ k) (hd : 1 ≤ d) :
∃ (s : ℕ), ∀ (f : MvPolynomial (Fin d) ℝ),
f.totalDegree = k →
∃ (forms : Fin s → MvPolynomial (Fin d) ℝ),
(∀ i, (forms i).totalDegree = 1) ∧
f = ∑ i, (forms i) ^ k := by
sorrySource