Local limit for walk passage times

Local limit for the first-hit probabilities of the stable-domain walk, used in Kendall's identity.

References: (D. G. Kendall, Some problems in the theory of dams, J. Roy. Statist. Soc. Ser. B 19 (1957), 207–212; A. A. Borovkov, Stochastic Processes in Queueing Theory, Springer, 1976; J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter VII, Corollary 3; local limit theorem: B. V. Gnedenko and A. N. Kolmogorov, Limit Distributions for Sums of Independent Random Variables, Addison-Wesley, 1954, §50).

noncomputable def BGW.StableTrees.kendallKernel (θ x s : ℝ) : ℝ

The Kendall kernel s ↦ (x/s) p_s(-x), s > 0, x > 0 (junk elsewhere).

Equations

• BGW.StableTrees.kendallKernel θ x s = x / s * BGW.StableTrees.stableDensityAt θ s (-x)

theorem BGW.StableTrees.kendallKernel_nonneg {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {x s : ℝ} (hx : 0 ≤ x) (hs : 0 < s) : 0 ≤ kendallKernel θ x s

The kernel is nonnegative for x ≥ 0, s > 0.

theorem BGW.StableTrees.kendallKernel_continuousOn {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ContinuousOn (fun (z : ℝ × ℝ) => kendallKernel θ z.1 z.2) {z : ℝ × ℝ | 0 < z.2}

Continuity of the Kendall density in time (and jointly in the level) for s > 0.

theorem BGW.StableTrees.continuousOn_kendallKernel_time {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : ℝ) : ContinuousOn (kendallKernel θ x) (Set.Ioi 0)

theorem BGW.StableTrees.tendsto_local_walkHitTime_mass {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {x : ℝ} (hx : 0 < x) {ℓ : ℕ → ℕ} (hℓ : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ ℓ n) (hscale : Filter.Tendsto (fun (n : ℕ) => ↑(ℓ n) / B n) Filter.atTop (nhds x)) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℕ), a * ↑n ≤ ↑k → ↑k ≤ b * ↑n → ↑(Scalar.latticeSpan μ) ∣ ↑k - ↑(ℓ n) → |↑n * (↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ))).real {w : ℕ → ℝ | walkHitTime (ℓ n) w = ↑k} - ↑(Scalar.latticeSpan μ) * kendallKernel θ x (↑k / ↑n)| ≤ ε

Local density limit for the walk passage time, with lattice cancellation. Let d = latticeSpan μ, ℓ n / B n → x > 0, 0 < a ≤ b. Uniformly over k ∈ [a n, b n] with d ∣ k - ℓ n, n P(first hit of -ℓ n at time k) → d · (x/(k/n)) p_{k/n}(-x).