Distance controlled by cumulative variation

Cumulative signed variation controls distances between values of a metric-valued function. In particular, the function is constant on each fibre of cumulative variation, allowing an arclength factorization even when the original curve has pauses. For locally bounded-variation functions, continuity of cumulative variation is equivalent to continuity of the function.

The file also records that cumulative variation only depends on the function on s (variationOnFromTo.eq_of_eqOn), and the antitone counterpart variationOnFromTo.comp_eq_of_antitoneOn of Mathlib's variationOnFromTo.comp_eq_of_monotoneOn.

theorem variationOnFromTo.eq_of_eqOn {α : Type u_1} {E : Type u_3} [LinearOrder α] [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f f' : α → E} {s : Set α} (h : Set.EqOn f f' s) : variationOnFromTo f s = variationOnFromTo f' s

Cumulative signed variation only depends on the function on s.

theorem variationOnFromTo.comp_eq_of_antitoneOn {α : Type u_1} {β : Type u_2} {E : Type u_3} [LinearOrder α] [LinearOrder β] [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {t : Set β} (φ : β → α) (hφ : AntitoneOn φ t) {x y : β} (hx : x ∈ t) (hy : y ∈ t) : variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ y) (φ x)

Composing with an antitone map reverses the endpoints of cumulative signed variation.

theorem LocallyBoundedVariationOn.edist_le_ofReal_variationOnFromTo_sub {α : Type u_1} {X : Type u_2} [LinearOrder α] [TopologicalSpace X] [WeakPseudoEMetricSpace X] {f : α → X} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a x y : α} (ha : a ∈ s) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≤ y) : edist (f x) (f y) ≤ ENNReal.ofReal (variationOnFromTo f s a y - variationOnFromTo f s a x)

The extended distance between two values at ordered points of s is at most the increase of the cumulative signed variation between them.

theorem LocallyBoundedVariationOn.dist_le_abs_sub_variationOnFromTo {α : Type u_1} {X : Type u_2} [LinearOrder α] [PseudoMetricSpace X] {f : α → X} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a x y : α} (ha : a ∈ s) (hx : x ∈ s) (hy : y ∈ s) : dist (f x) (f y) ≤ |variationOnFromTo f s a x - variationOnFromTo f s a y|

Distances between values are bounded by the difference of cumulative signed variations.

theorem LocallyBoundedVariationOn.continuousWithinAt_variationOnFromTo_iff {α : Type u_1} {X : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [PseudoEMetricSpace X] {f : α → X} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a x : α} (ha : a ∈ s) (hx : x ∈ s) : ContinuousWithinAt (variationOnFromTo f s a) s x ↔ ContinuousWithinAt f s x

Cumulative variation of a locally bounded-variation function is continuous at exactly the points where the original function is continuous, relative to the same set.

theorem LocallyBoundedVariationOn.exists_lipschitzOnWith_comp_variationOnFromTo_eqOn {α : Type u_1} {X : Type u_2} [LinearOrder α] [MetricSpace X] {f : α → X} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (ha : a ∈ s) : ∃ (g : ℝ → X), LipschitzOnWith 1 g (variationOnFromTo f s a '' s) ∧ Set.EqOn (g ∘ variationOnFromTo f s a) f s

A metric-valued function with locally bounded variation factors through its cumulative signed variation by a 1-Lipschitz map on the image of that variation.

theorem LocallyBoundedVariationOn.strictMonoOn_variationOnFromTo {α : Type u_1} {X : Type u_2} [LinearOrder α] [MetricSpace X] {f : α → X} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (ha : a ∈ s) (hinj : Set.InjOn f s) : StrictMonoOn (variationOnFromTo f s a) s

Cumulative signed variation is strictly increasing on a set where the original function is injective.

theorem LocallyBoundedVariationOn.strictMonoOn_variationOnFromTo_of_injOn_Ioo {α : Type u_1} {X : Type u_2} [LinearOrder α] [DenselyOrdered α] [MetricSpace X] {f : α → X} {a b c : α} (hf : LocallyBoundedVariationOn f (Set.Icc a b)) (hc : c ∈ Set.Icc a b) (hinj : Set.InjOn f (Set.Ioo a b)) : StrictMonoOn (variationOnFromTo f (Set.Icc a b) c) (Set.Icc a b)

Injectivity on the interior of an interval makes cumulative variation strictly increasing on the closed interval. Thus equal endpoint values do not obstruct the arclength coordinate.