Motivation

Online convex optimization models repeated decision making against an unknown, possibly adversarial environment: in each round $t=1,\dots,T$ a player picks a point $x_t$ of a convex set $\mathcal P\subseteq\mathbb R^n$, and only then learns a convex cost function $f_t$ and pays $f_t(x_t)$. Performance is measured by regret, the excess of the total cost over that of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that online gradient descent has regret $O(\sqrt T)$ for arbitrary convex costs with bounded gradients, and this rate cannot be improved in general.

Many costs met in practice have more curvature than bare convexity. The log-loss $f(x)=-\log(x^\top a)$ of universal portfolio management (Cover, Math. Finance 1991) is not strongly convex, but it is exp-concave. Hazan, Agarwal and Kale (Mach Learn 69, 2007) gave the first efficient algorithms with regret logarithmic in $T$ for exp-concave costs. This mission formalizes the second of their algorithms, the Online Newton Step (ONS), and its regret bound (Theorem 2 of the paper). ONS is the basis of later second-order online methods and appears as a standard algorithm in textbooks on online learning.

Timeline:

• 2003 — Zinkevich: $O(\sqrt T)$ regret for general convex costs by online gradient descent.
• 2006–2007 — Hazan, Agarwal, Kale (COLT 2006; Mach Learn 2007): $O(\log T)$ regret for strongly convex costs by gradient descent, and $O(n\log T)$ regret for exp-concave costs by ONS, Follow the Approximate Leader, and exponentially weighted online optimization.
• 2016 — Hazan, Introduction to Online Convex Optimization (Found. Trends Optim., arXiv:1909.05207): textbook treatment of ONS with modified parameters.

Setting

The decision set $\mathcal P\subseteq\mathbb R^n$ is nonempty, closed, bounded and convex, and $D$ bounds its diameter: $\|x-y\|\le D$ for all $x,y\in\mathcal P$, with the Euclidean norm. The costs $f_1,f_2,\dots$ are real functions, differentiable at every point of $\mathcal P$, with gradient bound $\|\nabla f_t(x)\|\le G$ on $\mathcal P$. A cost is $\alpha$-exp-concave ($\alpha>0$) if $x\mapsto\exp(-\alpha f_t(x))$ is concave on $\mathcal P$.

For a matrix $A$, the generalized projection $\Pi^A_{\mathcal P}(y)$ is a point of $\mathcal P$ minimising $(y-x)^\top A(y-x)$ over $x\in\mathcal P$.

The Online Newton Step fixes

$$\beta=\tfrac12\min\Big\{\frac1{4GD},\alpha\Big\},\qquad \varepsilon=\frac1{\beta^2D^2},$$

writes $\nabla_t=\nabla f_t(x_t)$ and $A_t=\sum_{i=1}^t\nabla_i\nabla_i^\top+\varepsilon I_n$, plays an arbitrary $x_1\in\mathcal P$, and then

$$x_{t+1}=\Pi^{A_t}_{\mathcal P}\Big(x_t-\frac1\beta A_t^{-1}\nabla_t\Big).$$

The regret after $T$ rounds against a comparator $u\in\mathcal P$ is $\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)$; the paper's regret is its maximum over $u\in\mathcal P$.

In Lean the objects are LogRegretOCO.ONS.onsBeta, onsEps, onsMatrix, IsGenProj and IsONSRun, with the regularised Gram matrix regGram and the quadratic form quadForm.

Formalization targets

Goal: Theorem 2 with $n\log T\ge4$

For every run of ONS, every horizon $T$ with $n\log T\ge 4$, and every $u\in\mathcal P$,

$$\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)\le 5\Big(\frac1\alpha+GD\Big)\,n\log T.$$

The added condition $n\log T\ge4$ is what makes the printed constant correct (see Formalization scope).

Milestones

1. Lemma 3 (p. 177): for $0<\beta\le\frac12\min\{1/(4GD),\alpha\}$ and $x,y\in\mathcal P$,

$$f(x)\ge f(y)+\nabla f(y)^\top(x-y)+\tfrac\beta2\big(\nabla f(y)^\top(x-y)\big)^2 .$$

2. Lemma 8 (p. 188): for convex $\mathcal P$, $A\succeq0$, $z=\Pi^A_{\mathcal P}(y)$ and $a\in\mathcal P$: $(y-a)^\top A(y-a)\ge(z-a)^\top A(z-a)$.
3. The display on p. 178: for every run of ONS and $u\in\mathcal P$,

$$\sum_{t=1}^T\big(f_t(x_t)-f_t(u)\big)\le\frac1{2\beta}\sum_{t=1}^T\nabla_t^\top A_t^{-1}\nabla_t+\frac1{2\beta}.$$

4. Lemma 12 (p. 191): for $A\succeq B\succ0$, $A^{-1}\bullet(A-B)\le\log(|A|/|B|)$.
5. Lemma 11 (p. 190): if $\|u_t\|\le r$, $\varepsilon>0$ and $V_t=\sum_{\tau\le t}u_\tau u_\tau^\top+\varepsilon I_n$, then $\sum_{t=1}^Tu_t^\top V_t^{-1}u_t\le n\log(r^2T/\varepsilon+1)$.

Significance

Theorem 2 shows that exp-concavity alone, without strong convexity, suffices for regret logarithmic in $T$, at a per-round cost of one rank-one matrix update and one generalized projection. Its consequences include logarithmic regret for universal portfolio selection with a polynomial-time algorithm, and, by online-to-batch conversion, fast rates for stochastic exp-concave optimization. Lemma 11 (the elliptical potential bound) is used well beyond this paper, in linear bandits and online regression.

The result has been proved on paper since 2007. The remaining work is its machine-checked proof: the potential argument, the log-determinant inequality and the generalized-projection inequality for positive semidefinite matrices. As far as is known, none of these results is formalized in Mathlib. Prove2Me holds a related elliptical potential lemma for linear bandits (BanditAlgorithm.elliptical_potential_lemma, with $V_{t-1}$ and a $\min(1,\cdot)$, a different statement) and the Euclidean case $A=I$ of Lemma 8 (UnderstandingML.projection_lemma). The textbook version of ONS (OnlineConvexOpt.SecondOrder.online_newton_step_regret, with $\gamma=\frac12\min\{1/(GD),\alpha\}$ and bound $2(1/\alpha+GD)n\log T$) is an open private draft with different parameters.

Difficulty

The obvious route to logarithmic regret, the gradient-descent argument of Theorem 1 with step sizes $1/(Ht)$, needs a uniform lower bound $H>0$ on the Hessians. Exp-concave costs such as the log-loss have no such bound: their curvature vanishes in directions orthogonal to the gradients seen so far. The analysis therefore has to track curvature only along the observed gradient directions. This requires a matrix-valued potential $\sum_t\nabla_t^\top A_t^{-1}\nabla_t$ and a projection in the norm of $A_t$ rather than the Euclidean norm. The Euclidean projection inequality does not transfer to this norm, which changes from round to round. Bounding the potential requires determinant inequalities for positive definite matrices. The analytic facts are elementary, but their Lean statements involve the interaction of EuclideanSpace, Matrix.mulVec, Matrix.inv and Matrix.det.

Formalization scope

Points live in EuclideanSpace ℝ (Fin n), so all norms are Euclidean; matrices are Matrix (Fin n) (Fin n) ℝ acting on coordinate vectors. Rounds are 1-based: sums run over Finset.Icc 1 T and the index $0$ is unused. Cost functions are ambient functions $\mathbb R^n\to\mathbb R$, differentiable at the points of $\mathcal P$, with $\nabla f_t$ given by Mathlib's gradient. The paper's standing assumptions of convexity and twice differentiability are not needed and are omitted. $D$ enters only as an upper bound on distances in $\mathcal P$. The generalized projection is a predicate that every minimiser satisfies, and ONS is the predicate IsONSRun on the whole trajectory, so the goal covers every tie-break and every adaptive adversary.

Corrections and added hypotheses:

• Theorem 2 is false as printed at $T=1$. Take $n=1$, $\mathcal P=[-1,1]$, $f_1(x)=x^2$, $\alpha=\frac12$, $G=D=2$ and $x_1=1$: the regret is $1$ and the bound is $0$. The paper's proof gives $4(1/\alpha+GD)(n\log T+1)$ for $T\ge2$; the final sentence drops the additive $1/(2\beta)$ of the p. 178 display. The goal adds $n\log T\ge4$, under which the printed constant $5$ follows.
• $G,D,\alpha>0$ are assumed wherever $\beta$ or $\varepsilon$ appear: they are the non-degeneracy the formulas presuppose (in Lean, $1/0=0$).
• Lemma 3 adds $0<\beta$; the proof divides by $\beta$.
• Lemma 11 adds $\varepsilon>0$ and reads the printed $\sum_{\tau=1}^tu_tu_t^\top$ as $\sum_{\tau=1}^tu_\tau u_\tau^\top$.
• Lemma 12's product $\bullet$ is the entrywise inner product $\sum_{i,j}C_{ij}E_{ij}$, written out as a double sum.
• The printed "$f_t:\mathcal P\to\mathbb R^n$" is read as $f_t:\mathcal P\to\mathbb R$, and "$\Pi^{A_t}_{S_n}$" on p. 177 as $\Pi^{A_t}_{\mathcal P}$.

Regret is stated against every comparator $u\in\mathcal P$, never as a real infimum ⨅ over $\mathcal P$, which is junk-valued in Lean on unbounded or empty sets. The goal is a statement about runs of the paper's algorithm with the paper's $\beta$, $\varepsilon$ and $A_t$. A bound for an arbitrary sequence satisfying the p. 178 display would be a milestone, not Theorem 2. The hypotheses are jointly satisfiable: the closed unit ball with $f_t(x)=\|x\|^2/2$, $\alpha=1$, $G=1$, $D=2$ is a model.

A complete development needs: first-order conditions for concave functions on convex sets at boundary points; the optimality condition for minimising a convex quadratic over a convex set; spectral facts about symmetric positive definite matrices (square roots, eigenvalues, $\operatorname{tr}$ and $\det$); and the telescoping of log-determinants. Lemmas 8, 11 and 12 are reusable beyond this mission, in the sibling missions of this series (Follow the Approximate Leader) and in linear-bandit analyses. Proofs of any milestone are welcome, as are alternative proofs of Lemma 12 through concavity of $\log\det$.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• T. M. Cover, Universal portfolios, Mathematical Finance 1 (1991), 1–29. https://doi.org/10.1111/j.1467-9965.1991.tb00002.x
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization 2 (2016); 2nd ed. arXiv:1909.05207. https://arxiv.org/abs/1909.05207

Motivation

The sample complexity of a learning problem is the number of labelled examples needed to learn to a prescribed accuracy with a prescribed confidence. In Valiant's probably approximately correct (PAC) model it is the basic quantity of statistical learning theory: it says how much data is necessary and sufficient, as a function of the complexity of the hypothesis class, when the target concept belongs to that class (the realizable case).

For a class of Vapnik–Chervonenkis (VC) dimension $d$ the answer was known up to a logarithmic factor for about 25 years:

• 1982–1989. Vapnik (1982) and Blumer, Ehrenfeucht, Haussler and Warmuth (J. ACM 1989) showed that any learner that outputs a classifier consistent with the sample succeeds with $O\left(\frac1\varepsilon\left(d\log\frac1\varepsilon+\log\frac1\delta\right)\right)$ examples.
• 1989. Ehrenfeucht, Haussler, Kearns and Valiant (Inform. Comput. 1989) together with Blumer et al. proved the lower bound $\Omega\left(\frac1\varepsilon\left(d+\log\frac1\delta\right)\right)$ for every learner.
• 1994. Haussler, Littlestone and Warmuth (Inform. Comput. 1994) showed $\mathcal M(\varepsilon,\delta)=O\left(\frac d\varepsilon\mathrm{Log}\frac1\delta\right)$ with a variant of the one-inclusion graph predictor, which is sometimes better but also does not match the lower bound.
• 2007–2015. The gap was closed for restricted classes, such as intersection-closed classes (Auer and Ortner 2007; Darnstädt 2015), but not for classes such as linear separators.
• 2015. Simon (COLT 2015) analysed a majority vote of consistent classifiers trained on disjoint parts of the data and reduced the logarithmic factor to a very slowly growing function of $1/\varepsilon$.
• 2016. Hanneke (JMLR 17(38), 2016; arXiv:1507.00473) removed the logarithmic factor for every class, with an explicit learner: a majority vote of consistent classifiers trained on recursively constructed, overlapping subsamples.

Setting

Let $\mathcal X$ be a set with a $\sigma$-algebra and $\mathcal Y=\{-1,+1\}$. A classifier is a measurable map $h:\mathcal X\to\mathcal Y$; the concept space $\mathbb C$ is a set of classifiers with $|\mathbb C|\ge3$. A finite sequence $x_1,\ldots,x_k$ is shattered by $\mathbb C$ if every labelling $y_1,\ldots,y_k$ is realized by some $h\in\mathbb C$; the VC dimension $d$ is the largest such $k$, assumed finite (then $d\ge1$).

A data set is a finite sequence $S$ of pairs in $\mathcal X\times\mathcal Y$, and $\mathbb C[S]$ is the set of $h\in\mathbb C$ with $h(x)=y$ for all $(x,y)\in S$. For a probability measure $P$ and a target $f^\star\in\mathbb C$, the error of $h$ is $\mathrm{er}_P(h;f^\star)=P(\mathrm{ER}(h))$, where $\mathrm{ER}(h)=\{x:h(x)\ne f^\star(x)\}$. A learning algorithm maps data sets to classifiers.

For $\varepsilon,\delta\in(0,1)$, the sample complexity $\mathcal M(\varepsilon,\delta)$ (Definition 1) is the least $m$ such that some algorithm $\mathcal A$ satisfies, for every probability measure $\mathcal P$ on $\mathcal X$ and every $f^\star\in\mathbb C$, with $X_1,\ldots,X_m$ independent with law $\mathcal P$,

$$\mathbb P\left(\mathrm{er}_{\mathcal P}\left(\mathcal A\big((X_i,f^\star(X_i))_{i\le m}\big);f^\star\right)\le\varepsilon\right)\ge1-\delta,$$

and $\mathcal M(\varepsilon,\delta)=\infty$ if there is no such $m$.

The learner of the paper uses three ingredients. A sample-consistent learner $L$ returns an element of $\mathbb C[S]$ whenever that set is nonempty. The majority vote is $\mathrm{Majority}(h_1,\ldots,h_k)(x)=2\mathbb 1\left[\sum_i h_i(x)\ge0\right]-1$. The subsample algorithm $\mathbb A(S;T)$ returns $\{S\cup T\}$ if $|S|\le3$; otherwise it splits $S$ into a head $S_0$ of $|S|-3\lfloor|S|/4\rfloor$ points and three blocks $S_1,S_2,S_3$ of $\lfloor|S|/4\rfloor$ points, and returns the concatenation of $\mathbb A(S_0;S_2\cup S_3\cup T)$, $\mathbb A(S_0;S_1\cup S_3\cup T)$ and $\mathbb A(S_0;S_1\cup S_2\cup T)$. The learned classifier is $\hat h=\mathrm{Majority}(L(\mathbb A(S;\emptyset)))$.

Formalization targets

Goal: Theorem 2 with its explicit constant

$$\mathcal M(\varepsilon,\delta)\le\frac{1800}{\varepsilon}\left(d+\ln\left(\frac{18}{\delta}\right)\right)\qquad(\varepsilon,\delta\in(0,1)).$$

The paper states Theorem 2 as $\mathcal M(\varepsilon,\delta)=O\left(\frac1\varepsilon\left(d+\mathrm{Log}\frac1\delta\right)\right)$ with a numerical constant; its proof establishes the bound above with $c=1800$, and that explicit form is the goal. Improving the constant would give a stronger theorem; this statement stays valid.

Milestones, in attack order

1. Lemma 4 (Blumer et al. 1989): with probability $1-\delta$, every $h\in\mathbb C[\{(Z_i,f^\star(Z_i))\}_{i\le m}]$ has $\mathrm{er}_P(h;f^\star)\le\frac2m\left(d\,\mathrm{Log}_2\frac{2em}d+\mathrm{Log}_2\frac2\delta\right)$.
2. Lemma 5: $a\ln(c_1(c_2+b/a))\le a\ln(c_1(c_2+e))+b/e$ for $a,b,c_1\ge1$, $c_2\ge0$.
3. Structure of $\mathbb A$: every subsample $\hat S$ satisfies $T\subseteq\hat S\subseteq S\cup T$, and the number of subsamples does not depend on $T$.
4. The Chernoff event $E_i''$: if $Q(E)\ge\frac{23}n\ln\frac9\delta$, then with probability $1-\delta/9$ at least $\frac7{10}Q(E)n$ of $n$ i.i.d. points fall in $E$.
5. The bound (8) and its comparison with $\frac{150}{m+1}\left(d+\ln\frac{18}\delta\right)$.
6. Majority averaging: $\mathrm{er}(h_{\mathrm{maj}})\le12\,\mathbb E\left[\mathcal P(\mathrm{ER}(h_I)\cap\mathrm{ER}(\tilde h))\right]$ for three equal-size committees.
7. Claim (9): with probability $1-\delta$, $\mathrm{er}_{\mathcal P}(\hat h_{m,T};f^\star)\le\frac{1800}{m+1}\left(d+\ln\frac{18}\delta\right)$.
8. Sample size (10): $\mathrm{Majority}(L(\mathbb A(\cdot;\emptyset)))$ is $(\varepsilon,\delta)$-PAC from $\left\lfloor\frac{1800}\varepsilon\left(d+\ln\frac{18}\delta\right)\right\rfloor$ examples.

Significance

Together with the classical lower bound, Theorem 2 gives $\mathcal M(\varepsilon,\delta)=\Theta\left(\frac1\varepsilon\left(d+\log\frac1\delta\right)\right)$: the realizable PAC sample complexity is determined up to a numerical constant by the VC dimension alone. It settles a question open since 1989, shows that the $\log\frac1\varepsilon$ factor in the classical bounds is an artifact of empirical risk minimization rather than of the learning problem, and supplies an explicit, simple learner that attains the optimal rate. Later work on optimal learners (majority votes over bagged or subsampled ERMs, optimal learning in other settings) builds on this construction.

The result is proved on paper. To our knowledge no proof assistant contains it, and the formal libraries lack parts of its infrastructure: the classical bound for consistent learners (Lemma 4), multiplicative Chernoff bounds for empirical counts, and conditioning on independent parts of an i.i.d. sample. This mission produces a machine-checked statement of the optimal bound with the paper's explicit constant, a verified formal model of the learner, and reusable components for these three.

Difficulty

The obvious approach is to sharpen the analysis of a single consistent classifier, as in the classical bound. Decades of effort along these lines did not remove the $\log\frac1\varepsilon$ factor, and the paper removes it only by aggregating many classifiers. The error of a majority vote is not controlled by the errors of its voters one at a time. The proof controls the probability that two voters trained on overlapping subsamples err at the same point, which requires tracking which parts of the sample are independent of which trained classifiers through a recursion of depth $\log_4 m$. In a formal development the difficult parts are the conditional-independence bookkeeping for random subsamples of a product measure, the induction over the sample size with a data set $T$ that varies with the level, and the numerical constants, which are tight (the key comparison is $149.9997<150$).

Formalization scope

• Representation. Labels are Bool (true for $+1$); data sets are lists and $\cup$ is concatenation; $\mathbb C$ is a set of measurable functions with $|\mathbb C|\ge3$; the VC dimension is a supremum in $\mathbb N\cup\{\infty\}$, assumed equal to a natural number $d$. The i.i.d. sample is the product measure $\mathcal P^m$ on $\mathrm{Fin}\,m\to\mathcal X$. "With probability at least $1-\delta$" is stated as a bound $\le\delta$ on the outer measure of the failure event. $\mathcal M$ takes values in $\mathbb N\cup\{\infty\}$, so the goal is stated as $\mathcal M(\varepsilon,\delta)\le\left\lfloor\frac{1800}\varepsilon\left(d+\ln\frac{18}\delta\right)\right\rfloor$, which is equivalent. Ties in the majority vote go to $+1$, as printed.
• Algorithms. $\mathcal M$ quantifies over deterministic algorithms that output measurable classifiers, chosen before $\mathcal P$ and $f^\star$ and seeing only the labelled sample. The paper also admits randomized algorithms (footnote 2), which can only lower $\mathcal M$, so the goal implies the paper's statement.
• Measurability. The paper assumes that every event in its probability claims is measurable (p. 3). The formalization makes this explicit with two hypotheses: the class is well-behaved (the event of Lemma 4 and the double-sample event of Blumer et al. are null-measurable for every distribution), and the base learner $L$ is jointly measurable in the sample and the point. Both hold for every countable class of measurable classifiers, with $L$ returning the first consistent classifier of an enumeration. Without the first hypothesis Lemma 4 fails for some classes of VC dimension 1.
• Ruled out. The following formalizations would make the goal trivial or weaker, and are not used here:
  • a sample complexity whose algorithm may depend on $\mathcal P$ or $f^\star$, which gives $\mathcal M\equiv0$;
  • a goal with an existential constant or a ceiling in place of $1800$ and the floor;
  • measurability hypotheses that no infinite class satisfies;
  • milestones 7–8 stated for an arbitrary family of subsamples instead of the algorithm $\mathbb A$.
• Needed infrastructure. VC theory for consistent learners (Lemma 4, via the double-sample argument), multiplicative Chernoff bounds for binomial counts, and conditioning of product measures on coordinate blocks. These are reusable beyond this mission. Contributions welcome: a proof of Lemma 4, the Chernoff milestone, the numerical milestone 5, and the majority-vote averaging step, each of which is independent of the others.

Selected references

• S. Hanneke, The Optimal Sample Complexity of PAC Learning, Journal of Machine Learning Research 17(38):1–15, 2016. arXiv:1507.00473v4
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4):929–965, 1989. doi:10.1145/76359.76371
• A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3):247–261, 1989. doi:10.1016/0890-5401(89)90002-3
• H. U. Simon, An almost optimal PAC algorithm, Proceedings of the 28th Conference on Learning Theory (COLT), PMLR 40:1552–1563, 2015. proceedings.mlr.press/v40/Simon15a
• D. Haussler, N. Littlestone, M. K. Warmuth, Predicting {0,1}-functions on randomly drawn points, Information and Computation 115(2):248–292, 1994. doi:10.1006/inco.1994.1097
• P. Auer, R. Ortner, A new PAC bound for intersection-closed concept classes, Machine Learning 66(2–3):151–163, 2007. doi:10.1007/s10994-006-8638-3
• V. Vapnik, Estimation of Dependences Based on Empirical Data, Springer, 1982.

Motivation

Where to hold safety stock in a multi-stage supply chain is a basic question of inventory planning. Graves and Willems (MSOM 2(1), 2000) optimize safety-stock placement under the guaranteed-service assumption: each stage quotes a service time to its customers and always meets it. That assumption makes the placement problem tractable, and it is the basis of the dynamic program in the body of the paper and of later work built on it. It also has a price. A stage that promises a service time must hold enough stock to keep the promise even when it would be cheaper to let a downstream stage absorb an occasional delay.

The paper's Appendix measures that price in the simplest setting where it can be computed exactly. The setting is a serial chain in which internal stages promise nothing and only the external customer is guaranteed 100% service. Its one theorem, called the Result, characterizes the optimal base stocks of this relaxed model in closed form. The paper then compares that policy with the guaranteed-service optimum on 36 test instances. The guaranteed-service counterpart of this serial model, Simpson's all-or-nothing property of optimal service times, is on Prove2Me as a separate statement (SupplyChainTheory.gs_all_or_nothing, from Snyder and Shen's textbook). This mission formalizes the other side of the comparison.

Setting

A serial supply chain has $N$ stages. Stage $1$ is the demand node and stage $i$ supplies stage $i-1$ for $i = 2, \dots, N$. Time is discrete, with periods $t \in \mathbb{Z}$. Stage $i$ has a deterministic lead time $T_i \in \mathbb{N}$ and a base stock $B_i \in \mathbb{R}$. It follows a base-stock policy: in each period it observes end-item demand and orders that amount from its supplier.

The end-item demand in period $t$ is $d(t)$. The window demand is $d(a, b] = d(a+1) + \dots + d(b)$, which is $0$ when $a \ge b$. The demand bound $D : \mathbb{N} \to \mathbb{R}$ gives $D(\tau)$, the maximum possible end-item demand over $\tau$ periods, with $D(0) = 0$.

The backlog $Q_i(t)$ is the amount the customer of stage $i$ has ordered but not yet received. It satisfies the recursion (A1):

$$Q_i(t) = \bigl[d(t - T_i, t] + Q_{i+1}(t - T_i) - B_i\bigr]^+, \qquad Q_{N+1} \equiv 0 .$$

Unrolling it gives the closed max-form (A2). The external customer receives 100% service when $Q_1(t) = 0$ for all $t$. When demand never exceeds its bound, this is ensured by the service constraints

$$B_1 + \dots + B_i \ge D(T_1 + \dots + T_i), \qquad i = 1, \dots, N. \tag{A3}$$

Let $h_i$ be the holding cost at stage $i$ and $e_i = h_i - h_{i+1}$ the echelon holding cost. After constant terms are dropped, the expected holding cost gives program $\mathbf P^*$:

$$\min_B\ \sum_{i=1}^N h_i B_i - \sum_{i=2}^N e_{i-1} E[Q_i] \quad\text{s.t. (A3) and } B_i \ge 0 .$$

Demand is random, and $E[Q_i]$ is the expected backlog at stage $i$ in a period $t$.

Formalization targets

Goal: the Result, Eq. (A6)

If the echelon holding costs are nonnegative and $D$ is nondecreasing, then an optimal solution of $\mathbf P^*$ is

$$B_1 = D(T_1), \qquad B_i = D(T_1 + \dots + T_i) - D(T_1 + \dots + T_{i-1}), \quad i = 2, \dots, N. \tag{A6}$$

Formally, (A6) is feasible, and for every period $t$ its objective value is at most that of every feasible vector. The goal names this vector and compares it with every feasible $B$. The weaker claim that "some optimal solution binds all of (A3)" would not be enough.

Milestones

1. Eq. (A2). The closed max-form of $Q_i(t)$, derived from the recursion (A1).
2. Eq. (A3). Under the demand bound $d(a, a+s] \le D(s)$, the constraints (A3) force $Q_1 \equiv 0$ (sufficiency).
3. (A6) is feasible and is the unique binding solution of (A3).
4. Backlog bounds under a transfer. Moving $\Delta \ge 0$ units of base stock from stage $k$ to stage $k+1$ leaves $E[Q_i]$ unchanged for $i > k+1$ and raises it by at most $\Delta$ for $i \le k$. It lowers $E[Q_{k+1}]$ by at most $\Delta$.
5. Eqs. (A7)–(A8). For $k < N$, the transfer that makes the $k$-th constraint binding keeps the vector feasible and does not raise the objective.
6. The case $k = N$. Lowering $B_N$ until the $N$-th constraint binds does not raise the objective.

Significance

The Result shows that, without guaranteed internal service, the optimal base stocks do not depend on the holding costs, provided the echelon costs are nonnegative. Each stage then covers exactly the increment of maximal demand that its own lead time adds. This closed form is the benchmark against which the paper measures the cost of guaranteed service: 26% more safety-stock holding cost on average over its test problems. The paper also remarks, without proof, that Rosling's transformation extends the Result to assembly systems.

The Result is proved in the paper. As far as is known, neither it nor the backlog identity (A2) has been machine-checked. A complete development would yield a verified model of serial base-stock backlogs under bounded demand. It would also verify an exchange argument that recurs in multi-echelon inventory theory: moving stock toward the customer, with echelon costs controlling the sign of the change.

Difficulty

The objective is not linear in $B$. Each $E[Q_i]$ is a convex, nonsmooth function of $B_i, \dots, B_N$ through the maximum in (A2), and the objective subtracts these terms, so $\mathbf P^*$ minimizes a concave function over a polyhedron. The obvious approaches are linear-programming duality and convex first-order optimality conditions on $\mathbf P^*$, and neither applies. The result is a comparison of objective values between arbitrary feasible vectors and (A6). It has to hold pathwise under every demand distribution, and it then has to be carried through expectations. The hypotheses the Result leaves implicit must be recovered from the rest of the paper. Two of them, stated below, are necessary.

Formalization scope

Stages are natural numbers read on the range $\{1, \dots, N\}$. Lead times are natural numbers cast to $\mathbb{Z}$. Base stocks, holding costs and the demand bound are real-valued. A base-stock vector is a function $\mathbb{N} \to \mathbb{R}$, and only indices $1, \dots, N$ are read. The backlog is defined by the recursion (A1), computed in $N + 1 - i$ steps, with $Q_i \equiv 0$ for $i > N$. The closed form (A2) is a theorem. Randomness is a probability space $(\Omega, \mu)$ with a demand path $d(\omega, \cdot)$ whose value in each period is integrable. The integrability of the backlog is not assumed; it follows from the integrability of demand.

The page's informal words are read as follows:

• "The echelon holding costs are nonnegative" means $h_i - h_{i+1} \ge 0$ for $1 \le i < N$, and $h_N \ge 0$, i.e. $e_N \ge 0$ with $h_{N+1} := 0$. The case $k = N$ of the proof uses $h_N \ge 0$. Without it the Result is false ($N = 1$, $h_1 < 0$).
• $D(0) = 0$ is the paper's convention (§2, p. 70) and is added as a hypothesis. Without it (A6) can be infeasible ($D \equiv -1$ is nondecreasing).
• "$D(\,)$ is a nondecreasing function" means Monotone D on $\mathbb{N}$.
• "An optimal solution to $\mathbf P^*$" means feasible, with objective at most that of every feasible vector.
• "$E[Q_i]$" means the expectation of $Q_i(t)$ at a fixed period $t$. Every statement holds for all $t$, and stationarity is not assumed. The paper writes $E[Q_i]$ without $t$ because its demand is stationary, and this reading is at least as strong.
• The demand bound $d(a, a+s] \le D(s)$ appears only in milestone 2. The Result does not use it, so it is not a hypothesis of the goal.
• Eq. (A3) is formalized in the sufficiency direction only. The page's necessity remark ("as we assume that the demand bounds can be realized") is not stated.

A non-integrable backlog would make its Bochner integral $0$ and erase the backlog terms of the objective. The formalization rules this out by assuming integrable demand, which makes the backlogs integrable; it does not assume the backlogs themselves integrable. Out of scope: the spanning-tree dynamic program of §5, the unproved remarks of §§3–4, the Rosling extension, the Kodak application and the computational study.

Useful contributions include a proof of (A2) by downward induction on stages, the integrability of $Q_i(t)$, the pathwise version of milestone 4, and the iteration argument that assembles milestones 3, 5 and 6 into the goal.

Selected references

• S. C. Graves and S. P. Willems, Optimizing Strategic Safety Stock Placement in Supply Chains, Manufacturing & Service Operations Management 2(1):68–83, 2000. https://doi.org/10.1287/msom.2.1.68.23267
• K. F. Simpson, In-Process Inventories, Operations Research 6(6):863–873, 1958. https://doi.org/10.1287/opre.6.6.863
• K. Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. https://doi.org/10.1287/opre.37.4.565
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, Wiley, 2nd ed., 2019. https://doi.org/10.1002/9781119584445

Motivation

Many combinatorial optimization problems ask for a subset of a finite ground set that maximizes a set function with diminishing returns: Max Cut and Max Directed Cut in graphs, facility location, maximum entropy sampling, and welfare problems in combinatorial auctions all fit this pattern. The common abstraction is the maximization of a submodular function, the discrete analogue of a concave function. Unlike the monotone case, where the objective only grows as elements are added, the non-monotone problem has no constraint at all and is still NP-hard, since Max Cut is a special case.

For Max Cut and Max Directed Cut, the simplest algorithm there is, putting every vertex on a side by an independent fair coin, already cuts half, respectively a quarter, of the optimum in expectation. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011; extended abstract at FOCS 2007) showed that this is not a feature of cut functions: the same random choice achieves the same factors for every nonnegative submodular function, and for every symmetric one. This mission formalizes that result, Theorem 2.1 of the paper, together with the two sampling lemmas on which it rests. The paper's other results (a nonadaptive 1/3-approximation, deterministic and smoothed local search, and query lower bounds) are the subjects of companion missions in the same series.

Setting

Let $X$ be a finite set with $n = |X|$ elements. A set function assigns a real number $f(S)$ to every subset $S \subseteq X$. It is submodular if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X,$$

equivalently if the marginal value $f(B \cup \{x\}) - f(B)$ of an element $x$ does not increase as the set $B$ grows. It is symmetric if $f(X \setminus S) = f(S)$ for every $S \subseteq X$; the cut function of an undirected graph is the standard example. The optimum is

$$OPT = \max_{S \subseteq X} f(S).$$

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; similarly $A(p)$ is the random subset of a fixed $A \subseteq X$. The Random Set Algorithm (RS) returns $R = X(1/2)$, a uniformly random subset of $X$, without querying $f$. Its expected value is the average of $f$ over all subsets,

$$\mathbf{E}[f(R)] = F(\tfrac12, \dots, \tfrac12) = \frac{1}{2^n} \sum_{S \subseteq X} f(S),$$

where $F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{i \notin S} (1 - x_i)$ is the multilinear extension of $f$, the expectation of $f$ on a random set that includes element $i$ independently with probability $x_i$.

Formalization targets

Goal: Theorem 2.1

For every nonnegative submodular $f : 2^X \to \mathbb{R}_+$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14\, OPT,$$

and if $f$ is in addition symmetric,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac12\, OPT.$$

Both parts form the goal, stated as one theorem. The constants $\tfrac14$ and $\tfrac12$ are exact, not asymptotic, and they are tight: the directed cut of a single arc attains $\tfrac14$, and the cut of a single edge attains $\tfrac12$.

Milestones

1. Lemma 2.2. For submodular $g : 2^X \to \mathbb{R}$, $A \subseteq X$ and $p \in [0,1]$,

$$\mathbf{E}[g(A(p))] \ge (1-p)\, g(\emptyset) + p\, g(A).$$

2. Lemma 2.3. For submodular $f : 2^X \to \mathbb{R}$, sets $A, B \subseteq X$ that need not be disjoint, independent samples $A(p)$, $B(q)$, and $p, q \in [0,1]$,

$$\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B).$$

3. The display in the proof of Theorem 2.1. For submodular $f : 2^X \to \mathbb{R}$ and every $S \subseteq X$, with $\bar S = X \setminus S$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14 f(\emptyset) + \tfrac14 f(S) + \tfrac14 f(\bar S) + \tfrac14 f(X).$$

The milestones need no sign on the function; nonnegativity enters only in the goal.

Significance

The result. Theorem 2.1 gives an algorithm that makes no query at all and is still a constant-factor approximation for unconstrained non-monotone submodular maximization. It sets the baseline that every later algorithm for the problem is measured against: the paper's own nonadaptive $\tfrac13$-algorithm and its local search algorithms with factors $\tfrac13$ and $\tfrac25$, followed by later work culminating in the tight $\tfrac12$-approximation of Buchbinder, Feldman, Naor and Schwartz (FOCS 2012). The paper also shows that $\tfrac14$ is optimal among nonadaptive algorithms required to return one of the queried sets, and that $\tfrac12$ is optimal for symmetric functions among all algorithms using polynomially many value queries, so both factors of Theorem 2.1 have a precise place in the complexity landscape. Lemma 2.3, the probabilistic inequality behind it, is reused in the analyses of the nonadaptive algorithm and of smooth local search.

Formalizing it. The result is proved, with a short proof. What this mission adds is a machine-checked version of the random-set guarantee and of the two sampling lemmas, stated for arbitrary finite ground sets and, for the lemmas, for real-valued submodular functions without a sign. To our knowledge none of these statements has a machine-checked proof; Mathlib has no theory of submodular set functions or of their multilinear extension.

Difficulty

The goal itself is a two-line consequence of the third milestone. The work sits in the lemmas and in one change of viewpoint.

Lemma 2.2 is not a pointwise statement: the random set $A(p)$ can be any subset of $A$, and $g$ can be smaller on it than both $g(\emptyset)$ and $g(A)$. The inequality holds only in expectation, and only because submodularity controls the marginal value of each element uniformly across the sets it can be added to. Lemma 2.3 needs a conditioning argument over two independent samples; the sets $A$ and $B$ may overlap, and on $A \cap B$ the union $A(p) \cup B(q)$ contains an element with probability $1 - (1-p)(1-q)$, so it is not the product distribution with probability $p$ on $A$ and $q$ on $B$. Finally, the third milestone requires identifying the uniform random subset $X(1/2)$ with the union of independent half-samples of $S$ and of its complement, as a statement about finite sums.

The obvious attempt at the goal, comparing $f(R)$ with $f(S^*)$ for an optimal $S^*$ set by set, fails: $f$ is not monotone, so a random set that contains most of $S^*$ may still have small value, and a random set can pick up elements that hurt.

Formalization scope

The ground set is a Lean type X with [Fintype X] [DecidableEq X]; subsets are Finset X and set functions are f : Finset X → ℝ. Submodularity is the lattice inequality of Definition 1.1, not the decreasing-marginals property. Nonnegativity, the paper's standing assumption $f : 2^X \to \mathbb{R}_+$, is the hypothesis ∀ S, 0 ≤ f S; it appears only in the goal. Symmetry is ∀ S, f Sᶜ = f S for all subsets, not only for an optimal one. $OPT$ is Finset.univ.sup' Finset.univ_nonempty f, a maximum over the always nonempty family of all subsets, so it is attained. The ground set may be empty; the goal holds there too and no nonemptiness is assumed.

Expectations are written as exact finite sums, not as integrals. $\mathbf{E}[f(X(1/2))]$ is the multilinear extension F f (fun _ => 1/2). $\mathbf{E}[g(A(p))]$ is $\sum_{T \subseteq A} p^{|T|}(1-p)^{|A \setminus T|} g(T)$, and $\mathbf{E}[f(A(p) \cup B(q))]$ is the double sum over independent samples $S \subseteq A$, $T \subseteq B$ with the product of the two weights. The ranges $0 \le p \le 1$ and $0 \le q \le 1$, implied in the paper by the word "probability", are explicit hypotheses; Lemma 2.2 is false without them.

Trivializing formalizations are excluded: the weights are exactly those of the uniform distribution on all $2^n$ subsets, $OPT$ is the true maximum rather than the value at one fixed set, and $f$ is required to be both nonnegative and submodular.

Reusable infrastructure produced by a complete development: the multilinear extension of a set function and its expression as an expectation, product-weight identities for independent sampling of subsets (including the decomposition of $X(1/2)$ along a set and its complement), and Lemmas 2.2 and 2.3, which the companion missions on the nonadaptive algorithm and on smooth local search also need. Proofs of any milestone are welcome independently.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM Journal on Computing 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing non-monotone submodular functions, Proceedings of the 48th IEEE Symposium on Foundations of Computer Science (FOCS), 2007, pp. 461–471. https://doi.org/10.1109/FOCS.2007.29
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5):1384–1402, 2015 (FOCS 2012). https://doi.org/10.1137/130929205
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions — I, Mathematical Programming 14:265–294, 1978. https://doi.org/10.1007/BF01588971

Motivation

Stochastic programs are solved in practice on a finite set of scenarios: a discrete probability distribution $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ that approximates the true distribution of the uncertain data. The size of the resulting deterministic problem grows with $N$, and for multistage models it grows very fast, so $N$ is often reduced before solving. The question is which scenarios to delete and how to reweight the remaining ones so that the optimal value and solutions of the stochastic program change as little as possible.

Dupačová, Gröwe-Kuska and Römisch (Math. Program. Ser. A 95 (2003) 493–511) answered this with probability metrics. Stability results for stochastic programs bound the change of the optimal value by a Fortet–Mourier type distance, which is in turn bounded by a Kantorovich functional $\hat\mu_c$ (an optimal transport cost). Scenario reduction then becomes: find a measure $Q$ supported on a subset of the scenarios with $\hat\mu_c(P,Q)$ small. Section 3 of the paper solves the weight part of this problem in closed form. That result, together with the heuristics built on it (backward reduction and forward selection), became the standard scenario-reduction method, implemented for example in the GAMS tool SCENRED.

Setting

Let $\Omega$ be a set and $c:\Omega\times\Omega\to\mathbb R_+$ a cost function with $c(\omega,\tilde\omega)=0$ if and only if $\omega=\tilde\omega$, and $c(\omega,\tilde\omega)=c(\tilde\omega,\omega)$ (conditions (C1)–(C2), p. 498). The original distribution has scenarios $\omega_1,\dots,\omega_N\in\Omega$ with weights $p_i>0$ and $\sum_i p_i=1$. Write $c_{ij}=c(\omega_i,\omega_j)$.

A set $J\subset\{1,\dots,N\}$ of scenarios is deleted. The reduced measure is $Q=\sum_{j\notin J}q_j\delta_{\omega_j}$ with reduced weights $q_j\ge0$, $\sum_{j\notin J}q_j=1$. A transport plan from $P$ to $Q$ is a nonnegative matrix $(\eta_{ij})_{i\le N,\,j\notin J}$ with row sums $\sum_{j\notin J}\eta_{ij}=p_i$ and column sums $\sum_i\eta_{ij}=q_j$. The Kantorovich functional (10) is the value of this transportation problem,

$$D(J;q)=\min\Big\{\sum_{i}\sum_{j\notin J}c_{ij}\eta_{ij}:\ \eta\ \text{a transport plan from }P\text{ to }Q\Big\},$$

and $D_J=\min\{D(J;q): q\ \text{reduced weights}\}$ is the best distance achievable once $J$ is fixed. The optimal deletion problem (13) asks for $\min\{D_J:\#J=k\}$ for a given $1\le k<N$.

In the Lean development these objects are IsReducedWeight, IsTransportPlan, transportCost, transportValue ($D(J;q)$), optWeightsValue ($D_J$) and optimalDeletionValue (the value of (13)), all in the namespace ScenarioReduction.Redistribution.

Formalization targets

Goal: Theorem 2 (optimal weights), p. 500

For every $J\neq\{1,\dots,N\}$,

$$D_J=\min\Big\{D(J;q): q_j\ge0,\ \sum_{j\notin J}q_j=1\Big\}=\sum_{i\in J}p_i\min_{j\notin J}c(\omega_i,\omega_j),$$

and the minimum is attained at the optimal redistribution rule $\bar q_j=p_j+\sum_{i\in J_j}p_i$, where $J_j=\{i\in J: j(i)=j\}$ and $j(i)\in\arg\min_{j\notin J}c(\omega_i,\omega_j)$, for every such choice of $j(\cdot)$.

Milestones

1. Primal–dual representation of $D(J;q)$ (first display of the proof, p. 501): the transportation problem and its linear-programming dual both attain $D(J;q)$.
2. Lower bound (p. 501): $\sum_{i\in J}p_i\min_{k\notin J}c_{ik}\le D(J;q)$ for every feasible $q$.
3. Upper bound at $\bar q$ (p. 501): $\bar q$ is feasible and $D(J;\bar q)\le\sum_{i\in J}p_i\min_{j\notin J}c_{ij}$.
4. Theorem 3 (p. 501): for weights prescribed by $q_j=p_j+\lambda_jp_J$, $D(J;q)\le\sum_{i\in J}p_i\sum_{j\notin J}\lambda_jc(\omega_i,\omega_j)$, with equality if $\#J=1$ and $c$ satisfies the triangle inequality.
5. Theorem 4 (p. 503): the greedy recursions (16) and (17) give a lower and an upper bound for $\min\{D_J:\#J=k\}$, and the backward set $\{l_1,\dots,l_k\}$ is optimal under a nonemptiness condition.

Significance

Theorem 2 reduces the continuous part of scenario reduction to a formula: once the set of kept scenarios is chosen, the best reweighting is to move the mass of every deleted scenario to a nearest kept scenario, and the resulting distance is an explicit sum. This leaves only the combinatorial choice of $J$, which Theorem 4 brackets by two greedy procedures; these are the backward-reduction and forward-selection algorithms of the paper and of later work by Heitsch and Römisch. Theorem 3 covers the case in which the reduced weights are fixed by the modeller, for instance to keep a uniform distribution uniform.

The results are proved in the paper by elementary linear-programming arguments. As far as is known, none of them has a machine-checked proof. Formalizing them produces a verified finite transportation-problem layer with a general (not necessarily metric) cost and a deleted index set, and verified correctness certificates for the two standard scenario-reduction heuristics.

Difficulty

The upper bound of Theorem 2 is a direct construction. The content lies in the lower bound, which must hold for every reweighting $q$ simultaneously; this needs the dual side of the transportation problem, and the full primal–dual representation (Milestone 1) requires strong duality for a transportation problem with only the kept columns, which Mathlib does not provide in this form. A naive argument that bounds each plan row by row gives the lower bound directly for plans, but relating it to $D(J;q)$ as an infimum also requires that plans exist and that the infimum is attained. In Theorem 4, the recursions (16) and (17) are greedy and do not in general produce optimal sets; the lower bound works only because its inner minimum ranges over all $j\neq l$, not over the kept scenarios.

Formalization scope

Scenarios are indexed by Fin N (0-based), scenarios are a function ω : Fin N → Ω into an arbitrary type Ω, the cost is c : Ω → Ω → ℝ, and weights, plans and dual variables are real-valued functions on Fin N and Fin N × Fin N. Only the entries at kept indices $j\notin J$ enter any constraint, cost or objective. No measure theory is used: the index-level transportation problem is the paper's own representation of $\hat\mu_c$ for discrete measures (p. 495). Every theorem carries the standing assumptions of Section 3: $c\ge0$, (C1), (C2), $p_i>0$ and $\sum_ip_i=1$. Measurability of $c$ and conditions (C3) and (C4) concern $\Omega\subset\mathbb R^s$ and play no role for finitely supported measures; they are dropped, so the statements are more general than the page. The hypothesis $J\neq\{1,\dots,N\}$, implicit in Theorem 2, is stated explicitly; in Theorem 4, $1\le k<N$ plays this role.

$D(J;q)$ and $D_J$ are real infima (sInf) of transport costs and are only asserted about where the underlying sets are nonempty and bounded below; "min" is stated as attainment (IsLeast), not as an equality of infima. $D(J;q)$ is defined as the transportation problem and is not defined by the closed form $\sum_{i\in J}p_i\min_{j\notin J}c_{ij}$; under that definition Theorem 2 would be trivial, and it is ruled out here. Likewise the reduced-weight constraint does not force $q=\bar q$.

Needed infrastructure: finite transportation problems with nonnegativity and marginal constraints, existence of optimal plans (compactness of the feasible polytope), and LP duality for transportation problems. The transportation-problem layer is reusable beyond this mission. Contributions welcome: proofs of the milestones, a general strong-duality result for finite transportation problems, and the examples of p. 502 (single scenario deletion, keeping one scenario).

Selected references

• J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Math. Program. Ser. A 95 (2003) 493–511. https://doi.org/10.1007/s10107-002-0331-0
• S. T. Rachev, Probability Metrics and the Stability of Stochastic Models, Wiley, 1991.
• H. Heitsch, W. Römisch, Scenario reduction algorithms in stochastic programming, Comput. Optim. Appl. 24 (2003) 187–206. https://doi.org/10.1023/A:1021805924152
• W. Römisch, R. Schultz, Stability analysis for stochastic programs, Ann. Oper. Res. 30 (1991) 241–266. https://doi.org/10.1007/BF02204819

Motivation

Nash's equilibrium existence theorem assumes that each player's set of available strategies is fixed. Many social and economic systems do not work that way: a consumer's budget set depends on prices, which are the choices of another agent, and a firm's feasible production may depend on what other firms do. Gerard Debreu's A Social Equilibrium Existence Theorem (PNAS 38(10), 1952) proves that an equilibrium exists in such a system, called a social system or abstract economy (today also a generalized game). Here each agent's feasible actions depend on the actions of all the others.

Arrow and Debreu used this theorem to prove the existence of a competitive equilibrium (Econometrica 22(3), 1954). It is the standard existence result for generalized Nash equilibrium problems in operations research, where the feasible sets are coupled by shared constraints.

Timeline.

• 1928: von Neumann proves the minimax theorem for matrix games.
• 1941: Kakutani proves a fixed-point theorem for convex-valued maps with closed graphs on compact convex sets (Duke Math. J. 8, 1941).
• 1946: Eilenberg and Montgomery extend fixed-point theory to acyclic-valued maps on acyclic absolute neighbourhood retracts (Amer. J. Math. 68, 1946).
• 1950: Nash proves the existence of equilibrium points for finite games (PNAS 36, 1950).
• 1952: Debreu proves the theorem of this mission. He requires contractibility instead of convexity, and his payoffs take values in the completed real line.

Setting

There are finitely many agents $\iota=1,\dots,\nu$. Agent $\iota$ chooses an action $a_\iota$ in a set $\mathfrak A_\iota$, a subset of a finite-dimensional real space. A profile $a=(a_1,\dots,a_\nu)$ lies in $\mathfrak A=\mathfrak A_1\times\cdots\times\mathfrak A_\nu$. For each agent, $\bar a_\iota$ denotes the actions of the others, ranging over $\bar{\mathfrak A}_\iota=\prod_{j\ne\iota}\mathfrak A_j$.

Given $\bar a_\iota$, agent $\iota$ may only choose from a nonempty set $A_\iota(\bar a_\iota)\subseteq\mathfrak A_\iota$, a multi-valued function of the others' actions. Its graph is $G_\iota=\{(\bar a_\iota,a_\iota)\mid a_\iota\in A_\iota(\bar a_\iota)\}$. The payoff $f_\iota(\bar a_\iota,a_\iota)$ takes values in the completed real line $\overline{\mathbb R}=\mathbb R\cup\{-\infty,+\infty\}$. The best value available to agent $\iota$ and the set of constrained best responses are

$$\varphi_\iota(\bar a_\iota)=\max_{a_\iota\in A_\iota(\bar a_\iota)}f_\iota(\bar a_\iota,a_\iota),\qquad M_{\bar a_\iota}=\{a_\iota\in A_\iota(\bar a_\iota)\mid f_\iota(\bar a_\iota,a_\iota)=\varphi_\iota(\bar a_\iota)\}.$$

An equilibrium point is a profile $a^*$ such that, for every $\iota$, $a^*_\iota\in A_\iota(\bar a^*_\iota)$ and $f_\iota(a^*)=\varphi_\iota(\bar a^*_\iota)$.

The topological vocabulary is Debreu's §1:

• a convex cell is the convex hull of finitely many points;
• a geometric polyhedron is a finite union of convex cells;
• a polyhedron is a set homeomorphic to a geometric polyhedron;
• a nonempty set $Z$ is contractible if there is a continuous $H:[0,1]\times Z\to Z$ with $H(0,z)=z$ and $H(1,z)=z^0$ for a fixed $z^0\in Z$.

A multi-valued function is semicontinuous if its graph is closed.

Formalization targets

Goal: the THEOREM (p. 888)

Assume that for every $\iota$, $\mathfrak A_\iota$ is a contractible polyhedron, $G_\iota$ is closed, $f_\iota$ is continuous on $G_\iota$, $\varphi_\iota$ is continuous on $\bar{\mathfrak A}_\iota$, and $M_{\bar a_\iota}$ is contractible for every $\bar a_\iota$. Then

$$\exists\,a^*\in\mathfrak A\ \ \forall\iota:\quad a^*_\iota\in A_\iota(\bar a^*_\iota)\ \text{ and }\ f_\iota(\bar a^*_\iota,b)\le f_\iota(a^*)\ \text{ for all } b\in A_\iota(\bar a^*_\iota).$$

Milestones on the path of the proof

1. §1: products of two convex cells, of two geometric polyhedra, of two polyhedra and of two contractible sets are of the same kind.
2. $\mathfrak A$ is a contractible polyhedron, and $\phi(a)=M_{\bar a_1}\times\cdots\times M_{\bar a_\nu}$ is contractible for every $a$.
3. The LEMMA (p. 889): a semicontinuous multi-valued function $\phi:Z\to Z$ on a contractible polyhedron with contractible values has a fixed point $z^*\in\phi(z^*)$.
4. The set $M_\iota=\{(\bar a_\iota,a_\iota)\mid a_\iota\in M_{\bar a_\iota}\}$ is closed, and so is the graph $\Gamma$ of $\phi$.
5. $a^*\in\phi(a^*)$ holds exactly when $a^*$ is an equilibrium point.

Further results of the paper

• The Remark (p. 889) and its steps (α) and (β) (p. 890). If $G_\iota$ is compact and $f_\iota$ is continuous on it, then $\varphi_\iota$ is upper semicontinuous. If $A_\iota$ is moreover continuous at a point, $\varphi_\iota$ is lower semicontinuous, and hence continuous, there.
• The COROLLARY (p. 890). A continuous $f:X\times Y\to\overline{\mathbb R}$ on contractible polyhedra whose argmin sets $U_{x^0}$ and argmax sets $V_{y^0}$ are contractible has a saddle point, $\min_y f(x^0,y)=f(x^0,y^0)=\max_x f(x,y^0)$.

Significance

The result. The theorem gives an equilibrium for games in which one agent's choices constrain another's. This is the step that makes competitive equilibrium an equilibrium of a game: the market participant's price choice constrains the consumers' budget sets. The same result gives existence for generalized Nash equilibrium problems, including games with shared constraints. Replacing convexity by contractibility also admits non-convex best-response sets: a contractible set such as a star-shaped region or an arc qualifies. Nash's theorem for finite games and von Neumann's minimax theorem are special cases. With values in $\overline{\mathbb R}$, payoffs may take infinite values.

The formalization. The theorem was proved in 1952. None of it is formalized on the platform: neither the theorem itself, nor the LEMMA, nor the topological vocabulary of polyhedra and contractible sets used here. Brouwer's theorem is available on the platform as AGT.brouwer_fixed_point. Nash's existence theorem for finite games (AGT.nash_existence) and Sion's minimax theorem are also formalized. All of these assume convexity. The mission produces a machine-checked existence theorem for generalized games, together with a fixed-point theorem for set-valued maps with contractible values on polyhedra.

Difficulty

Most of the argument reduces to the LEMMA, which is a particular case of the Eilenberg–Montgomery fixed-point theorem. The usual route to Kakutani's theorem does not carry over: it approximates a convex-valued map by continuous selections and applies Brouwer's theorem on a convex set. Contractible values do not admit convex combinations of nearby values, and a contractible polyhedron need not be convex, so neither the selection step nor Brouwer on a simplex applies directly. Debreu cites the LEMMA without proof, and Mathlib has no fixed-point theorem for set-valued maps and none of the algebraic topology of polyhedra that the classical results rest on.

The remaining steps are point-set topology. The product milestones require building homeomorphisms and deformations on products of subspaces, and the closed-graph steps require care with continuity on $G_\iota$ as opposed to continuity everywhere.

Formalization scope

• Spaces and agents. Each $\mathfrak A_\iota$ is a subset of a finite-dimensional real normed space $E_\iota$, standing in for Debreu's "finite Euclidean spaces". The agents form a Fintype. Profiles live in $\prod_\iota\mathfrak A_\iota$. The others' actions $\bar a_\iota$ range over the product over the subtype $\{j\mid j\ne\iota\}$, so $A_\iota$ cannot depend on agent $\iota$'s own action. With a single agent this product is a point, and the theorem becomes the one-agent statement.
• Payoffs. The completed real line is Mathlib's EReal with its order topology. $\varphi_\iota$ is a supremum (sSup) in EReal; under the hypotheses it is attained, so it is Debreu's Max. No arithmetic in EReal is used anywhere.
• Polyhedra and contractible sets. A polyhedron is a subspace homeomorphic to a finite union of convex hulls of nonempty finite sets in some $\mathbb R^m$; polyhedra are therefore compact. Contractibility is Debreu's definition verbatim, and it includes nonemptiness.
• Hypotheses. Non-void values of $A_\iota$ are Debreu's standing assumption and are stated explicitly. Continuity of $f_\iota$ is required on $G_\iota$ only, and continuity of $\varphi_\iota$ on all of $\bar{\mathfrak A}_\iota$.

Three formalizations would be easier but are not this theorem: one that replaces contractible by convex (that is the Kakutani–Nash setting), one that maximizes over all of $\mathfrak A_\iota$ instead of $A_\iota(\bar a_\iota)$, and one that assumes a fixed point of $\phi$ or states only the closed-graph step. None of these is acceptable, and the LEMMA may not be weakened to convex domains or convex values.

The work needed includes a small library of polyhedra and contractible subsets, and closed-graph correspondences on products. The largest piece is a proof of the LEMMA, a fixed-point theorem that is reusable well beyond this mission. Proofs of any milestone, alternative routes to the LEMMA, and supporting lemmas on polyhedra, such as compactness, triangulation or being absolute neighbourhood retracts, are all welcome.

Selected references

• G. Debreu, A Social Equilibrium Existence Theorem, Proc. Natl. Acad. Sci. USA 38(10), 886–893, 1952. https://doi.org/10.1073/pnas.38.10.886
• S. Eilenberg and D. Montgomery, Fixed Point Theorems for Multi-Valued Transformations, Amer. J. Math. 68(2), 214–222, 1946. https://doi.org/10.2307/2371832
• E. G. Begle, A Fixed Point Theorem, Ann. of Math. 51(3), 544–550, 1950. https://doi.org/10.2307/1969367
• S. Kakutani, A Generalization of Brouwer's Fixed Point Theorem, Duke Math. J. 8(3), 457–459, 1941. https://doi.org/10.1215/S0012-7094-41-00838-4
• J. F. Nash, Equilibrium Points in N-Person Games, Proc. Natl. Acad. Sci. USA 36(1), 48–49, 1950. https://doi.org/10.1073/pnas.36.1.48
• K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 265–290, 1954. https://doi.org/10.2307/1907353