Passage endpoints after a restart

Deterministic inverse-passage identities used for translating marked excursions.

(J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.)

theorem BGW.StableTrees.ae_excursionPointMeasure_shift {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (a : NNReal), excursionPointMeasure (Skorokhod.DLoc.shiftAt (firstPassageBelow a) f) = MeasureTheory.Measure.map (fun (p : NNReal × Excursion) => (p.1 - a, p.2)) ((excursionPointMeasure f).restrict (Set.Ioi a ×ˢ Set.univ))

Shift identity (deterministic on a good event, simultaneously in all levels a): the excursion point measure of the post-T_a centered path is the translate by a of the restriction of μ f to labels > a (same cuts, since T_{(x-a)-}(f') = T_{x-}(f) - T_a).