Continuity and identification at the selected long excursion

The good-path predicate gives continuity of the source at both selected endpoints, and the selected excursion is the actual translated stopped cut.

theorem BGW.StableTrees.GoodLongExtractionPath.continuousAt_firstLong_ends {M : NNReal} {f : Skorokhod.DLoc} (hf : GoodLongExtractionPath M f) : ContinuousAt (↑f) (passageTimeMinus (firstLongLabel f) f) ∧ ContinuousAt (↑f) (passageTime (firstLongLabel f) f)

The source path is continuous at both endpoints of the selected long excursion. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.GoodLongExtractionPath.translatedStoppedCut_eq {M T : NNReal} {f : Skorokhod.DLoc} (hf : GoodLongExtractionPath M f) : translatedStoppedCut T (Skorokhod.DLoc.restrict M f) ⟨↑(passageTimeMinus (firstLongLabel f) f), ⋯⟩ ⟨↑(passageTime (firstLongLabel f) f), ⋯⟩ ⋯ = excursionRestrict T (firstLongMark f)

The finite stopped cut of the restricted source is the selected excursion restriction. Reference: Billingsley (1999), Chapter 3.