The OR Formalization Drive

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the objective only through its values: the function is computed by a black-box code, and derivatives are unavailable or too expensive to program. Zeroth-order (derivative-free) methods address this setting. Classical derivative-free methods (pattern search, Nelder–Mead, model-based trust regions) come with weak or no global complexity guarantees for convex problems.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that replacing the gradient by a finite difference along a random Gaussian direction yields methods whose expected complexity is that of the corresponding gradient method multiplied by a factor proportional to the dimension. Their paper is a standard reference for zeroth-order convex optimization and for Gaussian smoothing, and its oracle and analysis are reused in bandit convex optimization, zeroth-order stochastic optimization (e.g. Ghadimi–Lan 2013) and derivative-free reinforcement learning.

This mission concerns Section 5 of the paper: the random gradient method $\mathcal{RG}_\mu$ for smooth convex functions and its linear rate for strongly convex ones.

Setting

Let $E$ be a real inner product space of finite dimension $n$, with norm $\|\cdot\|$. (The paper works with a space carrying an operator $B = B^* \succ 0$ and norm $\|x\| = \langle Bx, x\rangle^{1/2}$; choosing $\langle B\cdot,\cdot\rangle$ as the inner product gives exactly this setting, and the dual norm $\|\cdot\|_*$ becomes the norm of the Riesz representative.)

A function $f : E \to \mathbb R$ belongs to $C^{1,1}(E)$ with constant $L_1$ if it is differentiable and $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ for all $x, y$. It is strongly convex with parameter $\tau > 0$ if $f(y) \ge f(x) + \langle \nabla f(x), y - x\rangle + \frac{\tau}{2}\|y-x\|^2$ for all $x, y$.

Let $u$ be a standard Gaussian vector of $E$ (coordinates in any orthonormal basis are independent $N(0,1)$). The Gaussian approximation of $f$ with parameter $\mu \ge 0$ is $f_\mu(x) = \mathbb E_u f(x + \mu u)$, and the moments are $M_p = \mathbb E_u\|u\|^p$. The random gradient-free oracle returns, for a sampled direction $u$,

$$B^{-1}g_\mu(x) = \frac{f(x+\mu u) - f(x)}{\mu}\, u \quad (\mu > 0), \qquad B^{-1}g_0(x) = f'(x,u)\, u,$$

and the symmetric oracle is $B^{-1}\hat g_\mu(x) = \frac{f(x+\mu u) - f(x - \mu u)}{2\mu}u$.

Consider $f^* = \min_{x\in E} f(x)$ for a convex $f \in C^{1,1}(E)$, assumed solvable with a minimizer $x^*$, and $n \ge 2$. The random gradient method $\mathcal{RG}_\mu$ (Eq. (54), p. 546) is:

Method $\mathcal{RG}_\mu$: Choose $x_0 \in E$. Iteration $k \ge 0$. a). Generate $u_k$ and corresponding $g_\mu(x_k)$. b). Compute $x_{k+1} = x_k - hB^{-1}g_\mu(x_k)$.

The directions $u_0, u_1, \dots$ are independent standard Gaussian vectors, and $\phi_k = \mathbb E f(x_k)$ (with $\phi_0 = f(x_0)$).

Formalization targets

Goal: Theorem 8 (p. 546)

With step size $h = \frac{1}{4(n+4)L_1}$ and any $\mu \ge 0$, for every $N \ge 0$,

$$\frac{1}{N+1}\sum_{k=0}^{N}(\phi_k - f^*) \le \frac{4(n+4)L_1\|x_0-x^*\|^2}{N+1} + \frac{9\mu^2(n+4)^2L_1}{25},$$

and, if $f$ is strongly convex with parameter $\tau > 0$, then with $\delta_\mu = \frac{18\mu^2(n+4)^2}{25\tau}L_1$,

$$\phi_N - f^* \le \frac12 L_1\left[\delta_\mu + \left(1 - \frac{\tau}{8(n+4)L_1}\right)^{N}\big(\|x_0-x^*\|^2 - \delta_\mu\big)\right].$$

Both bounds are one theorem with one proof in the paper, so the goal states their conjunction, with every constant as printed.

Milestones

The milestones are the results the paper's proof of Theorem 8 rests on, in attack order:

1. Lemma 1 (p. 534): $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$.
2. Theorem 3.1, (32) (p. 537): $\mathbb E_u\|g_0(x)\|_*^2 \le (n+4)\|\nabla f(x)\|_*^2$ at a point of differentiability.
3. Theorem 4.2, (35) (p. 538): $\mathbb E_u\|g_\mu(x)\|_*^2 \le \frac{\mu^2}{2}L_1^2(n+6)^3 + 2(n+4)\|\nabla f(x)\|_*^2$, and the same with $\frac{\mu^2}{8}$ for $\hat g_\mu$.
4. Eq. (21) (pp. 534–535): for $\mu > 0$, $f_\mu$ is differentiable with $\nabla f_\mu(x) = \mathbb E_u B^{-1}g_\mu(x)$.
5. Eq. (25) (p. 535): $\mathbb E_u \langle\nabla f(x), u\rangle u = \nabla f(x)$, the $\mu = 0$ counterpart.
6. Convexity of $f_\mu$ (p. 533) and Eq. (11): $f \le f_\mu$ for convex $f$.
7. Theorem 1, (19) (p. 534): $|f_\mu(x) - f(x)| \le \frac{\mu^2}{2}L_1 n$.

Significance

The result. Theorem 8 shows that a method using two function values per iteration reaches accuracy $\epsilon$ on a smooth convex problem in $O(\frac{n}{\epsilon}L_1\|x_0 - x^*\|^2)$ iterations, and in $O(\frac{nL_1}{\tau}\ln\frac{L_1\|x_0-x^*\|^2}{\epsilon})$ iterations under strong convexity, provided $\mu$ is small enough. This is $n$ times the complexity of the deterministic gradient method, which is the natural price for replacing an $n$-dimensional gradient by one directional estimate. The strongly convex bound makes explicit the bias floor $\frac12 L_1\delta_\mu$ caused by the finite-difference step, and shows that it vanishes for the limiting method $\mathcal{RG}_0$.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. A formalization produces a reusable Gaussian-smoothing layer on Mathlib's stdGaussian (moments of the Gaussian norm, differentiation of $f_\mu$ under the integral, variance bounds of random oracles) and a complete expected-complexity proof of a randomized first-order method, in which the probabilistic structure (independent directions, iterates depending only on past directions, tower property) has to be handled explicitly.

Difficulty

The deterministic part of the argument is the textbook analysis of gradient descent. The difficulty is in the Gaussian facts it uses. The obvious bound on the oracle's second moment, $\mathbb E\langle\nabla f(x),u\rangle^2\|u\|^2 \le \|\nabla f(x)\|^2 M_4 \le (n+4)^2\|\nabla f(x)\|^2$, loses a factor of $n$ and would give a quadratic dependence on dimension; the $(n+4)$ of (32) needs a sharper computation. The moment bounds of Lemma 1 for non-integer $p$ and the differentiation under the integral in (21) are measure-theoretic steps that Mathlib does not package. Finally, the step from per-iteration inequalities to bounds on $\phi_k$ requires conditioning on the past directions, which must be set up on a probability space carrying the whole sequence $u_0, u_1, \dots$.

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space with MeasurableSpace and BorelSpace, $n$ is Module.finrank ℝ E, and $\nabla f$ is Mathlib's gradient. Expectations over $u$ are Bochner integrals against ProbabilityTheory.stdGaussian E. A run of $\mathcal{RG}_\mu$ lives on a probability space $(\Omega, P)$: measurable directions $u_k$, jointly independent (iIndepFun) with law stdGaussian E, iterates with $x_0$ deterministic and the update holding for every $k$ and outcome. $\phi_k$ is ∫ ω, f (x k ω) ∂P. The oracle is defined by cases, with $f'(x,u)u$ at $\mu = 0$ ($f'(x,u)$ the one-sided directional derivative of Eq. (23), a Filter.limUnder, which equals fderiv ℝ f x u for differentiable $f$), so the goal covers every $\mu \ge 0$ as the paper claims. $L_1$ and $\tau$ are any constants satisfying the defining inequalities. The standing assumptions of Section 5 (convexity, a global minimizer $x^*$, $n \ge 2$) and $L_1 > 0$ are explicit hypotheses; $n \ge 2$ is needed for the constant $9/25$.

A trivializing formalization is ruled out: the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the true gradient (which would be deterministic gradient descent), and every expectation in the statements is of a quantity that is integrable under the stated hypotheses, so no bound holds through a junk value of a non-integrable integral.

A complete development needs Gaussian moment computations in finite dimension, differentiation under the integral sign for $f_\mu$, the variance bounds of the oracles, and a conditional-expectation argument for the iteration. The smoothing layer is reusable for the companion missions on random search for nonsmooth problems and on the accelerated random method, and for other zeroth-order methods. Contributions of any of the milestones, of general Gaussian-integrability lemmas, or of alternative proofs are welcome.

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4):2341–2368, 2013. https://doi.org/10.1137/120880811
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

In network revenue management a firm sells $n$ products that consume $m$ capacitated resources over $T$ periods, and in each period it chooses which offer set of products to make available. When customers choose among the offered products according to a choice model, the standard planning tool is the choice-based linear program, which assigns a frequency $u_S\ge 0$ to every offer set $S\subseteq N$ (Liu and van Ryzin 2008). It has $2^n$ variables. Its optimal solution is what the firm actually implements: a randomization over offer sets.

For the Markov chain choice model of Blanchet, Gallego and Goyal (2016), Feldman and Topaloglu (2017) show that the choice-based program is equivalent to a reduced linear program with only $2n$ variables. The reduced program can be solved directly, but its solution is a pair of vectors $(\hat x,\hat z)$, not a randomization over offer sets. This mission formalizes the paper's Section 7, which converts the reduced solution back into a randomization over offer sets: the Dimension Reduction algorithm, and Theorem 9, which says that the algorithm produces at most $n+1$ offer sets and that these sets are nested.

Setting

Products are indexed by $N=\{1,\dots,n\}$. A customer arrives wanting product $j$ with probability $\lambda_j$. If the product she visits is offered, she buys it. Otherwise she moves to product $i$ with probability $\rho_{j,i}$, and leaves without buying with probability $1-\sum_{i\in N}\rho_{j,i}$. Throughout, $\lambda_j>0$, $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j,i$.

For an offer set $S\subseteq N$, the (Balance) equations

$$P_{j,S}+R_{j,S}=\lambda_j+\sum_{i\in N}\rho_{i,j}R_{i,S}\ \ \forall j\in N,\qquad P_{j,S}=0\ \ \forall j\notin S,\qquad R_{j,S}=0\ \ \forall j\in S$$

have a unique solution. $P_{j,S}$ is the probability that product $j$ is purchased, and $R_{j,S}$ is the expected number of visits to $j$ while it is not offered. Write $P_S=(P_{j,S})_j$ and $R_S=(R_{j,S})_j$.

The set $\mathcal H$ consists of all pairs $(x,z)\in\mathbb R^n\times\mathbb R^n$ with $x,z\ge0$ and $x_j+z_j=\lambda_j+\sum_{i}\rho_{i,j}z_i$ for all $j$. The (Reduced) linear program maximizes $\sum_j T r_j x_j$ over $(x,z)\in\mathcal H$ subject to the capacity rows $\sum_j T a_{q,j}x_j\le c_q$ for each resource $q$.

The Dimension Reduction algorithm starts from the optimal solution $(\hat x,\hat z)$ of (Reduced) and sets $(x^1,z^1)=(\hat x,\hat z)$. At iteration $k$ it forms $S^k=\{j: x^k_j>0\}$. It stops with $\alpha^k=1$ if $S^k=\emptyset$. Otherwise it sets $\alpha^k=\min\{x^k_j/P_{j,S^k}: j\in S^k\}$, stops if $\alpha^k=1$, and if not updates

$$x^{k+1}_j=\frac{x^k_j-\alpha^kP_{j,S^k}}{1-\alpha^k},\qquad z^{k+1}_j=\frac{z^k_j-\alpha^kR_{j,S^k}}{1-\alpha^k}.$$

The weights are $\gamma^k=(1-\alpha^1)\cdots(1-\alpha^{k-1})\alpha^k$.

Formalization targets

Goal: Theorem 9

Let $(\hat x,\hat z)$ be optimal for (Reduced). The algorithm stops at some first iteration $K$ with $1\le K\le n+1$. At that $K$,

$$\hat x=\sum_{k=1}^K\gamma^kP_{S^k},\qquad \hat z=\sum_{k=1}^K\gamma^kR_{S^k},\qquad \sum_{k=1}^K\gamma^k=1,\qquad S^1\supseteq S^2\supseteq\cdots\supseteq S^K .$$

Milestones

In the order the proof uses them:

1. (Balance) has a unique, nonnegative solution for every $S$ (p. 1325).
2. $P_{j,S}>0$ for $j\in S$ (p. 1325).
3. For $(\hat x,\hat z)\in\mathcal H$: $\hat z_j\ge R_{j,S_{\hat x}}$. This is Lemma 11 of the online appendix, as quoted on p. 1332.
4. For $(\hat x,\hat z)\in\mathcal H$ with nonempty support: $\alpha_{\hat x}\le1$ (p. 1332).
5. The two stopping configurations are (Balance) solutions: $S_{\hat x}=\emptyset$ gives $(P_\emptyset,R_\emptyset)$, and $\alpha_{\hat x}=1$ gives $(P_{S_{\hat x}},R_{S_{\hat x}})$ (p. 1332).
6. Lemma 8: one step of the algorithm maps $\mathcal H$ into $\mathcal H$ and removes a minimizing index from the support (p. 1333).
7. The iterates stay in $\mathcal H$, and $S^{k+1}\subseteq S^k\setminus\{j^k\}$ (pp. 1333–1334).

Significance

Theorem 9 makes the reduced program usable. Together with the equivalence of (Reduced) and the choice-based program, it produces an optimal choice-based solution that offers at most $n+1$ sets. By a basic-solution count the choice-based program has an optimal solution with at most $m+1$ nonzero offer sets. Theorem 9 bounds the number by the number of products instead, and adds a structural property: the offered sets form a chain. Each set is contained in the previous one, so the implemented policy offers a single nested sequence of assortments. The algorithm needs at most $n+1$ solutions of linear systems of size $n$. It never enumerates offer sets.

The result is proved in the paper. As far as a search of the platform and of Mathlib shows, it has not been formalized. Mathlib's Carathéodory theorem (Analysis/Convex/Caratheodory) bounds the number of points in a convex combination. It does not construct this decomposition, and it does not give nestedness. Formalizing Theorem 9 therefore requires the paper's argument: a verified, terminating peeling procedure on the polyhedron $\mathcal H$ whose output is a convex combination of (Balance) solutions indexed by a chain of sets.

Difficulty

The algorithm divides twice. Step 2 divides by $P_{j,S^k}$, which must be positive on $S^k$. Step 3 divides by $1-\alpha^k$, which must be nonzero whenever the algorithm continues. Both rest on nontrivial facts: the positivity of purchase probabilities, and the bound $\alpha\le1$ on $\mathcal H$. That bound in turn requires the comparison $\hat z\ge R_{S_{\hat x}}$. The paper proves this comparison only in its online appendix; it is a monotonicity property of the inverse of $I-\rho^\top$ restricted to the unoffered products. The update of Step 3 can make coordinates of $z$ negative unless this comparison holds, so the naive observation that "$(x^k,z^k)$ is a combination of points of $\mathcal H$" does not by itself keep the iterates in $\mathcal H$.

Termination is not a consequence of $\alpha^k<1$ alone. It needs the strict decrease of the support, which comes from choosing a minimizing index. The weights $\gamma^k$ are defined by products of the $(1-\alpha^l)$. Their sum telescopes to $1$ only because the last step has $\alpha^K=1$.

Formalization scope

Everything lives in the namespace MarkovChainChoice.DimReduction. Products are Fin n and offer sets are Finset (Fin n). The model is a structure carrying $\lambda_j>0$, $\sum_i\rho_{j,i}<1$ and, as a disclosed implicit hypothesis, $\rho_{j,i}\ge0$. The pair $(P_S,R_S)$ is chosen by Classical.epsilon among the solutions of (Balance); milestone 1 is what identifies it with the paper's unique solution. Revenues, capacities and consumptions carry no sign conditions. "Optimal for (Reduced)" means feasible and at least as good as every feasible point.

The iterates are indexed from $k=1$ as in the paper. The value at index $0$ is an unused copy of the input. "The algorithm stops at iteration $K$" is the first $K\ge1$ with $S^K=\emptyset$ or $\alpha^K=1$. Iterates after the first stop involve a division by zero, which Lean evaluates to $0$, and no statement refers to them. The termination bound $K\le n+1$ is a conclusion of the goal, not a hypothesis. The goal is about the algorithm's actual iterates, not about an arbitrary sequence that satisfies the invariants. The paper's $\subset$ and $\supset$ denote non-strict inclusion and are rendered as $\subseteq$ and $\supseteq$.

Two milestones are stated more generally than the page. The paper states the iteration invariants for the (Reduced) optimum; the Lean requires only $(\hat x,\hat z)\in\mathcal H$, which every feasible (Reduced) solution satisfies. Lemma 8's $\arg\min$ may be a set; the statement holds for every minimizer. The page contains printed slips: on p. 1332, $\hat v_j$ has numerator $\hat x_j-\alpha R_{j,S}$, and the paper writes $R_{\hat x}$ for $R_{S_{\hat x}}$. The Lean uses the correct forms, as in Lemma 8 and Step 3. None of these slips appears in a milestone quotation.

A complete development needs a small theory of M-matrices, in the form of nonnegativity of $(I-Q)^{-1}$ for substochastic $Q$, together with finite induction on supports. The comparison lemma (milestone 3) and the (Balance) existence and uniqueness result (milestone 1) are reusable across the other missions on this paper. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• J. B. Feldman, H. Topaloglu, Revenue Management Under the Markov Chain Choice Model, Operations Research 65(5):1322–1342, 2017. https://doi.org/10.1287/opre.2017.1628
• J. Blanchet, G. Gallego, V. Goyal, A Markov Chain Approximation to Choice Modeling, Operations Research 64(4):886–905, 2016. https://doi.org/10.1287/opre.2016.1505
• Q. Liu, G. van Ryzin, On the Choice-Based Linear Programming Model for Network Revenue Management, Manufacturing & Service Operations Management 10(2):288–310, 2008. https://doi.org/10.1287/msom.1070.0169

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access only to function values: the objective is the output of a simulator or a black-box program, and its gradient is unavailable or too expensive. Derivative-free (or zeroth-order) methods address this setting. Nesterov and Spokoiny (Found. Comput. Math. 17 (2017)) showed that a very simple oracle, the finite difference of $f$ along a random Gaussian direction, can replace the gradient in standard first-order schemes at the price of a factor depending only on the dimension. Their analysis became the reference point for later work on zeroth-order stochastic optimization and on gradient-free methods in reinforcement learning and adversarial attacks.

This mission covers Section 6 of the paper: the accelerated random method $\mathcal{FG}_\mu$ and its rate, Theorem 9. It is the third mission of a series; the first covers random search for nonsmooth problems (Theorem 6), the second the random gradient method for smooth problems (Theorem 8).

Setting

Let $E$ be a real inner product space of dimension $n \ge 2$ with norm $\|\cdot\|$ (the paper's space with operator $B$ is $E$ with the inner product $\langle Bx, y\rangle$). Let $u$ be a standard Gaussian vector in $E$, and write $\mathbb E_u$ for expectation over $u$.

The objective $f : E \to \mathbb R$ is differentiable with Lipschitz gradient, $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ with $L_1 > 0$, and strongly convex with parameter $\tau \ge 0$:

$$f(y) \ge f(x) + \langle\nabla f(x), y - x\rangle + \tfrac{\tau}{2}\|y - x\|^2 .$$

The value $\tau = 0$ is allowed (plain convexity). The condition number is $\kappa = \tau/L_1$. The problem $f^* = \min_{x \in E} f(x)$ is assumed solvable, with minimizer $x^*$.

For $\mu \ge 0$ the Gaussian approximation is $f_\mu(x) = \mathbb E_u f(x + \mu u)$, and the random gradient-free oracle is

$$B^{-1}g_\mu(x) = \frac{f(x + \mu u) - f(x)}{\mu}\,u \quad (\mu > 0), \qquad B^{-1}g_0(x) = \langle\nabla f(x), u\rangle\,u .$$

The paper (p. 548) sets $\theta_n = 1/(16(n+1)^2L_1(f))$ and $h_n = 1/(4(n+4)L_1(f))$. This mission uses $\theta_n = 1/(16(n+4)^2L_1)$; the reason is given under Formalization scope. Method $\mathcal{FG}_\mu$ (Eq. (60)) chooses $x_0 \in E$, $v_0 = x_0$ and $\gamma_0 > 0$ with $\gamma_0 \ge \tau$, and at every iteration $k \ge 0$:

1. computes $\alpha_k > 0$ with $\theta_n^{-1}\alpha_k^2 = (1 - \alpha_k)\gamma_k + \alpha_k\tau \equiv \gamma_{k+1}$;
2. sets $\lambda_k = \alpha_k\tau/\gamma_{k+1}$, $\beta_k = \alpha_k\gamma_k/(\gamma_k + \alpha_k\tau)$ and $y_k = (1-\beta_k)x_k + \beta_k v_k$;
3. draws a fresh Gaussian direction $u_k$, independent of the past, and computes $g_\mu(y_k)$;
4. sets $x_{k+1} = y_k - h_n B^{-1}g_\mu(y_k)$ and $v_{k+1} = (1-\lambda_k)v_k + \lambda_k y_k - (\theta_n/\alpha_k)B^{-1}g_\mu(y_k)$.

Write $\phi_k = \mathbb E f(x_k)$ (expectation over $u_0, \dots, u_{k-1}$), $\psi_k = \prod_{i=0}^{k-1}(1-\alpha_i)$ and $C_k = 1 + \sum_{i=1}^{k-1}\prod_{j=k-i}^{k-1}(1-\alpha_j)$ for $k \ge 1$, with $\psi_0 = 1$ and $C_0 = 0$ (p. 550).

Formalization targets

Goal: Theorem 9 (p. 549)

For all $k \ge 0$,

$$\phi_k - f^* \le \psi_k\Big[f(x_0) - f(x^*) + \frac{\gamma_0}{2}\|x_0 - x^*\|^2\Big] + \mu^2 L_1\Big(n + \frac{3(n+8)}{16}C_k\Big), \tag{62}$$

where

$$\psi_k \le \min\Big\{\Big(1 - \frac{\kappa^{1/2}}{4(n+4)}\Big)^k,\ \Big(1 + \frac{k}{8(n+4)}\sqrt{\frac{\gamma_0}{L_1}}\Big)^{-2}\Big\}, \qquad C_k \le \min\Big\{k,\ \frac{4(n+4)}{\kappa^{1/2}}\Big\}.$$

The two regimes are a rate $O(n^2/k^2)$ for convex $f$ and a linear rate with ratio $1 - \kappa^{1/2}/(4(n+4))$ for strongly convex $f$, both up to a bias proportional to $\mu^2$.

Milestones

In attack order: Lemma 1 (Gaussian moments, (16)–(17)); Theorem 3.1 (the bound (32) on the second moment of $g_0$); Theorem 1's (19), $|f_\mu - f| \le \frac{\mu^2}{2}L_1 n$; Eq. (12), $L_1(f_\mu) \le L_1(f)$; Lemma 5, the bound (37) on $\mathbb E_u\|g_\mu(x)\|_*^2$ in terms of $\nabla f_\mu(x)$; Eq. (21), $\nabla f_\mu = \mathbb E_u g_\mu$; and Eq. (11), $f_\mu \ge f$ for convex $f$.

Significance

Theorem 9 shows that the $n$-fold slowdown of gradient-free methods relative to their gradient counterparts survives acceleration: $\mathcal{FG}_\mu$ reaches accuracy $\epsilon$ in $O(n L_1^{1/2}R/\epsilon^{1/2})$ iterations for convex $f$, against $O(nL_1R^2/\epsilon)$ for the non-accelerated random gradient method. The analysis also quantifies how small the finite-difference step $\mu$ must be for this to hold. The result is used as the baseline accelerated zeroth-order rate in later work.

The theorem is proved in the paper. As far as is known it has not been machine-checked, and Mathlib has no Gaussian smoothing, no random gradient-free oracle and no analysis of an accelerated method driven by random directions. A formal proof also settles the constant question raised by the printed $\theta_n$ (see below).

Difficulty

The deterministic fast gradient method is analysed by an estimate-sequence argument in which the gradient step is exact. Here the step uses $g_\mu(y_k)$, which is an unbiased estimate of $\nabla f_\mu(y_k)$ and not of $\nabla f(y_k)$, and whose second moment is of order $n\|\nabla f_\mu\|^2$ plus a bias term. The step size and the coupling parameter $\theta_n$ must absorb this second moment, and the argument must be run for $f_\mu$ rather than $f$. The estimate sequence then has to be passed through expectations over the history $u_0, \dots, u_{k-1}$, which requires the independence of $u_k$ from $x_k, v_k, y_k$ and integrability of every quantity involved. Transporting the result from $f_\mu$ back to $f$ uses (11) and (19), and requires that $f_\mu$ inherits strong convexity with the same parameter $\tau$, a fact the paper uses without stating it.

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space (InnerProductSpace ℝ E, FiniteDimensional ℝ E, Borel measurable), $n$ is Module.finrank ℝ E, and the Gaussian is Mathlib's stdGaussian E. The operator $B$ is absorbed into the inner product, so $\nabla f$ is gradient f and $B^{-1}g_\mu$ is $\frac{f(x+\mu u)-f(x)}{\mu}u$. This is not a restriction to $B = I$ on $\mathbb R^n$. All expectations are Bochner integrals; under the hypotheses every integrand is integrable, so no integrability hypothesis is added.

The run is a structure over a probability space $(\Omega, \mathbb P)$: directions $u_k$ that are measurable, mutually independent (iIndepFun) and standard Gaussian; deterministic sequences $\gamma, \alpha$ satisfying step a) as equations; and random points $x_k, v_k$ satisfying steps b)–d) for every outcome. The smoothing parameter satisfies $\mu \ge 0$, and at $\mu = 0$ the oracle is $g_0$. The goal pins $\theta = 1/(16(n+4)^2L_1)$ and $h = 1/(4(n+4)L_1)$. $\psi_k$ and $C_k$ are definitions computed from $\alpha$.

The constant $\theta_n$. The paper prints $\theta_n = \frac{1}{16(n+1)^2L_1(f)}$. The proof (pp. 549–550) needs $\frac{h_n}{4(n+4)} - \frac{h_n^2L_1}{2} = \frac{1}{32(n+4)^2L_1} = \frac{\theta_n}{2}$, $\alpha_k \ge [\tau\theta_n]^{1/2} = \frac{\kappa^{1/2}}{4(n+4)}$ and $\theta_n^{1/2} = \frac{1}{4(n+4)L_1^{1/2}}$, which hold only with $(n+4)$. With the printed value $\theta_n$ is larger than the first inequality allows, and the argument does not go through. The mission therefore states Theorem 9 with $\theta_n = \frac{1}{16(n+4)^2L_1}$; all other constants are as printed.

Two trivializing formalizations are ruled out. First, the bound $C_k \le 4(n+4)/\kappa^{1/2}$ carries the hypothesis $\tau > 0$: at $\tau = 0$ the paper's value is $+\infty$, while Lean's division by zero would turn it into $C_k \le 0$, which is false. $\psi_k$ and $C_k$ are definitions from the run, not free variables that only satisfy the bounds. Second, the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the exact gradient (which would give Nesterov's deterministic method) and not an arbitrary direction sequence.

A complete development needs Gaussian integration by parts in an inner product space, moment bounds for $\|u\|$, differentiation under the integral sign for $f_\mu$, and conditional expectation along an i.i.d. sequence. The smoothing layer (Lemma 1, (11), (12), (19), (21), (32), (37)) is reusable for any zeroth-order method, and contributions of these components as separate lemmas are welcome.

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (Lemma 2.2.4 and Section 2.2.1, the estimate-sequence analysis the proof of Theorem 9 follows). https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Minimizing the total weighted completion time $\sum_j w_j C_j$ of jobs with release dates on a single machine, written $1\,|\,r_j\,|\,\sum w_j C_j$ in scheduling notation, is strongly NP-hard. It is one of the basic models of machine scheduling, and it has served as a test case for a general technique in approximation algorithms: solve a linear programming relaxation, read off a preemptive schedule, and convert it into a nonpreemptive one using $\alpha$-points, the times at which a given fraction of each job has been processed. Phillips, Stein and Wein (doi:10.1007/BF01585872) introduced ordering jobs by points of a preemptive schedule; Goemans (SODA 1997, reference [11] of the paper below) and Chekuri, Motwani, Natarajan and Stein (doi:10.1137/S0097539797327180) showed that choosing $\alpha$ at random improves the guarantee.

Goemans, Queyranne, Schulz, Skutella and Wang (doi:10.1137/S089548019936223X) combine two LP relaxations, shown to have equal value, with carefully chosen random $\alpha$. This mission formalizes their Theorem 3.5: when a single $\alpha$ is drawn from a truncated exponential density, the resulting schedule costs in expectation at most $c < 1.7451$ times the LP lower bound.

Timeline:

• 1998: Phillips, Stein and Wein give the first constant-factor approximation (ratio $2$) for the unit-weight problem $1\,|\,r_j\,|\,\sum C_j$ by converting a preemptive schedule.
• 1997: Goemans (SODA) introduces randomly chosen $\alpha$-points for the weighted problem, the conference precursor of the paper formalized here.
• 2001: Chekuri, Motwani, Natarajan and Stein give a randomized $e/(e-1) \approx 1.58$-approximation for the unit-weight problem.
• 2002: Goemans, Queyranne, Schulz, Skutella and Wang give $1.7451$ for a single random $\alpha$ (Theorem 3.5) and $1.6853$ for job-dependent random $\alpha_j$ (Theorem 3.9), both against the same LP bound.
• 1999: Afrati et al. (doi:10.1109/SFFCS.1999.814574) give a polynomial-time approximation scheme for the problem. It is not LP-based, so the LP-relative factors of Theorems 3.5 and 3.9 remain of interest as bounds on the relaxations' integrality gaps.

Setting

There are $n$ jobs $N = \{1, \dots, n\}$. Job $j$ has an integral processing time $p_j > 0$, an integral release date $r_j \ge 0$ and a weight $w_j > 0$. The jobs are indexed so that $w_1/p_1 \ge w_2/p_2 \ge \cdots \ge w_n/p_n$.

A preemptive schedule gives each job a set $A_j \subseteq [r_j, \infty)$ of processing times of measure $p_j$, the sets pairwise disjoint. The mean busy time of $j$ is $M_j = \frac{1}{p_j}\int_{A_j} t\,dt$.

The LP schedule is the preemptive schedule that always processes the available job of smallest index, which under the indexing above is the available job of largest ratio $w_j/p_j$. Its mean busy times are $M^{LP}_j$.

The mean busy time relaxation (R) minimizes $\sum_j w_j (M_j + \tfrac12 p_j)$ subject to $\sum_{j \in S} p_j M_j \ge p(S)\big(r_{\min}(S) + \tfrac12 p(S)\big)$ for every nonempty $S \subseteq N$, where $p(S) = \sum_{j\in S} p_j$ and $r_{\min}(S) = \min_{j\in S} r_j$. Its optimal value is $Z_R$, a lower bound on the optimum of $1\,|\,r_j\,|\,\sum w_j C_j$.

For $0 < \alpha \le 1$, the $\alpha$-point $t_j(\alpha)$ is the first time at which $j$ has received $\alpha p_j$ units of processing in the LP schedule, and $t_j(0^+)$ is its start time. The $\alpha$-schedule processes the jobs nonpreemptively, each as early as possible, in nondecreasing order of $t_j(\alpha)$; $C^\alpha_j$ is the completion time of $j$ in it. More generally, the $(\alpha_j)$-schedule orders the jobs by $t_j(\alpha_j)$ for a vector $\boldsymbol\alpha = (\alpha_j)$.

Let $0 < \gamma < 1$ solve $1 - \frac{\gamma^2}{1+\gamma} = \gamma + \ln(1+\gamma)$ ($\gamma \approx 0.4675$), and set

$$c = \frac{1+\gamma}{1+\gamma-e^{-\gamma}}, \qquad \delta = 1 - \frac{\gamma^2}{1+\gamma}, \qquad f(\alpha) = \begin{cases}(c-1)e^{\alpha} & 0 < \alpha \le \delta,\\ 0 & \text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 3.5

If $\alpha$ is drawn with density $f$, then $c < 1.7451$, the expectation below is finite, and

$$\mathbb E_f\Big[\sum_{j} w_j C^\alpha_j\Big] \le c \cdot Z_R .$$

Milestones

1. Theorem 2.5: $M^{LP}$ is an optimal solution to (R), so $Z_R = \sum_j w_j (M^{LP}_j + \tfrac12 p_j)$.
2. Eq. (3.1): $M^{LP}_j = \int_0^1 t_j(\alpha)\,d\alpha$.
3. Corollary 3.2: $C^{\boldsymbol\alpha}_j \le t_j(\alpha_j) + \sum_{k:\,\alpha_k\le\eta_k(\alpha_j)} (1+\alpha_k-\eta_k(\alpha_j))\,p_k$, where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$ in the LP schedule.
4. Eq. (3.10): $M^{LP}_j = t_j(0^+) + \sum_{k\in N_2}(1-\mu_k)p_k + \tfrac12 p_j$, where $N_2$ is the set of jobs processed between the start and the completion of $j$ and $\mu_k$ the fraction of $j$ done before $k$ starts.
5. Eq. (3.11): the bound of Corollary 3.2 rewritten in terms of $N_1$, $N_2$ and $\mu_k$.
6. Lemma 3.6: $f$ is a density on $[0,1]$ with $\int_0^\eta f(\alpha)(1+\alpha-\eta)\,d\alpha \le (c-1)\eta$ and $\int_\mu^1 f(\alpha)(1+\alpha)\,d\alpha \le c(1-\mu)$ for $\eta, \mu \in [0,1]$.

Significance

Theorem 3.5 is a randomized $1.7451$-approximation for $1\,|\,r_j\,|\,\sum w_j C_j$, and simultaneously a bound on the integrality gap of (R): every instance has $\mathrm{OPT} \le 1.7451\, Z_R$. The paper also derandomizes it: there are at most $n$ distinct $\alpha$-schedules (its Proposition 3.8), and the best of them can be found in $O(n^2)$ time. The paper remarks that the truncated exponential density is optimal for its analysis and that the factor is tight for it.

On the formal side, the mission produces a reusable model of single-machine preemptive schedules, the LP schedule, $\alpha$-points and list scheduling, and the first machine-checked instance of the $\alpha$-point rounding technique that recurs across scheduling approximation. The result itself is proved in the paper; no machine-checked proof of it or of the LP-schedule identities (3.1), (3.10) is known to exist.

Difficulty

The obvious approach, bounding each $C^\alpha_j$ separately by a multiple of $t_j(\alpha)$, gives only the factor $\max\{1 + 1/\alpha, 1 + 2\alpha\}$ for fixed $\alpha$ (Theorem 3.3 of the paper), which is at least $1+\sqrt2$. The improvement needs the precise structure of the LP schedule around each job: which jobs interrupt $j$ ($N_2$) and which do not ($N_1$), and how the fraction $\eta_k(\alpha)$ of each other job depends on $\alpha$. Turning this structure into exact identities for piecewise-constant, piecewise-linear functions of $\alpha$ defined through a recursively built schedule is the bulk of the formal work. The analytic part (Lemma 3.6) is elementary but depends on the specific equation that defines $\gamma$.

Formalization scope

Jobs are Fin n (0-based) with $p, r : \texttt{Fin } n \to \mathbb N$ and real weights. The sortedness $w_j/p_j \ge w_k/p_k$ for $j \le k$, positivity $p_j > 0$ and $w_j > 0$ are hypotheses of every theorem about the LP schedule. Because the data are integral, the LP schedule is defined slot by slot on unit intervals $[\tau, \tau+1)$; a job's processing set is a finite union of such intervals. $\alpha$-points are infima over reals, and every statement restricts $\alpha$ to $(0,1]$. The $(\alpha_j)$-schedule's completion times are given by the closed form of list scheduling, $C_j = \max_{k \preceq j}(r_k + \sum_{k \preceq i \preceq j} p_i)$, with ties of $\alpha$-points broken by index (they do not occur for $\alpha \in (0,1]$). $Z_R$ is the infimum of the objective of (R) over its feasible set. The random $\alpha$ has law $f(\alpha)\,d\alpha$ on $\mathbb R$, and the expectation is a Lebesgue integral.

The goal asserts integrability of $\alpha \mapsto \sum_j w_j C^\alpha_j$ together with the bound, so the inequality cannot hold through the convention that a non-integrable function has integral $0$. The bound is against $Z_R$ defined from (R), not against $\sum_j w_j (M^{LP}_j + \tfrac12 p_j)$, which would build Theorem 2.5 into the goal; and the density's support $(0,\delta]$ is written out, so no mass is placed outside $(0,1]$. The running-time claims are not formalized, and the uniqueness of $\gamma$ is not asserted: the statements hold for every solution in $(0,1)$.

Useful infrastructure: finite unions of intervals and their measures, monotone piecewise-linear functions and their integrals, and list-scheduling identities. Contributions to any milestone, and general lemmas about the LP schedule (it is a preemptive schedule, has no idle time inside a job's span, processes interrupting jobs completely), are welcome.

Selected references

• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single Machine Scheduling with Release Dates, SIAM J. Discrete Math. 15(2):165–192, 2002. doi:10.1137/S089548019936223X
• C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998. doi:10.1007/BF01585872
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 591–598, 1997 (no DOI; reference [11] of Goemans et al. 2002).
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31(1):146–166, 2001. doi:10.1137/S0097539797327180
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th IEEE FOCS, 32–43, 1999. doi:10.1109/SFFCS.1999.814574

Motivation

Scheduling jobs with release dates on one machine to minimize the total weighted completion time, written $1|r_j|\sum w_jC_j$, is strongly NP-hard even with unit weights (Lenstra, Rinnooy Kan & Brucker, 1977). It is a basic model of scheduling theory and a standard testbed for approximation algorithms built on linear programming relaxations. Several LP relaxations give lower bounds for it (Dyer & Wolsey, 1990; Queyranne, 1993), and the question how far these bounds can be from the optimum is also a question about the quality of branch-and-bound methods that use them.

Timeline, as surveyed in Table 1 of Goemans, Queyranne, Schulz, Skutella & Wang (2002):

• Phillips, Stein & Wein (Math. Programming, 1998) introduce converting a preemptive schedule into a nonpreemptive one by list scheduling, and the notion of $\alpha$-points; for the weighted problem their bound is $16+\epsilon$.
• Hall, Shmoys & Wein (SODA 1996) obtain 4; Schulz (IPCO 1996) and Hall, Schulz, Shmoys & Wein (Math. Oper. Res., 1997) obtain 3; Chakrabarti et al. obtain $2.8854+\epsilon$, and a combination of methods gives $2.4427+\epsilon$.
• Goemans (SODA 1997) orders jobs by $\alpha$-points of the LP schedule: $\alpha=1/\sqrt2$ gives $1+\sqrt2\approx2.4143$, a uniformly random $\alpha$ gives 2.
• Chekuri, Motwani, Natarajan & Stein (SIAM J. Comput., 2001) use random $\alpha$-points of an arbitrary preemptive schedule and obtain $e/(e-1)$ for unit weights, relative to the preemptive optimum rather than an LP value.
• Goemans, Queyranne, Schulz, Skutella & Wang (2002) prove $1.7451$ for the best common $\alpha$ and $1.6853$ for job-dependent random $\alpha_j$, both relative to the LP value $Z_R$. Afrati et al. (FOCS 1999) later give a polynomial-time approximation scheme, which does not bound the LP relaxations.

This mission formalizes the $1.6853$ result, the paper's main theorem.

Setting

There are $n$ jobs $N=\{0,\dots,n-1\}$. Job $j$ has an integral processing time $p_j>0$, an integral release date $r_j\ge0$ and a weight $w_j>0$. The jobs are indexed so that $w_0/p_0\ge w_1/p_1\ge\dots\ge w_{n-1}/p_{n-1}$.

The LP schedule is the preemptive schedule that at every moment processes the available (released, unfinished) job of smallest index. Since the data are integral, it is determined slot by slot: in $[\tau,\tau+1)$ it runs the smallest-index job $j$ with $r_j\le\tau$ and work left, or idles. Let $A^{LP}_j\subseteq\mathbb R$ be the set of times at which it processes $j$. The mean busy time of $j$ is

$$M^{LP}_j=\frac1{p_j}\int_{A^{LP}_j}t\,dt .$$

The mean busy time relaxation (R) has a variable $M_j$ per job:

$$Z_R=\min\Bigl\{\sum_j w_j\bigl(M_j+\tfrac12p_j\bigr)\ :\ \sum_{j\in S}p_jM_j\ge p(S)\bigl(r_{\min}(S)+\tfrac12p(S)\bigr)\ \text{for all nonempty }S\subseteq N\Bigr\},$$

with $p(S)=\sum_{j\in S}p_j$ and $r_{\min}(S)=\min_{j\in S}r_j$. $Z_R$ is a lower bound on the optimum of $1|r_j|\sum w_jC_j$.

For $0<\alpha\le1$ the $\alpha$-point $t_j(\alpha)$ is the first time at which $j$ has been processed for $\alpha p_j$ units in the LP schedule; $t_j(0^+)$ is the start time of $j$. For a vector $\boldsymbol\alpha\in(0,1]^n$, the $(\alpha_j)$-schedule processes the jobs nonpreemptively, as early as possible, in nondecreasing order of $t_j(\alpha_j)$; $C^{\boldsymbol\alpha}_j$ is the completion time of $j$ in it.

Let $\gamma\approx0.4835$ be the solution in $(0,1)$ of $\gamma+\ln(2-\gamma)=e^{-\gamma}\bigl((2-\gamma)e^{\gamma}-1\bigr)$, and set

$$\delta=\gamma+\ln(2-\gamma)\approx0.8999,\qquad c=1+\frac{e^{-\gamma}}{\delta},\qquad g(\alpha)=\begin{cases}(c-1)e^\alpha&0<\alpha\le\delta,\\0&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 3.9 (p. 185)

$c<1.6853$, and if $\alpha_1,\dots,\alpha_n$ each have density $g$ and are pairwise independent, then $\sum_j w_jC^{\boldsymbol\alpha}_j$ is integrable and

$$\mathbb E\Bigl[\sum_j w_jC^{\boldsymbol\alpha}_j\Bigr]\le c\cdot Z_R .$$

The bound is against the constant $c$ defined by the formula; the decimal $1.6853$ appears only in the separate inequality $c<1.6853$.

Milestones

1. Theorem 2.5 (p. 173): $M^{LP}$ is an optimal solution of (R), so $Z_R=\sum_jw_j(M^{LP}_j+\tfrac12p_j)$.
2. Eq. (3.1) (p. 176): $M^{LP}_j=\int_0^1t_j(\alpha)\,d\alpha$.
3. Corollary 3.2 (p. 179): $C^{\boldsymbol\alpha}_j\le t_j(\alpha_j)+\sum_{k:\alpha_k\le\eta_k(\alpha_j)}(1+\alpha_k-\eta_k(\alpha_j))p_k$, where $\eta_k(\alpha_j)$ is the fraction of $k$ processed by $t_j(\alpha_j)$.
4. Eq. (3.10) (p. 182): $M^{LP}_j=t_j(0^+)+\sum_{k\in N_2}(1-\mu_k)p_k+\tfrac12p_j$, where $N_2$ is the set of jobs processed between the start and completion of $j$ and $\mu_k$ is the fraction of $j$ processed before $k$ starts.
5. Eq. (3.11) (p. 183): the bound of Corollary 3.2 split over $N_1=N\setminus(N_2\cup\{j\})$ and $N_2$.
6. Lemma 3.11 (p. 185): $g$ is a probability density on $(0,1]$, and (i) $\int_0^\eta g(\alpha)(1+\alpha-\eta)\,d\alpha\le(c-1)\eta$, (ii) $(1+E_g[\alpha])\int_\mu^1g(\alpha)\,d\alpha\le c(1-\mu)$ for $\eta,\mu\in[0,1]$.

Significance

Theorem 3.9 gives a randomized algorithm for $1|r_j|\sum w_jC_j$ whose expected cost is at most $1.6853$ times the optimum, and a variant of it runs on-line (Theorem 3.14). Since $Z_R$ is a lower bound, it also shows that the relaxation (R), and the preemptive time-indexed relaxation (D), which has the same value, is within a factor $1.6853$ of the optimum (Corollary 3.10). The paper's Section 3.6 shows the gap of these relaxations can approach $e/(e-1)\approx1.5819$, so the bound is not far from what this relaxation can give.

The result is proved on paper; no machine-checked proof exists, and no part of this theory (LP schedule, $\alpha$-points, list scheduling from a preemptive schedule) is on the platform. The mission produces, besides the goal, a reusable formal account of $\alpha$-point scheduling: the LP schedule as a concrete object, the identity between mean busy times and average $\alpha$-points, and the deterministic completion-time bound of Corollary 3.2, which underlies many later $\alpha$-point analyses.

Difficulty

The obvious argument, bounding $C^{\boldsymbol\alpha}_j$ by Corollary 3.2 and integrating each $\alpha_k$ independently against $g$, does not work directly: the set of jobs $k$ with $\alpha_k\le\eta_k(\alpha_j)$ depends on $\alpha_j$, and the two effects of the random $\alpha_k$ pull in opposite directions (a small $\alpha_k$ shrinks the terms $1+\alpha_k-\eta_k$, a large one removes terms from the sum). The analysis needs the structure of the LP schedule around job $j$ (equations (3.9)–(3.11)) to separate the jobs whose $\eta_k$ is constant in $\alpha_j$ from those for which it jumps from $0$ to $1$, and then a density tuned to both at once. The claim is made under pairwise independence only, so no product structure of the random vector is available. On the formal side, the LP schedule, $\alpha$-points and list scheduling are defined from scratch, and the measure-theoretic content (integrability of a piecewise-constant function of $\boldsymbol\alpha$, conditioning under pairwise independence) is real work.

Formalization scope

Jobs are Fin n (0-based), $p$ and $r$ are natural numbers and $w$ is real. The ordering by $w_j/p_j$ is a hypothesis of every statement about the LP schedule, which is defined by the smallest-index rule; under that hypothesis the two coincide. The LP schedule is defined slot by slot, which is exact for integral data. Processing is represented by sets of times, not indicator functions. $t_j(\alpha)$ is an infimum over times, $t_j(0^+)=\inf A^{LP}_j$, and the $(\alpha_j)$-schedule is the closed form $C^{\boldsymbol\alpha}_j=\max_{k\preceq j}\bigl(r_k+\sum_{k\preceq i\preceq j}p_i\bigr)$ of list scheduling in lexicographic (α-point, index) order. $Z_R$ is the real infimum of the objective over the feasible set of (R), which is nonempty and bounded below for $w\ge0$. The random vector is any probability measure on $\mathbb R^n$ whose coordinate laws all equal the law with density $g$ and whose coordinates are pairwise independent; the product measure is one example, but the theorem is for all of them. $\gamma$ is any solution in $(0,1)$ of its equation.

A trivializing formalization is ruled out: the expectation is asserted together with integrability (a non-integrable integrand would have Bochner integral $0$), $g$ is supported on $(0,\delta]$ so every $\alpha_j$ lies in $(0,1]$ almost surely, and the bound is against $Z_R$ defined from (R), not against an expression that already contains Theorem 2.5.

Running times ($O(n\log n)$, $O(n^2)$), derandomization, the counting results (Proposition 3.8, Lemma 3.12) and the on-line variant are not formalized. Lemma 3.1 on the auxiliary $(\alpha_j)$-Conversion schedule is not a milestone; Corollary 3.2 is stated directly for the $(\alpha_j)$-schedule.

Contributions welcome: proofs of the milestones in any order; general lemmas on list scheduling and $\alpha$-points of preemptive schedules, which are reusable beyond this mission; and the measure-theoretic step from pairwise independence to the conditional bound on $\mathbb E[C^{\boldsymbol\alpha}_j\mid\alpha_j]$.

Selected references

• M. X. Goemans, M. Queyranne, A. S. Schulz, M. Skutella, Y. Wang, Single machine scheduling with release dates, SIAM J. Discrete Math. 15(2):165–192, 2002. https://doi.org/10.1137/S089548019936223X
• C. Phillips, C. Stein, J. Wein, Minimizing average completion time in the presence of release dates, Math. Programming 82:199–223, 1998.
• L. A. Hall, A. S. Schulz, D. B. Shmoys, J. Wein, Scheduling to minimize average completion time: off-line and on-line approximation algorithms, Math. Oper. Res. 22:513–544, 1997. https://doi.org/10.1287/moor.22.3.513
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM–SIAM SODA, 591–598, 1997.
• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation techniques for average completion time scheduling, SIAM J. Comput. 31:146–166, 2001. https://doi.org/10.1137/S0097539797327180
• M. E. Dyer, L. A. Wolsey, Formulating the single machine sequencing problem with release dates as a mixed integer program, Discrete Appl. Math. 26:255–270, 1990.
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Ann. Discrete Math. 1:343–362, 1977.