Probability

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the values of an objective function but not to its gradient: the function is computed by a black-box program, by a simulator, or by a model whose derivatives are unavailable or too expensive. Zeroth-order (or derivative-free) methods use only function values. Classical direct-search methods of this kind usually come without complexity bounds.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that a very simple randomized scheme has explicit, dimension-dependent worst-case complexity bounds. The idea is to replace the gradient by a finite difference of $f$ along a random Gaussian direction. The resulting oracle is an unbiased estimate of the gradient of a smoothed version of $f$. Their analysis is the reference point for the later literature on zeroth-order stochastic optimization, bandit convex optimization and gradient-free training.

This mission covers the paper's result for nonsmooth convex problems over a closed convex set: the projected random search method $\mathcal{RS}_\mu$ and its convergence bound, Theorem 6.

Setting

Let $E$ be a real inner product space of finite dimension $n$, with norm $\|\cdot\|$. (The paper works with a space carrying a positive definite operator $B$ and the norm $\langle Bx, x\rangle^{1/2}$. This is the same thing as an arbitrary finite-dimensional inner product space, with $B$ encoding the inner product, and the development is written in that generality.)

A function $f : E \to \mathbb R$ is Lipschitz continuous with constant $L_0 \ge 0$ if $|f(x) - f(y)| \le L_0 \|x - y\|$ for all $x, y$. The paper calls this class $C^{0,0}(E)$ and writes $L_0(f)$ for the constant.

Let $u$ be a standard Gaussian vector in $E$: its coordinates in any orthonormal basis are independent $N(0,1)$ variables. For $\mu \ge 0$ the Gaussian smoothing of $f$ is

$$f_\mu(x) = \mathbb E_u\, f(x + \mu u),$$

and the Gaussian moments are $M_p = \mathbb E_u \|u\|^p$.

For $\mu > 0$ the random gradient-free oracle at $x$ draws $u$ and returns the vector

$$g_\mu(x) = \frac{f(x+\mu u) - f(x)}{\mu}\, u .$$

It costs two function values.

The problem is

$$f^* = \min_{x \in Q} f(x),$$

where $Q \subseteq E$ is closed and convex, $f$ is convex and Lipschitz, and $x^* \in Q$ is a minimizer. With $\pi_Q$ the Euclidean projection onto $Q$, positive steps $h_0, h_1, \ldots$ and a starting point $x_0 \in Q$, the random search method $\mathcal{RS}_\mu$ iterates

$$x_{k+1} = \pi_Q\big(x_k - h_k\, g_\mu(x_k)\big),$$

drawing a fresh independent Gaussian direction $u_k$ at every iteration. The iterates are random. Write $\phi_k = \mathbb E f(x_k)$ and $S_N = \sum_{k=0}^N h_k$.

Formalization targets

Goal: Theorem 6

For every $N \ge 0$,

$$\frac{1}{S_N}\sum_{k=0}^{N} h_k(\phi_k - f^*) \le \mu L_0\, n^{1/2} + \frac{1}{S_N}\left[\frac12\|x_0 - x^*\|^2 + \frac{(n+4)^2}{2} L_0^2 \sum_{k=0}^{N} h_k^2\right].$$

The step sizes, the smoothing parameter and the horizon are left free, so every step-size rule in the paper follows from this one inequality. The constants are the paper's.

Milestones

The facts about smoothing and the oracle on which the goal rests, in the paper's order:

1. Lemma 1: $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$.
2. Theorem 1 (18): $|f_\mu(x) - f(x)| \le \mu L_0 n^{1/2}$.
3. Convexity of $f_\mu$ for convex $f$.
4. Eq. (11): $f_\mu \ge f$ for convex $f$.
5. Eq. (21): $\nabla f_\mu(x) = \mathbb E_u\, g_\mu(x)$ for $\mu > 0$.
6. Theorem 4.1 (34): $\mathbb E_u \|g_\mu(x)\|^2 \le L_0^2 (n+4)^2$.
7. Theorem 2 ($\mu \ge 0$): $f(y) \ge f(x) - \mu L_0 n^{1/2} + \langle \nabla f_\mu(x), y - x\rangle$ for all $y$, where at $\mu = 0$ the vector is the limiting $\nabla f_0(x) = \mathbb E_u[f'(x,u)\,u]$ of Eq. (24).

Significance

Theorem 6 shows that a method using only function values, with no subgradient, solves nonsmooth convex problems with the classical projected-subgradient guarantee. Two things change: $L_0^2$ is multiplied by $(n+4)^2$, and a bias $\mu L_0 n^{1/2}$ appears, which can be made as small as desired. With suitable $\mu$, $h_k$ and $N$ an $\epsilon$-accurate expected value is reached in $O(n^2 L_0^2 R^2/\epsilon^2)$ oracle calls. The factor $n^2$ quantifies the cost of not having gradients. The same analysis carries over to stochastic objectives (the paper's Theorem 7).

The results are proved in the paper. As far as is known, none of them has a machine-checked proof. The mission produces a Lean development of Gaussian smoothing on an arbitrary finite-dimensional inner product space: the moment bounds, the approximation, convexity and gradient identities, and the oracle variance bound. On top of it sits the full convergence theorem for a randomized projected method, stated for the actual random process rather than for an idealized expectation recursion. The smoothing layer is reusable: the same facts underlie the smooth and accelerated random methods of the same paper and most Gaussian-smoothing analyses in zeroth-order optimization.

Difficulty

A plain subgradient analysis does not apply. The vector $g_\mu(x_k)$ is not a subgradient of $f$, nor an unbiased estimate of one. It is an unbiased estimate of the gradient of a different function, $f_\mu$, and its second moment grows with the dimension. The argument therefore has to move between $f$ and $f_\mu$ at exactly the right places, using properties of $f_\mu$ that hold for every nonsmooth Lipschitz $f$.

Those properties are genuinely analytic. Differentiating $f_\mu$ requires differentiating a Gaussian integral of a function that need not be differentiable. The moment bounds need estimates of $\mathbb E\|u\|^p$ for real $p$. In the probabilistic part, $x_k$ depends on $u_0, \ldots, u_{k-1}$, and each one-step estimate has to be integrated using the independence of $u_k$ from the past. Mathlib provides the standard Gaussian measure and independence, but no Gaussian smoothing, no projection onto convex sets and no conditional-expectation argument for this kind of recursion.

Formalization scope

The space is E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E], and $n$ is Module.finrank ℝ E. No lower bound on $n$ is assumed. The Gaussian is ProbabilityTheory.stdGaussian E, and expectations are Bochner integrals against it. $f_\mu$ is the definition smoothing, $M_p$ is moment (with real exponent Real.rpow), and $g_\mu$ is oracle.

The projection is the relation IsMetricProjection Q y z ($z \in Q$ and $z$ is a nearest point of $Q$ to $y$). The run is the predicate IsRandomSearchRun: directions $u_k : \Omega \to E$ on a probability space $(\Omega, P)$, measurable, mutually independent (iIndepFun) and each with law stdGaussian E; a deterministic $x_0 \in Q$; and the update above for every $k$ and every outcome.

$\phi_k$ is $\int f(x_k)\,dP$. The Lipschitz constant $L_0 \ge 0$ is any constant satisfying the Lipschitz inequality. It is an explicit hypothesis, because the paper's bound uses $L_0(f)$, which presupposes $f \in C^{0,0}(E)$. The smoothing parameter satisfies $\mu > 0$ and every step satisfies $h_k > 0$.

Two trivializing formalizations are ruled out. First, an expectation of a non-integrable function would be $0$ as a Bochner integral; Lipschitz continuity of $f$ makes every expectation in the mission integrable, and no statement relies on the junk value. Second, a run whose directions are not independent standard Gaussians, or whose update uses a subgradient instead of the finite difference, is a different theorem (the projected subgradient method). The run predicate fixes the paper's process exactly. A run exists for every closed $Q$ containing $x_0$ (on the countable product of Gaussians), so the goal is not vacuous.

A complete development needs:

• Gaussian integration by parts, or differentiation under the integral, for Lipschitz integrands;
• moment estimates for the standard Gaussian norm;
• existence and nonexpansiveness of projections onto closed convex sets;
• an expectation argument for the random recursion.

The smoothing lemmas, the moment bounds and the projection facts are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, general lemmas about stdGaussian and projections, and alternative proofs of Lemma 1 (for example through the chi distribution).

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• A. D. Flaxman, A. T. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
• J. C. Duchi, M. I. Jordan, M. J. Wainwright, A. Wibisono, Optimal rates for zero-order convex optimization: the power of two function evaluations, IEEE Trans. Inf. Theory 61(5):2788–2806, 2015. https://arxiv.org/abs/1312.2139

Motivation

The capacitated vehicle routing problem (CVRP) asks for delivery routes of minimum cost. Each route starts and ends at a depot, every customer is visited exactly once, and the demand served on a route does not exceed the vehicle capacity. The problem is central in logistics and one of the most studied problems in combinatorial optimization. Its standard exact methods are branch-and-cut algorithms built on the two-index vehicle flow formulation, a 0/1 program over arcs whose capacity constraints are the rounded capacity inequalities (RCIs); see Laporte, Nobert and Desrochers (1985) and Semet, Toth and Vigo (2014).

In practice customer demands are uncertain. A chance-constrained CVRP requires each route to respect its capacity with probability at least $1-\epsilon$ under a known distribution. That distribution is rarely known. Most solution methods also need independent demands. Ghosal and Wiesemann (Oper. Res. 68(3), 2020) study the distributionally robust chance-constrained CVRP. There the chance constraint must hold for every distribution in an ambiguity set $\mathcal P$ of plausible distributions. The ambiguity set may contain dependent distributions and uncountably many of them, so it is not clear a priori that the problem can be solved by the usual branch-and-cut machinery. This mission formalizes the paper's answer to that question: its Theorem 1 and the counterexample that precedes it.

Setting

The graph is complete and directed. Its nodes are $V=\{0,\dots,n\}$ and its arcs are $A=\{(i,j)\in V\times V:i\neq j\}$. Node $0$ is the depot and $V_C=\{1,\dots,n\}$ are the customers. There are $m$ vehicles, indexed by $K=\{1,\dots,m\}$, each of capacity $Q>0$. Traversing the arc $(i,j)$ costs $c(i,j)\ge 0$; costs may be asymmetric.

A route $\mathbf R_k=(R_{k,1},\dots,R_{k,n_k})$ is an ordered list of customers, with $R_{k,0}=R_{k,n_k+1}=0$. A route set $\mathbf R=(\mathbf R_1,\dots,\mathbf R_m)\in\mathfrak P(V_C,m)$ partitions $V_C$ into $m$ nonempty ordered routes. Its cost is $c(\mathbf R)=\sum_{k}\sum_{l=0}^{n_k}c(R_{k,l},R_{k,l+1})$.

The demand vector $\tilde{\boldsymbol q}\in\mathbb R^n$ is random. The ambiguity set $\mathcal P$ is a set of probability distributions of $\tilde{\boldsymbol q}$ and $\epsilon\in(0,1)$ is the risk level. The problem RVRP($\mathcal P$) minimizes $c(\mathbf R)$ over route sets such that

$$\mathbb P\Big[\textstyle\sum_{i\in\mathbf R_k}\tilde q_i\le Q\Big]\ge 1-\epsilon\qquad\forall\,\mathbb P\in\mathcal P,\ \forall\,k\in K .$$

With $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]=\inf\{x:\mathbb Q[\tilde X\le x]\ge1-\epsilon\}$, the demand estimator of the paper's Eq. (2) is

$$d_{\mathcal P}(S)=\max\left\{\left\lceil\frac1Q\sup_{\mathbb P\in\mathcal P}\mathbb P\text{-VaR}_{1-\epsilon}\Big[\sum_{i\in S}\tilde q_i\Big]\right\rceil,1\right\}\quad(S\neq\emptyset),\qquad d_{\mathcal P}(\emptyset)=0 .$$

The problem 2VF($\mathcal P$) minimizes $\sum_{(i,j)\in A}c(i,j)x_{ij}$ over $x\in\{0,1\}^A$ with in- and out-degree $1$ at every customer and $m$ at the depot, and with the RCIs

$$\sum_{i\in V\setminus S}\sum_{j\in S}x_{ij}\ge d_{\mathcal P}(S)\qquad\forall\,S\subseteq V_C,\ S\neq\emptyset .$$

A route set induces the arc vector with $x_{ij}=1$ exactly when $(i,j)=(R_{k,l},R_{k,l+1})$ for some $k,l$ (the paper's Eq. (3)). The estimator satisfies the subadditivity condition (S) if $d_{\mathcal P}(S\cup T)\le d_{\mathcal P}(S)+d_{\mathcal P}(T)$ for all $S,T\subseteq V_C$.

Formalization targets

Goal: Theorem 1

Assume $\tilde{\boldsymbol q}\ge\mathbf 0$ $\mathbb P$-a.s. for all $\mathbb P\in\mathcal P$, and assume $d_{\mathcal P}$ is real valued and satisfies (S). Then:

$$\begin{aligned} &\text{(i)}\ \ \mathbf R \text{ feasible in RVRP}(\mathcal P)\ \Longrightarrow\ x(\mathbf R)\text{ feasible in 2VF}(\mathcal P),\ \ c(x(\mathbf R))=c(\mathbf R);\\ &\text{(ii)}\ \ x\text{ feasible in 2VF}(\mathcal P)\ \Longrightarrow\ x=x(\mathbf R)\text{ for an RVRP}(\mathcal P)\text{-feasible }\mathbf R,\text{ unique up to reordering routes},\ c(x)=c(\mathbf R). \end{aligned}$$

Milestones

1. The chance constraint $\mathbb Q[\tilde X\le\tau]\ge1-\epsilon$ is equivalent to $\mathbb Q\text{-VaR}_{1-\epsilon}[\tilde X]\le\tau$ (p. 720).
2. Eq. (1): a route satisfies its robust chance constraint if and only if the worst-case VaR of its cumulative demand is at most $Q$.
3. Example 1: an instance with two customers where a route set is RVRP($\mathcal P$)-feasible, yet its induced flow violates the RCI for $S=\{1,2\}$, since $d_{\mathcal P}(\{1,2\})\ge3$.
4. Example 1 (continued): on that instance $d_{\mathcal P}$ violates (S).
5. Theorem 1 (i) and 6. Theorem 1 (ii), stated separately.

Significance

Theorem 1 separates the modeling question from the algorithmic one. Whenever the ambiguity set yields a subadditive estimator, the distributionally robust CVRP is solved exactly by a two-index flow branch-and-cut. The only change from the deterministic case is the right-hand side $d_{\mathcal P}(S)$ of the RCIs, however many distributions $\mathcal P$ contains. The companion missions of this series show that (S) holds for every moment ambiguity set (Theorem 2 of the paper) and compute $d_{\mathcal P}$ for several classes of such sets. Example 1 shows that the hypothesis cannot be dropped: ambiguity sets that pin down each customer's marginal distribution break the equivalence.

The paper's proofs are in its online supplement; no machine-checked version of these statements exists. Formalizing them produces a checked reduction between a stochastic routing model and an integer program. It also produces reusable definitions of route sets, induced arc flows and RCIs over directed graphs with a depot.

Difficulty

Direction (ii) is a graph decomposition. A 0/1 vector with the prescribed degrees splits into $m$ depot cycles plus possibly depot-free subtours. The RCIs, through the $\max\{\cdot,1\}$ in $d_{\mathcal P}$, must exclude the subtours, and the RCI on the customers of a single route must enforce that route's chance constraint. Uniqueness up to reordering requires that directed routes are recovered from arcs.

Direction (i) is where (S) enters. The naive argument bounds the number of vehicles entering $S$ by $d_{\mathcal P}(S)$ directly from the chance constraints. It fails because the chance constraints control each route separately, while $d_{\mathcal P}(S)$ looks at the joint worst case of the demands in $S$; Example 1 is exactly this failure. A set $S$ is typically visited by several routes, each covering only part of it. Relating the per-route guarantees to the joint quantity $d_{\mathcal P}(S)$ needs both hypotheses of the theorem: nonnegative demands and (S).

Formalization scope

Customers are Fin n (0-based; the paper's customer $i$ is i - 1). Nodes are Fin (n+1) with the depot 0 and customer i at i.succ, and vehicles are Fin m. A route set is R : Fin m → List (Fin n): every route is nonempty and the concatenated routes are a permutation of all customers. Arc vectors are ℕ-valued functions on ordered node pairs, with values in $\{0,1\}$ and the non-arcs $(i,i)$ fixed to $0$.

Distributions are measures on Fin n → ℝ, and the ambiguity set is a set of probability measures. Chance constraints are written ENNReal.ofReal (1 - ε) ≤ P {q | …}. Value-at-risk is the published MultistageStochastic.valueAtRisk at level 1 - ε. The worst-case VaR is a real sSup and $d_{\mathcal P}$ is integer valued.

Two conventions implicit on the page are explicit hypotheses:

• $Q>0$, because (2) divides by $Q$;
• boundedness of the VaR values for every customer set, which encodes the paper's declaration $d_{\mathcal P}:2^{V_C}\to\mathbb R_+$.

A real sSup of an unbounded set is $0$ in Lean. Without the boundedness hypothesis every such estimator would silently equal $1$ and (ii) would fail. For an empty ambiguity set the Lean estimator equals $1$ on nonempty sets, as the paper's does.

The RCIs range over all nonempty customer sets with the depot on the outside. The estimator keeps the ceiling and the $\max\{\cdot,1\}$. 2VF feasibility mentions neither routes nor chance constraints. RVRP feasibility does not mention $d_{\mathcal P}$. A formalization in which either side refers to the other, or in which $d_{\mathcal P}$ drops the $\max\{\cdot,1\}$, is not this theorem.

Useful contributions include lemmas on the decomposition of degree-constrained 0/1 arc vectors into depot cycles, monotonicity of VaR under almost-sure ordering, and the CDF right-continuity behind milestone 1.

Related platform work: SupplyChainTheory_vrp formalizes a different, symmetric, unit-demand VRP and is not reused.

Selected references

• S. Ghosal, W. Wiesemann, The Distributionally Robust Chance-Constrained Vehicle Routing Problem, Operations Research 68(3):716–732, 2020. https://doi.org/10.1287/opre.2019.1924
• G. Laporte, Y. Nobert, M. Desrochers, Optimal routing under capacity and distance restrictions, Operations Research 33(5):1050–1073, 1985. https://doi.org/10.1287/opre.33.5.1050
• F. Semet, P. Toth, D. Vigo, Classical exact algorithms for the capacitated vehicle routing problem, in P. Toth, D. Vigo (eds.), Vehicle Routing: Problems, Methods, and Applications, 2nd ed., SIAM, 2014, 37–57. https://doi.org/10.1137/1.9781611973594.ch2
• J. Lysgaard, A. N. Letchford, R. W. Eglese, A new branch-and-cut algorithm for the capacitated vehicle routing problem, Mathematical Programming 100(2):423–445, 2004. https://doi.org/10.1007/s10107-003-0481-8

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions ("arms") one at a time, and must eventually stop and name the arm with the largest mean, with an error probability at most a prescribed risk $\delta$, while using as few samples as possible. The problem goes back to the sequential design of experiments (Chernoff, 1959; Even-Dar, Mannor and Mansour, 2006) and underlies adaptive A/B testing, clinical trial design and hyperparameter selection.

Any fixed-confidence strategy consists of three parts: a sampling rule, a stopping rule and a decision rule. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) proposed the Track-and-Stop strategy, the first shown to match the asymptotic lower bound on the expected sample complexity. Its stopping rule is a generalized likelihood ratio (GLR) test, Chernoff's stopping rule. Its correctness, the guarantee that the recommended arm is wrong with probability at most $\delta$, must hold whatever the sampling rule, which is what allows the sampling rule to be tuned freely for efficiency. This mission formalizes that guarantee for Bernoulli arms, Theorem 10 of the paper, with its explicit threshold $\beta(t,\delta) = \log(2t(K-1)/\delta)$.

Setting

The arms are $\mathcal A = \{1,\dots,K\}$. A Bernoulli bandit model is a mean vector $\boldsymbol\mu = (\mu_1,\dots,\mu_K) \in [0,1]^K$: pulling arm $a$ returns reward $1$ with probability $\mu_a$ and $0$ otherwise, independently of the past. The class $\mathcal S$ contains the models with a unique optimal arm $a^*(\boldsymbol\mu)$, i.e. $\mu_{a^*} > \mu_i$ for all $i \ne a^*$.

At round $t$ the learner chooses an arm $A_t$ as a (possibly randomized) function of the past observations and observes a reward $X_t$. Write $N_a(t)$ for the number of pulls of arm $a$ among the first $t$ rounds, $s_a(t)$ for the number of those pulls that returned $1$, and $\hat\mu_a(t) = N_a(t)^{-1}\sum_{s \le t} X_s \mathbb 1\{A_s = a\}$ for the empirical mean. The likelihood of arm $a$'s observations under mean $u$ is $p_u(\underline X^a_{N_a(t)}) = u^{s_a(t)}(1-u)^{N_a(t)-s_a(t)}$.

The GLR statistic for "arm $a$ is at least as good as arm $b$" is

$$Z_{a,b}(t) = \log \frac{\max_{\mu'_a \ge \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}{\max_{\mu'_a \le \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}.$$

Chernoff's stopping rule with exploration rate $\beta(t,\delta)$ is

$$\tau_\delta = \inf\{t \ge 1 : \exists a \in \mathcal A,\ \forall b \ne a,\ Z_{a,b}(t) > \beta(t,\delta)\},$$

and the decision rule recommends $\hat a_{\tau_\delta} \in \operatorname{argmax}_a \hat\mu_a(\tau_\delta)$.

The Krichevsky–Trofimov (KT) distribution on binary sequences $x \in \{0,1\}^n$ is $\mathrm{kt}(x) = \int_0^1 \big(\pi\sqrt{u(1-u)}\big)^{-1} p_u(x)\,\mathrm du$, the Bernoulli likelihood mixed over the Beta$(1/2,1/2)$ prior.

Formalization targets

Goal: Theorem 10

For every $\delta \in (0,1)$, every sampling strategy, and the threshold $\beta(t,\delta) = \log\big(2t(K-1)/\delta\big)$,

$$\forall \boldsymbol\mu \in \mathcal S,\qquad \mathbb P_{\boldsymbol\mu}\big(\tau_\delta < \infty,\ \hat a_{\tau_\delta} \ne a^*\big) \le \delta .$$

Milestone: Lemma 11 (Willems, Shtarkov and Tjalkens, 1995)

$\mathrm{kt}$ is a probability law on $\{0,1\}^n$, and for $n \ge 1$,

$$\sup_{x\in\{0,1\}^n}\ \sup_{u\in[0,1]} \frac{p_u(x)}{\mathrm{kt}(x)} \le 2\sqrt n .$$

Milestone: the pairwise crossing bound of Appendix C.1

With $T_{a,b} = \inf\{t : Z_{a,b}(t) > \beta(t,\delta)\}$, for all arms with $\mu_a < \mu_b$,

$$\mathbb P_{\boldsymbol\mu}(T_{a,b} < \infty) \le \frac{\delta}{K-1}.$$

Significance

Theorem 10 decouples correctness from efficiency. Because the guarantee holds for every sampling strategy, any sampling rule, including the C-Tracking and D-Tracking rules of Track-and-Stop, the uniform rule, or a heuristic, inherits $\delta$-correctness as soon as it is paired with Chernoff's stopping rule at this threshold. The asymptotic optimality result of the paper (Theorem 14) then only has to control the sample complexity. The threshold is explicit, with no unspecified constant, in contrast to the deviational threshold of Proposition 12.

The result is proved in the paper, in Appendix C.1, and rests on Lemma 11, which the paper quotes from the universal coding literature without proof. As far as the platform's catalog shows, none of these results is formalized. The platform holds a machine-checkable statement of the analogous result for Gaussian arms with the Lattimore–Szepesvári threshold (BanditAlgorithm.chernoff_stopping_rule_sound, Lemma 33.7 of Bandit Algorithms), which is a different model and a different threshold. Formalizing Theorem 10 adds a proof of Lemma 11 (the KT regret bound, reusable in information theory and universal prediction), the Bernoulli GLR statistic, and a change of measure from the true bandit law to a Bayesian mixture law on the trajectory space.

Difficulty

The obvious approach bounds, for each fixed $t$, the probability that $Z_{a,b}(t)$ exceeds $\beta(t,\delta)$ by a concentration inequality and sums over $t$. This fails: the sampling strategy is arbitrary and adaptive, so $N_a(t)$ and $N_b(t)$ are random and depend on the past rewards, and a fixed-sample-size deviation bound does not apply; a union bound over the possible values of the counts loses more than the threshold allows. The maximum likelihood in the numerator of $Z_{a,b}$ is also not a probability density, so the likelihood ratio cannot directly be read as a change of measure. The argument must control the whole trajectory law under an arbitrary randomized policy, and must handle empty samples (an arm never pulled contributes likelihood $1$) and the boundary means $0$ and $1$.

Formalization scope

The formalization is in Lean 4 with Mathlib and reuses the platform's canonical bandit model: StochasticBandit, BanditPolicy (a Markov kernel per round from the observed history to the next arm, so randomized strategies are included), banditTrajMeasure (the law of the infinite trajectory, where coordinate $s$ is round $s+1$) and IsSoundBAI from BanditTrajectory; bernoulliBandit from bernoulliRelativeEntropy; and only the pull counts trajPullCount and empirical means trajEmpiricalMean from TrackAndStop. The Gaussian GLR and threshold of TrackAndStop are not used.

Conventions committed to:

• Arms are Fin K. Bernoulli means range over $[0,1]$, degenerate laws included; the paper's exponential-family mean space is $(0,1)$, so the $[0,1]$ statement implies the paper's.
• $Z_{a,b}(t)$ is defined as the ratio of the two maxima over $[0,1]^2$, not by the closed form (7), which holds only when $\hat\mu_a(t) \ge \hat\mu_b(t)$. Both maxima are attained and positive.
• The stopping rule ranges over $t \ge 1$; at $t = 0$ there is no observation and the paper's $\beta(0,\delta) = \log 0$ is undefined. $\tau_\delta = \infty$ when the rule never fires.
• The decision rule is quantified: the goal holds for every recommendation that maximizes the empirical mean at $\tau_\delta$, whatever the tie-breaking.
• Probabilities of events are outer measures under the trajectory law; no measurability is assumed.
• $K \ge 1$ only. For $K = 1$ the statement is trivially true (no suboptimal arm).

Disclosed deviations from the page: Lemma 11's ratio bound is stated for $n \ge 1$, since at $n = 0$ the printed bound reads $1 \le 0$; the use of the lemma in Appendix C.1 is unaffected. Appendix C.1 calls the result "Proposition 10" (a slip for Theorem 10) and prints the KT density as $1/\sqrt{\pi u(1-u)}$ (a slip for $1/(\pi\sqrt{u(1-u)})$ of Lemma 11, which is the normalized one); the formalization follows Lemma 11.

A trivializing formalization is ruled out: stating the result for Gaussian arms or with the Lattimore–Szepesvári threshold is the platform's existing Lemma 33.7 and is not Theorem 10, and a free decision rule without the argmax hypothesis would make the claim false rather than faithful.

Contributions welcome: a proof of Lemma 11; a change-of-measure lemma for banditTrajMeasure under a mixture of environments; and the union-bound reduction from the goal to the pairwise claim.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2, 2016. https://arxiv.org/abs/1602.04589
• F. M. J. Willems, Y. M. Shtarkov, T. J. Tjalkens, The context-tree weighting method: basic properties, IEEE Transactions on Information Theory 41(3), 1995. https://doi.org/10.1109/18.382012
• R. Krichevsky, V. Trofimov, The performance of universal encoding, IEEE Transactions on Information Theory 27(2), 1981. https://doi.org/10.1109/TIT.1981.1056331
• H. Chernoff, Sequential design of experiments, Annals of Mathematical Statistics 30(3), 1959. https://doi.org/10.1214/aoms/1177706205
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 33. https://doi.org/10.1017/9781108571401

Motivation

Estimating a probability by the relative frequency of the event in an independent sample is justified for one event by the law of large numbers. Statistics and learning theory need more: the frequencies of a whole class of events $S$ must approach their probabilities simultaneously, so that a quantity chosen after looking at the data (the empirical risk minimizer, the empirical distribution function) is still close to its expectation. Glivenko's theorem on the empirical distribution function is the classical instance; empirical risk minimization rests on the same property for the class of loss sets of a model.

Vapnik and Chervonenkis, On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities, Theory Probab. Appl. 16 (1971), treat this question in two parts. The first gives a distribution-free sufficient condition through the growth function (Theorems 1–3). The second, which this mission formalizes, gives a condition that is necessary and sufficient for a fixed distribution: Theorem 4, the entropy criterion.

Timeline. 1933: Glivenko and Cantelli prove uniform convergence for the class of rays $\{x \le a\}$ on the line. 1968: Vapnik and Chervonenkis announce the results in Dokl. Akad. Nauk SSSR 181. 1971: the full paper appears, with the growth-function bound and the entropy criterion. Later work (Talagrand 1987; Dudley, Giné and Zinn 1991) recasts such criteria as the theory of Glivenko–Cantelli classes.

Setting

Let $X$ be a set carrying a probability measure $P$, and $S$ a collection of measurable subsets of $X$ (events). A sample of size $l$ is a sequence $x_1, \dots, x_l$ of independent draws from $P$; repetitions are allowed. For $A \in S$ the relative frequency $\nu_A^{(l)}$ is the fraction of sample terms lying in $A$, and $P_A = P(A)$. The maximal deviation is

$$\pi^{(l)}(x_1, \dots, x_l) = \sup_{A \in S} \bigl|\nu_A^{(l)} - P_A\bigr| .$$

The relative frequencies converge in probability to the probabilities uniformly over $S$ when $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \to 0$ as $l \to \infty$ for every $\varepsilon > 0$.

Each $A \in S$ induces in a sample the subsample of terms lying in $A$. The index $\Delta^S(x_1, \dots, x_l)$ is the number of different subsamples induced by the sets of $S$; it lies between $0$ and $2^l$. The entropy of $S$ in samples of size $l$ is

$$H^S(l) = \mathbf{E} \log_2 \Delta^S(x_1, \dots, x_l) .$$

For a sample of size $2l$, split into halves $x_1, \dots, x_l$ and $x_{l+1}, \dots, x_{2l}$ with relative frequencies $\nu'_A$ and $\nu''_A$, the semi-sample deviation is $\rho^{(l)} = \sup_{A \in S} |\nu'_A - \nu''_A|$. Finally $\Phi(n, r)$ is defined by the recurrence $\Phi(n, r) = \Phi(n, r-1) + \Phi(n-1, r-1)$, $\Phi(0, r) = \Phi(n, 0) = 1$.

Formalization targets

Goal: Theorem 4 (p. 275)

$$\Bigl(\forall \varepsilon > 0:\ \lim_{l\to\infty} \mathbf{P}\{\pi^{(l)} > \varepsilon\} = 0\Bigr) \iff \lim_{l \to \infty} \frac{H^S(l)}{l} = 0 .$$

Milestones

1. Entropy rate. (12) $\Delta^S(x_1, \dots, x_l) \le \Delta^S(x_1, \dots, x_k)\Delta^S(x_{k+1}, \dots, x_l)$; the subadditivity $H^S(l_1 + l_2) \le H^S(l_1) + H^S(l_2)$; Lemma 3, $H^S(l)/l \to c \in [0, 1]$; Lemma 4, $\mathbf{P}(|l^{-1}\log_2 \Delta^S - c| > \varepsilon) \to 0$.
2. Sufficiency. Lemma 2, $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \le 2\,\mathbf{P}\{\rho^{(l)} \ge \varepsilon/2\}$ for $l \ge 2/\varepsilon^2$; the per-sample permutation bound $2\Delta^S(x_1, \dots, x_{2l}) e^{-\varepsilon^2 l/8}$; and

$$\mathbf{P}\{\rho^{(l)} \ge \tfrac{\varepsilon}{2}\} \le 2\Bigl(\frac{2}{e}\Bigr)^{\varepsilon^2 l/8} + \mathbf{P}\Bigl\{\tfrac{1}{2l}\log_2 \Delta^S(x_1, \dots, x_{2l}) > \tfrac{\varepsilon^2}{16}\Bigr\} .$$

3. Necessity. Lemma 1 (Sauer–Shelah in sequence form); step 1°, $1 - \mathbf{P}(C') \ge (1 - \mathbf{P}(Q))^2$ with $C' = \{\rho^{(l)} > 2\varepsilon\}$; (26), $\mathbf{P}\{\Delta^S > \Phi([ql], l)\} \to 1$ when $0 < q < \frac14$ and $q\log_2(2e/q) < c$; and (29), $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \to 1$ when moreover $0 < \varepsilon < q/7$.

Significance

Theorem 4 characterizes uniform convergence for a given distribution exactly, with no gap between the necessary and the sufficient condition. It separates the cases the growth-function bound cannot: a class may have $m^S(l) = 2^l$ for every $l$ (all open subsets of $[0,1]$) and still satisfy $H^S(l)/l \to 0$ under a particular $P$, or fail it. The entropy $H^S(l)$ is the distribution-dependent quantity from which later work on Glivenko–Cantelli classes and on consistency of empirical risk minimization proceeds; the 1981 paper of the same authors extends the criterion to classes of functions. The quantitative form (29) states more than the negation of convergence: when the entropy rate is positive, the maximal deviation stays above a fixed $\varepsilon$ with probability tending to one.

The result has been proved since 1971; it has not been formalized. The platform holds Sauer–Shelah variants over sets of distinct points and PAC bounds with other constants, but no statement of the VC entropy or of Theorem 4. The mission produces machine-checked statements of the entropy criterion and of its supporting lemmas with the paper's own constants ($l \ge 2/\varepsilon^2$, $2e^{-\varepsilon^2 l/8}$, $\delta = \varepsilon^2/16$, $\varepsilon < q/7$).

Difficulty

The sufficiency half is a variant of the proof of the growth-function bound; its new ingredient is the concentration of $l^{-1} \log_2 \Delta^S$ (Lemma 4), which needs subadditivity and a law of large numbers over independent blocks of the sample rather than a single mean estimate. The hypergeometric tail estimate behind the permutation bound is omitted in the paper ("a simple but long computation").

Necessity is harder. The obvious attempt, bounding $\mathbf{P}\{\pi^{(l)} > \varepsilon\}$ from below by exhibiting a single bad event, fails: $S$ may be uncountable and no single $A$ deviates with non-vanishing probability. A positive entropy rate has to be converted into a combinatorial statement about typical samples ((26) combines Lemma 4 with an estimate of $\Phi([ql], l)$), and that statement back into a lower bound on a probability over the product measure; the constants $q < \frac14$ and $\varepsilon < q/7$ must be tracked through both conversions, and the conclusion $\lim \mathbf{P}\{\pi^{(l)} > \varepsilon\} = 1$ needs the unweakened inequality of step 1°.

Formalization scope

A sample of size $l$ is a function Fin l → X (positions $0, \dots, l-1$) and its law is the product measure Measure.pi (fun _ => P), with P a probability measure. A subsample is a set of positions, so the index counts distinct Finset (Fin l) of the form $\{i : x_i \in A\}$. The halves of x : Fin (l + l) → X are x ∘ Fin.castAdd l and x ∘ Fin.natAdd l. $P_A$ is P.real A; the suprema $\pi^{(l)}$ and $\rho^{(l)}$ are real suprema over the subtype of $S$ (values in $[0,1]$; $0$ for $S = \emptyset$). $H^S(l)$ is a Bochner integral of Real.logb 2 of the index, and $[ql]$ is ⌊q * l⌋₊. Probabilities are values in $[0, \infty]$, except in the inequalities between probabilities (step 1°, the sufficiency estimate), which use Measure.real.

Measurability. The paper assumes, and the statements carry as hypotheses, that the events of $S$ are measurable (p. 264), that $\pi^{(l)}$ is a random variable (p. 265), that $\rho^{(l)}$ is measurable (p. 268), and that the index is measurable in the sample (p. 273). Each statement carries the ones its proof uses. Without them the Bochner integral defining $H^S(l)$ can be the junk value $0$ and the equivalence can fail; replacing them by "$S$ countable" would weaken the theorem. The goal is not trivialized by degenerate cases: the equivalence is not vacuous for any class, and $S = \emptyset$ gives the true instance $H^S = 0$, $\pi^{(l)} = 0$.

Corrections of the printed text. Lemma 2 is printed for $l > 2/\varepsilon^2$; its proof gives $l \ge 2/\varepsilon^2$, which is stated. On p. 275 Lemma 2 is recalled as "$2\mathbf{P}(C) \ge \frac12 P(Q)$", meaning $\mathbf{P}(C) \ge \frac12\mathbf{P}(Q)$. On p. 276 the first display carries a stray upper limit "4" on the integral, and the region of integration is printed $\{\log_2 \Delta^S \le 2\delta\}$ where $\{\log_2\Delta^S \le 2\delta l\}$ is meant. The event $C'$ is defined with "$> 2\varepsilon$" (p. 276) but integrated in step 3° as $\theta(\cdot - 2\varepsilon)$, which counts "$\ge 2\varepsilon$"; the strict form is stated, and the estimate of step 3° is itself strict. Step 1° is stated unweakened. Milestone texts are verbatim.

Contributions welcome: a reusable development of the index and its submultiplicativity, the hypergeometric tail bound for sampling without replacement, a block law of large numbers for subadditive functionals of i.i.d. samples, and the permutation-invariance argument for product measures on Fin (l + l) → X.

Selected references

• V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and Its Applications 16(2) (1971), 264–280. https://doi.org/10.1137/1116025
• V. N. Vapnik and A. Ya. Chervonenkis, Necessary and sufficient conditions for the uniform convergence of means to their expectations, Theory of Probability and Its Applications 26(3) (1981), 532–553. https://doi.org/10.1137/1126059
• M. Talagrand, The Glivenko–Cantelli problem, Annals of Probability 15(3) (1987), 837–870. https://doi.org/10.1214/aop/1176992069
• R. M. Dudley, E. Giné and J. Zinn, Uniform and universal Glivenko–Cantelli classes, Journal of Theoretical Probability 4(3) (1991), 485–510. https://doi.org/10.1007/BF01210321

Motivation

Portfolio selection and other decisions under risk are routinely solved as mean–risk models: maximize the expected outcome minus a multiple of a risk measure over the feasible set. Such a model is computationally convenient, but it is only defensible if its answers agree with the preferences of risk-averse decision makers. The standard formal expression of those preferences is second-degree stochastic dominance (SSD): a random outcome $X$ dominates $Y$ when every nondecreasing concave utility prefers $X$. A mean–risk model whose optimal solution may be SSD-dominated by another feasible decision recommends something every risk-averse investor would reject; the classical mean–variance model has exactly this defect.

Ogryczak and Ruszczyński (SIAM J. Optim. 13 (2002) 60–78) characterize SSD through the absolute Lorenz curve (the second quantile function) and use this dual view to study risk measures defined from quantiles: the vertical diameter of the dual dispersion space, the tail Gini measure and the Gini mean difference. Their §5 shows that the mean–Gini model, with trade-off coefficient at most one, has optimal solutions and that all of them are SSD-efficient. This mission formalizes that result together with the lemmas it rests on. A companion mission of this series formalizes the dual characterization of SSD itself (the paper's Theorems 3.1–3.2).

Timeline. Yitzhaki (1982) showed the mean–Gini necessary condition for SSD for bounded distributions; Ogryczak and Ruszczyński proved SSD consistency of mean-semideviation models (Eur. J. Oper. Res. 116 (1999)) and, in the present paper, extended the analysis to quantile-based and Gini-type risk measures for general integrable outcomes, with existence and efficiency of optimal solutions over sets in $L_q$.

Setting

Let $(\Omega,\mathcal B,P)$ be a probability space and $X:\Omega\to\mathbb R$ an integrable random variable with mean $\mu_X=E X$ and distribution function $F_X(\eta)=P\{X\le\eta\}$. The second performance function is

$$F_X^{(2)}(\eta)=\int_{-\infty}^{\eta}F_X(\xi)\,d\xi ,$$

and $X\succeq_{SSD}Y$ means $F_X^{(2)}(\eta)\le F_Y^{(2)}(\eta)$ for all $\eta\in\mathbb R$. Strict dominance is $X\succ_{SSD}Y$ iff $X\succeq_{SSD}Y$ and not $Y\succeq_{SSD}X$. For a set $Q$ of random variables, $X\in Q$ is SSD-efficient in $Q$ if no $Y\in Q$ satisfies $Y\succ_{SSD}X$.

The left quantile function is $F_X^{(-1)}(p)=\inf\{\eta:F_X(\eta)\ge p\}$ for $0<p\le1$; a number $q$ is a $p$-quantile if $P\{X<q\}\le p\le P\{X\le q\}$. The absolute Lorenz curve is $F_X^{(-2)}(p)=\int_0^pF_X^{(-1)}(\alpha)\,d\alpha$ on $[0,1]$. From it the paper defines

• the vertical diameter $h_X(p)=\mu_Xp-F_X^{(-2)}(p)$, $p\in[0,1]$ (eq. (3.6));
• the Gini mean difference $\Gamma_X=2\int_0^1(\mu_Xp-F_X^{(-2)}(p))\,dp$ (eq. (3.8));
• the tail Gini measure $G_X(p)=\frac{2}{p^2}\int_0^p(\mu_X\alpha-F_X^{(-2)}(\alpha))\,d\alpha$, $p\in(0,1]$ (eq. (4.8)), so that $\Gamma_X=G_X(1)$.

The optimization problem is

$$\max_{X\in Q}\ (\mu_X-\lambda r_X),\tag{5.1}$$

with $\lambda>0$, $r_X$ one of these dual risk measures, and $Q$ a convex, closed, bounded subset of $L_q(\Omega,P)$ for some $q>1$.

Formalization targets

Goal: Theorem 5.3

For $1<q<\infty$, a nonempty convex bounded closed $Q\subseteq L_q$, $r_X=\Gamma_X$ and every $\lambda\in(0,1]$:

$$\operatorname*{arg\,max}_{X\in Q}(\mu_X-\lambda\Gamma_X)\neq\emptyset\quad\text{and every } X\in\operatorname*{arg\,max}_{X\in Q}(\mu_X-\lambda\Gamma_X)\text{ is SSD-efficient in }Q.$$

Milestones

1. Lemma 3.4: for $p\in(0,1)$, $h_X(p)=\min_{\xi\in\mathbb R}E\{\max(p(X-\xi),(1-p)(\xi-X))\}$, attained at any $p$-quantile.
2. Lemma 5.1: $X\mapsto h_X(p)$ is convex and positively homogeneous on $L_1$ for $p\in[0,1]$.
3. Lemma 5.2: $X\mapsto G_X(p)$ is convex and positively homogeneous on $L_1$ for $p\in(0,1]$.
4. (4.1): $X\succeq_{SSD}Y\Rightarrow\mu_X\ge\mu_Y$.
5. Proposition 4.5: $X\succeq_{SSD}Y\Rightarrow\mu_X-\Gamma_X\ge\mu_Y-\Gamma_Y$ and $X\succ_{SSD}Y\Rightarrow\mu_X-\Gamma_X>\mu_Y-\Gamma_Y$.

Companion: Theorem 5.4

For $r_X=h_X(p)/p$ with $p\in(0,1)$ and $\lambda\in(0,1]$, the optimal set $Q^*$ is nonempty and each $X\in Q^*$ has an SSD-efficient $X^*\in Q^*$ with $\mu_{X^*}=\mu_X$ and $h_{X^*}(p)=h_X(p)$.

Significance

Theorem 5.3 certifies the mean–Gini model as a safe decision rule: whatever trade-off $\lambda\in(0,1]$ is chosen, the model returns a decision that no feasible alternative dominates for all risk-averse utilities, and such a decision exists under assumptions natural for portfolio sets in $L_q$. Theorem 5.4 gives the weaker but still usable guarantee for the tail-value-at-risk type measure $h_X(p)/p$, for which non-efficient optima can occur. Lemma 3.4 is the bridge to computation: it turns $h_X(p)$ into an expected piecewise-linear loss minimized over a scalar, which is how these models become linear programs over scenarios (§6 of the paper).

On the formalization side, the results are proved in the paper but, as far as a search of the platform shows, not machine-checked anywhere. A complete development produces reusable infrastructure: quantile functions and their integrals for integrable random variables, convexity of law-invariant functionals on $L_1$, the Gini mean difference, and an existence argument for concave maximization over weakly compact subsets of $L_q$.

Difficulty

The existence half needs weak compactness of $Q$ in the reflexive space $L_q$ and weak upper semicontinuity of $\mu_X-\lambda\Gamma_X$. The functional is defined through quantiles, which are not linear in $X$, so neither its concavity nor its continuity is visible from the definition. Closedness of $Q$ in the norm topology must be upgraded to weak closedness, which uses convexity. The efficiency half needs the strict inequality (4.7): a strict SSD relation must produce a strict gap in the integrated absolute Lorenz curves, and the pointwise inequality of $F^{(2)}$ alone does not give strictness in $\Gamma$. The obvious attempt to argue efficiency from (4.6) alone fails: it yields only a weak inequality, which is compatible with an optimum being strictly dominated.

Formalization scope

• One probability space $(\Omega,P)$ with IsProbabilityMeasure P; random variables are functions Ω → ℝ, and all random variables compared by $\succeq_{SSD}$ live on it.
• $F_X^{(2)}$ is the Bochner integral of P.real {X ≤ ξ} over $(-\infty,\eta]$; $\mu_X$ is ∫ X ∂P. Every statement about general random variables assumes Integrable X P (the paper's standing $E|X|<\infty$).
• $F_X^{(-1)}$ uses the real sInf; its junk value at $p=1$ does not enter any integral and is never used pointwise. $F_X^{(-2)}$ is used only on $[0,1]$, so it is real-valued here; the extended-real version with $+\infty$ off $[0,1]$ belongs to the companion mission.
• $\Gamma_X$ is defined by the area formula (3.8), not by the double-integral formula that the paper cites; $h_X$ is defined by (3.6), not by the minimum (3.7), so Lemma 3.4 is a genuine statement.
• $L_q$ is Mathlib's Lp ℝ q P with 1 < q and q ≠ ∞ (the paper's $q$ is a real number $>1$); the functionals are applied to the function of an $L_q$ element, and SSD-efficiency in $Q$ refers to the image of $Q$ in functions. Positive homogeneity is stated for the $L_1$ element $c\cdot X$.
• Added hypothesis: $Q$ is nonempty. The paper does not write it, and without it the optimal set is empty.
• Optimal solutions are maximizers in $Q$, not a supremum value. The trade-off coefficient is lam because λ is a Lean keyword; the range $\lambda\in(0,1]$ is kept exactly.
• A trivializing formalization is ruled out: the weak relation $\succeq_{SSD}$ must not replace the strict relation in SSD-efficiency (every $X$ weakly dominates itself), and $\Gamma$ must not be a hand-chosen closed form.

Needed infrastructure: quantile functions and the identity $\int_0^1F_X^{(-1)}=\mu_X$; the minimum representation of Lemma 3.4; convexity of law-invariant functionals on Lp; weak compactness of bounded closed convex sets in reflexive Lp. Contributions of general lemmas about quantiles and Lorenz curves are welcome and reusable beyond this mission.

Selected references

• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean-risk models, SIAM J. Optim. 13(1) (2002) 60–78. https://doi.org/10.1137/S1052623400375075
• W. Ogryczak, A. Ruszczyński, From stochastic dominance to mean-risk models: semideviations as risk measures, Eur. J. Oper. Res. 116 (1999) 33–50. https://doi.org/10.1016/S0377-2217(98)00167-2
• S. Yitzhaki, Stochastic dominance, mean variance, and Gini's mean difference, Amer. Econ. Rev. 72 (1982) 178–185. https://www.jstor.org/stable/1808584

Motivation

A decision maker who chooses a portfolio $x\in\mathbb R^n$ of risky assets with random return vector $R$ receives the scalar return $x'R$ and evaluates it by an expected utility $E[u(x'R)]$. In practice the law of $R$ is not known; what can be estimated with some confidence are its mean $\mu$ and covariance $\Sigma$. The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:

$$U(x)=\inf\{E[u(x'R)] : R \text{ has mean } \mu \text{ and covariance } \Sigma\}.$$

Ioana Popescu (Operations Research 55(1), 2007) showed that $U(x)$ depends on $x$ only through $\mu_x=x'\mu$ and $\sigma_x^2=x'\Sigma x$, and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility $1-e^{-ay}$ and all concave quadratics. The reduction to $(\mu_x,\sigma_x)$ is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.

The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of $E[u(r)]$ over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.

Setting

Fix $m\in\mathbb R$ and $s\ge 0$. The mean-variance class $\mathbb M_{(m,s^2)}$ is the set of Borel probability measures $\nu$ on $\mathbb R$ with $\int r^2\,d\nu<\infty$, $\int r\,d\nu=m$ and $\int (r-m)^2\,d\nu=s^2$ (Lean: MeanVarClass m (s ^ 2)). For a utility $u:\mathbb R\to\mathbb R$ the robust objective is

$$U(m,s)=\inf\Big\{\int u\,d\nu : \nu\in\mathbb M_{(m,s^2)}\Big\},$$

with $\min$ read, as in the paper, "in the wide sense of $\inf$", so the value $-\infty$ is allowed. The paper's $U(x)$ is $U(\mu_x,\sigma_x)$.

For $p\in(0,1)$ the two-point law $r_p$ puts mass $p$ on $b=m+\sqrt{(1-p)/p}\,s$ and mass $1-p$ on $a=m-\sqrt{p/(1-p)}\,s$; these are exactly the two-point laws of $\mathbb M_{(m,s^2)}$. Its expected utility is the two-point objective (8),

$$U(p)=p\,u(b)+(1-p)\,u(a)\qquad(\texttt{twoPointValue u m s p}).$$

A supporting quadratic of $u$ is $q(y)=Ay^2+By+C$ with $q\le u$ on $\mathbb R$; the set of their coefficients is $\mathcal Q$. Since every $r\sim(m,s^2)$ has $E[q(r)]=A(m^2+s^2)+Bm+C$, each element of $\mathcal Q$ gives a lower bound on $U(m,s)$ (Proposition 3). The function $u$ has the one-point support property with respect to $(m,s^2)$ (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches $u$ at $m$ and $E[u(r_p)]\to E[q(r_p)]$ as $p\to0^+$ or as $p\to1^-$; it has one-point support (OnePointSupport u) if this holds for every $m$ and every $s\ge0$.

Formalization targets

Goal: Proposition 7

Let $u$ be concave and twice differentiable with monotone $u''$.

(a) If $u'$ is convex, then

$$U(m,s)=u(m)+\lim_{y\to-\infty}u''(y)\,\frac{s^2}{2}\qquad\text{for all } m,\ s.$$

(b) If $u'$ is concave, the same holds with $\lim_{y\to+\infty}u''(y)$.

In each part the limit $L$ of $u''$ exists in $[-\infty,0]$. When $L$ is finite the goal asserts that $u$ is integrable under every law of every class, that $u(m)+Ls^2/2$ is the greatest lower bound of the expected utilities, and that $u$ has one-point support. When $L=-\infty$ and $s>0$ it asserts $U(m,s)=-\infty$.

Milestones

1. Display (9): $\partial U/\partial p=u(b)-u(a)-(b-a)\,\frac{u'(b)+u'(a)}{2}$.
2. For convex $u'$ and $s>0$, $U(p)$ is nonincreasing on $(0,1)$.
3. Appendix (4): $\lim_{p\to1^-}U(p)=u(m)+\frac{s^2}{2}\lim_{y\to-\infty}u''(y)$, including the value $-\infty$.
4. Proposition 3: every $E[u(r)]$ dominates every $A(m^2+s^2)+Bm+C$ with $(A,B,C)\in\mathcal Q$.
5. The function $d(y)=\frac{u(y)-u(m)}{(y-m)^2}-\frac{u'(m)}{y-m}$ is nondecreasing on $\{y \neq m\}$ when $u'$ is convex.
6. Appendix (5): $q(y)=\tfrac12u''(-\infty)(y-m)^2+u'(m)(y-m)+u(m)$ supports $u$, and $\inf_{y\ne m}d(y)=\lim_{y\to-\infty}d(y)=\tfrac12u''(-\infty)$.

An additional item states Proposition 8: a monotone convex $u$ has one-point support and $U(m,s)=u(m)$.

Significance

Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ($u'$ convex) is penalized by $\tfrac12\lim_{y\to-\infty}u''(y)$ per unit of variance, an imprudent one by the limit at $+\infty$. With Proposition 1, the robust portfolio problem becomes $\max_x\ u(\mu_x)+\tfrac12 L\,\sigma_x^2$, a concave mean-variance program. For exponential utility the weight is $-\infty$ (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the $-\infty$ case of the theorem.

The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step "$\lim_{y\to-\infty}u'(y)=\infty$" fails for affine $u$, where the theorem nevertheless holds, and the claim that $u$ "has one-point support" fails when $\lim u''=-\infty$ (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.

Difficulty

The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over $p$, gives only an upper bound (display (7)), and here the minimizing $p$ runs off to the boundary: the extremal law puts vanishing mass on a point escaping to $-\infty$. Identifying the limiting value requires controlling $u(m-sq)/(1+q^2)$ as $q\to\infty$, a second-order asymptotic statement about $u$ at $-\infty$. The matching lower bound requires a supporting quadratic whose curvature is exactly $\tfrac12\lim u''$; showing that it lies below $u$ everywhere, not only near $m$, is a global statement that uses the convexity of $u'$ on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.

Formalization scope

Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean $m$ and variance $s^2$ with $s\ge0$. The statements are univariate: $U(x)$ of the paper is the univariate objective at $(\mu_x,\sigma_x)$ by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of $u$ and of $u'$. Limits of $u''$ are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in $p$ are one-sided inside $(0,1)$. Expectations under two-point laws are written by the explicit formula (8).

"Min" is never a real ⨅, which Lean evaluates to $0$ on sets unbounded below. The finite case uses IsGLB together with integrability of $u$ under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value $\ge$ every value". Proposition 3 assumes $u$ integrable under the law; Proposition 8 takes the infimum over laws under which $u$ is integrable, which for convex $u$ loses nothing.

One correction to the printed statement: Proposition 7 opens with "then $u$ has one-point support", which is false when $\lim u''=-\infty$, since no quadratic lies below $1-e^{-ay}$ on $\mathbb R$. The formalization asserts one-point support only in the finite-limit case and the value $-\infty$ in the other. A formalization that took $\min$ as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.

A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at $-\infty$, the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.

Selected references

• I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30, 1991.
• S. Karlin, W. J. Studden, Tchebycheff Systems: With Applications in Analysis and Statistics, Interscience, 1966.