Commit 2025-07-17 17:33 ed84d14c

View on Github →

feat: length of a path in a manifold (#26778) 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 manifold derivative. We develop a reasonable API around this notion We also define riemannianEDist x y as the infimum of the length of paths from x to y. We show that it is symmetric and satisfies the triangle inequality.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/MulAction.lean

modified theorem enorm_smul

Modified Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

added theorem MeasureTheory.measurePreserving_subtype_coe

Modified Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

added theorem ContMDiff.piecewise

added theorem ContMDiff.piecewise_Iic

Created Mathlib/Geometry/Manifold/Riemannian/PathELength.lean

added theorem Manifold.exists_lt_locally_constant_of_riemannianEDist_lt

added theorem Manifold.exists_lt_of_riemannianEDist_lt

added theorem Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc

added theorem Manifold.pathELength_add

added theorem Manifold.pathELength_comp_of_antitoneOn

added theorem Manifold.pathELength_comp_of_monotoneOn

added theorem Manifold.pathELength_congr

added theorem Manifold.pathELength_congr_Ioo

added theorem Manifold.pathELength_eq_lintegral_mfderivWithin_Icc

added theorem Manifold.pathELength_eq_lintegral_mfderiv_Icc

added theorem Manifold.pathELength_eq_lintegral_mfderiv_Ioo

added theorem Manifold.pathELength_mono

added theorem Manifold.pathELength_self

added theorem Manifold.riemannianEDist_comm

added theorem Manifold.riemannianEDist_le_pathELength

added theorem Manifold.riemannianEDist_self

added theorem Manifold.riemannianEDist_triangle