Documentation

BGW.StableTrees.LongExtractionCutTerminal

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.