Probability

Motivation

An inequality involving only four rows can feed into a recursion for a much larger permutation shuffle. The source seeks an exponent strictly below two that survives a small perturbation of the uniform permutation law. The source is OpenAI's September 2026 manuscript.

Setting

A permanent expectation averages the product of four selected entries, one from each row and each column, over a probability law on the 24 permutations. Uniform marginals require every row to choose each column with probability $1/4$.

Formalization targets

$$\exists p_0\in(4/3,2),\ \varepsilon>0:\quad\sum_{\pi\in S_4}\nu(\pi)\prod_i f_i(\pi(i))\le\prod_i\left(\frac14\sum_j f_i(j)^{p_0}\right)^{1/p_0}.$$

The theorem is stated as admitted, not proved here. Sites are Fin 4, and a law is a real-valued mass function ν on the 24 permutations of the four sites. It states that there exist a real exponent p₀ with 4/3 < p₀ < 2 and a real ε > 0 such that the following holds for every law ν that is a probability law (all masses nonnegative and summing to 1), has total variation distance from the uniform law less than ε (total variation being half the sum over permutations π of |ν(π) − 1/24|), and has uniform marginals (for every pair of sites i and j, the total mass of permutations with π(i)=j equals 1/4). For every 4-by-4 array f of real numbers with all entries f(i,j) ≥ 0, the permanent expectation Σ_π ν(π) ∏_i f(i, π(i)) is at most the product over the four rows i of the normalized ℓ^{p₀} norm of row i, where the norm of a row g is ((Σ_j g(j)^{p₀})/4)^{1/p₀}, using the uniform counting normalization with division by 4.

The goal is OAI.FourRow.robust_permanent. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.

• remaining main.

Significance

The goal is uniform over all nonnegative arrays and all probability laws within the chosen total-variation neighborhood that have exactly uniform marginals. The shared Thorp bundle is included as a separate supporting target. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Near-uniformity alone does not enforce the marginal identities. The exponent improvement must hold even for highly uneven nonnegative row entries.

Formalization scope

The law has nonnegative real masses summing to one. Its distance from the uniform $1/24$ law is strictly less than the selected $\varepsilon$, and row norms use division by four. No explicit value for the existential exponent or radius is imposed.

The shared definitions are supplied by FourRowPermanent, ThorpRemaining. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, A strict four-row permanent inequality and permutation moments, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

Scheduling jobs on unrelated parallel machines to minimize the total weighted completion time, the problem written $R\,|\,|\sum w_jC_j$ in the three-field notation, is one of the basic NP-hard models of machine scheduling. Each job may take a different time on each machine, as when heterogeneous processors, plants or crews serve the same pool of tasks, and the objective rewards finishing important jobs early. For a single machine the problem is solved exactly by Smith's ratio rule (Smith, 1956). With several unrelated machines the problem is strongly NP-hard and the question is how close to the optimum a polynomial-time algorithm can come.

Timeline of the guarantees for $R\,|\,|\sum w_jC_j$:

• Lenstra, Shmoys and Tardos (1990) gave an LP-based 2-approximation for the makespan on unrelated machines; their assignment variables $a_{ij}$ are the ones used here.
• Hall, Schulz, Shmoys and Wein (1997) gave constant-factor approximations for $\sum w_jC_j$ on unrelated machines via time-indexed and interval-indexed LP relaxations.
• Schulz and Skutella (conference version 1999, journal 2002) obtained $3/2+\varepsilon$ by randomized rounding of a time-indexed LP.
• Skutella (J. ACM 2001), the paper of this mission, gave a convex quadratic relaxation in assignment variables alone and a $3/2$-approximation by randomized rounding, with a short analysis.
• Bansal, Srinivasan and Svensson (2016) improved $3/2$ to $3/2-\varepsilon$ for a small constant $\varepsilon>0$; later work lowered the constant further.

Setting

There are $n$ jobs $j\in J$ and $m$ machines $i$. Job $j$ has a weight $w_j\ge 0$ and a processing time $p_{ij}>0$ on machine $i$. A schedule assigns each job to one machine and orders the jobs on every machine; the completion time $C_j$ of a job is the time at which it finishes when each machine works without idle time.

For a fixed assignment, Smith's ratio rule orders each machine optimally. Fix for each machine $i$ the total order $j\prec_i k$ iff $w_j/p_{ij}>w_k/p_{ik}$, ties broken by index. Under an assignment $\sigma$ the completion time of $j$ is

$$C_j(\sigma)=p_{\sigma(j)j}+\sum_{k\prec_{\sigma(j)}j,\ \sigma(k)=\sigma(j)}p_{\sigma(j)k},$$

and the problem is to minimize $\mathrm{val}(\sigma)=\sum_jw_jC_j(\sigma)$ over all assignments.

With $a_{ij}\in\{0,1\}$ indicating that $j$ runs on $i$, the problem is the integer quadratic program (IQP) with objective

$$Z_{QP}(a)=c^Ta+\tfrac12a^TDa,\qquad c_{ij}=w_jp_{ij},$$

where $D$ is symmetric with entry $w_jp_{ik}$ at $((i,j),(i,k))$ for $k\prec_ij$ and zero across machines and on the diagonal. Relaxing $a_{ij}\in\{0,1\}$ to $a\ge 0$ with $\sum_ia_{ij}=1$ gives (QP). Raising the diagonal gives the convex program (CQP), with objective $Z_{CQP}(a)=\tfrac12c^Ta+\tfrac12a^T(D+\operatorname{diag}(c))a$. Adding the lower bound $c^Ta$ gives (CQP′):

$$\min Z\quad\text{s.t.}\quad \textstyle\sum_ia_{ij}=1,\ \ a\ge 0,\ \ Z\ge Z_{CQP}(a),\ \ Z\ge c^Ta .$$

Randomized rounding of a fractional $\bar a$ sends job $j$ to machine $i$ with probability $\bar a_{ij}$, the choices being pairwise independent across jobs, and then orders every machine by $\prec_i$.

Formalization targets

Goal: (CQP′) is a relaxation, and rounding loses at most 3/2

For every instance with $p>0$, $w\ge 0$:

$$\forall\sigma:\ (a^\sigma,\ \mathrm{val}(\sigma))\ \text{is feasible for (CQP′)},$$ $$\forall(\bar a,Z)\ \text{feasible for (CQP′)}:\quad \mathbb E\Bigl[\sum_jw_jC_j\Bigr]\le\tfrac32 Z .$$

The first part makes $Z^*_{CQP'}$ a lower bound on the optimum. The second is Lemma 2.8. Together they are Corollary 2.9 and the value guarantee of the $3/2$-approximation.

Milestones

In attack order:

• Lemma 2.2: $\mathbb E[C_j]=\sum_i(\Pr[j\mapsto i]p_{ij}+\sum_{k\prec_ij}\Pr[j,k\mapsto i]p_{ik})$ for any random assignment.
• Theorem 2.1: rounding a feasible $\bar a$ has expected value exactly $Z_{QP}(\bar a)$.
• Corollary 2.3: (IQP) and (QP) have the same optimum.
• The positive semidefiniteness of $D+\operatorname{diag}(c)$ and Lemma 2.4: $a\mapsto(1-\gamma)c^Ta+\tfrac12a^T(D+2\gamma\operatorname{diag}(c))a$ is convex for all instances iff $\gamma\ge\tfrac12$.
• The identity $Z_{QP}=Z_{CQP}+\tfrac12(c^Ta-a^T\operatorname{diag}(c)a)$ and Theorem 2.6 a), the factor $2$ for (CQP).
• Lemma 2.8, the integrality step of Theorem 2.10, and Corollary 2.11, the bound $(1+c^T\bar a/(2Z))Z$.

Significance

The result gives a $3/2$-approximation for $R\,|\,|\sum w_jC_j$ from a relaxation with only $mn$ variables, without time indexing, so its size does not depend on the processing times. The same convexification, adapted to time slots, yields the factor 2 with release dates (§3 of the paper). The equality of Theorem 2.1 makes the analysis exact: the loss of rounding is exactly the gap between $Z_{QP}$ and the convex objective. The relaxation also bounds the power of preemption (§4), and for identical machines it connects scheduling to Max-$k$-Cut (§6).

All these results are proved in the paper; none is known to be formalized. A formal development adds:

• a checked model of Smith-sequenced assignment schedules;
• the expectation calculus for pairwise independent rounding;
• the positive-semidefiniteness argument of Lemma 2.4;
• a precise statement of what the $3/2$ guarantee says when complexity is set aside.

Difficulty

Two steps resist the obvious approach.

Positive semidefiniteness. $D$ alone is indefinite: two jobs with unit data give the block $\left(\begin{smallmatrix}0&1\\1&0\end{smallmatrix}\right)$. Positive semidefiniteness of $D+\operatorname{diag}(c)$ holds only because the jobs on each machine are ordered by Smith's ratio. A generic matrix argument that ignores this ordering fails, and the "only if" half of Lemma 2.4 needs a specific family of instances.

Exact expectations under pairwise independence. Theorem 2.1 is an equality that uses only the one- and two-job marginals. A proof that silently assumes full independence of the choices proves a different statement. A proof that drops the product condition on pairs is false: with correlated choices the expected value differs from $Z_{QP}$.

Formalization scope

Jobs and machines are Fin n and Fin m; vectors in $\mathbb R^{mn}$ are functions on Fin m × Fin n and $D$ is a Matrix over that type. The order $\prec_i$ is cross-multiplied ($w_jp_{ik}>w_kp_{ij}$, or equality and $j<k$), which equals the page's ratio definition because $p>0$.

Standing assumptions of p. 2 are hypotheses of every theorem: $p_{ij}>0$ and $w_j\ge0$. Hypotheses added relative to the page:

• Corollary 2.11 assumes $Z>0$, which its fraction presupposes;
• the integrality step of Theorem 2.10 assumes integral $p$ and $w$, as the page's proof does.

Optimum. The scheduling optimum $Z^*$ is the minimum of $\mathrm{val}$ over assignments, by Smith's rule (p. 7, cited by the paper, not reproved). "Within a factor $\alpha$ of the optimum" is stated as a bound against the value of every assignment, so no optimum is presupposed.

Rounding. Randomized rounding is any nonnegative weight $\mu$ of total mass 1 on assignments, with $\Pr_\mu[j\mapsto i]=\bar a_{ij}$ and $\Pr_\mu[j\mapsto i,\,k\mapsto h]=\bar a_{ij}\bar a_{hk}$ for $j\ne k$. The product weight satisfies this.

Not formalized. Polynomial running time, solvability of (CQP′) within additive error $\varepsilon$ (ellipsoid method), and derandomization by conditional probabilities. Theorem 2.10 is formalized as the existence of an outcome in the support of the rounding with the $3/2$ guarantee.

Trivializing formalization ruled out. A bound $\mathbb E\le\tfrac32Z$ for an arbitrary number $Z$ says nothing about schedules. The goal therefore also states that every schedule is feasible for (CQP′) at its own value, so $Z$ is a genuine lower bound on the optimum.

Contributions welcome. A complete development needs:

• linearity of expectation over a finite weight on assignments;
• the computation of Lemma 2.2;
• a positive-semidefiniteness criterion via principal minors or a direct sum-of-squares decomposition of $a^T(D+\operatorname{diag}(c))a$;
• convexity of quadratic forms with PSD matrices.

The rounding calculus and the PSD lemma are reusable for §§3–4 of the same paper. Alternative proofs of Lemma 2.4 are welcome.

Selected references

• M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, Journal of the ACM 48(2), 2001. https://doi.org/10.1145/375827.375840
• W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3, 1956. https://doi.org/10.1002/nav.3800030106
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46, 1990. https://doi.org/10.1007/BF01585745
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Mathematics of Operations Research 22(3), 1997. https://doi.org/10.1287/moor.22.3.513
• A. S. Schulz, M. Skutella, Scheduling unrelated machines by randomized rounding, SIAM Journal on Discrete Mathematics 15(4), 2002. https://doi.org/10.1137/S0895480199357078
• N. Bansal, A. Srinivasan, O. Svensson, Lift-and-round to improve weighted completion time on unrelated machines, STOC 2016. https://doi.org/10.1145/2897518.2897572

Motivation

Bounds on the upper tail $P(S_n\ge x)$ of a sum $S_n=X_1+\dots+X_n$ of independent random variables are used throughout probability, statistics, queueing and risk theory: they control ruin probabilities, the error of empirical averages, and the size of the largest deviations of random walks. The classical exponential inequalities (Bernstein, Hoeffding, Bennett) require the summands to be bounded or to have finite exponential moments of a fixed order. The polynomial bounds of Fuk and Nagaev only require finite power moments, at the price of a power-law rate.

Between these two regimes lie summands whose right tails decay like $e^{-g(u)}$ for a function $g$ growing faster than a logarithm — Weibull-type and other subexponential or superexponential tails. For such summands the natural size parameter is not a power moment but a generalized moment $b_{gj}=E[e^{g(X_j)};X_j\ge 0]$. Section 2 of S. V. Nagaev's survey Large deviations of sums of independent random variables (Ann. Probab. 7, 1979, doi:10.1214/aop/1176994938) develops bounds on $P(S_n\ge x)$ in terms of these quantities. Theorem 2.5 of that section, attributed to S. K. Sakoyan and Nagaev, treats the case where $g$ has a positive nondecreasing derivative — the case $\liminf_{x\to\infty}g(x)/x>0$ of the paper — and gives a bound in product form whose exponential order is $e^{-ng(x/n)}$.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $X_1,\dots,X_n$ independent real random variables with distribution functions $F_j(u)=P(X_j<u)$. Write

$$S_n=X_1+\dots+X_n .$$

Let $g:\mathbb R\to\mathbb R$ be differentiable with a derivative $g'$ that is positive and nondecreasing; in particular $g$ is convex and increasing, and $g(u)\to\infty$ as $u\to\infty$.

For each summand define the generalized moment

$$b_{gj}=\int_{u\ge 0}e^{g(u)}\,dF_j(u)=E\big[e^{g(X_j)};\,X_j\ge 0\big],$$

and, for a real $s$, the negative-part factor

$$b_j(s)=e^{g(0)}\int_{u<0}e^{g'(s)u}\,dF_j(u)=e^{g(0)}E\big[e^{g'(s)X_j};\,X_j<0\big].$$

The factor $b_j(s)$ is always finite, since its integrand lies in $(0,1]$; $b_{gj}$ may be infinite, and the theorem is meaningful only when every $b_{gj}$ is finite. In Lean these objects are S n X, bg P X g j and bj P X g g' j s in the namespace NagaevLD.GenMoment.

Formalization targets

Goal: Theorem 2.5, (2.44), p. 767

For every $x>0$,

$$P(S_n\ge x)\ \le\ \prod_{j=1}^n\big(b_j(x/n)+b_{gj}\big)\exp\{-ng(x/n)\}.$$

The statement holds for every $n$, every distribution of the summands with finite $b_{gj}$, and every admissible $g$; no constant is hidden.

Milestones

The proof of the paper passes through the following displays, all on pp. 767–768, with $h=g'(x/n)$ where indicated:

1. (2.45) the exponential Chebyshev bound $P(S_n\ge x)\le e^{-hx}\prod_{j}Ee^{hX_j}$ for $h\ge 0$;
2. (2.46) the exact split of $Ee^{hX_j}$ at zero and the bound $Ee^{hX_j}\le\int_{u<0}e^{hu}\,dF_j(u)+b_{gj}\sup_{u\ge 0}e^{hu-g(u)}$;
3. (2.47) for $h=g'(x/n)$, $\sup_{u\ge 0}e^{hu-g(u)}=e^{hx/n-g(x/n)}$;
4. the convexity step $g'(x/n)x/n\ge g(x/n)-g(0)$, hence $e^{hx/n-g(x/n)}\ge e^{-g(0)}$;
5. (2.48) $\int_{u<0}e^{hu}\,dF_j(u)\le\exp\{g(0)+hx/n-g(x/n)\}\int_{u<0}e^{hu}\,dF_j(u)$;
6. the per-factor bound $Ee^{hX_j}\le(b_j(x/n)+b_{gj})\exp\{hx/n-g(x/n)\}$.

Significance

The bound separates the tail of $S_n$ into a product of one-summand quantities. For fixed $n$ and $x\to\infty$ one has $\prod_j(b_j(x/n)+b_{gj})\to\prod_j b_{gj}$, so $P(S_n\ge x)<(1+\varepsilon)\prod_j b_{gj}\,e^{-ng(x/n)}$ for large $x$ (the paper's (2.49)); compared with the elementary lower bound $P(S_n\ge x)\ge\prod_j P(X_j\ge x/n)$ (2.50), this shows the exponential order $e^{-ng(x/n)}$ is the right one when the right tails of the summands are of order $b_{gj}e^{-g}$. The only case where the right side does not depend on $n$ is $g(u)=Tu$, the classical Chernoff regime, of which the theorem is a generalization.

The result is a published theorem with a complete half-page proof; it is not open. As far as a search of the Prove2Me catalogue shows, no part of it has been machine-checked: the catalogue contains single-variable Chernoff bounds (Mathlib's measure_ge_le_exp_mul_mgf) but no bound in terms of generalized moments. The mission produces a formal proof of the theorem and, along the way, reusable statements about tilted truncated moments of independent sums.

Difficulty

Each step of the argument is short; the work is in carrying it through real-valued measure theory. The exponential Chebyshev step requires the moment generating function of a sum of independent variables to factor, which needs the integrability of every $e^{hX_j}$ — a fact that here must be derived from the finiteness of $b_{gj}$ and the bound on $e^{hu-g(u)}$, not assumed. The supremum in (2.46) has to be identified as a maximum attained at $x/n$, which rests on the convexity of $g$ on $[0,\infty)$ obtained from a monotone derivative. Finally the split of $Ee^{hX_j}$ at $0$ must match the definition of $b_{gj}$ exactly: a mismatch at the single point $u=0$ breaks the theorem.

Formalization scope

The summands are X : Fin n → Ω → ℝ on a probability space, each measurable and jointly independent (iIndepFun); index $j$ in Lean is the paper's $j+1$. Integrals $\int\cdot\,dF_j(u)$ over a set of $u$ are written as expectations restricted to the corresponding event, so no distribution functions appear. Probabilities are P.real, and $P(S_n\ge x)$ is P.real {ω | x ≤ S n X ω}.

Committed conventions and disclosed additions:

• $b_{gj}$ over $u\ge 0$. The paper defines $b_{gi}=\int_{0+}^{\infty}e^{g(u)}\,dF_i(u)$ (p. 759), over $u>0$. The proof splits at $0-$ and bounds the whole part on $u\ge 0$ by $b_{gj}$; with the $u>0$ reading the theorem is false (two summands with $P(X_j=1)=0.1$, $P(X_j=0)=0.9$, $g(u)=u$, $x=1$ give $P(S_2\ge 1)=0.19$ against a bound of about $0.027$). The formalization integrates over $u\ge 0$.
• Finiteness of $b_{gj}$ is an explicit integrability hypothesis. The paper treats $b_{gj}$ as a finite factor; Lean's integral of a non-integrable function is $0$, which would turn the bound into a false statement rather than a trivial one. This rules out the trivializing reading in which a junk $b_{gj}=0$ is used.
• Hypotheses on $g$ — differentiability, $g'>0$, $g'$ nondecreasing — are imposed on $[0,\infty)$ only, the region where $g$ and $g'$ are evaluated; the paper's global hypothesis implies them. They also give §2's standing assumption that $g$ is nondecreasing with $g(u)\to\infty$, which is therefore not stated separately.
• Suprema in (2.46)–(2.47) are never real sSup: (2.46) is stated for every upper bound $M$ of $e^{hu-g(u)}$ on $u\ge 0$, and (2.47) as IsGreatest.
• The convexity step is stated with "$\ge$"; the page prints "$>$", which fails for $g(u)=Tu$.
• $n\ge1$ is explicit in the theorem statements, matching the paper's sum $X_1+\dots+X_n$ and avoiding Lean's $x/0=0$ value.
• (2.45) assumes the finiteness of each $Ee^{hX_j}$, which the page takes for granted.
• (2.46) assumes $h\ge0$, as used in the proof, so its negative-part expectation is finite; the finite $b_{gj}$ and an upper bound on $e^{hu-g(u)}$ make its positive part finite.

A complete development needs the factorization of exponential moments of independent sums (available in Mathlib as iIndepFun.mgf_sum), Markov's inequality, splitting a Bochner integral over an event and its complement, and the tangent-line inequality for a function with monotone derivative. Proofs of the milestones, alternative arguments, and lemmas on truncated exponential moments are all welcome.

Selected references

• S. V. Nagaev, Large deviations of sums of independent random variables, Annals of Probability 7(5), 745–789, 1979. doi:10.1214/aop/1176994938
• D. Kh. Fuk and S. V. Nagaev, Probability inequalities for sums of independent random variables, Theory of Probability and Its Applications 16(4), 643–660, 1971. doi:10.1137/1116071
• H. Chernoff, A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations, Annals of Mathematical Statistics 23(4), 493–507, 1952. doi:10.1214/aoms/1177729330

Motivation

The speed at which a finite reversible Markov chain approaches its stationary distribution is controlled by its eigenvalues. For a chain with eigenvalues $1=\beta_0>\beta_1\ge\dots\ge\beta_{m-1}\ge-1$, the distance to stationarity after $n$ steps is governed by $\beta_*^{\,n}$, where $\beta_*=\max(\beta_1,|\beta_{m-1}|)$ (Diaconis and Stroock 1991, Proposition 3). Upper bounds on the second eigenvalue $\beta_1$ are the familiar half of this picture, and they are what Cheeger-type and Poincaré inequalities provide. The other half is the smallest eigenvalue $\beta_{\min}=\beta_{m-1}$: a chain whose smallest eigenvalue is close to $-1$ oscillates almost periodically and mixes slowly whatever $\beta_1$ is. A chain is aperiodic exactly when $\beta_{\min}>-1$, but that qualitative fact gives no rate.

Diaconis and Stroock's paper gives geometric bounds for both ends of the spectrum, expressed through systems of paths in the graph of the chain. Their bound on $\beta_{\min}$ uses closed paths with an odd number of edges, the combinatorial witnesses of aperiodicity. The paper has been a standard reference for path (canonical-path, multicommodity-flow) methods in the analysis of Markov chain Monte Carlo since its publication.

Timeline:

• 1988–1989, Jerrum and Sinclair: conductance (Cheeger-type) bounds on $\beta_1$ for chains on combinatorial structures.
• 1991, Diaconis and Stroock: path bounds for $\beta_1$ (Proposition 1, the Poincaré inequality $\beta_1\le1-1/\kappa$) and for $\beta_{\min}$ (Proposition 2, this mission), with the specializations to random walks on graphs (Corollaries 1 and 2).

Setting

Let $X$ be a finite set and $P(x,y)$ the transition matrix of an irreducible Markov chain on $X$, reversible with respect to a probability distribution $\pi$:

$$Q(x,y)=\pi(x)P(x,y)=\pi(y)P(y,x)\qquad(x,y\in X).$$

The operator $(P\varphi)(x)=\sum_yP(x,y)\varphi(y)$ is self-adjoint on $L^2(\pi)$, with inner product $\langle\varphi,\psi\rangle_{L^2(\pi)}=\sum_x\varphi(x)\psi(x)\pi(x)$, so its eigenvalues are real. Write $E(\varphi^2)=\sum_x\varphi(x)^2\pi(x)$ and let $\beta_{\min}$ be the smallest eigenvalue of $P$.

The graph of the chain has vertex set $X$, an edge from $x$ to $y$ when $Q(x,y)>0$, and a self-loop at $x$ when $Q(x,x)>0$. An odd closed path $\sigma_x$ at $x$ is a sequence of edges from $x$ back to $x$, with an odd number of edges, in which no directed edge is traversed twice. Its length is

$$|\sigma_x|_Q=\sum_{e\in\sigma_x}Q(e)^{-1}.$$

A system of odd paths $\Sigma=(\sigma_x)_{x\in X}$ chooses one such path for every point, and its load is

$$\iota=\iota(\Sigma)=\max_e\sum_{\sigma_x\ni e}|\sigma_x|_Q\,\pi(x),$$

the maximum over directed edges $e$ of the weighted length of the paths through $e$ (display (1.7) of the paper).

For the random walk on a graph $G=(X,E)$, $P(x,y)=1/d(x)$ when $\{x,y\}\in E$, with $d(x)$ the degree, and $\pi(x)=d(x)/2|E|$. There $d_*$ is the maximum degree, $\sigma_*$ the largest number of edges of a path in $\Sigma$, and $b_*=\max_e\sharp\{\sigma\in\Sigma:e\in\sigma\}$.

Formalization targets

Goal: Proposition 2

For an irreducible, aperiodic, reversible chain and every system $\Sigma$ of odd closed paths,

$$\beta_{\min}\ge-1+\frac{2}{\iota(\Sigma)}.$$

Milestones (the steps of the paper's proof)

1. The identity (1.8): $\tfrac12\sum_{x,y}(\varphi(x)+\varphi(y))^2Q(x,y)=E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}$.
2. Along an odd closed path $x,y,w,\dots,z,x$: $\varphi(x)=\tfrac12\{(\varphi(x)+\varphi(y))-(\varphi(y)+\varphi(w))+\dots+(\varphi(z)+\varphi(x))\}$.
3. For every $\varphi$: $E(\varphi^2)\le\frac{\iota}{2}\big(E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}\big)$.
4. Every eigenvalue $\beta$ of $P$ satisfies $\beta\ge-1+2/\iota$.

Companions

• Corollary 2. For the random walk on a connected, non-bipartite graph and any system $\Sigma$ of odd paths, $\beta_{\min}\ge-1+\dfrac{2}{d_*\sigma_*b_*}$.
• Remark 1.3. With odd paths $\sigma_{xy}$ for every ordered pair and $\tilde\iota=\max_e\sum_{\sigma_{xy}\ni e}|\sigma_{xy}|_Q\pi(x)\pi(y)$: $\beta_{\min}\ge-1+1/\tilde\iota$.

Significance

Proposition 2 turns aperiodicity into a number. With Proposition 1, which bounds $\beta_1\le1-1/\kappa$ through paths between pairs of points, it bounds the absolute spectral gap $1-\beta_*$ entirely in terms of path geometry, and so bounds the variation distance to stationarity through Proposition 3. Corollary 2 is the form most often applied: for a random walk on a non-bipartite graph, a choice of short odd cycles that do not crowd any single edge certifies that the walk does not oscillate.

Proposition 2 and its corollary are proved in the paper. As far as a search of the platform shows, no machine-checked proof exists. The platform already has the vocabulary (stochastic matrices, stationarity, reversibility, eigenvalues and the $L^2(\pi)$ inner product, from the published Levin–Peres–Wilmer layer) and the qualitative fact that $-1$ is not an eigenvalue of an irreducible aperiodic chain. This mission adds the quantitative bound, the identity (1.8), and the path inequality, all reusable for other path-based eigenvalue estimates.

Difficulty

Each step is elementary, but the bookkeeping is where a proof can go wrong. The Cauchy–Schwarz step is applied along each path separately, and the resulting double sum over points and over the edges of their paths must be exchanged into a sum over edges. That exchange is exact only if each path traverses each directed edge at most once. A path that crosses an edge twice contributes twice, while $\iota$ counts it once. Self-loops are edges here, and the sum over directed edges in the last step must match the sum over ordered pairs $(x,y)$, including $x=y$, in the identity (1.8). The alternating signs work only because the number of edges is odd; an even closed path cancels $\varphi(x)$ instead of doubling it.

The bound is also only as good as the chosen paths: short odd cycles that spread their load over many edges give a small $\iota$, and the choice of $\Sigma$ is part of every application.

Formalization scope

The chain is a real matrix P : Matrix V V ℝ on a Fintype V, with the published predicates IsStochastic, Irreducible, Aperiodic, IsStationary (which includes that $\pi$ is a probability vector) and DetailedBalance. $Q$ is edgeMeasure, the inner product innerPi, eigenvalues IsEigenvalue (a real eigenvalue with a nonzero real eigenfunction). $\beta_{\min}$ is the infimum of the real eigenvalues of $P$, a minimum for a stochastic matrix on a nonempty set.

Paths are vertex lists. A path traverses the directed edges between consecutive vertices, each with $Q>0$. The paper defines $|\sigma_x|_Q$ "by analogy with (1.4)", whose paths may not repeat an edge. For the directed edges of §1C this rule is read as "no directed edge twice". Under the unordered reading a vertex of degree one would have no odd closed path, contradicting the page's remark that such paths always exist for irreducible aperiodic chains. $\iota$ is a real supremum over the finite set of directed edges with $Q>0$, and it is $0$ only when there is no edge. A system of odd paths on a nonempty set excludes that case, so the bound is never reduced to $\beta_{\min}\ge-1$ by $2/0=0$. The system $\Sigma$ is a universally quantified hypothesis of every statement, never an existential one. No milestone assumes the inequality of milestone 3 or the identity (1.8) as a hypothesis. No assumption $|X|\ge2$ is made.

Milestones 3 and 4 do not assume aperiodicity: the existence of an odd path system implies it. The identity (1.8) assumes only stochasticity and stationarity. Corollary 2 assumes only that the graph is connected and not 2-colorable; the chain properties follow from these. In Corollary 2, $b_*$ counts paths through a directed edge, which is at most the count through the unordered edge, so the stated bound implies the one with the unordered count. Only the first half of Remark 1.3 is stated; its second half needs Proposition 1's quantity, which belongs to another mission of the series.

Contributions welcome: proofs of the milestones in order, a general Cauchy–Schwarz-along-paths lemma shared with the Poincaré inequality, and the existence of odd path systems for irreducible aperiodic chains.

Selected references

• P. Diaconis and D. Stroock, Geometric bounds for eigenvalues of Markov chains, Ann. Appl. Probab. 1(1):36–61, 1991. https://doi.org/10.1214/aoap/1177005980
• A. Sinclair and M. Jerrum, Approximate counting, uniform generation and rapidly mixing Markov chains, Inform. and Comput. 82(1):93–133, 1989. https://doi.org/10.1016/0890-5401(89)90067-9
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (2nd ed. 2017). https://doi.org/10.1090/mbk/107

Motivation

How fast a finite Markov chain forgets its starting point is the central quantitative question in the analysis of Monte Carlo algorithms, card shuffling and random walks on groups. The classical tool is the spectral gap $\lambda$, which controls convergence in $\ell^2(\pi)$ but loses a factor $1/\pi(x)$ when converted into a bound for a chain started at a point. Diaconis and Saloff-Coste (Ann. Appl. Probab. 6 (1996) 695–750) brought the logarithmic Sobolev constant $\alpha$, introduced by Gross for Gaussian measures (Amer. J. Math. 97 (1975)), into the study of finite chains, and showed that it gives sharper mixing bounds in many examples.

The entropy route to ergodicity is the cleanest consequence of a log-Sobolev inequality: the relative entropy of the chain's law with respect to stationarity decays exponentially at rate $2\alpha$, and at rate $4\alpha$ for reversible chains. The paper notes that the reversible case is contained in Bakry's Saint-Flour lectures (Lecture Notes in Math. 1581, 1994) and Stroock's notes on Gibbs states (Lecture Notes in Math. 1563, 1993), and that Miclo (preprint, 1995) treated the nonreversible case.

Setting

Let $\mathcal X$ be a finite set and $K$ a Markov kernel: $K(x,y)\ge0$ and $\sum_y K(x,y)=1$. Let $\pi$ be an invariant probability, $\sum_x\pi(x)K(x,y)=\pi(y)$, with $\pi(x)>0$ for every $x$. Functions act on the right, $Kf(x)=\sum_yK(x,y)f(y)$, and $\langle f,g\rangle=\sum_xf(x)g(x)\pi(x)$ is the inner product of $\ell^2(\pi)$, with norms $\|f\|_p=(\sum_x|f(x)|^p\pi(x))^{1/p}$. The chain is reversible if $\pi(x)K(x,y)=\pi(y)K(y,x)$ for all $x,y$.

The continuous-time heat semigroup is

$$H_t=e^{-t(I-K)}=e^{-t}\sum_{n\ge0}\frac{t^n}{n!}K^n,$$

acting on functions by $H_tf(x)=\sum_yH_t(x,y)f(y)$ and on probability measures by $\mu H_t(y)=\sum_xH_t(x,y)\mu(x)$. The row $H_t^x=H_t(x,\cdot)$ is the law at time $t$ of the chain started at $x$.

The Dirichlet form is $\mathcal E(f,g)=\langle (I-K)f,g\rangle$; it is bilinear but not symmetric unless the chain is reversible. With

$$\mathcal L(f)=\sum_x|f(x)|^2\log\frac{|f(x)|^2}{\|f\|_2^2}\,\pi(x),$$

the log-Sobolev constant is

$$\alpha=\inf\Big\{\frac{\mathcal E(f,f)}{\mathcal L(f)}:\mathcal L(f)\ne0\Big\}.$$

The relative entropy of a probability $\mu$ is $\mathrm{Ent}_\pi(\mu)=\sum_x\mu(x)\log\frac{\mu(x)}{\pi(x)}$, and the total variation distance is $\|\mu-\pi\|_{TV}=\sup_{A\subset\mathcal X}|\mu(A)-\pi(A)|$.

Formalization targets

Goal: Theorem 3.6 (p. 722)

For every probability measure $\mu$ on $\mathcal X$,

$$\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-2\alpha t},\qquad t>0,$$

and, if $(K,\pi)$ is reversible,

$$\mathrm{Ent}_\pi(\mu H_t)\le\mathrm{Ent}_\pi(\mu)\,e^{-4\alpha t},\qquad t>0.$$

Milestones

1. §2.1, Remarks (ii), p. 702: if $\mu=f\pi$ then $\mu H_t$ has density $H_t^*f$, where $H_t^*$ is the semigroup of the adjoint kernel $K^*(x,y)=K(y,x)\pi(y)/\pi(x)$.
2. Lemma 2.5, second part, p. 707: $\partial_t\,\mathrm{Ent}_\pi(H_tf)|_{t=0}=-\mathcal E(f,\log f)$.
3. Lemma 2.7, p. 708: $\mathcal E(\log f,f)\ge2\,\mathcal E(\sqrt f,\sqrt f)$, and $\ge4\,\mathcal E(\sqrt f,\sqrt f)$ for reversible chains.
4. §3.3, p. 722: for $f\ge0$ with $\|f\|_2=1$ and $\mu=f^2\pi$, $\mathcal L(f)=\mathrm{Ent}_\pi(\mu)$.
5. (2.8), p. 710: $2\|\mu-\pi\|_{TV}^2\le\mathrm{Ent}_\pi(\mu)\le\|\mu-\pi\|_{TV}+\tfrac12\|\mu/\pi-1\|_{\pi,2}^2$.

Companion: (3.3) (p. 723)

For an irreducible chain, every $x$ and $t>0$,

$$2\|H_t^x-\pi\|_{TV}^2\le\Big(\log\frac1{\pi(x)}\Big)e^{-2\alpha t},$$

with $2\alpha$ replaced by $4\alpha$ for reversible chains.

Significance

Theorem 3.6 turns a single functional inequality into a convergence statement valid for every initial law, with no spectral assumption and no reversibility in the first half. Through Pinsker's inequality it gives (3.3), whose prefactor $\log(1/\pi(x))$ replaces the factor $1/\pi(x)$ of the spectral bound $4\|H_t^x-\pi\|_{TV}^2\le\pi(x)^{-1}e^{-2\lambda t}$. When $\pi(x)$ is exponentially small in the size of the problem, as for random walks on large groups or product spaces, $\log(1/\pi(x))$ is polynomial where $1/\pi(x)$ is exponential, and the time needed to make the bound small drops accordingly. This is the mechanism behind the sharp mixing bounds the paper derives from $\alpha$.

The results are proved in the paper and are classical; they are not, to our knowledge, formalized. The platform has measure-theoretic statements of Pinsker's inequality and the published finite Markov chain vocabulary of Levin–Peres–Wilmer (stochastic matrices, stationarity, total variation, the heat kernel), but nothing about log-Sobolev constants of finite chains, the entropy derivative along a Markov semigroup, or entropy decay. A formal development provides the entropy layer of the finite-chain theory: the adjoint semigroup, the dissipation identity, the comparison of $\mathcal E(\log f,f)$ with $\mathcal E(\sqrt f,\sqrt f)$, and Pinsker's inequality in the encoding used by the mixing-time library.

Difficulty

The statement is about measures, while the natural quantities to differentiate are densities with respect to $\pi$, and for a nonreversible chain the density of $\mu H_t$ evolves under the adjoint semigroup, not under $H_t$. The Dirichlet form is not symmetric, so the order of its arguments matters at every step, and the improvement from $2\alpha$ to $4\alpha$ holds only under reversibility.

The obvious first idea, differentiating $\mathrm{Ent}_\pi(\mu H_t)$ term by term, meets $\log 0$ wherever the density vanishes. The initial law may be a point mass, and for a reducible chain the density can stay zero at positive times. The argument must therefore handle the boundary $t=0$ and the degenerate laws separately from the smooth interior. The constant $\alpha$ is defined as an infimum over all functions, with no claim that it is attained or positive.

Formalization scope

The state space is a Fintype with decidable equality, $K$ is a real matrix with the published predicate MarkovMixing.IsStochastic, $\pi$ satisfies MarkovMixing.IsStationary K π and $\pi(x)>0$ for all $x$, and reversibility is MarkovMixing.DetailedBalance K π. $H_t$ is the published MarkovMixing.heatKernel K t (the Poisson series), the adjoint kernel is MarkovMixing.timeReversal K π, and total variation is MarkovMixing.tvDist. Time is real, and the decay statements are for $t>0$.

The local definitions are $\mathcal E(f,g)=\sum_x(f(x)-Kf(x))g(x)\pi(x)$, the norms $\|f\|_p$, $\mathcal L$, $\alpha$ as a real infimum over the ratios with $\mathcal L(f)\ne0$, $\mathrm{Ent}_\pi(\mu)$, and $\mu H_t$ as the row vector $\mu\,H_t$. Lean's Real.log 0 = 0 implements $0\log0=0$. The goal does not assume irreducibility: it is true for every stochastic $K$ with a positive invariant probability, and a reducible chain has $\alpha=0$. The companion (3.3) keeps irreducibility, the standing assumption of Section 3. In Lemmas 2.5 and 2.7 the paper's $f\ge0$ is strengthened to $f>0$, because $\log f$ is $-\infty$ at a zero of $f$ on the page and $0$ in Lean.

Several encodings would make the goal trivially true and are ruled out. $\alpha$ is not assumed positive. $\mu$ is a probability, since for $\mu=2\pi$ the entropy is a positive constant in $t$. $\pi$ is invariant and positive, so $\mu/\pi$ is meaningful. The eigenvalue-based MarkovMixing.spectralGap is not used. Applying $H_t$ to $\mu$ as a function, $H_t\mu$, is not the same as $\mu H_t$ for a nonreversible chain.

A complete development needs: termwise differentiation of the heat-kernel series and the semigroup property $\partial_tH_t=(K-I)H_t$; the adjoint identity for $H_t$; elementary convexity inequalities for $\log$ and $\sqrt{\cdot}$; the symmetric form of $\mathcal E$ for reversible chains; Pinsker's inequality on a finite set; and a scalar Grönwall lemma. The heat-kernel calculus and Pinsker's inequality in the MarkovMixing.tvDist encoding are reusable by the other missions of this series and by any mixing-time development. Proofs of individual milestones are welcome independently of the goal.

Selected references

• P. Diaconis and L. Saloff-Coste, Logarithmic Sobolev inequalities for finite Markov chains, Ann. Appl. Probab. 6 (1996), 695–750. https://doi.org/10.1214/aoap/1034968224
• L. Gross, Logarithmic Sobolev inequalities, Amer. J. Math. 97 (1975), 1061–1083. https://doi.org/10.2307/2373688
• D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, 2nd ed., American Mathematical Society, 2017. https://doi.org/10.1090/mbk/107

Motivation

The multi-armed bandit problem with discounted rewards asks how to allocate effort among $n$ independent projects, only one of which can be worked on at a time, when the project worked on evolves randomly and the others stay frozen. It models job scheduling, research planning, search, and sequential clinical experimentation. Gittins and Jones showed in 1974 that the problem has an index solution: each state of each project has a number, computed from that project alone, and it is optimal always to work on the project whose current state has the largest number. The result turns an $n$-dimensional dynamic program into $n$ one-dimensional computations.

Several proofs followed, each with its own model and its own definition of the index:

• Gittins and Jones (1974) and Gittins (1979): the original interchange proofs, with the index as a supremum over stopping times of a reward-to-time ratio.
• Whittle (1980): a proof through the retirement option and the dynamic-programming equation of the multi-armed problem.
• Varaiya, Walrand and Buyukkoc (1985): the largest-remaining-index algorithm for finite-state Markov bandits, which computes the indices by removing states one at a time.
• Weber (1992): the "prevailing charge" proof.
• Tsitsiklis (1994): the short proof formalized here, for semi-Markov bandits with finite state spaces, by induction on the total number of states, with the indices produced by an index algorithm of the largest-remaining-index type.

Setting

There are $n\ge1$ bandit processes. Bandit $i$ has a finite nonempty state space $\mathcal X_i$, and $\mathcal X=\mathcal X_1\cup\cdots\cup\mathcal X_n$ is their disjoint union. When bandit $i$ at state $x\in\mathcal X_i$ is played, a random reward $R(x)$ is received, the bandit is busy for a random time $T(x)\ge0$, and it then moves to a random state $Y(x)\in\mathcal X_i$; the other bandits do not move. The joint law of $(T(x),R(x),Y(x))$ depends only on $x$, and different plays are independent.

A policy is a map $\pi:\mathcal X_1\times\cdots\times\mathcal X_n\to\{1,\dots,n\}$: at time zero and at every play completion time it chooses the bandit to play from the current states. With $t_i$ the start time and $R_i$ the reward of the $i$-th play and a discount rate $\beta>0$, the expected discounted reward from the initial joint state $z$ is

$$J_\pi(z)=\mathbb E\Big[\sum_{i=1}^{\infty}R_i e^{-\beta t_i}\Big].$$

A policy is optimal if it maximizes $J_\pi(z)$ for every initial state $z$. A priority rule is a policy for which some ordering of $\mathcal X$ makes it always play the bandit whose current state is ordered highest.

The reward rate of a state is

$$r(x)=\frac{\mathbb E[R(x)]}{\mathbb E\big[\int_0^{T(x)}e^{-\beta t}\,dt\big]}. \tag{2.1}$$

Reducing bandit $i^*$ by removing a state $s^*$ merges every play that ends in $s^*$ with the following run of plays at $s^*$ into one composite play, whose reward rate is $\hat r(x)$ of (2.3). The index algorithm repeatedly picks a state $s^*$ of maximal current rate, sets its index $\gamma(s^*)$ to that rate, and reduces its bandit by removing $s^*$ (or removes the bandit if $s^*$ was its last state).

Formalization targets

Goal: Theorem 2.2

Let $\gamma$ be the indices of a run of the index algorithm. Then every priority rule whose ordering satisfies

$$\gamma(y)<\gamma(x)\ \Longrightarrow\ y \text{ is ordered below } x$$

is optimal. Ties in $\gamma$ may be ordered either way, and the run may break ties in its own choices arbitrarily.

Milestones, in the order the proof uses them

1. (2.2), the interchange inequality $\mathbb E\big[(1-e^{-\beta\tau})\int_0^{T(s^*)}r(s^*)e^{-\beta t}dt\big]\ge\mathbb E\big[(1-e^{-\beta T(s^*)})\int_0^{\tau}\bar r(t)e^{-\beta t}dt\big]$ when $\bar r\le r(s^*)$.
2. Lemma 2.1: if $r(s^*)=\max_{x}r(x)$, some optimal policy always plays bandit $i^*$ when it is at $s^*$.
3. Reduction step: optimizing within the policies giving $s^*$ top priority is a bandit problem with one state fewer, the reduced bandit with rates (2.3).
4. Theorem 2.1: some priority rule is optimal.
5. Pick-order optimality: a priority rule that orders the states as a run of the index algorithm picks them is optimal.
6. Index monotonicity: along a run, $\gamma(s^*)\ge\gamma(q^*)$ for consecutive picks $s^*,q^*$.
7. Picked-before characterization: $x$ can be picked before $y$ (in a run with the same indices) if and only if $\gamma(x)\ge\gamma(y)$.

Significance

The theorem shows that the optimal priority order is determined by numbers that, by the reduction formulas, depend only on the statistics of each bandit separately. It is the basis of index policies in scheduling (the $c\mu$ rule and its semi-Markov generalizations), of Klimov's problem and of branching bandits, which the paper's Section 3 obtains by modifying the same argument.

The result has been proved many times, but not in this generality on Prove2Me. The platform has a discrete-time Gittins index theorem for arms sharing one transition kernel and one reward function, with the index defined as a stopping-time supremum. This mission adds semi-Markov dynamics with random play durations and continuous discounting, heterogeneous finite bandits, priority rules, and the index algorithm as the definition of the index. A complete development would also give a machine-checked proof of correctness of a state-elimination algorithm for computing Gittins indices.

Difficulty

Lemma 2.1 compares an optimal stationary policy with a modified policy that is not stationary, and closes the gap by the optimality of stationary policies, which itself requires the dynamic-programming theory of discounted semi-Markov decision problems with finite state spaces. The reduction step requires an exact identification of the values of all top-priority policies with values in a different problem whose plays are composite and may never end. Theorem 2.1 is an induction over a family of problems with shrinking state spaces that are no longer raw semi-Markov bandits. Theorem 2.2 adds ties: a priority order compatible with the indices need not be the order of the given run, and one needs another run with the same indices.

Formalization scope

• Bandits are indexed by Fin n ($0,\dots,n-1$), with $n\ge1$ and each state type finite and nonempty. $\mathcal X$ is the sigma type Σ i, X i, disjoint by construction.
• The law of $(T(x),R(x),Y(x))$ is a probability measure on $\mathbb R\times\mathbb R\times\mathcal X_i$ with $T\ge0$ almost surely and $R$ integrable. The model also assumes $\mathbb P(T(x)>0)>0$, which the page leaves implicit: it makes the denominator of (2.1) nonzero.
• $J_\pi$ is computed from the moments $\mathbb E[R(x)]$ and $D(x,y)=\mathbb E[e^{-\beta T(x)};Y(x)=y]$: it is the limit of the expected discounted reward of the first $k$ plays, given by the first-step recursion. No path space is constructed. The row sums of $D$ are below $1$, so the limit exists; it never mentions rates, indices or reductions.
• Policies are the paper's stationary deterministic maps of the current joint state, and optimality is within that class, for every initial state. An ordering of $\mathcal X$ is an injective ranking into $\mathbb N$.
• The reduced bandit is given by explicit formulas for its expected discounted reward, discounted duration and discounted transition data. These make the page's "transition probabilities are suitably modified" concrete, and the reduced rate is (2.3). Removing a bandit is the reduction of its last state.
• The index is that of any run of the index algorithm, with arbitrary tie choices.

A formalization in which the value of a policy is defined through rates or indices, or in which $\gamma$ is any function compatible with some order rather than the output of the algorithm, would make the goal trivial or empty; both are excluded by the definitions above.

Needed infrastructure: the convergence of the $k$-play values and the first-step (Bellman) equation for $J_\pi$; existence of an optimal stationary policy for finite discounted semi-Markov problems; the value identity for composite plays. The last two are reusable for any finite semi-Markov decision problem. Proofs of individual milestones, alternative arguments (Weber's prevailing charge, the retirement formulation), and the separability statement of p. 198 ("the index algorithm can be carried out separately for each different bandit") are welcome.

Selected references

• J. N. Tsitsiklis, A Short Proof of the Gittins Index Theorem, Annals of Applied Probability 4(1) (1994), 194–199.
• J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 1974, 241–266.
• J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
• P. Whittle, Multi-armed bandits and the Gittins index, J. Roy. Statist. Soc. Ser. B 42 (1980), 143–149. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
• P. P. Varaiya, J. C. Walrand and C. Buyukkoc, Extensions of the multiarmed bandit problem: the discounted case, IEEE Trans. Automat. Control 30 (1985), 426–439. https://doi.org/10.1109/TAC.1985.1103989
• R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4) (1992), 1024–1033. https://doi.org/10.1214/aoap/1177005588

Why linear suprema arise

A family of linear forms turns independent observations into a single random maximum. Examples include the largest value of a collection of statistical scores and the norm of a random vector sum, which can itself be expressed through the continuous dual of a normed space. A bound for each form separately does not automatically control the supremum over an infinite family. Talagrand's 1995 paper gives a concentration inequality in which the coefficient scale, rather than the number of forms, controls the deviation Talagrand 1995, §8.1. The Banach-space consequence in Chapter 13 applies the same principle to norms of vector sums Talagrand 1995, Theorem 13.2.

The two results have a direct relationship: the norm of a vector is the supremum of its evaluations by continuous linear functionals of norm at most one. The formalization therefore gives a setting in which a general real-valued supremum theorem and a vector-valued corollary can be audited together. It also tests whether the concentration statement remains faithful when the family of forms is infinite and the coordinate laws differ.

The random supremum and its scale

Fix a finite number $N$ of coordinates and a nonempty family $\mathcal F\subseteq\mathbb R^N$ of coefficient vectors $\alpha=(\alpha_i)_{i=1}^N$. The coefficients may have either sign. Write $\|\alpha\|_2=(\sum_i\alpha_i^2)^{1/2}$, and let $\sigma=\sup_{\alpha\in\mathcal F}\|\alpha\|_2$. The mission treats the case in which this coefficient scale is finite and positive. Let $X_i$ be independent real random variables, with an individual interval $[r_i,r_i+1]$ containing each $X_i$ almost surely. The center $r_i$ and the law of $X_i$ may vary with $i$. The object of interest is

$$Z=\sup_{\alpha\in\mathcal F}\sum_{i=1}^N\alpha_iX_i.$$

A median $M$ of $Z$ means that both $P(Z\le M)$ and $P(Z\ge M)$ are at least $1/2$. This definition permits more than one median and makes no choice among them. With a bounded coefficient family and bounded coordinates, the supremum is finite for each input. The mission also assumes that $Z$ is measurable, because an uncountable supremum of measurable functions need not be measurable automatically. These are the mathematical conditions needed to give the displayed probability its ordinary meaning.

The supporting observation uses Talagrand's convex-hull distance. For a set $A$ of coordinate tuples and a point $x$, form the binary vectors $s$ for which there is some $y\in A$ such that every coordinate with $s_i=0$ agrees between $x$ and $y$. Let $V_A(x)$ be their convex hull in $\mathbb R^N$. The distance $f_c(A,x)$ is the Euclidean distance from zero to $V_A(x)$. If $A$ is empty, this distance is $+\infty$. This convention preserves the intended meaning of a distance to an empty target Talagrand 1995, §4.1.

Formalization targets

For $x\in[0,1]^N$, put $Z_r(x)=\sup_{\alpha\in\mathcal F}\sum_i\alpha_i(r_i+x_i)$ and $A(a)=\{y\in[0,1]^N:Z_r(y)\le a\}$. The first milestone is Eq. (8.1.3): if $A(a)$ is nonempty, then for every $\alpha\in\mathcal F$ some $y\in A(a)$ has disagreement set $I=\{i:y_i\ne x_i\}$ with

$$\sum_{i\in I}|\alpha_i|\le\|\alpha\|_2\,f_c(A(a),x)\le\sigma f_c(A(a),x).$$

The second milestone is the deterministic observation in Eq. (8.1.2):

$$Z_r(x)\le a+\sigma f_c(A(a),x).$$

The goal, Theorem 8.1.1, asserts that every median $M$ of $Z$ and every $u>0$ satisfy

$$P(|Z-M|\ge u)\le 4\exp\!\left(-\frac{u^2}{4\sigma^2}\right).$$

The third milestone is Theorem 13.2. For vectors $v_i$ in a real Banach space $W$, define the weak variance scale $\sigma_W=(\sup_{w^*\in W^*,\,\|w^*\|\le1}\sum_i w^*(v_i)^2)^{1/2}$. If the independent real variables $Y_i$ satisfy $|Y_i|\le1$, the theorem bounds deviations of $S=\|\sum_iY_iv_i\|$ from any median $M$:

$$P(|S-M|\ge t\sigma_W)\le4\exp(-t^2/16),\qquad t>0.$$

The statement is made for $\sigma_W>0$. With $\sigma_W=0$, the displayed event has threshold zero and probability one, while the right side falls below one for large $t$; the printed inequality therefore needs that qualification Talagrand 1995, p. 198.

What the results provide

Theorem 8.1.1 controls a supremum using only the largest Euclidean norm of its coefficient vectors. Its statement does not charge a factor for the cardinality of $\mathcal F$, so it applies equally to a finite collection and to an infinite measurable supremum. The coordinatewise interval condition allows different distributions and different centers. Theorem 13.2 converts the same concentration scale into a statement about Banach-space vector sums, where the dual unit ball supplies the coefficient family Talagrand 1995, pp. 156, 198.

Both results are proved in the paper. The work here is to formalize their exact statements and the distance interface used between them. The reusable pieces are the median convention, an extended-valued convex distance on arbitrary product spaces, a measurable supremum over a general set of coefficient vectors, and the weak variance scale for Banach-space vectors. None of the two claimed concentration inequalities is treated as already machine checked by this mission.

The difficult point

For a single fixed vector $\alpha$, bounded-coordinate concentration gives information about $\sum_i\alpha_iX_i$. Applying that estimate to every member of $\mathcal F$ and taking a union would introduce a dependence on the number of vectors. It would also give no useful bound for a genuinely infinite family without additional covering information. Talagrand's target avoids a cardinality term, so a direct collection of fixed-form estimates does not establish the stated result Talagrand 1995, §8.1.

The deterministic distance statement presents a second issue for formalization. Its set $A(a)$ can be empty, and the paper's distance then has value $+\infty$. A real-valued infimum with a default value at the empty set would erase that distinction. The exact Euclidean norm also matters: the usual norm on a Lean function space need not be the paper's $\ell^2$ norm. These choices affect the mathematical meaning of the milestone before any concentration argument begins.

Formalization scope

Coordinates are indexed by Fin N, corresponding to the paper's indices $1,\ldots,N$. The independent observations live on the canonical product of their individual real-valued laws. Each law gives probability one to its own interval $[r_i,r_i+1]$; identical distribution is not assumed. The coefficient family is a set, not a finite list. Its nonemptiness, finite norm supremum and positive scale are explicit. Measurability of the real supremum is also explicit, following the paper's convention of ignoring measurability questions Talagrand 1995, pp. 81–82.

The mismatch vectors and their convex hull are defined over the whole underlying product type. The distance is an extended nonnegative real infimum of Euclidean lengths, so an empty target has distance $+\infty$. Eq. (8.1.2) uses extended arithmetic for the positive part of $Z_r(x)-a$, which keeps the empty-sublevel case meaningful. The probability bounds retain the paper's constants $4$, $4\sigma^2$, and $16$. A zero coefficient scale cannot be used to make the goal a vacuous division-by-zero statement; the Banach result likewise requires a positive weak variance scale.

The mission welcomes proofs of the two concentration statements, the deterministic distance observation, and supporting facts about the supremum's finiteness and measurability. General lemmas about product measures, medians, extended distances, and dual norms would be useful beyond this chapter. The statements do not restrict $\mathcal F$ to a finite or countable subset, so a proof must address the general family under the explicit measurability assumption.

Selected references

• Michel Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publications Mathématiques de l'IHÉS 81 (1995), 73–205. DOI: 10.1007/BF02699376.