Optimization

Motivation

Strategic open pit mine planning decides which parts of an ore body are excavated, in which period, and where each block of material is sent: to a processing plant, a stockpile or a waste dump. Rivera Letelier, Espinoza, Goycoolea, Moreno and Muñoz (Operations Research 68(5), 2020) state the problem as a mixed-integer program, the precedence-constrained production scheduling problem with clusters (PCPSP-C), which extends the formulation of Bienstock and Zuckerberg (IPCO 2010) to clusters of blocks that are extracted together. The integer versions of this program have large integrality gaps on production scheduling instances (§5, p. 1432), so the authors derive problem-specific cutting planes. This mission concerns the variable-right-hand-side (VRHS) production cuts of §5.2. They combine the precedence order of the clusters with the capacity of a single destination: if a solution sends many blocks to a capacitated destination, the predecessors of those blocks must be fully extracted.

The VRHS cuts are introduced first on a one-period, two-destination set, the mode-knapsack set MK (§5.2.1), and then generalised to the full multi-period clustered model (§5.2.2). Disaggregated formulations with destination choices go back to Boland et al. (Comput. Oper. Res. 2009); cutting planes for the precedence-constrained knapsack structure of open pit scheduling were studied by Bley et al. (Comput. Oper. Res. 2010).

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 reverse closure of a cluster is $rcl(c)=\{c\}\cup\{c':c\prec c'\}$, the cluster and everything that requires it; for a set $S$ of clusters, $q(S)=\sum_{c\in S}\sum_{b\in c}q_b$.

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,$$

together 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 general rows $Gy\le g$ include the destination capacity rows (9), $\sum_b q_b\,y_{b,d,t}\le U^d_t$. The cuts use the cumulative variables $w_{c,t}=\sum_{t'=1}^{t}x_{c,t'}$ (17).

The mode-knapsack set MK (p. 1433) fixes a DAG $G=(\mathcal B,\mathcal A)$, weights $q_b>0$ and a capacity $U>0$, and consists of the vectors $(x,y^P,y^W)$ with

$$\sum_b q_b y^P_b\le U,\qquad y^P_b+y^W_b=x_b,\qquad x_b\le 1,\qquad x_b>0\Rightarrow x_{b'}=1\ ((b,b')\in\mathcal A),\qquad y^P,y^W\ge 0.$$

Formalization targets

Goal: Theorem 7 (VRHS cuts), p. 1434

Fix $d\in\mathcal D$, $t\in\mathcal T$ and clusters $c_1\prec c_2\prec\dots\prec c_n$ with $q(rcl(c_1)\setminus rcl(c_n))<U^d_t<q(rcl(c_1))$. Let $\Delta_k=rcl(c_k)\setminus rcl(c_{k+1})$, $\delta_k=q(\Delta_k)$ for $k<n$, and $\Delta_n=rcl(c_n)$, $\delta_n=U^d_t-q(rcl(c_1)\setminus rcl(c_n))$. For constants $0\le\alpha_b\le 1$ ($b\in c_n$), the inequality

$$\sum_{k=1}^{n-1}\sum_{c\in\Delta_k}\sum_{b\in c}q_b y_{b,d,t}+\sum_{b\in c_n}\alpha_b q_b y_{b,d,t}+\sum_{c\in rcl(c_n)\setminus\{c_n\}}\sum_{b\in c}q_b y_{b,d,t}\le\sum_{k=1}^{n}\delta_k w_{c_k,t}\tag{32}$$

is valid for the PCPSP-F, and, when $\sum_{b\in c_n}\alpha_b q_b\le U^d_t-q(rcl(c_1)\setminus rcl(c_n))$ (33), for the PCPSP-P. The goal is the conjunction of the two validity claims.

Milestones

• (29)–(30), p. 1434: under either integrality condition, $w_{c,t}<1$ implies $y_{b,d,t}=0$ for every block of a cluster in $rcl(c)\setminus\{c\}$, and $y_{b,d,t}\le w_{c(b),t}$. The third condition (31) of the page is the capacity row (9) itself.
• (35), p. 1435: $\sum_{c\in\Delta_k}\sum_{b\in c}q_b y_{b,d,t}\le\delta_k w_{c_k,t}$ for $k=1,\dots,n-1$.
• (36), p. 1435: under (33), $\sum_{b\in c_n}\alpha_b q_b y_{b,d,t}\le\delta_n w_{c_n,t}$.
• Theorem 5, p. 1434: in MK, every block $b$ with $q_b\le U$ gives the valid inequality $\sum_{b'\in rcl(b)}q_{b'}y^P_{b'}\le U x_b$.

Significance

A valid inequality removes fractional points of the linear relaxation while keeping every feasible schedule. The VRHS cuts are among the production cuts that the paper evaluates in its computational study (§8), alongside the extraction cuts and the hourglass cuts. Their right-hand side is not a constant but a combination of extraction variables along a chain, which is what lets them couple the destination capacity with the precedence order; the paper's Theorem 5 shows the mechanism on MK, Theorem 7 in the full model. The partial integrality regime, under which the second half of Theorem 7 holds, is the one used by commercial mine planning software (p. 1427).

The results are proved in the paper by case analysis on the first index $k$ with $w_{c_k,t}<1$. None of them has a machine-checked proof. Formalizing them makes explicit which rows of the formulation each cut uses (the destination capacity (9) and the integrality condition), and what role the coefficient condition (33) plays in the partially integral case.

Difficulty

The proof uses that $\Delta_1,\dots,\Delta_{n-1}$ partition $rcl(c_1)\setminus rcl(c_n)$ and are disjoint from $rcl(c_n)$, which requires $rcl(c_{k+1})\subseteq rcl(c_k)$ along the chain. It uses that $w_{c,t}\le w_{c_k,t}$ for every $c\in rcl(c_k)$, and that $w_{c,t}<1$ forces all strict successors of $c$ to be unextracted; both chain the constraints (4) and (11) along covering arcs of a finite strict order, since the formulation constrains only the arcs of $\mathcal A$, not all of $\prec$. A natural first attempt, arguing directly from $\prec$, therefore does not apply. The counting step needs $x\ge 0$, which is not a constraint of the formulation but follows from $x_{c(b),t}=\sum_d y_{b,d,t}$, $y\ge 0$ and the nonemptiness of clusters. In the partial integrality case a fractional $w_{c_n,t}$ is possible, and the bound on the $c_n$ term must come from (33) rather than from integrality.

Formalization scope

Blocks, destinations and clusters are finite types; periods are Fin T, index $t$ standing for period $t+1$. An instance carries the block-to-cluster map, the block precedence, values, discount rate, weights, capacities and $m$ side rows $Gy\le g$. Cluster precedence is derived from block precedence; $\mathcal A$ is its covering relation, and constraints (4) and (11) range over $\mathcal A$ only. The chain $c_1,\dots,c_n$ is a function on $\mathbb N$ read at $1,\dots,n$ with $n\ge 1$, and condition 1 of Theorem 7 is stated for consecutive pairs. In (32), $y$ is taken at the single period $t$ and $w$ is cumulative.

The standing assumptions of §2.1 are hypotheses of every PCPSP-C statement: clusters cover $\mathcal B$ (so each is nonempty), $\prec$ is a strict partial order on clusters, $r>0$, and $q_b\ge 0$. A cut "valid for the PCPSP-F (PCPSP-P)" is stated as: at every point feasible for the formulation with full (partial) integrality whose destination capacity rows (9) hold, the inequality holds. The capacity rows enter as an explicit hypothesis because the paper assumes they are among the rows of $Gy\le g$; without them the cut is false. Validity is never asserted for the LP relaxation, where (29) and (32) fail, so the integrality condition cannot be dropped. Conditions 2 and 3 of Theorem 7 are kept as on the page, although the proof does not use condition 3. In MK, the DAG property, $q>0$ and $U>0$ are hypotheses; an arc $(b,b')$ means that extracting $b$ forces $b'$, and $rcl(b)$ collects $b$ and the blocks from which $b$ is reachable.

The development needs only finite sums, finite sets and orders from Mathlib. Contributions are welcome on the chaining lemma for covering relations of finite strict orders, on the nonnegativity and monotonicity of $w$, and on the partition $\{\Delta_k\}$ of $rcl(c_1)\setminus rcl(c_n)$, which the goal and the milestones share.

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 IPCO, LNCS 6080, 1–14, 2010. https://doi.org/10.1007/978-3-642-13036-6_1
• N. Boland, I. Dumitrescu, G. Froyland, A. M. Gleixner, LP-based disaggregation approaches to solving the open pit mining production scheduling problem with block processing selectivity, Computers & Operations Research 36(4):1064–1089, 2009. https://doi.org/10.1016/j.cor.2007.12.006
• A. Bley, N. Boland, C. Fricke, G. Froyland, A strengthened formulation and cutting planes for the open pit mine production scheduling problem, Computers & Operations Research 37(9):1641–1647, 2010. https://doi.org/10.1016/j.cor.2009.12.008

Motivation

In many planning problems the decision changes the uncertainty it faces. Opening a facility raises the demand observed near it; a maintenance decision changes the failure distribution of a component; a price shifts the demand law. Decision-dependent uncertainty of this kind breaks the standard assumption of stochastic programming that the probability distribution is fixed in advance. When the distribution is in addition only partly known, the natural model is distributionally robust: the decision maker optimizes against the worst distribution in an ambiguity set whose shape itself depends on the decision.

X. Yu and S. Shen (arXiv:2002.12518v3, 2020; published in Mathematical Programming) study the multistage version of this model with binary state variables, and show that under three families of moment-based ambiguity sets each stage of the dynamic program can be rewritten as a single minimization, which can then be solved by stochastic dual dynamic integer programming (SDDiP). This mission formalizes the first family, Type 1, in which every moment is bounded above and below by decision-dependent functions.

Timeline. Two-stage decision-dependent DRO with moment bounds was reformulated by F. Luo and S. Mehrotra (Distributionally robust optimization with decision dependent ambiguity sets, Optimization Letters, 2020, arXiv:1806.09215), Theorem 3.1. SDDiP for multistage stochastic integer programs is due to J. Zou, S. Ahmed and X. A. Sun (Stochastic dual dynamic integer programming, Math. Program. 175(1–2):461–502, 2019, doi:10.1007/s10107-018-1249-5). Yu and Shen (2020) combine the two in the multistage setting, for Type 1 (moment bounds), Type 2 (mean and covariance) and Type 3 (Delage–Ye type) sets.

Setting

Fix one stage $t$ of the dynamic program. The state $x\in\{0,1\}^I$ links stage $t$ to stage $t+1$, and the stage variable $y\in\mathbb R^{I\times J}$ is used only at stage $t$. The pairs $(x,y)$ allowed at stage $t$ form the stage feasible set $S=X_t(x_{t-1},\xi_t)$, and $g(x,y)$ is the stage cost.

The random vector of stage $t+1$ takes one of $K$ values $\xi^1,\dots,\xi^K\in\mathbb R^J$, the same for every decision (Assumption 3). What depends on the decision is the probability vector $p\in\mathbb R^K$ on these points. $Q_{t+1}(x,\xi^k)$ is the value of the next stage when the state is $x$ and scenario $k$ occurs.

Moment functions. For nonnegative integers $k_{sj}$, the moment functions are $f_s(\xi)=\prod_{j=1}^J\xi_j^{k_{sj}}$, $s=1,\dots,m$, collected into $f=(f_1,\dots,f_m)$.

Type 1 ambiguity set. For decision-dependent bounds $l(x),u(x)\in\mathbb R^m$ and $\underline p(x),\bar p(x)\in\mathbb R^K$,

$$\mathcal P^{D_1}_{t+1}(x)=\Big\{p\in\mathbb R^K_+\ :\ \underline p(x)\le p\le\bar p(x),\ \ l(x)\le\sum_{k=1}^Kp_kf(\xi^k)\le u(x)\Big\}.$$

Normalization $\sum_kp_k=1$ is obtained by choosing one moment function $f_1\equiv1$ with $l_1=u_1=1$.

Stage Bellman equation. The stage value is

$$Q_t(x_{t-1},\xi_t)=\min_{(x,y)\in S}\Big\{g(x,y)+\max_{p\in\mathcal P^{D_1}_{t+1}(x)}\sum_{k=1}^Kp_k\,Q_{t+1}(x,\xi^k)\Big\}.\tag{2}$$

Formalization targets

Goal: Theorem 1 (p. 8)

If $\mathcal P^{D_1}_{t+1}(x)$ is nonempty for every feasible $x$, then (2) equals the joint minimization

$$\begin{aligned}\min_{\alpha,\beta,\underline\gamma,\bar\gamma,x,y}\ \ &g(x,y)-\alpha^{\mathsf T}l(x)+\beta^{\mathsf T}u(x)-\underline\gamma^{\mathsf T}\underline p(x)+\bar\gamma^{\mathsf T}\bar p(x)\\ \text{s.t.}\ \ &(-\alpha+\beta)^{\mathsf T}f(\xi^k)-\underline\gamma_k+\bar\gamma_k\ge Q_{t+1}(x,\xi^k),\quad k\in[K],\\ &(x,y)\in S,\qquad \alpha,\beta,\underline\gamma,\bar\gamma\ge0.\end{aligned}\tag{4}$$

In Lean, "equals" is the statement that for every real $q$, $q$ is the attained minimum of (2) if and only if it is the attained minimum of (4).

Milestones: the inner LP (C-17) (p. 36)

1. Weak duality. For a state $x$, every $p\in\mathcal P^{D_1}_{t+1}(x)$ and every dual point satisfying (4b) and (4d) at $x$, $\sum_kp_kQ_{t+1}(x,\xi^k)\le-\alpha^{\mathsf T}l(x)+\beta^{\mathsf T}u(x)-\underline\gamma^{\mathsf T}\underline p(x)+\bar\gamma^{\mathsf T}\bar p(x)$.
2. Strong duality. If $\mathcal P^{D_1}_{t+1}(x)\ne\emptyset$, some feasible $p$ and some dual point satisfying (4b) and (4d) have equal objective values.

Companion: (7) (p. 9)

With the $2J+1$ moment constraints of (5)–(6) (normalization, first and second moments of each coordinate around affine decision-dependent empirical moments $\mu_j(x)$, $S_j(x)$) and $\underline p=0$, $\bar p=1$, the stage value equals the joint program (7), whose objective (7a) has no $\gamma$-terms.

Significance

Theorem 1 removes the inner maximization from every stage of the multistage model. Without it, each stage is a min–max problem whose inner feasible set moves with the binary decision, and SDDiP's cut generation does not apply. After the reformulation, each stage is a single mixed-integer program whose only nonlinearities are products of a binary state with a continuous dual variable, which McCormick envelopes linearize exactly. The paper's facility-location experiments use exactly this route via (7).

The result is proved on paper by a one-line appeal to LP strong duality. No machine-checked version exists. The formal content this mission adds is the precise accounting of what the appeal needs: that the inner LP is bounded (from $0\le p\le\bar p(x)$), that its dual is attained, that the outer minimum transfers between the two formulations in both directions, and that the sign constraint $p\ge0$ is present. A Lean development also separates the parts that hold for arbitrary $S$ and $g$ from the paper's standing linearity and compactness assumptions.

The platform already has a general LP strong duality theorem, LinearOptimization.lp_strong_duality (Bertsimas–Tsitsiklis, Theorem 4.4, on a general-form LP structure; proved). It is a tool for the milestones, not a statement of this paper.

Difficulty

The inner problem is a finite LP, so the difficulty is not depth but bookkeeping that the paper leaves to the reader. Strong duality must be applied to an LP with four families of inequality rows plus sign constraints, with the moment rows written as sums of vectors. The obvious reading of (3) as printed — no $p\ge0$ — makes Theorem 1 false when $\underline p(x)$ has negative entries, because the free variable $p$ would force (4b) to be an equality. The equivalence of the two outer minima also needs care: (4) minimizes jointly over $(x,y)$ and the multipliers, so the attained minimum of (4) must be matched with a pair $(x,y)$ at which the inner maximum of (2) is attained, in both directions. For (7), the dual of (6) lacks the $\bar\gamma$-terms of (4), so (7) is not a literal instance of Theorem 1: the redundancy of $p\le1$ under $\sum_kp_k=1$, $p\ge0$ has to be used.

Formalization scope

All declarations live in the namespace DDMomentDRO.Type1. States are Fin I → ℝ, stage variables Fin I → Fin J → ℝ, scenarios Fin K → Fin J → ℝ, all indices $0$-based. The moment exponents are a matrix e : Fin m → Fin J → ℕ. $Q_{t+1}$ is an arbitrary real function of $(x,k)$: the theorems use nothing about the next stage, so the recursion is not formalized. The binary state is kept as a hypothesis on $S$; linearity of $g$ and compactness and polyhedrality of $S$ (p. 5) are dropped, a disclosed generalization. The ambiguity set includes $p\ge0$ (the proof's (C-17f)), which (3) as printed omits, and no normalization row is added. Minimum and maximum are IsLeast and IsGreatest of explicitly defined value sets, never sSup/sInf, so an empty ambiguity set or an unbounded inner problem cannot produce a junk value; nonemptiness of the ambiguity set at every feasible state is the theorem's hypothesis, as on the page. An empty stage set makes both sides of the equivalence false rather than vacuously true, so it does not trivialize the goal. The objective (7a) is transcribed term by term.

Contributions welcome: proofs of the two duality milestones (from the platform's LP duality or directly from Farkas' lemma in Mathlib), the transfer argument for Theorem 1, and the specialization (7).

Selected references

• X. Yu, S. Shen, Multistage distributionally robust mixed-integer programming with decision-dependent moment-based ambiguity sets, arXiv:2002.12518v3, 2020; Mathematical Programming, 2020. https://arxiv.org/abs/2002.12518
• F. Luo, S. Mehrotra, Distributionally robust optimization with decision dependent ambiguity sets, Optimization Letters, 2020. https://arxiv.org/abs/1806.09215
• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Mathematical Programming 175, 2019. https://doi.org/10.1007/s10107-018-1249-5
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 4.4.

Motivation

In many multistage decision problems the probability law of the next uncertainty depends on the decision taken now: opening a facility changes the demand it attracts, a price changes the distribution of sales, maintenance changes failure rates. Distributionally robust optimization (DRO) handles an imperfectly known law by optimizing against the worst distribution in an ambiguity set. When that set itself moves with the decision, the model is decision-dependent, and the classical reformulations, which treat the ambiguity set as fixed, do not apply directly.

X. Yu and S. Shen (arXiv:2002.12518v3, 2020; Math. Program., DOI 10.1007/s10107-020-01580-4) study multistage mixed-integer DRO with binary state variables and decision-dependent moment-based ambiguity sets over a finite support. Their Theorems 1–3 turn each stage's min–max Bellman equation into a single minimization, which is the input to a stochastic dual dynamic integer programming (SDDiP) algorithm. This mission covers their main result, Theorem 3, for the most general of their three sets: a Delage–Ye-type set in which the mean lies in an ellipsoid around a decision-dependent estimate and the centred second-moment matrix is bounded by a decision-dependent matrix.

Timeline. Delage and Ye (Oper. Res., 2010, DOI 10.1287/opre.1090.0741) introduced the ellipsoid-plus-second-moment set for a decision-independent law and gave a semidefinite reformulation. Luo and Mehrotra (Optim. Lett., 2020) derived duality-based reformulations for decision-dependent moment sets in a single stage. Yu and Shen (2020) carry these into the multistage mixed-integer setting with binary states.

Setting

Fix one stage $t$. The data are:

• a stage feasible set $S \subseteq \{0,1\}^I \times \mathbb R^{I\times J}$ of pairs $(x, y)$ (state and stage variable) and a stage cost $g(x,y)$;
• a finite support $\xi^1, \dots, \xi^K \in \mathbb R^J$ of the next-stage random vector (the same for every decision);
• next-stage values $Q^k(x) = Q_{t+1}(x, \xi^k)$;
• a decision-dependent mean estimate $\mu(x) \in \mathbb R^J$, a matrix $\Sigma(x) \in \mathbb R^{J\times J}$ (written Sig in Lean), and size parameters $\gamma, \eta \in \mathbb R$.

For weights $p \in \mathbb R^K$ write $M_k(x) = (\xi^k - \mu(x))(\xi^k - \mu(x))^\top$ and $\bar\xi(p) = \sum_k p_k \xi^k$. The Type 3 ambiguity set (14) is

$$\mathcal P^{D_3}(x) = \Big\{ p \ge 0 : \sum_k p_k = 1,\ (\bar\xi(p) - \mu(x))^\top \Sigma(x)^{-1} (\bar\xi(p) - \mu(x)) \le \gamma,\ \sum_k p_k M_k(x) \preceq \eta\,\Sigma(x) \Big\}.$$

The stage Bellman equation (2) is

$$Q_t = \min_{(x,y) \in S} \Big\{ g(x,y) + \max_{p \in \mathcal P^{D_3}(x)} \sum_k p_k Q^k(x) \Big\}.$$

Write $A \bullet B = \operatorname{tr}(A^\top B)$ for the Frobenius product.

Formalization targets

Goal: Theorem 3 (p. 12)

Assume that for every feasible $(x,y) \in S$, $\Sigma(x) \succ 0$, and that Slater's condition holds: some probability vector $p$ satisfies the ellipsoid constraint strictly and $\sum_k p_k M_k(x) \prec \eta\,\Sigma(x)$. Then the minimum of the Bellman equation exists exactly when the minimum of the mixed-integer semidefinite program (15) exists, and the two are equal:

$$\min_{x,y,s,Z,Y}\ g(x,y) + s + \Sigma(x)\bullet z_1 - 2\mu(x)^\top z_2 + \gamma z_3 + \eta\,\Sigma(x)\bullet Y$$

subject to $s - 2 z_2^\top \xi^k + M_k(x) \bullet Y \ge Q^k(x)$ for all $k$, $Z = \begin{pmatrix} z_1 & z_2 \\ z_2^\top & z_3 \end{pmatrix} \succeq 0$, $Y \succeq 0$, and $(x,y) \in S$.

Milestones (proof of Theorem 3, pp. 37–39)

1. The ellipsoid constraint (C-20d) is equivalent to $\begin{pmatrix} \Sigma(x) & \tau-\mu(x) \\ (\tau-\mu(x))^\top & \gamma \end{pmatrix} \succeq 0$.
2. The Lagrangian identity (C-21).
3. The dual function: maximizing the Lagrangian over $p \ge 0$, $\tau \in \mathbb R^J$ gives the stated objective under the stated constraints, and $+\infty$ otherwise.
4. Weak duality: every $p \in \mathcal P^{D_3}(x)$ is bounded by every dual-feasible objective value.
5. Strong duality (C-22) under Slater, with both sides attained.

A companion statement from §4.2.2 (p. 15) is also included: the cones $DD(U)$ built from diagonally dominant matrices consist of positive semidefinite matrices.

Significance

The result. Theorem 3 replaces a min–max problem, whose inner maximum ranges over a set that moves with $x$, by one minimization in which $x$ enters only through the data $\mu(x)$, $\Sigma(x)$. With affine $\mu$, $\Sigma$ and binary $x$, the bilinear terms can then be linearized, giving the mixed-integer SDP (16)–(17) to which the paper applies SDDiP-type cutting planes. Without the reformulation there is no single-level stage problem to generate cuts from.

Formalizing it. The result is proved on paper; it has no machine-checked proof that we know of. The proof in the paper is brief: it cites convexity and Slater for strong duality and does not check that the domain $p \ge 0$, the Schur-complement rewrite and the strict inequalities fit the conic duality theorem it relies on. A formal proof checks these points, and the per-stage duality lemmas (milestones 4 and 5) can be reused by any moment-based DRO model over a finite support.

Difficulty

Weak duality and the regrouping of the Lagrangian are routine. The difficulty is strong duality with dual attainment (milestone 5): the inner problem has an inverse-matrix constraint and a semidefinite constraint, and the duality theorem must be applied to the conic form after the Schur rewrite, with a Slater point of that form. The paper states Slater for "a vector $p$". A Slater point with negative entries does not lie in the domain $p \ge 0$, so it gives no interior point there. Passing from per-state duality to the equality of the two outer minima also needs care: the Bellman minimum is over pairs at which the inner maximum is attained, and the reformulated minimum is a joint minimization over $(x, y)$ and the dual variables.

Formalization scope

• Indices are 0-based (Fin I, Fin J, Fin K). States are Fin I → ℝ, the support is ξ : Fin K → Fin J → ℝ, and $\Sigma$, $Z$, $Y$ are Mathlib matrices. $\succeq$ and $\succ$ are PosSemidef/PosDef of the difference (both include symmetry). The block $Z$ is indexed by Fin J ⊕ Unit, with the same $z_2$ in both off-diagonal blocks.
• Minima and maxima are IsLeast/IsGreatest on sets of values, so attainment is part of every claim. The goal reads: for all $q$, $q$ is the least stage value iff $q$ is the least value of (15).
• Added hypotheses, disclosed: $\Sigma(x) \succ 0$ at feasible $x$ (implicit on the page, which writes $\Sigma(x)^{-1}$; Mathlib's inverse of a singular matrix is $0$). $p \ge 0$ in the ambiguity set ((C-20f); Assumption 3 calls $p$ a probability). The Slater point is a probability vector (Theorem A.3 says "a probability measure").
• Dropped hypotheses, disclosed generalization: linearity of $g$ and compactness and polyhedrality of $S$ are not used. $\mu$ and $\Sigma$ are arbitrary functions of $x$; the affine form (12) is imposed only later in the paper. $Q^k$ is an arbitrary real function, because the stage theorem uses nothing about the recursion. Binary states are kept as a hypothesis.
• Printed text not copied: the Slater clause of Theorem 3 is cut at the right margin of p. 12 and is restored from Theorem B.6 (p. 36). "$u \in \mathbb R^d$" on p. 38 is read as $u \in \mathbb R^J$.
• No trivializing reading: the strict inequalities of Slater are kept, since non-strict ones would make the theorem false. No sSup/sInf values are used, so there are no junk values. An empty $S$ makes both sides empty, so the equivalence carries no content there. A sorry-free check confirms that the hypotheses are satisfiable on a two-point instance with value 3.
• Needed infrastructure: Schur complements for positive definite blocks (in Mathlib), the trace inequality for products of PSD matrices, and a conic strong-duality theorem with dual attainment under Slater for semidefinite constraints. Contributions of the last as a reusable lemma are welcome.

Selected references

• X. Yu, S. Shen, Multistage distributionally robust mixed-integer programming with decision-dependent moment-based ambiguity sets, arXiv:2002.12518v3, 2020; Math. Program., 2020. https://arxiv.org/abs/2002.12518
• E. Delage, Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Oper. Res. 58(3), 2010. https://doi.org/10.1287/opre.1090.0741
• F. Luo, S. Mehrotra, Distributionally robust optimization with decision dependent ambiguity sets, Optimization Letters, 2020, pp. 1–30 (as cited by Yu & Shen).
• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Math. Program. 175, 2019. https://doi.org/10.1007/s10107-018-1249-5
• A. A. Ahmadi, G. Hall, Sum of squares basis pursuit with linear and second order cone programming, Algebraic and Geometric Methods in Discrete Mathematics, Contemp. Math. 685, 27–53, 2017 (as cited by Yu & Shen).

Motivation

Many planning problems are solved in stages. A decision is taken, uncertainty is revealed, and the next decision reacts to it. Facility location, capacity expansion and network design all fit this pattern. In a growing class of such problems, the distribution of the uncertainty depends on the decision: opening a facility changes the demand it attracts, and a maintenance decision changes the failure rates that follow. Stochastic programs with decision-dependent uncertainty go back to Jonsbråten, Wets and Woodruff (1998) and Goel and Grossmann (2006).

When the distribution is not known exactly, distributionally robust optimization (DRO) optimizes against the worst distribution in an ambiguity set of plausible ones. Moment-based ambiguity sets, which are defined by constraints on the mean and covariance, are one of the standard choices (Delage and Ye, 2010). Luo and Mehrotra (2020) studied single-stage DRO in which such moment sets depend on the decision. Yu and Shen (2020) carry this into the multistage mixed-integer setting. Their goal is to rewrite each stage's min–max Bellman equation as one minimization, so that the stagewise decomposition algorithm SDDiP (Zou, Ahmed and Sun, 2019) applies.

This mission formalizes their reformulation for the Type 2 ambiguity set, which matches a decision-dependent mean and covariance exactly.

Setting

Fix a stage $t$. The decision at stage $t$ is a pair $(x_t,y_t)$: a binary state $x_t\in\{0,1\}^I$, passed to the next stage, and a stage variable $y_t\in\mathbb R^{I\times J}$. The pair must lie in a stage feasible set $S=X_t(x_{t-1},\xi_t)$ and costs $g_t(x_t,y_t)$.

The next-stage random vector $\xi_{t+1}\in\mathbb R^J$ takes one of finitely many values $\xi^1_{t+1},\dots,\xi^K_{t+1}$. This support is fixed (Assumption 3), and only the probabilities $p=(p_1,\dots,p_K)$ are uncertain. The value of being in state $x_t$ when scenario $k$ occurs is $Q^k_{t+1}=Q_{t+1}(x_t,\xi^k_{t+1})$.

The decision determines a mean $\mu(x_t)\in\mathbb R^J$ and a covariance matrix $\Sigma(x_t)\in\mathbb R^{J\times J}$. The Type 2 ambiguity set is the set of probability vectors that match them exactly:

$$\mathcal P^{D_2}_{t+1}(x_t)=\Big\{p\in\mathbb R^K_{\ge 0}:\ \sum_{k}p_k=1,\ \ \sum_k p_k\xi^k_{t+1}=\mu(x_t),\ \ \sum_k p_k(\xi^k_{t+1}-\mu(x_t))(\xi^k_{t+1}-\mu(x_t))^\top=\Sigma(x_t)\Big\}.$$

The Bellman equation (2) of stage $t$ is

$$Q_t(x_{t-1},\xi_t)=\min_{(x_t,y_t)\in S}\Big\{g_t(x_t,y_t)+\max_{p\in\mathcal P^{D_2}_{t+1}(x_t)}\sum_{k=1}^Kp_kQ^k_{t+1}\Big\}.$$

Throughout, $A\bullet B=\operatorname{trace}(A^\top B)$ is the Frobenius inner product.

Formalization targets

Goal: Theorem 2 (p. 11)

If $\mathcal P^{D_2}_{t+1}(x_t)$ is nonempty for every feasible $x_t$, then

$$\begin{aligned} Q_t(x_{t-1},\xi_t)=\min_{x_t,y_t,s,u,Y}\ & g_t(x_t,y_t)+s+u^\top\mu(x_t)+\Sigma(x_t)\bullet Y\\ \text{s.t. }\ & s+u^\top\xi^k_{t+1}+(\xi^k_{t+1}-\mu(x_t))(\xi^k_{t+1}-\mu(x_t))^\top\bullet Y\ge Q^k_{t+1}\quad\forall k,\\ & (x_t,y_t)\in S,\ s\in\mathbb R,\ u\in\mathbb R^J,\ Y\in\mathbb R^{J\times J}. \end{aligned}$$

The left side is a minimum exactly when the right side is, and the two values agree.

Milestones (proof of Theorem 2, p. 37)

1. Weak duality. For every $p\in\mathcal P^{D_2}_{t+1}(x)$ and every $(s,u,Y)$ satisfying the constraints above at $x$,

$$\sum_k p_kQ^k_{t+1}\le s+u^\top\mu(x)+\Sigma(x)\bullet Y.$$

2. Strong duality. If $\mathcal P^{D_2}_{t+1}(x)\neq\emptyset$, both sides are attained and the two optimal values are equal.

Significance

The theorem turns a min–max problem into a single minimization. Under the paper's affine model (12) for $\mu$ and $\Sigma$, and with McCormick envelopes for the products of binary states and continuous duals, that minimization becomes a mixed-integer linear program. SDDiP can then solve the multistage model stage by stage, with valid cuts. The Type 2 set is the paper's middle case. It captures correlations between the components of $\xi_{t+1}$, which the separate moment bounds of the Type 1 set (Theorem 1) cannot, and it still has an LP dual. The Type 3 set of Theorem 3 instead leads to a semidefinite program.

The result is proved in the paper: Appendix C gives a short argument by linear-programming duality. It has not been formalized. A formal proof pins down details the printed proof leaves implicit:

• the nonnegativity constraint, which (10) omits;
• that the dual matrix $Y$ is unrestricted;
• that both optima are attained.

It also yields a reusable, machine-checked instance of LP duality for moment-matching problems on a finite support.

Difficulty

There are two steps. The first is linear-programming strong duality for the inner problem in matrix-valued form. Its constraints are a scalar equation, a vector equation in $\mathbb R^J$ and a matrix equation in $\mathbb R^{J\times J}$, so the dual variables are a scalar, a vector and a matrix, paired through dot and Frobenius products. Turning this into a standard-form LP to which a library duality theorem applies takes bookkeeping. The second step is the exchange of the outer minimum with the dual minimum. Here attainment matters: the inner maximum must be attained at every feasible $x_t$, and the stated equality must hold both when the outer minimum exists and when it does not. Weak duality alone gives only one inequality. The naive argument "dualize and combine" also hides the fact that, without $p\ge0$, the dual constraints would have to be equalities.

Formalization scope

• Indices and types. States are Fin I → ℝ, stage variables are Fin I → Fin J → ℝ, the support is ξ : Fin K → Fin J → ℝ, and the next-stage values are an arbitrary function Qn x k. The theorem uses nothing about the recursion that defines $Q_{t+1}$. The covariance map is named Sig.
• Minima and maxima. These are least and greatest elements of value sets (IsLeast, IsGreatest), never sInf/sSup. The goal states that $q$ is the least stage value if and only if $q$ is the least value of (11). An empty stage set, or an empty ambiguity set, cannot make the statement hold by default values. The ambiguity set is never empty at a feasible state, because that is the theorem's hypothesis, and an empty stage set makes both sides false.
• Hypotheses added or dropped.
  • The ambiguity set includes $p\ge0$. This is (C-18e) of the paper's proof; (10) as printed omits it.
  • $Y$ is a free real matrix.
  • The standing assumptions that $g_t$ is linear and $S$ is a nonempty compact mixed-integer polyhedron are not imposed, since the theorem holds for every $S$ and $g_t$. The binary state is kept as a hypothesis.
  • No symmetry or definiteness is assumed of $\Sigma(x)$.
  • The affine forms (12) are not imposed; they are used only afterwards, for the MILP.
• Infrastructure. Finite-dimensional LP duality with equality constraints and a nonnegative variable, transported to vector and matrix constraints. Statements of LP strong duality already exist on the platform and may be used as tools. Contributions welcome: a proof of each milestone, a general "finite-support moment-matching duality" lemma, and the attainment argument.

Selected references

• X. Yu, S. Shen, Multistage distributionally robust mixed-integer programming with decision-dependent moment-based ambiguity sets, arXiv:2002.12518v3, 2020; Mathematical Programming. https://arxiv.org/abs/2002.12518
• E. Delage, Y. Ye, Distributionally robust optimization under moment uncertainty with application to data-driven problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• F. Luo, S. Mehrotra, Distributionally robust optimization with decision dependent ambiguity sets, Optimization Letters, 2020. https://arxiv.org/abs/1806.09215
• J. Zou, S. Ahmed, X. A. Sun, Stochastic dual dynamic integer programming, Mathematical Programming 175(1–2):461–502, 2019. https://doi.org/10.1007/s10107-018-1249-5
• V. Goel, I. E. Grossmann, A class of stochastic programs with decision dependent uncertainty, Mathematical Programming 108(2–3):355–394, 2006. https://doi.org/10.1007/s10107-005-0658-4
• T. W. Jonsbråten, R. J.-B. Wets, D. L. Woodruff, A class of stochastic programs with decision dependent random elements, Annals of Operations Research 82:83–106, 1998. https://doi.org/10.1023/A:1018943626786

Motivation

First order methods (projected gradient, fast gradient) converge only sublinearly on general smooth convex problems, at rates $O(1/k)$ and $O(1/k^2)$ in function value. Linear convergence is classically proved under strong convexity, which fails for many problems arising in practice: least squares with a rank-deficient matrix, dual problems of linearly constrained programs, and compositions $f(x)=g(Ax)$ of a strongly convex $g$ with a singular linear map. For such problems the optimal set is not a single point, yet projected gradient methods are still observed to converge linearly.

Necoara, Nesterov and Glineur (arXiv:1504.06298, later Math. Program. 175 (2019)) introduce a hierarchy of relaxations of strong convexity, each obtained by evaluating a strong convexity inequality only at the projection of a point onto the optimal set, and show that first order methods converge linearly on each class. Two of these relaxations are the subject of this mission: quadratic functional growth and the global error bound stated with the gradient mapping. Error bounds of this kind go back to Luo and Tseng (Ann. Oper. Res. 46 (1993)) and Tseng's analysis of feasible descent methods; quadratic growth conditions appear in Anitescu and in Drusvyatskiy–Lewis (Math. Oper. Res. 43 (2018)).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $\langle u,v\rangle=u^\top v$ and norm $\|\cdot\|$. Problem (P) is

$$f^*=\min_{x\in X} f(x),$$

with $X\subseteq\mathbb R^n$ closed and convex and $f$ convex on $X$, differentiable on $X$, with Lipschitz continuous gradient of constant $L_f>0$ on $X$: $\|\nabla f(x)-\nabla f(y)\|\le L_f\|x-y\|$ for all $x,y\in X$. The optimal set $X^*=\{x\in X: f(x)\le f(y)\ \forall y\in X\}$ is assumed nonempty.

For a set $S$ and a point $u$, $[u]_S$ denotes a point of $S$ nearest to $u$; for nonempty closed convex $S$ it exists and is unique. Write $\bar x=[x]_{X^*}$. The projected gradient step from $x\in X$ is $x^+=[x-\tfrac1{L_f}\nabla f(x)]_X$, and the gradient mapping is

$$g(x)=L_f\,(x-x^+).$$

When $X=\mathbb R^n$, $g(x)=\nabla f(x)$.

• $f$ has quadratic functional growth (22) with constant $\kappa_f>0$ if $f(x)-f^*\ge\frac{\kappa_f}{2}\|x-\bar x\|^2$ for all $x\in X$.
• $f$ satisfies the global error bound (31) with constant $\kappa_f>0$ if $\|g(x)\|\ge\kappa_f\|x-\bar x\|$ for all $x\in X$.

The condition number is $\mu_f=\kappa_f/L_f$. In Lean these are QuadFunGrowth X f κ and ErrorBound X f Lf κ, with $g(x)$ written Lf • (x - xp).

Formalization targets

Goal: Theorem 7

Quadratic functional growth with constant $\kappa_f$ implies the global error bound with constant $\frac{1}{1+\mu_f+\sqrt{1+\mu_f}}\cdot\kappa_f$:

$$\|g(x)\|\ \ge\ \frac{\kappa_f}{1+\mu_f+\sqrt{1+\mu_f}}\,\|x-\bar x\|\qquad\forall x\in X .$$

In class notation, $\mathcal F_{L_f,\kappa_f}(X)\subseteq\mathcal E_{L_f,\kappa_f/(1+\mu_f+\sqrt{1+\mu_f})}(X)$.

Milestones

1. The decrease (28) of a projected gradient step: $f(x^+)\le f(x)-\frac{L_f}{2}\|x^+-x\|^2$.
2. The gradient mapping inequality (29): $f(y)\ge f(x^+)+\langle g(x),y-x\rangle+\frac{1}{2L_f}\|g(x)\|^2$ for $y\in X$.
3. The first chain of the proof of Theorem 7: with $\bar x^+=[x^+]_{X^*}$, $\langle g(x),x^+-\bar x^+\rangle+\frac1{2L_f}\|g(x)\|^2\ge f(x^+)-f^*\ge\frac{\kappa_f}{2}\|x^+-\bar x^+\|^2$.
4. The error bound at $x^+$: $\|g(x)\|\ge\bigl(\sqrt{L_f(\kappa_f+L_f)}-L_f\bigr)\|x^+-\bar x^+\|$.

Companion: Theorem 6

The converse direction, also included as a draft theorem: the error bound with $\kappa_f$ implies quadratic functional growth with constant $\mu_f\cdot\kappa_f$.

Significance

Theorems 6 and 7 together show that, for convex functions with Lipschitz gradient on a closed convex set, quadratic functional growth and the gradient-mapping error bound define the same class of functions up to a change of constant depending only on $\mu_f$. A linear convergence proof for projected gradient methods under one condition therefore transfers to the other, and the paper uses this to place the error-bound class $\mathcal E$ inside its hierarchy of relaxations of strong convexity. The explicit constant matters downstream: rates of the form $(1-c\,\mu_f)^k$ inherit it.

The results are proved in the paper. No machine-checked proof of Theorems 6–7 is known to exist. Related statements formalized elsewhere on the platform concern the unconstrained case (Karimi–Nutini–Schmidt, where $\nabla f$ replaces $g$) or the proximal-gradient error bound on sublevel sets (Drusvyatskiy–Lewis), with different constants. A complete development here yields a reusable library of projected-gradient facts on a general closed convex set: the descent inequality, the gradient-mapping inequality and the existence and characterization of projections.

Difficulty

The obvious approach applies (22) at $x$ and tries to bound $f(x)-f^*$ by $\|g(x)\|\,\|x-\bar x\|$, as in the unconstrained case where $g=\nabla f$ and convexity gives $f(x)-f^*\le\langle\nabla f(x),x-\bar x\rangle$. On a constrained set this fails: $g(x)$ is not a subgradient of $f$ at $x$, and the available inequality for the gradient mapping, (29), controls $f$ only through the value $f(x^+)$ at a different point. Relating the distance to $X^*$ at that point to the distance at $x$, without losing the exact constant $\kappa_f/(1+\mu_f+\sqrt{1+\mu_f})$, is the central difficulty.

At the Lean level, the descent inequality (2) has to be derived on a convex set from a Lipschitz condition assumed only on $X$, and the variational characterization of the Euclidean projection has to be connected to the nearest-point predicate.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $f$ is a real function on all of $\mathbb R^n$, convex on $X$ (ConvexOn ℝ X f), differentiable at every point of $X$, with $\nabla f$ = gradient f; its values off $X$ never enter.
• Standing assumptions of p. 3 as hypotheses: $X$ closed and convex; (1) on $X$ with $0<L_f$; a named optimal point $x^\star\in X^*$, so $X^*$ is never empty. The paper's "simple" (cheap projection) is not a mathematical assumption and is dropped; "closed convex function" adds nothing for a real-valued convex function continuous on $X$. $X^*$ closed and $f^*$ finite follow and are not assumed.
• Projections are predicates (IsNearest), not choice functions; $x^+$ is the predicate IsPGStep. Every statement quantifies over all points satisfying them. Nearest points in nonempty closed convex sets exist, so these quantifiers are not vacuous.
• $f^*$ is written $f(\bar x)$ for $\bar x\in X^*$, never as an infimum.
• The constant of Theorem 7 is written $\kappa/(1+\kappa/L_f+\sqrt{1+\kappa/L_f})$, of Theorem 6 $\kappa/L_f\cdot\kappa$. $\kappa_f\le L_f$ is not assumed.
• (29) is stated for $x\in X$ rather than $x\in\mathbb R^n$, since $\nabla f$ is only meaningful on $X$ under the standing assumptions.

A trivializing formalization is ruled out: the error bound uses the gradient mapping $g(x)$ and not $\nabla f(x)$, the projections are not defined by choice, $X^*$ is nonempty, and no junk gradient value off the differentiability set is used.

Needed infrastructure: the descent lemma on a convex set, the obtuse-angle characterization of the projection onto a closed convex set, existence of nearest points (Mathlib's exists_norm_eq_iInf_of_complete_convex), and closedness and convexity of $X^*$. These are reusable well beyond this mission; proofs of the milestones and of Theorem 6 are welcome independently.

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
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004, Theorem 2.2.7. 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
• D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Math. Oper. Res. 43 (2018) 919–948. https://doi.org/10.1287/moor.2017.0889
• 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

Motivation

Linear convergence of gradient-type methods is classically proved under strong convexity. Many problems that arise in practice are not strongly convex: dual formulations of linearly constrained convex problems, least-squares and logistic-type regression with rank-deficient data matrices, convex quadratic programs, and routing problems in data networks all have objectives of the form $f(x)=g(Ax)$, where $g$ is strongly convex and smooth but the matrix $A$ has a nontrivial kernel. Such an $f$ is constant along $\ker A$, so it is not strongly convex, and its set of minimizers need not be a single point.

Necoara, Nesterov and Glineur (arXiv:1504.06298v4, published in Math. Program. 175 (2019)) introduce a chain of relaxations of strong convexity: quasi-strong convexity, quadratic gradient growth and quadratic functional growth. They show that projected and fast gradient methods still converge linearly under them. Section 4 of the paper supplies the main examples: compositions $g(Ax)$, possibly with a linear term and polyhedral constraints. This mission formalizes those examples. The tool behind them is the error bound of Hoffman (1952) for systems of linear inequalities; its use for linear convergence goes back to Luo and Tseng (1993) and Wang and Lin (2014).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $\langle u,v\rangle=u^Tv$ and norm $\|\cdot\|$. For a set $X$ and a function $f$, the optimal set is $X^*=\{x\in X: f(x)\le f(y)\ \forall y\in X\}$ and $f^*$ is the optimal value. A nearest point $\bar x=[x]_S$ of a set $S$ to $x$ is a point of $S$ minimizing $\|x-z\|$ over $z\in S$.

The data are:

1. a linear map $A:\mathbb R^n\to\mathbb R^m$, $A\neq0$, with operator (spectral) norm $\|A\|$;
2. a polyhedral feasible set $X=\{x: Cx\le d\}$, with $C:\mathbb R^n\to\mathbb R^p$ linear and the inequality read componentwise;
3. a differentiable function $g:\mathbb R^m\to\mathbb R$ that is $\sigma_g$-strongly convex, $g(\alpha u+(1-\alpha)v)\le\alpha g(u)+(1-\alpha)g(v)-\frac{\sigma_g\alpha(1-\alpha)}2\|u-v\|^2$, and whose gradient is $L_g$-Lipschitz.

The objective is $f(x)=g(Ax)$, or $f(x)=g(Ax)+c^Tx$ in the extensions. The function $f$ has Lipschitz gradient with constant $L_f$ on $X$ if $\|\nabla f(x)-\nabla f(y)\|\le L_f\|x-y\|$ for $x,y\in X$. It is quasi-strongly convex with constant $\kappa$ if, for every $x\in X$ and $\bar x=[x]_{X^*}$,

$$f^*\ge f(x)+\langle\nabla f(x),\bar x-x\rangle+\tfrac\kappa2\|x-\bar x\|^2 .$$

The class $q\mathcal S_{L_f,\kappa_f}(X)$ collects the convex functions with $L_f$-Lipschitz gradient on $X$ satisfying this inequality with $\kappa_f$. The classes $\mathcal G_{L_f,\kappa_f}$ (quadratic gradient growth, $\langle\nabla f(x)-\nabla f(\bar x),x-\bar x\rangle\ge\kappa\|x-\bar x\|^2$) and $\mathcal F_{L_f,\kappa_f}$ (quadratic functional growth, $f(x)-f^*\ge\frac\kappa2\|x-\bar x\|^2$) are defined the same way.

A Hoffman constant $\theta(A,C)>0$ for the polyhedron $P=\{z: Az=t,\ Cz\le d\}$ is a number with

$$\|x-\bar x\|\le\theta(A,C)\sqrt{\|Ax-t\|^2+\|[Cx-d]_+\|^2}\qquad\forall x\in\mathbb R^n,\ \bar x=[x]_P ,$$

where $[v]_+$ is the componentwise positive part.

Formalization targets

Goal: Theorem 8

If $x^*$ is optimal for $\min_{x\in X}g(Ax)$ and $\theta(A,C)>0$ is a Hoffman constant for $\{z: Az=Ax^*,\ Cz\le d\}$, then

$$f=g\circ A\in q\mathcal S_{L_f,\kappa_f}(X),\qquad L_f=L_g\|A\|^2,\qquad \kappa_f=\frac{\sigma_g}{\theta^2(A,C)} .$$

Milestones

1. $\|\nabla f(x)-\nabla f(y)\|\le L_g\|A\|^2\|x-y\|$ on $X$.
2. (39): $Ax^*$ and $\nabla f(x^*)$ are the same for every $x^*\in X^*$.
3. $X^*=\{x: Ax=Ax^*,\ Cx\le d\}$.
4. For feasible $x$, $\|x-\bar x\|\le\theta(A,C)\|Ax-A\bar x\|$.

Companions

• Theorem 9: without constraints, $g(Ax)+c^Tx\in\mathcal G_{L_g\|A\|^2,\ \sigma_g/\theta^2(A,0)}(\mathbb R^n)$.
• Theorem 10: on $X=\{Cx\le d\}$ and for every $M>0$, $g(Ax)+c^Tx\in\mathcal F_{L_f,\kappa_f}(X_M)$ on the sublevel set $X_M=\{x\in X: f(x)-f^*\le M\}$, with $\kappa_f=\sigma_g/\big(\theta^2(A,c,C)(1+M\sigma_g+2c_g^2)\big)$ and $c_g=\|\nabla g(Ax^*)\|$.
• Example 1: $\tfrac12x_1^2+x_2$ on $\mathbb R^2_+$ has no global quadratic growth constant, but $\kappa_f(M)=\min\{1,1/M\}$ works on $\{f\le M\}$ for $M\ge1$.

Significance

Theorem 8 makes the linear convergence results of the paper apply to the whole family $g(Ax)$ over polyhedra. That family covers the duals of linearly constrained strongly convex problems and regression with arbitrary design matrices. The rate is explicit in $\sigma_g$, $L_g$, $\|A\|$ and the Hoffman constant. Theorems 9 and 10 extend the picture to a linear term, at the cost of moving to weaker classes. Example 1 shows that the sublevel restriction in Theorem 10 is needed.

All of these results are proved in the paper. None of them has a machine-checked proof that this mission is aware of. A formal development would produce a Lean proof of the class membership, a formal chain-rule computation of the gradient of $g\circ A$, and the strict-convexity argument that $A$ is constant on the optimal set. These pieces are reusable wherever a composite objective with a rank-deficient linear map appears.

Difficulty

The obvious route, strong convexity of $f$, fails as soon as $\ker A\neq\{0\}$. Two separate facts have to replace it. The first is that the minimizers of a strongly convex function composed with $A$ share the image point $Ax^*$, so the optimal set is itself a polyhedron. The second is that the distance to that polyhedron is controlled linearly by the residual $\|Ax-Ax^*\|$ on feasible points, which is exactly a Hoffman error bound. Neither follows from local information at a single minimizer. In Theorem 10 the linear term destroys the first fact's simplicity: the value $c^Tx$ must also be controlled, and that is possible only on bounded sublevel sets.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $A$ and $C$ are continuous linear maps, so $\|A\|$ is the operator norm, which is the spectral norm of the page; it is never the Frobenius norm. Strong convexity is Mathlib's StrongConvexOn Set.univ σg g, which is (5) on all of $\mathbb R^m$. The page's "$L_g$-Lipschitz gradient on $X$" is read on $\mathbb R^m$, the domain of $g$. The gradient of the composition is always gradient (fun z => g (A z)), and the identity $\nabla f(x)=A^T\nabla g(Ax)$ is a proof step, not part of any statement. $f^*$ is the value at a nearest point of $X^*$, which is exact because that point is optimal.

Standing assumptions of p. 3: the feasible set is closed and convex (automatic for a polyhedron), the optimal set is nonempty (a named optimal point $x^*$ is a hypothesis), and $f$ has Lipschitz gradient (a conclusion here). The "simple" set and "closed" function add no mathematical content and are dropped. The Hoffman constant is a hypothesis, because the page cites its existence (Hoffman 1952) rather than proving it. The hypothesis is the Hoffman inequality for the specific polyhedron $\{Az=Ax^*,\ Cz\le d\}$, not for every right-hand side.

Trivializing formalizations are ruled out. The projection is a predicate (IsNearest), never a choice function. The optimal set is nonempty by hypothesis. $g$ is differentiable everywhere, so no gradient takes a junk value. A sorry-free sanity file shows that the hypotheses of Theorems 8–10 are jointly satisfiable ($A=\mathrm{id}$ on $\mathbb R^1$, $g=\|\cdot\|^2/2$, $\theta=1$).

A complete development needs the chain rule for gradients through a continuous linear map and its adjoint, first-order characterizations of strong convexity, and optimality conditions for convex differentiable functions on convex sets. Contributions of these as reusable lemmas are welcome, as are proofs of the companion theorems.

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
• A. J. Hoffman, On approximate solutions of systems of linear inequalities, J. Res. Nat. Bur. Standards 49 (1952) 263–265. https://doi.org/10.6028/jres.049.027
• 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
• P.-W. Wang, C.-J. Lin, Iteration complexity of feasible descent methods for convex optimization, J. Mach. Learn. Res. 15 (2014) 1523–1548. https://jmlr.org/papers/v15/wang14a.html
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9