Proposition 3.6 Let $p \in \mathcal{M}$, $U$ a normal neighborhood of $p$, $B \subset U$ a normal ball of center $p$. Let $\gamma : [0,1] \to B$ be a geodesic segment with $\gamma(0) = p$. If $c : [0,1]\to \mathcal{M}$ is any piecewise differentiable curve joining $\gamma(0)$ to $\gamma(1)$ then $l(\gamma) \leq l(c)$ and if equality holds then $\gamma([0,1]) = c([0,1])$.
For the proof
Suppose initially that $c([0,1]) \subset B$. Since $\exp_p$ is a diffeomorphism on $U$, the curve $c(t)$, for $t \neq 0$, can be written uniquely as $\exp_p (r(t) \cdot v(t)) = f(r(t),t)$ where $t \to v(t)$ is a curve in $T_p\mathcal{M}$ with $\left| v(t) \right| = 1$ and $r : (0,1] \to \mathbb{R}$ is a positive piecewise differentiable function.
The first question is why can $c(t)$ be written in such a way? My first guess is because in $B$ by definition of exponential map there's a unique geodesic such that
$$ \exp_p(v) = \alpha(1,p,v) $$
And I can write $v$ in the form stated in the theorem and the equation
$$ c(t) = \exp_p(v) $$
Is well defined.
Carrying on with the prof
It follows that, except for a finite number of points, $$ \frac{dc}{dt} = \frac{\partial f}{\partial r} r'(t) + \frac{\partial f}{\partial t} $$
I think it's clear the rule applied is essentially the chain rule. However I do struggle to derive the formula using the definition of differentials in manifolds (rigorously).
My attempt was to decompose $f$ as
$$ t \to (r(t),t) \to f(r(t),t) $$
So $f = f_2 \circ f_1$, where $f_1 : \mathbb{R} \to \mathbb{R}^2$ and $f_2 : \mathbb{R}^2 \to \mathcal{M}$, for $f_1$ the differential is simply a derivative wrt $t$ componentwise. For $f_2$ I would assume I can use
$$ d f_{2_{(r,t)}} = \left[ d f_{2_{(r,t)}} \left( \frac{\partial}{\partial r} \right) \; d f_{2_{(r,t)}} \left(\frac{\partial}{\partial t} \right) \right] $$
And using the author notation I'll end up with the same expression, the question is whether my derivation is correct.
Finally
From the Gauss lemma, $\left\langle \frac{\partial f}{\partial r}, \frac{\partial f}{\partial t} \right\rangle = 0$
I'd assume from the Gauss Lemma more specifically it follows that
$$\left\langle \frac{\partial f}{\partial r}, \frac{\partial f}{\partial t} \right\rangle = \left\langle \frac{\partial}{\partial r}, \frac{\partial}{\partial t} \right\rangle$$
And the two vectors $\frac{\partial}{\partial r}$ and $\frac{\partial}{\partial t}$ and these are orthogonal.
Again, is this correct? Very last bit
Since $\left| \frac{\partial f}{\partial r} \right| = 1$, ... I'm not quite sure I understand why is 1, could you explain?
I'm still reading through the rest of the proof it seems ok, but I'll potentially ask a different question.
Also just to clarify shouldn't the expression $$ \frac{dc}{dt} = \frac{\partial f}{\partial r} r'(t) + \frac{\partial f}{\partial t} $$ actually be $$ \frac{dc}{dt} = r'(t) \frac{\partial f}{\partial r} + \frac{\partial f}{\partial t} $$
Mostly because $r'(t)$ is considered an element of a scalar field, while $\frac{\partial f}{\partial r}$ is a vector.
Thank you
In the following, we will consider $c$ as smooth as possible everywhere, so everything is well defined.
As $\exp_p : U_p \to \exp_p(U_p) \subset M$ is a diffeomorphism, if $c : [0,1] \to \exp_p(U_p)$ is a smooth curve, there exist a unique curve $\tilde{c} : [0,1] \to U_p$ such that $$ \forall t \in [0,1],~ c(t) = \exp_p(\tilde{c}(t)). $$ Now, as $\tilde{c}$ is a path in $U_p \subset T_pM$, by polar decomposition, one can write $\tilde{c}(t) = r(t) \cdot v(t)$ where $r(t) \geqslant 0$ and $\|v(t)\|_{g_p} = 1$. The author seems to chose a little-bit complicated notation, but it is clear that he uses polar decomposition.
Now, write $c(t) = \exp_p(r(t)\cdot v(t)) = f(r(t),t)$, where $f$ is the function $f(r,t) = \exp_p(rv(t))$ when $r$ is considered as a variable. Then $$ c'(t) = \left.\frac{\mathrm{d}}{\mathrm{d}s}\right|_{s=0}f(r(t+s),t+s),$$ and using the right-way the chain-rule says $$ c'(t) = \mathrm{d}f(r(t),t)\cdot( r'(t),1), $$ where $(r'(t),1)$ is the tangent vector to the curve $s\mapsto (r(s),s)$ at $s=t$. Hence, by the very definition of partial derivatives in differential geometry: $$ c'(t) = \dfrac{\partial f}{\partial r}(r(t),t) \cdot \left(r'(t),0 \right) + \frac{\partial f}{\partial t}(r(t),t) \cdot (0,1), $$ which we write for the sake of compactness $c'(t) = \frac{\partial f}{\partial r}\cdot r'(t) + \frac{\partial f}{\partial t} $. We put the $r'(t)$ at the right because we think of $r'(t)$ as a vector, tangent to the curve $s \mapsto r(s)$. Indeed, $r'(t)$ is just a scalar because $r$ takes value in an interval, so you can move it to the left. Basically, you can do whatever you want with these kind of expressions if you know exactly what are the objects.
Now, recall the general Gauss lemma:
Looking closely to $f(r,t) = \exp_p(r\times v(t))$, we find that \begin{align} \frac{\partial f}{\partial r}(r,t) &= \mathrm{d}\exp_p(r\times v(t))\cdot v(t) ,\\ \frac{\partial f}{\partial t}(r,t) &= \mathrm{d}\exp_p(r\times v(t))\cdot r\times v'(t). \end{align} Hence, by the Gauss lemma, we have $$ g_{\exp_p(rv(t))}\left(\frac{\partial f}{\partial r}(r,t),\frac{\partial f}{\partial t}(r,t) \right) = g_p(v(t),r\times v'(t)) = rg_p(v(t),v'(t)). $$ As $t \mapsto v(t)$ is a curve that lies on the unit sphere, $v'(t)$ is orthogonal to $v(t)$, and then, the above scalar product is equal to zero.
Finally, note that the function $f(\cdot,t) : r \mapsto \exp_p(r\times v(t))$ is actually a geodesic. Hence, all its tangent vectors have the same length. At $r=0$, the tengent vector is $v(t)$, which is of length $1$ by definition of polar decomposition. At $r >0$, the tangent vector to the curve is $\partial f /\partial r$. We can conclude that $\left\|\frac{\partial f}{\partial r}\right\| = 1$.
Comment. The function $f$ is defined so that we can write the equation $c'(t) = \frac{\partial f}{\partial r}\cdot r'(t) + \frac{\partial f}{\partial t} $, which tells us, together with the fact that the partial derivatives of $f$ are orthogonal, that we have a natural decomposition of $c'(t)$ into a radial component ($\partial_rf \cdot r'$) and a component orthogonal to geodesic spheres ($\partial_t f)$.