Probability

Motivation

In a principal–agent problem with moral hazard, a principal (an employer) pays an agent whose effort she cannot observe; she sees only an output process whose drift the effort controls. Continuous-time versions of the problem, starting with Holmström–Milgrom (1987) and Sannikov (2008), are solved by turning the agent's continuation utility into a state variable and writing a Hamilton–Jacobi–Bellman (HJB) equation for the principal's value.

Most of this literature assumes two-sided commitment: the agent cannot leave. In labour markets the agent can quit whenever an outside offer beats his continuation utility, and the principal must then hire someone else. Zhang and Zhu (arXiv:2208.06473; Mathematics of Operations Research, 2025) study this one-sided commitment: the principal is committed to the contract, the agent is free to quit at a stopping time of his choice, and after each quitting the principal pays a cost and hires a new agent, possibly of another type. The principal's value then depends on every future hire, and the paper characterises it by a coupled system of HJB equations.

Setting

Fix a horizon $T>0$ and a payment cap $C_0>0$. A standard Brownian motion $B$ on $(\Omega,\mathcal F,\mathbb P)$ is the output. Agents have types $\theta\in\Theta$. An agent of type $\theta$ receiving a payment rate $\eta\le C_0$ and exerting effort $\alpha$ has running utility $f(\theta;s,\eta)$ and running cost $h(\theta;s,\alpha)$; $f$ is increasing and concave in $\eta$, $h$ is convex in $\alpha$ (Assumption 2.2). Effort shifts the drift of $B$ through the Girsanov measure $\mathbb P^\alpha$ (weak formulation). The agent's optimal effort against a sensitivity process $Z$ is $\alpha=I^h(\theta;\cdot,Z)$, the inverse of $\partial_\alpha h$, and $\mathbb E^{\theta,Z}$ denotes expectation under the corresponding measure.

A contract started at time $t$ is described in forward form by $(\eta,Z)$: the agent's continuation utility is

$$\mathcal X^{\theta;t,x,\eta,Z}_s=x-\int_t^s\big[f(\theta;r,\eta_r)+H(\theta;r,Z_r)\big]dr+\int_t^sZ_r\,dB_r,$$

with $H(\theta;s,z)=\sup_\alpha[\alpha z-h(\theta;s,\alpha)]$ and the constraint $\mathcal X_T=0$. The agent's utility is capped by the upper barrier $\overline L^\theta_t=\int_t^Tf(\theta;s,C_0)\,ds$. He quits at the first time $\mathcal X$ reaches the lower barrier $\underline L^\theta_t=R^\theta_t-c^\theta_t$, where $R^\theta$ is his market value and $c^\theta\ge1/\Lambda_0$ his quitting cost (Assumptions 2.7, 3.1). The relevant domain is

$$D_\theta=\{(t,x):0\le t<T,\ \underline L^\theta_t<x\le\overline L^\theta_t\}.$$

When the $i$-th agent quits at $\tau_i<T$, the principal pays $c^P_{\tau_i}$ and hires an agent of type $\zeta_{\tau_i}$ at utility $R^{\zeta_{\tau_i}}_{\tau_i}$ (the quitting sequence (5.8)). The principal's value is

$$u_\infty(\theta;t,x)=\sup_{(\eta,Z,\zeta)}\mathbb E^{\zeta,Z}\Big[\int_t^T\big[I^h(\zeta_s;s,Z_s)-\eta_s\big]ds-\sum_{i\ge1}c^P_{\tau_i}\mathbf 1_{\{\tau_i<T\}}\Big],$$

and the value of the best new hire at time $t$ is $\overline u_\infty(t)=\sup_\theta u_\infty(\theta;t,R^\theta_t)-c^P_t$.

Formalization targets

Goal: Theorem 6.3

The family $\{u_\infty(\theta;\cdot,\cdot)\}_{\theta\in\Theta}$ is the minimal continuous viscosity solution of

$$\partial_tu+\sup_{\eta\le C_0,\ z\in\mathbb R}\Big[\tfrac12|z|^2\partial_{xx}u-\big[f(\theta;t,\eta)+\tilde H(\theta;t,z)\big]\partial_xu+I^h(\theta;t,z)-\eta\Big]=0\quad\text{on }D_\theta,\ \theta\in\Theta,$$

with boundary conditions

$$u(\theta;t,\overline L^\theta_t)=-C_0(T-t),\qquad u(\theta;T-,x)=0,\qquad u(\theta;t,\underline L^\theta_t+)\ge\sup_{\theta'}u(\theta';t,R^{\theta'}_t)-c^P_t.$$

The last condition couples the equations for different types. The goal also asserts that the value sets in (6.1) are nonempty and bounded above, so that $u_\infty$ is a genuine real-valued function.

Milestones

1. Lemma 3.4: explicit contracts with $\int_t^T[C_0-\eta_s]ds\le\delta$ under which the agent never quits.
2. Lemma 2.5 (2.20): a priori estimates for admissible contracts.
3. Proposition 2.8 and Lemma 3.6: the self-enforcing value $V^P_0$ and the new-hire value $\overline u_0$ are uniformly continuous with modulus $C\sqrt\rho$.
4. Theorem 4.5: with at most one quitting, $u_1$ is the minimal continuous viscosity solution of the same equation with boundary datum $\overline u_0$.
5. Proposition 5.4: a non-recursive representation of $u_n$ (at most $n$ quittings).
6. Proposition 6.1: $\mathbb P^{\zeta,Z}(\tau_n<T)\le C/n$, and $|u_n-u_\infty|\le C/n$.
7. Proposition 6.2: monotonicity and uniform continuity of $u_\infty$, regularity of $\overline u_\infty$, and the boundary conditions.
8. (6.7): the dynamic programming principle for $u_\infty$.

Significance

The theorem identifies the principal's value under one-sided commitment as a PDE object, which makes it computable and comparable with other contracting regimes. Along the way the paper shows that the principal sees only finitely many quittings (Proposition 6.1) and that tolerating more quittings never lowers her value, so contracts that prevent quitting altogether (self-enforcing contracts) are in general suboptimal. The coupling through $\overline u_\infty$ turns the problem into an infinite system of HJB equations indexed by agent types, a structure that also appears in switching and re-hiring problems.

The result is proved in the paper; none of it is formalized. A formalization would add to the platform a continuous-time moral-hazard model in the weak formulation, hitting-time stopping driven by an Itô integral, a quitting sequence with random restarts and type switching, and a viscosity-solution notion for a fully nonlinear HJB equation on a time-dependent domain. The paper's own proof leaves several steps to the reader (the dynamic programming principle, the viscosity property, comparison for a truncated equation), so a complete development would also supply these.

Difficulty

The obvious route is "dynamic programming principle, then viscosity property, then comparison". Each step is harder here than in a textbook control problem. The control $z$ is unbounded, so the Hamiltonian can be $+\infty$ and the viscosity property must be derived without a finite Hamiltonian. The process is stopped at a hitting time of a moving barrier and restarted at a random level with a new type, so the dynamic programming principle must handle restarts. Minimality cannot come from a standard comparison principle, because the boundary datum at $\underline L^\theta$ depends on the competitor itself and no growth condition is imposed on competitors; the paper argues through approximation by $u_n$ and Theorem 4.5 instead.

Formalization scope

All objects are defined in the namespace DynPrincipalAgent.HJB. Process time is $\mathbb R_{\ge0}$; deterministic data are functions of real time. The Itô integral is the published Peng1990.SMP.IsItoIntegral, with a continuous version required wherever hitting times read paths. Controls started at $t$ are progressively measurable for the filtration $\mathbb F^t$ of $B_s-B_t$. Value functions are real suprema of value sets that record an expectation only when it is genuine (integrable payoffs, almost surely integrable drifts and running rewards, summable quitting costs); these conditions hold for every admissible control.

Pinned readings, all disclosed in the items: viscosity solutions are the standard Crandall–Ishii–Lions notion with $C^2$ test functions on $\mathbb R^2$, tested on the interior of $D_\theta$, with the supremum in the HJB operator never formed; the boundary condition at $\underline L^\theta$ requires a real right limit compared against every $u(\theta';t,R^{\theta'}_t)-c^P_t$; $\Theta$ carries a σ-algebra and $f$, $h$, $\partial_\alpha h$ are jointly measurable; Assumption 2.7 (ii) is read as $|R^\theta_s-R^\theta_{s'}|\le\rho(|s-s'|)$; a modulus of continuity is nondecreasing, vanishes at $0^+$ and satisfies $\rho(\delta)\ge\delta$; generic constants depend only on $(T,C_0,\Lambda_0,\Lambda_1)$ and are fixed before the model; $H$ and $\tilde H$ take the closed forms of (2.11)–(2.12). The agent's BSDE and reflected BSDE (Propositions 2.3, 3.2), §7's standard contracts and the economic interpretation of $R^\theta$, $c^\theta$, $c^P$ are out of scope.

A formalization in which a value function equals a junk value (an empty or unbounded real supremum, a Bochner integral of a non-integrable payoff, a hitting time of an empty set) or in which the viscosity notion is vacuous does not count: the goal states that the value sets are nonempty and bounded, and the definitions avoid junk by construction. Competitors in the minimality clause satisfy exactly the printed boundary conditions, with no added growth bound.

Reusable infrastructure: Girsanov measures for BMO drifts, forward utility processes, hitting times of continuous semimartingales, and viscosity solutions of HJB equations on non-cylindrical domains. Contributions on any milestone, and on general lemmas such as the dynamic programming principle for controlled diffusions stopped at hitting times, are welcome.

Selected references

• J. Zhang, Z. Zhu, A Dynamic Principal Agent Problem with One-sided Commitment, Mathematics of Operations Research, 2025. Preprint arXiv:2208.06473v3. https://arxiv.org/abs/2208.06473
• Y. Sannikov, A Continuous-Time Version of the Principal–Agent Problem, Review of Economic Studies 75 (2008). https://doi.org/10.1111/j.1467-937X.2008.00486.x
• B. Holmström, P. Milgrom, Aggregation and Linearity in the Provision of Intertemporal Incentives, Econometrica 55 (1987). https://doi.org/10.2307/1913238
• M. G. Crandall, H. Ishii, P.-L. Lions, User's guide to viscosity solutions of second order partial differential equations, Bull. AMS 27 (1992). https://doi.org/10.1090/S0273-0979-1992-00266-5

Motivation

Mean-variance (MV) preferences, $U_\theta(X)=\mathbb E[X]-\frac\theta2\mathrm{Var}(X)$, are the standard objective of portfolio selection since Markowitz. They are not monotone: an investor can prefer a terminal wealth $X$ to a wealth $X'\ge X$ that is larger in every state, because the extra upside raises the variance. Monotone mean-variance (MMV) preferences (Maccheroni, Marinacci, Rustichini and Taboga, 2009) repair this. They are the largest monotone preferences that agree with MV preferences on the domain of monotonicity $\mathcal G_\theta=\{f\in\mathcal L^2:f-\mathbb E[f]\le1/\theta\}$.

A natural question is when switching from MV to MMV changes the optimal investment. In continuous-time markets driven only by Brownian motions, the optimal strategies under the two preferences coincide (Trybuła and Zawisza, 2019, for a stochastic factor model; Strub and Li, 2020, for continuous semimartingale markets), and whether this persists with jumps was left open by Trybuła and Zawisza. Li, Liang and Pang study a market whose risky asset also jumps and whose coefficients depend on a stochastic factor. They show that the two problems agree if and only if a pathwise condition on the jumps, Assumption 1, holds.

Setting

On a probability space $(\Omega,\mathcal F,\mathbb P)$ live two independent Brownian motions $W^1,W^2$ and an independent Poisson random measure $N(\mathrm ds,\mathrm dp)$ with finite Lévy measure $\nu$ and compensated measure $\tilde N$. The filtration $\{\mathcal F_t\}$ is generated by $W^1,W^2,N$. A stochastic factor follows

$$\mathrm dZ_s=a(Z_s)\,\mathrm ds+b(Z_s)(\rho_W\,\mathrm dW^1_s+\bar\rho_W\,\mathrm dW^2_s),\qquad Z_t=z,$$

with $\rho_W^2+\bar\rho_W^2=1$. Investing the amount $\pi_s$ in the risky asset gives the (discounted) wealth

$$\mathrm dX^\pi_s=\pi_s(\mu(Z_s)-r)\,\mathrm ds+\pi_s\sigma(Z_s)\,\mathrm dW^1_s+\pi_s\int_{\mathbb R}\gamma(Z_s,p)\,\tilde N(\mathrm ds,\mathrm dp),\qquad X_t=x,$$

on $[t,T]$, with $\gamma>-1$. Write $\Sigma(z)=\sigma(z)^2+\int\gamma(z,p)^2\nu(\mathrm dp)$ and $\lambda(z)=(\mu(z)-r)^2/\Sigma(z)$.

The MMV preference is

$$V_\theta(X)=\inf_{\mathbb Q}\Big\{\mathbb E^{\mathbb Q}[X]+\frac1{2\theta}\Big(\mathbb E^{\mathbb P}\Big[\Big(\frac{\mathrm d\mathbb Q}{\mathrm d\mathbb P}\Big)^2\Big]-1\Big)\Big\}.$$

The infimum runs either over the Doléans-Dade measures $\mathcal Q^t$ or over all of $\mathcal Q_0=\{\mathbb Q\ll\mathbb P:\mathbb E[(\mathrm d\mathbb Q/\mathrm d\mathbb P)^2]<\infty\}$. A measure in $\mathcal Q^t$ has density $\mathcal E_T$, where $\mathcal E$ is the stochastic exponential of $\int\eta_1\mathrm dW^1+\int\eta_2\mathrm dW^2+\int\!\int\phi\,\mathrm d\tilde N$ with $\mathcal E_T\ge0$, $\mathbb E[\mathcal E_T]=1$ and $\mathcal E_T\in L^2$.

The optimal utilities from $(x,z,t)$ are suprema over the admissible strategies of the paper's Definitions 2 and 3: predictable $\pi$ whose wealth has $\mathbb E[\sup_s|X^\pi_s|^2]<\infty$, under $\mathbb P$ for MV and under every $\mathbb Q\in\mathcal Q^t$ for MMV. Both solutions are expressed through the solution $G=-e^F$ of the nonlinear parabolic PDE (20),

$$G_t+\alpha(z)G_z+\tfrac12b(z)^2G_{zz}-\beta(z)b(z)^2\frac{G_z^2}{G}+\lambda(z)G=0,\qquad G(z,T)=-1.$$

Through $\zeta(z,s)=-(\mu(z)-r-\sigma(z)b(z)\rho_WG_z/G)/\Sigma(z)$ it also enters Assumption 1. Let $\tau$ be the first jump time after $t$ at which $\zeta(Z_s,s)\gamma(Z_s,\Delta L_s)=-1$. Assumption 1 requires $\zeta\gamma\ge-1$ at every jump in $(t,T]$ up to time $\tau$.

Formalization targets

Goal: Theorem 9

$$\sup_{\pi\in\mathcal B_{x,z,t}}U_\theta(X^\pi_T)=\sup_{\pi\in\mathcal A_{x,1/(2\theta),z,t}}V_\theta(X^\pi_T)\iff\text{Assumption 1 holds at }(z,t).$$

The same holds when $V_\theta$ ranges over $\mathcal Q_0$ instead of $\mathcal Q^t$.

Milestones

1. Theorem 3 links the market player's density process to the wealth: $2Y_sG(Z_s,s)=X^{\pi^*}_s-x+2yG(z,t)$.
2. Theorem 4 solves the MMV problem: the value is $V(x,y,z,t)=-x+G(z,t)y$, with an explicit saddle point.
3. Theorem 6 solves the auxiliary quadratic problem: $U_D(x,z,t)=-(x-D)^2/G(z,t)$.
4. Theorem 7 gives the Lagrange multiplier and the optimal target.
5. (39) gives the optimal MV strategy.
6. The moment identities $\mathbb E[R_T]=\mathbb E[R_T^2]=H(z,t)=-1/G(z,t)$.
7. Theorem 8: under Assumption 1 the optimal strategies coincide.
8. Lemma 4: the optimal MV wealth lies in $\mathcal G_\theta$ if and only if Assumption 1 holds.
9. (44)–(45): the mean and variance of the optimal wealth.

Significance

The result separates the two preferences by an observable property of the market. The Brownian theory gives agreement for free. With jumps the MV-optimal wealth can leave $\mathcal G_\theta$, and that happens exactly when a jump of size $\zeta\gamma<-1$ can occur before the first jump with $\zeta\gamma=-1$. In that case MMV and MV investors hold different portfolios. The paper's §5.4 examines in market data whether Assumption 1 is reasonable. The explicit closed forms (the value $-x+G(z,t)y$, the variance $-(G(z,t)+1)/\theta^2$ of the optimal wealth, the efficient frontier) are what applied work uses.

The result is proved on paper, in an arXiv preprint later published in Mathematics of Operations Research (2025). None of it is machine-checked. A formal proof would check the verification arguments for a stochastic differential game with jumps, a Feynman–Kac representation with a jump density, and the comparison with Maccheroni et al.'s monotone hull. The paper's own proofs are brief at several of these steps. The underlying infrastructure (Itô calculus with Poisson jumps, Doléans-Dade exponentials, verification theorems) would be reusable for most of continuous-time portfolio theory.

Difficulty

The obvious argument would show $U_\theta=V_\theta$ along the optimal wealth and conclude. Lemma 4 shows this argument breaks: the optimal MV wealth need not lie in $\mathcal G_\theta$. Remark 7 also notes that membership in $\mathcal G_\theta$ alone does not identify the optimal values; both optimal strategies must be found and compared.

Finding them needs a verification theorem for a two-player stochastic differential game with jumps (Theorems 1 and 4). That in turn needs Itô's formula for jump diffusions and martingale properties of Doléans-Dade exponentials that may vanish (Lemma 2, Mémin's criterion). Identifying the two strategies needs the moment identities $\mathbb E[R_T]=\mathbb E[R_T^2]=H$, which come from a Feynman–Kac argument with a jump-driven density (Lemma 3). The converse direction needs a stopping argument at the first "bad" jump. None of this exists in Mathlib, which has Brownian motion but no stochastic integral and no Poisson process.

Formalization scope

• Time is $[0,\infty)$; every process lives on $[t,T]$ with $t<T$, and $\int_t^s$ is a difference of integral processes whose integrands vanish before $t$.
• Brownian integrals are the $L^2$ Itô integrals of Peng1990.SMP.Stochastic. The admissible classes $\mathcal A$, $\mathcal B$, $\mathcal M^t$ therefore contain only strategies whose Brownian integrands are in $L^2$; all strategies used in the paper qualify.
• The Poisson random measure is JacodTodorov10.LLN.IsFPoisson with $\nu$ finite and $\nu(\{0\})=0$. The compensated integral is the pathwise sum over atoms minus the compensator integral.
• The filtration is the natural (uncompleted) filtration of $(W^1,W^2,N)$.
• Processes are adapted with càdlàg paths; $X_{s-}$ is Mathlib's Function.leftLim. Feedback strategies come with an existence claim, never as bare assumptions.
• All optimal values are infima/suprema in EReal over the full admissible classes. Measures in $\mathcal Q_0$ are probability measures.
• $\mathcal M^t$ is defined by the defining equation (5) of the stochastic exponential. The printed formula (4) has $\Delta X$ where $\Delta M$ is meant and is not used.
• Proposition 1 is not formalized: its hypotheses do not deliver a classical solution. $G$ is a hypothesis: $G=-e^F$ with $F$ bounded, $C^{2,1}$ with bounded derivatives, solving (20). The Conditions of Proposition 1 are kept as printed. $\Sigma,\lambda,\beta>0$ is a standing hypothesis (implicit on p. 12).
• Assumption 1 uses $\tau$ in $[0,\infty]$ ($\inf\emptyset=\infty$), and "a.s." holds simultaneously for all $s\in(t,T]$.
• Printed slips: (37) evaluates $G_z/G$ at $(Z_s,t)$; it is read at $(Z_s,s)$. Lemma 4's "Equation (1)" means (20)/(21).
• Divisions by $1-\mathbb E[R_T]$ and $\mathrm{Var}[R_T]$ carry the hypotheses $\mathbb E[R_T]\neq1$, $\mathrm{Var}[R_T]>0$.

A formalization that replaces either optimal utility by a closed form or by the utility of one fixed strategy is out of scope: it assumes Theorems 4 and 7 and empties the goal. So is one that removes the jumps, freezes the factor, or replaces Assumption 1 by a sufficient condition such as $\gamma\ge0$; each of these makes the "only if" vacuous or false. Contributions that build general infrastructure (an Itô formula for jump diffusions, Doléans-Dade exponentials, a Feynman–Kac theorem) are especially welcome.

Selected references

• B. Li, Z. Liang, L. Pang, Comparison Between Mean-Variance and Monotone Mean-Variance Preferences Under Jump Diffusion and Stochastic Factor Model, arXiv:2211.14473v2, 2023. https://arxiv.org/abs/2211.14473
• F. Maccheroni, M. Marinacci, A. Rustichini, M. Taboga, Portfolio selection with monotone mean-variance preferences, Mathematical Finance 19(3):487–521, 2009. https://doi.org/10.1111/j.1467-9965.2009.00376.x
• J. Trybuła, D. Zawisza, Continuous-time portfolio choice under monotone mean-variance preferences—stochastic factor case, Mathematics of Operations Research 44(3):966–987, 2019 (cited as [Trybuła and Zawisza 2019] in arXiv:2211.14473v2).
• M. S. Strub, D. Li, A note on monotone mean–variance preferences for continuous processes, Operations Research Letters 48(4):397–400, 2020 (cited as [Strub and Li 2020] in arXiv:2211.14473v2).
• P. Protter, Stochastic Integration and Differential Equations, 2nd ed., Springer, 2005, ISBN 978-3-662-10061-5.

Why scoring rules for multivariate distributions

A probabilistic forecast issues a whole distribution $P_X$ for an uncertain quantity $Y\in\mathbb R^d$ rather than a single number: wind and wave heights at several sites, demand for several products, the joint returns of several assets. Forecasts of this kind are compared and estimated with a scoring rule $S(P_X,y)$, a number assigned to the forecast once the realization $y$ is observed. A scoring rule is proper if a forecaster who knows the true distribution $P_Y$ minimizes the expected score by reporting it, and strictly proper if $P_Y$ is the only minimizer (Gneiting and Raftery 2007). Properness is what makes a score usable for model ranking and for M-estimation: an improper score rewards systematic misreporting.

For univariate distributions the continuous ranked probability score (CRPS) and the quadratic score are standard. In several dimensions the choices are thinner: the quadratic score needs a density and is sensitive to its spikes, and the energy score and the multivariate CRPS (MCRPS) were treated as separate constructions. Meng, Taylor, Ben Taieb and Li (arXiv:2002.09578v6, Operations Research, 2025) give one family, the L² scoring rules, which contains the quadratic score, the CRPS and the MCRPS as special cases and produces new ones, such as a score based on lower partial moments. Their Theorem 1 says these rules are proper. This mission formalizes that theorem.

Setting

Work on $\mathbb R^d$ with Lebesgue measure $\mathcal L^d$ and the componentwise order. A distribution is a probability measure $P$ on $\mathbb R^d$; the paper writes it through a generalized density $f_P$ (a PDF, a PMF or a mixture), and every integral $\int g(s)f_P(s)\,ds$ below is $\int g\,dP$. The forecasts range over a class $\mathcal V^d$ of distributions.

Fix a kernel $w:\mathbb R^d\to\mathbb R$ and a weight $h\ge0$ that is integrable. The smoothed density of $P$ is the convolution

$$(f_P*w)(z)=\int_{\mathbb R^d} w(z-s)\,dP(s).$$

For the Heaviside kernel $u(z)=\mathbb 1\{z\ge0\}$ it is the CDF $F_P(z)=P\{s\le z\}$.

The two L² scoring rules are, for a forecast $P_X$ and a realization $y$,

$$S(P_X,y;w,h)=\int_{\mathbb R^d}\big((f_X*w)(z)-w(z-y)\big)^2h(z)\,dz \qquad (2)$$ $$S'(P_X,y;w,h)=\int_{\mathbb R^d}(f_X*w)^2(z)h(z)\,dz-2\int_{\mathbb R^d}(f_X*w)(z)\,w(z-y)\,h(z)\,dz. \qquad (3)$$

The realization $y$ is treated as a point mass, whose convolution with $w$ is $w(\cdot-y)$. The divergence of a score is $\mathbb E_{P_Y}[S(P_X,\bullet)]-\mathbb E_{P_Y}[S(P_Y,\bullet)]$, and the paper's candidate is the weighted L² distance between smoothed densities,

$$\int_{\mathbb R^d}\big((f_X*w)(z)-(f_Y*w)(z)\big)^2h(z)\,dz. \qquad (1)$$

Assumption 1 (p. 32) collects the integrability under which all these integrals are finite.

Formalization targets

Goal: Theorem 1 (p. 8)

Under Assumption 1, for all $P_X,P_Y\in\mathcal V^d$,

$$\mathbb E_{P_Y}[S(P_X,\bullet)]-\mathbb E_{P_Y}[S(P_Y,\bullet)]=\mathbb E_{P_Y}[S'(P_X,\bullet)]-\mathbb E_{P_Y}[S'(P_Y,\bullet)]=\int\big(f_X*w-f_Y*w\big)^2h\,dz\ \ge 0,$$

so both rules are proper. If in addition $h\ne0$ $\mathcal L^d$-a.e. and $f_Y*w$ determines $P_Y$ within $\mathcal V^d$, both are strictly proper. The goal fixes no kernel and no weight: it holds for every pair $(w,h)$ meeting the assumption.

Milestones

1. The relation between (2) and (3): $S=S'+\int w^2(z-y)h(z)\,dz$, a term that does not depend on the forecast (p. 8).
2. The Fubini step of the proof: $\int\!\int g(z)w(z-s)h(z)\,dz\,dP_Y(s)=\int g\,(f_Y*w)\,h\,dz$ (p. 32).
3. The divergence display: the divergence of (2) equals (1) and is nonnegative (p. 32).
4. The strict step: a vanishing divergence with $h\ne0$ a.e. forces $f_X*w=f_Y*w$ a.e. (p. 32).
5. MCRPS (5) and MCRPS′ (6) are strictly proper for all distributions when $h\ne0$ a.e. (p. 11).
6. Lower partial moments of any order $k$ determine the distribution (Appendix, p. 34).

Significance

Theorem 1 is the paper's justification for its whole family of scores. With $w=u$ it shows that the MCRPS is proper; with $w$ the kernel of lower partial moments it shows that a new LPM score is proper; and in Section 4 of the paper the same smoothed densities $f_Y*w$ define the level sets whose scoring functions are the subject of the companion mission (Mission II of this series). Strict properness reduces to one question about the kernel: whether $f_Y*w$ determines $P_Y$. Milestones 5 and 6 answer it for the CDF and for lower partial moments.

The result is proved in the paper (appendix, pp. 32 and 34). To our knowledge none of it is formalized: Mathlib has no scoring rules, and the platform has no proper scoring rule for distributions, no multivariate CRPS and no lower partial moment. The formalization adds the integrability bookkeeping the paper leaves implicit, a machine-checked uniqueness theorem for the multivariate CDF (Mathlib's ext_of_Iic covers linear orders only, i.e. $d=1$), and the same for lower partial moments.

Difficulty

The algebraic core of Theorem 1 is the expansion of a square, and the obvious argument is the paper's. The cost lies elsewhere. Every expectation is an iterated integral of a function of $(s,z)$, and exchanging the order (Fubini) and splitting an integral of a difference require the integrability that Assumption 1 states only as "then (2) is well-defined and finite". The proof also uses $\int dP_Y=1$ when it integrates the $y$-free terms against $P_Y$.

For the companions the obstacle is measure-theoretic. An a.e. equality of multivariate CDFs must first be upgraded to equality everywhere, by right-continuity in each coordinate, and then measures that agree on lower orthants must be shown equal, a π-system argument in $\mathbb R^d$. For lower partial moments the paper differentiates $k$ times under the integral; a rigorous version has to control the finiteness of the lower-order moments.

Formalization scope

• $\mathbb R^d$ is Fin d → ℝ with its product Lebesgue measure volume and the Pi order, so $y\le z$ is componentwise and lower orthants are Set.Iic z. $d$ is any natural number; at $d=0$ the strict clauses are vacuous, as in the paper.
• Distributions are measures with IsProbabilityMeasure; the class $\mathcal V^d$ is a set of such measures. Its convexity (§2) is never used and is not imposed.
• Standing assumptions. The kernel $w$ is a measurable function. The paper also allows a local Borel measure, so that $w=\delta_0$ gives the quadratic score (4); that case is not covered. $h$ is measurable, nonnegative and integrable, not normalized to a density.
• Assumption 1 made explicit. Its clauses (b) and (c) are formalized as integrability hypotheses, each labelled with its clause: $(f_Y*w)^2h$ and $w(\cdot-y)^2h$ integrable; $(s,z)\mapsto w(z-s)^2h(z)$ integrable for $P_Y\otimes\mathcal L^d$; $(f_X*w)\,w(\cdot-y)\,h$ integrable; and $(s,z)\mapsto(f_X*w)(z)\,w(z-s)\,h(z)$ integrable for $P_Y\otimes\mathcal L^d$. Clause (a) adds that $f_Y*w$ is well defined.
• "$f_X*w=f_Y*w$" is an $\mathcal L^d$-a.e. equality. "$f_Y*w$ uniquely characterizes any $P_Y\in\mathcal V^d$" is a property of the whole class $\mathcal V^d$, not of the pair at hand. "$h$ nonzero $\mathcal L^d$-a.e." is used with the paper's quantifier. The theorem's printed "$f_{\mathbf y}*w$" is read as $f_Y*w$.
• Lower partial moments are defined from the explicit kernel printed in (7), $\prod_j (z_j-s_j)^k\mathbb 1\{z_j\ge s_j\}/k!$, for $k\in\mathbb N$, not as a convolution power of $u$. Milestone 6 states equality of the LPMs implying $P_X=P_Y$, the claim of its opening sentence.
• Ruling out trivial readings. A Bochner integral of a non-integrable function is $0$ in Lean, so every expectation in every statement carries the integrability that makes it the paper's integral. Without it, properness could hold because both sides are $0$. The characterization hypothesis is never assumed for the pair $(P_X,P_Y)$ alone.
• Needed infrastructure: product-measure Fubini (integral_integral_swap), integrability of products and squares, and uniqueness of measures from a generating π-system. A general lemma "a multivariate CDF determines its measure" would be reusable well beyond this mission and is welcome as a separate contribution.

Selected references

• X. Meng, J. W. Taylor, S. Ben Taieb, S. Li, Scores for Multivariate Distributions and Level Sets, Operations Research, 2025; preprint arXiv:2002.09578v6, 2023. https://arxiv.org/abs/2002.09578v6
• T. Gneiting, A. E. Raftery, Strictly Proper Scoring Rules, Prediction, and Estimation, Journal of the American Statistical Association 102(477), 359–378, 2007. https://doi.org/10.1198/016214506000000437
• T. Gneiting, R. Ranjan, Comparing Density Forecasts Using Threshold- and Quantile-Weighted Scoring Rules, Journal of Business & Economic Statistics 29(3), 411–422, 2011. https://doi.org/10.1198/jbes.2010.08110

Motivation

Risk sharing asks how a total loss $X$ should be split among $n$ agents, each of whom evaluates its share with its own risk measure, so that the sum of their assessments is as small as possible. The smallest achievable sum is the inf-convolution of the agents' risk measures, and an allocation that attains it is an optimal allocation. For Value-at-Risk, the risk measure of the Basel framework, this problem was solved by Embrechts, Liu and Wang (2018) and extended to agents with heterogeneous beliefs by Embrechts, Liu, Mao and Wang (2020).

Lambda Value-at-Risk ($\Lambda\mathrm{VaR}$), introduced by Frittelli, Maggis and Peri (2014), replaces the fixed confidence level of VaR by a function $\Lambda$ of the loss threshold, so that the tolerated exceedance probability may depend on the size of the loss. Liu and Schied (2025) study $\Lambda\mathrm{VaR}$ when probabilities are replaced by capacities, which model ambiguity about the underlying distribution: a capacity can be the upper envelope of a family of probability measures. Their Section 5.1 answers the question of what the inf-convolution of such risk measures is, which earlier work had settled for constant $\Lambda$ under capacities (Choquet quantiles, Liu, Mao and Wang 2024) and for $\Lambda\mathrm{VaR}$ under probability measures (Liu 2025; Liu, Tsanakas and Wei 2025).

Setting

$(\Omega,\mathcal F)$ is a measurable space and $\mathcal X$ a set of random variables containing every bounded one. A capacity is a map $w:\mathcal F\to[0,1]$ that is increasing for inclusion with $w(\emptyset)=0$ and $w(\Omega)=1$; it is continuous if $w(A_n)\to0$ whenever $A_n\downarrow\emptyset$. For a function $\Lambda:\mathbb R\to(0,1)$ (the class $\mathcal H$; increasing members form $\mathcal H_I$) and a capacity $w$,

$$\Lambda\mathrm{VaR}^w(X)=\inf\{x\in\mathbb R:\ w(X>x)\le\Lambda(x)\},\qquad\inf\emptyset=+\infty,$$

a value in $[-\infty,\infty]$. $\mathcal H^*_I$ ($\mathcal H^*_D$) denotes the increasing (decreasing) functions $\mathbb R\to(0,1]$.

The allocations of $X$ are $\mathbb A_n(X)=\{(X_1,\dots,X_n)\in\mathcal X^n:\sum_iX_i=X\}$, and the inf-convolution of $\rho_1,\dots,\rho_n$ is

$$\mathop{\square}_{i=1}^n\rho_i(X)=\inf\Big\{\sum_{i=1}^n\rho_i(X_i):(X_1,\dots,X_n)\in\mathbb A_n(X)\Big\}.$$

A downset is a collection $\mathcal A\subseteq\mathcal F$ containing $\emptyset$ and closed under taking measurable subsets. A family $\{\mathcal A_x\}_{x\in\mathbb R}$ of downsets induces the risk measure $\rho(X)=\inf\{x:\{X>x\}\in\mathcal A_x\}$. For $\boldsymbol\Lambda=(\Lambda_1,\dots,\Lambda_n)$ and $\mathbf w=(w_1,\dots,w_n)$ the paper defines

$$\mathcal A^{\boldsymbol\Lambda,\mathbf w}_x=\Big\{\bigcup_{i=1}^nA_i:\ w_i(A_i)\le\Lambda_i(y_i),\ i\in[n],\ \textstyle\sum_iy_i=x\Big\},$$

and $\Pi_n(\Omega)$ denotes the measurable partitions of $\Omega$ into $n$ (possibly empty) parts.

Formalization targets

Goal: Proposition 8

For $\Lambda_i\in\mathcal H$ with $\lambda^-_i=\inf\Lambda_i>0$ and continuous capacities $w_1,\dots,w_n$:

$$\mathop{\square}_{i=1}^n\Lambda_i\mathrm{VaR}^{w_i}(X)=\inf\{x\in\mathbb R:\{X>x\}\in\mathcal A^{\boldsymbol\Lambda,\mathbf w}_x\};$$

if this infimum is attained at $x^*$, then $X_i=(X-x^*)\mathbb 1_{A^*_i}+y^*_i$ is optimal for every $(y^*_i)$ with $\sum_iy^*_i=x^*$ and $(A^*_i)\in\Pi_n(\Omega)$ with $w_i(\{X>x^*\}\cap A^*_i)\le\Lambda_i(y^*_i)$ (and such data exist); and if all $\Lambda_i$ are increasing, the inf-convolution equals $\Lambda\mathrm{VaR}^w$ for some $\Lambda\in\mathcal H^*_I$ and capacity $w$.

Milestones

• Remark 1: under a continuous capacity, $\Lambda\mathrm{VaR}^w(X)<\infty$ when $\inf\Lambda>0$ or $\Lambda\in\mathcal H_I$.
• Theorem 3 (7): for risk measures $\rho_i$ induced by families of downsets $\{\mathcal A^{(i)}_x\}$ with values in $[-\infty,\infty)$, $\mathop{\square}\rho_i(X)=\inf\{x:\{X>x\}\in\widetilde{\mathcal A}_x\}$, where $\widetilde{\mathcal A}_x=\bigcup_{y_1+\dots+y_n=x}\{\bigcup_iA_i:A_i\in\mathcal A^{(i)}_{y_i}\}$.
• Theorem 3 (8): a minimizer of (7) yields the optimal allocation $(X-x^*)\mathbb 1_{A^*_i}+y^*_i$.
• Theorem 3, monotonicity: $\{\widetilde{\mathcal A}_x\}$ is increasing (decreasing) when all input families are.
• Theorem 1 (i): $\rho$ is a $\Lambda\mathrm{VaR}^w$ with $\Lambda\in\mathcal H^*_I$ iff it is induced by an increasing family of downsets.
• Theorem 1 (ii): the decreasing, left-continuous counterpart.

Significance

Proposition 8 shows that risk measures of $\Lambda\mathrm{VaR}$ type, under possibly different capacities for different agents, are closed under inf-convolution when all $\Lambda_i$ increase, and it gives explicit optimal allocations: each agent pays a fixed amount $y^*_i$ and carries the excess $X-x^*$ on one cell of a partition. It contains as special cases the inf-convolution of VaR (Embrechts et al. 2018), of VaR with heterogeneous beliefs (Embrechts et al. 2020) and of Choquet quantiles (Liu, Mao and Wang 2024). Via the paper's Corollary 4 it yields risk sharing for robust $\Lambda\mathrm{VaR}$ over sets of probability measures.

The result is proved in the preprint; it has no machine-checked proof. A formalization adds a verified account of the extended-real bookkeeping that the paper leaves implicit, and it pins down which printed claims hold: two claims in the preprint are false (see Formalization scope), which a formal development has to avoid.

Difficulty

The individual risk measures are not real-valued: $\Lambda_i\mathrm{VaR}^{w_i}$ can be $-\infty$, and without the finiteness of Remark 1 it can be $+\infty$, in which case a sum over agents is meaningless. Every step of (9) therefore has to be carried out in the extended reals, and the identity has to hold in the degenerate cases (an empty or unbounded threshold set) as well as the generic one. Capacities are neither additive nor continuous from above in general, so the familiar quantile arguments for probability measures do not transfer.

The last claim of the goal is not a consequence of (9) alone: it needs the representation Theorem 1 (i), whose converse direction must produce a $\Lambda$ and a capacity from an abstract increasing family of downsets, including degenerate families in which $\Omega$ itself is eventually admissible or no nonempty event ever is. The natural first idea, that the decreasing case is symmetric, fails: the convolved family of downsets need not be left-continuous, and the decreasing analogue of the claim is false.

Formalization scope

Lean namespace LambdaVaRAmb.InfConv. Random variables are measurable maps $\Omega\to\mathbb R$; the domain $\mathcal X$ is any set of functions that contains all bounded measurable functions, consists of measurable functions, and is closed under $X\mapsto(X-c)\mathbb 1_A+d$ and under $X\mapsto f(X)$ for increasing 1-Lipschitz $f$ with $f(0)=0$. This is the disclosed reading of the paper's "good enough properties"; bounded and all measurable functions both qualify. Capacities are real set functions whose axioms are imposed on measurable sets. $\Lambda\mathrm{VaR}$, induced risk measures and the inf-convolution are valued in EReal, with $\inf\emptyset=+\infty$. Agents are indexed by Fin n with $n\ge1$ (implicit in the paper). "Increasing" is Monotone; left-continuity of $\Lambda$ is continuity within $(-\infty,x]$; "admits a minimizer" is attainment of the infimum (IsLeast).

Not posed, because false: the claim of Theorem 3 that $\{\widetilde{\mathcal A}_x\}$ is left-continuous when all input families decrease, and the decreasing branch of Proposition 8. With $w_1=w_2$ Lebesgue measure on $[0,1]$, $\Lambda_1$ equal to $0.4$ on $(-\infty,0)$ and $0.1$ on $[0,\infty)$, and $\Lambda_2(y)=0.1+0.4/(1+e^y)$, the convolved family is not left-continuous and the inf-convolution is not a $\Lambda\mathrm{VaR}^w$ with decreasing $\Lambda$. The goal states the increasing branch only.

Trivializing encodings are ruled out: infima are taken in EReal (a real sInf would collapse unbounded sets to $0$); the finiteness hypothesis of Theorem 3 keeps $+\infty$ and $-\infty$ out of the sums; the domain $\mathcal X$ is constrained so that the tail allocations lie in it; downsets consist of events; the allocation clause comes with an existence clause so that it cannot hold vacuously; and the representing pair $(\Lambda,w)$ is chosen uniformly in $X$. Sanity checks (not part of the mission) confirm that the hypotheses of Proposition 8 are satisfiable and that $\Lambda\mathrm{VaR}$ of a constant is that constant.

Contributions welcome: Remark 1 and the monotonicity milestone are short and independent; Theorem 3 is reusable for any risk measure induced by downsets; Theorem 1 is a general representation result for $\Lambda\mathrm{VaR}$ under capacities.

Selected references

• P. Liu and A. Schied, Lambda Value-at-Risk under ambiguity and risk sharing, arXiv preprint, 2025. https://arxiv.org/abs/2511.00717v1
• M. Frittelli, M. Maggis and I. Peri, Risk measures on $\mathcal P(\mathbb R)$ and Value at Risk with probability/loss function, Mathematical Finance 24(3), 442–463, 2014.
• P. Embrechts, H. Liu and R. Wang, Quantile-based risk sharing, Operations Research 66(4), 936–949, 2018. https://doi.org/10.1287/opre.2017.1716
• P. Embrechts, H. Liu, T. Mao and R. Wang, Quantile-based risk sharing with heterogeneous beliefs, Mathematical Programming Series B 181(2), 319–347, 2020. https://doi.org/10.1007/s10107-018-1313-1
• P. Liu, Risk sharing with Lambda value at risk, Mathematics of Operations Research 50(1), 313–333, 2025.
• P. Liu, T. Mao and R. Wang, Quantiles under ambiguity and risk sharing, arXiv preprint, 2024. https://arxiv.org/abs/2412.19546v1
• P. Liu, A. Tsanakas and Y. Wei, Risk sharing with Lambda Value-at-Risk under heterogeneous beliefs, Finance and Stochastics, forthcoming. https://arxiv.org/abs/2408.03147

Motivation

Ranking and selection (R&S) asks which of $k$ simulated systems has the largest mean performance when every observation is costly. It is a basic tool of simulation optimization: choosing a staffing level, an inventory policy or a network design from a large catalogue of candidates that can only be evaluated by noisy simulation. In the fixed-budget formulation a total of $B$ observations is spent sequentially and one alternative is selected at the end; procedures are compared by their probability of correct selection (PCS).

Cloud and parallel computing have made problems with thousands to millions of alternatives routine, and the relevant question is how the budget must grow with $k$. A procedure is sample optimal if a budget $B = ck$, linear in $k$, keeps its PCS bounded away from zero as $k \to \infty$; a total budget of order $k$ is clearly necessary. Li, Fan and Hong (arXiv:2303.02951) show that the simplest procedure of all, the greedy procedure, which always samples the alternative with the largest current sample mean, is sample optimal. They also show that its PCS limit is strictly below one under the slippage configuration, however large $c$ is: the greedy procedure is not consistent. This mission formalizes the remedy: an exploration phase of $n_0$ observations per alternative before the greedy phase makes the procedure consistent.

Setting

There are $k$ alternatives. Alternative $i$ produces independent observations $X_{i1}, X_{i2}, \dots \sim N(\mu_i, \sigma_i^2)$, independent across alternatives, and alternative 1 is the unique best. The running average after $n$ observations is $\bar X_i(n) = \frac1n\sum_{j=1}^n X_{ij}$.

Assumption 1 (p. 12). There are constants $\gamma > 0$ and $\bar\sigma^2 > 0$ such that $\mu_1 - \max_{i \ge 2}\mu_i \ge \gamma$ and $\max_i \sigma_i^2 \le \bar\sigma^2$, regardless of how large $k$ is.

The explore-first greedy (EFG) procedure (Procedure 2, p. 21) with exploration size $n_0$ and budget $B$:

1. take $n_0$ observations from every alternative, and set $n_i = n_0$;
2. while $\sum_i n_i < B$, take one more observation from $\arg\max_i \bar X_i(n_i)$;
3. select $\arg\max_i \bar X_i(n_i)$.

With $B = ck$ the exploration phase uses $n_0 k$ observations and the greedy phase $n_g k$, where $n_g = c - n_0$. The greedy procedure is the case $n_0 = 1$.

Crossing times. Let $Z_1, Z_2, \dots$ be iid standard normal, $\bar Z(n) = \frac1n\sum_{j=1}^n Z_j$, and

$$\tilde N(x; n_0) = \inf\{n \ge n_0 : \bar Z(n) < x\}, \qquad C(x; n_0) = \mathrm E\big[\tilde N(x; n_0)\big] \in [0, \infty],$$

with $\inf \emptyset = \infty$. $C(\cdot\,; n_0)$ is finite exactly on $(0, \infty)$, where it is strictly decreasing and continuous.

Consistency (Definition 2, p. 21): A sample-optimal fixed-budget R&S procedure is consistent if the PCS of the procedure satisfies that, for any $\alpha \in (0,1)$, there exists a constant $c>0$ such that $\liminf_{k\to\infty} \mathrm{PCS} \ge \alpha$, for $B = ck$.

Formalization targets

Goal: Theorem 4 (p. 24)

Suppose Assumption 1 holds. Let $\alpha \in (0,1)$ and $\gamma_0 \in (0, \gamma)$. Let $n_0 \ge 1$ satisfy

$$\Pr\Big\{\min_{n \ge n_0} \bar X_1(n) > \mu_1 - \gamma_0\Big\} \ge \alpha \tag{5.3}$$

and let $n_g \ge C\big(\tfrac{\gamma - \gamma_0}{\bar\sigma}; n_0\big) - n_0$. If $B = (n_0 + n_g)k$, then the PCS of the EFG procedure satisfies

$$\liminf_{k \to \infty} \mathrm{PCS} \ \ge\ \alpha .$$

Milestones

1. Lemma 3 (p. 22): $\bar Z(n)$, $n \ge n_0$, attains its minimum at a finite time almost surely.
2. (5.1) (p. 22): $\tilde N(x) \le \tilde N(x; n_0) \le n_0 \inf\{m \ge 1 : \bar Z(mn_0) < x\}$, and the last crossing time is distributed as $\tilde N(\sqrt{n_0}\,x)$ (scaling corrected, see below).
3. Lemma 4 (p. 22): $\tilde N(x;n_0)$ is a.s. finite with finite mean for $x > 0$; finite with probability strictly between 0 and 1, with infinite mean, for $x < 0$; a.s. finite with infinite mean for $x = 0$.
4. Lemma 7 (p. ec6): $C(x; n_0)$ is strictly decreasing and continuous on $(0, \infty)$.
5. (5.2) (p. 23): $\mathrm{PCS} \ge \Pr\big\{\sum_{i=2}^k N_i(\bar X_1^*(n_0); n_0) + N_1^*(n_0) \le B\big\}$, where $\bar X_1^*(n_0)$ and $N_1^*(n_0)$ are the minimum and argmin of $\bar X_1(n)$ over $n \ge n_0$, and $N_i(b; n_0)$ is the first $n \ge n_0$ with $\bar X_i(n) < b$.
6. Theorem 3 (p. 23, first sentence): if $B/k = n_0 + n_g$ and $n_g > C(\gamma/\bar\sigma; n_0) - n_0$, then $\liminf_k \mathrm{PCS} \ge \Pr\{\min_{n\ge n_0}\bar X_1(n) > \mu_1 - \gamma_0\}$, where $\gamma_0 \in (0, \gamma)$ solves $C\big(\tfrac{\gamma-\gamma_0}{\bar\sigma}; n_0\big) = n_g + n_0$.
7. Lemma 5 (p. 24): for every $\gamma_0 > 0$ and $\alpha \in (0,1)$ some finite $n_0 \ge 1$ satisfies (5.3).

Significance

The result. Theorem 4 shows that a one-line change to the greedy procedure, a fixed number of initial observations per alternative, turns a sample-optimal but inconsistent procedure into one that is both sample optimal and consistent. Any PCS target is reached with a budget that grows only linearly in the number of alternatives, without variance estimates, elimination rules or pairwise comparisons. Together with (5.4) (p. 24) it also gives a recipe for choosing $n_0$ and $n_g$ when $\gamma$ and $\bar\sigma^2$ are known, which converts the fixed-budget procedure into a fixed-precision one.

Formalizing it. The results are proved in the paper, but Lemma 4 and Theorem 4 have their proofs omitted ("straightforward"), and Theorem 3's proof refers to "almost the same analysis" as Theorem 1. A machine-checked development makes these steps explicit. It also corrects the scaling in (5.1), which is misprinted in the source. No part of it is formalized on the platform. The boundary-crossing inequality (5.2) and the crossing-time lemmas for the Gaussian running average are reusable in the companion missions of this series and for other greedy procedures.

Difficulty

The obvious approach is to bound each inferior alternative's sample size by the number of observations it needs to fall below alternative 1, and to sum. It fails because alternative 1's running average is itself random, may drop below its mean, and can lose the lead at any time before it reaches its minimum. The boundary must be the random minimum $\bar X_1^*(n_0)$, and the crossing times of the other alternatives are then dependent through it. The step from (5.2) to Theorem 3 needs crossing times dominated by iid copies of $\tilde N(\cdot\,; n_0)$ on the event that the minimum is high, a strong law over the growing array, and the continuity of $C(\cdot\,; n_0)$ (Lemma 7) to pass to the limit in the level. Lemma 4 needs fluctuation facts for the Gaussian random walk (finite expected crossing time for $x>0$, infinite mean at $x=0$) that are not in Mathlib.

Formalization scope

• Model. Observations form an array $X_{ij}$ indexed by $\mathbb N \times \mathbb N$ on a probability space, mutually independent, with $X_{ij} \sim N(\mu_i, \sigma_i^2)$ and $\sigma_i^2 > 0$. Problem $k$ uses alternatives $0, \dots, k-1$; Lean's alternative $0$ is the paper's alternative 1. One array serves every $k$, which does not change any PCS.

• Procedure. The EFG procedure is a deterministic map from the observation array to the selected index. Ties in every arg max go to the smallest index, which is a null event under the model. The greedy loop runs $B - n_0k$ times (none if $B \le n_0k$).

• Budget. $B = (n_0 + n_g)k$ is read as $\lfloor (n_0+n_g)k \rfloor$. Conditions involving $C(\cdot\,; n_0) - n_0$ are written additively in $[0, \infty]$.

• Crossing times, argmins and $C$. These take values in $\mathbb N \cup \{\infty\}$ and $[0, \infty]$. A path that never crosses has crossing time $\infty$, and $C(0; n_0) = \infty$ is literal. "$\min_{n \ge n_0} \bar X_1(n) > a$" means that the path is bounded below from $n_0$ on and its infimum exceeds $a$. The minimum is attained a.s. (Lemma 3).

• Probabilities and limits. These are extended nonnegative reals. The liminf is taken in $[0, \infty]$.

• (5.1) correction. The paper derives $\tilde N(x;n_0) \le n_0\tilde N(x/\sqrt{n_0})$ from "$\bar Z(mn_0) = \sqrt{n_0}\,\bar Z(m)$ statistically". In fact $\bar Z(mn_0) \overset{d}{=} \bar Z(m)/\sqrt{n_0}$, so the milestone states the bound with $\tilde N(\sqrt{n_0}\,x)$. The printed form is false for $x < 0$ and $n_0 \ge 2$.

• Theorem 3. The existence of $\gamma_0$, implicit in the paper, is a conclusion of the statement, so the lower bound cannot hold vacuously. The slippage-configuration limit in its second sentence is not stated.

• Ruled out. None of the following can make the statements trivial, because the encodings above exclude them:

  • an $\mathbb N$-valued crossing time with $\inf\emptyset = 0$;
  • a real infimum of an unbounded path read as $0$;
  • an unsolvable equation for $\gamma_0$.

• Infrastructure needed. A complete development needs the following, all reusable beyond this mission:

  • laws of crossing times of the Gaussian random walk;
  • the strong law for iid $\mathbb N\cup\{\infty\}$-valued variables;
  • a coupling of the crossing times with iid copies;
  • a pathwise induction over the run of the procedure for (5.2).

  Contributions to any milestone are welcome.

• Source. The source is the authors' arXiv preprint, version 3 (11 Dec 2023), and all numbering follows it.

Selected references

• Z. Li, W. Fan, L. J. Hong, The (Surprising) Sample Optimality of Greedy Procedures for Large-Scale Ranking and Selection, arXiv:2303.02951v3, 2023; Management Science, 2025. https://arxiv.org/abs/2303.02951
• R. E. Bechhofer, A single-sample multiple decision procedure for ranking means of normal populations with known variances, Annals of Mathematical Statistics 25(1):16–39, 1954. https://doi.org/10.1214/aoms/1177728845
• S.-H. Kim, B. L. Nelson, A fully sequential procedure for indifference-zone selection in simulation, ACM Transactions on Modeling and Computer Simulation 11(3):251–273, 2001. https://doi.org/10.1145/502109.502111