Derivative of distance function to a convex set in CAT(0) space Let $(X,d)$ be a complete CAT(0) space. We denote by $T_x X$ the tangent cone at a point $x\in X$ and by $d_x$ its associated distance. So $(T_x X,d_x)$ is also a complete CAT(0) space. In CAT(0) spaces, for any two points $x,y \in X$, there exists a unique unit speed geodesic joining them. We denote by $\uparrow_x^y$ the direction of such geodesic. Let $C$ be a closed convex subset of $X$. So $(C,d)$ seen as a metric space is also a complete CAT(0) space. Let $f : x \mapsto d(x,C)$ be the function defined by
$$x \mapsto d(x,C) := \inf_{y\in C} d(x,y).$$
It is known fact that the infinimum is reached and it is unique, we denote it by $\pi(x)$. Furthermore, the function $f$ is convex. Hence it admits directional derivatives everywhere. I am trying to find the differential of this function explicitly. I strongly suspect that the differential at a point $x \in X$ has the following form:
$$\forall v \in T_xX, \quad D_x f \centerdot v = \begin{cases} - \langle \uparrow_x^{\pi(x)}, v \rangle, \quad \mbox{if } x \notin C, \\
d_x(T_x C , v), \quad \mbox{if } x \in C, \end{cases} 
$$
where $T_x C$ is seen as a convex subset of $(T_x X,d_x)$.
However, I can't find a proof anywhere in the literature. The only case I found was when the convex subset $C$ is reduced to a point $C = \{x_0\}$. Is my formula correct ?
 A: It is true.
First part.
Assume $x\notin C$, note that $\mathrm{dist}_{\pi(x)}\ge\mathrm{dist}_{C}$.
It follows that
$$d_x\mathrm{dist}_{C}(v) \le d_x\mathrm{dist}_{\pi(x)}(v)= -\langle \uparrow_x^{\pi(x)}, v \rangle.$$
On the other hand $$d_x\mathrm{dist}_{C}(v) \le  -\langle \uparrow_x^{\pi(x)}, v \rangle.$$
The latter follows since
$d_x\mathrm{dist}_{C}\colon \mathrm{T}_x\to\mathbb{R}$ is 1-Lipschitz and evidently
$$d_x\mathrm{dist}_{C}(\lambda \cdot\uparrow_x^{\pi(x)})=-\lambda$$
for any $\lambda\ge 0$.
Second part. We may assume that $v$ points in a geodesic direction; that is, there is a geodesic $\gamma$ from $x$ such that $\gamma'(0)=v$.
The lower bound follows from the definition of angle.
To prove the upper bound, choose $y=\gamma(\varepsilon)$, set $z=\pi(y)$ and apply that triangle $[xyz]$ is thin.
Remark.
For nongeodesic direction, one might define directional derivative as derivative of limit instead of the limit of derivative.
In this case the answer is "no".
Consider the unit disc $C$ in the plane
with an attached half-line to each point.
It is a complete CAT(0) length space
with extendable geodesics.
Observe that your equality does not hold at a boundary point of $C$ in the direction tangent to the disc.

It is closely related to the discussion after the solution of Exercise 2.2.8. in our book.
