Measurability of the exploration measure

The restricted Stieltjes measures form a measurable family of finite measures. A measurable height map then gives the exploration measure by pushforward.

theorem BGW.StableTrees.measurable_exploration_apply (θ : ℝ) {B : Set NNReal} (hB : MeasurableSet B) : Measurable fun (p : NNReal × Skorokhod.DLoc) => (exploration θ p.2 p.1) B

(t, f) ↦ ρ_t(B) is measurable for measurable B.