English
The natural parameterization f on s is defined via the inverse of variationOnFromTo and has the property that it is unit speed if f has locally bounded variation on s; the composed version is at distance zero from f.
Русский
Естественная параметризация f на s задается через обратную функцию variationOnFromTo; она имеет единичную скорость при локально ограниченной вариации на s, а образованная композиция приближает f к нулю по евклидовому расстоянию.
LaTeX
$$naturalParameterization(f,s,a) = f ∘ Function.invFunOn(variationOnFromTo f s a) s$$
Lean4
/-- The natural parameterization of `f` on `s`, which, if `f` has locally bounded variation on `s`,
* has unit speed on `s` (by `has_unit_speed_naturalParameterization`).
* composed with `variationOnFromTo f s a`, is at distance zero from `f`
(by `edist_naturalParameterization_eq_zero`).
-/
noncomputable def naturalParameterization (f : α → E) (s : Set α) (a : α) : ℝ → E :=
f ∘ @Function.invFunOn _ _ ⟨a⟩ (variationOnFromTo f s a) s
