Missions · Prove2Me

Machine Learning Optimization·Captain: mikedeng1

Suboptimal Local Minima Exist for Wide Neural Networks with Smooth Activations: For Generic Inputs and Any Depth and Width, Some Output Data Gives the Squared Loss a Sub-Optimal Local MinimumResearch Paper

Motivation

Training a neural network means minimizing a non-convex loss over its weights. Local search methods can only certify local optimality, so a recurring question in the theory of neural network optimization is whether every local minimum of the training loss is a global minimum. A local minimum that is not global is called a sub-optimal (or bad) local minimum.

A line of positive results suggested that sufficiently wide networks have no bad local minima. Yu and Chen (IEEE Trans. Neural Networks 6(5), 1995, Theorem 3) stated that for one-hidden-layer sigmoid networks with at least as many hidden neurons as training samples, every local minimum is global; the survey of Bianchini and Gori (Neurocomputing, 1996) lists this as a main result of the area. Later work proved weaker landscape properties for deep over-parameterized networks, such as the absence of sub-optimal valleys or basins (Nguyen, Mukkamala and Hein, arXiv:1809.10749; Nguyen, arXiv:1901.07417), and Nguyen, Mukkamala and Hein conjectured that "no bad local minima" holds under mild conditions.

Timeline of related results, as attributed in the source paper:

1995: Yu and Chen state that wide one-hidden-layer sigmoid networks have no bad local minima.
1996: Auer, Herbster and Warmuth construct exponentially many local minima for a single neuron.
2016: Kawaguchi (NeurIPS 2016) shows that deep linear networks have no bad local minima.
2018: Safran and Shamir (ICML 2018) find spurious local minima in two-layer ReLU networks with Gaussian inputs; Yun, Sra and Jadbabaie (arXiv:1802.03487) construct bad local minima for networks with piecewise linear activations.
2019–2020: Ding, Li and Sun (arXiv:1911.01413) construct bad local minima for networks of any depth and width with almost every smooth activation, which also refutes the 1995 claim.

Setting

A fully connected network with $H$ hidden layers has widths $d_1, \dots, d_H$ , input width $d_0$ and output width $d_{H+1}$ . Its parameters are

\Theta = (W_1, \mathbf b_1, W_2, \mathbf b_2, \dots, W_H, \mathbf b_H, W_{H+1}),\qquad W_h \in \mathbb R^{d_h \times d_{h-1}},\ \mathbf b_h \in \mathbb R^{d_h}.

Given an activation $\sigma : \mathbb R \to \mathbb R$ and a data matrix $X \in \mathbb R^{d_0 \times N}$ whose columns are the $N$ samples, the post-activations are $T_0 = X$ and

(T_h)_{i,n} = \sigma\Big(\sum_{j} w_{h,i,j}\,(T_{h-1})_{j,n} + b_{h,i}\Big),\qquad 1 \le h \le H,

and the network output is $T_{H+1}(\Theta) = W_{H+1} T_H$ , with no output bias. For targets $Y \in \mathbb R^{d_{H+1}\times N}$ , the empirical loss is

E(\Theta) = \|Y - T_{H+1}(\Theta)\|_F^2 .

Two assumptions are made.

Assumption 1 (data). $d_0^2/2 + 3d_0/2 < N$ , and the vectors $\mathbf 1_N$ , the rows $X(i,:)$ , and the Hadamard products $X(i,:) \circ X(j,:)$ for $i \le j$ are linearly independent in $\mathbb R^N$ . Given the dimension condition, this holds for all $X$ outside a set of measure zero.
Assumption 2 (activation). For some $a \in \mathbb R$ and $\delta > 0$ , $\sigma$ is twice continuously differentiable on $[a - \delta, a + \delta]$ and $\sigma(a), \sigma'(a), \sigma''(a)$ are all nonzero. Sigmoid, softplus, ELU and Swish satisfy it.

Formalization targets

Goal: Theorem 1

For every $X$ satisfying Assumption 1 with $N \ge 3$ , every $\sigma$ satisfying Assumption 2, any depth $H \ge 1$ and any widths with $d_H \ge 2$ , there is an output matrix $Y$ such that

\exists\, \Theta:\quad \Theta \text{ is a local minimum of } E \quad\text{and}\quad \exists\, \Theta' :\ E(\Theta') < E(\Theta).

The data $X$ and the activation $\sigma$ are given; only $Y$ is chosen. The widths other than $d_H$ are unrestricted, so the statement covers arbitrarily wide and deep networks.

Milestones

Lemma 1 (p. 20): given linearly independent $\mathbf a_1, \dots, \mathbf a_{L_1}$ and $1 \le d < L_1$ , there are $L_2 - d$ linearly independent vectors orthogonal to $\mathbf a_1, \dots, \mathbf a_d$ and with positive inner product with $\mathbf a_{d+1}, \dots, \mathbf a_{L_1}$ .
The output data (§6.1, eqs. (25)–(29)): under Assumption 1, $\Delta Y = \sigma(a)\mathbf 1 - Y$ can be chosen with rows orthogonal to $\mathbf 1$ , to every row of $X$ and to every mixed product $X(j,:) \circ X(j',:)$ , and with $[\sigma'(a)]^{H-1}\sigma''(a)\langle \Delta Y(i,:), X(j,:)\circ X(j,:)\rangle > 0$ (conditions (23)).
The constant-output configuration (eqs. (19)–(21)): with $W_1 = 0$ , $\mathbf b_1 = a\mathbf 1$ , positive deeper weights, biases $b_{h,i} = a - \sigma(a)\sum_j w_{h,i,j}$ and $W_{H+1} = \frac1{d_H}\mathbf 1$ , every hidden neuron outputs $\sigma(a)$ and $T_{H+1} = \sigma(a)\mathbf 1$ .
Lemma 2 (p. 21): for each hidden layer $h$ there is such a configuration near which the change of $T_h$ caused by perturbing everything except $W_1$ is positively correlated with each row of $\Delta Y$ , quadratically in its size (32), and some nearby configuration makes $T_h$ itself positively correlated (33).
Local minimality (§6.2, eqs. (34)–(42)): the configuration of Lemma 2 at $h = H$ is a local minimum of $E$ .
Sub-optimality (§6.3, eqs. (43)–(50)): $E(\Theta) = \|\Delta Y\|_F^2 > 0$ and some $\Theta^*$ has a strictly smaller loss.

Significance

The theorem is a counter-example: for generic data and almost every smooth activation, increasing width or depth does not by itself remove bad local minima of the squared loss. It refutes Theorem 3 of Yu and Chen (1995) (Corollary 2 of the paper) and the conjecture of Nguyen, Mukkamala and Hein for this setting. Positive landscape results therefore need further assumptions on the data, the targets or the architecture, and the construction indicates which assumptions cannot be dropped.

The result is proved in the paper; no machine-checked proof of it is known. A formalization would verify a full counter-example for arbitrary depth, which involves a layer-by-layer second-order expansion whose bookkeeping across layers is where informal arguments of this type are most error-prone. It also provides a reusable Lean model of a deep fully connected network with biases and an arbitrary activation, which other landscape results can build on.

Difficulty

The output of the constructed configuration does not depend on the input, so a perturbation of $\Theta$ changes $T_{H+1}$ in ways that need not be first-order: the obvious approach of checking a vanishing gradient and a positive semidefinite Hessian is inconclusive, because the loss is flat along several directions at the constructed point (for instance, changes of $W_{H+1}$ that keep its row sums), and the decisive effect of perturbing $W_1$ appears only at second order in the hidden layers. Local minimality must be shown for all nearby configurations at once, by controlling the second-order term of every layer uniformly in a neighbourhood and propagating the sign through the $H$ layers. The correlation condition must hold for every row of $\Delta Y$ and every neuron simultaneously.

Formalization scope

Model. Matrices are functions Fin a → Fin b → ℝ; indices of neurons and samples are 0-based. The parameter space is the full product of all weights $W_1, \dots, W_{H+1}$ and all hidden biases $\mathbf b_1, \dots, \mathbf b_H$ , with its usual sup-norm metric; local minimality is Mathlib's IsLocalMin. The forward pass is defined by recursion over the layers, feeding the post-activation of layer $h-1$ to layer $h$ (the printed eq. (2b) writes the pre-activation, a slip).
Assumptions. Assumption 1(a) is written over ℕ as $d_0^2 + 3d_0 < 2N$ ; the products in 1(b) are indexed by unordered pairs $i \le j$ , so that the family has $d_0^2/2 + 3d_0/2 + 1$ members, as the paper counts. Assumption 2(a) is read as $C^2$ on the interval, matching the paper's gloss; $\sigma$ is arbitrary outside it.
Added hypotheses. $H \ge 1$ and positive widths $d_0, d_1, \dots, d_{H+1} \ge 1$ . With output width zero the loss is identically zero, and with a zero-width hidden layer the output does not depend on $X$ ; the paper's setting presupposes positive widths.
Lemma 2 is stated with hypothesis (23) on $\Delta Y$ instead of (28) on $Y$ (milestone 2 shows (28) implies (23)), with the printed index range $d_{h+1}$ read as $d_{H+1}$ , and with sup-norm balls around the full parameter in place of Euclidean balls around its first $h$ layers.
Ruled out. Fixing $W_1 = 0$ in the parameter type, choosing $X$ or $\sigma$ existentially, or indexing the Hadamard products by ordered pairs (which makes Assumption 1 unsatisfiable for $d_0 \ge 2$ and the theorem vacuous) would each trivialize the goal; none is done.
Not included. Theorems 2–5 and Corollaries 1–2 of the paper (piecewise linear activations, positive-measure sets of targets for sigmoid networks, and the cases $N = 1, 2$ ).

Contributions welcome: proofs of the milestones, in particular a Lean development of the layer-wise Taylor expansion behind Lemma 2.

Selected references

T. Ding, D. Li, R. Sun, Sub-Optimal Local Minima Exist for Neural Networks with Almost All Non-Linear Activations, arXiv:1911.01413v3, 2020; published as Suboptimal local minima exist for wide neural networks with smooth activations, Mathematics of Operations Research 47(4), 2022. https://arxiv.org/abs/1911.01413
X.-H. Yu, G.-A. Chen, On the local minima free condition of backpropagation learning, IEEE Transactions on Neural Networks 6(5):1300–1303, 1995. https://doi.org/10.1109/72.410380
Q. Nguyen, M. C. Mukkamala, M. Hein, On the loss landscape of a class of deep neural networks with no bad local valleys, ICLR 2019. https://arxiv.org/abs/1809.10749
K. Kawaguchi, Deep learning without poor local minima, NeurIPS 2016. https://arxiv.org/abs/1605.07110
I. Safran, O. Shamir, Spurious local minima are common in two-layer ReLU neural networks, ICML 2018. https://arxiv.org/abs/1712.08968
C. Yun, S. Sra, A. Jadbabaie, Small nonlinearities in activation functions create bad local minima in neural networks, ICLR 2019. https://arxiv.org/abs/1802.03487

8 thms2 active usersReviewed

Completed

Operations Research Optimization Statistics·Captain: mikedeng1

Flexible Drug Approval Policies: The Optimal Significance Level Is Higher for Diseases with Long Clinical Trials, High Attrition and Low R&D IntensityResearch Paper

Motivation

A drug regulator approves a candidate drug when its clinical trial rejects the null hypothesis of no effect at a fixed significance level $\alpha$ . FDA guidelines recommend the same threshold, $\alpha = 2.5\%$ , for every disease (Bravo, Corcoran and Long, p. 2). A uniform threshold balances the wrong errors for some diseases. For a severe disease with no available treatment, wrongly rejecting an effective drug (a type II error) can cost far more than wrongly approving an ineffective one (a type I error). For a crowded therapeutic area the balance is the other way. Regulators have responded with expedited programmes (Fast Track, Breakthrough Therapy, Accelerated Approval), and decision-analytic work has asked how trial design should account for the harm of each error (Montazerhodjat, Chaudhuri, Sargent and Lo, 2017).

Bravo, Corcoran and Long (2021) add the drug development pipeline and the market to this question. Candidate drugs arrive in clinical trials, some are abandoned, the rest are reviewed, and approved drugs stay on the market for a while. The optimal $\alpha$ then depends on operational quantities such as trial duration and attrition, and not only on the costs of the two errors. The paper's main analytical result is a set of comparative statics. The optimal level is higher for diseases with long trials, high attrition and few compounds in development. This mission formalizes that result together with the analytical steps of its proof.

Setting

A two-armed trial with $n$ patients per arm measures an outcome of standard deviation $\sigma$ . The information of the sample is $I_n = n/(2\sigma^2)$ . Under the alternative hypothesis, which says the drug has effect $\delta>0$ , the Wald statistic is approximately normal with mean $\delta\sqrt{I_n}$ and variance one. A drug is effective with prior probability $p$ . With $\Phi$ the standard normal distribution function, the probabilities that a drug is approved and effective (AE), approved and ineffective (AI), or rejected and effective (RE) are

\pi_{AE}(\alpha)=\big[1-\Phi(\Phi^{-1}(1-\alpha)-\delta\sqrt{I_n})\big]p,\qquad \pi_{AI}(\alpha)=\alpha(1-p),\qquad \pi_{RE}(\alpha)=\Phi(\Phi^{-1}(1-\alpha)-\delta\sqrt{I_n})\,p .

Drugs enter trials at rate $\lambda$ . Each trial is a race between completion at rate $\mu_{CT}$ and abandonment at rate $\mu_{AB}$ , so drugs reach review at rate $\tilde\lambda=\lambda\mu_{CT}/(\mu_{CT}+\mu_{AB})$ , and the outcome streams have rates $\lambda_{XY}(\alpha)=\tilde\lambda\,\pi_{XY}(\alpha)$ . Approved effective drugs fall into one of $K$ therapeutic classes and stay on the market at exit rate $\mu_E$ . Approved ineffective drugs leave at rate $\mu_I$ . With $\psi_E(\alpha)=\lambda_{AE}(\alpha)/(K\mu_E)$ and $\psi_I(\alpha)=\lambda_{AI}(\alpha)/\mu_I$ , the paper's expected numbers of effective and ineffective drugs on the market are $\mathbb E[N_E(\alpha)]=K\psi_E(\alpha)/(1+\psi_E(\alpha))$ and $\mathbb E[N_I(\alpha)]=\psi_I(\alpha)$ .

Each effective drug on the market yields health benefit $Q_E$ and each ineffective one costs $Q_I$ , valued at $\mathrm{WTP}$ per unit. Approving an effective drug yields $C_{AE}$ , approving an ineffective drug costs $C_{AI}$ , and rejecting an effective drug costs $C_{RE}$ . The expected net benefit is

V(\alpha)=\big(Q_E\,\mathbb E[N_E(\alpha)]-Q_I\,\mathbb E[N_I(\alpha)]\big)\mathrm{WTP}+C_{AE}\lambda_{AE}(\alpha)-C_{AI}\lambda_{AI}(\alpha)-C_{RE}\lambda_{RE}(\alpha),

and an optimal approval policy is a maximizer $\alpha^*$ of $V$ over $[0,1]$ .

Formalization targets

Goal: Proposition 1 (p. 13)

The optimal approval policy $\alpha^*$ is

\text{(a) increasing in } Q_E,\ C_{AE},\ C_{RE},\ \mu_I,\ \mu_{AB};\qquad \text{(b) decreasing in } Q_I,\ C_{AI},\ \lambda,\ \mu_{CT};

\text{(c) increasing in } p \text{ and decreasing in } \mu_E \text{ if } \psi_E(\alpha^*)<1 .

Each clause compares two parameter vectors that differ in one parameter only.

Milestones

Concavity of the pieces (proof of Theorem 1): $\psi_E$ is concave and increasing in $\alpha$ , $\psi\mapsto K\psi/(1+\psi)$ is concave and increasing, so $\mathbb E[N_E(\alpha)]$ is concave.
Theorem 1, first part: $V$ is concave on $[0,1]$ .
Eq. (A.9): the closed form of $V'(\alpha)$ on $(0,1)$ .
Theorem 1, second part: $\alpha^*$ is unique and interior, and it satisfies the first-order condition

\alpha^*=1-\Phi\left(\frac{1}{\delta\sqrt{I_n}}\log\left(\frac{1-p}{p}\cdot\frac{C_{AI}+\mathrm{WTP}\,Q_I/\mu_I}{\mathrm{WTP}\,Q_E/(\mu_E(1+\psi_E(\alpha^*))^2)+C_{RE}+C_{AE}}\right)+\frac{\delta\sqrt{I_n}}{2}\right).

Eq. (A.8): $\partial\alpha^*/\partial x=-(\partial V'(\alpha^*)/\partial x)/(\partial V'(\alpha^*)/\partial\alpha)$ , with a negative denominator.
Eqs. (A.10)–(A.15): the signs of $\partial V'/\partial x$ for $Q_E, Q_I, C_{AE}, C_{AI}, C_{RE}, \mu_I$ .
Eqs. (A.16)–(A.18): $\tilde\lambda\,\partial V'/\partial\tilde\lambda\le0$ at the optimum.
Eqs. (A.19), (A.20): $\partial V'/\partial\mu_E$ and $\partial V'/\partial p$ , with their signs when $\psi_E<1$ .

Significance

Proposition 1 turns the model into policy statements. The approval bar should be lower for diseases with long trials (small $\mu_{CT}$ ), high attrition (large $\mu_{AB}$ ) or few compounds in development (small $\lambda$ ), and for drugs whose rejection is costly. It should be higher where ineffective drugs linger on the market (small $\mu_I$ ). Part (c) shows that the natural intuition fails in general: more promising candidates (larger $p$ ) and longer effective market lives (smaller $\mu_E$ ) call for more lenient approval only when the market for effective drugs is not crowded, $\psi_E(\alpha^*)<1$ . Figure 3 of the paper shows $\alpha^*$ decreasing in $p$ over most of the range when the condition fails. The paper's numerical study estimates $\alpha^*$ for many diseases, and these monotonicity properties are what make those estimates readable.

The result is proved in the paper; nothing here is open. No machine-checked version of Theorem 1 or Proposition 1 exists. A formalization needs to supply what the paper calls "direct computation" and "straightforward differentiation": the concavity of the Gaussian power curve, the interior first-order condition, and the implicit-function argument. The printed derivatives (A.19) and (A.20) drop positive factors, and the formal statements give the corrected derivatives.

Difficulty

The obvious argument is to differentiate the first-order condition. That needs $\alpha^*$ to be interior, unique and differentiable in each parameter, and the paper asserts all three without proof. Interiority depends on the behaviour of the power curve's slope $e^{\delta\sqrt{I_n}\Phi^{-1}(1-\alpha)-\delta^2 I_n/2}$ at the endpoints: it tends to $+\infty$ as $\alpha\to0$ and to $0$ as $\alpha\to1$ . That in turn needs facts about the normal quantile that Mathlib does not package.

For $\lambda$ , $\mu_{CT}$ and $\mu_{AB}$ , $\partial V'/\partial x$ has no sign at a general $\alpha$ . Its sign is known only at the optimum, through the first-order condition. A pointwise sign argument therefore does not work, and one has to argue along the optimal path. In part (c) the side condition is a condition at the optimum, so it must hold at every parameter value between the two being compared. Checking it at the two endpoints only does not give the monotonicity.

Formalization scope

All declarations live in the namespace FlexApproval.Statics. $\Phi$ and $\Phi^{-1}$ on $(0,1)$ are the published Cohen2019.Robust.Phi and PhiInvReal. A parameter vector is a structure of real fields plus $n, K\in\mathbb N$ . The model fixes the following conventions:

Standing assumptions. The paper never lists them, so the formalization adds them and every statement carries them: $0<p<1$ , $\delta>0$ , $\sigma>0$ , $n\ge1$ , positive rates, $K\ge1$ , $\mathrm{WTP}>0$ , $Q_E>0$ , $Q_I, C_{AE}, C_{AI}, C_{RE}\ge0$ , and $C_{AI}+\mathrm{WTP}\,Q_I/\mu_I>0$ . Without the last one the optimum is $\alpha=1$ and the logarithm in (5) is $\log 0$ .
Power curve at the endpoints. The power curve $\alpha\mapsto1-\Phi(\Phi^{-1}(1-\alpha)-\delta\sqrt{I_n})$ takes its limits $0$ and $1$ at $\alpha=0$ and $\alpha=1$ . This makes $V$ the continuous extension to $[0,1]$ .
Market means. The formulas for $\mathbb E[N_E]$ and $\mathbb E[N_I]$ are the paper's steady-state means of $K$ preemptive M/M/1/1 queues and an M/M/∞ queue. They are taken as definitions; their queueing derivation is out of scope.
Optimality and monotonicity. Optimality is a predicate (a maximizer over $[0,1]$ ), and the comparative statics hold for arbitrary maximizers. Monotonicity is weak.
Varying one parameter. "Differs only in $x$ " is a record update of one parameter vector.
Derivatives. $V'$ is Mathlib's deriv. Derivatives in a parameter are stated with HasDerivAt and an explicit value, never as a bare deriv sign, which would hold trivially wherever the derivative fails to exist. The derivative in $\tilde\lambda$ is taken through $\lambda$ , since $\lambda\,\partial/\partial\lambda=\tilde\lambda\,\partial/\partial\tilde\lambda$ .
Side condition in (c). It is required at every optimal policy for every parameter value in $[x_1,x_2]$ .

The optimal policy is never defined by the first-order condition (5). Doing so would make Theorem 1 a tautology and the comparative statics a statement about a formula. Every statement quantifies over maximizers of $V$ .

Useful infrastructure beyond this mission: smoothness and the endpoint limits of the normal quantile, concavity of Gaussian power curves (ROC curves of the equal-variance normal model), and a monotone comparative-statics lemma for strictly concave objectives. Proofs of individual milestones are welcome, and so are alternative routes to Proposition 1 that avoid the implicit function theorem.

Not formalized: Proposition 2 (ordering of $\alpha^*$ in $K$ ), Proposition 3 (monotonicity and diminishing increments of the optimal value in $K$ ), the queueing derivation of (4), and the numerical study of §5.

Selected references

F. Bravo, T. C. Corcoran, E. F. Long, Flexible Drug Approval Policies, Manufacturing & Service Operations Management 23(1), 2021. https://doi.org/10.1287/msom.2020.0963 (cited version: SSRN working paper 3027263, 17 Jul 2019, https://ssrn.com/abstract=3027263)
V. Montazerhodjat, S. E. Chaudhuri, D. J. Sargent, A. W. Lo, Use of Bayesian Decision Analysis to Minimize Harm in Patient-Centered Randomized Clinical Trials in Oncology, JAMA Oncology 3(9), 2017. https://doi.org/10.1001/jamaoncol.2017.0123

12 thms2 active usersReviewed

Actuarial Science Operations Research Probability·Captain: mikedeng1

Affine Storage and Insurance Risk Models: Closed Form for the Joint Transform of Ruin Time, Overshoot and Undershoot Before an Exponential Horizon from an Exponential Initial SurplusResearch Paper

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

15 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Negative Advertising and Competitive Positioning: When Negative Advertising Is Permitted, There Is an Equilibrium in Which the Entrant Co-Locates and Both Firms Prioritize Positive AdvertisingResearch Paper

Negative advertising and where products are placed

Negative advertising (comparative advertising that points to a rival's flaw) is used both in product markets and in political campaigns, and its regulation differs across jurisdictions: until the 1990s it was not permitted in numerous countries of the European Union (Anderson and Renault, 2009). Many models of advertising take the products' positions as given. Bostanci, Yildirim and Jerath (Management Science, 2023) ask what happens when a firm chooses its product position knowing which advertising war that position will invite. Their main finding, Proposition 2, is that permitting negative advertising can make an entrant give up differentiation: it places its product next to the incumbent's, and both firms then advertise positively.

The mechanism is a spillover effect: products positioned close together tend to share attributes, so revealing that the rival's product has a flaw also raises the probability that one's own product has it. Co-location therefore disarms negative advertising.

The model

There are two locations, $L$ and $R$ , each with a unit mass of consumers whose ideal product sits there. The incumbent (firm 1) is at $L$ ; the entrant (firm 2) chooses $x_2 \in \{L, R\}$ . A consumer at $\chi$ buying product $i$ at $x_i$ gets utility $U_{ij} = \gamma_j - |x_i - \chi| + A_i$ , where the distance is $0$ at the own location and $\delta > 0$ at the other, and the reservation value $\gamma_j$ is uniform on $[\underline\gamma, \bar\gamma]$ . Not buying gives $0$ .

Each product has a positive attribute $P_i$ , equal to $\Pi$ with probability $\sigma_\Pi$ and $0$ otherwise, and a negative attribute $N_i$ , equal to $-\beta$ with probability $\sigma_\beta$ and $0$ otherwise; $A_i = P_i + N_i$ . The normalization $\sigma_\Pi\Pi = \sigma_\beta\beta$ makes $E[A_i] = 0$ . Under co-location $\mathrm{cor}(P_1,P_2) = \mathrm{cor}(N_1,N_2) = \rho > 0$ ; apart, the attributes are independent.

The timeline: the entrant positions; nature draws the type profile $\theta = (P_1, P_2, N_1, N_2)$ , seen by the firms only; each firm simultaneously chooses $a_i \in \{P_i, N_{-i}, \varnothing\}$ (advertise its own positive attribute, advertise the rival's negative attribute, or nothing), truthfully; consumers update their beliefs by Bayes' rule and buy. The price is normalized to 1, so a firm's payoff is its demand. A perfect Bayesian equilibrium (PBE) consists of the entrant's location, advertising strategies at both locations, and consumer beliefs, such that consumers choose optimally, the ads form a Nash equilibrium of every advertising sub-game, the location maximizes the entrant's expected demand, and beliefs follow Bayes' rule.

A firm $-i$ is a weak opponent of $i$ if it cannot advertise ( $P_{-i} = 0$ and $N_i = 0$ ), and a strong opponent otherwise.

Formalization targets

Goal: Proposition 2 on the corrected region

Under the standing assumptions, Assumption 1′ ( $\underline\gamma < -\Pi$ , $\bar\gamma > \delta + \sigma_\Pi\Pi + (1-\sigma_\beta)\beta$ ), and

\beta > (1-\sigma_\Pi)\Pi + \delta,\quad \bar\gamma + \sigma_\beta\beta \ge (1-\sigma_\Pi)\Pi + \delta,\quad \Pi > (1-\rho)(1-\sigma_\beta)\beta,\quad \delta < \Pi + \sigma_\beta\beta,\quad \text{(A1d′)},

there is a PBE in which the entrant co-locates, every firm holding the positive attribute advertises it after co-location, and after locating apart a firm that can attack a strong opponent does so.

Milestones

Table 1: the Bayes posteriors $E[A_i], E[A_{-i}]$ after each advertising outcome of the proof's strategies, apart and under co-location.
Lemmas 1–4: the best advertising reply against weak and strong opponents, apart and co-located, each as an exact condition on the parameters.
(A5′), (A6′): the entrant's expected demand at each location in closed form.
Lemma 5′: the entrant co-locates if and only if (A1d′).

Significance

The result links two decisions usually studied separately. Positioning models predict differentiation to soften competition; Proposition 2 shows that when the advertising stage follows positioning, the entrant may prefer to co-locate, and that banning negative advertising (Proposition 1 of the paper) changes the positioning outcome. This bears on the regulation of comparative advertising and on the welfare comparisons of §4 of the paper.

The formalization produces a checked version of a result whose printed parameter region is wrong. The printed conditions are not sufficient: at $\delta = 1/2$ , $\Pi = \beta = 2$ , $\sigma_\Pi = \sigma_\beta = 1/2$ , $\rho = 1/4$ , $\underline\gamma = -3$ , $\bar\gamma = 7/2$ , every printed condition of the proof holds, yet the entrant earns $479/832$ by co-locating and $127/208$ by locating apart, so the described profile is not an equilibrium. The mission states the corrected theorem, and a machine-checked proof would settle that the corrected region is right. The result has not been formalized before.

Difficulty

The obvious argument fills in Table 1 and compares demands case by case, which is what the paper does; its slips sit in exactly that bookkeeping. Two places need care. First, demand is piecewise linear in the posteriors: whether a firm steals the rival's location depends on the sign of $E[A_i] - E[A_{-i}] - \delta$ , and ties are broken differently under co-location (equal split) and apart (closer product), so each lemma is a case analysis whose boundaries matter (Lemma 4's printed strict condition fails at its boundary). Second, the entrant's location payoff is an expectation over 16 type profiles under a correlated prior; the paper's two closed forms both carry errors, so the comparison has to be recomputed rather than copied. The goal then requires checking every advertising sub-game at both locations, including those off the equilibrium path.

Formalization scope

Everything is finite and real-valued; no measure theory is needed. Firms, locations and ads are small inductive types; a type profile is a pair of Boolean functions; the prior is the product of two correlated Bernoulli pairs. Consumer behaviour is built into the demand function: consumers choose the product with the larger posterior expected attribute minus distance, buy iff the reservation value is at least minus that maximum, and break ties as in footnote 11 of the paper. The uniform cdf is clipped to $[0,1]$ . Beliefs are probability mass functions on type profiles; the PBE definition requires Bayes' rule wherever the observed outcome has positive prior probability, and only consistency with the truthful ads elsewhere.

Corrections relative to the page, all disclosed in the item statements: $\underline\gamma < -\Pi$ in Assumption 1 (printed $\underline\gamma < \Pi$ ); the added condition $\delta < \Pi + \sigma_\beta\beta$ (the proof claims this region is excluded, but it is not, and there the profile fails); $\rho < 1$ ; (A5′), (A6′), (A1d′) in place of (A5), (A6), (A1d); and Lemma 4 with a weak inequality.

The goal is an existence statement over all profiles satisfying every PBE condition; beliefs are computed by Bayes' rule, not defined as Table 1's numbers, and demand comes from consumer choice, not from the paper's demand tables, so neither the table nor the closed forms hold by definition.

All definitions live in one file, NegAdPosition.CoLocate.Model. Proofs of the milestones in any order are welcome; Table 1 and the closed forms are mechanical but long, and reusable tactics for sums over the 16 type profiles would help every item.

Selected references

G. Bostanci, P. Yildirim, K. Jerath, Negative Advertising and Competitive Positioning, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4439 (cited from the authors' manuscript, November 2021).
S. P. Anderson, R. Renault, Comparative advertising: disclosing horizontal match information, RAND Journal of Economics 40(3), 558–581, 2009. https://doi.org/10.1111/j.1756-2171.2009.00080.x

11 thms2 active usersReviewed

Completed

Economics Mechanism Design·Captain: mikedeng1

Expectations-Based Loss Aversion in Auctions with Interdependent Values: Extensive vs. Intensive Risk: Under CPE, First-Price Revenue Exceeds Second-Price Revenue iff Bidders Are Loss-Averse in MoneyResearch Paper

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.

9 thms2 active usersReviewed

Algorithmic Game Theory Mechanism Design Probability·Captain: mikedeng1

Towards a Functional Fee Market for Cryptocurrencies: Truthful Bidding Is Not Dominant, but the Expected Gain from Strategic Bidding Converges to 0 as the Number of Users DivergesResearch Paper

Motivation

A cryptocurrency user can attach a fee to a transaction, and a miner can choose which waiting transactions enter the next block. When the most valuable waiting transactions compete for a limited number of places, the fee rule affects both the user's bid and the amount the user expects to pay. Basu, Easley, O'Hara and Sirer study a protocol that charges every included transaction the minimum included fee. This makes the fee visible from the block itself, but it also lets a bidder affect the price when that bidder supplies the lowest winning bid. Their Result 3 asks how much this incentive matters when many users are active. Basu et al., §4 and Result 3, pp. 13–16.

The result is a useful distinction for the design of a multi-unit fee auction. Truthful bidding can fail as an exact dominant strategy even while the maximum expected benefit from deviating becomes small in a large active market. The paper treats this as one part of a proposed fee mechanism; the claims about miner payments, fill penalties and longer-run blockchain behavior are separate from Result 3. Basu et al., §4, pp. 13–16.

Setting

A block has $K$ places for transactions. There are $m$ other active users besides the bidder being studied, with $m\ge K$ . Each user's value for inclusion in the current block and each allowed bid lie in $[0,\bar V]$ . The others' truthful bids form a vector $x=(x_j)_{j=1}^m$ . Write $V_k(x)$ for its $k$ th highest entry, counting repeated values. The rule places the $K$ highest bids in the block. A winning bidder pays the lowest of those bids. Basu et al., §3, pp. 10–11; §4, pp. 13–16.

For a bidder with value $v$ who bids $b$ , let $u_K(v,b;x)$ be the current-block payoff: value less the charged fee when included, and zero otherwise. A bid strictly above $V_K(x)$ wins; the bidder then pays $\min\{b,V_{K-1}(x)\}$ . A bid equal to $V_K(x)$ loses under the tie convention used here. The strategic gain is the best admissible payoff minus the payoff from bidding one's value,

G_{K,\bar V}(v;x)=\sup_{b\in[0,\bar V]}u_K(v,b;x)-u_K(v,v;x).

The model draws active users' values independently from a common continuous density $g$ on $[0,\bar V]$ , with $g(z)\ge\epsilon>0$ throughout that interval. Thus the joint law of $x$ is the product law of $m$ draws. A bidder knows their own value and the number of active users, but does not observe the other users' values or bids before choosing their own bid. The expected strategic gain therefore fixes the bid before averaging over the others' values $X$ :

\mathcal G_{K,\bar V}(v;m)=\sup_{b\in[0,\bar V]}\mathbb E[u_K(v,b;X)]-\mathbb E[u_K(v,v;X)].

Basu et al., §3, pp. 10–11.

Formalization targets

The goal is Result 3. Its first clause says that truthful bidding fails to be a dominant strategy: for every admissible number of other active users, there is a valid profile and an admissible deviation with higher current-block payoff. Its second clause concerns the expected strategic gain when the others bid truthfully:

\forall\eta>0\;\exists M\;\forall m\ge\max\{M,K\}\;\forall v\in[0,\bar V],\qquad |\mathcal G_{K,\bar V}(v;m)|\le\eta.

The quantifier over $v$ makes the convergence uniform across the bidder's possible values. It follows the paper's claim for “any bidder” and the value-independent upper bound stated immediately before Result 3. Basu et al., Result 3, p. 16; proof, pp. 21–22.

The milestone list records the statements in the paper's proof: an explicit profitable deviation when $V_{K-1}>V_K$ ; no profitable bid below the lower threshold; the two possible prices for a winning slot; the pointwise bound $G_{K,\bar V}(v;x)\le V_{K-1}(x)-V_K(x)$ ; the bound $\mathcal G_{K,\bar V}(v;m)\le\mathbb E[V_{K-1}(X)-V_K(X)]$ ; and the assertion that this expected spacing tends to zero as $m$ grows. These are intermediate targets, not replacements for the goal about strategic gain. Basu et al., proof of Result 3, pp. 21–22.

Significance

The theorem identifies what the mechanism does and does not guarantee for a user. It rules out an exact dominant-strategy interpretation of truthful bidding for the minimum included fee protocol, while bounding the incentive to depart from truthfulness in a sufficiently large active market. Without the first clause, a claim of truthfulness would be misleading; without the second, the protocol would lack the paper's quantitative reason to expect truthful behavior to be nearly optimal when participation is high. Basu et al., §4, p. 16.

The paper gives the mathematical result and an appendix argument. This mission asks for a machine-checked account of that result, including the auction payoff, the order statistics, and the probability statement; these claims are open Lean targets in the proposed mission, not already machine-checked results. The definitions of the finite order statistic and of gain from an admissible deviation can be reused in later multi-unit auction formalizations. The density and product-law interface may also support other bounded-support order-statistic results.

Difficulty

A pointwise payoff comparison is not by itself an asymptotic statement. The gain depends on the entire vector of other bids through two adjacent order statistics and on a supremum over all allowed bids. Turning its bound into a statement about expectations requires those random quantities to be measurable and integrable. The spacing between the $(K-1)$ st and $K$ th highest of $m$ draws then has to vanish in expectation for the stated class of densities. Merely showing that this spacing is nonnegative or at most $\bar V$ gives no decay with $m$ . Basu et al., proof of Result 3, p. 22.

There is also a boundary issue in the auction itself: a bid tied at the last included position requires a specified outcome. The protocol states the payment for included users but does not prescribe a complete deterministic tie rule for this one-bidder analysis. The chosen strict inclusion threshold makes every payoff a total function, and the continuous value law makes ties irrelevant to the expected-gain limit.

Formalization scope

Lean represents the other active users as Fin m → ℝ, their $k$ th highest value as a real supremum defining kthHighest, and their i.i.d. values as Measure.pi of a density law supported on $[0,\bar V]$ . The density assumption includes $0<\bar V$ , continuity on that interval, $g\ge\epsilon>0$ , and total integral one. The slots satisfy $2\le K\le m$ : $K=1$ has no $V_{K-1}$ and the fee rule becomes a first-price case. The index $m$ is the number of other active users; the convergence is conditional on that count, matching the model's statement that bidders know how many users are active. Basu et al., §3, p. 11; Result 3, p. 16.

Bids range over $[0,\bar V]$ . The gain is computed from the protocol payoff by a supremum over that interval; it is not defined as the adjacent order-statistic spacing or as a closed expression for the optimum. The expected gain takes the supremum over bids of expected payoffs, not the expectation of the pointwise supremum, since a bidder cannot condition a bid on the others' bids. The theorem explicitly requires integrability of the payoff of every admissible bid, so the real-valued integral cannot acquire meaning from Lean's default value for a non-integrable function. The first clause uses a concrete admissible bid profile; the second uses the product law of truthful others. The participation probability $\delta$ , the total potential user count $N$ , miner rewards, and the multi-block averaging parameter $B$ do not enter this conditional one-block claim. Basu et al., §3–§4, pp. 10–16.

The development needs finite order statistics, a measurable payoff and gain, probability laws from continuous densities, and integrability and convergence of adjacent order-statistic spacings. Contributions that establish those interfaces or prove the quoted intermediate claims serve the stated goal directly.

Selected references

S. Basu, D. Easley, M. O'Hara and E. G. Sirer, Towards a Functional Fee Market for Cryptocurrencies, arXiv preprint arXiv:1901.06830v1, 2019, §§3–4 and Result 3, pp. 10–16; appendix proof, pp. 21–22. Preprint.

8 thms2 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

Over-Conservativeness of Variance-Based Efficiency Criteria and Probabilistic Efficiency in Rare-Event Simulation: Most Significant Dominating Points Suffice for Strong Probabilistic EfficiencyResearch Paper

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

12 thms2 active usersReviewed

Completed

Control Theory Economics Operations Research·Captain: mikedeng1

Market Making and Incentives Design in the Presence of a Dark Pool: Existence and Uniqueness of the Continuous Viscosity Solution of the Exchange's HJB EquationResearch Paper

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:

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.
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$ .
$0\in\mathcal V^l,\mathcal V^d$ , so a best response always exists.
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$ .
$\mathcal H$ is valued in the extended reals.
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$ .
The goal holds for every best-response selection, not for one specific selection.
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

3 thms2 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Optimally Scheduling Heterogeneous Impatient Customers: The Fluid-Optimal Schedule Splits at Most One Customer Class into Two SubclassesResearch Paper

Motivation

Call centers and other many-server service systems serve several classes of customers, each with its own service-time distribution, patience distribution and cost of waiting or abandoning. A customer who waits longer than its patience time abandons. The system manager decides, whenever an agent becomes free, which class to serve and which customer inside that class to serve.

Classical scheduling rules for such systems, such as the $c\mu/\theta$ rule of Atar, Giat and Shimkin (2010) and the generalized rule of Long, Shimkin, Zhang and Zhang (2020), serve customers of the same class first-come, first-served (FCFS). Bassamboo and Randhawa (2015, published in Management Science 2016) showed that FCFS within a class is suboptimal when patience times are not exponential: as a customer waits, the conditional distribution of its residual patience changes, and serving by time in queue can reduce cost. Their fluid analysis showed that a single class should be split into at most two FCFS subclasses.

Bassamboo, Randhawa and Wu (Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1190) combine the two decisions, across classes and within a class, in one fluid optimization problem. Their structural result is that the fluid-optimal schedule needs within-class differentiation for at most one class; every other class is served FCFS. This is the basis of their "mostly-FCFS" policy. This mission formalizes that result together with the two lemmas stated before it.

Setting

There are $m$ classes $i = 1, \dots, m$ and a total capacity of $N$ agents. Class $i$ arrives at rate $\Lambda_i > 0$ , has mean service time $1/\mu_i$ with $\mu_i > 0$ , and its patience time has distribution $F_i$ with survival function $\bar F_i = 1 - F_i$ . The offered wait $w \in [0, \infty]$ of a customer is the time it would wait before service if it were infinitely patient; $w = \infty$ means the customer is never served. A customer offered wait $w$ incurs an average cost $\bar c_i(w)$ , obtained in the paper by integrating a cost $\xi_i(x, y, w)$ over service time $x$ and patience $y$ (display (5)).

In the fluid model, class $i$ receives capacity $n_i \ge 0$ and is divided into $J(i) \ge 1$ subclasses, each served FCFS. Subclass $j$ has arrival rate $\lambda_{i,j} \ge 0$ , offered wait $w_{i,j}$ and capacity $n_{i,j} \ge 0$ . The within-class program (6) defines the class cost function

C_i(n_i) = \inf \sum_{j=1}^{J(i)} \lambda_{i,j}\,\bar c_i(w_{i,j}) \quad\text{s.t.}\quad \sum_{j=1}^{J(i)} \lambda_{i,j} = \Lambda_i,\quad \lambda_{i,j}\,\bar F_i(w_{i,j}) \le n_{i,j}\,\mu_i,\quad \sum_{j=1}^{J(i)} n_{i,j} \le n_i ,

the infimum ranging over $J(i)$ and all subclass rates, waits and capacities. The middle constraint says that the rate of customers of subclass $j$ who remain patient long enough to reach service does not exceed the subclass's service rate. The across-class program (2) is

\min_{n:\ \sum_i n_i \le N}\ \sum_{i=1}^m C_i(n_i).

A plan is a choice of capacities $n_i$ and, for each class, a subclass configuration feasible for (6) at $n_i$ ; a fluid-optimal solution is a feasible plan of least total cost $\sum_i \sum_j \lambda_{i,j}\,\bar c_i(w_{i,j})$ .

Formalization targets

Goal: Proposition 1 (p. 1071)

The fluid-optimal solution to (2) with $C_i$ defined in (6) splits the $m$ classes into at most $m+1$ subclasses; in particular $J(i) > 1$ for at most one class $i$ , and for this class $J(i) = 2$ . Formally: every feasible plan is weakly improved by a feasible plan $Q$ with

\sum_{i=1}^m J_Q(i) \le m + 1,\qquad J_Q(i) > 1 \text{ for at most one } i,\qquad J_Q(i) > 1 \implies J_Q(i) = 2 .

Milestones

Lemma 1 (p. 1070): the optimal number of subclasses in (6) satisfies $J^*(i) \le 2$ ; every feasible configuration of (6) is weakly improved by a feasible configuration with at most two subclasses.
Lemma 2, first sentence (p. 1071): the cost function $C_i$ is nonincreasing and convex on $[0, \infty)$ .

Significance

Proposition 1 is what makes the paper's policy simple. Lemma 1 alone would permit every class to be split in two, giving up to $2m$ FCFS queues with their own priority rules; Proposition 1 says that one non-FCFS class suffices, so a fluid-optimal schedule can be implemented as a priority ordering of classes with time-in-queue differentiation in at most one of them. Combined with Lemma 2, which makes (2) a convex allocation problem, it underlies the index-based characterization of the optimum in Proposition 2 and the mostly-FCFS and multi-class time-in-queue policies of §4.

The paper's proofs are in an online appendix that this mission does not use. To our knowledge none of the three results has a machine-checked proof. The formal development provides a reusable encoding of the fluid model of a multi-class queue with abandonment, with offered waits that may be infinite, and a checked version of the sparsity statement underlying the mostly-FCFS policy.

Difficulty

The program (6) has an unbounded number of subclasses, offered waits drawn from $[0, \infty]$ , and arbitrary cost and survival functions, so the feasible set is not a fixed finite-dimensional polytope and the infimum need not be attained. Lemma 1 for each class separately does not give Proposition 1: splitting each class into two subclasses is consistent with Lemma 1 and violates Proposition 1. The bound in Proposition 1 depends on capacity being free to move between classes, with only the total budget $\sum_i n_i \le N$ shared; with each $n_i$ held fixed the claim fails. The statements must also respect the never-served subclass $w = \infty$ , which the paper uses to represent LCFS as the offered-wait vector $(0, \infty)$ .

Formalization scope

Everything lives in the namespace HetImpatient.FluidSplit, in one definitions file HetImpatient.FluidSplit.Model and three theorem items.

Classes are Fin m; a class configuration carries its own number of subclasses J : ℕ, with subclasses Fin J, and feasibility requires J ≥ 1. The number of subclasses is otherwise unbounded.
Offered waits are in ℝ≥0∞, so $w = \infty$ is allowed. Rates, capacities and costs are real numbers.
The cost $\bar c_i$ is an arbitrary function of the offered wait. Display (5) defines it from $\xi_i$ , $G_i$ , $F_i$ , but every function of $w$ arises that way, so this is the generality of (5). $\bar F_i$ and $\bar c_i$ are independent data.
Standing assumptions, written out as one predicate: $\Lambda_i > 0$ , $\mu_i > 0$ , $0 \le \bar F_i \le 1$ , $\bar F_i$ nonincreasing, $\bar F_i(\infty) = 0$ (a finite patience time). Nonnegativity $\lambda_{i,j}, n_{i,j} \ge 0$ is part of feasibility. Nonnegative costs $\bar c_i \ge 0$ are a separate hypothesis used only by Lemma 2.
The two-stage program (2)+(6) is encoded as one joint program over plans. A plan is optimal for the joint program exactly when its capacities are optimal in (2) and each class configuration is optimal in (6), whenever these optima exist.
"The fluid-optimal solution has property $P$ " is read in reduction form: every feasible plan (or configuration) is weakly improved by a feasible one with property $P$ . Applied to an optimal solution, this gives an optimal solution with property $P$ . It does not assert that every optimum has the property, which fails when costs tie; the paper itself notes that optima can be multiple.
$C_i$ is a real infimum; Lemma 2 is posed on $[0, \infty)$ , where the feasible set is nonempty, under $\bar c_i \ge 0$ , where it is bounded below.
The second sentence of Lemma 2 (differentiability of $C_i$ for $n < \Lambda_i/\mu_i$ ) and Proposition 2 onwards are not formalized.

A statement that drops the comparison of costs, or builds "at most two subclasses" into the definition of feasibility, is trivial and is not what is formalized here: the improved plan must be feasible and no more costly, and feasibility permits any number of subclasses (a sanity check confirms that a plan splitting two classes is feasible).

Welcome contributions: proofs of Lemma 1, Lemma 2 and Proposition 1, and supporting lemmas about subclass configurations stated for this model.

Selected references

A. Bassamboo, R. Randhawa, C. (A.) Wu, Optimally scheduling heterogeneous impatient customers, Manufacturing & Service Operations Management 25(3):1066–1080, 2023. https://doi.org/10.1287/msom.2023.1190
A. Bassamboo, R. S. Randhawa, Scheduling homogeneous impatient customers, Management Science 62(7):2129–2147, 2016 (cited in the paper as 2015).
R. Atar, C. Giat, N. Shimkin, The cµ/θ rule for many-server queues with abandonment, Operations Research 58(5):1427–1439, 2010.
Z. Long, N. Shimkin, H. Zhang, J. Zhang, Dynamic scheduling of multiclass many-server queues with abandonment: The generalized cµ/h rule, Operations Research 68(4):1218–1230, 2020.

4 thms2 active usersReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Testing, Voluntary Social Distancing, and the Spread of an Infection: Greater Testing Raises the Equilibrium Infection Probability of the Type That Mixes Its Social ActivityResearch Paper

Why testing can raise infections

Testing makes an infected person less likely to pass an infection to someone else. In a society whose contacts depend on voluntary social activity, that direct benefit changes behavior: an agent who expects fewer infections may choose more contacts. The central question is whether the added contacts can outweigh the direct benefit of testing in equilibrium. Acemoglu, Makhdoumi, Malekian, and Ozdaglar study this question in a finite random network with two values for social interaction NBER Working Paper 27483. The paper later appeared in Operations Research in 2024; the mathematical statements in this mission follow the July 2020 NBER working paper, whose numbering and page locations are used throughout.

The effect matters when testing policy and voluntary distancing operate together. A prediction made with fixed contact patterns can have the opposite direction from a prediction made after agents adjust their activity. The result targets this difference directly: in two policy regions the equilibrium infection probability of the agents who mix between activity and inactivity rises with more testing, even though infection probability at a fixed activity profile falls NBER Working Paper 27483, Proposition 1 and Theorem 1.

The activity and infection model

There are $n$ agents. Agent $i$ chooses an activity $x_i\in[0,1]$ , valued at either $v_L$ or $v_H$ , where $0\le v_L<v_H\le1$ . A fixed fraction $r_H\in(0,1)$ of agents is designated high value. Conditional on the activities, each unordered pair $\{i,j\}$ forms a contact independently with probability $\eta x_i x_j$ , with $\eta\in(0,1]$ . One agent is chosen uniformly as the initial infection source. Each infected agent is tested with a probability determined by her type: $\alpha_L$ for low value and $\alpha_H$ for high value. Untested agents transmit across each contact with probability $\beta\in(0,1]$ ; tested agents transmit with probability $\beta p$ , where $p\in[0,1)$ NBER Working Paper 27483, Section 2.

Write $P_i^{\mathrm{inf}}(G,\alpha_L,\alpha_H)$ for the chance that infection reaches $i$ on a fixed contact graph $G$ , after averaging over the source, testing, and transmissions. Averaging again over the random graph formed by an activity profile $x$ gives $P_i^{\mathrm{inf}}(x,\alpha_L,\alpha_H)$ . These are distinct probabilities: the first holds contacts fixed and the second includes how activity changes the contact network. An agent's utility is

u_i(x,\alpha_L,\alpha_H)=v_i x_i-P_i^{\mathrm{inf}}(x,\alpha_L,\alpha_H)-c\alpha_i,

where $c>0$ and $\alpha_i$ is her type's testing probability. A symmetric equilibrium assigns one activity distribution to each type and permits no agent to gain by choosing any other activity in $[0,1]$ NBER Working Paper 27483, equation (1) and Definition 3.

The testing square $[0,1]^2$ is partitioned, with shared boundaries, into four regions $A_1,A_2,A_3,A_4$ by comparisons of infection probabilities at all-active and partially active profiles with the thresholds $v_L+1/n$ and $v_H+1/n$ . In $A_1$ both types are active. In $A_2$ high-value agents are active and low-value agents mix. In $A_3$ only high-value agents are active. In $A_4$ high-value agents mix and low-value agents are inactive NBER Working Paper 27483, Section 3.1 and Proposition 2.

Formalization targets

The goal is the finite-population comparative statics in Theorem 1. For sufficiently large $n$ , compare coordinatewise ordered policies $\alpha\le\alpha'$ in the interior of the same region, and their symmetric equilibria. The target includes existence of an equilibrium for every policy. In the two pure-activity regions, infection weakly falls:

\alpha,\alpha'\in\operatorname{int}(A_1)\text{ or }\operatorname{int}(A_3) \quad\Longrightarrow\quad P_i^{\mathrm{eq}}(\alpha')\le P_i^{\mathrm{eq}}(\alpha).

In the mixing regions, the mixing type's infection probability rises. For $A_2$ , the increase is strict for distinct ordered policies; for $A_4$ , it is strict when the high-type testing probability increases. The inactive low-value agents in $A_4$ have infection probability $1/n$ at both policies:

\begin{aligned} \alpha,\alpha'\in\operatorname{int}(A_2),\ \alpha<\alpha' &\Longrightarrow P_l^{\mathrm{eq}}(\alpha)<P_l^{\mathrm{eq}}(\alpha'),\\ \alpha,\alpha'\in\operatorname{int}(A_4),\ \alpha_H<\alpha'_H &\Longrightarrow P_h^{\mathrm{eq}}(\alpha)<P_h^{\mathrm{eq}}(\alpha'). \end{aligned}

The target also includes the theorem's closing sentence: at policies on the boundaries of the four regions, equilibrium infection probabilities are continuous in the policy.

The milestone list follows the paper's activity monotonicity and concavity result, fixed-network testing result, endpoint best responses, four-region equilibrium characterization, and the mixing indifference equations (9) and (10) NBER Working Paper 27483, Lemmas 1–2, Propositions 1–2, Theorem 1.

What the result establishes

The theorem gives a precise setting in which the direct effect of testing and the equilibrium effect of changed contacts have different signs. It distinguishes the regions where everyone or no one of a type changes activity from the regions where a type mixes. Thus a policy comparison can specify whose infection probability rises, falls, or stays at the source-infection floor $1/n$ , rather than claiming one direction for every agent and policy NBER Working Paper 27483, Theorem 1.

The paper presents proofs of these claims, but this mission's Lean theorems remain open. A completed formalization would provide a reusable finite independent-cascade model with shared testing coins, a random activity-dependent contact network, and equilibrium predicates that compare against all unilateral activities. Those definitions can support later work on intervention and network-formation games. The formalization also makes the finite-population qualifications explicit, including the signs of the mixing-type infection identities.

Main mathematical difficulty

Testing monotonicity on a fixed network does not settle the equilibrium comparison, because the contact graph's law changes when agents change activity. The difficult step is the uniform, large-population equilibrium characterization in Proposition 2: the paper needs a single threshold $M$ that works across all policies and keeps the two types' incentives separated. Its proof asserts a bound on the effect of one agent's choice on another's infection probability for large $n$ without a quantitative derivation NBER Working Paper 27483, proof of Proposition 2. This is a substantive open proof obligation for solvers, not a condition assumed in the theorem.

Formalization scope

Lean uses Fin n for agents and SimpleGraph (Fin n) for undirected contacts. All probabilities are finite sums of Bernoulli weights. A single testing coin per agent is shared by that agent's outgoing transmission arcs; ordered arcs have independent transmission coins. Infection means reflexive reachability from the uniformly selected source in the resulting live-arc graph, so even an isolated inactive agent can be infected as the source. The activity-dependent graph draws one coin per unordered pair. This is the paper's stochastic process in finite form NBER Working Paper 27483, Section 2 and proof of Proposition 1.

The high-value agents are the first $\lceil r_H n\rceil$ members of Fin n. Policies and typewise strategies are real pairs ordered low then high. Symmetric mixed strategies are independent Bernoulli mixtures on activities $\{0,1\}$ , as in the proof of Proposition 2; deviations still range over every real activity in $[0,1]$ . Region interiors are taken in $\mathbb R^2$ . The source's weak direction is used for decreases; the strict increases are restricted to policy changes that affect the mixing type. The printed high-type constancy claim in Theorem 1(b) is false in the finite model and is excluded. Two printed statements fail at degenerate inputs and are stated in corrected form. Lemma 2's claim that every best response is $0$ or $1$ fails when utility is constant in the agent's own activity, so that case is the stated exception. Proposition 2's uniqueness fails at the corner $p=0$ , $\alpha_L=1$ , where low-value agents never transmit and every low-type mixing probability can be an equilibrium. That corner is excluded from parts (a)–(c) and from the continuity clause of Theorem 1. The paper's displayed formulas $\gamma_Tv_T-1/n$ are corrected to $\gamma_Tv_T+1/n$ , as their preceding lines require NBER Working Paper 27483, pp. 37–38.

The infection probability is defined by the cascade itself, and equilibrium is checked against every unilateral deviation. The goal includes equilibrium existence so that a universal claim over equilibria cannot hold vacuously. The definitions, finite-sum facts, and equilibrium results are welcome contributions; no closed-form infection probability is built into the model.

Selected references

Daron Acemoglu, Ali Makhdoumi, Azarakhsh Malekian, and Asuman Ozdaglar, Testing, Voluntary Social Distancing, and the Spread of an Infection, NBER Working Paper 27483, 2020. Working paper.
Daron Acemoglu, Ali Makhdoumi, Azarakhsh Malekian, and Asuman Ozdaglar, Testing, Voluntary Social Distancing, and the Spread of an Infection, Operations Research, 2024. DOI. The mission cites the working paper's statements and page numbers.

14 thms2 active usersReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Extended Producer Responsibility for Pharmaceuticals: End-of-Pipe Control Maximizes Total Welfare for Medicines with High Health Benefit, High Collection Cost and High Environmental DisutilityResearch Paper

Motivation

Unused prescription medicines create disposal and public health costs, while a patient may use less medicine than a doctor prescribes. A regulator can make the pharmaceutical producer collect unused medicine, or charge a fee on dispensed medicine and use the proceeds to fund collection. These two policies charge the producer for different quantities. Alev, Atasu, Toktay and Zhang study how that distinction affects a producer's incentives to influence prescriptions and the regulator's choice of policy. The question matters when regulation changes both the amount prescribed and the share of unused medicine collected.

Setting

A patient has a need level $\theta_n$ and a preferred use level $\theta_u$ . They are independent and uniform on $[0,1]$ . The producer chooses a medicine price $p$ and two promotional effort levels, $\eta_d$ directed at the doctor and $\eta_p$ directed at the patient. Both efforts lie in $[0,1]$ . The doctor chooses a prescription $q_p\in[\theta_n,1]$ to maximize

U_d(q_p)=u_p\theta_n-pq_p+\eta_dq_p-o_d(1-\eta_p)(q_p-\theta_n).

Here $u_p$ is the unit health benefit and $o_d$ is the doctor's reputational cost per unit of over-prescription. At indifference the model selects $q_p=1$ . The amount used is $q_u=\min\{\theta_u,q_p\}$ ; the remaining $q_p-q_u$ is unused. These choices and the tie convention reproduce the doctor's rule in Lemma 1, p. 15.

Under end-of-pipe control (EC), the planner sets a collection rate $r_{EC}\in[0,1]$ . The producer pays unit cost $k$ to collect that fraction of unused medicine. Under source reduction (SR), the planner charges the producer a fee $t\ge0$ for each dispensed unit and collects unused medicine at rate $r_{SR}\in[0,1]$ . The SR planner must fund collection without a deficit. For either policy, the producer maximizes expected revenue minus the quadratic promotion costs $\alpha\eta_d^2+\beta\eta_p^2$ and its policy cost. The doctor must receive nonnegative utility for every need level.

The planner evaluates expected doctor utility, producer profit, and planner surplus, then subtracts two harms. Environmental disutility is $\epsilon_e[q_u+(1-r)(q_p-q_u)]$ ; social disutility from uncollected unused medicine is $\epsilon_s(1-r)(q_p-q_u)$ . The resulting expected total welfare $W$ is maximized subject to the collection, fee, producer participation, and no-deficit constraints. The planner may choose among producer actions tied for maximal profit. The full primitives and constraints are those of Section 3, pp. 8–14.

Formalization targets

The producer thresholds in the appendix's stated regime are

\bar u_p^{EC}=\frac{4\alpha-2\beta-1}{3},\qquad \bar u_p^{SR}=\alpha-\beta,\qquad \bar k(u_p)=\frac{3(1-2\beta-u_p)}{2}.

Write $W^{EC}_*$ and $W^{SR}_*$ for the attained maximum welfare values under the two policies. Proposition 4 and Table 2, pp. 17–18, give the mission's goal: the models tie for $u_p<\bar u_p^{EC}$ ; they tie when $\bar u_p^{EC}\le u_p<\bar u_p^{SR}$ and $k<\bar k$ ; SR weakly wins when $u_p\ge\bar u_p^{SR}$ and $k<\bar k$ . When $u_p\ge\bar u_p^{EC}$ and $k\ge\bar k$ , a threshold $\tilde\epsilon_e$ divides SR's weak advantage below it from EC's weak advantage above it. Above that threshold, an EC welfare optimum eliminates over-prescription, encoding the paper's requirement $\tilde\epsilon_e\ge\bar\epsilon_e^{EC}$ .

The milestones cover the doctor's prescription rule, the producer's optimal profit in each prescription region, the health-benefit and collection-cost thresholds, the EC environmental threshold, and the appendix's SR replication claim. Together these are the named results and displayed steps used by the paper's welfare comparison.

Significance

The result identifies when a fee on every dispensed unit can match or improve a direct collection obligation, and when the direct obligation can weakly improve welfare because it acts on unused medicine. Its threshold form connects a medicine's health benefit and the cost and harm of its disposal to the preferred regulatory instrument. The comparison also separates the ability to discourage over-prescription from the value of doing so: a policy may allow its elimination without making it welfare maximizing.

The paper proves these claims analytically in its stated appendix regime; this mission asks for machine-checked proofs of the game model, equilibrium welfare comparisons, and threshold results. The proposed Lean theorems are currently open. The model definitions are reusable for the paper's producer-preference and advocacy results, which are outside this mission.

Difficulty

Comparing the two policies at a fixed prescription quantity misses the producer's response. Changing a collection rate or unit fee changes the producer's optimal price and promotion, which can switch the doctor's choice between prescribing need and over-prescribing. The planner must also respect producer participation, and SR must cover its collection costs. The welfare comparison therefore requires the feasible equilibria in both prescription regions and careful treatment of ties at the switching boundary. The online appendix, pp. 1–5, records the relevant region calculations.

Formalization scope

Lean represents all parameters, actions, and policies by real numbers. It computes expectations by iterated interval integrals over independent uniform $\theta_n,\theta_u\in[0,1]$ . The prescription response, producer profit, planner surplus, disutilities, and welfare are defined from the Section 3 formulas. Welfare is the supremum over feasible planner policies and producer optima, with attainment asserted in the goal. The model never defines welfare by an appendix closed form, and the three named thresholds are fixed to the appendix formulas rather than left as free witnesses. The environmental threshold must also lead to an EC optimum without over-prescription, so an empty or arbitrary switch does not satisfy the intended claim.

The goal states the appendix's $0<\alpha<1/4$ , $0<\beta<o_d/2$ , and $\alpha+\beta\le1$ regime, together with $u_p\ge0$ , $k>0$ , and nonnegative disutilities. The restriction $\alpha+\beta\le1$ is the appendix's nonnegative-profit convention. In this regime $\bar u_p^{EC}<0$ , so the first column of Table 2 has no instance with $u_p\ge0$ ; it remains stated because it belongs to the printed table. Proposition 1's strict ordering of health-benefit thresholds requires $\alpha+\beta<1$ , a disclosed strengthening of that milestone's premise. The doctor's tie goes to over-prescription; the planner can select among producer optima; price $p$ has no sign restriction. EC uses only its collection rate, so the unused fee field of the shared policy record has no effect. The participation condition is pointwise in need. The SR half of Proposition 3, later propositions, numerical study, and regimes outside the printed proof are outside this mission.

Selected references

I. Alev, A. Atasu, L. B. Toktay, and C. Zhang, Extended Producer Responsibility for Pharmaceuticals, SSRN 2693169, 2020 posting. SSRN.
I. Alev, A. Atasu, L. B. Toktay, and C. Zhang, Extended Producer Responsibility for Pharmaceuticals, Manufacturing & Service Operations Management, 2022. DOI. The mission's page numbers refer to the SSRN posting above.

17 thms2 active users

Completed

Probability Statistics Theoretical Computer Science·Captain: mikedeng1

Local Density Estimation in High Dimensions: LSH Count Is a (1 ± ε)-Approximation to the Number of Points Within Angle 𝒜 of the Query, with Probability 1 − δResearch Paper

Motivation

Many tasks on high-dimensional data ask not for the nearest neighbours of a query but for how many data points lie close to it. Density estimates of this kind feed outlier detection, kernel density estimation, classification by neighbourhood counts, and the tuning of nearest-neighbour search itself. Exact counting needs a scan of the whole dataset for every query, and uniform random sampling needs about $n/|\mathcal A_q|$ samples per unit of relative accuracy, which is prohibitive when the neighbourhood $\mathcal A_q$ is a tiny fraction of the $n$ points.

Locality-sensitive hashing (LSH) is the standard tool for finding near neighbours in sublinear time: a random hash function sends nearby points to the same bucket with higher probability than distant ones (Indyk–Motwani 1998; for angles, the random-hyperplane family of Charikar 2002). Wu, Charikar and Natchu (arXiv:1809.07471; Mathematics of Operations Research, 2022) turn LSH tables into a counting device. Their estimator LSH Count samples from the buckets near the query and corrects the bias of hashing by importance weighting, so that the number of samples depends on how well the hash concentrates the neighbourhood rather than on $n/|\mathcal A_q|$ .

Setting

The dataset $\mathcal D$ consists of unit vectors $v_1,\dots,v_n\in\mathbb R^d$ , and the query $q\in\mathbb R^d$ is a unit vector. For a set $\mathcal A$ of angles, the neighbourhood is

\mathcal A_q=\{\,i:\theta_{qv_i}\in\mathcal A\,\},\qquad \theta_{qx}=\arccos(q\cdot x),

and the target is its size $|\mathcal A_q|$ .

A table is built from a random hash function $g:\mathbb R^d\to\{0,1\}^t$ , which stores $v_i$ in the bucket $g(v_i)$ . For a set $\mathcal I$ of Hamming distances, $\mathcal B^k_q(\mathcal I)$ is the set of points of table $k$ whose bucket is at a Hamming distance in $\mathcal I$ from the query's bucket $g_k(q)$ , and $C^k_q(\mathcal I)$ is their number. The collision probabilities are

p(x)=\mathbb P\big(x\in\mathcal B_q(\mathcal I)\big),\qquad p(x,y)=\mathbb P\big(x\in\mathcal B_q(\mathcal I),\ y\in\mathcal B_q(\mathcal I)\big)

for one random table, $p_{\min}=\min_{x\in\mathcal A_q}p(x)$ , and $\mathbb E(C_q(\mathcal I))=\sum_{y\in\mathcal D}p(y)$ is the expected pool size of one table.

LSH Count with parameters $K,S,M$ :

Build $K$ independent tables.
Draw $S$ samples, independently and with replacement, uniformly from the pool: the multiset of pairs $(k,x)$ with $x\in\mathcal B^k_q(\mathcal I)$ .
Give a sample $(k,x)$ the weight $Z=\sum_{k}C^k_q(\mathcal I)\big/\big(K\,p(x)\big)$ if $x\in\mathcal A_q$ , and $Z=0$ otherwise, as in (2). The estimate is $E=\frac1S\sum_{i=1}^S Z_i$ .
Repeat $M$ times independently, with fresh tables and samples, and report the median of $E_1,\dots,E_M$ .

The table bias $W=\frac1K\sum_k\sum_{x\in\mathcal A_q}\mathbb 1(x\in\mathcal B^k_q(\mathcal I))/p(x)$ is the mean of $Z$ given the tables.

Formalization targets

Goal: Theorem 1, with the constants of its proof

For $\varepsilon>0$ and $0<\delta<1$ , if

K\ge\frac{8}{\varepsilon^2p_{\min}},\qquad S\ge\frac{8(1+\varepsilon^2)\,\mathbb E(C_q(\mathcal I))}{\varepsilon^2|\mathcal A_q|\,p_{\min}},\qquad M\ge11\ln\frac1\delta,

then

\mathbb P\Big(\big|\operatorname{median}(E_1,\dots,E_M)-|\mathcal A_q|\big|\le\varepsilon|\mathcal A_q|\Big)\ge1-\delta .

This uses $MK$ tables and $MS$ samples in total, the $O(\cdot)$ of the printed Theorem 1 (p. 6).

Milestones, in the order of the proof

Lemma 1 (p. 10): $\mathbb E(Z\mid\text{tables})=W$ and $\mathbb E(W)=\mathbb E(Z)=|\mathcal A_q|$ .
Lemma 2 (p. 10): $\sigma^2(W)=\frac1K\sum_{x,y\in\mathcal A_q}\big(\frac{p(x,y)}{p(x)p(y)}-1\big)$ .
Lemma 3 (p. 11): $K\ge 8/(\varepsilon^2p_{\min})$ gives $\sigma^2(W)\le\varepsilon^2|\mathcal A_q|^2/8$ , so $W$ is within $\varepsilon|\mathcal A_q|$ of $|\mathcal A_q|$ with probability $7/8$ .
Lemma 4 (p. 14): $\mathbb E[(E-|\mathcal A_q|)^2]\le\mathbb E[Z^2]/S+\sigma^2(W)$ .
Lemma 5 (p. 15): $\mathbb E[Z^2]=\sum_{x\in\mathcal A_q}\sum_{y\in\mathcal D}\big[\frac{p(x,y)}{Kp(x)^2}+(1-\frac1K)\frac{p(y)}{p(x)}\big]$ .
Lemma 6 (p. 16): under the bounds on $K$ and $S$ , $\mathbb E[Z^2]/S\le\varepsilon^2|\mathcal A_q|^2/8$ .
§5, p. 16: one estimator fails, $|E-|\mathcal A_q||\ge\varepsilon|\mathcal A_q|$ , with probability at most $1/4$ .
§5, pp. 15–16: if the median fails, at least half of the $E_m$ fail.
§5, p. 16: for $M$ independent failure events of probability at most $1/4$ , $\mathbb P(F\ge M/2)\le e^{-(2\ln2-1)M/4}\le e^{-M/11}$ .

Significance

Theorem 1 bounds the cost of counting near neighbours with LSH: the sample complexity $\mathbb E(C_q(\mathcal I))/(\varepsilon^2|\mathcal A_q|p_{\min})\cdot\log(1/\delta)$ replaces the ratio $n/|\mathcal A_q|$ of uniform sampling by the ratio of the expected pool size to the expected number of neighbours in the pool. When the hash concentrates the neighbourhood, this is a large saving, and the number of tables depends only on $p_{\min}$ and $\varepsilon$ . The same template (importance weights from known inclusion probabilities, a variance split into a sampling term and a design term, median of means) recurs in randomized estimation; Lemma 4's decomposition is the step that makes the two sources of error separately controllable.

The result is proved on paper. No machine-checked proof of it, or of any LSH-based estimator, is known. The mission produces a formal proof with explicit constants. Theorem 1 is printed with $O(\cdot)$ ; the constants here are the ones its proof determines, and one of them corrects the printed proof: the final display of Lemma 6 (p. 17) drops a factor $8$ that its own target inequality needs. The mission also produces reusable, generic pieces: the deterministic median lemma and a Chernoff bound for independent events with probability at most $1/4$ .

Difficulty

The arithmetic of each lemma is short; the difficulty is the probability model. The samples are not independent of the tables: their law is uniform on a random pool whose size is itself random, and the weight $Z$ divides by that size. Unconditional moments therefore require conditioning on the tables and then averaging over them, and the cross terms in Lemmas 2 and 5 separate a single table $k$ from pairs of distinct tables $k\ne l$ . A tempting simplification samples uniformly from the set of distinct points in the probed buckets; it makes Lemma 1 false whenever a point is probed in several tables, because the weight then no longer averages to $W$ . A second tempting step treats $Z_1,\dots,Z_S$ as unconditionally independent, which would give an error of order $\sigma^2(Z)/S$ and lose the table term $\sigma^2(W)$ , which does not decay in $S$ ; the samples are independent only given the tables. The Chernoff step needs independence across the $M$ estimators, which comes from building each estimator from fresh tables.

Formalization scope

Data. Points are indexed by Fin n, so duplicates count separately; vectors live in EuclideanSpace ℝ (Fin d), and $\theta_{qx}$ is InnerProductGeometry.angle.
Tables. A table is the tuple of the $n+1$ codes $(g(v_1),\dots,g(v_n),g(q))\in(\{0,1\}^t)^{n+1}$ . A hash law $\mu$ is an arbitrary probability measure on tables. The paper writes $p(x)$ as a function of $\theta_{qx}$ because, for random-hyperplane LSH, it depends only on that angle. Here $p$ and $p(x,y)$ are defined from $\mu$ , which generalizes the paper: its proofs use nothing about hyperplanes.
Randomness. One estimator run is a family of tables and samples on a probability space whose joint law is pinned on atoms: i.i.d. tables with law $\mu$ , and, given the tables, i.i.d. samples uniform on the pool. The $M$ runs are mutually independent. On an empty pool every weight is $0$ (the paper does not treat this case; Lemma 1 survives it).
Conventions. The median is the lower median. " $(1\pm\varepsilon)$ -approximation" means $|E-|\mathcal A_q||\le\varepsilon|\mathcal A_q|$ . Lemma 1 conditions on the tables, not on $W$ , which is what its proof does.
Added hypotheses, all implicit in the paper: $\mathcal A_q\ne\emptyset$ , $p(x)>0$ on $\mathcal A_q$ , $\varepsilon>0$ , $0<\delta<1$ .
Constants. Theorem 1 and Lemma 6 are printed with $O(\cdot)$ and stated with the constants of their proofs, including the restored factor $8$ .
Ruling out trivial versions. $p$ and $p(x,y)$ are computed from the same hash law that drives the run, never free parameters, and the run predicate is satisfiable: a sorry-free sanity check exhibits a run meeting every hypothesis of the goal.
Libraries. The development needs finite sums and conditioning on finite types, ProbabilityTheory.variance, Chebyshev's inequality (meas_ge_le_variance_div_sq), the moment generating function of a sum of independent indicators (measure_ge_le_exp_mul_mgf), and List.insertionSort. The median lemma and the Chernoff step are independent of LSH and reusable.

Not in scope: Theorem 2 (Multi-Probe Count) with Lemmas 7–9; the running-time Theorems 3–4; the random-hyperplane collision formulas (Theorems 5–6, Lemma 12, (1)); the experiments.

Selected references

X. Wu, M. Charikar, V. Natchu, Local Density Estimation in High Dimensions, arXiv:1809.07471v1, 2018; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1809.07471
M. S. Charikar, Similarity estimation techniques from rounding algorithms, STOC 2002, pp. 380–388. https://doi.org/10.1145/509907.509965
P. Indyk, R. Motwani, Approximate nearest neighbors: towards removing the curse of dimensionality, STOC 1998, pp. 604–613. https://doi.org/10.1145/276698.276876
Q. Lv, W. Josephson, Z. Wang, M. Charikar, K. Li, Multi-probe LSH: efficient indexing for high-dimensional similarity search, VLDB 2007, pp. 950–961. https://www.vldb.org/conf/2007/papers/research/p950-lv.pdf
M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, Journal of the ACM 42(6), 1995, pp. 1115–1145. https://doi.org/10.1145/227683.227684

12 thms2 active usersReviewed

Completed

Economics Operations Research Probability·Captain: mikedeng1

Inducing Compliance with Postmarket Studies for Drugs Under FDA’s Accelerated Approval Pathway: The Compliance Cost-Type Threshold Increases with Enforceability and with Success ProbabilityResearch Paper

Motivation

The U.S. Food and Drug Administration's accelerated approval pathway permits some drugs to reach patients before their clinical benefit has been fully confirmed. A manufacturer then promises a post-market study, but completion requires costly effort that the regulator cannot directly observe. If the study becomes overdue, withdrawal is a process rather than an instantaneous event. The time that process takes changes the manufacturer's incentive to finish the study. Xu, Zhao, and Petruzzi model this interaction and ask how withdrawal enforceability and the chance of a favorable study result affect compliance Xu, Zhao, and Petruzzi, SSRN preprint, 2019.

The question matters to a regulator setting a study deadline. A stronger withdrawal process can reduce the expected time a drug remains on the market after missing that deadline. A higher probability of confirming clinical benefit makes successful completion more valuable to the manufacturer. The paper's Proposition 2 compares these two changes through the largest study-cost type that a deadline can induce to comply.

Setting

A drug enters the market under accelerated approval at time zero. Its patent expires at time $T>0$ . Before expiry it earns a profit rate $\pi_A>0$ while accelerated approval remains in effect, and a rate $\pi_R\ge\pi_A$ after conversion to regular approval. The regulator chooses a deadline $d\in[0,T]$ . If the study is still incomplete at $d$ , the regulator starts withdrawal; the additional withdrawal time $\tau$ is exponentially distributed with rate $s>0$ . Thus increasing $s$ shortens the expected withdrawal delay. Sales under accelerated approval stop at $\tilde d=\min(d+\tau,T)$ unless the study finishes earlier.

The manufacturer chooses a nonnegative effort $\lambda$ , interpreted as the patient recruitment rate for a study requiring $n$ patients. For $\lambda>0$ , the completion time $t$ follows a Gamma distribution with shape $n$ and rate $\lambda$ . At $\lambda=0$ the study never completes. A completed study confirms benefit with probability $\alpha\in(0,1]$ . If confirmation occurs before $\tilde d$ , the drug earns the regular-approval rate until $T$ ; otherwise it leaves the market at completion. For realized $t$ and $\tau$ , revenue is

\phi(t,\tau)= \begin{cases} t\pi_A+(T-t)\alpha\pi_R,&t\le\tilde d,\\ \tilde d\pi_A,&t>\tilde d. \end{cases}

The effort cost is $\theta\lambda^k$ , where $\theta>0$ is the manufacturer's cost type and $k\ge1$ . The resulting expected profit is $\Pi(\lambda,d,\theta)=\mathbb E_t\mathbb E_\tau[\phi(t,\tau)]-\theta\lambda^k$ for positive effort. With no effort, profit is $\Pi_N(d)=\mathbb E_\tau[\tilde d]\pi_A$ . An effort is optimal if it maximizes this profit over all nonnegative efforts. The manufacturer complies at a deadline if some positive effort is optimal; a tie with zero effort counts as compliance, as in the paper's comparison $\Pi_C\ge\Pi_N$ . Let $C(s,\alpha)$ be the positive cost types for which some feasible deadline induces compliance, with the other parameters fixed. The compliance threshold $\hat\theta(s,\alpha)$ is the supremum of that set.

Formalization targets

The compliance threshold

The goal is the paper's Proposition 2. For fixed $T,\pi_A,\pi_R,n,k$ and admissible rates and probabilities, it asserts

s_1\le s_2\Longrightarrow\hat\theta(s_1,\alpha)\le\hat\theta(s_2,\alpha), \qquad \alpha_1\le\alpha_2\Longrightarrow\hat\theta(s,\alpha_1)\le\hat\theta(s,\alpha_2).

The proof in the paper supports strict inequalities for a strict parameter increase when the initial compliant-type set is nonempty. This guarded strict version is included in the goal. If the set is empty, its Lean real supremum is zero, so an unconditional strict statement would be false.

Supporting statements

The milestones record the integral representation of profit and the no-effort closed form, the single crossing of the deadline kernel, the threshold characterization from Proposition 1, and the two comparison steps used for enforceability and success probability. Together they connect the operational study model to the cost-type threshold. They are statements from Proposition 1 and the proofs of Propositions 1 and 2 in the same SSRN preprint.

Significance

The threshold tells the regulator which manufacturers can be induced to finish a required study by choosing an appropriate deadline. Raising it means that a manufacturer with a higher effort cost can still find positive effort optimal. The result concerns whether compliance can be induced; it does not assert a particular optimal deadline, a user-fee menu, or patient welfare. Those require further parts of the paper's mechanism-design model Xu, Zhao, and Petruzzi, §§4–5.

The mathematical result has a paper proof. This mission's Lean statements give it a precise computational interpretation: the completion and withdrawal distributions, the revenue rule, the no-study case, maximization over feasible effort, and the threshold are all explicit. The local index found no existing platform theorem with this model and conclusion. A complete development would add machine-checked proofs and reusable facts about Gamma completion probabilities, exponential delays, bounded expected revenue, and optimal effort. The present draft statements themselves are not proofs.

Difficulty

Comparing profit at the same deadline and effort does not settle the enforceability claim. Increasing $s$ changes both the return from completion and the benchmark profit from never completing, while the deadline that gives the best compliance incentive can move. Similarly, a positive payoff change at a fixed effort does not by itself identify the largest complying cost type: the optimum must still be taken over all efforts, and the supremum over deadlines must be justified. The proof must also control the zero-effort boundary and establish that the relevant set of cost types is bounded.

Formalization scope

Lean uses real values for time, rates, profits, effort, and cost type, and a natural number $n$ for sample size. Params.Standing includes $T>0$ , $0<\pi_A\le\pi_R$ , $0<\alpha\le1$ , $s>0$ , and $1\le k<n$ . The paper gives $k\ge1$ and derives the profit-rate order from its demand assumptions. Positivity of $\alpha$ , finite positive $s$ , and $k<n$ are disclosed restrictions needed for the stated threshold and the paper's limiting argument. Types satisfy $\theta>0$ , deadlines lie in $[0,T]$ , and the two boundary regimes $s=0$ and $s=\infty$ discussed as limits in the paper are outside the mission.

The withdrawal delay is Mathlib's exponential measure and positive-effort completion is its Gamma measure. Since Gamma measure at rate zero does not represent a study that never completes, the profit definition has a separate $\lambda=0$ branch equal to $\Pi_N$ . Revenue integrands are bounded on the distributions' nonnegative support under the standing assumptions. The threshold is computed as the real supremum of cost types for which an actual positive maximizer exists at some feasible deadline. A formulation based only on a positive-effort supremum would make compliance automatic and would not represent the paper's decision rule. If no positive cost type complies, the real supremum is zero; boundedness and the nonempty case are explicit in the milestones and goal.

A full proof needs integration against the Gamma and exponential measures, continuity and existence of an effort maximizer, a characterization of the cost-type set, and comparison of profit across deadline choices. Measure and optimization lemmas from this work can be reused beyond the drug-study application. Contributions to those components and to the stated milestones are within scope; the deadline-dependent fee menu and patient-welfare optimization of later sections are not part of this target.

Selected references

L. Xu, H. Zhao, and N. C. Petruzzi, Inducing Compliance with Post-Market Studies for Drugs under FDA's Accelerated Approval Pathway, SSRN preprint, March 2019; published in Manufacturing & Service Operations Management 22(6), 2020. SSRN 3471632.

7 thms2 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

Extremizing and Antiextremizing in Bayesian Ensembles of Binary-Event Forecasts: Jointly Normal Information States Make the Generalized Probit Ensemble the Optimal AggregatorResearch Paper

Motivation

A decision maker often receives several probability forecasts for the same binary event. The forecasters may have overlapping information, so averaging their numbers can count shared evidence more than once. Lichtendahl, Grushka-Cockayne, Jose and Winkler study the probability of the event conditional on the forecasts themselves. Their generalized probit ensemble gives this conditional probability for jointly normal information states and a broad class of response curves. It lets the information states have a general covariance matrix, which records how much information the experts share.

The question is operational: given the experts' reported probabilities, what probability should the decision maker report? Under a proper scoring rule, the conditional event probability is the optimal report. The paper first develops ensembles based on conjugate prior and likelihood pairs, then treats the normal information-state model in Proposition 4. This mission concerns that latter result, using the preprint's §3 and Appendix rather than the published article's pagination.

Setting

There are $k$ experts. Their information states form a jointly normal vector $x=(x_1,\ldots,x_k)$ with mean $\mu$ and covariance matrix $\Sigma=(\sigma_{ij})$ . The event is $Y=\{y=1\}$ . A generalized linear model specifies the probability of that event after all information states are known:

P(Y\mid x)=F_{z_0}\!\left(\alpha_0+\sum_{i=1}^k\alpha_i x_i\right).

Here $F_{z_0}$ is the cumulative distribution function of a continuous, full-support real random variable $z_0$ . Expert $i$ reports the conditional probability $p_i=P(Y\mid x_i)$ . The prior-predictive probability is $p_0=P(Y)$ , and the Bayesian aggregate is $\hat p=P(Y\mid p_1,\ldots,p_k)$ . None of these probabilities is defined by the closed formula to be proved.

Write $F_{z_0+\sqrt v x_0}$ for the distribution function of the sum of independent $z_0$ and $\sqrt v x_0$ , where $x_0$ is standard normal. The paper gives its variance parameters $v_0$ and $v_i$ in terms of $\alpha$ and $\Sigma$ , and weights $\beta_i$ in terms of the correlations $\rho_{ij}=\sigma_{ij}/(\sqrt{\sigma_{ii}}\sqrt{\sigma_{jj}})$ . The inverse distribution function in Proposition 4 is evaluated only at probabilities arising from the model.

Formalization targets

Gaussian and conditional-law milestones

Lemma 1 identifies the normal law of the full linear predictor and the conditional normal law of the predictor excluding expert $i$ , given $\alpha_i x_i$ . Equation (14) identifies an expectation of the link function under a normal law with $F_{z_0+\sqrt v x_0}$ . The proof of Proposition 4 then identifies the weights, each expert's report, and the prior-predictive probability. The five milestones are the two Gaussian laws, equation (14), the report formula, and the prior-predictive formula; the weight chain is a supporting theorem item.

Proposition 4: generalized probit ensemble

The target is the paper's formula for the Bayesian aggregate, including its stated formulas for $p_0$ and $p_i$ :

\hat p =F_{z_0}\!\left(\beta_0 F^{-1}_{z_0+\sqrt{v_0}x_0}(p_0) +\sum_{i=1}^k\beta_i F^{-1}_{z_0+\sqrt{v_i}x_0}(p_i)\right), \qquad \beta_0=1-\sum_{i=1}^k\beta_i.

The corresponding parameters are $m_0=\alpha_0+\sum_i\alpha_i\mu_i$ , $v_0=\sum_{i,j}\alpha_i\alpha_j\sigma_{ij}$ , $v_i=\sum_{j,j'\ne i}\alpha_j\alpha_{j'}\sigma_{jj'}-(\sum_{j\ne i}\alpha_j\sigma_{ij})^2/\sigma_{ii}$ , and $\beta_i=\alpha_i\sqrt{\sigma_{ii}}/(\sum_j\alpha_j\sqrt{\sigma_{jj}}\rho_{ij})$ . The two other conclusions are $p_0=F_{z_0+\sqrt{v_0}x_0}(m_0)$ and $p_i=F_{z_0+\sqrt{v_i}x_0}(m_0+\beta_i^{-1}\alpha_i(x_i-\mu_i))$ .

Significance

Proposition 4 expresses a forecast based on all reports using only the reports, a prior probability, the link distribution, and coefficients determined by the information-state covariance. It allows the decision maker to account for correlated expert information without reconstructing each expert's private sample. The result also states that an expert's report is calibrated under the model: if only that report is heard, its conditional event probability is the reported number.

The result is proved in the paper. The remaining task here is a machine-checked proof of the conditional Gaussian, integral, inversion, and conditioning identities behind the displayed ensemble. The formal definitions of the forecast as a conditional probability and the covariance-derived coefficients can be reused when comparing other forecast aggregation rules. No proof of Proposition 4 is claimed by this proposal; the Lean theorem is an open target.

Difficulty

The report $p_i$ is itself a conditional probability, while the aggregate conditions on the vector of these reports. Replacing either by its expected closed form at the outset would erase the central claim. A proof must instead connect the Gaussian conditional law of the unobserved states to each report, and then relate conditioning on the reports to conditioning on the full state. The inverse cdf also requires care: its real-valued representation is meaningful at probabilities strictly between zero and one, and its value outside that interval has no role in the paper's formula.

Formalization scope

Experts are indexed by Fin k; the formulas do not require $k\ge2$ , although §2.2 discusses at least two experts. The information state is EuclideanSpace ℝ (Fin k), and its law is Mathlib's multivariate Gaussian with a positive semidefinite covariance matrix. A probability measure $\nu$ represents $z_0$ ; absolute continuity and positive measure for every nonempty open interval express the paper's continuous, entire-real-line support assumption. The cdf of $z_0+\sqrt v x_0$ is the cdf of the convolution of $\nu$ with a centered normal law. A generalized inverse uses the infimum of its upper level set; it is used only on the probability range $(0,1)$ .

Three nondegeneracy assumptions are stated explicitly: $\alpha_i\ne0$ , $\sigma_{ii}>0$ , and $\sum_j\alpha_j\sigma_{ij}\ne0$ for each expert. They make the paper's inverses, correlations, and denominators meaningful. Positive semidefiniteness gives $v_0,v_i\ge0$ , so conversion to Mathlib's nonnegative variance type does not clip them. The location-scale statement fixes $z_0$ as its standard member, with location zero and scale one.

The event is measurable, the information-state map is measurable, and its law and conditional event probability are model hypotheses. Reports and aggregate are conditional expectations of the event indicator, with identities stated almost surely because conditional probabilities are only determined up to null sets. The proposal never defines reports or the aggregate by their claimed closed formulas. Contributions may develop general Gaussian pushforward and conditional-law results, cdf convolution identities, and measure-theoretic results about conditioning on transformed reports.

Selected references

K. C. Lichtendahl Jr., Y. Grushka-Cockayne, V. R. R. Jose and R. L. Winkler, Bayesian Ensembles of Binary-Event Forecasts: When Is It Appropriate to Extremize or Anti-Extremize?, arXiv:1705.02391v2, 2018, §3 and Appendix. Preprint

7 thms2 active usersReviewed

Algorithmic Game Theory Combinatorics Mechanism Design+1·Captain: mikedeng1

Polyhedral Clinching Auctions for Two-Sided Markets: An Incentive-Compatible, Individually Rational, Budget-Balanced, Pareto-Optimal Mechanism ExistsResearch Paper

Motivation

Auctions in which bidders face budget constraints do not fit the classical quasi-linear theory: a bidder cannot pay more than a fixed amount, however much the goods are worth to him. For a single divisible good, Dobzinski, Lavi and Nisan showed that the adaptive clinching auction of Ausubel is incentive compatible, individually rational and Pareto optimal, and that with two bidders it is the only such mechanism (Dobzinski–Lavi–Nisan 2012). Goel, Mirrokni and Paes Leme extended clinching to supply constraints described by a polymatroid, the polyhedral clinching auction (Goel–Mirrokni–Paes Leme 2015), which covers sponsored-search and matching-type markets.

These results are one-sided: a single auctioneer sells and keeps the revenue. In markets with many sellers, such as advertising exchanges or electricity markets, sellers have their own valuations and the mechanism must also make them better off and pass payments through. For non-budgeted bilateral trade, the Myerson–Satterthwaite theorem rules out efficiency together with incentive compatibility, individual rationality and budget balance (Myerson–Satterthwaite 1983), so a positive result needs a weaker efficiency notion and sellers that report truthfully.

Timeline:

2008–2012: Dobzinski, Lavi and Nisan, adaptive clinching for one divisible good with budgets.
2015: Goel, Mirrokni and Paes Leme, polyhedral clinching auction for polymatroidal supply.
2017–2022: Hirai and Sato, the two-sided extension that is the subject of this mission (arXiv:1708.04881, Mathematics of Operations Research 2022).

Setting

The market is a bipartite graph $(N,M,E)$ : buyers $N=\{1,\dots,n\}$ , sellers $M=\{1,\dots,m\}$ , and edges $E\subseteq N\times M$ ; $ij\in E$ means that buyer $i$ wants the goods of seller $j$ . Write $E_i$ and $E_j$ for the edges at buyer $i$ and at seller $j$ . The goods are divisible and homogeneous.

Buyer $i$ has a valuation $v_i$ , a bid $v'_i$ and a budget $B_i$ , all nonnegative reals. Seller $j$ has a reserve price $\rho_j\ge0$ , which he reports truthfully, and a monotone submodular function $f_j$ on the subsets of $E_j$ : $f_j(\emptyset)=0$ , $f_j$ is monotone, and $f_j(S\cup T)+f_j(S\cap T)\le f_j(S)+f_j(T)$ . The value $f_j(F)$ bounds the goods transacted through $F$ , and $f_j(E_j)$ is seller $j$ 's stock. The polymatroid of $f_j$ is $P_j=\{x\in\mathbb R^{E_j}_+\mid x(F)\le f_j(F)\ (F\subseteq E_j)\}$ .

An allocation is a triple $(w,p,r)$ of transactions $w\in\mathbb R^E$ , payments $p\in\mathbb R^N$ and revenues $r\in\mathbb R^M$ with $w|_{E_j}\in P_j$ for every seller and $p_i\le B_i$ for every buyer. A mechanism maps the public information $\mathcal I$ (graph, bids, budgets, reserve prices, the $f_j$ ) to an allocation; it does not see the true valuations. The utilities are

u_i=\begin{cases}v_i\,w(E_i)-p_i & p_i\le B_i\\ -\infty&\text{otherwise}\end{cases},\qquad u_j=r_j+\rho_j\bigl(f_j(E_j)-w(E_j)\bigr).

The five properties are: (ICb) truthful bidding is a dominant strategy for buyers; (IRb) truthful buyers get nonnegative utility; (IRs) each seller ends with utility at least $\rho_j f_j(E_j)$ ; (SBB) $\sum_i p_i=\sum_j r_j$ ; (PO) under truthful bids, no allocation with $\sum_i p_i\ge\sum_j r_j$ makes everyone weakly better off and someone strictly.

Formalization targets

Goal: Theorem 2.1

\exists\,\mathcal M:\quad \mathcal M \text{ outputs allocations and satisfies (ICb), (IRb), (IRs), (SBB), (PO)},

for every market and clock step $\varepsilon>0$ , on inputs whose bids, reserve prices and true valuations are multiples of $\varepsilon$ (Assumption 3.2).

Milestones

The witness is Mechanism 2: add a virtual buyer $n+j$ with infinite budget and bid $\rho_j$ for each seller, run the two-sided clinching auction (Algorithm 2), and subtract the virtual buyers' payments from the revenues. The milestones follow the paper's argument:

Theorem 3.3: the one-sided polyhedral clinching auction (Algorithm 1) on the reduced market $\tilde P=\{(w(E_i))_i\mid w\in P\}$ satisfies (ICb), (IRb) and ends on the base polytope.
Theorem 3.6: each clinching polytope $P^i_{w,d}$ is a polymatroid, so a maximal clinch exists.
Lemma 3.7 and Proposition 3.8: Mechanism 2 satisfies (SBB) and (IRs).
Theorem 3.9: Algorithms 1 and 2 end with the same $(w(E_i))_i$ and payments.
Corollary 3.10 and Theorem 3.11: Mechanism 2 satisfies (ICb), (IRb) and (PO).
Lemma 3.4: a revenue vector with (17)–(18) exists for Algorithm 1's output.

Significance

The theorem shows that the impossibility for two-sided trade disappears when efficiency is weakened to Pareto optimality and sellers report truthfully, even with budgets and with polymatroidal transaction constraints on each seller. Mechanism 2 is implementable: each clinching step reduces to a polymatroid greedy computation (Theorem 3.6). The polymatroid layer covers matching-type markets and sellers with structured supplies.

The result is proved in the paper; no machine-checked proof of it or of the polyhedral clinching auction is known. The mission produces a formal model of budgeted two-sided markets, of ascending clock auctions as relations on runs, and of the clinching polytopes, together with the statements of the paper's main steps. Formal proofs of any milestone are welcome, including the one-sided theorem of Goel et al. (Theorem 3.3) on its own.

Difficulty

The obvious route, running the one-sided polyhedral clinching auction on the aggregated polymatroid $\tilde P$ , gives the buyers' quantities and payments but not who buys from whom, and not the sellers' revenues; nothing in the one-sided analysis protects a seller from selling below his reserve price. The paper's Mechanism 2 clinches edge by edge, and the central step is Theorem 3.9: a buyer's sequential edge-wise clinch in the two-sided market coincides in total with his simultaneous clinch in the reduced market, for every choice of maximal clinching vector. This needs a polymatroidal network-flow description of the remnant supply and a careful invariant on the minimizers of the associated submodular functions (§5.2). Pareto optimality requires, in addition, tracking the sellers' utilities through the virtual buyers.

Formalization scope

Buyers are Fin n, sellers Fin m, edges a Finset (Fin n × Fin m); transactions are functions on the edges in E. All indices are 0-based. Budgets and demands that can be infinite live in WithTop ℝ; buyer utility lives in WithBot ℝ and is only compared. The properties are imposed on the inputs of Assumption 3.2 (p. 10): bids, reserve prices (the virtual buyers' bids) and true valuations are nonnegative integer multiples of $\varepsilon$ ; budgets and the $f_j$ are unrestricted apart from the standing assumptions.

Algorithms 1 and 2 are relations: a run is a finite sequence of states, one per while-iteration, ending at the first state where all demands are $0$ , and results are stated for every run. The demand of a buyer whose clock is still $0$ and below his bid is $\infty$ (line 1 and Table 1, p. 16). Line 13 of Algorithm 2 updates the demand of the buyer whose clock was just increased. The polynomial-time clauses of Theorem 3.6 are not formalized.

A mechanism that reads the true valuations, a (PO) whose competitors need not be allocations, or a mechanism that is not required to output allocations would make the goal trivial; the definitions exclude all three.

Mechanism 1 (polymatroidal network flow, Theorem 3.5) and the deeper lemmas of §5 are not stated. Reusable parts: the polymatroid definitions and the one-sided Algorithm 1, stated for an arbitrary feasible set.

Selected references

H. Hirai, R. Sato, Polyhedral Clinching Auctions for Two-Sided Markets, Mathematics of Operations Research, 2022; arXiv:1708.04881v2 (2018). https://arxiv.org/abs/1708.04881
G. Goel, V. Mirrokni, R. Paes Leme, Polyhedral Clinching Auctions and the AdWords Polytope, Journal of the ACM 62(3), 2015. https://doi.org/10.1145/2757277
S. Dobzinski, R. Lavi, N. Nisan, Multi-unit Auctions with Budget Limits, Games and Economic Behavior 74(2), 2012. https://doi.org/10.1016/j.geb.2011.08.003
R. B. Myerson, M. A. Satterthwaite, Efficient Mechanisms for Bilateral Trading, Journal of Economic Theory 29(2), 1983. https://doi.org/10.1016/0022-0531(83)90048-0

12 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Profit Effects of Consumers’ Identity Management: A Dynamic Model: Under Full Information Acquisition, Active and Unserved Consumers Exist if and only if the Privacy Cost Is Below a ThresholdResearch Paper

Motivation

Firms that track their customers can charge a returning customer according to what they have learned about her, while a newcomer pays an introductory price. Consumers can respond by identity management: deleting cookies, using new accounts or anonymising tools, so that they keep being treated as newcomers. The economics of this behaviour-based price discrimination with strategic consumers goes back to two-period models such as Fudenberg and Tirole (2000); the closest privacy models are the two-period monopolies of Acquisti and Varian (2005) and Conitzer, Taylor and Wagman (2012).

Laussel, Long and Resende (2023) study the question in an infinite-horizon setting; the formalization cites their CIRANO working paper 2021s-29. A monopolist gradually expands its market by lowering an introductory price, as a durable-good monopolist does in the Coase conjecture, and recognises every passive customer after her first purchase. Consumers decide once whether to pay a privacy cost to remain anonymous. The paper's main analytic result, Proposition 1, states that under full information acquisition the firm leaves part of the market unserved exactly when privacy is cheap enough, and gives the threshold in closed form.

Setting

Time is divided into contracting periods $n = 0, 1, 2, \dots$ with discount factor $\beta = e^{-\Delta} \in (0,1)$ . A monopolist sells a non-durable good at zero marginal cost. A unit mass of consumers has types $\theta$ uniform on $[0,1]$ ; type $\theta$ obtains utility $\theta$ per period of consumption.

Under full information acquisition (FIA) a passive consumer who has bought once is recognised and charged exactly $\theta$ in every later period. A consumer may instead pay a once-for-all privacy cost $c \ge 0$ in period $0$ and become active: she remains anonymous and buys every period at the introductory price $p^I(n)$ offered to new customers. Types in $[\tilde\theta, 1]$ are active and types below the pivot $\tilde\theta$ are passive.

The firm uses a quasi-linear cut-off rule $\theta_{n+1} = \Phi(\theta_n) = K + \gamma\theta_n$ with $0 \le \gamma < 1$ : in period $n$ the new passive customers are the types in $[\theta_{n+1}, \theta_n)$ , starting from $\theta_0 = \tilde\theta$ . The path converges to $\theta_{\inf} = K/(1-\gamma)$ , and types below $\theta_{\inf}$ are never served. Consumers hold a quasi-linear expectations rule $\Psi(\theta) = C + \lambda\theta$ : the lifetime net utility of the period- $n$ marginal passive customer when the state is $\theta_n = \theta$ . The introductory price is $p^I(n) = \theta_{n+1} - \Psi(\theta_n)/(1-\beta)$ , and the firm's period profit at state $x$ and choice $y$ is

\pi(x,y) = (1-\beta)\Big[\tfrac{\tilde\theta^2 - x^2}{2} + (1-\tilde\theta+x-y)\Big(y - \tfrac{\Psi(x)}{1-\beta}\Big)\Big].

A Markov perfect equilibrium (MPE) is a profile $(\beta, c, K, \gamma, C, \lambda, \tilde\theta)$ satisfying, at every state $\theta \in [0,1]$ :

the arbitrage equation $\Psi(\theta) = \beta[\Psi(\Phi\theta) + (1-\beta)(\Phi\theta - \Phi(\Phi\theta))]$ ;
the Euler condition $\partial_y\pi(\theta,\Phi\theta) + \beta\,\partial_x\pi(\Phi\theta, \Phi(\Phi\theta)) = 0$ , which is the first-order condition of the firm's Bellman equation combined with the envelope condition;
the pivot condition: with $G = \beta\tilde\theta - c - \sum_{n \ge 1}(1-\beta)p^I(n)\beta^n$ , $G = 0$ when $\tilde\theta < 1$ and $G \le 0$ when $\tilde\theta = 1$ .

It must also satisfy $0 \le \theta_{\inf} \le \tilde\theta \le 1$ .

Formalization targets

Goal: Proposition 1

With the threshold

\bar c^{FIA} = \frac{\beta(1-\gamma)(1+(1-2\beta)\gamma)}{(1-\beta\gamma)^2},

every FIA MPE satisfies:

(i) if $c < \bar c^{FIA}$ then $\tilde\theta < 1$ and $\theta_{\inf} > 0$ ;
(i) both $\theta_{\inf}$ and $1 - \tilde\theta$ decrease strictly in $c$ , among equilibria with the same $\beta$ , and tend to $0$ as $c \uparrow \bar c^{FIA}$ ;
(ii) if $c \ge \bar c^{FIA}$ then $\tilde\theta = 1$ and $\theta_n \to 0$ ;
(iii) $\Psi(\theta_n) \to 0$ , so the last served type gets zero lifetime utility.

Milestones

Lemma 2: every Markov equilibrium has $\lambda = \beta(1-\beta)(\gamma-\gamma^2)/(1-\beta\gamma)$ and $C = -\beta K\gamma(1-\beta)/(1-\beta\gamma)$ ; an MPE exists for every $\beta \in (0,1)$ and $c \ge 0$ .
$\gamma^*(\beta)$ : equilibria with the same $\beta$ have the same $\gamma$ , and $\gamma > 0$ .
Corollary 1: $\theta_{\inf}$ is strictly decreasing in $\tilde\theta$ and vanishes at $\tilde\theta = 1$ .
Lemma 3: the pivot formula (18).
The gap identity, $\tilde\theta - \theta_{\inf} = c(1-\beta\gamma)^2/(\beta(1-\gamma)(1+(1-2\beta)\gamma))$ when $\tilde\theta < 1$ .
The threshold: $\tilde\theta < 1 \wedge \theta_{\inf} > 0 \iff c < \bar c^{FIA}$ .
The limit $\Psi(\theta_n) \to 0$ .

Significance

Proposition 1 shows that consumer privacy can stop a dynamic monopolist from serving the whole market. Without active consumers the firm keeps lowering its introductory price until everyone buys, in line with Coasian dynamics. With them, every price cut is also collected by the anonymous high-value consumers, so the firm stops at a strictly positive $\theta_{\inf}$ . The gap identity makes the effect quantitative: the share of passive customers who are eventually served is linear in the privacy cost. These statements underlie the paper's managerial recommendation that a firm facing cheap identity management should not aim at full coverage, and its comparison with the partial-history (PHI) information structure.

The result is proved in the paper, but by computer algebra with several printed slips. The prior-art search found no machine-checked formalization of this result. A formal proof would turn the closed-form calculation into a checked argument about a precisely defined equilibrium notion. The mission also provides a reusable encoding of an infinite-horizon pricing game with rational-expectations consumers, specified by arbitrage, Euler and indifference conditions. Nothing comparable is on the platform.

Difficulty

The equilibrium conditions couple the cut-off slope $\gamma$ , the pivot $\tilde\theta$ and the expectation rule. The Euler equation leaves an algebraic condition on $\gamma$ whose admissible root must be unique for every $\beta \in (0,1)$ ; without uniqueness, two equilibria with the same discount factor could have different expansion speeds. At $\tilde\theta = 1$ the pivot condition is an inequality, so a calculation valid at an interior pivot does not settle the threshold case. The pivot also contains an infinite price series whose convergence matters to the claimed threshold.

The Online Appendix's closed forms (29), (30) and (31) do not follow from the model as printed: the envelope expression (23) has a sign slip. For example, at $\beta = 1/2$ the corrected Euler equation gives $\gamma \approx 0.48966$ , whereas the printed (29) gives $0.47862$ . The Lean statements use the derivative of the period profit and omit those printed formulas.

Formalization scope

Everything is real-valued. The definitions file IdentityMgmt.FIA.Model has the following parts:

a Profile structure with fields $\beta, c, K, \gamma, C, \lambda, \tilde\theta$ ;
the rules $\Phi$ and $\Psi$ , the path $\theta_n = \Phi^{n}(\tilde\theta)$ (iterate), $\theta_{\inf}$ , $p^I(n)$ and the period profit $\pi$ ;
the predicates Arbitrage, Euler (via Mathlib's deriv), Pivot, IsMarkovEq and IsMPE;
the threshold cbarFIA.

The formalization commits to the following conventions:

The standing assumptions $0 < \beta < 1$ , $0 \le \gamma < 1$ and $c \ge 0$ are part of the equilibrium predicates.
Arbitrage and Euler are required at every state in $[0,1]$ , as a Markov rule must be.
Feasibility is the weak $\theta_{\inf} \le \tilde\theta$ , because at $c = 0$ the equilibrium path is constant.
At the corner $\tilde\theta = 1$ the pivot condition is the inequality "type 1 does not gain from going active".
The firm's best reply is encoded, as in the paper, by its first-order system; the paper never verifies global optimality.
The pivot series is a tsum, which is summable under the standing assumptions.

The boundary condition $\lim \Psi(\theta_n) = 0$ is not part of the definition: it is Proposition 1 (iii), and must be derived. Defining $\tilde\theta$ , $K$ or $\gamma$ by formulas, or taking $\gamma$ as a root of the printed (29), would trivialize or falsify the goal and is ruled out. Every equilibrium quantity is a field constrained only by the model's conditions. The existence part of Lemma 2 guards against vacuity.

Not formalized: Lemma 1 (the cut-off structure of the privacy decision, which the model builds in), the first sentence of Corollary 1, Corollary 2 (a graphical argument), the numerical Corollaries 3–4, and the PHI analysis (Lemma 4, Proposition 2).

Contributions are welcome at every milestone. The most reusable pieces are lemmas computing the derivatives of the period profit, the closed form of the expansion path, and the evaluation of the pivot series.

Selected references

D. Laussel, N. V. Long, J. Resende, Profit Effects of Consumers' Identity Management: A Dynamic Model, Management Science, 2023. https://doi.org/10.1287/mnsc.2022.4511 — formalized from the CIRANO working paper 2021s-29 (24 Aug. 2021) with its online appendix
D. Fudenberg, J. Tirole, Customer Poaching and Brand Switching, RAND Journal of Economics 31(4), 2000. https://doi.org/10.2307/2696354
A. Acquisti, H. R. Varian, Conditioning Prices on Purchase History, Marketing Science 24(3), 2005. https://doi.org/10.1287/mksc.1040.0103
V. Conitzer, C. R. Taylor, L. Wagman, Hide and Seek: Costly Consumer Privacy in a Market with Repeat Purchases, Marketing Science 31(2), 2012. https://doi.org/10.1287/mksc.1110.0669
A. Acquisti, C. Taylor, L. Wagman, The Economics of Privacy, Journal of Economic Literature 54(2), 2016. https://doi.org/10.1257/jel.54.2.442
R. H. Coase, Durability and Monopoly, Journal of Law and Economics 15(1), 1972. https://doi.org/10.1086/466731

9 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Robust Bidding in First-Price Auctions: How to Bid Without Knowing What Others Are Doing: Under Variation in Bidding the Unique Minimax Loss Bid Equalizes Both Maximal Losses and Increases in nResearch Paper

Motivation

First-price sealed-bid auctions are used for procurement contracts, treasury securities, timber, and, since 2019, most display advertising. The classical advice for how to bid comes from Bayes–Nash equilibrium: each bidder knows the distribution of the others' values, and everyone plays the equilibrium. Practitioners rarely have that information. In a survey of auction consultants reported by Kasberger and Schlag, almost none of the respondents modelled equilibrium behaviour, and most named the distribution of rivals' bids as something they could not quantify.

Kasberger and Schlag (SSRN 3044438, version of 3 September 2022) propose a bid that needs no such prior. The bidder lists the bid distributions she considers conceivable and chooses the bid whose worst-case shortfall from the best response is smallest: the minimax loss bid (a criterion axiomatized by Milnor 1954, Hayashi 2008 and Stoye 2011). This mission formalizes the paper's choice-based recommendation, variation in bidding (§6.2), where the closed-form bid depends only on the number of bidders, a reserve level and one trust parameter.

Setting

There are $n \ge 2$ bidders. Bidder 1 has value $v_1$ and bids $b_1 \ge 0$ ; the highest bid wins and pays its bid, and ties are broken uniformly at random. If $m$ bidders (bidder 1 included) tie at the top with $b_1$ , bidder 1 receives $(v_1 - b_1)/m$ ; otherwise she receives $0$ .

A bid distribution $B$ is any joint law of the $n-1$ opponent bids. The expected utility of a bid is $u_1(b_1, B) = \int u_1(b_1, b_{-1})\,dB(b_{-1})$ , and its loss is

l(b_1, B \mid v_1) = \sup_{\bar b_1 \ge 0} u_1(\bar b_1, B) - u_1(b_1, B).

Given an ambiguity set $\mathcal B$ , the maximal loss of $b_1$ is $\sup_{B\in\mathcal B} l(b_1, B\mid v_1)$ , and a minimax loss bid minimizes it over all $b_1 \ge 0$ .

The ambiguity set of variation in bidding, $\mathcal B_{\tau,G}$ , has three ingredients: a probability $\tau \in (0,1)$ , a threshold $L \ge 0$ below which no one bids, and a bid distribution $G$ . Each opponent is independently constrained with probability $\tau$ , and a constrained opponent bids an independent draw from $G$ . The unconstrained opponents bid a vector $Z$ with an arbitrary joint law $H$ on $[L,\infty)^{n-1}$ , independent of who is constrained. Every such $H$ gives a member of $\mathcal B_{\tau,G}$ . The salient choice is $G$ uniform on $[L, v_1]$ , with $p(b) = (b-L)/(v_1-L)$ and

u^+(b) = (v_1 - b)\bigl(1-\tau+\tau p(b)\bigr)^{n-1},\qquad u^-(b) = \tau^{n-1}p(b)^{n-1}(v_1-b),\qquad \tilde b = v_1 - \frac{v_1-L}{n\tau}.

These are the utilities of bidding just above, respectively below, a common bid of all unconstrained opponents.

Formalization targets

Goal: Proposition 4

For $G$ uniform on $[L, v_1]$ , $n \ge 2$ , $0<\tau<1$ and $0 \le L < v_1$ :

there is exactly one minimax loss bid $b_1^*$ ;
a bid $b$ is the minimax loss bid if and only if $b \in [\max\{L,\tilde b\}, v_1]$ and

u^+(\max\{L,\tilde b\}) - u^+(b) = u^+(b) - u^-(b); \tag{3}

the minimax loss is $l_1^* = u^+(b_1^*) - u^-(b_1^*)$ ;
the minimax loss bid with $n+1$ bidders is strictly larger than with $n$ bidders.

Milestones

In the order the paper's proof uses them:

Lemma 1 (p. 21): the maximal loss over $\mathcal B_{\tau,G}$ equals the supremum over the environments in which all unconstrained opponents bid one common value $x \ge L$ .
§6.2 (p. 22): for $b \in [L, v_1]$ the maximal loss is the larger of the loss of bidding too high, $\sup_{\hat h\in[L,b]} u^+(\hat h) - u^+(b)$ , and the loss of bidding too low, $\sup_{\hat h> b} u^+(\hat h) - u^-(b)$ .
Proposition 3 (pp. 22–23): the set $X$ of bids in $[L,v_1]$ equalizing these two losses is nonempty, a minimax loss bid exists, and every minimax loss bid lies in $X$ and minimizes the too-high loss there.
Lemma 2 (p. 49): $\max\{\tilde b, L\}$ maximizes $u^+$ on $[L,\infty)$ .
p. 49: $X$ is exactly the set of solutions of (3) in $[\max\{L,\tilde b\}, v_1]$ .
p. 50: on that interval the left side of (3) is nondecreasing, the right side strictly decreasing, and (3) has a unique root.
p. 51: the root of (3) for $n+1$ bidders exceeds the root for $n$ bidders.

Significance

Proposition 4 turns a minimax problem over an infinite-dimensional set of joint distributions into a single equation in one variable. The resulting bid can be computed from $n$ , $\tau$ , $L$ and $v_1$ , and comes with a guarantee: against every environment in $\mathcal B_{\tau,G}$ the loss is at most $l_1^*$ . The paper evaluates this guarantee at $\tau = 0.15$ and tests the bid on field data. The monotonicity in $n$ is the robust analogue of the equilibrium fact that bids shade less as competition grows.

The result is proved in the paper; it has not been formalized anywhere. A machine-checked version adds three things. It fixes the ambiguity set: the printed set is too large, and the formal one is the version under which the statements hold. It records exactly which hypotheses the argument uses ( $0<\tau<1$ , $L<v_1$ ). And it checks the analytic steps, whose printed versions contain small slips. The first-price model, the loss, and the minimax loss bid are reusable for the paper's other two recommendations (Propositions 1 and 5), which use different ambiguity sets.

Difficulty

The definition quantifies over every joint law of the unconstrained bids, including correlated and atomic ones. The crux is Lemma 1: one must show that, for each bid, collapsing all unconstrained mass to a single point (just below the best response when bidding too high, just above the own bid when bidding too low) does not decrease the loss. Some worst cases are limits of point masses approaching a tie, and the tie-breaking rule matters at those limits, so the argument has to work with suprema rather than maximizers.

A natural first idea is to argue coordinate by coordinate, moving one unconstrained bid at a time. It fails: the shift that raises the loss depends on the realized pattern of constrained bidders, and a profile that is worst for one pattern is not worst for another. Once Lemma 1 holds, the rest is one-variable analysis, but uniqueness of the root of (3) needs the strict decrease of $u^+ - u^-$ , which uses $\tau<1$ in an essential way.

Formalization scope

Opponents are indexed by Fin (n - 1); bids, values, $L$ and $\tau$ are reals and $n$ is a natural number with $n \ge 2$ . The payoff splits ties evenly among all tied bidders, bidder 1 included. Expected utility is a Bochner integral of this bounded measurable payoff. Best utility and maximal loss are real suprema; they are finite because utilities of non-negative bids are at most $v_1$ and the ambiguity set is nonempty. The minimax loss bid is a predicate on bids $b \ge 0$ , defined from the maximal loss and never from Equation (3); the goal quantifies over bids satisfying it.

$\mathcal B_{\tau,G}$ is built as a pushforward: i.i.d. pairs (Bernoulli( $\tau$ ) coin, draw from $G$ ) for the opponents, independent of $Z \sim H$ , with $H$ ranging over all probability measures on $\mathbb R^{n-1}$ concentrated on $[L,\infty)^{n-1}$ . The printed definition (p. 20) lets the law of the unconstrained bids depend on who is constrained and allows bids below $L$ ; under it Lemma 1 and Propositions 3–4 fail for $n\ge3$ , so the corrected set is used and the affected items are labelled "corrected". Lemma 1, the p. 22 formula and Proposition 3 are stated for $G$ uniform; the paper states them for general $G$ , and for general continuous $G$ the claim of Proposition 3 that the minimax bid lies in $X$ fails numerically.

Restricting the ambiguity set to point masses, or defining the minimax bid as the root of (3), would make the goal trivial; neither is done. Contributions on the measure-theoretic layer (expected utility of a point-mass environment, the reduction of Lemma 1) are reusable for any first-price robust-bidding problem; the calculus milestones need only Mathlib's real analysis.

Selected references

K. Kasberger and K. H. Schlag, Robust Bidding in First-Price Auctions: How to Bid Without Knowing What Others Are Doing, SSRN 3044438, version of 3 September 2022. https://ssrn.com/abstract=3044438.
J. Milnor, Games against nature, in Decision Processes, Wiley, 1954.
T. Hayashi, Regret aversion and opportunity dependence, Journal of Economic Theory 139 (2008). https://doi.org/10.1016/j.jet.2007.07.001
J. Stoye, Axioms for minimax regret choice correspondences, Journal of Economic Theory 146 (2011). https://doi.org/10.1016/j.jet.2011.09.004
R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018.

11 thms2 active usersReviewed

Completed

Combinatorics Operations Research Probability+1·Captain: mikedeng1

Queueing with Negative Network Effects: Closed-Form Joint Law of the Later Arrivals Met and the Queue-Filling Arrivals for a Customer Joining an M/M/c/n Queue at Position jResearch Paper

Motivation

In many service systems a waiting customer is harmed not only by the time spent in line but also by the other customers met there. Contagion in a clinic, a pharmacy or a government office during an epidemic is the motivating example of Hassin, Meilijson and Perlman, Queueing with Negative Network Effects (SSRN 4097977, 2022; Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1223). There the cost of joining a queue is a function of the number of meets, the customers present in the waiting room at the same time. A customer who joins a queue meets those ahead of her and those who arrive while she still waits. The second number is random and depends on the capacity of the waiting room, because arrivals that find the room full are turned away.

Strategic queueing in the tradition of Naor (1969) assumes a cost linear in waiting time; with negative network effects the relevant random variable is the count of meets, and equilibrium joining strategies and socially safe capacity regulations both require its exact distribution. Section 4 of the paper computes it: first as a row of a matrix power (Theorem 2), then in closed form, jointly with the number of arrivals that fill the room to capacity (Theorem 3). This mission formalizes that section.

Setting

An FCFS M/M/c/n queue has Poisson arrivals at rate $\lambda>0$ , $c\ge1$ servers each working at exponential rate $\mu>0$ , and a waiting room of capacity $n$ : an arrival that finds $n$ customers waiting is lost. The server utilization factor is $\rho=\lambda/(c\mu)$ , and

q=\frac{c\mu}{\lambda+c\mu}=\frac{1}{1+\rho}

is the probability that the next change of the queue is a service completion while all servers are busy.

A tagged customer arrives at position $j$ : $j-1$ customers wait ahead of her. The queue length is the number of waiting customers, herself included, not counting those in service. While she waits, every change of the queue is either a service completion (everybody moves up one place) or an arrival (which joins at the end if the queue length is below $n$ , and is lost otherwise). She enters service at the $j$ -th service completion.

$X_j$ is the number of later arrivals that join the queue before she enters service; $M_j=j-1+X_j$ is the total number of waiting customers she meets.
$Y_j$ is the number among these $X_j$ who fill up the queue, that is, arrive to position $n$ .
The matrix $A$ of (2) is the $(n+1)\times(n+1)$ matrix, indexed by queue sizes $0,\dots,n$ , whose row $k$ is the law of the queue size at the next service completion from queue size $k$ : for $0<k<n$ , $A(k,i)=q(1-q)^{i-k+1}$ for $k-1\le i\le n-2$ and $A(k,n-1)=(1-q)^{n-k}$ ; $A(n,n-1)=1$ ; $A(0,0)=1$ ; all other entries are $0$ .

Formalization targets

Goal: Theorem 3 in full

For $n\ge2$ , $j\in\{1,\dots,n-1\}$ and $d=x-y$ ,

P(X_j=x,Y_j=0)=\left[\binom{j+x-1}{j-1}-\binom{j+x-1}{n-1}\right]\frac{\rho^x}{(1+\rho)^{j+x}},\quad 0=y\le x<n,

P(X_j=x,Y_j=y)=\left[\binom{j+d-1}{n-2}-\binom{j+d-1}{n-1}\right]\frac{\rho^x}{(1+\rho)^{j+d}},\quad 0<y\le x<n,\tag{3}

with probability $0$ elsewhere; $X_n$ has the same law as $X_{n-1}$ ; and the expectation formula (4) for $E[\psi(X_j)]$ and the generating function (5) for $G_j(s)=E[s^{X_j}]$ , $s\rho\ne1$ , hold. The statement depends on $\lambda,\mu,c$ only through $\rho$ , as printed.

Milestones

(2), p. 9. Row $k$ of $A$ is the law of the queue size at the next service completion, $1\le k\le n$ .
p. 9 and Theorem 2 (2), p. 10. From queue size $k$ , the queue size after $j\le k$ service completions has law row $k$ of $A^j$ ; the number of additional customers met by a customer in position $j$ of a queue of length $k$ has that row shifted by $k-j$ .
Theorem 2 (1), p. 9. $X_j$ has law row $j$ of $A^j$ , and $M_j=j-1+X_j$ accordingly.
Theorem 3, (3), p. 10. The joint law (3) with its support, and $X_n\sim X_{n-1}$ .

Significance

The result. Theorem 3 gives the exposure of a joining customer in closed form, as a finite sum of binomial terms in $\rho$ , instead of a power of an $(n+1)\times(n+1)$ matrix. Through (5) it gives the expected utility $U_j=R-S(1-\eta^{j-1}G_j(\eta))$ of a customer facing the exponential loss $\phi_M(m)=S(1-\eta^m)$ , display (6), which is the input to the paper's equilibrium and safe-threshold computations for that loss function. The joint law with $Y_j$ also records how often the room is filled to capacity during one customer's wait, the quantity that a capacity regulation acts on.

Formalizing it. The paper proves Theorem 3 in an Online Appendix that is not part of the preprint, and states (4) and (5) as straightforward corollaries. To the best of a search of the Prove2Me library, no transient result about a tagged customer in a finite-capacity queue, and no path count for a reflected walk with a capacity barrier, has been formalized. A complete development would give a machine-checked account of an embedded-chain argument, of the identification of the matrix $A$ , and of a reflection-type counting identity with two barriers.

Difficulty

The obvious route to $P(X_j=x)$ is to enumerate the sequences of arrivals and completions until the $j$ -th completion. Two features break a plain ballot-type count. First, the walk is reflected at the capacity $n$ : an arrival at a full room is lost, so trajectories with the same number of joining arrivals do not have the same probability, as the paper remarks (p. 10). Only after also fixing $Y_j$ do all trajectories become equally likely, which is why the closed form is a joint law. Second, the walk is absorbed when the customer enters service, so the count must also respect the lower boundary, and the subtracted binomial terms account for both constraints at once. Connecting the closed form back to the matrix $A$ of Theorem 2 requires identifying $A$ as the transition matrix of the queue size at consecutive service completions, a statement that itself relies on the memorylessness of the exponential clocks.

Formalization scope

The queue is represented by its event sequence. While the tagged customer waits, all servers are busy, so successive changes are i.i.d.: a service completion with probability $q$ , an arrival with probability $1-q$ . Every statement is made for an arbitrary probability space carrying a sequence $\varepsilon_0,\varepsilon_1,\dots$ of independent, measurable, $\{\mathrm{true},\mathrm{false}\}$ -valued variables with $P(\varepsilon_t=\mathrm{true})=q$ , for every $\lambda,\mu>0$ and $c\ge1$ (IsEventSeq). The reduction from the continuous-time queue to this sequence is the paper's own ("the probability that the next change will be a service completion", p. 9); it is disclosed, not formalized.
The counts are eventual values. The tagged customer's state (position, queue length, arrivals met, queue-filling arrivals) is updated event by event; $X_j$ , $Y_j$ , $M_j$ and the queue length at entry are suprema of non-decreasing sequences in $\mathbb N\cup\{\infty\}$ , so no default value enters. $X_j\le n$ everywhere.
Conventions. Queue length counts waiting customers, the tagged one included; $Y_j$ counts arrivals that make the queue length $n$ . Binomial coefficients are cast to real numbers before subtracting. $n\ge2$ in Theorem 3, as required by $j\in\{1,\dots,n-1\}$ and $\binom{\cdot}{n-2}$ . (3) is read as including probability $0$ off its two ranges. The third case of (2) is printed with $k$ for the column index $i$ and is formalized as $A(n,n-1)=A(0,0)=1$ .
Printed slip. Theorem 2 (2) says the number of additional customers met is distributed as row $k$ of $A^j$ ; that row is the law of the queue length at entry, and the number of new arrivals is that row shifted by $k-j$ . The milestone states both the queue-length form and the corrected count.
Ruled out. Defining $X_j$ , $Y_j$ or their law by the formulas of (3), or stating the goal about the matrix $A$ alone (which carries no $Y_j$ ), would make the goal empty; the counts are defined from the event dynamics only.
Needed and welcome. Lemmas on the strong Markov structure of the event sequence (the state after the first completion), the identification of $A$ , and a two-barrier reflection count are reusable beyond this mission. Proofs of the milestones, alternative arguments for (3), and a formal reduction from the continuous-time M/M/c/n queue to the event sequence are all welcome.

Selected references

R. Hassin, I. Meilijson, Y. Perlman, Queueing with Negative Network Effects, SSRN 4097977, version of July 2, 2022; Manufacturing & Service Operations Management, 2023. https://ssrn.com/abstract=4097977 , https://doi.org/10.1287/msom.2023.1223
P. Naor, The regulation of queue size by levying tolls, Econometrica 37(1), 15–24, 1969. https://doi.org/10.2307/1909200
W. Feller, An Introduction to Probability Theory and Its Applications, Vol. I, 3rd ed., Wiley, 1968, Ch. III (random walks and the reflection principle).

7 thms2 active usersReviewed

Completed

Markov Chain Operations Research Probability·Captain: mikedeng1

Diffusion of New Products with Heterogeneous Consumers: In a Complete Network, Heterogeneity in the External Influence Rates Always Slows Down the Expected AdoptionResearch Paper

Why heterogeneity matters

The Bass model describes how a new product spreads when consumers can adopt through external exposure and through contact with previous adopters. A homogeneous model assigns the same response rates to everyone. Actual networks can have consumers who respond at different rates, even when the average rate is known. For a fixed average, it is therefore useful to know whether replacing the individual rates by that average changes the expected adoption curve. Fibich and Golan study this question for a stochastic, individual-level Bass model on weighted networks Fibich and Golan, 2022.

This mission concerns heterogeneity in the external influence rates on a complete network. The paper's Theorem 3 says that, with a common total internal influence rate, heterogeneity strictly reduces the expected adopted fraction at every positive finite time. The result distinguishes the expected behavior of the individual-level process from a calculation made using only average external influence.

The adoption network

There are $M$ consumers, indexed by $i=1,\ldots,M$ . Each is either a nonadopter or an adopter. Everyone is a nonadopter at time zero, and adoption is permanent. A nonadopter $j$ adopts at rate

p_j+\sum_{k\in S}q_{k,j},

where $S$ is the current set of adopters, $p_j$ is the external influence rate, and $q_{k,j}$ is the influence of adopter $k$ on $j$ . The rates are nonnegative. Thus the adopter set is a finite continuous-time Markov chain: it can move from $S$ to $S\cup\{j\}$ , for $j\notin S$ , at precisely the rate above. This is equation (5) of the pinned preprint, p. 5.

Write $N(t)$ for the number of adopters at time $t$ . The paper studies the expected adoption fraction $f(t)=\mathbb E[N(t)]/M$ , equations (10)–(11) on p. 5. In this development, $f$ is evaluated from the transition matrix $\exp(tG)$ of the adopter-set generator $G$ . Its initial state is the empty adopter set.

On a complete network, let $q_j$ be the total incoming influence on consumer $j$ . The mild-heterogeneity convention divides it equally among the other $M-1$ consumers: $q_{k,j}=q_j/(M-1)$ when $k\ne j$ . The target case has a common $q_j=q>0$ . The homogeneous comparison network has the same $M$ and $q$ , and external rate $\bar p=M^{-1}\sum_i p_i$ at every node. These are the paper's equations (9), (12), and (34)–(35) on pp. 5–6 and 11.

Formalization targets

Theorem 3: slower expected adoption

For nonnegative $p_i$ that are not all equal, a common $q>0$ , and every $t>0$ , the goal is the strict comparison

f^{\mathrm{het}}(t;\{p_i\}_{i=1}^{M},q) < f^{\mathrm{hom}}(t;\bar p,q,M).

This is Theorem 3, p. 11. Its conclusion is about the original adopter-set process, not about a substitute curve defined from a comparison theorem. In particular, no ordering of the $p_i$ is imposed on the goal.

Intermediate distributions

If $t_k$ is the time between adoption $k-1$ and adoption $k$ , its CDF is $F_k(\tau)=\Pr(t_k\le\tau)$ . Lemma 5, p. 11 compares these CDFs on a complete graph when the external and total incoming influence rates are ordered together. It gives equality for $F_1$ and a strict heterogeneous-versus-homogeneous comparison for every later $F_k$ at positive $\tau$ .

Let $T_m=t_1+\cdots+t_m$ be the time of adoption $m$ . Equation (60) in Appendix D, p. 26 compares adoption times of auxiliary, independently coupled waiting-time sequences. It does not compare the actual dependent adoption times in the heterogeneous network, so it is not a milestone here. Equations (32) and (61) identify adoption-time probabilities with the generator process and its expected count pp. 10 and 26. A separate milestone records Lemma 4, p. 11, the two-consumer case.

What the result establishes

The strict inequality says that replacing unequal external adoption rates by their mean overstates the expected adopted fraction at every positive time, under the paper's complete-network and homogeneous-internal-influence assumptions. It supplies a precise direction for the bias caused by a homogeneous approximation. It does not assert a comparison for each individual consumer or for arbitrary network topology.

The theorem is stated in the cited paper, but its printed proof invokes Lemma 6, which claims independence of inter-adoption times. That claim fails for heterogeneous networks with three or more consumers. For $M=3$ , $q=1$ , and $(p_1,p_2,p_3)=(2,1,0)$ , the covariance of the second and third inter-adoption times is $-1/1944$ by exact rational calculation. The paper's printed argument therefore does not establish the required adoption-time dominance. This mission does not attribute that missing comparison to equation (60). Neither Theorem 3 nor the included milestones have a machine-checked proof here yet. A complete formalization would settle the theorem through a valid argument about the actual dependent adoption times.

Main difficulty

The total rate after an adoption depends on which consumer adopted. Consequently, the adopter count alone does not generally form a Markov chain, and successive inter-adoption times need not be independent. Comparing the marginal CDF of each holding time does not by itself compare the sum of those times. This is exactly where the paper's argument becomes incomplete: its independence claim cannot carry the comparison from Lemma 5 to the adoption times needed for Theorem 3. The missing step is a strict comparison between mixtures of waiting-time sums over possible adoption orders.

Formalization scope

Consumers are Fin M; adopter states are finite subsets. The Lean model uses real-valued nonnegative rates, a generator with jumps that add exactly one nonadopter, and the matrix exponential for transitions. The expected fraction is the weighted sum of transition probabilities from the empty set, divided by $M$ . A reusable finite-state jump-generator definition is separate from the paper-specific adoption rates. Complete-network weights use real division by $M-1$ and have zero diagonal. The goal's heterogeneity assumption implies $M\ge2$ , so that denominator is nonzero.

For the distribution milestones, an adoption order is a permutation, and a stage is numbered from zero in Lean: Lean stage $k$ corresponds to the paper's $t_{k+1}$ and $F_{k+1}$ . Each order has its jump-chain weight; conditional holding times use independent exponential measures with the corresponding positive stage rates. The stage rates appear in denominators and exponential measures, so the general generator-to-jump-chain milestone states positivity explicitly. It also carries the paper's standing assumption (7) that each consumer has positive total incoming peer influence; accordingly its network has at least two consumers. The paper's $m$ in $T_m$ remains one-based.

The paper does not define “heterogeneous in $p$ ” formally; Lean reads it as the existence of two unequal $p_i$ . Nonnegative $p_i$ are included because they are adoption rates. Lemma 5 additionally requires a positive initial total rate and some variation in $p$ or $q$ for its strict conclusion. The model uses the generator-defined $f(t)$ throughout: replacing it with a sum of adoption-time CDFs in the goal would erase the bridge the mission asks solvers to establish. Contributions on finite-chain laws, jump-chain representations, strict distribution comparisons, and the two-consumer calculation all serve the listed targets.

Selected references

Gadi Fibich and Amir Golan, Diffusion of new products with heterogeneous consumers, preprint arXiv:2102.05926v3, 2022; published in Mathematics of Operations Research, 2023. Pinned preprint.

6 thms2 active usersReviewed

Algorithmic Game Theory Economics Probability·Captain: mikedeng1

Does Competition Improve Analysts’ Forecast Informativeness?: Competition Lowers Informativeness Exactly When Payoffs Are Convex in Rank, Signals Are Correlated and Prior Uncertainty Is HighResearch Paper

Motivation

Sell-side analysts are ranked against each other. Published rankings, such as Institutional Investor's annual "All-Star" ranking cited in the paper, and the career outcomes tied to them, reward an analyst for being more accurate than peers, not only for being accurate. A common intuition holds that such competition disciplines analysts and makes their forecasts more informative for investors. Sanjay Banerjee's paper Does Competition Improve Analysts' Forecast Informativeness? (working paper, Alberta School of Business Research Paper No. 2017-311, 2017; later published in Management Science, doi:10.1287/mnsc.2019.3544) asks whether that intuition survives a model in which analysts best-respond to each other strategically.

The paper places itself next to the multi-sender cheap-talk literature (Krishna and Morgan 2001, Battaglini 2002). There, several senders typically reveal more than one. Two features separate this model: forecasts are scored against the realised state, and analysts' private signals are correlated conditional on the state. Its main result identifies exactly when competition makes forecasts less informative.

Setting

A state $\omega\in\{H,L\}$ has prior $\Pr(H)=q\in(0,1)$ ; for measuring information, $H=1$ and $L=0$ , so $\mathrm{Var}(\omega)=q(1-q)$ . Two risk-neutral analysts each observe a private signal $s_i\in\{h,l\}$ of precision $\gamma=\Pr(s_i=\omega\mid\omega)\in(\tfrac12,1)$ . Given the state, the signals have correlation $\rho\in[0,1]$ . With $\chi=\rho\gamma(1-\gamma)$ , each ordered pair of signals has conditional probability $\gamma^2+\chi$ if both equal the state, $(1-\gamma)^2+\chi$ if both differ from it, and $\gamma(1-\gamma)-\chi$ if they disagree.

Each analyst forecasts $m_i\in\{\hat h,\hat l\}$ . A symmetric strategy is $\sigma=(\sigma^h,\sigma^l)$ , with $\sigma^h=\Pr(\hat h\mid h)$ and $\sigma^l=\Pr(\hat l\mid l)$ . Under competition, an analyst whose forecast alone matches the state earns $w_1$ , the other earns $w_2$ , and identical forecasts earn $w_0$ each, with $w_1>w_0>w_2$ . The payoff convexity is

\varphi=\frac{w_1-w_0}{w_0-w_2},

and the payoff is convex if $\varphi>1$ , concave if $\varphi<1$ . In the benchmark, an analyst is paid for his own accuracy only.

A symmetric equilibrium is a $\sigma\in[0,1]^2$ with $\sigma^h\ge1-\sigma^l$ such that, for each signal, the prescribed probability of a truthful forecast maximises the analyst's expected payoff, computed by Bayes' rule, when the other analyst plays $\sigma$ . It is pooling if $\sigma^h=1-\sigma^l$ and separating if $\sigma=(1,1)$ . A most informative equilibrium is an equilibrium that is coordinatewise at least every other equilibrium of the same game. Forecast informativeness is the posterior precision normalised by the prior precision,

\Pi(\sigma)=\frac{\mathrm{Var}(\omega)}{E_{m_i,m_j}\big[\mathrm{Var}(\omega\mid m_i,m_j)\big]}-1 .

Finally, the separation threshold of the rank game is

\check q_{\min}=\gamma-\chi\,\frac{\varphi-1}{(1-\gamma)\varphi+\gamma}.

Formalization targets

Goal: Proposition 5 (B.1), corrected

Fix $\gamma\in(\tfrac12,1)$ , $\rho\in[0,1]$ and $w_1>w_0>w_2$ with $\varphi\ne1$ , and restrict to $q\ge\tfrac12$ , as the paper does ("Results for $q<\frac12$ are symmetric"). Let $\sigma$ and $\sigma_B$ be most informative equilibria of the rank game and of the benchmark at $q$ . Then

\Pi(\sigma)<\Pi(\sigma_B)\ \Longrightarrow\ \varphi>1,\ \rho>0,\ \check q_{\min}<q\le\gamma,

and conversely, if $\varphi>1$ and $\rho>0$ , then for every $q\in[\tfrac12,1)\cap(\check q_{\min},\gamma]$ both most informative equilibria exist and every such pair satisfies $\Pi(\sigma)<\Pi(\sigma_B)$ .

The paper prints " $q<\gamma$ ". At $q=\gamma$ informativeness still drops (for $\gamma=0.7$ , $\rho=0.4$ , $\varphi=3$ : $\Pi=0.147<\Pi_B=0.232$ ). On $[\tfrac12,\check q_{\min}]$ it does not drop, because the separating profile remains an equilibrium. The interval $(\check q_{\min},\gamma]$ is the paper's own reading: " $\Pi_{\varphi>1}<\Pi_B$ at $q\in(\check q_{\min},\gamma]$ " (p. 26).

Milestones

The milestones are the paper's numbered results that the proof uses:

the benchmark's equilibria (Lemma 1, with the interval corrected to $[1-\gamma,\gamma]$ );
the separation threshold (Claim 1);
the comparative statics of the net payoffs (Claim 2);
the comparison function $g_l-g_h$ (Claim 3);
the exclusion of fully mixed and semi-separating equilibria (Claims 4–5);
the characterisation of the most informative equilibrium without and with correlation (Proposition 2 (A), Proposition 3 (A.1)–(A.2));
the monotonicity of $\Pi$ (Claim 7).

Significance

The result. Proposition 5 (B.1) is the paper's main counterintuitive finding. Convex rank incentives combined with correlated information make analysts understate their private signals in order to differentiate themselves, and the market learns less than it would from two analysts who ignore each other. The conditions are sharp: with uncorrelated signals or a concave payoff, competition never lowers informativeness at $q\ge\frac12$ . This is relevant to the design of analyst rankings and of tournament incentives for forecasters more generally.

Formalizing it. The result is proved on paper through seven claims and a case analysis over regimes of $(\rho,\varphi,q)$ . The case analysis contains slips, such as the empty interval in Lemma 1, a sign error in (B.28), and boundary cases $\varphi=\bar\varphi$ and $q=\gamma$ assigned to the wrong regime. A machine-checked proof would settle the exact statement. To the best of our knowledge none of these results has been formalized; the mission produces the first formal model of this game.

Difficulty

Each analyst's best response depends on the other's strategy through a conditional law of the other's forecast, which is affine in $\sigma$ , and through Bayesian posteriors, which are ratios of such terms. The equilibrium conditions are therefore piecewise-affine inequalities whose sign pattern changes with $(\rho,\varphi,q)$ . The obvious argument would compute a single equilibrium and compare informativeness. It fails because the goal speaks of the most informative equilibrium. One must show that no other equilibrium dominates it coordinatewise, and in the high-convexity, high-correlation regime the relevant equilibrium is fully mixed and is defined through an implicit root ( $\ddot\sigma^l$ ). The "only if" half requires excluding a decrease in every other regime, including $q>\gamma$ , where the benchmark pools and one needs $\Pi\ge0$ .

Formalization scope

States, signals and forecasts are Bool (true = H, h, ĥ). A strategy is a pair σ : ℝ × ℝ, and the equilibrium set carries the restriction $\sigma^h\ge1-\sigma^l$ of p. 9. Expected payoffs are conditional expectations of the rank payoff (3) under the joint signal law and Bayes' rule. The equilibrium condition is that the prescribed mixing probability maximises the expected payoff over all of $[0,1]$ . The benchmark pays $1$ for a correct forecast, a positive rescaling of the paper's $\pi_a=W$ . A forecast pair of probability zero contributes zero to the expected posterior variance. The paper's standing restriction $q\ge\frac12$ is part of the goal: below one half the decrease occurs on the mirror interval $[1-\gamma,1-\check q_{\min})$ , and the condition $q\le\gamma$ would be vacuous.

The trivializing formalizations are ruled out. The net payoffs $\Delta U$ and informativeness $\Pi$ are computed from the primitives, never from the paper's closed forms (A.13)–(A.14) or Lemma 3. The "if" half asserts that the most informative equilibrium exists. The benchmark value is the benchmark game's own most informative equilibrium, not $\Pi(1,1)$ written into the statement.

The "Furthermore, the decrease in information revelation increases with payoff convexity" clause is not part of the goal. Neither are Proposition 5 (A) and (B.2), Propositions 2 (B) and 3 (B), Lemmas 2–3, Proposition 4, Claim 6 and Appendix C. Corrected milestones are labelled in their titles:

Lemma 1: the interval is $[1-\gamma,\gamma]$ ;
Claim 3 (B.2) and Proposition 3 (A.2): $\varphi>\bar\varphi$ ;
Proposition 3 (A.2): on $[1-\bar q,\bar q]$ , the fully mixed formula's coordinates lie in $(0,1)$ strictly inside the interval, and one of them equals $1$ at each endpoint;
Proposition 3 (A.1): extended to $\varphi\le\bar\varphi$ ;
Claim 3 (C): restricted to $\sigma^h\ge1-\sigma^l$ .

A complete development needs:

finite sums over Bool;
real field arithmetic for rational functions of $(q,\gamma,\rho,\varphi,\sigma)$ ;
an intermediate value argument for the root $\ddot\sigma^l$ ;
the concavity fact that posterior variance does not exceed prior variance on average.

The finite Bayesian-game layer (symmetric equilibria of a two-player game with binary types) is reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal from the milestones.

Selected references

S. Banerjee, Does Competition Improve Analysts' Forecast Informativeness?, Alberta School of Business Research Paper No. 2017-311 (13 Nov 2017), the version formalized here; published in Management Science, 2020. https://doi.org/10.1287/mnsc.2019.3544
V. Krishna and J. Morgan, A Model of Expertise, Quarterly Journal of Economics 116(2), 2001. https://doi.org/10.1162/00335530151144159
M. Battaglini, Multiple Referrals and Multidimensional Cheap Talk, Econometrica 70(4), 2002. https://doi.org/10.1111/1468-0262.00335
V. P. Crawford and J. Sobel, Strategic Information Transmission, Econometrica 50(6), 1982. https://doi.org/10.2307/1913390

32 thms2 active users

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Naive Feature Selection: A Nearly Tight Convex Relaxation for Sparse Naive Bayes: The Sparse Multinomial Relaxation Bound Is Tight up to Four Features, ψ(k − 4) ≤ ϕ(k) ≤ ψ(k) ≤ ϕ(k + 4)Research Paper

Motivation

Naive Bayes is one of the oldest and cheapest classifiers for text and count data: given word counts for documents in two classes, it fits one multinomial distribution per class by maximum likelihood and classifies by the likelihood ratio. Its cost is a single pass over the data. In high-dimensional applications (text, genomics) one also wants the classifier to depend on few features, both for interpretability and to discard noise. Imposing that the two class distributions differ in at most $k$ coordinates turns maximum-likelihood fitting into a cardinality-constrained, nonconvex problem.

Askari, d'Aspremont and El Ghaoui (arXiv:1905.09884, Mathematics of Operations Research, 2024) show that the Lagrangian dual of this sparse problem is a one-dimensional convex problem solvable by bisection at essentially the cost of naive Bayes itself, and that its value is within a shift of four features of the true optimum. The shift comes from a duality-gap bound for separable problems in the line of Aubin and Ekeland (1976) and Ekeland and Temam, based on the Shapley–Folkman lemma.

Setting

There are $m$ features. A nonnegative data matrix with labels $\pm1$ enters only through the class sums $f^+,f^-\in\mathbb R^m$ (the total count of each feature in each class), assumed entrywise positive. Write $g=f^++f^-$ and $S=\mathbf 1^\top g$ .

The sparse multinomial naive Bayes problem (SMNB) at sparsity level $k$ is

\phi(k)=\max_{\theta^+,\theta^-\in[0,1]^m}\ f^{+\top}\log\theta^++f^{-\top}\log\theta^-\quad\text{s.t.}\quad \mathbf 1^\top\theta^+=\mathbf 1^\top\theta^-=1,\quad \|\theta^+-\theta^-\|_0\le k,

where $\|\theta^+-\theta^-\|_0$ counts the coordinates in which the two class distributions differ. Without the last constraint the problem is ordinary naive Bayes.

For a vector $c$ , $s_k(c)$ is the sum of its $k$ largest entries. Let

\tilde C=f^+\circ\log f^++f^-\circ\log f^--g\circ\log g,\qquad h(\alpha)=\tilde C-f^+\log\alpha-f^-\log(1-\alpha)\quad(0<\alpha<1),

and $C=g^\top\log g-S\log S$ . The relaxation (USMNB) has value

\psi(k)=C+\min_{\alpha\in(0,1)}s_k\big(h(\alpha)\big).

It is a convex problem in one variable. Its dual (D) is a concave maximization over $x\in[0,1]^m$ with $\mathbf 1^\top x\le k$ , which plays the role of a fractional feature-selection vector.

Formalization targets

Goal: Theorem 3.6

For $4\le k<m$ ,

\psi(k-4)\le\phi(k)\le\psi(k)\le\phi(k+4).

The constant four does not depend on $m$ , $k$ or the data. Numerically it is not tight (a shift of one suffices on random instances), but the goal keeps the paper's constant.

Milestones

Lemma 3.11: $s_k(c)=\min_{\lambda\ge0}\lambda k+\sum_i\max(0,c_i-\lambda)$ for $c\ge0$ , the optimal multipliers, and the structure of solutions of the dual linear program (36).
§3.4: $w(\mu)\ge v(\mu)$ for $\mu>0$ , the inequality behind the top- $k$ form.
§3.4: the Lagrangian dual of (SMNB) equals $-S+\min(17)$ , which equals $\psi(k)$ .
Theorem 3.2: $\phi(k)\le\psi(k)$ .
Theorem 3.5: the duality-gap bound $h_P(\bar p)\le h_P(0)^{**}+(m+1)\max_i\rho(f_i)$ for separable problems.
The lack of convexity of $\mathbf 1_{x\ne y}$ on $[0,1]^2$ is one, its convex envelope being $|x-y|$ .
Proposition 3.7: strong duality between (USMNB) and its dual (D).
Proposition 3.8: an optimal solution of (D) with $J$ fractional coordinates yields a feasible point of (SMNB) at level $k+|J|$ whose value lies between $\phi(k)$ and $\phi(k+|J|)$ .
Proposition 3.9: (D) has an optimal solution with at most four fractional coordinates.

Milestones 1–6 follow the paper's proof of Theorem 3.6; milestones 7–9, on top of 1–4, are the paper's second, constructive route to the upper bound $\psi(k)\le\phi(k+4)$ .

Significance

The theorem certifies that a convex problem of negligible cost brackets a nonconvex, combinatorial maximum-likelihood problem: the relaxation's value at $k$ lies between the true values at $k$ and $k+4$ . Whenever $\psi$ varies slowly in $k$ , which the paper observes past the "elbow" in the number of relevant features, the duality gap is small, and Propositions 3.8–3.9 turn the relaxation's solution into a sparse classifier with at most four extra features. The paper uses this to run feature selection on data sets with millions of features.

The results are proved in the paper (Theorem 3.5 is quoted from the literature). None is formalized. Formalizing them yields the perturbation-function duality-gap bound for separable nonconvex problems as a reusable statement, a verified variational formula for top- $k$ sums, and a check of a printed formula: the dual (D) as printed carries a spurious term $-(x^\top g)$ , and the formal statement uses the corrected objective.

Difficulty

The lower and middle inequalities are weak duality once the dual is computed, and computing it is a separable calculation. The upper inequality $\psi(k)\le\phi(k+4)$ is the content: it bounds a duality gap, and nothing in the one-dimensional structure of (USMNB) gives it. The naive approach, rounding the fractional $x$ of (D) to its top $k$ coordinates, has no a priori control on the loss. Both of the paper's routes need a Shapley–Folkman type argument, in which the number of nonconvex contributions is bounded by the number of constraints plus one. The Shapley–Folkman lemma itself is not in Mathlib (it is an open goal on the platform), and Theorem 3.5 also requires conjugates of extended-valued functions and the convex envelope of a sum of separable terms.

Formalization scope

Features are indexed by Fin m, with fp fm : Fin m → ℝ entrywise positive. This positivity is stated on p. 7 and is needed because the formulas take $\log f^\pm$ . The standing assumption $k<m$ of §3.1 is carried by every statement about (SMNB). The commitments are:

$\phi(k)$ is a real supremum over $\theta^\pm\in(0,1]^m$ . Strict positivity matches the paper's value ( $f^\pm>0$ makes the objective $-\infty$ at any $\theta_i=0$ ) and avoids Lean's $\log0=0$ .
$s_k$ sums the largest $\min(k,m)$ entries, including for signed vectors. On the nonnegative vectors used by the relaxation, this equals the maximum over index sets of size at most $k$ from p. 6.
$\psi(k)$ minimizes over the open interval $(0,1)$ , where $h$ is defined, and the constant $C=g^\top\log g-S\log S$ of p. 8 is built in. Taking $C$ as a parameter, or defining $\psi$ as the Lagrangian dual, would make the goal false or turn milestone 3 into a definition; both are excluded.
The Lagrangian dual's inner maximum is over $\theta^\pm\in(0,\infty)^m$ , which is the problem the paper's closed forms solve. With the printed box $[0,1]^m$ the identity of milestone 3 fails on some instances.
(D) is used in its corrected form, with $z=\mathbf 1-x$ eliminated.
§3.6 uses EReal-valued functions on Fin d → ℝ. The conjugate is a supremum (p. 9 prints an infimum), and finiteness of each $\rho(g_{ji})$ is added in Theorem 3.5 so that $\bar p$ is a real vector.
In the paper's proof of Theorem 3.6, the equality constraints of (25) are not of the form " $\le b+u$ " required by (P). Because the objective is decreasing in $q$ and $r$ , replacing them by inequalities leaves the values unchanged.

Proposition 3.8 is stated with the additional conclusion that the constructed point's value is at least the optimum of (D). Its proof establishes this, and without it the statement is met by a maximizer of $\phi(k)$ and says nothing about (D).

A complete development needs Lagrangian duality for a separable problem, the perspective of $x\log x$ , top- $k$ sums and their LP dual, Fenchel conjugates of extended-valued functions, and a Shapley–Folkman lemma. The last three are reusable well beyond this mission, and contributions there are welcome.

Selected references

A. Askari, A. d'Aspremont, L. El Ghaoui, Naive Feature Selection: A Nearly Tight Convex Relaxation for Sparse Naive Bayes, Mathematics of Operations Research, 2024. https://arxiv.org/abs/1905.09884 (v4 used here).
J.-P. Aubin, I. Ekeland, Estimates of the duality gap in nonconvex optimization, Mathematics of Operations Research 1(3), 1976. https://doi.org/10.1287/moor.1.3.225
I. Ekeland, R. Temam, Convex Analysis and Variational Problems, SIAM Classics in Applied Mathematics, 1999, Appendix I. https://doi.org/10.1137/1.9781611971088
R. M. Starr, Quasi-equilibria in markets with non-convex preferences, Econometrica 37(1), 1969. https://doi.org/10.2307/1909201

13 thms2 active usersReviewed

Completed

Control Theory Operations Research Probability+1·Captain: mikedeng1

Optimal Retirement Under Partial Information: If a Dual Multiplier and a Dual-Optimal Retirement Time Meet the Budget, Their Plan Is Optimal and There Is No Duality GapResearch Paper

Motivation

When to stop working is one of the largest financial decisions a household makes, and it interacts with how much to consume and how to invest. In the continuous-time literature the decision is modelled as an optimal stopping time chosen jointly with consumption and portfolio controls; the standard tool is convex duality, which turns the coupled control–stopping problem into a family of pure optimal stopping problems indexed by a Lagrange multiplier. Dybvig and Liu (2010) and Yang and Koo (2018) solved such problems when the investor knows the expected return of the stock.

In practice the expected return is not observed. Chen, Jeon and Wong (SSRN 3683553, 2021; published in Mathematics of Operations Research) set up the retirement problem when the drift is unobserved and the agent's decisions may depend only on the stock price history. Their Proposition 2.4 is the bridge between the primal problem and the dual optimal stopping problem in that setting, and Sections 3–5 of the paper apply it to a hidden Markov drift (Wonham filter) and a Kalman–Bucy model.

Setting

A market has a bond $B_t=e^{rt}$ with a constant rate $r\neq 0$ and a stock with constant volatility $\sigma>0$ and drift $\mu_t$ ,

S_t=S_0\exp\Bigl(\int_0^t\mu_u\,du-\tfrac{\sigma^2}{2}t+\sigma W_t\Bigr),

the solution of $dS_t=\mu_tS_t\,dt+\sigma S_t\,dW_t$ , where $W$ is a Brownian motion with respect to a filtration $\mathcal F$ and $\mu$ is $\mathcal F$ -progressively measurable. The agent observes only $S$ : the observation filtration $\mathcal F^S_t$ is generated by $(S_u)_{u\le t}$ and the null sets. With the risk premium $\theta_t=(\mu_t-r)/\sigma$ , the density $Z_t=\exp(-\frac12\int_0^t\theta^2ds-\int_0^t\theta\,dW)$ is assumed to be a martingale (Assumption 2.1), $d\tilde{\mathbb P}=Z_T\,d\mathbb P$ , and the projected density is $\mathcal Z_t=\mathbb E[Z_T\mid\mathcal F^S_t]$ .

The agent has horizon $T$ , a mandatory retirement date $T_1\le T$ , labour income at rate $\xi\ge0$ until retirement, a utility cost of labour $\ell>0$ , a discount rate $\beta>0$ and utilities $U_1$ (consumption) and $U_2$ (terminal wealth) satisfying Assumption 2.2 (smooth, strictly concave, Inada, polynomial bounds on the inverse marginal utilities $I_1,I_2$ ). The quantity $b(t)=-\frac{\xi}{r}(1-e^{r(t-T_1)})$ for $t<T_1$ (and $0$ after) is minus the value of remaining labour income. A plan is an $\mathcal F^S$ -adapted consumption rate $c$ , wealth $H$ and retirement time $\tau$ (an $\mathcal F^S$ -stopping time in $[0,T_1]$ , with $R_s=\mathbf 1\{s\ge\tau\}$ ). The feasible set $\mathcal B(x)$ consists of plans with $H_0=x$ , $H_t\ge(1-R_t)b(t)$ and the budget constraint

\tilde{\mathbb E}\Bigl[\tfrac{H_t-b(t)(1-R_t)}{B_t}+\int_s^t\tfrac{c_u}{B_u}du-\int_s^t\tfrac{b(u)}{B_u}dR_u\Bigm|\mathcal F^S_s\Bigr]\le\tfrac{H_s-b(s)(1-R_s)}{B_s},\quad 0\le s<t\le T.

The primal value is $V(0,x,0)=\sup_{\mathcal B(x)}\mathbb E[\int_0^Te^{-\beta t}(U_1(t,c_t)-\ell(1-R_t))dt+e^{-\beta T}U_2(T,H_T)]$ ; $V(0,x,1)$ is the same with $\tau\equiv0$ .

The dual uses $y_s=y\,e^{\beta s}\mathcal Z_s/B_s$ and the convex duals $\tilde U_i(t,y)=\sup_{c>0}[U_i(t,c)-yc]$ :

\mathbf L(0,y,1)=\mathbb E\Bigl[\int_0^Te^{-\beta s}\tilde U_1(s,y_s)ds+e^{-\beta T}\tilde U_2(T,y_T)\Bigr],

\mathbf L(0,y,0)=\sup_{\tau}\mathbb E\Bigl[\int_0^\tau e^{-\beta s}(\tilde U_1(s,y_s)-\ell)ds+e^{-\beta\tau}\bigl(\mathbf L(\tau,y_\tau,1)+y_\tau b(\tau)\bigr)\Bigr],

the supremum over $\mathcal F^S$ -stopping times $\tau\in[0,T_1]$ . For a retirement time $\hat\tau$ , the budget cost of the dual candidate $c^*_s=I_1(s,y_s)$ , $H^*=I_2(T,y_T)$ , $R^*=\mathbf 1\{\cdot\ge\hat\tau\}$ is $\mathcal X(0,y)=\tilde{\mathbb E}[H^*/B_T+\int_0^Tc^*_u/B_u\,du-b(\hat\tau)/B_{\hat\tau}]$ ; Assumption 2.3 asks it to be finite.

Formalization targets

Goal: Proposition 2.4, verification clause (p. 13)

If $x>b(0)$ , $y^*>0$ , and $\hat\tau$ is optimal in the stopping problem defining $\mathbf L(0,y^*,0)$ with

\mathcal X(0,y^*)=x-b(0)\qquad(21),

then the candidate $(c^*,H^*,R^*)$ belongs to $\mathcal B(x)$ , is optimal, and

V(0,x,0)=\min_{y>0}\bigl\{\mathbf L(0,y,0)+y(x-b(0))\bigr\}=\mathbf L(0,y^*,0)+y^*(x-b(0)).

The retired case is the same with $\mathbf L(0,y,1)$ , budget $x>0$ and $\mathcal X_1+\mathcal X_2=x$ .

Milestones

The change of measure $\tilde{\mathbb E}[M]=\mathbb E[\mathcal Z_tM]$ for $\mathcal F^S_t$ -measurable $M$ (p. 6).
The Fenchel identity $\tilde U(t,y)=U(t,I(t,y))-yI(t,y)$ (11).
Weak duality after retirement (13): $J_1(c,H)\le\mathbf L(0,y,1)+yx$ on $\mathcal B_1(x)$ .
Weak duality with the retirement option (14), (16): $J(c,H,R)\le\mathbf L(0,y,0)+y(x-b(0))$ on $\mathcal B(x)$ .
The equality chain of the proof (p. 13): $\mathbf L(0,y^*,0)+y^*(x-b(0))$ equals the candidate's objective.
Feasibility (p. 14): under (21) the candidate lies in $\mathcal B(x)$ .

Significance

Proposition 2.4 is what makes the paper's four-step recipe (p. 14) work: choose a filter satisfying Assumption 2.3, solve the dual optimal stopping problem, solve for the multiplier, and read off consumption, terminal wealth and retirement time. It separates filtering from optimization: any filter whose projected density meets Assumption 2.3 can be combined with the dual stopping problem. The hidden-Markov results of Section 3 (variational inequality, free boundary, optimal strategies) rest on it.

The result is proved in the paper and has no machine-checked proof. The mission produces a formal statement of the verification direction of the duality theorem with the observation filtration, the projected density, and an optimal stopping problem inside the dual, and a decomposition of its proof into weak duality, the Fenchel identity, and the feasibility of the dual candidate.

Difficulty

The algebra of each step is short; the difficulty is measure-theoretic. Weak duality needs the change of measure from $\tilde{\mathbb P}$ to $\mathbb P$ for processes adapted to $\mathcal F^S$ , Fubini, and the tower property at a stopping time (the term $e^{-\beta\tau}y_\tau b(\tau)$ requires optional sampling for the continuous martingale $\mathcal Z$ ). The feasibility step must construct a wealth process: $H_s=B_sK_s+b(s)(1-R^*_s)$ with $K_s$ the conditional expected discounted remaining cost of the candidate, then check $H_0=x$ , the floor $H\ge(1-R^*)b$ and (8); it also needs $\int_0^Tc^*_s\,ds<\infty$ a.s., which uses that $\mathcal Z$ is bounded away from $0$ on $[0,T]$ along each path together with the bounds of Assumption 2.2(ii). Proving that $\mathbf L(0,y,0)$ is finite for every $y$ (so that weak duality compares real numbers) is part of the work.

A natural first idea is to treat the dual optimal stopping time as fixed in $y$ . It is not: $\hat\tau$ depends on $y$ , which is exactly what breaks the existence clause below.

Formalization scope

Conventions. Everything is posed at $t=0$ , the agent's problem of Definition 2.6: $\mathcal F^S_0$ is trivial, so $V$ , $\mathbf L$ and $\mathcal X$ are numbers. The paper's statement at a general time $t$ concerns conditional value fields that it does not construct and is not formalized. The stock is defined by the explicit solution of (1). The Itô integral $\int\theta\,dW$ is an explicit process constrained by a dyadic-Itô-sum characterisation built on the published EthierKurtz.itoStepSum. $\tilde{\mathbb P}$ is withDensity of $Z_T$ ; $\mathcal Z_t$ is the conditional expectation $\mathbb E[Z_T\mid\mathcal F^S_t]$ , used in time integrals through a continuous, everywhere positive, $\mathcal F^S$ -adapted version (such versions exist and are indistinguishable). Retirement indicators are encoded by stopping times; the atom of $dR$ at $\tau$ is counted in (14) and (17) also when $\tau=0$ . The dual-optimal stopping time is a hypothesis ("any optimal stopping time of (14) at $y^*$ "), which covers the paper's hitting time $\hat\tau_{0,y}$ (whose optimality the paper cites from Peskir–Shiryaev). Added hypotheses: $c>0$ and $H_T>0$ in the primal class (the utilities live on $(0,\infty)$ ), integrability of the primal objective and of the budget integrands, and integrability of $\tilde U_1(s,y_s)$ , $\tilde U_2(T,y_T)$ for every $y>0$ . Conclusions are greatest/least elements, not real suprema.

The existence clause. The printed Proposition 2.4 also asserts that for every $x>b(0)$ a multiplier $y^*$ with (21) exists. That clause is false in general and is not posed. Take $\mu\equiv r$ (so $\theta\equiv0$ , $Z\equiv\mathcal Z\equiv1$ , $\tilde{\mathbb P}=\mathbb P$ ), $\beta>r$ , $\xi>0$ and CRRA utilities. Then $y_s=ye^{(\beta-r)s}$ is deterministic and (14) reduces to $\mathbf L(0,y,1)-\min_{\tau\in[0,T_1]}h_y(\tau)$ with $h_y(\tau)=y\frac{\xi}{r}(e^{-r\tau}-e^{-rT_1})+\ell\frac{1-e^{-\beta\tau}}{\beta}$ . Since $h_y'(\tau)=e^{-r\tau}(\ell e^{-(\beta-r)\tau}-y\xi)$ changes sign at most once, from $+$ to $-$ , the optimal stopping times are $\{0\}$ below a threshold $y_0$ and $\{T_1\}$ above it. So $\mathcal X(0,\cdot)$ jumps down by $-b(0)=\frac{\xi}{r}(1-e^{-rT_1})>0$ at $y_0$ , and every $x$ with $x-b(0)$ in the gap has no $y^*$ . The paper's own proof begins "Suppose that such a $y^*$ exists", and p. 14 describes the result as transforming "the solution of the duality approach, if it exists" into the primal solution; the mission poses exactly that.

Ruling out trivial readings. All decisions and stopping times are $\mathcal F^S$ -adapted, not $\mathcal F$ -adapted (otherwise the statement is the full-information one). $\mathcal Z$ is the projection $\mathbb E[Z_T\mid\mathcal F^S_t]$ , not $Z_t$ or $1$ . The supremum in (14) ranges over all $\mathcal F^S$ -stopping times in $[0,T_1]$ , and the same $\hat\tau$ enters (21) and $R^*$ . The budget constraint is the conditional family (8) for all $0\le s<t\le T$ , not only $s=0$ , $t=T$ . Integrability is a hypothesis or a class condition everywhere, so no Bochner integral or conditional expectation defaults to $0$ .

Infrastructure and contributions. A complete development needs: change of measure and pull-out properties for withDensity and condExp; optional sampling for continuous martingales at bounded stopping times; Fubini on $[0,T]\times\Omega$ ; elementary convex analysis for the Fenchel identity and the inverse marginal utility; and the existence of a continuous version of the projected density. The change-of-measure and Fenchel milestones are reusable in any dual approach to utility maximisation. Proofs of any milestone, alternative decompositions, and lemmas establishing the finiteness of $\mathbf L(0,y,0)$ are welcome.

Selected references

K. Chen, J. Jeon, H. Y. Wong, Optimal retirement under partial information, SSRN 3683553, version of June 8, 2021; Mathematics of Operations Research, 2021. https://ssrn.com/abstract=3683553
P. Dybvig, H. Liu, Lifetime consumption and investment: Retirement and constrained borrowing, Journal of Economic Theory 145(3), 885–907, 2010. https://doi.org/10.1016/j.jet.2009.08.003
Z. Yang, H. K. Koo, Optimal consumption and portfolio selection with early retirement option, Mathematics of Operations Research 43(4), 1378–1404, 2018. https://doi.org/10.1287/moor.2017.0909
P. Lakner, Utility maximization with partial information, Stochastic Processes and their Applications 56, 247–273, 1995. https://doi.org/10.1016/0304-4149(94)00073-3
G. Peskir, A. Shiryaev, Optimal Stopping and Free-Boundary Problems, Birkhäuser, 2006. https://doi.org/10.1007/978-3-7643-7390-0

16 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research·Captain: mikedeng1

Managing Operations of a Hog Farm Facing Volatile Markets: Optimality of the Price-Dependent Multi-Threshold Hold-Fulfill-Sell Sales Allocation PolicyResearch Paper

Why the sales allocation problem matters

A hog producer selling to both a meatpacker and an open market faces a weekly allocation choice. The meatpacker contracts for a fixed quantity, pays different rates for underweight and regular-weight hogs, and charges for any shortfall. The open market has separate prices for the two weight classes. Holding an underweight hog costs money now but makes it regular-weight next week. These features make a single “sell or hold” rule inadequate: fulfilling the contract changes the value of the next hog allocated to either market. Kouvelis, Liu, Qiu and Turcic model this setting and state a price-dependent, multiple-threshold sales policy in Proposition 1 of their March 6, 2023 preprint.

The stated policy is of direct interest for inventory decisions with quality upgrading and contractual penalties. It also provides a precise test case for dynamic programming with continuous stock decisions, stochastic prices, and a capacity-constrained contract. The mission concerns the mathematical policy statement, rather than the paper’s empirical estimates or numerical comparisons.

Setting and notation

At the start of period $t\in\{1,\ldots,t_M\}$ , the producer observes $s_t=(s^1_t,s^2_t)$ underweight and regular-weight hogs and the price vector $P_t=(p^C_t,p^1_t,p^2_t,c^H_t,c^P_t)$ . The contract requires $q$ hogs. A regular-weight hog sent to the contract earns $p^C_t$ ; an underweight one earns $(1-\alpha)p^C_t$ . Open-market prices are $p^1_t\le p^2_t$ . Holding costs $c^H_t$ per hog, and a contract shortfall costs $c^P_t$ per missing hog. The discount factor is $\beta$ .

The decision is $y_t=(y^1_t,y^2_t)$ sent to the contract and $z_t=(z^1_t,z^2_t)$ held. Open-market sales are $x^i_t=s^i_t-y^i_t-z^i_t$ . Every decision is nonnegative; $y^1_t+y^2_t\le q$ and $y^i_t+z^i_t\le s^i_t$ . The immediate reward is

r_t=p^C_t\bigl(y^2_t+(1-\alpha)y^1_t\bigr) +\sum_{i=1}^{2}p^i_t(s^i_t-y^i_t-z^i_t) -c^H_t(z^1_t+z^2_t)-c^P_t(q-y^1_t-y^2_t).

Newly available hogs next period are $W_{t+1}=(W^1_{t+1},W^2_{t+1})$ . Both classes of held hogs enter the regular-weight pool, so $S_{t+1}=(W^1_{t+1},W^2_{t+1}+z^1_t+z^2_t)$ . The value function $V_t$ is the maximum expected discounted reward from periods $t$ through $t_M$ , with $V_{t_M+1}=0$ , as in equations (4) and (7a)–(7c) of the preprint.

For total holding $Z$ , write $G_t(Z)=\beta\mathbb E_t[V_{t+1}(W^1_{t+1},W^2_{t+1}+Z)]-c^H_t Z$ . Its increments are the holding margin. The fulfillment margins are $(1-\alpha)p^C_t+c^P_t$ and $p^C_t+c^P_t$ ; the spot margins are $p^1_t$ and $p^2_t$ . A break-even level for margin $v$ is the least nonnegative $Z$ at which every forward increment of $G_t$ is no greater than $v$ times the increment. The mission uses this level truncated at $s^1_t+s^2_t$ .

Formalization targets

The first targets are concavity of the value and action-value functions (Lemma 1), preservation of concavity in total holdings (Proposition 1, proof Step 1), and the holding-margin bound corresponding to Lemma 2(1). The one-period attainment result from Proposition 1, proof Step 2, connects those properties to the explicit actions. These are the four milestones.

The goal is the corrected part of Proposition 1, Cases 1(a), 1(b), 2(a), and 2(b). In each case, the indicated action must satisfy the feasibility constraints and attain the dynamic-programming value:

v_t(y_t,z_t;s_t,P_t)=V_t(s_t,P_t).

The cases split first on $p^2_t>p^C_t+c^P_t$ or $p^2_t\le p^C_t+c^P_t$ , then on the underweight fulfillment and spot margins. The explicit quantities are in the goal theorem. Its thresholds are computed from $G_t$ and the observed stock and prices, so the target is a policy for the original dynamic program. Proposition 1 also prints Case 2(c), but its multi-period formula is false under the paper’s stated assumptions and the additional no-arbitrage bound below; this mission does not assert it.

What the result provides

The result identifies feasible, optimal contract, spot-market, and holding quantities in four observable price regimes. It gives a policy rather than an existence statement: a producer can determine the action from the current stock, prices, and three break-even levels. The holding thresholds are linked to the actual continuation value, which matters when future penalties or regular-weight prices change.

The preprint supplies a proof on paper; these particular Lean statements do not yet have verified proofs. Formalizing them would yield a checked dynamic program and reusable facts about a concave continuation value, a shared holding pool, and a linear contract capacity. The corrected statement also separates the regimes that the available numerical checks support from the printed Case 2(c), which has a concrete counterexample. The four milestones expose the mathematical obligations needed to complete the verified result.

Main difficulty

The continuation value depends on the sum $z^1_t+z^2_t$ , while the two pools have different fulfillment and spot prices and share one contract capacity. A comparison of each pool’s holding and selling margins in isolation therefore does not settle the allocation: holding one pool changes the marginal value of holding the other. The dynamic value is also defined by a supremum over a continuous feasible polytope and an expectation over future data. The central difficulty is obtaining a well-defined, concave value function and then showing that each explicit threshold action attains it. The paper’s no-arbitrage assumption controls expected contract and spot price changes, but does not control a jump in the next period’s contract penalty; Lemma 2(1) fails without an additional bound.

Formalization scope

Lean uses real-valued stocks and decisions, a positive finite horizon, and a time-indexed Markov kernel on an exogenous information state $\omega$ . Taking $\omega$ to include the observed history represents the paper’s general adapted price and supply process; the formalization imposes no independence between supply and prices. Prices and supplies are measurable, nonnegative, and uniformly bounded. These are disclosed well-posedness additions that keep the expectations integrable and the real supremum finite. It also assumes $0<\beta\le1$ , $q>0$ , $0<\alpha<1$ , and $p^1_t\le p^2_t$ .

Assumption 1 from page 14 is retained. The added condition A* bounds the discounted expected next-period maximum of the regular-weight fulfillment and spot margins by the present maximum plus holding cost. Without it, a two-period instance with next-week penalty $100$ makes the printed Lemma 2(1) policy worth $-80$ while holding is worth $8$ . The corrected Case 1(b) holding quantity is the unsold underweight stock capped by its spot break-even level. Case 2 uses a regular-weight holding threshold net of already held underweight hogs. The printed Case 2(c) can yield $87$ when a feasible action yields $103$ , so it is excluded. These departures are recorded item by item in the moderation notes.

The definition layer contains the reward, feasible actions, Bellman recursion, continuation value, and break-even levels. A complete proof also needs measurability and integrability of the recursively defined value, compact feasible sets, concavity under integration and partial maximization, and real infimum properties. Contributions to those reusable results, the four milestones, and the corrected goal are within scope. A formulation with free thresholds or a free value function would make the policy claim empty; both are computed from the model data here.

Selected references

P. Kouvelis, Y. Liu, Y. Qiu and D. Turcic, Managing Operations of a Hog Farm Facing Volatile Markets: Inventory and Selling Strategies, SSRN preprint 3912801, March 6, 2023; subsequently Manufacturing & Service Operations Management, DOI 10.1287/msom.2023.1216. Preprint.

6 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

A Casino Gambling Model Under Cumulative Prospect Theory: Analysis and Algorithm: A Centred Law on [−T, T] Is the Law of S_τ for Some Stopping Time τ ≤ T iff Its Potential Satisfies (8)Research Paper

Motivation

Barberis' casino gambling model (Barberis 2012) asks when a gambler with cumulative prospect theory (CPT) preferences should leave a casino. At each of the times $t=0,1,\dots,T-1$ the gambler either stops or bets $1 on a fair coin. The value of a stopping strategy $\tau$ depends on it only through the law of the gain at exit, $S_\tau$ . Probability weighting makes the problem time-inconsistent, so dynamic programming does not apply. Barberis solved small horizons by enumerating Markovian strategies, which does not scale: the paper reports 27 hours of computation for $T=7$ .

Hu, Obłój and Zhou (arXiv:2102.03157v1, published in Management Science 2023) take the law of $S_\tau$ as the decision variable. This works only with a description of the set of laws that stopping before time $T$ can produce, and of a stopping rule that produces a given law. Their Theorem 3.1 gives both. It is a finite-horizon Skorokhod embedding theorem for the simple symmetric random walk.

Timeline:

1969: Root constructs barrier stopping times embedding any centred law with finite variance in Brownian motion, on an infinite horizon.
2004: Obłój's survey collects the potential-theoretic approach to Skorokhod embeddings.
2017 and 2019: He, Hu, Obłój and Zhou treat the infinite-horizon casino model with path-dependent and randomized strategies. They give explicit embeddings for the random walk without a time bound (Operations Research 65(1); Stochastic Processes and their Applications 129(9)).
2021: the present paper adds the horizon $T$ , through condition (8) and randomized Root times.

Setting

A casino space is a filtered probability space $(\Omega,\mathcal F,P;(\mathcal F_t)_{t\in\mathbb N})$ carrying a standard symmetric random walk $S$ and a variable $\xi$ . Here $S_0=0$ , each $S_t$ is $\mathcal F_t$ -measurable, and each increment $S_{t+1}-S_t$ is $\pm1$ , fair, and independent of $\mathcal F_t$ . The variable $\xi$ is $\mathcal F_0$ -measurable and uniform on $[0,1]$ . The variable $\xi$ lets a gambler randomize: from it one can build countably many independent biased coins. The admissible strategies $\mathcal T_T$ are all $(\mathcal F_t)$ -stopping times $\tau\le T$ ; they may depend on the whole path and on the coins.

$\mathcal P_0(\mathbb Z)$ is the set of probability laws $\mu$ on the integers with a finite first moment and mean zero. The potential of $\mu$ is

U_\mu(x)=\int|x-y|\,\mu(dy),\qquad x\in\mathbb R.

For a stopping time $\sigma$ , $U_{S_\sigma}$ is the potential of the law of $S_\sigma$ . The evolutional functions are defined on the integers by

U^\mu_0(x)=|x|,\qquad U^\mu_t(x)=\frac{U^\mu_{t-1}(x-1)+U^\mu_{t-1}(x+1)}{2}\wedge U_\mu(x).\tag{6}

A randomized Root stopping time has three ingredients:

a barrier $b(x)=x+2k\ge|x|$ , for some $k\in\mathbb Z$ ;
boundary probabilities $r(x)\in[0,1]$ ;
independent coins $\xi_{t,x}$ with $P(\xi_{t,x}=0)$ equal to $0$ , $r(x)$ or $1$ according as $t<b(x)$ , $t=b(x)$ or $t>b(x)$ .

It is

\tau_R(b,r)=\inf\{t\in\mathbb N:\ t\ge b(S_t),\ \xi_{t,S_t}=0\}.\tag{7}

Formalization targets

Goal: Theorem 3.1 (p. 16)

Let $T\ge1$ and let $\mu\in\mathcal P_0(\mathbb Z)$ satisfy $\mu([-T,T])=1$ . Then some $\tau\in\mathcal T_T$ has $S_\tau\sim\mu$ if and only if

U_\mu(x)\le\frac{U^\mu_{T-1}(x+1)+U^\mu_{T-1}(x-1)}{2},\qquad x=-(T-2),-(T-4),\dots,T-4,T-2.\tag{8}

In that case, some randomized Root stopping time $\tau_R(b,r)\in\mathcal T_T$ has $S_{\tau_R(b,r)}\sim\mu$ .

Milestones

Identities (5), p. 13: $\mu(\{x\})$ and $U_\mu(x)$ in terms of the potential.
The potential determines the law, p. 13.
Proposition A.1 (i), p. 44: convexity and bounds for the potentials of $S_{\tau\wedge t}$ .
Proposition A.1 (iii), p. 44: the one-step identity (17).
Proposition A.2 (i), p. 45: $U_0\le U^\mu_t\le U_\mu\wedge U_{S_t}$ .
Proposition A.2 (ii), p. 45: the parity structure of $U^\mu_t$ .
Proposition A.2 (iii), p. 45: convexity in $x$ and monotonicity in $t$ .
Proposition A.3, p. 46: three conditions are equivalent, $U^\mu_T=U_\mu$ , embedding by a Root time, and embedding by some $\tau\in\mathcal T_T$ ; and $U_{S_{\tau\wedge t}}\le U^\mu_t$ .
The proof of Theorem 3.1, pp. 48–49: (8) holds if and only if $U^\mu_T=U_\mu$ on $\mathbb Z$ .

Significance

The theorem makes the time-inconsistent stopping problem an optimisation over finitely many probabilities $\mu(\{-T\}),\dots,\mu(\{T\})$ . The constraints are explicit: (8) together with $\mu\in\mathcal P_0(\mathbb Z)$ . The paper builds its mathematical program (§4) and its algorithm on this reduction, replacing exhaustive search over strategies. The "moreover" clause shows that randomized Markovian barrier rules are as good as any path-dependent or randomized strategy for every law-invariant objective. This is a structural statement about optimal behaviour, not specific to CPT.

Formalizing the statement produces a machine-checked discrete Skorokhod embedding with a time bound. As far as a search of the platform shows, it would be the first formal treatment of Root-type stopping times. It also produces a potential-function toolkit for integer laws: identities (5), uniqueness, and the recursion (17) for stopped walks. That toolkit is reusable for other random-walk embedding and martingale optimal transport results. The result is proved in the paper; none of it is formalized.

Difficulty

The "only if" direction must hold for every stopping time on every casino space, including path-dependent, randomized and non-Markovian ones. A natural first idea is to prove it for Markovian or Root rules and argue that these are without loss of generality. That is exactly the content of the theorem, so it cannot be assumed. The bound $U_{S_{\tau\wedge t}}\le U^\mu_t$ must hold for an arbitrary $\tau$ that embeds $\mu$ , and the parity structure of the walk enters it in an essential way.

The "if" direction must construct the coins on the given space from the single uniform variable $\xi$ . The constructed stopping time must be bounded by $T$ , not merely almost surely finite. And condition (8) constrains only the odd or even sites, depending on $T$ ; showing that this partial condition forces $U^\mu_T=U_\mu$ at every integer needs convexity of $U_\mu$ and the parity identities of the evolutional functions.

Formalization scope

All objects live in the namespace CasinoCPT.Embedding and in one definitions module.

The casino space is a predicate IsCasinoSpace P F S ξ on an arbitrary measurable space. Every statement quantifies over all such spaces; no conclusion chooses the space.
Stopping times are Mathlib's ℕ∞-valued IsStoppingTime, and $\tau\in\mathcal T_T$ means a stopping time with $\tau(\omega)\le T$ for every $\omega$ .
The law of $S_\sigma$ is the push-forward of $P$ under stoppedValue S σ, a measure on $\mathbb Z$ .
$\mathcal P_0(\mathbb Z)$ requires a probability measure, an integrable identity and mean zero. The potential is a Bochner integral, so every statement carries this hypothesis or uniform integrability.
The evolutional functions are defined on $\mathbb Z$ only. Statements the paper makes for their linear interpolation on $\mathbb R$ are stated at the integers, which is equivalent: convexity becomes the discrete midpoint inequality, and comparisons with $U_{S_{\tau\wedge t}}$ are made at integers.
Condition (8) ranges over the integers $x$ with $|x|\le T-2$ and $x+T$ even, and every statement assumes $T\ge1$ .
Coins are Boolean with false meaning "stop". They are $\mathcal F_0$ -measurable and mutually independent, with the three laws of (7).

The Root clause of the goal asserts that a barrier, boundary probabilities and a coin family exist whose Root time lies in $\mathcal T_T$ and embeds $\mu$ .

A trivializing formalization is ruled out: $\mathcal T_T$ is not restricted to Root times, Markovian rules or a linear program on the binomial tree. The definition of $\tau_R$ is literally (7), with the infimum of the empty set equal to $\infty$ .

A complete development needs:

potentials of integer laws;
the martingale property of stopped random walks;
the construction of independent coins from a uniform variable;
the measurability of Root times.

Proofs of individual milestones are welcome independently. Propositions A.2 (i)–(iii) and the equivalence (8) ⇔ $U^\mu_T=U_\mu$ need no probability space.

Selected references

S. Hu, J. Obłój, X. Y. Zhou, When to Quit Gambling, if You Must!, arXiv preprint, 2021; published as A casino gambling model under cumulative prospect theory: analysis and algorithm, Management Science, 2023. https://arxiv.org/abs/2102.03157v1
N. Barberis, A model of casino gambling, Management Science 58(1):35–51, 2012. https://doi.org/10.1287/mnsc.1110.1435
D. H. Root, The existence of certain stopping times on Brownian motion, Annals of Mathematical Statistics 40(2):715–718, 1969. https://doi.org/10.1214/aoms/1177697749
J. Obłój, The Skorokhod embedding problem and its offspring, Probability Surveys 1:321–392, 2004. https://arxiv.org/abs/math/0401114
X. D. He, S. Hu, J. Obłój, X. Y. Zhou, Path-dependent and randomized strategies in Barberis' casino gambling model, Operations Research 65(1):97–103, 2017.
X. D. He, S. Hu, J. Obłój, X. Y. Zhou, Two explicit Skorokhod embeddings for simple symmetric random walk, Stochastic Processes and their Applications 129(9):3431–3435, 2019.

14 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Systemic Risk-Driven Portfolio Selection: Closed-Form Portfolio Maximizing Co-Expected Returns When the System Is at Its VaR Level and Portfolio Returns Are below CoVaRResearch Paper

Motivation

A portfolio can look attractive on average and still perform poorly when the financial system is under stress. Capponi and Rubtsov's Systemic Risk Driven Portfolio Selection asks an investor to choose asset weights using the portfolio return expected in a specified system stress state, rather than using only an unconditional mean or variance. The question is concrete: when the system return is at a low quantile, which portfolio has the highest expected return among outcomes below its own conditional low quantile? This mission formalizes the paper's closed-form answer for the Gaussian case, Proposition 2 of the May 25, 2019 working paper.

The paper distinguishes a system fixed at its value-at-risk level from a system lying anywhere below that level. The former has an explicit optimizer under a technical condition; the latter leads to a different criterion and is outside this mission. The distinction matters because conditioning on one exact system return and conditioning on a tail event produce different laws and different portfolio problems. The working paper, pp. 5–14, develops both settings.

Setting

There are $n\ge2$ risky assets and no risk-free asset. Their random return vector has mean $\mu$ and covariance matrix $\Sigma$ . A portfolio is a real weight vector $w$ satisfying $\mathbf1^\top w=1$ ; the paper imposes no nonnegative-weight or no-short-sale constraint. Its return $R_p$ has mean $\mu_p=w^\top\mu$ and standard deviation $\sigma_p=\sqrt{w^\top\Sigma w}$ . The system return $R_m$ has mean $\mu_m$ and standard deviation $\sigma_m$ , and $\sigma$ denotes the vector of covariances between each asset and the system. Thus the portfolio-system correlation is $\rho(w)=w^\top\sigma/(\sigma_m\sigma_p)$ .

For a law $\nu$ on the real line, value at risk at level $q$ is its lower $q$ -quantile, $\operatorname{VaR}_q(\nu)=\inf\{v:q\le\nu(({-}\infty,v])\}$ . Let $q_m$ and $q_p$ be quantile levels strictly between zero and one half, as in the paper's stress convention. The conditional value at risk $\operatorname{CoVaR}_{q_p}(w)$ is the $q_p$ -quantile of the conditional law of $R_p$ when $R_m=\operatorname{VaR}_{q_m}(R_m)$ . The performance criterion is the co-expected return

\operatorname{CoER}^{=}(w) =\mathbb E\!\left[R_p\mid R_p\le\operatorname{CoVaR}_{q_p}(w),\ R_m=\operatorname{VaR}_{q_m}(R_m)\right].

Under Assumption 2, $(R_p,R_m)$ is bivariate Gaussian, with the means, standard deviations and correlation above. The proof of Proposition 2 uses the joint covariance of all asset returns and the system, $[\Sigma\ \sigma;\sigma^\top\ \sigma_m^2]$ . The working paper, pp. 5–7 and 28, gives these definitions and parameters.

Formalization targets

The first targets identify the Gaussian quantile and lower-tail mean, then the conditional Gaussian law. They yield the paper's CoVaR display and the closed form for $\operatorname{CoER}^{=}(w)$ in Proposition 1:

\operatorname{CoER}^{=}(w) =w^\top\mu+\frac{\Phi^{-1}(q_m)}{\sigma_m}w^\top\sigma -\frac{\phi(\Phi^{-1}(q_p))}{q_p} \sqrt{w^\top\Sigma w-\frac{(w^\top\sigma)^2}{\sigma_m^2}}.

Here $\Phi$ and $\phi$ are the standard normal cumulative distribution and density. Define $\widehat\mu=\mu+\Phi^{-1}(q_m)\sigma/\sigma_m$ , $\widehat\Sigma=\Sigma-\sigma\sigma^\top/\sigma_m^2$ , and $\lambda=\phi(\Phi^{-1}(q_p))/q_p$ . The paper's Appendix partitions $\widehat\mu$ and $\widehat\Sigma$ after asset $n-1$ to obtain $\Delta$ and $Q$ . Proposition 2 gives a particular inverse-matrix expression $w^*$ and states that, provided $\lambda>\sqrt{\Delta^\top Q^{-1}\Delta}$ , it maximizes $\operatorname{CoER}^{=}$ over all weights summing to one. The goal includes feasibility and uniqueness:

\mathbf1^\top w^*=1,\qquad \operatorname{CoER}^{=}(w)\le\operatorname{CoER}^{=}(w^*) \quad\text{for every }w\text{ with }\mathbf1^\top w=1,

with equality only for $w=w^*$ . The exact $w^*$ is part of the Lean definitions and reproduces the formula printed in Proposition 2, including its last-asset partition and transpose on $Q^{-1}$ . The draft theorem chain covers the paper's displayed results (A.1)–(A.4), Proposition 1 (2.4), and the optimization step (A.7)–(A.8); the mission's milestones mark the conditional law, CoVaR, CoER=, the vector formula, and the optimizer. The working paper, pp. 7, 9 and 27–29, states them.

Significance

The result gives an explicit portfolio choice for a stress-sensitive objective, subject only to the full-investment constraint. Its condition identifies the regime in which the finite optimizer exists; when the condition fails, the paper notes that portfolios with arbitrarily high objective values can be constructed. The conditional-return formula also separates ordinary expected return, exposure to the system, and variance left after accounting for that exposure. This permits a precise comparison with a mean-variance portfolio using the same covariance data. The working paper, pp. 7–10, gives the comparison and its numerical illustration.

The paper proves these claims analytically. Here the Lean declarations compile as statements with open proofs; this mission does not claim a machine-checked proof of Proposition 2. A completed formalization would connect the conditional-density meaning of CoER= to the Gaussian formulas and then verify the optimizer for the full class of feasible weights. The quantile, conditional Gaussian, and quadratic objective interfaces are reusable in other risk and stochastic optimization results.

Difficulty

The event $R_m=\operatorname{VaR}_{q_m}(R_m)$ has probability zero for a nondegenerate Gaussian. An ordinary ratio of event probabilities therefore does not define the conditional law at that exact point. The paper relies on the bivariate density to specify it. Even after its Gaussian form is known, the objective contains a square root of a covariance quadratic form, and the feasible set is an unbounded affine hyperplane because weights may be negative. A first-order stationary calculation alone does not establish a global, unique maximizer or exclude unbounded cases. The condition in Proposition 2 addresses that boundary.

Formalization scope

Vectors use Fin (m + 1) → ℝ with $m\ge1$ ; the final asset is Fin.last m. Matrices are finite real Mathlib matrices. The formal model builds $\mu_p$ , $\sigma_p$ and $\rho(w)$ from asset and system parameters, and builds CoER= from the conditional law for every weight vector. It does not replace CoVaR or CoER= by their later closed forms. This prevents the Gaussian and portfolio milestones from becoming restatements of definitions.

The conditional law at an exact system value is the density ratio of the bivariate Gaussian, fixing the continuous version needed at a null event. VaR is a left quantile; $\Phi^{-1}$ is the same construction for the standard normal law. Gaussian variances use nonnegative reals, while portfolio quantities and matrix algebra use reals. Expectations are set integrals under the conditional law, divided by the actual conditional probability of the lower-tail event.

The standing assumptions include positive definiteness of the joint asset-system covariance $[\Sigma\ \sigma;\sigma^\top\ \sigma_m^2]$ and $\sigma_m>0$ . Positive definiteness makes all conditional Gaussian variances positive and supplies the nonsingular matrices required by the printed inverse formula. In particular, the mission excludes degenerate covariance matrices for which Lean's total inverse or square root could silently return a default value. The formalization needs finite-matrix positive-definiteness and Schur-complement facts, Gaussian density and quantile facts, set-integral facts, and a constrained optimization theorem for the square-root quadratic objective. Contributions proving any of those faithful milestones or reusable supporting lemmas are within scope.

Selected references

Agostino Capponi and Alexey Rubtsov, Systemic Risk Driven Portfolio Selection, SSRN working paper 3394471, version of May 25, 2019. SSRN.

10 thms2 active usersReviewed

All missions

Suboptimal Local Minima Exist for Wide Neural Networks with Smooth Activations: For Generic Inputs and Any Depth and Width, Some Output Data Gives the Squared Loss a Sub-Optimal Local MinimumResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Flexible Drug Approval Policies: The Optimal Significance Level Is Higher for Diseases with Long Clinical Trials, High Attrition and Low R&D IntensityResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 1 (p. 13)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Affine Storage and Insurance Risk Models: Closed Form for the Joint Transform of Ruin Time, Overshoot and Undershoot Before an Exponential Horizon from an Exponential Initial SurplusResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 1288)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Negative Advertising and Competitive Positioning: When Negative Advertising Is Permitted, There Is an Equilibrium in Which the Entrant Co-Locates and Both Firms Prioritize Positive AdvertisingResearch Paper

Negative advertising and where products are placed

The model

Formalization targets

Goal: Proposition 2 on the corrected region

Milestones

Significance

Difficulty

Formalization scope

Selected references

Expectations-Based Loss Aversion in Auctions with Interdependent Values: Extensive vs. Intensive Risk: Under CPE, First-Price Revenue Exceeds Second-Price Revenue iff Bidders Are Loss-Averse in MoneyResearch Paper

Why auction revenue depends on bidders’ expectations

Auction and preference setting

Formalization targets

What the result gives

Main difficulty

Formalization scope

Selected references

Towards a Functional Fee Market for Cryptocurrencies: Truthful Bidding Is Not Dominant, but the Expected Gain from Strategic Bidding Converges to 0 as the Number of Users DivergesResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Over-Conservativeness of Variance-Based Efficiency Criteria and Probabilistic Efficiency in Rare-Event Simulation: Most Significant Dominating Points Suffice for Strong Probabilistic EfficiencyResearch Paper

Motivation

Setting

Formalization targets

Most significant dominating points

Supporting targets

Significance

Difficulty

Formalization scope

Selected references

Market Making and Incentives Design in the Presence of a Dark Pool: Existence and Uniqueness of the Continuous Viscosity Solution of the Exchange's HJB EquationResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (first assertion)

Milestone: Remark 4.2

Significance

Difficulty

Formalization scope

Selected references

Optimally Scheduling Heterogeneous Impatient Customers: The Fluid-Optimal Schedule Splits at Most One Customer Class into Two SubclassesResearch Paper

Motivation

Setting