Formal target: Corpus.WikipediaPierceBirkhoff.pierce_birkhoff_conjecture

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ᵢⱼ).

Exact formal statement

∀ {n : Nat} (f : (Fin n → Real) → Real),
  Corpus.WikipediaPierceBirkhoff.IsPiecewiseMvPolynomial f →
    Exists.{2} fun ι =>
      Exists.{2} fun κ =>
        Exists.{1} fun g =>
          And (Finite.{1} ι)
            (And (Finite.{1} κ)
              (∀ (x : Fin n → Real),
                Eq.{1} (f x)
                  (iSup.{0, 1} fun i =>
                    iInf.{0, 1} fun j => DFunLike.coe.{1, 1, 1} (MvPolynomial.eval.{0, 0} x) (g i j))))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record