Operations Research

Motivation

A seller who knows the distributions of a buyer's values for several goods can, in principle, design a mechanism that offers lotteries and prices conditional on the buyer's reported values. Finding the best such mechanism can be difficult even with two goods. Separate selling is much simpler: choose a one-good price for each item and let the buyer decide item by item. The question is how much revenue this simplicity can cost when the goods' values are independent. Hart and Nisan establish a guarantee that declines only with the square of the logarithm of the number of goods, even though the distributions need not be identical or bounded. Their result is Theorem C of Approximate Revenue Maximization with Multiple Items, stated on p. 7 and proved on p. 26.

The paper grew from the problem of comparing easy selling formats with fully optimal mechanisms. For one good, a posted price characterizes optimal revenue. With multiple goods, the choice of a mechanism becomes genuinely multidimensional: its allocation rule can correlate the disposition of the goods and use lotteries. The guarantee in this mission applies uniformly over all independent distributions on nonnegative valuations, so a seller does not need a regularity, density, or finite-moment assumption to use it.

Setting

There is one seller, one risk-neutral buyer, and $k\ge2$ goods. The buyer's valuation vector is $x=(x_i)_{i=1}^k\in\mathbb R_+^k$; receiving a set of goods gives the sum of the values of its members. The seller knows the joint law of the random vector $X$, but not its realization. In this mission the coordinates $X_i$ are independent, with possibly different probability laws $\nu_i$.

A direct mechanism consists of an allocation rule $q_i(x)\in[0,1]$ for each good and a real payment $s(x)$. At a truthful report $x$, the buyer's payoff is $b(x)=\sum_i q_i(x)x_i-s(x)$. The mechanism is incentive compatible if truthful reporting is at least as good as every alternative report, and individually rational if $b(x)\ge0$ for every $x$. The seller's expected payment is its revenue. The optimal revenue $\operatorname{Rev}(X)$ is the supremum of revenue over such mechanisms. Payments are taken to be measurable, following footnote 12 on p. 12 of Hart and Nisan.

For one good, $\operatorname{Rev}(X_i)$ equals the supremum of $p\Pr[X_i\ge p]$ over prices $p\ge0$, as in display (1) on p. 12. The separate revenue is $\operatorname{SRev}(X)=\sum_i\operatorname{Rev}(X_i)$. The bundled revenue is $\operatorname{BRev}(X)=\operatorname{Rev}(\sum_i X_i)$, where the sum is treated as one good. Both formats are defined through one-good revenue, even when the full optimum can use multidimensional allocations.

Formalization targets

Theorem C: a uniform guarantee for separate selling

The goal is the inequality form of Theorem C, with one constant that works for every number and every family of independent goods:

$$\exists c>0\;\forall k\ge2\;\forall (\nu_i)_{i=1}^k,\qquad \operatorname{SRev}(X_1,\ldots,X_k) \ge \frac{c}{(\log k)^2}\operatorname{Rev}(X_1,\ldots,X_k).$$

Here $X_i$ has law $\nu_i$, and the joint law is their product. The paper phrases the headline as a guarantee for an approximation ratio; the displayed inequality is the form used in its proof on p. 26. It handles zero and infinite optimal revenues without introducing a ratio with an undefined denominator.

Supporting targets

The milestone list records the one-good posted-price formula, monotonicity under first-order stochastic domination, the equal-revenue comparison of Lemma 20, Proposition 13(ii)'s comparison of separate and bundled revenue, the two inequalities of Theorem 7, and the two-good base case of Theorem A. It also records the power-of-two estimate and the zero-padding assertion stated in the proof of Theorem C. Each milestone is attached to its source page in the pinned preprint.

Significance

The theorem gives a distribution-independent performance floor for a mechanism that can be run using one price per good. It applies to unequal and unbounded independent distributions, for which expected values can be infinite while one-good optimal revenues remain finite. The comparison is with the best incentive-compatible and individually rational multi-good mechanism, including randomized allocations, rather than with another simple selling format. The result is proved in the 2017 preprint; the open work here is a machine-checked formalization of that known result and its selected supporting statements.

The formal development also supplies reusable objects: a law-based direct-mechanism model, extended-real expected revenue, product laws for independent groups of goods, and first-order stochastic domination of one-good laws. These are useful for other comparisons among separate selling, bundling, and optimal mechanisms in the same paper. The mission does not pose the paper's distinct i.i.d. bundling theorem, multi-buyer results, or tightness examples.

Difficulty

The main obstacle is that optimal multi-good revenue is not monotone in the values of the goods. Increasing each coordinate of a valuation vector does not, by itself, give a valid comparison between the optimal revenues of the two vectors' laws; Hart and Nisan, p. 23 explicitly warn against that inference. One-good revenue does have the needed monotonicity, but the full optimum can depend on how the goods interact in an incentive-compatible mechanism. Theorem 7 is a substantive bridge between these two regimes. Infinite expected values also make a real-valued integral or an ordinary ratio unsuitable for the general statement.

Formalization scope

Goods are indexed by finite types, and valuations lie in $\mathbb R_{\ge0}^k$. Each good's law is a probability measure; independence means the product law, while Theorem 7 allows dependence among coordinates within each of its two independent groups. A one-good law is represented by a singleton coordinate type. Revenue takes values in $\mathbb R_{\ge0}\cup\{\infty\}$, and the expectation of a mechanism's possibly negative payment is represented in extended reals. The supremum defining optimal revenue ranges only over feasible, incentive-compatible, individually rational mechanisms with measurable payments. Theorem C quantifies $c$ before $k$ and the laws, and the restriction $k\ge2$ keeps the logarithmic coefficient in its stated domain.

The equal-revenue law is represented by the density $x^{-2}$ on $[1,\infty)$, mapped to nonnegative reals. First-order stochastic domination compares the upper-tail probabilities at nonnegative thresholds, which is equivalent to testing every real threshold for nonnegative valuations. A complete proof will need measure-theoretic facts about that law, the posted-price characterization, product measures, and operations on extended nonnegative revenue. Contributions to those reusable facts and to the selected milestone theorems are within scope.

Selected references

• Sergiu Hart and Noam Nisan, Approximate Revenue Maximization with Multiple Items, arXiv:1204.1846v3, 2017. Preprint.

Motivation

In a cost sharing game (or, symmetrically, a revenue sharing game) self-interested players each pick a set of resources, every resource generates a welfare that depends on who uses it, and a distribution rule splits that welfare among the users. Network formation, atomic routing, coverage and distributed-control problems all fit this model (Anshelevich et al. 2004; Marden and Wierman, Distributed welfare games, 2013; see §2 of the paper). The designer controls only the distribution rule, and the first requirement on a rule is that the games it induces have a pure Nash equilibrium; without one, equilibrium-based efficiency guarantees say nothing.

Which rules guarantee equilibria? The Shapley value and its weighted and generalized-weighted versions do, because they induce potential games (Hart and Mas-Colell 1989). Chen, Roughgarden and Valiant (2010) and Marden and Wierman (Overcoming the limitations of utility design for multiagent systems, 2013) showed that, among budget-balanced rules, these are the only ones that work for every welfare function, by exhibiting one worst-case welfare function (Proposition 1 of the paper, p. 9). Marden and Wierman (Distributed welfare games) also showed that when players may choose only one resource, other budget-balanced rules can work. That left open what happens when the designer knows the welfare functions in advance, and whether dropping budget-balance enlarges the set of good rules. Gopalakrishnan, Marden and Wierman 2014 answered both questions: for any fixed set of welfare functions, with or without budget-balance, the equilibrium-guaranteeing rules are exactly generalized weighted Shapley values on suitable ground welfare functions.

Setting

Players are $N=\{1,\dots,n\}$ with $n>1$; resources are $R=\{r_1,\dots,r_m\}$ with $m>1$. A local welfare function is $W:2^N\to\mathbb R$ and a distribution rule is $f:N\times2^N\to\mathbb R$, where $f(i,S)$ is the share of player $i$ when sharing with the coalition $S$ (and $f(i,S)=0$ for $i\notin S$). Each player $i$ has a nonempty action set $\mathcal A_i\subseteq 2^R$. In an allocation $a$, the users of $r$ are $\{a\}_r=\{i:r\in a_i\}$ and player $i$ receives

$$U_i(a)=\sum_{r\in a_i}f^{W_r}\bigl(i,\{a\}_r\bigr).$$

Resources with equal welfare functions use the same rule. For a nonempty set $\mathbb W$ of welfare functions, $\mathcal G(N,f^{\mathbb W},\mathbb W)$ is the class of all such games with every $W_r\in\mathbb W$, any number of resources and any action sets. A rule is budget-balanced for $W$ if $\sum_{i\in S}f(i,S)=W(S)$.

A weight system $\omega=(\lambda,\Sigma)$ consists of positive weights $\lambda_i$ and an ordered partition $\Sigma=(S_1,\dots,S_K)$ of $N$ into priority classes. For nonempty $T$, $\overline T=T\cap S_k$ with $k$ the first class meeting $T$. With the basis coefficients $q^W_T=\sum_{R\subseteq T}(-1)^{|T|-|R|}W(R)$, the generalized weighted Shapley value is

$$f^W_{GWSV}[\omega](i,S)=\sum_{T\subseteq S:\,i\in\overline T}\frac{\lambda_i}{\sum_{j\in\overline T}\lambda_j}\,q^W_T .$$

The distributed welfare of a rule is $W'(S)=\sum_{i\in S}f^W(i,S)$, display (10).

Formalization targets

Goal: Theorem 1

$$\text{all games in }\mathcal G(N,f^{\mathbb W},\mathbb W)\text{ have a pure Nash equilibrium}\iff\exists\,\omega\ \forall W\in\mathbb W:\ f^W=f^{W'}_{GWSV}[\omega]\text{ on }\{(i,S):i\in S\},$$

with $W'$ the distributed welfare of $f^W$. One weight system serves all of $\mathbb W$.

Milestones

The "if" direction (Appendix A, p. 16). For a single $W$ and a budget-balanced $f$ guaranteeing equilibria: $f(i,S)=0$ when $S$ contains no contributing coalition (Lemma 1) and for non-contributing $i$ (Lemma 2); $f(i,S)=f(i,N(S))$ (Lemma 3). The basis rules $f^T$ of the recursion (27) are budget-balanced for the inclusion functions (Lemma 5), recover $f=\sum_Tq_Tf^T$ (Lemma 7), obey an inclusion–exclusion principle (Corollary 1), and are generalized weighted Shapley basis rules $f^T_{GWSV}[\omega^T]$ (Lemma 8). Across welfare functions the basis shares are consistent pairwise (Lemma 9) and around cycles (Lemma 10); the induced relation on players is a partial order modulo equivalence (Lemma 11), and one universal weight system replaces all $\omega^{W,T}$ (Lemma 13).

Companions

Proposition 2: for welfare functions normalized by $W'(\emptyset)=W''(\emptyset)=0$, $f^{W'}_{GWSV}[\omega]=f^{W''}_{GWMC}[\omega]$ iff $\mathcal T'=\mathcal T''$ and $q'_T=(\sum_{j\in\overline T}\lambda_j)q''_T$. Theorem 2: the same characterization with generalized weighted marginal contributions on $W''=h(W')$.

Significance

The theorem settles the design space completely: a designer who wants equilibria in every game over known welfare functions must use a generalized weighted Shapley value, and the only freedom is the weight system and the ground welfare functions, which control budget-balance. Since these rules induce (generalized weighted) potential games, potential games are necessary for guaranteed equilibrium existence in this model, and computing shares inherits the exponential cost of Shapley values. Theorem 2 gives the marginal-contribution form, which needs one marginal contribution per share.

The paper proves Theorem 1 with a full appendix of counterexample constructions; none of it has a published machine-checked proof. The mission asks for a Lean proof of the characterization, of the reusable structure behind it (necessary conditions, basis decomposition, inclusion–exclusion for basis rules, consistency of weight systems), and of the Shapley–marginal-contribution correspondence.

Difficulty

The "if" direction is a potential argument. The "only if" direction is not: every necessary condition is proved by building, from a hypothetical violation, a specific game with no equilibrium, and the games grow more elaborate as the conditions do. Lemma 8 needs the inclusion–exclusion principle to isolate a single basis share, using many weighted copies of resources; Lemma 10's proof combines best-response cycles over $k$ welfare functions and is partly omitted on the page ("We omit the proof for brevity", p. 51), so it is the hardest milestone. A tempting shortcut, applying the worst-case result of Chen et al. and Marden–Wierman (Proposition 1, p. 9), fails: it uses one worst-case welfare function, while here $\mathbb W$ is arbitrary and may not contain it.

Formalization scope

Players are Fin n, resources Fin m, an action is a Finset (Fin m) (the empty action is allowed). The family of rules is one function f : Welfare n → Rule n, which encodes that equal welfare functions get equal rules. GuaranteesPNE 𝕎 f quantifies over every m > 1, every assignment Fin m → 𝕎 (repetitions allowed: the counterexamples rely on many copies of one welfare function) and every family of nonempty action sets. A weight system stores a block index Fin K per player (empty blocks allowed) and positive weights. Rules are compared only at $i\in S$. Contributing coalitions exclude $\emptyset$ (Appendix A's normalization $W(\emptyset)=0$). The recursion (27) divides by $q_T$ and is used only for contributing $T$; where it reads $f(i,T)$ with $i\notin T$, the paper's convention $f(i,S)=0$ off $S$ is a hypothesis.

The ground welfare in Theorem 1 is the distributed welfare (10), written out, never an arbitrary function: an existentially quantified ground welfare would make the right side easier and the theorem a different one. The weight system is quantified before the welfare functions, and empty action sets are excluded; with them no game would have an equilibrium and the theorem would claim that no rule is a Shapley value.

Disclosed readings: Lemma 11's "partial order" is antisymmetry modulo the equivalence $=^+_\Omega$, as the proof states; in (74) the first block $S_1^{W,T}$ is read on $T$ as its positive-share block $\overline T$. Proposition 2 carries $W'(\emptyset)=W''(\emptyset)=0$ so that the paper's basis support, which ranges over all coalitions, agrees with the local support of nonempty coalitions.

A complete development needs: finite games and pure equilibria on resource-selection models, Möbius inversion on Finset lattices, the potential argument for generalized weighted Shapley values (shared with the companion mission on generalized weighted potential games), and counterexample games built from copies of resources. The game model and the basis-rule recursion are reusable for other cost-sharing results. Proofs of any milestone, and alternative arguments for the necessary conditions, are welcome.

Selected references

• R. Gopalakrishnan, J. R. Marden, A. Wierman, Potential Games are Necessary to Ensure Pure Nash Equilibria in Cost Sharing Games, Math. Oper. Res. 39(4), 2014; preprint arXiv:1402.3610v1, 2014. https://arxiv.org/abs/1402.3610v1
• S. Hart, A. Mas-Colell, Potential, Value, and Consistency, Econometrica 57(3), 589–614, 1989. https://doi.org/10.2307/1911054
• H.-L. Chen, T. Roughgarden, G. Valiant, Designing Network Protocols for Good Equilibria, SIAM J. Comput. 39(5), 1799–1832, 2010 (reference [8] of arXiv:1402.3610v1).
• J. R. Marden, A. Wierman, Overcoming the Limitations of Utility Design for Multiagent Systems, IEEE Trans. Autom. Control, 2013 (reference [30] of arXiv:1402.3610v1).
• J. R. Marden, A. Wierman, Distributed Welfare Games, Oper. Res., 2013 (reference [29] of arXiv:1402.3610v1).
• E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler, T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, FOCS 2004, 295–304 (reference [3] of arXiv:1402.3610v1).
• L. S. Shapley, A Value for n-Person Games, Contributions to the Theory of Games II, Princeton University Press, 1953 (reference [43] of arXiv:1402.3610v1).

Motivation

Retailers observe demand signals (point-of-sale data, local forecasts) that their suppliers do not. Whether a retailer should pass such a signal upstream is a central question of the supply chain information-sharing literature. In a single chain, sharing helps the manufacturer plan, but the retailer may lose from it. Competition between chains adds a second effect: sharing in one chain changes how the rival chain responds to its own signal.

Ha, Tian and Tong (MSOM 2017) study this question when the manufacturer's planning decision is production cost reduction: a manufacturer that knows more about demand can invest in lowering its unit cost more efficiently. They find that the equilibrium of the information-sharing game between two competing chains depends on a single efficiency parameter $k$ in a three-regime pattern. This mission formalizes that pattern for quantity (Cournot) competition.

Earlier work on information sharing in competing chains (for example Ha, Tong and Zhang, Management Science 2011, on production diseconomies of scale) found related threshold structures under different upstream technologies. The present paper replaces the production cost with a cost-reduction investment.

Setting

There are two identical supply chains $i=1,2$, each with one manufacturer and one retailer. Retailer $i$ faces the inverse demand

$$p_i=a+\theta-q_i-\gamma_C q_j,$$

where $\theta$ is a demand shock with mean $0$ and variance $\sigma^2$, and $\gamma_C\in(0,1)$ is the competition intensity. Manufacturer $i$ has unit production cost $c$ and lowers it by $x_i$ at effort cost $\tfrac12 kx_i^2$; a small $k$ means efficient cost reduction. Retailer $i$ observes a signal $Y_i$ with accuracy $t$; under the linear information structure, $E[\theta\mid Y_i]=E[Y_j\mid Y_i]=\tfrac{t\sigma^2}{1+t\sigma^2}Y_i$.

In stage one, each chain fixes its arrangement $X_i\in\{S,N\}$: the retailer shares its signal with the manufacturer ($S$) or not ($N$). Then the manufacturer sets a wholesale price and a cost reduction, and the retailer a quantity. For each arrangement profile $(X_i,X_j)$ the quantity stage has a linear equilibrium $q_i=\bar q+C^{X_iX_j}Y_i$ with explicit response coefficients $C^{X_iX_j}(k,\gamma_C,t,\sigma^2)$ (Lemma 2(a)). These give closed-form ex-ante profits $\Pi^{X_iX_j}_{R_i,C}$, $\Pi^{X_iX_j}_{M_i,C}$ and $\Pi^{X_iX_j}_{i,C}$ for the retailer, the manufacturer and the chain.

The value of information sharing to chain $i$ is $V^{X_j}_{i,C}=\Pi^{SX_j}_{i,C}-\Pi^{NX_j}_{i,C}$. In stage one, manufacturer $i$ offers retailer $i$ the smallest side payment $\hat m^{X_j}$ that makes sharing acceptable to the retailer, and chooses $S$ or $N$. The result is a symmetric $2\times2$ game between the two manufacturers (Table 1). Manufacturer $i$'s payoff is $\Pi^{SX_j}_{M_i,C}-\hat m^{X_j}$ for $S$ and $\Pi^{NX_j}_{M_i,C}$ for $N$. The standing assumptions are $k>a/(4c)$, $k>1/3$ and $a>c$.

Formalization targets

Goal: Proposition 7(a)

For fixed $\gamma_C\in(0,1)$, $t>0$ and $\sigma^2>0$ there are thresholds

$$\tfrac12<k^N_C<k^S_C<\tfrac{3+\sqrt5}{4}$$

such that the set $\mathcal E$ of pure-strategy equilibria of the stage-one game is

$$\mathcal E=\{(S,S)\}\ (k<k^N_C),\qquad \mathcal E=\{(S,S),(N,N)\}\ (k^N_C<k<k^S_C),\qquad \mathcal E=\{(N,N)\}\ (k>k^S_C).$$

In the middle regime, both manufacturers are strictly better off at $(S,S)$ than at $(N,N)$.

Milestones

• the linear strategies solve the best responses (proof of Lemma 2(a));
• $C^{X_jX_i}_j<1$ and the four coefficient differences in closed form with their signs (proof of Lemma 3);
• the retailer gains from sharing if and only if $k\le1/2$, and for $k\le1/2$ free information strictly raises the manufacturer's profit (§5.3);
• $V^S_{i,C}>0\iff g>0$ and $V^N_{i,C}>0\iff h>0$ for two explicit polynomials $g,h$ (proof of Proposition 6(a));
• Proposition 6(a): $V^S_{i,C}>0\iff k<k^S_C$, $V^N_{i,C}>0\iff k<k^N_C$, the bounds above, and both thresholds strictly decreasing in $t$ and in $\gamma_C$.

A companion item states the Cournot half of Proposition 7(c): for $k<1/2$ no side payment is needed and $(S,S)$ is the unique equilibrium.

Significance

Proposition 7(a) separates three regimes of cost-reduction efficiency. When cost reduction is efficient ($k<k^N_C$), sharing is dominant. At intermediate efficiency the stage-one game is a coordination game: both chains sharing is Pareto-better for the manufacturers, but both not sharing is also an equilibrium. When cost reduction is inefficient, no chain shares. Competition matters through the gap $k^N_C<k^S_C$: a chain whose rival shares tolerates a less efficient cost reduction before it stops sharing, and the thresholds fall as signals become more accurate or competition more intense.

The paper proves these facts by hand-checked algebra, often stated as "we can verify". The formalization turns each such step into a checked statement: the fixed-point identities behind Lemma 2(a), the closed forms of Lemma 3, the reduction of the sign of $V$ to the polynomials $g$ and $h$, and the monotonicity and location of their roots. None of these results has a machine-checked proof yet. The definitions (response coefficients, profits, side payment, stage-one game) are reusable for the Bertrand half of the paper and for other two-chain information-sharing models.

Difficulty

The obvious approach expands $V^S$ and $V^N$ as rational functions of $(k,\gamma_C,t,\sigma^2)$ and tries to read off their signs. That does not finish by itself. After cancelling positive factors, the signs are those of $g$ and $h$, which are quadratics in $\xi=t^2\sigma^4\gamma_C^2/(t\sigma^2+1)^2\in(0,1)$ with coefficients polynomial in $k$. The thresholds are defined implicitly by a root of each quadratic crossing $\xi$. Showing that $\{g>0\}$ and $\{h>0\}$ are initial intervals of $(1/3,\infty)$ needs the relevant root to be strictly decreasing in $k$, to exceed $1$ below $k=1/2$ and to change sign at $(3+\sqrt5)/4$. The strict ordering $k^N_C<k^S_C$ needs a comparison of two roots involving $\sqrt{k^3(6k-1)}$ and $\sqrt{k(6k-1)}$ on $(1/2,(3+\sqrt5)/4)$. The equilibrium analysis then needs the retailer comparison, to know when the side payment is positive. Table 1's payoff entries are valid only in that case.

Formalization scope

Everything is over $\mathbb R$, in the namespace CompetingChains.Cournot. A general definition TwoPlayerGame gives pure-strategy Nash equilibria of a two-player normal-form game. The definition Setting records the paper's reduced form: the standing assumptions, the response coefficients $C^{X_iX_j}$ of Lemma 2(a), the best responses (7) and (9), the ex-ante profit functions of p. 17, the equilibrium profits $\Pi^{X_iX_j}=\pi^{X_i}(C_j^{X_jX_i})$, $V$, $\hat m$, the stage-one payoff and its set of pure equilibria. The Bayesian stages enter only through these closed forms. The arrangements are an inductive type {S, N}. Manufacturer 2's payoff at $(X_1,X_2)$ is manufacturer 1's payoff at $(X_2,X_1)$. The chain profit is defined as retailer plus manufacturer profit. The stage-one payoff uses $\hat m$ as printed on p. 21, and agrees with Table 1 whenever the side payment is positive.

Conventions and added hypotheses, each disclosed in the items:

• $\gamma_C>0$ wherever the result needs it; at $\gamma_C=0$ the chains do not interact and the middle regime is empty. Positivity of $c$, $t$ and $\sigma^2$ is part of the standing assumptions.
• The goal's "otherwise" is read as $k>k^S_C$, because both profiles are equilibria at $k=k^N_C$ and $k=k^S_C$.
• Only pure-strategy equilibria are counted. "Unique equilibrium" is equality of the equilibrium set with a singleton, not membership.
• The thresholds depend on $(\gamma_C,t,\sigma^2)$ only and are chosen before $a,c,k$.
• "Decreasing" means strictly decreasing.
• Every division is real division by a quantity positive under $k>1/3$, $\gamma_C\ge0$, $t\sigma^2>0$. These hypotheses are carried in every theorem, so no statement is about Lean's value $x/0=0$.

The coefficients, profits, $V$ and payoffs are definitions, never free parameters. A statement with free coefficients, a goal whose thresholds lack $k^N_C<k^S_C$, or one that only asserts membership of $(S,S)$ would be trivial or weaker, and is not what is posed. No published platform definition states this model, so none is referenced.

Not in scope: Lemma 2's uniqueness (delegated by the paper to earlier work), the wholesale-price and cost-reduction lines of Lemma 2(a), the Bertrand half (Propositions 6(b), 7(b)), the single-chain analysis of §4, Proposition 8 and the numerical study. Proofs of any item are welcome. The polynomial root analysis behind Proposition 6(a) is the main open piece of work.

Selected references

• A. Y. Ha, Q. Tian and S. Tong, Information Sharing in Competing Supply Chains with Production Cost Reduction, Manufacturing & Service Operations Management 19(2), 2017. https://doi.org/10.1287/msom.2016.0607
• A. Y. Ha, S. Tong and H. Zhang, Sharing Imperfect Demand Information in Competing Supply Chains with Production Diseconomies, Management Science 57(3), 566–581, 2011. https://doi.org/10.1287/mnsc.1100.1295

Motivation

A seller with several goods and a single buyer of unknown, additive valuation faces the multi-dimensional revenue maximization problem. For one good the answer is classical: by Myerson's theorem (Myerson 1981) a single posted price is optimal. For two or more goods no such simplification exists in general: optimal mechanisms may randomize, may offer menus of lotteries, and are rarely known in closed form. Selling the grand bundle at one price is the simplest multi-good mechanism, and it is used widely in practice.

Hart and Nisan (arXiv:1204.1846, J. Econ. Theory 2017) quantify how much revenue simple mechanisms lose. Most of their results are approximation bounds. Section 7.2 of the paper also contains an exact result: for two independent and identically distributed goods whose density decays fast enough, in the sense of a differential inequality, bundling is exactly optimal. This mission formalizes that theorem, Theorem 16, and the steps of its proof in Appendix A.6.

Timeline. Manelli and Vincent (2006) gave conditions under which a bundled mechanism is optimal for a multiple-good monopolist. Hart and Nisan's preprint (2012, revised 2017) proved Theorem 16 with the condition $x f'(x) + \tfrac32 f(x) \le 0$. Daskalakis, Deckelbaum and Tzamos (2017) later gave a strong duality theory for the multiple-good monopolist, based on optimal transport.

Setting

There are two goods and one buyer. A valuation is a vector $x = (y, z) \in \mathbb{R}^2_+$. The buyer's values $Y, Z$ are i.i.d. with a one-good law $F$ on $\mathbb{R}_+$.

A mechanism $\mu = (q, s)$ assigns to each reported valuation $x$ an allocation vector $q(x) \in [0,1]^2$ ($q_i(x)$ is the probability that good $i$ is sold) and a payment $s(x) \in \mathbb{R}$. The buyer's payoff is $b(x) = q(x)\cdot x - s(x)$. The mechanism is

• incentive compatible (IC) if $b(x) \ge q(\tilde x)\cdot x - s(\tilde x)$ for all $x, \tilde x \in \mathbb{R}^2_+$;
• individually rational (IR) if $b(x) \ge 0$ for all $x$;
• NPT (no positive transfer) if $s \ge 0$.

The revenue of $\mu$ is $R(\mu; X) = \mathbb{E}[s(X)]$, and the optimal revenue is $\mathrm{Rev}(X) = \sup R(\mu; X)$ over all IC and IR mechanisms. The bundled revenue is $\mathrm{BRev}(X) = \mathrm{Rev}(Y + Z)$, the optimal revenue from selling the bundle as a single good.

A two-good mechanism is symmetric if $q_1(y,z) = q_2(z,y)$ and $s(y,z) = s(z,y)$. For a level $a \ge 0$, the bundled majorant $\hat\mu = (\hat q, \hat s)$ of $\mu$ is

$$\hat q(y,z) = \bigl(q_1(y+z-a, a),\ q_1(y+z-a, a)\bigr), \qquad \hat s(y,z) = \hat q(y,z)\cdot(y,z) - b(y+z-a, a).$$

It depends on $(y,z)$ only through $y + z$, so it is a bundled mechanism.

Formalization targets

Goal: Theorem 16

Let $a > 0$ and let $F$ have a density $f$ supported in $[a, \infty)$, differentiable on $(a,\infty)$, with

$$x f'(x) + \tfrac32 f(x) \le 0 \qquad (x > a). \tag{9}$$

Then for two i.i.d.-$F$ goods,

$$\mathrm{Rev}(X_1, X_2) = \mathrm{BRev}(X_1, X_2) = \mathrm{Rev}(X_1 + X_2).$$

The substance is $\mathrm{Rev} \le \mathrm{BRev}$. The reverse inequality holds for every law, and the second equality is the definition of $\mathrm{BRev}$.

Milestones

1. Proposition 5 (at least one good): IC holds if and only if $b$ is convex and $q(x)$ is a subgradient of $b$ at every $x$.
2. Proposition 6 (iii) (at least one good): the supremum defining $\mathrm{Rev}$ may be restricted to NPT mechanisms.
3. Symmetrization (p. 32): for i.i.d. goods, the symmetrization $\bar\mu$ is IC, IR, NPT and symmetric, and it has the same revenue.
4. Display (18): for symmetric IC $\mu$ and $y, z \ge a$, $b(y,z) \le b(y+z-a, a)$.
5. $\hat\mu$ is feasible, IC and IR on the quadrant $[a,\infty)^2$, and bundled.
6. Under (9), $R(\mu; X) \le R(\hat\mu; X)$ for symmetric IC, IR and NPT $\mu$.

Companion: Corollary 17

For two i.i.d. goods with the equal-revenue law $\mathbb{P}[V \ge p] = 1/p$ ($p \ge 1$),

$$\mathrm{Rev}(V_1,V_2) = \mathrm{BRev}(V_1,V_2) = 2(w+1) \approx 2.56,$$

where $w e^{w+1} = 1$.

Significance

Theorem 16 is one of the few closed-form optimality results for multi-good monopoly. It gives an explicit, checkable condition: $x^{3/2} f(x)$ is nonincreasing. The condition covers the equal-revenue distribution and Pareto distributions with index $\alpha \ge 1/2$. On these distributions the optimal revenue reduces to a one-dimensional pricing problem for $Y + Z$. Corollary 17 is the resulting exact value for two equal-revenue goods. Elsewhere in the paper, Theorems C and D use the equal-revenue law as the extremal example for the approximation ratios.

The theorem is proved in the paper. As far as is known it has not been machine-checked. The mission formalizes the model and every step of the proof as a separate milestone. These steps are Rochet's characterization (Proposition 5), the NPT reduction, symmetrization, the convexity majorization (18), and the revenue comparison under (9). Propositions 5 and 6 (iii) and symmetrization are shared with other missions of this series, so they are reusable beyond Theorem 16.

Difficulty

The obvious approach is to show that the optimal mechanism is bundled by exhibiting it. This fails because nothing is known about the optimal mechanism, and it need not exist. The proof instead compares an arbitrary symmetric mechanism with its bundled majorant $\hat\mu$. A pointwise comparison fails: $\hat b \ge b$ does not imply $\hat s \ge s$. The comparison holds only in expectation and only for densities satisfying (9); without (9) bundling is not optimal in general.

Making this rigorous requires several things:

• the a.e. differentiability of the convex function $b$, together with $q_1 = \partial b/\partial y$ a.e.;
• integration by parts on truncated squares $[a, M]^2$ with possibly infinite total revenue;
• control of the boundary term at $y = a$, where $f$ need not be bounded or continuous;
• the extension of $\hat\mu$, defined on $[a,\infty)^2$, to an IC and IR mechanism on all of $\mathbb{R}^2_+$.

Formalization scope

Valuations are functions $\mathrm{Fin}\ 2 \to \mathbb{R}_{\ge 0}$, and random valuations are given by their laws. "Two i.i.d. goods" is the product measure $\nu \otimes \nu$. The law $\nu$ is the image on $\mathbb{R}_{\ge0}$ of $f(x)\,dx$, so no mass is lost because $f = 0$ below $a > 0$. "Density function" means: $f$ measurable, $f \ge 0$, $\int f = 1$, and $f = 0$ on $(-\infty, a)$. Continuity of $F$ is then automatic. Differentiability of $f$ is required at every $x > a$, the range of (9). Nothing is assumed about $f$ at $a$; in particular $f$ may blow up there.

Admissible mechanisms are feasible, IC, IR and have a measurable payment function. The paper allows measurability without loss of generality (footnote 12). Revenue $R(\mu;X)$ is an extended real, so a non-integrable payment never collapses to $0$. $\mathrm{Rev}$ takes values in $[0,\infty]$ and may be infinite under (9), for instance for $f(x) = c\,x^{-3/2}$ on $[a,\infty)$. Milestone 5 states IC and IR of $\hat\mu$ on the quadrant only, as the paper defines $\hat\mu$ there. Off the quadrant, $y + z - a$ is truncated at $0$.

The goal must not be stated as the second equality alone, which is definitional. Nor may it assume the law is bounded or that $f(a)$ is finite: these would replace the theorem with a special case. The display (17) and the limit formula (16) are not posed, because their boundary term $2a f(a)\int b(a,z) f(z)\,dz$ refers to the value of $f$ at $a$, which the hypotheses do not control.

A complete development needs Rochet's characterization, a.e. gradients of convex functions on $\mathbb{R}^2_+$, Fubini–Tonelli on the product law, one-dimensional integration by parts with an absolutely continuous weight, and Myerson's one-good formula for Corollary 17. Contributions of any of these as standalone lemmas are welcome.

Selected references

• S. Hart and N. Nisan, Approximate Revenue Maximization with Multiple Items, J. Econ. Theory 172 (2017); arXiv:1204.1846v3. https://arxiv.org/abs/1204.1846
• R. Myerson, Optimal Auction Design, Math. Oper. Res. 6 (1981) 58–73. https://doi.org/10.1287/moor.6.1.58
• J.-C. Rochet, The taxation principle and multi-time Hamilton–Jacobi equations, J. Math. Econ. 14 (1985) 113–128. https://doi.org/10.1016/0304-4068(85)90015-1
• A. Manelli and D. Vincent, Bundling as an optimal selling mechanism for a multiple-good monopolist, J. Econ. Theory 127 (2006) 1–35. https://doi.org/10.1016/j.jet.2005.08.007
• S. Hart and P. Reny, Maximal revenue with multiple goods: nonmonotonicity and other observations, Theoretical Economics 10 (2015) 893–922. https://doi.org/10.3982/TE1517
• C. Daskalakis, A. Deckelbaum and C. Tzamos, Strong duality for a multiple-good monopolist, Econometrica 85 (2017) 735–767. https://doi.org/10.3982/ECTA12618

Motivation

A seller who offers several goods to a buyer with private values has to choose a selling mechanism. For one good the optimal mechanism is known: post the best take-it-or-leave-it price (Myerson 1981). For two or more goods the optimal mechanism can be complicated: it may use lotteries, its menu may be infinite, and it may not be computable in closed form even for simple value distributions. Sellers therefore use simple mechanisms, such as selling each good separately or selling all goods as one bundle, and the question is how much revenue this costs.

Hart and Nisan (arXiv:1204.1846v3, J. Econ. Theory 2017) answer this with guaranteed fractions of the optimal revenue. Their basic tool is a decomposition theorem: when the goods split into two groups whose values are independent, the optimal revenue from all goods together is bounded by revenues computed from each group separately. This mission formalizes that theorem (Theorem 7) and the paper's first headline result, Theorem A, which is its two-good case.

Setting

There are $k \ge 1$ goods and one buyer with additive values. A valuation is a vector $x \in \mathbb{R}^k_+$, and a $k$-good random valuation $X$ is a random vector in $\mathbb{R}^k_+$ whose law the seller knows.

A mechanism $\mu = (q, s)$ consists of an allocation $q : \mathbb{R}^k_+ \to [0,1]^k$, where $q_i(x)$ is the probability that the buyer receives good $i$ when reporting $x$, and a payment $s : \mathbb{R}^k_+ \to \mathbb{R}$. The buyer's payoff from truthful reporting is $b(x) = q(x)\cdot x - s(x)$. The mechanism is

• incentive compatible (IC) if $b(x) \ge q(\tilde x)\cdot x - s(\tilde x)$ for all $x, \tilde x \in \mathbb{R}^k_+$;
• individually rational (IR) if $b(x) \ge 0$ for all $x$;
• no positive transfer (NPT) if $s(x) \ge 0$ for all $x$.

Let $\mathcal M$ be the class of IC and IR mechanisms. The expected revenue of $\mu \in \mathcal M$ is $R(\mu; X) = \mathbb{E}[s(X)]$, which lies in $(-\infty, +\infty]$, and the optimal revenue is

$$\mathrm{Rev}(X) = \sup_{\mu \in \mathcal M} R(\mu; X) \in [0, \infty].$$

Two benchmarks reduce to one-good problems: the separate revenue $\mathrm{SRev}(X) = \mathrm{Rev}(X_1) + \dots + \mathrm{Rev}(X_k)$ and the bundled revenue $\mathrm{BRev}(X) = \mathrm{Rev}(X_1 + \dots + X_k)$. Finally $\mathrm{Val}(X) = \mathbb{E}[\sum_i X_i]$ is the expected total value.

For the decomposition, $Y$ is a random valuation for $k_1 \ge 1$ goods and $Z$ one for $k_2 \ge 1$ goods. The coordinates of $Y$ may be arbitrarily dependent, and so may those of $Z$, but the vectors $Y$ and $Z$ are independent. $\mathrm{Rev}(Y, Z)$ is the optimal revenue from selling all $k_1 + k_2$ goods together, and $X\mathbf 1_{X \in A}$ is the random valuation equal to $X$ on the event $X \in A$ and to $0$ otherwise.

Formalization targets

Goal: Theorem 7 (p. 18)

If $Y$ and $Z$ are independent, then

$$\mathrm{Rev}(Y, Z) \le \mathrm{Rev}(Y) + \mathrm{Rev}(Z) + \mathrm{BRev}(Y) + \mathrm{BRev}(Z) \le 2\big(\mathrm{Rev}(Y) + \mathrm{Rev}(Z)\big).$$

Both inequalities are part of the goal, with the same middle term.

Milestones, in the order of the paper's proof

1. Proposition 6 (iii), p. 14: $\mathrm{Rev}(X)$ is the supremum of $R(\mu; X)$ over IC, IR and NPT mechanisms.
2. The NPT split, p. 20: $\mathrm{Rev}(Y,Z) \le \mathrm{Rev}\big((Y,Z)\mathbf 1_{\sum_i Y_i \ge \sum_j Z_j}\big) + \mathrm{Rev}\big((Y,Z)\mathbf 1_{\sum_j Z_j \ge \sum_i Y_i}\big)$.
3. Proposition 6 (iv), p. 14: for $\mu \in \mathcal M$ and a set $A$ of values, $\mathbb{E}[s(X)\mathbf 1_{X\in A}] \le \mathrm{Rev}(X\mathbf 1_{X\in A}) \le \mathrm{Rev}(X)$.
4. Lemma 8, p. 19: $\mathrm{Rev}\big((Y,Z)\mathbf 1_{(Y,Z)\in A}\big) \le \mathrm{Rev}(Y) + \mathrm{Val}\big(Z\mathbf 1_{(Y,Z)\in A}\big)$.
5. Lemma 9, p. 20: for one-dimensional independent $Y, Z$, $\mathrm{Val}(Z\mathbf 1_{Y \ge Z}) \le \mathrm{Rev}(Y)$.
6. Lemma 10, p. 20: $\mathrm{Val}\big(Z\mathbf 1_{\sum_i Y_i \ge \sum_j Z_j}\big) \le \mathrm{BRev}(Y)$.
7. BRev ≤ Rev, p. 18.

Companions

Theorem A in the form (2), p. 16: for two independent goods $Y, Z$, $\mathrm{Rev}(Y, Z) \le 2(\mathrm{Rev}(Y) + \mathrm{Rev}(Z))$. Also posed is display (5), p. 17: $z\cdot\mathbb{P}[Y \ge z] \le \mathrm{Rev}(Y)$ for one good and every $z \ge 0$.

Significance

Theorem A says that for two independent goods, selling them separately guarantees half of the optimal revenue, whatever the distributions. Theorem 7 extends this to two independent groups of goods. It is the induction step behind the paper's bounds for many goods: separate selling guarantees a fraction $c/\log^2 k$ of the optimal revenue for $k$ independent goods (Theorem C), and bundling guarantees $c/\log k$ for $k$ i.i.d. goods (Theorem D). These are other missions of this series, and both use Theorem 7 as a black box. The same approach underlies later work on simple versus optimal mechanisms, for example Babaioff, Immorlica, Lucier and Weinberg (FOCS 2014) and Li and Yao (PNAS 2013).

All results posed here are proved in the paper. As far as we know, none has a machine-checked proof. A formal proof would give a reusable development of mechanism design with multi-dimensional types: IC and IR mechanisms on $\mathbb{R}^k_+$, revenue as an extended-real expectation, restriction of mechanisms to subdomains, and marginal mechanisms obtained by fixing some coordinates of an independent product.

Difficulty

The proofs are short on paper but rest on measure theory the prose passes over. Lemma 8 conditions on $Z = z$ and applies Proposition 6 (iv) to a one-group mechanism for each fixed $z$. Formally this is a Tonelli argument on a product measure, with an integrand that may be negative on part of the space and $+\infty$ in expectation. The induced mechanism $s^z(y) = s(y, z) - \sum_j q_j(y,z) z_j$ involves the allocation $q$, which is not assumed measurable. Proposition 6 (iv) bounds a mechanism with possibly negative payments by the optimal revenue on a modified valuation $X\mathbf 1_{X \in A}$, and this requires shifting the mechanism to make it NPT. Finally, every revenue may be infinite, so the inequalities must be handled in $[0,\infty]$ and in the extended reals, without cancelling.

A natural first idea is to apply Theorem A coordinate by coordinate. This fails, because the coordinates inside $Y$ may be dependent. Only the independence of $Y$ from $Z$ is available, and the bound must go through the bundled revenue $\mathrm{BRev}$.

Formalization scope

• Valuations as laws. A random valuation is represented by its law, a probability measure on ι → ℝ≥0 for a finite type ι of goods. Every quantity of the paper depends only on the law. One good is ι = Unit.
• Independence as a product law. The law of $(Y,Z)$ is the product of the laws of $Y$ and $Z$, transported to ι₁ ⊕ ι₂ → ℝ≥0. Theorems that need independence are never stated over an arbitrary joint law with given marginals, since they are false for correlated groups. The NPT split in the proof of Theorem 7 is stated for independent groups, as on the page. Proposition 6 applies to an arbitrary law.
• The class $\mathcal M$. $\mathcal M$ requires $q \in [0,1]^k$, IC, IR and a measurable payment $s$, the last as allowed by the paper's footnote 12. $q$ is not required to be measurable.
• Revenue. $R(\mu;X)$ is $\int s^+ - \int s^-$ in the extended reals, so that $\mathbb{E}[s(X)] = +\infty$ is kept. Since $s \ge s(0)$ under IC, the negative part is finite. The Bochner integral is not used, because it would assign $0$ to a non-integrable payment. $\mathrm{Rev}$, $\mathrm{SRev}$, $\mathrm{BRev}$ and $\mathrm{Val}$ take values in $[0,\infty]$.
• Subdomains. $X\mathbf 1_{X\in A}$ is the image law under $x \mapsto x\mathbf 1_A(x)$, and $A$ is assumed measurable. The regions of the proof of Theorem 7 are both closed, so the diagonal is counted twice, as in the paper.
• Not trivializable. A formalization in which $\mathrm{Rev}$ is computed with a Bochner integral, the expected revenue is clipped before comparing a single mechanism with $\mathrm{Rev}$, or independence is dropped does not state the paper's theorem, and none of these is used.
• Not posed. The ratio form of Theorem A ($\mathrm{GFOR} \ge 1/2$) is not posed, because of its conventions $0/0 = 1$ and $\infty/\infty$. Theorems B, C, D, 16 and 33 are separate missions of this series.

Contributions are welcome at every level: Proposition 6 (the NPT shift and subdomain restriction), the marginal-mechanism construction behind Lemma 8, and the one-good facts (5) and Lemma 9 are all reusable in the sibling missions on Theorems C and D.

Selected references

• S. Hart and N. Nisan, Approximate Revenue Maximization with Multiple Items, Journal of Economic Theory 172 (2017); preprint arXiv:1204.1846v3, 2017. https://arxiv.org/abs/1204.1846
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6 (1981) 58–73. https://doi.org/10.1287/moor.6.1.58
• S. Hart and P. J. Reny, Maximal Revenue with Multiple Goods: Nonmonotonicity and Other Observations, Theoretical Economics 10 (2015) 893–922. https://doi.org/10.3982/TE1517
• M. Babaioff, N. Immorlica, B. Lucier and S. M. Weinberg, A Simple and Approximately Optimal Mechanism for an Additive Buyer, FOCS 2014. https://arxiv.org/abs/1405.6146
• X. Li and A. C.-C. Yao, On Revenue Maximization for Selling Multiple Independently Distributed Items, PNAS 110 (2013) 11232–11237. https://doi.org/10.1073/pnas.1309533110

Why online matching needs a stronger rounding guarantee

In online selection, candidate items reveal themselves one at a time and an algorithm must decide immediately whether to keep each one. When the kept items must form a matching, accepting one edge can prevent a later edge sharing an endpoint from being accepted. A fractional solution supplies useful marginal probabilities, but it does not by itself specify which active edges can be kept under an unfavorable arrival order. Online contention resolution schemes provide that missing rounding step: they turn independent edge activity into a feasible online selection while guaranteeing each edge a chance of selection. Feldman, Svensson, and Zenklusen introduced the strong selectability guarantee used here, which protects an edge even against an arrival order chosen with knowledge of all random outcomes (Feldman–Svensson–Zenklusen, §1.1).

This mission isolates the matching result of their paper. It concerns a degree relaxation that is weaker than the full matching polytope, so the result applies even when the input fractional point satisfies only local vertex constraints. The source states the existence theorem as Theorem 2.7 and gives its numerical guarantee explicitly (Theorem 2.7, p. 13).

Finite graphs, fractional edges, and greedy families

Let $G=(V,E)$ be a finite graph. An edge $g$ has two distinct endpoints; multiple edges may have the same endpoints. A matching is a set of edges with no shared vertex. For a vertex $u$, write $\delta(u)$ for its incident edges. The degree relaxation is

$$P_G=\left\{x\in\mathbb R_{\ge0}^{E}:\sum_{g\in\delta(u)}x_g\le1\text{ for every }u\in V\right\}.$$

Since each edge meets a vertex, these constraints also give $x_g\le1$. Every matching has a characteristic vector in $P_G$. The degree relaxation can contain points outside the convex hull of matchings, which makes the theorem stronger than a statement restricted to the matching polytope (§2.2, p. 13).

For $x\in[0,1]^E$, the active set $R(x)$ includes each edge $g$ independently with probability $x_g$. A greedy family $\mathcal F_x$ is a downward closed family of matchings containing the empty set. A greedy online scheme accepts an active edge if adding it to the already accepted set remains in $\mathcal F_x$. The family may itself be random, sampled independently of $R(x)$.

An edge $g$ is selectable for a realized active set and greedy family when every member $I\in\mathcal F_x$ with $I\subseteq R(x)$ can be extended by $g$ while staying in $\mathcal F_x$. Thus selectability promises acceptance regardless of which eligible active edges preceded $g$. A scheme is $(b,c)$-selectable if this event has probability at least $c$ for every $x\in bP_G$ and every edge. The probability includes both the active-set draw and any random family draw (Definitions 1.3–1.5, pp. 3–4).

Formalization targets

Theorem 2.7: a randomized matching scheme

For every $b\in[0,1]$ and every finite loopless graph $G$,

$$\exists\text{ a randomized greedy scheme for }P_G\text{ that is }(b,e^{-2b})\text{-selectable}.$$

Equivalently, for each $x\in bP_G$ and each edge $g\in E$, the probability that $g$ is selectable is at least $e^{-2b}$. The statement includes edges with $x_g=0$; the selectability event concerns the ability to add an edge, rather than the probability that it becomes active. The milestones are the steps the source states in its proof, in attack order (proof of Theorem 2.7, pp. 13–14):

1. for $t>0$, $0\le(1-e^{-t})/t\le1$, so that an edge can be put into a random set $K$ of potential edges with probability $(1-e^{-x_g})/x_g$;
2. drawing $K$ this way and using the matchings inside $K$ as the family is a randomized greedy scheme;
3. an edge $g'$ with ends $u,v$ is selectable exactly when $g'\in K$ and $A\cap K\cap(\delta(u)\cup\delta(v)\setminus\{g'\})=\varnothing$;
4. the probability of that event equals $\frac{1-e^{-x_{g'}}}{x_{g'}}\,e^{-\sum_{g\in\delta(u)\cup\delta(v)\setminus\{g'\}}x_g}$;
5. for $x\in bP_G$, $\sum_{g\in\delta(u)\cup\delta(v)\setminus\{g'\}}x_g\le2(b-x_{g'})$;
6. for $t>0$, $e^{t}(e^{t}-1)/t\ge1$.

Remark (p. 14): the deterministic variant

Taking $K=E$, the deterministic greedy scheme whose family is the set of all matchings is $(b,(1-b)^2)$-selectable for $P_G$, $b\in[0,1]$:

$$\Pr_{A\sim R(x)}\big[g\text{ is selectable for }A\big]\ \ge\ (1-b)^2\qquad\forall x\in bP_G,\ \forall g\in E.$$

This companion is weaker than Theorem 2.7 for every $b\in(0,1]$ and is not used by it (Remark, p. 14).

What the result contributes

The theorem gives a constant probability bound against the paper's strongest, “almighty” arrival-order adversary. The guarantee is available from vertex degree inequalities alone. Consequently it applies to points of the exact matching polytope as well, without asking the online rounding procedure to exploit its additional odd-set inequalities. The paper places this result beside analogous existence claims for matroids and knapsacks in Theorem 1.8, and uses greedy schemes as components in more general selection results (Theorem 1.8, p. 4).

The existence theorem is proved in the source; it is an open formalization target here. A completed Lean development would supply a reusable finite model of independent active sets, random greedy families, edge selectability, and matching degree relaxations. It would also put the exact $e^{-2b}$ constant and its endpoint cases under machine checking. The definitions can support future formalizations of the paper's combination and application results, although this mission claims only Theorem 2.7 and its local proof milestones.

Where the argument is delicate

The local degree constraints bound the fractional weight at each endpoint separately, while selectability must survive conflicts at either endpoint under any arrival order. Merely ensuring that the algorithm outputs a matching gives no lower bound for a particular edge: the adversary can expose competing active edges first. The theorem therefore asks for a stronger event that certifies an edge could be added after every eligible previously selected matching. The numerical guarantee must hold uniformly over all edges, even when a coordinate is zero (Definitions 1.4–1.5, pp. 3–4; proof of Theorem 2.7, p. 13).

Formalization scope

The ground set is the finite edge type $E$. The published EdmondsMatching65.Polyhedron.Graph structure represents a graph by a map from edges to unordered pairs of vertices and includes a proof excluding self-loops; its matching predicate is reused directly. This admits parallel edges, a harmless generalization of the page's graph language. Incident edge sets and matchings are finite sets. The polytope is the set of real edge vectors satisfying precisely the nonnegativity and vertex degree inequalities above. Scaling is the pointwise set operation $bP_G$, so $b=0$ remains meaningful. The parameter range $0\le b\le1$ is explicit.

Probability is represented by finite sums of product weights. A randomized scheme is a weight function on finite greedy families, independent of the active-set draw. Each family contains the empty set and lies inside the matchings; allowing an empty family would make selectability vacuous. The degree inequalities keep relevant coordinates in $[0,1]$, so active-set weights are genuine probabilities. The source's ratio $(1-e^{-x_g})/x_g$ is given its continuous value $1$ at $x_g=0$. For inputs outside the nonnegative domain, which the theorem never uses, that inclusion probability is also assigned $1$ to keep the distribution well formed. These choices and the loopless graph convention are recorded with the draft statements.

The formalization needs finite product probability identities, elementary exponential inequalities, and set facts about matchings and incident edges. Contributions proving the six listed milestones, the deterministic Remark, or the full existential theorem are welcome. The finite model of active sets, greedy families and selectability is shared with the other missions of this series (matroids, knapsack, combinations of schemes, submodular rounding).

Selected references

• Moran Feldman, Ola Svensson, and Rico Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015, preprint. Published as Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM Journal on Computing, 2021.

Motivation

Many online selection problems ask an algorithm to accept or reject items one at a time, irrevocably, while keeping the accepted set feasible: independent in a matroid, a matching in a graph, or within a knapsack budget. In Bayesian versions, such as prophet inequalities and posted-price mechanisms, a fractional point $x$ of a relaxation of the feasible sets is available in advance, and each item is active independently with probability $x_e$. An online contention resolution scheme (OCRS), introduced by Feldman, Svensson and Zenklusen, turns this random active set into a feasible selection as items arrive.

The quality of an OCRS is measured by its selectability: the probability that every element is accepted when it is active, whatever the arrival order. Applications, however, care about the value of the selected set, often a submodular function such as a coverage or a utility with diminishing returns. Theorem 1.10 of the paper is the bridge between the two: a selectability guarantee $c$ yields an approximation guarantee $c$ for every monotone submodular objective, and $c/4$ for non-monotone ones, even against an adversary who sees every random outcome before fixing the order. The other four missions of this series construct selectable OCRSs for matroids, matchings and knapsacks and combine them; this mission formalizes what such a guarantee is worth.

The offline counterpart is the theory of contention resolution schemes (CRSs) of Chekuri, Vondrák and Zenklusen (SIAM J. Comput. 2014), whose Theorem 1.3 shows that a monotone balanced CRS rounds the multilinear extension of a submodular function with the balancedness factor. The proof of Theorem 1.10 reduces the online statement to that offline result.

Setting

Let $N$ be a finite ground set and $\mathcal F\subseteq 2^N$ a down-closed family of feasible sets. A polytope $P\subseteq[0,1]^N$ is a relaxation of $\mathcal F$ if it contains exactly the characteristic vectors $\mathbf 1_I$ with $I\in\mathcal F$ among the $\{0,1\}$-points. For $x\in[0,1]^N$, the random set $R(x)$ contains every $e$ independently with probability $x_e$.

A greedy OCRS fixes, for each input $x$, a down-closed family $\mathcal F_x\subseteq\mathcal F$ containing $\emptyset$ (deterministically, or drawn from a distribution independent of $R(x)$). The elements then arrive one by one; an arriving active element is selected if, together with the elements already selected, it forms a set in $\mathcal F_x$. An element $e$ is selectable for the active set $A$ if $I\cup\{e\}\in\mathcal F_x$ for every $I\subseteq A$ with $I\in\mathcal F_x$. For $b,c\in[0,1]$ the OCRS is $(b,c)$-selectable if for every $x\in bP$ and every $e\in N$

$$\Pr\big[I\cup\{e\}\in\mathcal F_x\ \ \forall I\subseteq R(x),\ I\in\mathcal F_x\big]\ge c .$$

The arrival order is chosen by the almighty adversary, which knows $R(x)$, the realized family $\mathcal F_x$ and every random bit of the algorithm before choosing it.

For $f:2^N\to\mathbb R$, the multilinear extension is $F(x)=\mathbb E[f(R(x))]$. The function $f$ is submodular if $f(A\cup B)+f(A\cap B)\le f(A)+f(B)$ for all $A,B$, and monotone if $A\subseteq B$ implies $f(A)\le f(B)$. For a set $S$, $S(1/2)$ keeps every element of $S$ independently with probability $1/2$.

An (offline) CRS $\pi$ for $P$ maps each $S\subseteq N$, possibly at random, to a subset $\pi(S)\subseteq S$ with $\mathbf 1_{\pi(S)}\in P$. It is $(b,c)$-balanced if $\Pr[e\in\pi(R(x))\mid e\in R(x)]\ge c$ for $x\in bP$ and $x_e>0$, and monotone if $\Pr[e\in\pi(S_1)]\ge\Pr[e\in\pi(S_2)]$ whenever $e\in S_1\subseteq S_2$. The characteristic CRS of a greedy OCRS is $\bar\pi(A)=\{e\in A : e \text{ selectable for } A\}$.

Formalization targets

Goal: Theorem 1.10

Let $P$ be a relaxation of $\mathcal F$, let $\pi$ be a $(b,c)$-selectable greedy OCRS for $P$, let $x\in bP$, and let $f\ge0$ be submodular. Against every almighty adversary, the selected set $S$ satisfies

$$\mathbb E[f(S)]\ge c\cdot F(x)\quad\text{if } f \text{ is monotone},\qquad \mathbb E[f(S(1/2))]\ge \frac c4\cdot F(x)\quad\text{in general},$$

where in the second case the coins defining $S(1/2)$ are known to the adversary. The constants are the paper's and are not parameters to be improved here.

Milestones

1. Observation 3.3: for every greedy family, active set and order, $\bar\pi(A)$ is contained in the selected set.
2. The remark after Definition 3.2: $\bar\pi$ is a CRS for $P$.
3. Lemma 3.4: the characteristic CRS of a $(b,c)$-selectable greedy OCRS is $(b,c)$-balanced and monotone.
4. Lemma 3.5 (from Chekuri–Vondrák–Zenklusen): for every non-negative submodular $f$ there is a pruning map $\eta_f$, with $\eta_f(S)\subseteq S$, such that $\mathbb E[f(\eta_f(\pi(R(x))))]\ge c\cdot F(x)$ for every monotone $(b,c)$-balanced CRS $\pi$ and every $x\in bP$.
5. Lemma 3.6 (Feige–Mirrokni–Vondrák, Lemma 2.2): if $T_p\subseteq T$ contains every element of $T$ with probability $p$, not necessarily independently, then $\mathbb E[g(T_p)]\ge(1-p)g(\emptyset)+p\,g(T)$ for submodular $g$.
6. Lemma 3.7 (Buchbinder–Feldman–Naor–Schwartz, Lemma 2.2): if $N_p$ contains every element with probability at most $p$, then $\mathbb E[g(N_p)]\ge(1-p)g(\emptyset)$ for non-negative submodular $g$.

Significance

Theorem 1.10 is what makes selectability useful. Combined with the paper's OCRSs for matroids, matchings and knapsacks (Theorem 1.8) and the combination rule (Theorem 1.9), it gives constant-factor online algorithms for submodular objectives under intersections of these constraints, and through them the paper's applications to prophet inequalities, posted-price mechanisms and stochastic probing. The guarantee holds against the strongest adversary considered, so it applies whatever arrival order the application imposes.

The theorem and its proof are published; none of the statements of this mission has a machine-checked proof. Formalizing it produces a reusable interface between online and offline contention resolution, and machine-checked versions of two standard lemmas on correlated random subsets of submodular functions (Lemmas 3.6 and 3.7) used throughout submodular maximization. Lemma 3.5 is the substantial imported ingredient: its formal proof amounts to formalizing the rounding theorem of Chekuri, Vondrák and Zenklusen for non-monotone objectives.

Difficulty

The first idea is to compare the online selection directly with $F(x)$ element by element: each element is selected with probability at least $c\,x_e$. For a linear objective this suffices. For a submodular objective it does not, because the marginal value of an element depends on which other elements are selected, and the adversary controls this through the order. The reduction to the characteristic CRS removes the order, but the offline rounding result (Lemma 3.5) then needs the full CRS machinery, including a pruning step that depends on $f$ alone.

For non-monotone $f$, selecting extra elements can lose value, and the adversary decides which elements beyond $\bar\pi(A)$ are selected, after seeing the coins. Controlling this requires the correlated-sampling bounds of Lemmas 3.6 and 3.7 rather than independence.

Formalization scope

The ground set is a finite type α : Type with decidable equality; sets are Finset α; vectors are α → ℝ. All probabilities and expectations are exact finite sums of product weights, without measure theory. $bP$ is the pointwise scaling b • P, which handles $b=0$. The multilinear extension and submodularity are the published definitions NonmonotoneSubmod.Shared.F and NonmonotoneSubmod.Shared.Submodular.

A randomized greedy OCRS is a weight function on families Finset (Finset α), a CRS a weight function on maps Finset α → Finset α; a deterministic OCRS is a point mass. The almighty adversary is any function from the realized family and active set (and, in part 2, the coin set $C$, with $S(1/2)=S\cap C$ and $C$ uniform and independent of everything else) to an order listing every element once. The standing assumptions of Definition 1.3 are explicit hypotheses: $\mathcal F$ down-closed, $P$ a polytope contained in $[0,1]^N$ and a relaxation of $\mathcal F$, and $b,c\in[0,1]$. A polytope is encoded as the convex hull of finitely many vectors. Every greedy family contains $\emptyset$, so the empty family cannot make every element vacuously selectable, and the inputs $x\in bP$ lie in $[0,1]^N$, so the product weights are probabilities.

Definition 3.1 is printed with "$\ge c\cdot x_e$"; the formalization uses "$\ge c$", as the proof of Lemma 3.4 and Definition 4.5 do. Lemma 3.5 keeps the paper's quantifier order: $\eta_f$ is fixed before $P$, $b$, $c$, $\pi$ and $x$.

Welcome contributions: proofs of the milestones in any order; Lemmas 3.6 and 3.7 are self-contained and reusable; Lemma 3.5 may be split further along the proof of Chekuri–Vondrák–Zenklusen.

Selected references

• M. Feldman, O. Svensson, R. Zenklusen, Online Contention Resolution Schemes, arXiv:1508.00142v2, 2015; Online Contention Resolution Schemes with Applications to Bayesian Selection Problems, SIAM J. Comput. 50(2), 2021. https://arxiv.org/abs/1508.00142v2
• C. Chekuri, J. Vondrák, R. Zenklusen, Submodular Function Maximization via the Multilinear Relaxation and Contention Resolution Schemes, SIAM J. Comput. 43(6), 2014. https://doi.org/10.1137/110839655
• U. Feige, V. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, Submodular Maximization with Cardinality Constraints, SODA 2014. https://doi.org/10.1137/1.9781611973402.106