Operations Research

Motivation

Optimal portfolio liquidation asks how a trader should unwind a position of $\mathcal X$ shares over a horizon $[0,T]$ when trading moves prices. Since Almgren and Chriss (2001) the standard model charges a quadratic cost $\eta_t\xi_t^2$ for trading at rate $\xi_t$ (temporary impact) and a risk penalty $\lambda_tX_t^2$ on the open position, and imposes the liquidation constraint $X_T=0$. When many traders liquidate at once, each one's costs also depend on the others' aggregate trading rate $\mu_t$ through a permanent impact term $\kappa_t\mu_tX_t$. Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and prove that, under a weak-interaction condition, the game has a unique equilibrium.

The liquidation constraint makes the problem singular: the value function blows up at $T$, and the equilibrium is described by a forward-backward system whose decoupling field $A$ satisfies a Riccati BSDE with terminal value $A_T=+\infty$. A natural question is whether the constraint can be replaced by a finite penalty $nX_T^2$ on the unliquidated position, a non-singular problem of the type studied in the MFG literature, and whether the penalized equilibria approach the constrained one as $n\to\infty$. Section 4 of the paper answers this at the level of values. In the single-agent case, singular terminal conditions of this type were studied by Ankirchner, Jeanblanc and Kruse (SIAM J. Control Optim., 2014) and Graewe, Horst and Séré (Stochastic Process. Appl., 2018), references [3] and [28] of the paper.

Setting

Fix $T>0$, an $m$-dimensional Brownian motion $\widetilde W=(W^0,W)$ whose first coordinate $W^0$ is common noise, and an initial position $\mathcal X\in L^2$ independent of $\widetilde W$. Let $\mathbb F^0$ be the filtration of $W^0$ and $\mathbb F$ that of $(\mathcal X,\widetilde W)$, both augmented. The coefficients $\kappa,\lambda,\eta$ are bounded, nonnegative, $\mathbb F$-progressive processes, with $\lambda$ and $\eta$ bounded below by positive constants. Write $\kappa_{\max}$, $\eta_\star$, $\lambda_\star$ for the essential supremum of $\kappa$ and the essential infima of $\eta$ and $\lambda$, $\|\eta\|$ for the essential supremum of $|\eta|$, and $\alpha=\eta_\star/\|\eta\|\in(0,1]$. Assumption 2.3 adds the weak-interaction condition: some $\theta>0$ satisfies $\kappa_{\max}<4\eta_\star\theta$ and $\theta\kappa_{\max}<4\lambda_\star$.

Given an aggregate rate $\mu$, a trading rate $\xi\in L^2_{\mathbb F}$ yields the position $X^\xi_t=\mathcal X-\int_0^t\xi_s\,ds$. The constrained problem minimizes

$$J(\mathcal X,\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_s\mu_sX^\xi_s+\eta_s\xi_s^2+\lambda_s(X^\xi_s)^2\big)ds\,\Big|\,\mathcal X\Big]$$

over $\xi$ with $\int_0^T\xi_s\,ds=\mathcal X$; its value is $V(\mathcal X;\mu)$. The penalized problem (4.1) drops the constraint and minimizes

$$J^n(\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_t\mu_tX^\xi_t+\eta_t\xi_t^2+\lambda_t(X^\xi_t)^2\big)dt+n(X^\xi_T)^2\,\Big|\,\mathcal X\Big]$$

over all $\xi\in L^2_{\mathbb F}$, with value $V^n(\mathcal X;\mu)$. An equilibrium is a fixed point $\mu_t=\mathbb E[\xi^*_t|\mathcal F^0_t]$.

The constrained equilibrium is given by the FBSDE (2.3), $dX_t=-\frac{Y_t}{2\eta_t}dt$, $-dY_t=\big(\kappa_t\mathbb E[\frac{Y_t}{2\eta_t}|\mathcal F^0_t]+2\lambda_tX_t\big)dt-Z_t\,d\widetilde W_t$, $X_0=\mathcal X$, $X_T=0$, decoupled as $Y=AX+B$ where

$$-dA_t=\Big(2\lambda_t-\frac{A_t^2}{2\eta_t}\Big)dt-Z^A_t\,d\widetilde W_t,\qquad A_T=+\infty .$$

The penalized equilibria are given by the FBSDE (4.2) with $Y^n_T=2nX^n_T$, decoupled by $A^n$, the solution of the same Riccati BSDE with $A^n_T=2n$. The solutions live in weighted spaces: $\mathcal H_l$ with norm $\big(\mathbb E\sup_t|Y_t/(T-t)^l|^2\big)^{1/2}$, and the penalized analogue $\mathcal H^n_l$ with weight $(T-t+\eta_\star/n)^{-l}$. Assumption 4.1 requires a constant $C$ with $\exp\big(-\int_r^s\frac{A_u}{2\eta_u}du\big)\le C\frac{T-s}{T-r}$ for all $0\le r\le s<T$, almost surely.

Formalization targets

Goal: Theorem 4.6

Under Assumptions 2.3 and 4.1, with $\mu^*=\mathbb E[Y/(2\eta)|\mathcal F^0]$ the constrained equilibrium and $\mu^n=\mathbb E[Y^n/(2\eta)|\mathcal F^0]$ the penalized ones,

$$\lim_{n\to\infty}\mathbb E\big|V^n(\mathcal X;\mu^n)-V(\mathcal X;\mu^*)\big|=0 .$$

Milestones

1. Lemma 4.2 (first condition). If $\eta$ is deterministic, Assumption 4.1 holds.
2. Lemma A.3. $A^n$ exists uniquely, $A^n_t\ge\big(\frac1{2n}+\mathbb E[\int_t^T\frac{ds}{2\eta_s}|\mathcal F_t]\big)^{-1}$, $A^n\uparrow A$, and $\|A^n\|_{\mathcal M_{-1}}+\|A^n\|_{\mathcal M^n_{-1}}\le\mathfrak C$ uniformly in $n$.
3. Theorem 4.3. The FBSDE (4.4), with parameter $\mathfrak p\in[0,1]$ and data $f\in L^2$, has a unique solution in $\mathcal H^n_\alpha\times\mathcal H^n_\gamma\times S^2\times L^2\times L^2$.
4. Lemma 4.4. $\|X^n\|_{n,\alpha}+\|B^n\|_{n,\gamma}+\mathbb E\int_0^T|Y^n_t|^2dt\le\overline{\mathfrak C}$ uniformly in $n$.
5. (4.8). Under Assumption 4.1 the constrained equilibrium position satisfies $\|X^*\|_1<\infty$.
6. Lemma 4.5. $(X^n,B^n,Y^n)\to(X,B,Y)$ in $L^2(dt\otimes d\mathbb P)$.

Significance

The result is a consistency statement between two models of liquidation. Penalized models are what a numerical scheme or a standard MFG solver can handle, since their FBSDEs have finite terminal data. Theorem 4.6 says that equilibrium values computed with a large penalty approximate the value of the hard-constrained game, and Lemma 4.5 says the same for positions and trading rates. Without it, a penalized model would be an unrelated object rather than an approximation of the constrained one.

The result is proved in the paper; it is not formalized anywhere. A machine-checked development would need, beyond the paper, the theory of quadratic BSDEs with finite and singular terminal values, conditional mean-field FBSDEs with common noise, and conditional essential infima of control problems. The milestones isolate reusable pieces: the monotone approximation of a singular Riccati BSDE (Lemma A.3) and uniform estimates in $n$-dependent weighted spaces (Lemma 4.4).

Difficulty

The obvious argument compares the two problems control by control: the constrained optimizer is admissible for the penalized problem, so $V^n\le V$ up to the change of $\mu$. The reverse inequality is where it fails. The penalized optimizer leaves a residual position $X^n_T\neq0$, and its cost has to be compared with the singular one, whose weight $(T-t)^{-1}$ explodes at $T$. Controlling this requires estimates uniform in $n$ in spaces whose weights $(T-t+\eta_\star/n)^{-l}$ degenerate as $n\to\infty$, and the bare exponent $\alpha=\eta_\star/\|\eta\|<1$ of the constrained problem is not enough to make the boundary terms vanish. Assumption 4.1, which upgrades the state to $\mathcal H_1$, is what closes the gap. In addition, the aggregate rate $\mu^n$ changes with $n$, so both the controls and the cost functional move at once.

Formalization scope

Time is $\mathbb R_{\ge0}$; processes are real-valued functions of $(t,\omega)$; $W$ is the $m=k+1$-dimensional $\widetilde W$ with coordinate $0$ the common noise. Stochastic integrals and BSDEs come from the published definition Peng1990.SMP.Stochastic. BSDEs on $[0,T)$ are imposed on every $[0,\tau]$, $\tau<T$; $A_T=+\infty$ is $\lim_{t\uparrow T}A_t=+\infty$ a.s. Conditional expectations inside drivers are $\mathbb F^0$-progressive versions of integrable processes. Weighted norms are computed in $[0,\infty]$. The explicit readings are:

• $\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $dt\otimes d\mathbb P$; (2.4) is stated without division; "$1/\lambda,1/\eta\in L^\infty$" is a positive essential lower bound.
• Assumption 2.3 is a hypothesis of every statement, including Lemma A.3 (the appendix assumes only its boundedness part).
• Assumption 4.1 holds almost surely with the constant chosen before $\omega$ (as restated on p. 32).
• The penalty index is an integer $n\ge1$; constants in Lemma A.3 and Lemma 4.4 are chosen before $n$.
• The class of $A^n$ is $S^2\times L^2$ on $[0,T]$ (not printed in Lemma A.3).
• The penalized control set is $L^2_{\mathbb F}$, with no terminal constraint.
• Values are conditional essential infima given $\sigma(\mathcal X)$.
• The equilibria $\mu^n,\mu^*$ of Theorem 4.6 are defined through the FBSDE solutions, as in the proof; uniqueness of penalized equilibria is not claimed.
• The solution of Proposition 2.8 includes the relation $Y=AX+B$ on $[0,T)$; "Theorem 2.8" on pp. 25–29 means Proposition 2.8.
• $L^1$ convergence means $\int|V^n-V|\,d\mathbb P\to0$, not convergence of expectations.

A trivializing formalization would quantify over all solutions of the penalized MFG (claiming a uniqueness the paper does not state) or define $V$ by a pointwise infimum over all controls (which is $-\infty$ or junk); both are ruled out above. Contributions toward BSDE comparison principles and quadratic BSDE well-posedness on this stochastic-integral layer are welcome and reusable.

Selected references

• G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, Math. Oper. Res. 46(4), 2021; preprint arXiv:1804.04911v3. https://arxiv.org/abs/1804.04911
• R. Almgren, N. Chriss, Optimal execution of portfolio transactions, Journal of Risk 3, 2001. https://doi.org/10.21314/JOR.2001.041
• S. Ankirchner, M. Jeanblanc, T. Kruse, BSDEs with singular terminal condition and a control problem with constraints, SIAM J. Control Optim. 52(2):893–913, 2014 (reference [3] of the paper).
• P. Graewe, U. Horst, E. Séré, Smooth solutions to portfolio liquidation problems under price-sensitive market impact, Stochastic Process. Appl. 128(3):979–1006, 2018 (reference [28] of the paper).
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

Why optimize over a trained ReLU neuron

A trained feed-forward neural network with ReLU activations, $\mathrm{ReLU}(v)=\max\{0,v\}$, is a piecewise linear function of its input. Many tasks ask for an optimization over such a network with its weights held fixed: verifying that no small perturbation of an image changes its classification, finding adversarial examples, or embedding a learned model of demand or cost inside a decision problem ("predict, then optimize"). The standard way to solve such problems exactly is mixed-integer programming (MIP): each neuron is written as a small set of linear constraints with one binary variable, and the network is the composition of these neuron formulations. How strong each neuron formulation is decides how fast branch-and-bound can close the gap.

The formulation used in the literature up to 2018 is the big-M formulation. It is valid but weak. This mission formalizes the main result of Anderson, Huchette, Tjandraatmadja and Vielma, IPCO 2019 extended abstract (arXiv:1811.08359v2), which gives the strongest possible formulation of a single ReLU neuron that uses the original variables and one binary variable only.

Timeline. Big-M formulations of ReLU networks were used by several groups in 2017–2018 for verification and adversarial analysis (see §1.2 of the paper). Balas's disjunctive programming (1985, 1998) and the multiple choice formulation of piecewise linear functions (Vielma and Nemhauser, Math. Program. 2011) give an ideal formulation of the neuron that needs a copy of the input variables. Anderson et al. (2019) project out that copy and obtain the formulation (6) below; a longer journal version (Math. Program. 2020, with W. Ma) develops the analysis further, including interactions between neurons.

Setting

Fix $\eta\in\mathbb N$, a weight vector $w\in\mathbb R^\eta$, a bias $b\in\mathbb R$, and bounds $L,U\in\mathbb R^\eta$ with $L_i<U_i$ for every $i$. The neuron computes $\mathrm{ReLU}(f(x))$ for the affine function $f(x)=w\cdot x+b$ on the box $[L,U]=\{x: L\le x\le U\}$. Its graph is

$$\operatorname{gr}(\mathrm{ReLU}\circ f;[L,U])=\{(x,\mathrm{ReLU}(f(x))) : L\le x\le U\}.$$

The sign-adjusted bounds are $\breve L_i=L_i$, $\breve U_i=U_i$ when $w_i\ge 0$, and $\breve L_i=U_i$, $\breve U_i=L_i$ when $w_i<0$. Then $M^+(f)=w\cdot\breve U+b$ and $M^-(f)=w\cdot\breve L+b$ are the maximum and minimum of $f$ on $[L,U]$, and $\operatorname{supp}(w)=\{i: w_i\ne 0\}$. Strict activity means $M^-(f)<0<M^+(f)$: the neuron is neither always off nor always on. The paper assumes throughout that $L_i<U_i$ and that strict activity holds.

A set $R$ of points $(x,y,z)$ with $z\in[0,1]$, read together with the constraint $z\in\{0,1\}$, is a formulation of the graph if $(x,y)$ lies on the graph exactly when $(x,y,z)\in R$ for some $z\in\{0,1\}$; $R$ is then its LP relaxation. The formulation is ideal if every extreme point of $R$ has $z\in\{0,1\}$.

The big-M formulation (3) is $y\ge f(x)$, $y\le f(x)-M^-(f)(1-z)$, $y\le M^+(f)z$, $(x,y,z)\in[L,U]\times\mathbb R_{\ge0}\times\{0,1\}$. The formulation of Proposition 1 is

$$\begin{aligned} &y\ge w\cdot x+b &&(6a)\\ &y\le\sum_{i\in I}w_i\bigl(x_i-\breve L_i(1-z)\bigr)+\Bigl(b+\sum_{i\notin I}w_i\breve U_i\Bigr)z\qquad\forall I\subseteq\operatorname{supp}(w) &&(6b)\\ &(x,y,z)\in[L,U]\times\mathbb R_{\ge0}\times\{0,1\}. &&(6c) \end{aligned}$$

Formalization targets

Goal: Proposition 1 (p. 6)

$$\text{(6a)–(6c) is a formulation of }\operatorname{gr}(\mathrm{ReLU}\circ f;[L,U]),\ \text{and every extreme point of its LP relaxation has } z\in\{0,1\}.$$

Milestones (Appendix A.1 and §2.2)

1. The multiple choice formulation (5), with copies $x^0,x^1,y^0,y^1$, has only integral $z$ at extreme points in its lifted space and formulates the graph; projected to $(x,y,z)$, its LP relaxation is the convex hull of its points with $z\in\{0,1\}$ (§2.2, pp. 5–6).
2. Projecting the copies out of the LP relaxation of (5) gives the linear system (7): (6a), (6b), a second exponential family (7c), and the bounds (7d) (App. A.1, p. 14).
3. The family (7c) is implied by the other constraints (App. A.1, pp. 14–15).
4. The LP relaxation of (6) is the convex hull of its points with $z\in\{0,1\}$ (App. A.1, p. 14).

Companion results

• $M^\pm(f)$ are the maximum and minimum of $f$ on $[L,U]$ (§1.3, p. 4).
• Proposition 3 (p. 7): for $(\hat x,\hat y,\hat z)\in[L,U]\times\mathbb R_{\ge0}\times[0,1]$, if some inequality of (6b) is violated, the one for $\hat I=\{i\in\operatorname{supp}(w): w_i\hat x_i<w_i(\breve L_i(1-\hat z)+\breve U_i\hat z)\}$ is the most violated.
• The big-M formulation (3) is a formulation of the graph (p. 4); Examples 1 and 2 (p. 5) show that it is not ideal and that its gap grows like $\tfrac12\gamma\eta$; its inequalities (3b), (3c) are (6b) for $I=\operatorname{supp}(w)$ and $I=\emptyset$ (p. 7).

Significance

Proposition 1 says that the convex hull of the graph, lifted with one binary variable, is described by (6a), (6b) and the bounds, with no auxiliary continuous variables. Optimizing a linear function over the LP relaxation of (6) therefore gives the tightest convex relaxation available for a single neuron, and Proposition 3 gives a separation routine linear in $\eta$, so the exponential family can be added on demand to a big-M model. The paper's experiments (§3, not formalized) report that separating over (6b) solves smaller MNIST verification instances faster than Gurobi's default cut generation by a factor of 7.

The result is proved in the paper; nothing here is open. To our knowledge none of these statements has a machine-checked proof. The work this mission asks for is the formalization of the known proof: an ideality statement for the multiple choice formulation, a Fourier–Motzkin projection carried out for an arbitrary index set with general-sign weights, and the passage from a hull identity to integrality of extreme points.

Difficulty

The formulation half of Proposition 1 is a short case analysis on $z\in\{0,1\}$; the content is ideality. The obvious attempt, characterizing the extreme points of the LP relaxation of (6) directly, is impractical: the polytope is cut out by $2^{|\operatorname{supp}(w)|}$ inequalities, and showing that every point with fractional $z$ is a proper convex combination of feasible points means handling all patterns of tight inequalities of (6b) at once. Ideality of the extended formulation (5) is classical and passes to its projection onto $(x,y,z)$, but that only helps once the projection is known to be exactly the LP relaxation of (6): it has to be computed for an arbitrary index set, and every inequality it produces must be shown to be one of (6a), (6b), the bounds, or implied by them. Weights of both signs must be handled throughout: the page treats negative weights by a change of variables, and a formal development has to carry the sign-adjusted bounds $\breve L,\breve U$ through every step.

Formalization scope

Inputs $x\in\mathbb R^\eta$ are Fin η → ℝ, so indices are 0-based; points $(x,y,z)$ are (Fin η → ℝ) × ℝ × ℝ. A formulation is encoded by its LP relaxation $R$ (with $z\in[0,1]$) and the predicate "$(x,y)\in S$ iff $(x,y,z)\in R$ for some $z\in\{0,1\}$"; ideality is ∀ p ∈ Set.extremePoints ℝ R, p.2.2 = 0 ∨ p.2.2 = 1. $M^\pm(f)$ are defined by their closed forms, and a companion theorem proves that they are the maximum and minimum. In (6b) and (7c), "$i\notin I$" ranges over all indices outside $I$, zero weights included. The system (7) is stated with $\breve L,\breve U$, i.e. after undoing the page's substitution $\tilde x_i=-x_i$; for $w\ge 0$ it is the page's display. The LP relaxation of (5) is represented both in its lifted space and projected to $(x,y,z)$, with the copies quantified existentially in the latter, and constant $b$ is scaled by $1-z$ in (5b) and by $z$ in (5c).

The goal carries both standing assumptions of §1.3 ($L_i<U_i$ and strict activity) and nothing else. Milestones that do not need strict activity omit it, which makes them stronger. Example 2 includes the page's $\gamma=0$ boundary: although its box then violates $L_i<U_i$ when $\eta>0$, the example's three stated claims remain true.

Ideality is a statement about the LP relaxation, not about the set with $z\in\{0,1\}$: applied to the latter it would hold trivially, and a goal stating only that (6) is a formulation would omit the result's content. Both are ruled out by the statement of the goal.

A complete development needs: extreme points and convex hulls of polyhedra in product spaces (Mathlib), the hull of a union of two polytopes as a projection, Fourier–Motzkin elimination over an arbitrary finite index set, and finite-sum manipulations over subsets of $\operatorname{supp}(w)$. The Fourier–Motzkin and disjunctive-hull lemmas are reusable well beyond this mission; contributions of either are welcome, as are proofs of the companion results.

Source: the IPCO 2019 extended abstract, arXiv:1811.08359v2 (28 Feb 2019); all labels and pages refer to that version.

Selected references

• R. Anderson, J. Huchette, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, IPCO 2019 (LNCS 11480), extended abstract. arXiv:1811.08359v2
• R. Anderson, J. Huchette, W. Ma, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, Mathematical Programming 183 (2020) 3–39. doi:10.1007/s10107-020-01474-5, arXiv:1811.01988
• J. P. Vielma, G. Nemhauser, Modeling disjunctive constraints with a logarithmic number of binary variables and constraints, Mathematical Programming 128 (2011) 49–72. doi:10.1007/s10107-009-0295-4
• E. Balas, Disjunctive programming and a hierarchy of relaxations for discrete optimization problems, SIAM Journal on Algebraic and Discrete Methods 6(3) (1985) 466–486. doi:10.1137/0606047
• E. Balas, Disjunctive programming: properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998) 3–44. doi:10.1016/S0166-218X(98)00136-X
• J. P. Vielma, Mixed integer linear programming formulation techniques, SIAM Review 57(1) (2015) 3–57. doi:10.1137/130915303

Motivation

Large traders who must unwind a position by a deadline face a trade-off between trading fast, which moves prices against them, and trading slowly, which exposes them to price risk. When many traders liquidate at once, each one's execution price also depends on the aggregate selling rate of the others. Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and a hard liquidation constraint: every position must be zero at the terminal time $T$. Single-player liquidation with this constraint leads to backward equations with singular terminal values (Ankirchner, Jeanblanc and Kruse, SIAM J. Control Optim. 2014; Graewe, Horst and Séré, Stoch. Proc. Appl. 2018). Earlier MFG models of execution (Cardaliaguet and Lehalle, Math. Financ. Econ. 2018; Carmona and Lacker, Ann. Appl. Probab. 2015) allow no liquidation constraint. This mission formalizes the paper's first main result: the constrained game has a unique equilibrium under a weak-interaction condition.

Setting

Fix $T>0$ and a probability space carrying an $m$-dimensional Brownian motion $\widetilde W=(W^0,W)$, where $W^0$ is the one-dimensional common noise, and an initial portfolio $\mathcal X\in L^2$ independent of $\widetilde W$. Let $\mathbb F^0$ be the filtration of $W^0$ and $\mathbb F$ that of $(\mathcal X,W^0,W)$, both augmented by null sets. The cost coefficients are bounded nonnegative $\mathbb F$-progressive processes $\kappa$ (interaction), $\lambda$ (risk aversion) and $\eta$ (temporary impact), with $\lambda,\eta$ bounded away from zero.

A player's trading rate $\xi$ produces the position $X^\xi_t=\mathcal X-\int_0^t\xi_sds$. The admissible strategies are $\mathcal A_{\mathbb F}(\mathcal X)=\{\xi\in L^2_{\mathbb F}:\int_0^T\xi_sds=\mathcal X\}$. Given an $\mathbb F^0$-progressive aggregate rate $\mu$, the cost is

$$J(\mathcal X,\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_sX^\xi_s\mu_s+\eta_s\xi_s^2+\lambda_s(X^\xi_s)^2\big)ds\ \Big|\ \mathcal X\Big],$$

and $V(\mathcal X;\mu)$ is its essential infimum over $\mathcal A_{\mathbb F}(\mathcal X)$. A process $\mu$ solves the MFG (1.7) if some optimal strategy $\xi^*$ given $\mu$ satisfies $\mu_t=\mathbb E[\xi^*_t\mid\mathcal F^0_t]$ for a.e. $t$.

The equilibrium is described by the conditional mean-field FBSDE (2.3):

$$X_t=\mathcal X-\int_0^t\frac{Y_s}{2\eta_s}ds,\quad X_T=0,\quad -dY_t=\Big(\kappa_t\,\mathbb E\Big[\frac{Y_t}{2\eta_t}\Big|\mathcal F^0_t\Big]+2\lambda_tX_t\Big)dt-Z_t\,d\widetilde W_t\ \ \text{on }[0,T).$$

Solutions are sought in weighted spaces: $Y\in\mathcal H_l$ if $\mathbb E\sup_{t\le T}|Y_t/(T-t)^l|^2<\infty$, and $Y\in\mathcal M_l$ if $(T-t)^{-l}|Y_t|$ is essentially bounded. The weak-interaction condition (Assumption 2.3) asks for $\theta>0$ with $\kappa_{\max}/(4\eta_\star)<\theta<4\lambda_\star/\kappa_{\max}$, and $\alpha:=\eta_\star/\|\eta\|\in(0,1]$. The decoupling $Y=AX+B$ uses the solution $A$ of the singular Riccati BSDE $-dA_t=(2\lambda_t-A_t^2/(2\eta_t))dt-Z^A_td\widetilde W_t$, $A_T=+\infty$.

Formalization targets

Goal: Theorem 2.4

Under Assumption 2.3 the FBSDE (2.3) has a unique solution

$$(X,Y,Z)\in\mathcal H_\alpha\times L^2_{\mathbb F}([0,T])\times L^2_{\mathbb F}([0,T-];\mathbb R^m);$$

$\xi^*=Y/(2\eta)$ is optimal, $X$ is the optimal position, $\mu^*_t=\mathbb E[Y_t/(2\eta_t)\mid\mathcal F^0_t]$ is the unique solution of the MFG (1.7), and

$$V(\mathcal X;\mu^*)=\tfrac12A_0\mathcal X^2+\tfrac12B_0\mathcal X+\tfrac12\mathbb E\Big[\int_0^T\kappa_sX^*_s\mu^*_sds\ \Big|\ \mathcal X\Big].$$

Milestones

The milestones follow the paper's proof: Fact 2.2 on the weighted spaces; Lemma A.1, existence and uniqueness of $A$ with the bounds (A.1), and $A\in\mathcal M_{-1}$; the decay estimate (2.9), $\exp(-\int_r^sA_u/(2\eta_u)du)\le((T-s)/(T-r))^\alpha$; Lemma 2.5, an a priori estimate for the decoupled system (2.11) with homotopy parameter $\mathfrak p\in[0,1]$; Lemma 2.6, explicit unique solvability at $\mathfrak p=0$; Lemma 2.7, the continuation step $\mathfrak p\to\mathfrak p+\mathfrak d$; Proposition 2.8, unique solvability of (2.3) with (2.10) and a norm bound; the boundary limit (2.15); and Proposition 2.9, optimality, the equilibrium property and the value formula.

Significance

The theorem gives a complete equilibrium description for constrained liquidation with many players and stochastic, partially common market data: the equilibrium rate is the conditional expectation of the decoupled feedback rate given the common noise, and its value is explicit in terms of the Riccati solution. It is the basis of the paper's other two results, the $O(N^{-1/2})$-Nash property of the equilibrium in the $N$-player game (Theorem 3.3) and the approximation by penalized games (Theorem 4.6), which are separate missions in this series.

The result is proved in the paper; none of it is machine-checked. A formal development would contain the first formal treatment of BSDEs with singular terminal value and of a conditional (common-noise) mean-field FBSDE. Shorter proofs of individual steps, in particular of the a priori estimate and the continuation step, are welcome.

Difficulty

The obvious approach fails at the terminal time. Standard FBSDE theory requires a terminal condition for $Y$; here only $X_T=0$ is known, and $Y_T$ is undetermined. The decoupling coefficient $A$ blows up like $(T-t)^{-1}$, so the driver of the equation for $B$ is singular, and the classical monotonicity method of Hu–Peng and Peng–Wu, applied to $(X,B)$ in unweighted spaces, does not close. The paper works instead with weighted norms that encode the rate at which $X$ and $B$ vanish at $T$, and runs the continuation on the triple $(X,B,Y)$. The mean-field term is a conditional expectation given the common-noise filtration, not an expectation, so it remains random and has to be controlled pathwise in the weighted norms.

Formalization scope

Time is ℝ≥0; processes are real valued and $\widetilde W$ has $m=k+1$ coordinates, coordinate $0$ being $W^0$. The Itô calculus is the published definition Peng1990.SMP.Stochastic (standard Brownian motion, $L^2_{\mathbb F}$, Itô integrals, BSDEs in integrated form). The explicit choices:

• Filtrations are augmented by the measurable null sets, and $\mathbb F$ contains $\sigma(\mathcal X)$.
• $\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $dt\otimes d\mathbb P$. Condition (2.4) is written without division, and "$1/\lambda,1/\eta$ bounded" as positive essential lower bounds.
• Assumption 2.3 is a hypothesis of every statement of §2, as the paper's standing assumption. Lemma A.1 (appendix) assumes only what §A assumes: $\lambda,\eta$ progressive, nonnegative and bounded, and $1/\eta$ bounded.
• Backward equations on $[0,T)$ are imposed on every $[0,\tau]$, $\tau<T$. $A_T=\infty$ means $A_t\to+\infty$ as $t\uparrow T$ a.s.
• Weighted norms are computed in $[0,\infty]$, with the weight $(T-t)^{-l}$ in ℝ≥0∞.
• Every conditional expectation $\mathbb E[\cdot\mid\mathcal F^0_t]$ in an equation is evaluated through a progressive version, and its argument is required to be integrable.
• The value is an essential infimum of conditional costs.
• The relation $Y=AX+B$ is part of the solution concept of (2.11): without it, $Y$ is determined only up to an additive $\mathcal F_0$-measurable constant.
• The constant of Proposition 2.8 is uniform over initial portfolios in an $L^2$ ball, for fixed coefficients.
• Fact 2.2's product rule assumes paths of $K_1$ continuous on $[0,T)$, and its claim that $K_T=0$ for $K\in\mathcal M_l$ is not stated. Both printed versions fail under the essential-supremum norm.

The interaction term must stay conditioned on $\mathcal F^0_t$: conditioning on $\mathcal F_t$ makes it $Y_t/(2\eta_t)$ itself and collapses the game. The constraint $X_T=0$ and the admissibility condition $\int_0^T\xi=\mathcal X$ cannot be dropped either. The degenerate instance $\kappa\equiv0$ satisfies all hypotheses but decouples the game.

A complete development needs the following, all reusable beyond this mission: martingale representation for the augmented filtration $\mathbb F$; existence of progressive versions of conditional expectation processes; Doob's inequality on $[0,\tau]$; and linear BSDE solution formulas.

Selected references

• G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, arXiv:1804.04911v3, 2021; Math. Oper. Res. 46(4), 2021. https://arxiv.org/abs/1804.04911
• S. Ankirchner, M. Jeanblanc, T. Kruse, BSDEs with singular terminal condition and a control problem with constraints, SIAM J. Control Optim. 52(2), 2014. https://doi.org/10.1137/130913411
• P. Graewe, U. Horst, E. Séré, Smooth solutions to portfolio liquidation problems under price-sensitive market impact, Stoch. Proc. Appl. 128(3), 2018. https://doi.org/10.1016/j.spa.2017.07.002
• P. Cardaliaguet, C.-A. Lehalle, Mean field game of controls and an application to trade crowding, Math. Financ. Econ. 12, 2018. https://doi.org/10.1007/s11579-017-0206-z
• R. Carmona, D. Lacker, A probabilistic weak formulation of mean field games and applications, Ann. Appl. Probab. 25(3), 2015. https://doi.org/10.1214/14-AAP1020
• Y. Hu, S. Peng, Solution of forward-backward stochastic differential equations, Probab. Theory Related Fields 103, 1995. https://doi.org/10.1007/BF01204214

Motivation

A trader who must sell a large position within a fixed horizon faces a trade-off: selling fast moves the price against her (temporary price impact), selling slowly exposes her to price risk. Since Almgren and Chriss, this optimal liquidation problem has been studied as a stochastic control problem with a terminal state constraint: the remaining position must be zero at the horizon $T$. When many traders liquidate at the same time, each trader's sales also depress the price that the others receive (permanent price impact), and the problem becomes a game.

Fu, Graewe, Horst and Popier (arXiv:1804.04911v3) study this game in the mean-field limit. Their §2 constructs a mean-field equilibrium through a singular conditional mean-field FBSDE. Their §3, the subject of this mission, justifies the limit: the strategies computed from the mean field game are an approximate Nash equilibrium of the finite game with $N$ traders, with an error of order $1/\sqrt N$. Without such a result, the mean-field equilibrium describes a model nobody plays; with it, the equilibrium is a usable approximation for large but finite markets.

The approximation of $N$-player games by mean field games goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007); Carmona and Delarue (SIAM J. Control Optim. 51, 2013) proved an $\varepsilon_N$-Nash property for a McKean–Vlasov class with state interaction and a rate $N^{-1/(d+4)}$. The present game differs in three respects: players interact through their controls (the average trading rate), there is a common noise observed by all, and each player's state must reach zero at time $T$.

Setting

A single probability space carries a one-dimensional Brownian motion $W^0$ (the common noise, which drives the benchmark price and is observed by every player), for each player $i$ a $k$-dimensional Brownian motion $W^i$ (the private noise), and i.i.d. initial portfolios $\mathcal X^i$ with law $\nu$; all of these are mutually independent. Player $i$ observes $\mathbb F^i$, $\mathcal F^i_t=\sigma(\mathcal X^i,W^0_s,W^i_s,\ s\le t)$, and chooses a trading rate $\xi^i$; her position is $X^i_t=\mathcal X^i-\int_0^t\xi^i_s\,ds$ and must satisfy $X^i_T=0$. Given the profile $\vec\xi=(\xi^1,\dots,\xi^N)$, her conditional cost is

$$J^{N,i}(\vec\xi)=\mathbb E\Big[\int_0^T\Big(\frac{\kappa^i_t}{N}\sum_{j=1}^N\xi^j_tX^i_t+\eta^i_t(\xi^i_t)^2+\lambda^i_t(X^i_t)^2\Big)dt\ \Big|\ \mathcal X^i\Big],$$

where $\kappa^i$ (permanent impact), $\eta^i$ (temporary impact) and $\lambda^i$ (risk aversion) are nonnegative bounded processes. Under Assumption 3.1 they are the same deterministic measurable functionals $\kappa,\eta,\lambda$ of $(t,\mathcal X^i,W^i_{\cdot\wedge t},W^0_{\cdot\wedge t})$ for every player, so the players are statistically identical.

In the mean field game, the average $\frac1N\sum_j\xi^j$ is replaced by a process $\mu$ adapted to the common-noise filtration $\mathbb F^0$, and an equilibrium is a $\mu^*$ with $\mu^*_t=\mathbb E[\xi^*_t\mid\mathcal F^0_t]$ for the representative player's best response $\xi^*$. The paper characterizes it through the FBSDE (2.3),

$$dX_t=-\frac{Y_t}{2\eta_t}dt,\qquad -dY_t=\Big(\kappa_t\,\mathbb E\Big[\frac{Y_t}{2\eta_t}\Big|\mathcal F^0_t\Big]+2\lambda_tX_t\Big)dt-Z_t\,d\widetilde W_t,\qquad X_0=\mathcal X,\ X_T=0,$$

with $\widetilde W=(W^0,W)$; the optimal rate is $\xi^*=Y/(2\eta)$. Player $i$'s mean-field strategy $\xi^{*,i}=Y^i/(2\eta^i)$ comes from the same FBSDE with her own data.

Formalization targets

Goal: Theorem 3.3

For a positive function $M$ with $\psi\le M$, where $\psi(\mathcal X^i)=\mathbb E[\int_0^T|\xi^{*,i}_t|^2dt\mid\mathcal X^i]$, and admissible sets $\mathcal A^i=\{\xi\in\mathcal A_{\mathbb F^i}(\mathcal X^i):\mathbb E[\int_0^T|\xi_t|^2dt\mid\mathcal X^i]\le M(\mathcal X^i)\}$, there is a function $g$, independent of $i$ and $N$, with

$$J^{N,i}(\vec\xi^*)\le J^{N,i}(\xi^i,\xi^{*,-i})+\frac{g(\mathcal X^i)}{\sqrt N}\qquad\text{for all }N\ge1,\ 1\le i\le N,\ \xi^i\in\mathcal A^i .$$

The goal asserts only the shape of the bound, not its constant.

Milestones

1. Lemma 3.2: one measurable map $\Phi$ gives $(X^i,Y^i,\int_0^\cdot Z^i)=\Phi(\mathcal X^i,W^i,W^0)$ for every player, and $\xi^{*,i}=\phi(\mathcal X^i,W^0,W^i)$ (3.1).
2. (3.2): a single $\mu^*$ with $\mu^*_t=\mathbb E[\xi^{*,i}_t\mid\mathcal F^0_t]$ for every $i$.
3. (3.3): $\mathbb E\int_0^T|\xi^{*,i}_t|^2dt\le C$ uniformly in $i$.
4. (3.5): $\mathbb E[\int_0^T(\mu^*_t-\frac1N\sum_j\xi^{*,j}_t)^2dt\mid\mathcal X^i]\le 2(M(\mathcal X^i)+(2N-1)C)/N^2$.
5. The bounds on $I_1$ and $I_2$ (p. 24): the two differences of conditional costs into which the proof splits $J^{N,i}(\xi,\xi^{*,-i})-J^{N,i}(\vec\xi^*)$ are $O(1/\sqrt N)$.

Significance

The result turns the mean-field equilibrium of §2 into a statement about the finite market: when all $N$ traders use their mean-field strategies, a trader who deviates can save at most $g(\mathcal X^i)/\sqrt N$ in conditional expected cost. The error bound depends on the trader's own initial position only through $M(\mathcal X^i)$, and the rate $1/\sqrt N$ is dimension-free, in contrast with the $N^{-1/(d+4)}$ rates of state-interaction games, because the interaction runs through the empirical mean of the controls rather than through an empirical measure.

The paper's proof of Theorem 3.3 is short but rests on several facts it states without proof: the Yamada–Watanabe-type Lemma 3.2 (whose proof is referred to other papers), the identification (3.2) of a common conditional mean, and the moment bound (3.3) attributed to Proposition 2.8. This mission makes each of these a separate machine-checkable statement. As far as we know, none of these results, nor any optimal-liquidation mean field game, has a machine-checked proof.

Difficulty

The estimate (3.5) is a law-of-large-numbers bound for the average of $N$ processes that are not independent: all of them depend on the common noise $W^0$. The obvious argument, expanding the square and using independence, fails as stated; the cross terms vanish only conditionally on $W^0$, and only once one knows that every $\xi^{*,j}$ is the same measurable functional of $(\mathcal X^j,W^0,W^j)$. That is Lemma 3.2, a Yamada–Watanabe-type statement for a singular FBSDE with a conditional mean-field term, which needs strong uniqueness of the FBSDE in the class $\mathcal H_\alpha\times L^2\times L^2([0,T-])$ and is the main technical step. The terminal constraint $X_T=0$ makes the backward component singular at $T$ ($Y$ blows up like $X/(T-t)$), so standard Lipschitz FBSDE theory does not apply. Finally, the deviation $\xi$ is constrained only through a conditional second-moment bound $M$, and the comparison with the mean-field cost uses the optimality of $\xi^{*,i}$ (Proposition 2.9) against $\mu^*$.

Formalization scope

Everything is stated on one probability space carrying all players, with players indexed by $\mathbb N$; the $N$-player game uses players $i<N$ (the paper's $1,\dots,N$, shifted by one). Time is $\mathbb R_{\ge0}$ and the processes are real valued. Choices made explicit:

• Assumption 2.3 for every player is a hypothesis of every theorem: the paper states it "throughout" (p. 8), and the proof of Theorem 3.3 uses Propositions 2.8 and 2.9, which need it. Its constants $\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $[0,T]\times\Omega$; "$1/\lambda,1/\eta\in L^\infty$" is a positive essential lower bound.
• The equilibrium processes $(X^i,Y^i,Z^i)$ are hypotheses: solutions of (2.3) for player $i$'s data in the class of Theorem 2.4. $\xi^{*,i}$ is defined as $Y^i/(2\eta^i)$, never through $\phi$.
• Conditioning on $\mathcal X^i=x^i$ is conditioning on $\sigma(\mathcal X^i)$; every conclusion holds almost surely, i.e. for $\nu$-a.e. $x^i$. "$\psi\le M$" is the a.s. inequality of conditional second moments, and $M$ is assumed measurable.
• $g$ is quantified before $N$ and $i$. A statement in which $g$ may depend on $N$ is trivially true and is ruled out.
• Filtrations are augmented by null sets. Each conditional expectation $\mathbb E[\,\cdot\mid\mathcal F^0_t]$ is evaluated through a progressive version of an integrable argument. BSDEs on $[0,T)$ are imposed on every $[0,\tau]$, $\tau<T$.
• Lemma 3.2's path spaces carry the product σ-algebra; its identities hold for each $t$ almost surely.
• The paper's bound on $I_2$ is stated for $|I_2|$, which is what its Cauchy–Schwarz step gives and what the proof needs.

The development reuses the Itô-calculus definitions of Peng1990.SMP.Stochastic (standard Brownian motion, $L^2_{\mathbb F}$, Itô integrals, BSDEs). Contributions useful beyond this mission: conditional independence given a common noise for functionals of independent inputs, a Yamada–Watanabe argument for FBSDEs, and conditional Cauchy–Schwarz bounds for time integrals. Proofs of any milestone, and of the facts from §2 they rely on, are welcome.

Selected references

• G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, arXiv:1804.04911v3, 2021; Math. Oper. Res. 46(4), 2021. https://arxiv.org/abs/1804.04911
• R. Almgren, N. Chriss, Optimal execution of portfolio transactions, J. Risk 3(2), 2001. https://doi.org/10.21314/JOR.2001.041
• M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6(3), 2006. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• J.-M. Lasry, P.-L. Lions, Mean field games, Jpn. J. Math. 2, 2007. https://doi.org/10.1007/s11537-007-0657-8
• R. Carmona, F. Delarue, Probabilistic analysis of mean-field games, SIAM J. Control Optim. 51(4), 2013. https://doi.org/10.1137/120883499
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

Motivation

Brands are routinely held responsible for the labour and environmental practices of their suppliers. A brand that is linked in public to a non-compliant supplier loses consumer willingness to pay, and firms answer this risk by auditing their suppliers. Supply networks are not trees, however: one supplier often serves several competing brands. Chen, Qi and Dawande (SSRN 2889889, Manufacturing & Service Operations Management, 2020) ask how the position of a supplier in such a network, and in particular its centrality (the number of buyers it serves), affects which suppliers get audited when buyers decide on their own, and when they audit jointly.

This mission formalizes the paper's answer for unilateral auditing by competing buyers (Sec. 4.2, Proposition 2). A companion mission treats joint auditing (Proposition 3).

Setting

Two buyers $B_1, B_2$ source from three suppliers: an independent supplier $S_i$ for each buyer $B_i$, and a common supplier $S_c$ that serves both. Each supplier complies with social-responsibility standards with probability $e \in (0,1)$. In stage 1, buyer $B_i$ chooses an auditing effort $e_{ii} \in [0,1]$ on $S_i$ and $e_{ic} \in [0,1]$ on $S_c$, and audits at most one of them: $e_{ii}\,e_{ic} = 0$. Auditing a supplier with effort $x > 0$ costs $K + \tfrac a2 x^2$, with a fixed cost $K \ge 0$ and $a > 0$; effort $0$ means no audit and costs nothing.

A non-compliant supplier that passes the audits is discovered in public with probability $r \in (0,1]$. Hence $S_i$ causes damage to $B_i$ with probability $\lambda_I(e_{ii}) = r(1-e)(1-e_{ii})$, and $S_c$ causes damage to both buyers with probability $\lambda_C(e_{1c},e_{2c}) = r(1-e)(1-e_{1c})(1-e_{2c})$, independently. A buyer with at least one exposed supplier suffers the MWTP damage $d_M > 0$: his demand intercept drops from $\alpha$ to $\alpha - d_M$. Each exposed supplier is then paid $\hat w \ge w$ per unit instead of $w$, so a buyer with $n \in \{0,1,2\}$ exposed suppliers has unit cost $(2-n)w + n\hat w$.

In stage 2 the buyers compete in quantities with inverse demands $p_i = A_i - q_i - \beta q_{i'}$, $\beta \in (0,1]$ (Dixit 1979; Singh and Vives 1984). Its equilibrium profit for $B_1$ is $\pi^b_1(n_1,n_2) = q^*_1(n_1,n_2)^2$, in closed form (Lemma 1). Buyer $B_1$'s ex ante expected profit $\Pi^b_1(e_{11},e_{1c};e_{22},e_{2c})$ is the expectation of $\pi^b_1$ over the eight damage outcomes, minus his audit costs; $\Pi^b_2$ is symmetric. Three conditions on $(\alpha,\beta,w,\hat w,d_M)$ (p. 8) make all stage-2 quantities positive.

An equilibrium is a profile $(s_1,s_2)$, $s_i = (e_{ii},e_{ic})$, in which each buyer's strategy is a best response to the other's, with the tie-breaking rule of p. 10: a buyer who is indifferent between auditing and not auditing does not audit. Two explicit efforts, $e^*_I$ (eq. (1)) and $\hat e_I$ (eq. (2)), are rational functions of the parameters; $\hat e_I$ is a buyer's optimal effort on his independent supplier when the rival audits nobody, and $e^*_I$ is the symmetric solution when both audit their independent suppliers.

Formalization targets

Goal: Proposition 2

Assume $\beta \in (0,1]$ and $\hat e_I < 1$. There exist $K^L_u < K^M_u < K^H_u$ such that for every $K \ge 0$, writing $A = ((e^*_I,0),(e^*_I,0))$, $B_1 = ((\hat e_I,0),(0,0))$, $B_2 = ((0,0),(\hat e_I,0))$, $N = ((0,0),(0,0))$,

$$\mathrm{EqSet}(K) = \begin{cases} \{A\} & K < K^L_u,\\ \{A, B_1, B_2\} & K^L_u \le K < K^M_u,\\ \{B_1, B_2\} & K^M_u \le K < K^H_u,\\ \{N\} & K \ge K^H_u. \end{cases}$$

In every equilibrium the common supplier receives zero effort.

Milestones

Lemma 1 (stage-2 equilibrium), the OA.2 expected-profit display, the best-response function (OA-9) with $e^*_I$ and $\hat e_I$ as its values, the dominance inequality (OA-11), Lemmas OA5 and OA6 (the two kinds of auditing equilibria and their threshold ranges), the monotonicity facts (OA-14)–(OA-15), Lemma OA7 (the order of the thresholds) and Lemma OA8 (no equilibrium audits $S_c$). The thresholds of the milestones are the explicit ones the proof defines in (OA-10), (OA-12), (OA-13).

Significance

The result separates network position from competition. Without downstream competition ($\beta = 0$, Proposition 1) there is a Pareto-dominant equilibrium in which one buyer audits the common supplier. With competition, Proposition 2 shows that the common supplier, the most central and therefore the most consequential source of risk, is never audited: auditing it would also protect the rival, who free-rides. This inefficiency is what motivates the paper's analysis of joint auditing (Proposition 3) and of social welfare (Proposition 4).

The result is proved in the paper, partly by omission: the e-companion leaves the proof of Lemma OA8 and the case $K \ge K^H_u$ to the reader. No machine-checked version exists. A formal proof would give a complete case analysis of a two-stage game with a discontinuous fixed cost, a constrained strategy set and a tie-breaking rule, and would check the paper's closed forms, several of which are printed with small slips.

Difficulty

The first-order conditions alone do not determine the equilibria. The fixed cost makes each buyer's payoff discontinuous at zero effort, so every candidate must be compared with no audit, and the best response is a choice among three regimes (audit $S_i$, audit $S_c$, audit nobody). Uniqueness claims therefore require excluding every profile in the constrained strategy set, including those where a buyer audits the common supplier, for which the paper gives no proof. The threshold comparisons $K^L_u < K^M_u < K^H_u$ rest on monotonicity in the rival's effort, and the expected profit is multilinear in the four efforts (plus the quadratic audit costs), with coefficients that are differences of squared Cournot quantities whose signs depend on the p. 8 conditions.

Formalization scope

All objects live in the namespace SupplierAudit.Competition. The source is the authors' accepted manuscript on SSRN (2889889); main-text printed pages equal PDF pages, and e-companion page ec $k$ is PDF page $28 + k$.

• Parameters. A structure Params carries $\alpha, \beta, w, \hat w, d_M, e, r, a$ and the standing assumptions $\beta \in [0,1]$, $w \le \hat w$, $d_M > 0$, $e \in (0,1)$, $r \in (0,1]$, $a > 0$ and the three conditions of p. 8. The theorems add $\beta > 0$ (competition, Sec. 4.2). $K$ is a separate real argument and the goal quantifies over $K \ge 0$.
• Stage 2. The general linear differentiated Cournot duopoly is its own definition (CournotDuopoly). The model's stage-2 profit is the closed form $q^*_1(n_1,n_2)^2$ for all $(n_1,n_2)$; Lemma 1 states that it is the game's unique equilibrium.
• Expected profit. $\Pi^b_1$ is the eight-outcome expectation; $\Pi^b_2$ is $\Pi^b_1$ with the roles exchanged. The grouped display of OA.2 is a milestone.
• Strategies and equilibrium. Strategies are pairs in $[0,1]^2$ with product zero. Equilibria include the strict-improvement tie-breaking rule of p. 10; without it the goal is false at $K = K^M_u$ and $K = K^H_u$.
• Interior efforts. The paper assumes equilibrium efforts lie in $(0,1)$ (p. 10; sufficient conditions in OA.1 are not given in closed form). This is encoded as the single hypothesis $\hat e_I < 1$ on the explicit formula (2), never as a hypothesis on an unknown equilibrium variable.
• Thresholds. The goal states the thresholds existentially, as printed, with their order as part of the conclusion; the milestones use the explicit (OA-10), (OA-12), (OA-13). $e^*_I$, $\hat e_I$ and $e^*_{11}(\cdot)$ are the printed formulas, not argmaxes.
• Printed slips, corrected. In (OA-11) the second prefactor should be $\beta(\hat w - w)$; only the strict inequality is stated. The printed derivative of $e^*_{11}$ in the proof of Lemma OA7 lacks a factor $1/a$; only monotonicity is stated.

A formalization in which equilibrium is plain Nash, efforts range over all of $\mathbb R$, a buyer may audit both suppliers, or "interior" is a hypothesis on the equilibrium efforts themselves would state a different (and in places false or vacuous) theorem; these are ruled out by the definitions above. Proofs of any milestone are welcome, as is reusable infrastructure for linear Cournot duopolies and for finite expectations over independent Bernoulli events.

Selected references

• F. Chen, A. Qi, M. Dawande, Supplier Centrality and Auditing Priority in Socially-Responsible Supply Chains, Manufacturing & Service Operations Management, 2020 (accepted manuscript). https://ssrn.com/abstract=2889889
• A. Dixit, A Model of Duopoly Suggesting a Theory of Entry Barriers, Bell Journal of Economics 10(1), 1979. https://doi.org/10.2307/3003317
• N. Singh, X. Vives, Price and Quantity Competition in a Differentiated Duopoly, RAND Journal of Economics 15(4), 1984. https://doi.org/10.2307/2555525
• E. L. Plambeck, T. A. Taylor, Supplier Evasion of a Buyer's Audit: Implications for Motivating Supplier Social and Environmental Responsibility, Manufacturing & Service Operations Management 18(2), 2016. https://doi.org/10.1287/msom.2015.0550