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