Algorithmic Game Theory

Pricing with unit-demand consumers

A seller with $n$ distinct items faces $m$ consumers, each of whom wants at most one item. Choosing item prices to maximise revenue in this setting is the unit-demand envy-free pricing problem, introduced by Rusmevichientong and studied in algorithmic game theory and revenue management since the mid-2000s. Optimal prices are hard to compute in general, so the guarantees of simple pricing rules matter. The simplest such rule is uniform pricing: put one price $q$ on every item and choose $q$ to maximise revenue.

Aggarwal, Feder, Motwani and Zhu (ICALP 2004) and Guruswami, Hartline, Karlin, Kempe, Kenyon and McSherry (SODA 2005) analysed uniform pricing; in the min-buying model it recovers a $1/(1+\ln m)$ fraction of the optimum, a bound Berbeglia and Joret attribute to Aggarwal et al. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) observed that the min-buying problem is a special case of assortment optimisation under a regular discrete choice model, and that uniform pricing then coincides with the revenue-ordered assortments heuristic. Their general guarantee for that heuristic yields a second bound for uniform pricing, in terms of the spread of the valuations rather than the number of consumers. This mission formalizes that bound (Corollary 4.7) together with the reduction it rests on (Theorem 4.6).

Setting

Unit-demand min-pricing ($\mathrm{UDP}_{\min}$). There are items $[n]$ and consumers $[m]$, $m\ge 1$. Consumer $i$ is interested in a set $B_i\subseteq[n]$ and has a valuation $v_i>0$. Given a price assignment $p:[n]\to\mathbb R_{>0}$, consumer $i$ buys a cheapest item of $B_i$ if its price is at most $v_i$, and nothing otherwise. The seller's revenue is

$$\mathrm{rev}_{\mathrm{UDP}}(p)=\sum_{i:\ B_i\ne\emptyset,\ \min_{x\in B_i}p(x)\le v_i}\ \min_{x\in B_i}p(x),$$

the optimum is $\mathrm{OPT}_{\mathrm{UDP}}=\sup_{p>0}\mathrm{rev}_{\mathrm{UDP}}(p)$, and uniform pricing earns $\mathrm{UP}=\sup_{q>0}\mathrm{rev}_{\mathrm{UDP}}(q,\dots,q)$. Write $v_{\max}=v_m$ and $v_{\min}=v_1$ for the extreme valuations.

Regular choice models. A finite product set $\mathcal C$ carries choice probabilities $\mathcal P(x,S)$ for $x\in\mathcal C$, $S\subseteq\mathcal C$, with no-purchase probability $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular if (i) all probabilities are nonnegative, (ii) $\mathcal P(x,S)=0$ for $x\notin S$, (iii) $\sum_{x\in S}\mathcal P(x,S)\le1$, and (iv) $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$. With revenues $r:\mathcal C\to\mathbb R_{>0}$, an assortment earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)r(x)$ and $\mathrm{OPT}=\max_S\mathrm{rev}(S)$. If $r_1<\dots<r_k$ are the distinct revenues and $S_i=\{x: r(x)\ge r_i\}$, revenue-ordered assortments earn $\mathrm{RO}=\max_i\mathrm{rev}(S_i)$.

The reduction. From a $\mathrm{UDP}_{\min}$ instance the paper builds $\mathcal C=[n]\times\{v_1,\dots,v_m\}$, $r((x,v))=m\,v$, and $\mathcal P=\frac1m\sum_i\mathcal P_i$, where $\mathcal P_i$ spreads probability one over the set $Q_i(S)$ of pairs $(x,v)\in S$ with $x\in B_i$, $v\le v_i$ and $v$ minimal among the pairs of $S$ whose item lies in $B_i$.

Formalization targets

Goal: Corollary 4.7

$$\mathrm{OPT}_{\mathrm{UDP}}\ \le\ \Big(1+\ln\frac{v_{\max}}{v_{\min}}\Big)\cdot\mathrm{UP}.$$

The bound is the paper's "approximates the optimum revenue to within a factor of $1/(1+\ln\rho)$, $\rho:=v_m/v_1$", stated in product form.

Milestones

1. Lemma 4.5. Some optimal price assignment takes only valuations as prices; in particular $\mathrm{OPT}_{\mathrm{UDP}}$ is attained.
2. Regularity of the reduction's choice model (proof of Theorem 4.6, pp. 17–18).
3. Assortments to prices: $\mathrm{rev}(S)=\mathrm{rev}_{\mathrm{UDP}}(p_S)$ with $p_S(x)=\min\{v:(x,v)\in S\}$ (p. 19).
4. Prices to assortments: for valuation-valued $p$, $\mathrm{rev}(S_p)=\mathrm{rev}_{\mathrm{UDP}}(p)$ with $S_p=\{(x,v): v\ge p(x)\}$ (p. 19).
5. Theorem 4.6 for the explicit instance: regularity, positive revenues, equal optima, and the two-way correspondence between threshold sets and uniform valuation prices.
6. Theorem 3.2 for an arbitrary regular model:

$$\mathrm{OPT}\le\Big(\sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\Big)\mathrm{RO},\qquad \sum_{i=1}^k\frac{r_i-r_{i-1}}{r_i}\le 1+\ln\frac{r_k}{r_1},\qquad r_0:=0.$$

Significance

The corollary gives a uniform-pricing guarantee that is independent of the number of consumers and items: when valuations lie within a factor $\rho$ of each other, a single price recovers a $1/(1+\ln\rho)$ fraction of the optimum, which improves on $1/(1+\ln m)$ whenever $\rho<m$. More broadly, Theorem 4.6 places $\mathrm{UDP}_{\min}$ inside the class of regular choice models, so every guarantee proved for revenue-ordered assortments under regularity transfers to uniform pricing.

All results here are proved in the paper. Nothing in this mission is formalized elsewhere as far as a search of the platform shows: there is no regular choice model, no $\mathrm{UDP}_{\min}$ problem and no revenue-ordered guarantee on Prove2Me. The mission produces the reduction as reusable infrastructure, a machine-checked version of the paper's Lemma 4.5 (whose appendix proof is an informal repair argument), and the first formal guarantee for uniform pricing.

Difficulty

The reduction is where the work sits. Regularity hinges on the no-purchase case of axiom (iv): enlarging an assortment can only make $Q_i$ nonempty, never empty, and this must be checked for the specific sets $Q_i(S)$ whose definition depends on the whole of $S$. The revenue identities require tracking the minimum over $B_i$ of a price function obtained from an assortment, including items absent from $S$, which receive the paper's "$+\infty$" price. Lemma 4.5 is needed to make the optimum of the uncountable pricing problem coincide with that of a finite assortment problem, and the statement is about a supremum over a continuum of price vectors whose attainment is not obvious. Theorem 3.2 has to relate the optimum to threshold sets of an arbitrary regular model, where products may share revenues and the optimal assortment need not be a threshold set.

The naive route of comparing uniform pricing to the optimum directly, consumer by consumer, does not give a bound in terms of $v_m/v_1$; the reduction to a regular model is what supplies it.

Formalization scope

• Items and consumers are finite types X and M, with Nonempty M ($m\ge1$). Valuations satisfy $v_i>0$ as a field of the instance; the paper says "non-negative", but its reduction ($r=m\,v>0$) and its ratio $v_m/v_1$ need positivity.
• A consumer with $B_i=\emptyset$ pays $0$. Ties among cheapest items do not affect payments, so payments are defined directly.
• $\mathrm{OPT}_{\mathrm{UDP}}$ and $\mathrm{UP}$ are real suprema over positive price assignments and positive uniform prices; both index sets are nonempty and the revenues are bounded by $\sum_i v_i$. Uniform pricing ranges over all $q>0$, not only valuations.
• The no-purchase option is not a product: it is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$, and regularity includes axiom (iv) for it. OPT is a maximum over all Finset C; RO is a maximum over the $k$ threshold sets only. Distinct revenues are sorted 0-based (Fin k), with $r_0=0$ handled as a separate case.
• The paper's $+\infty$ price for $p_S$ is the real $1+\sum_i v_i$, which exceeds every valuation, as its Remark on p. 18 allows. The valuation set collapses equal valuations.
• Approximation factors are in product form, $\mathrm{OPT}\le D\cdot\mathrm{RO}$; $\ln$ is Real.log applied to ratios $\ge1$.
• Trivializing readings are excluded: Theorem 4.6 is stated for the explicit instance of its proof, not as the bare existence of a regular instance with the same optimum (a single product of revenue $\mathrm{OPT}_{\mathrm{UDP}}$ would satisfy that); $\mathrm{OPT}_{\mathrm{UDP}}$ ranges over all positive price assignments, not uniform ones; valuations are positive, so no logarithm takes a junk value.
• Theorem 3.2 is restated here for this mission's copy of the regular model; it is also the goal of mission I of this series. Reusable pieces: the regular choice model and revenue-ordered value, and the $\mathrm{UDP}_{\min}$ model. Contributions of any milestone, and alternative proofs of Lemma 4.5, are welcome.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; Algorithmica 82 (2020). https://arxiv.org/abs/1606.01371
• G. Aggarwal, T. Feder, R. Motwani and A. Zhu, Algorithms for multi-product pricing, ICALP 2004. https://doi.org/10.1007/978-3-540-27836-8_8
• V. Guruswami, J. D. Hartline, A. R. Karlin, D. Kempe, C. Kenyon and F. McSherry, On profit-maximizing envy-free pricing, SODA 2005. https://dl.acm.org/doi/10.5555/1070432.1070598
• P. Rusmevichientong, B. Van Roy and P. W. Glynn, A nonparametric approach to multiproduct pricing, Operations Research 54(1), 2006. https://doi.org/10.1287/opre.1050.0236
• A. Aouad, V. Farias, R. Levi and D. Segev, The approximability of assortment optimization under ranking preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1754

Motivation

A minimax theorem asserts that for a real function $f(\mu,\nu)$ of two variables the order of optimization does not matter:

$$\sup_{\mu}\inf_{\nu} f(\mu,\nu)=\inf_{\nu}\sup_{\mu} f(\mu,\nu).$$

In game theory it says that a two-person zero-sum game has a value; in optimization it is the engine behind Lagrangian duality, robust optimization (exchanging the decision and the adversary) and distributionally robust and online-learning bounds, where a worst case over a family of distributions is exchanged with a minimization over decisions.

Most minimax theorems require linear structure: $f$ concave in $\mu$ and convex in $\nu$ on convex sets. K. Fan observed that a much weaker, purely order-theoretic condition suffices, which he called concavelike and convexlike, and which makes sense on sets with no linear structure at all. This is the setting needed when the strategy sets are, for instance, sets of stopping times, of measurable policies, or of combinatorial objects whose mixtures are only "dominated" by another member of the set.

Timeline:

• 1928 — J. von Neumann proves the minimax theorem for bilinear payoffs on simplices (finite matrix games).
• 1952 — H. Kneser proves it for $f$ concave-convex on a compact convex set and a convex set, with $f$ upper semicontinuous in the compact variable (Kneser, C. R. Acad. Sci. Paris 234, 1952; reference [6] of Sion's paper).
• 1953 — K. Fan replaces concavity-convexity by concavelikeness-convexlikeness and removes the linear structure (Fan 1953).
• 1958 — M. Sion, in On general minimax theorems (Sion 1958), proves the quasi-concave-convex minimax theorem and, in §4, re-derives the Kneser–Fan theorem from a finite-reduction criterion (his Theorems 4.1, 4.1′, 4.2, 4.2′).

Setting

Let $M$ and $N$ be arbitrary sets and $f:M\times N\to\mathbb R$ a real-valued function; $\mu\in M$ is the maximizing variable and $\nu\in N$ the minimizing one.

• $f$ is concavelike in $M$ if for all $\mu_1,\mu_2\in M$ and $0\le t\le1$ there is one $\mu\in M$ with $t f(\mu_1,\nu)+(1-t)f(\mu_2,\nu)\le f(\mu,\nu)$ for every $\nu\in N$.
• $f$ is convexlike in $N$ if for all $\nu_1,\nu_2\in N$ and $0\le t\le1$ there is one $\nu\in N$ with $t f(\mu,\nu_1)+(1-t)f(\mu,\nu_2)\ge f(\mu,\nu)$ for every $\mu\in M$.
• $f$ is concave-convexlike if it is both.

In each definition the witness depends only on the two given points and on $t$, never on the point of the other space. The two values compared are the extended reals

$$\sup\inf f=\sup_{\mu\in M}\inf_{\nu\in N}f(\mu,\nu),\qquad \inf\sup f=\inf_{\nu\in N}\sup_{\mu\in M}f(\mu,\nu),$$

which may be $\pm\infty$. In the Lean development these are Concavelike f, Convexlike f, ConcaveConvexlike f, supInf f and infSup f in the namespace SionMinimax.KneserFan. The inequality $\sup\inf f\le\inf\sup f$ always holds; the theorems assert the reverse.

Formalization targets

Goal: the Kneser–Fan theorem (Theorem 4.2, p. 175)

If $M$ is a compact topological space, $f$ is concave-convexlike, and $\mu\mapsto f(\mu,\nu)$ is upper semicontinuous for each $\nu\in N$, then

$$\sup\inf f=\inf\sup f.$$

No structure on $N$ and no linear structure on $M$ are assumed.

Milestones

• Theorem 4.1′ (p. 175): if $f$ is concave-convexlike and for every real $c>\sup\inf f$ there is a finite $Y\subset N$ such that every $\mu\in M$ has some $y\in Y$ with $f(\mu,y)<c$, then $\sup\inf f=\inf\sup f$.
• Theorem 4.1 (p. 175): the dual criterion — for every real $c<\inf\sup f$ a finite $X\subset M$ such that every $\nu\in N$ has some $x\in X$ with $f(x,\nu)>c$.
• Theorem 4.2′ (p. 175): the dual of the goal — $N$ compact and $f(\mu,\cdot)$ lower semicontinuous for each $\mu$.

The paper itself states that 4.2 is a special case of 4.1′, which in turn follows from the finite-dimensional minimax theorem. Sion's own minimax theorem (Theorem 3.4 and its Corollary) is already formalized on the platform as FamousTheorems.sion_minimax_theorem and is included in the mission as a reference item.

Significance

The Kneser–Fan theorem is the standard minimax theorem for settings without a natural linear structure. Its finite-reduction form (4.1, 4.1′) isolates the only place where topology enters: compactness and semicontinuity are used solely to replace $N$ (or $M$) by a finite set, after which the argument is finite-dimensional. Statements of this kind are used to exchange the order of optimization in robust and distributionally robust optimization, in statistical decision theory (existence of least favourable priors, Wald's complete-class theorems) and in learning theory, where the adversary's set is a space of distributions and the learner's set is a space of hypotheses with no convex parametrization.

The theorem is classical and fully proved in the literature. No machine-checked proof of it is known in Mathlib or on the platform: Mathlib contains Sion's quasi-concave-convex theorem (Topology/Sion.lean) and the platform has the bilinear and quasi-convex cases, but neither covers concavelike-convexlike functions, which are independent of quasi-concave-convex ones. This mission produces machine-checked versions of all four §4 statements in the extended reals, including the degenerate cases where values are infinite.

Difficulty

The obvious reduction, "replace $M$ by its convex hull and apply a linear minimax theorem", is unavailable: $M$ and $N$ are bare sets, so there is no convex hull and no mixed strategy to form. Concavelikeness only promises that a mixture of two strategies is dominated by some third strategy, and this has to be iterated to finite mixtures and combined with a separation argument in $\mathbb R^Y$ for a finite $Y$.

The second difficulty is bookkeeping: the minimax values live in $[-\infty,+\infty]$, the threshold $c$ is real, and $f$ may be unbounded, so every step comparing a real $c$ with $\sup\inf f$ or $\inf\sup f$ must handle infinite values; a real-valued supremum would silently replace them by $0$.

Formalization scope

• $M$, $N$ are arbitrary Lean types and $f : M\to N\to\mathbb R$. For Theorem 4.2 the type $M$ carries an arbitrary topology with CompactSpace M; for 4.2′, $N$ carries one with CompactSpace N. No Hausdorff, metric or linear structure is assumed.
• "Upper (lower) semi-continuous in $\mu$ for each $\nu$" is Mathlib's UpperSemicontinuous (fun μ => f μ ν) (resp. LowerSemicontinuous (fun ν => f μ ν)) on the whole compact space.
• $\sup\inf f$ and $\inf\sup f$ are EReal-valued (⨆ μ, ⨅ ν, (f μ ν : EReal) and its dual); the threshold $c$ in 4.1, 4.1′ is a real number compared through the coercion; the finite sets are Finsets chosen after $c$.
• Added reading. Every statement assumes Nonempty M ∨ Nonempty N. When $M=N=\varnothing$ all printed hypotheses hold vacuously (take $X=\varnothing$ or $Y=\varnothing$), yet $\sup\inf f=\sup\varnothing=-\infty$ and $\inf\sup f=\inf\varnothing=+\infty$, so the printed statements fail only in that corner. When exactly one of the sets is empty both sides coincide and that case is kept. No printed slip is corrected; the milestone texts are verbatim.
• Ruled out. The concavelike/convexlike witnesses are chosen before the universally quantified point of the other space; reversing the quantifiers would make every function with pointwise maximizers concavelike and the theorems false. The definitions contain no compactness or finite-cover property, and there is no linear structure through which concavity could be substituted for concavelikeness.
• Infrastructure. A complete development needs the extension of concavelikeness to finite convex combinations, a finite-dimensional separation (or a finite minimax) lemma for $\mathbb R^Y$, and lemmas on EReal suprema of real-valued families; these are reusable for any minimax result without linear structure. Contributions proving the milestones independently, or deriving 4.1′ from the referenced Sion theorem by embedding into a simplex, are welcome.

Selected references

• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1), 171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171
• K. Fan, Minimax theorems, Proceedings of the National Academy of Sciences 39, 42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
• H. Kneser, Sur un théorème fondamental de la théorie des jeux, Comptes Rendus de l'Académie des Sciences Paris 234, 2418–2420, 1952 (cited as [6] in Sion 1958, https://doi.org/10.2140/pjm.1958.8.171).
• H. Nikaidô, On von Neumann's minimax theorem, Pacific Journal of Mathematics 4, 65–72, 1954. https://doi.org/10.2140/pjm.1954.4.65

Motivation

A minimax theorem asserts that, for a function $f(\mu, \nu)$ of two variables,

$$\sup_{\mu \in M} \inf_{\nu \in N} f(\mu, \nu) = \inf_{\nu \in N} \sup_{\mu \in M} f(\mu, \nu).$$

Such equalities are the basis of zero-sum game theory, of Lagrangian duality in optimization, of robust optimization, and of minimax lower bounds in statistics and online learning. Maurice Sion's 1958 paper On general minimax theorems proved the version most often cited today: $M$ and $N$ convex subsets of topological vector spaces, one of them compact, $f$ quasi-concave and upper semicontinuous in $\mu$, quasi-convex and lower semicontinuous in $\nu$.

Sion's theorem itself is already machine-checked: Mathlib's Sion.minimax proves it, following the elementary argument of Komiya (1988), and the platform holds it as FamousTheorems.sion_minimax_theorem. Sion's own proof is different. It runs through an open-cover form of the Knaster–Kuratowski–Mazurkiewicz (KKM) theorem, a Helly-type fact about $n+1$ points in low dimension, and a lemma about minimal finite covers (Lemma 3.3). That route has not been formalized. This mission formalizes its ingredients, with Lemma 3.3 as the goal.

Timeline:

• 1928: von Neumann proves the minimax theorem for bilinear payoffs on simplices (mixed strategies of matrix games).
• 1929: Knaster, Kuratowski and Mazurkiewicz prove the KKM covering theorem for closed sets.
• 1952–1953: Kneser and Fan extend the minimax theorem to concave-convex and concavelike-convexlike functions on compact sets.
• 1958: Sion proves the quasi-concave-convex version with semicontinuity, by the KKM route.
• 1988: Komiya gives an elementary proof avoiding KKM; it is the proof formalized in Mathlib.

Setting

Let $E$ be a real topological vector space: a real vector space with a topology for which addition and scalar multiplication are continuous. A set $M \subseteq E$ is convex if it contains the segment between any two of its points. The convex hull $\ulcorner X \urcorner$ of a set $X$ is the smallest convex set containing it.

A real function $g$ on a convex set $M$ is quasi-concave on $M$ if every superlevel set $\{\mu \in M : g(\mu) \ge r\}$ is convex, and quasi-convex if every sublevel set $\{\mu \in M : g(\mu) \le r\}$ is convex. It is upper semicontinuous (u.s.c.) on $M$ if every strict sublevel set $\{\mu \in M : g(\mu) < r\}$ is open in the topology $M$ inherits from $E$; lower semicontinuous (l.s.c.) is the mirror notion.

Let $Y$ be a finite set, $c$ a real number, and $f$ a real function on $M \times Y$. Say that $Y$ has property P if for each $\mu \in M$ there is a $y \in Y$ with $f(\mu, y) < c$, and that $Y$ is minimal for P if no proper subset of $Y$ has P.

An $n$-dimensional simplex with vertices $a_0, \dots, a_n$ is the convex hull of $n+1$ affinely independent points.

Formalization targets

Goal: Lemma 3.3 (p. 173)

Let $M \subseteq E$ be nonempty and convex, $Y$ finite, and $f(\cdot, y)$ quasi-concave and u.s.c. on $M$ for each $y \in Y$. If $Y$ is minimal for P, then

$$\exists\, \mu_0 \in M \;\; \forall y \in Y: \quad f(\mu_0, y) < c.$$

The lemma makes no compactness or finite-dimensionality assumption on $M$; that generality is what lets Sion apply it on the convex hull of a finite set inside an arbitrary topological vector space.

Milestones

1. Theorem 3.2 (p. 173). If $\mathfrak A = \{a_0, \dots, a_n\}$ are $n+1$ points in a real vector space of dimension $k < n$, then $\bigcap_{i=0}^n \ulcorner \mathfrak A - \{a_i\} \urcorner \ne \emptyset$.
2. Theorem 3.1 (p. 173). If $S$ is an $n$-simplex with vertices $a_0, \dots, a_n$ and $A_0, \dots, A_n$ are open in the ambient space, $S \subseteq \bigcup_i A_i$, each $S - A_i$ is convex, and $a_i \notin A_j$ for $i \ne j$, then $\bigcap_{i} A_i \neq \emptyset$.
3. Lemma 3.3′ (p. 173). The dual of the goal: quasi-convex, l.s.c. in the second variable, with $>$ in place of $<$.
4. Remark 3.6 (p. 174). The explicit function on $[0,1]^2$, quasi-concave-convex and l.s.c. in $\nu$ but not u.s.c. in $\mu$, with $\sup\inf f = 0 < 1 = \inf\sup f$.

Sion's Theorem 3.4 and the Corollary on p. 174 (the minimax theorem) enter the mission as the existing, proved platform item FamousTheorems.sion_minimax_theorem.

Significance

Lemma 3.3 is a finite, one-sided statement that already contains the full strength of the quasi-concave case: a finite family of "threats" $y \in Y$, none of which can be dropped, can be beaten simultaneously by one point $\mu_0$. On p. 174 Sion derives the minimax theorem from Lemma 3.3 and Lemma 3.3′ by reducing open covers to minimal finite ones, alternately on each side. Theorem 3.1 is an open-set KKM theorem with a convexity condition on complements, a covering principle of independent use in fixed-point theory and equilibrium existence. Remark 3.6 shows that the semicontinuity hypotheses are not decorative.

On the formal side, the minimax theorem is proved in Mathlib by another route, so nothing in this mission is needed to know that Sion's theorem is true. What the mission adds is the infrastructure of the original proof: a KKM-type theorem (absent from Mathlib and from the platform), a Helly-type statement about $n+1$ points, and the minimal-cover lemma. None of these has a machine-checked proof today. A formalized open KKM theorem is reusable for Fan's lemma, for Gale–Nikaido–Debreu type existence results and for other covering arguments.

Difficulty

The obvious approach to Lemma 3.3 is induction on $|Y|$, using quasi-concavity to combine points that are good for subfamilies. It fails because quasi-concavity gives control over superlevel sets $\{f \ge c\}$ only, so the union of two "bad" sets is not controlled, and nothing forces two partial witnesses to have a common improvement on the segment between them. The lemma is genuinely topological: without upper semicontinuity it is false (Remark 3.6 exhibits the resulting failure of the minimax equality).

The topological content sits in Theorem 3.1. Neither Mathlib nor the platform has a KKM theorem (the platform has Brouwer's fixed-point theorem), and the passage from the classical closed-set KKM theorem to the open-set form, and from a simplex inside a possibly non-Hausdorff topological vector space to the standard simplex, both need care: the topology induced on a finite-dimensional subspace need not be the Euclidean one.

Formalization scope

• The ambient space is a real topological vector space: [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E], the class of Mathlib's Sion file. No Hausdorff or finite-dimensionality assumption is made. The paper never names the ambient space; "convex set" is read as a convex subset of such a space.
• Quasi-concavity, quasi-convexity and semicontinuity are Mathlib's QuasiconcaveOn, QuasiconvexOn, UpperSemicontinuousOn, LowerSemicontinuousOn, all relative to the set $M$ or $N$.
• $f$ is typed $E \to \iota \to \mathbb R$ (or $\iota \to E \to \mathbb R$) and $Y$ is a Finset ι; values off $M \times Y$ are irrelevant. Minimality is "no strict sub-Finset has property P".
• Added hypothesis $M \ne \emptyset$ in Lemma 3.3 and $N \neq \emptyset$ in Lemma 3.3′: with $M = Y = \emptyset$ the hypotheses hold vacuously and the conclusion fails.
• Theorem 3.1 uses the page's ambient openness hypothesis and nonempty intersection conclusion. In the application to Lemma 3.3, relatively open strict sublevel sets on $M$ must be represented by ambient open sets before restricting to the simplex.
• Theorem 3.2 takes the points as an injective family (encoding "$n+1$ points") and $\mathfrak A - \{a_i\}$ as a set difference; dimension is linear dimension (Module.finrank).
• Remark 3.6 formalizes only the checkable claims about the example, with $\sup\inf$ and $\inf\sup$ over the subtype $[0,1]$ in EReal; "cannot be removed nor appreciably weakened" is informal and omitted.
• Trivializing formalizations are ruled out: minimality is not defined in terms of the conclusion, and $M$ is neither finite-dimensional nor compact.

Contributions welcome: a formal KKM theorem (closed and open versions), Theorem 3.2 from Mathlib's Convex.helly_theorem, and proofs of the milestones in any order.

Selected references

• M. Sion, On general minimax theorems, Pacific Journal of Mathematics 8(1), 171–176, 1958. https://doi.org/10.2140/pjm.1958.8.171
• B. Knaster, C. Kuratowski, S. Mazurkiewicz, Ein Beweis des Fixpunktsatzes für n-dimensionale Simplexe, Fundamenta Mathematicae 14, 132–137, 1929. https://doi.org/10.4064/fm-14-1-132-137
• K. Fan, Minimax theorems, Proceedings of the National Academy of Sciences 39(1), 42–47, 1953. https://doi.org/10.1073/pnas.39.1.42
• H. Kneser, Sur un théorème fondamental de la théorie des jeux, Comptes Rendus de l'Académie des Sciences 234, 2418–2420, 1952.
• H. Komiya, Elementary proof for Sion's minimax theorem, Kodai Mathematical Journal 11(1), 5–7, 1988. https://doi.org/10.2996/kmj/1138038812
• J. von Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen 100, 295–320, 1928. https://doi.org/10.1007/BF01448847

Motivation

Markets for indivisible goods, in which each participant owns one unit and wants one unit (houses, kidneys in paired donation, dormitory rooms, school seats), cannot be analysed with the convexity assumptions of classical general equilibrium theory. Shapley and Scarf (1974) introduced the housing market to ask whether the two central solution concepts of exchange economies survive indivisibility: the core (allocations no coalition can improve upon by trading among itself) and competitive equilibrium (allocations supported by prices at which every trader optimizes within his budget). Their paper (doi:10.1016/0304-4068(74)90033-0) gives two proofs that the core is nonempty. The first (Section 4) shows that the associated game without side payments is balanced and invokes Scarf's theorem; that is the companion mission of this series. The second (Section 6) is a constructive argument the authors attribute to David Gale, the top trading cycles method, which also produces competitive prices. This mission formalizes the second.

Timeline.

• 1967: Scarf proves that balanced games without side payments have nonempty cores (doi:10.2307/1909383).
• 1974: Shapley and Scarf define the housing market, prove that it has a nonempty core by both arguments, and give Gale's top-trading-cycle construction with competitive prices, allowing indifferences.
• 1977: Roth and Postlewaite show that with strict preferences the competitive allocation is unique and is the unique allocation in the strong core (doi:10.1016/0304-4068(77)90004-0).
• 1982: Roth shows the top-trading-cycles mechanism is strategy-proof under strict preferences (doi:10.1016/0165-1765(82)90003-9).
• 2003: Abdulkadiroğlu and Sönmez adapt top trading cycles to school choice (doi:10.1257/000282803322157061).

Setting

A finite set $N$ of traders each brings one indivisible good; "item $j$" is the good of trader $j$. Preferences are a real matrix $A = (a_{ij})_{i,j\in N}$: trader $i$ prefers item $j$ to item $k$ when $a_{ij} > a_{ik}$ and is indifferent when $a_{ij} = a_{ik}$. Ties are allowed, and only comparisons matter.

An allocation is a bijection $\sigma : N\to N$; trader $i$ receives item $\sigma(i)$. For a coalition $S$, an $S$-permutation $\tau$ reshuffles the items of $S$ among the members of $S$. The allocation $\sigma$ is a core allocation if there is no nonempty $S$ and $S$-permutation $\tau$ with $a_{i\tau(i)} > a_{i\sigma(i)}$ for every $i \in S$.

Prices $\mathrm{price}: N \to \mathbb R$ are competitive for $\sigma$ if each trader $i$, selling his own item for $\mathrm{price}(i)$, can afford $\sigma(i)$, i.e. $\mathrm{price}(\sigma(i)) \le \mathrm{price}(i)$, and no item $k$ with $\mathrm{price}(k) \le \mathrm{price}(i)$ is better for him than $\sigma(i)$.

For $R \subseteq N$, a top trading cycle for $R$ is a nonempty $S \subseteq R$ whose members can be arranged in a cycle $i_1 \to i_2 \to \cdots \to i_s \to i_1$ so that each $i_r$ likes the good of $i_{r+1}$ at least as well as any other good in $R$. A top-trading-cycle partition is

$$N = S^1 \cup S^2 \cup \cdots \cup S^p,$$

with $S^1$ a top trading cycle for $N$ and each $S^j$ a top trading cycle for $N - (S^1\cup\cdots\cup S^{j-1})$. In Lean the partition carries stage : N → Fin p and the successor map next : N → N.

Formalization targets

Goal: Section 6, assertions (1) and (2), p. 114

For every market $A$ and every top-trading-cycle partition with successor map $\mathrm{next}$, the allocation $i \mapsto \mathrm{next}(i)$ is a core allocation, and for every choice of prices

$$\pi^1 > \pi^2 > \cdots > \pi^p > 0$$

on the goods of $S^1,\dots,S^p$ it is competitive. The paper asserts that "a set of competitive prices exists"; its argument works for every such choice, and the goal states that.

Milestones (Section 6, p. 114)

1. Every nonempty $R\subseteq N$ has a top trading cycle.
2. A top-trading-cycle partition of $N$ exists (so the goal is not vacuous and every market has a competitive core allocation).
3. If $j$ is the first index with $S \cap S^j \ne \emptyset$ and $i \in S\cap S^j$, then $a_{ik} \le a_{i\,\mathrm{next}(i)}$ for all $k \in S$.
4. Under the prices $\pi^{\mathrm{stage}(k)}$, the successor's item costs the same as one's own, and every affordable item lies in one's own cycle or a later one.

Example (Section 7, pp. 115–116)

For the matrix $\begin{pmatrix}0&1&2\\1&0&-1\\-1&1&0\end{pmatrix}$ the unique competitive payoff is $(2,1,1)$ at equal prices, while the allocation with payoff $(1,1,0)$ is a core allocation that is competitive at no prices.

Significance

The result gives the existence of a core allocation of every housing market by an explicit construction, and shows that this allocation is competitive, so the competitive solution is nonempty even though goods are indivisible and preferences may have ties. The Section 7 example shows that the inclusion of competitive allocations in the core is strict in general. Under strict preferences, the outcome of the construction is the basis of the matching-market literature: uniqueness of the strong core (Roth–Postlewaite), strategy-proofness (Roth), and the school-choice and kidney-exchange mechanisms built on top trading cycles.

The mathematics is classical and proved. The formalization adds a machine-checked statement of the weak-preference version with the paper's strict blocking notion and its price argument, which existing formal developments do not cover. The closest platform items are AGT.house_core_unique, the strict-preference refinement (Roth–Postlewaite: with strict preferences and weak blocking the core is exactly one allocation), and the school-choice items SchoolChoice.TTC.*. Neither is this statement: the first assumes strict total orders and a different blocking notion, under which the core can be empty once ties are allowed, and says nothing about prices; the second concerns another model with priorities.

Difficulty

Each step is short on paper; the work is in the bookkeeping. The cycle allocation must be shown to be a bijection of $N$ from the stage-by-stage cycle structure; the "chain of best-liked goods that eventually must come back to some earlier element" must be turned into a cycle whose members each get a best good in $R$, with ties handled by a choice rather than by a unique top choice; and the first-stage argument must be carried out with the coalition's reshuffling restricted to its own goods. A tempting shortcut, assuming strict preferences or using a union of cycles at a stage, proves a different statement and is ruled out by the definitions.

Formalization scope

• Traders form an arbitrary finite type N with decidable equality; no nonemptiness is assumed (the empty market has the empty partition). The matrix A : N → N → ℝ has no hypothesis, so ties are allowed.
• Allocations are bijections σ : N → N rather than zero-one matrices. This loses nothing: a coalition in which all members are strictly better off gives each member exactly one item of the coalition (owning nothing is ranked below everything), and an allocation leaving a trader without an item is blocked by that trader alone.
• Blocking is strict for every member of the coalition, as on p. 107; the weak notion (all weakly, one strictly better off) makes assertion (1) false with ties.
• The paper gives no displayed definition of competitive prices. The Lean notion is: $\sigma$ is a bijection, $\mathrm{price}(\sigma(i)) \le \mathrm{price}(i)$, and $\mathrm{price}(k)\le\mathrm{price}(i) \Rightarrow a_{ik}\le a_{i\sigma(i)}$. This transcribes "can sell his own item for $\pi^j$ dollars", "cannot afford", and "his utility is maximized" (p. 114).
• A top trading cycle is a single cycle of the successor map: nonempty, inside $R$, closed under next, every member reaching every other by iterating next. A one-trader cycle with next i = i is allowed (footnote, p. 114).
• Explicit readings of loose phrases: "it is evident" (milestone 1) is an existence statement; "the highest possible payoff available to him in $S$" (milestone 3) is $a_{ik} \le a_{i\,\mathrm{next}(i)}$ for all $k\in S$; "cannot afford any items from $S^1,\dots,S^{j-1}$" (milestone 4) is: price at most $\pi^j$ implies stage at least $j$; "a set of competitive prices exists" (goal) is strengthened to every strictly decreasing positive $\pi$, as the proof gives.
• Trivializing formalizations are ruled out: the partition is quantified over all choices and its existence is a milestone, cycles are required to be nonempty and single, and the budget clause is part of the price notion, so competitiveness does not reduce to "everyone gets a best good".
• Contributions welcome: proofs of the milestones, a computable top-trading-cycle algorithm with a proof that it produces a partition, and a proof of the paper's remark that no other competitive prices exist up to ties.

Selected references

• L. Shapley and H. Scarf, On cores and indivisibility, Journal of Mathematical Economics 1 (1974) 23–37. https://doi.org/10.1016/0304-4068(74)90033-0
• H. Scarf, The core of an N person game, Econometrica 35 (1967) 50–69. https://doi.org/10.2307/1909383
• A. E. Roth and A. Postlewaite, Weak versus strong domination in a market with indivisible goods, Journal of Mathematical Economics 4 (1977) 131–137. https://doi.org/10.1016/0304-4068(77)90004-0
• A. E. Roth, Incentive compatibility in a market with indivisible goods, Economics Letters 9 (1982) 127–132. https://doi.org/10.1016/0165-1765(82)90003-9
• A. Abdulkadiroğlu and T. Sönmez, School choice: a mechanism design approach, American Economic Review 93 (2003) 729–747. https://doi.org/10.1257/000282803322157061

Motivation

A correlated equilibrium (Aumann 1974) describes play in a game where a mediator draws a profile of recommended actions from a joint distribution and tells each player only that player's own recommendation; the distribution is an equilibrium when no player gains, on average, by departing from the recommendation. Correlated equilibria are the natural outcome of regret-minimizing learning dynamics and the solution concept underlying much of algorithmic game theory, so it matters in which games they are guaranteed to exist.

For finite games existence follows from Nash's theorem, since every Nash equilibrium is a correlated one. Hart and Schmeidler (1989) gave a direct proof based on linear duality, with no fixed-point theorem, and then extended it beyond finite games. This mission formalizes the last and most general of their three existence theorems: games with arbitrarily many players whose strategy spaces are compact Hausdorff spaces.

Timeline.

• 1952: Fan and Glicksberg prove fixed-point theorems that yield Nash equilibria, hence correlated equilibria, for continuous games on compact strategy spaces.
• 1969: Peleg proves existence of Nash equilibria for games with infinitely many players, finite strategy sets and continuous payoffs.
• 1974: Aumann introduces correlated equilibria (J. Math. Econ. 1).
• 1987: Aumann characterizes correlated equilibrium as Bayesian rationality (Econometrica 55).
• 1989: Hart and Schmeidler prove existence of correlated equilibria by a separation argument: Theorem 1 for finite games, Theorem 2 for infinitely many players with finite strategy sets, Theorem 3 for compact Hausdorff strategy spaces (Math. Oper. Res. 14).

Setting

A game consists of a nonempty set $N$ of players, possibly uncountable; for each player $i\in N$ a nonempty set $S^i$ of pure strategies; and for each player a payoff function $h^i:S\to\mathbb R$ on the set of strategy profiles $S=\prod_{j\in N}S^j$. For a profile $s$ and a strategy $t^i\in S^i$, $(s^{-i},t^i)$ denotes the profile obtained from $s$ by replacing player $i$'s coordinate with $t^i$; thus $h^i(s)=h^i(s^{-i},s^i)$.

In this mission each $S^i$ is a compact Hausdorff space with its Borel σ-algebra $\Sigma^i$, the profile space $S$ carries the product topology, and $\Sigma$ is the Borel σ-algebra of $S$. The product σ-algebra $\Sigma_0$ generated by the $\Sigma^i$ is contained in $\Sigma$, and the inclusion may be strict when $S$ is not metrizable (the paper's footnote 13).

Let $p$ be a probability measure on $(S,\Sigma)$. Think of $p$ as the mediator's distribution; player $i$ learns the coordinate $s^i$ of the drawn profile. A deviation of player $i$ is a $\Sigma^i$-measurable map $\zeta^i:S^i\to S^i$ that replaces each recommendation by an action. The measure $p$ is a correlated equilibrium with respect to $\{\Sigma^i\}_{i\in N}$ and $\Sigma$ when, for every player $i$ and every deviation $\zeta^i$,

$$\int_S\bigl[h^i(s^{-i},s^i)-h^i\bigl(s^{-i},\zeta^i(s^i)\bigr)\bigr]\,dp(s)\ \ge\ 0 . \tag{4}$$

The left side is the expected gain from obeying the recommendation instead of following $\zeta^i$.

Formalization targets

Goal: Theorem 3

If every $S^i$ is compact Hausdorff and every $h^i$ is continuous on $S$ with the product topology, then

$$\exists\, p\ \text{probability measure on } (S,\Sigma)\ \text{such that (4) holds for all } i\in N \text{ and all } \Sigma^i\text{-measurable } \zeta^i .$$

"Countably additive" in the paper's statement is automatic: $p$ is a measure.

Milestones, in the order of the proof

1. Every f-set game has a correlated equilibrium. An f-set is a product $T=\prod_iT^i$ of finite nonempty sets $T^i\subseteq S^i$ with $T^i$ a singleton for all but finitely many $i$; the game $\Gamma_T$ restricts each player to $T^i$, and its correlated equilibrium $q_T$ is a finitely supported probability on $S$.
2. On a compact Hausdorff space, every net of probability measures has a regular probability measure as a cluster point for the topology induced by the continuous functions.
3. For a regular probability $p$ on $S$ and a Borel set $R^i\subseteq S^i$, there are a closed $F^i\subseteq R^i$ and an open $G^i\supseteq R^i$ with $p\bigl((G^i\setminus F^i)\times S^{-i}\bigr)<\varepsilon$: the marginal of a regular measure is regular.
4. The special case. A regular cluster point $p$ of the $q_T$ satisfies (4) for every deviation that equals a fixed $t^i$ on a Borel set $R^i$ and the identity elsewhere.
5. For continuous $h^i$ and $\varepsilon>0$, $S^i$ has a finite Borel partition $A_1,\dots,A_K$ with $|h^i(s^{-i},a)-h^i(s^{-i},b)|<\varepsilon$ for $a,b$ in the same piece and every $s^{-i}$.
6. The general case. If (4) holds for all deviations of the special form, it holds for every Borel deviation.

An optional milestone records the remark on p. 23 that, for a finite strategy set $S^i$, condition (4) for player $i$ is equivalent to the earlier condition (3), one inequality per recommendation $r^i$ and alternative $t^i$.

Significance

The result. Theorem 3 guarantees correlated equilibria, with a genuine (countably additive) probability measure, in every continuous game on compact strategy spaces, however many players there are. It also justifies taking $\Sigma$ to be the full Borel σ-algebra rather than the smaller product σ-algebra, so that every Borel-measurable deviation rule is allowed. Nash existence under the same hypotheses (Fan 1952, Glicksberg 1952) implies existence of correlated equilibria too, but through a fixed-point theorem; the proof here uses only finite-dimensional duality and compactness.

Formalizing it. The theorem is classical and its proof is published; nothing here is open. To our knowledge no machine-checked proof of Theorem 3, or of any existence result for correlated equilibria in infinite games, exists. Finite-game existence results are on the platform (AGT.nash_existence; the correlated-equilibrium encodings of Aumann 1987 and Foster and Vohra 1997, and AGT.swap_regret_correlated_equilibrium). The formalization would add reusable measure-theoretic tools on compact products: the regular cluster point of a net of probability measures, the regularity of marginals, and uniform partitions for continuous functions on a product.

Difficulty

The obvious argument is the one that proves Theorem 2: approximate the game by finite games $\Gamma_T$, take correlated equilibria $q_T$, extract a weak-* cluster point $p$, and pass the inequalities of $\Gamma_T$ to the limit. Passing to the limit works only for integrands that are continuous in $s$, because $p$ is a cluster point against continuous functions only. The integrand of (4) is $h^i(s)-h^i(s^{-i},\zeta^i(s^i))$, and $\zeta^i$ is merely Borel measurable, so this integrand need not be continuous and the limit step fails. Restricting to continuous deviations would avoid the difficulty but would prove a weaker theorem. Two further points need care: on a non-metrizable product the Borel σ-algebra is larger than the product σ-algebra, and the f-sets ordered by inclusion are not a directed set.

Formalization scope

The profile space is a type synonym Profile S of ∀ i, S i carrying the product topology and the instance borel (Profile S), so measures on $S$ live on the Borel σ-algebra $\Sigma$ and not on Mathlib's product σ-algebra MeasurableSpace.pi ($=\Sigma_0$). The pair $(s^{-i},t^i)$ is Function.update s i t. Players form a type ι with Nonempty ι; each S i is nonempty, compact and Hausdorff with BorelSpace (S i); payoffs are h : ι → Profile S → ℝ with each h i continuous. Deviations are all maps ζ : S i → S i with Measurable ζ.

The predicate IsCorrelatedEq h μ requires IsProbabilityMeasure μ and, for each player and measurable deviation, both integrability of the integrand and nonnegativity of its integral. The integrability clause prevents a trivializing reading in which a non-integrable integrand, whose Lean integral is $0$, satisfies (4) vacuously; restricting deviations to continuous maps, or using the product σ-algebra, would also change the theorem and is ruled out.

The f-set net is indexed by the f-sets containing a fixed profile $\hat s$, which are directed; the paper's "ordered by inclusion of the sets $T$" over all f-sets is not directed, and anchoring repairs this without affecting any statement of the paper. A correlated equilibrium $q_T$ of $\Gamma_T$ is encoded by its finite support and weights (IsFSetCE). The special case is stated for a regular cluster point of the $q_T$ given by these constructed objects, not for an arbitrary measure.

A complete development needs Banach–Alaoglu or the compactness of probability measures on a compact space, the Riesz–Markov–Kakutani representation (RealRMK), regularity of measures (Measure.Regular), Urysohn's lemma, and uniform continuity on compact spaces, all available in Mathlib in some form. Proofs of any milestone, including the general-purpose milestones 2, 3 and 5, are welcome.

Selected references

• S. Hart and D. Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14(1), 18–25, 1989. https://doi.org/10.1287/moor.14.1.18
• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1, 67–96, 1974. https://doi.org/10.1016/0304-4068(74)90037-8
• R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55(1), 1–18, 1987. https://doi.org/10.2307/1911154
• B. Peleg, Equilibrium Points for Games with Infinitely Many Players, Journal of the London Mathematical Society s1-44, 292–294, 1969. https://doi.org/10.1112/jlms/s1-44.1.292
• I. L. Glicksberg, A Further Generalization of the Kakutani Fixed Point Theorem, with Application to Nash Equilibrium Points, Proceedings of the AMS 3, 170–174, 1952. https://doi.org/10.1090/S0002-9939-1952-0046638-5
• K. Fan, Fixed-Point and Minimax Theorems in Locally Convex Topological Linear Spaces, PNAS 38, 121–126, 1952. https://doi.org/10.1073/pnas.38.2.121
• N. Dunford and J. T. Schwartz, Linear Operators, Part I, Interscience, 1958.

Motivation

Two parties who can cooperate for mutual benefit must still agree on how to share the benefit. In The Bargaining Problem (Econometrica, 1950) John Nash asked which agreement two rational bargainers of equal skill should reach. His answer is not a model of haggling: it is a list of conditions any reasonable rule should satisfy, together with a proof that exactly one point of the set of feasible agreements is compatible with them. That point maximizes the product of the two parties' utility gains. Known as the Nash bargaining solution, it is the reference point of cooperative bargaining theory. Economics, operations research and networking all use it: in supply contracts, in wage bargaining, and in fair bandwidth allocation, where maximizing a product of gains becomes maximizing a sum of logarithms (proportional fairness).

Timeline:

• 1944. von Neumann and Morgenstern axiomatize expected utility. A utility is determined up to a positive affine transformation $au+b$. Nash quotes this on p. 157.
• 1950. Nash introduces the two-person bargaining problem and the axioms of Pareto efficiency, independence of irrelevant alternatives and symmetry, the solution being invariant under the choice of utility scales. He proves that they force the maximizer of the product $u_1u_2$ (doi:10.2307/1907266).
• 1953. Nash's Two-Person Cooperative Games adds the threat game that fixes the disagreement point.
• 1975. Kalai and Smorodinsky replace independence of irrelevant alternatives by monotonicity and obtain a different solution.
• 1986. Binmore, Rubinstein and Wolinsky show that the Nash solution is the limit of equilibria of alternating-offers bargaining as the time between offers vanishes.

Setting

A bargaining problem is a pair $\langle S,d\rangle$. Here $S\subseteq\mathbb R^2$ is the set of utility pairs $u=(u_1,u_2)$ the two players can reach by agreement, including lotteries over agreements. $d\in S$ is the disagreement point, the utilities of no cooperation. As in the platform goal, $S$ is compact and convex, and some $s\in S$ has $s_1>d_1$ and $s_2>d_2$ (both individuals could gain). Write $\mathcal B$ for the set of such pairs.

A bargaining solution is a map $g$ from $\mathcal B$ to $\mathbb R^2$. Nash requires:

• Selection. $g(S,d)\in S$.
• PAR (Nash's assumption 6). If $s,t\in S$ and $t$ is strictly better than $s$ for both players, then $g(S,d)\neq s$.
• IIA (assumption 7). If $S\subseteq T$ and $g(T,d)\in S$, then $g(S,d)=g(T,d)$.
• SYM (assumption 8). If $d_1=d_2$ and $S$ is symmetric in the line $u_1=u_2$, then $g(S,d)$ lies on that line.
• INV. For $L(s)=(\alpha_1s_1+\beta_1,\ \alpha_2s_2+\beta_2)$ with $\alpha_1,\alpha_2>0$, $g(L(S),L(d))=L(g(S,d))$.

The paper has no separate INV axiom. It normalizes the disagreement utility to $0$ and notes that each utility is then determined only up to a positive multiple (p. 158), so the solution must not depend on that choice.

Formalization targets

Goal

The goal is the platform theorem NashBargaining.nash_bargaining_solution_unique, posed by Nickrobbins95 and currently Open. This mission references it and does not restate it. It asserts that there is a solution $f$ such that a solution $g$ satisfies selection, INV, SYM, IIA and PAR if and only if $g=f$, and that for every $\langle S,d\rangle\in\mathcal B$

$$f(S,d)\ge d,\qquad (s_1-d_1)(s_2-d_2)<(f_1-d_1)(f_2-d_2)\ \text{ for all } s\in S,\ s\ge d,\ s\neq f(S,d).$$

Nash's paper proves the necessity half: a solution satisfying the conditions must select the maximizer of the Nash product. The sufficiency half, that the maximizer map satisfies the five conditions, is not argued in the paper. It must be supplied by whoever closes the goal.

Milestones

1. On a compact convex $S\ni(0,0)$ that contains a point where both players gain, $u_1u_2$ has exactly one strict maximizer $p$ in the closed first quadrant, and $p_1,p_2>0$.
2. Multiplying the utilities by positive constants maps the maximizer to the maximizer, so $p$ may be moved to $(1,1)$.
3. If $S$ is convex and $(1,1)$ maximizes $u_1u_2$, then $u_1+u_2\le2$ on all of $S$.
4. A compact $S$ under that line lies in a square $Q_h=\{2-2h\le u_1+u_2\le2,\ |u_1-u_2|\le h\}$.
5. $(1,1)$ is the only point of $Q_h$ on the diagonal that no point of $Q_h$ strictly dominates.
6. Necessity. Under the five conditions, $g(S,d)$ is the strict maximizer of $(s_1-d_1)(s_2-d_2)$ over $S\cap\{s\ge d\}$.

Two further items formalize the paper's examples: the Bill–Jack barter, whose solution is the vertex $(12,5)$ reached by exactly one exchange, and trade with money, where the solution gives equal money profits.

Significance

The Nash product characterization is used, mostly without proof, wherever a "fair" split of a cooperative surplus is needed. Examples are generalized Nash bargaining in supply-chain contracting and labour economics, the proportional-fairness criterion in network rate control, and the Nash-in-Nash models of bilateral negotiations. Many papers that build on it apply it to a specific feasible set. They therefore rely on the necessity direction, which is the step that makes the maximizer the unique answer rather than one answer among several.

The result has been proved since 1950, while the referenced Prove2Me goal remains Open. This mission supplies the milestones of Nash's own argument in the encoding of that goal, so that the necessity direction can be assembled from them. Sufficiency remains as separate work. The two examples are small, concrete checks of the solution concept.

Difficulty

Each step is elementary. The difficulty is in keeping the bookkeeping honest across the normalizations. The axioms are stated on the class $\mathcal B$, and a solution is a function on a subtype. Every application of INV, SYM or IIA therefore needs a membership proof for a transformed set: the image of $S$ under an affine map, or the enclosing square. It also needs the disagreement point to be carried along. The tempting short cut is to argue "without loss of generality $d=0$ and $p=(1,1)$". That is exactly what INV licenses, but only after compactness, convexity, the point where both gain, and the location of $d$ inside the square have been re-established for each transformed problem. Uniqueness of the maximizer also needs care at the boundary of the quadrant, where the product vanishes.

Formalization scope

Utility pairs are ℝ × ℝ, with u.1 player 1's utility and u.2 player 2's. Milestones 1–5 work at $d=(0,0)$, the paper's normalization. Milestone 6 has a general $d$ and the goal's encoding. Milestones 1–5 make the following readings explicit:

• "First quadrant" is the closed quadrant $u_1\ge0,\ u_2\ge0$.
• "The point where $u_1u_2$ is maximized" is the strict maximizer over $S$ in that quadrant, in the goal's form. Milestone 1 also states $p_1,p_2>0$, which follows from the point where both gain (p. 158).
• Milestone 3's hypothesis is the weak maximum $s_1s_2\le1$. Its conclusion covers every point of $S$, not only first-quadrant points.
• The square is the explicit set $Q_h$. Its compactness, convexity and literal symmetry $(a,b)\in Q_h\iff(b,a)\in Q_h$ are part of milestone 4's conclusion.
• "Satisfying assumptions (6) and (8)" in the square means lying on $u_1=u_2$ and being strictly dominated by no point of the square.

Milestone 6's five hypotheses are copied verbatim from the goal, and its conclusion is the goal's last conjunct for the given $g$. It does not restate the goal: it has no existence claim and no "if and only if".

Trivializing formalizations are ruled out. The point where both gain is a hypothesis wherever uniqueness is claimed; without it a segment on an axis has many maximizers of $u_1u_2=0$. The square is a concrete set, not "some symmetric compact convex set", and the solution's properties are quantified over the goal's class $\mathcal B$, which is nonempty.

The examples need finite sums, convex hulls of finite sets, and extreme points, all in Mathlib. Contributions are welcome on each milestone and on the sufficiency half of the goal.

Related platform work treats other bargaining models. These are Rubinstein's alternating-offers game (RubinsteinBargaining.PEP) and the Chatterjee–Samuelson sealed-offer double auction (ChatterjeeSamuelson). Neither is used here. The von Neumann–Morgenstern utility theorem behind the normalization is formalized as TheoryOfGames.Utility.utility_existence_uniqueness.

Selected references

• J. F. Nash, Jr., The Bargaining Problem, Econometrica 18(2), 155–162, 1950. doi:10.2307/1907266
• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.
• J. F. Nash, Jr., Two-Person Cooperative Games, Econometrica 21(1), 128–140, 1953. doi:10.2307/1906951
• E. Kalai, M. Smorodinsky, Other Solutions to Nash's Bargaining Problem, Econometrica 43(3), 513–518, 1975. doi:10.2307/1914280
• K. Binmore, A. Rubinstein, A. Wolinsky, The Nash Bargaining Solution in Economic Modelling, RAND Journal of Economics 17(2), 176–188, 1986. doi:10.2307/2555382
• M. J. Osborne, A. Rubinstein, Bargaining and Markets, Academic Press, 1990, Theorem 2.3.