Survival bound for the first height upcrossing

A height reached before the end of the first l trees occurs in a block surviving to the same generation. The block laws and a finite union bound give the unscaled first-upcrossing estimate used in the discrete regeneration argument.

theorem BGW.StableTrees.HeightTightness.blockLF_not_extinctBy_of_le_height {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) {k r q : ℕ} (hr : DiscreteForest.ladderTime ω r ≤ k) (hk : k < DiscreteForest.ladderTime ω (r + 1)) (hq : q ≤ DiscreteForest.forestHeight ω k) : DiscreteForest.blockLF ω r ∉ LocallyFinite.extinctBy q

A height in a decoded block forces survival of that block to the same generation.

theorem BGW.StableTrees.HeightTightness.exists_surviving_block_of_height {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) {k l q : ℕ} (hk : k < DiscreteForest.ladderTime ω l) (hq : q ≤ DiscreteForest.forestHeight ω k) : ∃ r < l, DiscreteForest.blockLF ω r ∉ LocallyFinite.extinctBy q

Before the end of the first l trees, every height above q occurs in a surviving block.

theorem BGW.StableTrees.HeightTightness.block_survival_real (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (r q : ℕ) : (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | DiscreteForest.blockLF ω r ∉ LocallyFinite.extinctBy q} = Survival.survivalProb μ q

Every block has the unconditioned BGW survival probability.

theorem BGW.StableTrees.HeightTightness.height_hit_probability_le (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q m l : ℕ) : (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | ∃ k ≤ m, q ≤ DiscreteForest.forestHeight ω k} ≤ ↑l * Survival.survivalProb μ q + (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | DiscreteForest.ladderTime ω l ≤ m}

The first height upcrossing is bounded by survival among the first l trees and passage beyond those trees. This is the finite, unscaled regeneration estimate.