A density bound uniform over short prefixes #
All cutoffs at most one half share a single density bound. This lets small-block maximal estimates control a shrinking initial or terminal window.
theorem
BGW.StableTrees.DiscreteBridge.bridgePathDensity_short_le
{μ : PMF ℕ}
{θ : ℝ}
{B : ℕ → ℝ}
(h : StableDomain μ θ B)
:
∃ (C : ℝ),
0 < C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, Admissible μ n → ∀ (a : NNReal), 0 < a → ↑a ≤ 1 / 2 → ∀ (x : Skorokhod.D ↑a ℝ), bridgePathDensity μ B n a x ≤ C
A single positive constant bounds every bridge density with cutoff at most one half.