FormalConjectures.HilbertProblems.«17»

/-
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 FormalConjecturesUtil

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.


open Real MvPolynomial


namespace Hilbert17

Hilbert's 17th problem: every non-negative multivariate polynomial is a sum of squares of rational functions.

@[category research solved, AMS 12]
theorem declaration uses 'sorry'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 := byn:ℕ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
  sorryAll 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 + 1

The Motzkin polynomial is non-negative everywhere.

@[category textbook, AMS 12]
theorem f_nonneg : ∀ x y : ℝ, 0 ≤ f.eval ![x, y] := by⊢ ∀ (x y : ℝ), 0 ≤ (eval ![x, y]) f
  intro x yx:ℝy:ℝ⊢ 0 ≤ (eval ![x, y]) f
  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, f, Fin.isValue, map_add, map_sub, map_mul, map_pow,
    eval_X, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one, eval_ofNat, map_one]x:ℝy:ℝ⊢ 0 ≤ x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1
  by_cases hx : x = 0posx:ℝy:ℝhx:x = 0⊢ 0 ≤ x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1negx:ℝy:ℝhx:¬x = 0⊢ 0 ≤ x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1
  ·posx:ℝy:ℝhx:x = 0⊢ 0 ≤ x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1 simp [hx]All goals completed! 🐙
  have h : 0 < (x ^ 2 + y ^ 2) ^ 2 := by⊢ ∀ (x y : ℝ), 0 ≤ (eval ![x, y]) f positivityAll goals completed! 🐙
  refine nonneg_of_mul_nonneg_left ?_ hnegx:ℝy:ℝhx:¬x = 0h:0 < (x ^ 2 + y ^ 2) ^ 2 := 
  pow_pos
    (add_pos_of_pos_of_nonneg (lt_of_le_of_ne' (Even.pow_nonneg (even_two_mul 1) x) (pow_ne_zero 2 hx))
      (Even.pow_nonneg (even_two_mul 1) y))
    2⊢ 0 ≤ (x ^ 4 * y ^ 2 + x ^ 2 * y ^ 4 - 3 * x ^ 2 * y ^ 2 + 1) * (x ^ 2 + y ^ 2) ^ 2
  have H : 0 ≤ (x ^ 3 * y + x * y ^ 3 - 2 * x * y) ^ 2 * (1 + x ^ 2 + y ^ 2)
    + (x ^ 2 - y ^ 2) ^ 2 := by⊢ ∀ (x y : ℝ), 0 ≤ (eval ![x, y]) f positivityAll goals completed! 🐙
  linear_combination HAll goals completed! 🐙

The Motzkin polynomial cannot be written as a sum of squares of polynomials.

@[category textbook, AMS 12]
theorem declaration uses 'sorry'f_not_sum_of_squares :
    ¬∃ (n : ℕ) (hn : 0 < n) (S : Fin n → MvPolynomial (Fin 2) ℝ), f = ∑ i, S i ^ 2 := by⊢ ¬∃ n, ∃ (_ : 0 < n), ∃ S, f = ∑ i, S i ^ 2
  sorryAll 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) ^ 2


@[category test, AMS 12]
theorem Hilbert17thProblemHomogenousPoly_zero_left (d : ℕ) :
    Hilbert17thProblemHomogenousPoly 0 d := byd:ℕ⊢ Hilbert17thProblemHomogenousPoly 0 d
  refine fun f hf hf₀ ↦ ⟨1, fun _ ↦ C √(f.coeff 0), ?_⟩d:ℕf:MvPolynomial (Fin 0) ℝhf:f.IsHomogeneous (2 * d)hf₀:∀ (x : Fin 0 → ℝ), 0 ≤ (eval x) f⊢ f = ∑ i, (fun x => C √(coeff 0 f)) i ^ 2
  have hfd := hf.totalDegreed:ℕf:MvPolynomial (Fin 0) ℝhf:f.IsHomogeneous (2 * d)hf₀:∀ (x : Fin 0 → ℝ), 0 ≤ (eval x) fhfd:f ≠ 0 → f.totalDegree = 2 * d := IsHomogeneous.totalDegree hf⊢ f = ∑ i, (fun x => C √(coeff 0 f)) i ^ 2
  rw [f.eq_C_of_isEmpty] at hf₀ ⊢d:ℕ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) = ∑ i, (fun x => C √(coeff 0 (C (coeff 0 f)))) i ^ 2
  rw [Finset.sum_congr rfl fun _ _ ↦ (map_pow _ _ _).symm, Real.sq_sqrt <| by simpa using hf₀]d:ℕ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)))
  simpAll goals completed! 🐙


@[category test, AMS 12]
theorem Hilbert17thProblemHomogenousPoly_zero_right (n : ℕ) :
    Hilbert17thProblemHomogenousPoly n 0 := byn:ℕ⊢ Hilbert17thProblemHomogenousPoly n 0
  intro f hfn:ℕf:MvPolynomial (Fin n) ℝhf:f.IsHomogeneous (2 * 0)⊢ (∀ (x : Fin n → ℝ), 0 ≤ (eval x) f) → ∃ m g, f = ∑ i, g i ^ 2 hf₀n:ℕf:MvPolynomial (Fin n) ℝhf:f.IsHomogeneous (2 * 0)hf₀:∀ (x : Fin n → ℝ), 0 ≤ (eval x) f⊢ ∃ m g, f = ∑ i, g i ^ 2
  rcases eq_or_ne f 0 with (rfl | hf_zero)inln:ℕhf:IsHomogeneous 0 (2 * 0)hf₀:∀ (x : Fin n → ℝ), 0 ≤ (eval x) 0⊢ ∃ m g, 0 = ∑ i, g i ^ 2inrn:ℕf:MvPolynomial (Fin n) ℝhf:f.IsHomogeneous (2 * 0)hf₀:∀ (x : Fin n → ℝ), 0 ≤ (eval x) fhf_zero:f ≠ 0⊢ ∃ m g, f = ∑ i, g i ^ 2; ·inln:ℕhf:IsHomogeneous 0 (2 * 0)hf₀:∀ (x : Fin n → ℝ), 0 ≤ (eval x) 0⊢ ∃ m g, 0 = ∑ i, g i ^ 2 exact ⟨0, 0, byn:ℕhf:IsHomogeneous 0 (2 * 0)hf₀:∀ (x : Fin n → ℝ), 0 ≤ (eval x) 0⊢ 0 = ∑ i, 0 i ^ 2 simpAll goals completed! 🐙⟩
  have hfd := f.totalDegree_eq_zero_iff_eq_C.1 <| byn:ℕf:MvPolynomial (Fin n) ℝhf:f.IsHomogeneous (2 * 0)hf₀:∀ (x : Fin n → ℝ), 0 ≤ (eval x) fhf_zero:f ≠ 0⊢ f.totalDegree = 0 simpa using hf.totalDegree hf_zeroAll goals completed! 🐙
  use 1, fun _ ↦ C √(f.coeff 0)hn:ℕ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) := 
  totalDegree_eq_zero_iff_eq_C.mp
    (Eq.mp (congrArg (Eq f.totalDegree) (mul_zero 2)) (IsHomogeneous.totalDegree hf hf_zero))⊢ f = ∑ i, (fun x => C √(coeff 0 f)) i ^ 2
  rw [Finset.sum_congr rfl fun _ _ ↦ (map_pow _ _ _).symm, Real.sq_sqrt <| by simpa using hf₀ 0]hn:ℕ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) := 
  totalDegree_eq_zero_iff_eq_C.mp
    (Eq.mp (congrArg (Eq f.totalDegree) (mul_zero 2)) (IsHomogeneous.totalDegree hf hf_zero))⊢ f = ∑ x, C (coeff 0 f)
  simpa using hfdAll 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 declaration uses 'sorry'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 := byn:ℕd:ℕhn:0 < nhd:0 < d⊢ Hilbert17thProblemHomogenousPoly n d ↔ n = 1 ∨ n = 2 ∨ d = 1 ∨ n = 3 ∧ d = 2
  sorryAll goals completed! 🐙


end Hilbert17