Documentation

BGW.StableTrees.HeightTightnessUpcrossings

First height upcrossings as integer stopping times #

The first integer time at which the forest height reaches a level is determined by the offspring coordinates strictly before it, and it is almost surely finite for a critical nondegenerate offspring law.

source
noncomputable def BGW.StableTrees.HeightTightness.heightUpcrossingStop (q : ℕ) (ω : ℕ → ℕ) :
ℕ∞

First integer time at which the forest height reaches q, with value infinity if absent.

Equations
Instances For
    source
    theorem BGW.StableTrees.HeightTightness.heightUpcrossingStop_eq_natCast_iff (q n : ℕ) (ω : ℕ → ℕ) :
    heightUpcrossingStop q ω = ↑n ↔ q ≤ DiscreteForest.forestHeight ω n ∧ ∀ k < n, DiscreteForest.forestHeight ω k < q

    A finite first upcrossing is characterized by the height at that time and its past.

    source
    theorem BGW.StableTrees.HeightTightness.isSeqStoppingTime_heightUpcrossingStop (q : ℕ) :
    DiscreteForest.IsSeqStoppingTime (heightUpcrossingStop q)

    First upcrossings use only the offspring coordinates strictly before the crossing time.

    source
    theorem BGW.StableTrees.HeightTightness.ae_heightUpcrossingStop_ne_top (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q : ℕ) :
    ∀ᵐ (ω : ℕ → ℕ) ∂↑(DiscreteForest.offspringSeqLaw μ), heightUpcrossingStop q ω ≠ ⊤

    Every fixed height is eventually reached almost surely in a critical nondegenerate forest.