Scaling and the simple Markov property of the stable process

The time-space scaling identity follows from the characterization of the stable process law. The simple Markov property expresses independence of the restricted past and the future increment path, and identifies the law of the latter (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter I, Section 1 and Chapter VIII).

theorem BGW.StableTrees.stableProcessLaw_scaling {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) {c : ℝ} (hc : 0 < c) : ((stableProcessLaw θ (c * T)).map fun (f : Skorokhod.D (c * T) ℝ) => Skorokhod.timeSpaceScale T ⋯ (f, c ^ (-(1 / θ)), ⟨c, ⋯⟩)) = stableProcessLaw θ T

Time-space scaling of the stable process law from horizon c * T to T.

theorem BGW.StableTrees.stableProcessLaw_simpleMarkov {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) {s : ℝ} (hs : 0 ≤ s) (hsT : s ≤ T) : ProbabilityTheory.IndepFun (Skorokhod.restrict hsT) (Skorokhod.shiftIncrement hs hsT) ↑(stableProcessLaw θ T) ∧ (stableProcessLaw θ T).map (Skorokhod.shiftIncrement hs hsT) = stableProcessLaw θ (T - s)

Simple Markov property at a deterministic time s ∈ [0, T], as independence of the whole past path (the natural past, via comap_restrict_eq_iSup_comap_eval) and the whole future increment path, together with the law of the future increment path.