Restart at inverse local time and the ascending ladder pair

Occupation additivity at a contact time identifies the restarted public clock. Strict inversion then identifies the ladder increments with the ladder of the independent future.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VI (ladder processes).
• A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapter 6.

theorem BGW.StableTrees.ae_supRestart_at_ladderTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), supLadderHeight θ z f = ↑f (supLadderTime θ z f) ∧ ∀ (t : NNReal), supReflected f (supLadderTime θ z f + t) = supReflected (Skorokhod.DLoc.shiftAt (fun (g : Skorokhod.DLoc) => ↑(supLadderTime θ z g)) f) t ∧ supRunning f (supLadderTime θ z f + t) = supLadderHeight θ z f + supRunning (Skorokhod.DLoc.shiftAt (fun (g : Skorokhod.DLoc) => ↑(supLadderTime θ z g)) f) t ∧ supLocalTime θ f (supLadderTime θ z f + t) = ↑z + supLocalTime θ (Skorokhod.DLoc.shiftAt (fun (g : Skorokhod.DLoc) => ↑(supLadderTime θ z g)) f) t

Restart identity at A_z. Let f' = shiftAt A_z f be the post-A_z centered path. Almost surely X_{A_z} = S_{A_z} = B_z (zero drawdown at A_z, not zero overshoot), the reflected process restarts, S_{A_z+t} = B_z + S'_t, and M(A_z + t) = z + M'(t) for all t, where S', M' are computed from f'.

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

The ladder pair (A_z, B_z) as a real vector.

Equations

• BGW.StableTrees.supLadderPair θ z f = (↑(BGW.StableTrees.supLadderTime θ z f), BGW.StableTrees.supLadderHeight θ z f)

noncomputable def BGW.StableTrees.supLadderIncrement (θ : ℝ) (y z : NNReal) (f : Skorokhod.DLoc) : ℝ × ℝ

The ladder increment (A_z - A_y, B_z - B_y) over levels y ≤ z.

Equations

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

theorem BGW.StableTrees.measurable_supLadderPair (θ : ℝ) (z : NNReal) : Measurable (supLadderPair θ z)

Measurability of the ladder pair at each level.

theorem BGW.StableTrees.measurable_supLadderIncrement (θ : ℝ) (y z : NNReal) : Measurable (supLadderIncrement θ y z)

Measurability of each ladder increment.

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

Start at the origin: (A_0, B_0) = (0, 0) almost surely.

theorem BGW.StableTrees.ae_supLadderPair_path {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (∀ (z : NNReal), 0 ≤ (supLadderPair θ z f).1 ∧ 0 ≤ (supLadderPair θ z f).2) ∧ (Monotone fun (z : NNReal) => (supLadderPair θ z f).1) ∧ (Monotone fun (z : NNReal) => (supLadderPair θ z f).2) ∧ ∀ (z : NNReal), ContinuousWithinAt (fun (z : NNReal) => supLadderPair θ z f) (Set.Ici z) z

Almost surely the ladder pair is nonnegative, nondecreasing in both coordinates, and right-continuous in the level, for all levels simultaneously.

theorem BGW.StableTrees.ae_supLadder_restart {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (z : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (u : NNReal), supLadderTime θ (z + u) f = supLadderTime θ z f + supLadderTime θ u (Skorokhod.DLoc.shiftAt (fun (g : Skorokhod.DLoc) => ↑(supLadderTime θ z g)) f) ∧ supLadderHeight θ (z + u) f = supLadderHeight θ z f + supLadderHeight θ u (Skorokhod.DLoc.shiftAt (fun (g : Skorokhod.DLoc) => ↑(supLadderTime θ z g)) f)

Ladder process restarts: with f' = shiftAt A_z f, for all u ≥ 0 simultaneously, A_{z+u}(f) = A_z(f) + A_u(f') and B_{z+u}(f) = B_z(f) + B_u(f').

theorem BGW.StableTrees.map_supLadderIncrement {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {y z : NNReal} (hyz : y ≤ z) : MeasureTheory.Measure.map (supLadderIncrement θ y z) ↑(stableLocalLaw θ) = MeasureTheory.Measure.map (supLadderPair θ (z - y)) ↑(stableLocalLaw θ)

Stationary increments: the increment over [y, z] has the law of the pair at level z - y.

theorem BGW.StableTrees.indep_supLadderIncrement_stopped {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {y z : NNReal} (hyz : y ≤ z) : ProbabilityTheory.Indep ⋯.measurableSpace (MeasurableSpace.comap (supLadderIncrement θ y z) inferInstance) ↑(stableLocalLaw θ)

Independence of the future increment from F_{A_y}: the increment over [y, z] is independent of the stopped σ-algebra of supHitting θ y.

theorem BGW.StableTrees.iIndepFun_supLadderIncrement {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (n : ℕ) (z : Fin (n + 1) → NNReal) (hz : Monotone z) : ProbabilityTheory.iIndepFun (fun (k : Fin n) => supLadderIncrement θ (z k.castSucc) (z k.succ)) ↑(stableLocalLaw θ)

Independent increments: along every finite monotone chain of levels z 0 ≤ z 1 ≤ ... ≤ z n, the n successive increments are mutually independent.