Arclength factorization of rectifiable metric curves #
A continuous curve of bounded variation on a compact real interval factors through cumulative
variation. The resulting curve is 1-Lipschitz on its length interval and has variation equal to
the parameter difference on every subinterval. The construction collapses constant pieces;
it does not require an inverse to cumulative variation. It also applies to constant curves,
whose length interval is a singleton.
For curves injective on the interior of their parameter interval, cumulative variation induces
an increasing homeomorphism between the original parameter interval and the length interval.
This includes injective arcs and simple closed curves.
On its length interval, the factor is Mathlib's naturalParameterization.
We use Mathlib's variationOnFromTo, its continuity criterion, and the exact variation formula
for composition with a monotone map. Length is always eVariationOn; its conversion to a real
parameter is justified by the bounded-variation hypothesis.
References #
- L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows, second edition, §1.1 (arclength parametrization of metric curves).
The natural parameterization of a curve of locally bounded variation on s recovers the
curve at the cumulative variation of each point of s.
The natural parameterization of a curve of locally bounded variation has the same trace when restricted to the set of cumulative variations from a base point.
The natural parameterization of a curve of locally bounded variation on s starts, at
parameter 0, at the value of the curve at the base point.
The natural parameterization of a curve of bounded variation on [a, b] ends, at the length
L of the curve, at γ b.
If a curve of bounded variation on [a, b] (a ≤ b) has equal endpoint values γ a = γ b,
then its natural parameterization takes equal values at 0 and at the length of the curve.
Cumulative variation maps the parameter interval of a continuous rectifiable curve onto its length interval.
A continuous rectifiable curve factors through a 1-Lipschitz curve on its length interval. The factor has exactly the parameter difference as variation on every subinterval, including when the original curve has pauses or zero length. Values of the factor outside its length interval are unspecified.
The arclength factor of a continuous rectifiable curve is unique on its length interval:
a curve g with g ∘ variationOnFromTo γ (Icc a b) a = γ on [a, b] agrees there with the
natural parameterization.
The natural parameterization of a continuous rectifiable curve traces, on its length interval, the same set as the curve on its parameter interval.
The natural parameterization of a continuous rectifiable curve has unit speed on its length interval.
The natural parameterization of a continuous rectifiable curve has, on its length interval, the same length as the curve.
For a continuous rectifiable curve injective on the interior of its parameter interval, cumulative variation is an increasing homeomorphism onto the length interval. The endpoint values may coincide, and the singleton interval case is included.
A rectifiable curve injective on the open interval (a, b) with a < b has strictly positive
total variation.
Composing a continuous rectifiable curve with an increasing continuous map onto [a, b]
leaves its natural parameterization unchanged on the length interval.
Composing a continuous rectifiable curve with a decreasing continuous map onto [a, b]
reverses its natural parameterization on the length interval.
If γ = g ∘ s on [a, b] with s monotone, then the values of γ on the intervals where
s is constant form a countable set: each such interval contains a rational parameter. For
example, the values a curve takes while its cumulative arclength pauses form a countable set.