Operations Research

Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation $E_\pi f$ one runs a Markov chain with stationary distribution $\pi$ and reports the sample average $\bar f_n$. The ergodic theorem guarantees $\bar f_n \to E_\pi f$, but honest error bars require more: a central limit theorem

On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions ($\alpha$-, $\rho$-, $\varphi$-mixing) against moment conditions on $f$. This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.

The basic UCB regret bound of Mission II is logarithmic but not tight: its leading constant $16/\Delta_i$ is eight times the information-theoretic limit, and its worst-case rate carries a spurious $\sqrt{\log n}$. Chapters 8–9 of Lattimore–Szepesvári close both gaps. A refined confidence schedule $f(t) = 1 + t\log^2 t$ yields the asymptotically optimal $\limsup_{n\to\infty} R_n/\log n \le \sum_{i:\Delta_i>0} 2/\Delta_i$ — exactly matching the instance-dependent lower bound of Mission VII for Gaussian noise. The MOSS index $\hat\mu_i + \sqrt{\tfrac{4}{T_i}\log^+\!\big(\tfrac{n}{k T_i}\big)}$ achieves minimax regret $R_n \le 39\sqrt{kn} + \sum_i \Delta_i$, matching the $\Omega(\sqrt{kn})$ lower bound up to a constant. These two theorems are the gold standard for finite-armed stochastic bandits.

A learner repeatedly chooses one of $k$ slot machines, observes only the reward of the chosen arm, and wants to earn almost as much as the best arm in hindsight. This is the stochastic multi-armed bandit, the canonical model of the exploration–exploitation dilemma. This mission formalizes the model (environments, policies, regret, and the regret decomposition $R_n = \sum_i \Delta_i\,\mathbb{E}[T_i(n)]$) and the two classical algorithms of Chapters 6–7 of Lattimore–Szepesvári: Explore-Then-Commit and the Upper Confidence Bound algorithm built on the optimism principle. The goal theorem is the instance-dependent UCB regret bound $R_n \le 3\sum_i \Delta_i + \sum_{i:\Delta_i>0} 16\log(n)/\Delta_i$ — logarithmic regret with explicit constants, the single most cited result of bandit theory — together with its distribution-free companion $R_n \le 8\sqrt{nk\log n} + 3\sum_i \Delta_i$.

Motivation

Machine scheduling asks how to assign jobs to machines over time. In many applications a job also needs additional scarce resources while it runs: a tool, a skilled operator, a memory bank, a channel. Adding such resources can turn a problem with a polynomial algorithm into an NP-hard one. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the standard three-field classification $\alpha\,|\,\beta\,|\,\gamma$ of scheduling problems (Graham, Lawler, Lenstra and Rinnooy Kan 1979) with a resource field $res\lambda\sigma\rho$. They then drew the complete borderline between easy and hard problems for unit-time jobs, identical or uniform machines and the makespan criterion. Their Fig. 2 marks each problem type as polynomially solvable or NP-hard.

This mission formalizes the two hardness results of that classification that come from graph partition problems (Theorems 2 and 3, p. 15). Two identical machines are easy under any resource constraints (Theorem 1, after Garey and Johnson 1975). Theorems 2 and 3 show that a third identical machine, or two machines of different speeds, already makes the problem strongly NP-hard, once the number of unit resources is part of the input.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$. Each machine processes at most one job at a time, and each job runs on one machine without interruption. Machine $M_i$ has a speed $q_i>0$, and every job has unit execution requirement $p_j=1$, so it takes time $1/q_i$ on $M_i$. Identical machines ($P$) are the case $q_i=1$; uniform machines ($Q$) allow arbitrary speeds.

There are $l$ resources $R_1,\dots,R_l$. Resource $R_h$ has a positive integer size $s_h$, the amount available at any time. Job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. A schedule assigns each job a machine $\mu(j)$ and a start time $S_j\ge 0$. Its completion time is $C_j=S_j+1/q_{\mu(j)}$, and it is being executed at every time $t$ with $S_j\le t<C_j$. A schedule is feasible when:

• jobs on the same machine do not overlap in time;
• at every time $t$, the set $S_t$ of jobs being executed satisfies

The makespan is $C_{\max}=\max_j C_j$.

The resource type $res{\cdot}11$ means three things: the number $l$ of resources is part of the input, every size is $s_h=1$, and every requirement satisfies $r_{hj}\le1$. A unit resource is therefore a conflict: two jobs that both need it can never run at the same time. The problems here have no precedence constraints. $Pm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ and $Qm\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ ask for a feasible schedule of minimum makespan. Their decision versions ask, for a threshold $y$, whether a feasible schedule with $C_{\max}\le y$ exists.

The source problems are two graph problems on a graph $G=(V,E)$ with $|V|=3t$:

• PARTITION INTO TRIANGLES: can $V$ be partitioned into $t$ triples of pairwise adjacent vertices?
• PARTITION INTO PATHS OF LENGTH 2: can $V$ be partitioned into $t$ triples, each with at most one nonadjacent pair, that is, each spanning a path of length 2?

Both are NP-complete (Garey and Johnson 1979, problems GT11 and GT13).

The construction of p. 15 introduces one job per vertex and one unit resource $R_{\{j,k\}}$ per nonadjacent pair $\{j,k\}$, required by $J_j$ and $J_k$ only.

Formalization targets

Goal: Theorem 3

Formally: if the language of PARTITION INTO PATHS OF LENGTH 2 is NP-hard, then the language of unary codes of yes-instances of the decision version of $Q2\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard. The two speeds are arbitrary positive integers.

Milestones

1. The construction's key property (p. 15). In the constructed instance, two distinct jobs can be executed simultaneously if and only if their vertices are adjacent.
2. The triangle equivalence (proof of Theorem 2). $G$ has a partition into triangles if and only if the constructed instance on three identical machines has a feasible schedule with $C_{\max}\le t$.
3. Theorem 2. $P3\,|\,res{\cdot}11,\,p_j=1\,|\,C_{\max}$ is NP-hard in the strong sense, given the NP-hardness of PARTITION INTO TRIANGLES.
4. The paths equivalence (proof of Theorem 3). $G$ has a partition into paths of length 2 if and only if the constructed instance on two uniform machines with speeds $q_1=2$, $q_2=1$ has a feasible schedule with $C_{\max}\le t$.

Significance

The results. Theorems 2 and 3 are two of the minimal NP-hard problems in the paper's classification. Together with Theorem 1 they place the borderline exactly: with unit resources whose number is part of the input, two identical machines are polynomial, while three identical machines, or two machines of different speeds, are strongly NP-hard. Strong NP-hardness rules out pseudo-polynomial algorithms unless P = NP, and it carries over to every more general resource type and machine environment in Fig. 1 and Fig. 2. Section 4.1 of the paper also derives hardness for $\sum C_j$ and $L_{\max}$ from these instances.

Formalizing it. The results are classical and proved on paper, but the paper's proofs are one sentence each ("Clearly", "It is easily seen"). No machine-checked proof exists, and the platform has no model of resource-constrained scheduling with real-valued time. This mission produces that model. It also produces a precise statement of strong NP-hardness on top of Cook's Turing-machine definitions, and the first formal NP-hardness reductions from graph partition problems to scheduling.

Difficulty

The scheduling half of each equivalence depends on the real-time model. On two uniform machines of speeds 2 and 1, jobs take time $\tfrac12$ and $1$, so jobs on the fast machine start at half-integers or anywhere else. The resource constraint must hold at every real time, not at a finite set of checkpoints. An argument that treats time as integer slots applies to the triangle case but does not transfer to the paths case.

The complexity half needs polynomial-time computability of the construction on Cook's one-tape Turing machines, on encoded strings that include malformed inputs. It also needs closure of polynomial-time reductions under composition, which the imported complexity layer states but does not prove.

Formalization scope

• Time and schedules. Start times are nonnegative reals, execution intervals are half-open $[S_j,C_j)$, and the resource constraints are imposed at every real time. Schedules are nonpreemptive.
• Indices. Jobs, machines and resources are 0-based (Fin n, Fin m, Fin l), so $q_1,q_2$ are q 0, q 1.
• Decision versions. "NP-hard" refers to the decision version with a threshold $y$. Thresholds are natural numbers and the $Q2$ speeds are positive integers. This restricted problem is a subproblem of the one with rational data, so its hardness is the stronger statement.
• Encodings and strong NP-hardness. Instances are strings over a two-letter alphabet with every number in unary. Graphs are $t$ in unary followed by the $3t\times 3t$ adjacency matrix, so $|V|=3t$ is part of the instance. Languages contain only codes of yes-instances. Strong NP-hardness is NP-hardness of the unary code language. With unary numbers, $\mathrm{Max}(I)\le\mathrm{Length}(I)$, so this is equivalent to Garey and Johnson's definition. The complexity layer is the published module CookPvsNP_defs.
• Cited hypothesis. Each hardness theorem takes as its only hypothesis the NP-hardness of its source problem, which the paper cites from Garey and Johnson rather than proves. The hypothesis is a true statement about a nonempty, non-universal language. The statements are not weakened to a reduction between languages, and they assume nothing about P versus NP.
• Source problems. The paper's phrase "three vertices, at most two of which are nonadjacent" is read as "at most one nonadjacent pair", which is Garey and Johnson's GT13. Reading it as "at most two nonadjacent pairs" would admit triples with a single edge and change the problem. PARTITION INTO PATHS OF LENGTH 2 reuses the published definition CubicP3Partition.P3Factor, a spanning non-induced $P_3$-factor.
• Construction. Resources are indexed by the nonadjacent pairs $j<k$ in lexicographic order, one per unordered pair and none for a pair $\{j,j\}$. A diagonal resource would make every job infeasible.
• Not trivial. A model that checks resources only at integer times, or only at start times, would make the paths equivalence false. A hypothesis on the target problem would make the goal circular. The definitions rule out both.

Welcome contributions: proofs of the two equivalences, polynomial-time computability of the construction on Cook's machines, and a general composition lemma for polynomial-time reductions. The composition lemma is reusable for every hardness mission built on CookPvsNP_defs.

Selected references

• J. Błażewicz, J. K. Lenstra, A. H. G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
• M. R. Garey, D. S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, Freeman, San Francisco, 1979, ISBN 0-7167-1045-5.
• R. L. Graham, E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
• S. Cook, The P versus NP problem, Clay Mathematics Institute Millennium Problems. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Several classical min-max theorems of combinatorial optimization say that a discrete maximization problem and a continuous minimization problem have the same optimal value, and that both have integral optimal solutions when the data are integral. Edmonds' polymatroid intersection theorem (1970), Fujishige's Fenchel-type duality for submodular functions (1984), Frank's discrete separation theorem for a submodular/supermodular pair (1982), and the potential characterizations of weighted matroid intersection (Frank's weight splitting theorem, 1981; Iri and Tomizawa's criterion for the assignment problem, 1976) are instances. Murota's paper Convexity and Steinitz's exchange property, 1996 places all of them under one theorem: a Fenchel-type min-max formula for a pair of an M-concave and an M-convex function, with integrality on both sides.

Timeline:

• 1970: Edmonds proves the polymatroid intersection theorem.
• 1982: Frank proves the discrete separation theorem for submodular/supermodular set functions, with integrality.
• 1984: Fujishige proves a Fenchel-type min-max theorem for submodular functions.
• 1976–1981: Iri and Tomizawa characterize optimality for independent assignment by potentials; Frank proves the weight splitting theorem for weighted matroid intersection (1981).
• Early 1990s: Dress and Wenzel introduce valuated matroids.
• 1995–1996: Murota proves the valuated matroid intersection theorem (SIAM J. Discrete Math. 9, 1996) and the M-concave intersection theorem (Bonn report, 1995), and in the present paper the Fenchel-type duality (Theorem 6.4).
• Later: the result becomes the central duality theorem of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM, 2003).

Setting

Let $V$ be a finite nonempty set. For $u\in V$, $\chi_u\in\mathbb Z^V$ is its characteristic vector; for $x\in\mathbb R^V$, $\operatorname{supp}^{\pm}(x)$ are the sets of coordinates where $x$ is positive or negative, $x(X)=\sum_{v\in X}x(v)$, and $\langle p,x\rangle=\sum_v p(v)x(v)$.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v\in B$. These are exactly the integer points of integral base polytopes of submodular systems. $\overline B$ is the convex hull of $B$.

A function $\omega:B\to\mathbb R$ has the exchange property (EXC), and is called M-concave, if for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ some $v\in\operatorname{supp}^-(x-y)$ has $x-\chi_u+\chi_v,\ y+\chi_u-\chi_v\in B$ and

A function $\zeta$ is M-convex when $-\zeta$ is M-concave.

For $\omega:B_1\to\mathbb R$ and $\zeta:B_2\to\mathbb R$ the concave conjugate and convex conjugate are

and the concave closure and convex closure are $\hat\omega(b)=\inf_p(\langle p,b\rangle-\omega^\circ(p))$ and $\check\zeta(b)=\sup_p(\langle p,b\rangle-\zeta^\bullet(p))$; they are finite exactly on $\overline{B_1}$ and $\overline{B_2}$.

The primal problem maximizes $\omega(x)-\zeta(x)$ over $x\in B_1\cap B_2$; the relaxed primal problem maximizes $\hat\omega(b)-\check\zeta(b)$ over $b\in\overline{B_1}\cap\overline{B_2}$; the dual problem minimizes $\zeta^\bullet(p)-\omega^\circ(p)$ over $p\in\mathbb R^V$. A maximum over an empty family is $-\infty$.

Formalization targets

Goal: Theorem 6.4

If $\omega$ and $-\zeta$ satisfy (EXC), then

with (P1) a finite dual infimum forces $B_1\cap B_2\neq\emptyset$, and (P2) if $B_1\cap B_2\neq\emptyset$ all values are finite and equal and the infimum is attained. If $\omega,\zeta$ are integer-valued, the infimum may be taken over $p\in\mathbb Z^V$ and is attained there when finite.

Milestones

1. Lemma 6.3 (weak duality): for arbitrary $\omega,\zeta$ on finite nonempty sets, primal $\le$ relaxed $=$ dual (the Fenchel identity (6.5)).
2. Lemma 6.1: $(-f)^\circ(p)=-f^\bullet(-p)$ and $(-f)^\wedge=-\check f$ on $\overline B$.
3. Lemma 4.5: an M-concave $\omega$ satisfies $\hat\omega=\omega$ on $B$.
4. Theorem 2.1: (B1) is equivalent to being the integer points of an integral submodular (or supermodular) base polytope, with the describing functions $\max_{x\in B}x(X)$ and $\min_{x\in B}x(X)$.
5. Theorem 6.5 (Frank's discrete separation theorem, cited in the paper).
6. Lemma 6.7: four equivalent forms of boundedness of the dual problem.
7. Theorem 6.6 (the M-concave intersection theorem, cited in the paper): optimality of $x^*$ for $\omega_1+\omega_2$ is equivalent to a potential $p^*$ with $x^*$ maximizing both $\omega_1[-p^*]$ and $\omega_2[p^*]$, integral when the data are.

Significance

The formula gives, in one statement, the integrality of an optimal solution of the relaxed primal problem (the essential content of the first half, as the paper observes on p. 296) and of the dual problem. The paper presents it as a unification of two groups of theorems: Edmonds' polymatroid intersection theorem, Fujishige's Fenchel-type duality and Frank's discrete separation theorem on one side, and Iri and Tomizawa's potential characterization for independent assignment with its extensions by Fujishige and Frank (weight splitting) on the other. In the paper it yields the primal and dual separation theorems (Theorems 6.8, 6.9) and the convolution results (Theorems 6.10, 6.11), and it is the prototype of the Fenchel-type duality of discrete convex analysis.

All results here are proved in the literature; none is known to be formalized. Mathlib has no submodular base polytopes, no matroid intersection theorem and no discrete convex analysis. A formal proof of Theorem 6.4 would also require formal proofs of the two cited results, Frank's discrete separation theorem and the M-concave intersection theorem, which the paper uses without proof.

Difficulty

Lemma 6.3 is polyhedral convex duality and holds for any functions. The content is equality with the integral problem: the relaxed maximum over the polytope $\overline{B_1}\cap\overline{B_2}$ must be attained at an integer point. For general finite sets it is not, and the intersection of two integral polytopes generally has fractional vertices. Both the integrality of $\overline{B_1}\cap\overline{B_2}$ (Edmonds) and the existence of an integral optimal potential depend on the exchange structure; a direct argument from the definitions of conjugates does not see it. The dual integrality claim, that $p$ can be taken integral, is again specific to (EXC) and fails for general concave extensions.

Formalization scope

Lean conventions, all in namespace SteinitzExchange.Duality:

• $V$ is a type with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ; finite sets of integer vectors are Finset (V → ℤ).
• A function on $B$ is a total (V → ℤ) → ℝ used only at points of $B$. M-convexity of $\zeta$ is (EXC) for fun x => -ζ x; $\omega$ lives on $B_1$ and $\zeta$ on $B_2$, which are distinct sets in general.
• Conjugates are real-valued min/max over the finite set. The closures are real ⨅/⨆ over $p\in\mathbb R^V$ and are evaluated only on the convex hulls, where they equal the paper's values; off the hulls they carry a junk value instead of $\mp\infty$, which no statement uses.
• The three optimal values are in EReal, as suprema and infima of coerced reals, so no $\infty-\infty$ occurs. EReal's supremum of the empty family is $-\infty$, the paper's convention. The dual infimum is never a real ⨅ (which would return $0$ when unbounded and make (P1) meaningless).
• Every "max" of the page includes attainment: (P2) asserts points $x$, $b$, $p$ at which the three values are achieved; the integral dual infimum is attained when it is not $-\infty$.
• "Integer-valued" means $\omega(x)\in\mathbb Z$ on $B_1$ and $\zeta(x)\in\mathbb Z$ on $B_2$; integral potentials and separating vectors are V → ℤ.
• Theorem 2.1's "$\forall X\subset V$" is read as all $X\subseteq V$.

Formalizations that would trivialize the goal are excluded: an unrestricted real infimum for the dual, a convex closure built from $\zeta^\circ$ instead of $\zeta^\bullet$, a single base set for both functions, and a relaxed maximum taken over all of $\mathbb R^V$ instead of $\overline{B_1}\cap\overline{B_2}$.

Needed infrastructure: finite convex hulls and polyhedral Fenchel duality, submodular base polytopes and their integrality, Frank's separation theorem, and the valuated intersection theorem. The submodular-system layer (Theorem 2.1, Theorem 6.5) is reusable beyond this mission. Contributions to any milestone, including proofs of the two cited theorems, are welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996) 272–311. https://doi.org/10.1006/aima.1996.0084
• K. Murota, Valuated matroid intersection I: optimality criteria, SIAM J. Discrete Math. 9 (1996) 545–561.
• K. Murota, Submodular flow problem with a nonseparable cost function, Report 95843-OR, Forschungsinstitut für Diskrete Mathematik, Universität Bonn, 1995 (source of Theorem 6.6).
• A. Frank, An algorithm for submodular functions on graphs, Annals of Discrete Mathematics 16 (1982) 97–120 (source of Theorem 6.5).
• A. Frank, A weighted matroid intersection algorithm, J. Algorithms 2 (1981) 328–336.
• J. Edmonds, Submodular functions, matroids and certain polyhedra, in: Combinatorial Structures and Their Applications, Gordon and Breach, New York, 1970, 69–87.
• S. Fujishige, Theory of submodular programs: a Fenchel-type min-max theorem and subgradients of submodular functions, Mathematical Programming 29 (1984) 142–155.
• M. Iri and N. Tomizawa, An algorithm for finding an optimal "independent assignment", J. Oper. Res. Soc. Japan 19 (1976) 32–57.
• K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508

Motivation

Linear optimization over the bases of a matroid, over the integer points of a polymatroid, or over the flows of a network is well understood: the greedy algorithm is exact, the feasible sets are the integer points of polytopes described by submodular functions, and min-max theorems of Edmonds and Frank hold with integrality. Nonlinear objectives on the same sets are much less uniform. Valuated matroids (Dress and Wenzel, 1990; see Murota 2003) showed that a quantitative form of the Steinitz exchange axiom is exactly what keeps the greedy algorithm exact for a nonlinear weight. Kazuo Murota's paper Convexity and Steinitz's Exchange Property (Adv. Math. 124 (1996) 272–311) extends this exchange axiom from matroid bases to the integer points of arbitrary integral base polytopes, names the resulting functions M-concave, and proves that they are the discrete counterpart of concave functions. The paper is the starting point of discrete convex analysis (Murota, Discrete Convex Analysis, SIAM 2003), which is now used in auction theory (gross-substitutes valuations are M♮-concave), inventory and resource allocation, and combinatorial optimization.

This mission covers the first of the paper's three characterizations of M-concavity: the Extension Theorem (Theorem 4.6).

Setting

Let $V$ be a finite nonempty set. For $u\in V$, $\chi_u\in\mathbb Z^V$ is the characteristic vector of $u$. For $x\in\mathbb R^V$, $\operatorname{supp}^+(x)=\{v\mid x(v)>0\}$, $\operatorname{supp}^-(x)=\{v\mid x(v)<0\}$, $\|x\|=\sum_v|x(v)|$, and $\langle p,x\rangle=\sum_v p(v)x(v)$.

A finite integral base set is a finite nonempty $B\subseteq\mathbb Z^V$ such that for $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v\in B$ (axiom (B1)). Examples are the incidence vectors of the bases of a matroid. Its convex hull $\overline B$ is an integral base polytope; in general, an integral base polytope is the convex hull of some finite integral base set.

A function $\omega:B\to\mathbb R$ satisfies the exchange property (EXC), and is called M-concave, if for all $x,y\in B$ and $u\in\operatorname{supp}^+(x-y)$ there is $v\in\operatorname{supp}^-(x-y)$ with $x-\chi_u+\chi_v\in B$, $y+\chi_u-\chi_v\in B$ and

The local exchange property (EXC$_{\mathrm{loc}}$) asks only, for $x,y\in B$ with $\|x-y\|=4$, for some $u\in\operatorname{supp}^+(x-y)$ and some $v\in\operatorname{supp}^-(x-y)$ with the same conclusion.

For $p\in\mathbb R^V$, $\omega[p](x)=\omega(x)+\langle p,x\rangle$, and $\operatorname{argmax}(\omega)=\{x\in B\mid\omega(x)\ge\omega(y)\ \forall y\in B\}$. For any $g:B\to\mathbb R$, the concave conjugate is $g^\circ(p)=\min_{x\in B}(\langle p,x\rangle-g(x))$ and the concave closure is $\hat g(b)=\inf_{p\in\mathbb R^V}(\langle p,b\rangle-g^\circ(p))$, a concave function that is finite exactly on $\overline B$. A function $\bar\omega:\overline B\to\mathbb R$ extends $\omega$ if $\bar\omega=\omega$ on $B$.

Formalization targets

Goal: the Extension Theorem (Theorem 4.6)

For a finite integral base set $B$ and $\omega:B\to\mathbb R$,

Milestones

• Lemma 3.2 (p. 282): under (EXC$_{\mathrm{loc}}$), for $y=x-\chi_{u_0}-\chi_{u_1}+\chi_{v_0}+\chi_{v_1}\in B$, $\omega_p(y)-\omega_p(x)\le\max(\pi_{00}+\pi_{11},\pi_{01}+\pi_{10})$ with $\pi_{ij}=\omega_p(x-\chi_{u_i}+\chi_{v_j})-\omega_p(x)$ ($-\infty$ off $B$).
• Theorem 3.1 (p. 282): (EXC) $\iff$ (EXC$_{\mathrm{loc}}$).
• Theorem 2.2 (p. 280): (EXC) for $\omega$ implies (EXC) for every $\omega[p]$.
• Lemma 4.3 (p. 285): under (EXC), $\operatorname{argmax}(\omega)$ is an integral base set.
• Lemma 4.1 (p. 285): $\hat g\ge g$ on $B$; $\max_{\overline B}\hat g=\max_B g$; $\operatorname{argmax}(\hat g)=\overline{\operatorname{argmax}(g)}$.
• Lemma 4.2 (p. 285): $(g[p_0])^\circ(p)=g^\circ(p-p_0)$ and $(g[p_0])^\wedge=\hat g+\langle p_0,\cdot\rangle$ on $\overline B$.
• Theorem 4.4 (p. 286): (EXC) $\iff$ $\operatorname{argmax}(\omega[p])$ is an integral base set for every $p$.
• Lemma 4.5 (p. 288): under (EXC), $\hat\omega=\omega$ on $B$.

Significance

The Extension Theorem identifies a combinatorial axiom with a convex-analytic property: M-concave functions are exactly the restrictions to lattice points of concave functions on the base polytope whose linear perturbations are all maximized on integral base polytopes. It is the reason the M-concave class supports a convex-analysis-style theory at all: local optimality implies global optimality, maximizers of linear perturbations are well behaved, and conjugacy (the paper's Theorems 5.3 and 6.4, separate missions of this series) can be developed. Theorem 3.1 on its own is widely used to verify M-concavity in applications, since it reduces the exchange axiom to pairs at distance four.

All results here were proved in 1996. To our knowledge none of them has a machine-checked proof; Mathlib has matroids on sets but no integral base sets in $\mathbb Z^V$, no M-concave functions and no concave closure of a function on a finite set. A formal proof of this chain would be a first formal development of discrete convex analysis.

Difficulty

The equivalence of (EXC) with its local version (Theorem 3.1) is not a routine induction on $\|x-y\|$: the exchange inequality for a far pair does not follow from the inequalities along a path of distance-4 pairs, because the exchange partner $v$ must be chosen consistently with the prescribed $u$. For the "if" direction of Theorem 4.4, knowing that every maximizer set is an integral base set says nothing directly about the values of $\omega$ at non-maximizing points; turning this global information on maximizers into the local inequality (EXC$_{\mathrm{loc}}$) requires a supporting hyperplane of the concave closure at a well-chosen point and the integrality of the intersection of an integral base polytope with a box (a cited result on submodular systems). Theorem 4.6 then needs the concave closure to agree with $\omega$ on $B$ (Lemma 4.5), which fails for general $\omega$.

Formalization scope

All declarations live in the namespace SteinitzExchange.Extension. The ground set is a type V with [Fintype V] [DecidableEq V] [Nonempty V]; integer vectors are V → ℤ, real vectors V → ℝ, and toReal embeds the former into the latter. $B$ is a Finset (V → ℤ). A function $\omega:B\to\mathbb R$ is a total (V → ℤ) → ℝ whose values are only ever read at points required to be in $B$. $\overline B$ is Mathlib's convexHull ℝ of the image of $B$. Pinned readings:

1. Integral base polytope means the convex hull of a finite nonempty set satisfying (B1) (by the paper's Theorem 2.1 this is its meaning), not "a polytope with integer vertices".
2. The concave closure is a real infimum; it is the paper's value on $\overline B$ and a junk value $0$ off $\overline B$ (the paper's $-\infty$), so every statement uses it only on $\overline B$. $\operatorname{argmax}(\hat g)$ and $\operatorname{argmax}(\bar\omega[p])$ range over $\overline B$ only; the concave conjugate is a minimum over the nonempty finite $B$.
3. Lemma 3.2's maximum with $-\infty$ entries is stated as: for one of the two pairings both exchanged points lie in $B$ and the bound holds for that pairing.
4. Theorem 4.4 and Lemma 4.3 conclude that $\operatorname{argmax}(\omega[p])$ is itself an integral base set. Read literally ("its convex hull is an integral base polytope") the "if" direction of Theorem 4.4 is false: $B=\{(2,0),(1,1),(0,2)\}$ with $\omega=(0,-1,0)$ is a counterexample. The paper's proof, its gloss in Lemma 4.3 and its use on p. 292 all take the integral-base-set reading. Theorem 4.6 needs no such adjustment and is stated as printed.
5. Theorem 2.2 carries the standing assumption of §2.3 that $\omega$ satisfies (EXC).

Trivializing formalizations are ruled out: the extension $\bar\omega$ must agree with $\omega$ on $B$ and be concave on $\overline B$, the argmax is over $\overline B$ and not over $\mathbb R^V$, and an integral base polytope is never empty.

A complete development needs basic facts on integral base sets (the equivalence of (B1) with the simultaneous exchange (B2), $B=\mathbb Z^V\cap\overline B$, and the paper's cited Theorem 2.1 relating them to submodular functions), the representation (4.3) of the concave closure as a maximum of convex combinations, and supporting hyperplanes of polyhedral concave functions. The layer of integral base sets and M-concave functions is reusable for the two other missions of this series and for any later formalization of discrete convex analysis; contributions of general-purpose lemmas about it are welcome.

Selected references

• K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124 (1996) 272–311. https://doi.org/10.1006/aima.1996.0084
• K. Murota, Discrete Convex Analysis, SIAM Monographs on Discrete Mathematics and Applications, 2003. https://doi.org/10.1137/1.9780898718508

The oldest bandit algorithm (Thompson, 1933) is also the most modern: sample a parameter from the posterior and act greedily. Chapters 34–36 of Lattimore–Szepesvári develop the Bayesian view in two crowning results. The Gittins index theorem: for infinite-horizon discounted Markov bandits, the seemingly intractable dynamic program is solved exactly by an index policy — each arm gets a retirement-value index computable arm-by-arm, and playing the largest index is Bayesian optimal. And the frequentist analysis of Thompson sampling — the goal theorem: with Gaussian posteriors, Thompson sampling on 1-subgaussian bandits achieves $\lim_{n\to\infty} R_n/\log n = \sum_{i:\Delta_i>0} 2/\Delta_i$, exactly asymptotically optimal, alongside the minimax-grade $R_n \le C\sqrt{kn\log n}$. Together they explain why posterior sampling is both principled and practically dominant.

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

Line search methods for unconstrained minimization of a smooth function $f : \mathbb{R}^n \to \mathbb{R}$ choose a direction $d_k$ and a step $\alpha_k > 0$ and set $x_{k+1} = x_k + \alpha_k d_k$. Classical rules (Armijo, Wolfe) insist that every step decrease $f$. For quasi-Newton and conjugate gradient directions this monotonicity requirement often forces short steps, and nonmonotone line searches, which only ask for a decrease relative to some reference value built from past iterates, have been used since Grippo, Lampariello and Lucidi (1986) to let such methods take longer steps.

Zhang and Hager (SIAM J. Optim., 2004) replaced the maximum of recent function values used by Grippo et al. with a weighted average $C_k$ of all past function values. The paper proves two results: global convergence to stationary points (the companion mission) and, the subject of this mission, R-linear convergence of the function values when $f$ is strongly convex.

Timeline:

• 1986, Grippo, Lampariello, Lucidi: nonmonotone line search based on the maximum of the last $M$ function values; global convergence.
• 2002, Dai: R-linear convergence of the max-based scheme for strongly convex $f$.
• 2004, Zhang and Hager: the averaged reference value $C_k$; global convergence (Theorem 2.2) and R-linear convergence for strongly convex $f$ (Theorem 3.1).

Setting

Fix parameters $0 \le \eta_{\min} \le \eta_{\max} \le 1$, $0 < \delta < \sigma < 1 < \rho$ and $\mu > 0$. Write $g_k = \nabla f(x_k)$ and $\nabla f(x)d = \langle \nabla f(x), d\rangle$. The Nonmonotone Line Search Algorithm (NLSA) keeps weights $Q_k$ and reference values $C_k$:

with $\eta_k \in [\eta_{\min}, \eta_{\max}]$ chosen freely at each step. A step $\alpha_k$ is accepted either by the nonmonotone Wolfe conditions

or by the nonmonotone Armijo rule $\alpha_k = \bar\alpha_k \rho^{h_k}$, where $\bar\alpha_k > 0$ is a trial step and $h_k$ is the largest integer such that the first inequality holds and $\alpha_k \le \mu$. With $\eta_k = 0$ one recovers the monotone rules.

The direction assumption asks for constants $c_1, c_2 > 0$ with $g_k^{\mathsf T} d_k \le -c_1\|g_k\|^2$ and $\|d_k\| \le c_2\|g_k\|$. The function $f$ is strongly convex with constant $\gamma > 0$ if

Let $x^*$ be the minimizer, $\mathcal L = \{x : f(x) \le f(x_0)\}$, $d_{\max} = \sup_k\|d_k\|$, and $\bar{\mathcal L}$ the set of points within distance $\mu d_{\max}$ of $\mathcal L$.

Formalization targets

Goal: Theorem 3.1

Let $f$ be strongly convex with minimizer $x^*$, let $\nabla f$ be Lipschitz continuous on bounded sets, let $\eta_{\max} < 1$, let the directions satisfy the direction assumption at every iteration, and let $\alpha_k \le \mu$ for all $k$. Then there is $\theta \in (0,1)$ with

The goal fixes no value of $\theta$: it asserts only the existence of a linear rate.

Milestones

In the paper's order of use:

1. Lemma 1.1: $f(x_k) \le C_k \le A_k$ when $g_k^{\mathsf T}d_k \le 0$ for each $k$.
2. $C_{k+1} \le C_k$, so all iterates lie in $\mathcal L$.
3. (3.4): $f(x) - f(x^*) \le \gamma\|\nabla f(x)\|^2$.
4. (2.15): $Q_{k+1} \le 1/(1 - \eta_{\max})$.
5. (3.6): $f(x_{k+1}) \le C_k - \beta\|g_k\|^2$, with

6. (3.7): $\|g_{k+1}\| \le b\|g_k\|$, $b = 1 + \mu c_2 L$.
7. (3.8): the explicit contraction

Here $L$ is a Lipschitz constant of $\nabla f$ on $\bar{\mathcal L}$. A further result on the same definitions is Theorem 3.2: if $f(x_k)$ converges R-linearly with ratio $\theta < \eta_{\min}$ inside a compact convex set on which $f$ is strongly convex, then the sufficient decrease condition with reference value $C_k$ holds for all large $k$.

Significance

Theorem 3.1 shows that averaging past function values costs nothing in the rate: on strongly convex functions the nonmonotone method keeps the linear rate of monotone descent, for any direction sequence satisfying the direction assumption (steepest descent, L-BFGS with bounded condition numbers, and so on). Theorem 3.2 is the converse side: for weights close enough to 1, the averaged test eventually accepts the steps of any R-linearly convergent iteration of this kind. The paper contrasts this with the max-based test of Grippo et al.

These results are proved in the paper. As far as the platform catalogue shows, no line search with the Wolfe conditions or a nonmonotone reference value has been formalized. The only related item is a monotone backtracking gradient descent rate, which is a different theorem. Machine-checked proofs would give reusable Lean statements of the nonmonotone Wolfe and Armijo rules and of the averaged reference value. They would also give the explicit constants $\beta$, $b$ and $\theta$ in checked form, and a checked record of the repair of the printed statement described below.

Difficulty

The obvious argument would show that $f(x_k) - f(x^*)$ contracts at each step. It fails: the method is nonmonotone, and $f(x_{k+1})$ may exceed $f(x_k)$. The quantity that contracts is $C_k - f(x^*)$, and only $C_k$ is controlled by the line search. The contraction must be derived by relating $\|g_k\|^2$ to $C_k - f(x^*)$ in two regimes, and the second regime needs a bound on $f(x_{k+1}) - f(x^*)$ from the gradient at the previous iterate. That bound requires the Lipschitz constant on a region containing every point the line search examines, which is why the region $\bar{\mathcal L}$ and the step bound $\mu$ enter. In Lean, the sufficient decrease (3.6) also rests on the step-length lower bounds of Lemma 2.1 for both rules, including the integer-exponent Armijo rule with its maximality condition.

Formalization scope

Conventions:

• The space is EuclideanSpace ℝ (Fin n), $f$ is ContDiff ℝ 1, and $\nabla f(x)d$ is ⟪gradient f x, d⟫_ℝ.
• A run is infinite, uses one rule throughout (Wolfe or Armijo), and has arbitrary directions subject to the stated hypotheses.
• $Q_k$ and $C_k$ are defined by recursion from the run.
• The Armijo exponent ranges over $\mathbb{Z}$ and "largest" is IsGreatest.
• $d_{\max}$ and distances are taken in $[0,\infty]$, so unbounded directions make $\bar{\mathcal L}$ the whole space.
• Strong convexity keeps the paper's constant $\gamma$, the inverse modulus.
• "Lipschitz on bounded sets" means that every bounded set admits a Lipschitz constant for $\nabla f$.

Repair of the printed statement: the paper's direction assumption holds only for all sufficiently large $k$, but Theorem 3.1 concludes (3.5) for each $k$, and its proof uses the assumption at every $k$. As printed the theorem is false: $d_0 = 0$ with the Wolfe step $\alpha_0 = 1$ gives $x_1 = x_0$, which violates (3.5) at $k = 1$ whenever $x_0 \ne x^*$. The goal therefore requires the direction assumption for every $k \ge 0$.

The step bound "there exists $\mu > 0$ with $\alpha_k \le \mu$" is stated with $\mu$ the algorithm's parameter. For the Armijo rule this holds by construction. The Wolfe rule does not use $\mu$, so nothing is lost.

Trivializing formalizations are ruled out:

• the printed hypotheses with "for each $k$" (false, as shown above);
• a $\theta$ allowed to equal 1, or an unspecified constant factor in front of $\theta^k$ (weaker than (3.5));
• a globally Lipschitz gradient, or a step bound different from the $\mu$ used to build $\bar{\mathcal L}$.

A complete development needs:

• the NLSA model and Lemma 1.1;
• the step-length lower bounds of Lemma 2.1 for both rules (via the descent lemma for Lipschitz gradients);
• the geometric bound on $Q_k$;
• boundedness of level sets of strongly convex functions.

The NLSA definitions are reusable by any later mission on nonmonotone line searches. Proofs of the milestones in any order are welcome, as are a proof of the counterexample to the printed statement and a proof that the platform theorem ConvexOptimization.strong_convexity_quadratic_lower_bound implies (3.4).

Selected references

• H. Zhang, W. W. Hager, A Nonmonotone Line Search Technique and Its Application to Unconstrained Optimization, SIAM J. Optim. 14(4):1043–1056, 2004. https://doi.org/10.1137/S1052623403428208
• L. Grippo, F. Lampariello, S. Lucidi, A Nonmonotone Line Search Technique for Newton's Method, SIAM J. Numer. Anal. 23(4):707–716, 1986. https://doi.org/10.1137/0723046
• Y.-H. Dai, On the Nonmonotone Line Search, J. Optim. Theory Appl. 112:315–330, 2002 (reference [4] of the paper).

Motivation

In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first $n$ rounds.

The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret $O(d\sqrt n\log^{3/2} n)$ with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.

Setting

Fix a dimension $d \ge 1$ and an unknown parameter $\theta_* \in \mathbb R^d$. In round $t = 1, 2, \dots$ the learner is given a nonempty decision set $D_t \subseteq \mathbb R^d$, chooses $X_t \in D_t$, and observes the reward

There is a filtration $\{F_t\}_{t \ge 0}$ such that $X_t$ is $F_{t-1}$-measurable and $\eta_t$ is $F_t$-measurable and conditionally $R$-sub-Gaussian: $\mathbf E[e^{\lambda\eta_t} \mid F_{t-1}] \le \exp(\lambda^2R^2/2)$ for all $\lambda \in \mathbb R$, with $R \ge 0$ fixed.

For a regularization parameter $\lambda > 0$ let $\overline V_t = \lambda I + \sum_{s=1}^t X_sX_s^\top$ and let $\widehat\theta_t = \overline V_t^{-1}\sum_{s=1}^t Y_sX_s$ be the regularized least-squares estimate. With $\|v\|_A = \sqrt{v^\top A v}$ and a known bound $\|\theta_*\|_2 \le S$, the confidence ellipsoid is

The OFUL algorithm chooses, in round $t$, a pair $(X_t, \widetilde\theta_t)$ maximizing $\langle x, \theta \rangle$ over $D_t \times C_{t-1}$. The pseudo-regret is $R_n = \sum_{t=1}^n \langle x^*_t - X_t, \theta_* \rangle$, where $\langle x^*_t, \theta_*\rangle = \max_{x\in D_t}\langle x,\theta_*\rangle$.

Formalization targets

Goal: Theorem 3, the regret of OFUL

If $\|X_t\|_2 \le L$, $\langle x, \theta_*\rangle \in [-1,1]$ for all $x \in D_t$, and $\lambda \ge \max(1, L^2)$, then for every $\delta > 0$, with probability at least $1 - \delta$,

Milestone: Theorem 1, the self-normalized bound

For any positive definite $V$, $\overline V_t = V + \sum_{s\le t}X_sX_s^\top$ and $S_t = \sum_{s \le t}\eta_sX_s$: with probability at least $1-\delta$, for all $t \ge 0$,

Milestones: Theorem 2, the confidence ellipsoids

With probability at least $1 - \delta$, $\theta_* \in C_t$ for all $t \ge 0$ (first claim). If $\|X_t\|_2 \le L$, then with probability at least $1-\delta$, for all $t$, $\|\widehat\theta_t - \theta_*\|_{\overline V_t} \le R\sqrt{d\log((1 + tL^2/\lambda)/\delta)} + \lambda^{1/2}S$ (second claim, stated here for $d \ge 2$).

Significance

Theorem 3 bounds the regret of OFUL by $O(d\sqrt n\log n)$ with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.

All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases $V = \lambda I$, $R = 1$, $\delta < 1$ of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.

Difficulty

The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence $X_t$ has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix $\overline V_t$, which is itself built from the adaptively chosen actions; a bound for each fixed $t$ does not give it.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and $\|x\|_A$ is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed $t+1$ for $t : ℕ$, so sums over $s \le t$ are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy $R^2$) requires; this is an added hypothesis. Every "with probability at least $1-\delta$, for all $t$" is stated as an outer-measure bound $\le \delta$ on the failure event, with the time quantifier inside the event. $\det(\cdot)^{1/2}$ is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.

OFUL is a predicate on the whole process: in every round the chosen pair maximizes $\langle x,\theta\rangle$ over $D_t \times C_{t-1}$, with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward $\langle x^*_t, \theta_*\rangle$ is the supremum over $D_t$, finite because of the reward bound.

Two corrections to the printed Theorem 3 are made and disclosed. The printed $nL/d$ is replaced by $nL^2/d$, which is what the determinant–trace bound $\det\overline V_n \le (\lambda + nL^2/d)^d$ gives; for $L \le 1$ the corrected bound implies the printed one. The hypothesis $\lambda \ge \max(1, L^2)$ is added: for $\lambda < 1$ the printed logarithm can be negative, and the printed bound would then assert $R_n \le 0$. In the second claim of Theorem 2, $d \ge 2$ is added, because at $d = 1$ the claim does not follow from the first claim and the paper's proof is not available.

The goal is a probability bound over the noise, not the pathwise statement "if $\theta_* \in C_{t-1}$ for all $t$ then $R_n \le \dots$". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same $\delta$ as the conclusion.

Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on $\mathbb R^d$, log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general $V$ and $R$, and reusable determinant lemmas are all welcome.

Selected references

• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://proceedings.neurips.cc/paper/2011
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT, 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 19–20. https://doi.org/10.1017/9781108571401

Motivation

A cooperative game with transferable utility assigns to every coalition of players the total payoff the coalition can secure on its own. Two solution concepts for such games go back to the foundations of game theory: the core, the set of payoff divisions no coalition can improve upon, and the stable set (von Neumann–Morgenstern solution), a set of divisions that is internally consistent and externally absorbing under the relation of domination. For general games the two concepts behave badly: the core may be empty, stable sets may fail to exist (Lucas 1968), and when they exist there are usually many of them.

Lloyd Shapley's paper Cores of Convex Games (Int. J. Game Theory 1, 1971) isolates a class of games, the convex games (supermodular characteristic functions), on which all of this becomes well behaved. Convex games arise in cost allocation, in bankruptcy and airport problems, in scheduling and sequencing games, and in any setting with increasing returns to cooperation; the supermodular functions behind them are the same objects studied as polymatroid rank functions in combinatorial optimization (Edmonds 1970). For such games the paper shows that the core is nonempty, that its faces fit together in a rigid combinatorial pattern, that its vertices are exactly the marginal-contribution vectors, and that the core is the unique stable set.

Setting

Let $N=\{1,\dots,n\}$ be a finite set of players. A game is a function $v$ from subsets of $N$ to the reals with $v(\emptyset)=0$. It is convex if

A payoff vector is $a\in\mathbb R^N$, and $a(S)=\sum_{i\in S}a_i$. It is feasible if $a(N)\le v(N)$. The core $C$ is the set of feasible $a$ with $a(S)\ge v(S)$ for every $S\subseteq N$; in particular $a(N)=v(N)$ on $C$.