Convergence of strict prefixes of the discrete bridge

Skorokhod representation of the unconditioned FCLT and the signed lattice local limit theorem give convergence of bounded weighted expectations. Conditioning is handled by the prefix Radon–Nikodym identity.

theorem BGW.StableTrees.DiscreteBridge.tendsto_restrictLaw_walkBridgeLaw {μ : 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) : Filter.Tendsto (fun (k : ℕ) => restrictLaw a ⋯ (walkBridgeLaw μ B (q k) ⋯)) Filter.atTop (nhds (restrictLaw a ⋯ (stableBridgeLaw θ)))

Prefix convergence of the walk bridge: for every a ∈ (0,1) the law of the walk bridge on [0,a] converges to the corresponding prefix of the stable bridge.