Solving polynomial inequalities over spaces of convex sets and applications
Abstract
We develop a symbolic elimination theory for finite systems of recursive containment inequalities whose unknowns are convex subsets of a finite-dimensional real vector space. The right-hand sides are formal expressions generated from variables and parameters by convex linear combinations, finite union, and a positive geometric join encoding strict convex combinations. We prove that every parameter assignment has a unique smallest convex-set-valued solution and give a finite Gaussian-elimination-type procedure that eliminates the unknowns while preserving this solution and produces parameter-only expressions for its coordinate sets. More generally, let $\mathcal B$ be a family of subsets containing $\emptyset$ and closed under finite unions, nonnegative dilation, Minkowski sums, positive geometric joins, and convex hulls. If all parameter sets lie in $\mathcal B$, then every coordinate set of the smallest solution lies in $\mathcal B$; when these operations are effective, so is the resulting description. In particular, if the parameters are finite unions of hemihedra---where a hemihedron is a bounded convex semi-linear set, equivalently a convex finite union of relative interiors of polytopes---then each coordinate set is a hemihedron and admits a quantifier-free semi-linear description. We apply this theory to lamination hulls. For \[ V=U\oplus\bigoplus_{i=1}^{k}W_i,\qquad \dim W_i=1,\qquad Λ=\bigcup_{i=1}^{k}(U+W_i), \] we prove that the lamination hull $G_Λ^{(\infty)}(S)$ of every finite $S\subset V$ is semi-algebraic and effectively computable by a quantifier-free formula over the reals.
Disclosure
“nding to our example system. Declaration of generative AI and AI-assisted technologies in the writing process During the preparation of this work, the authors used OpenAI’s ChatGPT, accessed through a ChatGPT Pro subscription, and Anthropic’s Claude, accessed through a Claude Max subscription, solely to assist with proofreading and the supplementary verification of mathematical arguments. The authors indepen- dently reviewed and verified all suggestions and outputs produced by these t”
PDF page 55
- Classification
- Proof ideas or individual proof-step assistance
- Multiplier
- 8
- Verified
Structural counts
Count notes
- Source counts use the expanded primary TeX file arxiv-main.tex.
- Appendix pages include the first PDF page with an explicit Appendix heading through the final page.