The Brownian joint excursion law

At stability index two, the normalized excursion path and its height are almost surely the same function. Combining this diagonal support with the Brownian path marginal identifies their joint law with the law of a single scaled Vervaat excursion, viewed both as a càdlàg and as a continuous path.

theorem BGW.StableTrees.BrownianIdentification.measurable_sqrtTwoPair : Measurable fun (e : C(↑unitInterval, ℝ)) => (Skorokhod.ofContinuous (√2 • e), √2 • e)

Measurability guard: the pair map e ↦ (√2 e, √2 e), with the first coordinate seen as a càdlàg path, is measurable (so the image law in excLaw_two is not a junk pushforward).

theorem BGW.StableTrees.BrownianIdentification.excLaw_two : excLaw 2 = ContinuumTrees.VervaatBridge.law.map fun (e : C(↑unitInterval, ℝ)) => (Skorokhod.ofContinuous (√2 • e), √2 • e)

K18c. At θ = 2 the normalized excursion/height pair has the law of (√2 e, √2 e) for one Brownian excursion e (Vervaat transform of the Brownian bridge).

theorem BGW.StableTrees.BrownianIdentification.excLaw_two_map_snd : (excLaw 2).map Prod.snd = ContinuumTrees.VervaatBridge.law.map fun (e : C(↑unitInterval, ℝ)) => √2 • e

Height marginal at θ = 2 (C30(a)): the excursion height has the law of √2 e.

theorem BGW.StableTrees.BrownianIdentification.excLaw_two_map_diag : ((excLaw 2).map fun (p : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)) => (p.2, p.2)) = ContinuumTrees.VervaatBridge.law.map fun (e : C(↑unitInterval, ℝ)) => (√2 • e, √2 • e)

The C29 (K16) limit at θ = 2: the duplicated excursion height has the law of (√2 e, √2 e).