Uniform tightness of the regenerated crossing count

A uniformly positive chance of a macroscopic gap contracts the Laplace transform below one. The exponential crossing-count bound then controls the number of crossings before any fixed scaled horizon.

theorem BGW.StableTrees.HeightTightness.heightUpcrossing_laplace_le (μ : PMF ℕ) (q m n : ℕ) : ∫ (ω : ℕ → ℕ), Real.exp (-↑(heightUpcrossingStop q ω).toNat / ↑n) ∂↑(DiscreteForest.offspringSeqLaw μ) ≤ Real.exp (-↑m / ↑n) + (1 - Real.exp (-↑m / ↑n)) * (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | (heightUpcrossingStop q ω).toNat ≤ m}

Splitting at a deterministic cutoff bounds the first-crossing Laplace transform.

theorem BGW.StableTrees.HeightTightness.heightRegenerationGap_zero (q : ℕ) (ω : ℕ → ℕ) : heightRegenerationGap q 0 ω = (heightUpcrossingStop q ω).toNat

The initial regenerated gap is the finite reading of the first-upcrossing time.

theorem BGW.StableTrees.HeightTightness.exists_eventually_heightUpcrossing_laplace_le_lt_one {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {η : ℝ} (hη : 0 < η) : ∃ (ρ : ℝ), 0 ≤ ρ ∧ ρ < 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∫ (ω : ℕ → ℕ), Real.exp (-↑(heightUpcrossingStop ⌊η * ↑n / B n⌋₊ ω).toNat / ↑n) ∂↑(DiscreteForest.offspringSeqLaw μ) ≤ ρ

A uniform positive chance of a macroscopic gap contracts its Laplace transform.

theorem BGW.StableTrees.HeightTightness.exists_eventually_heightRegenerationStop_probability_small {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {η T ε : ℝ} (hη : 0 < η) (hT : 0 ≤ T) (hε : 0 < ε) : ∃ (L : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | heightRegenerationStop ⌊η * ↑n / B n⌋₊ L ω ≤ ↑⌊↑n * T⌋₊} ≤ ε

The number of regenerated upcrossings before a fixed scaled horizon is eventually tight.