Monotone mean-value point of an integral average (source code)

= Monotone mean-value point of an integral average
{title2=$f(g(x))=x^{-1}\int_0^xf(t)\,dt$}

For a continuous strictly decreasing real function, its average $h(x)=x^{-1}\int_0^xf(t)dt$ lies strictly between $f(x)$ and $f(0)$ for $x>0$. There is a unique $g(x)\in(0,x)$ with $f(g(x))=h(x)$. If $f$ is <differentiable> and $f'<0$ throughout the positive half-line, the <fundamental theorem of calculus> and the derivative formula for the monotone inverse give
$$
g'(x)=\frac{f(x)-f(g(x))}{xf'(g(x))}>0.
$$
Continuity of $f'$ is unnecessary: differentiability of a strictly monotone function with nonzero derivative at a point suffices for differentiability of its inverse there.