Operations Research

Why the final licensing choice matters

A component supplier can influence a product market through both the wholesale price it charges and the technology its customers may share. Wang, Huang and Lee study a supply chain with one upstream supplier and two downstream manufacturers that invest in product quality and then compete in quantities. A cross-licensing policy lets each manufacturer use some of the other's innovation. The supplier may promise a policy before the investments, or leave the decision until after the investments and wholesale price are fixed. The latter choice creates a precise comparison: at that final stage, does permitting cross-licensing reduce the supplier's revenue? The authors answer it in Proposition 1 of their SSRN manuscript, version of 2023-04-27. Its proof is in the attached appendix, p. A.1.

This mission concerns that final-stage comparison. It is one part of the paper's broader study of how a supplier's licensing commitment affects manufacturers' innovation incentives and downstream market structure. The later innovation and initial-contract comparisons are separate questions. Here, investments and wholesale price are fixed, so the result isolates the direct quantity-market effect of licensing at the moment the supplier chooses its policy.

The downstream quantity game

Manufacturers $M_1$ and $M_2$ have already selected nonnegative innovation levels $T_1$ and $T_2$, with $T_1\le T_2$ in the presentation of equations (2) and (3). Each chooses a nonnegative production quantity $q_i$. The wholesale price $r$ is the amount each manufacturer pays the common supplier for one unit. The market-size intercept is normalized to one and per-unit manufacturing cost to zero. If licensing effectiveness is $\beta\in[0,1]$, manufacturer $i$ receives a quality improvement $T_i+\beta T_j$; $\beta=0$ represents no cross-licensing. Its inverse demand is $1+T_i+\beta T_j-q_1-q_2$. These are the model's conventions on pp. 9–10.

At fixed $T_1,T_2,\beta,r$, the manufacturers play a simultaneous quantity game. Their respective profits are

$$\Pi_1(q_1;q_2)=(1+T_1+\beta T_2-q_1-q_2-r)q_1, \qquad \Pi_2(q_2;q_1)=(1+T_2+\beta T_1-q_1-q_2-r)q_2.$$

A Nash equilibrium is a pair $(q_1,q_2)\in[0,\infty)^2$ for which neither manufacturer increases its profit by changing its own nonnegative quantity while the other's quantity stays fixed. The supplier's profit at a quantity profile is $r(q_1+q_2)$. The supplier's comparison must therefore account for the manufacturers' responses under each licensing policy; it cannot compare profit at an arbitrary fixed quantity pair.

Formalization targets

The first milestone gives the exact equilibrium quantities of equation (2). Write $r_1=1+T_1(2-\beta)-T_2(1-2\beta)$ and $r_2=1+\beta T_1+T_2$. For $r\le r_1$ both manufacturers can sell; for $r_1<r\le r_2$ only $M_2$ sells; above $r_2$ neither sells. The statement characterizes every equilibrium and thereby gives existence and uniqueness across the two threshold boundaries, including the cases where a manufacturer's equilibrium quantity is zero.

The second milestone identifies the supplier's revenue at an equilibrium with the piecewise expression $\pi_s^{\mathrm{cl}}(r)$ in equation (3). Setting $\beta=0$ in that expression gives the paper's no-licensing expression $\pi_s^{\mathrm n}(r)$ in equation (4). This milestone links the paper's algebraic profit comparison to the strategic quantity game, while keeping the equilibrium property as the premise.

The goal is the supplier's ex-post preference in Proposition 1. If $q^{\mathrm{cl}}$ is any equilibrium with licensing effectiveness $\beta$ and $q^{\mathrm n}$ is any equilibrium at $\beta=0$, then both equilibria exist and

$$r\bigl(q^{\mathrm n}_1+q^{\mathrm n}_2\bigr) \le r\bigl(q^{\mathrm{cl}}_1+q^{\mathrm{cl}}_2\bigr) \qquad(0\le\beta\le1,\;0\le T_1\le T_2,\;r\ge0).$$

This weak inequality is intentional. At $\beta=0$ the two games coincide, and there are other parameter values at which the profits tie. The comparison holds at the same innovation levels and the same wholesale price; it is not a comparison after re-optimizing the supplier's price or the manufacturers' investment decisions.

What the result establishes

For fixed investments and price, the supplier need not lose revenue by enforcing cross-licensing after observing the manufacturers' innovation. This gives mathematical content to the paper's claim that, without an initial commitment, the supplier will choose to enforce licensing at the final contract stage. The model does not specify a separate final-contract bargaining game, so the formal goal is the profit comparison that supports that interpretation. The result does not settle whether committing to licensing before innovation is preferable: changing the initial policy can change the innovation levels themselves, which the ex-post comparison holds fixed.

The authors prove Proposition 1 by comparing the supplier-profit expressions (3) and (4) in the manuscript's appendix. A machine-checked development would additionally secure the connection from the manufacturers' Nash conditions to those expressions, including the monopoly and zero-sales regimes. These statements are currently posed as open formalization targets; a Lean file with sorry only checks that the statements are well formed, not that the paper's argument has been verified by Lean. The general two-player Nash definition can be reused for other real-strategy games; the payoff and threshold definitions are specific to this supply chain.

Where the argument has to account for cases

The quantity equilibrium changes form as the wholesale price crosses $r_1$ and $r_2$. An argument confined to the two-selling-firms region misses cases in which $M_1$ sells nothing, or neither manufacturer sells. Comparing only the duopoly formulas cannot establish an inequality at every nonnegative price. The first milestone therefore covers all three regimes, and the goal compares the profits of actual equilibria. The fact that $T_2\ge T_1$ orders the possible monopoly toward $M_2$ under the paper's chosen labels; a formulation that silently assumes both equilibrium quantities are strictly positive would lose part of Proposition 1.

Formalization scope

All parameters and quantities are real. The permitted quantity strategies and wholesale prices are nonnegative. The paper treats $r$ as a wholesale price without writing a bound in Proposition 1; $r\ge0$ is made explicit because a negative price can reverse the supplier-profit inequality. The innovation ordering $0\le T_1\le T_2$ is the convention immediately preceding equation (2). Licensing effectiveness lies in $[0,1]$. Innovation costs $k_iT_i^2$ and the paper's bound $k_2>49/144$ are unnecessary once innovation levels are fixed, so they do not enter this mission's statements.

The formalization uses an explicit pair $(q_1,q_2)$, with the first coordinate for $M_1$. The quantity-game equilibrium is defined by unilateral payoff comparisons over $[0,\infty)$, and it is not defined by equation (2). Equation (2) is instead a theorem characterizing the equilibrium. The supplier's profit is defined as $r(q_1+q_2)$ for any pair, independently of equation (3). These choices prevent the goal from becoming an inequality between two expressions whose connection to the game has merely been assumed. Equation (2)'s missing closing parenthesis in the manuscript is interpreted as the displayed first quantity divided by three. No division in the model's displayed formulas has a variable denominator.

Selected references

• J. Wang, T. Huang and J. Lee, Cross-licensing in a Supply Chain with Asymmetric Manufacturers, SSRN manuscript 3053682, version of 2023-04-27, pp. 9–11 and Appendix p. A.1; published in Manufacturing & Service Operations Management, 2023. Manuscript; DOI.

Motivation

Distributed energy resources (DERs) — rooftop solar, home batteries, electric vehicles — turn electricity consumers into prosumers who can both buy and sell power. Their individual capacities are far too small to bid in a wholesale electricity market directly, so regulators have opened these markets to DER aggregators, intermediaries that pool many small resources and trade on their behalf (FERC Order 2222, 2020). An aggregator is a monopolist toward the prosumers it serves, and a profit-seeking monopolist between a market and its suppliers ordinarily distorts quantities: with a single unit price, the aggregator buys less than the efficient amount, and social welfare falls (Alshehri, Ndrio, Bose, Başar 2019, 2020).

Gao, Alshehri and Birge ask whether this loss can be avoided without regulating the aggregator. Their answer is that it can, provided the aggregator uses two-part pricing: a participation fee plus a per-unit price. This mission formalizes that efficiency result.

Setting

A power network has a finite set $K$ of nodes and a finite set $L$ of transmission lines. The ISO chooses nodal net injections $h\in\mathbb R^K$; the DC approximation of the AC network gives a matrix $B$ and line capacities $f$, and the network constraints are (5b): $\mathbf 1^\top h=0$ and $Bh\le f$.

A finite set $I$ of prosumers sits at the nodes. Prosumer $i$ owns a DER capacity $C_i\ge0$ and has a utility of consumption $u_i$ on $[0,Z]$, $Z>C_i$. Assumption 1: $u_i$ is increasing, strictly concave and continuous on $[0,Z]$, differentiable on $(0,Z)$, with $u_i'(z)\to\infty$ as $z\to0^+$ and $u_i'(z)\to0$ as $z\to Z^-$. A finite set $J$ of conventional generators sits at the nodes; generator $j$ produces $y_j\in[\underline y_j,\overline y_j]$ at cost $c_j(y_j)$. Assumption 2: $c_j$ is increasing, strictly convex and continuous on its interval, differentiable inside, with $c_j'\to0$ at the lower end and $c_j'\to\infty$ at the upper end.

Benchmark (direct participation). Prosumer $i$ sells $x_i$ and buys $d_i$ directly in the market at the locational price; only the net sale $z_i=x_i-d_i$ matters. Writing $X^k$, $D^k$, $Y^k$ for the nodal totals of sales, purchases and generation, the ISO solves the economic dispatch problem (9):

$$\max\ \mathcal W_B=\sum_i u_i(C_i-z_i)-\sum_j c_j(y_j)\quad\text{s.t. (5a) } h=D-Y-X,\ \text{(5b)},\ \text{(6) } C-Z\le z\le C,\ \underline y\le y\le\overline y .$$

The wholesale prices $\lambda\in\mathbb R^K$ are the optimal Lagrange multipliers of the nodal balance constraints (5a).

Unregulated aggregation. Each prosumer sells only to the aggregator $\mathcal A$, which offers her a fee $P_i$ and a unit price $p_i$. At wholesale price $\lambda$ she maximizes the payoff (10), $p_ix_i-P_i+u_i(d_i+C_i-x_i)-\lambda d_i$ if she sells $x_i>0$ and $u_i(d_i+C_i)-\lambda d_i$ otherwise, over $x_i\in[0,C_i]$, $d_i\in[0,Z-C_i+x_i]$ (11). The aggregator earns (13) $P_i\mathbf 1\{x_i>0\}+(\lambda-p_i)x_i$ and chooses nonnegative offers anticipating the responses: a Stackelberg game $\mathcal G(\lambda)$ (Definition 1). The ISO now dispatches $x$ and $d$ separately, solving (21): maximize $\mathcal W_A=\sum_i u_i(d_i+C_i-x_i)-\sum_j c_j(y_j)$ subject to (5a), (5b) and (18) $0\le x\le C$, $0\le d\le Z-C+x$, $\underline y\le y\le\overline y$; its wholesale prices are again the multipliers of (5a).

Formalization targets

Goal: Theorem 1 (p. 14)

Under Assumptions 1–3 (Assumption 3: (9) is feasible), with $(h^*,z^*,y^*)$ the optimal solution of (9),

$$\mathcal W_A^*=\mathcal W_B^*,$$

every optimal solution of (21) has $x-d=z^*$, $y=y^*$, $h=h^*$, the split $([z^*]^+,[-z^*]^+)$ is optimal for (21), and a price vector is a multiplier of (5a) for (21) if and only if it is one for (9).

Milestones

1. Lemmas 1 and 2 (pp. 5–6): a price-taking prosumer's problem (1) and generator's problem (3) have unique optima, characterized by $u'(C-z^*)=\lambda$ (2) and $c'(y^*)=\lambda$ (4).
2. Proposition 1 (p. 8): (9) has a unique optimum, and at every multiplier vector of (5a) it is a competitive equilibrium.
3. Lemma 3 (p. 10): the prosumer's optimal response to a two-part offer, in terms of $u'(z_1)=\lambda$, $u'(z_2)=p$.
4. Lemma 4 (p. 11): the aggregator's optimal offer is

$$p^*=\lambda,\qquad P^*=\lambda(C-z_1)+u(z_1)-u(C).$$

5. Proposition 2 (p. 12): these offers form a Stackelberg equilibrium of $\mathcal G(\lambda)$.
6. Proposition 3 (p. 14): (21) has an optimum consistent with Lemmas 3, 4 and (4) at its multipliers.

Significance

The result. Theorem 1 shows that the efficiency loss attributed to profit-seeking aggregators is a consequence of one-part pricing, not of aggregation itself. With two-part pricing the aggregator passes the locational marginal price through as its unit price and extracts its profit only through participation fees, so welfare, dispatch and locational prices are exactly those of direct participation. The paper builds on this to analyse a regulated aggregator (§4) and the interaction of prosumer participation with generators' market power (§5, the companion mission of this series).

Formalizing it. The result is proved on paper, in a short argument relying on unstated conventions; no machine-checked version exists. A formal proof must make precise what "optimal Lagrange multiplier" means for a nonsmooth-at-the-boundary concave program on a network, handle the indicator in the prosumer's payoff (10) and the ties it creates, and settle the edge cases (nonpositive locational prices, capacity below the efficient consumption level) that the printed statements pass over.

Difficulty

The welfare identity is the easy part: the objective (20) and the balance (5a) of (21) depend on $(x,d)$ only through $x-d$, and the box (18) projects onto the box (6). The work lies elsewhere. Price equality requires an argument about saddle points of the Lagrangian on two different domains, not just optimal values. The prosumer's two-part problem (11) is discontinuous at $x=0$ because of the fee, so its optimal responses must be found by comparing branches, and the aggregator's optimality in Lemma 4 must hold against every nonnegative offer — including unit prices above the wholesale price — and every optimal response to it, not a selected one. The first-order conditions (2) and (4) require interior optima, which follow from the derivative limits in Assumptions 1–2 but only at positive prices.

Formalization scope

Everything lives in the namespace DERAggregation.Unregulated, in one definition file Setting. Nodes, prosumers, generators and lines are finite types; the node of prosumer $i$ is loc i. All quantities are real. Optimality is "feasible and at least as good as every feasible point", never a supremum. A multiplier vector of (5a) is a saddle point of the partial Lagrangian: (5a) and (5b) are dualized (with $\nu\ge0$ and complementary slackness for $Bh\le f$), the participant box is kept as the domain, and $h$ is free. Prices are never free variables and never defined by a closed form.

Assumptions 1–2 read "differentiable" as differentiable on the open interval and continuous on the closed one, since the derivative limits rule out differentiability at the endpoints; $0\le C_i$ and $\underline y_j<\overline y_j$ are added. Theorem 1 names no assumptions; it is stated under Assumptions 1–3. Problem (21) determines only $x-d$, so "the same $x^*,d^*$" is stated as equality of $x-d$ plus optimality of the canonical split. The first-order conditions are stated at nodes with positive price, Lemma 3 adds $P\ge0$ and $0<p\le\lambda$, and Lemma 4's second part adds the standing restriction $p\le\lambda$; each addition is disclosed in its item. Problem (21) is written in the separate variables $x$ and $d$ with the constraint $d\le Z-C+x$ exactly as printed: a formalization through $z=x-d$ would make Theorem 1 true by unfolding and is ruled out.

The source is the authors' SSRN working paper (abstract 3931052, PDF of September 26, 2021); the published version in Manufacturing & Service Operations Management (2024) may number or state results differently. Useful contributions include the one-dimensional lemmas (unique maximizers of strictly concave functions with derivative limits at the endpoints), which are reusable well beyond this mission, and a general saddle-point lemma for separable concave programs with linear coupling constraints.

Selected references

• Z. Gao, K. Alshehri, J. R. Birge, Aggregating Distributed Energy Resources: Efficiency and Market Power, working paper, SSRN abstract 3931052, 2021. https://ssrn.com/abstract=3931052 ; published in Manufacturing & Service Operations Management, 2024, https://doi.org/10.1287/msom.2021.0539
• K. Alshehri, M. Ndrio, S. Bose, T. Başar, The impact of aggregating distributed energy resources on electricity market efficiency, 53rd Annual Conference on Information Sciences and Systems (CISS), IEEE, 2019, pp. 1–6.
• K. Alshehri, M. Ndrio, S. Bose, T. Başar, Quantifying market efficiency impacts of aggregated distributed energy resources, IEEE Transactions on Power Systems 35(5), 2020, pp. 4067–4077.
• Federal Energy Regulatory Commission, Participation of Distributed Energy Resource Aggregations in Markets Operated by Regional Transmission Organizations and Independent System Operators, Order No. 2222, 2020.

Motivation

Recommender systems on online platforms are usually trained to maximize engagement: time spent, items consumed, sessions returned. The implicit justification is revealed preference: a user who consumes more must value the content more. Behavioural economics questions that inference when a person's choices are driven by two conflicting processes, a deliberate one that weighs long-run utility and an impulsive one that reacts to the item in front of it.

Kleinberg, Mullainathan and Raghavan (2023) build a minimal model of such a user and ask when engagement is a good proxy for utility. Their first characterization (Theorem 4.1, a separate mission) says that the engagement-maximizing content differs from the utility-maximizing content only through higher moreishness, or higher span with lower value. This mission formalizes the complementary positive result, Theorem 4.2: on a content manifold where no content is very moreish and all content has roughly equal value (a "salad"-like manifold), maximizing engagement loses only a small, explicitly bounded amount of user utility.

Setting

A content distribution is a triple $\omega=(p,q,\bar v)$ in the parameter space

$$\Omega=[0,1)\times[0,1)\times\mathbb R_+ .$$

The user consumes items one at a time. System 2, the deliberate agent, collects utility with mean $\bar v$ per item while it is still interested, and pays an outside option $W>0$ per step spent on the platform. After each item system 2 stays interested with probability $q$, the span. System 1, the impulsive agent, is hooked by each item with probability $p$, the moreishness, and then consumes the next item without consulting system 2. Define

$$g_S(\omega)=\frac{\bar v-W}{1-q}-\frac{pW}{1-p},\qquad g_T(\omega)=\frac{1}{1-q}+\frac{p}{1-p}.$$

System 2 visits the platform only if this is worthwhile, so its expected utility is equation (1),

$$\mathbb E[S(\omega)]=\max\bigl(g_S(\omega),0\bigr),$$

and the session length $T$ is $0$ when the user does not visit ($g_S(\omega)<0$) and otherwise has expectation $\mathbb E[T(\omega)]=g_T(\omega)$, equation (2).

A platform chooses content from a content manifold $\mathcal M\subseteq\Omega$, which the paper assumes contains a point with $\mathbb E[S]>0$. The utility maximizer $\omega_S=(p_S,q_S,\bar v_S)$ maximizes $g_S$ over $\mathcal M$ (3). The engagement maximizer $\omega_T=(p_T,q_T,\bar v_T)$ maximizes $g_T$ over the points of $\mathcal M$ at which the user participates, $\{\omega\in\mathcal M:g_S(\omega)\ge0\}$ (4). The proof uses $a_i=\frac{1}{1-p_i}$ and $b_i=\frac{1}{1-q_i}$ for $i\in\{S,T\}$, so that $\mathbb E[T(\omega_S)]=a_S+b_S-1$.

Formalization targets

Goal: Theorem 4.2 (p. 17)

Suppose $p\le\alpha<1$ for every $(p,q,\bar v)\in\mathcal M$, and $|\bar v-v_0|<\beta$ for every $(p,q,\bar v)\in\mathcal M$, for some $v_0$. Then

$$\mathbb E[S(\omega_T)]\ \ge\ \mathbb E[S(\omega_S)]-2\beta\,\mathbb E[T(\omega_S)]-\frac{\alpha(v_0+\beta)}{1-\alpha}.$$

Milestones (p. 18)

1. Inequality (5): if $g_T(\omega_T)\ge g_T(\omega_S)$, then $b_S-b_T\le a_T-a_S$.
2. Inequality (7): if $0\le p_i\le\alpha<1$, then $1\le a_i\le\frac{1}{1-\alpha}$.
3. The gap identity: when $g_S\ge0$ at both points,

$$\mathbb E[S(\omega_S)]-\mathbb E[S(\omega_T)]=b_S(\bar v_S-\bar v_T)+(b_S-b_T)(\bar v_T-W)+W(a_T-a_S).$$

A supporting statement, implicit in the proof, is that participation $g_S(\omega)\ge0$ at a point of $\Omega$ forces $\bar v\ge W$.

Significance

The theorem is the paper's sufficient condition for engagement optimization to be benign. It is quantitative: the utility loss is linear in the value spread $\beta$, scaled by the engagement $\mathbb E[T(\omega_S)]$ of the utility-optimal content, plus a term that vanishes as the moreishness bound $\alpha$ goes to $0$. The paper notes that the linear dependence on engagement is unavoidable, since a user can lose a constant utility per step when $\bar v_T<\bar v_S$. Together with Theorem 4.1 it delimits when a platform that observes only engagement can safely optimize it, and it motivates the paper's §5, on how a platform might learn which kind of manifold it is on.

The result is proved in the paper, with a short proof. As far as is known, neither the model nor the theorem has been machine-checked. The formalization fixes the participation convention for $\mathbb E[T]$, the feasibility of $\omega_S$ in the engagement problem, and the implicit hypotheses listed below, which the printed proof uses without stating.

Difficulty

The algebra is elementary once the denominators are known to be positive. The difficulty lies in the bookkeeping the printed proof leaves implicit. Inequality (5) is derived from "$\mathbb E[T(\omega_T)]>\mathbb E[T(\omega_S)]$", but (4) only gives $\ge$, and only once $\omega_S$ is shown feasible for (4), which needs $g_S(\omega_S)>0$, i.e. the standing assumption on $\mathcal M$. Multiplying (5) by $\bar v_T-W$ needs $\bar v_T\ge W$, which follows from $g_S(\omega_T)\ge0$ and $W>0$. The bound on $(a_T-a_S)\bar v_T$ splits on the sign of $a_T-a_S$, and uses $\alpha\ge0$ (from $\mathcal M\neq\emptyset$) and $v_0+\beta>\bar v_T\ge0$. Finally, $\mathbb E[T(\omega_S)]$ must be identified with $a_S+b_S-1$ through participation at $\omega_S$. Using $g_T$ in place of $\mathbb E[T]$, or dropping the participation constraint from (4), changes the theorem.

Formalization scope

The Lean development lives in the namespace EngagementOpt.Salad and imports the frozen shared model in EngagementOpt.Misalign. There, a content distribution is a structure Params with real fields p, q, v; InOmega ω states $0\le p<1$, $0\le q<1$, $0\le\bar v$. The shared functions gS W, gT and this chunk's ES W, ET W, aCoef, bCoef are as above, with ET W ω = if gS W ω < 0 then 0 else gT ω. The shared maximizer predicates IsUtilityMaximizer W M ωS (membership and IsMaxOn (gS W) M ωS) and IsEngagementMaximizer W M ωT (membership, 0 ≤ gS W ωT, and IsMaxOn gT {ω ∈ M | 0 ≤ gS W ω} ωT) hold for every maximizer, so the theorem holds for any tie-breaking rule. Closedness of $\mathcal M$ only guarantees that maximizers exist and is not assumed. The goal's hypotheses are: $W>0$; $\mathcal M\subseteq\Omega$; a point of $\mathcal M$ with $g_S>0$; the two maximizer predicates; $\alpha<1$ and $p\le\alpha$ on $\mathcal M$; and $|\bar v-v_0|<\beta$ on $\mathcal M$ for a given $v_0$.

Three of these are implicit in the paper and are disclosed: $W>0$ (§2.1 normalizes $W=1$); $\alpha<1$, without which condition 1 is vacuous on $\Omega$ and the bound fails (Lean's $x/0=0$ would turn $\alpha=1$ into a false statement); and the standing assumption of p. 16. Neither $0\le\alpha$ nor $0<\beta$ is assumed; both follow from the hypotheses. Inequality (5) is posed with $\le$ rather than the printed $<$, because only $\ge$ is available from (4). The hypotheses are satisfiable: with $W=1$, $\mathcal M=\{(0,\tfrac12,3),(\tfrac12,\tfrac12,3)\}$, $\alpha=\tfrac12$, $v_0=3$, $\beta=0.1$, the maximizers are $\omega_S=(0,\tfrac12,3)$ and $\omega_T=(\tfrac12,\tfrac12,3)$, and the bound reads $3\ge0.5$.

Everything needed is in Mathlib (real arithmetic, max, |·|, IsMaxOn). Proofs of the milestones and the goal are welcome; the base model module is shared with the Theorem 4.1 mission of the same paper.

Selected references

• J. Kleinberg, S. Mullainathan, M. Raghavan, The Challenge of Understanding What Users Want: Inconsistent Preferences and Engagement Optimization, Management Science, 2023. DOI 10.1287/mnsc.2022.03683; read as arXiv:2202.11776v3.
• G. S. Becker, K. M. Murphy, A Theory of Rational Addiction, Journal of Political Economy 96(4), 1988. DOI 10.1086/261558.

Motivation

Treatments for rare diseases can require substantial research and development spending while reaching a small patient population. A public subsidy can cover part of the manufacturer's development cost, part of the patient's price, or both. Which recipient should receive the subsidy depends on how the manufacturer responds. A further design choice is whether the manufacturer is paid when a drug is sold or only when treatment succeeds. Olsder, Martagan, and Tang formulate these choices as a sequential game between the government, a manufacturer, and patients in their SSRN working paper, §§3–4. This mission concerns their results for the case in which the manufacturer sets the price.

The paper reports that a manufacturer subsidy alone is optimal under either payment scheme and that the relative prices under the two schemes change with the government budget. The price comparison is useful because a payment contract intended to protect patients can change the price set by the manufacturer. The mission uses the working paper dated 2019-11-13. Its page and equation numbers are those of that version, which precedes the published article.

Setting

The government first chooses two subsidy shares: $\alpha\in[0,1)$ covers the fraction $\alpha$ of research cost and $\beta\in[0,1)$ covers the fraction $\beta$ of the unit price paid on a patient's behalf. The manufacturer then chooses a nonnegative unit price $p$ and a positive target efficacy $e$. Research cost is $ke^2$, with $k>0$, so the manufacturer's effective cost is $(1-\alpha)ke^2$. The government has a budget $B>0$. The market size is one, and patient valuations are uniform on $[0,1]$; these conventions are given in §3.1–§3.2.

In Setting (1A) the manufacturer receives the price for every sale. Its profit is $\pi_A=p(1-(1-\beta)p/e)-(1-\alpha)ke^2$. At price and efficacy $(p,e)$, patient welfare is $W_A=(e-(1-\beta)p)^2/(2e)$, while government spending is $M_A=\alpha ke^2+\beta p(1-(1-\beta)p/e)$. These are the paper's equations (2), (3), and (5). In Setting (1B) payment occurs only if treatment succeeds. The corresponding expressions are $\pi_B=ep(1-(1-\beta)p)-(1-\alpha)ke^2$, $W_B=e(1-(1-\beta)p)^2/2$, and $M_B=\alpha ke^2+e\beta p(1-(1-\beta)p)$, from equations (7), (8), and (10) of the same source.

For each scheme, a manufacturer best response is a pair $(p,e)$ maximizing that scheme's profit over all $p\ge0$, $e>0$. A government policy is optimal when it has a best response at which spending does not exceed $B$, and its patient welfare is at least the welfare of every feasible policy evaluated at every manufacturer best response. This expresses the government's leader role and the manufacturer's follower role in the game's sequence of events, rather than assigning the closed forms of §§4.1–4.2 to either player by definition.

Formalization targets

Government policy under each payment scheme

Proposition 1 of the working paper, p. 12, gives the unique optimal policy under sales-based payment. The paragraph after (16) on p. 13 says the same policy is optimal under outcome-based payment:

$$(\alpha,\beta)=(\alpha^*,0),\qquad \alpha^*=\frac{1+128Bk-\sqrt{256Bk+1}}{128Bk}.$$

The budget binds at this policy. In both settings the optimal patient welfare and the manufacturer's profit equal $2B/(\sqrt{256Bk+1}-1)$. These policy claims, the two best-response formulas, and the two welfare and spending reductions form the six milestones.

Price comparison

Corollary 1 on p. 13 compares the manufacturer's optimal price in the two payment schemes. If $p_A$ and $p_B$ denote prices at optimal policies and best responses, the goal is the three-way statement

$$B<k-\tfrac18\Rightarrow p_A<p_B,\qquad B=k-\tfrac18\Rightarrow p_A=p_B,\qquad B>k-\tfrac18\Rightarrow p_A>p_B.$$

The printed second clause uses $B\ge k-1/8$ and says “higher”; equality of the two prices at the threshold is a boundary slip. The formal target records equality separately and preserves the strict high-budget comparison.

Significance

The policy result identifies which subsidy reaches patients most effectively within this model: when the manufacturer sets the price, the government uses its entire budget on the manufacturer's development cost, regardless of whether payment is per sale or contingent on treatment success. The price result adds a distinct comparison. Equal optimal subsidies and equal patient welfare do not imply equal prices; the sign of the price difference depends on $B$ relative to $k-1/8$. This distinction appears explicitly in the paper's discussion following Corollary 1, pp. 13–14.

The working paper proves these results mathematically. The mission's remaining work is to give machine-checked proofs for the game definitions, both best-response results, both welfare and spending reductions, the unique optimum, and the final price comparison. It does not assert that those proofs have already been formalized. The definitions of attained best response and government optimality can also support later analyses of different subsidy or payment rules.

Difficulty

The government cannot compare the two schemes by holding the manufacturer's choices fixed. The manufacturer optimizes both price and efficacy after observing the subsidy policy, and the two profit functions have different price terms. Even after determining each manufacturer's response, identical formulas for government welfare and spending do not themselves establish an attained and unique optimum on the continuous half-open policy region $[0,1)^2$. The price comparison then concerns the actual best-response prices at that optimum, including the threshold where the two prices coincide. These dependencies explain why the reduced expressions alone cannot serve as the definition of the game.

Formalization scope

Lean represents all parameters, policies, prices, efficacies, profit, welfare, and spending in $\mathbb R$. The policy predicate requires $\alpha,\beta\in[0,1)$. Every theorem assumes $k>0$; the budget results also assume $B>0$. These positivity conditions make the paper's denominators meaningful and state its implicit economic regime. Prices chosen by the manufacturer satisfy $p\ge0$. Its efficacy choice satisfies $e>0$ and has no imposed upper bound of one: equations (3) and (8) maximize over $e$, and in the high-budget part of Corollary 1 their optimizer can exceed one. This is a convention of the paper's algebraic model, even though efficacy is introduced as a probability.

The demand expressions used in the paper's equations are left unclipped. At the stated best responses, they lie in the relevant nonnegative range. Best responses are represented as sets of all maximizers, and the goal compares every response at every optimal policy. Government optimality requires a feasible best response and comparison with every feasible competing policy and response, so neither existence nor uniqueness is obtained from an empty set. In particular, the reduced welfare and budget formulas (13) and (16) are milestone conclusions, not definitions of government choice. Reusable contributions include real optimization arguments for joint price and efficacy maximization and for attained welfare maxima over subsidy policies.

Selected references

• W. Olsder, T. Martagan, and C. S. Tang, Improving Access to Rare Disease Treatments: Optimal Subsidies, Pricing, and Payment, SSRN working paper 3481150, version of 2019-11-13, §§3–4, pp. 8–14. SSRN.
• W. Olsder, T. Martagan, and C. S. Tang, Improving Access to Rare Disease Treatments: Subsidy, Pricing, and Payment Schemes, Management Science, 2023. DOI: 10.1287/mnsc.2022.4634.

Why parameter uncertainty changes portfolio choice

An investor selecting a portfolio from estimated returns faces two distinct outcomes: the average utility the chosen rule delivers across possible historical samples, and the variation of that utility from one sample to another. A portfolio rule can perform well on average while being sensitive to the particular observations used to estimate it. Lassance, Martín-Utrera, and Simaan quantify this sensitivity for portfolios estimated from Gaussian returns and propose a mean-risk criterion that penalizes the standard deviation of out-of-sample utility (OOSU). This mission concerns the shrinkage intensity that maximizes that criterion. Its source is the authors' SSRN manuscript dated August 18, 2023, including the Internet Appendix; page labels IA1–IA45 refer to that appendix.

The paper's Proposition 1 provides an exact finite-sample variance for OOSU, and Proposition IA.1 restates a closed-form OOSU mean from Kan, Wang, and Zhou. Those formulas make it possible to compare choices that maximize average utility, minimize utility variance, or balance the two. Proposition 4 characterizes the balancing choice without fixing the risk weight to a particular numerical calibration. Lassance, Martín-Utrera, and Simaan, §§4–5 and Internet Appendix IA.1.

The market and the shrinkage rule

There are $N$ risky stocks. Their excess-return vector has population mean $\mu$ and positive-definite covariance matrix $\Sigma$. An investor with risk-aversion coefficient $\gamma>0$ holds weights $w$ summing to one and evaluates their mean-variance utility as $U(w)=w^\top\mu-(\gamma/2)w^\top\Sigma w$. The population global-minimum-variance portfolio has mean $\mu_g$ and variance $\sigma_g^2>0$. The zero-cost portfolio that accounts for mean-return opportunities has return variance $\psi^2\geq0$. These constants are defined from $\mu$ and $\Sigma$ in equations (5)–(7). Source, §3.1.

From $T$ independent Gaussian observations, the investor estimates the mean and covariance, using a $1/T$ factor in the sample covariance. The sample mean-variance portfolio and sample global-minimum-variance portfolio are mixed using an intensity $\kappa\in[0,1]$: $\kappa=0$ selects the latter and $\kappa=1$ the former. Because the data are random, this portfolio's OOSU is random. Let $E_T(\kappa)$ and $V_T(\kappa)$ denote its OOSU mean and variance. In this mission they are the exact analytic expressions in (IA1)–(IA2) and (13)–(19), respectively. The formulas depend on $N,T,\gamma,\mu_g,\sigma_g^2,\psi^2$, and $\kappa$; the variance formula is a fourth-degree polynomial in $\kappa$. Source, §§3.2–4.1 and Appendix IA.1.

For a fixed robustness weight $\lambda\geq0$, the mean-risk OOSU is

$$R_T(\kappa)=E_T(\kappa)-\lambda\sqrt{V_T(\kappa)}.$$

The robust intensity $\kappa_R$ maximizes $R_T$ on $[0,1]$. A variance-minimizing intensity is denoted $\kappa_V$, while $\kappa_E(T)$ maximizes $E_T$ and has the explicit form (IA3). The sample-size condition throughout finite-sample claims is $N\geq2$ and $T>N+7$. Source, Assumption 1 and equations (20)–(21).

Formalization targets

The main target is Proposition 4. For every finite sample size allowed by Assumption 1, maximizers of $R_T$ and minimizers of $V_T$ exist, and every such pair obeys

$$\kappa_V\leq\kappa_R\leq\kappa_E(T).$$

When $\psi^2>0$, every sequence of robust maximizers for increasing $T$ also obeys

$$\lim_{T\to\infty}\kappa_R(T)=1.$$

The ordered milestones establish that $\kappa_E(T)$ is the OOSU mean maximizer and lies in $[0,1]$; that it tends to one for $\psi^2>0$; that OOSU variance decreases with sample size and tends to zero for each fixed admissible $\kappa$; and that variance is nondecreasing as $\kappa$ rises from $\kappa_E(T)$ to one. The last milestone isolates the shrinkage-intensity clause of Proposition 2(2). Source, Proposition IA.1, Proposition 2, and Proposition 4.

What the result supplies

The inequality puts the risk-balanced choice on a single interval with two interpretable endpoints. A user of the model can compare robust allocations with the mean-optimal and variance-optimal portfolios without solving an unconstrained optimization problem over all intensities. The asymptotic statement says that, for fixed market parameters and positive $\psi^2$, any robust choice approaches the sample mean-variance endpoint as the historical sample grows. The theorem itself is proved in the manuscript; this mission asks for machine-checked statements and proofs of that known result, not for a new mathematical claim. Source, §5.2 and proof of Proposition 4, pp. IA44–IA45.

Formalizing the closed-form analysis also produces reusable tools for optimizing a polynomial mean and a polynomial variance under a square-root risk penalty on a compact interval. The supporting items separate the paper's exact formulas from the statements about their extrema and limits. The probabilistic derivation of the variance is the target of the separate Proposition 1 mission; the closed-form identities here let this mission focus on the optimizer comparison. No proof of this mission's goal is claimed to be machine checked yet.

The central difficulty

The mean has a transparent quadratic maximum, but the variance is a fourth-degree expression whose coefficients are rational functions of $T,N,\gamma,\sigma_g^2,$ and $\psi^2$. A direct comparison of objective values at arbitrary intensities does not expose the ordering of all possible extrema. Moreover, the risk penalty uses $\sqrt{V_T}$, so its behavior cannot be inferred from the mean and variance formulas by treating the penalty as $V_T$ itself. The sample-size limit concerns every sequence of optimizers, while the variance milestone gives a pointwise limit for each fixed $\kappa$; relating the two requires control over the entire admissible interval. Source, Proposition 1 and proof of Proposition 4.

Formalization scope

Lean stores $N$ and $T$ as natural numbers and casts them to real numbers before every subtraction in the rational formulas. A fixed parameter structure holds $N,\gamma,\sigma_g^2,\psi^2,\mu_g,$ and $\lambda$; $T$ remains an argument so that limits as $T\to\infty$ keep the other parameters fixed. The standing predicate requires $N\geq2$, $\gamma>0$, $\sigma_g^2>0$, $\psi^2\geq0$, and $\lambda\geq0$. Individual finite-sample statements require $T>N+7$. The positivity and nonnegativity of the population variances come from positive definiteness of $\Sigma$; the Gaussian sampling model is what identifies the closed forms as actual OOSU moments in Proposition 1 and Proposition IA.1.

The variance function is the exact sum of (14) and the polynomial (15) with coefficients (16)–(19), including the displayed polynomial $C(T,N,\psi^2)$. The mean function is (IA1)–(IA2); $\kappa_E(T)$ is (IA3); and the robustness function uses Real.sqrt of the variance, exactly as (20) requires. Extrema are taken on Set.Icc 0 1, with explicit existence and quantification over every optimizer. The goal does not choose a convenient maximizer or rely on a potentially empty optimizer set. The added $\psi^2>0$ condition appears only in the two limit statements, since at $\psi^2=0$ the printed limits fail. The manuscript's claim that the underlying estimated portfolio is consistent is outside this closed-form model, which does not contain that random portfolio.

The complete development needs real polynomial and rational inequalities, continuity and extrema on compact intervals, and limits of the coefficient functions. These tools can serve other mean-risk optimization problems. Contributions that close the four cited milestones or supply reusable analytic lemmas for them fit this mission. The paper's monotonicity claim in the stock count $N$ is excluded because it is false for some admissible parameters; its variance and zero-cost-variance clauses are outside the focused milestone list. Source, Proposition 2(2) and proof, pp. 16 and IA39–IA44.

Selected references

• N. Lassance, A. Martín-Utrera, and M. Simaan, The Risk of Expected Utility under Parameter Uncertainty, authors' SSRN manuscript dated August 18, 2023, later published in Management Science (2024). SSRN 3855546; DOI 10.1287/mnsc.2023.00178.
• R. Kan, X. Wang, and G. Zhou, Optimal Portfolio Choice with Estimation Risk: No Risk-Free Asset Case, Management Science 68(3), 2047–2068 (2022). DOI 10.1287/mnsc.2021.3989.

Why engagement is not utility

Online platforms rank content by what they can measure: clicks, watch time, session length. The implicit justification is revealed preference: if users stay longer, they must like what they see. Kleinberg, Mullainathan and Raghavan (arXiv:2202.11776v3, Management Science 2023, doi:10.1287/mnsc.2022.03683) question this justification with a model of a user whose preferences are internally inconsistent, in the tradition of dual-process models of choice. Within the model, an engagement-maximizing platform can serve content that lowers the user's welfare, and the paper asks exactly when this happens. This mission formalizes its first characterization result, Theorem 4.1 (p. 16).

The model

A user consumes a stream of items $t=0,1,2,\dots$ and is a composite of two agents (§2.1, pp. 5–8).

• System 2 is forward-looking. Each consumed item gives it a random value with mean $\bar v$, while leaving the platform gives an outside option $W$ per step. After each item, system 2 still wants to continue with probability $q$, and otherwise it is "done" for the rest of the session.
• System 1 is impulsive. With probability $p$ it is hooked by the current item and consumes the next one without consulting system 2.

A content distribution is the triple $\omega=(p,q,\bar v)$, read as moreishness $p$, span $q$ and value $\bar v$. The parameter space is (p. 15)

$$\Omega=[0,1)\times[0,1)\times\mathbb R_+ .$$

The content a platform can offer forms a content manifold $\mathcal M\subseteq\Omega$.

Summing system 2's utility over the two phases of a session (before and after system 2 is done) gives, when the user participates,

$$g_S(\omega)=\frac{\bar v-W}{1-q}-\frac{pW}{1-p},\qquad g_T(\omega)=\frac{1}{1-q}+\frac{p}{1-p}$$

(p. 16). Here $g_S$ is system 2's expected utility $\mathbb E[S]=\max(g_S,0)$ (equation (1), p. 7) and $g_T$ is the expected session length $\mathbb E[T]$ (equation (2), p. 8). The user stays away when $g_S(\omega)<0$, and then $T=0$.

Write $\omega_S=(p_S,q_S,\bar v_S)$ and $\omega_T=(p_T,q_T,\bar v_T)$ for the utility and engagement maximizers (p. 16):

$$\omega_S\in\arg\max_{\omega\in\mathcal M} g_S(\omega)\quad(3),\qquad \omega_T\in\arg\max_{\omega\in\mathcal M,\ g_S(\omega)\ge0} g_T(\omega)\quad(4).$$

The platform observes only engagement, so it serves $\omega_T$, and only among content the user is willing to consume. The paper assumes that $\mathcal M$ contains at least one point with $g_S>0$.

Formalization targets

Goal: Theorem 4.1 (p. 16)

Suppose $\omega_S\neq\omega_T$ and the disagreement is strict, $g_S(\omega_S)>g_S(\omega_T)$ and $g_T(\omega_T)>g_T(\omega_S)$. Then

$$p_T>p_S\qquad\text{or}\qquad\bigl(q_T>q_S\ \text{ and }\ \bar v_T<\bar v_S\bigr).$$

Milestones (the two steps of the printed proof)

1. Proof of Theorem 4.1, p. 16: for $\omega_S,\omega_T\in\Omega$, if $p_T\le p_S$ and $g_T(\omega_T)>g_T(\omega_S)$, then $q_T>q_S$.
2. Proof of Theorem 4.1, p. 17: for $\omega_S,\omega_T\in\Omega$ and $W>0$, if $p_T\le p_S$, $q_T>q_S$, $g_S(\omega_S)>g_S(\omega_T)$ and $g_S(\omega_T)\ge0$, then $\bar v_T<\bar v_S$.

A supporting item, not a milestone: for $\omega\in\Omega$ and $W>0$, $g_S(\omega)\ge0$ implies $\bar v\ge W$.

Significance

The theorem names the only two ways an engagement maximizer can do worse for the user than a utility maximizer. Either the content is more habit-forming (it raises system 1's grip), or it keeps system 2 interested for longer while delivering less per item, as when a long series of instructional videos replaces a short one. A platform that wants to diagnose misalignment therefore needs to look at moreishness and at the span–value trade-off, and at nothing else. The companion result of the paper (Theorem 4.2, a separate mission) turns this around: when moreishness is small and value nearly constant across $\mathcal M$, engagement maximization is near-optimal.

The result is proved in the paper by a few lines of algebra. No machine-checked version of it was found on Prove2Me or in Mathlib. Formalizing it pins down what the printed proof leaves implicit: the step from $\frac{\bar v_T-W}{1-q_T}$ to $\frac{\bar v_T-W}{1-q_S}$ on p. 17 is valid only because $\bar v_T\ge W$, which follows from the participation constraint of (4). The mission also provides a reusable encoding of the paper's model (Ω, $g_S$, $g_T$, (3), (4)).

Difficulty

The mathematics is elementary. What makes the statement delicate is its hypotheses. If the participation constraint $g_S(\omega_T)\ge0$ is dropped from (4) together with the standing assumption that $\mathcal M$ contains a point with $g_S>0$, the theorem is false. With $W=1$ and $\mathcal M=\{(0,0,\tfrac12),(0,\tfrac12,\tfrac12)\}$, the first point maximizes $g_S$ and the second maximizes $g_T$, the disagreement is strict, yet $p_T=p_S$ and $\bar v_T=\bar v_S$. The obvious reading of the second step, "a larger $q$ shrinks the denominator", fails when $\bar v_T<W$, because the numerator is then negative.

Formalization scope

• A content distribution is a structure Params with three real fields p, q, v (for $\bar v$). Membership in $\Omega$ is the predicate InOmega: $0\le p<1$, $0\le q<1$, $0\le\bar v$. Every theorem requires it of the points it uses, because Lean's division gives $x/0=0$ and $g_S$, $g_T$ would take junk values at $p=1$ or $q=1$.
• The outside option $W$ is a real parameter with the added hypothesis $W>0$. The paper sets $W=1$ "without loss of generality" (p. 5) but keeps $W$ in its formulas, and the proof uses $W>0$.
• (3) and (4) are the predicates IsUtilityMaximizer and IsEngagementMaximizer, built from Mathlib's IsMaxOn. $\omega_S$ maximizes over all of $\mathcal M$; $\omega_T$ lies in $\mathcal M$, satisfies $g_S(\omega_T)\ge0$, and maximizes $g_T$ over $\{\omega\in\mathcal M:g_S(\omega)\ge0\}$. The theorem holds for every pair of maximizers, which is stronger than the paper's "ties broken consistently" and needs no tie-breaking rule.
• The paper's closedness of $\mathcal M$ only guarantees that the maximizers exist. Since the theorem assumes them, closedness is not required.
• The standing assumption "$\mathcal M$ contains at least one point with strictly positive $\mathbb E[S]$" is kept as a hypothesis, as printed, although the proof does not need it once $g_S(\omega_T)\ge0$ is part of (4).
• "One of the following conditions must hold" is an inclusive or.
• A trivializing formalization would drop the participation constraint from (4) (the statement is then false), or replace (4) by maximization over a set that may be empty; both are ruled out by IsEngagementMaximizer, which requires $\omega_T$ itself to be feasible.
• No library beyond Mathlib's real arithmetic is needed. Proofs of the milestones and the goal are welcome; the definitions are shared in spirit with mission II of this series, which keeps its own copy.

Selected references

• J. Kleinberg, S. Mullainathan, M. Raghavan, The Challenge of Understanding What Users Want: Inconsistent Preferences and Engagement Optimization, arXiv:2202.11776v3, 2023. https://arxiv.org/abs/2202.11776
• Same paper, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.03683

Motivation

A delivery company can assign each driver a permanent district instead of allowing every driver to serve the whole city. This makes dispatching simpler, but it raises a service question: if the districts receive almost equal shares of demand and travel workload, how different can their expected delivery times be? Carlsson, Liu, Salari and Yu study this question for a region partitioning policy in which one vehicle serves each district. Their Proposition 3 gives an explicit error bound for a partition whose shares are accurate within a tolerance ε. The proposition complements their exact equitability result, Theorem 6, by quantifying the effect of a partition that can only be computed approximately.

Setting

The service region R is a compact convex subset of the Euclidean plane, with depot x₀ ∈ R. Orders arrive at a rate λ and have locations distributed with density f on R. The density is nonnegative, Lipschitz on R, and normalized by ∫_R f(x) dx = 1. There are m ≥ 1 identical vehicles, each with speed v > 0 and capacity q ≥ 1. An order requires a mean on site service time s̄ ≥ 0. The positive constant β is the geometric constant in the paper's heavy traffic delivery time expression. A partition R₁, …, R_m covers R, with districts disjoint up to area zero; vehicle i serves R_i.

For a measurable district S, let p(S) = ∫_S f(x) dx be its share of demand. Its arrival rate is λ_S = λp(S), and its conditional density is f_S(x) = f(x)/p(S) when p(S) > 0. The paper uses two partition measures:

$$\mu_1(S)=\int_S\sqrt{f(x)}\,dx,\qquad \mu_2(S)=\int_S(\bar s vq+2\lVert x-x_0\rVert)f(x)\,dx.$$

The first controls the leading travel term. The second combines service time and radial travel from the depot. A partition is ε equitable when, for every district i and each j ∈ {1,2}, the difference between μ_j(R_i) and μ_j(R)/m has absolute value at most ε.

For vehicle count k, arrival rate a, region S, and density g, write the workload factor as

$$W(k,a,S,g)=\frac{a\bar s}{k} +\frac{2a}{kvq}\int_S\lVert x-x_0\rVert g(x)\,dx.$$

The heavy traffic expression from the paper's Theorem 3 is

$$L(k,a,S,g)=\frac{\beta^2a(1-1/q)^2 \left[\int_S\sqrt{g(x)}\,dx\right]^2} {2k^2v^2(1-W(k,a,S,g))^2}.$$

The comparison value is L* = L(m,λ,R,f). For district i, the value L_i = L(1,λ_{R_i},R_i,f_{R_i}) uses that district's own arrival rate, density, and workload factor.

Formalization targets

Proposition 3: approximate districts

For λ > 0 with W(m,λ,R,f) < 1, ε ≥ 0, and an ε equitable partition, define the corrected tolerance factor

$$\eta=\frac{\varepsilon}{ \min\left\{\mu_1(R)/m,\; \frac{vq}{\lambda}\left(1-\frac{\lambda\mu_2(R)}{mvq}\right) \right\}}.$$

When η < 1, the target is the two sided estimate

$$\lvert L_i-L^*\rvert\le \frac{4\eta}{(1-\eta)^2}L^* \qquad\text{for every }i.$$

The first milestone rewrites each district's Theorem 3 expression using μ₁(R_i) and μ₂(R_i). The next two milestones give upper and lower comparisons with L*. The final algebraic milestone evaluates the larger of the two relative deviations. These are the displayed steps on the paper's e companion pages ec6 and ec12–ec13.

The printed Proposition 3 uses max in the denominator defining η. Its proof requires min: when the two entries are 1 and 100 and ε = 0.1, a district can have L_i/L* = (1.1/0.999)² ≈ 1.212, while the printed η = 0.001 permits a deviation of only about 0.004. The correction is recorded in the theorem statements and audit notes.

Significance

The bound makes partition accuracy interpretable as a service guarantee. Once both shares are close enough that η < 1, every district's leading delivery time lies in a controlled interval around the flexible policy's benchmark. It states a guarantee for each district, rather than just for a demand weighted average, so it addresses unequal service across the region.

The authors prove the displayed comparison in their accepted manuscript. This mission formalizes the comparison between explicit heavy traffic expressions; it does not claim a new queueing theorem or a machine checked proof of the stochastic model. The reusable output is a precise Lean interface for spatial demand integrals, workload, conditional district densities, and perturbation bounds involving both numerator and denominator errors. The theorem items are proof targets.

Difficulty

The denominator responds to the μ₂ error in the opposite direction from the numerator's response to the μ₁ error. Bounding their ratio requires both the district workload and the lower numerator estimate to stay in their proper sign ranges. Simply squaring the ε share inequalities is invalid until those signs are known. The condition η < 1 supplies the required room; it also rules out a zero probability district under the other hypotheses. The printed choice of max for η fails to control the error in whichever of the two scales is smaller.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin 2), Lebesgue set integrals, and real valued leading terms. The density, region, depot, fleet parameters, and positive β are fixed while λ and ε vary. The source's compactness, convexity, Lipschitz density, normalization, positive vehicle count, speed, and capacity, and nonnegative mean service time are included in a single standing predicate. A partition has null measurable pieces, pairwise disjoint almost everywhere, and exact union R; shared district boundaries have area zero. The goal also states λ > 0, global workload < 1, ε ≥ 0, and η < 1, matching the stable regime and the proof's small ε condition. Capacity q = 1 remains admitted: both leading terms then vanish and the inequality still holds.

The stochastic renewal arrivals, routing policy, and queueing process are outside this development. Theorem 3 supplies the paper's leading expression, applied separately to the full region and each district. Thus L_i and L* here are leading expressions at one fixed λ, not the underlying expected delivery time functions. A fixed positive ε makes η grow near the heavy traffic boundary, so the page's parenthetical “in heavy traffic” is read through the leading expressions used by its proof. The district value is formed from λ_{R_i} and f_{R_i}; it is not defined from the global benchmark or from the right hand side of the first milestone.

A complete proof will need standard facts about set integrals and square roots, the normalization of a conditional density, and inequalities for positive real denominators. The setting definitions can support other region partition comparisons. Contributions establishing these identities and the upper and lower estimates are welcome.

Selected references

• J. G. Carlsson, S. Liu, N. Salari, and H. Yu, Provably Good Region Partitioning for On-Time Last-Mile Delivery, accepted manuscript, SSRN 3915544; published in Operations Research 72(1), 91–109 (2024), DOI: 10.1287/opre.2021.0588. Proposition 3, printed p. 21; proofs on pp. ec6 and ec12–ec13.
• D. J. Bertsimas and G. J. van Ryzin, Stochastic and Dynamic Vehicle Routing with General Demand and Interarrival Time Distributions, Advances in Applied Probability 25(4), 947–978 (1993), DOI: 10.2307/1427801. Source of the heavy traffic expression cited as Theorem 3 in the Carlsson et al. manuscript.

Motivation

Platforms that rank content by engagement (time spent, items consumed) implicitly assume revealed preference: a user who stays longer is a user who is better off. Kleinberg, Mullainathan and Raghavan (arXiv:2202.11776, Management Science 2023, doi:10.1287/mnsc.2022.03683) model a user with inconsistent preferences, a forward-looking system 2 and an impulsive system 1, and show that engagement and utility can come apart. Because utility cannot be read off behavioural data, platforms also run post-session surveys. Section 5.1 of the paper asks what such surveys can reveal: if a survey gives an estimate of the utility $S$ of a session, does $\mathbb E[S\mid T=t]$ rise or fall with the session length $t$, and what does that say about the content? Theorem 5.1 answers this in terms of two content parameters, the span $q$ and the moreishness $p$.

Setting

A session proceeds in two phases (§2.1, pp. 5–7).

• Span. After each item, system 2 remains interested with probability $q$. The number of items it enjoys, $T_q$, has the geometric law on $\{1,2,\dots\}$: $\Pr[T_q=\tau]=q^{\tau-1}(1-q)$.
• Moreishness. Once system 2 is done, system 1 keeps the user on: with probability $p$ at each step, the first one included, it consumes one more item. With $T_p:=T-T_q+1$, $\Pr[T_p=k]=p^{k-1}(1-p)$ for $k\ge1$.
• $T_q$ and $T_p$ are independent, and the session length is $T=T_q+T_p-1\in\{1,2,\dots\}$. For $1\le\tau\le t$,

$$\Pr[T_q=\tau\cap T_p=t-\tau+1]=q^{\tau-1}(1-q)\,p^{t-\tau}(1-p).$$

• Utility. Each item system 2 enjoys has value of mean $\bar v$; every step costs the outside option $W$. The paper's equations (8)–(9) give

$$\mathbb E[S\mid T=t]=\bar v\,\mathbb E[T_q\mid T=t]-Wt,\qquad \mathbb E[T_q\mid T=t]=\frac{\sum_{\tau=1}^{t}\tau\Pr[T_q=\tau\cap T_p=t-\tau+1]}{\sum_{\tau'=1}^{t}\Pr[T_q=\tau'\cap T_p=t-\tau'+1]}.$$

The Lean development names these objects geomLaw (the law $g_r(k)=r^{k-1}(1-r)$, $k\ge1$), jointMass, condMeanTq (9) and condUtility (8), all in the namespace EngagementOpt.Survey. Write $f(t)=\mathbb E[S\mid T=t]$ and

$$\varphi(x)=\frac{x+1}{x}\left(1-\frac{\ln(x+1)}{x}\right)$$

(phi), the function of the paper's (11) and Lemma D.1.

Formalization targets

Goal: Theorem 5.1 (p. 19)

Assume $0<p<1$, $0<q<1$, $\bar v\ge0$ and $W>0$. For integer session lengths $t\ge1$:

1. $q=p$: $\;\bigl(\forall t\ge1,\ f(t)<f(t+1)\bigr)\iff \bar v>2W$.
2. $q>p$: (a) if $\bar v>2W$ then $f(t)<f(t+1)$ for all $t\ge1$; (b) if $\bar v>W$ there is $t^*$ with $f(t)<f(t+1)$ for all $t>t^*$.
3. $q<p$: (a) if $\bar v<2W$ then $f(t+1)<f(t)$ for all $t\ge1$; (b) there is $t^*$ with $f(t+1)<f(t)$ for all $t>t^*$.

The goal is the conjunction of the five claims.

Milestones, in proof order

• (9) with $p=q$ (p. 20): $\mathbb E[T_q\mid T_q+T_p=t+1]=\frac{t+1}{2}$.
• (10) (p. 21): $f(t)=\bar v\frac{t+1}{2}-Wt$ if $p=q$, and $f(t)=\bar v\bigl(\frac{t\beta^t}{\beta^t-1}-\frac1{\beta-1}\bigr)-Wt$ with $\beta=q/p$ if $p\ne q$.
• (11) (p. 21): extending (10) to real $s>0$, its derivative at $t$ is $\bar v\,\varphi(\beta^t-1)-W$.
• Proof of Lemma D.1 (pp. 40–41): $\varphi(x)\to\frac12$ as $x\to0$; $(x+2)\ln(x+1)-2x$ is $\ge0$ for $x>0$ and $\le0$ on $(-1,0)$.
• Lemma D.1 (p. 40): $\varphi(x)\ge\frac12$ for $x>0$ and $\varphi(x)\le\frac12$ for $-1<x<0$.
• Proof of Theorem 5.1 (p. 22): $\varphi(x)\to1$ as $x\to\infty$ and $\varphi(x)\to0$ as $x\to-1^+$.

Significance

The theorem describes how span and moreishness affect the relation between survey utility and session length. When $q>p$ and $\bar v>W$, utility eventually increases; when $q<p$, it eventually decreases. In the symmetric case $q=p$, the sign is decided by $\bar v$ against $2W$ alone. These are conditional predictions for survey data, rather than a converse that identifies $q$ and $p$ from the sign by itself.

The result is proved in the paper; it has no machine-checked proof. Formalizing it checks the Bayes computation (9)–(10), including an arithmetico-geometric sum and a printed exponent slip on p. 20 ($p^{t+1}$ for $p^{t-1}$, harmless because it cancels), and the real-analytic Lemma D.1. It also makes explicit one hypothesis the printed theorem omits (below).

Difficulty

The closed form (10) needs the sum $\sum_{\tau=1}^t\tau\beta^{\tau}$ and care with $\beta^t-1$ in denominators. The main obstacle is that monotonicity is a statement about integer $t$, while the natural tool, the derivative $\varphi(\beta^t-1)$ of the real extension, lives on real $t$; the integer statement must be recovered from bounds on $\varphi$ over whole intervals, not at single points. Lemma D.1 is a two-level sign analysis of a function with a removable singularity at $0$, and the two limits at $\infty$ and at $-1^+$ are of L'Hôpital type. The obvious argument for 2(b), "$\varphi\to1>W/\bar v$", silently uses $\bar v>W$; without it, since $\varphi<1$ on $(0,\infty)$, the claim fails.

Formalization scope

• Explicit discrete model. (8) and (9) are taken as the definitions of $\mathbb E[S\mid T=t]$ and $\mathbb E[T_q\mid T=t]$; no measure-theoretic conditioning is involved. Independence of $T_q$ and $T_p$ is the product form of jointMass.
• Integer time in the goal. $t\in\mathbb N$, $t\ge1$ (the support of $T$). "Increases with $t$" is $f(t)<f(t+1)$, strictly; "for $t>t^*$" is $\exists t_0\in\mathbb N,\ \forall t>t_0$. Real $t$ and the real power $\beta^t$ appear only in the milestone (11).
• Hypotheses. $0<p<1$ and $0<q<1$ are the paper's standing assumptions; they exclude the degenerate $p=q=0$, where $T=1$ almost surely and Lean's $x/0=0$ would make claim 1 false. The paper's parameter space has $\bar v\ge0$ (p. 15). $W>0$ is implicit (§2.1 normalizes $W=1$). $\bar v>W$ in 2(b) is added: the proof uses it on p. 22 ("since $\bar v>W$ by assumption") and 2(b) is false without it.
• Domain of $\varphi$. Every statement about $\varphi$ restricts $x$ to $x>0$, $-1<x<0$, a punctured neighbourhood of $0$, the right neighbourhood of $-1$, or $x\to\infty$, so the junk values at $x=0$ and $x\le-1$ never enter.
• Ruled out. Stating the goal for real $t$, dropping $p,q>0$, or reading 1 as a one-way implication all give a different theorem.
• Infrastructure. Mathlib's Real.log, Real.rpow, HasDerivAt, Filter.Tendsto and finite sums suffice. The inequality $\ln(1+x)\ge 2x/(x+2)$ for $x\ge0$ is in Mathlib (Real.le_log_one_add_of_nonneg). Contributions of any milestone, of alternative discrete proofs of monotonicity that avoid the real extension, and of the full goal are welcome.

Selected references

• J. Kleinberg, S. Mullainathan, M. Raghavan, The Challenge of Understanding What Users Want: Inconsistent Preferences and Engagement Optimization, Management Science, 2023. arXiv:2202.11776v3 (cited version): https://arxiv.org/abs/2202.11776 ; https://doi.org/10.1287/mnsc.2022.03683
• G. S. Becker, K. M. Murphy, A Theory of Rational Addiction, Journal of Political Economy 96(4), 1988. https://doi.org/10.1086/261558