From https://mathworld.wolfram.com/CylindricalAlgebraicDecomposition.html it is said that:
Define a cell in ${\mathbb{R}^1}$ as an open interval or a point. A cell in ${\mathbb{R}^{k + 1}}$ then has one of two forms:
Form 1: $\left\{ {\left( {x,y} \right):x \in C,f\left( x \right) < y < g\left( x \right)} \right\}$
Form 2: $\left\{ {\left( {x,y} \right):x \in C,y = f\left( x \right)} \right\}$
Where $x = \left\{ {{x_1},{x_2},...{x_k}} \right\}$ and $C$ is a cell in ${\mathbb{R}^{k}}$.
$f$ and $g$ are either:
1/ Continuous function on $C$ such that for some polynomials $F$ and $G$, $F\left( {x,f\left( x \right)} \right) = 0$ and $G\left( {x,g\left( x \right)} \right) = 0$
2/ $\pm \infty$ and $f\left( x \right) < g\left( x \right)$ for all $x \in C$
A cylindrical algebraic decomposition of $S \subset {\mathbb{R}^n}$ is a representation of $S$ as a finite union of disjoint cells. Let $F$ be finite set of polynomials in $n$ variables.
A cylindrical algebraic decomposition of $S \subset {\mathbb{R}^n}$ is said to be $F$-invariant if each of the polynomials from $F$ has a constant sign on each cell of the decomposition.
An example of the decomposition of the decomposition of ${x^2} + {y^2} + {z^2} < 1$ is:
$\left\{ {\begin{array}{*{20}{c}} {\begin{array}{*{20}{c}} { - 1 < x < 1} \\ { - \sqrt {1 - {x^2}} < y < \sqrt {1 - {x^2}} } \\ { - \sqrt {1 - {x^2} - {y^2}} < z < \sqrt {1 - {x^2} - {y^2}} } \end{array}}&{\begin{array}{*{20}{c}} {\left( 1 \right)} \\ {\left( 2 \right)} \\ {\left( 3 \right)} \end{array}} \end{array}} \right.$
1/ From the result of the example does it mean that (1),(2) and (3) are the three cell of this decomposition ?
2/ In this example does it mean that $S$ is ${x^2} + {y^2} + {z^2} < 1$ , what is $F$ and what does it mean by $F$-invariant ?
3/ From what I know the Cylindrical Algebraic Decomposition could be thought as some form of quantifier elimination. Then does that mean the result in (1)(2)(3) is a quantifier free of this statement:
$\exists x,y,z \in {\mathbb{R}^3},{x^2} + {y^2} + {z^2} < 1$
4/ Is there anyway to rigorous proof that integrating over (3)(2)(1) yield the spherical volume of ${x^2} + {y^2} + {z^2} < 1$ ? By inspection it seem that way.
Please help me !
Thank you for your enthusiasm !
1/ Three cells are specified here. The first cell, which we will call $C_1$, is in $\Bbb{R}^1$ and is given by (1), in Form 1, and is $(-1,1) \subseteq \Bbb{R}$.
The second cell, which we will call $C_2$, is in $\Bbb{R}^2$ (so take $k = 1$ for this cell), has $C = C_1$, and is given by (2) in Form 1, $$ \{(x,y) : x \in C_1, -\sqrt{1-x^2} < y < \sqrt{1-x^2}\} \text{.} $$
The third cell is in $\Bbb{R}^3$ (so take $k = 2$) for this cell), has $C = C_2$, and is given by (3) in Form 1, $$ \{((x,y),z) : (x,y) \in C_2, -\sqrt{1 - x^2 - y^2} < z < \sqrt{1-x^2-y^2} \text{.} $$
2/ Yes, $S$ is the set in $\Bbb{R}^3$ given by $x^2 + y^2 + z^2 < 1$.
Regarding $F$-invariance... The use of $F$ in the specification of the cell forms is unrelated to the use of $F$ in $F$-invariance.
In the first cell, we need a polynomial $\hat{F}_1(x)$ that has constant sign on $C_1$. An example if $\hat{F}_1(x) = x^2 - 1$. Notice that this polynomial comes directly from $x^2 + y^2 + z^2 < 1$ by ignoring the $y$ and $z$ terms, $x^2 < 1$, then moving everything to the left: $x^2 - 1 < 0$. This means $\hat{F}_1$ is negative exactly on $C_1$. However, to match the usage in the example, we should negate this: $F_1(x) = 1 - x^2$. Notice that this is exactly the form of $x$ that appears in the bounds of the inequality in the second cell. In particular, $$ -F_1(x) < y^2 < F_1(x) $$ (The existence of these polynomial relations for the boundary of $C_2$ in terms of $F_1(x)$ and $y$ is the content of the text "$F(x,f(x)) = 0$ and $G(x,g(x)) = 0$".)
Continuing this pattern, $F_2(x,y) = 1 - x^2 - y^2$ is positive exactly on $C_2$ and $F_3(x,y,z) = 1 - x^2 - y^2 - z^2$ is positive exactly on $S$. Then the given example CAD is $\{F_1, F_2, F_3\}$-invariant.
3/ Not necessarily. If the quantifier order and the decomposition order do not match, a CAD may not be very helpful in eliminating quantifiers.
This particular example is easy, though since the variables are quantified in the same order as the variable order of the CAD. It is trivial to determine that there is an $x$ satisfying (1). Then, this choice of $x$ gives an interval of choices for $y$ in (2). Then a choice of $y$ in that interval gives an interval of choices for $z$. Notice that this is easy when the variable order $x$, $y$, $z$ is the same as the quantifier order. If we quantify on $z$ first, this CAD is not particularly helpful. If you construct a new CAD with variable order matching quantifier order, this is easy.
More discussion of quantification and elimination is present in http://www3.risc.jku.at/publications/download/risc_4231/s65kauers.pdf (Also presented: a nontrivial example and an example of how much changes when you replace the present example of the open unit ball with the closed unit ball.)
4/ Yes. This is immediate. The volume $S$ is exactly given by the CAD, so the question you ask is equivalent to "is integration over $S$ given by this one inequality the same as integration over $S$ given by this CAD?" Yes; they're both $S$.