Lengths of paths in manifolds

Consider a manifold in which the tangent spaces have an enormed structure. Then one defines pathELength γ a b as the length of the path γ : ℝ → M between a and b, i.e., the integral of the norm of its derivative on Icc a b.

We give several ways to write this quantity (as an integral over Icc, or Ioo, or the subtype Icc, using either mfderiv or mfderivWithin).

We show that this notion is invariant under reparameterization by a monotone map, in pathELength_comp_of_monotoneOn.

We define riemannianEDist x y as the infimum of the length of C^1 paths between x and y. We prove, in exists_lt_locally_constant_of_riemannianEDist_lt, that it is also the infimum on such path that are moreover locally constant near their endpoints. Such paths can be glued while retaining the C^1 property. We deduce that riemannianEDist satisfies the triangle inequality, in riemannianEDist_triangle.

Note that riemannianEDist x y could also be named finslerEDist x y as we do not require that the metric comes from an inner product space. However, as all the current applications in mathlib are to Riemannian spaces we stick with the simpler name. This could be changed when Finsler manifolds are studied in mathlib.

@[irreducible]

def Manifold.pathELength {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [(x : M) → ENorm (TangentSpace I x)] (γ : ℝ → M) (a b : ℝ) : ENNReal

The length on Icc a b of a path into a manifold, where the path is defined on the whole real line.

We use the whole real line to avoid subtype hell in API, but this is equivalent to considering functions on the manifold with boundary Icc a b, see lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc.

We use mfderiv instead of mfderivWithin in the definition as these coincide (apart from the two endpoints which have zero measure) and mfderiv is easier to manipulate. However, we give a lemma pathELength_eq_integral_mfderivWithin_Icc to rewrite with the mfderivWithin form.

Equations

• Manifold.pathELength I γ a b = ∫⁻ (t : ℝ) in Set.Icc a b, ‖(mfderiv (modelWithCornersSelf ℝ ℝ) I γ t) 1‖ₑ

theorem Manifold.pathELength_def {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [(x : M) → ENorm (TangentSpace I x)] (γ : ℝ → M) (a b : ℝ) : pathELength I γ a b = ∫⁻ (t : ℝ) in Set.Icc a b, ‖(mfderiv (modelWithCornersSelf ℝ ℝ) I γ t) 1‖ₑ

theorem Manifold.pathELength_eq_lintegral_mfderiv_Icc {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] [(x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M} : pathELength I γ a b = ∫⁻ (t : ℝ) in Set.Icc a b, ‖(mfderiv (modelWithCornersSelf ℝ ℝ) I γ t) 1‖ₑ

theorem Manifold.pathELength_eq_lintegral_mfderiv_Ioo {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] [(x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M} : pathELength I γ a b = ∫⁻ (t : ℝ) in Set.Ioo a b, ‖(mfderiv (modelWithCornersSelf ℝ ℝ) I γ t) 1‖ₑ

theorem Manifold.pathELength_eq_lintegral_mfderivWithin_Icc {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] [(x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M} : pathELength I γ a b = ∫⁻ (t : ℝ) in Set.Icc a b, ‖(mfderivWithin (modelWithCornersSelf ℝ ℝ) I γ (Set.Icc a b) t) 1‖ₑ

@[simp]

theorem Manifold.pathELength_self {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] [(x : M) → ENorm (TangentSpace I x)] {a : ℝ} {γ : ℝ → M} : pathELength I γ a a = 0

theorem Manifold.pathELength_congr_Ioo {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] [(x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ γ' : ℝ → M} (h : Set.EqOn γ γ' (Set.Ioo a b)) : pathELength I γ a b = pathELength I γ' a b

theorem Manifold.pathELength_congr {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] [(x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ γ' : ℝ → M} (h : Set.EqOn γ γ' (Set.Icc a b)) : pathELength I γ a b = pathELength I γ' a b

theorem Manifold.pathELength_mono {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] [(x : M) → ENorm (TangentSpace I x)] {a b a' b' : ℝ} {γ : ℝ → M} (h : a' ≤ a) (h' : b ≤ b') : pathELength I γ a b ≤ pathELength I γ a' b'

theorem Manifold.pathELength_add {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] [(x : M) → ENorm (TangentSpace I x)] {a b c : ℝ} {γ : ℝ → M} (h : a ≤ b) (h' : b ≤ c) : pathELength I γ a b + pathELength I γ b c = pathELength I γ a c

theorem Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc {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] [(x : M) → ENorm (TangentSpace I x)] {a b : ℝ} [h : Fact (a < b)] {γ : ↑(Set.Icc a b) → M} : ∫⁻ (t : ↑(Set.Icc a b)), ‖(mfderiv (modelWithCornersEuclideanHalfSpace 1) I γ t) 1‖ₑ = pathELength I (γ ∘ Set.projIcc a b ⋯) a b

Given a path γ defined on the manifold with boundary [a, b], its length (as the integral of the norm of its manifold derivative) coincides with pathELength of the lift of γ to the real line, between a and b.

theorem Manifold.pathELength_comp_of_monotoneOn {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] [(x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M} [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {f : ℝ → ℝ} (h : a ≤ b) (hf : MonotoneOn f (Set.Icc a b)) (h'f : DifferentiableOn ℝ f (Set.Icc a b)) (hγ : MDifferentiableOn (modelWithCornersSelf ℝ ℝ) I γ (Set.Icc (f a) (f b))) : pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b)

The length of a path in a manifold is invariant under a monotone reparametrization.

theorem Manifold.pathELength_comp_of_antitoneOn {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] [(x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M} [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {f : ℝ → ℝ} (h : a ≤ b) (hf : AntitoneOn f (Set.Icc a b)) (h'f : DifferentiableOn ℝ f (Set.Icc a b)) (hγ : MDifferentiableOn (modelWithCornersSelf ℝ ℝ) I γ (Set.Icc (f b) (f a))) : pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)

The length of a path in a manifold is invariant under an antitone reparametrization.

@[irreducible]

noncomputable def Manifold.riemannianEDist {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [(x : M) → ENorm (TangentSpace I x)] (x y : M) : ENNReal

The Riemannian extended distance between two points, in a manifold where the tangent spaces have an extended norm, defined as the infimum of the lengths of C^1 paths between the points.

Equations

• One or more equations did not get rendered due to their size.

theorem Manifold.riemannianEDist_def {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] [(x : M) → ENorm (TangentSpace I x)] (x y : M) : riemannianEDist I x y = ⨅ (γ : Path x y), ⨅ (_ : ContMDiff (modelWithCornersEuclideanHalfSpace 1) I 1 ⇑γ), ∫⁻ (x_2 : ↑unitInterval), ‖(mfderiv (modelWithCornersEuclideanHalfSpace 1) I (⇑γ) x_2) 1‖ₑ

theorem Manifold.riemannianEDist_le_pathELength {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] [(x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x y : M} {a b : ℝ} {γ : ℝ → M} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (ha : γ a = x) (hb : γ b = y) (hab : a ≤ b) : riemannianEDist I x y ≤ pathELength I γ a b

The Riemannian edistance is bounded above by the length of any C^1 path from x to y. Here, we express this using a path defined on the whole real line, considered on some interval [a, b].

theorem Manifold.exists_lt_of_riemannianEDist_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] [(x : M) → ENorm (TangentSpace I x)] {x y : M} {r : ENNReal} (hr : riemannianEDist I x y < r) : ∃ (γ : ℝ → M), γ 0 = x ∧ γ 1 = y ∧ ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc 0 1) ∧ pathELength I γ 0 1 < r

If some r is strictly larger than the Riemannian edistance between two points, there exists a path between these two points of length < r. Here, we get such a path on [0, 1]. For a more precise version giving locally constant paths around the endpoints, see exists_lt_locally_constant_of_riemannianEDist_lt

theorem Manifold.exists_lt_locally_constant_of_riemannianEDist_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] [(x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x y : M} {r : ENNReal} {a b : ℝ} (hr : riemannianEDist I x y < r) (hab : a < b) : ∃ (γ : ℝ → M), γ a = x ∧ γ b = y ∧ ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[nhds a] fun (x_1 : ℝ) => x) ∧ γ =ᶠ[nhds b] fun (x : ℝ) => y

If some r is strictly larger than the Riemannian edistance between two points, there exists a path between these two points of length < r. Here, we get such a path on an arbitrary interval [a, b] with a < b, and moreover we ensure that the path is locally constant around a and b, which is convenient for gluing purposes.

theorem Manifold.riemannianEDist_self {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] [(x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x : M} : riemannianEDist I x x = 0

theorem Manifold.riemannianEDist_comm {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] [(x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x y : M} : riemannianEDist I x y = riemannianEDist I y x

theorem Manifold.riemannianEDist_triangle {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] [(x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x y z : M} : riemannianEDist I x z ≤ riemannianEDist I x y + riemannianEDist I y z