Weak-epoch cutoff removal

Before a bounded walk maximum, many weak epochs force their attained height to remain bounded. The ladder transform controls this event exponentially.

theorem BGW.StableTrees.DiscreteHeightApprox.measure_walk_maximum (μ : PMF ℕ) (k : ℕ) (r : ℝ) : ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | ∃ u ≤ k, r < |↑(DiscreteForest.walk ω u)|} = ENNReal.ofReal (Probability.RealWalk.maxTail (realOffspringStepLaw μ) k r)

The finite offspring-walk maximum has the canonical real iid-walk tail.

theorem BGW.StableTrees.DiscreteHeightApprox.ladderCount_large_subset {ω : ℕ → ℕ} (hω : EpochsFinite ω) (k : ℕ) {b q x K : ℝ} (hb : 0 < b) (hq : 0 < q) (hlarge : x < b / q * ↑(weakLadderCount ω k)) : (∃ u ≤ k, K * b < |↑(DiscreteForest.walk ω u)|) ∨ ↑(weakEpochHeight ω ⌈x * q / b⌉₊) ≤ K * b

Many epochs before time k force either a large walk maximum or a low attained height.

theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderCount_tight_ascending {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (t : NNReal) : Filter.Tendsto (fun (x : ℝ) => Filter.limsup (fun (n : ℕ) => ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | x < B n / ↑n * ↑(weakLadderCount ω ⌊↑n * ↑t⌋₊)}) Filter.atTop) Filter.atTop (nhds 0)

The normalized weak ladder count is tight on every fixed finite horizon.

theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderCount_tight {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (t : NNReal) : Filter.Tendsto (fun (x : ℝ) => Filter.limsup (fun (n : ℕ) => ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | x < B n / ↑n * ↑(DiscreteForest.forestHeight ω ⌊↑n * ↑t⌋₊)}) Filter.atTop) Filter.atTop (nhds 0)

Cutoff removal: the normalized ladder count (B_n/n) H_{⌊nt⌋} is tight (ladder-height subordinator of index θ-1 and sealed walk-supremum tightness: {H_k ≥ N} = {τ_N ≤ k}).