Show that $\cos(x) \le e^{-x^2/2}$ for $0 \le x \lt \pi/2$. Show that $\cos(x) \le e^{-x^2/2}$ for $0 \le x \lt \pi/2$.
This inequality came up
in my solution to
Show that the sequence $\sum\limits_{k=1}^n\cos\left(\frac kn\right)^{2n^2/k}$ converges.
This is in the category of
"There should be
a number of ways
to prove this."
Here is one way
I came up with.
I am interested in seeing
how many others
there are.
$(\ln(\cos(x))'
=-\tan(x)
\le -x$
for $0 \le x \lt \pi/2$.
Integrating from $0$ to $x$,
since the two sides are $0$
at $x=0$,
$\ln(\cos(x))
\le -x^2/2$
so
$\cos(x)
\le e^{-x^2/2}
$.
 A: Presumably we all agree that both of these functions are positive on $[0,\pi/2)$. It therefore suffices to show that
$$ e^{x^2/2}\cos{x} \leq 1, $$
or since the logarithm is increasing,
$$ \frac{1}{2}x^2 - \log{\cos{x}} = \log{(e^{x^2/2}\cos{x})} \leq 0. $$
But the derivative of the left-hand side is $x-\tan{x}$, and this is easy to prove nonpositive in the range we care about.
So starting from $$t-\tan{t} \leq 0,$$ and integrating from $0$ to $x$ gives
$$ \frac{1}{2}x^2 - 0 - \log{\cos{x}} + \log{1} \leq 0, $$
which is what we wanted.

Alternative:
It suffices to show that
$$ \arccos{y} < \sqrt{-2\log{y}} $$
for $0<y<1$. Differentiating, and considering the integral from $x$ to $1$, it is enough to show that
$$ -\frac{1}{\sqrt{1-y^2}} > -\frac{1}{\sqrt{-2y^2\log{y}}}, $$
or rearranging,
$$ y^{-2}-1 > -\log{(y^{-2})}. $$
But this is a standard logarithm inequality that follows from e.g. concavity.

Is there a way to do this kind of proof forwards?
$$ e^{-x^2/2} \geq \left( 1 - \frac{x^2}{4} \right)^2, $$
so it suffices to show that $\cos{x} \leq ( 1 - x^2/4)^2 $. It's easy enough to see that
$$ \cos{x} = 1-2\sin{\tfrac{1}{2}x} \geq 1-\frac{x^2}{2}. $$
Differentiating $( 1 - x^2/4)^2-\cos{x}$ twice gives
$$ \cos{x} - 1 + \frac{3}{4}x^2 \geq \frac{x^2}{4} \geq 0, $$
and integrating this twice gives the result.
It would be interesting to construct a "calculus-free" proof of the inequality $\cos{x} \geq ( 1 - x^2/4)^2 $, based only on $\sin{x} \leq x$ and the like.
A: For $0\le t\le 1$, we have
$$\sin t\ge t-{t^3\over6}= t\left(1-{t^2\over2}+{t^2\over3}\right)\ge t\left(1-{t^2\over2}+{t^4\over24}\right)\ge te^{-t^2/2}$$
and thus
$$\int_0^x\sin t\,dt\ge\int_0^xte^{-t^2/2}\,dt$$
for all $0\le x\le 1$.  
On the other hand, it's easy to see that $te^{-t^2/2}$ attains a maximum at $t=1$ and is decreasing for $t\gt1$.  Since $\sin1\approx0.84\gt.6065\approx1/\sqrt e$, we have
$$\int_1^x\sin t\,dt\ge\int_1^xte^{-t^2/2}\,dt$$
for all $1\le x\le\pi/2$ (since $\sin t$ increases while $te^{-t^2/2}$ decreases in that range). It follows that
$$1-\cos x=\int_0^x\sin t\,dt\ge\int_0^xte^{-t^2/2}\,dt=1-e^{-x^2/2}$$
for all $0\le x\le \pi/2$.
A: By Taylor's expansion
$$\cos(x) \le 1-\frac{x^2}2+\frac{x^4}{24} \le 1-\frac{x^2}2+\frac{x^4}{8}-\frac{x^6}{48} \le e^{-x^2/2}$$
indeed
$$1-\frac{x^2}2+\frac{x^4}{24} \le 1-\frac{x^2}2+\frac{x^4}{8}-\frac{x^6}{48}\iff \frac{x^4}{12}-\frac{x^6}{48}\ge 0 \iff x^4(4-x^2)\ge 0$$ 
A: The function $\tan x$ has a Maclaurin series with positive coefficients, convergent for $|x|<\pi/2$, see series . Its integral $\log(\sec x)$ also has a series with positive coefficients
$$\log(\sec x)=\frac{x^2}{2} + \frac{x^4}{12} + \frac{x^6}{45} + \frac{17 x^8}{2520} + \frac{31 x^{10}}{14175}+\mathcal{O}(x^{12})$$
We conclude
$$\cos x = \exp(-\frac{x^2}{2} - \frac{x^4}{12} - \frac{x^6}{45}-\cdots )$$
for $|x|<\pi/2$, so truncating at any point will give an inequality, for instance
$$\cos x \le \exp(-\frac{x^2}{2} - \frac{x^4}{12} - \frac{x^6}{45})$$ for $|x|\le |3\pi/2|$. The inequality holds in fact on $[-\delta, \delta]$, where $\delta$ is the smallest positive root of $\cos(x)=\exp(-\frac{x^2}{2} - \frac{x^4}{12} - \frac{x^6}{45})$, a number $>3\pi/2$ but very close to it.
A: Does proof by brute calculation count?
We wish to show $f(x) = \cos (x) \leq e^{-x^2/2} = g(x)$ for $x \in [0, \pi/2)$. 

Since the functions are equal at $x=0$, showing that $f'(x) \leq g'(x)$ on the interval should suffice as
$$f(a) = \int_{0}^{a}f'(x)\, dx \leq \int_{0}^{a}g'(x)\, dx = g(a)$$
(We use this fact twice.) 

Now, we would wish to show that (after multiplying by $x \neq 0$)
$$\frac{\sin(x)}{x} \geq e^{-\frac{x^2}{2}}$$
Utilizing the same lemma, it would be great if
$$\frac{\sin (x) - x\cos (x)}{x^3} \leq e^{-\frac{x^2}{2}}$$
for $x \in [0, \pi/2)$. But this is obviously true, as the LHS bounded above by $1/3$, and the RHS is bounded below by $\exp(-\pi^2/8)$, which is true by brute calculation. (You can also try showing $3^{8/9} < e$)
