The Łukasiewicz walk of offspring counts and the Kemperman identity for trees

Let ω : Fin n → ℕ be independent offspring counts with law μ, and let S_n = ∑ (ω i - 1) (subtraction in ℤ) be the Łukasiewicz walk. The event S_n = -1 is ∑ ω i + 1 = n. Bridge words of length n are exactly the step words (ω i - 1) of such vectors, and the walk weight of the step word is ∏ μ {ω i}, the mass of the point ω under Measure.pi (fun _ => μ). Together with the weighted cycle lemma this gives, for every offspring probability measure μ and every n,

n * P(|T| = n) = P(S_n = -1)

(natCast_mul_bienaymeLaw_sizeEvent_eq_pi), with no criticality, aperiodicity or positivity assumption; both sides vanish for n = 0. The walk is the product measure on counts, not a measure on ℤ, and only its endpoint at time n is considered. The forest version, the uniform cyclic-shift representation and the conditional bridge law are not part of this module. Adapted from PoissonDeclumping/Lukasiewicz/BridgeLaw.lean and Cyclic/WalkBridge.lean.

def BGW.countBridges (n : ℕ) : Set (Fin n → ℕ)

The offspring-count vectors whose Łukasiewicz walk ∑ (ω i - 1) ends at -1.

Equations

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

def BGW.stepWord {n : ℕ} (ω : Fin n → ℕ) : List ℤ

The step word (ω i - 1) of a vector of offspring counts, subtracting in ℤ.

Equations

• BGW.stepWord ω = List.ofFn fun (i : Fin n) => ↑(ω i) - 1

theorem BGW.stepWord_injective {n : ℕ} : Function.Injective stepWord

theorem BGW.stepWord_mem_bridgeWords_iff {n : ℕ} (ω : Fin n → ℕ) : stepWord ω ∈ bridgeWords n ↔ ω ∈ countBridges n

theorem BGW.walkWeight_stepWord (p : ℕ → ENNReal) {n : ℕ} (ω : Fin n → ℕ) : walkWeight p (stepWord ω) = ∏ i : Fin n, p (ω i)

theorem BGW.exists_stepWord_eq_of_entries {x : List ℤ} {n : ℕ} (hlen : x.length = n) (hge : ∀ a ∈ x, -1 ≤ a) : ∃ (ω : Fin n → ℕ), stepWord ω = x

Every word of length n with entries at least -1 is a step word.

theorem BGW.exists_stepWord_eq {x : List ℤ} {n : ℕ} (hx : x ∈ bridgeWords n) : ∃ (ω : Fin n → ℕ), stepWord ω = x

theorem BGW.tsum_bridgeWords_walkWeight (p : ℕ → ENNReal) (n : ℕ) : ∑' (x : List ℤ), (bridgeWords n).indicator (walkWeight p) x = ∑' (ω : Fin n → ℕ), (countBridges n).indicator (fun (ω : Fin n → ℕ) => ∏ i : Fin n, p (ω i)) ω

Reindexing the bridge words by offspring-count vectors.

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

The mass of countBridges n under the product measure is the sum of its point masses.

theorem BGW.LocallyFinite.natCast_mul_bienaymeLaw_sizeEvent_eq_pi (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : ↑n * (bienaymeLaw μ) (sizeEvent n) = (MeasureTheory.Measure.pi fun (x : Fin n) => μ) (countBridges n)

Kemperman's identity for trees: n * P(|T| = n) = P(S_n = -1).