Whole-path restart law at inverse local time #
The everywhere stopping representative of inverse local time is finite almost surely. Strong Markov therefore gives the original law and independence of the entire shifted path.
Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VI.
theorem
BGW.StableTrees.ae_shiftAt_supHitting_eq
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(z : NNReal)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Skorokhod.DLoc.shiftAt (supHitting θ z) f = Skorokhod.DLoc.shiftAt (fun (g : Skorokhod.DLoc) => ↑(supLadderTime θ z g)) f
The stopping representative and raw ladder time give the same centered shift almost surely.
theorem
BGW.StableTrees.ae_supHitting_lt_top
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(z : NNReal)
:
∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), supHitting θ z f < ⊤
A_z < ⊤ almost surely (for the stopping representative), so restart is a.s. defined.
theorem
BGW.StableTrees.measure_inter_preimage_shiftAt_supHitting
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(z : NNReal)
{A : Set Skorokhod.DLoc}
(hA : MeasurableSet A)
(hAτ : A ⊆ {f : Skorokhod.DLoc | supHitting θ z f < ⊤})
{B : Set Skorokhod.DLoc}
(hB : MeasurableSet B)
:
↑(stableLocalLaw θ) (A ∩ Skorokhod.DLoc.shiftAt (supHitting θ z) ⁻¹' B) = ↑(stableLocalLaw θ) A * ↑(stableLocalLaw θ) B
Independence of stopped events from measurable events of the restarted whole path.
theorem
BGW.StableTrees.map_shiftAt_supHitting
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(z : NNReal)
:
MeasureTheory.Measure.map (Skorokhod.DLoc.shiftAt (supHitting θ z)) ↑(stableLocalLaw θ) = ↑(stableLocalLaw θ)
The post-inverse-local-time whole path has the original stable law.