Operations Research

Price discrimination when demand has network effects

Third-degree price discrimination means charging different prices to identifiable groups of customers. Its welfare effects are a classical question in industrial organization. With linear demands and every market served under uniform pricing, discrimination leaves total output unchanged and lowers total welfare (Pigou 1920). More generally, welfare can rise only if total output rises (Schmalensee 1981; Varian 1985).

Many current markets are two-sided platforms: marketplaces, app stores and payment networks that charge sellers participation fees and differentiate those fees by seller category (for instance, app stores charging games and non-games differently). On such a platform, a seller's presence is worth something to the buyers on the other side. De Cornière, Mantovani and Shekhar (Management Science 71(4), 2025) show that this cross-side benefit overturns the classical conclusion: discriminating between seller types raises seller participation, which attracts more buyers, which raises seller participation further. In their linear model, total welfare rises, and for large enough cross-side benefits every group gains.

The baseline model

A monopoly platform serves a mass one of buyers and two categories of sellers, $L$ and $H$, each of mass one.

• A buyer obtains a stand-alone value $v$ from the platform and a benefit $b$ for each seller on it.
• A seller of type $j\in\{L,H\}$ earns $\theta_j$ per buyer on the platform, with $\theta_H>\theta_L>0$.
• All agents have outside options uniform on $[0,1]$. With $N_B$ buyers, the type-$j$ seller demand at fee $f_j$ is $\theta_jN_B-f_j$. With $N_S$ sellers, the buyer demand at price $p$ is $v+bN_S-p$.

The platform chooses participation levels, and the fees follow from the inverse demands.

Uniform pricing ($f_L=f_H$). The platform chooses $(N_B,N_S)$ to maximize

$$\Pi^U(N_B,N_S)=N_B\,(v+bN_S-N_B)+N_S\,\frac{(\theta_L+\theta_H)N_B-N_S}{2}.$$

At the common fee $f^U$, type-$j$ participation is $N^U_j=\theta_jN_B-f^U$.

Price discrimination. The platform chooses $(N_B,N_L,N_H)$ to maximize

$$\Pi^D(N_B,N_L,N_H)=N_B\big(v+b(N_L+N_H)-N_B\big)+N_L(\theta_LN_B-N_L)+N_H(\theta_HN_B-N_H).$$

The participant with outside option $k$ joins when its net value exceeds $k$. Buyer surplus $CS$ and type-$j$ seller surplus $DS_j$ are therefore integrals over $k$ from $0$ to the participation level of (net value $-\,k$). Total welfare is $SW=CS+\Pi+DS_L+DS_H$.

Assumption 1 (p. 3343) restricts the parameters: (i) $0<v<4-(b+\theta_L)^2-(b+\theta_H)^2$; (ii) $(\theta_H-3\theta_L)/2<b$.

Two denominators recur: $U=8-(2b+\theta_H+\theta_L)^2$ and $D=4-2b^2-\theta_H^2-\theta_L^2-2b(\theta_H+\theta_L)$.

Formalization targets

Goal: Proposition 2 (p. 3346)

Under $\theta_H>\theta_L>0$, $b>0$ and Assumption 1, both optimization problems have a solution, and for every uniform optimum and every discrimination optimum:

$$\Pi^U<\Pi^D,\qquad CS^U<CS^D,\qquad DS^U_L<DS^D_L,\qquad SW^U<SW^D,$$ $$DS^U_H<DS^D_H\iff b>\hat b(\theta_H,\theta_L)=\frac{\sqrt{32-7(\theta_H-\theta_L)^2}-3\theta_H-\theta_L}{4}.$$

When $b>\hat b$, all four groups (platform, buyers, low-type sellers and high-type sellers) are strictly better off: a strict Pareto improvement.

Milestones

1. The uniform optimum, display (12): $N^U_B=4v/U$, $N^U_S=2v(2b+\theta_H+\theta_L)/U$, $\Pi^U=2v^2/U$, with the fees and, from footnote 14, $N^U_j$.
2. The discrimination optimum, (13)–(15): $N^D_B=2v/D$, $N^D_j=v(b+\theta_j)/D$, $\Pi^D=v^2/D$, with the fees.
3. Proposition 1: $N^U_B<N^D_B$ and $N^U_S<N^D_L+N^D_H$.
4. The surpluses and welfare at the uniform optimum (A.2.1).
5. The surpluses and welfare at the discrimination optimum, (A.6)–(A.8).
6. $\Pi^D-\Pi^U=v^2(\theta_H-\theta_L)^2/(DU)>0$.
7. $DS^D_L-DS^U_L>0$.
8. $SW^D-SW^U=v^2(\theta_H-\theta_L)^2\lambda/(2D^2U^2)$ for an explicit quartic $\lambda(b,\theta_H,\theta_L)$.
9. $\lambda>0$ on the parameter region.
10. $DS^D_H-DS^U_H>0\iff b>\hat b$.

Significance

The result. Proposition 2 is a counterpoint to the Pigouvian benchmark. In a two-sided market with linear demands, seller-side discrimination can be a strict Pareto improvement, so a blanket presumption against fee differentiation by platforms is not justified on welfare grounds. The comparison also isolates the mechanism. The low-type sellers gain even though the platform could already serve them, and the high types gain only when the buyer-side benefit $b$ is large enough. The paper's extensions in §5 (seller-type-dependent buyer benefits, ad valorem fees, competition) start from this baseline.

Formalizing it. The paper proves Proposition 2 by explicit algebra in Appendix A.2. Most of that algebra is printed, but the positivity of $\lambda$ is argued only through claims about the roots of a quartic in $b$, which are asserted rather than shown. No part of the argument is machine-checked. A formalization would give:

• a certified positivity proof for $\lambda$;
• verified closed forms for both optima, with existence and uniqueness of the maximizers;
• corrected versions of several printed displays (see the scope section).

The model is a small, self-contained template for platform pricing with linear demands, and the same definitions can serve later comparisons (fees, prices, exclusion).

Difficulty

The optimization steps are routine: both objectives are concave quadratics, strictly concave exactly when $U>0$ and $D>0$, and Assumption 1(i) gives $D>v>0$. The integrals have affine integrands. The comparison steps are where the work is.

• $\lambda>0$. $\lambda$ is a quartic in three variables that must be shown positive on a region cut out by $D>0$, $b>0$, $0<\theta_L<\theta_H$ and condition (ii). Its minimum over the region is small (numerically about $0.02$, approached near the boundary $D=0$), so crude bounds fail. The paper's argument ("only one positive root $b^{sol}$", "$b^{sol}$ greater than $\bar b$") is not a proof.
• The $\hat b$ equivalence. It compares two rational functions with different denominators $D^2$ and $U^2$. It reduces to the sign of $(b+\theta_H)U-(2b+3\theta_H-\theta_L)D$ on the region, which must be tied to the root $\hat b$ of a quadratic.
• Proposition 1 is a comparison of explicit rational functions under the same region constraints. The paper argues it through best-response curves instead (App. A.1).

Formalization scope

• Representation. Parameters are real numbers $v,b,\theta_H,\theta_L$. A uniform allocation is $(N_B,N_S)\in\mathbb R^2$, a discriminatory one $(N_B,N_L,N_H)\in\mathbb R^3$ (low type before high type).
• Equilibrium means a global maximizer of $\Pi^U$ (resp. $\Pi^D$) over all real participation levels, the object the first-order conditions (7)–(11) solve. No $[0,1]$ box is imposed.
• Surpluses are Lean interval integrals at an arbitrary allocation. Uniform-regime seller participation by type is the demand at the common fee.
• Standing assumptions and pins.
  • $\theta_H>\theta_L>0$ is §3.1's assumption.
  • $b>0$ is the standing assumption of §3.2 and footnote 10.
  • Assumption 1 is used as printed. The paper's bound $\bar b$ (p. 3344) corresponds to $2v<4-(b+\theta_L)^2-(b+\theta_H)^2$, the condition for interior buyer participation $N^D_B=2v/D<1$. Under the printed $v<\dots$, participation can exceed one, so the mission does not pose §3.4's claim that all participation levels are interior. Every comparison in the goal holds over the printed region.
• Printed slips, corrected in the Lean and disclosed.
  • The $\Pi^D-\Pi^U$ denominator prints $2b(\theta_H-\theta_L)$ where $D$ has $2b(\theta_H+\theta_L)$.
  • The $SW^D-SW^U$ denominator prints $\theta_l$ for $\theta_L$.
  • The $DS_L$ and $DS_H$ difference displays swap their two fractions.
  • "$\sum_{i=1,2}DS_j$" means $DS_L+DS_H$.
• Ruled-out formalizations. The optima are not defined by their closed forms, the surpluses are not defined by their final expressions, and the goal and the equilibrium milestones assert existence of the maximizers, so the universally quantified comparisons are not vacuous. Uniform-regime seller participation is split by demand, never as $N_S/2$.
• Not posed. Propositions 3–9, Lemma 1, §4.4 and §5 are not part of this mission. Propositions 3–5 need box-constrained or corner models, and the proofs for §5 are in an Online Appendix.
• Infrastructure. Maximizers of strictly concave quadratics on $\mathbb R^n$, integrals of affine functions, and polynomial positivity certificates (SOS or case splits) on semialgebraic regions. A clean lemma that a negative-definite quadratic form plus a linear term has a unique maximizer given by its first-order conditions would be reusable well beyond this mission. Contributions toward any milestone, and alternative proofs of $\lambda>0$, are welcome.

Selected references

• A. de Cornière, A. Mantovani, S. Shekhar, Third-Degree Price Discrimination in Two-Sided Markets, Management Science 71(4):3340–3356, 2025. doi:10.1287/mnsc.2023.02788
• A. C. Pigou, The Economics of Welfare, Macmillan, London, 1920.
• R. Schmalensee, Output and Welfare Implications of Monopolistic Third-Degree Price Discrimination, American Economic Review 71(1):242–247, 1981.
• H. R. Varian, Price Discrimination and Social Welfare, American Economic Review 75(4):870–875, 1985.
• M. Armstrong, Competition in Two-Sided Markets, RAND Journal of Economics 37(3):668–691, 2006. doi:10.1111/j.1756-2171.2006.tb00037.x

Motivation

Large online marketplaces such as Amazon, JD.com and Walmart.com act both as a sales channel for third-party sellers and as a retailer of their own. A platform watches which third-party products sell well and may start selling the same product itself, a move called platform entry. Over ten months of 2013–2014, Amazon entered about 3% of the products first offered only by third-party sellers, and its entry lowered the affected products' sales rankings, that is, raised their total sales (Zhu & Liu, Strategic Management Journal 2018). The conventional view is that a seller should deter entry, since the platform becomes a competitor that also collects a referral fee on every sale the seller makes.

L. Qi, H. Song and W. Xiao (Management Science 2025) build a two-stage model with three features: the platform charges a referral rate on the seller's revenue, the platform's marketing effort spills over to the seller's product, and the two parties compete in quantities with differentiated products. Their Proposition 2 identifies exactly when the seller is better off if the platform enters. This mission formalizes that result together with the equilibrium analysis it rests on.

Setting

There are five parameters: the degree of spillover $\delta \in [0,1]$, the referral rate $f \in [0,1)$, the competition intensity $\beta \in [0,1]$, the seller's effort-cost coefficient $c_S$ and the platform's entry cost $K$. The product has base value $a$. The platform's effort-cost coefficient is normalized to $1/2$.

Stage 1. The seller chooses an effort $e_S$ at cost $c_S e_S^2$, which raises the product value to $a + e_S$, and a quantity $q_1$. The price is $p_1 = a + e_S - q_1$, and the seller earns $q_1 p_1 (1-f) - c_S e_S^2$ after paying the referral fee $f q_1 p_1$.

Stage 2 without entry. The seller alone sells $q_S$ at price $p_S = a + e_S - q_S$ and earns $q_S p_S(1-f)$.

Stage 2 with entry. The platform chooses an effort $e_P \ge 0$ at cost $e_P^2/2$. Its own product's value becomes $a + e_S + e_P$, and the seller's product's value becomes $a + e_S + \delta e_P$. The two then choose quantities simultaneously, with prices

$$p_S = a + e_S + \delta e_P - q_S - \beta q_P, \qquad p_P = a + e_S + e_P - q_P - \beta q_S .$$

The seller earns $q_S p_S (1-f)$. The platform earns $q_S p_S f + q_P p_P - e_P^2/2 - K$: the referral fee on the seller's revenue plus its own margin.

Backward induction gives closed forms. Write

$$N_5 = 4(1+\delta) - 2\beta(2-\delta+\delta^2) + \beta^3(1+f) - \beta^2(2+f+\delta f)$$

and let $D$ be the quartic denominator of the platform's optimal effort (Lemma 2). Condition (5) is $N_5 > 0$: under it the seller stays in the market after entry. The paper assumes (5) from that point on. Let

$$H = \begin{cases} N_5^2/D^2 & \text{if (5) holds},\\ 0 & \text{otherwise,}\end{cases}$$

so that the seller's two-stage profits as functions of the effort $e_S$ are

$$\Pi^S_N(e_S) = \tfrac12 (1-f)(a+e_S)^2 - c_S e_S^2, \qquad \Pi^S_E(e_S) = \big(\tfrac14 + H\big)(1-f)(a+e_S)^2 - c_S e_S^2 .$$

The receptive regime is $\Omega = \{(\delta,f,\beta) \mid H > 1/4\}$.

Formalization targets

Goal: Proposition 2

$$\Pi^S_E(e_S) > \Pi^S_N(e_S) \iff (\delta,f,\beta) \in \Omega \qquad (a + e_S \ne 0),$$

and the shape of $\Omega$ on the box $[0,1]\times[0,1)\times[0,1]$:

• for fixed $(f,\beta)$ there is $\tilde\delta(f,\beta)$ with $(\delta,f,\beta)\in\Omega \iff \delta > \tilde\delta(f,\beta)$;
• for fixed $(\delta,\beta)$ there is $\tilde f(\delta,\beta)$ with $(\delta,f,\beta)\in\Omega \iff f > \tilde f(\delta,\beta)$;
• for fixed $(\delta,f)$ there are $\beta_1(\delta,f) \le \beta_2(\delta,f)$ with $(\delta,f,\beta)\in\Omega \iff \beta < \beta_1$ or $\beta > \beta_2$.

The thresholds are existentials, as the paper defines them only inside its proof.

Milestones

1. Lemma 1: the stage-2 quantity game after entry has a unique equilibrium, given in closed form.
2. Lemma 2 under (5): the platform's optimal effort $e^*_P$ in closed form, and the seller stays ($q^*_S > 0$). The positivity of $e^*_P$ and of its denominator is a separate milestone.
3. Equations (6)–(8): the seller's equilibrium two-stage profits are $\Pi^S_N$ and $\Pi^S_E$ above.
4. The identity $4N_5^2 - D^2 = P_{11}\cdot S_2$ from the proof of Proposition 2, where $P_{11}$ is the function (11).
5. Under (5) the second factor $S_2$ is positive.
6. Lemma 3, in three parts: the sign pattern of (11) in $\delta$, in $f$ and in $\beta$.

Significance

The result. Proposition 2 says that the seller's preference does not depend on the seller's own effort or on the base value, only on $(\delta, f, \beta)$. It shows that the conventional advice to deter entry is wrong on a nonempty region: a strong enough spillover, or a high enough referral rate (which gives the platform a stake in the seller's sales and so a reason to invest more effort), makes entry welcome. In the competition intensity the regime is not monotone. The seller welcomes entry when products are well differentiated, opposes it at intermediate $\beta$, and can welcome it again near perfect substitutes. The paper's later results on the seller's optimal effort and on entry deterrence (Proposition 3 onward) are stated separately inside and outside $\Omega$, so this classification is their starting point.

Formalizing it. The result is proved in the paper, and nothing about it is machine-checked yet. Its proof leans on "one can verify" claims about quartic polynomials on a box: the positivity of $D$, of the platform's effort and of $S_2$ under (5), and the sign patterns of (11). A formal proof checks each of them. The mission also ties the closed forms (6)–(7) to an explicit game, with equilibria defined as best responses, so the comparison is between equilibrium profits and not between formulas taken on trust.

Difficulty

The first part of the goal is immediate once (6)–(7) are known, since $\Pi^S_E - \Pi^S_N = (H - \tfrac14)(1-f)(a+e_S)^2$. The content lies elsewhere.

• The equilibrium analysis. The platform's payoff includes the referral fee on the seller's revenue, so its best-response slope is $\beta(1+f)/2$, not the textbook $\beta/2$. The seller's quantity has a corner at zero. The platform's effort problem must be solved against every equilibrium after every deviation, and it reduces to a single variable only after uniqueness in Lemma 1.
• Polynomial sign conditions. Positivity of $D$ and $S_2$ under (5), and the threshold structure of (11) in each variable, are statements about polynomials of degree up to four on a box with the semialgebraic side condition (5).
• A step the paper omits. $\Omega$ is defined through $H$, and $H = 0$ off (5). Moving Lemma 3's thresholds from (11) to $\Omega$ therefore also needs "(11) $> 0$ implies (5)", which the paper does not state. It holds numerically: on a $201^3$ grid, wherever (11) is positive the left side of (5) is above $1.01$. A complete proof of the goal must supply it.

Formalization scope

All quantities are real numbers. The parameters are explicit arguments, and the standing ranges $\delta\in[0,1]$, $f\in[0,1)$, $\beta\in[0,1]$ are a hypothesis InBox δ f β. Every polynomial ($N_5$, $D$, the numerator of $e^*_P$, (11), $S_2$) is written term for term as printed. $H$ keeps the case split of (8), so $\Omega$ is false wherever (5) fails. Conventions:

• Defined from the game: the quantity equilibrium (a pure Nash equilibrium over nonnegative quantities, through the published general two-player definition CompetingChains.Cournot.IsPureNash), the entry equilibrium (the platform's effort $e_P \ge 0$ is a global maximizer against every equilibrium after every deviation), and the stage-1 and no-entry problems.
• The paper's closed forms: $H$, $\Omega$, $\Pi^S_N$ and $\Pi^S_E$. Milestone 3 proves that the closed forms equal the equilibrium profits.
• "Optimal" means a global maximizer, ties allowed.
• The platform's effort is nonnegative. The seller's effort $e_S$ is any real number, as in the paper.
• Lemmas 1–2 assume $a + e_S > 0$ (a positive product value), and Lemma 2 assumes (5), the paper's standing assumption.
• Only the branch of Lemma 2 under (5) is formalized.
• The goal's first part assumes $a + e_S \ne 0$. At $a + e_S = 0$ both profits equal $-c_S e_S^2$ and no strict preference exists.
• Condition (5) is not a hypothesis of the goal.

The first part of the goal is near-definitional given (6)–(7). The mission's content is the threshold structure of $\Omega$ and milestones 1–3, which make (6)–(7) the equilibrium profits. A formalization in which the thresholds may depend on the varying parameter, or in which $\Omega$ is taken as $\{(11) > 0\}$ by definition, would not be this theorem.

A complete development needs real polynomial inequalities on boxes (nlinarith/polyrith-style certificates or interval arguments) and elementary concave maximization. A uniqueness lemma for two-player games whose best responses have slopes with product below one would be reusable for other differentiated Cournot models. Contributions are welcome for any milestone, for the step "(11) $> 0$ implies (5)", and for proofs of the sign lemmas by certificates.

Selected references

• L. Qi, H. Song, W. Xiao, Coopetition in Platform-Based Retailing: On the Platform's Entry, Management Science, 2025. https://doi.org/10.1287/mnsc.2023.00260 (formalized from the authors' manuscript with Online Supplement, 2024-08-03).
• F. Zhu, Q. Liu, Competing with complementors: An empirical look at Amazon.com, Strategic Management Journal 39(10), 2018. https://doi.org/10.1002/smj.2932
• N. Singh, X. Vives, Price and quantity competition in a differentiated duopoly, RAND Journal of Economics 15(4), 1984. https://doi.org/10.2307/2555525

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

In a Bayesian multi-armed bandit a decision maker pulls one of $K$ arms in each of $T$ periods, observes the reward, and updates a prior belief about each arm's unknown parameter. The best achievable expected total reward, $V^*(T, y)$, is the value of a dynamic program over beliefs, and for all but the smallest instances it cannot be computed. Upper bounds on $V^*$ are therefore the yardsticks against which heuristics such as Thompson sampling (TS) are measured: the gap between a policy's performance and an upper bound certifies how far the policy can be from optimal.

The conventional benchmark is the expected total reward of a clairvoyant who knows the arms' parameters, $W^{TS}(T, y) = \mathbb E_y[T \max_a \mu_a(\theta_a)]$, the quantity behind every Bayesian regret bound. Min, Maglaras and Moallemi (arXiv:1902.04251v2, Management Science 2025) apply the information relaxation duality of Brown, Smith and Sun (Operations Research 2010) to the bandit: a clairvoyant who sees the whole future but pays a penalty for using it. Each penalty yields a performance bound $W^z(T,y)$ and a randomized policy (IRS, "information relaxation sampling"); the zero-information penalty recovers TS and $W^{TS}$, the ideal penalty recovers $V^*$. The paper's Theorem 2 shows that its intermediate penalties give bounds that are provably tighter than $W^{TS}$. This mission formalizes that theorem.

Setting

Let $\mathcal A = \{1, \dots, K\}$, $K \ge 1$. Arm $a$ has an unknown parameter $\theta_a$; given $\theta_a$, its rewards $R_{a,1}, R_{a,2}, \dots$ are i.i.d. with law $\mathcal R_a(\theta_a)$. The parameter has a prior $\mathcal P_a(y_a)$ from a conjugate family indexed by a belief $y_a$, and the Bayesian update $\mathcal U_a(y_a, r)$ is the belief after a reward $r$: if $\theta_a \sim \mathcal P_a(y_a)$ then $\theta_a \mid R_{a,1} \sim \mathcal P_a(\mathcal U_a(y_a, R_{a,1}))$. The outcome $\omega = (\theta, (R_{a,n})_{a,n})$ has law $\mathcal I(y)$, under which arms are independent. Throughout, $\mathbb E_{y_a}|R_{a,1}| < \infty$ for every belief.

The conditional and predictive mean rewards are $\mu_a(\theta_a) = \mathbb E[R_{a,n} \mid \theta_a]$ and $\bar\mu_a(y_a) = \mathbb E_{y_a}[\mu_a(\theta_a)]$, and the posterior predictive mean after $n$ rewards of arm $a$ is $\hat\mu_{a,n} = \mathbb E_{y_a}[\mu_a(\theta_a) \mid R_{a,1}, \dots, R_{a,n}]$. With $\mathcal N_T = \{n \in \mathbb N_0^K : \sum_a n_a = T\}$ and $S_a(n) = \sum_{i=1}^{n} \hat\mu_{a,i-1}$, the four bounds compared are

$$W^{TS}(T,y) = \mathbb E_y\Big[T\max_a \mu_a(\theta_a)\Big], \qquad W^{IRS.FH}(T,y) = \mathbb E_y\Big[T\max_a \hat\mu_{a,T-1}\Big],$$ $$W^{IRS.V\text{-}Zero}(T,y) = \mathbb E_y\Big[\max_{n\in\mathcal N_T} \sum_a S_a(n_a)\Big], \qquad W^{IRS.V\text{-}EMax}(T,y) = \mathbb E_y\Big[\max_{a_{1:T}} \sum_{t=1}^T \big(r_t - z_t^{IRS.V\text{-}EMax}\big)\Big].$$

In the last one the clairvoyant chooses a whole action sequence $a_{1:T}$ knowing $\omega$, and at time $t$ receives the conditional expected reward $\bar\mu_{a_t}$ under the current belief $y_{t-1}$, minus $W^{TS}(T-t, y_t)$, plus the expectation of $W^{TS}(T-t, y_t)$ given the history $H_{t-1}$. A supersolution is a function $\hat V(T, y)$ with $\hat V(0, y) = 0$ and $\hat V(T, y) \ge \mathbb E_{y_a}[R_{a,1} + \hat V(T-1, \mathcal U(y, a, R_{a,1}))]$ for all $T \ge 1$, $y$, $a$ (Definition 2).

Formalization targets

Goal: Theorem 2 (p. 25)

$$W^{TS}(T,y) \ge W^{IRS.FH}(T,y) \ge W^{IRS.V\text{-}Zero}(T,y), \qquad W^{TS}(T,y) \ge W^{IRS.V\text{-}EMax}(T,y),$$

for every horizon $T$ and every belief vector $y$ of every conjugate model satisfying the standing assumptions.

Milestones (Appendix D.3)

1. $W^{TS} \ge W^{IRS.FH}$, (124).
2. Lemma 1, a variant of Jensen's inequality: for non-decreasing $\varphi$, $\mathbb E[\max\{X+\varphi(X),0\}] \ge \mathbb E[\max\{\mathbb E X+\varphi(X),0\}]$.
3. Corollary 1, its version conditional on a sub-$\sigma$-field $\mathcal H$.
4. Corollary 2, the form for a maximum of affine functions $(i-n)^+X + C_i$ with $\mathcal H$-measurable $C_i$.
5. (155): the interpolating expectations $U_{k,n}$ of (154) decrease in $n$, with $W^{IRS.FH} = U_{1,0}$, $W^{IRS.V\text{-}Zero} = U_{K,T}$ and $U_{k+1,0} = U_{k,T}$.
6. Lemma 2 (Theorem 4 of Desai, Farias and Moallemi): a supersolution $\hat V$ bounds the inner problem of its own penalty outcome by outcome, hence $W^{\hat z} \le \hat V$.
7. (176)–(180): $W^{TS}$ is a supersolution.

Significance

The result. Theorem 2 says that the penalties IRS.FH and IRS.V-Zero, which only require sampling a future and solving a deterministic allocation problem, produce upper bounds on $V^*$ that are never looser than the regret benchmark $W^{TS}$, and that IRS.V-EMax is too. A bound below $W^{TS}$ gives a sharper certificate of suboptimality for any policy, and the paper's experiments (§5) report these bounds next to the policies' performance. The ordering also organises the paper's family of policies: the bounds move monotonically from the TS benchmark towards the optimal value.

Formalizing it. The theorem is proved in the paper (Appendix D.3); it has no machine-checked proof. A formal development checks three different mechanisms: conditional Jensen for (124); a one-arm-at-a-time interpolation through $U_{k,n}$, driven by a non-standard Jensen-type inequality (Lemma 1, Corollaries 1–2), for (57); and the supersolution argument of Desai et al. for (58). The paper's own remark (pp. 59–60) shows that the middle inequality does not follow from the general "finer information gives a weaker bound" principle of Brown et al.; formalization fixes exactly which properties of the bandit (conjugacy, independence of arms, the martingale property of $\hat\mu_{a,n}$) carry the argument.

Difficulty

The obvious route to $W^{IRS.FH} \ge W^{IRS.V\text{-}Zero}$ is to observe that IRS.FH conditions on more information ($T-1$ rewards of every arm) than IRS.V-Zero (only the history so far) and invoke monotonicity of dual bounds in the relaxation. That argument fails: the two penalties are not generated by a common function, and the paper exhibits a modified bandit (163)–(165) in which the inequality reverses. The interpolation must instead trade one arm's realized cumulative payoff for a constant per-pull payoff one pull at a time, and each step needs Corollary 2, where conditioning acts inside a maximum of affine functions; ordinary Jensen points the wrong way there.

For (58), the difficulty is that the payoff of the penalised inner problem depends on the whole outcome along an adaptively chosen action sequence; the bound must hold uniformly over all $K^T$ sequences, which is why it is proved pathwise by backward induction rather than in expectation.

Formalization scope

Arms are Fin K (0-based) with [NeZero K]. All arms share one parameter type $\Theta$ (standard Borel, nonempty) and one belief type $Y$, the disjoint unions of the per-arm ones. Rewards are a Kernel Θ ℝ per arm, priors a Kernel Y Θ per arm, both Markov. The outcome is Fin K → Θ × (ℕ → ℝ) with law the product over arms of $\theta_a \sim \mathcal P_a(y_a)$ followed by an i.i.d. reward sequence. The standing assumptions are one predicate: conjugacy (the update agrees a.e. with Mathlib's posterior of the reward kernel), joint measurability of each $\mathcal U_a$, and $\mathbb E_{y_a}|R_{a,1}| < \infty$ for every belief, (3). $\hat\mu_{a,n}$ is the conjugate (pathwise) version $\bar\mu_a(y_{a,n})$ of the conditional expectation (10). $W^{IRS.FH}$ is defined by its closed form (33). In the penalties (26) and (168) the conditional expectations given $H_{t-1}$ are replaced by their conjugate closed forms: $\mathbb E[r_t \mid H_{t-1}] = \hat\mu_{a_t, n_{t-1}(a_t)}$, and the expectation of $\hat V(T-t, y_t)$ is the integral over the predictive law of the next reward. The supersolution predicate requires the expectation in (166) to exist. Lemma 1 and Corollary 1 compare lower Lebesgue integrals in $[0,\infty]$; Corollary 1 adds joint measurability of $\varphi$; Corollary 2 assumes the $C_i$ integrable; Lemma 2's integral form assumes the pathwise maximum integrable.

Trivializations ruled out. No expectation in a goal can silently be a junk $0$: the standing integrability makes every bound an honest integral, and Lemma 1 and Corollary 1 are stated with lower integrals. $W^{IRS.V\text{-}EMax}$ is the penalised clairvoyant value of the penalty generated by $W^{TS}$, not $W^{TS}$ itself or the closed form (41) substituted into it. The standing assumptions are satisfiable (a sorry-free check with a one-point parameter space is in the development).

A complete development needs: conjugate updating along reward sequences and the martingale property of $\hat\mu_{a,n}$ (Remark 1); measurability of $\theta \mapsto \bigotimes_n \mathcal R_a(\theta)$; independence of arms under $\mathcal I(y)$; conditional Jensen for finite maxima. Lemma 1, Corollaries 1–2 and Lemma 2 are reusable beyond this mission. Contributions of any milestone, or of the infrastructure lemmas above, are welcome.

Selected references

• S. Min, C. Maglaras, C. C. Moallemi, Thompson Sampling with Information Relaxation Penalties, Management Science, 2025; preprint arXiv:1902.04251v2, 2021. https://arxiv.org/abs/1902.04251
• D. B. Brown, J. E. Smith, P. Sun, Information Relaxations and Duality in Stochastic Dynamic Programs, Operations Research 58(4), 2010. https://doi.org/10.1287/opre.1090.0796
• V. V. Desai, V. F. Farias, C. C. Moallemi, Bounds for Markov Decision Processes, in F. L. Lewis and D. Liu (eds.), Reinforcement Learning and Approximate Dynamic Programming for Feedback Control, Wiley/IEEE Press, pp. 452–473, 2012 (the paper's Desai et al. 2012a; Theorem 4 there is Lemma 2 here).
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4), 2014. https://doi.org/10.1287/moor.2014.0650

Motivation

The European Union's General Data Protection Regulation (GDPR, in force since 2018) requires a firm to obtain a consumer's explicit opt-in consent before it collects her personal data. Most of the economic literature reads such consent rules as a cost to data-driven firms. Choe, Matsushima and Shekhar (ISER Discussion Paper No. 1246, Osaka University, June 2024; published in Management Science, 2025, doi:10.1287/mnsc.2024.06653) ask what happens to the price of a digital service when consumers gain the right to buy it without sharing data. Their model is a monopoly with two-dimensional consumer heterogeneity, simple enough to be solved in closed form, and it lets the answer be stated for every value of the firm's opt-in benefit and every mix of usage-based and data-based revenue.

This mission formalizes the paper's general price comparison, Proposition A1: the equilibrium price is higher after the GDPR.

Setting

A monopolist sells an online service at zero marginal cost and price $p \in \mathbb{R}$. A consumer has a type $(v, c) \in [0,1]^2$, where $v$ is her valuation for the service and $c$ her privacy cost of sharing data; types are independent and uniform on $[0,1]^2$, so the mass of a set of consumers is its area. A consumer who shares data receives an opt-in benefit $x \in (0, 1)$, and the firm earns an exogenous data revenue $\alpha \ge 0$ per unit of shared data.

The utilities of opt-in purchase (buy and share) and opt-out purchase (buy without sharing) are

$$U_S(v,c) = v + (x - c) - p, \qquad U_N(v,c) = v - p.$$

• Before the GDPR opt-out purchase is unavailable. A consumer buys, and shares data, iff $U_S \ge 0$. The demand $\widehat D(p)$ is the area of $\{(v,c) \in [0,1]^2 : c \le v + x - p\}$, and the profit is $\widehat\Pi(p) = (p + \alpha)\widehat D(p)$.
• After the GDPR a consumer opts in iff $U_S \ge \max\{U_N, 0\}$ and opts out iff $U_N \ge \max\{U_S, 0\}$. The opt-in set is $\{c \le v + x - p,\ c \le x\}$, the opt-out set is $\{v \ge p,\ c > x\}$, their areas are $\widetilde D_S(p)$ and $\widetilde D_N(p)$, and the profit is $\widetilde\Pi(p) = p\,(\widetilde D_S(p) + \widetilde D_N(p)) + \alpha\,\widetilde D_S(p)$.

The firm chooses the price first and consumers respond, so the equilibrium price in each regime is a maximizer over $\mathbb{R}$ of the corresponding profit: $\hat p^\star$ for $\widehat\Pi$ and $\tilde p^\star$ for $\widetilde\Pi$. The paper's appendix expresses them through the thresholds

$$\alpha_1(x) = \max\Big\{\tfrac{1-2x}{2}, 0\Big\}, \qquad \alpha_2(x) = \max\Big\{\tfrac{2-4x+x^2}{2x}, 0\Big\}$$

and the radicals $\beta = \sqrt{6 + (x+\alpha-1)^2}$, $\Gamma = \sqrt{6 + (2-2x+\alpha)^2}$.

Formalization targets

Goal: Proposition A1 (p. 34)

For every $0 < x < 1$ and $\alpha \ge 0$, both profits attain a global maximum on $\mathbb{R}$, and every pair of maximizers satisfies

$$\tilde p^\star > \hat p^\star.$$

Milestones

1. Display (4) (p. 11): $\widehat D(p) = (1+x-p)^2/2$ for $x < p < 1+x$, and $1 - (1-x+p)^2/2$ for $x-1 \le p \le x$.
2. Display (5) (p. 14): $\widetilde D_S(p)$ equals $(1+x-p)^2/2$, $x^2/2 + x(1-p)$ or $x - p^2/2$ on $(1, 1+x)$, $(x, 1]$, $[0, x]$.
3. Display (6) (p. 14): $\widetilde D_N(p) = (1-x)(1-p)$ for $0 \le p \le 1$, and $0$ for $1 < p < 1 + x$.
4. Online Appendix A.1 (OA p. 2): $\hat p$ maximizes $\widehat\Pi$ iff $\hat p = (1+x-2\alpha)/3$ when $\alpha < \alpha_1(x)$ and $\hat p = (2(x-1) - \alpha + \beta)/3$ otherwise.
5. Online Appendix A.2 (OA p. 4): $\tilde p$ maximizes $\widetilde\Pi$ iff $\tilde p = (2(1-\alpha x) + x^2)/4$ when $\alpha < \alpha_2(x)$ and $\tilde p = (\Gamma - (2 - 2x + \alpha))/3$ otherwise.
6. p. 14: $\alpha_1(x) \le \alpha_2(x)$ for all $x \in (0,1)$.
7. Lemma A3 (pp. 33–34): the three possible pairs of equilibrium regimes (case 1a/2a, 1b/2a, 1b/2b), located by price intervals.
8. Online Appendix D, first display (OA p. 7): the closed form of $\tilde p^\star - \hat p^\star$ in each of the three regions.

Significance

The result. Proposition A1 says the price rise is robust: it holds for every opt-in benefit and every revenue model, from a firm that earns nothing from data ($\alpha = 0$) to one whose data revenue dominates. The paper's welfare results (on demand, profit and consumer surplus) are comparisons of the same two equilibria, and the price comparison is the one among them that holds uniformly; the others change sign with $(x, \alpha)$ and are established in the paper only numerically. The main text's Proposition 1 is the instance $x = 1/4$.

Formalizing it. The paper's proof is a chain of closed-form computations spread over the appendix and online appendix: areas of polygons, the maximization of piecewise cubic profits over all of $\mathbb{R}$, and a sign argument with nested square roots. Several steps are stated as "one can verify", and the online appendix contains printed slips (a derivative written with respect to the wrong variable in §D, a pair of cases listed incorrectly on p. 14). A machine-checked proof turns the chain into a verified one. The milestones isolate the parts that are reusable on their own: the demand formulas (4)–(6) and the closed-form equilibria, on which the paper's companion profit comparison (Proposition A3) also rests. None of these results has been formalized before.

Difficulty

The obvious route, solving the first-order condition on each demand piece, gives candidates, not maximizers. The profits are only piecewise smooth, the pieces meet at $p = x$ and $p = 1$, and the price ranges over all of $\mathbb{R}$, including negative prices before the GDPR. Showing that the candidate is the unique global maximizer requires comparing values across pieces and controlling the profit outside the paper's displayed price ranges. The comparison step is the second difficulty: in the middle region $\alpha_1(x) \le \alpha < \alpha_2(x)$ the gap $(14 + 4\alpha + 3x^2 - 8x - 6x\alpha - 4\beta)/12$ mixes a polynomial with a square root, and its positivity is not a one-line estimate. The gap tends to $0$ as $x \to 1$, so no uniform margin is available.

Formalization scope

• Types are pairs q : ℝ × ℝ with q.1 = v, q.2 = c; the type square is Set.Icc 0 1 ×ˢ Set.Icc 0 1, and every demand is (volume S).toReal for the Lebesgue measure on ℝ × ℝ.
• The after-GDPR sets are copied from p. 13; they send the tie $U_S = U_N \ge 0$ to opt-in, which changes only a null set.
• Profits are functions ℝ → ℝ of the price, and an equilibrium price is IsMaxOn profit Set.univ p. The price is never restricted to the paper's case ranges, and $\tilde p^\star \ge 0$ is a consequence, not an assumption.
• Standing assumptions on every theorem: $0 < x$, $x < 1$, $\alpha \ge 0$ (pp. 7–8). The data revenue is written α in Lean.
• "Case 1a/1b/2a/2b equilibrium" means the maximizer lies in $(x, 1+x)$, $[x-1, x]$, $(x, 1+x)$, $[0, x]$ respectively.
• The thresholds $\alpha_1, \alpha_2$ and radicals $\beta, \Gamma$ are plain definitions with the paper's formulas.

A formalization that compares the two closed-form prices instead of maximizers of the modelled profits, that asserts a property of "every maximizer" without proving one exists, or that restricts prices to a bounded interval, would not state Proposition A1; the goal and the milestones rule all three out. Results of the paper established only numerically (Propositions 2–4, A2, the second and third bullets of A3, A4) are not posed, and neither are the comparative statics of Lemmas A1–A2.

A complete development needs areas of polygons under the Lebesgue measure on $\mathbb{R}^2$ (via MeasureTheory.volume_regionBetween or Fubini), elementary calculus on piecewise polynomials, and inequalities with square roots. The demand computations and the global-maximization arguments are reusable for the companion mission on the paper's profit comparison. Contributions of any milestone, or of further intermediate lemmas such as the continuity of the demands in the price, are welcome.

Selected references

• C. Choe, N. Matsushima, S. Shekhar, The Bright Side of the GDPR: Welfare-Improving Privacy Management, ISER Discussion Paper No. 1246, Osaka University, June 2024 (the version formalized; theorem and page numbers refer to it).
• C. Choe, N. Matsushima, S. Shekhar, The Bright Side of the GDPR: Welfare-Improving Privacy Management, Management Science, 2025. https://doi.org/10.1287/mnsc.2024.06653
• Regulation (EU) 2016/679 (General Data Protection Regulation), Official Journal of the European Union L 119, 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj

Motivation

Online advertising lets a firm aim its messages at the consumers most likely to want its product, but the data behind that aim is noisy: a platform's prediction of who belongs to a demographic or interest segment is right only with some probability. A natural expectation is that sharper targeting raises firms' profits, since fewer messages are wasted. Karle and Reisinger (SSRN 4626076, March 2024; published in Management Science, doi:10.1287/mnsc.2023.03632) show that this can fail: when both firms chase the same valuable consumers, better targeting also increases the number of consumers who see both firms' advertisements, which intensifies price competition.

The model combines a targeting stage with the clearinghouse price-competition model of Varian (1980) and Narasimhan (1988), in which some consumers are informed about one firm only (loyal consumers) and others about both (shoppers), and equilibrium prices are dispersed. This mission formalizes the paper's result for costless advertising: industry profit first falls as targeting improves, then jumps up when firms switch to segmenting the market, then stays flat.

Setting

There are two consumer groups $a$ and $b$, each of mass one. Group-$b$ consumers value the product at $1$, group-$a$ consumers at $A$, with $0 < A < 1$. Two firms produce at zero cost. For every consumer each firm receives a signal of the consumer's group that is correct with probability $\alpha \in (1/2, 1]$, independently across firms. Only consumers of the group a firm targets are interested in its product.

Stage 1. Each firm chooses a target group $k \in \{a, b\}$ and a message scope: expected (message only the consumers its signal places in group $k$, which reaches a mass $\alpha$ of group $k$) or all (message every consumer, which reaches all of group $k$). Messages cost $c \ge 0$ each; in this mission $c = 0$.

Stage 2. Having observed stage 1, firms set prices. For a stage-1 profile $s$, if both firms target the same group, the shoppers $S(s) = r_1 r_2$ are the targeted consumers reached by both, where $r_i \in \{\alpha, 1\}$ is firm $i$'s reach; firm $i$'s loyal mass is $L_i(s) = r_i - S(s)$. If they target different groups, $S(s) = 0$ and $L_i(s) = r_i$. A consumer buys if the price does not exceed her valuation; shoppers buy from the cheaper firm and split equally on ties. Firm $i$'s profit at prices $(p, q)$ is $p\,(L_i + S)$, $p\,(L_i + S/2)$ or $p\,L_i$ according as $p < q$, $p = q$ or $p > q$, and $0$ if $p$ exceeds the valuation.

Firms may randomize prices: a price strategy is a probability measure on $[0,1]$, and $U_i(s; \mu, \nu)$ is firm $i$'s expected profit. A subgame perfect Nash equilibrium (SPNE) is a pure stage-1 profile $s^\star$ and a continuation that assigns to each of the sixteen stage-1 profiles a Nash equilibrium of its pricing subgame, such that no firm gains at stage 1 by changing its action. The sum of expected profits is $V_1(s^\star) + V_2(s^\star)$.

Two cumulative distribution functions appear, on $[1-\alpha, 1)$:

$$F(p) = \frac1\alpha - \frac{1-\alpha}{\alpha p}, \qquad H(p) = \frac{p - (1-\alpha)}{p},$$

both $0$ below $1-\alpha$ and $1$ from $1$ on, so $H$ has an atom $1 - \alpha$ at $p = 1$. The thresholds are $\hat\alpha_1(A) = 1 - A$ and $\hat\alpha_2(A) = \bigl(1 + \sqrt{1 - 4A}\bigr)/2$.

Formalization targets

Goal: Proposition 2 (p. 15)

For $0 < A < 1/4$: $1/2 < \hat\alpha_2(A) < \hat\alpha_1(A)$; for every $\alpha \in (1/2, \hat\alpha_2(A))$ there is an SPNE with

$$\textstyle\sum_i E[\pi_i^\star(\alpha)] = 1 - \alpha^2,$$

which is strictly decreasing in $\alpha$; for every $\alpha \in (\hat\alpha_2(A), 1]$ there is an SPNE with sum $1 + A$; and $1 - \hat\alpha_2(A)^2 < 1 + A$ (the upward jump).

Milestones

1. Display (1), p. 11. If both firms target $b$ and message expected consumers, both pricing by $F$ is an equilibrium with profit $\alpha(1-\alpha)$ each.
2. Lemma 2 part 1, display (2), pp. 14–15. If firm 1 messages expected and firm 2 all group-$b$ consumers, $(F, H)$ is an equilibrium with profits $\alpha(1-\alpha)$ and $1-\alpha$.
3. Bertrand, p. 13. If both message all group-$b$ consumers, pricing at $0$ is an equilibrium with zero profits.
4. Segmentation, pp. 9, 13. If firm 1 targets $a$ and firm 2 targets $b$, prices $A$ and $1$ are an equilibrium.
5. Threshold, p. 14. For $\alpha \in (1/2, 1]$ and $A \le 1/4$: $\alpha(1-\alpha) \ge A \iff \alpha \le \hat\alpha_2(A)$.
6. Footnote 36, p. 15. $\hat\alpha_2(A) < \hat\alpha_1(A)$ for $0 < A < 1/4$.
7. Lemma 2, pp. 14–15. The SPNE with $c = 0$ in both regimes.

Significance

The proposition shows that the non-monotonicity of industry profit in targeting precision, which the paper first derives for high advertising costs, does not rely on advertising being costly. With free messages a firm could inform every consumer, which is equivalent to perfect targeting; the equilibrium instead has one firm refrain from doing so, because the resulting asymmetry keeps prices high. For regulation of consumer data and for platforms selling targeting precision, the result says that better targeting technology can lower sellers' profits over a range of precisions and raise them discontinuously elsewhere.

The result is proved in the paper (main text and Online Appendix A). It has not been machine-checked. Formalizing it means verifying mixed-strategy equilibria of a pricing game with a continuum of prices, including an atom at the valuation, in all sixteen subgames of a two-stage game, a pattern that recurs throughout the clearinghouse and price-dispersion literature.

Difficulty

The stage-1 comparison is arithmetic once the stage-2 payoffs are known; the work is in the pricing subgames. Each mixed equilibrium must be verified against every real price deviation, which needs the expected profit at price $p$ against a distribution with an atom, where the tie-splitting rule matters exactly at the atom. Subgame perfection requires a pricing equilibrium in every off-path subgame too, including those where both firms target group $a$ (the group-$b$ equilibria rescaled by $A$) and the Bertrand subgames. The obvious shortcut, assigning each subgame its textbook profit as a number, is not available: the stage-1 values are defined as integrals against the equilibrium strategies.

Formalization scope

Lean 4 with Mathlib. The pricing game is a separate definition (a general clearinghouse duopoly with valuations $v_i$, loyal masses $L_i$ and shopper mass $S$); the targeting game builds on it. Committed conventions:

• price strategies are probability measures on $\mathbb R$ with no mass outside $[0,1]$; expected profits are Bochner integrals; deviations range over all real prices;
• a consumer buys at a price equal to her valuation (the page says "lower than"; the atom of $H$ at $1$ needs the sale);
• targeting is in pure strategies (the paper's footnotes 26 and 34); the message scope is binary, the paper's options (1) and (2); the no-message option and the continuous message masses of the appendix proof are not modelled;
• cdfs are Mathlib's ProbabilityTheory.cdf; statements about all measures with cdf $F$ also assert that such a measure exists;
• the paper's "firm $i$ / firm $-i$" are firm 1 (the expected-only firm, and the group-$a$ firm) and firm 2;
• for $A > 1/4$ Lean's square root gives $\hat\alpha_2(A) = 1/2$, the reading Lemma 2's range $(\max\{1/2, \hat\alpha_2(A)\}, 1]$ needs;
• pricing-stage profits exclude the sunk message cost; the goal and Lemma 2 are at $c = 0$.

The goal is Proposition 2 in existence form: it asserts an SPNE with the stated total. The paper exhibits that equilibrium; uniqueness of equilibrium payoffs is not claimed. Propositions 1 and 3 (high and general costs) are not posed. Trivializing encodings are excluded by construction: stage-1 values are integrals of the continuation strategies, not a table; the equilibrium condition quantifies over all sixteen subgames, not just the path; strategies are probability measures on $[0,1]$, so no integral takes a junk value; and statements quantifying over measures with a given cdf include the existence of one.

Contributions welcome: integration of the tie-split profit against cdfs with atoms, a reusable lemma that a clearinghouse with given loyal and shopper masses has an equilibrium, and the rescaling of equilibria by the valuation.

Selected references

• H. Karle and M. Reisinger, Imperfect Targeting and Advertising Strategies, SSRN working paper 4626076, March 25, 2024. https://ssrn.com/abstract=4626076 ; published in Management Science, 2024. https://doi.org/10.1287/mnsc.2023.03632
• H. R. Varian, A Model of Sales, American Economic Review 70(4), 651–659, 1980. https://www.jstor.org/stable/1805229
• C. Narasimhan, Competitive Promotional Strategies, Journal of Business 61(4), 427–449, 1988. https://doi.org/10.1086/296442