The fresh marked measure at a passage time

Whole-path strong Markov transfers to arbitrary measurable modifications of the marked measure. Stopped-history measurability gives independent consecutive windows and the time-simple Lévy adapter with finite long-excursion rates.

(J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV, Sections 2–4; K. Itô, Poisson point processes attached to Markov processes, Proc. Sixth Berkeley Symp. Math. Statist. Probab. 3 (1972), 225–239.)

theorem BGW.StableTrees.map_excursionPointMeasure_shiftAt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => excursionPointMeasure (Skorokhod.DLoc.shiftAt (firstPassageBelow a) f)) ↑(stableLocalLaw θ) = MeasureTheory.Measure.map excursionPointMeasure ↑(stableLocalLaw θ)

Law of the future point measure: the post-T_a point measure has the same law as the whole point measure.

theorem BGW.StableTrees.measure_inter_excursionPointMeasure_shiftAt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) {A : Set Skorokhod.DLoc} (hA : MeasurableSet A) {B : Set (MeasureTheory.Measure (NNReal × Excursion))} (hB : MeasurableSet B) : ↑(stableLocalLaw θ) (A ∩ (fun (f : Skorokhod.DLoc) => excursionPointMeasure (Skorokhod.DLoc.shiftAt (firstPassageBelow a) f)) ⁻¹' B) = ↑(stableLocalLaw θ) A * ↑(stableLocalLaw θ) (excursionPointMeasure ⁻¹' B)

Independence of the future point measure from F_{T_a} (whole-path strong Markov at T_a plus the shift identity; scalar passage-increment independence is not enough).

theorem BGW.StableTrees.map_windowShift_excursionPointMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a h : NNReal) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => Probability.windowShift a (a + h) (excursionPointMeasure f)) ↑(stableLocalLaw θ) = MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => Probability.windowShift 0 h (excursionPointMeasure f)) ↑(stableLocalLaw θ)

Stationarity of window restrictions (the stationary field of IsTimeSimpleLevy; for the AE-measurable μ, through P.map).

theorem BGW.StableTrees.iIndepFun_windowRestrict_excursionPointMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hξ : Measurable ξ) (hae : ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure) (n : ℕ) (t : Fin (n + 1) → NNReal) (ht : Monotone t) : ProbabilityTheory.iIndepFun (fun (i : Fin n) (f : Skorokhod.DLoc) => Probability.windowRestrict (t i.castSucc) (t i.succ) (ξ f)) ↑(stableLocalLaw θ)

Independence of consecutive window restrictions (the indep field of IsTimeSimpleLevy), for any measurable modification ξ of the point measure (so that the σ-algebras involved are honest).

theorem BGW.StableTrees.isTimeSimpleLevy_of_ae_eq_excursionPointMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hξ : Measurable ξ) (hae : ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure) : Probability.IsTimeSimpleLevy (↑(stableLocalLaw θ)) ξ ∧ ∀ (ε : NNReal), 0 < ε → MeasurableSet {e : Excursion | ε < e.lifetime} ∧ Probability.IsFiniteRate (↑(stableLocalLaw θ)) ξ {e : Excursion | ε < e.lifetime}

Poisson characterization adapter: every measurable modification of the excursion point measure is a time-simple Lévy point measure, and every {ε < lifetime} has finite rate.