Independent reversed prefix and fresh increments

Reversal preserves the compact prefix law, and deterministic-time independence separates that prefix from the future increment path.

theorem BGW.StableTrees.measurable_restrict_height_filtration (t : NNReal) : Measurable (Skorokhod.DLoc.restrict t)

The compact prefix is measurable for the right-continuous past filtration.

theorem BGW.StableTrees.map_reversed_prefix_shift_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => (Skorokhod.DLoc.restrict t (reversedAt t f), Skorokhod.DLoc.shift t f)) ↑(stableLocalLaw θ) = (MeasureTheory.Measure.map (Skorokhod.DLoc.restrict t) ↑(stableLocalLaw θ)).prod ↑(stableLocalLaw θ)

Reversed prefix and fresh increments have the independent stable product law.