12
$\begingroup$

What is the simple test with exponential polynomials to determine whether $$f(x)=e^x+ax^2+bx+c$$ has a positive zero?

This was prompted by the question about discriminants here. We have an ineffective result, a partial result, and a result for a broader class of algorithms.

As an ineffective result: According to Wilkie's 1996 paper, there must be a list of exponential polynomials in $a,b,c$ whose signs will determine whether $f$ has a positive zero. However, that paper does not provide an effective algorithm. It might be possible to get a similar ineffective result more simply using compactness and some of the arguments below.

As a partial result: If $a=0$, then $f$ has a zero iff one of the following holds: \begin{align} &b>0 \\ &b=0\ \ \&\ \ c<0 \\ &b<0\ \ \&\ \ b + e^{1-c/b}<0 \end{align} The last of these comes from using calculus to find the minimum of $f$, evaluating $f$ there, and replacing the logs in the expression with exponentials.

As a result with a broader class of algorithms: We can test this for any algebraic $a,b,c$. Check for each positive rational $q$ if $$e^q+aq^2+bq+c<0$$ and check for each natural $n$ if $$\forall x(x>0\implies ax^2+bx+c+\sum^n_{k=0}x^k/k!\ge0)$$ We can test the first piece using the proof of the transcendence of $e$ (like this answer); if $f$ goes negative we will eventually verify that. We can test the second piece using Tarski-Seidenberg quantifier elimination; if $f$ is always positive we will eventually verify that. The third possibility, that $f$ is tangent to the $x$-axis, would imply that $f$ and $f'$ have a simultaneous zero, and we can rule that out by the Lindemann-Weierstrass theorem. However, this is an algorithm without an obvious time bound. And even if we convert each of the subtests above into a test via exponential polynomials, this doesn't give a single set of exponential polynomials which can be used for all $a,b,c$.

What is the single set of exponential polynomials in $a,b,c$ whose signs determine if $f$ has a positive zero?

$\endgroup$
2
  • 2
    $\begingroup$ If I remember correctly there are decision procedures for fragments of the theory of $\mathbb{R}_{\exp}$ that contain such sentences. See for example this: core.ac.uk/download/pdf/82722706.pdf or Theorem 1 of this sciencedirect.com/science/article/pii/S0021869316000247 $\endgroup$ Commented Mar 24, 2021 at 18:17
  • $\begingroup$ @ErikWalsberg, thanks. It looks like the first of those two papers, by McCallum and Weispfenning, would already be enough to cover my question. E.g. their first example on p. 13 is effectively looking for roots of $e^x-x^2$. $\endgroup$
    – user44143
    Commented Apr 1, 2021 at 1:38

1 Answer 1

5
$\begingroup$

First let's consider a simpler problem on testing whether $g(x) := e^x + ux + v$ has a zero in the given interval $(L,U]$. It does when one of the following cases takes place:

  • $g(L)<0$ and $g(U)\geq 0$;
  • $g(L)>0$ and $g(U)\leq 0$;
  • $g(L)\geq 0$ and $g(U)\geq 0$ and $u<0$ and $L<\log(-u)\leq U$ and $u(\log(-u)-1)+v \leq 0$.

Let $\text{TEST}(u,v,L,U)$ denotes testing these conditions and giving True (pass) / False (no pass) answer. To be on a safe side, we also let it return False when $L\geq U$ (i.e., when the given interval is empty).


Back to the original problem, we consider the case $a\ne 0$.

If $c<-1$, then $f(0)=1+c<0$, so the answer is Yes.

If $c\geq -1$ and $\neg \text{TEST}(2a,b,0,+\infty)$, then $f’$ has no positive zeroes, so $f$ must be increasing for $x\ge 0$, so the answer is No.

If $c\geq -1$ and $\text{TEST}(2a,b,0,+\infty)$ then let $z$ be a positive zero of $f’$. It remains to check whether $f(z)\leq 0$.

Since $0=f'(z)=e^{z} + 2az + b$, we have $$f(z) = -(2az+b) + az^2 + bz + c = az^2 + (b-2a)z + (c-b).$$ Let $D:=4a^2 + b^2 - 4ac$ be the discriminant of this quadratic, and let $s := \frac{2a-b-\sqrt{D}}{2a}$ and $t:= \frac{2a-b+\sqrt{D}}{2a}$ be its roots. We use these roots to teat whether $f’$ has a zero in the interval(s) where $z$ is positive and this quadratic is negative; if so, that root is $z$ and therefore $f(z)$ is negative, leading to a Yes.

Now there are four subcases:

  • If $D<0$ and $a<0$, then the quadratic is always negative, so the answer is Yes.

  • If $D<0$ and $a>0$, then the quadratic is always positive, so the answer is No.

  • If $D\ge 0$ and $a<0$, then let $ s_0:=\max(s,0)$. The answer is Yes iff $\text{TEST}(2a,b,0,t)$ or ($s_0>0$ and $f'(s_0)=0$) or $\text{TEST}(2a,b,s_0,+\infty)$.

  • If $D\geq 0$ and $a>0$, then let $s_0:=\max(s,0)$. The answer is Yes iff ($s_0>0$ and $f'(s_0)=0$) or $\text{TEST}(2a,b,s_0,t)$.

Remark. If numbers $a,b,c$ are algebraic (in particular, rational), then $f'(x)$ cannot have positive algebraic zeros, and thus conditions ($s_0>0$ and $f'(s_0)=0$) never hold and can be safely removed from the last two cases.

$\endgroup$
3
  • 1
    $\begingroup$ @MattF.: Thanks for streamlining my answer. As for the last two subcases, I'm not sure what exactly is unclear. Just as an example, if in last case $\text{TEST}(2a,b,s_0,t)$ is True, $f'(x)$ has a zero $x=z$ in the interval $(s_0,t]\subset (0,t]\cap (s,t]$. Then $z>0$ and $f(z)\leq 0$, implying the Yes answer. $\endgroup$ Commented Mar 23, 2021 at 3:42
  • 2
    $\begingroup$ Curiously, this leads to explicit expressions which are not exponential polynomials, but rather things like $s(\ln(-s)-1)+t\le 0$, which are expressions in $a,b,c$ with lots of divisions and square roots. We can convert the inequality with one $\ln$ into an inequality with one $\exp$, but there will still be square roots inside the $\exp$ that I don’t see how to eliminate. So if the best we can do is to formulate criteria as a mix of exponential and algebraic functions, that is a significant difference from the quantifier elimination for the reals without exponentiation. $\endgroup$
    – user44143
    Commented Mar 23, 2021 at 11:38
  • 1
    $\begingroup$ This looks good to me. I will wait for other answers until the bounty expires on the question linked at the beginning, and assuming I don't get any, I will accept this. In any case, if you like this sort of analysis, a decision procedure for the existential theory of the reals under exponentiation, and one whose correctness does not depend on Schanuel's conjecture, would be very nice. $\endgroup$
    – user44143
    Commented Mar 23, 2021 at 22:19

You must log in to answer this question.