Riemannian manifolds

A Riemannian manifold M is a real manifold such that its tangent spaces are endowed with an inner product, depending smoothly on the point, and such that M has an emetric space structure for which the distance is the infimum of lengths of paths.

We register a Prop-valued typeclass IsRiemannianManifold I M recording this fact, building on top of [EMetricSpace M] [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)].

We show that an inner product vector space, with the associated canonical Riemannian metric, satisfies the predicate IsRiemannianManifold 𝓘(ℝ, E) E.

In a general manifold with a Riemannian metric, we define the associated extended distance in the manifold, and show that it defines the same topology as the pre-existing one. Therefore, one may endow the manifold with an emetric space structure, see EmetricSpace.ofRiemannianMetric. By definition, it then satisfies the predicate IsRiemannianManifold I M.

The following code block is the standard way to say "Let M be a C^∞ Riemannian manifold".

variable
  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  {M : Type*} [EMetricSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
  [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
  [IsContMDiffRiemannianBundle I ∞ E (fun (x : M) ↦ TangentSpace I x)]
  [IsRiemannianManifold I M]

To register a C^n manifold for a general n, one should replace [IsManifold ∞ I M] with [IsManifold I n M] [IsManifold I 1 M], where the second one is needed to ensure that the tangent bundle is well behaved (not necessary when n is concrete like 2 or 3 as there are automatic instances for these cases). One can require whatever regularity one wants in the IsContMDiffRiemannianBundle instance above, for example [IsContMDiffRiemannianBundle I n E (fun (x : M) ↦ TangentSpace I x)], and one should also add [IsContinuousRiemannianBundle E (fun (x : M) ↦ TangentSpace I x)] (as above, Lean can not infer the latter from the former as it can not guess n).

class IsRiemannianManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] : Prop

Consider a manifold in which the tangent spaces are already endowed with an inner product, and the space is already endowed with an extended distance. We say that this is a Riemannian manifold if the distance is given by the infimum of the lengths of C^1 paths, measured using the norm in the tangent spaces.

This is a Prop valued typeclass, on top of existing data.

If you need to construct a distance using a Riemannian structure, see EmetricSpace.ofRiemannianMetric.

• out (x y : M) : edist x y = Manifold.riemannianEDist I x y

Riemannian structure on an inner product vector space

We endow an inner product vector space with the canonical Riemannian metric, given by the inner product of the vector space in each of the tangent spaces, and we show that this construction satisfies the IsRiemannianManifold 𝓘(ℝ, E) E predicate, i.e., the extended distance between two points is the infimum of the length of paths between these points.

noncomputable def riemannianMetricVectorSpace (F : Type u_4) [NormedAddCommGroup F] [InnerProductSpace ℝ F] : Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ F) ⊤ F fun (x : F) => TangentSpace (modelWithCornersSelf ℝ F) x

The standard riemannian metric on a vector space with an inner product, given by this inner product on each tangent space.

Equations

• riemannianMetricVectorSpace F = { inner := fun (x : F) => innerSL ℝ, symm := ⋯, pos := ⋯, isVonNBounded := ⋯, contMDiff := ⋯ }

noncomputable instance instRiemannianBundleTangentSpaceRealModelWithCornersSelf {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : Bundle.RiemannianBundle fun (x : F) => TangentSpace (modelWithCornersSelf ℝ F) x

Equations

• instRiemannianBundleTangentSpaceRealModelWithCornersSelf = { g := (riemannianMetricVectorSpace F).toRiemannianMetric }

theorem norm_tangentSpace_vectorSpace {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {v : TangentSpace (modelWithCornersSelf ℝ F) x} : ‖v‖ = ‖v‖

theorem nnnorm_tangentSpace_vectorSpace {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {v : TangentSpace (modelWithCornersSelf ℝ F) x} : ‖v‖₊ = ‖v‖₊

theorem enorm_tangentSpace_vectorSpace {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {v : TangentSpace (modelWithCornersSelf ℝ F) x} : ‖v‖ₑ = ‖v‖ₑ

theorem lintegral_fderiv_lineMap_eq_edist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} : ∫⁻ (t : ℝ) in Set.Icc 0 1, ‖(fderivWithin ℝ (⇑(ContinuousAffineMap.lineMap x y)) (Set.Icc 0 1) t) 1‖ₑ = edist x y

instance instIsRiemannianManifoldModelWithCornersSelfReal {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] : IsRiemannianManifold (modelWithCornersSelf ℝ F) F

An inner product vector space is a Riemannian manifold, i.e., the distance between two points is the infimum of the lengths of paths between these points.

Constructing a distance from a Riemannian structure

Let M be a real manifold with a Riemannian structure. We construct the associated distance and show that the associated topology coincides with the pre-existing topology. Therefore, one may endow M with an emetric space structure, called EmetricSpace.ofRiemannianMetric. Moreover, we show that in this case the resulting emetric space satisfies the predicate IsRiemannianManifold I M.

Showing that the distance topology coincides with the pre-existing topology is not trivial. The two inclusions are proved respectively in eventually_riemmanianEDist_lt and setOf_riemmanianEDist_lt_subset_nhds.

For the first one, we have to show that points which are close for the topology are at small distance. For this, we use the path between the two points which is the pullback of the segment in the extended chart, and argue that it is short because the images are close in the extended chart.

For the second one, we have to show that any neighborhood of x contains all the points y with riemannianEDist x y < c for some c > 0. For this, we argue that a short path from x to y remains short in the extended chart, and therefore it doesn't have the time to exit the image of the neighborhood in the extended chart.

def normedAddCommGroupTangentSpaceVectorSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : NormedAddCommGroup (TangentSpace (modelWithCornersSelf ℝ E) x)

Register on the tangent space to a normed vector space the same NormedAddCommGroup structure as in the vector space.

Should not be a global instance, as it does not coincide definitionally with the Riemannian structure for inner product spaces, but can be activated locally.

Equations

• normedAddCommGroupTangentSpaceVectorSpace x = inferInstanceAs (NormedAddCommGroup E)

def normedSpaceTangentSpaceVectorSpace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (x : E) : NormedSpace ℝ (TangentSpace (modelWithCornersSelf ℝ E) x)

Register on the tangent space to a normed vector space the same NormedSpace structure as in the vector space.

Should not be a global instance, as it does not coincide definitionally with the Riemannian structure for inner product spaces, but can be activated locally.

Equations

• normedSpaceTangentSpaceVectorSpace x = inferInstanceAs (NormedSpace ℝ E)

theorem eventually_norm_mfderiv_extChartAt_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) : ∃ C > 0, ∀ᶠ (y : M) in nhds x, ‖mfderiv I (modelWithCornersSelf ℝ E) (↑(extChartAt I x)) y‖ < C

theorem eventually_enorm_mfderiv_extChartAt_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) : ∃ C > 0, ∀ᶠ (y : M) in nhds x, ‖mfderiv I (modelWithCornersSelf ℝ E) (↑(extChartAt I x)) y‖ₑ < ↑C

theorem eventually_norm_mfderivWithin_symm_extChartAt_comp_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) : ∃ C > 0, ∀ᶠ (y : M) in nhds x, ‖mfderivWithin (modelWithCornersSelf ℝ E) I (↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) y)‖ < C

theorem eventually_norm_mfderivWithin_symm_extChartAt_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) : ∃ C > 0, ∀ᶠ (y : E) in nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I), ‖mfderivWithin (modelWithCornersSelf ℝ E) I (↑(extChartAt I x).symm) (Set.range ↑I) y‖ < C

theorem eventually_enorm_mfderivWithin_symm_extChartAt_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) : ∃ C > 0, ∀ᶠ (y : E) in nhdsWithin (↑(extChartAt I x) x) (Set.range ↑I), ‖mfderivWithin (modelWithCornersSelf ℝ E) I (↑(extChartAt I x).symm) (Set.range ↑I) y‖ₑ < ↑C

theorem eventually_riemannianEDist_le_edist_extChartAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) : ∃ C > 0, ∀ᶠ (y : M) in nhds x, Manifold.riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)

Around any point x, the Riemannian distance between two points is controlled by the distance in the extended chart. In other words, the extended chart is locally Lipschitz.

theorem eventually_riemmanianEDist_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) {c : ENNReal} (hc : 0 < c) : ∀ᶠ (y : M) in nhds x, Manifold.riemannianEDist I x y < c

If points are close for the topology, then their Riemannian distance is small.

theorem setOf_riemmanianEDist_lt_subset_nhds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [RegularSpace M] {x : M} {s : Set M} (hs : s ∈ nhds x) : ∃ c > 0, {y : M | Manifold.riemannianEDist I x y < ↑c} ⊆ s

Any neighborhood of x contains all the points which are close enough to x for the Riemannian distance, ℝ≥0 version.

theorem setOf_riemmanianEDist_lt_subset_nhds' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [RegularSpace M] {x : M} {s : Set M} (hs : s ∈ nhds x) : ∃ c > 0, {y : M | Manifold.riemannianEDist I x y < c} ⊆ s

Any neighborhood of x contains all the points which are close enough to x for the Riemannian distance, ℝ≥0∞ version.

@[reducible]

def PseudoEmetricSpace.ofRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [RegularSpace M] : PseudoEMetricSpace M

The pseudoemetric space structure associated to a Riemannian metric on a manifold. Designed so that the topology is defeq to the original one.

This should only be used when constructing data in specific situtations. To develop the theory, one should rather assume that there is an already existing emetric space structure, which satisfies additionally the predicate IsRiemannianManifold I M.

Equations

• PseudoEmetricSpace.ofRiemannianMetric I M = PseudoEmetricSpace.ofEdistOfTopology (Manifold.riemannianEDist I) ⋯ ⋯ ⋯ ⋯

instance instIsRiemannianManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [RegularSpace M] : IsRiemannianManifold I M

Given a manifold with a Riemannian metric, consider the associated Riemannian distance. Then by definition the distance is the infimum of the length of paths between the points, i.e., the manifold satsifies the IsRiemannianManifold I M predicate.

@[reducible]

def EmetricSpace.ofRiemannianMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [T3Space M] : EMetricSpace M

The emetric space structure associated to a Riemannian metric on a manifold. Designed so that the topology is defeq to the original one.

This should only be used when constructing data in specific situations. To develop the theory, one should rather assume that there is an already existing emetric space structure, which satisfies additionally the predicate IsRiemannianManifold I M.

Equations

• EmetricSpace.ofRiemannianMetric I M = EMetricSpace.ofT0PseudoEMetricSpace M