Talagrand's Convolution Bound for Tensor Powers of Finite-State Markov Semigroups
Alexander Marsh
math.PR
Nov 11, 2026 · v1
TL;DR
The main theorem, a generalization of Talagrand's convolution bound to finite-state Markov semigroups, is formally verified in Lean 4 with a public formalization produced with AI assistance.
Abstract
Talagrand's convolution conjecture, recently proven by J. Lu, S. Guo, and E. Fang, concerns the smoothing properties of the heat semigroup on $\{-1,1\}^N$. We follow their perturbed coupled reverse-heat approach to generalize the theorem to tensor powers of irreducible continuous-time Markov semigroups on finite state spaces. Specifically, let $(S_t)_{t\geq0}$ be the semigroup of an irreducible continuous-time Markov chain on a finite state space $G_0$ with stationary distribution $π$. Then, for every $τ>0$, there exists a finite constant $C_{τ,S,π}<\infty$ such that, for every $N\geq1$, every nonnegative function $f:G_0^N\to[0,\infty)$, and every $η>1$, \begin{align*} π^{\otimes N}\left(S_τ^{\otimes N}f>η\int_{G_0^N}f\,dπ^{\otimes N}\right)\leq\frac{C_{τ,S,π}}{η\sqrt{\logη}}, \end{align*} where the constant is independent of $N$, $f$, and $η$. Most of the machinery developed by Lu, Guo, and Fang transfers cleanly, but since probability distributions on $|G_0|$ elements are not determined by their mean for $|G_0|>2$, we must use explicit terminal bridge laws to find a dimension-independent bound for the terminal-discrepancy estimate. We have formalized our result in Lean 4. The formalization is publicly available.
Problem
Talagrand's convolution conjecture, recently proven by Lu, Guo, and Fang for the heat semigroup on {-1,1}^N, gives a dimension-free tail bound of order 1/(η√log η) for smoothed functions. The question is whether the same bound holds for tensor powers of general irreducible continuous-time Markov semigroups on finite state spaces.
Approach
The authors first prove the bound for a π-refresh semigroup, in which each coordinate is independently resampled from π. They follow Lu–Guo–Fang's perturbed coupled reverse-heat approach, using anti-concentration profiles, a general log-Sobolev inequality, band contraction and stopped score bounds. Explicit terminal bridge laws are needed because distributions on more than two states are not determined by their mean. The general case follows by factoring any semigroup through the π-refresh semigroup, and the main theorem is formalized in Lean 4.
Results
For every τ>0 there is a constant C, independent of N, f and η, such that π^{⊗N}(S_τ^{⊗N} f > η∫f) ≤ C/(η√log η). The main theorem is formally verified in Lean 4, with larger constants allowed in intermediate lemmas, and the formalization is publicly available.
