Nash implicit functions for finite systems

A finite system of Nash equations with invertible derivative in the unknown variables has a Nash implicit solution. The equations are expressed on σ ⊕ τ → ℝ, with parameter coordinates σ and unknown coordinates τ; the differential uses the corresponding product space. The equation coordinates may have any finite index type ρ.

HasStrictFDerivAt.isNashAt_implicitFunctionOfProdDomain identifies Mathlib's chosen implicit function as Nash, coordinatewise. The existence theorem also retains its local level-set characterization. Finally, any continuous solution through the same point agrees with this implicit function as a germ, so it is Nash without a separate analyticity assumption. These results supply implicit coordinate changes for Nash charts, not just scalar root sections.

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.

The analytic solution and local uniqueness are those of HasStrictFDerivAt.implicitFunctionOfProdDomain; Nashness follows from the local Nash graph criterion by identifying its graph with a level set on a smaller semialgebraic neighborhood.

theorem HasStrictFDerivAt.isNashAt_implicitFunctionOfProdDomain {σ : Type u_1} {τ : Type u_2} {ρ : Type u_3} [Fintype σ] [Fintype τ] [Fintype ρ] {F : (σ ⊕ τ → ℝ) → ρ → ℝ} {u : (σ → ℝ) × (τ → ℝ)} {D : (σ → ℝ) × (τ → ℝ) →L[ℝ] ρ → ℝ} (hD : HasStrictFDerivAt (fun (p : (σ → ℝ) × (τ → ℝ)) => F (Sum.elim p.1 p.2)) D u) (hInv : (D ∘SL ContinuousLinearMap.inr ℝ (σ → ℝ) (τ → ℝ)).IsInvertible) (hF : ∀ (i : ρ), TauCeti.IsNashAt (fun (z : σ ⊕ τ → ℝ) => F z i) (Sum.elim u.1 u.2)) (i : τ) : TauCeti.IsNashAt (fun (x : σ → ℝ) => hD.implicitFunctionOfProdDomain hInv x i) u.1

Nash implicit function theorem for systems. If the coordinates of a finite system are Nash at u and its partial derivative in the unknown variables is invertible, every coordinate of Mathlib's chosen implicit function is a Nash germ at the parameter point.

theorem TauCeti.exists_isNashAt_implicit_system {σ : Type u_1} {τ : Type u_2} {ρ : Type u_3} [Fintype σ] [Fintype τ] {F : (σ ⊕ τ → ℝ) → ρ → ℝ} {u : (σ → ℝ) × (τ → ℝ)} [Finite ρ] (hF : ∀ (i : ρ), IsNashAt (fun (z : σ ⊕ τ → ℝ) => F z i) (Sum.elim u.1 u.2)) (hInv : (fderiv ℝ (fun (p : (σ → ℝ) × (τ → ℝ)) => F (Sum.elim p.1 p.2)) u ∘SL ContinuousLinearMap.inr ℝ (σ → ℝ) (τ → ℝ)).IsInvertible) : ∃ (g : (σ → ℝ) → τ → ℝ), (∀ (i : τ), IsNashAt (fun (x : σ → ℝ) => g x i) u.1) ∧ g u.1 = u.2 ∧ (∀ᶠ (x : σ → ℝ) in nhds u.1, F (Sum.elim x (g x)) = F (Sum.elim u.1 u.2)) ∧ ∀ᶠ (p : (σ → ℝ) × (τ → ℝ)) in nhds u, F (Sum.elim p.1 p.2) = F (Sum.elim u.1 u.2) ↔ g p.1 = p.2

A finite Nash system with invertible partial derivative admits a coordinatewise Nash implicit solution. Near the original point its level set is exactly the graph of that solution. No nonemptiness assumption on the parameter or unknown coordinate types is required.

theorem TauCeti.isNashAt_of_implicit_system {σ : Type u_1} {τ : Type u_2} {ρ : Type u_3} [Fintype σ] [Fintype τ] {F : (σ ⊕ τ → ℝ) → ρ → ℝ} {u : (σ → ℝ) × (τ → ℝ)} [Finite ρ] (hF : ∀ (i : ρ), IsNashAt (fun (z : σ ⊕ τ → ℝ) => F z i) (Sum.elim u.1 u.2)) (hInv : (fderiv ℝ (fun (p : (σ → ℝ) × (τ → ℝ)) => F (Sum.elim p.1 p.2)) u ∘SL ContinuousLinearMap.inr ℝ (σ → ℝ) (τ → ℝ)).IsInvertible) {g : (σ → ℝ) → τ → ℝ} (hg : ContinuousAt g u.1) (hgu : g u.1 = u.2) (hsol : ∀ᶠ (x : σ → ℝ) in nhds u.1, F (Sum.elim x (g x)) = F (Sum.elim u.1 u.2)) (i : τ) : IsNashAt (fun (x : σ → ℝ) => g x i) u.1

Every continuous solution of a nonsingular finite Nash system through the original point is Nash there. Analyticity of the solution is a conclusion, not a hypothesis.