Discrete forest mass adapters

The definitions of admissibility, forest masses, tails and prefix weights are shared with the sealed periodic local-limit interface.

theorem BGW.StableTrees.DiscreteForest.summable_forestMass (μ : PMF ℕ) (j : ℕ) : Summable fun (r : ℕ) => forestMass μ j r

The series ∑ f_j converges.

theorem BGW.StableTrees.DiscreteForest.forestTail_eq_tsum_shift (μ : PMF ℕ) (j r : ℕ) (hs : Summable (forestMass μ j)) : forestTail μ j r = ∑' (k : ℕ), forestMass μ j (r + k)

The shifted-sum form of forestTail agrees with the indicator form of K03.

theorem BGW.StableTrees.DiscreteForest.admissible_iff_forestWeight_pos (μ : PMF ℕ) (n : ℕ) : Admissible μ n ↔ 0 < (forestWeight (⇑μ) 1 n).toReal

Admissibility is positivity of the forest weight f_1 (n).

theorem BGW.StableTrees.DiscreteForest.tailMass_eq_forestTail (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) : ((LocallyFinite.bienaymeLaw μ.toMeasure) (Attraction.sizeGeEvent n)).toReal = forestTail μ 1 n

The tail mass is G_1(n) (infinite trees are null under criticality and μ 1 ≠ 1).