Hilbert's 17th problem

Let $f(x_1, \dots, x_n)$ be a multivariable polynomial with real coefficients that takes only nonnegative values for all real inputs. Hilbert's 17th problem asks whether there exist rational functions $g_1, \dots, g_m$ such that $f = g_1^2 + g_2^2 + \cdots + g_m^2$. Resolved affirmatively by Artin in 1927. References:

• Wikipedia
• Motzkin, "The arithmetic-geometric inequality". In Shisha, Oved (ed.). Inequalities. Academic Press. pp. 205–224.

@[reducible, inline]

abbrev Hilbert17.MvRatFunc (σ : Type u_1) (K : Type u_2) [CommRing K] : Type (max u_2 u_1)

Equations

• Hilbert17.MvRatFunc σ K = FractionRing (MvPolynomial σ K)

theorem Hilbert17.hilbert_17th_problem {n : ℕ} (hn : 0 < n) (f : MvPolynomial (Fin n) ℝ) (h : ∀ (x : Fin n → ℝ), 0 ≤ (MvPolynomial.eval x) f) : ∃ (m : ℕ) (g : Fin m → MvRatFunc (Fin n) ℝ), (algebraMap (MvPolynomial (Fin n) ℝ) (MvRatFunc (Fin n) ℝ)) f = ∑ i : Fin m, g i ^ 2

noncomputable def Hilbert17.f : MvPolynomial (Fin 2) ℝ

The statement is false in general if we restrict to polynomials. The polynomial (by Motzkin) $f(x, y) = x^4 y^2 + x^2 y^4 - 3 x^2 y^2 + 1$ takes only nonnegative values but cannot be written as a sum of squares of polynomials.

Equations

• Hilbert17.f = MvPolynomial.X 0 ^ 4 * MvPolynomial.X 1 ^ 2 + MvPolynomial.X 0 ^ 2 * MvPolynomial.X 1 ^ 4 - 3 * MvPolynomial.X 0 ^ 2 * MvPolynomial.X 1 ^ 2 + 1

theorem Hilbert17.f_nonneg (x y : ℝ) : 0 ≤ (MvPolynomial.eval ![x, y]) f

theorem Hilbert17.f_not_sum_of_squares : ¬∃ (n : ℕ) (_ : 0 < n) (S : Fin n → MvPolynomial (Fin 2) ℝ), f = ∑ i : Fin n, S i ^ 2

def Hilbert17.Hilbert17thProblemHomogenousPoly (n d : ℕ) : Prop

For the polynomial version, Hilbert showed that every nonnegative homogeneous polynomial in $n$ variables of degree $2d$ can be written as a sum of squares of polynomials if and only if

• $n = 1$
• $n = 2$
• $d = 1$
• $(n, d) = (3, 2)$.

Equations

• One or more equations did not get rendered due to their size.

theorem Hilbert17.Hilbert17thProblemHomogenousPoly_zero_left (d : ℕ) : Hilbert17thProblemHomogenousPoly 0 d

theorem Hilbert17.Hilbert17thProblemHomogenousPoly_zero_right (n : ℕ) : Hilbert17thProblemHomogenousPoly n 0

theorem Hilbert17.hilbert_17th_problem_poly {n d : ℕ} (hn : 0 < n) (hd : 0 < d) : Hilbert17thProblemHomogenousPoly n d ↔ n = 1 ∨ n = 2 ∨ d = 1 ∨ n = 3 ∧ d = 2