# Constant speed #

This file defines the notion of constant (and unit) speed for a function f : ℝ → E with pseudo-emetric structure on E with respect to a set s : Set ℝ and "speed" l : ℝ≥0, and shows that if f has locally bounded variation on s, it can be obtained (up to distance zero, on s), as a composite φ ∘ (variationOnFromTo f s a), where φ has unit speed and a ∈ s.

## Main definitions #

• HasConstantSpeedOnWith f s l, stating that the speed of f on s is l.
• HasUnitSpeedOn f s, stating that the speed of f on s is 1.
• naturalParameterization f s a : ℝ → E, the unit speed reparameterization of f on s relative to a.

## Main statements #

• unique_unit_speed_on_Icc_zero proves that if f and f ∘ φ are both naturally parameterized on closed intervals starting at 0, then φ must be the identity on those intervals.
• edist_naturalParameterization_eq_zero proves that if f has locally bounded variation, then precomposing naturalParameterization f s a with variationOnFromTo f s a yields a function at distance zero from f on s.
• has_unit_speed_naturalParameterization proves that if f has locally bounded variation, then naturalParameterization f s a has unit speed on s.

## Tags #

arc-length, parameterization

def HasConstantSpeedOnWith {E : Type u_2} (f : E) (s : ) (l : NNReal) :

f has constant speed l on s if the variation of f on s ∩ Icc x y is equal to l * (y - x) for any x y in s.

Equations
Instances For
theorem HasConstantSpeedOnWith.hasLocallyBoundedVariationOn {E : Type u_2} {f : E} {s : } {l : NNReal} (h : ) :
theorem hasConstantSpeedOnWith_of_subsingleton {E : Type u_2} (f : E) {s : } (hs : s.Subsingleton) (l : NNReal) :
theorem hasConstantSpeedOnWith_iff_ordered {E : Type u_2} {f : E} {s : } {l : NNReal} :
∀ ⦃x : ⦄, x s∀ ⦃y : ⦄, y sx yeVariationOn f (s Set.Icc x y) = ENNReal.ofReal (l * (y - x))
theorem hasConstantSpeedOnWith_iff_variationOnFromTo_eq {E : Type u_2} {f : E} {s : } {l : NNReal} :
∀ ⦃x : ⦄, x s∀ ⦃y : ⦄, y s = l * (y - x)
theorem HasConstantSpeedOnWith.union {E : Type u_2} {f : E} {s : } {l : NNReal} {t : } (hfs : ) (hft : ) {x : } (hs : ) (ht : IsLeast t x) :
theorem HasConstantSpeedOnWith.Icc_Icc {E : Type u_2} {f : E} {l : NNReal} {x : } {y : } {z : } (hfs : HasConstantSpeedOnWith f (Set.Icc x y) l) (hft : HasConstantSpeedOnWith f (Set.Icc y z) l) :
theorem hasConstantSpeedOnWith_zero_iff {E : Type u_2} {f : E} {s : } :
xs, ys, edist (f x) (f y) = 0
theorem HasConstantSpeedOnWith.ratio {E : Type u_2} {f : E} {s : } {l : NNReal} {l' : NNReal} (hl' : l' 0) {φ : } (φm : ) (hfφ : HasConstantSpeedOnWith (f φ) s l) (hf : HasConstantSpeedOnWith f (φ '' s) l') ⦃x : (xs : x s) :
Set.EqOn φ (fun (y : ) => l / l' * (y - x) + φ x) s
def HasUnitSpeedOn {E : Type u_2} (f : E) (s : ) :

f has unit speed on s if it is linearly parameterized by l = 1 on s.

Equations
Instances For
theorem HasUnitSpeedOn.union {E : Type u_2} {f : E} {s : } {t : } {x : } (hfs : ) (hft : ) (hs : ) (ht : IsLeast t x) :
theorem HasUnitSpeedOn.Icc_Icc {E : Type u_2} {f : E} {x : } {y : } {z : } (hfs : HasUnitSpeedOn f (Set.Icc x y)) (hft : HasUnitSpeedOn f (Set.Icc y z)) :
theorem unique_unit_speed {E : Type u_2} {f : E} {s : } {φ : } (φm : ) (hfφ : HasUnitSpeedOn (f φ) s) (hf : HasUnitSpeedOn f (φ '' s)) ⦃x : (xs : x s) :
Set.EqOn φ (fun (y : ) => y - x + φ x) s

If both f and f ∘ φ have unit speed (on t and s respectively) and φ monotonically maps s onto t, then φ is just a translation (on s).

theorem unique_unit_speed_on_Icc_zero {E : Type u_2} {f : E} {s : } {t : } (hs : 0 s) (ht : 0 t) {φ : } (φm : MonotoneOn φ (Set.Icc 0 s)) (φst : φ '' Set.Icc 0 s = Set.Icc 0 t) (hfφ : HasUnitSpeedOn (f φ) (Set.Icc 0 s)) (hf : HasUnitSpeedOn f (Set.Icc 0 t)) :
Set.EqOn φ id (Set.Icc 0 s)

If both f and f ∘ φ have unit speed (on Icc 0 t and Icc 0 s respectively) and φ monotonically maps Icc 0 s onto Icc 0 t, then φ is the identity on Icc 0 s

noncomputable def naturalParameterization {α : Type u_1} [] {E : Type u_2} (f : αE) (s : Set α) (a : α) :
E

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).
Equations
Instances For
theorem edist_naturalParameterization_eq_zero {α : Type u_1} [] {E : Type u_2} {f : αE} {s : Set α} (hf : ) {a : α} (as : a s) {b : α} (bs : b s) :
edist (naturalParameterization f s a ()) (f b) = 0
theorem has_unit_speed_naturalParameterization {α : Type u_1} [] {E : Type u_2} (f : αE) {s : Set α} (hf : ) {a : α} (as : a s) :