The scalar convolution law in Kemperman's forest identity

The existing forest weights and offspring-count product law agree with the scalar convolution walk. The multiplied identity holds for ℓ ≥ 1 and every time n; division by n is restricted to positive times. No criticality or lattice assumption is needed.

The scalar form adapts PoissonDeclumping/Bridge/Kemperman.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0), using the forest identity already proved in BGW.LocallyFinite.ForestWalkLaw.

theorem BGW.StableTrees.Scalar.walkLaw_neg_eq_pi_countForestBridges (μ : PMF ℕ) (ℓ n : ℕ) : (walkLaw μ n) {-↑ℓ} = (MeasureTheory.Measure.pi fun (x : Fin n) => μ.toMeasure) (countForestBridges ℓ n)

An endpoint -ℓ in the convolution walk is the existing count-bridge event.

theorem BGW.StableTrees.Scalar.natCast_mul_forestWeight_eq_walkLaw (μ : PMF ℕ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (n : ℕ) : ↑n * forestWeight (⇑μ) ℓ n = ↑ℓ * (walkLaw μ n) {-↑ℓ}

Kemperman's identity with the scalar convolution law, including time zero.

theorem BGW.StableTrees.Scalar.natCast_mul_forestWeight_toReal (μ : PMF ℕ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (n : ℕ) : ↑n * (forestWeight (⇑μ) ℓ n).toReal = ↑ℓ * walkProb μ (↑n) (-↑ℓ)

Real-valued Kemperman identity; no division by time is performed.

theorem BGW.StableTrees.Scalar.forestWeight_toReal_eq (μ : PMF ℕ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) {n : ℕ} (hn : 1 ≤ n) : (forestWeight (⇑μ) ℓ n).toReal = ↑ℓ / ↑n * walkProb μ (↑n) (-↑ℓ)

The divided forest formula is restricted to positive times.