Local correction of a time change

A triangular perturbation of the identity moves one interior time to a nearby time and is the identity outside a prescribed window. Its slope stays positive.

theorem BGW.Skorokhod.exists_local_timeChange (g a : ↑(Set.Icc 0 1)) {η : ℝ} (hη : 0 < η) (hleft : η ≤ ↑g) (hright : ↑g + η ≤ 1) (hnear : |↑a - ↑g| < η) : ∃ (κ : TimeChange 1), κ g = a ∧ (∀ (t : ↑(Set.Icc 0 1)), η ≤ |↑t - ↑g| → κ t = t) ∧ ∀ (t : ↑(Set.Icc 0 1)), |↑(κ t) - ↑t| ≤ |↑a - ↑g|

Move g to a by a time change supported in the radius η window around g. The displacement is at most the distance between the two times.