Conditional prefix atoms

Dividing the unconditioned prefix-completion identities by the conditioning masses gives the tail and exact prefix atoms and their discrete density ratio.

theorem BGW.StableTrees.DiscreteForest.forestTail_pos (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) : 0 < forestTail μ 1 n

Every inclusive tree-size tail has positive real mass in the critical nondegenerate case.

theorem BGW.StableTrees.DiscreteForest.tailTreeLaw_toMeasure (μ : PMF ℕ) (n : ℕ) (h : (LocallyFinite.bienaymeLaw μ.toMeasure) (Attraction.sizeGeEvent n) ≠ 0) : ↑(tailTreeLaw μ n) = (LocallyFinite.bienaymeLaw μ.toMeasure)[|Attraction.sizeGeEvent n]

The tail tree law is the conditional BGW measure when its tail mass is positive.

theorem BGW.StableTrees.DiscreteForest.exactTreeLaw_toMeasure (μ : PMF ℕ) (n : ℕ) (h : Admissible μ n) : ↑(exactTreeLaw μ n) = (LocallyFinite.bienaymeLaw μ.toMeasure)[|LocallyFinite.sizeEvent n]

The exact tree law is the conditional BGW measure at every admissible size.

theorem BGW.StableTrees.DiscreteForest.tailPrefixMass (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n m : ℕ} {a : List ℕ} (ham : a.length = m) (hmn : m < n) (hs : IsSurvivingPrefix a) (hG : 0 < forestTail μ 1 n) : (↑(tailTreeLaw μ n)).real (prefixCylinder m a) = degreeWeight μ a * forestTail μ (prefixStack a) (n - m) / forestTail μ 1 n

Tail law of a surviving prefix: P(prefix = a | ζ ≥ n) = ∏μ(a_i) G_j(n-m) / G_1(n), with m = |a| < n, j = W_m + 1, positive denominator.

theorem BGW.StableTrees.DiscreteForest.exactPrefixMass (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n m : ℕ} {a : List ℕ} (hn : Admissible μ n) (ham : a.length = m) (hmn : m < n) (hs : IsSurvivingPrefix a) : (↑(exactTreeLaw μ n)).real (prefixCylinder m a) = degreeWeight μ a * forestMass μ (prefixStack a) (n - m) / forestMass μ 1 n

Exact law of a surviving prefix: P(prefix = a | ζ = n) = ∏μ(a_i) f_j(n-m) / f_1(n), at an admissible size.

theorem BGW.StableTrees.DiscreteForest.exactPrefixMass_eq_prefixRN_mul (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n m : ℕ} {a : List ℕ} (hn : Admissible μ n) (ham : a.length = m) (hmn : m < n) (hs : IsSurvivingPrefix a) (hG : 0 < forestTail μ (prefixStack a) (n - m)) : (↑(exactTreeLaw μ n)).real (prefixCylinder m a) = exactPrefixWeight μ n m (prefixStack a) * (↑(tailTreeLaw μ n)).real (prefixCylinder m a)

Prefix-atom form of the RN identity: exact mass = R_n(m,j) times tail mass, on every surviving prefix with positive denominators.