Operations Research

Motivation

In a two-person zero-sum game with objective randomization, whatever one player gains the other loses: the value $v$ of the game is the most player 1 can guarantee and the least player 2 can hold him to, and no arrangement between the players can give player 1 more than $v$ and player 2 more than $-v$ at the same time. Aumann's 1974 paper (doi:10.1016/0304-4068(74)90037-8) replaces objective coin flips by ordinary events of the world, about which players may hold different subjective probabilities and may be differently informed. Sect. 6 of the paper shows that this breaks the zero-sum logic: once the players disagree about the probability of events they can observe, a zero-sum game becomes, in expectation as each player computes it, a game in which both can gain.

The phenomenon is the game-theoretic form of betting between people who disagree: two players with different beliefs can each expect to profit from the same wager. Aumann's proposition identifies exactly what information structure makes such an agreement possible inside a given zero-sum game, and shows by an example that informing only one player of a subjective event is not enough. The same paper introduced correlated equilibrium; the companion mission of this series formalizes its two-person result on subjective mixed equilibria (Proposition 5.1).

Setting

A game has a finite set $N=\{1,\dots,n\}$ of players, a finite set $S_i$ of pure strategies for each player, a finite set $X$ of outcomes and an outcome function $g$ from $S=\times_{i\in N}S_i$ onto $X$. Player $i$ has a utility $u_i:X\to\mathbb R$; write $h_i(a)=u_i(g(a))$ for $a\in S$.

A randomizing structure consists of a set $\Omega$ of states of the world with a $\sigma$-field $\mathcal B$ of events, a sub-$\sigma$-field $\mathcal J_i\subseteq\mathcal B$ for each player (the events regarding which $i$ is informed), and a probability measure $p_i$ on $\mathcal B$ for each player (the subjective probability of $i$). A strategy of $i$ is a map $s_i:\Omega\to S_i$ whose level sets lie in $\mathcal J_i$. For a profile $s$ of strategies, player $i$'s payoff is computed under his own beliefs:

$$H_i(s)=\int_\Omega h_i\big(s(\omega)\big)\,dp_i(\omega).$$

An event $A$ is objective if all $p_i(A)$ coincide, and subjective otherwise. It is $i$-secret if $A\in\mathcal J_i$ and every other player $j$ regards $A$ as independent of every event in the $\sigma$-field generated by the $\mathcal J_k$, $k\ne i$. It is public if it lies in every $\mathcal J_i$. A measure is non-atomic on a $\sigma$-field $\mathcal R$ if every event of $\mathcal R$ of positive measure contains an event of $\mathcal R$ of strictly smaller positive measure; a roulette is a sub-$\sigma$-field of $\mathcal B$ on which every $p_j$ is non-atomic, and a public roulette is a roulette of public events. Throughout, Assumption II holds: every player $i$ has a $\sigma$-field $\mathcal R_i$ of $i$-secret events on which every $p_j$ is non-atomic.

The game is two-person zero-sum if $n=2$ and $u_1(x)+u_2(x)=0$ for all $x\in X$. Its value $v$ is player 1's payoff $F_1(\sigma)=\sum_{a\in S}h_1(a)\sigma_1(a_1)\sigma_2(a_2)$ at a Nash equilibrium $\sigma$ of the classical mixed extension; by the minimax theorem all such equilibria give the payoff pair $(v,-v)$.

Formalization targets

Goal: Proposition 6.1 (p. 80)

Let $G$ be a two-person zero-sum game with value $v$, and assume

$$\exists\,x,y\in X:\ u_1(x)>v>u_1(y),\tag{6.2}$$ $$\text{for each } i\in\{1,2\} \text{ there is } B_i\in\mathcal J_i \text{ with } p_1(B_i)\ne p_2(B_i).\tag{6.3}$$

Then there is a pair $s=(s_1,s_2)$ of strategies with

$$H_1(s)>v,\qquad H_2(s)>-v.\tag{6.4}$$

The pair is not an equilibrium: it is an agreement that each player, by his own beliefs, strictly prefers to playing the game.

Milestones

1. Lemma 7.1 (p. 81): in a roulette $\mathcal R$ there is, for every $\alpha\in[0,1]$ and events $B^1,\dots,B^l$, an objective event $A\in\mathcal R$ with $p(A)=\alpha$, independent of each $B^k$.
2. Lemma 4.2 (p. 77): for every $i$, event $B$ and $\alpha\in[0,1]$ there is an objective $i$-secret event of probability $\alpha$ independent of $B$.
3. Lemma 4.4 (p. 77): if there is a public roulette, the same holds with "public" in place of "$i$-secret".
4. Remark after Proposition 6.1 (p. 80): the conclusion (6.4) under (6.2) and

$$\text{there is a public subjective event } B \text{ and there is a public roulette,}\tag{6.5}$$

a special case of the goal in which the players share both the subjective event and the correlating device.

Significance

The proposition shows that the value of a zero-sum game is a property of objective randomization, not of the game alone. With subjective randomization available to both players, the conflict of a zero-sum game can be resolved by agreement, so the classical prediction (each player receives his security level) is not robust to disagreement about probabilities. The counterexample on p. 81 (the game with matrix rows $(1,1)$ and $(2,0)$) shows that hypothesis (6.3) is needed for both players, and the paper notes that in any specific game only one player need use a subjective strategy, though which one depends on the game.

Lemmas 4.2, 4.4 and 7.1 are the model's basic existence results for objective randomization: every probability can be realised by an event that is secret (or public) and independent of finitely many given events. They are used throughout the paper, including in the companion mission.

The paper's proofs are published and accepted; none of these statements has a machine-checked proof. This mission produces the formal statements and invites complete proofs; Lemma 7.1 requires Lyapunov's convexity theorem for finite-dimensional non-atomic vector measures, which is not in Mathlib.

Difficulty

The central difficulty for the goal is that (6.3) gives each player only some subjective event, of unknown size and in his own information field, while (6.4) requires strict gains for both players under two different measures at once. The obvious approach, betting on one subjective event, gives one player a strict gain but, when that event is not known to the other player, the other player cannot condition his choice on it; the example on p. 81 shows that one-sided information genuinely fails. Both inequalities must be arranged simultaneously, and the strategies must remain measurable with respect to each player's own information.

For Lemma 7.1, a non-atomic scalar measure takes every value in $[0,p(\Omega)]$, but the lemma asks for one event with prescribed values under $n$ measures and $nl$ further measures simultaneously; this is the range of a vector measure, not of a scalar one.

Formalization scope

• Players of the zero-sum game are 0, 1 : Fin 2 (the paper's 1, 2). S 0, S 1, X are finite types and g is surjective.
• $\mathcal B$ is the σ-field mΩ, an explicit parameter of RandomizingStructure; $\mathcal J_i$ are σ-fields below it, and each $p_i$ is a probability measure on $\mathcal B$. Probabilities are ℝ≥0∞-valued; "probability $\alpha$" is ENNReal.ofReal α with $0\le\alpha\le1$.
• Non-atomicity is the standard notion on a sub-σ-field, not Mathlib's NoAtoms, which would trivialize the roulette hypotheses.
• $H_i$ is a Bochner integral under $p_i$; for strategies with finitely many values it is the finite sum $\sum_a p_i\{s=a\}h_i(a)$.
• The value $v$ is not a free real: IsValue u g v requires $v=F_1(\sigma)$ for a Nash equilibrium $\sigma$ of the mixed extension (AGT.IsMixedNash from the published definition agt_games). A free $v$ would make the goal false. The minimax theorem is the published AGT.zero_sum_minimax.
• Assumption II is a hypothesis of every theorem, including those whose proofs do not need it.
• The conclusion of the goal and of the Remark asks for strategies, not for an equilibrium point, and does not require the strategies to be independent or objective.

Needed infrastructure: Lyapunov's theorem (or a direct argument for the finite-dimensional case), manipulation of σ-fields generated by families of sub-σ-fields, and computation of $H_i$ for strategies with finitely many values. Lyapunov's theorem is reusable far beyond this mission. Contributions of any milestone are welcome.

Selected references

• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• A. Lyapunov, Sur les fonctions-vecteurs complètement additives, Bull. Acad. Sci. URSS Sér. Math. 4 (1940) 465–478.
• J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100 (1928) 295–320. https://doi.org/10.1007/BF01448847
• J. Nash, Non-cooperative games, Annals of Mathematics 54 (1951) 286–295. https://doi.org/10.2307/1969529

Motivation

Many sequential decisions are personalised: a physician chooses a drug dose for each arriving patient, a platform chooses which offer to show each arriving user. Each decision is made after observing a vector of covariates describing the individual, and its outcome is observed only for the option chosen. This is the contextual (covariate) bandit problem, studied in operations research and machine learning since Auer (JMLR 2002) and Goldenshluger and Zeevi (Stochastic Systems 2013).

In medical and e-commerce applications the covariate vector is often high-dimensional: the number of covariates $d$ is comparable to or larger than the number of decisions that will ever be made, while the outcome of each option depends on a few of them. Low-dimensional bandit algorithms then incur regret that grows polynomially with $d$. Bastani and Bayati (Operations Research 2020) proposed the LASSO Bandit, which estimates each option's reward model with the LASSO, and proved a regret bound that grows only logarithmically in $d$. The paper evaluates the method on warfarin dosing data.

Timeline:

• 2002–2003: Auer introduces linear-reward contextual bandits with confidence bounds.
• 2013: Goldenshluger and Zeevi give a forced-sampling algorithm for two arms in low dimension with $O(\log T)$ regret under a margin condition and an arm-optimality condition, and an information-theoretic lower bound of the same order.
• 2020: Bastani and Bayati extend the forced-sampling scheme to $K$ arms and high-dimensional sparse parameters, with regret $O(s_0^2[\log T+\log d]^2)$.

Setting

There are $K$ arms with unknown parameters $\beta_1,\dots,\beta_K\in\mathbb R^d$. At each time $t=1,2,\dots,T$ a covariate vector $X_t\in\mathbb R^d$ arrives; the $X_t$ are i.i.d. with law $\mathcal P_X$ and take values in a fixed set $\mathcal X$. If arm $i$ is pulled, the reward is $X_t^\top\beta_i+\varepsilon_{i,t}$, where the noises $\varepsilon_{i,t}$ are independent, $\sigma$-subgaussian ($\mathbb E[e^{s\varepsilon}]\le e^{\sigma^2s^2/2}$ for all $s$), and independent of the covariates. A policy chooses the arm $\pi_t$ from $X_t$ and the past covariates, arms and observed rewards. Its cumulative expected regret is

$$R_T=\sum_{t=1}^T\mathbb E\Big[\max_jX_t^\top\beta_j-X_t^\top\beta_{\pi_t}\Big].$$

The sparsity $s_0$ is the smallest integer $s_0\ge1$ with $\|\beta_i\|_0\le s_0$ for all $i$.

The four assumptions are: (1) $\|x\|_\infty\le x_{\max}$ on $\mathcal X$ and $\|\beta_i\|_1\le b$; (2) a margin condition $\Pr[0<|X^\top(\beta_i-\beta_j)|\le\kappa]\le C_0\kappa$; (3) arm optimality: every arm is either suboptimal by a margin $h$ at every covariate, or optimal by margin $h$ on a region $U_i$ of probability at least $p_*$; (4) a compatibility condition: the conditional second-moment matrix $\Sigma_i=\mathbb E[XX^\top\mid X\in U_i]$ of each optimal arm lies in the set $\mathcal C(\mathrm{supp}(\beta_i),\phi_0)$ of matrices $M\succeq0$ with $\|v_I\|_1^2\le|I|\,v^\top Mv/\phi_0^2$ whenever $\|v_{I^c}\|_1\le3\|v_I\|_1$.

The LASSO estimator on $n$ samples is any minimizer of $\|Y-\mathbf X\beta'\|_2^2/n+\lambda\|\beta'\|_1$. The LASSO Bandit forces arm $i$ at the prescribed times $\mathcal T_i=\{(2^n-1)Kq+j : n\ge0,\ q(i-1)<j\le qi\}$. At every other time it keeps the arms whose forced-sample estimate $\hat\beta(\mathcal T_{i,t-1},\lambda_1)$ is within $h/2$ of the best. Among them it plays the arm with the largest all-sample estimate $\hat\beta(\mathcal S_{i,t-1},\lambda_{2,t-1})$, trained on every past pull of the arm, with $\lambda_{2,t}=\lambda_{2,0}\sqrt{(\log t+\log d)/t}$.

Formalization targets

Goal: Theorem 1 (regret of the LASSO Bandit)

For $q\ge4\lceil q_0\rceil$, $K\ge2$, $d>2$, $T\ge C_5$, $\lambda_1=\phi_0^2p_*h/(64s_0x_{\max})$ and $\lambda_{2,0}=[\phi_0^2/(2s_0)]\sqrt{1/(p_*C_1)}$,

$$R_T\le C_3(\log T)^2+\big[2Kbx_{\max}(6q+4)+C_3\log d\big]\log T+\big(2bx_{\max}C_5+2Kbx_{\max}+C_4\big),$$

with the explicit constants $C_1,\dots,C_5$, $q_0$ of the paper (p. 285).

Milestones

1. Proposition 1: a LASSO tail inequality for adaptively collected rows with conditionally subgaussian noise.
2. Lemma 1: a LASSO tail inequality when a constant fraction of the rows is i.i.d. with a compatible second-moment matrix.
3. Proposition 2: the forced-sample estimator of an optimal arm is within $h/(4x_{\max})$ of $\beta_i$ except with probability $5/t^4$.
4. Proposition 3: the all-sample estimator of an optimal arm is within $16\sqrt{(\log t+\log d)/(p_*^3C_1t)}$ of $\beta_i$ except with probability $2/t+2e^{-p_*^2C_2^2t/32}$.

Significance

The theorem shows that exploiting sparsity makes the regret depend on the ambient dimension only through $\log d$, while its dependence on the horizon is within one $\log T$ factor of the $\Omega(\log T)$ lower bound known in low dimension. Proposition 1 is a LASSO oracle inequality for adapted designs, where each row may depend on earlier observations. It applies whenever a LASSO is fitted to data gathered by a feedback policy: adaptive experiments, dynamic pricing, sequential treatment assignment.

The results are proved in the paper and its online appendix; none of them has a machine-checked proof. This mission produces a formal model of the covariate bandit with a non-anticipating algorithm, a formal LASSO for adapted designs, and, when complete, a verified regret bound with every constant explicit. Proposition 1 and Lemma 1 are reusable beyond bandits.

Difficulty

The all-sample estimator is trained on the times at which the algorithm chose an arm, and those choices depend on earlier estimates. Its design rows are therefore neither independent nor identically distributed, and the standard LASSO analysis, which starts from i.i.d. rows and a restricted-eigenvalue bound on their population covariance, does not apply. The forced samples are i.i.d. but only $O(\log t)$ in number, too few for the $\sqrt{\log t/t}$ rate the regret bound needs. Controlling the compatibility constant of the adaptively selected sample covariance, and the martingale noise term, is where the naive argument breaks.

Formalization scope

Arms are Fin K (paper arm $i$ is i.val + 1), coordinates Fin d, times are natural numbers from $1$. The model is a structure IsCovariateNoiseModel on a probability space: i.i.d. measurable covariates in a measurable set $\mathcal X$, independent subgaussian noises (Mathlib's HasSubgaussianMGF with parameter $\sigma^2$), noise independent of covariates. Assumptions 1–4 are separate predicates. $\|x\|_\infty$ is Mathlib's sup norm, logarithms are natural, and $\Sigma_i$ is the uncentred conditional second moment.

The LASSO minimizer and the arg max need not be unique, so the algorithm takes a selection rule and a tie-breaking rule as parameters, and the theorems hold for all of them. Each round reads only the current covariate, the past covariates, the past arms and their observed rewards. The regret theorem and Proposition 3, whose data set $\mathcal S_{i,t}$ is chosen by the algorithm, require both rules to be measurable. Otherwise the trajectory would not be a random variable, and the expectations in $R_T$ could be integrals of non-measurable functions, which Lean evaluates to $0$ and which would make the goal trivially true. For the same reason every assumption constant is required to be positive, and $T\ge C_5$ is imposed on the horizon. Only the explicit inequality of Theorem 1 is stated, not the trailing $O(s_0^2[\log T+\log d]^2)$ or $q_0=O(s_0^2\log d)$. Proposition 2 is stated for optimal arms (see its note).

A complete development needs matrix concentration for bounded i.i.d. rows, the Azuma–Hoeffding inequality, and the deterministic LASSO basic inequality under a compatibility condition. Contributions of any of these as standalone lemmas are welcome.

Selected references

• H. Bastani and M. Bayati, Online Decision Making with High-Dimensional Covariates, Operations Research 68(1):276–294, 2020. https://doi.org/10.1287/opre.2019.1902
• A. Goldenshluger and A. Zeevi, A Linear Response Bandit Problem, Stochastic Systems 3(1):230–261, 2013. https://doi.org/10.1287/11-SSY032
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• P. Bühlmann and S. van de Geer, Statistics for High-Dimensional Data, Springer, 2011. https://doi.org/10.1007/978-3-642-20192-9

Motivation

A retailer or manufacturer that stocks several grades of the same item (memory chips of different speeds, steel of different strengths, seats in fare classes) can often meet demand for a lower grade with a higher one when the lower grade runs out. This downward substitution changes the stocking decision: each product now protects the demand of every class below it, so the optimal stock of one product depends on the stock of all the others, and the single-product newsvendor answer no longer applies product by product.

Bassok, Anupindi and Akella (Operations Research 47(4), 1999) set up a single-period model with $N$ products and full downward substitution and showed that the optimal ordering policy still has a simple structure: there is a base-stock vector $y^*$; products below it are ordered up to it, and a product already at or above its base-stock level is not ordered at all. Earlier work on multiproduct ordering, Veinott (1965) and Ignall and Veinott (1969), gave monotonicity conditions through a substitute matrix condition on the Hessian of the cost, which is hard to verify for a general $N$-product substitution structure; the paper works instead with concavity, submodularity and explicit first partial derivatives. Two-product substitution models had been analysed by McGillivray and Silver (1978) and Parlar and Goyal (1984).

Setting

There are $N$ products and $N$ demand classes, both numbered $1,\dots,N$. Class $i$ can be served by product $j$ whenever $j \le i$, at a unit substitution cost $b$ when $j < i$. Each class $i$ has unit revenue $p_i$ and unit backorder cost $\pi_i$; each product $j$ has unit purchase cost $c_j$ and effective unit salvage value $s_j$ (salvage value minus holding cost, possibly negative). Put $a_{ji} = p_i$ if $j = i$, $a_{ji} = p_i - b$ if $j < i$, and $T_k = p_k + \pi_k - b$. The standing assumptions are: (1) $\pi_i + p_i \ge \pi_j + p_j$ for $i < j$; (2) $s_i \ge s_j$ for $i < j$; (3) $a_{ij} + \pi_j - s_i \ge 0$ for $i \le j$.

The sequence of events: the starting inventory $x$ is observed; stock is raised to $y \ge x$ at unit costs $c$; the demand vector $d$ is realized; stock is allocated to classes; leftovers are salvaged. For fixed $y$ and $d$ the allocation is the linear program

$$G(y,d) = \max \sum_{i}\sum_{j \le i} a_{ji} w_{ji} + \sum_i s_i v_i - \sum_i \pi_i u_i$$

subject to $u_i + \sum_{j\le i} w_{ji} = d_i$, $v_j + \sum_{i \ge j} w_{ji} = y_j$, and $w, u, v \ge 0$, where $w_{ji}$ is the amount of product $j$ given to class $i$, $u_i$ the shortage of class $i$ and $v_j$ the leftover of product $j$. The expected profit is

$$P(x,y) = -\sum_k c_k (y_k - x_k) + \mathbb E\, G(y, D),$$

and the ordering problem is $\max_{y \ge x} P(x,y)$; a maximizer is an optimal level $\bar y(x)$.

Allocation Algorithm (A) serves the classes in the order $1,2,\dots,N$, class $i$ first from product $i$ and then from the leftovers of products $i-1,\dots,1$. The subproblem shortage $S^k_j$ is the unmet demand of class $j$ when (A) runs on the classes $k,\dots,j$ with the products $k,\dots,j$ only; $\vec S^k_{a,n} = 0$ means $S^k_m = 0$ for all $a \le m \le n$. The paper's first partial derivatives of $P$ are sums of salvage values, substitution costs and the $T_k$, weighted by probabilities of such shortage events.

Formalization targets

Goal: Theorem 2

With $y^*$ a maximizer of $P(0,\cdot)$ over $y \ge 0$, every optimal level $\bar y$ for every starting inventory $x \ge 0$ satisfies

$$x_i \ge y^*_i \implies \bar y_i = x_i .$$

Milestones

• Proposition 1: Algorithm (A) is feasible and optimal for the allocation LP, and its value is $G(y,d)$.
• Proposition 2: $y \mapsto P(x,y)$ is concave and submodular on $\{y \ge 0\}$.
• Eq. (4): the explicit formula for $\partial P/\partial y_i$ in terms of shortage probabilities.
• Theorem 1: there is $y^* \ge 0$ with $\bar y(x) = y^*$ whenever $0 \le x \le y^*$.
• Lemmas 1, 2, 3, 5: identities and monotonicity properties of the shortage probabilities used to compare $\partial P/\partial y_i$ and $\partial P/\partial y_{i+1}$.

Significance

Theorems 1 and 2 give the optimal ordering policy of the substitution model its base-stock form: a vector $y^*$, computed once, determines the decision for every starting inventory in the region $x \le y^*$ and fixes the order of every overstocked product elsewhere. The paper builds its bounds on $y^*$, its iterative algorithm for two products and its computational study of the value of substitution (§3) on this structure. Proposition 1 turns the second-stage linear program into a closed-form greedy allocation, which is what makes the derivative formula (4) explicit.

The results are proved in the paper, but none of them has been machine-checked. Several steps of the paper are informal: Proposition 1 is proved by reference to Monge sequences of transportation problems, the proof of Theorem 2 treats only the adjacent pair $j = i+1$, and the paper uses independence of demand classes, densities and a unique optimal level without stating them. A formal development makes these hypotheses explicit and checks each step. The model, the greedy allocation and the shortage calculus are reusable for other multi-product newsvendor and assortment models.

Difficulty

The obvious argument for Theorem 2 is the one-dimensional one: if $x_i \ge y^*_i$ then $\partial P/\partial y_i \le 0$ at $\bar y$, so product $i$ should not be raised. It fails because $\partial P/\partial y_i$ depends on the other coordinates: at $\bar y$ some products are raised above $x$ and others kept at $x_j > y^*_j$, and concavity plus submodularity alone do not control the sign. For a general concave submodular function the conclusion is false; a three-variable quadratic in which raising one coordinate lowers the optimal level of a second one, which in turn raises the marginal value of the first, is a counterexample. The proof has to use the specific structure of the substitution model, through the pairwise comparison of the partial derivatives in Eq. (4). The derivative formula itself requires a careful account of how an extra unit of product $i$ propagates through the greedy allocation of every later class.

Formalization scope

Products and classes are indexed by Fin N (the paper's index $k$ is Lean index $k-1$); stocks, demands and prices are real. The allocation LP is encoded with the upward arcs $w_{ji}$, $i < j$, forbidden (fixed to $0$), as in the paper's proof of Proposition 1; $G$ is the supremum of the LP objective. The demand law is a product $\nu_1 \otimes \dots \otimes \nu_N$. Submodularity is the lattice inequality $P(x, y \vee y') + P(x, y \wedge y') \le P(x,y) + P(x,y')$, which is equivalent to the paper's nonpositive cross partials (Definition 2) for twice differentiable functions. Derivatives are stated with HasDerivAt, and the derivative inequalities of Lemmas 2 and 5 in the stronger monotone form, so that no statement is made true by a junk value of deriv. The "…" in Eq. (4) and in the lemmas are expanded as finite sums with the general term inferred from the printed first and last terms.

Hypotheses the paper uses without stating, made explicit here:

• the substitution cost is nonnegative, $b \ge 0$ (Proposition 1 is false for $b < 0$);
• the demand classes are independent (product forms in Lemma 3 and Appendix B);
• each demand is nonnegative, has finite mean and has a density;
• $s_i < c_i < p_i + \pi_i$ for every product (Theorem 1's proof);
• every demand law charges every nonempty open interval of $[0,\infty)$, standing in for the uniqueness of the optimal level $\bar y(x)$ that the notation presupposes (Theorems 1 and 2).

The goal quantifies over every maximizer $y^*$ of $P(0,\cdot)$ and every optimal $\bar y$; it is not an existence statement, and $y^*$ is not chosen by the prover. Without the full-support hypothesis the universal statement fails already for one product (a flat-topped profit). Lemmas 4 and 6 of the paper are not included: under the definitions used here both are false as printed (small two- and three-product computations with exponential demands show it), and Theorem 3 comes after the goal and fails as printed for $x_i \ge y^*_i$.

A proof needs integrals of piecewise-linear functions of the demand vector, differentiation under the integral sign, and facts about product measures. Contributions of any of the milestones, and of general lemmas on the greedy allocation (monotonicity of $S^k_j$ in $y$ and $d$), are welcome.

Selected references

• Y. Bassok, R. Anupindi, R. Akella, Single-Period Multiproduct Inventory Models with Substitution, Operations Research 47(4):632–642, 1999. https://doi.org/10.1287/opre.47.4.632
• A. F. Veinott, Jr., Optimal Policy for a Multi-Product, Dynamic, Nonstationary Inventory Problem, Management Science 12(3):206–222, 1965. https://doi.org/10.1287/mnsc.12.3.206
• E. Ignall, A. F. Veinott, Jr., Optimality of Myopic Inventory Policies for Several Substitute Products, Management Science 15(5):284–304, 1969. https://doi.org/10.1287/mnsc.15.5.284
• A. J. Hoffman, On Simple Linear Programming Problems, in V. Klee (ed.), Convexity, Proceedings of Symposia in Pure Mathematics, Vol. 7, AMS, 1963.

Pooling inventory among independent retailers

Retailers that sell the same product can raise their joint profit by pooling: stock left over at one location is shipped to meet unmet demand at another, and stock can be held in shared warehouses until demand is known (Eppen 1979; Eppen and Schrage 1981). When the retailers are independent firms, pooling creates two questions at once. After demand is realized, the extra profit from shipping must be split in a way no group of retailers would reject. Before demand is realized, each retailer chooses its own stock, and that choice depends on how the split will be made. A split that is fair ex post may lead to stocking decisions that are poor for the system as a whole.

Anupindi, Bassok and Zemel (MSOM 2001) model the ex-post split as a cooperative game, the ex-ante stocking as a non-cooperative game, and ask whether a single allocation rule can serve both. Their framework is a standard reference for "coopetition" models in supply chains, where firms compete on stocking decisions and cooperate on redistribution.

Setting

There are retailers $\mathcal N=\{1,\dots,N\}$ and warehouses $\mathcal W=\{1,\dots,W\}$. Retailer $n$ has unit cost $c_n$, revenue $r_n$ and salvage value $v_n$; warehouse $w$ has purchasing cost $c_w$ and salvage value $v_w$. Shipping from location $i$ to retailer $n$ costs $t_{i,n}$ per unit, and a fraction $\beta_{i,n}\in[0,1]$ of the customers at $n$ accept service from $i$.

Before demand, retailer $n$ chooses a position $\vec Z_n=(X_n,Y_{1,n},\dots,Y_{W,n})$: local stock $X_n$ and claims $Y_{w,n}$ on warehouse stock, so warehouse $w$ holds $Y_w=\sum_nY_{w,n}$. A profile is $[Z]=(\vec Z_1,\dots,\vec Z_N)$. Demand $\vec D$ is random with law $\mu$. After demand, retailer $n$ has local sales $S_n=\min\{X_n,D_n\}$, residual inventory $H_n=\max\{X_n-D_n,0\}$ and residual demand $E_n=\max\{D_n-X_n,0\}$.

The snapshot allocation game SAG$([Z],\vec D)$ gives each coalition $\mathcal S\subseteq\mathcal N$ the value $W^*_{\mathcal S}([Z],\vec D)$: the optimal value of the linear program (6), which ships $q_{i,n}$ units from $i\in\mathcal S\cup\mathcal W$ to $n\in\mathcal S$ at profit $r_n-v_i-t_{i,n}$ per unit, subject to $\sum_nq_{i,n}\le H_i$, $\sum_nq_{w,n}\le\sum_{n\in\mathcal S}Y_{w,n}$ and $\sum_iq_{i,n}/\beta_{i,n}\le E_n$. Its core is the set of allocations $\alpha$ with $\sum_{j\in\mathcal S}\alpha_j\ge W^*_{\mathcal S}$ for every $\mathcal S$ and $\sum_{j\in\mathcal N}\alpha_j=W^*_{\mathcal N}$ (7).

An allocation rule AR-$m$ assigns surplus $\alpha^m_n([Z],\vec D)$; retailer $n$ earns

$$P^m_n([Z],\vec D)=r_nS_n+v_nH_n-c_nX_n-\sum_w(c_w-v_w)Y_{w,n}+\alpha^m_n([Z],\vec D)\qquad(9)$$

and expects $J^m_n([Z])=E_{\vec D}P^m_n$. A Nash equilibrium (10) is a profile at which no retailer gains by changing its own position. The first-best profile $[Z]^{c*}$ maximizes the expected centralized profit $J^c_{\mathcal N}([Z])=E_{\vec D}P^c_{\mathcal N}([Z],\vec D)$, where $P^c_{\mathcal N}=\sum_n[r_nS_n+v_nH_n-c_nX_n]-\sum_w(c_w-v_w)Y_w+W^*_{\mathcal N}$.

The fractional rule AR-f (11) pays $\alpha^f_n=\theta_nP^c_{\mathcal N}-[\,r_nS_n+v_nH_n-c_nX_n-\sum_w(c_w-v_w)Y_{w,n}]$ with fixed shares $\theta_n\in(0,1)$, $\sum_n\theta_n=1$. The dual allocation (8) is $\alpha^d_n=\nu_nH_n+\sum_w\gamma_wY_{w,n}+\delta_nE_n$ for optimal dual prices $(\nu,\gamma,\delta)$ of (6) for $\mathcal N$. The modified rule AR-c is $\alpha^c_n([Z],\vec D)=\alpha^f_n([Z],\vec D)+w_n([Z]^{c*},\vec D)$ with $w_n=\alpha^d_n([Z]^{c*},\cdot)-\alpha^f_n([Z]^{c*},\cdot)$.

Formalization targets

Goal: Corollary 5.1 (p. 361)

For a first-best profile $[Z]^{c*}$ and a measurable choice of dual prices at $[Z]^{c*}$,

$$[Z]^{c*}\ \text{is a pure Nash equilibrium under AR-c, and}\ \ \alpha^c([Z]^{c*},\vec D)\in\operatorname{Core}\big(\mathrm{SAG}([Z]^{c*},\vec D)\big)\ \ \forall\vec D,$$

with integrable side payments.

Milestones

• Examples 1 and 2 (pp. 358–359): a transfer-price allocation outside the core; the dual allocation $(8,8,8,0)$ and the non-dual core allocation $(0,0,0,24)$.
• Theorem 4.1 (p. 358): if all inventory is claimed, the core of SAG$([Z],\vec D)$ is nonempty and contains the dual allocation (8) for every optimal dual.
• Theorem 5.2 (p. 361): under AR-f every first-best profile is a Nash equilibrium.
• Theorem 5.1 (p. 361): for any rule and any of its equilibria $[Z]^{m*}$ there are integrable demand-dependent side payments that leave the set of equilibria unchanged and put the allocations at $[Z]^{m*}$ in the core for every $\vec D$.

Significance

The goal answers the paper's central question positively: there is an allocation mechanism under which the centrally optimal stock levels are an equilibrium of the decentralized stocking game, while every ex-post split of the pooling surplus is stable against all coalitions. Theorem 4.1 is the ex-post half: shadow prices of the shipping LP give a stable split for every realization, independently of who owns which units. The paper also shows (Proposition 5.1, not included here) that the dual allocation alone does not induce first-best stocking, which is why the side payments of Theorem 5.1 are needed.

The results are proved in the paper; Theorem 4.1 is proved there only by reference to the LP-game literature (Owen 1975; Samet and Zemel 1984). None of them has a machine-checked proof. The mission would produce the first formal treatment on Prove2Me of a linear-production (LP) game and its core, and of a model combining a cooperative second stage with a non-cooperative first stage.

Difficulty

Theorem 4.1 is an instance of Owen's theorem on LP games, but the instance is not a standard linear production game: coalition LPs have variables only on arcs inside the coalition, warehouse capacity is limited to the coalition's own claims, and the acceptance constraint divides by $\beta_{i,n}$, which may be zero, so the general theorem cannot be quoted as it stands. The paper leaves the dual of (6) unwritten, and Mathlib has no ready-made LP duality in this form.

The stochastic layer is the other obstacle. Expected payoffs are integrals, and the side payment is built from a choice of dual prices for each demand realization. Its integrability requires measurability of that choice and of the LP value as a function of demand; neither is given by the paper, which treats the side payments as "constants".

Formalization scope

Retailers are Fin N, warehouses Fin W, locations Fin N ⊕ Fin W; quantities, prices and demands are real numbers; demand is a probability measure on Fin N → ℝ; expectations are Bochner integrals. $W^*_{\mathcal S}$ is the real supremum of (6a) over the feasible set, and profiles are required to be nonnegative, which makes the feasible set nonempty and bounded. Arcs with $\beta_{i,n}=0$ carry no shipment. The core is the platform definition Supermodularity.Cooperative.Core. The dual of (6) is written out explicitly (the paper does not state it). The paper's continuous-CDF assumption is not used and is dropped.

Pinned readings:

1. "Dual prices" means any optimal solution of the dual of (6) for $\mathcal N$; Theorem 4.1 is stated for every such solution.
2. "Induces the same equilibrium inventory levels as the first-best" (Theorem 5.2) and "the NE using $\alpha^c$ is first-best" (Corollary 5.1) are stated as "every first-best profile is a Nash equilibrium", the direction the proofs give.
3. "$[Z]^{\tilde m*}=[Z]^{m*}$" (Theorem 5.1) is stated as equality of the two sets of equilibria; the continuity and unimodality assumptions, which only guarantee existence of an equilibrium, are dropped because the equilibrium is a hypothesis.
4. "An appropriate way of breaking ties" is a measurable choice of optimal dual prices; demand is almost surely nonnegative; the rule's payoffs in Theorem 5.1 are integrable.
5. The shares $\gamma_n$ of Theorem 5.2 are written $\theta_n$, and Eq. (11) is used with $+v_nH_n$ in the bracket (printed $-v_nH_n$), as the proof on p. 367 requires.

Not acceptable: a core without the efficiency equation (7b); a feasible set that lets $q_{i,n}/0=0$ sell to customers who balk; an arbitrary side payment instead of the constructed one; or a Nash equilibrium evaluated through non-integrable payoffs, whose Bochner integral is $0$ and makes every profile an equilibrium.

Useful infrastructure: finite-dimensional LP duality in inequality form, measurable selection of LP optimal solutions, and continuity of LP values in the right-hand side. All of it can be reused in other LP-game and two-stage stochastic programming missions.

Selected references

• R. Anupindi, Y. Bassok, E. Zemel, A General Framework for the Study of Decentralized Distribution Systems, Manufacturing & Service Operations Management 3(4):349–368, 2001. https://doi.org/10.1287/msom.3.4.349.9973
• G. Owen, On the core of linear production games, Mathematical Programming 9:358–370, 1975. https://doi.org/10.1007/BF01681356
• D. Samet, E. Zemel, On the core and dual set of linear programming games, Mathematics of Operations Research 9(2):309–316, 1984. https://doi.org/10.1287/moor.9.2.309
• G. D. Eppen, Effects of centralization on expected costs in a multi-location newsboy problem, Management Science 25(5):498–501, 1979. https://doi.org/10.1287/mnsc.25.5.498

Motivation

Market equilibrium is the central solution concept of general equilibrium theory: prices at which every agent buys a utility-maximizing bundle and supply meets demand. Arrow and Debreu (1954) proved that equilibria exist under mild conditions on endowments and utilities, and a line of work in algorithmic game theory asks how hard it is to compute them. For linear utilities an equilibrium can be computed in polynomial time, and there is an efficiently checkable condition for its existence. The next natural class, additively separable piecewise-linear concave utilities, models diminishing marginal utility and is the class most used in applications.

Vazirani and Yannakakis (J. ACM 58(3), 2011) settle the complexity of this class. They show that equilibria are rational whenever they exist (Theorems 4.1 and 5.1), that computing an equilibrium under the standard sufficient conditions is PPAD-complete (Theorems 6.1 and 7.1, building on Chen, Dai, Du and Teng 2009), and — the subject of this mission — that deciding whether an equilibrium exists at all is NP-complete (Theorem 8.1). The hardness half rests on an explicit construction: from an instance of Exact Cover by 3-Sets, a market whose equilibria encode exact covers.

Setting

An Arrow–Debreu market has a finite set $B$ of agents and a finite set $G$ of divisible goods. Agent $i$ owns an endowment $w_{ij}\ge 0$ of each good $j$ and has utility $u_i(y)=\sum_{j} f^i_j(y_j)$, where each $f^i_j$ is a piecewise-linear concave utility function: slopes $c_1\ge c_2\ge\dots\ge c_m>0$ on consecutive pieces of lengths $a_1,\dots,a_m$, followed by a last piece of slope $t\in[0,c_m]$ until infinity ($t=0$ means the function goes flat).

At prices $p$, agent $i$'s income is $\sum_j p_j w_{ij}$. An optimal bundle is an affordable $y\ge 0$ maximizing $u_i$ among affordable bundles, bought only along the pieces of $f^i_j$ that carry utility. A price equilibrium is a price vector $p$ in the unit simplex ($p\ge 0$, $\sum_j p_j=1$) together with an allocation of optimal bundles such that $\sum_i x_{ij}=\sum_i w_{ij}$ for every good $j$. It is an $\epsilon$-approximate equilibrium if instead $|\sum_i x_{ij}-\sum_i w_{ij}|\le\epsilon\sum_i w_{ij}$ for every $j$.

An X3C instance is a family $\mathcal C=(C_1,\dots,C_n)$ of $3$-element subsets of $X=\{x_1,\dots,x_n\}$; an exact cover is a subfamily in which every element of $X$ lies in exactly one set. Following the paper, $n$ is a multiple of $3$, $n>35$, and $\bigcup_i C_i=X$.

The market $D(\mathcal C)$ has $2n+1$ goods (good $0$, goods $C_i$, goods $x_j$) and $2n+2$ agents, with $e_0=n^3$:

1. agent $0$ owns $e_0$ units of every good; his utility for every good has slope $2$ up to $e_0$ units and slope $1$ beyond;
2. agent $C_i$ owns one unit of good $C_i$; segments of slope $1$, length $1/2$ for good $0$, slope $1/3$, length $1/6$ for each good $x_j\in C_i$, slope $1/9$, length $1/4$ for good $C_i$;
3. agent $x_j$ owns $1/6$ unit of good $x_j$; one segment of slope $1$, length $1/12$ for good $0$;
4. the extra agent owns $n/2$ units of good $0$; one segment of slope $1$, length $3/4$ for each good $C_i$.

All other utility functions are flat.

Formalization targets

Goal: the reduction statement

$$\mathcal C\ \text{has an exact cover}\iff D(\mathcal C)\ \text{has an equilibrium}\iff D(\mathcal C)\ \text{has an } n^{-5}\text{-approximate equilibrium}.$$

This is the mathematical content of the NP-hardness half of Theorem 8.1, assembled by the paper from Lemmas 8.2 and 8.3.

Milestones

1. Lemma 8.2: an exact cover yields an equilibrium of $D(\mathcal C)$.
2. Lemma 7.2, as applied in Lemma 8.3: in an $n^{-5}$-approximate equilibrium of $D(\mathcal C)$ all prices are positive and within a factor $2$ of each other.
3. Claims 8.4–8.7: in such an equilibrium, with $p_m$ the minimum price, $p(0)=2p_m$; $p(x_j)<2p_m$; with $S=\{i: p(C_i)\ge p_m+\tfrac16\sum_{x_j\in C_i}p(x_j)\}$, every $i\notin S$ has $p(C_i)=p_m$; and the sets indexed by $S$ are pairwise disjoint.
4. Lemma 8.3: an equilibrium, or an $n^{-5}$-approximate equilibrium, of $D(\mathcal C)$ yields an exact cover.

Significance

Theorem 8.1 shows that there is no efficiently checkable necessary and sufficient condition for the existence of an equilibrium in piecewise-linear concave markets unless P = NP, in contrast with the linear case. Together with the PPAD results of the same paper it separates two questions: under the classical sufficient conditions an equilibrium exists and finding one is PPAD-complete; without them, even deciding existence is NP-hard, and remains so for $n^{-5}$-approximate equilibria. The construction illustrates the technique the paper uses for both of its negative results: well-chosen piecewise-linear pieces make an agent buy a segment wholly or not at all, depending on how prices compare, which gives the equilibrium problem a discrete character.

The result is proved in the paper. To our knowledge no part of it has been machine-checked. This mission formalizes the reduction's correctness at full strength, including the approximate version, which requires quantitative control of clearing errors that the exact version does not.

Difficulty

The direction "exact cover ⇒ equilibrium" is an explicit verification: prescribed prices and an allocation, and a check that every bundle is optimal, which for separable piecewise-linear utilities is a bang-per-buck comparison. The converse is the substantial part. An arbitrary approximate equilibrium must be shown to have the rigid price structure — every price in $[p_m,2p_m]$, good $0$ at $2p_m$, unused sets at $p_m$ — before a counting argument on agent $0$'s savings forces $|S|=n/3$. Each step is an excess-demand argument in which the error $\epsilon$ times the supply must be compared with quantities of order $1/n$; this is where $n>35$ and the exponent $5$ enter, and why the approximate statement does not follow from the exact one. Optimality of bundles is a statement about all affordable bundles, so each claim needs the structure of optimal bundles under piecewise-linear concave utility, which is not in Mathlib.

Formalization scope

Lean namespace PLCMarkets.ExactCover. Market data (endowments, slopes, lengths) are rationals; prices and allocations are reals. Goods and agents of $D(\mathcal C)$ are small inductive types named as in the paper; indices are 0-based. Supplies are not normalized to $1$, so clearing is $\sum_i x_{ij}=\sum_i w_{ij}$; prices are normalized to the simplex in both equilibrium notions, as in the proof of Lemma 8.3. The family $\mathcal C$ is indexed and may repeat a set; exact cover and the disjointness of $S$ count indices.

Standing hypotheses of every theorem: each $C_i$ has three elements, $3\mid n$, $n>35$, $\bigcup_i C_i=X$ — the paper's own "without loss of generality" assumptions (p. 10:19). Two conventions depart from the printed page, both necessary and both disclosed on the items:

• Optimal bundles buy only utility-bearing pieces. If a utility function is flat beyond its segments, the agent does not buy beyond them. The paper uses this throughout (an agent "can only spend $p_m/6$ on the single segment", Claim 8.5). Without it, agents can spend leftover income on goods worth nothing to them; then setting $p(0)=2p_m$ and every other price to $p_m$ gives an exact equilibrium of every $D(\mathcal C)$, and the goal is false.
• The extra agent's segments have length $3/4$. The page prints $3n/4$; every computation in the paper (Lemma 8.2, Claim 8.6, the end of Lemma 8.3) uses $3/4$ per good, and with $3n/4$ the prices of Lemma 8.2 are not an equilibrium.

Trivializing encodings are excluded: optimality of bundles is part of both equilibrium notions (without it the endowment itself clears every market), clearing is relative and per good, and the goal quantifies only over $n$ and $\mathcal C$, with $D(\mathcal C)$ an explicit function of $\mathcal C$.

Out of scope: the complexity-class statement "NP-complete" and NP membership (which comes from the rationality theorems of the companion mission); polynomial-time computability of the construction and string encodings of markets; and the Fisher market $F$ of §8, whose half of Lemmas 8.2 and 8.3 is a natural follow-up. Reusable infrastructure: piecewise-linear concave utilities, Arrow–Debreu markets with exact and approximate equilibria, and bang-per-buck characterizations of optimal bundles. Contributions proving that characterization as a standalone lemma are welcome.

Selected references

• V. V. Vazirani and M. Yannakakis, Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities, Journal of the ACM 58(3), Article 10, 2011. https://doi.org/10.1145/1970392.1970394
• X. Chen, D. Dai, Y. Du and S.-H. Teng, Settling the Complexity of Arrow–Debreu Equilibria in Markets with Additively Separable Utilities, Proceedings of the IEEE Symposium on Foundations of Computer Science (FOCS), 2009 (reference [Chen et al. 2009a] of the paper).
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 1954. https://doi.org/10.2307/1907353

Motivation

A Fisher market is the simplest model of a market in which prices are set by supply and demand: buyers bring money, sellers bring goods, and a price vector is an equilibrium when every buyer, spending her money optimally at those prices, leaves every good exactly sold out. Computing equilibria is one of the central questions of algorithmic game theory, because a polynomial-time algorithm is what would make the equilibrium concept usable as a prediction or as a pricing mechanism.

For linear utilities an equilibrium always exists, is rational, and can be computed in polynomial time (Eisenberg and Gale 1959; Devanur, Papadimitriou, Saberi and Vazirani, J. ACM 2008, https://doi.org/10.1145/1411509.1411512). The next natural class, additively separable, piecewise-linear, concave utilities, captures diminishing marginal utility and is the class studied by Vazirani and Yannakakis (J. ACM 58(3), Article 10, 2011, https://doi.org/10.1145/1970392.1970394). Their paper shows that equilibria in this class are hard to compute (PPAD-complete) and that deciding whether one exists is NP-complete. Both results rest on a structural fact proved first: whenever such a market has an equilibrium at all, it has one whose prices are rational numbers of polynomial bit length. That fact is the subject of this mission.

Timeline:

• 1959, Eisenberg and Gale: a convex program whose optimal solutions are the equilibria of linear Fisher markets; equilibrium prices are rational.
• 2008, Devanur, Papadimitriou, Saberi and Vazirani: a combinatorial polynomial-time algorithm for linear Fisher markets, based on a max-flow test of candidate prices.
• 2009, Chen, Dai, Du and Teng, and Chen and Teng (FOCS 2009; ISAAC 2009): PPAD-hardness for additively separable piecewise-linear concave utilities in Arrow–Debreu and Fisher markets.
• 2011, Vazirani and Yannakakis: rationality of equilibria with polynomial bit size (Theorem 4.1 for Fisher markets, Theorem 5.1 for Arrow–Debreu markets), PPAD membership, and NP-completeness of existence.

Setting

There are $n$ buyers $B=\{1,\dots,n\}$ and $g$ divisible goods $G=\{1,\dots,g\}$, one unit of each good. Buyer $i$ has a rational budget $e(i)>0$. For each buyer $i$ and good $j$ a function $f^i_j:\mathbb R_+\to\mathbb R_+$ gives the utility that $i$ derives from an amount of good $j$. It is piecewise linear and concave: it is given by a finite list of bounded segments $(c_1,a_1),\dots,(c_m,a_m)$ with rational amounts $a_k>0$, followed by a last, unbounded segment, with rational slopes $c_1\ge c_2\ge\dots\ge c_m\ge c_\infty\ge 0$. The function has slope $c_k$ on $[a_1+\dots+a_{k-1},\,a_1+\dots+a_k]$ and slope $c_\infty$ afterwards. Buyer $i$'s utility for a bundle $x=(x_1,\dots,x_g)$ is additively separable:

$$u_i(x)=\sum_{j\in G}f^i_j(x_j).$$

Given prices $p\in\mathbb R^g_{\ge0}$, a bundle $x\ge0$ is optimal for buyer $i$ if $\sum_jp_jx_j\le e(i)$ and no bundle $y\ge0$ with $\sum_jp_jy_j\le e(i)$ has $u_i(y)>u_i(x)$. The prices $p$ are equilibrium prices if there is an allocation $(x_{ij})$ that gives each buyer an optimal bundle and sells every good exactly: $\sum_ix_{ij}=1$ for every $j$.

The bit size of a rational number $a/b$ in lowest terms is the binary length of $|a|$ plus that of $b$. The encoding size $\|M\|$ of a market $M$ is $n+g$ plus the bit sizes of all budgets, slopes and amounts, plus the number of bounded segments.

For the intermediate results, fix positive prices $p$. The bang per buck of a segment $s$ of good $j$ is $\mathrm{slope}(s)/p_j$ and its value is $\mathrm{amount}(s)\cdot p_j$ (infinite for an unbounded segment). Sorting buyer $i$'s segments by decreasing bang per buck into classes of equal bang per buck, the first class at which the cumulative value exceeds $e(i)$ is her flexible class. Segments of strictly larger bang per buck are forced, the others undesirable. From these the paper defines $\mathrm{spent}(i)$ (value of the forced segments), $\mathrm{unspent}(i)=e(i)-\mathrm{spent}(i)$, $\mathrm{unsold}(j)$ (the part of good $j$ not taken by forced segments), and a network $N(p)$ from a source through goods and buyers to a sink.

Formalization targets

Goal: Theorem 4.1 (p. 10:9)

There is a polynomial $P$ such that for every Fisher market $M$ as above,

$$M\text{ has equilibrium prices }p\in\mathbb R^g\ \Longrightarrow\ M\text{ has equilibrium prices }q\in\mathbb Q^g\text{ with }\sum_{j}\operatorname{bits}(q_j)\le P(\|M\|).$$

The polynomial is fixed before the market. Nothing beyond the existence of some real equilibrium is assumed.

Milestones

1. Lemma 3.1 (p. 10:8). For positive prices with $\sum_jp_j=\sum_ie(i)$, $\mathrm{unspent}\ge0$ and $\mathrm{unsold}\ge0$: $p$ are equilibrium prices iff the max-flow value of $N(p)$ is $\sum_i\mathrm{unspent}(i)$.
2. Proof of Theorem 4.1, first sentence (p. 10:9). From a positive equilibrium $p'$ with $\sum_jp'_j=\sum_ie(i)$, build the linear program of §4, whose variables are prices and flows and whose combinatorial data are fixed by $p'$. Then $p'$, with a suitable flow, is an optimal solution of value $\sum_ie(i)$.
3. §4, second paragraph (p. 10:8). Every optimal solution of that LP with positive prices gives equilibrium prices.

Significance

The result is what makes the existence problem for these markets a problem in NP: a rational equilibrium of polynomial size is a certificate that can be checked, with Lemma 3.1, by one max-flow computation. The same rationality statement underlies the paper's PPAD-membership proof and its NP-completeness result for existence. It also marks the boundary with markets whose equilibria can be irrational, as happens for some non-separable utilities. In that sense it shows that separable piecewise-linear concave utilities keep the "linear" character of the problem even though computing an equilibrium becomes hard.

All three statements are proved in the source, and none of them has a machine-checked proof on the platform or, as far as is known, anywhere else. The mission produces the first formal account of piecewise-linear Fisher markets: the model, the forced/flexible/undesirable classification of segments, the max-flow test for equilibrium, and the linear program of §4. It also forces precision where the paper is informal. The §4 bang-per-buck inequalities are printed with their directions reversed, and the claim about optimal LP solutions needs positive prices. The formal statements record each of these choices.

Difficulty

The obvious argument is: "equilibria are solutions of a linear system, so a rational one exists". It fails as stated, because the set of equilibrium prices is not a polyhedron. Which segments a buyer buys depends on the prices themselves, through the ordering of the ratios $\mathrm{slope}/p_j$, so the equilibrium conditions are a finite union of polyhedral pieces glued along the price-dependent ordering. The work is to freeze the combinatorial structure of one given equilibrium and to show that the resulting fixed linear program still certifies equilibrium at every one of its optimal points. That second step is what Lemma 3.1 is for. The polynomial bit bound then needs a quantitative bound on the vertices of a rational LP, uniform in the market's encoding.

Formalization scope

Buyers and goods are Fin n and Fin g. Budgets, slopes and amounts are rationals (ℚ). Prices and allocations are reals (ℝ), so that "admits rational prices" is a real conclusion: the goal returns q : Fin g → ℚ whose cast is an equilibrium. The committed conventions are:

• each good has unit supply;
• budgets are positive;
• each $f^i_j$ is a list of (slope, amount) pairs of bounded segments together with the slope of its last, unbounded segment ("the last (infinite) segment", §6), with nonnegative slopes, positive amounts and nonincreasing slopes, stored inside the market structure;
• the unbounded segment has infinite value and, when flexible, gives its network edge infinite capacity; this is encoded logically (no upper bound on that edge);
• equilibrium requires exact clearing of every good, which by the paper's footnote 3 gives the same equilibrium prices as leaving zero-price goods partly unsold;
• the classes $Q_l$ are represented by the bang per buck of the flexible class, not by an index;
• parallel network edges are merged;
• max-flow is the supremum of the values of feasible flows on the good–buyer edges.

Hypotheses added relative to the page, each disclosed in its statement:

• positivity of the LP solution's prices (milestone 3).

The §2 condition on p. 10:7 is a sufficient condition for existence and is deliberately not a hypothesis of the goal, which assumes only that an equilibrium exists. Complexity-class statements ("in NP", "PPAD-complete") are out of scope. What is formalized is the explicit polynomial bit bound, with a polynomial chosen before the market. A goal with the polynomial chosen after the market, an encoding size that ignores the bits of the data, or an equilibrium notion without utility-maximizing bundles would be trivially satisfiable. The statements rule all three out.

Beyond this mission, a complete development needs LP theory with rational data: existence of optimal basic solutions and determinant bounds on their bit size. Existing platform results that may serve as substrate include SmaleNinth.exists_square_subsystem and SmaleNinth.abs_det_le_factorial_mul_pow. Contributions welcome: proofs of the milestones, a reusable bit-size theory for rational LP vertices, and the Arrow–Debreu analogue (Theorem 5.1).

Selected references

• V. V. Vazirani and M. Yannakakis, Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities, J. ACM 58(3), Article 10, 2011. https://doi.org/10.1145/1970392.1970394
• N. R. Devanur, C. H. Papadimitriou, A. Saberi and V. V. Vazirani, Market Equilibrium via a Primal–Dual Algorithm for a Convex Program, J. ACM 55(5), 2008. https://doi.org/10.1145/1411509.1411512
• E. Eisenberg and D. Gale, Consensus of Subjective Probabilities: The Pari-Mutuel Method, Ann. Math. Statist. 30(1), 1959. https://doi.org/10.1214/aoms/1177706369
• X. Chen, D. Dai, Y. Du and S.-H. Teng, Settling the Complexity of Arrow–Debreu Equilibria in Markets with Additively Separable Utilities, FOCS 2009. https://doi.org/10.1109/FOCS.2009.29
• W. C. Brainard and H. E. Scarf, How to Compute Equilibrium Prices in 1891, Cowles Foundation Discussion Paper 1272, 2000. https://cowles.yale.edu/research/cfdp-1272

Motivation

Stochastic approximation finds a root $x^*$ of an unknown map $R:\mathbb R^N\to\mathbb R^N$ from noisy evaluations $y_t=R(x_{t-1})+\xi_t$, by the Robbins–Monro recursion $x_t=x_{t-1}-\gamma_ty_t$. It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, $\sqrt t(x_t-x^*)\Rightarrow N(0,G^{-1}S(G^{-1})^T)$ with $G=R'(x^*)$ and $S$ the noise covariance, is achieved by the matrix step $\gamma_t=t^{-1}G^{-1}$, which requires knowing $G$.

Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of $G$: run the recursion with scalar steps that decrease more slowly than $1/t$ and output the running average $\bar x_t$ of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.

Timeline:

• 1951, Robbins and Monro: the recursion and its convergence in probability.
• 1958, Sacks: asymptotic normality of $x_t$ for $\gamma_t=\gamma/t$.
• 1988, Ruppert: averaging in one dimension, i.i.d.-type noise.
• 1990–1992, Polyak; Polyak and Juditsky: averaging in $\mathbb R^N$ for linear problems with martingale-difference noise (Theorem 1) and nonlinear problems (Theorem 2).

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},P)$ be a filtered probability space and $(\xi_t)_{t\ge1}$ an adapted $\mathbb R^N$-valued noise process. Given a nonrandom $x_0\in\mathbb R^N$ and step sizes $\gamma_t>0$, algorithm (7) is

$$x_t=x_{t-1}-\gamma_t\bigl(R(x_{t-1})+\xi_t\bigr),\qquad\bar x_t=\frac1t\sum_{i=0}^{t-1}x_i .$$

The error is $\Delta_t=x_t-x^*$ and the estimation error is $\bar\Delta_t=\bar x_t-x^*$.

The hypotheses are:

• Assumption 3.1: a Lyapunov function $V$ with $V(x)\ge\alpha|x|^2$, Lipschitz gradient, $V(0)=0$, $\nabla V(x-x^*)^TR(x)>0$ for $x\neq x^*$, and $\nabla V(x-x^*)^TR(x)\ge\lambda_1V(x-x^*)$ near $x^*$.
• Assumption 3.2: $|R(x)-G(x-x^*)|\le K_1|x-x^*|^{1+\lambda}$ near $x^*$, with $0<\lambda\le1$ and every eigenvalue of $G$ having positive real part.
• Assumption 3.3: $\xi_t$ is a martingale difference with $E(|\xi_t|^2\mid\mathcal F_{t-1})+|R(x_{t-1})|^2\le K_2(1+|x_{t-1}|^2)$. It splits as $\xi_t=\xi_t(0)+\zeta_t$, where $\xi_t(0)$ is a martingale difference whose conditional covariance tends to $S\succ0$ in probability and whose conditional second moments are uniformly integrable, and $E(|\zeta_t|^2\mid\mathcal F_{t-1})\le\delta(x_{t-1}-x^*)$ with $\delta(x)\to0$ as $x\to0$.
• Assumption 3.4: $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$, $\sum_t\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, $\gamma_t\to0$ and $\sum_t\gamma_t^2<\infty$.

The linear case, algorithm (2), is $R(x)=Ax-b$ with every eigenvalue of $A$ having positive real part.

Formalization targets

Goal: Theorem 2

Under Assumptions 3.1–3.4,

$$\bar x_t\to x^*\ \text{a.s.},\qquad\sqrt t\,(\bar x_t-x^*)\xrightarrow{D}N\bigl(0,\;G^{-1}S(G^{-1})^T\bigr).$$

Milestones

• Lemma 1, Part 2: under condition (4) on the steps, $t\gamma_t\to\infty$.
• Lemma 1: the matrices $\varphi_j^t=A^{-1}-\gamma_j\sum_{i=j}^{t-1}\prod_{k=j}^{i-1}(I-\gamma_kA)$ are uniformly bounded, and $\frac1t\sum_{j<t}\|\varphi_j^t\|\to0$.
• Lemma 2: the representation (A9) of $\sqrt t\,\bar\Delta_t$ for the linear error recursion.
• Theorem 1(a): the linear case, $\sqrt t(\bar x_t-x^*)\Rightarrow N(0,A^{-1}S(A^{-1})^T)$.
• Proof of Theorem 2, Part 1: $V(\Delta_t)$ converges almost surely to a finite limit.
• Proof of Theorem 2, p. 850: $x_t\to x^*$ almost surely.
• Proof of Theorem 2, Part 4: the average of the linearised process $\Delta^1_t=\Delta^1_{t-1}-\gamma_t(G\Delta^1_{t-1}+\xi_t)$ satisfies $\sqrt t(\bar\Delta^1_t-\bar\Delta_t)\to0$ almost surely.

Significance

Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance $G^{-1}S(G^{-1})^T$ is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).

The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.

Difficulty

The obvious approach analyses $x_t$ directly. It fails: with steps decreasing more slowly than $1/t$, $\sqrt t(x_t-x^*)$ diverges, and only the average has the $\sqrt t$ rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ in a quantitative way.

The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the $\sqrt t$ scale, which needs a summability estimate on $|\Delta_i|^{1+\lambda}i^{-1/2}$ obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by $\sqrt t$.

Formalization scope

Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given $\mathcal F_{t-1}$" is written with shifted indices ($\xi_{t+1}$ given $\mathcal F_t$). The algorithm is a recursive definition from $(x_0,\gamma,R,\xi)$, with $\gamma_0,\xi_0$ unused and $\bar x_t$ averaging $x_0,\dots,x_{t-1}$. Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its $\eta$–$\delta$ definition.

Corrections of the printed text, each used by the paper's own proof:

1. Assumption 3.1 prints $V(x^*)=0$ and $\ge\lambda V(x)$. Stated as $V(0)=0$ and $\ge\lambda_1V(x-x^*)$ (as printed they force $x^*=0$). The drift constant is renamed $\lambda_1$, since the paper uses $\lambda$ also in Assumption 3.2.
2. Eq. (10) is garbled as printed. It is stated as $\sum\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$, the form of Assumptions 4.7 and 5.6 and of p. 851.
3. Assumption 3.3's $\delta(x_{t-1})$ is stated as $\delta(x_{t-1}-x^*)$.
4. $\gamma_t\to0$ and $\sum\gamma_t^2<\infty$ are added to Assumption 3.4. The proof uses them (p. 849), and they do not follow from it.
5. $R$ is assumed continuous. The paper states no regularity of $R$, but its proof of almost sure convergence (pp. 849–850) needs $\nabla V(x-x^*)^TR(x)$ bounded away from $0$ on annuli around $x^*$, which continuity and Assumption 3.1 provide.
6. Lemma 1 and Theorem 1(a) are stated under condition (4) only. The constant-step condition (3) is false as printed ($A=\mathrm{diag}(1,10)$, $\gamma=1$), and Theorem 2 does not use it.
7. (A3) is stated with the norm inside, as its proof establishes.
8. (A9) and the linearised process of Part 4 are stated with $-\gamma_t\xi_t$ noise signs, and with $\Delta^1_0=\Delta_0$. The printed $+$ signs contradict (A8) at $t=2$.

Several formalizations would make the goal trivial, and all are ruled out:

• conditional expectations of non-integrable functions, which are $0$ in Lean (every noise process is required to be in $L^2$);
• a real supremum for the uniform integrability in Assumption 3.3, which is $0$ on unbounded families;
• an arbitrary process with a property in place of the recursion (7);
• a degenerate Dirac target (the covariance $G^{-1}S(G^{-1})^T$ is positive definite under the hypotheses).

Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.

Selected references

• B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
• H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22, 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• J. Sacks, Asymptotic distribution of stochastic approximation procedures, Ann. Math. Statist. 29, 373–405, 1958. https://doi.org/10.1214/aoms/1177706619
• D. Ruppert, Efficient estimations from a slowly convergent Robbins–Monro process, Cornell University ORIE Technical Report 781, 1988 (no stable online link located).
• H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 233–257, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8