The Gaussian stable bridge #

At stability index θ = 2, the spectrally positive stable density is the centered Gaussian density of variance 2. Its transition densities and bridge prefix weights therefore agree with those of √2 times standard Brownian motion. Uniqueness of the bridge with prescribed prefix laws and pinned endpoints identifies the stable bridge with √2 times the Brownian bridge.

source

theorem BGW.StableTrees.BrownianIdentification.stableDensity_two (x : ℝ) :

Scalar.stableDensity 2 x = ProbabilityTheory.gaussianPDFReal 0 2 x

The θ = 2 stable density is the centered Gaussian density of variance 2.

source

theorem BGW.StableTrees.BrownianIdentification.stableDensityAt_two {t : ℝ} (ht : 0 < t) (x : ℝ) :

stableDensityAt 2 t x = ProbabilityTheory.gaussianPDFReal 0 (ContinuumTrees.BrownianD.variance (NNReal.sqrt 2) t) x

At time t > 0, the θ = 2 stable density is the density of √2 B_t.

source

theorem BGW.StableTrees.BrownianIdentification.bridgePrefixWeight_two {a : ℝ} (ha : 0 ≤ a) (ha1 : a < 1) (f : Skorokhod.D a ℝ) :

bridgePrefixWeight 2 a ha f = ContinuumTrees.BrownianD.prefixDensity (NNReal.sqrt 2) a (f ⟨a, ⋯⟩)

The θ = 2 bridge prefix weight is the Brownian bridge prefix density with c = √2.

source

theorem BGW.StableTrees.BrownianIdentification.stableBridgeLaw_two :

stableBridgeLaw 2 = ContinuumTrees.BrownianD.bridgeD (NNReal.sqrt 2)

K18a. The θ = 2 stable bridge is √2 times the standard Brownian bridge.