Papers With

← All papers
First page of Conditional Stable Laws and Rare-Event Limits for Absorbing Markov Chains

Conditional Stable Laws and Rare-Event Limits for Absorbing Markov Chains

Bernat Bassols Cornudella, Matheus M Castro

math.PR Sep 18, 2026 · v2 math.DS
formalization mathlib probability
Read PDF arXiv abstract Code
TL;DR
Main theorems A–F and nine remarks on conditional limit laws for absorbing Markov chains are formalised in Lean 4 using Mathlib.
Abstract
We establish conditional limit theorems, pointwise in the initial state, for absorbing Markov chains on a compact metric space $M$. We assume $L^1(M,ρ)$-continuous transition densities, irreducibility and aperiodicity. For the observable $f_β(x)=d_M(x,x_0)^{-β}$, with suitable $x_0$ satisfying $ρ(B_r(x_0))\sim C_d(x_0)r^d$, we prove that the point-process of normalised observations converges to a Poisson random measure. This yields totally right-skewed $α$-stable laws for $α=d/β\in(0,2)$ and, at the boundary value $α=2$, a Gaussian limit with the non-standard normalisation $\sqrt{n\log n}$. We also establish a conditional central limit theorem for $L^2$ observables, exponential deviation bounds for bounded observables and a conditional Poisson law for visits to shrinking targets. The results and remarks have been formalised in Lean 4.
Problem

Absorbing Markov chains have stationary measures concentrated on the absorbing set, so these measures say nothing about long-lived transient trajectories. The question is whether observations along trajectories conditioned on survival obey classical limit laws: central and stable limit theorems, deviation bounds, and Poisson limits.

Approach

The setting is chains on a compact metric space with L^1-continuous transition densities, irreducibility and aperiodicity. A spectral decomposition of the killed transition operator yields conditional mixing of all orders. Factorial-moment methods then give point-process convergence, truncation arguments give the stable laws, and the Nagaev–Guivarc'h perturbation method gives the CLT. The theorems and remarks are formalised in Lean 4 with Mathlib.

Results

For f_β(x)=d(x,x0)^{-β}, the normalised observations converge to a Poisson random measure. This gives totally right-skewed α-stable laws for α=d/β in (0,2) and a Gaussian limit with √(n log n) normalisation at α=2. The paper also proves a conditional CLT for L^2 observables, exponential deviation bounds for bounded observables, and a conditional Poisson law for visits to shrinking targets.