# mathlib3documentation

analysis.constant_speed

# Constant speed #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 φ ∘ (variation_on_from_to f s a), where φ has unit speed and a ∈ s.

## Main definitions #

• has_constant_speed_on_with f s l, stating that the speed of f on s is l.
• has_unit_speed_on f s, stating that the speed of f on s is 1.
• natural_parameterization 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_natural_parameterization_eq_zero proves that if f has locally bounded variation, then precomposing natural_parameterization f s a with variation_on_from_to f s a yields a function at distance zero from f on s.
• has_unit_speed_natural_parameterization proves that if f has locally bounded variation, then natural_parameterization f s a has unit speed on s.

## Tags #

arc-length, parameterization

def has_constant_speed_on_with {E : Type u_2} (f : E) (s : set ) (l : nnreal) :
Prop

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
theorem has_constant_speed_on_with.has_locally_bounded_variation_on {E : Type u_2} {f : E} {s : set } {l : nnreal} (h : l) :
theorem has_constant_speed_on_with_of_subsingleton {E : Type u_2} (f : E) {s : set } (hs : s.subsingleton) (l : nnreal) :
theorem has_constant_speed_on_with_iff_ordered {E : Type u_2} {f : E} {s : set } {l : nnreal} :
⦃x : ⦄, x s ⦃y : ⦄, y s x y (s y) = ennreal.of_real (l * (y - x))
theorem has_constant_speed_on_with_iff_variation_on_from_to_eq {E : Type u_2} {f : E} {s : set } {l : nnreal} :
⦃x : ⦄, x s ⦃y : ⦄, y s x y = l * (y - x)
theorem has_constant_speed_on_with.union {E : Type u_2} {f : E} {s : set } {l : nnreal} {t : set } (hfs : l) (hft : l) {x : } (hs : x) (ht : x) :
(s t) l
theorem has_constant_speed_on_with.Icc_Icc {E : Type u_2} {f : E} {l : nnreal} {x y z : } (hfs : l) (hft : l) :
l
theorem has_constant_speed_on_with_zero_iff {E : Type u_2} {f : E} {s : set } :
(x : ), x s (y : ), y s has_edist.edist (f x) (f y) = 0
theorem has_constant_speed_on_with.ratio {E : Type u_2} {f : E} {s : set } {l l' : nnreal} (hl' : l' 0) {φ : } (φm : s) (hfφ : s l) (hf : '' s) l') ⦃x : (xs : x s) :
(λ (y : ), l / l' * (y - x) + φ x) s
def has_unit_speed_on {E : Type u_2} (f : E) (s : set ) :
Prop

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

Equations
theorem has_unit_speed_on.union {E : Type u_2} {f : E} {s t : set } {x : } (hfs : s) (hft : t) (hs : x) (ht : x) :
(s t)
theorem has_unit_speed_on.Icc_Icc {E : Type u_2} {f : E} {x y z : } (hfs : (set.Icc x y)) (hft : (set.Icc y z)) :
(set.Icc x z)
theorem unique_unit_speed {E : Type u_2} {f : E} {s : set } {φ : } (φm : s) (hfφ : has_unit_speed_on (f φ) s) (hf : '' s)) ⦃x : (xs : x s) :
(λ (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 : (set.Icc 0 s)) (φst : φ '' s = t) (hfφ : has_unit_speed_on (f φ) (set.Icc 0 s)) (hf : (set.Icc 0 t)) :
(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 natural_parameterization {α : Type u_1} [linear_order α] {E : Type u_2} (f : α E) (s : set α) (a : α) :

The natural parameterization of f on s, which, if f has locally bounded variation on s,

• has unit speed on s (by natural_parameterization_has_unit_speed).
• composed with variation_on_from_to f s a, is at distance zero from f (by natural_parameterization_edist_zero).
Equations
theorem edist_natural_parameterization_eq_zero {α : Type u_1} [linear_order α] {E : Type u_2} {f : α E} {s : set α} (hf : s) {a : α} (as : a s) {b : α} (bs : b s) :
has_edist.edist a a b)) (f b) = 0
theorem has_unit_speed_natural_parameterization {α : Type u_1} [linear_order α] {E : Type u_2} (f : α E) {s : set α} (hf : s) {a : α} (as : a s) :
a '' s)