The OR Formalization Drive

Motivation

Newton's method is the standard second-order algorithm for unconstrained minimization, but without safeguards it has no global guarantee: far from a minimizer the Newton step can increase the objective, and at a point where the Hessian is indefinite the step can head for a saddle point or a maximum. The usual repairs (line search, trust regions, Levenberg–Marquardt damping) come with convergence proofs, but for nonconvex objectives those proofs typically give no rate at all, or only the rate of the gradient method.

Nesterov and Polyak (Math. Program. 108 (2006) 177–205) proposed to regularize the second-order Taylor model of the objective with a cubic term and to take as the next iterate a global minimizer of the regularized model. They showed that the resulting method has a global worst-case rate of convergence to points satisfying the second-order necessary conditions, for every objective with a Lipschitz continuous Hessian and without any convexity. That rate, $O(k^{-2/3})$ for the gradient norm, is better than the $O(k^{-1/2})$ of the gradient method. It became the reference point for the complexity theory of nonconvex second-order optimization: adaptive variants (Cartis, Gould and Toint, Math. Program. 127 (2011) 245–295) and lower bounds showing that $O(\epsilon^{-3/2})$ iterations are optimal among second-order methods (Carmon, Duchi, Hinder and Sidford, Math. Program. 184 (2020) 71–120) are stated against it.

This mission formalizes the general convergence result of that paper, Theorem 1 of Section 3, together with the properties of the cubic step from Section 2 on which it rests.

Setting

Let $F \subseteq \mathbb{R}^n$ be a closed convex set with nonempty interior, and let $f$ be twice differentiable on $F$ with gradient $f'(x)$ and Hessian $f''(x)$. A starting point $x_0 \in \operatorname{int} F$ is fixed, and $F$ is assumed to contain the level set $\mathcal{L}(f(x_0)) = \{x \in \mathbb{R}^n : f(x) \le f(x_0)\}$ in its interior. Assumption 1: the Hessian is Lipschitz continuous on $F$ in the spectral norm, $\|f''(x) - f''(y)\| \le L\|x - y\|$ for all $x, y \in F$, with $L > 0$.

For a parameter $M > 0$ the cubic model of $f$ at $x$ is

The cubic-regularized Newton step $T_M(x)$ is any global minimizer of $m_{M,x}$ over $\mathbb{R}^n$; it exists because the model is continuous and coercive. Write $r_M(x) = \|x - T_M(x)\|$ and $\bar f_M(x) = f(x) + \min_y m_{M,x}(y)$.

The cubic regularization of Newton method (3.3) fixes $L_0 \in (0, L]$, starts at $x_0$ and, for $k \ge 0$, chooses $M_k \in [L_0, 2L]$ such that $f(T_{M_k}(x_k)) \le \bar f_{M_k}(x_k)$, then sets $x_{k+1} = T_{M_k}(x_k)$. The choice $M_k = L$ always passes the test.

Write $\lambda_n(A)$ for the smallest eigenvalue of a symmetric matrix $A$. The measure of local optimality is

It is nonnegative and vanishes exactly when $f'(x) = 0$ and $f''(x) \succeq 0$.

Formalization targets

Goal: Theorem 1, inequality (3.4)

If $f(x) \ge f^*$ for all $x \in F$, then every run of method (3.3) satisfies, for every $k \ge 1$,

The constant $8/3$ and the exponent $1/3$ are the paper's; the statement holds for every admissible choice of the parameters $M_k$ and of the global minimizers $x_{k+1}$.

Milestones, in attack order

1. Lemma 1 (2.2): $\|f'(y) - f'(x) - f''(x)(y - x)\| \le \tfrac12 L\|y - x\|^2$ on $F$.
2. Eq. (2.5): $f'(x) + f''(x)(T - x) + \tfrac12 M\|T - x\|(T - x) = 0$ for $T = T_M(x)$.
3. Proposition 1 (2.7): $f''(x) + \tfrac12 M r_M(x) I \succeq 0$.
4. Lemma 2 (2.8): $\langle f'(x), x - T_M(x)\rangle \ge 0$ when $f(x) \le f(x_0)$.
5. Lemma 4 (2.11): $f(x) - \bar f_M(x) \ge \tfrac{M}{12} r_M(x)^3$.
6. Lemma 4 (2.12): for $M \ge L$, $T_M(x) \in F$ and $f(T_M(x)) \le \bar f_M(x)$.
7. Lemma 3 (2.9): $\|f'(T_M(x))\| \le \tfrac12(L + M) r_M(x)^2$ when $T_M(x) \in F$.
8. Lemma 5: $\mu_M(T_M(x)) \le r_M(x)$.
9. Theorem 1, first claim: $\sum_{i \ge 0} r_{M_i}(x_i)^3 \le \tfrac{12}{L_0}(f(x_0) - f^*)$.
10. Theorem 1, second claim: $\lim_{i\to\infty} \mu_L(x_i) = 0$.

Significance

Inequality (3.4) is a global, dimension-free complexity bound for reaching approximate second-order stationarity. It controls both the gradient norm, $\min_{1\le i\le k}\|f'(x_i)\| = O(k^{-2/3})$, and the most negative curvature, $\max\{0, -\lambda_n(f''(x_i))\} = O(k^{-1/3})$, along the best iterate, from a single scalar potential $f(x_0) - f^*$. The second claim of Theorem 1 gives the asymptotic counterpart: every limit point satisfies the second-order necessary conditions. Section 4 of the paper derives its faster rates for star-convex and gradient-dominated functions from the same Section 2 lemmas.

The result is proved on paper and widely cited; to our knowledge no machine-checked proof of it or of the Section 2 lemmas exists. A formalization adds a checked statement of the method with its exact constants, and reusable facts about global minimizers of cubic models (Proposition 1 in particular) that the companion missions on star-convex, gradient-dominated and locally quadratic convergence also rely on.

Difficulty

Most steps are short inequalities, but two are not. Proposition 1 is a statement about a global minimizer of a nonconvex function: the first- and second-order conditions of a local minimizer give only $f''(x) + \tfrac12 M r I + \tfrac{M}{2r}(T - x)(T - x)^\top \succeq 0$, which is weaker. The natural first attempt, "take the second-order optimality condition of the model at $T$", therefore fails. The paper proves it in Section 5.1 through a one-dimensional dual characterization of the minimizer.

The second is Lemma 2's second claim, used for (2.12): showing that $T_M(x)$ stays in $F$ requires a boundary argument along the segment from $x$ to $T_M(x)$, since the Taylor bounds are only available inside $F$. The remaining work is calculus in $\mathbb{R}^n$: the integral form of Taylor's theorem for the gradient under a Lipschitz Hessian, and eigenvalue perturbation for the second entry of $\mu$.

Formalization scope

The space is EuclideanSpace ℝ (Fin n) for arbitrary n : ℕ. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every x ∈ F. At boundary points of $F$ this asks for two-sided derivatives, a mild strengthening of "twice differentiable on $F$". The Lipschitz condition uses the operator norm, which is the spectral norm. $T_M(x)$ is represented by the predicate IsCubicStep (global minimizer of cubicModel), and every lemma is stated for every such minimizer. The run predicate IsCubicNewtonRun is 0-based. It writes $\bar f_{M_k}(x_k)$ as $f(x_k)$ plus the model value at $x_{k+1}$, which is the minimum because $x_{k+1}$ attains it. $\lambda_n$ is lamMin, the Rayleigh-quotient infimum over the unit sphere, which equals the smallest eigenvalue for the (symmetric) Hessian. The lower bound $f^*$ is required on $F$ only. The minimum over $1 \le i \le k$ is written as the existence of an index attaining the bound.

A stationary point of the cubic model is not an admissible step, and the run must keep the test $M_k \in [L_0, 2L]$ and the acceptance test. Replacing the step by any point with $f(x_{k+1}) \le f(x_k)$ makes the goal false, and dropping the square root in $\mu_M$ makes Lemma 5 false. The statements rule out all three. Lemma 5 carries the hypothesis $T_M(x) \in F$, which its printed proof uses and which holds at every iterate.

A complete development needs the Taylor bounds (2.2)–(2.3) for vector-valued derivatives on convex sets, and first- and second-order optimality for the cubic model. It also needs a proof of Proposition 1 (Section 5.1 or any other correct argument) and eigenvalue perturbation via Rayleigh quotients. The cubic-model lemmas and Proposition 1 are reusable across the whole series. Proofs of any milestone, alternative proofs of Proposition 1, and general Mathlib-level lemmas about Rayleigh quotients are welcome.

Selected references

• Yu. Nesterov and B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming, Ser. A 108 (2006) 177–205. https://doi.org/10.1007/s10107-006-0706-8
• C. Cartis, N. I. M. Gould and Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming 127 (2011) 245–295. https://doi.org/10.1007/s10107-009-0286-5
• Y. Carmon, J. C. Duchi, O. Hinder and A. Sidford, Lower bounds for finding stationary points I, Mathematical Programming 184 (2020) 71–120. https://doi.org/10.1007/s10107-019-01406-y
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Quasi-Newton methods minimize a smooth function $f$ on $\mathbb{R}^n$ by moving along $d_k = -H_k g_k$, where $g_k$ is the gradient and $H_k$ is an approximation of the inverse Hessian built from observed gradient differences. The BFGS update is the most widely used way of building $H_k$, but it stores a dense $n \times n$ matrix, which is prohibitive for large $n$.

Nocedal's 1980 paper (Math. Comp. 35, 773–782) proposed keeping only the last $m$ correction pairs and rebuilding the matrix from a simple initial matrix $H_0$ at every step. The resulting method, called SQN in the paper, is now known as L-BFGS, and it is the default large-scale unconstrained optimizer in many numerical libraries and in machine learning. The paper's main theoretical claim is that this truncation does not destroy the finite termination of BFGS on quadratics.

Timeline:

• 1970: Broyden, Fletcher, Goldfarb and Shanno introduce the BFGS update (references [1] and [5] of the paper).
• 1977: Nazareth relates BFGS to conjugate gradients (Argonne Tech. Memo 282, reference [7]); his form of preconditioned conjugate gradients is the one the paper uses.
• 1977–1978: Shanno studies the memoryless BFGS update, the case $m = 1$ (reference [11]; journal version Math. Oper. Res. 3, 1978).
• 1980: Nocedal defines the special BFGS matrices and the SQN method and states that on quadratics with exact line searches SQN is identical to preconditioned conjugate gradients, hence has quadratic termination.
• 1989: Liu and Nocedal (Math. Programming 45) study the method, now called L-BFGS, for large-scale problems.
• 1998: Kolda, O'Leary and Nazareth (SIAM J. Optim. 8) treat limited-memory and update-skipping BFGS variants with exact line searches on quadratics.

Setting

Let $A$ be a symmetric positive definite $n \times n$ matrix and $b \in \mathbb{R}^n$, and let $f(x) = \tfrac12 x^T A x + b^T x$, a strictly convex quadratic with gradient $g(x) = Ax + b$ and unique minimizer $x^\ast = -A^{-1} b$.

Exact line search. Along a direction $d \neq 0$ from $x$, the step $\alpha = -g(x)^T d / d^T A d$ minimizes $f(x + \alpha d)$.

BFGS update. For a pair $(s, y)$ with $\rho = 1/y^T s$ and $v = I - \rho y s^T$, the BFGS update of $H$ is

Special BFGS matrices. Fix $H_0$ symmetric positive definite and a number $m \ge 1$ of stored corrections. Given pairs $(s_j, y_j)$, the special matrix $H_K$ is $H_0$ updated by the pairs $j = K - \min(K, m), \dots, K-1$, oldest first (the paper's (4)–(5)). Only the $m$ most recent pairs enter, and the matrix is rebuilt from $H_0$.

SQN. Starting from $x_0$, with $g_i = g(x_i)$:

with $\alpha_i$ the exact step and $H_{i+1}$ the special matrix built from the last $\min(i+1, m)$ pairs.

PCG with fixed preconditioner $H_0$. $d_0 = -H_0 g_0$, $x_{i+1} = x_i + \alpha_i d_i$, $d_{i+1} = -H_0 g_{i+1} + \beta_{i+1} d_i$ with $\beta_{i+1} = y_i^T H_0 g_{i+1} / y_i^T d_i$.

Formalization targets

Goal: quadratic termination of SQN

For every $n$, every symmetric positive definite $A$ and $H_0$, every $b$, $x_0$ and every $m \ge 1$,

where $x_k$ are the SQN iterates. The statement fixes no constant beyond the dimension bound $n$.

Milestones

1. Property (a): the special matrices are positive definite whenever $y_i^T s_i > 0$ for all $i$.
2. Eq. (7): along conjugate steps, $v_i y_i = 0$ and $v_i y_j = y_j$ for $i > j$.
3. Eq. (6): along conjugate steps, $H_k y_j = s_j$ for the $m$ most recent $j$ (when $k > m$).
4. Eq. (10): the special matrix equals $m$ sum-form BFGS corrections applied to $H_0$.
5. Eq. (15): the PCG directions satisfy $d_i^T y_j = 0$ for $i \neq j$.
6. Eq. (16): $g_i^T H_0 g_j = 0$ for $i \neq j$ and $g_i^T d_j = 0$ for $j < i$.
7. The PCG with fixed preconditioner $H_0$ reaches the minimizer in at most $n$ steps.
8. SQN and this PCG produce identical iterates and directions at every step.

Significance

The result shows that storing only $m$ correction pairs costs nothing on quadratics: for any $m \ge 1$, SQN terminates in at most $n$ steps, like full BFGS and conjugate gradients. It explains why L-BFGS with small $m$ is competitive, and it is the model case for later analyses of limited-memory methods (their linear convergence on uniformly convex functions, and their relation to Krylov methods). Property (b) is the reason one expects efficiency to grow with $m$: the matrix satisfies the secant equation on the $m$ most recent directions.

The claims are classical and generally accepted, but the paper argues them in a few lines ("it is straightforward to show"), deferring the PCG facts (15)–(16) to a reference. No machine-checked proof of the termination of BFGS, L-BFGS or preconditioned conjugate gradients is known to this mission. A formalization would provide a verified model of L-BFGS on quadratics and a reusable development of conjugate-direction methods with a preconditioner.

Difficulty

The obvious route, "SQN is BFGS and BFGS terminates", fails: SQN discards old corrections, so the classical BFGS argument (hereditary secant conditions on all past directions) does not apply once more than $m$ steps have been taken. The paper asserts the identity of SQN with preconditioned conjugate gradients in one sentence ("using a similar argument as for the SCG"), and the PCG relations it relies on are quoted from a technical report. The other difficulty is bookkeeping: the window of stored pairs shifts, the matrix is a nested product, and the runs must remain meaningful after the minimizer is reached.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, $x^T y$ is dotProduct, and $s y^T$ is Matrix.vecMulVec. Symmetric positive definiteness is Matrix.PosDef. Indices are 0-based, as in the paper. The exact line search is the closed-form step $-g^T d / d^T A d$. The iterations have no stopping rule: once the gradient vanishes the direction and step are zero and the iterate stays at the minimizer (Lean's $0/0 = 0$). Past that point the zero pair stored by SQN leaves the BFGS step unchanged. The hypotheses are exactly the paper's: $A \succ 0$, $H_0 \succ 0$, $m \ge 1$ and exact line searches. $H_0$ need not be diagonal.

Two misprints are corrected and flagged in the items: the denominator of $\beta$ in (13) is $y_{i-1}^T d_{i-1}$ (as in (12) and p. 778), and the second relation of (16) is stated for $j < i$ (as used on p. 778), since it fails for $i < j$.

Ruled out: SQN is defined through its own matrices (4)–(5), rebuilt from $H_0$ and the last $m$ pairs. It is not defined through the PCG recurrence, not by one BFGS update of the previous matrix, and not with a stop rule that returns $-A^{-1}b$. The standing assumption $y_k^T s_k > 0$ is not a hypothesis of any statement about a run (it fails after termination and would make the goal vacuous). With $m = 0$ SQN is steepest descent and the goal is false, so $m \ge 1$ is required.

Needed infrastructure: algebra of rank-one updates and of Matrix.PosDef under congruence, conjugate-direction lemmas for quadratics, and the fact that $n+1$ mutually $H_0$-orthogonal vectors in $\mathbb{R}^n$ include a zero vector. The PCG results (milestones 5–7) are reusable beyond this mission. Proofs of any milestone, or of the goal directly, are welcome.

Selected references

• J. Nocedal, Updating Quasi-Newton Matrices with Limited Storage, Mathematics of Computation 35(151), 1980, 773–782. https://doi.org/10.1090/s0025-5718-1980-0572855-7
• D. F. Shanno, Conjugate gradient methods with inexact searches, Mathematics of Operations Research 3(3), 1978, 244–256. https://doi.org/10.1287/moor.3.3.244
• L. Nazareth, A Relationship Between the BFGS and Conjugate Gradient Algorithms, ANL-AMD Tech. Memo 282 (rev.), Argonne National Laboratory, 1977 (reference [7] of Nocedal 1980; no online copy located).
• T. G. Kolda, D. P. O'Leary, L. Nazareth, BFGS with update skipping and varying memory, SIAM Journal on Optimization 8(4), 1998, 1060–1083. https://doi.org/10.1137/S1052623496306450
• D. C. Liu, J. Nocedal, On the limited memory BFGS method for large scale optimization, Mathematical Programming 45, 1989, 503–528. https://doi.org/10.1007/BF01589116

Motivation

In robust stochastic optimization a decision maker chooses a decision $x$ whose outcome depends on a random vector $\mathbf R$, but knows only the first two moments of $\mathbf R$: its mean vector $\mu$ and its covariance matrix $\Sigma$. The decision is evaluated by its worst-case expected utility over every distribution consistent with those moments. This model is standard in portfolio selection, where estimated means and covariances are the usual inputs, and in pricing and inventory problems with mean-variance information. It goes back to Scarf's min-max newsvendor (1958) and the Chebyshev-type moment bounds of Bertsimas and Popescu (2005).

For a linear outcome $x'\mathbf R$, such as the return of a portfolio with weights $x$, the robust objective is

an optimization over an infinite-dimensional set of $n$-variate distributions. Popescu (2007) showed that this problem depends on $\mu$ and $\Sigma$ only through the scalar mean $\mu_x = x'\mu$ and variance $\sigma_x^2 = x'\Sigma x$. The multivariate robust problem then reduces to a univariate moment problem, and for many utilities to a parametric quadratic program. The reduction rests on one structural fact, the general projection property, which this mission formalizes.

Setting

Fix a dimension $n$. A law on $\mathbb R^n$ is a Borel probability measure on $\mathbb R^n$. For a vector $\mu \in \mathbb R^n$ and a real $n\times n$ matrix $\Sigma$, the mean-covariance class $\mathbb M^n_{(\mu,\Sigma)}$ is the set of laws $P$ under which every coordinate $R_i$ has a finite second moment and

Writing $\mathbf R \sim (\mu,\Sigma)$ means that the law of $\mathbf R$ lies in $\mathbb M^n_{(\mu,\Sigma)}$. For $n=1$ the superscript is dropped: for real $m$ and $v$, $\mathbb M_{(m,v)}$ is the set of laws on $\mathbb R$ with finite second moment, mean $m$ and variance $v$.

For a vector $x \in \mathbb R^n$, the $x$-projection sends the law $P$ of $\mathbf R$ to the law of the scalar $\mathbf r = x'\mathbf R$, that is, to the pushforward of $P$ under $R \mapsto x'R$. Write $\mu_x = x'\mu$ and $\sigma_x^2 = x'\Sigma x$. The matrix $\Sigma$ is positive semidefinite, $\Sigma \succeq 0$, when $x'\Sigma x \ge 0$ for all $x$ (and $\Sigma$ is symmetric); $\Sigma^{1/2}$ denotes its positive semidefinite square root.

Formalization targets

Goal: Theorem 1 (General Projection Property)

For every $\mu \in \mathbb R^n$, every $\Sigma \succeq 0$ and every nonzero $x \in \mathbb R^n$, the $x$-projection maps $\mathbb M^n_{(\mu,\Sigma)}$ into and onto $\mathbb M_{(\mu_x,\sigma_x^2)}$:

The "into" half says every projected law has the right mean and variance. The "onto" half says that every univariate law with mean $\mu_x$ and variance $\sigma_x^2$, however heavy-tailed or irregular, is the law of $x'\mathbf R$ for some $\mathbf R \sim (\mu,\Sigma)$. The degenerate case $x'\Sigma x = 0$ is included.

Milestones

1. The into half (§2.1, justification of (4)): $x'\mathbf R$ has mean $x'\mu$ and variance $x'\Sigma x$.
2. The degenerate case: if $x'\Sigma x = 0$ then $x'\mathbf R = x'\mu$ almost surely.
3. Standardization: if $\mathbf r \sim (m, v)$ with $v > 0$, then $v^{-1/2}(\mathbf r - m) \sim (0,1)$.
4. Normalization: for $x'\Sigma x > 0$, the vector $y = (x'\Sigma x)^{-1/2}\Sigma^{1/2}x$ satisfies $y'y = 1$.
5. Isotropic lift: if $y'y = 1$ and $\mathbf z \sim (0,1)$, there is $\mathbf Z \sim (0, I_n)$ with $y'\mathbf Z$ distributed as $\mathbf z$.
6. Affine image: if $\mathbf Z \sim (0,I_n)$ then $\mu + \Sigma^{1/2}\mathbf Z \sim (\mu,\Sigma)$, and $x'(\mu + \Sigma^{1/2}Z) = x'\mu + (x'\Sigma x)^{1/2}\,y'Z$ for every $Z$.

Significance

The result. Theorem 1 immediately yields Proposition 1 of the paper: for every objective $u$,

with minima in the wide sense of infima. The robust objective is therefore a function of $(\mu_x, \sigma_x)$ alone, which makes every robust mean-covariance problem with a linear outcome a bicriteria mean-variance problem. The paper's later results use this: the two-point and one-point support properties, the parametric quadratic programming solution, and the portfolio applications (bonus schemes, value at risk). The projection property holds with no assumption on $u$, so it serves non-concave, discontinuous and quantile-based objectives alike.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. The mission produces a formal definition of mean-covariance classes that treats integrability honestly, a proof of the projection property, and through it a formally verified reduction of multivariate moment-robust problems to univariate ones. The paper's own construction of the lifted vector has a gap (see Difficulty), so a formal proof also records a corrected argument.

Difficulty

The into half is a computation with linearity of expectation. The difficulty is entirely in the onto half. Given an arbitrary univariate law with prescribed mean and variance, one must build an $n$-variate law with a prescribed full covariance matrix whose one-dimensional marginal in direction $x$ is exactly the given law. This is a coupling problem: the obvious approach, taking independent coordinates, fixes the marginal in direction $x$ as a convolution and cannot reproduce an arbitrary target. Taking $\mathbf R$ supported on the line through $\mu$ in a single direction reproduces the target law but has a rank-one covariance and fails whenever $\Sigma$ has rank above one.

The paper's appendix constructs the lift through conditional distributions of the remaining coordinates given the projected one. As printed, the conditional second-moment requirement it imposes cannot hold for unbounded targets, so that argument does not go through verbatim. The milestone for the lift states only the claim, not the printed construction.

The integrability bookkeeping is real work: every intermediate law must be shown to have finite second moments before its moments can be computed.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Borel σ-algebra; $x'R$ is the inner product $\langle x, R\rangle$; $x'\Sigma x$ is x.ofLp ⬝ᵥ S *ᵥ x.ofLp, where the matrix $\Sigma$ is named S (the symbol Σ is reserved in Lean).
• Laws are probability measures. Both classes require finite second moments (MemLp … 2), so that means and covariances are genuine integrals, not the default value $0$ that Lean assigns to non-integrable functions. The univariate class is parametrized by the variance $v = \sigma^2$, not by $\sigma$.
• The projection is the pushforward P.map (fun R => ⟪x, R⟫) under a continuous map. "Pathwise" identities in the paper become equalities of pushforward laws, or pointwise algebraic identities.
• $\Sigma^{1/2}$ is CFC.sqrt S, acting through Matrix.toEuclideanCLM, as in Mathlib's multivariateGaussian.
• The goal is stated as Set.MapsTo ∧ Set.SurjOn with both classes explicit. Its only hypotheses are $\Sigma \succeq 0$ and $x \ne 0$, as in the paper. No bound on $n$, no invertibility of $\Sigma$ and no positivity of $x'\Sigma x$ is assumed. Restricting the target to Gaussian, bounded or finitely supported laws, or dropping the finite-second-moment clause (which would admit Cauchy laws as "mean 0, variance 0"), would trivialize or change the theorem and is ruled out.
• Milestones 3, 4 and 6 assume $x'\Sigma x > 0$ (or $v > 0$), the case the proof treats after its first sentence; milestone 2 covers the complementary case.

Needed infrastructure: moments of pushforwards under linear and affine maps, a covariance calculus for coordinates of random vectors, and a coupling that realizes the isotropic lift. Mathlib's multivariateGaussian, stdGaussian and CFC.sqrt are available. A reusable lemma "the covariance of $A\mathbf Z + b$ is $A\,\mathrm{Cov}(\mathbf Z)A'$" would serve beyond this mission. Related platform work on moment-based ambiguity sets: Wasserstein Distributionally Robust Optimization II. Contributions of any milestone, and alternative proofs of the lift, 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
• D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM Journal on Optimization 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903
• H. Scarf, A Min-Max Solution of an Inventory Problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• W. W. Rogosinski, Moments of Non-Negative Mass, Proceedings of the Royal Society A 245:1–27, 1958. https://doi.org/10.1098/rspa.1958.0062

Motivation

In stochastic optimization the law of a random return $r$ is rarely known exactly, while its mean and variance can be estimated. A robust mean-covariance decision maker therefore evaluates a utility $u$ by its worst case

Popescu (Operations Research 55(1), 2007) shows that for large classes of utilities this infinite-dimensional problem collapses to a one-dimensional one. The paper projects multivariate problems to a single dimension (the subject of the first mission of this series) and then asks for which $u$ the univariate worst case sits on laws with two support points. This mission formalizes the answer the paper gives for utilities whose marginal utility $u'$ is decreasing and changes curvature once, with finite limits: log-logistic utilities $C+\log\frac{1}{1+e^{-ax}}$ used in statistics and classification, and catenary-type utilities $C-b\cosh(ax)$, each plus a concave quadratic.

The result has a bounded-support precursor: Birge and Dulá (Annals of Operations Research 30, 1991, Theorem 5.1, as cited on p. 102 of Popescu 2007) proved an analogous two-point statement for functions on a bounded interval. Popescu's Proposition 5 is the unbounded version on the whole real line.

Setting

Let $u:\mathbb R\to\mathbb R$.

• The family $\mathcal Q$ collects the coefficient triples of quadratics lying below $u$: $\mathcal Q=\{(A,B,C) \mid q(y)=Ay^2+By+C\le u(y)\ \forall y\in\mathbb R\}$.
• A two-point law with support $\{a,b\}$, $a<b$, puts mass $p\in(0,1)$ on $a$ and $1-p$ on $b$. It has mean $\mu$ and variance $\sigma^2$ when $pa+(1-p)b=\mu$ and $p(a-\mu)^2+(1-p)(b-\mu)^2=\sigma^2$.
• Two-point support property (Definition 1). $u$ has it with respect to $(\mu,\sigma^2)$ if some quadratic $q$ with coefficients in $\mathcal Q$ meets $u$ at two points $a<b$, i.e. $q(a)=u(a)$, $q(b)=u(b)$, and a two-point law with support $\{a,b\}$, mean $\mu$ and variance $\sigma^2$ exists. $u$ has the two-point support property if this holds for every $\mu\in\mathbb R$ and every $\sigma>0$.
• Shapes (Definition 2). $f:\mathbb R\to\mathbb R$ is convex-concave if for some $x_0$ it is convex on $(-\infty,x_0)$ and concave on $(x_0,\infty)$; concave-convex if $-f$ is convex-concave; S-shaped if increasing and convex-concave; inverse S-shaped if $-f$ is S-shaped. So an inverse S-shaped $f$ is decreasing, concave on $(-\infty,x_0)$ and convex on $(x_0,\infty)$.
• Lemma 1's quadratic. For $a<b$ and slopes $q_a,q_b$, set