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} [PseudoEMetricSpace E] (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

• HasConstantSpeedOnWith f s l = ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → eVariationOn f (s ∩ Set.Icc x y) = ENNReal.ofReal (↑l * (y - x))

theorem HasConstantSpeedOnWith.hasLocallyBoundedVariationOn {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} (h : HasConstantSpeedOnWith f s l) : LocallyBoundedVariationOn f s

theorem hasConstantSpeedOnWith_of_subsingleton {E : Type u_2} [PseudoEMetricSpace E] (f : ℝ → E) {s : Set ℝ} (hs : s.Subsingleton) (l : NNReal) : HasConstantSpeedOnWith f s l

theorem hasConstantSpeedOnWith_iff_ordered {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} : HasConstantSpeedOnWith f s l ↔ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Set.Icc x y) = ENNReal.ofReal (↑l * (y - x))

theorem hasConstantSpeedOnWith_iff_variationOnFromTo_eq {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} : HasConstantSpeedOnWith f s l ↔ LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)

theorem HasConstantSpeedOnWith.union {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} {t : Set ℝ} (hfs : HasConstantSpeedOnWith f s l) (hft : HasConstantSpeedOnWith f t l) {x : ℝ} (hs : IsGreatest s x) (ht : IsLeast t x) : HasConstantSpeedOnWith f (s ∪ t) l

theorem HasConstantSpeedOnWith.Icc_Icc {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {l : NNReal} {x y z : ℝ} (hfs : HasConstantSpeedOnWith f (Set.Icc x y) l) (hft : HasConstantSpeedOnWith f (Set.Icc y z) l) : HasConstantSpeedOnWith f (Set.Icc x z) l

theorem hasConstantSpeedOnWith_zero_iff {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} : HasConstantSpeedOnWith f s 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0

theorem HasConstantSpeedOnWith.ratio {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l l' : NNReal} (hl' : l' ≠ 0) {φ : ℝ → ℝ} (φm : MonotoneOn φ s) (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} [PseudoEMetricSpace E] (f : ℝ → E) (s : Set ℝ) : Prop

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

Equations

• HasUnitSpeedOn f s = HasConstantSpeedOnWith f s 1

theorem HasUnitSpeedOn.union {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {s t : Set ℝ} {x : ℝ} (hfs : HasUnitSpeedOn f s) (hft : HasUnitSpeedOn f t) (hs : IsGreatest s x) (ht : IsLeast t x) : HasUnitSpeedOn f (s ∪ t)

theorem HasUnitSpeedOn.Icc_Icc {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {x y z : ℝ} (hfs : HasUnitSpeedOn f (Set.Icc x y)) (hft : HasUnitSpeedOn f (Set.Icc y z)) : HasUnitSpeedOn f (Set.Icc x z)

theorem unique_unit_speed {E : Type u_2} [PseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {φ : ℝ → ℝ} (φm : MonotoneOn φ s) (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} [PseudoEMetricSpace E] {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} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (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

• naturalParameterization f s a = f ∘ Function.invFunOn (variationOnFromTo f s a) s

theorem edist_naturalParameterization_eq_zero {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) {b : α} (bs : b ∈ s) : edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0

theorem has_unit_speed_naturalParameterization {α : Type u_1} [LinearOrder α] {E : Type u_2} [PseudoEMetricSpace E] (f : α → E) {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) : HasUnitSpeedOn (naturalParameterization f s a) (variationOnFromTo f s a '' s)