Operations Research

Motivation

Coordinate descent methods update one block of variables at a time. They are the method of choice when the number of variables is so large that even one full gradient is too expensive, while a single partial derivative is cheap: support vector machines, $\ell_1$-regularized regression, and large sparse least-squares problems are the standard examples. Yu. Nesterov's paper Efficiency of coordinate descent methods on huge-scale optimization problems (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012), doi:10.1137/100802001) gave the first global efficiency estimates for randomized coordinate descent, and these estimates started a large literature on random coordinate and block methods.

Many applications carry simple constraints on each block: bounds on each variable, a simplex or a ball per block. Section 4 of the paper shows that randomized coordinate descent handles such block-separable constraints at no loss: a projected block step, chosen uniformly at random, enjoys the same $O(n/k)$ expected rate as the unconstrained method, and a linear rate under strong convexity. This mission formalizes that result, Theorem 5.

Setting

The space $\mathbb R^N$ is split into $n\ge1$ blocks, $\mathbb R^N=\mathbb R^{n_1}\times\cdots\times\mathbb R^{n_n}$ with $N=\sum_in_i$ and every $n_i\ge1$. A point $x$ is the family of its blocks $x^{(i)}\in\mathbb R^{n_i}$, and $U_ih$ is the point whose $i$-th block is $h$ and whose other blocks are zero. Each block carries a Euclidean norm $\|h\|_{(i)}^2=\langle B_ih,h\rangle$ with $B_i\succ0$ (3.4).

The objective $f:\mathbb R^N\to\mathbb R$ is convex and differentiable, and its gradient is coordinate-wise Lipschitz (2.2): writing $f'_i(x)=U_i^T\nabla f(x)$ for the $i$-th block of the gradient, there are constants $L_i>0$ with

$$\|f'_i(x+U_ih)-f'_i(x)\|^*_{(i)}\le L_i\|h\|_{(i)}\quad\text{for all }x,\ i,\ h .$$

The weighted norm is $\|x\|_1^2=\sum_iL_i\|x^{(i)}\|_{(i)}^2$ (3.5). The function $f$ is strongly convex in $\|\cdot\|_1$ with constant $\sigma>0$ if $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\sigma2\|y-x\|_1^2$ for all $x,y$ (3.1).

The problem is (4.1), $\min_{x\in Q}f(x)$ with $Q=Q_1\times\cdots\times Q_n$ and each $Q_i\subseteq\mathbb R^{n_i}$ nonempty, closed and convex. Its optimal value is $f^*$, attained at an optimal solution $x_*\in Q$. The constrained coordinate update (4.2) is

$$u^{(i)}(x)=\arg\min_{u\in Q_i}\Big[\langle f'_i(x),u-x^{(i)}\rangle+\tfrac{L_i}2\|u-x^{(i)}\|_{(i)}^2\Big],\qquad V_i(x)=x+U_i\big(u^{(i)}(x)-x^{(i)}\big).$$

The uniform coordinate descent method UCDM$(x_0)$ (4.5) draws $i_k$ uniformly from $\{1,\dots,n\}$ and sets $x_{k+1}=V_{i_k}(x_k)$. Its expected objective is $\varphi_k=\mathbb E f(x_k)$, the expectation over $i_0,\dots,i_{k-1}$. The level-set radius $R_1(x_0)$ is the largest $\|\cdot\|_1$-distance between a feasible $x$ with $f(x)\le f(x_0)$ and an optimal solution.

Formalization targets

Goal: Theorem 5

For every $k\ge0$,

$$\varphi_k-f^*\le\frac n{n+k}\Big[\tfrac12R_1^2(x_0)+f(x_0)-f^*\Big],$$

and, if $f$ is strongly convex in $\|\cdot\|_1$ with constant $\sigma>0$,

$$\varphi_k-f^*\le\Big(1-\frac{2\sigma}{n(1+\sigma)}\Big)^k\Big(\tfrac12R_1^2(x_0)+f(x_0)-f^*\Big).\qquad(4.6)$$

Milestones

1. (4.3): the optimality condition $\langle f'_i(x)+L_iB_i(u^{(i)}(x)-x^{(i)}),u-u^{(i)}(x)\rangle\ge0$ for all $u\in Q_i$.
2. (4.4): for feasible $x$, $f(x)-f(V_i(x))\ge\frac{L_i}2\|u^{(i)}(x)-x^{(i)}\|_{(i)}^2$.
3. (4.7): with $r_k=\|x_k-x_*\|_1$, $\ \mathbb E_{i_k}\big(\frac12r_{k+1}^2+f(x_{k+1})-f^*\big)\le\frac12r_k^2+f(x_k)-f^*+\frac1n\langle\nabla f(x_k),x_*-x_k\rangle$.
4. Footnote 2: under (2.2), the strong convexity constant satisfies $\sigma\le1$.

Significance

The result. Theorem 5 shows that the cost of a constrained problem with separable constraints is, up to the projection onto each $Q_i$, the cost of the unconstrained one: $O(n/\epsilon)$ block steps for accuracy $\epsilon$, and $O\big(\frac n\sigma\log\frac1\epsilon\big)$ under strong convexity. The method needs no knowledge of $\sigma$; the same iteration attains whichever rate applies. The Lyapunov function $\frac12\|x-x_*\|_1^2+f(x)-f^*$ of (4.7) needs no level-set argument, so it applies wherever the projected step is cheap.

Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any rate for a randomized constrained coordinate method, appears in the Prove2Me catalogue or in Mathlib. The Prove2Me catalogue holds Bubeck's scalar, unconstrained random coordinate descent results (ConvexOptAlg.CoordDescent.*) and the deterministic Tseng–Yun coordinate gradient descent; neither covers a projected block step. A formalization produces the first verified rate for a randomized method with constraints, and a reusable model of block-structured spaces, block projections and expectations over random index sequences.

Difficulty

The unconstrained analysis of the paper (Theorem 1) bounds the distance to the optimum by a level-set radius and uses the decrease $f(x)-f(T_i(x))\ge(\|f'_i(x)\|^*_{(i)})^2/(2L_i)$ of a gradient step. Neither carries over: with constraints the gradient at the optimum need not vanish, so the decrease of a projected step is not controlled by the gradient norm, and the unconstrained recursion $\varphi_k-\varphi_{k+1}\ge(\varphi_k-f^*)^2/C$ is not available. A different potential is needed, and its one-step estimate (4.7) is the central milestone. For the linear rate, the contraction factor must be shown nonnegative without assuming $\sigma\le1$, which is where footnote 2 enters.

Formalization scope

$\mathbb R^N$ is the dependent product Blocks E $=\prod_{i:\mathrm{Fin}\,n}E_i$, each $E_i$ a finite-dimensional real inner product space whose inner product is the paper's $\langle B_i\cdot,\cdot\rangle$. Indices are 0-based. The dual norm is the operator norm of linear functionals, and $f'_i(x)$ is the Fréchet derivative of $f$ composed with the block inclusion. Random draws are explicit index sequences, so $\varphi_k$ is the finite average of $f(x_k)$ over all $n^k$ sequences of draws; no measure theory is involved.

Explicit choices where the paper is silent:

• $n\ge1$, every block nontrivial ($n_i\ge1$), and $L_i>0$ are hypotheses.
• Every $Q_i$ is nonempty, and $x_0\in Q$. The paper leaves both implicit; without $x_0\in Q$ the iterates are infeasible and $\varphi_k-f^*$ can be negative.
• $u^{(i)}(x)$ is a choice among the minimizers of the block subproblem. Under the hypotheses the minimizer exists and is unique, so the choice is the paper's update.
• $R_1(x_0)$ is never computed: the theorem takes any $R$ with $\|x-x_*\|_1\le R$ for every feasible $x$ with $f(x)\le f(x_0)$ and every optimal solution $x_*$. This is equivalent to the paper's bound when $R_1(x_0)$ is finite and avoids the default value of a supremum. The level set is taken inside $Q$, the reading of the p. 7 definition for problem (4.1).
• $f^*$ is the constrained optimum $f(x_*)$ for an optimal solution $x_*\in Q$, not an unconstrained minimum.
• Strong convexity is (3.1) on all of $\mathbb R^N$ in $\|\cdot\|_1$. The linear rate does not assume $\sigma\le1$; footnote 2 derives it.
• Printed typos are corrected in the Lean: $U_i^T$ in (4.2) is $U_i$; $u^i$ in (4.3) is $u^{(i)}$.

A formalization in which the update is an arbitrary point of $Q_i$ or an unprojected gradient step, the draws are not uniform, or $f^*$ is the unconstrained minimum, proves a different theorem and is ruled out by the definitions above.

Needed infrastructure: existence and the variational characterization of the minimizer of a strongly convex quadratic over a closed convex set (Mathlib has projections onto closed convex sets in Hilbert spaces), the block descent inequality (2.3) obtained from (2.2), and manipulation of the finite expectations over index sequences (conditioning on the last draw). The block model, the weighted norm and the expectation are shared with the other missions of this series. Proofs of the milestones, and of (2.3) as a supporting lemma, are welcome.

Selected references

• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, CORE Discussion Paper 2010/2, Université catholique de Louvain, 2010. https://core.ac.uk/download/6430808.pdf
• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2) (2012), 341–362. https://doi.org/10.1137/100802001
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (Section 2.1, cited in the proof). https://doi.org/10.1007/978-1-4419-8853-9
• P. Tseng and S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Mathematical Programming 117 (2009), 387–423. https://doi.org/10.1007/s10107-007-0170-0

Motivation

City logistics often moves goods in two stages: large trucks bring freight from a central depot to a few intermediate satellites, and small vehicles distribute it from the satellites to the customers. The two-echelon capacitated vehicle routing problem (2E-CVRP) is the basic optimization model of such systems; it contains the capacitated location-routing problem as a special case. Baldacci, Mingozzi, Roberti and Wolfler Calvo (Oper. Res. 61(2), 2013) gave an exact method that solved benchmark instances out of reach for earlier algorithms.

Their method does not attack the whole problem at once. It enumerates configurations, sets of first-level (depot–satellite) routes, discards most of them with cheap tests, and solves a second-level problem only for the survivors. The correctness of the method rests on two facts stated in §5 of the paper: the problem decomposes exactly over configurations (Eq. (26)), and the pruning tests of Propositions 1 and 2 never discard the configuration of a solution better than the incumbent. This mission formalizes those facts.

Setting

An instance has a depot $0$, satellites $N_S$ and customers $N_C$, a symmetric cost $d$ on the edges (with the fixed vehicle costs folded in), positive integer demands $q_i$ with total $q_{\mathrm{tot}}$, $m^1$ first-level vehicles of capacity $Q_1$, $m_k$ second-level vehicles of capacity $Q_2<Q_1$ at satellite $k$ with a global limit $m^2$, satellite capacities $B_k$ and handling costs $H_k$.

A first-level route $r\in\mathcal M$ leaves the depot, visits a set $R_r$ of satellites and returns; its cost $g_r$ is the length of the closed walk. A second-level route $l\in\mathcal R_k$ leaves satellite $k$, visits a set $R_{kl}$ of customers of total demand $w_{kl}\le Q_2$ and returns; its cost $c_{kl}$ is the walk length plus $H_k w_{kl}$. Formulation $F$ chooses binary $x_{kl}$, $y_r$ and integer deliveries $q_{kr}\ge0$ minimizing $\sum c_{kl}x_{kl}+\sum g_r y_r$ subject to: each customer on exactly one used second-level route; at most $m_k$ used routes at $k$ and $m^2$ in total; load at $k$ at most $B_k$; at most $m^1$ first-level routes; the deliveries to $k$ equal the load leaving $k$; each used first-level route carries at most $Q_1$. Its optimal value is $z(F)$, $+\infty$ when infeasible.

The set of configurations is

$$\mathcal P=\{M\subseteq\mathcal M:\ |M|Q_1\ge q_{\mathrm{tot}},\ |M|\le m^1\}.$$

For $M\subseteq\mathcal M$, $N_S(M)=\bigcup_{r\in M}R_r$, $M_k=\{r\in M:k\in R_r\}$ and $U(M)=\sum_{r\in M}g_r$. Problem $F(M)$ is $F$ with the first-level routes fixed to $M$: second-level routes only at satellites of $N_S(M)$, real deliveries $q_{kr}\ge0$ for $r\in M$, and $\sum_{k\in R_r}q_{kr}\le Q_1$. Its value $z(F(M))$ is $+\infty$ when infeasible.

The bounds of §5.1 use multipliers $\lambda_i$, $\mu_k\le0$, $\mu_0\le0$ and marginal costs $\beta_{ik}$ satisfying the penalty system (12), $\sum_i a_{ikl}\beta_{ik}\le c_{kl}-\sum_i a_{ikl}\lambda_i-\mu_k-\mu_0$ for every route $l$ of satellite $k$:

$$\mathrm{LB}_R=\sum_{i}\min_{k\in N_S}\beta_{ik}+\sum_i\lambda_i+\sum_{k\in N_S}m_k\mu_k+m^2\mu_0,$$ $$\mathrm{LBW}(M)=\sum_{i}\min_{k\in N_S(M)}\beta_{ik}+\sum_i\lambda_i+\sum_{k\in N_S(M)}m_k\mu_k+m^2\mu_0.$$

Formalization targets

Goal: Proposition 1, necessity of conditions (b)–(e)

Let $z(\mathrm{UB})$ be a real number and $(x,y,q)$ a feasible solution of $F$ of cost less than $z(\mathrm{UB})$, with configuration $M=\{r:y_r=1\}$. Then $M\in\mathcal P$ and

$$\sum_{r\in M}\min\Bigl\{Q_1,\sum_{k\in R_r}m_kQ_2\Bigr\}\ge q_{\mathrm{tot}},\qquad \sum_{r\in M}\sum_{k\in R_r}m_k\ge\Bigl\lceil\frac{q_{\mathrm{tot}}}{Q_2}\Bigr\rceil,$$ $$U(M)<z(\mathrm{UB})-\mathrm{LB}_R,\qquad U(M)<z(\mathrm{UB})-\mathrm{LBW}(M).$$

Milestones

1. Eq. (26): $z(F)=\min_{M\in\mathcal P}\{U(M)+z(F(M))\}$.
2. §5.1: $\mathrm{LB}_R$ is at most the second-level routing cost of every feasible solution of $F$.
3. §5.1: $\mathrm{LBW}(M)\le z(F(M))$.
4. Proposition 2: if $\theta(k)$ bounds from below the supply to satellite $k$ in every feasible solution of $F(M)$, and $\sum_{k\in N_S(M)}\lceil\theta(k)/Q_2\rceil>m^2$ or $\lceil\theta(k)/Q_2\rceil>m_k$ for some $k\in N_S(M)$, then $F(M)$ is infeasible.
5. §5.2.2, Eq. (33): the capacity constraints $\sum_{k\in N_S(M)}\sum_{l:R_{kl}\cap H\neq\emptyset}x_{kl}\ge\lceil\sum_{i\in H}q_i/Q_2\rceil$, $|H|\ge2$, hold for every feasible solution of $F(M)$.

Significance

Eq. (26) is what makes the method exact: once every configuration that can carry a solution better than the incumbent is examined, the best $U(M)+z(F(M))$ is the optimum. Propositions 1 and 2 are what make it fast: they remove configurations from $\mathcal P$ before any second-level problem is solved. If a pruning test discarded the configuration of a cheaper solution, the method would return a suboptimal value and still report it as optimal; the formal statements rule this out for every instance, not just the benchmark ones. The capacity constraints (33) play the same role inside $F(M)$: a cut that removed a feasible solution would make the bound $z(\bar F(M))$ invalid.

The paper's proofs are in an electronic companion; none of these statements has been machine-checked before, and none is on the platform. The formalization also records exactly what the tests need: positive demands, integral vehicle counts, and the sign conditions on the multipliers, and nothing about the optimality of the incumbent.

Difficulty

Most statements are elementary counting and Lagrangean weak-duality arguments over finite index sets. The work lies in the bookkeeping between two formulations with different index sets: $F$ sums over all satellites, $F(M)$ only over $N_S(M)$, and a solution of one must be turned into a solution of the other. One step is not elementary: $F$ has integer deliveries and $F(M)$ real ones, so the inequality $z(F)\le U(M)+z(F(M))$ in (26) needs an integral delivery plan from a fractional one. That is an integrality property of a bipartite transportation problem (routes to satellites, integral capacities and demands), which no counting argument gives.

Formalization scope

Satellites and customers are Fin ns and Fin nc, 0-based. The route families $\mathcal M$ and $\mathcal R$ are arbitrary finite families of elementary routes with costs computed along the closed walk; the paper uses all such routes, so every statement here is a generalization. Demands are positive integers; the triangle inequality is not assumed. Binary variables are Bool; optimal values are infima in EReal, with ⊤ for an infeasible problem. A configuration is a Finset of route indices. The penalties are any $\lambda$, $\mu\le0$, $\mu_0\le0$ and $\beta$ satisfying (12), not only those producing the paper's bound LD1. Ceilings of $q_{\mathrm{tot}}/Q_2$ and $\sum_{i\in H}q_i/Q_2$ are natural-number ceilings of rationals; those in Proposition 2 are integer ceilings of reals.

The goal departs from the printed proposition in three disclosed ways. Only necessity is stated: the "if" direction is false, because (b)–(e) ignore the satellite capacities $B_k$. Condition (a), $|R_r\cap R_{r'}|\le1$, is omitted: it holds for some optimal solution, not every one (its split-delivery analogue is posed, and open, on the platform as SplitDeliveryVRPTW.Known.exists_optimal_split_customers; it is not reused here). "An optimal solution" becomes "a feasible solution of cost below $z(\mathrm{UB})$", the property the paper's own justification uses. Proposition 2 is stated with $\theta$ as a hypothesis; the paper's computation of $\theta$ by problem (27)–(32) is not formalized, because (32) forces positive deliveries that $F(M)$ does not require. The goal is not trivialized by an infeasible hypothesis: feasible solutions of $F$ exist on small instances, and a toy instance was checked in Lean.

A complete development needs finite-sum manipulations, Lagrangean weak duality for (12), and, for (26), integrality of bipartite transportation polytopes, which is reusable well beyond this mission. Proofs of any milestone, and a general transportation-integrality lemma, are welcome.

Selected references

• R. Baldacci, A. Mingozzi, R. Roberti, R. Wolfler Calvo, An Exact Algorithm for the Two-Echelon Capacitated Vehicle Routing Problem, Operations Research 61(2), 298–314, 2013. https://doi.org/10.1287/opre.1120.1153
• R. Baldacci, A. Mingozzi, A unified exact method for solving different classes of vehicle routing problems, Mathematical Programming 120(2), 347–380, 2009. https://doi.org/10.1007/s10107-008-0218-9
• G. Perboli, R. Tadei, D. Vigo, The two-echelon capacitated vehicle routing problem: models and math-based heuristics, Transportation Science 45(3), 364–380, 2011. https://doi.org/10.1287/trsc.1110.0368

Motivation

Randomized coordinate descent updates one block of variables per iteration, chosen at random. For problems whose dimension makes even one full gradient expensive (the "huge-scale" problems of the title, such as sparse least squares or truss topology design), a coordinate step can cost a tiny fraction of a gradient step. Nesterov's paper (CORE Discussion Paper 2010/2; journal version SIAM J. Optim. 22 (2012) 341–362) gave the first global complexity bounds for such methods with non-uniform sampling, and it is the reference point for the later literature on randomized block methods (Richtárik and Takáč 2014, Lu and Xiao 2015, Allen-Zhu et al. 2016).

The first results of the paper (Theorem 1, the subject of a companion mission) bound the expected objective value after k iterations. An expected bound does not say what happens in a single run. This mission formalizes the paper's answer to that question in §3: by running the method on a slightly regularized objective, one run returns an ε-solution with any prescribed probability β, after a number of iterations that grows only logarithmically in 1/(1 − β).

Setting

The variable space is a product $\mathbb R^N=\mathbb R^{n_1}\times\cdots\times\mathbb R^{n_n}$ of $n\ge1$ blocks; a point $x$ has blocks $x^{(i)}$, and $U_ih$ is the point whose $i$-th block is $h$ and whose other blocks vanish. In this mission each block carries a Euclidean norm $\|h^{(i)}\|_{(i)}^2=\langle B_ih^{(i)},h^{(i)}\rangle$ with $B_i\succ0$ (3.4), and the whole space carries

$$\|h\|_0^2=\sum_{i=1}^n\|h^{(i)}\|_{(i)}^2,\qquad \|g\|_0^*=\Big[\sum_{i=1}^n\big(\|g^{(i)}\|_{(i)}^*\big)^2\Big]^{1/2}.$$

The objective $f:\mathbb R^N\to\mathbb R$ is convex and differentiable, has a minimizer $x_*$ with value $f^*$, and its partial gradients $f'_i(x)=U_i^T\nabla f(x)$ are Lipschitz along their own block with constants $L_i>0$ (2.2): $\|f'_i(x+U_ih)-f'_i(x)\|^*_{(i)}\le L_i\|h\|_{(i)}$. Write $S_\alpha=\sum_iL_i^\alpha$.

The method RCDM$(\alpha,x_0)$ (2.6) draws, independently at each step, block $i$ with probability $L_i^\alpha/S_\alpha$ and replaces $x$ by $T_i(x)=x-\frac1{L_i}U_if'_i(x)^\#$, where $s^\#$ is a maximizer of $\langle s,x\rangle-\frac12\|x\|^2$ (1.8). The quantity $\phi_k$ is the expectation of $f(x_k)$ over the first $k$ draws.

The level-set radius is $R_0(x_0)=\max_x\{\max_{x_*}\|x-x_*\|_0: f(x)\le f(x_0)\}$, and for $\mu>0$ the regularized objective is

$$f_\mu(x)=f(x)+\frac\mu2\|x-x_0\|_0^2 .$$

It has block constants $L_i+\mu$, so RCDM$(1,x_0)$ applied to $f_\mu$ samples block $i$ with probability $(L_i+\mu)/(S_1+n\mu)$ and steps with $1/(L_i+\mu)$.

Formalization targets

Goal: Theorem 4 (p. 11)

For $\epsilon>0$, $\beta\in(0,1)$, $\mu=\epsilon/(4R_0^2(x_0))$ and

$$k\ \ge\ 2\Big[n+\frac{4S_1R_0^2(x_0)}{\epsilon}\Big]\Big(\ln\frac1{1-\beta}+\ln\Big(\frac12+\frac{2S_1R_0^2(x_0)}{\epsilon}\Big)\Big),$$

the point $x_k$ produced by RCDM$(1,x_0)$ on $f_\mu$ satisfies

$$\mathrm{Prob}\big(f(x_k)-f^*\le\epsilon\big)\ge\beta .$$

Milestones

1. Theorem 2 (p. 9), for arbitrary block norms: if $f$ is $\sigma$-strongly convex in $\|\cdot\|_{1-\alpha}$, then $\phi_k-f^*\le(1-\sigma/S_\alpha)^k(f(x_0)-f^*)$.
2. The constants of $f_\mu$ (p. 11): $f_\mu$ is $\mu$-strongly convex in $\|\cdot\|_0$, has block constants $L_i+\mu$, so that $S_1(f_\mu)=S_1(f)+n\mu$, and its gradient is $(S_1(f)+\mu)$-Lipschitz in $\|\cdot\|_0$.
3. Lemma 4 (p. 11): $\mathbb E\,\|\nabla f_\mu(x_k)\|_0^*\le\big[2(S_1+\mu)(f(x_0)-f^*)(1-\mu/(S_1+n\mu))^k\big]^{1/2}$.

Significance

Theorem 4 turns an in-expectation guarantee into a single-run guarantee with an explicit, non-asymptotic iteration count. Its dependence on the confidence level is logarithmic, so very high confidence costs little; and the count $O\big((n+S_1R_0^2/\epsilon)\log(1/\epsilon)\big)$ replaces the largest eigenvalue of the Hessian, which governs the full gradient method, by the trace-type quantity $S_1$, which for sparse problems makes groups of $n$ coordinate steps competitive with one gradient step. Theorem 2 is the linear-rate result for strongly convex objectives that later analyses of randomized block methods take as their starting point.

The results are proved in the paper. None of them is formalized in the block setting. The scalar Euclidean case $n_i=1$ of Theorem 2 is proved on Prove2Me as ConvexOptAlg.CoordDescent.theorem_6_8 (Bubeck, Theorem 6.8), and the bound (3.2), $f(x)-f^*\le\frac1{2\sigma}(\|\nabla f(x)\|^*)^2$ for a $\sigma$-strongly convex $f$ in any norm, is proved as ConvexOptAlg.CoordDescent.lemma_6_9. This mission adds block variables with general norms (Theorem 2), the regularization constants, the gradient-norm bound, and the high-probability statement itself, which has no formalized counterpart.

Difficulty

The obvious argument fails. Theorem 2 controls the expected suboptimality of $f_\mu$, not of $f$, and Markov's inequality applied to $f_\mu(x_k)-f_\mu^*$ does not reach accuracy ε: $f_\mu^*$ and $f^*$ differ by an amount comparable to ε, and the contraction factor itself depends on μ. Relating the run on $f_\mu$ to the original problem requires the global Lipschitz constant of $\nabla f_\mu$ in $\|\cdot\|_0$, which for $f$ is the weighted co-coercivity statement of Lemma 2 of the paper and is not a consequence of (2.2) alone without convexity. The constants of (3.11) are exact, including the factor 2 and the ½, so no estimate may lose a constant. Finally, the iterates depend on all previous draws, so even the finite-sum expectations need a careful account of linearity and of conditioning on the last draw.

Formalization scope

• $\mathbb R^N$ is the dependent product Blocks E of finite-dimensional real spaces E i indexed by Fin n (0-based for the paper's 1, …, n). Euclidean blocks (3.4) are inner-product spaces, with $B_i$ absorbed into the inner product; Theorem 2 is stated for arbitrary normed blocks. The dual norm of a block is the operator norm of a functional.
• The draws are explicit sequences Fin k → Fin n; expectations and probabilities are finite sums weighted by $\prod_sp(i_s)$. No measure theory is involved.
• The vectors $s^\#$ are an arbitrary selection satisfying (1.8); the theorems hold for every selection.
• $R_0(x_0)$ is replaced by any positive upper bound $R$ (every point of the level set within $R$ of every minimizer), and $\mu=\epsilon/(4R^2)$ is defined from it. The paper's theorem is the case $R=R_0(x_0)$; $R>0$ excludes the case $R_0(x_0)=0$, in which the paper's μ is undefined.
• Explicit hypotheses the paper leaves implicit: $n\ge1$, $L_i>0$, $f$ convex and differentiable, existence of a minimizer, and $\epsilon>0$, $\beta\in(0,1)$ (fixed on p. 10).
• The paper prints Theorem 2's left side as $\phi_k-\phi^*$; the statement uses $\phi_k-f^*$, which is what its proof establishes.
• The run in Theorem 4 and Lemma 4 is on $f_\mu$ with $f_\mu$'s constants $L_i+\mu$ (step and sampling); the event of Theorem 4 is about $f$ and $f^*$ of the original problem. Running RCDM with $f$'s constants $L_i$, or stating the event for $f_\mu$, would be a different theorem.
• Lemma 3 and Theorem 3 (the variant in the norm $\|\cdot\|_1$) are not posed: applied to $f_\mu$ with constants $(1+\mu)L_i$, Theorem 2 gives a contraction factor weaker than the printed $1-\mu/n$, and the paper's argument does not establish them as printed.

Contributions are welcome on the probabilistic bookkeeping for expect (normalization, linearity, conditioning on the last draw, Jensen for a concave function), which is reusable by every mission of this series; on Lemma 2 of the paper in the block setting; and on the milestones in the stated order.

Selected references

• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, CORE Discussion Paper 2010/2, Université catholique de Louvain, 2010. https://core.ac.uk/download/6430808.pdf
• Yu. Nesterov, Efficiency of coordinate descent methods on huge-scale optimization problems, SIAM Journal on Optimization 22(2), 341–362, 2012. https://doi.org/10.1137/100802001
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 231–357, 2015, §6.4. https://arxiv.org/abs/1405.4980
• P. Richtárik and M. Takáč, Iteration complexity of randomized block-coordinate descent methods for minimizing a composite function, Mathematical Programming 144, 1–38, 2014. https://doi.org/10.1007/s10107-012-0614-z
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

A retailer that orders stock months before the selling season carries inventory risk: its profit depends on a demand it cannot observe when it commits. For many goods that demand moves with a quantity traded on financial markets: sales of housing-related products with an interest-rate or construction index, sales of fashion or luxury goods with a stock index, sales of commodity-intensive products with a commodity price. V. Gaur and S. Seshadri, Hedging Inventory Risk Through Market Instruments (MSOM 7(2), 2005), ask what such a firm gains by trading in that market, and how the trade interacts with the ordering decision.

Their analysis has two halves. When demand is perfectly correlated with the asset price, the newsvendor payoff can be replicated by a portfolio of the asset and call options, and inventory risk can be removed completely (§2). When demand is only partially correlated, the hedge is imperfect, and the question becomes whether a decision maker with a concave utility still benefits from hedging, and whether hedging changes the order quantity (§3.2). This mission formalizes the first of these two questions in the partially correlated model: Proposition 5, which says that a small fair hedge never lowers expected utility at the margin. A companion mission of the same series treats Proposition 7, on the order quantity.

Setting

A firm orders $I$ units now at unit cost $c$, sells at price $p$ at a future time $T$, and salvages leftovers at $s$. The demand is

$$D = a + bS_T + \varepsilon',$$

where $S_T$ is the time-$T$ price of a traded asset and $\varepsilon'$ is a forecast error, independent of $S_T$, with $\mathbb E[\varepsilon'] = 0$ and $\mathbb E[\varepsilon'^2] < \infty$ (§3, p. 107). Write $\varepsilon = \varepsilon'/b$. The paper's standing assumptions (§2, p. 106) are $b > 0$, $I > \max\{a, 0\}$, and $p > ce^{rT} > s$, where $r$ is the risk-free rate.

After scaling all cash flows by $1/((p-s)b)$ (p. 110) the firm's terminal wealth without hedging is

$$W + \Pi_U(I) = W + \min\{S_T + \varepsilon,\ (I-a)/b\} - c_1 I,$$

with $c_1 = (ce^{rT}-s)/((p-s)b)$ and $W$ the scaled initial wealth plus $(p-s)a$. In these units $p > ce^{rT} > s$ reads $0 < c_1$ and $c_1 b < 1$.

A hedge is a portfolio with time-$T$ payoff $X_T$ and time-0 price $X_0$. The paper requires it to be a fair gamble, $\mathbb E[X_T - X_0e^{rT}] = 0$ (12), and $X_T$ to be an increasing function of $S_T$ (p. 111). If the firm shorts $\alpha$ units of the hedge, its wealth is

$$W + \Pi_H(I,\alpha) = W + \min\{S_T + \varepsilon, (I-a)/b\} - c_1 I - \alpha X_T + \alpha X_0 e^{rT}, \tag{14}$$

and a decision maker with utility $u:\mathbb R \to \mathbb R$ evaluates it by $\mathbb E[u(\Pi_H(I,\alpha))]$.

In Lean, the law of $S_T$ is a probability measure ν on ℝ, the law of $\varepsilon$ is a probability measure G on ℝ, the hedge is X_T = φ S_T for a function φ : ℝ → ℝ, the forward price $X_0e^{rT}$ is one real x0r, and every expectation is an integral against the product measure ν.prod G. The definitions file provides unhedgedPayoff, hedgedPayoff and expUtil.

Formalization targets

Goal: Proposition 5 (p. 111)

For any concave and differentiable utility function $u$, and any fixed order quantity $I$,

$$\frac{d}{d\alpha}\,\mathbb E[u(\Pi_H(I,\alpha))]\Big|_{\alpha = 0} \ \ge\ 0. \tag{15}$$

The Lean statement asserts that the two-sided derivative exists at $\alpha = 0$ and is nonnegative.

Milestones (proof of Proposition 5, p. 118)

1. Derivative at $\alpha = 0$. The derivative exists and equals

$$\mathbb E\big[u'(W + \min\{S_T + \varepsilon, (I-a)/b\} - c_1I)\,\{-X_T + X_0e^{rT}\}\big].$$

2. Covariance inequality. Since both factors decrease in $S_T$,

$$\mathbb E\big[u'(W+\Pi_U)\{-X_T + X_0e^{rT}\}\big] \ \ge\ \mathbb E[u'(W+\Pi_U)]\cdot\mathbb E[-X_T + X_0e^{rT}] = 0.$$

Significance

Proposition 5 is the paper's answer to "should a risk-averse newsvendor hedge at all?": with any concave utility and any order quantity, a small short position in a fair hedge that rises with the asset price weakly increases expected utility. It needs no assumption on the shape of the utility beyond concavity, no sign of $u'$, and no assumption on the law of the forecast error beyond independence. It is the starting point for the paper's later results on the optimal hedge (Proposition 4) and on how hedging raises the optimal order (Propositions 6 and 7), and it is a clean instance of a general principle in operations-finance: a fair bet that is negatively correlated with marginal utility is worth taking at the margin.

The result is proved in the paper in a few lines. What this mission adds is a machine-checked version with every regularity condition explicit: the paper differentiates under the expectation and multiplies expectations without stating when this is legitimate, and conditions on $S_T$ informally. To the best of a search of the Prove2Me catalog, neither the result nor the two steps of its proof (an integral version of Chebyshev's covariance inequality for monotone functions, and differentiation of a concave expected utility under the integral sign) is formalized there.

Difficulty

The obvious argument has two analytic gaps. First, exchanging $d/d\alpha$ with the expectation needs a dominating function, and the only integrability available is at finitely many values of $\alpha$, for both signs of $\alpha$. Second, "$u'(\cdot)$ is a decreasing function of $S_T$" is false as a statement about the pair $(S_T, \varepsilon)$: $u'(W + \Pi_U)$ depends on $\varepsilon$ too. The covariance step is Chebyshev's inequality for the function $s \mapsto \mathbb E_\varepsilon[u'(W + \min\{s+\varepsilon, (I-a)/b\} - c_1 I)]$ and the function $s \mapsto X_0e^{rT} - X_T(s)$, which needs independence (Fubini on the product measure) and has to cope with the conditional expectation being finite only almost everywhere. Neither $u'$ nor the hedge payoff is bounded.

Formalization scope

The Lean development commits to the following conventions.

• Random inputs are two probability measures ν (law of $S_T$) and G (law of $\varepsilon$) on ℝ; independence is the product measure ν.prod G. The standing assumptions $\mathbb E[\varepsilon] = 0$ and $\mathbb E[\varepsilon^2] < \infty$ are hypotheses (∫ e, e ∂G = 0, MemLp id 2 G).
• The scaled parameters $W, a, b, c_1, I$ are reals with $b > 0$, $\max\{a,0\} < I$, $0 < c_1$, $c_1 b < 1$.
• The hedge is φ : ℝ → ℝ, monotone (nondecreasing, reading the paper's "increasing" weakly), measurable and ν-integrable; the fair-gamble condition (12) is ∫ s, φ s ∂ν = x0r. The paper's further remark that $X_T$ is piecewise continuous and a.e. differentiable is not needed and not imposed.
• The utility is u : ℝ → ℝ with ConcaveOn ℝ Set.univ u and Differentiable ℝ u, exactly "concave and differentiable"; no monotonicity of $u$ is assumed.
• Regularity hypotheses, disclosed: for some $\delta > 0$ the utility $u(W + \Pi_H(I,\alpha))$ is integrable at $\alpha \in \{-\delta, 0, \delta\}$, and $u'(W + \Pi_U)$ is integrable. The paper uses these silently.

A statement of the form 0 ≤ deriv (fun α => expUtil …) 0 would be trivially true whenever the derivative fails to exist (Lean's deriv returns 0 there); the goal instead asserts HasDerivAt with a value D and 0 ≤ D. The hypotheses are satisfiable with a non-constant hedge: a sorry-free check uses $u(w) = -e^{-w}$, $S_T$ uniform on $\{0,1\}$, $\varepsilon$ uniform on $\{-1,1\}$ and $X_T = S_T$.

Infrastructure that a complete proof needs, reusable beyond this mission: Chebyshev's integral (covariance) inequality for two monotone functions of a real random variable; differentiation under the integral sign for concave integrands with integrability at three points; Fubini-based conditioning on one coordinate of a product measure. Contributions of these general lemmas as separate theorems are welcome. The source PDF is a scan of the published article.

Selected references

• V. Gaur, S. Seshadri, Hedging Inventory Risk Through Market Instruments, Manufacturing & Service Operations Management 7(2):103–120, 2005. https://doi.org/10.1287/msom.1040.0061
• K. J. Arrow, Essays in the Theory of Risk-Bearing, Markham, 1971 (absolute risk aversion, cited on p. 111 of the paper).
• M. S. Kimball, Precautionary Saving in the Small and in the Large, Econometrica 58(1):53–73, 1990. https://doi.org/10.2307/2938334

Motivation

In a time-inconsistent control problem, a control that is optimal when planned at time $t$ stops being optimal when the problem is re-solved at a later time. Two sources of time inconsistency are common in finance and economics. One is a variance term in the objective, as in continuous-time Markowitz mean–variance portfolio selection (Zhou–Li 2000; Basak–Chabakauri 2010). The other is a state-dependent target, as in Björk–Murgoci–Zhou 2014. Dynamic programming does not apply. A standard response is to look for an equilibrium: a control that no planner at any time $t$ can improve by an infinitesimal deviation on $[t,t+\varepsilon)$.

Hu, Jin and Zhou define open-loop equilibria for a general stochastic linear–quadratic (LQ) problem with both sources of time inconsistency. They give a sufficient condition through a flow of forward–backward SDEs, which is the subject of mission I of this series. This mission covers §4 of the paper: the scalar-state case with deterministic coefficients, where the equilibrium is computed explicitly from a system of coupled Riccati equations. Mission III covers §5, the mean–variance application with random coefficients.

Setting

On a probability space carrying a standard $d$-dimensional Brownian motion $W$ with its filtration $(\mathcal F_t)$, the state $X$ is scalar ($n=1$) and the control $u$ takes values in $\mathbb R^l$:

$$dX_s=[A_sX_s+B_s'u_s+b_s]\,ds+[C_sX_s+D_su_s+\sigma_s]'\,dW_s,\qquad X_0=x_0.$$

The coefficients are deterministic functions on $[0,T]$: $A_s,b_s,Q_s\in\mathbb R$, $B_s\in\mathbb R^l$, $C_s,\sigma_s\in\mathbb R^d$, $D_s\in\mathbb R^{d\times l}$ and $R_s\in\mathbb R^{l\times l}$ symmetric. $A,B,C,D,Q,R$ are bounded, $b,\sigma$ are square integrable, $Q\ge0$, $R\succeq0$, and $G\ge0$. At time $t$, in state $x_t$, the planner evaluates

$$J(t,x_t;u)=\tfrac12\mathbb E_t\!\int_t^T\!\big(Q_sX_s^2+\langle R_su_s,u_s\rangle\big)ds+\tfrac12\mathbb E_t[GX_T^2]-\tfrac h2\big(\mathbb E_t[X_T]\big)^2-(\mu_1x_t+\mu_2)\,\mathbb E_t[X_T],$$

where $\mathbb E_t=\mathbb E[\,\cdot\mid\mathcal F_t]$. The third term (the variance-like term) and the fourth term (which depends on $x_t$) make the problem time-inconsistent. A control $u^*$ with state $X^*$ is an equilibrium (Definition 2.1) if, for every $t\in[0,T)$ and every $\mathcal F_t$-measurable square-integrable $v$, the spike $u^{t,\varepsilon,v}=u^*+v\mathbf 1_{[t,t+\varepsilon)}$ satisfies

$$\liminf_{\varepsilon\downarrow0}\frac{J(t,X^*_t;u^{t,\varepsilon,v})-J(t,X^*_t;u^*)}{\varepsilon}\ge0.$$

With $\Gamma^{(1)}_s=\mu_1e^{\int_s^TA_r\,dr}$, $|C|^2=C'C$ and $K=(R+MD'D)^{-1}$, the coupled Riccati system (4.9) for deterministic $(M,N)$ is

$$\begin{aligned}\dot M&=-\big[2A+|C|^2+\Gamma^{(1)}B'K(B+D'C)\big]M-Q+(B+D'C)'K(B+D'C)M^2-B'K(B+D'C)MN,& M_T&=G,\\ \dot N&=-\big[2A+\Gamma^{(1)}B'KB\big]N+B'K(B+D'C)MN-B'KBN^2,& N_T&=h.\end{aligned}$$

Given $(M,N)$, a linear ODE (4.8) determines $\Phi$ with $\Phi_T=-\mu_2$. The candidate equilibrium is the linear feedback (4.4)

$$u^*_s=\alpha_sX^*_s+\beta_s,\quad\alpha_s=-K_s\big[(M_s-N_s-\Gamma^{(1)}_s)B_s+M_sD_s'C_s\big],\quad\beta_s=-K_s(\Phi_sB_s+M_sD_s'\sigma_s).$$

Formalization targets

Goal: Theorem 4.4

Suppose $G\ge h>0$ and one of three cases holds:

• (i) $R\succeq\delta I$, $\frac{QD'D+|C|^2R}{l}+\Gamma^{(1)}\mathcal S(D'CB')\succeq0$ and $B=\lambda D'C$ with $\lambda\ge0$;
• (ii) the first two conditions of (i) and $D'D\succeq\delta I$;
• (iii) $R\equiv0$, $D'D\succeq\delta I$, $Q+\Gamma^{(1)}B'(D'D)^{-1}(B+D'C)\ge0$ and $Q+\Gamma^{(1)}B'(D'D)^{-1}D'C\ge0$.

Then

$$\text{(4.9) has a unique positive solution pair }(M,N)\text{ on }[0,T],$$

and, for every solution $\Phi$ of (4.8), the closed-loop equation of (4.4) has a solution, and the feedback control along every closed-loop state is an equilibrium.

Milestones

• Proposition 4.1: a positive solution $(M,J)$ of the transformed system (4.10) gives the positive solution $(M,M/J)$ of (4.9).
• Theorem 4.2: existence and uniqueness of positive solutions of (4.10) and (4.9) in the standard case $R\succeq\delta I$.
• Theorem 4.3: existence for (4.13) and (4.9) in the singular case $R\equiv0$.
• Three steps from the proof of Theorem 4.4:
  • $\alpha$ is bounded, so $u^*$ is admissible and $X^*$ has continuous paths with $\mathbb E\sup_s|X^*_s|^2<\infty$;
  • the ansatz $p(s;t)=M_sX^*_s-N_s\mathbb E_t[X^*_s]-\Gamma^{(1)}_sX^*_t+\Phi_s$, $k(s;t)=M_s[C_sX^*_s+D_su^*_s+\sigma_s]$ solves the adjoint flow (3.10);
  • the identity $\Lambda(s;t)=N_s[X^*_s-\mathbb E_tX^*_s]B_s+\Gamma^{(1)}_s(X^*_s-X^*_t)B_s$ holds, and $\Lambda$ satisfies condition (3.4).

Significance

The theorem gives an equilibrium in closed form, as a linear feedback of the current state with deterministic gains. That makes the equilibrium computable and comparable with the classical, time-consistent LQ regulator. Setting $h=\mu_1=0$ recovers a standard LQ problem, but (4.9) differs from the classical Riccati equation even then: it is a nonsymmetric coupled system (footnote 2, p. 10), and the cases (i)–(iii) are the conditions under which it is solvable. The mean–variance results of §5 (mission III) follow the same pattern.

The result is proved in the paper; to our knowledge it has not been formalized. A formal proof needs global existence for a nonlinear, nonautonomous ODE system with Carathéodory coefficients, obtained by truncation and a priori bounds. It also needs linear SDEs with bounded feedback, Itô calculus for products of deterministic and Itô processes, and the sufficient condition of mission I. Uniqueness in case (iii) is claimed by Theorem 4.4 but not proved in Theorem 4.3; it is part of the goal.

Difficulty

The system (4.9) is quadratic in $(M,N)$. Its solutions can blow up in finite time, and $(R+MD'D)^{-1}$ can degenerate when $M$ changes sign. Picard–Lindelöf therefore gives only local solutions, and a global solution needs a priori bounds $0<\eta\le M\le L$ and $J\ge1$, with $\eta$ and $L$ independent of the truncation level. Those bounds are where the case hypotheses enter. In the stochastic half, the equilibrium property is not proved by computing $J$ directly. It requires checking that the explicit candidate meets the flow-of-FBSDE sufficient condition, and the flow carries a parameter $t$ and the conditional expectations $\mathbb E_t[X^*_s]$ for every $s\ge t$.

Formalization scope

The general model (data, standing assumptions, states, conditional cost, spike, equilibrium) is stated for arbitrary $n$ and instantiated at $n=1$ through toData. It is built on the published substrate Peng1990_SMP_Stochastic (Brownian motion, natural filtration, $L^2_{\mathcal F}$, Itô integrals, SDE solutions). The formalization commits to the following choices.

• Definition 2.1 uses $\liminf$ in $\overline{\mathbb R}$, along every sequence $\varepsilon_k\downarrow0$, almost surely for each sequence, and for every version of the state and of the perturbed states. The page writes $\lim$, which need not exist.
• The filtration is the natural, uncompleted filtration of $W$, not the augmented one.
• The state from time $t$ is encoded through the full horizon. The spike is additive on $[t,t+\varepsilon)$.
• "Essentially bounded" and "a.s., a.e." are read $d\mathbb P\otimes ds$-a.e.
• Every ODE ((4.8), (4.9), (4.10), (4.13)) is stated in integral form on $[0,T]$, because the coefficients are only bounded measurable. A solution includes invertibility of $R+MD'D$ (resp. $D'D$) on $[0,T]$. Uniqueness means agreement on $[0,T]$.
• The constants $\delta,\lambda$ are uniform in $s$, and the case conditions hold for every $s\in[0,T]$. In $\frac{QD'D+|C|^2R}{l}$, $l$ is the control dimension.
• "Let $\Phi$ be a solution of (4.8)" means every solution. "$u^*$ is an equilibrium" means that a closed-loop state exists and that the feedback is an equilibrium along every closed-loop state.
• Conditional-expectation families $\mathbb E_t[X^*_s]$ are handled through arbitrary progressive versions. Condition (3.4) is stated exactly: its first part as a localization on $\mathcal F_t$-sets, its second part with a jointly measurable version and "a.e. $s$".
• The paper's "$\beta$ uniformly bounded" is false when $\sigma$ is only square integrable. The milestone states the true claim: $\alpha$ is essentially bounded on $[0,T]$ (the coefficients are only essentially bounded) and $\beta$ is square integrable.

The goal's conclusion is Definition 2.1 itself; it does not mention $\Lambda$, $p$ or (3.4). Existence of the closed-loop state is asserted, not assumed. A formalization that assumes existence, or that replaces equilibrium by condition (3.4), is a different and weaker theorem.

Theorem 3.3 (the $n=1$ sufficient condition) is not posed here. Under the shared model it is mission I's goal at $n=1$. Contributions are welcome on the ODE layer (truncation, comparison and Gronwall bounds for Carathéodory systems), on linear SDEs with bounded feedback, and on the Itô product rule. These parts are reusable well beyond this paper.

Selected references

• Y. Hu, H. Jin, X. Y. Zhou, Time-Inconsistent Stochastic Linear–Quadratic Control, arXiv:1111.0818v1, 2011; SIAM J. Control Optim. 50(3), 2012. https://arxiv.org/abs/1111.0818
• T. Björk, A. Murgoci, X. Y. Zhou, Mean–variance portfolio optimization with state-dependent risk aversion, Mathematical Finance 24(1), 2014. https://doi.org/10.1111/j.1467-9965.2011.00515.x
• S. Basak, G. Chabakauri, Dynamic mean–variance asset allocation, Review of Financial Studies 23(8), 2010. https://doi.org/10.1093/rfs/hhq028
• X. Y. Zhou, D. Li, Continuous-time mean–variance portfolio selection: a stochastic LQ framework, Applied Mathematics and Optimization 42, 2000. https://doi.org/10.1007/s002450010003
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054
• J. Yong, X. Y. Zhou, Stochastic Controls: Hamiltonian Systems and HJB Equations, Springer, 1999. https://doi.org/10.1007/978-1-4612-1466-3
• Missions I and III of this series: the sufficient condition (Theorem 3.2) and the mean–variance equilibrium (Theorem 5.4).