Large measurable events for source-horizon localization

A measurable version of the selected end gives measurable good events. Their bad probabilities vanish as the source horizon increases, by the sealed first-long-end supplier.

theorem BGW.StableTrees.PathTail.exists_firstLongEnd_good_set {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {δ : ℝ} (hδ : 0 < δ) : ∃ (M : NNReal) (_ : 0 < M) (G : Set Skorokhod.DLoc), MeasurableSet G ∧ (↑(stableLocalLaw θ)).real Gᶜ < δ ∧ ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), f ∈ G ↔ passageTime (firstLongLabel f) f < M

The first long excursion ends inside a deterministic positive horizon on a measurable event whose complement has arbitrarily small real probability.