Real Algebraic
Results named in Tau Ceti's TauCeti.Geometry.RealAlgebraic modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremFinite-fiber dimension theorem#
A semialgebraic function with finite fibers on its domain preserves dimension. In particular this applies to semialgebraic bijections, without requiring continuity of the function or its inverse.
TauCeti.IsSemialgebraicOn.semialgebraicDim_image_of_finite {m n : ℕ} {s : Set (Fin n → ℝ)}
{f : (Fin n → ℝ) → Fin m → ℝ} (hf : TauCeti.IsSemialgebraicOn f s)
(hfin : ∀ (y : Fin m → ℝ), {x | x ∈ s ∧ f x = y}.Finite) :
TauCeti.semialgebraicDim (f '' s) = TauCeti.semialgebraicDim s
Lean
Formalized in Tau Ceti as TauCeti.IsSemialgebraicOn.semialgebraicDim_image_of_finite.
Other forms
Finite-fiber dimension theorem for coordinate projections. Formalized in Tau Ceti as TauCeti.IsSemialgebraic.semialgebraicDim_image_comp_of_finite.
TauCeti.IsSemialgebraic.semialgebraicDim_image_comp_of_finite {m n : ℕ} {s : Set (Fin n → ℝ)}
(hs : TauCeti.IsSemialgebraic s) (ι : Fin m → Fin n)
(hfin : ∀ (y : Fin m → ℝ), {x | x ∈ s ∧ x ∘ ι = y}.Finite) :
TauCeti.semialgebraicDim ((fun x => x ∘ ι) '' s) = TauCeti.semialgebraicDim s
Sources
TheoremThe local Nash graph criterion#
A scalar function is a Nash germ at x exactly when
it is analytic there and its graph is semialgebraic on some open semialgebraic neighbourhood.
TauCeti.isNashAt_iff_exists_isSemialgebraicOn.{u_1} {σ : Type u_1} [Fintype σ] {f : (σ → ℝ) → ℝ}
{x : σ → ℝ} :
TauCeti.IsNashAt f x ↔
AnalyticAt ℝ f x ∧
∃ U,
IsOpen U ∧ x ∈ U ∧ TauCeti.IsSemialgebraic U ∧ TauCeti.IsSemialgebraicOn (fun y x => f y) U
Lean
Formalized in Tau Ceti as TauCeti.isNashAt_iff_exists_isSemialgebraicOn.
Other forms
The local Nash graph criterion for maps. Formalized in Tau Ceti as TauCeti.forall_isNashAt_apply_iff_exists_isSemialgebraicOn.
TauCeti.forall_isNashAt_apply_iff_exists_isSemialgebraicOn.{u_1, u_2} {σ : Type u_1} {τ : Type u_2}
[Fintype σ] [Fintype τ] {g : (σ → ℝ) → τ → ℝ} {x : σ → ℝ} :
(∀ (i : τ), TauCeti.IsNashAt (fun y => g y i) x) ↔
AnalyticAt ℝ g x ∧ ∃ U, IsOpen U ∧ x ∈ U ∧ TauCeti.IsSemialgebraicOn g U
Sources
TheoremNash 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.
HasStrictFDerivAt.isNashAt_implicitFunctionOfProdDomain.{u_1, u_2, u_3} {σ : 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
Lean
Formalized in Tau Ceti as HasStrictFDerivAt.isNashAt_implicitFunctionOfProdDomain.
Sources
TheoremThe 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.
TauCeti.IsNashAt.exists_isNashAt_eventually_eq_zero_iff.{u_1} {σ : Type u_1} [Fintype σ]
{f : (σ ⊕ Unit → ℝ) → ℝ} {x : σ → ℝ} {z : ℝ} (hf : TauCeti.IsNashAt f (Sum.elim x fun x => z))
(hz : f (Sum.elim x fun x => z) = 0) (hd : deriv (fun t => f (Sum.elim x fun x => t)) z ≠ 0) :
∃ g,
TauCeti.IsNashAt g x ∧
g x = z ∧
(∀ᶠ (y : σ → ℝ) in nhds x, f (Sum.elim y fun x => g y) = 0) ∧
∀ᶠ (p : σ ⊕ Unit → ℝ) in nhds (Sum.elim x fun x => z),
f p = 0 ↔ g (p ∘ Sum.inl) = p (Sum.inr ())
Lean
Formalized in Tau Ceti as TauCeti.IsNashAt.exists_isNashAt_eventually_eq_zero_iff.
Sources
TheoremThe Nash inverse function theorem#
A map with Nash coordinate germs and invertible
Fréchet derivative at a restricts, inside any prescribed neighbourhood, to a local
homeomorphism with open semialgebraic source and target and semialgebraic graphs in both
directions. Every coordinate of the map and its inverse is Nash throughout those domains.
Empty coordinate index types are allowed.
TauCeti.exists_openPartialHomeomorph_of_forall_isNashAt.{u_1, u_2} {σ : Type u_1} {τ : Type u_2}
[Fintype σ] [Fintype τ] {f : (σ → ℝ) → τ → ℝ} {a : σ → ℝ}
(hf : ∀ (i : τ), TauCeti.IsNashAt (fun x => f x i) a) {L : (σ → ℝ) ≃L[ℝ] τ → ℝ}
(hL : fderiv ℝ f a = ↑L) {s : Set (σ → ℝ)} (hs : s ∈ nhds a) :
∃ Θ,
↑Θ = f ∧
a ∈ Θ.source ∧
Θ.source ⊆ s ∧
TauCeti.IsSemialgebraicOn (↑Θ) Θ.source ∧
TauCeti.IsSemialgebraicOn (↑Θ.symm) Θ.target ∧
(∀ x ∈ Θ.source, ∀ (i : τ), TauCeti.IsNashAt (fun z => f z i) x) ∧
∀ y ∈ Θ.target, ∀ (i : σ), TauCeti.IsNashAt (fun z => ↑Θ.symm z i) y
Lean
Formalized in Tau Ceti as TauCeti.exists_openPartialHomeomorph_of_forall_isNashAt.
Sources
TheoremThom's lemma for delineations#
Suppose that at a point x of the base the derivative of
every member of the family is zero or a member. If every member has the same sign at two distinct
points t ≠ t' of the fiber over x, then no root function takes a value in [t, t'] at x.
TauCeti.Delineation.root_notMem_uIcc_of_sign_eval_eq.{u_1, u_3} {X : Type u_1} {ι : Type u_3}
[TopologicalSpace X] {P : ι → X → Polynomial ℝ} (D : TauCeti.Delineation P) {x : X}
(hder : ∀ (k : ι), Polynomial.derivative (P k x) = 0 ∨ ∃ l, P l x = Polynomial.derivative (P k x))
{t t' : ℝ} (htt' : t ≠ t')
(h :
∀ (k : ι),
SignType.sign (Polynomial.eval t (P k x)) = SignType.sign (Polynomial.eval t' (P k x)))
(i : Fin D.count) : D.root i x ∉ Set.uIcc t t'
Lean
Formalized in Tau Ceti as TauCeti.Delineation.root_notMem_uIcc_of_sign_eval_eq.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.