Independence auxiliaries for the stable process

The increments of a stable Lévy law along strictly increasing times are independent with stable marginals. From this, the restricted past and the future increment path are independent, and the future increment path is again a stable Lévy law (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter I).

theorem BGW.StableTrees.IsStableLevyLaw.map_sub_eval {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) (r t : ↑(Set.Icc 0 T)) (hrt : r < t) : MeasureTheory.Measure.map (fun (f : Skorokhod.D T ℝ) => f t - f r) ↑P = ↑(stableLawAt θ (↑t - ↑r))

A single increment of a stable Lévy law has the corresponding stable law.

theorem BGW.StableTrees.IsStableLevyLaw.iIndepFun_eval_sub_of_strictMono {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) (n : ℕ) (t : Fin (n + 1) → ↑(Set.Icc 0 T)) (ht : StrictMono t) : ProbabilityTheory.iIndepFun (fun (i : Fin n) (f : Skorokhod.D T ℝ) => f (t i.succ) - f (t i.castSucc)) ↑P

The increments along strictly increasing times are independent.

theorem BGW.StableTrees.IsStableLevyLaw.indepFun_restrict_shiftIncrement {θ T s : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) (hs : 0 ≤ s) (hsT : s ≤ T) : ProbabilityTheory.IndepFun (Skorokhod.restrict hsT) (Skorokhod.shiftIncrement hs hsT) ↑P

The whole restricted past is independent of the whole future increment path.

theorem BGW.StableTrees.IsStableLevyLaw.isStableLevyLaw_map_shiftIncrement {θ T s : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) (hs : 0 ≤ s) (hsT : s ≤ T) : IsStableLevyLaw θ (T - s) (P.map (Skorokhod.shiftIncrement hs hsT))

Shifting a stable Lévy law to a positive remaining horizon gives a stable Lévy law.

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

The future increment path has the stable process law on the remaining horizon.