Operations Research

Motivation

Service systems such as public fast-charging stations for electric vehicles let each customer choose how long to be served. Lin, Shang and Sun (SSRN 3709573, 2020; later in Management Science, doi:10.1287/mnsc.2022.4474) study a firm that announces to every arriving customer the current wait time $w$ (the work already in the queue) and a price rate $p$ per unit of service time. The customer then decides whether to join and, if so, how long a service to buy. Queue pricing usually conditions on the queue length with random service times (Low 1974; Paschalidis and Tsitsiklis 2000; Kim and Randhawa 2018). Here the state is the wait time, and it moves deterministically between arrivals.

The firm maximizes long-run average revenue or social welfare. The optimality condition the paper derives is not an ordinary differential equation but a delay differential equation (DDE) that looks ahead: the value at $w$ depends on the value at $w + \mathtt t(p) > w$. This mission formalizes the paper's existence theorem for that equation.

Setting

A model has a usage utility $U$, a waiting cost $c$, a Poisson arrival rate $\lambda > 0$ and a maximum service time $C > 0$, under Assumption 1 (p. 7):

1. $U(t) \ge 0$, $U(0) = 0$, $0 \le U'(t) \le U'(0)$ and $U''(t) < 0$ on $[0, C]$;
2. $\frac{d^2}{dt^2}[U'(t)t] < 0$ on $[0, C]$;
3. $c(0) = 0$, $c'(w) > 0$ and $c''(w) \ge 0$ for $w \ge 0$.

At price $p \in [0, U'(0)]$ a joining customer chooses the service time $\mathtt t(p) = \min\{(U')^{-1}(p), C\}$ (5). They join when $U(\mathtt t(p)) - p\,\mathtt t(p) - c(w) \ge 0$. Three thresholds follow:

• $\bar w$ solves $U(C) = c(\bar w)$; above it nobody joins.
• $\Gamma(w)$, for $w \in [0, \bar w]$, is the highest price at which a customer still joins (Proposition 2).
• $\hat w$ and $L(w)$ (Proposition 1) describe when the marginal price $U'(t)$ still attracts a customer.

The per-customer value is $\mathbf v(p) - \alpha c(w)$, with $\mathbf v(p) = p\,\mathtt t(p)$, $\alpha = 0$ for revenue and $\mathbf v(p) = U(\mathtt t(p))$, $\alpha = 1$ for welfare (Lemma 1).

The optimality equations (12)–(15) ask for a constant $\mathsf g$ (the average rate) and a relative value function $V$ with

$$\mathsf g = -V'(w) + \lambda \max\Big\{\max_{p \in [0, \Gamma(w)]} \big[\mathbf v(p) - \alpha c(w) + V(w + \mathtt t(p)) - V(w)\big],\ 0\Big\}, \quad w \in (0, \bar w],$$ $$\mathsf g = \lambda \max\Big\{\max_{p \in [0, \Gamma(0)]} \big[\mathbf v(p) + V(\mathtt t(p)) - V(0)\big],\ 0\Big\}, \qquad \mathsf g = -V'(w) \ (w > \bar w), \qquad V(\bar w) = 0.$$

Algorithm 1 (p. 14) is a backward explicit-Euler shooting scheme. For a guess $g \ge 0$ and $N$ grid cells on $[0, \bar w]$, it starts from $V^g_N(w) = -(w - \bar w)g$ for $w \ge \bar w$. It then builds a piecewise-linear $V^g_N$ cell by cell from right to left. On the cell ending at $x$ the slope is $-g + K^g_N(x)$, where the slope adjustment $K^g_N(x)$ is $\lambda$ times the positive part of the inner maximum at $x$. The shooting value is $g_N = \min\{g \ge 0 : g \ge K^g_N(0)\}$ (23). Finally $\bar g = \lim_j g_{2^j}$ (24) and $V^{\bar g}(w) = \lim_j V^{\bar g}_{2^j}(w)$ (Proposition 6).

Formalization targets

Goal: Theorem 1 (p. 17)

$$\bar g = \lim_{j\to\infty} g_{2^j} \ \text{exists},\quad V^{\bar g}_{2^j}(w) \to V^{\bar g}(w)\ (w \ge 0),\quad (\bar g, V^{\bar g}) \text{ solves (12)–(15)},\quad V^{\bar g} \text{ is nonincreasing and concave on } [0, \bar w + C].$$

Milestones

The milestones follow the paper's proof in order:

• Thresholds and the value function (Propositions 1–3, pp. 8–11): uniqueness of $\hat w$ and $\bar w$, the characterization (8) of $\Gamma$, $\Gamma(0) = U'(0)$ with $\Gamma$ decreasing, and the bounds (V1)–(V2) on $\mathbf v$.
• The finite-$N$ scheme (Proposition 4, Lemmas 2, 3, 5): $V^g_N$ is concave and $K^g_N$ is nonincreasing; $K$ increases when the grid is refined and decreases in $g$; and $K^{U'(0)}_N \equiv 0$.
• The limits (Proposition 5, Lemma 6, Proposition 6): $g_{2^j}$ increases to $\bar g \le U'(0)$, the $V^{\bar g}_{2^j}$ are uniformly $\bar g$-Lipschitz, and they converge uniformly to a concave, nonincreasing, Lipschitz $V^{\bar g}$.
• The equations in the limit (Lemma 7, Propositions 7–8): $K^{\bar g}_{2^j}(0) \to \bar g$; the boundary condition (13); differentiability of $V^{\bar g}$ on $[0, \bar w]$ and the DDE (12).

Significance

Theorem 1 is the existence half of the paper's verification argument. Its Theorem 2 then shows that the constructed $\bar g$ equals the optimal long-run average rate over all predictable price processes. Its Theorem 3 reads the structure of the optimal price and service-time policies off $V^{\bar g}$. Without a solution of (12)–(15) neither result has an object to talk about. The construction also gives a convergent numerical method (Algorithm 1) for a class of look-ahead DDEs that standard ODE theory does not cover.

The proofs are written out in the paper's Appendix B, except Lemma 12, an internal step of Proposition 8 whose proof the authors leave out. None of it is machine-checked. A complete formalization would check every step of the shooting argument and supply the omitted lemma. It would also yield a reusable framework: Euler-type schemes for delay equations whose delay points forward, monotone in the grid and in a scalar parameter.

Difficulty

The obvious approach, Cauchy–Lipschitz, fails: (12) is not an initial-value problem. $V'(w)$ depends on $V$ on $[w, w + C]$, so the equation must be integrated backwards from $\bar w$, and then the value $\mathsf g$ is unknown. The shooting scheme fixes $g$, integrates backwards, and tunes $g$ so that the boundary condition (13) at $w = 0$ holds in the limit. For fixed $g$ the approximations need not converge as $N \to \infty$ (the slope at $0$ can diverge), so $g$ and $N$ must be coupled through $g_N$.

The hard step is Proposition 8. Each $V^{\bar g}_{2^j}$ has kinks at every grid point, yet the limit has to be differentiable. One has to show that the left and right derivatives of the concave limit coincide and equal the right-hand side of (12), which requires passing a maximum over a $w$-dependent price set to the limit.

Formalization scope

All declarations live in the namespace WaitTimePricing.Existence, and only Mathlib is imported. Conventions:

• $U, c : \mathbb R \to \mathbb R$ are $C^3$ and $C^2$ on $\mathbb R$, a disclosed strengthening of "three/two times differentiable". Assumption 1's inequalities are imposed exactly on $[0, C]$ and $[0, \infty)$. $\lambda > 0$ and $C > 0$ are added; the paper uses them without stating them.
• $\mathtt t(p) = \sup\{t \in [0, C] : p \le U'(t)\}$, meaningful for $p \in [0, U'(0)]$. $\hat w$, $L(w)$, $\bar w$ and $\Gamma(w)$ are defined by their characterizing sets, not by closed forms. Propositions 1–2 are theorems about these sets.
• The objective is one of Lemma 1's two cases. The paper's remark that any $\mathbf v$ satisfying (V1)–(V2) would do is not formalized, because it silently needs continuity of $\mathbf v$.
• Every "max" in (12), (13), (19) and (22) is a real supremum over $[0, \Gamma(w)]$. For the continuous $V$ used here this set is nonempty and bounded, and the supremum is attained.
• $V'$ is never a default-valued derivative. (12) and (14) assert that $V$ has the prescribed derivative, two-sided for $w \in (0, \bar w]$ and $w > \bar w$; Proposition 8 states the case $w = 0$ with a right derivative.
• Algorithm 1 is a recursion over the passes of its loop, with $N \ge 1$. The initialization (16) is extended from $[\bar w, \bar w + C]$ to $[\bar w, \infty)$ so that (14) can hold as printed on $(\bar w, \infty)$. Only values on $[0, \bar w + C]$ enter the loop, so the construction is unchanged.
• $\bar g$ and $V^{\bar g}$ are defined as limits that take a default value when the limit does not exist. Propositions 5–6 and the goal assert the convergence.
• "Decreasing" is nonincreasing everywhere (including $\Gamma$, Proposition 2(iii)), the reading the proofs establish.

Trivializations ruled out. The goal names the paper's $\bar g$ and $V^{\bar g}$ together with their convergence, not an arbitrary solution and not default values of undefined limits. It cannot be met at a kink through a default-valued derivative. Its inner maxima cannot vanish through an empty or unbounded set. $\Gamma$ and $\mathtt t$ are not closed forms that would make (8) true by definition. The weaker statement "some $(\mathsf g, V)$ solves (12)–(15)" is not the goal.

Contributions are welcome at every milestone. Reusable pieces include monotonicity of a max-operator under backward induction, Dini-type uniform convergence of monotone sequences of equi-Lipschitz concave functions, and the differentiability of a concave limit of piecewise-linear functions. Theorem 2 (optimality over predictable controls) and Theorem 3 (policy structure) are outside this mission. Theorem 3 appears to fail as printed when $\bar g > U'(C)$.

Selected references

• C.-A. Lin, K. Shang, P. Sun, Wait Time Based Pricing for Queues with Customer-Chosen Service Times, SSRN 3709573, version of October 12, 2020. https://ssrn.com/abstract=3709573 (journal version: Management Science, https://doi.org/10.1287/mnsc.2022.4474)
• D. W. Low, Optimal dynamic pricing policies for an M/M/s queue, Operations Research 22(3), 1974. https://doi.org/10.1287/opre.22.3.545
• I. C. Paschalidis, J. N. Tsitsiklis, Congestion-dependent pricing of network services, IEEE/ACM Transactions on Networking 8(2), 2000. https://doi.org/10.1109/90.842140
• J. Kim, R. S. Randhawa, The value of dynamic pricing in large queueing systems, Operations Research 66(2), 2018. https://doi.org/10.1287/opre.2017.1668
• D. P. Bertsekas, Dynamic Programming and Optimal Control, 2nd ed., Athena Scientific, 2000. http://www.athenasc.com/dpbook.html

Motivation

Firms that collect data on individual consumers can price each one separately. This is personalized pricing (PP): targeted coupons, individualized offers, prices that depend on a customer's browsing or purchase history. Whether competing firms gain from this ability is a long-standing question in industrial organization. When firm positions are fixed, the classical answer is that they do not. Each firm adopts PP because it is individually rational, the targeted offers intensify price competition for every consumer, and both firms end up worse off: a prisoner's dilemma (Thisse and Vives 1988; Shaffer and Zhang 1995; Bester and Petrakis 1996; Choudhary et al. 2005).

Li, Wang and Nault ask what happens when firms also choose where to position their products, so that differentiation itself responds to the availability of PP. Their answer for the costless case is that PP makes things worse for the firms twice over. The firms still adopt it, and it also draws them towards the centre of the market, where competition is fiercest. This mission formalizes that result, Proposition 1 of their paper, together with the stage-3 and stage-2 analysis it rests on.

Setting

A unit mass of consumers is uniformly distributed on the interval $[0,1]$. Each buys one unit. The reservation value is large enough that every consumer buys, so the market is covered. Two firms $A$ and $B$ choose positions $x_A,x_B\in\mathbb R$; positions outside $[0,1]$ are allowed. A consumer at $x$ who buys from firm $j$ pays the price plus a misfit cost $t(x-x_j)^2$, where $t>0$ measures taste heterogeneity. The misfit advantage of firm $i$ over firm $j$ at $x$ is

$$\operatorname{adv}_t(x_i,x_j;x)=t(x-x_j)^2-t(x-x_i)^2 ,$$

the amount by which the consumer at $x$ prefers $i$ to $j$ at equal prices.

The game has three stages:

1. the firms choose positions simultaneously;
2. each firm decides whether to implement PP (here at zero cost);
3. the firms set prices.

A firm without PP charges one uniform price; a firm with PP charges a price $p_j(x)$ to each consumer $x$. When both or neither firm has PP, prices are chosen simultaneously. When only one firm has PP, the uniform-price firm moves first and the targeting firm responds.

The three stage-3 outcomes are:

• Both firms implement PP. Every consumer is contested à la Bertrand: the firm with the positive advantage charges that advantage and the other charges $0$, so firm $i$ earns $\pi^{PP}_t(x_i,x_j)=\int_0^1\max\{0,\operatorname{adv}_t(x_i,x_j;x)\}\,dx$.
• Only firm $j$ implements PP. The leader $i$ charges $p$ and keeps the consumers with $p<\operatorname{adv}_t(x_i,x_j;x)$; an indifferent consumer buys from the targeting firm. The leader earns $p$ times that share, and an optimal leader price maximizes this over $p\in\mathbb R$. The follower charges each consumer it wins $p-\operatorname{adv}_t(x_i,x_j;x)$.
• Neither firm implements PP. Each firm's share is the set of consumers with a strictly lower full price at that firm, plus half of any ties. A price equilibrium is a pair of uniform prices from which neither firm gains by deviating to any real price.

Formalization targets

Goal: Proposition 1

For every $t>0$:

$$(x_A,x_B)=\Big(\tfrac14,\tfrac34\Big)\ \text{is the unique position equilibrium with } x_A\le x_B,\quad \text{both firms implement PP},\quad \pi_A=\pi_B=\frac t8 .$$

Here a position equilibrium means that no firm can raise its both-PP profit $\pi^{PP}_t$ by moving to any point of $\mathbb R$. "Both firms implement PP" means PP is strictly dominant for each firm at these positions in the stage-2 game.

Milestones

1. Both-PP profits (Appendix A, p. 33). For $x_A\le x_B$ with $0\le x_A+x_B\le 2$: $\pi^{PP}_t(x_A,x_B)=t(x_B-x_A)(x_A+x_B)^2/4$ and $\pi^{PP}_t(x_B,x_A)=t(x_B-x_A)(2-x_A-x_B)^2/4$.
2. One-sided PP (Appendix A, pp. 33–34). The uniform leader's unique optimal price is $t(x_A+x_B)(x_B-x_A)/2$ when $B$ targets, and its mirror when $A$ targets. The profits are those of Table 3: $/8$ and $/16$.
3. Uniform prices (§4, Stage 3, pp. 8–9). $p_A=t(x_B-x_A)(2+x_A+x_B)/3$ and $p_B=t(x_B-x_A)(4-x_A-x_B)/3$ form a price equilibrium, with profits $/18$.
4. Lemma 1, dominance (p. 10). For $x_A<x_B$ and $0<x_A+x_B<2$, PP is strictly dominant for both firms.
5. Lemma 1, prisoner's dilemma (p. 10). For $2(5-3\sqrt2)/7<x_A+x_B<2(2+3\sqrt2)/7$, both firms earn less when both implement PP than when neither does.

Significance

The result. In the uniform-pricing benchmark of the same paper the firms locate at $-1/4$ and $5/4$, outside the market, and earn $3t/4$ each: excess differentiation softens price competition. Proposition 1 shows that costless PP reverses this. The firms move to the quartiles, differentiation falls from $3/2$ to $1/2$, and each firm's profit falls to $t/8$, a loss of 83.3%. The fixed-position prisoner's dilemma is therefore not the whole cost of PP: endogenous positioning adds a second, larger loss. The positions $1/4,3/4$ also minimize total misfit cost, so the result separates firm profits from social efficiency. The costly-PP analysis of the paper (its Propositions 2–4) and the short-run positioning variant (Proposition 5) take these subgame outcomes as their starting point.

Formalizing it. The paper's proofs are short computations, and several are only asserted ("solving firm A's profit maximization problem we obtain", "straightforward to analyze and is omitted"). The formalization makes explicit what the page leaves implicit: the ranges of positions on which each closed form holds, the uniqueness of the leader's optimum that makes the follower's profit well defined, and deviations across the rival in the position game. To our knowledge none of these results has been machine-checked.

Difficulty

Each stage-3 outcome is an optimization over a market share that is a clipped linear function of the price. The first-order conditions on the page describe only the interior branch. A complete argument has to rule out the corners: a price at which the firm serves everyone or no one, negative prices, and coincident firms where ties matter.

The position game is harder than calculus on the closed forms. Those formulas hold only for $0\le x_A+x_B\le 2$, while a deviation can take a firm anywhere on $\mathbb R$, including past its rival, where the firms' roles are swapped and different formulas apply. Uniqueness requires showing that every ordered pair outside the interior region leaves some firm with zero profit and a profitable move.

Both-PP profits are integrals of a positive part, so every evaluation involves a case split at the midpoint $x_0=(x_A+x_B)/2$.

Formalization scope

All objects live in the namespace PPDifferentiation.Costless and are defined from primitives in one Setting file. Profits are integrals ∫ x in (0:ℝ)..1, … or real prices times the Lebesgue measure of a consumer set intersected with $[0,1]$. No stage-3 profit is defined by its closed form. Optimality is a predicate (IsLeaderOpt, IsPriceNE), never an sSup, and every statement quantifying over optima also asserts that one exists.

Committed conventions:

• the reservation value $v$ is omitted (full coverage; it cancels from every profit);
• prices are unsigned reals;
• positions and deviations range over all of $\mathbb R$;
• under one-sided PP the indifferent consumer buys from the targeting firm, and under uniform prices ties are split half-half.

The page states Lemma 1 "for any firm locations $x_A\le x_B$". The formalization poses each closed form on the range where it holds: $0\le x_A+x_B\le 2$ for the both-PP profits, $0<x_A+x_B<4$ (and $-2<x_A+x_B<2$ for the mirror) for one-sided PP, $-2<x_A+x_B<4$ for uniform prices, and $x_A<x_B$, $0<x_A+x_B<2$ for dominance. As in the paper's proof, the position game of Proposition 1 uses the both-PP profits as stage-1 payoffs at every position pair.

A formalization in which $\pi^{PP}$ is defined as $t(x_B-x_A)(x_A+x_B)^2/4$, or in which deviations are restricted to one side of the rival, would make the goal a statement about a polynomial and is ruled out.

Contributions welcome: interval-integral evaluations of the positive part of a linear function, the optimization of $p\cdot\operatorname{clip}(a-bp)$ over $\mathbb R$, and the stage-1 deviation analysis. The first two are reusable in other Hotelling models.

The source is the authors' SSRN manuscript of August 3, 2021 (abstract 3881900). The published Management Science version may number or state results differently.

Selected references

• X. Li, X. (Shane) Wang, B. R. Nault, Is Personalized Pricing Profitable When Firms Can Differentiate?, working paper, SSRN abstract 3881900, version of August 3, 2021. https://ssrn.com/abstract=3881900 (published in Management Science, 2023, https://doi.org/10.1287/mnsc.2021.02740)
• J.-F. Thisse, X. Vives, On the Strategic Choice of Spatial Price Policy, American Economic Review 78(1), 1988, 122–137. https://www.jstor.org/stable/1814702
• G. Shaffer, Z. J. Zhang, Competitive Coupon Targeting, Marketing Science 14(4), 1995, 395–416. https://doi.org/10.1287/mksc.14.4.395
• H. Bester, E. Petrakis, Coupons and Oligopolistic Price Discrimination, International Journal of Industrial Organization 14(2), 1996, 227–242. https://doi.org/10.1016/0167-7187(94)00474-9
• V. Choudhary, A. Ghose, T. Mukhopadhyay, U. Rajan, Personalized Pricing and Quality Differentiation, Management Science 51(7), 2005, 1120–1130. https://doi.org/10.1287/mnsc.1050.0383

Motivation

Households and small firms increasingly own distributed energy resources (DERs): rooftop solar, batteries, small generators. A household that owns a DER is a prosumer: it consumes electricity and can also sell its surplus. Whether prosumers should be allowed to sell into the wholesale market, directly or through an aggregator that pools many small units, is now a regulatory question: in the United States, FERC Order 2222 (2020) requires grid operators to open their markets to DER aggregators.

Gao, Alshehri and Birge (SSRN 3931052) study two questions about such aggregation. The first, the subject of a companion mission, is efficiency: does a profit-seeking aggregator distort the market outcome? The second, the subject of this mission, is market power. Conventional generators are few and large, and they can raise the market price by withholding supply. The paper asks whether letting prosumers sell back to the grid weakens that power, and shows in a stylized one-node model that it does: participation raises welfare, and the welfare lost to strategic generators is smaller with participation than without it.

The source is the authors' SSRN working paper (PDF of September 26, 2021). A revised version appeared in Manufacturing & Service Operations Management (2024, doi:10.1287/msom.2021.0539) and may number or state the results differently; every index here refers to the working paper.

Setting

The market has one node and no network constraints. There are finitely many prosumers $i$ and $N\ge1$ identical generators $j$.

• Prosumer $i$ owns a capacity $C_i\ge0$ and has the quadratic utility of consumption $u_i(z)=a_iz^2+b_iz$ with $a_i<0$. Write $C=\sum_iC_i$.
• Every generator has the true linear cost $c_j(y_j)=\alpha y_j$ with $\alpha>0$.
• With participation, prosumer $i$ chooses a net purchase $z_i>-C_i$ (negative $z_i$ is a sale). Without participation, it can only buy, $d_i\ge0$.

At a market price $\lambda$, a prosumer is a price taker: it maximizes $u_i(C_i+z)-\lambda z$ over its feasible purchases. A price $\lambda$ clears the market at total generator supply $y$ if the prosumers' optimal responses sum to $y$.

Four welfare numbers are compared.

• $\mathcal W^T$ is the optimal welfare of the dispatch problem (49): maximize $\sum_iu_i(C_i+z_i)-\sum_j\alpha y_j$ over $z_i>-C_i$, $y_j\ge0$ with $\sum_jy_j=\sum_iz_i$. This is the outcome when generators bid truthfully.
• $\mathcal W^{TN}$ is the same with $d_i\ge0$ in place of $z_i$, problem (69).
• $\mathcal W^S$ and $\mathcal W^{SN}$ are the true welfares at a strategic outcome: a symmetric pure equilibrium of the generators' quantity game. Each generator supplies $q\ge0$; the price is the one that clears the market at total $Nq$; and no single generator gains by changing its supply to any $q'\ge0$ while the other $N-1$ keep $q$, with the price then clearing the market at $q'+(N-1)q$.

Assumption 5 collects the hypotheses: $a_i<0$, $\alpha>0$, at least one prosumer with $2a_iC_i+b_i>\alpha$, and two clauses the paper states informally, made precise as H1 (the participation clearing price at zero supply, $(C+\sum_lb_l/(2a_l))/\sum_l1/(2a_l)$, lies below every $b_i$) and H2 ($-C+\sum_i(\alpha-b_i)/(2a_i)>0$, the efficient supply is positive).

Formalization targets

Goal: Theorem 3 (p. 27)

$$\mathcal W^T\ge\mathcal W^{TN},\qquad \mathcal W^S\ge\mathcal W^{SN},\qquad \mathcal W^T\ge\mathcal W^S,\qquad \mathcal W^{TN}\ge\mathcal W^{SN},$$ $$\mathcal W^{TN}-\mathcal W^{SN}\ge\mathcal W^T-\mathcal W^S,$$

where every inequality involving a strategic welfare holds for every strategic outcome of the model concerned.

Milestones

1. Proposition 5: the truthful optimum with participation, the price $\lambda^T=\alpha$, and $\mathcal W^T=\alpha C-\sum_i(b_i-\alpha)^2/(4a_i)$.
2. (58): the clearing price with participation, $\lambda^S(y)=(y+C+\sum_ib_i/(2a_i))/\sum_i1/(2a_i)$ for $y\ge0$.
3. (60) and (64): the strategic outcome with participation is unique, with $y^S_j=(-C+\sum_i(\alpha-b_i)/(2a_i))/(N+1)$.
4. Proposition 7: the truthful optimum without participation and $\mathcal W^{TN}$.
5. (81): at every strategic outcome without participation, the per-generator supply is the active-set formula, and it is positive.
6. Proposition 9: the four welfares relative to $\mathcal W_0=\sum_iu_i(C_i)$.
7. (93), (95): the price rises $\delta=\lambda^S-\alpha$ and $\delta^N=\lambda^{SN}-\alpha$.
8. Proposition 10: the explicit gaps $\mathcal W^T-\mathcal W^{TN}$, $\mathcal W^T-\mathcal W^S$, $\mathcal W^{TN}-\mathcal W^{SN}$.

Significance

The result. Theorem 3 gives a policy argument in welfare terms. Opening the market to prosumer sales, directly or through an aggregator, never lowers welfare in this model, whether the generators behave competitively or strategically. More specifically, the deadweight loss caused by the generators' market power, $\mathcal W^T-\mathcal W^S$, is smaller than its counterpart without participation. Prosumer sales make the residual demand that generators face more elastic, and the theorem quantifies the effect through the explicit gaps of Proposition 10. Together with the companion efficiency result (the profit-seeking aggregator is fully efficient), it supports allowing DER aggregation in wholesale markets.

Formalizing it. The result is proved in the paper, by explicit computation. To our knowledge none of it has been machine-checked. A formal development adds two things beyond confirming the algebra. First, it fixes the solution concept: welfares are optimal values, prices are market-clearing prices, and strategic outcomes are equilibria with unilateral deviations, not closed forms read off first-order conditions. Second, it makes explicit the facts the paper uses without stating them: the open constraint $z_i>-C_i$ never binds, the no-participation outcome lies on one linear piece of a kinked inverse demand, and its active set is nonempty.

Difficulty

With participation, everything is affine: the inverse demand is linear and the Cournot outcome is the textbook one. The difficulty is the model without participation. There the inverse demand, obtained from prosumers who can only buy, is piecewise linear and convex, with a kink each time one more prosumer starts buying. The equilibrium is characterized by the fixed point (81) on an active set that depends on the equilibrium itself. Two obvious shortcuts fail. One cannot take the paper's sorted closed form (86) as the definition of $\mathcal W^{SN}$, because it is only valid at an equilibrium. One cannot assume an equilibrium exists either: numerical computation finds parameters satisfying Assumption 5 for which the no-participation game has no symmetric pure equilibrium, and others for which it has several. So (46b), (46d) and (46e) have to hold for every strategic outcome, whichever active set it uses. Comparing the two models then needs the active-set identities (95) and (96d) at each such outcome.

Formalization scope

All quantities are real. Prosumers are a Fintype index ι; generators are Fin N, and Assumption5 includes 1 ≤ N. u a b i z = a i * z ^ 2 + b i * z. The definitions are:

• WT and WTN: the sSup of the welfare over the feasible sets of (49) and (69). Propositions 5 and 7 show that both suprema are attained.
• IsRespP and IsRespN: price-taking optimal responses, over the open set $z>-C_i$ and over $d\ge0$.
• ClearsP and ClearsN: market clearing.
• IsStratP and IsStratN: symmetric equilibria with unilateral deviations to any $q'\ge0$, against every clearing price at the deviation total.
• welS and welSN: the true welfare $\sum_iu_i(C_i+z_i)-N\alpha q$.

Hypotheses added to or read into the paper:

• H1 and H2 (Assumption 5's informal clauses), and $C_i\ge0$. The paper's §5.4 example ($a_i=-0.1$, $b_i=10$, $C=(10,30)$, $\alpha=5$) satisfies them, which a verification file checks.
• The paper's strategic generators bid tilted cost functions that implement the quantity equilibrium (Lemmas 5 and 8). That bid layer is not modelled: the strategic outcome is the quantity equilibrium itself, at which the paper evaluates $\mathcal W^S$ and $\mathcal W^{SN}$.
• Existence of a strategic outcome without participation is not claimed, because the paper does not prove it and it can fail.

No welfare, price or equilibrium is defined by its closed form. Defining $\mathcal W^T$ by (51), the price by (58) or the equilibrium by (60) would make the milestones definitional and the goal an algebraic identity about unverified objects. For the same reason the strategic outcome quantifies over unilateral deviations, not over symmetric profiles.

A complete development needs only elementary real analysis: maximization of concave quadratics, finite sums, and a case analysis on the active set. The definitions of price-taking response, market clearing and symmetric quantity equilibrium against a clearing correspondence can be reused for other single-node market models. Proofs of any milestone are welcome, as are alternative arguments for (46b) and (46e) that avoid the closed forms.

Selected references

• Z. Gao, K. Alshehri, J. R. Birge, Aggregating Distributed Energy Resources: Efficiency and Market Power, working paper, SSRN abstract 3931052 (PDF of September 26, 2021). https://ssrn.com/abstract=3931052
• Z. Gao, K. Alshehri, J. R. Birge, Aggregating Distributed Energy Resources: Efficiency and Market Power, Manufacturing & Service Operations Management, 2024. https://doi.org/10.1287/msom.2021.0539
• 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 (cited as FERC 2020 in the working paper, p. 2). https://ssrn.com/abstract=3931052

Motivation

Private equity funds ask investors to commit capital before the timing of their own cash needs is known. If an investor needs liquidity before the fund pays out, selling a partnership claim can be more useful than holding it to maturity. The price at which such claims trade therefore affects both the return investors demand when a fund is raised and the way fund managers schedule capital calls. Maurin, Robinson, and Strömberg study these two markets together in A Theory of Liquidity in Private Equity. The mission follows the authors’ December 2020 working-paper draft, whose Proposition 3 characterizes equilibrium when L-fund claims can trade in a secondary market.

Setting

A unit mass of general partners (GPs) each has wealth $A$ and raises one fund of size $I>A$. The fund makes two independent investments. A share $x$ is invested at the first date and $1-x$ at the second. Each unit succeeds with probability $p$ if the GP works, pays $R$ when successful, and otherwise pays zero. Shirking lowers the success probability to $q<p$ but gives the GP a private benefit $B$ per unit. A contract assigns the GP a fee to each pair of success outcomes. The fee is subject to limited liability and must give the GP enough incentive to work on both investments. The GP chooses the fee, $x$, and $I$ to maximize expected fee income, while meeting the investors’ promised return and the constraint that they will honor the second capital call.

The limited partners (LPs) have total capital $K$. A fraction $\mu_H$ belongs to type H and the rest to type L. With probability $\lambda$, a common liquidity shock makes period-two proceeds less useful at period one. Type $i$ values a unit of those later proceeds at $\delta_i$, with $0<\delta_L<\delta_H<1$. Type H is therefore more willing to hold an illiquid claim. Each LP chooses whether to supply capital to a primary fund or keep cash, and a cash holder may buy fund claims after the shock.

The secondary market has one actively traded asset: an L-fund claim. Its price is $P_L$ and its promised expected payoff is $\bar R_{PE,L}$. L-LPs supply claims when the price reaches their reservation value $\delta_L\bar R_{PE,L}$. H-LPs buy them when the price is at most $\delta_H\bar R_{PE,L}$, using capital left after any primary H-fund commitment. The discount to net asset value is

$$D_L=1-\frac{P_L}{\bar R_{PE,L}}.$$

An equilibrium specifies both funds’ contracts and promised returns, the fractions of GPs raising each fund type, primary capital supply, and secondary claims sold and bought. Contracts must be globally optimal among feasible contracts at their quoted returns, and both markets must clear.

Formalization targets

Return gap and market clearing

At a discount $D_L\in[1-\delta_H,1-\delta_L]$, the minimum returns acceptable to L- and H-LPs are described by (C.5) and (C.6). Lemma 3 asserts that the gap between the H and L minimum returns grows strictly with the discount. The gap is zero at $D_L=1-\delta_H$ and positive above it. For interior discounts, the secondary clearing equation is

$$(I_L-A)P_L=\mu_H K.$$

These statements are milestones because they give solvers the return comparison and the equation that determines price when all claims sell.

Proposition 3: secondary-market equilibrium

Under the paper’s Assumptions 1–3 and 5–7, together with the capacity condition described below, the goal is a set of ordered capital-share thresholds

$$0<\mu_{H,1}<\mu_{H,2}<\mu_{H,3}<\bar\mu_H.$$

An equilibrium exists for every $\mu_H\in(0,1)$. H-funds are raised only at or above $\mu_{H,3}$; if both fund types are raised, their promised returns agree. At or below $\mu_{H,3}$, only L-funds are raised and their promised return is $1/(1-\lambda D_L)$. Equation (22) gives $D_L=1-\delta_L$ below $\mu_{H,1}$, a capital-clearing ratio between $\mu_{H,1}$ and $\mu_{H,3}$, and $D_L=1-\delta_H$ at the third threshold. It also describes the early capital call: the lower boundary $\hat x(\lambda,\delta_L)$ at small H capital shares, the binding no-default call in the middle, and an interval of undistorted optimal calls near the third threshold.

Significance

The result explains why more liquid investors may prefer to provide liquidity in the resale market instead of financing funds directly. It ties the observed secondary-market discount to the amount of H capital available to buy claims and identifies the ranges where that discount changes the GP’s early capital call. Without the return and clearing conditions, the discount would be an exogenous price rather than an equilibrium object.

The cited paper proves this characterization in its economic model; this mission asks for machine-checked proofs of the formal statements. The resulting definitions cover incentive-compatible partnership contracts, primary capital supply, and the secondary claims market. They can also support later formal work on the welfare comparison in Corollary 2. None of the goal or milestone statements is claimed to have a machine-checked proof here.

Difficulty

There are two linked optimization problems. A GP chooses a fee and an early call under incentive, limited-liability, and no-default constraints. LPs then compare the value of primary investment with cash that can be used to buy claims after the shock. Solving only the contract problem does not determine the secondary price: that price changes the LPs’ outside option and the no-default constraint at the same time. The return comparison in Lemma 3 and the capacity available to each LP type are central to ruling out an apparently attractive H-fund equilibrium.

Formalization scope

Lean represents amounts, probabilities, prices, and returns by real numbers. Fee schedules are functions on the four ordered pairs of investment outcomes; the source indexes them by cash flow, so two equal-cash-flow outcomes at $x=1/2$ are formally distinct. Fund size satisfies the multiplied identity $(pR-\bar f)I=\bar R(I-A)$ and $I>A$, avoiding a meaningless value from division by zero. An optimal contract is compared with every feasible contract at the same promised return. The secondary value of cash uses the two positive prices, and the discount is defined only from a positive L return.

The standing parameters impose $q>0$, $p\leq1$, strict Assumption 5 at $\delta_L$, and $B\leq p(p-q)R$ so a fee with the required incentives can satisfy limited liability. The equilibrium also specifies nonnegative GP fractions summing to one. A raised fund must maximize GP profit; at a profit tie either fund may be selected. The printed supply and demand schedules are extended by zero outside their quoted reservation-price range. These choices fix cases left implicit by the paper.

The goal adds a sufficient L-capital condition: at $\mu_{H,3}$, L-LP capital covers the maximum primary external-financing need. The printed Proposition 3 lacks this condition. Its Step 1 assumes L-LP participation binds, yet Assumption 3 bounds only total $K$; for permitted smaller $K$, L-LPs can be scarce and the printed return formula fails. The added condition is explicit in the goal rather than hidden in the equilibrium definition. Assumption 7 is also a goal hypothesis, since it is specific to the no-segmentation result.

Assumption 4’s capital-call relief argument, Appendix A’s alternative contracts, the option for no GP fund, and the dynamic interpretation in Section 5.2 are outside this mission. The no-default constraint of (4) is imposed directly. A proof must establish equilibrium existence as well as properties of all equilibria, so a vacuous equilibrium predicate cannot meet the target. Contributions to the contract, return-gap, and clearing milestones are welcome.

Selected references

• Vincent Maurin, David T. Robinson, and Per Strömberg, A Theory of Liquidity in Private Equity, Management Science, 2023. DOI: 10.1287/mnsc.2022.4612. The formal statements use the authors’ December 2020 working-paper draft, especially §§3–4, §6, and Appendix C.5–C.6.

Motivation

Many service platforms set a price paid by customers and a wage paid to the providers who serve them. A platform may instead announce how much of each transaction's price it will pass to providers, then choose prices after both platforms have announced their shares. These are different games: a price change in the second game changes both customer demand and provider pay. Hu and Liu's study of precommitments in two-sided competition asks which timing gives platforms a more favorable equilibrium. This mission isolates their comparison between a commission precommitment and no commitment, Proposition 3(b) of the submitted manuscript. The authors' Online Appendix, included in that manuscript, contains the proofs.

The comparison is useful where a platform must choose a contract with providers before it can adjust customer prices. It is not enough to know that either side of the market is competitive: the answer changes as demand-side and supply-side competition intensities move relative to each other. The mission makes the claimed parameter regions precise and ties them to equilibria of the two games.

Setting

There are two platforms, indexed by $i=1,2$, with rival $j\ne i$. Platform $i$ posts a consumer price $p_i$ and a provider wage $w_i$. Fix a potential market size $\Omega>0$. The demand substitution factor $\gamma\in[0,1)$ measures how a rival's price raises demand for platform $i$. The supply substitution factor $\beta\in[0,1)$ measures how a rival's wage draws providers away. The paper uses the positive part $[x]^+=\max\{x,0\}$:

$$d_i(p)=[\Omega-p_i+\gamma p_j]^+,\qquad s_i(w)=[w_i-\beta w_j]^+.$$

The number of completed matches is $z_i=\min\{d_i(p),s_i(w)\}$. Profit is $\pi_i=(p_i-w_i)z_i$. Unmatched consumers or providers generate no revenue. Keeping the positive parts matters when a platform chooses a price or wage that leaves one side of the market empty.

In mode P, both platforms choose their prices and wages simultaneously, and each can change its own price and wage together while its rival's choices stay fixed. In mode C, each platform first commits to a pay-out ratio $\alpha_i\in(0,1)$. The provider then receives $w_i=\alpha_i p_i$ per match and the platform keeps $1-\alpha_i$ of its price. After observing both ratios, the platforms choose prices. Their profit in this second stage is

$$\pi_i(\alpha,p)=(1-\alpha_i)p_i\min\{d_i(p),s_i(\alpha p)\}.$$

A subgame-perfect equilibrium in mode C specifies a price equilibrium after every admissible pair of ratios and an initial pair of ratios that resists unilateral deviation when prices are chosen again. The mission compares symmetric commission equilibria to the positive-profit equilibrium of mode P. In the paper's platform preference ranking, $X\succeq Y$ means that mode $X$ gives each platform a weakly higher price and profit, and a weakly lower wage and matching quantity, than mode $Y$.

Formalization targets

No commitment and commission outcomes

Lemma 1 gives the simultaneous price-and-wage outcome. Writing $D=4-3\beta-3\gamma+2\beta\gamma$, its price, wage, matching quantity, and profit are

$$p_P^*=\frac{3-2\beta}{D}\Omega,\quad w_P^*=\frac{\Omega}{D},\quad z_P^*=\frac{1-\beta}{D}\Omega,\quad \pi_P^*=\frac{2(1-\beta)^2}{D^2}\Omega^2.$$

Lemma F.2 says that second-stage commission prices equate demand and supply. Lemma 4 characterizes the symmetric commission equilibrium by the radical $\alpha^*$ in equation (7), its price $p_C^*=\Omega/[1-\gamma+(1-\beta)\alpha^*]$, and its profit in equation (9). These are the three milestones. The radical is transcribed exactly in the Lean definition associated with equation (7).

Proposition 3(b)

The goal compares the two equilibrium outcomes using all four components of the platform preference ranking:

$$\gamma\geq\beta\ \Longrightarrow\ C\succeq P;\qquad \gamma\ll\beta\ \Longrightarrow\ C\succeq P;\qquad \gamma\leq\beta\text{ and sufficiently close to }\beta\ \Longrightarrow\ P\succeq C.$$

The two informal proximity phrases are expressed by the existence of positive thresholds, with the threshold allowed to depend on $\beta$. At $\gamma=\beta$, both rankings can hold because the outcomes coincide. The goal also asserts that the equilibria being compared exist for every admissible parameter pair.

Significance

The result identifies when committing to a provider share yields a platform outcome that is preferable to choosing price and wage together. Its four-way comparison is stronger than a profit-only ranking: the associated prices, wages, and match counts all move in specified directions. It makes clear that the relative competition intensities on the two sides determine whether the timing of the provider contract helps or hurts platforms. Without the comparison, the closed-form equilibrium results for modes P and C would not say which contract timing platforms prefer.

The result is proved in the cited manuscript, with derivations in Online Appendix §F; it is not an open mathematical conjecture. The remaining work in this mission is a machine-checked Lean proof of the equilibrium statements and the parameter-region comparison. The development will also provide a reusable formal model of simultaneous and two-stage decisions in a two-sided market. No existing machine-checked proof of this particular comparison is identified in the local Prove2Me index.

Difficulty

A change in a commission ratio changes the wage at any given price, while the subsequent price decision changes both demand and the wage again. That coupling makes the comparison more delicate than ordering two prices by inspection. The commission equilibrium ratio contains a square root, and the ranking must establish the directions of four outcome quantities in several parameter regions. The apparent shortcut of comparing profits alone would leave three of Definition 1's required inequalities unresolved. The positive-part demand and supply functions also admit zero-match equilibria that complicate an unqualified uniqueness statement.

Formalization scope

The Lean development uses real-valued prices and wages, two platforms indexed by Fin 2, and all unilateral deviations in the stated strategy sets. Market size is positive, both substitution factors lie in $[0,1)$, and pay-out ratios lie in $(0,1)$. The paper does not spell out the strategy sets; these choices preserve the derivations in §3 and Appendix §F. The no-commitment uniqueness statement is restricted to equilibria where both platforms profit, because the literal unrestricted claim has zero-profit counterexamples. A second-stage strategy in mode C selects an equilibrium with positive profits for both platforms whenever one exists. This condition prevents off-path zero-profit punishments from making the printed symmetric SPE claim false.

The goal quantifies over equilibria derived from the demand, supply, match, and profit functions. It does not define an outcome to equal the paper's closed form, and it asserts equilibrium existence so that its universal comparisons have content. The radical for $\alpha^*$ is a named expression; Lemma 4, rather than its definition, establishes its equilibrium role. A full proof needs reasoning about unilateral deviations, positive-part functions, equilibrium existence and uniqueness, the radical expression, and real inequalities. The general Nash condition and the paper's market primitives are intended for reuse in other two-player platform games. Contributions addressing these foundations and any of the three cited milestones are within scope. Wage- and price-precommitment modes are outside this mission.

Selected references

• Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, submitted manuscript with Online Appendix associated with the 2023 publication, SSRN 3734828. Manuscript.
• Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, Manufacturing & Service Operations Management 25(2), 704–718, 2023. DOI.

Why out-of-sample utility risk matters

A portfolio chosen from historical returns can look attractive in the data used to construct it and deliver a different result when evaluated under the population return distribution. The gap is driven by estimation error in both the mean return and covariance matrix. A mean of future utility values describes average performance, but it does not describe how much that utility varies across possible estimation samples. Lassance, Martín-Utrera and Simaan study this variation for a portfolio that blends an estimated mean-variance choice with an estimated global-minimum-variance choice. Their closed-form variance makes the sampling risk of that blend an explicit function of market and sample parameters. The source for this mission is the authors’ SSRN manuscript, version dated August 18, 2023, including its Internet Appendix; appendix pages are cited as IA pages.

The market and the estimated portfolio

There are $N$ risky stocks. Their excess-return vector has population mean $\mu\in\mathbb R^N$ and positive-definite population covariance $\Sigma\in\mathbb R^{N\times N}$. The investor has risk aversion $\gamma>0$. A portfolio is a vector of weights $w$ whose entries sum to one. Its population mean-variance utility is

$$U(w)=w^\top\mu-\frac{\gamma}{2}w^\top\Sigma w.$$

Write $e$ for the vector of ones. The global-minimum-variance portfolio and its variance are $w_g=\Sigma^{-1}e(e^\top\Sigma^{-1}e)^{-1}$ and $\sigma_g^2=(e^\top\Sigma^{-1}e)^{-1}$. Its mean is $\mu_g=\mu^\top\Sigma^{-1}e\,\sigma_g^2$. The population matrix $B=\Sigma^{-1}(I-ew_g^\top)$ maps the mean vector to a zero-cost portfolio. The variance of that portfolio is $\psi^2=\mu^\top\Sigma^{-1}\mu-\mu_g^2/\sigma_g^2$. These quantities are computed from $\mu$ and $\Sigma$; they are not independent inputs. These definitions are equations (3)–(7) of the manuscript.

The investor observes $T$ independent return vectors $r_1,\ldots,r_T$, each with multivariate Gaussian law $\mathcal N(\mu,\Sigma)$. The sample mean is $\hat\mu=T^{-1}\sum_t r_t$, and the sample covariance is $\hat\Sigma=T^{-1}\sum_t(r_t-\hat\mu)(r_t-\hat\mu)^\top$. Replacing the population parameters in $w_g$ and $B$ by these estimates gives the sample GMV portfolio $\hat w_g$ and the sample zero-cost portfolio $\hat w_z=\hat B\hat\mu$. The estimated mean-variance portfolio is $\hat w^\star=\hat w_g+\gamma^{-1}\hat w_z$. At shrinkage intensity $\kappa\in[0,1]$, the portfolio under study is $\hat w^\star(\kappa)=(1-\kappa)\hat w_g+\kappa\hat w^\star$. Its out-of-sample utility, $U(\hat w^\star(\kappa))$, is evaluated using population $\mu$ and $\Sigma$. It is random because the weights depend on the sample. These choices are fixed by equations (9)–(12) and Assumption 2 of the manuscript.

Formalization targets

The goal is Proposition 1, equations (13)–(19). Under $N\ge2$ and $T>N+7$, it asserts that the utility has a finite second moment and that

$$\mathbb V[U(\hat w^\star(\kappa))] =\mathbb V[U(\hat w_g)]+\Delta(\kappa),\qquad \Delta(\kappa)=a_1\kappa^4+a_2\kappa^3+a_3\kappa^2+a_4\kappa.$$

The coefficients $a_1,\ldots,a_4$ and $\mathbb V[U(\hat w_g)]$ are the exact rational expressions in $T,N,\gamma,\sigma_g^2,\psi^2$ on pp. 14–15 of the manuscript. In particular, the result covers every $\kappa\in[0,1]$, including the sample GMV portfolio at $\kappa=0$ and the sample mean-variance portfolio at $\kappa=1$.

The milestones follow the quantities named in the authors’ proof, Section IA.10. Equation (IA43) gives the covariance matrix of the random weights, and (IA44) gives the variance of their population mean return. The jointly distributed mean-return and return-variance pair in (IA45)–(IA48) supplies the setting for two auxiliary moment identities, (IA53) and (IA57). Equations (IA49), (IA59), and (IA60) give the first and second moments needed for return variance and mean return; (IA68) gives their covariance. All are statements from the Internet Appendix, pp. IA35–IA39.

What the result supplies

The expression tells an investor how the sampling risk of utility changes with the shrinkage intensity, sample size, stock count, risk aversion, and the two population variance parameters. The later comparison of variance-minimizing, mean-maximizing, and robustness-maximizing intensities uses this formula. Without Proposition 1, those comparisons have no explicit OOSU risk function to analyze. The result is already proved in the paper; this mission asks for its Lean proof and for reusable formal statements of the associated Gaussian portfolio and moment identities. No machine-checked proof of this paper’s proposition is included in the draft.

Where the difficulty lies

The sample covariance is random and its inverse appears in the estimated weights. Taking the variance of utility therefore involves inverse-covariance terms and moments beyond those needed for expected utility. The requirement $T>N+7$ is tied to existence of the fourth negative moment of a chi-squared variable in (IA57). A direct calculation that replaces random weights by their population counterparts loses the dependence on the estimation sample. A calculation from separate marginal laws also does not determine the covariance between mean return and return variance; the representation in (IA47)–(IA48) describes them jointly.

Formalization scope

The Lean market uses vectors Fin N → ℝ, matrices indexed by Fin N, and returns in EuclideanSpace ℝ (Fin N) to use Mathlib’s multivariate Gaussian law. The sample has Fin T observations on a probability space. Its covariance divisor is exactly $T$, as in (9). The standing assumptions are $N\ge2$, $T>N+7$, $\Sigma\succ0$, $\gamma>0$, and independent, identically distributed Gaussian returns. Every theorem about a variance or covariance explicitly asserts finite second moments; expectation statements explicitly assert integrability. The source’s finite-variance convention is thereby represented without Lean’s default value for a nonintegrable variance.

The left side of the goal is the probability-theory variance of utility under the sampling law. It is not defined by the closed formula. Likewise $\sigma_g^2$, $\mu_g$, and $\psi^2$ are computed from the market; independence is part of the sampling hypothesis. In the auxiliary representation, the chi-squared law is the squared norm of independent standard normals. The zero-degree cases and footnote 6’s $N=2,3$ rules are encoded explicitly. Mathlib’s matrix inverse and real division are total operations; their values on singular sample covariances or zero denominators do not alter the distributions because those events have probability zero under the stated assumptions. Contributions establishing the sample-covariance distribution, the joint representation, the negative moments, and the final variance identity are within scope and can support other Gaussian portfolio results.

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, subsequently in Management Science (2024). SSRN 3855546; DOI 10.1287/mnsc.2023.00178.

Why compare subsidy formats?

Governments sometimes pay crop producers to increase supply. A payment for each unit planted and a payment for each unit harvested create different incentives when farmers have different yields. An agency choosing among those formats needs to know how much it must spend to attain the same total output. Fan, Feng, Li, Shanthikumar, and Wu study that question in an agricultural Cournot market and compare four programs: planting-only, harvesting-only, combined, and selective subsidies. Their Proposition 10 orders the minimum budgets required by those programs, with the order of the two single subsidies changing at a specified output threshold. The source for this mission is the 2023-03-18 SSRN version of their paper; the proof is in Online Appendix A.

The comparison matters because the payment format changes both who receives money and how much each farmer produces. The government seeks a target output, while each farmer chooses output in response to the market price and the payment offered. A budget comparison therefore has to account for the farmers' equilibrium response, rather than compare payment rates alone. The paper's Section 5 and Proposition 10 give the target and the resulting ordering.

Market and government programs

There are $N>0$ farmers. Farmer $j$ plants $x_j=z_jq_j$ units of input to harvest $q_j$ units of output, so $z_j$ is an input-to-output ratio. The farmers are indexed in nondecreasing order of $z_j$. Planting costs $c_P$ per input unit and harvesting costs $c_H$ per output unit. If total output is $Q=\sum_jq_j$, the market-clearing price is $p(Q)=\alpha-\beta Q$, with $\alpha,\beta>0$. An output profile is a Cournot equilibrium when every $q_j$ is nonnegative and no farmer can earn more by changing its own output while the other outputs stay fixed. These are the objects in the paper's Section 3 and equation (1).

A subsidy profile gives farmer $j$ a payment $t_j$ for each unit of output. Under a combined subsidy $(s_P,s_H)$, $t_j=z_js_P+s_H$: the planting part pays for $z_jq_j$ units of input and the harvesting part pays for $q_j$ units of output. Under a selective subsidy, the farmer chooses one payment, so $t_j=\max(z_js_P,s_H)$. Planting-only sets $s_H=0$; harvesting-only sets $s_P=0$. The model allows negative subsidy rates, which are taxes. When the two selective payments tie, either choice pays the same amount. These formats come from Sections 3, 4.1, and 4.2.

The government budget at equilibrium is $\sum_jt_jq_j$. A profile is feasible when every farmer produces a positive quantity and $\sum_jq_j\ge\bar Q$, where $\bar Q$ is the target output. For each program, its optimum is the infimum of its feasible budgets. This matches the paper's requirement that output reach at least the target, and the all-active regime used for the comparisons. The average ratio and its variability are $\bar z=N^{-1}\sum_jz_j$ and $v_z=N^{-1}\sum_jz_j^2-\bar z^2$. The paper introduces these statistics in Section 3.

Formalization targets

Write $B_C,B_S,B_P,B_H$ for the least feasible budgets under the combined, selective, planting-only, and harvesting-only programs. The goal is Proposition 10:

$$\bar Q\le Q^C(c_P,0)\quad\Longrightarrow\quad B_C\le B_S\le B_P\le B_H,$$ $$\bar Q>Q^C(c_P,0)\quad\Longrightarrow\quad B_C\le B_S\le B_H\le B_P.$$

Here $Q^C(c_P,0)$ is the all-active expression for market output under a combined subsidy with planting rate $c_P$ and harvesting rate zero, as given by equation (5). In addition, $v_z=0$ implies $B_C=B_S=B_P=B_H$. The target exceeds the no-subsidy output, as required at the start of Section 5. All farmers are assumed to produce at the three closed-form designs of Proposition 8.

The milestones record the market quantities in Proposition 3, equations (2)–(6), the three minimizing designs of Proposition 8, and the single-subsidy budget difference in the proof of Proposition 10, Online Appendix A, page 13. A separate theorem item states the selective optimum's lower bound from the same proof.

What the result establishes

The ordering identifies a minimum-spending format for any target in the stated all-active regime. The combined program never requires a higher optimal budget than the other three, and the selective program never requires a higher optimal budget than either single subsidy. The threshold tells the government which single subsidy is cheaper. When farmer input-to-output ratios have zero variability, the choice among all four formats has no budget effect. These conclusions are the specific content of Proposition 10, rather than a claim about all policy objectives or about equilibria with inactive farmers.

The mathematical result is proved in the paper. This mission asks for a machine-checked proof of its stated all-active comparison. It also creates reusable Lean definitions for a finite Cournot equilibrium with affine inverse demand, per-farmer subsidy payments, and budget optimization over equilibrium-feasible profiles. The formalization has not yet proved the goal or milestones; each theorem is offered as a statement for solvers. The paper's proofs are in Online Appendix A of the SSRN version.

Where the formalization is difficult

The government controls subsidy rates, but feasibility and spending are determined after farmers respond. The four programs therefore have different sets of possible payment vectors, and the output constraint may be met by several profiles. Comparing one chosen profile from each program does not by itself establish a comparison of their minima. The selective program adds another difficulty: farmers can receive different types of payments within the same equilibrium. The proof of Proposition 10 records a separate budget inequality for that program.

Formalization scope

Farmers are represented by Fin N, with Lean index $0$ corresponding to the paper's farmer $1$. A generic Cournot game is a separate definition; the agricultural market supplies its unit costs. Equilibrium is a best-response predicate over nonnegative real outputs. Subsidies are per-output payment vectors, and the government budget is the finite sum of payment times output. The combined program contains all pairs $(s_P,s_H)$; its definition does not fix the optimal planting rate $c_P/2$. The output constraint is $Q\ge\bar Q$, exactly as printed in Section 5. Subsidy rates and costs have no added sign restrictions.

The formalization explicitly assumes $N>0$, $\alpha>0$, $\beta>0$, nondecreasing $z_j$, and $z_j>0$. The last condition states the physical meaning of an input-to-output ratio and is a disclosed addition. For Proposition 10, $\bar Q$ is strictly above the no-subsidy output in the all-active regime, and the planting-only, harvesting-only, and combined designs of Proposition 8 each have an all-positive equilibrium. Every feasible budget set is restricted to all-active equilibria. This is the fixed-active-set reading of the paper's phrase “all farmers produce”; a variable-active-set version is outside this mission. The three design assumptions make the single-subsidy and combined feasible sets nonempty, and a single-subsidy profile also belongs to the selective program. The separate selective lower-bound theorem assumes that the paper's chosen optimal selective budget is attained. These conditions and the budget lower bounds ensure that real sInf represents a finite budget value.

The equilibrium formulas, optimality statements, and budget inequalities are proof obligations; none is built into the definitions. Contributions establishing those claims or reusable finite-game and finite-sum facts are in scope. Results on inactive farmers, random yields, or convex production costs are outside this mission.

Selected references

• Fan, T., Q. Feng, Y. Li, J. G. Shanthikumar, and Y. Wu, Output-Oriented Agricultural Subsidy Design, forthcoming in Management Science, SSRN version dated March 18, 2023, SSRN 4378693, DOI 10.1287/mnsc.2023.4749.

Motivation

A service platform makes decisions on two sides of a market. It charges consumers a price and pays independent providers a wage, then earns a margin only when it can match a consumer with a provider. Capacity is another decision available to the platform: it can limit how many matches it will carry, for example by limiting the active provider pool. Hu and Liu ask whether committing to this limit before setting price and wage changes the competitive outcome. Their submitted manuscript models this question for two competing platforms and states a two-sided counterpart of the quantity-precommitment result associated with Kreps and Scheinkman. The point matters for platform operations because a capacity decision can determine the price, wage, volume, and profit that emerge after both platforms react. Hu and Liu, submitted manuscript, §3.5.

Setting

There are two platforms, indexed by $i\in\{1,2\}$; $j$ denotes the other platform. The potential market size is $\Omega>0$. Each platform posts a consumer price $p_i\in\mathbb R$ and a provider wage $w_i\in\mathbb R$. Demand and supply are the positive parts

$$d_i(p)=[\Omega-p_i+\gamma p_j]^+, \qquad s_i(w)=[w_i-\beta w_j]^+,$$

where $[x]^+=\max\{x,0\}$. The demand substitution factor $\gamma$ and the supply substitution factor $\beta$ both lie in $[0,1)$. Higher rival prices raise a platform's demand; higher rival wages reduce its supply. A platform can serve only the smaller of its demand and supply. Its profit without a capacity limit is the margin $p_i-w_i$ times that number of matches. These are the manuscript's displays (1)–(3). Hu and Liu, submitted manuscript, pp. 8–9.

The first game is quantity competition. Each platform chooses a nonnegative matching quantity $z_i$. The prices and wages that clear demand and supply at those quantities are

$$p_i(z)=\frac{(1+\gamma)\Omega-z_i-\gamma z_j}{1-\gamma^2}, \qquad w_i(z)=\frac{z_i+\beta z_j}{1-\beta^2}.$$

A platform earns $(p_i(z)-w_i(z))z_i$. A quantity Nash equilibrium is a nonnegative vector $z$ at which neither platform can gain by choosing any other nonnegative quantity while the rival quantity stays fixed. The inverse price and wage appear in the proof of Lemma 6, where the profit function is written as (F.3). Hu and Liu, submitted manuscript, p. 14 and Online Appendix p. 32.

The second game is capacity precommitment. In stage one, each platform chooses a nonnegative capacity $q_i$, the most matches it can make. In stage two, both platforms simultaneously choose prices and wages. Platform $i$ then serves $m_i=\min\{d_i(p),s_i(w),q_i\}$ matches and earns $(p_i-w_i)m_i$. A second-stage Nash equilibrium lets a platform change its price and wage together. A subgame-perfect equilibrium specifies stage-two play after every admissible capacity vector and requires that no platform benefit from changing its stage-one capacity and then following the continuation for the changed vector. Hu and Liu, submitted manuscript, pp. 14–15 and Online Appendix §A.

Formalization targets

The goal is Proposition 1: capacity precommitment and quantity competition have the same equilibrium price, wage, matching quantity, and profit for each platform. Writing $q,\sigma$ for a capacity profile and its continuation plan, and $z$ for a quantity equilibrium, the target is

$$\forall i\in\{1,2\},\qquad \bigl(p_i(\sigma(q)),w_i(\sigma(q)),m_i(q,\sigma(q)),\pi_i(q,\sigma(q))\bigr) = \bigl(p_i(z),w_i(z),z_i,(p_i(z)-w_i(z))z_i\bigr).$$

The goal also asserts that an equilibrium of each game exists, so this comparison has actual outcomes to compare. Lemma 6 gives the unique quantity equilibrium and its closed forms. The subgame analysis in Online Appendix §A.1 gives a platform's best response to fixed rival price and wage. Lemma 7 states that demand and supply both equal committed capacity in the two-stage equilibrium. These three statements are the mission's milestones. Hu and Liu, submitted manuscript, pp. 14–15 and Online Appendix p. 1.

Significance

Proposition 1 supplies an operational interpretation of quantity competition in a market where each platform controls both consumer price and provider wage. A quantity outcome can arise through an earlier capacity choice followed by ordinary spot-market price and wage decisions. The conclusion covers four separate outcomes for each firm, so it supports comparisons of capacity policies in terms of what consumers pay, what providers receive, how many matches occur, and platform profit. The result is proved in the manuscript; its proofs are in Online Appendix §F of the same cited artifact. Hu and Liu, submitted manuscript, p. 15 and Online Appendix p. 33.

The formalization asks for machine-checked proofs of these known statements under explicit equilibrium conventions. It also creates reusable definitions for a two-sided market with positive-part demand and supply, a quantity game, and a two-stage capacity game. The paper's displayed formulas become auditable statements about every equilibrium of those games rather than numbers inserted into the definition of an outcome. No machine-checked proof of this specific proposition is asserted here.

Difficulty

The central issue is the full two-stage game. A stage-two platform changes price and wage jointly, and a stage-one capacity deviation leads to a new stage-two equilibrium. Checking a price deviation while holding wages fixed, or checking only capacities near a proposed equilibrium, does not establish the proposition. The positive parts in demand and supply also create zero-profit price-and-wage equilibria. Such equilibria can be used as off-path continuations and can change the set of stage-one equilibria. The formal target therefore selects positive profit for each platform whenever a subgame equilibrium permits it. The manuscript's Appendix §A distinguishes several regions of capacity profiles; this regime structure is part of the difficulty of proving a statement about all deviations. Hu and Liu, submitted manuscript, Online Appendix §§A.1–A.2.

Formalization scope

Lean uses Fin 2 for platforms and a named rival map. Prices and wages are real-valued. Capacities and chosen quantities are nonnegative reals. The standing parameters are $\Omega>0$ and $0\le\beta,\gamma<1$; these ranges keep the market-clearing denominators $1-\beta^2$ and $1-\gamma^2$ nonzero. Demand and supply retain the manuscript's positive-part operation even when it is inactive at a positive equilibrium.

A continuation plan maps every capacity profile to a pair of price and wage profiles. At every nonnegative capacity profile it must choose a second-stage Nash equilibrium. For each platform, if that subgame has an equilibrium in which it earns positive profit, the chosen equilibrium must give it positive profit. This includes a subgame in which its rival committed zero capacity. This selection is an explicit addition to the printed equilibrium language, needed because the unqualified statement admits zero-profit off-path punishments. The stage-one Nash condition evaluates a capacity deviation using the continuation plan at the deviated capacity. The manuscript does not specify strategy sets; the stated real and nonnegative domains make them explicit. The goal ranges over equilibria rather than defining outcomes from Lemma 6's closed forms, and it asserts existence to prevent a vacuous comparison.

Contributions can establish the market-clearing identities, the quantity equilibrium and its uniqueness, joint price-and-wage best responses, the capacity-binding result, and the existence and outcome claims of Proposition 1. The generic two-player Nash predicate and the positive-part market model are reusable beyond this mission.

Selected references

• Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, submitted manuscript (SSRN 3734828; TSpace), published in Manufacturing & Service Operations Management 25(2), 2023, DOI 10.1287/msom.2022.1173. Mission statements follow the submitted manuscript and its Online Appendix, not the journal pagination.

Motivation

In reward-based crowdfunding, a seller asks customers to pay before the product's quality is known to them. A high-quality seller can try to communicate private quality through the prices he posts. That signal is costly because a price that deters imitation may also reduce the seller's own expected revenue. Bolandifar, Chen, Kouvelis and Zhou study this tradeoff when a campaign must meet a financing target and a successful campaign leads to a later retail period (SSRN manuscript, §§3–5). Their model asks whether a high-quality seller can separate himself from a low-quality seller by committing in advance to both the crowdfunding price and the later retail price.

The manuscript treats price commitment separately from the case in which the seller chooses the retail price after the campaign. This mission concerns the commitment case, specifically Proposition 2 and the lemmas that support it. The theorem describes a separating equilibrium after applying the intuitive criterion: the high-quality seller chooses a lower crowdfunding price and a higher retail price than he would under full information. The cited artifact is the authors' SSRN manuscript dated 2022-05-30; its proofs are in Appendix A (manuscript, pp. 38–43).

Setting

There are two privately known product qualities, $0<q_L<q_H$. A seller commits to a price pair $x=(P_1,P_2)$, where $P_1$ is paid by crowdfunding backers and $P_2$ is charged in the regular selling period. The project needs a financing target $T>0$, so a feasible pair satisfies $P_1\ge T$ and $P_2>0$. Both period market sizes are normalized to one; production and salvage costs are zero, and future revenue is not discounted (manuscript, pp. 9–13).

All funding customers have the same taste $\theta_c$, uniformly distributed on $[0,1]$ and unknown to the seller. They believe quality is $q_j$ and back the campaign when $\theta_c q_j\ge P_1$. Thus success has probability $\max\{0,1-P_1/q_j\}$. After a successful campaign, true quality $q_i$ becomes known. A fraction $\alpha\in(0,1)$ of regular customers have the same taste as the funding customers; success updates their conditional taste distribution. The remaining fraction has independent uniform tastes. A customer in the regular period buys if taste times $q_i$ is at least $P_2$ (manuscript, pp. 10–11).

Write $\Pi^{ij}(P_1,P_2)$ for the seller's expected total profit when true quality is $q_i$ and customers believe $q_j$. The expressions $V^{ij}$ and $W^{ij}$ distinguish the regions in which returning customers buy for sure or with a conditional probability. Write $\Pi^{ij*}$ for the maximum of $\Pi^{ij}$ over feasible pairs. In particular, $\Pi^{L*}=\Pi^{LL*}$ is the low type's full-information payoff. These are outcomes of optimization, not inserted formulas (manuscript, pp. 22–24, (7)–(11)).

In a separating equilibrium, the two seller types choose different feasible pairs $x_H$ and $x_L$. Funding customers believe the product is high quality exactly at $x_H$ and low quality at every other pair, including off-path pairs. Neither seller type can gain by deviating under those beliefs. The intuitive criterion then checks whether an off-path pair would be profitable to the high type if believed high while being unattractive to the low type (manuscript, pp. 13, 19).

Formalization targets

Lemma 4 identifies an attained full-information optimum for any choice of true and believed quality in $\{q_L,q_H\}$. Its crowdfunding price is

$$P_1^{ij*}=\max\left\{\frac{4q_j-(1-\alpha)q_i}{8},T\right\},$$

and its retail price follows the three cases of equation (11), depending on whether $T$ lies below $q_j/2$, between that threshold and $q_j/[2(1-\alpha)]$, or above the second threshold (manuscript, p. 23, Lemma 4).

The goal is Proposition 2 in the small-quality-gap regime $q_L<q_H\le(\alpha^2+6\alpha+25)q_L/16$. Define $(\dot P_1,\dot P_2)$ by its equations, requiring $\dot P_2>q_H/2$:

$$4\dot P_1+(1-\alpha)\dot P_2=2q_H,\qquad W^{LH}(\dot P_1,\dot P_2)=\Pi^{L*}.$$

When $T\le\dot P_1$, the goal states that the unique separating equilibrium surviving the intuitive criterion has $x_H=(\dot P_1,\dot P_2)$ and the low type at his full-information optimum. Relative to every full-information optimum $(P^H_{1f},P^H_{2f})$ of the high type, it also states

$$\dot P_1<P^H_{1f},\qquad \dot P_2>P^H_{2f}.$$

The mission separately targets uniqueness of the dotted pair, the first claim of Lemma 6 concerning profitable imitation of the high type's full-information pair, and the constrained optimum in equations (A.13)–(A.14) (manuscript, pp. 26–27, 41).

Significance

The result identifies how a commitment to the later price changes the signal available during crowdfunding. The high type's retail price is raised while his crowdfunding price is lowered, so the signal is encoded in the pair, rather than in a single crowdfunding price. The theorem also determines which separating outcome survives a refinement intended to remove equilibria supported only by arbitrary off-path beliefs (manuscript, pp. 26–27).

The mathematical result is already proved in the manuscript. The remaining formalization work is to give the economic model an exact Lean meaning, prove the optimization and equilibrium assertions, and make the boundary conventions explicit. The five open Lean theorems in this proposal are statements to be proved; their sorry bodies are not machine-checked proofs.

Difficulty

The seller's payoff changes expression when the regular price crosses a threshold determined by the funding price and the two qualities. The low type can mimic a pair whose regular price exceeds $q_L$, in which case regular sales vanish but the crowdfunding payoff can still rise. This makes a direct comparison of the printed $W^{LH}$ expression with the actual mimicking payoff invalid outside its demand region. The intuitive criterion adds a second layer: it tests deviations under a different belief from the default off-path belief. These regime changes and belief-dependent deviations are the central obstacles to a concise, faithful Lean statement (manuscript, pp. 23, 26–27, 41–43).

Formalization scope

Lean represents qualities, prices, probabilities and payoffs as real numbers. Its parameter structure contains $q_L,q_H,\alpha,T$, with $0<q_L<q_H$, $0<\alpha<1$ and $T>0$. The prior high-quality belief is omitted because the separating statements use beliefs fixed by the observed pair. Market sizes, zero costs, salvage value and discount rate are incorporated into the payoff. The funding success probability and purchase probabilities are clipped at zero outside their printed domains. The printed $V^{ij}$ and $W^{ij}$ remain available for the page 41 equations; $W^{ij}$ is only used away from its zero denominator. Suprema range over all feasible pairs $P_1\ge T$, $P_2>0$, and “optimal” means the displayed pair attains that supremum.

The manuscript's Proposition 2 needs the additional bound $T\le(3+\alpha)q_L/8$. Without it, the low type's constrained full-information payoff can be too small and he can profitably mimic a dotted pair with $\dot P_2>q_L$; a numerical counterexample and the discrepancy are recorded in the local moderation notes. This proposal states that bound openly rather than treating the printed proposition as valid for all $T\le\dot P_1$. Lemma 4 also records its displayed domain $T\le q_j$. The goal does not define the optimum by a formula, the equilibrium by the paper's necessary conditions (13)–(14), or the dotted pair by an arbitrary choice.

The foundational setting is a reusable two-type, two-price payoff and equilibrium model. A complete development must establish the payoff's agreement with the manuscript's regions, attainment and comparison of the full-information optima, uniqueness of the dotted pair, optimization on the relevant iso-profit curve, and the no-deviation and intuitive-criterion conclusions. Contributions proving these targets or reusable real optimization lemmas are within scope.

Selected references

• E. Bolandifar, Z. Chen, P. Kouvelis and W. Zhou, Quality Signaling through Crowdfunding Pricing, SSRN manuscript 3689946, 2022-05-30, SSRN. Published as Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1177.