Measurability of the limiting extraction triple

The first long label is a.e. measurable. Jointly measurable passage maps and excursion restriction then give the limiting endpoints and cut as an a.e. measurable map.

theorem BGW.StableTrees.PathTail.aemeasurable_firstLongEnd {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : AEMeasurable (fun (f : Skorokhod.DLoc) => passageTime (firstLongLabel f) f) ↑(stableLocalLaw θ)

The selected end is a.e. measurable under the local stable law.

theorem BGW.StableTrees.PathTail.aemeasurable_longCutTriple {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : AEMeasurable (longCutTriple T) ↑(stableLocalLaw θ)

The endpoint/cut triple is a.e. measurable under the local stable law.