Pierce–Birkhoff conjecture

Reference: Wikipedia

The Pierce-Birkhoff conjecture asserts that any piecewise-polynomial function can be expressed as a maximum of finite minima of finite collections of polynomials. It was first stated in 1956 by Garrett Birkhoff and Richard S. Pierce, though the modern rigorous formulation is due to Melvin Henriksen and John R. Isbell.

The conjecture has been proved for n = 1 and n = 2 by Louis Mahé.

def IsSemiAlgebraic {n : ℕ} (S : Set (EuclideanSpace ℝ (Fin n))) : Prop

A set is semi-algebraic in ℝⁿ if it can be described by a finite union of sets defined by multivariate polynomial equations and inequalities.

Equations

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

def IsSemiAlgebraic₁ (S : Set ℝ) : Prop

A set is semi-algebraic in ℝ if it can be described by a finite boolean combination of polynomial equations and inequalities.

Equations

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

def IsPiecewiseMvPolynomial {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) : Prop

A function f : ℝⁿ → ℝ is piecewise polynomial if there exists a finite covering of ℝⁿ by closed semi-algebraic sets such that the restriction of f to each set in the covering is polynomial.

Equations

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

def IsPiecewisePolynomial (f : ℝ → ℝ) : Prop

A function f : ℝ → ℝ is piecewise polynomial if there exists a finite covering of ℝ by closed semi-algebraic sets such that the restriction of f to each set in the covering is polynomial.

Equations

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

theorem pierce_birkhoff_conjecture {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : IsPiecewiseMvPolynomial f) : ∃ (ι : Type) (κ : Type) (g : ι → κ → MvPolynomial (Fin n) ℝ), Finite ι ∧ Finite κ ∧ ∀ (x : EuclideanSpace ℝ (Fin n)), f x = ⨆ (i : ι), ⨅ (j : κ), (MvPolynomial.eval x) (g i j)

The Pierce-Birkhoff conjecture states that for every real piecewise-polynomial function f : ℝⁿ → ℝ, there exists a finite set of polynomials gᵢⱼ ∈ ℝ[x₁, ..., xₙ] such that f = supᵢ infⱼ(gᵢⱼ).

theorem pierce_birkhoff_conjecture_dim_one (f : ℝ → ℝ) (hf : IsPiecewisePolynomial f) : ∃ (ι : Type) (κ : Type) (g : ι → κ → Polynomial ℝ), Finite ι ∧ Finite κ ∧ ∀ (x : ℝ), f x = ⨆ (i : ι), ⨅ (j : κ), Polynomial.eval x (g i j)

The Pierce-Birkhoff conjecture holds for n = 1. This was proved by Louis Mahé.

theorem pierce_birkhoff_conjecture_dim_two (f : EuclideanSpace ℝ (Fin 2) → ℝ) (hf : IsPiecewiseMvPolynomial f) : ∃ (ι : Type) (κ : Type) (g : ι → κ → MvPolynomial (Fin 2) ℝ), Finite ι ∧ Finite κ ∧ ∀ (x : EuclideanSpace ℝ (Fin 2)), f x = ⨆ (i : ι), ⨅ (j : κ), (MvPolynomial.eval x) (g i j)

The Pierce-Birkhoff conjecture holds for n = 2. This was proved by Louis Mahé.