Unconditioned masses of surviving prefixes

Completing a surviving initial word is first passage of the remaining forest. The exact mass is a product, and summing over the size gives the inclusive tail.

theorem BGW.StableTrees.DiscreteForest.sizeEvent_prefixCylinder_mass (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n m : ℕ} {a : List ℕ} (ham : a.length = m) (hmn : m < n) (hs : IsSurvivingPrefix a) : (LocallyFinite.bienaymeLaw μ.toMeasure) (LocallyFinite.sizeEvent n ∩ prefixCylinder m a) = (List.map (⇑μ) a).prod * forestWeight (⇑μ) (prefixStack a) (n - m)

The joint exact-size/prefix mass is the prefix weight times the remaining forest mass.

theorem BGW.StableTrees.DiscreteForest.sizeEvent_prefixCylinder_real (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n m : ℕ} {a : List ℕ} (ham : a.length = m) (hmn : m < n) (hs : IsSurvivingPrefix a) : (LocallyFinite.bienaymeLaw μ.toMeasure).real (LocallyFinite.sizeEvent n ∩ prefixCylinder m a) = degreeWeight μ a * forestMass μ (prefixStack a) (n - m)

The real-valued exact joint mass.

theorem BGW.StableTrees.DiscreteForest.sizeGeEvent_prefixCylinder_real (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {n m : ℕ} {a : List ℕ} (ham : a.length = m) (hmn : m < n) (hs : IsSurvivingPrefix a) : (LocallyFinite.bienaymeLaw μ.toMeasure).real (Attraction.sizeGeEvent n ∩ prefixCylinder m a) = degreeWeight μ a * forestTail μ (prefixStack a) (n - m)

The real joint inclusive-tail/prefix mass.