Kemperman's identity for forests

For an offspring probability measure μ, ℓ ≥ 1 and every n, the total weight forestWeight (fun d => μ {d}) ℓ n of the ordered forests of ℓ trees with n vertices satisfies

n * forestWeight μ ℓ n = ℓ * Measure.pi (fun _ : Fin n => μ) {ω | ∑ i, ω i + ℓ = n},

that is n P(|𝒢_ℓ| = n) = ℓ P(S_n = -ℓ) for ℓ independent trees and the Łukasiewicz walk of independent offspring counts (natCast_mul_forestWeight_eq_pi). No criticality, aperiodicity or positivity is assumed; both sides vanish when n < ℓ, and ℓ = 1 is the identity for trees (forestWeight_one_eq_bienaymeLaw_sizeEvent, countForestBridges_one). The multiplied form is kept: no division and no conditioning event is involved. Adapted from PoissonDeclumping/Bridge/Kemperman.lean; the first-passage convolution, the conditional bridge law and local limits are not part of this module.

def BGW.countForestBridges (ℓ n : ℕ) : Set (Fin n → ℕ)

Offspring-count vectors whose walk ∑ (ω i - 1) ends at -ℓ.

Equations

• BGW.countForestBridges ℓ n = {ω : Fin n → ℕ | ∑ i : Fin n, ω i + ℓ = n}

theorem BGW.countForestBridges_one (n : ℕ) : countForestBridges 1 n = countBridges n

theorem BGW.countForestBridges_eq_empty_of_lt {ℓ n : ℕ} (h : n < ℓ) : countForestBridges ℓ n = ∅

theorem BGW.stepWord_mem_forestBridgeWords_iff {ℓ n : ℕ} (ω : Fin n → ℕ) : stepWord ω ∈ forestBridgeWords ℓ n ↔ ω ∈ countForestBridges ℓ n

theorem BGW.tsum_forestBridgeWords_walkWeight (p : ℕ → ENNReal) (ℓ n : ℕ) : ∑' (x : List ℤ), (forestBridgeWords ℓ n).indicator (walkWeight p) x = ∑' (ω : Fin n → ℕ), (countForestBridges ℓ n).indicator (fun (ω : Fin n → ℕ) => ∏ i : Fin n, p (ω i)) ω

Reindexing the forest bridge words by offspring-count vectors.

theorem BGW.pi_eq_tsum_indicator (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (A : Set (Fin n → ℕ)) : (MeasureTheory.Measure.pi fun (x : Fin n) => μ) A = ∑' (ω : Fin n → ℕ), A.indicator (fun (ω : Fin n → ℕ) => ∏ i : Fin n, μ {ω i}) ω

The mass of any set of count vectors under the product measure is the sum of its point masses.

theorem BGW.natCast_mul_forestWeight_eq_pi (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (n : ℕ) : ↑n * forestWeight (fun (d : ℕ) => μ {d}) ℓ n = ↑ℓ * (MeasureTheory.Measure.pi fun (x : Fin n) => μ) (countForestBridges ℓ n)

Kemperman's identity for forests: n P(|𝒢_ℓ| = n) = ℓ P(S_n = -ℓ), for every offspring probability measure, every 1 ≤ ℓ and every n.

theorem BGW.forestWeight_one (p : ℕ → ENNReal) (n : ℕ) : forestWeight p 1 n = ∑' (t : PlaneTree), if t.size = n then PlaneTree.weight p t else 0

A forest of one tree is a tree.

theorem BGW.LocallyFinite.forestWeight_one_eq_bienaymeLaw_sizeEvent (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : forestWeight (fun (d : ℕ) => μ {d}) 1 n = (bienaymeLaw μ) (sizeEvent n)