Conditioned tree laws and degree-prefix observables

Tree laws use the existing locally finite carrier. Null conditioning events are totalized by a leaf, and finite DFS prefixes use the finite-tree equivalence. Complete finite trees show that every size tail has positive mass in the critical nondegenerate case.

noncomputable def BGW.StableTrees.DiscreteForest.tailTreeLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.ProbabilityMeasure LocallyFinite.Tree

The BGW law conditioned on size ≥ n (including the null event of infinite trees); the Dirac law at the leaf when the conditioning event has mass zero.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.StableTrees.DiscreteForest.exactTreeLaw (μ : PMF ℕ) (n : ℕ) : MeasureTheory.ProbabilityMeasure LocallyFinite.Tree

The BGW law conditioned on size exactly n; the Dirac leaf if n is not admissible.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.DiscreteForest.bienaymeLaw_sizeGeEvent_ne_zero (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) : (LocallyFinite.bienaymeLaw μ.toMeasure) (Attraction.sizeGeEvent n) ≠ 0

Critical nondegenerate trees have arbitrarily large finite sizes: the tail mass is positive for every n.

noncomputable def BGW.StableTrees.DiscreteForest.treePrefix (m : ℕ) (τ : LocallyFinite.Tree) : List ℕ

The first m DFS degrees of a finite tree (empty list for infinite trees).

Equations

• BGW.StableTrees.DiscreteForest.treePrefix m τ = if h : BGW.LocallyFinite.FiniteVertices τ then List.take m (BGW.PlaneTree.equivFiniteVertices.symm ⟨τ, h⟩).degrees else []

def BGW.StableTrees.DiscreteForest.prefixCylinder (m : ℕ) (a : List ℕ) : Set LocallyFinite.Tree

Finite trees whose first m DFS degrees are a.

Equations

• BGW.StableTrees.DiscreteForest.prefixCylinder m a = {τ : BGW.LocallyFinite.Tree | BGW.LocallyFinite.FiniteVertices τ ∧ BGW.StableTrees.DiscreteForest.treePrefix m τ = a}

noncomputable def BGW.StableTrees.DiscreteForest.prefixDensity (μ : PMF ℕ) (n m : ℕ) (a : List ℕ) : ENNReal

The prefix density, as a function of the first m degrees; 0 off surviving prefixes.

Equations

• One or more equations did not get rendered due to their size.