Geodesics and the exponential map in inner-product spaces

This file identifies the Riemannian geodesics of a finite-dimensional real inner-product space. Its standard Riemannian metric is constant, so the Levi-Civita connection has vanishing Christoffel map, and the geodesic equation says that the acceleration vanishes. On every interval the geodesics are therefore exactly the affine segments. Consequently the maximal intervals are all of ℝ, and the chosen maximal geodesic with initial point p and velocity v is t ↦ p + t • v.

It follows that the exponential map at p is defined on all of T_p F and is translation by p, under the canonical identification NormedSpace.fromTangentSpace of T_p F with F, so its differential is the identity everywhere. Since the metric is the inner product of F at every point, this differential preserves inner products; in particular it satisfies the radial identity of the Gauss lemma. Every open neighbourhood of the origin that is star-shaped at the origin is therefore a normal domain. In particular the tangent ball of radius r > 0 is a normal domain whose normal neighbourhood is Metric.ball p r, and on it the Riemannian logarithm is q ↦ q - p.

These formulas include the zero-dimensional space. They provide the flat model against which the exponential map, normal domains, and the logarithm can be checked.

Main results

• TauCeti.Manifold.christoffelMap_leviCivita_model_space: the Christoffel map of the standard Riemannian metric vanishes.
• TauCeti.Manifold.isGeodesicCurve_add_smul: an affine line is an all-time geodesic.
• TauCeti.Manifold.isGeodesicCurveOn_iff_model_space: the geodesic equation is the vanishing of the acceleration.
• TauCeti.Manifold.isGeodesicCurveOn_iff_exists_eqOn_add_smul and TauCeti.Manifold.isGeodesicCurveOnFrom_iff_eqOn_add_smul: on an interval, the geodesics are exactly the affine segments, and the one with initial data (p, v) is t ↦ p + t • v.
• TauCeti.Manifold.isGeodesicCurve_iff_exists_eq_add_smul: the all-time geodesics are exactly the affine lines.
• TauCeti.Manifold.geodesicInterval_model_space: every affine initial condition exists for all time.
• TauCeti.Manifold.maximalGeodesic_model_space: the chosen maximal geodesic is the affine line.
• TauCeti.Manifold.expDomain_model_space and TauCeti.Manifold.isGeodesicallyCompleteAt_model_space: the exponential map is defined everywhere, so the space is geodesically complete at every point.
• TauCeti.Manifold.riemannianExp_model_space: the exponential map at p is translation by p.
• TauCeti.Manifold.mfderiv_riemannianExp_apply_model_space and TauCeti.Manifold.fderiv_riemannianExp_apply_model_space: its differential is the identity.
• TauCeti.Manifold.inner_mfderiv_riemannianExp_model_space: hence its differential preserves inner products; in particular it satisfies the radial identity of the Gauss lemma.
• TauCeti.Manifold.isNormalDomain_model_space and TauCeti.Manifold.isNormalDomain_ball_model_space: open star-shaped neighbourhoods of the origin, in particular tangent balls, are normal domains.
• TauCeti.Manifold.image_riemannianExp_ball_model_space: the exponential image of the tangent ball of radius r is the ball of radius r about p.
• TauCeti.Manifold.riemannianLog_model_space and TauCeti.Manifold.riemannianLog_ball_model_space: the logarithm sends q to q - p.

References

• M. P. do Carmo, Riemannian Geometry, Chapter 3, §§2–3.

@[simp]

theorem TauCeti.Manifold.leviCivitaConnection_const_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (v x : F) : ↑(CovariantDerivative.leviCivitaConnection (modelWithCornersSelf ℝ F) F) (fun (x : F) => v) x = 0

The Levi-Civita connection of the standard Riemannian metric differentiates a constant vector field to zero.

@[simp]

theorem TauCeti.Manifold.christoffelMap_leviCivita_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (x : F) : christoffelMap (Module.finBasis ℝ F) ⋯ x = 0

The Christoffel map of the standard Riemannian metric on an inner-product space vanishes in its canonical coordinates.

theorem TauCeti.Manifold.isGeodesicCurveOnFrom_add_smul {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p v : F) : IsGeodesicCurveOnFrom (modelWithCornersSelf ℝ F) (fun (t : ℝ) => p + t • v) Set.univ p v

Every affine line in a finite-dimensional real inner-product space is a geodesic for the standard Riemannian metric, with its evident initial point and velocity.

theorem TauCeti.Manifold.isGeodesicCurve_add_smul {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p v : F) : IsGeodesicCurve (modelWithCornersSelf ℝ F) fun (t : ℝ) => p + t • v

Every affine line in a finite-dimensional real inner-product space is a geodesic for the standard Riemannian metric.

@[simp]

theorem TauCeti.Manifold.geodesicInterval_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p v : F) : geodesicInterval (modelWithCornersSelf ℝ F) F p v = Set.univ

Geodesics in a finite-dimensional inner-product space exist for every real parameter.

@[simp]

theorem TauCeti.Manifold.maximalGeodesic_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p v : F) (t : ℝ) : maximalGeodesic (modelWithCornersSelf ℝ F) F p v t = p + t • v

The chosen maximal geodesic in an inner-product space is its affine line.

theorem TauCeti.Manifold.isGeodesicCurveOn_iff_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} {s : Set ℝ} (hs : UniqueDiffOn ℝ s) : IsGeodesicCurveOn (modelWithCornersSelf ℝ F) γ s ↔ ContDiffOn ℝ 2 γ s ∧ ∀ r ∈ s, derivWithin (derivWithin γ s) s r = 0

The geodesic equation in an inner-product space. Since the Christoffel map vanishes, a curve is a geodesic on a parameter set with unique derivatives exactly when it is C² there and its acceleration within that set vanishes.

theorem TauCeti.Manifold.isGeodesicCurveOn_iff_exists_eqOn_add_smul {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} {s : Set ℝ} (hs : UniqueDiffOn ℝ s) (hs' : IsPreconnected s) : IsGeodesicCurveOn (modelWithCornersSelf ℝ F) γ s ↔ ∃ (p : F) (v : F), Set.EqOn γ (fun (t : ℝ) => p + t • v) s

The geodesics of an inner-product space on an interval are affine segments. On a preconnected parameter set with unique derivatives, such as a nondegenerate interval, a curve in a finite-dimensional real inner-product space is a geodesic exactly when it agrees there with an affine line.

theorem TauCeti.Manifold.isGeodesicCurveOnFrom_iff_eqOn_add_smul {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} {s : Set ℝ} (hs : UniqueDiffOn ℝ s) (hs' : IsPreconnected s) (h0 : 0 ∈ s) {p v : F} : IsGeodesicCurveOnFrom (modelWithCornersSelf ℝ F) γ s p v ↔ Set.EqOn γ (fun (t : ℝ) => p + t • v) s

The geodesic of an inner-product space with given initial data. On a preconnected parameter set with unique derivatives containing 0, the geodesic starting at p with velocity v is the affine line t ↦ p + t • v there.

theorem TauCeti.Manifold.isGeodesicCurve_iff_exists_eq_add_smul {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {γ : ℝ → F} : IsGeodesicCurve (modelWithCornersSelf ℝ F) γ ↔ ∃ (p : F) (v : F), γ = fun (t : ℝ) => p + t • v

The geodesics in a finite-dimensional real inner-product space are exactly the affine lines.

The exponential map and the logarithm

@[simp]

theorem TauCeti.Manifold.expDomain_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F) : expDomain (modelWithCornersSelf ℝ F) F p = Set.univ

The exponential map of a finite-dimensional inner-product space is defined on every tangent vector.

theorem TauCeti.Manifold.isGeodesicallyCompleteAt_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F) : IsGeodesicallyCompleteAt (modelWithCornersSelf ℝ F) F p

A finite-dimensional inner-product space is geodesically complete at every point.

@[simp]

theorem TauCeti.Manifold.riemannianExp_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F) (v : TangentSpace (modelWithCornersSelf ℝ F) p) : riemannianExp (modelWithCornersSelf ℝ F) F p v = p + (NormedSpace.fromTangentSpace p) v

The exponential map of a finite-dimensional inner-product space at p is translation by p, under the canonical identification NormedSpace.fromTangentSpace of T_p F with F.

theorem TauCeti.Manifold.mfderiv_riemannianExp_apply_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F) (v w : TangentSpace (modelWithCornersSelf ℝ F) p) : (mfderiv% (riemannianExp (modelWithCornersSelf ℝ F) F p) v) w = (NormedSpace.fromTangentSpace p) w

The differential of the exponential map of a finite-dimensional inner-product space is the identity at every tangent vector.

@[simp]

theorem TauCeti.Manifold.fderiv_riemannianExp_apply_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F) (v w : TangentSpace (modelWithCornersSelf ℝ F) p) : (fderiv ℝ (riemannianExp (modelWithCornersSelf ℝ F) F p) v) w = (NormedSpace.fromTangentSpace p) w

The Fréchet derivative of the exponential map of a finite-dimensional inner-product space is the identity at every tangent vector. This is the simp-normal form of mfderiv_riemannianExp_apply_model_space.

@[simp]

theorem TauCeti.Manifold.inner_mfderiv_riemannianExp_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F) (v w₁ w₂ : TangentSpace (modelWithCornersSelf ℝ F) p) : inner ℝ ((mfderiv% (riemannianExp (modelWithCornersSelf ℝ F) F p) v) w₁) ((mfderiv% (riemannianExp (modelWithCornersSelf ℝ F) F p) v) w₂) = inner ℝ w₁ w₂

The Gauss lemma in an inner-product space. The differential of the exponential map of a finite-dimensional inner-product space at every tangent vector v preserves inner products. Taking w₁ = v gives the radial identity ⟪d(exp_p)_v(v), d(exp_p)_v(w)⟫ = ⟪v, w⟫ of the Gauss lemma TauCeti.Manifold.inner_mfderiv_riemannianExp_radial; in this flat case it holds for every pair of tangent vectors, not only for the radial direction.

theorem TauCeti.Manifold.image_riemannianExp_ball_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F) (r : ℝ) : riemannianExp (modelWithCornersSelf ℝ F) F p '' Metric.ball 0 r = Metric.ball p r

The exponential map of a finite-dimensional inner-product space at p maps the tangent ball of radius r onto the ball of radius r about p.

theorem TauCeti.Manifold.isNormalDomain_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F) {U : Set (TangentSpace (modelWithCornersSelf ℝ F) p)} (hU : IsOpen U) (h0 : 0 ∈ U) (hstar : StarConvex ℝ 0 U) : IsNormalDomain (modelWithCornersSelf ℝ F) F p U

In a finite-dimensional inner-product space, every open neighbourhood of the origin that is star-shaped at the origin is a normal domain.

theorem TauCeti.Manifold.isNormalDomain_ball_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F) {r : ℝ} (hr : 0 < r) : IsNormalDomain (modelWithCornersSelf ℝ F) F p (Metric.ball 0 r)

In a finite-dimensional inner-product space, every tangent ball of positive radius is a normal domain; its normal neighbourhood is the ball of the same radius about the base point (image_riemannianExp_ball_model_space).

theorem TauCeti.Manifold.riemannianLog_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {p q : F} {U : Set (TangentSpace (modelWithCornersSelf ℝ F) p)} (hq : (NormedSpace.fromTangentSpace p).symm (q - p) ∈ U) : riemannianLog (modelWithCornersSelf ℝ F) F p U q = (NormedSpace.fromTangentSpace p).symm (q - p)

The Riemannian logarithm of a finite-dimensional inner-product space at p sends q to q - p, read in T_p F, whenever this vector lies in the chosen set of tangent vectors.

@[simp]

theorem TauCeti.Manifold.riemannianLog_ball_model_space {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {p q : F} {r : ℝ} (hq : q ∈ Metric.ball p r) : riemannianLog (modelWithCornersSelf ℝ F) F p (Metric.ball 0 r) q = (NormedSpace.fromTangentSpace p).symm (q - p)

On the ball of radius r about p in a finite-dimensional inner-product space, the Riemannian logarithm relative to the tangent ball of radius r sends q to q - p, read in T_p F.