Consequences of the excursion Markov property

The measurable lifetime bridge gives the residual passage law. Finite survival measures also permit bounded signed tests. Restarting at half the observation time proves the absence of fixed jumps under the excursion measure.

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

theorem BGW.StableTrees.excursion_remainingLifetime_lintegral {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) (F : Skorokhod.D ↑t ℝ → ENNReal) (hF : Measurable F) (H : ℝ → ENNReal) (hH : Measurable H) : ∫⁻ (e : Excursion) in {e : Excursion | t < e.lifetime}, F (excursionRestrict t e) * H (↑e.lifetime - ↑t) ∂excursionMeasure θ = ∫⁻ (e : Excursion) in {e : Excursion | t < e.lifetime}, F (excursionRestrict t e) * ∫⁻ (s : ℝ), H s ∂passageLaw θ (e.valueNN t) ∂excursionMeasure θ

Remaining-lifetime identity. Given the prefix up to age t, the remaining lifetime ζ - t has the law of the passage time T_{e(t)} of the stable process, i.e. passageLaw θ (e(t)) (whose density is qKernel, see passageLaw_eq_qKernel). For measurable H : ℝ → ℝ≥0∞. Proof route: the bridge ae_lastPositiveTime_futureFrom/_killedPath, not firstHitBelow.

theorem BGW.StableTrees.excursion_markov_integral {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) (F : Skorokhod.D ↑t ℝ → ℝ) (hF : Measurable F) (hFb : ∃ (C : ℝ), ∀ (p : Skorokhod.D ↑t ℝ), |F p| ≤ C) (G : Skorokhod.DLoc → ℝ) (hG : Measurable G) (hGb : ∃ (C : ℝ), ∀ (f : Skorokhod.DLoc), |G f| ≤ C) : ∫ (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 θ

Signed bounded-test version of the Markov property (finite survival measure, Markov kernel).

theorem BGW.StableTrees.N_noFixedJump {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) : ∀ᵐ (e : Excursion) ∂excursionMeasure θ, Function.leftLim (↑e.path) t = ↑e.path t

No fixed jumps under N: for each t > 0, N-a.e. excursion is left-continuous at t (restart at t/2; the killed path creates no jump since the passage creeps).