ThmDex – An index of mathematical definitions, results, and conjectures.
P3254
Fix $\varepsilon > 0$. Since $f(t) \to 0$ as $t \to \infty$, then there exists $t_0 \in [0, \infty)$ such that $f(t) < \varepsilon / 2$ for all $t \geq t_0$. Choose $x \in [t_0, \infty]$ such that \begin{equation} \frac{1}{x} \int^{t_0}_0 f(t) \, d t < \frac{\varepsilon}{2} \end{equation} Applying results
(i) R4288:
(ii) R2112: Isotonicity of Riemann integral

we have \begin{equation} \begin{split} \left| \frac{1}{x} \int^x_0 f(t) \, d t \right| & = \frac{1}{x} \int^{t_0}_0 f(t) \, d t + \frac{1}{x} \int^x_{t_0} f(t) \, d t \\ & < \frac{\varepsilon}{2} + \frac{1}{x} \int^x_{t_0} \frac{\varepsilon}{2} \, d t \\ & = \frac{\varepsilon}{2} + \frac{\varepsilon}{2 x} \int^x_{t_0} \, d t \\ & < \frac{\varepsilon}{2} + \frac{\varepsilon}{2 x} \int^x_0 \, d t \\ & = \frac{\varepsilon}{2} + \frac{\varepsilon}{2 x} x \\ & = \frac{\varepsilon}{2} + \frac{\varepsilon}{2} \\ & = \varepsilon \end{split} \end{equation} Since $\varepsilon > 0$ was arbitrary, we have $\frac{1}{x} \int^x_0 f(t) \, d t \to 0$ as $x \to \infty$. $\square$