Finite first-passage masses

The finite count-vector law and the sealed forest-code correspondence give the mass of first passage to any strictly negative integer level.

def BGW.StableTrees.DiscreteForest.forestHit (j r : ℕ) : Set (ℕ → ℕ)

First passage to -j at time r, expressed without a totalized hitting time.

Equations

• BGW.StableTrees.DiscreteForest.forestHit j r = {ω : ℕ → ℕ | BGW.StableTrees.DiscreteForest.walk ω r = -↑j ∧ ∀ i < r, -↑j < BGW.StableTrees.DiscreteForest.walk ω i}

theorem BGW.StableTrees.DiscreteForest.forestHit_eq_preimage (j r : ℕ) : forestHit j r = (fun (ω : ℕ → ℕ) (i : Fin r) => ω ↑i) ⁻¹' {a : Fin r → ℕ | IsForestCode j (stepWord a)}

The first-passage event is a finite count-vector forest-code cylinder.

theorem BGW.StableTrees.DiscreteForest.measurableSet_forestHit (j r : ℕ) : MeasurableSet (forestHit j r)

First passage is a measurable finite cylinder.

theorem BGW.StableTrees.DiscreteForest.forestHit_mass (μ : PMF ℕ) {j : ℕ} (hj : 1 ≤ j) (r : ℕ) : ↑(offspringSeqLaw μ) (forestHit j r) = forestWeight (⇑μ) j r

The mass of first passage to -j is the mass of the corresponding j-forest.