Mechanism Design

Motivation

A seller who must auction one item without knowing how buyers value it needs a mechanism that performs acceptably against every plausible value distribution. Anunrojwong, Balseiro and Besbes (arXiv:2204.10478, Operations Research 2025) measure performance by regret: the expected revenue lost relative to a seller who knows the realized valuations and extracts the highest one. Their main result (Theorem 1, the subject of mission I of this series) shows that against independent and identically distributed valuations the minimax-regret mechanism is a second-price auction whose reserve price is random, drawn from an explicit distribution.

Practitioners rarely randomize reserves. The natural benchmark is the familiar second-price auction with a fixed deterministic reserve $r$, and the question this mission addresses is how much is lost by insisting on a deterministic reserve: what is the worst-case regret of that auction, and which reserve minimizes it? The paper answers this exactly in Proposition 5 (§5.2.1, p. 24, proof in Appendix D, pp. App-10–11). For a single buyer, regret-optimal posted pricing was studied by Bergemann and Schlag (2008), where a deterministic price $1/2$ has worst-case regret $1/2$; Proposition 5 is the $n$-buyer version of that benchmark.

Setting

There are $n\ge1$ buyers with valuations $v=(v_1,\dots,v_n)$ in the type cube $[0,1]^n$, drawn from a joint distribution $\mathbf F$ unknown to the seller. Write $v^{(1)}=\max_i v_i$ and $v^{(2)}$ for the second-highest valuation. A direct mechanism charges buyer $i$ a payment $p_i(v)$, and its regret under $\mathbf F$ is

$$R_n(m,\mathbf F)=\mathbb E_{v\sim\mathbf F}\Big[v^{(1)}-\sum_{i=1}^n p_i(v)\Big].$$

The second-price auction with reserve $r$, $\mathrm{SPA}(r)$, gives the item to the highest bidder if the highest bid is at least $r$, at price $\max(v^{(2)},r)$, and otherwise does not sell. Its revenue is $\max(v^{(2)},r)\,\mathbf 1(v^{(1)}\ge r)$.

Three classes of distributions on $[0,1]^n$ are considered:

• $\mathcal F_{\mathrm{iid}}$: product laws $G^{\otimes n}$, with $G$ a law on $[0,1]$;
• $\mathcal F_{\mathrm{aff}}$: exchangeable laws (invariant under permuting buyers) that are affiliated, meaning $\Pr(A\cap B\mid S)\ge\Pr(A\mid S)\Pr(B\mid S)$ for all increasing sets $A,B$ and every sublattice $S$ (a set closed under coordinatewise minimum and maximum);
• $\mathcal F_{\mathrm{mix}}$: mixtures of i.i.d. laws, whose joint CDF is $\mathbf F(v)=\int\prod_i G(v_i)\,d\mu(G)$ for a probability measure $\mu$ on distributions.

The worst-case regret of $\mathrm{SPA}(r)$ over a class $\mathcal F$ is $\sup_{\mathbf F\in\mathcal F}R_n(\mathrm{SPA}(r),\mathbf F)$. The closed form found by the paper is

$$W_n(r)=\begin{cases}\max(1-r,\,r), & n=1,\\[2pt] \dfrac{(1-r)^n(n-1)^{n-1}}{((1-r)n-r)^{n-1}}, & n\ge 2,\ r\le\tfrac12,\\[4pt] r, & n\ge2,\ r>\tfrac12,\end{cases}$$

called wcFixed n r in the Lean development.

Formalization targets

Goal: Proposition 5

For every $n\ge1$, every class $\mathcal F\in\{\mathcal F_{\mathrm{iid}},\mathcal F_{\mathrm{aff}},\mathcal F_{\mathrm{mix}}\}$ and every $r\in[0,1]$,

$$\sup_{\mathbf F\in\mathcal F}R_n(\mathrm{SPA}(r),\mathbf F)=W_n(r),$$

the no-reserve auction has $W_n(0)=1$ for $n=1$ and $\big(\frac{n-1}{n}\big)^{n-1}$ for $n\ge2$, and

$$\min_{r\in[0,1]}W_n(r)=W_n\Big(\frac1{n+1}\Big)=\Big(\frac n{n+1}\Big)^n,$$

with $r^*=1/(n+1)$ the unique minimizer.

Milestones

1. The regret of $\mathrm{SPA}(r)$ under an i.i.d. law with marginal CDF $F$: $rF_-(r)^n-\int_0^rF^n+\int_r^1(nF^{n-1}-nF^n)$.
2. For $n\ge2$, the maximum of $rc^n+(1-r)(nc^{n-1}-nc^n)$ over $c\in[\frac{n-1}{n},1]$ equals $W_n(r)$.
3. For $n=1$, the maximum of $rc+(1-r)(1-c)$ over $c\in[0,1]$ is $\max(1-r,r)$.
4. $W_n$ is minimized on $[0,1]$ exactly at $1/(n+1)$, with value $(n/(n+1))^n$.
5. For $n\ge2$, every exchangeable affiliated law gives $\mathrm{SPA}(r)$ regret at most $W_n(r)$.

Significance

The result. Proposition 5 gives the exact price of determinism. The optimal fixed reserve $1/(n+1)$ has worst-case regret $(n/(n+1))^n$: $1/2$ for one buyer, $4/9$ for two. The minimax regret of the optimal randomized auction is about $0.368$ and $0.324$ for the same cases, so the benchmark shows how much of the paper's improvement comes from randomizing the reserve. Both values converge to $1/e$ as $n\to\infty$. Proposition 5 also shows that the worst case does not change when valuations are positively dependent (affiliated, or mixtures of i.i.d.), the same robustness the paper establishes for its optimal mechanism.

Formalizing it. The result is proved on paper in the paper's Appendix D, and no machine-checked version is known. A formal proof needs an expression of the expected revenue of a second-price auction through the order-statistic CDFs, a careful treatment of atoms at the reserve, two elementary but fiddly one-variable optimizations, and, for $\mathcal F_{\mathrm{aff}}$ and $\mathcal F_{\mathrm{mix}}$, the reduction to the i.i.d. case.

Difficulty

The supremum over $\mathcal F_{\mathrm{iid}}$ is not attained. The auction's revenue jumps at the reserve: a buyer valued exactly at $r$ buys, while one valued just below does not. Nature exploits this with two-point laws placing mass just below $r$ and the rest at $1$, and the regret approaches $W_n(r)$ only in the limit. So the first idea, exhibiting a maximizing distribution, fails, and any formalization must treat the worst case as a least upper bound. The upper bound over $\mathcal F_{\mathrm{aff}}$ is the real difficulty: it rests on an order-statistic identity and on an inequality between the CDFs of the maxima of $n-1$ and $n$ affiliated valuations, which in turn needs properties of affiliation that are quoted from Milgrom and Weber (1982) rather than proved in the paper. For $\mathcal F_{\mathrm{mix}}$ the bound needs the regret to be linear in the mixing measure, i.e. a disintegration of the mixture law through its joint CDF.

Formalization scope

• Representation. Buyers are Fin n; valuations are vectors Fin n → ℝ; a distribution is a probability measure on Fin n → ℝ whose complement of the cube $[0,1]^n$ is null. $\mathcal F_{\mathrm{iid}}$ is the set of products Measure.pi (fun _ => G) of a probability law G on $[0,1]$. $\mathcal F_{\mathrm{mix}}$ uses a probability measure on Measure ℝ with the Giry σ-algebra and states the CDF identity of Definition 6 for every $v$.
• The auction. $\mathrm{SPA}(r)$ is the random-reserve auction SPA ρ at ρ = Measure.dirac r; the winner pays $\max(v^{(2)},r)$ when its bid is at least $r$. Ties go to the lowest index (the paper breaks them arbitrarily; revenue does not depend on the rule).
• Affiliation is stated cross-multiplied, $\mu(A\cap S)\mu(B\cap S)\le\mu(A\cap B\cap S)\mu(S)$, for measurable increasing $A,B$ and measurable sublattices $S$.
• Conventions committed to. The reserve ranges over $[0,1]$ (the page leaves this implicit; for $r>1$ the closed form is false). Worst-case regret is IsLUB of the set of regrets, not a maximum and not sSup. "The optimal reserve" is IsLeast of $W_n$ on $[0,1]$, its value at $1/(n+1)$, and uniqueness of the minimizer.
• Ruled out. A statement with IsGreatest would be false (the supremum is not attained); sSup of the regret image would be a junk value if the image were unbounded; classes without the $[0,1]^n$ support condition, or $r$ unconstrained, change the theorem.
• Infrastructure. Expected revenue of a second-price auction via order statistics, the CDF of the maximum and second maximum of i.i.d. variables, and the reduction of mixtures to their components are reusable for the rest of this series and for auction theory generally. Contributions to the affiliation inequalities (Milgrom–Weber) are particularly welcome.

Selected references

• J. Anunrojwong, S. R. Balseiro, O. Besbes, On the Robustness of Second-Price Auctions in Prior-Independent Mechanism Design, arXiv:2204.10478v5, 2024; Operations Research, 2025. https://arxiv.org/abs/2204.10478
• D. Bergemann, K. Schlag, Pricing without Priors, Journal of the European Economic Association 6(2–3), 560–569, 2008. https://doi.org/10.1162/JEEA.2008.6.2-3.560
• P. R. Milgrom, R. J. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1089–1122, 1982. https://doi.org/10.2307/1911865

Motivation

Data brokers sell two kinds of products to marketers. A marketing list supplies the contacts a marketer needs in order to act at all; a data append enriches a list the marketer already holds. In both cases the broker can also choose how informative its accompanying analytics are, and it can price a menu of plans of different informativeness to marketers whose costs of acting it cannot observe. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) studies how such a seller should design this menu, and in particular when it should sell more or less information than would be efficient.

The paper first works with a two-point value distribution (Sections 2–3) and then, in Section 4, with a general information structure in which informativeness is ordered by the rotation order of the distribution of the posterior mean (Johnson and Myatt 2006). This mission formalizes the marketing-list result of Section 4.1: Proposition 4 (comparative statics of the efficient informativeness) and Proposition 5 (the optimal screening menu). It is the third mission of a four-mission series on the paper; the first two treat the two-point model, the fourth treats data appends under the rotation order.

Setting

A marketer's value $u$ from targeting a consumer is unknown. The seller supplies a signal of informativeness $\alpha\in[\underline\alpha,\bar\alpha]\subset(0,1)$. The marketer's posterior mean $v=E[u\mid w]$ has cumulative distribution function $H(v,\alpha)$ on a support $[\underline v,\bar v]$, with a strictly positive density $h(v,\alpha)$. Bayesian updating keeps the mean fixed: $\int_{\underline v}^{\bar v} v\,h(v,\alpha)\,dv=\hat u$ for every $\alpha$, where $\hat u$ is the prior mean. The rotation order (9) requires a point $v^+\in(\underline v,\bar v)$ such that

$$\frac{\partial H(v,\alpha)}{\partial\alpha}>0\ \text{for } v<v^+,\qquad \frac{\partial H(v,\alpha)}{\partial\alpha}<0\ \text{for } v>v^+ .$$

Raising $\alpha$ moves probability mass from the middle of the distribution to its tails.

The seller incurs a selling cost $k(\alpha)$, increasing, with $k(\underline\alpha)=0$. A marketer's targeting cost is $c_H$ with probability $\theta\in(0,1)$ and $c_L$ with probability $1-\theta$, with $c_H>c_L>0$. A marketer with cost $c$ targets exactly when $v>c$, so informativeness $\alpha$ is worth

$$P(\alpha,c)=\int_c^{\bar v}(v-c)\,dH(v,\alpha).$$

With observable costs (the benchmark), the seller sells to type $i$ the informativeness maximizing (12), $\Pi_i=\theta_i\,[P(\alpha,c_i)-k(\alpha)]$; a maximizer is an efficient level $\alpha^e_i$. With private costs, the seller offers a menu of plans $(T_H,\alpha_H)$, $(T_L,\alpha_L)$, with fees $T_j\ge0$. A type-$i$ marketer choosing plan $j$ gets $U_{ij}=-T_j+P(\alpha_j,c_i)$ (13). The seller maximizes $\Pi=\theta[T_H-k(\alpha_H)]+(1-\theta)[T_L-k(\alpha_L)]$ subject to individual rationality $U_{ii}\ge0$ and incentive compatibility $U_{ii}\ge U_{ii'}$ (problem (6)). Its solutions are written $\alpha^*_H,\alpha^*_L$.

Formalization targets

Goal: Proposition 5

In general $\alpha^*_L=\alpha^e_L$, and if $c_L<c_H<v^+$ (resp. $v^+<c_L<c_H$), then

$$\alpha^*_H>\alpha^e_H\quad(\text{resp. } \alpha^*_H<\alpha^e_H).$$

The first identity says that the low-cost marketer, the "high type" of the screening problem, receives the efficient informativeness. The second says that the high-cost marketer's informativeness is distorted, upward when both costs lie below the rotation point and downward when both lie above it. Both are stated for every optimal menu and every efficient level.

Milestones

1. Integration by parts: $P(\alpha,c)=\int_c^{\bar v}[1-H(v,\alpha)]\,dv$ (proof of Proposition 4).
2. The cross derivative $\partial^2\Pi_i/\partial\alpha_i\partial c_i=\theta_i\,\partial H(c_i,\alpha_i)/\partial\alpha_i$ and its sign on either side of $v^+$.
3. Proposition 4: $\alpha^e_i$ first increases and then decreases with $c_i$, with the turning point at $v^+$.
4. The reduction of (6) to the two-variable problem (14) by the binding constraints $IR_H$ and $IC_{L,H}$.
5. (14) integrated by parts, with the high type's rent $R(\alpha_H)=\int_{c_L}^{c_H}[1-H(v,\alpha_H)]\,dv$, and its separation, which gives $\alpha^*_L=\alpha^e_L$ for (14).
6. The derivative $\partial\Pi/\partial\alpha_H$ of (14) compared with the benchmark derivative.

Significance

Proposition 4 states that the value of information to a marketer is non-monotone in the cost of acting: it is largest for costs near the rotation point $v^+$, where the targeting decision is hardest. Proposition 5 turns this into a pricing rule. In the two-point model the direction of the distortion depends only on the prior (Proposition 2, $\varphi<1/2$ or $\varphi>1/2$). Under the rotation order it depends on where the costs lie relative to $v^+$, so a seller facing marketers with low costs over-supplies information to its less profitable segment, and one facing high costs under-supplies it. The comparison with the two-point model (pp. 17–18 of the manuscript) connects the two settings through the single-crossing point of the posterior-mean distributions.

The results are proved in the paper, through integration by parts, signs of derivatives and Topkis's monotonicity theorem. None of them is formalized. Formalizing them checks the reduction of the screening problem, which the paper performs by analogy with the two-point model, including the constraints it drops without comment. It also produces a reusable treatment of rotation-ordered distribution families on an interval. Topkis's Theorem 2.8.4 is already proved on the platform and is part of this mission as a reference.

Difficulty

The obvious argument has two gaps. The first is the reduction (14). The paper substitutes the binding $IR_H$ and $IC_{L,H}$ constraints and drops $IR_L$, $IC_{H,L}$ and $T_j\ge0$. That the dropped constraints hold at a solution of (14) is not shown in the paper. The second gap is strictness: Topkis's theorem compares maximizers weakly. The strict inequalities $\alpha^*_H\gtrless\alpha^e_H$ require showing that efficient levels are interior and that the first-order conditions differ there. This uses the footnote-5 behaviour of $k$ at the endpoints and the mean-preserving property (10), which follows from (9) and the constancy of the mean.

Formalization scope

The model is one Lean structure, SellingData.ListsRotation.Model, with real parameters and its standing assumptions as fields. The committed conventions are:

• The support $[\underline v,\bar v]$ is a bounded real interval; the paper allows an unbounded one.
• $H(\cdot,\alpha)$ is continuous on the support, with $H(\underline v,\alpha)=0$, $H(\bar v,\alpha)=1$ and a strictly positive continuous density $h(\cdot,\alpha)$. The derivative $\partial H/\partial\alpha$ exists on the support, for $\alpha\in(0,1)$.
• $dH(v,\alpha)$ is $h(v,\alpha)\,dv$, so $P(\alpha,c)=\int_c^{\bar v}(v-c)\,h(v,\alpha)\,dv$.
• The rotation order (9) is imposed on the open support. The mean property is a field of the model; (10) is not assumed, since it follows.
• The costs satisfy $\underline v<c_L<c_H<\bar v$.
• $k$ is monotone on $[\underline\alpha,\bar\alpha]$ with $k(\underline\alpha)=0$.

Two further hypotheses are pinned, and only on the statements that need strictness or differentiation under the integral sign:

• the footnote-5 conditions on $k$: continuity on $[\underline\alpha,\bar\alpha]$, differentiability inside, $k'(\underline\alpha)=0$ from the right and $k'(\alpha)\to+\infty$ as $\alpha\to\bar\alpha^-$; convexity and twice differentiability are not assumed;
• joint continuity of $\partial H/\partial\alpha$ on $[\underline v,\bar v]\times(0,1)$.

Optimal menus and efficient levels are sets of maximizers, not chosen maximizers, because $k$ need not be convex. "$\alpha^*_L=\alpha^e_L$" is the equality of the set of low-cost plans of optimal menus with the set of efficient levels. The goal is stated for the screening problem (6) itself, with all four constraints and nonnegative fees. Defining the optimal menu through (14), or efficient levels through a first-order condition, would make half of the goal a restatement of a milestone, and is ruled out. As on the page, $\alpha^*_L=\alpha^e_L$ is stated with no condition on the position of the costs relative to $v^+$; only the comparison of $\alpha^*_H$ with $\alpha^e_H$ carries the two cost ranges. A sorry-free instance shows that the model's hypotheses are jointly satisfiable: $[\underline v,\bar v]=[0,1]$, $H(v,\alpha)=v+\tfrac{\alpha}{2}v(1-v)(1-2v)$, $v^+=\hat u=1/2$.

Contributions are welcome on the integration-by-parts and differentiation-under-the-integral lemmas for families of distributions on an interval, which are reusable beyond this paper, and on any milestone in any order.

Selected references

• Liang Guo, Selling Data to Marketers, Management Science, 2025, author's manuscript. https://doi.org/10.1287/mnsc.2023.01350
• Justin P. Johnson and David P. Myatt, On the Simple Economics of Advertising, Marketing, and Product Design, American Economic Review 96(3), 2006. https://doi.org/10.1257/aer.96.3.756
• Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998 (Theorem 2.8.4). https://doi.org/10.1515/9781400822539

Motivation

Data brokers sell information about consumers to firms that decide whom to target: a lender deciding whom to offer credit, a retailer deciding whom to mail. Two products dominate this market. A marketing list sells contact information together with an analysis, so that a firm cannot reach the consumer at all without buying. A data append adds information about consumers the firm already knows, so that the firm can act even without buying. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) studies how a monopoly data seller should design a menu of data products when the buyers' targeting costs are private, and shows that the answer differs sharply between the two products.

This mission formalizes the data-append result in the paper's base model with a binary targeting value: Proposition 3 (p. 13 of the author's manuscript). The companion missions of the series cover marketing lists and the general model with a rotation-ordered family of posterior distributions.

Setting

A marketer can take an action at cost $c>0$. The action yields a value $u\in\{\underline u,\bar u\}$, with $u=\bar u$ with prior probability $\varphi\in(0,1)$, so the prior mean is $\hat u=\varphi\bar u+(1-\varphi)\underline u$. Not acting yields $0$.

The seller can produce a signal $w\in\{w_h,w_l\}$ with $\Pr(w_h\mid\bar u)=\Pr(w_l\mid\underline u)=\alpha$, where the informativeness $\alpha$ is chosen from $[\underline\alpha,\bar\alpha]\subset(1/2,1)$. The signal probabilities are $\sigma_h(\alpha)=\varphi\alpha+(1-\varphi)(1-\alpha)$ and $\sigma_l(\alpha)=1-\sigma_h(\alpha)$, and the posterior means after $w_h$ and $w_l$ are $v_h(\alpha)$ and $v_l(\alpha)$, computed by Bayes' rule. The standing assumption $v_l(\underline\alpha)<c<v_h(\underline\alpha)$ makes acting worthwhile exactly after the high signal, so a marketer of cost $c$ values information $\alpha$ at $\sigma_h(\alpha)[v_h(\alpha)-c]$. Serving a marketer with informativeness $\alpha$ costs the seller $k(\alpha)$, with $k(\underline\alpha)=0$ and $k$ increasing.

Marketers have cost $c_H$ with probability $\theta$ and $c_L<c_H$ with probability $1-\theta$, privately known. The seller offers a menu of two plans $(T_H,\alpha_H)$ and $(T_L,\alpha_L)$ with fees $T_j\ge0$. Type $i$'s payoff from plan $j$ is

$$U_{ij}=-T_j+\sigma_h(\alpha_j)[v_h(\alpha_j)-c_i].$$

With data appends, a marketer who buys nothing can still act on the prior, so its outside option is $U_{i0}=\max\{\hat u-c_i,0\}$. The seller maximizes $\Pi=\sum_i\theta_i[T_i-k(\alpha_i)]$ subject to $U_{ii}\ge U_{i0}$ ($IR_i$) and $U_{ii}\ge U_{ii'}$ ($IC_{i,i'}$). An optimal menu solves this problem; its informativeness levels are $\alpha_H^*,\alpha_L^*$.

The benchmark is the seller's problem when costs are observable: for each type it maximizes $\Pi_i=\theta_i[\sigma_h(\alpha)[v_h(\alpha)-c_i]-k(\alpha)]$ over $[\underline\alpha,\bar\alpha]$. Any maximizer is an efficient informativeness $\alpha_i^e$.

Formalization targets

Goal: Proposition 3 (p. 13)

When $c_L<c_H<\hat u$:

$$\{\alpha_H^*\}=\{\alpha_H^e\},\qquad \varphi<\tfrac12\ \Rightarrow\ \alpha_L^*<\alpha_L^e,\qquad \varphi>\tfrac12\ \Rightarrow\ \alpha_L^*>\alpha_L^e .$$

The first claim is an equality of sets: the high-cost informativeness levels of optimal menus are exactly the efficient ones at $c_H$. The inequalities hold for every optimal menu and every efficient $\alpha_L^e$.

Milestones

1. Willingness to pay (§3.2, p. 13): for $c_L<c_H<\hat u$, $U_{ij}-U_{i0}=-T_j+\sigma_l(\alpha_j)[c_i-v_l(\alpha_j)]$, which is increasing in $c_i$.
2. Reduction (8) (p. 13): with $IR_L$ and $IC_{H,L}$ binding, the problem becomes the maximization over $(\alpha_H,\alpha_L)$ of

$$\theta\big[\sigma_h(\alpha_H)[v_h(\alpha_H)-c_H]-\sigma_h(\alpha_L)(c_L-c_H)-k(\alpha_H)\big]+(1-\theta)\big[\sigma_h(\alpha_L)[v_h(\alpha_L)-c_L]-k(\alpha_L)\big]-\hat u+c_L .$$

3. The $\alpha_L$-derivatives (proof of Proposition 3, p. 32): the benchmark derivative $(1-\theta)[\varphi(\bar u-c_L)-(1-\varphi)(\underline u-c_L)-k'(\alpha_L)]$ and the derivative of (8), which adds $\theta(1-2\varphi)(c_L-c_H)$.

Significance

The result says that a data seller's distortion depends on the product's form. With marketing lists the low-cost marketers are the high type, their plan is efficient, and the high-cost plan is distorted (Proposition 2, p. 11). With data appends and costs below the prior mean, the outside option $\hat u-c_i$ falls with $c_i$ faster than the value of information does, so high-cost marketers have the larger willingness to pay. The roles of the types switch, the low-cost plan is distorted, and the direction of the distortion is reversed, giving the paper's "double mirror image" (p. 13). The direction is set by the skewness of the prior through the sign of $1-2\varphi$, not by an assumed single-crossing condition.

The result is proved in the paper, in an appendix argument of a few lines that invokes Topkis's monotonicity theorem. To our knowledge it has no machine-checked proof. Formalizing it makes explicit what the printed proof leaves to the reader: that the constraints dropped in (8) hold at its optimum, that the efficient and optimal informativeness need not be unique, and which regularity of $k$ the strict inequalities need.

Difficulty

The obvious argument substitutes the binding constraints, compares first-order conditions, and invokes Topkis's theorem. Three steps of it are not automatic. First, the reduction drops $IR_H$, $IC_{L,H}$ and the nonnegativity of fees; these must be shown to hold at every maximizer of (8), and $IC_{L,H}$ holds only because the maximizers of (8) are ordered in the right direction, which is itself a comparative-statics fact. Second, the reduction identifies the optimal menus only if (8) attains its maximum. Third, Topkis's theorem yields only weak inequalities, $\alpha_L^*\le\alpha_L^e$; strictness needs the efficient informativeness to be interior and $k$ to be differentiable there, which footnote 5 (p. 7) supplies. Without it, both optima can sit at the same corner $\underline\alpha$ or $\bar\alpha$.

Formalization scope

Everything is stated over $\mathbb R$ in the sub-namespace SellingData.AppendsBinary. The two types form an inductive type CostType with constructors H and L. A Model structure holds $\underline u<\bar u$, $\varphi\in(0,1)$, $1/2<\underline\alpha<\bar\alpha<1$, $\theta\in(0,1)$, $0<c_L<c_H$, $k(\underline\alpha)=0$, $k$ weakly increasing on $[\underline\alpha,\bar\alpha]$, and the standing assumption $v_l(\underline\alpha)<c_i<v_h(\underline\alpha)$ for both costs. The posteriors are defined with the divisions of the paper's (2). The outside option is the printed $\max\{\hat u-c_i,0\}$.

Optimality and efficiency are predicates on maximizers, never a chosen maximizer. The optimal menu is defined from the data-append screening problem itself; defining it through (8) would make the first claim of the goal trivial and is ruled out. The goal additionally assumes the part of footnote 5 that the strict inequalities need: $k$ continuous on $[\underline\alpha,\bar\alpha]$, differentiable on $(\underline\alpha,\bar\alpha)$, right derivative $0$ at $\underline\alpha$, and $k'(\alpha)\to+\infty$ as $\alpha\to\bar\alpha^-$. Convexity and twice differentiability, which the footnote also lists, are not assumed. The milestones carry only what they need: none for the willingness to pay, continuity of $k$ for one part of the reduction, and differentiability at the point for the derivative.

A complete development needs Bayes posteriors for a symmetric binary signal, elementary calculus (derivatives, the mean value theorem, extrema on compact intervals), and Topkis's monotonicity theorem, which is on the platform (Theorem 2.8.4) and is referenced by this mission. Proofs of the milestones and of the goal are welcome. Lemmas on the binary-signal posteriors (for instance the identity $\sigma_h(\alpha)v_h(\alpha)+\sigma_l(\alpha)v_l(\alpha)=\hat u$) are reusable by the companion mission on marketing lists.

Selected references

• Liang Guo, Selling Data to Marketers, Management Science, 2025, author's manuscript. doi:10.1287/mnsc.2023.01350
• Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. doi:10.1515/9781400822539

Why sell information to marketers

Data brokers such as Acxiom, Nielsen and Oracle, and data generators such as Google and Facebook, sell processed consumer data to firms that use it to decide whom to target, whom to lend to, or which market to enter. The U.S. Federal Trade Commission's 2014 report on data brokers distinguishes two products: a marketing list, which carries contact information without which the buyer cannot act at all, and a data append, which enriches data the buyer already holds. Liang Guo's Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) asks how a seller should design a menu of data products of different informativeness when buyers differ in a privately known cost of acting.

The question belongs to the theory of optimal screening (Mussa and Rosen 1978; Maskin and Riley 1984), but with a twist: the buyer's marginal value of information is not a primitive. It is derived from the buyer's decision problem, so the direction of the single-crossing condition is itself an outcome of the model. This mission formalizes the paper's analysis of marketing lists in the base model with a binary value.

Setting

A marketer can take an action (target a consumer) at cost $c>0$. The action's value $u$ is $\bar u$ with prior probability $\phi\in(0,1)$ and $\underline u<\bar u$ otherwise. The seller can provide a binary signal $w\in\{w_h,w_l\}$ with $\Pr(w_h\mid\bar u)=\Pr(w_l\mid\underline u)=\alpha$, where the informativeness $\alpha$ lies in an interval $[\underline\alpha,\bar\alpha]\subset(1/2,1)$. The probability of the optimistic signal is $\sigma_h(\alpha)=\phi\alpha+(1-\phi)(1-\alpha)$, the posterior probability of $\bar u$ after it is $\phi_h(\alpha)=\phi\alpha/\sigma_h(\alpha)$, and the posterior mean is $v_h(\alpha)=\phi_h(\alpha)\bar u+[1-\phi_h(\alpha)]\underline u$; $\sigma_l,\phi_l,v_l$ are defined symmetrically. The paper assumes $v_l(\underline\alpha)<c<v_h(\underline\alpha)$, so a marketer acts exactly after $w_h$, and a marketer with cost $c$ who pays $T$ for a signal of informativeness $\alpha$ gets

$$U=-T+\sigma_h(\alpha)[v_h(\alpha)-c].$$

Serving a marketer at informativeness $\alpha$ costs the seller $k(\alpha)$, with $k(\underline\alpha)=0$ and $k$ increasing.

There are two cost types, $c_H>c_L>0$, with $\Pr(H)=\theta\in(0,1)$; write $\theta_H=\theta$, $\theta_L=1-\theta$. Under the benchmark with observable cost, the seller extracts all surplus and chooses $\alpha$ to maximize

$$\Pi_i(\alpha)=\theta_i\big[\sigma_h(\alpha)[v_h(\alpha)-c_i]-k(\alpha)\big],$$

whose maximizers are the efficient levels $\alpha^e_i$. With private costs the seller offers a menu $(T_H,\alpha_H),(T_L,\alpha_L)$ with $T_j\ge0$ and maximizes $\Pi=\sum_i\theta_i[T_i-k(\alpha_i)]$ subject to individual rationality $U_{ii}\ge0$ and incentive compatibility $U_{ii}\ge U_{ii'}$, where $U_{ij}=-T_j+\sigma_h(\alpha_j)[v_h(\alpha_j)-c_i]$. This is problem (6); its solutions are the optimal menus, with informativeness levels $\alpha^*_H,\alpha^*_L$.

Formalization targets

Goal: Proposition 2

Under the regularity of $k$ described below,

$$\alpha^*_L=\alpha^e_L,\qquad \alpha^*_H>\alpha^e_H\ \text{ if }\phi<\tfrac12,\qquad \alpha^*_H<\alpha^e_H\ \text{ if }\phi>\tfrac12.$$

The first claim is an equality of sets of maximizers; the inequalities compare every optimal menu with every efficient level.

Milestones

1. The derivative of the benchmark profit: $\partial\Pi_i/\partial\alpha_i=\theta_i[\phi(\bar u-c_i)-(1-\phi)(\underline u-c_i)-k'(\alpha_i)]$.
2. The cross derivative $\partial^2\Pi_i/\partial\alpha_i\partial c_i=\theta_i(1-2\phi)$, stated as a mixed second difference.
3. Proposition 1: $\alpha^e_i$ increases with $c_i$ if $\phi<1/2$ and decreases if $\phi>1/2$.
4. The reduction of (6) to the problem in $(\alpha_H,\alpha_L)$ alone,

$$\max_{\alpha_H,\alpha_L}\ \theta\big[\sigma_h(\alpha_H)[v_h(\alpha_H)-c_H]-k(\alpha_H)\big]+(1-\theta)\big[\sigma_h(\alpha_L)[v_h(\alpha_L)-c_L]-\sigma_h(\alpha_H)(c_H-c_L)-k(\alpha_L)\big],\qquad(7)$$

obtained by making IR$_H$ and IC$_{L,H}$ bind. 5. The derivative of (7) in $\alpha_H$: $\theta[\phi(\bar u-c_H)-(1-\phi)(\underline u-c_H)-k'(\alpha_H)]+(1-\theta)(1-2\phi)(c_H-c_L)$.

Significance

In textbook screening the low type's allocation is distorted downward to reduce the high type's rent. Here the low type of the screening problem is the high-cost marketer, and its information can be distorted in either direction: the rent $\sigma_h(\alpha_H)(c_H-c_L)$ conceded to low-cost marketers falls with $\alpha_H$ when $\phi<1/2$ and rises when $\phi>1/2$. Proposition 2 therefore says that a seller of marketing lists may supply socially excessive information to some buyers, a possibility absent from the data-appends literature the paper compares against, where provision can only be insufficient. Proposition 1 isolates the mechanism: the prior decides whether information mainly prevents wasteful targeting or restores profitable targeting, and the cost of acting amplifies one or the other.

The result is proved in the paper; nothing in it has been machine-checked. The mission produces a checked version of the two-type screening reduction (including the verification that the constraints dropped in (7) hold at its solutions, which the paper asserts as standard) and of the comparative statics with set-valued optima, since $k$ is not assumed convex and optima need not be unique.

Difficulty

The derivative computations are routine once $\sigma_h(\alpha)v_h(\alpha)$ is simplified to $\phi\alpha\bar u+(1-\phi)(1-\alpha)\underline u$. The work lies elsewhere. First, the reduction: "IR binds for the high-cost type and IC binds for the low-cost type" is the standard heuristic, but at a solution of (7) one still has to check the dropped constraint IC$_{H,L}$ and the nonnegativity $T_L\ge0$; both depend on the ordering of $\alpha_H$ and $\alpha_L$ at the optimum, which in turn depends on the sign of $1-2\phi$. Second, strictness: comparative statics through increasing differences give only weak inequalities between maximizer sets. Upgrading $\alpha^*_H\ge\alpha^e_H$ to $\alpha^*_H>\alpha^e_H$ requires ruling out a common maximizer, which needs the optimum to be interior and $k$ differentiable there; the naive argument by first-order conditions fails at the corners $\underline\alpha,\bar\alpha$. Third, $\alpha^*_L=\alpha^e_L$ as sets requires existence of optimal menus, hence attainment of the maximum of (7).

Formalization scope

Everything is over $\mathbb R$. The model is a structure Model (values, prior, informativeness interval, selling cost) extended by Screening (type probability and the two costs); the standing assumptions $\underline u<\bar u$, $0<\phi<1$, $1/2<\underline\alpha<\bar\alpha<1$, $k(\underline\alpha)=0$, $k$ increasing on $[\underline\alpha,\bar\alpha]$ (weakly), $0<\theta<1$, $0<c_L<c_H$, and $v_l(\underline\alpha)<c_i<v_h(\underline\alpha)$ for both types are fields. The posteriors are defined with the divisions printed in (2). Efficient levels and optimal menus are sets of maximizers, never chosen by Classical.choose or a first-order condition. Menus include $T_j\ge0$.

The goal additionally assumes the part of footnote 5 (p. 7) that makes optima interior: $k$ continuous on $[\underline\alpha,\bar\alpha]$, differentiable on $(\underline\alpha,\bar\alpha)$, with right derivative $k'(\underline\alpha)=0$ and $k'(\alpha)\to+\infty$ as $\alpha\to\bar\alpha^-$. Convexity and twice differentiability, also in the footnote, are not assumed. The milestones carry no regularity beyond differentiability at the point considered (milestones 1, 5) and continuity for the optimality characterization in milestone 4.

The optimal menu is a maximizer of (6) under all four constraints, not a maximizer of (7): defining it through (7) would make half of the goal immediate and skip the reduction.

The development needs the algebra of the binary posterior, the two-type screening reduction, and a strict version of monotone comparative statics; Topkis's theorem on strictly increasing differences (Theorem 2.8.4) is already proved on the platform and referenced. Proofs of any milestone, and alternative arguments for the strict inequalities, are welcome.

Selected references

• L. Guo, Selling Data to Marketers, Management Science, 2025 (author's manuscript). https://doi.org/10.1287/mnsc.2023.01350
• D. M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• M. Mussa and S. Rosen, Monopoly and Product Quality, Journal of Economic Theory 18(2), 1978. https://doi.org/10.1016/0022-0531(78)90085-6
• E. Maskin and J. Riley, Monopoly with Incomplete Information, RAND Journal of Economics 15(2), 1984. https://doi.org/10.2307/2555674
• Federal Trade Commission, Data Brokers: A Call for Transparency and Accountability, 2014. https://www.ftc.gov/reports/data-brokers-call-transparency-accountability-report-federal-trade-commission-may-2014

Motivation

Data brokers sell consumer data to firms that use it to decide whom to target, whom to lend to, or where to open a store. Two kinds of products are common: a marketing list, which supplies contact information without which the buyer cannot act at all, and a data append, which enriches information about consumers the buyer can already reach (Federal Trade Commission, Data Brokers, 2014). A seller who does not know a buyer's cost of acting must screen buyers with a menu of plans that differ in price and in how informative the data are.

Liang Guo's paper Selling Data to Marketers (Management Science, doi:10.1287/mnsc.2023.01350) characterizes the optimal menu, first for a binary-value model (§3) and then for a general information structure ordered by rotation (§4), following Johnson and Myatt (2006). This mission formalizes Proposition 7: data appends under the rotation order. It is the fourth mission of a series built from the same manuscript; the first three cover marketing lists and data appends in the binary model and marketing lists under the rotation order.

Setting

A marketer can take an action (target a consumer) at cost $c$; the action's value $u$ is uncertain with prior mean $\hat u$. A data service of informativeness $\alpha\in[\underline\alpha,\bar\alpha]\subset(0,1)$ produces a signal, and its information is summarized by the posterior mean $v$. For each $\alpha$, $v$ has cumulative distribution function $H(v,\alpha)$ on a support $[\underline v,\bar v]$, with a strictly positive density $h(v,\alpha)$ and mean $\hat u$ for every $\alpha$. The family is rotation ordered: there is a point $v^+\in(\underline v,\bar v)$ with

$$\frac{\partial H(v,\alpha)}{\partial\alpha}>0 \ (v<v^+),\qquad \frac{\partial H(v,\alpha)}{\partial\alpha}<0 \ (v>v^+).$$

A more informative service spreads the posterior mean away from $\hat u$.

A service plan $(T,\alpha)$ charges a fixed fee $T\ge0$. Serving a marketer with informativeness $\alpha$ costs the seller $k(\alpha)$, with $k(\underline\alpha)=0$ and $k$ increasing. A marketer targets exactly when $v>c$, so a marketer with cost $c_i$ who buys $(T_j,\alpha_j)$ earns

$$U_{ij}=-T_j+\int_{c_i}^{\bar v}(v-c_i)\,dH(v,\alpha_j).$$

Costs are $c_H$ with probability $\theta\in(0,1)$ and $c_L$ with probability $1-\theta$, $0<c_L<c_H$. A data-append buyer can act without the data, so its outside option is $U_{i0}=\max\{\hat u-c_i,0\}$.

The seller offers a menu $(T_H,\alpha_H),(T_L,\alpha_L)$ and maximizes $\Pi=\theta[T_H-k(\alpha_H)]+(1-\theta)[T_L-k(\alpha_L)]$ subject to individual rationality $U_{ii}\ge U_{i0}$ and incentive compatibility $U_{ii}\ge U_{ii'}$ for both types. Call any maximizer an optimal menu, with levels $\alpha^*_H,\alpha^*_L$. The benchmark with observable costs is

$$\max_{\alpha\in[\underline\alpha,\bar\alpha]}\ \theta_i\Big[\int_{c_i}^{\bar v}(v-c_i)\,dH(v,\alpha)-k(\alpha)\Big],$$

and its maximizers are the efficient levels $\alpha^e_i$.

Formalization targets

Goal: Proposition 7

Assume $c_L<c_H<\hat u$. If $c_L<c_H<v^+$, then

$$\alpha^*_H=\alpha^e_H,\qquad \alpha^*_L<\alpha^e_L ,$$

and if $v^+<c_L<c_H$, then

$$\alpha^*_H=\alpha^e_H,\qquad \alpha^*_L>\alpha^e_L .$$

Here $\alpha^*_H=\alpha^e_H$ means that the set of $\alpha_H$-levels of optimal menus equals the set of efficient levels, and each strict inequality holds for every optimal menu and every efficient level.

Milestones

1. The willingness to pay for a data append (p. 20): for $c\le\hat u$, $U_{ij}-U_{i0}=-T_j+\int_{\underline v}^{c_i}(c_i-v)\,dH(v,\alpha_j)$, which is increasing in $c_i$.
2. Its integrated form (proof of Proposition 8, p. 33): $U_{ij}-U_{i0}=-T_j+\int_{\underline v}^{c_i}H(v,\alpha_j)\,dv$.
3. The reduction (15) (p. 20): substituting the binding $IR_L$ and $IC_{H,L}$ turns the screening problem into a maximization over $(\alpha_H,\alpha_L)$.
4. (15) integrated by parts, and $\alpha^*_H=\alpha^e_H$ for it (p. 33).
5. The derivative $\partial\Pi/\partial\alpha_L$ of (15) compared with the benchmark's (p. 33).

Significance

Proposition 7 is the general-distribution form of a "double reversal". With marketing lists the low-cost marketers are the high type: they get efficient information, and the high-cost marketers' information is distorted (Proposition 5 of the paper). With data appends and costs below the prior mean, the outside option makes the high-cost marketers value data more. The roles of the types swap, and the direction of the distortion flips with the position of the costs relative to the rotation point. The result tells a data seller which customers to under- or over-supply, and shows that the answer depends on whether its data enable an action or only refine it.

The paper proves the result on a few pages, partly by phrases such as "it can be readily verified". No machine-checked version exists. A formalization makes explicit what the printed argument leaves implicit: that the dropped constraints hold at the reduced optimum, which regularity of $k$ and $H$ the strict inequalities need, and that statements about "the" optimum hold for every optimum when maximizers are not unique.

Difficulty

The obvious approach substitutes the binding constraints and compares first-order conditions. Two steps of it fail as stated. First, the reduction to (15) drops $IR_H$ and $IC_{L,H}$; $IC_{L,H}$ holds at a maximizer of (15) only when the two informativeness levels are ordered as the rotation order dictates. That ordering is available only when both costs lie on the same side of $v^+$. Second, first-order conditions say nothing at a corner of $[\underline\alpha,\bar\alpha]$. The strict comparison $\alpha^*_L\ne\alpha^e_L$ needs the efficient level to be interior, where the derivative of $k$ exists. That comes from the conditions of footnote 5 together with the mean-preserving property of the family. The selling cost need not be convex, so maximizers can be non-unique, and every comparison must hold for every pair of maximizers.

Formalization scope

• Information structure. A structure RotationFamily with a bounded support $\underline v<\bar v$ (the paper allows an unbounded one). $H(\cdot,\alpha)$ is continuous on $[\underline v,\bar v]$ with $H(\underline v,\alpha)=0$, $H(\bar v,\alpha)=1$ and derivative $h(\cdot,\alpha)>0$, continuous on the closed support. $\partial H/\partial\alpha$ exists on the closed support. The rotation order (9) holds on the open support, and the mean is $\hat u$ for every $\alpha\in(0,1)$. Condition (10) is not assumed; it follows.
• Model. Model extends it with $0<\underline\alpha<\bar\alpha<1$, $\theta\in(0,1)$, and $0<c_L<c_H$ with both costs in $(\underline v,\bar v)$ (a pin: the integrals $\int_{c_i}^{\bar v}$ presume it). It also fixes $k(\underline\alpha)=0$ with $k$ monotone on $[\underline\alpha,\bar\alpha]$. $dH$ is written as $h\,dv$.
• Objects of the goal. Optimal menus are maximizers of the full problem: fees $T\ge0$, levels in $[\underline\alpha,\bar\alpha]$, $IR_i$ with outside option $\max\{\hat u-c_i,0\}$, and both IC constraints. Efficient levels are maximizers of the benchmark (12). Neither is defined through (15) or a first-order condition. That would make the first half of the goal a restatement of milestone 4, and writing the outside option as $\hat u-c$ instead of the maximum would change the model.
• Pinned hypotheses. On the goal only: the part of footnote 5 the strict results use ($k$ continuous on $[\underline\alpha,\bar\alpha]$, differentiable inside, $k'(\underline\alpha)=0$ from the right, $k'(\alpha)\to+\infty$ as $\alpha\to\bar\alpha^-$) and joint continuity of $\partial H/\partial\alpha$ on $[\underline v,\bar v]\times(0,1)$. The derivative milestone uses only the latter. Convexity of $k$ is not assumed.
• Range restriction. The first sentence of Proposition 7 ($\alpha^*_H=\alpha^e_H$) is posed on the full problem only within the two ranges $c_H<v^+$ and $v^+<c_L$. For (15) it is posed without restriction in milestone 4. The branch $v^+<c_L<c_H<\hat u$ is empty when $v^+\ge\hat u$, for example for symmetric structures; non-symmetric rotation families with $v^+<\hat u$ inhabit it.
• Reuse. Topkis's monotonicity theorem (Theorem 2.8.4) is on the platform and is the tool the paper invokes. The integration-by-parts facts for distribution functions on a bounded support, and differentiation of $\int_c^{\bar v}H(v,\alpha)\,dv$ in $\alpha$, are reusable beyond this mission. Proofs of the milestones in any order are welcome.

Selected references

• Liang Guo, Selling Data to Marketers, Management Science, 2025 (author's manuscript used here). https://doi.org/10.1287/mnsc.2023.01350
• Justin P. Johnson and David P. Myatt, On the Simple Economics of Advertising, Marketing, and Product Design, American Economic Review 96(3), 2006. https://doi.org/10.1257/000282806777211946
• Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539
• Federal Trade Commission, Data Brokers: A Call for Transparency and Accountability, 2014. https://www.ftc.gov/reports/data-brokers-call-transparency-accountability-report-federal-trade-commission-may-2014

Motivation

A seller with several goods can sell them one at a time or offer a mechanism that links allocation and payment across goods. Separate selling asks the seller to solve a one-good pricing problem for each item. A general mechanism can offer lotteries and menus whose outcomes depend on the buyer's whole valuation vector. The difference matters because the buyer's private information covers several values at once, and an optimal multidimensional mechanism need not resemble an ordinary posted price. Hart and Nisan ask how much revenue is guaranteed by simple selling rules when the joint valuation distribution is unrestricted apart from the stated independence assumptions (Hart and Nisan, arXiv:1204.1846v3).

This mission isolates their two-good, identically distributed result, Theorem B. The paper first gives a one-half guarantee for two independent goods with potentially different distributions, then improves the guarantee to $e/(e+1)$ when their distributions agree. The improvement is a claim about every probability law on nonnegative values. It assumes neither a density nor a regularity condition on the tail of that law. The paper proves the result in Appendix A.1 after stating it in the introduction (Hart and Nisan, pp. 6 and 31–35).

Setting

There is one risk-neutral buyer and one seller. For two goods, the buyer's private valuation is a vector $(Y,Z)$ with $Y,Z\ge0$. Values are additive: receiving both goods is worth $Y+Z$. The seller knows the distribution of the vector but not the realized values. In this mission, $Y$ and $Z$ are independent and have the same arbitrary probability law $\nu$ on $\mathbb R_{\ge0}$. A law, rather than a named pair of random variables on a probability space, carries all the data needed by the revenue quantities.

A direct mechanism $\mu=(q,s)$ takes a reported pair $x=(y,z)$ and returns an allocation probability $q_i(x)\in[0,1]$ for each good and a real payment $s(x)$ to the seller. The buyer's payoff from reporting truthfully is $b(x)=q(x)\cdot x-s(x)$. The mechanism is incentive compatible (IC) if truthful reporting is at least as good as any other report for every possible valuation, and individually rational (IR) if truthful payoff is nonnegative everywhere. These requirements hold on the whole nonnegative orthant, as in Section 2.1 of the paper (Hart and Nisan, pp. 11–14).

Write $R(\mu;X)$ for the expected payment under a valuation law $X$ and $\operatorname{Rev}(X)$ for the supremum of $R(\mu;X)$ over feasible, IC, IR mechanisms. For one good, write $\operatorname{Rev}_1(\nu)$. The separate-selling revenue for two identically distributed goods is $\operatorname{SRev}(Y,Z)=2\operatorname{Rev}_1(\nu)$. Equation (1) of the paper identifies the one-good value with the supremum of posted-price revenue $p\Pr[Y\ge p]$; the supremum formulation covers laws for which no maximizing price exists (Hart and Nisan, p. 12; Myerson, 1981).

Formalization targets

Theorem B: the guarantee for two i.i.d. goods

The goal is the exact upper bound written at the start of the paper's proof:

$$\operatorname{Rev}(Y,Z)\le\frac{e+1}{e}\bigl(\operatorname{Rev}(Y)+\operatorname{Rev}(Z)\bigr)=\frac{e+1}{e}\operatorname{SRev}(Y,Z).$$

Equivalently, separate selling guarantees at least $e/(e+1)$ of optimal revenue whenever the ratio has an ordinary meaning. The inequality itself is the stable formulation at zero and infinite revenues. The formal goal uses the exact constant $(e+1)/e$, not the rounded percentage in the theorem's prose (Hart and Nisan, Theorem B, p. 6; proof, p. 31).

Supporting targets

The milestones include the one-good posted-price identity, the fact that nonnegative payments suffice when optimizing, symmetrization for identical independent goods, Lemma 19's lower-valuation revenue bound, equation (12), and the two expectation estimates and final numerical bound used after it. Proposition 5's IC characterization is also a draft theorem, though it is not a milestone. Each statement retains its source's domain and the constant $1/e$. The final inequality for the right side of (12) is stated for every nondecreasing allocation function into $[0,1]$, as required by the paper's argument on pp. 33–35.

Significance

Theorem B gives a distribution-free quantitative guarantee for an easy-to-describe selling rule in a setting where the optimal rule may depend on the buyer's entire two-dimensional private type. Its $e/(e+1)$ guarantee is stronger than the one-half guarantee for merely independent goods stated as Theorem A. The conclusion concerns the best revenue available from all feasible IC and IR mechanisms, so the benchmark includes randomized allocations and payments depending on both reported values (Hart and Nisan, pp. 6 and 11–13).

The formalization target is a machine-checked version of a proved result, not a new conjecture. The proposal currently contains compiled Lean statements with unproved theorem bodies. A completed development would prove the stated inequality and its selected supporting results. It would also supply reusable definitions for direct mechanisms with additive nonnegative values, extended-real revenue, optimal revenue as a supremum, and symmetry of two-good mechanisms. No machine-checked proof of these proposed Hart–Nisan statements is claimed here.

Difficulty

The one-good posted-price formula does not directly control an arbitrary two-good mechanism: allocation of either good and the payment can depend on both reported values. Applying a one-good bound separately to the two coordinates therefore leaves terms that depend on the other coordinate. In particular, a direct comparison between each marginal posted-price optimum and the total payment loses the improved constant. The proof has to control the dependence created by a joint mechanism while retaining the exact $1/e$ numerical estimate. A second formal difficulty is that an admissible mechanism can have a negative expected payment even though optimal revenue is nonnegative, while an unrestricted law can give infinite optimal revenue. Replacing every expectation by an ordinary real integral or clipping each mechanism's revenue would change Lemma 19 and the intermediate inequalities (Hart and Nisan, pp. 31–35).

Formalization scope

Valuations are finite vectors $\iota\to\mathbb R_{\ge0}$; the main theorem fixes $\iota=\operatorname{Fin}(2)$. The two-good law is the product of the same one-good probability measure in both coordinates, so independence and identical distribution are built into the data. The model represents allocation probabilities as real numbers with explicit bounds $0\le q_i\le1$. It requires IC and IR pointwise on all reports. No positive transfer (NPT) means $s(x)\ge0$ and is imposed only on supporting statements where the paper uses it. Following the paper's footnote 12, admissibility also requires the payment function to be measurable.

An individual expected payment is an extended real difference of positive and negative Lebesgue integrals. For IC mechanisms, the negative part is finite because the payment is bounded below by its value at zero. Optimal revenue is the supremum of the nonnegative clips of admissible mechanisms' expected payments; the zero mechanism makes this the same supremum as in the paper. Lemma 19 and equation (12) keep individual revenue in the extended reals. Supporting inequalities that write $r=\operatorname{Rev}_1(\nu)$ as a real number explicitly assume $r<\infty$; Theorem B does not. Integrals of bounded threshold functions use ordinary real expectation, while the nonnegative term $W$ uses a nonnegative Lebesgue integral. The goal cannot be satisfied by a correlated joint law, a bounded-support special case, a vacuous assumption on $\nu$, or a rounded constant.

The reusable work includes one-good posted-price revenue for arbitrary laws, a nonnegative-transfer reduction, a faithful single-mechanism revenue type, and probability identities for two independent coordinates. Theorem A, Theorem 7, Theorem 16, and a full formalization of the paper's other selling rules are outside this mission.

Selected references

• Sergiu Hart and Noam Nisan, Approximate Revenue Maximization with Multiple Items, Journal of Economic Theory, 2017. Source used here: arXiv:1204.1846v3.
• Roger B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. DOI:10.1287/moor.6.1.58.