Exponential bounds for the number of regenerated height crossings

The finite crossing time is the sum of its iid durations. Its Laplace transform therefore factors. Exponential Markov gives a bound for the probability of L crossings before a fixed scaled horizon.

theorem BGW.StableTrees.HeightTightness.heightRegenerationStop_toNat_eq_sum {q L : ℕ} {ω : ℕ → ℕ} (hfin : heightRegenerationStop q L ω ≠ ⊤) : (heightRegenerationStop q L ω).toNat = ∑ j ∈ Finset.range L, heightRegenerationGap q j ω

On a finite crossing time, the preceding gap durations add to that time.

theorem BGW.StableTrees.HeightTightness.integral_exp_heightRegenerationStop (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q L n : ℕ) : ∫ (ω : ℕ → ℕ), Real.exp (-↑(heightRegenerationStop q L ω).toNat / ↑n) ∂↑(DiscreteForest.offspringSeqLaw μ) = (∫ (ω : ℕ → ℕ), Real.exp (-↑(heightUpcrossingStop q ω).toNat / ↑n) ∂↑(DiscreteForest.offspringSeqLaw μ)) ^ L

The Laplace transform of the Lth crossing time factors into L identical transforms.

theorem BGW.StableTrees.HeightTightness.heightRegenerationStop_probability_le (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q L : ℕ) {n : ℕ} (hn : 1 ≤ n) {T : ℝ} (hT : 0 ≤ T) : (↑(DiscreteForest.offspringSeqLaw μ)).real {ω : ℕ → ℕ | heightRegenerationStop q L ω ≤ ↑⌊↑n * T⌋₊} ≤ Real.exp T * (∫ (ω : ℕ → ℕ), Real.exp (-↑(heightUpcrossingStop q ω).toNat / ↑n) ∂↑(DiscreteForest.offspringSeqLaw μ)) ^ L

Exponential Markov bound for the number of regenerated upcrossings before a horizon.