Nash germs

A real function f on σ → ℝ is a Nash germ at x (TauCeti.IsNashAt) if it is analytic at x and satisfies a nonzero polynomial relation P (y, f y) = 0 for all y near x. The relation P is a polynomial in the value variable t whose coefficients are polynomials in the coordinates y, that is, an element P : (MvPolynomial σ ℝ)[X] of ℝ[y][t] ≃ ℝ[y, t]. Both the polynomial and the neighbourhood may depend on x. A function on an open set is a Nash function when its germ at every point is a Nash germ. Nash functions are the analytic functions of real algebraic geometry; classically, an analytic function on an open semialgebraic set is Nash exactly when its graph is semialgebraic (Bochnak–Coste–Roy, Section 8.1), a criterion not proved here.

This file proves that being a Nash germ is a property of the germ, that it propagates to nearby points, and that Nash germs form a subring of the analytic germs that is closed under inverses of nonvanishing germs:

• polynomial functions, in particular constants and coordinate functions, are Nash germs;
• sums, negations, differences, products, powers, finite sums and finite products of Nash germs are Nash germs;
• the inverse and quotients of Nash germs are Nash germs where the denominator does not vanish.

The algebraic closure properties come from Mathlib's algebraic elements of an algebra over a domain (IsAlgebraic.add, IsAlgebraic.mul, IsAlgebraic.invOf): a polynomial relation near x is exactly algebraicity of the germ of f at x over ℝ[y], where polynomials act on germs as polynomial functions (Filter.Germ.isAlgebraic_coe_iff).

Main declarations

• TauCeti.IsNashAt f x: f is a Nash germ at x.
• TauCeti.isNashAt_iff_exists_mem_nhds: the neighbourhood form, an analytic function with a polynomial relation on a whole neighbourhood of x.
• TauCeti.IsNashAt.congr: Nash germs depend only on the germ.
• TauCeti.IsNashAt.eventually_isNashAt: a Nash germ at x is a Nash germ at every nearby point.
• MvPolynomial.isNashAt_eval, TauCeti.IsNashAt.add, TauCeti.IsNashAt.mul, TauCeti.IsNashAt.inv, TauCeti.IsNashAt.div: the algebraic closure properties.

References

• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Ergebnisse der Mathematik und ihrer Grenzgebiete (3) 36, Springer, 1998, Section 8.1 (Nash functions).

def TauCeti.IsNashAt {σ : Type u_1} [Fintype σ] (f : (σ → ℝ) → ℝ) (x : σ → ℝ) : Prop

A real function f on σ → ℝ is a Nash germ at x if it is analytic at x and satisfies a nonzero polynomial relation P (y, f y) = 0 for all y near x. Here P : (MvPolynomial σ ℝ)[X] is a polynomial in the value variable whose coefficients are polynomials in the coordinates, and P (y, t) is (P.map (MvPolynomial.eval y)).eval t.

theorem TauCeti.isNashAt_iff {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} : IsNashAt f x ↔ AnalyticAt ℝ f x ∧ ∃ (P : Polynomial (MvPolynomial σ ℝ)), P ≠ 0 ∧ ∀ᶠ (y : σ → ℝ) in nhds x, Polynomial.eval (f y) (Polynomial.map (MvPolynomial.eval y) P) = 0

Unfolding TauCeti.IsNashAt.

theorem TauCeti.IsNashAt.analyticAt {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) : AnalyticAt ℝ f x

A Nash germ is analytic.

theorem TauCeti.isNashAt_iff_exists_mem_nhds {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} : IsNashAt f x ↔ ∃ U ∈ nhds x, AnalyticOnNhd ℝ f U ∧ ∃ (P : Polynomial (MvPolynomial σ ℝ)), P ≠ 0 ∧ ∀ y ∈ U, Polynomial.eval (f y) (Polynomial.map (MvPolynomial.eval y) P) = 0

A Nash germ at x is an analytic function on a neighbourhood U of x satisfying a single nonzero polynomial relation P (y, f y) = 0 at every point y ∈ U.

theorem TauCeti.IsNashAt.congr {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (hg : f =ᶠ[nhds x] g) : IsNashAt g x

Being a Nash germ depends only on the germ of the function.

theorem Filter.EventuallyEq.isNashAt_iff {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hg : f =ᶠ[nhds x] g) : TauCeti.IsNashAt f x ↔ TauCeti.IsNashAt g x

Functions with the same germ at x are Nash germs at x together.

theorem TauCeti.IsNashAt.eventually_isNashAt {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) : ∀ᶠ (y : σ → ℝ) in nhds x, IsNashAt f y

A Nash germ at x is a Nash germ at every point near x.

Nash germs as algebraic germs

Polynomial functions

theorem MvPolynomial.isNashAt_eval {σ : Type u_1} [Fintype σ] {x : σ → ℝ} (p : MvPolynomial σ ℝ) : TauCeti.IsNashAt (fun (y : σ → ℝ) => (eval y) p) x

Polynomial functions are Nash germs at every point.

theorem TauCeti.isNashAt_const {σ : Type u_1} [Fintype σ] {x : σ → ℝ} (c : ℝ) : IsNashAt (fun (x : σ → ℝ) => c) x

Constant functions are Nash germs.

theorem TauCeti.isNashAt_apply {σ : Type u_1} [Fintype σ] {x : σ → ℝ} (i : σ) : IsNashAt (fun (y : σ → ℝ) => y i) x

Coordinate functions are Nash germs.

Ring operations

theorem TauCeti.IsNashAt.add {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (hg : IsNashAt g x) : IsNashAt (f + g) x

The sum of two Nash germs is a Nash germ.

theorem TauCeti.IsNashAt.fun_add {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (hg : IsNashAt g x) : IsNashAt (fun (i : σ → ℝ) => f i + g i) x

Eta-expanded form of TauCeti.IsNashAt.add

---

The sum of two Nash germs is a Nash germ.

theorem TauCeti.IsNashAt.neg {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) : IsNashAt (-f) x

The negation of a Nash germ is a Nash germ.

theorem TauCeti.IsNashAt.fun_neg {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) : IsNashAt (fun (i : σ → ℝ) => -f i) x

Eta-expanded form of TauCeti.IsNashAt.neg

---

The negation of a Nash germ is a Nash germ.

theorem TauCeti.IsNashAt.sub {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (hg : IsNashAt g x) : IsNashAt (f - g) x

The difference of two Nash germs is a Nash germ.

theorem TauCeti.IsNashAt.fun_sub {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (hg : IsNashAt g x) : IsNashAt (fun (i : σ → ℝ) => f i - g i) x

Eta-expanded form of TauCeti.IsNashAt.sub

---

The difference of two Nash germs is a Nash germ.

theorem TauCeti.IsNashAt.mul {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (hg : IsNashAt g x) : IsNashAt (f * g) x

The product of two Nash germs is a Nash germ.

theorem TauCeti.IsNashAt.fun_mul {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (hg : IsNashAt g x) : IsNashAt (fun (i : σ → ℝ) => f i * g i) x

Eta-expanded form of TauCeti.IsNashAt.mul

---

The product of two Nash germs is a Nash germ.

theorem TauCeti.IsNashAt.pow {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (n : ℕ) : IsNashAt (f ^ n) x

Powers of a Nash germ are Nash germs.

theorem TauCeti.IsNashAt.fun_pow {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (n : ℕ) : IsNashAt (fun (i : σ → ℝ) => f i ^ n) x

Eta-expanded form of TauCeti.IsNashAt.pow

---

Powers of a Nash germ are Nash germs.

theorem Finset.isNashAt_sum {σ : Type u_1} [Fintype σ] {x : σ → ℝ} {ι : Type u_2} {F : ι → (σ → ℝ) → ℝ} (N : Finset ι) (h : ∀ i ∈ N, TauCeti.IsNashAt (F i) x) : TauCeti.IsNashAt (∑ i ∈ N, F i) x

Finite sums of Nash germs are Nash germs.

theorem Finset.fun_isNashAt_sum {σ : Type u_1} [Fintype σ] {x : σ → ℝ} {ι : Type u_2} {F : ι → (σ → ℝ) → ℝ} (N : Finset ι) (h : ∀ i ∈ N, TauCeti.IsNashAt (F i) x) : TauCeti.IsNashAt (fun (a : σ → ℝ) => ∑ c ∈ N, F c a) x

Eta-expanded form of Finset.isNashAt_sum

---

Finite sums of Nash germs are Nash germs.

theorem Finset.isNashAt_prod {σ : Type u_1} [Fintype σ] {x : σ → ℝ} {ι : Type u_2} {F : ι → (σ → ℝ) → ℝ} (N : Finset ι) (h : ∀ i ∈ N, TauCeti.IsNashAt (F i) x) : TauCeti.IsNashAt (∏ i ∈ N, F i) x

Finite products of Nash germs are Nash germs.

theorem Finset.fun_isNashAt_prod {σ : Type u_1} [Fintype σ] {x : σ → ℝ} {ι : Type u_2} {F : ι → (σ → ℝ) → ℝ} (N : Finset ι) (h : ∀ i ∈ N, TauCeti.IsNashAt (F i) x) : TauCeti.IsNashAt (fun (a : σ → ℝ) => ∏ c ∈ N, F c a) x

Eta-expanded form of Finset.isNashAt_prod

---

Finite products of Nash germs are Nash germs.

Inverses

theorem TauCeti.IsNashAt.inv {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (h0 : f x ≠ 0) : IsNashAt f⁻¹ x

The inverse of a Nash germ which does not vanish at x is a Nash germ at x.

theorem TauCeti.IsNashAt.fun_inv {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (h0 : f x ≠ 0) : IsNashAt (fun (i : σ → ℝ) => (f i)⁻¹) x

Eta-expanded form of TauCeti.IsNashAt.inv

---

The inverse of a Nash germ which does not vanish at x is a Nash germ at x.

theorem TauCeti.IsNashAt.div {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (hg : IsNashAt g x) (h0 : g x ≠ 0) : IsNashAt (f / g) x

The quotient of Nash germs is a Nash germ where the denominator does not vanish.

theorem TauCeti.IsNashAt.fun_div {σ : Type u_1} [Fintype σ] {f g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f x) (hg : IsNashAt g x) (h0 : g x ≠ 0) : IsNashAt (fun (i : σ → ℝ) => f i / g i) x

Eta-expanded form of TauCeti.IsNashAt.div

---

The quotient of Nash germs is a Nash germ where the denominator does not vanish.