Path estimates for the local window correction #
The source and corrected source times remain near the minimum inside the window. Outside it the original approximation is preserved exactly.
theorem
BGW.Skorokhod.exists_aligned_timeChange
(u f : D 1 ℝ)
(σ : TimeChange 1)
(g a : ↑(Set.Icc 0 1))
{η d e : ℝ}
(hη : 0 < η)
(hleft : η ≤ ↑g)
(hright : ↑g + η ≤ 1)
(hnear : dist ((OrderIso.symm σ) a) g < η)
(hd : ∀ (t : ↑(Set.Icc 0 1)), |↑(σ t) - ↑t| ≤ d)
(hp : ∀ (t : ↑(Set.Icc 0 1)), dist (u (σ t)) (f t) ≤ e)
(hf : ∀ (s : ↑(Set.Icc 0 1)), dist s g < 2 * η → dist (f s) (f g) ≤ e)
:
Align one time by a local correction, paying only the oscillation in its window.