mathlib3 documentation

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 #

Main statements #

Tags #

arc-length, parameterization

def has_constant_speed_on_with {E : Type u_2} [pseudo_emetric_space 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
theorem has_constant_speed_on_with_iff_ordered {E : Type u_2} [pseudo_emetric_space E] {f : E} {s : set } {l : nnreal} :
has_constant_speed_on_with f s l ⦃x : ⦄, x s ⦃y : ⦄, y s x y evariation_on f (s set.Icc x y) = ennreal.of_real (l * (y - x))
theorem has_constant_speed_on_with.union {E : Type u_2} [pseudo_emetric_space E] {f : E} {s : set } {l : nnreal} {t : set } (hfs : has_constant_speed_on_with f s l) (hft : has_constant_speed_on_with f t l) {x : } (hs : is_greatest s x) (ht : is_least t x) :
theorem has_constant_speed_on_with_zero_iff {E : Type u_2} [pseudo_emetric_space E] {f : E} {s : set } :
has_constant_speed_on_with f s 0 (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} [pseudo_emetric_space E] {f : E} {s : set } {l l' : nnreal} (hl' : l' 0) {φ : } (φm : monotone_on φ s) (hfφ : has_constant_speed_on_with (f φ) s l) (hf : has_constant_speed_on_with f '' s) l') ⦃x : (xs : x s) :
set.eq_on φ (λ (y : ), l / l' * (y - x) + φ x) s
def has_unit_speed_on {E : Type u_2} [pseudo_emetric_space E] (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} [pseudo_emetric_space E] {f : E} {s t : set } {x : } (hfs : has_unit_speed_on f s) (hft : has_unit_speed_on f t) (hs : is_greatest s x) (ht : is_least t x) :
theorem has_unit_speed_on.Icc_Icc {E : Type u_2} [pseudo_emetric_space E] {f : E} {x y z : } (hfs : has_unit_speed_on f (set.Icc x y)) (hft : has_unit_speed_on f (set.Icc y z)) :
theorem unique_unit_speed {E : Type u_2} [pseudo_emetric_space E] {f : E} {s : set } {φ : } (φm : monotone_on φ s) (hfφ : has_unit_speed_on (f φ) s) (hf : has_unit_speed_on f '' s)) ⦃x : (xs : x s) :
set.eq_on φ (λ (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} [pseudo_emetric_space E] {f : E} {s t : } (hs : 0 s) (ht : 0 t) {φ : } (φm : monotone_on φ (set.Icc 0 s)) (φst : φ '' set.Icc 0 s = set.Icc 0 t) (hfφ : has_unit_speed_on (f φ) (set.Icc 0 s)) (hf : has_unit_speed_on f (set.Icc 0 t)) :

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} [pseudo_emetric_space E] (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} [pseudo_emetric_space E] {f : α E} {s : set α} (hf : has_locally_bounded_variation_on f s) {a : α} (as : a s) {b : α} (bs : b s) :