Analytic functions with semialgebraic graphs are Nash

A real-valued function with semialgebraic graph on any specified domain satisfies a single nonzero polynomial relation on that entire domain. Neither continuity nor openness of the domain is needed for this algebraic assertion. In particular, if the function is analytic at a point and its graph is semialgebraic on a neighbourhood, it is a Nash germ there.

The scalar output is encoded as Unit → ℝ in IsSemialgebraicOn, in accordance with its finite-coordinate graph convention. The resulting relation is a polynomial in the value variable with coefficients in the coordinate polynomial ring, as used by IsNashAt. The empty domain and the zero-dimensional input space are included. No nonsingularity of the relation at a graph point is asserted or needed.

References

• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998, Section 8.1 (the semialgebraic graph criterion for Nash functions).

theorem TauCeti.IsSemialgebraicOn.exists_ne_zero_polynomial_relation {σ : Type u_1} {f : (σ → ℝ) → ℝ} {s : Set (σ → ℝ)} (hf : IsSemialgebraicOn (fun (x : σ → ℝ) (x_1 : Unit) => f x) s) : ∃ (P : Polynomial (MvPolynomial σ ℝ)), P ≠ 0 ∧ ∀ x ∈ s, Polynomial.eval (f x) (Polynomial.map (MvPolynomial.eval x) P) = 0

A scalar function with semialgebraic graph on s satisfies one nonzero polynomial relation on all of s, without continuity or openness assumptions.

theorem TauCeti.IsSemialgebraicOn.isNashAt {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {s : Set (σ → ℝ)} {x : σ → ℝ} (hf : IsSemialgebraicOn (fun (y : σ → ℝ) (x : Unit) => f y) s) (hfa : AnalyticAt ℝ f x) (hs : s ∈ nhds x) : IsNashAt f x

An analytic function whose graph is semialgebraic on a neighbourhood of x is a Nash germ at x. The neighbourhood need not itself be open.

theorem TauCeti.IsSemialgebraicOn.isNashAt_of_isOpen {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {s : Set (σ → ℝ)} (hf : IsSemialgebraicOn (fun (y : σ → ℝ) (x : Unit) => f y) s) (hfa : AnalyticOnNhd ℝ f s) (hs : IsOpen s) (x : σ → ℝ) : x ∈ s → IsNashAt f x

An analytic function with semialgebraic graph on an open domain is Nash at every point of that domain.