Uniform bounds for discrete bridge prefix densities

The scalar local upper bound and admissible endpoint lower bound, combined with regular variation of the norming, control every prefix strictly before time one.

noncomputable def BGW.StableTrees.DiscreteBridge.bridgePathDensity (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (a : NNReal) (x : Skorokhod.D ↑a ℝ) : ℝ

The bridge prefix density as a function of the path on [0,a]: walkProb μ (n-m) (-1-W_m) / walkProb μ n (-1), m = ⌊a n⌋, W_m = B n * x(a) rounded.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.DiscreteBridge.bridgeRemaining_ratio (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (n : ℕ) => ↑(n - ⌊↑a * ↑n⌋₊) / ↑n) Filter.atTop (nhds (1 - ↑a))

The remaining number of increments divided by the full size tends to 1-a.

theorem BGW.StableTrees.DiscreteBridge.bridgePathDensity_le {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, Admissible μ n → ∀ (x : Skorokhod.D ↑a ℝ), 0 ≤ bridgePathDensity μ B n a x ∧ bridgePathDensity μ B n a x ≤ C

Uniform bound of the bridge prefix density for a fixed a < 1 (Scalar.exists_walkProb_le, Scalar.exists_lower_bound_neg_one, regular variation of B).