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.

Author: sgouezel

Mathlib.lean

@@ -3733,6 +3733,7 @@ import Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
 import Mathlib.Geometry.Manifold.Metrizable
 import Mathlib.Geometry.Manifold.PartitionOfUnity
 import Mathlib.Geometry.Manifold.PoincareConjecture
+import Mathlib.Geometry.Manifold.Riemannian.PathELength
 import Mathlib.Geometry.Manifold.Sheaf.Basic
 import Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
 import Mathlib.Geometry.Manifold.Sheaf.Smooth

Mathlib/Analysis/Normed/MulAction.lean

@@ -109,6 +109,15 @@ instance (priority := 100) NormMulClass.toNormSMulClass_op [SeminormedRing α] [
     NormSMulClass αᵐᵒᵖ α where
   norm_smul a b := mul_comm ‖b‖ ‖a‖ ▸ norm_mul b a.unop
 
+/-- Mixin class for scalar-multiplication actions with a strictly multiplicative norm, i.e.
+`‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ`. -/
+class ENormSMulClass (α β : Type*) [ENorm α] [ENorm β] [SMul α β] : Prop where
+  protected enorm_smul (r : α) (x : β) : ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ
+
+lemma enorm_smul [ENorm α] [ENorm β] [SMul α β] [ENormSMulClass α β] (r : α) (x : β) :
+    ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ :=
+  ENormSMulClass.enorm_smul r x
+
 variable [SeminormedRing α] [SeminormedAddGroup β] [SMul α β]
 
 theorem NormSMulClass.of_nnnorm_smul (h : ∀ (r : α) (x : β), ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊) :
@@ -120,7 +129,8 @@ variable [NormSMulClass α β]
 theorem nnnorm_smul (r : α) (x : β) : ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊ :=
   NNReal.eq <| norm_smul r x
 
-lemma enorm_smul (r : α) (x : β) : ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ := by simp [enorm, nnnorm_smul]
+instance (priority := 100) : ENormSMulClass α β where
+  enorm_smul r x := by simp [enorm, nnnorm_smul]
 
 instance Pi.instNormSMulClass {ι : Type*} {β : ι → Type*} [Fintype ι]
     [SeminormedRing α] [∀ i, SeminormedAddGroup (β i)] [∀ i, SMul α (β i)]

Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

@@ -214,6 +214,11 @@ theorem exists_mem_iterate_mem [IsFiniteMeasure μ] (hf : MeasurePreserving f μ
 
 end MeasurePreserving
 
+lemma measurePreserving_subtype_coe {s : Set α} (hs : MeasurableSet s) :
+    MeasurePreserving (Subtype.val : s → α) (μa.comap Subtype.val) (μa.restrict s) where
+  measurable := measurable_subtype_coe
+  map_eq := map_comap_subtype_coe hs _
+
 namespace MeasurableEquiv
 
 theorem measurePreserving_symm (μ : Measure α) (e : α ≃ᵐ β) :

Mathlib/Geometry/Manifold/ContMDiff/Basic.lean

@@ -259,6 +259,39 @@ alias contMDiffAt_of_not_mem := contMDiffAt_of_notMem
 @[to_additive existing contMDiffAt_of_not_mem, deprecated (since := "2025-05-23")]
 alias contMDiffAt_of_not_mem_mulTSupport := contMDiffAt_of_notMem_mulTSupport
 
+/-- Given two `C^n` functions `f` and `g` which coincide locally around the frontier of a set `s`,
+then the piecewise function defined using `f` on `s` and `g` elsewhere is `C^n`. -/
+lemma ContMDiff.piecewise
+    {f g : M → M'} {s : Set M} [DecidablePred (· ∈ s)]
+    (hf : ContMDiff I I' n f) (hg : ContMDiff I I' n g)
+    (hfg : ∀ x ∈ frontier s, f =ᶠ[𝓝 x] g) :
+    ContMDiff I I' n (piecewise s f g) := by
+  intro x
+  by_cases hx : x ∈ interior s
+  · apply (hf x).congr_of_eventuallyEq
+    filter_upwards [isOpen_interior.mem_nhds hx] with y hy
+    rw [piecewise_eq_of_mem]
+    apply interior_subset hy
+  by_cases h'x : x ∈ closure s
+  · have : x ∈ frontier s := ⟨h'x, hx⟩
+    apply (hf x).congr_of_eventuallyEq
+    filter_upwards [hfg x this] with y hy
+    simp [Set.piecewise, hy]
+  · apply (hg x).congr_of_eventuallyEq
+    filter_upwards [isClosed_closure.isOpen_compl.mem_nhds h'x] with y hy
+    rw [piecewise_eq_of_notMem]
+    contrapose! hy
+    simpa using subset_closure hy
+
+/-- Given two `C^n` functions `f` and `g` from `ℝ` to a real manifold which coincide locally
+around a point `s`, then the piecewise function using `f` before `t` and `g` after is `C^n`. -/
+lemma ContMDiff.piecewise_Iic
+    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H]
+    {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
+    {f g : ℝ → M} {s : ℝ}
+    (hf : ContMDiff 𝓘(ℝ) I n f) (hg : ContMDiff 𝓘(ℝ) I n g) (hfg : f =ᶠ[𝓝 s] g) :
+    ContMDiff 𝓘(ℝ) I n (Set.piecewise (Iic s) f g) :=
+  hf.piecewise hg (by simpa using hfg)
 
 /-! ### Being `C^k` on a union of open sets can be tested on each set -/
 section contMDiff_union