Extension of a clock from an interior interval #
Affine initial and final segments extend an increasing map to a time change. Its displacement is bounded by the displacement on the preserved middle interval.
theorem
BGW.StableTrees.exists_extraction_middle_timeChange
{T l r D : ℝ}
(hl : 0 < l)
(hlr : l < r)
(hrT : r < T)
(h : ↑(Set.Icc l r) → ℝ)
(hc : Continuous h)
(hm : StrictMono h)
(hlo : 0 < h ⟨l, ⋯⟩)
(hhi : h ⟨r, ⋯⟩ < T)
(hdisp : ∀ (t : ↑(Set.Icc l r)), |h t - ↑t| ≤ D)
:
Extend a middle clock affinely to both endpoints without increasing its displacement bound. Reference: Billingsley (1999), Chapter 3.