Unique minimum of the Brownian bridge

A countable collection of deterministic comparisons between interval minima rules out two distinct global minimizers almost surely. Since the global minimum is negative and the bridge vanishes at its endpoints, the unique minimizer is interior. Rotating at that minimizer in the Vervaat construction consequently gives a path strictly positive on the open unit interval.

The probabilistic input is BrownianBridge.measure_prefixMin_eq_intervalMin (Kim–Pollard regression), applied to rational interval endpoints, together with BrownianBridge.ae_intervalMin_neg; see Vervaat (1979) and Le Gall, Random trees and applications (2005), §2, for the classical statement.

theorem BGW.ContinuumTrees.BrownianBridge.ae_existsUnique_isMin : ∀ᵐ (f : C(↑unitInterval, ℝ)) ∂↑law, ∃! t : ↑unitInterval, ∀ (s : ↑unitInterval), f t ≤ f s

Almost surely, the Brownian bridge attains its global minimum at exactly one time.

theorem BGW.ContinuumTrees.BrownianBridge.ae_firstMinimum_mem_Ioo : ∀ᵐ (f : C(↑unitInterval, ℝ)) ∂↑law, 0 < ↑(Vervaat.firstMinimum f) ∧ ↑(Vervaat.firstMinimum f) < 1

Almost surely, the first (hence unique) minimum time lies in the open interval (0,1).

theorem BGW.ContinuumTrees.VervaatBridge.ae_path_pos : ∀ᵐ (ω : NNReal → ℝ) ∂ProbabilityTheory.gaussianLimit, ∀ (t : ↑unitInterval), 0 < ↑t → ↑t < 1 → 0 < (path ω) t

Almost surely, the Vervaat transform of the anchored bridge is strictly positive on (0,1).

theorem BGW.ContinuumTrees.VervaatBridge.ae_law_pos : ∀ᵐ (f : C(↑unitInterval, ℝ)) ∂↑law, ∀ (t : ↑unitInterval), 0 < ↑t → ↑t < 1 → 0 < f t

The Vervaat path law is carried by paths strictly positive on (0,1).