Documentation

BGW.StableTrees.DiscreteHeightApproxRenewalGreen

The Green diagonal and weak ascending renewal #

Splitting killed visits at weak epochs and applying the exact conditional level mean identifies the Green diagonal with the expected number of epoch heights below its level. Zero height increments remain included in this renewal function.

source
noncomputable def BGW.StableTrees.DiscreteHeightApprox.weakLadderRenewal (μ : PMF ℕ) (m : ℕ) :
ENNReal

Renewal function expressed through the actual weak ascending epoch heights.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem BGW.StableTrees.DiscreteHeightApprox.killedGapGreen_diag_eq_renewal (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (m : ℕ) :
    killedGapGreen μ m m = weakLadderRenewal μ m

    The killed-gap Green diagonal equals the weak ascending height renewal function.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderRenewal_lt_top (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (m : ℕ) :
    weakLadderRenewal μ m < ⊤

    The weak ascending height renewal function is finite at every finite level.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderRenewal_mono (μ : PMF ℕ) :
    Monotone (weakLadderRenewal μ)

    The weak ascending height renewal function is increasing in its cutoff level.