Inversion of the public supremum clock

The real clock discards infinite extended values. Its strict inverse therefore requires a boundary test at the common hitting and blow-up time, even though blow-up is almost surely absent.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

noncomputable def BGW.StableTrees.supLocalTimeInverse (θ : ℝ) (f : Skorokhod.DLoc) (z : NNReal) : WithTop NNReal

Inverse local time A_z = inf{t | M_t > z}.

Equations

• BGW.StableTrees.supLocalTimeInverse θ f z = sInf {t : WithTop NNReal | ∃ (u : NNReal), t = ↑u ∧ ↑z < BGW.StableTrees.supLocalTime θ f u}

noncomputable def BGW.StableTrees.supLadderTime (θ : ℝ) (z : NNReal) (f : Skorokhod.DLoc) : NNReal

Ladder time A_z (finite reading, junk 0 on ⊤).

Equations

• BGW.StableTrees.supLadderTime θ z f = WithTop.untopD 0 (BGW.StableTrees.supLocalTimeInverse θ f z)

noncomputable def BGW.StableTrees.supLadderHeight (θ : ℝ) (z : NNReal) (f : Skorokhod.DLoc) : ℝ

Ladder height B_z = S_{A_z}.

Equations

• BGW.StableTrees.supLadderHeight θ z f = BGW.StableTrees.supRunning f (BGW.StableTrees.supLadderTime θ z f)

noncomputable def BGW.StableTrees.supInverseRep (θ : ℝ) (z : NNReal) (f : Skorokhod.DLoc) : ENNReal

The explicit measurable representative of the public inverse: a if a < b, or if a = b < ⊤ and z < p(a) < ⊤ (isolated finite crossing at blow-up); ⊤ otherwise.

Equations

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

theorem BGW.StableTrees.supLocalTimeInverse_eq_rep (θ : ℝ) (f : Skorokhod.DLoc) (z : NNReal) : supLocalTimeInverse θ f z = supInverseRep θ z f

The raw inverse equals its explicit representative on every path, including blow-up paths.

theorem BGW.StableTrees.measurable_supInverseRep_uncurry (θ : ℝ) : Measurable fun (p : NNReal × Skorokhod.DLoc) => supInverseRep θ p.1 p.2

The explicit inverse representative is jointly measurable.

theorem BGW.StableTrees.measurable_supLocalTimeInverse_uncurry (θ : ℝ) : Measurable fun (p : NNReal × Skorokhod.DLoc) => supLocalTimeInverse θ p.2 p.1

Joint measurability of the raw public inverse in its extended reading.

theorem BGW.StableTrees.measurable_supLadder_uncurry (θ : ℝ) : (Measurable fun (p : NNReal × Skorokhod.DLoc) => supLadderTime θ p.1 p.2) ∧ Measurable fun (p : NNReal × Skorokhod.DLoc) => supLadderHeight θ p.1 p.2

Everywhere joint measurability of both public ladder processes.

theorem BGW.StableTrees.supHitting_eq_inverse_of_finite (θ : ℝ) (f : Skorokhod.DLoc) (z : NNReal) (hfin : ∀ (t : NNReal), supLocalTimeENN θ f t ≠ ⊤) : supHitting θ z f = supLocalTimeInverse θ f z

For an everywhere finite extended clock, its strict hitting time equals the raw inverse.

theorem BGW.StableTrees.ae_supHitting_eq_inverse {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), supHitting θ z f = supLocalTimeInverse θ f z

The stopping representative agrees almost surely with the public inverse at each level.

theorem BGW.StableTrees.exists_isStoppingTime_supLocalTimeInverse {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : ∃ (τ : Skorokhod.DLoc → ENNReal), MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration τ ∧ ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), τ f = supLocalTimeInverse θ f z

The inverse admits an almost surely equal stopping-time representative.