Operations Research

Algorithmic Game Theory Probability·Captain: mikedeng1

Subjectivity and Correlation in Randomized Strategies II: Subjective Events Let Both Zero-Sum Players Beat the ValueResearch Paper

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

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$ .
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$ .
Lemma 4.4 (p. 77): if there is a public roulette, the same holds with "public" in place of " $i$ -secret".
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

9 thms2 active usersReviewed

Completed

Dynamic Programming Probability·Captain: mikedeng1

The Theory of Dynamic Programming: The Index Rule for Bellman's Stochastic Gold-Mining ProblemResearch Paper

Motivation

Richard Bellman's survey The theory of dynamic programming (Bull. Amer. Math. Soc. 60 (1954), 503–515, DOI 10.1090/s0002-9904-1954-09848-8) introduced dynamic programming to a general mathematical audience. It states the principle of optimality (§2, p. 504): "An optimal policy has the property that whatever the initial state and initial decisions are, the remaining decisions must constitute an optimal policy with regard to the state resulting from the first decisions", and derives from it the functional equations of finite and infinite stochastic decision processes, (4.2) and (5.1) (p. 506).

The survey illustrates the method on a small number of worked examples. The second of them, §8 "Stochastic gold mining" (pp. 508–509), is the one with a sharp answer: a two-armed sequential allocation problem with an absorbing failure state, whose optimal policy is a simple index rule. It is an early instance of the allocation-index phenomenon later made general by Gittins and Jones (1974) and Gittins (1979), and the paper itself notes (p. 509) that the rule "is not valid generally in more complicated decision processes", citing a counterexample of Karlin and Shapiro. The full treatment is in Bellman's RAND report R-245 and his 1957 book Dynamic Programming.

Setting

Two gold mines, Anaconda ( $A$ ) and Bonanza ( $B$ ), hold amounts $x \ge 0$ and $y \ge 0$ of gold. A single machine can be used in either mine. A use in Anaconda succeeds with probability $p$ : it then mines a fraction $r$ of the gold currently in Anaconda and the machine stays undamaged. With probability $1-p$ it mines nothing and the machine is destroyed. Bonanza behaves the same way with probability $q$ and fraction $s$ . While the machine works, the operator chooses the next mine; the aim is to maximize the expected amount mined before the machine is destroyed.

The only information the operator ever receives is that the machine still works. A policy is therefore a choice sequence $\sigma = (\sigma_0, \sigma_1, \dots) \in \{A, B\}^{\mathbb N}$ : the mine for use number $n$ , applied if uses $0, \dots, n-1$ succeeded. With $a_n$ , $b_n$ the numbers of $A$ - and $B$ -uses among the first $n$ , use $n$ collects $g_n = r x (1-r)^{a_n}$ if $\sigma_n = A$ and $g_n = s y (1-s)^{b_n}$ if $\sigma_n = B$ , and does so with probability $\prod_{k=0}^{n} \pi_{\sigma_k}$ ( $\pi_A = p$ , $\pi_B = q$ ). The expected return is

J(\sigma; x, y) = \sum_{n \ge 0} \Big(\prod_{k=0}^{n} \pi_{\sigma_k}\Big) g_n ,

and Bellman's (8.1) defines the optimal return

f(x, y) = \sup_\sigma J(\sigma; x, y).

In Lean these are expectedReturn p q r s σ x y and optimalReturn p q r s x y in the namespace BellmanTheoryDP.GoldMining.

Formalization targets

Milestone: the functional equation (8.2), p. 508

f(x, y) = \max\Big\{ p\,[r x + f((1-r)x, y)],\ q\,[s y + f(x, (1-s)y)] \Big\}.

Goal: the decision rule (8.3), p. 509, corrected

Write $V_A = p[rx + f((1-r)x, y)]$ and $V_B = q[sy + f(x, (1-s)y)]$ for the two branches of (8.2). For $0 < p, q, r, s < 1$ and $x, y \ge 0$ :

\frac{prx}{1-p} > \frac{qsy}{1-q} \Rightarrow V_A > V_B, \qquad \frac{prx}{1-p} < \frac{qsy}{1-q} \Rightarrow V_A < V_B, \qquad \frac{prx}{1-p} = \frac{qsy}{1-q} \Rightarrow V_A = V_B .

The paper prints the rule with $(1-r)$ and $(1-s)$ in the denominators:

a. For $prx/(1 - r) > qsy/(1 - s)$ , choose A, b. For $prx/(1 - r) < qsy/(1 - s)$ , choose B, c. For $prx/(1 - r) = qsy/(1 - s)$ , choose either.

and glosses it as "the locus of points where immediate expected gain over immediate expected loss is the same for both choices". The immediate expected loss is the probability of destroying the machine, $1-p$ (resp. $1-q$ ), not $1 - r$ . As printed the rule is false: with $p = 1/2$ , $r = 0.9$ , $q = 0.9$ , $s = 0.1$ , $x = 1$ , $y = 2$ the printed indices are $4.5 > 0.2$ , but $V_A \approx 0.924 < V_B \approx 1.055$ . The mission's goal is the corrected rule, the one the paper describes in words.

Companion: the index policy is optimal, p. 509

"Using this prescription, $f(x, y)$ may be computed recurrently": the choice sequence $\sigma^*$ generated by applying the corrected rule to the current amounts at every use satisfies $J(\sigma^*; x, y) = f(x, y)$ .

Significance

The decision rule reduces an optimization over infinite sequences to comparing two explicit numbers, one per mine, each depending only on that mine's own data. This is the defining property of an index policy, and gold mining is one of the earliest problems where it was observed. The functional equation (8.2) is the concrete form, for this process, of the infinite-horizon equation (5.1) that the paper states formally.

Formalizing the example yields a complete machine-checked instance of the principle of optimality for an infinite-horizon stochastic process whose state space (the amounts left in the two mines) is infinite, where the supremum over policies is not attained trivially and the finite-horizon recursion does not apply directly. It also records, with a checked statement, the correction of the misprint in (8.3). No machine-checked proof of (8.2) or (8.3) is known to exist.

Difficulty

The equation (8.2) looks immediate, and the paper calls it "easily seen". The informal argument treats $f$ as the value of an optimal policy, but $f$ is a supremum over infinite sequences that need not be attained a priori, and the return of a sequence is an infinite series. The finite-horizon recursion (4.2) does not apply as it stands, because the process has no last stage and its state space, the amounts left in the two mines, is infinite.

The rule (8.3) compares the two optimal continuations $f((1-r)x, y)$ and $f(x, (1-s)y)$ , which are themselves unknown. A comparison of the one-step gains alone does not decide it, as the misprinted rule shows. Parts a and b are strict preferences, so it is not enough to show that one choice is at least as good as the other.

Formalization scope

Representation. The mines are a two-element inductive type Mine; a policy is a function ℕ → Mine (ChoiceSeq). All quantities are real numbers. Randomized policies are mixtures of choice sequences and give no larger return, so they are not modelled. No restriction to stationary or Markov policies is made: $f$ is the supremum over all sequences.
Parameter ranges. The paper does not state them. The theorems assume $0 < p, q, r, s < 1$ and $x, y \ge 0$ (zero amounts allowed). $p, q < 1$ keeps the indices $prx/(1-p)$ , $qsy/(1-q)$ well defined.
Series and supremum. $J$ is a real tsum and $f$ a real iSup. For the parameter ranges above the terms are nonnegative, the partial sums are bounded by $x + y$ , and the family is bounded above, so neither Lean default value (0 for a divergent series or an unbounded supremum) arises; this is stated as the auxiliary theorem expectedReturn_le_add.
Survival indexing. The gold of use $n$ is counted only if use $n$ itself succeeds, so the survival product runs over $k \le n$ .
The misprint. The goal and the index policy use $(1-p)$ , $(1-q)$ in place of the printed $(1-r)$ , $(1-s)$ . The printed rule appears only as the quotation above.
No trivializing encoding. $f$ is defined as the supremum of expected returns over all choice sequences, per (8.1); it is not defined as a solution of (8.2), as the value of the index policy, or as a limit of value iteration, any of which would make the milestone or the goal true by definition.
Auxiliary theorems (not from the paper). The bound $0 \le J \le x + y$ with summability, the one-step unrolling $J(\sigma) = p[rx + J(\sigma'; (1-r)x, y)]$ when $\sigma_0 = A$ (and symmetrically), and the single-mine values $f(x, 0) = prx/(1 - p(1-r))$ , $f(0, y) = qsy/(1-q(1-s))$ are included as footholds. They are not milestones.
Related platform content. AllocationIndices.two_discount_index_policy_optimal (Gittins et al., Theorem 3.4) concerns Markov bandits whose rewards are discounted by $a^t$ at global time $t$ ; gold mining multiplies by the success probability of each use of the mine used, so it is a different model and is not reused. BertsekasDP.dp_algorithm_optimality is finite-horizon and does not give (8.2).

Contributions welcome: proofs of the auxiliary theorems, of (8.2), of the decision rule, and of the optimality of the index policy.

Selected references

R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), no. 6, 503–515. https://doi.org/10.1090/s0002-9904-1954-09848-8
R. Bellman, Dynamic Programming, Princeton University Press, 1957.
J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
J. C. Gittins, K. D. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9780470980033

4 thms2 active usersReviewed

Bandit Algorithms Machine Learning Statistics·Captain: mikedeng1

Online Decision Making with High-Dimensional Covariates: Regret Bound of the LASSO BanditResearch Paper

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

Proposition 1: a LASSO tail inequality for adaptively collected rows with conditionally subgaussian noise.
Lemma 1: a LASSO tail inequality when a constant fraction of the rows is i.i.d. with a compatible second-moment matrix.
Proposition 2: the forced-sample estimator of an optimal arm is within $h/(4x_{\max})$ of $\beta_i$ except with probability $5/t^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

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

School Choice: A Mechanism Design Approach 2: The Top Trading Cycles Mechanism with Type-Specific Quotas Is Strategy-ProofResearch Paper

Motivation

Many US school districts assign children to public schools centrally. Each family ranks the schools. Each school ranks the children by priority, which is set by state or local law (siblings, walking distance, a lottery). A procedure then turns these rankings into an assignment. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) cast this as a mechanism design problem. They showed that the mechanisms then in use in Boston, Columbus and Minneapolis gave families reasons to misreport their preferences. They proposed two alternatives: the student-optimal stable mechanism of Gale and Shapley, and a school-choice version of Shapley and Scarf's top trading cycles (TTC) mechanism.

Many districts also operate under controlled choice: court-ordered or voluntary rules that keep the racial or ethnic composition of each school within bounds. In Minneapolis, for instance, a 100-seat school could admit at most 75 majority and at most 55 minority students (paper, Section III). Such rules are implemented as type-specific quotas. Section III.B of the paper modifies TTC to respect these quotas. It proves that the modified mechanism keeps both properties that recommend TTC: it wastes nothing beyond what the quotas force (constrained efficiency, Proposition 6), and truth-telling is a dominant strategy (strategy-proofness, Proposition 7). This mission formalizes those two results.

Setting

There is a finite set $I$ of students and a finite set $S$ of schools. School $s$ has a capacity $q_s$ , and the total number of seats suffices: $|I|\le\sum_s q_s$ . Each student $i$ has a strict preference over all schools, encoded as a ranking $P_i : S\to\{0,\dots,|S|-1\}$ with rank $0$ the favourite. Each school $s$ has a strict priority ranking over all students, with rank $0$ the highest priority. Each student belongs to exactly one type $\tau(i)$ , and school $s$ has a type quota $q_s^t$ for each type $t$ .

An assignment $\nu$ gives each student a school or nothing ( $\varnothing$ , worse than every school). It satisfies the controlled choice constraints if every school $s$ receives at most $q_s$ students, and at most $q_s^t$ students of each type $t$ . An assignment $\mu$ is constrained efficient if no assignment satisfying the constraints makes every student weakly better off and some student strictly better off.

The top trading cycles mechanism with type-specific quotas, $\mathrm{TTC}^q$ , runs in steps. Each school keeps a counter $c_s$ (initially $q_s$ ) and one type counter $c_s^t$ for each type (initially $q_s^t$ ). A school is removed when $c_s$ reaches zero. At each step:

every remaining student points to her favourite remaining school with room for her type, that is, with $c_s>0$ and $c_s^{\tau(i)}>0$ ;
every remaining school points to its highest-priority remaining student, whatever her type;
every student on a cycle of this graph is assigned the school she points to and leaves;
that school's counter and its counter for her type each drop by one.

A direct mechanism is strategy-proof if no student can ever gain by misreporting her preference, whatever the others report.

Formalization targets

Goal: Proposition 7 (p. 23)

For every student $i$ , every profile $P$ of announced preferences and every alternative report $Q_i$ ,

\mathrm{TTC}^q(Q_i,P_{-i})(i)=s' \implies \mathrm{TTC}^q(P)(i)=s \text{ with } P_i(s)\le P_i(s').

This holds for all capacities without shortage, all quotas, all types and all priorities. The priorities are fixed data, not reported.

Milestones

Section III.B, Step 1 (p. 22). At every step there is at least one cycle, after the convention below has removed the students who cannot point.
The Lemma (Appendix, pp. 28–29; declared valid for the modified mechanism on p. 30). Fix the other students' reports, and suppose student $i$ is still present at the beginning of a step under two different reports of hers. Then the two runs have the same remaining students and the same counters at that point.
Proposition 6 (p. 23). $\mathrm{TTC}^q(P)$ satisfies the controlled choice constraints and is constrained efficient with respect to $P$ .

Significance

Strategy-proofness is what lets a district publish a simple instruction: rank the schools in your true order. A strategy-proof mechanism does not reward families who can afford to gather information and game the system. Proposition 7 shows that this guarantee survives the addition of flexible diversity quotas, which many districts are legally bound to impose. Proposition 6 shows that the quotas cost nothing beyond the losses they themselves cause. Both results were proved in 2003 by pen and paper. The published proof of Proposition 7 is a short adaptation of the proof of Proposition 4 (strategy-proofness of plain TTC). It rests on a lemma about how the algorithm's intermediate states depend on one student's report.

To our knowledge neither result has a machine-checked proof. The related platform theorem AGT.ttc_strategyproof concerns the Shapley–Scarf housing market, where every agent owns one house and the mechanism selects the core. It does not cover capacities, priorities or quotas. A formal proof here would check the adaptation that the paper leaves to the reader, and would give a reusable formal model of cycle-clearing allocation algorithms with multiple counters.

Difficulty

The algorithm clears all cycles of a step at once, and a student's report changes the graph at every step she is present. The paper's argument compares two whole runs of the algorithm, under the true report and under a misreport, step by step. That comparison needs precise control of which parts of the state a single student's report can influence, and when. A local argument about one step does not suffice. The student's outcome can depend on cycles that form several steps after the two runs could first have diverged.

With quotas, the pointing graph also depends on the type counters. A school can be present but closed to one type, and a school points to its best remaining student even when it has no room for her type. The comparison must therefore track the type counters as well as the set of remaining schools. Efficiency cannot be read off step by step against unrestricted matchings either: every competing assignment must satisfy both the capacity and the quota constraints.

Formalization scope

Students, schools and types are finite types; no nonemptiness is assumed. Preferences and priorities are bijective rankings onto Fin, so strictness is built in. Rank $0$ is the favourite or the highest priority. The no-shortage condition $|I|\le\sum_s q_s$ appears in every theorem, as the standing assumption of Section I. No relation between $q_s$ and $q_s^t$ is imposed, which generalises the paper.

The algorithm is a concrete, total definition: a state with remaining students, counters, type counters and partial assignments, a step map that clears all cycles simultaneously, and $|I|$ iterations. run … t is the state at the beginning of the paper's Step $t+1$ .

The paper's step is undefined when a remaining student has no remaining school with room for her type. She cannot point, and the promised cycle may not exist. The formalization adopts one convention: at the beginning of each step, such a stuck student is removed unassigned, and her outcome is $\varnothing$ , ranked below every school. Counters only decrease, so a stuck student stays stuck. Whenever nobody gets stuck, the algorithm is exactly the paper's, and when every quota is at least the capacity it is plain TTC. The goal and Proposition 6 are stated for assignments that may leave students unassigned. When everyone is assigned, they coincide with the paper's statements over matchings.

The formalization does not add a hypothesis that the run never gets stuck. Such a hypothesis would restrict the algorithm's own behaviour and could make the theorems vacuous. Nor may strategy-proofness be weakened to comparisons at the truthful profile only: the others' reports and the misreport are arbitrary.

Contributions welcome: invariants of the step map (counters bounded by the initial values, assigned students leave for good), the cycle-existence lemma for functional graphs on finite sets, and the comparison lemma. These pieces are shared with the plain-TTC mission of this series.

Selected references

Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

School Choice: A Mechanism Design Approach 1: The Top Trading Cycles Mechanism Is Strategy-ProofResearch Paper

Motivation

Public school districts in many US cities let families rank schools and then assign seats by a centralized procedure. Each school has a limited number of seats, and state or local law gives some students priority at some schools, for example for a sibling already enrolled or for living within walking distance. Abdulkadiroğlu and Sönmez (Columbia Economics Discussion Paper 0203-18, 2003; published in the American Economic Review 93(3), 2003) framed this as a mechanism design problem and showed that the mechanism then used in Boston rewards families who misreport their preferences. They proposed two replacements with written proofs of their properties. This mission covers the second one, the top trading cycles mechanism, and its two properties: every outcome is Pareto efficient, and no student can gain by misreporting.

The paper drew on earlier results for simpler allocation problems:

1974: Shapley and Scarf introduce housing markets and Gale's top trading cycles algorithm, in which each agent owns one house.
1977: Roth and Postlewaite show the algorithm finds the unique core allocation of a housing market.
1982: Roth proves the core mechanism for housing markets is strategy-proof.
1999: Abdulkadiroğlu and Sönmez adapt the algorithm to house allocation with existing tenants and prove strategy-proofness.
2000: Pápai introduces hierarchical exchange rules, a wider class that includes these mechanisms.
2003: the paper formalized here extends the algorithm to schools with capacities and school-specific priorities (Propositions 3 and 4).

Setting

A school choice problem consists of a finite set $I$ of students, a finite set $S$ of schools, a capacity $q_s \in \mathbb N$ for each school, a strict preference $P_i$ of each student over all schools, and a strict priority ordering $\succ_s$ of each school over all students. The standing assumption is that there is no shortage of seats:

|I| \le \sum_{s\in S} q_s .

Preferences are rankings: $P_i(s)\in\{0,\dots,|S|-1\}$ is the rank of $s$ for student $i$ , with rank $0$ the favourite. Priorities are rankings of students in the same way, with rank $0$ the highest priority. A matching is a map $\mu : I\to S$ with $\#\{i:\mu(i)=s\}\le q_s$ for every school $s$ . A matching $\mu$ is Pareto efficient if no other matching $\nu$ gives every student a weakly better school ( $P_i(\nu(i))\le P_i(\mu(i))$ ) and some student a strictly better one.

A direct mechanism maps the reported preference profile, together with the fixed priorities and capacities, to a matching. It is strategy-proof if no student can ever obtain a school she strictly prefers by changing her own report while the others keep theirs.

The top trading cycles algorithm keeps a counter $c_s$ of free seats at each school, starting at $q_s$ . A school is remaining while $c_s>0$ . At each step every remaining student points to her favourite remaining school, and every remaining school points to the remaining student with the highest priority for it. A cycle is a list $(s_1,i_1,\dots,s_k,i_k)$ of distinct schools and students in which $s_1$ points to $i_1$ , $i_1$ points to $s_2$ , and so on, and $i_k$ points to $s_1$ . Every student on a cycle is assigned the school she points to and is removed. Each school on a cycle loses one seat. All cycles present at a step are cleared at that same step. The top trading cycles mechanism $\mathrm{TTC}(q,\succ,P)$ returns the resulting assignment.

Formalization targets

Goal: Proposition 4 (strategy-proofness)

For all capacities with no shortage, all priorities, every profile $P$ , every student $i$ and every alternative report $Q_i$ , student $i$ is assigned schools $s = \mathrm{TTC}(q,\succ,P)(i)$ and $s' = \mathrm{TTC}(q,\succ,(Q_i,P_{-i}))(i)$ , and

P_i(s) \le P_i(s') .

Milestones

At every step at which some student remains, there is a cycle (Section II.B, p. 15).
After $|I|$ steps no student remains, and the outcome is a matching (Section II.B, p. 16).
Lemma (Appendix, pp. 28–29): if student $i$ is still remaining at the beginning of a step under two different reports of her own, the remaining students and the remaining schools at that point are the same under both reports.
Proposition 3 (p. 17): the outcome is a Pareto efficient matching with respect to the reported profile.
When all schools share one priority ordering $\pi$ , the mechanism equals the serial dictatorship induced by $\pi$ (Section II.B, p. 16).

Significance

Strategy-proofness means truthful reporting is a dominant strategy for every student. Families need no information about other families' reports. Under the Boston mechanism, ranking a popular school first can cost a student her priority at her second choice. Proposition 3 separates the top trading cycles mechanism from the Gale–Shapley student-optimal stable mechanism, which is also strategy-proof but can select Pareto dominated matchings.

The results are proved in the paper, in short prose arguments in its Appendix. To the best of our knowledge they have no machine-checked proof. The platform already has the housing-market version, AGT.ttc_strategyproof, but that statement covers one house per agent with the mechanism characterised as the core. Capacities, school priorities and the step-by-step algorithm are absent from it. This mission produces a checked account of the algorithm with capacities and counters, together with its termination and invariance properties.

Difficulty

The paper's argument moves from the step at which student $i$ leaves under one report to the step at which she leaves under another. It relies on the claim that the cycles formed before either step are unaffected by $i$ 's report. Informally, $i$ is not on a cycle yet, so what she points to does not matter. Formally, "the same cycles form" requires comparing two runs of a simultaneous-clearing procedure step by step. At each step one has to show that the set of cycles, and hence the counters and the remaining schools, agree, even though $i$ points to different schools in the two runs. Reasoning about a single cycle at a time does not work, because the algorithm clears all cycles of a step at once. Termination is also not immediate: without the no-shortage condition the algorithm can leave students unassigned. Seats are counted with multiplicity, so a school can stay in the market for several steps.

Formalization scope

Everything lives in the namespace SchoolChoice.TTC. Students and schools are arbitrary finite types with decidable equality; the set of students may be empty. Capacities are q : S → ℕ, and a school of capacity zero is never remaining. A preference is a bijection S ≃ Fin (card S) and a priority is a bijection I ≃ Fin (card I), in both cases with rank 0 the best. Strictness and completeness of both therefore hold by construction, and every school is acceptable. A state of the algorithm consists of the remaining students, the counters and the assignments made so far. run q pri P t is the state after t completed steps, which is the beginning of the paper's Step t + 1. The mechanism ttc q pri P : I → Option S reads off the assignment after card I steps. Every theorem assumes card I ≤ ∑ s, q s.

The algorithm is a concrete, deterministic definition that clears all cycles at every step. The mechanism is not defined as "some Pareto efficient matching" or characterised by properties, since that would make Proposition 3 trivial. The goal asserts that both outcomes exist, so an unassigned outcome cannot satisfy it vacuously. The misreport, the other students' reports and the priorities are all universally quantified.

A complete development needs termination of the algorithm, a combinatorial account of the pointing graph (cycles in a finite functional graph), and the step-by-step invariance argument of the Lemma. The last two are reusable for the type-specific quota variant and for other trading-cycle mechanisms. Contributions of intermediate lemmas are welcome: counter invariants such as "the sum of the counters is at least the number of remaining students", monotonicity of the remaining sets, and the fact that a student on a cycle receives her favourite remaining school.

Selected references

Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, Columbia University Department of Economics Discussion Paper No. 0203-18, 2003. https://doi.org/10.7916/D8057T27
Atila Abdulkadiroğlu and Tayfun Sönmez, School Choice: A Mechanism Design Approach, American Economic Review 93(3), 729–747, 2003. https://doi.org/10.1257/000282803322157061
Lloyd Shapley and Herbert Scarf, On Cores and Indivisibility, Journal of Mathematical Economics 1(1), 23–37, 1974. https://doi.org/10.1016/0304-4068(74)90033-0
Alvin E. Roth and Andrew Postlewaite, Weak versus Strong Domination in a Market with Indivisible Goods, Journal of Mathematical Economics 4(2), 131–137, 1977. https://doi.org/10.1016/0304-4068(77)90004-0
Alvin E. Roth, Incentive Compatibility in a Market with Indivisible Goods, Economics Letters 9(2), 127–132, 1982. https://doi.org/10.1016/0165-1765(82)90003-9
Atila Abdulkadiroğlu and Tayfun Sönmez, House Allocation with Existing Tenants, Journal of Economic Theory 88(2), 233–260, 1999. https://doi.org/10.1006/jeth.1999.2553
Szilvia Pápai, Strategyproof Assignment by Hierarchical Exchange, Econometrica 68(6), 1403–1433, 2000. https://doi.org/10.1111/1468-0262.00166

9 thms2 active usersReviewed

Algorithmic Game Theory Linear Optimization Probability·Captain: mikedeng1

A General Framework for the Study of Decentralized Distribution Systems: A Core Allocation Rule Whose Nash Equilibrium Is First-BestResearch Paper

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:

"Dual prices" means any optimal solution of the dual of (6) for $\mathcal N$ ; Theorem 4.1 is stated for every such solution.
"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.
" $[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.
"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.
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

10 thms2 active usersReviewed

Completed

Discrete Geometry Linear Optimization Optimization·Captain: mikedeng1

Elementare Theorie der konvexen Polyeder I: A Point on All Extreme Supports of a Finite Cone Is a Nonnegative Combination of at Most n GeneratorsResearch Paper

Motivation

A polyhedral cone can be described in two ways: as the set of nonnegative combinations of finitely many vectors (a finitely generated cone), or as the intersection of finitely many closed half-spaces through the origin. That the two descriptions give the same class of sets is the Minkowski–Weyl theorem. It is the structural basis of linear programming: the simplex method, LP duality, Farkas' lemma, and the vertex/facet description of polytopes used throughout combinatorial optimization all rest on it.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv. 7, 290–306) gives an elementary, self-contained proof of both directions. Its first result, which Weyl calls the Hauptsatz (main theorem, Satz 1), is the direction "finitely generated ⇒ finite intersection of half-spaces", in a sharp form: the half-spaces needed are exactly the extreme supports of the generating set, i.e. its facets. Its sharpening, Satz 2, bounds the number of generators needed to represent a point by the dimension $n$ . This mission formalizes §§1–2 of the paper (pp. 290–295): the Hauptsatz, its sharpening, and the steps of Weyl's inductive proof.

Timeline:

1896, H. Minkowski, Geometrie der Zahlen: polytopes as bounded intersections of half-spaces and as convex hulls of finitely many points.
1911, C. Carathéodory: a point in the convex hull of a set in $\mathbb{R}^d$ is a convex combination of at most $d+1$ of its points (Rend. Circ. Mat. Palermo 32).
1935, H. Weyl: the present paper; Satz 1 and Satz 2 for cones, with the dual statements in §3 and the polytope theorem in §4.

Setting

Points of $\mathbb{R}^n$ are $n$ -tuples $x = (x_1, \ldots, x_n)$ , and $\langle \alpha, x \rangle = \alpha_1 x_1 + \cdots + \alpha_n x_n$ . A vector $\alpha \ne 0$ determines the half-space $\{x : \langle\alpha,x\rangle \ge 0\}$ ; positive multiples of $\alpha$ give the same half-space.

A point system $S$ is a finite set of points of $\mathbb{R}^n$ . It is non-degenerate if its points do not all satisfy one equation $\langle\alpha,x\rangle = 0$ with $\alpha \neq 0$ , i.e. the only $\alpha$ orthogonal to every point of $S$ is $0$ .

A half-space $\langle\alpha,x\rangle\ge 0$ ( $\alpha\ne 0$ ) is a support of $S$ if every point of $S$ lies in it. It is an extreme support if, in addition, equality $\langle\alpha,x\rangle = 0$ holds at $n-1$ linearly independent points $x$ of $S$ .

A point $x$ is representable by $S$ if it is a nonnegative combination of the points of $S$ :

x = \sum_{s\in S} c_s\, s, \qquad c_s \ge 0 .

The set of points lying in all extreme supports of $S$ is Weyl's konvexe Pyramide. In the Lean development these objects are Representable, NonDegenerate, IsSupport and IsExtremeSupport in the namespace WeylPolyhedra.Pyramid, with points of type Fin n → ℝ and $\langle\alpha,x\rangle$ written α ⬝ᵥ x.

Formalization targets

Goal: Satz 2 (Verschärfung des Hauptsatzes), p. 295

For a finite non-degenerate $S \subset \mathbb{R}^n$ and a point $x$ with $\langle\alpha,x\rangle\ge 0$ for every extreme support $\alpha$ of $S$ ,

\exists\, T \subseteq S,\quad |T| \le n,\quad x = \sum_{t\in T} c_t\, t,\ \ c_t \ge 0 .

Satz 1 (Hauptsatz), p. 291

Under the same hypotheses, $x$ is representable by $S$ . Satz 2 contains Satz 1.

Steps of the proof (§1–§2)

A finite non-degenerate $S$ has only finitely many extreme supports, up to positive scaling (p. 291).
The reduction step of case a) (p. 292): if $S$ has an extreme support $\beta$ and $p$ satisfies all extreme supports, there are $e \in S$ with $\langle\beta,e\rangle>0$ and $\lambda\ge 0$ such that $q = p-\lambda e$ still satisfies all extreme supports and lies on the plane of one of them.
The lifting step (p. 293): with $x_n \ge 0$ an extreme support of $S$ and $S_0$ the points on $x_n = 0$ , every extreme support $\beta$ of $S_0$ in $\mathbb{R}^{n-1}$ lifts to the extreme support $\beta_1x_1+\cdots+\beta_{n-1}x_{n-1} - \mu x_n \ge 0$ of $S$ (inequality (6)).
Case b) (p. 291, proved pp. 293–294): if $S$ has no extreme support, every point of $\mathbb{R}^n$ is representable by $S$ .

Significance

Satz 1 together with its trivial converse identifies the cone generated by $S$ with the intersection of its extreme-support half-spaces. This is one half of the Minkowski–Weyl theorem for cones, and it names the half-spaces: they are the facets of the cone. Satz 2 adds the conic form of Carathéodory's theorem: every point of a cone generated by a finite spanning set in $\mathbb{R}^n$ is a nonnegative combination of at most $n$ generators. In linear programming this is the statement that a feasible system has a basic feasible solution. The second mission in this series, on §§3–4 of the paper, uses Satz 1 to prove that a bounded region cut out by finitely many inequalities is the convex hull of finitely many points, and conversely.

On formalization status: Mathlib defines finitely generated and dually finitely generated pointed cones (PointedCone, PointedCone.DualFG) and proves Carathéodory's theorem for convex hulls (convexHull_eq_union), but, at the pinned revision, it does not prove the Minkowski–Weyl theorem or the facet description of a finitely generated cone. The results are classical and proved in the paper; this mission produces machine-checked proofs of them, in Weyl's formulation with extreme supports, together with the intermediate steps of his induction.

Difficulty

The hypothesis only controls $x$ against the extreme supports, not against every support. Showing that $x$ lies in the cone generated by $S$ whenever $\langle\alpha,x\rangle\ge 0$ holds for every support is the conic Farkas lemma, which follows from a separating hyperplane argument. Here that argument is not enough: a separating hyperplane is a support, but in general not an extreme one, and the statement is about the finitely many extreme ones. The proof has to produce, for a point outside the cone, a violated extreme support, which requires control over the facet structure of the cone.

The dimension count of Satz 2 is a second difficulty. An induction on the dimension naturally gives $n$ generators in one case and $n+1$ in another (a point of a half-space needs one generator on each side), and Weyl notes that he could not avoid a detour to recover the bound $n$ . The case where $S$ has no extreme support at all must also be handled separately; it is not vacuous, since $S$ can then generate all of $\mathbb{R}^n$ .

Formalization scope

Conventions committed to in Lean:

$\mathbb{R}^n$ is Fin n → ℝ; points and normals share this type (the dual space is identified with $\mathbb{R}^n$ , as in the paper). The pairing is dotProduct, written α ⬝ᵥ x.
A point system is a Finset (Fin n → ℝ). The zero vector is not excluded.
A support normal satisfies α ≠ 0. Extreme supports require a subset T ⊆ S with T.card = n - 1 whose elements are linearly independent in the vector space $\mathbb{R}^n$ .
"All extreme support equations are satisfied" in Satz 1 is read as the inequalities $\langle\alpha,x\rangle\ge0$ for every extreme normal $\alpha$ , as the proof and Satz 2 make explicit. The hypothesis quantifies over all extreme normals, so no representatives are chosen.
"Positive-linear" combinations have nonnegative coefficients (display (3)). In Satz 2 the subset $T$ is not required to be linearly independent.
Finiteness of extreme supports is stated up to positive scaling.
The lifting step is stated in the coordinates Weyl fixes on p. 293: $\mathbb{R}^n$ is Fin (m+1) → ℝ, the extreme support is $x_n \ge 0$ (Fin.last m), $S_0$ is projected by Fin.init, and $\mu$ is given together with hypotheses that it is the attained minimum. The hypothesis $n \ge 2$ is made explicit.

Replacing extreme supports by all supports in the hypothesis of Satz 1 or Satz 2 would turn the goal into a much weaker theorem (the conic Farkas lemma plus Carathéodory) and is not an admissible formalization. Dropping non-degeneracy makes Satz 1 false: for $S = \{e_1\} \subset \mathbb{R}^2$ the extreme supports are $\pm x_2 \ge 0$ , and $x = (-1, 0)$ satisfies both without being a nonnegative multiple of $e_1$ .

A complete development needs basic linear algebra over Fin n → ℝ (hyperplanes through $n-1$ independent points, projection to a coordinate hyperplane) and finite minimisation. The facet description of finitely generated cones, conic Carathéodory and the finiteness of facets are reusable beyond this mission, including for the second mission of the series. Contributions of lemmas on PointedCone that connect Representable with PointedCone.span are welcome.

Selected references

H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici 7 (1935), 290–306. https://doi.org/10.1007/BF01292722
C. Carathéodory, Über den Variabilitätsbereich der Fourier'schen Konstanten von positiven harmonischen Funktionen, Rendiconti del Circolo Matematico di Palermo 32 (1911), 193–217. https://doi.org/10.1007/BF03014795
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (the Farkas–Minkowski–Weyl theorem). ISBN 978-0-471-98232-6
G. M. Ziegler, Lectures on Polytopes, Springer GTM 152, 1995, Lecture 1. https://doi.org/10.1007/978-1-4613-8431-1

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Complexity Theory·Captain: mikedeng1

Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities II: An Exact 3-Cover Exists iff the Constructed Market Has an EquilibriumResearch Paper

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$ :

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;
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$ ;
agent $x_j$ owns $1/6$ unit of good $x_j$ ; one segment of slope $1$ , length $1/12$ for good $0$ ;
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

Lemma 8.2: an exact cover yields an equilibrium of $D(\mathcal C)$ .
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.
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.
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

12 thms2 active usersReviewed

Algorithmic Game Theory Linear Optimization·Captain: mikedeng1

Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities I: Fisher Markets with an Equilibrium Have Rational Equilibrium Prices of Polynomial Bit SizeResearch Paper

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

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)$ .
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)$ .
§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

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Optimization+1·Captain: mikedeng1

An Analysis of Several Heuristics for the Traveling Salesman Problem II: Every Insertion Method Is Within ⌈lg n⌉ + 1 of the Optimal TourResearch Paper

Motivation

The traveling salesman problem asks for a shortest closed route visiting every node of a weighted complete graph exactly once. It is NP-hard, so practitioners use fast heuristics, and the basic question about a heuristic is how far from optimal its tour can be. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the simple constructive heuristics under the triangle inequality: nearest neighbor, the family of insertion methods, and several variants.

Insertion methods build a tour by growing it one node at a time. They are among the most widely used construction heuristics in practice and in textbooks, and they differ only in the rule that chooses which node to insert next: the nearest one, the cheapest one, the farthest one, a random one, or any other. This mission formalizes the paper's result that holds for the whole family at once, regardless of that rule: every insertion method produces a tour at most $\lceil \lg n\rceil + 1$ times longer than an optimal one (Theorem 3, p. 571).

Timeline. 1977: Rosenkrantz, Stearns and Lewis prove $\lceil\lg n\rceil+1$ for every insertion method (Theorem 3), $\tfrac12(\lceil\lg n\rceil+1)$ for nearest neighbor (Theorem 1), both from a shared counting lemma (Lemma 1), and the constant $2$ for nearest and cheapest insertion (Theorem 4). 1994: Bafna, Kalyanasundaram and Pruhs (Theoretical Computer Science 125, 1994) give instances on which some insertion methods reach ratio $\Omega(\log n/\log\log n)$ , so the logarithmic growth cannot be replaced by a constant for the family as a whole.

Setting

A traveling salesman graph with $n$ nodes consists of a finite node set $N$ with $|N|=n$ and a distance $d:N\times N\to\mathbb R$ with $d(i,j)=d(j,i)$ , $d(i,j)\ge 0$ and $d(i,j)+d(j,k)\ge d(i,k)$ for all nodes (the triangle inequality). A tour visits every node once and returns to its start; its length is the sum of its edge lengths, and OPTIMAL is the least length of a tour.

A subtour is a tour on a subset of the nodes; a single node is a tour without edges. Given a subtour $T$ and a node $k\notin T$ , TOUR $(T,k)$ is obtained by choosing an edge $(x,y)$ of $T$ minimizing

d(x,k)+d(k,y)-d(x,y)

and replacing it by the edges $(x,k)$ and $(k,y)$ ; if $T$ is a single node $i$ , TOUR $(T,k)$ is the two-node tour $(i,k),(k,i)$ . COST $(T,k)$ is the length of TOUR $(T,k)$ minus the length of $T$ .

An insertion method constructs subtours $T_1,\dots,T_n$ with $T_1=\{a_0\}$ a single node and $T_{i+1}=\mathrm{TOUR}(T_i,a_i)$ for some node $a_i\notin T_i$ , $1\le i<n$ . The final tour $T_n$ is the approximation, and INSERT denotes its length. No rule for choosing the $a_i$ is fixed, and ties between minimizing edges are broken arbitrarily.

Write $\lg$ for the logarithm to base 2 and $\lceil x\rceil$ for the least integer $\ge x$ .

Formalization targets

Goal: Theorem 3

For every traveling salesman graph with $n\ge 1$ nodes and every run of every insertion method,

\mathrm{INSERT}\ \le\ \bigl(\lceil\lg n\rceil+1\bigr)\cdot\mathrm{OPTIMAL}.

Milestones

(2.2), shortcutting: visiting a subset of the nodes in the order of a tour gives a tour of the subset that is no longer.
(2.1): if the numbers $l_1\ge\dots\ge l_n$ satisfy $d(p,q)\ge\min(l_p,l_q)$ for distinct $p,q$ , then $\mathrm{OPTIMAL}\ge 2\sum_{i=k+1}^{\min(2k,n)} l_i$ for $1\le k\le n$ .
Lemma 1: if $d(p,q)\ge\min(l_p,l_q)$ for distinct nodes and $l_p\le\frac12\mathrm{OPTIMAL}$ for all $p$ , then

\sum_p l_p\le\tfrac12\bigl(\lceil\lg n\rceil+1\bigr)\mathrm{OPTIMAL}.

Lemma 2: $\mathrm{COST}(T,k)\le 2\,d(k,j)$ for every node $j$ of $T$ .
(3.7): $\mathrm{INSERT}=\sum_{i=1}^{n-1}\mathrm{COST}(T_i,a_i)$ .
(3.10): $\mathrm{COST}(T_i,a_i)\le 2\,d(a_i,a_j)$ whenever $j<i$ .
(3.12): $\mathrm{COST}(T_i,a_i)\le\mathrm{OPTIMAL}$ for $1\le i<n$ .

Significance

The result. Theorem 3 is a guarantee for an entire class of algorithms rather than for one. Any rule for choosing the next node, including rules designed for speed or for empirical quality, inherits a worst-case ratio of $\lceil\lg n\rceil+1$ from the insertion step alone. The rule matters only for improving on that: nearest and cheapest insertion achieve the constant $2(1-1/n)$ (Theorem 4 and its corollary, the subject of the third mission of this series), while the logarithmic bound remains the best general statement for other rules, such as farthest or arbitrary insertion. Lemma 1 is reusable on its own: it converts "every node carries a charge bounded by half the optimum and by its distance to other nodes" into a logarithmic bound, and the same lemma yields the nearest neighbor bound of Theorem 1.

Formalizing it. The theorem has been proved since 1977; the work here is a machine-checked proof of the known argument together with a reusable library for subtours, insertion and insertion costs. The companion nearest neighbor bound (Theorem 1) is already on the platform as SupplyChainTheory.nearest_neighbor_bound (proved), and nearest insertion with constant 2 as SupplyChainTheory.nearest_insertion_bound; neither covers arbitrary insertion methods or states Lemma 1 separately.

Difficulty

The per-step facts are local: each insertion is cheap relative to a node already present (Lemma 2) and relative to OPTIMAL (3.12). The obvious way to combine them, adding up $n-1$ costs each at most OPTIMAL, gives only the ratio $n-1$ . The logarithm comes from a global counting argument over all nodes simultaneously (Lemma 1), in which OPTIMAL is compared with tours on nested subsets of nodes of doubling size, and the per-node charges must be matched against the edges of those tours. Formally, the delicate parts are the bookkeeping of subtours as they grow (that every earlier node lies on the current subtour, and that the insertion cost equals the length increase), the shortcutting of a tour to an arbitrary subset, and the ceiling-of-logarithm arithmetic.

Formalization scope

Nodes are Fin n; a tour of all nodes is a permutation τ : Equiv.Perm (Fin n), and OPTIMAL is the minimum of the tour length over the finite, nonempty set of permutations. Subtours are duplicate-free lists of nodes, with closed length $d(x_0,x_1)+\dots+d(x_{m-1},x_0)$ . TOUR $(T,k)$ is encoded as inserting $k$ at a list position whose resulting length is minimal among all positions; inserting at a position removes exactly one edge of $T$ and raises the length by exactly $d(x,k)+d(k,y)-d(x,y)$ , so this is the paper's rule, with every tie-breaking allowed. COST is the minimum length increase over positions. The paper's 1-based subtour index is kept ( $T_1=[a_0]$ , $T_n$ final). $\lceil\lg n\rceil$ is Nat.clog 2 n. All quantities are real.

Conventions and deviations, each disclosed in the item statements:

The distance satisfies $d(i,i)=0$ , a normalization not in the paper; a loop never enters any length.
Ratios are multiplied out ( $\mathrm{INSERT}\le c\cdot\mathrm{OPTIMAL}$ ), so the paper's exclusion of the identically zero distance (1.1) is not needed.
Condition a) of Lemma 1 is required for distinct nodes only. The page says "for all nodes $p$ and $q$ ", which for $p=q$ would force every $l_p\le 0$ and make the lemma inapplicable in the proof of Theorem 3; the proof uses the condition only on edges of a tour.
(2.2) is stated for every subset of the nodes and every tour, which is what the shortcut argument shows; the paper applies it to one specific subset and an optimal tour.
(2.1) uses 0-based node labels, so its range $k+1,\dots,\min(2k,n)$ becomes $k,\dots,\min(2k,n)-1$ .

The goal quantifies over every run: any choice of the inserted nodes $a_i$ and any minimizing insertion position. Adding a selection rule (nearest, cheapest) or fixing a tie-breaking would state a weaker, different theorem; restricting to instances with OPTIMAL $=0$ or to a fixed small $n$ would trivialize it.

Reusable beyond this mission: the subtour and insertion library (closed length of a list, TOUR, COST, insertion runs) and Lemma 1, which also yields Theorem 1. Contributions welcome: proofs of the milestones, general lemmas about the closed length of List.insertIdx and of filtered lists, and a proof of Theorem 1 from this mission's Lemma 1.

Selected references

D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM Journal on Computing 6(3):563–581, 1977. https://doi.org/10.1137/0206041
V. Bafna, B. Kalyanasundaram, K. Pruhs, Not all insertion methods yield constant approximate tours in the Euclidean plane, Theoretical Computer Science 125(2):345–353, 1994.

10 thms2 active usersReviewed

Completed

Optimization Probability·Captain: mikedeng1

Robust Mean-Covariance Solutions for Stochastic Optimization I: The General Projection Property of Mean-Covariance Distribution ClassesResearch Paper

Motivation

In robust stochastic optimization a decision maker chooses a decision $x$ whose outcome depends on a random vector $\mathbf R$ , but knows only the first two moments of $\mathbf R$ : its mean vector $\mu$ and its covariance matrix $\Sigma$ . The decision is evaluated by its worst-case expected utility over every distribution consistent with those moments. This model is standard in portfolio selection, where estimated means and covariances are the usual inputs, and in pricing and inventory problems with mean-variance information. It goes back to Scarf's min-max newsvendor (1958) and the Chebyshev-type moment bounds of Bertsimas and Popescu (2005).

For a linear outcome $x'\mathbf R$ , such as the return of a portfolio with weights $x$ , the robust objective is

U(x) = \min_{\mathbf R \sim (\mu,\Sigma)} E[u(x'\mathbf R)],

an optimization over an infinite-dimensional set of $n$ -variate distributions. Popescu (2007) showed that this problem depends on $\mu$ and $\Sigma$ only through the scalar mean $\mu_x = x'\mu$ and variance $\sigma_x^2 = x'\Sigma x$ . The multivariate robust problem then reduces to a univariate moment problem, and for many utilities to a parametric quadratic program. The reduction rests on one structural fact, the general projection property, which this mission formalizes.

Setting

Fix a dimension $n$ . A law on $\mathbb R^n$ is a Borel probability measure on $\mathbb R^n$ . For a vector $\mu \in \mathbb R^n$ and a real $n\times n$ matrix $\Sigma$ , the mean-covariance class $\mathbb M^n_{(\mu,\Sigma)}$ is the set of laws $P$ under which every coordinate $R_i$ has a finite second moment and

\int R_i\,dP(R) = \mu_i, \qquad \int (R_i-\mu_i)(R_j-\mu_j)\,dP(R) = \Sigma_{ij} \qquad (1\le i,j\le n).

Writing $\mathbf R \sim (\mu,\Sigma)$ means that the law of $\mathbf R$ lies in $\mathbb M^n_{(\mu,\Sigma)}$ . For $n=1$ the superscript is dropped: for real $m$ and $v$ , $\mathbb M_{(m,v)}$ is the set of laws on $\mathbb R$ with finite second moment, mean $m$ and variance $v$ .

For a vector $x \in \mathbb R^n$ , the $x$ -projection sends the law $P$ of $\mathbf R$ to the law of the scalar $\mathbf r = x'\mathbf R$ , that is, to the pushforward of $P$ under $R \mapsto x'R$ . Write $\mu_x = x'\mu$ and $\sigma_x^2 = x'\Sigma x$ . The matrix $\Sigma$ is positive semidefinite, $\Sigma \succeq 0$ , when $x'\Sigma x \ge 0$ for all $x$ (and $\Sigma$ is symmetric); $\Sigma^{1/2}$ denotes its positive semidefinite square root.

Formalization targets

Goal: Theorem 1 (General Projection Property)

For every $\mu \in \mathbb R^n$ , every $\Sigma \succeq 0$ and every nonzero $x \in \mathbb R^n$ , the $x$ -projection maps $\mathbb M^n_{(\mu,\Sigma)}$ into and onto $\mathbb M_{(\mu_x,\sigma_x^2)}$ :

\bigl\{\, \text{law of } x'\mathbf R \;:\; \mathbf R \sim (\mu,\Sigma) \bigr\} \;=\; \mathbb M_{(x'\mu,\; x'\Sigma x)}.

The "into" half says every projected law has the right mean and variance. The "onto" half says that every univariate law with mean $\mu_x$ and variance $\sigma_x^2$ , however heavy-tailed or irregular, is the law of $x'\mathbf R$ for some $\mathbf R \sim (\mu,\Sigma)$ . The degenerate case $x'\Sigma x = 0$ is included.

Milestones

The into half (§2.1, justification of (4)): $x'\mathbf R$ has mean $x'\mu$ and variance $x'\Sigma x$ .
The degenerate case: if $x'\Sigma x = 0$ then $x'\mathbf R = x'\mu$ almost surely.
Standardization: if $\mathbf r \sim (m, v)$ with $v > 0$ , then $v^{-1/2}(\mathbf r - m) \sim (0,1)$ .
Normalization: for $x'\Sigma x > 0$ , the vector $y = (x'\Sigma x)^{-1/2}\Sigma^{1/2}x$ satisfies $y'y = 1$ .
Isotropic lift: if $y'y = 1$ and $\mathbf z \sim (0,1)$ , there is $\mathbf Z \sim (0, I_n)$ with $y'\mathbf Z$ distributed as $\mathbf z$ .
Affine image: if $\mathbf Z \sim (0,I_n)$ then $\mu + \Sigma^{1/2}\mathbf Z \sim (\mu,\Sigma)$ , and $x'(\mu + \Sigma^{1/2}Z) = x'\mu + (x'\Sigma x)^{1/2}\,y'Z$ for every $Z$ .

Significance

The result. Theorem 1 immediately yields Proposition 1 of the paper: for every objective $u$ ,

\min_{\mathbf R\sim(\mu,\Sigma)} E[u(x'\mathbf R)] = \min_{\mathbf r\sim(\mu_x,\sigma_x^2)} E[u(\mathbf r)],

with minima in the wide sense of infima. The robust objective is therefore a function of $(\mu_x, \sigma_x)$ alone, which makes every robust mean-covariance problem with a linear outcome a bicriteria mean-variance problem. The paper's later results use this: the two-point and one-point support properties, the parametric quadratic programming solution, and the portfolio applications (bonus schemes, value at risk). The projection property holds with no assumption on $u$ , so it serves non-concave, discontinuous and quantile-based objectives alike.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. The mission produces a formal definition of mean-covariance classes that treats integrability honestly, a proof of the projection property, and through it a formally verified reduction of multivariate moment-robust problems to univariate ones. The paper's own construction of the lifted vector has a gap (see Difficulty), so a formal proof also records a corrected argument.

Difficulty

The into half is a computation with linearity of expectation. The difficulty is entirely in the onto half. Given an arbitrary univariate law with prescribed mean and variance, one must build an $n$ -variate law with a prescribed full covariance matrix whose one-dimensional marginal in direction $x$ is exactly the given law. This is a coupling problem: the obvious approach, taking independent coordinates, fixes the marginal in direction $x$ as a convolution and cannot reproduce an arbitrary target. Taking $\mathbf R$ supported on the line through $\mu$ in a single direction reproduces the target law but has a rank-one covariance and fails whenever $\Sigma$ has rank above one.

The paper's appendix constructs the lift through conditional distributions of the remaining coordinates given the projected one. As printed, the conditional second-moment requirement it imposes cannot hold for unbounded targets, so that argument does not go through verbatim. The milestone for the lift states only the claim, not the printed construction.

The integrability bookkeeping is real work: every intermediate law must be shown to have finite second moments before its moments can be computed.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Borel σ-algebra; $x'R$ is the inner product $\langle x, R\rangle$ ; $x'\Sigma x$ is x.ofLp ⬝ᵥ S *ᵥ x.ofLp, where the matrix $\Sigma$ is named S (the symbol Σ is reserved in Lean).
Laws are probability measures. Both classes require finite second moments (MemLp … 2), so that means and covariances are genuine integrals, not the default value $0$ that Lean assigns to non-integrable functions. The univariate class is parametrized by the variance $v = \sigma^2$ , not by $\sigma$ .
The projection is the pushforward P.map (fun R => ⟪x, R⟫) under a continuous map. "Pathwise" identities in the paper become equalities of pushforward laws, or pointwise algebraic identities.
$\Sigma^{1/2}$ is CFC.sqrt S, acting through Matrix.toEuclideanCLM, as in Mathlib's multivariateGaussian.
The goal is stated as Set.MapsTo ∧ Set.SurjOn with both classes explicit. Its only hypotheses are $\Sigma \succeq 0$ and $x \ne 0$ , as in the paper. No bound on $n$ , no invertibility of $\Sigma$ and no positivity of $x'\Sigma x$ is assumed. Restricting the target to Gaussian, bounded or finitely supported laws, or dropping the finite-second-moment clause (which would admit Cauchy laws as "mean 0, variance 0"), would trivialize or change the theorem and is ruled out.
Milestones 3, 4 and 6 assume $x'\Sigma x > 0$ (or $v > 0$ ), the case the proof treats after its first sentence; milestone 2 covers the complementary case.

Needed infrastructure: moments of pushforwards under linear and affine maps, a covariance calculus for coordinates of random vectors, and a coupling that realizes the isotropic lift. Mathlib's multivariateGaussian, stdGaussian and CFC.sqrt are available. A reusable lemma "the covariance of $A\mathbf Z + b$ is $A\,\mathrm{Cov}(\mathbf Z)A'$ " would serve beyond this mission. Related platform work on moment-based ambiguity sets: Wasserstein Distributionally Robust Optimization II. Contributions of any milestone, and alternative proofs of the lift, are welcome.

Selected references

I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM Journal on Optimization 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903
H. Scarf, A Min-Max Solution of an Inventory Problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
W. W. Rogosinski, Moments of Non-Negative Mass, Proceedings of the Royal Society A 245:1–27, 1958. https://doi.org/10.1098/rspa.1958.0062

10 thms2 active usersReviewed

Optimization Probability Statistics+1·Captain: mikedeng1

Acceleration of Stochastic Approximation by Averaging: Almost-Sure Convergence and Asymptotic Normality of the Averaged IterateResearch Paper

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:

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.
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.
Assumption 3.3's $\delta(x_{t-1})$ is stated as $\delta(x_{t-1}-x^*)$ .
$\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.
$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.
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.
(A3) is stated with the norm inside, as its proof establishes.
(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

10 thms2 active usersReviewed

Completed

Convex Optimization Linear algebra Linear Optimization+1·Captain: mikedeng1

Path-Finding Methods for Linear Programming II: Properties of the Regularized D-Optimal-Design Weight FunctionResearch Paper

Motivation

Interior point methods for a linear program $\min\{c^\top x : Ax\ge b\}$ with $A\in\mathbb R^{m\times n}$ follow the central path of the logarithmic barrier $-\sum_i\log s_i$ , where $s=Ax-b$ is the slack vector. Renegar's path-following analysis (1988) gives $O(\sqrt m\,L)$ iterations, and for decades this was the best bound for methods whose iterations cost a linear system solve. Vaidya's volumetric barrier $-\log\det(A^\top S^{-2}A)$ and the hybrid volumetric barriers of Vaidya and of Anstreicher (references [45] and [2] of the paper) reached $O((m\,\mathrm{rank}(A))^{1/4}L)$ iterations at the price of more expensive linear algebra. Nesterov and Nemirovski showed that a universal barrier gives $O(\sqrt n\,L)$ iterations, but that barrier cannot be evaluated efficiently.

Lee and Sidford (FOCS 2014; full version arXiv:1312.6677) obtained $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ iterations, each costing $\tilde O(1)$ linear system solves, by following a weighted central path whose weights are recomputed from the slacks. The weights come from a weight function $g$ , defined as the minimizer of a regularized D-optimal-design problem. This mission is about that weight function and the theorem (Theorem 1 of the paper) certifying its properties. The companion mission, Path-Finding Methods for Linear Programming I, formalizes the path-following framework (Theorem 5 of §IV.C) that consumes these properties.

Setting

Fix $A\in\mathbb R^{m\times n}$ with full column rank, $\mathrm{rank}(A)=n$ , and $1\le n<m$ . For vectors $s,w\in\mathbb R^m_{>0}$ write $S=\mathrm{diag}(s)$ , $W=\mathrm{diag}(w)$ , $W^\alpha=\mathrm{diag}(w_i^\alpha)$ , and $A_s=S^{-1}A$ . For a matrix $M$ let $\|v\|_M=\sqrt{v^\top Mv}$ .

Projection matrix and slack sensitivity (Definition 2, p. 428). The projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A\,(A^\top S^{-1}WS^{-1}A)^{-1}A^\top S^{-1}W^{1/2}$ , and the slack sensitivity is

\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\mathbb 1_i\big\|_{P_{S^{-1}A}(w)} .

Weight function (Definition 4, p. 428). A map $g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ is a weight function with constants $c_1,c_\gamma,c_r$ if it is differentiable and, for every $s>0$ , with $G(s)=\mathrm{diag}(g(s))$ , $G'(s)$ the Jacobian of $g$ at $s$ , and $\|y\|_{G(s)}=\sqrt{\sum_ig_i(s)y_i^2}$ :

Size: $\|g(s)\|_1\le c_1$ ;
Slack sensitivity: $c_\gamma\ge1$ and $\gamma(s,g(s))\le c_\gamma$ ;
Step consistency: $c_r\ge1$ and for all $r\ge c_r$ , $y\in\mathbb R^m$ : $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ and $\|y+r^{-1}G^{-1}G'Sy\|_\infty\le\|y\|_\infty+c_r\|y\|_{G(s)}$ ;
Uniformity: $\|g(s)\|_\infty\le2$ .

The regularized objective (6), p. 429. For $\alpha,\beta\in\mathbb R$ ,

\hat f(s,w)=\mathbb 1^\top w-\frac1\alpha\log\det\big(A_s^\top W^\alpha A_s\big)-\beta\sum_{i\in[m]}\log w_i ,\qquad g(s)=\arg\min_{w\in\mathbb R^m_{>0}}\hat f(s,w).

At $\alpha=1,\beta=0$ this is the D-optimal design problem, dual to computing the John ellipsoid of the polytope $\{y:|[A(y-x)]_i|\le s_i\}$ (§V.B).

Formalization targets

Goal: Theorem 1 (Properties of Weight Function), §V.A, p. 429

With

\alpha=1-\Big(\log_2\frac{2m}{\mathrm{rank}(A)}\Big)^{-1},\qquad \beta=\frac{\mathrm{rank}(A)}{2m},

the objective $\hat f(s,\cdot)$ has a unique minimizer over $\mathbb R^m_{>0}$ for every $s>0$ , and the resulting $g$ is a weight function with

c_1(g)=2\,\mathrm{rank}(A),\qquad c_\gamma(g)=2,\qquad c_r(g)=2\log_2\frac{2m}{\mathrm{rank}(A)} .

Milestones: the three bullets of Theorem 1

Size: every minimizer $w$ of $\hat f(s,\cdot)$ satisfies $\|w\|_1\le2\,\mathrm{rank}(A)$ .
Slack sensitivity: every minimizer $w$ satisfies $\gamma(s,w)\le2$ .
Step consistency: any map $g$ selecting a minimizer at every $s>0$ is differentiable on $\mathbb R^m_{>0}$ and satisfies the two step-consistency inequalities for every $r\ge2\log_2\frac{2m}{\mathrm{rank}(A)}$ .

A supporting (non-milestone) item states the existence and uniqueness of the minimizer on its own.

Significance

The result. Theorem 1 is the input that turns the weighted path-following framework into an $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ -iteration method: the framework needs $O(c_\gamma^{-1}c_r^{-3}c_1^{-1/2})$ -sized steps in $t$ (p. 428), and Theorem 1 makes that $\tilde\Omega(1/\sqrt{\mathrm{rank}(A)})$ . The step consistency bound is what allows the weights to be recomputed after each Newton step without losing centrality. The same construction underlies later work on Lewis-weight barriers and on fast approximate John ellipsoids and maximum flow (§VIII of the paper).

Formalizing it. The theorem is proved in the full version of the paper (arXiv:1312.6677); the FOCS extended abstract contains no proofs. No part of it has a machine-checked proof. A complete formalization would give a verified account of leverage-score calculus (sums of leverage scores equal the rank; derivatives of projection matrices), of the convexity of $w\mapsto-\log\det(A^\top W^\alpha A)$ for $\alpha\in(0,1)$ , and of differentiability of an argmin via the implicit function theorem, none of which is currently packaged in Mathlib in this form.

Difficulty

Size and slack sensitivity are statements about the minimizer, which is only characterized implicitly; they require precise matrix calculus for $\log\det(A_s^\top W^\alpha A_s)$ and a comparison between the matrices $A^\top WA$ (which defines $\gamma$ ) and $A^\top W^\alpha A$ (which defines $g$ ). The specific values of $\alpha$ and $\beta$ matter here: the unregularized choice $\alpha=1$ , $\beta=0$ makes the problem degenerate (p. 429).

The hard part is step consistency. The Jacobian $G'$ of an argmin is available only implicitly, as the solution of a linear system obtained by differentiating the optimality condition. A bound on $\|G'\|$ that depends on $m$ is easy to get and useless: the theorem needs the operator norm of $I+r^{-1}G^{-1}G'S$ in the $G(s)$ -norm to be at most $1$ as soon as $r$ exceeds $2\log_2(2m/\mathrm{rank}(A))$ , and an $\ell_\infty$ bound with only an additive $c_r\|y\|_{G(s)}$ loss.

Existence and differentiability of the minimizer are conclusions, not hypotheses. The minimization is over an open orthant on which the objective is not obviously coercive or strictly convex for $\alpha<1$ , and differentiability of $g$ requires the Hessian of $\hat f$ at the minimizer to be invertible.

Formalization scope

Vectors are Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; inverses are Matrix.inv, $\log\det$ is Real.log (Matrix.det …), $w_i^\alpha$ is Real.rpow, $\log_2$ is Real.logb 2, the Jacobian is fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm on Fin m → ℝ.

Conventions and pinned hypotheses:

Full column rank A.rank = n is assumed in every theorem. The paper never states it, but without it $A_s^\top W^\alpha A_s$ is singular and every formula is undefined (in Lean, Matrix.inv and Real.log would return junk $0$ ).
$1\le n<m$ . $\beta=\mathrm{rank}(A)/(2m)$ and $\log_2(2m/\mathrm{rank}(A))$ need $\mathrm{rank}(A)\ge1$ ; at $m=\mathrm{rank}(A)$ the page's $\alpha$ is $0$ and $1/\alpha$ in (6) is undefined.
Reading of $\alpha$ : the exponent $-1$ is the reciprocal of $\log_2\frac{2m}{\mathrm{rank}(A)}$ , giving $\alpha\in(0,1)$ .
Size is an upper bound $\|g(s)\|_1\le c_1$ (the paper's weight function has $\|g(s)\|_1=\tfrac32\mathrm{rank}(A)$ , while Theorem 1 reports $c_1=2\,\mathrm{rank}(A)$ ).
The first step-consistency bullet (an operator-norm bound) is stated for every vector $y$ .
$g$ is any map $\mathbb R^m\to\mathbb R^m$ whose value at each positive $s$ minimizes $\hat f(s,\cdot)$ over $\mathbb R^m_{>0}$ . Only its values on the open orthant matter. The goal also asserts that such minimizers exist and are unique, so it is not vacuous.

Ruling out trivializations: the goal does not assume $g$ to be a weight function or to be differentiable, and it does not replace $g$ by an arbitrary weight function; differentiability is a conclusion (a predicate using fderiv without it would make step consistency hold vacuously wherever $g$ fails to be differentiable).

Useful infrastructure, reusable beyond this mission: leverage scores and their sum; derivatives of $w\mapsto\log\det(A^\top WA)$ and of projection matrices; convexity of $-\log\det(A^\top W^\alpha A)$ in $w$ (related to the published ConvexOptimization.log_det_concaveOn); differentiability of the argmin of a strictly convex smooth function. Contributions of these as separate theorems are welcome, as is a proof of any single bullet of Theorem 1.

Selected references

Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv, 2013. https://arxiv.org/abs/1312.6677
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40 (1988). https://doi.org/10.1007/BF01580724

7 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Optimization·Captain: mikedeng1

Path-Finding Methods for Linear Programming I: Centering with Weights on the Weighted Central PathResearch Paper

Motivation

Interior point methods solve a linear program by following a central path: a curve of minimizers of a penalized objective that trades off cost against distance from the boundary of the feasible region. The classical analysis of path following with the logarithmic barrier needs $O(\sqrt{m}\,L)$ iterations for a program with $m$ constraints, where $L$ is the bit complexity of the input (Renegar 1988). For programs with many more constraints than variables, $m$ can be far larger than the dimension $n$ or the rank of the constraint matrix, and the $\sqrt m$ factor is then the bottleneck.

Lee and Sidford (FOCS 2014) reduce the iteration count to $\tilde O(\sqrt{\mathrm{rank}(A)}\,L)$ by following a weighted central path in which each constraint carries its own positive weight, and the weights are re-computed as the algorithm moves. Their improved maximum-flow algorithm is an application of the same method.

Timeline. Karmarkar (1984) gave the first polynomial-time interior point method for linear programming. Renegar (1988) showed that path following with the logarithmic barrier needs $O(\sqrt m L)$ iterations. Nesterov and Nemirovskii (1994) showed that a universal self-concordant barrier yields $O(\sqrt n L)$ iterations, but that barrier is not known to be efficiently computable. Lee and Sidford (2014) achieved $\tilde O(\sqrt{\mathrm{rank}(A)}L)$ iterations, each reducible to $\tilde O(1)$ linear-system solves.

This mission covers the first half of that framework (§IV of the paper): the weighted central path, the weighted Newton step, and the centering theorem that shows a single step followed by re-weighting makes constant-factor progress.

Setting

Let $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , and consider the linear program

\min_{x\in\mathbb R^n:\ Ax\ge b} c^Tx .

The slack of a point $x$ is $s(x)=Ax-b$ , and the interior is $S^0=\{x : Ax>b\}$ , the points with all slacks strictly positive. For a path parameter $t$ and a vector of positive weights $w\in\mathbb R^m_{>0}$ , the weighted penalized objective is

f_t(x,w)=t\,c^Tx-\sum_{i=1}^m w_i\log s(x)_i .

A pair $(x,w)$ is feasible if $x\in S^0$ and $w>0$ .

Write $S_x=\mathrm{diag}(s(x))$ , $W=\mathrm{diag}(w)$ and $\|v\|_M=\sqrt{v^TMv}$ . The Newton step and the centrality are

\vec h_t(x,w)=\big(A^TS_x^{-1}WS_x^{-1}A\big)^{-1}\big(tc-A^TS_x^{-1}w\big),\qquad \delta_t(x,w)=\big\|\vec h_t(x,w)\big\|_{A^TS_x^{-1}WS_x^{-1}A}.

The matrix $A^TS_x^{-1}WS_x^{-1}A$ is the Hessian of $f_t$ in $x$ , and $tc-A^TS_x^{-1}w$ is its gradient; $\delta_t(x,w)=0$ exactly when $x$ minimizes $f_t(\cdot,w)$ .

For slacks $s$ and weights $w$ the projection matrix is $P_{S^{-1}A}(w)=W^{1/2}S^{-1}A(A^TS^{-1}WS^{-1}A)^{-1}A^TS^{-1}W^{1/2}$ and the slack sensitivity is

\gamma(s,w)=\max_{i\in[m]}\big\|W^{-1/2}\vec 1_i\big\|_{P_{S^{-1}A}(w)} .

A weight function (Definition 4) is a differentiable map $\vec g:\mathbb R^m_{>0}\to\mathbb R^m_{>0}$ from slacks to weights with constants $c_1$ (size, a bound on $\|\vec g(s)\|_1$ ), $c_\gamma\ge1$ (slack sensitivity, $\gamma(s,\vec g(s))\le c_\gamma$ ), $c_r\ge1$ (step consistency, two inequalities on the Jacobian $G'(s)$ of $\vec g$ that hold for every $r\ge c_r$ ), and uniformity $\|\vec g(s)\|_\infty\le2$ .

Formalization targets

Goal: Theorem 5 (Centering with Weights), §IV.C

Let $\vec g$ be a weight function for $A$ with constants $c_1,c_\gamma,c_r$ , let $x^{(old)}\in S^0$ , $s^{(old)}=s(x^{(old)})$ , and

x^{(new)}=x^{(old)}-\frac{1}{1+c_r}\,\vec h_t\big(x^{(old)},\vec g(s^{(old)})\big).

If $\delta_t(x^{(old)},\vec g(s^{(old)}))\le\frac{1}{100c_\gamma c_r^2}$ , then $x^{(new)}\in S^0$ and

\delta_t\big(x^{(new)},\vec g(s^{(new)})\big)\le\Big(1-\frac{1}{4c_r}\Big)\delta_t\big(x^{(old)},\vec g(s^{(old)})\big).

The theorem is stated for every weight function, not for the specific one constructed in §V of the paper; that construction is the subject of a separate mission.

Milestone: Lemma 3 (Split Newton Step), §IV.B

For feasible $(x^{(old)},w^{(old)})$ and $r\ge0$ , the split step $x^{(new)}=x^{(old)}-\frac1{1+r}\vec h_t$ , $w^{(new)}=w^{(old)}+\frac r{1+r}W_{(old)}S_{(old)}^{-1}A\vec h_t$ satisfies, whenever $\delta_t\le\frac1{8\gamma}$ ,

\delta_t\big(x^{(new)},w^{(new)}\big)\le\frac{2}{1+r}\,\gamma\,\delta_t^2,

with $\gamma=\gamma(s(x^{(old)}),w^{(old)})$ , and the new pair is feasible.

Milestone: Lemma 1, §IV.B

For feasible $(x,w)$ and $\alpha,t\ge0$ :

\delta_{(1+\alpha)t}(x,w)\le(1+\alpha)\delta_t(x,w)+\alpha\sqrt{\|w\|_1}.

Significance

Theorem 5 is the centering half of the weighted path-following method. Combined with Lemma 1, it shows that the path parameter can be doubled, while staying close to the weighted central path, in a number of steps of the form (5) controlled by $c_\gamma$ , $c_r$ and $\sqrt{c_1}$ . The paper then constructs (§V, Theorem 1) a weight function with $c_1=2\,\mathrm{rank}(A)$ , $c_\gamma=2$ and $c_r$ logarithmic in $m/\mathrm{rank}(A)$ , which yields the $\tilde O(\sqrt{\mathrm{rank}(A)})$ iteration bound. The theorem isolates exactly which properties of a weighting scheme are needed, so it applies to any weight function satisfying Definition 4.

The FOCS extended abstract states these results without proofs; the proofs are in the arXiv full version (arXiv:1312.6677). The results are proved on paper. No machine-checked formalization of weighted path following, or of the Lee–Sidford framework, is known. A formal proof would check the constants $\frac1{100}$ , $\frac1{4}$ , $\frac18$ and $\frac2{1+r}$ as stated in the extended abstract, and would produce reusable Lean infrastructure for Newton steps of barrier functions with explicit matrix formulas.

Difficulty

The standard analysis of Newton's method on a self-concordant barrier gives quadratic convergence of centrality for a fixed barrier. Here the barrier changes during the step: the weights are reset to $\vec g(s(x^{(new)}))$ , so the new centrality is measured with respect to a different Hessian and a different gradient. The obvious argument, analysing the step at fixed weights and then treating the re-weighting as a small perturbation, does not give a contraction factor independent of $m$ : without control of how $\vec g$ reacts to changes in the slacks, the re-weighting can undo the progress of the step. The step-consistency conditions of Definition 4 are the only hypotheses that control this reaction, and they are pointwise bounds on the Jacobian of $\vec g$ , while the step moves the slacks by a finite amount.

Formalization scope

Vectors are Fin n → ℝ and Fin m → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and products are Matrix.mulVec and dotProduct. $S^{-1}$ is the diagonal matrix of reciprocals, $W^{\pm1/2}$ the diagonal matrices of $\sqrt{w_i}^{\pm1}$ , and $\|v\|_M=\sqrt{v^TMv}$ . The Newton step and centrality are defined by the explicit formulas (3) and (4), not by derivatives of $f_t$ ; the centrality uses the Hessian-norm form of (4). The Jacobian $G'(s)$ is the Fréchet derivative fderiv ℝ g s, and $\|\cdot\|_\infty$ is Mathlib's sup norm.

Conventions fixed where the paper is silent:

Full column rank. Every theorem assumes A.rank = n. The paper uses $(A^TS_x^{-1}WS_x^{-1}A)^{-1}$ without comment; the inverse exists for positive slacks and weights exactly when $A$ has full column rank. Lean's matrix inverse is $0$ on singular matrices, which would make $\vec h_t$ , $\delta_t$ and $\gamma$ vanish and every statement trivially true; the rank hypothesis rules this trivializing reading out.
Size as an upper bound. Definition 4's " $c_1(\vec g)=\|\vec g(s)\|_1$ " is read as $\|\vec g(s)\|_1\le c_1$ for all $s>0$ (the paper's own weight function reports a $c_1$ above its $\ell_1$ norm). $c_1$ does not enter Theorem 5.
Operator norm. Step consistency's first bullet is written as $\|(I+r^{-1}G^{-1}G'S)y\|_{G(s)}\le\|y\|_{G(s)}$ for all $y$ .
Lemma 3's $r$ ranges over $r\ge0$ , and $\gamma(x,w)$ means $\gamma(s(x),w)$ .
Feasibility of the new point is part of the conclusion of Lemma 3 and Theorem 5, since the page's conclusion evaluates quantities defined only on the interior.
Maximum over $[m]$ is a supremum over Fin m (attained for $m\ge1$ , equal to $0$ for $m=0$ ).
The path parameter $t$ is unrestricted in Theorem 5 and Lemma 3, as on the page; Lemma 1 assumes $t\ge0$ as the page does.

A complete development needs basic facts about weighted norms and the projection matrix $P_{S^{-1}A}(w)$ , spectral comparison of the matrices $A^TS^{-1}WS^{-1}A$ for nearby slacks and weights, and calculus for vector-valued maps on the positive orthant. The weighted-norm and projection-matrix material is reusable for any interior point analysis. Proofs of the milestones, alternative arguments, and sharper constants are welcome.

Selected references

Y. T. Lee, A. Sidford, Path Finding Methods for Linear Programming: Solving Linear Programs in Õ(√rank) Iterations and Faster Algorithms for Maximum Flow, FOCS 2014, pp. 424–433. https://doi.org/10.1109/FOCS.2014.52
Y. T. Lee, A. Sidford, Path Finding I: Solving Linear Programs with Õ(√rank) Linear System Solves, arXiv:1312.6677, 2013. https://arxiv.org/abs/1312.6677
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Mathematical Programming 40, 1988, pp. 59–93. https://doi.org/10.1007/BF01580724
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 1984, pp. 373–395. https://doi.org/10.1007/BF02579150
Y. Nesterov, A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

6 thms2 active usersReviewed

Completed

Linear Optimization Optimization·Captain: mikedeng1

Critical-Path Planning and Scheduling II: The Project Cost Curve Is Non-Increasing, Piecewise Linear and ConvexResearch Paper

Motivation

A large engineering or construction project is a set of jobs with precedence constraints, and most jobs can be finished faster at a higher cost (overtime, more crews, faster equipment). Planners want to know, for every possible project duration, the cheapest way to meet it. The resulting trade-off between duration and direct cost is what management compares with overhead, penalties and market losses when it picks a schedule.

J. E. Kelley, Jr. and M. R. Walker introduced the critical-path method (CPM) in 1959, from work at du Pont and Remington Rand (Kelley and Walker 1959). Alongside the critical-path computation, they modelled each job's cost as a linear function of its duration and posed the choice of durations as a parametric linear program. They stated that its optimal value, as a function of the project duration $\lambda$ , is a non-increasing, piecewise linear, convex function, which they called the project cost curve. The 1959 paper gives no proof and defers the detailed development to a separate paper (Kelley 1961). Fulkerson (1961) gave a network-flow algorithm that computes the curve. Time–cost trade-off analysis ("crashing") has been a standard part of project management since then.

Setting

A project network has events labelled $0, 1, \dots, n$ with $n \ge 1$ . Event $0$ is the origin and event $n$ the terminus. A finite set $P$ of jobs is given, each an ordered pair $(i,j)$ : an arrow from event $i$ to event $j$ . As in the paper, labels increase along arrows ( $i < j$ for every $(i,j) \in P$ ), the origin precedes every event, and the terminus follows every event.

For job durations $y = (y_{ij})$ , the earliest event times are given by recursion (1):

t_0^{(0)} = 0,\qquad t_j^{(0)} = \max\,[\,y_{ij} + t_i^{(0)} \mid i<j,\ (i,j)\in P\,],\quad 1\le j\le n,

and $t_n^{(0)}(y)$ is the earliest project completion time.

Each job has a crash duration $d_{ij}$ and a normal duration $D_{ij}$ with $0 \le d_{ij} \le D_{ij}$ , and a linear job cost $a_{ij}y_{ij} + b_{ij}$ with $a_{ij} \le 0$ , $b_{ij} \ge 0$ . The project (direct) cost is

\text{(7)}\qquad \sum_{(i,j)\in P} (a_{ij} y_{ij} + b_{ij}).

A schedule for $\lambda$ is a pair $(y,t)$ with

\text{(5)}\ d_{ij}\le y_{ij}\le D_{ij},\qquad \text{(8)}\ y_{ij}\le t_j-t_i\quad ((i,j)\in P),\qquad \text{(9)}\ t_0=0,\ t_n=\lambda.

Let $\Lambda$ be the set of $\lambda$ for which a schedule exists. For $\lambda \in \Lambda$ the project cost curve $C(\lambda)$ is the minimum of (7) over schedules for $\lambda$ . Write $\lambda_c = t_n^{(0)}(d)$ (all jobs crashed) and $\lambda_N = t_n^{(0)}(D)$ (all jobs normal).

Formalization targets

Goal: the shape of the project cost curve (p. 165)

C \text{ is non-increasing on } \Lambda,\qquad C \text{ is piecewise linear on } \Lambda,\qquad C \text{ is convex on } \Lambda .

Piecewise linear means finitely many breakpoints $\beta_0<\dots<\beta_m$ with $\Lambda\subseteq[\beta_0,\infty)$ , and affine pieces on $\Lambda\cap[\beta_k,\beta_{k+1}]$ and on $\Lambda\cap[\beta_m,\infty)$ . The goal fixes no breakpoints or slopes. It asserts only the shape the paper claims, on the whole of $\Lambda$ .

Milestones

Feasible range (p. 165, "until no further reduction in project completion time is possible"): $\Lambda = [\lambda_c, \infty)$ .
Existence of optimal schedules (p. 165, the linear program (8), (9)): for every $\lambda\in\Lambda$ the minimum of (7) is attained.
All-normal solution (p. 165): $(D, t^{(0)}(D))$ is a minimum cost schedule for $\lambda = \lambda_N$ .
$\lambda$ is the earliest completion time (p. 165, "within the limits of most interest"): for $\lambda_c\le\lambda\le\lambda_N$ some minimum cost schedule $(y,t)$ for $\lambda$ has $t_n^{(0)}(y)=\lambda$ .

Significance

The cost curve is the output of CPM's cost analysis. Its convexity is what makes the paper's parametric procedure valid: jobs are expedited in order of increasing marginal cost, and the curve is traced from $\lambda_N$ down to $\lambda_c$ one linear piece at a time. Monotonicity justifies reading the curve as a trade-off. Piecewise linearity with finitely many pieces means the whole curve is determined by finitely many characteristic schedules, the vertices plotted in the paper's Fig. 3. The milestones identify the domain of the curve, show that it is well defined, and fix its right end at the all-normal solution.

These facts are classical: they follow from parametric linear programming, and Kelley (1961) and Fulkerson (1961) develop them in detail. No machine-checked proof of them is known. Prove2Me has a related result, LinearOptimization.lp_optimal_cost_convex_in_rhs (Bertsimas–Tsitsiklis, Theorem 5.1): convexity of the optimal cost of a standard-form LP in its right-hand side. It covers convexity only, for a different LP form, and says nothing about monotonicity or finitely many pieces. This mission adds a formal model of CPM's time–cost program and the full three-part shape theorem.

Difficulty

Convexity alone follows from the usual argument: a convex combination of optimal schedules for two durations is a schedule for the combined duration. Monotonicity needs the structure of the network: when $\lambda$ increases, only the constraints (8) on jobs ending at the terminus loosen, because no job leaves the terminus. The hard part is piecewise linearity with finitely many pieces. Convexity does not imply it, and a general result on value functions of linear programs has to be tied to this specific program, whose right-hand side depends on $\lambda$ only through $t_n = \lambda$ . The domain is also unbounded, so the argument must show that the curve is eventually a single affine (in fact constant) piece. It cannot just produce finitely many pieces on a compact interval.

Formalization scope

Events are Fin (n + 1) with origin 0 and terminus Fin.last n, and 1 ≤ n. Jobs are a Finset of ordered pairs, with at most one job per ordered pair. The standing assumptions of pp. 161–162 are fields of ProjectNetwork: labels increase along jobs, and reachability via Relation.ReflTransGen from the origin and to the terminus. Times and durations are real. Job data are functions Fin (n+1) → Fin (n+1) → ℝ, constrained and read only on $P$ . The hypotheses $0\le d_{ij}\le D_{ij}$ , $a_{ij}\le 0$ and $b_{ij}\ge 0$ are fields of JobData. Recursion (1) is earliest, defined by well-founded recursion on the label. It uses a fallback value $0$ for an event without predecessors, which occurs only at the origin. The paper's $\lambda$ is written lam. Constraint (9) fixes $t_n = \lambda$ exactly, and the event times are otherwise unconstrained.

The goal takes $C : \mathbb{R}\to\mathbb{R}$ with the hypothesis that $C(\lambda)$ is the least element of the set of costs of schedules for $\lambda$ , for every $\lambda \in \Lambda$ . All three conclusions are stated on $\Lambda$ only. This rules out the trivializing formalizations:

a junk-valued infimum off $\Lambda$ plays no role;
$C$ is tied to the program, and the hypothesis on $C$ is satisfiable by milestone 2;
piecewise linearity requires finitely many pieces that cover all of $\Lambda$ ;
all three properties are claimed, not convexity alone.

The goal keeps $a_{ij}\le 0$ , as the page does throughout §3, although monotonicity and convexity would hold without it.

Disclosed readings:

Milestone 1 renders "until no further reduction in project completion time is possible" as $\Lambda=[\lambda_c,\infty)$ .
Milestone 4 reads "within the limits of most interest" as $\lambda_c\le\lambda\le\lambda_N$ . It asserts that some optimal schedule has $t_n^{(0)}(y)=\lambda$ . "Every" is false: when all $a_{ij}=0$ , the all-crash durations are optimal for every $\lambda$ .

A complete development needs:

the existence of LP optima under a bounded objective, or a direct compactness argument on the feasible polyhedron;
a parametric-LP or polyhedral argument for finitely many linear pieces;
basic facts on the recursion (1).

The one-variable notion IsPiecewiseLinearOn and the facts on earliest event times can be reused in scheduling missions. Proofs of the milestones, of any of the three goal conjuncts separately, and general lemmas on parametric LP value functions are all welcome.

Not formalized: general piecewise linear convex job costs (deferred by the paper to its references [7], [8]), and the primal–dual procedure itself (a method, not a claim).

Selected references

J. E. Kelley, Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proc. Eastern Joint IRE-AIEE-ACM Computer Conference, 1959, pp. 160–173. https://doi.org/10.1145/1460299.1460318
J. E. Kelley, Jr., Critical-Path Planning and Scheduling: Mathematical Basis, Operations Research 9(3), 1961, pp. 296–320. https://doi.org/10.1287/opre.9.3.296
D. R. Fulkerson, A Network Flow Computation for Project Cost Curves, Management Science 7(2), 1961, pp. 167–178. https://doi.org/10.1287/mnsc.7.2.167
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §5.2 (the optimal cost as a function of the right-hand side).

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design·Captain: mikedeng1

Incentives in Teams: The Own Profit Incentive Structure Is an Optimal Incentive Structure for a ConglomerateResearch Paper

Motivation

An organization whose members hold private information faces two problems at once. The first is the team problem of Marschak and Radner: choose the rules by which members observe, communicate and decide so as to maximize the expected payoff of the organization as a whole (Marschak–Radner 1972). The second is the incentive problem: a member who is paid by their own results has no reason to follow those rules, and in particular no reason to report truthfully what they have observed. Theodore Groves' Incentives in Teams (Econometrica 41(4), 1973) connected the two. For a decentralized firm in which subunits report to a head, it exhibits compensation rules that make the team-optimal behaviour, truthful messages included, each subunit manager's unique best reply.

The construction is the origin of what is now called the Groves scheme, and with Vickrey's second-price auction (Vickrey 1961) and Clarke's pivot rule (Clarke 1971) it forms the Vickrey–Clarke–Groves (VCG) family of mechanisms.

Timeline:

1961, Vickrey: second-price auctions make truthful bidding a dominant strategy for a single object.
1971, Clarke: pivot payments for public-good decisions with deterministic valuations.
1972, Marschak–Radner: the economic theory of teams, with information and decision structures but a common payoff.
1973, Groves: compensation $C_i^{II}$ based on the head's conditional expectation of the other units' payoffs; Theorem 1 proves optimality in a conglomerate with independent component states and one round of communication.
1977, Green–Laffont: in the complete-information setting, Groves-type payments are the only ones that make truth-telling dominant (Econometrica 45(2)).
1979, d'Aspremont–Gérard-Varet: Bayesian incentive-compatible mechanisms with expected externality payments (J. Public Econ. 11(1)).

The conglomerate model

The organization consists of a head (component $0$ ) and finitely many subunits $i = 1, \dots, n$ . Each component $k$ has its own random component state $s_k \in S_k$ , and the components are independent: the state of the environment $s = (s_0, s_1, \dots, s_n)$ is distributed according to the product law $P(s) = P_0(s_0) \prod_{i} P_i(s_i)$ (Condition S.2).

Every member plays a strategy $\beta_k = (\zeta_k, \gamma_k, \delta_k)$ made of an observation strategy $\zeta_k$ on its own state, a message strategy $\gamma_k$ and a decision strategy $\delta_k$ (Condition S.3). Communication runs only between the head and each subunit, in one exchange: the head observes $\zeta_0(s_0)$ and sends $\gamma_0^i(\zeta_0(s_0))$ to subunit $i$ ; the subunit, with information $y_i(s) = [\zeta_i(s_i), \gamma_0^i(\zeta_0(s_0))]$ , sends back $\gamma_i(y_i(s))$ ; the head's information is $y_0(s) = [\zeta_0(s_0), \{\gamma_i(y_i(s))\}_{i}]$ (3.1). Decisions are $\delta_i(y_i(s))$ and $\delta_0(y_0(s))$ .

The organization payoff is a sum of components (Condition S.4),

\omega_0(\beta, s) = \sum_{i=1}^n v_i[\delta_i(y_i(s)), \delta_0(y_0(s)); s_i] + v_0[\delta_0(y_0(s)), s_0],

and $\bar\omega_0(\beta) = E[\omega_0(\beta, s)]$ . Each $v_i$ accrues directly to subunit $i$ (Condition S.5). Strategy sets $B_0, B_1, \dots, B_n$ are given; $\beta/\beta_i$ denotes $\beta$ with subunit $i$ 's strategy replaced by $\beta_i$ . Two strategies $\beta_i', \beta_i''$ are equivalent if $\bar\omega_0(\beta/\beta_i') = \bar\omega_0(\beta/\beta_i'')$ for every $\beta \in B$ .

Assumption A requires a $\beta^* \in B$ maximizing $\bar\omega_0$ over $B$ such that, for each subunit, $\bar\omega_0(\beta^*) > \bar\omega_0(\beta^*/\beta_i)$ whenever $\beta_i \in B_i$ is not equivalent to $\beta_i^*$ .

An incentive structure $W = \{\omega_i\}$ pays subunit $i$ the amount $\omega_i(\beta, s)$ . The class $\mathscr{J}$ (3.2) consists of those of the form $\omega_i = v_i[\dots] + C_i(y_0(s))$ : own payoff plus a compensation computed from the head's information only. $W$ is optimal (2.6) if $\beta_i^*$ maximizes $\bar\omega_i(\beta^*/\beta_i)$ over $B_i$ , uniquely up to equivalence.

Formalization targets

Goal: Theorem 1 (p. 625)

With $C_i^{II}(y_0) = \sum_{j \ne i} E\big[v_j[\delta_j^*(y_j^*(s)), \delta_0^*(y_0^*(s)); s_j] \,\big|\, y_0^*(s) = y_0\big] - A_i$ , the sum running over all components $j \in \{0, \dots, n\}$ other than $i$ and the expectation taken under $\beta^*$ (3.3), the structure $\omega_i^{II} = v_i[\dots] + C_i^{II}(y_0(s))$ lies in $\mathscr{J}$ and satisfies, for every subunit $i$ and every $\beta_i \in B_i$ ,

\bar\omega_i^{II}(\beta^*/\beta_i) \le \bar\omega_i^{II}(\beta^*), \qquad \text{with strict inequality if } \beta_i \not\equiv \beta_i^*.

It holds for every $\beta^*$ satisfying Assumption A, all strategy sets and all constants $A_i$ .

Milestones

The Appendix Lemma: the sets of states consistent with the head's information under $\beta^*/\beta_i$ and under $\beta^*$ have the same projections onto every component other than $i$ .
The right-hand side of (A.2): the head's conditional expectation factorizes over the independent components.
(A.2) for a subunit $j \ne i$ , and 4. (A.2) for the head's component $j = 0$ : the expected payoff of component $j$ under $\beta^*/\beta_i$ equals the expected value of its conditional expectation.
(A.1): $\bar\omega_i^{II}(\beta^*/\beta_i) + A_i = \bar\omega_0(\beta^*/\beta_i)$ for all $\beta_i \in B_i$ .

Significance

Theorem 1 shows that a head who knows only the messages it receives can nonetheless align every subunit's interest with the organization's, without monitoring decisions or observations. It is an early statement that expected-externality payments make truthful communication an equilibrium of a decentralized organization, and the Bayesian, team-theoretic counterpart of the dominant-strategy results of Vickrey and Clarke. Its structure (own payoff plus a transfer depending only on the others' reported information) is the template later characterized by Green and Laffont and generalized by d'Aspremont and Gérard-Varet.

Theorem 1 is proved in the paper; nothing here is open mathematically. What the mission adds is a machine-checked version with every modelling choice explicit: how information is generated by the message protocol, what the conditional expectation in (3.3) means on events of probability zero, and which equivalence "uniquely" refers to. No machine-checked proof of Theorem 1 is known to the platform. The platform's AGT.vcg_incentive_compatible treats the complete-information, direct-revelation analogue (deterministic valuations, dominant strategies), a different model with a different conclusion.

Difficulty

The tempting argument conditions on the head's information $y_0^*(s) = y_0$ under $\beta^*$ and compares it with the head's information under a deviation. That comparison fails when a deviating subunit sends a message that $\gamma_i^*$ never sends: the conditioning event then has probability zero under $\beta^*$ , and the conditional expectation of (3.3) is not determined by the joint law. A second obstacle is that the head's information under a deviation differs from the information under $\beta^*$ in every coordinate the deviation touches, while the compensation is computed as if $\beta^*$ were played; the statement to be proved compares expectations taken under two different joint strategies, and the one-exchange protocol makes the head's messages, and hence every subunit's information, depend on the head's own state. Treating these dependencies loosely either produces a circular definition of the information functions (as (3.1) is printed) or a statement that fails on events of probability zero.

Formalization scope

Every component state space $S_k$ is a finite type with weights that are nonnegative and sum to one; the joint law is the product of these weights and expectations are finite sums. The paper allows general probability spaces; the finite case covers the whole argument and gives conditional expectations at a point an elementary meaning.
Subunits form a finite index type; the head is a separate component with its own observation, message and decision types. Observation, message and decision spaces are fixed types per component.
Information (3.1) follows the single exchange of messages the paper describes in §4.A (p. 627): the head's message to subunit $i$ is a function of the head's observation. As printed, (3.1) is circular; this protocol is the paper's own resolution.
$C_i^{II}$ is used in factorized form: the head's term conditions only the head's state on the head's observation, and subunit $j$ 's term conditions only $s_j$ on the message $j$ sent. A separate milestone states that this equals the literal conditional expectation of (3.3) whenever the conditioning event has positive probability. The literal elementary quotient takes the value $0$ on null events, and with it Theorem 1 is false (one subunit that can send an unused message suffices); the factorized form is what the Appendix computes. The sum in (3.3) includes the head's component $v_0$ .
Equivalence of strategies is footnote 5's, over all $\beta \in B$ ; optimality includes the strict inequality for non-equivalent deviations. A formalization that replaces equivalence by equality of strategies, fixes $B_i = \{\beta_i^*\}$ , drops the strict inequality, or assumes (A.1) as a hypothesis is not this theorem.
The Lemma carries the added hypothesis that the set $B(s)$ is nonempty; the paper's proof presumes it and the statement is false without it.

Contributions welcome: proofs of the milestones, and reusable finite-probability facts (conditioning on product events, iterated expectation over a coordinate) stated for product weights.

Selected references

T. Groves, Incentives in Teams, Econometrica 41(4):617–631, 1973. https://doi.org/10.2307/1914085
J. Marschak and R. Radner, Economic Theory of Teams, Yale University Press, 1972.
W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16(1):8–37, 1961. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
E. H. Clarke, Multipart Pricing of Public Goods, Public Choice 11:17–33, 1971. https://doi.org/10.1007/BF01726210
J. Green and J.-J. Laffont, Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods, Econometrica 45(2):427–438, 1977. https://doi.org/10.2307/1911219
C. d'Aspremont and L.-A. Gérard-Varet, Incentives and Incomplete Information, Journal of Public Economics 11(1):25–45, 1979. https://doi.org/10.1016/0047-2727(79)90043-4

7 thms2 active usersReviewed

Completed

Graph Theory Linear Optimization Theoretical Computer Science·Captain: mikedeng1

Finding Minimum-Cost Circulations by Canceling Negative Cycles: Polynomial Termination of Minimum-Mean Cycle CancelingResearch Paper

Motivation

The minimum-cost circulation problem is a central problem of network optimization: transportation, assignment, shortest-path and maximum-flow problems are all special cases, and it is one of the few classes of linear programs with fast combinatorial algorithms. The oldest algorithm for it, the cycle-canceling algorithm of Klein (1967), repeatedly finds a residual cycle of negative cost and pushes as much flow as possible around it. With an arbitrary choice of cycle it can take exponentially many iterations even on integer data, and it need not terminate at all when capacities are irrational.

Goldberg and Tarjan (J. ACM 36(4), 1989) showed that one simple selection rule repairs this: always cancel a residual cycle whose mean cost (cost divided by number of arcs) is as small as possible. The resulting algorithm is strongly polynomial: its number of iterations is bounded by a polynomial in the number of vertices and arcs alone, independent of the magnitudes of capacities and costs. This mission formalizes that bound.

Timeline:

1967, Klein: the cycle-canceling algorithm, without an iteration bound.
1972, Edmonds and Karp: the first polynomial algorithm for minimum-cost flow (capacity scaling), polynomial in the bit length of the capacities.
1985, Tardos: the first strongly polynomial algorithm, introducing the arc-fixing idea that Theorem 3.8 generalizes.
1987–1989, Goldberg and Tarjan: generalized cost scaling and ε-optimality; in this paper, minimum-mean cycle canceling terminates after O(nm² log n) iterations for real costs (Theorem 3.9) and O(nm log(nC)) for integer costs bounded by C (Theorem 3.7).

Setting

A circulation network is a finite directed graph $G=(V,E)$ with $n=|V|$ vertices and $m=|E|$ arcs, which is symmetric ( $(v,w)\in E$ iff $(w,v)\in E$ , so $m$ counts both directions), together with real capacities $u(v,w)$ and real costs $c(v,w)$ , the cost being antisymmetric: $c(v,w)=-c(w,v)$ .

A circulation is a real function $f$ on arcs satisfying $f(v,w)\le u(v,w)$ , $f(v,w)=-f(w,v)$ on every arc, and conservation $\sum_{v:(w,v)\in E} f(v,w)=0$ at every vertex $w$ . Its cost is $\operatorname{cost}(f)=\tfrac12\sum_{(v,w)\in E}c(v,w)f(v,w)$ , and $f$ is minimum-cost (optimal) if no circulation has smaller cost.

The residual capacity of an arc is $u_f(v,w)=u(v,w)-f(v,w)$ ; arcs with $u_f>0$ are residual arcs. A residual cycle is a simple cycle of residual arcs; its capacity is the minimum residual capacity along it, its cost $c(\Gamma)$ is the sum of its arc costs, and its mean cost is $c(\Gamma)/|\Gamma|$ . Canceling a residual cycle raises the flow on each of its arcs by its capacity (and lowers the flow on each reverse arc by the same amount).

The minimum-mean cycle-canceling algorithm starts from any circulation and, while some residual cycle has negative cost, cancels a residual cycle whose mean cost is minimum among all residual cycles. Ties are broken arbitrarily, so the algorithm is a nondeterministic process; a run of length $K$ is any sequence $f_0,\dots,f_K$ of circulations produced by $K$ such iterations.

The analysis uses a price function $p:V\to\mathbb R$ , the reduced cost $c_p(v,w)=c(v,w)+p(v)-p(w)$ , and ε-optimality: for $\varepsilon\ge0$ , $f$ is ε-optimal if some $p$ gives $c_p(v,w)\ge-\varepsilon$ on every residual arc. The quantity $\varepsilon(f)$ is the least such $\varepsilon$ , and an arc is ε-fixed if all ε-optimal circulations carry the same flow on it.

Formalization targets

Goal: Theorem 3.9, with the proof's constant

For every circulation network with $n\ge2$ vertices, $m$ arcs, arbitrary real capacities and arbitrary real antisymmetric costs, every run of the minimum-mean cycle-canceling algorithm has length

K\ \le\ n\,m^2\,\lceil \ln n+1\rceil .

The statement quantifies over all starting circulations, all tie-breaking choices and all real data; it is the paper's $O(nm^2\log n)$ with the constant its proof establishes.

Milestones

In the order the proof uses them: Theorem 2.1 (optimal iff no negative residual cycle), Theorem 3.1 (optimal iff some price function has $c_p\ge0$ on residual arcs), Theorem 3.3 ( $\varepsilon(f)=-\mu(f)$ for nonoptimal $f$ , where $\mu(f)$ is the minimum cycle mean of the residual graph), Lemma 3.5 (a minimum-mean cancellation does not increase $\varepsilon(f)$ ), Lemma 3.6 ( $m$ cancellations shrink $\varepsilon(f)$ by a factor $1-1/n$ ), and Theorem 3.8 (an arc with $|c_p(v,w)|\ge2n\varepsilon$ is ε-fixed).

Significance

Theorem 3.9 shows that a classical, natural algorithm is strongly polynomial: its iteration count depends only on the combinatorial size of the network. Combined with Karp's $O(nm)$ minimum-mean cycle algorithm it yields an $O(n^2m^3\log n)$ strongly polynomial algorithm (Theorem 3.10), and its method, measuring progress by the minimum cycle mean and fixing arcs once $\varepsilon(f)$ is small, underlies the faster cancel-and-tighten algorithm of Section 4 and later strongly polynomial analyses of network-flow and related algorithms.

The theorem has been proved since 1989; this mission's contribution is a machine-checked proof. To the best of the platform's catalogue, no cycle-canceling bound, minimum cycle mean or ε-optimality statement has been formalized. The platform does hold the negative-cycle optimality criterion in a different model (LinearOptimization.network_no_negative_cycle_optimal, Bertsimas–Tsitsiklis Theorem 7.6, with nonnegative flows and supplies) and a flow decomposition theorem (LinearOptimization.network_flow_decomposition); both are related to milestones here but are stated for a different network model.

Difficulty

The obvious potential function, the cost of the circulation, decreases at every iteration but by amounts that depend on the data, so it yields no bound independent of the capacities and costs. The analysis instead has to track $\varepsilon(f)$ , an infimum over price functions, and relate it to the minimum cycle mean of a residual graph that changes after each cancellation, including arcs that appear only because of earlier cancellations. The strongly polynomial part needs a second ingredient: showing that the flow on some arc never changes again, which requires comparing the current circulation with all other ε-optimal circulations of the network, not only those the algorithm visits.

Formalization scope

Vertices form a finite type V; the arc set is E : Finset (V × V); capacities, costs and flows are real functions V → V → ℝ read only on E. $n$ is Fintype.card V and $m$ is E.card, counting $(v,w)$ and $(w,v)$ separately, as in the paper. Cycles are nonempty duplicate-free vertex lists, whose arcs are the cyclically consecutive pairs; one- and two-vertex cycles are allowed and have cost $0$ . Minimum mean is taken over all residual simple cycles of the current circulation. $\varepsilon(f)$ is an infimum (sInf) over a set that is nonempty and bounded below for every circulation; its attainment is to be proved, never assumed.

Explicit constants replacing the paper's $O(\cdot)$ :

Theorem 3.9: the paper prints $O(nm^2\log n)$ ; its proof uses groups of $k=m\,n\lceil\ln n+1\rceil$ iterations, at most $m$ of them, so the goal states $K\le n\,m^2\lceil\ln n+1\rceil$ with the natural logarithm.
The standing assumption $n\ge2$ (p. 874) is kept on the goal; the standing assumption $m\ge n$ is not used by the proof and is omitted.

"Terminates after at most $B$ iterations" means that every run has length at most $B$ . Asserting only that some run is short, or that the process eventually stops, does not formalize the theorem; nor does a step relation that drops negativity, simplicity of the cycle, minimality of the mean over all residual cycles, or the update by exactly the cycle's capacity.

A complete development needs cycle decomposition of the difference of two circulations, LP duality for circulations (Theorem 3.1), and bookkeeping for the residual graph under cancellation. These are reusable for any cycle-canceling or cost-scaling analysis, and contributions of that infrastructure as separate lemmas are welcome. Theorem 3.7 (the integer-cost bound) and Section 4 are outside this mission.

Selected references

A. V. Goldberg, R. E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, J. ACM 36(4):873–886, 1989. https://doi.org/10.1145/76359.76368
M. Klein, A primal method for minimal cost flows with applications to the assignment and transportation problems, Management Science 14(3):205–220, 1967. https://doi.org/10.1287/mnsc.14.3.205
É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5(3):247–255, 1985. https://doi.org/10.1007/BF02579369
A. V. Goldberg, R. E. Tarjan, Finding minimum-cost circulations by successive approximation, Mathematics of Operations Research 15(3):430–466, 1990. https://doi.org/10.1287/moor.15.3.430
R. M. Karp, A characterization of the minimum cycle mean in a digraph, Discrete Mathematics 23(3):309–311, 1978. https://doi.org/10.1016/0012-365X(78)90011-0
J. Edmonds, R. M. Karp, Theoretical improvements in algorithmic efficiency for network flow problems, J. ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699

10 thms2 active usersReviewed

Dynamic Programming Probability Stochastic Systems·Captain: mikedeng1

On the optimality equation for average cost Markov decision processes and its validity for inventory control: The Average-Cost Optimality Equation for Setup-Cost Inventory ControlResearch Paper

Motivation

Average-cost criteria are standard in inventory, queueing and maintenance models that run indefinitely. For a Markov decision process (MDP), the central object is the average-cost optimality equation (ACOE). It couples a constant $w$ (the optimal long-run cost per period) with a relative value function $\tilde u$ . A stationary policy that attains the minimum in the ACOE is average-cost optimal. When the state space is uncountable, the one-step cost is unbounded and the transition probability is only weakly continuous, the ACOE is not automatically available.

Feinberg, Kasyanov and Zadoianchuk (2012) proved that under their Assumptions W* and B the weaker average-cost optimality inequality (ACOI) holds. For setwise continuous transition probabilities, Hernández-Lerma and Lasserre (1996, Theorem 5.5.4) gave conditions for the ACOE via equicontinuity. Feinberg and Lewis (2015) established the ACOI and optimality of $(s,S)$ policies for periodic-review inventory control with setup costs and general demand. Feinberg and Liang (2022, online 2017) extended the equicontinuity condition to weakly continuous transitions and used it to show that the inventory problem satisfies the full equation, not just the inequality.

Setting

An MDP has a state space $\mathbb X$ and an action space $\mathbb A$ (Borel subsets of Polish spaces). It has a one-step cost $c:\mathbb X\times\mathbb A\to\mathbb R\cup\{+\infty\}$ , bounded below, and a transition probability $q(dy\mid x,a)$ . A policy chooses actions from the observed history, possibly at random. A stationary policy is a measurable map $\phi:\mathbb X\to\mathbb A$ . For a discount factor $\alpha\in[0,1)$ :

$v_\alpha(x)$ is the infimum over all policies of the expected total discounted cost from $x$ ;
$m_\alpha=\inf_x v_\alpha(x)$ ;
$u_\alpha=v_\alpha-m_\alpha$ is the discounted relative value function.

The average cost of a policy is $w^\pi(x)=\limsup_N \frac1N\mathbb E^\pi_x\sum_{t<N}c(x_t,a_t)$ , and $w(x)=\inf_\pi w^\pi(x)$ . Set $\underline w=\liminf_{\alpha\uparrow1}(1-\alpha)m_\alpha$ . For a sequence $\alpha_n\uparrow1$ , define

\tilde u(x)=\liminf_{n\to\infty,\ y\to x}u_{\alpha_n}(y).

Assumption EC for $\{\alpha_n\}$ has two parts:

the family $\{u_{\alpha_n}\}$ is equicontinuous;
some measurable $U\ge u_{\alpha_n}$ has $\int U\,dq(\cdot\mid x,a)<\infty$ for all $x,a$ .

The inventory problem has inventory level $x\in\mathbb R$ (negative means backlog) and order quantity $a\ge0$ . Inventory evolves by $x_{t+1}=x_t+a_t-D_{t+1}$ , with i.i.d. nonnegative demands $D$ . The cost is

c(x,a)=K\,I_{\{a>0\}}+\bar c\,a+\mathbb E[h(x+a-D)],

with setup cost $K\ge0$ , unit cost $\bar c>0$ , and convex $h$ with $h(x)\to\infty$ as $|x|\to\infty$ . Let $\alpha^*=1+\lim_{x\to-\infty}h(x)/(\bar cx)$ and $H(x)=\bar cx+\mathbb E[h(x-D)]+\mathbb E[\tilde u(x-D)]$ . A function $f$ is $K$ -convex if $f((1-\lambda)x+\lambda y)\le(1-\lambda)f(x)+\lambda f(y)+\lambda K$ for $x\le y$ and $\lambda\in(0,1)$ . An $(s,S)$ policy orders up to $S$ whenever the inventory is below $s$ .

Formalization targets

Goal: Theorem 4.5

For every sequence of nonnegative discount factors $\alpha_n\uparrow1$ with $\alpha_1>\alpha^*$ , the inventory MDP satisfies Assumption EC. Along a subsequence, $u_{\alpha_{n_k}}\to\tilde u$ , and some stationary $\phi$ satisfies

w+\tilde u(x)=K I_{\{\phi(x)>0\}}+H(x+\phi(x))-\bar cx=\min\Big\{\min_{a\ge0}[K+H(x+a)],\,H(x)\Big\}-\bar cx .

Moreover:

$\tilde u$ and $H$ are $K$ -convex, continuous and inf-compact;
the $(s,S)$ policy built from a minimizer of $H$ satisfies the equation;
so do the limits $(s^*,S^*)$ of discount-optimal thresholds.

Milestones

Lemma 3.3: for equicontinuous families, the pointwise and joint lower limits coincide.
Theorem 3.2: Assumptions W*, B and EC imply the ACOE for a general MDP.
The cited facts used in §4:
- Assumptions W* and B hold for the inventory problem;
- the sets $\mathbb X_\alpha$ of minimizers of $v_\alpha$ lie in a bounded interval (4.4);
- discount-optimal $(s_\alpha,S_\alpha)$ policies (Theorem 4.3);
- their average-cost limits (Theorem 4.4);
- the renewal bounds (4.11)–(4.12).
Lemma 4.6: an explicit dominating function $U$ .
Lemma 4.7: equicontinuity of $\{u_{\alpha_n}\}$ for the inventory problem.

Significance

The ACOE is stronger than the ACOI. It identifies the optimal actions of an average-cost problem as the minimizers of a one-step lookahead with $\tilde u$ , and it makes $\tilde u$ a genuine relative value function: $\tilde u$ is the pointwise limit of the discounted relative values along a subsequence. For inventory control, Theorem 4.5 gives three further conclusions:

the $K$ -convexity and continuity of the average-cost relative value function;
that an optimal $(s,S)$ policy can be computed from $H$ by the same argmin rule that works for discounted costs;
that limits of discount-optimal thresholds solve the average-cost problem.

The results are proved in the paper, and in the cited works of Feinberg and coauthors for the cited milestones. None is formalized. There is no formal library of MDPs on Borel spaces with history-dependent randomized policies. This mission builds that layer (strategic measures via Ionescu Tulcea, discounted and average costs, Assumptions W*, B and EC) and states the general ACOE theorem on it. A proof of the goal would also require formal proofs of the cited inventory results of Feinberg–Lewis (2015) and Feinberg–Liang (2017a), which are milestones here.

Difficulty

One obvious route is to pass to the limit in the discounted optimality equation $v_\alpha=\min_a[c+\alpha\int v_\alpha\,dq]$ . After subtracting $m_\alpha$ , this needs two things: convergence of $u_{\alpha_n}$ , and exchanging limit and integral. Pointwise lower limits give only the inequality (ACOI). The reverse inequality needs actual convergence of a subsequence and a dominating function. For weakly continuous $q$ , convergence of $\int u_{\alpha_n}\,dq$ additionally requires uniform convergence on compacts, which is where equicontinuity enters.

For the inventory problem the hard step is equicontinuity itself. The functions $u_\alpha$ are not uniformly Lipschitz. It must be shown that costs from two nearby starting inventories stay close uniformly in $\alpha$ . This comparison runs through the time until inventory falls below the reorder point, and it is controlled by renewal-theoretic bounds on the number of demand arrivals.

Formalization scope

The Lean development lives in the namespace FeinbergLiang.ACOE. It commits to the following conventions.

Spaces. $\mathbb X,\mathbb A$ are separable metric spaces with standard Borel σ-algebras. This is the paper's "Borel subsets of Polish spaces", up to homeomorphism. The inventory case is $\mathbb X=\mathbb R$ , $\mathbb A=\mathbb R_{\ge0}$ . The integer case $\mathbb X=\mathbb Z$ , $\mathbb A=\mathbb N_0$ is out of scope, as are Corollary 4.8 and Theorem 4.9.
Costs and infinities. The cost is stored as a real lower bound plus a $[0,\infty]$ -valued part. Every value function ( $v_\alpha$ , $m_\alpha$ , $u_\alpha$ , $w$ , $\underline w$ , $\tilde u$ ) is the $[0,\infty]$ -valued part, with the explicit real shift described in the definitions. $u_\alpha$ equals $v_\alpha-m_\alpha$ whenever $m_\alpha<\infty$ , which Assumption B guarantees. $\alpha^*$ is an extended real and may be $-\infty$ . $G_\alpha$ and $H$ are extended-real valued, and each theorem using them concludes their finiteness. Likewise the ACOE conclusions include $\underline w<\infty$ and $\tilde u<\infty$ , so an equation of the form $\infty=\infty$ can never satisfy them.
Policies. $v_\alpha$ and $w$ are infima over all history-dependent randomized policies, with trajectory laws given by Mathlib's Ionescu Tulcea kernel Kernel.trajMeasure. They are never defined as solutions of an optimality equation.
Readings of informal words.
1. " $\alpha_n\uparrow1$ " means values in $[0,1)$ , nondecreasing, with limit $1$ ; "nonnegative discount factors" is the lower end of $[0,1)$ .
2. The paper's $\alpha_1$ is Lean's α 0.
3. "Equicontinuous" is Mathlib's Equicontinuous, applied to the real values of $u_{\alpha_n}$ together with their finiteness.
4. " $\liminf_{n\to\infty,y\to x}$ " is the lower limit along the product filter atTop ×ˢ 𝓝 x.
5. "Uniform on each compact subset" is TendstoUniformlyOn on every compact set.
6. " $=\min$ " in (3.3) and (4.10) means the middle term is attained and is a lower bound for all actions.
7. "Assumption EC for the sequence" is a property of a given sequence.
8. "Can be selected as an $(s^*,S^*)$ policy" is stated for every limit of discount-optimal thresholds along a further subsequence, with $\tilde u$ that of Theorem 3.2(i).
9. "Can be selected as an $(s,S)$ policy" is stated for every minimizer $S$ of $H$ .
10. Theorem 4.4's "optimality inequality (4.8)" is read as the ACOI (3.1) for the $(s^*,S^*)$ policy.
Standing assumptions. The paper's "without loss of generality $h\ge0$ and $h(0)=0$ " is a pair of hypotheses of the inventory model. This is the paper's normalization, not an addition.
Not trivializable. Defining $v_\alpha$ through its optimality equation, restricting policies to stationary ones, or dropping the finiteness conclusions would make the goal a different, weaker statement. The definitions rule each of these out.

Contributions welcome: proofs of the milestones, especially the general Theorem 3.2 and the renewal estimates behind Lemmas 4.6–4.7. The Borel-space MDP definitions are reusable by later average-cost and discounted MDP missions.

Selected references

E. A. Feinberg and Y. Liang, On the optimality equation for average cost Markov decision processes and its validity for inventory control, Annals of Operations Research 317 (2022) 569–586. https://doi.org/10.1007/s10479-017-2561-9
E. A. Feinberg, P. O. Kasyanov and N. V. Zadoianchuk, Average cost Markov decision processes with weakly continuous transition probability, Mathematics of Operations Research 37(4) (2012) 591–607. https://doi.org/10.1287/moor.1120.0555
E. A. Feinberg and M. E. Lewis, On the convergence of optimal actions for Markov decision processes and the optimality of (s, S) policies for inventory control, preprint arXiv:1507.05125, 2015. https://arxiv.org/abs/1507.05125
E. A. Feinberg and Y. Liang, Structure of optimal policies to periodic-review inventory models with convex costs and backorders for all values of discount factors, Annals of Operations Research (2017a). https://doi.org/10.1007/s10479-017-2548-6
O. Hernández-Lerma and J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0

12 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Probability·Captain: mikedeng1

Stochastic Linear Optimization under Bandit Feedback 2: A Regret Lower Bound on the CircleResearch Paper

Motivation

In stochastic linear optimization under bandit feedback a learner repeatedly chooses a point $x_t$ from a compact decision set $D\subset\mathbb R^n$ and observes only the random cost $\ell_t$ of that point, whose mean is $\mu\cdot x_t$ for an unknown vector $\mu$ . The problem models online routing, ad placement and other sequential decisions with linearly structured costs. The quality of a learner is measured by its regret against the best fixed decision.

For the $K$ -armed bandit the achievable regret for a fixed instance is logarithmic in the horizon $T$ (Lai and Robbins 1985; Auer, Cesa-Bianchi and Fischer 2002). Dani, Hayes and Kakade (COLT 2008) showed that for linear costs the picture depends on the geometry of $D$ . Their Theorem 1 gives polylogarithmic regret when the decision set has a positive gap between the best and second-best extreme point (a polytope, for instance), and their Theorem 2 gives $O^*(n\sqrt T)$ regret for every decision set. Their Theorem 3 shows that the second rate cannot be improved in general: on a decision set with zero gap, every algorithm pays $\Omega(\sqrt T)$ in expectation.

Timeline:

2002: Auer, Using confidence bounds for exploitation–exploration trade-offs (JMLR 3), introduces confidence-bound algorithms for linear bandits on finite decision sets.
2008: Dani, Hayes and Kakade prove the $O^*(n\sqrt T)$ upper bound for ConfidenceBall₂ and the $\Omega(\sqrt T)$ lower bound on a product of circles, the subject of this mission. A hypercube lower bound for the adversarial setting appears in their NIPS 2007 paper.
2010: Rusmevichientong and Tsitsiklis, Linearly parameterized bandits (Math. OR 35), give $\Omega(n\sqrt T)$ lower bounds on the unit sphere.
2020: Lattimore and Szepesvári, Bandit Algorithms, Theorems 24.1 and 24.2, give minimax lower bounds on the hypercube and the unit ball with Gaussian noise.

Setting

The decision set is the unit circle $D_2=S^1=\{x\in\mathbb R^2: x_1^2+x_2^2=1\}$ . An unknown mean vector $\mu\in\mathbb R^2$ is drawn once, uniformly from the circle $D_2/2$ of radius $1/2$ ; concretely $\mu=\mu(\theta)=\tfrac12(\cos\theta,\sin\theta)$ with $\theta$ uniform on $[0,2\pi)$ .

On each round $t=1,\dots,T$ the algorithm plays $x_t\in D_2$ and observes a cost $\ell_t\in\{-1,+1\}$ with $\Pr(\ell_t=+1)=(1+\mu\cdot x_t)/2$ , so that $\mathbb E[\ell_t]=\mu\cdot x_t$ . Given the decision, the cost is independent of the past.

An algorithm may be randomised. It draws a seed $s$ once from a probability measure $\rho$ on a measurable space $S$ , and chooses $x_t$ as a function of $s$ and the costs $\ell_1,\dots,\ell_{t-1}$ observed so far, measurably in $s$ .

The regret over $T$ rounds is

R=\sum_{t=1}^T(\mu\cdot x_t-\mu\cdot x^*),\qquad \mu\cdot x^*=\min_{x\in D_2}\mu\cdot x,

so each round costs $r_t=\mu\cdot x_t+\tfrac12\ge0$ when $\|\mu\|=1/2$ . The expected regret $\mathbb E R=\mathbb E_\mu\,\mathbb E(R\mid\mu)$ averages over the seed, the prior and the costs.

In the Lean development these objects are unitCircle, meanVec, optCost, RandomizedPolicy and expectedRegret in the namespace StochLinOpt.LowerBound.

Formalization targets

Goal: Theorem 3 for $n=2$

There is a universal constant $c>0$ such that for every randomised algorithm and every $T\ge1$ ,

\mathbb E R\ \ge\ c\sqrt T.

The constant is left existential, which is the form that survives any later improvement of the constant; it is chosen before the algorithm and before $T$ .

Milestones

Section 6.1, Eq. (3). For $\|\mu_1\|=\|\mu_2\|=1/2$ , $x\in S^1$ , a posterior probability $p\in[0,1]$ of $\mu=\mu_1$ and a cost $\ell\in\{\pm1\}$ , the Bayes-updated bias $b_{t+1}$ satisfies $|b_{t+1}-b_t|\le|(\mu_1-\mu_2)\cdot x|$ , where $b_t=2p-1$ .
Lemma 15. With $\varepsilon=\|\mu_1-\mu_2\|>0$ and the same data,

\mathbb E_\mu(r_t\mid\mathcal H_t)\ge\frac1{16}\Big(\varepsilon^2+\frac{|b_{t+1}-b_t|^2}{\varepsilon^2}\Big)\mathbf 1\{|b_t|\le1/2\}.

Theorem 4 (Freedman). For a martingale difference sequence $X_1,\dots,X_T$ bounded above by $b$ , with conditional variance sum $V$ , and all $a,v>0$ ,

\Pr\Big(\sum_i X_i\ge a,\ V\le v\Big)\le\exp\Big(\frac{-a^2}{2v+2ab/3}\Big).

Significance

The lower bound shows that the $\sqrt T$ dependence of the problem-independent upper bound (Theorem 2 of the same paper) is necessary. It also shows that the gap-dependent polylogarithmic rate of Theorem 1 cannot extend to decision sets without a gap, such as the sphere. Together with the upper bound it characterises the minimax regret of stochastic linear bandits in $T$ up to logarithmic factors, and in the paper's general- $n$ form it also underlies the claim that the price of bandit information is $\Theta^*(\sqrt n)$ .

The result is proved in the paper for $n=2$ and has not been machine-checked. The mission produces a checked Bayesian lower bound over all randomised algorithms, with an explicit probability model for the protocol. Two related platform results are different theorems: BanditAlgorithm.linear_bandit_unit_ball_minimax_lower_bound (Lattimore–Szepesvári Theorem 24.2: unit ball, Gaussian noise, a worst-case $\mu$ ) and BanditAlgorithm.linear_bandit_hypercube_minimax_lower_bound (Theorem 24.1: hypercube). The $\{-1,+1\}$ costs, the circle and the uniform prior used here are not covered by either.

Difficulty

The obvious attempt is a two-point change-of-measure argument with a fixed pair of means at distance $\varepsilon$ . It fails as stated because the decision set has no gap: an algorithm that plays close to the optimum of both candidates learns slowly but also pays little. The per-round trade-off between regret and information (Lemma 15) is exact only while the posterior is undecided, $|b_t|\le1/2$ . Turning it into a bound on the whole horizon requires controlling how long the posterior stays undecided, which is a statement about a martingale whose step sizes are chosen by the algorithm; a concentration bound that ignores the accumulated conditional variance (Azuma–Hoeffding with worst-case steps) is too weak for this. The averaging step from a two-point prior to the uniform prior on the circle is also part of the formal work.

Formalization scope

Vectors are Fin 2 → ℝ with the dot product ⬝ᵥ; Euclidean norms are written through dot products, never with Lean's sup norm. Rounds are 0-indexed internally: the Lean index $t$ is the paper's round $t+1$ . The expected regret is the exact finite expectation

\mathbb E R=\int_S\frac1{2\pi}\int_0^{2\pi}\sum_{\ell\in\{\pm1\}^T}\prod_{t=1}^T\frac{1+\ell_t\,\mu(\theta)\cdot x_t}{2}\;R\;d\theta\,d\rho(s),

so no infinite product of measures is needed. A randomised algorithm is a seeded policy, which covers every randomised algorithm. The optimal cost is the infimum of $\mu\cdot x$ over the compact circle and is attained. Every junk value in the model (a non-integrable integrand) could only make the lower bound harder to prove, never easier.

A statement over deterministic algorithms only, over a worst-case $\mu$ instead of the uniform prior, or with the constant allowed to depend on the algorithm or on $T$ would be a weaker theorem. The goal quantifies $\exists c>0$ before the algorithm and $T$ , and fixes the prior.

Corrections relative to the printed paper:

General $n$ is not stated. Theorem 3 as printed claims $\mathbb E R\ge\frac1{10}n\sqrt T$ for every even $n$ . It is false for $n>10$ : on $D_n$ with $\mu\in D_n/n$ each round has regret at most $1$ , so at $T=1$ the claim would need $\mathbb E R\ge n/10>1$ . The general case rests on Lemma 16, which has no proof. The goal is the $n=2$ case, which Section 6.1 proves.
The constant. For $n=2$ the paper prints $\frac15\sqrt T$ ; its proof gives $c=\frac1{16}\min(\frac12-\frac1e,\frac1{64})=\frac1{1024}$ . The proof's Freedman step prints $2\exp(-\frac{1/4}{1/8+\varepsilon/3})\le 2/e^2$ ; with $v=1/32$ the denominator is $1/16+\varepsilon/3$ , and the bound $2/e^2$ then needs $\varepsilon=T^{-1/4}\le3/16$ . Small $T$ is covered by the first round, whose expected regret is $1/2$ . The goal leaves $c$ existential.
Theorem 4. The printed variance sum runs to $n$ ; it runs to $T$ . The conditioning is on a general filtration, and square-integrability of the steps is assumed so that the conditional variance is defined.
Lemma 15. Its right side depends on the round- $t$ cost $\ell_t$ , which is not part of $\mathcal H_t$ ; the Lean statement holds for either value of $\ell_t$ .

Welcome contributions: a Lean proof of Freedman's inequality (reusable across the bandit and concentration missions on the platform); the averaging argument from two-point priors to the uniform prior; and the stopped-martingale bookkeeping for the bias sequence.

Selected references

Varsha Dani, Thomas P. Hayes, Sham M. Kakade, Stochastic Linear Optimization under Bandit Feedback, Proceedings of the 21st Annual Conference on Learning Theory (COLT), 2008.
David A. Freedman, On tail probabilities for martingales, The Annals of Probability 3(1):100–118, 1975. https://doi.org/10.1214/aop/1176996452
Colin McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998. https://doi.org/10.1007/978-3-662-12788-9_6
Peter Auer, Using confidence bounds for exploitation–exploration trade-offs, JMLR 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
Paat Rusmevichientong, John N. Tsitsiklis, Linearly parameterized bandits, Mathematics of Operations Research 35(2):395–411, 2010. https://doi.org/10.1287/moor.1100.0446
Tor Lattimore, Csaba Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 24. https://doi.org/10.1017/9781108571401

5 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

On Certain Polytopes Associated with Graphs IV: Adjacent Stable Sets on the Stable Set PolytopeResearch Paper

Motivation

Many combinatorial optimization problems are linear programs over a polytope whose vertices are the zero–one incidence vectors of the feasible objects: matchings, stable sets, spanning trees. The edges of such a polytope (pairs of vertices joined by a one-dimensional face) govern the behaviour of the simplex method and of local-search procedures, which move from vertex to vertex along edges: a pivot of the simplex method on a nondegenerate basis replaces a vertex by one of its neighbours.

In December 1971 M. L. Balinski asked when two matchings $M_1, M_2$ of a graph are neighbours on the matching polyhedron determined by Edmonds (Edmonds 1965). V. Chvátal answered a more general question in §6 of On certain polytopes associated with graphs (Chvátal 1975): he characterized the neighbours on the stable set polytope of an arbitrary graph. Since matchings of $G$ are the stable sets of the line graph $L(G)$ , Balinski's question is the special case of line graphs (Corollary 6.3 of the paper).

Setting

Let $G=(V,E)$ be a finite undirected loopless graph. A stable set is a set of vertices no two of which are adjacent. $S(G)$ denotes the set of all zero–one vectors $x=(x_u : u\in V)$ such that $\{u : x_u=1\}$ is stable, and the stable set polytope is

P(G)=\operatorname{conv} S(G)\subseteq \mathbb R^V .

For $y\in S(G)$ the corresponding stable set is $Y=\{u : y_u=1\}$ .

For an integer-valued vector $c=(c_u : u\in V)$ write $cx=\sum_{u\in V}c_ux_u$ . Two vectors $y, z$ are neighbours in $P(G)$ if there is an integer-valued $c$ such that $y$ and $z$ are the only two vectors which maximize $cx$ over $S(G)$ ; in particular $y\neq z$ . This is the definition the paper states at the start of the proof of Theorem 6.2.

A bicoloration of a graph $T$ is a partition $V=B\cup R$ , $B\cap R=\emptyset$ , such that every edge joins $B$ to $R$ . Every tree has one.

In the Lean development these objects are stableVectors G ( $S(G)$ ), stablePolytope G ( $P(G)$ ), onesSet y ( $Y$ ), AreNeighbors G y z and IsBicoloration T B R, all in the namespace ChvatalPolytopes.Neighbors.

Formalization targets

Goal: Theorem 6.2 (p. 149)

For $y,z\in S(G)$ with corresponding stable sets $Y,Z$ ,

y \text{ and } z \text{ are neighbours in } P(G) \iff \text{the subgraph } H \text{ of } G \text{ induced by } (Y-Z)\cup(Z-Y) \text{ is connected.}

Milestone: Lemma 6.1 (p. 149)

For a tree $T=(V,E)$ with a bicoloration $V=B\cup R$ there are nonnegative integers $c_u$ ( $u\in V$ ) and $m$ with

\sum_{u\in V}c_ux_u\le m\quad\text{for all } x\in S(T),

with equality exactly when $x$ is the incidence vector of $B$ or of $R$ .

Milestone: the certificate of the "if" part (p. 149, proof of Theorem 6.2, (i))

If $H$ is connected with spanning tree $T$ , and $c_u$ ( $u\in (Y-Z)\cup(Z-Y)$ ), $m$ are as in Lemma 6.1 for $T$ , extend $c$ by $c_u=1$ on $Y\cap Z$ and $c_u=-1$ outside $Y\cup Z$ . Then

\sum_{u\in V}c_ux_u\le m+|Y\cap Z|\quad\text{for all } x\in S(G),

with equality if and only if $x=y$ or $x=z$ .

Significance

Theorem 6.2 describes the 1-skeleton of the stable set polytope of every graph by a condition that can be checked in linear time, although optimizing over $P(G)$ is NP-hard in general and no complete linear description of $P(G)$ is known for general graphs. Through line graphs it gives the adjacency criterion for the matching polytope (two matchings are neighbours if and only if their symmetric difference is a single path or cycle), which settled Balinski's question. Characterizations of this type underlie the analysis of simplex-type and pivoting algorithms on combinatorial polytopes and the study of their diameters.

The result has been proved since 1975. The mission asks for a machine-checked proof of the theorem as stated in the paper; no formal proof of Theorem 6.2 or of the matching-polytope corollary is known to exist on Prove2Me or in Mathlib. The two milestones isolate the constructive half (Lemma 6.1 and the weighting built from it), which is reusable for any statement that needs an explicit objective singling out two stable sets.

Difficulty

The "only if" direction and the equality analysis are elementary; the substance lies in the "if" direction. An objective that makes both $y$ and $z$ optimal is easy to write down, for example $c=y+z$ ; the difficulty is to make them the only optimal vectors. Any stable set that agrees with $Y$ on some connected pieces of $H$ and with $Z$ on others ties with $y$ and $z$ under naive weightings, so the weights on $(Y-Z)\cup(Z-Y)$ must be chosen so that every mixed choice loses strictly. The integrality requirement on $c$ and the need to control all of $S(G)$ , not only the stable sets contained in $Y\cup Z$ , rule out a direct perturbation argument.

Formalization scope

Graphs. $V$ is a finite type with decidable equality and $G$ is a SimpleGraph V; loops and multiple edges are excluded, as in the paper.
$S(G)$ and $P(G)$ . $S(G)$ is the set of incidence vectors in V → ℝ of stable finsets; $P(G)$ is convexHull ℝ (S G).
Neighbours. Defined exactly as on p. 149: $y\ne z$ and, for some $c : V\to\mathbb Z$ , the set of maximizers of $cx$ over $S(G)$ equals $\{y,z\}$ . The face-lattice notion of an edge of $P(G)$ is not used; its equivalence with this definition is not part of the paper.
Induced subgraph and connectedness. $H$ is G.induce of the set $(Y\setminus Z)\cup(Z\setminus Y)$ , and "connected" is Mathlib's SimpleGraph.Connected, which requires at least one vertex. For $y=z$ both sides of the goal are therefore false.
Trees. SimpleGraph.IsTree, which includes connectedness; a spanning tree of $H$ is a graph $T$ on the vertex set of $H$ with $T\le H$ and T.IsTree. In Lemma 6.1 the integers $c_u$ and $m$ are natural numbers.

A trivializing formalization — defining neighbours through the symmetric-difference condition or through Lemma 6.1's certificate, or omitting $y\neq z$ from the definition — is excluded: neighbours are defined only through unique maximizers of integer objectives over $S(G)$ .

A complete development needs only finite graphs, induced subgraphs, spanning trees of connected graphs (available in Mathlib) and finite sums. Contributions welcome beyond the milestones: the equivalence of this notion of neighbours with the one-dimensional faces of $P(G)$ , and Corollary 6.3 for the matching polytope via line graphs.

Selected references

V. Chvátal, On certain polytopes associated with graphs, Journal of Combinatorial Theory, Series B 18 (1975), 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
M. W. Padberg, On the facial structure of set packing polyhedra, Mathematical Programming 5 (1973), 199–215. https://doi.org/10.1007/BF01580121

6 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

On Certain Polytopes Associated with Graphs II: No Clique Is a Cutset of a Connected α-Critical GraphResearch Paper

Motivation

The stability number $\alpha(G)$ of a graph, the largest number of pairwise non-adjacent vertices, is the optimum of an integer program over the stable set polytope $P(G)$ . Linear programming duality turns any explicit linear description of $P(G)$ into a certificate of optimality for $\alpha(G)$ , which is why the question "which inequalities are needed to describe $P(G)$ ?" has been central to polyhedral combinatorics since Edmonds' description of the matching polytope (Edmonds 1965). Chvátal's 1975 paper (doi:10.1016/0095-8956(75)90041-6) initiated the systematic study of $P(G)$ for arbitrary graphs: which graph operations preserve a known description, and which inequalities are facets, i.e. indispensable in every description.

Section 4 of the paper treats one such operation, gluing two graphs along a complete subgraph, and one family of facets, the "rank" inequality $\sum_u x_u\le\alpha(G)$ for graphs whose critical edges connect all vertices. Combining the two yields a purely graph-theoretic fact about $\alpha$ -critical graphs (graphs in which deleting any edge increases the stability number): no complete subgraph separates such a graph. The fact is due to Berge (Graphes et hypergraphes, 1970, Ch. 13, §3, Corollary 2); Chvátal's derivation obtains it from polyhedral arguments. $\alpha$ -critical graphs were studied by Erdős and Gallai, Hajnal, Andrásfai and Lovász, and their structure is closely tied to the facets of $P(G)$ .

Setting

Graphs are finite, undirected and loopless: $G=(V,E)$ . A stable set is a set of pairwise non-adjacent vertices; $\alpha(G)$ is the largest size of a stable set. The incidence vector of $s\subseteq V$ is $\chi^s\in\mathbb R^V$ with $\chi^s_u=1$ for $u\in s$ and $0$ otherwise. $S(G)$ is the set of incidence vectors of stable sets and

P(G)=\operatorname{conv}S(G)\subseteq\mathbb R^V .

A finite system $\sum_{u\in V}a_{iu}x_u\le b_i$ $(i\in J)$ is a defining linear system of $P$ if its solution set is exactly $P$ . An inequality $\sum_u a_ux_u\le b$ is a facet of $P$ if every defining linear system of $P$ contains, for some $t>0$ , the inequality $\sum_u ta_ux_u\le tb$ .

An edge $e$ of $G$ is critical if $\alpha(G-e)=\alpha(G)+1$ ; $E^*$ denotes the set of critical edges, $G^*=(V,E^*)$ , and $G$ is $\alpha$ -critical if every edge is critical. For graphs $G_1=(V_1,E_1)$ , $G_2=(V_2,E_2)$ put $G_1\cap G_2=(V_1\cap V_2,E_1\cap E_2)$ and $G_1\cup G_2=(V_1\cup V_2,E_1\cup E_2)$ . A vertex set $K$ is a cutset of $G$ if two vertices outside $K$ are joined by no path of $G-K$ , the subgraph induced on $V\setminus K$ .

In Lean, all objects live in the namespace ChvatalPolytopes.Separation: stablePolytope G, IsFacet P a b, IsCriticalEdge, criticalGraph G (for $G^*$ ), IsAlphaCritical G and IsCutset G K.

Formalization targets

Goal: Corollary 4.3 (p. 144)

For a finite connected $\alpha$ -critical graph $G$ and any $K\subseteq V$ inducing a complete subgraph,

K \text{ is not a cutset of } G .

The goal is pure graph theory; its proof in the paper consists of the two polyhedral theorems below.

Milestones

Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$ $(u\in V)$ , $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$ : the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.

Theorem 4.1 (p. 141). If $G_1\cap G_2$ is complete, the union of defining linear systems of $P(G_1)$ and $P(G_2)$ (each containing its nonnegativity rows) is a defining linear system of $P(G_1\cup G_2)$ .
Theorem 4.2 (p. 143). If $G^*$ is connected, then

\sum_{u\in V}x_u\le\alpha(G)

is a facet of $P(G)$ .

Significance

Theorem 4.1 says that clique-sums are harmless for linear descriptions of $P(G)$ : a description of a graph glued along a clique is the union of descriptions of the pieces. It underlies the later decomposition theory of stable set polytopes (clique cutsets appear throughout the study of perfect and $t$ -perfect graphs). Theorem 4.2 supplies a large class of facets with a combinatorial certificate, and was the starting point of the study of rank facets. Corollary 4.3 illustrates how polyhedral statements yield structural graph theory: the facet in Theorem 4.2 cannot coexist with a clique cutset.

All three results are proved in the paper, and Berge's corollary was known before it. None of them has, to the knowledge of this mission, a machine-checked proof; Mathlib has stable sets (IsIndepSet, indepNum), cliques and convex hulls, but no stable set polytope, no notion of facet via defining systems, and no $\alpha$ -critical graphs. The mission produces these definitions and the formal proofs of Proposition 2.1, Theorems 4.1, 4.2 and Corollary 4.3.

Difficulty

Proposition 2.1 requires LP duality in the form "min = max with both optima attained" together with a separation argument that reduces arbitrary objectives to integral ones; the "if" direction fails without the nonnegativity rows, so the statement is sensitive to the exact form of the system. In Theorem 4.1 the inclusion $P(G_1\cup G_2)\subseteq$ (solutions of the union) is routine; the difficulty is the converse: a point whose restrictions lie in $P(G_1)$ and in $P(G_2)$ is a convex combination of stable sets on each side, and the two combinations have to be matched on the clique $V_1\cap V_2$ to produce stable sets of $G_1\cup G_2$ . Theorem 4.2 concerns every defining linear system, so it cannot be proved by exhibiting one description; the natural route via "affinely independent tight points" is a different definition of facet and needs full-dimensionality of $P(G)$ to be equivalent. Finally, the goal requires translating a cutset into a decomposition $G=G_1\cup G_2$ with complete intersection, and then showing that a union of two systems on smaller vertex sets cannot contain a positive multiple of $\sum_{u\in V}x_u\le\alpha(G)$ .

Formalization scope

Graphs are SimpleGraph V on a Fintype V with DecidableEq V. $S(G)$ is a set of functions V → ℝ (incidence vectors of stable finsets), and $P(G)$ is convexHull ℝ (stableVectors G).
Linear systems are indexed by finite types with real coefficients. "Defining linear system" is equality of the solution set with the polytope. IsFacet quantifies over all finite index types J : Type and all real systems whose solution set equals the polytope; it is the paper's definition, not the affinely-independent-points characterization.
Proposition 2.1: "min = max" means an attained minimum equal to the maximum; the hypothesis $S\neq\emptyset$ is added (the paper's $\max$ over $S$ needs it), and the nonnegativity rows are kept.
Theorem 4.1: the glued graph $G$ lives on a type $V$ with finsets $V_1\cup V_2=V$ ; $G_1,G_2$ are the induced subgraphs on $V_1,V_2$ ; " $G_1\cap G_2$ complete" is encoded as " $V_1\cap V_2$ is a clique of $G$ and no edge joins $V_1-V_2$ to $V_2-V_1$ ", which is equivalent to the paper's hypotheses. The rows of each system are evaluated on the restriction of $x$ .
Theorem 4.2: " $G^*$ connected" is Mathlib's Connected, which requires $V\neq\emptyset$ — for $V=\emptyset$ the statement would be false. $\alpha(G)$ is indepNum, cast to $\mathbb R$ .
Corollary 4.3: "complete subgraph" is any clique set G.IsClique K, not only maximal cliques (the paper reserves "clique" for maximal complete subgraphs, but the corollary speaks of complete subgraphs), including $K=\emptyset$ . "Cutset" means two vertices outside $K$ joined by no path of $G-K$ . The formalization " $G-K$ is not connected" is ruled out: under Mathlib's convention it would make $K=V$ a cutset and the statement false for $K_1$ and $K_2$ .
Reusable infrastructure: the stable set polytope, facets via defining systems, Proposition 2.1 (shared with the other missions of this series), critical edges and $\alpha$ -critical graphs. Contributions of intermediate lemmas (LP duality in the attained form, full-dimensionality of $P(G)$ , the cutset–decomposition equivalence) are welcome.

Selected references

V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
C. Berge, Graphes et hypergraphes, Dunod, Paris, 1970 (English translation: Graphs and Hypergraphs, North-Holland, 1973), Chapter 13, §3.
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, J. Res. Nat. Bur. Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
M. W. Padberg, On the facial structure of set packing polyhedra, Math. Programming 5 (1973) 199–215. https://doi.org/10.1007/BF01580121
L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4

8 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Linear Optimization·Captain: mikedeng1

On Certain Polytopes Associated with Graphs I: Clique Inequalities Define the Stable Set Polytope Exactly for Perfect GraphsResearch Paper

Motivation

Many combinatorial optimization problems ask for the best subset of a finite set subject to combinatorial side conditions. The polyhedral method replaces the finite family of feasible subsets by the convex hull of their incidence vectors and asks for an explicit system of linear inequalities describing that convex hull; once such a system is known, linear programming duality gives min–max theorems and certificates of optimality. The maximum weight stable set problem is the central test case: it is NP-hard in general, so no tractable complete description of its polytope is expected for all graphs, and the question becomes for which graphs a simple description suffices.

V. Chvátal's 1975 paper On certain polytopes associated with graphs answers this question for the two simplest families of valid inequalities, and its Section 3 connects the answer to Berge's perfect graphs. The result is a standard entry point to polyhedral combinatorics and is one of the ingredients behind the later polynomial-time algorithms for stable sets in perfect graphs by Grötschel, Lovász and Schrijver.

Timeline. Berge (1961) introduced perfect graphs and conjectured that a graph is perfect if and only if its complement is. Lovász (Normal hypergraphs and the perfect graph conjecture, Discrete Math. 1972; A characterization of perfect graphs, J. Combin. Theory Ser. B 1972) proved this, together with the characterization of perfection by $\alpha(G_A)\,\omega(G_A)\ge|A|$ and the invariance of perfection under vertex duplication. Fulkerson's theory of antiblocking polyhedra (1971–72) gave a polyhedral route to the same equivalence. Chvátal (received 1972, published 1975) gave the self-contained polyhedral statement formalized here, with a proof based on Lovász's two theorems.

Setting

A graph $G=(V,E)$ is finite, undirected and loopless. A stable set is a set of vertices no two of which are adjacent. A clique is a maximal complete subgraph, and $C(G)$ is the set of vertex sets $W\subseteq V$ of the cliques of $G$ .

$S(G)\subseteq\mathbb R^V$ is the set of zero–one vectors $x=(x_u:u\in V)$ such that $\{u:x_u=1\}$ is stable, and the stable set polytope is $P(G)=\operatorname{conv}S(G)$ . A finite system of linear inequalities is a defining linear system of $P(G)$ if its solution set is exactly $P(G)$ . For $c\in\mathbb R^V$ write $cx=\sum_{u\in V}c_ux_u$ .

$G$ is perfect (the paper's $\alpha$ -perfect) if for every zero–one vector $c$ ,

\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\ \lambda_W\in\{0,1\},\ \sum_{W\in C(G),\,u\in W}\lambda_W\ge c_u\ (u\in V)\Big\}.

For $A\subseteq V$ , $G_A$ is the induced subgraph, $\alpha(G_A)$ its stability number and $\omega(G_A)$ its clique number. To duplicate a vertex $u$ is to add a new vertex $u'$ adjacent to all neighbours of $u$ but not to $u$ .

In the Lean development these are stableVectors G, stablePolytope G, maximalCliques G, IsPerfect G and duplicate G u in the namespace ChvatalPolytopes.Perfect.

Formalization targets

Goal: Theorem 3.1 (p. 140)

For every graph $G$ , the system

-x_u\le0\quad(u\in V),\qquad\sum_{u\in W}x_u\le1\quad(W\in C(G))

is a defining linear system of $P(G)$ if and only if $G$ is perfect. Both directions are required.

Milestones

Proposition 2.1 (pp. 139–140). For a finite nonempty set $S$ of solutions of $-x_u\le0$ , $\sum_u a_{iu}x_u\le b_i$ $(i\in J)$ , the solution set equals $\operatorname{conv}S$ if and only if for every $c\in\mathbb Z^V$

\max\{cx:x\in S\}=\min\Big\{\sum_i\lambda_ib_i:\lambda\ge0,\ \sum_i\lambda_ia_{iu}\ge c_u\ (u\in V)\Big\}.

Lovász's first theorem (§3, p. 140). Every nonperfect $G$ has $A\subseteq V$ with $\alpha(G_A)\,\omega(G_A)<|A|$ .
Lovász's second theorem (§3, p. 140). Duplicating a vertex of a perfect graph gives a perfect graph.
Condition (iii) (p. 141). $G$ is perfect if and only if for every $c\in\mathbb Z^V$

\max\{cx:x\in S(G)\}=\min\Big\{\sum_{W\in C(G)}\lambda_W:\lambda_W\ge0,\ \sum_{W\ni u}\lambda_W\ge c_u\ (u\in V)\Big\}.

Significance

The result. The nonnegativity and clique inequalities are valid for $P(G)$ for every graph. Theorem 3.1 says they are complete exactly for perfect graphs, so on perfect graphs the maximum weight stable set problem is a linear program over an explicitly described polytope, and weighted min–max theorems (stable sets versus clique covers) follow from LP duality. Combined with the perfect graph theorem, it gives a polyhedral characterization of perfect graphs, and it is the model for later results that identify graph classes by the facets of their stable set polytopes (odd-cycle inequalities, $t$ -perfection, Section 7 of the same paper).

Formalizing it. The result is classical and proved. No machine-checked version of it is known, and Mathlib has neither perfect graphs nor stable set polytopes. The mission produces a formal statement of the polyhedral characterization with the paper's own notion of perfection, a formal version of the convex-hull/LP min–max principle (Proposition 2.1), which is reusable for any 0–1 polytope, and formal statements of the two theorems of Lovász that the proof relies on.

Difficulty

Proposition 2.1 reduces Theorem 3.1 to the equivalence of perfection with a fractional min–max for all integer weights. The obvious approach to that equivalence fails in both directions. From perfection one only gets the min–max for zero–one weights and zero–one multipliers; general integer weights do not reduce to zero–one weights by linearity, because the minimum over clique covers is not additive in $c$ . Conversely, a fractional clique cover of value $\alpha$ does not directly produce an integral one. The paper crosses this gap with two theorems of Lovász: a numerical certificate of nonperfection, and the invariance of perfection under vertex duplication. Both are substantial graph-theoretic results in their own right, and neither follows from the definitions by routine manipulation.

Proposition 2.1 itself needs separation of a point from a polytope by an integral objective and LP strong duality with the nonnegativity rows handled separately.

Formalization scope

Vertices form a finite type V with decidable equality; a graph is a SimpleGraph V. $S(G)$ is a set of functions V → ℝ, and $P(G)$ is Mathlib's convexHull ℝ of it. $C(G)$ is the finset of finsets that are maximal among cliques (Maximal), as on the page; with $V=\emptyset$ the only maximal clique is $\emptyset$ . "Defining linear system" is an equality of sets. Every "max = min" is written out in full: there is a value $m$ that is the maximum over $S$ (attained and an upper bound), some feasible multiplier vector attains $m$ , and every feasible multiplier vector has objective at least $m$ . Clique multipliers are functions Finset V → ℝ read only on $C(G)$ .

Explicit conventions and added hypotheses:

In Proposition 2.1 the index set $J$ is a finite type, coefficients are real, the nonnegativity rows are kept as a separate conjunct $x\ge0$ , and $S$ is assumed nonempty (the paper's $\max$ over $S$ needs it).
$\alpha$ and $\omega$ are Mathlib's indepNum and cliqueNum (natural numbers) of G.induce A.
The duplicated graph lives on Option V, with none the new vertex.

Perfection is the paper's zero–one min–max, not "the clique system defines $P(G)$ " (which would make the goal a tautology) and not Berge's $\chi(G_A)=\omega(G_A)$ (a different definition, equivalent only through the perfect graph theorem). $P(G)$ is the convex hull of $S(G)$ , never the solution set of an inequality system.

Needed infrastructure, all reusable: integral separation from a rational polytope and LP strong duality in the form $\max\{cx:Ax\le b,x\ge0\}=\min\{\lambda b:\lambda A\ge c,\lambda\ge0\}$ ; basic facts about stable sets and maximal cliques of induced subgraphs and of duplicated graphs; invariance of IsPerfect under graph isomorphism and under taking induced subgraphs. Proofs of the Lovász milestones, which have independent value for a Mathlib theory of perfect graphs, are welcome.

Selected references

V. Chvátal, On certain polytopes associated with graphs, J. Combin. Theory Ser. B 18 (1975) 138–154. https://doi.org/10.1016/0095-8956(75)90041-6
L. Lovász, Normal hypergraphs and the perfect graph conjecture, Discrete Math. 2 (1972) 253–267. https://doi.org/10.1016/0012-365X(72)90006-4
L. Lovász, A characterization of perfect graphs, J. Combin. Theory Ser. B 13 (1972) 95–98. https://doi.org/10.1016/0095-8956(72)90045-7
D. R. Fulkerson, Anti-blocking polyhedra, J. Combin. Theory Ser. B 12 (1972) 50–71. https://doi.org/10.1016/0095-8956(72)90032-9
M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

8 thms2 active usersReviewed

Completed

Optimization Theoretical Computer Science·Captain: mikedeng1

An Optimal On-Line Algorithm for Metrical Task System 1: Every n-State Metrical Task System Has Competitive Ratio 2n - 1Research Paper

Motivation

A system that processes a stream of tasks can often be configured in several ways, and the configuration affects both the cost of the current task and the cost of switching before the next one: paging schemes, replicated files, server placements. When the future is unknown, the natural worst-case yardstick is competitive analysis, introduced by Sleator and Tarjan for list update and paging (Sleator–Tarjan 1985): an on-line strategy is compared with the optimal strategy that knows the whole input in advance.

Borodin, Linial and Saks (J. ACM 1992; conference version STOC 1987) proposed metrical task systems as a single model containing all such problems, and determined the exact deterministic competitive ratio of every such system. Their theorem is the starting point of the on-line-algorithms literature on metrical task systems, the $k$ -server problem (Manasse–McGeoch–Sleator 1990) and their randomized variants.

Timeline. 1985: Sleator and Tarjan introduce competitive analysis for paging and list update. 1987: Borodin, Linial and Saks prove $w(S,d)=2n-1$ for every $n$ -state metrical task system (journal version 1992). 1990: Manasse, McGeoch and Sleator extend the task-system model to restricted task sets and pose the $k$ -server conjecture. The randomized ratio of the uniform task system, bounded in the same paper between $H(n)$ and $2H(n)$ , is the subject of the companion mission.

Setting

A task system $(S,d)$ has a finite set $S$ of $n$ states and a transition-cost matrix $d$ with $d(i,i)=0$ , $d(i,j)>0$ for $i\neq j$ , and the triangle inequality $d(i,j)+d(j,k)\ge d(i,k)$ . It is metrical if also $d(i,j)=d(j,i)$ .

A task $T$ is a vector of nonnegative processing costs $T(s)$ , $s\in S$ . Given a task sequence $\mathbf T=T^1\cdots T^m$ and an initial state $s_0$ , a schedule is a map $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$ ; task $T^i$ is processed in state $\sigma(i)$ , and the cost is

c(\mathbf T;\sigma)=\sum_{i=1}^m d(\sigma(i-1),\sigma(i))+\sum_{i=1}^m T^i(\sigma(i)).

The off-line optimum $c_0(\mathbf T)$ is the minimum over all schedules. An on-line algorithm $A$ chooses $\sigma(i)$ knowing only $s_0$ and $T^1,\dots,T^i$ ; its cost is $c_A(\mathbf T)$ . For $w>0$ , $A$ is $w$ -competitive if there is a constant $K_w$ with $c_A(\mathbf T)\le w\,c_0(\mathbf T)+K_w$ for every finite task sequence. The competitive ratio of $A$ is $w(A)=\inf\{w: A\text{ is }w\text{-competitive}\}$ , and the competitive ratio of the task system is $w(S,d)=\inf_A w(A)$ .

For the upper bound the paper also uses continuous-time schedules, in which task $T^i$ occupies the interval $[i,i+1)$ and the scheduler may change state at any real time, paying $\int_i^{i+1}T^i(\sigma(t))\,dt$ for processing. For a general (possibly asymmetric) matrix $d$ , the cycle offset ratio $\psi(d)$ is the maximum over closed walks $s_0,\dots,s_k=s_0$ of $\sum_i d(s_{i-1},s_i)\big/\sum_i d(s_i,s_{i-1})$ ; it equals $1$ when $d$ is symmetric.

Formalization targets

Goal: Theorem 1.1

For every metrical task system $(S,d)$ with $n$ states,

w(S,d)=2n-1 .

The value depends on $n$ only, not on the distances.

Milestones

Lemma 2.1. If $c_0(T^1\cdots T^m)\to\infty$ along an infinite task sequence $\mathbf T$ , then $w(A)\ge w_{\mathbf T}(A)=\limsup_m c_A/c_0$ .
Theorem 2.2. Against the cruel taskmaster $M(\varepsilon)$ , which charges $\varepsilon$ in the state the algorithm currently occupies,

w_{\mathbf T(\varepsilon)}(A)\ge\frac{2n-1}{1+\varepsilon/\min_{i\neq j}d(i,j)} .

Lemma 3.1. Every on-line continuous-time algorithm is matched, on every task sequence, by an on-line discrete-time algorithm.
Lemmas 6.3, 6.4, 6.2. Properties of the functions $f_k$ that drive the algorithm $A^*_d$ : $f_k(s)-f_k(s')\le d(s',s)$ ; the identity $2\sum_{s\ne s_k}f_k(s)+f_k(s_k)=C_{k-1}+\sum_{i\le k}d(s_i,s_{i-1})$ ; and $f_k\le h_k$ , the off-line cost at the $k$ -th transition time.
Theorem 6.1 (= Theorem 1.2). For every task system, symmetric or not, $A^*_d$ has competitive ratio at most $(2n-1)\psi(d)$ .

Significance

The theorem settles the deterministic competitive ratio of the whole class of metrical task systems: the lower bound says that no deterministic on-line strategy can beat $2n-1$ on any metric, and the upper bound supplies one algorithm that achieves it on every metric. For asymmetric costs the same algorithm gives $(2n-1)\psi(d)$ . The $2n-1$ lower bound is also the benchmark against which restricted models, such as paging and the $k$ -server problem, measure their improvements, and the randomized question it leaves open drove much of the later work on metrical task systems.

The result was proved in 1987 and is standard; to the best of our knowledge no machine-checked proof exists. A formal development would provide a reusable model of deterministic on-line algorithms and competitiveness (on-line maps from task prefixes, additive competitiveness, infima over algorithms), an adversary construction by mutual recursion with an arbitrary algorithm, and an exact treatment of continuous-time schedules with piecewise-constant task costs. These pieces are reusable for other competitive-analysis results.

Difficulty

The lower bound is not a single bad input: the adversary is built from the algorithm it plays against, so the hard task sequence exists only as a recursion interleaved with the algorithm's choices, and the bound must hold for every deterministic on-line map, including ones that behave erratically. Obtaining the exact constant $2n-1$ , rather than some $\Omega(n)$ bound, requires a sharp estimate of the off-line cost of that sequence.

The upper bound needs an algorithm defined in continuous time, whose transition times are determined by accumulated processing costs; the budgets can be zero, so transitions can be instantaneous, and a formal cost must remain well defined before one knows that only finitely many transitions occur. Relating the off-line cost function at those times to the recursively defined $f_k$ (Lemma 6.2) requires reasoning about all continuous-time off-line schedules. Finally, the goal combines both directions through infima over all on-line algorithms, and the discretization of Lemma 3.1 must be composed with the continuous-time algorithm.

Formalization scope

States form a finite type S (Fintype, DecidableEq, Nonempty); the goal is stated for all $n\ge1$ , where $n=1$ gives $w(S,d)=1$ . Task costs are finite nonnegative reals; the paper also allows $+\infty$ entries, which are excluded (this affects neither bound). A task sequence is T : Fin m → S → ℝ, with T i the paper's $T^{i+1}$ , and a schedule is σ : Fin (m+1) → S. An on-line algorithm is a map sending $(s_0,[T^1,\dots,T^i])$ to $\sigma(i)$ , so on-line behaviour is built into the type. Competitiveness is written additively, $c_A\le w\,c_0+K$ , with $K$ independent of the task sequence and of $s_0$ .

The competitive ratio competitiveRatio d is the real infimum of the set of all $w$ for which some on-line algorithm is $w$ -competitive. It is not defined as an infimum of per-algorithm real infima: a non-competitive algorithm has $W_A=\emptyset$ , whose real infimum is $0$ , and that would drag $w(S,d)$ to $0$ for every system. Since the goal's value $2n-1$ is at least $1$ while the empty set's real infimum is $0$ , the goal cannot hold vacuously.

Continuous-time algorithms are given as lists of $(\text{state},\text{length})$ pieces per unit interval; processing integrals are exact finite sums. The algorithm $A^*_d$ minimizes over states different from the current one, as its proof requires (the printed rule ranges over all states, and would stall); ties are left arbitrary. Its budgets may be $0$ , its entry times are Option ℝ, and its cost is a sum in $[0,\infty]$ , so that Theorem 6.1 itself asserts that only finitely many transitions occur. The ratio $\psi(d)$ excludes closed walks that never move, and Theorems 2.2 and 6.1 require $n\ge2$ , where $\min_{i\ne j}d(i,j)$ and $\psi(d)$ are defined. Lemma 3.1 is stated comparing $A$ with $A'$ (the printed statement says "as well as $A$ ").

A complete development needs: the discrete model and off-line optimum (finite minimum over schedules), limsup arguments in EReal, continuous-time schedules with piecewise-constant costs, and the recursion defining $A^*_d$ . Proofs of any milestone, including the purely combinatorial Lemmas 6.3 and 6.4, are welcome, as is a formal composition of Lemma 3.1 with Theorem 6.1.

Selected references

A. Borodin, N. Linial, M. E. Saks, An optimal on-line algorithm for metrical task system, Journal of the ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Communications of the ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive algorithms for server problems, Journal of Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W

12 thms2 active usersReviewed

Combinatorics Discrete Geometry Linear Optimization·Captain: mikedeng1

On Sub-determinants and the Diameter of Polyhedra: A Polynomial Diameter Bound in the Largest SubdeterminantResearch Paper

Motivation

The combinatorial diameter of a polyhedron is the largest distance, in its vertex-edge graph, between two vertices. It is a lower bound on the number of pivots any edge-following method such as the simplex method needs in the worst case, which is why the polynomial Hirsch conjecture — the diameter of $P = \{x \in \mathbb{R}^n : Ax \le b\}$ is bounded by a polynomial in $m$ and $n$ — is a central open question of linear optimization and discrete geometry. The best general upper bound is quasi-polynomial, $m^{1+\log n}$ (Kalai–Kleitman 1992); the original Hirsch bound $m - n$ is false for polytopes (Santos 2012).

A different line of work bounds the diameter by the arithmetic of the constraint matrix instead of its size. For an integer matrix $A$ let $\Delta$ be the largest absolute value of a sub-determinant of $A$ . Dyer and Frieze (1994) showed that for totally unimodular $A$ ( $\Delta = 1$ ) the diameter is polynomial, $O(m^{16} n^3 (\log mn)^3)$ . Bonifas, Di Summa, Eisenbrand, Hähnle and Niemeier (SoCG 2012; Discrete Comput Geom 52, 2014) improved and generalized this to $O(\Delta^2 n^4 \log n\Delta)$ for all polyhedra and $O(\Delta^2 n^{3.5} \log n\Delta)$ for polytopes, bounds that do not depend on the number $m$ of inequalities. This mission formalizes the polytope case.

Setting

Let $A \in \mathbb{Z}^{m\times n}$ with rows $a_1,\dots,a_m$ , let $b \in \mathbb{R}^m$ , and let $P = \{x \in \mathbb{R}^n : Ax \le b\}$ . A vertex of $P$ is an extreme point; for a polyhedron this is a point of $P$ at which $n$ linearly independent inequalities are tight. Two vertices $u \ne v$ are adjacent if the segment $[u,v]$ is an edge (a one-dimensional face) of $P$ . This gives the polyhedral graph $G_P = (V, E)$ , and the diameter of $P$ is at most $B$ if every two vertices are joined by a walk of at most $B$ edges.

$A$ has sub-determinants bounded by $\Delta$ if every $k\times k$ submatrix, for every $k \ge 1$ , has determinant in $[-\Delta, \Delta]$ . In particular every entry is at most $\Delta$ in absolute value.

For a vertex $v$ the normal cone $C_v$ is the set of objectives $c$ for which $v$ maximizes $c^T x$ over $P$ . With $B_n$ the closed unit ball, the volume of a set $U \subseteq V$ of vertices is

\mathrm{vol}(U) = \mathrm{vol}\Big(\bigcup_{v\in U} C_v \cap B_n\Big),

and the neighbourhood $\mathcal N(I)$ of $I \subseteq V$ is the set of vertices outside $I$ adjacent to a vertex of $I$ . A spherical cone is $S = C \cap B_n$ with $C$ closed under non-negative scaling; its dockable surface $D(S)$ is the $(n-1)$ -dimensional measure of the part of its boundary inside the open ball. A cone of revolution of angle $0<\theta\le\pi/2$ is $\{x \in B_n : v^T x \ge \cos\theta\,\|v\|\,\|x\|\}$ . $P$ is non-degenerate if every vertex has exactly $n$ tight inequalities.

Formalization targets

Goal: Theorem 2 (p. 105)

If $A \in \mathbb{Z}^{m\times n}$ has all sub-determinants bounded by $\Delta$ and $P$ is bounded, then

\operatorname{diam}(P) \le 2\Big\lfloor \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln\!\big(2^n\, n!\, n^{n/2}\,\Delta^n\big)\Big\rfloor + 2 \;=\; O(\Delta^2 n^{3.5}\log n\Delta).

No non-degeneracy, full-dimensionality or rank condition is assumed, and the bound is uniform in $m$ and $b$ .

Milestones

Lemma 3 (p. 108): for a vertex $v$ of a non-degenerate polytope, $D(S_v) \le \Delta^2 n^3\,\mathrm{vol}(S_v)$ , where $S_v = C_v \cap B_n$ .
Lemma 4 (p. 109): among spherical cones of a given volume, a cone of revolution has minimum dockable surface.
Lemma 5 (p. 110): for a cone of revolution, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$ .
Lemma 6 (p. 111): for every measurable spherical cone with $\mathrm{vol}(S) \le \frac12 \mathrm{vol}(B_n)$ , $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$ .
Lemma 1 (p. 105): for a non-degenerate polytope and $I \subseteq V$ with $\mathrm{vol}(I) \le \frac12\mathrm{vol}(B_n)$ ,

\mathrm{vol}(\mathcal N(I)) \ge \sqrt{\tfrac{2}{\pi}}\,\frac{1}{\Delta^2 n^{2.5}}\,\mathrm{vol}(I).

Eq. (1) (p. 105): if $I_j$ is the set of vertices at graph distance at most $j$ from a vertex $v$ and $\mathrm{vol}(I_j) \le \frac12\mathrm{vol}(B_n)$ , then $j \le \sqrt{2\pi}\,\Delta^2 n^{2.5}\ln(2^n/\mathrm{vol}(I_0))$ .

Significance

The result. Theorem 2 bounds the diameter of every integral polytope by a polynomial in the dimension and the largest sub-determinant, independently of the number of facets. For totally unimodular matrices, which cover network-flow, bipartite matching and transportation polytopes, it gives $O(n^{3.5}\log n)$ , improving the Dyer–Frieze bound by a large polynomial factor. It shows that the obstruction to a polynomial Hirsch bound, if any, must come from matrices with large sub-determinants. The volume-expansion method — measuring breadth-first search by the volume of the normal fan it has covered — was later refined, for instance in the shadow-vertex analysis of Dadush–Hähnle, which improves the dependence on $n$ .

Formalizing it. The theorem is proved (2012/2014); no machine-checked proof is known. A formal development needs, on top of Mathlib, the normal fan of a polytope and its relation to the vertex-edge graph, a Hausdorff-measure calculus for cones (surface of a cone in terms of its base), Lévy's isoperimetric inequality on the sphere in a measure-theoretic form, and explicit Gamma-function estimates. Each of these is reusable well beyond this paper.

Difficulty

The combinatorial side is short; the geometry is not. Lemma 4 is the spherical isoperimetric inequality of Lévy, which Mathlib does not have in any form, and which the paper cites rather than proves; the relations between the volume of a spherical cone, the area of its base, its lateral surface and the length of the base's boundary (Eq. (3), "basic integration") are also absent. Lemma 3 depends on the structure of the normal cone of a vertex of a non-degenerate polytope (full-dimensional, simplicial, generated by rows of $A$ ), none of which is available for Mathlib's extreme points. Lemma 1 depends on the normal fan of a polytope: the normal cones have pairwise disjoint interiors, cover $\mathbb{R}^n$ , and share a facet exactly when their vertices are adjacent. The step from non-degenerate to arbitrary polytopes perturbs $b$ and needs the diameter not to decrease, a statement about the vertex-edge graph under perturbation. A shortcut through a finite graph abstraction is not available: the constant depends on the geometry of the normal cones, not only on the graph.

Formalization scope

The polyhedron is Hirsch.Hpoly (rowVec A) b, with rowVec A i the $i$ -th row of $A \in$ Matrix (Fin m) (Fin n) ℤ as a vector of EuclideanSpace ℝ (Fin n). Vertices are Set.extremePoints ℝ P, adjacency is Hirsch.Adj, "diameter at most $B$ " is Hirsch.DiamLE P B, all from the published Hirsch_model. The normal cone is the published FirstOrderOpt.ConvexTheory.normalCone. Volumes are Lebesgue measure with values in $[0,\infty]$ ; the dockable surface uses μHE[n-1], the Hausdorff measure normalized to agree with Lebesgue measure on hyperplanes, applied to frontier S ∩ Metric.ball 0 1. $\Delta$ is a natural number and the sub-determinant bound ranges over all sizes $k \ge 1$ .

Explicit constants. The paper writes $O(\Delta^2 n^{3.5}\log n\Delta)$ in Theorem 2; the proof on pp. 105–106 yields $2\lfloor K\rfloor + 2$ with $K = \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln(2^n n!\, n^{n/2}\Delta^n)$ , from Eq. (1), the bound $\mathrm{vol}(I_0) \ge 1/(n!\,n^{n/2}\Delta^n)$ and the fact that the diameter is at most twice the number of breadth-first-search iterations needed to cover more than half of $B_n$ . This explicit bound is the goal. The ratios $D/\mathrm{vol}$ of Lemmas 3, 5, 6 are stated in multiplicative form.

Non-degeneracy is a hypothesis of Lemma 3, Lemma 1 and Eq. (1) only, as in the paper's §1.1, and never of Theorem 2. The neighbourhood $\mathcal N(I)$ excludes $I$ ; including it would make Lemma 1 trivial, since its constant is below $1$ . Lemma 4 is stated against every competitor: for every measurable spherical cone $S$ and every cone of revolution $S^*$ of the same volume, $D(S^*) \le D(S)$ ; it does not assert existence of a cone of a prescribed volume. The goal is Theorem 2 about the polytope and its graph, not an abstract statement about set families with a volume-expansion property; integrality of $A$ and the bound on minors of every size are both essential (scaling a real matrix down makes $\Delta$ arbitrarily small), and the raw Hausdorff measure μH[n-1] would put Lemmas 3 and 6 on incompatible scales.

Contributions are welcome at every level: the normal fan and its adjacency structure, cone surface formulas, the Gamma estimate $\Gamma(x+\frac12)/\Gamma(x) \ge \sqrt{x-\frac14}$ , and a formal Lévy inequality.

Selected references

N. Bonifas, M. Di Summa, F. Eisenbrand, N. Hähnle, M. Niemeier, On Sub-determinants and the Diameter of Polyhedra, Discrete Comput Geom 52 (2014) 102–115. https://doi.org/10.1007/s00454-014-9601-x
M. Dyer, A. Frieze, Random walks, totally unimodular matrices, and a randomised dual simplex algorithm, Math. Program. 64 (1994) 1–16. https://doi.org/10.1007/BF01582563
G. Kalai, D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992) 315–316. https://doi.org/10.1090/S0273-0979-1992-00285-9
F. Santos, A counterexample to the Hirsch conjecture, Annals of Math. 176 (2012) 383–412. https://doi.org/10.4007/annals.2012.176.1.7
T. Figiel, J. Lindenstrauss, V. Milman, The dimension of almost spherical sections of convex bodies, Acta Math. 139 (1977) 53–94 (Lévy's isoperimetric inequality, Theorem 2.1). https://doi.org/10.1007/BF02392234
D. Dadush, N. Hähnle, On the shadow simplex method for curved polyhedra, Discrete Comput Geom 56 (2016). https://arxiv.org/abs/1412.6705

11 thms2 active usersReviewed

Completed

Convex Optimization Optimization·Captain: mikedeng1

Nonmonotone Spectral Projected Gradient Methods on Convex Sets I: SPG2 Is Well Defined and Its Accumulation Points Are StationaryResearch Paper

Motivation

Minimizing a smooth function over a closed convex set $\Omega\subseteq\mathbb R^n$ on which projection is cheap (a box, a ball, a simplex) is a routine subproblem in large-scale optimization: box-constrained minimization is the inner solver of augmented Lagrangian methods, and bound-constrained least squares, image restoration and density estimation all have this form. The classical projected gradient method of Goldstein and of Levitin and Polyak is simple and needs only gradients and projections, but with constant or Armijo-type step lengths it is slow.

Spectral projected gradient (SPG) methods, introduced by Birgin, Martínez and Raydan (paper), combine three ingredients: the projected gradient direction; the Barzilai–Borwein (spectral) step length $\alpha_{k+1}=\langle s_k,s_k\rangle/\langle s_k,y_k\rangle$ , an inverse Rayleigh quotient of the average Hessian along the last step; and the nonmonotone line search of Grippo, Lampariello and Lucidi, which compares a trial value with the worst of the last $M$ objective values instead of the current one. The method is widely used in practice, and its analysis is the template for many later nonmonotone projected methods.

Timeline:

1964–1966: Goldstein; Levitin and Polyak introduce gradient projection.
1976: Bertsekas analyses the Armijo rule along the projection arc.
1986: Grippo, Lampariello and Lucidi introduce the nonmonotone line search for unconstrained problems.
1988: Barzilai and Borwein propose the two-point step size; Raydan (1993, 1997) proves convergence for quadratics and combines it with nonmonotone search in the unconstrained case.
2000: Birgin, Martínez and Raydan define SPG1 and SPG2 for convex constraints (SIAM J. Optim. 10(4)).
2003: the same authors publish the convergence proof that Theorem 2.1 refers to, in the inexact setting (IMA J. Numer. Anal. 23).

Setting

Let $\Omega\subseteq\mathbb R^n$ be nonempty, closed and convex, with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let $f$ have continuous partial derivatives on an open set $U\supseteq\Omega$ and write $g(x)=\nabla f(x)$ . The orthogonal projection $P(z)$ is the unique point of $\Omega$ nearest to $z$ . The scaled projected gradient is $g_t(x)=P(x-t\,g(x))-x$ for $x\in\Omega$ , $t>0$ . A point $\bar x$ is a constrained stationary point if $\langle g(\bar x),x-\bar x\rangle\ge0$ for all $x\in\Omega$ .

The parameters are an integer $M\ge1$ , reals $0<\alpha_{\min}<\alpha_{\max}$ , a sufficient-decrease constant $\gamma\in(0,1)$ and safeguards $0<\sigma_1<\sigma_2<1$ . Algorithm SPG2 starts from $x_0\in\Omega$ and $\alpha_0\in[\alpha_{\min},\alpha_{\max}]$ and at iteration $k=0,1,\dots$ :

Stop test. If $\|P(x_k-g(x_k))-x_k\|=0$ , stop: $x_k$ is stationary.
Backtracking. Set $d_k=P(x_k-\alpha_k g(x_k))-x_k$ and $\lambda=1$ . While

f(x_k+\lambda d_k)\le\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})+\gamma\lambda\langle d_k,g(x_k)\rangle\qquad(3)

fails, replace $\lambda$ by any $\lambda_{\rm new}\in[\sigma_1\lambda,\sigma_2\lambda]$ . When (3) holds, $\lambda_k=\lambda$ and $x_{k+1}=x_k+\lambda_kd_k$ . 3. Spectral step. With $s_k=x_{k+1}-x_k$ , $y_k=g(x_{k+1})-g(x_k)$ , $b_k=\langle s_k,y_k\rangle$ : $\alpha_{k+1}=\alpha_{\max}$ if $b_k\le0$ , else $\alpha_{k+1}=\min\{\alpha_{\max},\max\{\alpha_{\min},\langle s_k,s_k\rangle/b_k\}\}$ .

In Lean the projection is a function P with the predicate IsProjOnto Ω P, $g_t$ is scaledProjGrad P f t, stationarity is IsConstrainedStationary Ω f, the maximum in (3) is nonmonotoneRef f x M k, and an infinite run is IsSPG2Run Ω f P M αmin αmax γ σ₁ σ₂ x α.

Formalization targets

Goal: Theorem 2.1, accumulation points are stationary

For every infinite run $(x_k,\alpha_k)$ of SPG2 and every accumulation point $\bar x$ of $(x_k)$ ,

\langle g(\bar x),x-\bar x\rangle\ge0\qquad\text{for all }x\in\Omega.

The statement fixes no parameter values and assumes neither convexity of $f$ nor a bounded level set.

Milestones

Lemma 2.1 (ii). For $\bar x\in\Omega$ and $t\in(0,\alpha_{\max}]$ : $g_t(\bar x)=0$ iff $\bar x$ is a constrained stationary point.
Lemma 2.1 (i). For $x\in\Omega$ and $t\in(0,\alpha_{\max}]$ :

\langle g(x),g_t(x)\rangle\le-\tfrac1t\|g_t(x)\|_2^2\le-\tfrac1{\alpha_{\max}}\|g_t(x)\|_2^2.

Theorem 2.1, first clause (SPG2 is well defined). At a point where Step 1 does not stop, every admissible backtracking sequence reaches a step satisfying (3). The step is stated for an arbitrary reference value $R\ge f(x)$ , which covers the maximum in (3).
Section 2, p. 4. The iterates remain in $\Omega_0=\{x\in\Omega:f(x)\le f(x_0)\}$ .

Significance

Theorem 2.1 is the global convergence guarantee for SPG2. It holds without monotone decrease of $f$ and without any restriction on the spectral step beyond the safeguards. These are the two features that make the method fast in practice, and together they mean that no classical monotone projected-gradient argument applies directly. The same statement underlies the convergence claims of the SPG software (ACM TOMS Algorithm 813) and of the many methods that reuse the nonmonotone spectral framework: inexact SPG, augmented Lagrangian inner solvers, and projected BB methods for machine learning.

Status: the theorem is proved in the literature. This paper's proof reads "See [7]", a pointer to Birgin, Martínez and Raydan (2003). No Lean formalization of this theorem, of the nonmonotone Armijo analysis, or of the projected-gradient stationarity lemma is known. The mission produces a formal proof and a reusable Lean interface for projection-based first-order methods on convex sets.

Difficulty

The obvious argument for monotone descent methods is to show that $f(x_k)$ decreases, so that the total decrease is finite and the per-iteration decrease $\gamma\lambda_k|\langle d_k,g(x_k)\rangle|$ tends to zero. Here $f(x_k)$ need not decrease. Only the reference value $\max_{0\le j\le\min\{k,M-1\}}f(x_{k-j})$ is nonincreasing, and a small decrease of this maximum along the whole sequence does not by itself give a small decrease at the iterates that approach a given accumulation point $\bar x$ . A second difficulty is that the accepted step lengths $\lambda_k$ may tend to zero along the subsequence, while $f$ is $C^1$ only on a neighbourhood of $\Omega$ and no Lipschitz constant for $g$ is available, so no uniform sufficient-decrease estimate holds. The spectral steps $\alpha_k$ vary within $[\alpha_{\min},\alpha_{\max}]$ , so the directions $d_k$ are not a fixed function of $x_k$ .

Formalization scope

Space and data. The space is EuclideanSpace ℝ (Fin n) with inner ℝ and the 2-norm. $f$ is a total function EuclideanSpace ℝ (Fin n) → ℝ with ContDiffOn ℝ 1 f U on an open U ⊇ Ω, and $g$ is Mathlib's gradient f. The algorithm evaluates $f$ and $g$ only at points of $\Omega$ .
Iteration and trials. Iterations are indexed from $0$ . The backtracking choice (2) is universally quantified: a run carries, at each iteration, a finite trial list $\lambda^{(0)}=1$ , $\lambda^{(i+1)}\in[\sigma_1\lambda^{(i)},\sigma_2\lambda^{(i)}]$ , in which test (3) fails at every trial but the last and holds at the last.
Step size. $\alpha_{k+1}$ is given by Step 3 exactly.
Accumulation point. An accumulation point is MapClusterPt x̄ atTop x.
Excluded simplifications. A run predicate that accepts any positive step, or lets $\alpha_{k+1}$ range freely over $[\alpha_{\min},\alpha_{\max}]$ , is not SPG2. Nor is a goal stating $g_t(\bar x)=0$ instead of the variational inequality, or one that adds convexity of $f$ , a Lipschitz gradient or a bounded level set.
Non-vacuity. The hypotheses of the goal are satisfiable: for $f(x)=\|x\|^2$ , $\Omega=\mathbb R^n$ , $M=1$ , $\alpha_{\min}=1/8$ , $\alpha_{\max}=1/4$ , $\gamma=1/2$ and $v\ne0$ , the iterates $x_k=2^{-k}v$ with $\alpha_k=1/4$ form an infinite run with accumulation point $0$ .
Infrastructure. A complete development needs the variational characterization of the projection (Mathlib has it for the iInf form: norm_eq_iInf_iff_real_inner_le_zero), continuity properties of the projection, a mean-value estimate for $C^1$ functions on segments in $\Omega$ , and the nonmonotone reference-value bookkeeping. The projection lemmas and the nonmonotone bookkeeping are reusable beyond this mission, in particular for the companion mission on SPG1, and contributions of them as separate lemmas are welcome.

Selected references

E. G. Birgin, J. M. Martínez, M. Raydan, Nonmonotone spectral projected gradient methods on convex sets, SIAM J. Optim. 10(4) (2000) 1196–1211; authors' updated version, July 2004. https://doi.org/10.1137/S1052623497330963, https://www.ime.unicamp.br/~martinez/bmr.pdf
E. G. Birgin, J. M. Martínez, M. Raydan, Inexact spectral projected gradient methods on convex sets, IMA J. Numer. Anal. 23 (2003) 539–559. https://doi.org/10.1093/imanum/23.4.539
J. Barzilai, J. M. Borwein, Two-point step size gradient methods, IMA J. Numer. Anal. 8 (1988) 141–148. https://doi.org/10.1093/imanum/8.1.141
L. Grippo, F. Lampariello, S. Lucidi, A nonmonotone line search technique for Newton's method, SIAM J. Numer. Anal. 23 (1986) 707–716. https://doi.org/10.1137/0723046
M. Raydan, The Barzilai and Borwein gradient method for the large scale unconstrained minimization problem, SIAM J. Optim. 7 (1997) 26–33. https://doi.org/10.1137/S1052623494266365
D. P. Bertsekas, On the Goldstein–Levitin–Polyak gradient projection method, IEEE Trans. Automat. Control 21 (1976) 174–184. https://doi.org/10.1109/TAC.1976.1101194

10 thms2 active usersReviewed

Operations Research

Missions

Subjectivity and Correlation in Randomized Strategies II: Subjective Events Let Both Zero-Sum Players Beat the ValueResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 6.1 (p. 80)

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Theory of Dynamic Programming: The Index Rule for Bellman's Stochastic Gold-Mining ProblemResearch Paper

Motivation

Setting

Formalization targets

Milestone: the functional equation (8.2), p. 508

Goal: the decision rule (8.3), p. 509, corrected

Companion: the index policy is optimal, p. 509

Significance

Difficulty

Formalization scope

Selected references

Online Decision Making with High-Dimensional Covariates: Regret Bound of the LASSO BanditResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (regret of the LASSO Bandit)

Milestones

Significance

Difficulty

Formalization scope

Selected references

School Choice: A Mechanism Design Approach 2: The Top Trading Cycles Mechanism with Type-Specific Quotas Is Strategy-ProofResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 7 (p. 23)

Milestones

Significance

Difficulty

Formalization scope

Selected references

School Choice: A Mechanism Design Approach 1: The Top Trading Cycles Mechanism Is Strategy-ProofResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 4 (strategy-proofness)

Milestones

Significance

Difficulty

Formalization scope

Selected references

A General Framework for the Study of Decentralized Distribution Systems: A Core Allocation Rule Whose Nash Equilibrium Is First-BestResearch Paper

Pooling inventory among independent retailers

Setting

Formalization targets

Goal: Corollary 5.1 (p. 361)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Elementare Theorie der konvexen Polyeder I: A Point on All Extreme Supports of a Finite Cone Is a Nonnegative Combination of at Most n GeneratorsResearch Paper

Motivation

Setting

Formalization targets

Goal: Satz 2 (Verschärfung des Hauptsatzes), p. 295

Satz 1 (Hauptsatz), p. 291

Steps of the proof (§1–§2)

Significance

Difficulty

Formalization scope

Selected references

Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities II: An Exact 3-Cover Exists iff the Constructed Market Has an EquilibriumResearch Paper

Motivation

Setting

Formalization targets

Goal: the reduction statement

Milestones