Proposition $3.6$ of Riemannian Geometry by Do Carmo I am reading the proof of the proposition $3.6$ of Riemannian Geometry by Do Carmo, which can be read here, and I would like to understand why the following statement is true:

If $l(c) = l(\gamma)$, then $\left| \frac{\partial f}{\partial t} \right| = 0$, that is, $v(t) = \ \text{const.}$, and $|r'(t)| = r'(t) > 0$.

Specifically, my doubts are

*

*Why $l(c) = l(\gamma)$ imply $\left| \frac{\partial f}{\partial t} \right| = 0$?

$l(c) = l(\gamma)$ imply $c'(t) = r'(t)$?


*Why $\left| \frac{\partial f}{\partial t} \right| = 0$ imply $v(t) = \ \text{const.}$, and $|r'(t)| = r'(t) > 0$?

Thanks in advance!
 A: First, I would like to make a short comment. Do Carmo's book is really great and covers a large part of basics in Riemannian geometry. But I personnally do not really like all this part concerning the exponential map, normal coordinates etc. It is always a pain to me to understand the author's notation and ideas. I would highly recommand to look at the corresponding parts in J. Lee's Riemannian manifolds: an introduction to curvature, or S. Gallot, D. Hulin and J. Lafontaine's Riemannian Geometry, which provide (in my opinion) a bit clearer proofs.
Note that
$
|c'|^2 = |r'|^2 + |\partial_tf|^2 \geqslant |r'|^2,
$
which yields
$$
|c'| \geqslant |r'|.
$$
Integrating this between $\varepsilon>0$ and $1$ together with the triangular inequality yields
$$
l(c) = \int_0^1|c'| \geqslant \int_{\varepsilon}^1|c'| \geqslant \int_{\varepsilon}^{1} |r'| \underset{(1)}{\geqslant} \left| \int_{\varepsilon}^1 r' \right| = |r(1)-r(\varepsilon)| = r(1)-r(\varepsilon) \to_{\varepsilon \to 0} r(1)  =l (\gamma),
$$
and therefore, we have
$l(c) \geqslant l(\gamma)$. Suppose this last inequality is an equality.

*

*This implies that $|c'|-|r'|$ is a non-negative function with vanishing integral, and it follows that $|c'|-|r'|=0$ and thus $|c'| = |r'|$.
Equality $|c'|^2 = |r'|^2 + |\partial_tf|^2$ gives $|\partial_tf|^2 = 0$.


*First: note that $\partial_tf = \mathrm{d}\exp_p\left(r(t)v(t)\right)\cdot \left(r(t) v'(t)\right)$. Moreover, the exponential map is supposed to be a diffeomorphism (we are considering a normal geodesic ball!), hence $\mathrm{d}\exp_p\left(r(t)v(t)\right)$ is a linear isomorphism. It follows from $|\partial_t f|=0$
that $r(t)v'(t) = 0$, and therefore, $v'(t) = 0$
(recall that $r>0$). It follows that $v(t) = v_0$. Second: in inequality $(1)$, there is equality in the triangle inequality (when $\varepsilon \to 0$):
$$
\left|\int_{0}^1 r' \right| = \int_0^1|r'|,
$$
which implies (by an integration-theory result) that $r'$ has constant sign. As $r(\varepsilon) \to 0$ and $r(1) = l(\gamma)>0$, it follows that $r(1) - r(\varepsilon) >0$ for $\varepsilon >0$ small enough.By the MVT, there is $t \in (\varepsilon,1)$ with $r'(t) = \frac{r(1)-r(\varepsilon)}{1-\varepsilon} >0$. The result follows.
