The killed-gap Green kernel

The gap walk started at x > 0 is killed when the original increment walk first reaches x. Prepending x zero offspring values embeds it in a first weak cycle. Duality then gives a finite Green kernel without any offspring second moment. The bound here is geometric in x; it is not the scale-uniform renewal estimate.

def BGW.StableTrees.DiscreteHeightApprox.killedGapEvent (x y k : ℕ) : Set (ℕ → ℕ)

A killed-gap walk started at x survives through time k and is then at y.

Equations

• BGW.StableTrees.DiscreteHeightApprox.killedGapEvent x y k = {ω : ℕ → ℕ | BGW.StableTrees.DiscreteForest.walk ω k = ↑x - ↑y ∧ ∀ u ≤ k, BGW.StableTrees.DiscreteForest.walk ω u < ↑x}

noncomputable def BGW.StableTrees.DiscreteHeightApprox.killedGapGreen (μ : PMF ℕ) (x y : ℕ) : ENNReal

The Green kernel of the gap walk killed on entering the nonpositive half-line.

Equations

• BGW.StableTrees.DiscreteHeightApprox.killedGapGreen μ x y = ∑' (k : ℕ), ↑(BGW.StableTrees.DiscreteForest.offspringSeqLaw μ) (BGW.StableTrees.DiscreteHeightApprox.killedGapEvent x y k)

theorem BGW.StableTrees.DiscreteHeightApprox.measurableSet_killedGapEvent (x y k : ℕ) : MeasurableSet (killedGapEvent x y k)

Each finite killed-gap transition event is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.killedGapGreen_weighted_le_one (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (x y : ℕ) : μ 0 ^ x * killedGapGreen μ x y ≤ 1

A geometric entrance bound controls every killed-gap transition series. It proves finiteness, but does not replace the sharper weak-ladder renewal bound.

theorem BGW.StableTrees.DiscreteHeightApprox.killedGapGreen_lt_top (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (x y : ℕ) : killedGapGreen μ x y < ⊤

Every killed-gap Green entry is finite, with infinite offspring variance allowed.