The closed stable bridge

This module characterizes the closed stable bridge by its strict prefix laws and terminal pinning, proves invariance under time reversal, and establishes absence of discontinuities at fixed times (P. Fitzsimmons, J. Pitman and M. Yor, Markovian bridges: construction, Palm interpretation, and splicing, Seminar on Stochastic Processes 1992, Birkhäuser, 1993; L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403).

Bounded-prefix expectation formulas

theorem BGW.StableTrees.integral_restrict_stableBridgeLaw {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) {F : Skorokhod.D a ℝ → ℝ} (hF : Measurable F) (hFb : ∃ (C : ℝ), ∀ (x : Skorokhod.D a ℝ), |F x| ≤ C) : ∫ (f : Skorokhod.D 1 ℝ), F (Skorokhod.restrict ⋯ f) ∂↑(stableBridgeLaw θ) = ∫ (g : Skorokhod.D a ℝ), bridgePrefixWeight θ a ⋯ g * F g ∂↑(stableProcessLaw θ a)

Prefix expectation. For 0 < a < 1 and bounded Borel F on D a ℝ: E_bridge[F(f|[0,a])] = E_{P_a}[w_a · F]. The integrand on the right lives on D a ℝ (it is not another restriction from D 1 ℝ).

theorem BGW.StableTrees.measure_restrict_preimage_stableBridgeLaw {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) {B : Set (Skorokhod.D a ℝ)} (hB : MeasurableSet B) : ↑(stableBridgeLaw θ) (Skorokhod.restrict ⋯ ⁻¹' B) = ∫⁻ (g : Skorokhod.D a ℝ) in B, ENNReal.ofReal (bridgePrefixWeight θ a ⋯ g) ∂↑(stableProcessLaw θ a)

Prefix probabilities: for measurable B ⊆ D a ℝ, P_bridge(f|[0,a] ∈ B) = ∫_B w_a dP_a.

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

Strict prefixes of the bridge are absolutely continuous with respect to the stable law.

theorem BGW.StableTrees.integral_bridgePrefixWeight_stableProcessLaw {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) : ∫ (g : Skorokhod.D a ℝ), bridgePrefixWeight θ a ⋯ g ∂↑(stableProcessLaw θ a) = 1

The prefix weight integrates to one against P_a (mass one of the tilted prefix law).

theorem BGW.StableTrees.stableBridgeLaw_unique {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {Q : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)} (hprefix : ∀ (a : ℝ) (ha : 0 < a) (ha1 : a < 1), MeasureTheory.Measure.map (Skorokhod.restrict ⋯) ↑Q = bridgePrefixLaw θ a ⋯ ↑(stableProcessLaw θ a)) (hend : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑Q, f ⟨1, ⋯⟩ = Function.leftLim ⇑f ⟨1, ⋯⟩) : Q = stableBridgeLaw θ

Uniqueness, minimal endpoint form. A law on D 1 ℝ with the prescribed prefix laws on every [0, a], a < 1, and which a.s. has no jump at time 1 (f 1 = f 1-), is the stable bridge. (The prefix laws force f 1- = 0 a.s.)

theorem BGW.StableTrees.stableBridgeLaw_unique_of_endpoints {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {Q : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)} (hprefix : ∀ (a : ℝ) (ha : 0 < a) (ha1 : a < 1), MeasureTheory.Measure.map (Skorokhod.restrict ⋯) ↑Q = bridgePrefixLaw θ a ⋯ ↑(stableProcessLaw θ a)) (hend : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑Q, f ⟨1, ⋯⟩ = 0 ∧ Function.leftLim ⇑f ⟨1, ⋯⟩ = 0) : Q = stableBridgeLaw θ

Uniqueness, pinned form (the endpoint conditions of stableBridgeLaw_endpoints): prefix laws plus f 1 = 0 ∧ f 1- = 0 almost surely.

theorem BGW.StableTrees.eq_stableBridgeLaw_iff {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {Q : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)} : Q = stableBridgeLaw θ ↔ (∀ (a : ℝ) (ha : 0 < a) (ha1 : a < 1), MeasureTheory.Measure.map (Skorokhod.restrict ⋯) ↑Q = bridgePrefixLaw θ a ⋯ ↑(stableProcessLaw θ a)) ∧ ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑Q, f ⟨1, ⋯⟩ = 0 ∧ Function.leftLim ⇑f ⟨1, ⋯⟩ = 0

Characterization. Q is the stable bridge law iff it has the tilted prefix laws and is a.s. pinned at time 1.

theorem BGW.StableTrees.exists_ne_stableBridgeLaw_same_prefixes {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (Q : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)), Q ≠ stableBridgeLaw θ ∧ ∀ (a : ℝ) (ha : 0 < a) (ha1 : a < 1), MeasureTheory.Measure.map (Skorokhod.restrict ⋯) ↑Q = bridgePrefixLaw θ a ⋯ ↑(stableProcessLaw θ a)

Prefix laws alone do not determine the law: the value at time 1 is free. This is the necessity of the endpoint hypothesis (a concrete second law with the same prefixes: the bridge with its terminal value overwritten by 1).

theorem BGW.StableTrees.stableBridgeLaw_ae_continuousAt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : ↑(Set.Icc 0 1)) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), ContinuousAt (⇑f) t

No fixed discontinuities. At every fixed time t ∈ [0, 1] (including 0 and 1) the bridge is almost surely continuous.

theorem BGW.StableTrees.stableBridgeLaw_ae_leftLim_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : ↑(Set.Icc 0 1)) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), Function.leftLim (⇑f) t = f t

Fixed-time left limit equals the value, almost surely (equivalent form, quantified over all fixed times at once is not claimed).

theorem BGW.StableTrees.map_reverseBridge_stableBridgeLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.Measure.map Skorokhod.reverseBridge ↑(stableBridgeLaw θ) = ↑(stableBridgeLaw θ)

Reversal invariance. (stableBridgeLaw θ).map reverseBridge = stableBridgeLaw θ.

theorem BGW.StableTrees.ae_reverseBridge_eq_reverseIncrements {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), Skorokhod.reverseBridge f = Skorokhod.reverseIncrements ⋯ f

Almost surely the reversed path is the increment reversal of the original (the reversal of the bridge is the reversal of increments on {f 1 = 0}).

theorem BGW.StableTrees.ae_reverseBridge_reverseBridge {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(stableBridgeLaw θ), Skorokhod.reverseBridge (Skorokhod.reverseBridge f) = f

Almost surely the reversal is an involution on the bridge (the totalized map is NOT an involution on arbitrary paths with endpoint jumps, so this is stated a.s. only).

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

The reversed bridge is again a pinned bridge: almost surely it starts and ends at 0 and has no left jump at 1.