Operations Research

Motivation

Online marketplaces rely on consumer reviews, and a negative review lowers what future buyers believe about a product. Review blackmail exploits this: a consumer buys, posts a negative review, and offers to remove it for a ransom. Platforms counter with dispute-resolution mechanisms. Papanastasiou, Yang and Zhang (Management Science 69(10), 2023) compare two of them in a Bayesian game between a seller, one consumer and the market. Under the centralized mechanism the seller reports the review and the platform decides whether to remove it. Under the semi-decentralized mechanism the seller removes the review himself, and the platform checks afterwards. If it judges the removal wrongful, it reinstates the review and fines the seller a penalty $b$.

This mission covers the semi-decentralized mechanism. Its main result, Proposition 5, gives the ransom a blackmailer can extract in equilibrium in closed form and says when blackmail pays at all. A platform needs that answer when it chooses the penalty. Mission I of this series treats the centralized mechanism.

Setting

A product has quality $q\in\{l,h\}$. The prior that $q=h$ is $a\in(0,1)$. A buyer of a high-quality product gets a positive experience with probability $\theta\in(0,1)$; a low-quality product never gives one. With probability $\beta\in(0,1)$ the consumer is malicious. A malicious consumer buys at price $p$, posts a negative review $N$ and demands a ransom $r$. Otherwise the consumer is regular. A regular consumer buys with probability $\rho=1-p/(a\theta)$ (valuation $v_j$ uniform on $[0,1]$) and reviews truthfully: positive ($P$) or negative ($N$). No purchase means no review, written $R=0$; a removed review is also seen as $R=0$.

The market observes $R\in\{N,0,P\}$ and forms the posterior $a'$ by Bayes' rule. The seller then earns $\pi(a')$, where $\pi$ is nonnegative, convex and strictly increasing on $[0,1]$.

Facing a ransom demand, the seller can settle ($s$: pay $r$, review removed), do nothing ($n$), or use the mechanism ($d$). Under $d$ the platform judges immediately with probability $\gamma\in[0,1]$ (timeliness). It recognises a malicious review with probability $\delta\in[0,1]$ (accuracy). The review is therefore reinstated with probability $\gamma(1-\delta)$, and the penalty $b\ge0$ is paid with probability $1-\delta$. Write $a^i_R$ for the posterior after review $R$ when the market believes the seller's response is $i$. The payoffs of the three responses are then

$$\pi(a^i_0)-r,\qquad \pi(a^i_N),\qquad (1-\gamma(1-\delta))\pi(a^i_0)+\gamma(1-\delta)\pi(a^i_N)-(1-\delta)b.$$

The market cannot see the interaction, so $i$ is an equilibrium at $r$ if no response pays more given the belief $i$. The equilibrium ransom $r^*$ is the largest $r$ at which settling is an equilibrium and no equilibrium pays the seller more. The malicious consumer buys iff $p<r^*$.

A seller could also use the mechanism against genuine negative reviews. Proposition 4 shows that this is deterred exactly when $b\ge\underline b:=(1-\gamma)[\pi(a)-\pi(a^s_N)]$.

Formalization targets

Goal: Proposition 5 (p. 21)

Let $\delta<1$ and $T=\frac{1-\gamma(1-\delta)}{1-\delta}\big(\pi(a)-\pi(a^n_N)\big)$.

1. If $b\ge T>\underline b$:

$$r^*=\pi(a)-\pi(a^n_N),\qquad\text{and the malicious consumer buys iff } p<r^*.$$

2. If $\underline b\le b<T$:

$$r^*=(1-\delta)\big(\gamma(\pi(a)-\pi(a^d_N))+b\big),\qquad\text{and the malicious consumer buys iff } p<r^*.$$

Milestones

• (5), p. 21: the closed form of $a^d_N$, together with $a^i_0=a$.
• §5.1, p. 21: the ordering $a^s_N<a^d_N<a^n_N$.
• Proposition 4, p. 20: genuine negative reviews are kept iff $b\ge\underline b$.
• Proof of Proposition 5, Step 1, pp. 41–42: the conditions under which $s$, $n$ and $d$ are equilibria, one milestone each.

Significance

Proposition 5 has two regimes. If the penalty is high, the mechanism plays no part in blackmail: the seller would never use it, and the ransom equals the one with no mechanism at all. Below the threshold, the ransom is the seller's expected loss from using the mechanism. A lower ransom then means less blackmail, and it pushes the price at which blackmail stops paying downward. The threshold $T$ rises with the accuracy $\delta$ and falls with the timeliness $\gamma$. The paper's later results on pricing and on the platform's penalty build on this characterization.

The result is proved in the paper (Appendix C, pp. 41–43). It has no machine-checked proof. Formalizing it pins down the equilibrium concept, including the selection among multiple equilibria. It also corrects a printed slip in the proof: the simplified condition for the mechanism to be an equilibrium drops a factor $1-\delta$.

Difficulty

Each individual equilibrium condition is a rearrangement of payoff inequalities. The difficulty lies in selecting among equilibria. Several responses can be equilibria at the same ransom. Settling prevails only if no other equilibrium pays more, and the equilibria themselves depend on $r$. So the set of ransoms at which settling prevails is not given by one inequality. Its greatest element must be found across three scenarios, comparing three thresholds that involve three different posteriors. Those comparisons require the posterior ordering $a^s_N<a^d_N<a^n_N$, which comes from Bayes' rule and not from the payoff algebra. Reading the equilibrium condition for $s$ alone as the answer gives the wrong ransom in case 1.

Formalization scope

Everything lives in the namespace ReviewBlackmail.SemiDec, with one structure Model holding $a,\theta,\beta,p,\gamma,\delta,b$ and the payoff fut (the paper's $\pi$; Real.pi is never used). The predicate Standing collects the standing assumptions: $a,\theta,\beta\in(0,1)$; $\pi$ nonnegative, convex and strictly increasing on $[0,1]$; $\gamma,\delta\in[0,1]$; $b\ge0$; and the disclosed addition $0<p<a\theta$, which makes the purchase probability $\rho$ lie in $(0,1)$. Per-statement additions, each disclosed in the item:

• $\delta<1$ on the goal and on Step 1 for $n$ and $d$, which divide by $1-\delta$;
• $0<\gamma(1-\delta)<1$ on the strict ordering;
• $0<\gamma<1$ on the second half of Proposition 4.

Posteriors are defined by Bayes' rule over an explicit likelihood table with two visibility probabilities: $m$ for malicious and $g$ for genuine negative reviews. Proposition 4 needs beliefs in which genuine reviews are removed. The payoffs of Proposition 5 keep genuine reviews ($g=1$), the case the paper reduces to via Proposition 4. Ties in the selection rule go to settling.

The posteriors $a^i_R$ are never defined by their closed forms, and $r^*$ is never defined by (6) or (7). The goal is stated with IsGreatest on the set of ransoms at which settling prevails, not with sSup, so neither the closed forms nor junk values of a supremum can make the goal trivial.

A complete development needs only Mathlib's ConvexOn, StrictMonoOn and IsGreatest and real-field algebra. The algebra of Bayes posteriors with two-point priors may be reusable. Proofs of the milestones and the goal are welcome, in any order.

Selected references

• Y. Papanastasiou, S. A. Yang, A. H. Zhang, Improving Dispute Resolution in Two-Sided Platforms: The Case of Review Blackmail, Management Science 69(10):6021–6037, 2023. https://doi.org/10.1287/mnsc.2022.4655 (cited from the accepted manuscript, LBS Research Online eprint 1988, https://lbsresearch.london.edu/id/eprint/1988/).

Motivation

Young innovative firms often fund research out of internal cash flow rather than external capital. Whether such financial constraints make firms invest less in research and development (R&D) is a long-standing question in corporate finance and the economics of innovation. Myers (1977) showed that the possibility of default leads to under-investment in growth options. Danmo Lin (Management Science, 2022) separates two ways in which spending more on a project can pay off: it can make the payoff larger (scalability) or make the discovery arrive sooner (accelerability). The paper's Corollary 1 says that the classical under-investment result holds exactly when the project is scalable but not accelerable, while acceleration can reverse it. This mission formalizes the under-investment half of that corollary.

Setting

A firm faces a one-time R&D opportunity. It chooses an investment intensity $R$, a spending rate per unit of time, and pays it until discovery. Discovery is the first arrival of a Poisson process of rate $\lambda(R)$, and on discovery the firm receives a payoff with mean $u(R)$. As in the paper's equation (2),

$$u(R)=A\,R^{\beta},\qquad \lambda(R)=\eta\,R^{\gamma},\qquad A>0,\ \eta>0,\ \beta,\gamma\in[0,1),\ \beta+\gamma<1,$$

and intensities are at least $\underline R=1$. The project is scalable if $u'>0$ (here $\beta>0$) and accelerable if $\lambda'>0$ (here $\gamma>0$). Future cash is discounted at rate $r>0$.

An unconstrained (UC) firm can always pay $R$. By the paper's Lemma 1, equation (5), its project value at intensity $R$ is the perpetuity

$$V_{uc}(R)=\frac{u(R)\lambda(R)-R}{\lambda(R)+r}.$$

A financially constrained (FC) firm pays $R$ out of an asset-in-place (AIP) cash flow $X_t$, a geometric Brownian motion with drift $\mu$ and volatility $\sigma$ that starts at $X$. It must abandon the project once $X_t<R$. Lemma 1, equation (6), gives its project value as

$$V_{fc}(R)=\frac{u(R)\lambda(R)-R}{\lambda(R)+r}\Big(1-\big(\tfrac{X}{R}\big)^{\alpha}\Big),\qquad \alpha=\tfrac12-\tfrac{\mu}{\sigma^2}-\sqrt{\big(\tfrac12-\tfrac{\mu}{\sigma^2}\big)^2+\tfrac{2(\lambda(R)+r)}{\sigma^2}}.$$

The ranges of intensities are those of (7): $[1,\bar R]$ for the UC firm and $[1,\min\{\bar R,X\}]$ for the FC firm, with $\bar R=(A\eta)^{1/(1-(\beta+\gamma))}$. The optimal intensities $R^*_{uc}$ and $R^*_{fc}$ are the sets of maximizers of $V_{uc}$ and $V_{fc}$ over these ranges.

Formalization targets

Goal: Corollary 1, first statement (p. 6)

If $\lambda'=0$ and $u'>0$, then $R^*_{fc}<R^*_{uc}$. Formally: under the standing assumptions, $r>0$, $\sigma>0$, $X\ge1$, $\gamma=0$, $\beta>0$ and $A\beta\eta>1$, both optimal sets are nonempty and

$$x<y\qquad\text{for every } x\in R^*_{fc}\text{ and every } y\in R^*_{uc}.$$

Milestones (Appendix A.4, p. 20)

1. Without accelerability, every interior FC optimum ($1<R<\min\{\bar R,X\}$) satisfies $u'(R)\lambda-1>0$. This is the paper's consequence of the first-order condition (A.25).
2. Without accelerability and with $A\beta\eta>1$, every UC optimum satisfies $u'(R)\lambda-1=0$ (in particular it is interior).

Significance

The statement pins down when the textbook under-investment effect of financing frictions holds: exactly when extra spending scales the prize but cannot speed it up. The paper contrasts it with the possibility of over-investment on accelerable projects (Corollary 1's second statement, supported by numerical exercises). Taken together, the two statements show that the R&D technology, not only the severity of the constraint, decides the direction of the distortion.

The result is proved in the paper (Appendix A.4); it has no machine-checked proof. A formal proof certifies the comparison for every pair of optima, without the paper's tacit assumption that optima are unique. It also makes explicit the interior-optimum condition $A\beta\eta>1$ under which the inequality is strict. The resulting facts about maximizers of products of a concave power-law profit and a decreasing survival factor are reusable for other real-options models with a survival discount.

Difficulty

The first idea is to compare the two first-order conditions. The UC optimum solves $u'\lambda=1$, and at an interior FC optimum the derivative of the survival factor pushes $u'\lambda-1$ to be positive. Concavity of $f(R)=u(R)\lambda-R$ then orders the two. Turning this into a theorem about sets of maximizers needs more. The FC optimum can sit at a corner, either $R=1$ or the right end $\min\{\bar R,X\}$, where no first-order condition holds, and the corners must be ruled out or handled separately. The survival factor $1-(X/R)^\alpha$ vanishes at $R=X$. The UC value vanishes at $\bar R$. When $X\le R^*_{uc}$, the comparison is settled by the range rather than by the first-order condition. The strict inequality is false without an interior UC optimum: if $A\beta\eta\le1$, both optimal sets equal $\{1\}$.

Formalization scope

All objects are in the namespace AccelScal.FCMonopoly, in one definition file. It holds the parameter structure Tech $(A,\beta,\eta,\gamma)$, the predicate Standing, $u$, $\lambda$, $\bar R$, $\alpha$, $V_{uc}$ (5), $V_{fc}$ (6), and the maximizer sets RstarUC, RstarFC over the ranges (7). Powers are Real.rpow, and $u'$ is Mathlib's deriv.

Committed conventions:

• The reduced problems are the definitions. The FC firm's original problem (3) is an expectation over a geometric Brownian motion and its first-passage time below $R$. That its value is (6) is the paper's Lemma 1 (Appendix A.12), which needs first-passage machinery absent from Mathlib, and it is not posed. The mission takes (6), and for symmetry (5), as the definitions of the two firms' problems, exactly as the paper's proof of Corollary 1 does. $V_{fc}$ is "the value of problem (3)" only through Lemma 1.
• The random payoff is replaced by its mean $u(R)$, and the AIP term of (3)/(4), which does not depend on $R$, is dropped.
• Standing assumptions: (2), plus the added condition $A\eta>1$ (investment takes place, so $V_{uc}(1)>0$). The goal adds $A\beta\eta>1$, which is necessary for the strict inequality (the UC optimum is interior), and $X\ge1$, which keeps the FC range nonempty. "$\lambda'=0$, $u'>0$" is encoded as $\gamma=0$, $\beta>0$, which is equivalent under (2). No sign condition on $\mu$ is imposed, and $\sigma>0$.
• The paper's single-valued $R^*$ is read as a set of maximizers. The inequality is claimed for every pair of optima.

Trivializing formalizations are ruled out. $R^*_{uc}$ is never defined by its closed form, and neither optimum is a selected value. The goal asserts that both optimal sets are nonempty. The FC range depends on $X$ through $\min\{\bar R,X\}$. The conclusion is the strict "$<$", not "$\le$".

The paper's second and third statements of Corollary 1 (over-investment when $\lambda'>0$, and when it is "more likely") are numerical or informal and are not posed. Contributions are welcome on both milestones and on the goal. Also welcome: general lemmas on the maximizers of a positive concave function times a decreasing positive factor, and a future formalization of Lemma 1 (6) from a geometric Brownian first-passage Laplace transform.

Selected references

• D. Lin, Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition, Management Science, Articles in Advance, 2022. https://doi.org/10.1287/mnsc.2022.4503
• S. C. Myers, Determinants of Corporate Borrowing, Journal of Financial Economics 5(2), 147–175, 1977. https://doi.org/10.1016/0304-405X(77)90015-0

Motivation

Firms that serve several customers from shared capacity must decide which demands to fulfil after demand is observed. A customer-level service commitment constrains the allocation policy even when total capacity appears adequate: serving one customer can consume resources that another customer needs. The question in this mission is how to test a fixed capacity vector against all individual service targets without first specifying a particular rationing rule. Jiang, Wang, and Zhang give a characterization for a broad family of pooled-resource models, including inventory pooling, process flexibility, and assemble-to-order systems (SSRN preprint, §§1.1–2).

The authors' model allows service to mean more than the probability of completely filling an order. It can represent the probability of full service, a fulfilled fraction relative to expected demand, or a fulfilled fraction of realized demand. Their Theorem 1 addresses asymptotic feasibility: every target can be met to within any prescribed positive tolerance. It is distinct from exact feasibility, which the paper treats later under stronger conditions (Jiang, Wang, and Zhang, Theorems 1–2).

Setting

There are $n$ customers and $m$ resource types. A nonnegative capacity vector $c$ is fixed before a random, nonnegative demand vector $D$ is observed. The joint law of $D$ is $F$ and has a bounded second moment. After seeing $D$, a decision consists of a vector $s$ of fulfilled customer demands and an allocation array $y$ recording the amount of each resource assigned to each customer. The paper's set $P(c,D)$ specifies all feasible pairs $(s,y)$ for that capacity and demand. It is a model input: the three operational examples use different feasible sets (§1.1, equations (1)–(4)).

For customer $j$, a service measure $R_j(s_j,D_j)$ assigns a nonnegative score to fulfilled demand $s_j$ and demand $D_j$. The customer has a target $\beta_j\in(0,1)$. A deterministic policy chooses a feasible pair in $P(c,D)$ for each $D$. A randomized policy chooses among deterministic policies. Its expected service to customer $j$ is denoted $S_j(\lambda)$. The capacity is asymptotically feasible when, for every $\varepsilon>0$, some randomized policy $\lambda_\varepsilon$ satisfies $S_j(\lambda_\varepsilon)\ge\beta_j-\varepsilon$ for every customer (Definition 1, equation (8)).

For nonnegative customer weights $w=(w_j)_j$, define maximum weighted service at a realized demand by

$$M_w(D)=\max_{(s,y)\in P(c,D)}\sum_j w_jR_j(s_j,D_j).$$

The maximum uses only service, with zero allocation cost. The paper also introduces a linear allocation cost $f(y)$, a deterministic Max-Weighted-Service minimization problem, and its expected dual functional; Lemma 1 concerns those general objects (§2, equations (14), (16)–(17)).

Formalization targets

Theorem 1: capacity characterization

Under Assumption 1, the target is the equivalence

$$c\text{ is asymptotically feasible} \quad\Longleftrightarrow\quad \mathbb E_F[M_w(D)]\ge\sum_jw_j\beta_j \quad\text{for every }w\ge0.$$

The weights range over the whole nonnegative orthant; they are not restricted to a simplex in the theorem. Assumption 1 requires each $R_j$ to be nondecreasing and upper semicontinuous in fulfilled demand at fixed realized demand, and each $P(c,D)$ to be compact (Theorem 1, equation (18)).

Milestones from the paper

Lemma 1 identifies the value of the pointwise Max-Weighted-Service rule: $\inf_\phi F(w,\phi)=F(w,\phi_w)=\mathbb E_F[g(w,c;D)]$ for a fixed $w\ge0$. The proof of Theorem 1 then uses a minimax display over $W=\{w\ge0:\sum_jw_j\le1\}$ to obtain, for every $\varepsilon>0$, a randomized policy whose weighted service shortfall is at most $\varepsilon$ throughout $W$ (equation (21)). Equation (22) gives the corresponding individual service bounds. These three source claims are the mission's milestones (Lemma 1 and proof of Theorem 1, pp. 12–14).

Significance

Theorem 1 supplies a test for a vector of simultaneous service targets using a family of deterministic, weighted allocation problems. It applies to any feasible-set model satisfying the stated assumptions, rather than only to one pooling network. It also delineates the strength of the conclusion: satisfying all weighted tests guarantees arbitrarily close service, while exact attainment requires the additional assumptions in the paper's next result (Theorems 1–2).

The statements in this mission compile as Lean declarations, but their proofs have not yet been machine checked. Completing the mission would provide a reusable formal interface for demand-dependent feasible sets, measurable rationing policies, finite policy randomization, service expectations, and pointwise weighted optimization. Those definitions can also support formal study of the paper's later exact-feasibility and policy-optimality results.

Difficulty

The forward implication compares service under one policy with a maximum over feasible decisions at every demand. The reverse implication is harder: a weighted inequality for each $w$ must yield one policy that serves all customers simultaneously to a common tolerance. A separate policy chosen for each weight does not itself meet the vector of targets. The optimization involves a set of demand-dependent policies, and the source's argument relies on properties of its attainable service vectors that need explicit representation in Lean (proof of Theorem 1, pp. 13–14).

Formalization scope

Customers and resources are Fin n and Fin m, with zero-based indices; the paper numbers them from one. A solution is a pair $(s,y)$, and $P(c,D)$ remains an arbitrary feasible set. Deterministic policies are measurable functions of $D$ that select from $P(c,D)$ for every demand realization, at the theorem's fixed capacity. Randomized policies are finite probability mixtures of these selectors. Only finitely many expected services and costs occur in the statements, and finite mixtures represent the corresponding finite-dimensional expectation vectors of the paper's policy measures. The definition of asymptotic feasibility is made directly from these policies and their service values. The maximum in the theorem is made directly from $P(c,D)$ and $R$, so the equivalence cannot follow from defining either side in terms of the other.

The paper defines $R_j$ on nonnegative pairs. Lean uses a total real-valued extension; the theorem requires it to be nonnegative, monotone and upper semicontinuous as specified, and jointly measurable. A common integrable envelope bounds every feasible service value, preventing a nonintegrable Bochner integral from silently taking Lean's default value of zero. A measurable maximizing selector is assumed for every nonnegative $w$; it ensures that the expectation of $M_w(D)$ and the policy behind the source's tie-breaking are meaningful. The demand law is a probability measure with bounded second moment and nonnegative demand, capacity is nonnegative, and $\beta_j\in(0,1)$, matching the section's standing setup. Compactness alone permits an empty feasible set in Lean; the selector assumption ensures nonemptiness at each demand.

The definitions include the linear allocation-cost functional because Lemma 1 is stated with the paper's general $f$. An integrable envelope also bounds its absolute value in that milestone. Reusable work includes measurable selection for a demand-dependent compact feasible set, integrability of finite policy mixtures, interchange of the pointwise optimum and expectation under the stated bounds, and the finite-dimensional minimax statement. Proofs or improvements to these interfaces are welcome as long as the source claims retain their stated strength.

Selected references

• J. Jiang, S. Wang, and J. Zhang, Achieving High Individual Service-Levels without Safety Stock? Optimal Rationing Policy of Pooled Resources, SSRN preprint 3385089, version of 31 July 2021. SSRN.
• J. Jiang, S. Wang, and J. Zhang, Achieving High Individual Service-Levels without Safety Stock? Optimal Rationing Policy of Pooled Resources, Operations Research, 2023. DOI: 10.1287/opre.2022.2386. The mission's labels and pages follow the SSRN preprint.

Motivation

In the secretary problem $n$ candidates arrive one at a time in uniformly random order; at each arrival the decision maker sees only how the current candidate compares with the earlier ones and must accept or reject irrevocably, aiming to accept the best candidate overall. Dütting, Lattanzi, Paes Leme and Vassilvitskii, Secretaries with Advice (arXiv:2011.06726), study a family of variants in which each candidate also carries a signal about its quality, and show that for many of them the optimal stopping rule is the solution of a finite factor-revealing linear program whose dual can be solved greedily by backward induction.

One of their main examples is the secretary problem with samples: before the $n$ candidates arrive, $k$ further elements of the same random order are revealed as a sample, and a candidate's signal is the number of sample elements smaller than it. This model interpolates between the classical problem ($k=0$, optimal success probability tending to $1/e$) and, as $k\to\infty$, the full-information problem of Gilbert and Mosteller (1966). The paper's Theorem 17 gives the optimal dual solution of this LP in closed form.

Setting

Fix natural numbers $n\ge 1$ (secretaries) and $k\ge 0$ (samples). Rounds are $i=1,\dots,n$; signals are $s\in\{0,1,\dots,k\}$. The dual LP of §5 has the coefficients

$$a(i,s)=\frac{1}{k+1}\prod_{t=1}^{n-1}\frac{s+t}{k+t+1},\qquad c(j,s',i,s)=\frac{1}{s'+1}\prod_{t=1}^{i-1}\frac{s+t}{s'+t+1}\ \ (s'\ge s),$$

with $c(j,s',i,s)=0$ for $s'<s$, and reads

$$\min\sum_{i}\sum_{s}u(i,s)\quad\text{s.t.}\quad u(i,s)+\sum_{j>i}\sum_{s'\ge s}u(j,s')\,c(j,s',i,s)\ge a(i,s),\quad u(i,s)\ge 0 .$$

The greedy solution (equation (8) of the paper) sets $u(n,s)=a(n,s)$ and, going backwards,

$$u(i,s)=\max\Bigl\{0,\ a(i,s)-\sum_{j>i}\sum_{s'}u(j,s')\,c(j,s',i,s)\Bigr\}\qquad(i<n).$$

The un-clipped recursion $v(i,s)$ is the same backward induction with the $\max\{0,\cdot\}$ removed. In Lean, the generic recursion (8) is greedyDual (and unclippedDual) over an arbitrary finite signal type, and the samples instance is samplesGreedy n k i s (resp. samplesUnclipped) with s : Fin (k + 1). Products $\prod_{t=a}^{b}$ with $b<a$ equal $1$.

Formalization targets

Goal: Theorem 17

For every $1\le i\le n$ and $0\le s\le k$: $u(n,s)=a(n,s)$, and for $i<n$

$$u(i,s)=\max\left\{0,\frac{1}{k+1}\prod_{t=1}^{i-1}\frac{s+t}{k+t+1}\left(\prod_{t=i}^{n-1}\frac{s+t}{k+t+1}-\frac{\sum_{j=1}^{n-i}\binom{n-i}{j}\frac1j\prod_{\ell=1}^{j}(k-s+\ell)\prod_{\ell=1}^{n-i-j}(s+i-1+\ell)}{\prod_{t=i}^{n-1}(k+t+1)}\right)\right\}.$$

Milestones (the steps of the paper's proof)

1. Reduction (p. 17): if $v(i',\cdot)$ has the closed form for all $i'>i$, then $v(i,s)=a(n,s)-\frac{1}{k+1}\prod_{t=1}^{n-1}\frac{1}{k+t+1}\prod_{t=1}^{i-1}(s+t)\sum_{s'=s}^{k}T(i,s')$, with $T(i,s')$ an explicit double sum.
2. Two forms of $T$ (pp. 17–18): the double sum collapses to $\sum_{j=1}^{n-i-1}(n-i)\binom{n-i-1}{j}\frac{1}{j(j+1)}\prod_{\ell\le j}(k-s'+\ell)\prod_{t=i+1}^{n-j-1}(s'+t)$.
3. Key identity (p. 18): $\sum_{s'=s}^{k}T(i,s')=\sum_{j=1}^{n-i}\binom{n-i}{j}\frac1j\prod_{\ell=1}^{j}(k-s+\ell)\prod_{t=i}^{n-j-1}(s+t)$.
4. Base case $s=k$ (p. 18) and 5. inductive step $s+1\to s$ (Appendix B, pp. 26–28) of the key identity.
5. Un-clipped closed form (pp. 17–19): $v(i,s)$ equals the expression inside the max, for all $1\le i\le n$.

Significance

Theorem 16 of the paper shows that the greedy dual solution is optimal and that the optimal policy for secretaries with samples is a threshold policy in the signal: accept a best-so-far candidate in round $i$ iff its signal is large enough. Theorem 17 makes this solution explicit, so the optimal thresholds can be read off from the sign of a closed-form expression rather than computed by running the backward recursion, and it is the discrete precursor of the paper's Corollary 18, which recovers the Gilbert–Mosteller full-information thresholds in the limit $k\to\infty$.

The identities are proved in the paper by explicit manipulation of finite sums and products of binomials. No machine-checked version exists. A formal proof checks the long index computations of the proof and of Appendix B, and closes a gap: the paper proves the identity for the un-clipped recursion only ("for the proof we can ignore the $\max\{0,\cdot\}$") and does not argue why the clipped greedy solution has the same form. The goal as stated here, with the maximum, is the statement the paper asserts.

Difficulty

The identities are rational-function identities in $s$, $k$ and the round indices, with sums whose ranges depend on the summation variables and products whose ranges may be empty. The natural first idea, induction on $n-i$ directly on the formula, requires the key identity for $\sum_{s'=s}^{k}T(i,s')$, a double sum over $s'$ and $j$ of products of rising factorials; the paper handles it by a second backward induction over $s$, and both the base case and the step re-index sums with shifted bounds and boundary terms such as $(n-i-1)!$ and $\frac{1}{n-i}\prod_{\ell=1}^{n-i}(k-s+\ell)$.

The passage from the un-clipped to the clipped recursion is a separate difficulty: once $u(j,s')$ is clipped to $0$ at a later round, the sums used at earlier rounds differ from those of the un-clipped recursion, and the closed form survives only because the clipped entries do not affect the relevant sums. That argument is not in the paper.

Formalization scope

• Rounds are natural numbers $1\le i\le n$ (1-based, as printed); signals are Fin (k + 1) in the recursion and naturals $s\le k$ in the formulas. All arithmetic is in $\mathbb R$; naturals are cast before $k-s$, and the natural differences $n-i$, $n-i-j$, $n-j-1$ appear only where the ranges keep them non-truncated.
• Products and sums are over Finset.Icc a b, empty when $b<a$, matching the paper's convention.
• The recursion is defined by well-founded recursion on $n-i$ and sums over all later rounds $j\in\{i+1,\dots,n\}$ and all signals; $c=0$ for $s'<s$ encodes the paper's $\sum_{s'\ge s}$.
• The goal keeps the $\max\{0,\cdot\}$. Stating instead the identity for the un-clipped recursion would be a different (weaker-content) theorem; it is milestone 6.
• No probability model appears: the coefficients are taken as given by their formulas on p. 15. Their probabilistic derivation, the optimality of the greedy solution (Theorem 16), the running time of the LP algorithm, the "natural interpretation" paragraph, Corollary 18 and the plots are out of scope.
• The generic recursion greedyDual is reusable for any instance of the paper's factor-revealing LP (the binary-classifier model of §6 included). General lemmas about sums of rising factorials (ascPochhammer) and binomial re-indexing developed for the milestones are welcome contributions.

Selected references

• P. Dütting, S. Lattanzi, R. Paes Leme, S. Vassilvitskii, Secretaries with Advice, arXiv:2011.06726v1, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2011.06726
• J. P. Gilbert, F. Mosteller, Recognizing the Maximum of a Sequence, Journal of the American Statistical Association 61(313), 1966. https://doi.org/10.1080/01621459.1966.10502008
• T. S. Ferguson, Who Solved the Secretary Problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

Motivation

Banks lend to each other. When one bank's investments fail, it may be unable to repay its interbank debt, and its creditors then receive less. Since Eisenberg and Noe (2001), the standard way to compute who pays whom after such losses has been a clearing vector: a fixed point of a system in which every bank pays the smaller of what it owes and what it has. Much of the later literature on systemic risk takes the banks' assets as given and asks how losses spread through this fixed point, for example Acemoglu, Ozdaglar and Tahbaz-Salehi (2015).

Chong Shu's paper Endogenous Risk Exposure and Systemic Instability (Management Science, doi:10.1287/mnsc.2022.01519) reverses the question: when banks know they are connected, how much risk do they choose? A successful bank pays its interbank debt in full while its failed counterparties do not, so success is partly taxed by the network. This cross-subsidy shrinks the reward for choosing a safe project. The paper's first main result, Proposition 1, says that in every network the banks' risk choices are strategic complements: when one bank takes more risk, every other bank wants to take more risk too. This mission formalizes Proposition 1.

Setting

A finite set of banks is given. For banks $i,j$, $\bar d_{ij}\ge 0$ is the face value of the debt that bank $j$ owes bank $i$. Bank $j$'s total interbank liability is $\bar d_j=\sum_i\bar d_{ij}$, assumed positive, and $\theta_{ij}=\bar d_{ij}/\bar d_j$ is bank $i$'s share of it. Bank $i$ also owes a deposit $v_i>0$, which must be paid before its interbank debt.

Every bank $i$ picks a project $Z_i$ from an interval $[\underline Z,\overline Z]$. The project pays $Z_i$ with probability $P(Z_i)$ and $0$ otherwise, independently across banks. Assumption 1: $P(z)\in(0,1)$, $P$ is decreasing, and $P(z)\,z$ is concave. A standing assumption rules out systemic default: $\underline Z\ge v_i+\bar d_i$ for every $i$, so a bank whose project succeeds can always pay in full.

A state $\omega\in\{s,f\}^N$ records which projects succeeded; bank $i$'s cash flow is $e_i=Z_i$ if $\omega_i=s$ and $0$ otherwise. A payment equilibrium $d^*(\omega;Z)$ solves

$$d_i^*=\Big\{\min\Big[\sum_j\theta_{ij}d_j^*+e_i-v_i,\ \bar d_i\Big]\Big\}^+\quad\text{for all } i .$$

Bank $i$'s profit is $\Pi_i=(\sum_j\theta_{ij}d_j^*+e_i-v_i-d_i^*)^+$, and its expected profit $\mathbb E[\Pi_i(\omega;Z)]$ is the sum over states weighted by $\Pr(\omega)=\prod_j\Pr(\omega_j)$. The best-response set $\hat Z_i(Z_{-i})$ is the set of maximizers of $\mathbb E[\Pi_i]$ over $Z_i\in[\underline Z,\overline Z]$, with the other banks' choices $Z_{-i}$ held fixed. The cross-subsidy is

$$\mathcal D_i(Z_{-i})=\sum_{\omega_{-i}}\Big(\bar d_i-\sum_j\theta_{ij}d^*_j(\omega^{i=s})\Big)\Pr(\omega_{-i}),$$

bank $i$'s expected net payment to the network when its own project succeeds.

Formalization targets

Goal: Proposition 1 (p. 10)

For banks $i\ne m$, profiles $Z\in[\underline Z,\overline Z]^N$, and $Z'$ equal to $Z$ except that $Z_m\le Z'_m$:

$$\hat z\in\hat Z_i(Z_{-i}),\ \hat z'\in\hat Z_i(Z'_{-i})\ \Longrightarrow\ \max(\hat z,\hat z')\in\hat Z_i(Z'_{-i})\ \text{ and }\ \min(\hat z,\hat z')\in\hat Z_i(Z_{-i}).$$

This is the strong-set-order form of "$\hat Z_i$ is nondecreasing in $Z_m$". It does not require the network to be regular or path-connected.

Milestones, in the order of the paper's proof

1. Lemma 2 (p. 8): $d^*(\omega;Z)$ does not depend on $Z$.
2. Auxiliary Lemma (IA p. 7): $d^*(\omega^{j=f})\le d^*(\omega^{j=s})$ componentwise.
3. (7) (p. 9): $\mathbb E[\Pi_i]=P(Z_i)(Z_i-v_i)-P(Z_i)\mathcal D_i(Z_{-i})+(1-P(Z_i))\cdot(\text{expected payoff after failure})$.
4. (I.4) (IA p. 8): $\mathcal D_i(Z_{-i})\le\mathcal D_i(Z'_{-i})$.
5. The $\Omega^{f+}_{-i}$ claims (IA p. 9): a bank that survives its own failure pays $\bar d_i$ in full, and its own state does not change what it receives.
6. $\mathcal D^*_i$ is increasing in $Z_m$ (IA p. 10).
7. Supermodularity (IA p. 10): $\mathbb E[\Pi_i]$ has increasing differences in $(Z_i,Z_m)$.

The regular-network step (I.3) (IA p. 7), that the maximizer of $P(z)(z-v)-P(z)D$ is increasing in $D$, is also posed, as a theorem outside the milestone list.

Significance

Proposition 1 makes the risk-taking game supermodular. That property is what the rest of the paper relies on. It gives existence of equilibrium (Proposition 2) through Tarski's fixed-point theorem, it identifies least and greatest equilibria, and it lets the later comparative statics compare networks: complete against ring, size, central clearing, bailouts. Each of these results argues "the cross-subsidy rises, so equilibrium risk rises", and that step is Proposition 1 applied through Topkis's monotonicity theorem.

On the formal side, no clearing model is currently on the platform. This mission supplies one: the Eisenberg–Noe clearing system with a stochastic state, the greatest clearing vector, expected profits, and best responses. It also checks the paper's proof in the non-regular case. That proof splits on the states in which a bank survives its own failure, and one inequality in it is asserted without proof. The result is proved on paper; none of it has been machine-checked.

Difficulty

In a regular network a failed bank always defaults, and the argument reduces to two monotonicity facts: (I.3) and (I.4). In a non-regular network a failed bank can still earn a profit when enough of its debtors succeed. A riskier counterparty then has two opposite effects. It raises the cross-subsidy, which pushes toward risk, and it lowers the chance of being bailed out after one's own failure, which pushes away from risk. The proof must show that the first effect dominates in every network. It does so by partitioning the states according to whether bank $i$ survives its own failure, $\Omega^{f+}_{-i}$, and by showing that the states in that set contribute nothing to the cross-partial. This requires the clearing vector to be monotone in every bank's success and stable when a surviving bank's own state flips. It also needs an inequality, $v_i+\bar d_i\ge\sum_j\theta_{ij}d^*_j(\omega^{m=f,i=s})$ whenever $\omega^{m=f}_{-i}\notin\Omega^{f+}_{-i}$, which the paper asserts without proof.

The naive route is to differentiate the first-order condition, as the paper does in (I.3). That route is not available: Assumption 1 gives neither differentiability of $P$ nor a unique maximizer.

Formalization scope

Banks form a finite type, and states are Boolean vectors (true = success). All probabilities are finite products and all expectations are finite sums: no measure theory is involved. Sums over $\omega_{-i}$ are written as sums over full states with $\omega_i$ fixed, weighted by the product over $j\ne i$.

Conventions the Lean statements commit to:

• $\bar d_{ij}\ge0$ rather than the page's $\bar d_{ij}>0$. This is the reading forced by the paper's own ring network (Definition 3), and every total $\bar d_j>0$ is assumed. Self-loops are allowed.
• $d^*$ is the greatest solution of the clearing system, the componentwise supremum of all solutions in $[0,\bar d]$. Lemma 1 asserts only generic uniqueness, so a selection is required. The greatest solution is the one Eisenberg–Noe's algorithm returns, and it equals the solution whenever that is unique.
• "Decreasing" in Assumption 1 is read weakly (AntitoneOn), which is the more general hypothesis.
• Every bank's choice, including the varied $Z'_m$, lies in $[\underline Z,\overline Z]$, and the no-default assumption $\underline Z\ge v_i+\bar d_i$ is an explicit hypothesis. Without either, Lemma 2 fails.
• Derivative statements are replaced by order-theoretic ones: the strong set order for $d\hat Z_i/dZ_m\ge0$ and for (I.3), increasing differences for the cross-partial. Strict "$>0$" claims become weak, because they are false when banks $i$ and $m$ are not path-connected.

The goal is vacuous when a best-response set is empty. This is faithful, since $\hat Z_i$ presupposes a maximizer, and best responses exist whenever $P$ is continuous. A formalization that takes $d^*$ as an arbitrary solution under a uniqueness hypothesis, or as an sSup that could be junk, would trivialize the mission. The definition used here is shown, in a sorry-free check, to solve the clearing system.

Not posed: Lemma 1 (cited from Eisenberg–Noe), Proposition 2 and Corollary 1 (consequences of Proposition 1), and the later comparative statics (Propositions 3–9). Proposition 4, the comparison of complete and ring networks, is a separate mission of this series. Reusable contributions are welcome: monotonicity of greatest fixed points in a parameter, and a general Topkis-style argmax monotonicity on chains.

Selected references

• Chong Shu, Endogenous Risk Exposure and Systemic Instability, Management Science (accepted manuscript, 17 Sep 2024). https://doi.org/10.1287/mnsc.2022.01519
• Larry Eisenberg and Thomas H. Noe, Systemic Risk in Financial Systems, Management Science 47(2), 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
• Daron Acemoglu, Asuman Ozdaglar and Alireza Tahbaz-Salehi, Systemic Risk and Stability in Financial Networks, American Economic Review 105(2), 2015. https://doi.org/10.1257/aer.20130456
• Paul Milgrom and John Roberts, Rationalizability, Learning, and Equilibrium in Games with Strategic Complementarities, Econometrica 58(6), 1990. https://doi.org/10.2307/2938316
• Paul Milgrom and Chris Shannon, Monotone Comparative Statics, Econometrica 62(1), 1994. https://doi.org/10.2307/2951479
• Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

Motivation

Antitrust authorities review horizontal mergers by asking whether the merged firm will raise prices. A prior question is which mergers firms will choose to form at all. When several firms can merge, the identity of the partner matters: a large firm may absorb a small rival, or two small rivals may combine to face the large one. Wang, Wu, Tang and Dai (Management Science, 2024) study this partner-selection question in a price-competition model with two frictions common in retail and service markets: limited capacity of the small firms, and loyal segments, buyers who only buy from their own firm. Their main result says exactly which merger, if any, arises in equilibrium. Every step of its proof is an explicit comparison of closed-form profits, which makes the result a natural target for complete machine verification.

Setting

Three firms $A$, $B$, $C$ sell a homogeneous product at zero marginal cost. A unit mass of buyers each demand one unit and value it at the reservation price $r>0$. Each firm has $\alpha$ loyal buyers, $0<\alpha<1/3$; the remaining $1-3\alpha$ buyers are switchers who buy from the cheapest firm. Firm $A$ is unconstrained; the small firms $B$ and $C$ each have capacity $k$, with $\alpha<k<1$. Unserved buyers are rationed at random and spill over to the next cheapest firm.

The firms may stay independent, $\{A,B,C\}$; firm $A$ may merge with one small firm, the mixed merger $\{AB,C\}$; or the two small firms may merge, the small merger $\{A,BC\}$. A merged entity pools capacities and loyal buyers. In each structure the firms play a price game whose equilibrium is in mixed strategies. The paper's Table A1 lists, for each structure, the lower bound of price support $L^{(0)}$, $L^{(AB)}$, $L^{(BC)}$ and the equilibrium profits $\Pi^{(0)}_A$, $\Pi^{(0)}_B=\Pi^{(0)}_C$, $\Pi^{(AB)}$, $\Pi^{(AB)}_C$, $\Pi^{(BC)}_A$, $\Pi^{(BC)}$, as piecewise functions of $(\alpha,k,r)$ built from

$$s_1=(1-3\alpha)\Bigl(1-\tfrac{k}{1-2\alpha}\Bigr),\quad s_2=s_1\Bigl(1-\tfrac{k}{\alpha+s_1}\Bigr),\quad s_3=(1-3\alpha)\Bigl(1-\tfrac{2k}{1-\alpha}\Bigr),$$

the numbers of spilled-over switchers. In the small merger each small firm receives half: $\Pi^{(BC)}_B=\Pi^{(BC)}_C=\Pi^{(BC)}/2$.

A structure is an equilibrium structure when no firm or coalition gains by deviating. For $\{AB,C\}$ this is

$$\text{(1a) } \Pi^{(AB)}>\Pi^{(0)}_A+\Pi^{(0)}_B,\qquad \text{(1b) } \Pi^{(AB)}>\Pi^{(BC)}_A+\Pi^{(BC)}_B\ \text{ or }\ \Pi^{(AB)}_C\ge\Pi^{(BC)}_C ;$$

for $\{A,BC\}$ it is

$$\text{(2a) } \Pi^{(BC)}_C>\Pi^{(0)}_C,\qquad \text{(2b) } \Pi^{(BC)}_A+\Pi^{(BC)}_B\ge\Pi^{(AB)} ;$$

and the status quo $\{A,B,C\}$ is the equilibrium structure when neither condition (1) nor condition (2) holds.

Formalization targets

Goal: Proposition 3

With $k^*=\alpha(1-2\alpha)/(1-3\alpha)$,

$$\{S : S\text{ is an equilibrium structure}\}= \begin{cases} \{\{AB,C\}\} & \text{if } k^*<k<1-2\alpha,\\ \{\{A,B,C\}\} & \text{otherwise.} \end{cases}$$

The statement is an exact characterization: in the interval the mixed merger is an equilibrium structure and the small merger is not; outside it neither merger is.

Milestones

1. Lemmas 3–5: on the regions $\Omega^{(0)}_{1,2}$, $\Omega^{(BC)}_{1,2,3}$, $\Omega^{(AB)}_{1,2}$ of the $(\alpha,k)$ plane, each Table A1 maximum equals one explicit branch.
2. Proposition 1: for $k\ge 1-2\alpha$ the independent structure is the unique equilibrium structure.
3. Proposition 2 and the inequality $s_2<s_3$ from its proof: $L^{(AB)}\ge L^{(BC)}\ge L^{(0)}$.
4. The comparisons in the proof of Proposition 3: the $\Sigma$ inequality, the threshold $k^*$ for (1a), the joint profit of $A$ and $B$ under $\{A,B,C\}$, $\{A,BC\}$ and $\{AB,C\}$, and firm $C$'s three pairwise profit comparisons.

Significance

The result separates the two forces of the model. Loyal buyers make a merged entity less aggressive in price, which is why no merger is profitable when capacity is ample. Limited capacity creates spillover demand, which a large firm captures by merging with a small rival but which two small firms do not capture by merging with each other. Proposition 3 says the second force wins exactly on $(k^*,1-2\alpha)$ and that the small merger never forms. This answers one of the paper's opening questions, whether two capacity-constrained small firms merge to compete with a large one: in this model they do not.

The paper proves the result by hand, over eight regions of the parameter plane (its Figure A1). The comparisons involve rational functions whose denominators are positive only under the region's constraints, and threshold curves with square roots. A machine-checked proof certifies the region bookkeeping. No formalization of this result exists.

Difficulty

Each single comparison is elementary algebra; the difficulty is the case structure. Table A1 has four rows in $k$ whose boundaries ($(1-2\alpha)^2/(2-5\alpha)$, $(1-\alpha)/2$, $1-2\alpha$) differ per column, and three of its cells are maxima whose active branch changes along the curves $k^{(0)}_{1,2}$, $k^{(BC)}_{1,2}$, $k^{(AB)}_1$. Root-location facts such as $\alpha<k^{(0)}_1$ and $k^{(BC)}_2<(1-2\alpha)^2/(2-5\alpha)$ are needed to know which row a region lies in. One inclusion the proof uses is only shown in the paper's figure: on $\Omega^{(BC)}_1$, where condition (2a) holds, one needs $k>k^*$ in order to conclude that (2b) fails. At the region boundaries $k=(1-\alpha)/2$ and $k=k^{(AB)}_1$ several of the proof's strict inequalities are equalities.

Formalization scope

Everything is stated over the reals in the namespace EndogMerger.SymLoyal. All definitions take explicit parameters (α k r : ℝ). The standing assumptions $0<\alpha<1/3$, $\alpha<k$, $r>0$, and $k<1$ or $k<1-2\alpha$ as each statement requires, are hypotheses of each theorem. Relative to the paper, $0<\alpha$ replaces $0\le\alpha$ (every region of the analysis has $\alpha>0$), and $r>0$ is made explicit. Firm $A$'s capacity $k_A\ge 1-2\alpha$ does not enter Table A1 and is not modelled. The split of $\Pi^{(AB)}$ between $A$ and $B$ is left unspecified, as in the paper.

Table A1 is the definition. The profits and lower bounds are defined by Table A1's piecewise expressions, row by row, with max where the table has a maximum. The paper's derivation of these values as equilibrium outcomes of a mixed-strategy price game with random rationing is not formalized; Section 6 of the paper itself obtains Proposition 3 from the Table A1 profits. The paper's PDF page numbers are cited throughout; the appendix restarts its printed numbering, so printed page numbers are not used.

Three trivializing formalizations are ruled out. The profits are not defined by the closed forms of Lemmas 3–5, which would make those lemmas definitional. The equilibrium predicate for $\{A,B,C\}$ requires that neither condition (1) nor condition (2) holds, so the goal includes the claim that the small merger is never an equilibrium. The thresholds $\alpha^{(0)}_1$ and $\alpha^{(BC)}_1$ are not defined by the paper's equation $k_1(\alpha_1)=k_2(\alpha_1)$, which Real.sqrt satisfies for every $\alpha$ with a negative radicand. Instead $\alpha^{(BC)}_1=(11-\sqrt{17})/52$, and $\alpha^{(0)}_1$ is a parameter pinned as the root in $(0,1/3)$ of $-43\alpha^3+43\alpha^2-13\alpha+1$.

Where the paper's proof claims a strict inequality on a closed region whose boundary gives equality, the milestone states it on the open region, and its Formalization Note says so.

No library beyond Mathlib's real arithmetic and Real.sqrt is needed. Lemmas about the threshold curves, for example that $k^{(AB)}_1(\alpha)$ lies in $(\alpha,(1-\alpha)/2)$, are reusable across milestones. Contributions of intermediate lemmas, including the region inclusion $\Omega^{(BC)}_1\subseteq\{k>k^*\}$, are welcome.

Selected references

• D. Wang, X. Wu, C. S. Tang, Y. Dai, Endogenous Merger Decisions Among Competitors: Impact of Limited Capacity and Loyal Segments, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.01943
• H. R. Varian, A Model of Sales, American Economic Review 70(4), 1980. https://www.jstor.org/stable/1803558
• S. W. Salant, S. Switzer, R. J. Reynolds, Losses from Horizontal Merger: The Effects of an Exogenous Change in Industry Structure on Cournot–Nash Equilibrium, Quarterly Journal of Economics 98(2), 1983. https://doi.org/10.2307/1885626

Conditioning on a covariate under distributional ambiguity

A portfolio manager who observes side information (a covariate $X$, such as a market indicator) before choosing a portfolio wants to control the loss of the asset returns $Y$ conditional on the observed covariate value $x_0$. The conditional law of $Y$ given $X=x_0$ is unknown and must be learned from $N$ historical pairs $(\widehat x_i,\widehat y_i)$. When $x_0$ itself was never observed, the empirical conditional law is undefined, and kernel or nearest-neighbour estimates are fragile. Nguyen, Zhang, Wang, Blanchet, Delage and Ye (arXiv:2103.16451v3, Operations Research, 2025) robustify the conditional decision with an optimal transport ambiguity set: the decision maker hedges against every joint law $\mathbb Q$ of $(X,Y)$ within transport distance $\rho$ of the empirical law. The resulting objective is a ratio of two linear functionals of $\mathbb Q$, so the standard Wasserstein distributionally robust duality (Blanchet and Murthy, 2019; Gao and Kleywegt, 2023) does not apply directly.

The paper settles every regime of the three parameters (ball radius $\rho$, fiber radius $\gamma$, minimum fiber mass $\varepsilon$). This mission formalizes the simplest regime, $\gamma=\varepsilon=0$, where the answer is negative: the worst case does not depend on the data at all.

Setting

The covariate space $\mathcal X$ and the return space $\mathcal Y$ are Polish spaces with their Borel $\sigma$-algebras. Two ground costs $\mathbb D_{\mathcal X}$ and $\mathbb D_{\mathcal Y}$ combine into the separable cost $\mathbb D((x,y),(x',y'))=\mathbb D_{\mathcal X}(x,x')+\mathbb D_{\mathcal Y}(y,y')$. The data define the empirical measure $\widehat{\mathbb P}=\frac1N\sum_{i\in[N]}\delta_{(\widehat x_i,\widehat y_i)}$.

The optimal transport cost between two probability measures $\mathbb Q_1,\mathbb Q_2$ on $\mathcal X\times\mathcal Y$ is

$$W(\mathbb Q_1,\mathbb Q_2)=\inf\{\mathbb E_\pi[\mathbb D(\xi_1,\xi_2)]:\pi\in\Pi(\mathbb Q_1,\mathbb Q_2)\},$$

the infimum over couplings $\pi$ with marginals $\mathbb Q_1$ and $\mathbb Q_2$. The ambiguity set is the ball $\mathbb B_\rho=\{\mathbb Q:W(\mathbb Q,\widehat{\mathbb P})\le\rho\}$.

Given a covariate value $x_0$ and a radius $\gamma\ge0$, the neighbourhood is $\mathcal N_\gamma(x_0)=\{x:\mathbb D_{\mathcal X}(x,x_0)\le\gamma\}$, and $\mathcal N_\gamma(x_0)\times\mathcal Y$ is the fiber set. For a loss $\ell(y)=\ell(y,\alpha,\beta)$ at a fixed decision $(\alpha,\beta)$ and a law $\mathbb Q$ with positive fiber mass, the conditional expected loss is

$$\mathbb E_{\mathbb Q}[\ell(Y)\mid X\in\mathcal N_\gamma(x_0)]=\frac{\mathbb E_{\mathbb Q}[\ell(Y)\mathbb 1_{\mathcal N_\gamma(x_0)}(X)]}{\mathbb Q(X\in\mathcal N_\gamma(x_0))}.$$

The paper's standing Assumption 2.4 requires: (i) $\mathbb D_{\mathcal X}$ and $\mathbb D_{\mathcal Y}$ are symmetric, non-negative and continuous, and $\mathbb D$ vanishes exactly on the diagonal; (ii) every $\widehat x_i$ has a unique projection onto $\mathcal N_\gamma(x_0)$; (iii) every boundary point of $\mathcal N_\gamma(x_0)$ has points outside $\mathcal N_\gamma(x_0)$ at arbitrarily small cost.

With $\gamma=0$ the fiber is $\{x_0\}\times\mathcal Y$. With $\varepsilon=0$ the fiber-mass constraint is taken as the strict inequality $\mathbb Q(X=x_0)>0$, so that the conditioning event is never null.

Formalization targets

Goal: Proposition 3.1 (p. 14)

For every $x_0\in\mathcal X$, every $\rho>0$ and every loss $\ell:\mathcal Y\to\mathbb R$,

$$\sup_{\mathbb Q\in\mathbb B_\rho,\ \mathbb Q(X=x_0)>0}\mathbb E_{\mathbb Q}[\ell(Y)\mid X=x_0]=\sup_{y\in\mathcal Y}\ell(y),$$

both sides in $[-\infty,+\infty]$.

Milestones (in the order of the proof, pp. 40–41)

1. Representation of the ball (p. 40, the same set as display (24), p. 47): $\mathbb Q\in\mathbb B_\rho$ if and only if $\mathbb Q=\frac1N\sum_i\pi_i$ for probability measures $\pi_i$ with $\frac1N\sum_i\mathbb E_{\pi_i}[\mathbb D(\cdot,(\widehat x_i,\widehat y_i))]\le\rho$.
2. Lower bound (pp. 40–41): for every $y_0\in\mathcal Y$ some $\mathbb Q'\in\mathbb B_\rho$ has $\mathbb Q'(X=x_0)>0$ and $\mathbb E_{\mathbb Q'}[\ell(Y)\mid X=x_0]=\ell(y_0)$.
3. Upper bound (p. 41): $\mathbb E_{\mathbb Q}[\ell(Y)\mid (X,Y)\in S]\le\sup_y\ell(y)$ whenever $\mathbb Q(S)>0$.

Significance

The proposition shows that conditioning on a single covariate value with an optimal transport ball is uninformative: the worst-case conditional loss equals the robust optimization value $\sup_{y\in\mathcal Y}\ell(y,\alpha,\beta)$ for every data set. This is what motivates the rest of the paper: either a minimum fiber mass $\varepsilon>0$ (Theorem 3.2) or a fiber of positive radius $\gamma>0$ (Section 4) is needed for the data to matter. The paper contrasts this with the type-$\infty$ Wasserstein ball, for which it points to existing results to compute the worst case.

For the platform, the mission sets up the shared model of the series: the separable ground cost, the empirical measure, the fiber, the conditional expectation as an extended-real ratio, and the paper's Assumption 2.4. The ball representation (milestone 1) is used by every other mission of the series; it rests on the existence of optimal couplings on Polish spaces, which Mathlib does not yet have. The result is proved in the paper; no machine-checked proof is known to exist.

Difficulty

The statement is an equality of two suprema over very different index sets, and neither inequality reduces to the other. The natural first idea, that the worst case is attained by a small perturbation of the empirical measure, fails: the empirical measure may put no mass on the fiber $\{x_0\}\times\mathcal Y$, or put its mass there at returns far from where $\ell$ is large, and the value must be reached for every data set. Points of the data sitting exactly at $x_0$ are the delicate case, since the transport budget charges for every displacement of mass. The ball representation (milestone 1) is the hard infrastructure step in its "only if" direction: it needs an optimal coupling, i.e. attainment of the transport infimum on Polish spaces, which is absent from Mathlib.

Formalization scope

Samples are indexed by Fin N with $N\ge1$. The ground cost is $\max(\mathbb D_{\mathcal X}+\mathbb D_{\mathcal Y},0)$ as a $[0,\infty]$-valued function. The transport cost reuses the published RWPI.SqrtLasso.transportCost, an infimum over couplings whose first marginal is $\mathbb Q$ and second marginal is $\widehat{\mathbb P}$; the paper's "min" is not built into the definition. The radius enters as ENNReal.ofReal ρ, and the goal assumes $\rho>0$ as on the page ($\rho\in\mathbb R_{++}$). Expectations use the published ModelRiskOT.Duality.extIntegral, $\int\ell^+-\int\ell^-$ in $[-\infty,+\infty]$, so the loss $\ell:\mathcal Y\to\mathbb R$ is arbitrary: no measurability, boundedness or integrability. The loss stands for $\ell(\cdot,\alpha,\beta)$ at an arbitrary fixed decision, which is how "for any feasible $(\alpha,\beta)$" is read. The fiber at $\gamma=0$ is $\{x:\mathbb D_{\mathcal X}(x,x_0)\le0\}\times\mathcal Y$; that it equals $\{x_0\}\times\mathcal Y$ follows from Assumption 2.4(i). The boundary in Assumption 2.4(iii) is the topological frontier in $\mathcal X$.

One hypothesis is added to the paper and disclosed: $x_0$ is not isolated for $\mathbb D_{\mathcal X}$ (for every $r>0$ some $x\neq x_0$ has $\mathbb D_{\mathcal X}(x,x_0)\le r$). This is Assumption 2.4(iii) at $\gamma=0$ when the boundary of $\{x_0\}$ is read in an ambient Euclidean space, as the paper's remark on p. 11 does; the proof uses it, and without it the statement fails at an isolated $x_0$ that is also a sample point.

Trivializing encodings are excluded: the supremum ranges only over probability measures in the ball with strictly positive fiber mass, so the conditional expectation is never evaluated at a null fiber; no Bochner integral (which is $0$ for a non-integrable loss) is used; $\rho<0$ cannot enter through ofReal; and the feasible set is exactly $\mathbb B_\rho$ intersected with the positive-mass constraint.

Contributions welcome: the existence of optimal couplings for lower semicontinuous costs on Polish spaces (reusable far beyond this mission), the decomposition of couplings with a finitely supported marginal, and the two halves of the goal.

Selected references

• V. A. Nguyen, F. Zhang, S. Wang, J. Blanchet, E. Delage, Y. Ye, Robustifying conditional portfolio decisions via optimal transport, arXiv:2103.16451v3, 2024; Operations Research, 2025. https://arxiv.org/abs/2103.16451
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, Springer, 2009 (Theorem 4.1, existence of optimal couplings). https://doi.org/10.1007/978-3-540-71050-9
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
• R. Gao, A. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, Mathematics of Operations Research 48(2), 2023. https://doi.org/10.1287/moor.2022.1275