Finite-vector bridge prefix masses

Restriction of the infinite iid product to Fin n transports K02's conditional prefix mass identity to offspring vectors.

@[instance_reducible]

def BGW.StableTrees.DiscreteBridge.prefixWordMeasurable : MeasurableSpace (List ℕ)

Discrete measurable structure for degree words, local to the prefix adapter.

Equations

• BGW.StableTrees.DiscreteBridge.prefixWordMeasurable = ⊤

theorem BGW.StableTrees.DiscreteBridge.prefixWordSingleton : MeasurableSingletonClass (List ℕ)

Degree-word singletons are measurable in the local structure.

theorem BGW.StableTrees.DiscreteBridge.bridgeVecPrefix_cond_mass (μ : PMF ℕ) {n m : ℕ} {a : List ℕ} (ham : a.length = m) (hmn : m ≤ n) (hpos : 0 < walkProb μ (↑n) (-1)) : (offspringVec μ n)[|countBridges n].real {ω : Fin n → ℕ | List.take m (List.ofFn ω) = a} = DiscreteForest.degreeWeight μ a * (walkProb μ (↑(n - m)) (-1 - DiscreteForest.prefixWalk a) / walkProb μ (↑n) (-1))

Conditional on W_n = -1, the mass of the first m degrees a is ∏ μ(a_i) * walkProb μ (n-m) (-1-W_m(a)) / walkProb μ n (-1).