Documentation

BGW.StableTrees.DiscreteForestBlockLaw

The iid law of ladder blocks #

Work first on finite plane trees with a module-local discrete measurable structure. Finite word cylinders give every finite initial joint law, and projective-limit uniqueness gives the sequence law. Transport then uses the existing embedding into locally finite trees.

source
@[instance_reducible]
def BGW.StableTrees.DiscreteForest.blockLawTreeMeasurable :
MeasurableSpace PlaneTree

A discrete structure used only for the countable finite-tree transport.

Equations
Instances For
    source
    theorem BGW.StableTrees.DiscreteForest.blockLawTreeSingleton :
    MeasurableSingletonClass PlaneTree

    Finite tree singletons are measurable for the local discrete structure.

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

    Degree words also use a local discrete measurable structure.

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

      Degree-word singletons are measurable in the local structure.

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

      The blocks of the walk are iid BGW trees: (blockLF ω r)_r ~ (bienaymeLaw μ)^{⊗ ℕ}. Finite degree-word cylinders and the finite-tree atom formula identify all finite-dimensional laws.