Continuity at the observed terminal source time #
Continuity of a cut at its cutoff gives left continuity of the source at the corresponding interior time. Càdlàg right continuity supplies the other side.
theorem
BGW.StableTrees.continuousAt_source_of_translatedStoppedCut
{M : ℝ}
{T : NNReal}
(hT : 0 < T)
(f : Skorokhod.D M ℝ)
(g d q : ↑(Set.Icc 0 M))
(hgd : g ≤ d)
(hqt : ↑q = ↑g + ↑T)
(hqd : q < d)
(hc : ContinuousAt ⇑(translatedStoppedCut T f g d hgd) ⟨↑T, ⋯⟩)
:
ContinuousAt (⇑f) q
Continuity at an interior cut cutoff implies continuity of the source at the shifted cutoff. Reference: Billingsley (1999), Chapter 3.