A function whose antiderivative equals its inverse.

Does there exist a continuous function $F$ satisfying the property

\begin{align} F\left(\int^x_0 F(s)\ ds\right) = x \end{align}

If yes, then is the solution unique?

As stated, the question is not well-posed since I haven't specified the domain of $F$. But, the question is intended to be open-ended since it was posed by a couple colleagues of mine during a coffee break.

We did find such a $F$, but couldn't show that it is unique. Here's the spoiler

$F(x) = Cx^\gamma$ where $\gamma = \frac{-1+\sqrt{5}}{2}$ and $C = (1+\gamma)^{\frac{\gamma}{1+\gamma}}$ \begin{align} C\left(\int^x_0 Ct^{\gamma}\ dt\right)^\gamma = C^{1+\gamma}\left( \frac{x^{1+\gamma}}{1+\gamma}\right)^\gamma =\frac{C^{1+\gamma}}{(1+\gamma)^\gamma}x^{\gamma+\gamma^2} = \frac{C^{1+\gamma}}{(1+\gamma)^\gamma}x = x, \ \ \text{ for all } x> 0 \end{align}

We prove a slightly weaker claim, namely that there exists an infinitude of functions which are inverse to one of their antiderivatives, i.e., functions $F$ for which there exists a constant $C$ such that $$F \bigg( C+\int_0^t F(u)du \bigg) =t.$$ The functions will be defined on $[0,\infty)$, not the whole line.

Proof: We use fixed point theory. Fix a real number $x>4$. For $T>0$, let us define the metric space $C_x[0,T]$ which consists of all $f \in C^1[0,T]$ which satisfy the following three conditions: $f(0)=x$, $ f(t) \geq 4$ for all $t \in [0,T]$, and $\|f'\|_{\infty} \leq \frac{1}{4}$. One may easily verify that this is a complete metric space, with respect to the norm $\|f\|_{C_x[0,T]} = \|f\|_{\infty}+\|f'\|_{\infty}$. Here $\| \cdot \|_{\infty}$ denotes the uniform norm on $[0,T]$. When $T=\infty$ we define the analogous space $C_x[0,\infty)$, with the topology of uniform convergence on compact sets.

We define a map $S: C_x[0,\infty) \to C_x[0,\infty)$ by sending a function $f$ to the unique solution of the IVP: $$y'=\frac{1}{f(y)},\;\;\;\;\;\;\; y(0)=x.$$

The solution exists for global time by the Picard Lindelof theorem, since $f \geq 4$ is differentiable. Moreover, it is clear that $S$ maps $C_x[0,\infty)$ to itself. One crucial remark is that since $1/f \leq 1/4$, it necessarily follows that $y(t) \leq x+t/4$ for all $t$.

If $y=Sf$ and $z=Sg$, then we have that $$|y(t)-z(t)| \leq \int_0^t \bigg| \frac{1}{f(y(s))} - \frac{1}{g(z(s))} \bigg| ds = \int_0^t \frac{|f(y(s))-g(z(s))|}{|f(y(s))g(z(s))|}ds \\ \leq \frac{1}{16} \int_0^t |f(y(s))-g(z(s))|ds \leq \frac{1}{16} \int_0^t |f(y(s)) - g(y(s))| +|g(y(s))-g(z(s))| ds \\ \leq \frac{1}{16}t \|f-g\|_{L^\infty[0,x+t/4]} + \frac{1}{16}\|g'\|_{L^\infty[0,x+t/4]} \int_0^t |y(s)-z(s)|ds$$ Again, we have used the fact that $y(s),z(s) \leq x+t/4$. Now by Gronwall's lemma, it necessarily follows that $$\|y-z\|_{L^{\infty}[0,t]} \leq \frac{t}{16} \|f-g\|_{L^\infty[0,x+t/4]} e^{\|g'\|_{L^\infty[0,x+t/4]} \frac{t}{16}} \leq \frac{t}{16}e^{\frac{t}{64}} \|f-g\|_{L^{\infty}[0,x+t/4]}. $$where we used $\|g'\|_{\infty} \leq \frac{1}{4}$. Now for the derivative-norm, we have by the same inequalities that $$\|y'-z'\|_{L^\infty[0,t]} \leq \bigg\| \frac{1}{f \circ y}-\frac{1}{g \circ z} \bigg\|_{L^{\infty}[0,t]} \leq \frac{1}{16} \| f \circ y- g \circ z\|_{L^{\infty}[0,t]} \\ \leq \frac{1}{16} \|f-g\|_{L^{\infty}[0,x+t/4]} + \frac{1}{16} \|g'\|_{L^\infty[0,x+t/4]} \|y-z\|_{L^{\infty}[0,t]} \\ \leq \big( \frac{1}{16} + \frac{t}{256} e^{\frac{t}{64}} \big) \|f-g\|_{L^{\infty}[0,x+t/4]}$$ The preceding two expressions together show that if we define a Picard iteration scheme $f_n=S^nf_0$, then by induction we have that $$\|f_{n+1}-f_n\|_{L^{\infty}[0,t]} + \|f'_{n+1}-f'_n\|_{L^{\infty}[0,t]} \\ \leq \big(\frac{t}{256}e^{\frac{t}{64}} + \frac{1}{16} \big) \big( \frac{t}{16}e^{\frac{t}{64}} \big)^n \big\| f_1-f_0 \big\|_{L^{\infty}[0, (1+4^{-1}+...+4^{1-n})x +4^{-n}t]}$$so that the restriction to $[0,T]$ of these iterates will converge to some function $f$ as $n \to \infty$, whenever $T$ is small enough so that $\frac{T}{16}e^{T/64} <1$ (e.g. $T<13$ works). Now as long as $x<39/4$ (note that this doesn't interfere with the condition $x>4$), we have that $\sum_0^{\infty} 4^{-n}x=\frac{4}{3}x<13$ which is less than the critical $T$-value just discussed. Hence given any $T>0$, there exists some $N$ large enough so that $\sum_0^{N-1} 4^{-k}x + 4^{-N}T< 13$, and hence we see that $f_n$ actually converges in $C_x[0,T]$ for every $T>0$. This argument shows that the map $S$ actually has a globally defined fixed point on the whole space $C_x[0,\infty)$.

Now let $f$ be a fixed point of the map $S$. This means that for every $t>0$, one has $$f'(t) f(f(t)) = 1.$$ So if we define $F(t) = \int_0^t f(u)du$ it holds that $F'(f(t))f'(t)=1$, therefore $F(f(t))=t+F(x)$. Clearly each initial value $x$ gives a different solution $f$.

Now we claim that the fixed point $f$ satisfies $\lim_{t \to \infty} f(t) = +\infty$. If this was not the case, then $f\circ f$ would be bounded on $[0,\infty)$, hence $f' = 1/(f \circ f)$ would be bounded below, hence $f(t) \geq x+ct$ for some $c>0$, contradiction. Therefore $f$ is a continuously increasing bijection from $[0,\infty)$ to $[x,\infty)$. Let $C:=F(x)$, and define $g:[C,\infty) \to [x,\infty)$ by $g(t) = f(t-C)$. Clearly $F(g(t)) = t$, and therefore by the fact that $f$ is a bijection, it follows (by uniqueness of inverses) that $g(F(t))=t$. In other words, we have $$f(F(t)-C)=t,\;\;\;\;\;\;\text{i.e.},\;\;\;\; f\bigg( \int_x^t f(u)du \bigg) = t,\;\;\;\;\forall t \geq x,$$thus proving the claim.