The Markov property of the stable excursion measure

The strong Markov property at strict age crossings gives the identity for each selected excursion. Exact-once reindexing, compensation and nonnegative summation give the identity under the excursion measure.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.excursion_markov_lintegral {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) (F : Skorokhod.D ↑t ℝ → ENNReal) (hF : Measurable F) (G : Skorokhod.DLoc → ENNReal) (hG : Measurable G) : ∫⁻ (e : Excursion) in {e : Excursion | t < e.lifetime}, F (excursionRestrict t e) * G (futureFrom t e) ∂excursionMeasure θ = ∫⁻ (e : Excursion) in {e : Excursion | t < e.lifetime}, F (excursionRestrict t e) * ∫⁻ (f : Skorokhod.DLoc), G f ∂(killedStableKernel θ) (e.valueNN t) ∂excursionMeasure θ

Excursion Markov property. For nonnegative measurable F on the prefix path space D t ℝ (through excursionRestrict t) and G on the whole future (through the uncentred futureFrom t): N[1_{ζ>t} F(r_t e) G(e(t+·))] = N[1_{ζ>t} F(r_t e) (K_{e(t)} G)].