Exponential clocks for the stable supremum

The path law and an independent exponential clock, with joint measurability and nonnegativity of the running supremum and its reflection.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

noncomputable def BGW.StableTrees.expClockLaw (θ q : ℝ) : MeasureTheory.Measure (Skorokhod.DLoc × ℝ)

Path law times an independent Exp(q) clock on DLoc × ℝ.

Equations

• BGW.StableTrees.expClockLaw θ q = (↑(BGW.StableTrees.stableLocalLaw θ)).prod (ProbabilityTheory.expMeasure q)

theorem BGW.StableTrees.isProbabilityMeasure_expClockLaw (θ : ℝ) {q : ℝ} (hq : 0 < q) : MeasureTheory.IsProbabilityMeasure (expClockLaw θ q)

The clock model is a probability space for q > 0.

theorem BGW.StableTrees.ae_clock_nonneg_expClockLaw (θ : ℝ) {q : ℝ} (hq : 0 < q) : ∀ᵐ (p : Skorokhod.DLoc × ℝ) ∂expClockLaw θ q, 0 ≤ p.2

The clock is a.s. nonnegative, so toNNReal reads it without junk.

theorem BGW.StableTrees.measurable_supRunning_expTime : Measurable fun (p : Skorokhod.DLoc × ℝ) => supRunning p.1 p.2.toNNReal

p ↦ S_{e_q} is measurable.

theorem BGW.StableTrees.measurable_supReflected_expTime : Measurable fun (p : Skorokhod.DLoc × ℝ) => supReflected p.1 p.2.toNNReal

p ↦ R_{e_q} = S_{e_q} - X_{e_q} is measurable.

theorem BGW.StableTrees.ae_nonneg_supRunning_supReflected_expTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : ∀ᵐ (p : Skorokhod.DLoc × ℝ) ∂expClockLaw θ q, 0 ≤ supRunning p.1 p.2.toNNReal ∧ 0 ≤ supReflected p.1 p.2.toNNReal

Both S_{e_q} and R_{e_q} are a.s. nonnegative (f 0 = 0 a.s.; R ≥ 0 always).