Absolute continuity of excursion increment windows

The forward Markov property at a positive deterministic age transfers stable null sets to centered excursion increments on an interior window. Killing agrees with the full path on survival, and no restart at the random excursion start is used.

theorem BGW.StableTrees.restrict_center_killedPath {f : Skorokhod.DLoc} {y r τ : NNReal} (hT : firstPassageBelow y f = ↑τ) (hr : r < τ) (hf : ↑f 0 = 0) : Skorokhod.DLoc.restrict r (Skorokhod.DLoc.shift 0 (killedPath y f)) = Skorokhod.DLoc.restrict r f

Centering an unkilled initial window of a killed path recovers the stable prefix.

theorem BGW.StableTrees.shift_zero_futureFrom (s : NNReal) (e : Excursion) : Skorokhod.DLoc.shift 0 (futureFrom s e) = Skorokhod.DLoc.shift s e.path

Centered increments of a future excursion path are its ordinary centered shift.

theorem BGW.StableTrees.killedStableKernel_center_prefix_null {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (r y : NNReal) {A : Set (Skorokhod.D ↑r ℝ)} (hA : MeasurableSet A) (hnull : (MeasureTheory.Measure.map (Skorokhod.DLoc.restrict r) ↑(stableLocalLaw θ)) A = 0) : ((killedStableKernel θ) y) {g : Skorokhod.DLoc | 0 < ↑g r ∧ Skorokhod.DLoc.restrict r (Skorokhod.DLoc.shift 0 g) ∈ A} = 0

A null stable prefix event remains null for surviving centered killed paths.

theorem BGW.StableTrees.excursion_shift_prefix_absolutelyContinuous {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (s r : NNReal) (hs : 0 < s) : (MeasureTheory.Measure.map (fun (e : Excursion) => Skorokhod.DLoc.restrict r (Skorokhod.DLoc.shift s e.path)) ((excursionMeasure θ).restrict {e : Excursion | s + r < e.lifetime})).AbsolutelyContinuous (MeasureTheory.Measure.map (Skorokhod.DLoc.restrict r) ↑(stableLocalLaw θ))

Centered excursion increments strictly after the start have an absolutely continuous prefix law on survival to the end of their window.