ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4743 on D4650: Vanishing function
Riemann integral average of vanishing unsigned basic real function vanishes
Formulation 0
Let $f : [0, \infty) \to [0, \infty)$ be an D4367: Unsigned real function such that
(i) $f$ is a D1760: Riemann integrable real function on $[0, b]$ for every $b \in [0, \infty)$
(ii) \begin{equation} \lim_{t \to \infty} f(t) = 0 \end{equation}
Then \begin{equation} \lim_{x \to \infty} \frac{1}{x} \int^x_0 f(t) \, d t = 0 \end{equation}
Proofs
Proof 0
Let $f : [0, \infty) \to [0, \infty)$ be an D4367: Unsigned real function such that
(i) $f$ is a D1760: Riemann integrable real function on $[0, b]$ for every $b \in [0, \infty)$
(ii) \begin{equation} \lim_{t \to \infty} f(t) = 0 \end{equation}
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$