Support of a nondegenerate critical offspring law

A critical probability mass function other than the point mass at one assigns positive mass to zero and to some integer at least two. These scalar facts supply the support assumptions used in lattice Fourier inversion.

Adapted from PoissonDeclumping/Bienayme/Normalization.lean in igor-kortchemski/rare-subtree-patterns, commit fc5ef722392b1af41e8b9d5fc45d5a521b7823dd (Apache-2.0). The second proof reuses the generating-function theorem on measures already available in BGW.GeneratingFunction through the PMF-to-measure map.

theorem BGW.StableTrees.IsCritical.exists_two_le_ne_zero {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : ∃ (j : ℕ), 2 ≤ j ∧ μ j ≠ 0

A critical law with μ 1 ≠ 1 assigns positive mass to some j ≥ 2.

theorem BGW.StableTrees.IsCritical.apply_zero_ne_zero {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : μ 0 ≠ 0

A critical law with μ 1 ≠ 1 assigns positive mass to zero.