Algorithmic Game Theory

Motivation

When indivisible goods are shared among people, comparing each person's bundle with another person's bundle is only one way to judge fairness. A second test asks whether a group could repartition the goods it collectively received so that one of its members would reliably obtain more. Groupwise maximin share (GMMS) makes this test for every subgroup. It strengthens the ordinary maximin-share benchmark, which tests only the grand coalition and all goods. Chaudhury, Kavitha, Mehlhorn and Sgouritsa use this distinction to study a complete allocation obtained from their almost envy-free allocation: goods initially left unassigned are given to one unenvied agent. Their Theorem 16 proves that the resulting allocation gives every agent at least four sevenths of her groupwise maximin share under additive valuations. Chaudhury et al., pp. 4–5, 15–16.

The paper first constructs a partial EFX allocation whose unallocated goods have bounded value to every agent. Its Section 3 then assumes additive valuations and derives maximin-share and GMMS guarantees. This mission addresses the GMMS consequence of that construction. The existence of the starting allocation is the subject of the first mission in this series; the present theorem specifies what happens when its pool is donated. Chaudhury et al., Theorems 8 and 16.

Setting

Let $N$ be a finite set of agents and $M$ a finite set of indivisible goods. Each agent $i$ has a valuation $v_i(S)$ for a bundle $S\subseteq M$. Here valuations are nonnegative and additive: $v_i(S)$ is the sum of the values of the individual goods in $S$. A partial allocation $X=(X_i)_{i\in N}$ gives pairwise disjoint bundles to the agents. The remaining goods form its pool, $P=M\setminus\bigcup_{i\in N}X_i$. An allocation is complete when its pool is empty. These are the paper's allocation conventions. Chaudhury et al., pp. 3–4.

An allocation is envy-free up to any good (EFX) if, after any single good $g$ is removed from agent $j$'s bundle, agent $i$ values that remainder no more than her own bundle: $v_i(X_j\setminus\{g\})\le v_i(X_i)$ for all $i,j$ and $g\in X_j$. The envy graph has a directed edge $i\to j$ when $i$ values $j$'s bundle more than her own. A source is a vertex with no incoming edge, so nobody envies that agent. Chaudhury et al., pp. 3, 8.

For a set $S$ and a positive number $k$ of parts, $\operatorname{MMS}_i(k,S)$ is the largest worst-part value agent $i$ can secure by partitioning $S$ into $k$ bundles. A complete allocation $Y$ is $\alpha$-GMMS when each agent meets an $\alpha$ fraction of this benchmark for every subgroup containing her:

$$v_i(Y_i)\ge\alpha\operatorname{MMS}_i\!\left(|N'|,\bigcup_{j\in N'}Y_j\right) \qquad(N'\subseteq N,\ i\in N').$$

The benchmark uses only goods allocated to that subgroup. The paper states it both as a complete-allocation property in its introduction and in Definition 15. Chaudhury et al., pp. 5, 15.

Formalization targets

The donated allocation

Assume $X$ is partial and EFX, every agent satisfies $v_i(P)\le v_i(X_i)$, and $s$ is a source of its envy graph. Define $Y_s=X_s\cup P$ and $Y_j=X_j$ for $j\ne s$. The goal states that $Y$ is complete, that donation does not lower any agent's own value, and that

$$v_i(Y_i)\ge\frac47\operatorname{MMS}_i\!\left(|N'|,\bigcup_{j\in N'}Y_j\right) \qquad(N'\subseteq N,\ i\in N').$$

This is the GMMS bullet of Theorem 16 applied to the particular allocation the authors define immediately before it. The paper obtains a suitable $X$ from Lemma 12, which has the relevant properties of Theorem 8. Chaudhury et al., pp. 11–12, 14–16.

Intermediate results

The milestones are Proposition 13, the reduction step in Theorem 16's proof, and all three parts of Lemma 17. Proposition 13 compares maximin shares after deleting agents and at most as many goods. Lemma 17 bounds the value of each bad good, the donated bundle, and the other good bundles. They retain the constants $2$ and $3/2$ used in the paper. Chaudhury et al., pp. 14, 16–17.

Significance

The result turns an almost envy-free partial allocation into a complete allocation with a guarantee for every coalition. A plain maximin-share statement would only compare each agent with a partition of all goods among all agents; here every subgroup and its allocated goods count. The distinction matters even when an ordinary maximin-share bound is easy to meet because there are fewer goods than agents. Chaudhury et al., p. 5.

The paper proves Theorem 16 mathematically. The remaining work for this mission is a machine-checked proof of its stated GMMS consequence and its supporting results. Its definitions of partial allocation, pool, finite maximin share and groupwise guarantee can also serve later formalizations of fair division. The Nash-social-welfare half-guarantee in the printed theorem depends on the starting allocation from Lemma 12; this mission records only the value preservation under donation. Chaudhury et al., pp. 14, 16.

Difficulty

Giving all leftover goods to one agent makes the allocation complete, but it can change how another agent values that enlarged bundle and how a subgroup's benchmark is calculated. EFX alone compares bundles after deleting one good; GMMS compares an agent with every repartition of a subgroup's goods. The difficulty is to control those repartitions while keeping the exact $4/7$ constant. Merely applying an ordinary maximin-share bound to the grand coalition does not establish the required subgroup inequalities. Chaudhury et al., pp. 15–17.

Formalization scope

Agents and goods are represented by Fin n and Fin m; Lean numbers agents from zero, and the paper's “agent 1” is an explicit source $s$. Bundles are finite sets. Valuations are real-valued but include nonnegativity alongside additivity, representing the paper's codomain $\mathbb R_{\ge0}$. The pool is computed from $X$, and the donated allocation is a function of $X$ and $s$. No independent pool or arbitrary completed allocation is allowed. Completeness is a conclusion. The maximin share is a finite maximum of finite minima over labelled partitions, which may have empty parts. Every use has a positive part count; in the GMMS definition this follows from $i\in N'$. Cardinality is converted to real numbers before fractions are formed. These choices exclude zero-part maximin shares and integer division. Chaudhury et al., pp. 3–5, 15–16.

The theorem is conditional on the EFX and pool-value properties of the source allocation, rather than repeating its existence proof. It states the conclusion for every such allocation and every source. The paper's half-optimal-Nash-social-welfare bullet is outside this mission because it invokes the separate black-box starting allocation of Lemma 12. Contributions toward finite-partition comparisons, EFX value bounds, and the groupwise estimate are welcome. Chaudhury et al., pp. 14–17.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn and A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, SIAM Journal on Computing, 2021. Formalization source: arXiv:1907.04596v3.

Fair division of indivisible goods

A set of $n$ agents must share a set $M$ of $m$ indivisible goods, each agent valuing bundles of goods by her own valuation. Two fairness notions dominate the literature. Envy-freeness up to any good (EFX), introduced by Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang (EC 2016), asks that no agent prefer another's bundle once any single good is removed from it. The maximin share (MMS), proposed by Budish (JPE 2011), asks that every agent receive at least what she could secure by splitting the goods into $n$ bundles herself and taking the worst one.

Neither notion is known to be achievable in full. Whether complete EFX allocations always exist is open in general. Complete MMS allocations need not exist: Procaccia and Wang (EC 2014) gave a counterexample with three agents, and the best known approximation factors for additive valuations are $3/4-\varepsilon$ (Ghodsi et al., EC 2018) and $3/4$ (Garg and Taki, arXiv:1903.00029). Amanatidis, Birmpas and Markakis (IJCAI 2018) showed that every complete EFX allocation is a $4/7$-MMS allocation.

Caragiannis, Gravin and Huang (EC 2019) showed that EFX can be achieved if some goods are left unallocated, with no bound on how many. Chaudhury, Kavitha, Mehlhorn and Sgouritsa (arXiv:1907.04596, SODA 2020, SIAM J. Comput. 2021) relax completeness instead: some goods may be "donated to charity". Their Theorem 8 produces an EFX partial allocation in which nobody envies the donated set and the donated set has fewer goods than there are unenvied agents. This mission formalizes their Theorem 14: such an allocation also gives every agent a maximin-share guarantee that improves as more goods are donated.

Setting

Agents are $N=[n]$ and goods are $M$, $|M|=m$. Agent $i$ has a valuation $v_i:2^M\to\mathbb{R}_{\ge 0}$, assumed additive: $v_i(S)=\sum_{g\in S}v_i(\{g\})$ for every $S\subseteq M$.

A (partial) allocation $X=\langle X_1,\dots,X_n\rangle$ gives agent $i$ the bundle $X_i\subseteq M$, the bundles being pairwise disjoint. The pool of unallocated goods is $P=M\setminus\bigcup_i X_i$, and $k=|P|$.

• $X$ is EFX if $v_i(X_i)\ge v_i(X_j\setminus\{g\})$ for all agents $i,j$ and every $g\in X_j$.
• The envy graph $G_X$ has the agents as vertices and an edge $i\to j$ exactly when $v_i(X_i)<v_i(X_j)$. A source is a vertex of indegree zero: an agent nobody envies.
• The maximin share of agent $i$ over $k'\ge1$ bundles of a set $S$ of goods is

$$\mathrm{MMS}_i(k',S)=\max_{(S_1,\dots,S_{k'})}\ \min_{1\le j\le k'} v_i(S_j),$$

the maximum over partitions of $S$ into $k'$ possibly empty bundles. Agent $i$'s maximin share in the instance is $\mathrm{MMS}_i(n,M)$.

The three conditions of Theorem 8 on $(X,P)$ are:

1. $X$ is EFX;
2. $v_i(X_i)\ge v_i(P)$ for every agent $i$;
3. $|P|$ is less than the number of sources of $G_X$; in particular $|P|<n$.

Formalization targets

Goal: Theorem 14 (MMS bullet)

For every allocation $X$ with pool $P$ satisfying conditions 1–3, and every agent $i$,

$$v_i(X_i)\ \ge\ \frac{\mathrm{MMS}_i(n,M)}{2-\frac{k}{n}},\qquad k=|P|.$$

The factor ranges from $\tfrac12$ when $P=\emptyset$ to $(1+\tfrac1n)^{-1}$ when $|P|=n-1$.

Milestones

1. Proposition 13 (quoted by the paper from Garg, McGlaughlin and Taki, SOSA 2019): for $N'\subseteq N$ and $M'\subseteq M$ with $|N\setminus N'|\ge|M\setminus M'|$ and $i\in N'$,

$$\mathrm{MMS}_i(|N'|,M')\ \ge\ \mathrm{MMS}_i(|N|,M).$$

2. MMS is at most the proportional share: $\mathrm{MMS}_i(k',S)\le v_i(S)/k'$ for additive valuations and $k'\ge1$.
3. The EFX half-bound: if $X$ is EFX and $|X_j|\ge2$, then $v_i(X_i)\ge(1-1/|X_j|)\,v_i(X_j)\ge\tfrac12 v_i(X_j)$.
4. The counting step (summing inequalities (1)–(3) of the proof): with $N'$ the sources of $G_X$, agent $i$ and all agents holding at least two goods, $n'=|N'|$ and $M'=\bigcup_{j\in N'}X_j$,

$$(2n'-k)\,v_i(X_i)\ \ge\ v_i(M'\cup P).$$

Significance

Theorem 14 shows that leaving goods unallocated is not merely a cost: under conditions 1–3, each donated good buys a quantitative improvement of every agent's maximin-share guarantee, interpolating between the factor $\tfrac12$ the bound gives when the pool is empty and a factor tending to $1$ when nearly $n$ goods are donated. Together with Theorem 8 it shows that a single allocation can be simultaneously EFX, envy-free towards the charity, small in its charity, and approximately MMS. The same reduction (Proposition 13 applied to a carefully chosen sub-instance) is the template for the paper's $4/7$-groupwise-maximin-share result, Theorem 16, formalized in mission III of this series.

The result is proved in the paper; no machine-checked proof of it, of Proposition 13, or of the existence of EFX allocations with bounded charity is known to exist. The mission produces a formal maximin-share definition on arbitrary subsets of goods with an arbitrary number of bundles, a formal proof of the monotonicity of the maximin share under removal of agents and goods (Proposition 13, which the paper quotes without proof), and the guarantee itself. Combined with mission I of this series (Theorem 8), it yields the printed existence statement.

Difficulty

The guarantee compares an agent's own bundle with a benchmark defined over all partitions of all goods, while EFX and the source condition speak only about the allocation at hand. The obvious attempt, summing $v_i(X_i)\ge\tfrac12 v_i(X_j)$ over all agents and adding the pool, gives only a factor near $\tfrac12$ and ignores the pool's size. Agents holding a single good are the obstruction: EFX gives no bound on the value of their bundles relative to $v_i(X_i)$, and the benchmark $\mathrm{MMS}_i(n,M)$ is defined on the full instance, which contains them. Proposition 13, the comparison of maximin shares across instances, is a combinatorial statement about all partitions of the original instance and requires nonnegativity of the valuations: with a good of negative value it fails.

Formalization scope

Agents are Fin n (0-based) and goods Fin m; the set $M$ is the whole of Fin m. Valuations are functions Fin n → Finset (Fin m) → ℝ; additivity is the sum formula together with nonnegativity, which is the paper's codomain $\mathbb{R}_{\ge0}$. An allocation is a family of pairwise disjoint finsets and the pool is always computed as the complement of their union, never taken as a free parameter. Sources are agents of indegree zero in the envy graph (nobody envies them), not agents who envy nobody. The maximin share $\mathrm{MMS}(k',S)$ is a supremum over labellings Fin m → Fin k' restricted to $S$ of the minimum bundle value; it is used only with $k'\ge1$, which every statement has in its hypotheses or derives from them (in the goal, condition 3 forces $n\ge1$). Every cardinality is cast to $\mathbb{R}$ before division or subtraction, and $2-k/n>1$ under condition 3, so no division by zero occurs.

The goal is posed as an implication for every allocation satisfying conditions 1–3, rather than as the paper's "there exists an allocation"; the paper's proof of the MMS bullet uses only those three conditions, and existence is Theorem 8. The Nash-social-welfare bullet of Theorem 14 is not posed: it depends on Lemma 12, which takes the allocation of an earlier paper as a black box. The goal cannot be trivialized by a free pool, by overlapping bundles, by zero agents (condition 3 excludes them), by a junk maximin share over zero bundles, or by natural-number division; the statement keeps all three conditions, each of which is needed.

Contributions welcome: a library-quality maximin-share API for additive valuations (attainment of the maximum, monotonicity, the proportional bound), which is reusable for other MMS results; proofs of the milestones; and the final assembly.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn, A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, SIAM J. Comput. 50(4), 2021; cited from arXiv:1907.04596v3. https://arxiv.org/abs/1907.04596
• E. Budish, The Combinatorial Assignment Problem: Approximate Competitive Equilibrium from Equal Incomes, J. Political Economy 119(6), 2011. https://doi.org/10.1086/664613
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah, J. Wang, The Unreasonable Fairness of Maximum Nash Welfare, EC 2016. https://doi.org/10.1145/2940716.2940726
• A. D. Procaccia, J. Wang, Fair Enough: Guaranteeing Approximate Maximin Shares, EC 2014. https://doi.org/10.1145/2600057.2602835
• M. Ghodsi, M. HajiAghayi, M. Seddighin, S. Seddighin, H. Yami, Fair Allocation of Indivisible Goods: Improvements and Generalizations, EC 2018. https://doi.org/10.1145/3219166.3219238
• J. Garg, S. Taki, An Improved Approximation Algorithm for Maximin Shares, CoRR abs/1903.00029, 2019. https://arxiv.org/abs/1903.00029
• J. Garg, P. McGlaughlin, S. Taki, Approximating Maximin Share Allocations, SOSA 2019. https://doi.org/10.4230/OASIcs.SOSA.2019.20
• I. Caragiannis, N. Gravin, X. Huang, Envy-Freeness up to Any Item with High Nash Welfare: The Virtue of Donating Items, EC 2019. https://doi.org/10.1145/3328526.3329574
• G. Amanatidis, G. Birmpas, E. Markakis, Comparing Approximate Relaxations of Envy-Freeness, IJCAI 2018. https://doi.org/10.24963/ijcai.2018/7

Why a cloudlet price matters

Mobile devices can divide work between local execution, a nearby shared cloudlet, and a remote cloud. A cloudlet has limited capacity, so one user's choice changes the delay faced by the others. Cardellini and coauthors model this as a generalized Nash equilibrium problem, in which each user's feasible choices depend on the aggregate cloudlet load. The shared utilization cap makes a direct distributed solution awkward: a user must know how much capacity all other users consume before choosing a feasible deviation. The paper therefore introduces an additional player who sets a cloudlet price. This mission formalizes the relationship between the original coupled game and that extended, ordinary Nash game Cardellini et al., accepted manuscript, pp. 10–16.

The offloading game

There are $N$ users and $n$ cloudlet servers. User $u$ chooses fractions $x_{u,m}$, $x_{u,\mathrm{clet}}$, and $x_{u,\mathrm{cloud}}$ for local, cloudlet, and remote-cloud execution. These fractions are nonnegative and sum to one. At most a fraction $\chi$ can be offloaded, and a user-specific linear power constraint applies. The set $\widetilde K_u$ contains these private feasible choices. The cloudlet load and the shared feasible set are

$$L(x)=\frac1n\sum_{u=1}^{N}\delta_u x_{u,\mathrm{clet}},\qquad \Omega=\{x:L(x)\le U_{\max}\},\qquad K=\left(\prod_{u=1}^{N}\widetilde K_u\right)\cap\Omega.$$

Each user's cost $\lambda_u R_u$ is the response-time expression on p. 10, with coefficients $\alpha_u,\beta_u,\gamma_u,\delta_u$. The VI map $F$ is the stack of the user's partial gradients, written in closed form on p. 11. A variational solution $\bar x$ belongs to $K$ and satisfies $\langle F(\bar x),x-\bar x\rangle\ge0$ for every $x\in K$. The pairing sums all three coordinates for each user. Section 5 assumes $0<U_{\max}<1$ and $0<\alpha_u,\delta_u<1$ for every user; the model also has $n>0$ and $0<\chi\le1$ Cardellini et al., pp. 7, 9–11.

The extended game replaces the joint cap in each user's feasible set by a price. User $u$ minimizes $\lambda_uR_u(x)+\rho(\delta_u/n)x_{u,\mathrm{clet}}$ over $\widetilde K_u$. A cloudlet manager chooses $\rho\ge0$ to maximize $\rho(L(x)-U_{\max})$. The manager's choice is part of the Nash equilibrium condition, not a preimposed complementary-slackness equation. The extended game's VI set is $K_e=(\prod_u\widetilde K_u)\times\mathbb R_+$ and its map is $F_e(x,\rho)=(F(x)+\operatorname{price}(\rho),U_{\max}-L(x))$ Cardellini et al., p. 15.

Formalization targets

The goal is the two-part assertion of Theorem 2. Under the standing assumptions and a strict load bound on the full product of private feasible sets, its equilibrium characterization is

$$\bar x\in\operatorname{SOL}(K,F) \quad\Longleftrightarrow\quad \exists\bar\rho,\; (\bar x,\bar\rho)\in\operatorname{NE}_{\mathrm{ext}}.$$

The same goal states that monotonicity of $F$ on $\prod_u\widetilde K_u$ implies monotonicity of $F_e$ on $K_e$. The three milestones follow the paper's path: the extended Nash game is equivalent to its VI; the shared affine constraint has a scalar multiplier at a VI solution; and the price-load coupling cancels in the monotonicity pairing. The source states the first as a classical result and gives the last two in its proof Cardellini et al., pp. 15–16.

What the result provides

The characterization lets a variational solution of a game with coupled feasible sets be found as an equilibrium of a game whose $N$ users have separate feasible sets. The additional scalar has a concrete interpretation: it is the multiplier of the shared cloudlet-utilization cap. The monotonicity assertion connects the paper's analysis of the original VI to methods for the extended one. The paper uses this relationship as the entry point for its distributed algorithms in the next section Cardellini et al., pp. 16–17.

The result is proved in the paper but is not yet machine checked in this mission. A complete development would give reusable Lean interfaces for a finite-dimensional VI on an intersection of a product polytope and one affine half-space, a multiplier characterization for that intersection, and an equilibrium-to-VI conversion for separable player constraints. Those components could support other capacity-sharing games. The theorem drafts remain proof obligations; the definitions compile locally.

Where the proof is delicate

A Nash equilibrium requires each user to be optimal against every privately feasible deviation, including deviations that violate the original shared cap. Consequently, the user's cloudlet cost must remain well defined throughout $\widetilde K_u$ for the equivalence to hold. A load bound only on $K$ does not cover those deviations. The multiplier comparison must also account for the manager's maximization condition and the sign of the load term in $F_e$. For monotonicity, $F_e$ evaluates $F$ on the whole product $\prod_u\widetilde K_u$, a larger domain than $K$. These domain distinctions explain why the statement needs two explicit repairs to the printed theorem Cardellini et al., pp. 15–16.

Formalization scope

Lean represents the users as Fin N and the three processing locations as a finite tier type. Indices therefore start at zero. The costs, the map $F$, the private sets, $\Omega$, and $K$ are separate definitions. The Euclidean pairing is written as a finite sum; no Pi-type sup norm is used. The extended Nash predicate quantifies over user deviations in $\widetilde K_u$ and over every nonnegative manager price. The VI predicates are in their own module so the game is not built into their meaning. The theorem's statement remains meaningful at $N=0$; no positive-user hypothesis is added to Section 5's assumptions.

The first repair requires $L(x)<1$ at every $x\in\prod_u\widetilde K_u$. The paper's Theorem 1 condition (18) implies this bound, but is stronger than needed. Without the bound, a private deviation can cross the pole of $\delta_u x_{u,\mathrm{clet}}/(1-L(x))$; Lean's total division then assigns a value at a zero denominator even though the paper's cost has none. In a two-user instance with $n=1$, $\delta_u=0.9$ and $U_{\max}=0.5$, the pole can lie within one user's private feasible interval. The second repair reads “the original game is monotone” on $\prod_u\widetilde K_u$, because that is precisely the $x$-domain of $K_e$. Monotonicity on $K$ alone is insufficient. Both repairs are disclosed in the item notes, and the source wording remains visible in the milestone quotations.

An empty $K$ would make a solution statement vacuous; the formal development should retain concrete feasible parameter instances. The map $F$ is the paper's displayed formula, rather than a derivative chosen to make a milestone tautological. The VI uses all user coordinates, and the extended game does not silently reinstate the shared constraint in user deviations. Contributions toward the stated multiplier theorem, Nash-to-VI equivalence, and the cancellation identity are welcome, along with reusable finite-dimensional convex-analysis lemmas.

Selected references

• V. Cardellini, V. De Nitto Personé, V. Di Valerio, F. Facchinei, V. Grassi, F. Lo Presti, and V. Piccialli, A game-theoretic approach to computation offloading in mobile cloud computing, accepted manuscript for Mathematical Programming, 2015, DOI 10.1007/s10107-015-0881-6.

Motivation

Allocating indivisible goods fairly is difficult because a single good can change how an agent compares two bundles. Exact envy-freeness can be impossible (one good, two agents), so the field works with relaxations. Envy-freeness up to any good (EFX) requires each agent to prefer her own bundle to every other agent's bundle after any one good of that other bundle is removed. Whether EFX allocations of all goods always exist is open; the question motivates weakening the requirement that every good be assigned, and asking how little must be left over. Chaudhury, Kavitha, Mehlhorn and Sgouritsa show that leaving a small, unenvied set of goods unallocated (donated to "charity") suffices for every normalized monotone valuation profile (arXiv:1907.04596v3, Theorem 8, pp. 11–12).

Timeline (as recounted on pp. 2–3 of the source):

• 2004: Lipton, Markakis, Mossel and Saberi introduce the envy-graph and cycle-elimination technique and compute allocations now called EF1 (DOI 10.1145/988772.988792).
• 2016: Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang define EFX (DOI 10.1145/2940716.2940726).
• 2018: Plaut and Roughgarden prove EFX allocations of all goods exist for two agents, or for any number of agents with identical valuations (arXiv:1707.04769).
• 2019: Caragiannis, Gravin and Huang introduce EFX with charity: a partial EFX allocation in which each agent gets at least half her value in a Nash-optimal allocation, with no bound on the number or value of donated goods (arXiv:1902.04319).
• 2020: Chaudhury, Garg and Mehlhorn prove existence of complete EFX allocations for three agents with additive valuations (arXiv:2002.05119).
• 2020/2021: the present paper bounds the charity: fewer goods than unenvied agents, and no agent envies the donated set. Its SODA 2020 version assumed gross-substitute valuations; the journal version (arXiv v3) needs only normalized monotone valuations (p. 8, §1.4).

The two bounds matter separately. The empty allocation is EFX and donates everything; a cardinality bound alone still lets the donated goods carry most of an agent's value; the value bound alone allows almost all goods to be donated. The paper's later maximin-share and groupwise-maximin-share guarantees (Theorems 14 and 16, treated in the next missions of this series) are derived from exactly the allocation produced here.

Setting

There are $n\ge1$ agents, indexed by $N=\{1,\ldots,n\}$ in the paper, and a finite set $M$ of $m$ indivisible goods. Agent $i$ has a valuation $v_i:2^M\to\mathbb R_{\ge0}$. It is normalized if $v_i(\varnothing)=0$ and monotone if $S\subseteq T$ implies $v_i(S)\le v_i(T)$. No additivity, submodularity or substitutes condition is assumed. These are the general valuations of §1.1.1, p. 3, and §2 of the source.

A partial allocation $X=(X_i)_{i\in N}$ consists of pairwise disjoint bundles $X_i\subseteq M$. Its pool is the goods not assigned to anyone,

$$P(X)=M\setminus\bigcup_{i\in N}X_i.$$

The allocation is EFX when

$$v_i(X_j\setminus\{g\})\le v_i(X_i) \qquad\text{for all }i,j\in N\text{ and every }g\in X_j.$$

The paper calls allocations partial by default (p. 3, footnote 5). The envy graph $G_X$ has the agents as vertices and an edge $i\to j$ when $v_i(X_i)<v_i(X_j)$. A source is a vertex with no incoming edge. Its reachability component $C(s)$ includes $s$ itself. The social welfare of $X$ is $\phi(X)=\sum_i v_i(X_i)$. These notions are introduced on pp. 8–9 of the source.

For a set $S$ of goods, an envied set is one some agent values more than her own bundle. An inclusion-wise minimal envied subset $Z$ is envied, but no strict subset of $Z$ is envied by anyone. An agent who envies such a $Z$ is a most envious agent of $S$; the paper allows ties. The three update rules U0, U1 and U2 use these sets to change an allocation while maintaining EFX (Definition 3 and Algorithm 2, p. 9).

Formalization targets

The goal is the allocation guarantee of Theorem 8:

$$\exists X\text{ partial}:\quad X\text{ is EFX},\qquad v_i(P(X))\le v_i(X_i)\ (i\in N),\qquad |P(X)|<|\operatorname{sources}(G_X)|\le n.$$

Both the stronger source-count bound and its consequence $|P(X)|<n$ are stated. The theorem asserts existence for every normalized, monotone valuation profile, including nonadditive profiles. It does not require the returned envy graph to be acyclic; acyclicity is an invariant used during construction, rather than an additional advertised property of the final allocation.

The attack path consists of the paper's numbered Lemmas 2, 4, 5, 6 and 7. Lemma 2 concerns removal of envy cycles; its Lean form keeps the page's conditional "if $X$ is EFX then $X'$ is EFX" and the unconditional strict welfare increase. Lemma 4 records what U0 does and what its failure implies. Lemma 5 records U1's welfare and EFX guarantees. Lemma 6 supplies the finite source, good and agent data required for U2. Lemma 7 states U2's welfare and EFX guarantees. Their source wording and page locations appear in the milestone list; the Lean statements include the exact allocation updates where those lemmas rely on them.

Significance

The theorem guarantees a partial EFX allocation even for general monotone valuations, while limiting the unallocated pool more tightly than the number of agents: its size is below the number of unenvied agents. Every agent also values that entire pool no more than her own bundle. These two bounds distinguish the allocation from a merely EFX partial allocation. They provide the starting point for the paper's later statements on approximate maximin shares under additive valuations (Theorems 14 and 16).

The mathematical result is proved in the paper. The mission asks for a machine-checked proof of its allocation guarantee and of the supporting lemmas, with a reusable Lean account of finite partial allocations, the unallocated pool, envy graphs, minimal envied subsets and the update rules. Such definitions are useful for other fair-division questions involving unallocated indivisible goods.

Difficulty

EFX must hold after the allocation is changed, for every agent pair and for removal of every good from the other agent's new bundle. Simply giving a pool good to an agent may violate that condition, even though it makes the pool smaller. Conversely, replacing a bundle with an envied subset can improve welfare while returning goods to the pool. The source-count bound depends on controlling both kinds of progress. Rule U2 adds a further complication: its bundle moves follow envy paths, so an overlap between selected paths would make the new allocation ambiguous. These are the points at which the straightforward approach of distributing the remaining goods one at a time stops working.

Formalization scope

Lean represents agents by Fin n, goods by Fin m, bundles by finite sets of goods, and valuations by real-valued functions on bundles. The paper's one-based subscripts become zero-based Lean indices. Nonnegative values need no separate hypothesis: normalization and monotonicity imply them. The hypothesis $n>0$ is explicit because the paper presumes agents and the strict bound $|P|<n$ is false when $n=0$. The pool is computed as the complement of the union of pairwise disjoint assigned bundles. It is never a free set. EFX ranges over every pair $i,j$, including $i=j$, and every good of $X_j$.

The minimal-envied-subset definition checks every strict subset against every agent. The most envious agent is a relation, allowing the paper's arbitrary tie choice. Reachability includes a path of length zero. U2's new allocation is calculated from its paths and chosen subsets. Lemma 6 includes Algorithm 1's acyclic-graph invariant and the ordering property established in its proof. It replaces the printed threshold $|P|\ge n$ with $|P|\ge|\operatorname{sources}(G_X)|$, the exact number of fresh goods its construction needs and the threshold used by the goal. Lemma 7 takes that ordering property to make path assignments unambiguous.

The printed U2 pool expression in Algorithm 2, line 13, is malformed; the formal statement uses the pool of the constructed allocation and the corrected union of leftover goods. Theorem 8's final sentence also asserts an $nmV/\Delta$ iteration bound. This mission poses the allocation conclusions, while a future run-level formalization would be needed to state and check the iteration count. The paper's preceding count of U1/U2 steps and successive U0 steps does not by itself imply the printed number. Definitions and the numbered lemma statements are welcome contributions; a purported proof that uses a free empty pool, overlapping bundles, zero agents or an arbitrary replacement allocation would not establish this target.

Selected references

• B. R. Chaudhury, T. Kavitha, K. Mehlhorn and A. Sgouritsa, A Little Charity Guarantees Almost Envy-Freeness, arXiv:1907.04596v3, 2020; published in SIAM Journal on Computing, 2021. Pinned preprint.
• R. J. Lipton, E. Markakis, E. Mossel and A. Saberi, On approximately fair allocations of indivisible goods, ACM EC 2004. https://doi.org/10.1145/988772.988792
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah and J. Wang, The unreasonable fairness of maximum Nash welfare, ACM EC 2016. https://doi.org/10.1145/2940716.2940726
• B. Plaut and T. Roughgarden, Almost envy-freeness with general valuations, SODA 2018. https://arxiv.org/abs/1707.04769
• I. Caragiannis, N. Gravin and X. Huang, Envy-freeness up to any item with high Nash welfare: the virtue of donating items, ACM EC 2019. https://arxiv.org/abs/1902.04319
• B. R. Chaudhury, J. Garg and K. Mehlhorn, EFX exists for three agents, ACM EC 2020. https://arxiv.org/abs/2002.05119

Motivation

In a congestion game, several users choose facilities and each facility becomes more costly as more users choose it. Such games model settings in which each participant chooses a route or collection of resources for personal use while the resulting load is shared. A pure Nash equilibrium is a stable choice of routes: no single participant can lower their own cost by switching. Stability alone gives no assurance that the resulting allocation serves the group well. The price of anarchy compares the social cost of an equilibrium with the best social cost attainable by coordinated choices.

Christodoulou and Koutsoupias studied finite congestion games with linear latency functions and several notions of social cost. For the maximum cost borne by any player, their STOC 2005 paper gives both an upper bound valid for all such games and a family of instances showing that its square-root dependence on the number of players has the right order. This mission formalizes those two claims together. The maximum criterion matters when a single heavily delayed user is significant even if the total cost of the population is moderate.

Setting

Let $N\ge1$ be the number of players and let $E$ be a finite set of facilities. Player $i$ has a finite collection $\Sigma_i$ of available pure strategies, each a subset of $E$. A profile $A$ chooses one strategy $A_i\in\Sigma_i$ for every player. For a facility $e$, its load $n_e(A)$ is the number of players whose chosen strategy contains $e$. The latency of $e$ at load $n$ is $f_e(n)$. Player $i$ pays the sum of the latencies on the facilities they chose:

$$c_i(A)=\sum_{e\in A_i}f_e(n_e(A)).$$

A profile is a pure Nash equilibrium if no player can decrease this cost by replacing their own strategy while the others keep theirs. The paper calls latencies linear when $f_e(n)=a_en+b_e$ with $a_e,b_e\ge0$; these are affine functions in standard terminology. The paper displays many calculations for the special case $f_e(n)=n$ and states the general nonnegative affine convention in its model section. The maximum social cost is $\operatorname{MAX}(A)=\max_i c_i(A)$; the total cost is $\operatorname{SUM}(A)=\sum_i c_i(A)$. The paper's average social cost is $\operatorname{SUM}(A)/N$.

For a game with at least one pure Nash equilibrium and a positive optimal maximum cost, the maximum-cost pure price of anarchy is the largest equilibrium value of $\operatorname{MAX}$ divided by the smallest feasible value. The Lean targets use inequalities against every feasible comparison profile $P$ rather than dividing by an optimum. This form continues to say something when an optimum has cost zero, and finite strategy sets ensure an optimum exists whenever the profile space is nonempty.

Formalization targets

Universal upper bound

For every $N\ge1$, every finite game with nonnegative affine latencies, every pure Nash equilibrium $A$, and every feasible profile $P$, Theorem 5's proof yields

$$\operatorname{MAX}(A)\le \left(1+\sqrt{\frac{5N}{2}}\right)\operatorname{MAX}(P).$$

This states a numerical version of the paper's $O(\sqrt N)$ theorem without an unspecified constant. Taking $P$ to minimize $\operatorname{MAX}$ gives the corresponding price-of-anarchy bound. The bound is about asymmetric games: players may have different strategy sets, and no symmetry assumption is present.

Lower-bound family

For every integer $k\ge2$, let $N=k(k-1)+1$. Theorem 6 provides an identity-latency congestion game with $N$ players and $kN$ facilities, a pure Nash profile $A$, and an optimal profile $P$ for which

$$\operatorname{MAX}(A)=k^2,\qquad \operatorname{MAX}(P)=k.$$

Every feasible profile in the instance has maximum cost at least $k$. Thus the ratio is $k$, and $k\ge\sqrt N$. The proof's explicit instance has positive comparison cost, so the lower bound cannot be satisfied by a zero-cost game. The source also says such behavior occurs in network congestion games and sketches a network realization in Figure 2; this mission's formal lower target is the finite congestion-game construction.

Significance

Together these results identify the order of growth of the worst pure equilibrium maximum cost relative to an optimum: it can grow with the population, yet for linear latencies it grows no faster than a constant times $\sqrt N$. The upper statement applies to any feasible comparison profile, so it can also be used when a convenient benchmark is known without solving the entire optimization problem. The lower family prevents replacing the square-root dependence by a bound independent of $N$ for this class of games.

The results are proved in the 2005 paper; the mission is to give them machine-checked Lean proofs in a common finite-game representation. The development also supplies reusable definitions of congestion games, loads, pure cost equilibria, and maximum social cost, together with the total-cost estimate of Theorem 1 and the intermediate bounds appearing in Theorem 5. The current draft contains statements with sorry placeholders, not completed proofs.

Difficulty

A bound on total player cost does not directly control the cost of the most expensive player sharply enough. An individual player can use several facilities whose loads interact, and bounding each load separately loses the dependence required for the square-root result. Affine coefficients add another issue: the proof printed for identity latencies writes a cardinality where the general statement needs a coefficient-weighted quantity. The lower example has an indexing discrepancy in the printed alternative strategies, so the intended Nash profile must be checked against the costs on every permitted deviation.

Formalization scope

Players are represented by Fin N; facilities by an arbitrary finite type in upper bounds and by a type with $kN$ elements in the lower family. A profile is a function from players to finite facility sets, with feasibility stated separately. Latencies are real-valued on natural-number loads. The IsLinear predicate requires explicit nonnegative affine coefficients. Pure Nash uses a cost inequality; it is the negative-payoff version of a standard finite game's payoff equilibrium. MAX requires at least one player, and all upper-bound targets therefore require $N\ge1$. The lower family begins at $k=2$, where $N=k(k-1)+1$ is positive.

The source's number $k^2-k+1$ is written as $k(k-1)+1$ in Lean to keep natural-number subtraction inside its valid range. The two expressions agree for $k\ge2$. In the source's one-based indexing, the proposed alternative strategy uses a ceiling index. The printed denominator $k$ makes some alternative facilities carry $k+1$ users and breaks the Nash assertion; denominator $k-1$ agrees with Figure 2's $k-1$ short-route users per layer and gives the stated costs. This correction is recorded with the lower theorem. No normalization of coefficients or artificially restricted strategy class is assumed. Contributions to the finite-game definitions, Theorem 1, the player-cost bounds, and the explicit lower instance are all in scope.

Selected references

• G. Christodoulou and E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, Proceedings of the 37th Annual ACM Symposium on Theory of Computing, 2005. DOI: 10.1145/1060590.1060600.

Motivation

Mean field games describe the limit of symmetric stochastic differential games with $n$ players as $n\to\infty$. A basic question of the theory is which mean field equilibria are limits of Nash equilibria of the $n$-player games. For closed-loop equilibria, in which each player's control may depend on the states of all players, this question was open in general until D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745, Ann. Appl. Probab. 2020). That paper shows that limits of closed-loop $\varepsilon_n$-Nash equilibria are weak mean field equilibria, a class that can be strictly larger than the classical (strong) one.

Section 7.3 of the paper gives an explicit game in which the difference is visible. It has exactly three strong equilibria (Lacker, Probab. Theory Related Fields 165, 2016, Proposition 3.6, cited as [43] in the paper) and infinitely many weak ones. The weak equilibria form a family indexed by a switching time $t_0\in[0,T]$, and for $t_0\in(0,T)$ they are not mixtures of strong equilibria (Remark 7.1). Proposition 7.2, the subject of this mission, treats $t_0=0$: the natural symmetric feedback is an $n$-player approximate Nash equilibrium, and its population mean selects the equal mixture of the two strong equilibria $m^{\pm1}$ rather than the third one, $m^0$. The selection mechanism is regularization by noise: the mean of the population solves an ill-posed ODE, and the small noise of the $n$-player system picks out a particular random solution (Trevisan, Electron. Commun. Probab. 18, 2013, cited as [57] in the paper).

Setting

Fix a horizon $T>0$. In the mean-sign game each of $n$ players controls a real state

$$X^i_t = \int_0^t \alpha^i_s\,ds + W^i_t,\qquad X^i_0=0,$$

with controls $\alpha^i_s\in A=[-1,1]$ and independent standard Brownian motions $W^1,\dots,W^n$. The mean process is $\overline\mu^n_t=\frac1n\sum_{k=1}^n X^k_t$, the mean of the empirical measure $\mu^n_t=\frac1n\sum_k\delta_{X^k_t}$. Player $i$ maximizes the expected terminal reward

$$J^n_i=\mathbb E\big[X^i_T\,\overline\mu^n_T\big],$$

that is, $b(t,x,m,a)=a$, $f\equiv0$, $g(x,m)=x\,\overline m$ with $\overline m=\int y\,m(dy)$, and initial law $\lambda=\delta_0$.

A Markovian control of player $i$ is a Borel function $\beta:[0,T]\times\mathbb R^n\to[-1,1]$ of time and the current states of all players. A profile $(\alpha^1,\dots,\alpha^n)$ is a Markovian $\varepsilon$-Nash equilibrium if no player can raise their payoff by more than $\varepsilon$ by switching to another Markovian control while the others keep theirs (Definition 2.1).

With $\operatorname{sgn}(x)=1,-1,0$ for $x>0$, $x<0$, $x=0$, the sign feedback (7.13) with $t_0=0$ is

$$\alpha^{n,i}_0(t,x_1,\dots,x_n)=\operatorname{sgn}\Big(\frac1n\sum_{k=1}^n x_k\Big)\mathbf 1_{(0,T]}(t),$$

the same for every player. Finally $H^\pm_0(t)=\pm t$ on $[0,T]$ (7.11).

Formalization targets

Goal: Proposition 7.2

For the profile $\alpha^n=(\alpha^{n,1}_0,\dots,\alpha^{n,n}_0)$:

$$\exists\,\varepsilon_n\ge0,\ \varepsilon_n\to0:\quad \alpha^n\ \text{is a Markovian }\varepsilon_n\text{-Nash equilibrium for each }n,$$ $$\mathcal L\big((\overline\mu^n_t[\alpha^n])_{t\in[0,T]}\big)\ \Longrightarrow\ \tfrac12\delta_{H^+_0}+\tfrac12\delta_{H^-_0}\quad\text{on }C([0,T];\mathbb R).$$

The goal also asserts that the $n$-player system under $\alpha^n$ has a solution, so that the equilibrium property cannot hold vacuously.

Milestones

1. The equilibrium payoff: $J^n_1(\alpha^n)=\mathbb E[|\overline\mu^n_T|^2]\to T^2$ (proof of Proposition 7.2, p. 49).
2. Lemma 7.4, the part about the mean $Y^n$ and player 1's noise $W^1$ when player 1 deviates to a $\frac1n$-optimal control (7.15): the laws of $(Y^n,W^1)$ are tight, and every limit $(Y,W)$ has $\mathcal L(Y)=\tfrac12\delta_{H^+_0}+\tfrac12\delta_{H^-_0}$, solves $Y_t=\int_0^t\operatorname{sgn}(Y_s)\,ds$, and has $Y$ independent of $W$.
3. The upper bound (7.14): $\limsup_n\sup_{\beta}J^n_1(\beta,\alpha^{n,2}_0,\dots,\alpha^{n,n}_0)\le T^2$.

Significance

Proposition 7.2 is a concrete instance of the paper's main theme. Theorem 2.7 says that limits of closed-loop equilibria are weak equilibria; this example exhibits explicit, symmetric, Markovian approximate equilibria whose limit is a genuinely random equilibrium (the sign of the mean is a fair coin), selected by noise among infinitely many candidates, and it identifies the limiting law of the population mean exactly. The paper states that the analogous claim for $t_0\in(0,T)$, where the limit would be a weak equilibrium that is not a mixture of strong ones, is not resolved; a formal treatment of the $t_0=0$ case makes the structure of that question precise.

Nothing of this proposition is machine-checked. Formalizing it requires weak solutions of SDEs with discontinuous drift, Nash equilibria over Markovian feedback controls, and weak convergence of laws on path space, all stated so that the junk values of Lean's total functions never enter. The objects defined here (the $n$-player game with quantified weak solutions, its payoffs and Markovian $\varepsilon$-Nash equilibria) are shared with the other missions of this series.

Difficulty

The obvious argument for $\varepsilon_n\to0$ compares player 1's payoff under a deviation with $T^2$. A deviation changes the drift of the mean only by $O(1/n)$, but the dynamics of the mean, $dY_t=\operatorname{sgn}(Y_t)dt+n^{-1/2}d\overline W_t$, is ill-posed in the limit: the ODE $\dot y=\operatorname{sgn}(y)$, $y_0=0$, has infinitely many solutions $\pm(t-s)^+$. Continuity of the solution map, the usual tool, is unavailable, and one must instead identify the limit law, which comes from the vanishing noise, and show that it is unchanged by the deviation. The second difficulty is that the payoff $X^1_TY_T$ is unbounded, so convergence of laws does not give convergence of payoffs without a uniform integrability estimate. The proof in the paper is short, but relies on a cited result on the vanishing-noise limit and on a compactness argument in a weak $L^2$ topology for the deviating controls.

Formalization scope

• Dimension and state. $d=1$; $\mathbb R^1$ is EuclideanSpace ℝ (Fin 1) (the platform's EthierKurtz.SDEState 1) and its coordinate is y 0. Controls are real, $A=[-1,1]$.
• Pathwise equations. Volatility is the identity, so the SDE of each player is stated as $X^i_t=X^i_0+\int_0^t b\,ds+W^i_t$ almost surely for all $t\in[0,T]$, with a Lebesgue integral of a bounded measurable integrand.
• Solutions are quantified. A weak solution of the $n$-player system is a structure (probability space, filtration, independent $\mathbb F$-Brownian motions, i.i.d. initial states independent of the noise, adapted path-valued states, the empirical flow). Payoffs are functions of a solution; the Nash inequality and every limit statement are required for every solution. Solutions exist and are unique in law, so this matches the paper's definitions; the goal asserts existence explicitly.
• Index shift. Term $n$ of every sequence is the $(n+1)$-player game; the factor $\frac1n$ in the controls and the mean is then $\frac1{n+1}$.
• sgn and time. $\operatorname{sgn}$ is Real.sign ($\operatorname{sgn}0=0$), and the control vanishes at $t=0$, both as printed.
• Unbounded payoff. Assumption A fails ($g$ is unbounded) and is not assumed anywhere. Payoffs are Bochner integrals; $X^i_T\overline\mu^n_T$ is integrable on every solution (bounded drift, $X^i_0=0$), which is a fact to be proved rather than an assumption.
• Laws. Laws on $C([0,T];\mathbb R)$ carry the topology of weak convergence; the mean path is a continuous function of the state paths, so its law is a probability measure by construction.
• Lemma 7.4. Only the $(Y,W)$ coordinates are stated: tightness, (i), the equation for $Y$ in (ii), and (iv). The coordinates $X$ and $\beta$, which need the weak topology of $L^2([0,T];[-1,1])$, and item (iii) are not stated; the norm topology must not be substituted, because the deviating controls are not tight in it.
• Ruled out. A statement in which the profiles have no solutions would make the Nash clause vacuous; the existence clause of the goal excludes it.

Contributions welcome: the existence of weak solutions for bounded measurable Markovian drifts, the vanishing-noise limit of $dZ=\operatorname{sgn}(Z)dt+\epsilon\,dW$, and Girsanov-type change-of-measure estimates are all reusable beyond this mission.

Selected references

• D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit, Ann. Appl. Probab. 30(4), 2020; arXiv:1808.02745v1, 2018. https://arxiv.org/abs/1808.02745
• D. Lacker, A general characterization of the mean field limit for stochastic differential games, Probab. Theory Related Fields 165(3–4), 581–648, 2016 (reference [43] of the paper).
• D. Trevisan, Zero noise limits using local times, Electron. Commun. Probab. 18, 2013 (reference [57] of the paper).
• R. Carmona, D. Lacker, A probabilistic weak formulation of mean field games and applications, Ann. Appl. Probab. 25(3), 2015. https://arxiv.org/abs/1307.1152

Motivation

How should a set of indivisible items (courses, shifts, inherited objects) be divided among people who have different entitlements but no money to transfer? A classical answer for divisible goods is the competitive equilibrium from equal incomes (CEEI): give every agent a budget of artificial currency, find prices at which every agent can afford her favourite bundle and the market clears. The resulting allocation is Pareto optimal and fair. With indivisible items a CEEI can fail to exist already for one item and two agents with equal budgets: at any price, either both agents can afford the item or neither can.

Babaioff, Nisan and Talgam-Cohen (arXiv:1703.08150; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) study this Fisher market with indivisible goods when budgets are generic: unequal budgets, with a measure-zero set of exceptional budget pairs excluded. Their main result is for two agents with almost equal budgets. This mission formalizes the companion result for two agents with identical additive preferences and arbitrary unequal budgets (Theorem 8.1 of the paper, its informal Theorem 1.4). With identical preferences the division problem is a discrete claims (bankruptcy) problem: one cake of fixed value is split between claimants with different entitlements $b_1, b_2$.

Timeline of the relevant results:

• Budish (2011, doi:10.1086/664613): approximate CEEI with almost equal budgets for many agents, with an approximate market-clearing error.
• Segal-Halevi (AAMAS 2018, arXiv:1705.04212), a follow-up to the preprint of this paper: for four agents with arbitrary budgets, non-existence of CE persists even with generic budgets.
• Babaioff, Nisan and Talgam-Cohen (preprint 2017, journal 2021): exact CE for two additive agents with almost equal unequal budgets (Theorem 7.1), and for two agents with identical preferences and generic budgets (Theorem 8.1).

Setting

There are $m$ indivisible items $M$ and two agents. Agent $i$ has a valuation $v_i : 2^M \to \mathbb R$ that is additive, normalized ($v_i(M)=1$), non-negative, monotone and strict (different bundles have different values), and a budget $b_i > 0$, with $b_1 + b_2 = 1$. An allocation $\mathcal S = (\mathcal S_1, \mathcal S_2)$ gives every item to exactly one agent. Item prices $p_j \ge 0$ price a bundle at $p(S) = \sum_{j \in S} p_j$.

A bundle $S$ is demanded by agent $i$ at prices $p$ if $p(S) \le b_i$ and $p(T) > b_i$ for every bundle $T$ with $v_i(T) > v_i(S)$. A competitive equilibrium (CE) is a pair $(\mathcal S, p)$ in which each $\mathcal S_i$ is demanded by agent $i$. An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent. It is budget-proportional if $v_i(\mathcal S_i) \ge b_i$ for both agents, and anti-proportional if $v_i(\mathcal S_i) \le b_i$ for both, strictly for one.

The truncated share of agent $i$ is

$$b_i^- = \max\{ v_i(\mathcal S'_i) : \mathcal S' \text{ PO},\ v_i(\mathcal S'_i) \le b_i \},$$

the best she can get in a PO allocation that gives her at most her budget share; an allocation gives her the truncated share if $v_i(\mathcal S_i) \ge b_i^-$. The exceptional set $R_i$ (Definition 6.2) consists of the budget pairs $(b_i, 1-b_i)$ for which two PO allocations $\mathcal S(r), \mathcal S(r+1)$, consecutive in agent $i$'s order of preference, satisfy $b_i / v_i(\mathcal S(r+1)_i) = (1-b_i)/(1-v_i(\mathcal S(r)_i))$. It is finite. The rectangle $T_i$ (Definition 6.1) is a set of allocations between the truncated-share maximizers of the two agents.

In Lean all objects live in GenericBudgets.IdenticalPrefs: bundle, price, IsDemanded, IsCE, IsPO, IsStandardValuation, IsBudgetProportional, IsAntiProportional, GetsTruncatedShare, IsTruncMaximizer, InRectT, InR.

Formalization targets

Goal: Theorem 8.1 (p. 20)

If $v_1 = v_2$, $b_1 > b_2$, and $(b_1,b_2) \notin R_i$ for some agent $i$, then

$$\exists\, (\mathcal S, p) \text{ a CE with } v_j(\mathcal S_j) \ge b_j^- \text{ for } j = 1, 2.$$

Milestones

1. Proposition 5.1 (p. 12): every budget-proportional, and every anti-proportional, PO allocation is supported in a CE.
2. Lemma 6.3 (p. 15): no budget-proportional allocation, no PO anti-proportional allocation, $(b_1,b_2) \notin R_i$ and $T_i = \emptyset$ imply a CE with truncated shares.
3. Constant-sum claim (p. 20): with identical preferences every allocation is PO and none is anti-proportional.
4. Lemma 8.2 (p. 20): if every allocation is PO and $(b_1,b_2) \notin R_i$ for some $i$, a CE exists; if moreover no PO allocation is anti-proportional, the same CE gives truncated shares.

Significance

Theorem 8.1 shows that the non-existence of CEEI for identical preferences is a knife-edge phenomenon: for every market with identical strict additive preferences, every unequal budget pair outside a finite set admits a CE, and the CE allocation is as close to budget-proportional as indivisibility allows. It gives a market-based solution to the indivisible claims problem with unequal entitlements, and its CE inherits Pareto optimality from the first welfare theorem (Theorem 2.4 of the paper).

The formalization targets three things on top of the paper. First, a machine-checked proof of the paper's main technical tool, Lemma 6.3, which also drives the paper's main Theorem 7.1 (mission 1 of this series), where it is applied to almost equal budgets instead of identical preferences. Second, precise definitions of the truncated share, the rectangle $T_i$ and the exceptional set $R_i$, whose informal versions leave conventions implicit (the maximization runs over PO allocations only; $R_i$ is indexed by consecutive PO allocations). Third, verification of the proof chain Proposition 5.1 → Lemma 6.3 → Lemma 8.2 → Theorem 8.1. The statements compile, but none of these results has a machine-checked proof yet.

Difficulty

The reduction of Theorem 8.1 to Lemma 8.2 and the proof of Lemma 8.2 from Proposition 5.1 and Lemma 6.3 are short. The substance is in Lemma 6.3, which must exhibit prices supporting a PO allocation when no allocation gives both agents their budget shares. Demand is a condition over all $2^m$ bundles, so a candidate price vector has to be checked against every bundle each agent prefers, and the paper's construction breaks down on the exceptional budget pairs $R_i$, which is why they are excluded; the argument is a case analysis over the finite Pareto frontier. The easy case, Proposition 5.1, covers only markets with a budget-proportional or anti-proportional PO allocation; with identical preferences and unequal budgets neither typically exists (no allocation is ever anti-proportional), so Lemma 6.3 cannot be avoided.

Formalization scope

Items are Fin m; agents are Fin 2, with indices $0, 1$ for the paper's agents $1, 2$, so $b_1 > b_2$ is b 1 < b 0. Valuations are functions Finset (Fin m) → ℝ bundled with the standing assumptions in IsStandardValuation; identical preferences are the hypothesis v 0 = v 1. An allocation is a map Fin m → Fin 2, so every item is allocated exactly once. Budgets are positive reals summing to $1$. All quantities are real.

Committed conventions and disclosed restrictions:

• Strictness is injectivity of each valuation on bundles. The paper allows one exception, identical items; that exception is dropped, so markets with identical items are not covered by these statements.
• The budget-proportional share is written $b_i\,v_i(M)$, which equals $b_i$ under normalization.
• The truncated share is stated without a max: $v_i(\mathcal S_i) \ge v_i(\mathcal S'_i)$ for every PO $\mathcal S'$ with $v_i(\mathcal S'_i) \le b_i$.
• "$(b_1,b_2)$ does not belong to $R_i$ for some agent $i$" is read as an existential over $i$.
• $R_i$ is encoded with consecutive PO allocations and the cross-multiplied equation, equivalent to the page's quotient form.
• The constant-sum sentence of p. 20 says "at most their truncated share"; the definition it paraphrases (anti-proportional, p. 12) uses the budget-proportional share, and that is what is stated.

Trivializing formalizations are ruled out: the demand condition quantifies over every bundle with strict inequality, allocations must assign every item, prices are non-negative, the truncated share is maximized over PO allocations only (not over all allocations), and the budget hypothesis excludes only the finite set $R_i$ for one agent, never all unequal budgets.

Proposition 5.1 and Lemma 6.3 are posed with the same statement as in mission 1 of this series; a proof of either transfers verbatim. Contributions welcome: the finite-frontier infrastructure (existence and uniqueness of the truncated-share maximizer), Proposition 5.1 through budget-exhausting combination pricing, and Lemma 6.3.

Selected references

• M. Babaioff, N. Nisan, I. Talgam-Cohen, Competitive Equilibrium with Indivisible Goods and Generic Budgets, arXiv:1703.08150v2, 2018; Mathematics of Operations Research 46(1), 2021. https://arxiv.org/abs/1703.08150, https://doi.org/10.1287/moor.2020.1062
• E. Budish, The Combinatorial Assignment Problem: Approximate Competitive Equilibrium from Equal Incomes, Journal of Political Economy 119(6), 2011. https://doi.org/10.1086/664613
• E. Segal-Halevi, Competitive Equilibrium for Almost All Incomes, Proceedings of the 17th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), 2018, pp. 1267–1275. https://arxiv.org/abs/1705.04212

Motivation

A failed buyer can leave a supplier with goods it can no longer sell through an existing order. A failed supplier can leave a buyer without inputs for future production. In a network, either loss can weaken another firm and start a sequence of defaults. Birge, Capponi and Chen model these effects together with two responses: suppliers reroute unsold goods to other buyers, and buyers seek replacement suppliers. Their accepted manuscript asks whether the resulting market decisions and the default cascade determine a single outcome. The issue matters when a network's resilience or fragility is measured from that outcome: a measure based on an unspecified equilibrium would not be well defined.

Setting

A supply chain order network has finitely many firms $i,j$ and goods $m$. An order $o^m_{ij}$ is the nonnegative quantity of good $m$ that firm $i$ promises to deliver to firm $j$. The network also records each good's original price $p^m$, each firm's initial equity $w_i$, its safety stock $\theta_i^m$ and holding cost $\lambda_i^m$, and a realized net production cost $c_i$. The realization is fixed throughout this mission; the source treats it as random when comparing network performance later in the paper. Rerouting one unit costs firm $i$ an amount $\iota_i^m$; an unfilled unit of demand incurs back-order cost $b_i^m$. These costs and the orders and stocks are nonnegative. The basic model is on pp. 8–17 of the manuscript.

If firm $j$ defaults, a promised delivery to it is not made. Write $\gamma^m_{ij}$ for this undelivered order, and $\bar r_i^m=\sum_j\gamma^m_{ij}$ for firm $i$'s total amount of good $m$ available to reroute. If a supplier $j$ defaults, write $\delta^m_{ji}$ for the buyer $i$'s lost input. After using safety stock, that buyer's unserved demand is $\bar\sigma_i^m=(\sum_j\delta^m_{ji}-\theta_i^m)^+$, where $x^+=\max(0,x)$. These are the quantities in equations (1)–(5).

The rerouted market for good $m$ contains firms with $\bar r_i^m>0$. At price $\pi_i^m$, firm $i$ can sell up to $\bar r_i^m$. Aggregate demand at price $\pi$ is $d_m(\pi)$, with inverse demand $d_m^{-1}$. The sourcing market contains firms with $\bar\sigma_i^m>0$. At switching cost $\kappa_i^m$, firm $i$ can replace up to $\bar\sigma_i^m$ units. Aggregate supply is $s_m(\kappa)$, with inverse supply $s_m^{-1}$. In either market, an efficient allocation maximizes the stated integral objective over the capacity box, and allocates proportionally to capacity among firms quoting the same price or cost. A partial equilibrium additionally makes every active firm's quoted price or cost a best response to all nonnegative unilateral deviations. These are Definitions 2.1–2.2 and 3.1–3.2.

A firm's ex-post net worth $e_i^*$ combines original-order revenue, production and stock costs, rerouting revenue and cost, and back-order and replacement-supplier costs exactly as in equation (10). A firm defaults when its net worth is strictly negative. Starting with no undelivered orders or unserved demand, the update maps $\Phi^*$ and $\Psi^*$ mark all orders affected by firms that default after each market has reached its partial equilibrium. A market stable state is both the limit of that sequence and a fixed point of the update. A general equilibrium combines such a state with a partial equilibrium in every market (Definitions 3.3–3.4 and equation (18)).

Formalization targets

The goal is Proposition 4.3, stated on p. 24:

$$\exists!\,(\Pi,K,\Gamma,\Delta)\;\operatorname{GeneralEquilibrium}(\Pi,K,\Gamma,\Delta).$$

The quadruple consists of rerouting prices $\Pi$, switching costs $K$, undelivered orders $\Gamma$, and unserved demand $\Delta$. The claim includes existence and uniqueness of the full outcome, not merely of its default set. The milestone list follows the paper's dependency path: Propositions A.3 and A.6 identify the unique efficient allocations in the two markets; Propositions 4.1 and 4.2 identify their partial equilibria; Lemma A.7 states that greater disruption cannot increase any firm's partial-equilibrium net worth; and Lemma A.8 states that the default updates are bounded and increasing. The numbered results and their equations are in the E-Companion, EC pp. 4–12, and the main text, p. 22.

Significance

Proposition 4.3 makes the network's outcome a function of its order commitments, stocks, prices, market functions, and realized production costs. Later comparisons of network structures can therefore refer to the equilibrium without choosing among several price or default profiles. The result also separates local market choice from the way losses spread through the network: a firm can reroute or switch optimally and still fail once the effects of other failures are accounted for.

The paper proves the result in its E-Companion, EC pp. 12–13. This mission concerns a Lean statement of that known result and the reusable definitions needed to check a proof. The draft propositions are open proof obligations; this proposal does not claim machine-checked proofs of them. The two market allocation predicates, the default update, and the cascade limit can also support later formal work on the paper's resilience results.

Difficulty

The market and network conditions interact. An arbitrary fixed point of the default update need not be the state reached from zero; using only the fixed-point equation loses the uniqueness asserted by the paper. Conversely, knowing a cascade limit does not by itself show that the limit is fixed, because the update changes discontinuously when a firm's net worth crosses zero. At the market level, the price and switching-cost equilibria must be established from optimization and best-response conditions. Writing the formulas for the claimed equilibrium prices into those definitions would leave the central market claims unproved.

Formalization scope

Firms are Fin N and goods are Fin M, with $N,M>0$; the source numbers both from one, while Lean numbers them from zero. Orders and all default matrices are real valued and coordinatewise ordered. Active markets may be empty, as at the start of the cascade. Market objectives are ordinary real interval integrals over finite capacity boxes. The standing conditions include the paper's smoothness, concavity, and monotonicity assumptions on demand wherever it is positive and on the supply function, plus inverse identities and continuity on the quantity ranges used by the model. The inverse functions remain general data tied to $d_m$ and $s_m$; no linear demand or supply curve is imposed.

Several domain conventions make the displayed formulas meaningful. Assumption 2.1's minimum order is read over positive-order suppliers of a good; over all firms it would force zero safety stock whenever a nonsupplier exists. The inverse supply is nonnegative on feasible quantities, with $s_m(0)\le0$, so the claimed switching cost belongs to the nonnegative strategy space. Demand inverse at zero is fixed to the reservation price. Assumptions 4.1–4.2 apply at each positive active-market total; for the general-equilibrium goal they are required for every binary $0/o^m_{ij}$ profile the cascade can visit. Differentiability at those totals is explicit. Initial equity and the order, stock, holding, rerouting, and back-order data are nonnegative; the realized net production cost can have either sign. The model uses the p. 23 convention for prices and costs outside active markets.

An efficient allocation remains an optimizer of equations (7) or (9), with proportional tie handling; a partial equilibrium remains a best response to every admissible deviation. The general equilibrium includes both the limit from zero and the fixed-point condition. These clauses exclude an equilibrium that is true by definition or a fixed point unrelated to the default cascade. The source's informal statement that every firm “supplies, consumes, or purchases” a good has no separate activity flag in this model; a firm with no internal order can still have outside production or consumption represented in $c_i$. Milestone statements involving arbitrary disruption profiles restrict them to the feasible order box $[0,O]$, where the market inverses are defined.

Selected references

• John R. Birge, Agostino Capponi, and Peng-Chu Chen, Disruption and Rerouting in Supply Chain Networks, accepted manuscript dated October 31, 2022, SSRN 3669363; published in Operations Research, 2023, DOI 10.1287/opre.2022.2409.

Motivation

Mean field games (Lasry–Lions 2006, Huang–Malhamé–Caines 2006) describe Nash equilibria of stochastic differential games with very many symmetric players. In this description each player interacts with the others only through the empirical distribution of their states. The mean field game is meant to be the limit of the $n$-player games as $n\to\infty$. Making that link rigorous has two halves:

• a limit theorem: every limit of $n$-player equilibria is a mean field equilibrium;
• a converse: every mean field equilibrium is the limit of $n$-player approximate equilibria.

For closed-loop equilibria, where players react to the observed states of all others, both halves are harder than for open-loop equilibria. A single player's deviation changes the feedback of the whole system.

This mission covers the converse half of D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020).

Timeline.

• Carmona–Delarue (2013) and Huang–Malhamé–Caines constructed $\epsilon_n$-Nash equilibria from mean field equilibria, under Lipschitz or linear-quadratic structure, with continuous feedbacks.
• Cardaliaguet–Delarue–Lasry–Lions (2015, arXiv:1509.02505) obtained such a converse implicitly from a smooth master equation.
• Lacker (2018) proved the converse for every strong mean field equilibrium. His hypotheses are bounded continuous coefficients and a drift that is Lipschitz in total variation, and the feedback may be discontinuous. The key input is a propagation-of-chaos result in total variation (Lacker, On a strong form of propagation of chaos for McKean–Vlasov equations, arXiv:1805.04476).

Setting

Fix a horizon $T>0$, a compact convex action set $A$ in a real normed space, an initial law $\lambda\in\mathcal P(\mathbb R^d)$ and coefficients

$$b:[0,T]\times\mathbb R^d\times\mathcal P(\mathbb R^d)\times A\to\mathbb R^d,\quad f:[0,T]\times\mathbb R^d\times\mathcal P(\mathbb R^d)\times A\to\mathbb R,\quad g:\mathbb R^d\times\mathcal P(\mathbb R^d)\to\mathbb R .$$

The $n$-player game.

• A Markovian control is a Borel map $\alpha:[0,T]\times(\mathbb R^d)^n\to A$.
• Under a profile $\alpha=(\alpha^1,\dots,\alpha^n)$ the states solve

$$dX^i_t=b\big(t,X^i_t,\mu^n_t,\alpha^i(t,X_t)\big)dt+dW^i_t,\qquad \mu^n_t=\tfrac1n\textstyle\sum_{k}\delta_{X^k_t},$$

with independent Brownian motions $W^i$ and i.i.d. initial states of law $\lambda$.

• Player $i$ receives $J^n_i(\alpha)=\mathbb E\big[\int_0^Tf(t,X^i_t,\mu^n_t,\alpha^i(t,X_t))dt+g(X^i_T,\mu^n_T)\big]$.
• The profile is a Markovian $\epsilon$-Nash equilibrium if no player gains more than $\epsilon$ by switching to another Markovian control.
• Relaxed controls take values in $\mathcal P(A)$ and average $b$ and $f$ against them.

The mean field game. A flow $m\in C([0,T];\mathcal P(\mathbb R^d))$ is a strong MFE if some Borel feedback $\alpha^*:[0,T]\times\mathbb R^d\to A$ satisfies two conditions:

• the state $dX^*_t=b(t,X^*_t,m_t,\alpha^*(t,X^*_t))dt+dW_t$, $X^*_0\sim\lambda$, has law $m_t$ at every time;
• $\alpha^*$ maximizes $\mathbb E[\int_0^Tf(t,X_t,m_t,\alpha(t,X_t))dt+g(X_T,m_T)]$ among all Borel feedbacks $\alpha$.

A strong RMFE is the relaxed analogue.

The assumptions are:

• Assumption A: $A$ compact convex; $b,f,g$ bounded and jointly continuous.
• Assumption B: the sets $\{(b(t,x,m,a),z):a\in A,\ z\le f(t,x,m,a)\}$ are convex.
• Assumption C: $|b(t,x,m,a)-b(t,x,m',a)|\le c\,\|m-m'\|_{TV}$, with $\|m-m'\|_{TV}=\sup_{|\varphi|\le1}\int\varphi\,d(m-m')$.

Formalization targets

Goal: Theorem 2.11

Under Assumptions A, B and C, if $m$ is a strong MFE, there are two families of objects:

• numbers $\epsilon_n\ge0$ with $\epsilon_n\to0$;
• for each $n$, Markovian $\epsilon_n$-Nash equilibria $\alpha^n$;

such that

$$\mu^n[\alpha^n]\ \xrightarrow{\ \text{law}\ }\ m\quad\text{in }C([0,T];\mathcal P(\mathbb R^d)).$$

The goal asserts no rate, so any quantitative improvement still implies it.

Milestones

• Proposition 3.7 (strong part): under A and B, strong MFE and strong RMFE are the same flows.
• Theorem 2.14 (Markovian projection): a drift process can be replaced by a Markovian drift $\hat b(t,x)=\mathbb E[b_t\mid X_t=x]$ with the same one-dimensional marginals.
• (7.2): for the symmetric profile $\Lambda^{n,i}(t,x)=\Lambda^*(t,x^i)$, $\mu^n\to m$ in law and $\int\varphi\,d\mu^n_t\to\int\varphi\,dm_t$ in probability for bounded measurable $\varphi$.
• $\nu^n\to m$ (§7.1, p. 45): after one player deviates, the empirical flow still converges to $m$ in probability.
• Theorem 3.10: the relaxed converse, under A and C only.
• Proposition 3.4(a): under A and B, a relaxed Markovian $\epsilon$-Nash equilibrium can be replaced by a strict one with the same state law.

Significance

The result. Theorem 2.11 says that the strong MFE is a faithful idealization: every classical mean field equilibrium is approximately realized by Markovian feedback equilibria of large finite games. No continuity of the equilibrium feedback and no master equation are required. Together with the paper's main limit theorem (mission 1 of this series), it locates strong MFE inside the set of limits of closed-loop equilibria. The paper's Section 2.4 explains why the same converse is open for weak MFE.

Formalizing it. The result is proved on paper but has no machine-checked proof. A complete development would produce several reusable pieces:

• pathwise formulations of SDEs with bounded measurable drift;
• the Markovian projection theorem;
• total-variation propagation of chaos;
• relaxed-control purification by measurable selection.

None of these is in Mathlib.

Difficulty

The obvious argument has every player use $\alpha^*(t,X^i_t)$, invokes the McKean–Vlasov limit, and passes optimality to the limit. It fails at two places:

• Discontinuous feedback. $\alpha^*$ is only measurable, so weak convergence of $\mu^n$ does not give convergence of payoffs. Convergence in probability of $\int\varphi\,d\mu^n_t$ for discontinuous $\varphi$ is needed, and that is exactly what the total-variation Lipschitz Assumption C provides.
• Arbitrary deviations. A deviating player's control $\beta^n$ is arbitrary and depends on all $n$ states. Its limit is a relaxed, non-Markovian control. Comparing it with the mean field optimum requires a projection back onto Markovian feedbacks, without losing the marginal laws.

Formalization scope

Representation.

• States live in EuclideanSpace ℝ (Fin d).
• $\mathcal P(\cdot)$ is Mathlib's ProbabilityMeasure with the weak topology and the Borel $\sigma$-field.
• Paths and flows are continuous maps on Set.Icc 0 T with the compact-open (uniform) topology.
• Unit volatility makes every SDE a pathwise integral equation $X_t=X_0+\int_0^t(\text{drift})ds+W_t$ a.s., with no stochastic integral.
• Solutions are quantified, not chosen. Payoffs are functions of a solution, and every equilibrium inequality, consistency condition and convergence statement is required for every solution. This equals the paper's definitions because solutions exist and are unique in law (Girsanov; Veretennikov; Krylov–Röckner).
• The game with $n+1$ players is indexed by $n$.

Committed choices.

• The paper's consistency condition "$m_t=\mathcal L(X_t)$" is read as $\mathcal L(X^*_t)$.
• "Strong RFME" in Proposition 3.7 is read as strong RMFE.
• Theorem 2.14's "unique strong solution" is a strong solution adapted to the completed filtration of $(X_0,W)$; its existence is part of the conclusion.
• The $\nu^n$ milestone is stated for arbitrary relaxed Markovian deviations, which include the paper's near-optimal ones.
• Coefficients and controls are defined at all real times; only $[0,T]$ matters.

Ruled out. Because equilibria quantify over solutions, a profile whose state system has no solution would be an equilibrium vacuously. For this reason every existence conclusion (the goal, Theorem 3.10, Proposition 3.4(a)) also asserts that the chosen profiles have solutions, and strong (R)MFE requires the equilibrium SDE to have one.

Infrastructure. A complete proof needs Girsanov's theorem, strong existence for SDEs with bounded measurable drift, measurable selection, tightness on path space, and total-variation propagation of chaos. Each is reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.4(b), the weak half of Proposition 3.7, and Theorem 2.7 are outside this mission.

Selected references

• D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit, arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020. https://arxiv.org/abs/1808.02745
• D. Lacker, On a strong form of propagation of chaos for McKean–Vlasov equations, Electron. Commun. Probab. 23, 2018. https://arxiv.org/abs/1805.04476
• I. Gyöngy, Mimicking the one-dimensional marginal distributions of processes having an Itô differential, Probab. Theory Related Fields 71, 1986. https://doi.org/10.1007/BF00699039
• G. Brunick, S. Shreve, Mimicking an Itô process by a solution of a stochastic differential equation, Ann. Appl. Probab. 23(4), 2013. https://arxiv.org/abs/1011.0111
• R. Carmona, F. Delarue, Probabilistic analysis of mean-field games, SIAM J. Control Optim. 51(4), 2013. https://arxiv.org/abs/1210.5780
• P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The master equation and the convergence problem in mean field games, Annals of Math. Studies 201, 2019. https://arxiv.org/abs/1509.02505
• A. Yu. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR Sb. 39, 1981. https://doi.org/10.1070/SM1981v039n03ABEH001518