Prefix masses for the offspring walk bridge

Deterministic splitting at the end of a word and the product law identify the remaining endpoint mass. Conditioning divides by the full bridge mass.

@[instance_reducible]

def BGW.StableTrees.DiscreteForest.bridgeWordMeasurable : MeasurableSpace (List ℕ)

A local discrete structure for bridge degree-word observables.

Equations

• BGW.StableTrees.DiscreteForest.bridgeWordMeasurable = ⊤

theorem BGW.StableTrees.DiscreteForest.bridgeWordSingleton : MeasurableSingletonClass (List ℕ)

Degree-word singletons are measurable in the bridge's local structure.

theorem BGW.StableTrees.DiscreteForest.prefixWalk_seqPrefix (m : ℕ) (ω : ℕ → ℕ) : prefixWalk (seqPrefix m ω) = walk ω m

The word walk agrees with the walk of its originating sequence.

theorem BGW.StableTrees.DiscreteForest.walk_event_real (μ : PMF ℕ) (n : ℕ) (z : ℤ) : (↑(offspringSeqLaw μ)).real {ω : ℕ → ℕ | walk ω n = z} = walkProb μ (↑n) z

A scalar walk atom as the real mass of an offspring-sequence event.

theorem BGW.StableTrees.DiscreteForest.bridgePrefix_mass (μ : PMF ℕ) {n m : ℕ} {a : List ℕ} (ham : a.length = m) (hmn : m ≤ n) : (↑(offspringSeqLaw μ)).real {ω : ℕ → ℕ | seqPrefix m ω = a ∧ walk ω n = -1} = degreeWeight μ a * walkProb μ (↑(n - m)) (-1 - prefixWalk a)

Bridge prefix mass: P(first m degrees = a, W_n = -1) = ∏μ(a_i) * P(W_{n-m} = -1 - W_m(a)), for m ≤ n.

theorem BGW.StableTrees.DiscreteForest.bridgePrefix_cond_mass (μ : PMF ℕ) {n m : ℕ} {a : List ℕ} (ham : a.length = m) (hmn : m ≤ n) (hpos : 0 < walkProb μ (↑n) (-1)) : (↑(offspringSeqLaw μ))[|{ω : ℕ → ℕ | walk ω n = -1}].real {ω : ℕ → ℕ | seqPrefix m ω = a} = degreeWeight μ a * bridgePrefixDensity μ n m (prefixWalk a)

Conditional on W_n = -1, the prefix mass is ∏μ(a_i) times the bridge-prefix density (positive denominator).