English
If a path γ is defined on Icc(a,b), then the lintegral of the derivative's norm equals the path length of γ projected to Icc(a,b).
Русский
Если путь γ задан на Icc(a,b), лин-интеграл нормы производной равен длине траектории γ после проекции на Icc(a,b).
LaTeX
$$lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc$$
Lean4
/-- 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 exists_lt_locally_constant_of_riemannianEDist_lt (hr : riemannianEDist I x y < r) (hab : a < b) :
∃ γ : ℝ → M,
γ a = x ∧
γ b = y ∧ ContMDiff 𝓘(ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ γ =ᶠ[𝓝 a] (fun _ ↦ x) ∧ γ =ᶠ[𝓝 b] (fun _ ↦ y) :=
by
/- We start from a path from `x` to `y` defined on `[0, 1]` with length `< r`. Then, we
reparameterize it using a smooth monotone map `η` from `[a, b]` to `[0, 1]` which is moreover
locally constant around `a` and `b`.
Such a map is easy to build with `Real.smoothTransition`.
Note that this is a very standard construction in differential topology.
TODO: refactor once we have more differential topology in Mathlib and this gets duplicated. -/
rcases exists_lt_of_riemannianEDist_lt hr with ⟨γ, hγx, hγy, γ_smooth, hγ⟩
rcases exists_between hab with ⟨a', haa', ha'b⟩
rcases exists_between ha'b with ⟨b', ha'b', hb'b⟩
let η (t : ℝ) : ℝ := Real.smoothTransition ((b' - a')⁻¹ * (t - a'))
have A (t) (ht : t < a') : η t = 0 :=
by
simp only [η, Real.smoothTransition.zero_iff_nonpos]
apply mul_nonpos_of_nonneg_of_nonpos
· simpa using ha'b'.le
· linarith
have A' (t) (ht : t < a') : (γ ∘ η) t = x := by simp [A t ht, hγx]
have B (t) (ht : b' < t) : η t = 1 :=
by
simp only [η, Real.smoothTransition.eq_one_iff_one_le, inv_mul_eq_div]
rw [one_le_div₀] <;> linarith
have B' (t) (ht : b' < t) : (γ ∘ η) t = y := by simp [B t ht, hγy]
refine ⟨γ ∘ η, A' _ haa', B' _ hb'b, ?_, ?_, ?_, ?_⟩
· rw [← contMDiffOn_univ]
apply γ_smooth.comp
· rw [contMDiffOn_univ, contMDiff_iff_contDiff]
fun_prop
· intro t ht
exact ⟨Real.smoothTransition.nonneg _, Real.smoothTransition.le_one _⟩
· convert hγ using 1
rw [← A a haa', ← B b hb'b]
apply pathELength_comp_of_monotoneOn hab.le
· apply Monotone.monotoneOn
apply Real.smoothTransition.monotone.comp
intro t u htu
dsimp only
gcongr
simpa only [inv_nonneg, sub_nonneg] using ha'b'.le
· simp only [η]
apply (ContDiff.contDiffOn _).differentiableOn le_rfl
fun_prop
· rw [A a haa', B b hb'b]
apply γ_smooth.mdifferentiableOn le_rfl
· filter_upwards [Iio_mem_nhds haa'] with t ht using A' t ht
· filter_upwards [Ioi_mem_nhds hb'b] with t ht using B' t ht
