The projective stable bridge

The open law has the prescribed tilted prefixes and converges to zero at its terminal time almost surely. Closing gives a measurable compact path with pinned endpoints and the same strict-prefix laws.

References

• P. Fitzsimmons, J. Pitman and M. Yor, Markovian bridges: construction, Palm interpretation, and splicing, Seminar on Stochastic Processes 1992, Progr. Probab. 33, Birkhäuser, 1993, 101–134.
• 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.closeBridge_one (f : BridgeOpen) : (closeBridge f) ⟨1, ⋯⟩ = 0

Every closed path has terminal value zero.

theorem BGW.StableTrees.closeBridge_leftLim_one (f : BridgeOpen) : Function.leftLim ⇑(closeBridge f) ⟨1, ⋯⟩ = 0

Every closed path has terminal left limit zero.

theorem BGW.StableTrees.stableBridgeLaw_endpoints {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), f ⟨0, ⋯⟩ = 0 ∧ f ⟨1, ⋯⟩ = 0 ∧ Function.leftLim ⇑f ⟨1, ⋯⟩ = 0

Terminal pinning (and start): almost surely X_0 = 0, X_1 = 0 and X_{1-} = 0.

theorem BGW.StableTrees.map_restrict_stableBridgeLaw_horizon_of_terminal_limit {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hpin : ∀ᵐ (f : BridgeOpen) ∂↑(bridgeOpenLaw θ), Filter.Tendsto f.eval (nhdsWithin 1 (Set.Iio 1)) (nhds 0)) (n : ℕ) : MeasureTheory.Measure.map (Skorokhod.restrict ⋯) ↑(stableBridgeLaw θ) = bridgePrefixLaw θ (bridgeHorizon n) ⋯ ↑(stableProcessLaw θ (bridgeHorizon n))

Given terminal pinning of the open law, every closed dyadic prefix has its tilted law.

theorem BGW.StableTrees.map_restrict_stableBridgeLaw_of_terminal_limit {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) (hpin : ∀ᵐ (f : BridgeOpen) ∂↑(bridgeOpenLaw θ), Filter.Tendsto f.eval (nhdsWithin 1 (Set.Iio 1)) (nhds 0)) : MeasureTheory.Measure.map (Skorokhod.restrict ⋯) ↑(stableBridgeLaw θ) = bridgePrefixLaw θ a ⋯ ↑(stableProcessLaw θ a)

Given terminal pinning of the open law, every strict closed prefix has its tilted law.

theorem BGW.StableTrees.map_restrict_stableBridgeLaw {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) : MeasureTheory.Measure.map (Skorokhod.restrict ⋯) ↑(stableBridgeLaw θ) = bridgePrefixLaw θ a ⋯ ↑(stableProcessLaw θ a)

Prefix identity: for 0 < a < 1, the restriction to [0, a] is the tilted stable law w_a · P_a (bridgePrefixLaw, i.e. withDensity of bridgePrefixWeight).