All missions

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

Motivation

The quantum linear systems problem asks, given a sparse Hermitian $N \times N$ matrix $A$ with condition number $\kappa$ and a procedure preparing a state $|b\rangle$, to prepare a state close to $A^{-1}|b\rangle / \|A^{-1}|b\rangle\|$. Harrow, Hassidim and Lloyd (2009) gave a quantum algorithm whose running time is polynomial in $\log N$ and $\kappa$ but grows like $1/\varepsilon$ in the target precision $\varepsilon$, because it estimates eigenvalues by phase estimation. Childs, Kothari and Somma (arXiv:1511.02306, SIAM J. Comput. 46(6), 2017) reduced the precision dependence to $\mathrm{poly}\log(1/\varepsilon)$, an exponential improvement.

The reduction has two parts. A quantum part implements a linear combination of unitaries applied to $A$, and turns any function that is $\varepsilon$-close to $1/x$ on the spectrum of $A$ into an approximate preparation of the solution state (Corollary 10 and Proposition 9 of the paper). An analytic part supplies such a function with small degree and small coefficient weight. The paper gives two analytic constructions: a Fourier expansion (Section 3) and an expansion in Chebyshev polynomials (Section 4). This mission formalizes the analytic core of the Chebyshev construction, the input to the paper's Theorem 4. The quantum algorithms and their query and gate counts are not formalized here.

Setting

For a real number $\kappa \ge 1$ (a condition number: the ratio of the largest to the smallest singular value), the domain is

$$D_\kappa := [-1, -1/\kappa] \cup [1/\kappa, 1].$$

A function $g$ is $\varepsilon$-close to $h$ on a set $D \subseteq \mathbb R$ if $|g(x) - h(x)| \le \varepsilon$ for all $x \in D$.

The Chebyshev polynomials of the first kind are $\mathcal T_0(x) = 1$, $\mathcal T_1(x) = x$ and $\mathcal T_{n+1}(x) = 2x\mathcal T_n(x) - \mathcal T_{n-1}(x)$; those of the second kind $\mathcal U_n$ satisfy the same recursion with $\mathcal U_0 = 1$, $\mathcal U_1 = 2x$.

For natural numbers $b, j$ let

$$c_{b,j} := \frac{1}{2^{2b}} \sum_{i=j+1}^{b} \binom{2b}{b+i},$$

the probability of more than $b+j$ heads in $2b$ fair coin flips. The tamed inverse (74) is $f_b(x) = (1 - (1-x^2)^b)/x$, and the odd Chebyshev series is

$$S_{b,n}(x) := 4 \sum_{j=0}^{n-1} (-1)^j c_{b,j}\, \mathcal T_{2j+1}(x).$$

In Lean these are Dκ, coeff b j, fTamed b, and chebSum b n in the namespace QuantumLinSys.Chebyshev; bOf κ ε and j0Of b ε are the parameters $b$ and $j_0$ below.

Formalization targets

Goal: Lemma 14 (p. 16)

With $b = \kappa^2 \log(\kappa/\varepsilon)$ and $j_0 = \sqrt{b\log(4b/\varepsilon)}$, the truncated series

$$g(x) = 4\sum_{j=0}^{j_0} (-1)^j c_{b,j}\, \mathcal T_{2j+1}(x)$$

is $2\varepsilon$-close to $1/x$ on $D_\kappa$, for every $\kappa \ge 1$ and $\varepsilon > 0$.

Milestones, in the order the proof uses them

1. Lemma 17 (p. 19). For integers $d \ge 1$ and $b \ge (\kappa d)^2\log(\kappa d/\varepsilon)$, $f_b$ is $\varepsilon$-close to $1/x$ on $D_{\kappa d}$.
2. Lemma 18 (p. 19). On $[-1,1]$, $f_b = S_{b,b}$ exactly:

$$\frac{1-(1-x^2)^b}{x} = 4\sum_{j=0}^{b-1}(-1)^j c_{b,j}\,\mathcal T_{2j+1}(x).$$

3. Display (89) (p. 21). $c_{b,j} \le e^{-j^2/b}$.
4. Lemma 19 (p. 21). The series truncated at $j_0 = \sqrt{b\log(4b/\varepsilon)}$ is $\varepsilon$-close to $f_b$ on $[-1,1]$.

Two further statements of the same approach are included as companion theorems: Lemma 16 (p. 17), the closed form of the $n$-th power of the $2\times 2$ rotation block in terms of $\mathcal T_n$ and $\mathcal U_{n-1}$, and Proposition 9 (p. 9), the $4\varepsilon$ perturbation bound for normalized states.

Significance

Lemma 14 provides a polynomial of degree $O(\kappa\log(\kappa/\varepsilon))$ whose Chebyshev coefficients have total weight $O(\sqrt{b\log(b/\varepsilon)})$, approximating $1/x$ uniformly on the region where a well-conditioned matrix has its eigenvalues. Applied to a Hermitian matrix through a quantum walk, whose powers implement $\mathcal T_n$ (Lemma 16), it gives the query complexity $O(d\kappa^2\log^2(d\kappa/\varepsilon))$ of Theorem 4. The same polynomial approximation of $1/x$ reappears in later work on quantum singular value transformation and matrix inversion.

All results of this mission are proved in the paper. None of them is machine-checked in Mathlib or on the platform, as far as a search found: Mathlib has the Chebyshev polynomials and the identity $\mathcal T_n(\cos\theta) = \cos n\theta$, but no Chebyshev expansion of a rational function, no binomial tail bound in this form, and no approximation theorem for $1/x$. The formalization produces a checked uniform approximation of $1/x$ with explicit, non-asymptotic parameters.

Difficulty

The exact identity (Lemma 18) has no slack: every coefficient, sign and summation bound of (77) must be right for all $b$, and an off-by-one in the inner sum or in the Chebyshev index makes it false. Mathlib's Chebyshev library offers evaluation facts but no expansion of a given polynomial in the Chebyshev basis. The bound (89) is a Chernoff–Hoeffding tail bound for a symmetric binomial distribution, which must be stated for sums of binomial coefficients rather than for random variables. The goal then needs both approximation errors at the page's specific parameters, including the corner cases in which $\log(\kappa/\varepsilon)$ or $\log(4b/\varepsilon)$ is negative.

Formalization scope

All functions are real functions of one real variable. Chebyshev polynomials are Mathlib's Polynomial.Chebyshev.T ℝ and Polynomial.Chebyshev.U ℝ, indexed by integers. The sum $\sum_{j=0}^{n-1}$ is over Finset.range n, so the series of (55)/(88) truncated at $j_0$ is chebSum b (j₀ + 1) and the full series (77) is chebSum b b.

The formalization commits to the following conventions, each disclosed in the item it affects.

• $\kappa \ge 1$ on every statement that mentions $D_\kappa$, and $d \ge 1$ in Lemma 17. Below these values the domain is empty or contains $0$.
• $\varepsilon > 0$. No upper bound on $\varepsilon$ is imposed in this mission.
• The paper's real $b = \kappa^2\log(\kappa/\varepsilon)$ is rounded up to a natural number in the goal, and the truncation index $j_0$ is rounded down, the sum running over $j = 0,\dots,\lfloor j_0\rfloor$.
• In Lemmas 17–19 $b$ is a natural number. The page's "integer" exponent cannot be negative without making $(1-x^2)^b$ singular.
• At $x = 0$, $f_b(0)$ is Lean's $0/0 = 0$, which is the value of its continuous extension. Lemma 18 is therefore stated on all of $[-1,1]$.
• Proposition 9 is stated for continuous linear operators on $\mathbb C^N$, with $\|C^{-1}\| \le 1$ given as a two-sided inverse of norm at most $1$, and for unit vectors $\psi$.

A trivializing reading is ruled out: the goal fixes the page's $b$, $j_0$ and constant $2\varepsilon$, so neither an arbitrarily large truncation nor a weaker constant satisfies it, and the domain $D_\kappa$ excludes the origin, where Lean's $1/0 = 0$ would make closeness to $1/x$ meaningless.

Useful infrastructure, reusable beyond this mission: Chebyshev expansions of polynomials on $[-1,1]$, binomial tail bounds, and uniform approximation of $1/x$. Contributions of general lemmas of this kind are welcome.

Selected references

• A. M. Childs, R. Kothari and R. D. Somma, Quantum algorithm for systems of linear equations with exponentially improved dependence on precision, SIAM J. Comput. 46(6), 2017; arXiv:1511.02306v2. https://arxiv.org/abs/1511.02306
• A. W. Harrow, A. Hassidim and S. Lloyd, Quantum algorithm for linear systems of equations, Phys. Rev. Lett. 103, 150502, 2009. https://arxiv.org/abs/0811.3171
• D. W. Berry, A. M. Childs and R. Kothari, Hamiltonian simulation with nearly optimal dependence on all parameters, FOCS 2015. https://arxiv.org/abs/1501.01715
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 1963. https://doi.org/10.1080/01621459.1963.10500830

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

Firms increasingly account for, and offset, the greenhouse-gas emissions of their entire supply chain, not only their own operations. Emissions in a supply chain are often jointly produced: the footprint of one process (transport, packaging, a molten-bulk delivery) depends on the abatement efforts of several firms at once. When each firm is charged for "its" emissions, the question is how to allocate the footprint of a jointly produced process so that every firm has the right incentive to abate.

Caro, Corbett, Tan and Zuidwijk (working paper, 2012; published in Manufacturing & Service Operations Management 15(4), 2013) model this as a moral-hazard problem in teams. Their §4 shows that a social planner who wants the first-best efforts must, under joint production, double-count emissions: the marginal payments across firms for one process exceed the carbon price. This mission formalizes §5, which looks at a different institutional arrangement observed in practice. One firm, the carbon leader (the paper's example is the cosmetics company Natura), voluntarily pays for all supply-chain emissions at a carbon price $p$ and compensates the other firms to induce abatement.

Timeline. Holmström (1982) showed that a budget-balanced sharing rule cannot implement efficient efforts in a team. Strausz (1999) showed that sequential moves can restore efficiency. Battaglini (2006) studied joint production with multidimensional output. Caro et al. (2012) placed the carbon leader in this line: a Stackelberg leader whose commitment plays the role of Strausz's sequential structure.

Setting

There are finite sets of firms $\mathcal N$ and processes $\mathcal I$. Firm $n$ chooses efforts $\mathbf e_n\in[0,A]^{m_n}$, one for each of its abatement actions, and the effort profile $\mathbf e$ lies in the box $[0,A]^M$. Firm $n$ earns profit $V_n(\mathbf e_n)$, which is differentiable, concave and componentwise decreasing: effort is costly. Process $i$ emits $f_i(\mathbf e)\ge0$, which is differentiable, convex and componentwise decreasing on the box. The influence matrix $B$ has $b_{n,i}=1$ if firm $n$ influences process $i$, that is, if $\sum_j\partial f_i/\partial e_{n,j}<0$, and $b_{n,i}=0$ otherwise.

The first best at carbon price $c$ maximizes the social value $\sum_n V_n(\mathbf e_n)-c\sum_i f_i(\mathbf e)$ over the box. At the societal cost $c=p_S$ its maximizer is $\mathbf e^*$, assumed unique.

The carbon leader is a firm $N$, written L in Lean. Every other firm $n$ has a reservation profit $\bar\pi_n$. The signed transfer $g_n$ is recorded as a payment by firm $n$; a negative value means compensation from the leader. The leader faces two problems.

• $P_E$ (6)–(8): it sets $g_n(\mathbf e_n)$, contingent on firm $n$'s own effort. It maximizes $V_N(\mathbf e_N)-p\sum_i f_i(\mathbf e)+\sum_{n\ne N}g_n(\mathbf e_n)$ subject to participation, $V_n-g_n\ge\bar\pi_n$, and incentive compatibility, $\mathbf e_n$ being a best response. Its optimal value is $z^E$, attained at efforts $\mathbf e^E$.
• $P_F$ (9)–(11): the same problem, except that the payments $g_n(\mathbf f)$ may depend only on the emissions vector $\mathbf f=\mathbf f(\mathbf e)$, because efforts cannot be verified.

Formalization targets

Goal: Proposition 5 (p. 16)

Let $(g^E,\mathbf e^E)$ be optimal for $P_E$ and define, for $n\neq N$,

$$g_n(\mathbf f)=p\sum_{i\in\mathcal I}b_{n,i}f_i+k_n,\qquad k_n=V_n(\mathbf e^E_n)-p\sum_{i\in\mathcal I}b_{n,i}f_i(\mathbf e^E)-\bar\pi_n.\qquad(12)$$

Then $(g,\mathbf e^E)$ is feasible for $P_F$, its value equals $z^E$, and every feasible solution of $P_F$ has value at most $z^E$:

$$\max P_F \;=\; z^E \;=\; \max P_E .$$

Milestones (proof in App. A.4, p. 26)

1. Reduction of $P_E$ (p. 15). $z^E=\max_{\mathbf e}\big[\sum_n V_n(\mathbf e_n)-p\sum_i f_i(\mathbf e)\big]-\sum_{n\ne N}\bar\pi_n$, attained at $\mathbf e^E$.
2. Participation under (12). $V_n(\mathbf e^E_n)-g_n(\mathbf f(\mathbf e^E))=\bar\pi_n$ for $n\ne N$.
3. First-order identity. $\partial V_n(\mathbf e^E)/\partial e_{n,j}=p\sum_i b_{n,i}\,\partial f_i(\mathbf e^E)/\partial e_{n,j}$ for $n\neq N$.
4. Incentive compatibility under (12). $\mathbf e^E_n$ maximizes $V_n(\mathbf x)-g_n(\mathbf f(\mathbf e^E_{-n},\mathbf x))$ over firm $n$'s box.
5. Upper bound. Every feasible solution of $P_F$ has value at most $z^E$.

Companion: Lemma 6 (p. 17)

If $0\le p<p_S$, each $V_n$ is supermodular and each $f_i$ is submodular, then $\mathbf e^E\le\mathbf e^*$ componentwise.

Significance

The result. Proposition 5 says that, when efforts are unobservable, a carbon leader that can commit loses nothing compared with contracting on efforts. A linear rule, the form footprint accounting already takes in practice, achieves the benchmark. The rule charges each firm the full price $p$ on every footprint it influences, so emissions are double-counted internally, yet the supply chain as a whole pays for carbon once. This is how the paper reconciles its §4 impossibility (a planner must double-count) with a footprint-balanced scheme: the leader moves first and is excluded from the incentive constraints. Lemma 6 then says that a leader paying a price below the societal cost induces weakly less effort than the first best.

Formalizing it. Both results are proved in the paper. As far as the platform's catalog shows, neither is machine-checked anywhere. The proof of Proposition 5 combines a reduction of a bilevel problem with a first-order argument for concave games on a box. The appendix compresses these into three sentences, one of which contains a misprint ("since f is concave" for convex). Formalizing it makes the leader–follower conventions explicit: the leader's tie-breaking choice of follower efforts, and the unilateral deviation in (11).

Difficulty

The paper calls $P_F$ a constrained version of $P_E$, but their feasible sets are not literally nested: $P_F$'s payments are functions of the emission vector and $P_E$'s of a firm's own effort. Establishing the common upper bound therefore requires care with the two payment domains and the participation constraint (10).

The incentive compatibility of (12) is the substantive step. It is a global best-response claim on a closed effort box, while the appendix states only a first-order identity at an interior point. The influence indicator $b_{n,i}=0$ also has to agree with every action-level derivative, rather than only their sum. For Lemma 6, the optimum at price $p$ need not be unique.

Formalization scope

• Indices. Firms, actions and processes are finite types. Efforts are e : (n : ι) → act n → ℝ, and a unilateral deviation is Function.update.
• Partial derivatives. A partial derivative is the one-variable deriv along one coordinate. Every theorem that uses one assumes differentiability.
• Optimality. "Optimal" means feasible with value at least that of every feasible point, never sSup. $z^E$ is the $P_E$ objective at an optimal pair.
• Influence matrix. $B$ is a real 0/1 matrix, and its defining sign condition is assumed at every profile in the box.
• Interiority. $\mathbf e^E$ is assumed interior, the page's "A is a sufficiently large bound to guarantee interior solutions"; the box itself stays closed.
• Followers' efforts. In $P_E$ and $P_F$ the leader chooses the followers' efforts subject to the best-response constraints, as the page assumes.
• Hypotheses not imposed. The row and column sums of $B$, the strictness of $c_n$ and $g_n\le0$ are unused and not imposed.

Rule (12) is a function of the emission vector only, and the deviation in (11) moves only firm $n$'s efforts. A formalization in which payments may depend on efforts, or in which a deviation also moves the leader, would make the goal trivial and is ruled out. A sorry-free instance with two firms checks that every hypothesis of the goal can be satisfied. Supermodularity reuses the published Supermodularity.Monotonicity.SupermodularOn. All other definitions live in CarbonDoubleCount.Leader.Setting.

Proofs of the milestones, or alternative routes such as a Lagrangian argument for incentive compatibility, are welcome. A general lemma that a concave differentiable function on a box is maximized at an interior stationary point would be reusable beyond this mission.

Selected references

• F. Caro, C. J. Corbett, T. Tan, R. Zuidwijk, Double-Counting in Supply Chain Carbon Footprinting, working paper dated December 21, 2012; Manufacturing & Service Operations Management 15(4), 2013. https://doi.org/10.1287/msom.2013.0443
• B. Holmström, Moral Hazard in Teams, Bell Journal of Economics 13(2), 1982. https://doi.org/10.2307/3003457
• R. Strausz, Efficiency in Sequential Partnerships, Journal of Economic Theory 85, 1999. https://doi.org/10.1006/jeth.1998.2488
• M. Battaglini, Joint Production in Teams, Journal of Economic Theory 130(1), 2006. https://doi.org/10.1016/j.jet.2005.03.003
• D. M. Topkis, Minimizing a Submodular Function on a Lattice, Operations Research 26(2), 1978. https://doi.org/10.1287/opre.26.2.305
• R. K. Sundaram, A First Course in Optimization Theory, Cambridge University Press, 1996. https://doi.org/10.1017/CBO9780511804526

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