Characteristic-function tail bound (source code)

= Characteristic-function tail bound
{title2=$\mu(|y|\ge\lambda)\le\frac{\lambda}{1-\sin1}\int_0^{1/\lambda}(1-\operatorname{Re}\phi(u))du$}

Average $1-\cos(uy)$ over $0\le u\le1/\lambda$. Multiplication by $\lambda$ gives $1-\sin(y/\lambda)/(y/\lambda)$, with value zero at $y=0$. This is at least $1-\sin1$ when $|y|\ge\lambda$. <Tonelli's theorem> then gives the displayed bound for a <probability measure> with <characteristic function> $\phi$. The bound converts control of the <characteristic function> near zero into <tightness of probability measures> and is useful in proving the <Lévy continuity theorem>.