Operations Research

Why a one-sided market can have a core

Workers can form groups and produce an output that they divide through salaries. A group may object to a proposed allocation when it can pay all of its members at least as much and one member more. The central question is whether any allocation survives every such objection. Kelso and Crawford's 1982 paper gives a sufficient condition based on how an imaginary firm would demand workers as their salaries change. This is useful when production depends on combinations of workers, yet there is no actual employer side to the market.

The one-sided result belongs to a seven-mission series: 1, the salary-adjustment process; 2, continuous-salary core existence; 3, this one-sided theorem; 4, firm-optimality; 5, comparative statics; 6, returns to workers; and 7, the no-core example. Each mission can be read independently. None of Kelso and Crawford's results was on Prove2Me before this series. The paper itself notes that Theorem 3 is similar in spirit to Shapley's core-existence result but logically independent: Shapley's convex-game condition concerns second differences of a characteristic function, whereas this theorem uses a condition on input demand. Kelso and Crawford, footnote 3.

The market and its allocations

Let $W$ be a finite set of workers, with $m=|W|$. A coalition technology $v$ assigns a real output $v(C)$ to each worker set $C\subseteq W$. A one-sided allocation consists of a partition $P=(C_z)$ of all workers and one real salary $s_i$ for each worker. The parts of $P$ are disjoint and cover $W$. Each worker has a utility $\mu^i(s_i)$ that is continuous and strictly increasing in salary, so salary comparisons express the same preferences as utility comparisons.

The paper's individual rationality condition D1′ asks for nonnegative salaries and one aggregate resource constraint:

$$s_i\ge 0\quad(i\in W),\qquad \sum_{i\in W}s_i\le\sum_{C\in P}v(C).$$

It does not require each partition block to finance its own salaries. An improving coalition is a worker set $C$ with salaries $r_i\ge s_i$ for every $i\in C$, a strict inequality for at least one member, and $\sum_{i\in C}r_i\le v(C)$. A D1′ allocation is in the strict core D2′ when no improving coalition exists. The empty coalition cannot improve because it contains no member whose salary could rise. These are equations (12)–(15) on pages 1492–1493 of the source paper.

To state gross substitutes (GS), imagine $m+1$ identical firms, each with production $v$. At a salary vector $s:W\to\mathbb R$, a firm's profit from employing $C$ is $\pi(C;s)=v(C)-\sum_{i\in C}s_i$; a demanded set maximizes this profit over all worker subsets. GS says that if salaries rise coordinatewise from $s$ to $s'$, then for every demanded set at $s$ there is a demanded set at $s'$ containing all workers of the old set whose salaries stayed unchanged. The requirement is over all real salary vectors, as in the continuous market of Section 2.

Formalization targets

Goal: Theorem 3

Assume nonnegative marginal production (MP′), no free lunch (NFL), and GS for the identical fictitious firms:

$$v(C\cup\{i\})-v(C)\ge 0,\qquad v(\varnothing)=0,\qquad \operatorname{GS}(v).$$

The goal is the exact existence statement

$$\exists (P,s),\quad (P,s)\text{ is a one-sided strict-core allocation for }v.$$

Theorem 3 appears on page 1493 of Kelso and Crawford. Its two milestones are claims from the proof: every dummy firm has zero profit at a fictitious-market strict-core allocation, and that allocation induces a one-sided strict-core allocation. Mission 2 targets the paper's Theorem 2, which supplies existence of the fictitious-market allocation; this mission does not pose a duplicate specialized version of it.

What the result gives

The theorem ensures that workers can be partitioned and paid without any group being able to make at least one of its members strictly better off while preserving every member's prior salary. It turns a condition on a firm's reactions to wage increases into stability of a market containing no firms. The result also identifies a concrete boundary for the core-existence argument: the paper later constructs a market without GS that has no core allocation in its two-sided setting. Kelso and Crawford, Section 6.

The theorem is proved in the 1982 paper; this mission asks for machine-checked statements and proofs of its one-sided definitions, the two transfer claims, and Theorem 3. The local Lean files compile as open statements, and a concrete one-worker instance checks that MP′, NFL and GS can hold together. That local check is not a proof of Theorem 3. The definition of GS for a finite demand problem can be reused beyond this mission, but the dummy-firm construction and the one-sided D1′–D2′ predicates follow this paper's conventions.

Why the transfer is delicate

A strict-core allocation of a two-sided market controls coalitions containing a firm, while D2′ is expressed entirely through worker coalitions. The fictitious market has more firms than workers, which forces at least one firm to employ nobody. The proof must connect that observation to every firm's profit and then translate a one-sided improving coalition into a two-sided improvement. Individual rationality also has to preserve the paper's aggregate budget condition. Merely assigning each worker to a firm or showing nonnegative firm profits would leave these links unproved.

Formalization scope

Workers form an arbitrary finite type; the empty case is included. The fictitious firms have type Fin (m + 1), so their count is strictly greater than the worker count even when $m=0$. Salaries and output are real. In the fictitious market, every firm uses the same $v$, each worker's utility at every firm is $\mu^i(s)$, and reservation salary is zero, matching unemployment utility $\mu^i(0)$. The milestones retain arbitrary strictly increasing continuous functions $\mu^i$; Theorem 3 does not quantify over them because D1′ and D2′ compare salaries directly. Theorem 3's GS condition ranges over all real salary vectors, not a discrete salary grid.

Mathlib finite partitions contain nonempty parts. The paper permits empty indexed groups, but NFL makes them contribute zero output. The allocation model assigns every worker to one firm, and strict blocking allows any worker coalition, including the empty set, although strict improvement excludes that case. D1′ uses one total salary bound; a per-group bound would change the theorem. D2′ requires a strict gain in a worker's salary, not merely slack in the production budget. No vacuous regularity condition, fixed special technology, or restriction to a single worker is part of the mission goal.

Contributions are welcome on the finite partition interface, properties of profit-maximizing demand under GS, the zero-profit claim, and the transfer from fictitious firms to worker coalitions. The shared market and demand definitions are kept in their own module so they can be consolidated with the other missions of this paper.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, pp. 1483–1504. DOI: 10.2307/1913392.
• L. S. Shapley, Cores of convex games, International Journal of Game Theory 1, 1971, pp. 11–26. DOI: 10.1007/BF01753431.

Motivation

Labor markets match heterogeneous workers to heterogeneous firms, and the terms of each match — the salary — are negotiated. Kelso and Crawford (Econometrica 50 (1982)) studied such a market in which a firm may hire many workers, its output depends on the whole set it hires, and salaries are set worker by worker. Their model contains the marriage problem of Gale and Shapley (1962) and the assignment game of Shapley and Shubik (1971) as special cases, and its gross substitutes condition later became the central hypothesis of the theory of matching with contracts and of ascending auctions for indivisible goods (Hatfield and Milgrom, AER 2005; Gul and Stacchetti, JET 1999).

Markets of this kind usually have many stable outcomes, so which one arises depends on how the market is organized. Gale and Shapley showed that their deferred-acceptance procedure picks the stable matching that is best for the proposing side. Crawford and Knoer (Econometrica 1981) proved the analogue for one-to-one matching with money. Theorem 4 of Kelso and Crawford extends it to firms that hire many workers, under gross substitutes: the paper's salary-adjustment process, in which firms make offers, ends at the end of the strict core that favors the firms.

Setting

There are finitely many workers $i \in W$ and firms $j \in F$. Worker $i$ values working for firm $j$ at salary $s$ by $u^i(j; s)$, strictly increasing and continuous in $s$. Firm $j$ produces $y^j(C)$ when it hires the set $C$ of workers and earns the profit $\pi^j(C; s^j) = y^j(C) - \sum_{i\in C} s_{ij}$ at the salary vector $s^j$. The number $\sigma_{ij}$ is the starting permitted salary for $i$ at $j$; Section 2 initially defines it as a reservation salary, and Section 5 permits it to be perturbed. The paper's standing assumptions are (MP), $y^j(C\cup\{i\}) - y^j(C) - \sigma_{ij} \ge 0$ for $i \notin C$; (NFL), $y^j(\varnothing) = 0$; and (GS): if $C$ maximizes firm $j$'s profit at $s^j$ and salaries rise weakly to $\tilde s^j$, some profit-maximizing set at $\tilde s^j$ still contains every worker of $C$ whose salary did not change.

In a discrete market with unit $\delta > 0$, firm $j$ may offer worker $i$ only the salaries $\sigma_{ij} + k\delta$, $k \in \mathbb{N}$. An allocation assigns every worker $i$ to a firm $f(i)$ at a salary; $C^j$ is the set hired by $j$. It is individually rational if every worker gets at least $\sigma_{if(i)}$ and every firm a nonnegative profit. A firm and a set of workers at permitted salaries improve upon it if all of them are weakly better off and one of them strictly; they strictly improve upon it if all are strictly better off. Discrete strict core allocations (D2) admit no improving coalition, discrete core allocations (D3) no strictly improving one.

The salary-adjustment process (R1–R5) starts with permitted salaries $s_{ij}(0) = \sigma_{ij}$ and offers from every firm to every worker. In each round, each firm offers jobs to a profit-maximizing set at its current permitted salaries, repeating unrejected offers; each worker holds a favorite offer and rejects the others; a rejected firm's permitted salary for that worker rises by $\delta$. The process stops in a round with no rejections. A worker is (strictly) $s$-possible for firm $j$ if some discrete (strict) core allocation assigns him or her to $j$ at salary $s$. The no-ties conditions are (NTW): a worker who is $s_{ij}$-possible for $j$ is never indifferent between $(j, s_{ij})$ and any permitted salary at another firm; and (NTF): a firm is never indifferent between its profit in a discrete core allocation and the profit from another nonempty set of workers at permitted salaries.

Formalization targets

Goal: Theorem 4 (p. 1495)

Under regularity, (MP), (NFL), (GS) on the permitted salary vectors, (NTW) and (NTF): every run of the process stops at some round, and at every stopping round $T$ the resulting allocation $\phi$ is a discrete strict core allocation with

$$\pi^j(C^j_{A'}; s'^j) \le \pi^j(C^j_\phi; s^j(T)) \qquad \text{for every firm } j \text{ and every discrete strict core allocation } A'.$$

Milestones (proof of Theorem 4, p. 1495)

1. Every equilibrium of the process is a discrete strict core allocation.
2. No worker ever rejects a firm at a salary $s$ at which he or she is strictly $s$-possible for it.
3. For every strict core allocation $(f; s')$, every round $t$ and every worker $i$: $s_{if(i)}(t) \le s'_{if(i)}$.

Significance

Theorem 4 says that the outcome of a decentralized ascending process, in which firms make the offers, is not an arbitrary stable outcome but the one best for every firm simultaneously. This existence of a firm-optimal point of the strict core is itself a consequence. Its Corollary (uniqueness of the equilibrium, mission 5 of this series) and Theorem 5 (an entering firm helps every worker, a departing worker hurts every firm, also mission 5) are both proved from it.

The result has been proved on paper since 1982, and nothing of this paper was on Prove2Me before this series. The mission produces a machine-checked version of the paper's model, of the salary-adjustment process for every tie-breaking rule, and of the firm-optimality argument. The no-money analogue, Gale and Shapley's optimality theorem for college admissions, has a proved formalization on the platform (GS62CollegeAdmissions.PaperInterface.theorem2_applicant_optimality); it does not involve salaries and is credited, not reused.

The series has seven missions: 1 (Theorem 1, convergence to a discrete core allocation), 2 (Theorem 2, the continuous strict core), 3 (Theorem 3, one-sided markets), 4 (this mission), 5 (comparative statics, Theorem 5), 6 (Theorem 6, gross substitutes and returns to workers), 7 (the no-core example of Section 6). This mission does not depend on the others: it states its own copy of the model.

Difficulty

The process is defined for every tie-breaking rule of firms and workers, so the claim concerns an entire family of executions, each indexed by rounds and carrying offers, tentative acceptances and salaries. The firm-optimality statement compares the process outcome with every strict core allocation, objects defined by a nonexistence condition over all coalitions and permitted salaries. The step that does not follow from Theorem 1 alone is that rejections never occur at a strictly possible salary. That claim is about the entire history of a run, not about its final round, and it ties a property of the core to every intermediate rejection. Without the no-ties hypotheses the paper guarantees only that the process stops at a discrete core allocation (D3, Theorem 1).

Formalization scope

Workers and firms are arbitrary finite types, with at least one firm; salaries are real numbers; larger utility is better. A discrete market is given by the unit $\delta > 0$, and the permitted salaries are $\sigma_{ij} + \delta\mathbb{N}$ (the paper's unit is 1; Theorem 2 lets it shrink, so it is kept general). The starting salaries $\sigma_{ij}$ are data; the relation $u^i(j;\sigma_{ij}) = u^i(0;0)$ is not assumed, because Section 5 perturbs $\sigma_{ij}$ independently of $u^i(0;0)$ to obtain (NTW), and under that relation (NTW) typically fails in round 0. Allocations assign every worker to a firm. (GS) is imposed on the permitted salary vectors of the discrete market only.

Explicit readings of the paper's phrases:

• "converges to" means: every run stops at some round, and every stopping round yields the stated allocation;
• "any other strict core allocation" means any discrete strict core allocation of the same discrete market;
• "at least as good for every firm" is a weak profit inequality at every firm;
• (NTW) and (NTF) are about discrete core allocations (D3), as printed, and "any other non-empty set of workers" in (NTF) is read as a nonempty set different from $C^j$;
• a run of R1–R5 is any sequence of salaries, offers and tentative acceptances obeying the rules, with all ties broken arbitrarily; the statements cover every run.

Statements that quantify over runs would be empty if no run existed, and (NTW), (NTF) are hypotheses about the core that could in principle be contradictory; a sorry-free local check confirms all hypotheses on a market with one firm and one worker and exhibits a run that stops at a strict core allocation, so the goal is not vacuous. Trivializing readings — comparing with continuous strict core allocations, imposing (NTW)/(NTF) only on strict core allocations, or comparing a single firm — are excluded by the statement.

Infrastructure needed: the model, the run encoding, and lemmas about runs (salaries are monotone and stay on the grid, every worker always holds an offer, every run stops — Theorem 1). These are reusable for missions 1 and 5. Contributions to any milestone, and alternative proofs, are welcome.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job matching, coalition formation, and gross substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
• V. P. Crawford and E. M. Knoer, Job matching with heterogeneous firms and workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1912758
• D. Gale and L. S. Shapley, College admissions and the stability of marriage, American Mathematical Monthly 69(1), 1962, 9–15. https://doi.org/10.2307/2312726
• L. S. Shapley and M. Shubik, The assignment game I: The core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
• J. W. Hatfield and P. R. Milgrom, Matching with contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466
• F. Gul and E. Stacchetti, Walrasian equilibrium with gross substitutes, Journal of Economic Theory 87(1), 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531

Motivation

Linear programming, second-order cone programming and semidefinite programming are all instances of conic linear programming: minimize a linear function over the intersection of an affine subspace with a closed convex cone. Primal-dual interior-point methods solve these problems in polynomially many iterations and are the algorithms behind most conic solvers in practical use. Nesterov and Todd showed that the primal-dual path-following analysis known for linear programming extends verbatim to every cone that admits a self-scaled barrier, a class containing the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products (Nesterov & Todd 1997; Nesterov & Todd 1998).

Timeline. Kojima, Mizuno and Yoshise (1989) and Monteiro and Adler (1989) gave short-step primal-dual path-following methods for linear programming with an $O(\sqrt n \ln(1/\varepsilon))$ iteration bound. Mizuno, Todd and Ye (1993) added the predictor-corrector variant. Nesterov and Nemirovskii (1994) developed the general theory of self-concordant barriers. Nesterov and Todd (1997) introduced self-scaled barriers and scaling points; the 1998 paper analysed the short-step, adaptive-step and predictor-corrector methods for them. Güler (1996) identified self-scaled cones with symmetric (homogeneous self-dual) cones.

Setting

Let $E = \mathbb R^n$ with inner product $\langle\cdot,\cdot\rangle$, and let $K \subseteq E$ be a closed convex cone that is pointed and has nonempty interior; $K^* = \{s : \langle s, x\rangle \ge 0\ \forall x \in K\}$ is its dual cone. A linear map $A : \mathbb R^n \to \mathbb R^m$ (surjective), $b \in \mathbb R^m$ and $c \in \mathbb R^n$ define the primal problem $\min\{\langle c, x\rangle : Ax = b,\ x \in K\}$ and its dual $\max\{\langle b, y\rangle : A^*y + s = c,\ s \in K^*\}$. Strictly feasible points are $x \in S^0(P)$ ($x \in \operatorname{int} K$, $Ax = b$) and $(y, s) \in S^0(D)$ ($s \in \operatorname{int}K^*$, $A^*y + s = c$).

A $\nu$-self-concordant logarithmically homogeneous barrier $F$ for $K$ is a self-concordant convex function on $\operatorname{int} K$ that tends to $+\infty$ at the boundary, satisfies $(\langle F'(x), h\rangle)^2 \le \nu\langle F''(x)h, h\rangle$ and $F(\tau x) = F(x) - \nu\ln\tau$. Its conjugate is $F_*(s) = \sup_{x \in \operatorname{int}K}\{-\langle s, x\rangle - F(x)\}$. The barrier is self-scaled if $F''(w)x \in \operatorname{int}K^*$ and $F_*(F''(w)x) = F(x) - 2F(w) - \nu$ for all $w, x \in \operatorname{int}K$. For $x \in \operatorname{int}K$ and $s \in \operatorname{int}K^*$ the scaling point is the $w \in \operatorname{int}K$ with $F''(w)x = s$.

Local norms at $x \in \operatorname{int}K$ are $\|v\|_x = \langle F''(x)v, v\rangle^{1/2}$ for primal vectors and $\|u\|_x = \langle [F''(x)]^{-1}u, u\rangle^{1/2}$ for dual vectors; $|u|_x$ is the cone-induced (max-type) norm. With $\mu(x, s) = \langle s, x\rangle/\nu$ the proximity measures are

$$\lambda_2(x, s) = \Big\|\frac{s}{\mu(x,s)} + F'(x)\Big\|_x,\qquad \lambda_\infty(x, s) = \Big|\frac{s}{\mu(x,s)} + F'(x)\Big|_x,$$

and $\bar\lambda_2(x, s, \mu) = \|s/\mu + F'(x)\|_x$. The narrow neighbourhood is $N(\beta) = \{(x,y,s) \in S^0(P)\times S^0(D) : \lambda_2(x, s) \le \beta\}$.

The short step from $(x, y, s) \in N(\beta)$ targets $\mu_+ = (1 - \kappa/\sqrt\nu)\mu(x,s)$ and solves

$$F''(w)q_x + q_s = s + \mu_+F'(x),\qquad Aq_x = 0,\qquad A^*q_y + q_s = 0,$$

then sets $(x_+, y_+, s_+) = (x - q_x, y - q_y, s - q_s)$.

Formalization targets

Goal: Theorem 6.4

With $\delta = \lambda_\infty(x,s)$, $\epsilon = \lambda_2(x,s)$, $\epsilon_+ = \bar\lambda_2(x, s, \mu_+)$ and $\eta = \epsilon_+/(1-\delta) < 1$:

$$x_+ \in \operatorname{int}K,\quad s_+ \in \operatorname{int}K^*,\quad \mu(x_+, s_+) = \mu_+,\quad \lambda_2(x_+, s_+) = \bar\lambda_2(x_+, s_+, \mu_+) \le \frac{(2 + \delta - \kappa)(\epsilon + \kappa)^2}{(1-\delta)^2(1-\kappa)^3}.$$

The constant $\kappa \in (0,1)$ and $\beta \in (0,1)$ are free; no numerical choice is hard-coded.

Milestones

Theorem 3.6 (norms at neighbouring points), Lemma 3.13 and Corollary 3.14 (scaling-point Hessian versus the Hessians at $x$ and $s$), Lemma 6.2 (effect of decreasing $\mu$), (6.10) (the gap after the step), and Lemma 6.3 (size of the step, feasibility, norms at $x_+$).

Companion results

The Algorithm 6.1 invariant ($\beta = 1/10$, $\kappa = 1/15$: iterates stay in $N(1/10)$ while $\mu$ shrinks by $1 - (15\sqrt\nu)^{-1}$), Theorem 6.5 (the predictor step length $\alpha^* \ge (10\sqrt\nu)^{-1}$), and Lemma 6.1.

Significance

Theorem 6.4 is the one-step estimate behind the $O(\sqrt\nu\ln(\langle s_0, x_0\rangle/\zeta))$ iteration bound of the short-step method on every symmetric cone, and with it of the most widely used complexity bounds for semidefinite and second-order cone programming. The same estimate, with $\kappa = 0$, certifies the corrector step of the predictor-corrector method (Algorithm 6.3).

The results are proved in the paper; none is formalized. A Lean development would provide a machine-checked core of conic interior-point theory: the local-norm calculus of self-scaled barriers (Theorem 3.6, Lemma 3.13), which is reused across all the methods of the paper, and a verified complexity statement for an algorithm family used in practice. The companion mission on the functional-proximity method (Theorem 7.1 of the same paper) shares the setting.

Difficulty

The obvious argument expands $s_+ + \mu_+F'(x_+)$ and bounds each term by self-concordance. Generic self-concordance controls norms at a new point only under $\|x_+ - x\|_x < 1$ and gives constants that do not close the recursion with $\beta = 1/10$; it also says nothing about the dual side. The proof needs properties special to self-scaled barriers: the scaling point $w$ and the two-sided comparison of $F''(w)/\mu$ with $F''(x)$ (Lemma 3.13), norm comparisons under the weaker hypothesis $|x_+ - x|_x < 1$ (Theorem 3.6), and a third-derivative bound from Nesterov–Todd 1997. In Lean, none of the self-scaled barrier theory, conjugate barriers on cones, or local norms exists in Mathlib.

Formalization scope

$E$ is EuclideanSpace ℝ (Fin n) and $E^*$ is identified with $E$ through the inner product. Because the paper distinguishes primal and dual norms by the space of the argument, the formalization names them: lnorm G v u (same space as $v$) and dnorm G v u (other space, through the inverse Hessian), for $G = F$ or $G = F_*$; sigma C c u and absn C c u take the cone and the centre explicitly. The conjugate is a real supremum over $\operatorname{int}K$ and is only evaluated in $\operatorname{int}K^*$. $\lambda_2$, $\lambda_\infty$ use the first of their two printed forms.

Standing assumptions carried by every statement: $K$ proper, $F$ a $\nu$-self-scaled barrier, and $\nu \ge 1$ (a consequence of pointedness that the paper derives). The barrier definition adds positive definiteness of $F''$ on $\operatorname{int}K$, implied by the other conditions for a pointed cone. Theorem 6.4 adds $0 < \kappa < 1$ (the paper's "some fixed constant", forced by its proof) and the conclusion $x_+ \in \operatorname{int}K$, $s_+ \in \operatorname{int}K^*$ from Lemma 6.3. Assumptions (2.4)–(2.5) are implied by the strictly feasible starting point. In Theorem 3.6 the middle factors of (3.12) are corrected to $(1 - p_+)$ and $(1 + p_-)$; the printed ones fail for the half-line.

Search directions are any solution of their linear systems; their existence is not assumed. The goal assumes no bound from Lemmas 6.2–6.3 and no value of $\mu(x_+, s_+)$, so it cannot be discharged by restating its hypotheses.

Needed infrastructure: derivatives of logarithmically homogeneous functions ((2.7)–(2.10)), properties of the conjugate barrier ((2.12)–(2.16)), the existence and properties of scaling points (Nesterov–Todd 1997), and the local norm inequalities of self-concordant functions. These are reusable for any interior-point formalization; contributions of such lemmas are welcome.

Selected references

• Yu. E. Nesterov and M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM J. Optim. 8 (1998) 324–364. https://doi.org/10.1137/S1052623495290209
• Yu. E. Nesterov and M. J. Todd, Self-scaled barriers and interior-point methods for convex programming, Math. Oper. Res. 22 (1997) 1–42. https://doi.org/10.1287/moor.22.1.1
• Yu. Nesterov and A. Nemirovskii, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
• O. Güler, Barrier functions in interior point methods, Math. Oper. Res. 21 (1996) 860–885. https://doi.org/10.1287/moor.21.4.860
• M. Kojima, S. Mizuno and A. Yoshise, A primal-dual interior point algorithm for linear programming, in Progress in Mathematical Programming, Springer, 1989, 29–47. https://doi.org/10.1007/978-1-4613-9617-8_2
• S. Mizuno, M. J. Todd and Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Math. Oper. Res. 18 (1993) 964–981. https://doi.org/10.1287/moor.18.4.964

Motivation

Labour markets match workers to firms that hire teams: a firm's output depends on the whole set of workers it employs, while each worker holds one job. A salary agreement is stable when no firm and group of workers can renegotiate among themselves to the benefit of all of them. Shapley and Shubik (1971) showed that such stable outcomes exist when each firm hires at most one worker and utility is transferable; Crawford and Knoer (1981) extended this to general utilities, still one-to-one. Kelso and Crawford (1982) let firm size be endogenous and identified the condition under which existence survives: workers must be gross substitutes for every firm. Their condition later became the standard assumption for existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti, 1999) and the basis of matching with contracts (Hatfield and Milgrom, 2005).

This mission is the second of a seven-mission series on the paper: 1, the salary-adjustment process; 2, existence of a strict core with continuous salaries (this mission); 3, one-sided coalition formation; 4, the firm-optimal allocation; 5, comparative statics; 6, gross substitutes versus nonincreasing returns; 7, a market with no core. Each mission is self-contained. Nothing of this paper was on Prove2Me before this series.

Setting

There is a finite set $W$ of $m$ workers and a nonempty finite set $F$ of firms. Worker $i$'s utility of working for firm $j$ at salary $s\in\mathbb R$ is $u^i(j;s)$, strictly increasing and continuous in $s$. Firm $j$'s gross product when it hires the set $C\subseteq W$ is $y^j(C)$, and its profit at the salary vector $s^j=(s_{ij})_{i\in W}$ is

$$\pi^j(C;s^j)=y^j(C)-\sum_{i\in C}s_{ij}.$$

The reservation salary $\sigma_{ij}$ is defined by $u^i(j;\sigma_{ij})=u^i(0;0)$, worker $i$'s utility of unemployment. Section 2 of the paper assumes, for every firm $j$:

• (MP) $y^j(C\cup\{i\})-y^j(C)-\sigma_{ij}\ge0$ whenever $i\notin C$;
• (NFL) $y^j(\emptyset)=0$;
• (GS) if $C$ maximizes $\pi^j(\cdot\,;s^j)$ and $\tilde s^j\ge s^j$ componentwise, then some maximizer $\tilde C$ of $\pi^j(\cdot\,;\tilde s^j)$ contains every $i\in C$ with $\tilde s_{ij}=s_{ij}$.

An allocation assigns each worker $i$ to a firm $f(i)$ at salary $s_{if(i)}$; firm $j$ hires $C^j=\{i:f(i)=j\}$. It is individually rational (D1) if $s_{if(i)}\ge\sigma_{if(i)}$ and $\pi^j(C^j;s^j)\ge0$ for all $i,j$. A firm $j$, a set $C$ and salaries $r_{ij}$ improve upon it if $u^i(j;r_{ij})\ge u^i(f(i);s_{if(i)})$ for $i\in C$ and $\pi^j(C;r^j)\ge\pi^j(C^j;s^j)$, with at least one inequality strict; they strictly improve upon it if all are strict. A strict core allocation (D2) is an individually rational allocation no coalition improves upon; a core allocation (D3) is one no coalition strictly improves upon. In the continuous market coalitions may use any real salaries; in the discrete market of unit $\delta>0$ all salaries lie on the grids $\sigma_{ij}+\delta\mathbb N$.

Formalization targets

Goal: Theorem 2

Under regular utilities, (MP), (NFL), the reservation-salary relation and (GS) on all real salary vectors,

$$\exists\,(f;s)\ \text{individually rational that no firm–worker coalition can improve upon (D2).}$$

The goal fixes no grid, no constant and no particular technology.

Milestones, in the order of the paper's proof

1. Every discrete market has a core (p. 1490): for every $\delta>0$, if (GS) holds on grid salary vectors, a discrete core allocation (D3) exists.
2. The gains are bounded above zero (p. 1491, eqs. (8)–(11)): if the continuous market has no strict core allocation, there is $H>0$ such that every individually rational allocation admits a coalition that leaves its workers no worse off and raises its firm's profit by at least $H$.
3. A fine grid inherits the improvement (pp. 1491–1492): with such an $H$, every individually rational grid allocation of unit $0<\delta<H/(m+1)$ can be strictly improved upon in the discrete market.

Significance

Theorem 2 gives existence of a stable assignment of workers to firms with salaries, for arbitrary technologies under which workers are gross substitutes, without any convexity or divisibility of labour. Because the core and the competitive equilibrium coincide in this model when salaries are divisible (p. 1487), it is also an existence theorem for competitive equilibrium in a market with indivisible workers; the example of mission 7 shows that it fails without (GS). The Shapley–Shubik assignment game is the special case $u^i(j;s)=a_{ij}+s$, $y^j(C)=\sum_{i\in C}b_{ij}$ with at most one worker per firm.

The result has been proved since 1982; it has not been machine-checked. Prove2Me holds a formalization of the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core-existence theorem is a different model and is not yet proved, and Murota's gross-substitutes axioms for demand on $\mathbb Z^n$, which concern one price per good rather than firm-specific salary vectors over sets of workers. Neither supplies this market or Theorem 2.

Difficulty

Discrete core allocations exist at every unit $\delta$, so the natural first idea is to take a sequence of them as $\delta\to0$ and pass to a limit. A limit of discrete core allocations need only be a core allocation of the continuous market in the weak sense D3, and a coalition that improves upon the limit may need salaries off every grid; nothing in the discrete statements controls how much a coalition gains, so the blocking coalitions of the continuous market may vanish on the grids. The required control has to be uniform over all individually rational allocations, which form an infinite set, while each blocking comparison involves the utilities of several workers and a nonadditive technology. A second obstacle is in the paper's notation: the gain (8) uses the salary $\rho_{ij}$ with $u^i(j;\rho_{ij})=u^i[f(i);s_{if(i)}]$, which need not exist when $u^i(j;\cdot)$ is bounded.

Formalization scope

Workers and firms are arbitrary finite types; every theorem assumes at least one firm (the paper's $n\ge1$), since with no firm and some worker no allocation exists. Salaries, utilities, outputs and profits are real numbers. An allocation has no unemployment, as in D1. The reservation salaries $\sigma$ are data, and the paper's definition of $\sigma_{ij}$ enters as the hypothesis $u^i(j;\sigma_{ij})=u^i(k;\sigma_{ik})$; it is assumed on the goal and on milestones 2 and 3, where the discretization step needs every improving salary to be at least $\sigma_{ij}$. Milestone 1 assumes neither this relation nor continuous (GS). The standing assumptions of p. 1486, which Theorem 2's sentence does not repeat, are hypotheses of the goal.

Explicit readings of the paper's phrases: "continuous market" means coalitions may use any real salary; "bounded above zero" is one $H>0$ valid for every individually rational allocation, stated without $\rho_{ij}$ by quantifying over admissible coalition salaries; "the unit of measurement smaller than $H/(m+1)$" is $0<\delta<H/(m+1)$ with $m=|W|$ and the division in $\mathbb R$; the discrete market's salaries are $\sigma_{ij}+\delta k$, $k\in\mathbb N$, the paper's integer salaries starting at $\sigma_{ij}$ (R1, R4) with a general unit.

Trivializing formalizations are ruled out: the goal assumes (GS) on all real vectors rather than on one grid (a stronger theorem the paper does not prove), its conclusion is the strict core D2 rather than the weaker core D3, and its hypotheses are satisfiable (a one-worker, one-firm market satisfies all of them).

A complete development needs finite optimization over sets of workers, a compactness argument over the individually rational salary schedules of each assignment, and the existence of discrete core allocations (the existence form of Theorem 1, mission 1). Proofs of the milestones, of the equivalence of D2 and D3 in the continuous market, and lemmas on finite demand correspondences reusable across the series are welcome.

Selected references

• A. S. Kelso, Jr. and V. P. Crawford, Job Matching, Coalition Formation, and Gross Substitutes, Econometrica 50(6), 1982, 1483–1504. https://doi.org/10.2307/1913392
• V. P. Crawford and E. M. Knoer, Job Matching with Heterogeneous Firms and Workers, Econometrica 49(2), 1981, 437–450. https://doi.org/10.2307/1912751
• L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1, 1971, 111–130. https://doi.org/10.1007/BF01753437
• F. Gul and E. Stacchetti, Walrasian Equilibrium with Gross Substitutes, Journal of Economic Theory 87(1), 1999, 95–124. https://doi.org/10.1006/jeth.1999.2531
• J. W. Hatfield and P. R. Milgrom, Matching with Contracts, American Economic Review 95(4), 2005, 913–935. https://doi.org/10.1257/0002828054825466

Motivation

A retailer who restocks a product every period must pick an order-up-to level without knowing the demand distribution. When a period ends with an empty shelf, the retailer records only its sales, so the true demand above the stock level is censored. The classical newsvendor solution, the critical fractile of the demand distribution, cannot be computed. Huh and Rusmevichientong (Math. Oper. Res., 2009) treat this as an online convex optimization problem: the expected one-period cost is convex in the stock level, and its derivative can be estimated without bias from the censored observation alone. Their Adaptive Inventory Management (AIM) algorithm is a projected stochastic subgradient method in the style of Zinkevich (2003) and Flaxman, Kalai and McMahan (2005). Its average expected cost converges to the newsvendor cost at rate $O(1/\sqrt T)$.

That analysis assumes that the manager knows an upper bound $\bar y$ on the newsvendor quantity, and the algorithm projects onto $[0,\bar y]$. This mission formalizes §3.1 of the paper, which removes the assumption. The projection interval grows with time, and the regret bound is explicit in the unknown newsvendor quantity. Earlier adaptive schemes for censored newsvendor problems include Godfrey and Powell (2001) and Burnetas and Smith (2000).

Setting

Periods are $t = 1, 2, \dots$. Demands $D_1, D_2, \dots$ are i.i.d. copies of a nonnegative random variable $D$ with finite mean and distribution function $F$. Inventory is perishable: every period starts empty, so the stock level is exactly the order-up-to level. With holding cost $h > 0$ per unit left over and shortage cost $b > 0$ per unit of unmet demand, the expected one-period cost at level $y \ge 0$ is

$$Q(y) = h\,E[y-D]^+ + b\,E[D-y]^+ .$$

The newsvendor quantity is $y^{NV} = \inf\{y \ge 0 : F(y) \ge b/(b+h)\}$, the minimizer of $Q$.

Write $\bar B = \max\{b,h\}$ and $P_{[0,a]}(z) = \max\{\min\{z,a\},0\}$. After period $t$, the manager observes whether demand fell short of the stock level and forms the signal

$$H_t(y) = \begin{cases} h, & D_t < y,\\ -b, & D_t \ge y.\end{cases}$$

Fix $\delta \in (0, 1/2)$. The modified AIM algorithm starts from a level $\hat y^\delta_1 \in [0,1]$ and updates

$$\hat y^\delta_{t+1} = P_{[0,\,t^{\delta/2}]}\!\left(\hat y^\delta_t - \epsilon_t H_t(\hat y^\delta_t)\right), \qquad \epsilon_t = \frac{1}{\bar B\sqrt t}.$$

Neither the step size nor the projection interval uses any bound on $y^{NV}$. The level $\hat y^\delta_t$ depends only on $D_1, \dots, D_{t-1}$, and only through the censored observations.

Formalization targets

Goal: Theorem 7 (p. 11)

For every $\delta \in (0, 1/2)$ and every $T \ge 1$,

$$E\left[\frac1T\sum_{t=1}^T Q(\hat y^\delta_t)\right] - Q(y^{NV}) \le \max\{b,h\}\left[\frac{1}{T^{0.5-\delta}} + \frac{1}{T^{0.5}} + \frac{(y^{NV})^{1+2/\delta}}{T}\right].$$

The bound holds uniformly over all demand laws with finite mean. The price of not knowing $\bar y$ is the slower rate $T^{\delta - 1/2}$ and a transient term in which $y^{NV}$ enters polynomially.

Milestones (proof of Theorem 7, p. 12)

1. One-step inequality, the instance of Eq. (15) (Appendix A, p. 16) used in the proof. For each $t$ with $y^{NV} \le t^{\delta/2}$,

$$E[Q(\hat y^\delta_t) - Q(y^{NV})] \le \frac{E|\hat y^\delta_t - y^{NV}|^2}{2\epsilon_t} - \frac{E|\hat y^\delta_{t+1} - y^{NV}|^2}{2\epsilon_t} + \frac{\epsilon_t}{2} E|H_t(\hat y^\delta_t)|^2 .$$

2. Eq. (10): early rounds, where the projection interval has not yet reached $y^{NV}$:

$$E\Big[\sum_{1 \le t \le T,\ t < (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\,(y^{NV})^{1+2/\delta}.$$

3. Eq. (11): late rounds:

$$E\Big[\sum_{1 \le t \le T,\ t \ge (y^{NV})^{2/\delta}} \{Q(\hat y^\delta_t) - Q(y^{NV})\}\Big] \le \bar B\, T^{0.5+\delta} + \bar B\, T^{0.5}.$$

Significance

The result. Theorem 7 shows that a distribution-free, censored-data policy can be asymptotically optimal without any prior bound on the optimal stock level. The only inputs are $b$, $h$ and the tuning parameter $\delta$. The explicit constant separates two effects. A transient cost grows with $y^{NV}$ and vanishes like $1/T$. A steady-state rate $T^{\delta-1/2}$ approaches the known-bound rate $T^{-1/2}$ as $\delta \to 0$, at the cost of a larger transient. The expanding-projection device applies to other stochastic subgradient methods whose feasible region is unbounded.

Formalizing it. The theorem is proved in the paper, but as far as is known it has no machine-checked proof. The mission produces the modified algorithm as an explicit function of the demand path, the per-step stochastic gradient inequality with a time-varying projection, and the two-phase regret decomposition. The per-step inequality with a varying domain is reusable for other growing-domain online methods.

Difficulty

The standard projected-gradient analysis compares every iterate with a fixed minimizer in a fixed compact set, and it bounds the telescoping distance terms by the diameter of that set. Neither applies here. In the early rounds the projection interval does not contain $y^{NV}$, so the distance to $y^{NV}$ can grow from step to step. Once the interval contains $y^{NV}$, the diameter that controls the telescoping sum grows with $t$. The step sizes and the growing radii must be traded against each other through Abel summation. The bound on $E[H_t(\hat y^\delta_t)(\hat y^\delta_t - y^{NV})]$ needs the conditional-expectation argument that $H_t$ is an unbiased subgradient of $Q$ at a random point independent of $D_t$. Applying the known-bound theorem with $\bar y$ replaced by $T^{\delta/2}$ does not work, because the algorithm is not given $T$ and the projection radius changes at every step.

Formalization scope

• Demand: CappedBaseStock.DemandLaw (a probability law on $\mathbb R_{\ge 0}$ with finite and strictly positive mean) and the i.i.d. path demandPathLaw (Measure.infinitePi), from the published definition CappedBaseStock_Model. The path is zero-based: the paper's $D_t$ is coordinate $t-1$. The positive-mean field is not needed by Theorem 7. It excludes only $D = 0$ almost surely.
• $Q$ and $y^{NV}$: backorderCost and newsvendorLevel from the published definition LostSalesOrderUpTo.Asymptotic.Backorder. Real levels are passed through Real.toNNReal, and the levels involved are always nonnegative.
• The algorithm modAimTarget δ b h ŷ₁ d t is a deterministic recursion on the demand path, and expectations are Bochner integrals over the path measure. All integrands are bounded and measurable, so no non-integrability default enters.
• Explicit readings of the paper's loose phrases:
  • the first level, which the paper leaves unspecified, is assumed to satisfy $\hat y^\delta_1 \in [0,1]$; the theorem fails without it;
  • $0 < b$ and $0 < h$ are assumed;
  • the sums in (10) and (11) are restricted to $1 \le t \le T$;
  • when $y^{NV} = 0$, the sum in (11) starts at $t = 1$;
  • all powers are real powers, with $0^p = 0$ for $p > 0$;
  • "the manager does not know any upper bound" is not a hypothesis, because the algorithm uses none.
• Trivializing formalizations are ruled out. The statements concern the algorithm's own iterates, not an arbitrary sequence of levels. The constants are the printed ones. The hypotheses are satisfiable, for example with $\hat y^\delta_1 = 0$.
• Useful contributions:
  • convexity and Lipschitz continuity of $Q$ with constant $\max\{b,h\}$;
  • the subgradient identity $E[H_t(y)] = (b+h)F(y^-) - b$;
  • measurability and boundedness of the iterates;
  • independence of $D_t$ from $\hat y^\delta_t$ under the product measure;
  • the projected-step inequality.

Selected references

• W. T. Huh and P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1), 2009. https://doi.org/10.1287/moor.1080.0355
• M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
• A. D. Flaxman, A. T. Kalai and H. B. McMahan, Online Convex Optimization in the Bandit Setting: Gradient Descent without a Gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
• G. A. Godfrey and W. B. Powell, An Adaptive, Distribution-Free Algorithm for the Newsvendor Problem with Censored Demands, Management Science 47(8), 2001. https://doi.org/10.1287/mnsc.47.8.1101.10231
• A. N. Burnetas and C. E. Smith, Adaptive Ordering and Pricing for Perishable Products, Operations Research 48(3), 2000. https://doi.org/10.1287/opre.48.3.436.12437