Uniform control of aligned Vervaat transforms

After aligning the minimizing times, rotation preserves uniform path control. The two endpoint values and the infimum account for the additional errors.

theorem BGW.Skorokhod.exists_vervaat_timeChange_bound (u f : D 1 ℝ) (ρ : TimeChange 1) (halign : ρ (vervaatTime f) = vervaatTime u) {d e : ℝ} (hd : ∀ (t : ↑(Set.Icc 0 1)), |↑(ρ t) - ↑t| ≤ d) (hp : ∀ (t : ↑(Set.Icc 0 1)), dist (u (ρ t)) (f t) ≤ e) (hm : dist (⨅ (s : ↑(Set.Icc 0 1)), u s) (⨅ (s : ↑(Set.Icc 0 1)), f s) ≤ e) : ∃ (μ : TimeChange 1), (∀ (t : ↑(Set.Icc 0 1)), |↑(μ t) - ↑t| ≤ 2 * d + |↑(vervaatTime u) - ↑(vervaatTime f)|) ∧ ∀ (t : ↑(Set.Icc 0 1)), dist ((vervaatD u) (μ t)) ((vervaatD f) t) ≤ 4 * e

Rotating an aligned approximation controls both the time and path errors.