Prove2Me

§2.1, p. 546 — Condition C.1 is equivalent to M⪰0M \succeq 0

Proved
WorstCaseVaR.KnownMoments.quadratic_form_nonneg_iff_posSemidef

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

p2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1semidefinite-programmingvalue-at-risk

Let MM be a symmetric (n+1)×(n+1)(n+1)\times(n+1) real matrix and let l(x)=[x⊤ 1] M [x⊤ 1]⊤l(x) = [x^\top\ 1]\, M\, [x^\top\ 1]^\top be the associated quadratic function on Rn\mathbb R^n. Then

l(x)≥0  for every x∈Rn⟺M⪰0.l(x) \ge 0 \ \text{ for every } x \in \mathbb R^n \quad\Longleftrightarrow\quad M \succeq 0.

This is Condition C.1 in the proof of Theorem 1: finiteness of the dual function of the moment problem requires l≥0l \ge 0 everywhere, and this lemma turns that requirement into a semidefinite constraint.

Formalization Note. xx ranges over EuclideanSpace ℝ (Fin n); MM is indexed by Fin n ⊕ Fin 1 and assumed symmetric (IsSymm), as the paper's M=M⊤M = M^\top.

Preamble
import Mathlib
import Definitions.Def_WorstCaseVaR_KnownMoments_Basic

open MeasureTheory Matrix
open scoped InnerProductSpace
Formal statement
namespace WorstCaseVaR.KnownMoments

/-- Condition C.1 (p. 546): for a symmetric `(n+1) × (n+1)` matrix `M`, the quadratic function
`l(x) = [xᵀ 1] M [xᵀ 1]ᵀ` is nonnegative for every `x ∈ ℝⁿ` iff `M ⪰ 0`. -/
theorem quadratic_form_nonneg_iff_posSemidef {n : ℕ}
    (M : Matrix (Fin n ⊕ Fin 1) (Fin n ⊕ Fin 1) ℝ) (hM : M.IsSymm) :
    (∀ x : EuclideanSpace ℝ (Fin n), 0 ≤ quadFn M ⇑x) ↔ M.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), p. 546, §2.1, proof of Theorem 1, Condition C.1 and Eq. (15)
Read-back

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

Let n≥0n \ge 0 and let MM be a real symmetric (n+1)×(n+1)(n+1)\times(n+1) matrix. Its indices are those of Rn\mathbb{R}^n plus one extra index ⋆\star. For x∈Rnx \in \mathbb{R}^n, let (x,1)∈Rn+1(x,1) \in \mathbb{R}^{n+1} be xx with 11 appended in the ⋆\star coordinate, and let

lM(x)=(x,1)⊤M (x,1).l_M(x) = (x,1)^\top M\, (x,1).

The statement asserts the equivalence

(∀x∈Rn: lM(x)≥0)  ⟺  M⪰0.\bigl(\forall x \in \mathbb{R}^n:\ l_M(x) \ge 0\bigr) \iff M \succeq 0.

Here M⪰0M \succeq 0 means MM is symmetric and z⊤Mz≥0z^\top M z \ge 0 for every z∈Rn+1z \in \mathbb{R}^{n+1}, including vectors whose ⋆\star coordinate is 00 or any other value.

Degenerate cases. If n=0n = 0, then MM is a 1×11\times 1 matrix (c)(c) and lM(x)=cl_M(x) = c for the only point xx. Both sides reduce to c≥0c \ge 0. No other degenerate case applies: every quantity is defined without division or truncation.

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