Terminal pinning of the projective bridge

Centered prefix reversal bounds late excursions by an initial excursion and an endpoint tail. The one-dimensional endpoint density identifies that tail with a small-time tail. Continuity from above then gives the full path limit at one.

theorem BGW.StableTrees.bridgeOpen_ae_terminal_limit {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (P : (a : ℝ) → MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)) (hP : ∀ (a : ℝ), 0 < a → a < 1 → IsStableLevyLaw θ a (P a)) (Q : MeasureTheory.ProbabilityMeasure BridgeOpen) (hQ : ∀ (n : ℕ), MeasureTheory.Measure.map (Skorokhod.CompatiblePaths.coord n) ↑Q = bridgePrefixLaw θ (bridgeHorizon n) ⋯ ↑(P (bridgeHorizon n))) : ∀ᵐ (f : BridgeOpen) ∂↑Q, Filter.Tendsto f.eval (nhdsWithin 1 (Set.Iio 1)) (nhds 0)

Terminal pinning, abstract form. Any law on the open carrier with the tilted prefix marginals has full path limit 0 at the terminal time, almost surely.

theorem BGW.StableTrees.bridgeOpenLaw_ae_terminal_limit {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : BridgeOpen) ∂↑(bridgeOpenLaw θ), Filter.Tendsto f.eval (nhdsWithin 1 (Set.Iio 1)) (nhds 0)

Terminal pinning for the stable bridge: the open stable bridge converges to 0 at time 1 almost surely.