Hausdorff measure and the length of curves

A continuous curve on a compact real interval [a, b] that is injective on the open interval (a, b) has variation equal to the one-dimensional Hausdorff measure of its trace. This covers injective arcs and simple closed curves, where γ a = γ b; the endpoints may also coincide with other points of the trace. In particular, finite trace measure is equivalent to bounded variation, without any Lipschitz or bounded-variation hypothesis on the parametrization. The results include empty and singleton parameter intervals.

Both raw Hausdorff measure μH[1] and Euclidean-normalized measure μHE[1] are supported. These results let one compute the length of such a curve from its trace using either convention.

For an arbitrary continuous curve, the variation is the Hausdorff integral of the extended cardinality of the fibers: the Banach indicatrix formula, which counts repeated traversals. A partition argument bounds the variation by the integral. Conversely, along uniform partitions the number of subarcs through a point eventually reaches the number of parameters over it, and each such count has integral at most the variation, so Fatou's lemma gives the reverse bound. For a curve injective on (a, b), almost every fiber over the trace is a single point, which gives the bound by the trace measure.

References

• H. Federer, Geometric Measure Theory, Theorem 2.10.13 (the Banach indicatrix formula for continuous curves).

theorem ContinuousOn.eVariationOn_le_lintegral_encard {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) : eVariationOn γ (Set.Icc a b) ≤ ∫⁻ (y : X), ↑(Set.Icc a b ∩ γ ⁻¹' {y}).encard ∂MeasureTheory.Measure.hausdorffMeasure 1

Banach indicatrix inequality. The variation of a continuous curve on [a, b] is at most the raw one-dimensional Hausdorff integral of the extended cardinality of its fibers. No injectivity or rectifiability hypothesis is needed; repeated traversals are counted by the fiber cardinality.

theorem ContinuousOn.eVariationOn_eq_lintegral_encard {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) : eVariationOn γ (Set.Icc a b) = ∫⁻ (y : X), ↑(Set.Icc a b ∩ γ ⁻¹' {y}).encard ∂MeasureTheory.Measure.hausdorffMeasure 1

Banach indicatrix formula. The variation of a continuous curve on [a, b] is the raw one-dimensional Hausdorff integral of the extended cardinality of its fibers. No Lipschitz or bounded-variation hypothesis is needed: both sides are infinite together. Pauses and repeated traversals are allowed, and infinite fibers have infinite multiplicity.

theorem ContinuousOn.eVariationOn_le_hausdorffMeasure_image {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Ioo a b)) : eVariationOn γ (Set.Icc a b) ≤ (MeasureTheory.Measure.hausdorffMeasure 1) (γ '' Set.Icc a b)

The variation of a continuous curve on [a, b] that is injective on (a, b), such as an injective arc or a simple closed curve, is at most the raw one-dimensional Hausdorff measure of its trace. No rectifiability hypothesis on the parametrization is needed.

theorem ContinuousOn.eVariationOn_le_euclideanHausdorffMeasure_image {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Ioo a b)) : eVariationOn γ (Set.Icc a b) ≤ (MeasureTheory.Measure.euclideanHausdorffMeasure 1) (γ '' Set.Icc a b)

The variation of a continuous curve on [a, b] that is injective on (a, b), such as an injective arc or a simple closed curve, is at most the Euclidean-normalized one-dimensional Hausdorff measure of its trace. This also covers empty and singleton intervals.

theorem ContinuousOn.eVariationOn_eq_hausdorffMeasure_image {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Ioo a b)) : eVariationOn γ (Set.Icc a b) = (MeasureTheory.Measure.hausdorffMeasure 1) (γ '' Set.Icc a b)

A continuous curve on [a, b] that is injective on (a, b), such as an injective arc or a simple closed curve, has variation equal to the raw one-dimensional Hausdorff measure of its trace. The equality also holds for infinite length and for empty or singleton intervals.

theorem ContinuousOn.eVariationOn_eq_euclideanHausdorffMeasure_image {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Ioo a b)) : eVariationOn γ (Set.Icc a b) = (MeasureTheory.Measure.euclideanHausdorffMeasure 1) (γ '' Set.Icc a b)

A continuous curve on [a, b] that is injective on (a, b), such as an injective arc or a simple closed curve, has variation equal to the Euclidean-normalized one-dimensional Hausdorff measure of its trace, including when the length is infinite.

theorem ContinuousOn.boundedVariationOn_iff_hausdorffMeasure_image_lt_top {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Ioo a b)) : BoundedVariationOn γ (Set.Icc a b) ↔ (MeasureTheory.Measure.hausdorffMeasure 1) (γ '' Set.Icc a b) < ⊤

Finite raw Hausdorff length of the trace is equivalent to bounded variation for a continuous curve injective on the open interval. No Lipschitz hypothesis on its parametrization is needed.

theorem ContinuousOn.boundedVariationOn_iff_euclideanHausdorffMeasure_image_lt_top {X : Type u_1} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {γ : ℝ → X} {a b : ℝ} (hγ : ContinuousOn γ (Set.Icc a b)) (hinj : Set.InjOn γ (Set.Ioo a b)) : BoundedVariationOn γ (Set.Icc a b) ↔ (MeasureTheory.Measure.euclideanHausdorffMeasure 1) (γ '' Set.Icc a b) < ⊤

Finite Euclidean Hausdorff length of the trace is equivalent to bounded variation for a continuous curve injective on the open interval, including injective arcs and simple closed curves.