The first-passage convolution for forests

For an offspring probability measure μ, 1 ≤ ℓ and every N, decomposing the walk of independent offspring counts at its first passage time q to -ℓ,

P(S_N = -ℓ) = ∑_{q ≤ N} P(|𝒢_ℓ| = q) P(S_{N-q} = 0)

(pi_countForestBridges_eq_sum), where P(S_n = -ℓ) is the mass of countForestBridges ℓ n under Measure.pi (fun _ : Fin n => μ) and P(|𝒢_ℓ| = q) is forestWeight (fun d => μ {d}) ℓ q. The identity is unconditional: no criticality, positivity or lattice hypothesis, and it holds for N < ℓ as well, where both sides vanish. For ℓ = 1 the factor P(|𝒢_1| = q) is the mass of sizeEvent q under the Bienaymé–Galton–Watson law (pi_countBridges_eq_sum). It is obtained from the word-level decomposition tsum_forestBridgeWords_eq_sum by the reindexing of ForestWalkLaw. The uniform cyclic-shift representation and the conditional bridge law are not part of this module. Adapted from PoissonDeclumping/Bridge/Kemperman.lean (walkMass_neg_eq_sum).

theorem BGW.pi_countForestBridges_eq_sum (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (N : ℕ) : (MeasureTheory.Measure.pi fun (x : Fin N) => μ) (countForestBridges ℓ N) = ∑ q ∈ Finset.range (N + 1), forestWeight (fun (d : ℕ) => μ {d}) ℓ q * (MeasureTheory.Measure.pi fun (x : Fin (N - q)) => μ) (countForestBridges 0 (N - q))

First-passage convolution for forests: P(S_N = -ℓ) = ∑_{q ≤ N} P(|𝒢_ℓ| = q) P(S_{N-q} = 0), for every offspring probability measure, 1 ≤ ℓ and every N.

theorem BGW.countForestBridges_zero (n : ℕ) : countForestBridges 0 n = {ω : Fin n → ℕ | ∑ i : Fin n, ω i = n}

The walk ends at 0 exactly when the counts sum to n.

theorem BGW.pi_countBridges_eq_sum (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsProbabilityMeasure μ] (N : ℕ) : (MeasureTheory.Measure.pi fun (x : Fin N) => μ) (countBridges N) = ∑ q ∈ Finset.range (N + 1), (LocallyFinite.bienaymeLaw μ) (LocallyFinite.sizeEvent q) * (MeasureTheory.Measure.pi fun (x : Fin (N - q)) => μ) {ω : Fin (N - q) → ℕ | ∑ i : Fin (N - q), ω i = N - q}

The tree case ℓ = 1: P(S_N = -1) = ∑_{q ≤ N} P(|T| = q) P(S_{N-q} = 0).