Constant speed and the length of curves of bounded variation

Constant speed bounds distances by elapsed parameter time. Mathlib's natural parameterization therefore shows that the image of any curve of locally bounded variation has Hausdorff dimension at most one. In particular this applies to absolutely continuous planar curves.

The same factorization bounds the one-dimensional Hausdorff measure of the trace of a curve by its total variation, H¹(f '' s) ≤ eVariationOn f s, both for Mathlib's raw Hausdorff measure μH[1] and for the Euclidean normalization μHE[1]. No continuity, injectivity, or finiteness hypothesis is needed: the bound is trivial when the variation is infinite.

Main results

• LocallyBoundedVariationOn.dimH_image_le_one: a curve of locally bounded variation has a trace of Hausdorff dimension at most one.
• eVariationOn.hausdorffMeasure_image_le: μH[1] (f '' s) ≤ eVariationOn f s.
• eVariationOn.euclideanHausdorffMeasure_image_le: μHE[1] (f '' s) ≤ eVariationOn f s.

theorem HasConstantSpeedOnWith.lipschitzOnWith {E : Type u_1} [PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} (hf : HasConstantSpeedOnWith f s l) : LipschitzOnWith l f s

A curve with constant speed is Lipschitz with that speed as its Lipschitz constant.

theorem variationOnFromTo.ediam_image_le {α : Type u_1} {E : Type u_2} [LinearOrder α] [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s : Set α} {a : α} (ha : a ∈ s) : Metric.ediam (variationOnFromTo f s a '' s) ≤ eVariationOn f s

The extended diameter of the set of cumulative variations from a base point of s is at most the total variation on s.

theorem LocallyBoundedVariationOn.image_subset_image_naturalParameterization {α : Type u_1} {E : Type u_2} [LinearOrder α] [EMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (ha : a ∈ s) : f '' s ⊆ naturalParameterization f s a '' variationOnFromTo f s a '' s

A curve of locally bounded variation on s factors, on s, through its natural parameterization restricted to the set of cumulative variations from a base point.

theorem LocallyBoundedVariationOn.dimH_image_le_one {α : Type u_1} {E : Type u_2} [LinearOrder α] [MetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) : dimH (f '' s) ≤ 1

The image of a curve of locally bounded variation has Hausdorff dimension at most one, because its natural parameterization is Lipschitz on a subset of the real line.

theorem eVariationOn.hausdorffMeasure_image_le {α : Type u_1} {E : Type u_2} [LinearOrder α] [EMetricSpace E] [MeasurableSpace E] [BorelSpace E] (f : α → E) (s : Set α) : (MeasureTheory.Measure.hausdorffMeasure 1) (f '' s) ≤ eVariationOn f s

The one-dimensional Hausdorff measure of the image of s under f is at most the total variation of f on s. In particular, the trace of a rectifiable curve has Hausdorff length at most the length of the curve.

theorem eVariationOn.euclideanHausdorffMeasure_image_le {α : Type u_1} {E : Type u_2} [LinearOrder α] [EMetricSpace E] [MeasurableSpace E] [BorelSpace E] (f : α → E) (s : Set α) : (MeasureTheory.Measure.euclideanHausdorffMeasure 1) (f '' s) ≤ eVariationOn f s

The Euclidean one-dimensional Hausdorff measure of the image of s under f is at most the total variation of f on s. In particular, the trace of a rectifiable curve has one-dimensional Euclidean Hausdorff measure at most the length of the curve.

theorem LocallyBoundedVariationOn.addHaar_image_eq_zero {α : Type u_1} {E : Type u_2} [LinearOrder α] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hd : 1 < Module.finrank ℝ E) : μ (f '' s) = 0

The image of a curve of locally bounded variation has zero additive Haar measure in every finite-dimensional real normed space of dimension greater than one.