Can anyone see a nice way to prove the following for $0\le x \le 1$?
$$\sqrt{1-x^2}\ge \operatorname{erf}(\sqrt{-\log x})$$
$\operatorname{erf}$ is defined as
$$\operatorname{erf}(z) = \frac{2}{\sqrt{\pi}}\int_{0}^{z} e^{-t^2} \, dt$$
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this communityLet $y = \sqrt{-\log x}$. Then the inequality reduces to $\text{erf}(y) \leq \sqrt{(1-e^{-2y^2})}$ or equivalently $\text{erf}^2(y) + e^{-2y^2} \leq 1$. Now $\text{erf}^2(y)$ can be written as a double integral $\text{erf}^2(y) = \frac{4}{\pi} \int_{0}^y \int_{0}^{y} e^{- (a^2+b^2)} da db$ (As Qiaochu Yuan points out, the functions involved are well behaved and the double integral is well defined). Replace the area of integration from the square of side $y$ in the first quadrant to a quarter-circle of radius $y\sqrt{2}$ in the first quadrant and switch to polar co-ordinates. This would give the inequality $\text{erf}^2(y) \leq 1-e^{-2y^2}$ which is what we wanted.