In a connected Riemannian manifold, choose a small compact geodesic sphere around with . Minimize on this sphere. Every path from to crosses it, so an almost-minimizing path has length at least . The triangle inequality gives the reverse bound, yielding the displayed equality. No global completeness is needed.
Write for the Levi-Civita connection and define its Christoffel symbols by . For the Riemannian metric matrix and its inverse ,
A curve with affine parameter is a geodesic when , equivalently
The connection is metric compatible and torsion free; in particular . The coordinate velocities are , and the displayed coefficients are smooth functions of position.
For whose initial-value geodesic exists through time , with and , define . The domain is open and contains a neighborhood of zero. Indeed the geodesic equation is a smooth first-order ODE in ; the constant solution with initial velocity zero exists through time , and existence on a compact time interval and smooth dependence persist for nearby initial data. Reparameterization and uniqueness give wherever defined. Consequently the differential of the exponential map at zero is
The inverse function theorem gives a neighborhood of zero on which is a diffeomorphism onto a neighborhood of . Shrink to a ball in and choose an orthonormal basis there. Its linear coordinate functions composed with are the geodesic normal coordinates on . This establishes well-defined local coordinates without assuming geodesic completeness.
In these geodesic normal coordinates, every radial geodesic has coordinate expression . Its equation at reads for every . The coefficients are symmetric in by the torsion-free connection property. Evaluating at the coordinate unit vectors and their pairwise sums, or using the polarization identity, therefore gives
This is the fact that Christoffel symbols vanish at the center of normal coordinates. Also , since is the identity in an orthonormal basis.
For sufficiently small , the geodesic sphere is . It is a smooth hypersurface because is a diffeomorphism on the ball. It equals the local distance sphere for sufficiently small radius, as the length comparison below shows; no assertion of global smoothness for large radii is needed.
The full Gauss lemma is
for in a star-shaped domain of and . To prove it, set , and , for near zero. Every -curve is a geodesic and has squared speed . The torsion-free connection property and the commuting parameter fields give ; metric compatibility and then give
At , , so . Integration from to followed by setting proves the boxed identity, because and . For any in the domain, a small neighborhood of its compact radial segment suffices for the variation. The zero vector is covered directly.
In particular, if , the images of the radial and spherical tangent directions are orthogonal; taking also proves preservation of radial length. Thus in geodesic polar coordinates the Riemannian metric has radial part and no mixed radial-angular term. Every curve in a small normal ball from its center to radial coordinate has length at least , by integrating the absolute radial derivative; the radial geodesic realizes this length. To exclude shortcuts leaving the ball, choose a larger normal ball of radius with compact closure in and restrict to : an escaping curve first reaches radial coordinate and already has length at least . This proves the asserted small-radius distance interpretation and orthogonality of radial geodesics to geodesic spheres.
Figure 1.
Radial geodesics and a geodesic sphere on the round unit sphere, with orthogonal radial and angular tangent vectors
.
For in the domain of the exponential map at , let be the unique geodesic with initial data and define . The domain consists of initial velocities whose geodesics exist on ; it is open, contains zero, and need not be the whole tangent space. The ordinary differential equation theorem used here says that a smooth vector field has unique maximal integral curves, with an open flow domain and smooth dependence on initial point and time. Applied to the geodesic equation on , it gives smoothness of the exponential map. Rescaling the parameter gives and hence . The inverse function theorem makes a diffeomorphism from a neighbourhood of zero to one of . Coordinates in an orthonormal tangent basis transported by this map are geodesic normal coordinates.
The geodesic sphere of radius is . For small , it is , a smooth compact hypersurface; larger distance spheres need not be smooth. The Gauss lemma states
In particular radial and angular directions are orthogonal and the radial coordinate measures arc length.
For a piecewise smooth path , put . The Riemannian distance is over such paths from to . Connectedness makes it finite. Reversal and concatenation give symmetry and the triangle inequality; positivity and compatibility with the manifold topology follow locally from geodesic normal coordinates and the Gauss lemma.
Choose so that is a diffeomorphism on a neighbourhood of the closed tangent ball of radius . For , radial geodesics realize the distance from on that ball. Indeed, Gauss lemma bounds any path remaining in the normal ball below by its radial change, while a path leaving the radius- ball already has length at least . Thus the radius- sphere is the compact exponential image described above.
Given , take . The continuous function attains its minimum at some . Every path from to crosses that sphere, since the distance from is continuous. Splitting at a crossing gives length at least . Taking the infimum over paths, and using the triangle inequality in the other direction, proves the distance splitting through a small geodesic sphere equality
This compact local argument does not assume completeness or the existence of a globally minimizing geodesic to .
For the Lie-group clause, a bi-invariant Riemannian metric has adjoint-invariant identity inner product. Differentiating this invariance gives . The Koszul formula for left-invariant vector fields has no metric-derivative terms, and this skew-adjointness reduces it to
This is the Levi-Civita connection of a bi-invariant metric.
Let be the integral curve through the identity of the left-invariant field with identity value . Uniqueness and left translation show wherever the local curves are defined. The field is complete: a fixed local existence interval about the identity translates to an equally long interval at every point of the group. Restarting the curve before any proposed finite endpoint extends it beyond that endpoint. Thus exists on , and uniqueness now gives the group law for every .
Since , this integral curve is a geodesic. Conversely any geodesic starting at the identity has the same initial data as one of these curves and agrees with it by uniqueness. Therefore the geodesics of a bi-invariant metric are one-parameter subgroups conclusion is
The zero velocity gives the constant, trivial subgroup. Here is the Exponential map of a Lie group; for this metric it agrees at the identity with the Riemannian exponential.