Documentation

Mathlib.Analysis.ConstantSpeed

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 #

Main statements #

Tags #

arc-length, parameterization

def HasConstantSpeedOnWith {E : Type u_2} [PseudoEMetricSpace E] (f : E) (s : Set ) (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_iff_ordered {E : Type u_2} [PseudoEMetricSpace E] {f : E} {s : Set } {l : NNReal} :
    HasConstantSpeedOnWith f s l ∀ ⦃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} [PseudoEMetricSpace E] {f : E} {s : Set } {l : NNReal} :
    HasConstantSpeedOnWith f s l LocallyBoundedVariationOn f s ∀ ⦃x : ⦄, x s∀ ⦃y : ⦄, y svariationOnFromTo 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) :
    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) :
    theorem hasConstantSpeedOnWith_zero_iff {E : Type u_2} [PseudoEMetricSpace E] {f : E} {s : Set } :
    HasConstantSpeedOnWith f s 0 xs, ys, edist (f x) (f y) = 0
    theorem HasConstantSpeedOnWith.ratio {E : Type u_2} [PseudoEMetricSpace E] {f : E} {s : Set } {l : NNReal} {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 ) :

    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} [PseudoEMetricSpace E] {f : E} {s : Set } {t : Set } {x : } (hfs : HasUnitSpeedOn f s) (hft : HasUnitSpeedOn f t) (hs : IsGreatest s x) (ht : IsLeast t x) :
      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)) :
      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,

      Equations
      Instances For
        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) :
        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) :