Brownian excursion normalization

At stability index two, the normalized Itô excursion is the Vervaat transform of a Brownian bridge scaled by √2. Positive scaling commutes with the continuous-loop Vervaat transform, so this law is √2 times the Brownian Vervaat path law.

theorem BGW.StableTrees.BrownianIdentification.vervaat_smul {c : ℝ} (hc : 0 < c) (g : { g : C(↑unitInterval, ℝ) // g 0 = g 1 }) : ContinuumTrees.Vervaat.vervaat ⟨c • ↑g, ⋯⟩ = c • ContinuumTrees.Vervaat.vervaat g

Positive scaling commutes with the continuous-loop Vervaat transform.

theorem BGW.StableTrees.BrownianIdentification.levyExcLaw_two : ↑(levyExcLaw 2) = MeasureTheory.Measure.map (fun (e : C(↑(Set.Icc 0 1), ℝ)) => Skorokhod.ofContinuous (√2 • e)) ↑ContinuumTrees.VervaatBridge.law

K18b. At θ = 2 the normalized Itô excursion is √2 times the Brownian excursion (Vervaat transform of the Brownian bridge).