Proving $1-\exp(-4x^2/ \pi) \ge \text{erf}(x)^2$

Question

This is a follow-up to this question. I came across a tighter potential bound and checked it numerically for $0\le x\le 5$. I think it holds for all positive $x$, can anyone see a proof?

$$1-\exp(-4x^2/ \pi) \ge \text{erf}(x)^2$$

Note: using analysis for previous question you can show that $1-\exp(-k x^2)$ is an upper bound on $\text{erf}(x)^2$ for $k=2$ and a lower bound when $k=1$. The factor $k=4/\pi$ comes out when numerically searching for tightest upper bound. Not only does it seem to give an upper bound, but it also tracks $\text{erf}(x)^2$ very closely.

Dashed graph below is $\text{erf}(x)^2$, red is $1-\exp(-k x^2)$ for $k=4/\pi$, other two graphs are for $k=1$ and $k=2$

Answer 1

As before we consider

$$\text{erf}(x)^2={4\over \pi}\int_0^x\int_0^x \exp{-(s^2+t^2)}\ ds \ dt\,.$$

Now compare this with the same over the area which is given by the quarter of a circle of radius $\displaystyle \frac{2x}{\sqrt{\pi}}$. The area of this is same as the area of the square of side $x$.

Since $\displaystyle e^{-(s^2 + t^2)}$ decreases as $\displaystyle s^2 + t^2$ increases, we are done!

The integral over the non-common area for the quarter circle is greater than the integral over the non-common area of the square (which lies outside the circle and so $\displaystyle s^2 + t^2$ is higher in that region).

Answer 2

Alternative proof:

It suffices to prove that, for $x > 0$, $$\sqrt{1 - \mathrm{e}^{-4x^2/\pi}} - \frac{2}{\sqrt{\pi}}\int_0^x \mathrm{e}^{-t^2} \mathrm{d} t \ge 0.$$ Denote LHS by $f(x)$. We have $$f'(x) = \frac{4x \mathrm{e}^{-4x^2/\pi}}{\pi\sqrt{1 - \mathrm{e}^{-4x^2/\pi}}} - \frac{2}{\sqrt{\pi}}\mathrm{e}^{-x^2}.$$

Fact 1: $f'(x) = 0$ has exactly one positive real solution, denoted by $x_0$.
(The proof is given at the end.)

By Fact 1 and $f'(1) > 0$ and $f'(2) < 0$, we have $f'(x) > 0$ on $(0, x_0)$ and $f'(x) < 0$ on $(x_0, \infty)$. Thus, $f(x)$ is strictly increasing on $(0, x_0)$ and strictly decreasing on $(x_0, \infty)$. Also, $f(0) = 0, f(\infty) = 0$. Thus, $f(x) > 0$ on $(0, \infty)$. We are done.

---

Proof of Fact 1:

For $x > 0$, we have \begin{align} f'(x) = 0 \quad &\Longleftrightarrow \quad \left(\frac{4x \mathrm{e}^{-4x^2/\pi}}{\pi\sqrt{1 - \mathrm{e}^{-4x^2/\pi}}}\right)^2 = \left(\frac{2}{\sqrt{\pi}}\mathrm{e}^{-x^2}\right)^2\\[6pt] \quad &\Longleftrightarrow \quad \frac{4x^2}{\pi} = \mathrm{e}^{8x^2/\pi} \mathrm{e}^{-2x^2}(1 - \mathrm{e}^{-4x^2/\pi}) \\[6pt] \quad &\Longleftrightarrow \quad \frac{4x^2}{\pi} + \mathrm{e}^{(1-\pi/2)\cdot \frac{4x^2}{\pi}} = \mathrm{e}^{(2-\pi/2)\cdot \frac{4x^2}{\pi}}\\ &\Longleftrightarrow \quad u + \mathrm{e}^{(1-\pi/2)u} = \mathrm{e}^{(2-\pi/2)u}, \quad u = \frac{4x^2}{\pi}. \end{align}

Let $g(u) = u + \mathrm{e}^{(1-\pi/2)u} - \mathrm{e}^{(2-\pi/2)u}$. We have $$g'(u) = 1 + (1-\pi/2)\mathrm{e}^{(1-\pi/2)u} - (2-\pi/2)\mathrm{e}^{(2-\pi/2)u}$$ and $$g''(u) = (1-\pi/2)^2\mathrm{e}^{(1-\pi/2)u} - (2-\pi/2)^2\mathrm{e}^{(2-\pi/2)u}.$$

Let $u_0 = 2\ln (\pi - 2) - 2\ln (4 - \pi)$. It is easy to prove that $g''(u) > 0$ on $(0, u_0)$, and $g''(u) < 0$ on $(u_0, \infty)$.

Thus, $g'(u)$ is strictly increasing on $(0, u_0)$, and strictly decreasing on $(u_0, \infty)$. Also, $g'(0) = 0$ and $g'(\infty) = -\infty$. Thus, $g'(u) = 0$ has exactly one positive real solution, denoted by $u_1$. Thus, $g'(u) > 0$ on $(0, u_1)$, and $g'(u) < 0$ on $(u_1, \infty)$. Thus, $g(u)$ is strictly increasing on $(0, u_1)$, and strictly decreasing on $(u_1, \infty)$. Also, $g(0) = 0$ and $g(\infty) = -\infty$. Thus, $g(u) = 0$ has exactly one positive real solution. As a result, $f'(x) = 0$ has exactly one positive real solution. We are done.

Answer 3

This is one of the many results that keep being periodically rediscovered. The bound, together with a less accurate lower bound of the same form, was given in a report by J.T. Chu (1954; On bounds for the normal integral). It was noted in the report that the upper bound had previously been obtained independently by G. Polya and J.D. Williams. Both used the nice geometrical argument that has been here expounded.