The stable process as a law on local càdlàg paths

This module constructs the stable process law on DLoc from its compatible integer-horizon marginals. It proves the characterization by compact restrictions and the coordinate properties used downstream: initial value, fixed-time marginals and continuity, and simultaneous spectral positivity (J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters I and VIII; P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Section 16).

def BGW.Skorokhod.DLoc.zero : DLoc

The zero local path.

Equations

• BGW.Skorokhod.DLoc.zero = ⟨fun (x : NNReal) => 0, BGW.Skorokhod.DLoc.zero._proof_1⟩

theorem BGW.StableTrees.stableProcessLaw_zero (θ : ℝ) : ↑(stableProcessLaw θ 0) = MeasureTheory.Measure.dirac (Skorokhod.ofContinuous (ContinuousMap.const (↑(Set.Icc 0 0)) 0))

At horizon zero, the stable process law is the Dirac mass at the zero path.

theorem BGW.StableTrees.stableProcessLaw_succ_restrict {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (n : ℕ) : (stableProcessLaw θ (↑(n + 1) + 1)).map (Skorokhod.restrict ⋯) = stableProcessLaw θ (↑n + 1)

Compatibility of the integer-horizon stable process laws under restriction (the compatibility hypothesis of exists_unique_compatiblePathLaw).

noncomputable def BGW.StableTrees.stableLocalLaw (θ : ℝ) : MeasureTheory.ProbabilityMeasure Skorokhod.DLoc

The local stable law. For 1 < θ ≤ 2: the unique law on DLoc whose integer-horizon restrictions are stableProcessLaw θ (n + 1), obtained from exists_unique_compatiblePathLaw and transported along measurableEquivCompatible.symm. Junk value (Dirac at the zero path) otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.map_restrict_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {T : NNReal} (hT : 0 < T) : MeasureTheory.Measure.map (Skorokhod.DLoc.restrict T) ↑(stableLocalLaw θ) = ↑(stableProcessLaw θ ↑T)

Restriction. The restriction of the local stable law to every positive real horizon T is the compact stable process law P_T.

theorem BGW.StableTrees.stableLocalLaw_of_not {θ : ℝ} (hθ : ¬(1 < θ ∧ θ ≤ 2)) : stableLocalLaw θ = ⟨MeasureTheory.Measure.dirac Skorokhod.DLoc.zero, ⋯⟩

Junk branch of the definition.

theorem BGW.StableTrees.stableLocalLaw_restrict {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {T : NNReal} (hT : 0 < T) : (stableLocalLaw θ).map (Skorokhod.DLoc.restrict T) = stableProcessLaw θ ↑T

The same statement in ProbabilityMeasure form.

theorem BGW.StableTrees.eq_stableLocalLaw_of_forall_nat {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {Q : MeasureTheory.ProbabilityMeasure Skorokhod.DLoc} (h : ∀ (n : ℕ), MeasureTheory.Measure.map (Skorokhod.DLoc.restrict (↑n + 1)) ↑Q = ↑(stableProcessLaw θ ↑(↑n + 1))) : Q = stableLocalLaw θ

Uniqueness, restricted to the integer horizons (the form used with exists_unique_compatiblePathLaw).

theorem BGW.StableTrees.eq_stableLocalLaw_iff {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {Q : MeasureTheory.ProbabilityMeasure Skorokhod.DLoc} : Q = stableLocalLaw θ ↔ ∀ (T : NNReal), 0 < T → MeasureTheory.Measure.map (Skorokhod.DLoc.restrict T) ↑Q = ↑(stableProcessLaw θ ↑T)

Characterization and uniqueness. A law on DLoc is the local stable law iff its restriction to every positive horizon is the stable process law.

theorem BGW.StableTrees.map_restrict_zero_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.Measure.map (Skorokhod.DLoc.restrict 0) ↑(stableLocalLaw θ) = ↑(stableProcessLaw θ 0)

Restriction to horizon zero: the zero-path Dirac mass, i.e. stableProcessLaw θ 0.

theorem BGW.StableTrees.map_eval_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (Skorokhod.DLoc.eval t) ↑(stableLocalLaw θ) = ↑(stableLawAt θ ↑t)

Fixed-time marginals: X_t ∼ stableLawAt θ t for t > 0.

theorem BGW.StableTrees.ae_eval_zero_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ↑f 0 = 0

The local stable process starts at 0 almost surely.

theorem BGW.StableTrees.ae_continuousAt_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ContinuousAt (↑f) t

No fixed discontinuities: for each deterministic time t, almost surely the path is continuous at t (at t = 0 this is right-continuity in ℝ≥0).

theorem BGW.StableTrees.ae_leftLim_le_stableLocalLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), Function.leftLim (↑f) t ≤ ↑f t

Spectral positivity, simultaneously at all times: almost surely, for every t : ℝ≥0, the left limit does not exceed the value.