I come across a system of polynomial equations. Although I can solve it by Mathematica (numerically), I wonder whether it is possible to prove this root indeed exists. Any general method to do it? For example, $f(x_1,x_2)=0$ ; $g(x_1,x_2)=0$ ; $f$ and $g$ are polynomials of $x_1$ and $x_2$, and I compute an approximate root $(x_1^*,x_2^*)$ by some numerical method. How can I show there indeed exists a root around this approximate calculated root? I just wonder whether there exist some general theories in doing so.
$\begingroup$
$\endgroup$
3
-
$\begingroup$ Real root or complex root? How many equations/unknowns? $\endgroup$– Igor RivinCommented Oct 6, 2016 at 10:54
-
$\begingroup$ real and two equations with two unknowns $\endgroup$– stephenkkCommented Oct 6, 2016 at 11:19
-
1$\begingroup$ Could you perhaps tell us the system? In some cases you can guess the exact algebraic solution after you solved the system to high accuracy and then check the algebraic solution in exact arithmetic. Sometimes Smale's Alpha Theory helps. $\endgroup$– Moritz FirschingCommented Oct 6, 2016 at 13:04
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
2
The magic words are: Cylindrical Algebraic Decomposition.
answered Oct 6, 2016 at 11:36
-
$\begingroup$ I have the impression that in the zero-dimensional case that Grobner bases plus picking out the real solutions works better. $\endgroup$– arsmathCommented Oct 6, 2016 at 13:59
-
$\begingroup$ @arsmath I am not sure, but it is certainly true that the zero-dimensional case is special... $\endgroup$ Commented Oct 6, 2016 at 14:33
$\begingroup$
$\endgroup$
2
For polynomials you can, though the details are technical. For a single univariate polynomial you can use the technique of Sturm sequences to find out how many real roots there are, and put bounds on the roots. For a system of that has finitely-many solutions, you can use the theory of Grobner bases to find all complex solutions, and then there are special techniques to pick out the real solutions. Sturmfels' book has details in chapter 4.
In theory you can do it even if you have infinitely many solutions, though it's much much harder. This goes under the name of Tarski's quantifier elimination for real closed fields.
-
$\begingroup$ The cylindrical algebraic decomposition mentioned by Igor Rivin is a more computationally efficient quantifier elimination algorithm than Tarski's. $\endgroup$ Commented Oct 7, 2016 at 2:51
-
$\begingroup$ I used to be in computer algebra, and back then people used "quantifier elimination" for any algorithm to decide the theory of real closed fields, including CAD. That was a while ago, so maybe that usage as died out, or maybe I hung out with a bunch of weirdos. (It was only a long time later that I learned that "quantifier elimination" was a general concept in model theory.) $\endgroup$– arsmathCommented Oct 7, 2016 at 5:59