The infimum and drawdown at an independent exponential clock

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

noncomputable def BGW.StableTrees.infimumLevel (p : NNReal × Skorokhod.DLoc) : ℝ

The infimum coordinate as a separate function of nonnegative time and path.

Equations

• BGW.StableTrees.infimumLevel p = BGW.StableTrees.localTime p.2 p.1

noncomputable def BGW.StableTrees.clockLocalTime (p : Skorokhod.DLoc × ℝ) : ℝ

The infimum local time evaluated at the independent clock.

Equations

• BGW.StableTrees.clockLocalTime p = BGW.StableTrees.infimumLevel (p.2.toNNReal, p.1)

theorem BGW.StableTrees.measurable_clockLocalTime : Measurable clockLocalTime

Measurability of the infimum local time at the clock.

theorem BGW.StableTrees.lintegral_supReflected_eq_localTime_expTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {G : ℝ → ENNReal} (hG : Measurable G) : ∫⁻ (p : Skorokhod.DLoc × ℝ), G (supReflected p.1 p.2.toNNReal) ∂expClockLaw θ q = ∫⁻ (p : Skorokhod.DLoc × ℝ), G (clockLocalTime p) ∂expClockLaw θ q

Fixed-time reversal integrated over the independent clock identifies the drawdown marginal with the negative infimum marginal.

theorem BGW.StableTrees.expClockLaw_clockLocalTime_gt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (x : NNReal) : (expClockLaw θ q) {p : Skorokhod.DLoc × ℝ | ↑x < clockLocalTime p} = ENNReal.ofReal (Real.exp (-↑x * q ^ (1 / θ)))

The local-time tail at an independent exponential clock is the passage Laplace transform.

theorem BGW.StableTrees.expClockLaw_supReflected_gt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {y : ℝ} (hy : 0 ≤ y) : (expClockLaw θ q) {p : Skorokhod.DLoc × ℝ | y < supReflected p.1 p.2.toNNReal} = ENNReal.ofReal (Real.exp (-(y * q ^ (1 / θ))))

Tail form: P ⊗ Exp(q) (R_{e_q} > y) = e^{-y q^{1/θ}} for y ≥ 0.

theorem BGW.StableTrees.law_supReflected_expTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : MeasureTheory.Measure.map (fun (p : Skorokhod.DLoc × ℝ) => supReflected p.1 p.2.toNNReal) (expClockLaw θ q) = ProbabilityTheory.expMeasure (q ^ (1 / θ))

Exponential drawdown. S_{e_q} - X_{e_q} ~ Exp(q^{1/θ}).