Characterization of the stable Lévy law on Skorokhod space

Finite-dimensional increments characterize the law and are preserved under restriction and stable scaling.

The predicate characterizes the spectrally positive θ-stable Lévy law only for 1 < θ ≤ 2 and 0 < T; outside that range stableLaw is a junk Dirac mass and the zero-path law satisfies it.

References: J. Bertoin, Lévy Processes (1996), ch. I and VII; K. Sato, Lévy Processes and Infinitely Divisible Distributions (1999), §§11, 14.

structure BGW.StableTrees.IsStableLevyLaw (θ T : ℝ) (P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)) : Prop

P is a law of a spectrally positive θ-stable Lévy process on [0,T], expressed through its finite-dimensional increments and its initial value.

• start (h : 0 ≤ T) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, f ⟨0, ⋯⟩ = 0

  The path starts at zero almost surely whenever the horizon is nonnegative.

• increments (k : ℕ) (t : Fin (k + 1) → ↑(Set.Icc 0 T)) : StrictMono t → ↑(t 0) = 0 → MeasureTheory.Measure.map (fun (f : Skorokhod.D T ℝ) (i : Fin k) => f (t i.succ) - f (t i.castSucc)) ↑P = MeasureTheory.Measure.pi fun (i : Fin k) => ↑(stableLawAt θ (↑(t i.succ) - ↑(t i.castSucc)))

  Increments along increasing times starting at zero have independent stable laws.

theorem BGW.StableTrees.IsStableLevyLaw.unique {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) {P Q : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) (hQ : IsStableLevyLaw θ T Q) : P = Q

Uniqueness of the stable Lévy law on a positive horizon.

theorem BGW.StableTrees.IsStableLevyLaw.map_increments {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) (k : ℕ) (t : Fin (k + 1) → ↑(Set.Icc 0 T)) (ht : StrictMono t) : MeasureTheory.Measure.map (fun (f : Skorokhod.D T ℝ) (i : Fin k) => f (t i.succ) - f (t i.castSucc)) ↑P = MeasureTheory.Measure.pi fun (i : Fin k) => ↑(stableLawAt θ (↑(t i.succ) - ↑(t i.castSucc)))

Increments along any strictly increasing finite family of times are independent with stable laws, whether or not the first time is zero.

theorem BGW.StableTrees.IsStableLevyLaw.ae_continuousAt {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) (t : ↑(Set.Icc 0 T)) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑P, ContinuousAt (⇑f) t

P3: the stable Lévy law is almost surely continuous at each fixed time, including T. The quantifier over the time is outside ∀ᵐ.

theorem BGW.StableTrees.measurable_restrict {T a : ℝ} (haT : a ≤ T) : Measurable (Skorokhod.restrict haT)

Restriction to a shorter horizon is measurable for the Borel structures.

theorem BGW.StableTrees.IsStableLevyLaw.map_restrict {θ T a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (haT : a ≤ T) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) : IsStableLevyLaw θ a (P.map (Skorokhod.restrict haT))

The restriction of a stable Lévy law to a positive subhorizon is a stable Lévy law.

theorem BGW.StableTrees.measurable_timeSpaceScale_fixed {T : ℝ} (hT : 0 < T) {c : ℝ} (hc : 0 < c) (k : ℝ) : Measurable fun (f : Skorokhod.D (c * T) ℝ) => Skorokhod.timeSpaceScale T ⋯ (f, k, ⟨c, ⋯⟩)

For fixed positive horizons, time–space scaling is Borel measurable.

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

The stable Lévy law rescales to the original horizon after inverse stable space scaling.