Masses of finite offspring words

A fixed initial word has the product of its coordinate masses. Fixed-time suffixes are independent of that word, and their walk has the scalar walk law.

theorem BGW.StableTrees.DiscreteForest.seqPrefix_mass (μ : PMF ℕ) (a : List ℕ) : ↑(offspringSeqLaw μ) {ω : ℕ → ℕ | seqPrefix a.length ω = a} = (List.map (⇑μ) a).prod

An initial degree-word cylinder has the product of its coordinate masses.

theorem BGW.StableTrees.DiscreteForest.map_offspringSeqLaw_walk (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => walk ω n) ↑(offspringSeqLaw μ) = walkLaw μ n

The scalar walk law is the law of the integer walk coordinate.

theorem BGW.StableTrees.DiscreteForest.seqPrefix_inter_shift_mass (μ : PMF ℕ) (a : List ℕ) {A : Set (ℕ → ℕ)} (hA : MeasurableSet A) : ↑(offspringSeqLaw μ) ({ω : ℕ → ℕ | seqPrefix a.length ω = a} ∩ shiftSeq a.length ⁻¹' A) = (List.map (⇑μ) a).prod * ↑(offspringSeqLaw μ) A

A degree-word cylinder is independent of the suffix after the word.

theorem BGW.StableTrees.DiscreteForest.prefixWalk_eq_sum_steps (a : List ℕ) : prefixWalk a = (List.map (fun (d : ℕ) => ↑d - 1) a).sum

The walk value of a degree word is the sum of its integer increments.