Passage subordinator and local time at the minimum

The strict downward passage times of the spectrally positive stable process form a càdlàg subordinator. Its right-continuous inverse is the negative running infimum, whose Stieltjes measure is carried by the zero set of the reflected path.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII, Section 1 and Chapter IV, for the local time at the infimum and its inverse.

noncomputable def BGW.StableTrees.passageTime (x : NNReal) (f : Skorokhod.DLoc) : NNReal

The ℝ≥0-valued passage time (junk value 0 on {T_x = ⊤}, a null set).

Equations

• BGW.StableTrees.passageTime x f = WithTop.untopD 0 (BGW.StableTrees.firstPassageBelow x f)

noncomputable def BGW.StableTrees.firstHitBelow (x : NNReal) (f : Skorokhod.DLoc) : WithTop NNReal

First hitting time of (-∞, -x], H_x = inf{t | X_t ≤ -x} (weak hitting, NOT strict).

Equations

• BGW.StableTrees.firstHitBelow x f = sInf {t : WithTop NNReal | ∃ (u : NNReal), t = ↑u ∧ ↑f u ≤ -↑x}

noncomputable def BGW.StableTrees.passageLaw (θ : ℝ) (x : NNReal) : MeasureTheory.Measure ℝ

The law of the passage time T_x under the local stable law, as a measure on ℝ (finite reading passageTime).

Equations

• BGW.StableTrees.passageLaw θ x = MeasureTheory.Measure.map (fun (f : BGW.Skorokhod.DLoc) => ↑(BGW.StableTrees.passageTime x f)) ↑(BGW.StableTrees.stableLocalLaw θ)

theorem BGW.StableTrees.measurable_passageTime (x : NNReal) : Measurable (passageTime x)

passageTime x is measurable in the path.

theorem BGW.StableTrees.measurable_passageTime_uncurry : Measurable fun (p : NNReal × Skorokhod.DLoc) => passageTime p.1 p.2

Joint measurability of (x, f) ↦ T_x(f) (finite reading).

theorem BGW.StableTrees.passageLaw_isProbabilityMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) : MeasureTheory.IsProbabilityMeasure (passageLaw θ x)

passageLaw θ x is a probability measure (x = 0 uses T_0 = 0).

Pathwise structure: finiteness, monotonicity, strict right-continuity, T_0 = 0

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

Almost surely, for every x ≥ 0, T_x is finite and equals its finite reading, and T_0 = 0.

theorem BGW.StableTrees.ae_isCadlag_monotone_passage {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (IsCadlag fun (x : NNReal) => ↑(passageTime x f)) ∧ (Monotone fun (x : NNReal) => passageTime x f) ∧ passageTime 0 f = 0

Monotone, càdlàg, starts at 0 Right-continuity here is the one for the strict passage time T_x = inf{t | X_t < -x}.

theorem BGW.StableTrees.ae_tendsto_passageTime_atTop {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Filter.Tendsto (fun (x : NNReal) => passageTime x f) Filter.atTop Filter.atTop

Almost surely T is unbounded: T_x → ∞ as x → ∞.

Inverse relation with the running infimum (L = -runningInf is the local time)

theorem BGW.StableTrees.firstPassageBelow_eq_inverseLocalTime (x : NNReal) (f : Skorokhod.DLoc) : firstPassageBelow x f = sInf {t : WithTop NNReal | ∃ (u : NNReal), t = ↑u ∧ ↑x < -runningInfLoc f u}

T is the strict right inverse of L = -runningInf: T_x = inf{t | L_t > x}. This is a deterministic identity, valid for every path (bounded-below on compacts), every x ≥ 0, and the inf over the empty set is ⊤.

theorem BGW.StableTrees.runningInf_lt_sandwich (x t : NNReal) (f : Skorokhod.DLoc) : (firstPassageBelow x f < ↑t → runningInfLoc f t < -↑x) ∧ (runningInfLoc f t < -↑x → firstPassageBelow x f ≤ ↑t)

Event sandwich for the running infimum, strict side. For every path, level and time: {T_x < t} ⊆ {I_t < -x} ⊆ {T_x ≤ t}.

theorem BGW.StableTrees.runningInf_le_of_firstHitBelow_le (x t : NNReal) (f : Skorokhod.DLoc) (h : firstHitBelow x f ≤ ↑t) : runningInfLoc f t ≤ -↑x

Weak side of the sandwich. For every path, H_x ≤ t → I_t ≤ -x; also T_x ≤ t → I_t ≤ -x (deterministic; stated a.s. for uniformity with the other items). The converses are NOT claimed: at a plateau level x of L (an excursion from the minimum straddling t) one has I_t = -x but T_x > t.

theorem BGW.StableTrees.ae_runningInf_le_of_firstPassageBelow_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x t : NNReal), firstPassageBelow x f ≤ ↑t → runningInfLoc f t ≤ -↑x

theorem BGW.StableTrees.iSup_firstPassageBelow_le_firstHitBelow_le (f : Skorokhod.DLoc) {x : NNReal} (hx : 0 < x) : ⨆ (y : ↑(Set.Iio x)), firstPassageBelow (↑y) f ≤ firstHitBelow x f ∧ firstHitBelow x f ≤ firstPassageBelow x f

Strict passage versus first hitting (deterministic sandwich). For every path and level x > 0, sup_{y<x} T_y ≤ H_x ≤ T_x. The left limit T_{x-} of the passage process is at most the first hitting time of -x; a plateau of -runningInf at level x is exactly where these are <.

Local time L = -I: measurability, adaptedness, Stieltjes concentration, straddling

noncomputable def BGW.StableTrees.localTime (f : Skorokhod.DLoc) (t : NNReal) : ℝ

The local time at the minimum, L_t = -I_t.

Equations

• BGW.StableTrees.localTime f t = -BGW.StableTrees.runningInfLoc f t

theorem BGW.StableTrees.measurable_localTime_uncurry : Measurable fun (p : NNReal × Skorokhod.DLoc) => localTime p.2 p.1

L is jointly measurable in (t, f).

theorem BGW.StableTrees.stronglyAdapted_localTime : MeasureTheory.StronglyAdapted Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => localTime f t

L is adapted to the right-continuous filtration of DLoc.

theorem BGW.StableTrees.ae_localTime_spec {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), localTime f 0 = 0 ∧ Monotone (localTime f) ∧ Continuous (localTime f) ∧ Filter.Tendsto (localTime f) Filter.atTop Filter.atTop

Almost surely L_0 = 0 (from f 0 = 0), L is monotone, continuous, and unbounded.

noncomputable def BGW.StableTrees.localTimeStieltjes (f : Skorokhod.DLoc) : StieltjesFunction ℝ

The Stieltjes function s ↦ L_{s⁺} on ℝ (s⁺ = max s 0) when L is monotone and continuous; junk value the zero function otherwise (a null set of paths).

Equations

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

noncomputable def BGW.StableTrees.passageTimeMinus (x : NNReal) (f : Skorokhod.DLoc) : NNReal

The ℝ≥0-valued left limit T_{x-} = sup_{y<x} T_y of the passage process, with T_{0-} = 0; junk 0 where some T_y = ⊤ (null set).

Equations

• BGW.StableTrees.passageTimeMinus x f = WithTop.untopD 0 (⨆ (y : ↑(Set.Iio x)), BGW.StableTrees.firstPassageBelow (↑y) f)

noncomputable def BGW.StableTrees.localTimeNN (f : Skorokhod.DLoc) (t : NNReal) : NNReal

L_t as a level in ℝ≥0 (L_t ≥ 0 almost surely).

Equations

• BGW.StableTrees.localTimeNN f t = (BGW.StableTrees.localTime f t).toNNReal

theorem BGW.StableTrees.measurable_passageTimeMinus (x : NNReal) : Measurable (passageTimeMinus x)

passageTimeMinus x is measurable in the path.

theorem BGW.StableTrees.measurable_passageTimeMinus_uncurry : Measurable fun (p : NNReal × Skorokhod.DLoc) => passageTimeMinus p.1 p.2

Joint measurability of (x, f) ↦ T_{x-}(f).

theorem BGW.StableTrees.ae_firstHitBelow_eq_firstPassageBelow {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), firstHitBelow x f = firstPassageBelow x f

First hitting agrees with strict passage at each FIXED level (a.s., NOT simultaneously for all levels).

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

Straddling. Almost surely for all t: T_{L_t -} ≤ t ≤ T_{L_t}.

theorem BGW.StableTrees.ae_localTime_passageTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x : NNReal), localTime f (passageTime x f) = ↑x ∧ localTime f (passageTimeMinus x f) = ↑x

Generalized inverse identities. Almost surely for all x ≥ 0: L (T_x) = x and L (T_{x-}) = x.

Strong Markov at T_x and independent stationary increments

theorem BGW.StableTrees.ae_firstPassageBelow_add {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x y : NNReal), firstPassageBelow (x + y) f = firstPassageBelow x f + firstPassageBelow y (Skorokhod.DLoc.shiftAt (firstPassageBelow x) f)

Additivity from creeping (deterministic on the creeping event): a.s., for all x y ≥ 0, T_{x+y}(f) = T_x(f) + T_y(shiftAt T_x f).

theorem BGW.StableTrees.ae_reflected_shiftAt_passage {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x t : NNReal), ↑f (passageTime x f + t) - runningInfLoc f (passageTime x f + t) = ↑(Skorokhod.DLoc.shiftAt (firstPassageBelow x) f) t - runningInfLoc (Skorokhod.DLoc.shiftAt (firstPassageBelow x) f) t

Reflected process after T_x: on the creeping event, X_{T_x + t} - I_{T_x + t} = X'_t - I'_t for the centered shift X' = shiftAt T_x.

theorem BGW.StableTrees.measure_inter_passageIncrement {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x y : NNReal) {A : Set Skorokhod.DLoc} (hA : MeasurableSet A) {S : Set ℝ} (hS : MeasurableSet S) : ↑(stableLocalLaw θ) (A ∩ {f : Skorokhod.DLoc | ↑(passageTime (x + y) f) - ↑(passageTime x f) ∈ S}) = ↑(stableLocalLaw θ) A * (passageLaw θ y) S

Fresh increment: independence of F_{T_x} and law. For x, y ≥ 0, any event A of the stopped σ-algebra F_{T_x} and Borel S ⊆ ℝ: P(A ∩ {T_{x+y} - T_x ∈ S}) = P(A) · P(T_y ∈ S).

theorem BGW.StableTrees.map_passageIncrement {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x y : NNReal) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => ↑(passageTime (x + y) f) - ↑(passageTime x f)) ↑(stableLocalLaw θ) = passageLaw θ y

Stationary increments. T_{x+y} - T_x has the law of T_y.

One-dimensional law: Laplace transform, positivity, scaling

theorem BGW.StableTrees.integral_exp_neg_passageLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {q : ℝ} (hq : 0 ≤ q) : ∫ (t : ℝ), Real.exp (-q * t) ∂passageLaw θ x = Real.exp (-↑x * q ^ (1 / θ))

Laplace transform: ∫ e^{-q t} d passageLaw θ x = e^{-x q^{1/θ}} for x ≥ 0, q ≥ 0.

theorem BGW.StableTrees.passageLaw_Iic_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {x : NNReal} (hx : 0 < x) : (passageLaw θ x) (Set.Iic 0) = 0

For x > 0 the law of T_x lives on (0, ∞).

theorem BGW.StableTrees.passageLaw_scaling {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {c : NNReal} (hc : 0 < c) : passageLaw θ (c * x) = MeasureTheory.Measure.map (fun (t : ℝ) => ↑c ^ θ * t) (passageLaw θ x)

Scaling. T_{c x} =d c^θ T_x, for c > 0.

theorem BGW.StableTrees.eq_passageLaw_of_integral_exp_neg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {ρ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ρ] (h0 : ρ (Set.Iio 0) = 0) (hρ : ∀ (q : ℝ), 0 < q → ∫ (t : ℝ), Real.exp (-q * t) ∂ρ = Real.exp (-↑x * q ^ (1 / θ))) : ρ = passageLaw θ x

Identification of the law by its Laplace transform: any probability law on ℝ with the transform e^{-x q^{1/θ}} is passageLaw θ x (the positive (1/θ)-stable law).