All missions

Motivation

Sellers sometimes offer a customer a choice among individual products and a product whose final item is revealed only after purchase. Airlines, for example, can sell a fixed itinerary alongside a discounted option that leaves one feature unspecified. The seller must decide whether this opaque product earns enough to justify limiting how much individual item prices can differ. Elmachtoub and Hamilton study this question for unit-demand customers who know their own values for the possible items. Their 2021 paper identifies two conditions under which the best menu of opaque products earns at least as much as the best separate item prices.

The comparison matters because the opaque menu uses less item-specific pricing information. The seller gives every item one price and gives opaque products of equal size the same price. The theorem says that this constrained format can still match discriminatory pricing when the valuation law is symmetric and either customers assess opaque products pessimistically or valuations have only two levels. The paper also supplies counterexamples outside those conditions; the symmetry and customer-type hypotheses are substantive.

Setting

There are $N\ge2$ items. A customer has a nonnegative valuation vector $v=(v_1,\ldots,v_N)$, sampled from a probability law $F$. A menu option has a price and a valuation. Its utility is valuation minus price. The customer buys one option of greatest utility when that utility is nonnegative. If several options have greatest utility, the customer buys one with the highest price. Remaining ties at the same price do not affect revenue. A customer may also buy nothing, yielding zero revenue.

In discriminatory pricing (DP), the seller assigns a nonnegative price $p_i$ to each item and offers only the individual items. Write $R_{\mathrm{DP}}(p_1,\ldots,p_N)$ for expected revenue and $R_{\mathrm{DP}}$ for its optimum over item-price vectors.

In opaque selling (OPQ), the seller offers the items at a common price $p$ and also offers every set $S$ of at least two items. A set of size $k$ costs $p^k$, independent of which items it contains. A pessimistic customer values $S$ at $\min_{i\in S}v_i$; a risk-neutral customer values it at $|S|^{-1}\sum_{i\in S}v_i$. Both value a singleton at its item value. A customer is pessimistic with probability $\alpha$ and risk-neutral with probability $1-\alpha$, independently of the valuation vector. The expected revenue of a price menu is $R_{\mathrm{OPQ}}^\alpha(p,p^2,\ldots,p^N)$; its optimum is $R_{\mathrm{OPQ}}^\alpha$.

A law $F$ is exchangeable if permuting the coordinates of $v$ leaves its joint distribution unchanged. Coordinates may be correlated, and they need not be independent. A law is two-valued when there are real numbers $a<b$ such that almost every valuation vector has every coordinate in $\{a,b\}$. This says the same pair applies to the entire vector, rather than allowing a different pair at each coordinate.

Formalization targets

Theorem 1: revenue dominance

For exchangeable $F$, nonnegative valuations, and $0\le\alpha\le1$, the target is

$$\bigl(\alpha=1\ \text{or}\ F\text{ is two-valued}\bigr) \quad\Longrightarrow\quad R_{\mathrm{OPQ}}^\alpha\ge R_{\mathrm{DP}}.$$

The first case covers any exchangeable law, including discrete laws with ties, when all customers are pessimistic. The second covers every mix of customer types when the valuations take two common values. Neither case requires independent item values. This mission retains both cases in one goal because that is Theorem 1 as stated in the paper.

The milestones trace the two cases. They identify the equal probabilities of valuation-order events, the value of the best opaque subset at a fixed size, the pessimistic dominance case, the three candidate DP price vectors under two values, the conditional revenue identity printed as display (1), the opaque price ladder's revenue for both customer types, and the two-valued dominance case. Each milestone is attached to a passage in the proof of Theorem 1.

Significance

The theorem gives a comparison of optimal revenues, not just a comparison of one chosen menu with one chosen price vector. For a seller with exchangeable valuations, it guarantees that size-based opaque prices can recover at least the revenue available from item-specific prices in either named regime. Outside those regimes, the paper's counterexamples prevent extending that guarantee merely by relaxing the hypotheses.

The result is proved in the cited paper; the goal here is a machine-checked version of its statement and proof. A formal development would establish the choice rule for finite menus, expectations for discrete and continuous valuation laws, permutation symmetry, finite order statistics, and the behavior of size-based menus at utility and price ties. These components are reusable in later formalizations of unit-demand pricing and opaque-product models. The present mission starts with unproved Lean theorem statements; compiling those statements does not certify the paper's argument.

Difficulty

One tempting argument treats the opaque menu as discriminatory pricing with the valuation order known to the seller. That comparison overlooks a restriction: the same price must be attached to each product size, so a price that is useful for the highest-valued item need not be useful for every realized ordering. The paper explicitly notes that the apparent information advantage alone would also suggest dominance in settings where dominance fails.

Ties create another obstacle. The probability formulas displayed for DP and OPQ in the selling-model section use inequalities that can count a tied purchase more than once. The paper sets aside ties for exposition in that section, yet the two-valued case necessarily has them. A faithful proof has to use the stated customer choice rule and the highest-price tie-break, rather than treating those displayed sums as definitions for discrete laws. The two-valued case also requires tracking how revenue changes with the number of high valuations, without assuming independent coordinates.

Formalization scope

Items are represented by Fin N and valuation profiles by functions Fin N → ℝ; the paper's item indices start at one, while Lean's start at zero. The probability law is a measure on profiles with a probability-measure instance and almost-sure nonnegative coordinates. Exchangeability means invariance of this law under every coordinate permutation. Two-valued support is an almost-sure condition on the whole profile. No independence or density assumption is included.

The menu contains every nonempty item set. Singletons stand for the ordinary items at their common price; sets of equal larger size share an opaque price. All seller prices are nonnegative. Revenue is the highest price among options with maximal nonnegative utility, with zero when no option qualifies. This directly represents the rule on page 8, including discrete laws. The pessimistic valuation is a finite minimum and the risk-neutral valuation a finite average. Customer type is mixed independently of the valuation law, so the OPQ expectation is the $\alpha$-weighted sum of the two type-specific expectations.

Expected revenues and optimal revenues use extended nonnegative reals $[0,\infty]$. The optima are suprema over nonnegative prices; existence of a maximizing price vector is not assumed. This avoids default values for an unbounded real supremum and records possible infinite revenue. Prices for unused cardinalities are nonnegative but have no effect on the menu. The order statistic sorts the coordinates with multiplicity; it is not defined through the subset identity it is meant to satisfy.

The goal is not implied by a degenerate model: the revenue function charges the highest price among utility maximizers and sells only at nonnegative utility; the optimal revenues range over nonnegative prices; exchangeability is invariance under every coordinate permutation. Contributions toward the finite-menu choice lemmas, permutation-invariant integration, order-statistic identity, two-valued DP structure, and the two cases are within scope.

Selected references

• A. N. Elmachtoub and M. L. Hamilton, The Power of Opaque Products in Pricing, Management Science, 2021, doi:10.1287/mnsc.2020.3750. This mission uses the author's 54-page manuscript, pinned locally by SHA-256 ccd5b53ae01d607eca3b7df8549f418f52245b99bb2dfa050b6f5c4878a3cffe; its printed and PDF page numbers agree.

Motivation

Rewards-based crowdfunding platforms such as Kickstarter and Indiegogo let a creator pre-sell a product before it exists. Most backers cannot judge the product's quality from a campaign page, while some (experts, early adopters, people who have seen a prototype) can. A creator who knows her product is good therefore faces a classical signaling problem: how to convince the uninformed crowd without simply copying what a creator of a worse product could also do. Chakraborty and Swinney (SSRN 2885457, forthcoming in Manufacturing & Service Operations Management, doi:10.1287/msom.2019.0833) show that crowdfunding offers a signaling device absent from ordinary retail: the funding target of an all-or-nothing campaign. The paper sits in the signaling literature that starts with Spence (1973) and Milgrom and Roberts (1986), and uses the equilibrium refinement of Cho and Kreps (1987).

Setting

A creator of private type $i\in\{H,L\}$ runs an all-or-nothing campaign whose reward is one unit of her product. Backers value the products at $v_H>v_L$; producing requires a fixed startup cost $S_i$, with $S_H\ge S_L$. The number of interested backers is $N\sim U[0,\bar N]$, and $S_i<\bar N v_i$, so success is uncertain for both types.

The creator chooses a design $(C,p)$: a funding target $C\ge S_i$ (the funding constraint) and a reward price $p>0$. A fraction $1-\alpha$ of the backers is informed and pledges iff $p\le v_i$. The remaining fraction $\alpha\in[0,1]$ is uninformed: it sees only $(C,p)$, forms a belief about the type and pledges iff $p$ does not exceed the believed valuation. If a share $k$ of the $N$ backers pledges, the campaign succeeds iff $kpN\ge C$; then the creator collects $kpN$ and pays $S_i$, otherwise all pledges are refunded. The expected profit is (1):

$$\Pi=\int_{\{N\in[0,\bar N]:\,C\le kpN\}}\frac{kpN-S_i}{\bar N}\,dN.$$

A separating equilibrium is a pair of distinct designs $d_L,d_H$ such that, with the uninformed backers believing $H$ exactly at $d_H$ and $L$ at every other design, neither type gains from any feasible deviation; in particular the L-type does not gain by mimicking $d_H$. It survives the intuitive criterion if no off-path design makes one type strictly better off when recognized, while making the other type strictly worse off under any belief. With

$$B=v_L+\frac{S_L^2}{\bar N^2v_L},\qquad \alpha^*=\frac{B+\sqrt{B^2+4\frac{S_H^2-2S_LS_H}{\bar N^2}}}{2v_H},$$

the paper's target is

$$C^*(\alpha)=\begin{cases}S_H,&\alpha\le\alpha^*,\\ S_L+\sqrt{S_L^2+\bar N^2(\alpha^2v_H^2-\alpha v_HB)},&\text{otherwise}.\end{cases}$$

Formalization targets

Goal: Proposition 3 (p. 15)

For every $\alpha\in[0,1]$, the designs $(S_L,v_L)$ and $(C^*(\alpha),v_H)$ form a separating equilibrium that survives the intuitive criterion, and every separating equilibrium that survives the criterion has

$$d_L=(S_L,v_L),\qquad d_H=(C^*(\alpha),v_H)\quad\text{unless }\alpha=1\text{ and }S_L=S_H.$$

Milestones

1. Proposition 1 (p. 12): under complete information $(S_i,v_i)$ is the unique optimal design, and the L-type plays $(S_L,v_L)$ in every separating equilibrium.
2. The closed form of (1) (Online Supplement p. 1): $\Pi=\frac{\bar N}{2}kp+\frac{2SC-C^2}{2\bar Nkp}-S$ when $C<kp\bar N$, and $0$ otherwise.
3. The no-mimic window (Online Supplement (5)–(7)): mimicking $(C,p)$ does not pay iff $p_1(C)\le p\le p_2(C)$, with $p_{1,2}(C)=\bigl(B\mp\sqrt{B^2+4(C^2-2S_LC)/\bar N^2}\bigr)/(2\alpha)$; and (8): $p_1(C)<C/(\alpha\bar N)<p_2(C)$.
4. Case 1: $v_H\le p_2(S_H)$ iff $\alpha\le\alpha^*$, and then $(S_H,v_H)$ separates. Case 2: for $\alpha>\alpha^*$, $C^*(\alpha)>S_H$ is the root of $p_2(C)=v_H$.
5. Along the curve $p=p_2(C)$ the H-type's profit is nondecreasing on $[S_H,C^*]$, strictly unless $\alpha=1$ and $S_L=S_H$. The supplement shows it through the derivative

$$\frac{d\Pi_H(C,p_2(C))}{dC}=\frac{C-S_L}{\alpha\bar Np_2(C)^2\sqrt{B^2+4\frac{C^2-2S_LC}{\bar N^2}}}\Bigl[\Bigl(1-\alpha^2\frac{C-S_H}{C-S_L}\Bigr)p_2(C)^2-\frac{S_H-S_L}{C-S_L}\frac{C^2}{\bar N^2}\Bigr]\ge0.$$

6. The informed-only deviation $(S_H,v_H)$, believed $L$, earns strictly less than $(C^*,v_H)$ when $\alpha>\alpha^*$.

Significance

Proposition 3 says that a high-quality creator signals by raising her funding target, accepting a lower chance of success, and never by lowering her price; signaling is free when the informed fraction is large ($\alpha\le\alpha^*$). In contrast with signaling by price alone (Proposition 2 of the paper), a separating equilibrium always exists. The closed form $C^*(\alpha)$ is what the paper's later results build on, notably the endogenous quality choice of Proposition 5.

The result is proved in the paper's Online Supplement by calculus and case analysis. As far as is known, no part of it has been machine-checked. A formalization verifies the equilibrium characterization, including the boundary cases the printed proof treats in a sentence (uniqueness fails at $\alpha=1$, $S_L=S_H$), and gives a reusable model of all-or-nothing campaigns with a uniform crowd.

Difficulty

The algebra of each step is elementary. The difficulty lies in the equilibrium argument. Showing that the given pair is an equilibrium requires bounding the H-type's profit at every design believed to be low quality, including prices at or below $v_L$, where the informed and uninformed backers both pledge. The paper checks only the deviation to $(S_H,v_H)$. The characterization requires turning the intuitive criterion into a maximization of the H-type's profit over the mimicking-proof designs and showing that $(C^*,v_H)$ is its unique maximizer. A natural first idea, to fix $C=S_H$ and lower the price until mimicking stops (Proposition 2's equilibrium), does not give the maximizer: along $p=p_2(C)$ raising the target pays more than lowering the price.

Formalization scope

• Parameters $(\bar N,v_H,v_L,S_H,S_L)$ are real numbers with $0<\bar N$, $0<v_L<v_H$, $0<S_L\le S_H$, $S_L<\bar Nv_L$, $S_H<\bar Nv_H$. The paper uses the positivity of $\bar N,v_L,S_L$ without stating it. $\alpha$ ranges over $[0,1]$, so both extremes are included.
• Profit is the integral of $(kpN-S)/\bar N$ over the success event $\{N\in[0,\bar N]:C\le kpN\}$ (Lebesgue measure). This gives $0$ when success is impossible, including when no backer pledges. The pledging share is computed from the pledging rules, so a mimicking L-type at a price $p\le v_L$ also receives informed pledges (the supplement's formula (5) assumes $p>v_L$).
• Feasibility is $C\ge S_i$ and $p>0$. The pricing constraint $p\le v_i$ is not imposed in the game, because prices above every threshold simply receive no pledges.
• Beliefs are types: $H$ exactly at the H-type's equilibrium design and $L$ elsewhere (p. 11). The intuitive criterion is tested for both deviating types, and the other type must be strictly worse off under both beliefs.
• The characterization excludes $\alpha=1$, $S_L=S_H$, as the proof does. "Any separating equilibrium" is read as any that survives the intuitive criterion.
• Ruled out: an empty characterization (the goal carries the explicit equilibrium), a one-sided intuitive criterion, $C^*$ defined as an unspecified root, and profit formulas with the bound $C/(kp)$, which Lean evaluates to $0$ when $k=0$.
• Needed: set integrals of affine functions on intervals, Real.sqrt algebra, monotonicity along a curve. All of it is in Mathlib; the model definitions are new. Proofs of any milestone are welcome, and so are alternative proofs of the goal that avoid the derivative.

Selected references

• S. Chakraborty, R. Swinney, Signaling to the Crowd: Private Quality Information and Rewards-Based Crowdfunding, SSRN 2885457 (rev. June 2019); Manufacturing & Service Operations Management, 2021. https://ssrn.com/abstract=2885457, https://doi.org/10.1287/msom.2019.0833
• I.-K. Cho, D. M. Kreps, Signaling Games and Stable Equilibria, Quarterly Journal of Economics 102(2), 1987. https://doi.org/10.2307/1885060
• M. Spence, Job Market Signaling, Quarterly Journal of Economics 87(3), 1973. https://doi.org/10.2307/1882010
• P. Milgrom, J. Roberts, Price and Advertising Signals of Product Quality, Journal of Political Economy 94(4), 1986. https://doi.org/10.1086/261408

Motivation

Firms that moved production offshore for low unit costs pay for it in lead time: a slow global supplier forces large safety stocks, and the cost of those stocks grows with demand variability. A recurring question in operations management is when it pays to re-shore part of production to a fast, local, more expensive plant. Adidas's "SpeedFactories" are the example that gives this paper its name. Boute, Disney, Gijsbrechts and Van Mieghem (accepted manuscript, 2020; Management Science 2022) answer this for a linear dual-sourcing policy. Their analysis yields an explicit break-even price for the off-shore supplier, together with a condition under which a small local plant that absorbs only demand variability beats full off-shoring, even when local production costs more per unit than off-shore purchasing.

The dual-sourcing literature (Whittemore and Saunders 1977; Song and Zipkin 2009; Janakiraman, Seshadri and Sheopuri 2015) shows that optimal dual-sourcing policies have no simple structure for general lead times. Xin and Goldberg (2018) proved that tailored base-surge (TBS) policies are asymptotically optimal as the global lead time grows. The present paper combines TBS with a smoothing local replenishment rule and prices the local capacity explicitly.

Setting

A firm serves demand $d_t$, $t = 1, 2, \dots$, from finished-goods inventory $i_t$; excess demand is backlogged. The demands are independent and identically distributed $N(\mu, \sigma)$, where $\sigma$ is the standard deviation. Holding costs $h$ and backlog costs $b$ per unit and period: $C^i_t = h[i_t]^+ + b[-i_t]^+$.

Two sources replenish the inventory:

• a global supplier with lead time $L \ge 2$ and unit price $p$;
• a local SpeedFactory with lead time one, nominal capacity $k$ paid at $u$ per unit whether used or not, and overtime at $um$ per unit, $m > 1$: $C^q_t = uk + um[q_t - k]^+$.

The TBS-POUT policy with allocation $\gamma \in [0,1]$ and smoothing parameter $\alpha \in (-1, 1)$ orders the constant $\mu(1-\gamma)$ globally and

$$q_t = \mu\gamma + (1-\alpha)(i^\star - i_t)$$

locally, where $i^\star$ is the safety stock. The inventory evolves by $i_t = i_{t-1} - d_t + \mu(1-\gamma) + q_{t-1}$. The long-run average cost is $\liminf_n \frac1n \sum_{t=1}^n \mathbb E[C^i_t + p\mu(1-\gamma) + C^q_t]$. The optimized dual-sourcing cost $C^{\mathrm{TBS\text{-}POUT},k^\star}(\gamma)$ is its infimum over $(i^\star, k) \in \mathbb R^2$.

The benchmark is full off-shoring with the order-up-to policy: order $q^g_t = (i^\star + L\mu) - (i_t + \sum_{j=1}^{L-1} q^g_{t-j})$ with inventory $i_t = i_{t-1} - d_t + q^g_{t-L}$. Its optimized long-run cost over $i^\star$ is $C^s$.

With $\varphi, \Phi$ the standard normal density and distribution function, $z_i = \Phi^{-1}[b/(b+h)]$ and $z_q = \Phi^{-1}[(m-1)/m]$. The paper's standard deviations are

$$\sigma_i = \frac{\sigma}{\sqrt{1-\alpha^2}}, \qquad \sigma_q = \sigma\sqrt{\frac{1-\alpha}{1+\alpha}}, \qquad \sigma_{i,s} = \sigma\sqrt L,$$

and the break-even price (20) is

$$p^-(\gamma) = \frac{h+b}{\mu\gamma}(\sigma_i - \sigma_{i,s})\varphi[z_i] + \frac{um}{\mu\gamma}\sigma_q\varphi[z_q] + u, \qquad \gamma \in (0,1].$$

Formalization targets

Goal: Proposition 4 (pp. 18–19)

If

$$\frac{h+b}{um}\cdot\frac{\sigma_{i,s}-\sigma_i}{\sigma_q}\cdot\frac{\varphi[z_i]}{\varphi[z_q]} > 1, \qquad (21)$$

then $p^-$ is concave on $(0,1]$ and $C^{\mathrm{TBS\text{-}POUT},k^\star}(\gamma) < C^s$ whenever $p^-(\gamma) < p < u$. Otherwise $p^-$ is convex on $(0,1]$, and whenever $p > p^-(\gamma)$ for some $\gamma$, the allocation $\gamma = 1$ is the unique minimizer of $C^{\mathrm{TBS\text{-}POUT},k^\star}$ on $[0,1]$ and beats $C^s$. The smoothing parameter $\alpha$ is fixed and arbitrary in $(-1,1)$.

Milestones

1. Lemma 3 (Tsypkin, p. 32): an iid input of variance $\sigma_x^2$ through a linear filter $g$ has long-run output variance $\sigma_x^2 \sum_t g_t^2$.
2. (14) (p. 9): under TBS-POUT, $i_t$ and $q_t$ are normal, and their variances tend to $\sigma_i^2$ and $\sigma_q^2$.
3. Proposition 1 (p. 9): the safety stock $\sigma_i z_i$ and capacity $\mu\gamma + \sigma_q z_q$ are the unique optima, and

$$C^{\mathrm{TBS\text{-}POUT},k^\star} = \sigma_i(h+b)\varphi[z_i] + \sigma_q um\varphi[z_q] + ((u-p)\gamma + p)\mu.$$

4. (18) (p. 11): $C^s = \sigma_{i,s}(h+b)\varphi[z_i] + p\mu$.
5. Proposition 3 (p. 11): $\gamma^\star = 0$ if $u > p$ and $\gamma^\star = 1$ if $u < p$.
6. (19) (p. 17): the closed form of $C^{\mathrm{TBS\text{-}POUT},k^\star} - C^s$.
7. (20) (p. 18): for $\gamma \in (0,1]$, $C^{\mathrm{TBS\text{-}POUT},k^\star}(\gamma) < C^s \iff p > p^-(\gamma)$.

Significance

Proposition 4 is the paper's strategic prescription. It splits the parameter space by one dimensionless product of a financial factor, a variability factor and a service/flexibility factor. On one side, a small SpeedFactory serving only the demand variability is profitable in a price band $p^- < p < u$ below the local unit cost. On the other side, re-shoring is all-or-nothing. Since $\sigma_{i,s}$ grows like $\sqrt L$ while $\sigma_i, \sigma_q$ do not depend on $L$, long off-shore lead times push towards the first regime (Figure 6 of the paper: concave at $L = 6$, convex at $L = 2$).

The printed proof of Proposition 4 is a single sentence ("readily obtained from the second derivative of $p^-$"). The content is in the chain behind it: the inventory under TBS-POUT is an AR(1) process, two Gaussian newsvendor problems give its optimal cost, and the order-up-to benchmark has inventory variance $L\sigma^2$. Formalizing the mission machine-checks that chain from the dynamics to the strategic conclusion. None of these results is formalized anywhere to our knowledge. Reusable outputs include the variance of a linear filter of iid noise, the Gaussian newsvendor minimization, and the long-run cost of the order-up-to policy under iid normal demand.

Difficulty

Once the closed forms (13) and (18) are known, the goal is algebra: $p^-(\gamma) = u + D/(\mu\gamma)$ with $D = (h+b)(\sigma_i - \sigma_{i,s})\varphi[z_i] + um\sigma_q\varphi[z_q]$, and (21) is equivalent to $D < 0$. The work is in reaching (13) and (18) from the dynamics:

• the long-run average is a $\liminf$ of Cesàro means of expected costs, so one needs the convergence of the laws of $i_t$ and $q_t$ and the continuity of the Gaussian newsvendor cost in its mean and variance;
• the infimum over the safety stock and the capacity has to be identified, with uniqueness, through a strictly convex limit;
• the order-up-to system carries an $L$-period pipeline, and the exact variance $L\sigma^2$ holds only once the initial pipeline has been flushed ($t \ge L$).

Taking (13) and (18) as definitions would skip all of this and is ruled out.

Formalization scope

Lean namespace SpeedFactory.BreakEven, two definition files and eight theorem statements.

• Demand. d : ℕ → Ω → ℝ on a probability space, mutually independent, each with law gaussianReal μ (σ²). Periods start at $t = 1$; d 0 is unused. Independence is assumed, although the printed propositions say "identically, normally distributed": (14), $\sigma_{i,s} = \sigma\sqrt L$ and §5 all need it.
• Parameters. $\mu, \sigma, h, b, u > 0$, $p \ge 0$, $L \ge 2$. The model takes $m > 1$: the paper allows $m \ge 1$, but at $m = 1$, $z_q = -\infty$ and the capacity problem has no minimizer. It also takes $\alpha \in (-1, 1)$: the paper allows $\alpha = 1$, where $\sigma_i = \infty$ and (21) divides by $\sigma_q = 0$.
• Long-run cost. The paper prints (5) as a pathwise $\liminf$ of realized costs. The proof of Proposition 1 computes expected costs under the limiting Gaussian law, so the formalization takes the expected Cesàro form $\liminf_n \frac1n\sum_{t=1}^n \mathbb E[\cdot]$.
• Linearized model. Safety stock and capacity range over $\mathbb R$, and orders may be negative, as the paper's linear analysis does ("allows capacity $k^\star < 0$", p. 9).
• TBS pipeline. The global receipts equal $\mu(1-\gamma)$ from the first period on, so $L$ drops out of the TBS system, as the paper states.
• OUT benchmark. $C^s$ is the optimized cost of the order-up-to policy from arbitrary deterministic initial inventory and pipeline. The paper's claim that this policy is optimal among all single-sourcing policies is not formalized.
• Closed forms. $\Phi^{-1}$ is defined as $\sup\{z : \Phi(z) \le r\}$, since Mathlib has no normal quantile. $p^-$ is used only on $\gamma \in (0,1]$.
• Not trivial by construction. The optimized costs are infima of costs defined from the recursions, never the closed forms (13) or (18). The milestones pin them with attained lower bounds (IsLeast) and unique minimizers, so no junk value of sInf or liminf can make a statement true by accident. The critical fractiles are computed from the quantile, not left free.
• Not formalized. Corollary 1 ($\alpha^\star = \lambda$) and Proposition 2, because the goal holds for every fixed $\alpha$. Also left out: the AR(1)/IMA results of §6 (Lemmas 1, 2, 4, 5), the numerics of §4 and §7, and Table 4. That table's last column is inconsistent with its own cost columns.

Contributions welcome: proofs of the milestones, in particular a general Gaussian newsvendor lemma and the AR(1) variance recursion, which are reusable beyond this mission.

Selected references

• R. N. Boute, S. M. Disney, J. Gijsbrechts, J. A. Van Mieghem, Dual Sourcing and Smoothing under Non-Stationary Demand Time Series: Re-shoring with SpeedFactories, accepted manuscript (revised Nov 28, 2020); published in Management Science 68(2), 2022. https://doi.org/10.1287/mnsc.2020.3951
• L. Xin, D. A. Goldberg, Asymptotic optimality of tailored base-surge policies in dual-sourcing inventory systems, Management Science 64(1), 437–452, 2018. https://doi.org/10.1287/mnsc.2016.2607
• R. N. Boute, J. A. Van Mieghem, Global dual sourcing and order smoothing: The impact of capacity and lead times, Management Science 61(9), 2080–2099, 2015.
• G. Janakiraman, S. Seshadri, A. Sheopuri, Analysis of tailored base-surge policies in dual sourcing inventory systems, Management Science 61(7), 1547–1561, 2015.
• Y. Z. Tsypkin, Sampling Systems Theory and its Application, vol. 2, Pergamon Press, Oxford, 1964.

Motivation

Portfolio selection uses observed asset returns to choose weights that balance expected return against variability. Estimates of both quantities can change sharply when the historical sample changes. A distributionally robust model addresses this uncertainty by allowing the return law to vary around the empirical law, then judging a portfolio by its worst variance and worst expected return. In the model of Blanchet, Chen, and Zhou, the allowed laws form a ball defined by an optimal transportation cost. Theorem 1 asks whether this optimization over probability laws can be expressed using only the sample and a norm of the portfolio weights.

The paper presents this equivalence as its first main contribution. Its later sections use statistical assumptions on a return time series to guide the choice of the ball radius and the return target. This mission concerns the finite-sample equivalence itself; those statistical choices are separate results. The distinction matters because the equivalence holds for a given nonnegative radius and target, without imposing a model for how the observations were generated. Theorem 1 and §3 of the preprint make these two roles explicit.

Setting

There are $d$ assets and $n\ge1$ observed return vectors $R_1,\ldots,R_n\in\mathbb R^d$. A portfolio is a vector $\varphi\in\mathbb R^d$ whose weights sum to one. Its return when the asset return vector is $x$ is $\varphi^Tx$. The empirical law is $P_n=n^{-1}\sum_{i=1}^n\delta_{R_i}$, so empirical expectations and variances use the population normalization $1/n$. No independence assumption is needed for this finite-sample problem.

Fix $1\le q<\infty$ and its Hölder conjugate $p$, so $1/p+1/q=1$. The endpoint $q=1$, $p=\infty$ is included. Moving a return vector $u$ to $w$ costs $c(u,w)=\|w-u\|_q^2$. For two probability laws $P,Q$, the transportation cost $D_c(P,Q)$ is the infimum of expected $c(U,W)$ over joint laws whose first marginal is $P$ and second marginal is $Q$. With radius $\delta\ge0$, the ambiguity set is

$$U_\delta(P_n)=\{P\text{ a probability law}:D_c(P,P_n)\le\delta\}.$$

For target return $\bar\alpha$, the feasible region $F_{\delta,\bar\alpha}(n)$ contains portfolios whose weights sum to one and whose expected return under every $P\in U_\delta(P_n)$ is at least $\bar\alpha$. This is the paper's worst-case mean condition. For any such portfolio, the robust objective is the supremum of $\operatorname{Var}_P(\varphi^TR)$ over the same ambiguity set. These objects are defined in §§1–2.2 of the preprint.

Formalization targets

Robust mean and mean-constrained second moment

Proposition 1 identifies the minimum expected return over the ball:

$$\min_{P\in U_\delta(P_n)}E_P(\varphi^TR) =E_{P_n}(\varphi^TR)-\sqrt\delta\,\|\varphi\|_p.$$

Proposition 3 evaluates the maximum second moment subject to a specified mean $\alpha$. Write $m=E_{P_n}(\varphi^TR)$, $N=\|\varphi\|_p$, and $v=\operatorname{Var}_{P_n}(\varphi^TR)$. When $(\alpha-m)^2\le\delta N^2$, its value is

$$h(\alpha,\varphi)=E_{P_n}[(\varphi^TR)^2]+2(\alpha-m)m+\delta N^2 +2\sqrt{\delta N^2-(\alpha-m)^2}\sqrt v.$$

The two displayed steps in the proof of Theorem 1 connect this constrained value to the unconstrained worst variance: $h(\alpha,\varphi)-\alpha^2=(\sqrt v+\sqrt{\delta N^2-(\alpha-m)^2})^2$, whose maximum over allowed $\alpha\ge\bar\alpha$ is $(\sqrt v+\sqrt\delta N)^2$ and is attained at $\alpha=m$. These milestones retain the paper's constants, feasibility range, and attainment claims. Propositions 1 and 3 and the proof of Theorem 1 give the source statements.

Equivalence of the portfolio problems

Theorem 1 is the goal. It says that the robust problem (2) and the empirical problem (9) have both the same optimal portfolios and the same optimal value:

$$\min_{\varphi\in F_{\delta,\bar\alpha}(n)} \sup_{P\in U_\delta(P_n)}\operatorname{Var}_P(\varphi^TR) =\min_{\varphi\in F_{\delta,\bar\alpha}(n)} \left(\sqrt{\operatorname{Var}_{P_n}(\varphi^TR)} +\sqrt\delta\,\|\varphi\|_p\right)^2.$$

The statement also equates the minimizer sets, rather than equating values alone. The paper calls (9) the dual problem; here that name denotes this regularized empirical optimization problem. Theorem 1, p. 6 is the pinned target.

Significance

The theorem replaces an optimization over probability laws with a finite-dimensional portfolio objective containing a norm penalty. It gives a precise interpretation of that penalty: its size and exponent follow from the Wasserstein radius and transport norm. It also preserves which portfolios are optimal, so the reformulation supports the portfolio decision itself, not only its reported objective value. The target-return constraint still depends on the worst expected return; Proposition 1 gives its explicit empirical form. These consequences are stated in §2.2 of the preprint.

A complete formalization would establish the finite-sample equivalence and the attained extrema that underlie it. It would also supply reusable results about finite empirical measures, transport balls with quadratic norm costs, and portfolio moments under those balls. The pinned results are proved in the paper; the work here is to give their statements and proofs in Lean under a shared, audited model. The current local proposal consists of statements with proof placeholders, not machine-checked proofs of those results.

Difficulty

The adversary changes the whole probability law, while the robust objective subtracts the square of the law's own mean from its second moment. Maximizing the second moment alone does not therefore give the worst variance. The mean constraint in Proposition 3 and the subsequent optimization over $\alpha$ are essential to recovering the centered objective. Attainment also matters: the paper states minima and maxima, whereas a bound on an infimum or supremum would be weaker. At the level of Lean definitions, every law in the quadratic transport ball must have sufficiently integrable portfolio returns for the real moment formulas to express the paper's quantities. These are the central obligations of §2.2 and Appendices A–C.

Formalization scope

Return vectors and weights are functions Fin d → ℝ; the sample is indexed by Fin n with $n\ge1$. Exponents are extended nonnegative reals to include $p=\infty$, while $q$ is finite as in the paper's fixed real exponent. The cost takes values in $[0,\infty]$, and the reused transport definition fixes both coupling marginals. The ambiguity set contains all probability laws within the cost radius, with no added moment restriction. The portfolio moments are real Bochner integrals. Showing that the quadratic-cost ball makes these integrals meaningful is part of proving the results.

The robust variance objective uses an extended-real supremum. This represents an empty or unbounded indexing set without the default value of a real supremum. The feasible mean constraint is written as a universal lower bound over the ball, matching the paper's minimum constraint. The goal compares both minimizer sets and infimum values on that feasible region. It cannot be discharged by defining the robust objective to equal the regularized formula, narrowing the ambiguity set, or assuming the desired moment and value identities. Proposition 1 and Proposition 3 retain attainment through IsLeast and IsGreatest.

This mission covers the finite-sample reformulation in §§1–2.2. The time-series assumptions A1–A3, the data-driven choices of $\delta$ and $\bar\alpha$ in §3, Theorem 2, and Proposition 4 are outside its scope. Contributions on transport-ball integrability, the two attained extrema, the scalar maximization, and the final equivalence would all support the goal. The general-cost dual formula of Proposition 2 is omitted because the printed formulation has a boundary counterexample at $\delta=0$; a faithful version needs a separate audit of its duality hypotheses.

Selected references

• José Blanchet, Lin Chen, and Xun Yu Zhou, Distributionally Robust Mean-Variance Portfolio Selection with Wasserstein Distances, arXiv:1802.04885v1, 2018 preprint; published in Management Science, 2022. Pinned preprint.

Motivation

A seller with one item and several buyers whose values are private but drawn from known, independent distributions can maximize expected revenue with Myerson's optimal auction (Myerson, 1981). That auction depends on every distribution through virtual values, asks buyers to report their values, and allocates through a computation that buyers must trust. A sequential posted-price (SPP) mechanism is far simpler: the seller fixes one take-it-or-leave-it price per buyer and approaches the buyers one at a time. Posted prices are common in practice, and no buyer reports anything. The natural question is how much revenue this simplicity costs, measured as the worst-case ratio between the best SPP revenue and the optimal revenue.

Timeline. Chawla, Hartline, Malec and Sivan (2010) showed that sequential posted prices earn at least $1 - (1 - 1/n)^n \ge 1 - 1/e \approx 0.632$ of the optimal revenue in the single-unit setting with $n$ independent buyers. Azar, Chiplunkar and Kaplan (2018) improved this to $0.6346$ for $n \ge 74$, which gave the best universal bound before the present paper. No SPP mechanism can guarantee more than about $0.745$ even for i.i.d. values (Hill and Kertz, 1982; Correa et al., 2017). Beyhaghi, Golrezaei, Paes Leme, Pál and Sivan (Operations Research, 2021; arXiv:1807.03435) proved the universal bound $0.6543$, valid for every $n$, together with $n$-dependent, multi-unit and matroid results and a bound of $0.6620$ for eager second-price auctions. This mission formalizes their single-unit universal bound.

Setting

There are $n$ buyers $i \in [n]$. Buyer $i$ has a value $v_i$ drawn from a probability distribution $\mu_i$ on $\mathbb R$, independently across buyers; the profile $v = (v_1,\dots,v_n)$ has law $\mu_1 \otimes \cdots \otimes \mu_n$.

SPP$(p)$. Given prices $p = (p_1,\dots,p_n)$, the mechanism approaches buyers in decreasing order of price, offers $p_i$ to buyer $i$ while the item is unsold, and sells to the first buyer with $v_i \ge p_i$ at price $p_i$. Its revenue at the profile $v$ is therefore $\max\{p_i : v_i \ge p_i\}$ (zero if nobody accepts), and $\mathrm{SPP}(p)$ denotes its expectation.

Threshold mechanisms (the benchmark). By the taxation principle (Lemma 1 of the paper, cited from Nisan et al.), a deterministic truthful mechanism is described by thresholds $t_i(v_{-i}) \ge 0$ depending only on the other buyers' values: buyer $i$ wins and pays $t_i$ when $v_i \ge t_i$. In the single-unit setting, almost surely at most one buyer weakly exceeds their threshold. The expected revenue is $\mathrm{Opt} = \mathbb E[\sum_i t_i \mathbf 1\{v_i \ge t_i\}]$. Define

$$s^\star_i(\tau) = \mathbb P[v_i \ge t_i \ge \tau], \qquad s^\star(\tau) = \sum_i s^\star_i(\tau),$$

so that $\mathrm{Opt} = \int_0^\infty s^\star(\tau)\,d\tau$ (Equation (1)).

Two pricing rules. Myersonian prices post to buyer $i$ the threshold $t'_i = t_i(v'_{-i})$ computed on an independent re-sample of the other buyers' values, freshly for each $i$; MP is the resulting expected revenue and $m(\tau)$ the probability that some buyer has $v_i \ge t'_i \ge \tau$. The uniform price rule posts the same price $\tau$ to everyone; $\mathrm{UP} = \sup_{\tau \ge 0}\mathrm{SPP}(\tau,\dots,\tau)$.

The factor-revealing program (FR). With $f(x) = 1 - e^{-x}$,

$$\mathrm{FR} = \max_{s}\ \int_0^\infty s(\tau)\,d\tau \quad\text{s.t.}\quad 0 \le s(\tau) \le \min(1, 1/\tau)\ \ \forall \tau \ge 0,\quad \int_0^\infty f(s(\tau))\,d\tau \le 1,\quad s \text{ weakly decreasing}.$$

Formalization targets

Goal: Theorem 1 (p. 13)

For every $n$, every independent value distributions and every single-unit threshold mechanism with finite expected revenue $\mathrm{Opt}$, there is a vector of nonnegative prices $p$ with

$$\mathrm{SPP}(p) \ \ge\ 0.6543 \cdot \mathrm{Opt}.$$

The prices depend on the instance; the constant does not.

Milestones, in the order the proof uses them

1. Equation (1), p. 12: $\mathrm{Opt} = \int_0^\infty s^\star(\tau)\,d\tau$ and $s^\star$ is weakly decreasing.
2. Inequality (2), p. 14: $\tau\, s^\star(\tau) \le \mathrm{SPP}(\tau,\dots,\tau)$ for $\tau \ge 0$, hence $\sup_{\tau \ge 0}\tau s^\star(\tau) \le \mathrm{UP}$; and $s^\star \le 1$.
3. Lemma 2, Inequality (5), p. 15: $\mathbb P[Z_\tau = 0] \le (1 - s^\star(\tau)/n)^n \le e^{-s^\star(\tau)}$, where $Z_\tau$ counts buyers with $v_i \ge t'_i \ge \tau$.
4. Inequalities (3)–(4), p. 14: $\mathrm{MP} = \int_0^\infty m(\tau)\,d\tau$ and $m(\tau) \ge 1 - e^{-s^\star(\tau)}$.
5. Solving Problem (FR), p. 15: the root $\tau^\star > 1$ of $(1 - e^{-1}) + \int_1^{\tau^\star}(1 - e^{-1/\tau})\,d\tau = 1$ is unique and lies in $[1.6955, 1.6965]$.
6. Solving Problem (FR), p. 15: the optimal value of (FR) is attained and equals $1 + \ln\tau^\star$, which is at most $1.5283$.

The intermediate statement $\max(\mathrm{MP}, \mathrm{UP}) \ge 0.6543 \cdot \mathrm{Opt}$, the "best of Myersonian and uniform" form shown first in the proof, is context only: Theorem 1 asserts one deterministic price vector, and that is the goal.

Significance

The result. Theorem 1 was the first improvement over $1 - 1/e$ for single-unit posted pricing that holds for every number of buyers and for arbitrary (regular or irregular) independent distributions. It quantifies the price of simplicity of posted pricing against the optimal auction, and its method (two pricing rules, each giving one constraint on the revenue curve $s^\star$, and a factor-revealing program over all curves meeting both) is reused in the paper for $n$-dependent, multi-unit, position-auction and eager second-price bounds.

Formalizing it. The result is proved on paper; no machine-checked version exists. A formalization checks the probabilistic core, the solution of an infinite-dimensional program, and the numerical constants. The printed constants carry rounding slips ($\tau^\star = 1.696$ is a rounding of $1.69572\ldots$; $1 + \ln\tau^\star = 1.52810\ldots$, printed as $1.5283$), which the milestones state precisely. The paper's normalization $\max(\mathrm{MP}, \mathrm{UP}) = 1$ silently assumes that Opt is finite; the formal statement makes that hypothesis explicit.

Difficulty

The Myersonian rule alone gives only $1 - 1/e$, and the paper's example (values uniform on $[1, 1+\epsilon]$) shows this is tight for it; the uniform rule alone is also bounded away from 1. The improvement comes only from combining them, and the combination is expressed as an optimization over all decreasing curves $s$: the step that the obvious argument misses is the exact solution of (FR), whose optimum must be guessed and certified for an infinite-dimensional program with a nonlinear constraint. The probabilistic step is subtle as well: the true thresholds $t_i$ are correlated across buyers, and Lemma 2 holds only for the independently re-sampled $t'_i$. Finally, the theorem claims a single deterministic price vector, so the random Myersonian prices and a possibly unattained best uniform price must both be converted into one concrete $p$, with the slack between $0.6543$ and $1/\mathrm{FR} = 0.65440\ldots$ absorbing the approximation.

Formalization scope

Buyers are Fin n; values have law Measure.pi μ with each μ i a probability measure on ℝ; values need not be nonnegative. Revenues and probabilities are in ℝ≥0∞ (lower Lebesgue integrals and measures), never Bochner integrals, so that a non-integrable revenue cannot become a junk zero. The SPP revenue at a profile is the closed form $\max\{p_i : v_i \ge p_i\}$ of the price-ordered sale. A threshold mechanism is a family t i v with t i measurable, nonnegative, independent of coordinate i, and almost surely at most one buyer with t i v ≤ v i. Myersonian prices are read from a fresh copy of the whole profile per buyer, independent of everything else. In (FR) the constraint $s(\tau) \le \min(1, 1/\tau)$ is encoded as $s(\tau) \le 1$ and $\tau s(\tau) \le 1$.

Benchmark. The goal is stated for every single-unit threshold mechanism, which is the taxation-principle form of Lemma 1; for the optimal mechanism's thresholds it is the printed theorem, and the paper's proof never uses optimality. Lemma 1 and Myerson's theorem are cited by the paper and are not part of the mission. The one added hypothesis on the goal, finiteness of Opt, is necessary: without it some single-unit threshold mechanisms have infinite revenue while every posted-price revenue is finite.

Ruled out. The SPP revenue is the revenue of the actual sequential sale, not a free function; thresholds may not depend on the buyer's own value (that would allow full surplus extraction) and must be single-unit feasible (otherwise Opt could be $n$ times any posted-price revenue); the constant is the explicit $0.6543$, not an existential one.

Out of scope. Theorem 2 ($n$-dependent bounds), Theorem 3 and Lemmas 3–4 (multi-unit), Lemmas 5–7 and Theorem 4 (position auctions), the partition-matroid claim and Proposition 1 (matroids), Lemma 8 and Theorems 5–6 (eager second-price auctions), Inequality (6) of Lemma 2, the $(1-1/e)$ illustration of §4.1, and the numerical tables.

Infrastructure. The development needs the layer-cake formula for lower integrals, independence under product measures, the AM–GM inequality and $(1 - y/n)^n \le e^{-y}$, all in Mathlib, plus a numerical certificate for the root of a transcendental equation. The threshold-mechanism and SPP definitions are reusable for the multi-unit and matroid results of the same paper. Proofs of any milestone, alternative arguments, and sharper constants are welcome.

Selected references

• H. Beyhaghi, N. Golrezaei, R. Paes Leme, M. Pál, B. Sivan, Improved Revenue Bounds for Posted-Price and Second-Price Mechanisms, Operations Research 69(6), 2021. arXiv:1807.03435v4. https://arxiv.org/abs/1807.03435
• R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 1981. https://doi.org/10.1287/moor.6.1.58
• S. Chawla, J. D. Hartline, D. L. Malec, B. Sivan, Multi-parameter Mechanism Design and Sequential Posted Pricing, STOC 2010. https://doi.org/10.1145/1806689.1806733
• Y. Azar, A. Chiplunkar, H. Kaplan, Prophet Secretary: Surpassing the 1 − 1/e Barrier, ACM EC 2018, 303–318. https://doi.org/10.1145/3219166.3219182
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted Price Mechanisms for a Random Stream of Customers, ACM EC 2017, 169–186. https://doi.org/10.1145/3033274.3085137
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Theorem 9.36.

Why congestion in matching markets matters

Online matching platforms (labor platforms such as Upwork or TaskRabbit, dating sites, short-term rental platforms) make it cheap to contact potential partners, but not cheap to find one who is still available. A worker who has already accepted a job, or a listing that is already booked, keeps receiving applications and keeps being screened. Arnosti, Johari and Kanoria, Managing Congestion in Matching Markets (M&SOM 23(3):620–636, 2021), build a stochastic game-theoretic model of this effect, in which applicants pay to apply and employers pay to screen, and employers cannot see which applicants have already matched. They prove that the model has a unique equilibrium, compute both sides' welfare in it in closed form, and use the formulas to evaluate platform interventions (application limits, application fees, a market-wide wage).

This mission formalizes the equilibrium characterization: the closed-form equilibrium welfare of Theorem 2, together with the existence and uniqueness results (Proposition 2, Theorem 1) and the identities from the paper's endnotes that connect them.

The stationary mean-field model

A market has four parameters: $r>0$, the number of applicants per employer; $\beta\in(0,1]$, the probability that an applicant is qualified for a given employer; $c_a$, the cost of one application; and $c_s$, the cost of screening one applicant. Throughout, Assumption 1 holds: $\max(c_a,c_s)<\beta$. Write $c'_s = c_s/\beta$.

Applicants choose an application intensity $m\ge0$: an applicant sends a Poisson($m$) number of applications, each of which becomes an offer independently with probability $p$, the acceptance probability. The applicant takes the first offer, so the expected payoff is

$$W_a(m,p) = 1-e^{-mp}-c_a m, \tag{2}$$

maximized by the applicant best response

$$\mathcal M(p) = 0 \ \text{ if } p\le c_a, \qquad \mathcal M(p)=\tfrac1p\log\bigl(\tfrac p{c_a}\bigr)\ \text{ if } p>c_a. \tag{3}$$

Employers receive a Poisson($rm$) number of applications. Each applicant is qualified with probability $\beta$ and still available with probability $q$. An employer either screens sequentially until it hires (screening probability $\alpha$) or exits. The employer best-response correspondence is

$$\mathcal A(q) = \{0\}\ \text{if } q<c'_s,\qquad [0,1]\ \text{if } q=c'_s,\qquad \{1\}\ \text{if } q>c'_s, \tag{4}$$

and the employer payoff is $W_e(\alpha,m,q) = \alpha(1-e^{-rm\beta q})(1-c'_s/q)$ (5).

With $E(x) = (1-e^{-x})/x$ ($E(0)=1$), the consistency conditions are

$$q = E(mp), \qquad p = \alpha\beta\,E(rm\beta q). \tag{6–7}$$

A solution $(p,q)$ is a mean-field steady state of the strategies $(m,\alpha)$. A mean-field equilibrium (MFE) is a pair $(m^*,\alpha^*)$ with a steady state $(p^*,q^*)$ such that $m^* = \mathcal M(p^*)$ and $\alpha^*\in\mathcal A(q^*)$ (Definition 1). Equilibrium welfare is $\Pi^*_a = W_a(m^*,p^*)$ and $\Pi^*_e = W_e(\alpha^*,m^*,q^*)$.

Formalization targets

Goal: Theorem 2 (p. 628)

There are unique $\hat p,\bar p>c_a$ with

$$r\Bigl(1-\frac{c_a}{\hat p}\Bigr) = 1-e^{-\frac{r\beta}{\hat p}\left(1-\frac{c_a}{\hat p}\right)}, \qquad 1-\frac{c_a}{\bar p}+\frac{c_s}{\beta}\log\Bigl(\frac{c_a}{\bar p}\Bigr)=0, \tag{13–14}$$

the MFE is unique, and in it

$$p^*=\min(\hat p,\bar p),\qquad \Pi^*_a = 1-\frac{c_a}{p^*}+\frac{c_a}{p^*}\log\frac{c_a}{p^*},\qquad \Pi^*_e = r\Bigl(1-\frac{c_a}{p^*}+\frac{c_s}{\beta}\log\frac{c_a}{p^*}\Bigr). \tag{15–16}$$

The theorem is exact; it has no constants to improve.

Milestones

1. Proposition 2 (p. 626): for fixed $m\ge0$, $\alpha\in[0,1]$, $r$, $\beta$, the system (6)–(7) has a unique solution.
2. Theorem 2, (13) and Theorem 2, (14) (p. 628): the two root equations each have a unique root above $c_a$.
3. Endnote 13 (p. 635): at the applicant best response, consistency (7) with every employer screening ($\alpha=1$) is equation (13).
4. §5.1 (p. 628): at the applicant best response, employers are exactly indifferent ($q=c'_s$) iff (14) holds.
5. Theorem 1 (p. 627): the MFE exists and is unique.
6. Endnote 12 (p. 635): the welfare identities (15) and (16) at the best response and a steady state.

Significance

Theorem 2 reduces equilibrium welfare on both sides to one scalar, $p^*=\min(\hat p,\bar p)$, and splits markets into two regimes (Definition 2): application-limited ($\bar p>\hat p$; all employers screen; applicants compete in a "tragedy of the commons") and screening-limited ($\bar p<\hat p$; employers are indifferent and their welfare is zero, by (14) and (16)). All of the paper's later results, including the welfare bounds of Theorem 3, the effect of application limits (Theorems 4–5), application costs (Theorem 6) and wages (Theorem 7), are computed from these formulas.

Proposition 2, Theorem 1 and Theorem 2 are stated in the article but their proofs are in a technical report (Arnosti, Johari, Kanoria 2019, SSRN), not reproduced in the article and not used here. To our knowledge none of these results has a machine-checked proof. A formal development would give a self-contained, checked proof of the equilibrium characterization from the article's definitions alone.

Where the difficulty lies

The welfare identities (15)–(16) are algebra once $m^*=\mathcal M(p^*)$ and $p^*>c_a$ are known. The root statements are one-variable analysis. The hard part is the equilibrium itself. Proposition 2 is a fixed-point problem: substituting (7) into (6) gives an increasing map $q\mapsto E(m\alpha\beta E(rm\beta q))$, and an increasing map can have several fixed points, so a monotonicity argument alone does not give uniqueness. Theorem 1 then has to handle the correspondence $\mathcal A$: an equilibrium may sit at the kink $q^*=c'_s$ with an interior $\alpha^*$, and the case analysis has to show that exactly one of the regimes $\alpha^*=1$, $\alpha^*<1$ applies and that it pins down $(m^*,\alpha^*)$.

Formalization scope

All objects live in the namespace MatchCongestion.Welfare, over ℝ. The conventions are:

• Positivity. Params.Standing is Assumption 1 together with $0<r$, $0<\beta\le1$, $0<c_a$, $0<c_s$, which the paper uses without listing them ("costs", $\beta$ a probability). Without $c_s>0$, (14) has no root above $c_a$.
• The ratio at zero. The page leaves (6)–(7) undefined at $mp=0$ and $rm\beta q=0$. They are written through $E$ with $E(0)=1$, the continuous extension.
• Definition 1. It composes $\mathcal M$ and $\mathcal A$ with the steady-state maps $\mathcal P,\mathcal Q$. IsMFE instead asks for some steady state $(p,q)$; by Proposition 2 the two readings agree.
• The correspondence. $\mathcal A(q)$ is a Set ℝ.
• Roots and welfare. $\hat p,\bar p$ are quantified (any roots above $c_a$), not chosen. $\Pi^*_a,\Pi^*_e$ are $W_a,W_e$ at the MFE's own steady state. $\log$ is Real.log.

Several formalizations would make the goal trivial or false, and none is used:

• a raw division (1 - exp (-x)) / x in (6)–(7) would make $(m,\alpha,p,q)=(0,0,0,0)$ a spurious second equilibrium;
• an "every MFE satisfies …" goal without the existence-and-uniqueness conjunct would be vacuous;
• choosing $\hat p,\bar p$ by Classical.choose, or $\mathcal P,\mathcal Q$ in Definition 1, would leave junk values unconstrained;
• $\mathcal A$ as a function would erase the screening-limited equilibrium, which has an interior $\alpha^*$;
• $\mathcal M$ without the case split $p\le c_a$ would make the best response negative.

Proposition 1 (the employer's sequential screening problem, specified only in an online appendix), the application-limit model (8)–(9) with Proposition 3, Theorems 3–7 and the finite-system limit theorems 8–10 are out of scope. Contributions of independent interest are a general lemma on unique roots of strictly convex or concave one-variable functions on an interval, and analytic facts about $E$ (positivity, strict monotonicity, $E\le1$ on $[0,\infty)$).

Selected references

• N. Arnosti, R. Johari, Y. Kanoria, Managing Congestion in Matching Markets, Manufacturing & Service Operations Management 23(3):620–636, 2021. https://doi.org/10.1287/msom.2020.0927
• N. Arnosti, R. Johari, Y. Kanoria, Managing Congestion in Matching Markets (full technical report), preprint, 2019. http://dx.doi.org/10.2139/ssrn.2427960