Index-two stable processes and Donsker's theorem

At stability index two, the stable process law is the law of √2 times Brownian motion. The finite-dimensional increment characterization identifies the two laws. The stable-domain functional limit theorem then gives Donsker's theorem for critical offspring laws with finite variance and the normalization used throughout the project (P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Theorem 8.2; J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VIII).

theorem BGW.StableTrees.stableProcessLaw_two {T : ℝ} (hT : 0 < T) : stableProcessLaw 2 T = ContinuumTrees.BrownianD.wienerD (NNReal.sqrt 2) T

At θ = 2 the stable process law is the law of √2 · B.

theorem BGW.StableTrees.coe_stableProcessLaw_two {T : ℝ} (hT : 0 < T) : ↑(stableProcessLaw 2 T) = ↑(ContinuumTrees.BrownianD.wienerD (NNReal.sqrt 2) T)

Measure form of stableProcessLaw_two.

theorem BGW.StableTrees.ae_mem_range_ofContinuous_stableProcessLaw_two {T : ℝ} (hT : 0 < T) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑(stableProcessLaw 2 T), f ∈ Set.range Skorokhod.ofContinuous

The index-two stable law is carried by continuous paths.

theorem BGW.StableTrees.StableDomain.tendsto_stepPathLaw_wienerD {μ : PMF ℕ} {a : ℕ → ℝ} (h : StableDomain μ 2 a) {T : ℝ} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => stepPathLaw (realOffspringStepLaw μ) T a n) Filter.atTop (nhds (ContinuumTrees.BrownianD.wienerD (NNReal.sqrt 2) T))

Donsker form: a critical nondegenerate offspring law in the index-2 stable domain with normalizer a has FCLT limit wienerD (√2) T.

theorem BGW.StableTrees.tendsto_stepPathLaw_wienerD_of_finiteVariance {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) {T : ℝ} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => stepPathLaw (realOffspringStepLaw μ) T (fun (n : ℕ) => √(∫ (z : ℤ), ↑z ^ 2 ∂stepLaw μ) / √2 * √↑n) n) Filter.atTop (nhds (ContinuumTrees.BrownianD.wienerD (NNReal.sqrt 2) T))

Donsker's theorem for critical finite-variance offspring laws: with σ² = E[(ξ - 1)²], the step paths normalized by σ √n / √2 converge to wienerD (√2) T.