English
Let I be a Riemannian structure on M and γ: ℝ → M a rectifiable path from a to b. Then the length of γ equals the lintegral over the closed interval [a,b] of the norm of the manifold derivative within Icc(a,b).
Русский
Пусть I задаёт риманнову структуру на M, и γ: ℝ → M — путь от a до b. Тогда длина пути γ равна лин-интегралу по замкнутому отрезку [a,b] от нормы mfderivWithin внутри Icc(a,b).
LaTeX
$$$pathELength\\ I\\ γ\\ a\\ b = \\int\\!\\!⁻ t \\in Icc(a,b), \\left\\| mfderivWithin\\ 𝓘(\\mathbb{R})\\ I\\ γ\\ (Icc\\ a\\ b)\\ t\\ 1 \\right\\|_{e}$$$
Lean4
theorem pathELength_eq_lintegral_mfderivWithin_Icc :
pathELength I γ a b = ∫⁻ t in Icc a b, ‖mfderivWithin 𝓘(ℝ) I γ (Icc a b) t 1‖ₑ := by
-- we use that the endpoints have measure 0 to rewrite on `Ioo a b`, where `mfderiv` and
-- `mfderivWithin` coincide.
rw [pathELength_eq_lintegral_mfderiv_Icc, ← restrict_Ioo_eq_restrict_Icc]
apply setLIntegral_congr_fun measurableSet_Ioo (fun t ht ↦ ?_)
rw [mfderivWithin_of_mem_nhds]
exact Icc_mem_nhds ht.1 ht.2
