Documentation

BGW.StableTrees.DiscreteForestPrefixCoding

Surviving prefixes and the remaining forest #

After a surviving prefix, the remaining pending subtrees are counted by the prefix stack. First passage to minus that stack is exactly completion of the first tree. This is a deterministic finite-word statement.

source
@[instance_reducible]
def BGW.StableTrees.DiscreteForest.prefixCodingWordMeasurable :
MeasurableSpace (List ℕ)

A local discrete structure for finite prefix words.

Equations
Instances For
    source
    theorem BGW.StableTrees.DiscreteForest.prefixCodingWordSingleton :
    MeasurableSingletonClass (List ℕ)

    Prefix-word singletons are measurable in the local structure.

    source
    theorem BGW.StableTrees.DiscreteForest.treePrefix_toLocallyFinite (m : ℕ) (t : PlaneTree) :
    treePrefix m t.toLocallyFinite = List.take m t.degrees

    The finite-tree bridge preserves the DFS prefix observable.

    source
    theorem BGW.StableTrees.DiscreteForest.prefixCylinder_eq_image (m : ℕ) (a : List ℕ) :
    prefixCylinder m a = PlaneTree.toLocallyFinite '' {t : PlaneTree | List.take m t.degrees = a}

    Prefix cylinders are countable images of finite trees.

    source
    theorem BGW.StableTrees.DiscreteForest.measurableSet_prefixCylinder (m : ℕ) (a : List ℕ) :
    MeasurableSet (prefixCylinder m a)

    Every finite prefix cylinder is measurable.

    source
    theorem BGW.StableTrees.DiscreteForest.measurable_treePrefix (m : ℕ) :
    Measurable (treePrefix m)

    The totalized tree-prefix observable is measurable.

    source
    theorem BGW.StableTrees.DiscreteForest.prefixStack_cast {a : List ℕ} (hs : IsSurvivingPrefix a) :
    ↑(prefixStack a) = prefixWalk a + 1

    The pending-stack integer of a surviving prefix is its walk value plus one.

    source
    theorem BGW.StableTrees.DiscreteForest.prefixStack_pos {a : List ℕ} (hs : IsSurvivingPrefix a) :
    1 ≤ prefixStack a

    A surviving prefix always leaves a positive number of pending subtrees.

    source
    theorem BGW.StableTrees.DiscreteForest.prefix_ladder_iff_forestHit {ω : ℕ → ℕ} (hω : LadderFinite ω) {n m : ℕ} {a : List ℕ} (ham : a.length = m) (hmn : m < n) (hs : IsSurvivingPrefix a) :
    seqPrefix m ω = a ∧ ladderTime ω 1 = n ↔ seqPrefix m ω = a ∧ shiftSeq m ω ∈ forestHit (prefixStack a) (n - m)

    Completing the first tree after a surviving prefix is first passage for its pending forest.

    source
    theorem BGW.StableTrees.DiscreteForest.first_block_size {ω : ℕ → ℕ} (hω : LadderFinite ω) :
    (blockTree ω 0).size = ladderTime ω 1

    The first decoded block has length equal to its first ladder time.

    source
    theorem BGW.StableTrees.DiscreteForest.treePrefix_first_block {ω : ℕ → ℕ} (hω : LadderFinite ω) (m : ℕ) (hm : m ≤ ladderTime ω 1) :
    treePrefix m (blockLF ω 0) = seqPrefix m ω

    Prefixes within the first block are exactly initial offspring prefixes.

    source
    theorem BGW.StableTrees.DiscreteForest.first_block_law (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) :
    MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => blockLF ω 0) ↑(offspringSeqLaw μ) = LocallyFinite.bienaymeLaw μ.toMeasure

    The first block has the unconditioned BGW law.