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 #

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} [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

has_constant_speed_on_with f s l = ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → evariation_on f (s ∩ set.Icc x y) = ennreal.of_real (↑l * (y - x))

theorem has_constant_speed_on_with.has_locally_bounded_variation_on {E : Type u_2} [pseudo_emetric_space E] {f : ℝ → E} {s : set ℝ} {l : nnreal} (h : has_constant_speed_on_with f s l) :

has_locally_bounded_variation_on f s

theorem has_constant_speed_on_with_of_subsingleton {E : Type u_2} [pseudo_emetric_space E] (f : ℝ → E) {s : set ℝ} (hs : s.subsingleton) (l : nnreal) :

has_constant_speed_on_with f s l

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_iff_variation_on_from_to_eq {E : Type u_2} [pseudo_emetric_space E] {f : ℝ → E} {s : set ℝ} {l : nnreal} :

has_constant_speed_on_with f s l ↔ has_locally_bounded_variation_on f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variation_on_from_to f s x y = ↑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) :

has_constant_speed_on_with f (s ∪ t) l

theorem has_constant_speed_on_with.Icc_Icc {E : Type u_2} [pseudo_emetric_space E] {f : ℝ → E} {l : nnreal} {x y z : ℝ} (hfs : has_constant_speed_on_with f (set.Icc x y) l) (hft : has_constant_speed_on_with f (set.Icc y z) l) :

has_constant_speed_on_with f (set.Icc x z) l

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

has_unit_speed_on f s = has_constant_speed_on_with f s 1

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) :

has_unit_speed_on f (s ∪ t)

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)) :

has_unit_speed_on f (set.Icc x 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)) :

set.eq_on φ 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 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

natural_parameterization f s a = f ∘ function.inv_fun_on (variation_on_from_to f s a) s

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) :

has_edist.edist (natural_parameterization f s a (variation_on_from_to f s a b)) (f b) = 0

theorem has_unit_speed_natural_parameterization {α : 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) :

has_unit_speed_on (natural_parameterization f s a) (variation_on_from_to f s a '' s)