Les géodésiques minimisent localement la longueur

Notons $\mathcal B = \operatorname{Exp}_m\big(B_m(0, \varepsilon)\big)$, ouvert de $U$, et, pour $y \in \mathcal B$, $\varrho(y) = \|\operatorname{Exp}_m^{-1}(y)\|_m$. La fonction $\varrho$ est continue sur $\mathcal B$, et de classe $C^1$ là où elle ne s'annule pas, la norme $\|\cdot\|_m$ provenant d'un produit scalaire.

Le premier passage à la distance $\rho$. Soit $\mathcal B_\rho = \operatorname{Exp}_m(B_m(0, \rho))$, ouvert, et $K_\rho = \operatorname{Exp}_m(\bar B_m(0, \rho))$, compact comme image continue d'un compact, donc fermé dans $U$. Par injectivité, $q \notin \mathcal B_\rho$. Soit $t_1 = \inf\{t : \beta(t) \notin \mathcal B_\rho\}$ ; comme $\beta(0) = m \in \mathcal B_\rho$, ouvert, $t_1 > 0$. Pour $t < t_1$, $\beta(t) \in \mathcal B_\rho \subset K_\rho$, donc $\beta(t_1) \in K_\rho$ ; et $\beta(t_1) \notin \mathcal B_\rho$, sans quoi, $\mathcal B_\rho$ étant ouvert, $\beta$ y resterait un peu après $t_1$, ou bien $t_1 = 1$ et $\beta(1) = q \in \mathcal B_\rho$. Donc $\varrho(\beta(t_1)) = \rho$.

Le dernier passage en $m$. Soit $t_0$ le plus grand $t \in [0, t_1]$ tel que $\beta(t) = m$, qui existe car cet ensemble est fermé et non vide. Sur $]t_0, t_1]$, $\beta$ reste dans $K_\rho \setminus \{m\} \subset \mathcal B$, et $\varrho \circ \beta$ est strictement positive et de classe $C^1$.

Comparaison. Soit $t \in \,]t_0, t_1]$. Au voisinage de $\beta(t)$, la démonstration du nœud Coordonnées polaires géodésiques, (iv), fournit des fonctions $r = \varrho \circ \beta$ et $\theta$ de classe $C^1$ telles que $\beta = \operatorname{Exp}_m(r\,\omega(\theta))$, donc $x \circ \beta = X(r, \theta)$. Par le lemme de Gauss et $\|X_r\| = 1$, $$\begin{aligned} \|(x \circ \beta)'\|^2 &= \|r'X_r + \theta'X_\theta\|^2 \\ &= r'^2 + G\theta'^2 \geqslant r'^2. \end{aligned}$$ Pour $t_0 < s < t_1$, il vient $$\int_s^{t_1}\|(x \circ \beta)'\| \geqslant \int_s^{t_1} r' = \rho - r(s).$$ Quand $s \to t_0$, $r(s) \to \varrho(m) = 0$ par continuité, et l'intégrale de gauche tend vers $\int_{t_0}^{t_1}$, majorée par la longueur totale.