Moving endpoint local limits for discrete bridges

The lattice local limit theorem applies to signed endpoints. The lattice factors in the remaining-walk numerator and admissible bridge denominator cancel.

theorem BGW.StableTrees.DiscreteBridge.walkProb_neg_one_pos {μ : PMF ℕ} {n : ℕ} (hn : Admissible μ n) : 0 < walkProb μ (↑n) (-1)

Every admissible size has a strictly positive bridge endpoint probability.

theorem BGW.StableTrees.DiscreteBridge.walkLocalLimit_seq {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hq : Filter.Tendsto q Filter.atTop Filter.atTop) {z : ℕ → ℤ} {x : ℝ} (hz : Filter.Tendsto (fun (k : ℕ) => ↑(z k) / B (q k)) Filter.atTop (nhds x)) (hdiv : ∀ᶠ (k : ℕ) in Filter.atTop, ↑(Scalar.latticeSpan μ) ∣ z k + ↑(q k)) : Filter.Tendsto (fun (k : ℕ) => B (q k) * walkProb μ (↑(q k)) (z k)) Filter.atTop (nhds (↑(Scalar.latticeSpan μ) * Scalar.stableDensity θ x))

A sequential local limit for arbitrary signed endpoints on the reachable lattice.

theorem BGW.StableTrees.DiscreteBridge.bridgeRemaining_norming_ratio {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (n : ℕ) => B n / B (n - ⌊↑a * ↑n⌋₊)) Filter.atTop (nhds ((1 - ↑a) ^ (-(1 / θ))))

Regular variation compares the full and remaining normings at a fixed strict prefix.

theorem BGW.StableTrees.DiscreteBridge.bridgeRemaining_atTop (a : NNReal) (ha : a ∈ Set.Ioo 0 1) {q : ℕ → ℕ} (hq : Filter.Tendsto q Filter.atTop Filter.atTop) : Filter.Tendsto (fun (k : ℕ) => q k - ⌊↑a * ↑(q k)⌋₊) Filter.atTop Filter.atTop

The remaining time tends to infinity along every unbounded sequence of full sizes.

theorem BGW.StableTrees.DiscreteBridge.bridgeRatio_tendsto {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) {z : ℕ → ℤ} {x : ℝ} (hz : Filter.Tendsto (fun (k : ℕ) => ↑(z k) / B (q k)) Filter.atTop (nhds x)) (hdiv : ∀ᶠ (k : ℕ) in Filter.atTop, ↑(Scalar.latticeSpan μ) ∣ z k + ↑(q k - ⌊↑a * ↑(q k)⌋₊)) : Filter.Tendsto (fun (k : ℕ) => walkProb μ (↑(q k - ⌊↑a * ↑(q k)⌋₊)) (z k) / walkProb μ (↑(q k)) (-1)) Filter.atTop (nhds (stableDensityAt θ (1 - ↑a) x / Scalar.stableDensity θ 0))

Ratio limit for signed remaining endpoints, with their lattice compatibility explicit.