The uniform minimum time of the stable bridge

The proof uses cyclically exchangeable finite grids and convergence of their minimum times.

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_vervaatTime_le {θ x : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hx : x ∈ Set.Icc 0 1) : ↑(stableBridgeLaw θ) {f : Skorokhod.D 1 ℝ | ↑(Skorokhod.vervaatTime f) ≤ x} = ENNReal.ofReal x

Distribution-function form.

theorem BGW.StableTrees.map_vervaatTime_stableBridgeLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.Measure.map (fun (f : Skorokhod.D 1 ℝ) => ↑(Skorokhod.vervaatTime f)) ↑(stableBridgeLaw θ) = MeasureTheory.volume.restrict (Set.Icc 0 1)

The minimum time of the stable bridge is uniform on [0,1].