English
If γ is defined on Icc(a,b), then the lintegral of the norm of mfderivWithin equals the path length of γ projected to Icc(a,b).
Русский
Если γ задан на Icc(a,b), то лин-интеграл нормы mfderivWithin равен длине траектории γ после проекции на Icc(a,b).
LaTeX
$$∫⁻ t, ‖mfderivWithin 𝓘(ℝ) I γ (Icc a b) t 1‖ₑ = pathELength I (γ ∘ (projIcc a b h.out.le)) a b$$
Lean4
/-- Given a path `γ` defined on the manifold with boundary `[a, b]`, its length (as the integral of
the norm of its manifold derivative) coincides with `pathELength` of the lift of `γ` to the real
line, between `a` and `b`. -/
theorem lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc {a b : ℝ} [h : Fact (a < b)] {γ : Icc a b → M} :
∫⁻ t, ‖mfderiv (𝓡∂ 1) I γ t 1‖ₑ = pathELength I (γ ∘ (projIcc a b h.out.le)) a b :=
by
rw [pathELength_eq_lintegral_mfderivWithin_Icc]
simp_rw [← mfderivWithin_comp_projIcc_one]
have : MeasurePreserving (Subtype.val : Icc a b → ℝ) volume (volume.restrict (Icc a b)) :=
measurePreserving_subtype_coe measurableSet_Icc
rw [← MeasurePreserving.lintegral_comp_emb this (MeasurableEmbedding.subtype_coe measurableSet_Icc)]
congr
ext t
have : t = projIcc a b h.out.le (t : ℝ) := by simp
congr
