Theorem 1 — five equivalent representations of the worst-case VaR under known mean and covariance

Proved

WorstCaseVaR.KnownMoments.worst_case_var_equivalences

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

moment-problemp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1portfolio-optimizationrobust-optimizationsemidefinite-programmingvalue-at-risk

Let $\hat x \in \mathbb R^n$ and let $\Gamma$ be a positive definite $n\times n$ matrix. Let $\mathcal P$ be the set of all probability distributions on $\mathbb R^n$ with mean $\hat x$ and covariance matrix $\Gamma$ . Fix a portfolio $w \in \mathbb R^n$ with $w \ne 0$ , a loss probability level $\varepsilon \in (0,1)$ and a loss level $\gamma \in \mathbb R$ . Let $\kappa(\varepsilon) = \sqrt{(1-\varepsilon)/\varepsilon}$ , let $\Sigma = \begin{bmatrix} \Gamma + \hat x\hat x^\top & \hat x \\ \hat x^\top & 1\end{bmatrix}$ be the second-moment matrix, and write $\langle A, B\rangle = \operatorname{Tr}(AB)$ . The following propositions are equivalent.

The worst-case VaR at level $\varepsilon$ is at most $\gamma$ :

\sup_{P \in \mathcal P} \operatorname{Prob}_P\{\gamma \le -w^\top x\} \le \varepsilon.

\kappa(\varepsilon)\,\|\Gamma^{1/2}w\|_2 - \hat x^\top w \le \gamma.

There exist a symmetric $(n+1)\times(n+1)$ matrix $M$ and $\tau \in \mathbb R$ with

\langle M, \Sigma\rangle \le \tau\varepsilon,\quad M \succeq 0,\quad \tau \ge 0,\quad M + \begin{bmatrix} 0 & w \\ w^\top & -\tau + 2\gamma\end{bmatrix} \succeq 0.

For every $x \in \mathbb R^n$ with $\begin{bmatrix}\Gamma & x - \hat x\\ (x - \hat x)^\top & \kappa(\varepsilon)^2\end{bmatrix} \succeq 0$ we have $-x^\top w \le \gamma$ .
There exist a symmetric $n\times n$ matrix $\Lambda$ and $v \in \mathbb R$ with

\langle \Lambda, \Gamma\rangle + \kappa(\varepsilon)^2 v - \hat x^\top w \le \gamma, \qquad \begin{bmatrix}\Lambda & w/2\\ w^\top/2 & v\end{bmatrix} \succeq 0.

Proposition 2 is a closed form of the worst-case Value-at-Risk $V_{\mathcal P}(w)$ : it is the smallest $\gamma$ satisfying 1, namely $\kappa(\varepsilon)\|\Gamma^{1/2}w\|_2 - \hat x^\top w$ . Propositions 3–5 are semidefinite representations that extend to the case where the moments are only known to lie in a set.

Formalization Note.

The supremum in Proposition 1 is encoded as "every $P \in \mathcal P$ has $P(\mathcal S) \le \varepsilon$ ", with the probability in $[0,\infty]$ compared with $\varepsilon$ .
The paper prints $\varepsilon \in (0,1]$ . At $\varepsilon = 1$ Proposition 1 holds for every $\gamma$ , while Propositions 2–5 reduce to $\gamma \ge -\hat x^\top w$ , so the theorem is stated for $0 < \varepsilon < 1$ .
The hypothesis $w \ne 0$ is the paper's standing assumption that the admissible set of portfolios does not contain $0$ (used in its proof); with $w = 0$ and $\gamma = 0$ , Proposition 1 fails and Proposition 2 holds.
"Less than $\gamma$ " is the non-strict inequality of the display.
$\|\Gamma^{1/2}w\|_2$ is written $\sqrt{w^\top\Gamma w}$ . The class $\mathcal P$ is HasMeanCov (any Borel probability measure with these first two moments, square-integrable coordinates).

Preamble

import Mathlib
import Definitions.Def_WorstCaseVaR_KnownMoments_Basic

open MeasureTheory Matrix
open scoped InnerProductSpace

Formal statement

namespace WorstCaseVaR.KnownMoments

/-- **Theorem 1** (El Ghaoui–Oks–Oustry 2003, pp. 545–546). Let `𝒫` be the set of probability
distributions on `ℝⁿ` with mean `x̂` and covariance matrix `Γ ≻ 0`, let `w ≠ 0`,
`ε ∈ (0, 1)` and `γ ∈ ℝ`. The following are equivalent:
1. `sup_{P ∈ 𝒫} Prob{γ ≤ -wᵀx} ≤ ε`;
2. `κ(ε) ‖Γ^{1/2} w‖₂ - x̂ᵀw ≤ γ` (7);
3. there exist `M ∈ 𝒮_{n+1}`, `τ ∈ ℝ` with `⟨M, Σ⟩ ≤ τε`, `M ⪰ 0`, `τ ≥ 0`,
   `M + [[0, w], [wᵀ, -τ + 2γ]] ⪰ 0` (9);
4. for every `x` with `[[Γ, x - x̂], [(x - x̂)ᵀ, κ(ε)²]] ⪰ 0` (10), `-xᵀw ≤ γ`;
5. there exist `Λ ∈ 𝒮_n`, `v ∈ ℝ` with `⟨Λ, Γ⟩ + κ(ε)² v - x̂ᵀw ≤ γ` and
   `[[Λ, w/2], [wᵀ/2, v]] ⪰ 0` (11).
The printed range `ε ∈ (0, 1]` is read as `(0, 1)`: at `ε = 1` item 1 holds for every `γ`. -/
theorem worst_case_var_equivalences {n : ℕ}
    (xhat w : EuclideanSpace ℝ (Fin n)) (Γ : Matrix (Fin n) (Fin n) ℝ) (hΓ : Γ.PosDef)
    (hw : w ≠ 0) (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε < 1) (γ : ℝ) :
    List.TFAE
      [ ∀ P : Measure (EuclideanSpace ℝ (Fin n)), HasMeanCov P xhat Γ →
          P (lossSet w γ) ≤ ENNReal.ofReal ε,
        kappa ε * Real.sqrt (⇑w ⬝ᵥ Γ *ᵥ ⇑w) - ⟪xhat, w⟫_ℝ ≤ γ,
        ∃ (M : Matrix (Fin n ⊕ Fin 1) (Fin n ⊕ Fin 1) ℝ) (τ : ℝ),
          (M * secondMomentMatrix xhat Γ).trace ≤ τ * ε ∧ M.PosSemidef ∧ 0 ≤ τ ∧
          (M + bordered 0 ⇑w (-τ + 2 * γ)).PosSemidef,
        ∀ x : EuclideanSpace ℝ (Fin n),
          (bordered Γ ⇑(x - xhat) (kappa ε ^ 2)).PosSemidef → -⟪x, w⟫_ℝ ≤ γ,
        ∃ (Λ : Matrix (Fin n) (Fin n) ℝ) (v : ℝ), Λ.IsSymm ∧
          (Λ * Γ).trace + kappa ε ^ 2 * v - ⟪xhat, w⟫_ℝ ≤ γ ∧
          (bordered Λ ((1 / 2 : ℝ) • ⇑w) v).PosSemidef ] := by sorry

end WorstCaseVaR.KnownMoments

Source

El Ghaoui, Oks and Oustry, Worst-Case Value-at-Risk and Robust Portfolio Optimization: A Conic Programming Approach, Oper. Res. 51 (2003), pp. 545–546, Theorem 1, Eqs. (7)–(11); worst-case VaR Eq. (4), p. 544; w ≠ 0 from p. 543

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Fix a natural number $n$ and work in $\mathbb{R}^n$ with the standard Euclidean inner product $\langle x, y\rangle = \sum_i x_i y_i$ . The data are:

vectors $\hat x, w \in \mathbb{R}^n$ , with the hypothesis $w \neq 0$ ;
a real $n \times n$ matrix $\Gamma$ that is positive definite in Mathlib's sense. This means $\Gamma$ is symmetric and $z^\top \Gamma z > 0$ for every nonzero $z \in \mathbb{R}^n$ ;
a real number $\varepsilon$ with $0 < \varepsilon < 1$ . Both ends are strict;
a real number $\gamma$ , with no restriction.

Under these hypotheses the theorem says that the following five statements are pairwise equivalent: each one holds if and only if each of the others does.

Several names come from an imported definitions file that is not shown here: $\mathrm{HasMeanCov}$ , $\mathrm{lossSet}$ , $\kappa$ (written kappa), $\mathrm{secondMomentMatrix}$ and $\mathrm{bordered}$ . This read-back cannot unfold them, so the statements below depend on those definitions exactly as they are written in that file. The typing does fix some facts:

$\kappa$ takes a real number and returns a real number.
$\mathrm{lossSet}(w, \gamma)$ is a set of points of $\mathbb{R}^n$ .
$S := \mathrm{secondMomentMatrix}(\hat x, \Gamma)$ is a real $(n+1)\times(n+1)$ matrix. Its rows and columns are indexed by the $n$ coordinates plus one extra index.
$\mathrm{bordered}(A, b, c)$ takes an $n\times n$ real matrix $A$ , a vector $b \in \mathbb{R}^n$ and a real number $c$ , and returns a real $(n+1)\times(n+1)$ matrix with that same indexing. The name suggests the block matrix $\begin{pmatrix} A & b \\ b^\top & c\end{pmatrix}$ , but the code shown does not confirm this.

"Positive semidefinite" (PSD) below is also Mathlib's notion: the matrix is symmetric and $z^\top A z \ge 0$ for every $z$ .

(1) For every measure $P$ on $\mathbb{R}^n$ that satisfies $\mathrm{HasMeanCov}(P, \hat x, \Gamma)$ ,

P\big(\mathrm{lossSet}(w,\gamma)\big) \le \varepsilon .

The binder ranges over all measures. Any requirement that $P$ be a probability measure, or that it have mean $\hat x$ and covariance $\Gamma$ , exists only if $\mathrm{HasMeanCov}$ imposes it. The set is not required to be measurable: $P$ is applied to it as an outer measure. The comparison takes place in the extended nonnegative reals, where the right-hand side equals $\varepsilon$ because $\varepsilon > 0$ .

(2)

\kappa(\varepsilon)\,\sqrt{w^\top \Gamma w} \;-\; \langle \hat x, w\rangle \;\le\; \gamma .

(3) There exist a real $(n+1)\times(n+1)$ matrix $M$ , indexed as above, and a real number $\tau$ such that all of the following hold:

\operatorname{tr}(M S) \le \tau\,\varepsilon,\qquad M \succeq 0,\qquad \tau \ge 0,\qquad M + \mathrm{bordered}\big(0_{n\times n},\, w,\, -\tau + 2\gamma\big) \succeq 0 .

Here $\succeq 0$ means PSD, so in particular $M$ is symmetric.

(4) For every $x \in \mathbb{R}^n$ :

\mathrm{bordered}\big(\Gamma,\; x - \hat x,\; \kappa(\varepsilon)^2\big) \succeq 0 \;\Longrightarrow\; -\langle x, w\rangle \le \gamma .

(5) There exist a real $n\times n$ matrix $\Lambda$ and a real number $v$ such that all of the following hold:

$\Lambda$ is symmetric. It is not required to be PSD.
$\operatorname{tr}(\Lambda\Gamma) + \kappa(\varepsilon)^2\, v - \langle \hat x, w\rangle \le \gamma$ .
$\mathrm{bordered}\big(\Lambda,\; \tfrac12 w,\; v\big) \succeq 0$ .

The number $v$ has no sign constraint.

Degenerate cases.

$n = 0$ : $\mathbb{R}^0$ has exactly one point, the zero vector. The hypothesis $w \neq 0$ then cannot be satisfied, so the theorem says nothing when $n = 0$ (it holds vacuously). For $n \ge 1$ all the hypotheses can be satisfied together.
The square root: $\Gamma$ is positive definite and $w \neq 0$ , so $w^\top \Gamma w > 0$ . The square root in (2) is therefore never applied to a negative number, and its "return 0 for negative input" default never occurs.
$\varepsilon$ at the ends of $(0,1)$ : $\varepsilon = 0$ and $\varepsilon = 1$ are excluded. Only the values of $\kappa$ on $(0,1)$ matter, and nothing is claimed about $\kappa$ elsewhere.
Statement (1): if no measure satisfies $\mathrm{HasMeanCov}(P, \hat x, \Gamma)$ , then (1) is vacuously true. Also, if $\mathrm{HasMeanCov}$ does not force $P$ to be finite or a probability measure, (1) quantifies over such measures as well.
Statement (4): if no $x$ makes the bordered matrix PSD, then (4) is vacuously true.
Statement (3): $\tau = 0$ is allowed. The first condition then requires $\operatorname{tr}(MS) \le 0$ .

Whether any of these vacuous situations actually arises depends on the unseen definitions of $\mathrm{HasMeanCov}$ , $\mathrm{bordered}$ and $\kappa$ . In every such situation the theorem still asserts that all five statements have the same truth value.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph