Small sets (minorization) and the geometric / polynomial drift conditions

Definition

MarkovDriftMinorization

by Shuze Chen · Aug 15, 2026 · Mathlib c5ea003 (Lean v4.30.0)

markov-chainsmcmcprobability

The constructive tools of the source's Section 2, for a transition kernel $P$ on a state space $\mathsf{X}$ .

Small set (minorization condition, eq. (4)): a set $C$ is small for $P$ if there exist an integer $n_0 \ge 1$ , a real $\varepsilon > 0$ and a probability measure $Q$ such that

P^{n_0}(x, A) \;\ge\; \varepsilon\, Q(A) \qquad \text{for all } x \in C \text{ and all measurable } A.

Geometric drift condition (eq. (5)) towards $C$ , with constants $d, b$ : the function $V$ is integrable under every $P(x, \cdot)$ and

PV(x) - V(x) \;\le\; -d\, V(x) + b\, \mathbb{1}_C(x) \qquad \text{for all } x, \quad \text{where } PV(x) = \int V(y)\, P(x, dy).

Polynomial drift condition (eq. (6)), with exponent $0 \le \tau < 1$ : likewise with $-d\, V(x)^{\tau}$ in place of $-d\, V(x)$ .

Drift and minorization are the standard constructive route to geometric and polynomial ergodicity in Markov chain Monte Carlo, and the hypotheses of the mission's Theorem 1.

Formalization Note The integrability of $V$ under each $P(x, \cdot)$ is part of each drift condition, so that $PV$ is genuinely defined rather than a vacuous convention.

Definition code

import Definitions.Def_MarkovIterKernel
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.MeasureTheory.Integral.Bochner.Basic

/-!
Minorization (small sets) and the geometric / polynomial drift conditions.

Source: Galin L. Jones, *On the Markov Chain Central Limit Theorem*,
Probability Surveys 1 (2004) 299-320 (arXiv math/0409112v2), §2:
eq. (4) (minorization), eq. (5) (geometric drift), eq. (6) (polynomial drift).
-/

open MeasureTheory ProbabilityTheory

namespace MarkovChainCLT

/-- **Minorization / small set** (Jones 2004 eq. (4)): `C` is small for `P` if there
are `n₀ ≥ 1`, `ε > 0` and a probability measure `Q` with
`P^{n₀}(x, A) ≥ ε Q(A)` for all `x ∈ C` and all measurable `A`. -/
def IsSmallSet {X : Type*} [MeasurableSpace X] (P : Kernel X X) (C : Set X) : Prop :=
  ∃ n₀ : ℕ, 1 ≤ n₀ ∧ ∃ ε : ℝ, 0 < ε ∧ ∃ Q : Measure X, IsProbabilityMeasure Q ∧
    ∀ x ∈ C, ∀ A : Set X, MeasurableSet A →
      ENNReal.ofReal ε * Q A ≤ (iterKernel P n₀) x A

/-- **Geometric drift condition** (Jones 2004 eq. (5)): `V` is integrable under every
`P(x, ·)` and `PV(x) - V(x) ≤ -d V(x) + b 1_C(x)` for all `x`.  (The integrability
conjunct is part of the condition: it rules out the vacuous reading where the
integral of a non-integrable `V` is junk.) -/
def GeoDriftCondition {X : Type*} [MeasurableSpace X] (P : Kernel X X) (V : X → ℝ)
    (d b : ℝ) (C : Set X) : Prop :=
  (∀ x, Integrable V (P x)) ∧
    ∀ x, (∫ y, V y ∂(P x)) - V x ≤ -d * V x + b * C.indicator (fun _ => (1 : ℝ)) x

/-- **Polynomial drift condition** (Jones 2004 eq. (6)):
`PV(x) - V(x) ≤ -d V(x)^τ + b 1_C(x)` for all `x`, with `V` integrable under every
`P(x, ·)`. -/
def PolyDriftCondition {X : Type*} [MeasurableSpace X] (P : Kernel X X) (V : X → ℝ)
    (d b τ : ℝ) (C : Set X) : Prop :=
  (∀ x, Integrable V (P x)) ∧
    ∀ x, (∫ y, V y ∂(P x)) - V x ≤ -d * V x ^ τ + b * C.indicator (fun _ => (1 : ℝ)) x

end MarkovChainCLT

Source

G. L. Jones, "On the Markov Chain Central Limit Theorem", Probability Surveys 1 (2004) 299-320, arXiv math/0409112v2, Section 2 (arXiv v2 p. 4), eqs. (4), (5), (6)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

IsSmallSet — For a measurable type $X$ , a kernel $P$ from $X$ to $X$ (not assumed Markov), and an arbitrary set $C \subseteq X$ (not assumed measurable): the proposition that there exist a natural number $n_0 \ge 1$ , a real $\varepsilon > 0$ , and a measure $Q$ on $X$ which is a probability measure, such that for every $x \in C$ and every measurable set $A \subseteq X$ , $\varepsilon \cdot Q(A) \le (\mathrm{iterKernel}\,P\,n_0)(x)(A)$ — an inequality of extended-nonnegative reals, with $\varepsilon$ embedded into $[0,\infty]$ . Here $\mathrm{iterKernel}\,P\,n_0$ is the $n_0$ -step kernel: identity kernel ( $x \mapsto \delta_x$ ) at step $0$ , and each successor step applies $P$ once more, so $(\mathrm{iterKernel}\,P\,(m+1))(x)(A) = \int P(y,A)\,d(\mathrm{iterKernel}\,P\,m)(x)(y)$ . Degenerate cases: if $C = \varnothing$ , the condition quantified over $x \in C$ is vacuous, so the empty set satisfies the predicate as soon as any probability measure exists on $X$ (which holds for any nonempty $X$ via a Dirac measure); conversely if $X$ admits no probability measure (e.g. $X$ empty), no set — not even $\varnothing$ — satisfies it.

GeoDriftCondition — For a measurable type $X$ , a kernel $P$ , a function $V : X \to \mathbb{R}$ , reals $d$ and $b$ (both completely unconstrained in sign), and an arbitrary set $C \subseteq X$ (not assumed measurable): the conjunction of (i) for every $x$ , $V$ is Bochner-integrable with respect to the measure $P(x,\cdot)$ (almost-everywhere strong measurability plus finite $\int |V|\,dP(x,\cdot)$ ); and (ii) for every $x \in X$ , $\bigl(\int V(y)\,dP(x,\cdot)(y)\bigr) - V(x) \le -d\,V(x) + b\,\mathbf{1}_C(x)$ , where $\mathbf{1}_C$ is the indicator function equal to $1$ on $C$ and $0$ off $C$ . No sign or lower-bound condition is imposed on $V$ itself.

PolyDriftCondition — For a measurable type $X$ , a kernel $P$ , a function $V : X \to \mathbb{R}$ , reals $d$ , $b$ , $\tau$ (all unconstrained), and an arbitrary set $C \subseteq X$ : the conjunction of (i) for every $x$ , $V$ is Bochner-integrable with respect to $P(x,\cdot)$ ; and (ii) for every $x \in X$ , $\bigl(\int V(y)\,dP(x,\cdot)(y)\bigr) - V(x) \le -d\,\bigl(V(x)\bigr)^{\tau} + b\,\mathbf{1}_C(x)$ , with $\mathbf{1}_C$ the indicator of $C$ . The power $\bigl(V(x)\bigr)^{\tau}$ is the real power with real exponent, whose conventions matter when $V(x) \le 0$ : for base $0$ it equals $0$ when $\tau \ne 0$ and $1$ when $\tau = 0$ ; for negative base $V(x) < 0$ it equals $|V(x)|^{\tau} \cos(\pi\tau)$ . Nothing forces $V \ge 0$ , $d > 0$ , $b \ge 0$ , or $\tau \in (0,1)$ .

Human review

Endorsed by Community (Bot) · Aug 15, 2026
Endorsed by Shuze Chen · Aug 15, 2026
Confirmed by the mission captain (proposal self-audit).

View graph