Balls, closures and interiors of real semialgebraic sets

This file shows that the basic metric and topological constructions on the real coordinate space σ → ℝ, for a finite index type σ, preserve semialgebraicity.

• Open and closed balls are semialgebraic, both for the sup norm, which is the norm Mathlib puts on σ → ℝ, and for the Euclidean norm of EuclideanSpace ℝ σ. In particular every point has arbitrarily small open semialgebraic neighbourhoods of either kind.
• The closure, interior and frontier of a semialgebraic set are semialgebraic.
• A semialgebraic subset of ℝ ^ n with empty interior is nowhere dense. It is the union of the cells of an adapted cylindrical algebraic decomposition that it contains, and these are locally closed with empty interior, hence nowhere dense. This fails for arbitrary sets, as the rationals in ℝ show.

The ball statements only use the polynomial description of the two norms. The closure statement uses the Tarski–Seidenberg theorem in the form of projection closure (TauCeti.HasSemialgebraicProjections ℝ): a point x lies in closure s exactly when for every ε > 0 there is y ∈ s with dist x y < ε, and the two quantifiers are eliminated by two projections and a complement. Interiors and frontiers then follow from closures by complements and differences.

Main results

• TauCeti.isSemialgebraic_setOf_dist_eval_lt, TauCeti.isSemialgebraic_setOf_dist_eval_le: the locus where the sup distance between two polynomial maps is bounded by a polynomial is semialgebraic.
• TauCeti.isSemialgebraic_ball, TauCeti.isSemialgebraic_closedBall: sup-norm balls.
• TauCeti.isSemialgebraic_preimage_toLp_ball, TauCeti.isSemialgebraic_preimage_toLp_closedBall: Euclidean balls, read in the coordinates σ → ℝ.
• TauCeti.IsSemialgebraic.closure, TauCeti.IsSemialgebraic.interior, TauCeti.IsSemialgebraic.frontier.
• TauCeti.IsSemialgebraic.setOf_mem_interior_fiber, TauCeti.IsSemialgebraic.setOf_fiber_interior_nonempty: interiors taken separately in the fibers of a semialgebraic family, and the parameters where these interiors are nonempty.
• TauCeti.IsSemialgebraic.isNowhereDense_iff: a semialgebraic set is nowhere dense exactly when its interior is empty.

References

• J. Bochnak, M. Coste, and M.-F. Roy, Real Algebraic Geometry, Ergebnisse der Mathematik und ihrer Grenzgebiete 36, Springer (1998), Proposition 2.2.2.
• S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Section 3.1.

Balls

theorem TauCeti.isSemialgebraic_setOf_dist_eval_lt {σ : Type u_1} {τ : Type u_2} [Fintype σ] (p q : σ → MvPolynomial τ ℝ) (r : MvPolynomial τ ℝ) : IsSemialgebraic {z : τ → ℝ | (dist (fun (i : σ) => (MvPolynomial.eval z) (p i)) fun (i : σ) => (MvPolynomial.eval z) (q i)) < (MvPolynomial.eval z) r}

The locus where the sup distance between two polynomial maps is less than the value of a polynomial is semialgebraic.

theorem TauCeti.isSemialgebraic_setOf_dist_eval_le {σ : Type u_1} {τ : Type u_2} [Fintype σ] (p q : σ → MvPolynomial τ ℝ) (r : MvPolynomial τ ℝ) : IsSemialgebraic {z : τ → ℝ | (dist (fun (i : σ) => (MvPolynomial.eval z) (p i)) fun (i : σ) => (MvPolynomial.eval z) (q i)) ≤ (MvPolynomial.eval z) r}

The locus where the sup distance between two polynomial maps is at most the value of a polynomial is semialgebraic.

theorem TauCeti.isSemialgebraic_ball {σ : Type u_1} [Fintype σ] (x : σ → ℝ) (r : ℝ) : IsSemialgebraic (Metric.ball x r)

An open ball for the sup norm on σ → ℝ is semialgebraic.

theorem TauCeti.isSemialgebraic_closedBall {σ : Type u_1} [Fintype σ] (x : σ → ℝ) (r : ℝ) : IsSemialgebraic (Metric.closedBall x r)

A closed ball for the sup norm on σ → ℝ is semialgebraic.

theorem TauCeti.isSemialgebraic_preimage_toLp_ball {σ : Type u_1} [Fintype σ] (x : EuclideanSpace ℝ σ) (r : ℝ) : IsSemialgebraic (WithLp.toLp 2 ⁻¹' Metric.ball x r)

An open ball of the Euclidean space EuclideanSpace ℝ σ, read in the coordinates σ → ℝ, is semialgebraic.

theorem TauCeti.isSemialgebraic_preimage_toLp_closedBall {σ : Type u_1} [Fintype σ] (x : EuclideanSpace ℝ σ) (r : ℝ) : IsSemialgebraic (WithLp.toLp 2 ⁻¹' Metric.closedBall x r)

A closed ball of the Euclidean space EuclideanSpace ℝ σ, read in the coordinates σ → ℝ, is semialgebraic.

Closures, interiors and frontiers

theorem TauCeti.IsSemialgebraic.closure {σ : Type u_1} [Finite σ] {s : Set (σ → ℝ)} (hs : IsSemialgebraic s) : IsSemialgebraic (_root_.closure s)

The closure of a semialgebraic subset of σ → ℝ is semialgebraic.

theorem TauCeti.IsSemialgebraic.interior {σ : Type u_1} [Finite σ] {s : Set (σ → ℝ)} (hs : IsSemialgebraic s) : IsSemialgebraic (_root_.interior s)

The interior of a semialgebraic subset of σ → ℝ is semialgebraic.

theorem TauCeti.IsSemialgebraic.frontier {σ : Type u_1} [Finite σ] {s : Set (σ → ℝ)} (hs : IsSemialgebraic s) : IsSemialgebraic (_root_.frontier s)

The frontier of a semialgebraic subset of σ → ℝ is semialgebraic.

Interiors in families

theorem TauCeti.IsSemialgebraic.setOf_mem_interior_fiber {σ : Type u_1} {τ : Type u_2} [Finite τ] {s : Set (σ ⊕ τ → ℝ)} (hs : IsSemialgebraic s) : IsSemialgebraic {z : σ ⊕ τ → ℝ | z ∘ Sum.inr ∈ _root_.interior {y : τ → ℝ | Sum.elim (z ∘ Sum.inl) y ∈ s}}

Taking the interior separately in each fiber of a semialgebraic family preserves semialgebraicity. The parameters need not have finitely many coordinates.

theorem TauCeti.IsSemialgebraic.setOf_fiber_interior_nonempty {σ : Type u_1} {τ : Type u_2} [Finite τ] {s : Set (σ ⊕ τ → ℝ)} (hs : IsSemialgebraic s) : IsSemialgebraic {x : σ → ℝ | (_root_.interior {y : τ → ℝ | Sum.elim x y ∈ s}).Nonempty}

The parameters whose fiber has nonempty interior form a semialgebraic set.

Nowhere dense semialgebraic sets

theorem TauCeti.IsSemialgebraic.isNowhereDense_iff {n : ℕ} {s : Set (Fin n → ℝ)} (hs : IsSemialgebraic s) : IsNowhereDense s ↔ _root_.interior s = ∅

A semialgebraic set is nowhere dense exactly when its interior is empty.