Optimization

Motivation

Many optimization problems of operations research have objectives that are convex but not differentiable: Lagrangian duals of integer and combinatorial programs, maxima of finitely many affine or smooth functions, penalty functions for systems of inequalities, and the value functions produced by decomposition. For such functions the gradient method and steepest descent fail. Constant steps cannot work because the subgradients need not tend to zero at a nondifferentiable minimum, and exact line search along the negative gradient can converge to a point that is not a minimizer (the example on pp. 22–23 of the source).

The subgradient method replaces the gradient by an arbitrary subgradient and gives up monotone decrease of the objective. Its convergence theory is the foundation of nondifferentiable optimization and of Lagrangian relaxation in integer programming.

Timeline. N. Z. Shor proposed the method with normalized steps in 1962 (Kiev). Yu. M. Ermoliev proved convergence in finite dimensions with divergent-series stepsizes (Kibernetika, 1966), and B. T. Polyak proved it for constrained problems in Hilbert space (Doklady Akad. Nauk SSSR, 1967). Held, Wolfe and Crowder (Mathematical Programming, 1974) brought the method to large combinatorial problems through Lagrangian relaxation. This mission formalizes the exposition of Section 2.1–2.2 of Shor's monograph (Springer, 1985), which gives self-contained proofs of these results.

Setting

Let $E_n$ be the $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. Let $f : E_n \to \mathbb{R}$ be a convex function finite everywhere. A vector $g$ is a subgradient of $f$ at $x_0$ if

$$f(x) - f(x_0) \ge (g, x - x_0) \quad \text{for all } x \in E_n.$$

Every convex $f$ has at least one subgradient at every point. Let $M^* = \{x : f(x) \le f(y) \ \forall y\}$ be the set of minimum points and, when it is nonempty, $f^* = \min f$.

A subgradient selection $g_f$ assigns to each $x$ some subgradient $g_f(x)$ of $f$ at $x$. No particular choice is made: every result holds for every selection. Given stepsizes $h_1, h_2, \dots > 0$ and a starting point $x_0$, the normalized subgradient method is

$$x_{k+1} = x_k - h_{k+1}\, \frac{g_f(x_k)}{\|g_f(x_k)\|}, \qquad k = 0, 1, \dots \tag{2.4}$$

If $g_f(x_k) = 0$, then $x_k$ is a minimizer and the computation stops. The unnormalized method is $x_{k+1} = x_k - h_{k+1} g_f(x_k)$ (2.5), and the method with restarts takes that step when $h_{k+1}\|g_f(x_k)\| \le c$ and returns to $x_0$ otherwise.

Formalization targets

Goal: Theorem 2.2 (p. 25)

If $M^*$ is nonempty and bounded, $h_k > 0$, $h_k \to 0$ and $\sum_{k \ge 1} h_k = +\infty$, then for every $x_0$ and every subgradient selection, the method (2.4) either reaches $M^*$ at some index $\bar k$ or

$$\lim_{k \to \infty} \min_{y \in M^*} \|x_k - y\| = 0, \qquad \lim_{k \to \infty} f(x_k) = f^*.$$

Milestones

1. Eq. (2.3), the one-step inequality $\|x_{k+1} - x^*\|^2 \le \|x_k - x^*\|^2 + h^2 - 2h\,\rho(x^*, U_k)$, where $U_k = \{x : f(x) = f(x_k)\}$.
2. Theorem 2.1: with constant step length $h$, some level surface $\{f = f(x_{k^*})\}$ passes within $h(1+\varepsilon)/2$ of any $x^* \in M^*$.
3. Corollaries 1 and 2: a suitable constant step length yields a subsequence with $f(x_{k_i}) - f^* < \delta$. If $M^*$ contains a ball of radius $r > h/2$, the method terminates in $M^*$.
4. Theorem 2.5: if $M^*$ contains a ball of radius $r$, $\sum h_k = \infty$ and $\limsup h_k < 2r$, then (2.4) terminates in $M^*$.
5. Theorem 2.3: for the unnormalized method (2.5), bounded subgradients along the trajectory imply convergence, and unbounded subgradients rule it out.
6. Theorem 2.4: the method with restarts converges for every $c > 0$.

Significance

Theorem 2.2 is the basic convergence guarantee for first-order methods on general nonsmooth convex functions. It needs no Lipschitz constant, no bound on the subgradients and no smoothness: normalizing the step makes the step length independent of the size of the subgradient. The divergent-series rule $h_k \to 0$, $\sum h_k = \infty$ is the standard stepsize condition of stochastic approximation and of Lagrangian relaxation codes. Theorems 2.3–2.5 mark its boundaries. The unnormalized method needs bounded subgradients (Theorem 2.3), restarts remove that need (Theorem 2.4), and a solution set with nonempty interior gives finite termination (Theorem 2.5). The last result is the basis of the finite methods for systems of convex inequalities and for the dual of an assignment problem with a unique solution (pp. 28–29).

All of these results are classical and proved in the source. None of them is formalized in Lean's Mathlib. The platform has neighbouring results that are not the same statements: Poljak's divergent-series theorem for concave piecewise-linear maximization (in Validation of Subgradient Optimization I), and rate bounds for Lipschitz objectives (First-Order and Stochastic Optimization Methods for ML II, Understanding Machine Learning X). This mission adds the general convex case with normalized steps, the dichotomy for unnormalized steps, and finite termination.

Difficulty

The standard rate analysis of the subgradient method bounds $\|x_{k+1} - x^*\|^2 - \|x_k - x^*\|^2$ by $-2h_{k+1}(f(x_k) - f^*)/\|g_f(x_k)\| + h_{k+1}^2$. It then needs a uniform bound on $\|g_f(x_k)\|$, which is exactly what is not assumed here. Nothing a priori keeps the iterates in a bounded set, and the subgradients of a general convex function (for instance $f(x) = x^4$, the source's example on p. 26) grow without bound away from $M^*$; with unnormalized steps this makes the method diverge. Even with normalized steps, the distance to a minimizer decreases only outside a neighbourhood of $M^*$ whose size is of the order of the current step, so a monotone decrease argument gives at best a subsequence with small function values. Convergence of the whole sequence $\min_{y \in M^*}\|x_k - y\|$ to zero is a stronger statement, and boundedness of $M^*$ is essential to it.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $f$ is real-valued (finite everywhere) with ConvexOn ℝ Set.univ f.
• The subgradient selection g is arbitrary, with the hypothesis ∀ x, IsSubgradient f x (g x). The starting point is arbitrary.
• The iterations are defined recursively (normalizedIter, plainIter, resetIter); the stepsize sequence is h : ℕ → ℝ with h (k+1) used at step $k$. In (2.4), a zero subgradient is handled by an explicit branch that repeats the current iterate (which is then in $M^*$). No statement relies on Lean's convention $x/0 = 0$.
• $M^*$ is required to be nonempty wherever the book writes $\min_{y \in M^*}$ or $f^* = \min f$. $\min_{y \in M^*}\|x_k - y\|$ is Metric.infDist, and $f^*$ is ⨅ y, f y.
• $\sum_{k \ge 1} h_k = +\infty$ is Tendsto (fun N => ∑ k ∈ Finset.range N, h (k+1)) atTop atTop. $\limsup h_k < 2r$ is "for some $q < 2r$, eventually $h_k \le q$", so it cannot hold vacuously for an unbounded sequence.
• Corollary 1's step length $h_\delta$ is quantified before the selection and the starting point: it depends only on $f$ and $\delta$.
• Theorem 2.3 is stated as two implications, (bounded subgradients ⇒ convergence) and (unbounded ⇒ no convergence), not as a disjunction that one case could satisfy trivially.
• A formalization of Theorem 2.2 that assumes bounded subgradients, a Lipschitz $f$, or a specific subgradient choice (such as the minimal-norm one) proves a different and weaker theorem, and does not close the goal.

Needed infrastructure: continuity of convex functions on $E_n$ (in Mathlib), compactness of sublevel sets when $M^*$ is bounded, and the geometry of level surfaces relative to supporting hyperplanes. The one-step inequality (2.3) and the level-set compactness lemma are reusable by the later missions of this series (linear rate, Polyak's stepsize, stochastic subgradient). Contributions that prove Eq. (2.3) or Theorem 2.1 first are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985, Chapter 2, pp. 22–30. https://doi.org/10.1007/978-3-642-82118-9
• B. T. Polyak, A general method for solving extremal problems, Doklady Akademii Nauk SSSR 174 (1967), 33–36 (the source's reference [64]).
• Yu. M. Ermoliev, Methods for solving nonlinear extremal problems, Kibernetika (Kiev), no. 4 (1966), 1–17 (the source's reference [24]).
• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974), 62–88. https://doi.org/10.1007/BF01580223

Motivation

Gradient methods assume a continuous gradient; subgradient methods assume convexity. Many objective functions met in practice satisfy neither. Shor's example is economic planning, where components of the objective are piecewise-smooth, not necessarily convex functions of a parameter describing the productivity of a unit, and where minimax formulations produce kinks as a rule (Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, §1.4, p. 17, DOI 10.1007/978-3-642-82118-9). Such problems need a class of functions wide enough to contain piecewise-smooth and minimax functions and narrow enough to carry a usable replacement for the gradient.

Shor's answer is the class of almost differentiable functions, introduced in his 1972 work and presented in §1.4 of the book, together with the almost-gradient, a limit of gradients taken at nearby points of differentiability. The capstone of the section, Theorem 1.15, connects this class with convex analysis: every convex function on $E_n$ is almost differentiable, and its almost-gradients are subgradients. This is what lets the later chapters treat convex minimization and almost-differentiable minimization with one set of tools. Clarke's generalized gradient of locally Lipschitz functions (Clarke 1975) is the closest relative; Shor's definition differs in requiring the gradient to be continuous on its domain (p. 19).

Setting

Let $E_n$ denote $n$-dimensional Euclidean space with inner product $(x, y)$ and norm $\|x\|$. For $f : E_n \to \mathbb{R}$, write $M = \{x \in E_n : f \text{ is differentiable at } x\}$ and $\nabla f(x)$ for the gradient at $x \in M$.

A function $f$ is almost differentiable if

1. on every bounded set $S$ it is Lipschitz: $|f(x) - f(y)| \le L_S \|x - y\|$ for $x, y \in S$, with a constant $L_S$ depending on $S$;
2. it is differentiable at Lebesgue-almost every point of $E_n$;
3. the map $x \mapsto \nabla f(x)$, restricted to $M$, is continuous.

An almost-gradient of $f$ at $x_0$ is a vector $g$ that is an accumulation point of a sequence $\nabla f(x_1), \nabla f(x_2), \dots$ with $x_k \in M$ and $x_k \to x_0$. The set of almost-gradients is $G(x_0)$. A generalized almost-gradient is a point of the closure of the convex hull of $G(x_0)$.

A vector $g$ is a subgradient of $f$ at $x_0$ if $f(x) - f(x_0) \ge (g, x - x_0)$ for all $x \in E_n$; for convex $f$ the set of subgradients is the subdifferential $G_f(x_0)$.

In Lean these objects are AlmostDifferentiable f, almostGradients f x₀ and IsSubgradient f x₀ g in the namespace ShorNonsmooth.AlmostDiff, with $E_n$ = EuclideanSpace ℝ (Fin n).

Formalization targets

Goal: Theorem 1.15 (p. 18)

For convex $f : E_n \to \mathbb{R}$,

$$f \text{ is almost differentiable} \quad\text{and}\quad G(x_0) \subseteq G_f(x_0) \ \text{ for every } x_0 \in E_n .$$

The printed statement says the almost-gradients "coincide with" the subgradients. As a set equality this is false (for $f(x) = |x|$ on $E_1$, $G(0) = \{-1, 1\}$ while $G_f(0) = [-1, 1]$), and the book's proof establishes the inclusion. The goal is the inclusion.

Milestones

1. Proof of Theorem 1.15, display (p. 18). For convex $f$ differentiable at $x_k$: $f(x) - f(x_k) \ge (\nabla f(x_k), x - x_k)$ for all $x$.
2. Proof of Theorem 1.15 (p. 18). For convex $f$ and bounded $S$ there is $C$ with $|f'_v(x)| \le C\|v\|$ for all $x \in S$ and all $v$, the one-sided directional derivatives existing.
3. Proof of Theorem 1.15 (p. 18). A convex $f$ is differentiable almost everywhere and $\nabla f$ is continuous on $M$.
4. Theorem 1.14 (p. 18). For almost differentiable $f$, $G(x)$ is nonempty, bounded and closed at every $x$.
5. p. 19. For almost differentiable $f$, $\overline{\operatorname{conv}}\, G(x)$ is convex, bounded and closed.

Significance

The result. Theorem 1.15 embeds convex functions into the almost differentiable class and identifies each almost-gradient of a convex function as a subgradient. Consequently any method that only needs almost-gradients (limits of gradients at nearby differentiable points, which is what a numerical procedure can actually compute) produces valid subgradients when applied to a convex function. Theorem 1.14 supplies the compactness that makes $G(x)$ usable as a set-valued substitute for the gradient.

Formalizing it. All results here are classical and proved on paper. Mathlib contains Rademacher's theorem for Lipschitz functions (LipschitzWith.ae_differentiableAt) and local Lipschitz continuity of convex functions on open sets; it does not contain the continuity of the gradient of a convex function on its domain of differentiability, nor any notion of almost-gradient. The mission produces those, together with a formal record that the printed "coincide" is an inclusion. A formal proof of the true equality $G_f(x_0) = \overline{\operatorname{conv}}\, G(x_0)$ would be a welcome further contribution.

Difficulty

Two parts of the goal carry real content. The first is condition (c): the gradient of a convex function, restricted to the set where it exists, is continuous. The book cites this from the literature; it is not a consequence of Rademacher's theorem, which gives differentiability almost everywhere and says nothing about how gradients at nearby points relate. The second is condition (b) in a form Lean accepts: Rademacher's theorem in Mathlib is stated for globally Lipschitz functions, while a convex function on $E_n$ is only Lipschitz on bounded sets, so the almost-everywhere statement has to be assembled from local pieces. The passage from gradients to subgradients in the second conjunct is comparatively routine.

The analogous closure properties claimed on the same pages for sums, products and maxima of almost differentiable functions (Theorems 1.16 and 1.17) are false as printed and are not targets; see the formalization scope.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n); $n = 0$ is allowed and harmless. Functions are total and real-valued; convexity is ConvexOn ℝ Set.univ f.
• The gradient is Mathlib's gradient f x; condition (c) is ContinuousOn (gradient f) {x | DifferentiableAt ℝ f x}, continuity of the restriction in the subspace topology.
• Condition (a) is quantified over every bounded set with a set-dependent constant: ∀ S, Bornology.IsBounded S → ∃ L, LipschitzOnWith L f S. Condition (b) is ∀ᵐ x ∂volume, DifferentiableAt ℝ f x.
• An almost-gradient is a cluster point (MapClusterPt) of the gradient sequence, not its limit; the points $x_k$ may equal $x_0$.
• Subgradients are taken relative to the whole space, the domain of every function in this mission.
• The goal states the inclusion $G(x_0) \subseteq G_f(x_0)$ proved in the book. Stating the printed set equality would make the goal false; weakening the first conjunct to "locally Lipschitz and differentiable almost everywhere" would drop condition (c) and with it the substance of the theorem. Neither is acceptable.
• Theorem 1.16 (sums, differences, products) and Theorem 1.17 (maxima) are omitted: both are false for the class as defined. With $h(x) = x^2 \sin(1/x)$, the functions $h + |x|$ and $-|x|$ are almost differentiable but their sum $h$ is differentiable everywhere with a derivative discontinuous at $0$; and $\max(h - |x|,\, h - |x| + 2x) = h + x$. Theorem 1.18 (Mifflin's superposition theorem for semismooth functions) is cited from the literature without proof and rests on Clarke's generalized gradient; it is outside this mission.

Infrastructure that is reusable beyond this mission: continuity of the gradient of a convex function on its domain; Rademacher's theorem for locally Lipschitz functions on $E_n$; the almost-gradient set and its compactness. Contributions that prove these as standalone lemmas are welcome.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer, 1985. https://doi.org/10.1007/978-3-642-82118-9
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, Theorem 25.5 (continuity of the gradient of a convex function). https://doi.org/10.1515/9781400873173
• F. H. Clarke, Generalized gradients and applications, Transactions of the American Mathematical Society 205 (1975), 247–262. https://doi.org/10.1090/S0002-9947-1975-0367131-6
• H. Rademacher, Über partielle und totale Differenzierbarkeit von Funktionen mehrerer Variabeln und über die Transformation der Doppelintegrale, Mathematische Annalen 79 (1919), 340–359. https://doi.org/10.1007/BF01498415

Motivation

Military and commercial service parts systems keep repairable parts at a central depot warehouse and at a set of operating bases. Chapter 10 of Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) turns from the planning models of the earlier chapters to execution. Each period, the stock that is at the depot or arriving there must be divided among the bases. The planner knows what is already in the pipeline and faces random demand at each base. The chapter's models are solved in a rolling-horizon manner. Each period's decisions are the first step of an optimal plan over a short horizon. That plan has to be computable at scale, for thousands of items and dozens of bases.

What makes this possible is a structural fact. In an optimal allocation, the cumulative stock sent to a base never exceeds what a single-period newsvendor problem at that base would ask for. This bound shrinks the allocation integer programs to linear programs of manageable size. This mission formalizes that bound and the facts it rests on.

Setting

Fix one item. Time is counted in whole periods $t = 0, 1, 2, \dots$, and $J$ is the finite set of bases. For each base $j$:

• $T_{i0}$ is the repair lead time, so shipments are decided in periods $t = 0, \dots, T_{i0}$;
• $T^r_{ij}$ and $T^e_{ij}$ are the regular and expedited transportation times from the depot to base $j$, integers with $1 \le T^e_{ij} < T^r_{ij}$;
• $\tilde S_{i0t}$ is the known cumulative supply at the depot through period $t$ (stock on hand plus arrivals already in the pipeline), and $\tilde S_{ijt}$ the known cumulative supply at base $j$. The latter is constant for $t \ge T^r_{ij}$, since nothing not yet shipped can arrive earlier than $T^r_{ij}$ by regular transport;
• $X_{ijt}$ is the cumulative demand at base $j$ through period $t$, a nonnegative integer random variable, nondecreasing in $t$, with finite mean;
• $h_{ij} > 0$, $b_{ij} > 0$ and $e_{ij} \ge 0$ are the incremental holding, shortage and expediting costs.

If $S_{ijt}$ units have arrived at base $j$ by period $t$, the expected cost of that period is

$$G_{ijt}(S) = h_{ij}\,E[S - X_{ijt}]^+ + b_{ij}\,E[X_{ijt} - S]^+,$$

and stock left at the end of the horizon costs

$$Q_{ij}(S) = h_{ij}\sum_{t > T^r_{ij} + T_{i0}} E[S - X_{ijt}]^+ .$$

The stock allocation model $\mathrm{SAM}_i$ chooses nonnegative integer regular shipments $y^r_{ijt}$, $t = 0, \dots, T_{i0}$, with cumulative shipments never exceeding cumulative depot supply. The cumulative stock at base $j$ is $S_{ijt} = \tilde S_{ij(T^r_{ij}-1)} + \sum_{t' \le t - T^r_{ij}} y^r_{ijt'}$, and the model minimizes $\sum_j \{\sum_{t=T^r_{ij}}^{T^r_{ij}+T_{i0}} G_{ijt}(S_{ijt}) + Q_{ij}(S_{ij(T^r_{ij}+T_{i0})})\}$. The extended model $\mathrm{ESAM}_i$ adds expedited shipments $y^e_{ijt}$, which arrive after $T^e_{ij}$ periods at an extra cost $e_{ij}$ per unit.

The constrained newsvendor problem $\mathrm{CN}_{ijt}$ minimizes $G_{ijt}(S)$ over integers $S \ge \tilde S_{ijt}$. Its largest optimal solution is written $\hat S_{ijt}$.

Formalization targets

Goal: Theorem 15 (p. 237)

In every optimal solution of $\mathrm{SAM}_i$, for every base $j$ and every $t \in [T^r_{ij}, T^r_{ij} + T_{i0}]$,

$$\tilde S_{ij(T^r_{ij}-1)} \;\le\; S^*_{ijt} \;\le\; \hat S_{ijt}.$$

The bound is uniform over optimal solutions and uses nothing but the single-period problems.

Milestones

1. Separability (Section 10.4.1, p. 236). The multi-item problem $\mathrm{SAM}$ splits into the $\mathrm{SAM}_i$: its optimal solutions are exactly the tuples of optimal item solutions, and $Z^* = \sum_i Z^*_i$.
2. Convexity of $Q_{ij}$ (p. 234) and of $G_{ijt}$ (p. 237), in the discrete sense of nondecreasing first differences on $\mathbb Z$.
3. The newsvendor solution (10.19). $\hat S_{ijt} = \max(\tilde S_{ijt}, s^0)$ with $s^0$ the least integer such that $P(X_{ijt} \le s^0) > b_{ij}/(b_{ij}+h_{ij})$.
4. Monotonicity (10.20). $\hat S_{ij(t-1)} \le \hat S_{ijt}$ on $[T^r_{ij}, T^r_{ij} + T_{i0}]$.
5. Theorem 16, corrected (p. 244). In every optimal solution of $\mathrm{ESAM}_i$, $\tilde S_{ijt} \le S^*_{ijt}$. Writing $M_{jt} = \max_{k \in [T^e_{ij}, t]}(\hat S_{ijk} - \tilde S_{ijk})$, also $S^*_{ijt} \le \tilde S_{ijt} + M_{jt}$, provided $T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$.

Two supporting items state that $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ have optimal solutions. A third, theorem16_counterexample, exhibits an instance in which Theorem 16's upper bound, as printed, fails.

Significance

Theorem 15 is what allows the book (pp. 238–239) to rewrite $\mathrm{SAM}_i$ with 0–1 variables $\delta_{ijtk}$ indicating $S_{ijt} = k$. Only $k$ between $\tilde S_{ij(T^r_{ij}-1)}$ and $\hat S_{ijt}$ is needed, so the number of variables is governed by the newsvendor quantities rather than by the total depot supply. Theorem 16 plays the same role for the model with expediting. Both bounds also justify the greedy heuristics of Sections 10.4.3 and 10.5.3. Those heuristics never raise a base's stock above its newsvendor level.

The book proves both theorems in half a page each by an exchange argument. This mission produces machine-checked versions and, in doing so, settles the exact scope of Theorem 16. As printed it is false. With $T^r_{ij} \ge T^e_{ij} + 2$, an expedited shipment in the last decision period can be the only way to cover a later period's demand, and the optimal plan then overstocks an earlier period. The mission states the corrected theorem and the counterexample; the counterexample was checked in Lean during drafting. None of the chapter's results has been formalized before, as far as the platform's catalogue shows.

Difficulty

The central step is the exchange. Take the first period $k$ in which an optimal plan overshoots its bound, and delay by one period one unit that arrives at $k$. This must be shown feasible, to change only $S_{ijk}$, and to lower the objective strictly. That in turn needs strict decrease of a convex function to the right of its largest minimizer, and an argument for the last period, where there is no later period to delay into. The indexing is heavy: two lead times, truncated sums $\min(t - T^e_{ij}, T_{i0})$, and cumulative constraints across bases.

The first idea, that a plan above the newsvendor level can always be improved by shipping less, fails. Shipping less changes the stock in every later period too, and later periods may need the unit. The bound follows only from a delay that affects exactly one period. For $\mathrm{ESAM}_i$ even such a delay is sometimes unavailable, which is where the book's Theorem 16 breaks.

Formalization scope

• One item at a time: ItemModel J Ω P bundles the data of one item with the cumulative demands on a probability space $(\Omega, P)$, [IsProbabilityMeasure P]. Bases form a Fintype. Periods are ℕ. Stock levels and supplies are ℤ, since net inventory may be negative. Shipments are functions J → ℕ → ℕ, so nonnegativity and integrality are built in. Costs are in ℝ.
• $G$ and $Q$ are defined from the demand as in the book: Bochner integrals of $(S - X)^+$ and $(X - S)^+$, and a tsum for $Q$. The item model requires finite means and convergence of the series for $Q$ at every stock level, so that no integral or sum takes Lean's junk value $0$.
• "The largest optimal solution" is the predicate IsLargestCNSolution (feasible, minimizing, and above every feasible minimizer). Theorems take $\hat S$ as a function satisfying it. Milestone (10.19) shows it exists.
• "An optimal solution" means a feasible plan with objective at most that of every feasible plan. The theorems hold for every optimal plan.
• Pinned conventions and additions. The following are not written in the book: $h_{ij}, b_{ij} > 0$ and $e_{ij} \ge 0$; nonnegative, nondecreasing depot supply; nondecreasing base supply (used in the book's proof of Theorem 16); finite mean demand; convergence of $Q$'s series. (10.19) is read with the critical fractile "least $s$ with $F(s) > b/(b+h)$", the book's $\lceil F^{-1}\rceil$/$\lfloor F^{-1}\rfloor$ with ties broken upward. Theorem 16 carries the proviso "$T^r_{ij} = T^e_{ij} + 1$ or $t < T^e_{ij} + T_{i0}$". Separability is stated both for optimal plans and for optimal values.
• Ruled out. The feasible sets of $\mathrm{SAM}_i$ and $\mathrm{ESAM}_i$ impose no upper bound on the cumulative stock, and $\hat S$ is defined from $G$ alone, never from the allocation problem. The bounds are therefore not true by definition.
• Omitted. The LP reformulations (10.22)–(10.28) and (10.45)–(10.52) and the integrality of their relaxations, which the book asserts with a reference to [68]; the greedy algorithms and their optimality conditions (asserted); the book's claim that $Q_{ij}$ is strictly increasing (p. 238), which fails when $P(X_{ijt} \le S) = 0$ beyond the horizon and is not needed; the dynamic program of Section 10.3 and the repair model of Section 10.6.
• The discrete-convexity and newsvendor facts are reusable for any single-location inventory model on $\mathbb Z$. Contributions are welcome on the convexity lemmas, the critical-fractile characterization, and a reusable exchange lemma for cumulative-shipment models.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005, Chapter 10, pp. 225–246. DOI 10.1007/b138879
• K. J. Arrow, T. Harris, J. Marschak, "Optimal inventory policy", Econometrica 19(3), 1951, 250–272 (the newsvendor critical fractile). DOI 10.2307/1906813

Motivation

Service parts networks (spare parts for aircraft, military systems, industrial equipment) hold stock at several echelons: a depot, intermediate stocking facilities, and bases or warehouses that face demand. Two questions recur in their planning. First, how should a given amount of stock be split among locations whose expected costs are convex in the stock they hold? Second, does adding an echelon, a depot that pools the demand of several warehouses, raise or lower the stock the system needs?

Chapter 7 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879), treats both. For the second it follows Eppen and Schrage (1981, reference [78] of the book): with normal demands, a depot that places orders every period and allocates stock so that all warehouses face the same stockout probability reduces the choice of system stock to a single critical-fractile equation. For the first, the chapter's multi-echelon pooling model (Section 7.3) evaluates nested cost functions of the form "holding and shortage cost plus the minimum over allocations of a sum of convex costs", and its appendix (Section 7.4) gives the marginal allocation algorithm AllocOpt that computes these minima exactly for every stock level at once.

Marginal analysis for separable convex resource allocation is classical (Fox, Management Science, 1966); the monograph of Ibaraki and Katoh (MIT Press, 1988) surveys it.

Setting

Allocation data (Section 7.4). There is a set $M = \{1, \dots, \bar M\}$ of locations and an augmented set $M_0 = \{0\} \cup M$. Each location $m \in M_0$ has integer gridpoints $0 = r^m_0 < r^m_1 < \dots < r^m_{n(m)}$. For $m \in M$, the value $c^m_n$ of a convex function is given at each gridpoint. The slopes (7.19) are $\hat c^m_n = (c^m_{n+1} - c^m_n)/(r^m_{n+1} - r^m_n)$ for $n < n(m)$, and $\hat c^m_{n(m)}$ repeats the last one. The piecewise linear approximation $\tilde C_m$ of (7.20)–(7.21) interpolates the values $c^m_n$ at the gridpoints and continues with slope $\hat c^m_{n(m)}$ beyond the last one. A convex function $f$ on $\mathbb R_+$ is also given.

The allocation optimization (7.22) asks, for each $n \in N_0 = \{0, \dots, n(0)\}$, for

$$c^0_n = f(r^0_n) + \min\Bigl\{ \sum_{m \in M} \tilde C_m(r_m) : r_m \ge 0 \text{ integer},\ \sum_{m \in M} r_m = r^0_n \Bigr\}.$$

Algorithm AllocOpt (Definition 4) keeps a current gridpoint index $n^*(m)$ and allocation $r^*(m)$ per location. For each increment $r^0_n - r^0_{n-1}$ of the target, it repeatedly gives units to a location $m^*$ whose current slope $\hat c^{m^*}_{n^*(m^*)}$ is minimal, up to that location's next gridpoint, and records the accumulated cost.

Pooling system (Section 7.2.1). One depot supplies $m$ warehouses. The demand $d_{jt}$ at warehouse $j$ in period $t$ is normal with mean $\mu_j$ and variance $\sigma_j^2$, independent across periods and warehouses. The supplier-to-depot lead time is $D$ periods, the depot-to-warehouse lead time $A$ periods, and holding and backorder costs $h, b$ are equal at all warehouses. Positions $I_j$ are in balance when $\Phi((I_j - A\mu_j)/(\sqrt A\,\sigma_j))$ is the same for all $j$. For system inventory position $s$, with $Y_0$ the system demand over $D$ periods and $Y_j$ the demand at $j$ over the next $A + 1$ periods, the balanced allocation gives each warehouse a share proportional to $\sigma_j$, and $z_j$ is its end-of-period net inventory.

Formalization targets

Goal: Proposition 2 (correctness)

For every tie-breaking rule in its arg min steps, AllocOpt returns values $c^0_n$ that satisfy (7.22) for every $n \in N_0$: some feasible integer allocation attains $c^0_n - f(r^0_n)$, and no feasible integer allocation does better.

Milestones

1. Slope monotonicity (p. 178): $\hat c^m_n \ge \hat c^m_{n-1}$ for $0 < n \le n(m)$.
2. Convexity of $\tilde C_m$ on $[0, \infty)$ (proof of Proposition 2, p. 179).
3. Remark 2 (p. 179): with the inner loop run only while the current slope is $\le 0$, AllocOpt solves (7.22) with $\sum_m r_m \le r^0_n$.
4. Lemma 3 (p. 152): if the positions are in balance and

$$\sum_{j} d_{j,t-1} \ge \max_{i} \Bigl\{ \sum_{j \ne i} d_{j,t+D-1} + d_{i,t+D-1}\Bigl(1 - \frac{\sum_j \sigma_j}{\sigma_i}\Bigr)\Bigr\},$$

then a nonnegative allocation of the arriving $\sum_j d_{j,t-1}$ units restores balance. 5. Net inventory law (pp. 156–157): $z_j$ is normal with mean $(s - (D + A + 1)\sum_i \mu_i)\,\sigma_j / \sum_i \sigma_i$ and variance $(A + 1)\sigma_j^2 + (\sigma_j / \sum_i \sigma_i)^2 D \sum_i \sigma_i^2$. 6. Critical fractile (pp. 157–158): $s$ minimizes $\sum_j E[h (z_j)^+ + b (z_j)^-]$ if and only if $\Phi(z) = b/(b+h)$, where

$$z = \frac{s - (D + A + 1)\sum_i \mu_i}{\bigl[(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2\bigr]^{1/2}}.$$

Significance

The goal certifies an algorithm that the chapter uses as a subroutine three times: in the pool cost (7.14), the subsystem cost (7.15) and the system cost (7.17), and hence in the claim of Section 7.3 that the system-wide cost function can be computed in time $n \log n$ in the number of locations. Because AllocOpt produces the whole vector $(c^0_n)_{n \in N_0}$ in one pass, its correctness gives the nested value functions at every gridpoint of the next echelon, which is what allows the recursion up the echelons. The Eppen–Schrage milestones give the classical quantitative form of risk pooling: the system stock is set by one critical fractile, and the standard deviation term $(A + 1)(\sum_i \sigma_i)^2 + D \sum_i \sigma_i^2$ is what the book compares with the single-warehouse and the decentralized systems.

On formalization: the book states Proposition 2 with a two-sentence argument and Remark 2 without proof. The Eppen–Schrage computations are displayed derivations. None of these results has a machine-checked proof on the platform. A verified AllocOpt, stated for an explicit algorithm rather than for an abstract greedy procedure, is reusable for any separable convex integer allocation with a sum constraint.

Difficulty

The usual greedy exchange argument assumes that units are allocated one at a time. AllocOpt allocates in blocks, up to the next gridpoint of the chosen location, and it carries its state across successive targets $r^0_{n-1} \to r^0_n$ without restarting. The proof must therefore show that the state after each outer step is itself an optimal allocation for the current target, and that block moves never step past a breakpoint where the arg min would change. The slopes can be negative, and the equality constraint forces allocation even when every marginal cost is positive. Remark 2 needs an additional argument: under the inequality constraint the loop may stop before $u$ reaches zero, and that point is optimal only because the slopes are nondecreasing.

For the pooling results, the balanced allocation mixes the depot-lead-time demand $Y_0$ of all warehouses with the local demand $Y_j$, and the Gaussian law of $z_j$ rests on the independence of disjoint blocks of periods. The fractile statement requires strict monotonicity of each warehouse's expected cost derivative in $s$, not only a first-order condition.

Formalization scope

• Indices and types. Locations of $M$ are Fin Mbar; gridpoints are integers, values and slopes real numbers; allocations are functions Fin Mbar → ℕ. The standing assumptions of Section 7.4 form the predicate WellFormed: $\bar M \ge 1$, $n(m) \ge 1$ for $m \in M$ (a slope (7.19) needs two gridpoints), gridpoints starting at $0$ and strictly increasing at every location of $M_0$, each $c^m_n$ the value of a function convex on $[0, \infty)$, and $f$ convex on $[0, \infty)$.
• The minimum in (7.22) is stated as attainment plus a lower bound over the finite, nonempty set of feasible integer allocations, never as an unconstrained infimum.
• Ties. The book's arg min fixes no tie-breaking rule. Results are stated for every selection rule that returns a minimizing location.
• Termination. AllocOpt is a total Lean function. The inner loop is given more passes than it can use, so it always exits through its own condition.
• Not stated. The operation count of Proposition 2, $O((1 + \log_2 \bar M)\sum_{m \in M_0} n(m))$, and Proposition 1 and Remark 1 (p. 177) are operation counts with no machine model and are left out.
• Corrections. The first expected-cost display on p. 157 has $+\,b\int_{-\infty}^0 z\,dF_{z_j}(z)$, which is negative. The formalization uses $b\,E[(z_j)^-]$, as in the book's next display.
• Pinnings. Lemma 3 is deterministic: the demands are arbitrary reals, and "in balance following the allocation" means that some $x_j \ge 0$ with $\sum_j x_j = \sum_j d_{j,t-1}$ exists. The critical-fractile milestone is the characterization "minimizer if and only if $\Phi(z) = b/(b+h)$" of the book's "can be found by setting".
• Trivialization ruled out. The allocation problem (7.22) is defined independently of the algorithm, as a minimum over explicit integer allocations, and the $\tilde C_m$ are built from the data by (7.19)–(7.21). Neither (7.22) nor the $\tilde C_m$ are defined as, or required to agree with, what AllocOpt returns.
• Welcome contributions. Lemmas on the invariants of AllocOpt, in particular that after each outer step the allocation $r^*$ is feasible for $r^0_n$ with cost $z$ and all slopes to the left of $n^*(m)$ are at most those to the right. Also Gaussian sum lemmas over finite index sets and a general newsvendor first-order characterization.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, Springer, 2005. DOI 10.1007/b138879
• G. D. Eppen and L. Schrage, "Centralized ordering policies in a multi-warehouse system with lead times and random demand", in L. B. Schwarz (ed.), Multi-Level Production/Inventory Control Systems: Theory and Practice, Studies in the Management Sciences, North-Holland, Amsterdam, 1981, pp. 51–67.
• G. D. Eppen, "Effects of centralization on expected costs in a multi-location newsboy problem", Management Science 25(5), 1979, 498–501. DOI 10.1287/mnsc.25.5.498
• B. Fox, "Discrete optimization via marginal analysis", Management Science 13(3), 1966, 210–216. DOI 10.1287/mnsc.13.3.210
• T. Ibaraki and N. Katoh, Resource Allocation Problems: Algorithmic Approaches, MIT Press, 1988.

Motivation

A stocking point that reviews its inventory once per period and must decide how much to order is the basic unit of every service parts supply chain: each warehouse, each repair depot and each forward location in the networks studied later in Muckstadt's Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) faces this decision for thousands of items. The practical rule used everywhere is the order-up-to (base-stock) rule: bring the inventory position up to a fixed target level whenever it falls below it, and order nothing otherwise. Chapter 2 of the book justifies this rule for a single item with linear costs, following the dynamic-programming argument of Karlin and Scarf, and the rest of the book takes the rule as given.

Timeline. Arrow, Harris and Marschak posed the periodic-review inventory problem as a dynamic program in 1951 (Econometrica). Bellman, Glicksberg and Gross showed in 1955 that with linear ordering cost and convex expected holding and shortage costs the optimal policy has a critical-number form (Management Science). Karlin and Scarf (1958) extended the analysis to a positive lead time, the setting of the book's Theorems 1–3. Veinott (1965) gave conditions under which a base-stock policy is optimal in multi-product, nonstationary models (Management Science).

Setting

One item is stocked at one location. At the start of each period the inventory position $y$ is observed and a quantity $u \ge 0$ is ordered; with lead time one period it arrives at the start of the next period. Demand in each period is independent of other periods and has a density $g$ on $(0,\infty)$ that is positive and continuous. Unmet demand is backordered. Costs are linear: $c$ per unit ordered, $h$ per unit on hand at the end of a period, $b$ per unit backordered at the end of a period, and future costs are discounted by $\alpha \in (0,1)$. The one-period cost is

$$L(y) = \begin{cases} h\displaystyle\int_0^y (y-x)g(x)\,dx + b\int_y^\infty (x-y)g(x)\,dx, & y > 0,\\[1mm] b\displaystyle\int_0^\infty (x-y)g(x)\,dx, & y \le 0. \end{cases}$$

The book assumes throughout that $b > \frac{1-\alpha}{\alpha}\,c$: the backorder cost outweighs the saving from deferring a purchase.

The $n$-period value functions are $f_1 = L$ and, for $n \ge 2$,

$$f_n(y) = \min_{u \ge 0}\Big\{ c\,u + L(y) + \alpha\int_0^\infty f_{n-1}(y+u-x)\,g(x)\,dx \Big\}.$$

An order $u$ is optimal at $y$ if it attains this minimum over all $u \ge 0$. The order-up-to rule with level $s$ orders $u(y) = \max\{0, s-y\}$. The marginal function of eq. (2.8) is $F_n(w) = c + \alpha\int_0^\infty f_n'(w-x)\,g(x)\,dx$. In Lean these are Model, Model.L, Model.f, Model.IsOptimalOrder, Model.IsOrderUpToOptimal and Model.F in the namespace ServiceParts.BaseStock.

Formalization targets

Goal: Theorem 2 (p. 18) in its $n$-period form

For every horizon $n \ge 2$, either there is a real level $s_n^*$ with

$$u_n^*(y) = \max\{0,\ s_n^* - y\} \ \text{optimal for every } y,$$

or ordering nothing is optimal for every $y$ (level $-\infty$); and there is $N \ge 2$ such that the level is real for all $n \ge N$. No value of $s_n^*$ is fixed: the goal asserts the shape of the optimal policy only.

Milestones, in attack order

1. $L$ is convex (p. 21).
2. Every $f_n$, $n \ge 1$, is convex (p. 19, property (c)).
3. Every $f_n$ is differentiable with $-(c+b) \le f_n' \le h/(1-\alpha)$ (p. 20).
4. Property (b): given an optimal real level $s$ for horizon $n \ge 2$, $f_n' = -c + L'$ below $s$ and $f_n' = L' + \alpha\int_0^\infty f_{n-1}'(\cdot - x)g(x)\,dx$ from $s$ on (p. 19).
5. Given such a level, $F_n(w) \to (1-\alpha)c - b\alpha < 0$ as $w \to -\infty$ (p. 19).
6. Property (a): optimal real levels are nondecreasing in the horizon, $s_n^* \le s_{n+1}^*$ (p. 18).

Significance

The theorem reduces an infinite-dimensional control problem, a choice of order quantity for every possible inventory position, to one number per period. Every later chapter of the book (Palm's theorem for $(s-1,s)$ policies, METRIC-type stock level optimization, allocation in multi-echelon systems) parameterizes policies by such stock levels; this is where the book justifies that parameterization.

The result is classical and proved in many texts. On Prove2Me the mission produces a machine-checked finite-horizon version with a continuous demand density, including the calculus the proof needs: convexity of an expected cost defined by integrals against a density, differentiation under the integral sign in the recursion, and the one-sided behaviour of the value function at the order-up-to level. Existing platform results on base-stock optimality (Veinott's multi-product model, advance demand information) use different models and different arguments; none covers this recursion.

Difficulty

The argument is an induction on $n$ whose hypothesis carries convexity, the derivative formula (b), and bounds on $f_n'$. The delicate step is the existence of a finite root of $F_n$: its limit at $-\infty$ depends on whether the previous level was finite. For $n = 1$ nothing is ordered and the limit is $c - b\alpha$, which the assumption $b > \frac{1-\alpha}{\alpha}c$ does not make negative. The book's base case ("left to the reader") therefore fails when $c > \alpha b$: with $\alpha = \tfrac12$, $c = 1$, $b = \tfrac32$ the two-period problem never orders. The goal is corrected accordingly.

Two properties the book's induction also carries are not usable as printed. Property (d), $f_n' \le f_{n-1}'$, is false: for large $y$, $f_n'(y)$ approaches $h(1 + \alpha + \dots + \alpha^{n-1})$, which increases with $n$. The second-derivative clause of property (c) fails at $y = 0$ whenever $g(0^+) > 0$. A solver cannot follow the printed induction step for step; property (a), which the book derives from (d), is true and is a milestone in its own right.

Formalization scope

• Horizon. The book states Theorem 2 for "the optimal policy" without a horizon. Its proof is an induction on a finite horizon, and the passage $n \to \infty$ is left as a conjecture (p. 21). The goal is the finite-horizon theorem; no infinite-horizon value function is constructed.
• Lead time. The proof sets $\tau = 1$ "to simplify notation"; so does the formalization. Theorem 1 (dependence on the inventory position only) and Theorem 3 (general $\tau$, whose level equation is the conjectured infinite-horizon one) are not stated.
• Level $-\infty$. The goal allows "never order" as the order-up-to rule with level $-\infty$ and adds eventual finiteness; see Difficulty.
• Added hypotheses. $c \ge 0$, $h > 0$ (the book uses $\lim_{w\to\infty} f_n'(w - x) > 0$), $0 < \alpha$ (the book divides by $\alpha$), and a finite mean $\int_0^\infty x\,g(x)\,dx < \infty$ (without it $L$ is infinite). All are fields of Model, together with positivity and continuity of $g$ on $(0,\infty)$, $\int_0^\infty g = 1$, and $b > \frac{1-\alpha}{\alpha}c$.
• Minimum and derivatives. $f_n$ is defined with the infimum over $u \ge 0$ of a nonnegative quantity; optimality is always against every $u' \ge 0$. Statements about $f_n'$ assert differentiability (Differentiable, HasDerivAt) and do not read deriv as evidence of it.
• Levels. The book's $s_n^*$ is "the unique solution of (2.6)"; milestones take any real level at which the order-up-to rule is optimal.

A recursion in which ordering is restricted to order-up-to rules, or in which $f_n$ is defined through $s_n^*$, would make the goal a tautology; here $f_n$ is defined by minimization over all $u \ge 0$ and optimality is checked against all orders.

Needed infrastructure: convexity and differentiation of parametric integrals against a density on $(0,\infty)$, and minimization of a differentiable convex function over a half-line. Both are reusable for the other stochastic inventory missions on the platform. Proofs of individual milestones are welcome independently of the goal.

Selected references

• J. A. Muckstadt, Analysis and Algorithms for Service Parts Supply Chains, Springer Series in Operations Research and Financial Engineering, 2005, Chapter 2, Section 2.1. https://doi.org/10.1007/b138879
• S. Karlin and H. Scarf, Inventory models of the Arrow–Harris–Marschak type with time lag, in K. J. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958 (no DOI).
• K. J. Arrow, T. Harris and J. Marschak, Optimal inventory policy, Econometrica 19(3), 1951, 250–272. https://doi.org/10.2307/1906814
• R. Bellman, I. Glicksberg and O. Gross, On the optimal inventory equation, Management Science 2(1), 1955, 83–104. https://doi.org/10.1287/mnsc.2.1.83
• A. F. Veinott Jr., Optimal policy for a multi-product, dynamic, nonstationary inventory problem, Management Science 12(3), 1965, 206–222. https://doi.org/10.1287/mnsc.12.3.206

Motivation

Two-stage stochastic integer programs combine the two hardest features of mathematical programming: uncertainty in the data and integrality of the decisions. Even evaluating the objective of such a program at a single first-stage decision requires the expected optimal value of an NP-hard combinatorial problem. Chapter 8 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by A. H. G. Rinnooy Kan and L. Stougie, argues that for many such problems the way forward is probabilistic analysis: the random optimal value of the second-stage problem often converges, after normalization, to a simple function of the problem parameters, and that function can replace the intractable expectation.

The chapter illustrates this on the machine investment problem: first buy $m$ identical machines at cost $c$ each, knowing only the distribution of the processing times of $n$ jobs, then schedule the jobs once their processing times are revealed so as to minimize the makespan. This mission formalizes the chapter's analysis of that example: the almost sure asymptotics of the optimal makespan (8.13), its expectation version, and the asymptotic clairvoyance of the resulting two-stage heuristic.

Setting

Let $p_1, p_2, \dots$ be processing times: independent, identically distributed, nonnegative random variables on a probability space $(\Omega, \mathcal F, P)$ with mean $\mu = \mathbb E p_1 > 0$ and finite second moment $\mathbb E p_1^2 < \infty$. The instance with $n$ jobs uses the first $n$ of them.

An assignment of the $n$ jobs to $m \ge 1$ identical machines is a map $\sigma : \{1, \dots, n\} \to \{1, \dots, m\}$. The load of machine $i$ is $\sum_{j : \sigma(j) = i} p_j$ and the makespan of $\sigma$ is its largest load. The minimum makespan is

$$C^*_n(m) = \min_{\sigma} \max_{i=1,\dots,m} \sum_{j:\ \sigma(j) = i} p_j ,$$

and the machine investment problem is to minimize $Z_n(m) = cm + \mathbb E\, C^*_n(m)$ over integers $m$ (8.9).

List scheduling takes the jobs in the order $1, \dots, n$ and assigns each to the first available machine, a machine of least current load (lowest index on ties). Its makespan is $C^H_n(m)$. Write $S_n = \sum_{j=1}^n p_j$ and $p_{\max} = \max_{j \le n} p_j$.

For §8.3, the estimate $Z'_n(m) = cm + n\mu/m$ is minimized over integers by the heuristic first-stage decision $m^{H1}_n$, the better of $\lfloor\sqrt{n\mu/c}\rfloor$ and $\lceil\sqrt{n\mu/c}\rceil$. A clairvoyant decision maker who sees the processing times first chooses $m^\circ_n(\omega) \ge 1$ minimizing $cm + C^*_n(m)$.

Formalization targets

Goal: Eq. (8.13)

For machine counts $m = m(n) \ge 1$ with $m(n) = O(\sqrt n)$,

$$P\Bigl\{ \lim_{n\to\infty} \frac{C^*_n(m)}{n\mu/m} = 1 \Bigr\} = 1 .$$

The machine count is allowed to grow with $n$; this is the regime the first-stage heuristic lives in, since $m^{H1}_n$ is of exact order $\sqrt n$.

Milestones

1. Eq. (8.10): the deterministic sandwich $S_n/m \le C^*_n(m) \le C^H_n(m) \le S_n/m + p_{\max}$, divided by $n\mu/m$.
2. Eq. (8.11): the strong law of large numbers, $(S_n - n\mu)/(n\mu) \to 0$ almost surely (a published platform theorem).
3. Lemma 8.1 (i): $p_{\max}/\sqrt n \to 0$ almost surely.
4. Eq. (8.12): $m\, p_{\max}/(n\mu) \to 0$ almost surely when $m = O(\sqrt n)$.
5. Lemma 8.1 (ii): $\mathbb E\, p_{\max}/\sqrt n \to 0$.
6. p. 207: $\mathbb E\, C^*_n(m)/(n\mu/m) \to 1$ when $m = O(\sqrt n)$.
7. p. 211, asymptotic clairvoyance: almost surely

$$\lim_{n\to\infty} \frac{c\, m^{H1}_n + C^{H2}_n(m^{H1}_n)}{c\, m^\circ_n + C^*_n(m^\circ_n)} = 1 ,$$

where $C^{H2}_n$ is the list-scheduling makespan.

Significance

Result (8.13) says that the optimal value of an NP-hard problem, rescaled, is almost surely asymptotic to the elementary function $n\mu/m$ of the data and the first-stage decision. Its expectation version replaces the intractable term $\mathbb E\,C^*_n(m)$ in (8.9) by $n\mu/m$, and the clairvoyance statement shows that the heuristic built on that replacement loses asymptotically nothing, not even against a decision maker with full information. The chapter presents the example as the template for vehicle routing and location problems preceded by an investment decision.

All results here are classical and proved in the literature cited by the chapter (Lemma 8.1 is quoted from Feller without proof; the chapter refers to Dempster et al. for the asymptotic optimality of the two-stage heuristic and to Lenstra et al. for the notion of asymptotic clairvoyance). None of them has, to our knowledge, a machine-checked proof. The mission produces a formal model of identical-machine makespan scheduling and of list scheduling, the extreme-value estimates of Lemma 8.1 for square-integrable i.i.d. sequences, and the full chain from the strong law to (8.13).

Difficulty

The deterministic part is elementary on paper, but list scheduling is a recursively defined procedure, and its makespan bound has to be established for that recursion rather than for a picture like the chapter's Figure 8.3. The probabilistic core is Lemma 8.1: the strong law controls $S_n/n$, but the error term $m\, p_{\max}/(n\mu)$ is of order $p_{\max}/\sqrt n$ once $m$ grows like $\sqrt n$, and the strong law says nothing about maxima. With a fixed number of machines the whole statement would reduce to the strong law; the growth $m(n) = O(\sqrt n)$ is exactly where the second moment is needed. For the clairvoyance statement, the clairvoyant choice $m^\circ_n$ is a random, unstructured minimizer, so its value must be bounded below without knowing where the minimum is attained.

Formalization scope

Processing times are one sequence p : ℕ → Ω → ℝ, 0-based (the book's $p_j$ is p (j-1)), with each p j measurable, the family mutually independent (iIndepFun), identically distributed with p 0, pointwise nonnegative, p 0 ^ 2 integrable and ∫ p 0 = μ with μ > 0. Nonnegativity and $\mu > 0$ are not printed in the book; they are implicit in "processing times" and in the division by $n\mu$. Machines are Fin m; a schedule is an assignment Fin n → Fin m, which is faithful because jobs are non-preemptive, machines identical and there are no precedence constraints.

The book writes "$m = 0(\sqrt n)$"; this is read as $m$ a function of $n$ with $m(n) \ge 1$ and (fun n => (m n : ℝ)) =O[atTop] (fun n => √n). Stating (8.13) for a fixed $m$ would trivialize it into the strong law and is ruled out. "$\Pr\{\lim \dots = 1\} = 1$" means that almost surely the limit exists and equals $1$. Expectations are Bochner integrals of functions that are measurable and bounded by $S_n$, hence integrable. List scheduling uses the index order and breaks ties towards the lowest machine index; both are admissible instances of the book's "arbitrary fixed order" and "first available machine". In the clairvoyance statement the minimum is over $m \ge 1$ (the book writes $m \in \mathbb N$; no machine cannot process any job, and the Lean value $C^*_n(0)$ is an empty-infimum convention). No explicit constants replace an O(·): the statements are limits and the O-hypothesis is carried as stated.

Out of scope: (8.14) and the p. 210 expectation statement, which need a positive density at $0$ and whose proof the book calls "far from easy", and the dynamic programming recursion of §8.3.

Needed infrastructure: finite maxima and minima of measurable functions, extreme-value estimates for square-integrable i.i.d. sequences (Lemma 8.1), and Mathlib's strong law. The makespan and list-scheduling definitions are reusable for other identical-machine scheduling results; alternative proofs of Lemma 8.1 and sharper forms of the clairvoyance statement are welcome.

Selected references

• A. H. G. Rinnooy Kan, L. Stougie, "Stochastic Integer Programming", in Yu. Ermoliev, R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 8, pp. 201–213. https://doi.org/10.1007/978-3-642-61370-8
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, 3rd edition, Wiley, 1968 (cited by the chapter for Lemma 8.1).
• M. A. H. Dempster, M. L. Fisher, L. Jansen, B. J. Lageweg, J. K. Lenstra, A. H. G. Rinnooy Kan, "Analysis of heuristics for stochastic programming: results for hierarchical scheduling problems", Mathematics of Operations Research 8 (1983) 525–537. https://doi.org/10.1287/moor.8.4.525
• J. K. Lenstra, A. H. G. Rinnooy Kan, L. Stougie, "A framework for the design and analysis of hierarchical planning systems", Annals of Operations Research 1 (1984) 23–42. https://doi.org/10.1007/BF01874451
• R. L. Graham, "Bounds on multiprocessing timing anomalies", SIAM Journal on Applied Mathematics 17 (1969) 416–429. https://doi.org/10.1137/0117039

Motivation

Many optimization problems in operations research have an objective that is an expectation, $F^0(x)=E f^0(x,\omega)$, over a random parameter $\omega$ whose distribution is known only through samples or is too complex to integrate. Two-stage stochastic programs, inventory and reliability models, and simulation-based design all have this form. Neither $F^0$ nor its subgradients can be evaluated exactly, but a random vector whose conditional mean is close to a subgradient is often cheap to compute: a sample subgradient of $f^0(\cdot,\omega)$, or a finite-difference quotient of two sampled values.

Stochastic quasigradient (SQG) methods, developed by Ermoliev and co-workers in Kiev from the late 1960s, use such vectors in place of subgradients. They extend the stochastic approximation procedures of Robbins–Monro (1951) and Kiefer–Wolfowitz (1952) to nonsmooth convex objectives, general convex constraints, and directions whose conditional mean is biased by a vanishing amount. This mission formalizes the basic convergence theory of the simplest SQG method, the projection method, as presented by Yu. Ermoliev in Chapter 6 of the IIASA volume Numerical Techniques for Stochastic Optimization (Springer 1988).

Timeline (as cited in the chapter's bibliography).

• 1951–1954: Robbins and Monro, Kiefer and Wolfowitz, Dvoretzky and Blum prove convergence of stochastic approximation for unconstrained smooth problems.
• 1962–1967: Shor introduces the generalized gradient (subgradient) method; Ermoliev (Kibernetika 4, 1966) and Polyak (Soviet Math. Doklady 8, 1967) prove its convergence.
• 1967–1969: Ermoliev and Nekrylova introduce stochastic subgradients; Ermoliev ("On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2, 1969) introduces stochastic quasi-Féjer sequences.
• 1976: Ermoliev's monograph Stochastic Programming Methods (Nauka) contains the proof of Theorem 6.1 (p. 98).
• 1988: the survey chapter formalized here presents the projection method, Theorems 6.1 and 6.2, and an efficiency estimate for the averaged iterate.

Setting

Let $X\subseteq\mathbb R^n$ be a nonempty convex compact set and $F^0:\mathbb R^n\to\mathbb R$ convex and continuous on $X$. The optimal set is $X^*=\{x\in X: F^0(x)\le F^0(y)\ \forall y\in X\}$. The projection onto $X$ is $\pi_X(y)=\operatorname{argmin}\{\|y-x\|^2:x\in X\}$.

On a probability space, the stochastic quasigradient projection method produces random vectors $x^0,x^1,\dots$ by

$$x^{s+1}=\pi_X\big[x^s-\rho_s\,\xi^0(s)\big],\qquad s=0,1,\dots \tag{6.11}$$

where $\rho_s\ge0$ is a step size and $\xi^0(s)$ a random direction. Write $E\{\cdot\mid x^0,\dots,x^s\}$ for conditional expectation given the history $\sigma(x^0,\dots,x^s)$. The direction is a stochastic quasigradient if, for every $x^*\in X^*$,

$$F^0(x^*)-F^0(x^s)\ge\big\langle E\{\xi^0(s)\mid x^0,\dots,x^s\},\,x^*-x^s\big\rangle+\gamma_0(s)\quad\text{a.s.}, \tag{6.12}$$

where the error $\gamma_0(s)$ is a function of the history. If the conditional mean of $\xi^0(s)$ is a subgradient plus a bias $b^0(s)$, then (6.12) holds with $\gamma^0(s)=-\langle b^0(s),x^*-x^s\rangle$ (6.13).

A sequence of random vectors $z^0,z^1,\dots$ is a stochastic quasi-Féjer sequence for $Z\subseteq\mathbb R^n$ if $E\|z^0\|^2<\infty$ and there are random $r_s\ge0$ with $\sum_s E r_s<\infty$ such that for all $z\in Z$

$$E\{\|z-z^{s+1}\|^2\mid z^0,\dots,z^s\}\le\|z-z^s\|^2+r_s. \tag{6.14}$$

Formalization targets

Goal: Theorem 6.2

If, with probability 1, $\rho_s\ge0$ and $\sum_s\rho_s=\infty$, and

$$\sum_{s=0}^\infty E\{\rho_s|\gamma_0(s)|+\rho_s^2\|\xi^0(s)\|^2\}<\infty, \tag{6.15}$$

then with probability 1 the iterates converge and $\lim_s x^s\in X^*$.

Milestones

1. Theorem 6.1 (a)–(c). For a stochastic quasi-Féjer sequence for $Z$: $\|z-z^{s+1}\|^2$ converges a.s. and $E\|z-z^s\|^2$ is bounded, for each $z\in Z$; accumulation points exist a.s. (for $Z\ne\emptyset$); and a.s. $Z$ lies in the hyperplane equidistant from any two distinct accumulation points outside $Z$.
2. Eq. (6.13). Biased stochastic subgradients satisfy (6.12).
3. One-step inequality (p. 145): $E\{\|x^*-x^{s+1}\|^2\mid\cdot\}\le\|x^*-x^s\|^2+2\rho_s\langle E\{\xi^0(s)\mid\cdot\},x^*-x^s\rangle+E\{\rho_s^2\|\xi^0(s)\|^2\mid\cdot\}$ for $x^*\in X$.
4. Quasi-Féjer property (p. 145): the iterates of (6.11) form a stochastic quasi-Féjer sequence for $X^*$.
5. Efficiency estimate (p. 147), for deterministic $\rho_k$ and $\bar x^s=\sum_{k\le s}\rho_kx^k/\sum_{k\le s}\rho_k$:

$$E F^0(\bar x^s)-F^0(x^*)\le\Big(2\sum_{k=0}^s\rho_k\Big)^{-1}\Big[E\|x^*-x^0\|^2+\sum_{k=0}^s E\big(2\rho_k|\gamma_0(k)|+\rho_k^2\|\xi^0(k)\|^2\big)\Big].$$

Significance

Theorem 6.2 is the prototype convergence theorem for SQG methods. Its hypotheses allow random step sizes chosen from the history, nonsmooth objectives, and directions with a bias that vanishes fast enough; its conclusion is convergence of the iterates themselves to a single optimal point, not only convergence of function values or of $\operatorname{dist}(x^s,X^*)$. The later chapters of the same volume (adaptive step sizes, Chapters 17–18; nonstationary problems, §6.4) reuse the same framework. Theorem 6.1 isolates the probabilistic content in a form that applies to any algorithm with a quasi-Féjer inequality. The efficiency estimate gives a non-asymptotic accuracy bound for the averaged iterate.

The results are classical and proved in the literature: Theorem 6.1 in Ermoliev (1976, p. 98), Theorem 6.2 in this chapter (pp. 145–146). To our knowledge none of them has a machine-checked proof. Mathlib has conditional expectations and the a.s. martingale convergence theorem, but no Robbins–Siegmund-type almost-supermartingale lemma and no stochastic subgradient method. A formal proof of this mission would supply both.

Difficulty

The deterministic argument for projected subgradient methods compares $\|x^*-x^{s+1}\|$ with $\|x^*-x^s\|$ for a fixed $x^*$. In the stochastic setting this comparison holds only in conditional mean, with a perturbation $r_s$ that is random, and the distances converge only almost surely, with an exceptional null set that depends on $x^*$. Since $X^*$ is typically uncountable, "for every $x^*$, almost surely" does not immediately give "almost surely, for every $x^*$", and it is the second form that identifies a single limit. A second difficulty is that $\sum\rho_s(F^0(x^s)-F^0(x^*))<\infty$ only yields a subsequence along which $F^0$ approaches its minimum; passing from there to convergence of the whole sequence is exactly what part (c) of Theorem 6.1 is for.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). The probability space is an arbitrary measurable space with a probability measure. $\pi_X$ is a chosen minimizer of $\|y-x\|^2$ over $X$ (unique for nonempty closed convex $X$). The history is the $\sigma$-algebra generated by $x^0,\dots,x^s$; $\rho_s$ and $\gamma_0(s)$ are measurable with respect to it.
• Directions $\xi^0(s)$ are integrable and random vectors are measurable; conditional expectations are Mathlib's condExp. The quasi-Féjer definition requires square integrability of every $z^s$ (implied by the book's definition when $Z\ne\emptyset$), so no conditional expectation is taken of a non-integrable function.
• $X\ne\emptyset$ and $x^0\in X$ are stated; $Z\ne\emptyset$ is added in Theorem 6.1 (b), which is false without it.
• $\gamma_0(s)$ does not depend on $x^*$; the $x^*$-dependent error of (6.13) is dominated on a bounded $X$ by $\|b^0(s)\|\operatorname{diam}X$.
• (6.15) keeps its mixed form: $\rho_s\ge0$ and $\sum\rho_s=\infty$ almost surely, and a deterministic sum of expectations (lower Lebesgue integrals) finite.
• Explicit constants. The book's "$C$" in the efficiency estimate is instantiated from its proof: $2$ on $\rho_k|\gamma_0(k)|$ and $1$ on $\rho_k^2\|\xi^0(k)\|^2$. The unspecified $C$ before the quasi-Féjer sentence is replaced by the existence of summable $r_s$.
• Typo corrections. The one-step inequality on p. 145 prints $\rho_sE\{\|\xi^0(s)\|^2\mid\cdot\}$; it is $\rho_s^2$. The efficiency estimate on p. 147 omits $E$ before the last sum; it is restored. "$\rho_k$ independent of $(x^0,\dots,x^k)$" is read as deterministic step sizes.
• A trivializing formalization is excluded: the goal does not replace $\xi^0(s)$ by an exact subgradient, does not set $\gamma_0\equiv0$, and concludes convergence of $x^s$ to a point of $X^*$ rather than $\operatorname{dist}(x^s,X^*)\to0$.
• Reusable infrastructure: a Robbins–Siegmund lemma for nonnegative almost-supermartingales, the nonexpansiveness of $\pi_X$, and Theorem 6.1 itself, which applies to any quasi-Féjer algorithm (Chapter 6 §6.4 and Chapters 17–18 of the same book). Contributions of these general lemmas are welcome.

Selected references

• Yu. Ermoliev, "Stochastic Quasigradient Methods", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 6, §6.1–6.2 (pp. 141–147). https://doi.org/10.1007/978-3-642-61370-8
• Yu. Ermoliev, "On the stochastic quasi-gradient method and stochastic quasi-Feyer sequences", Kibernetika 2 (1969) (in Russian; English translation in Cybernetics). Reference [3] of the chapter.
• Yu. Ermoliev, Stochastic Programming Methods, Nauka, Moscow, 1976 (in Russian); Theorem 6.1 is on p. 98. Reference [5] of the chapter.
• H. Robbins and D. Siegmund, "A convergence theorem for non negative almost supermartingales and some applications", in J. S. Rustagi (ed.), Optimizing Methods in Statistics, Academic Press, 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• H. Robbins and S. Monro, "A stochastic approximation method", Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586