Existence of adapted cylindrical algebraic decompositions

For every finite set F of real polynomials in n variables there is a cylindrical algebraic decomposition of ℝ ^ n adapted to F: every member of F is sign-invariant on every cell (TauCeti.exists_isCAD_signInvariant).

The proof is by induction on n. Single out the first variable with MvPolynomial.finSuccEquiv and take an adapted CAD of ℝ ^ n for the Collins projection of the resulting family. By Collins delineability, the family has a delineation over each cell. Its stacks give the CAD of ℝ ^ (n + 1).

These stacks are semialgebraic by TauCeti.Delineation.isSemialgebraicStack: their sections and sectors are described by membership in the shared distinct root set and the number of shared roots below the height. No derivatives need to be added to the input family. Nullified members, repeated roots, the empty family and stacks without sections are included.

Main results

• TauCeti.exists_isCAD_signInvariant: every finite set of polynomials has an adapted CAD.
• TauCeti.IsSemialgebraic.exists_isCAD_subset_or_disjoint: every semialgebraic set is a union of cells of some CAD.
• TauCeti.HasSemialgebraicProjections ℝ: projection closure, the Tarski–Seidenberg theorem. Forgetting the coordinate 0 maps semialgebraic subsets of ℝ ^ (n + 1) to semialgebraic subsets of ℝ ^ n (TauCeti.HasSemialgebraicProjections.isSemialgebraic_image_tail). A semialgebraic set is a sign condition on finitely many polynomials, so it is a union of cells of an adapted CAD, and its projection is a union of cells of the projected CAD. With this instance the results of TauCeti.Geometry.RealAlgebraic.Semialgebraic.QuantifierElimination and TauCeti.Geometry.RealAlgebraic.Semialgebraic.Image apply to ℝ.
• TauCeti.exists_finite_image_sign_eval_eq: finitely many sample points realize every sign vector of a finite family of polynomials.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Section 5.1 and Chapter 11 (cylindrical decomposition).

theorem TauCeti.exists_isCAD_signInvariant {n : ℕ} (F : Finset (MvPolynomial (Fin n) ℝ)) : ∃ (𝒞 : Set (Set (Fin n → ℝ))), IsCAD n 𝒞 ∧ ∀ f ∈ F, ∀ E ∈ 𝒞, SignInvariant (fun (x : Fin n → ℝ) => (MvPolynomial.eval x) f) E

Existence of adapted cylindrical algebraic decompositions. For every finite set F of real polynomials in n variables there is a cylindrical algebraic decomposition of ℝ ^ n on each cell of which every member of F is sign-invariant.

theorem TauCeti.IsSemialgebraic.exists_isCAD_subset_or_disjoint {n : ℕ} {s : Set (Fin n → ℝ)} (hs : IsSemialgebraic s) : ∃ (𝒞 : Set (Set (Fin n → ℝ))), IsCAD n 𝒞 ∧ ∀ E ∈ 𝒞, E ⊆ s ∨ Disjoint E s

Decompositions adapted to a semialgebraic set. For a semialgebraic subset s of ℝ ^ n there is a cylindrical algebraic decomposition of ℝ ^ n each cell of which lies in s or misses it, so that s is the union of the cells it contains (TauCeti.IsCAD.sUnion_sep_subset).

instance TauCeti.instHasSemialgebraicProjectionsReal : HasSemialgebraicProjections ℝ

The Tarski–Seidenberg theorem. The projection of a semialgebraic subset of ℝ ^ (n + 1) forgetting the coordinate 0 is semialgebraic. So quantifier elimination, the identification of semialgebraic sets with definable sets, and the image and composition laws of semialgebraic functions, which assume HasSemialgebraicProjections, hold over ℝ unconditionally.

theorem TauCeti.exists_finite_image_sign_eval_eq {n : ℕ} {ι : Type u_1} [Finite ι] (p : ι → MvPolynomial (Fin n) ℝ) : ∃ (T : Set (Fin n → ℝ)), T.Finite ∧ (fun (x : Fin n → ℝ) (i : ι) => SignType.sign ((MvPolynomial.eval x) (p i))) '' T = Set.range fun (x : Fin n → ℝ) (i : ι) => SignType.sign ((MvPolynomial.eval x) (p i))

Sample points. For finitely many real polynomials p i in n variables there is a finite set of points of ℝ ^ n at which the p i take every sign vector that they take on ℝ ^ n.