Coordinate displacement is bounded by Riemannian path length

This file supplies local analytic bridges between the Riemannian distance and coordinate charts. If the chart derivative is bounded along a C¹ path, the coordinate displacement of the path is bounded by that derivative bound times its Riemannian length. Fix a point x and r > 1. Every continuous linear map from T_x M to a real normed space, read in the extended chart at x, satisfies a Lipschitz bound at the base point x for the Riemannian distance: for all y in a neighbourhood of x (depending on r), its displacement from x to y is at most r times its norm times the distance from x to y.

This is the chart-level estimate needed when transferring vector-valued variation estimates to Manifold.pathELength in the Hopf--Rinow lower-semicontinuity argument. The proof uses the interval-integral estimate enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc and the chain rule for mfderivWithin.

The interval-integral estimate and the local-coordinate differential argument follow the corresponding constructions in Mathlib's Geometry/Manifold/Riemannian/Basic.lean.

Main results

• TauCeti.Manifold.enorm_sub_le_mul_pathELength: a differential bound along a differentiable path controls the displacement of a function whose composition with the path is C¹.
• TauCeti.Manifold.enorm_extChartAt_sub_le_mul_pathELength: the chart-valued specialization.
• ContinuousLinearMap.enorm_apply_extChartAt_sub_le_mul_pathELength: the specialization to a continuous linear map applied to chart coordinates, with a bound on chart distortion.
• TauCeti.Manifold.eventually_enorm_apply_extChartAt_sub_le: the sharp local chart--distance estimate for continuous linear maps.
• TauCeti.Manifold.edist_le_mul_riemannianEDist: a C¹ map whose differential stretches tangent vectors by at most C ≠ 0 is C-Lipschitz from the Riemannian distance.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 7 §2.

theorem TauCeti.Manifold.enorm_sub_le_mul_pathELength {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → F} {γ : ℝ → M} {a b : ℝ} (hab : a ≤ b) (hγ : MDiff[Set.Icc a b] γ) (hf : ContMDiffOn (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ F) 1 (f ∘ γ) (Set.Icc a b)) (hfdiff : ∀ t ∈ Set.Icc a b, MDiffAt f (γ t)) {C : NNReal} (hC : ∀ t ∈ Set.Icc a b, ‖(mfderiv% f (γ t)) ((mfderiv[Set.Icc a b] γ t) 1)‖ₑ ≤ ↑C * ‖(mfderiv[Set.Icc a b] γ t) 1‖ₑ) : ‖f (γ b) - f (γ a)‖ₑ ≤ ↑C * Manifold.pathELength I γ a b

A bound on the differential of a vector-valued function applied to the within-derivative of a differentiable path controls the displacement of the function along that path, provided the composition is C¹.

theorem TauCeti.Manifold.enorm_extChartAt_sub_le_mul_pathELength {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] (x : M) {γ : ℝ → M} {a b : ℝ} (hab : a ≤ b) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (hγsrc : ∀ t ∈ Set.Icc a b, γ t ∈ (chartAt H x).source) {C : NNReal} (hC : ∀ t ∈ Set.Icc a b, ‖(mfderiv% ↑(extChartAt I x) (γ t)) ((mfderiv[Set.Icc a b] γ t) 1)‖ₑ ≤ ↑C * ‖(mfderiv[Set.Icc a b] γ t) 1‖ₑ) : ‖↑(extChartAt I x) (γ b) - ↑(extChartAt I x) (γ a)‖ₑ ≤ ↑C * Manifold.pathELength I γ a b

A chart-valued instance of enorm_sub_le_mul_pathELength.

theorem ContinuousLinearMap.enorm_apply_extChartAt_sub_le_mul_pathELength {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] {x : M} {r : ℝ} (ℓ : TangentSpace I x →L[ℝ] F) {γ : ℝ → M} {a b : ℝ} (hab : a ≤ b) (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (hmem : ∀ s ∈ Set.Icc a b, γ s ∈ (chartAt H x).source ∧ ‖Bundle.Trivialization.symmL ℝ (trivializationAt E (fun (x : M) => TangentSpace I x) x) x ∘SL Bundle.Trivialization.continuousLinearMapAt ℝ (trivializationAt E (fun (x : M) => TangentSpace I x) x) (γ s)‖ ≤ r) : ‖ℓ (↑(extChartAt I x) (γ b) - ↑(extChartAt I x) (γ a))‖ₑ ≤ ENNReal.ofReal r * ‖ℓ‖ₑ * Manifold.pathELength I γ a b

Along a C¹ path which stays where the chart at x distorts Riemannian norms by at most r, a continuous linear map ℓ from T_x M to F, read in that chart, changes by at most r ‖ℓ‖ times the length of the path.

theorem TauCeti.Manifold.edist_le_mul_riemannianEDist {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {f : M → F} (hf : ContMDiff I (modelWithCornersSelf ℝ F) 1 f) {C : NNReal} (hC0 : C ≠ 0) (hC : ∀ (x : M) (v : TangentSpace I x), ‖(d% f x) v‖ₑ ≤ ↑C * ‖v‖ₑ) (x y : M) : edist (f x) (f y) ≤ ↑C * Manifold.riemannianEDist I x y

A map with bounded differential is Lipschitz for the Riemannian distance. If a C¹ map f to a real normed space stretches every tangent vector by a factor at most C ≠ 0, then the distance between the images of two points is at most C times their Riemannian distance. The condition C ≠ 0 cannot be dropped: a locally constant map has zero differential, while points of different components are at infinite Riemannian distance and 0 * ∞ = 0.

theorem TauCeti.Manifold.eventually_enorm_apply_extChartAt_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_4} [PseudoEMetricSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I 1 M] [IsRiemannianManifold I M] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (x : M) {r : ℝ} (hr : 1 < r) : ∀ᶠ (y : M) in nhds x, ∀ (ℓ : TangentSpace I x →L[ℝ] F), ‖ℓ (↑(extChartAt I x) y - ↑(extChartAt I x) x)‖ₑ ≤ ENNReal.ofReal r * ‖ℓ‖ₑ * edist x y

Sharp local Lipschitz bound for the extended chart. For r > 1, near x every continuous linear map ℓ from T_x M to a real normed space, read in the extended chart at x, is (r ‖ℓ‖)-Lipschitz at x for the Riemannian distance.