Independent increments of the passage subordinator

This module upgrades the strong-Markov factorization at one level to arbitrary finite strictly increasing level grids (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII, Theorem 1).

theorem BGW.StableTrees.firstPassage_map_increments {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (k : ℕ) (x : Fin (k + 1) → NNReal) (hx : StrictMono x) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) (i : Fin k) => ↑(passageTime (x i.succ) f) - ↑(passageTime (x i.castSucc) f)) ↑(stableLocalLaw θ) = MeasureTheory.Measure.pi fun (i : Fin k) => passageLaw θ (x i.succ - x i.castSucc)

Independent increments over a strictly increasing level grid.