# Nonnegative derivative bounded by function, show that $f$ is zero

I'm struggling to prove the following statement, which makes intuitive sense:

Let $$f: \mathbb{R} \to \mathbb{R}$$ be differentiable. Suppose $$\forall x \in \mathbb{R} \quad 0 \le f'(x) \le f(x)\,$$. If $$f$$ vanishes at some point, show that $$f$$ is identically zero.

This is exercise 6 in section 6.7, in Elementary Classical Analysis by Mardsen & Hofmann.

I've managed to do the following:

Let $$\omega \in \mathbb{R}$$ be the point such that $$f(\omega) = 0$$ (which exists by hypothesis). Let $$x < \omega$$. By Cauchy's Mean Value Theorem,

$$\exists \xi \in (x, \omega)\colon\quad 0 \le f(x) =f(x) - f(\omega) = f'(\xi)(x - \omega)\,.$$

By hypothesis, we have that $$f'(\xi) \ge 0$$. On the other hand, $$x - \omega < 0$$. Thus, $$f'(\xi)(x - \omega) \le 0$$. By the above proposition, though, $$f'(\xi)(x - \omega) \ge 0\,$$. Therefore, $$f'(\xi) = 0$$ which implies $$f(x) = 0$$.

With this we have proven that $$\forall x \in \mathbb{R}\quad x \le \omega \rightarrow f(x) = 0\,$$.

But for $$x > \omega$$, I haven't been able to prove much. I've got so far:

Let $$x > \omega$$. By Cauchy's Mean Value Theorem,

$$\exists \xi_1 \in (\omega, x)\colon\quad 0 \le f(x) = f(x) - f(\omega) = f'(\xi_1)(x - \omega) \le f(\xi_1)(x - \omega)\,.$$

If we apply this reasoning recursively on $$f(\xi_1)$$, we get a succession $$(\xi_i)_{i\in\mathbb{N}} \subseteq (\omega, x)$$ such that $$\forall i \in \mathbb{N}\quad \xi_{i+1} \in (\omega, \xi_i)$$ and

$$\forall n \in \mathbb{N}\quad f(x) \le f(\xi_n) \prod_{i = 0}^{n - 1} (\xi_i - \omega)$$

where $$\xi_0 = x$$.

Is there a hint?

$$(e^{-x}f(x))'=e^{-x}(f'(x)-f(x)) \leq 0$$ so $$e^{-x}f(x)$$ is decreasing. If $$f(x_o)=0$$ then $$e^{-x}f(x)$$ is non-negative and $$\leq e^{-x_0}f(x_0) =0$$ for $$x>x_0$$ so $$f(x)=0$$ for $$x \geq x_0$$. For $$x \leq x_0$$ you already have a proof.
The idea is to see that if $$f \neq 0$$, then there exists $$y>\omega$$ such taht $$\forall x \geq y, f(x)>0$$. For such an $$x$$ you have $$\dfrac{f'(x)}{f(x)}\leq 1$$. You can integrate and this gives $$f(x) \leq e^x$$, thus giving an hint to introduce the function $$g(x)\doteq f(x)e^{-x}$$. You can work from that point.