Documentation

BGW.StableTrees.DiscreteForestMeasurable

Measurability of discrete ladder blocks and selection #

The totalized first-hit convention is measurable, including paths that never hit. All decoding is performed through the countable space of finite degree lists. The first block of size at least a cutoff, and its measurability, are defined here.

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

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

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

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

    source
    theorem BGW.StableTrees.DiscreteForest.measurable_ladderTime (r : ℕ) :
    Measurable fun (ω : ℕ → ℕ) => ladderTime ω r

    A totalized ladder time is measurable even on paths failing to reach the level.

    source
    theorem BGW.StableTrees.DiscreteForest.measurable_blockDegrees (r : ℕ) :
    Measurable fun (ω : ℕ → ℕ) => blockDegrees ω r

    Each finite block degree list is a measurable function of the offspring sequence.

    source
    theorem BGW.StableTrees.DiscreteForest.measurable_blockLF :
    Measurable fun (ω : ℕ → ℕ) (r : ℕ) => blockLF ω r

    Measurability of the sequence of block trees.

    source
    noncomputable def BGW.StableTrees.DiscreteForest.firstLongIndex (n : ℕ) (ω : ℕ → ℕ) :
    ℕ

    The index of the first block of size ≥ n (junk 0 if there is none).

    Equations
    Instances For
      source
      noncomputable def BGW.StableTrees.DiscreteForest.firstLongTree (n : ℕ) (ω : ℕ → ℕ) :
      LocallyFinite.Tree

      The first tree among the ladder blocks of size ≥ n; junk only on a null set.

      Equations
      Instances For
        source
        theorem BGW.StableTrees.DiscreteForest.measurable_firstLongTree (n : ℕ) :
        Measurable (firstLongTree n)

        Measurability of the first long tree.