Convex Optimization

Completed

Functional Analysis·Captain: wenxinzhang

Vector Space Methods VIII: Fenchel DualityTextbook

Motivation

Convex duality converts an optimization problem over points into one over linear functionals. It supplies lower bounds, certificates of optimality, and alternative formulations whose geometry can be simpler than the primal problem. In §§7.8–7.12 of David G. Luenberger's Optimization by Vector Space Methods, this theory is developed for finite-valued convex and concave functions on convex subsets of a real normed space. The capstone is Fenchel duality with restricted domains and an attained continuous-linear-functional dual optimum. This mission preserves that functional-analytic setting rather than reducing the theorem to Euclidean space or silently extending the functions to the whole space.

Setting

Let $X$ be a real normed space, let $C,D\subseteq X$ be nonempty convex sets, let $f:X\to\mathbb R$ be convex on $C$ , and let $g:X\to\mathbb R$ be concave on $D$ . For a continuous linear functional $\ell\in X^*$ , the restricted convex conjugate and restricted concave conjugate are

f_C^*(\ell)=\sup_{x\in C}\bigl(\ell(x)-f(x)\bigr),\qquad g_D^*(\ell)=\inf_{x\in D}\bigl(\ell(x)-g(x)\bigr).

The convex conjugate is admitted into $C^*$ only when its defining set is bounded above; the concave conjugate is admitted into $D^*$ only when its defining set is bounded below. Because $C$ and $D$ are nonempty and the functions are real-valued, these predicates exactly exclude the unwanted infinite endpoint. The Lean definitions use real sSup and sInf, with boundedness carried explicitly by theorem hypotheses.

The restricted epigraph of $(f,C)$ is the set of $(x,r)$ satisfying $x\in C$ and $f(x)\le r$ ; the restricted hypograph of $(g,D)$ reverses the scalar inequality. Luenberger's qualification requires a common point of the relative interiors of $C$ and $D$ , represented by Mathlib's intrinsicInterior, and also requires ordinary nonempty interior of at least one of these two graph sets.

Formalization targets

Main goal: Fenchel duality

Assume the finite primal value $\mu$ is the greatest lower bound of

\{f(x)-g(x):x\in C\cap D\}.

Prove that some $\ell_0\in C^*\cap D^*$ attains

\mu=g_D^*(\ell_0)-f_C^*(\ell_0) =\max_{\ell\in C^*\cap D^*} \bigl(g_D^*(\ell)-f_C^*(\ell)\bigr).

If $x_0$ attains the primal infimum, also prove that $x_0$ attains both conjugate extrema at $\ell_0$ : $f_C^*(\ell_0)=\ell_0(x_0)-f(x_0)$ and $g_D^*(\ell_0)=\ell_0(x_0)-g(x_0)$ .

Milestones

The mission records four source milestones. A local minimum of a convex function on its convex domain is global (§7.8, Proposition 1). Convexity of a restricted function is equivalent to convexity of its restricted epigraph (§7.8, Proposition 2). The finite-conjugate domain and the convex conjugate are convex (§7.10, Proposition 1). Finally, a closed restricted epigraph agrees pointwise on $C$ with the continuous-linear biconjugate (§7.10, Proposition 2). Together these statements expose the geometric and conjugacy interfaces on which the capstone depends without turning every paragraph of the chapter into a separate item.

Significance

The theorem gives an attained dual certificate in an arbitrary real normed space. Equality of primal and dual values eliminates a duality gap, while attainment produces a specific functional that can certify an optimal primal point through simultaneous conjugate equality. The biconjugate milestone is independently useful: it expresses a closed convex function as a supremum of continuous affine minorants on its domain.

Formalizing this material adds a restricted-domain conjugacy API that is not supplied by the existing project artifact named fenchelConjugate. That artifact accepts finite-valued functions on a Euclidean space and has no independent convex domain or concave conjugate. Reusing it here would erase hypotheses that are central to Luenberger's theorem. The new definitions remain small, but their exact boundedness contracts make them reusable for later separation, minimax, and Lagrange-duality missions. The theorem is classical; the mission asks for a checked development faithful to the 1969 source and the current Mathlib representation of continuous dual spaces.

Difficulty

The qualification is not the usual finite-dimensional slogan that relative interiors merely intersect. The source additionally demands that either the restricted epigraph or restricted hypograph have nonempty ordinary interior. Dropping that condition changes the theorem in infinite-dimensional spaces. Replacing intrinsicInterior by topological interior would also make valid lower-dimensional domains appear empty.

Extended values create another boundary. Real sSup and sInf are meaningful here only together with nonempty domains and the respective boundedness hypotheses. Treating their default values outside those hypotheses as genuine conjugates would admit false dual candidates. A finite-dimensional conjugate definition avoids neither issue and would prove only a special case. The biconjugate target must quantify over continuous linear functionals, not all algebraic linear maps, because closed epigraph separation is topological. Finally, the dual statement must include actual attainment; proving only equality with a supremum would omit a principal assertion of §7.12.

Formalization scope

All primal functions are finite-valued real functions. Infinite conjugate values are represented by domain predicates—BddAbove for $f_C^*$ and BddBelow for $g_D^*$ —rather than by changing the public conjugate codomain. The primal finiteness assumption is encoded by a real number $\mu$ together with IsGLB, which simultaneously rules out an empty feasible intersection and an infimum of $-\infty$ . Epigraph pairs are ordered as $(x,r)$ to match Mathlib conventions, although Luenberger prints the scalar coordinate first.

The ambient space is normed but is not assumed finite-dimensional, reflexive, or complete. Both $C$ and $D$ are explicitly nonempty. The main theorem keeps the common intrinsic-interior condition and the disjunctive ordinary-interior condition verbatim. Contributions may develop separation lemmas, boundedness facts for restricted conjugates, or direct proofs of the milestone statements. A whole-space Euclidean specialization is welcome only as a corollary, not as a replacement for the root. The minimax theorem of §7.13 and extended-real lower-semicontinuous variants are outside this mission.

Selected references

David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 7, §§7.8–7.12, pp. 191–202. Open Library record
R. Tyrrell Rockafellar, Convex Analysis, Princeton University Press, 1970. DOI: 10.1515/9781400873173

7 thms3 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Convex Optimization IV: Löwner–John EllipsoidsTextbook

Every full-dimensional convex body is sandwiched between an ellipsoid and its $n$ -fold dilation: shrinking the minimum-volume covering (Löwner–John) ellipsoid $\mathcal{E}$ about its centre $x_0$ by the factor $1/n$ lands inside the body,

x_0 + \tfrac{1}{n}\,(\mathcal{E} - x_0) \;\subseteq\; C \;\subseteq\; \mathcal{E},

and the factor $n$ is tight on simplices. This rounding theorem underlies the ellipsoid method, John's theorem on the Banach–Mazur distance to the Euclidean ball, and much of modern convex geometry. The mission formalizes §8.4 of Boyd & Vandenberghe for polytopes $C = \operatorname{conv}\{x_1,\dots,x_m\}$ , exactly as the book proves it: existence and uniqueness of the extremal ellipsoid, the KKT identities at the normalized optimum ( $\sum_i \lambda_i x_i x_i^{T} = I$ , $\sum_i \lambda_i x_i = 0$ , $\sum_i \lambda_i = n$ ), the convex-combination step that produces the $1/n$ ball, and affine invariance.

8 thms3 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization VI: The Moment Set U^CS Has Support Function μ̂ᵀv + Γ₁‖v‖ + √(1/ε − 1)‖Cv‖, an Upper Bound on the Worst-Case Value at RiskResearch Paper

Motivation

In robust optimization, a constraint is checked against every parameter value in an uncertainty set. This turns uncertainty into a deterministic optimization problem, but the set must be chosen carefully: a large set can make decisions unnecessarily conservative, while a small one can miss likely outcomes. Bertsimas, Gupta and Kallus use data to calibrate sets through statistical confidence regions. Their question is whether feasibility for every parameter in the set protects a decision against a fresh uncertain outcome with a specified probability. This mission treats the part of their construction based on estimated first and second moments. Bertsimas, Gupta and Kallus, §8.1.

The moment region originates in a concentration result attributed in the paper to Shawe-Taylor and Cristianini. That result bounds the distance between sample and population means and covariances when the uncertain vector is supported in a Euclidean ball. Bertsimas, Gupta and Kallus also discuss replacing those analytic thresholds with bootstrap thresholds; they describe the resulting coverage as approximate. The present target concerns the mathematical relation between a fixed moment region and its uncertainty set, leaving the statistical calibration of the thresholds to its cited source. Shawe-Taylor and Cristianini, 2003; Bertsimas, Gupta and Kallus, pp. 24–25.

Setting

Let the uncertain vector $\tilde u$ take values in $\mathbb R^d$ . A probability law $P$ belongs to the moment confidence region $\mathcal P^{CS}$ when it is supported in the Euclidean ball of radius $R$ , its mean $m_P$ is within $\Gamma_1$ of an estimate $\hat\mu$ , and its covariance $S_P$ is within $\Gamma_2$ of an estimate $\hat\Sigma$ in Frobenius norm. The covariance is $S_P=\mathbb E_P[\tilde u\tilde u^\top]-m_Pm_P^\top$ . The thresholds $\Gamma_1,\Gamma_2$ are nonnegative and can be chosen by either calibration procedure discussed in the paper. Bertsimas, Gupta and Kallus, Theorem 9 and (33).

For a vector $v$ , Value at Risk $\operatorname{VaR}^{P}_{\varepsilon}(v)$ is the smallest threshold $t$ for which $P(\tilde u^\top v\le t)\ge1-\varepsilon$ . The support function of a set $\mathcal U$ is $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$ . The authors construct the set

\mathcal U^{CS}_{\varepsilon} =\{\hat\mu+y+C^\top w:\|y\|_2\le\Gamma_1,\ \|w\|_2\le\sqrt{1/\varepsilon-1}\}, \qquad C^\top C=\hat\Sigma+\Gamma_2 I.

Here $0<\varepsilon<1$ is the allowed violation probability, $I$ is the identity matrix, and $C$ is a matrix factor of the adjusted covariance. The estimates and $C$ stay fixed while $\varepsilon$ varies. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization targets

The first milestone bounds the quantile for every law in the moment region:

\operatorname{VaR}^{P}_{\varepsilon}(v)\le \hat\mu^\top v+\Gamma_1\|v\|_2+ \sqrt{\frac{1-\varepsilon}{\varepsilon}} \sqrt{v^\top(\hat\Sigma+\Gamma_2I)v} \quad(P\in\mathcal P^{CS}).

The second milestone evaluates the two linear maxima over the Euclidean balls in $\mathcal U^{CS}_{\varepsilon}$ and identifies $\|Cv\|_2$ with the quadratic form above. The goal, the deterministic part of Theorem 10, says the displayed bound equals $\delta^*(v\mid\mathcal U^{CS}_{\varepsilon})$ for every $v$ , while the set is nonempty, convex and compact. This gives the support-function criterion of Theorem 1 for each law in the region. A companion formalizes Theorem 13(a): the resulting support constraint is separately convex in $(v,t)$ and in $\varepsilon$ for $0<\varepsilon<3/4$ . Bertsimas, Gupta and Kallus, Theorems 10 and 13(a).

Significance

The support formula turns a distributional statement about an entire region of probability laws into a deterministic bound on a linear projection. It gives the robust model an explicit quantity to compare with a constraint threshold. The companion convexity result describes which risk levels allow separate convex optimization in the decision variables and the violation probability. Together they explain why the particular set in (35) is useful beyond the fact that it contains plausible uncertain vectors. Bertsimas, Gupta and Kallus, §§8.1 and 9.

The paper proves the mathematical construction and cites statistical results for the region's coverage. In Lean, the published Value-at-Risk and support-function definitions are already available, while this paper's moment region and set (35) need their own definitions. Formalizing the result therefore establishes a reusable interface between moment bounds, quantiles and set support. The theorem statements in this proposal are open proof targets; compiling them checks their types, not their proofs.

Difficulty

A bound on the mean and covariance does not directly bound a high quantile of every projection. The bound must work simultaneously for every probability law in the moment region, including discrete laws and singular covariances. The factor $\sqrt{(1-\varepsilon)/\varepsilon}$ is essential: replacing it by a standard deviation or a Gaussian quantile would change the claim. On the set side, the ordinary norm of a Lean function vector is a sup norm, whereas both balls in (35) are Euclidean. Getting the norm wrong changes the support function. Bertsimas, Gupta and Kallus, (34)–(35).

Formalization scope

Vectors are functions on Fin d, whose coordinates start at zero. enorm and frob explicitly compute the Euclidean and Frobenius norms. The ball-support condition in $\mathcal P^{CS}$ secures finite first and second moments; no density is assumed. The goal fixes $R\ge0$ , $\Gamma_1,\Gamma_2\ge0$ , $0<\varepsilon<1$ , and $C^\top C=\hat\Sigma+\Gamma_2I$ . This factor relation makes the quadratic form nonnegative; a separate positive-semidefinite assumption on $\hat\Sigma$ is unnecessary. The matrix need not be triangular because (35) and its support depend on $C^\top C$ . The uncertainty set's nonemptiness and compactness appear in the goal so the real support-function supremum cannot take Lean's default value for an empty or unbounded set.

Theorem 10's sampling claim is represented by its deterministic criterion for each $P\in\mathcal P^{CS}$ . The confidence-region coverage of Theorem 9 is cited, and the bootstrap coverage discussed on p. 25 is approximate; neither is asserted as an exact probability theorem here. Equation (34) prints an equality for a supremum over $\mathcal P^{CS}$ , yet that region restricts support to a ball, and the page does not establish attainment under that restriction. This mission uses the upper-bound direction needed for Theorem 10 and does not assert the equality or Remark 16's exact equivalence. The scope includes a sharp quantile bound, the exact support formula and the $3/4$ convexity range; a definition that merely makes the claim true by construction would miss these targets. Bertsimas, Gupta and Kallus, pp. 24–25 and 29.

Selected references

D. Bertsimas, V. Gupta and N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised in Mathematical Programming 167 (2018), 235–292. arXiv preprint.
J. Shawe-Taylor and N. Cristianini, Estimating the Moments of a Random Vector with Applications, 2003. University of Southampton ePrint.
G. C. Calafiore and L. El Ghaoui, On Distributionally Robust Chance-Constrained Linear Programs, Journal of Optimization Theory and Applications 130 (2006), 1–22. DOI.

6 thms2 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization V: The Order-Statistic Box U^M Built from Marginal Samples Dominates Value at Risk with Probability at Least 1 − αResearch Paper

Motivation

Robust optimization replaces an uncertain constraint $f(\tilde{\mathbf u},\mathbf x)\le 0$ by the requirement that it hold for every $\mathbf u$ in an uncertainty set $\mathcal U\subseteq\mathbb R^d$ . The resulting problems are tractable for many sets, but the choice of $\mathcal U$ decides whether the solution means anything probabilistically. Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167:235–292, 2018) propose to build $\mathcal U$ from data so that, with high probability over the sample, every robust-feasible decision is also feasible with probability at least $1-\epsilon$ under the unknown distribution $\mathbb P^*$ .

This mission covers §6 of that paper, the case where the data are samples of the marginals of $\mathbb P^*$ , observed separately, with no assumption that the marginals are independent. This is the situation of asynchronous measurements or records with many missing entries: the joint law cannot be learned, yet a valid uncertainty set can still be built. The set is a box whose sides are order statistics, and its guarantee rests on an elementary binomial test (David and Nagaraja, Order Statistics, §7.1) and a Value-at-Risk bound of Embrechts, Höing and Juri (Finance Stoch. 7, 2003).

Setting

Let $\mathbb P^*$ be a probability measure on $\mathbb R^d$ whose support lies in a known box $[\hat{\mathbf u}^{(0)},\hat{\mathbf u}^{(N+1)}]=\{\mathbf u:\hat u^{(0)}_i\le u_i\le\hat u^{(N+1)}_i\}$ . Fix a violation level $0<\epsilon<1$ and a significance level $0<\alpha<1$ .

The Value at Risk of $\tilde{\mathbf u}^T\mathbf v$ under a probability measure $\mathbb P$ is

\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^T\mathbf v\le t)\ge1-\epsilon\},

and the support function of a set $\mathcal U$ is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^T\mathbf u$ . A set $\mathcal U$ implies a probabilistic guarantee at level $\epsilon$ for $\mathbb P^*$ if for every $f(\mathbf u,\mathbf x)$ concave in $\mathbf u$ and every $\mathbf x^*$ , $f(\mathbf u,\mathbf x^*)\le0$ for all $\mathbf u\in\mathcal U$ implies $\mathbb P^*(f(\tilde{\mathbf u},\mathbf x^*)\le0)\ge1-\epsilon$ .

From a sample $\hat{\mathbf u}^1,\dots,\hat{\mathbf u}^N$ let $\hat u^{(j)}_i$ , $1\le j\le N$ , be the $j$ -th order statistic (the $j$ -th smallest value) of coordinate $i$ , and let $\hat u^{(0)}_i,\hat u^{(N+1)}_i$ be the box ends. The index $s$ is

s=\min\Big\{k\in\mathbb N:\sum_{j=k}^N\binom Nj(\epsilon/d)^{N-j}(1-\epsilon/d)^j\le\frac{\alpha}{2d}\Big\},\qquad s=N+1\text{ if the set is empty}, \tag{26}

and the uncertainty set is the box

\mathcal U^M_\epsilon=\{\mathbf u\in\mathbb R^d:\hat u^{(N-s+1)}_i\le u_i\le\hat u^{(s)}_i,\ i=1,\dots,d\}. \tag{28}

The confidence region $\mathcal P^M$ is the set of probability measures on the box with $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(\mathbf e_i)\le\hat u^{(s)}_i$ and $\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ for every $i$ .

Formalization targets

Goal: Theorem 7

If $N-s+1<s$ , then with probability at least $1-\alpha$ over the sample ( $N$ samples of each marginal of $\mathbb P^*$ , each marginal's samples i.i.d., arbitrary dependence across marginals),

\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)\qquad\text{for all }\mathbf v\in\mathbb R^d,

and, for every sample, $\mathcal U^M_\epsilon$ is nonempty, convex and compact with

\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)=\sum_{i=1}^d\max\big(v_i\hat u^{(N-s+1)}_i,\,v_i\hat u^{(s)}_i\big). \tag{29}

Milestones

Positive homogeneity: $\mathrm{VaR}^{\mathbb P}_\delta(c\mathbf w)=c\,\mathrm{VaR}^{\mathbb P}_\delta(\mathbf w)$ for $c>0$ (p. 10).
Each one-sided order-statistic test is valid at level $\alpha/(2d)$ : $\mathbb P^*_{\mathcal S}(\hat u^{(s)}_i<\mathrm{VaR}^{\mathbb P^*}_{\epsilon/d}(\mathbf e_i))\le\alpha/(2d)$ , and the mirror bound for $-\mathbf e_i$ with $\hat u^{(N-s+1)}_i$ (pp. 20–21).
Union bound: $\mathbb P^*_{\mathcal S}(\mathbb P^*\in\mathcal P^M)\ge1-\alpha$ (p. 21).
The weak Embrechts bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_i\mathrm{VaR}^{\mathbb P}_{\epsilon/d}(v_i\mathbf e_i)$ for every probability measure $\mathbb P$ (p. 21).
If $N-s+1<s$ then $\hat u^{(N-s+1)}_i\le\hat u^{(s)}_i$ (p. 21).
(EC.8): for $\mathbb P\in\mathcal P^M$ , $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\sum_{v_i>0}v_i\hat u^{(s)}_i+\sum_{v_i\le0}v_i\hat u^{(N-s+1)}_i$ (p. ec5).
(29) as a standalone statement (p. 21).

Significance

Theorem 7 gives an uncertainty set with a finite-sample guarantee from data that carry no information on the dependence between coordinates. The set is a box, so the robust counterpart of a linear constraint is again linear, and Remark 12 of the paper notes that separation over $\{(\mathbf v,t):\delta^*(\mathbf v\mid\mathcal U^M)\le t\}$ is in closed form. Unlike the other confidence regions of the paper (χ², G-test, Kolmogorov–Smirnov, bootstrap), whose coverage is asymptotic, tabulated or approximate, the test here is exact and distribution-free, so the probability statement itself is in scope.

The result is proved in the paper; to our knowledge none of it has a machine-checked proof. The mission produces a complete formal statement of Theorem 7 including the sampling probability, the binomial order-statistic test for a quantile, and the marginal Value-at-Risk bound, all of which are standard tools in nonparametric statistics and risk management that are absent from Mathlib.

Difficulty

The deterministic half, (EC.8) and (29), is short once the weak Embrechts bound is available. The work is in the probabilistic half, which the paper delegates to a textbook citation. Validity of the order-statistic test ties together facts that no library currently connects: the combinatorics of sorted tuples, the binomial law of the number of i.i.d. sample points below a threshold, the behaviour of a quantile at its left limit (the distribution function at the quantile can exceed $1-\epsilon/d$ , so the obvious bound uses the wrong probability), and the comparison of binomial tails across success probabilities. The lower-tail test must be handled with the index $N-s+1$ and the quantile of $-\tilde u_i$ , where a sign or off-by-one slip produces a false statement that still looks plausible. The boundary regime $s=N+1$ , where $\mathcal U^M_\epsilon$ is the a priori box, is valid only because $\mathbb P^*$ lives in that box and needs separate treatment.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with 0-based coordinates; vectors pair by ⬝ᵥ. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ applied to $\mathbf u\mapsto\mathbf u^T\mathbf v$ , and the support function is the published RobustMDP.Shared.supportFunction; both are real infima/suprema, genuine under $0<\epsilon<1$ , a probability measure, and a nonempty bounded set (the goal proves the latter). The order statistics use Mathlib's Tuple.sort; the index $N-s+1$ is N + 1 - s in natural numbers, which is the paper's value since $1\le s\le N+1$ .

The data are an array S : Fin N → Fin d → ℝ, S k i the $k$ -th sample of marginal $i$ , under any probability law Q such that, for each $i$ , the samples S 0 i, …, S (N-1) i are i.i.d. from the $i$ -th marginal of $\mathbb P^*$ (IsMarginalSampleLaw). The dependence between samples of different marginals is left arbitrary, as the paper's asynchronous setting requires; i.i.d. draws of whole vectors are one admissible law. Probabilities of possibly non-measurable events are outer measures. The level $\epsilon$ is fixed: by Remark 11 the family $\{\mathcal U^M_\epsilon\}$ need not work for all $\epsilon$ simultaneously.

The guarantee is stated in the criterion form of Theorem 1(a) of the paper: $\delta^*(\mathbf v\mid\mathcal U^M_\epsilon)\ge\mathrm{VaR}^{\mathbb P^*}_\epsilon(\mathbf v)$ for all $\mathbf v$ , together with nonemptiness, convexity and compactness of $\mathcal U^M_\epsilon$ . Theorem 1 (mission I of this series) shows that for such sets this criterion is equivalent to implying a probabilistic guarantee. The coverage of the test is proved, not assumed: there is no hypothesis that $\mathbb P^*\in\mathcal P^M$ . A formalization in which the support function is evaluated on an empty or unbounded set, where the library value is 0, would make the criterion trivial; the nonemptiness and compactness conjunct of the goal rules it out.

Standing assumptions: $d\ge1$ , $0<\epsilon<1$ , $0<\alpha<1$ , $\hat{\mathbf u}^{(0)}\le\hat{\mathbf u}^{(N+1)}$ , $\mathbb P^*$ a probability measure with $\mathbb P^*$ -null complement of the box, and Theorem 7's hypothesis $N-s+1<s$ . The page prints the second condition of $\mathcal P^M$ as " $\mathrm{VaR}^{\mathbb P_i}_{\epsilon/d}\ge\hat u^{(N-s+1)}_i$ "; the formal region uses the lower-tail condition $\mathrm{VaR}_{\epsilon/d}(-\mathbf e_i)\le-\hat u^{(N-s+1)}_i$ that the hypothesis, its rejection rule and the proof use. (EC.8) is stated with " $\le$ " for each $\mathbb P\in\mathcal P^M$ ; the page's middle equality is not claimed.

Reusable infrastructure welcome beyond this mission: order statistics of tuples and the binomial law of threshold counts for i.i.d. samples; monotonicity of binomial tails in the success probability; the left-limit property of quantiles; the Embrechts-type subadditivity bound for Value at Risk.

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
H. A. David, H. N. Nagaraja, Order Statistics, Wiley (cited by the paper as 1970; third edition 2003), §7.1, distribution-free confidence intervals for quantiles. https://doi.org/10.1002/0471722162
P. Embrechts, A. Höing, A. Juri, Using copulae to bound the Value-at-Risk for functions of dependent risks, Finance and Stochastics 7:145–167, 2003. https://doi.org/10.1007/s007800200085

11 thms2 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization IV: The Forward–Backward Deviation Set U^FB Has a Closed-Form Support Function That Bounds the Worst-Case Value at RiskResearch Paper

Motivation

A robust linear constraint $u^\top v \le t$ with $u$ ranging over an uncertainty set $\mathcal U\subseteq\mathbb R^d$ is tractable whenever the support function $\delta^*(v\mid\mathcal U)=\sup_{u\in\mathcal U}u^\top v$ is. Robust optimization gains a probabilistic meaning when $\mathcal U$ is chosen so that every robustly feasible decision also satisfies the constraint with probability at least $1-\varepsilon$ under the true distribution $\mathbb P^*$ of the uncertain parameter $\tilde u$ . Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets from data: a statistical hypothesis test yields a confidence region $\mathcal P$ of distributions, and the uncertainty set is any convex set whose support function dominates the worst-case Value at Risk over $\mathcal P$ .

Section 5.2 of the paper applies this schema to the forward and backward deviations of Chen, Sim and Sun (Oper. Res. 55, 2007), one-sided measures of spread that capture skewness. Chen, Sim and Sun assume the mean and deviations are known; the data-driven version replaces them by confidence intervals and must work out the worst case over those intervals. The result is the set $\mathcal U^{FB}_\varepsilon$ of Theorem 6, whose support function has a closed form.

Setting

The uncertain parameter $\tilde u$ takes values in $\mathbb R^d$ and $\mathbb P$ is its law. For $\varepsilon\in(0,1)$ and $v\in\mathbb R^d$ , the Value at Risk is

\mathrm{VaR}^{\mathbb P}_\varepsilon(v)=\inf\{t:\mathbb P(\tilde u^\top v\le t)\ge1-\varepsilon\}.

For a probability measure $\mathbb P_i$ on $\mathbb R$ with mean $\mu_i$ , the forward deviation and the backward deviation are

\sigma_f(\mathbb P_i)=\sup_{x>0}\sqrt{-\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{x\tilde u_i}]},\qquad\sigma_b(\mathbb P_i)=\sup_{x>0}\sqrt{\tfrac{2\mu_i}{x}+\tfrac{2}{x^2}\log\mathbb E^{\mathbb P_i}[e^{-x\tilde u_i}]}.

From a sample, a bootstrap produces thresholds $t_i$ , $\bar\sigma_{fi}$ , $\bar\sigma_{bi}$ . With the sample mean $\hat\mu_i$ put $m_{bi}=\hat\mu_i-t_i$ and $m_{fi}=\hat\mu_i+t_i$ . The confidence region $\mathcal P^{FB}$ consists of the distributions of vectors with independent components $\tilde u_i\sim\mathbb P_i$ , each $\mathbb P_i$ having bounded support, mean in $[m_{bi},m_{fi}]$ , $\sigma_f(\mathbb P_i)\le\bar\sigma_{fi}$ and $\sigma_b(\mathbb P_i)\le\bar\sigma_{bi}$ .

The uncertainty set is

\mathcal U^{FB}_\varepsilon=\Big\{y_1+y_2-y_3:\ y_2,y_3\in\mathbb R^d_+,\ \sum_{i=1}^d\Big(\frac{y_{2i}^2}{2\bar\sigma_{fi}^2}+\frac{y_{3i}^2}{2\bar\sigma_{bi}^2}\Big)\le\log(1/\varepsilon),\ m_{bi}\le y_{1i}\le m_{fi}\Big\}.

Formalization targets

Goal: Theorem 6

For $m_b\le m_f$ , $\bar\sigma_f,\bar\sigma_b>0$ and $\varepsilon\in(0,1)$ , the set $\mathcal U^{FB}_\varepsilon$ is nonempty, convex and compact,

\delta^*(v\mid\mathcal U^{FB}_\varepsilon)=\sum_{i:v_i\ge0}m_{fi}v_i+\sum_{i:v_i<0}m_{bi}v_i+\sqrt{2\log(1/\varepsilon)\Big(\sum_{i:v_i\ge0}\bar\sigma_{fi}^2v_i^2+\sum_{i:v_i<0}\bar\sigma_{bi}^2v_i^2\Big)}\qquad(24)

for every $v$ , and $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)$ is at most the right-hand side of (24) for every $\mathbb P\in\mathcal P^{FB}$ and every $v$ .

Milestones

The Chen–Sim–Sun bound (22): for independent components with known means $\mu_i$ and deviations, $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\sum_i\mu_iv_i+\sqrt{2\log(1/\varepsilon)(\sum_{v_i<0}\sigma_{bi}^2v_i^2+\sum_{v_i\ge0}\sigma_{fi}^2v_i^2)}$ .
The right-hand side of (24) is the worst case of (22) over the parameters allowed by $\mathcal P^{FB}$ .
Lagrangian strong duality for $\max_{u\in\mathcal U^{FB}_\varepsilon}u^\top v$ .
The three one-dimensional sub-subproblems and their optimal values.
The combined formula: $\delta^*$ equals a linear term plus $\inf_{\lambda>0}\{\lambda\log(1/\varepsilon)+S/(2\lambda)\}$ .
$\inf_{\lambda>0}\{\lambda L+S/(2\lambda)\}=\sqrt{2LS}$ , attained at $\lambda^*=\sqrt{S/(2L)}$ when $S>0$ .

Companions

Remark 9: when (24) exceeds $t$ , an explicit point of $\mathcal U^{FB}_\varepsilon$ gives a violated cut $u^\top v\le t$ .
Theorem 13(b): the constraint $\delta^*(v\mid\mathcal U^{FB}_\varepsilon)\le t$ is convex in $(v,t)$ and convex in $\varepsilon$ for $0<\varepsilon<1/\sqrt e$ .

Significance

Theorem 6 gives a data-driven uncertainty set for which a robust linear constraint is a second-order cone constraint, (24) being an explicit norm expression. By Theorem 1 of the paper, the domination of the worst-case Value at Risk over the region by the support function means that every robustly feasible solution satisfies a chance constraint at level $\varepsilon$ for every distribution in the region. Unlike the Chen–Sim–Sun set, which requires the true mean and deviations, $\mathcal U^{FB}_\varepsilon$ needs only data and allows the mean and the support to be unknown. Theorem 13(b) supports the alternating heuristic of §9 for choosing the levels $\varepsilon_j$ across several constraints.

The paper's proof is short and leans on "by inspection" and "by Lagrangian strong duality". A formal development makes each of these steps explicit, including the case where the multiplier is not attained, and corrects two printed slips (the optimal values $v_i\bar\sigma^2/(2\lambda)$ , which should be $v_i^2\bar\sigma^2/(2\lambda)$ , and the bound $m_b\le y_1\le m_b$ ). The Chen–Sim–Sun bound itself, a Chernoff-type tail bound under one-sided moment-generating conditions, is cited by the paper without proof. None of these results has a machine-checked proof that this mission is aware of.

Difficulty

The support function of (23) is a maximisation over a set defined by a box, two nonnegative orthants and one coupled quadratic constraint. A coordinate-wise argument does not apply directly because the quadratic budget is shared. The worst case over $\mathcal P^{FB}$ is not a single distribution: the extreme mean and the extreme deviations are chosen coordinate by coordinate according to the sign of $v_i$ . The Value at Risk bound needs independence of the components; without it (22) fails. When $v=0$ or the sign pattern makes the quadratic term vanish, the dual multiplier escapes to zero and the dual minimum is only an infimum.

Formalization scope

Vectors are Fin d → ℝ, with 0-based coordinates; $\tilde u^\top v$ is u ⬝ᵥ v. The Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\varepsilon$ , and the support function is the published RobustMDP.Shared.supportFunction, a real supremum; the goal includes nonemptiness and compactness of $\mathcal U^{FB}_\varepsilon$ , so the supremum is a true maximum and cannot hold through the value $0$ of an empty or unbounded set.

The statement is formalized in the criterion form: $\mathrm{VaR}^{\mathbb P}_\varepsilon(v)\le\delta^*(v\mid\mathcal U^{FB}_\varepsilon)$ for all $v$ and every $\mathbb P$ in the region. By Theorem 1 (mission I of this series), for a nonempty convex compact set this criterion is equivalent to the probabilistic guarantee. The page's "with probability $1-\alpha$ with respect to the sample" is the coverage of the bootstrap confidence region, which the paper itself treats as approximate; it is not formalized.

Conventions and added hypotheses:

$\bar\sigma_{fi},\bar\sigma_{bi}>0$ , so that the denominators of (23) are genuine; with $\bar\sigma=0$ Lean's $x/0=0$ would leave $y_2$ unconstrained instead of forcing $y_2=0$ .
$m_b\le m_f$ , which holds because $t_i\ge0$ .
The region is built from a product measure (independence) of probability measures with bounded support. These are the hypotheses of Theorem 6 on $\mathbb P^*$ and the section's standing assumption; the page's set-builder for $\mathcal P^{FB}$ omits independence. Without bounded support, the Bochner integral of a non-integrable exponential is $0$ in Lean and the deviation conditions would lose their meaning.
" $\sigma_f(\mathbb P_i)\le\bar\sigma$ " is the predicate "the expression under the root is at most $\bar\sigma^2$ for every $x>0$ ", which is equivalent and avoids an unbounded supremum.
Dual minimisations over $\lambda\ge0$ are infima over $\lambda>0$ , stated with IsGLB.

A trivializing formalization is ruled out: a region without independence would make the goal false, a region without the probability and bounded-support conditions would let junk integrals satisfy the deviation predicates, and a support function of an empty set would make (24) a statement about $0$ .

The development needs a Chernoff argument for products of measures, finite-dimensional Lagrangian duality for one convex quadratic constraint (or a direct Cauchy–Schwarz argument), and compactness of the set (23). The definitions file is self-contained and reusable for other forward/backward-deviation sets. Proofs of any milestone, and of the Chen–Sim–Sun bound as a standalone tail inequality, are welcome.

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
X. Chen, M. Sim, P. Sun, A Robust Optimization Perspective on Stochastic Programming, Operations Research 55(6):1058–1071, 2007. https://doi.org/10.1287/opre.1070.0441

12 thms2 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization III: For Independent Marginals, the Kolmogorov–Smirnov Set U^I Has Support Function (19) and Bounds the Worst-Case Value at RiskResearch Paper

Motivation

A robust linear constraint $f(\mathbf u,\mathbf x)\le 0$ for all $\mathbf u\in\mathcal U$ replaces an uncertain parameter $\tilde{\mathbf u}$ by a deterministic uncertainty set $\mathcal U\subseteq\mathbb R^d$ . Bertsimas, Gupta and Kallus (arXiv:1401.0212v2; Math. Program. 167, 2018) build such sets directly from data. Their requirement is a probabilistic guarantee: every robust-feasible decision should satisfy the constraint with probability at least $1-\epsilon$ under the true distribution $\mathbb P^*$ , and this should hold with probability at least $1-\alpha$ over the sample. The construction runs a statistical hypothesis test, takes its confidence region of distributions, and turns the worst-case Value at Risk over that region into a set.

This mission covers the case where $\mathbb P^*$ may be continuous but its $d$ coordinates are known to be independent and supported in a known box (§5.1 of the paper). The test is the classical Kolmogorov–Smirnov (KS) goodness-of-fit test, applied separately to each marginal. The result is a convex set $\mathcal U^I_\epsilon$ whose support function has a one-dimensional closed form, (19). The set is representable with exponential cones, and a line search over a single multiplier separates over it (Remarks 6–7).

Setting

Let $d\ge 0$ and $N\ge 1$ (the sample size). For each coordinate $i$ we are given points $\hat u^{(0)}_i<\hat u^{(1)}_i<\cdots<\hat u^{(N)}_i<\hat u^{(N+1)}_i$ . The interval $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ is the known box containing the support, and $\hat u^{(1)}_i,\dots,\hat u^{(N)}_i$ are the order statistics of the $i$ -th coordinates of the data. Let $\Gamma=\Gamma^{KS}\in(0,1)$ be the KS threshold and $0<\epsilon<1$ .

The Value at Risk of $\mathbb P$ in direction $\mathbf v$ is $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)=\inf\{t:\mathbb P(\tilde{\mathbf u}^{\mathsf T}\mathbf v\le t)\ge 1-\epsilon\}$ .
The support function of a set is $\delta^*(\mathbf v\mid\mathcal U)=\sup_{\mathbf u\in\mathcal U}\mathbf v^{\mathsf T}\mathbf u$ .
The KS region $\mathcal P^{KS}_i$ is the set of Borel probability measures $\mathbb P_i$ on $[\hat u^{(0)}_i,\hat u^{(N+1)}_i]$ with $\mathbb P_i(\tilde u_i\le\hat u^{(j)}_i)\ge j/N-\Gamma$ and $\mathbb P_i(\tilde u_i<\hat u^{(j)}_i)\le (j-1)/N+\Gamma$ for $j=1,\dots,N$ .
The independent region $\mathcal P^I$ is the set of product measures $\prod_i\mathbb P_i$ with $\mathbb P_i\in\mathcal P^{KS}_i$ .
The vectors $q^L(\Gamma),q^R(\Gamma)\in\Delta_{N+2}$ of (17) are the two boundary distributions of the KS band. With $k=\lfloor N(1-\Gamma)\rfloor$ , $q^L$ puts mass $\Gamma$ at $j=0$ , mass $1/N$ at $j=1,\dots,k$ , and mass $1-\Gamma-k/N$ at $j=k+1$ . Its mirror image is $q^R_j=q^L_{N+1-j}$ .
The relative entropy is $D(\mathbf q,\mathbf p)=\sum_jq_j\log(q_j/p_j)$ .
The uncertainty set (18) is

\mathcal U^I_\epsilon=\Big\{\mathbf u:\exists\,\theta_i\in[0,1],\ \mathbf q^i\in\Delta_{N+2},\ \sum_{j=0}^{N+1}\hat u^{(j)}_iq^i_j=u_i,\ \sum_{i=1}^dD\big(\mathbf q^i,\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R\big)\le\log(1/\epsilon)\Big\}.

Formalization targets

Goal: Theorem 5 (deterministic content)

For every $\mathbf v\in\mathbb R^d$ :

\mathcal U^I_\epsilon\ \text{is nonempty, convex and compact},\qquad \mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)\ \ \forall\,\mathbb P\in\mathcal P^I,

\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)=\inf_{\lambda>0}\Big\{\lambda\log(1/\epsilon)+\lambda\sum_{i=1}^d\log\Big[\max\Big(\sum_{j}q^L_je^{v_i\hat u^{(j)}_i/\lambda},\sum_jq^R_je^{v_i\hat u^{(j)}_i/\lambda}\Big)\Big]\Big\}.\tag{19}

Milestones, in attack order

The Nemirovski–Shapiro bound $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\lambda\log(1/\epsilon)+\lambda\sum_i\log\mathbb E^{\mathbb P_i}[e^{v_i\tilde u_i/\lambda}]$ for independent, compactly supported marginals.
The boundary laws $q^L$ , $q^R$ belong to $\mathcal P^{KS}_i$ .
Theorem EC.2: for monotone $g$ , $\sup_{\mathcal P^{KS}_i}\mathbb E[g(\tilde u_i)]=\max(\sum_jq^L_jg(\hat u^{(j)}_i),\sum_jq^R_jg(\hat u^{(j)}_i))$ .
(16) combined with EC.2: the Value at Risk over $\mathcal P^I$ is at most the expression in (19), for every $\lambda>0$ .
The Lagrangian dual of $\max\{\mathbf v^{\mathsf T}\mathbf u:\mathbf u\in\mathcal U^I_\epsilon\}$ .
(EC.6): $\max_{\mathbf q\in\Delta}\{\mathbf c^{\mathsf T}\mathbf q-D(\mathbf q,\mathbf p)\}=\log\sum_jp_je^{c_j}$ .
(EC.7): the linear optimization over $\theta_i\in[0,1]$ is solved at an endpoint.

Significance

Theorem 5 gives a data-driven uncertainty set for continuous distributions with independent components. Its guarantee is finite-sample, not asymptotic, and its support function costs one line search over $\lambda$ to evaluate. Theorem 1 of the paper shows that $\mathrm{VaR}\le\delta^*$ for all $\mathbf v$ is equivalent to the probabilistic guarantee for nonempty convex compact sets. So the goal certifies that every robust-feasible solution of a constraint concave in $\mathbf u$ satisfies the chance constraint for every distribution the KS tests cannot reject. Theorem EC.2 is a reusable fact about KS bands: monotone expectations are extremized at the band's two boundary distributions.

The result is proved in the paper, but none of it has been formalized. A formal development would supply:

worst-case expectations over a KS confidence band;
the finite Gibbs variational identity with possibly vanishing reference masses;
a Chernoff-type Value-at-Risk bound for product measures;
a strong-duality statement for an entropy-constrained convex program.

Difficulty

The obvious route to the VaR bound is a union bound over coordinates. It loses a factor of $d$ in $\epsilon$ , which is why the paper uses exponential moments and independence instead. The KS region is infinite dimensional, so the inner supremum of (16) is not a finite linear program. Reducing it to the boundary distributions needs the monotonicity of $u\mapsto e^{v_iu/\lambda}$ , and a measure-level comparison of distribution functions against the band. The support-function identity needs strong duality for a jointly convex divergence constraint. The duality holds because $\theta_i\mapsto\theta_i\mathbf q^L+(1-\theta_i)\mathbf q^R$ is affine and $D$ is jointly convex. The reference vector can have zero entries (when $N(1-\Gamma)$ is an integer, or in the middle of the band), so the Gibbs step must handle vanishing masses.

Formalization scope

Data and conventions. Coordinates are Fin d. The points are uhat : Fin d → Fin (N + 2) → ℝ with the page's indices $j=0,\dots,N+1$ , and the KS constraints run over j : Fin N, which is the page's $j-1$ . The order statistics are data. They are ordered, $\hat u^{(0)}_i\le\hat u^{(1)}_i\le\dots\le\hat u^{(N+1)}_i$ (Monotone (uhat i)), as order statistics of a sample in the box are; ties are allowed.
Standing assumptions. $N\ge1$ , $0<\Gamma<1$ and $0<\epsilon<1$ .
Regions. Measures in $\mathcal P^{KS}_i$ are probability measures on $\mathbb R$ carried by the box, and $\mathcal P^I$ consists of the Measure.pi products of such measures, so independence is built in.
Relative entropy. $D$ carries an explicit finiteness predicate ( $q_j>0\Rightarrow p_j>0$ ), so Lean's log 0 = 0 cannot make an infinite divergence finite.
Published definitions. Value at Risk is the published MultistageStochastic.valueAtRisk at level $1-\epsilon$ , and $\delta^*$ is the published RobustMDP.Shared.supportFunction, a real sSup. The goal proves $\mathcal U^I_\epsilon$ nonempty and compact, so $\delta^*$ is never the junk value $0$ of an empty or unbounded set.
Infima and the multiplier. Infima over $\lambda$ are over $\lambda>0$ and stated with IsGLB. The page's $\lambda\ge0$ gives the same value.
Criterion form of the guarantee. The guarantee is stated as $\mathrm{VaR}^{\mathbb P}_\epsilon(\mathbf v)\le\delta^*(\mathbf v\mid\mathcal U^I_\epsilon)$ for all $\mathbb P\in\mathcal P^I$ . By Theorem 1 (mission I of this series), this criterion is equivalent to the probabilistic guarantee for nonempty convex compact sets.
Coverage of the test. The statement "with probability at least $1-\alpha$ over the sample" is the coverage of $\mathcal P^I$ . It rests on the distribution-free law of the KS statistic (tables) and on combining $d$ tests at level $1-\sqrt[d]{1-\alpha}$ . This part is cited, not formalized.
Ruled out. The VaR inequality is never checked against a $\delta^*$ that sSup collapses to $0$ , and the divergence budget is never relaxed by unguarded logarithms.

Contributions are welcome on any milestone. Milestones 1, 3 and 6 are independent of each other and of the rest; the goal follows from milestones 1–7 together with the convex-analytic facts about $\mathcal U^I_\epsilon$ .

Selected references

D. Bertsimas, V. Gupta, N. Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; Math. Program. 167:235–292, 2018. https://arxiv.org/abs/1401.0212
A. Nemirovski, A. Shapiro, Convex approximations of chance constrained programs, SIAM J. Optim. 17(4):969–996, 2006. https://doi.org/10.1137/050622328
M. A. Stephens, EDF statistics for goodness of fit and some comparisons, J. Amer. Statist. Assoc. 69(347):730–737, 1974. https://doi.org/10.1080/01621459.1974.10480196
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/

11 thms2 active usersReviewed

Operations Research Probability Statistics·Captain: mikedeng1

Data-Driven Robust Optimization II: With Known Finite Support, the χ² and G Uncertainty Sets Bound the Worst-Case Value at Risk over Their Confidence RegionsResearch Paper

Motivation

Robust optimization replaces uncertain data by a set of possible values and requires a decision to work for every value in that set. A central question is how to choose the set from data so that robust feasibility also gives a specified chance of satisfying the original constraint. Bertsimas, Gupta, and Kallus study this question for several sampling models in Data-Driven Robust Optimization. Their finite-support construction addresses a practical case: the uncertain vector can take one of finitely many known outcomes, while their probabilities must be inferred from observations. The resulting sets use classical goodness-of-fit tests to account for uncertainty in those probabilities. Bertsimas, Gupta, and Kallus, §§2–4, pp. 2–13.

In this case the support vectors are known in advance, so the problem is not to discover which outcomes are possible. The question is how much confidence to place in their estimated frequencies and how to turn that confidence region into a set of uncertain vectors suitable for a robust constraint. The paper gives two answers, one based on Pearson's chi-square statistic and one based on the likelihood-ratio, or G, statistic. Both answers are meant to work at every requested risk level $0<\epsilon<1$ for the same observed sample. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13.

Setting

Let $a_0,\ldots,a_{n-1}\in\mathbb R^d$ be the listed possible outcomes. A probability vector $p=(p_j)$ belongs to the simplex $\Delta_n$ when all $p_j$ are nonnegative and $\sum_jp_j=1$ . It determines the finite-support law $P_p=\sum_jp_j\delta_{a_j}$ . From a sample one obtains the empirical frequencies $\hat p\in\Delta_n$ . A nonnegative number $\rho$ records the test threshold; in the paper it is $\chi^2_{n-1,1-\alpha}/(2N)$ , where $N$ is sample size and $\alpha$ is the test's significance level. Bertsimas, Gupta, and Kallus, (10), p. 12.

The Pearson confidence region $\mathcal P^{\chi^2}$ contains candidates $p\in\Delta_n$ satisfying $\sum_j(p_j-\hat p_j)^2/(2p_j)\le\rho$ . The G confidence region $\mathcal P^G$ instead requires $D(\hat p,p)\le\rho$ , with relative entropy $D(r,p)=\sum_jr_j\log(r_j/p_j)$ . In either region, a candidate $p_j=0$ is excluded when $\hat p_j>0$ : the source's divergence is then infinite. If both entries are zero, that coordinate contributes zero. These conventions matter because ordinary real division and logarithm in Lean have total values at zero. Bertsimas, Gupta, and Kallus, (10), p. 12.

For a direction $v\in\mathbb R^d$ , value at risk $\operatorname{VaR}^{P_p}_\epsilon(v)$ is the lower $1-\epsilon$ quantile of the scalar loss $u^{\mathsf T}v$ . Conditional value at risk is the minimum over real $t$ of $t+\epsilon^{-1}\sum_jp_j(a_j^{\mathsf T}v-t)^+$ . The paper's auxiliary set $U^{\operatorname{CVaR}_{P_p}}_\epsilon$ reweights the outcomes with another probability vector $q$ constrained by $q_j\le p_j/\epsilon$ . The two data-driven uncertainty sets $U^{\chi^2}_\epsilon$ and $U^G_\epsilon$ allow such a reweighting for some $p$ in the corresponding confidence region. Their support function $\delta^*(v\mid U)$ is the largest $u^{\mathsf T}v$ over $u\in U$ . Bertsimas, Gupta, and Kallus, (11)–(13), pp. 12–13; Theorem EC.1, p. ec2.

Formalization targets

The first target is the paper's finite-support CVaR identity and the comparison between the two risk measures:

\operatorname{VaR}^{P_p}_\epsilon(v) \le \operatorname{CVaR}^{P_p}_\epsilon(v) =\delta^*(v\mid U^{\operatorname{CVaR}_{P_p}}_\epsilon).

The goal is Theorem 4's deterministic claim, simultaneously for all $0<\epsilon<1$ . For each $p$ in the relevant confidence region, it asks for both bounds

\operatorname{VaR}^{P_p}_\epsilon(v)\le\delta^*(v\mid U^{\chi^2}_\epsilon), \qquad \operatorname{VaR}^{P_p}_\epsilon(v)\le\delta^*(v\mid U^G_\epsilon)

for every $v$ , with each uncertainty set nonempty, convex, and compact. A supporting milestone identifies each support function as the supremum of CVaR over its confidence region. The paper also displays conic optimization programs for these support functions in (14) and (15); those programs are outside this mission's drafted statements. Bertsimas, Gupta, and Kallus, Theorem 4, p. 13; proof, p. ec2.

Significance

The bounds give a way to certify the directional risk of every candidate distribution accepted by a goodness-of-fit test. For a nonempty convex compact uncertainty set, the paper's Theorem 1 turns this directional condition into a probabilistic guarantee for every constraint concave in the uncertain vector. Theorem 4 adds the sampling claim through coverage of the confidence region: when the true finite-support distribution belongs to that region, the whole family indexed by $\epsilon$ receives the guarantee. The statistical tests use chi-square approximations, so their advertised coverage is asymptotic rather than an exact finite-sample result. Bertsimas, Gupta, and Kallus, Theorems 1–4, pp. 10–13.

The paper proves the mathematical result. This mission asks for machine-checked proofs of its finite-dimensional definitions, the CVaR identity, the worst-case support identities, and the deterministic risk bounds. The drafted Lean statements are open goals. A completed development would also give reusable facts about finite-support risk measures and support functions under divergence-constrained probabilities. It would leave the test coverage calculation and the explicit programs (14)–(15) for separate work.

Difficulty

The risk comparison alone does not identify a robust uncertainty set: the support function must agree with the worst-case CVaR over an entire region of probability vectors. This brings a finite-dimensional optimization identity into the formal proof, including attainment and the relationship between reweightings and distributions. Boundary coordinates create another difficulty. The Pearson expression divides by $p_j$ , and the G expression contains $\log(\hat p_j/p_j)$ ; silently accepting Lean's values at zero would enlarge the regions and change the theorem. The support function and CVaR are real infima or suprema, so their nonempty, bounded domains must also be established. Bertsimas, Gupta, and Kallus, (10)–(13), pp. 12–13; proof, p. ec2.

Formalization scope

Lean represents outcomes and probability vectors as functions on Fin d and Fin n; indices start at zero. The simplex is Mathlib's stdSimplex. The law is a finite sum of point masses. If two listed vectors coincide, their point masses aggregate; the paper's notation $p_j=P_p(\tilde u=a_j)$ is recovered with the intended distinct listing. Value at risk and the support function reuse published Prove2Me definitions; the finite-vector relative entropy also reuses a published definition, guarded at zero in this mission's G region. CVaR uses a real sInf, equal to the paper's minimum for a simplex law and $0<\epsilon<1$ . No statement applies it outside that domain.

The goal assumes $\hat p\in\Delta_n$ and $\rho\ge0$ . These express, respectively, that the center is an empirical probability vector and that the chi-square threshold is nonnegative. It quantifies over every $0<\epsilon<1$ , with the same confidence regions for all levels. The paper's sample size, chi-square quantile, and significance level are compressed into $\rho$ ; coverage of the true distribution by the test is a separate statistical premise and is not formalized here. The source's $\mathbb P^*$ is represented by $P_{p^*}$ for a supported probability vector $p^*$ . The draft does not treat an arbitrary unsupported law as a member of the confidence region.

The nonempty and compact conclusions rule out a zero returned by a support function on an empty or unbounded set. The zero-denominator guards rule out candidates the paper assigns infinite divergence. Contributions needed to close the mission include finite-simplex geometry, the finite-support CVaR identity, continuity of the divergence regions at boundary coordinates, and the risk-bound theorem. Those facts can be reused in later data-driven robust optimization developments.

Selected references

Dimitris Bertsimas, Vishal Gupta, and Nathan Kallus, Data-Driven Robust Optimization, arXiv:1401.0212v2, 2014; revised version in Mathematical Programming 167 (2018), 235–292. Preprint.

8 thms2 active usersReviewed

Operations Research Probability·Captain: mikedeng1

Optimization with Stochastic Dominance Constraints: Lagrange Multipliers of a Second-Order Dominance Constraint Are Concave Nondecreasing Utility FunctionsResearch Paper

Motivation

A decision maker choosing a random outcome $X$ (a portfolio return, a policy's cost savings, a schedule's throughput) often has a reference outcome $Y$ , the result of a benchmark policy, and wants the new outcome to be preferable to it for every risk-averse decision maker, not just on average. Expected-utility theory (von Neumann and Morgenstern) makes this precise: $X$ is preferred to $Y$ by every decision maker with a concave nondecreasing utility function $u$ exactly when $X$ dominates $Y$ in the second order, $X\succeq_{(2)}Y$ . Requiring $X\succeq_{(2)}Y$ as a constraint in an optimization problem avoids having to elicit any particular utility function, which is rarely possible in practice and impossible when several decision makers must agree.

Dentcheva and Ruszczyński (preprint 2002, published in SIAM J. Optim. 14(2), 2003) introduced optimization problems with stochastic dominance constraints and developed their optimality and duality theory. The central finding is that the Lagrange multiplier of a second-order dominance constraint is itself a concave nondecreasing utility function: the optimal solution maximizes the objective plus an expected utility, for a utility function implied by the problem. This interpretation underlies the later literature on dominance-constrained portfolio optimization, risk-averse stochastic programming, and the dual (quantile) theory of stochastic orders.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $\mathcal L^1=\mathcal L^1(\Omega,\mathcal F,P)$ the space of integrable random variables with its norm topology. For $X\in\mathcal L^1$ the distribution function is $F(X;\eta)=P[X\le\eta]$ and the second-order shortfall function is

F_2(X;\eta)=\int_{-\infty}^{\eta}F(X;\alpha)\,d\alpha,\qquad \eta\in\mathbb R. \tag{2.1}

Changing the order of integration gives $F_2(X;\eta)=\mathbb E[(\eta-X)_+]$ (2.6), where $(\cdot)_+=\max(0,\cdot)$ . The relation $X\succeq_{(2)}Y$ means $F_2(X;\eta)\le F_2(Y;\eta)$ for all $\eta$ , and $A_2(Y)=\{X\in\mathcal L^1:X\succeq_{(2)}Y\}$ .

The problem data are a reference outcome $Y\in\mathcal L^1$ , a convex closed set $C\subseteq\mathcal L^1$ , a functional $f$ that is concave and continuous on $C$ , and an interval $[a,b]$ . The paper studies the relaxation in which dominance is enforced on $[a,b]$ :

\max f(X)\quad\text{subject to}\quad\mathbb E[(\eta-X)_+]\le\mathbb E[(\eta-Y)_+]\ \ \text{for all }\eta\in[a,b],\qquad X\in C. \tag{3.1–3.3}

The uniform dominance condition (Definition 4.1) asks for some $\tilde X\in C$ with $\inf_{\eta\in[a,b]}\{F_2(Y;\eta)-F_2(\tilde X;\eta)\}>0$ .

The multiplier class $\mathcal U_1$ consists of the functions $u:\mathbb R\to\mathbb R$ that are concave and nondecreasing, vanish on $[b,\infty)$ , and are affine on $(-\infty,a]$ : $u(t)=u(a)+c(t-a)$ for $t\le a$ , with a constant $c\ge0$ . The Lagrangian is

L(X,u)=f(X)+\mathbb E[u(X)]-\mathbb E[u(Y)]. \tag{4.1}

Formalization targets

Goal: Theorem 4.2

Assume the uniform dominance condition. If $\hat X$ is an optimal solution of (3.1)–(3.3), there is $\hat u\in\mathcal U_1$ with

L(\hat X,\hat u)=\max_{X\in C}L(X,\hat u)\quad(4.2)\qquad\text{and}\qquad\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)].\quad(4.3)

Conversely, if for some $\hat u\in\mathcal U_1$ a maximizer $\hat X\in C$ of $L(\cdot,\hat u)$ satisfies (3.2) and (4.3), then $\hat X$ is optimal for (3.1)–(3.3).

Milestones

The milestones follow the paper's proof. They are: finiteness of $\mathbb E[u(X)]$ for $u\in\mathcal U_1$ ; the identity (2.6), already proved on the platform; Proposition 2.3 (convexity and closedness of $A_2(Y)$ , and its recession cone); the concavity of the constraint operator $G(X)(\eta)=F_2(Y;\eta)-F_2(X;\eta)$ with respect to the cone of nonnegative functions; the existence of a nonnegative measure multiplier $\hat\mu$ on $[a,b]$ satisfying (4.5)–(4.6); the facts that the function $u_\mu(t)=-\int_t^b\mu([\tau,b])\,d\tau$ ( $t<b$ ), $u_\mu(t)=0$ ( $t\ge b$ ) of a nonnegative measure lies in $\mathcal U_1$ and that every $u\in\mathcal U_1$ is $u_\mu$ for exactly one $\mu$ ; the key identity

\int_a^b F_2(X;\eta)\,d\mu(\eta)=-\mathbb E[u_\mu(X)]; \tag{4.9}

and the weak-duality step: (3.2) implies $\mathbb E[u(X)]\ge\mathbb E[u(Y)]$ for every $u\in\mathcal U_1$ .

Further: Theorem 5.1

With $D(u)=\sup_{X\in C}L(X,u)$ , the dual problem $\min_{u\in\mathcal U_1}D(u)$ has a solution, its value equals the primal optimal value, and its solutions are exactly the $\hat u\in\mathcal U_1$ satisfying (4.2)–(4.3).

Significance

Theorem 4.2 turns an infinite family of constraints, one for each $\eta\in[a,b]$ , into a single scalar trade-off: at the optimum, the decision maker behaves as an expected-utility maximizer for an implicit utility $\hat u$ , and the dominance constraint is active exactly in the sense $\mathbb E[\hat u(\hat X)]=\mathbb E[\hat u(Y)]$ . Theorem 5.1 makes $\mathcal U_1$ the space of dual variables, which is the starting point of dual decomposition and cutting-plane methods for dominance-constrained problems and of their extensions to several constraints and to higher orders (Sections 6–7 of the paper, not part of this mission).

All results are proved in the paper. Apart from the identity (2.6), which is proved on the platform, none of them is formalized as far as the platform records show. A machine-checked development would provide, on top of the paper, a rigorous treatment of the measure–utility correspondence that the paper obtains from a textbook theorem "after an obvious adaptation", and a careful account of the multiplier class itself (see the scope section on the constant $c$ ). The definitions of $F_2$ and of the identity (2.6) are shared with the platform's missions on Dual Stochastic Dominance and Related Mean-Risk Models (Ogryczak and Ruszczyński, 2002).

Difficulty

The necessity half needs a Lagrange multiplier for a constraint taking values in the infinite-dimensional space $\mathcal C([a,b])$ ; finite-dimensional convex duality does not apply, and the multiplier first appears as a nonnegative measure on $[a,b]$ , an element of the dual of $\mathcal C([a,b])$ . A Slater-type point is required: without the uniform dominance condition the multiplier may not exist. This is why the dominance relation, which the paper first poses on all of $\mathbb R$ , is relaxed to a bounded interval $[a,b]$ : for a reference outcome with a smallest value $y_1$ , $F_2(Y;y_1)=0$ , so no $\tilde X$ can dominate $Y$ strictly near $y_1$ .

The second obstacle is the translation of that measure into a utility function. The identity (4.9) requires an interchange of integrals over $\mathbb R\times[a,b]$ and an integration by parts against the distribution function of an arbitrary integrable $X$ , followed by a limit in which the integrability of $X$ controls the linear growth of $u$ at $-\infty$ . The converse direction needs every $u\in\mathcal U_1$ to be represented by a unique measure, through the left derivative of a concave function.

Formalization scope

Outcomes are elements of Mathlib's $L^1$ space Ω →₁[P] ℝ over a probability measure P, coerced to functions inside integrals; no statement is pointwise in $\omega$ . $F_2$ is the published definition DualSSD.Shared.secondPerformance, a Bochner integral of $P[X\le\alpha]$ over $(-\infty,\eta]$ . The problem data form a structure whose fields include every standing assumption of the paper: $C$ convex and closed, $f$ concave and continuous on $C$ . The constraint (3.2) is stated in its printed expectation form, while Definition 4.1 and the proof objects use $F_2$ , as printed; their equality is (2.6).

Committed conventions:

$\mathcal U_1$ uses $c\ge0$ . The paper prints $c>0$ . With $c>0$ the necessity half of Theorem 4.2 is false: take $Y\equiv0$ , $[a,b]=[1,2]$ , $f(X)=\mathbb EX$ and $C$ the constant random variables with values in $[0,1]$ . Then $\tilde X\equiv1$ satisfies Definition 4.1, $\hat X\equiv1$ is optimal, and (4.3) forces $c=0$ . The proof itself produces $c=\mu([a,b])$ , which vanishes for the zero multiplier of a slack constraint, and the paper calls $\mathcal U_1$ a convex cone, which must contain $0$ .
Definition 4.1's infimum is encoded as a positive lower bound $\varepsilon$ on $[a,b]$ . " $=\max_{X\in C}$ " is encoded as membership in $C$ plus an upper bound over $C$ .
A nonnegative measure in $\mathbf{rca}([a,b])$ is a finite Borel measure on $\mathbb R$ giving zero mass to the complement of $[a,b]$ , which is the paper's own extension by zero. Integrals $\int_a^b\cdot\,d\mu$ are over the closed interval, so atoms at $a$ and $b$ count.
No relation between $a$ and $b$ is assumed. For $a>b$ every statement remains meaningful: the constraint is vacuous and $\mathcal U_1=\{0\}$ .
Theorem 5.1's dual function takes values in the extended reals.

A trivializing formalization is ruled out: a junk-valued expectation (a Bochner integral of a non-integrable function, which Lean sets to $0$ ) cannot occur for $u\in\mathcal U_1$ , and its integrability is a milestone. Dropping the concavity of $f$ or the convexity of $C$ would make the necessity half false, so these assumptions are fields of the problem data.

Infrastructure a complete development needs: convex duality for cone constraints in $\mathcal C([a,b])$ (or a direct separation argument in $\mathbb R\times\mathcal C([a,b])$ ), the Riesz representation of nonnegative functionals on $\mathcal C([a,b])$ , Fubini and integration by parts for Stieltjes measures, and the measure of a left-continuous monotone function. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The extensions to several dominance constraints and to higher-order dominance are not included.

Selected references

D. Dentcheva and A. Ruszczyński, Optimization with stochastic dominance constraints, preprint dated December 27, 2002 (Stochastic Programming E-Print Series); published in SIAM Journal on Optimization 14(2):548–566, 2003. https://doi.org/10.1137/S1052623402420528
W. Ogryczak and 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
J. F. Bonnans and A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.

13 thms2 active usersReviewed

Linear Optimization Operations Research·Captain: mikedeng1

Robust Solutions of Uncertain Linear Programs I: Under Constraint-wise Uncertainty and the Boundedness Assumption the Robust Counterpart Is No Worse Than the Worst InstanceResearch Paper

Motivation

A linear program is solved with data that, in practice, is rarely known exactly: coefficients come from measurements, estimates or forecasts. Robust optimization asks for a solution that remains feasible for every realization of the data in a prescribed uncertainty set, and among those the one with the best guaranteed objective value. Ben-Tal and Nemirovski introduced this framework for linear programming in Robust solutions of uncertain linear programs (Oper. Res. Lett. 25, 1999), following their treatment of robust convex optimization (Math. Oper. Res. 23, 1998) and Soyster's earlier work on inexact linear programming (Oper. Res. 21, 1973). The robust counterpart has since become the starting point of a large literature on uncertainty sets, budgets of uncertainty and adjustable policies.

A natural first objection is that the robust counterpart might be needlessly conservative: by demanding feasibility for all realizations simultaneously, it could be infeasible, or have a worse value, even when every individual realization is perfectly well behaved. This mission formalizes the paper's answer (§2.2): under two structural hypotheses, the robust counterpart is no worse than the worst realization.

Setting

Fix $c, f \in \mathbb R^n$ and write a linear program in the homogeneous form (6)

(P)\qquad \min\{c^{T}x \mid Ax \ge 0,\ f^{T}x = 1\},

where $A$ is a real $m\times n$ matrix and $Ax\ge0$ is componentwise. Every linear program can be put in this form. The matrix $A$ is uncertain: it is only known to lie in an uncertainty set $\mathcal U$ of $m\times n$ matrices. Each $A\in\mathcal U$ gives an instance $(P)$ with feasible set $\{x\mid Ax\ge0,\ f^{T}x = 1\}$ and optimal value $c^*(P)$ ; the family of instances is $\mathcal P$ . The robust counterpart (7) is

(P_{\mathcal U})\qquad \min\{c^{T}x \mid x \in G_{\mathcal U}\},\qquad G_{\mathcal U} = \{x\mid Ax\ge0\ \ \forall A\in\mathcal U;\ f^{T}x = 1\},

and its optimal value is $c^*$ . Since $G_{\mathcal U}$ does not change when $\mathcal U$ is replaced by its closed convex hull, the paper assumes throughout that $\mathcal U$ is convex and closed.

Let $\mathcal U_i\subseteq\mathbb R^n$ be the set of all realizations of the $i$ -th row, the projection of $\mathcal U$ onto the data of the $i$ -th constraint. The uncertainty is constraint-wise if $\mathcal U = \mathcal U_1\times\dots\times\mathcal U_m$ : the rows vary independently. The Boundedness Assumption asks for a convex compact set $Q\subseteq\mathbb R^n$ that contains the feasible set of every instance.

Formalization targets

Goal: Proposition 2.1 (p. 5)

If the uncertainty is constraint-wise and the Boundedness Assumption holds, then

$(P_{\mathcal U})$ is infeasible if and only if some instance is infeasible:

G_{\mathcal U} = \emptyset \iff \exists A\in\mathcal U:\ \{x\mid Ax\ge0,\ f^{T}x=1\}=\emptyset;

if $(P_{\mathcal U})$ is feasible with optimal value $c^*$ , then

c^* = \sup\{c^*(P)\mid (P)\in\mathcal P\}. \tag{9}

Milestones

The milestones follow the paper's proof: the row-wise description (8) of robust feasibility; the inclusion of $G_{\mathcal U}$ in every instance's feasible set; the reduction of the semi-infinite system (8) on $Q$ to a finite subsystem; the statement that the finite system (10) $A_1x\ge0,\dots,A_Nx\ge0,\ f^{T}x=1$ then has no solution at all; the Farkas certificate (11); the construction of one infeasible instance from it; and part (i) alone, which part (ii) uses for an augmented program.

Companions

The §2.2 example (every instance has optimal value 1, the robust counterpart is infeasible), and the two invariance remarks: $G_{\mathcal U}$ is unchanged under passing to the closed convex hull of $\mathcal U$ (§2.1) or to the product $\mathcal U_1\times\dots\times\mathcal U_m$ of its projections (§2.2).

Significance

Proposition 2.1 says that, for constraint-wise uncertainty, robustness costs nothing beyond what the worst realization already costs: the robust counterpart is feasible exactly when every instance is, and its optimal value equals the worst instance value. The §2.2 example shows the hypothesis cannot be dropped: there, correlated uncertainty in two rows makes every instance solvable with value 1 while the robust counterpart is infeasible. Together with the invariance of $G_{\mathcal U}$ under passing to the product of projections, this explains why row-wise (constraint-wise) uncertainty sets are the standard modelling choice in robust linear optimization.

The result is proved in the paper; no machine-checked version is known to exist. Formalizing it produces a reusable development of semi-infinite linear systems: the compactness reduction to finite subsystems, a homogeneous Farkas alternative, and the row-averaging argument that uses convexity and the product structure of $\mathcal U$ .

Difficulty

The robust counterpart has a continuum of constraints, one for each $A\in\mathcal U$ , so Farkas' Lemma cannot be applied to it directly. The step that requires care is passing from infeasibility of this semi-infinite system to infeasibility of a single instance. Compactness yields only finitely many instances whose joint system has no solution in $Q$ ; those instances are in general all feasible individually, and the infeasible instance has to be manufactured from their rows. Without constraint-wise uncertainty the manufactured matrix need not lie in $\mathcal U$ , which is exactly what the §2.2 example exploits. Part (ii) needs the optimal values of the instances to be attained on compact feasible sets, which is where the Boundedness Assumption enters again.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, and $Ax\ge0$ is 0 ≤ A *ᵥ x in the componentwise order. The $i$ -th row of $A$ is A i and $a^{T}x$ is a ⬝ᵥ x. The projections $\mathcal U_i$ are the images of $\mathcal U$ under $A\mapsto A_i$ , not free sets, and constraint-wise uncertainty is the inclusion $\mathcal U_1\times\dots\times\mathcal U_m\subseteq\mathcal U$ (the reverse inclusion always holds). The Boundedness Assumption keeps both convexity and compactness of $Q$ , as on the page.

Optimal values are infima: $c^*$ is the greatest lower bound (IsGLB) of $c^{T}x$ over $G_{\mathcal U}$ , and (9) states that $c^*$ is the least upper bound (IsLUB) of the set of real optimal values of the instances. No real sInf/sSup is used, so no junk value can make the statement true.

The goal carries the paper's standing assumption that $\mathcal U$ is convex and closed, and one disclosed addition: $\mathcal U$ is nonempty. The paper takes this for granted; without it part (i) fails for $f = 0$ and the supremum in (9) ranges over the empty set. The goal does not assume that the robust counterpart or any instance attains its optimum, and it does not mention finite subsystems, multipliers or the averaged matrix; those appear only in the milestones. A formalization in which the uncertainty sets $\mathcal U_i$ are arbitrary sets with $\mathcal U = \prod_i\mathcal U_i$ , or in which optimal values are taken as sInf without boundedness, would not be faithful and is ruled out.

A complete development needs: compactness arguments for families of closed half-spaces, a Farkas alternative for homogeneous systems with one normalizing equation, and elementary convexity of linear images. These pieces are general and reusable beyond robust optimization. Proofs of the milestones, alternative arguments (for instance via LP duality for part (ii)) and proofs of the companion statements are welcome.

Selected references

A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Operations Research Letters 25(1):1–13, 1999. https://doi.org/10.1016/s0167-6377(99)00016-4 (cited here by the pages of the authors' manuscript).
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Operations Research 21(5):1154–1157, 1973. https://doi.org/10.1287/opre.21.5.1154

9 thms2 active usersReviewed

Numerical Analysis Optimization·Captain: mikedeng1

The Relaxation Method of Finding the Common Point of Convex Sets and Its Application to the Solution of Problems in Convex Programming 2: Under Remotest-Set Control Every Limit Point Is CommonResearch Paper

Motivation

Many problems in optimization, image reconstruction and statistics reduce to the convex feasibility problem: given closed convex sets $A_i$ , $i\in I$ , find a point of their intersection $R=\bigcap_{i\in I}A_i$ . A classical approach is the relaxation method: from the current point, move to the nearest point of one of the sets, and repeat. For Euclidean distance and half-spaces this is the method of Agmon and of Motzkin and Schoenberg (1954); for hyperplanes it is Kaczmarz's method.

L. M. Bregman's 1967 paper replaced the Euclidean distance by an abstract function $D(x,y)$ satisfying six conditions. The resulting D-projections include what are now called Bregman projections, and the paper is the origin of the Bregman divergence $D(x,y)=f(x)-f(y)-\langle\nabla f(y),x-y\rangle$ , used today in mirror descent, entropy maximization and the theory of row-action methods (Censor and Zenios, 1997).

The paper proves convergence for two rules for choosing which set to project onto. This mission covers the second one, Theorem 2: always project onto the set that is farthest from the current point in the sense of $D$ (the "remotest-set" or maximal-distance control).

Setting

Let $X$ be a real linear topological space and $(A_i)_{i\in I}$ a family of closed convex subsets of $X$ ; the index set $I$ is arbitrary and may be infinite. Let $S\subseteq X$ be convex with $S\cap R\ne\emptyset$ , and let $D:S\times S\to\mathbb R$ satisfy:

(I) $D(x,y)\ge0$ , with equality if and only if $x=y$ ;
(II) for every $i$ and $y\in S$ there is a point $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$ , the D-projection of $y$ onto $A_i$ ;
(III) $z\mapsto D(z,y)-D(z,P_iy)$ is convex on $A_i\cap S$ ;
(IV) $D(y+tz,y)/t\to0$ as $t\to0$ ;
(V) for each $z\in R\cap S$ and real $L$ , the set $\{x\in S: D(z,x)\le L\}$ is compact;
(VI) if $D(x^n,y^n)\to0$ , $y^n\to y^*\in\overline S$ , and $\{x^n\}$ lies in a compact set, then $x^n\to y^*$ .

A relaxation sequence starts at $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$ ; the sequence of indices $(i_n)$ is the control. The control is remotest-set if at every step $i_n$ realizes

\max_{j\in I}\ \min_{x\in A_j}D(x,x^n)=\max_{j\in I}D(P_jx^n,x^n).

In the Lean development these objects are DConditions A S D P (conditions I–IV and VI), CondV S D ((⋂ j, A j) ∩ S) (condition V), IsRelaxSeq S P i x (in the series' shared namespace BregmanRelax.Cyclic) and IsRemotestControl D P i x (in BregmanRelax.Remotest).

Formalization targets

Goal: Theorem 2 (p. 203)

For every remotest-set control and every relaxation sequence it generates, every limiting point is a common point:

x^{n_k}\to x^*\ \Longrightarrow\ x^*\in\bigcap_{i\in I}A_i .

Milestones

Lemma 1 (pp. 201–202): for $z\in A_i\cap S$ and $y\in S$ , $D(P_iy,y)\le D(z,y)-D(z,P_iy)$ .
Lemma 2 (p. 202), for any control: (1) the iterates lie in a compact set; (2) $\lim_n D(z,x^n)$ exists for each $z\in R\cap S$ ; (3) $D(x^{n+1},x^n)\to0$ .

Significance

Theorem 2 is the first convergence result for greedy (most-violated-constraint) selection in projection methods with a non-Euclidean distance. Unlike the cyclic Theorem 1 of the same paper, it applies to infinite families of sets, which covers semi-infinite systems of convex inequalities. Lemma 1, the generalized Pythagorean inequality, is the basic estimate for Bregman projections and recurs throughout mirror-descent and row-action analyses; Lemma 2 records the Fejér-type monotonicity of the iterates with respect to $D$ .

The results are classical and proved in the paper. To our knowledge they are not formalized in Lean or another proof assistant at this level of generality. The mission produces a machine-checked version of the abstract D-projection framework, with the conditions stated so that the Bregman divergence of §2 of the paper, and the Euclidean distance, are instances.

Difficulty

The obvious argument for Euclidean projections uses Fejér monotonicity and the fact that a bounded sequence in $\mathbb R^p$ has convergent subsequences. Here neither the triangle inequality nor symmetry of $D$ is available, and $X$ need not be normed or finite-dimensional. The remotest-set rule controls only the D-distance $D(P_jx^n,x^n)$ from the iterate to each projection, in that argument order; turning "these distances tend to zero along a subsequence" into "the limit lies in every $A_j$ " requires the interplay of conditions V and VI, and it must hold uniformly over a possibly infinite index set.

Formalization scope

Conventions committed to in Lean:

The D-projection is a fixed map $P:I\to X\to X$ ; condition II says $P_iy$ is a minimizer over $A_i\cap S$ . The paper's misprint in II (" $\min_{z\in A_i\cap S}D(z,x)$ ", " $i\in T$ ") is read as $\min D(z,y)$ , $i\in I$ .
Condition IV is assumed only as a vanishing right derivative at $y\in S$ in directions $w-y$ with $w\in S$ . The paper's IV implies this, so the theorems are at least as strong as the paper's.
"Compact" in V, VI and Lemma 2 (1) is sequential compactness (the proofs extract convergent subsequences); "the set of elements of $\{x^n\}$ is compact" means all $x^n$ lie in one sequentially compact set.
"Limiting point" is the limit of a subsequence $x^{\varphi(k)}$ with $\varphi$ strictly increasing.
The paper assumes that $\max_i\min_{x\in A_i}D(x,y)$ exists for each $y\in S$ , so that a remotest-set control exists. The goal is stated for every control with the maximizing property, which covers every choice of maximizer; the existence assumption is therefore not a hypothesis.
The index type is arbitrary: no finiteness is assumed. No Hausdorff assumption on $X$ is made.
$D$ is a total function $X\to X\to\mathbb R$ , but every condition and every statement only evaluates it on $S\times S$ .

A trivializing formalization is ruled out: the hypotheses are jointly satisfiable with a genuine run (in $\mathbb R$ with $D(x,y)=(x-y)^2$ , $A_0=[0,1]$ , $A_1=[1,2]$ , and $x^0=3$ ), checked locally without sorry, so neither the goal nor the lemmas holds vacuously.

A complete development needs subsequence extraction from sequentially compact sets, one-sided limits of difference quotients, and monotone convergence of real sequences — all available in Mathlib. The D-projection framework, Lemma 1 and Lemma 2 are shared with the cyclic-control mission of the same paper and are reusable for any Bregman-projection algorithm. Proofs of the lemmas, of Theorem 2, and of the instance showing the Euclidean distance satisfies conditions I–VI are welcome.

Selected references

L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3), 200–217, 1967. https://doi.org/10.1016/0041-5553(67)90040-7
T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6, 393–404, 1954. https://doi.org/10.4153/CJM-1954-038-x
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6, 382–392, 1954. https://doi.org/10.4153/CJM-1954-037-2
Y. Censor and S. A. Zenios, Parallel Optimization: Theory, Algorithms, and Applications, Oxford University Press, 1997, ISBN 978-0-19-510062-4.

7 thms2 active usersReviewed

Machine Learning Optimization Probability+1·Captain: mikedeng1

Variance-based Regularization with Convex Objectives IV: Fast Rates for Approximate Robust Minimizers under a Growth ConditionResearch Paper

Motivation

In stochastic optimization and statistical learning one chooses a parameter $\theta$ from a set $\Theta\subseteq\mathbb R^d$ to make the risk $R(\theta)=\mathbb E_P[\ell(\theta;X)]$ small, having seen only a sample $X_1,\dots,X_n$ from $P$ . Generalization bounds suggest trading empirical risk against its standard deviation, but the variance-penalized objective is non-convex even for convex losses. Duchi and Namkoong (arXiv:1610.02581v3) replace it by the robustly regularized risk, the worst-case expected loss over a $\chi^2$ -divergence ball around the empirical distribution. This objective is convex whenever $\ell$ is, and it agrees with the variance-penalized objective up to a small error.

When the risk has curvature near its minimizers, empirical risk minimization attains rates faster than $1/\sqrt n$ (Bartlett, Bousquet and Mendelson 2005; Shapiro, Dentcheva and Ruszczyński 2009). Section 4.1 of the paper asks whether minimizers of the robust risk, which carry an extra variance-dependent penalty of order $\sqrt{\rho/n}$ , keep these fast rates. Its Theorem 5 answers yes, and does so for approximate minimizers, which is what iterative solvers return.

Setting

A loss $\ell:\mathbb R^d\times\mathcal X\to\mathbb R$ is fixed, with $\ell(\cdot;x)$ convex and $L$ -Lipschitz on a convex set $\Theta$ for every $x$ , and $\ell(\theta;\cdot)$ integrable. The risk is $R(\theta)=\mathbb E_P[\ell(\theta;X)]$ .

For a radius $\rho\ge0$ , the $\chi^2$ ball around the empirical distribution $\widehat P_n$ is the set of weight vectors

\mathcal P_n=\Big\{p\in\mathbb R^n_+:\tfrac12\|np-\mathbf 1\|_2^2\le\rho,\ \langle\mathbf 1,p\rangle=1\Big\},

and the robust risk is $R_n(\theta,\mathcal P_n)=\sup_{p\in\mathcal P_n}\sum_i p_i\,\ell(\theta;X_i)$ .

For $\epsilon\ge0$ the $\epsilon$ -suboptimal sets of the risk and of the robust risk are

S_\star^\epsilon=\{\theta\in\Theta:R(\theta)\le\inf_\Theta R+\epsilon\},\qquad\widehat S_\star^\epsilon=\{\theta\in\Theta:R_n(\theta,\mathcal P_n)\le\inf_\Theta R_n(\cdot,\mathcal P_n)+\epsilon\},

with $S_\star=S_\star^0$ the solution set and $\pi_{S_\star}$ the Euclidean projection onto it. The risk satisfies a growth condition of order $\gamma>1$ if, for some $\lambda>0$ and $r>0$ ,

R(\theta)-\inf_\Theta R\ \ge\ \lambda\,\mathrm{dist}(\theta,S_\star)^\gamma\quad\text{whenever }\mathrm{dist}(\theta,S_\star)\le r.\tag{26}

The complexity of the problem enters through the localized class $\{x\mapsto\ell(\theta;x)-\ell(\pi_{S_\star}(\theta);x):\theta\in A\}$ and its empirical Rademacher complexity $\mathfrak R_n(A)=\mathbb E_\varepsilon\big[\sup_{\theta\in A}\frac1n\sum_i\varepsilon_i(\ell(\theta;X_i)-\ell(\pi_{S_\star}(\theta);X_i))\big]$ , with independent uniform signs $\varepsilon_i\in\{\pm1\}$ .

Formalization targets

Goal: Theorem 5 (p. 19)

For $t>0$ , $\rho\ge0$ , and $0<\epsilon\le\frac12\lambda r^\gamma$ satisfying

\epsilon\ge\Big(2\frac{8^\gamma L^\gamma}{\lambda}\Big)^{\frac1{\gamma-1}}\Big(\frac\rho n\Big)^{\frac\gamma{2(\gamma-1)}}\quad\text{and}\quad\frac\epsilon2\ge2\,\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+L\Big(\frac{2\epsilon}\lambda\Big)^{\frac1\gamma}\sqrt{\frac{2t}n},\tag{27}

\mathbb P\big(\widehat S_\star^\epsilon\subset S_\star^{2\epsilon}\big)\ \ge\ 1-e^{-t}.

Milestones, in attack order

Localization (p. 44). Under (26), $S_\star^{2\epsilon}$ lies in $\{\theta\in\Theta:\mathrm{dist}(\theta,S_\star)\le(2\epsilon/\lambda)^{1/\gamma}\}$ .
Theorem 1, upper half of (10) (p. 7). $\sup_{p\in\mathcal P_n}\langle p,z\rangle-\bar z\le\sqrt{2\rho s_n^2/n}$ for every $z\in\mathbb R^n$ .
Claim E.1 (p. 44). If $\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon}$ , the localized deviation $\Delta_n$ plus a variance term reaches $\epsilon$ somewhere on $S_\star^{2\epsilon}$ .
Display (43) (p. 45). $\mathbb P(\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon})\le\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge\epsilon/2)$ .
Concentration (p. 45). $\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge2\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+u)\le\exp(-\frac{nu^2}{2L^2}(\frac\lambda{2\epsilon})^{2/\gamma})$ .

Significance

The theorem says that the variance penalty implicit in the robust objective does not cost the fast rates available under curvature. The $\rho$ -dependent condition in (27) is of order $(\rho/n)^{\gamma/(2(\gamma-1))}$ , which for quadratic growth ( $\gamma=2$ ) is $\rho/n$ , the same order as the localized complexity term in typical parametric problems. Corollary 4.1 of the paper derives explicit rates of order $\frac dn\log\frac nd+\frac tn+\frac\rho n$ from it for a unique minimizer. The result applies to $\epsilon$ -approximate minimizers, so it covers the output of the stochastic-gradient methods used to solve the robust problem.

The result is proved in the paper (Appendix E). None of it is formalized: no statement about growth conditions, localized deviations of a robust objective, or fast rates for robust minimizers is on Prove2Me. A formal proof would check the printed constants, settle the boundary case $\epsilon=0$ (see below), and produce a localization lemma and a reduction from approximate robust minimizers to empirical processes that apply to other estimators.

Difficulty

The obvious argument fails at two points. First, a uniform deviation bound over all of $\Theta$ gives only the $1/\sqrt n$ rate: the speed-up comes from localizing to $S_\star^{2\epsilon}$ , which requires transferring the growth condition, assumed only within distance $r$ of $S_\star$ , to every $2\epsilon$ -suboptimal point by convexity. Second, the robust risk is not an empirical average, so standard comparisons between empirical and population minimizers do not apply. Claim E.1 handles this by moving along the segment from a bad approximate minimizer to its projection, which needs the projection to be preserved along that segment (a normal-cone property of $\pi_{S_\star}$ ) and the risk to be continuous there. The robust–empirical gap is then controlled by the variance expansion of Theorem 1. The concentration step needs a bounded-differences inequality for a supremum over an uncountable class, together with symmetrization; neither is in Mathlib in this form.

Formalization scope

Parameters live in EuclideanSpace ℝ (Fin d), so norms, distances and projections are Euclidean. The sample is the coordinate process of the product measure $P^{\otimes n}$ on Fin n → X, $n\ge1$ , and probabilities are measures of sample sets (the outer measure for a set that is not measurable). The $\chi^2$ ball is the weight-vector form (8). The suboptimal sets are written without infima ( $R(\theta)\le R(\theta')+\epsilon$ for all $\theta'\in\Theta$ ). Each supremum " $\sup\ge c$ " is written as "for every $\delta>0$ some $\theta$ reaches $c-\delta$ ", so no statement relies on the default value of a real supremum. The Rademacher complexity is the published UnderstandingML.rademacher, and its expectation over the sample is assumed integrable, so that it is the true expectation and not the default value $0$ of a Bochner integral. Lipschitz continuity is required on $\Theta$ , as printed.

Corrections and presuppositions:

$\epsilon>0$ . The paper prints $0\le\epsilon$ . At $\epsilon=0$ , $\rho=0$ , both conditions of (27) hold, yet for $\ell(\theta;x)=\frac12(\theta-x)^2$ on $\Theta=[-1,1]$ with $X$ uniform on $[-\frac12,\frac12]$ the robust minimizer is the sample mean, which is almost surely not in $S_\star=\{0\}$ . The proof divides by $\epsilon$ (p. 45). The goal is stated for $\epsilon>0$ .
$S_\star$ nonempty and closed are assumed. The projection $\pi_{S_\star}$ presupposes them, and Appendix E calls $S_\star$ closed.
Only the upper half of Theorem 1's (10) is stated; it needs no boundedness of the values.

The constant $\big(2\cdot8^\gamma L^\gamma/\lambda\big)^{1/(\gamma-1)}$ is the printed one; the proof uses a smaller one, which the printed condition implies. The hypotheses $\epsilon>0$ , $\gamma>1$ and $\lambda>0$ make every power well defined. A formalization that assumed (26) vacuously, took $\epsilon=0$ , or let the Rademacher term be a non-integrable Bochner integral would trivialize the goal; the statements rule these out.

Infrastructure: Euclidean projection onto closed convex sets and its normal-cone characterization (partly in Mathlib), convexity of integral functionals, McDiarmid's bounded-differences inequality, and symmetrization for suprema of empirical processes. The concentration tools and the localization lemma can be reused beyond this mission. Contributions toward McDiarmid's inequality and symmetrization are especially welcome.

Selected references

J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT, 2009. https://arxiv.org/abs/0907.3740

12 thms2 active usersReviewed

Numerical Analysis Optimization·Captain: mikedeng1

The Relaxation Method of Finding the Common Point of Convex Sets and Its Application to the Solution of Problems in Convex Programming 1: Under Cyclic Control Every Limit Point Is a Common PointResearch Paper

Motivation

Many problems in optimization and numerical analysis reduce to finding a point in the intersection of finitely many closed convex sets: solving a system of linear equations or inequalities, reconstructing an image from projections, or finding a feasible point of a convex program. The classical methods for this convex feasibility problem project the current point onto one set at a time, in Euclidean distance: Kaczmarz (1937) for linear equations, Agmon and Motzkin–Schoenberg (1954) for linear inequalities, and the cyclic projection method for general convex sets studied by Gubin, Polyak and Raik (1967).

L. M. Bregman's 1967 paper replaces the Euclidean distance by a general function $D(x,y)$ satisfying a short list of axioms, and shows that the projection method still works. The functions $D(x,y)=f(x)-f(y)-\langle\nabla f(y),x-y\rangle$ built from a strictly convex $f$ are the ones now called Bregman divergences, and the paper is the origin of Bregman projections, of the row-action methods of Censor and collaborators, and indirectly of mirror descent. Its §2 uses the abstract result to solve convex programs with linear constraints by relaxation.

This mission formalizes §1 of the paper for the cyclic control, in which the sets are visited in a fixed round-robin order. A companion mission treats the remotest-set control of Theorem 2, and two further missions treat the convex-programming results of §2.

Setting

Let $X$ be a real linear topological space and $A_0,\dots,A_{m-1}$ closed convex subsets of $X$ , with intersection $R=\bigcap_i A_i$ . Let $S\subset X$ be a convex set with $S\cap R\ne\emptyset$ , and let $D:S\times S\to\mathbb R$ . The paper requires:

I. $D(x,y)\ge 0$ , with equality if and only if $x=y$ .
II. For every $y\in S$ and every $i$ there is a point $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$ ; it is the $D$ -projection of $y$ onto $A_i$ .
III. For every $i$ and $y\in S$ , the function $z\mapsto D(z,y)-D(z,P_iy)$ is convex on $A_i\cap S$ .
IV. $D(\cdot,y)$ has derivative $0$ at the point $y$ .
V. For every $z\in R\cap S$ and real $L$ , the sublevel set $\{x\in S\mid D(z,x)\le L\}$ is compact.
VI. If $D(x^n,y^n)\to 0$ , $y^n\to y^*\in\bar S$ , and $\{x^n\}$ lies in a compact set, then $x^n\to y^*$ .

The relaxation sequence with control $(i_n)$ starts at any $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$ . Under the cyclic control $i_n=n\bmod m$ , the sets are projected onto in the order $A_0,A_1,\dots,A_{m-1},A_0,\dots$ . A limiting point of $\{x^n\}$ is the limit of a convergent subsequence $x^{n_k}$ .

The Lean development uses the namespace BregmanRelax.Cyclic: DConditions A S D P bundles conditions I–IV and VI together with the closedness and convexity of the sets, CondV S D Z is condition V for the points of $Z$ , IsRelaxSeq S P i x is the relaxation sequence with control $i$ , and cyclicControl hm is $n\mapsto n\bmod m$ .

Formalization targets

Goal: Theorem 1 (p. 203)

Under conditions I–VI, with the cyclic control, every limiting point of every relaxation sequence lies in every set:

x^{n_k}\to x^* \quad\Longrightarrow\quad x^*\in\bigcap_{i=0}^{m-1}A_i .

The statement is about every starting point $x^0\in S$ and every convergent subsequence. It does not assert that the whole sequence converges.

Milestones

Lemma 1 (pp. 201–202): for $z\in A_i\cap S$ and $y\in S$ ,

D(P_iy,y)\le D(z,y)-D(z,P_iy).

Lemma 2 (2) (p. 202): for any control and any $z\in R\cap S$ , $\lim_{n\to\infty}D(z,x^n)$ exists.
Lemma 2 (3) (p. 202): for any control, $D(x^{n+1},x^n)\to 0$ .
Lemma 2 (1) (p. 202): for any control, $\{x^n\}$ lies in a compact set.

Further result: Note 1, condition (1) (pp. 204–205)

For any control whose relaxation sequence has all its limiting points in $R$ (the cyclic control, by Theorem 1), if in addition $S$ is closed and $y\mapsto D(z_1,y)-D(z_2,y)$ is continuous on $S$ for all $z_1,z_2\in R\cap S$ , then the relaxation sequence converges to a point of $R$ .

Significance

Theorem 1 is the abstract convergence theorem behind cyclic Bregman projections. With $D(x,y)=\|x-y\|^2$ in a Hilbert space it gives the convergence of cyclic orthogonal projections onto finitely many closed convex sets in the weak topology (the paper's Example 1). With $D$ given by a Bregman divergence it gives the method that the paper's §2 turns into an algorithm for convex programs with linear equality and inequality constraints, including entropy maximization. Lemma 1, the generalized Pythagorean inequality, is used throughout the later literature on Bregman projections, mirror descent and online learning.

The results are proved in the paper and are classical. To our knowledge no machine-checked version exists: Mathlib has orthogonal projections onto closed convex sets in Hilbert spaces, but no Bregman projections and no convergence theorem for cyclic projection methods. A formalization supplies an axiomatic interface (conditions I–VI) that does not depend on any particular divergence, so special cases (Euclidean distance, Kullback–Leibler divergence, Bregman divergences of Legendre functions) can be obtained by checking the conditions.

Difficulty

There is no norm and no metric: $D$ is neither symmetric nor subject to a triangle inequality, and $X$ is only a topological vector space. The usual Fejér-monotonicity argument for Euclidean projections, which compares distances to a fixed point of $R$ , works only one way in $D$ . Convergence of a subsequence $x^{n_k}$ does not by itself say anything about the shifted subsequences $x^{n_k+1},\dots,x^{n_k+m-1}$ , and these are needed to reach every set $A_i$ . That step requires condition VI together with compactness, and condition VI has a compactness premise that has to be supplied separately. Throughout, convergence is in a general topology where "compact" and "sequentially compact" may differ.

Formalization scope

The formalization commits to the following readings, each recorded in the items' Formalization Notes.

The projection is a map. $P:\iota\to X\to X$ is fixed, and condition II states that $P_iy$ is a minimizer. Condition III is stated for this map.
Condition IV, one-sided. The paper asks for $\lim_{t\to0}D(y+tz,y)/t=0$ for every $z\in X$ . The formalization assumes only the right-hand limit in the directions $w-y$ with $w\in S$ , which is what the proofs use and what the paper's IV implies. Every theorem is therefore at least as strong as the paper's.
Compactness is sequential. "Compact" in V, VI and Lemma 2 (1) is IsSeqCompact. The set of elements of $\{x^n\}$ being compact is read as $\{x^n\}$ lying in a sequentially compact set.
Hausdorff space. The proof of Theorem 1 identifies two limits of one sequence, so T2Space X is assumed. $X$ is a real topological vector space (IsTopologicalAddGroup, ContinuousSMul ℝ).
Limiting point means the limit of x ∘ φ for a strictly increasing φ : ℕ → ℕ.
Index base. The sets are indexed by Fin m with $0<m$ , and the cyclic control is $n\mapsto n\bmod m$ , the paper's $i_n=(n\bmod m)+1$ shifted by one.
Translation typos. Condition II is printed as " $D(x,y)=\min_{z\in A_i\cap S}D(z,x)$ " with " $i\in T$ ". The formalization reads $\min_z D(z,y)$ and $i\in I$ . In Lemma 2 (2) the faint set symbol is read as $R$ , and $z$ is taken in $R\cap S$ , as in the proof.
Domain of $D$ . $D$ is a total function X → X → ℝ; every condition constrains it on $S\times S$ only, and the standing assumption $S\cap R\ne\emptyset$ is an explicit hypothesis.

A trivializing formalization is ruled out: the hypotheses are satisfiable (a sorry-free local check takes $X=\mathbb R$ , $D(x,y)=(x-y)^2$ , two overlapping closed intervals and the clamp projections), the conclusion concerns every limiting point of every cyclic run, and the goal neither assumes convergence nor restricts the control.

Contributions welcome: proofs of the milestones, a proof of the goal, and instances of DConditions for concrete divergences (squared Euclidean distance in finite dimension, Bregman divergences of strictly convex differentiable functions). These instances are reusable by the companion missions of this paper.

Selected references

L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3) (1967) 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
L. G. Gubin, B. T. Polyak, E. V. Raik, The method of projections for finding the common point of convex sets, USSR Computational Mathematics and Mathematical Physics 7(6) (1967) 1–24. https://doi.org/10.1016/0041-5553(67)90113-9
T. S. Motzkin, I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 393–404. https://doi.org/10.4153/CJM-1954-038-x
Y. Censor, A. Lent, An iterative row-action method for interval convex programming, Journal of Optimization Theory and Applications 34 (1981) 321–353. https://doi.org/10.1007/BF00934676

6 thms2 active usersReviewed

Numerical Analysis Partial Differential Equations·Captain: mikedeng1

Mean Field Games: Numerical Methods for the Planning Problem II: Solutions of the Penalized Scheme Converge to a Solution of the Discrete Planning Scheme as ε → 0Research Paper

Motivation

Mean field games (MFG), introduced by Lasry and Lions and by Huang, Caines and Malhamé, describe Nash equilibria of very large populations of identical rational agents. The equilibrium is a coupled system: a backward Hamilton–Jacobi–Bellman equation for the value function $u$ of a representative agent and a forward Fokker–Planck equation for the density $m$ of the population. In the planning problem, proposed by P.-L. Lions, both the initial density $m_0$ and the final density $m_T$ are prescribed, and one asks for a cost structure under which the population moves from one to the other. This is a mean field analogue of optimal transport.

Achdou, Camilli and Capuzzo-Dolcetta (hal-00465404, SIAM J. Control Optim. 2012) propose finite-difference schemes for the planning problem. Mission I of this series treats the existence of a solution of the discrete planning scheme. Since the two boundary conditions on $m$ make the discrete system hard to solve directly, the paper also introduces a penalized scheme, in which the initial condition $M^0 = m_0$ is replaced by a penalty $U^0 = (M^0 - m_0)/\varepsilon$ ; for each $\varepsilon > 0$ this is a standard discrete MFG system with a unique solution. This mission formalizes the paper's §3.2: the penalized solutions converge, as $\varepsilon \to 0$ , to a solution of the planning scheme.

Setting

Fix integers $N_h \ge 1$ , $N_T \ge 1$ , a horizon $T > 0$ and a viscosity $\nu \ge 0$ ; put $h = 1/N_h$ and $\Delta t = T/N_T$ . The grid $\mathbb T^2_h$ consists of the points $x_{i,j}$ , $(i,j) \in (\mathbb Z/N_h\mathbb Z)^2$ (periodic indices). A grid function is a real function on $\mathbb T^2_h$ ; time levels are $n = 0, \dots, N_T$ .

$(D_1^+U)_{i,j} = (U_{i+1,j} - U_{i,j})/h$ , $(D_2^+U)_{i,j} = (U_{i,j+1} - U_{i,j})/h$ , and the discrete gradient is $[D_hU]_{i,j} = ((D_1^+U)_{i,j}, (D_1^+U)_{i-1,j}, (D_2^+U)_{i,j}, (D_2^+U)_{i,j-1}) \in \mathbb R^4$ .
$\Delta_h$ is the five-point Laplacian.
A numerical Hamiltonian $g(x_{i,j}, q)$ , $q \in \mathbb R^4$ , is monotone (G1), $C^1$ (G3), convex (G4) and coercive (G5) in $q$ .
$\mathcal B_{i,j}(U, M)$ is the discrete transport term $\mathrm{div}_h\big(M\,\nabla_q g(\cdot, [D_hU])\big)$ .
$W : \mathbb R \to \mathbb R$ is strictly convex, superlinear and $C^2$ , with $V = W'$ (hypothesis (24)).
$\mathcal K = \{M \ge 0 : h^2\sum_{i,j} M_{i,j} = 1\}$ is the set of discrete probability densities, and $m_0, m_T \in \mathcal K$ with $m_0 > 0$ .

The planning scheme (18) asks for families $(U^n, M^n)$ with, for $n < N_T$ ,

\frac{U^{n+1} - U^n}{\Delta t} - \nu\Delta_hU^{n+1} + g(x, [D_hU^{n+1}]) = V(M^n), \qquad \frac{M^{n+1} - M^n}{\Delta t} + \nu\Delta_hM^n + \mathcal B(U^{n+1}, M^n) = 0,

$M^n \in \mathcal K$ , $M^0 = m_0$ and $M^{N_T} = m_T$ . The penalized scheme (20)–(23) has the same two equations, $M^n \in \mathcal K$ for $n < N_T$ , $M^{N_T} = m_T$ , and $U^0 = (M^0 - m_0)/\varepsilon$ in place of $M^0 = m_0$ .

Formalization targets

Goal: Proposition 4

Under the hypotheses of Theorem 1, for every sequence $\varepsilon_k \downarrow 0$ , every choice of penalized solutions $(U^{\varepsilon_k}, M^{\varepsilon_k})$ , and every limit $M^{\varepsilon_k} \to M$ in $\mathcal K^{N_T+1}$ ,

\exists\, U,\ \text{a subsequence with } U^{\varepsilon_k} \to U, \quad (U, M) \text{ solves (43)–(46)}.

If $g$ is strictly convex, the whole sequence $(U^{\varepsilon_k}, M^{\varepsilon_k})$ converges to the unique solution of (43)–(46) with $\sum_{i,j} U^0_{i,j} = 0$ .

Milestones

(13): (G5) implies $\max_{i,j} g(x_{i,j}, [D_hU]_{i,j}) / \|[D_hU]\|_\infty \to +\infty$ .
Theorem 2: the penalized control problem (50), $\min \Theta^*(M,Z) + \frac{1}{2\varepsilon\Delta t}\sum(M^0 - m_0)^2$ under the discrete Fokker–Planck constraint, has a minimizer whose optimality system is (20)–(23).
Proposition 2: $\max_{i,j}|M^{\varepsilon,0}_{i,j} - (m_0)_{i,j}| \le C\varepsilon^{1/2}$ .
Proposition 3: $\max_{n,i,j}|U^{\varepsilon,n}_{i,j}| \le C$ .
Corollary 1: $\max_{i,j}|M^{\varepsilon,0}_{i,j} - (m_0)_{i,j}| \le C\varepsilon$ .
Proposition 1: uniqueness of $M$ for (18), and of $U$ normalized by $\sum U^0 = 0$ when $g$ is strictly convex.

In 3–5 the constant $C$ depends on $h$ , $\Delta t$ and the data, never on $\varepsilon$ .

Significance

Proposition 4 justifies the penalized scheme as a way to compute solutions of the discrete planning problem. The penalized system has a standard initial–terminal structure that Newton's method (the paper's §4) handles well. The planning system does not, because it prescribes two conditions on $M$ and none on $U$ . The estimates of Propositions 2–3 and Corollary 1 also give a rate: the initial mismatch of the penalized density is $O(\varepsilon)$ .

The results are proved in the paper. None of them has been machine-checked: the platform holds no formalization of mean field games, of their finite-difference schemes, or of the Lasry–Lions monotonicity argument. A complete development would yield a reusable library of the monotone finite-difference operators on the discrete torus, a formal Lasry–Lions uniqueness argument for discrete MFG systems, and a template for compactness-plus-uniqueness convergence proofs in finite dimension.

Difficulty

Compactness of the densities is free, since $\mathcal K^{N_T+1}$ is compact. Passing to the limit in the scheme needs only continuity of $g$ , $\nabla_q g$ and $V$ . The substance lies in the two uniform estimates.

Bounding $U^\varepsilon$ uniformly in $\varepsilon$ (Proposition 3) is the central difficulty. The initial condition $U^{\varepsilon,0} = (M^{\varepsilon,0} - m_0)/\varepsilon$ involves division by $\varepsilon$ , so the obvious bound $|U^{\varepsilon,0}| \le 2/(h^2\varepsilon)$ blows up. The comparison principle for the discrete HJB equation, which is the natural first idea, cannot repair this: it propagates whatever bound $U^0$ has. The HJB equation alone does not bound $U^\varepsilon$ ; the coupling with the Fokker–Planck equation, the coercivity (13), and a lower bound on $M^{\varepsilon,0}$ that is uniform in $\varepsilon$ (which is where Proposition 2 enters) all have to be used.
Proposition 2 compares the penalized problem with the planning problem through the convex duality of Theorem 2. It therefore needs a solution of the planning scheme, which is mission I's goal.
Proposition 1 needs the discrete Lasry–Lions identity, a summation by parts across the coupled system.

Formalization scope

All objects live in the namespace MFGPlanning.Penalized.

Grid points are ZMod Nh × ZMod Nh (periodicity is built in), time levels are Fin (NT + 1), and the four momentum components $q_1, \dots, q_4$ are Fin 4 indices 0, …, 3.
The data structure carries $N_h, N_T \ge 1$ , $T > 0$ and $\nu \ge 0$ .
$g$ is given only at the grid points. (G2), which only defines the continuous Hamiltonian, is not encoded.
"Coercive" in (24) is read as superlinear.
$V_h[M] = V(M_{i,j})$ , as (24) prescribes.
$\Theta^*$ and $(W+\chi)^*$ take values in EReal, so unbounded suprema are $+\infty$ .
Convergence is in the product topology, which on these finite-dimensional spaces is $\max_n \|\cdot\|_\infty$ convergence.
"The unique solution" of (43)–(46) means unique under the normalization $\sum_{i,j} U^0_{i,j} = 0$ , because $U$ is otherwise determined only up to a constant.

Three trivializing formalizations are ruled out. The constants in Propositions 2–3 and Corollary 1 are quantified before $\varepsilon$ and before the solution. The goal quantifies over every sequence $\varepsilon_k \to 0$ and assumes no convergence of $U$ and no limit solution. Its part 2 does not assume convergence of $M$ .

The existence of a solution of the planning scheme (Theorem 1) is posed in mission I and not restated here. A solver of Proposition 2 will need it once mission I's goal is proved. The existence and uniqueness of solutions of (20)–(23) are quoted by the paper from Achdou–Capuzzo-Dolcetta (2010) and are not items. Welcome contributions include discrete summation-by-parts lemmas on the torus, the discrete comparison principle for monotone schemes, and the Poincaré-type inequality $\|W\|_\infty \le c\|[D_hW]\|_\infty$ on zero-mean grid functions.

Selected references

Y. Achdou, F. Camilli, I. Capuzzo-Dolcetta, Mean field games: numerical methods for the planning problem, HAL preprint hal-00465404v1, 2010; SIAM J. Control Optim. 50 (2012). https://hal.science/hal-00465404v1, https://doi.org/10.1137/100790069
Y. Achdou, I. Capuzzo-Dolcetta, Mean field games: numerical methods, SIAM J. Numer. Anal. 48 (2010) 1136–1162. https://doi.org/10.1137/090758477
J.-M. Lasry, P.-L. Lions, Mean field games, Japanese Journal of Mathematics 2 (2007) 229–260. https://doi.org/10.1007/s11537-007-0657-8
M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Communications in Information and Systems 6 (2006) 221–252. https://doi.org/10.4310/CIS.2006.v6.n3.a5

11 thms2 active usersReviewed

Completed

Linear Optimization Statistics·Captain: mikedeng1

Conditional Logit Analysis of Qualitative Choice Behavior 4: Existence of the Maximum Likelihood Estimate Is Decided by a Quadratic ProgramResearch Paper

Why a likelihood maximum needs a diagnostic

The conditional logit model assigns probabilities to choices among alternatives whose observable attributes differ from trial to trial. A fitted parameter vector is usually obtained by maximizing a log-likelihood. For a finite data set, however, maximization need not produce a finite vector: some directions in parameter space can keep improving the likelihood while their length grows without bound. McFadden identifies a condition that rules out these directions and then gives a quadratic program that can test the condition. This mission formalizes that test, Lemma 4 of the published 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior.

The chapter develops a statistical model from observable choice data and addresses the existence of a maximum likelihood estimate in Lemma 3. Lemma 4 turns its existence condition into a finite optimization problem. The diagnostic matters because an optimization routine returning increasingly large parameter estimates is not, by itself, evidence that a finite maximizer exists. The result specifies a mathematical test tied to the observed choice counts and the attributes of the alternatives.

Choice experiments and weighted differences

There are $N\geq1$ trials. Trial $n$ offers $J_n$ alternatives, indexed by $i$ and $j$ . Alternative $i$ has an attribute vector $z_{in}\in\mathbb R^K$ , and $S_{in}$ counts how many times it was selected in that trial. Each trial has at least two alternatives and $R_n=\sum_iS_{in}>0$ observations. The vector $\theta\in\mathbb R^K$ is the unknown parameter of the underlying conditional logit model. Equation (16) assigns alternative $i$ a probability proportional to $\exp(z_{in}\cdot\theta)$ , with the probabilities normalized over the alternatives in the same trial McFadden, pp. 113–114, equation (16).

For the test, define the weighted difference

w_{nij}=S_{in}(z_{jn}-z_{in})\in\mathbb R^K.

It is indexed by every trial and every ordered pair of alternatives, including $i=j$ and alternatives whose observed count is zero. Such terms simply produce zero vectors. Keeping them in the index set makes the formal statement agree with the chapter's quantifiers and its quadratic program.

Axiom 5, called full rank in the chapter, says that the rows obtained by subtracting each trial's probability weighted mean attribute vector from its alternative attributes have rank $K$ . Equivalently, the vectors $z_{jn}-z_{in}$ span $\mathbb R^K$ ; the probability weights in that mean are strictly positive and sum to one. Axiom 6 says that no nonzero direction $\gamma\in\mathbb R^K$ satisfies $w_{nij}\cdot\gamma\leq0$ for every ordered index triple. These are conditions on the same observed experiment, but they serve different roles: full rank concerns the attribute geometry, while Axiom 6 also uses the choice counts McFadden, p. 116, Axioms 5–6.

Formalization targets

Lemma 4: a quadratic-programming test

Let $Q$ be the set of feasible vectors

Q=\left\{y=\sum_{n=1}^{N}\sum_{i,j=1}^{J_n}\alpha_{ijn}w_{nij}: \alpha_{ijn}\geq1\text{ for all }n,i,j\right\}.

The mission's goal is the equivalence in Lemma 4:

\text{Axiom 6 holds} \quad\Longleftrightarrow\quad \min_{y\in Q}y\cdot y=0.

The right side means that the program attains a value of zero. An infimum of zero without an attained feasible point would be a weaker statement and would not express the lemma. The three milestones follow the three assertions in the printed proof: a zero minimum implies Axiom 6; an interior origin in the cone generated by the $w_{nij}$ gives positive coefficients and a zero minimum; and a noninterior origin gives a separating direction that violates Axiom 6 McFadden, p. 117, Lemma 4 and equation (22).

What the result provides

Lemma 3 of the chapter states that Axiom 6 characterizes the existence of a vector maximizing the conditional-logit log-likelihood under the preceding axioms. Lemma 4 gives a finite quadratic-programming criterion for that same condition. It therefore allows the model's existence question to be checked from data before treating a numerical optimizer's output as an estimate McFadden, pp. 116–117, Lemmas 3–4.

The paper proves these results. The work here is to produce machine-checkable statements for the finite-dimensional data, the two axioms, the feasible set, and the equivalence, followed by proofs in the solver stage. The cone and separation milestones can support later formalizations of existence conditions in other finite exponential-family models, provided their hypotheses and signs are checked anew. This mission does not claim a general theorem for all such models.

Why the equivalence is delicate

The tempting diagnostic is to ask whether a numerical solve returns a small objective value. That does not settle the mathematical question: the objective's infimum could approach zero without the feasible set containing a zero vector. The paper's conclusion is about a minimum, so attainment must remain visible in the formal statement. There is also a distinction between positive coefficients in a cone representation and the printed constraints $\alpha_{ijn}\geq1$ in equation (22). Both conditions must appear in their proper places.

The full-rank condition alone does not ensure that the vectors $w_{nij}$ span the attribute space if a trial has no observed choices. The section describes $R_n$ repetitions of each trial, and the formal data require $R_n>0$ . This convention is needed for the strict-inequality claim in the first paragraph of Lemma 4's proof. The geometry also has to account for every ordered pair, even when its vector is zero; dropping these indices would alter the program stated in the chapter.

Formalization scope

Lean represents a nonempty set of trials by Fin N, alternatives in trial $n$ by Fin (J n), counts by natural numbers, and attributes by EuclideanSpace ℝ (Fin K). The count $R_n$ is the sum of observed choice counts. The model requires $J_n\geq2$ and $R_n>0$ for each trial. There is no extra assumption that $K>0$ : the zero-dimensional case is included and the equivalence has its ordinary degenerate meaning there.

Axiom 5 is encoded through the equivalent span of within-trial attribute differences. This removes the parameter dependent logit probabilities from a theorem that only uses rank. Axiom 6 retains exactly the nonpositive sign and every $n,i,j$ from the page. The feasible set uses coefficients at least one, while the auxiliary generated cone uses nonnegative coefficients. The quadratic objective is the square of the Euclidean norm. IsLeast on its image over the feasible set expresses an attained minimum, so the statement cannot be satisfied by a vacuous or unattained infimum.

The definition bundle and the three proof-step theorems are the mission's direct scope. A complete development needs finite-dimensional inner-product geometry, finite sums, a cone interior argument, and separation. The definitions of weighted differences and the feasible set are reusable for studying nearby existence tests. Contributions that prove the stated milestones or supply faithful finite-dimensional geometry for them are welcome; substitutions that weaken the coefficient constraint or the attainment claim do not establish Lemma 4.

Selected references

Daniel McFadden, “Conditional Logit Analysis of Qualitative Choice Behavior,” in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, pp. 105–142; especially pp. 113–117, Axioms 5–6, Lemmas 3–4, and equation (22). Book catalog search.

5 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Consensus of Subjective Probabilities: The Pari-Mutuel Method: Equilibrium Track Probabilities Exist and Are UniqueResearch Paper

Motivation

A group of $m$ individuals each hold a subjective probability distribution over the same $n$ outcomes, and one wants a single distribution representing their consensus. Averaging and convolution are the obvious candidates. Eisenberg and Gale (Ann. Math. Statist. 30(1), 1959) observe that a real institution already performs such an aggregation: the pari-mutuel method of betting on horse races, in which the final "track's odds" on a horse are proportional to the total amount bet on it.

The difficulty is circular. Each bettor wants to bet where the ratio of their own probability to the track probability is largest, but the track probabilities are only known after everyone has bet. The paper asks whether track probabilities and bets compatible with both the bettors' strategies and the pari-mutuel principle exist, and whether they are determined by the data. It answers yes on both counts for the probabilities, which gives a well-defined notion of pari-mutuel consensus.

The variational problem the paper introduces, maximizing $\sum_i b_i \log(\text{utility}_i)$ , is now known as the Eisenberg–Gale convex program. It is the standard tool for computing equilibria of linear Fisher markets, and the pari-mutuel market is the special case in which every bettor's utility for a horse is their subjective win probability.

Setting

There are $m$ bettors $B_1,\dots,B_m$ and $n$ horses $H_1,\dots,H_n$ .

The subjective probability matrix $P=(p_{ij})$ is $m\times n$ ; $p_{ij}$ is the probability, in the opinion of $B_i$ , that $H_j$ wins. Each row is a probability distribution: $p_{ij}\ge 0$ and $\sum_j p_{ij}=1$ .
Bettor $B_i$ has a budget $b_i>0$ , with the unit of money chosen so that $\sum_i b_i=1$ .
Each column of $P$ contains at least one positive entry (a horse nobody believes in can be removed).

Unknowns are Greek. $\pi_j$ is the track probability of $H_j$ and $\beta_{ij}$ is the amount $B_i$ bets on $H_j$ . Nonnegative $\pi_j,\beta_{ij}$ are equilibrium probabilities and bets when

\text{(1)}\ \sum_{j=1}^n\beta_{ij}=b_i,\qquad \text{(2)}\ \sum_{i=1}^m\beta_{ij}=\pi_j,\qquad \text{(3)}\ \text{if } \mu_i=\max_s\frac{p_{is}}{\pi_s}\text{ and }\beta_{ij}>0,\text{ then }\mu_i=\frac{p_{ij}}{\pi_j}.

(1) is the budget relation, (2) the pari-mutuel condition, and (3) says each bettor bets only on horses that maximize the subjective expectation $p_{ij}/\pi_j$ .

The paper's variational problem is

\varphi(\xi)=\sum_{i=1}^m b_i\log\sum_{j=1}^n p_{ij}\xi_{ij}\quad\text{on}\quad D=\Big\{\xi:\ \xi_{ij}\ge0,\ \sum_{i=1}^m\xi_{ij}=1\ \text{for all } j\Big\},

with $\varphi=-\infty$ where an inner sum vanishes. From a maximizer $\bar\xi$ it builds $\pi_j=\max_i b_ip_{ij}/\sum_s p_{is}\bar\xi_{is}$ (6) and $\beta_{ij}=\bar\xi_{ij}\pi_j$ (7). In Lean the market is PariMutuel.Consensus.Market m n, equilibrium is Market.IsEquilibrium, and $\varphi$ , $D$ , the maximizer predicate, (6) and (7) are Market.phi, D m n, Market.IsPhiMaximizer, Market.trackProb, Market.bets.

Formalization targets

Goal: existence and uniqueness of equilibrium probabilities

\exists!\,\pi\in\mathbb R^n\ \ \exists\,\beta\in\mathbb R^{m\times n}:\ (\pi,\beta)\ \text{are equilibrium probabilities and bets}.

Only $\pi$ is unique; the paper notes that equilibrium bets need not be.

Milestones

$\varphi$ attains its maximum on $D$ at a point with every inner sum positive (p. 167).
$\partial\varphi/\partial\xi_{ij}=b_ip_{ij}/\sum_s p_{is}\xi_{is}$ wherever the inner sums are positive (p. 167).
(8): at a maximizer, $\bar\xi_{ij}>0$ implies $\pi_j=\partial\varphi/\partial\bar\xi_{ij}$ (p. 167).
Every $\pi_j$ of (6) is positive (p. 167).
EXISTENCE THEOREM: for every maximizer $\bar\xi$ , (6)–(7) are equilibrium probabilities and bets (p. 167).
Every equilibrium has $\pi_j>0$ (p. 168).
For two equilibria, $\sum_k\bar\pi_k\bar\pi_k/\pi_k\le 1$ (p. 168).
If $\pi>0$ , $\bar\pi\ge0$ , both sum to 1 and $\sum_k\bar\pi_k^2/\pi_k\le1$ , then $\bar\pi=\pi$ (p. 168).
UNIQUENESS THEOREM: equilibrium probabilities are unique (p. 168).

A further, non-milestone item states the referee's example (p. 168): with two bettors of equal budgets and two horses, if the first bettor's distribution is $(\tfrac12,\tfrac12)$ , the equilibrium probabilities are $(\tfrac12,\tfrac12)$ whatever the second bettor believes.

Significance

The result makes pari-mutuel odds a well-defined function of the bettors' beliefs and budgets, so the consensus can be studied as a mathematical object; the referee's example shows it behaves very differently from averaging, since a single indifferent bettor can fix it. The existence proof replaces a fixed-point argument by a concave maximization, which is the origin of the Eisenberg–Gale program, later the basis of convex-programming and combinatorial algorithms for Fisher market equilibria.

The theorems are classical and fully proved in the paper. To the knowledge of this mission they have no machine-checked proof. The mission produces a formal pari-mutuel market model, the Eisenberg–Gale program with the correct treatment of $\log 0=-\infty$ , and Lean proofs of existence and uniqueness. The platform's Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities missions (Vazirani–Yannakakis) concern a related Fisher-market model with rational piecewise-linear utilities.

Difficulty

The existence statement, as the paper proves it, has two delicate points. $\varphi$ is $-\infty$ on part of the boundary of $D$ , so "continuous on a compact set" needs the extended-real reading, and a real-valued formalization must handle the boundary separately. The first-order condition (8) has to be derived from maximality on a polytope with equality constraints on columns, not from an unconstrained critical point.

For uniqueness, the natural first idea, strict concavity of $\varphi$ , fails: $\varphi$ is concave but not strictly concave in $\xi$ , and indeed equilibrium bets are not unique. Uniqueness has to be proved for the probabilities directly, for arbitrary equilibria and not only those built from a maximizer, and it needs positivity of all $\pi_j$ , which the paper uses without proof.

Formalization scope

Bettors are Fin m and horses Fin n, indexed from 0. All data are real. Every standing assumption (rows of $P$ are probability vectors, no zero column, $b_i>0$ , $\sum_i b_i=1$ ) is a field of Market; $m\ge1$ follows from $\sum_ib_i=1$ .
Condition (3) is written multiplied out: $\beta_{ij}>0\Rightarrow p_{is}\pi_j\le p_{ij}\pi_s$ for all $s$ . This equals (3) when $\pi>0$ and encodes the paper's $p/0=+\infty$ when some $\pi_s=0$ . Positivity of $\pi$ is not part of the definition of equilibrium; it is milestone 6.
$D$ has column sums one, as in (5).
$\varphi$ is real-valued. A maximizer is a point of $D$ with positive inner sums that dominates every point of $D$ with positive inner sums; the excluded points have $\varphi=-\infty$ on the page. The max in (6) is Finset.sup' over the nonempty set of bettors.
Ruled out: a version of (3) with real division ( $x/0=0$ ) admits spurious equilibria with $\pi_s=0$ and makes uniqueness false; a maximizer defined with the raw real $\varphi$ ( $\log0=0$ ) changes the set of maximizers; adding $\pi>0$ or $\sum_j\pi_j=1$ to the equilibrium definition weakens the goal.
Needed infrastructure: compactness of $D$ and an argument handling the $-\infty$ boundary, one-variable derivatives of $\log$ of linear forms, and the equality case of the Cauchy–Schwarz inequality. Milestones 7–9 use no analysis and can be attacked independently of 1–5. Proofs of any milestone, and reusable lemmas on the Eisenberg–Gale program, are welcome.

Selected references

E. Eisenberg and D. Gale, Consensus of subjective probabilities: the pari-mutuel method, The Annals of Mathematical Statistics 30(1):165–168, 1959. https://doi.org/10.1214/aoms/1177706369
V. V. Vazirani and M. Yannakakis, Market equilibrium under separable, piecewise-linear, concave utilities, Journal of the ACM 58(3), 2011. https://doi.org/10.1145/1970392.1970394

12 thms2 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

Stability and Generalization 4: Relative-Entropy Regularization of Mixtures Has Uniform Stability M²/(λm)Research Paper

Motivation

A learning algorithm generalizes when its error on fresh data is close to its error on the training sample. Bousquet and Elisseeff (JMLR 2, 2002) showed that a single property of the algorithm, uniform stability, controls this gap with exponential concentration: if removing any one example from a training set of size $m$ changes the loss of the output at every point by at most $\beta$ , the generalization error exceeds the empirical error by roughly $2\beta + (4m\beta + M)\sqrt{\ln(1/\delta)/(2m)}$ with probability $1-\delta$ (their Theorem 12). The bound is useful only when $\beta = O(1/m)$ , and the second half of the paper identifies algorithms with that rate: Tikhonov regularization in a reproducing kernel Hilbert space (Theorem 22), and relative-entropy regularization of mixtures (Theorem 24), the subject of this mission.

Mixtures arise whenever a learner outputs a distribution over a parametric base class instead of a single hypothesis: Bayesian posterior averaging, Gibbs and randomized classifiers, exponential weights. Regularizing by the relative entropy to a prior is the maximum-a-posteriori reading of these procedures, and Theorem 24 is one of the earliest results showing that such posteriors are uniformly stable with rate $1/(\lambda m)$ . The same mechanism (entropic regularization, stability through Pinsker's inequality) reappears in PAC-Bayesian analysis and in the stability of exponential-weights methods.

Setting

Let $\Theta$ be a measurable space with a reference measure $\nu$ , and write $d\theta$ for integration against $\nu$ . A base class $\mathcal H = \{h_\theta : \theta \in \Theta\}$ is indexed by $\Theta$ , and $r(h_\theta, z) \in [0, M]$ is the loss of the base hypothesis $h_\theta$ at an example $z \in Z$ .

The algorithm outputs a density $g$ with respect to $\nu$ : a measurable, nonnegative, integrable $g : \Theta \to \mathbb R$ with $\int_\Theta g\,d\theta = 1$ . $F$ denotes the set of all densities. A density is scored by the averaged loss

\ell(g, z) = \int_\Theta r(h_\theta, z)\, g(\theta)\, d\theta \qquad (28),

the expected loss of a randomized predictor that draws $h_\theta$ from $g$ . The relative entropy of $g$ to $g'$ is

K(g, g') = \int_\Theta g(\theta) \ln \frac{g(\theta)}{g'(\theta)}\, d\theta \in [0, \infty],

with $K(g, g') = +\infty$ when $g\,\nu$ is not absolutely continuous with respect to $g'\,\nu$ or the integrand is not integrable.

Fix a prior $f_0 \in F$ , a parameter $\lambda > 0$ , and a training set $S = (z_1, \dots, z_m)$ . The algorithm returns a minimizer over $F$ of

R_r(g) = \frac1m \sum_{j=1}^m \ell(g, z_j) + \lambda K(g, f_0) \qquad (29).

For an index $i$ , the truncated objective is $R_r^{\setminus i}(g) = \frac1m \sum_{j \ne i} \ell(g, z_j) + \lambda K(g, f_0)$ , and $f^{\setminus i}$ denotes one of its minimizers over $F$ .

Formalization targets

Goal: Theorem 24

For every minimizer $f$ of (29), every minimizer $f^{\setminus i}$ of the truncated objective, and every example $z$ ,

|\ell(f, z) - \ell(f^{\setminus i}, z)| \le \frac{M^2}{\lambda m}.

Milestones

$M$ -admissibility of (28) (§5.2.3, p. 518): $|\ell(g,z) - \ell(g',z)| \le M \int_\Theta |g - g'|\,d\theta$ .
Pinsker's inequality, $L^1$ form (proof of Theorem 24): $\tfrac12 \bigl(\int_\Theta |g - g'|\,d\theta\bigr)^2 \le K(g, g')$ for densities $g, g'$ .
Lemma 21 (p. 513): for a differentiable convex regularizer $N$ on a vector space and a $\sigma$ -admissible loss,

d_N(f, f^{\setminus i}) + d_N(f^{\setminus i}, f) \le \frac{1}{\lambda m}\Bigl(\ell(f^{\setminus i}, z_i) - \ell(f, z_i) - d_{\ell(\cdot, z_i)}(f^{\setminus i}, f)\Bigr) \le \frac{\sigma}{\lambda m}|\Delta f(x_i)|.

Bregman divergence of the relative entropy (proof of Theorem 24): $d_{K(\cdot, f_0)}(g, g') = K(g, g')$ .
$L^1$ displacement bound (proof of Theorem 24):

\int_\Theta |f - f^{\setminus i}|\,d\theta \le \frac{M}{\lambda m}.

Significance

Theorem 24 places entropy-regularized posteriors among the algorithms to which the paper's exponential generalization bound applies: combined with Theorem 12 it gives, for the averaged loss, a deviation of order $M^2/(\lambda m) + (M^2/\lambda + M)\sqrt{\ln(1/\delta)/m}$ . The proof also yields the $L^1$ bound $\int |f - f^{\setminus i}| \le M/(\lambda m)$ , which by itself gives classification stability $M/(\lambda m)$ for base hypotheses with values in $\{-1, 1\}$ (remark after Theorem 24, p. 518).

The result is proved in the paper; no machine-checked proof is known to exist. A formalization produces reusable pieces that Mathlib does not have: Pinsker's inequality for densities in $L^1$ form (Mathlib has the Kullback–Leibler divergence InformationTheory.klDiv, but not Pinsker), the Bregman identity for the relative entropy, and a stability statement for minimizers over a space of probability densities.

Difficulty

The paper derives Theorem 24 from Lemma 21, which is stated for a regularizer that is defined and differentiable on a vector space. The relative entropy $K(\cdot, f_0)$ is defined only on the convex set of densities and is not differentiable at densities that vanish on a set of positive measure, so the general lemma does not literally apply, and the identity $d_{K(\cdot,f_0)} = K$ needs integrability conditions that the page does not state. A complete proof of the goal must either justify that application on the set of densities, or work directly with the minimizers, which requires identifying them and handling the $+\infty$ values of $K$ . Pinsker's inequality itself requires a separate argument at the level of general measures.

Formalization scope

Densities are IsDensity ν g: measurable, nonnegative, integrable, total mass one, with respect to a σ-finite reference measure ν. The integral $d\theta$ is always against ν, never Lebesgue measure.
The base loss is r : Θ → Z → ℝ, measurable in θ, with 0 ≤ r ≤ M; the paper's costs are nonnegative (p. 502).
$K$ is InformationTheory.klDiv of the measures g · ν and g' · ν, in ℝ≥0∞. The objectives (29) and its truncation take values in ℝ≥0∞. A formalization that converts $K$ to a real number with toReal would send $K = +\infty$ to $0$ and make the worst densities minimizers; that reading is excluded.
The minimizers are given as hypotheses: f minimizes (29) and f' minimizes the truncated objective over all densities, for the given S : Fin m → Z and i : Fin m.
Corrected reading of the algorithm on $S^{\setminus i}$ . The goal is stated in the pairwise form of the paper's proof: $f^{\setminus i}$ minimizes the truncated objective with factor $1/m$ , the analogue of (20), not (29) run on the $m-1$ points of $S^{\setminus i}$ with factor $1/(m-1)$ .
Corrected display. The objective displayed before Theorem 24 has $\ell(g, z)$ inside the sum; (29) has $\ell(g, z_i)$ , which is used.
Lemma 21 is stated as printed, in its differentiable case, on a real normed space whose elements act as functions on $X$ through a linear map; the goal does not instantiate it. The Bregman identity is stated with the explicit gradient $\ln(g'/f_0) + 1$ , for $f_0, g' > 0$ , finite $K(g, f_0)$ , $K(g', f_0)$ , and integrable $g \ln(g'/f_0)$ .

Contributions welcome: proofs of Pinsker's inequality for klDiv (reusable far beyond this mission), of the Bregman identity, of Lemma 21, and of the goal by any route.

Selected references

O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991 (Pinsker's inequality). https://doi.org/10.1002/0471200611
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Bregman divergences, Appendix C of the paper). https://doi.org/10.1515/9781400873173

11 thms2 active usersReviewed

Functional Analysis Optimization·Captain: mikedeng1

The Rate of Convergence of Nesterov's Accelerated Forward-Backward Method is Actually Faster than 1/k^2 II: For α > 3, the Iterates Converge Weakly to a Minimizer of Ψ + ΦResearch Paper

Motivation

Many problems in signal processing, statistics and machine learning take the additively separable form

\min\{\Psi(x) + \Phi(x) : x \in \mathcal H\},

a smooth term $\Phi$ plus a nonsmooth but "simple" term $\Psi$ , such as an $\ell^1$ penalty or the indicator function of a convex constraint set. The forward-backward method alternates a gradient step on $\Phi$ with a proximal step on $\Psi$ . Beck and Teboulle's FISTA (Beck–Teboulle 2009) combined it with Nesterov's acceleration and improved the worst-case rate for function values from $\mathcal O(k^{-1})$ to $\mathcal O(k^{-2})$ . Whether the iterates of the accelerated scheme converge at all, and not just their function values, remained unsettled for a long time; in the words of Attouch and Peypouquet, it "puzzled researchers for over two decades".

Timeline.

1967: Opial proves that weak convergence of a sequence in a Hilbert space follows from two facts, the convergence of its distance to every point of a target set and the location of its weak cluster points in that set (Opial 1967).
2009: Beck and Teboulle introduce FISTA, with an $\mathcal O(k^{-2})$ rate for function values.
2014: Su, Boyd and Candès read the accelerated method as a discretization of the ODE $\ddot x + \frac{\alpha}{t}\dot x + \nabla\Theta(x) = 0$ (Su–Boyd–Candès 2014).
2014–2015: for the variant with inertial coefficient $\frac{k-1}{k+\alpha-1}$ and $\alpha > 3$ , Chambolle and Dossal (2015) and, independently, Attouch, Chbani, Peypouquet and Redont (arXiv:1507.04782) prove weak convergence of the iterates.
2016: Attouch and Peypouquet (arXiv:1510.08740, SIAM J. Optim. 26(3), 2016) prove the $o(k^{-2})$ rate and, as Theorem 3, give a short proof of weak convergence from the same energy estimates.

The case $\alpha = 3$ , the original choice of FISTA, is not covered by this result.

Setting

Let $\mathcal H$ be a real Hilbert space with scalar product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ .

$\Psi : \mathcal H \to \mathbb R \cup \{+\infty\}$ is proper (finite somewhere), lower-semicontinuous and convex. The value $+\infty$ matters: indicator functions of closed convex sets are the main example.
$\Phi : \mathcal H \to \mathbb R$ is convex and continuously differentiable, and its gradient $\nabla\Phi$ is $L$ -Lipschitz continuous.
$\Theta = \Psi + \Phi$ , and $S = \operatorname{argmin}\Theta$ is assumed nonempty.
For $s > 0$ , the proximal map $\operatorname{prox}_{s\Psi}(x)$ is the unique minimizer of $y \mapsto \Psi(y) + \frac{1}{2s}\|y - x\|^2$ .

Given $\alpha > 0$ and $s > 0$ , algorithm (2) generates $(x_k)$ by

y_k = x_k + \frac{k-1}{k+\alpha-1}(x_k - x_{k-1}),\qquad x_{k+1} = \operatorname{prox}_{s\Psi}\big(y_k - s\nabla\Phi(y_k)\big).

The auxiliary sequence (6) is $z_k = x_k + \frac{k-1}{\alpha-1}(x_k - x_{k-1})$ . For a point $x^*$ , the proof of Theorem 3 uses

\delta_k = (k-1)\big[\|x_k - x^*\|^2 - \|x_{k-1} - x^*\|^2\big] + (\alpha-1)\|x_k - x^*\|^2 .

A sequence $(x_k)$ converges weakly to $\bar x$ , written $x_k \rightharpoonup \bar x$ , if $\langle x_k, y\rangle \to \langle \bar x, y\rangle$ for every $y \in \mathcal H$ .

In Lean these are theta, extrap ( $y_k$ ), IsAccelFBRun and zSeq (shared definitions in the namespace NesterovFB.Rates), and deltaSeq in the namespace NesterovFB.Weak. The predicates IsProperClosedConvex and IsProx and the predicate WeakTendsto are reused from the platform.

Formalization targets

Goal: Theorem 3 (p. 5)

Under the assumptions above, with $\alpha > 3$ and $0 < s < 1/L$ ,

\exists\, \bar x \in S:\quad x_k \rightharpoonup \bar x .

The limit is required to be a minimizer of $\Theta$ ; weak convergence to an arbitrary point would be a weaker statement.

Milestones (proof of Theorem 3, p. 5)

For every $x^* \in S$ and $k \ge 1$ :

\|x_{k+1} - x^*\|^2 \le \|y_k - x^*\|^2,

\delta_{k+1} - \delta_k \le 2(k+\alpha-1)\,\|x_k - x_{k-1}\|^2,

\lim_{k\to\infty}\|z_k - x^*\| \text{ exists},\qquad \lim_{k\to\infty}\|x_k - x^*\| \text{ exists}.

Significance

The result. Theorem 3 shows that the accelerated forward-backward method with $\alpha > 3$ behaves like the unaccelerated method in one important respect: its iterates converge to a solution rather than just producing small function values. In infinite-dimensional settings (inverse problems, PDE-constrained optimization, signal recovery in function spaces) weak convergence is the natural notion, and strong convergence can fail. The four milestones are the steps that matter for other analyses too: a "Fejér-type" step inequality from the extrapolated point, and the convergence of the distance to every minimizer.

Formalizing it. The result is proved in the literature; no machine-checked proof of it is known. A complete formalization needs the energy estimates of the paper's §1.1–1.2 (summability of $k\|x_k - x_{k-1}\|^2$ , boundedness of $(z_k)$ , and the convergence of $k^2\|x_{k+1}-x_k\|^2 + (k+1)^2(\Theta(x_{k+1}) - \min\Theta)$ ), which a companion mission poses separately, and Opial's lemma, which is not in Mathlib.

Difficulty

The unaccelerated forward-backward method is Fejér monotone: $\|x_{k+1} - x^*\|$ decreases for every minimizer $x^*$ , and Opial's lemma applies directly. The accelerated iterates are not Fejér monotone. The first milestone only compares $x_{k+1}$ with the extrapolated point $y_k$ , and $\|y_k - x^*\|$ can exceed $\|x_k - x^*\|$ by the inertial term. The quantity $\|x_k - x^*\|^2$ therefore satisfies only a second-order inequality with coefficients that grow in $k$ . The obvious attempt, to show that $\|x_k - x^*\|$ is eventually monotone and apply Opial's lemma as for the unaccelerated method, fails.

A second difficulty is the passage from distances to weak convergence: in a Hilbert space this needs the weak sequential compactness of bounded sets and the weak lower-semicontinuity of $\Theta$ (to place weak cluster points in $S$ ).

Formalization scope

$\mathcal H$ is a general real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H), not $\mathbb R^n$ ; in finite dimensions weak and strong convergence coincide and the goal would be a different, weaker theorem.
$\Psi$ and $\Theta$ take values in EReal; $\Psi$ is never assumed real-valued.
$L$ is a nonnegative real and " $0 < s < 1/L$ " is written $0 < s$ , $sL < 1$ , which also allows $L = 0$ .
$\operatorname{prox}_{s\Psi}$ is a map $P$ given with its minimization property; under the hypotheses it is unique, so this is the proximal map.
The run starts at $k = 1$ with $x_0, x_1$ arbitrary. At $k = 1$ the inertial coefficient vanishes, so $x_0$ never matters; every sequence the paper generates satisfies the predicate.
"The limit exists" means a real limit. Weak convergence is the platform's WeakTendsto, not convergence in norm.
The milestones keep the standing hypothesis $\alpha > 3$ of Theorem 3, although the first two do not need it.

A trivializing formalization is ruled out by the sanity check: the hypotheses are jointly satisfiable, and the goal asks for weak convergence to a minimizer, so neither a vacuous hypothesis nor an arbitrary limit point is admitted.

Infrastructure that a complete development needs, and that is reusable beyond this mission: the descent inequality (9) of the proximal-gradient operator, Opial's lemma in a real Hilbert space, the weak lower-semicontinuity of proper lower-semicontinuous convex functions, and the lemma that a bounded real sequence whose positive increments are summable converges. Contributions of any of these are welcome.

Selected references

H. Attouch, J. Peypouquet, The rate of convergence of Nesterov's accelerated forward-backward method is actually faster than $1/k^2$ , SIAM J. Optim. 26(3):1824–1834, 2016. https://arxiv.org/abs/1510.08740 (v4 is the source of this mission)
H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168, 2018. https://arxiv.org/abs/1507.04782
A. Chambolle, C. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", J. Optim. Theory Appl. 166, 2015. https://doi.org/10.1007/s10957-015-0746-4
A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2(1):183–202, 2009. https://doi.org/10.1137/080716542
Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73:591–597, 1967. https://doi.org/10.1090/S0002-9904-1967-11761-0
W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, NIPS 2014. https://arxiv.org/abs/1503.01243

9 thms2 active usersReviewed

Optimization·Captain: mikedeng1

On Conjugate Convex Functions: Conjugation Is a Symmetric Correspondence Between Lower Semicontinuous Convex FunctionsResearch Paper

Motivation

Convex duality in optimization rests on one transformation: to a convex function $f$ one associates the function $\varphi(\xi) = \sup_x(\Sigma x\xi - f(x))$ , which records, for each slope $\xi$ , the best affine lower bound of $f$ with that slope. Lagrangian duality, the duality theory of linear and conic programming, the analysis of first-order methods through smoothness and strong convexity of conjugates, and the dual representations of risk measures and divergences all read off properties of $f$ from properties of $\varphi$ . Each of these uses needs one fact: that the transformation loses no information, so that applying it twice returns $f$ .

That fact, for functions on $\mathbb R^n$ , is the theorem of W. Fenchel's five-page note On conjugate convex functions (Canad. J. Math. 1 (1949) 73–77). Its timeline:

1912. W. H. Young proves the inequality $ab \le F(a) + G(b)$ for a pair of mutually inverse increasing functions $F', G'$ of one variable (Proc. R. Soc. Lond. A 87, 1912).
1949. Fenchel defines the conjugate of a convex function on a convex subset of $\mathbb R^n$ , without any differentiability, and proves that conjugation is a symmetric correspondence on convex functions that are semi-continuous from below and whose domain is closed relative to the function (Fenchel 1949).
1965. J.-J. Moreau develops conjugation for convex functions with values in $(-\infty, +\infty]$ on a real Hilbert space, together with the proximal map (Bull. SMF 93, 1965); the biconjugation theorem in this generality is called the Fenchel–Moreau theorem.
1970. R. T. Rockafellar's Convex Analysis makes the conjugate the central object of finite-dimensional convex analysis (Princeton, 1970).

Setting

Points of $\mathbb R^n$ are $x = (x_1,\dots,x_n)$ , and $\Sigma x\xi = x_1\xi_1 + \dots + x_n\xi_n$ .

A standing pair $(G, f)$ consists of a set $G \subseteq \mathbb R^n$ and a real function $f$ defined in $G$ such that

$G$ is nonempty and convex;
$f$ is convex on $G$ : $f((1-\theta)x' + \theta x'') \le (1-\theta)f(x') + \theta f(x'')$ for $x', x'' \in G$ , $0 < \theta < 1$ ;
$f$ is semi-continuous from below on $G$ : $\liminf_{x \to x^*,\, x \in G} f(x) \ge f(x^*)$ for $x^* \in G$ ;
$G$ is closed relative to $f$ : $f(x) \to +\infty$ as $x \to x^*$ within $G$ , for every boundary point $x^*$ of $G$ not in $G$ .

$G$ need be neither open, nor closed, nor bounded. The paper writes the lower limit as a "lim" with a bar under it; the milestone texts write it $\lim_{x\to x^*}$ , and it always means $\liminf$ .

The conjugate pair of $(G, f)$ is

\Gamma = \{\xi \in \mathbb R^n : x \mapsto \Sigma x\xi - f(x) \text{ is bounded above on } G\}, \qquad \varphi(\xi) = \sup_{x \in G}\bigl(\Sigma x\xi - f(x)\bigr)\quad (\xi \in \Gamma).

The same construction applied to $(\Gamma, \varphi)$ gives the pair $(G^*, f^*)$ , with $f^*(x) = \sup_{\xi\in\Gamma}(\Sigma\xi x - \varphi(\xi))$ . An interior point of $G$ is a point of the relative interior of $G$ , its interior within its affine hull.

In Lean: IsClosedConvexPair G f, conjDomain G f $= \Gamma$ , conjFun G f $= \varphi$ , and $(G^*, f^*)$ is conjDomain (conjDomain G f) (conjFun G f), conjFun (conjDomain G f) (conjFun G f).

Formalization targets

Goal: Fenchel's theorem (§3, p. 75)

For every standing pair $(G, f)$ :

(\Gamma,\varphi) \text{ is a standing pair},\qquad \Sigma x\xi \le f(x) + \varphi(\xi)\ \ (x\in G,\ \xi\in\Gamma), \tag{5}

with equality for some $\xi \in \Gamma$ at every interior point $x$ of $G$ ;

G^* = G, \qquad f^*(x) = f(x)\ \ (x \in G);

and every standing pair $(\Gamma', \varphi')$ whose conjugate pair is $(G, f)$ equals $(\Gamma, \varphi)$ .

Milestones, in the order of the proof

(5), with no hypothesis on $(G, f)$ .
$\Gamma \ne \emptyset$ , and $\varphi(\xi) = \Sigma x^\circ\xi - f(x^\circ)$ for some $\xi\in\Gamma$ at each interior point $x^\circ$ .
$\Gamma$ and $\varphi$ are convex.
$\varphi$ is semi-continuous from below and $\Gamma$ is closed relative to $\varphi$ .
(6): $G \subseteq G^*$ and $f^* \le f$ on $G$ .
Two convex functions, semi-continuous from below on $G$ and equal at the interior points of $G$ , are equal on $G$ .
$f^* = f$ on $G$ .
(7): $\sup_{\xi\in\Gamma}(\Sigma\xi x^\circ - \varphi(\xi)) = \infty$ for every $x^\circ \notin G$ .

Significance

The theorem identifies, among convex functions on convex subsets of $\mathbb R^n$ , exactly the class on which conjugation is a bijection and an involution. It is the finite-dimensional base case of the Fenchel–Moreau theorem and underlies Fenchel's duality theorem for $\inf(f - g)$ , the conjugate-based optimality conditions of convex programming, and the inversion of gradients of conjugate differentiable convex functions (the paper's §6, the Legendre transformation). The pair form is also how the result is used in practice: the conjugate of a function finite on a set comes with an explicit domain $\Gamma$ , and the theorem says that domain determines and is determined by $G$ .

The result has been proved for 75 years. What a formalization adds is the theorem in Fenchel's own form: a real-valued function on an explicit convex domain rather than an extended-real function on all of $\mathbb R^n$ , the domain identity $G^* = G$ together with the identity of values, and the attainment of equality in (5) at relative-interior points. Machine-checked versions of biconjugation exist in other forms: for extended-real functions on Hilbert spaces, for finite convex functions on all of $\mathbb R^n$ , and for functions on a set with a closed restricted epigraph over continuous linear functionals. None of them states the domain identity or the attained equality, and none is in the paper's pair form.

Difficulty

Milestones 1, 3, 4 and 5 follow from the definition of the conjugate alone. The content sits in three places.

Supporting hyperplanes at relative-interior points. When $G$ is lower-dimensional, the topological interior of $G$ is empty, and a supporting hyperplane must be produced inside the affine hull of $G$ and then extended. Points that are interior to a segment of $G$ but on its relative boundary do not suffice.
Passing from the interior to the boundary of $G$ . Equality $f^* = f$ at interior points does not by itself give equality at boundary points of $G$ ; it needs semi-continuity from below of both functions and convexity along segments ending at the boundary point.
$G^* \subseteq G$ . Points outside the closure of $G$ and boundary points of $G$ not in $G$ behave differently: a boundary point cannot be separated from $G$ by a hyperplane, and the inclusion there depends on the condition that $G$ be closed relative to $f$ . Without that condition the inclusion is false: for $G = (0, 1]$ and $f \equiv 0$ , the point $0$ lies in $G^*$ .

Formalization scope

$\mathbb R^n$ is Fin n → ℝ with its product topology, which is the Euclidean one; $\Sigma x\xi$ is Mathlib's x ⬝ᵥ ξ. The paper's $\Sigma\xi x$ in $G^*, f^*$ is ξ ⬝ᵥ x, equal by commutativity.
$f$ is a total function (Fin n → ℝ) → ℝ, but every hypothesis and conclusion concerns its values on $G$ only: ConvexOn ℝ G f, LowerSemicontinuousOn f G, and Tendsto f (𝓝[G] x) atTop for x ∈ closure G \ G.
$\varphi$ is the real sSup, which is $0$ on unbounded sets; it is evaluated only on $\Gamma$ .
Three readings are fixed and disclosed in the goal's Formalization Note:
- (P1) $G$ is nonempty. The paper assumes it tacitly and proves $\Gamma \neq \emptyset$ .
- (P2) Interior points are relative-interior points (intrinsicInterior ℝ G). The paper's segment definition makes the equality clause false, and the topological interior makes it vacuous for lower-dimensional $G$ .
- (P3) Uniqueness is stated as the symmetry gives it. The literal "one and only one $\Gamma$ , $\varphi$ with these properties, (5) and equality at interior points" is false: for $G = [0,1]$ , $f \equiv 0$ , the pair $\Gamma' = \{0\}$ , $\varphi'(0) = 0$ also qualifies.
A statement of the goal that asserts only $f^* = f$ on $G$ and drops $G^* = G$ is a different and much weaker theorem; the goal carries the domain identity.
Needed infrastructure: supporting hyperplanes to convex sets at relative-interior points (Mathlib has separation theorems for Fin n → ℝ and the intrinsic interior), affine minorants of convex functions on lower-dimensional domains, and the boundary-limit argument of milestone 6. All of these are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

W. Fenchel, On conjugate convex functions, Canadian Journal of Mathematics 1 (1949), 73–77. https://doi.org/10.4153/CJM-1949-007-x
W. H. Young, On classes of summable functions and their Fourier series, Proceedings of the Royal Society of London A 87 (1912), 225–229. https://doi.org/10.1098/rspa.1912.0076
J.-J. Moreau, Proximité et dualité dans un espace hilbertien, Bulletin de la Société Mathématique de France 93 (1965), 273–299. https://doi.org/10.24033/bsmf.1625
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

12 thms2 active usersReviewed

Functional Analysis Operations Research Optimization·Captain: mikedeng1

On the Douglas–Rachford Splitting Method and the Proximal Point Algorithm for Maximal Monotone Operators: Generalized Douglas–Rachford Splitting Converges Weakly if A+B Has a Zero, Else Is UnboundedResearch Paper

Motivation

Many problems in convex optimization, variational inequalities and equilibrium modelling reduce to finding a point $x$ with $0 \in A x + B x$ , where $A$ and $B$ are maximal monotone operators on a real Hilbert space $\mathcal H$ : for example, minimizing $f + g$ for closed proper convex $f, g$ is the case $A = \partial f$ , $B = \partial g$ . When the resolvent of $A + B$ is hard to evaluate but the resolvents of $A$ and $B$ separately are easy, one uses a splitting method. Douglas–Rachford splitting, introduced for monotone operators by Lions and Mercier (1979) after an alternating-direction scheme of Douglas and Rachford (1956) for the heat equation, is the most widely used one; through its dual form it underlies the alternating direction method of multipliers (ADMM) used throughout large-scale optimization and statistics.

Eckstein and Bertsekas (MIT report LIDS-P-1919, 1989; Mathematical Programming 55, 1992) showed that Douglas–Rachford splitting is a special case of the proximal point algorithm applied to a single derived operator, the splitting operator $S_{\lambda,A,B}$ . This identification lets the convergence theory of the proximal point algorithm transfer to splitting, and yields a generalized method with inexact resolvent evaluations and relaxation.

Timeline.

Minty (1962): a monotone $T$ is maximal iff $I + T$ is onto.
Rockafellar (1976): the proximal point algorithm with variable stepsizes and summable errors converges weakly to a zero.
Lions and Mercier (1979): Douglas–Rachford splitting for maximal monotone $A$ , $B$ ; its map $G_{\lambda,A,B}$ is firmly nonexpansive.
Gol'shtein and Tret'yakov (1979): relaxed proximal iterations with factors $\rho_k \in (0,2)$ , in finite dimension, with a fixed stepsize.
Eckstein and Bertsekas (1989/1992): the splitting operator; Douglas–Rachford as a proximal point method; the generalized proximal point algorithm and the generalized Douglas–Rachford method, including the case with no solution.

Setting

An operator on $\mathcal H$ is a subset $T \subseteq \mathcal H \times \mathcal H$ , with $Tx = \{y \mid (x,y) \in T\}$ ; it may be multivalued and partially defined. Its domain is $\operatorname{dom} T = \{x \mid Tx \ne \emptyset\}$ , its image $\operatorname{im} T$ the projection on the second coordinate, its inverse $T^{-1} = \{(y,x) \mid (x,y) \in T\}$ . Scaling and sum are $cT = \{(x, cy)\}$ and $A + B = \{(x, y+z) \mid (x,y) \in A, (x,z) \in B\}$ ; $I$ is the identity. $T$ is monotone if $\langle x' - x, y' - y\rangle \ge 0$ for all $(x,y),(x',y') \in T$ , and maximal monotone if no other monotone operator strictly contains it. The resolvent is $J_{cT} = (I + cT)^{-1}$ , and $\operatorname{zer} T = \{x \mid 0 \in Tx\}$ . An operator $J$ is firmly nonexpansive if $\|y'-y\|^2 \le \langle x'-x, y'-y\rangle$ for all $(x,y),(x',y') \in J$ .

For $\lambda > 0$ the Douglas–Rachford map is $G_{\lambda,A,B} = J_{\lambda A} \circ (2J_{\lambda B} - I) + (I - J_{\lambda B})$ , and the splitting operator is

S_{\lambda,A,B} = \{(v + \lambda b,\ u - v) \mid (u,b) \in B,\ (v,a) \in A,\ v + \lambda a = u - \lambda b\}.

Its zero set is $Z^*_\lambda = \{u + \lambda b \mid b \in Bu,\ -b \in Au\}$ .

Formalization targets

Goal: Theorem 7 (generalized Douglas–Rachford splitting)

Let $A$ , $B$ be maximal monotone, $\lambda > 0$ , and let $\{z^k\}, \{u^k\}, \{v^k\} \subseteq \mathcal H$ , $\alpha_k, \beta_k \ge 0$ and $\rho_k$ satisfy

\|u^k - J_{\lambda B}(z^k)\| \le \beta_k,\quad \|v^{k+1} - J_{\lambda A}(2u^k - z^k)\| \le \alpha_k,\quad z^{k+1} = z^k + \rho_k (v^{k+1} - u^k),

with $\sum \alpha_k < \infty$ , $\sum \beta_k < \infty$ and $0 < \inf \rho_k \le \sup \rho_k < 2$ . Then

\operatorname{zer}(A+B) \ne \emptyset \implies z^k \rightharpoonup z^* \text{ for some } z^* \in Z^*_\lambda,\qquad \operatorname{zer}(A+B) = \emptyset \implies \{z^k\} \text{ unbounded}.

Milestones

In the paper's order: Minty's theorem (Theorem 1); properties of firmly nonexpansive operators (Lemma 1); the monotone / firmly nonexpansive correspondence (Theorem 2, Corollaries 2.1–2.3); zeros as fixed points of resolvents (Lemma 2); the generalized proximal point algorithm (Theorem 3): weak convergence to a zero of $T$ under summable errors, relaxation in $(0,2)$ and stepsizes bounded away from $0$ , unboundedness when $\operatorname{zer} T = \emptyset$ ; (maximal) monotonicity of $S_{\lambda,A,B}$ (Theorem 4) and firm nonexpansiveness of its resolvent (Corollary 4.1); $\operatorname{zer} S_{\lambda,A,B} = Z^*_\lambda$ (Theorem 5); and $(I + S_{\lambda,A,B})^{-1} = G_{\lambda,A,B}$ (Theorem 6).

Significance

Theorem 7 gives convergence of Douglas–Rachford splitting with both resolvents evaluated inexactly and with over- or under-relaxation, and it characterizes the case without a solution: the iterates are unbounded exactly when $A + B$ has no zero. The relaxed, inexact form is the one implementations actually run, and through Gabay's identification of ADMM with Douglas–Rachford on the dual it is the basis of the paper's Theorem 8, a convergence theorem for a generalized ADMM. Theorem 3, used to prove Theorem 7, is itself a standard reference form of the inexact relaxed proximal point algorithm.

All results here are proved in the paper (one step in the unbounded case of Theorem 3 rests on results of Rockafellar 1969 and 1970 on sums of maximal monotone operators). As of 2026, neither Douglas–Rachford splitting in this generality nor the generalized proximal point algorithm is formalized in Lean or Mathlib. Mathlib has Hilbert spaces, weak topologies and summability, but no theory of maximal monotone operators, Minty's theorem or resolvents. The mission builds that layer and machine-checks the paper's results on it.

Difficulty

The convergence argument cannot be strong: in infinite dimensions the proximal point algorithm need not converge in norm (Güler 1991), so the conclusion is weak convergence, and identifying the weak limit as a zero requires the weak–strong closedness of the graph of a maximal monotone operator. The maximality halves of Theorems 2 and 4 need Minty's theorem, whose proof requires a nontrivial existence argument (all known proofs use Zorn's lemma or an equivalent). The unbounded case of Theorem 3 is a contradiction argument that truncates $T$ by the subdifferential of the indicator of a ball and invokes two external facts: maximality of the sum of two maximal monotone operators under an interiority condition (Rockafellar 1970), and existence of zeros for maximal monotone operators with bounded domain (Rockafellar 1969). Neither is available in Lean. The natural first idea for Theorem 7, iterating the firm nonexpansiveness of $G_{\lambda,A,B}$ , gives neither the error tolerance on both resolvents nor the unbounded case without the full machinery of Theorem 3.

Formalization scope

$\mathcal H$ is a real inner product space that is complete ([CompleteSpace H]). An operator is a map H → Set H. Monotonicity, maximal monotonicity, $\operatorname{dom}$ , $\operatorname{zer}$ and the function-level resolvent predicate IsResolvent are the published definitions ThreeOpSplitting_Convergence_MonotoneOperators; weak convergence is the published WeakTendsto ( $\langle z^k, y\rangle \to \langle z^*, y\rangle$ for every $y$ ).
§2 notions are graph notions (opResolvent, IsFirmlyNonexpansiveOp, ...), so Theorem 2 and Corollary 2.1 can speak of resolvents that are a priori partial or multivalued. In Theorems 3, 6 and 7 the resolvents are maps $J : \mathcal H \to \mathcal H$ with $\lambda^{-1}(x - J x) \in A(Jx)$ for all $x$ , unique by Corollary 2.2.
$S_{\lambda,A,B}$ is defined by its set formula, not as $G_{\lambda,A,B}^{-1} - I$ ; with the latter, Theorem 6 and Corollary 4.1 would be unfoldings. Taking free resolvent functions without the IsResolvent hypothesis would make the iteration unrelated to $A$ and $B$ ; the hypothesis is always present.
$\inf \rho_k > 0$ , $\sup \rho_k < 2$ are encoded as $\exists\, \rho_1, \rho_2$ with $0 < \rho_1 \le \rho_k \le \rho_2 < 2$ ; $\inf c_k > 0$ as $\exists\, c_0 > 0$ , $c_0 \le c_k$ . Summability is Summable with nonnegative terms. Sequences start at $k = 0$ ; $v^0$ is unused. Unboundedness is ¬ Bornology.IsBounded (Set.range z).
Printed slips corrected and disclosed in the items: Theorem 7 states its sequences in $\mathbb R^n$ (read $\mathcal H$ ); Theorem 3 prints $(1 - \rho_k) w^k$ (read $\rho_k w^k$ , as on p. 9 and in the proof) and $(I + cT)^{-1}$ (read $(I + c_k T)^{-1}$ ).
Not included: Corollary 2.4, Corollaries 6.1–6.2 (special cases of Theorem 7), §5 (partial inverses, generalized ADMM). The second sentence of Corollary 6.1 (convergence of $J_{\lambda B}(z^k)$ ) is deliberately excluded: its argument does not transfer weak convergence (Svaiter 2011).
Welcome contributions: Minty's theorem in Hilbert space, the resolvent calculus of §2, and weak-limit lemmas (Opial-type arguments) are reusable well beyond this mission.

Selected references

J. Eckstein and D. P. Bertsekas, On the Douglas–Rachford splitting method and the proximal point algorithm for maximal monotone operators, MIT report LIDS-P-1919, 1989; Mathematical Programming 55 (1992) 293–318. https://doi.org/10.1007/BF01581204
P.-L. Lions and B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16 (1979) 964–979. https://doi.org/10.1137/0716071
G. J. Minty, Monotone (nonlinear) operators in Hilbert space, Duke Math. J. 29 (1962) 341–346. https://doi.org/10.1215/S0012-7094-62-02933-2
R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14 (1976) 877–898. https://doi.org/10.1137/0314056
O. Güler, On the convergence of the proximal point algorithm for convex minimization, SIAM J. Control Optim. 29 (1991) 403–419. https://doi.org/10.1137/0329022
B. F. Svaiter, On weak convergence of the Douglas–Rachford method, SIAM J. Control Optim. 49 (2011) 280–287. https://doi.org/10.1137/100788100

17 thms2 active usersReviewed

Machine Learning Optimization·Captain: mikedeng1

SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives II: The 4n/k Rate of the Averaged Iterate without Strong ConvexityResearch Paper

Motivation

Many problems in statistics and machine learning minimize an average of $n$ losses, one per data point, plus a regularizer: least squares, logistic regression, and their $\ell_1$ - or $\ell_2$ -penalized versions. When $n$ is large, a full gradient costs $n$ component gradients, while stochastic gradient descent, which uses one component per step, needs decreasing step sizes and converges slowly. Incremental gradient methods with variance reduction (SAG, SVRG, SDCA, Finito, MISO) use one component gradient per step but converge at the rate of a full-gradient method.

SAGA (Defazio, Bach and Lacoste-Julien, NIPS 2014, arXiv:1407.0202) is a method of this family. It handles a non-smooth regularizer through its proximal operator, and it comes with a guarantee when the losses are convex but not strongly convex. This mission covers that second guarantee, Theorem 2 of the paper. A companion mission covers the linear rate under strong convexity (Theorem 1, Corollary 1).

Timeline.

2012: SAG (Le Roux, Schmidt and Bach) gives a linear rate for smooth, strongly convex finite sums. Its analysis does not cover a proximal term.
2013: SVRG (Johnson and Zhang) gives a linear rate for the strongly convex case, using periodic full-gradient passes.
2013: SDCA (Shalev-Shwartz and Zhang) works on the dual and needs strong convexity.
2014: Prox-SVRG (Xiao and Zhang, arXiv:1403.4699) extends SVRG to composite objectives. Its key inequality is reused by SAGA's Theorem 2.
2014: SAGA proves both a linear rate under strong convexity and an $O(n/k)$ rate for the averaged iterate under convexity alone, for composite objectives.

Setting

Let $d\ge 0$ and $n\ge 1$ . The components $f_1,\dots,f_n:\mathbb R^d\to\mathbb R$ are convex and differentiable, and each gradient $f_i'$ is $L$ -Lipschitz ( $L>0$ ). Write

f(x)=\frac1n\sum_{i=1}^n f_i(x),\qquad f'(x)=\frac1n\sum_{i=1}^n f_i'(x).

The regularizer $h:\mathbb R^d\to\mathbb R$ is convex but possibly non-differentiable. The objective is the composite function $F=f+h$ , and $x^*$ is any minimizer of $F$ . Minimizers need not be unique, and $f'(x^*)$ need not vanish.

The proximal operator with parameter $\gamma>0$ is

\mathrm{prox}_\gamma^h(y)=\arg\min_{x\in\mathbb R^d}\Big\{h(x)+\frac1{2\gamma}\|x-y\|^2\Big\}.

SAGA keeps an iterate $x^k$ and a table of points $\phi_1^k,\dots,\phi_n^k$ , initialized as $\phi_i^0=x^0$ . At step $k+1$ it draws an index $j$ uniformly from $\{1,\dots,n\}$ , independently of the past, and sets

w^{k+1}=x^k-\gamma\Big[f_j'(x^k)-f_j'(\phi_j^k)+\frac1n\sum_{i=1}^n f_i'(\phi_i^k)\Big],\qquad x^{k+1}=\mathrm{prox}_\gamma^h(w^{k+1}).

It then sets $\phi_j^{k+1}=x^k$ and leaves the other table entries unchanged. The averaged iterate is $\bar x^k=\frac1k\sum_{t=1}^k x^t$ , which excludes $x^0$ .

Formalization targets

Goal: Theorem 2 (p. 11)

With step size $\gamma=1/(3L)$ , for every $k\ge1$ ,

\mathbb E\big[F(\bar x^k)\big]-F(x^*)\le\frac{4n}{k}\Big[\frac{2L}{n}\|x^0-x^*\|^2+f(x^0)-\langle f'(x^*),x^0-x^*\rangle-f(x^*)\Big].

The expectation is over the indices $j^1,\dots,j^k$ . The constants are those printed in the paper.

Milestones (in attack order)

Lemma 1 (p. 6) is an inner-product bound for averages of $\mu$ -strongly convex functions with $L$ -Lipschitz gradients. It is stated for $\mu\ge0$ , and Theorem 2 uses the case $\mu=0$ .
Lemma 2 (p. 7): $\frac1n\sum_i\|f_i'(\phi_i)-f_i'(x^*)\|^2\le 2L\big[\frac1n\sum_i f_i(\phi_i)-f(x^*)-\frac1n\sum_i\langle f_i'(x^*),\phi_i-x^*\rangle\big]$ .
The bound on $\Delta$ (p. 12). Write $\Delta=-\frac1\gamma(w^{k+1}-x^k)-f'(x^k)$ for the gradient error. For every $\beta>0$ , $\mathbb E\|\Delta\|^2\le(1+\beta^{-1})\mathbb E\|f_j'(\phi_j^k)-f_j'(x^*)\|^2+(1+\beta)\mathbb E\|f_j'(x^k)-f_j'(x^*)\|^2$ .
The prox-SVRG inequality (p. 12): $\alpha\mathbb E\|x^{k+1}-x^*\|^2\le\alpha\|x^k-x^*\|^2-2\alpha\gamma\mathbb E[F(x^{k+1})-F(x^*)]+2\alpha\gamma^2\mathbb E\|\Delta\|^2$ .
The one-step Lyapunov decrease (p. 12): $\mathbb E[T^{k+1}]-T^k\le-\frac1{4n}\mathbb E[F(x^{k+1})-F(x^*)]$ . Here $T(x,\phi)=\frac1n\sum_i f_i(\phi_i)-f(x^*)-\frac1n\sum_i\langle f_i'(x^*),\phi_i-x^*\rangle+(c+\alpha)\|x-x^*\|^2$ , with $c=\frac{3L}{2n}$ and $\alpha=\frac{3L}{8n}$ .

In milestones 3–5, $\mathbb E$ is the expectation over the single index $j$ of the next step, given the current state.

Significance

The result. Theorem 2 shows that one method, with a step size that depends only on $L$ , covers composite problems that are not strongly convex. Examples are $\ell_1$ -regularized least squares and logistic regression without a ridge term. On these problems the method converges in expected objective value at rate $O(n/k)$ . SAG has no proximal analysis, and SDCA requires strong convexity. With the same step size $1/(3L)$ , the paper also states adaptivity to strong convexity, so no strong convexity constant has to be known in advance. The bound is in terms of $T^0$ , a quantity computable from the starting point.

Formalizing it. The result is proved on paper, but the proof is not self-contained. Its central inequality (milestone 4) is quoted from the prox-SVRG analysis of Xiao and Zhang, with only the remark that their argument uses $\mathbb E[\Delta]=0$ . A machine-checked proof must therefore reconstruct that argument for SAGA's estimator. To our knowledge, no machine-checked proof of SAGA, SVRG or prox-SVRG exists in Lean or Mathlib. The mission also produces reusable statements about convex functions with Lipschitz gradients (Lemmas 1 and 2) and an explicit finite model of a randomized incremental method.

Difficulty

The naive approach applies the non-expansiveness of the proximal operator to $\|x^{k+1}-x^*\|^2$ , as in the strongly convex proof. That bounds distances, but it produces no term in $F(x^{k+1})-F(x^*)$ . Without strong convexity, the distance terms cannot be traded for function values, so the argument yields no rate.

The function-value term comes from the prox-SVRG inequality (milestone 4), which the paper does not prove. Its difficulty is that $x^{k+1}$ depends on the same random index as $\Delta$ , so the cross term between them does not vanish in expectation even though $\mathbb E[\Delta]=0$ . A second difficulty is bookkeeping: $w^{k+1}$ uses the old table, the table entry $j$ receives $x^k$ and not $x^{k+1}$ , and the constants must make three coefficients vanish exactly. A final step converts the bound on $\frac1k\sum_t\mathbb E[F(x^t)]$ into a bound on $\mathbb E[F(\bar x^k)]$ , which requires Jensen's inequality for the convex $F$ .

Formalization scope

Space and indices. Points live in EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with $n\ge1$ .
Gradients and smoothness. The gradients are given maps f' with HasGradientAt (f i) (f' i x) x at every point. Smoothness is the Lipschitz bound $\|f_i'(x)-f_i'(y)\|\le L\|x-y\|$ .
Convexity. Convexity is ConvexOn ℝ Set.univ. Lemma 1 uses StrongConvexOn Set.univ μ, whose modulus $\frac\mu2\|x-y\|^2$ is the paper's.
The regularizer. $h$ is real-valued and convex. Extended-valued regularizers such as indicator functions are outside the statement.
The proximal map. The proximal operator enters as any map $P$ such that $P(y)$ minimizes $h(z)+\frac1{2\gamma}\|z-y\|^2$ for every $y$ . For convex $h$ this determines $P=\mathrm{prox}_\gamma^h$ .
State and expectation. The state is the pair $(x^k,\phi^k)$ . The expectation over $k$ steps is the uniform average over the $n^k$ index sequences, which is exactly the law of $k$ independent uniform indices.

Two trivializations are excluded. The averaged-iterate bound carries $k\ge1$ , since at $k=0$ the factor $4n/k$ collapses to $0$ . The left side is $F$ evaluated at the averaged point, not the average of $F(x^t)$ , which is a weaker intermediate step.

A complete development needs the descent lemma and co-coercivity for convex functions with Lipschitz gradients, the characterization and non-expansiveness of the proximal operator, and finite-sum manipulations over index sequences. The lemmas on smooth convex functions and on proximal operators are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, a reusable proximal-operator library, and the telescoping argument for the goal.

Selected references

A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NIPS 2014. arXiv:1407.0202
L. Xiao, T. Zhang, A Proximal Stochastic Gradient Method with Progressive Variance Reduction, SIAM J. Optim. 24(4), 2014. arXiv:1403.4699
N. Le Roux, M. Schmidt, F. Bach, A Stochastic Gradient Method with an Exponential Convergence Rate for Finite Training Sets, NIPS 2012. arXiv:1202.6258
R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NIPS 2013. NeurIPS proceedings
S. Shalev-Shwartz, T. Zhang, Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization, JMLR 14, 2013. arXiv:1209.1873
Y. Nesterov, Introductory Lectures on Convex Optimization, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9

11 thms2 active usersReviewed

Operations Research Optimization Reinforcement Learning·Captain: mikedeng1

Twice Regularized MDPs and the Equivalence Between Robustness and Regularization 1: The Robust Value Function Is the Optimum of a Policy- and Value-Regularized Convex ProgramResearch Paper

Motivation

A Markov decision process (MDP) is solved for one model of its dynamics and rewards, but in practice that model is estimated from data, and a policy that is optimal for the estimate can perform poorly on the true system (Mannor et al., 2007). Robust MDPs address this by evaluating a policy against the worst model in an uncertainty set $\mathcal U$ (Iyengar, 2005; Nilim and El Ghaoui, 2005; Wiesemann, Kuhn and Rustem, 2013). Robust planning, however, solves an inner optimization over $\mathcal U$ at every Bellman update, which is expensive and does not scale to learning settings.

A separate line of work regularizes the policy (entropy, KL, Tsallis penalties) and observes empirically that regularized policies are robust to perturbations (Geist, Scherrer and Pietquin, 2019). Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) make this precise: for uncertainty sets centred at a nominal model, the robust value function is the solution of a regularized problem posed on the nominal model alone, with a regularizer that is the support function of the uncertainty set. This mission formalizes that equivalence: Proposition 3.1, Theorem 3.1 and Theorem 4.1 of the paper.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite sets of states and actions, $\mathcal A$ nonempty, and $\mathcal X := \mathcal S\times\mathcal A$ . Fix a discount factor $\gamma\in(0,1)$ and a strictly positive initial distribution $\mu_0\in\Delta_{\mathcal S}$ . A transition kernel $P$ assigns to every pair $(s,a)$ a probability distribution $P(\cdot\mid s,a)$ on $\mathcal S$ ; a reward is $r\in\mathbb R^{\mathcal X}$ . A policy $\pi\in\Delta_{\mathcal A}^{\mathcal S}$ assigns to every state an action distribution $\pi_s$ .

For $v\in\mathbb R^{\mathcal S}$ write $r^\pi(s) = \sum_a\pi_s(a)r(s,a)$ , $P^\pi(s'\mid s) = \sum_a\pi_s(a)P(s'\mid s,a)$ , and define the evaluation Bellman operator

T^\pi_{(P,r)}v := r^\pi + \gamma P^\pi v .

The inner product on $\mathbb R^{\mathcal S}$ is $\langle v,\mu\rangle = \sum_s v(s)\mu(s)$ , and the support function of a set $C\subseteq\mathbb R^{\iota}$ is $\sigma_C(y) = \max_{a\in C}\langle a,y\rangle$ .

Given a set $\mathcal U$ of models $(P,r)$ , the robust Bellman operator is

[T^{\pi,\mathcal U}v](s) := \min_{(P,r)\in\mathcal U}T^\pi_{(P,r)}v(s),

and the robust value function $v^{\pi,\mathcal U}$ is its fixed point. Around a nominal model $(P_0,r_0)$ , an s-rectangular uncertainty set $\mathcal U = (P_0+\mathcal P)\times(r_0+\mathcal R)$ is given by sets $\mathcal P_s\subseteq\mathbb R^{\mathcal X}$ and $\mathcal R_s\subseteq\mathbb R^{\mathcal A}$ , one per state: its models are $P(s'\mid s,a) = P_0(s'\mid s,a)+P_s(s',a)$ and $r(s,a) = r_0(s,a)+r_s(a)$ , with $P_s\in\mathcal P_s$ and $r_s\in\mathcal R_s$ chosen independently for each $s$ . Finally $[v\cdot\pi_s](s',a) := v(s')\pi_s(a)$ .

Formalization targets

Goal: Theorem 4.1 (general robust MDP)

For $\mathcal U = (P_0+\mathcal P)\times(r_0+\mathcal R)$ and every policy $\pi$ , $T^{\pi,\mathcal U}$ has a unique fixed point $v^{\pi,\mathcal U}$ , and it is the optimal solution of

\max_{v\in\mathbb R^{\mathcal S}}\langle v,\mu_0\rangle\quad\text{s.t.}\quad v(s)\le T^\pi_{(P_0,r_0)}v(s)-\sigma_{\mathcal R_s}(-\pi_s)-\sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)\quad\forall s\in\mathcal S. \tag{2}

Milestones

Proposition 3.1. For any uncertainty set $\mathcal U = \mathcal P\times\mathcal R$ with $\mathcal P$ a nonempty compact set of kernels and $\mathcal R$ a nonempty compact set of rewards, $v^{\pi,\mathcal U}$ is the optimal solution of the robust program $\max_{v}\langle v,\mu_0\rangle\quad\text{s.t.}\quad v\le T^\pi_{(P,r)}v\ \ \forall(P,r)\in\mathcal U. \tag{$P_{\mathcal U}$}$
Theorem 3.1. For $\mathcal U=\{P_0\}\times(r_0+\mathcal R)$ , $v^{\pi,\mathcal U}$ is the optimal solution of $\max_v\langle v,\mu_0\rangle$ s.t. $v(s)\le T^\pi_{(P_0,r_0)}v(s)-\sigma_{\mathcal R_s}(-\pi_s)$ for all $s$ .
Robust counterpart (proof of Theorem 4.1, App. B.1). For every $v$ and $s$ ,

\max_{(P,r)\in\mathcal U}\{v(s)-r^\pi(s)-\gamma P^\pi v(s)\} = \sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)+\sigma_{\mathcal R_s}(-\pi_s)+v(s)-T^\pi_{(P_0,r_0)}v(s).

Theorem 3.1 is the special case $\mathcal P_s=\{0\}$ of the goal; it is listed separately because it is the paper's statement that policy regularization is equivalent to reward uncertainty.

Significance

The goal says that a robust MDP with s-rectangular uncertainty in both reward and transitions is a regularized MDP on the nominal model, with two regularizers: a policy regularizer $\sigma_{\mathcal R_s}(-\pi_s)$ coming from reward uncertainty, and a regularizer $\sigma_{\mathcal P_s}(-\gamma v\cdot\pi_s)$ coming from transition uncertainty that depends on both the policy and the value. For ball-shaped sets these support functions are explicit ( $\alpha^r_s\|\pi_s\|$ and $\alpha^P_s\gamma\|v\|\|\pi_s\|$ , Corollary 4.1 of the paper), which leads to the twice regularized (R²) Bellman operators of Section 5 and to robust planning at the cost of non-robust planning. Theorem 3.1 also explains why standard policy regularizers (negative entropy, KL, Tsallis) yield robustness: each is the support function of a reward uncertainty set.

The results are proved in the paper (appendices A.1, A.2, B.1); none has a machine-checked proof. The mission produces formal statements and proofs of the equivalence, the robust Bellman operator's fixed-point theory for stochastic policies and general compact uncertainty sets, and a closed-form robust counterpart that later R² results can import. The paper's printed proof of Proposition 3.1 treats $T^{\pi,\mathcal U}$ as linear in one step; a formal proof settles the statement independently of that step.

Difficulty

The obvious argument reads Proposition 3.1 as linear-programming duality, as for a single MDP. That fails: $T^{\pi,\mathcal U}$ is a minimum of affine maps, hence concave and not affine, and the feasible set of $(P_{\mathcal U})$ is an intersection of infinitely many half-space systems; the argument has to go through monotonicity and contraction of $T^{\pi,\mathcal U}$ , which in turn requires every model in $\mathcal U$ to be a genuine transition kernel. For the goal, the paper invokes Fenchel–Rockafellar duality to evaluate the inner maximum; the work in Lean is to separate the maximum over the product set $\mathcal U$ into per-state maxima, which needs the s-rectangular structure and attainment of every maximum (compactness), and to track the index order of the perturbation $P_s(s',a)$ against the kernel $P(s'\mid s,a)$ .

Formalization scope

States and actions are finite types, A nonempty; values are S → ℝ ordered pointwise; a transition array is P : S → A → S → ℝ with P s a s' $=P(s'\mid s,a)$ , and the kernel property is the published IsTransitionKernel; $P^\pi(s'\mid s)$ is the published InducedTransition. A policy has π s ∈ stdSimplex ℝ A for every s.
Perturbations $P_s$ are functions S × A → ℝ indexed $(s',a)$ , as in the paper's $\mathbb R^{\mathcal X}$ ; rewards perturbations are A → ℝ.
Minima and maxima (in $T^{\pi,\mathcal U}$ and in $\sigma$ ) are real sInf/sSup. Every theorem assumes the sets nonempty and compact, so these are attained; nothing is quantified over an unbounded set.
The robust value function is encoded as the fixed point of $T^{\pi,\mathcal U}$ , and each theorem asserts its existence and uniqueness. The paper's definition $v^{\pi,\mathcal U}(s)=\min_{(P,r)\in\mathcal U}v^\pi_{(P,r)}(s)$ (p. 4) coincides with it for rectangular sets by a cited result; the proofs use only the fixed-point property. For the non-rectangular sets of Proposition 3.1 the pointwise minimum can be strictly larger than the fixed point and is then not the optimum of $(P_{\mathcal U})$ , so the fixed point is the object the proposition is true for.
"The optimal solution" means: feasible, objective-maximal, and the unique maximizer (uniqueness uses $\mu_0>0$ ).
Disclosed hypotheses: $\mathcal U=\mathcal P\times\mathcal R$ with $\mathcal P$ , $\mathcal R$ nonempty and compact and every transition in $\mathcal P$ a kernel (Prop. 3.1); $\mathcal P_s$ , $\mathcal R_s$ nonempty and compact and every perturbed row $P_0(\cdot\mid s,a)+P_s(\cdot,a)$ in $\Delta_{\mathcal S}$ (Thm 4.1); reward sets rectangular in Thm 3.1, as its proof uses. These are the robust-MDP standing assumptions of p. 4 ( $\mathcal P\subseteq\Delta^{\mathcal X}_{\mathcal S}$ ) and what makes "min" and "max" well defined.
Not drafted: Corollary 4.1, whose ℓ²-ball $\mathcal P_s$ contains perturbations that leave the simplex, so $P_0+\mathcal P$ is not a set of kernels; Corollary 3.1 and Proposition 3.2 (consequences after the goal; Prop. 3.2 depends on an unspecified policy parametrization).
A formalization that asserts only that the feasible sets of $(P_{\mathcal U})$ and (2) coincide, or that drops the kernel condition or the existence of the fixed point, does not count: the goal names the robust value function and its optimality.
"Convex" in the statement of Theorem 4.1 is descriptive and is not part of the formal goal.

Contributions welcome: the monotone-contraction fixed-point lemma for $T^{\pi,\mathcal U}$ and the per-state separation of maxima over rectangular sets are reusable for any robust MDP mission.

Selected references

E. Derman, M. Geist, S. Mannor, Twice regularized MDPs and the equivalence between robustness and regularization, NeurIPS 2021. arXiv:2110.06267v1
G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. doi:10.1287/moor.1040.0129
A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. doi:10.1287/opre.1050.0216
W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. doi:10.1287/moor.1120.0566
M. Geist, B. Scherrer, O. Pietquin, A theory of regularized Markov decision processes, ICML 2019. PMLR 97
S. Mannor, D. Simester, P. Sun, J. N. Tsitsiklis, Bias and variance approximation in value function estimates, Management Science 53(2), 2007. doi:10.1287/mnsc.1060.0614

8 thms2 active usersReviewed

Machine Learning Optimization·Captain: mikedeng1

SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives I: Linear Convergence under Strong ConvexityResearch Paper

Motivation

Many problems in machine learning and statistics are finite sums: an empirical risk $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ over $n$ data points, often plus a regulariser $h$ such as an $\ell_1$ penalty. When $n$ is large, a full gradient of $f$ costs $n$ component gradients, while stochastic gradient descent uses one component per step but converges only sublinearly because its gradient estimate has non-vanishing variance. Incremental gradient methods with variance reduction keep the per-step cost of one component gradient and still converge linearly on strongly convex problems.

SAGA, introduced by Defazio, Bach and Lacoste-Julien at NIPS 2014 (arXiv:1407.0202), is one of the standard methods of this family, alongside SAG, SVRG, SDCA and Finito/MISO. It keeps a table of past component gradients and handles a non-smooth regulariser through its proximal operator.

Timeline. Le Roux, Schmidt and Bach (2012) gave SAG the first linear rate for strongly convex finite sums at the cost of one gradient per step. Shalev-Shwartz and Zhang (2013) proved linear rates for SDCA, a dual method. Johnson and Zhang (2013) introduced SVRG, with periodic full-gradient passes; Xiao and Zhang (2014) extended it to composite objectives (prox-SVRG). SAGA (2014) combines an unbiased SVRG-style estimator with a SAG-style table, and proves a linear rate in the composite strongly convex case with a simple Lyapunov argument.

Setting

Let $\mathbb R^d$ carry the Euclidean inner product. There are $n\ge1$ differentiable components $f_1,\dots,f_n:\mathbb R^d\to\mathbb R$ with gradients $f_i'$ . Each $f_i$ is $\mu$ -strongly convex ( $\mu>0$ ): $f_i(ax+by)\le af_i(x)+bf_i(y)-ab\frac\mu2\|x-y\|^2$ for $a,b\ge0$ , $a+b=1$ . Each gradient is $L$ -Lipschitz: $\|f_i'(x)-f_i'(y)\|\le L\|x-y\|$ . Write $f=\frac1n\sum_i f_i$ and $f'=\frac1n\sum_i f_i'$ . The regulariser $h:\mathbb R^d\to\mathbb R$ is convex, and the goal is to minimise the composite objective $F=f+h$ ; $x^*$ denotes its minimiser, which is unique.

The proximal operator with step $\gamma>0$ is

\operatorname{prox}^h_\gamma(y)=\operatorname*{argmin}_{x}\Big\{h(x)+\tfrac1{2\gamma}\|x-y\|^2\Big\}.

SAGA keeps an iterate $x^k$ and points $\phi_1^k,\dots,\phi_n^k$ at which the stored gradients $f_i'(\phi_i^k)$ were taken. It starts from $x^0$ with $\phi_i^0=x^0$ . At iteration $k+1$ it draws $j$ uniformly from $\{1,\dots,n\}$ , independently of the past, and sets

w^{k+1}=x^k-\gamma\Big[f_j'(x^k)-f_j'(\phi_j^k)+\frac1n\sum_{i=1}^n f_i'(\phi_i^k)\Big],\qquad x^{k+1}=\operatorname{prox}^h_\gamma(w^{k+1}),

then $\phi_j^{k+1}=x^k$ , with every other entry unchanged.

The analysis uses the Lyapunov function

T(x,\{\phi_i\})=\frac1n\sum_i f_i(\phi_i)-f(x^*)-\frac1n\sum_i\langle f_i'(x^*),\phi_i-x^*\rangle+c\|x-x^*\|^2 .

Formalization targets

Goal: Corollary 1 (p. 8)

With $\gamma=\frac1{2(\mu n+L)}$ , for every $k\ge0$ ,

\mathbb E\|x^k-x^*\|^2\le\Big(1-\frac{\mu}{2(\mu n+L)}\Big)^k\Big[\|x^0-x^*\|^2+\frac{n}{\mu n+L}\big(f(x^0)-\langle f'(x^*),x^0-x^*\rangle-f(x^*)\big)\Big],

where the expectation is over the indices drawn in the first $k$ iterations. The constants are the paper's.

Theorem 1 (p. 7)

With $\gamma$ as above, $c=\frac1{2\gamma(1-\gamma\mu)n}$ and $\kappa=\frac1{\gamma\mu}$ , for every state $(x^k,\{\phi^k_i\})$ ,

\mathbb E\big[T^{k+1}\big]\le\Big(1-\frac1\kappa\Big)T^k ,

with the expectation over the next index only.

Supporting lemmas

Lemma 4 (p. 10), a lower bound combining strong convexity and smoothness; Lemma 1 (pp. 6–7), its average over the components; Lemma 2 (p. 7), which bounds the stale-gradient variance by the table part of $T$ ; and Lemma 3 (p. 7), a second-moment bound for the SAGA step.

Significance

The result. Corollary 1 gives an $\varepsilon$ -accurate iterate in expectation after $O\big((n+L/\mu)\log(1/\varepsilon)\big)$ component-gradient evaluations. This is the complexity of full-gradient descent with the condition number decoupled from $n$ , and it holds in the composite setting, so it covers the lasso and elastic-net problems that SAG's analysis does not reach. The paper notes that the rate improves on the published rates of SAG and SVRG and is within a factor 2 of SDCA's. Theorem 1 is the template of later Lyapunov analyses of variance-reduced methods.

Formalizing it. The result has been proved since 2014, and no machine-checked proof is known to this mission. The work left is to formalize the known proof: the convexity inequalities (Lemmas 4, 1, 2), the variance computation (Lemma 3), the one-step contraction (Theorem 1), and the passage from conditional to total expectation along the random index sequence (Corollary 1). The paper's Lemma 3 has a sign misprint, which the formalization corrects; see the scope section.

Difficulty

The obvious argument for SGD-type methods bounds $\mathbb E\|x^{k+1}-x^*\|^2$ in terms of $\|x^k-x^*\|^2$ alone. That fails here: the variance of the SAGA estimator depends on the stale table points $\phi_i^k$ , which can be far from $x^*$ even when $x^k$ is close. One needs a potential that also measures the table. Balancing the terms of $T$ then requires the four round-bracket coefficients in the paper's display (10) to be non-positive for the specific $\gamma$ , $c$ and an auxiliary $\beta=(2\mu n+L)/L$ . Checking these coefficients is routine but long algebra in $\mu$ , $L$ , $n$ . The composite case adds one step: since $f'(x^*)\neq0$ in general, the argument goes through the fixed-point identity $x^*=\operatorname{prox}^h_\gamma(x^*-\gamma f'(x^*))$ and the non-expansiveness of the proximal operator, neither of which is a numbered result of the paper.

Formalization scope

Space and data. The space is EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with 0 < n. The gradients $f_i'$ are given maps with HasGradientAt (f i) (f' i x) x. Strong convexity is Mathlib's StrongConvexOn Set.univ μ, whose modulus $\frac\mu2\|x-y\|^2$ is the paper's.
Regulariser and minimiser. $h$ is real-valued and convex; extended-valued regularisers are out of scope, as on the page. A minimiser $x^*$ of $f+h$ is a hypothesis.
Proximal operator. It is any map $P$ such that $P(y)$ minimises $h(x)+\frac1{2\gamma}\|x-y\|^2$ for every $y$ (IsProxPoint). The minimiser is unique, so $P$ is $\operatorname{prox}^h_\gamma$ .
State and expectation. The state is the pair $(x,\phi)$ . The run after $k$ steps is a deterministic function of the index sequence in Fin k → Fin n. The expectation in Corollary 1 is the average over all $n^k$ sequences, which is exactly the law of $k$ independent uniform indices; no measure theory is involved. Theorem 1's conditional expectation is the average over the next index.
Constants and corrections. Constants are as printed and fixed, not "for some constant" and not "for all small enough steps". Lemma 4 carries the hypothesis $\mu<L$ , which its fractions $1/(L-\mu)$ require. Lemma 3 is stated with $+\gamma f'(x^*)$ , as in its proof and its use in Theorem 1; the printed $-\gamma f'(x^*)$ is false whenever $f'(x^*)\neq0$ .
Trivializing formalizations, ruled out. Taking the proximal step as merely non-expansive, fixing an index sequence instead of averaging over all of them, measuring $x^*$ against $f$ instead of $f+h$ , or restricting Theorem 1 to reachable states changes the theorem and is excluded.
Infrastructure. A complete development needs:
- the co-coercivity inequality for convex functions with Lipschitz gradient;
- existence, uniqueness and non-expansiveness of the proximal map of a finite convex function;
- the optimality condition $x^*=\operatorname{prox}^h_\gamma(x^*-\gamma f'(x^*))$ ;
- finite-sum variance identities.
These pieces are reusable well beyond SAGA, by SVRG, SAG and proximal-gradient analyses. Contributions of any of them, or of proofs of the individual milestones, are welcome.

Selected references

A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NIPS 2014. arXiv:1407.0202
N. Le Roux, M. Schmidt, F. Bach, A Stochastic Gradient Method with an Exponential Convergence Rate for Finite Training Sets, NIPS 2012. arXiv:1202.6258
R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NIPS 2013. NeurIPS proceedings
L. Xiao, T. Zhang, A Proximal Stochastic Gradient Method with Progressive Variance Reduction, SIAM J. Optim. 24(4), 2014. arXiv:1403.4699
S. Shalev-Shwartz, T. Zhang, Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization, JMLR 14, 2013. arXiv:1209.1873
Y. Nesterov, Introductory Lectures on Convex Optimization, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9

11 thms2 active usersReviewed

Linear algebra Operations Research Optimization·Captain: mikedeng1

A Nonlinear Programming Algorithm for Solving Semidefinite Programs via Low-rank Factorization: A Regular Local Minimum That Stays Locally Minimal After Adding a Zero Column Solves the SDPResearch Paper

Motivation

Semidefinite programs (SDPs) arise as convex relaxations of combinatorial problems such as maximum cut and the Lovász theta function, and in control and eigenvalue optimization. Interior-point methods solve them reliably but manipulate dense $n\times n$ matrices, which limits the size of the instances they can handle. Burer and Monteiro (Math. Program. 95 (2003)) proposed replacing the matrix variable $X\succeq 0$ by a factorization $X=RR^{T}$ with $R$ having only $r$ columns, and solving the resulting nonconvex program by a first-order augmented Lagrangian method. The approach rests on a theorem of Barvinok (1995) and Pataki (1998): an SDP with $m$ linear constraints has an optimal solution of rank $r$ with $r(r+1)/2\le m$ , so a small number of columns suffices.

Because the factorized problem is nonconvex, a local minimum it returns is not automatically a solution of the SDP. Section 2 of the paper gives conditions under which it is. This mission formalizes those conditions, culminating in Proposition 2.5, which justifies the paper's strategy of increasing the rank one column at a time.

Setting

For real $p\times q$ matrices, the trace inner product is $A\bullet B=\operatorname{trace}(A^{T}B)$ . The data are symmetric matrices $C, A_1,\dots,A_m\in\mathcal S^n$ and a vector $b\in\mathbb R^m$ . The primal SDP and dual SDP are

\text{(1)}\quad \min\{C\bullet X : A_i\bullet X=b_i,\ i=1,\dots,m,\ X\succeq0\},\qquad \text{(3)}\quad \max\Big\{b^{T}y : S=C-\sum_{i=1}^m y_iA_i,\ S\succeq0\Big\}.

The standing assumptions of the paper are that $A_1,\dots,A_m$ are linearly independent and that there are feasible $X^*$ and $(S^*,y^*)$ with $C\bullet X^*=b^{T}y^*$ .

For a positive integer $r\le n$ , the low-rank program is

(N_r)\qquad \min\{C\bullet(RR^{T}) : A_i\bullet(RR^{T})=b_i,\ i=1,\dots,m,\ R\in\mathbb R^{n\times r}\}.

Its Lagrangian is $L(R,y)=C\bullet(RR^{T})-\sum_i y_i(A_i\bullet(RR^{T})-b_i)$ , and $S(y)=C-\sum_i y_iA_i$ . A feasible $R$ is a local minimum if it minimizes the objective among nearby feasible points; it is a regular point if $A_1R,\dots,A_mR$ are linearly independent; it is a stationary point with multiplier $y$ if $\nabla_RL(R,y)=0$ . The injection of $R\in\mathbb R^{n\times r}$ is $\hat R=[\,R\ \ 0\,]\in\mathbb R^{n\times(r+1)}$ , obtained by appending a zero column.

Formalization targets

Goal: Proposition 2.5

Let $r<n$ and let $R^*$ be a regular local minimum of $(N_r)$ with multiplier $y^*$ , $S^*=S(y^*)$ , $S^*R^*=0$ . If $\hat R$ is a local minimum of $(N_{r+1})$ , then

X^*=R^*(R^*)^{T}\ \text{solves (1)}\quad\text{and}\quad (S^*,y^*)\ \text{solves (3)}.

Milestones

The derivative formulas (9): $\nabla_R(A_i\bullet(RR^T)-b_i)=2A_iR$ , $\nabla_RL(R,y)=2SR$ , and $L''_{RR}(R,y)[D,D]=2S\bullet(DD^T)$ .
Proposition 2.3: at a regular local minimum of $(N_r)$ there is a unique $y^*$ with $S^*R^*=0$ , and $S^*\bullet(DD^T)\ge0$ for every $D$ with $A_iR^*\bullet D=0$ for all $i$ .
Proposition 2.1: feasible $X$ and $(S,y)$ are simultaneously optimal if and only if $X\bullet S=0$ .
Proposition 2.4: a stationary point of $(N_r)$ whose $S^*$ is positive semidefinite gives optimal $X^*=R^*R^{*T}$ and $(S^*,y^*)$ .

Significance

Proposition 2.5 is a certificate of global optimality for a nonconvex problem obtained from local information alone. It is the basis of the rank-increase scheme described on p. 8 of the paper: compute a local minimum of $(N_r)$ for a small $r$ ; if the zero-column extension is still a local minimum of $(N_{r+1})$ , the current point solves the SDP; otherwise a better point of $(N_{r+1})$ exists and $r$ is increased. Proposition 2.4 gives the companion test, valid for every $r$ : positive semidefiniteness of the multiplier matrix at a stationary point. These statements underlie the later convergence analysis of the method (Burer & Monteiro 2005) and the literature on benign landscapes of low-rank SDP formulations (Boumal, Voroninski & Bandeira 2016).

The results are proved in the paper. What this mission adds is a machine-checked version of the full chain from the standard-form SDP to the rank-increase certificate, including the matrix calculus (9), the first- and second-order necessary conditions for an equality-constrained program over rectangular matrices, and SDP complementary slackness in standard form. No machine-checked proof of these results is recorded in Mathlib or on the platform.

Difficulty

The SDP side (Propositions 2.1 and 2.4) is linear algebra: weak duality and the fact that the trace inner product of two positive semidefinite matrices is nonnegative. The substance lies in Proposition 2.3. The feasible set of $(N_r)$ is a variety cut out by $m$ quadratic equations, and the multiplier rule and, especially, the second-order necessary condition require a constraint qualification and a curve in the feasible set realizing every tangent direction. Mathlib provides a first-order Lagrange multiplier rule, but not the second-order condition on the tangent space. A naive attempt to read Proposition 2.5 off Proposition 2.4 fails: local minimality of $R^*$ alone does not make $S^*$ positive semidefinite (when $r$ is below the minimal optimal rank, it is not); the hypothesis on $(N_{r+1})$ is indispensable.

Formalization scope

Matrices are Matrix (Fin n) (Fin r) ℝ with 0-based indices. The trace inner product is frob A B = trace(Aᵀ * B), defined for rectangular matrices. The data carry explicit symmetry hypotheses C.IsSymm and (A i).IsSymm; without them the formulas (9) are false. Primal feasibility uses Mathlib's PosSemidef, which over $\mathbb R$ includes symmetry. Optimality for (1) and (3) is defined relative to their entire feasible sets. The standing assumptions are a separate predicate carried as a hypothesis by Propositions 2.1, 2.3, 2.4 and 2.5, and every statement about $(N_r)$ carries $0<r$ and $r\le n$ (or $r<n$ ). Gradients are Fréchet derivatives under the Frobenius norm, identified with matrices through the trace inner product; local minima use IsLocalMinOn on the feasible set of $(N_r)$ together with feasibility. The injection appends the zero column as the last column.

The statement admits several trivializing encodings, all excluded here: optimality defined relative to the factorized feasible set instead of the whole SDP, an empty or unconstrained $(N_r)$ (an unconstrained local minimum or a local minimum without feasibility), a stationarity notion that already includes $S\succeq0$ , and an injection other than the zero-column extension.

A complete development needs the matrix calculus of $R\mapsto RR^{T}$ , a second-order necessary optimality condition under linear independence of the constraint gradients, and standard-form SDP weak duality and complementary slackness; all of these are reusable well beyond this mission. Proofs of individual milestones, in particular the derivative formulas and Proposition 2.4, are welcome independently of the goal.

Selected references

S. Burer and R. D. C. Monteiro, A nonlinear programming algorithm for solving semidefinite programs via low-rank factorization, Mathematical Programming 95 (2003), 329–357. https://doi.org/10.1007/s10107-002-0352-8 (statements cited from the authors' manuscript of March 9, 2001)
A. Barvinok, Problems of distance geometry and convex properties of quadratic maps, Discrete & Computational Geometry 13 (1995), 189–202. https://doi.org/10.1007/BF02574037
G. Pataki, On the rank of extreme matrices in semidefinite programs and the multiplicity of optimal eigenvalues, Mathematics of Operations Research 23 (1998), 339–358. https://doi.org/10.1287/moor.23.2.339
R. D. C. Monteiro and M. Todd, Path-following methods for semidefinite programming, in Handbook of Semidefinite Programming, Kluwer, 2000 (source of Proposition 2.1).
S. Burer and R. D. C. Monteiro, Local minima and convergence in low-rank semidefinite programming, Mathematical Programming 103 (2005), 427–444. https://doi.org/10.1007/s10107-004-0564-1
N. Boumal, V. Voroninski and A. S. Bandeira, The non-convex Burer–Monteiro approach works on smooth semidefinite programs, NeurIPS 2016. https://arxiv.org/abs/1606.04970

10 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research+1·Captain: mikedeng1

Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems V: Bandit Convex Optimization with One-Point FeedbackTextbook

Motivation

In bandit convex optimization a forecaster repeatedly picks a point $x_t$ of a convex set $\mathcal K\subseteq\mathbb R^d$ , and an adversary picks a convex loss $\ell_t$ . The forecaster pays $\ell_t(x_t)$ and observes only that number: it never sees the function, its gradient, or its value elsewhere. This is the model of online optimization with only function-value access, as in tuning a system online from measured costs, dynamic pricing with an unknown convex demand-cost curve, or routing with path costs observed only on the route taken. The question is how fast the forecaster can approach the best fixed point in hindsight.

Chapter 6 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2, Foundations and Trends in Machine Learning 5(1), 2012) treats the problem through spherical gradient estimates fed to projected gradient descent. The one-point method is due to Flaxman, Kalai and McMahan (SODA 2005, arXiv:cs/0408007), who obtained an $\mathcal O(n^{3/4})$ regret bound. Agarwal, Dekel and Xiao (COLT 2010) showed that two function evaluations per round allow $\mathcal O(\sqrt n)$ . Whether one-point feedback admits $\sqrt n$ regret was open when the monograph was written (p. 94); Bubeck, Eldan and Lee (STOC 2017, arXiv:1607.03084) later obtained $\sqrt n$ regret up to logarithmic and polynomial-in- $d$ factors for convex losses, with a different and much more involved algorithm.

Setting

Let $\mathbb B=\{x\in\mathbb R^d:\|x\|\le1\}$ be the closed Euclidean unit ball and $\mathbb S=\{x:\|x\|=1\}$ the unit sphere, with unnormalized spherical measure $\sigma$ , so that $\sigma(\mathbb S)=d\,\mathrm{Vol}(\mathbb B)$ . Fix $\delta>0$ . For a loss $\ell$ , the smoothed loss is $\widetilde\ell(x)=\mathbb E\,\ell(x+\delta B)$ with $B$ uniform on $\mathbb B$ .

The set $\mathcal K$ is closed and convex with $r\mathbb B\subseteq\mathcal K\subseteq R\mathbb B$ . The losses $\ell_1,\ell_2,\dots:\mathbb R^d\to\mathbb R$ are $G$ -Lipschitz, differentiable and convex, and are fixed before the game (an oblivious adversary).

OSGD (Online Stochastic Gradient Descent) on a set $\mathcal K'$ with learning rate $\eta$ starts at $x_1=0$ and sets $x_{t+1}=\operatorname{argmin}_{y\in\mathcal K'}\|y-(x_t-\eta\widetilde g_t(x_t))\|$ , where $\widetilde g_t$ is a gradient estimate. With $S_1,S_2,\dots$ independent and uniform on $\mathbb S$ :

the two-point estimate (6.1) is $\widetilde g_t(x_t)=\frac d{2\delta}\big(\ell_t(X_t^+)-\ell_t(X_t^-)\big)S_t$ with $X_t^\pm=x_t\pm\delta S_t$ ; the played point is $X_t^+$ or $X_t^-$ by a fair coin;
the one-point estimate (6.3) is $\widetilde g_t(x_t)=\frac d\delta\,\ell_t(\widetilde X_t)S_t$ with played point $\widetilde X_t=x_t+\delta S_t$ .

OSGD runs on the shrunken set $\mathcal K'=(1-\delta/r)\mathcal K$ , so that the perturbed points stay in $\mathcal K$ . The pseudo-regret is

\overline R_n=\mathbb E\sum_{t=1}^n\ell_t(\widetilde X_t)-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t(x).

Formalization targets

Goal: Theorem 6.2, tuned

If in addition $|\ell_t|\le L$ on $\mathcal K$ , and $\delta=(2n)^{-1/4}\sqrt{RdL/((3+R/r)G)}$ , $\eta=(2n)^{-3/4}\sqrt{R^3/(dL(3+R/r)G)}$ , then one-point OSGD satisfies

\overline R_n\le 4n^{3/4}\sqrt{RdL\,(3+R/r)\,G}.

Milestones

Lemma 6.1: $\nabla\int_{\mathbb B}\ell(x+\delta b)\,db=\frac1\delta\int_{\mathbb S}\ell(x+\delta s)s\,d\sigma(s)$ .
Lemma 6.2: $\frac d\delta\mathbb E[\ell(x+\delta S)S]=\nabla\mathbb E\,\ell(x+\delta B)$ .
Eq. (6.2): $|\ell(x)-\widetilde\ell(x)|\le\delta G$ .
Lemma 6.3: the queried points' regret against $x$ is at most the smoothed regret of the iterates against $(1-\xi)x$ , plus $3\delta Gn+\xi GRn$ .
Theorem 6.1: two-point OSGD has $\overline R_n\le R^2/\eta+\eta(Gd)^2n+\delta(3+R/r)Gn$ , and $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ .
Theorem 6.2, first display: one-point OSGD has $\overline R_n\le R^2/\eta+\frac{(dL)^2}{\delta^2}\eta n+\delta(3+R/r)Gn$ for every $0<\delta\le r$ and $\eta>0$ .

Significance

The $n^{3/4}$ bound shows that a single function value per round suffices for sublinear regret against any oblivious sequence of Lipschitz convex losses, with a forecaster whose only operations are a random perturbation and a Euclidean projection. The smoothing identity of Lemmas 6.1–6.2 is the basic tool of zeroth-order (derivative-free) optimization, used well beyond bandits, and Theorem 6.1 is the $\sqrt n$ benchmark for two-point methods.

All results are proved in the source. To the best of current knowledge none is formalized: the related items of the Introduction to Online Convex Optimization series on Prove2Me (Hazan's Lemma 6.7 and Theorem 6.9) were formalized with missing hypotheses and are recorded as disproved. This mission produces machine-checked statements with every hypothesis explicit, and the formal infrastructure (sphere measure calculus, a projected stochastic gradient analysis) for later zeroth-order results.

Difficulty

Two steps resist a direct formal treatment. First, Lemma 6.1 is a divergence-theorem identity on the ball; Mathlib has the sphere measure and polar coordinates, but its divergence theorem covers boxes rather than balls, so differentiating the ball average in $x$ requires either such a theorem or a direct argument about translates of the ball. Second, the regret analysis takes expectations of quantities that depend on the whole past: the iterate $x_t$ is a function of $S_1,\dots,S_{t-1}$ , and unbiasedness $\mathbb E[\widetilde g_t\mid x_t]=\nabla\widetilde\ell_t(x_t)$ holds only conditionally, via independence of $S_t$ from the past. A pathwise gradient-descent inequality must be combined with this conditional expectation round by round, with measurability of the projected iterates established along the way. The naive approach of treating the estimate as the true gradient of $\ell_t$ fails: it is a gradient of $\widetilde\ell_t$ , and the gap is handled only by Eq. (6.2) and Lemma 6.3.

Formalization scope

Points are in EuclideanSpace ℝ (Fin d) with $d\ge1$ ; rounds are $t=1,2,\dots$ , sums run over Finset.Icc 1 n. $\sigma$ is Mathlib's Measure.toSphere of Lebesgue measure; the uniform laws are normalized restrictions. Randomness lives on an arbitrary probability space; the directions $S_t$ are measurable, mutually independent (iIndepFun) and uniform on $\mathbb S$ , and in Theorem 6.1 the pairs $(S_t,C_t)$ are independent with $C_t$ a fair sign independent of $S_t$ . A run of OSGD is a predicate (start at $0$ , each iterate a Euclidean projection onto $(1-\delta/r)\mathcal K$ ), which determines the run uniquely, so the forecaster uses only observed values and its own randomness. The losses are Lipschitz, differentiable and convex on all of $\mathbb R^d$ ; the bound $|\ell_t|\le L$ is on $\mathcal K$ , because a convex function bounded on $\mathbb R^d$ is constant. The minimum over $\mathcal K$ is an infimum over the subtype $\mathcal K$ , attained in every theorem.

Conventions and corrections, each stated in the item's Formalization Note:

Lemma 6.1 carries the factor $1/\delta$ that the printed statement omits and the proof contains (corrected misprint).
Theorem 6.1's second display prints $\eta=R/(GD\sqrt n)$ and a limit "for $\delta\to0$ "; the item states $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ and every admissible $\delta$ , which implies the limit (corrected misprint).
Theorems 6.1 and 6.2 add $0<\delta\le r$ , which the proofs need for $X_t^\pm,\widetilde X_t\in\mathcal K$ ; for the tuned $\delta$ of the goal it is a condition on $n$ .
The goal adds $G,L>0$ and $n\ge1$ , which its formulas for $\delta,\eta$ need; the constant $4$ is the book's rounding of $2\cdot2^{3/4}$ and is kept, as is the form $R^2/\eta$ .

The statements cannot be satisfied trivially: the run is pinned by its recursion, the losses are fixed before the randomness, the expectations are of bounded measurable functions (no zero-valued Bochner integrals), and the minimum is over the nonempty compact $\mathcal K$ . Section 6.3 (Lemma 6.4, Theorem 6.3) is not included, because its algorithm box and proof use different stage lengths and its unimodality condition is stated on a smaller set than the proof uses.

Needed infrastructure: calculus of ball averages and sphere integrals, symmetry of the uniform sphere law, nonexpansiveness of projections onto closed convex sets, and conditional-expectation bookkeeping for adapted iterates. Each is reusable for zeroth-order optimization; contributions of any of them as separate lemmas are welcome.

Selected references

S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
A. Flaxman, A. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. arXiv:cs/0408007
A. Agarwal, O. Dekel, L. Xiao, Optimal algorithms for online convex optimization with multi-point bandit feedback, COLT 2010. link
S. Bubeck, R. Eldan, Y. T. Lee, Kernel-based methods for bandit convex optimization, STOC 2017. arXiv:1607.03084

10 thms2 active usersReviewed

Optimization Probability·Captain: mikedeng1

The Entropic Barrier: A Simple and Optimal Universal Self-Concordant Barrier: The Entropic Barrier of a Convex Body in ℝⁿ Is a (1 + εₙ)n-Self-Concordant Barrier with εₙ ≤ 100√(log n / n)Research Paper

Motivation

Interior-point methods minimize a linear function $x\mapsto\langle c,x\rangle$ over a convex set $\mathcal K\subset\mathbb R^n$ by following the minimizers of $\langle c,x\rangle+\frac1t g(x)$ as $t\to\infty$ , where $g$ is a self-concordant barrier for $\mathcal K$ . Each Newton step of such a method shrinks $1/t$ by a factor $1-1/\sqrt\nu$ , where $\nu$ is the self-concordance parameter of $g$ , so $\nu$ controls the iteration count of every interior-point method built on $g$ (Nesterov and Nemirovski 1994; Nesterov 2004).

Timeline:

1994. Nesterov and Nemirovski construct the universal barrier for any convex body and show it is a $\nu$ -self-concordant barrier with $\nu\le Cn$ for a universal constant $C$ . They also show that $\nu\ge n$ is necessary for some bodies (the simplex, the cube).
2014–2015. Hildebrand (Math. Oper. Res. 2014) and Fox (Ann. Mat. Pura Appl. 2015) show that the canonical barrier of a convex cone has parameter equal to the dimension, which gives parameter $n+1$ for convex bodies.
2015. Bubeck and Eldan (arXiv:1412.1587, COLT 2015) show that the Fenchel dual of the log-Laplace transform of the uniform measure on $\mathcal K$ , which they call the entropic barrier, is a $(1+o(1))n$ -self-concordant barrier, with an explicit $o(1)$ term.

Beyond optimization, the entropic barrier is the mirror map that pairs naturally with the exponential-family sampling scheme in bandit linear optimization, which the paper discusses in its §3.1.

Setting

Let $\mathcal K\subset\mathbb R^n$ be a convex body: compact, convex, with non-empty interior $\operatorname{int}(\mathcal K)$ . The log-Laplace transform of $\mathcal K$ is

f(\theta)=\log\left(\int_{x\in\mathcal K}\exp(\langle\theta,x\rangle)\,dx\right),\qquad\theta\in\mathbb R^n,

and the entropic barrier is its Fenchel dual

f^*(x)=\sup_{\theta\in\mathbb R^n}\ \langle\theta,x\rangle-f(\theta),\qquad x\in\operatorname{int}(\mathcal K).

For a function $g:\operatorname{int}(\mathcal K)\to\mathbb R$ write $\nabla g(x)[h]$ , $\nabla^2g(x)[h,h]$ , $\nabla^3g(x)[h,h,h]$ for its directional derivatives. Following Definition 1 of the paper:

$g$ is a barrier for $\mathcal K$ if $g(x)\to+\infty$ as $x\to\partial\mathcal K$ ;
a $C^3$ convex $g$ is self-concordant if $\nabla^3g(x)[h,h,h]\le2(\nabla^2g(x)[h,h])^{3/2}$ for all $x\in\operatorname{int}(\mathcal K)$ , $h\in\mathbb R^n$ ;
it is $\nu$ -self-concordant if moreover $\nabla g(x)[h]\le\sqrt{\nu\cdot\nabla^2g(x)[h,h]}$ for all such $x,h$ .

The proof works with the canonical exponential family $p_\theta$ , the probability measure with density $\exp(\langle\theta,x\rangle-f(\theta))\mathbb 1\{x\in\mathcal K\}$ , its mean $x(\theta)$ , covariance $\Sigma(\theta)$ and third central moment $T(\theta)$ ; with $Y=\langle\theta/\|\theta\|,X\rangle$ for $X\sim p_\theta$ and its density $\rho$ ; and with the section marginal $\lambda(y)=\mathrm{Vol}_{n-1}(\mathcal K\cap\{y\theta/\|\theta\|+\theta^\perp\})/\mathrm{Vol}(\mathcal K)$ .

Formalization targets

Goal: Theorem 1

For every $n\ge80$ and every convex body $\mathcal K\subset\mathbb R^n$ , $f^*$ is a $\nu$ -self-concordant barrier for $\mathcal K$ with

\nu=(1+\varepsilon_n)\,n,\qquad\varepsilon_n=100\sqrt{\frac{\log n}{n}}.

Milestones, in attack order

Lemma 1 (p. 5): strict convexity of $f$ , $f^*$ ; $\nabla f^*:\operatorname{int}(\mathcal K)\to\mathbb R^n$ is a bijection; $\nabla^2f=\Sigma$ , $\nabla^3f=T$ (eqs. (4)–(5)); $\nabla^2f^*(x)=\Sigma(\theta(x))^{-1}$ (eq. (6)).
$f^*$ is a barrier (§4, p. 6).
Lemma 2 (p. 7): $\mathbb EX^3\le2(\mathbb EX^2)^{3/2}$ for a real centered log-concave $X$ ; its consequence $\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^3\le2(\mathbb E_{p_\theta}\langle X-x(\theta),h\rangle^2)^{3/2}$ ; $f^*$ is self-concordant (§4, pp. 6–7).
Reduction of (3) (p. 7): $f^*$ satisfies (3) with parameter $\nu$ iff $\langle\Sigma(\theta)\theta,\theta\rangle\le\nu$ for all $\theta$ .
$\lambda$ is $n$ -concave on its support (p. 9) and Lemma 5 (p. 9): $\varphi$ is $n$ -concave iff $(\log\varphi)''\le-\frac1n((\log\varphi)')^2$ .
Lemma 3 (p. 8): $\rho(y+y_0)=\rho(y_0)\zeta(y)e^{-y^2/(2\sigma^2)}$ on $[-M,M]$ , with $\zeta\in[0,1]$ unimodal, $M=\sqrt{7n\log n}/\|\theta\|$ , $\sigma^2=\frac{n}{\|\theta\|^2}\frac{1}{1-\sqrt{7\log(n)/n}}$ ; and its consequence (9): $\mathbb E(|Y-y_0|^2\mid|Y-y_0|\le M)\le\sigma^2$ .
Lemma 4 (p. 8): $(1-2c(\varepsilon)\varepsilon\log^2(1/\varepsilon))\mathrm{Var}(X)\le\int_{x_1}^{x_2}(x-x_0)^2\lambda(x)dx\le\mathbb E(|X-x_0|^2\mid X\in[x_1,x_2])$ for log-concave $X$ .
(7) (p. 7): $\mathrm{Var}(Y)\le\frac{n}{\|\theta\|^2}(1+\varepsilon_n)$ .

Significance

The result. Theorem 1 gives, for every convex body, an explicit barrier whose parameter is $n$ up to a second-order term, against the $Cn$ of the universal barrier, and it is optimal up to that term because $\nu\ge n$ is necessary for some bodies. The barrier is defined by a single formula, its derivatives are moments of an explicit probability measure, and its parameter bound reduces to a variance bound for one-dimensional log-concave marginals. Lemmas 2 and 4 are self-contained facts about log-concave laws on $\mathbb R$ (a sharp third-moment bound and a variance-localization bound) that are usable outside this paper.

Formalizing it. The theorem is proved in the paper; nothing here is formalized elsewhere. The platform has a definition of self-concordance (reused here) and results for given self-concordant functions, but no universal or entropic barrier, no exponential family over a convex body, and no moment bounds for log-concave laws. A complete development produces machine-checked versions of the duality facts of Lemma 1, of the two log-concave lemmas, and of the Brunn–Minkowski consequence for section volumes. Two steps of the paper are sketched rather than proved in full: the end of the proof of Lemma 2 ("We omit further details of this proof", p. 12) and, in Lemma 4, a normalization step that cites a lemma stated for isotropic densities. A formal proof either fills or replaces them.

Difficulty

Self-concordance of $f^*$ reduces to self-concordance of $f$ by a general duality fact, and that reduces to Lemma 2; the difficulty there is the sharp constant $2$ , since generic moment comparisons for log-concave laws give a worse constant. The parameter bound is the hard part. The obvious bound $\langle\Sigma(\theta)\theta,\theta\rangle\le Cn$ follows from standard concentration for log-concave measures, but any argument that loses a constant factor proves only the 1994 result. The $1+o(1)$ requires the one-dimensional marginal of the tilted measure to be compared with a Gaussian of variance $n/\|\theta\|^2$ to within a factor $1+O(\sqrt{\log n/n})$ , using the fact that $\lambda$ is $n$ -concave and not merely log-concave. The paper does this pointwise near the mode (Lemma 3) and controls the tails separately (Lemma 4). The pointwise argument assumes $\rho$ smooth, which holds for smooth bodies, and an approximation argument passes to general convex bodies.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), so $n$ is the dimension, not a separate parameter. A convex body is compact, convex, with non-empty interior; a lower-dimensional set is excluded, which rules out a formalization in which the barrier and self-concordance clauses hold vacuously.
$f^*$ is a real supremum. On $\operatorname{int}(\mathcal K)$ it is the true supremum; elsewhere Lean returns a junk value that no statement reads. The barrier property is a limit within $\operatorname{int}(\mathcal K)$ at every frontier point.
Self-concordance (2) is the published ConvexOptimization.IsSelfConcordantOn on interior K, stated by line restrictions with an absolute value. It is equivalent to (2), because $h\mapsto-h$ flips the sign of the third derivative.
The goal states the parameter as the explicit number $\nu=(1+100\sqrt{\log(n)/n})\,n$ . The page says $\varepsilon_n\le100\sqrt{\log(n)/n}$ , and (3) is monotone in $\nu$ , so this is the same claim. An existential $\nu$ is not used.
Corrections and implicit hypotheses:
- Lemma 4 is stated for $0<\varepsilon<1$ . The page says $\varepsilon>0$ , but the statement is false for $\varepsilon\ge1$ and the paper applies it only with $\varepsilon<1$ .
- Lemma 5 assumes $\varphi>0$ , which is implicit in $\zeta=\log\varphi$ .
- The reduction of (3) assumes $\nu\ge0$ .
- Lemma 3 and (9) carry the smoothness of $\rho$ (the paper's own without-loss-of-generality step on p. 7) as a hypothesis, and the theorem's range $n\ge80$ .
Section volumes use Mathlib's unnormalized $(n-1)$ -dimensional Hausdorff measure. The normalization constant cancels in $\rho$ and does not affect $n$ -concavity. $\lambda$ and $\rho$ are fixed pointwise functions, because Lemma 3 evaluates $\rho$ at a maximizer.
Log-concavity on $\mathbb R$ is the published ConvexOptimization.LogConcaveOn on the whole line.
Needed infrastructure that is reusable beyond this mission:
- differentiation under the integral sign for exponential families on compact sets;
- Fenchel duality for smooth strictly convex functions;
- Brunn's concavity theorem for sections of convex bodies;
- moment and tail bounds for log-concave densities on $\mathbb R$ .
Contributions to any of these, or proofs of single milestones, are welcome.

Selected references

S. Bubeck, R. Eldan, The entropic barrier: a simple and optimal universal self-concordant barrier, COLT 2015; arXiv:1412.1587v3. https://arxiv.org/abs/1412.1587
Y. Nesterov, A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
R. Hildebrand, Canonical barriers on convex cones, Mathematics of Operations Research 39:841–850, 2014.
D. Fox, A Schwarz lemma for Kähler affine metrics and the canonical potential of a proper convex cone, Annali di Matematica Pura ed Applicata 194:1–42, 2015.
B. Klartag, On convex perturbations with a bounded isotropic constant, Geometric and Functional Analysis 16(6):1274–1290, 2006.
C. Borell, Convex set functions in d-space, Periodica Mathematica Hungarica 6(2):111–136, 1975.

21 thms2 active usersReviewed

Convex Optimization

Missions

Vector Space Methods VIII: Fenchel DualityTextbook

Motivation

Setting

Formalization targets

Main goal: Fenchel duality

Milestones

Significance

Difficulty

Formalization scope

Selected references

Convex Optimization IV: Löwner–John EllipsoidsTextbook

Data-Driven Robust Optimization VI: The Moment Set U^CS Has Support Function μ̂ᵀv + Γ₁‖v‖ + √(1/ε − 1)‖Cv‖, an Upper Bound on the Worst-Case Value at RiskResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Data-Driven Robust Optimization V: The Order-Statistic Box U^M Built from Marginal Samples Dominates Value at Risk with Probability at Least 1 − αResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 7

Milestones

Significance

Difficulty

Formalization scope

Selected references

Data-Driven Robust Optimization IV: The Forward–Backward Deviation Set U^FB Has a Closed-Form Support Function That Bounds the Worst-Case Value at RiskResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

Data-Driven Robust Optimization III: For Independent Marginals, the Kolmogorov–Smirnov Set U^I Has Support Function (19) and Bounds the Worst-Case Value at RiskResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5 (deterministic content)

Milestones, in attack order

Significance

Difficulty

Formalization scope

Selected references

Data-Driven Robust Optimization II: With Known Finite Support, the χ² and G Uncertainty Sets Bound the Worst-Case Value at Risk over Their Confidence RegionsResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Optimization with Stochastic Dominance Constraints: Lagrange Multipliers of a Second-Order Dominance Constraint Are Concave Nondecreasing Utility FunctionsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.2

Milestones

Further: Theorem 5.1

Significance

Difficulty

Formalization scope

Selected references

Robust Solutions of Uncertain Linear Programs I: Under Constraint-wise Uncertainty and the Boundedness Assumption the Robust Counterpart Is No Worse Than the Worst InstanceResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2.1 (p. 5)

Milestones

Companions

Significance

Difficulty