Distribution functions of finite-grid minimum times

Uniform finite minimum indices give a grid distribution function converging to the identity. Almost sure convergence and atomlessness identify the limiting distribution function.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VIII (Vervaat's transformation and the uniform law of the minimum time); L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

theorem BGW.StableTrees.stableBridgeLaw_bridgeGridMinTime_le {θ x : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hx : 0 ≤ x) (hx1 : x < 1) (M : ℕ) : ↑(stableBridgeLaw θ) {f : Skorokhod.D 1 ℝ | ↑(bridgeGridMinTime M f) ≤ x} = ENNReal.ofReal ((↑⌊(↑M + 1) * x⌋₊ + 1) / (↑M + 1))

Exact distribution function of a finite-grid minimum time below one.

theorem BGW.StableTrees.tendsto_stableBridgeLaw_bridgeGridMinTime_le {θ x : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hx : 0 ≤ x) (hx1 : x < 1) : Filter.Tendsto (fun (M : ℕ) => ↑(stableBridgeLaw θ) {f : Skorokhod.D 1 ℝ | ↑(bridgeGridMinTime M f) ≤ x}) Filter.atTop (nhds (ENNReal.ofReal x))

The finite-grid distribution functions tend to the uniform distribution function.

theorem BGW.StableTrees.tendsto_bridgeGridMinTime_event {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : ℝ) : Filter.Tendsto (fun (M : ℕ) => ↑(stableBridgeLaw θ) {f : Skorokhod.D 1 ℝ | ↑(bridgeGridMinTime M f) ≤ x}) Filter.atTop (nhds (↑(stableBridgeLaw θ) {f : Skorokhod.D 1 ℝ | ↑(Skorokhod.vervaatTime f) ≤ x}))

Almost sure convergence and absence of atoms give convergence of the grid event masses.