Parametrized piecewise-linear paths and reparametrization

TauCeti.PLPath 𝕜 V models piecewise-linear paths up to reparametrization by reduced segment lists. This file compares that model with parametrized paths, that is with functions 𝕜 → V.

A timed presentation is a list of pairs (d, v) of a positive duration d and a segment v. Its parametrized path TauCeti.PLPath.evalTimed p starts at 0 at time 0 and runs along the segments in order, along v at constant velocity d⁻¹ • v during a time interval of length d; it is constant before time 0 and after the total duration TauCeti.PLPath.duration p. A timed presentation φ in 𝕜 with nonnegative segments presents a nondecreasing piecewise-linear map from [0, duration φ] onto [0, s], where s is the sum of its segments. So p is a reparametrization of q (TauCeti.PLPath.IsReparam p q) when evalTimed p = evalTimed q ∘ evalTimed φ for such a φ running from [0, duration p] onto [0, duration q]; for presentations of duration 1 these are Littelmann's nondecreasing surjective piecewise-linear reparametrizations of [0, 1].

The main result is that the segment-list model is faithful: two timed presentations of positive duration present the same TauCeti.PLPath exactly when they are reparametrizations of a common timed presentation, which may be chosen of any prescribed positive duration. All constructions use only the field operations of 𝕜, so over ℚ every subdivision time and every reparametrization stays rational.

Main definitions

• TauCeti.PLPath.duration, TauCeti.PLPath.IsTimed: the total duration of a list of (duration, segment) pairs, and the condition that every duration is positive.
• TauCeti.PLPath.evalTimed: the parametrized path of a timed presentation.
• TauCeti.PLPath.timedComp: a timed presentation of the composite of two parametrized paths.
• TauCeti.PLPath.IsReparam: one timed presentation is a reparametrization of another.
• TauCeti.PLPath.reverseTimed: the reversal of a timed presentation, presenting the reversed path.

Main results

• TauCeti.PLPath.evalTimed_duration: the parametrized path ends at the endpoint of the path it presents.
• TauCeti.PLPath.evalTimed_append: the parametrized path of a concatenation runs through the first presentation and then, shifted by its duration, through the second.
• TauCeti.PLPath.monotone_evalTimed, TauCeti.PLPath.exists_evalTimed_eq: a timed presentation in 𝕜 with nonnegative segments is nondecreasing, and maps [0, duration φ] onto [0, s], where s is the sum of its segments.
• TauCeti.PLPath.evalTimed_timedComp: timedComp presents the composite.
• TauCeti.PLPath.ofSegments_map_snd_eq_of_evalTimed_eq: two timed presentations with the same parametrized path present the same TauCeti.PLPath.
• TauCeti.PLPath.IsReparam.trans, TauCeti.PLPath.IsReparam.ofSegments_map_snd_eq: reparametrization is transitive and does not change the presented TauCeti.PLPath.
• TauCeti.PLPath.IsReparam.append: reparametrization is compatible with concatenation.
• TauCeti.PLPath.ofSegments_map_snd_eq_iff_exists_isReparam: two timed presentations of positive duration present the same TauCeti.PLPath exactly when they are reparametrizations of a common timed presentation.

References

• P. Littelmann, A Littlewood-Richardson rule for symmetrizable Kac-Moody algebras, Invent. Math. 116 (1994), §1.
• P. Littelmann, Paths and root operators in representation theory, Ann. of Math. 142 (1995), §1.

Timed presentations and their parametrized paths

def TauCeti.PLPath.duration {𝕜 : Type u} {V : Type v} [AddMonoid 𝕜] (p : List (𝕜 × V)) : 𝕜

The total duration of a list of (duration, segment) pairs.

theorem TauCeti.PLPath.duration_def {𝕜 : Type u} {V : Type v} [AddMonoid 𝕜] (p : List (𝕜 × V)) : duration p = (List.map Prod.fst p).sum

@[simp]

theorem TauCeti.PLPath.duration_nil {𝕜 : Type u} {V : Type v} [AddMonoid 𝕜] : duration [] = 0

@[simp]

theorem TauCeti.PLPath.duration_cons {𝕜 : Type u} {V : Type v} [AddMonoid 𝕜] (x : 𝕜 × V) (p : List (𝕜 × V)) : duration (x :: p) = x.1 + duration p

@[simp]

theorem TauCeti.PLPath.duration_append {𝕜 : Type u} {V : Type v} [AddMonoid 𝕜] (p q : List (𝕜 × V)) : duration (p ++ q) = duration p + duration q

theorem TauCeti.PLPath.duration_eq_fst_sum {𝕜 : Type u} {V : Type v} [AddMonoid 𝕜] [AddMonoid V] (p : List (𝕜 × V)) : duration p = p.sum.1

The total duration is the time coordinate of the sum of the (duration, segment) pairs.

def TauCeti.PLPath.IsTimed {𝕜 : Type u} {V : Type v} [Zero 𝕜] [LT 𝕜] (p : List (𝕜 × V)) : Prop

A list of (duration, segment) pairs is a timed presentation when every duration is positive.

theorem TauCeti.PLPath.isTimed_iff {𝕜 : Type u} {V : Type v} [Zero 𝕜] [LT 𝕜] {p : List (𝕜 × V)} : IsTimed p ↔ ∀ x ∈ p, 0 < x.1

The characterization of timed presentations, for use outside this file.

@[simp]

theorem TauCeti.PLPath.isTimed_nil {𝕜 : Type u} {V : Type v} [Zero 𝕜] [LT 𝕜] : IsTimed []

@[simp]

theorem TauCeti.PLPath.isTimed_cons {𝕜 : Type u} {V : Type v} [Zero 𝕜] [LT 𝕜] {p : List (𝕜 × V)} {x : 𝕜 × V} : IsTimed (x :: p) ↔ 0 < x.1 ∧ IsTimed p

theorem TauCeti.PLPath.IsTimed.nonneg {𝕜 : Type u} {V : Type v} [Zero 𝕜] [Preorder 𝕜] {p : List (𝕜 × V)} (hp : IsTimed p) (x : 𝕜 × V) : x ∈ p → 0 ≤ x.1

theorem TauCeti.PLPath.IsTimed.and_nonneg {𝕜 : Type u} {W : Type u_1} [Zero 𝕜] [Preorder 𝕜] [Zero W] [LE W] {p : List (𝕜 × W)} (hp : IsTimed p) (hp' : ∀ x ∈ p, 0 ≤ x.2) (x : 𝕜 × W) : x ∈ p → 0 ≤ x.1 ∧ 0 ≤ x.2

A timed presentation with nonnegative segments has nonnegative durations and segments.

def TauCeti.PLPath.reverseTimed {𝕜 : Type u} {V : Type v} [Neg V] (p : List (𝕜 × V)) : List (𝕜 × V)

The reversal of a list of (duration, segment) pairs: the segments are negated and traversed in the opposite order, each in its own time. It presents the reversed path (TauCeti.PLPath.ofSegments_map_snd_reverseTimed).

theorem TauCeti.PLPath.reverseTimed_def {𝕜 : Type u} {V : Type v} [Neg V] (p : List (𝕜 × V)) : reverseTimed p = (List.map (fun (z : 𝕜 × V) => (z.1, -z.2)) p).reverse

@[simp]

theorem TauCeti.PLPath.mem_reverseTimed {𝕜 : Type u} {V : Type v} [InvolutiveNeg V] {p : List (𝕜 × V)} {z : 𝕜 × V} : z ∈ reverseTimed p ↔ (z.1, -z.2) ∈ p

@[simp]

theorem TauCeti.PLPath.reverseTimed_reverseTimed {𝕜 : Type u} {V : Type v} [InvolutiveNeg V] (p : List (𝕜 × V)) : reverseTimed (reverseTimed p) = p

@[simp]

theorem TauCeti.PLPath.isTimed_reverseTimed {𝕜 : Type u} {V : Type v} [Zero 𝕜] [LT 𝕜] [Neg V] {p : List (𝕜 × V)} : IsTimed (reverseTimed p) ↔ IsTimed p

@[simp]

theorem TauCeti.PLPath.duration_reverseTimed {𝕜 : Type u} {V : Type v} [AddCommMonoid 𝕜] [Neg V] (p : List (𝕜 × V)) : duration (reverseTimed p) = duration p

@[simp]

theorem TauCeti.PLPath.ofSegments_map_snd_reverseTimed {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] (p : List (𝕜 × V)) : ofSegments 𝕜 (List.map Prod.snd (reverseTimed p)) = (ofSegments 𝕜 (List.map Prod.snd p)).reverse

def TauCeti.PLPath.evalTimed {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] : List (𝕜 × V) → 𝕜 → V

The parametrized path of a list of (duration, segment) pairs. At time t the first pair (d, v) contributes (max 0 (min t d) / d) • v, and the remaining pairs are run from time d on. For a timed presentation (TauCeti.PLPath.IsTimed p, every duration positive) this starts at 0 at time 0 and runs along each segment v in turn at constant velocity, during a time interval of length the duration d of v.

@[simp]

theorem TauCeti.PLPath.evalTimed_nil {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] (t : 𝕜) : evalTimed [] t = 0

@[simp]

theorem TauCeti.PLPath.evalTimed_cons {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] (d : 𝕜) (v : V) (p : List (𝕜 × V)) (t : 𝕜) : evalTimed ((d, v) :: p) t = (max 0 (min t d) / d) • v + evalTimed p (t - d)

theorem TauCeti.PLPath.evalTimed_append {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] (p q : List (𝕜 × V)) (t : 𝕜) : evalTimed (p ++ q) t = evalTimed p t + evalTimed q (t - duration p)

The parametrized path of a concatenation runs through the first presentation and then, from its total duration on, through the second.

theorem TauCeti.PLPath.evalTimed_eq_zero_of_forall {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] {p : List (𝕜 × V)} (h : ∀ x ∈ p, x.2 = 0) (t : 𝕜) : evalTimed p t = 0

Stationary segments do not move the parametrized path.

theorem TauCeti.PLPath.duration_nonneg {𝕜 : Type u} {V : Type v} [AddCommMonoid 𝕜] [PartialOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : List (𝕜 × V)} (hp : ∀ x ∈ p, 0 ≤ x.1) : 0 ≤ duration p

theorem TauCeti.PLPath.IsTimed.duration_pos {𝕜 : Type u} {V : Type v} [AddCommMonoid 𝕜] [PartialOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : List (𝕜 × V)} (hp : IsTimed p) (hne : p ≠ []) : 0 < duration p

theorem TauCeti.PLPath.IsTimed.eq_nil_of_duration_nonpos {𝕜 : Type u} {V : Type v} [AddCommMonoid 𝕜] [PartialOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : List (𝕜 × V)} (hp : IsTimed p) (h : duration p ≤ 0) : p = []

A timed presentation of nonpositive duration is empty.

theorem TauCeti.PLPath.evalTimed_cons_of_nonpos {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] {p : List (𝕜 × V)} {d t : 𝕜} [AddCommGroup V] [Module 𝕜 V] {v : V} (ht : t ≤ 0) : evalTimed ((d, v) :: p) t = evalTimed p (t - d)

Up to time 0, the first segment has not been started.

theorem TauCeti.PLPath.evalTimed_cons_of_le {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] {p : List (𝕜 × V)} {d t : 𝕜} [AddCommGroup V] [Module 𝕜 V] {v : V} (hd : 0 < d) (ht : d ≤ t) : evalTimed ((d, v) :: p) t = v + evalTimed p (t - d)

From time d on, the first segment, of duration d, has been run entirely.

theorem TauCeti.PLPath.evalTimed_of_nonpos {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p : List (𝕜 × V)} {t : 𝕜} [AddCommGroup V] [Module 𝕜 V] (hp : ∀ x ∈ p, 0 ≤ x.1) (ht : t ≤ 0) : evalTimed p t = 0

The parametrized path is 0 up to time 0.

@[simp]

theorem TauCeti.PLPath.evalTimed_zero {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] (hp : ∀ x ∈ p, 0 ≤ x.1) : evalTimed p 0 = 0

theorem TauCeti.PLPath.evalTimed_of_duration_le {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p : List (𝕜 × V)} {t : 𝕜} [AddCommGroup V] [Module 𝕜 V] (hp : IsTimed p) (ht : duration p ≤ t) : evalTimed p t = (List.map Prod.snd p).sum

The parametrized path is constant at the sum of the segments after the total duration.

theorem TauCeti.PLPath.evalTimed_duration {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] (hp : IsTimed p) : evalTimed p (duration p) = (ofSegments 𝕜 (List.map Prod.snd p)).endpoint

The parametrized path of a timed presentation ends, at its total duration, at the endpoint of the path it presents.

theorem TauCeti.PLPath.evalTimed_eq_evalTimed_cons_add_sub {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p : List (𝕜 × V)} {d : 𝕜} [AddCommGroup V] [Module 𝕜 V] {v : V} (hd : 0 < d) {s : 𝕜} (hs : 0 ≤ s) : evalTimed p s = evalTimed ((d, v) :: p) (s + d) - v

After the first segment, the parametrized path of the remaining segments is that of the whole presentation, shifted back by the first duration and translated back by the first segment.

Subdividing a segment

theorem TauCeti.PLPath.evalTimed_cons_eq_evalTimed_cons_cons {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {v : V} {d₁ d₂ D : 𝕜} {v₁ v₂ : V} (h₁ : 0 ≤ d₁) (h₂ : 0 ≤ d₂) (hD : d₁ + d₂ = D) (hv₁ : v₁ = (d₁ / D) • v) (hv₂ : v₂ = (d₂ / D) • v) (p : List (𝕜 × V)) (t : 𝕜) : evalTimed ((D, v) :: p) t = evalTimed ((d₁, v₁) :: (d₂, v₂) :: p) t

Subdividing a segment of duration D = d₁ + d₂ into its pieces of durations d₁ and d₂ does not change the parametrized path. The durations d₁ and d₂ may vanish.

theorem TauCeti.PLPath.evalTimed_cons_eq_evalTimed_cons_cons_sub {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {d e : 𝕜} [AddCommGroup V] [Module 𝕜 V] (hd : 0 ≤ d) (hde : d ≤ e) (w : V) (p : List (𝕜 × V)) (t : 𝕜) : evalTimed ((e, w) :: p) t = evalTimed ((d, (d / e) • w) :: (e - d, ((e - d) / e) • w) :: p) t

Subdividing a segment w of duration e at the time d, for 0 ≤ d ≤ e, into its pieces (d / e) • w of duration d and ((e - d) / e) • w of duration e - d does not change the parametrized path.

Timed presentations in 𝕜

theorem TauCeti.PLPath.evalTimed_nonneg {𝕜 : Type u} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {φ : List (𝕜 × 𝕜)} (hφ : ∀ x ∈ φ, 0 ≤ x.1 ∧ 0 ≤ x.2) (t : 𝕜) : 0 ≤ evalTimed φ t

A timed presentation in 𝕜 with nonnegative segments has a nonnegative parametrized path.

theorem TauCeti.PLPath.monotone_evalTimed {𝕜 : Type u} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {φ : List (𝕜 × 𝕜)} (hφ : ∀ x ∈ φ, 0 ≤ x.1 ∧ 0 ≤ x.2) : Monotone (evalTimed φ)

A timed presentation in 𝕜 with nonnegative segments has a nondecreasing parametrized path.

theorem TauCeti.PLPath.exists_evalTimed_eq {𝕜 : Type u} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {φ : List (𝕜 × 𝕜)} (hφ : IsTimed φ) {u : 𝕜} (hu₀ : 0 ≤ u) (hu : u ≤ (List.map Prod.snd φ).sum) : ∃ (t : 𝕜), 0 ≤ t ∧ t ≤ duration φ ∧ evalTimed φ t = u

Every u ∈ [0, s], where s is the sum of the segments of a timed presentation φ in 𝕜, is a value of evalTimed φ on [0, duration φ].

Composing with a reparametrization

theorem TauCeti.PLPath.evalTimed_cons_comp {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q : List (𝕜 × V)} {d : 𝕜} [AddCommGroup V] [Module 𝕜 V] {v : V} {d' : 𝕜} {φ : List (𝕜 × 𝕜)} (hd : 0 < d) (hd' : 0 ≤ d') (hv : d' = 0 → v = 0) (hφ : ∀ x ∈ φ, 0 ≤ x.1 ∧ 0 ≤ x.2) (hq : ∀ x ∈ q, 0 ≤ x.1) (h : ∀ (t : 𝕜), evalTimed p t = evalTimed q (evalTimed φ t)) (t : 𝕜) : evalTimed ((d, v) :: p) t = evalTimed ((d', v) :: q) (evalTimed ((d, d') :: φ) t)

Prepending a segment v, run during time d on the source side and during time d' on the target side, to a factorization evalTimed p = evalTimed q ∘ evalTimed φ gives a factorization through the timing (d, d') :: φ. A zero target duration d' requires a stationary segment.

Reparametrization

def TauCeti.PLPath.IsReparam {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] (p q : List (𝕜 × V)) : Prop

p is a reparametrization of q: there is a timed presentation φ in 𝕜 with nonnegative segments, of duration duration p and with segments summing to duration q, such that evalTimed p = evalTimed q ∘ evalTimed φ. By TauCeti.PLPath.monotone_evalTimed and TauCeti.PLPath.exists_evalTimed_eq, evalTimed φ is a nondecreasing piecewise-linear map from [0, duration p] onto [0, duration q]; outside [0, duration p] both sides of the factorization are constant.

theorem TauCeti.PLPath.isReparam_iff {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] {p q : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] : IsReparam p q ↔ ∃ (φ : List (𝕜 × 𝕜)), IsTimed φ ∧ (∀ x ∈ φ, 0 ≤ x.2) ∧ duration φ = duration p ∧ (List.map Prod.snd φ).sum = duration q ∧ ∀ (t : 𝕜), evalTimed p t = evalTimed q (evalTimed φ t)

The characterization of reparametrizations by their timings, for use outside this file.

theorem TauCeti.PLPath.isReparam_of_map_snd_eq {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] (hp : IsTimed p) (hq : IsTimed q) (h : List.map Prod.snd p = List.map Prod.snd q) : IsReparam p q

Two timed presentations with the same segments are reparametrizations of each other.

theorem TauCeti.PLPath.IsReparam.refl {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] (hp : IsTimed p) : IsReparam p p

A timed presentation is a reparametrization of itself, through the identity timing.

theorem TauCeti.PLPath.IsReparam.cons {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q : List (𝕜 × V)} {d : 𝕜} [AddCommGroup V] [Module 𝕜 V] (h : IsReparam p q) (hd : 0 < d) (hq : ∀ x ∈ q, 0 ≤ x.1) (v : V) : IsReparam ((d, v) :: p) ((d, v) :: q)

Prepending the same segment, run during the same time, preserves reparametrization.

theorem TauCeti.PLPath.IsReparam.append {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {p₁ p₂ q₁ q₂ : List (𝕜 × V)} (h₁ : IsReparam p₁ q₁) (h₂ : IsReparam p₂ q₂) (hq₁ : IsTimed q₁) (hq₂ : ∀ x ∈ q₂, 0 ≤ x.1) : IsReparam (p₁ ++ p₂) (q₁ ++ q₂)

Concatenating reparametrizations is a reparametrization: the timings concatenate.

theorem TauCeti.PLPath.isReparam_cons_cons_add {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {r : List (𝕜 × V)} {d e : 𝕜} [AddCommGroup V] [Module 𝕜 V] {v w : V} (hd : 0 < d) (he : 0 < e) (hvw : SameRay 𝕜 v w) (hr : IsTimed r) : IsReparam ((d, v) :: (e, w) :: r) ((d + e, v + w) :: r)

Merging two adjacent segments pointing in the same direction, run during the sum of their durations, is a reparametrization.

Composites of parametrized paths

@[irreducible]

def TauCeti.PLPath.timedComp {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] : List (𝕜 × V) → List (𝕜 × 𝕜) → List (𝕜 × V)

A list of (duration, segment) pairs presenting the composite evalTimed q ∘ evalTimed φ of the parametrized path of q with a timing φ in 𝕜, when q and φ are timed presentations and every segment of φ is nonnegative (see TauCeti.PLPath.evalTimed_timedComp). It runs through the pieces of φ in turn: a piece of φ that ends before the current segment (e, w) of q does is run along the corresponding part of w, and a piece of φ that ends after it is subdivided at the end of that segment.

theorem TauCeti.PLPath.evalTimed_timedComp {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {q : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] {φ : List (𝕜 × 𝕜)} (hq : IsTimed q) (hφ : IsTimed φ) (hφ' : ∀ x ∈ φ, 0 ≤ x.2) (t : 𝕜) : evalTimed (timedComp q φ) t = evalTimed q (evalTimed φ t)

TauCeti.PLPath.timedComp q φ presents the composite evalTimed q ∘ evalTimed φ.

theorem TauCeti.PLPath.isTimed_timedComp {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {q : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] {φ : List (𝕜 × 𝕜)} (hq : IsTimed q) (hφ : IsTimed φ) : IsTimed (timedComp q φ)

@[simp]

theorem TauCeti.PLPath.duration_timedComp {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] (q : List (𝕜 × V)) (φ : List (𝕜 × 𝕜)) : duration (timedComp q φ) = duration φ

theorem TauCeti.PLPath.timedComp_snd_nonneg {𝕜 : Type u} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {q φ : List (𝕜 × 𝕜)} (hq' : ∀ x ∈ q, 0 ≤ x.2) (hφ' : ∀ x ∈ φ, 0 ≤ x.2) (x : 𝕜 × 𝕜) : x ∈ timedComp q φ → 0 ≤ x.2

Composing a presentation in 𝕜 with nonnegative segments with a timing with nonnegative segments gives nonnegative segments again.

theorem TauCeti.PLPath.ofSegments_map_snd_timedComp {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {q : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] {φ : List (𝕜 × 𝕜)} (hq : IsTimed q) (hφ' : ∀ x ∈ φ, 0 ≤ x.2) (h : duration q ≤ (List.map Prod.snd φ).sum) : ofSegments 𝕜 (List.map Prod.snd (timedComp q φ)) = ofSegments 𝕜 (List.map Prod.snd q)

When the timing φ runs through all of q, the composite TauCeti.PLPath.timedComp q φ presents the same TauCeti.PLPath as q.

The parametrized path determines the presented path

theorem TauCeti.PLPath.ofSegments_map_snd_eq_of_evalTimed_eq {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] (hp : IsTimed p) (hq : IsTimed q) (h : ∀ (t : 𝕜), evalTimed p t = evalTimed q t) : ofSegments 𝕜 (List.map Prod.snd p) = ofSegments 𝕜 (List.map Prod.snd q)

Two timed presentations with the same parametrized path present the same TauCeti.PLPath: the presented TauCeti.PLPath depends only on the parametrized path.

Reparametrizations present the same path

theorem TauCeti.PLPath.IsReparam.trans {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q r : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] (hpq : IsReparam p q) (hqr : IsReparam q r) : IsReparam p r

Reparametrization is transitive: the timings compose by TauCeti.PLPath.timedComp.

theorem TauCeti.PLPath.IsReparam.ofSegments_map_snd_eq {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] (h : IsReparam p q) (hp : IsTimed p) (hq : IsTimed q) : ofSegments 𝕜 (List.map Prod.snd p) = ofSegments 𝕜 (List.map Prod.snd q)

A reparametrization presents the same TauCeti.PLPath.

theorem TauCeti.PLPath.exists_isReparam_map_snd_eq_normalize {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] (hp : IsTimed p) : ∃ (r : List (𝕜 × V)), IsTimed r ∧ List.map Prod.snd r = normalize 𝕜 (List.map Prod.snd p) ∧ IsReparam p r

Every timed presentation is a reparametrization of a timed presentation of its normal form.

theorem TauCeti.PLPath.ofSegments_map_snd_eq_iff_exists_isReparam {𝕜 : Type u} {V : Type v} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q : List (𝕜 × V)} [AddCommGroup V] [Module 𝕜 V] (hp : IsTimed p) (hq : IsTimed q) (hp₀ : 0 < duration p) (hq₀ : 0 < duration q) {T : 𝕜} (hT : 0 < T) : ofSegments 𝕜 (List.map Prod.snd p) = ofSegments 𝕜 (List.map Prod.snd q) ↔ ∃ (r : List (𝕜 × V)), IsTimed r ∧ duration r = T ∧ IsReparam p r ∧ IsReparam q r

Faithfulness of the segment-list model. Two timed presentations of positive duration present the same TauCeti.PLPath exactly when they are both reparametrizations of a common timed presentation, which can be chosen of any prescribed positive duration T. For T = 1 and presentations of duration 1, these are nondecreasing surjective piecewise-linear reparametrizations of [0, 1].