English
The length of a path in a manifold, defined via an integral of the measure of its mfderiv, is a well-defined ENRN length function with respect to ENorm data along the path.
Русский
Длина пути в многообразии определяется как интеграл нормы производной вдоль пути; это корректная мера длины пути в рамках заданной структуры.
LaTeX
$$$$\\text{pathELength}(I,\\gamma, a, b)=\\int_{a}^{b} \\|\\mathrm{mfderiv}(I,\\gamma(t))\\|_e\, dt.$$$$
Lean4
/-- The length on `Icc a b` of a path into a manifold, where the path is defined on the whole real
line.
We use the whole real line to avoid subtype hell in API, but this is equivalent to
considering functions on the manifold with boundary `Icc a b`, see
`lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc`.
We use `mfderiv` instead of `mfderivWithin` in the definition as these coincide (apart from the two
endpoints which have zero measure) and `mfderiv` is easier to manipulate. However, we give
a lemma `pathELength_eq_integral_mfderivWithin_Icc` to rewrite with the `mfderivWithin` form. -/
def pathELength :=
val_proj @wrapped✝.{}
