/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilHilbert'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:
Motzkin, "The arithmetic-geometric inequality". In Shisha, Oved (ed.). Inequalities. Academic Press. pp. 205–224.
open Real MvPolynomialnamespace Hilbert17Hilbert's 17th problem: every non-negative multivariate polynomial is a sum of squares of rational functions.
@[category research solved, AMS 12]
theorem hilbert_17th_problem {n : ℕ} (hn : 0 < n) (f : MvPolynomial (Fin n) ℝ)
(h : ∀ x : Fin n → ℝ, 0 ≤ f.eval x) :
∃ (m : ℕ) (g : Fin m → MvRatFunc (Fin n) ℝ), algebraMap _ _ f = ∑ i, (g i) ^ 2 := n:ℕhn:0 < nf:MvPolynomial (Fin n) ℝh:∀ (x : Fin n → ℝ), 0 ≤ (eval x) f⊢ ∃ m g, (algebraMap (MvPolynomial (Fin n) ℝ) (MvRatFunc (Fin n) ℝ)) f = ∑ i, g i ^ 2
All goals completed! 🐙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.
noncomputable def f : MvPolynomial (Fin 2) ℝ :=
X 0 ^ 4 * X 1 ^ 2 + X 0 ^ 2 * X 1 ^ 4 - 3 * X 0 ^ 2 * X 1 ^ 2 + 1The Motzkin polynomial is non-negative everywhere.
x:ℝy:ℝhx:¬x = 0h:0 < (x ^ 2 + y ^ 2) ^ 2H:0 ≤ (x ^ 3 * y + x * y ^ 3 - 2 * x * y) ^ 2 * (1 + x ^ 2 + y ^ 2) + (x ^ 2 - y ^ 2) ^ 2⊢ 0 ≤ (x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1) * (x ^ 2 + y ^ 2) ^ 2
All goals completed! 🐙The Motzkin polynomial cannot be written as a sum of squares of polynomials.
@[category textbook, AMS 12]
theorem f_not_sum_of_squares :
¬∃ (n : ℕ) (hn : 0 < n) (S : Fin n → MvPolynomial (Fin 2) ℝ), f = ∑ i, S i ^ 2 := ⊢ ¬∃ n, ∃ (_ : 0 < n), ∃ S, f = ∑ i, S i ^ 2
All goals completed! 🐙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)$.
def Hilbert17thProblemHomogenousPoly (n d : ℕ) : Prop :=
∀ f : MvPolynomial (Fin n) ℝ, f.IsHomogeneous (2 * d) →
(∀ x : Fin n → ℝ, 0 ≤ f.eval x) →
∃ (m : ℕ) (g : Fin m → MvPolynomial (Fin n) ℝ), f = ∑ i, (g i) ^ 2d:ℕf:MvPolynomial (Fin 0) ℝhf:f.IsHomogeneous (2 * d)hf₀:∀ (x : Fin 0 → ℝ), 0 ≤ (eval x) (C (coeff 0 f))hfd:f ≠ 0 → f.totalDegree = 2 * d⊢ C (coeff 0 f) = ∑ x, C (coeff 0 (C (coeff 0 f)))
All goals completed! 🐙n:ℕf:MvPolynomial (Fin n) ℝhf:f.IsHomogeneous (2 * 0)hf₀:∀ (x : Fin n → ℝ), 0 ≤ (eval x) fhf_zero:f ≠ 0hfd:f = C (coeff 0 f)⊢ f = ∑ x, C (coeff 0 f)
All goals completed! 🐙Hilbert's 17th problem for homogeneous polynomials: characterization of dimensions and degrees where non-negative polynomials are sums of squares of polynomials.
@[category research solved, AMS 12]
theorem 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 := n:ℕd:ℕhn:0 < nhd:0 < d⊢ Hilbert17thProblemHomogenousPoly n d ↔ n = 1 ∨ n = 2 ∨ d = 1 ∨ n = 3 ∧ d = 2
All goals completed! 🐙end Hilbert17