Translated stopped cuts on a fixed horizon

The finite-horizon cut is centered at its initial point and continued constantly after its end.

noncomputable def BGW.StableTrees.translatedStoppedCut {M : ℝ} (T : NNReal) (p : Skorokhod.D M ℝ) (g d : ↑(Set.Icc 0 M)) (hgd : g ≤ d) : Skorokhod.D ↑T ℝ

Center a finite path at g, stop at d, and continue constantly to the horizon T. Reference: Billingsley (1999), Chapter 3.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.translatedStoppedCut_apply {M : ℝ} (T : NNReal) (p : Skorokhod.D M ℝ) (g d : ↑(Set.Icc 0 M)) (hgd : g ≤ d) (t : ↑(Set.Icc 0 ↑T)) : (translatedStoppedCut T p g d hgd) t = p ⟨min (↑g + ↑t) ↑d, ⋯⟩ - p g

The finite stopped cut has the usual translated, clipped evaluation formula. Reference: Billingsley (1999), Chapter 3.