Kendall's identity for stable passage times

This module deduces the density of the stable first-passage time from the discrete Kemperman identity, the lattice local limit theorem, and convergence of the rescaled walk passage laws. The lattice factor in the local limit cancels against the mesh of the arithmetic-progression Riemann sums.

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).

theorem BGW.StableTrees.walkHitTime_mass_eq_zero_of_not_dvd {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) {k : ℕ} (hk : ¬↑(Scalar.latticeSpan μ) ∣ ↑k - ↑ℓ) : (↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ))).real {w : ℕ → ℝ | walkHitTime ℓ w = ↑k} = 0

Off the residue class k ≡ ℓ (mod d) the first-hit mass vanishes (Kemperman + LLT support).

theorem BGW.StableTrees.integral_walkPassageLaw_eq_tsum {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) {n : ℕ} (hn : 1 ≤ n) (g : BoundedContinuousFunction ℝ ℝ) (hg : ∀ t ≤ 0, g t = 0) : ∫ (t : ℝ), g t ∂walkPassageLaw μ ℓ n = ∑' (k : ℕ), g (↑k / ↑n) * (↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ))).real {w : ℕ → ℝ | walkHitTime ℓ w = ↑k}

The mass of the walk passage law as a series over the hitting time (ℓ ≥ 1): ∫ g d(walkPassageLaw) = Σ_k g(k/n) P(hit = k) for bounded g vanishing on (-∞, 0].

theorem BGW.StableTrees.walkPassageLaw_tight {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {x : NNReal} (hx : 0 < x) {ℓ : ℕ → ℕ} (hℓ : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ ℓ n) (hscale : Filter.Tendsto (fun (n : ℕ) => ↑(ℓ n) / B n) Filter.atTop (nhds ↑x)) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∃ (R : ℝ), δ < R ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (walkPassageLaw μ (ℓ n) n) (Set.Iio δ) + (walkPassageLaw μ (ℓ n) n) (Set.Ioi R) ≤ ENNReal.ofReal ε

Uniform integrability / tightness near 0 needed to pass from local densities on compacts to the full law: no mass of walkPassageLaw escapes to 0 or ∞ (follows from the weak convergence of walk passage laws (tendsto_walkPassageLaw) and passageLaw_Iic_zero; no walkHitTime tail bound is assumed).

theorem BGW.StableTrees.tendsto_integral_walkPassageLaw_kendall {μ : 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)) {g : ℝ → ℝ} (hg : Continuous g) (hsupp : HasCompactSupport g) (hpos : tsupport g ⊆ Set.Ioi 0) : Filter.Tendsto (fun (n : ℕ) => ∫ (t : ℝ), g t ∂walkPassageLaw μ (ℓ n) n) Filter.atTop (nhds (∫ (s : ℝ) in Set.Ioi 0, g s * kendallKernel θ x s))

Weak limit against compactly supported tests. The density limit is compared with the weak convergence of walk passage laws (tendsto_walkPassageLaw): ∫ g d(walkPassageLaw (ℓ n) n) → ∫ g(s) (x/s) p_s(-x) ds for g continuous with compact support in (0,∞).

theorem BGW.StableTrees.integral_passageLaw_eq_kendall {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {x : NNReal} (hx : 0 < x) {g : ℝ → ℝ} (hg : Continuous g) (hsupp : HasCompactSupport g) (hpos : tsupport g ⊆ Set.Ioi 0) : ∫ (t : ℝ), g t ∂passageLaw θ x = ∫ (s : ℝ) in Set.Ioi 0, g s * kendallKernel θ (↑x) s

Kendall, tested against compactly supported continuous functions. Combining the previous statement with tendsto_walkPassageLaw and uniqueness of weak limits.

theorem BGW.StableTrees.kendall {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {x : NNReal} (hx : 0 < x) : passageLaw θ x = (MeasureTheory.volume.restrict (Set.Ioi 0)).withDensity fun (s : ℝ) => ENNReal.ofReal (↑x / s * stableDensityAt θ s (-↑x))

Kendall's identity for EVERY x > 0 (not just a.e. x): the law of T_x = inf{t | X_t < -x} on real time has density (x/s) p_s(-x) on (0, ∞).

theorem BGW.StableTrees.lintegral_kendallKernel {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {x : NNReal} (hx : 0 < x) : ∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal (kendallKernel θ (↑x) s) = 1

Corollary: total mass one of the Kendall density.