Algorithmic Game Theory

Motivation

A correlated equilibrium (Aumann, 1974) is a joint distribution over the players' strategy profiles from which no player gains by deviating from a recommended strategy. A central question of learning in games is which equilibria repeated play of simple, myopic rules can reach. Foster and Vohra (1997) answered it for calibrated forecasting: if each player forecasts the opponent with a calibrated rule and best-responds to the forecast, the empirical distribution of play approaches the set of correlated equilibria (their Theorem 1). That result has become a basic reference point for no-regret and calibration-based learning in games (Hart and Mas-Colell, 2000).

This mission formalizes the paper's converse. Theorem 1 says calibrated learning ends up in the correlated equilibria; the converse says it can end up at any of them, for almost every game. Together the two results characterize exactly which long-run outcomes calibrated learning with best responses can produce.

Setting

Two players choose strategies from finite sets $S(1)$ with $m$ elements and $S(2)$ with $n$ elements; player $i$ receives payoff $u_i(x,y)\in\mathbb{R}$ and maximizes it. A game $G=(u_1,u_2)$ is a pair of real $m\times n$ matrices, that is, a point of $\mathbb{R}^{2mn}$; a set of games has measure zero if it is Lebesgue-null in $\mathbb{R}^{2mn}$.

A joint distribution $D$ on $S(1)\times S(2)$ is a correlated equilibrium if for every map $\Phi:S(1)\to S(1)$, $\sum_{x,y}D(x,y)u_1(\Phi(x),y)\le\sum_{x,y}D(x,y)u_1(x,y)$, and symmetrically for player 2. $\pi(G)$ is the set of correlated equilibria.

Play is repeated in rounds $t=0,1,2,\dots$. Before each round, player 1 issues a forecast $f_1(t)$, a probability vector over $S(2)$, produced by a deterministic forecasting rule from the history of play so far; player 2 likewise forecasts player 1. For a forecast sequence $f$ and the opponent's plays $z$, let $N(p,t)$ be the number of the first $t$ rounds with forecast $p$, and $\rho(p,j,t)$ the fraction of those rounds in which the opponent played $j$ (zero if $N(p,t)=0$). The forecasts are calibrated if for every $j$

$$\sum_p |\rho(p,j,t)-p_j|\,\frac{N(p,t)}{t}\ \longrightarrow\ 0 \qquad (t\to\infty).$$

Each player then plays $R_i$ of its forecast, where the best-reply function $R_i$ picks a best response to every forecast and does not depend on the round. $D_t(x,y)$ is the fraction of the first $t$ rounds in which $(x,y)$ was played.

$\lambda(G)$, the set of limit points of calibrated forecasts, consists of the $D$ for which some best-reply functions $R_1,R_2$ and some calibrated forecasting rules make $D_t(x,y)\to D(x,y)$ for all $(x,y)$.

Formalization targets

Goal: Theorem 2 (p. 47)

$$\text{for Lebesgue-almost every } G\in\mathbb{R}^{2mn}:\qquad \lambda(G)=\pi(G).$$

Milestones

1. $\lambda(G)\subseteq\pi(G)$ for every game (Theorem 1 restated, p. 46).
2. Every joint distribution $D$ is the limiting empirical distribution of a deterministic play sequence supported on $\{D>0\}$ (p. 47).
3. Along such a sequence the conditional forecasts $p_{1,t}=D(x_t,\cdot)/\sum_yD(x_t,y)$ and $p_{2,t}=D(\cdot,y_t)/\sum_xD(x,y_t)$ are calibrated (p. 47).
4. In a correlated equilibrium each recommended strategy is a best response to its conditional forecast (p. 47).
5. For almost every payoff matrix, each set $M_b(x)$ of forecasts to which $x$ is a best response is either empty or contains a forecast in the open simplex at which $x$ is the unique best response (p. 47).
6. The perturbed forecasts $p_i=(1-1/i)p^*+(1/i)q$ converge to $p^*$ and keep a unique best reply (p. 48).
7. For the $3\times3$ game of p. 48, a correlated equilibrium lies outside $\lambda(G)$, and $\lambda(G)$ is the single point mass on $(C,2)$.

Significance

Theorem 1 by itself leaves open whether calibration selects among correlated equilibria, for instance toward Nash equilibria or toward particular payoffs. Theorem 2 closes that question negatively for generic games: every correlated equilibrium is the genuine limit, not merely an accumulation point, of calibrated play with stationary best replies. As the paper notes, adding the assumption that the limit exists therefore does not refine the equilibrium reached, in contrast with Fudenberg and Kreps's result for asymptotically myopic Bayesian play. The $3\times3$ example shows that the genericity hypothesis cannot be dropped.

The results are proved in the 1997 paper; none is formalized. A complete development produces a reusable layer for repeated two-player games (calibration, empirical distributions, best-reply maps, correlated equilibria), a genericity lemma for best-response regions that is useful beyond this paper, and a machine-checked version of an argument that the paper gives only in outline.

Difficulty

The natural construction takes a correlated equilibrium $D$, a play sequence realizing $D$, and forecasts equal to the conditional distributions of $D$. The forecasts are then calibrated and each played strategy is a best response. What fails is the best-reply function: two strategies $x'\ne x''$ can have the same conditional forecast $p^*$, while a stationary $R_1$ maps $p^*$ to only one strategy. Separating them needs forecasts near $p^*$ at which each is the unique best response, and that exists only when the best-response regions have nonempty relative interior, a property that fails on a null set of games (the $3\times3$ example) and whose genericity must be proved. The perturbed forecasts are no longer exactly equal to the conditional frequencies, so calibration has to be re-established with errors that vanish along the sequence.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; players maximize. A game is a point of (Fin m → Fin n → ℝ) × (Fin m → Fin n → ℝ) with Mathlib's volume (Lebesgue measure on $\mathbb{R}^{2mn}$), and "almost every" is ∀ᵐ.
• A correlated equilibrium is the joint-distribution form of p. 44 (a joint distribution with the two deviation inequalities).
• Forecasting rules map finite histories to probability vectors; the play is generated recursively from the rules and the best-reply functions. Best-reply functions are arbitrary stationary selections of a best response at every probability vector; they may not depend on the round, since round-dependent tie-breaking enlarges $\lambda(G)$ (the matching pennies example of p. 46).
• Rounds are $0,\dots,t-1$; $D_0=0$. The calibration sum runs over the forecasts issued so far, which is the paper's sum over all $p$ since the other terms vanish.
• $\lambda(G)$ requires convergence of $D_t$, not a subsequence. Replacing the limit by a limit point, or stating only $\pi(G)\subseteq\lambda(G)$, does not formalize the theorem.
• The page's sentence "Almost every game has the property that all the sets $M_b(x)$ have non-empty interior" is false for dominated strategies ($M_b(x)=\emptyset$ on an open set of games). Milestone 5 states the dichotomy the page's argument proves: empty or with relative interior.
• The page prints the denominator of $p_{2,t}$ as $\sum_{x}D(x_t,y)$; the mission uses $\sum_xD(x,y_t)$.

The theorems are stated from the mission's own definitions of the game, calibration and $\lambda(G)$; no statement is vacuous: at $m=0$ or $n=0$ both sides of the goal are empty, and the $3\times3$ example exercises every definition. Contributions welcome: proofs of the milestones in any order, the genericity lemma (Lebesgue-null sets of linear degeneracies), and the calibration estimates for the perturbed forecasts.

Selected references

• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77 (1982), 605–610. https://doi.org/10.1080/01621459.1982.10477856
• D. Fudenberg and D. M. Kreps, Learning mixed equilibria, Games and Economic Behavior 5 (1993), 320–367. https://doi.org/10.1006/game.1993.1021
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

Motivation

Cooperative games model the division of a jointly produced surplus, or a jointly incurred cost, among the participants of an enterprise: towns sharing a water supply system, divisions of a firm sharing overhead, members of a consortium sharing the savings of joint investment. In such applications allocations are rarely fixed once and for all. Costs and revenues are re-estimated, projects are re-scoped, and the allocation is recomputed. A natural requirement on any allocation method is then monotonicity: when the underlying data change in a player's favour, that player's share should not fall.

H. P. Young, Monotonic Solutions of Cooperative Games (Int. J. Game Theory 14, 1985), studies several forms of this principle. The weakest, aggregate monotonicity, asks that no player lose when only the value of the grand coalition increases; Megiddo (1974) had already shown that the nucleolus violates it. The paper's first theorem concerns a stronger and more natural form, coalitional monotonicity, which was first proposed by Shubik (1962) in the context of cost allocation within a firm, and shows that it cannot be reconciled with the core, the most widely used stability requirement. This mission formalizes that impossibility theorem.

Setting

Fix $n$ players, $N = \{1, 2, \dots, n\}$. A cooperative game on $N$ is a function $v$ assigning a real number $v(S)$ to every coalition $S \subseteq N$, with $v(\emptyset) = 0$. No superadditivity or other structural assumption is imposed.

An allocation procedure is a map $\varphi$ that assigns to every game $v$ on $N$ an allocation $\varphi(v) = (\varphi_1(v), \dots, \varphi_n(v)) \in \mathbb{R}^N$ satisfying efficiency:

$$\sum_{i \in N} \varphi_i(v) = v(N).$$

The core of $v$ is the set of allocations that no coalition can improve upon on its own:

$$C(v) = \Big\{x \in \mathbb{R}^N : \sum_{i \in S} x_i \ge v(S) \text{ for all } S \subseteq N,\ \sum_{i \in N} x_i = v(N)\Big\}.$$

It may be empty. An allocation procedure is a core allocation rule if $\varphi(v) \in C(v)$ for every game $v$ whose core is nonempty. The nucleolus is the standard example.

An allocation procedure is coalitionally monotonic (Eq. (4) of the paper) if raising the value of a single coalition, with all other values unchanged, never decreases the allocation of any member of that coalition: for all games $v, w$ and every coalition $T \subseteq N$,

$$v(T) \ge w(T),\ \ v(S) = w(S)\ \ \forall S \ne T \ \Longrightarrow\ \varphi_i(v) \ge \varphi_i(w)\ \ \forall i \in T.$$

The paper notes that this is equivalent to its one-player form (5): if every coalition containing player $i$ weakly gains in value and every coalition not containing $i$ is unchanged, then $\varphi_i$ does not decrease.

In the Lean development these objects are Game n, IsAllocationProcedure, IsCoreRule and IsCoalitionallyMonotonic in the namespace MonotonicSolutions.CoreRules, and the core is the published definition Supermodularity.Cooperative.Core.

Formalization targets

Goal: Theorem 1

For every $n \ge 5$,

$$\neg\,\exists\,\varphi \ :\ \varphi \text{ is an allocation procedure on } N=\{1,\dots,n\},\ \varphi \text{ is a core allocation rule, and } \varphi \text{ is coalitionally monotonic}.$$

Milestones

1. Eqs. (4)–(5). Coalitional monotonicity is equivalent to the one-player condition (5).
2. The core of the game $w$. For the explicit five-player game $w$ of the proof, built from the coalitions $S_1 = \{3,5\}$, $S_2=\{1,2,3\}$, $S_3=\{1,3,4\}$, $S_4=\{2,4,5\}$, $S_5=\{1,2,4,5\}$ with values $3,3,9,9,9$ and $w(N) = 11$, the core is the single point $(0,1,2,7,1)$.
3. The core of the game $v$. For the game $v$ equal to $w$ except $v(S_5) = v(N) = 12$, the core is the single point $(3,0,0,6,3)$.
4. The case $|N| = 5$. The goal with $n = 5$.

An additional statement records the paper's remark that the egalitarian rule $\varphi_i(v) = v(N)/|N|$ satisfies (5), so that the monotonicity axiom on its own is satisfiable.

Significance

The theorem shows that no refinement of the core, however cleverly designed, can be coalitionally monotonic once there are five or more players. For the nucleolus this strengthens Megiddo's earlier observation, and the paper uses it to motivate the search for monotonic solution concepts outside the core, which leads to its second theorem: the Shapley value is the unique symmetric allocation procedure satisfying an even stronger monotonicity property (the subject of the companion mission). In cost-allocation practice the result says that an allocation method that is always stable against coalitional secession must sometimes penalise a division for making its own operations cheaper.

The result has been proved since 1985, and its proof is a short explicit counterexample. What the formalization adds is a machine-checked version of the counterexample (two explicit games whose cores are single points), a verified equivalence between the coalition-wise and player-wise forms of monotonicity, and the extension from five to arbitrarily many players, which the paper dismisses as an "obvious extension". To the best of the curators' knowledge none of these statements is formalized in any proof assistant.

Difficulty

The individual steps are elementary, but each requires care. Determining the core of each counterexample game exactly means showing both that the given point satisfies all $2^5$ coalition constraints and that no other point does. The equivalence of (4) and (5) is stated in the paper as following from "successive application" of (4), and every game involved must vanish on the empty coalition. The two counterexample games differ on two coalitions, $S_5$ and $N$, so a single application of (4) does not suffice. Finally, the paper passes from five players to $n \ge 5$ players with the words "by obvious extension"; a formal proof has to make that step explicit, for arbitrary $n$ and for rules defined on all games with $n$ players, not only on those derived from five-player games.

Formalization scope

• Players are Fin n; the paper's player $k$ is the Lean index $k-1$. Thus the core points $(0,1,2,7,1)$ and $(3,0,0,6,3)$ appear as ![0,1,2,7,1] and ![3,0,0,6,3], and the players "2 and 4" whose allocations decrease are indices 1 and 3.
• A game is the subtype Game n := {v : Finset (Fin n) → ℝ // v ∅ = 0}. Monotonicity axioms therefore quantify only over normalised games, as in the paper.
• Allocations are real vectors Fin n → ℝ. Efficiency is part of the goal's hypotheses, matching the paper's definition of an allocation procedure.
• The core is Supermodularity.Cooperative.Core Finset.univ v.1, the published core definition from Supermodularity and Complementarity, which coincides with the set on p. 68 of the paper.
• IsCoreRule requires $\varphi(v) \in C(v)$ only when $C(v)$ is nonempty. The unconditional requirement would be unsatisfiable, because some games have an empty core, and would make the goal trivially true; that reading is ruled out.
• IsCoalitionallyMonotonic is Eq. (4) with $T$ ranging over all coalitions, including $N$. Restricting to $T \ne N$, or restricting the games to superadditive ones, would change the theorem.
• The counterexample games are defined in YoungGames: for $S \ne N$, the value is the largest listed $w(S_k)$ over the $S_k \subseteq S$, and $0$ if there is none.

Contributions welcome: proofs of the four milestones and the goal; a general lemma that padding a game with null players preserves the core up to zeros, which is reusable for other small-counterexample results in cooperative game theory; and decision procedures for linear feasibility over the coalitions of small games.

Selected references

• H. P. Young, Monotonic Solutions of Cooperative Games, International Journal of Game Theory 14 (1985), 65–72. https://doi.org/10.1007/BF01769885
• N. Megiddo, On the Nonmonotonicity of the Bargaining Set, the Kernel and the Nucleolus of a Game, SIAM Journal on Applied Mathematics 27 (1974), 355–358. https://doi.org/10.1137/0127026
• M. Shubik, Incentives, Decentralized Control, the Assignment of Joint Costs and Internal Pricing, Management Science 8 (1962), 325–343. https://doi.org/10.1287/mnsc.8.3.325
• D. B. Gillies, Solutions to General Non-Zero-Sum Games, in Contributions to the Theory of Games IV, Annals of Mathematics Studies 40 (1959), 47–85 (Princeton University Press). Cited as in Young (1985); no DOI checked.

Motivation

A two-sided market in which each participant trades with at most one partner on the other side — houses and buyers, workers and firms, producers and consumers under exclusive bilateral contracts — is the setting of L. S. Shapley and M. Shubik's assignment game (Int. J. Game Theory 1 (1971) 111–130). Money is transferable, so the natural solution concept is cooperative: a division of the total gain that no coalition of traders can improve upon. The question the paper answers first is whether such a division exists and how to find it, given that a market with $m$ sellers and $n$ buyers has $2^{m+n}$ coalitions.

The answer, Theorem 2 of the paper, connects the core of the game with the dual of the linear-programming relaxation of the optimal assignment problem. It is the starting point of the literature on two-sided matching markets with transfers: the lattice structure of the core (Theorem 3 of the same paper), the ascending auctions of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the equivalence of core outcomes with competitive equilibrium prices. The same LP pairing reappears in stable matching with transfers and in the VCG analysis of multi-item auctions with unit demand.

Setting

Let $M$ be a finite set of sellers and $N$ a finite set of buyers; either may be empty and their sizes need not agree. A matrix $a = (a_{ij})_{i \in M, j\in N}$ of nonnegative reals records the profit $a_{ij} \ge 0$ that the partnership of seller $i$ and buyer $j$ can realise (in the real-estate reading, $a_{ij} = \max(0, h_{ij} - c_i)$ with $h_{ij}$ buyer $j$'s valuation of house $i$ and $c_i$ its owner's reservation value).

A coalition $S \subseteq M \cup N$ is described by its sellers $A = S\cap M$ and buyers $B = S \cap N$. A matching inside $(A, B)$ is a set of seller–buyer pairs from $A \times B$ in which no player appears twice. The characteristic function (2.6) assigns to $S$ its worth

$$v(S) = \max_{P} \sum_{(i,j) \in P} a_{ij},$$

the maximum over matchings $P$ inside $S$. One-sided coalitions and singletons are worth $0$.

A payoff vector is a pair $(u, v)$ with $u \in \mathbb R^M$, $v \in \mathbb R^N$ (the paper uses $v$ both for the characteristic function and for buyers' payoffs; the formal development calls the former worth). The core is the set of payoff vectors with

$$\sum_{i\in M} u_i + \sum_{j \in N} v_j = v(M \cup N) \quad (3.5), \qquad \sum_{i\in S\cap M} u_i + \sum_{j \in S\cap N} v_j \ge v(S)\ \text{ for all } S \quad (3.6).$$

The assignment LP (3.1)–(3.2) maximises $z = \sum_{i,j} a_{ij} x_{ij}$ over $x_{ij} \ge 0$ with $\sum_{i} x_{ij} \le 1$ for each $j$ and $\sum_j x_{ij} \le 1$ for each $i$. Its dual (3.3)–(3.4) minimises $w = \sum_i u_i + \sum_j v_j$ over $u_i \ge 0$, $v_j \ge 0$ with $u_i + v_j \ge a_{ij}$ for all $i, j$. The optimal values are $z_{\max}$ and $w_{\min}$.

Formalization targets

Goal: Theorem 2 (p. 118)

$$\operatorname{core}(a) = \{(u,v) : (u,v) \text{ is an optimal solution of the dual LP (3.3)–(3.4)}\}.$$

The statement holds for every finite $M$, $N$ and every $a \ge 0$, with no constants to fix.

Milestones, in the order the paper's argument uses them

1. Eq. (3.6), p. 118: every dual-feasible $(u, v)$ gives every coalition at least its worth.
2. Sec. 3.1, p. 117 (quoting Dantzig, p. 318): the assignment LP attains its maximum at a $0/1$ point, and $z_{\max} = v(M \cup N)$.
3. Sec. 3.1, p. 118 (quoting Dantzig, p. 129): both LPs have optima and $w_{\min} = z_{\max}$.
4. Eq. (3.5), p. 118: every dual minimiser satisfies $\sum_i u_i + \sum_j v_j = v(M \cup N)$.

Further results on the same definitions

• Sec. 3.2, p. 118: the core is nonempty.
• Sec. 3.2, p. 119: for $(u,v)$ in the core, $v_j = \max\bigl(0, \max_{i}(a_{ij} - u_i)\bigr)$ for every buyer $j$ — at the seller prices $p_i = c_i + u_i$, buyer $j$'s best net gain is exactly $v_j$.

Significance

Theorem 2 replaces the $2^{m+n}$ coalition constraints of the core with the $mn$ constraints of a linear program. Consequences stated in the paper: the core is never empty; its points are exactly the dual optimal solutions, so the core is a polytope computable by linear programming without evaluating the worth of any coalition other than the grand one; and dual variables are prices — a seller's core payoff determines a price at which every buyer's best purchase yields that buyer's core payoff. The lattice and corner results of Sec. 3.3 build on this identification.

The paper's proof is short but leans on two results quoted from Dantzig's Linear Programming and Extensions: the integrality of the rectangular assignment polytope and the LP duality theorem. A formalization makes these dependencies explicit for the inequality-constrained rectangular case with possibly unequal sides. To our knowledge Theorem 2 has no machine-checked proof. On Prove2Me, general LP strong duality is formalized (LinearOptimization.lp_strong_duality, SmaleNinth.lp_strong_duality), and integrality of the square doubly stochastic assignment LP (UnderstandingML.assignment_lp_integral, FamousTheorems.birkhoff_von_neumann); neither is the specialised statement here, but both are natural substrate.

Difficulty

The inclusion "dual optimal ⊆ core" needs the value of the dual to equal the combinatorial worth $v(M \cup N)$, which is not a statement about linear programming alone: it needs both LP duality and the integrality of the assignment polytope. The integrality needed is for the polytope cut out by inequalities $\le 1$ on a possibly non-square matrix, which is not the Birkhoff polytope of doubly stochastic matrices already on the platform; the gap between the two must be bridged.

The converse, "core ⊆ dual optimal", is dismissed as "clearly" in the paper, but the core is defined through the worth of every coalition, a maximum over exponentially many matchings, while dual optimality is a comparison with every dual-feasible vector. Neither side mentions the other's objects, and the naive reading "the core is the dual feasible set" is false: large payoffs are dual feasible and violate (3.5).

Formalization scope

Lean represents sellers and buyers as types M, N with [Fintype M] [Fintype N]; no nonemptiness is assumed, so markets with an empty side are included (there the core is $\{0\}$). The matrix is a : M → N → ℝ with the standing hypothesis ∀ i j, 0 ≤ a i j on every theorem. A coalition is a pair (A, B) : Finset M × Finset N. A matching is a Finset (M × N) inside A ×ˢ B with no repeated seller and no repeated buyer. The worth is Finset.sup' over the finite, nonempty set of matchings (the empty matching is always present), so there is no junk value. The paper's (2.6) takes exactly $k = \min(|S\cap M|, |S\cap N|)$ pairs; the formal definition takes all partial matchings, which gives the same maximum because $a \ge 0$.

Payoff vectors are pairs (M → ℝ) × (N → ℝ). The core is defined by (3.5) and (3.6) for all coalitions; nonnegativity is not a separate clause since it follows from singleton coalitions. The dual LP keeps the nonnegativity of $u$ and $v$ that (3.3) imposes, and "solutions of the LP dual" is read as optimal solutions (DualOptimal: dual feasible and of minimal objective among dual-feasible vectors), as the text preceding Theorem 2 does.

The worth is the combinatorial maximum, not the LP value, and the core is defined by coalitions, not through the dual; defining either through the other would make Theorem 2 true by unfolding, and such a formalization is ruled out. Likewise the goal is not the weaker "core = dual feasible set", which is false.

Contributions welcome: integrality of the rectangular inequality-form assignment polytope, a specialisation of general LP duality to this pair, and the coalitional inequality (3.6). The first two are reusable for any bipartite matching model.

Selected references

• 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
• G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179
• L. S. Shapley, Complements and substitutes in the optimal assignment problem, Naval Research Logistics Quarterly 9 (1962), 45–48. https://doi.org/10.1002/nav.3800090106
• G. Demange, D. Gale and M. Sotomayor, Multi-Item Auctions, Journal of Political Economy 94 (1986), 863–872. https://doi.org/10.1086/261393

Motivation

Large retailers pay their suppliers weeks or months after delivery, and small suppliers fill the gap with short-term finance. In factoring the supplier sells the receivable to a factor for immediate cash; in reverse factoring the retailer arranges the program with a bank, which pays the supplier early at a rate priced on the retailer's credit rating. Retailers commonly attach a condition: the supplier must accept a longer payment term. Wuttke et al. (Journal of Operations Management, 2019) report that buyers extended payment terms by 54 days on average on adopting reverse factoring and that many suppliers delayed adoption; Corsten (2010) reports suppliers resisting a program because of the demanded payment delay (both as cited by Kouvelis and Xu, pp. 6082–6083). How long an extension a retailer can demand, and what it gains by demanding it, is therefore a practical design question.

Kouvelis and Xu (Management Science 67(10), 2021) answer it inside a Stackelberg supply chain model with credit and liquidity risk. This mission formalizes their answer, Proposition 6 of §5.3: the retailer's optimal payment extension when she keeps the existing wholesale price.

Setting

Demand $D\ge0$ has density $f$, distribution function $F$ and $\bar F=1-F$; $f>0$ on $[0,\mathbb Z]$ with $\mathbb Z\le+\infty$ the upper end of the support, $f$ is continuous there, the mean is finite, and the failure rate $z(\xi)=f(\xi)/\bar F(\xi)$ is strictly increasing. Write $S(q)=\int_0^q\bar F(\xi)\,d\xi$ for expected sales and $k(q)=S(q)/\bar F(q)$.

A retailer (the leader) sets a wholesale price $w$, and a capital-constrained supplier (the follower) chooses a production quantity $q\ge0$; the retail price $p$ exceeds the unit cost $c$. Each firm $j\in\{s,r\}$ has a credit rating $C_j\in(C_{\min},C_{\max})$, a default probability $\rho_j=\rho(C_j)\in[0,1]$ with $\rho$ strictly decreasing, and an interest premium $\eta_j=\eta(C_j)>0$ with $\eta$ decreasing. The lead time is $t_1$, the payment term $t_2$, and $\lambda_s,\lambda_r\ge0$ are the liquidity risks.

Under a post-shipment scheme with coefficient $\Lambda$ the supplier earns

$$\pi(q;w)=(1-\rho_s)\bigl(\Lambda e^{-\lambda_s t_1}wS(q)-c\,q\,e^{\eta_s t_1}\bigr),$$

with $\Lambda_{\mathcal F}=(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}$ (recourse factoring), $\Lambda_{\mathcal N}=e^{-\eta_r t_2}(1-\rho_r)$ (non-recourse factoring) and $\Lambda_{\mathcal R}=e^{-\eta_r(t_2+\tau)}$ (reverse factoring with payment extension $\tau\ge0$). The retailer earns $\Pi=e^{-\lambda_s t_1}(1-\rho_r)(p-w)S(q)$ under factoring and

$$\Pi_{\mathcal R}(w,\tau)=e^{-\lambda_s t_1}(1-\rho_r)(2-e^{-\lambda_r\tau})(p-w)S(q_{\mathcal R})$$

under reverse factoring, where $q_{\mathcal R}$ is the supplier's best response. Its first-order condition is $w\bar F(q_{\mathcal R})=c_{\mathcal R}(\tau)=c\,e^{(\eta_s+\lambda_s)t_1+\eta_r(t_2+\tau)}$ (Eq. (12)).

Before reverse factoring, the supplier uses the better of the two factoring schemes. By Proposition 4 this is non-recourse, with equilibrium $(w^*_{\mathcal N},q^*_{\mathcal N})$, when $\mathbb C_{\mathcal N}<C_s\le\mathbb C_1$, and recourse, with $(w^*_{\mathcal F},q^*_{\mathcal F})$, when $C_s>\mathbb C_{\mathcal F}\vee\mathbb C_1$. The retailer keeps the existing wholesale price $w_s$ and solves problem (13): maximize $\Pi_{\mathcal R}(w_s,\tau)$ over $\tau\ge0$, subject to the supplier's acceptance (his reverse factoring profit is at least his existing one). $\mathbb C^{\max}_{\mathcal R}$ is the rating at which $\Lambda_{\mathcal F}=e^{-\eta_r t_2}$, and $\Xi_{[0,z]}(x)=\max\{0,\min\{z,x\}\}$.

Formalization targets

Goal: Proposition 6

(i) If $C_s\ge\mathbb C^{\max}_{\mathcal R}$, reverse factoring is dominated by recourse factoring. (ii) If $\mathbb C_{\mathcal N}<C_s<\mathbb C^{\max}_{\mathcal R}$, reverse factoring should be offered with

$$\tau^*_{\mathcal R}=\Xi_{[0,\tau_s]}(\tau^*_0),\qquad \lambda_r k(q)z(q)+\eta_r=2\eta_r e^{\lambda_r\tau^*_0},\quad w_s\bar F(q)=c_{\mathcal R}(\tau^*_0),$$

where $\tau_s=-\eta_r^{-1}\ln(1-\rho_r)$ with $w_s=w^*_{\mathcal N}$ in the non-recourse case, and $\tau_s=-\eta_r^{-1}\ln[(1-\rho_r)+(1-\rho_s)-e^{\eta_s t_2}]-t_2$ with $w_s=w^*_{\mathcal F}$ in the recourse case.

Milestones, in attack order

1. Eq. (12): the supplier's best response under reverse factoring.
2. Proposition 4: which factoring scheme is in force before reverse factoring.
3. §5.3, $\tau_s$: acceptance holds exactly on $[0,\tau_s]$.
4. §5.3, $\tau^*_0$: the retailer's unconstrained profit is unimodal around $\tau^*_0$.

A follow-on item states Corollary 3(ii): the retailer's profit strictly increases, and the supplier's profit is unchanged when $\tau^*_0\ge\tau_s$.

Significance

Proposition 6 is the paper's prescription for program design. It says which suppliers should be offered reverse factoring: every supplier below the indifference rating $\mathbb C^{\max}_{\mathcal R}$ and above the non-recourse feasibility threshold. It also gives the extension in closed form, the unconstrained optimum clipped to the supplier's acceptance limit. Two consequences are drawn in the paper: non-recourse factoring is dominated once the extension is optimized, and reverse factoring may leave the supplier exactly as well off as before, so it is not necessarily a win-win (Corollary 3).

The proofs are in the paper's Online Appendix B and have not been machine-checked. A formal proof here produces a checked derivation of the projection formula from the model's primitives. It covers the strict-IFR analysis of the follower's response, the reduction of the acceptance constraint to an interval, and the unimodality of the retailer's objective. The same analysis of the pull game with an effective unit cost recurs across the supply chain finance literature.

Difficulty

The retailer's objective depends on $\tau$ through two opposing channels: the liquidity factor $2-e^{-\lambda_r\tau}$ increases, while expected sales $S(q_{\mathcal R}(\tau))$ decrease because the supplier's effective cost rises. Neither factor is concave in $\tau$, and the objective need not be concave. The natural move, to set the derivative to zero and call the root a maximum, proves nothing without a sign analysis. That analysis needs the monotonicity of $k\cdot z$ along the implicitly defined response $q_{\mathcal R}(\tau)$, which is where strict IFR enters. The acceptance constraint compares the supplier's profits in two different games (reverse factoring at $\tau$ against the existing equilibrium). Reducing it to $\tau\le\tau_s$ requires the supplier's best-response profit as an explicit increasing function of his quantity. Identifying the existing equilibrium requires Proposition 4, whose "adopted" compares equilibrium profits of two Stackelberg games.

Formalization scope

The model is a single Lean structure SupplyChainFactoring.Extension.Model. Demand is a probability measure on $\mathbb R$ with a density $f$, and $\mathbb Z$ is an extended real. "Continuous p.d.f. with $f>0$ in $[0,\mathbb Z]$" is read as continuity on $[0,\mathbb Z]$, with $f=0$ outside the support. Credit functions $\rho,\eta$ are real functions constrained on $(C_{\min},C_{\max})$. The finance derivations behind the profit functions (Eqs. (1), (5), (6), Lemma 1) are not formalized: the profit functions are the model.

Readings of informal words, each also recorded in the item's Formalization Note:

• Best response: a maximizer of the supplier's profit over $q\ge0$; equilibrium: a best response pair from which no nonnegative wholesale price with a best response gives the retailer more. Neither is defined through first-order conditions.
• Feasible: some $w\ge0$ with a best response gives the retailer positive profit; adopted (Proposition 4): feasible, with equilibrium supplier profit at least (non-recourse) or strictly above (recourse) the other feasible scheme's.
• Thresholds "the unique value of $C_s$ that satisfies …" are hypotheses in exactly that form; $c_{\mathcal N}=p$ and $c_{\mathcal F}=p$ are cross-multiplied because $\Lambda_{\mathcal F}$ can be $\le0$.
• In (13) $w$ is fixed at $w_s$ (§5.3's first sentence, footnote 23). $\pi^*_{\mathcal R}$ is the supplier's best-response profit under reverse factoring at $(w_s,\tau)$, and $\max\{\pi^*_{\mathcal F},\pi^*_{\mathcal N}\}$ is his profit in the existing equilibrium.
• Dominated (Proposition 6(i)): at every $\tau\ge0$ and every $w$, the supplier's reverse factoring best-response profit is at most his recourse one. Should be offered (6(ii)): $\tau^*_{\mathcal R}$ solves (13) and the retailer's profit is at least her existing equilibrium profit.
• $\tau^*_0$ is a hypothesis: it and some $q\in(0,\mathbb Z)$ solve the paper's two equations (the paper does not argue existence). Its optimality "without the nonnegativity constraint" is stated as unimodality of $\Pi_{\mathcal R}$ on the set of real $\tau$ with $c_{\mathcal R}(\tau)<w$.
• Always increases (Corollary 3(ii)) is strict; may remain unchanged when $\tau^*_0\ge\tau_s$ is read as "is unchanged whenever $\tau^*_0\ge\tau_s$".

Three misprints of the paper are corrected: $\Xi_{[0,z]}(x)=0$ "if $x<z$" is read as "if $x<0$"; "the retailer's maximization problem in (16)" refers to (13); the middle line of the $\Pi_{\mathcal R}$ display on p. 6082 carries a stray factor $w$, and the last line is used.

The hypotheses on $\tau^*_0$ cannot be met when $\lambda_r=0$, and the goal then says nothing about the case, as in the paper. The existing equilibrium, $\tau_s$ and $\tau^*_0$ are never free parameters: $\tau_s$ is the paper's explicit formula, and the reduction of acceptance to $\tau\le\tau_s$ is a milestone to be proved, not an assumption. Every logarithm is applied to a quantity the hypotheses force positive. A formalization that assumed acceptance equivalent to $\tau\le\tau_s$ or assumed unimodality would be trivial and is excluded.

The pull game with an effective cost has the same structure as Cachon's pull contract without salvage value (platform items CachonPushPull.*), but those items assume IGFR demand with a salvage value, so they are not reused. Reusable infrastructure welcome: the strict-IFR lemmas ($k$, $k\cdot z$ and $k(q)-q$ increasing) and the explicit best response of a newsvendor-type follower.

Selected references

• P. Kouvelis, F. Xu, A Supply Chain Theory of Factoring and Reverse Factoring, Management Science 67(10):6071–6088, 2021. https://doi.org/10.1287/mnsc.2020.3788
• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• D. A. Wuttke, E. S. Rosenzweig, H. S. Heese, An Empirical Analysis of Supply Chain Finance Adoption, Journal of Operations Management 65(3):242–261, 2019. https://doi.org/10.1002/joom.1023

Motivation

Von Neumann's minimax theorem says that in a zero-sum game with real payoffs, Player I can guarantee an expected gain of at least the value $v$ and Player II can hold it to at most $v$. In a long series of plays, the law of large numbers turns this into a statement about the average payoff: I can make it exceed $v-\varepsilon$, II can keep it below $v+\varepsilon$, with probability approaching one.

Blackwell's 1956 paper asks the same question when the payoff of each play is a vector in $\mathbb R^N$ rather than a number. A single player then cannot optimize "the" payoff, and the natural question becomes geometric: can a player force the running average of the payoff vectors to converge to a prescribed set $S$, whatever the opponent does? The resulting notion, approachability, became a basic tool in repeated games with incomplete information (Aumann–Maschler), in the theory of calibration and regret minimization (Foster–Vohra; Hart–Mas-Colell), and in online learning, where no-regret algorithms and Blackwell approachability are known to be equivalent (Abernethy–Bartlett–Hazan 2011).

Timeline.

• 1928: von Neumann's minimax theorem for matrix games.
• 1954: Blackwell's maximal inequality for sums with negative conditional drift (On optimal systems, Ann. Math. Statist.), quoted in this paper as THEOREM 2.
• 1956: this paper. A sufficient condition for approachability (THEOREM 1), a complete characterization for closed convex sets (THEOREM 3) and for $N=1$, an example of a set that is neither approachable nor excludable, and a conjecture on weak approachability.
• 1992: Vieille proved Blackwell's conjecture that every set is weakly approachable or weakly excludable.

Setting

Fix integers $N\ge0$ and $r,s\ge1$, and a closed, bounded, convex set $X\subseteq\mathbb R^N$. The game is an $r\times s$ matrix $M=\|m(i,j)\|$ whose entries are probability distributions concentrated on $X$. Write $\bar m(i,j)$ for the mean of $m(i,j)$, $P$ for the simplex of mixed actions $p=(p_1,\dots,p_r)$ of Player I, and $Q$ for that of Player II.

A strategy $f=\{f_n\}_{n\ge0}$ of I is a sequence of measurable maps from the $n$-tuples $(x_1,\dots,x_n)$ of past outcomes to $P$; $f_0$ is a point of $P$. Strategies $g=\{g_n\}$ of II take values in $Q$. A play of $(f,g)$ is a sequence of random vectors $x_1,x_2,\dots$ such that, given $x_1,\dots,x_n$, the players draw $i$ and $j$ independently from $f_n(x_1,\dots,x_n)$ and $g_n(x_1,\dots,x_n)$, and $x_{n+1}$ is drawn from $m(i,j)$. The average payoff is $\bar x_n=\frac1n\sum_{i=1}^n x_i$, and $\delta_n$ is its distance from $S$.

A set $S\subseteq\mathbb R^N$ is approachable with $f^*$ if for every $\varepsilon>0$ there is $N_0$ such that for every strategy $g$ of II,

$$\mathrm{Prob}\{\delta_n\ge\varepsilon\text{ for some }n\ge N_0\}<\varepsilon .$$

It is excludable with $g^*$ if there is $d>0$ such that for every $\varepsilon>0$ there is $N_0$ such that for every strategy $f$ of I,

$$\mathrm{Prob}\{\delta_n\ge d\text{ for all }n\ge N_0\}>1-\varepsilon .$$

$S$ is approachable (excludable) if some strategy approaches (excludes) it. Finally, for $p\in P$ and $q\in Q$,

$$R(p)=\operatorname{conv}\Big\{\textstyle\sum_i p_i\bar m(i,j)\Big\}_{j=1}^{s},\qquad T(q)=\operatorname{conv}\Big\{\textstyle\sum_j q_j\bar m(i,j)\Big\}_{i=1}^{r}:$$

$R(p)$ is the set of expected payoffs I can guarantee to stay in by playing $p$, and $T(q)$ the set II can confine them to by playing $q$.

Formalization targets

Goal: THEOREM 3

For a closed convex set $S\subseteq\mathbb R^N$,

$$S\text{ is approachable}\iff S\cap T(q)\neq\emptyset\ \text{ for every }q\in Q,$$

and if $S\cap T(q_0)=\emptyset$ then $S$ is excludable with the stationary strategy $g_n\equiv q_0$. In particular every closed convex set is either approachable or excludable. Both sentences are part of the goal.

Milestones, in the paper's order

1. THEOREM 2: for $|z_k|\le1$ with $E(z_k\mid z_1,\dots,z_{k-1})\le-u\,E(|z_k|\mid z_1,\dots,z_{k-1})$ and $0<u<1$,

$$\mathrm{Prob}\{z_1+\dots+z_k\ge t\text{ for some }k\}\le\Big(\tfrac{1-u}{1+u}\Big)^t .$$

2. The LEMMA: a sequence satisfying the almost-supermartingale conditions (5), (6), (7) converges to $0$ at a rate depending only on the constants $a,b,c$.
3. In the proof of THEOREM 1, the squared distances $\delta_n^2$ satisfy (5)–(7) uniformly in II's strategy.
4. THEOREM 1: if every $x\notin S$ admits $p(x)\in P$ such that the hyperplane through a closest point $y\in S$, perpendicular to $xy$, separates $x$ from $R(p(x))$, then $S$ is approachable with any strategy playing $p(\bar x_n)$ when $\bar x_n\notin S$.
5. No set is both approachable and excludable.
6. If a closed $S$ is approachable in the transpose $M'$ with $f$, then every closed $T$ disjoint from $S$ is excludable in $M$ with $f$.
7. A closed convex $S$ meeting every $T(q)$ satisfies THEOREM 1's hypothesis.
8. Every $T(q_0)$ is approachable in $M'$ with $f_n\equiv q_0$.

Significance

The result. THEOREM 3 is the vector analogue of the minimax theorem. For a closed convex target it reduces an infinite-horizon stochastic question, about every strategy of the opponent over all histories, to a finite family of one-shot conditions on the mean matrix $\bar M$, and it shows that the game is determined for convex targets: one of the two players always wins. Its sufficient condition, THEOREM 1, is the origin of the "Blackwell strategy", which steers the average toward the target by playing, at each step, a mixed action that pushes the expected next payoff across the supporting hyperplane. Regret-matching, calibration algorithms and the reductions between online linear optimization and approachability are instances of this construction.

Formalizing it. The result is proved in the paper; to the best of available knowledge no machine-checked proof of it exists. This mission produces one: the stochastic model of a repeated game with vector payoffs, the probabilistic estimates (THEOREM 2 and the LEMMA) with the uniform rate the paper claims, and the minimax reduction for convex sets. A related platform mission, Introduction to Online Convex Optimization XIII, states a deterministic, sufficiency-only textbook variant for bounded sets; the present mission covers the stochastic model, unbounded convex targets, and the excludability half.

Difficulty

The obvious argument shows that the expected squared distance $E\delta_n^2$ decreases like $1/n$. That is not approachability: the definition asks for the probability that the average is ever again $\varepsilon$-far after time $N_0$, uniformly over the opponent's strategies. Controlling the whole tail of the path, with a threshold $N_0$ that does not depend on the opponent, is the step that fails for a naive expectation bound and is why the paper needs a maximal inequality for sums with negative conditional drift. On the geometric side, the "only if" direction is not automatic: it requires that approachability and excludability be incompatible, which in turn requires that a play of every pair of strategies exists.

Formalization scope

Points live in EuclideanSpace ℝ (Fin N); pure actions are Fin r and Fin s; mixed actions are elements of stdSimplex. The game is a structure carrying $X$ (closed, bounded, convex) and the distributions $m(i,j)$ (probability measures with $m(i,j)(X^{c})=0$). A play is described by the conditional law of the next outcome given the past, and approachability and excludability quantify over every probability space in Type carrying such a play. Distances are extended (Metric.infEDist), equal to $+\infty$ to the empty set.

Conventions and disclosed additions:

• $r,s\ge1$ where a statement needs both players to have strategies;
• strategies are measurable in the history;
• outcomes are indexed from $1$; (5) and (7) start at $n=2$, (6) at $n=1$;
• "the closest point" in THEOREM 1 is some closest point, and "separates" is weak separation;
• THEOREM 2 is stated with $E(|z_k|\mid\cdot)$ in place of the printed "max" (the weaker hypothesis, as in the cited source), and with $u<1$ so that $((1-u)/(1+u))^t$ is a real power.

$S$ is not assumed bounded or nonempty. With the real-valued distance, the empty set would be approachable with every strategy and THEOREM 3 would be false; the extended distance rules this out. Stating only the sufficiency direction, fixing the approaching strategy in the hypotheses, or assuming a play exists would each trivialize the goal, and none is done.

A complete development needs: conditional laws of the next outcome from a strategy pair (Ionescu–Tulcea, Kernel.traj in Mathlib), a nonnegative-supermartingale maximal inequality, the metric projection onto closed convex sets, and the minimax theorem (Mathlib's Sion theorem). The maximal inequality of THEOREM 2 and the LEMMA are reusable beyond this mission. Contributions to any milestone, and to a construction of plays, are welcome.

Selected references

• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific J. Math. 6(1):1–8, 1956. https://doi.org/10.2140/pjm.1956.6.1
• D. Blackwell, On optimal systems, Ann. Math. Statist. 25(2):394–397, 1954. https://doi.org/10.1214/aoms/1177728796
• N. Vieille, Weak approachability, Math. Oper. Res. 17(4):781–791, 1992. https://doi.org/10.1287/moor.17.4.781
• J. Abernethy, P. Bartlett, E. Hazan, Blackwell approachability and no-regret learning are equivalent, COLT 2011. https://arxiv.org/abs/1011.1936
• S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68(5):1127–1150, 2000. https://doi.org/10.1111/1468-0262.00153

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark down later. When customers anticipate the markdown, some of them wait, and the seller's pricing problem becomes a game between the seller and a population of forward-looking (strategic) customers. Aviv and Pazgal (MSOM 10(3), 2008) study this game in a model with limited inventory, stochastic arrivals and valuations that decline over the season, under two classes of seller policies: contingent pricing, where the discount depends on the inventory left, and announced fixed-discount pricing, where the seller commits to both prices upfront. Their numerical study (§7.3) compares the two classes and finds that precommitment can raise expected revenue by up to about 8%.

That comparison needs, for every announced price path, the customers' equilibrium response. Theorem 2 of the paper (p. 348) supplies it: a threshold purchasing policy, pinned down by a scalar fixed-point equation for the probability that a waiting customer is served. This mission formalizes Theorem 2. A companion mission of the same series formalizes Theorem 1, the contingent-pricing counterpart.

Setting

A seller has $Q \ge 1$ units to sell over a season $[0, H]$, split at a fixed time $T$ with $0 < T \le H$. Customers arrive by a Poisson process with rate $\lambda > 0$. Customer $j$ has a base valuation $V_j$ drawn from a continuous distribution $F$ (tail $\bar F = 1 - F$), and at time $t$ values the product at $V_j(t) = V_j e^{-\alpha t}$, where the decline factor $\alpha \ge 0$ is common to all customers.

Under an announced price path the seller commits to a premium price $p_1$ on $[0, T)$ and a discount price $p_2 \le p_1$ from $T$ on; $p_2$ does not depend on the remaining inventory. Customers know the initial inventory but not the current one.

A customer arriving at $t < T$ buys immediately if and only if (i) the current surplus $V(t) - p_1$ is nonnegative and (ii) it is at least the expected surplus of waiting,

$$\omega\cdot\max\{V(T) - p_2, 0\},$$

where $\omega$ is the probability that a unit will be allocated to the customer at time $T$. Units left at $T$ are rationed at random among the customers who request one.

For a threshold function $\psi$ on $[0, T)$ the paper defines three segment rates: $\Lambda_I(\psi)$, the expected number of customers who buy at $p_1$; $\Lambda_S(\psi, p_1, p_2)$, those who could buy at $p_1$ but wait and want to buy at $p_2$; and $\Lambda_W(p_1, p_2)$, those whose valuation was below $p_1$ and who want to buy at $p_2$. Each is $\lambda$ times an integral over $[0, T]$ of $\bar F$ at scaled prices (p. 345). With $P(x \mid \Lambda)$ the Poisson probabilities, the allocation probability of $q$ units is

$$A(q \mid \Lambda) = \sum_{y=0}^{\infty} \frac{q}{\max\{1+y, q\}}\,P(y \mid \Lambda).$$

Formalization targets

Goal: Theorem 2 (p. 348)

For $w \in [0,1]$ let

$$\psi_A(t) = \max\left\{p_1, \frac{p_1 - wp_2}{1 - we^{-\alpha(T-t)}}\right\},\qquad 0 \le t < T, \tag{7}$$

and suppose $w$ solves

$$w = \sum_{x=0}^{Q-1} P\big(x \mid \Lambda_I(\psi_A)\big)\cdot A\big(Q-x \mid \Lambda_S(\psi_A, p_1, p_2) + \Lambda_W(p_1, p_2)\big). \tag{8}$$

Then, when all other customers use $\psi_A$ (so that a waiting customer is served with the probability on the right of (8)), every customer arriving at $t \in [0, T)$ buys immediately if and only if $V(t) \ge \psi_A(t)$: the symmetric threshold profile is a Nash equilibrium.

Milestones: the two cases of the proof (p. 358)

1. If $e^{-\alpha(T-t)} \le p_2/p_1$, the threshold is $p_1$.
2. If $e^{-\alpha(T-t)} > p_2/p_1$, the threshold is $(p_1 - wp_2)/(1 - we^{-\alpha(T-t)}) \ge p_1$.

Significance

Theorem 2 reduces the customers' equilibrium under an announced path to a single scalar $w$. Everything downstream in §5 and §7 rests on it: the seller's expected revenue $\pi_{A/S}(p_1, p_2)$ (p. 348) is written in terms of $\psi_A$, the seller's optimal announced path maximizes it, and the comparison between announced and contingent pricing uses the resulting value $\pi^*_{A/S}$. The theorem also explains the qualitative prediction of the model: the threshold exceeds $p_1$ exactly when the announced discount is deep relative to the decline of valuations, and it rises with the perceived availability $w$.

The result is proved in the paper; to the best of our search it has no machine-checked proof. A formal development contributes the model objects (segment rates for threshold policies, the allocation probability for random rationing among Poisson requesters) in a form reusable by the rest of the series and by other strategic-customer pricing models, and a checked proof of the equilibrium property. The existence of a solution to (8) is not proved in the paper and is a natural further target.

Difficulty

The best-response part of the argument is elementary once the availability is known. The substance of the statement lies in the availability itself: the probability that a waiting customer is served is not a free parameter but the one generated, through (8), by the other customers' use of the same threshold. A formalization must connect the segment rates, the Poisson counts and random rationing into one expression and keep the fixed-point coupling between $w$ and $\psi_A$ intact; dropping it turns the theorem into a one-line inequality about an arbitrary $w$. The division by $1 - we^{-\alpha(T-t)}$ also degenerates when $w = 1$ and $\alpha = 0$, and has to be excluded explicitly.

Formalization scope

The Lean development lives in namespace SeasonalPricing.Announced. Conventions:

• Time is real; base valuations have law μ : Measure ℝ with IsProbabilityMeasure μ, $F$ = ProbabilityTheory.cdf μ, and continuity of $F$ (the paper's "continuous distribution") is a hypothesis of the goal. No support condition on $[0,\infty)$ is imposed; the statement quantifies over every real base valuation $V$.
• $\Lambda_I, \Lambda_S, \Lambda_W$ are interval integrals over $[0, T]$ exactly as printed. $P(x \mid \Lambda) = e^{-\Lambda}\Lambda^x/x!$ is written out; $A(q\mid\Lambda)$ is the infinite series (tsum) as printed, not its closed form.
• availability is the right-hand side of (8), with $\psi_A$ built from $w$ by (7).

Readings of the paper's informal words:

• "Nash equilibrium" is read as the best-response property the paper's proof checks: against the availability generated by (8), the immediate-purchase rule of p. 344 coincides with the threshold $\psi_A$ at every $t \in [0, T)$ and every valuation. The paper defines no strategy space beyond threshold rules.
• "$w$ is a solution to (8)": the theorem is conditional on a solution; its existence is neither assumed elsewhere nor claimed. The conditional statement has content only when (8) has a solution, which the paper does not prove.
• $w$ as a likelihood: $0 \le w \le 1$ is a hypothesis (it also follows from (8)).
• Added hypothesis: $\alpha > 0$ or $w < 1$, which keeps $1 - we^{-\alpha(T-t)} > 0$ for $t < T$; the paper's formula is undefined when it fails. In the milestones the same condition appears as $we^{-\alpha(T-t)} < 1$, and $0 < p_1$ is added so that $p_2/p_1$ is meaningful.
• The rule on $[T, H]$ (buy at $T$ iff $V(T) > p_2$) is part of the model and is not restated; $H$ does not enter the statements.

A formalization in which $w$ is an arbitrary number in $[0,1]$, not tied to (8), is ruled out: it is the best-response lemma alone, not Theorem 2. Contributions welcome: proofs of the two milestones and the goal; lemmas such as $0 \le A(q\mid\Lambda) \le 1$ and summability of its series; the closed form of $A(q \mid \Lambda)$ printed on p. 346; and an existence result for (8).

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667

Motivation

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

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

Timeline.

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

Setting

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

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

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

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

The topological vocabulary is Debreu's §1:

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

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

Formalization targets

Goal: the THEOREM (p. 888)

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

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

Milestones on the path of the proof

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

Further results of the paper

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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