Finite offspring cylinders and degree words

Degree words, their weights, walk values, surviving prefixes and pending stacks. Finite restrictions of the infinite offspring product have the usual finite product law. Degree lists retain their order from time zero.

@[instance_reducible]

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

The discrete sigma-algebra on degree words, local to this module.

Equations

• BGW.StableTrees.DiscreteForest.cylinderListMeasurable = ⊤

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

Single degree words are measurable in the local discrete sigma-algebra.

def BGW.StableTrees.DiscreteForest.seqPrefix (m : ℕ) (ω : ℕ → ℕ) : List ℕ

The first m offspring numbers of ω.

Equations

• BGW.StableTrees.DiscreteForest.seqPrefix m ω = List.map ω (List.range m)

def BGW.StableTrees.DiscreteForest.prefixWalk (a : List ℕ) : ℤ

The walk value W_m(a) = ∑ (a_i - 1) of a degree word.

Equations

• BGW.StableTrees.DiscreteForest.prefixWalk a = (List.map (fun (d : ℤ) => d - 1) do let a ← a pure ↑a).sum

noncomputable def BGW.StableTrees.DiscreteForest.degreeWeight (μ : PMF ℕ) (a : List ℕ) : ℝ

Product of offspring probabilities along a degree list.

Equations

• BGW.StableTrees.DiscreteForest.degreeWeight μ a = (List.map (⇑μ) a).prod.toReal

def BGW.StableTrees.DiscreteForest.IsSurvivingPrefix (a : List ℕ) : Prop

A prefix of degrees is surviving if all its partial walk values are ≥ 0.

Equations

• BGW.StableTrees.DiscreteForest.IsSurvivingPrefix a = ∀ i ≤ a.length, 0 ≤ (List.map (fun (d : ℤ) => d - 1) do let a ← List.take i a pure ↑a).sum

def BGW.StableTrees.DiscreteForest.prefixStack (a : List ℕ) : ℕ

The number of pending subtrees after exploring a: j = W_m + 1.

Equations

• BGW.StableTrees.DiscreteForest.prefixStack a = ((List.map (fun (d : ℤ) => d - 1) do let a ← a pure ↑a).sum + 1).toNat

theorem BGW.StableTrees.DiscreteForest.map_offspringSeqLaw_initial (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) (i : Fin n) => ω ↑i) ↑(offspringSeqLaw μ) = MeasureTheory.Measure.pi fun (x : Fin n) => μ.toMeasure

Finite restrictions of the offspring sequence have the finite product law.

theorem BGW.StableTrees.DiscreteForest.seqPrefix_eq_ofFn (m : ℕ) (ω : ℕ → ℕ) : seqPrefix m ω = List.ofFn fun (i : Fin m) => ω ↑i

A finite restriction written as a list of its coordinates.

theorem BGW.StableTrees.DiscreteForest.measurable_seqPrefix (m : ℕ) : Measurable (seqPrefix m)

Prefix lists are measurable.

theorem BGW.StableTrees.DiscreteForest.stepWord_initial (m : ℕ) (ω : ℕ → ℕ) : (stepWord fun (i : Fin m) => ω ↑i) = List.map (fun (d : ℕ) => ↑d - 1) (seqPrefix m ω)

The increment word of a finite restriction is the existing count-vector encoding.

theorem BGW.StableTrees.DiscreteForest.sum_seqPrefix (m : ℕ) (ω : ℕ → ℕ) : (List.map (fun (d : ℕ) => ↑d - 1) (seqPrefix m ω)).sum = walk ω m

The sum of the initial increment word is the infinite walk at the same time.

theorem BGW.StableTrees.DiscreteForest.take_seqPrefix (m i : ℕ) (ω : ℕ → ℕ) (hi : i ≤ m) : List.take i (seqPrefix m ω) = seqPrefix i ω

Taking an initial part of a degree prefix just gives the shorter degree prefix.

noncomputable def BGW.StableTrees.DiscreteForest.bridgePrefixDensity (μ : PMF ℕ) (n m : ℕ) (w : ℤ) : ℝ

Bridge-prefix density: walkProb μ (n-m) (-1-W_m) / walkProb μ n (-1).

Equations

• BGW.StableTrees.DiscreteForest.bridgePrefixDensity μ n m w = BGW.StableTrees.walkProb μ (↑(n - m)) (-1 - w) / BGW.StableTrees.walkProb μ (↑n) (-1)