Convex Optimization

Completed

Machine Learning Statistics·Captain: mikedeng1

Stability and Generalization 3: Tikhonov Regularization in a Reproducing Kernel Hilbert Space Has Uniform Stability σ²κ²/(2λm)Research Paper

Motivation

Learning from a finite sample is useful only if changing the sample has a controlled effect on the learned predictor. Uniform stability asks for a bound on the change in loss at every test point when one training example is removed. Bousquet and Elisseeff use this property to obtain generalization bounds for learning algorithms, and identify regularization as a source of stability in methods built from reproducing kernels. The present mission isolates their result for a squared norm penalty in a reproducing kernel Hilbert space (RKHS). It concerns the sensitivity of the optimizer itself, before any probability bound on a random training sample is applied. The result is Theorem 22 of Bousquet and Elisseeff (2002).

Setting

Let $X$ be an input space, $Y$ a label space, and $H$ a real reproducing kernel Hilbert space of real-valued predictors on $X$ . A kernel $K:X\times X\to\mathbb R$ and a feature representative $\Phi(x)\in H$ express the reproducing identity $f(x)=\langle f,\Phi(x)\rangle_H$ and $K(x,x')=\langle\Phi(x),\Phi(x')\rangle_H$ . Thus $K(x,x)=\|\Phi(x)\|_H^2$ . The source assumes that all diagonal kernel values satisfy $K(x,x)\le\kappa^2$ .

A labeled example is $z=(x,y)\in X\times Y$ . Its loss under $f$ is $\ell(f,z)=c(f(x),y)$ , where $c$ is a real-valued cost. Let $D_H$ be the set of predictions that some element of $H$ can produce at some input. The loss is $\sigma$ -admissible when $c(\cdot,y)$ is convex for every label $y$ and $|c(a,y)-c(b,y)|\le\sigma|a-b|$ for all $a,b\in D_H$ and $y\in Y$ . Here $\sigma$ is a nonnegative Lipschitz constant. The definition compares any two attainable predictions, even when they arise at different inputs.

Fix a sample $S=(z_1,\ldots,z_m)$ , a deleted index $i$ , and a regularization weight $\lambda>0$ . The paper's full and truncated objectives, with squared RKHS norm regularization, are

R_r(g)=\frac1m\sum_{j=1}^{m}\ell(g,z_j)+\lambda\|g\|_H^2, \qquad R_r^{\setminus i}(g)=\frac1m\sum_{j\ne i}\ell(g,z_j)+\lambda\|g\|_H^2.

The factor in both objectives is $1/m$ . Let $f$ and $f^{\setminus i}$ be minimizers of these respective objectives over all of $H$ . The statements allow any minimizer satisfying the relevant global optimality condition; they do not choose one by an arbitrary fallback rule.

Formalization targets

The central target is the explicit deletion stability estimate of Theorem 22. For every test point $z\in X\times Y$ ,

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

Its four milestones follow the paper's route through Lemma 20, the point-evaluation inequality (25), and the two quantitative inequalities displayed in the proof of Theorem 22. In particular, the intermediate RKHS distance bound is $\|f^{\setminus i}-f\|_H\le\kappa\sigma/(2\lambda m)$ when $\kappa\ge0$ . The main theorem uses $\kappa^2$ , so it does not need a choice of sign for $\kappa$ . These numerical constants are part of the target, rather than placeholders for unspecified bounds.

Significance

The theorem supplies a deterministic, uniform sensitivity estimate for kernel methods trained by squared norm regularization. The bound applies simultaneously to every test example and decreases as either the sample size or the regularization weight increases. It is one of the ingredients that lets the paper apply its earlier stability-to-generalization results to concrete learning procedures. The loss need not be bounded for this theorem; bounding it is a separate question addressed later in the paper.

The result is proved in the source article. This mission asks for a machine-checked version of its exact pairwise claim and the reusable infrastructure around it: the paper's admissibility condition, the two objectives, the general regularizer inequality, and the RKHS evaluation bound. The existing Prove2Me library already has definitions for loss, empirical error, and the RKHS reproducing identity, so the new definitions concentrate on what is specific to these pages. The related replace-one estimate in Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning uses a different perturbation and constant; it is not interchangeable with this result.

Difficulty

The two minimizers solve different objectives, and the deleted example appears in only one of them. A comparison of their objective values alone does not directly give a bound on their distance in the Hilbert norm. The source also distinguishes an abstract convex class of functions in Lemma 20 from the full RKHS used in Theorem 22. A proof must keep those domains straight while preserving the precise normalization of the truncated objective. Another delicate point is that the kernel bound controls evaluations through the reproducing identity; a bound on $K(x,x)$ is not by itself a bound on loss unless the admissibility condition is also used.

Formalization scope

The Lean model uses an abstract complete real inner product space $H$ , an evaluation map $\operatorname{ev}:H\to(X\to\mathbb R)$ , a feature map $\Phi:X\to H$ , and the published IsRKHSOf predicate tying these to $K$ . The completeness instance matches the source's Hilbert-space assumption. Samples have type Fin m → X × Y, so an index i : Fin m already forces $m\ge1$ . Minimization ranges over the entire $H$ for Theorem 22 and over the declared convex class for Lemma 20. The objective definitions use the published Loss and EmpiricalError objects. No probability measure or measurability assumption is needed for these deterministic assertions.

There is a printed mismatch that affects what “deletion” means. Theorem 22 names an algorithm defined by equation (26), which, run afresh on $m-1$ points, would normalize its data term by $1/(m-1)$ . Lemma 20 and the proof of Theorem 22 instead compare the full objective with equation (20), whose data term uses $1/m$ . The formalized goal states that comparison, with its explicit constant, and records the discrepancy for audit. This excludes the tempting shortcut of treating the two normalizations as identical. The regularizer is the genuine squared norm and the second minimizer is required to minimize the genuine truncated objective; neither a restricted hypothesis ball nor an artificially assumed distance bound enters the goal. Contributions that establish minimizer existence or connect the pairwise bound to an algorithmic selection would extend this core without changing its statement.

Selected references

Olivier Bousquet and André Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002), 499–526. Article and PDF.
Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar, Foundations of Machine Learning, second edition, MIT Press, 2018, Chapter 14. Book information.

9 thms2 active usersReviewed

Numerical Analysis Optimization·Captain: mikedeng1

The Rate of Convergence of Nesterov's Accelerated Forward-Backward Method is Actually Faster than 1/k^2 I: For α > 3, (Ψ + Φ)(x_k) − min(Ψ + Φ) = o(k⁻²) and ‖x_{k+1} − x_k‖ = o(k⁻¹)Research Paper

Motivation

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

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

where $\Phi$ is smooth and convex (a data-fit term) and $\Psi$ is convex but possibly nonsmooth or infinite-valued (an $\ell^1$ penalty, the indicator function of a constraint set). The forward-backward method alternates a gradient step on $\Phi$ with a proximal step on $\Psi$ and reduces the objective gap at rate $O(k^{-1})$ after $k$ iterations. Combining it with Nesterov's extrapolation scheme gives the accelerated forward-backward method, best known as FISTA, which improves the guaranteed rate to $O(k^{-2})$ . FISTA and its variants are standard solvers for sparse recovery and image reconstruction.

Timeline:

1983. Nesterov introduces the extrapolation scheme for smooth convex minimization, with an $O(k^{-2})$ rate for function values (Nesterov 1983).
2009. Beck and Teboulle extend it to the composite problem above (FISTA), with the $O(k^{-2})$ rate (doi:10.1137/080716542).
2014. Su, Boyd and Candès read the scheme as a discretization of the ODE $\ddot x+\frac{\alpha}{t}\dot x+\nabla\Theta(x)=0$ (arXiv:1503.01243).
2014–2015. Chambolle and Dossal (doi:10.1007/s10957-015-0746-4) and, independently, Attouch, Chbani, Peypouquet and Redont (arXiv:1507.04782) prove weak convergence of the iterates for the variant with parameter $\alpha>3$ . Before that, convergence of the iterates had been open for about two decades.
2015. May shows that for $\alpha>3$ the continuous-time gap is $o(t^{-2})$ (arXiv:1509.05598).
2016. Attouch and Peypouquet prove the discrete analogue: for $\alpha>3$ the function gap of the algorithm is $o(k^{-2})$ and the velocity is $o(k^{-1})$ (arXiv:1510.08740, SIAM J. Optim. 26(3):1824–1834).

Setting

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

$\Psi:\mathcal H\to\mathbb R\cup\{+\infty\}$ be proper (finite somewhere), lower semicontinuous and convex;
$\Phi:\mathcal H\to\mathbb R$ be convex and continuously differentiable, with gradient $\nabla\Phi$ Lipschitz continuous with constant $L$ ;
$\Theta=\Psi+\Phi$ , and assume the set of minimizers $S=\operatorname{argmin}\Theta$ is nonempty.

For $s>0$ , the proximal map $\operatorname{prox}_{s\Psi}(z)$ is the unique minimizer of $u\mapsto\Psi(u)+\frac1{2s}\|u-z\|^2$ . Given $\alpha>0$ , a step size $0<s<1/L$ and starting points $x_0,x_1$ , algorithm (2) generates

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),\qquad k\ge1.

The common choice is $\alpha=3$ ; this mission concerns $\alpha>3$ .

The proofs use the operator $G_s(y)=\frac1s\big(y-\operatorname{prox}_{s\Psi}(y-s\nabla\Phi(y))\big)$ , the sequence $z_k=x_k+\frac{k-1}{\alpha-1}(x_k-x_{k-1})$ , a minimizer $x^*$ , and the quantity

\mathcal E(k)=\frac{2s}{\alpha-1}(k+\alpha-2)^2\big(\Theta(x_k)-\Theta(x^*)\big)+(\alpha-1)\|z_k-x^*\|^2 .

Write $\theta_k=\Theta(x_k)-\Theta(x^*)$ and $d_k=\frac1{2s}\|x_{k+1}-x_k\|^2$ .

Formalization targets

Goal: Theorem 1 (p. 2)

For $\alpha>3$ and $0<s<1/L$ ,

\lim_{k\to\infty}k^2\big(\Theta(x_k)-\min\Theta\big)=0\qquad\text{and}\qquad\lim_{k\to\infty}k\,\|x_{k+1}-x_k\|=0.

The statement fixes no constants, so it is unaffected by later improvements of the explicit bounds below.

Milestones (in attack order)

(9), p. 2. If $sL\le1$ , then for all $x,y$ : $\Theta(y-sG_s(y))\le\Theta(x)+\langle G_s(y),y-x\rangle-\frac s2\|G_s(y)\|^2$ .
(13), p. 3. For $\alpha\ge3$ and $k\ge1$ : $\mathcal E(k+1)+2s\frac{\alpha-3}{\alpha-1}k\,\theta_k\le\mathcal E(k)$ .
Fact 1, p. 3. $(\mathcal E(k))$ is nonincreasing and has a finite limit.
Fact 2, p. 3. $\theta_k\le\frac{(\alpha-1)\mathcal E(1)}{2s(k+\alpha-2)^2}$ and $\|z_k-x^*\|^2\le\frac{\mathcal E(1)}{\alpha-1}$ for $k\ge1$ .
Fact 3, p. 3. For $\alpha>3$ : $\sum_{k\ge1}k\,\theta_k\le\frac{(\alpha-1)\mathcal E(1)}{2s(\alpha-3)}$ .
(14), p. 4. $\Theta(x_{k+1})+d_k\le\Theta(x_k)+\frac{(k-1)^2}{(k+\alpha-1)^2}d_{k-1}$ for $k\ge1$ .
Fact 4, p. 4. For $\alpha>3$ : $\sum_{k\ge1}k\,d_k\le\frac{\alpha(3\alpha-5)\mathcal E(1)}{4s(\alpha-1)(\alpha-3)}$ .
Lemma 2, p. 4. For $\alpha>3$ , $\lim_k\big[k^2d_k+(k+1)^2\theta_{k+1}\big]$ exists and is finite.

Significance

The result. The $O(k^{-2})$ rate of FISTA is often quoted as optimal for first-order methods. Theorem 1 shows that for $\alpha>3$ the worst-case rate along every single run is strictly better, $o(k^{-2})$ , and that the steps $\|x_{k+1}-x_k\|$ decay faster than $1/k$ . No better power is possible: by Attouch et al., Example 2.13 there is no $p>2$ with an $O(k^{-p})$ rate for every $\Phi$ and $\Psi$ . The intermediate estimates (Facts 2–4) give explicit, quantitative bounds that are reused in the analysis of inexact and perturbed variants (Theorem 4 of the paper) and in mission II of this series, which proves weak convergence of the iterates.

Formalizing it. The result is proved on paper. As far as we know, no machine-checked proof of the $O(k^{-2})$ rate of FISTA in this Hilbert-space, extended-valued setting exists in Mathlib or on this platform, and neither does the $o(k^{-2})$ refinement. A complete development would provide reusable statements about proximal-gradient steps for functions valued in $\mathbb R\cup\{+\infty\}$ . The page also has a factor slip in Fact 4 and Lemma 2 (see Formalization scope); checking it mechanically is one of the outputs.

Difficulty

The $O(k^{-2})$ bound follows from the monotonicity of $\mathcal E$ alone. That argument cannot give $o(k^{-2})$ : it controls $k^2\theta_k$ only by the constant $\mathcal E(1)$ , and summability of $k\theta_k$ (Fact 3) gives a decay of $k^2\theta_k$ only along a subsequence, not of the whole sequence. The missing ingredient is convergence of a weighted combination of function gaps and velocities, which is Lemma 2. The bookkeeping is delicate: every step carries explicit coefficients in $k$ and $\alpha$ , and the inequalities must hold in the extended reals because $\Psi$ may be $+\infty$ at the starting point.

Formalization scope

Space and functions. $\mathcal H$ is a real inner product space that is complete. $\Psi$ takes values in EReal and satisfies the published predicate IsProperClosedConvex (never $-\infty$ , finite somewhere, lower semicontinuous, convex epigraph). $\Phi:\mathcal H\to\mathbb R$ is ConvexOn and ContDiff ℝ 1, and gradient Φ is LipschitzWith L for some L : ℝ≥0.
Step size. $0<s<1/L$ is written 0 < s and s * L < 1, so that $L=0$ is allowed (s < 1 / L would be unsatisfiable when $L=0$ ). Display (9) uses the page's $s\le1/L$ , written s * L ≤ 1.
Proximal map. It is a map P with the published predicate IsProx s Ψ P, which determines $P=\operatorname{prox}_{s\Psi}$ for proper closed convex $\Psi$ and $s>0$ .
The run. It is required to follow (2) for every $k\ge1$ , with $x_0,x_1$ arbitrary; the coefficient of $x_0$ vanishes at $k=1$ .
Extended reals. $\Theta$ , $\mathcal E$ and the function-value statements live in EReal. No value is ever converted to $\mathbb R$ with toReal, which would turn $+\infty$ into $0$ . "The limit exists" (Fact 1, Lemma 2) means convergence to a real number, because in EReal every monotone sequence converges. Infinite series of nonnegative terms are stated as bounds on every partial sum. $\min\Theta$ in the goal is ⨅ y, Θ y together with the hypothesis that a minimizer exists.
Corrected slips. Fact 2 is stated with $\mathcal E(1)$ for $k\ge1$ ; the page writes $\mathcal E(0)$ for $k\ge0$ , which needs an iterate $x_{-1}$ . Fact 4 is stated for $\sum k\,d_k$ ; the page prints $\sum k\|x_{k+1}-x_k\|^2$ with the same constant, which is off by the factor $2s$ and false in general. Lemma 2 is stated for the bracket $k^2d_k+(k+1)^2\theta_{k+1}$ of its proof (16).
Ruled out. The goal assumes nothing about $\mathcal E$ , $z_k$ , $\theta_k$ or $d_k$ . A statement of the first limit for toReal values, or with an extended-real "limit exists", would be trivially weaker and is not what is asked.
Welcome contributions. Proofs of any milestone; general facts about proximal maps of EReal-valued convex functions and about the descent property of $L$ -smooth convex functions, which are reusable well beyond this mission.

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. arXiv:1510.08740v4, doi:10.1137/15M1046095
H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168:123–175, 2018. arXiv:1507.04782
A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2(1):183–202, 2009. doi:10.1137/080716542
A. Chambolle, C. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", J. Optim. Theory Appl. 166:968–982, 2015. doi:10.1007/s10957-015-0746-4
R. May, Asymptotic for a second order evolution equation with convex potential and vanishing damping term, 2015. arXiv:1509.05598
Y. Nesterov, A method of solving a convex programming problem with convergence rate $O(1/k^2)$ , Soviet Math. Dokl. 27:372–376, 1983. mathnet
W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17(153):1–43, 2016. arXiv:1503.01243

11 thms2 active usersReviewed

Completed

Discrete Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Understanding and Using Linear Programming XI: The KKT Conditions and the Unique Smallest Enclosing BallTextbook

Motivation

The smallest enclosing ball problem asks, for finitely many points $p_1,\dots,p_n\in\mathbb{R}^d$ , for a ball of the smallest radius that contains all of them. It appears in clustering, in collision detection and bounding-volume hierarchies, in facility location (placing one service point so that the farthest client is as close as possible), and in the analysis of geometric algorithms. Sylvester posed the planar version in 1857; Megiddo (1983) gave a linear-time algorithm in fixed dimension, and Welzl (1991) a simple randomized one.

This mission formalizes Section 8.7 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer, 2007), which uses the problem to introduce convex programming. Unlike the geometric problems of the book's Chapter 2, the smallest ball cannot be written as a linear program. The section shows instead that it is a convex quadratic program, derives the Karush–Kuhn–Tucker (KKT) conditions for convex programs in equational form from the duality theorem of linear programming, and uses them to prove that the smallest enclosing ball exists and is unique. It is the book's bridge from linear to convex optimization.

Setting

A function $f:\mathbb{R}^n\to\mathbb{R}$ is convex if $f((1-t)x+ty)\le(1-t)f(x)+tf(y)$ for all $x,y\in\mathbb{R}^n$ and $t\in[0,1]$ . A convex program in equational form is

\text{minimize } f(x)\quad\text{subject to } Ax=b,\ x\ge 0,

with $A$ a real $m\times n$ matrix with columns $a_1,\dots,a_n$ , $b\in\mathbb{R}^m$ and $f$ convex. A vector $x$ is feasible if $Ax=b$ and $x\ge 0$ componentwise, and optimal if it is feasible and $f(x)\le f(x')$ for every feasible $x'$ . For differentiable $f$ , $\nabla f(x)$ is the row vector of partial derivatives, so $\nabla f(x^*)(x-x^*)$ is a scalar.

For points $p_1,\dots,p_n\in\mathbb{R}^d$ , write $P=\{p_1,\dots,p_n\}$ and let $Q$ be the $d\times n$ matrix whose $j$ th column is $p_j$ . The program studied is

\text{(8.15)}\qquad \text{minimize } f(x)=x^TQ^TQx-\sum_{j=1}^n x_j\,p_j^Tp_j\quad\text{subject to } \sum_{j=1}^n x_j=1,\ x\ge 0 .

A ball is a closed Euclidean ball $B(c,r)=\{z\in\mathbb{R}^d:\|z-c\|\le r\}$ . The ball $B(c,r)$ is the unique smallest enclosing ball of a set $S$ if $r\ge 0$ , $S\subseteq B(c,r)$ , every ball containing $S$ has radius at least $r$ , and every ball containing $S$ of radius at most $r$ has center $c$ .

Formalization targets

Goal: Theorem 8.7.4

For $n\ge 1$ points $p_1,\dots,p_n\in\mathbb{R}^d$ , the objective $f$ of (8.15) is convex, and

(8.15) has an optimal solution $x^*$ ;
there is a point $p^*$ with $p^*=Qx^*$ for every optimal $x^*$ , and for every optimal $x^*$

-f(x^*)\ge 0\quad\text{and}\quad B\big(p^*,\sqrt{-f(x^*)}\big)\ \text{is the unique smallest enclosing ball of } P .

Milestones

Fact 8.7.1. For $C\subseteq\mathbb{R}^n$ convex, $f$ differentiable and convex, and $x^*\in C$ : $x^*$ minimizes $f$ over $C$ iff $\nabla f(x^*)(x-x^*)\ge 0$ for all $x\in C$ .
Proposition 8.7.2 (KKT conditions). For $f$ convex with continuous partial derivatives and $x^*$ feasible: $x^*$ is optimal iff there is $\tilde y\in\mathbb{R}^m$ with

\nabla f(x^*)_j+\tilde y^Ta_j\ \begin{cases}=0&\text{if } x^*_j>0,\\ \ge 0&\text{otherwise,}\end{cases}\qquad j=1,\dots,n.

Lemma 8.7.3. If $s_1,\dots,s_k$ lie on the boundary of the ball $B$ with center $s^*$ , then $B$ is the unique smallest enclosing ball of $\{s_1,\dots,s_k\}$ iff for every $u\in\mathbb{R}^d$ some $j$ has $u^T(s_j-s^*)\le 0$ .

Significance

The result. Theorem 8.7.4 gives existence and uniqueness of the smallest enclosing ball together with an explicit certificate: the center is a convex combination $Qx^*$ of the input points, the squared radius is the negated optimum value, and the points $p_j$ with $x^*_j>0$ lie on the boundary. It reduces the geometric problem to a convex quadratic program, for which interior-point and simplex-type solvers exist, and it is the basis of the combinatorial characterization "the center lies in the convex hull of the boundary points" used by Welzl-type algorithms. Proposition 8.7.2 is the KKT theorem for equational-form convex programs; it holds without any constraint qualification because the constraints are linear.

Formalizing it. All results here are classical and proved in the book; none is open. The mission produces machine-checked statements and, when solved, proofs of: the first-order optimality criterion for convex functions on convex sets in $\mathbb{R}^n$ ; the equational-form KKT theorem derived from LP duality; the boundary characterization of unique smallest enclosing balls; and existence and uniqueness of the smallest enclosing ball in every dimension. Mathlib has first-order necessary conditions at local minima and general convexity theory, but no KKT theorem for linearly constrained convex programs in this form and no smallest-enclosing-ball theory.

Difficulty

Existence of an optimum and convexity of $f$ are routine. For the KKT conditions, the necessary direction needs multipliers, which do not come from calculus alone: the obvious Lagrange-multiplier argument handles only equality constraints and says nothing about the sign pattern forced by $x\ge 0$ . For the goal, a solver must connect three layers — the gradient of a quadratic form in matrix notation, the multiplier conditions, and the Euclidean geometry of distances to $p^*$ — and uniqueness of the ball does not follow from uniqueness of the optimizer $x^*$ , which in general is not unique (repeated or cospherical points). The statement quantifies over all optimal $x^*$ and asserts that they all yield the same center.

Formalization scope

Vectors of $\mathbb{R}^n$ are Fin n → ℝ, so the book's indices $1,\dots,n$ become $0,\dots,n-1$ . Points of $\mathbb{R}^d$ are EuclideanSpace ℝ (Fin d), so $\|\cdot\|$ and $p^Tq$ are Euclidean. The matrix $Q$ is Matrix (Fin d) (Fin n) ℝ.
Optimality is stated against every feasible point; no infimum or supremum is taken. $\nabla f(x^*)(x-x^*)$ is the Fréchet derivative applied to $x-x^*$ , and $\nabla f(x^*)_j$ its value on the $j$ th unit vector. "Continuous partial derivatives" is ContDiff ℝ 1 f. Convexity is ConvexOn ℝ Set.univ f.
Balls are closed. The squared radius $-f(x^*)$ is expressed by asserting $-f(x^*)\ge 0$ and taking the radius $\sqrt{-f(x^*)}$ . "Unique ball of smallest radius" is written out as minimality of the radius among all enclosing closed balls plus equality of centers for every enclosing ball of radius at most the optimum; merely stating that the ball encloses $P$ would not be the theorem.
The goal assumes $n\ge 1$ (for $n=0$ the feasible set is empty). In Fact 8.7.1 the minimizer $x^*$ is assumed to lie in $C$ , as "minimizes $f$ over $C$ " presupposes. In Lemma 8.7.3 the radius is nonnegative and each $s_j$ is at distance exactly $r$ from $s^*$ .
Needed infrastructure: gradients of quadratic forms on Fin n → ℝ, LP duality for the pair (maximize $c^Tx$ , $Ax=b$ , $x\ge0$ ) / (minimize $b^Ty$ , $A^Ty\ge c$ ), compactness of the standard simplex, and elementary Euclidean geometry. The first-order criterion and the KKT theorem are reusable beyond this mission; proofs through any route are welcome.

Selected references

J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.7, pp. 184–191. https://doi.org/10.1007/978-3-540-30717-4
S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
N. Megiddo, Linear-time algorithms for linear programming in $\mathbb{R}^3$ and related problems, SIAM J. Comput. 12(4), 1983. https://doi.org/10.1137/0212052
E. Welzl, Smallest enclosing disks (balls and ellipsoids), in New Results and New Trends in Computer Science, LNCS 555, Springer, 1991. https://doi.org/10.1007/BFb0038202
J. J. Sylvester, A question in the geometry of situation, Quarterly Journal of Pure and Applied Mathematics 1, 1857.

6 thms2 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization IV: Nonstationary Optimization and a Convergence Criterion for Nonmonotone SequencesTextbook

Motivation

Many stochastic and nondifferentiable optimization problems are not solved by minimizing their true objective $f^0$ directly: $f^0$ may be nonsmooth, an expectation that cannot be evaluated, or only approximately known. A standard remedy replaces $f^0$ by a sequence of "good" approximations $F^0(\cdot, s)$ (smoothed versions, sample averages, perturbations) that converge to $f^0$ , and runs one step of a descent method on the current approximation at every iteration. Approximation and optimization then proceed simultaneously. More generally, in nonstationary optimization the objective $F^0(\cdot, s)$ and the feasible set $X_s$ change with the iteration number $s$ , and the iterates $x^s$ are required to follow the time path of the optimal solutions,

\lim_{s\to\infty}\bigl[F^0(x^s, s) - \min\{F^0(x, s) \mid x \in X_s\}\bigr] = 0 .

Such procedures are essentially nonmonotone: a step on $F^0(\cdot, s)$ gives no guarantee of decrease of $F^0(\cdot, t)$ for $t \ge s+1$ , nor of $f^0$ . Their convergence therefore cannot be proved by the usual monotone Lyapunov argument. Section 6.4 of Yu. Ermoliev's chapter "Stochastic Quasigradient Methods" in Ermoliev & Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), gives the basic deterministic convergence theorem for this setting (Theorem 6.3) and the convergence criterion for nonmonotone sequences on which its proof rests (Theorem 6.4, taken from Ermoliev's 1976 monograph; the chapter compares its conditions with Zangwill's necessary and sufficient convergence conditions).

Timeline, as recorded in the chapter's bibliography (pp. 180–181): Ermoliev and Nurminski introduced limit extremal problems, in which $F^0(\cdot, s)$ and $X_s$ both converge ("Limit extremal problems", Kibernetika 1973, [14]); Nurminski gave convergence conditions for stochastic programming algorithms (Kibernetika 1973, [11]); Gupal treated time-varying functions (Kibernetika 1974, [15]); Ermoliev's monograph Stochastic Programming Methods (Nauka, 1976, [5]) contains the criterion stated here as Theorem 6.4 (p. 181); Nurminski formulated the general problem of nonstationary optimization (Kibernetika 1977, [16]); and Gaivoronski proved convergence of stochastic nonstationary procedures (Kibernetika 1978, [19]), the source of the chapter's Theorem 6.5.

Setting

Throughout, points are vectors of $\mathbb R^n$ with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$ .

The projection onto a nonempty closed convex set $X \subseteq \mathbb R^n$ is $\pi_X(y) = \arg\min\{\|y - x\|^2 : x \in X\}$ , the unique nearest point of $X$ to $y$ .
A subgradient of a convex function $F : \mathbb R^n \to \mathbb R$ at $x$ is a vector $g$ with $F(y) \ge F(x) + \langle g, y - x\rangle$ for all $y$ . The book writes $F^0_x(x, s)$ for a subgradient of $F^0(\cdot, s)$ at $x$ .
The nonstationary projected subgradient method (6.41) starts from any $x^0 \in \mathbb R^n$ and sets

x^{s+1} = \pi_X\bigl[x^s - \rho_s g_s\bigr], \qquad g_s \text{ a subgradient of } F^0(\cdot, s) \text{ at } x^s,\quad s = 0, 1, \dots

with step sizes $\rho_s \ge 0$ .

For a closed set $X^*$ (in the application, the set of minimizers of $f^0$ on $X$ ) and a sequence $(x^s)$ , the exit time from the $\varepsilon$ -ball around $x^{s_k}$ is $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ .
The Lyapunov function of the proof is $V(x) = \min_{x^* \in X^*}\|x^* - x\|^2$ , the squared distance to $X^*$ .

Formalization targets

Goal: Theorem 6.3 (pp. 153–154)

Let $F^0(\cdot, s)$ and $f^0$ be convex continuous on $\mathbb R^n$ , $X$ a nonempty convex compact set, $F^0(\cdot, s) \to f^0$ uniformly on $X$ , $\|g_s\| \le C$ , $\rho_s \ge 0$ , $\rho_s \to 0$ and $\sum_s \rho_s = \infty$ . Then the iterates of (6.41) satisfy

F^0(x^s, s) \longrightarrow \min\{f^0(x) \mid x \in X\} \qquad (s \to \infty).

The statement fixes no rate and no constant: only the qualitative limit, which is what the book proves.

Milestones

p. 155 — the one-step recursion $V(x^{s+1}) \le V(x^s) + 2\rho_s\langle g_s, x^*(s) - x^s\rangle + \rho_s^2\|g_s\|^2$ , with $x^*(s)$ a point of $X^*$ nearest to $x^s$ .
p. 156 — the travel bound $\|x^b - x^a\| \le \sum_{s=a}^{b-1}\|x^{s+1} - x^s\| \le C\sum_{s=a}^{b-1}\rho_s$ along (6.41) once $x^a \in X$ .
p. 155 — conditions (1) and (2)(a) of Theorem 6.4 for (6.41): the iterates stay in a compact set and $\|x^{s+1} - x^s\| \to 0$ .
Theorem 6.4 (p. 155) — if $X^*$ is closed, $(x^s)$ lies in a compact set, steps vanish along subsequences converging into $X^*$ , the sequence leaves every small ball around a subsequential limit outside $X^*$ , and it leaves with a strictly lower value of a continuous $V$ that takes countably many values on $X^*$ , then $V(x^s)$ converges and all accumulation points lie in $X^*$ .
pp. 155–156 — conditions (2)(b) and (3) of Theorem 6.4 for (6.41) with $X^* = \arg\min_X f^0$ and $V = \operatorname{dist}(\cdot, X^*)^2$ :

\limsup_{k\to\infty} V(x^{\tau_k}) < \lim_{k\to\infty} V(x^{s_k}).

Significance

Theorem 6.3 is the prototype of the convergence results for simultaneous optimization and approximation. It covers smoothing schemes in which $f^0$ is replaced by $F^0(x, s) = \mathbb E f^0(x + h(s))$ with a vanishing perturbation $h(s)$ (the chapter's (6.39)–(6.40)), penalty and regularization sequences, and the deterministic skeleton of stochastic nonstationary methods such as Theorem 6.5. Theorem 6.4 is reusable well beyond this mission: it is a general tool for proving that accumulation points of a nonmonotone algorithm are solutions; the chapter introduces it as the tool for "essentially nonmonotonic solution procedures" in general.

Both results are classical and proved (Theorem 6.3 in the chapter itself, Theorem 6.4 in Ermoliev's 1976 monograph, whose proof the chapter cites but does not reproduce). No machine-checked proof of either is known to the platform's catalogue (searches for nonstationary optimization, Zangwill-type criteria and nonmonotone convergence return no match). The formalization adds a Lean statement and proof of a nonmonotone convergence criterion, a Lean proof of convergence for projected subgradient steps on a changing objective, and reusable facts about Euclidean projection onto a convex compact set.

Difficulty

The obvious argument for projected subgradient methods tracks $V(x^s) = \operatorname{dist}(x^s, X^*)^2$ and shows that it decreases whenever $x^s$ is far from $X^*$ . Here that argument fails at two points. First, the subgradient is taken on $F^0(\cdot, s)$ , not on $f^0$ , so the decrease of $V$ holds only up to an error controlled by $\sup_X|F^0(\cdot, s) - f^0|$ , and only while the iterate stays away from $X^*$ ; near $X^*$ , $V$ may increase. Second, a decrease of $V$ over each excursion does not by itself exclude "cycling": the sequence may visit every neighbourhood of a point $x' \notin X^*$ infinitely often. Theorem 6.4 is formulated in terms of exit times and subsequences rather than single steps for this reason, and its hypothesis that $V$ takes only countably many values on $X^*$ is what separates it from a monotone-descent statement.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); sequences are indexed by ℕ from $s = 0$ as in the book. The iteration (6.41) is a hypothesis on a given sequence, x (s+1) = projX X (x s - ρ s • g s), with a given selection of subgradients g s; the subgradient inequality is required on all of $\mathbb R^n$ , and $F^0(\cdot, s)$ , $f^0$ are convex and continuous on all of $\mathbb R^n$ .
projX X y is a minimizer of $\|y - x\|^2$ over $X$ (junk value $y$ when none exists; every statement assumes $X$ nonempty, closed and convex). optimalSet f X is the set of minimizers of $f$ on $X$ ; $V$ is Metric.infDist · X* ^ 2.
Added hypotheses the page does not print: $\rho_s \ge 0$ (step sizes are nonnegative throughout the chapter) and $X \ne \varnothing$ (the minimum over $X$ must exist). The limit $\min_X f^0$ is written sInf (f '' X); $\sum_s\rho_s = \infty$ is divergence of the partial sums.
Constants. The only unspecified constant is the $C$ of the travel bound on p. 156 ("where $C$ is a constant"); the proof yields $C$ = the bound of hypothesis (d), $\|g_s\| \le C$ , and that is the constant in milestone 2. All other results are qualitative.
Corrections of the page. (i) Theorem 6.4 (2)(b) is printed as " $\tau_k = \min\{s \mid s \ge s_k, \|x^{s_k} - x^s\| < \varepsilon\} > \infty$ ", which no sequence satisfies; following the proof of Theorem 6.3 it is read as: $\tau_k = \min\{s \ge s_k : \|x^s - x^{s_k}\| > \varepsilon\}$ is finite. "For $\varepsilon$ sufficiently small and for any $s_k$ " is read as "there is $\varepsilon_0 > 0$ such that for all $\varepsilon \in (0,\varepsilon_0)$ and all $k$ ", and condition (3) is imposed for the same $\varepsilon$ . (ii) The left limit in (3) is read as $\limsup$ (the proof prints $\overline{\lim}$ ); the right limit is $V(x')$ . (iii) The display on p. 155 prints " $=$ " where the projection gives " $\le$ ". (iv) The proof on p. 155 prints " $x^{s_k} \to x' \in X^*$ " where $x' \notin X^*$ is meant.
Theorem 6.5 (the stochastic version, p. 156) is not formalized: the chapter states it without proof, citing [19], its moment hypothesis $E\|\xi^0(s)\| < \mathrm{const}$ and the measurability of the random step sizes $\rho_s$ are not pinned down on the page, and it is not used by Theorem 6.3.
A trivializing formalization is ruled out: the goal is about the iteration (6.41) itself, not a statement that assumes $x^s \to X^*$ and derives the limit of the values, and no hypothesis forces the sequence or the functions to be constant.
Contributions welcome: properties of projX (existence, uniqueness, nonexpansiveness, the obtuse-angle characterization), a proof of Theorem 6.4, and the two proof steps on pp. 155–156.

Selected references

Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, pp. 141–185 (§6.4, pp. 152–156). https://doi.org/10.1007/978-3-642-61370-8
Yu. M. Ermoliev, Stochastic Programming Methods (in Russian), Nauka, Moscow, 1976 (the chapter's [5]; Theorem 6.4 is on p. 181).
Yu. M. Ermoliev and E. A. Nurminski, "Limit extremal problems", Kibernetika 1 (1973) (the chapter's [14]).
E. A. Nurminski, "Convergence conditions of algorithms of stochastic programming", Kibernetika 3 (1973) (the chapter's [11]).
E. A. Nurminski, "The problem of nonstationary optimization", Kibernetika 2 (1977) (the chapter's [16]).
A. A. Gaivoronski, "Nonstationary stochastic programming problems", Kibernetika 4 (1978) (the chapter's [19]).
W. I. Zangwill, Nonlinear Programming: A Unified Approach, Prentice-Hall, 1969.

8 thms2 active usersReviewed

Completed

Information Theory Linear algebra Operations Research+1·Captain: naimengye

Decoding by Linear Programming: Exact Recovery by ℓ1 Minimization under the Restricted Isometry ConditionResearch Paper

Motivation

Consider the classical error-correcting problem. An input vector $f \in \mathbb{R}^n$ (the plaintext) is encoded as $Af \in \mathbb{R}^m$ by a coding matrix $A$ with $m > n$ , and an unknown, arbitrary vector of errors $e$ corrupts the result, so that only $y = Af + e$ is observed. Can $f$ be recovered exactly, and by an algorithm whose running time is polynomial in $m$ ? Candès and Tao (2005) answer both questions at once: if a matrix $F$ annihilating $A$ satisfies a restricted orthonormality condition, then $f$ is the unique solution of the convex program $\min_g \|y - Ag\|_{\ell^1}$ , which is a linear program, whenever at most $S$ entries of $y$ are corrupted, whatever their positions and values. Read for the matrix $F$ alone, the same theorem says that $\ell^1$ minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.

Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of $\ell^0$ and $\ell^1$ minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order $\sqrt{m}$ , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order $m/\log m$ . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction $\rho m$ of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, $\delta_S + \theta_{S,S} + \theta_{S,2S} < 1$ , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition $\delta_{2S} < \sqrt{2} - 1$ , sharpened the sufficient condition; those later results are not part of this mission.

Setting

Let $F$ be a real $p \times m$ matrix with columns $v_1, \dots, v_m \in \mathbb{R}^p$ , and let $H$ be the linear span of these columns. For an index set $T \subseteq \{1,\dots,m\}$ and real coefficients $c = (c_j)_{j \in T}$ , write $F_T c = \sum_{j \in T} c_j v_j$ . A vector $c \in \mathbb{R}^m$ is supported on $T$ when $c_j = 0$ for all $j \notin T$ ; with this convention $F_T c$ is just the product $Fc$ . Norms are the Euclidean norm $\|c\| = (\sum_j c_j^2)^{1/2}$ and the $\ell^1$ norm $\|c\|_{\ell^1} = \sum_j |c_j|$ .

Definition 1.1. For an integer $S$ , the $S$ -restricted isometry constant $\delta_S$ is the smallest quantity such that

(1 - \delta_S)\|c\|^2 \le \|F_T c\|^2 \le (1 + \delta_S)\|c\|^2

for all $T$ of cardinality at most $S$ and all real coefficients $(c_j)_{j \in T}$ . The $S, S'$ -restricted orthogonality constant $\theta_{S,S'}$ is the smallest quantity such that

|\langle F_T c, F_{T'} c' \rangle| \le \theta_{S,S'} \, \|c\| \, \|c'\|

for all disjoint $T, T'$ with $|T| \le S$ and $|T'| \le S'$ . The paper writes $\theta_S$ for $\theta_{S,S}$ . These numbers measure how far the columns of $F$ are from an orthonormal system when only linear combinations of at most $S$ columns are considered.

The two optimization problems are

(P_1)\quad \min_{d \in \mathbb{R}^m} \|d\|_{\ell^1} \ \text{ subject to } \ Fd = f, \qquad\qquad (P_1')\quad \min_{g \in \mathbb{R}^n} \|y - Ag\|_{\ell^1}.

A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.

Formalization targets

Goal: Theorem 1.5 (decoding by linear programming)

Let $A$ be a real $m \times n$ matrix of full rank with $m > n$ , and $F$ a real $p \times m$ matrix with $FA = 0$ . Let $S \ge 1$ satisfy

\delta_S(F) + \theta_{S,S}(F) + \theta_{S,2S}(F) < 1 . \tag{1.10}

If $y = Af + e$ where $e$ is supported on a set of size at most $S$ , then $f$ is the unique minimizer of $(P_1')$ .

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)

Let $S \ge 1$ satisfy (1.10) for $F$ , and let $c$ be supported on a set $T$ with $|T| \le S$ . Then $c$ is the unique minimizer of $(P_1)$ with $f := Fc$ .

Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the $\delta$ numbers control the $\theta$ numbers), Lemma 1.3 (uniqueness of sparse representations under $\delta_{2S} < 1$ ), and the two dual sparse reconstruction properties, Lemma 2.1 ( $\ell^2$ version) and Lemma 2.2 ( $\ell^\infty$ version).

Significance

The result. The guarantee is deterministic and uniform: one condition on $F$ , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of $S/m$ , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.

Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of $\delta_S$ and $\theta_{S,S'}$ exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.

Difficulty

The whole proof rests on a dual certificate: a vector $w \in H$ with $\langle w, v_j \rangle = \operatorname{sgn}(c_j)$ for $j \in T$ and $|\langle w, v_j \rangle| < 1$ for $j \notin T$ . Given such a $w$ , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is $w = F_T (F_T^* F_T)^{-1} \operatorname{sgn}(c)$ ; this interpolates the signs on $T$ and, by restricted orthogonality, its inner products off $T$ are small in an $\ell^2$ sense, but not in the $\ell^\infty$ sense required. That is exactly Lemma 2.1: the $\ell^\infty$ bound holds only outside an exceptional set of at most $S'$ indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on $T$ fixed, and summing a geometrically convergent series.

Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to $2S$ ( $T_0 \cup T_n$ ) at each step, while the per-step factors it quotes, $\theta_{S,2S}/(1-\delta_S)$ , are what Lemma 2.1 gives for a set of size $S$ ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with $\theta_S$ in its $\ell^2$ bound on the exceptional set, while the inequality (2.3) its proof establishes gives $\theta_{S,S'}$ ; the mission states the lemma with $\theta_{S,S'}$ , which coincides with the printed form in the case $S' = S$ used by Lemma 2.2.

Formalization scope

Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on $T$ is a vector in Fin m → ℝ supported on the finite set $T$ , and $F_T c$ is F.mulVec c. The Euclidean and $\ell^1$ norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. $H$ is the span of the columns.

The constants $\delta_S$ and $\theta_{S,S'}$ are the infimum of the set of nonnegative $\delta$ (resp. $\theta$ ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as $S = 0$ . The definitions are total in $S, S'$ , and each theorem carries the paper's domain conditions ( $S \ge 1$ , and $2S \le m$ , $3S \le m$ or $S + S' \le m$ as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has $\delta_S = \theta_{S,S'} = 0$ , so none of the statements is vacuous.

"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the $m \times n$ matrix $A$ with $m > n$ is injectivity of $g \mapsto Ag$ ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant $K > 0$ depending only on $\delta_S$ " is a positive function of the real number $\delta_S$ , quantified before all other data.

Out of scope, with the reason for each: Theorem 1.6 refers to a threshold $r^*(p,m)$ "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for $m$ and $p$ "large enough", with an unspecified threshold and an $o(1)$ term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant $C$ and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.

Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix $F_T^* F_T$ and its inverse under $\delta_S < 1$ , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to $\delta_{2S} < \sqrt{2} - 1$ ) belong to a separate mission.

Selected references

E. J. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51 (12), 2005, 4203–4215. https://doi.org/10.1109/TIT.2005.858979 (arXiv: https://arxiv.org/abs/math/0502327)
E. J. Candès, J. Romberg and T. Tao, Robust uncertainty principles: exact signal reconstruction from highly incomplete frequency information, IEEE Trans. Inform. Theory 52 (2), 2006. https://arxiv.org/abs/math/0409186
E. J. Candès and T. Tao, Near optimal signal recovery from random projections: universal encoding strategies?, IEEE Trans. Inform. Theory 52 (12), 2006. https://arxiv.org/abs/math/0410542
D. L. Donoho and X. Huo, Uncertainty principles and ideal atomic decomposition, IEEE Trans. Inform. Theory 47, 2001, 2845–2862. https://doi.org/10.1109/18.959265
S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20, 1999, 33–61. https://doi.org/10.1137/S1064827596304010
E. J. Candès, The restricted isometry property and its implications for compressed sensing, C. R. Acad. Sci. Paris, Ser. I 346, 2008, 589–592. https://doi.org/10.1016/j.crma.2008.03.014

9 thms2 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Analysis and Algorithms for Service Parts Supply Chains VIII: Bounds on Optimal Stock AllocationsTextbook

Motivation

Military and commercial service parts systems keep repairable parts at a central depot warehouse and at a set of operating bases. Chapter 10 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) turns from the planning models of the earlier chapters to execution. Each period, the stock that is at the depot or arriving there must be divided among the bases. The planner knows what is already in the pipeline and faces random demand at each base. The chapter's models are solved in a rolling-horizon manner. Each period's decisions are the first step of an optimal plan over a short horizon. That plan has to be computable at scale, for thousands of items and dozens of bases.

What makes this possible is a structural fact. In an optimal allocation, the cumulative stock sent to a base never exceeds what a single-period newsvendor problem at that base would ask for. This bound shrinks the allocation integer programs to linear programs of manageable size. This mission formalizes that bound and the facts it rests on.

Setting

Fix one item. Time is counted in whole periods $t = 0, 1, 2, \dots$ , and $J$ is the finite set of bases. For each base $j$ :

$T_{i0}$ is the repair lead time, so shipments are decided in periods $t = 0, \dots, T_{i0}$ ;
$T^r_{ij}$ and $T^e_{ij}$ are the regular and expedited transportation times from the depot to base $j$ , integers with $1 \le T^e_{ij} < T^r_{ij}$ ;
$\tilde S_{i0t}$ is the known cumulative supply at the depot through period $t$ (stock on hand plus arrivals already in the pipeline), and $\tilde S_{ijt}$ the known cumulative supply at base $j$ . The latter is constant for $t \ge T^r_{ij}$ , since nothing not yet shipped can arrive earlier than $T^r_{ij}$ by regular transport;
$X_{ijt}$ is the cumulative demand at base $j$ through period $t$ , a nonnegative integer random variable, nondecreasing in $t$ , with finite mean;
$h_{ij} > 0$ , $b_{ij} > 0$ and $e_{ij} \ge 0$ are the incremental holding, shortage and expediting costs.

If $S_{ijt}$ units have arrived at base $j$ by period $t$ , the expected cost of that period is

G_{ijt}(S) = h_{ij}\,E[S - X_{ijt}]^+ + b_{ij}\,E[X_{ijt} - S]^+,

and stock left at the end of the horizon costs

Q_{ij}(S) = h_{ij}\sum_{t > T^r_{ij} + T_{i0}} E[S - X_{ijt}]^+ .

The stock allocation model $\mathrm{SAM}_i$ chooses nonnegative integer regular shipments $y^r_{ijt}$ , $t = 0, \dots, T_{i0}$ , with cumulative shipments never exceeding cumulative depot supply. The cumulative stock at base $j$ is $S_{ijt} = \tilde S_{ij(T^r_{ij}-1)} + \sum_{t' \le t - T^r_{ij}} y^r_{ijt'}$ , and the model minimizes $\sum_j \{\sum_{t=T^r_{ij}}^{T^r_{ij}+T_{i0}} G_{ijt}(S_{ijt}) + Q_{ij}(S_{ij(T^r_{ij}+T_{i0})})\}$ . The extended model $\mathrm{ESAM}_i$ adds expedited shipments $y^e_{ijt}$ , which arrive after $T^e_{ij}$ periods at an extra cost $e_{ij}$ per unit.

The constrained newsvendor problem $\mathrm{CN}_{ijt}$ minimizes $G_{ijt}(S)$ over integers $S \ge \tilde S_{ijt}$ . Its largest optimal solution is written $\hat S_{ijt}$ .

Formalization targets

Goal: Theorem 15 (p. 237)

In every optimal solution of $\mathrm{SAM}_i$ , for every base $j$ and every $t \in [T^r_{ij}, T^r_{ij} + T_{i0}]$ ,

\tilde S_{ij(T^r_{ij}-1)} \;\le\; S^*_{ijt} \;\le\; \hat S_{ijt}.

The bound is uniform over optimal solutions and uses nothing but the single-period problems.

Milestones

Separability (Section 10.4.1, p. 236). The multi-item problem $\mathrm{SAM}$ splits into the $\mathrm{SAM}_i$ : its optimal solutions are exactly the tuples of optimal item solutions, and $Z^* = \sum_i Z^*_i$ .
Convexity of $Q_{ij}$ (p. 234) and of $G_{ijt}$ (p. 237), in the discrete sense of nondecreasing first differences on $\mathbb Z$ .
The newsvendor solution (10.19). $\hat S_{ijt} = \max(\tilde S_{ijt}, s^0)$ with $s^0$ the least integer such that $P(X_{ijt} \le s^0) > b_{ij}/(b_{ij}+h_{ij})$ .
Monotonicity (10.20). $\hat S_{ij(t-1)} \le \hat S_{ijt}$ on $[T^r_{ij}, T^r_{ij} + T_{i0}]$ .
Theorem 16, corrected (p. 244). In every optimal solution of $\mathrm{ESAM}_i$ , $\tilde S_{ijt} \le S^*_{ijt}$ . Writing $M_{jt} = \max_{k \in [T^e_{ij}, t]}(\hat S_{ijk} - \tilde S_{ijk})$ , also $S^*_{ijt} \le \tilde S_{ijt} + M_{jt}$ , provided $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$ .

Two supporting items state that $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ have optimal solutions. A third, theorem16_counterexample, exhibits an instance in which Theorem 16's upper bound, as printed, fails.

Significance

Theorem 15 is what allows the book (pp. 238–239) to rewrite $\mathrm{SAM}_i$ with 0–1 variables $\delta_{ijtk}$ indicating $S_{ijt} = k$ . Only $k$ between $\tilde S_{ij(T^r_{ij}-1)}$ and $\hat S_{ijt}$ is needed, so the number of variables is governed by the newsvendor quantities rather than by the total depot supply. Theorem 16 plays the same role for the model with expediting. Both bounds also justify the greedy heuristics of Sections 10.4.3 and 10.5.3. Those heuristics never raise a base's stock above its newsvendor level.

The book proves both theorems in half a page each by an exchange argument. This mission produces machine-checked versions and, in doing so, settles the exact scope of Theorem 16. As printed it is false. With $T^r_{ij} \ge T^e_{ij} + 2$ , an expedited shipment in the last decision period can be the only way to cover a later period's demand, and the optimal plan then overstocks an earlier period. The mission states the corrected theorem and the counterexample; the counterexample was checked in Lean during drafting. None of the chapter's results has been formalized before, as far as the platform's catalogue shows.

Difficulty

The central step is the exchange. Take the first period $k$ in which an optimal plan overshoots its bound, and delay by one period one unit that arrives at $k$ . This must be shown feasible, to change only $S_{ijk}$ , and to lower the objective strictly. That in turn needs strict decrease of a convex function to the right of its largest minimizer, and an argument for the last period, where there is no later period to delay into. The indexing is heavy: two lead times, truncated sums $\min(t - T^e_{ij}, T_{i0})$ , and cumulative constraints across bases.

The first idea, that a plan above the newsvendor level can always be improved by shipping less, fails. Shipping less changes the stock in every later period too, and later periods may need the unit. The bound follows only from a delay that affects exactly one period. For $\mathrm{ESAM}_i$ even such a delay is sometimes unavailable, which is where the book's Theorem 16 breaks.

Formalization scope

One item at a time: ItemModel J Ω P bundles the data of one item with the cumulative demands on a probability space $(\Omega, P)$ , [IsProbabilityMeasure P]. Bases form a Fintype. Periods are ℕ. Stock levels and supplies are ℤ, since net inventory may be negative. Shipments are functions J → ℕ → ℕ, so nonnegativity and integrality are built in. Costs are in ℝ.
$G$ and $Q$ are defined from the demand as in the book: Bochner integrals of $(S - X)^+$ and $(X - S)^+$ , and a tsum for $Q$ . The item model requires finite means and convergence of the series for $Q$ at every stock level, so that no integral or sum takes Lean's junk value $0$ .
"The largest optimal solution" is the predicate IsLargestCNSolution (feasible, minimizing, and above every feasible minimizer). Theorems take $\hat S$ as a function satisfying it. Milestone (10.19) shows it exists.
"An optimal solution" means a feasible plan with objective at most that of every feasible plan. The theorems hold for every optimal plan.
Pinned conventions and additions. The following are not written in the book: $h_{ij}, b_{ij} > 0$ and $e_{ij} \ge 0$ ; nonnegative, nondecreasing depot supply; nondecreasing base supply (used in the book's proof of Theorem 16); finite mean demand; convergence of $Q$ 's series. (10.19) is read with the critical fractile "least $s$ with $F(s) > b/(b+h)$ ", the book's $\lceil F^{-1}\rceil$ / $\lfloor F^{-1}\rfloor$ with ties broken upward. Theorem 16 carries the proviso " $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$ ". Separability is stated both for optimal plans and for optimal values.
Ruled out. The feasible sets of $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ impose no upper bound on the cumulative stock, and $\hat S$ is defined from $G$ alone, never from the allocation problem. The bounds are therefore not true by definition.
Omitted. The LP reformulations (10.22)–(10.28) and (10.45)–(10.52) and the integrality of their relaxations, which the book asserts with a reference to [68]; the greedy algorithms and their optimality conditions (asserted); the book's claim that $Q_{ij}$ is strictly increasing (p. 238), which fails when $P(X_{ijt} \le S) = 0$ beyond the horizon and is not needed; the dynamic program of Section 10.3 and the repair model of Section 10.6.
The discrete-convexity and newsvendor facts are reusable for any single-location inventory model on $\mathbb Z$ . Contributions are welcome on the convexity lemmas, the critical-fractile characterization, and a reusable exchange lemma for cumulative-shipment models.

Selected references

J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005, Chapter 10, pp. 225–246. DOI 10.1007/b138879
K. J. Arrow, T. Harris, J. Marschak, "Optimal inventory policy", Econometrica 19(3), 1951, 250–272 (the newsvendor critical fractile). DOI 10.2307/1906813

10 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Value of Information in Bayesian Routing Games II: Equilibrium Adoption Rates of Information Systems Are the Minimizers of the Equilibrium PotentialResearch Paper

Motivation

Traffic information systems (TIS) such as navigation apps send drivers private, noisy signals about the state of the road network: incidents, weather, closures. When several such systems coexist, their subscribers act on different information, and the congestion each population experiences depends on how all of them route. A question then arises for transport planners and for the information providers themselves: if travelers are free to choose which system to subscribe to, which market shares of the competing systems are stable?

Wu, Amin and Ozdaglar (Operations Research 69(1):148–163, 2021; preprint arXiv:1808.10590) model this situation as a Bayesian routing game with heterogeneous information and answer the question exactly: the equilibrium adoption rates are the minimizers of a convex function of the population sizes, the equilibrium value of a weighted potential. This mission formalizes that characterization (Theorem 4 of the paper) together with the results its proof rests on. A companion mission (Value of Information in Bayesian Routing Games I) formalizes the paper's other main result, the sign and monotonicity of the relative value of information between two populations.

Setting

A Bayesian routing game $\Gamma(\lambda)$ has a single origin–destination pair, a finite set of edges $\mathcal E$ and a finite nonempty set of routes $\mathcal R$ (each route a set of edges), and a finite set of network states $\mathcal S$ . Travelers of total demand $D>0$ are split into populations $i\in\mathcal I$ , one per TIS; population $i$ has size $\lambda^iD$ , where the size vector $\lambda$ lies in the simplex $\Delta=\{\lambda:\lambda^i\ge0,\ \sum_i\lambda^i=1\}$ . Each population receives a signal (its type) $t^i$ from a finite set $\mathcal T^i$ ; states and type profiles $t=(t^i)_i$ are drawn from a common prior $\pi\in\Delta(\mathcal S\times\mathcal T)$ . Edge $e$ in state $s$ has cost $c^s_e(w)$ at load $w$ , positive, strictly increasing and differentiable.

A strategy profile $q$ assigns to each population and type a split $q^i_r(t^i)\ge0$ of its demand over routes, with $\sum_rq^i_r(t^i)=\lambda^iD$ ; these form the polytope $\mathcal Q(\lambda)$ . It induces route flows $f_r(t)=\sum_iq^i_r(t^i)$ and edge loads $w_e(t)=\sum_{r\ni e}f_r(t)$ . A traveler of population $i$ with signal $t^i$ forms the belief $\beta^i(s,t^{-i}\mid t^i)=\pi(s,t^i,t^{-i})/\Pr(t^i)$ and evaluates the expected route cost $\mathbb E[c_r(q)\mid t^i]=\sum_{s,t^{-i}}\sum_{e\in r}\beta^i(s,t^{-i}\mid t^i)\,c^s_e(w_e(t))$ . A Bayesian Wardrop equilibrium (BWE) is a $q\in\mathcal Q(\lambda)$ in which every type uses only routes of minimal expected cost. The equilibrium population cost is

C^{i*}(\lambda)=\sum_{t^i\in\mathcal T^i}\Pr(t^i)\min_{r\in\mathcal R}\mathbb E[c_r(q^*)\mid t^i].

The weighted potential is $\Phi(q)=\sum_{s,e,t}\pi(s,t)\int_0^{w_e(t)}c^s_e(z)\,dz$ , and $\Psi(\lambda)=\min_{q\in\mathcal Q(\lambda)}\Phi(q)$ is its equilibrium value. In route-flow form, $\widehat\Phi(f)$ is the same expression in terms of $f$ ; route flows satisfy linear constraints (14a)–(14c) (a separability condition across populations, total demand $D$ , nonnegativity) and one information impact constraint per population, $\widehat J^i(f)\le\lambda^iD$ , where $\widehat J^i(f)=D-\sum_r\min_{t^i}f_r(t^i,\widehat t^{-i})$ measures how much of the demand reacts to population $i$ 's signal. Let $\mathcal F^\dagger$ be the set of minimizers of $\widehat\Phi$ subject to (14a)–(14c) only, and

\Lambda^\dagger=\{\lambda\in\Delta:\ \exists f^\dagger\in\mathcal F^\dagger,\ \widehat J^i(f^\dagger)\le\lambda^iD\ \ \forall i\}.

In the two-stage game, travelers first choose a TIS, inducing $\lambda$ , and then play $\Gamma(\lambda)$ . A size vector is a vector of equilibrium adoption rates if no traveler gains by switching TIS:

\lambda^i>0\ \Longrightarrow\ C^{i*}(\lambda)=\min_{j\in\mathcal I}C^{j*}(\lambda)\qquad\forall i\in\mathcal I.\tag{31}

Formalization targets

Goal: Theorem 4

For every $\lambda\in\Delta$ and every BWE of $\Gamma(\lambda)$ ,

(31)\ \text{holds}\iff\lambda\in\Lambda^\dagger .

With the existence of a BWE for every $\lambda\in\Delta$ , this is the paper's statement that the set of equilibrium adoption rates is $\Lambda^\dagger$ .

Milestones

Theorem 1. $q$ is a BWE of $\Gamma(\lambda)$ iff $q$ minimizes $\Phi$ over $\mathcal Q(\lambda)$ ; the equilibrium edge load $w^*(\lambda)$ is unique.
Proposition 2. A route flow in the flow polytope $\mathcal F(\lambda)$ ((14a)–(14c) plus all information impact constraints) is an equilibrium flow iff it minimizes $\widehat\Phi$ over $\mathcal F(\lambda)$ .
Lemma 5. $\Psi$ is convex on $\Delta$ , and with $z^{ij}=e_i-e_j$ and $V^{ij*}=C^{j*}-C^{i*}$ ,

\lim_{\epsilon\to0^+}\frac{\Psi(\lambda+\epsilon z^{ij})-\Psi(\lambda)}{\epsilon}=-D\,V^{ij*}(\lambda).

Proposition 5. $\Lambda^\dagger$ is convex, $\Lambda^\dagger=\operatorname{argmin}_{\lambda\in\Delta}\Psi(\lambda)$ , and the equilibrium edge load equals the size-independent load $w^\dagger$ of $\mathcal F^\dagger$ iff $\lambda\in\Lambda^\dagger$ .

A separate item states the existence of a BWE for every $\lambda\in\Delta$ .

Significance

The result. Theorem 4 reduces a question about a two-stage game with a continuum of travelers and private signals to the minimization of one convex function over a simplex. It shows that the stable market shares form a convex set, generally not a single point, so each system's equilibrium adoption rate ranges over an interval; and that this set is determined by the joint information environment of all systems, not by each system's signal alone. On $\Lambda^\dagger$ the equilibrium edge load does not depend on the shares at all, which identifies when changes in market shares leave congestion unchanged.

Formalizing it. The proofs of Theorem 1, Proposition 2 and Proposition 5 are in the paper's online e-companion, and Lemma 5 relies on sensitivity results for parametric convex programs cited from the literature. No part of this development has, to our knowledge, been machine-checked. A complete formalization would produce a verified potential-game characterization of Bayesian Wardrop equilibria with heterogeneous information and a verified directional-derivative formula for the optimal value of a parametric convex program; nothing comparable is currently on the platform (the existing Wardrop development covers complete information only).

Difficulty

The direction " $\lambda\in\Lambda^\dagger$ implies (31)" is not a pointwise statement about costs: it follows from $\Lambda^\dagger$ being the argmin of $\Psi$ together with the formula linking directional derivatives of $\Psi$ to cost differences. Both are hard. The derivative formula (26) is a statement about the optimal value of a convex program whose feasible set moves with $\lambda$ ; its standard proofs pass through uniqueness of Lagrange multipliers, which fails exactly at the degenerate size vectors ( $\lambda^i=0$ ) that Theorem 4 must cover, since an unused TIS is a legitimate outcome. The identity $\Lambda^\dagger=\operatorname{argmin}\Psi$ needs the route-flow reformulation (Proposition 2), in which the size vector enters only through the information impact constraints, and the uniqueness of the minimizing edge load. The natural first idea, comparing population costs directly at a given equilibrium, gives no handle on which size vectors make them equal.

Formalization scope

The Lean development lives in the namespace BayesRouting.Adoption. Populations, types, states, edges and routes are finite types; type spaces and the route set are nonempty; routes are edge sets. The game is a structure whose fields include the paper's standing assumptions: the prior is a probability distribution, $D>0$ , and each cost is positive on nonnegative loads, strictly increasing and differentiable (on all of $\mathbb R$ , which loses no generality). One assumption is added: every type profile has positive probability. Without it the equilibrium edge load need not be unique and the beliefs can be undefined; it excludes the paper's Example 2(i) (perfectly correlated signals).

Conventions: size vectors range over the probability simplex; $\Psi$ is the infimum of $\Phi$ over $\mathcal Q(\lambda)$ and is only compared at points of the simplex (outside it the feasible set can be empty and the value is a default); $C^{i*}$ is the last form of the paper's (7), well defined when $\lambda^i=0$ ; $\widehat J^i$ is the maximum over reference profiles, which equals the paper's value on flows satisfying (14a); equilibrium statements are made for every BWE rather than for "the" equilibrium; $\mathcal F^\dagger$ and similar sets are argmin sets. Lemma 5 is stated for the directions $z^{ij}$ with $\lambda^j>0$ (otherwise $\lambda+\epsilon z^{ij}$ leaves the simplex); $\lambda^i=0$ is allowed.

A trivializing formalization is ruled out: the existence of a BWE is its own item, so "for every BWE" is not vacuous, and $\Lambda^\dagger$ is defined by (30) from the flow problem (28), not as the argmin of $\Psi$ , so the goal is not a restatement of Proposition 5.

Infrastructure a complete development needs: KKT conditions for convex programs with linear constraints, convexity of integrals of increasing functions, compactness arguments for existence of minimizers, and one-sided directional derivatives of optimal-value functions. The last two are reusable well beyond this mission. Proofs of any item, and of auxiliary lemmas such as Proposition 1 of the paper (feasible route flows form the polytope $\mathcal F(\lambda)$ ), are welcome.

Selected references

M. Wu, S. Amin, A. E. Ozdaglar, Value of Information in Bayesian Routing Games, Operations Research 69(1):148–163, 2021. https://doi.org/10.1287/opre.2020.1999 (preprint: https://arxiv.org/abs/1808.10590)
W. H. Sandholm, Potential games with continuous player sets, Journal of Economic Theory 97(1):81–108, 2001. https://doi.org/10.1006/jeth.2000.2696
A. V. Fiacco, J. Kyparisis, Convexity and concavity properties of the optimal value function in parametric nonlinear programming, Journal of Optimization Theory and Applications 48(1):95–126, 1986. https://doi.org/10.1007/BF00938592

9 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Optimization·Captain: mikedeng1

Value of Information in Bayesian Routing Games I: Sign and Monotonicity of the Relative Value of Information Across Size RegimesResearch Paper

Motivation

Traffic information systems (TIS) such as navigation apps send drivers noisy signals about the state of a road network: incidents, weather, closures. When several such systems coexist, each with its own subscriber base and its own information, a natural question for operators and regulators is whether subscribing to one system rather than another actually lowers a driver's expected travel cost in equilibrium, and how this advantage depends on how many drivers use each system. More information for one population also changes the congestion everybody else faces, so the answer is not simply "more information is better".

Wu, Amin and Ozdaglar (Operations Research 69(1), 2021) answer this question for nonatomic routing games with heterogeneous, possibly correlated information. Their model builds on the weighted potential game framework of Sandholm (2001) and on sensitivity analysis of convex programs. This mission formalizes their Section 5 result: for any two populations the sign of the relative value of information is determined by which of three explicitly computable size regimes the population sizes lie in, and the relative value decreases as one population grows at the expense of the other.

Setting

A Bayesian routing game has a finite set of populations $\mathcal I$ , one per TIS, a finite set of network states $\mathcal S$ , and for each population $i$ a finite nonempty type space $\mathcal T^i$ of signals. A common prior $\pi$ is a probability distribution on $\mathcal S\times\mathcal T$ , $\mathcal T=\prod_i\mathcal T^i$ . A network with a single origin–destination pair has edges $\mathcal E$ and a finite nonempty set of routes $\mathcal R$ ; each edge has a state-dependent cost $c^s_e$ that is positive, strictly increasing and differentiable. The total demand is $D>0$ , and population $i$ carries the fraction $\lambda^i$ of it, with $\lambda^i\ge0$ and $\sum_i\lambda^i=1$ .

A strategy profile $q$ assigns to each population $i$ and type $t^i$ a split $q^i_r(t^i)\ge0$ of its demand $\lambda^iD$ over routes. It induces the route flow $f_r(t)=\sum_iq^i_r(t^i)$ and the edge load $w_e(t)=\sum_{r\ni e}f_r(t)$ . With the belief $\beta^i(s,t^{-i}\mid t^i)=\pi(s,t^i,t^{-i})/\Pr(t^i)$ , type $t^i$ evaluates route $r$ by its expected cost $\mathbb E[c_r(q)\mid t^i]$ . A Bayesian Wardrop equilibrium (BWE) is a feasible $q$ in which every type uses only routes of minimal expected cost. The equilibrium population cost is $C^{i*}(\lambda)=\sum_{t^i}\Pr(t^i)\min_r\mathbb E[c_r(q)\mid t^i]$ at a BWE $q$ .

The game has a weighted potential $\Phi(q)=\sum_{s,e,t}\pi(s,t)\int_0^{w_e(t)}c^s_e(z)\,dz$ ; its minimum over feasible profiles is the equilibrium potential value $\Psi(\lambda)$ . For two populations $i\ne j$ , the direction $z^{ij}$ moves demand share from $j$ to $i$ , and $|\lambda^{-ij}|$ is the total share of the other populations. The impact of information $\widehat J^i(f)$ measures how much of population $i$ 's demand is moved by its signal. Two thresholds $\underline\lambda^i\le\overline\lambda^i$ are computed from the optimal set $\mathcal F^{ij,\dagger}$ of an auxiliary convex program over route flows in which the separate information constraints of $i$ and $j$ are merged. They define three regimes: $\Lambda^{ij}_1$ ( $\lambda^i<\underline\lambda^i$ ), $\Lambda^{ij}_2$ ( $\underline\lambda^i\le\lambda^i\le\overline\lambda^i$ ) and $\Lambda^{ij}_3$ ( $\lambda^i>\overline\lambda^i$ ). The relative value of information is $V^{ij*}(\lambda)=C^{j*}(\lambda)-C^{i*}(\lambda)$ .

Formalization targets

Goal: Theorem 3

For $i\ne j$ and admissible $\lambda$ (in the simplex with $\lambda^i,\lambda^j>0$ ), and every BWE of $\Gamma(\lambda)$ ,

V^{ij*}(\lambda)>0 \text{ on } \Lambda^{ij}_1,\qquad V^{ij*}(\lambda)=0 \text{ on } \Lambda^{ij}_2,\qquad V^{ij*}(\lambda)<0 \text{ on } \Lambda^{ij}_3,

and $V^{ij*}$ is nonincreasing along $z^{ij}$ : $V^{ij*}(\lambda+\varepsilon z^{ij})\le V^{ij*}(\lambda)$ for $\varepsilon>0$ with both endpoints admissible.

Milestones

The route to the goal follows the paper: Lemma 1 (weighted potential), Lemma 2 (strict convexity of the edge-load potential), Theorem 1 (equilibria are the minimizers of $\Phi$ ; unique edge load), Lemma 3 (unique Lagrange multipliers), Proposition 1 (the feasible route flows form a polytope $\mathcal F(\lambda)$ ), Proposition 2 (equilibrium route flows minimize $\widehat\Phi$ over $\mathcal F(\lambda)$ ), Lemma 4 ( $0\le\underline\lambda^i\le\overline\lambda^i\le1-|\lambda^{-ij}|$ ), Theorem 2 (equilibrium flows in each regime), Proposition 3 ( $\Psi$ decreases, stays constant, increases along $z^{ij}$ in the three regimes) and Lemma 5 ( $\Psi$ is convex and directionally differentiable, and $V^{ij*}(\lambda)=-\frac1D\nabla_{z^{ij}}\Psi(\lambda)$ ).

Significance

Theorem 3 says that a population has an advantage over another exactly when it is the minor population of the pair, relative to thresholds that depend only on the other populations' sizes. Both populations face the same equilibrium cost in the middle regime. It gives a procedure for comparing two information systems without computing equilibria for each size vector: solve one convex program, read off two thresholds, and locate $\lambda^i$ . The paper's Section 6 uses the same machinery, through Lemma 5, to characterize the equilibrium adoption rates of information systems.

The paper proves these results with the main proofs in the article and the sensitivity-analysis lemmas (Lemmas EC.1–EC.4) in its e-companion. None of them has a machine-checked proof. The formalization requires a Lean account of Bayesian Wardrop equilibria, of the equivalence between equilibria and a convex program, and of directional derivatives of the optimal value of a parametric convex program. Parts of this are reusable for any nonatomic routing or congestion game.

Difficulty

The equilibrium strategy profile is not unique and changes discontinuously with $\lambda$ . Differentiating equilibrium costs in $\lambda$ directly therefore fails. The paper instead works with the optimal value $\Psi(\lambda)$ , whose one-sided directional derivative is expressed through Lagrange multipliers. That requires a sensitivity theorem for convex programs whose constraints depend affinely on the parameter, together with uniqueness of multipliers, which fails for populations of size zero. The regime analysis also needs a characterization of the route flows that are induced by feasible strategy profiles. That set is described by the nonlinear-looking constraint $\widehat J^i(f)\le\lambda^iD$ , a minimum over types inside a sum over routes. Strict monotonicity of $\Psi$ in the side regimes needs the tightness of an information constraint at every equilibrium, not only at one.

Formalization scope

The model is a Lean structure BayesRouting.VOI.Game over finite types of populations, type spaces, states, edges and routes. Routes are given by their edge sets, and the directed-graph structure is not used. Type spaces and the route set are nonempty. The prior is a probability distribution, $D>0$ , and costs are positive on nonnegative loads, strictly increasing and differentiable on $\mathbb R$ . One assumption is added: every type profile has positive probability. It makes beliefs well defined and the equilibrium edge load unique, and it excludes perfectly correlated signals.

Conventions: $C^{i*}$ is the last form of eq. (7), which does not divide by $\lambda^iD$ . $\widehat J^i$ is the maximum of eq. (16) over the reference profile, so that $\widehat J^i(f)\le\lambda^iD$ is exactly (14d). $\Psi$ and the thresholds are sInf/sSup over sets that are nonempty and compact for size vectors in the simplex, and every statement keeps size vectors there. Statements about "the" equilibrium are stated for every BWE, and existence of a BWE is a separate item, so they are not vacuous. The thresholds are defined from the optimal set of the auxiliary program, not assumed as parameters. Taking them as parameters constrained only by Lemma 4 would give a different theorem.

Disclosed deviations: Lemma 2's $C^2$ clause assumes $C^1$ costs; Lemma 3 is stated for populations of positive size; Lemma 5 assumes $\lambda^j>0$ ; Proposition 3 is stated with strict monotonicity in the side regimes, as used in the proof of Theorem 3. Contributions of reusable infrastructure are welcome: interval-integral potentials of monotone costs, KKT theory for polyhedral constraints, and directional derivatives of parametric optimal values.

Selected references

M. Wu, S. Amin, A. Ozdaglar, Value of Information in Bayesian Routing Games, Operations Research 69(1):148–163, 2021. https://doi.org/10.1287/opre.2020.1999
W. H. Sandholm, Potential Games with Continuous Player Sets, Journal of Economic Theory 97(1):81–108, 2001. https://doi.org/10.1006/jeth.2000.2696
R. T. Rockafellar, Directional Differentiability of the Optimal Value Function in a Nonlinear Programming Problem, in Sensitivity, Stability and Parametric Analysis (Mathematical Programming Studies 21), Springer, 1984, pp. 213–226.
A. V. Fiacco, J. Kyparisis, Convexity and Concavity Properties of the Optimal Value Function in Parametric Nonlinear Programming, Journal of Optimization Theory and Applications 48(1):95–126, 1986.

15 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program II: Stability of the Deterministic Equivalent Convex ProgramResearch Paper

Motivation

A two-stage stochastic linear program with fixed recourse chooses a first-stage decision $x$ before a random vector $\xi$ is observed, and then pays for a cheapest corrective action $y$ once $\xi$ is known. It is the basic model of planning under uncertainty in operations research: capacity expansion, production planning with random demand, and energy dispatch are all written in this form, and every decomposition algorithm of the field (L-shaped, stochastic decomposition, progressive hedging) works on it.

Roger J.-B. Wets' survey Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program (SIAM Review, 1974) collected the structural theory of this model: where the problem is feasible (§4), what the expected cost looks like as a function of $x$ (§7), and when the resulting convex program is well behaved (§8). This mission formalizes the second chain, from the polyhedral structure of the recourse function to the stability of the deterministic equivalent program: the existence of an optimal Lagrange multiplier for the first-stage constraints. Stability is what makes the optimal value react at a bounded rate to perturbations of the first-stage right-hand side, and it is the hypothesis under which dual and decomposition methods have something to converge to.

Setting

The data are a random element $\xi=(c,q,p,T)$ with $c\in\mathbb R^n$ , $q\in\mathbb R^{\bar n}$ , $p\in\mathbb R^{\bar m}$ and $T$ an $\bar m\times n$ matrix, distributed according to a probability measure $\mu$ . The recourse matrix $W$ ( $\bar m\times\bar n$ ), the first-stage matrix $A$ ( $m\times n$ ) and $b\in\mathbb R^m$ are fixed. The recourse function is

Q(x,\xi)=\min\{q(\xi)y \mid Wy=p(\xi)-T(\xi)x,\ y\ge0\},

equal to $+\infty$ if the second-stage program is infeasible and $-\infty$ if it is unbounded.

The weak covariance condition (Definition 2.2) requires $c_j$ , $q_jp_i$ and $q_jt_{ik}$ to be integrable for all indices; it does not require $q$ , $p$ or $T$ themselves to be integrable. The paper also assumes throughout that $W$ has full row rank (p. 312).

Expectations use the paper's integral: positive part minus negative part, with each part infinite if its integral diverges or the integrand is infinite on a set of positive measure, and $(+\infty)+(-\infty)=+\infty$ . The expected recourse is $\mathcal Q(x)=E_\xi\{Q(x,\xi)\}$ and the objective is

Z(x)=\bar c\,x+\mathcal Q(x),\qquad \bar c=E_\xi\{c(\xi)\}.

The induced constraints are $K_2=\bigcap_{\zeta\in\tilde\Xi_{p,T}}\{x : p-Tx\in\operatorname{pos}W\}$ , where $\operatorname{pos}W=\{Wy:y\ge0\}$ and $\tilde\Xi_{p,T}$ is the support of the distribution of $(p,T)$ . The fixed constraints are $K_1=\{x: Ax=b,\ x\ge0\}$ , and $K=K_1\cap K_2$ . The deterministic equivalent program (8.2) is to minimize $Z$ over $K$ .

A convex program of the form $\min\{f(x) : Ax=b,\ x\ge0,\ x\in D\}$ with finite value $v$ is stable (Definition 8.1(iv)) if there is $\pi\in\mathbb R^m$ with $v\le f(x)+\pi(b-Ax)$ for all $x\in D$ , $x\ge0$ . Equivalently, the dual obtained by perturbing $b$ is solvable and has no duality gap.

Formalization targets

Goal: Theorem 8.11 (p. 337)

If the weak covariance condition holds, $W$ has full row rank, $K_2$ is a polyhedron and the program is finite, $v=\inf_K Z\in\mathbb R$ , then

\exists\,\pi\in\mathbb R^m:\quad v\le Z(x)+\pi\,(b-Ax)\quad\text{for all }x\in K_2,\ x\ge0 .

Milestones

Corollary 7.3 (p. 328). The value $t\mapsto\min\{cx\mid Ax=t,\ x\ge0\}$ is a finite maximum of affine functions on $\operatorname{pos}A$ , or $-\infty$ on all of $\operatorname{pos}A$ .
Proposition 7.5 (p. 329). $Q(x,\xi)$ is convex polyhedral in $x$ on $K_2$ for each $\xi$ in the support, concave polyhedral in $q$ , and convex polyhedral in $(p,T)$ .
Theorem 7.6 (p. 329). $Z$ is convex on $K$ , and it is either finite on $K$ or identically $-\infty$ on $K$ .
Theorem 7.7 (pp. 329–330). If $Z>-\infty$ on $K$ , then $|Z(x)-Z(x^0)|\le\bar B\|x-x^0\|$ on $K$ (Euclidean norm).
Lemma 8.9 (p. 337). A finite program $\min\{f(x): Ax=b,\ x\ge0\}$ whose objective is convex and Lipschitz on a polyhedral domain is stable.

Significance

Stability of (8.2) is the regularity property that the dual and sensitivity theory of two-stage programs relies on. It gives a finite Lagrange multiplier for the first-stage constraints, a supporting hyperplane of the perturbation function $\phi(u)=\inf\{Z(x) : Ax=b-u,\ x\in K_2\cap\mathbb R^n_+\}$ at $u=0$ , and hence a bounded rate of change of the optimal value under perturbations of $b$ . The route through Theorems 7.6 and 7.7 also yields facts that are used on their own: the objective is a convex function that is either finite or identically $-\infty$ on the feasible region, and it is Lipschitz with a constant controlled by the weak covariance moments.

The results have been proved since 1974, and Lemma 8.9 is cited there to Walkup and Wets (1969). As far as the platform's catalog shows, none of them is formalized for a general distribution. The platform has finite-scenario versions of related facts from Birge and Louveaux's textbook, Chapter 3: StochasticProg.Recourse.thm6a_Q_lipschitz_convex_finite (the expected recourse is finite, convex and Lipschitz on $K_2$ for finitely many scenarios) and StochasticProg.Recourse.thm5a_K2_closed_convex. A complete development would supply the general-distribution versions, with the paper's own extended integral.

Difficulty

The obvious argument for Theorem 7.7 integrates a pointwise Lipschitz constant of $Q(\cdot,\xi)$ . It fails unless that constant is integrable, and the weak covariance condition, not integrability of $\xi$ , is what has to deliver this, uniformly over the finitely many second-stage bases.

For the goal, convexity and finiteness of the program are not enough. The paper's Example 8.5 has a finite convex deterministic equivalent with an infinite duality gap, and the counterexample under Formalization scope has a finite value and no multiplier. When the domain of $Z$ has curved boundary, the perturbation function can have infinite slope at $0$ ; the polyhedral hypothesis on $K_2$ is what excludes this.

Formalization scope

Types. Vectors are Fin n → ℝ; matrices are Matrix (Fin _) (Fin _) ℝ; row vectors of the paper ( $c$ , $q$ , $\pi$ ) enter through dotProduct. The law $\mu$ is a probability measure on (Fin n → ℝ) × (Fin n̄ → ℝ) × (Fin m̄ → ℝ) × (Fin m̄ → Fin n → ℝ). $Q$ is the platform definition KallMayer.Recourse.PointwiseRecourse, an EReal-valued infimum. Supports are MeasureTheory.Measure.support.
The integral. $\mathcal Q$ is written as lintegral of the positive part minus lintegral of the negative part, with $+\infty$ whenever the positive part is $+\infty$ . This is the paper's $(+\infty)+(-\infty)=+\infty$ ; Mathlib's EReal subtraction resolves the other way. A Bochner integral of toReal would be $0$ for non-integrable integrands and make every expected-cost statement trivial, and it is not used. $\bar c$ is a Bochner integral, legitimate because Definition 2.2 makes each $c_j$ integrable.
Readings of informal words.
- "Has first moments" is Integrable.
- "Convex polyhedron" means finitely many weak linear inequalities; $\emptyset$ and $\mathbb R^n$ are included.
- "Finite convex (concave) polyhedral function on $S$ " means equal on $S$ to the maximum (minimum) of finitely many affine functions. The $x$ and $(p,T)$ parts of Proposition 7.5 are stated as a dichotomy with the identically $-\infty$ case; the $q$ part is stated, as Corollary 7.4 gives it, as finite concave polyhedral on $\operatorname{pos}(W^T,-W^T,I)$ when the recourse problem is feasible.
- "Convex" for the extended-real $Z$ (Theorem 7.6) is ConvexOn of toReal on the finite branch.
- "Bounded on $K$ " (Theorem 7.7) is read as $Z>-\infty$ on $K$ , the proof's own reading. Finiteness on $K$ is part of the conclusion.
- "Convex and Lipschitz on a polyhedron" (Lemma 8.9) means the objective's domain is the polyhedron.
- "The program is finite" means the infimum over $K$ is a real number.
- "Stable" is the Kuhn–Tucker form above: a multiplier compared against the primal value, not merely a solvable dual. The latter would allow a duality gap.
Standing assumptions. Full row rank of $W$ appears in Theorems 7.7 and 8.11, where the proof uses square nonsingular submatrices of $W$ . It is omitted from Theorem 7.6 and Corollary 7.3 (Theorem 7.2's rank assumption), where it is not needed; this makes those statements stronger.
Corrections to the page. Theorem 8.11 is printed with " $K$ is polyhedral", $K=K_1\cap K_2$ , and read literally it is false. Take $T(\xi)$ uniform on the unit circle, $p\equiv1$ , $W=(1)$ , $q\equiv0$ , $c\equiv(-1,0)$ and $K_1=\{x_2=1,\ x\ge0\}$ . Then $K_2$ is the unit disk and $K=\{(0,1)\}$ is polyhedral with finite value $0$ , but no multiplier exists. The goal therefore assumes " $K_2$ is polyhedral", as the sentence before Lemma 8.9 and the proof require. In the dual (8.3) the page writes $c$ for $\bar c$ .
Ruled out. A statement of stability as "the dual supremum is attained" without equality to the primal value is not the goal, and neither is a hypothesis making $K$ empty or $Z$ identically $-\infty$ : the finiteness hypothesis excludes both.
Infrastructure. The needed pieces are Minkowski–Weyl for polyhedra (PointedCone.FG/DualFG in Mathlib), LP duality with $\pm\infty$ values, the paper's extended integral, and a Kuhn–Tucker theorem for convex programs with polyhedral constraints (Rockafellar, Convex Analysis, Thm 28.2). Corollary 7.3 and Lemma 8.9 contain no probability and are reusable across convex analysis. Proofs of any milestone, and lemmas on the paper's extended integral (monotonicity, subadditivity), are welcome.

Selected references

R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
D. W. Walkup and R. J.-B. Wets, Stochastic programs with recourse, SIAM J. Appl. Math. 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
R. M. Van Slyke and R. J.-B. Wets, A duality theory for abstract mathematical programs with applications to optimal control theory, J. Math. Anal. Appl. 22(3):679–706, 1968 (cited by Wets for Definition 8.1 and the dual (8.3)).
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 3. https://doi.org/10.1007/978-1-4614-0237-4

10 thms2 active usersReviewed

Completed

Numerical Analysis Operations Research Optimization·Captain: mikedeng1

A New Projection Method for Variational Inequality Problems: The Hyperplane Projection Method Converges to a Solution Under Continuity and Generalized MonotonicityResearch Paper

Motivation

A variational inequality asks for a point of a convex set at which a vector field points "inward" against every feasible direction. The format covers the first-order optimality conditions of constrained optimization, nonlinear complementarity problems, traffic and economic equilibria (Wardrop, Walrasian, Nash–Cournot), and systems of nonlinear equations; see Harker and Pang's survey (Math. Programming 48, 1990) and Facchinei and Pang's monograph (Springer, 2003).

When the map has no special structure (not strongly monotone, not Lipschitz with known constant, not affine) and the feasible set is a general closed convex set, the practical algorithms are projection methods. The oldest is Korpelevich's extragradient method (1976). Without a known Lipschitz constant, extragradient-type methods need a linesearch in which every trial point costs one projection onto the feasible set, and projection onto a general convex set is itself an optimization problem.

Solodov and Svaiter (SIAM J. Control Optim. 37 (1999) 765–776) proposed a method that spends exactly two projections per iteration, whatever the linesearch does, and proved global convergence under only continuity of the map and a generalized monotonicity condition weaker than pseudomonotonicity. The method, often called the hyperplane projection method, is a standard reference point for later projection and extragradient-type algorithms.

Timeline:

1976: Korpelevich, extragradient method, Lipschitz monotone maps.
1987–1994: Khobotov (1987), Iusem (1994) and others: extragradient variants with Armijo-type stepsize rules, which need one projection per trial step.
1997: Iusem and Svaiter, a separating-hyperplane variant of extragradient for monotone maps (reference [9] of the paper).
1999: Solodov and Svaiter, Algorithm 2.1: two projections per iteration, convergence under condition (1.2) below.

Setting

Work in $\mathbb{R}^n$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . Let $C \subseteq \mathbb{R}^n$ be closed and convex and $F : \mathbb{R}^n \to \mathbb{R}^n$ continuous. The problem $\mathrm{VI}(F, C)$ is to find $x^*$ with

x^* \in C, \qquad \langle F(x^*), x - x^*\rangle \ge 0 \quad \text{for all } x \in C. \tag{1.1}

Its solution set is $S$ . The projection onto a nonempty closed convex set $K$ is $P_K[x] := \arg\min_{y \in K}\|y - x\|$ . The projected residual is $r(x) := x - P_C[x - F(x)]$ ; its zeros are exactly the points of $S$ .

Condition (1.2) requires, for every $x^* \in S$ ,

\langle F(x), x - x^*\rangle \ge 0 \qquad \text{for all } x \in C. \tag{1.2}

It holds when $F$ is monotone or pseudomonotone, and in cases where $F$ is neither.

Algorithm 2.1. Fix $\gamma, \sigma \in (0,1)$ and $x^0 \in C$ . Given $x^i$ : if $r(x^i) = 0$ , stop. Otherwise let $k_i$ be the smallest nonnegative integer $k$ with

\langle F(x^i - \gamma^k r(x^i)), r(x^i)\rangle \ge \sigma\|r(x^i)\|^2, \tag{2.1}

set $\eta_i = \gamma^{k_i}$ , $z^i = x^i - \eta_i r(x^i)$ , $H_i = \{x \mid \langle F(z^i), x - z^i\rangle \le 0\}$ , and

x^{i+1} = P_{C \cap H_i}[x^i].

The hyperplane $\partial H_i$ separates $x^i$ from $S$ .

Formalization targets

Goal: Theorem 2.1

If $C$ is closed and convex, $F$ is continuous, $S \ne \emptyset$ and (1.2) holds, then every sequence generated by Algorithm 2.1 converges to a single point of $S$ :

\exists\, \hat x \in S:\quad x^i \to \hat x \quad (i \to \infty).

The theorem fixes no rate and no constant; it asserts convergence of the whole sequence, not only of a subsequence.

Milestones (in attack order)

Lemma 2.1 (p. 768): for nonempty closed convex $B$ , $\langle x - P_B[x], z - P_B[x]\rangle \le 0$ for $z \in B$ , and $\|P_B[x]-P_B[y]\|^2 \le \|x-y\|^2 - \|P_B[x]-x+y-P_B[y]\|^2$ .
Residual characterization (p. 767): $x \in S \iff r(x) = 0$ .
(2.5) (p. 769): $\langle F(x), r(x)\rangle \ge \|r(x)\|^2$ for $x \in C$ .
Linesearch well-definedness (p. 769): for $x \in C$ with $r(x) \ne 0$ , some $k$ satisfies (2.1).
Lemma 2.2 (p. 768): $x^{i+1} = P_{C\cap H_i}[\bar x^i]$ with $\bar x^i = P_{H_i}[x^i]$ .
(2.6) (pp. 769–770): $\|x^{i+1}-x^*\|^2 \le \|x^i-x^*\|^2 - \|x^{i+1}-\bar x^i\|^2 - \big(\eta_i\sigma/\|F(z^i)\|\big)^2\|r(x^i)\|^4$ for every $x^* \in S$ .
(2.8) (p. 770): $\eta_i\|r(x^i)\| \to 0$ .

Significance

Theorem 2.1 gives global convergence of a projection method for variational inequalities with no Lipschitz constant, no monotonicity and no knowledge of the problem beyond continuity and (1.2), at a fixed cost of two projections per iteration. Condition (1.2) covers pseudomonotone maps, which arise as gradients of pseudoconvex functions and in equilibrium models where monotonicity fails. The separating-hyperplane-and-project template of the proof is reused throughout the later literature on projection, proximal and hybrid methods for monotone inclusions.

The result has been proved since 1999. To the best of available knowledge no machine-checked proof of it, or of any convergence theorem for a projection method for variational inequalities, exists in Lean or Mathlib. This mission produces the statement and the supporting layer: a Euclidean projection onto closed convex sets with its standard inequalities, variational inequality solution sets, the projected residual, and a formal model of an Armijo-type linesearch algorithm with termination.

Difficulty

The Fejér-type inequality (2.6) quickly gives bounded iterates and $\eta_i\|r(x^i)\| \to 0$ . The obvious next step, concluding $r(x^i) \to 0$ , fails: nothing prevents the stepsizes $\eta_i$ from tending to zero, and in that regime the product going to zero says nothing about the residual. This regime is where the minimality of $k_i$ and the continuity of $F$ enter, and it is the step a naive formalization (for instance one that drops minimality, or fixes the stepsize) cannot reach. A second subtlety is that (1.2) is needed at an accumulation point that is only known to lie in $S$ at the end of the argument, which is why the condition must hold for every $x^* \in S$ . Finally, subsequential convergence must be upgraded to convergence of the whole sequence to one solution; convergence of a subsequence, or of the distance to $S$ , is strictly weaker.

Formalization scope

$\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) (not Fin n → ℝ, whose norm is the sup norm). The accumulation-point step needs finite dimension; no Hilbert-space generalization is intended.
Projection encoding. projOnto K x is a nearest point of $K$ to $x$ when one exists, chosen by Classical.choose, and the junk value $x$ otherwise. On nonempty closed convex sets it is exactly $P_K[x]$ ; the paper only projects onto such sets ( $C$ , $H_i$ , $C \cap H_i$ ), so the junk value is never reached under the hypotheses.
Stopping-rule encoding. A run is a sequence x : ℕ → ℝⁿ with Armijo indices k : ℕ → ℕ (predicate IsAlg21Run). If $r(x^i) = 0$ the method has stopped and the run stalls, $x^{i+1} = x^i$ ; otherwise $k_i$ is the least index satisfying (2.1) and $x^{i+1} = P_{C \cap H_i}[x^i]$ . A stalled point is a solution, so finitely terminating runs are included in the goal.
Parameters $\gamma, \sigma$ are real with $0 < \gamma < 1$ , $0 < \sigma < 1$ , universally quantified; $n$ , $C$ , $F$ and $x^0 \in C$ are arbitrary.
(2.6) is stated for one generic step ( $x \in C$ , $r(x)\ne 0$ , $k$ satisfying (2.1)) rather than along a run; it is the same inequality with $x^i, k_i$ abstracted.
Trivializing formalizations are ruled out: condition (1.2) is quantified over every solution and every $x \in C$ (not replaced by monotonicity or an existential), $k_i$ is the least index satisfying (2.1), the update projects $x^i$ onto $C \cap H_i$ (not onto $C$ alone), the stopped case is pinned down by the stall encoding, and the conclusion is convergence of the whole sequence to one solution, not $r(x^i) \to 0$ or $\operatorname{dist}(x^i, S) \to 0$ .
Needed infrastructure: existence, uniqueness and variational characterization of the projection (Mathlib has exists_norm_eq_iInf_of_complete_convex and norm_eq_iInf_iff_real_inner_le_zero), firm nonexpansiveness, the explicit projection onto a halfspace, and a bounded-sequence subsequence argument in $\mathbb{R}^n$ . The projection lemmas are reusable for any projection-type method; contributions proving them as standalone lemmas are welcome.

Selected references

M. V. Solodov and B. F. Svaiter, A New Projection Method for Variational Inequality Problems, SIAM J. Control Optim. 37(3), 765–776, 1999. https://doi.org/10.1137/S0363012997317475
G. M. Korpelevich, The extragradient method for finding saddle points and other problems, Matecon 12, 747–756, 1976.
A. N. Iusem and B. F. Svaiter, A variant of Korpelevich's method for variational inequalities with a new search strategy, Optimization 42, 309–321, 1997. https://doi.org/10.1080/02331939708844365
P. T. Harker and J.-S. Pang, Finite-dimensional variational inequality and nonlinear complementarity problems: a survey of theory, algorithms and applications, Math. Programming 48, 161–220, 1990. https://doi.org/10.1007/BF01582255
F. Facchinei and J.-S. Pang, Finite-Dimensional Variational Inequalities and Complementarity Problems, Springer, 2003. https://doi.org/10.1007/b97543

16 thms2 active usersReviewed

Completed

Functional Analysis Operations Research Optimization·Captain: mikedeng1

Accelerated Proximal Point Method for Maximally Monotone Operators: The Fixed-Point Residual Rate of the Accelerated MethodResearch Paper

Motivation

Many problems in optimization reduce to finding a zero of a maximally monotone operator: minimizing a closed proper convex function (its subdifferential is maximally monotone), finding a saddle point of a convex–concave function, and solving monotone variational inequalities. The basic algorithm for this problem is the proximal point method of Martinet (1970) and Rockafellar (1976), which repeatedly applies the resolvent of the operator. The augmented Lagrangian method, the proximal method of multipliers, the Douglas–Rachford splitting method, ADMM and the primal–dual hybrid gradient method are all instances of it, so any speed-up of the proximal point method transfers to these widely used algorithms.

For convex minimization, Güler (1992) accelerated the proximal point method in the style of Nesterov, improving the rate of the function value from $O(1/i)$ to $O(1/i^2)$ . For general maximally monotone operators no function value exists, and the natural measure of progress is the fixed-point residual $\|x_{i}-y_{i-1}\|$ , the distance moved by one resolvent step. Gu and Yang (2020) showed that the plain proximal point method has the exact worst-case rate $O(1/i)$ for the squared residual. Relaxed and inertial variants had been studied, but none guaranteed an accelerated rate for this measure. Kim (arXiv:1905.05149, Math. Program. 2021) found one using the performance estimation problem (PEP) of Drori and Teboulle (2014): a new accelerated proximal point method whose squared fixed-point residual is at most $R^2/i^2$ .

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ . A set-valued operator $M:\mathcal H\to2^{\mathcal H}$ assigns a subset $Mx\subseteq\mathcal H$ to every point $x$ . It is monotone if $\langle x-y,u-v\rangle\ge0$ whenever $u\in Mx$ and $v\in My$ , and maximally monotone if moreover no monotone operator has a graph that properly contains the graph of $M$ . The class of maximally monotone operators is $\mathcal M(\mathcal H)$ , and $X_*(M)=\{x:0\in Mx\}$ is the set of zeros.

For a step size $\lambda>0$ , the resolvent $J_{\lambda M}=(I+\lambda M)^{-1}$ maps $y$ to the unique $x$ with $y\in x+\lambda Mx$ . It is single-valued for monotone $M$ and defined on all of $\mathcal H$ for maximally monotone $M$ .

The general proximal point method with step coefficients $h=\{h_{i,k}\}$ starts at $y_0$ and iterates

x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=y_i+\sum_{k=0}^{i}h_{i+1,k+1}(x_{k+1}-y_k).

Kim's proposed accelerated proximal point method starts at $x_0=y_0=y_{-1}$ and iterates

x_{i+1}=J_{\lambda M}(y_i),\qquad y_{i+1}=x_{i+1}+\frac{i}{i+2}(x_{i+1}-x_i)-\frac{i}{i+2}(x_i-y_{i-1}).

The coefficients (25) are $h_{i,k}=-\frac{2k}{i(i+1)}$ for $k<i$ and $h_{i,i}=\frac{2i}{i+1}$ .

The PEP of Section 3 bounds the worst case of $\|x_N-y_{N-1}\|^2/R^2$ over all $M\in\mathcal M(\mathcal H)$ and all starts with $\|y_0-x_*\|\le R$ . A semidefinite relaxation leads to the dual problem (D): minimize $c$ over nonnegative $a_2,\dots,a_N,b_N,c$ such that $\sum_{i=2}^Na_iA_{i-1,i}(h)+b_NB_N(h)+cC-u_Nu_N^\top\succeq0$ . The matrices are explicit symmetric $(N+1)\times(N+1)$ matrices built from $h$ and the canonical basis $u_1,\dots,u_{N+1}$ . Its optimal value is $\mathcal B_D(h)$ .

Formalization targets

Goal: Theorem 4.1

For every $M\in\mathcal M(\mathcal H)$ , every $\lambda>0$ , every run of the proposed method, and every $x_*\in X_*(M)$ with $\|x_0-x_*\|\le R$ for a constant $R>0$ ,

\|x_i-y_{i-1}\|^2\le\frac{R^2}{i^2}\qquad\text{for every }i\ge1.

The constant is the paper's, and nothing is left unfixed.

Milestones

Lemma 4.1. For every $N\ge1$ , $h$ from (25) with $a_i=\frac{2(i-1)i}{N^2}$ , $b_N=\frac2N$ , $c=\frac1{N^2}$ is feasible for (D) and for (HD) $=\min_h\mathcal B_D(h)$ .
Section 3, (D). For any $h$ and any feasible point of (D), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le c$ for every run of the general method with $\|y_0-x_*\|\le R$ .
Eq. (28). With $h$ from (25), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le\mathcal B_D(h)\le\frac1{N^2}$ for every $N\ge1$ .
Proposition 4.1. The general method with (25) and the proposed method generate identical sequences from the same initial point.

Significance

Theorem 4.1 gives the first $O(1/i^2)$ rate for the fixed-point residual of a proximal point method on general maximally monotone operators. The rate uses no strong monotonicity, no smoothness, and no finite dimension. Because the proximal point method underlies the proximal method of multipliers, PDHG, Douglas–Rachford splitting and ADMM, the paper derives accelerated versions of each (Section 6). The same analysis also accelerates the forward method for cocoercive operators (Section 7). Later work related the method to the Halpern iteration (Lieder 2021) and showed that its rate is optimal among a broad class of fixed-point methods up to a constant (Park and Ryu 2022).

The result is proved in the paper, and to our knowledge no machine-checked proof exists. Formalizing it produces a verified chain of four results: an explicit semidefinite certificate (Lemma 4.1), the weak-duality step from an SDP certificate to an algorithmic bound, the resulting rate for the general method, and the algebraic identity between two recursions (Proposition 4.1). It also produces reusable definitions of monotone and maximally monotone set-valued operators on a real Hilbert space, which Mathlib does not have.

Difficulty

The obvious approach would be a Lyapunov (potential) function argument, but the paper does not give one. The rate comes out of a semidefinite program. Lemma 4.1 asks for positive semidefiniteness of an $(N+1)\times(N+1)$ matrix whose entries are double sums over $h$ , uniformly in $N$ . The passage from the dual certificate back to the iterates happens in an arbitrary, possibly infinite-dimensional Hilbert space, where each constraint matrix corresponds to a monotonicity inequality between iterates, so matrix positivity has to be turned into an inequality between inner products in $\mathcal H$ . The PEP is a relaxation that discards constraints, so only weak duality is available, and a rate that holds only for $\dim\mathcal H\ge N+1$ (Lemma 3.1) is not what is asked. Proposition 4.1 is a two-level induction with index bookkeeping at $i=0,1$ .

Formalization scope

$\mathcal H$ is any real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), with no finite-dimensional specialization. An operator is M : H → Set H. Maximal monotonicity says that every monotone A with M x ⊆ A x for all x equals M.

The resolvent step is relational: $x_{i+1}=J_{\lambda M}(y_i)$ is encoded as $\lambda^{-1}(y_i-x_{i+1})\in Mx_{i+1}$ . For monotone $M$ and $\lambda>0$ this determines $x_{i+1}$ uniquely, and for maximally monotone $M$ such an $x_{i+1}$ exists for every $y_i$ (Minty's theorem). No function-valued resolvent with junk values off its domain is used. Sequences are indexed by ℕ. The paper's $y_{-1}=y_0$ is y (0 - 1) = y 0 under natural-number subtraction. The general method has no $x_0$ , so its initial-distance condition is on $y_0$ , as in (17). The step size $\lambda$ is written lam.

PEP matrices are Matrix (Fin (N+1)) (Fin (N+1)) ℝ, with a 1-based basis basisVec N i $=u_i$ . $\mathcal B_D(h)$ is the infimum of the feasible values of $c$ computed in EReal, so an infeasible $h$ gets the value $+\infty$ as in the paper; Eq. (28) compares it with the real bounds cast to EReal.

A formalization in which the iterate predicate cannot be satisfied, the residual is $\|x_i-x_{i-1}\|$ , the correction term is dropped or has the wrong sign, the initial point is decoupled ( $x_0\ne y_0$ ), or $M$ is only monotone on finitely many points, would state a different theorem, and none is used here.

Useful infrastructure includes a Minty-type existence lemma, uniqueness of the resolvent, and a lemma turning a positive semidefinite certificate into an inequality between inner products in $\mathcal H$ (via Matrix.PosSemidef and Gram matrices). These are reusable for PEP-based rates of other first-order methods. Proofs of any milestone, and of the goal by other routes, are welcome.

Selected references

D. Kim, Accelerated proximal point method for maximally monotone operators, Math. Program. 190 (2021) 57–87; arXiv:1905.05149v4. https://arxiv.org/abs/1905.05149
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, New proximal point algorithms for convex minimization, SIAM J. Optim. 2 (1992) 649–664. https://doi.org/10.1137/0802032
Y. Drori, M. Teboulle, Performance of first-order methods for smooth convex minimization: a novel approach, Math. Program. 145 (2014) 451–482. https://doi.org/10.1007/s10107-013-0653-0
G. Gu, J. Yang, Tight sublinear convergence rate of the proximal point algorithm for maximal monotone inclusion problems, SIAM J. Optim. 30 (2020) 1905–1921. https://doi.org/10.1137/19M1299049
F. Lieder, On the convergence rate of the Halpern-iteration, Optim. Lett. 15 (2021) 405–418. https://doi.org/10.1007/s11590-020-01617-9
J. Park, E. K. Ryu, Exact optimal accelerated complexity for fixed-point iterations, ICML 2022; arXiv:2201.11413. https://arxiv.org/abs/2201.11413
H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5

10 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

On the Global Convergence of Stochastic Fictitious Play I: Every Additive Random Utility Choice Function Has an Admissible Deterministic Perturbation RepresentationResearch Paper

Motivation

Models of learning in games, and discrete choice models in econometrics, describe an agent who does not always pick the best alternative. Two descriptions of such an agent are standard. In the additive random utility model (McFadden 1981; Anderson, de Palma and Thisse 1992) the agent maximizes payoffs perturbed by random shocks. In the deterministic perturbation model (Fudenberg and Levine 1998) the agent chooses a probability vector and pays a deterministic, strictly convex cost for it. The logit choice rule arises from both: from i.i.d. extreme-value shocks, and from the entropy cost $V(y) = \eta \sum_j y_j \ln y_j$ .

Hofbauer and Sandholm (Econometrica 70 (2002)) show that the second description is general enough to cover the first for every shock distribution with a strictly positive density, not only for logit. Their analysis of stochastic fictitious play rests on this: the deterministic representation provides the perturbed payoff functions from which Lyapunov functions for the learning dynamics are built, for arbitrary noise. This mission formalizes that discrete choice theorem, Theorem 2.1 of the paper, together with the steps of its proof.

Setting

Fix $n \ge 1$ alternatives $A = \{1, \dots, n\}$ with base payoffs $\pi = (\pi_1, \dots, \pi_n) \in \mathbb{R}^n$ . A random vector $\varepsilon = (\varepsilon_1, \dots, \varepsilon_n)$ has a strictly positive density $f : \mathbb{R}^n \to \mathbb{R}$ , whose law does not depend on $\pi$ . The agent chooses the alternative whose total payoff $\pi_j + \varepsilon_j$ is largest, which gives the choice probability function $C : \mathbb{R}^n \to \mathbb{R}^n$ ,

C_i(\pi) = P\big(\operatorname{argmax}_j\, \pi_j + \varepsilon_j = i\big).

The probability simplex is $\Delta A = \{x \in \mathbb{R}^n_+ : \sum_j x_j = 1\}$ , with relative interior $\operatorname{int}(\Delta A)$ (all coordinates positive) and tangent space $\mathbb{R}^n_0 = \{z \in \mathbb{R}^n : \sum_j z_j = 0\}$ .

A deterministic perturbation is a function $V : \operatorname{int}(\Delta A) \to \mathbb{R}$ . Because $V$ lives on the relative interior, its gradient $\nabla V(y)$ is the vector of $\mathbb{R}^n_0$ with $V(y + hz) = V(y) + (\nabla V(y) \cdot z) h + o(h)$ for all $z \in \mathbb{R}^n_0$ , and its second derivative $D^2 V(y)$ is a quadratic form on $\mathbb{R}^n_0$ . The perturbation is admissible if $V$ is twice continuously differentiable along the simplex, $D^2V(y)$ is positive definite on $\mathbb{R}^n_0$ for every $y$ , and $\|\nabla V(y)\| \to \infty$ as $y$ approaches the boundary of $\Delta A$ .

Formalization targets

Goal: Theorem 2.1

If $\varepsilon$ has a strictly positive density and $C$ is continuously differentiable, then there is an admissible $V$ such that, for every $\pi \in \mathbb{R}^n$ ,

C(\pi) = \operatorname*{argmax}_{y \in \operatorname{int}(\Delta A)} \big( y \cdot \pi - V(y) \big),

with a unique maximizer. The perturbation $V$ is one function serving all payoff vectors at once.

Milestones

The milestones are the steps of the paper's proof (pp. 5–7), in order:

Eq. (4). $DC(\pi)$ is symmetric, $\partial C_i/\partial \pi_j = \partial C_j / \partial \pi_i$ , and its off-diagonal terms are strictly negative.
Eq. (5). $\partial C_i/\partial \pi_i = -\sum_{j \ne i} \partial C_j/\partial \pi_i$ , and $DC(\pi)\mathbf{1} = 0$ .
Eq. (6). $z \cdot DC(\pi) z > 0$ whenever $z$ is not proportional to $\mathbf{1}$ .
Shift invariance and injectivity. $C(\pi + c\mathbf{1}) = C(\pi)$ , and $C$ is one-to-one on $\mathbb{R}^n_0$ .
Range observation. If the payoffs $\pi_j$ , $j \in J$ , stay bounded while the others tend to $+\infty$ , then $C_j(\pi) \to 0$ for $j \in J$ .
Convex potential. There is $W : \mathbb{R}^n \to \mathbb{R}$ with $\nabla W \equiv C$ , strictly convex on $\mathbb{R}^n_0$ .
Range. $C$ takes values in $\operatorname{int}(\Delta A)$ , and $C(\mathbb{R}^n_0) = \operatorname{int}(\Delta A)$ .

Significance

The result. Theorem 2.1 lets any smooth additive random utility model be replaced by an optimizing agent with a strictly convex, boundary-repelling cost. In the paper this is the bridge from the perturbed best response dynamic to a deterministic perturbed-payoff formulation, which yields Lyapunov functions for zero-sum games, games with an interior evolutionarily stable strategy, and potential games (§4 of the paper), and so the almost sure convergence of stochastic fictitious play under general noise (Theorem 6.1). Without it those convergence results would be restricted to noise distributions whose choice rule has a known deterministic representation, essentially logit. The paper also shows (Proposition 2.2) that the converse fails when $n \ge 4$ : deterministic perturbations generate strictly more choice rules than random utility.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it is known. The mission asks for a formal proof of Theorem 2.1 and the seven steps above. Along the way it requires symmetric Jacobians of probability integrals, a gradient-field potential on $\mathbb{R}^n$ , and the Legendre transform of a strictly convex function restricted to a hyperplane. None of these is currently packaged in Mathlib in the needed form.

Difficulty

The obvious argument is to take $V$ to be the Legendre transform of the potential $W(\pi) = \mathbb{E}\max_j(\pi_j + \varepsilon_j)$ and read off the first-order conditions. Three steps of that argument are not routine. First, the derivative identity (4) is a change of variables inside an $(n-1)$ -fold integral over a moving region, and its strict sign needs the density to be positive on the relevant hyperplane sections. Second, the Legendre transform is well defined on all of $\operatorname{int}(\Delta A)$ only if $C$ maps $\mathbb{R}^n_0$ onto the whole open simplex. The paper takes this from Theorem 26.5 of Rockafellar (1970), whose hypotheses (essential smoothness, strict convexity, identification of the conjugate's domain) must be checked here. Third, positive definiteness of $D^2V$ and the gradient blow-up at the boundary are statements about the inverse of $C$ on $\mathbb{R}^n_0$ . They need an inverse function argument on a subspace and a properness argument, not only pointwise convexity.

Verifying that $C(\pi)$ satisfies the first-order condition for one fixed $\pi$ does not suffice: the goal requires a single $V$ for all $\pi$ , and a unique maximizer.

Formalization scope

Alternatives are indexed by Fin n with $n \ge 1$ ; vectors are Fin n → ℝ with its sup norm. The density is a real function $f$ that is continuous, strictly positive at every point, and has $\int f = 1$ ; the law of $\varepsilon$ is Lebesgue measure weighted by $f$ . The paper's formula (4) evaluates $f$ on hyperplanes, which is meaningful for a continuous $f$ . Without continuity the theorem can fail: a density that is positive everywhere but tends to zero near a hyperplane can make $C$ continuously differentiable with a vanishing off-diagonal derivative, and then no twice differentiable $V$ represents $C$ . Continuous differentiability of $C$ is a hypothesis, as in the paper, stated as ContDiff ℝ 1 of the map $\pi \mapsto C(\pi)$ . The event " $i$ is the argmax" uses strict inequalities; ties have probability zero.

$V$ is a function on $\mathbb{R}^n$ of which only the values on $\operatorname{int}(\Delta A)$ enter. Its smoothness and second derivative are taken in the chart $z \mapsto V(y + z)$ on the subspace $\mathbb{R}^n_0$ . $\nabla V(y)$ is the tangent gradient of the paper's footnote 3, not an ambient gradient of an extension. The boundary blow-up is stated uniformly: for every $M$ there is $\delta > 0$ such that every tangent gradient at an interior point with some coordinate below $\delta$ has norm above $M$ .

The goal cannot be satisfied trivially. $V$ must be chosen before $\pi$ , all three admissibility conditions are part of the definition, and the maximizer must be unique. Weakening any of these (a $V$ depending on $\pi$ , a $V$ without second derivatives, a non-strict maximum) changes the theorem.

Reusable infrastructure: differentiation of choice probabilities under a density, potentials of symmetric $C^1$ vector fields on $\mathbb{R}^n$ , and Legendre duality for strictly convex functions on a subspace. Contributions of any of these as separate lemmas are welcome, as are alternative proofs of the milestones, for instance obtaining the potential directly as $\mathbb{E}\max_j(\pi_j + \varepsilon_j)$ .

Selected references

J. Hofbauer and W. H. Sandholm, On the Global Convergence of Stochastic Fictitious Play, Econometrica 70(6), 2265–2294, 2002. https://doi.org/10.1111/1468-0262.00376 (theorem numbers and pages here follow the authors' manuscript of February 21, 2002).
D. Fudenberg and D. K. Levine, The Theory of Learning in Games, MIT Press, 1998.
S. P. Anderson, A. de Palma and J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.
D. McFadden, Econometric Models of Probabilistic Choice, in C. F. Manski and D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981.
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

11 thms2 active usersReviewed

Completed

Graph Theory Operations Research Optimization·Captain: mikedeng1

The Traveling-Salesman Problem and Minimum Spanning Trees, Part II: Convergence of the Constant-Step Ascent to the 1-Tree BoundResearch Paper

Motivation

The traveling-salesman problem (TSP) asks for a cheapest cycle through all vertices of a weighted complete graph. Exact algorithms for it are branch-and-bound searches, and their size depends almost entirely on the quality of the lower bounds used to prune the search. In 1970 Held and Karp introduced the 1-tree bound: a Lagrangian relaxation of the degree-2 constraints of a tour, whose value can be evaluated by one minimum-spanning-tree computation (Held & Karp, Part I, 1970). Part II (Held & Karp, 1971) replaces the ascent procedure of Part I by an iterative method related to the relaxation method for linear inequalities of Agmon and of Motzkin and Schoenberg (1954), and with it solved to proven optimality every instance presented to it, up to 64 cities. The iteration is the prototype of what is now called the subgradient method with Polyak-type step sizes, and the 1-tree bound remains a standard lower bound in exact TSP codes.

Timeline:

1954 — Agmon; Motzkin and Schoenberg: the relaxation method for systems of linear inequalities, and convergence of Féjer-monotone sequences relative to full-dimensional sets.
1970 — Held and Karp (Part I): the 1-tree bound $\max_\pi w(\pi)$ and a column-generation / ascent method for it.
1971 — Held and Karp (Part II): the iteration $\pi^{m+1} = \pi^m + t_m v_{k(\pi^m)}$ , its relaxation-method analysis (Lemmas 1–3) and the constant-step guarantee (Theorem 1).
1974 — Held, Wolfe and Crowder validate the method as general subgradient optimization.

Setting

Let $n \ge 3$ and let $(c_{ij})$ be a symmetric real $n\times n$ matrix of weights on the edges of the complete graph $K_n$ with vertex set $\{1,\dots,n\}$ ; weights may be negative and need not satisfy the triangle inequality. A subgraph has weight equal to the sum of its edge weights. A tour is a cycle through every vertex exactly once; $C^*$ is the weight of a minimum tour.

A 1-tree is a tree on the vertex set $\{2,\dots,n\}$ together with two distinct edges at vertex $1$ . Index the 1-trees by $k$ ; let $c_k$ be the weight of the $k$ -th 1-tree, $d_{ik}$ the degree of vertex $i$ in it, and $v_k \in \mathbb R^n$ the degree-excess vector with components $d_{ik}-2$ . For $\pi \in \mathbb R^n$ define

w(\pi) = \min_k\,[c_k + \pi\cdot v_k].

A tour is a 1-tree with $v_k = 0$ , so $C^* \ge w(\pi)$ for every $\pi$ (Eq. (2)); the best bound is $\max_\pi w(\pi)$ . For a point $\pi$ , $k(\pi)$ denotes a minimum-weight 1-tree at $\pi$ , a 1-tree attaining the minimum defining $w(\pi)$ . The ascent iteration (3) is

\pi^{m+1} = \pi^m + t_m\,v_{k(\pi^m)}.

For a target value $\bar w$ , $P_{\bar w}$ is the polyhedron of solutions of $\bar w \le c_k + \pi\cdot v_k$ for all $k$ (system (5)). All norms $\|\cdot\|$ are Euclidean.

Formalization targets

Goal: Theorem 1

With constant step $t_m = \bar t > 0$ , any starting point and any choice of minimum-weight 1-trees,

\sup_m w(\pi^m) \;\ge\; \max_\pi w(\pi) - \tfrac12\,\bar t\,\limsup_{m\to\infty}\|v_{k(\pi^m)}\|^2 .

Milestones

Eq. (2): $C^* \ge w(\pi)$ for every $\pi$ .
Lemma 1: if $w(\bar\pi) \ge w(\pi)$ then $(\bar\pi-\pi)\cdot v_{k(\pi)} \ge w(\bar\pi) - w(\pi) \ge 0$ .
Lemma 2: if $0 < t < 2(w(\bar\pi)-w(\pi))/\|v_{k(\pi)}\|^2$ then $\|\bar\pi - (\pi + t v_{k(\pi)})\| < \|\bar\pi-\pi\|$ .
Féjer-monotone convergence (Motzkin–Schoenberg, quoted in the proof of Lemma 3): a sequence whose distance to every point of a set with nonempty interior is nonincreasing converges.
Lemma 3, Case 1: for $\bar w < \max_\pi w$ and the relaxation iteration

\pi^{m+1} = \pi^m + \lambda_m\,\frac{\bar w - w(\pi^m)}{\|v_{k(\pi^m)}\|^2}\,v_{k(\pi^m)} \qquad (6)

with $0<\varepsilon<\lambda_m\le 2$ , the iterates enter $P_{\bar w}$ or converge to a boundary point of $P_{\bar w}$ . 6. Lemma 3, Case 2: with $\lambda_m = 2$ the iterates enter $P_{\bar w}$ . 7. §3 bound: the restricted minimum $w_{X,Y}(\pi)$ over 1-trees containing the edges $X$ and avoiding the edges $Y$ is a lower bound on every tour of the derived problem.

Milestones 1–5 are the steps of the paper's proof of Theorem 1; 6 and 7 are further results of the paper on the same objects.

Significance

Theorem 1 is the paper's justification of the step rule actually used in its computations: a fixed step $\bar t$ loses at most $\tfrac12\bar t$ times the asymptotic squared deviation of the generated 1-trees from being tours. Since $\|v_k\|^2$ is an even integer that vanishes exactly on tours, and the paper observes it is typically small in practice, the bound explains why the constant-step ascent reaches bounds sharp enough for branch-and-bound. Lemmas 1–3 are the first analysis of a subgradient-type method for a nonsmooth concave function, cast as the relaxation method for the (exponentially large) system (5).

All results are proved in the paper (except the Féjer-monotone convergence and Case 2 of Lemma 3, which it cites from Motzkin and Schoenberg). None is formalized: the platform has the 1-tree lower bound only under a metric assumption on the weights (SupplyChainTheory.held_karp_bound, SupplyChainTheory.one_tree_lower_bound), and the subtour-LP bound MetricTSP.held_karp_le_opt, a different object. This mission produces the bound for arbitrary real weights, the supergradient property of $v_{k(\pi)}$ , and a machine-checked convergence analysis of the relaxation iteration.

Difficulty

Lemmas 1 and 2 and Eq. (2) are short once the finite minimum defining $w$ is handled. The difficulty is in Lemma 3 and Theorem 1. The iteration is not monotone in $w$ , so no descent argument applies; progress is measured by the Euclidean distance to the target polyhedron $P_{\bar w}$ , and turning distance decrease into convergence requires the Féjer-monotonicity theorem, which in turn needs $P_{\bar w}$ to have nonempty interior (from $\bar w < \max_\pi w$ ). In Theorem 1 the step is constant rather than of the relaxation form (6), and the target polyhedron is not given in advance: the relevant relaxation parameters are admissible only eventually and must be kept away from zero, which requires controlling degenerate directions $v_{k(\pi^m)} = 0$ and the behaviour of $w$ along an iteration that is not known a priori to stay bounded. A direct argument that $w(\pi^m)$ increases fails, since single steps can decrease $w$ .

Formalization scope

Vertices are Fin n, the paper's vertex 1 is 0 : Fin n, and graphs are SimpleGraph (Fin n). Weights are c : Sym2 (Fin n) → ℝ, arbitrary reals. A 1-tree is a graph whose restriction to the vertices other than 0 is a tree and in which 0 has degree 2; a tour is a connected graph with all degrees 2. w(π) is the minimum of weight c G + ∑ i, π i * (deg G i − 2) over 1-trees, written as an sInf over a finite set that is nonempty for n ≥ 3; every theorem assumes 3 ≤ n. Euclidean norms and inner products are written as coordinate sums of squares and products, never Mathlib's sup norm on Fin n → ℝ. The minimum-weight 1-tree $k(\pi^m)$ is a hypothesis at every step, and ties may be broken arbitrarily. The goal is stated as "for every $\pi^*$ and $\delta>0$ some iterate has $w(\pi^m) > w(\pi^*) - \tfrac12\bar t L - \delta$ ", which is equivalent to the printed inequality; $L$ is the limsup of a sequence with finitely many values, a genuine real.

The statements exclude trivializing readings: the 1-tree predicate rejects graphs without exactly two edges at vertex 1; w is never a minimum over an empty set under the standing hypothesis 3 ≤ n; no ⨆ of a possibly unbounded family is used; the step size $\bar t$ and the parameter $\varepsilon$ are strictly positive.

A complete development needs finite minima of affine functions (concavity, attainment), 1-tree and tour combinatorics on simple graphs, and Féjer-monotone sequences in $\mathbb R^n$ ; the last two are reusable beyond this mission. Proofs of any milestone, and alternative arguments for Lemma 3, are welcome.

Selected references

M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
M. Held and R. M. Karp, The traveling-salesman problem and minimum spanning trees, Operations Research 18 (1970) 1138–1162. https://doi.org/10.1287/opre.18.6.1138
T. S. Motzkin and 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
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 382–392. https://doi.org/10.4153/CJM-1954-037-2
M. Held, P. Wolfe and H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223

10 thms2 active usersReviewed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis XXXV: Gross Substitutes and Equilibrium PricesTextbook

Motivation

This mission continues chapter 11's account of the M♮-concave/M♮-convex exchange-economy model begun in mission 14-economic-equilibrium, placing seven of that chunk's own results that were previously left out-of-cone: the two gross-substitutes-style characterizations of M♮-concavity (§11.3), the transfer theorem that lifts an equilibrium of the continuous relaxation to one for indivisible commodities (§11.4), and the explicit polyhedral description of the equilibrium price set together with its feasibility criterion (§11.5).

Setting

Mission 14-economic-equilibrium built the exchange-economy vocabulary this mission redeclares in full (UDom, ArgMaxBot/ArgMinTop, PriceShift/PriceShiftConvex, DemandSet/SupplySet, IsEquilibrium, MNaturalConcave, IsMNaturalConvexSet, the concave/convex closures ConcaveClosureR/ConvexClosureR and their continuous analogues ContDemandSet/ContSupplySet/ IsContEquilibrium) and placed the qualitative structural theorems (Theorems 11.1-11.3, 11.4, 11.16-11.18, 11.23-11.24). This mission adds the gross-substitutes axioms (−M♮-GS[Z], the price-monotonicity property NegGS, and −M♮-SWGS[Z], its one-price-at-a-time refinement NegSWGS), the M♮-convex-set transfer machinery connecting a continuous equilibrium to a discrete one, and the equilibrium price polyhedron built from the three bound families ℓ(j), u(j), u(i,j) (Eqs. (11.40)-(11.42)) that make Theorem 11.16's qualitative L♮-convex-polyhedron fact concrete and linear-programming-checkable.

Formalization targets

Goal: The equilibrium price set is the explicit L♮-convex polyhedron (11.43) (Theorem 11.21)

For a fixed allocation (x,y), the set P* of all equilibrium price vectors is an L♮-convex polyhedron and equals the polyhedron cut out by max{0,ℓ(j)} ≤ p(j) ≤ u(j) and p(j)-p(i) ≤ u(i,j). Chosen as goal: it is the sharpest structural result of chapter 11's computation section, upgrading Theorem 11.16's qualitative fact to a concrete description, and is what Theorem 11.22 (also placed) builds on directly.

Supporting structural targets

Theorem 11.5 and Theorem 11.6 characterize M♮-concavity via the gross-substitutes and stepwise gross-substitutes properties, completing chapter 11's suite of M♮-concavity characterizations begun with Theorem 11.4 (mission 14). Theorem 11.15 is the general transfer theorem (continuous equilibrium ⟹ discrete equilibrium) that mission 14's own Theorem 11.14 invokes as a special case. Theorem 11.22 gives the feasibility criterion for the existence of an equilibrium price vector, the mission's second theorem built on the equilibrium price polyhedron.

Significance

Together with mission 14-economic-equilibrium, this mission completes the book's account of how M♮-concavity/convexity — a purely combinatorial exchange condition — reproduces, and sharpens, the classical gross-substitutes theory of competitive equilibrium for economies with indivisible goods: existence transfers from the continuous relaxation, and the equilibrium price set itself has a description exact enough to reduce to a linear feasibility question. None of these results are open — they are Murota's own account (attributed in the book's own notes to Danilov-Koshevoy- Lang and Murota-Tamura for the gross-substitutes theorems, and to Murota-Tamura for the equilibrium price polyhedron); this mission contributes a faithful, machine-checked formal statement of each (see Formalization scope).

Difficulty

Two of this chunk's seven BRIEF.md results are not drafted this pass, for a disclosed time- budget reason rather than any faithfulness failure: Proposition 11.19 and Theorem 11.20 require the H,L-indexed bipartite MSFP2 flow-network vocabulary (separate vertex sets V+_e, V+_l, V-_h, an M-convex/M-concave-combining flow objective) that neither this mission nor mission 14 builds, and building it in proportion to placing exactly these two results was judged disproportionate to the remaining time in this pass; see HARD.md and STATUS.md. This is explicitly not a hard exclusion — both results are well-posed and provable from the book's own complete proofs — and is recorded as an honest scope limitation for a future pass. Theorem 11.22's own trailing algorithmic remark (that equilibrium prices can be found via a shortest-path computation, yielding a polynomial-time equilibrium-checking algorithm) is a computational/ complexity claim outside this series' propositional-formalization methodology and is omitted; the mathematical "iff feasibility" content is placed in full. See HARD.md.

Formalization scope

Ground set K is a Fintype with DecidableEq; consumer/producer index sets H, L are Fintypes (Nonempty where the price-bound formulas (11.40)-(11.42) need a nonempty sup'/inf' range). All base vocabulary is redeclared fresh from mission 14-economic-equilibrium's own definitions, since this draft cannot import that sibling mission. The gross-substitutes axioms are formalized directly from their defining inequalities (Eqs. preceding (11.19) and following, and p.331); the equilibrium price polyhedron's bound families ℓ(j)/u(j)/u(i,j) are formalized literally from Eqs. (11.40)-(11.42), extracting each WithBot ℝ/WithTop ℝ operand to ℝ before subtracting (since WithBot ℝ carries no subtraction instance). Two results (Proposition 11.19, Theorem 11.20) are not drafted this pass for the disclosed time-budget reason above; one result (Theorem 11.22's trailing algorithmic remark) is scoped out as computational content. Contributions completing any of the five sorrys, or building the MSFP2 vocabulary to place Proposition 11.19/Theorem 11.20 in a follow-up mission, are welcome.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
V. Danilov, G. Koshevoy, K. Murota, "Discrete convexity and equilibria in economies with indivisible goods and money," Mathematical Social Sciences, 41 (2001), pp. 251-273 [33] (origin of the gross-substitutes characterization, Theorem 11.6).
K. Murota, A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [160] (origin of the equilibrium price polyhedron, Theorems 11.20-11.22).

41 thms2 active usersReviewed

Completed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis XXXIII: Near-Optimality for Submodular MinimizationTextbook

Motivation

Chapter 10 turns from structure theory to algorithms: efficient methods for minimizing M-convex functions (via domain reduction) and submodular set functions (via Schrijver's and the Iwata-Fleischer-Fujishige scaling algorithms). Most of chapter 10's numbered results are asymptotic running-time bounds for specific procedural algorithms — a genuinely different kind of claim from the rest of this book (see Formalization scope). This mission places the results of this block that ARE ordinary mathematical propositions: correctness certificates, min-max theorems, and structural facts the algorithms rely on and produce.

Setting

For an M-convex set B ⊆ Z^V, the central part B° (the vectors of B lying away from its boundary, defined via per-coordinate bounds ℓ°_B, u°_B) is what the domain reduction algorithm searches from. For a submodular set function ρ : 2^V → R, the base polyhedron B(ρ) and its extreme bases (one per linear ordering of V, via Eq. (10.12)) let any base be written as a convex combination of finitely many extreme bases (Eq. (10.13)); a candidate minimizer W is certified via the linear orderings representing an optimal base. The Iwata-Fleischer-Fujishige (IFF) scaling algorithm relaxes this problem with a flow-augmentation parameter δ, maintaining a δ-feasible flow φ and vector z = x + ∂φ; near the end of a scaling phase, no augmenting path and no "active triple" together certify near-optimality.

Formalization targets

Goal: Near-optimality from the absence of augmenting paths (Proposition 10.20)

If S ⊆ W ⊆ V∖T, no arc of the auxiliary network leaves W, and no active triple exists, then z⁻(V) ≥ ρ(W)-nδ and x⁻(V) ≥ ρ(W)-n²δ; moreover W exactly minimizes ρ once δ is small enough relative to the smallest positive gap between two values of ρ. Chosen as goal: the book calls this "a key property of the scaling algorithm" and "a relaxation version of the min-max relation in Proposition 10.8", its own proof is the most substantial argument among this chunk's placed results, and Proposition 10.23 is a direct corollary of it.

Supporting structural targets

Proposition 10.8 is the min-max relation underlying the whole of section 10.2 (an Edmonds- intersection-theorem consequence, found by direct reading — the extractor's table missed it). Proposition 10.9 gives the three-part sufficient condition for optimality, in terms of the linear orderings representing an optimal base, that both Schrijver's algorithm and the IFF algorithm use as their termination criterion (also found by direct reading). Propositions 10.5-10.6 establish that the domain reduction algorithm's central part B° is always nonempty, via an explicit vector-extension step (Proposition 10.5 likewise missing from the extractor's table). Proposition 10.23 fixes individual coordinates once a scaling phase ends, and Proposition 10.24 gives the termination certificate for the IFF fixing algorithm's own separate graph-contraction procedure.

Significance

Chapter 10 is where this book cashes out its structure theory as algorithms with provable running times, and this mission places every result of that chapter's first two sections that is a mathematical proposition rather than a runtime bound: two min-max/optimality-certificate theorems (10.8-10.9) that are the combinatorial core making the following two strongly polynomial algorithms (Schrijver's, and Iwata-Fleischer-Fujishige's) correct, one central-part nonemptiness fact (10.5-10.6) underlying the domain reduction algorithm, and the two fixing/termination certificates (10.23-10.24) that let the scaling algorithms actually output a minimizer with a proof of optimality attached, not just a numerical answer.

None of these results are open — they are Murota's own account of submodular-function- minimization algorithms (sections 10.1-10.2). What this mission contributes is a faithful, machine-checked formal statement of each, including two results (Propositions 10.5 and 10.8) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

Six numbered results in this block (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are excluded as hard: each states a Big-O asymptotic bound on the running time, function-evaluation count, or internal-procedure-call count of a specific iterative algorithm (the domain reduction algorithm, its scaling variant, Schrijver's algorithm, the IFF scaling algorithm). Faithfully stating "this algorithm runs in O(g(n)) time" requires a cost-tracked operational semantics for that specific algorithm — a well-founded recursive procedure with an oracle for evaluating the input function, threading a step/evaluation counter, instantiated over an unbounded family of ground-set sizes n and numeric parameters (K∞, M) — which is a fundamentally different kind of formalization task (computational complexity theory) from every one of the roughly 280 other numbered results in this book, none of which require modeling the cost of computing them. See HARD.md.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq. Base M-convex-set vocabulary is redeclared from prior missions. Linear orderings of V are represented as bijections V ≃ Fin (Fintype.card V) rather than as lists, matching this series' established preference for order-indexed families over sequential data structures. Proposition 10.5's witness vector is stated as an existence claim (the mathematical content of the proposition), rather than by reconstructing the specific recursive modification procedure the book uses to produce it — a choice consistent with how this series has always formalized "the algorithm produces X" claims where X is a mathematical property, by asserting X's existence rather than executing the algorithm (see, e.g., mission 33-ch09c-networkflows's cycle-cancellation theorem). Six numbered results (Propositions 10.4, 10.7, 10.17, 10.18, 10.21, 10.22) are hard; see HARD.md. Contributions completing any of the seven sorrys are welcome; the goal and Proposition 10.9 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
S. Iwata, L. Fleischer, and S. Fujishige, "A combinatorial strongly polynomial algorithm for minimizing submodular functions," Journal of the ACM, 48 (2001), pp. 761-777 [102] (the IFF scaling algorithm this mission's Proposition 10.20 certifies).
A. Schrijver, "A combinatorial algorithm minimizing submodular functions in strongly polynomial time," Journal of Combinatorial Theory, Series B, 80 (2000), pp. 346-355 [182] (Schrijver's algorithm, whose termination criterion is Proposition 10.9).

41 thms2 active usersReviewed

Completed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis XXXII: Network DualityTextbook

Motivation

Mission 32-ch09b-networkflows established the potential and negative-cycle optimality criteria for M-convex submodular flow problems. This mission finishes chapter 9 with the two topics that close it out: the constructive engine behind the negative-cycle criterion — cycle cancellation, which actually improves a nonoptimal flow rather than merely detecting suboptimality, resting on a delicate "unique-min condition" for bipartite matchings — and network duality, the chapter's capstone structural theorem showing that M-convexity and L-convexity are preserved (and their conjugacy is preserved) under transformation by an arbitrary network.

Setting

For a feasible integer flow ξ in the M-convex submodular flow problem MSFP2, a negative cycle in the auxiliary network (Gξ,ℓξ) witnesses suboptimality (mission 32's Theorem 9.20); cycle cancellation modifies ξ along a smallest such cycle to produce a strictly better flow ξ̄ (Eq. (9.75)). The unique-min condition for a pair (x,y) of integer vectors with ‖x-y‖∞=1 asks whether the bipartite graph G(x,y) — vertices the positive/negative supports of x-y, weights the M-convex exchange values Δf(x;v,u) — has a unique minimum-weight perfect matching; when it does, the M-convex exchange inequality of Proposition 6.25 becomes an equality. Separately, a network G=(V,A;S,T) with entrance set S and exit set T transforms a pair of functions f,g on Zˢ into induced functions f̃,g̃ on Zᵀ (Eqs. (9.81)-(9.82)), the minimum cost to meet a boundary specification at the exit given a production cost at the entrance and a transportation cost along arcs.

Formalization targets

Goal: Network duality for Z→Z functions (Theorem 9.26)

M-(resp. M $^\natural$ -)convexity and integer-valuedness of f transfer to the induced f̃; L-(resp. L $^\natural$ -)convexity and integer-valuedness of g transfer to g̃; and if f is M $^\natural$ -convex, g is its L $^\natural$ -conjugate, and each arc cost ga is the conjugate of fa, then g̃ is the conjugate of f̃. Chosen as goal: the book calls this "the harmonious relationship between network flow and M-/L-convexity", its own proof runs roughly six pages (the longest argument in this chunk), and it is the general fact from which Theorems 9.27-9.28 (analogues for other type combinations) and Notes 9.29-9.30 (the aggregation and infimal- convolution closure properties of M-convex functions, already placed in mission 22-ch06b-mconvexfunctions's own Theorem 6.13) all descend.

Supporting structural targets

Theorem 9.22 shows cycle cancellation strictly improves the objective; Propositions 9.23-9.25 are "the key ingredient" behind it: Proposition 9.23 shows the unique-min condition upgrades the M-convex exchange inequality to an equality, Proposition 9.24 gives a checkable characterization of when a bipartite weighted graph has a unique minimum-weight perfect matching, and Proposition 9.25 is the fact that makes the machine run — the specific pair (∂ξ,∂ξ̄) arising from cycle cancellation always satisfies the unique-min condition. Theorems 9.27 and 9.28 are the network duality theorem's own analogues for Z→R and R→R functions, the second restoring the conjugacy assertion (missing for Z→R) via the ordinary real Legendre-Fenchel transform.

Significance

Cycle cancellation is this book's constructive answer to the negative-cycle criterion: not just a certificate of suboptimality, but an actual improvement step, the combinatorial core of the cycle-canceling algorithm explained in section 10.4.3 (mission 35-ch10c-algorithms). Its correctness proof is one of the most intricate combinatorial arguments in the entire book — a proof by contradiction using a multiset-union identity (Eq. (9.80)) to derive a smaller negative cycle from an assumed non-uniqueness, itself resting on Proposition 9.24's Monge-like characterization of unique bipartite matchings. Network duality, meanwhile, is the theorem that explains why discrete convex analysis and network flow theory are so tightly intertwined throughout this book: it is the general mechanism (matroid induction, min-max relations, the M-convex aggregation and infimal-convolution closure properties) underlying nearly every construction chapter 2 introduced informally and chapter 6 proved piecemeal.

None of these results are open — they are Murota's own account of cycle cancellation (section 9.5.2) and network duality (section 9.6). What this mission contributes is a faithful, machine-checked formal statement of each, completing the platform's coverage of chapter 9 begun in missions 12-network-flows and 32-ch09b-networkflows; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

Theorem 9.26's own proof needs the full weight of everything chapter 9 has built (Theorem 9.16's potential criterion for integer flows, the conjugacy theorem of chapter 8), which this mission does not re-prove (proofs are sorry throughout, per this pass's scope) but whose statement still needs the induced-function machinery built faithfully: since the general framework's optimal-value-type quantities can genuinely be -∞ (the book's own blanket hypothesis f̃ > -∞ acknowledges this), InducedFTilde/InducedGTilde are EReal-valued, following the same soundness discipline established in mission 31-ch08d-conjugacyduality for Lagrangian duality's derived quantities.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions. Functions "on Zˢ" for S a proper subset of the ground set are represented as ordinary V→Z functions required to vanish outside S (SupportedOn), rather than as functions on a dependent subset type — a padding-with-zero encoding consistent with this whole series' preference for a single ambient ground-set domain. C[R→R] (univariate real polyhedral convex functions, needed only for Theorem 9.28's arc costs) is formalized as ordinary midpoint-style convexity (IsConvexUnivariateR) rather than the book's own polyhedral characterization, since polyhedrality plays no role in Theorem 9.28's conclusion beyond ensuring the induced functions are well-behaved. All seven numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the seven sorrys are welcome; the goal and Proposition 9.25 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
K. Murota, "Valuated matroid intersection," SIAM Journal on Discrete Mathematics, 9 (1996), pp. 545-561 [135] (the unique-max lemma Proposition 9.23 reformulates, and the proof technique behind Proposition 9.25).
K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (network duality and cycle cancellation for the M-convex submodular flow problem).

74 thms2 active usersReviewed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis XXXI: The Potential Criterion for Network FlowsTextbook

Motivation

Chapter 9 is where discrete convex analysis meets classical network flow theory: the minimum cost flow problem's three hallmark properties — an optimality criterion by potentials, an optimality criterion by negative cycles, and integrality of optimal solutions — are shown to survive, in a precise and increasingly general form, first for arbitrary polyhedral convex costs (MCFP3), then for the M-convex submodular flow problem (MSFP2/MSFP3), the chapter's own combinatorial generalization of the classical problem. This mission places the potential criterion (Theorem 9.4) and its cascade of six corollaries and generalizations, the block of results this book's own text uses to carry every other result in the chapter.

Setting

A digraph G = (V,A) with tail/head maps ∂⁺,∂⁻ : A → V. A flow ξ : A → R has boundary ∂ξ(v) = Σ{ξ(a) : ∂⁺a=v} − Σ{ξ(a) : ∂⁻a=v}. A potential p : V → R has coboundary δp(a) = p(∂⁺a) − p(∂⁻a). The minimum cost flow problem MCFP3 minimizes Γ₃(ξ) = Σₐ fₐ(ξ(a)) + f(∂ξ) over flows, for polyhedral convex arc costs fₐ : R → R∪{+∞} and boundary cost f : Rⱽ → R∪{+∞}; MCFP0 is its linear-cost, fixed-supply special case. The M-convex submodular flow problem MSFP3 is MCFP3 with f additionally M-convex; MSFP2 is its linear-arc-cost special case.

Formalization targets

Goal: The potential criterion for MCFP3 (Theorem 9.4)

For a feasible flow ξ, ξ is optimal for MCFP3 iff there is a potential p with ξ(a) a minimizer of the reduced arc cost fₐ[δp(a)] for every arc and ∂ξ a minimizer of the reduced boundary cost f[−p]; and any such optimal potential characterizes optimality of every feasible flow. This is the hub result of the whole chunk: the book states Theorem 9.14 is "immediate" from it, and every other placed result either specializes it directly or builds on that specialization.

Supporting structural targets

Theorem 9.5 reformulates MCFP0's optimality as the absence of a negative cycle in an auxiliary network; Theorem 9.6 gives MCFP0's primal and dual integrality, the latter identifying the optimal-potential set as an L-convex polyhedron. Theorem 9.14 specializes the goal to MSFP3; Theorem 9.15 upgrades this to a full polyhedral and integrality structure theorem for MSFP3's optimal-flow-boundary and optimal-potential sets (M2-convex and L-convex polyhedra respectively); Theorem 9.16 is the integer-flow analogue, with the boundary set now literally M2-convex and the integer-optimal-potential set literally L-convex. Theorems 9.18 and 9.20 give the negative-cycle reformulation for MSFP2, real and integer flows respectively, generalizing Theorem 9.5 by admitting a third class of auxiliary arcs governed by the M-convex boundary cost's directional derivative (or its discrete difference, in the integer case).

Significance

This is the chapter's demonstration that M-convexity is not merely an abstract combinatorial axiom but the exact structural hypothesis under which classical network-flow duality survives intact: every one of the four "nice properties" the book opens the chapter with (potentials, negative cycles, integrality, efficient algorithms) is preserved verbatim in the M-convex generalization, and this mission's eight results are the proof of that claim for the first three. The chunk's own internal dependency structure — one foundational theorem (9.4) from which every other placed result descends by specialization or direct generalization — is itself characteristic of how this book organizes its combinatorial machinery around a single convex- analytic core.

None of these results are open — they are Murota's own account of network flow duality under M-convexity (sections 9.1, 9.4, and 9.5). What this mission contributes is a faithful, machine-checked formal statement of each, extending the platform's coverage of chapter 9 begun in mission 12-network-flows (which covered §9.1.1-9.1.2 and §9.3, the feasibility and max-flow min-cut results, deliberately leaving this block for later apparatus); no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The eight results span real- and integer-flow versions of two nested problem hierarchies (MCFP0 ⊂ MCFP3, MSFP2 ⊂ MSFP3) and two distinct optimality certificates (potentials, negative cycles), which this mission handles by building one shared apparatus — FeasibleFlowMCFP3, Gamma3, OptimalFlowMCFP3, IsOptimalPotential — that MCFP0 and MSFP3 both instantiate (MCFP0 literally as the linear-cost/singleton-boundary special case of Eq. (9.11)), and one shared generic cycle/negative-cycle apparatus (IsCycle, CycleLength, HasNegativeCycle) instantiated three times with different auxiliary-arc types (A⊕A for MCFP0, A⊕A⊕(V×V) for MSFP2's extra Cξ arcs governed by the boundary cost's directional derivative). "Primal integral" and "dual integral" polyhedral convex functions (the book's own C[Z|R→R]/C[R→R|Z] notation, used in Theorem 9.15) needed a modeling decision, since the book's own definition of these classes lies outside this chunk's page range; see Formalization scope.

Formalization scope

Ground-set vertices V and arcs A are Fintype with DecidableEq. All base M-/L-convexity vocabulary is redeclared from prior missions in this series. "Primal integral" (C[Z|R→R], M[Z|R→R]) is formalized as integer effective domain (IsDomainIntegerArc/IsDomainIntegerR); "dual integral" (C[R→R|Z], M[R→R|Z]) is formalized as the existence of an integer subgradient at every domain point (IsDualIntegralArc/IsDualIntegralR) — a standard equivalent characterization for polyhedral convex functions, and a deliberate modeling choice recorded in MODERATION_NOTES.md rather than a literal transcription of the book's own (out-of-range) definition of these two notation classes. All eight numbered results found in this chunk's page range are placed in full, with no partial-coverage scope reduction. Contributions completing any of the eight sorrys are welcome; the goal and Theorem 9.15 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
R. T. Rockafellar, Network Flows and Monotropic Optimization, Wiley, 1984 [178] (the classical potential/Fenchel-duality framework this mission's Theorem 9.4 adapts).
K. Murota, "Discrete convex analysis," Mathematical Programming, 83 (1998), pp. 313-371 [140] (the Lagrange duality and negative-cycle theory of section 9.5 this mission's Theorems 9.18 and 9.20 draw from).

88 thms2 active usersReviewed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis XXIX: M2-Convex and L2-Convex FunctionsTextbook

Motivation

Mission 29-ch08b-conjugacyduality opened chapter 8's account of M2-convex functions — sums of M-convex functions — proving their domains and minimizers are M2-convex and that they are integrally convex. This mission completes that program and builds its exact mirror for L2-convex functions (integer infimal convolutions of L-convex functions), the class that appears on the opposite side of Edmonds's intersection theorem's min-max relation from M2-convexity. It proves optimality and proximity theorems for both classes, shows their subdifferentials add (a discrete analogue of the classical subdifferential sum rule), derives how the Legendre-Fenchel transform interacts with the sum/infimal-convolution operation, and — the technically hardest result in the whole cluster — establishes that L♮₂-convex functions are integrally convex, by a genuinely different and more intricate argument than the M2-side analogue required.

Setting

Fix a finite ground set $V$ . A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is L2-convex if $g = g_1 \square g_2$ , the integer infimal convolution $g_1\square g_2(p) = \inf\{g_1(p_1)+g_2(p_2) : p_1+p_2=p\}$ , of two L-convex functions $g_1, g_2$ ; L $^\natural_2$ -convex if the summands are L $^\natural$ -convex. An M2-convex function is a sum $f_1+f_2$ of two M-convex functions (mission 29-ch08b-conjugacyduality). The integer subdifferential $\partial_{\mathbb Z} f(x)$ and real subdifferential $\partial_{\mathbb R} f(x)$ generalize the subgradient set to integer- and real-valued perturbation directions respectively.

Formalization targets

Goal: L $^\natural_2$ -convex functions are integrally convex (Theorem 8.42)

Every L $^\natural_2$ -convex function is integrally convex, and in particular every L $^\natural_2$ -convex set is integrally convex. The book's own proof is the most intricate argument in this cluster: given $p$ in the Minkowski sum $D_1+D_2$ of two L-convex sets, it constructs an explicit representation of $p$ as a convex combination of finitely many integer points of $D_1+D_2$ , all lying in $p$ 's own integral neighborhood, via the sorted fractional-part values of a chosen decomposition $p=p_1+p_2$ — a genuinely different technique from the M2-side analogue (Theorem 8.31), whose proof is a two-line consequence of convex extensibility.

Supporting structural targets

Eleven further results build the M2-/L2-convex theory in parallel. Theorems 8.33-8.34 give the M2-optimality criterion (a nonnegative-sum condition over cyclic exchange families) and its scaling-based proximity theorem; Theorem 8.35 shows subdifferentials of a sum of M $^\natural$ - convex functions add, and that subdifferentials of M2-/M $^\natural_2$ -convex functions are L2-/L $^\natural_2$ -convex; Theorem 8.36 computes the conjugate of a sum as the infimal convolution of conjugates, with biconjugacy recovering the original sum. Propositions 8.39-8.41 transfer L-(natural-)convexity from summands to the domain and minimizer set of an L2-convex function, and give the precise attainment condition under which a linearly-perturbed infimal convolution's minimizer set splits additively. Theorems 8.43-8.44 give the L2-optimality and L2-proximity theorems, the exact L-side mirrors of Theorems 8.33-8.34; Theorem 8.45 mirrors Theorem 8.35 for subdifferentials of an infimal convolution; and Theorem 8.46 (found by direct reading, immediately following 8.45 and explicitly named by the book as 8.36's counterpart) shows biconjugacy for L $^\natural$ -convex infimal convolutions.

Significance

The M2-/L2-convex function classes are where discrete convex analysis's abstract machinery meets concrete combinatorial optimization: Edmonds's matroid intersection theorem and its generalizations are literally statements about M2-convex minimization, with the L2-convex side supplying the dual bound. Theorem 8.35's subdifferential additivity is the discrete analogue of the classical Moreau-Rockafellar sum rule, and its proof (via the M-convex intersection theorem, already a milestone of mission 10-conjugacy-i) shows the sum rule holding without the constraint-qualification technicalities the continuous theory needs — a case where the discrete theory is cleaner than its continuous ancestor. Theorem 8.42's harder, dedicated proof technique is itself informative: it demonstrates that L2-convexity's combinatorial structure is not a routine transcription of the M2-convex case, foreshadowing the book's broader theme that M- and L-convexity, while conjugate, are not interchangeable in how their proofs actually work.

None of these results are open — they are Murota's account of the sum/infimal-convolution closure properties of M-convex and L-convex functions, continuing chapter 8's duality program into its most combinatorially concrete corner. What this mission contributes is a faithful, machine-checked formal statement of each, including one result (Theorem 8.46) the platform's own automated extractor missed, extending the shared Lean vocabulary (InfConv, L2Convex, M2ConvexSet) mission 29-ch08b-conjugacyduality began; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal would try to adapt the M2-side integral-convexity proof (a direct appeal to convex extensibility) verbatim; the book's own proof shows this does not work, requiring instead a from-scratch construction: decompose $p=p_1+p_2$ , take fractional parts $a_1 = p_1-\lfloor p_1\rfloor$ and $a_2=\lceil p_2\rceil-p_2$ , sort their combined distinct values, build threshold sets exactly as in the Lovász-extension construction, and verify each resulting integer point $q_i = \lfloor p_1\rfloor+\chi_{U_{1i}}+\lceil p_2\rceil-\chi_{U_{2i}}$ both lies in $D_1+D_2$ (via L-convex-set closure properties, Theorem 5.10) and in $p$ 's integral neighborhood (a case split on whether $p(v)$ is itself an integer) — a genuinely multi-stage combinatorial argument with no single-inequality shortcut, unlike almost every other result in this mission.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; M2-/L2-convex functions are (V→ℤ)→WithTop ℝ. All twelve numbered results found in this chunk's page range are placed, with no partial-coverage scope reduction needed — every clause of every result, including all three parts of Theorems 8.35 and 8.45 and the full cyclic-exchange condition of Theorems 8.33-8.34, is stated in full. One numbered result nominally in this chunk's page range, Theorem 8.32, is not re-placed here: it was already found and placed as a milestone in mission 29-ch08b-conjugacyduality, whose own page range overlaps this chunk's by one page (PDF245) — see HARD.md. "g1□g2 > −∞" hypotheses are omitted rather than translated, since WithTop ℝ has no −∞ element to violate. This mission's base vocabulary is redeclared verbatim from mission 29-ch08b-conjugacyduality rather than imported, since sibling drafts in this series cannot yet reference one another; ConvexConjugate is redeclared from mission 10-conjugacy-i. Contributions completing any of the twelve sorrys are welcome; the goal and Theorem 8.35 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
K. Murota and A. Shioura, "Extreme points of a generalized polymatroid," Discrete Applied Mathematics, 152 (2005), pp. 268-278 [153] (the L2-convex integral-convexity proof this mission's goal is drawn from).
K. Murota and A. Tamura, "Application of M-convex submodular flow problem to mathematical economics," Japan Journal of Industrial and Applied Mathematics, 20 (2003), pp. 257-277 [162] (the M2-proximity theorem, Theorem 8.34).

55 thms2 active usersReviewed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis XXVIII: The Conjugacy TheoremTextbook

Motivation

Chapter 8 is where discrete convex analysis explains why it needed two separate notions — M-convexity (exchangeability) and L-convexity (submodularity) — rather than one. The answer is conjugacy: under the classical Legendre-Fenchel transform, the two classes turn out to be exactly dual to each other, the discrete analogue of the fact that convex analysis's transform is self-dual within a single class of convex functions. Mission 10-conjugacy-i proved the integer-lattice version of this fact (Theorem 8.12) but explicitly deferred the polyhedral version — Theorem 8.4, the chapter's own headline "Conjugacy theorem" — noting it needed a real-variable M-/L-convex-function layer the series had not yet built. That layer now exists, built across missions 23-24-ch06*-mconvexfunctions and 26-27-ch07*-lconvexfunctions. This mission proves Theorem 8.4 and its companions: the polar-cone correspondence it induces, its nonpolyhedral generalization, the separation and Fenchel-duality theorems for M♮-/L♮-convex functions, and the basic theory of M2-convex functions (sums of M-convex functions), which the Edmonds intersection theorem's own combinatorics is built from.

Setting

Fix a finite ground set $V$ . For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ , the Legendre-Fenchel transform is $f^\bullet(p) = \sup_x [\langle p,x\rangle - f(x)]$ . A polyhedral convex function $f$ is M-convex ( $f \in M[\mathbb R \to \mathbb R]$ ) if it satisfies (M-EXC[R]); $g$ is L-convex ( $g \in L[\mathbb R \to \mathbb R]$ ) if it satisfies (SBF[R]) and (TRF[R]). A concave function $h$ is always represented via $h_2 = -h$ , an ordinary convex function, so every " $f \ge h$ " hypothesis is restated as " $f + h_2 \ge 0$ " — an equivalent formulation avoiding any need to represent $-\infty$ in the codomain. A polyhedral cone's polar is $C^\circ = \{y : \langle y,x\rangle \le 0\ \forall x \in C\}$ . A function is M2-convex if it is the sum of two M-convex functions.

Formalization targets

Goal: the conjugacy theorem (Theorem 8.4)

The classes of polyhedral M-convex functions and polyhedral L-convex functions are in one-to-one correspondence under the Legendre-Fenchel transform: $f \in M \Rightarrow f^\bullet \in L$ , $g \in L \Rightarrow g^\bullet \in M$ , and the transform is an involution ( $f^{\bullet\bullet}=f$ , $g^{\bullet\bullet}=g$ ) on each class, with the identical statement for the M $^\natural$ /L $^\natural$ variants. This is the theorem mission 10-conjugacy-i deferred, citing exactly the missing infrastructure this series has since built.

Supporting structural targets

Twelve further results build the surrounding theory. Proposition 8.2 gives the easy two-variable case of the general submodularity-preservation fact (Theorem 8.1, already a milestone of mission 10-conjugacy-i); Proposition 8.3 is the technical minimizer-difference lemma the goal's harder direction is built from. Theorem 8.5 derives the M-convex/L-convex cone polarity from the goal, and Theorem 8.6 extends the correspondence beyond the polyhedral case to general closed proper convex functions. Proposition 8.14 and Theorems 8.15-8.16 build the separation theory for M♮-/L♮-convex and concave function pairs, with integral witnesses when the functions are integer valued; Theorem 8.21 (parts 1-2) derives the Fenchel-type strong-duality equality these separation theorems make possible. Propositions 8.29-8.30 and Theorem 8.31 (plus Theorem 8.32, found by direct reading immediately after 8.31) build the basic theory of M2-convex functions: their domains and minimizer sets are M2-convex, they are integrally convex, and their global optimality reduces to a finite local check.

Significance

The goal is the theorem that retroactively explains this entire series' two-track structure: missions 20-25 (M-convex sets and functions) and 08/21/26-28 (L-convex sets and functions) are not two independent theories that happen to share techniques — they are conjugate images of each other, so every theorem proved on one side has a dual counterpart automatically available on the other via Theorem 8.4. This is made concrete immediately: Theorem 8.5's cone polarity and the diagram the book draws connecting $M_0[\mathbb R]$ , $0L[\mathbb R\to\mathbb R]$ , and submodular set functions $S[\mathbb R]$ (already correspondences this series proved independently, in missions 24-ch06d-mconvexfunctions and 28-ch07d-lconvexfunctions) are shown to be facets of one single conjugacy fact rather than three separate coincidences. The separation and Fenchel duality theorems (8.15, 8.16, 8.21) are the discrete analogues of the two theorems every convex optimization course opens with, and the book is explicit that they are not corollaries of the classical versions plus convex extensibility — they carry genuinely combinatorial content, specializing to Frank's discrete separation theorem and Edmonds's intersection theorem as examples the book itself gives.

None of these results are open — they are Murota's account of the duality at the heart of discrete convex analysis, the reason the theory needed two dual notions rather than one. What this mission contributes is a faithful, machine-checked formal statement of each, completing a theorem mission 10-conjugacy-i explicitly left for a future session once the necessary polyhedral apparatus existed, and including one result (Theorem 8.32) the platform's own automated extractor missed; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to the goal's harder direction (L⇒M) would try to verify the exchange inequality for $g^\bullet$ directly from the definition of the transform; the book's actual proof instead identifies the exchange inequality with a statement about weighted minimizers of $g$ itself via Proposition 8.3 (the minimizer-difference bound), converting a claim about the conjugate function into a claim about $g$ 's own combinatorial structure — a genuine change of perspective, not a direct calculation. Proposition 8.3's own proof is the hardest single argument in this block: it derives the minimizer-difference bound by a contradiction argument that constructs an explicit pair of "worse" minimizers via a join/meet perturbation and derives a strict inequality from Theorem 7.29's translation inequality — a multi-step combinatorial argument with no direct shortcut.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; convex functions are WithTop ℝ valued throughout (never EReal, except for the Legendre-Fenchel transform itself, whose defining supremum/infimum can genuinely be infinite). All thirteen numbered results found in this chunk's page range — the twelve in BRIEF.md's own table plus Theorem 8.32 — are placed, with one documented scope reduction: Theorem 8.21 states only its real-attainment parts (1)-(2), not the integer-attainment refinement of parts (3)-(4), which needs a separate argument no other result in this chunk requires — see HARD.md. Concave functions $h$ are always represented via $h_2 = -h$ and every inequality $f \ge h$ restated as $f + h_2 \ge 0$ , avoiding WithTop ℝ negation entirely. This chunk's own BRIEF.md inherited the chapters-4-7 page-offset boilerplate (printed = PDF $-$ 19); chapter 8 uses offset 18, confirmed against the PDF's own footers — every citation here uses the corrected offset. This mission's base vocabulary is redeclared from missions 10-conjugacy-i, 20-ch04b-mconvexsets, 21-ch05b-lconvexsets, 23-24-ch06*-mconvexfunctions, and 26-27-ch07*-lconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the thirteen sorrys are welcome; the goal and Proposition 8.3 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 [152] (the polyhedral M-/L-convex conjugacy theory this mission's real-variable results are drawn from).

73 thms2 active usersReviewed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis IX: The Discrete Conjugacy TheoremTextbook

Motivation

The Legendre-Fenchel transform is the single most structurally important operation in convex analysis: for a proper closed convex function $f$ , its conjugate $f^\bullet(p) = \sup_x \{\langle p,x\rangle - f(x)\}$ is again proper closed convex, and the transform is an involution — $f^{\bullet\bullet} = f$ . This one fact underlies duality theory across optimization: every strong-duality theorem is, at bottom, a statement about conjugate pairs. Chapters 6 and 7 of this book developed M-convex and L-convex functions as if they were two separate theories, each with its own exchange axiom, optimality criterion, and proximity theorem. Chapter 8 reveals they were never separate: the Legendre-Fenchel transform, suitably discretized, is a bijection between the two classes. This mission formalizes that discrete conjugacy theorem together with its classical real-valued precursor and a genuine function-level generalization of Edmonds's intersection theorem, completing the picture that chunks 06 through 09 built the two halves of.

Setting

Let $V$ be a finite ground set. For $f : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ , the Legendre-Fenchel transform is $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb R^V\}$ ; $f$ is submodular if $f(x)+f(y) \ge f(x\vee y)+f(x\wedge y)$ and supermodular under the reverse inequality. For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ , the discrete Legendre-Fenchel transform restricts the same supremum formula to $p \in \mathbb Z^V$ : $f^\bullet(p) = \sup\{\langle p,x\rangle - f(x) : x \in \mathbb Z^V\}$ for $p \in \mathbb Z^V$ — a genuinely different object from the real-valued transform, since the supremum is now over integer $x$ only, and the codomain is checked back against the discrete M-/L-convexity axioms of chunks 06–09. The integer biconjugate $f^{\bullet\bullet}$ is the transform applied twice. $f$ is integer valued if every finite value it takes is an integer (the classes $M[\mathbb Z\to\mathbb Z]$ , $L[\mathbb Z\to\mathbb Z]$ of the goal theorem are exactly the M-/L-convex functions with this property).

Formalization targets

Goal: Theorem 8.12 (the discrete conjugacy theorem)

(1) The classes $M[\mathbb Z\to\mathbb Z]$ and $L[\mathbb Z\to\mathbb Z]$ are in one-to-one correspondence under the discrete Legendre-Fenchel transform: for $f \in M[\mathbb Z\to\mathbb Z]$ and $g \in L[\mathbb Z\to\mathbb Z]$ , $f^\bullet \in L[\mathbb Z\to\mathbb Z]$ , $g^\bullet \in M[\mathbb Z\to\mathbb Z]$ , $f^{\bullet\bullet}=f$ , and $g^{\bullet\bullet}=g$ . (2) The same correspondence holds between $M^\natural[\mathbb Z\to\mathbb Z]$ and $L^\natural[\mathbb Z\to\mathbb Z]$ .

Milestones: Theorem 8.1, Proposition 8.11, Theorem 8.17

Theorem 8.1: the conjugate of a real-valued submodular function is always supermodular — the classical warm-up, and evidence that submodularity/supermodularity is not symmetric under conjugation on its own (the converse fails). Proposition 8.11: the integer biconjugate recovers $f$ at any point with a nonempty integer subdifferential — the fact that makes discrete biconjugation meaningful at all. Theorem 8.17 (the M-convex intersection theorem): a point jointly minimizes a sum of two M $^\natural$ -convex functions if and only if a single linear functional separately certifies it as a minimizer of each perturbed function — the function-level generalization of chunk 04's Edmonds's intersection theorem for M-convex sets.

Significance

The result itself. The discrete conjugacy theorem is, in the book's own words, "the unifying result of the entire book": every theorem proved separately for M-convex functions (chunks 06–07) has an exact mirror for L-convex functions (chunks 08–09) precisely because the Legendre-Fenchel transform carries one class to the other. Theorem 8.17's function-level Edmonds generalization shows the payoff directly — the classical matroid-intersection-style min-max duality of chunk 04 was never really about sets; it is a special case (indicator functions) of a duality that holds for the whole class of M-convex functions.

Formalizing it. No matching item exists on the platform for conjugate functions, discrete conjugacy, or this generality of intersection theorem. This mission gives the first formal statement of the discrete conjugacy theorem, distinguishing it carefully from its real-valued (polyhedral) precursor, Theorem 8.4 — a genuinely different, harder theorem this mission does not draft (see Formalization scope), since the integer bijection needs the M-/L-proximity theorems of chunks 06–09 to control integrality under convex extension, while the real-valued case does not.

Difficulty

The obvious approach — try to prove the discrete conjugacy theorem directly by mimicking the real-valued proof (Theorem 8.4) with ℤ in place of ℝ everywhere — fails, because the real-valued proof's key step (Proposition 8.3, an infimal-convolution argument comparing arg min sets of perturbed polyhedral functions) has no immediate discrete analogue: a discrete arg min need not vary continuously with the perturbation the way a polyhedral one does. The book's actual strategy instead routes through the convex extension of the discrete function (chunk 06/08's bridge to chapter 3's integral convexity), applies the already-proved real-valued conjugacy theorem to the extension, and then must separately argue that the resulting conjugate, restricted back to integer points, is again integer-valued and satisfies the discrete exchange axiom — an argument that needs different treatment depending on whether the original function's domain is bounded or unbounded (an exhaustion argument via restriction to a growing integer interval, invoking chunk 06's proximity theorem to control convergence). Skipping this discreteness argument and treating the real-valued theorem as if it settled the integer case would silently discard exactly the chapter's own point.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq. ConvexConjugate (the discrete transform) has domain and codomain both (V → ℤ) → WithTop ℝ, obtained by taking the defining supremum in EReal (a complete lattice, so it is always total) and projecting back via a new FromEReal map — this is what lets the biconjugate f•• typecheck as an equality of functions of the same type as f. ConvexConjugateR (the real-valued transform, used only by the milestone Theorem 8.1) is a separate object with no shared code, per the explicit warning against conflating the two transforms; the two never appear in the same item.

A trivializing formalization of the goal would draft only the real-valued case (Theorem 8.4) as if it were the discrete theorem, or would silently allow WithTop ℝ's subtraction-avoidance convention to change which values are compared; neither is done. Theorem 8.4 itself (the polyhedral conjugacy theorem) is not drafted in this mission at all — it would require a fresh, otherwise-unused polyhedral M-/L-convex-function layer on Rⱽ that no other item here needs (see MODERATION_NOTES.md). The M-/L-separation theorems (8.15, 8.16) and the Fenchel-type duality theorem (8.21) are likewise left for a follow-on mission; contributions building the polyhedral bridge or the separation theorems, which depend on machinery this mission establishes, are welcome.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

13 thms2 active usersReviewed

Completed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis VII: The L-Optimality Criterion and the Proximity TheoremTextbook

Motivation

Submodularity — the diminishing-returns property $g(p) + g(q) \ge g(p \vee q) + g(p \wedge q)$ on a lattice — is one of the most useful structural hypotheses in combinatorial optimization, underlying efficient algorithms for network flows, matroid theory, and set-function minimization. Chapter 7 studies L-convex functions: functions on the integer lattice $\mathbb Z^V$ that are submodular and linear along the all-ones direction. This is the "dual" notion, under the conjugacy developed later in the book, to chunk 06's M-convex functions, and it inherits the same strong minimization theory — a purely local optimality criterion and a proximity theorem with an explicit distance bound — while additionally supporting a genuinely new characterization with no M-convex counterpart: discrete midpoint convexity, the direct lattice analogue of the classical real-valued midpoint convexity condition. This mission formalizes the chapter's definitional theorem, its midpoint-convexity characterization, the L-optimality criterion, and the L-proximity theorem itself.

Setting

Let $V$ be a finite ground set. A function $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain is an L-convex function if it satisfies (SBF[Z]): $g(p) + g(q) \ge g(p \vee q) + g(p \wedge q)$ for all $p, q$ ( $\vee, \wedge$ componentwise max/min), and (TRF[Z]): there is $r \in \mathbb R$ with $g(p + \mathbf 1) = g(p) + r$ for all $p$ , where $\mathbf 1$ is the all-ones vector. An L $^\natural$ -convex function is one whose lift to the extended ground set $\{0\} \cup V$ is L-convex; equivalently (Theorem 7.1), $g$ satisfies the translation-submodularity axiom (SBF $^\natural$ [Z]): $g(p) + g(q) \ge g((p - \alpha\mathbf 1) \vee q) + g(p \wedge (q + \alpha\mathbf 1))$ for all $p, q$ and all nonnegative integers $\alpha$ . Discrete midpoint convexity asks $g(p) + g(q) \ge g(\lceil (p+q)/2 \rceil) + g(\lfloor (p+q)/2 \rfloor)$ componentwise. For $\alpha$ a positive integer, a point satisfies scaled local optimality if $g(p_\alpha) \le g(p_\alpha \pm \alpha \chi_Y)$ for every $Y \subseteq V$ .

Formalization targets

Goal: Theorem 7.18 (the L-proximity theorem)

Assume $\alpha$ is a positive integer and $n = |V|$ . (1) If $g$ is L-convex with $g(p) = g(p+\mathbf 1)$ for all $p$ , and $p_\alpha \in \operatorname{dom} g$ satisfies $g(p_\alpha) \le g(p_\alpha + \alpha\chi_Y)$ for all $Y \subseteq V$ , then $\arg\min g \ne \emptyset$ and there is $p^* \in \arg\min g$ with the componentwise bound

p_\alpha \le p^* \le p_\alpha + (n-1)(\alpha-1)\mathbf 1.

(2) If $g$ is L $^\natural$ -convex and $p_\alpha$ satisfies the two-sided version, then there is $p^*$ with $p_\alpha - n(\alpha-1)\mathbf 1 \le p^* \le p_\alpha + n(\alpha-1)\mathbf 1$ . The bound is a genuine vector (lattice-order) inequality, not an $\ell^\infty$ -norm bound — the form later chapters' applications need.

Milestones: Theorems 7.1, 7.7, 7.14

Theorem 7.1: L $^\natural$ -convexity (defined via the lift) is equivalent to the direct translation-submodularity axiom. Theorem 7.7: this same class is also characterized by discrete midpoint convexity — a three-way equivalence with the approach property (L $^\natural$ -APR[Z]) as a bridge — giving L-convexity a genuinely different, more geometric face than anything available on the M-convex side. Theorem 7.14 (the L-optimality criterion): global optimality reduces to a purely local check against the sign-pattern neighbors $p \pm \chi_Y$ , mirroring chunk 06's Theorem 6.26 but with the plain L-convex case additionally requiring the periodicity condition $g(p) = g(p+\mathbf 1)$ .

Significance

The result itself. Discrete midpoint convexity (Theorem 7.7) is philosophically important: it shows the lattice-submodularity definition of L-convexity is not an arbitrary discretization choice but coincides exactly with the most direct discrete analogue of ordinary midpoint convexity, the classical characterization of convex functions via $f((p+q)/2) \le (f(p)+f(q))/2$ . The L-optimality criterion and L-proximity theorem give L-convex minimization the same algorithmic footing as M-convex minimization (chunk 06): scaling algorithms for L-convex objectives — which arise naturally from network flow and submodular-function duality — inherit a provable, dimension-and-scale-explicit distance guarantee between a coarse-scale local optimum and the true minimizer.

Formalizing it. No matching item exists on the platform for L-convex functions, discrete midpoint convexity, or the L-optimality/proximity theorems. This mission gives the first formal statement of these results, completing (alongside chunk 06's M-convex-function results) both halves of the exchange-axiom-based theory that chapter 8's conjugacy duality later unifies.

Difficulty

A natural shortcut, given the structural parallel to chunk 06, is to assume the L-proximity theorem's proof is a mechanical relabeling of the M-proximity theorem's proof. It is not: the M-convex proof (chunk 06) crucially uses the exchange axiom's additive four-term inequality to build a chain of strictly improving points, whereas the L-convex proof instead exploits (TRF[Z])'s periodicity directly — it reduces to the case $p_\alpha = 0$ using translation invariance, then constructs a minimal (with respect to the lattice order) point among all sufficiently good solutions and shows this minimality, combined with submodularity (SBF[Z]), forces the componentwise bound. The vector (rather than norm) form of the conclusion is not cosmetic: it is exactly what this lattice-order argument naturally produces, and is the form needed by later chapters' applications.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $g : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ is (V → ℤ) → WithTop ℝ. Unlike chunk 06's M-convex axiom, (SBF[Z]), (TRF[Z]), and (SBF $^\natural$ [Z]) are stated for all of $\mathbb Z^V$ , not restricted to $\operatorname{dom} g$ , so no explicit import of chunk 05's L-convex-set vocabulary was needed for dom g's structure (unlike the corresponding note in chunk 06's BRIEF.md, which flagged the same concern for dom f). L $^\natural$ -convexity is represented via an explicit lift to Option V, matching the book's own primary definition, with the direct axiom (SBF $^\natural$ [Z]) kept as a separate object related to it by Theorem 7.1.

A trivializing formalization of the goal would convert its componentwise vector bound into an $\ell^\infty$ -norm bound (losing the direction-of-approach information the vector form carries) or drop Part (1)'s periodicity hypothesis $g(p) = g(p+\mathbf 1)$ ; neither is done here. Propositions establishing dom g as an L-convex set, the L/L $^\natural$ relationship (Theorem 7.3), the submodular-set-function embedding (Proposition 7.4), and several structural closure properties are cut from this mission's scope (see MODERATION_NOTES.md) but are natural targets for a follow-on mission or for chunk 09, which builds directly on this chunk's exchange-axiom vocabulary, mirroring chunks 06→07.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.

18 thms2 active usersReviewed

Functional Analysis Operations Research·Captain: mikedeng1

On the Maximal Monotonicity of Subdifferential Mappings II: Subdifferentials Are Exactly the Maximal Cyclically Monotone Operators, Unique up to an Additive ConstantResearch Paper

Motivation

A differentiable convex function on $\mathbb{R}^n$ is determined, up to an additive constant, by its gradient, and a vector field is a gradient of a convex function exactly when it satisfies a monotonicity condition along closed cycles. Convex analysis and optimization need the same statement for nonsmooth and extended-valued functions on infinite-dimensional spaces: the subdifferential replaces the gradient, and the question becomes which multivalued maps from a Banach space to its dual arise as subdifferentials, and how much of the function they determine. The answer underlies the treatment of optimality conditions, variational inequalities and evolution equations governed by subdifferentials, where one works with the operator $\partial f$ and needs to recover $f$ from it.

Timeline.

1966: R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (DOI 10.2140/pjm.1966.17.497), studied cyclically monotone operators and stated the characterization of subdifferentials as the maximal cyclically monotone operators (its Theorem 3), together with the maximal monotonicity of subdifferentials (its Theorem 4).
1969: H. Brézis pointed out a gap in the 1966 proofs of maximality and uniqueness: a family of dual vectors $x_\varepsilon^*$ used in the argument might increase unboundedly in norm as $\varepsilon \to 0$ .
1970: Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (DOI 10.2140/pjm.1970.33.209), repaired the argument for arbitrary real Banach spaces, proving Theorem A (maximal monotonicity of $\partial f$ ) and Theorem B (the characterization treated here).

Setting

Let $E$ be a real Banach space with dual $E^*$ , and write $\langle x, x^* \rangle$ for the value of $x^* \in E^*$ at $x \in E$ . A proper convex function on $E$ is a function $f : E \to (-\infty, +\infty]$ , not identically $+\infty$ , with $f((1-\lambda)x + \lambda y) \le (1-\lambda)f(x) + \lambda f(y)$ for all $x, y \in E$ and $0 < \lambda < 1$ . It is lower semicontinuous (lsc) in the norm topology. Its subdifferential is the multivalued map

\partial f(x) = \{\, x^* \in E^* \mid f(y) \ge f(x) + \langle y - x, x^* \rangle \ \ \forall y \in E \,\}.

A multivalued map $T : E \to E^*$ is a cyclically monotone operator if

\langle x_0 - x_1, x_0^* \rangle + \cdots + \langle x_{n-1} - x_n, x_{n-1}^* \rangle + \langle x_n - x_0, x_n^* \rangle \ge 0 \qquad\text{whenever } x_i^* \in T(x_i),\ i = 0, \dots, n,

and maximal cyclically monotone if, in addition, its graph $\{(x, x^*) \mid x^* \in T(x)\}$ is not properly contained in the graph of any other cyclically monotone operator. The conjugate of $f$ is $f^*(x^*) = \sup_{x \in E} (\langle x, x^* \rangle - f(x))$ on $E^*$ , and $j(x) = \tfrac12\|x\|^2$ . In the Lean development these are ProperConvex, subdiff, IsCyclicallyMonotone, IsMaximalCyclicallyMonotone, conj and halfSqNorm, in the namespace RockafellarMaxMono.Cyclic.

Formalization targets

Goal: Theorem B (p. 210)

For every multivalued map $T : E \to E^*$ on a real Banach space $E$ ,

\bigl(\exists f \text{ lsc proper convex with } T = \partial f\bigr) \iff T \text{ is maximal cyclically monotone},

and if $f$ and $g$ are lsc proper convex with $\partial f = T = \partial g$ , then $g = f + c$ for a real constant $c$ . Both halves are one statement.

Milestones, in attack order

(3.7) For a finite continuous convex function $f$ on a real Banach space, $\partial f(x)$ is nonempty and weak* compact and $f'(x;u) = \max\{\langle u, x^* \rangle \mid x^* \in \partial f(x)\}$ .
Finite continuous case (pp. 214–215). For finite continuous convex $f, g$ on a real Banach space, $\partial g(x) \supset \partial f(x)$ for all $x$ implies $g = f + \mathrm{const}$ .
(3.1) $\partial(f + j)(x) = \partial f(x) + \partial j(x)$ for lsc proper convex $f$ .
Proposition 1 $x^{**} \in \partial f^*(x^*)$ if and only if $x^{**}$ is a weak** limit of a bounded net $x_i$ with $x_i^* \in \partial f(x_i)$ , $x_i^* \to x^*$ in norm.
(p. 213) $(f + j)^*$ is finite and continuous on $E^*$ .
(p. 211) $f^{**}$ restricted to $E$ is $f$ .
(3.6) For lsc proper convex $f, g$ : $\partial g(x) \supset \partial f(x)$ for all $x$ implies $g = f + \mathrm{const}$ .

Significance

The result. Theorem B gives an intrinsic description of subdifferential maps: an operator is the subdifferential of a closed proper convex function if and only if it satisfies the cycle inequality and cannot be enlarged without violating it. The uniqueness clause says that a closed convex function is recovered from its subdifferential up to a constant, the nonsmooth counterpart of recovering a function from its gradient. Milestone 7 is stronger than uniqueness: a one-sided inclusion $\partial f \subseteq \partial g$ already forces $g = f + c$ , and this is what gives maximality.

Formalizing it. The theorem is proved in the paper, and nothing of it is formalized on the platform. Mathlib has convex functions, continuous duals, biduals and weak-* topologies, but not extended-valued subdifferentials on Banach spaces, conjugate duality in the nonreflexive setting, or monotone operator theory. This mission produces formal statements of the paper's steps, the standard max formula for directional derivatives on a Banach space, and the Fenchel conjugate facts the argument uses, each as a separate target.

Difficulty

In a reflexive space the argument is short, because $\partial f^*$ is the inverse of $\partial f$ . In a nonreflexive space it is not: $\partial f^*$ maps $E^*$ into $E^{**}$ , and points of $E^{**} \setminus E$ appear. The naive route, transferring the inclusion $\partial f \subseteq \partial g$ to the conjugates by inverting the maps, breaks down there, and the 1966 argument failed at a related step, where the dual vectors in an approximation could be unbounded. Relating $\partial f^*$ to $\partial f$ without reflexivity is where the difficulty sits; the boundedness of the approximating nets in Proposition 1 is essential and cannot be dropped. The finite continuous case and the max formula (3.7) are needed on an arbitrary Banach space, including the dual $E^*$ , not only on $E$ .

Formalization scope

$E$ is a real Banach space (NormedAddCommGroup, NormedSpace ℝ, CompleteSpace); $E^*$ is StrongDual ℝ E with the operator norm, $E^{**}$ is StrongDual ℝ (StrongDual ℝ E), and $E \hookrightarrow E^{**}$ is NormedSpace.inclusionInDoubleDual. No reflexivity, inner product or finite dimension is assumed. Explicit readings:

Values in $(-\infty, +\infty]$ are EReal with the requirement $f(x) \ne -\infty$ ; convexity is the paper's inequality for $0 < \lambda < 1$ in EReal arithmetic. Lower semicontinuity is in the norm topology.
A multivalued map is E → Set (StrongDual ℝ E); $T = \partial f$ means $T(x) = \partial f(x)$ for every $x$ .
The cycle inequality quantifies over all $n \in \mathbb{N}$ and points indexed by Fin (n + 1) with wrap-around addition, so the last term is $\langle x_n - x_0, x_n^* \rangle$ . Maximality is graph inclusion among cyclically monotone operators, not among monotone operators.
The uniqueness constant is a real number, never $\pm\infty$ .
" $\supset$ " in (3.6) is non-strict inclusion, and the hypothesis is one-sided.
A net is a nonempty directed partially ordered index type with convergence along atTop; weak** convergence is pointwise convergence on $E^*$ ; "bounded" is a uniform norm bound.
"Finite and continuous" for $(f+j)^*$ means equal everywhere to a continuous real-valued function. The max in (3.7) is IsGreatest, so it is attained; the directional derivative is the limit along $\lambda \to 0^+$ .
The print's " $\partial(f + j) = \partial f(x) + \partial j(x)$ " in (3.1) is read as $\partial(f+j)(x)$ .

A formalization that drops lower semicontinuity, allows an extended-real constant, or replaces "maximal cyclically monotone" by "maximal monotone" states a different, and in the first two cases false or trivial, theorem; the statements here keep all three.

The proof reduces Theorem B to milestone 7 through Theorem 1 of Rockafellar (1966) and its Corollary 2, which are not stated in this paper and are not milestones; formal statements of them are welcome as supporting theorems. Contributions of reusable infrastructure are welcome: extended-valued subdifferentials and conjugates on normed spaces, the Fenchel–Moreau identity on $E$ , the sum rule with a continuous function, and the max formula for directional derivatives.

Selected references

R. T. Rockafellar, On the maximal monotonicity of subdifferential mappings, Pacific J. Math. 33 (1970), 209–216. https://doi.org/10.2140/pjm.1970.33.209
R. T. Rockafellar, Characterization of the subdifferentials of convex functions, Pacific J. Math. 17 (1966), 497–510. https://doi.org/10.2140/pjm.1966.17.497
G. J. Minty, On the monotonicity of the gradient of a convex function, Pacific J. Math. 14 (1964), 243–247. https://doi.org/10.2140/pjm.1964.14.243
J.-J. Moreau, Fonctionnelles convexes, mimeographed lecture notes, Collège de France, 1967.
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

13 thms2 active usersReviewed

Completed

Combinatorics Discrete Geometry Operations Research+1·Captain: Shuze Chen

Discrete Convex Analysis XXIII: Directional Derivatives and Subdifferentials of M-Convex FunctionsTextbook

Motivation

An M-convex function is defined on the integer lattice, but chapter 6's earlier results (companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions, 23-ch06c-mconvexfunctions) show it always extends to a genuine convex function on real space. Once that extension exists, every tool of classical convex analysis — directional derivatives, subdifferentials, positive homogeneity — becomes available, and the natural question is whether these classical objects remain combinatorially special when applied to an M-convex function's extension. This mission answers that question at its sharpest: the directional derivative of an M-convex function at any point is again a positively homogeneous M-convex function, its subdifferential is exactly the admissible-potential set of a distance function satisfying the triangle inequality, and this correspondence between positively homogeneous M-convex functions and triangle-inequality distance functions is itself a clean one-to-one correspondence. This closes the loop between chapters 4-5 (M-convex and L-convex sets, distance functions) and the continuous convex-analytic machinery chapter 8 needs for its duality theory.

Companion missions 06-mconvex-functions-i, 22-ch06b-mconvexfunctions, and 23-ch06c-mconvexfunctions cover this chapter's optimality theory, algebraic toolkit, and convex-extensibility characterization. This mission builds the vocabulary those results also need (redeclared here, since sibling drafts cannot yet import one another) and proves the chapter's real-variable capstones: the transfer of M-convexity's basic operations, optimality criterion, and supermodularity to the polyhedral (real-variable) setting, the identification of positively homogeneous M-convex functions with distance functions satisfying the triangle inequality, and — this mission's goal — the full directional-derivative/subdifferential correspondence.

Setting

Fix a finite ground set $V$ . A polyhedral convex function $g : \mathbb R^V \to \mathbb R \cup \{+\infty\}$ is (polyhedral) M-convex if it satisfies the real-variable exchange axiom (M-EXC[R]): for $x,y \in \operatorname{dom}_{\mathbb R} g$ and $u \in \operatorname{supp}^+(x-y)$ , some $v \in \operatorname{supp}^-(x-y)$ and $\alpha_0 > 0$ make the exchange inequality hold on $\alpha \in [0,\alpha_0]$ ; M♮-convex if its lift to one extra coordinate is M-convex. The directional derivative of $g$ at $x \in \operatorname{dom}_{\mathbb R} g$ in direction $d$ is $g'(x;d) = \inf_{t>0} (g(x+td) - g(x))/t$ . A function is positively homogeneous if $g(tx) = t \cdot g(x)$ for all $t > 0$ ; write $0M[\mathbb R \to \mathbb R]$ for the positively homogeneous polyhedral M-convex functions. A distance function $\gamma$ satisfying the triangle inequality and its set of admissible potentials $D(\gamma)$ were introduced in chapter 5; the subdifferential $\partial_{\mathbb R} f(x) = \{p : f(y) - f(x) \ge \langle p, y-x \rangle\ \forall y\}$ generalizes this to any function $f$ at a point $x$ in its domain.

Formalization targets

Goal: the directional-derivative/subdifferential correspondence

For $f \in M[\mathbb R \to \mathbb R]$ and $x \in \operatorname{dom}_{\mathbb R} f$ , setting $\gamma_{f,x}(u,v) = f'(x;-\chi_u+\chi_v)$ :

\gamma_{f,x} \text{ satisfies the triangle inequality}, \quad \partial_{\mathbb R} f(x) = D(\gamma_{f,x}) \ne \emptyset, \quad f'(x;\cdot) = \widehat{\gamma_{f,x}}(\cdot),

with the analogous statement for $f \in M[\mathbb Z \to \mathbb R]$ at an integer point $x$ , using $\gamma_{f,x}(u,v) = f(x-\chi_u+\chi_v)-f(x)$ (Theorem 6.61). This is the weakest stable form: it identifies the subdifferential exactly, as a set, rather than bounding its size or complexity, and holds at every point of the domain uniformly.

Supporting structural targets

Ten further results build the real-variable toolkit and the positive-homogeneity correspondence this goal completes: the transfer of M♮-convexity, the basic operations, the optimality criterion, supermodularity, and weighted-minimizer polyhedrality to the real-variable setting (Theorems 6.48-6.52, Proposition 6.53), the identification of the classes $0M[\mathbb Z|\mathbb R \to \mathbb R]$ and $0M[\mathbb R \to \mathbb R]$ and the compatibility of convex extension with positive homogeneity (Proposition 6.56), the two directions of the correspondence between positively homogeneous M-convex functions and triangle-inequality distance functions (Propositions 6.57-6.58, Theorem 6.59), and the fact that a directional derivative of an M-convex function is itself positively homogeneous and M-convex (Proposition 6.60).

Significance

Theorem 6.61 is the technical bridge that lets discrete convex analysis borrow the entire apparatus of classical convex duality: because the subdifferential of an M-convex function is always the admissible-potential set of a chapter-5 distance function, every fact already proved about $D(\gamma)$ (its polyhedral structure, its own L-convexity, its relationship to shortest paths) transfers immediately to subdifferentials of M-convex functions. This is exactly the mechanism the book calls out as essential for Chapter 8's separation theorem for M♮-convex functions. The $0M \leftrightarrow T$ correspondence (Theorem 6.59) is independently significant: it says the positively homogeneous special case of M-convex function theory — which is what directional derivatives of any M-convex function reduce to, by Proposition 6.60 — is exactly as rich as ordinary shortest-path distance function theory, no more and no less, so nothing new needs to be built to understand local behavior at a point.

None of these results are open — they are Murota's account of how the discrete exchange axiom interacts with directional differentiation and subgradients, a bridge chapter between the purely combinatorial theory of chapters 4-6 and the duality theory of chapter 8. What this mission contributes is a faithful, machine-checked formal statement of each, extending the shared Lean vocabulary (MExchangeAxiomR, DirDeriv, GammaHat) the Discrete Convex Analysis series builds on; no comparable formalization exists on the platform (see Formalization scope).

Difficulty

The naive approach to Theorem 6.61 would try to compute $\partial_{\mathbb R} f(x)$ directly from the definition of subgradient and separately verify it happens to equal some $D(\gamma)$ ; the book's actual proof instead derives the equality of sets from the M-optimality criterion (Theorem 6.52) applied pointwise: $p \in \partial_{\mathbb R} f(x)$ is shown, via a chain of logical equivalences, to be exactly the condition defining $D(\gamma_{f,x})$ , so no separate verification of polyhedrality or nonemptiness is needed beyond what Theorem 6.52 and Proposition 6.60 already supply. The genuine difficulty is upstream, in Proposition 6.60 itself: showing a directional derivative is M-convex requires exploiting the local validity of the identity $f(x+d)-f(x) = f'(x;d)$ for small $\|d\|_1$ (Eq. (6.85)) and then extending the exchange property from that neighborhood to all of $\mathbb R^V$ using positive homogeneity — a two-step argument with no single-step shortcut, since the exchange axiom's defining inequality is not obviously homogeneous-invariant on its own.

Formalization scope

Ground-set elements are a Fintype V with DecidableEq; real-domain functions are (V→ℝ)→WithTop ℝ. The directional derivative is built directly as an infimum of difference quotients over $t>0$ , matching the book's own local characterization (Eq. (6.85)) without a separate limit construction. Positive homogeneity and the classes 0M[R→R]/0M[Z→R] are stated exactly as the book defines them (the latter via positive homogeneity of the convex extension, not of f itself, since f is undefined off Zⱽ). Theorems 6.49-6.50 restate 4 of their 8 operations (matching the identical scope decision for chunk 22-ch06b-mconvexfunctions's Theorem 6.13); Theorem 6.61 omits the dual-integral refinement clauses for the M[R→R|Z]/ M[Z→Z] sub-classes. Both reductions are documented, not trivializing omissions — see Difficulty above and HARD.md/MODERATION_NOTES.md. No numeric constants are hard-coded anywhere in this mission. This mission's definitions are redeclared from chunks 06-mconvex-functions-i, 21-ch05b-lconvexsets (for the distance-function/admissible-potential vocabulary), 22-ch06b-mconvexfunctions, and 23-ch06c-mconvexfunctions rather than imported, since sibling drafts in this series cannot yet reference one another. Contributions completing any of the twelve sorrys are welcome; the goal and Proposition 6.60 carry the most independent proof content.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
K. Murota and A. Shioura, "M-convex function on generalized polymatroid," Mathematics of Operations Research, 24 (1999), pp. 95-105 (the polyhedral M-convex function theory this mission's real-variable results are drawn from).

56 thms2 active usersReviewed

Completed

Numerical Analysis Optimization·Captain: mikedeng1

The Relaxation Method for Linear Inequalities III: Reflexion in a Closed Bounded Convex Set Terminates or Ends in OscillationResearch Paper

Motivation

The relaxation method for a system of linear inequalities, introduced by Agmon and by Motzkin and Schoenberg in back-to-back papers of the Canadian Journal of Mathematics (1954), solves $\sum_j a_{ij}x_j + b_i \ge 0$ by repeatedly moving a point towards, or across, the most violated half-space. It is the ancestor of the perceptron algorithm, of Kaczmarz-type projection methods, and of the method of alternating projections, all of which are still used in feasibility problems, tomography and machine learning.

Motzkin and Schoenberg's paper ends (Part IV, §§9–10) by asking whether the behaviour of the reflexion process — the relaxation step with factor $\lambda = 2$ — survives when the finite family of half-spaces is replaced by an infinite one. They answer this for one natural infinite family: all supporting half-spaces of a closed bounded convex set. This mission formalizes that answer, Theorem 3 of the paper.

Timeline of the thread this mission belongs to:

1922 — Fejér observes that a sequence approaching every point of a set monotonically has useful convergence properties (Fejér, Math. Annalen 85, 1922).
1954 — Agmon proves convergence of the relaxation method for $0 < \lambda < 2$ (Agmon, Canad. J. Math. 6, 1954, pp. 382–392); Motzkin and Schoenberg prove finite termination of the reflexion method ( $\lambda = 2$ ) for full-dimensional solution polytopes (Theorem 1), the oscillation behaviour in lower dimension (Theorem 2), and the convex-body version (Theorem 3) (Motzkin–Schoenberg 1954).

Setting

Let $E_n$ be $n$ -dimensional Euclidean space and let $A \subseteq E_n$ be a nonempty, closed, bounded, convex set. Its dimension $r$ is the dimension of its affine span $L_r$ , the smallest flat containing $A$ .

For $p \notin A$ let $q$ be the point of $A$ nearest to $p$ ; it exists and is unique. The image of $p$ with respect to $A$ is

p_1 = F(p) = p + 2(q - p), \qquad (3.1)

the reflexion of $p$ through $q$ . The reflexion process starts at $p_0 \notin A$ and sets $p_{\nu+1} = F(p_\nu)$ as long as $p_\nu \notin A$ (3.2). Either the process terminates with some $p_N \in A$ , or it produces an infinite sequence of points outside $A$ .

The family $F$ of supporting half-spaces of $A$ consists of the closed half-spaces $H \supseteq A$ whose bounding hyperplane touches $A$ . The paper observes that the half-space $H_0$ through $q$ normal to $pq$ is the member of $F$ farthest from $p$ , so (3.1) is exactly the reflexion step of the relaxation method applied to the infinite family $F$ .

A sequence $\{q_\nu\}$ of points outside $A$ is Fejér-monotone with respect to $A$ if $q_\nu \ne q_{\nu+1}$ and $|q_{\nu+1} - a| \le |q_\nu - a|$ for all $a \in A$ . Two points $u, v$ are symmetric with respect to a flat $L$ if their midpoint lies in $L$ and $u - v$ is orthogonal to $L$ .

Formalization targets

Goal: Theorem 3 (p. 402)

For every nonempty closed bounded convex $A \subseteq E_n$ with affine span $L_r$ , every $p_0 \notin A$ and every run $\{p_\nu\}$ of the reflexion process:

\textbf{Case 1: } r = n \implies \exists N,\ p_N \in A.

\textbf{Case 2: } r < n \implies \begin{cases} p_0 \in L_r \implies \exists N,\ p_N \in A,\\[2pt] p_0 \notin L_r \implies p_\nu \notin A\ \forall \nu, \text{ and } \exists \nu_0, u \ne v \text{ symmetric w.r.t. } L_r:\ \{p_\nu, p_{\nu+1}\} = \{u, v\}\ \forall \nu > \nu_0. \end{cases}

No number of steps is fixed: termination is finite but not uniformly bounded.

Milestones (attack order)

§9 — the half-space $H_0$ belongs to $F$ , maximizes $\operatorname{dist}(p, H)$ over $F$ , and every farthest member of $F$ yields the step (3.1).
§10 — an infinite run of the reflexion process is Fejér-monotone with respect to $A$ .
Lemma 1, Case 1 — a sequence Fejér-monotone with respect to a set of dimension $n$ converges to a point.
§10 — the limit of an infinite run lies in $A$ and on its boundary.
Theorem 3, Case 1 — if $r = n$ the process always terminates.
§10 — orthogonal projection on a flat $L \supseteq A$ commutes with the image map, and each step keeps the distance to $L$ while switching sides.

Significance

The result. Theorem 3 shows that the dichotomy proved in the paper for finitely many half-spaces — finite termination when the target is full-dimensional, eventual oscillation otherwise — holds for the infinite family of all supporting half-spaces of a convex body. Case 1 says that reflecting through the nearest point, a method that uses no information about $A$ beyond metric projection, reaches a full-dimensional convex body in finitely many steps from any start. Case 2 says that for a lower-dimensional body the process detects this: the iterates settle into a two-cycle whose midpoint is a point of $A$ , so a solution can be read off.

Formalizing it. The theorem is proved in the paper (1954), with a short proof of Case 1 that relies on geometric intuition about normal cones near a boundary point. To our knowledge no machine-checked proof exists. A complete development produces a verified finite-termination theorem for a projection method on general convex bodies, together with reusable facts about Fejér-monotone sequences and metric projections that recur throughout the analysis of projection algorithms.

Difficulty

The obvious argument for Case 1 is: the run is Fejér-monotone, hence converges (Lemma 1), and its limit $a$ lies on the boundary of $A$ ; then derive a contradiction. For a polytope (Theorem 1) the contradiction comes from finiteness: eventually every reflexion is in one of finitely many hyperplanes through $a$ , which keeps the iterates on a sphere around $a$ . For a convex body there are infinitely many supporting hyperplanes near $a$ , and the iterates are reflected in a different one at every step; no finiteness argument is available. What replaces finiteness is an argument about how the supporting hyperplanes of $A$ at boundary points near $a$ are oriented, and the paper gives it only as an informal geometric sketch. Making this step rigorous is the main work of the mission.

Numerical experiments show that termination can take tens of thousands of steps near sharp corners of a polygon, so no bound on the number of steps in terms of the distance of $p_0$ to $A$ alone can be expected.

Formalization scope

Space. $E_n$ is EuclideanSpace ℝ (Fin n). $A$ is a Set with four explicit hypotheses: A.Nonempty, IsClosed A, Convex ℝ A, Bornology.IsBounded A. Nonemptiness is implicit in the paper ("of dimension $r$ ", "the point of $A$ nearest to $p$ ").
The image as a relation. IsImage A p p₁ holds when $p_1 = p + 2(q - p)$ for a nearest point $q$ of $A$ ; the nearest point is not chosen by a function. For closed convex nonempty $A$ this relation is a function on $E_n$ . A run is any sequence with IsImage A (p ν) (p (ν+1)) whenever p ν ∉ A; values after entering $A$ are unconstrained. Every statement quantifies over every run from every $p_0 \notin A$ ; a formalization that only asserts the existence of some terminating run is ruled out.
Dimension. $L_r$ is affineSpan ℝ A; $r = n$ is affineSpan ℝ A = ⊤, $r < n$ is affineSpan ℝ A ≠ ⊤. No separate natural number $r$ is introduced.
Symmetry. IsSymmetricWrt L u v: midpoint ℝ u v ∈ L and u - v orthogonal to L.direction. For $r < n - 1$ this is a point reflection through the foot of the perpendicular, not a reflection in a hyperplane. The goal also requires $u \ne v$ and strict alternation $p_\nu \leftrightarrow p_{\nu+1}$ for $\nu > \nu_0$ (strict inequality, as printed).
Boundary is frontier A; distances to sets are Metric.infDist.
Generalizations recorded. Lemma 1, Case 1 is stated for an arbitrary set $A \subseteq E_n$ with full affine span (the paper states it for the polytope of (1.4) and applies it in §10 to a convex body). The projection milestone is stated for any flat $L \supseteq A$ , not only after the paper's reduction to $r = n - 1$ . The §9 milestone expresses "the reflexion process with respect to $F$ amounts to (3.1)" as: every farthest member of $F$ , with any nearest point on it, gives the same step.
Duplication. Case 1 appears both as a milestone and inside the goal, because the paper's proof of Case 2 cites Case 1. Solvers will need to transfer Case 1 from $E_n$ to the flat $L_r$ (an isometric copy of $E_r$ ).
Infrastructure. Mathlib's metric projection onto complete convex sets (exists_norm_eq_iInf_of_complete_convex, norm_eq_iInf_iff_real_inner_le_zero) and EuclideanGeometry.orthogonalProjection cover the basic geometry. Normal cones of convex sets and their upper semicontinuity are not in Mathlib; a contribution there is reusable well beyond this mission. Proofs of any milestone, and alternative proofs of Case 1, are welcome.

Selected references

T. S. Motzkin and 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
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954), 382–392 (the companion paper in the same issue).
L. Fejér, Über die Lage der Nullstellen von Polynomen, die aus Minimumforderungen gewisser Art entspringen, Mathematische Annalen 85 (1922), 41–48.

11 thms2 active usersReviewed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis VI: Quasi M-Convex Functions and the Quasi-Proximity TheoremTextbook

Motivation

Convexity is normally defined additively — a function's value at a mixture is bounded by the mixture of its values — but many of the properties that make convexity useful in optimization (a local minimum is global, level sets are well-behaved) survive under a much weaker, purely ordinal notion: quasi-convexity, which compares function values rather than adding them. A nondecreasing rescaling of a convex function is generally not convex, but it is always quasi-convex — so a theory built only on ordinal comparisons automatically covers every such rescaling for free, at the cost of a more delicate proof architecture (since the algebraic cancellations available to additive convexity are no longer available).

Chapter 6's second half asks exactly how far this idea extends in the discrete setting: does the M-convexity exchange axiom have an ordinal, quasi-convex relaxation that still supports the same strong minimization theory — an optimality criterion, a minimizer-cut lemma, and, most significantly, a proximity theorem with the same explicit distance bound? This mission formalizes the chapter's answer: yes, and the relevant relaxed class, functions satisfying condition (SSQM $_{\ne}$ ), is large enough to include every strictly increasing rescaling of an M-convex function, a class the M-convex theory of chunk 06 alone says nothing about.

Setting

Let $V$ be a finite ground set and $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ with nonempty effective domain. Building on chunk 06's M-convex exchange axiom (M-EXC[Z]), this chapter introduces several ordinal relaxations. $f$ is weakly quasi M-convex, satisfying (QMw), if for every pair of distinct points $x, y \in \operatorname{dom} f$ there exist $u$ in the positive support and $v$ in the negative support of $x - y$ with $f(x - \chi_u + \chi_v) \le f(x)$ or $f(y + \chi_u - \chi_v) \le f(y)$ — an "or" where (M-EXC[Z]) demands an additive inequality. Two further conditions restrict attention to points of different function value and sharpen the conclusion to a three-way trichotomy (strictly better on one side, or exactly tied on both): (SSQM $_{\ne}$ ) quantifies universally over $u$ (as in (M-EXC[Z])), while (SSQM $_{\ne,w}$ ) quantifies existentially over both $u$ and $v$ (as in (QMw)). The linear perturbation of $f$ by $p : V \to \mathbb R$ is $f[p](x) = f(x) - \langle p, x \rangle$ .

Formalization targets

Goal: Theorem 6.78 (the quasi M-proximity theorem)

Let $f$ satisfy (SSQM $_{\ne}$ ), $n = |V|$ , $\alpha$ a positive integer. If $x_\alpha \in \operatorname{dom} f$ satisfies $f(x_\alpha) \le f(x_\alpha + \alpha(\chi_v - \chi_u))$ for all $u, v \in V$ , then $\arg\min f \ne \emptyset$ and there is $x^* \in \arg\min f$ with $\|x_\alpha - x^*\|_\infty \le (n-1)(\alpha - 1)$ — verbatim the same conclusion, and the same exact bound, as chunk 06's Theorem 6.37(1), now established for the strictly larger class satisfying (SSQM $_{\ne}$ ) rather than the M-convex exchange axiom itself.

Milestones: Theorems 6.68(2), 6.76, 6.77

Theorem 6.68(2): $f$ satisfies (M-EXC[Z]) if and only if every linear perturbation $f[p]$ satisfies (QMw) — quantifying exactly how much weaker (QMw) is pointwise, and how the gap closes once quantified over every perturbation. Theorem 6.76 (the quasi M-optimality criterion): the direct analogue of chunk 06's Theorem 6.26 for the quasi-convexity classes — a purely pairwise local check still characterizes global (or, in the (QMw) case, strict unique) optimality. Theorem 6.77 (the quasi M-minimizer cut): chunk 06's Theorem 6.28 continues to hold verbatim when its M-convexity hypothesis is replaced by (SSQM $_{\ne}$ ) — the structural fact the proximity theorem's proof is built from survives the relaxation intact.

Significance

The result itself. The proximity theorem is the result algorithms actually use: a scaling algorithm for minimizing quasi-convex functions of this kind inherits exactly the same correctness guarantee, with exactly the same distance bound, as the M-convex case — this is a genuine broadening of chapter 10's algorithmic reach, not a restatement dressed in weaker hypotheses. Every strictly increasing scalar transformation of an M-convex objective (a common modeling device — re-expressing a cost in utility units, or applying a monotone risk measure) now falls under a proximity theorem, whereas prior to this chapter's relaxation such a transformation would generally destroy M-convexity itself and leave optimization theory silent on the transformed problem.

Formalizing it. No matching item exists on the platform for quasi M-convexity in any of its forms. Formalizing Theorem 6.78 requires first pinning down (SSQM $_{\ne}$ ) exactly (there are six closely related axiom variants in this section of the book, only three of which — (QMw), (SSQM $_{\ne}$ ), (SSQM $_{\ne,w}$ ) — are needed for this mission's chosen results), and this mission also captures, via Theorem 6.68(2), the precise sense in which these relaxed conditions are strictly weaker than plain M-convexity while remaining tightly connected to it.

Difficulty

The natural first instinct, given how close the quasi-convexity axioms look to (M-EXC[Z]), is to try to prove Theorem 6.78 by directly imitating chunk 06's proof of Theorem 6.37 line by line. This mostly works — the proof structure (fix a target coordinate, build a chain of strictly decreasing values via repeated exchange steps, bound the chain's length using the scaled hypothesis) survives verbatim — but every step that chunk 06's proof took by adding two instances of the exchange inequality together must be replaced by an ordinal argument, since (SSQM $_{\ne}$ ) only ever asserts a disjunction of value comparisons, never an additive inequality relating four function values simultaneously the way (M-EXC[Z])'s $f(x)+f(y) \ge f(x-\chi_u+\chi_v)+f(y+\chi_u-\chi_v)$ does. The book's proof handles this by working with strict inequalities and the trichotomy structure of (SSQM $_{\ne}$ ) directly rather than algebraic cancellation — the same overall architecture, but every arithmetic step rebuilt as a case analysis on which disjunct of (SSQM $_{\ne}$ ) fires.

Formalization scope

This mission builds directly on chunk 06's published items (CharVec, SuppPos, SuppNeg, DomZ, MExchangeAxiom, ArgMin), per the platform's textbook convention that a later chapter of the same book imports an earlier one's definitions rather than redrafting them; its own namespace DiscreteConvex.MConvexFunctions.Quasi nests under chunk 06's DiscreteConvex.MConvexFunctions accordingly. Δf(z;v,u) (Eq. (6.2)) is never reified as a separate object; every occurrence is unfolded directly into an f-value comparison, avoiding WithTop ℝ subtraction throughout, consistent with chunk 06's own convention.

A trivializing formalization of the goal would silently strengthen (SSQM $_{\ne}$ ) back to plain M-convexity (making this mission redundant with chunk 06's Theorem 6.37) or loosen the exact bound $(n-1)(\alpha-1)$ to an unspecified function of $n, \alpha$ ; neither is done. Six axiom variants appear in this section of the book ((QM), (SSQM), (QMw), (SSQM $_w$ ), (SSQM $_{\ne}$ ), (SSQM $_{\ne,w}$ )); only the three actually needed by this mission's four items are drafted, and Theorem 6.68's first part (an implication chain among the other three) is left out — see MODERATION_NOTES.md. Contributions building the polyhedral M-convex-function bridge (§6.11–6.12, Theorems 6.59–6.64), the level-set characterizations (Theorems 6.72, 6.74), or the scaled quasi M-minimizer cut (Theorem 6.79, the direct generalization of Theorem 6.77 drafted here) are welcome.

Selected references

K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
M. Avriel, W. E. Diewert, S. Schaible, I. Zang, Generalized Concavity, Plenum Press, 1988.

8 thms2 active usersReviewed

Convex Optimization

Missions

Stability and Generalization 3: Tikhonov Regularization in a Reproducing Kernel Hilbert Space Has Uniform Stability σ²κ²/(2λm)Research Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

The Rate of Convergence of Nesterov's Accelerated Forward-Backward Method is Actually Faster than 1/k^2 I: For α > 3, (Ψ + Φ)(x_k) − min(Ψ + Φ) = o(k⁻²) and ‖x_{k+1} − x_k‖ = o(k⁻¹)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 2)

Milestones (in attack order)

Significance

Difficulty

Formalization scope

Selected references

Understanding and Using Linear Programming XI: The KKT Conditions and the Unique Smallest Enclosing BallTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 8.7.4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Numerical Techniques for Stochastic Optimization IV: Nonstationary Optimization and a Convergence Criterion for Nonmonotone SequencesTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 6.3 (pp. 153–154)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Decoding by Linear Programming: Exact Recovery by ℓ1 Minimization under the Restricted Isometry ConditionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1.5 (decoding by linear programming)

Core: Theorem 1.4 (exact recovery by ℓ1\ell^1ℓ1 minimization)

Significance

Difficulty

Formalization scope

Selected references

Analysis and Algorithms for Service Parts Supply Chains VIII: Bounds on Optimal Stock AllocationsTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 15 (p. 237)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Value of Information in Bayesian Routing Games II: Equilibrium Adoption Rates of Information Systems Are the Minimizers of the Equilibrium PotentialResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4

Milestones

Significance

Difficulty

Formalization scope

Selected references

Value of Information in Bayesian Routing Games I: Sign and Monotonicity of the Relative Value of Information Across Size RegimesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Core: Theorem 1.4 (exact recovery by $\ell^1$ minimization)