All missions

Is the $d\sqrt{n}$ regret of LinUCB (Mission X) an artifact of the algorithm or a law of nature? Chapters 24–25 of Lattimore–Szepesvári prove it is essentially unimprovable. On the unit ball there is a parameter $\theta$ with $\|\theta\|_2^2 = d^2/(48n)$ forcing $R_n \ge \frac{d\sqrt{n}}{16\sqrt{3}}$ — the goal theorem — and the hypercube gives the same $\Omega(d\sqrt{n})$ rate. The asymptotic chapter is more striking still: for fixed finite action sets, the instance-optimal constant $c(\mathcal{A},\theta)$ is characterized by an allocation program, and optimism itself is provably suboptimal — LinUCB and Thompson sampling cannot achieve it, because exploration must sometimes deliberately play actions optimism would never touch. These lower bounds define the targets for the entire linear-bandit literature.

What if the rewards are not random at all, but chosen by an adversary who knows your algorithm? Remarkably, a randomized learner can still compete with the best fixed arm in hindsight. Chapters 11–12 of Lattimore–Szepesvári develop the adversarial $k$-armed bandit: rewards $x_{ti} \in [0,1]$ are an arbitrary fixed matrix, the learner samples $A_t \sim P_t$, and regret is measured against $\max_i \sum_t x_{ti}$. The exponential-weights algorithm Exp3, fed by importance-weighted loss estimates $\hat X_{ti} = 1 - \mathbb{1}\{A_t = i\}(1 - X_t)/P_{ti}$, achieves $R_n \le \sqrt{2nk\log k}$ — the goal theorem. The companion Exp3-IX, which deliberately biases its estimator, upgrades this to a bound holding with high probability rather than only in expectation. These results are the foundation of all adversarial online learning with partial feedback.

Motivation

Strong subadditivity of the von Neumann entropy is the basic inequality of quantum information theory: most entropy inequalities used in quantum Shannon theory, the data-processing inequality for quantum mutual information, and many capacity converses rest on it (Nielsen–Chuang, ch. 11). This mission formalizes the route to it presented by M. A. Nielsen and D. Petz in A simple proof of the strong subadditivity inequality (arXiv:quant-ph/0408130v3), an expository account of Petz's proof through the relative modular operator and the operator convexity of $-\ln$.

Timeline.

• 1973: Lieb proves the concavity theorems (Adv. Math. 11); Lieb and Ruskai derive strong subadditivity from them (J. Math. Phys. 14).
• 1975: Lindblad proves monotonicity of the relative entropy under completely positive maps, after strong subadditivity (Commun. Math. Phys. 40).
• 1985–1986: Narnhofer and Thirring develop a relative-entropy approach (Fizika 17, 1985); independently, Petz gives the modular-operator proof that this mission follows (Rep. Math. Phys. 23).
• 2005: Nielsen and Petz publish the finite-dimensional exposition (Quantum Inf. Comput. 5).

Setting

A finite quantum system $A$ has a finite set of basis labels; an operator on $A$ is a complex $A\times A$ matrix, and $M(A)$ is the space of them. A density matrix is a positive semidefinite matrix of trace $1$. Operators on a composite system $AB$ are indexed by pairs $(a,b)$, and the partial trace $\operatorname{tr}_B$ produces the reduced density matrix $\rho_A=\operatorname{tr}_B\rho_{AB}$.

The von Neumann entropy is $S(\rho)\equiv-\operatorname{tr}(\rho\ln\rho)$ and the relative entropy is

both with the natural logarithm. $I_A/d_A$ is the maximally mixed state of $A$, $d_A$ its dimension.

$M(A)$ carries the Hilbert–Schmidt inner product $\langle X,Y\rangle\equiv\operatorname{tr}(X^\dagger Y)$. For invertible density matrices $\rho,\sigma$ the relative modular operator is the linear map $\Delta(X)=\sigma X\rho^{-1}$ on $M(A)$, the product of left multiplication $\mathcal L(X)=\sigma X$ and right multiplication $\mathcal R(X)=X\rho^{-1}$. It is strictly positive, and $\ln(\Delta)$ is defined by diagonalizing $\Delta$ and taking the logarithm of its eigenvalues. On a composite system, $\Delta_{AB}$ and $\Delta_A$ are built from $(\rho_{AB},\sigma_{AB})$ and from $(\rho_A,\sigma_A)$. The map $\mathcal U:M(A)\to M(AB)$ is

Formalization targets

Goal: strong subadditivity (1), p. 1

For every density matrix $\rho_{ABC}$ of a three-component system,

The goal is the existing Open platform theorem QAlgorithms.Papers.Independent.Gap48.P20.strongSubadditivity, which states $0\le H(CB)+H(RB)-H(B)-H(CRB)$ for every density matrix on $C\times(R\times B)$. With $A\mapsto C$, $C\mapsto R$ this is (1); it uses bits, which differ from nats by the positive factor $1/\ln2$.

Milestones

• Lemma 1 (p. 3). $f(x)=-\ln x$ is operator convex. Existing Proved theorem TroppMatrixConcentration.ch8_log_operator_concave.
• Lemma 2 (p. 3). For $f$ operator convex and an isometry $U$, $f(U^\dagger XU)\le U^\dagger f(X)U$. Existing Proved theorem TroppMatrixConcentration.ch8_jensen_isometric_compression.
• (7), p. 4. For invertible $\rho,\sigma$: $S(\rho\|\sigma)=\langle\rho^{1/2},-\ln(\Delta)(\rho^{1/2})\rangle$.
• Properties (1)–(3) of $\mathcal U$, pp. 4–5. $\mathcal U^\dagger\Delta_{AB}\mathcal U=\Delta_A$, $\mathcal U(\rho_A^{1/2})=\rho_{AB}^{1/2}$, $\mathcal U^\dagger\mathcal U=\mathcal I_A$, together with the stated adjoint $\mathcal U^\dagger(Y)=\operatorname{tr}_B(Y\rho_{AB}^{1/2}(\rho_A^{-1/2}\otimes I_B))$.
• (4), p. 2. Monotonicity, for invertible $\rho_{AB},\sigma_{AB}$:

• (5), p. 2. For every $\rho_{AB}$: $S(B|A)=\ln d_B-S(\rho_{AB}\|\rho_A\otimes I_B/d_B)$, with $S(B|A)=S(\rho_{AB})-S(\rho_A)$. The page prints the denominator as $d_b$; it is $d_B$.
• (6), p. 2. For invertible $\rho_{ABC}$:

Significance

Strong subadditivity is equivalent to monotonicity of the relative entropy under partial trace, to the nonnegativity of quantum conditional mutual information, and to the data-processing inequality for quantum mutual information. A machine-checked proof makes all of these available to formal developments of quantum Shannon theory, which currently have to assume strong subadditivity.

On the platform the goal has been Open, while the two operator-convexity lemmas of this proof are already Proved in the Tropp matrix-concentration series. This mission supplies the remaining steps of Petz's route as separate targets: the modular-operator formula (7), the isometry $\mathcal U$ with its three properties, monotonicity (4) for invertible states, and the identities (5)–(6) that connect monotonicity to strong subadditivity. Each is a known result; none of them, and neither strong subadditivity nor monotonicity of the relative entropy, has a machine-checked proof on the platform.

Difficulty

The density matrices in $S(\rho\|\sigma)$ need not commute, so $\ln\rho-\ln\sigma$ cannot be combined into a single logarithm and the classical argument (apply $\ln x\le x-1$ to a ratio of marginals) has no direct quantum analogue. Operator monotonicity or convexity of $\ln$ on $M(A)$ alone does not compare quantities living on $M(A)$ and on $M(AB)$; what is needed is a single operator on each space whose logarithm encodes the relative entropy, and a map between the spaces that intertwines those operators. Verifying the intertwining identities requires explicit computations with partial traces, Kronecker products and functional-calculus square roots in a vectorized picture of linear maps on matrices. The extension from invertible to arbitrary states is a continuity argument that the paper omits.

Formalization scope

• Systems. Finite nonempty types in Type; bipartite operators are Matrix (A × B) (A × B) ℂ (Mathlib's ⊗ₖ order), tripartite ones Matrix (A × (B × C)) (A × (B × C)) ℂ. Density matrices are QAlgorithms.IsDensityMatrix (PSD, trace 1); "invertible" is PosDef. Partial traces are the published WildeQIT.partialTraceRight / partialTraceLeft; $\operatorname{tr}_C$ on triples is defined locally.
• Logarithms are natural, via TroppMatrixConcentration.matrixLog (cfc Real.log, so $\ln0=0$ on kernels); square roots via ch8_matrixFunction. The relative entropy is real-valued and every statement applies it only to pairs where the paper's value is finite.
• Vectorization. A matrix $X$ is identified with $(X_{ij})_{(i,j)}$ in row-major order, so $\langle X,Y\rangle$ is the standard inner product and a linear map on $M(A)$ is a matrix on $\mathbb C^{A\times A}$. Then $\Delta=\sigma\otimes(\rho^{-1})^T$ (Kronecker), $\ln(\Delta)$ is its functional-calculus logarithm, and $\mathcal U$ is the matrix whose column $(a,a')$ is $\operatorname{vec}\,\mathcal U(E_{aa'})$, so $\mathcal U^\dagger$ is its conjugate transpose.
• Invertibility. (4), (6), (7) and the properties of $\mathcal U$ assume invertible states: this is the paper's own §3 assumption (p. 3). The continuity argument to general states is omitted by the paper and is not a milestone; the general case is the goal itself.
• Ruled out. $\ln(\Delta)$ is never defined as $\ln\mathcal L+\ln\mathcal R$, the relative entropy is never defined through (7), $\mathcal U$ is the specific map above and not an arbitrary isometry with the properties assumed, and (4), (6) are not stated for $\sigma=\rho$ or with a free real in place of $S(\cdot\|\cdot)$.
• Reused layers. TroppMatrixConcentration_ch8_entropy (functional calculus, operator convexity, matrixLog, Löwner order), WildeQIT_partialTrace, QAlgorithms_Defs_Information. Reindexing Lemma 1 (stated on Fin d) to A × A-indexed matrices is proof work, as is the bridge from nats to the goal's bits. Contributions of general lemmas on Kronecker products, partial traces and the functional calculus of Kronecker matrices are reusable beyond this mission.

Selected references

• M. A. Nielsen, D. Petz, A simple proof of the strong subadditivity inequality, Quantum Inf. Comput. 5 (2005) 507–513. arXiv:quant-ph/0408130v3
• D. Petz, Quasi-entropies for finite quantum systems, Rep. Math. Phys. 23 (1986) 57–65. doi:10.1016/0034-4877(86)90067-4
• E. H. Lieb, M. B. Ruskai, Proof of the strong subadditivity of quantum-mechanical entropy, J. Math. Phys. 14 (1973) 1938–1941. doi:10.1063/1.1666274
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. doi:10.1016/0001-8708(73)90011-X
• G. Lindblad, Completely positive maps and entropy inequalities, Commun. Math. Phys. 40 (1975) 147–151. doi:10.1007/BF01609396
• M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000 (10th anniversary ed. 2010). doi:10.1017/CBO9780511976667

Motivation

Many problems in combinatorial optimization, control and signal processing reduce to minimizing a nonconvex quadratic form over a box. Max-cut and other boolean quadratic programs are special cases. Computing the global minimum of such a program is NP-hard in general, so the practical question is how well a tractable convex problem can bound it. The semidefinite relaxation replaces the rank-one matrix $xx^T$ by an arbitrary positive semidefinite matrix $X$. It can be solved to any accuracy in polynomial time by interior-point methods, the subject of the preceding chapters of Ye's Interior Point Algorithms (Wiley 1997).

The quality of this relaxation has a short history. Goemans and Williamson (J. ACM 1995) showed that rounding a relaxation solution with a random hyperplane recovers at least $0.878$ of the maximum cut. Nesterov (Optim. Methods Softw. 1998) showed that for a positive semidefinite objective over $\{-1,1\}^n$ the relaxation is within a factor $\pi/2$, with no definiteness assumption needed for a bound on the range of the objective. Section 9.5 of Ye's book extends this range bound to quadratic programs with quadratic equality constraints and box bounds, and with an arbitrary symmetric objective. This mission formalizes that section.

Setting

Fix $n,m\ge 0$, a symmetric real $n\times n$ matrix $Q$, a real $m\times n$ matrix $A=\{a_{ij}\}$ with rows $a_i$, and $b\in\mathbb R^m$. Vector inequalities are componentwise and $e$ is the all-ones vector.

The quadratic program is

It is assumed feasible. Its maximum is $\bar q=-\underline q(-Q)$.

Write $P\bullet X=\sum_{i,j}P_{ij}X_{ij}$, $A_i=\operatorname{diag}(a_i)$, $d(X)$ for the diagonal of $X$, and $D(z)$ for the diagonal matrix with diagonal $z$. The relaxation (9.48) is

with $\bar p=-\underline p(-Q)$. Its dual (9.49) maximizes $e^Tz+b^Ty$ subject to $Q\succeq D(z)+\sum_iy_iA_i$ and $z\le0$.

For $V\in\mathbb R^{n\times n}$ with columns $v_1,\dots,v_n$, the sign rounding (9.50) is $\hat x=D\sigma(V^Tu)$. Here $D=\operatorname{diag}(\|v_1\|,\dots,\|v_n\|)$, $\sigma$ applies $\operatorname{sign}(t)=1$ for $t\ge0$ and $-1$ otherwise to each component, and $u$ is uniformly distributed on the unit sphere of $\mathbb R^n$. For a function $f$ of one variable, $f[X]$ is the matrix with entries $f(x_{ij})$.

Formalization targets

Goal: Theorem 9.33 (pp. 329–330)

The statement is deterministic. Its only hypotheses are that $Q$ is symmetric and that the quadratic program is feasible.

Milestones

• Lemma 9.31 (p. 328): if $X\succeq0$ and $d(X)\le e$, then $\arcsin[X]\succeq X$.
• Proposition 9.29 (p. 326): $\underline p\le\underline q\le\bar q\le\bar p$; $\bar q$ and $\bar p$ are attained maxima; and an optimal dual pair for $-Q$ yields $\bar p=e^T\bar z+b^T\bar y$ with $D(\bar z)+\sum_i\bar y_iA_i-Q\succeq0$.
• Lemma 9.30 (p. 327): $\underline q(Q)$ is the minimum, over $V$ with $A_i\bullet(V^TV)=b_i$ and $\|v_j\|\le1$, of $\mathbb E_u\,\sigma(V^Tu)^TDQD\,\sigma(V^Tu)$.
• Theorem 9.32 (p. 328): $\underline q(Q)$ is the infimum of $\frac2\pi Q\bullet(D\arcsin[D^{-1}XD^{-1}]D)$ over positive definite $X$ feasible for (9.48), with $D=\operatorname{diag}(\sqrt{x_{11}},\dots,\sqrt{x_{nn}})$.
• Theorem 9.35 (p. 331): for an optimal $\underline X=V^TV$ of the relaxation and $\hat x$ rounded from it, $(\mathbb E_u q(\hat x)-\underline q)/(\bar q-\underline q)\le\pi/2-1<4/7$.

Significance

Theorem 9.33 says that the range $[\underline p,\bar p]$ of a convex problem solvable by interior-point methods approximates the range $[\underline q,\bar q]$ of a nonconvex NP-hard program within the fixed factor $(4-\pi)/\pi\approx0.273$. This holds for any symmetric objective, in the presence of quadratic equality constraints. Theorem 9.35 converts the bound into a randomized algorithm. One rounding of the relaxation solution gives a feasible point whose expected objective lies within a $\pi/2-1<4/7$ fraction of the range above the minimum. Repeated draws give such a point almost surely. The constant $2/\pi$ recurs throughout semidefinite approximation theory, from the Goemans–Williamson analysis to Grothendieck-type inequalities.

The platform already holds the Gaussian form of the arcsine identity (ConvexOptAlg.GoemansWilliamson.lemma_6_12), Grothendieck's identity, the Schur product theorem and Nesterov's positive semidefinite case (HighDimProb.RandomVectors.sdp_relaxation_approximates_max_cut). None of these covers quadratic constraints, the box, an indefinite objective, or the uniform-sphere rounding used here. A complete development would be the first machine-checked proof of a constant-factor semidefinite range bound for constrained nonconvex quadratic programming.

Difficulty

Lemma 9.31 is a matrix inequality between a nonlinear entrywise function of $X$ and $X$ itself. Entrywise functions do not preserve positive semidefiniteness in general, so the obvious attempt (a scalar inequality between $\arcsin t$ and $t$) proves nothing about the matrices.

Lemma 9.30 and Theorem 9.32 need integration over the sphere. They need the probability that two hyperplane-sign coordinates disagree, which is a statement about the uniform measure on the sphere, not the Gaussian measure the existing platform results use.

The goal compares four optimal values, two of a nonconvex program and two of a semidefinite program, so it needs duality for the relaxation. The book's proof of Theorem 9.33 uses an optimal dual pair and positive definite feasible points of the relaxation. Neither is guaranteed under the stated hypotheses, and the theorem is claimed without them (see Beyond the paper).

Formalization scope

Vectors are Fin n → ℝ and matrices Matrix (Fin n) (Fin n) ℝ, indexed from $0$. $X\succeq0$ and $X\succ0$ are Mathlib's PosSemidef and PosDef, which include symmetry. $\underline q(Q)$ and $\underline p(Q)$ are real infima of the sets of feasible objective values. These sets are compact and, under the feasibility hypothesis every theorem carries, nonempty, so the infima are attained minima. The infimum in Theorem 9.32 is stated as IsGLB, so an empty set makes the statement false rather than trivially true. "Minimize" and "maximal value" in Lemma 9.30 and Proposition 9.29 are stated as a bound that is attained. The uniform measure on the sphere is Mathlib's surface measure volume.toSphere on the unit sphere of EuclideanSpace ℝ (Fin n), normalized to total mass one. Expectations are Bochner integrals of bounded measurable integrands, so the integral is the true expectation. $D^{-1}$ is Mathlib's matrix inverse, used only at positive definite $X$, where it is the true inverse.

Standing hypotheses of §9.5 that the book states once (p. 325) are explicit hypotheses of every theorem: $Q$ symmetric and the quadratic program feasible. No positive definite feasible point and no dual attainment are assumed in the goal. In Proposition 9.29(ii) the two clauses that name $(\bar y,\bar z)$ are stated for every optimal dual pair, since the book names such a pair without establishing that it exists; the maximality of $\bar p$ is stated outright. In Theorem 9.35, division is real division, so the case $\bar q=\underline q$, where the book's quotient is undefined, reads $0\le\pi/2-1$. No $O(\cdot)$ appears in this section, and every constant is the book's own: $2/\pi$, $(4-\pi)/\pi$, $\pi/2-1$ and $4/7$.

The theorem cannot be trivialized by an empty feasible region or a junk infimum. Feasibility is a hypothesis, the optimal values are attained minima of nonempty compact sets, and replacing the box or the quadratic constraints by an easy special case is ruled out by the definitions.

A complete development needs: the Schur product theorem and power series of entrywise functions of positive semidefinite matrices; the uniform measure on the sphere and its rotation invariance; and conic duality for the relaxation. The sphere and arcsine results are reusable well beyond this mission. Contributions on any milestone are welcome.

Beyond the paper. One variant is posed, qp_min_arcsin_infimum_corrected (kind: corrected). It is Theorem 9.32 with the added hypothesis that the relaxation has a positive definite feasible point. As printed, Theorem 9.32 fails for $n=2$, $a_1=(1,0)$, $b_1=0$, $Q=\operatorname{diag}(0,-1)$: there every feasible $X$ has $x_{11}=0$, while $\underline q=-1$. Two further findings are recorded without variants. The dual (9.49) need not attain its optimum, and the proof of Theorem 9.33 relies on both assumptions while the statement holds without them.

Selected references

• Y. Ye, Interior Point Algorithms: Theory and Analysis, Wiley-Interscience, 1997, §9.5. https://doi.org/10.1002/9781118032701
• M. X. Goemans and D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, Journal of the ACM 42(6), 1995. https://doi.org/10.1145/227683.227684
• Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optimization Methods and Software 9, 1998. https://doi.org/10.1080/10556789808805690

Motivation

Demand, prices and click-through rates often follow seasonal cycles: weekly, monthly, yearly. A decision maker who repeatedly chooses among options whose expected payoffs repeat in time faces a non-stationary multi-armed bandit. Chen, Wang and Wang (arXiv:2005.08088v4, Operations Research, 2025) study the model in which each arm's mean reward is periodic with its own unknown period. They give a two-stage policy whose regret is $\tilde O(\sqrt{T\sum_k T_k})$, and a lower bound showing that no policy, even one told the periods, does better than $\Omega(\sqrt{T\max_k T_k})$. This mission formalizes that lower bound, Theorem 3 of the paper. A companion mission of the same series covers the upper bound.

Lower bounds of this kind fix what is achievable. For the stationary $K$-armed bandit, the minimax regret is of order $\sqrt{TK}$ (Auer, Cesa-Bianchi, Freund and Schapire, 2002; Lattimore and Szepesvári, Bandit Algorithms, 2020, Ch. 15). In the periodic model a learner effectively faces $\sum_k T_k$ "effective arms" (arm $k$ at each phase of its cycle), which suggests the rate $\sqrt{T\sum_k T_k}$. The paper proves the weaker but general bound $\sqrt{T\max_k T_k}/(32e)$, which matches the upper bound up to a factor $\sqrt K$ and logarithms.

Setting

There are $K \ge 2$ arms and epochs $t = 1, \dots, T$. An instance $\nu$ is a family of mean rewards $\mu_{k,t}$. If arm $k$ is pulled at epoch $t$, the reward is drawn from the Gaussian law $\mathcal N(\mu_{k,t}, 1)$, independently of the past given the arm.

A sequence $f$ has minimum period $p \ge 1$ if $f(t+p) = f(t)$ for all $t \ge 1$ and no smaller positive integer has this property.

A policy $\pi$ chooses the arm $\pi_t$ at epoch $t$ at random, from a distribution that depends on the previous arms and rewards. Its expected regret on $\nu$ is display (1) of the paper:

Three classes of instances appear, all with unit-variance Gaussian rewards and means in $[0,1]$ (Assumption 1):

1. $\mathcal E_1$: every arm is stationary;
2. $\mathcal E_2(T_1)$: the first arm's mean has minimum period $T_1$, the other arms are stationary;
3. $\mathcal E_3(T_1,\dots,T_K)$: arm $k$'s mean has minimum period $T_k$.

The proof compares instances through the metric (B-48),

The periods satisfy Assumption 3 with the parameters (7): with $n = \lfloor\sqrt{T/K}\rfloor$ and $g = \lceil\sqrt n\rceil$, $T > 4K$, $g \ge 2$ and $T_k < n/(2g)$ for every $k$.

Formalization targets

Goal: Theorem 3 (p. 24)

For every policy $\pi$ there is $\nu \in \mathcal E_3(T_1,\dots,T_K)$ with

Milestones

1. Lemma 12 (p. 23). Stationary Gaussian bandits whose arms other than the first have known mean $1/2$: every policy has regret at least $\sqrt T/(8\sqrt2 e)$ on some choice of $\mu_1 \in [0,1]$.
2. Lemma 13 (p. 23). One periodic arm: every policy has regret at least $\sqrt{TT_1}/(16e)$ on some instance of $\mathcal E_2(T_1)$ whose other arms have mean $1/2$.
3. Fact 1 (proof of Theorem 3, p. 48). $\mathcal E_3$ is dense in $\mathcal E_2 \cup \mathcal E_3$ under $\mathcal M$: an instance of $\mathcal E_2(T_1)$ can be perturbed on the arms other than the first into an instance of $\mathcal E_3(T_1,\dots,T_K)$ at $\mathcal M$-distance less than any $\delta > 0$.
4. Fact 2 (proof of Theorem 3, p. 48). The regret $f_\pi(\nu) = \mathbb E_\nu[R^\pi_T]$ is continuous in $\nu$ on $\mathcal E_2 \cup \mathcal E_3$ for $\mathcal M$, uniformly in $\pi$.

Significance

Theorem 3 shows that knowing the periods does not remove the cost of learning them phase by phase: the regret must grow like $\sqrt{T\max_k T_k}$, not like $\sqrt{TK}$. Together with the paper's upper bound $\tilde O(\sqrt{T\sum_k T_k})$ and the inequality $\sqrt{T\max_k T_k} \ge \sqrt{T\sum_k T_k}/\sqrt K$, it shows the two-stage policy is near-optimal when $K$ is fixed. The intermediate results are reusable: Lemma 12 is a clean two-point Gaussian lower bound, Lemma 13 is a phase-decomposition argument that applies to any bandit model with known cyclic structure, and facts 1 and 2 give a continuity framework for the regret as a function of the instance.

The result has a published proof. As far as the platform's records show, none of it has been machine-checked. The stationary minimax lower bound of Lattimore and Szepesvári (a different family and constant) exists on the platform, together with the Bretagnolle–Huber inequality, the Gaussian KL divergence and the divergence decomposition, which this mission lists as tools.

Difficulty

The two-point argument of Lemma 12 is standard, but its constant needs $\Delta = \sqrt{1/(2T)} < 1/2$, so small horizons must be handled separately. Lemma 13 decomposes the problem into $T_1$ phase problems; making this rigorous means showing that a policy on the periodic problem induces, on each phase, a policy on a stationary problem of horizon $\lfloor T/T_1\rfloor$, with a history law that factorizes accordingly. The phase-wise instances produced by the decomposition need not have minimum period exactly $T_1$ (all phases may coincide), so a perturbation is needed to land in $\mathcal E_2(T_1)$; the constant has slack for it. Fact 2 asks for continuity of an integral against the law of a $T$-round adaptive process, uniformly over all policies, which needs a domination argument that does not depend on the policy's kernels.

Formalization scope

• Arms are Fin K, 0-based: the paper's first arm is index $0$. Epochs are 1-based natural numbers; history coordinate $i$ is epoch $i+1$. Values of the means at $t = 0$ are ignored.
• A policy is the platform's BanditAlgorithm.BanditPolicy K: one Markov kernel per round from the history to the next arm. The history law periodicMeasure reuses the platform's step kernel with the Gaussian bandit of the current epoch's means; with constant means it is BanditAlgorithm.banditMeasure of BanditAlgorithm.gaussianBandit. Lemma 12 is stated with the platform's banditRegret, $T\mu^* - \mathbb E[\sum_t X_t]$, which equals (1) for Gaussian arms; the other statements use (1) directly.
• Assumption 1 is stated on epochs $1,\dots,T$. Minimum periods are exact.
• Every lower bound has the order "for every policy there is an instance", with the instance in the class, so the policy may depend on $K$, $T$ and the periods; this is the paper's "policy that knows $T_k$". The supremum over the class is replaced by an attained instance, which is the stronger form.
• Added hypotheses, all disclosed: $K \ge 2$ (with one arm the regret is $0$); $T_k \ge 1$ (the paper's $T_k \in \mathbb N^+$); in Lemmas 12 and 13, the means of the arms other than the first are $1/2$, which is how "a policy that knows $\mu_k$ for $k \ge 2$" is read (with arbitrary known values the printed lemmas fail). Assumption 3 with (7) is the standing assumption of Appendix B.4.
• A statement with the quantifiers in the order "there is an instance for every policy", without the $[0,1]$ clause, or without exact minimum periods, would be false or trivial; none of these is the target.

Welcome contributions: the bridge between periodicMeasure with constant means and banditMeasure, the phase decomposition of the history law, and the uniform continuity of the regret in the means.

Selected references

• N. Chen, C. Wang, L. Wang, Learning and Optimization with Seasonal Patterns, Operations Research, 2025; arXiv:2005.08088v4, 2021. https://arxiv.org/abs/2005.08088v4
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The nonstochastic multiarmed bandit problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375

Motivation

Distributionally robust optimization evaluates a decision against a set of plausible probability laws rather than against a single estimated law. A common way to specify that set is to choose a nominal law $P_0$ and allow every law $P$ whose discrepancy from $P_0$ is below a radius $\varepsilon$. Different discrepancies produce different ambiguity sets, so comparing them tells a modeler what one constraint guarantees about another. Rahimian and Mehrotra collect such constructions in their survey and state a chain of comparisons among variation, Hellinger, Kullback–Leibler, and J-divergences in Lemma 5.4 (arXiv:1908.05659v1, pp. 31, 34–35). The chain connects four common ways of controlling model error without requiring a finite outcome space or a common density chosen in advance.

The source is the 2019 arXiv v1 preprint of a survey. Its proof of Lemma 5.4 cites earlier work rather than giving a full derivation. The preprint also prints an additional J-to-$\chi^2$ comparison that is false; this mission isolates the part that holds for every pair of probability measures. The distinction matters when an ambiguity set is used to certify a bound under a different divergence: an inclusion based on the false link can certify laws that are outside the intended set.

Setting

Let $(\Xi,\mathcal F)$ be a measurable space, and let $\mathfrak M(\Xi,\mathcal F)$ be its probability measures. Given $P_1,P_2\in\mathfrak M(\Xi,\mathcal F)$, a $\phi$-divergence $\mathfrak D^\phi(P_1,P_2)$ compares their densities using a function $\phi:[0,\infty)\to[0,\infty]$ with $\phi(1)=0$. The paper assumes $\phi$ is convex. To account for measures that are not mutually absolutely continuous, take the common dominating measure $\nu=P_1+P_2$ and write $p=dP_1/d\nu$ and $q=dP_2/d\nu$. The integrand is $q\phi(p/q)$ when $q>0$ and $p\phi'(\infty)$ when $q=0$, where $\phi'(\infty)=\lim_{t\to\infty}\phi(t)/t$; a point with $p=q=0$ contributes zero (§5.1.2, p. 31).

Table 1 gives four generators used here:

The first two divergences are the full $L^1$ variation discrepancy and the unhalved squared Hellinger discrepancy. In particular, $\mathfrak D^{\phi_v}=2d_{\mathrm{TV}}$, where $d_{\mathrm{TV}}$ is the total variation distance defined later in the paper. The J generator has $\phi_j(0)=+\infty$, understood as its limit at zero; $\phi_{\mathrm{kl}}(0)=1$ under $0\log0=0$. The recession slopes of the four generators, in the displayed order, are $1,1,+\infty,+\infty$ (Table 1, p. 31; §5.1.3, p. 35).

For a nominal probability measure $P_0$ and a nonnegative radius $\varepsilon$, equation (5.9) defines the ambiguity ball

Formalization targets

The three milestone comparisons are the valid initial part of (5.10), for every $P,P_0\in\mathfrak M(\Xi,\mathcal F)$:

The middle comparison is also stated in footnote 18. The mission goal is the corrected Lemma 5.4: it joins these three comparisons to the resulting valid part of (5.11), for every nominal $P_0$ and radius $\varepsilon$:

Each inclusion has the direction induced by the preceding divergence inequality: a stronger divergence constraint gives a smaller ball. The first comparison retains the paper's factor $1/4$, and the final ball retains its radius $2\sqrt\varepsilon$ (Lemma 5.4, p. 34).

Significance

The result allows a J-divergence or KL-divergence ambiguity model to carry a simultaneous bound in Hellinger and full variation divergence. A Hellinger radius $\varepsilon$ yields the explicit variation radius $2\sqrt\varepsilon$; this makes the scale change visible when comparing two models built with different discrepancies. Without a general-measure statement, a finite-outcome approximation does not itself cover continuous laws or pairs with a singular component.

The paper presents the inequalities as known and cites sources for them. A finite-alphabet TV–Hellinger–KL chain and a general-measure KL–affinity bound already have machine-checked results in the platform catalog. The work here is to formalize the four generators with one shared general-measure divergence, close the remaining inequalities in that representation, and connect them to the ambiguity-ball inclusions. This also provides reusable definitions for other distributionally robust models that use the same divergence convention.

Difficulty

Writing the density ratio only with respect to $P_0$ loses the part of $P$ singular to $P_0$. That would change both variation and Hellinger divergence and make the stated chain an unreliable comparison of the paper's objects. At the opposite boundary, $P$ can vanish on a set that $P_0$ charges. There the J generator must be infinite, although a direct use of a total real logarithm at zero can assign it an incorrect finite value. These two edge cases make an apparently routine pointwise comparison insufficient for the full measurable-space theorem.

Formalization scope

Lean represents $P$ and $P_0$ as ProbabilityMeasure Ξ on an arbitrary MeasurableSpace Ξ. It computes Radon–Nikodym densities relative to $P+P_0$, evaluates the divergence with an extended nonnegative Lebesgue integral, and represents both divergence values and radii in ENNReal. The generic definition computes the recession slope as a limsup; for the four Table 1 generators this is the limit in the paper. The formal ambiguity ball contains probability measures only. A top radius is allowed by the type; the finite nonnegative radii are the paper's intended model parameters. The generic operation does not take a convexity certificate, but the four named generators are the only ones used in the theorem.

The formalization must not turn a nondominated pair into divergence zero or assign $\phi_j(0)=0$: either choice changes the claimed chain. It must also retain the full variation divergence, without the half factor used for total variation distance. The definitions of the common-measure divergence, its four generators, and the ambiguity ball are intended for reuse. Contributions establishing properties of the recession slopes, comparison lemmas on arbitrary measurable spaces, and their ambiguity-set consequences are within scope.

The paper's final inequality in (5.10), $\mathfrak D^{\phi_j}\le\mathfrak D^{\phi_{\mathrm{ca}^2}}$, and the associated first inclusion in (5.11) are removed. They are false even on a two-point space: with $P_0=(1/2,1/2)$ and $P=(0,1)$, J-divergence is $+\infty$ while the order-two $\chi$-divergence is $1$. Thus $P$ lies in the latter ball of radius $1$ but outside the J ball of that radius. The source's footnote 18 separately notes an error in a cited Hellinger–KL comparison; the corrected Hellinger–KL inequality is retained (pp. 34–35).

Selected references

• H. Rahimian and S. Mehrotra, Distributionally Robust Optimization: A Review, arXiv preprint arXiv:1908.05659v1, 2019. Preprint.

Motivation

Schönhage and Strassen conjectured in 1971 that $n\log n$ is the optimal order of growth for multiplying two $n$-bit integers on a multitape Turing machine. Harvey and van der Hoeven proved the matching upper bound $O(n\log n)$ (Annals of Mathematics, 2021). In September 2026, a preprint by OpenAI, Integer multiplication below $n\log n$, claimed that this bound can itself be beaten by a power of the logarithm, in the same model. If correct, the upper half of the conjecture's "$\Theta(n\log n)$" is false. Two independent follow-up projects then increased the exponent saving $\kappa$ by many orders of magnitude. This mission targets the strongest claimed saving and takes the earlier claims as milestones.

Timeline (multitape Turing model; all bounds are of the form $O(n(\lg n)^{1-\kappa})$).

• 2021: Harvey and van der Hoeven, $\kappa=0$, that is, $O(n\log n)$. Published and refereed.
• 23 September 2026: OpenAI preprint, $\kappa=2^{-182}$ (Theorem 1 of the preprint). The preprint has not been refereed.
• October 2026: D. Colkitt, integer-mult-bounds, a series of patches to the OpenAI manuscript with checked numerical certificates, reaching $\kappa=2^{-30}$. The project describes this as conditional on the OpenAI manuscript and as having had no independent review.
• October 2026: S. Jain, integer-mult-kappa, building on both, reaching $\kappa=3666565558019/10^{17}\approx3.67\times10^{-5}>2^{-15}$ ("round six"). It is also stated to be conditional and unreviewed. Its numerical certificate is checked by computation in the Lean kernel, but the analytic facts behind that certificate are taken as premises.

Setting

A $k$-tape Turing machine, in the conventions of Montanaro's Computational Complexity lecture notes (§3, §3.4), has the following parts:

• a finite alphabet containing a blank $\square$ and a start symbol $\triangleright$;
• a finite set of states with a start state $\mathrm{START}$ and a distinct halting state $\mathrm{HALT}$;
• $k\ge2$ tapes: a read-only input tape, an output tape, and $k-2$ work tapes. Each tape is infinite in one direction, has its own head, and holds $\triangleright$ in its first cell and nowhere else.

In one step the machine reads the symbol under every head, writes a symbol under every head, moves each head by at most one cell (never left of $\triangleright$), and changes state. Once in $\mathrm{HALT}$ it stays there unchanged.

For $x\in\{0,1\}^n$ (most significant bit first), $\operatorname{val}(x)$ is the integer that $x$ represents, and $\operatorname{bin}_k(z)$ is the length-$k$ binary representation of $z$. A machine computes the product if, for every $n\ge1$ and all $x,y\in\{0,1\}^n$, when started on input $\triangleright\,x\#y$ it reaches $\mathrm{HALT}$ with the output tape holding exactly $\triangleright\,\operatorname{bin}_{2n}(\operatorname{val}(x)\operatorname{val}(y))$ followed by blanks. Its running time $T(n)$ is the largest number of steps on any pair of $n$-bit inputs. With $\lg n=\max(\lceil\log_2n\rceil,1)$, define

Formalization targets

Goal

Milestones: the earlier, weaker bounds

1. $\mathrm{KappaBound}(0)$: Harvey–van der Hoeven, Theorem 1.1. This is stated as a milestone of the companion mission, in the same machine model, and is referenced here.
2. $\mathrm{KappaBound}(2^{-182})$: OpenAI, Theorem 1.
3. $\mathrm{KappaBound}(2^{-30})$: Colkitt's ternary five-subset checkpoint.

Each milestone is implied by the goal, because $(\lg n)^{1-\kappa}$ decreases in $\kappa$. Each one is also a published claim in its own right and a natural intermediate formalization target. The $\kappa=0$ and $\kappa=2^{-182}$ constructions are the ones that the later claims rely on.

Significance

The result. Any $\kappa>0$ shows that $n\log n$ is not the optimal running time for multitape machines, which refutes the upper half of the Schönhage–Strassen conjecture as usually stated. The OpenAI preprint also derives the same bound for exact division and integer square roots (its Corollary 2). Larger values of $\kappa$ quantify how far below $n\log n$ multiplication can go. The bound is a statement about growth rates, and the constants involved are astronomically large.

Formalizing it. None of the three positive-$\kappa$ results has been refereed, and the two follow-ups explicitly depend on the OpenAI manuscript. Their written arguments, their computer-checked combinatorial certificates (rank sums, moment bounds, rational margins), and the full multiplication theorem have not been formally verified. Machine-checking any of the milestones would be the first independent confirmation of the corresponding claim. A formal disproof, or a formal identification of a gap, would be equally informative.

Difficulty

Fourier-based multiplication scans $\Theta(n)$ stored bits at each of $\Theta(\log n)$ transform levels, so any algorithm that performs those levels one at a time pays $\Theta(n\log n)$ for data movement and arithmetic alone. Beating this requires both moving data and carrying out butterfly layers at cost $o(V\log n)$ on a tape that is accessed sequentially, where $V$ is the stored volume. In the preprint this is done with recursive linear networks whose total number of smaller calls is strictly less than (number of roles) × (arity). The follow-ups improve $\kappa$ by finding better networks and tighter parameter choices, all certified by large exact computations. Each claim therefore combines a long analytic argument, a Turing-machine implementation, and a finite certificate, and all three must be formalized.

Formalization scope

• Machine model. The definitions are in IntMul_MultitapeModel, shared with the Harvey–van der Hoeven mission, and follow the $k$-tape conventions of Montanaro's lecture notes. Tapes begin with $\triangleright$. There is a $\mathrm{HALT}$ state that freezes the configuration. Tape $0$ is a read-only input tape holding $\triangleright\,x\#y$, and tape $1$ is the output tape, which must hold exactly $\triangleright$, then the product bits, then blanks. Running time is the number of steps until $\mathrm{HALT}$.
• The bound. As in the notes' definition of $O(\cdot)$: there are $c>0$ and $n_0$ with $T(n)\le c\,n(\lg n)^{1-\kappa}$ for $n\ge n_0$, and correctness is required for every $n\ge1$. Following the papers, $n$ is the length of each operand. The exponent $1-\kappa$ is a real power of a number that is at least $1$.
• No trivial solutions. A machine that fails to halt, or halts with a wrong output, on any well-formed input fails the definition. A proof must exhibit one fixed machine for all $n$.
• Infrastructure needed: Turing-machine composition with cost accounting; the Harvey–van der Hoeven reduction; the Nussbaumer synthetic transforms; the interchange and butterfly-layer networks of the preprint, with their rank and moment certificates; and the parameter assembly. The machine library and the certificate-checking infrastructure can be reused in other complexity missions.
• Welcome contributions: formal verification of the published certificates; formalization of the preprint's linear-network propositions; and machine-checked counterexamples to any step.

Selected references

• OpenAI, Integer multiplication below $n\log n$, preprint, 23 September 2026. https://github.com/openai/math/blob/main/preprints/Integer-multiplication-below-n-log-n-September-23-2026/paper.pdf
• D. Colkitt, A sharper exponent for integer multiplication (integer-mult-bounds), research draft, 2026. https://github.com/CrocSwap/integer-mult-bounds
• S. Jain, Integer multiplication: a conditional witness above $2^{-15}$ (integer-mult-kappa), research draft, 2026. https://github.com/Swapnil-jain/integer-mult-kappa
• D. Harvey, J. van der Hoeven, Integer multiplication in time $O(n\log n)$, Annals of Mathematics 193(2), 563–617, 2021. https://doi.org/10.4007/annals.2021.193.2.4
• A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7, 281–292, 1971. https://doi.org/10.1007/BF02242355
• H. J. Nussbaumer, Fast polynomial transform algorithms for digital convolution, IEEE Transactions on Acoustics, Speech, and Signal Processing 28(2), 205–215, 1980. https://doi.org/10.1109/TASSP.1980.1163372

Motivation

Lower bounds on the regret of stochastic multi-armed bandit strategies say how often any reasonable strategy must sample an arm that is not the best one. They are the benchmark against which upper bounds for UCB, KL-UCB and Thompson sampling are judged optimal. The classical bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) were proved by changes of measure on carefully chosen events, combined with Markov–Chernoff estimates of their probabilities.

Garivier, Ménard and Stoltz (arXiv:1602.07182v3), published in Mathematics of Operations Research in 2019, replace those arguments with one inequality, which they call the fundamental inequality of their article, inequality (6), p. 6. Every lower bound in the paper follows from it: the asymptotic Lai–Robbins / Burnetas–Katehakis bound for an arbitrary model (Theorem 1), the non-asymptotic bounds for small horizons (Theorems 2–4), and the non-asymptotic logarithmic bound for large horizons (Theorem 5). The same inequality, in the form of Lemma 1 of Kaufmann, Cappé and Garivier (2016), underlies lower bounds for best-arm identification. This mission formalizes the inequality and the lemma that carries its proof.

Setting

A bandit problem with $K$ arms is a family $\underline\nu=(\nu_a)_{a=1,\dots,K}$ of probability distributions on $\mathbb R$, each with a finite expectation. A strategy $\psi$ plays for $T$ rounds. In round $t+1$ it picks an arm $A_{t+1}$ as a measurable function of $I_t=(U_0,Y_1,U_1,\dots,Y_t,U_t)$, where the $U_t$ are independent uniforms on $[0,1]$. It then observes a reward $Y_{t+1}$ drawn from $\nu_{A_{t+1}}$ and a fresh independent uniform $U_{t+1}$. The strategy together with the problem determines the law $\mathbb P_{\underline\nu}$ of $I_T$; $\mathbb E_{\underline\nu}$ is its expectation. The number of draws of arm $a$ is

$\mathrm{KL}(P,Q)\in[0,+\infty]$ is the Kullback–Leibler divergence between two probability measures: $\int\ln\frac{\mathrm dP}{\mathrm dQ}\,\mathrm dP$ when $P$ is absolutely continuous with respect to $Q$ and the integral exists, and $+\infty$ otherwise. The binary divergence $\mathrm{kl}(p,q)$, for $p,q\in[0,1]$, is the Kullback–Leibler divergence between the Bernoulli distributions of parameters $p$ and $q$. For $q\in(0,1)$ it is given by (5):

It equals $+\infty$ for $q\in\{0,1\}$ and $p\ne q$.

The Lean development builds on the published StochasticBandit K, which holds the arm laws ν.P a. The local FullStrategy K implements the paper's measurable strategy on $I_t$; fullHistoryMeasure ν ψ T is the law of $I_T$, fullPullCount ψ a is $N_{\psi,a}(T)$, and fullExpPulls ν ψ T a is its expectation. The published BanditPolicy K describes the observed-history kernel model used by the two referenced chain-rule results. The shared definitions supply the Bernoulli law and klBer p q for $\mathrm{kl}(p,q)$.

Formalization targets

Goal: the fundamental inequality (6), p. 6

For every strategy $\psi$, every pair of bandit problems $\underline\nu,\underline\nu'$, every horizon $T$, and every $\sigma(I_T)$-measurable statistic $Z$ with values in $[0,1]$:

in $[0,+\infty]$, with $0\cdot(+\infty)=0$. The arm laws have the finite expectations required in §1.1; their divergences may be infinite.

Milestones, in the order of the proof (§2.1, pp. 7–8)

1. (9), p. 7: the one-round chain rule. Under finite arm divergences, the divergence between the observed-history laws after round $t+1$ is the divergence after round $t$ plus $\mathbb E_{\underline\nu}\big[\sum_a\mathrm{KL}(\nu_a,\nu'_a)\,\mathbb I\{A_{t+1}=a\}\big]$. The observed-history kernel version is proved on the platform.
2. Equality in (8), p. 7: $\sum_a\mathbb E_{\underline\nu}[N_{\psi,a}(T)]\,\mathrm{KL}(\nu_a,\nu'_a)=\mathrm{KL}(\mathbb P_{\underline\nu}^{I_T},\mathbb P_{\underline\nu'}^{I_T})$. The platform has the observed-history kernel version under finite arm divergences; relating it to the full information law is part of the goal's work.
3. Lemma 1, first display, p. 8: $\mathrm{KL}(\mathbb P_1,\mathbb P_2)=\mathrm{KL}(\mathbb P_1\otimes\lambda,\mathbb P_2\otimes\lambda)$, with $\lambda$ the Lebesgue measure on $[0,1]$.
4. Lemma 1, second display, p. 8: $\mathrm{KL}(\mathbb P_1,\mathbb P_2)\ge\mathrm{kl}\big((\mathbb P_1\otimes\lambda)(E),(\mathbb P_2\otimes\lambda)(E)\big)$ for every measurable $E\subseteq\Gamma\times[0,1]$.
5. Lemma 1, last display, p. 8: $(\mathbb P\otimes\lambda)\{(\gamma,x):x\le Z(\gamma)\}=\mathbb E[Z]$.
6. Lemma 1, p. 8: for probability measures $\mathbb P_1,\mathbb P_2$ on any measurable space and any measurable $Z$ with values in $[0,1]$, $\mathrm{KL}(\mathbb P_1,\mathbb P_2)\ge\mathrm{kl}(\mathbb E_1[Z],\mathbb E_2[Z])$.

Significance

The result. Inequality (6) turns a lower bound on the number of draws into a choice of an alternative problem $\underline\nu'$ and a statistic $Z$, usually $Z=N_{\psi,a}(T)/T$. The binary divergence then contains expected numbers of draws directly, and no event or concentration estimate is needed. In the paper this gives a few-line proof of the Lai–Robbins / Burnetas–Katehakis bound $\liminf_T\mathbb E[N_{\psi,a}(T)]/\ln T\ge 1/\mathcal K_{\inf}$ for any model. It also gives the non-asymptotic bounds showing that the regret grows almost linearly while $T$ is below a divergence-determined threshold. Each of these is a separate mission of this series, and each applies (6) once.

The formalization. The paper calls the equality in (8) standard and re-proves it for completeness; the inequality half, Lemma 1, is its own contribution. Observed-history kernel versions of the equality in (8) and the one-round step (9) are already formalized on the platform, under the hypothesis that every arm divergence is finite. Lemma 1 and the full-information inequality (6) itself are proved in the paper but not formalized. A machine-checked (6), stated with no divergence-finiteness hypothesis, would make every downstream lower bound in the series a matter of calculus with the binary divergence.

Difficulty

Two points need care. First, Lemma 1 is stated for an arbitrary $[0,1]$-valued $Z$. The data-processing inequality only gives it directly for indicators of events, and pushing $\mathbb P_j$ forward by $Z$ gives a law on $[0,1]$, not a Bernoulli law. The paper's route enlarges the space by an independent uniform variable, which needs the product with Lebesgue measure, the invariance of the divergence under that product, and Tonelli's theorem. Second, the goal has no finiteness hypothesis on the arm divergences, while the published chain-rule results assume it. When $\mathrm{KL}(\nu_a,\nu'_a)=+\infty$ for an arm that is drawn with positive probability, the left side is $+\infty$ and there is nothing to prove. When such an arm is never drawn, its term is $0\cdot(+\infty)=0$. The divergence between the history laws must then be shown to be finite and equal to the remaining sum, which the published decomposition does not cover.

Formalization scope

• Arms are Fin K, indexed from $0$. The horizon $T$ is a natural number; at $T=0$ both sides are $0$. For $K=0$ no policy exists, so $K\ge1$ needs no hypothesis.
• Strategies are FullStrategy K, measurable functions of the paper's $I_t$. The same strategy runs under $\underline\nu$ and $\underline\nu'$. The local history law includes every auxiliary uniform, so $Z$ may depend on any of them.
• Both bandit problems satisfy Integrable id for each arm, expressing §1.1's finite-expectation condition. The published StochasticBandit structure supplies only the probability-law condition.
• The binary divergence is the $[0,+\infty]$-valued Kullback–Leibler divergence of two Bernoulli laws, klBer, never a real formula. A real formula would return a finite junk value at $q\in\{0,1\}$, where (5) is $+\infty$, and would make the goal trivially true there. A version with a finiteness hypothesis on the arm divergences, or with a real-valued binary divergence restricted to $q\in(0,1)$, would be a weaker theorem and is not the target.
• In Lemma 1 and its displays, the "distributions" are probability measures on an arbitrary measurable space. $\lambda$ is the volume on Mathlib's unitInterval. $Z$ is real-valued and measurable, with values in $[0,1]$.
• Builds on the published definitions StochasticBandit and BanditPolicy and on Mathlib's InformationTheory.klDiv. The goal uses a local explicit auxiliary-uniform strategy; the published chain-rule references use observed-history kernel policies and are related proof tools. Other tools are data processing (klDiv_map_le), the chain rule for klDiv and composition products, and Tonelli. The tensorization identity for products of probability measures is Proved on the platform as Tensorization.klDiv_prod_eq_add. Lemma 1 is reusable well beyond bandits, wherever a divergence must be compared with the means of a bounded statistic. Proofs of the milestones, and an extension of the chain rule to infinite arm divergences, are welcome.

Selected references

• A. Garivier, P. Ménard, G. Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research 44(2), 2019; arXiv:1602.07182v3. https://arxiv.org/abs/1602.07182v3, https://doi.org/10.1287/moor.2017.0928
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Advances in Applied Mathematics 17, 1996. https://doi.org/10.1006/aama.1996.0007
• E. Kaufmann, O. Cappé, A. Garivier, On the complexity of best-arm identification in multi-armed bandit models, Journal of Machine Learning Research 17, 2016. https://jmlr.org/papers/v17/kaufman16a.html
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

Motivation

When many independent users share a network, each routes its own traffic to minimize its own delay, and nobody optimizes the system as a whole. Koutsoupias and Papadimitriou asked how much this lack of coordination can cost: how far the social cost of a Nash equilibrium can be from the social optimum, in the worst case. Their paper Worst-case equilibria (STACS 1999; journal version 2009, doi:10.1016/j.cosrev.2009.04.003) introduced this ratio, later named the price of anarchy, and studied it on the simplest network: parallel links between one source and one destination. The ratio has since become a standard measure of the inefficiency of equilibria in routing, scheduling and auctions (see Chapters 17–20 of Nisan, Roughgarden, Tardos and Vazirani, Algorithmic Game Theory, 2007).

Most of the paper concerns links of equal capacity. Its last result, Theorem 4, turns to two links of different speeds and shows that unequal speeds make equilibria worse: the worst-case ratio rises from $3/2$ for two identical links to the golden ratio $\varphi=(1+\sqrt5)/2\approx1.618$.

Timeline. 1999: Koutsoupias and Papadimitriou define the coordination ratio; for two identical links they prove it is exactly $3/2$, and for two links with speeds they give the golden-ratio lower bound of Theorem 4. 2002–2003: Mavronicolas and Spirakis, Koutsoupias, Mavronicolas and Spirakis, and Czumaj and Vöcking determine the asymptotic order of the price of anarchy for $m$ identical and for $m$ related links (Czumaj–Vöcking, ACM TALG 2007).

Setting

There are $n$ agents and $m$ parallel links. Agent $i$ has an amount of traffic $w_i>0$, and link $j$ has a speed $s_j>0$. A pure profile $a=(a_1,\dots,a_n)$ sends each agent's whole traffic over one link $a_i$. The load of link $j$ is $L_j(a)=\sum_{k:\,a_k=j}w_k$, and an agent on link $j$ experiences the delay $L_j(a)/s_j$.

A mixed strategy of agent $i$ is a probability distribution $(p_i^1,\dots,p_i^m)$ over the links; the agents randomize independently. The expected cost of agent $i$ is its expected delay. A profile $p$ is a Nash equilibrium if no agent can lower its expected cost by changing its own distribution. The expected traffic on link $j$ is $M^j=\sum_i p_i^jw_i$, and the cost to agent $i$ of placing its traffic on link $j$ is