Finite-variance contours and Brownian tree scaling

The stable norming gives the joint limit (√2 e, √2 e). Rescaling gives Aldous's height and contour normalization in both contour clocks. Spatial scaling of the coded Brownian tree preserves its root and probability mass.

Deterministic norming identities

theorem BGW.StableTrees.ExactContour.treeContourPath_const_mul (c : ℝ) (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (τ : LocallyFinite.Tree) : treeContourPath (fun (m : ℕ) => c * B m) n T τ = c • treeContourPath B n T τ

The contour path is linear in the norming sequence.

theorem BGW.StableTrees.ExactContour.heightContourPath_const_mul (c : ℝ) (B : ℕ → ℝ) (n : ℕ) (τ : LocallyFinite.Tree) : heightContourPath (fun (m : ℕ) => c * B m) n τ = c • heightContourPath B n τ

The height/contour pair is linear in the norming sequence.

theorem BGW.StableTrees.ExactContour.finiteVarianceNorming_eq (σ : ℝ) : (fun (n : ℕ) => σ / 2 * √↑n) = fun (n : ℕ) => 1 / √2 * (σ / √2 * √↑n)

The Aldous norming (σ/2)√n is 1/√2 times the stable norming (σ/√2)√n of Scalar.stableDomain_of_finiteVariance.

theorem BGW.StableTrees.ExactContour.finiteVarianceNorming_div (σ : ℝ) {z : ℕ} (hz : 0 < z) : σ / 2 * √↑z / ↑z = σ / (2 * √↑z)

Coefficient identity for every positive size z (deterministic, so usable with a random size): the Aldous amplitude is σ / (2√z).

theorem BGW.StableTrees.ExactContour.treeContourPath_finiteVariance_paper (σ : ℝ) (t : PlaneTree) (s : ↑unitInterval) : (treeContourPath (fun (n : ℕ) => σ / 2 * √↑n) t.size 1 t.toLocallyFinite) s = σ / (2 * √↑t.size) * t.paperContourFunction s

For one finite tree of any size z = t.size, the Aldous-normed contour path is σ / (2√z) times the sealed paper contour PlaneTree.paperContourFunction (s ↦ C_{2z s}).

C30: finite-variance exact-size contours

theorem BGW.StableTrees.ExactContour.tendsto_exactHeightContour_finiteVariance_stable {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : have σ := √(∫ (z : ℤ), ↑z ^ 2 ∂stepLaw μ); Filter.Tendsto (fun (k : ℕ) => exactHeightContourLaw μ (fun (n : ℕ) => σ / √2 * √↑n) (q k) ⋯) Filter.atTop (nhds (ContinuumTrees.VervaatBridge.law.map fun (e : C(↑unitInterval, ℝ)) => (√2 • e, √2 • e)))

C30, stable normalization B₀ n = σ √(n/2): the exact-size height and contour converge jointly to (√2 e, √2 e).

theorem BGW.StableTrees.ExactContour.tendsto_exactHeightContour_finiteVariance {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : have σ := √(∫ (z : ℤ), ↑z ^ 2 ∂stepLaw μ); Filter.Tendsto (fun (k : ℕ) => exactHeightContourLaw μ (fun (n : ℕ) => σ / 2 * √↑n) (q k) ⋯) Filter.atTop (nhds (ContinuumTrees.VervaatBridge.law.map fun (e : C(↑unitInterval, ℝ)) => (e, e)))

C30, Aldous normalization, joint form: with amplitude σ / (2√n), the exact-size height (time nt) and contour (time 2nt) converge jointly to (e, e).

theorem BGW.StableTrees.ExactContour.tendsto_exactContour_finiteVariance {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : have σ := √(∫ (z : ℤ), ↑z ^ 2 ∂stepLaw μ); Filter.Tendsto (fun (k : ℕ) => (DiscreteForest.exactTreeLaw μ (q k)).map (treeContourPath (fun (n : ℕ) => σ / 2 * √↑n) (q k) 1)) Filter.atTop (nhds ContinuumTrees.VervaatBridge.law)

C30 (Aldous's theorem along admissible sizes): (σ / (2√n)) C_{2nt} ⇒ e, the normalized Brownian excursion.

theorem BGW.StableTrees.ExactContour.tendsto_exactHeightLibContour_finiteVariance {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hfinite : MeasureTheory.MemLp (fun (j : ℕ) => ↑j) 2 μ.toMeasure) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : have σ := √(∫ (z : ℤ), ↑z ^ 2 ∂stepLaw μ); Filter.Tendsto (fun (k : ℕ) => exactHeightLibContourLaw μ (fun (n : ℕ) => σ / 2 * √↑n) (q k) ⋯) Filter.atTop (nhds (ContinuumTrees.VervaatBridge.law.map fun (e : C(↑unitInterval, ℝ)) => (e, e)))

C30 in the library contour clock (s ↦ C(2(z-1)s)): the same joint limit (e, e).

Deterministic CRT scaling and the θ = 2 tree law

theorem BGW.StableTrees.BrownianIdentification.rootedMeasuredGHSpace_sqrt_two_smul (hpos : 0 < 1 / √2) (e : C(↑unitInterval, ℝ)) : ContinuumTrees.Coding.rootedMeasuredGHSpace (√2 • e) = MetricMeasure.RootedMeasuredGHSpace.scale (1 / √2) hpos (ContinuumTrees.Coding.rootedMeasuredGHSpace (2 • e))

Deterministic CRT scaling T_{√2 e} = (1/√2) T_{2e}: spatial scaling by 1/√2, with unchanged root and probability mass.

theorem BGW.StableTrees.BrownianIdentification.stableTreeLaw_two (hpos : 0 < 1 / √2) : ((excLaw 2).map fun (p : Skorokhod.D 1 ℝ × C(↑(Set.Icc 0 1), ℝ)) => ContinuumTrees.Coding.rootedMeasuredGHSpace p.2) = ContinuumTrees.VervaatBridge.treeLaw.map (MetricMeasure.RootedMeasuredGHSpace.scale (1 / √2) hpos)

The θ = 2 height-coded tree law: the tree coded by the excursion height H^exc has the law of Aldous's CRT T_{2e} with distances multiplied by 1/√2.