Find all differentiable functions $f : [0, +\infty) \rightarrow \mathbb{R}$ such that $f(1) = 1$ and $f(x)f(y) \leq f(xy)$ The exercise
Find all differentiable functions $f : [0, +\infty) \rightarrow \mathbb{R}$ such that:

*

*$f(1) = 1$

*$f(x)f(y) \leq f(xy)$ for all $x, y \geq 0$
My try
I have found that the functions $x \mapsto x^\alpha$ for $\alpha \in [1, +\infty)$ are solutions. The constant function $x \mapsto 1$ is also solution.
As $f(0)^2 \leq f(0)$ one also has that $f(0) \in [0, 1]$.
If I take a solution $f$, my idea would be to try proving it is of the form $f(x) = x^\alpha$ for some $\alpha$. Necessarily this $\alpha$ would be equal to $f'(1)$. So I set $\alpha := f'(1)$ and considered $g(x) = \frac{f(x)}{x^\alpha}$ for $x > 0$. One can show $g$ is derivable and $g'(1) = 0$ and $g$ verifies the functional equation (for $x, y > 0$). So the goal would be to show that $g = 1$, but I've not managed to prove it yet. Any help is welcome folks!
 A: First note that $f(1)=1$, and $f$ differentiable, implies that continuous, and hence
$f(x)>0$, in $(1-\delta,1+\delta)$, for some $\delta>0$.
Next, if $x\in (0,\infty)$, then $x_n=x^{1/n}\in(1-\delta,1+\delta)$, for $n$ sufficiently large, and hence
$$
f(x_n\cdot x_n)\ge \big(f(x_n)\big)^2\quad\Longrightarrow\quad
f(x_n\cdot x_n\cdot x_n)\ge f(x_n\cdot x_n)f(x_n)\ge \big(f(x_n)\big)^3
 \\ \quad\Longrightarrow\quad f(x)\ge f(x_n^n)\ge\big(f(x_n)\big)^n>0.
$$
Thus $f(0,\infty)\subset (0,\infty)$.
Set next $g(x)=\log f(\mathrm{e}^x)$.
Then $g:\mathbb R\to\mathbb R$, $g(0)=0$ and
$$
g(x+y)\ge g(x)+g(y) \quad \text{for all $x,y\in\mathbb R$.}
$$
The $g$ is also differentiable as a composition of such and let
$$
c=\lim_{h\to 0} \frac{g(h)-g(0)}{h}=\lim_{h\to 0} \frac{g(h)}{h}.
$$
Then
$$
g(x+h)\ge g(x)+g(h) \quad\Longrightarrow\quad \frac{g(x+h)-g(x)}{h}-\frac{g(h)}{h}=
\left\{\begin{array}{ccc}\text{non-negative if $h>0$}, \\ \text{non-positive if $h<0$.} \end{array}\right.
$$
and since $\lim_{h\to 0}\frac{g(x+h)-g(x)}{h}$ exists, then
$$
\lim_{h\to 0}\frac{g(x+h)-g(x)}{h}=\lim_{h\to 0}\frac{g(h)}{h}=c
$$
which implies that $g(x)=cx$ and
$$
f(x)=\mathrm{e}^{g(\log x)}=\mathrm{e}^{c\log x}=x^c.$$
Finally, as $f$ is defined and it is also differentiable at $x=0$, then $c\ge 1$.
