Nash implicit roots

The analytic implicit root of a Nash scalar equation at a simple zero is a Nash germ. The equation uses coordinates σ ⊕ Unit: σ indexes the parameters and Unit the unknown. The parameter space may have dimension zero.

TauCeti.IsNashAt.exists_isNashAt_eventually_eq_zero_iff constructs the root and identifies its graph with the zero set near the given point. TauCeti.IsNashAt.implicit applies to an already specified solution continuous at the base point. These results allow simple-root sections to be used as Nash functions, without requiring the defining equation to be polynomial.

The graph argument shrinks to a semialgebraic ball where the equation has semialgebraic graph and the local uniqueness assertion holds. A smaller parameter ball keeps the entire solution graph inside that ball. Tarski–Seidenberg makes the zero locus semialgebraic, and the local Nash graph criterion then applies. The convergent analytic implicit function theorem supplies existence and uniqueness, rather than either being assumed in the simple-root theorem.

References

• J. Bochnak, M. Coste, M.-F. Roy, Real Algebraic Geometry, Springer, 1998, Section 8.1.
• S. G. Krantz, H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser, 2002, Chapter 2.

theorem TauCeti.IsNashAt.of_eventually_eq_zero_iff {σ : Type u_1} [Fintype σ] {f : (σ ⊕ Unit → ℝ) → ℝ} {g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f (Sum.elim x fun (x_1 : Unit) => g x)) (hg : AnalyticAt ℝ g x) (hzero : ∀ᶠ (p : σ ⊕ Unit → ℝ) in nhds (Sum.elim x fun (x_1 : Unit) => g x), f p = 0 ↔ g (p ∘ Sum.inl) = p (Sum.inr ())) : IsNashAt g x

An analytic graph which locally is the zero set of a Nash equation is a Nash germ. The equality of zero sets is required on a neighborhood in the full parameter/unknown space, not only on the graph.

theorem TauCeti.IsNashAt.exists_isNashAt_eventually_eq_zero_iff {σ : Type u_1} [Fintype σ] {f : (σ ⊕ Unit → ℝ) → ℝ} {x : σ → ℝ} {z : ℝ} (hf : IsNashAt f (Sum.elim x fun (x : Unit) => z)) (hz : f (Sum.elim x fun (x : Unit) => z) = 0) (hd : deriv (fun (t : ℝ) => f (Sum.elim x fun (x : Unit) => t)) z ≠ 0) : ∃ (g : (σ → ℝ) → ℝ), IsNashAt g x ∧ g x = z ∧ (∀ᶠ (y : σ → ℝ) in nhds x, f (Sum.elim y fun (x : Unit) => g y) = 0) ∧ ∀ᶠ (p : σ ⊕ Unit → ℝ) in nhds (Sum.elim x fun (x : Unit) => z), f p = 0 ↔ g (p ∘ Sum.inl) = p (Sum.inr ())

The Nash implicit root theorem. A Nash scalar equation with a simple zero admits a Nash root germ in the parameter variables. Near the given point its zero set is exactly the graph of this root. No polynomial equation or global semialgebraic domain is required.

theorem TauCeti.IsNashAt.implicit {σ : Type u_1} [Fintype σ] {f : (σ ⊕ Unit → ℝ) → ℝ} {g : (σ → ℝ) → ℝ} {x : σ → ℝ} (hf : IsNashAt f (Sum.elim x fun (x_1 : Unit) => g x)) (hg : ContinuousAt g x) (hroot : ∀ᶠ (y : σ → ℝ) in nhds x, f (Sum.elim y fun (x : Unit) => g y) = 0) (hd : deriv (fun (t : ℝ) => f (Sum.elim x fun (x : Unit) => t)) (g x) ≠ 0) : IsNashAt g x

Any solution germ of a Nash scalar equation that is continuous at the base point is Nash if the derivative in the unknown variable is nonzero at its central value.