Probability

Motivation

A seller who owns several goods and faces buyers with private values must decide how to sell them. The revenue-maximizing mechanism is known in closed form only for one good: for a single buyer it is a posted price, and for several buyers it is Myerson's optimal auction (Myerson 1981). With two or more goods the optimal mechanism may use lotteries, may be impossible to describe compactly, and may behave non-monotonically in the value distribution. This makes simple mechanisms with provable revenue guarantees the practical question: how much of the optimal revenue does a seller lose by selling each good separately with its own optimal one-good mechanism?

Hart and Nisan (arXiv:1204.1846v3) answer this for one buyer and two independent goods (their Theorem A): selling separately earns at least half of the optimal revenue. Their Theorem 18 (p. 29), proved in Appendix A.7 as Theorems 33 and 34, extends the factor $\tfrac12$ to any number $n$ of buyers. This mission formalizes the dominant-strategy half, Theorem 33, in which the buyers may be arbitrarily correlated with one another, as long as the two goods are independent.

Setting

One seller sells $k$ goods to $n \ge 1$ buyers. Buyer $j$'s value for good $i$ is a number $x^j_i \ge 0$; a valuation profile is $x = (x^j_i) \in \mathbb R^{kn}_+$, and $x^j = (x^j_i)_i$ is buyer $j$'s valuation vector. The profile is random, $X$, with a commonly known joint law.

A mechanism $\mu = (q^j, s^j)_{j=1,\dots,n}$ gives each buyer $j$ an allocation $q^j(x) \in [0,1]^k$ (the probability that $j$ receives each good) and a payment $s^j(x) \in \mathbb R$, as functions of the reported profile, subject to feasibility: $\sum_j q^j_i(x) \le 1$ for every good $i$. Buyer $j$'s payoff is $b^j(x) = q^j(x)\cdot x^j - s^j(x)$, and the seller's revenue is $S(x) = \sum_j s^j(x)$.

• IC-DS (dominant-strategy incentive compatibility): $b^j(x) \ge q^j(\tilde x^j, x^{-j})\cdot x^j - s^j(\tilde x^j, x^{-j})$ for every buyer $j$, every profile $x$ and every report $\tilde x^j$, where $(\tilde x^j, x^{-j})$ replaces $j$'s vector in $x$ by $\tilde x^j$.
• IR-DS: $b^j(x) \ge 0$ for every $j$ and $x$.
• NPT (no positive transfer): $s^j \ge 0$.

The expected revenue is $R(\mu; X) = \mathbb E[S(X)]$, and

$$\mathrm{Rev}^{DS}(X) = \sup\{R(\mu;X) : \mu \text{ feasible, IC-DS and IR-DS}\} \in [0, \infty].$$

For two goods write $Y = X_1 = (X^j_1)_j$ and $Z = X_2 = (X^j_2)_j$ for the vectors of the buyers' values for good 1 and good 2, so $X = (Y, Z)$. $\mathrm{Rev}^{DS}(Y)$ is the optimal dominant-strategy revenue from good 1 alone, sold to the same $n$ buyers. Finally $a^{(1)} = \max_j a^j$.

Formalization targets

Goal: Theorem 33 (p. 49)

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

$$\mathrm{Rev}^{DS}(X_1) + \mathrm{Rev}^{DS}(X_2) \ge \tfrac12\,\mathrm{Rev}^{DS}(X_1, X_2).$$

No independence among buyers is assumed: the values $X^1_i, \dots, X^n_i$ for the same good may have any joint law.

Milestones (the steps of the paper's proof)

1. Remark (b) of A.7 (p. 48): an IC-DS, IR-DS mechanism is NPT iff $s^j(0, x^{-j}) = 0$ for all $j$, $x^{-j}$, and NPT is without loss of generality for $\mathrm{Rev}^{DS}$.
2. Remark (b), subdomain property (p. 48): $\mathbb E[\sum_j s^j(X)\mathbf 1_{X\in A}] \le \mathrm{Rev}^{DS}(X\mathbf 1_{X\in A}) \le \mathrm{Rev}^{DS}(X)$.
3. Display (21) (p. 50): $z^{(1)}\,\mathbb P[Y^{(1)} \ge z^{(1)}] \le \mathrm{Rev}^{DS}(Y)$.
4. The marginal mechanism (p. 50): for fixed second-good values $z$, $\hat q^j(y) = q^j_1(y,z)$, $\hat s^j(y) = s^j(y,z) - q^j_2(y,z)z^j$ is feasible, IC-DS and IR-DS.
5. Display (19) (p. 49): $\mathbb E[S(Y,Z)\mathbf 1_{Y^{(1)} \ge Z^{(1)}}] \le 2\,\mathrm{Rev}^{DS}(Y)$ for an NPT, IC-DS, IR-DS mechanism.

Companion: Theorem 34 (p. 49)

With $n$ independent buyers and two independent goods, so that all $2n$ values are independent (footnote 27), the same inequality holds for Bayesian Nash implementation: $\mathrm{Rev}^{BN}(X_1) + \mathrm{Rev}^{BN}(X_2) \ge \tfrac12\mathrm{Rev}^{BN}(X_1, X_2)$.

Significance

The result. Theorem 33 shows that the factor-$\tfrac12$ guarantee of separate selling does not depend on there being a single buyer, nor on the buyers being independent, provided incentive compatibility is required in dominant strategies. It reduces a two-good, $n$-buyer design problem, whose optimum is not characterized, to two one-good problems, each of which can be handled by known single-good auction theory. Remark (a) on p. 29 records that the dominant-strategy statement holds for correlated buyers, while Remark (b) there explains, via Crémer and McLean (1988), why the Bayesian Nash analogue cannot be extended to correlated buyers.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. A formal proof requires multi-agent mechanisms on $\mathbb R^{kn}_+$, the Lebesgue integral of a possibly non-integrable revenue, conditioning on an independent coordinate of a product law, and the subdomain property of Remark (b). The definitions here (feasible multi-buyer mechanisms, IC-DS, IR-DS, $\mathrm{Rev}^{DS}$, and the Bayesian Nash counterparts) are reusable for any multi-buyer revenue-maximization result.

Difficulty

The obvious first idea is to apply the one-buyer Theorem A buyer by buyer. It fails: the feasibility constraint $\sum_j q^j_i \le 1$ couples the buyers, so a multi-buyer mechanism does not decompose into single-buyer mechanisms, and the revenue extracted from one buyer depends on the reports of all the others. Any reduction to one-good problems must produce, from a two-good mechanism, one-good mechanisms that remain feasible and dominant-strategy incentive compatible for every buyer at once. On the measure-theoretic side, payments of an incentive compatible mechanism may be negative and non-integrable, so expectations must be handled in the extended reals, and the passage from bounds that hold for each fixed value of one good to a bound in expectation needs the product structure of the law of $(Y, Z)$.

Formalization scope

• A profile is x : Fin n → ι → ℝ≥0 (x j i $= x^j_i$); a random profile is given by its law, a probability measure on that space. One good is ι = Unit, two goods are ι = Fin 2 (good 1 is index 0). The law of two independent goods is twoGoodsN μY μZ, the image of the product law $\mu_Y\otimes\mu_Z$; μY and μZ are arbitrary probability laws on $\mathbb R^n_+$, so correlation among buyers is allowed.
• $(\tilde x^j, x^{-j})$ is Function.update x j x'. Feasibility $\sum_j q^j_i \le 1$ is part of admissibility; without it a mechanism could sell each good to every buyer.
• Payments are required measurable (the paper's footnote 12). $R(\mu;X)$ is the EReal difference of the integrals of $S^+$ and $S^-$, never a Bochner integral, which would vanish on non-integrable revenues. $\mathrm{Rev}^{DS}$ takes values in $[0,\infty]$.
• The subdomain property requires the set $A$ to be measurable, so that the law of $X\mathbf 1_{X\in A}$ is defined. It also requires the signed expectation on $A$ to be defined: at least one of its positive and negative part integrals must be finite. The hypothesis $n \ge 1$ is the paper's.
• For Theorem 34, buyers are independent with laws $\rho_j$; interim payoffs integrate over the others' product law, and allocations as well as payments are required measurable.
• The constant $\tfrac12$ is stated exactly as printed. A statement over an arbitrary joint law with given marginals, or with the feasibility constraint dropped, would be a different (and false, or trivial) theorem.

Contributions of every kind are welcome: proofs of the milestones, of Theorem 34, and general lemmas on multi-buyer mechanisms.

Selected references

• S. Hart and N. Nisan, Approximate Revenue Maximization with Multiple Items, arXiv:1204.1846v3, 2017; J. Economic Theory 172 (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
• J. Crémer and R. P. McLean, Full Extraction of the Surplus in Bayesian and Dominant Strategy Auctions, Econometrica 56 (1988), 1247–1257. https://doi.org/10.2307/1913096
• 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

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

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

In random-feature models, also called extreme learning machines or random neural networks, the inner weights of a one-hidden-layer network are drawn at random and only the linear readout is trained. Training is then a least-squares problem, which is why such models, and their dynamic counterparts reservoir computing and echo state networks, are used in practice. The question is how well such a network can approximate a target when it is not allowed to choose its inner weights. Gonon, Grigoryeva and Ortega (Ann. Appl. Probab. 33 (2023) 28–69) answer it with explicit, non-asymptotic $L^2$ bounds. Their first result, Theorem 1, covers static ReLU networks on an arbitrary separable Hilbert space. The later results of the paper, on finite-dimensional inputs and on echo state networks, are built on it.

Timeline:

• 1993: Barron (IEEE Trans. Inf. Theory 39) proves $O(N^{-1/2})$ approximation rates for functions with a finite first Fourier moment, using networks whose inner weights are optimized.
• 2008: Rahimi and Recht (NeurIPS 2008) prove random kitchen-sink bounds for random features sampled from a fixed law.
• 2023: Gonon, Grigoryeva and Ortega prove bounds with explicit constants for ReLU units with importance-sampled inner weights, on infinite-dimensional input spaces, under weak conditions on the sampling law.

Setting

$\mathcal X$ is a separable real Hilbert space with inner product $\langle\cdot,\cdot\rangle$, and $\sigma(x)=\max(x,0)$ is the rectifier. The inner weights $\theta_i=(A_i,\zeta_i)\in\mathcal X\times\mathbb R$, $i=1,\dots,N$, are i.i.d. with law $\pi$. For a readout matrix $W\in\mathbb M_{m,N}$ the random ReLU network is

$$H_W^{A,\zeta}(z)=W\sigma(Az+\zeta),\qquad (Az+\zeta)_i=\langle A_i,z\rangle+\zeta_i .$$

The target $H^*:\mathcal X\to\mathbb R^m$ is assumed to have a Fourier representation on the ball of radius $M$: $H^*_j(z)=\int e^{i\langle w,z\rangle}\hat\mu_j(dw)$ for $\|z\|\le M$, with complex measures $\hat\mu_j$ whose total variations $|\hat\mu_j|$ have finite second moments (condition (15)). The sampling law has the product form $\pi=\pi_{\mathcal X}\otimes(\pi_{\mathbb R}(x)dx)$. Two further quantities enter: $F_\pi(x)=2\int_{-x}^0\pi_{\mathbb R}(u)^{-1}du$, and the density $g_j=d(|\hat\mu_j|+|\hat\mu_j|^-)/d\pi_{\mathcal X}$, where $\nu^-(\cdot)=\nu(-\cdot)$. The input $Z$ is an $\mathcal X$-valued random variable with law $\mu_Z$ and $\|Z\|\le M$, independent of the inner weights.

Formalization targets

Goal: Theorem 1 (pp. 37–38)

If $|\hat\mu_j|+|\hat\mu_j|^-\ll\pi_{\mathcal X}$, condition (i) or (ii) on $\pi_{\mathbb R}$ holds, and the integrals (16) of $F_\pi(M\|w\|)\|w\|^2g_j^2$ and $\max(\|w\|^2,1)g_j^2$ are finite, then there is a readout $W$, a measurable function of $(A,\zeta)$, with

$$\mathbb E\big[\|H_W^{A,\zeta}(Z)-H^*(Z)\|^2\big]\le\frac{C^*}{N},$$

and for every $\delta\in(0,1)$, with probability at least $1-\delta$, $\|H_W^{A,\zeta}-H^*\|_{L^2(\mu_Z)}\le\sqrt{C^*}/(\delta\sqrt N)$. Here $C^*=\sum_jC^*_j$ and

$$C^*_j=M^2\!\int F_\pi(M\|w\|)\|w\|^2g_j^2\,d\pi_{\mathcal X}+32\max(M^2,1)\big(F_\pi(1)-F_\pi(-1)\big)\!\int\max(\|w\|^2,1)g_j^2\,d\pi_{\mathcal X}.$$

Milestones

1. Lemma 1 (p. 37): $(\omega,z)\mapsto H_{W(\omega)}^{A(\omega),\zeta(\omega)}(z)$ is product-measurable.
2. Step 1 (p. 39): $\int i\langle v,w\rangle\hat\mu(dw)$ is real, and the identity (19).
3. (20) (p. 40): $H^*(v)=\int\sigma(\langle v,w\rangle+u)\,\alpha(dw,du)$ for $\|v\|\le M$, for an explicit signed measure $\alpha$.
4. (21) (p. 40): $\alpha\ll\pi$, with $|d\alpha/d\pi(w,u)|\le(\mathbb 1_{(-M\|w\|,0]}(u)+2\sqrt2\,\mathbb 1_{[-1,1]}(u))\,g(w)/\pi_{\mathbb R}(u)$.
5. (25) (p. 40): the mean-square error of the i.i.d. average is $\frac1N\operatorname{Var}$, which is at most $\frac1N$ times the second moment.
6. (26) (p. 41): that second moment is at most $C^*$.

Milestones 2–6 are stated for a single output component ($m=1$), to which the proof reduces.

Significance

Theorem 1 says that only the readout has to be trained. With inner weights drawn from an essentially arbitrary product law satisfying (i) or (ii), a least-squares readout achieves $L^2$ error $O(N^{-1/2})$ with a constant computable from the Fourier data of $H^*$ and the sampling law (Remark 3, p. 38). The finite-dimensional rates of Section 4.2 (Proposition 3, Corollary 1) follow from it, and so do, through the reservoir functional's Fourier representation, the echo state network bounds of Sections 5–6.

The result is proved on paper but has no machine-checked proof. A formal proof needs integral representations of Fourier-type functions by ReLU units, Radon–Nikodym arguments for signed measures on product spaces, and the variance identity for i.i.d. averages. A side product of formalizing it is a correction: the printed constant $32M^2$ is false for small $M$ and has to be replaced by $32\max(M^2,1)$, which agrees with it for $M\ge1$.

Difficulty

There is an obvious argument: sample features from $|\hat\mu|$ and use Maurey's empirical method. It does not apply, because the features here are ReLU ridge functions of a real-valued bias drawn from $\pi_{\mathbb R}$, not complex exponentials. The proof must first rewrite the oscillatory representation as an integral of rectifiers, (18)–(20). That step uses the realness of $\int i\langle v,w\rangle\hat\mu(dw)$, which is not given and follows only from $H^*$ being real near $0$. The signed measure $\alpha$ obtained this way must then be absolutely continuous with respect to the sampling law $\pi$, with a density whose second moment is controlled by (16). In case (ii), $\pi_{\mathbb R}$ may vanish outside a bounded interval, and the support of $\alpha$ has to be matched to it.

Formalization scope

• Space. $\mathcal X$ is a complete, separable real inner product space with its Borel $\sigma$-algebra.
• Complex measures. Each $\hat\mu_j$ is given in polar form $h_j\,\nu_j$, with $\nu_j=|\hat\mu_j|$ a finite measure and $h_j$ measurable with $|h_j|=1$. This loses no generality (Rudin, Thm 6.12).
• Randomness. The inner weights live on $(\mathcal X\times\mathbb R)^N$ with law $\pi^{\otimes N}$, and $Z$ has its own law $\mu_Z$. Expectations are iterated lower integrals; this is the standing independence of §4.1. "With probability $1-\delta$" bounds the $\pi^{\otimes N}$-measure of the bad set.
• Readout. The readout is a measurable function of the inner weights only. A readout allowed to depend on the input $Z$ would make the statement trivial, and it is ruled out.
• Norms and normalisation. Norms on $\mathbb R^m$ are Euclidean, as a sum of squares. $\pi_{\mathcal X}$ is a probability measure and $\int\pi_{\mathbb R}=1$; rescaling $\pi_{\mathcal X}$ by $c$ and $\pi_{\mathbb R}$ by $1/c$ changes neither $\pi$ nor $C^*$.
• Encodings. "$|F_\pi(x)|<\infty$" is integrability of $1/\pi_{\mathbb R}$ on the interval between $-x$ and $0$, and $F_\pi$ is an oriented interval integral. (15) is a finite lower integral and (16) is integrability, so none of them holds vacuously.
• Departures from the print. The page's "$C^*>0$" is dropped in favour of the explicit value. The constant uses $32\max(M^2,1)$.

A complete development needs the following:

• the rectifier integral identity (18), which is identity (8) of Proposition 2 and is posed in the companion mission on echo state networks;
• the Radon–Nikodym and Fubini arguments of Step 1;
• the variance of i.i.d. averages under product measures;
• Markov's inequality.

The variance identity (25) and the bound (26) are independent of the Fourier setting and reusable. Contributions to any milestone are welcome, and so are alternative proofs of (19) and (20).

Selected references

• L. Gonon, L. Grigoryeva, J.-P. Ortega, Approximation bounds for random neural networks and reservoir systems, Ann. Appl. Probab. 33(1), 2023, 28–69. https://doi.org/10.1214/22-AAP1806
• A. R. Barron, Universal approximation bounds for superpositions of a sigmoidal function, IEEE Trans. Inf. Theory 39(3), 1993, 930–945. https://doi.org/10.1109/18.256500
• A. Rahimi, B. Recht, Weighted sums of random kitchen sinks: replacing minimization with randomization in learning, NeurIPS 2008. https://papers.nips.cc/paper/2008/hash/0efe32849d230d7f53049ddc4a4b0c60-Abstract.html
• W. Rudin, Real and Complex Analysis, 3rd ed., McGraw-Hill, 1987 (Chapter 6, Theorem 6.12).

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