Separation of Brownian bridge minima

The minimum on a prefix and the minimum on a later closed interval ending strictly before one are almost surely different. Regression on the increment between the intervals leaves an independent continuous residual path. For each residual, equality of the two minima holds for at most one value of the nondegenerate Gaussian increment.

This is the one-dimensional Gaussian regression argument of Kim and Pollard, Cube Root Asymptotics (1990), Lemma 2.6, pp. 197–198, specialized to the explicit Brownian bridge covariance. No excursion-law identification is used.

theorem BGW.ContinuumTrees.BrownianBridge.measure_prefixMin_eq_intervalMin (b c d : ↑unitInterval) (hbc : b < c) (hcd : c ≤ d) (hd : d < 1) : ↑law {f : C(↑unitInterval, ℝ) | Coding.intervalMin f 0 b = Coding.intervalMin f c d} = 0

Minima on [0,b] and [c,d] are almost surely unequal when b < c ≤ d < 1. The second interval ends strictly before one, so its regression profile is strictly positive.