Optimization

Motivation

A chance-constrained program minimizes a cost $f(x)$ over a closed set $X\subseteq\mathbb R^n$ subject to a constraint that must hold with high probability rather than surely:

$$\min_{x\in X} f(x)\quad\text{s.t.}\quad \mathbb P\bigl(C(x,\xi)\le 0\bigr)\ge 1-\alpha,$$

where $\xi$ is a random vector, $C(x,\xi)=\max_j c_j(x,\xi)$ collects the uncertain constraints, and $\alpha\in(0,1)$ is the tolerated risk. Such models are used in power-system dispatch, portfolio selection, and supply-chain and process design, wherever a constraint may be violated in rare scenarios at a controlled rate.

The probability is rarely computable, so in practice it is replaced by an estimate from an i.i.d. sample $\xi_1,\dots,\xi_N$. The empirical frequency is a step function of $x$ and yields a mixed-integer program. Peña-Ordieres, Luedtke and Wächter (arXiv:1905.07377v2; SIAM J. Optim. 30(3), 2020) replace the indicator by a smooth approximation, which turns the sample problem into a smooth nonlinear program that standard solvers can handle. The question this mission addresses is whether a point accepted by the smoothed sample problem is actually feasible for the true chance constraint, and with what probability.

Timeline. Luedtke and Ahmed (SIAM J. Optim. 19 (2008)) proved finite-sample feasibility guarantees for the empirical (non-smooth) sample approximation, first for finite $X$ and then, under a Lipschitz condition on $C$, for bounded $X$ (their Theorem 10). Peña-Ordieres, Luedtke and Wächter (2020) extended these guarantees to the smoothed approximation (Theorems 3.8, 3.11 and 3.13 of the preprint).

Setting

Let $\varepsilon>0$ and let $\gamma_\varepsilon:[-\varepsilon,\varepsilon]\to[0,1]$ be admissible: strictly decreasing, symmetric in the sense $\gamma_\varepsilon(-y)=1-\gamma_\varepsilon(y)$, and such that the smoothed indicator

$$\Gamma_\varepsilon(y)=\begin{cases}1& y\le-\varepsilon\\ \gamma_\varepsilon(y)&-\varepsilon<y<\varepsilon\\ 0& y\ge\varepsilon\end{cases}$$

is differentiable on $\mathbb R$. The paper's concrete choice is a quartic-kernel polynomial (its (2.6)).

For a decision $x$ and a level $t$, define

• the true cdf $F(t;x)=\mathbb P(C(x,\xi)\le t)$;
• the smoothed cdf $F_\varepsilon(t;x)=\int\Gamma_\varepsilon(C(x,\xi)-t)\,d\mathbb P_\xi$;
• the smoothed sample cdf $F^N_\varepsilon(t;x)=\frac1N\sum_{i=1}^N\Gamma_\varepsilon(C(x,\xi_i)-t)$.

The true feasible set is $X_\alpha=\{x\in X\mid F(0;x)\ge1-\alpha\}$, and the shifted sample feasible set with shift $t$ and sample risk level $\delta$ is

$$X^{N,t}_{\varepsilon,\delta}=\{x\in X\mid F^N_\varepsilon(-t;x)\ge 1-\delta\}.$$

Throughout, $C(x,\xi)$ has a continuous distribution for each $x\in X$ (Assumption 3.1). The margin of a point is $M_x=F(0;x)-F_\varepsilon(-t;x)+(\alpha-\delta)$; Assumption 3.7 asks that $\delta\in[0,\alpha]$ and $M:=\inf_{x\in X}M_x>0$.

Formalization targets

Goal: Theorem 3.13

Suppose $X$ is bounded with sup-norm diameter $D$, that $|C(x,\xi)-C(y,\xi)|\le L\|x-y\|_\infty$ for all $x,y\in X$ with probability one (Assumption 3.12), and that Assumption 3.7 holds with $t>0$ and $\delta>0$. Then for every $\beta\in(0,\delta]$,

$$\mathbb P\bigl(X^{N,2t}_{\varepsilon,(\delta-\beta)}\subseteq X_\alpha\bigr)\ge 1-\lceil1/\beta\rceil\,\lceil 2LD/t\rceil^n\exp\{-2NM^2\}.$$

Milestones

1. Theorem 3.8. For $x\in X\setminus X_\alpha$, $\ \mathbb P(F^N_\varepsilon(-t;x)\ge1-\delta)\le\exp\{-2NM_x^2\}$.
2. Theorem 3.11. For finite $X$, $\ \mathbb P(X^{N,t}_{\varepsilon,\delta}\subseteq X_\alpha)\ge 1-|X\setminus X_\alpha|\exp\{-2NM^2\}$.
3. The net claim (proof of Theorem 3.13). Each slice $X_j$ of $X$ by the value of $F(0;\cdot)$ at resolution $1/\lceil1/\beta\rceil$ has a finite subset $Z_j$ with $|Z_j|\le\lceil2LD/t\rceil^n$ that is a $t/L$-net of $X_j$ in $\|\cdot\|_\infty$.
4. (3.5). Theorem 3.11 applied to the net $Z$ with levels $\alpha-\beta$ and $\delta-\beta$.
5. The transfer step. $x\in X^{N,2t}_{\varepsilon,(\delta-\beta)}$ and $\|x-z\|_\infty\le t/L$ imply $F^N_\varepsilon(-t;z)\ge1-\delta+\beta$.
6. Corollary 3.9 (companion). If $C(x,\xi)$ has a density strictly decreasing on $(-\varepsilon,\varepsilon)$ and $F(0;x)<1-\alpha$, then $\beta_x=F(0;x)-F_\varepsilon(0;x)>0$ and $\mathbb P(F^N_\varepsilon(0;x)\ge1-\alpha)\le\exp\{-2N\beta_x^2\}$.

Significance

The result. Theorem 3.13 gives an explicit, non-asymptotic sample size $N$ under which every point accepted by the smoothed sample problem (with a small shift $2t$ and a slightly tightened risk level $\delta-\beta$) is feasible for the original chance constraint, uniformly over an infinite decision set. Solving the smooth approximation therefore yields certifiably feasible solutions with a quantified failure probability, the bound depending on the dimension $n$ only through the covering number $\lceil 2LD/t\rceil^n$. Corollary 3.9 adds that, under a monotone density near zero, the unshifted smoothed approximation is conservative.

Formalizing it. The results are proved in the paper; none is formalized anywhere to our knowledge. A formal development would produce a machine-checked one-sided Hoeffding bound for averages of bounded functions of an i.i.d. sample, a union bound over a finite candidate set, and a sup-norm covering lemma, assembled into a uniform feasibility guarantee. These ingredients are reused across the sample-average-approximation literature.

Difficulty

The obvious argument is a union bound over $X$, which fails for infinite $X$: the event $X^{N,2t}_{\varepsilon,(\delta-\beta)}\subseteq X_\alpha$ involves uncountably many points, and is not even obviously measurable. Discretizing $X$ by a sup-norm grid is not enough on its own either: a grid point may be infeasible while nearby points are feasible, and the true cdf $F(0;\cdot)$ need not be continuous in $x$. The paper's device is to discretize simultaneously in $x$ and in the value of $F(0;x)$, which requires covering each level slice separately and then transferring sample feasibility from a point to its representative, at the price of the shift $2t\to t$ and the level change $\delta\to\delta-\beta$. Keeping the constants exactly as printed, with $\lceil1/\beta\rceil$ slices and $\lceil 2LD/t\rceil^n$ points per slice, is part of the task.

Formalization scope

• Decisions are Fin n → ℝ, whose Mathlib norm is the sup norm $\|\cdot\|_\infty$ used in Assumption 3.12 and Theorem 3.13. $X$ is closed (the paper's standing hypothesis).
• $\xi$ takes values in a measurable space $\Xi$ with probability law $\mathbb P_\xi$. The sample is $N\ge1$ measurable maps $\xi_i:\Omega\to\Xi$ on a probability space, mutually independent, each with law $\mathbb P_\xi$. $C(x,\cdot)$ is assumed measurable for $x\in X$ (a disclosed addition: it makes $C(x,\xi)$ a random variable). Assumption 3.1 is encoded as $\mathbb P_\xi(C(x,\xi)=y)=0$ for all $y$.
• Statements of the form "$\mathbb P(A)\ge1-b$" are stated as $\mathbb P(\text{not }A)\le b$ with $\mathbb P$ evaluated as an outer measure; this implies the printed form and assumes no measurability of the event.
• Assumption 3.7's infimum $M$ is a parameter with $M>0$ and $M\le M_x$ on $X$, equivalent to the infimum because the bounds decrease in $M$.
• "Bounded with diameter $D$" is $\|x-y\|_\infty\le D$ on $X$ with $D>0$. Positivity is necessary: for a single infeasible point and $n\ge1$ the printed bound with $D=0$ would read $\mathbb P\ge1$.
• A formalization in which these hypotheses are unsatisfiable, the event is assumed measurable, or $M$ is a junk infimum is ruled out: a sorry-free sanity file exhibits the quartic kernel (2.6) as admissible and a one-point instance meeting the goal's diameter and margin hypotheses.
• Not posed: Hoeffding's inequality (Theorem 3.6), whose one-sided form is in Mathlib (ProbabilityTheory.measure_sum_ge_le_of_iIndepFun with hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero); and Corollary 3.10, whose printed exponent does not follow from its proof.

Contributions welcome: proofs of any milestone, in particular the sup-norm covering lemma and the Hoeffding step, which are reusable beyond this mission.

Selected references

• A. Peña-Ordieres, J. R. Luedtke, A. Wächter, Solving chance-constrained problems via a smooth sample-based nonlinear approximation, SIAM J. Optim. 30(3), 2020; preprint arXiv:1905.07377v2. https://arxiv.org/abs/1905.07377 , https://doi.org/10.1137/19M1261985
• J. Luedtke, S. Ahmed, A sample approximation approach for optimization with probabilistic constraints, SIAM J. Optim. 19(2), 2008. https://doi.org/10.1137/070702928
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58, 1963. https://doi.org/10.1080/01621459.1963.10500830

Monotone inclusions and the cost of splitting

Many problems in convex optimization, variational inequalities and saddle-point computation can be written as a monotone inclusion: find $x$ in a real Hilbert space $H$ with

$$0 \in (A+B)(x),$$

where $A$ is a set-valued maximally monotone operator (a subdifferential, a normal cone, a constraint) and $B$ is a single-valued monotone operator (a gradient, or the skew operator of a saddle-point problem). Splitting methods solve such problems using $A$ and $B$ separately: a backward step evaluates the resolvent $J_{\lambda A}=(I+\lambda A)^{-1}$, and a forward step evaluates $B$.

The classical forward-backward method $x_{k+1}=J_{\lambda A}(x_k-\lambda B(x_k))$ converges when $B$ is cocoercive, but can fail when $B$ is merely monotone and Lipschitz, which is the case for saddle-point operators such as $B(z_1,z_2)=(z_2,-z_1)$. Tseng's forward-backward-forward method (Tseng 2000) removes the cocoercivity assumption at the price of two evaluations of $B$ per iteration. Malitsky and Tam (arXiv:1808.04162; SIAM J. Optim. 30(2), 2020) propose the forward-reflected-backward method, which needs one evaluation of $B$ and one resolvent of $A$ per iteration, reusing the previous value of $B$.

Timeline of the relevant results:

• 1967: Opial's lemma on weak convergence of sequences in Hilbert space (Opial 1967).
• 1979: Lions and Mercier analyse forward-backward splitting with cocoercive $B$ (Lions–Mercier 1979).
• 1980: Popov's modified Arrow–Hurwicz method for saddle points, with one operator evaluation per step (Popov 1980).
• 2000: Tseng's forward-backward-forward method for monotone and Lipschitz $B$.
• 2015: Malitsky's projected reflected gradient method for variational inequalities (Malitsky 2015), the special case $A=N_C$, $B$ affine.
• 2018–2020: Malitsky and Tam, the forward-reflected-backward method, Theorem 2.5.

Setting

$H$ is a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$. A set-valued operator $A:H\rightrightarrows H$ is monotone if $\langle x-y,u-v\rangle\ge 0$ whenever $u\in A(x)$, $v\in A(y)$, and maximally monotone if its graph is not properly contained in the graph of another monotone operator. Its resolvent $J_{\lambda A}=(I+\lambda A)^{-1}$ is, for $\lambda>0$ and $A$ maximally monotone, an everywhere defined single-valued map, characterised by $\lambda^{-1}(w-J_{\lambda A}w)\in A(J_{\lambda A}w)$. A map $B:H\to H$ is $L$-Lipschitz if $\|B(x)-B(y)\|\le L\|x-y\|$, and monotone if $\langle x-y,B(x)-B(y)\rangle\ge0$.

The zero set is $(A+B)^{-1}(0)=\{x : -B(x)\in A(x)\}$. Given initial points $x_0,x_{-1}\in H$ and step sizes $(\lambda_k)_{k\ge-1}$, the forward-reflected-backward method is

$$x_{k+1}=J_{\lambda_k A}\big(x_k-\lambda_k B(x_k)-\lambda_{k-1}(B(x_k)-B(x_{k-1}))\big)\qquad\forall k\in\mathbb N. \tag{13}$$

A sequence $(x_k)$ converges weakly to $\bar x$ if $\langle x_k,v\rangle\to\langle\bar x,v\rangle$ for every $v\in H$; a sequential weak cluster point is the weak limit of a subsequence.

Formalization targets

Goal: Theorem 2.5 (p. 6)

If $A$ is maximally monotone, $B$ is monotone and $L$-Lipschitz, $(A+B)^{-1}(0)\ne\varnothing$, and $(\lambda_k)\subseteq[\varepsilon,\tfrac{1-2\varepsilon}{2L}]$ for some $\varepsilon>0$, then every sequence generated by (13) satisfies

$$x_k\rightharpoonup\bar x\quad\text{for some }\bar x\in(A+B)^{-1}(0).$$

Milestones

In attack order:

1. Proposition 2.3, the basic inequality (19) for one resolvent step.
2. Lemma 2.4, the energy inequality (20).
3. The telescoped bound after (24).
4. Boundedness of $(x_k)$ and $\|x_k-x_{k+1}\|\to0$.
5. Weak cluster points lie in the zero set.
6. Convergence of the energy (26).
7. Its limit equals $\lim\|x_k-\bar x\|^2$.
8. Lemma 2.2, an Opial-type criterion for weak convergence.

Corollary 2.6, the constant-step case $\lambda\in(0,\tfrac1{2L})$, is included as a companion theorem.

Significance

Theorem 2.5 shows that monotone inclusions with a Lipschitz, non-cocoercive single-valued part can be solved by a splitting method with the per-iteration cost of forward-backward splitting: one forward and one backward evaluation. For saddle-point problems, where each evaluation of $B$ is a pair of matrix–vector products, this halves the operator cost of Tseng's method. The method contains the projected reflected gradient method and, for $A=0$, Popov's method and the optimistic gradient method used in training generative adversarial networks (Remark 2.1). The analysis of this section is reused for the linear rate, the linesearch, the inertial variant and the three-operator variant of later sections (missions 2–5 of this series).

The theorem is proved in the paper. Formalizing it requires a machine-checked Opial-type lemma and a machine-checked demiclosedness argument for maximally monotone operators perturbed by a continuous monotone map, both reusable well beyond this mission. To our knowledge no machine-checked proof of convergence of the forward-reflected-backward method exists.

Difficulty

The energy inequality of Lemma 2.4 is algebra plus monotonicity and the Lipschitz estimate, and it yields boundedness and $\|x_{k+1}-x_k\|\to0$. The difficulty lies in passing from these facts to weak convergence of the whole sequence. Norm convergence is false in general, so a Cauchy-sequence argument is unavailable. The energy is not Fejér monotone in $\|x_k-x\|$ alone, because of the cross term $2\lambda_{k-1}\langle B(x_k)-B(x_{k-1}),x-x_k\rangle$, so the standard Fejér/Opial lemma does not apply directly. Identifying weak cluster points as zeros requires the weak-strong closedness of the graph of $A+B$, which in turn rests on maximal monotonicity of the sum: this is not a consequence of monotonicity of the two parts, and the inclusion (25) can be passed to the limit only because the step sizes stay above $\varepsilon$.

Formalization scope

The Lean development uses a real inner product space H (InnerProductSpace ℝ H), complete wherever the page needs it, and the published operator vocabulary ThreeOpSplitting.Accel.MonotoneOperators (monotone and maximally monotone set-valued operators, monotone and Lipschitz single-valued maps, resolvents). Conventions:

• Resolvents are hypotheses. The iteration is driven by a family $J:\mathbb R\to H\to H$ with $\gamma^{-1}(w-J(\gamma)w)\in A(J(\gamma)w)$ for all $\gamma>0$, $w\in H$; for maximally monotone $A$ such a family exists and is unique. The goal keeps maximal monotonicity of $A$ as a hypothesis as well.
• Index shift. Lean's x j is $x_{j-1}$ and lam j is $\lambda_{j-1}$; the initial points are arbitrary.
• Step range. Every $\lambda_j$, $j\ge-1$, lies in $[\varepsilon,(1-2\varepsilon)/(2L)]$, including $\lambda_{-1}$ as on p. 4. $L>0$ is assumed, since the range divides by $L$.
• Weak convergence is convergence of $\langle x_k,v\rangle$ for every $v$; cluster points are sequential weak cluster points (subsequences along strictly increasing index maps).
• Several milestones are stated in a stronger form than the page, with $A$ only monotone, $H$ not complete, or a conclusion for every zero rather than the cluster point. Each item's note says which.

Three formalizations would trivialize the goal and are excluded:

• an unconstrained resolvent map;
• norm convergence or convergence of a subsequence in place of weak convergence of the whole sequence;
• a step range shrunk or pinned to a constant.

A complete development needs the Opial-type Lemma 2.2, which in turn needs weak sequential compactness of bounded sets in Hilbert space, and maximal monotonicity of $A+B$ for continuous monotone $B$ (Bauschke–Combettes, Corollaries 20.25 and 24.4(i)) with its demiclosedness (Proposition 20.33). These are general results of monotone operator theory, and contributions of them as separate theorems are welcome.

Selected references

• Y. Malitsky and M. K. Tam, A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity, SIAM J. Optim. 30(2), 2020; arXiv:1808.04162v4. https://arxiv.org/abs/1808.04162v4 (DOI https://doi.org/10.1137/18M1207260)
• H. H. Bauschke and 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
• P. Tseng, A modified forward-backward splitting method for maximal monotone mappings, SIAM J. Control Optim. 38(2), 2000. https://doi.org/10.1137/S0363012998338806
• Y. Malitsky, Projected reflected gradient methods for monotone variational inequalities, SIAM J. Optim. 25(1), 2015. https://doi.org/10.1137/14097238X
• L. D. Popov, A modification of the Arrow–Hurwicz method for search of saddle points, Math. Notes 28, 1980. https://doi.org/10.1007/BF01141092
• P.-L. Lions and B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM J. Numer. Anal. 16(6), 1979. https://doi.org/10.1137/0716071
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bull. Amer. Math. Soc. 73, 1967. https://doi.org/10.1090/S0002-9904-1967-11761-0

Motivation

First-order methods (projected gradient, fast gradient, feasible descent) converge linearly on smooth strongly convex problems, but many problems met in practice are not strongly convex: least squares with a rank-deficient matrix, the dual of a linearly constrained problem, or $g(Ax)$ with $g$ strongly convex and $A$ singular. Such problems have a whole set of minimisers, and strong convexity, which forces a unique minimiser, fails. Necoara, Nesterov and Glineur (arXiv:1504.06298; Math. Program. 175 (2019)) introduce a family of conditions that relax strong convexity by testing it only against the projection onto the optimal set, and prove that the classical first-order methods still converge linearly under them.

Related unconstrained conditions predate the paper: restricted strong convexity for $X=\mathbb R^n$ (Zhang and Cheng, Optim. Lett. 2015, the paper's reference [16]), and the error bounds of Luo and Tseng (1993). Karimi, Nutini and Schmidt (arXiv:1608.04636, 2016) compared similar unconstrained conditions with the Polyak–Łojasiewicz inequality. The constrained hierarchy treated here, with one constant along the whole chain, is the first section of the Necoara–Nesterov–Glineur paper and the basis of its convergence results.

This mission formalizes that hierarchy: Theorem 4 of the paper (arXiv v4, p. 9) and the results it is assembled from.

Setting

Let $X\subseteq\mathbb R^n$ be a closed convex set, with the Euclidean inner product $\langle u,v\rangle=u^\top v$ and norm $\|u\|$. Let $f$ be a convex function on $X$, differentiable at every point of $X$, with gradient $\nabla f$ Lipschitz on $X$ with constant $L_f>0$:

$$\|\nabla f(x)-\nabla f(y)\|\le L_f\|x-y\|\qquad\forall x,y\in X. \tag{1}$$

The optimal set $X^*=\{x\in X: f(x)\le f(y)\ \forall y\in X\}$ is assumed nonempty, and $f^*$ is the optimal value. For $x\in X$, $\bar x=[x]_{X^*}$ denotes the projection of $x$ onto $X^*$: the point of $X^*$ nearest to $x$.

For a constant $\kappa>0$ the paper considers five inequalities, for all $x,y\in X$:

• (7), first-order strong convexity: $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac{\kappa}{2}\|x-y\|^2$;
• (10), quasi-strong convexity: $f^*\ge f(x)+\langle\nabla f(x),\bar x-x\rangle+\frac{\kappa}{2}\|x-\bar x\|^2$;
• (13), quadratic under-approximation: $f(x)\ge f^*+\langle\nabla f(\bar x),x-\bar x\rangle+\frac{\kappa}{2}\|x-\bar x\|^2$;
• (17), quadratic gradient growth: $\langle\nabla f(x)-\nabla f(\bar x),x-\bar x\rangle\ge\kappa\|x-\bar x\|^2$;
• (22), quadratic functional growth: $f(x)-f^*\ge\frac{\kappa}{2}\|x-\bar x\|^2$.

The classes $\mathcal S_{L_f,\kappa}(X)$, $q\mathcal S_{L_f,\kappa}(X)$, $\mathcal G_{L_f,\kappa}(X)$, $\mathcal U_{L_f,\kappa}(X)$, $\mathcal F_{L_f,\kappa}(X)$ are the convex functions satisfying (1) and, respectively, (7), (10), (17), (13), (22). In Lean these are the predicates StrongIneq, QuasiStrong, QuadGradGrowth, QuadUnder and QuadFunGrowth of NecoaraNG.Chain.Setting, over optSet X f and the nearest-point predicate IsNearest.

Formalization targets

Goal: Theorem 4 (p. 9)

With the same constant $\kappa$ at every step,

$$(7)\Rightarrow(10)\Rightarrow(17)\Rightarrow(13)\Rightarrow(22),$$

that is

$$\mathcal S_{L_f,\kappa}(X)\subseteq q\mathcal S_{L_f,\kappa}(X)\subseteq\mathcal G_{L_f,\kappa}(X)\subseteq\mathcal U_{L_f,\kappa}(X)\subseteq\mathcal F_{L_f,\kappa}(X). \tag{23}$$

The goal is the conjunction of the four implications under the standing assumptions.

Milestones

1. The projection onto $X^*$ is constant along $[\bar x,x]$: $[\bar x+t(x-\bar x)]_{X^*}=\bar x$ for $t\in[0,1]$ (proof of Theorem 3, p. 8).
2. (11), p. 5: $(7)\Rightarrow(10)$.
3. Theorem 1, p. 6: $(10)\Rightarrow(13)$.
4. Theorem 2, p. 7: $(10)\Rightarrow(17)$.
5. Theorem 3, p. 8: $(17)\Rightarrow(13)$.
6. Proof of Theorem 4, p. 9: $(13)\Rightarrow(22)$.

A companion item states the remark on p. 7: for convex $f$, (10) alone or (13) alone gives (17) with constant $\kappa/2$.

Significance

The chain gives the hierarchy that the paper's convergence theorems are stated for: the projected gradient method converges linearly on $q\mathcal S$ and, in distance to $X^*$, exactly on $\mathcal F$; the fast gradient method keeps its accelerated rate on $q\mathcal S$; and $g(Ax)$ with $g$ strongly convex is in $q\mathcal S$ on a polyhedron. Each such result transfers down the chain once the inclusions are known, and the fact that one $\kappa$ survives every link is what keeps the rates' constants explicit.

All the statements are proved in the paper. None of them is formalized: the platform has unconstrained analogues (the Karimi–Nutini–Schmidt chain, with an existential constant and no feasible set), but no constrained statement and no statement with a fixed constant. A formal proof would also check the projection-invariance step that the paper uses without comment.

Difficulty

The links $(7)\Rightarrow(10)$ and $(13)\Rightarrow(22)$ are one-line substitutions. The substance is in Theorems 1 and 3, and specifically in the constant: combining (10) or (13) with the convexity inequality at a single pair of points gives (17) only with constant $\kappa/2$ (the companion item), and the same loss of a factor 2 appears in a direct derivation of (13) from (10). Keeping the full constant $\kappa$ is what makes (23) a chain of inclusions with one index, and it is where the geometry of the optimal set enters: the conditions are tested only against the projection $\bar x$, which moves with $x$. Convexity of $f$ cannot be dropped: (10) alone does not even imply convexity (p. 5).

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $\nabla f$ is Mathlib's gradient f. The function $f$ is defined on all of $\mathbb R^n$, with differentiability assumed at every point of $X$; "continuously differentiable" on $X$ follows from (1).
• Standing assumptions as hypotheses of every theorem: $X$ closed and convex, $f$ convex on $X$ (ConvexOn ℝ X f), (1) with $L_f>0$, a minimiser $x^*\in X^*$, $\kappa>0$. "Simple" (cheap projection) and "closed" for $f$ carry no mathematical content here and are dropped.
• $[x]_{X^*}$ is the predicate IsNearest (optSet X f) x xbar; each condition is required for every nearest point. $f^*$ is written $f(\bar x)$, which is exact because $\bar x\in X^*$.
• An empty optimal set would make every condition vacuous; the hypothesis $x^*\in X^*$ excludes this. The projection is never a choice function, and the gradient is only evaluated at points of $X$, where $f$ is differentiable, so no junk value enters a statement. (7) is the first-order inequality with $\nabla f$, not Mathlib's StrongConvexOn.
• Needed infrastructure: the fundamental theorem of calculus along a segment for a function differentiable on a convex set, first-order optimality for a minimiser over a convex set, and the elementary geometry of nearest points. All of it is reusable for the other missions of this series.

Selected references

• I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
• H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
• H. Zhang, L. Cheng, Restricted strong convexity and its applications to convergence analysis of gradient type methods in convex optimization, Optim. Lett. 9 (2015) 961–979. https://doi.org/10.1007/s11590-014-0795-x
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261

Why column-subset selection and curvature

The column-subset selection problem (CSSP) asks for $k$ columns of a real matrix $A$ whose span approximates all of $A$ as well as possible in squared Frobenius norm. It is a basic primitive of low-rank approximation, feature selection and numerical linear algebra, studied both for its exact complexity and for approximation algorithms (see Boutsidis, Drineas and Magdon-Ismail, doi:10.1137/12086755X, cited as [2] in the source paper).

Sviridenko, Vondrák and Ward study submodular maximization and supermodular minimization when the objective has bounded total curvature, a parameter $c \in [0,1]$ introduced by Conforti and Cornuéjols that measures how far a monotone set function is from being linear. Their guarantees improve as $c$ decreases. Section 8 of the paper applies this to CSSP: it bounds the curvature of the CSSP objective in terms of the condition number of $A$, so that a well-conditioned matrix has small curvature. This mission formalizes that bound (Lemma 8.2) and the steps of its proof.

Setting

Let $A$ be a real $m \times n$ matrix with columns $c_1, \dots, c_n \in \mathbb{R}^m$, so that $Ax = \sum_i x_i c_i$ for $x \in \mathbb{R}^n$, and let $\|\cdot\|$ be the Euclidean norm. For $S \subseteq [n]$ write $\mathrm{proj}_S(x)$ for the orthogonal projection of $x$ onto $\mathrm{span}\{c_i : i \in S\}$, the point of that subspace nearest to $x$ ($\mathrm{proj}_\emptyset = 0$). The CSSP objective is

$$f^A(S) = \sum_{i=1}^n \|c_i - \mathrm{proj}_S(c_i)\|^2 ,$$

the squared Frobenius distance from $A$ to the nearest matrix whose columns lie in the span of the selected columns.

For a set function $f$ on a finite set $X$, the marginal value of $i$ at $A$ is $f_A(i) = f(A+i) - f(A)$. The function $f$ is monotone decreasing if every $f_A(i) \le 0$. Following (1.1) of the paper, a monotone decreasing $f$ has total curvature at most $c$ when, for every $j \in X$,

$$f_{X-j}(j) \le (1-c)\, f_\emptyset(j),$$

i.e. the last marginal of $j$ is at least a $(1-c)$ fraction of its first marginal in absolute value.

When the columns of $A$ are linearly independent, the condition number is

$$\kappa(A) = \frac{\sup_{\|x\|=1}\|Ax\|}{\inf_{\|x\|=1}\|Ax\|} \in [1, \infty).$$

Formalization targets

Goal: Lemma 8.2 (p. 11)

For $A$ with linearly independent columns,

$$f^A_{[n]-j}(j) \le \frac{1}{\kappa^2(A)}\, f^A_\emptyset(j) \quad \text{for all } j \in [n], \qquad \text{i.e.}\quad c(f^A) \le 1 - \frac{1}{\kappa^2(A)} .$$

Milestones

1. The identity $f^A(S) = \sum_i (\|c_i\|^2 - \|\mathrm{proj}_S(c_i)\|^2)$ (p. 11).
2. Lemma 8.1, monotone part: $S \mapsto \|\mathrm{proj}_S(v)\|^2$ is monotone increasing (p. 11).
3. $f^A$ is monotone decreasing (p. 11).
4. $|f^A_\emptyset(i)| = \sum_j \|\mathrm{proj}_{\{i\}}(c_j)\|^2$ (p. 11).
5. Some unit $x$ has $\|Ax\| \ge \sqrt{|f^A_\emptyset(i)|}$ (p. 12).
6. $|f^A_{[n]-i}(i)| = \|c_i - \mathrm{proj}_{[n]-i}(c_i)\|^2$ (p. 12).
7. Some unit $x'$ has $\|Ax'\| \le \sqrt{|f^A_{[n]-i}(i)|}$ (p. 12).
8. $\kappa^2(A) \ge f^A_\emptyset(i)/f^A_{[n]-i}(i)$ for each $i$, under independence (p. 12).

Items 1–7 hold for arbitrary columns; only item 8 and the goal assume independence.

Significance

Lemma 8.2 turns a spectral quantity into a combinatorial one. With it, any curvature-dependent guarantee for monotone decreasing set functions can be stated for CSSP in terms of $\kappa(A)$. The paper's Lemma 8.3 shows the bound is asymptotically tight, so $1 - \Theta(1/\kappa^2)$ is the right order of the curvature.

There is a caveat that the formalization makes explicit. The paper deduces from Lemma 8.1 that $f^A$ is supermodular, and on that basis quotes its supermodular-minimization algorithm for CSSP with factor $1 + (\kappa^2 - 1)e^{-1} + \kappa^2 O(\epsilon)$ (p. 12). Both the submodularity half of Lemma 8.1 and the supermodularity of $f^A$ are false as printed. With $c_1 = e_1$, $c_2 = e_1 + e_2$ and $v = e_2$ in $\mathbb{R}^2$, the function $F(S) = \|\mathrm{proj}_S(v)\|^2$ has $F(\{1,2\}) + F(\emptyset) = 1 > \tfrac12 = F(\{1\}) + F(\{2\})$. With columns $e_1, e_1+e_2, 2e_2$, $f^A(\{1\}) + f^A(\{2\}) = \tfrac{15}{2} > 7 = f^A(\{1,2\}) + f^A(\emptyset)$. A small perturbation gives a counterexample with independent columns. This is the "suppressor variable" phenomenon of regression. The curvature bound itself does not depend on supermodularity and is true, so it is the goal here. The approximation factor for CSSP is not posed, because it rests on the false claim and is stated with $O(\epsilon)$.

As far as is known, none of these statements has a machine-checked proof. The results are proved on paper, except the two false claims above. The mission adds a formal proof of the curvature–conditioning bound, and makes explicit which parts of §8 survive.

Difficulty

The individual steps are short linear algebra, but they rest on infrastructure that has to be assembled: orthogonal projections onto spans of finite column families, the Pythagorean identities that relate $f^A$ to projections, and the variational characterization of $\sup$ and $\inf$ of $\|Ax\|$ over the unit sphere.

The paper's own route to the large unit vector (milestone 5) does not work as printed. It sets $x_j \propto \|\mathrm{proj}_{\{i\}}(c_j)\|$ and uses $c_i \cdot c_j = \|c_i\|\,\|\mathrm{proj}_{\{i\}}(c_j)\|$, which is false when $c_i \cdot c_j < 0$, so the signs of the inner products have to be accounted for. In the final step, the ratio $f^A_\emptyset(i)/f^A_{[n]-i}(i)$ is a quotient of two negative numbers. Comparing it with $\kappa^2$ requires the supremum to be finite and the infimum to be strictly positive, which is exactly what independence of the columns provides.

Formalization scope

• Columns are a family c : Fin n → EuclideanSpace ℝ (Fin m), and $Ax$ is ∑ j, x j • c j. Subsets of $[n]$ are Finset (Fin n). $[n] - i$ is Finset.univ.erase i and $S + i$ is insert i S.
• $\mathrm{proj}_S$ is Mathlib's Submodule.starProjection onto Submodule.span ℝ (c '' S), which is finite-dimensional, so the argmin of the page exists and is unique.
• $\kappa(A)$ is a real quotient of ⨆ and ⨅ of $\|Ax\|$ over the unit-sphere subtype of $\mathbb{R}^n$. It is used only under LinearIndependent ℝ c, the page's "non-singular", where both are finite and positive. The page's $\kappa = \infty$ for dependent columns is not encoded.
• Monotonicity is the marginal form of §2.1. Curvature is the product form above, which agrees with the ratio of (1.1) whenever $f_\emptyset(j) \ne 0$ and avoids Lean's $x/0 = 0$.
• For $n = 0$ the goal has no $j$ and is empty, as on the page.
• A trivializing reading is ruled out by the encoding: had $\kappa$ evaluated to a junk value $0$, the goal would reduce to monotonicity. Under independence the supremum and infimum are genuine, so the bound $1 - 1/\kappa^2$ is the paper's.
• Not in scope: Lemma 8.3 (stated with $O(\cdot)$), the CSSP approximation factor, and the false submodularity and supermodularity claims.

Useful infrastructure that would be reusable beyond this mission includes Pythagoras for starProjection, monotonicity of projection norms under inclusion of subspaces, and extremal characterizations of $\sup_{\|x\|=1}\|Ax\|$ and $\inf_{\|x\|=1}\|Ax\|$. Contributions of any of the milestones, or of these general lemmas, are welcome.

Selected references

• M. Sviridenko, J. Vondrák, J. Ward, Optimal approximation for submodular and supermodular optimization with bounded curvature, SODA 2015 (version of Oct. 9, 2014); journal version Math. Oper. Res. 42(4), 2017. https://doi.org/10.1287/moor.2016.0842
• M. Conforti, G. Cornuéjols, Submodular set functions, matroids and the greedy algorithm: tight worst-case bounds and some generalizations of the Rado–Edmonds theorem, Discrete Appl. Math. 7(3), 1984. https://doi.org/10.1016/0166-218X(84)90003-9
• C. Boutsidis, P. Drineas, M. Magdon-Ismail, Near-optimal column-based matrix reconstruction, SIAM J. Comput. 43(2), 2014. https://doi.org/10.1137/12086755X
• A. Das, D. Kempe, Submodular meets spectral: greedy algorithms for subset selection, sparse approximation and dictionary selection, ICML 2011. https://arxiv.org/abs/1102.3975

Motivation

Strategic open pit mine planning decides which parts of an ore body are excavated, in which period, and to which destination (a processing plant, a stockpile, a waste dump) each block of material is sent. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) model this as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), which extends the PCPSP of Bienstock and Zuckerberg (2010) by grouping blocks into clusters that are extracted together. The integer versions of the model have weak linear relaxations on production scheduling instances, so the authors derive cutting planes. Their production cuts (§5.2) exploit the capacity of a single destination together with the precedence structure. This mission concerns the second family of production cuts, the hourglass cuts: they bound how much material must be sent away from a capacitated destination once a cluster is started, using both the predecessors and the successors of that cluster.

Valid inequalities for precedence-constrained knapsack problems have been studied since Boyd (1993) (cited on p. 1433); the paper's contribution is the extension to several destinations, several periods, clusters and partial integrality, the condition used in commercial mine planning software.

All page references are journal pages of the published Operations Research article.

Setting

An instance has finite sets $\mathcal B$ of blocks, $\mathcal D$ of destinations and $\mathcal C$ of clusters, the latter a partition of $\mathcal B$, and periods $\mathcal T=\{1,\dots,T\}$. Block $b$ lies in cluster $c(b)$ and has weight $q_b\ge 0$. A precedence relation $b_1\prec b_2$ on blocks induces one on clusters ($c_1\prec c_2$ if some block of $c_1$ precedes some block of $c_2$), assumed to be a strict partial order. The arc set $\mathcal A$ is its transitive reduction: $(c,c')\in\mathcal A$ when $c'$ is an immediate predecessor of $c$. The closure is $cl(c)=\{c\}\cup\{c':c'\prec c\}$ and the reverse closure $rcl(c)=\{c\}\cup\{c':c\prec c'\}$; $b(S)$ is the set of blocks of a set $S$ of clusters, and $q(S)$ is the total weight of a set of blocks.

Variables $x_{c,t}$ give the fraction of cluster $c$ extracted in period $t$ and $y_{b,d,t}$ the fraction of block $b$ sent to destination $d$ in period $t$. The constraints (2)–(7) of p. 1427 are

$$x_{c(b),t}=\sum_{d}y_{b,d,t},\qquad \sum_{t}x_{c,t}\le 1,\qquad \sum_{t'\le t}x_{c,t'}\le\sum_{t'\le t}x_{c',t'}\ \ ((c,c')\in\mathcal A),\qquad Gy\le g,\qquad y\ge 0,$$

with an integrality condition: full integrality (10), $x_{c,t}\in\{0,1\}$, defines the PCPSP-F, and partial integrality (11), "$\sum_{t'\le t}x_{c,t'}>0$ implies $\sum_{t'\le t}x_{c',t'}=1$ for $(c,c')\in\mathcal A$", defines the PCPSP-P. The rows $Gy\le g$ include the destination capacity rows (9), $\sum_b q_b\,y_{b,d,t}\le U^d_t$. The cuts are written in the cumulative variables $w_{c,t}=\sum_{t'=1}^{t}x_{c,t'}$ (17).

The simplified setting of §5.2.1 is the mode-knapsack set MK (p. 1433): for a directed acyclic graph $G=(\mathcal B,\mathcal A)$, weights $q>0$ and a capacity $U>0$, the triples $(x,y^P,y^W)$ with $\sum_b q_by^P_b\le U$, $y^P_b+y^W_b=x_b\le 1$, $y^P,y^W\ge 0$, and $x_b>0\Rightarrow x_{b'}=1$ for every arc $(b,b')$. Here $P$ is processing and $W$ is waste.

Formalization targets

Goal: Theorem 8 (hourglass cuts), p. 1435

Let $d\in\mathcal D$, $1\le t_1\le t\le T$, $\bar c\in\mathcal C$, and let $S\subseteq b(cl(\bar c)\setminus\{\bar c\})$ be a set of blocks with $q(S)\ge\sum_{s=t_1}^{t}U^d_s$. With $R=rcl(\bar c)\setminus\{\bar c\}$, the inequality

$$\Bigl(q(S\cup\{\bar c\})-\sum_{s=t_1}^{t}U^d_s\Bigr)w_{\bar c,t}+\sum_{b\in b(R)}q_b\sum_{s=t_1}^{t}y_{b,d,s}\le\sum_{b\in S\cup\{\bar c\}}q_b\Bigl(w_{c(b),t}-\sum_{s=t_1}^{t}y_{b,d,s}\Bigr)\tag{37}$$

is valid for the PCPSP-C, that is, for both the PCPSP-F and the PCPSP-P.

Milestones

• Proof of Theorem 8, p. 1435: if $w_{\bar c,t}>0$, every cluster preceding $\bar c$ has $w_{c,t}=1$.
• Proof of Theorem 8, p. 1435: the blocks of $S$, of $\bar c$ and of $b(R)$ together respect the capacity $U^d_s$ of every period.
• Theorem 6, p. 1434: the simplified hourglass cut $(q(S)+q_b-U)x_b\le\sum_{b'\in S\cup\{b\}}q_{b'}y^W_{b'}$ is valid for MK when $S\subseteq cl(b)\setminus\{b\}$ and $q(S)\ge U$.
• The lifted inequality of p. 1434, which adds $\sum_{b'\in rcl(b)\setminus\{b\}}q_{b'}y^P_{b'}$ to the left-hand side of Theorem 6.
• Display (38), p. 1436: the block set $S^*=\{b: c(b)\prec\bar c,\ w^*_{\bar c,t}>w^*_{c(b),t}-\sum_{s=t_1}^{t}y^*_{b,d,s}\}$ maximizes the violation of (37) at any point $(w^*,y^*)$.

Significance

In the computational study of §8 (Table 5, p. 1440; discussion on p. 1442) the authors add early start, lifted clique, VRHS and hourglass cuts to the LP relaxation and drop one class at a time; they observe that all classes improve the bound and that the hourglass cuts have the most significant impact. Display (38) makes the separation of the most violated hourglass cut a single pass over the blocks for each cluster, destination and period window. The cuts are valid under partial integrality, the weaker condition that mine planning software imposes, so they strengthen the relaxation of the model actually solved in practice.

Theorem 8 is proved in the paper by a direct calculation; no machine-checked proof exists. A formal proof would certify the inequality in exactly the generality of the model (clusters, several destinations, several periods, both integrality conditions), and the formal model of the PCPSP-C built for it is shared with the other missions of this series.

Difficulty

The inequality is false for the LP relaxation: a fractional start of $\bar c$ need not force its predecessors to be complete. Every proof therefore has to use integrality, and the two integrality conditions behave differently. Under partial integrality (11) the implication "started implies predecessors complete" is stated only along the arcs of the transitive reduction $\mathcal A$, and has to be propagated along chains of immediate predecessors to reach every predecessor of $\bar c$. The capacity step needs that the strict predecessors, $\bar c$ itself and its strict successors are pairwise disjoint block sets, which is where the strict partial order is used. The $w$ terms are cumulative from period 1 while the $y$ terms are summed from $t_1$; the two must not be aligned.

Formalization scope

Periods are Fin T, so index $t$ denotes period $t+1$. Cluster precedence is derived from the block relation, and $\mathcal A$ is its covering relation. The standing assumptions of §2.1 (clusters partition the blocks, $\prec$ a strict partial order on clusters, discount rate $r>0$, weights $q\ge 0$) are a single hypothesis on the instance. "Valid for the PCPSP-C" is stated as: for each integrality condition, at every feasible $(x,y)$ whose destination capacity rows (9) hold, which is the page's assumption that (9) is among the rows $Gy\le g$. The destination $d$, unbound on the page, is a fixed arbitrary destination. In Theorem 8 $S$ is a set of blocks and $q(S\cup\{\bar c\})$ is the weight of $S$ together with the blocks of $\bar c$. In MK an arc $(b,b')$ means $b'$ precedes $b$, and $\prec$ is reachability in $G$.

Reading "valid" as "valid for the LP relaxation" would make the goal false, while dropping the condition $S\subseteq b(cl(\bar c)\setminus\{\bar c\})$, or the capacity rows, would make it a different statement; neither is the target. In (38) the maximum is taken over all $S\subseteq b(cl(\bar c)\setminus\{\bar c\})$ as on the page, without the side condition $q(S)\ge\sum U^d_s$, which $S^*$ need not satisfy.

A complete development needs only finite sums, finsets and the transitive closure of a relation from Mathlib. Proofs of the milestones, of the MK results and of the goal are all welcome; the lemma that partial integrality propagates along chains of arcs is reusable across all production cuts of the paper.

Selected references

• O. Rivera Letelier, D. Espinoza, M. Goycoolea, E. Moreno, G. Muñoz, Production scheduling for strategic open pit mine planning: a mixed-integer programming approach, Operations Research 68(5):1425–1444, 2020. https://doi.org/10.1287/opre.2019.1965
• D. Bienstock, M. Zuckerberg, Solving LP relaxations of large-scale precedence constrained problems, Proc. 14th Conf. Integer Programming and Combinatorial Optimization (IPCO), 1–14, 2010 (reference list of the article above).
• E. A. Boyd, Polyhedral results for the precedence-constrained knapsack problem, Discrete Applied Mathematics 41(3):185–201, 1993 (reference list of the article above).

Motivation

Unit commitment (UC) is the daily scheduling problem of electricity system operators: decide which generators are switched on in each hour of the next day, and how much each produces, so that supply meets the net load at minimum cost while respecting generation limits, ramping limits and transmission limits. With growing shares of wind and solar power, the net load is uncertain at the time the commitment is fixed. Adaptive robust UC protects the schedule against every net-load trajectory in an uncertainty set.

Lorca, Sun, Litvinov and Zheng (Oper. Res., 2016) argue that the dispatch must be nonanticipative (the output at hour $t$ may depend only on loads observed up to $t$) and propose a multistage robust UC model. To make it computable they restrict the dispatch to affine policies of the observed loads, in the spirit of Ben-Tal, Goryashko, Guslitzer and Nemirovski (Math. Program. 99, 2004). The paper solves the model on the IEEE 118-bus test case and on the 2718-bus Polish system. The two results of this mission are what makes the simplest such policy cheap to solve: under it, the semi-infinite robust constraints on generation, ramping and energy balance collapse to finitely many deterministic constraints.

Setting

There are $N_g$ generators $i$, $N_d$ load nodes $j$ and periods $t\in\mathcal T=\{1,\dots,T\}$. A net-load trajectory is $\boldsymbol d=(d^t_j)$, and its total load in period $t$ is $\sum_{j\in\mathcal N_d}d^t_j$. The budget uncertainty set (3) is

$$\mathcal D^t=\Big\{\boldsymbol d^t:\ \sum_{j}\frac{|d^t_j-\bar d^t_j|}{\hat d^t_j}\le\Gamma\sqrt{N_d},\ d^t_j\in[\bar d^t_j-\Gamma\hat d^t_j,\ \bar d^t_j+\Gamma\hat d^t_j]\Big\},\qquad\mathcal D=\prod_{t\in\mathcal T}\mathcal D^t,$$

with nominal loads $\bar d$, deviations $\hat d>0$ and a conservativeness parameter $\Gamma\ge0$.

The $W_{it}$-policy (10) sets the output of generator $i$ in period $t$ to an affine function of the current total load,

$$p^t_i(\boldsymbol d)=w^t_i+W_{it}\sum_{j\in\mathcal N_d}d^t_j ,$$

and the $W_i$-policy (9) is the special case in which $W_{it}=W_i$ does not depend on $t$. Given commitments $x^t_i,u^t_i,v^t_i$, output limits $p^{\min}_i,p^{\max}_i$ and ramp rates $RD,RU,SD,SU$, the robust constraints of the affine model (8) require, for all $\boldsymbol d\in\mathcal D$: generation limits $p^{\min}_ix^t_i\le p^t_i(\boldsymbol d)\le p^{\max}_ix^t_i$ (8c); ramping limits $-RD^t_ix^t_i-SD^t_iv^t_i\le p^t_i(\boldsymbol d)-p^{t-1}_i(\boldsymbol d)\le RU^t_ix^{t-1}_i+SU^t_iu^t_i$ ((8d), (8e)); and energy balance $\sum_ip^t_i(\boldsymbol d)=\sum_jd^t_j$ (8g).

The extreme total-load scenarios are a trajectory $\boldsymbol d_{\max}\in\mathcal D$ whose total load is maximal over $\mathcal D$ in every period (19), a trajectory $\boldsymbol d_{\min}\in\mathcal D$ whose total load is minimal in every period (20), and the mixed scenarios

$$\boldsymbol d_{minmax}(t)=(\boldsymbol d^1_{\min},\dots,\boldsymbol d^{t-1}_{\min},\boldsymbol d^t_{\max},\dots,\boldsymbol d^T_{\max}),\qquad\boldsymbol d_{maxmin}(t)=(\boldsymbol d^1_{\max},\dots,\boldsymbol d^{t-1}_{\max},\boldsymbol d^t_{\min},\dots,\boldsymbol d^T_{\min})$$

of (21), (22).

Formalization targets

Goal: Proposition 6

Under the $W_{it}$-policy (or the $W_i$-policy), for every generator $i$ and period $t$:

$$\text{(8c) over }\mathcal D\iff\text{(8c) over }\{\boldsymbol d_{\min},\boldsymbol d_{\max}\},$$ $$\text{(8d), (8e) at }t\text{ over }\mathcal D\iff\text{(8d), (8e) at }t\text{ over }\{\boldsymbol d_{\min},\boldsymbol d_{\max},\boldsymbol d_{minmax}(t),\boldsymbol d_{maxmin}(t)\}.$$

Milestones

1. Proof of (i) (pp. ec1–ec2): (8c) over $\mathcal D$ is equivalent to four deterministic inequalities, at the total loads of $\boldsymbol d_{\max}$ and $\boldsymbol d_{\min}$.
2. (23)–(24) (p. 19): because $\mathcal D$ is a product over periods, the worst case of $W_{it}\sum_jd^t_j-W_{i,t-1}\sum_jd^{t-1}_j$ over $\mathcal D$ is a maximum over $\mathcal D^t$ minus a minimum over $\mathcal D^{t-1}$.
3. (25a)–(25d) (p. 19): both the maximum and the minimum of that difference over $\mathcal D$ are attained in $\{\boldsymbol d_{\min},\boldsymbol d_{\max},\boldsymbol d_{minmax}(t),\boldsymbol d_{maxmin}(t)\}$.

Companion: Proposition 4

For a full-dimensional uncertainty set, the robust energy balance (8g) holds if and only if $\sum_iw^t_i=0$ and $\sum_iW_{it}=1$ for all $t$ ((15)); for the $W_i$-policy, $\sum_iw^t_i=0$ and $\sum_iW_i=1$ ((14)).

Significance

Proposition 6 removes the constraints (8c)–(8e) from the constraint-generation loop of the affine robust UC: they can be imposed before the algorithm starts, through two scenarios per generation constraint and four per ramping constraint, leaving only the worst-case cost constraint and the transmission constraints to be separated. Proposition 4 turns the semi-infinite energy balance into $2T$ linear equalities. Together they are the reason the $W_{it}$-policy scales to the 2718-bus system in the paper's experiments.

Both results are proved in the paper, and the proofs are short. No machine-checked version is known. The formalization fixes the exact handling of the first period (the initial dispatch $p^0_i$), the exact definition of the mixed scenarios, and the dependence of part (ii) on the product structure of $\mathcal D$, all of which the paper leaves implicit or states loosely.

Difficulty

Part (i) needs only that the constraint is affine in the scalar total load of one period. Part (ii) is where the obvious argument fails: the ramping constraint couples two periods, and a set that is not a product over periods may not contain a trajectory that is simultaneously maximal in period $t$ and minimal in period $t-1$. The separability of $\mathcal D$ is exactly what puts $\boldsymbol d_{minmax}(t)$ and $\boldsymbol d_{maxmin}(t)$ in $\mathcal D$. The labels the paper attaches to (25a) and (25d) are swapped relative to (21)–(22); following them literally sends the argument to the wrong scenario.

Formalization scope

• Representation. Generators, load nodes and periods are Fin Ng, Fin Nd, Fin T; trajectories are Fin T → Fin Nd → ℝ. Periods are 0-based: Lean period t is the paper's period $t+1$, so "periods $1,\dots,t-1$" in (21)–(22) are the Lean periods s < t.
• First period. The dispatch "at $t-1$" for the first period is the initial dispatch $p^0_i$ and $x^{t-1}_i$ is the initial status $x^0_i$; both are data.
• Commitments are arbitrary reals: the results do not use $x,u,v\in\{0,1\}$.
• Scenarios are hypotheses. $\boldsymbol d_{\max}$ and $\boldsymbol d_{\min}$ are any members of $\mathcal D$ with maximal, respectively minimal, total load in every period, never a chosen witness. A formalization in which they are arbitrary trajectories, or in which the four-scenario set is not tied to $\mathcal D$, is ruled out: part (ii) is false for it.
• Extrema in milestone 2 are taken in EReal, under the standing assumptions $\Gamma\ge0$, $\hat d>0$ that make every $\mathcal D^t$ nonempty and bounded.
• Policies. Everything is stated for the $W_{it}$-policy; the $W_i$-policy is the instance $W_{it}=W_i$.
• Proposition 4 is stated for a general set with nonempty interior, as on the page, with the added hypothesis $N_d\ge1$: with no load node the statement is false.

The development needs only finite sums, products of sets, and order facts about affine functions; it reuses nothing beyond Mathlib. Proofs of the milestones, the goal and Proposition 4 are welcome.

Selected references

• Á. Lorca, X. A. Sun, E. Litvinov, T. Zheng, Multistage adaptive robust optimization for the unit commitment problem, Operations Research, 2016 (manuscript of September 29, 2014). https://doi.org/10.1287/opre.2015.1456
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99:351–376, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, E. Litvinov, X. A. Sun, J. Zhao, T. Zheng, Adaptive robust optimization for the security constrained unit commitment problem, IEEE Transactions on Power Systems 28(1):52–63, 2013. https://doi.org/10.1109/TPWRS.2012.2205021