Convergence of finite-grid minimum times

The completed lower envelope has a positive gap away from its unique minimizer. A grid point near a continuous minimizer forces every grid minimum into that neighborhood.

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.

noncomputable def BGW.StableTrees.bridgeGridMinTime (M : ℕ) (f : Skorokhod.D 1 ℝ) : ↑(Set.Icc 0 1)

The minimum time of the finite grid, excluding the duplicate terminal endpoint.

Equations

• BGW.StableTrees.bridgeGridMinTime M f = BGW.StableTrees.gridTime M ↑(BGW.StableTrees.bridgeGridMinIndex M f)

theorem BGW.StableTrees.measurable_bridgeGridMinTime (M : ℕ) : Measurable fun (f : Skorokhod.D 1 ℝ) => ↑(bridgeGridMinTime M f)

The real finite-grid minimum time is measurable.

theorem BGW.StableTrees.tendsto_bridgeGridMinTime {f : Skorokhod.D 1 ℝ} (huniq : ∀ (t : ↑(Set.Icc 0 1)), min (Function.leftLim (⇑f) t) (f t) = ⨅ (s : ↑(Set.Icc 0 1)), f s → t = Skorokhod.vervaatTime f) (hcont : ContinuousAt (⇑f) (Skorokhod.vervaatTime f)) (hg1 : ↑(Skorokhod.vervaatTime f) < 1) : Filter.Tendsto (fun (M : ℕ) => bridgeGridMinTime M f) Filter.atTop (nhds (Skorokhod.vervaatTime f))

Finite-grid minimum times converge at a unique continuous interior minimum.

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

Under the stable bridge law, all finite-grid minimum times converge almost surely.