All missions

Motivation

Firms are run by managers who know more about cash flows than investors do. In the dynamic agency literature that started with DeMarzo and Fishman (2007) and DeMarzo and Sannikov (2006), a manager can divert cash by under-reporting output, and investors deter diversion with a contract that promises future pay after good reports and threatens liquidation after bad ones. Liquidation destroys value, so the threat itself is costly; the gap between the firm's value under the optimal contract and its first-best value is an agency cost, and in this class of models it is also the firm's credit spread.

Fu and Trigilia ask what happens when the manager can, from time to time, produce hard evidence that a low cash flow was bad luck rather than diversion. Disclosure is voluntary: evidence can be hidden, so the contract must reward disclosing it. The question is whether better information technology, a higher probability of evidence, makes the firm more valuable and less likely to default. The paper's answer (Proposition 4(a)) is used by the rest of the paper: by the analysis of when to invest in the technology (§7) and by the claims about default risk at initiation.

Setting

A firm produces i.i.d. cash flows $x_t \in \{h, l\}$ with $h > l > 0$ and $P(x_t = h) = p \in (0,1)$. Investors and the manager are risk neutral and discount at rate $r \in (0,1)$. Reporting a high cash flow as low lets the manager divert $\Delta = h - l$, of which the manager keeps the private benefit $\delta = \lambda\Delta$ with $\lambda \in (0,1]$. Write $\mu = ph + (1-p)l$. Each period, with probability $\pi \in [0,1)$, the manager also receives evidence of the true cash flow, which he may disclose or hide; $\pi = 0$ is the classical model without evidence.

The contract is written recursively in the manager's promised utility $v \ge 0$. At state $v$ it chooses a liquidation probability $\theta \in [0,1]$, cash payments $u_{ah} \ge 0$, $u_{al} \ge 0$ and continuation utilities $w_{ah}, w_{al} \ge 0$, indexed by $a \in \{d, n\}$ (evidence disclosed or not) and by the reported cash flow. Writing $U_{ai} = u_{ai} + w_{ai}/(1+r)$, it must satisfy

$$U_{dh} \ge U_{nh}\ (IC_g),\qquad U_{dl} \ge U_{nl}\ (IC_b),\qquad U_{nh} \ge \delta + U_{nl}\ (IC_n),$$ $$v = (1-\theta)\big[\pi(pU_{dh} + (1-p)U_{dl}) + (1-\pi)(pU_{nh} + (1-p)U_{nl})\big]\ (PK).$$

The firm value $s(v)$ (total surplus) is the fixed point of the Bellman operator

$$Tq(v) = \sup\ (1-\theta)\mu + \frac{1-\theta}{1+r}\Big\{\pi[pq(w_{dh}) + (1-p)q(w_{dl})] + (1-\pi)[pq(w_{nh}) + (1-p)q(w_{nl})]\Big\}$$

over feasible policies, in the class $\mathcal F$ of continuous functions on $\mathbb R_+$ with $0 \le q \le s^*$, where $s^* = (1+r)\mu/r$ is the first-best value. The credit spread is $1 - s(v)/s^*$. Two thresholds organise the solution: the cash payout boundary $\bar v = (1+r)p\delta/r$, above which $s = s^*$, and the first termination threshold $v^1(\pi) = \hat r\bar v/(1+\hat r)$ with $\hat r = r/(1-(1-p)\pi)$, below which the optimal contract liquidates with positive probability.

Formalization targets

Goal: Proposition 4(a), corrected

For $0 \le \pi < \pi' < 1$, with $s$, $s'$ the firm values for $\pi$ and $\pi'$, a firm value exists for each evidence probability and

$$s(v) \le s'(v)\quad \text{and}\quad 1 - \tfrac{s'(v)}{s^*} \le 1 - \tfrac{s(v)}{s^*}\qquad (v \ge 0),$$ $$s(v) < s'(v)\quad \text{and}\quad 1 - \tfrac{s'(v)}{s^*} < 1 - \tfrac{s(v)}{s^*}\qquad (v^1(\pi) < v < \bar v).$$

The paper states the strict inequality for every $v < \bar v$. That is false below $v^1(\pi)$ when $p \le r$: there firm value is linear through the origin with slope $s(v^1)/v^1 = (1+r)(r+p)\mu/(r^2\bar v)$, which does not depend on $\pi$, so $s(\cdot\,;\pi)$ and $s(\cdot\,;\pi')$ coincide on $[0, v^1(\pi)]$. The goal is the corrected statement: weak everywhere, strict above the first termination threshold of the smaller evidence probability.

Milestones, in attack order

1. Lemma A.1 (p. 38): $T$ maps the functions in $\mathcal F$ equal to $s^*$ on $[\bar v, \infty)$ into themselves.
2. Proposition A.1 (p. 38): the fixed point exists, is unique, nondecreasing, concave and equal to $s^*$ on $[\bar v, \infty)$.
3. Proposition 2 (p. 16): $\inf\{v : s(v) = s^*\} = \bar v$.
4. Lemma 1 (p. 18): for $0 < v < \bar v$, every optimal policy has $(IC_g)$, $(IC_n)$ binding and $(IC_b)$ strict.
5. Proposition 3, bullets 1–2 (p. 19): explicit optimal $\theta$, $w_{nl}$, $w_{dl}$, $w_h$ on $(0, v^1]$ and $(v^1, \bar v]$.
6. Linearity below $v^1$ (p. 19): $s(v) = (v/v^1)s(v^1)$ on $[0, v^1]$.

Significance

The result says that the value of a firm run under moral hazard, and its default risk, respond monotonically to the quality of information about cash flows, even though the information is controlled by the party whose incentives are the problem. It underlies the paper's analysis of when investors should pay for the information technology and how the credit spread varies with it. The correction also identifies precisely where better evidence is worthless: in the liquidation region below $v^1$ when $p \le r$, where the firm reaches the payout boundary after a single high cash flow.

These results are proved in the paper (with the gap noted above) and none has a machine-checked proof. A complete formalization gives a verified treatment of a discrete-time dynamic contracting problem: the Bellman operator of a constrained recursive contract, the shape of its fixed point, the binding incentive constraints and the closed-form optimal contract.

Difficulty

The value function is defined only implicitly, as the fixed point of an operator whose feasible set is not convex in the obvious variables: promise keeping multiplies the liquidation probability by the promised utility. Comparing two fixed points for different $\pi$ requires knowing their shape, which in turn requires the explicit optimal policy. The paper's comparative-statics argument differentiates in $\pi$ through an envelope condition at points where $s$ has kinks, and treats the region below $v^1$ by continuity; but $v^1$ itself moves with $\pi$, so the argument does not transfer from above $v^1$ to below it, and the strict claim fails there for $p \le r$. Any proof must handle the moving threshold explicitly.

Formalization scope

All objects are in the namespace VolDisclosure.Evidence. Parameters are a structure with fields $h, l, p, r$ and lam ($\lambda$), with the standing assumptions $0 < l < h$, $0 < p < 1$, $0 < r < 1$, $0 < \lambda \le 1$. A policy is nine real numbers ($\theta$, four cash payments, four continuation utilities). The conventions are:

• the "max" of (T) is the supremum over all feasible policies; attainment is part of Proposition 3, not of the definition;
• $\pi$ is a parameter of (T), not a choice variable (p. 37 lists it under the max by mistake);
• continuation utilities are nonnegative (p. 10, "$w_t \ge 0$"); (LL) covers the cash payments;
• membership in $\mathcal F$ and the fixed-point equation are required on $\mathbb R_+$ only;
• $\pi$ ranges over $[0,1)$, including the no-evidence benchmark $\pi = 0$; Lemma 1 additionally needs $0 < v$ and $0 < \pi$, both disclosed in its statement;
• "increasing" in Proposition A.1 means nondecreasing.

The firm value must be the fixed point of (T) over all feasible policies. Defining it from Proposition 3's policy, or dropping $(IC_n)$ (under which $s \equiv s^*$), would make the goal trivial; the goal also asserts existence of a firm value, so it cannot hold vacuously.

Not formalized: Proposition 2's cash formula (5) and the half of definition (3) that involves the investment-option problem (F); Proposition 3's third bullet ($n$-period thresholds); Proposition 4(b)–(d), of which (c) and (d) are misprinted; the two-period model, the investment option (§7) and the default-risk results at initiation (Proposition 7).

A complete development needs a contraction fixed-point argument on bounded continuous functions on $\mathbb R_+$, the shape results for the fixed point, and the explicit policy; contributions of any milestone are welcome, and the fixed-point layer is reusable for other recursive contracting models.

Selected references

• S. Fu and G. Trigilia, Voluntary Disclosure, Moral Hazard and Default Risk, working paper, August 28, 2019; published in Management Science, 2024. https://doi.org/10.1287/mnsc.2023.4860
• P. M. DeMarzo and M. J. Fishman, Optimal Long-Term Financial Contracting, Review of Financial Studies 20(6), 2007. https://doi.org/10.1093/rfs/hhm031
• P. M. DeMarzo and Y. Sannikov, Optimal Security Design and Dynamic Capital Structure in a Continuous-Time Agency Model, Journal of Finance 61(6), 2006. https://doi.org/10.1111/j.1540-6261.2006.01049.x

Motivation

Supply-chain traceability depends on firms adopting a technology together. A firm may benefit only after enough other firms in a shared supply chain have adopted; a supply chain may in turn become traceable only when a threshold number of its firms participate. Selecting firms to seed therefore couples many local adoption decisions. Blaettchen, Calmon, and Hall model this coupling as a network diffusion problem and ask for a least-cost seed set that eventually activates every firm Blaettchen, Calmon, and Hall, 2024. Their model permits overlapping supply chains and firm-specific benefits and costs, so it describes more than a single threshold rule on an ordinary graph.

The paper establishes an exact linear programming reformulation whose size depends exponentially on treewidth but only linearly on the numbers of firms and supply chains, up to parameter factors Theorem 2. This mission records that mathematical claim as a cost-independent extended formulation, together with source propositions describing the diffusion correspondence and the first binary formulation.

Setting

Let $N_F$ contain $n$ firms and let $N_{SC}$ contain $m$ supply chains. Supply chain $j$ comprises the hyperedge $e_j\subseteq N_F$. Firm $i$ has an adoption cost $c_i>0$ and receives a nonnegative integral benefit $r_{ji}$ from an incident supply chain $j$ once enough of that chain's firms are active. The chain's threshold satisfies $2\le\theta_j\le|e_j|$. The paper assumes that each firm's total incident benefit can cover its adoption cost. A seed set $S_0$ is active at time zero; every later set $S_t$ retains the already active firms and adds a firm $i$ when

$$c_i\le\sum_{j:\ i\in e_j,\ |S_t\cap e_j|\ge\theta_j-1}r_{ji}.$$

A seed set fully activates the network if $S_t=N_F$ at some finite time. Given real seeding costs $w_i$, the optimization value is

$$\operatorname{OPT}(w)=\min\left\{\sum_{i\in S}w_i:S\subseteq N_F\text{ fully activates the network}\right\}.\tag{1}$$

The auxiliary graph $G'$ has a firm vertex for each $i$ and a supply-chain vertex for each $j$, joined when $i\in e_j$. Its directed weighted version sends weight $1$ from a firm to a supply-chain vertex and weight $r_{ji}$ in the reverse direction. Firm thresholds are $c_i$; supply-chain thresholds are $\theta_j-1$. A weighted linear-threshold update activates vertices whose total incoming weight from active vertices reaches their threshold. Proposition 1 identifies the firms active after $t$ original steps with those active after $2t$ auxiliary-graph steps Proposition 1, p. 10.

A tree decomposition is a tree of vertex bags that covers every vertex, places each graph edge or hyperedge in a bag, and keeps the bags containing one vertex connected along the tree. Its width is the largest bag size minus one. Write $\omega$ for an upper bound on the treewidth of the original hypergraph and $\vartheta_{\max}=\max(\max_i c_i,\max_j(\theta_j-1))$ Definition 2, p. 13; Proposition 9, p. 18.

Formalization targets

Exact LP reformulation

The target is one finite linear system $Az\ge b$, where $z=(x,y)$ has visible seed coordinates $x\in\mathbb R^n$ and auxiliary coordinates $y$. The system is chosen from the adoption instance and is independent of $w$. Its projection onto $x$ is exactly the convex hull of fully activating seed indicators:

$$\operatorname{proj}_x\{(x,y):Az\ge b\}=\operatorname{conv}\{\mathbf1_S:S\text{ fully activates}\}.$$

Consequently, minimizing $\sum_iw_ix_i$ over the same LP yields $\operatorname{OPT}(w)$ for every real $w$. One absolute constant $C>0$, placed before all instances and treewidth parameters, bounds the total number of variables and constraints by

$$2^{C(\omega+1)^2}(\vartheta_{\max}+1)^{C(\omega+1)}C(n+m+1).$$

This is the $2^{O(\omega^2)}\vartheta_{\max}^{O(\omega)}O(n+m)$ form stated immediately after Theorem 2 p. 18. The source's more detailed displayed bracket is not used as the target because its fixed exponents do not match the asymptotic bound obtained from the propositions cited in the proof.

Supporting results

The milestones follow the proof of Theorem 2 on p. 41. Proposition 1 and Corollary 1 identify the adoption process with a weighted threshold process on $G'$. Proposition 5 gives a binary program (4) whose feasible seed vectors are exactly the fully activating seed sets. Proposition 7 replaces its global acyclicity constraints by constraints inside the bags of a tree decomposition of $G'$, formulation (5). Proposition 8 splits the long covering constraints of (5) into partial sums along a rooted binary decomposition, formulation (10). Proposition 9 bounds the treewidth of the intersection graph of (10) by $O(\omega'^2+\omega'\log_2\vartheta_{\max})$, where $\omega'$ is the width of the decomposition of $G'$. Proposition 3 gives $\operatorname{tw}(G')\le\operatorname{tw}(G)+1$, and Proposition 4 is the bounded-treewidth LP theorem for binary programs pp. 10–18.

Significance

An exact LP gives the same optimum for every seeding-cost vector while keeping the constraints fixed. The size guarantee explains why a structurally sparse supply-chain network can admit a formulation far smaller than a generic enumeration of seed sets. It also separates the economics of choosing $w$ from the combinatorics of diffusion: once the network formulation is built, different cost scenarios use the same feasible region Theorem 2 and §5.3.

The paper proves the theorem, citing Proposition 4 from Laurent (2009) and Bienstock and Muñoz (2018). Neither Theorem 2 nor Proposition 4 has a machine-checked proof on Prove2Me. The remaining work is to formalize the paper's chain of reformulations and the cited LP theorem. The tree decomposition definitions are already published as reusable Prove2Me objects from Robertson and Seymour. The diffusion model, the binary formulation, and their relationship to an LP extended formulation are the new formal objects here.

Difficulty

The first binary program represents the activation order but connects variables across many firm–supply-chain pairs. Its intersection graph has treewidth at least $nm-1$, even when the underlying supply-chain graph is sparse Proposition 6, p. 16. Applying a bounded-treewidth LP theorem directly to that program therefore loses the desired parameter bound. The source introduces a more local formulation tied to a tree decomposition, and controlling the intersection graph of that formulation is the central difficulty. Formulation (10) as printed is not exactly right: the bit count (6) is one bit short, so that an instance with $c_1=2$ loses its optimal seed set, and the root inequalities (10c), (10g) use an undeclared variable. The targets use the bit ranges of the integer program (11) in the proof of Proposition 8 and the partial sum $u$ at each subtree root.

Formalization scope

The Lean instance uses Fin n for firms, Fin m for supply chains, and natural numbers for benefits, adoption costs, and thresholds. The auxiliary graph is a simple graph on the disjoint union of these two finite types; the diffusion update retains active vertices and uses the paper's weak inequality at the threshold. Hypergraph treewidth requires every entire hyperedge in some bag and uses the published Robertson–Seymour tree decomposition predicate for the primal graph. Graph treewidth for $G'$ uses the corresponding published bound predicate.

The paper treats connectedness as without loss of generality. Here it means that the incidence graph $G'$ is connected and is included with the other standing assumptions. The gcd normalization discussed in §3.1 is a preprocessing convention, not a hypothesis. The finite family of successful seed sets always contains the all-firm set, so OPT is a genuine finite minimum. The formulation counts both auxiliary variables and inequalities. The additive shifts in the size bound handle small values of $n$, $m$, $\omega$, and $\vartheta_{\max}$; they do not change the asymptotic claim. The LP is quantified before $w$, and its projection is specified, excluding a trivial LP selected separately for each cost vector.

Formulations (4), (5) and (10) are binary feasibility predicates over natural-number variables bounded by one; the adoption inequality $c_i(1-s_i)\le\cdots$ is written as $c_i\le\cdots+c_is_i$. Constraints (5c), (5d), (10i), (10j) range over distinct vertices of a bag (with $i=j$ the printed (5c) would be infeasible). A rooted binary tree decomposition is a published tree decomposition together with a root, a parent map and at most two children per node; the subtree root $z_0^p$ is the node of the subtree nearest the root. The partitions $J^i_z$, $I^j_z$ are arbitrary data with the properties stated on p. 17, which are all the proofs use. Proposition 7 is stated for every tree decomposition of $G'$; binarity is not needed there.

The generic finite linear-system and intersection-graph definitions can be reused beyond this paper. Contributions are welcome at every milestone; Proposition 4 is a general result on binary programs and is the most widely reusable.

Selected references

• Paul Blaettchen, André P. Calmon, and George Hall, Traceability Technology Adoption in Supply Chain Networks, Management Science, 2024; preprint arXiv:2104.14818v4 (2023). arXiv
• Neil Robertson and Paul D. Seymour, Graph Minors. V. Excluding a Planar Graph, Journal of Combinatorial Theory, Series B 41, 1986. DOI
• Monique Laurent, Sums of Squares, Moment Matrices and Optimization over Polynomials, in Emerging Applications of Algebraic Geometry, IMA Vol. 149, Springer, 2009. DOI
• Daniel Bienstock and Gonzalo Muñoz, LP Formulations for Polynomial Optimization Problems, SIAM Journal on Optimization 28(2), 2018. DOI

Motivation

Optimal transport asks how cheaply several prescribed probability distributions can be coupled. Adding a divergence penalty relative to their independent product makes the problem amenable to numerical methods, but changes its value. A quantitative bound on that change tells users of regularized transport how much bias a chosen regularization parameter can introduce. Eckstein and Nutz study this question through quantization of an optimal plan. Their Theorem 3.8 gives an entropic bound and a bound for a broader family of divergence penalties when the cost has a bounded second derivative. The result concerns the value of the transport problem; it does not assert convergence of optimal couplings or dual potentials.

Setting

There are $N\ge1$ marginals. For $i=1,\ldots,N$, $X_i$ is a closed convex subset of a Euclidean space and $\mu_i$ is a probability measure on $X_i$ with finite second moment. Their product $X=X_1\times\cdots\times X_N$ has the Euclidean product metric. A coupling $\pi\in\Pi(\mu_1,\ldots,\mu_N)$ is a probability measure on $X$ whose $i$th marginal is $\mu_i$. The reference measure $P=\mu_1\otimes\cdots\otimes\mu_N$ makes the coordinates independent.

The transport value $\mathrm{OT}$ is the infimum of $\int c\,d\pi$ over these couplings. The cost $c$ is continuous and has growth of order two, so its integral and the value are finite in this setting. For a strictly convex, lower bounded generator $f:[0,\infty)\to\mathbb R$ with $f(1)=0$ and $f(t)/t\to\infty$, the $f$-divergence $D_f(\pi,P)$ integrates $f(d\pi/dP)$ against $P$ when $\pi\ll P$; it is $+\infty$ otherwise. The regularized value is

$$\mathrm{OT}_{f,\varepsilon}=\inf_{\pi\in\Pi(\mu_1,\ldots,\mu_N)}\left(\int c\,d\pi+\varepsilon D_f(\pi,P)\right),\qquad \varepsilon>0.$$

Entropic regularization has $f(t)=t\log t$, with $f(0)=0$. A law belongs to $\mathcal P^n(X)$ when it is supported on at most $n$ points of $X$. An optimal plan $\pi^*$ has quantization rate $\operatorname{quant}_2(C,\alpha)$ when, for each $n\ge1$, some $\nu_n\in\mathcal P^n(X)$ satisfies $W_2(\nu_n,\pi^*)\le Cn^{-\alpha}$. Here $W_2$ is the Wasserstein distance for the Euclidean product norm. The rate hypothesis is on the joint optimal plan, not merely on its individual marginals.

Formalization targets

The goal is the corrected form of Theorem 3.8. Assume $c$ is twice continuously differentiable on a neighborhood of $X$, $B\ge0$, $C>0$, $0<\alpha\le1$, and $\pi^*$ is an optimal plan with $\operatorname{quant}_2(C,\alpha)$. The Hessian bound is two-sided and holds for every direction $w$ in the ambient product space:

$$|D^2c(x)[w,w]|\le B\|w\|^2\qquad(x\in X).$$

For entropy and $0<\varepsilon\le1$, the first target is

$$\mathrm{OT}_{f,\varepsilon}-\mathrm{OT} \le \frac{N-1}{2\alpha}\,\varepsilon\log(1/\varepsilon) +8BC^2\varepsilon.$$

For two marginals, suppose $f(t)=t\varphi(t)$ on $t>0$, where $\varphi$ is nondecreasing and concave there. Write $\beta=1/(2\alpha)$ and $\widetilde f(t)=t\varphi(t^\beta)$. If $\widetilde f$ is strictly increasing on $[x_0,\infty)$, $x_0\ge0$, put $S_\varepsilon=\widetilde f^{-1}(1/\varepsilon)$. The second target includes $S_\varepsilon\to\infty$ and $\varepsilon S_\varepsilon\to0$ as $\varepsilon\downarrow0$ and, when $0<\varepsilon$, $\varepsilon x_0\le1$, and $S_\varepsilon\ge1$,

$$\mathrm{OT}_{f,\varepsilon}-\mathrm{OT} \le \frac{8BC^2+1}{S_\varepsilon}.$$

The source prints $8BC$ in both bounds and a one-sided condition in (3.4). The squared quantization estimate requires $C^2$, and the Hessian condition must control both signs in every ambient direction. The mission records these corrections explicitly rather than changing the quantization hypothesis.

Significance

The first estimate controls entropic bias at order $\varepsilon\log(1/\varepsilon)$ when an optimal joint plan admits the stated $W_2$ quantization rate. The second expresses a rate for other divergence generators through an inverse function determined by $f$. These are established analytical results in the cited paper, though the corrected formulation is needed for the stated constants and hypotheses. The formalization target is a machine-checked statement of those rates and their supporting cost and divergence bounds. No completed machine-checked proof of this mission's goal is claimed here.

Difficulty

A finite approximation of the optimal plan need not retain the prescribed marginals. Restoring them can increase cost and divergence. A direct first-order cost estimate also misses the improvement sought here: the result uses cancellation associated with martingale quantization, while the remaining cost change is quadratic in the Wasserstein error. The requested infrastructure therefore includes a transport model with actual probability couplings, finite-support quantizers on the joint space, and a divergence that keeps its infinite value outside absolute continuity.

Formalization scope

Lean represents each marginal space by EuclideanSpace ℝ (Fin (d i)) and the product by PiLp 2, whose norm is the paper's Euclidean product metric. The paper's marginal $\mu_{i+1}$ is Lean's index i : Fin N. The formal statement requires $N>0$, closed convex supports, probability marginals concentrated on those supports with finite second moments, growth of order two for $c$, and $C^2$ regularity on an open neighborhood. The real value OTval is used only under those conditions; OTreg and fDiv use extended real values, so an infinite divergence cannot silently become zero. The divergence definition assigns $+\infty$ when its density integrand is not integrable, consistent with a lower-bounded generator under a probability reference measure. The condition $\varepsilon x_0\le1$ covers $x_0=0$ without division by zero. The function $\varphi$ is constrained only on $(0,\infty)$, allowing generators with a nonzero value at zero.

The development reuses the published WassersteinDRO.Duality.wassersteinDistance for $W_2$. Its new definitions of couplings, product reference law, divergence, quantization, and martingale coupling are reusable for related finite-dimensional transport results. The milestones isolate the Taylor estimate, the marginal-restoring coupling and its data-processing bound, the corrected cost estimate, and the entropic discrete-marginal bound of Lemma 2.3(iii). Lemma 2.3(i) is not posed here because the proposed positive-argument interpretation of $f(t)=t\varphi(t)$ does not control $f(0)$, and its stated divergence bound then has a two-point counterexample. A valid closure must use joint-plan quantization and a two-sided Hessian bound; replacing the regularized infimum by a default real value, restricting the Hessian to directions inside $X$, or quantizing only the marginals would change the result.

Selected references

• Stephan Eckstein and Marcel Nutz, Convergence Rates for Regularized Optimal Transport via Quantization, Mathematics of Operations Research, 2024; arXiv:2208.14391v3, pp. 5–8, 14–17. This mission cites the held arXiv version's pagination and labels.

Motivation

Classical ruin theory studies the Cramér–Lundberg model: an insurer's capital grows linearly through premiums and drops at the arrival epochs of a compound Poisson stream of claims. Two features of real capital processes are missing from it. Free capital earns interest, so the drift depends on the current level. And a firm may receive capital injections, upward jumps that arrive at random. Ruin with compounding assets goes back to Harrison (1977) and is surveyed in Paulsen (2008). Discounted penalties at ruin, which involve the deficit at ruin and the surplus just before it, are the subject of Gerber–Shiu theory (Kyprianou 2013).

Boxma and Mandjes (Affine storage and insurance risk models, Math. Oper. Res. 46(4), 2021) combine both features. The surplus has an affine drift $p + rX_t$ and two-sided jumps. They give a closed form for the joint transform of three ruin quantities: the time of ruin, the surplus just before ruin (the undershoot) and the deficit at ruin (the overshoot). The same insurance process later drives the paper's two storage models (§3–§4), through a duality argument. This mission formalizes the insurance result, §2 of the paper, culminating in its Theorem 1.

Setting

Fix a premium rate $p > 0$ and an interest rate $r > 0$. Upward jumps arrive at the epochs $T^+_n$ of a Poisson process with rate $\lambda_+ > 0$, and their sizes $U_n$ are i.i.d. exponential with mean $\mu^{-1}$. Claims arrive at the epochs $T^-_n$ of an independent Poisson process with rate $\lambda_- > 0$. Their sizes $D_n$ are i.i.d. with a density $d$ on $(0,\infty)$ and Laplace–Stieltjes transform $\delta(s) = \int_0^\infty e^{-sy} d(y)\,dy$. Write $\lambda = \lambda_- + \lambda_+$.

Starting from $X_0 = x$, the surplus follows $dX_t = p\,dt + rX_t\,dt$ between jumps. It rises by $U_n$ at $T^+_n$ and falls by $D_n$ at $T^-_n$:

$$X_t = xe^{rt} + \tfrac pr(e^{rt}-1) + \sum_{T^+_n \le t} e^{r(t-T^+_n)}U_n - \sum_{T^-_n \le t} e^{r(t-T^-_n)} D_n .$$

The ruin time is $\tau_x = \inf\{s > 0 : X_s \le 0\}$, with $\tau_x = \infty$ if the surplus stays positive. The overshoot is $X_{\tau_x} \le 0$ and the undershoot is the left limit $X_{\tau_x-}$. Let $T_\nu$ be exponential with mean $\nu^{-1}$, independent of everything else. For $\alpha, \beta, \gamma \ge 0$ define

$$\varrho(x) = \mathbb E\big(e^{-\alpha\tau_x + \beta X_{\tau_x} - \gamma X_{\tau_x-}} 1_{\{\tau_x < T_\nu\}} \,\big|\, X_0 = x\big), \qquad \varphi(\vartheta) = \int_0^\infty \vartheta e^{-\vartheta x} \varrho(x)\,dx .$$

So $\varphi(\vartheta)$ is $\varrho$ evaluated at an initial surplus that is exponential with mean $\vartheta^{-1}$.

Put $A = -(\alpha+\nu)/r$ and

$$F(\vartheta) = \frac pr - \frac{\lambda_-}r \frac{1-\delta(\vartheta)}\vartheta + \frac{\lambda_+}r \frac1{\mu-\vartheta} + \frac A\vartheta .$$

Let $F_\star$ be a primitive of $F$ on $(0,\mu) \cup (\mu,\infty)$. Put $G_1 = -p/r$, $G_2(\vartheta) = -\frac{\lambda_+}{r}\frac{1}{\mu-\vartheta}$ and $G_3(\vartheta) = \frac{\lambda_-}r\frac{\delta(\beta)-\delta(\vartheta+\gamma)}{\vartheta+\gamma-\beta}$. Then let $I_k(\vartheta) = \int_\vartheta^\infty G_k(\eta) e^{-F_\star(\eta)}\,d\eta$ and $G = \varrho(0)G_1 + \varphi(\mu)G_2 + G_3$.

Formalization targets

Goal: Theorem 1 (p. 1288)

For every $\vartheta > 0$ with $\vartheta \neq \mu$,

$$\varphi(\vartheta) = -\Big(\int_\vartheta^\infty G(\eta) e^{-F_\star(\eta)}\,d\eta\Big) e^{F_\star(\vartheta)},$$

where $\Delta = I_1(0)I_2(\mu) - I_1(\mu)I_2(0) \neq 0$ and

$$\varrho(0) = -\frac{I_3(0)I_2(\mu) - I_3(\mu)I_2(0)}{\Delta}, \qquad \varphi(\mu) = -\frac{I_1(0)I_3(\mu) - I_1(\mu)I_3(0)}{\Delta}.$$

The constants $\varrho(0)$ and $\varphi(\mu)$ are the model's own, defined through the process, not free parameters.

Milestones

The milestones follow the paper's derivation:

• eq. (2), the flow between jumps;
• $\varphi(\infty) = \varrho(0) \in (0,1)$;
• Lemma 1, the integro-differential equation (4) for $\varrho$;
• the four transform identities of p. 1286, including eq. (5);
• Proposition 1, the linear differential equation $\varphi' = F\varphi + G$;
• the divergence of $F_\star$ at $\infty$, $0$ and $\mu$;
• Remark 3, finiteness of the $I_k$;
• eqs. (11), (9) and (10).

Significance

Theorem 1 reduces a three-dimensional joint law to one-dimensional integrals of explicit functions of the model data. Through $\alpha$, $\beta$, $\gamma$ and $\nu$ it gives the transform of the ruin time, overshoot and undershoot jointly. Inverting it numerically gives ruin probabilities before a fixed horizon. Its specialisations include discounted penalty functions of Gerber–Shiu type for a risk process with interest and capital injections. In the paper, the same analysis carries over to a reflected storage process and to the dual storage process with affine release rate.

On the formal side, no ruin-theory result for a risk process with interest is machine-checked yet. The mission produces a pathwise construction of a piecewise-deterministic jump process with level-dependent drift, and a rigorous version of the paper's heuristic derivation. The page derives Lemma 1 by an $o(h)$ argument that assumes $\varrho$ is differentiable. It also asserts the boundary behaviour of $F_\star$, and it solves the linear system (10)–(11) without checking that its determinant is nonzero. All three steps become proof obligations here.

Difficulty

The algebra from Proposition 1 to Theorem 1 is routine once its inputs are available. Two steps are not.

The first is analytic regularity of $\varrho$. Lemma 1 needs $\varrho$ to be differentiable on $(0,\infty)$. The obvious route conditions on the first event in $[0,h]$ and lets $h \downarrow 0$, but it presupposes that derivative. Proving it requires a first-jump decomposition along the deterministic flow, together with right-continuity of $\varrho$ at $0$, which is the identity $\varphi(\infty) = \varrho(0)$.

The second is the singular point $\vartheta = \mu$, where $F$ has a pole. The variation-of-constants formula fixes $F_\star$ only up to separate constants on $(0,\mu)$ and $(\mu,\infty)$. For $\vartheta < \mu$, the formula (9) integrates across the pole. Its correctness there rests on $I(\mu) = 0$, which in turn comes from the boundedness of $\varphi$ near $\mu$. The page's order, (9) before (11), hides this dependence.

Formalization scope

All primitives (interarrival times and jump sizes of both streams) form one independent family Z : Fin 4 × ℕ → Ω → ℝ on a probability space, with the stated laws. The surplus $X$ and its left limit are defined by the closed form above. Jump counts are least indices, which agree with the true counts almost surely. The ruin time takes values in $[0,\infty]$. The horizon $T_\nu$ is integrated out against expMeasure ν. $F_\star$ is quantified over all primitives of $F$ on $(0,\mu)\cup(\mu,\infty)$. At the removable point $\vartheta = \beta - \gamma$, $G_3$ takes its limit value $\frac{\lambda_-}{r}\int_0^\infty y e^{-\beta y}d(y)\,dy$.

The hypotheses $r > 0$, $\lambda_+ > 0$, $\lambda_- > 0$ and $\mu > 0$ are added to the page's $\lambda_\pm, r \ge 0$. With $\lambda_+ = 0$ the denominator in (12) vanishes, with $\lambda_- = 0$ ruin is impossible, and the page itself assumes $r > 0$ tacitly. The case $p = 0$ (Remark 5) and the page's sharper logarithmic rates of $F_\star$ are not formalized. Those rates need a moment of the claims that the paper does not assume; the milestones state only what holds without it.

The goal cannot be satisfied trivially. $\varrho$ and $\varphi$ are expectations over the pathwise process, not formulas. Theorem 1 is about these objects, not about an arbitrary bounded solution of (6). The determinant condition $\Delta \neq 0$ is part of the conclusion, so the quotient in (12) is never Lean's $x/0 = 0$.

Useful infrastructure, all welcome as contributions:

• Laplace-transform identities for bounded functions on $(0,\infty)$, including differentiation under the integral and integration by parts with boundary terms;
• regularity of expected functionals of piecewise-deterministic jump processes;
• variation-of-constants uniqueness for linear ODEs on intervals with singular endpoints.

The first and last are reusable beyond this mission.

Selected references

• O. Boxma and M. Mandjes, Affine storage and insurance risk models, Mathematics of Operations Research 46(4):1282–1302, 2021. https://doi.org/10.1287/moor.2020.1097
• J. M. Harrison, Ruin problems with compounding assets, Stochastic Processes and their Applications 5(1):67–79, 1977. https://doi.org/10.1016/0304-4149(77)90051-5
• J. Paulsen, Ruin models with investment income, Probability Surveys 5:416–434, 2008. https://doi.org/10.1214/08-PS134
• J. Paulsen and H. K. Gjessing, Ruin theory with stochastic return on investments, Advances in Applied Probability 29(4):965–985, 1997. https://doi.org/10.2307/1427849
• A. E. Kyprianou, Gerber–Shiu Risk Theory, Springer, 2013. https://doi.org/10.1007/978-3-319-02303-8
• S. Asmussen and H. Albrecher, Ruin Probabilities, 2nd ed., World Scientific, 2010. https://doi.org/10.1142/7431

Why auction revenue depends on bidders’ expectations

A seller choosing between a first-price auction (FPA) and a second-price auction (SPA) needs to know whether the payment rule changes expected revenue. In the classical independent private-value benchmark, the two formats can be revenue equivalent. Balzer and Rosato examine a different setting: a bidder’s value depends on other bidders’ private signals, and the bidder dislikes outcomes that fall below a reference lottery formed from the bid she chooses. Their result gives a precise revenue ranking under these preferences. The paper was published online in Management Science in 2020 in its Articles in Advance pagination Balzer and Rosato.

The question matters because a payment rule changes both what a winner pays and which monetary outcomes she anticipates. In an FPA the winner pays her own bid. In an SPA she pays the highest opposing bid, so her payment varies with competitors’ signals even when she wins. Balzer and Rosato distinguish the risk of winning versus losing, which they call extensive risk, from variation in value or payment among winning outcomes, which they call intensive risk. Their analysis asks how these risks affect bidding and the seller’s expected receipts Balzer and Rosato, §§3–4.

Auction and preference setting

There are $N=m+2\ge2$ bidders. Each observes a signal $t_i$ drawn independently from a continuously differentiable distribution $F$ on $[\underline t,\overline t]$, where $0\le\underline t<\overline t$ and the density $f$ is strictly positive. Bidder $i$ values the item at $v(t_i,t_{-i})$. The value is nonnegative, increasing in every signal, strictly increasing in the bidder’s own signal, twice continuously differentiable, and symmetric in opponents’ signals. The distribution of the highest of the $m+1$ opposing signals has cumulative distribution $F_1=F^{m+1}$ and density $f_1$ Balzer and Rosato, §2.1 and §3.1.

A realized outcome is a value-payment pair $(V,p)$. Its comparison point is another such pair $(r^V,r^p)$. Gain–loss utility is $\mu^l(x)=\eta^l x$ for $x\ge0$ and $\mu^l(x)=\eta^l\lambda^l x$ for $x<0$, with $l\in\{g,m\}$ denoting the item and money dimensions. Here $\eta^l\ge0$, $\lambda^l>1$, and $\Lambda^l=\eta^l(\lambda^l-1)$. Total utility is

$$U((V,p)\mid(r^V,r^p))=V-p+\mu^g(V-r^V)+\mu^m(r^p-p).$$

For outcome lottery $G$ and reference lottery $H$, expected utility $EU[G\mid H]$ averages this expression over an independent draw from each lottery. Under a choice-acclimating personal equilibrium (CPE), a type $t$ assesses each possible nonnegative bid against the lottery that the same bid induces. A symmetric increasing strategy $\beta$ is a CPE when bidding $\beta(t)$ maximizes this self-referenced expected utility for every type. The paper maintains Assumption 1, $\Lambda^g\le1$, through its CPE results Balzer and Rosato, Definition 1 and Assumption 1.

Formalization targets

The main target is Corollary 1. For any symmetric CPE strategies $\beta_I$ and $\beta_{II}$ in the FPA and SPA, respectively, let $R_I$ and $R_{II}$ be the expectation of the sum of all bidders’ payments. Then

$$\Lambda^m=0\ \Longrightarrow\ R_{II}=R_I, \qquad \Lambda^m>0\ \Longrightarrow\ R_{II}<R_I.$$

The milestone list follows the paper’s CPE results: the direct-utility representations (10) and (12), existence and bid formulas for every symmetric equilibrium in Propositions 7 and 9, the common equilibrium-utility identity in the proof of Proposition 11, and Proposition 11’s comparison of utilities and payments. These targets retain the distinction between a lottery-based preference definition and the formulas derived from it Balzer and Rosato, pp. 10–11 and Appendix.

What the result gives

The corollary tells the seller which format yields more expected revenue within this model. When bidders have no loss aversion over money, the two formats yield the same revenue even though values are interdependent. With positive monetary loss aversion, the FPA yields strictly more. Proposition 11 gives the bidder-level comparison behind this statement: equilibrium utility is the same in both formats, while each type above the lowest pays more in expectation in the FPA when $\Lambda^m>0$ Balzer and Rosato, Proposition 11 and Corollary 1.

The result is proved in the paper but is not yet machine-checked in this mission. A completed formalization would connect the primitive gain–loss utility, lottery construction, CPE incentive condition, interim payment comparison, and ex ante revenue ranking. The auction data module can also support other results about independent signals and interdependent values; the loss-aversion module records the additional preference and equilibrium structure.

Main difficulty

The expected utility of a bid changes when the bid changes because the reference lottery changes with it. Treating the comparison point as fixed would describe a different equilibrium concept. An SPA also exposes winners to variation in the payment itself, which is absent from the FPA. Thus the two formats cannot be compared merely by inserting the same bid into different payment formulas. The paper’s two direct-utility displays and its payment comparison are separate substantive targets Balzer and Rosato, §4 and proof of Proposition 11.

Formalization scope

Lean uses real-valued signals, values, bids, and payments, and exactly $m+2$ bidders, so an opponent always exists. The signal law is a density-weighted measure on $[\underline t,\overline t]$; opponent and all-bidder signals use product laws. Strategies are measurable, nonnegative, and strictly increasing on the signal support. The model requires measurable values so mapped lotteries are genuine measures. A bid wins only when it strictly exceeds every opposing bid; ties have probability zero under the stated atomless signal law and strict monotonicity. Values of strategies outside the support do not affect the lotteries.

Revenue is defined directly as the expectation of the sum of payments, rather than by the payment formulas that the results seek to establish. Likewise, CPE is the incentive inequality over every nonnegative bid, and expected utility is built from the primitive outcome and reference lotteries. The direct-utility formulas are theorem targets, not definitions. The conditional value $V(\widetilde t,t)$ is used only when $\widetilde t>\underline t$, where $F_1(\widetilde t)>0$; the bid formulas (11) and (13) are stated on $(\underline t,\overline t]$ because their displayed denominators vanish at the lower endpoint for some bidder counts.

The paper writes the intensive-risk term with a conditional density of value, although that density need not exist for private values. Lean instead uses a double expectation over the winning-signal region. The paper’s printed prefactor $F_1(t)F_1(\widetilde t)$ in (10) is inconsistent with a reference lottery induced by the deviation; the formalization uses $F_1(\widetilde t)^2$. This correction is recorded on both representation milestones. Contributions toward the measure identities, equilibrium existence, envelope identity, and bidder-level payment comparison are all within scope.

Selected references

• B. Balzer and A. Rosato, Expectations-Based Loss Aversion in Auctions with Interdependent Values: Extensive vs. Intensive Risk, Management Science, Articles in Advance, pp. 1–19, published online 2020. DOI: 10.1287/mnsc.2019.3563.

Motivation

Estimating a probability that is too small to observe often by direct simulation is a routine problem in reliability analysis and rare-event simulation. Importance sampling changes the sampling law so that the event is seen more often, then corrects each sampled outcome with a likelihood ratio. The conventional design in a large-deviations setting mixes one exponential tilt for every dominating point of the rare-event set. That design is judged by the estimator's second moment. Bai, Huang, Lam and Zhao ask whether the resulting variance requirement is stronger than what is needed for an estimate that is accurate with high probability Bai et al., 2022.

Their result concerns the case in which different parts of the rare-event set have different exponential rates. A part with a higher rate can contribute a very large likelihood ratio on the rare occasions it is sampled, making the variance large, while barely affecting an estimate from a feasible number of replications. The paper introduces probabilistic efficiency to express the sampling requirement directly through the estimator's relative error. The mission formalizes the paper's Theorem 6, which treats all ties among the most significant dominating points.

Setting

For each rarity parameter $\gamma>0$, let $X_\gamma$ be a random vector in $\mathbb R^d$ with law $\nu_\gamma$. Fix a Borel set $\mathcal E\subseteq\mathbb R^d$. The probability to be estimated is

$$p_\gamma=\Pr(\gamma^{-1}X_\gamma\in\mathcal E).$$

The scaled logarithmic moment generating function is $\mu_\gamma(s)=\gamma^{-1}\log\mathbb E[\exp(s^\top X_\gamma)]$. Assumption 1 requires a pointwise extended-real limit $\mu$, an interior effective domain containing zero, differentiability there, and steepness at its boundary. Its rate function is the Legendre transform $I(y)=\sup_s\{s^\top y-\mu(s)\}$, and $I(B)=\inf_{y\in B}I(y)$ for a set $B$. Assumption 2 requires $\mathcal E$ to be Borel, $\overline{\mathcal E}=\overline{\mathcal E^\circ}$, $\mathcal E^\circ\cap\mathcal D(I)^\circ\ne\varnothing$, and $I(\mathcal E)>0$ Bai et al., pp. 7–8.

A dominating set $A=\{a_1,\ldots,a_r\}$ is a finite minimal collection of boundary points of $\mathcal E$. Each $a_i$ has an associated tilt $s_{a_i}$ satisfying $\nabla\mu(s_{a_i})=a_i$, and the half-spaces $\{x:s_{a_i}^\top(x-a_i)\ge0\}$ cover $\mathcal E$. A point is more significant when it has a smaller value of $I$. Exponential tilting toward $a_i$ gives a sampling law whose density relative to the original law is $\exp(s_{a_i}^\top X_\gamma-\gamma\mu_\gamma(s_{a_i}))$. A mixture gives these laws positive weights $\alpha_i$ summing to one Bai et al., pp. 8–10.

For $n(\gamma)$ independent outputs $Z$ under the mixture law $\widetilde P_\gamma$, write $\hat p_\gamma$ for their mean. At tolerance $\varepsilon>0$, the minimal relative discrepancy is $\delta_\varepsilon(\hat p_\gamma,p_\gamma)=\inf\{\delta>0:\widetilde P_\gamma(|\hat p_\gamma-p_\gamma|>\delta p_\gamma)\le\varepsilon\}$. Strong probabilistic efficiency means that one sample-size function $n(\gamma)$ grows subexponentially in $-\log p_\gamma$ and makes this discrepancy tend to zero for every $\varepsilon>0$ Bai et al., p. 16.

Formalization targets

Most significant dominating points

Let $S$ contain exactly the points of $A$ having the smallest rate, including every tie. The goal is Theorem 6 Bai et al., p. 20:

$$\frac{d\widetilde P_\gamma}{dP_\gamma} =\sum_{i\in S}\alpha_i\exp\!\left(s_{a_i}^{\top}X_\gamma-\gamma\mu_\gamma(s_{a_i})\right), \qquad \sum_{i\in S}\alpha_i=1,\quad\alpha_i>0 \quad\Longrightarrow\quad \delta_\varepsilon(\hat p_\gamma,p_\gamma)\longrightarrow0 \quad(\forall\varepsilon>0)$$

for some $n(\gamma)\ge1$ with $\log n(\gamma)/(-\log p_\gamma)\to0$. The result allows the mixture to omit every dominating point with a strictly larger rate. It does not choose a fixed sample size or require a second-moment efficiency guarantee for the resulting mixture.

Supporting targets

The milestones state the Gärtner–Ellis bounds of Theorem 1, the rate minimization of Theorem 2, full-mixture asymptotic efficiency of Proposition 1, the implication of Proposition 6, and the rare-event and tilted decay estimates used in the paper. Theorem 3 supplies a general discrepancy bound for a disjoint split of a rare event Bai et al., pp. 8–9, 17–18, 21–22.

Significance

The theorem establishes that a sampler can satisfy the paper's relative-accuracy criterion while omitting less significant dominating points. It explains why a large variance caused by rare, high-weight observations need not predict poor performance at the sample sizes in this asymptotic regime. The single-point case, Theorem 5, is included when $S$ has one member; the mission takes the more general finite-mixture claim as its goal Bai et al., pp. 19–20.

The result is proved in the cited paper. The work here is to give the assumptions, mixture law, discrepancy criterion, and rate comparisons a common Lean statement that can support a machine-checked proof. Mathlib supplies measures, product measures, integrals, Euclidean geometry and filters; the paper-specific definitions and proofs remain to be formalized.

Difficulty

The familiar variance test can fail for a sampler that omits a dominating point: a sample from the omitted region may receive a very large likelihood ratio even though such samples are extremely unlikely under the selected tilts. Bounding the full second moment therefore does not establish the desired criterion. The formal target must keep the probability of encountering that region separate from the behavior of the estimator on the main region. The argument also needs the large-deviation rate under each tilted law, including the strict gap between selected and omitted dominating points Bai et al., pp. 20–22.

Formalization scope

The Lean model uses laws $\nu_\gamma$ on EuclideanSpace ℝ (Fin d) in place of random variables on an unspecified probability space; all probabilities in the paper depend only on those laws. The functions $\mu_\gamma$, $\mu$ and $I$ use extended real values, while event probabilities and discrepancy ratios use real values. The mixture uses Mathlib's exponential tilt and fixed positive weights. The output uses the paper's explicit likelihood ratio. The sample mean uses the product law on Fin n, and $n\ge1$ is fixed before the tolerance $\varepsilon$ is quantified.

The finite dominating set is enumerated injectively, and $S$ is a nonempty finite set of exactly the lowest-rate indices. The definition of asymptotic efficiency requires an eventual finite second moment; Theorem 3 also requires its variance to be genuine. Its displayed bound is stated for sufficiently large $\gamma$, where the denominator is positive. Theorem 3 states the sample-size and variance condition supplied by its printed asymptotic-efficiency premise. These choices exclude zero tilted measures, default zero values for nonintegrable variances, and the weaker quantifier order in which a new $n$ may be chosen for each tolerance. Theorem 1's second clause, as printed, asserts $\lim_{\gamma\to\infty}\gamma^{-1}\log P(\gamma^{-1}X_\gamma\in\mathcal E)=-I(\mathcal E)$ under Assumption 2 alone. This fails when $\mathcal E$ contains a point on the boundary of $\mathcal D(I)$ with finite rate and zero probability. An example is $X_\gamma$ a Poisson variable of mean $\gamma$ plus an independent uniform variable on $[0,1]$, with $\mathcal E=[-1,0]\cup[5,6]$. The milestone therefore states that clause for sets that also have a finite dominating set, which covers every use in the paper. Definitions of the rate function, dominating set, event split, and discrepancy can be reused in later formalizations of rare-event simulation.

Selected references

• Y. Bai, Z. Huang, H. Lam and D. Zhao, Over-Conservativeness of Variance-Based Efficiency Criteria and Probabilistic Efficiency in Rare-Event Simulation, arXiv:2110.12573v2, 2022; published in Management Science, 2024. arXiv preprint
• A. Dembo and O. Zeitouni, Large Deviations Techniques and Applications, second edition, Springer, 1998; corrected printing 2009. DOI

Motivation

Exchanges increasingly operate several venues side by side: a lit pool, where the limit order book is visible, and a dark pool, where orders are hidden and trades execute at the mid-price. Liquidity on both venues is supplied largely by market makers, and exchanges steer that supply through make-take fees: rebates paid to liquidity providers and fees charged to liquidity takers. How to set such fees is a principal–agent problem. The exchange (principal) designs a remuneration contract; the market maker (agent) chooses which volumes to post where, given the contract.

B. Baldacci, I. Manziuk, T. Mastrolia and M. Rosenbaum (arXiv:1912.01129, published in Operations Research in 2023) model this situation for one market maker quoting on a lit and a dark pool of the same exchange. The approach follows the contract-theoretic treatment of make-take fees by El Euch, Mastrolia, Rosenbaum and Touzi (arXiv:1805.01145), in which the exchange's problem reduces to a Hamilton–Jacobi–Bellman (HJB) equation once the market maker's best response is substituted. In the present model the inventory lives on a finite grid and the reduced equation is a finite system of backward ordinary differential equations whose right-hand side is a supremum over incentives. The paper's main theorem asserts that this system is well posed; its numerical sections then solve it with deep reinforcement learning.

Setting

Time runs over $[0,T]$ with $T>0$. The market maker posts volumes $\ell^{i,j}$ on side $i\in\{a,b\}$ (ask, bid) of pool $j\in\{l,d\}$, taken from finite sets $\mathcal V^l,\mathcal V^d\subset\mathbb N$ containing $0$. The inventory $q$ is an integer between the risk limits $-\bar q$ and $\bar q$; volumes are admissible at $q$ when $\ell^{a,l}+\ell^{a,d}\le q+\bar q$ and $\ell^{b,l}+\ell^{b,d}\le\bar q-q$. Write $\phi(a)=1$, $\phi(b)=-1$.

Market orders arrive with intensities driven by the lit-pool imbalances $I^a=\ell^{a,l}/(\ell^{a,l}+\ell^{b,l})$, $I^b=\ell^{b,l}/(\ell^{a,l}+\ell^{b,l})$ (both $0$ when nothing is posted in the lit pool):

$$\lambda^{i,j}(\mathcal L^l)=A^j\exp\Big(-\frac{\theta^j}{\sigma}\psi^{i,j}(\mathcal L^l)\Big)\ \text{if }\mathcal L^l\ne(0,0),\qquad \lambda^{i,j}=\epsilon\ \text{otherwise},$$

where $\psi^{i,j}$ is $I^a$ for $(a,l),(b,d)$ and $I^b$ for $(b,l),(a,d)$. A fill of size $k$ on side $i$ of pool $j$ has intensity $\lambda^{\mathcal L,i,j,k}=\lambda^{i,j}\mathbf 1_{\{\phi(i)q>-\bar q,\ \ell^{i,j}=k\}}$ and moves the inventory to $q-\phi(i)k$. A dark fill is executed at the mid-price, or at half a tick $\mathcal T/2$ from it under latency $\kappa\in K=\{\mathrm{lat},\text{non-lat}\}$, the latency states being weighted by $\phi^d(i,\kappa)\in\{I^a,I^b\}$. Fills carry market impact $\Gamma^l\ge\Gamma^d>0$.

The exchange offers jump incentives $z=(z^{i,j,k})_{i,j,k\in\mathcal V^j}$ and a price-risk incentive $z^{\tilde S}$. The market maker's Hamiltonian (4.10) is

$$h(\mathcal L,z,q)=\sum_i\gamma^{-1}\Big(\sum_{k\in\mathcal V^l}\big(1-e^{-\gamma(z^{i,l,k}+\ell^{i,l}(\frac{\mathcal T}{2}+\phi(i)\Gamma^lq)-\Gamma^l(\ell^{i,l})^2)}\big)\lambda^{\mathcal L,i,l,k}+\sum_{k\in\mathcal V^d}\sum_{\kappa}\big(1-e^{-\gamma(\cdots)}\big)\lambda^{\mathcal L,i,d,k}\phi^d(i,\kappa)\Big),$$

with risk aversion $\gamma>0$, and a best response $\mathcal L^\star(z,q)$ maximizes it over admissible volumes. The exchange, with risk aversion $\eta>0$ and fees $c^j>0$, faces

$$\mathcal U=v(t,q)\Big(\tfrac\eta2\sigma^2\gamma(z^{\tilde S}+q)^2+\tfrac{\eta^2\sigma^2}2(z^{\tilde S})^2\Big)+\sum_{i,j}\sum_{k\in\mathcal V^j}\lambda^{\mathcal L^\star,i,j,k}\Big(e^{\eta(z^{i,j,k}-kc^j)}v(t,q-\phi(i)k)-v(t,q)\big(1+\eta\,\mathcal E\big)\Big),$$

where $\mathcal E$ is the market maker's certainty-equivalent gain from the fill, and $\mathcal H(q,\mathcal L^\star,v(t,\cdot))=\sup_{z^{\tilde S},z}\mathcal U$.

Formalization targets

Goal: Theorem 3 (first assertion)

For every best-response selection $\mathcal L^\star$, the system

$$0=\partial_tv(t,q)+\mathcal H\big(q,\mathcal L^\star,v(t,\cdot)\big),\quad q\in\{-\bar q,\dots,\bar q\},\ t\in[0,T),\qquad v(T,q)=-1\qquad(4.15)$$

has a continuous viscosity solution, and any two continuous viscosity solutions coincide on $[0,T]\times\{-\bar q,\dots,\bar q\}$. No growth, sign or regularity condition is imposed on the competitors.

Milestone: Remark 4.2

Where $v(t,q)<0$, the supremum of $\mathcal U$ over $z^{\tilde S}$ is attained, uniquely, at

$$z^{\tilde S}=-\frac{\gamma}{\gamma+\eta}\,q.$$

Significance

Well-posedness of (4.15) is what licenses the rest of the paper: the reduced value $v(0,Q_0)$ is identified with the exchange's optimal utility, the optimal make-take incentives are read off the supremum in (4.15), and the neural-network scheme of §5 approximates a well-defined object. Without uniqueness, a numerical solution of (4.15) need not be the value of the design problem.

The well-posedness assertion is justified in the paper by a single citation to lecture notes on stochastic control; no argument specific to this Hamiltonian is printed. A machine-checked proof makes explicit which properties of $\mathcal H$ the citation requires and that they hold here: finiteness, convexity and local Lipschitz continuity on the negative cone, and invariance of that cone under the backward flow. The result has not been formalized before; the platform has no market-making or make-take-fee model, and no viscosity notion for finite systems of backward ODEs.

Difficulty

$\mathcal H$ is a supremum over an unbounded set of incentives and is $+\infty$ as soon as a relevant component of $v(t,\cdot)$ is nonnegative, so the standard Lipschitz ODE theory does not apply directly. The best response $\mathcal L^\star(z,q)$ is an argmax over a finite set and may jump in $z$, so $\mathcal U$ is not continuous in the incentives. Global existence requires that solutions neither reach the region where $\mathcal H=+\infty$ nor blow up before time $0$. Uniqueness is claimed among all continuous viscosity solutions, not only negative ones, so a competitor must first be shown to stay in the region where $\mathcal H$ is finite. Finally, viscosity solutions must be related to classical ones for a system whose coupling is nonlocal in the inventory.

Formalization scope

Everything lives in the namespace MMDarkPool.Exchange. One definition item, Model, holds the parameters and the standing assumptions (Standing: $T,\mathcal T,\sigma,\gamma,\eta,\epsilon>0$; $A^j,\theta^j,c^j>0$; $\Gamma^l\ge\Gamma^d>0$; $0\in\mathcal V^l,\mathcal V^d$), the grid, admissible volumes, $I^a,I^b,\psi,\lambda,\phi^{\mathrm{lat}},\phi^d$, $h$ (4.10), the best-response predicate (4.6), $\mathcal E$, $\mathcal U$, $\mathcal H$ (4.16) and IsViscositySolution. Inventories are integers, cast to reals inside formulas; a solution is a function $v:\mathbb R\to\mathbb Z\to\mathbb R$ constrained on $[0,T]\times\{-\bar q,\dots,\bar q\}$ only. Jump incentives are indexed exactly by the volume sets, so the supremum ranges over $\mathbb R\times\mathbb R^{2(\#\mathcal V^l+\#\mathcal V^d)}$.

The formalization commits to these readings, each disclosed in the items:

1. The risk limit "$2\bar q\in\mathbb N$" is read as $\bar q\in\mathbb N$, so that the initial inventory $0$ is on the grid.
2. Admissible volumes keep the inventory within $\pm\bar q$ after a fill (§5.1.1 of the paper), besides $\ell^{i,l}+\ell^{i,d}\le2\bar q$.
3. $0\in\mathcal V^l,\mathcal V^d$, so a best response always exists.
4. The double sum over $\mathcal V^l\times\mathcal V^d$ printed in (4.10) is read as one sum per pool, as in $\mathcal U$.
5. $\mathcal H$ is valued in the extended reals.
6. The paper does not define its viscosity notion. The standard per-component notion is used: $C^1$ test functions in $t$, interior test times $t_0\in(0,T)$, the solution's own row $v(t_0,\cdot)$ as the nonlocal argument, subsolution $\partial_t\varphi+\mathcal H\ge0$ at local maxima of $v(\cdot,q)-\varphi$, supersolution $\le0$ at local minima, plus continuity on $[0,T]$ and $v(T,\cdot)=-1$.
7. The goal holds for every best-response selection, not for one specific selection.
8. Remark 4.2 carries the hypothesis $v(t,q)<0$, without which the supremum is not attained.

A real-valued supremum for $\mathcal H$ (which Lean sets to $0$ on unbounded sets), a statement about an abstract convex Hamiltonian, a choice-based maximizer in place of the supremum, or one-sided tests at $t=0$ would each change the theorem, and are ruled out. The identity $v^E_0=v(0,Q_0)$, the third sentence of Theorem 3, Theorems 1 and 2, and the numerical sections are not part of this mission: they need the stochastic model of controlled point processes, which has no substrate.

A complete development needs comparison or Picard–Lindelöf arguments for finite ODE systems with extended-real right-hand sides, and the passage from viscosity to classical solutions for time-only equations; both are reusable beyond this mission. Contributions of such lemmas as separate theorems are welcome.

Selected references

• B. Baldacci, I. Manziuk, T. Mastrolia, M. Rosenbaum, Market making and incentives design in the presence of a dark pool: a deep reinforcement learning approach, arXiv preprint, 2019; published as Market Making and Incentives Design in the Presence of a Dark Pool: A Stackelberg Actor–Critic Approach, Operations Research, 2023. https://arxiv.org/abs/1912.01129
• O. El Euch, T. Mastrolia, M. Rosenbaum, N. Touzi, Optimal make-take fees for market making regulation, Mathematical Finance 31(1), 2021. https://arxiv.org/abs/1805.01145
• M. G. Crandall, H. Ishii, P.-L. Lions, User's guide to viscosity solutions of second order partial differential equations, Bulletin of the AMS 27(1), 1992. https://doi.org/10.1090/S0273-0979-1992-00266-5