Rotating an aligned time change #
Two clipped coordinates give a continuous formula for circular rotation of an aligned time change. One coordinate is always an endpoint, so the two pieces match at the circular cut.
theorem
BGW.Skorokhod.exists_rotated_timeChange
(ρ : TimeChange 1)
(g a : ↑(Set.Icc 0 1))
(halign : ρ g = a)
{d : ℝ}
(hd : ∀ (t : ↑(Set.Icc 0 1)), |↑(ρ t) - ↑t| ≤ d)
:
An aligned time change rotates to a time change of the transformed paths.