All missions

Motivation

Multistage stochastic linear programs model sequential decisions under uncertainty: capacity and reservoir planning, hydro-thermal scheduling, inventory and asset–liability management. When the data process is stagewise independent, the problem decomposes by dynamic programming into one linear program per stage, coupled through expected cost-to-go functions. These functions are convex and piecewise linear, and the stochastic dual dynamic programming (SDDP) method of Pereira and Pinto (1991) approximates them from below by cutting planes. SDDP is the standard solution method in the long-term planning of hydro-dominated power systems, and its convergence theory determines what the bounds it reports actually mean.

Shapiro's paper (Optimization Online 2009/12/2509; European J. Oper. Res. 209(1), 2011, doi:10.1016/j.ejor.2010.08.007) analyses SDDP applied to a sample average approximation (SAA) of the true problem, with all of the data $(c_t, A_t, B_t, b_t)$ random. Its convergence result, Proposition 3.1, asserts finite convergence with probability one when the forward scenarios are subsampled independently. A related almost-sure finite convergence theorem for a different algorithm (DOASA, with randomness only in the right-hand sides and cut sharing across outcomes) is due to Philpott and Guan (2008); it is posed as a separate mission on this platform and is not restated here.

Setting

There are $T\ge 2$ stages. The decision $x_t\in\mathbb R^{n_t}$ satisfies $x_t\ge 0$ and, at the first stage, $A_1x_1=b_1$ with deterministic data $(c_1,A_1,b_1)$. For $t=2,\dots,T$ the data are replaced by a sample $\tilde\xi_t^j=(\tilde c_{tj},\tilde A_{tj},\tilde B_{tj},\tilde b_{tj})$, $j=1,\dots,N_t$, each with probability $1/N_t$, independently across stages, and the stage-$t$ constraint is $\tilde B_{tj}x_{t-1}+\tilde A_{tj}x_t=\tilde b_{tj}$. The SAA cost-to-go functions are defined backwards from $\widetilde{\mathcal Q}_{T+1}\equiv 0$:

$$\widetilde Q_{tj}(x_{t-1})=\inf_{x_t\ge0}\big\{\tilde c_{tj}^\top x_t+\widetilde{\mathcal Q}_{t+1}(x_t):\tilde B_{tj}x_{t-1}+\tilde A_{tj}x_t=\tilde b_{tj}\big\},\qquad \widetilde{\mathcal Q}_t=\frac1{N_t}\sum_{j=1}^{N_t}\widetilde Q_{tj}.$$

A scenario is a choice $(j_2,\dots,j_T)$; there are $N=\prod_t N_t$ of them, each of probability $1/N$. A policy $\bar x_t=\bar x_t(\tilde\xi_{[t]})$ depends only on the outcomes up to stage $t$; it is optimal for the SAA problem if it is feasible on every scenario and its expected cost $\frac1N\sum_{\text{scenarios}}\sum_t\tilde c_t^\top\bar x_t$ is minimal.

SDDP keeps, for each stage, a finite set of cuts $\alpha+\beta^\top x$ whose maximum $\mathfrak Q_{t+1}$ lies below $\widetilde{\mathcal Q}_{t+1}$. An iteration has a forward step: $M$ scenarios are sampled, and along each of them the decisions $\bar x_t$ solve the stage problems with $\mathfrak Q_{t+1}$ in place of $\widetilde{\mathcal Q}_{t+1}$, (3.13)–(3.14). It also has a backward step: from $t=T-1$ down to $1$, at each trial point $\bar x_t$ the stage-$(t+1)$ problems with the current cuts are solved for all $N_{t+1}$ outcomes, and the cut (3.17) $\ell(x)=\underline{\widetilde{\mathcal Q}}_{t+1}(\bar x_t)+\tilde g^\top(x-\bar x_t)$ is added, where $\tilde g$ averages $-\tilde B^\top\pi$ over basic optimal (extreme-point) dual solutions $\pi$.

Formalization targets

Goal: Proposition 3.1

Suppose the forward scenarios are drawn independently and uniformly from the SAA scenarios, (A1) holds ((3.13) and (3.14) have finite optimal values for every scenario at every iteration), and the backward steps use basic optimal dual solutions. Then

$$P\Big(\exists K\ \forall k\ge K:\ \text{the forward policy defined by }\mathfrak Q^k_2,\dots,\mathfrak Q^k_{T}\text{ is optimal for the SAA problem}\Big)=1 .$$

The goal fixes no iteration count, no rate and no number of forward scenarios $M\ge1$.

Milestones, in attack order

1. Attainment: an LP of the form (3.13)/(3.14) with finite optimal value has an optimal solution.
2. Cut validity: every cut lies below $\widetilde{\mathcal Q}_{t+1}$ on reachable decisions, and $\underline{\widetilde Q}_{tj}\le\widetilde Q_{tj}$.
3. Lower bound: the optimal value $\underline\vartheta_k$ of (3.13) is at most the SAA optimal value.
4. Finitely many cutting planes (3.17) for a fixed next-stage cut set, uniformly in the trial point.
5. Finitely many realizations of the $\mathfrak Q_t$ and of first-stage solutions; along each run the cut sets are eventually constant.
6. A policy is optimal for the SAA problem if and only if it satisfies the dynamic programming conditions (3.18) on every scenario.
7. With probability one every SAA scenario is drawn at infinitely many iterations.

Significance

The result separates SDDP's sampling from its convergence: on a finite scenario tree, independent subsampling of forward paths suffices for the method to stop at an optimal policy, without ever enumerating the tree. It explains why the lower bound $\underline\vartheta_k$ eventually equals the SAA optimal value, which is what makes the gap-based stopping rules of the paper (§3, Remarks 4–6) meaningful. The paper's closing remark stresses that without independence of the forward scenarios there is no guarantee of convergence.

The proposition is proved in the paper. No machine-checked proof of it, or of any SDDP convergence theorem, exists to our knowledge. Formalizing it requires a precise account of what the method is: which dual solutions, which forward solutions, which order of updates. Several of these points are left implicit on the page.

Difficulty

Finiteness of the cut universe (milestones 4–5) is a statement about extreme points of dual polyhedra whose dimension grows with the cut sets of the next stage, so it must be organized stage by stage from $T$ down. The central difficulty is the last step of the argument. Once the approximations have stopped changing, one must show that the stable cuts are exact where the forward policy goes, so that the forward policy satisfies (3.18). The obvious argument, "if (3.18) fails at the last stage where it fails, the next cut there increases $\mathfrak Q$", does not work as printed: (3.18) holding at later stages does not by itself make the next-stage approximation exact at the trial point. Closing this step is where the conventions on forward solutions and on sampling listed below become essential.

Formalization scope

The Lean development is in the namespace ShapiroSDDP.Convergence. Stages are numbered $1,\dots,T$; the data of stage $t+1$ are stored under index $t$ (the coupling matrix is indexed by the decision it multiplies); V t is $\widetilde{\mathcal Q}_{t+1}$, with V t ≡ 0 for $t\ge T$. Cost-to-go values are real infima, used only on reachable decisions. The explicit readings are:

• cost-to-go functions finite valued on reachable decisions (the paper: everywhere; weaker);
• initial cut sets: a parameter, nonempty and valid on reachable decisions, with $\{(0,0)\}$ at stage $T$;
• forward solutions from a deterministic oracle that reads the cut set and returns an optimal solution whenever one exists; the goal holds for every such oracle;
• basic optimal duals: extreme points of the dual feasible region, chosen arbitrarily; the goal holds for every run;
• (A1) as a hypothesis on the run; $M\ge1$ forward scenarios per iteration, i.i.d. uniform (independence via iIndepFun);
• forward step before backward step within an iteration, with cuts at that iteration's trial points.

Optimality of a policy is defined by expected cost, never by (3.18), so that milestone 6 is not definitional. Sampling is stated as i.i.d. uniform draws, not as "every scenario recurs", which is milestone 7. All of $c,A,B,b$ depend on the outcome. If some $\tilde A_{tj}$ lacks full row rank, no basic dual solution exists and no run exists; a sorry-free witness instance shows that all hypotheses of the goal can hold together.

Useful infrastructure: LP weak and strong duality (LinearOptimization.lp_weak_duality, LinearOptimization.lp_strong_duality exist on the platform in their own encoding), finiteness of extreme points of polyhedra, attainment for polyhedral objectives, and the second Borel–Cantelli lemma (ProbabilityTheory.measure_limsup_eq_one). Proofs of any milestone, and reusable lemmas on LPs with cut epigraphs, are welcome.

Selected references

• A. Shapiro, Analysis of Stochastic Dual Dynamic Programming Method, Optimization Online preprint 2009/12/2509; European Journal of Operational Research 209(1):63–72, 2011. https://optimization-online.org/2009/12/2509/ · https://doi.org/10.1016/j.ejor.2010.08.007
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52:359–375, 1991. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Operations Research Letters 36(4):450–455, 2008. https://doi.org/10.1016/j.orl.2008.01.013
• J. E. Kelley, The cutting-plane method for solving convex programs, J. SIAM 8(4):703–712, 1960. https://doi.org/10.1137/0108053
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751

Motivation

Many graph algorithms run in time proportional to the number of edges. A sparsifier of a weighted graph $G$ is a graph $H$ on the same vertices with far fewer edges that approximates $G$ for the purpose at hand, so that the algorithm can be run on $H$ instead. Benczúr and Karger (1996) showed that every graph has a sparsifier with $O(n\log n/\varepsilon^2)$ edges preserving the weight of every cut up to a factor $1\pm\varepsilon$. Spielman and Teng (2004) introduced the stronger spectral notion, in which the Laplacian quadratic form is preserved for every real vector, not only for cut indicators; their sparsifiers had $O(n\log^c n)$ edges for a large constant $c$ and were the first step of their nearly-linear-time solvers for symmetric diagonally dominant linear systems.

Spielman and Srivastava (arXiv:0803.0929, STOC 2008, SIAM J. Comput. 2011) proved that independent sampling of $O(n\log n/\varepsilon^2)$ edges, each edge with probability proportional to its weight times its effective resistance, yields a spectral sparsifier. The result improved both earlier bounds, replaced a recursive partitioning construction by a one-line sampling rule, and made effective resistance a standard tool in graph algorithms. Batson, Spielman and Srivastava (arXiv:0808.0163) later obtained $O(n/\varepsilon^2)$ edges deterministically, by a slower method built on the same matrix $\Pi$.

Setting

Let $G=(V,E,w)$ be a connected weighted undirected graph with $n=|V|$ vertices, $m=|E|$ edges and weights $w_e>0$. Orient every edge arbitrarily, so that it has a head and a tail (distinct vertices).

• The incidence matrix $B\in\mathbb R^{m\times n}$ has $B(e,v)=1$ if $v$ is the head of $e$, $-1$ if $v$ is its tail, and $0$ otherwise; $b_e$ denotes its row for $e$. $W$ is the diagonal $m\times m$ matrix with $W(e,e)=w_e$.
• The Laplacian is $L=B^{\mathsf T}WB$, with quadratic form $x^{\mathsf T}Lx=\sum_e w_e\,(x(\mathrm{head}\,e)-x(\mathrm{tail}\,e))^2$.
• $L^{+}$ is the Moore–Penrose pseudoinverse of $L$: if $L=\sum_{i=1}^{n-1}\lambda_iu_iu_i^{\mathsf T}$ over its nonzero eigenvalues, then $L^{+}=\sum_{i=1}^{n-1}\lambda_i^{-1}u_iu_i^{\mathsf T}$.
• The effective resistance of the edge $e$ is $R_e=b_eL^{+}b_e^{\mathsf T}$: the potential difference across $e$ when a unit current enters at one end and leaves at the other, the edges being resistors of conductance $w_e$.
• $\Pi=W^{1/2}BL^{+}B^{\mathsf T}W^{1/2}$ is an $m\times m$ matrix with $\Pi(e,e)=w_eR_e$.
• Sparsify$(G,q)$ draws $q$ edges independently with replacement, the edge $e$ with probability $p_e=w_eR_e/\sum_f w_fR_f$, and gives $e$ the weight $w_e/(qp_e)$ for each time it is drawn. Its output $H$ has Laplacian $\tilde L=B^{\mathsf T}W^{1/2}SW^{1/2}B$, where $S$ is the random diagonal matrix with $S(e,e)=\#\{\text{draws of }e\}/(qp_e)$.

Formalization targets

Goal: Theorem 1

There are an absolute constant $C$ and a threshold $N_0$ such that, for every $n\ge N_0$, every connected weighted graph on $n$ vertices and every $1/\sqrt n<\varepsilon\le1$, with $q=\lceil 9C^2n\log n/\varepsilon^2\rceil$, with probability at least $1/2$

$$\forall x\in\mathbb R^n:\qquad (1-\varepsilon)\,x^{\mathsf T}Lx\;\le\;x^{\mathsf T}\tilde Lx\;\le\;(1+\varepsilon)\,x^{\mathsf T}Lx .$$

The constant $C$ is left unfixed; the statement asserts the shape $q=O(n\log n/\varepsilon^2)$ with the paper's explicit dependence on $C$.

Milestones

1. Lemma 3 (four parts): $\Pi$ is an orthogonal projection; $\operatorname{im}\Pi=\operatorname{im}W^{1/2}B$; the eigenvalues of $\Pi$ are $1$ with multiplicity $n-1$ and $0$ with multiplicity $m-n+1$; $\Pi(e,e)=\|\Pi(\cdot,e)\|^2$.
2. Lemma 4: for a nonnegative diagonal $S$, $\|\Pi S\Pi-\Pi\Pi\|_2\le\varepsilon$ implies $(1-\varepsilon)x^{\mathsf T}Lx\le x^{\mathsf T}B^{\mathsf T}W^{1/2}SW^{1/2}Bx\le(1+\varepsilon)x^{\mathsf T}Lx$ for all $x$.
3. Lemma 5 (Rudelson–Vershynin): for independent samples $y_1,\dots,y_q$ of a random vector with $\|y\|_2\le M$ and $\|\mathbb E\,yy^{\mathsf T}\|_2\le1$, and $q\ge2$,

$$\mathbb E\Big\|\frac1q\sum_{j=1}^q y_jy_j^{\mathsf T}-\mathbb E\,yy^{\mathsf T}\Big\|_2\le CM\sqrt{\frac{\log q}{q}}\quad\text{whenever the right side is }<1.$$

Significance

Theorem 1 says that every weighted graph is spectrally approximated by a reweighted subgraph with $O(n\log n/\varepsilon^2)$ edges. A spectral approximation preserves cut weights, the eigenvalues of the Laplacian up to $1\pm\varepsilon$, effective resistances, and the condition number of $L$ as a preconditioner, so any algorithm whose output depends on these quantities can run on $H$. Combined with fast approximate computation of effective resistances (the second mission of this series), it gives a nearly-linear-time construction, and it is the sampling step used in Laplacian solvers, in sparsification of sums of rank-one matrices, and in leverage-score sampling for regression, where $w_eR_e$ is exactly the statistical leverage of a row.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission formalizes the statement and the paper's proof structure: the linear algebra of $\Pi$ (Lemma 3), the deterministic reduction from quadratic forms to a spectral-norm bound (Lemma 4), and the matrix concentration inequality (Lemma 5), which is the substantive analytic input and is itself a reusable result about sums of independent rank-one matrices.

Difficulty

The deterministic part is linear algebra over the pseudoinverse. The obstacle is concentration: the expected Laplacian of $H$ equals $L$, but bounding the deviation uniformly over all $x\in\mathbb R^n$ is a statement about the spectral norm of a random matrix, and a union bound over a net of directions costs a factor of $n$ in the sample count rather than $\log n$. Scalar Chernoff bounds per cut, which suffice for cut sparsifiers, do not give the spectral statement. Lemma 5 is the matrix inequality that removes this loss, and no inequality of this kind (a concentration bound for the spectral norm of a sum of independent random matrices) is in Mathlib.

Formalization scope

All declarations sit in the namespace EffResSparsify.Sampling.

• Graphs. A structure WGraph V E with orientation maps head, tail : E → V, weights w : E → ℝ, and the fields head e ≠ tail e (no loops) and 0 < w e. Parallel edges are allowed; nothing in §3 uses simplicity. Connectivity is a separate hypothesis on the underlying simple graph and includes $V\ne\emptyset$. In Theorem 1 the vertex type is Fin n; the edge type is an arbitrary finite type.
• Pseudoinverse. $L^{+}$ is the matrix of the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on Euclidean $\mathbb R^V$; it equals the spectral formula above and is the gauge-fixed inverse, never "some solution of $Lx=y$".
• Sampling. $p_e$ is defined as $w_eR_e/\sum_f w_fR_f$; the identity $\sum_f w_fR_f=n-1$ is part of the proof. An outcome of Sparsify is a sequence in $E^q$ with probability $\prod_i p_{s_i}$, and probabilities and expectations are finite sums over $E^q$, with no measure theory.
• Norms and logarithms. $\|\cdot\|_2$ is the $\ell_2$ operator norm on matrices (Matrix.Norms.L2Operator); vector norms in Lemma 5 are Euclidean; $\log$ is natural (the base is absorbed into $C$).
• Constants. In Theorem 1, $\exists C>0,\ \exists N_0,\ \forall n\ge N_0$ precede the graph and $\varepsilon$; the sample count is $\lceil 9C^2n\log n/\varepsilon^2\rceil$, rounded up because the printed value is not an integer. In Lemma 5, $\exists C>0$ precedes the dimension, the distribution, $M$ and $q$.
• Corrected statement. Lemma 5 as printed, with right side $\min(CM\sqrt{\log q/q},1)$, is false (at $q=1$ the bound is $0$). The formal milestone is Rudelson and Vershynin's own Theorem 3.1: $q\ge2$, and the bound $a=CM\sqrt{\log q/q}$ holds when $a<1$. It is stated for finitely supported distributions, which is all Theorem 1 uses. Theorem 1 applies it with $a\le\varepsilon/2$, so the correction does not affect the goal.
• Not a trivialization. Theorem 1 does not take Lemma 5, a bound on $\mathbb E\|\Pi S\Pi-\Pi\|_2$, or a free sample count as a hypothesis; a statement with any of these, or with "$\exists q$" in place of $\lceil 9C^2n\log n/\varepsilon^2\rceil$, is a different theorem.

Reusable beyond this mission: the weighted Laplacian with its pseudoinverse and effective resistances, and Lemma 5, which applies to any sampling scheme for sums of rank-one matrices (leverage-score sampling, column subset selection). Contributions toward a matrix Chernoff or Rudelson-type inequality in Mathlib are welcome.

Selected references

• D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
• M. Rudelson, R. Vershynin, Sampling from large matrices: an approach through geometric functional analysis, J. ACM 54(4), 2007. https://doi.org/10.1145/1255443.1255449
• M. Rudelson, Random vectors in the isotropic position, J. Funct. Anal. 164(1), 1999. https://doi.org/10.1006/jfan.1998.3384
• A. A. Benczúr, D. R. Karger, Approximating s-t minimum cuts in Õ(n²) time, STOC 1996. https://doi.org/10.1145/237814.237827
• D. A. Spielman, S.-H. Teng, Spectral sparsification of graphs, SIAM J. Comput. 40(4), 2011 (arXiv:0808.4134). https://arxiv.org/abs/0808.4134
• J. Batson, D. A. Spielman, N. Srivastava, Twice-Ramanujan sparsifiers, SIAM J. Comput. 41(6), 2012 (arXiv:0808.0163). https://arxiv.org/abs/0808.0163

Motivation

An investor who trades continuously in a market driven by Brownian motion, and who may only hold portfolios in a prescribed set, wants to maximize the expected utility of terminal wealth. With power utility $U_\gamma(x)=\frac1\gamma x^\gamma$, $\gamma\in(0,1)$, this is the constant-relative-risk-aversion problem that goes back to Merton (Merton 1971). When there are fewer stocks than sources of noise the market is incomplete, and when portfolio proportions are restricted (no short sales, bounded positions, a fixed allocation) the problem is constrained.

For convex constraints, duality methods settle the problem (Cvitanić–Karatzas 1992; Kramkov–Schachermayer 1999). They do not apply when the constraint set is closed but not convex, as for integer-lot or "all-or-nothing" restrictions. Hu, Imkeller and Müller (2005, arXiv:math/0508448) treat that case by a martingale optimality principle: they build a process that is a supermartingale for every admissible strategy and a martingale for one, and obtain it from a backward stochastic differential equation (BSDE) with a driver that grows quadratically in $z$. The existence theory for such equations is due to Kobylanski (2000).

This mission formalizes the power-utility result, Theorem 14 of the paper. A companion mission treats the exponential-utility result, Theorem 7.

Setting

Fix a horizon $T>0$ and a probability space $(\Omega,\mathcal F,P)$ carrying an $m$-dimensional Brownian motion $W$; $\mathbb F$ is the augmentation of its natural filtration. $|\cdot|$ is the Euclidean norm, and $\lambda$ is Lebesgue measure on $[0,T]$.

Market. There is a bond with zero interest and $d\le m$ stocks with prices $dS^i_t/S^i_t=b^i_t\,dt+\sigma^i_t\,dW_t$. The rates $b_t\in\mathbb R^d$ and the volatility $\sigma_t\in\mathbb R^{d\times m}$ are predictable and uniformly bounded, and $KI_d\ge\sigma_t\sigma_t^{\mathrm{tr}}\ge\varepsilon I_d$ for constants $K>\varepsilon>0$. The market price of risk is $\theta_t=\sigma_t^{\mathrm{tr}}(\sigma_t\sigma_t^{\mathrm{tr}})^{-1}b_t\in\mathbb R^m$.

Constraints. A closed set $\tilde C\subseteq\mathbb R^{1\times d}$ of row vectors constrains the proportions $\tilde\rho_t$ of wealth held in the stocks. In the variable $\rho_t=\tilde\rho_t\sigma_t\in\mathbb R^{1\times m}$ the constraint reads $\rho_t\in C_t(\omega)=\tilde C\sigma_t(\omega)$. For a closed $C\subseteq\mathbb R^m$, $\operatorname{dist}_C(a)=\min_{b\in C}|a-b|$, and $\Pi_C(a)=\{b\in C:|a-b|=\operatorname{dist}_C(a)\}$ is the (possibly multi-valued) projection.

Wealth and admissible strategies. From initial capital $x>0$ the wealth (11) is

$$X^{(\rho)}_t=x\exp\Big(\int_0^t\rho_s\,dW_s+\int_0^t\rho_s\theta_s\,ds-\tfrac12\int_0^t|\rho_s|^2\,ds\Big).$$

The admissible class $\tilde{\mathcal A}$ (Definition 13) consists of predictable $\rho$ with $\rho_t\in C_t$ for $\lambda\otimes P$-a.e. $(t,\omega)$ and $\int_0^T|\rho_s|^2\,ds<\infty$ a.s. The value is (12), $\bar V(x)=\sup_{\rho\in\tilde{\mathcal A}}E[U_\gamma(X^{(\rho)}_T)]$.

The BSDE. $\mathcal H^\infty(\mathbb R)$ is the class of predictable, $\lambda\otimes P$-a.e. bounded processes and $\mathcal H^2(\mathbb R^m)$ that of predictable $Z$ with $E\int_0^T|Z_t|^2\,dt<\infty$. The BSDE (15) is

$$Y_t=0-\int_t^TZ_s\,dW_s-\int_t^Tf(s,Z_s)\,ds,\qquad f(t,z)=\frac{\gamma(1-\gamma)}2\operatorname{dist}^2\Big(\frac{z+\theta_t}{1-\gamma},C_t\Big)-\frac{\gamma|z+\theta_t|^2}{2(1-\gamma)}-\frac12|z|^2 .$$

A BMO martingale $\int_0^\cdot\xi\,dW$ is one with $\sup_\tau\|E[\int_\tau^T|\xi_s|^2ds\mid\mathcal F_\tau]\|_\infty<\infty$ over stopping times $\tau\le T$ (equation (2)).

Formalization targets

Goal: Theorem 14

(15) has a unique solution $(Y,Z)\in\mathcal H^\infty(\mathbb R)\times\mathcal H^2(\mathbb R^m)$, and for $x>0$

$$\bar V(x)=\frac1\gamma\,x^\gamma\exp(Y_0),$$

attained by some $\rho^*\in\tilde{\mathcal A}$ with

$$\rho^*_t\in\Pi_{C_t(\omega)}\Big(\frac1{1-\gamma}(Z_t+\theta_t)\Big).\qquad(16)$$

The page prints $V(x)=x^\gamma\exp(Y_0)$; its proof measures utility by $x^\gamma$, so the value of (12) with $U_\gamma=\frac1\gamma x^\gamma$ carries the factor $\frac1\gamma$ (see Formalization scope).

Milestones

1. (14), p. 17: for $\rho\in C$, $\gamma\rho\theta-\frac12\gamma|\rho|^2+f(z)\le-\frac12|\gamma\rho+z|^2$, with equality on $\Pi_C\big(\frac{z+\theta}{1-\gamma}\big)$.
2. (H1), p. 18: $|f(t,z)|\le c_0+c_1|z|^2$.
3. Existence and 4. uniqueness for (15), p. 18.
4. Lemma 17, p. 20: $\int Z\,dW$ and $\int\rho^*dW$ are BMO martingales.
5. Optimality of $\rho^*$, p. 18: $\rho^*\in\tilde{\mathcal A}$ and $E[(X^{(\rho^*)}_T)^\gamma]=x^\gamma\exp(Y_0)$.
6. Comparison, p. 18: $E[(X^{(\rho)}_T)^\gamma]\le x^\gamma\exp(Y_0)$ for every $\rho\in\tilde{\mathcal A}$.

Significance

The theorem gives the value of a constrained power-utility problem in closed form through one scalar, $Y_0$, of a BSDE, and identifies an optimal strategy as a measurable selection of a projection onto the constraint set. Convexity of the constraint is not needed; when $\tilde C$ is a convex cone the result recovers the strategy obtained by other methods (Remark 16 of the paper). The same scheme handles exponential and logarithmic utility in the paper's other sections, and the dynamic programming principle of Proposition 15 follows from it.

The result is proved in the paper. As far as the platform's records show, none of it is formalized: there is no quadratic BSDE, no BMO martingale and no continuous-time utility-maximization statement on the platform. A complete formalization would add an existence and uniqueness theory for BSDEs with quadratic growth, the BMO criterion for stochastic exponentials, and a verification theorem for constrained portfolio problems, each reusable well beyond this paper.

Difficulty

The verification argument is short on paper; its inputs are not. Existence for (15) rests on Kobylanski's existence theorem for drivers of quadratic growth, which is not in Mathlib; the Lipschitz theory does not cover a driver growing like $|z|^2$. Uniqueness needs a comparison principle for such drivers. Lemma 17 and the martingale property of $\tilde R^{(\rho^*)}$ need the theory of BMO martingales and of their stochastic exponentials, also absent. The comparison milestone concerns processes that are only local supermartingales. A naive attempt that treats $\tilde R^{(\rho)}$ as a martingale for every admissible $\rho$ fails: for a general $\rho\in\tilde{\mathcal A}$, which is only locally square integrable, it is merely a local supermartingale.

Formalization scope

All declarations live in HuImkellerMuller.Power. Time is ℝ≥0; vectors of $\mathbb R^{1\times m}$ are EuclideanSpace ℝ (Fin m), with products $z\theta$ as inner products; $\tilde C$ is a Set (Fin d → ℝ). The Brownian motion, the augmented filtration, the measure $\lambda\otimes P$ and the Itô-integral operator I are reused from published definitions (EthierKurtz_IsStandardBrownian, CvitanicKaratzas92_Optimality_Market). The wealth is constructed from I, $\rho$ and $\theta$; $\theta$ is computed from $b$ and $\sigma$.

Conventions and disclosed readings:

• The factor $\frac1\gamma$. The goal states $\bar V(x)=\frac1\gamma x^\gamma\exp(Y_0)$ for (12) with $U_\gamma$; milestones 6–7 state $E[(X_T)^\gamma]$ against $x^\gamma\exp(Y_0)$, as the proof does.
• Added hypothesis $\tilde C\neq\emptyset$ (needed for (4) and for $\Pi_{C_t}\neq\emptyset$).
• Strategies are written in $\rho=\tilde\rho\sigma\in\mathbb R^m$ (Definition 13 says "$d$-dimensional"); §3's "$\bar C_2\subseteq\mathbb R^d$" and $\tilde C$ are one closed set.
• (16) and the constraint hold $\lambda\otimes P$-a.e.; "$\rho^*$ given by (16)" means any predictable selection.
• $Y_0$ is a.s. constant; the value identity holds for $P$-a.e. $\omega$.
• Uniqueness means $Y^1_t=Y^2_t$ a.s. for every $t$ and $Z^1=Z^2$ $\lambda\otimes P$-a.e.
• Expectations of nonnegative quantities are lower integrals in $[0,\infty]$; the value is a supremum in $[0,\infty]$.
• Ellipticity holds for $P$-a.e. $\omega$ and every $t\le T$; boundedness of $b$, $\sigma$ holds everywhere.

The value is a supremum of lower integrals, never of Bochner integrals: a Bochner expectation of a non-integrable $U_\gamma(X_T)$ is $0$ and would make the supremum meaningless. The goal asserts existence of a solution of (15) and does not take one as a hypothesis, so it cannot hold vacuously.

Contributions welcome: a theory of BSDEs with quadratic growth (Kobylanski), BMO martingales and Kazamaki's criterion, measurable selection of metric projections, and proofs of the deterministic milestone (14) and the growth bound (H1).

Selected references

• Y. Hu, P. Imkeller, M. Müller, Utility maximization in incomplete markets, Ann. Appl. Probab. 15(3), 2005, 1691–1712. https://doi.org/10.1214/105051605000000188 (arXiv:math/0508448v1, https://arxiv.org/abs/math/0508448)
• M. Kobylanski, Backward stochastic differential equations and partial differential equations with quadratic growth, Ann. Probab. 28(2), 2000, 558–602. https://doi.org/10.1214/aop/1019160253
• N. Kazamaki, Continuous Exponential Martingales and BMO, Lecture Notes in Math. 1579, Springer, 1994. https://doi.org/10.1007/BFb0073585
• J. Cvitanić, I. Karatzas, Convex duality in constrained portfolio optimization, Ann. Appl. Probab. 2(4), 1992, 767–818. https://doi.org/10.1214/aoap/1177005576
• D. Kramkov, W. Schachermayer, The asymptotic elasticity of utility functions and optimal investment in incomplete markets, Ann. Appl. Probab. 9(3), 1999, 904–950. https://doi.org/10.1214/aoap/1029962818
• R. C. Merton, Optimum consumption and portfolio rules in a continuous-time model, J. Econom. Theory 3, 1971, 373–413. https://doi.org/10.1016/0022-0531(71)90038-X

Linear decision rules for stochastic programs with random recourse

In a one-stage stochastic program a decision maker observes a random outcome $\xi$ and then picks a decision $x(\xi)$, subject to constraints that depend on $\xi$, so as to minimize expected cost. The optimization variable is a whole function $x$, and computing the optimal value is #P-hard even for a uniform distribution on the unit cube (Dyer and Stougie, 2006, cited in the paper as [16, Theorem 3.2]). A standard tractable approximation, introduced for robust optimization by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004) and carried to stochastic programming by Shapiro–Nemirovski and Chen–Sim–Sun, restricts decisions to linear decision rules $x(\xi)=X\xi$. This restriction gives an upper bound on the optimal value.

Kuhn, Wiesemann and Georghiou (2009/2011) study these approximations systematically. Their §3 treats the case where the constraint matrix itself depends on $\xi$ (random recourse). Linear decisions then produce constraints that are quadratic in $\xi$, and the paper reformulates the resulting semi-infinite problem as a semidefinite program. This mission formalizes that reformulation, the primal half of the paper's Theorem 2.

Setting

Uncertainty is a probability measure $\mathbb P$ on $\mathbb R^k$, with outcomes $\xi$. The support $\Xi$ of $\mathbb P$ is the smallest closed set of probability one. It is assumed to have the form

$$\Xi=\{\xi\in\mathbb R^k:\ e_1^\top\xi=1,\ \ \xi^\top W_\ell\xi\ge0,\ \ell=1,\dots,l\}\qquad(3.11)$$

for symmetric matrices $W_1,\dots,W_l$, where $e_1$ is the first standard basis vector. The first coordinate of every outcome is therefore $1$, so linear functions of $\xi$ are affine functions of the remaining coordinates. $\Xi$ is assumed nonempty and bounded, and its linear hull is assumed to be $\mathbb R^k$. Let $\mathbb S$ denote the symmetric $k\times k$ matrices and $M=\mathbb E(\xi\xi^\top)$ the second-moment matrix.

The data are $C\in\mathbb R^{n\times k}$ (cost $c(\xi)=C\xi$), $B\in\mathbb R^{m\times k}$ (right-hand side $b(\xi)=B\xi$, with rows $b_\mu^\top$), and $A_1,\dots,A_m\in\mathbb R^{k\times n}$, where the $\mu$th row of the recourse matrix $A(\xi)$ is $\xi^\top A_\mu$. The stochastic program $\mathcal{SP}$ minimizes $\mathbb E(c(\xi)^\top x(\xi))$ over square-integrable $x$ subject to $A(\xi)x(\xi)\le b(\xi)$ almost surely. It is strictly feasible if some square-integrable $\bar x,\bar s$ and some $\varepsilon>0$ satisfy $A(\xi)\bar x(\xi)+\bar s(\xi)=b(\xi)$ and $\bar s(\xi)\ge\varepsilon e$ almost surely.

With linear decisions $X\xi$ and quadratic slacks $\xi^\top S_\mu\xi$, $S_\mu\in\mathbb S$, one obtains the primal approximation

$$\mathcal{SP}^u:\quad \min\ \operatorname{Tr}(MC^\top X)\ \ \text{s.t.}\ \ \xi^\top A_\mu X\xi+\xi^\top S_\mu\xi=b_\mu^\top\xi,\ \ \xi^\top S_\mu\xi\ge0\ \ \mathbb P\text{-a.s.},\ \mu=1,\dots,m,$$

and the SDP (3.14)

$$\min\ \operatorname{Tr}(MC^\top X)\ \ \text{s.t.}\ \ \tfrac12(A_\mu X+X^\top A_\mu^\top)+S_\mu=\tfrac12(e_1b_\mu^\top+b_\mu e_1^\top),\ \ S_\mu-\textstyle\sum_\ell\Lambda_{\mu\ell}W_\ell\succeq0,\ \ \Lambda\ge0 .$$

Formalization targets

Goal: Theorem 2, primal half (p. 17)

$$\operatorname{Feas}(3.14)\ \text{projects into}\ \operatorname{Feas}\mathcal{SP}^u,\qquad \operatorname{val}\mathcal{SP}^u\le\operatorname{val}(3.14),$$ $$l=1\ \text{and}\ \mathcal{SP}\ \text{strictly feasible}\ \Longrightarrow\ \operatorname{val}\mathcal{SP}^u=\operatorname{val}(3.14).$$

Milestones

1. §3.2, (3.13), p. 12. The $\mu$th equality constraint of $\mathcal{SP}^u$ holds almost surely if and only if $H_\mu:=\tfrac12(A_\mu X+X^\top A_\mu^\top-e_1b_\mu^\top-b_\mu e_1^\top)+S_\mu=0$.
2. Lemma 1 (S-lemma), p. 12. If $\bar\xi^\top W\bar\xi>0$ for some $\bar\xi$, then $[\xi^\top W\xi\ge0\Rightarrow\xi^\top S\xi\ge0]\iff\exists\lambda\ge0:\ S\succeq\lambda W$. This is linked to the platform's proved S-procedure, of which it is the homogeneous case.
3. Proposition 6, p. 12. For symmetric $S$: $\exists\lambda\ge0$ with $S-\sum_\ell\lambda_\ell W_\ell\succeq0$ implies $\xi^\top S\xi\ge0$ almost surely, and the converse holds when $l=1$.

Significance

The theorem replaces a problem with infinitely many constraints, one per outcome, by a semidefinite program with $O(mk^2+ml)$ variables. Its value is always an upper bound on $\mathcal{SP}^u$, and hence on $\mathcal{SP}$. When the support is a single ellipsoid in the hyperplane $e_1^\top\xi=1$ ($l=1$), the bound loses nothing beyond the restriction to linear decisions. For $l>1$ the gap is unavoidable in general: an exact tractable reformulation would decide copositivity, which is NP-hard (Remark 7). Random recourse arises whenever technology or yield coefficients are uncertain, for example in production planning and portfolio problems with uncertain returns.

The result is proved in the paper. As far as is known it has no machine-checked proof. A formalization adds a precise statement of the hypotheses. Writing those hypotheses out showed that the unnumbered §3.2 step needs $\Xi$ to have dimension $k-1$, which spanning alone does not give for nonconvex $\Xi$ (see Formalization scope). The other half of Theorem 2, about the lower-bounding SDP (3.18), is false in this preprint and is not part of the mission.

Difficulty

The semi-infinite constraints hold only $\mathbb P$-almost surely. The first step is to pass from "almost surely" to "for every $\xi\in\Xi$", which uses that $\Xi$ is exactly the support and that the constraint functions are continuous. A bound $\mathbb P(\Xi)=1$ alone is not enough. For the equality constraints, a quadratic form that vanishes on $\Xi$ must vanish identically. This requires $\Xi$ to be large enough, and the obvious argument from "$\Xi$ spans $\mathbb R^k$" fails when $\Xi$ is a finite set. For the inequality constraints with $l=1$, the implication $\xi^\top W_1\xi\ge0\Rightarrow\xi^\top S\xi\ge0$ must be established on all of $\mathbb R^k$ and not only on the slice $e_1^\top\xi=1$. Doing so needs boundedness of $\Xi$ (no recession directions) and a strictly feasible point for the S-lemma. The S-lemma itself is a nonconvex duality statement. It is available on the platform.

Formalization scope

Outcomes live in Fin k → ℝ, with $k\ge1$ carried in the setting. Indices are 0-based: $\xi_1$ is coordinate 0, and $\mu,\ell$ range over Fin m, Fin l. "$\Xi$ is the support of $\mathbb P$" is stated as: $\Xi$ is closed, $\mathbb P(\Xi^{\mathrm c})=0$, and every ball centred in $\Xi$ has positive measure. Mathlib has no Measure.support at this revision. The standing assumptions (probability measure, symmetric $W_\ell$, support, nonempty, bounded, spanning) form one predicate assumed by every theorem. Decision rules are Borel measurable square-integrable functions. Optimal values are infima in EReal, $+\infty$ for an empty feasible set and $-\infty$ for an unbounded one. "Equivalent" means equal optimal values. Each $S_\mu$ is required symmetric in both problems; $\succeq$ is positive semidefiniteness and $\Lambda\ge0$ is componentwise. Strict feasibility of $\mathcal{SP}$ in §3 is the paper's condition (2.9) of §2 with $A$ replaced by $A(\xi)$. The paper uses the phrase without restating it.

Repairs and narrowings:

• Only the clauses of Theorem 2 about (3.14) and $\mathcal{SP}^u$ are stated. The clauses about (3.18) and $\mathcal{SP}^l$ are false in this preprint: a strictly feasible instance with $l=1$ has $\operatorname{val}(3.18)\approx1.170>\ln3=\operatorname{val}\mathcal{SP}$. Propositions 7–9 serve only that half and are not included. "Polynomial size, efficiently solvable" is informal and omitted.
• The §3.2 milestone carries the extra hypothesis that $\Xi$ contains a relatively open piece of the hyperplane $e_1^\top\xi=1$ (the paper's "dimension $k-1$", p. 10). Without it the claim is false for $l\ge2$. For $l=1$ the hypothesis follows from the standing assumptions, so the goal is unaffected.
• Strict feasibility is kept in the $l=1$ clause as printed, although the argument does not use it.

The goal cannot be trivialized through its definitions. Feasibility is quantified $\mathbb P$-almost surely for a measure whose support is $\Xi$, not over an empty or arbitrary set. Both optimal values are infima of the same real objective over the problems' own feasible sets. The standing assumptions are satisfiable, for instance by $k=2$, $W_1=\operatorname{diag}(1,-1)$, and $\mathbb P$ the uniform law on $\{1\}\times[-1,1]$.

The definitions (support of a measure, $\mathcal L^2$ decision rules, the random-recourse data) are reusable for the other sections of the paper and for related work on decision rules. Proofs of any milestone, Lean lemmas on quadratic forms vanishing on open cones, and an almost-sure-to-support transfer lemma are welcome.

Selected references

• D. Kuhn, W. Wiesemann, A. Georghiou, Primal and dual linear decision rules in stochastic and robust optimization, Optimization Online 2009/02/2218 (2009); Math. Program. 130 (2011) 177–209. https://optimization-online.org/wp-content/uploads/2009/02/2218.pdf, https://doi.org/10.1007/s10107-009-0331-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99 (2004) 351–376. https://doi.org/10.1007/s10107-003-0454-y
• S. Boyd, L. El Ghaoui, E. Feron, V. Balakrishnan, Linear Matrix Inequalities in System and Control Theory, SIAM Studies in Applied Mathematics 15, 1994 (the paper's source for Lemma 1). https://doi.org/10.1137/1.9781611970777
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Appendix B (the S-procedure as stated on the platform). https://web.stanford.edu/~boyd/cvxbook/
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X
• M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Math. Program. 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0

Motivation

Matrix completion asks to recover a large matrix from a small number of its entries. It is the abstraction behind collaborative filtering (recommender systems in which a users × items rating matrix is observed on a sparse set of pairs), sensor localization from partial distance information, and system identification. Without structure the problem is hopeless; the standard structural assumption is that the unknown matrix has low rank, and the standard convex surrogate for rank is the nuclear norm, the sum of singular values.

In the noiseless case, exact recovery by nuclear-norm minimization from about $r(m_1\vee m_2)\,\mathrm{polylog}$ uniformly sampled entries was established by Candès and Recht (2009) and refined by Candès and Tao (2010) and Gross (2011). With noisy observations the relevant question is a rate: how fast does an estimator's error decrease with the number $n$ of observed entries? Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256, Ann. Statist. 2011) introduced a nuclear-norm penalized estimator that uses the known sampling distribution, showed that in matrix completion it is an explicit soft thresholding of the singular values of a rescaled data matrix, and proved for it sharp oracle inequalities (leading constant 1) whose rates are optimal up to logarithmic factors. This mission formalizes the version of that result for bounded responses: Theorem 4 of the paper, together with the probabilistic lemma and the matrix Bernstein inequality it rests on.

Setting

Fix positive integers $n, m_1, m_2$ and write $\mathbb R^{m_1\times m_2}$ for the real $m_1\times m_2$ matrices, with scalar product $\langle A,B\rangle=\operatorname{tr}(A^\top B)$, Frobenius norm $\|A\|_2$, nuclear norm $\|A\|_1$ (sum of singular values) and operator norm $\|A\|_\infty$ (largest singular value). Set $m=m_1+m_2$ and write $m_1\wedge m_2=\min(m_1,m_2)$.

The matrix completion basis is

$$\mathcal X=\{e_j(m_1)e_k^\top(m_2):1\le j\le m_1,\ 1\le k\le m_2\},$$

where $e_k(m)$ are the canonical basis vectors of $\mathbb R^m$. One observes $n$ independent random pairs $(X_i,Y_i)$, where $X_i$ is uniformly distributed on $\mathcal X$ and $Y_i$ is real, following the trace regression model

$$\mathbb E(Y_i\mid X_i)=\operatorname{tr}(X_i^\top A_0),$$

for an unknown $A_0\in\mathbb R^{m_1\times m_2}$. Thus $Y_i$ is a noisy reading of the entry of $A_0$ selected by $X_i$; this is matrix completion under uniform sampling at random (USR), entries possibly sampled more than once.

The estimator is, for a regularization parameter $\lambda>0$,

$$\hat A^\lambda=\operatorname*{argmin}_{A\in\mathbb R^{m_1\times m_2}}\Big(\frac1{m_1m_2}\|A\|_2^2-\Big\langle\frac2n\sum_{i=1}^nY_iX_i,A\Big\rangle+\lambda\|A\|_1\Big).$$

The stochastic error is the random matrix

$$\mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big).$$

Formalization targets

Goal: Theorem 4

Assume $\max_i|Y_i|\le\eta$ almost surely. For $t>0$ and

$$\lambda\ge4\eta\max\Big\{\sqrt{\frac{t+\log m}{(m_1\wedge m_2)n}},\ \frac{2(t+\log m)}{n}\Big\},$$

with probability at least $1-e^{-t}$, simultaneously for all $A\in\mathbb R^{m_1\times m_2}$,

$$\|\hat A^\lambda-A_0\|_2^2\le\|A-A_0\|_2^2+m_1m_2\min\Big\{2\lambda\|A\|_1,\ \Big(\frac{1+\sqrt2}2\Big)^2m_1m_2\lambda^2\operatorname{rank}(A)\Big\}.$$

Milestones

1. (1.4): $\|A\|_{L_2(\Pi)}^2=\frac1n\sum_i\mathbb E\langle A,X_i\rangle^2=(m_1m_2)^{-1}\|A\|_2^2$ for the uniform design.
2. Theorem 1 for USR matrix completion: at every sample point where $\lambda\ge2\|\mathbf M\|_\infty$, the inequality above holds for all $A$ (a deterministic statement).
3. Proposition 1 (matrix Bernstein): for independent centred $m_1\times m_2$ random matrices $Z_i$ with $\|Z_i\|\le U$ a.s., with probability at least $1-e^{-t}$,

$$\Big\|\frac{Z_1+\dots+Z_n}n\Big\|\le2\max\Big\{\sigma_Z\sqrt{\frac{t+\log m}n},\ U\frac{t+\log m}n\Big\}.$$

4. (6.2): for $X$ uniform on $\mathcal X$, $\|X\|=1$, $\|\mathbb EX\|=(m_1m_2)^{-1/2}$, $\sigma_X^2=1/(m_1\wedge m_2)$.
5. Lemma 1: with probability at least $1-e^{-t}$, $\|\mathbf M\|\le2\eta\max\{\sqrt{(t+\log m)/((m_1\wedge m_2)n)},\ 2(t+\log m)/n\}$.

Significance

Theorem 4 is a non-asymptotic, sharp oracle inequality: the leading constant in front of $\|A-A_0\|_2^2$ is 1, so the bound applies to misspecified targets ($A_0$ not low rank) without loss. Taking $A=A_0$ and $t$ of order $\log m$ gives a normalized Frobenius error of order $\eta^2(m_1\vee m_2)\operatorname{rank}(A_0)\log(m)/n$, which the paper's minimax lower bounds (§4) show to be optimal up to the logarithm. Because no model is needed for Lemma 1, the same probability bound also drives the paper's statistical-learning reformulation (Theorem 9).

The theorems here are proved in the paper. What is open is their formalization: no matrix Bernstein inequality, and no oracle inequality for nuclear-norm penalized estimators, has a machine-checked proof on this platform. Proposition 1 in particular is a reusable concentration tool well beyond this paper (covariance estimation, random graphs, sketching).

Difficulty

The deterministic part (milestone 2) needs the subdifferential of the nuclear norm, which is not in Mathlib. The probabilistic part is where the obvious argument fails. Bounding $\|\mathbf M\|_\infty$ entrywise and summing, or bounding it by the Frobenius norm, loses a factor polynomial in the dimension; a union bound over a net of the unit sphere loses the factor $m_1\wedge m_2$ that makes the rate optimal. The correct rate requires a noncommutative Bernstein inequality, controlling the operator norm of a sum of independent random matrices through the matrix variance $\sigma_Z^2$ at the price of only a $\log(m_1+m_2)$ factor. The matrix-analytic machinery such inequalities depend on (trace inequalities for matrix exponentials, the passage from rectangular to symmetric matrices) is not currently available in Mathlib.

Formalization scope

All objects are local to the namespace KLTNuclear.Completion, built on the published MatrixCompletion definitions (RealMatrix, nuclearNorm, spectralNorm, frobeniusNormSq, matrixInner, coordinateMatrix). Conventions:

• The probability space carries IsProbabilityMeasure; $n,m_1,m_2\ge1$ are hypotheses. $\log$ is the natural logarithm; $m=m_1+m_2\ge2$.
• The design is encoded by uniform random indices $I_i\in[m_1]\times[m_2]$ with $X_i=e_{j_i}e_{k_i}^\top$. Mathlib has no $\sigma$-algebra on Matrix, so measurability, independence and conditioning on a random matrix use its entry array with the product $\sigma$-algebra; expectations of matrices are entrywise.
• The model (1.1) is a conditional expectation given $\sigma(X_i)$. Independence of the pairs $(X_i,Y_i)$ is the paper's standing assumption (p. 1) and is assumed in Lemma 1 and Theorem 4, whose proof applies Proposition 1 to $Z_i=Y_iX_i-\mathbb E(Y_iX_i)$; the $Y_i$ are not assumed identically distributed. $\lambda>0$ is the standing assumption of (1.6). Integrable responses are assumed in milestone 2, bounded measurable responses in Lemma 1 and Theorem 4.
• $\hat A^\lambda$ is any minimizer of (3.1) at each sample point (it exists and is unique, but neither fact is assumed); the soft-thresholding formula (3.2) is not used as a definition.
• "With probability at least $1-e^{-t}$" is encoded as an upper bound $e^{-t}$ on the outer measure of the failure set; in Theorem 4 the failure set is $\{\omega:\exists A,\ \text{(3.5) fails}\}$, so the bound is uniform in $A$. A formalization that fixes $A$ before the probability is weaker and is not the target.
• No printed slip affects these statements; Corollary 2(ii) of the paper, whose $\lambda$ falls below (3.6), is deliberately not included.

The source is the arXiv preprint arXiv:1011.6256v4. Welcome contributions: a general matrix Bernstein inequality (Hermitian and rectangular forms), the nuclear-norm subdifferential, and proofs of the deterministic milestone.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, Ann. Statist. 39(5), 2011; preprint arXiv:1011.6256v4. https://arxiv.org/abs/1011.6256
• J. A. Tropp, User-friendly tail bounds for sums of random matrices, Found. Comput. Math. 12, 2012. https://doi.org/10.1007/s10208-011-9099-z
• E. J. Candès, B. Recht, Exact matrix completion via convex optimization, Found. Comput. Math. 9, 2009. https://doi.org/10.1007/s10208-009-9045-5
• E. J. Candès, T. Tao, The power of convex relaxation: near-optimal matrix completion, IEEE Trans. Inform. Theory 56, 2010. https://doi.org/10.1109/TIT.2010.2044061
• D. Gross, Recovering low-rank matrices from few coefficients in any basis, IEEE Trans. Inform. Theory 57, 2011. https://doi.org/10.1109/TIT.2011.2104999

Motivation

Scheduling jobs whose processing times are not known in advance is a basic problem of production planning, project management and computing systems. In the stochastic machine scheduling model only the distribution of each processing time is known beforehand; the actual duration of a job is revealed when the job completes. A solution is then not a schedule but a scheduling policy, which decides at every point in time what to start next on the basis of what has been observed so far.

For precedence-constrained problems, constant-factor guarantees for policies were long unavailable. Möhring, Schulz and Uetz (J. ACM 1999) introduced LP relaxations with load inequalities for stochastic scheduling and obtained the first constant-factor policies for independent jobs. In the deterministic setting, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 2001) gave a list scheduling algorithm with deliberate idle times for $\mathrm P\,|\,r_j,\mathit{prec}\,|\sum w_jC_j$. Skutella and Uetz (SIAM J. Comput. 2005) combined the two and gave the first constant-factor approximation for stochastic scheduling with precedence constraints and release dates. This mission formalizes that result.

Setting

A finite set $V$ of jobs is to be scheduled on $m\ge1$ identical parallel machines, nonpreemptively. Precedence constraints are the arcs $A$ of an acyclic digraph: an arc $(i,j)$ requires $j$ to start no earlier than $i$ completes, and $i$ is a predecessor of $j$ if a directed path leads from $i$ to $j$. Job $j$ has a release date $r_j\ge0$, before which it must not start, and a weight $w_j\ge0$. Following §2 of the paper, release dates are assumed to respect the precedence constraints (Assumption 2.1: $r_i\le r_j$ whenever $i$ is a predecessor of $j$).

The processing time of job $j$ is a random variable $P_j\ge0$ with finite mean $\mathrm E[P_j]$; the $P_j$ are stochastically independent. For a realization $p$ of the processing times, a feasible schedule assigns start times $S_j\ge r_j$ such that $S_i+p_i\le S_j$ for every arc and at most $m$ jobs are in process at any time. A policy $\Pi$ maps realizations to feasible schedules; it is nonanticipatory if what it has started by time $t$ depends only on what has been observed by $t$. The completion time of $j$ under $\Pi$ is $C^\Pi_j(P)=S^\Pi_j(P)+P_j$.

The coefficient of variation is $\mathrm{CV}[P_j]=\sqrt{\mathrm{Var}[P_j]}/\mathrm E[P_j]$; the mission assumes $\mathrm{CV}[P_j]\le\sqrt\Delta$ for all $j$ and some $\Delta\ge0$. With $\mu_j=\mathrm E[P_j]$, the set function

$$f(W)=\frac1{2m}\Big(\big(\textstyle\sum_{j\in W}\mu_j\big)^2+\sum_{j\in W}\mu_j^2\Big)-\frac{(m-1)(\Delta-1)}{2m}\sum_{j\in W}\mu_j^2$$

defines the LP relaxation: minimize $\sum_jw_jC^{\mathrm{LP}}_j$ subject to $\sum_{j\in W}\mu_jC^{\mathrm{LP}}_j\ge f(W)$ for all $W\subseteq V$, $C^{\mathrm{LP}}_j\ge C^{\mathrm{LP}}_i+\mu_j$ for $(i,j)\in A$, and $C^{\mathrm{LP}}_j\ge\mu_j$.

Algorithm CMNS takes a priority list $L$ and a parameter $\beta$. Whenever a machine is idle and the first job of the residual list (the jobs not yet scheduled) is available, it is scheduled. Otherwise the first available job $j$ of the residual list is deliberately delayed; idle machines accumulate deliberate idle time charged to $j$, and once $j$ has been charged $\beta\,\mathrm E[P_j]$ it is scheduled out of order. The critical chain of a job $j$ is traced backwards through critical predecessors (those completing last, after $r_j$); its length is $\ell_j(p)$.

Formalization targets

Goal: Theorem 4.1

If $C^{\mathrm{LP}}$ is an optimal LP solution, $L$ orders the jobs by nondecreasing $C^{\mathrm{LP}}_j$ and $\beta>0$, then for every feasible nonanticipatory policy $\Pi$

$$\mathrm E\Big[\sum_jw_jC^{\mathrm{CMNS}}_j(P)\Big]\le(1+\beta)\Big(1+\frac1\beta+\max\Big\{1,\frac{m-1}m\Delta\Big\}\Big)\,\mathrm E\Big[\sum_jw_jC^\Pi_j(P)\Big].$$

Milestones

1. Observation 2.4: each job is charged at most $\beta\,\mathrm E[P_j]$; idle time while $j$ waits is charged to jobs before $j$; no deliberate idle time is uncharged.
2. Lemma 2.5: the per-realization bound $C_j(p)\le\frac{m-1}m\ell_j(p)+\frac1mr_j+\frac1m\big(\sum_{i\in B_j}(p_i+\beta\mathrm E[P_i])+\sum_{i\in O_j(p)}p_i\big)$.
3. Lemma 2.6: $\mathrm E[\sum_{i\in O_j(P)}P_i]=\mathrm E[\sum_{i\in O_j(P)}\mathrm E[P_i]]$.
4. Lemma 2.7: $\frac1m\mathrm E[\sum_{i\in O_j(P)}\mathrm E[P_i]]\le\frac1\beta\mathrm E[\ell_j(P)]$.
5. Theorem 2.8: $\mathrm E[C_j(P)]\le\big(\frac{m-1}m+\frac1\beta\big)\mathrm E[\ell_j(P)]+\frac{1+\beta}m\sum_{i\in B_j}\mathrm E[P_i]+\frac1mr_j$.
6. Theorem 3.1: the load inequalities $\sum_{j\in W}\mathrm E[P_j]\mathrm E[C^\Pi_j(P)]\ge f(W)$.
7. §3: expected completion times of any policy are LP-feasible, so the LP optimum is a lower bound.
8. Lemma 3.3: $\frac1m\sum_{k\le j}\mathrm E[P_k]\le\big(1+\max\{1,\frac{m-1}m\Delta\}\big)C^{\mathrm{LP}}_j$ along the LP order.
9. §4: $\ell_j(p)\le C_j(p)$ in any feasible schedule, so $\mathrm E[\ell_j(P)]$ is a lower bound for every policy.

Significance

The theorem gives a policy with a performance guarantee independent of the number of jobs for $\mathrm P\,|\,r_j,\mathit{prec}\,|\,\mathrm E[\sum w_jC_j]$, using only the expected processing times and a bound on their coefficients of variation. For NBUE distributions ($\Delta=1$) and $\beta=1/\sqrt2$ it yields $3+2\sqrt2\approx5.83$, matching the deterministic guarantee of Chekuri et al. The analysis separates cleanly into an algorithmic half (Theorem 2.8, valid for arbitrary distributions) and a polyhedral half (load inequalities and Lemma 3.3), both reused for the in-forest results of the same paper and in later work on stochastic scheduling.

The result is proved in the paper; it has no machine-checked proof. Formalizing it produces a precise definition of nonanticipatory policies and of a list scheduling algorithm with deliberate idle times in continuous time, a formal proof of the Möhring–Schulz–Uetz load inequalities, and a verified approximation guarantee for a stochastic scheduling policy.

Difficulty

Lemma 2.6 is the step where the stochastic setting departs from the deterministic one: the set $O_j(P)$ of out-of-order jobs is random and correlated with the schedule, and the identity holds only because the decision to start a job out of order is taken before its processing time is revealed. Making this rigorous requires a formal notion of nonanticipation and an independence argument over a random set. On the algorithmic side, the bookkeeping of deliberate idle time, which accumulates at a rate equal to the number of idle machines, must be made precise at instants where several jobs start, including jobs of length zero. The load inequalities compare every nonanticipatory policy at once and involve second moments of the processing times, so they cannot be checked policy by policy.

Formalization scope

Jobs form a finite type; arcs are a relation whose transitive closure is irreflexive; machine capacity is the counting condition "at most $m$ jobs in process", with half-open processing intervals. Processing times may be zero. The CV bound is encoded as finite second moments, positive means and $\mathrm{Var}[P_j]\le\Delta\,\mathrm E[P_j]^2$.

Algorithm CMNS is characterized by its rules: a decision order nondecreasing in time, the scheduling rule at each decision, and the condition that after the decisions at any time nothing remains to be done. A CMNS policy is a map $\sigma$ with this property for every realization. Nonanticipation and measurability of $\sigma$, which the paper asserts without proof (p. 795; §5), are hypotheses. Critical chains use a fixed tie-breaking order.

Standing assumptions and added hypotheses: independence, Assumption 2.1, $r_j\ge0$, $w_j\ge0$ and finite means appear in every statement where they are used. $\beta>0$ is assumed wherever $1/\beta$ appears (Lemma 2.7, Theorem 2.8), where the page allows $\beta\ge0$ with $1/0=\infty$. Lemma 2.6 assumes that $L$ is a linear extension, as in the surrounding Lemma 2.5 and Theorem 2.8; with zero processing times it fails otherwise. Comparator policies have integrable completion times and, like $\sigma$, are measurable for the law of $P$, which §5's requirement that every policy be universally measurable implies.

The goal is not trivialized: comparators range over every feasible nonanticipatory policy, not over list policies or the algorithm itself; $C^{\mathrm{LP}}$ is optimal over all $W\subseteq V$, not merely feasible; and the expected cost of CMNS is asserted to be finite, so neither side can collapse to a default integral value.

Contributions welcome: proofs of any milestone, in particular Theorem 3.1 and Lemma 3.3, which are reusable for the companion in-forest mission, and a proof that the CMNS rules determine a unique, nonanticipatory, measurable policy.

Selected references

• M. Skutella, M. Uetz, Stochastic machine scheduling with precedence constraints, SIAM J. Comput. 34(4) (2005) 788–802. https://doi.org/10.1137/S0097539702415007
• R. H. Möhring, A. S. Schulz, M. Uetz, Approximation in stochastic scheduling: the power of LP-based priority policies, J. ACM 46(6) (1999) 924–942. https://doi.org/10.1145/331524.331530
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1) (2001) 146–166. https://doi.org/10.1137/S0097539797327180
• R. H. Möhring, F. J. Radermacher, G. Weiss, Stochastic scheduling problems I: General strategies, Z. Oper. Res. 28 (1984) 193–260. https://doi.org/10.1007/BF01919323