Operations Research

Motivation

A prophet inequality compares two players facing the same random sequence of rewards $X_1, X_2, \dots, X_n$. The gambler sees the values one at a time and must decide, as each value arrives, whether to stop and collect it; a value passed over is lost. The prophet knows the whole sequence in advance and simply takes its maximum. In 1978 Krengel, Sucheston and Garling showed that when the $X_i$ are independent, non-negative and $\mathbb E[\max_i X_i] < \infty$, the gambler has a stopping rule $\tau$ with

$$2\,\mathbb E[X_\tau] \;\ge\; \mathbb E\big[\max_i X_i\big],$$

and that the factor $2$ cannot be improved. This inequality, labelled (1) in Kleinberg and Weinberg's Matroid Prophet Inequalities (arXiv:1201.4764, STOC 2012), is the starting point of optimal stopping theory's prophet inequalities and, more recently, of a large literature in online algorithms and algorithmic mechanism design, where it is the reason that a single posted price can extract a constant fraction of the optimal welfare or revenue.

Timeline.

• 1977: Krengel and Sucheston prove the inequality with factor 4 in place of 2 (Bull. Amer. Math. Soc. 83).
• 1978: Krengel and Sucheston publish the result attributed to Krengel, Sucheston and Garling, the factor-2 inequality (1) for independent non-negative rewards with $\mathbb E[\max_i X_i] < \infty$; the factor $2$ cannot be improved.
• 1984: Samuel-Cahn shows that a single threshold suffices: stopping at the first value above a threshold $T$ with $\Pr[\max_i X_i > T] = \tfrac12$ (a median of $\max_i X_i$) already achieves the factor $2$ (doi:10.1214/aop/1176993223).
• 2012: Kleinberg and Weinberg, introducing the matroid prophet inequality, give in §3.1 a second single-threshold rule, with threshold $T = \mathbb E[\max_i X_i]/2$, and a half-page proof that it earns at least $T$. This rule and its analysis are the rank-one case of their matroid algorithm.

This mission formalizes that §3.1 result.

Setting

Let $(\Omega, \mathcal F, \mathbb P)$ be a probability space and $n \ge 1$. Let $X_1, \dots, X_n$ be real random variables on $\Omega$ that are independent (as a family), non-negative, and such that the prophet's value $\max_i X_i$ has finite expectation. Define

$$T = \tfrac12\,\mathbb E\big[\max_i X_i\big], \qquad p = \Pr\big[\max_i X_i \ge T\big].$$

The single-threshold rule observes $X_1, X_2, \dots$ in order and stops at the first time $\tau$ with $X_\tau \ge T$, collecting $X_\tau$. If no $X_i$ reaches $T$, the rule accepts nothing and collects $0$. Write $X_\tau$ for the amount collected; it equals $X_{\tau(\omega)}(\omega)$ on the event $\{\max_i X_i \ge T\}$, which has probability $p$, and $0$ off it.

In Lean the variables are X : Fin n → Ω → ℝ with [NeZero n]; $\max_i X_i$ is maxX X, $T$ is thr P X, $p$ is stopProb P X, and $X_\tau$ is reward P X, all in the namespace MatroidProphetKW.RankOne.

Formalization targets

Goal: the half-mean threshold rule

$$\mathbb E[X_\tau] \;\ge\; T \;=\; \tfrac12\,\mathbb E\big[\max_i X_i\big].$$

This is inequality (1) for an explicit rule, which is stronger than (1)'s existence statement. The constant $\tfrac12$ is sharp, so the goal is stated with it.

Milestones (in the order the paper's argument uses them)

1. Tail bound, for every $x > T$:

$$\Pr[X_\tau > x] \;\ge\; (1-p)\sum_{i=1}^n \Pr[X_i > x].$$

2. Comparison with the prophet's tail, for every $x > T$:

$$\Pr[X_\tau > x] \;\ge\; (1-p)\,\Pr\big[\max_i X_i > x\big].$$

3. The prophet's upper tail:

$$\int_T^\infty \Pr\big[\max_i X_i > x\big]\,dx \;\ge\; T.$$

4. The gambler's lower tail:

$$\int_0^T \Pr[X_\tau > x]\,dx \;\ge\; pT.$$

Significance

The result. A threshold that depends on the distributions only through one number, $\mathbb E[\max_i X_i]$, already matches the optimal worst-case guarantee of the best stopping rule. Because it is a single price, the rule translates directly into a posted-price mechanism: a seller who posts the price $T$ to arriving buyers obtains half of the expected maximum value. The same accounting, in which accepted value is charged against the threshold and rejected value against the probability of having accepted nothing, is what Kleinberg and Weinberg generalize to matroids (missions 1 and 2 of this series).

Formalizing it. The result is proved and classical; the work here is to formalize its known proof. No machine-checked proof of the factor-2 prophet inequality is in Mathlib, and none was found among the platform's published theorems in October 2026. A completed development provides the inequality itself, the tail comparisons, and the layer-cake bookkeeping for a stopped reward, all of which are reusable for other single-threshold prophet inequalities (Samuel-Cahn's median rule, $k$-choice and posted-price variants).

Difficulty

The expected reward of the rule is not a function of the marginals of the individual $X_i$ alone in an obvious way: the event that the rule is still running when $X_i$ arrives depends on $X_1, \dots, X_{i-1}$, and the reward is $X_\tau$ at a random index. The natural first attempt, comparing $X_\tau$ and $\max_i X_i$ pointwise, fails, since on a given outcome the rule may stop early at a value just above $T$ while the maximum comes later. The comparison has to be made between distributions, at each level $x$, and it has to use independence to decouple "nothing accepted before time $i$" from "$X_i > x$". The rest is measure-theoretic bookkeeping that is routine on paper and not routine in Lean: expressing expectations of non-negative variables as integrals of tail probabilities, splitting them at $T$, and keeping track of integrability.

Formalization scope

• Probability space. Ω with a MeasurableSpace, P : Measure Ω with [IsProbabilityMeasure P].
• Variables. X : Fin n → Ω → ℝ, [NeZero n]; each X i measurable; iIndepFun X P (mutual independence); 0 ≤ X i ω for all i, ω; Integrable (maxX X) P, which is the paper's $\mathbb E[\max_i X_i] < \infty$.
• Maximum. Finset.sup' over the nonempty index set; no junk supremum.
• Expectations and probabilities. Bochner integrals (∫ ω, … ∂P) and Measure.real probabilities. Tail integrals are Lebesgue integrals of $x \mapsto \Pr[\cdot > x]$ over $(T, \infty)$ and $(0, T]$.
• Weak and strict inequalities are as printed: the rule stops at $X_\tau \ge T$, $p = \Pr[\max_i X_i \ge T]$, tails are $\Pr[\cdot > x]$, for $x > T$.
• The rule may accept nothing. The reward is $0$ when no value reaches $T$; the rule is not forced to stop at $X_n$.

The threshold $T$ is a definition, $\mathbb E[\max_i X_i]/2$, not a free parameter constrained by hypotheses; a formalization in which $T$ is arbitrary and the upper-tail bound is assumed would make the goal a rearrangement of its hypotheses, and is ruled out.

Infrastructure that a complete development needs, and that is welcome as separate contributions: the layer-cake formula $\mathbb E[Y] = \int_0^\infty \Pr[Y > x]\,dx$ for non-negative integrable $Y$ split at a level $T$ (Mathlib has the unsplit form, MeasureTheory.integral_eq_integral_meas_lt); measurability and integrability of the stopped reward (it is dominated by $\max_i X_i$); and the probability of the event "the first $i-1$ values are below $T$ and $X_i > x$" as a product under iIndepFun.

Selected references

• Robert Kleinberg and S. Matthew Weinberg, Matroid Prophet Inequalities, STOC 2012, pp. 123–136; preprint arXiv:1201.4764v1, 2012. https://arxiv.org/abs/1201.4764 (doi:10.1145/2213977.2213991)
• Ulrich Krengel and Louis Sucheston, Semiamarts and finite values, Bulletin of the American Mathematical Society 83, 1977, pp. 745–747.
• Ulrich Krengel and Louis Sucheston, On semiamarts, amarts, and processes with finite value, Advances in Probability and Related Topics 4, 1978, pp. 197–266.
• Ester Samuel-Cahn, Comparison of threshold stop rules and maximum for independent nonnegative random variables, Annals of Probability 12(4), 1984, pp. 1213–1216. https://doi.org/10.1214/aop/1176993223

Motivation

Risk-averse stochastic optimization replaces the expected cost $\mathbb E[X]$ of an uncertain outcome $X$ by a risk function $\rho(X)$: conditional value-at-risk, mean–semideviation and mean–upper-semideviation models, and the coherent and convex risk measures of Artzner, Delbaen, Eber and Heath and of Föllmer and Schied. Ruszczyński and Shapiro, Optimization of convex risk functions (Math. Oper. Res. 31, 2006), develop the convex analysis of such functions on general spaces of random variables, so that they can be used inside optimization problems $\min_{z\in S}\rho(F(z))$.

Optimality conditions, duality and sensitivity analysis for such problems need two regularity properties of $\rho$: continuity, and the existence of subgradients that are continuous linear functionals. For extended-valued convex functions on infinite-dimensional spaces neither comes for free. The standard sufficient condition, boundedness from above on a neighbourhood of a point (Ioffe and Tikhomirov), often cannot be used: the paper notes (p. 436) that the cone of nonnegative functions in $\mathcal L_p(\mathbb R^m,\mathcal B,\mu)$, $p\in[1,+\infty)$, $\mu$ a continuous probability measure, has empty interior. Section 3.1 shows instead that for monotone convex risk functions on a Banach lattice both properties follow from convexity and monotonicity alone. This mission formalizes that result, Proposition 3.1, and its $\mathcal L_p$ instance, Corollary 3.1.

Setting

Let $\mathcal X$ be a real vector space with a partial order $\succeq$, and $\overline{\mathbb R}=[-\infty,+\infty]$. Outcomes are costs: smaller is better. A function $\rho:\mathcal X\to\overline{\mathbb R}$ has domain $\operatorname{dom}\rho=\{X:\rho(X)<+\infty\}$ and is proper if $\rho(X)>-\infty$ for all $X$ and $\operatorname{dom}\rho\neq\emptyset$. The paper's axioms used here are

• (A1) convexity: $\rho(\alpha X+(1-\alpha)Y)\le\alpha\rho(X)+(1-\alpha)\rho(Y)$ for all $X,Y\in\mathcal X$ and $\alpha\in[0,1]$;
• (A2) monotonicity: if $Y\succeq X$ then $\rho(Y)\ge\rho(X)$.

A linear functional $l:\mathcal X\to\mathbb R$, not necessarily continuous, is an algebraic subgradient of $\rho$ at $\bar X$ if

$$\rho(X)\ge\rho(\bar X)+l(X-\bar X)\qquad\forall X\in\mathcal X.\tag{3.1}$$

When $\mathcal X$ is a Banach space it carries its norm topology and is paired with its dual $\mathcal Y:=\mathcal X^*$. The subdifferential $\partial\rho(\bar X)$ is the set of continuous $l\in\mathcal X^*$ satisfying (3.1), and $\rho$ is subdifferentiable at $\bar X$ if $\partial\rho(\bar X)\neq\emptyset$.

A Banach lattice is a real Banach space $\mathcal X$ whose order makes it a lattice, compatible with addition, such that $|X_1|\le|X_2|$ implies $\|X_1\|\le\|X_2\|$. Every $\mathcal L_p(\Omega,\mathcal F,\bar\mu)$, $p\in[1,+\infty]$, with the almost-everywhere order, is one.

In Lean everything lives in the namespace ConvexRiskFn.Cont: dom, IsProper, A1, A2, IsAlgSubgradient and subdiff are defined in the setting file.

Formalization targets

Goal: Proposition 3.1 (p. 437)

Let $\mathcal X$ be a Banach lattice and $\rho:\mathcal X\to\overline{\mathbb R}$ proper, satisfying (A1) and (A2). Then

$$\rho \text{ is continuous on } \operatorname{int}(\operatorname{dom}\rho), \qquad \partial\rho(\bar X)\neq\emptyset \ \text{ for every } \bar X\in\operatorname{int}(\operatorname{dom}\rho).$$

Milestones (the steps of the paper's argument, pp. 436–437)

1. At $\bar X\in\operatorname{int}(\operatorname{dom}\rho)$ the directional derivative $\delta(X)=\rho'(\bar X,X)=\lim_{t\downarrow0}(\rho(\bar X+tX)-\rho(\bar X))/t$ is finite, positively homogeneous and convex, and $\rho(X)\ge\rho(\bar X)+\delta(X-\bar X)$.
2. $\rho$ has an algebraic subgradient at every $\bar X\in\operatorname{int}(\operatorname{dom}\rho)$.
3. Under (A2) an algebraic subgradient is positive: $l(X)\ge0$ for $X\succeq0$.
4. (Levin) Every positive linear functional on a Banach lattice is continuous.
5. If $l\in\partial\rho(\bar X)$, then $\rho$ is lower semicontinuous at $\bar X$.
6. (Phelps) A proper convex $\rho$ on a Banach space that is lower semicontinuous at every point of $\operatorname{int}(\operatorname{dom}\rho)$ is continuous there.

Companions

• Corollary 3.1 (p. 437): for $\mathcal X=\mathcal L_p(\Omega,\mathcal F,\bar\mu)$, $p\in[1,+\infty)$, paired with $\mathcal L_q$, the same conclusion, with subgradients represented by $g\in\mathcal L_q$ through $\int g\,(X-\bar X)\,d\bar\mu$.
• Real-valued case (p. 437): if moreover $\rho(X)<+\infty$ for every $X$, then $\rho$ is continuous on all of $\mathcal X$ and subdifferentiable everywhere.

Significance

Proposition 3.1 removes lower semicontinuity from the list of assumptions a modeller has to check. In the paper's framework, the dual representation $\rho(X)=\sup_{\mu\in\mathcal A}\{\langle\mu,X\rangle-\rho^*(\mu)\}$ (Theorem 2.2) requires lower semicontinuity. The subdifferential formulas, the Hadamard directional differentiability of composite functions $\rho(F(z))$ and the optimality conditions of §§3.2 and 6 require continuity or subdifferentiability at the point of interest. On $\mathcal L_p$ spaces, Corollary 3.1 gives all of these on the interior of the domain from (A1) and (A2) alone, for example for real-valued convex monotone risk functions such as the mean–upper-semideviation and conditional value-at-risk models of §4.

The result is proved in the paper, so the formalization adds no new mathematics. It does add two classical functional-analytic facts that the paper cites without proof: automatic continuity of positive functionals on Banach lattices, and continuity of lower semicontinuous convex functions on open subsets of Banach spaces, here for extended-real-valued functions. As far as a search of Mathlib and of the platform shows, neither is formalized in this generality. Mathlib's continuity result for convex functions is finite-dimensional. Mathlib has the Hahn–Banach extension theorem but no theory of positive functionals on Banach lattices.

Difficulty

An algebraic subgradient exists at an interior point by Hahn–Banach applied to the directional derivative, and in a general Banach space it may be discontinuous. Continuity cannot come from local boundedness either: the usual criterion (bounded above near a point) is exactly what fails for natural examples, since positive cones in $\mathcal L_p$, $p<\infty$, have empty interior. The order structure has to do the work. Monotonicity forces the subgradient to be positive, and positivity forces continuity on a Banach lattice. That last step needs completeness and solidity of the norm. Without them, positive linear functionals need not be continuous, for example on the space of finitely supported sequences.

The second difficulty is passing from lower semicontinuity at each interior point to continuity on the interior. For a convex function this needs a Baire category argument on the Banach space, and completeness cannot be dropped.

Formalization scope

• The Banach lattice is abstract: a type E with NormedAddCommGroup, NormedSpace ℝ, CompleteSpace, Lattice, HasSolidNorm (the solidity condition) and IsOrderedAddMonoid. This is the paper's definition, and it contains the paper's function spaces, so the formal goal is a generalization. Compatibility of the order with multiplication by nonnegative scalars is not assumed; it follows from these axioms.
• $\overline{\mathbb R}$ is EReal. Convexity (A1) is written with EReal arithmetic, which agrees with the paper's for proper functions. Continuity on the interior is continuity of an EReal-valued function in the order topology. On the interior the function is finite, so this is ordinary continuity.
• Subgradients in the goal are continuous linear functionals E →L[ℝ] ℝ, i.e. $\mathcal Y=\mathcal X^*$. A version stating only an algebraic (possibly discontinuous) subgradient would be the easy half of the result and is not the goal; it is milestone 2.
• The interior of the domain may be empty. The goal is then vacuous, as on the page. The domain is never assumed to be all of $\mathcal X$, except in the real-valued companion, where the page assumes it.
• Corollary 3.1 uses Mathlib's Lp ℝ p μbar (a.e. classes) with a finite measure $\bar\mu$ (the paper's measures are finite, p. 434) and $p\neq\infty$. Its subgradient is a function $g$ with MemLp g q μbar for the Hölder conjugate $q$, paired by the integral.
• Needed infrastructure: one-sided directional derivatives of extended-valued convex functions, Hahn–Banach for sublinear functionals (exists_extension_of_le_sublinear in Mathlib), positive functionals on Banach lattices, and the Baire-category continuity theorem for convex lower semicontinuous functions. The last two are reusable well beyond risk functions. Contributions proving any milestone, or proving the Phelps or Levin step in greater generality, are welcome.

Selected references

• A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
• V. L. Levin, Convex Analysis in Spaces of Measurable Functions and Its Applications in Economics, Nauka, Moscow, 1985 (cited as [11]: Lemma 1.1, Theorem 0.12).
• R. R. Phelps, Convex Functions, Monotone Operators and Differentiability, Lecture Notes in Mathematics 1364, Springer, 1989 (cited as [19]: Theorem 3.3).
• A. D. Ioffe, V. M. Tihomirov, Theory of Extremal Problems, North-Holland, 1979 (cited as [9]).
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072

Motivation

A risk function assigns to an uncertain cost $X$ (a function of the random state $\omega$) a single number $\rho(X)$ that a decision maker can minimize. Artzner, Delbaen, Eber and Heath (Math. Finance 9, 1999) singled out four axioms, convexity, monotonicity, translation equivariance and positive homogeneity, and called real-valued functions satisfying all four coherent. Föllmer and Schied (Finance Stoch. 6, 2002) and Frittelli and Rosazza Gianin dropped homogeneity to obtain convex risk measures. In each of these works, a central result is a dual representation: the risk function is a supremum of expectations under a family of probability measures, possibly with a penalty.

Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) place these representations inside general conjugate duality. Their Theorem 2.2 shows that, for any proper, lower semicontinuous, convex risk function on a locally convex space of measurable functions paired with a space of signed measures, the representation holds over the domain of the conjugate, and each remaining axiom corresponds exactly to a property of the measures in that domain. The paper then builds its optimization theory (subdifferentials of composite risk functions, optimality conditions, duality for nonanticipativity constraints) on this representation.

Timeline. Artzner et al. (1999): the coherent axioms, with a representation for finite $\Omega$. Delbaen (2002): coherent measures on $L^\infty$ under the Fatou property. Föllmer–Schied (2002): convex risk measures on bounded functions. Cheridito, Delbaen and Kupper (2004): spaces of processes. Rockafellar, Uryasev and Zabarankin (2002–2006): the risk envelope in $\mathcal L_2$. Ruszczyński–Shapiro (2006): the general paired-space statement formalized here.

Setting

Outcomes are costs: smaller values of $X$ are better. Let $(\Omega,\mathcal F)$ be a measurable space and $\mathbb Y$ the space of finite signed measures on it. The mission fixes

1. a real locally convex topological vector space $\mathcal X$ of $\mathcal F$-measurable functions $X:\Omega\to\mathbb R$, with its own topology (for instance a norm), not necessarily pointwise convergence;
2. a linear subspace $\mathcal Y\subseteq\mathbb Y$ with $\int_\Omega|X|\,d|\mu|<\infty$ for all $X\in\mathcal X$, $\mu\in\mathcal Y$, where $|\mu|=\mu^++\mu^-$;
3. the pairing $\langle\mu,X\rangle=\int_\Omega X\,d\mu=\int X\,d\mu^+-\int X\,d\mu^-$, compatible with the topology of $\mathcal X$: every $\langle\mu,\cdot\rangle$ is continuous, and every continuous linear functional on $\mathcal X$ is some $\langle\mu,\cdot\rangle$, $\mu\in\mathcal Y$.

Write $\mathcal X_+$ for the nonnegative functions, $Y\succeq X$ for $Y(\omega)\ge X(\omega)$ for all $\omega$, $\mathcal Y_+$ for the nonnegative measures in $\mathcal Y$, and $\mathcal P$ for the probability measures in $\mathcal Y$. Condition (C) requires that every $\mu\in\mathcal Y\setminus\mathcal Y_+$ have $\langle\mu,X\rangle<0$ for some $X\in\mathcal X_+$.

A risk function $\rho:\mathcal X\to\overline{\mathbb R}$ is proper if it never equals $-\infty$ and is finite somewhere. The axioms are

• (A1) $\rho(\alpha X+(1-\alpha)Y)\le\alpha\rho(X)+(1-\alpha)\rho(Y)$, $\alpha\in[0,1]$;
• (A2) $Y\succeq X\Rightarrow\rho(Y)\ge\rho(X)$;
• (A3) $\rho(X+a)=\rho(X)+a$, $a\in\mathbb R$;
• (A4) $\rho(tX)=t\rho(X)$, $t>0$.

The conjugate is $\rho^*(\mu)=\sup_{X\in\mathcal X}\{\langle\mu,X\rangle-\rho(X)\}$, the biconjugate $\rho^{**}(X)=\sup_{\mu\in\mathcal Y}\{\langle\mu,X\rangle-\rho^*(\mu)\}$, the dual domain $\mathcal A=\operatorname{dom}\rho^*=\{\mu\in\mathcal Y:\rho^*(\mu)<+\infty\}$, and $\operatorname{lsc}(\rho)(X)=\liminf_{Z\to X}\rho(Z)$ the lower semicontinuous hull. In Lean these are pair, PairedSpaces, CondC, IsProper, A1–A4, conj, biconj, dualDom and lscHull in ConvexRiskFn.Dual.

Formalization targets

Goal: Theorem 2.2 (p. 435)

Under condition (C), for $\rho$ proper, lower semicontinuous and convex,

$$\rho(X)=\sup_{\mu\in\mathcal A}\{\langle\mu,X\rangle-\rho^*(\mu)\}\quad\forall X,\qquad(2.6)$$

and (i) (A2) holds iff every $\mu\in\mathcal A$ is nonnegative; (ii) when $\mathcal X$ contains the constant function $1$, (A3) holds iff $\mu(\Omega)=1$ for all $\mu\in\mathcal A$; (iii) (A4) holds iff $\rho(X)=\sup_{\mu\in\mathcal A}\langle\mu,X\rangle$ for all $X$ (2.7).

Milestones

1. Under (C), $\mathcal Y_+=\{\mu\in\mathcal Y:\langle\mu,X\rangle\ge0\ \forall X\in\mathcal X_+\}$ (p. 434).
2. Theorem 2.1 (Fenchel–Moreau): $\rho^{**}=\operatorname{lsc}(\rho)$ for convex proper $\rho$ with $\operatorname{lsc}(\rho)>-\infty$.
3. The representation (2.6) by itself.
4. Under (C) and (A2), $\rho^*(\mu)=+\infty$ for $\mu\notin\mathcal Y_+$.
5. Under (A3), $\rho^*(\mu)=+\infty$ when $\mu(\Omega)\ne1$.
6. Under (A4), $\rho^*$ is the indicator function of $\{\mu\in\mathcal Y:\langle\mu,\cdot\rangle\le\rho\}$.

Companion: the risk envelope (2.8), p. 436

Under (A1)–(A3), (2.6) holds with $\mathcal A\subseteq\mathcal P$; adding (A4), $\rho^*$ is the indicator of $\mathcal A=\{\mu\in\mathcal P:\langle\mu,X\rangle\le\rho(X)\ \forall X\}$.

Significance

Theorem 2.2 is the unifying statement behind the dual representations of coherent and convex risk measures: one theorem covers bounded measurable functions paired with all finite signed measures, $\mathcal L_p$ paired with $\mathcal L_q$, and weak topologies. Downstream, the paper uses it to describe subdifferentials of risk functions as subsets of $\mathcal A$, to derive optimality conditions for $\min_z\rho(F(z))$, and to obtain the risk envelope (2.8) used in distributionally robust optimization.

The result is proved in the paper, assuming Fenchel–Moreau in locally convex spaces as a cited theorem. As far as is known, neither Theorem 2.2 nor Fenchel–Moreau for extended-real functions on a general locally convex space has a machine-checked proof. At the pinned revision Mathlib has geometric Hahn–Banach separation in locally convex spaces but no Fenchel conjugate at all. A formal proof of the goal would yield, in particular, a reusable Fenchel–Moreau theorem for extended-real convex functions under a measure pairing.

Difficulty

The characterizations (i)–(iii) are short once (2.6) is available; the weight sits in (2.6), that is, in Fenchel–Moreau. Its proof separates a point below the epigraph from the closed convex epigraph in $\mathcal X\times\mathbb R$, which needs Hahn–Banach in a locally convex space, the identification of the separating functional with a measure in $\mathcal Y$ through the compatibility assumption, and a careful case analysis when the separating hyperplane is vertical, a case that occurs because $\rho$ may take the value $+\infty$. The extended-real arithmetic ($r-(+\infty)=-\infty$, $0\cdot(+\infty)=0$) has to be tracked through every supremum. A finite-dimensional argument does not transfer: $\mathcal X$ is an arbitrary locally convex space, and lower semicontinuity is with respect to its own topology.

Formalization scope

$\mathcal X$ is an abstract real vector space with a topology and the instances IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ (no Hausdorff assumption), mapped injectively and linearly into $\Omega\to\mathbb R$. $\mathcal Y$ is a Submodule ℝ (SignedMeasure Ω). The pairing is the difference of the Bochner integrals against the Jordan parts; integrability against $|\mu|$ is a field of the structure, so the pairing is never the junk value of a non-integrable integral. The topology of $\mathcal Y$ is not modelled, since no statement uses it. Risk functions take values in EReal, and every supremum is an iSup in EReal. The order $\succeq$ is pointwise, not almost everywhere. The constant $a$ in (A3) is $a\cdot\mathbf 1$ for an element $\mathbf 1\in\mathcal X$ equal to the constant function $1$. Condition (C) is a separate hypothesis, assumed where it is used.

Two statements depart from the page, and both departures are disclosed in their items. Theorem 2.1 carries the extra hypothesis $\operatorname{lsc}(\rho)>-\infty$, without which the printed statement is false in infinite dimension; Theorem 2.1 is a cited result, and the goal does not depend on this choice. The indicator-function milestone names the set $\{\mu:\langle\mu,\cdot\rangle\le\rho\}$ explicitly instead of "a closed convex subset of $\mathcal Y$".

The goal mentions neither $\rho^{**}$ nor $\operatorname{lsc}(\rho)$: it is stated about $\rho$, $\rho^*$ and $\mathcal A$ alone, and a proof must establish (2.6) from the hypotheses, not assume it. The hypotheses are satisfiable: a one-point $\Omega$ with $\mathcal X=\mathbb R^{\{\ast\}}$, $\mathcal Y=\mathbb Y$ and $\rho(X)=X(\ast)$ meets all of them, including (C) and (A1)–(A4).

Contributions are welcome at every level: Fenchel–Moreau for EReal-valued convex functions on locally convex spaces (reusable well beyond this mission), lemmas about the pairing (linearity, $\langle\mu,1\rangle=\mu(\Omega)$, positivity), and the milestones in the order listed.

Selected references

• A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
• P. Artzner, F. Delbaen, J.-M. Eber, D. Heath, Coherent measures of risk, Mathematical Finance 9(3):203–228, 1999. https://doi.org/10.1111/1467-9965.00068
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
• F. Delbaen, Coherent risk measures on general probability spaces, in Advances in Finance and Stochastics, Springer, 2002, 1–37. https://doi.org/10.1007/978-3-662-04790-3_1
• P. Cheridito, F. Delbaen, M. Kupper, Coherent and convex monetary risk measures for bounded càdlàg processes, Stochastic Processes and their Applications 112(1):1–22, 2004. https://doi.org/10.1016/j.spa.2004.01.009
• R. T. Rockafellar, Conjugate Duality and Optimization, SIAM, 1974. https://doi.org/10.1137/1.9781611970524
• R. T. Rockafellar, S. Uryasev, M. Zabarankin, Generalized deviations in risk analysis, Finance and Stochastics 10(1):51–74, 2006. https://doi.org/10.1007/s00780-005-0165-8

Motivation

Risk-averse optimization replaces the expected cost $\mathbb E[X]$ of a random outcome by a risk function $\rho(X)$ that also penalizes dispersion: mean–deviation, mean–semideviation, conditional value-at-risk (CVaR) and their combinations are the standard examples in stochastic programming and portfolio selection. A decision maker who uses $\rho$ should not prefer an outcome that every risk-averse expected-utility maximizer rejects. For costs, the order that expresses this agreement among risk-averse agents is the increasing convex order: $X_2$ is worse than $X_1$ if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every increasing convex disutility $u$. It is the counterpart, for costs, of second-order stochastic dominance.

Whether a given mean–risk model is consistent with stochastic dominance was settled model by model: Ogryczak and Ruszczyński for mean–semideviation models (Eur. J. Oper. Res. 1999, Math. Program. 2001, SIAM J. Optim. 2002) and Pflug for CVaR (2000). Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) gave a single criterion, Theorem 5.1, which contains these results as special cases: among risk functions that depend only on the distribution of the outcome, consistency with the increasing convex order is equivalent to two structural properties, monotonicity and risk aversion.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $p\in[1,\infty)$. The space of outcomes is $\mathcal X=\mathcal L_p(\Omega,\mathcal F,P)$, the real random variables with $\mathbb E|X|^p<\infty$. An outcome is a cost: smaller is better. A risk function is a map $\rho:\mathcal X\to\mathbb R$.

• The cdf of $X$ is $F_X(t)=P(X\le t)$. $\rho$ is distribution invariant (Definition 5.2) if $F_{X_1}=F_{X_2}$ implies $\rho(X_1)=\rho(X_2)$.
• $\rho$ satisfies (A2) (monotonicity) if $X\le Y$ almost surely implies $\rho(X)\le\rho(Y)$.
• $\rho$ is risk averse (Definition 5.1) if for every $\sigma$-algebra $\mathcal G\subset\mathcal F$ and every $X\in\mathcal X$,

$$\rho(X)\ \ge\ \rho\big(\mathbb E[X\mid\mathcal G]\big),$$

for every version of the conditional expectation.

• For random variables $X_1,X_2$, the usual stochastic order $X_2\succeq_{\mathrm{st}}X_1$ holds if $\mathbb E[u(X_2)]\ge\mathbb E[u(X_1)]$ for every nondecreasing $u:\mathbb R\to\mathbb R$ for which both expectations exist; the increasing convex order $X_2\succeq_{\mathrm{icx}}X_1$ is the same with $u$ ranging over the increasing convex functions.
• $\rho$ is consistent with an order $\succeq$ if $X_2\succeq X_1$ implies $\rho(X_2)\ge\rho(X_1)$ for all $X_1,X_2\in\mathcal X$.

The paper places one more standing assumption on §5.2: the space is rich enough to carry a uniform random variable, a measurable $U:\Omega\to\mathbb R$ with $P(U\le t)=t$ for all $t\in[0,1]$.

In Lean these are IsUniformRV, cdfOf, cdfInv, DistInvariant, A2, RiskAverse, StLE, ConsistentSt and ConsistentIcx in the namespace ConvexRiskFn.Order; the increasing convex order is the published StochasticOrders.MonotoneConvex.IcxOrder P P X₁ X₂, read as $X_1\preceq_{\mathrm{icx}}X_2$.

Formalization targets

Goal: Theorem 5.1 (p. 446)

Under the standing assumptions, for every distribution-invariant $\rho:\mathcal X\to\mathbb R$,

$$\rho\ \text{consistent with}\ \succeq_{\mathrm{icx}}\quad\Longleftrightarrow\quad \rho\ \text{satisfies (A2) and is risk averse}.$$

No convexity, translation equivariance or positive homogeneity of $\rho$ is assumed.

Milestones

1. The usual stochastic order and the cdf (§5.2, p. 445): $X_2\succeq_{\mathrm{st}}X_1$ iff $F_{X_2}(t)\le F_{X_1}(t)$ for all $t$.
2. The quantile coupling (proof of Lemma 5.1, p. 446): $F_X^{-1}(U)$ has the law of $X$, and $F_{X_2}\le F_{X_1}$ gives $F_{X_1}^{-1}(U)\le F_{X_2}^{-1}(U)$ almost surely.
3. Lemma 5.1 (p. 445): a distribution-invariant $\rho$ is consistent with $\succeq_{\mathrm{st}}$ iff it satisfies (A2).
4. Conditional expectation is icx-smaller (proof of Theorem 5.1, p. 446): $\mathbb E[X\mid\mathcal G]\in\mathcal X$ and $\mathbb E[X\mid\mathcal G]\preceq_{\mathrm{icx}}X$.
5. Strassen's coupling on $\Omega$ (proof of Theorem 5.1, p. 446): if $X_1\preceq_{\mathrm{icx}}X_2$, there are $\widehat X_1\overset{D}{\sim}X_1$, $\widehat X_2\overset{D}{\sim}X_2$ on the same $\Omega$ with $\widehat X_1\le\mathbb E[\widehat X_2\mid\widehat X_1]$ a.s.

Significance

Theorem 5.1 reduces a property quantified over all pairs of ordered distributions to two properties that can be checked on the risk function directly. Monotonicity is usually immediate, and risk aversion follows for the main examples from the dual representation of the risk function (the paper verifies it for mean–semideviation and for CVaR-based models in §5.1). The theorem then yields at once the consistency of these models with the increasing convex order, which was previously proved case by case. It also explains the failures: a law-invariant risk function that violates (A2), such as mean–deviation for $p>1$ under the paper's condition $(*)$, cannot be consistent with any increasing integral stochastic order.

The result has a complete published proof. What the mission adds is a machine-checked version of it on the paper's own space $\mathcal L_p(\Omega,\mathcal F,P)$, together with reusable pieces of stochastic-order theory: the cdf characterization of the usual stochastic order, the quantile coupling, conditional Jensen in increasing-convex form, and Strassen's martingale coupling realized on a given space carrying a uniform random variable. Mathlib has conditional Jensen for convex functions (ConvexOn.map_condExp_le_univ) but not the stochastic orders, the quantile coupling or Strassen's theorem. Strassen's theorem for laws on $\mathbb R^n$, with a coupling on some probability space, is posed separately on Prove2Me but not proved.

Difficulty

The forward direction is short given milestone 4. The reverse direction is where the work is. Consistency compares $\rho(X_1)$ and $\rho(X_2)$ for random variables that are related only through their laws: $X_1\preceq_{\mathrm{icx}}X_2$ says nothing about $X_1(\omega)$ versus $X_2(\omega)$, so neither (A2) nor risk aversion applies to the pair as given. The argument has to replace the pair by another pair, with the same laws, on the same space $\Omega$, related by a conditional expectation; only then can monotonicity and risk aversion be chained. Producing that pair is Strassen's theorem, a nonconstructive existence result about martingale couplings, and it has to be realized on the given $\Omega$, not on a product space built for the purpose, because $\rho$ is defined only on $\mathcal L_p(\Omega,\mathcal F,P)$. That is the role of the uniform random variable, and transporting the coupling onto $\Omega$ through it is a separate measure-theoretic step. The first-order analogue, Lemma 5.1, needs the same kind of transfer, through quantile functions, whose values at $0$ and $1$ must be handled.

Formalization scope

• $\mathcal L_p$ is encoded by functions $\Omega\to\mathbb R$ satisfying MemLp X p P with 1 ≤ p and p ≠ ⊤, not by almost-everywhere classes. $\rho$ is a function (Ω → ℝ) → ℝ; every definition quantifies only over MemLp arguments, so its values elsewhere play no role. $\rho$ is real valued, as in Definition 5.2.
• The order in (A2) is the almost-sure order, the order of $\mathcal L_p$ (p. 434).
• "For which the expectations exist" is integrability of $u\circ X_1$ and $u\circ X_2$, as in the published increasing convex order.
• Risk aversion quantifies over every sub-$\sigma$-algebra $\mathcal G\subseteq\mathcal F$ and every $\mathcal G$-measurable version of Mathlib's conditional expectation P[X|m].
• The uniform random variable and $p\in[1,\infty)$ appear as hypotheses of the goal, of Lemma 5.1 and of milestone 5, exactly where the paper's standing assumptions of §5.2 apply. Milestones 1 and 4 do not need them.
• The quantile $F^{-1}(t)=\inf\{s:F(s)\ge t\}$ is a real infimum, which is $0$ where the paper's value is $\pm\infty$ ($t\notin(0,1)$); milestone 2 is therefore stated almost surely.
• The goal mentions neither quantiles, nor $U$ beyond its existence, nor any coupling. A statement that assumed convexity of $\rho$, dropped distribution invariance, restricted to bounded or pointwise-ordered outcomes, or replaced risk aversion by the single $\sigma$-algebra $\{\emptyset,\Omega\}$ would be a different and weaker theorem and does not count.

Needed infrastructure: equality in law from equality of cdfs, the quantile transform, conditional Jensen's inequality (in Mathlib) turned into the increasing convex order, and Strassen's theorem in dimension one with the transfer of a coupling to a space carrying a uniform random variable. The last two are reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas such as the cdf characterization of equality in law, are welcome.

Selected references

• A. Ruszczyński, A. Shapiro, Optimization of convex risk functions, Mathematics of Operations Research 31(3):433–452, 2006. https://doi.org/10.1287/moor.1050.0186
• A. Müller, D. Stoyan, Comparison Methods for Stochastic Models and Risks, Wiley, 2002 (Theorem 1.2.8, Corollary 1.5.21). https://www.wiley.com/en-us/Comparison+Methods+for+Stochastic+Models+and+Risks-p-9780471494461
• V. Strassen, The existence of probability measures with given marginals, Annals of Mathematical Statistics 36(2):423–439, 1965. https://doi.org/10.1214/aoms/1177700153
• D. Blackwell, Equivalent comparisons of experiments, Annals of Mathematical Statistics 24(2):265–272, 1953. https://doi.org/10.1214/aoms/1177729032
• W. Ogryczak, A. Ruszczyński, Dual stochastic dominance and related mean–risk models, SIAM Journal on Optimization 13(1):60–78, 2002. https://doi.org/10.1137/S1052623400375075
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

Conic quadratic optimization — linear optimization over products of quadratic (second-order, Lorentz) cones — covers robust linear programming, portfolio problems with risk constraints, norm minimization and many engineering design problems. Andersen, Roos and Terlaky describe the primal-dual interior-point method implemented in the MOSEK optimizer for this problem class (Math. Program. 95 (2003)). Their algorithm does not solve the primal and dual problems directly. It solves the homogeneous model, an embedding that has a solution whether or not the original problem is feasible, and from which either an optimal pair or a certificate of infeasibility is read off.

The convergence argument of such a method rests on one algebraic property of its search direction: a step along the Newton direction reduces the infeasibility of the homogeneous model and its complementarity gap at the same rate. For linear programming this is classical (Xu, Hung and Ye, 1996; Andersen and Andersen, 2000). This mission formalizes the conic quadratic version, Lemma 4.1 of the paper, in which the diagonal complementarity products of linear programming are replaced by arrow-head matrices.

Setting

The cone is a product $K = K^1\times\cdots\times K^k$. Each factor $K^i\subseteq\mathbb R^{n^i}$ is one of three kinds:

• the half-line $\mathbb R_+ = \{x\in\mathbb R : x\ge0\}$, with $n^i = 1$;
• the quadratic cone $K^q = \{x\in\mathbb R^{n} : x_1^2\ge\|x_{2:n}\|^2,\ x_1\ge0\}$, with $n^i\ge1$;
• the rotated quadratic cone $K^r = \{x\in\mathbb R^{n} : 2x_1x_2\ge\|x_{3:n}\|^2,\ x_1,x_2\ge0\}$, with $n^i\ge2$.

Vectors are partitioned by cones, $x = (x^1;\dots;x^k)$, and $x^Ts = \sum_i (x^i)^Ts^i$. To each cone is attached a symmetric orthogonal matrix $T^i$: the identity for $\mathbb R_+$ and $K^q$, and for $K^r$ the identity with its leading $2\times2$ block replaced by $\frac{1}{\sqrt2}\begin{bmatrix}1&1\\1&-1\end{bmatrix}$. For $v\in\mathbb R^d$ the arrow-head matrix is

$$\operatorname{mat}(v) = \begin{bmatrix} v_1 & v_{2:d}^T\\ v_{2:d} & v_1 I\end{bmatrix}.$$

At a point $(x,s)$ put $X^i = \operatorname{mat}(T^ix^i)$, $S^i = \operatorname{mat}(T^is^i)$, and let $X$, $S$, $T$ be block diagonal with blocks $X^i$, $S^i$, $T^i$. Let $e^i$ be the first unit vector of $\mathbb R^{n^i}$ and $e = (e^1;\dots;e^k)$.

The data are $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$. A current point is $(x^{(0)},\tau^{(0)},y^{(0)},s^{(0)},\kappa^{(0)})$, with

$$\mu^{(0)} = \frac{(x^{(0)})^Ts^{(0)} + \tau^{(0)}\kappa^{(0)}}{k+1}.$$

For a centering parameter $\gamma\in[0,1]$ the Newton direction $(d_x,d_\tau,d_y,d_s,d_\kappa)$ solves the linear system (22):

$$\begin{aligned} A d_x - b d_\tau &= (\gamma-1)(Ax^{(0)} - b\tau^{(0)}),\\ A^Td_y + d_s - c d_\tau &= (\gamma-1)(A^Ty^{(0)} + s^{(0)} - c\tau^{(0)}),\\ -c^Td_x + b^Td_y - d_\kappa &= (\gamma-1)(-c^Tx^{(0)} + b^Ty^{(0)} - \kappa^{(0)}),\\ X^{(0)}Td_s + S^{(0)}Td_x &= -X^{(0)}S^{(0)}e + \gamma\mu^{(0)}e,\\ \tau^{(0)}d_\kappa + \kappa^{(0)}d_\tau &= -\tau^{(0)}\kappa^{(0)} + \gamma\mu^{(0)}. \end{aligned}$$

The new point is $(x^{(1)},\tau^{(1)},y^{(1)},s^{(1)},\kappa^{(1)}) = (x^{(0)},\tau^{(0)},y^{(0)},s^{(0)},\kappa^{(0)}) + \alpha(d_x,d_\tau,d_y,d_s,d_\kappa)$ for a step size $\alpha\in[0,1]$ (23).

Formalization targets

Goal: Lemma 4.1 (p. 13)

Under (22) and (23),

$$\begin{aligned} Ax^{(1)} - b\tau^{(1)} &= (1-\alpha(1-\gamma))(Ax^{(0)} - b\tau^{(0)}),\\ A^Ty^{(1)} + s^{(1)} - c\tau^{(1)} &= (1-\alpha(1-\gamma))(A^Ty^{(0)} + s^{(0)} - c\tau^{(0)}),\\ -c^Tx^{(1)} + b^Ty^{(1)} - \kappa^{(1)} &= (1-\alpha(1-\gamma))(-c^Tx^{(0)} + b^Ty^{(0)} - \kappa^{(0)}),\\ d_x^Td_s + d_\tau d_\kappa &= 0,\\ (x^{(1)})^Ts^{(1)} + \tau^{(1)}\kappa^{(1)} &= (1-\alpha(1-\gamma))\big((x^{(0)})^Ts^{(0)} + \tau^{(0)}\kappa^{(0)}\big). \end{aligned}$$

Milestones

1. (25), p. 13: with $\eta = 1-\gamma$, the shifted point $\eta(x^{(0)},\tau^{(0)},y^{(0)},s^{(0)},\kappa^{(0)}) + d$ satisfies the three linear equations of the homogeneous model.
2. (26), p. 13: $0 = (\eta x^{(0)}+d_x)^T(\eta s^{(0)}+d_s) + (\eta\tau^{(0)}+d_\tau)(\eta\kappa^{(0)}+d_\kappa)$, and its expansion in powers of $\eta$.
3. (61), p. 36: $e^TXSe = \sum_i (T^ix^i)^TT^is^i = x^Ts$ for all $x$, $s$.
4. p. 14, first equality: $(x^{(0)})^Td_s + (s^{(0)})^Td_x = e^T(X^{(0)}Td_s + S^{(0)}Td_x)$, for all vectors.
5. p. 14, the chain's value: $(x^{(0)})^Td_s + (s^{(0)})^Td_x + \tau^{(0)}d_\kappa + \kappa^{(0)}d_\tau = (\gamma-1)\mu^{(0)}(k+1)$.
6. p. 14, orthogonality: $d_x^Td_s + d_\tau d_\kappa = 0$.

Significance

Lemma 4.1 is what makes the homogeneous algorithm analyzable. Because the three residuals and the gap shrink by the same factor $1-\alpha(1-\gamma)$, their ratios are invariant along the iterates, and a step with $\gamma<1$ and $\alpha>0$ makes measurable progress toward a solution of the homogeneous model. The paper notes (p. 14) that all properties stated in Lemma 4.1 hold for the Nesterov–Todd-scaled direction (27) as well, the direction actually implemented, for which polynomial complexity is shown by Monteiro and Tsuchiya (2000).

The result is proved on the page; it is not open. As far as the platform's catalogue shows, it has not been formalized. Machine-checked versions exist only for linear-programming analogues, with diagonal complementarity products in place of arrow-head matrices. The formalization adds two things. First, it fixes three printed slips: the third line of (22) prints $\kappa$ for $\kappa^{(0)}$; the fourth identity of (24) prints $d_x^Td_s^T$; and the proof's evaluation on p. 14 ends with $(\gamma-1)\mu^{(0)}k$ where $(\gamma-1)\mu^{(0)}(k+1)$ is correct, since $e^Te = k$ and the $\tau\kappa$ equation contributes the extra $\mu^{(0)}$. Second, the arrow-head identities (61) and the p. 14 equality are reusable for missions on the complementarity conditions (Lemma 3.1) and the scaled directions of the same paper.

Difficulty

The first three identities of (24) are linear and follow from the first three lines of (22) alone. The content is in the last two. They need an inner-product identity that turns the fourth line of (22), a statement about arrow-head matrix products, into a statement about the scalar quantity $(x^{(0)})^Td_s + (s^{(0)})^Td_x$. The naive reading treats $X^{(0)}Td_s$ as an abstract linear image of $d_s$ and loses exactly this link. What is needed is that the first row of $\operatorname{mat}(v)$ is $v^T$, that $\operatorname{mat}(u)\operatorname{mat}(v)e_1$ has first entry $u^Tv$, and that every $T^i$ is symmetric and orthogonal. The last fails for the rotated cone when $n^i<2$, so the dimension conventions are not decoration. The bookkeeping constant $e^Te = k$ must also be tracked correctly; the page itself gets it wrong.

Formalization scope

• Representation. Blocks are indexed by Fin k; block $i$ is Fin (n i) → ℝ, and indices are 0-based (the paper's $v_1$ is v 0). $A$ is given by its column blocks $A^i$, so $Ax = \sum_iA^ix^i$, $(A^Ty)^i = (A^i)^Ty$ and $c^Tx = \sum_i (c^i)^Tx^i$. The second line of (22) and of (24), and the fourth line of (22), are stated block by block; this is equivalent because $X$, $S$, $T$ are block diagonal.
• Definitions. The shared module ConicQuadIPM.Complementarity.Setting provides the cone kinds, $T^i$ (Tmat), $\operatorname{mat}(v)$ (arrow), $e^i$ (e1) and the predicate WellFormed; this mission's ConicQuadIPM.NewtonStep.Setting adds $\mu^{(0)}$ (mu0) and the system (22) (NewtonSystem). WellFormed is the paper's implicit dimension convention ($n^i = 1$, $\ge1$, $\ge2$ for the three kinds).
• Hypotheses. Every theorem assumes WellFormed. This is a disclosed addition: the paper never states the dimensions, and without them a block of dimension $0$ breaks $e^Te = k$. The ranges $\alpha\in[0,1]$ and $\gamma\in[0,1]$ are kept as on the page, although the identities hold for all real values. No interiority or cone membership of the current point is assumed, because Lemma 4.1 does not use any. The $\kappa$ of (22)'s third line is $\kappa^{(0)}$.
• No trivialization. The fourth line of (22) must stay in terms of arrow and Tmat. Replacing $X^{(0)}Td_s$ by an abstract linear map, or by $(x^{(0)})^Td_s$ directly, would turn milestone 4 into a definition and empty the goal. Milestone 5 states the corrected constant $k+1$; the printed $k$ is false whenever $\gamma\ne1$ and $\mu^{(0)}\ne0$.
• Reusable parts. The arrow-head lemmas (first row of $\operatorname{mat}(v)$, $e_1^T\operatorname{mat}(u)\operatorname{mat}(v)e_1 = u^Tv$, symmetry and orthogonality of $T^i$) are useful beyond this mission. Contributions of these as separate lemmas are welcome.

Selected references

• E. D. Andersen, C. Roos, T. Terlaky, On implementing a primal-dual interior-point method for conic quadratic optimization, Mathematical Programming 95 (2003) 249–277; cited from the authors' preprint of 18 December 2000. https://doi.org/10.1007/s10107-002-0349-3
• X. Xu, P.-F. Hung, Y. Ye, A simplified homogeneous and self-dual linear programming algorithm and its implementation, Annals of Operations Research 62 (1996) 151–171. https://doi.org/10.1007/BF02206815
• E. D. Andersen, K. D. Andersen, The MOSEK interior point optimizer for linear programming: an implementation of the homogeneous algorithm, in High Performance Optimization, Kluwer (2000) 197–232. https://doi.org/10.1007/978-1-4757-3216-0_8
• R. D. C. Monteiro, T. Tsuchiya, Polynomial convergence of primal-dual algorithms for the second-order cone program based on the MZ-family of directions, Mathematical Programming 88 (2000) 61–83. https://doi.org/10.1007/PL00011378

Motivation

Conic quadratic optimization (also called second-order cone programming) minimizes a linear function over the intersection of an affine subspace with a product of quadratic cones. It contains linear programming, convex quadratically constrained programming, robust linear programming with ellipsoidal uncertainty and many problems from engineering design; see Lobo, Vandenberghe, Boyd and Lebret (1998). Primal–dual interior-point methods solve these problems in practice; E. D. Andersen, C. Roos and T. Terlaky describe one such method, and an implementation of it linked to the MOSEK optimizer, in On implementing a primal-dual interior-point method for conic quadratic optimization (Math. Program., 2003).

A primal–dual method needs the optimality condition "the duality gap is zero" in a form that can be relaxed into a central path and linearized by Newton's method. For linear programming that form is the componentwise product $x_js_j=0$. For quadratic cones the scalar condition $x^Ts=0$ is not componentwise, and the paper's Lemma 3.1 gives the replacement: a block-wise system built from arrow-head matrices. This mission formalizes that lemma and the facts its proof uses.

Setting

A vector $v\in\mathbb R^n$ is written $v=(v_1,\dots,v_n)$ and $v_{2:n}=(v_2,\dots,v_n)$; $\|\cdot\|$ is the Euclidean norm. The paper works with three cones (Definition 3.1):

$$\mathbb R_+=\{x\ge 0\},\qquad K^q=\{x\in\mathbb R^n: x_1^2\ge\|x_{2:n}\|^2,\ x_1\ge0\},\qquad K^r=\{x\in\mathbb R^n: 2x_1x_2\ge\|x_{3:n}\|^2,\ x_1,x_2\ge0\},$$

the nonnegative half-line, the quadratic cone and the rotated quadratic cone. The cone of the problem is a product $K=K^1\times\cdots\times K^k$ of such cones, of dimensions $n^1,\dots,n^k$, and a point is partitioned accordingly, $x=(x^1;\dots;x^k)$; $x^Ts=\sum_i(x^i)^Ts^i$.

To each cone the paper attaches two matrices (Definition 3.2): $T^i=Q^i=1$ for $\mathbb R_+$; $T^i=I$ and $Q^i=\operatorname{diag}(1,-1,\dots,-1)$ for $K^q$; and for $K^r$, $T^i$ is the identity except for the leading block $\tfrac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$, while $Q^i$ is $-I$ except for the leading block $\begin{pmatrix}0&1\\1&0\end{pmatrix}$. The arrow-head matrix of a vector is

$$\operatorname{mat}(v)=\begin{pmatrix}v_1&v_{2:n}^T\\ v_{2:n}&v_1I\end{pmatrix},$$

and $X^i=\operatorname{mat}(T^ix^i)$, $S^i=\operatorname{mat}(T^is^i)$; $e^i$ is the first unit vector of $\mathbb R^{n^i}$.

For the companion statements the paper defines $\mu=(x^Ts+\tau\kappa)/(k+1)$ and the neighbourhood

$$\mathcal N(\beta)=\Bigl\{(x,\tau,s,\kappa):(x;\tau),(s;\kappa)\in K\times\mathbb R_+,\ \min_i\sqrt{(x^i)^TQ^ix^i\,(s^i)^TQ^is^i}\ge\beta\mu,\ \tau\kappa\ge\beta\mu\Bigr\}.$$

Formalization targets

Goal: Lemma 3.1 (p. 9)

For $x,s\in K$,

$$x^Ts=0\iff X^iS^ie^i=S^iX^ie^i=0\quad(i=1,\dots,k).$$

This is the paper's exact statement; it fixes no constants and covers every mixture of the three cone types.

Milestones

1. $Q^iQ^i=I$ and $T^iT^i=I$, with $Q^i$, $T^i$ symmetric (p. 9).
2. $K^q=\{x:x^TQx\ge0,\ x_1\ge0\}$ and $K^r=\{x:x^TQx\ge0,\ x_1,x_2\ge0\}$ (p. 9).
3. For the rotated cone's $T$: $x\in K^q\iff Tx\in K^r$ (p. 9).
4. $x\in K$ implies $T^ix^i\in K^q$ for every block (Appendix, p. 36).
5. Identity (61): $(e^i)^TX^iS^ie^i=(T^ix^i)^TT^is^i=(x^i)^Ts^i$, hence $e^TXSe=x^Ts$.
6. The explicit form of (20) for one block: $(x^i)^Ts^i=0$ and $(T^ix^i)_1(T^is^i)_{2:n}+(T^is^i)_1(T^ix^i)_{2:n}=0$ (p. 36).
7. For $x,s\in K$: $x^Ts=\sum_i(T^ix^i)^TT^is^i\ge\sum_i\bigl((T^ix^i)_1(T^is^i)_1-\|(T^ix^i)_{2:n}\|\|(T^is^i)_{2:n}\|\bigr)\ge\sum_i\sqrt{(x^i)^TQ^ix^i(s^i)^TQ^is^i}\ge0$ (pp. 36–37).
8. If $x^Ts=0$ and $(T^ix^i)_1,(T^is^i)_1\ne0$, then $(x^i)^TQ^ix^i=(s^i)^TQ^is^i=0$ and $(T^ix^i)_1(T^is^i)_1=\|(T^ix^i)_{2:n}\|\|(T^is^i)_{2:n}\|$ (p. 37).
9. If $(x^i)^Ts^i=0$ and $(T^ix^i)_1,(T^is^i)_1\ne0$, then $(T^ix^i)_{2:n}=\alpha(T^is^i)_{2:n}$ with $\alpha=-(T^ix^i)_1/(T^is^i)_1$, and (20) holds for block $i$ (p. 37).
10. Lemma 3.2 ii) (p. 11): a point of $\mathcal N(1)$ has $X^iS^ie^i=\mu e^i$ and $\tau\kappa=\mu$.
11. §6.1 (pp. 28–29): the starting point $x^{i(0)}=s^{i(0)}=T^ie^i_1$, $\tau^{(0)}=\kappa^{(0)}=1$ lies in $\mathcal N(1)$.

Significance

Lemma 3.1 is what makes a primal–dual method for conic quadratic problems possible in the familiar form: replacing $X^iS^ie^i=0$ by $X^iS^ie^i=\gamma\mu e^i$ gives the central path (21), and linearizing it gives the Newton system the paper analyses in §4. Lemma 3.2 ii) identifies $\mathcal N(1)$ with that central path, and the §6.1 statement shows the algorithm starts on it. The arrow-head product $X^iS^ie^i$ is the Jordan product of the Lorentz cone's Euclidean Jordan algebra, so the lemma is also the concrete, coordinate form of complementarity in that algebra (Alizadeh and Goldfarb, 2003).

The lemma is proved in the paper's Appendix and is classical; the mission's contribution is a machine-checked version. To our knowledge no proof assistant library contains complementarity for quadratic or rotated quadratic cones, the rotated-cone transformation, or the arrow-head matrix. The statements here are not yet proved anywhere in Lean.

Difficulty

The forward direction is an identity, (61). The converse is where the work is: $x^Ts=0$ is one scalar equation, yet it must force $n^i$ equations per block. The argument needs a reverse Cauchy–Schwarz bound inside each quadratic cone, an equality-case analysis that splits on whether a leading coordinate vanishes, and the reduction of the rotated cone to the quadratic one through $T$. A block-by-block argument fails without first showing that each $(x^i)^Ts^i$ is nonnegative, since only the sum is known to vanish. In Lean, the arithmetic of $1/\sqrt2$ in $T$ and the index bookkeeping of $v_{2:n}$ inside Fin n add their own friction.

Formalization scope

Vectors are Fin d → ℝ; the paper's $x_1$ is index 0 and $x_2$ is index 1, read through coord v r. The Euclidean tails are written out as sums, tailSq v 1 $=\|v_{2:n}\|^2$ and tailSq v 2 $=\|v_{3:n}\|^2$; Mathlib's norm on Fin d → ℝ is the sup norm and is never used. Points of $K$ are stored block by block, x : (i : Fin k) → Fin (n i) → ℝ, with a cone kind kind i ∈ {nonneg, quad, rot} per block; $x^Ts$ is $\sum_i x^i\cdot s^i$, and the block-diagonal $X$, $S$ are represented by their blocks. Tmat, Qmat, arrow and e1 are defined entrywise from (16)–(19) and p. 9.

Standing assumptions and additions:

• The paper never states block dimensions; every theorem assumes WellFormed: $n^i=1$ for $\mathbb R_+$, $n^i\ge1$ for $K^q$, $n^i\ge2$ for $K^r$ (the rotated cone needs $x_1$ and $x_2$).
• "$x,s\in K$" is taken literally; $K$ is self-dual, so no separate dual cone is introduced.
• The milestones 8 and 9 carry the page's case hypotheses $(T^ix^i)_1\ne0$, $(T^is^i)_1\ne0$.
• The printed upper limit $n$ in (61) is read as $k$; "(x; τ), (s; κ) ∈ N(1)" in Lemma 3.2 ii) is read as $(x,\tau,s,\kappa)\in\mathcal N(1)$.

The goal is stated with arrow and Tmat, not with the unfolded vector $((T^ix^i)^TT^is^i;\ (T^ix^i)_1(T^is^i)_{2:n}+(T^is^i)_1(T^ix^i)_{2:n})$: replacing the arrow-head matrices by that vector, or dropping the rotated cone, would remove the content the lemma is about. Contributions welcome: proofs of any milestone, and reusable lemmas on tailSq (Cauchy–Schwarz for tails, its equality case) and on the arrow-head matrix.

Selected references

• E. D. Andersen, C. Roos, T. Terlaky, On implementing a primal-dual interior-point method for conic quadratic optimization, Mathematical Programming 95 (2003). https://doi.org/10.1007/s10107-002-0349-3
• F. Alizadeh, D. Goldfarb, Second-order cone programming, Mathematical Programming 95 (2003), 3–51. https://doi.org/10.1007/s10107-002-0339-5
• M. S. Lobo, L. Vandenberghe, S. Boyd, H. Lebret, Applications of second-order cone programming, Linear Algebra and its Applications 284 (1998), 193–228. https://doi.org/10.1016/S0024-3795(98)10032-0
• Yu. E. Nesterov, M. J. Todd, Primal-dual interior-point methods for self-scaled cones, SIAM Journal on Optimization 8 (1998), 324–364. https://doi.org/10.1137/S1052623495290209