I've been recently interested in directional derivatives of the Riemannian distance function, and I came across this question, and its answer by Sergei Ivanov, where he stated an important result: (I quote from his answer without modifying anything)
"In general, the distance function has one-sided directional derivatives everywhere. This derivative has a nice description in the case when you fix $p\in M$ and study the function $f=d(p,\cdot)$. Namely let $q\in M$, $q\ne p$, and denote by $\vec{qp}$ the set of initial velocity vectors (in $T_qM$) of unit-speed minimizing geodesics from $q$ to $p$. Then, for a vector $v\in T_qM$, the one-sided derivative $f'_v$ of $f$ in the direction of $v$ is $$ f'_v=\min\{-\langle v,\xi\rangle:\xi\in \vec{qp}\} . $$ This follows from the first variation formula and holds not only in Riemannian manifolds but also in Alexandrov spaces."
I'd like to find a book and read the proof of this part:
$$ f'_v=\min\{-\langle v,\xi\rangle:\xi\in \vec{qp}\} . $$
In his answer, he also stated: "but any book that covers Berger's lemma about geodesics realizing the diameter probably has directional derivatives as a sublemma", but an internet search on "Berger's lemma about geodesics realizing the diameter" wasn't helpful.
Could you please give me a reference for this result and perhaps also for Berger's lemma? Or if you could prove it, that'd be very helpful too! Thank you in advance!!
