Optimization

Motivation

Blackwell approachability is the vector-payoff analogue of von Neumann's minimax theorem. In a repeated game where each round's outcome is a vector $u(x_t, y_t) \in \mathbb R^d$, a player wants the running average of these vectors to converge to a target set $S$, whatever the opponent does. Blackwell (1956) showed when this is possible, and approachability has since become a standard tool for calibrated forecasting, regret minimization with respect to general benchmarks, and learning in games.

Online linear optimization (OLO) is the problem of choosing points $\theta_t$ in a fixed decision set $\mathcal K$ against a sequence of linear losses $\langle f_t, \cdot\rangle$, with performance measured by regret against the best fixed point in hindsight. Algorithms with regret $o(T)$ — "no-regret" algorithms such as online gradient descent (Zinkevich, 2003) — are among the most studied objects of machine learning.

Abernethy, Bartlett and Hazan (COLT 2011) showed that the two problems are algorithmically equivalent: each can be converted into the other with explicit control of the rates. This mission covers the direction from OLO to approachability.

Timeline:

• 1956: Blackwell proves the approachability theorem for convex sets, via a geometric projection strategy.
• 2003: Zinkevich introduces online gradient descent, a no-regret algorithm for any bounded convex decision set.
• 2009: Even-Dar, Kleinberg, Mannor and Mansour state approachability in the response-satisfiability form (as cited on p. 32 of the 2011 paper).
• 2011: Abernethy, Bartlett and Hazan give the two reductions, with explicit rates, and apply them to efficient calibration.

Setting

A Blackwell instance $(\mathcal X, \mathcal Y, u, S)$ consists of compact convex sets $\mathcal X \subseteq \mathbb R^n$, $\mathcal Y \subseteq \mathbb R^m$, a payoff $u : \mathcal X \times \mathcal Y \to \mathbb R^d$ that is affine in each argument (biaffine), and a closed convex target set $S \subseteq \mathbb R^d$. Write $\mathtt{dist}(z, U) = \inf_{w \in U}\|z - w\|$ for the Euclidean distance to a set, and $B_2(r)$ for the closed Euclidean ball of radius $r$.

A halfspace oracle takes a halfspace $H = \{z : \langle a, z\rangle \le c\}$ and returns a point $\mathcal O(H) \in \mathcal X$; it is valid if for every halfspace $H \supseteq S$, $u(\mathcal O(H), y) \in H$ for all $y \in \mathcal Y$.

A set $X \subseteq \mathbb R^d$ is a cone if $\alpha z \in X$ for all $z \in X$, $\alpha \ge 0$. For $K \subseteq \mathbb R^d$, $\mathtt{cone}(K) = \{\alpha x : \alpha \ge 0, x \in K\}$, and the polar cone of $C$ is $C^0 = \{\theta : \langle \theta, x\rangle \le 0 \ \forall x \in C\}$.

An OLO algorithm $\mathcal L$ maps past loss vectors $(f_1, \dots, f_{t-1})$ to a point $\theta_t \in \mathcal K$, and its regret is

$$\mathrm{Regret}_T = \sum_{t=1}^T \langle f_t, \theta_t\rangle - \min_{\theta \in \mathcal K} \sum_{t=1}^T \langle f_t, \theta\rangle .$$

Algorithm 2 runs $\mathcal L$ on $\mathcal K = S^0 \cap B_2(1)$ when $S$ is a cone: at round $t$ it sets $\theta_t = \mathcal L(f_1, \dots, f_{t-1})$, plays $x_t = \mathcal O(\{z : \langle \theta_t, z\rangle \le 0\})$, observes $y_t \in \mathcal Y$, and feeds $f_t = -u(x_t, y_t)$ back to $\mathcal L$.

When $S$ is compact but not a cone, it is lifted: with $\kappa = \max_{s\in S}\|s\|$ and $\kappa \oplus z \in \mathbb R^{d+1}$ the concatenation, put $u'(x, y) = \kappa \oplus u(x, y)$ and $S' = \mathtt{cone}(\{\kappa\} \times S)$, and run Algorithm 2 on $(\mathcal X, \mathcal Y, u', S')$.

Formalization targets

Goal: Corollary 18 (p. 39)

For a Blackwell instance with $S$ nonempty and compact, any valid halfspace oracle for the lifted instance, any OLO algorithm with values in $\mathcal K' = (S')^0 \cap B_2(1)$, any $T \ge 1$ and any $y_1, \dots, y_T \in \mathcal Y$, the run of Algorithm 2 on the lifted instance satisfies

$$\mathtt{dist}\Big(\frac1T\sum_{t=1}^T u(x_t,y_t), S\Big) \le 2\,\mathtt{dist}\Big(\frac1T\sum_{t=1}^T u'(x_t,y_t), S'\Big) \le \frac2T\,\mathrm{Regret}_T .$$

The bound holds for every $T$ and every adversary, with no rate assumed for $\mathcal L$; a no-regret $\mathcal L$ then gives approachability.

Milestones

1. Lemma 13 (p. 35): for a nonempty convex cone $C$, $\mathtt{dist}(x, C) = \max_{\theta \in C^0 \cap B_2(1)} \langle \theta, x\rangle$.
2. Theorem 17 (p. 38): if $S$ is a cone, Algorithm 2 achieves $\mathtt{dist}\big(\frac1T\sum_t u(x_t,y_t), S\big) \le \mathrm{Regret}(\mathcal L_{\mathcal K}; f_{1:T})/T$.
3. Lemma 14 (p. 35): for nonempty compact convex $\mathcal K$, $\kappa = \max_{\mathcal K}\|\cdot\|$ and $x \notin \mathcal K$, $\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K)) \le \mathtt{dist}(x, \mathcal K) \le 2\,\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K))$.

Significance

The result. Corollary 18 turns any no-regret algorithm into an approachability strategy for a compact convex target, provided a valid halfspace oracle is available, with rate $2\,\mathrm{Regret}_T/T$. Combined with online gradient descent it gives an $O(1/\sqrt T)$ approachability rate, and through the choice of OLO algorithm it lets approachability inherit the computational efficiency of online learning. The paper uses this route to build an efficient calibrated forecaster (Section 5). Together with the converse reduction (Theorem 16), it shows that the two problems are equivalent.

Formalizing it. The results are proved in the paper; none of them has been machine-checked. Formalizing them requires the conic duality formula for distances (Lemma 13), a quantitative lifting lemma (Lemma 14) and the bookkeeping of an interactive protocol. The proof of Lemma 14 on the page is a sketch: it refers to an undefined point and uses a triangle-similarity argument, so a complete proof is new work.

Difficulty

The reduction's core is Lemma 13: the distance to a cone is a maximum of a linear function over the polar cone's unit ball. Lemma 13 needs projection onto a cone in Euclidean space; for a non-closed cone the projection may not exist, and the argument must go through the closure. The lifting Lemma 14 is a geometric statement whose page proof relies on a picture and an undefined point, so the factor 2 has no complete written argument. Finally, connecting the average lifted payoff to the lift of the average payoff, and the halfspace guarantee $\langle\theta_t, f_t\rangle \ge 0$ to the regret, requires keeping the round indexing and the oracle's validity domain exactly aligned.

Formalization scope

All spaces are EuclideanSpace ℝ (Fin d). The concatenation $\kappa\oplus z$ lives in EuclideanSpace ℝ (Fin (d+1)) with coordinate 0 equal to $\kappa$, so $\|\kappa\oplus z\|^2 = \kappa^2 + \|z\|^2$; a product type with the sup norm would change every distance and is ruled out. Distances are Metric.infDist. The polar cone uses the paper's sign ($\le 0$), the negative of Mathlib's innerDual. A halfspace is the pair $(a, c)$; a valid oracle must answer every halfspace containing $S$, including $a = 0$, not only the halfspaces the algorithm happens to query. The OLO algorithm is a map from histories Fin t → ℝᴰ with values in $S^0 \cap B_2(1)$ at every history. Rounds are $t = 1, \dots, T$, and the run of Algorithm 2 is given as hypotheses on sequences $\theta, x, f$, which exist and are unique by recursion. The minimum in the regret and $\kappa$ are written as sInf/sSup of images over nonempty compact sets, where they are attained.

Hypotheses added relative to the page: $S \neq \emptyset$ and $T \ge 1$ in the goal; $C \ne \emptyset$ in Lemma 13 (the empty set is a cone under Definition 11 and the identity fails for it); $\mathcal K \ne \emptyset$ in Lemma 14. Corrected misprints, each disclosed in the item's note: "$\mathrm{Regret}_T(\mathcal A)$" in Corollary 18 and (9) denotes the regret of the OLO algorithm $\mathcal L$ on the lifted losses; Lemma 14's "$\mathcal K \subseteq \mathcal H$" has a stray $\mathcal H$; $\kappa$ is the maximal norm of the set, not its diameter. The oracle in the goal is a valid oracle for the lifted instance, which is what applying Algorithm 2 to $(\mathcal X, \mathcal Y, u', S')$ requires.

A formalization in which the oracle is valid only at the run's own queries, the OLO algorithm is unconstrained, the regret's minimum ranges over all of $\mathbb R^{d+1}$, or the middle term of the goal is dropped, is a different statement and is ruled out.

The development needs: the dual formula for the distance to a convex cone, nearest-point projection onto closed convex sets (in Mathlib), compactness of polar-cone slices, and finite sums of biaffine payoffs. The cone layer (Lemma 13) is reusable for the converse direction of the paper and for conic duality generally. Proofs of any milestone, and of the bridge from an oracle for the original instance to one for the lifted instance, are welcome.

Selected references

• J. Abernethy, P. L. Bartlett, E. Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, JMLR W&CP 19 (COLT 2011), pp. 27–46. https://proceedings.mlr.press/v19/abernethy11b.html
• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6(1), 1956, pp. 1–8. https://doi.org/10.2140/pjm.1956.6.1
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf

Motivation

Many estimation procedures in statistics, and most stochastic optimization models in operations research, have the same shape: a decision or parameter $x\in\mathbb R^n$ is chosen to minimize an expected loss $Ef(x)=\int f(x,\xi)\,P(d\xi)$ under a distribution $P$ that is not known. In practice $P$ is replaced by an estimate $P^\nu$ built from the information available at stage $\nu$ (an empirical measure, a smoothed or parametric fit, a Bayesian posterior), and the minimizer of the estimated problem is used in place of the true one. The basic question is whether this is justified: do the estimated solutions converge to a true solution, and the estimated optimal values to the true optimal value, as information accumulates?

For maximum likelihood this is Wald's consistency theorem (Wald 1949); Huber extended it to M-estimators under non-standard conditions (Huber 1967). Both settings are unconstrained, or constrained to an open set, and assume finite-valued criteria. Constrained least squares, $L^1$ and Huber regression with inequality constraints, variance-component models with Heywood cases, and two-stage stochastic programs with recourse all lead instead to criteria that take the value $+\infty$ off a closed feasible set and are only lower semicontinuous in $x$.

J. Dupačová and R. Wets (IIASA WP-86-41, 1986; journal version Ann. Statist. 16 (1988)) proved consistency in this generality by combining epi-convergence of functions with the theory of measurable multifunctions and normal integrands. This mission formalizes their §3.

Setting

$\Xi$ is a Polish space with its Borel $\sigma$-field and $P$ is a probability measure on it. The integrand is $f:\mathbb R^n\times\Xi\to(-\infty,\infty]$, and the true problem is to minimize

$$Ef(x)=\int_\Xi f(x,\xi)\,P(d\xi),$$

with the convention that $Ef(x)=+\infty$ whenever $\xi\mapsto f(x,\xi)$ is not bounded above by a summable function. The effective domain of a function $h:\mathbb R^n\to[-\infty,\infty]$ is $\operatorname{dom}h=\{x: h(x)<\infty\}$, and $\operatorname{argmin}h=\{x: h(x)=\inf h\}$.

Information arrives on a probability space $(Z,\mathcal F,\mu)$ with an increasing sequence of $\sigma$-fields $\mathcal F^1\subseteq\mathcal F^2\subseteq\dots\subseteq\mathcal F$. Each sample $\zeta\in Z$ yields probability measures $P^\nu(\cdot,\zeta)$ on $\Xi$, and $\zeta\mapsto P^\nu(A,\zeta)$ is $\mathcal F^\nu$-measurable for every Borel $A$: the estimate at stage $\nu$ uses only stage-$\nu$ information. The estimated problem minimizes

$$E^\nu f(x,\zeta)=\int_\Xi f(x,\xi)\,P^\nu(d\xi,\zeta).$$

A sequence $g^\nu$ epi-converges to $g$ if, at every $x$, $\liminf g^\nu(x^\nu)\ge g(x)$ along every sequence $x^\nu\to x$, and $\limsup g^\nu(x^\nu)\le g(x)$ along some sequence $x^\nu\to x$.

The standing hypotheses are Assumption 3.4: $\operatorname{dom}f=S\times\Xi$ with $S$ closed and nonempty; $f(x,\cdot)$ is continuous for $x\in S$; $f(\cdot,\xi)$ is lower semicontinuous; and $f$ is locally lower Lipschitz on $S$ with a bounded continuous modulus $\beta(\xi)$. Assumption 3.5 asks that, for $\mu$-almost every $\zeta$, $P^\nu(\cdot,\zeta)$ converge in distribution to $P$, that $|f(x,\cdot)|$ be uniformly tight along $P=P^0,P^1,\dots$ for each $x\in S$, and that $\int\inf_x f(x,\xi)\,P^\nu(d\xi,\zeta)>-\infty$ for all $\nu$.

Formalization targets

Goal: Theorem 3.9, "In particular" (pp. 21–22)

Let $D\subseteq\mathbb R^n$ be compact, suppose $(\operatorname{argmin}E^\nu f)\cap D\neq\emptyset$ $\mu$-a.s. for every $\nu$, and suppose $\{x^*\}=\operatorname{argmin}Ef\cap D$. Then there are $\mathcal F^\nu$-measurable selections $x^\nu$ of $\operatorname{argmin}E^\nu f$ with

$$x^\nu(\zeta)\to x^*\quad\text{and}\quad \inf E^\nu f(\cdot,\zeta)\to\inf Ef\qquad\text{for }\mu\text{-almost every }\zeta .$$

The goal does not assume that $Ef$ has a unique global minimizer, and it does not assume convexity.

Milestones

In attack order:

• Proposition 3.3: epi-convergence gives $\limsup(\inf g^\nu)\le\inf g$, limits of minimizers are minimizers, and the minimum is attained in the closure of a bounded $D$.
• Lemma 3.6: almost surely, $Ef$ and every $E^\nu f$ are proper and l.s.c., with domain $S$.
• Theorem 3.7: almost surely, $E^\nu f$ epi-converges and converges pointwise to $Ef$.
• Theorem 3.8: almost surely, the epigraphs of $E^\nu f$ are closed, and they depend $\mathcal F^\nu$-measurably on $\zeta$.
• Theorem 3.9:
  • (3.14) $\limsup(\inf E^\nu f)\le\inf Ef$ a.s.;
  • (i) cluster points of estimated minimizers minimize $Ef$;
  • (ii) $\zeta\mapsto\operatorname{argmin}E^\nu f(\cdot,\zeta)$ is closed-valued and $\mathcal F^\nu$-measurable.
• Proposition 3.1: the measurable selection theorem.

Significance

The result separates two things: the statistical input, which is only convergence in distribution of $P^\nu$ plus a tightness condition, and the variational output, which is convergence of optimal values and solutions. It therefore applies to any estimator $P^\nu$ that converges weakly almost surely: empirical measures, kernel estimates, parametric fits. It also covers constrained and nonsmooth problems: the feasible set enters through $f=+\infty$ off $S$, and only lower semicontinuity in $x$ is required. Asymptotic distribution results for constrained estimators, such as the second part of the same paper and the subsequent literature on sample average approximation, start from this consistency.

The theorem is proved on paper. To the best of current knowledge none of it is machine-checked. Mathlib has weak convergence of probability measures, lower semicontinuity and extended-real integrals. It does not have epi-convergence, Effros-measurable multifunctions, normal integrands or the Kuratowski–Ryll-Nardzewski selection theorem. A formal proof produces these as reusable components. It also has to supply the details that the paper's proof of Theorem 3.8 leaves as a sketch.

Difficulty

Pointwise convergence $E^\nu f(x)\to Ef(x)$ is not enough to move minimizers to the limit, and uniform convergence fails because $f$ is $+\infty$ off $S$ and need not be bounded. Epi-convergence is the right notion. Proving it needs a liminf inequality along moving points $x^\nu\to x$ under moving measures $P^\nu$. That combines Fatou's lemma, the lower Lipschitz bound and the tightness condition, and the integrands are extended-real-valued, so care is needed.

The second difficulty is measurability. The exceptional null set lies in $\mathcal F$ but not in $\mathcal F^\nu$, so "$\mathcal F^\nu$-measurable" has to be understood on a full-measure set in the trace $\sigma$-field. The paper's argument for Theorem 3.8 appeals to continuity of $P\mapsto\operatorname{epi}E_Pf$ in the epi-topology, and it remarks itself that Theorem 3.7 gives this only along sequences satisfying Assumption 3.5. A solver will have to rebuild this step, for example through the normal-integrand structure of $E^\nu f$.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with its Euclidean norm.
• $\Xi$ is a Polish space with its Borel $\sigma$-algebra. This is exactly a closed subset of a Polish space with the relative Borel field.
• $f$ is EReal-valued. Every expectation is the mission's expect: $+\infty$ when $\int f^+=\infty$, and $\int f^+-\int f^-$ otherwise, both computed as Lebesgue integrals of $[0,\infty]$-valued functions. A Bochner integral, which would assign $0$ to non-integrable functions, is never used for $Ef$ or $E^\nu f$.
• The sample index is shifted: Lean's Pν k and 𝔽 k are the paper's $P^{k+1}$ and $\mathcal F^{k+1}$, and $P=P^0$ is a separate argument.
• Infima, $\liminf$ and $\limsup$ are taken in $[-\infty,\infty]$.
• Measurability on the full-measure set $Z_0$ uses the trace $\sigma$-field.
• The selections in the goal are total, $\mathcal F^\nu$-measurable maps $Z\to\mathbb R^n$ that select almost surely. This is equivalent to the paper's maps $Z_0\to\mathbb R^n$.
• "Random l.s.c. function" in Theorem 3.8 is encoded by the equivalent conditions (3.4i)–(3.4ii): nonempty, closed and measurable epigraphs.
• Lower Lipschitz (3.10) is written additively.
• The hypothesis that $\Xi$ is the support of $P$ is omitted. It is unused in §3, and omitting it strengthens every statement.
• Nothing beyond the page is assumed: no convexity, no compact $S$, no bounded $f$, no unique minimizer, no i.i.d. sampling, no empirical $P^\nu$, no completeness of $\mu$ or $\mathcal F^\nu$.

The hypotheses are not vacuous. A sorry-free check verifies all of them, including those of the goal, for $f(x,\xi)=\|x\|^2$ with Dirac measures. Defining the expectation through a Bochner integral, or dropping $S\neq\emptyset$ (which makes every $\operatorname{argmin}$ all of $\mathbb R^n$), would trivialize or change the statements; the definitions above rule both out.

Contributions are welcome on any milestone. Proposition 3.1 (Kuratowski–Ryll-Nardzewski for $\mathbb R^m$-valued multifunctions) and Proposition 3.3 (deterministic epi-convergence facts) are independent of the probabilistic setting and reusable beyond this mission.

Selected references

• J. Dupačová, R. Wets, Asymptotic Behavior of Statistical Estimators and Optimal Solutions for Stochastic Optimization Problems, IIASA Working Paper WP-86-41, 1986. https://pure.iiasa.ac.at/id/eprint/2818/ — journal version: Ann. Statist. 16(4), 1517–1549, 1988. https://doi.org/10.1214/aos/1176351052
• A. Wald, Note on the consistency of the maximum likelihood estimate, Ann. Math. Statist. 20, 595–601, 1949. https://doi.org/10.1214/aoms/1177729938
• P. J. Huber, The behavior of maximum likelihood estimates under nonstandard conditions, Proc. Fifth Berkeley Symp. Math. Statist. Probab. 1, 221–233, 1967. https://projecteuclid.org/euclid.bsmsp/1200512988
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998 (Ch. 7 epi-convergence; Ch. 14 measurable multifunctions and normal integrands). https://doi.org/10.1007/978-3-642-02431-3

Why the shadow of a perturbed polytope matters

The simplex method solves linear programs very fast in practice, yet for most pivot rules there are inputs on which it takes exponentially many steps (Klee and Minty, 1972, for Dantzig's rule; Goldfarb, 1983, for the shadow-vertex rule). Average-case analyses (Borgwardt, 1980s; Smale, 1983) explained good behaviour on random inputs, but random inputs look nothing like real ones. Spielman and Teng introduced smoothed analysis to close this gap: the input is chosen by an adversary and then perturbed by a small Gaussian, and the running time is measured in expectation over the perturbation. They proved that the shadow-vertex simplex method has smoothed complexity polynomial in the number of constraints $n$, the dimension $d$ and $1/\sigma$ (Spielman–Teng, J. ACM 2004; this mission follows the preprint arXiv:cs/0111050v7). The work received the Gödel Prize (2008) and the Fulkerson Prize (2009).

Timeline. Borgwardt (1977–1987) bounded the expected number of shadow-vertex pivots for rotationally symmetric random data. Spielman and Teng (2001, STOC; journal 2004) proved the first smoothed bound, with a shadow bound of order $nd^3/\sigma^6$ — the theorem of this mission. Deshpande and Spielman (FOCS 2005) improved the shadow bound, Vershynin (2009) reduced the dependence on $n$ to polylogarithmic, and Dadush and Huiberts (STOC 2018) obtained $O(d^2\sqrt{\log n}\,\sigma^{-2})$ for small $\sigma$.

Setting

Fix $d\ge3$ and $n>d$. The data are vectors $a_1,\dots,a_n\in\mathbb R^d$, the constraint vectors of the linear program $\max\langle z|x\rangle$ subject to $\langle a_i|x\rangle\le1$ for all $i$. Each $a_i$ is a Gaussian of standard deviation $\sigma$ centered at a point $\bar a_i$ with $\|\bar a_i\|\le1$: it has density

$$\mu_i(a)=\Big(\tfrac{1}{\sqrt{2\pi}\,\sigma}\Big)^d e^{-\|a-\bar a_i\|^2/2\sigma^2},$$

and the $a_i$ are independent (joint density $\prod_i\mu_i(a_i)$).

For a direction $q\in\mathbb R^d$, $\mathrm{optSimp}_q(a_1,\dots,a_n)$ is the set of index sets $I\subseteq\{1,\dots,n\}$ with $|I|=d$ such that $(a_i)_{i\in I}$ is linearly independent, the simplex $\triangle(A_I)=\mathrm{ConvHull}(a_i:i\in I)$ is a facet of $\mathrm{ConvHull}(0,a_1,\dots,a_n)$, and $q$ lies in the cone $\{\sum_{i\in I}\alpha_ia_i:\alpha_i\ge0\}$. In polar terms, $I$ is the set of tight constraints at the vertex of the feasible polyhedron that maximizes $\langle q|x\rangle$.

For linearly independent $t,z$, the shadow $\mathrm{Shadow}_{t,z}(a_1,\dots,a_n)$ is the set of index sets $I$ that belong to $\mathrm{optSimp}_q$ for some nonzero $q\in\mathrm{Span}(t,z)$. Its size is the number of vertices of the projection of the feasible polyhedron onto the plane $\mathrm{Span}(t,z)$; the shadow-vertex method walks along this polygon, one pivot per vertex. Finally

$$\mathcal D(n,d,\sigma)=\frac{58{,}888{,}678\,nd^3}{\min\big(\sigma,\,1/(3\sqrt{d\ln n})\big)^6}.$$

Formalization targets

Goal: Theorem 4.0.1 (Shadow Size)

$$\mathbb E_{a_1,\dots,a_n}\big[\,|\mathrm{Shadow}_{t,z}(a_1,\dots,a_n)|\,\big]\le\mathcal D(n,d,\sigma)$$

for every $d\ge3$, $n>d$, every pair of linearly independent $t,z$, every $\sigma>0$ and all centers of norm at most $1$.

Milestones

The milestones follow the paper's proof, leaves first.

• Probability tools: the chi-square bound (Corollary 2.4.6), the combination lemma (Lemma 2.3.5), almost polynomial densities (Lemma 2.3.7), and comparing Gaussian tails (Lemma 2.4.11).
• Reduction: the measure of the event $P=\{\|a_i\|\le2\ \forall i\}$ (Proposition 4.0.5), and the discretization of the shadow into $m$ equally spaced directions (Lemma 4.0.6).
• Angle bound: the probability, conditioned on $P$, that the ray through a fixed unit vector $q$ passes within angle $\varepsilon$ of the boundary of its optimal facet is $O(nd^3\varepsilon/\sigma^6)$ (Lemma 4.0.7, from Lemma 4.0.11).
• Distance and incidence: in Blaschke coordinates $a_i=R_\omega b_i+sq$, a deterministic split (Lemma 4.0.12), a distance bound (Lemmas 4.1.1–4.1.3) and an angle-of-incidence bound (Lemmas 4.2.1–4.2.3).

Significance

The result. Theorem 4.0.1 is the geometric heart of the smoothed analysis of the simplex method. Section 4.3 of the paper extends it to arbitrary centers, covariances and right-hand sides, and Section 5 combines these extensions with a two-phase method to show that the simplex method has polynomial smoothed complexity. The same shadow bound underlies later analyses of the simplex method, of perturbed polytopes' diameters, and of condition numbers of random linear programs.

Formalizing it. The theorem has been proved, and improved constants are known, but none of this is machine-checked. A formal proof would verify a long and delicate argument: a change of variables of integral geometry (Blaschke's formula), several conditional-density estimates, and explicit constants in the millions. The mission also produces reusable statements about Gaussian vectors and convex hulls of random points.

Difficulty

The obvious approach is to count, for each candidate facet $I$, the probability that $I$ appears in the shadow; there are $\binom nd$ candidates, so a union bound is exponential in $d$. The paper avoids this by discretizing the angle of $q$ (Lemma 4.0.6) and bounding, for each fixed direction, the probability that the optimal facet changes within a small angular step. That needs a lower bound on the angle between $q$ and the boundary of its optimal facet, conditioned on the facet being optimal. The conditioning changes the distribution of $a_1,\dots,a_d$, so the bound cannot come from the Gaussian density alone. The proof changes variables to the facet's normal $\omega$, offset $s$ and in-plane coordinates $b_i$ (Corollary 2.5.3), whose Jacobian contributes the factors $\langle\omega|q\rangle$ and $\mathrm{Vol}(\triangle(b))$. It then shows that both the distance of the origin to a face of the in-plane simplex and the angle of incidence $\langle\omega|q\rangle$ are unlikely to be small. Measure-theoretic bookkeeping is as hard as the geometry: densities known only up to normalization, conditioning on events of positive measure, and the measure-zero degeneracies the paper sets aside.

Formalization scope

Points live in EuclideanSpace ℝ (Fin d). Constraint vectors are indexed by Fin n (0-based), so the paper's $\{1,\dots,d\}$ is $\{i:i<d\}$. The Gaussian of standard deviation $\sigma$ centered at $c$ is Lebesgue measure with the density above, and the joint law is the product measure. Lemma 4.0.6 also uses Mathlib's multivariateGaussian with a positive definite covariance. Expectations of shadow sizes are lower Lebesgue integrals of $[0,\infty]$-valued counts, and their measurability is part of each conclusion. "Density proportional to $\nu$" and conditional probabilities are stated cross-multiplied, $\int_{E}\nu\le\text{bound}\cdot\int\nu$, so no $0/0$ appears.

The shadow is the set of index sets $I$, and the direction $q=0$ is excluded. Including it would add every facet of $\mathrm{ConvHull}(0,a_1,\dots,a_n)$ to the shadow, since $0$ lies in every cone, and make the goal false. $\mathrm{ang}(q,\emptyset)=\infty$ is represented exactly in $[0,\infty]$, never by a real infimum. Where the paper omits a hypothesis it uses, it is added and recorded in the item: the standing assumptions $d\ge3$, $n>d$ and $\sigma\le1/(3\sqrt{d\ln n})$ (Lemma 4.2.3 is false without a bound on $\sigma$), unit length of the reference vector $q$, $s\ge0$, and $\varepsilon>0$ for strict inequalities. Lemma 2.3.7 is stated with $\le$ rather than the page's $<$, which fails in an edge case.

Infrastructure a complete development needs: Gaussian tail and chi-square estimates; faces and facets of convex hulls; the Blaschke change of variables and the latitude–longitude change of variables on the sphere (not in Mathlib); surface measure on $S^{d-1}$ (Mathlib's Measure.toSphere); and the disintegration of the joint law used in the combination lemma. The Gaussian estimates, the combination lemma and the Blaschke formula are useful beyond this mission. Proofs of any milestone, and of supporting lemmas such as the change-of-variables formulas, are welcome.

Selected references

• D. A. Spielman, S.-H. Teng, Smoothed Analysis of Algorithms: Why the Simplex Algorithm Usually Takes Polynomial Time, arXiv:cs/0111050v7, 2003. https://arxiv.org/abs/cs/0111050v7
• D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. https://doi.org/10.1145/990308.990310
• K. H. Borgwardt, The Simplex Method: A Probabilistic Analysis, Springer, 1987.
• V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, 159–175.
• A. Deshpande, D. A. Spielman, Improved smoothed analysis of the shadow vertex simplex method, FOCS 2005, 387–396.
• R. Vershynin, Beyond Hirsch conjecture: walks on random polytopes and smoothed complexity of the simplex method, SIAM J. Comput. 39(2):646–678, 2009. https://doi.org/10.1137/070683386
• D. Dadush, S. Huiberts, A friendly smoothed analysis of the simplex method, STOC 2018; arXiv:1711.05667. https://arxiv.org/abs/1711.05667

Motivation

Many statistical procedures minimize an average observed loss. This treats two candidates with the same average as equally attractive even when one has much more variable losses across the sample. Adding a multiple of the empirical standard deviation can distinguish them, but the resulting objective need not be convex even when each individual loss is convex. Duchi and Namkoong study a distributionally robust alternative: they maximize expected loss over a small neighborhood of the empirical distribution, then minimize that worst-case value. Their paper identifies when this convex robust value agrees exactly with the mean-plus-standard-deviation expression and how far apart the two can be otherwise. The finite-sample statement is Theorem 1 of the pinned preprint.

The relation matters to someone choosing a loss function for stochastic optimization. The variance expression has a direct statistical interpretation, while the robust expression preserves convexity in a decision parameter when the loss is convex. Theorem 1 makes the relationship quantitative for a single bounded random variable, before the paper turns to uniform guarantees over whole classes of losses. This mission isolates that first step and its finite optimization model.

Setting

Take observed real values $z_1,\ldots,z_n$, with $n\ge1$. Their empirical mean and empirical variance are

$$\bar z=\frac1n\sum_{i=1}^n z_i,\qquad s_n^2=\frac1n\sum_{i=1}^n z_i^2-\bar z^2.$$

The variance uses $1/n$, not the unbiased-estimator factor $1/(n-1)$. A weight vector $p=(p_1,\ldots,p_n)$ is feasible when its entries are nonnegative, sum to one, and satisfy

$$\frac12\sum_{i=1}^n(np_i-1)^2\le\rho,\qquad \rho\ge0.$$

This is the paper's χ² neighborhood $\mathcal P_n(\rho)$ of the uniform empirical weights. Its robust sample expectation is

$$R_n(z,\rho)=\sup_{p\in\mathcal P_n(\rho)}\sum_{i=1}^n p_i z_i.$$

For a random variable $Z$ with law $P$ supported on $[M_0,M_1]$, write $M=M_1-M_0$ and $\sigma^2=\operatorname{Var}_P(Z)$. An independent sample $Z_1,\ldots,Z_n$ supplies the vector $z$. The paper describes $\mathcal P_n$ through a $\phi$-divergence from the empirical distribution, with $\phi(t)=\tfrac12(t-1)^2$; its finite maximization problem (8) is the weight-vector form used here. The preprint, pp. 2 and 5–7 fixes these conventions.

Formalization targets

Deterministic bound

For every sample in $[M_0,M_1]$, the robust value lies between the empirical mean plus a corrected variance penalty and the full penalty:

$$\left(\sqrt{\frac{2\rho s_n^2}{n}}-\frac{2M\rho}{n}\right)_+\le R_n(z,\rho)-\bar z\le\sqrt{\frac{2\rho s_n^2}{n}}.$$

This is inequality (10). The correction is explicit, so this target records more than an asymptotic approximation.

Exact expansion

When $\sigma^2>0$ and the sample size obeys

$$n\ge\max\left\{5,\frac{M^2}{\sigma^2}\max\{8\sigma,44,44\rho\}\right\},$$

the goal is the high-probability equality

$$\Pr\left\{R_n(Z_{1:n},\rho)\ne\bar Z+\sqrt{\frac{2\rho s_n^2}{n}}\right\}\le\exp\left(-\frac{n\sigma^2}{11M^2}\right).$$

This is Theorem 1's equality (11) with the missing $\rho$-dependent sample-size requirement supplied from the proof. The exact expansion is the mission goal; display (30), inequality (10), and Lemma A.2 form the milestone list, and the exact value under condition (9) is a further statement of the mission.

Significance

The deterministic result states how large the discrepancy between a convex robust risk and a variance penalty can be for any bounded sample. The equality says that, with the stated confidence, no discrepancy remains once the population variance and sample size make the penalty compatible with nonnegative probability weights. These are the numerical facts later sections need when they move from one loss variable to families of losses and minimizers. The claims and constants come from Theorem 1 and Section 2.1.

The paper develops arguments for these results, although its printed (11) needs the correction described below; the statements in this mission have no machine-checked proofs yet. The formalization work includes the finite χ² feasible set, its real supremum, exact handling of tied observations, empirical moments with the paper's normalization, and a product-law event for the probability estimate. The Samson concentration milestone is reusable for other bounded independent-coordinate models. Solvers can also contribute a different route to the corrected exact expansion; the goal concerns the statement, not one chosen argument.

Difficulty

Without the nonnegativity requirement on $p$, optimizing a linear function over the centered Euclidean ball gives the mean plus a standard-deviation term. The candidate weights can become negative when a sample coordinate is far below the mean, so that calculation alone cannot certify the robust value. Condition (9) records precisely when the candidate is feasible. The probability target then needs a quantitative guarantee that the sample variance is large enough often enough, with the stated exponential constant. A pointwise inequality for a fixed sample does not by itself yield that probability estimate. These are separate obligations in Section 2.1 and Appendix A.

Formalization scope

The sample is a function Fin n → ℝ; feasible weights have the same type. chiSqBall, robustSup, empMean, and empVar mirror equations (8) and the definitions on p. 6. Every theorem assumes $n>0$ and $\rho\ge0$, so the weight ball is nonempty and its real supremum is bounded. The high-probability theorem uses a probability measure $P$ on the reals, supported on $[M_0,M_1]$, and the independent product measure on Fin n → ℝ. Its conclusion bounds the measure of the event on which equality fails. The positive population variance hypothesis makes division by $\sigma^2$ and $M^2$ meaningful. The deterministic bounds include every sample in the interval and use $x_+=\max\{x,0\}$.

The paper prints the threshold without $44\rho$ in (11), but its Appendix A invokes the corresponding inequality, and the printed claim fails for sufficiently large $\rho$. The goal includes that term. The paper's route through Lemmas A.1 and A.4 contains misprinted lower-tail and moment claims, so those are not milestones. Lemma A.3's displayed (31b) is also omitted because its correction term has the wrong scaling; the corrected goal stands as a target to establish independently. These discrepancies are detailed in the local moderation notes and the pinned source, pp. 7 and 32–35.

No hypothesis may force the bad event to be empty, and the robust value must optimize over all feasible weights, not a selected optimizer. The supporting definitions are intended for reuse in later missions on uniform variance expansions. Contributions to the finite optimization facts, the concentration statement, and the probability goal are welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv preprint arXiv:1610.02581v3, 2017. Pinned preprint.

Motivation

Most physical supply chains hold stock at several levels: a factory warehouse feeds a regional depot, which feeds a retail outlet. Each level orders from the one above it, and a shortage upstream delays replenishment downstream. Optimizing such a multi-echelon system by dynamic programming looks hopeless, because the state is a vector of stock levels and stock in transit at every installation, and the value function of a two-installation system with a two-period shipping lag already depends on three continuous variables.

Andrew J. Clark and Herbert Scarf (Management Science 6(4):475–490, 1960) showed that for a serial system this curse of dimensionality disappears. Working with echelon stock (the stock at a level plus everything below it or in transit to a lower level), the optimal system cost separates into the cost of the lowest installation, optimized as if it stood alone, plus a function of echelon stock only. The result is the foundation of multi-echelon inventory theory: the echelon base-stock policies used in practice, the stationary analyses of Federgruen and Zipkin (1984) and Chen and Zheng (1994), and textbook treatments (Zipkin, Foundations of Inventory Management, 2000; Snyder and Shen, Fundamentals of Supply Chain Theory) all descend from it.

Timeline. Arrow, Harris and Marschak (1951) and Arrow, Karlin and Scarf (1958) set up periodic-review inventory models with discounted costs. Karlin and Scarf (1958) treated a single installation with a delivery lag, reducing it to a problem without lag (the paper's facts 1–3). Clark and Scarf (1960) proved the decomposition for serial systems with linear shipping costs and a setup cost permitted only at the top. Federgruen and Zipkin (1984) extended it to infinite horizons and Chen and Zheng (1994) gave a lower-bound proof that reaches more general structures.

Setting

Two installations are in series. Customer demand occurs only at installation 1; its demand in each period is non-negative with density $\varphi$ on $(0,\infty)$, independent across periods, and excess demand is backlogged. Installation 2 ships to installation 1 with a two-period lead time at unit cost $c_1\ge0$. The system orders $z\ge0$ units from outside at cost $c(z)=K+cz$ for $z>0$ and $c(0)=0$ (eq. (5)); these arrive at installation 2 one period later. Costs $n$ periods ahead are discounted by $\alpha^n$, $\alpha\ge0$.

The state at the start of a period is $(x_1,w_1,x_2)$: $x_1$ is the stock on hand at installation 1, $w_1$ the stock that reaches installation 1 next period, and $x_2$ the echelon-2 stock (on hand at both installations plus in transit), so $x_1+w_1\le x_2$. Installation 1 pays the expected holding and shortage cost (1),

$$L(x)=\begin{cases}hx+p\int_x^\infty(t-x)\varphi(t)\,dt,&x>0,\\ p\int_0^\infty(t-x)\varphi(t)\,dt,&x\le0,\end{cases}$$

and echelon 2 pays a natural one-period cost $\tilde L(x_2)$ (Assumption 3).

With $n$ periods remaining, the optimal system cost $C_n(x_1,w_1,x_2)$ satisfies, with $C_0\equiv0$,

$$C_n(x_1,w_1,x_2)=\min_{\substack{x_1+w_1\le y\le x_2\\0\le z}}\Big\{c(z)+c_1(y-x_1-w_1)+\tilde L(x_2)+L(x_1)+\alpha\int_0^\infty C_{n-1}(x_1+w_1-t,\,y-x_1-w_1,\,x_2+z-t)\varphi(t)\,dt\Big\}\qquad(14)$$

where $y$ is installation 1's target (stock on hand plus in transit after shipping). Installation 1 in isolation, buying at unit cost $c_1$ with a two-period lag, has optimal cost $\hat C_n(x_1,w_1)$, $\hat C_0\equiv0$:

$$\hat C_n(x_1,w_1)=\min_{y\ge x_1+w_1}\Big\{c_1(y-x_1-w_1)+L(x_1)+\alpha\int_0^\infty\hat C_{n-1}(x_1+w_1-t,\,y-x_1-w_1)\varphi(t)\,dt\Big\}.\qquad(15)$$

In Lean these are ClarkScarf.Serial.Model.sysCost and isoCost; the expressions in braces are sysObj and isoObj, indexed by $n$ for the problem with $n+1$ periods remaining.

Formalization targets

Goal: Theorem 1 (p. 482)

There are functions $g_n$ with $g_1=\tilde L$ such that, for all $n\ge1$ and $x_1+w_1\le x_2$,

$$C_n(x_1,w_1,x_2)=\hat C_n(x_1,w_1)+g_n(x_2),\qquad(16)$$

and installation 1 acts optimally by aiming at an isolated-optimal target $\hat y$ and taking $\min(x_2,\hat y)$, as much as installation 2 can supply. The goal fixes no form for $g_n$ and needs no critical numbers.

Milestones

1. Convexity of $y\mapsto\alpha\int\!\!\int L(y-t_1-t_2)\varphi(t_1)\varphi(t_2)$ (§2 item 2, p. 478).
2. The isolated decomposition $\hat C_n(x_1,w_1)=L(x_1)+\alpha\int_0^\infty L(x_1+w_1-t)\varphi(t)\,dt+f_n(x_1+w_1)$ for $n\ge2$, with $f_n$ of (7) (p. 480).
3. Convexity of every $f_n$ (§2 item 3, p. 478).
4. Eqs. (18)–(19) (p. 483): the system cost when echelon-2 stock is above or below the isolated critical number $\bar x_n$.
5. Eqs. (21)–(25) (pp. 483–484): the shortfall cost $\Lambda_n$ depends on $x_2$ alone,

$$\Lambda_n(x_2)=c_1(x_2-\bar x_n)+\alpha^2\int_0^\infty\!\!\int_0^\infty[L(x_2-t-y)-L(\bar x_n-t-y)]\varphi(t)\varphi(y)\,dy\,dt+\alpha\int_0^\infty[f_{n-1}(x_2-t)-f_{n-1}(\bar x_n-t)]\varphi(t)\,dt.$$

6. Theorem 2 (p. 484), the explicit form: given critical numbers, $g_n$ is computed by (26), $g_n(x_2)=\min_{z\ge0}\{c(z)+\tilde L(x_2)+\Lambda_n(x_2)+\alpha\int g_{n-1}(x_2+z-t)\varphi(t)\,dt\}$.

Significance

The result. Theorem 1 replaces one three-dimensional dynamic program by two one-dimensional ones. Installation 1 solves its own problem (15), whose solution is a critical-number policy, and echelon 2 solves a single-installation problem in $x_2$ with one-period cost $\tilde L+\Lambda_n$. When $\tilde L$ is convex the augmented cost is convex (the paper remarks this for Expression (10)), so the echelon-2 policy is of $(S,s)$ type by Scarf's theorem, and the whole system runs on echelon base-stock rules. Every later serial-system result, finite or infinite horizon, uses this decomposition or its proof idea, and the "induced penalty" $\Lambda_n$ is the prototype of the penalty functions used in the multi-echelon literature.

Formalizing it. The theorem is classical and proved, but no machine-checked version exists. The published platform items on Clark–Scarf are a stationary single-period decomposition with normal demand and a disproved infinite-horizon base-stock recursion, neither of which is this finite-horizon dynamic program. A formal development produces the value functions (14)–(15) with real infima and set integrals, the measurability and integrability of value functions defined by infima, the convexity propagation through the recursion (7), and the decomposition itself, which are reusable for any finite-horizon inventory recursion with lead times.

Difficulty

The obvious induction on $n$ substitutes (16) into (14) and separates the minimizations over $y$ and $z$. The separation is immediate; the hard step is that the constrained minimum over $x_1+w_1\le y\le x_2$ differs from the unconstrained one by an amount that a priori depends on $(x_1,w_1)$. Showing that it depends on $x_2$ alone is the content of Theorem 1; nothing in the separation step itself rules out a dependence on $(x_1,w_1)$. On the measure-theoretic side, every value function is defined by an infimum over an uncountable set and then integrated against $\varphi$. Its measurability and integrability are not automatic, and they must be established before any identity between integrals can be manipulated.

Formalization scope

Everything lives in ClarkScarf.Serial, one definition file Def_ClarkScarf_Serial_Model and seven theorem files. Conventions committed to:

• The model is a structure Model whose fields carry the data and the standing hypotheses: $h,p,\alpha,c_1,K,c\ge0$; $\varphi\ge0$ with $\int_0^\infty\varphi=1$; and two additions the page leaves implicit, disclosed in each statement: a finite demand mean (otherwise (1) is infinite for $x\le0$) and $\tilde L$ non-negative, continuous and of at most linear growth (Assumption 3 leaves $\tilde L$ unspecified; these make every expectation in (14) finite and measurable). No discount bound $\alpha<1$, no convexity of $\tilde L$, no $K=0$ and no sign condition on $w_1$ is assumed.
• Expectations are set integrals $\int_{(0,\infty)}F(t)\varphi(t)\,dt$; "Min" is a real infimum over a nonempty feasible set of a non-negative objective.
• Every statement about $C_n$ is restricted to the state domain $x_1+w_1\le x_2$; outside it the feasible set of (14) is empty.
• The horizon index counts periods remaining, $C_0\equiv\hat C_0\equiv0$, and $f_n\equiv0$ for $n\le2$.

A formalization in which the feasible set of (14) is empty, in which the expectations are junk zeros of non-integrable integrands, or in which $g_n$ may depend on $(x_1,w_1)$ would make (16) trivial; the domain restriction, the integrability conditions and the order $\exists g\,\forall x_1,w_1,x_2$ rule these out. A sorry-free check (not part of the mission) verifies $C_1=L(x_1)+\tilde L(x_2)$ and $\hat C_1=L(x_1)$ and exhibits a model with exponential demand satisfying all hypotheses.

Needed infrastructure: Fubini-type rearrangement of iterated set integrals against a density, integrability of functions of linear growth against a finite-mean density, convexity preserved under infimal projection $u\mapsto\inf_{y\ge u}$ and under convolution with a density, and measurability of infimum-defined functions. Contributions of these general lemmas, of the base cases $n=1,2$, and of any milestone are welcome.

Selected references

• A. J. Clark and H. Scarf, Optimal Policies for a Multi-Echelon Inventory Problem, Management Science 6(4):475–490, 1960. https://doi.org/10.1287/mnsc.6.4.475
• S. Karlin and H. Scarf, Inventory Models of the Arrow-Harris-Marschak Type with Time Lag, in Arrow, Karlin, Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• A. Federgruen and P. Zipkin, Computational Issues in an Infinite-Horizon, Multiechelon Inventory Model, Operations Research 32(4):818–836, 1984. https://doi.org/10.1287/opre.32.4.818
• F. Chen and Y.-S. Zheng, Lower Bounds for Multi-Echelon Stochastic Inventory Systems, Management Science 40(11):1426–1443, 1994. https://doi.org/10.1287/mnsc.40.11.1426

Motivation

Long-running projects such as construction, plant engineering or software development involve payments to and from the contractor at many points in time: disbursements when activities are carried out, progress payments when milestones are reached. When the planning horizon is long, money received later is worth less, and the natural financial objective is the net present value of all cash flows. Scheduling a project to maximize its net present value subject to minimum and maximum time lags was studied by Russell (1970) and Grinold (1972), and the problem is the prototype of a nonregular objective: delaying an activity can be profitable, because disbursements lose value when they are postponed.

This mission follows Chapter 3 of Neumann, Schwindt and Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). The book shows that the net present value objective belongs to the class of binary-monotone objective functions (§3.3.5), and it uses this in §3.9.1 to give a combinatorial optimality criterion for the resource-free problem: a vertex schedule is optimal exactly when the subprojects cut off by the arcs of a spanning tree have net present values of the right sign (Proposition 3.9.2). That criterion drives the book's parametric analysis of the net present value as a function of the discount rate and the deadline.

Setting

A project consists of activities $V=\{0,1,\dots,n+1\}$, $n\ge1$, where $0$ is the project beginning and $n+1$ the project completion. Activity $i$ has an integer duration $p_i$, with $p_0=p_{n+1}=0$ and $p_i>0$ otherwise. Temporal constraints are the arcs of a project network $N=\langle V,E;\delta\rangle$: an arc $\langle i,j\rangle$ with integer weight $\delta_{ij}$ requires $S_j-S_i\ge\delta_{ij}$ for the start times $S_i$. A maximum project duration $\bar d$ is the arc $\langle n+1,0\rangle$ with weight $-\bar d$. The time-feasible region is

$$\mathcal S_T=\{S\in\mathbb R^{n+2}_{\ge0}\mid S_0=0,\ S_j-S_i\ge\delta_{ij}\ (\langle i,j\rangle\in E)\}.$$

Let $0<\beta\le1$ be the discount rate ($\beta=1/(1+I)$ for an interest rate $I$) and $c_i^F\in\mathbb R$ the cash flow of activity $i$, paid at its completion time $C_i=S_i+p_i$. The problem (3.9.1) is

$$\text{minimize } f(S)=-\sum_{i\in V}c_i^F\beta^{S_i+p_i}\quad\text{subject to } S\in\mathcal S_T,$$

and a minimizer is a time-optimal schedule. A vertex of $\mathcal S_T$ is an extreme point. A spanning tree $G=\langle V,E^G\rangle$ is associated with $S$ if $E^G\subseteq E$, $E^G$ has $n+1$ arcs and a connected underlying undirected graph, and $S$ is the unique solution of $S_0=0$, $S_j-S_i=\delta_{ij}$ for $\langle i,j\rangle\in E^G$. Deleting a tree arc $\langle i,j\rangle$ splits $G$ into two subtrees; $V_{ij}$ is the node set of the one not containing $0$. The arc is forward if the tree path from $0$ passes it from $i$ to $j$ and backward otherwise, and

$$npv^{ij}(S)=\sum_{h\in V_{ij}}c_h^F\beta^{S_h+p_h}$$

is the net present value of the subproject $V_{ij}$. Finally, $f$ is binary-monotone if it is monotone on every line $\{S+\lambda z\ge0\mid\lambda\in\mathbb R\}$ with direction $z\in\{0,1\}^{n+2}$ (Definition 3.3.2).

Formalization targets

Goal: Proposition 3.9.2, pinned reading

Assume every node is reached from $0$ by a path of nonnegative length (the standing convention of §1.2) and let $S$ be a vertex of $\mathcal S_T$.

$$\text{(sufficiency)}\quad G \text{ associated with } S,\ \ npv^{ij}(S)\ge0 \text{ on forward arcs},\ npv^{ij}(S)\le0 \text{ on backward arcs}\ \Longrightarrow\ S \text{ time-optimal};$$ $$\text{(necessity, } \beta<1)\quad S \text{ time-optimal}\ \Longrightarrow\ \exists\, G \text{ associated with } S \text{ satisfying the sign conditions}.$$

The book states "if and only if … for each arc of the corresponding spanning tree", where the corresponding tree is chosen using optimality. The two directions above are the reading that makes the statement well defined: sufficiency for every associated tree, necessity for some associated tree.

Milestones

1. §3.3.5: the net present value objective is binary-monotone and sum-separable.
2. §3.9.1: if $\mathcal S_T$ is nonempty and bounded, some vertex of $\mathcal S_T$ is time-optimal.
3. Proposition 3.2.16: every vertex of $\mathcal S_T$ has an associated spanning tree, an outtree rooted at $0$ if the vertex is a minimal point.
4. Proposition 3.5.4: a directed forest with at least one node has a source with at most one successor or a sink with exactly one predecessor.

Significance

Proposition 3.9.2 turns a nonconvex continuous optimization problem into a finite check on a spanning tree. Read as an economic statement, it says that at an optimal schedule no subproject with positive net present value can be started earlier and no subproject with negative net present value can be postponed. The book builds on it the parametric procedure of §3.9.1, which tracks the optimal tree as the discount rate or the deadline varies (Propositions 3.9.3 and 3.9.4), and the steepest descent method of §3.5.2 terminates exactly when the criterion holds.

The results are proved in the book, partly by reference to network optimization (Ahuja et al., 1993) and to Schwindt and Zimmermann (2001, 2002). None of them is formalized on the platform or, as far as is known, anywhere else. A formal proof would give the first machine-checked optimality certificate for a nonregular project scheduling objective, and the spanning-tree description of vertices (Proposition 3.2.16) is shared with Mission VI of this series.

Difficulty

The objective $f$ is neither convex nor concave when cash flows of both signs occur, so local optimality at a vertex does not imply global optimality by a convexity argument, and a first-order check along the edges of $\mathcal S_T$ is not obviously enough. The criterion is also not a statement about one tree: a degenerate vertex, where more than $n+1$ temporal constraints are binding, has several associated trees, and the sign conditions may hold on some and fail on others. Necessity therefore requires producing a suitable tree, not checking a given one. Finally, the combinatorial objects (the subtree $V_{ij}$, forward and backward orientation relative to the root) have to be connected to the geometry of $\mathcal S_T$ through Proposition 3.2.16, whose proof in the book is a citation.

Formalization scope

Activities are Fin (n + 2) with 0 the project beginning and Fin.last (n+1) the project completion; start times are real; durations are natural numbers and arc weights integers. The deadline is a structure field together with the backward arc $\langle n+1,0\rangle$ of weight $-\bar d$. $\beta^x$ is Real.rpow, and every statement assumes $0<\beta\le1$ as the book does (p. 203). Vertices are Set.extremePoints ℝ. A spanning tree is a Finset of $n+1$ arcs whose SimpleGraph.fromRel is connected; $V_{ij}$ is the set of nodes not reachable from $0$ once the arc is deleted.

Three readings are committed and disclosed in the item statements. Necessity is stated only for $\beta<1$: at $\beta=1$ the objective is constant, every schedule is optimal, and the sign conditions can fail on every tree. The standing convention of §1.2 (a path of nonnegative length from $0$ to every node) is a hypothesis of Proposition 3.2.16 and of the goal; without it a vertex can be fixed by $S_i\ge0$ rather than by arcs of $N$, and necessity fails. The existence of an optimal vertex assumes $\mathcal S_T$ nonempty and bounded, which the book asserts in §3.1. Chapter 3's resource constraints do not occur in this mission, which concerns $PS\infty|temp,\bar d|f$ only.

The goal cannot be discharged by choosing the tree freely: associated trees must consist of arcs of $N$ that are binding at $S$ and determine $S$ uniquely, and sufficiency must hold for every such tree. Contributions welcome beyond the milestones: a proof of Proposition 3.2.16 reusable by Mission VI, and a general lemma relating binding spanning trees of difference constraints to extreme points.

Selected references

• K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §3.1 (p. 203), §3.3.5 (pp. 224–225), §3.5.2 (p. 252), §3.9.1 (pp. 333–334). https://doi.org/10.1007/978-3-540-24800-2
• A. H. Russell, "Cash flows in networks", Management Science 16 (1970), 357–373. https://doi.org/10.1287/mnsc.16.5.357
• R. C. Grinold, "The payment scheduling problem", Naval Research Logistics Quarterly 19 (1972), 123–136.
• C. Schwindt, J. Zimmermann, "A steepest ascent approach to maximizing the net present value of projects", Mathematical Methods of Operations Research 53 (2001), 435–450.
• C. Schwindt, J. Zimmermann, "Parametrische Optimierung als Instrument zur Bewertung von Investitionsprojekten", Zeitschrift für Betriebswirtschaft 72 (2002), 593–617.
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows, Prentice Hall, 1993.
• C. Berge, Graphs and Hypergraphs, North-Holland, Amsterdam, 1976.

Motivation

The Pontryagin maximum principle is the basic first-order necessary condition of optimal control: along an optimal control, the control value at almost every time extremizes a Hamiltonian built from the dynamics and an adjoint vector. The classical statement presupposes that an optimal control exists. For many problems none does: the set of trajectories is not closed, or the cost does not attain its infimum, and the classical principle then says nothing.

Ekeland's 1974 paper On the Variational Principle (DOI 10.1016/0022-247X(74)90025-0) proves a general result about lower semicontinuous functions on complete metric spaces (its Theorem 1.1, now called Ekeland's variational principle) and closes with an application to control theory in §7 (pp. 348–351): for every terminal-cost problem satisfying mild regularity and growth conditions, there are ε-optimal controls that satisfy the maximum principle up to ε, whether or not an optimal control exists. The argument equips the measurable controls with the metric "measure of the set where two controls differ", which has since become a standard device in nonsmooth and approximate optimal control. For the classical theory, Ekeland refers to the treatise of Pallu de la Barrière (Optimal Control Theory, Saunders, 1967).

Setting

Fix $n \ge 0$, a horizon $T > 0$, an initial state $x_0 \in \mathbb R^n$, and a nonempty compact metrizable space $K$ of control values, with its Borel σ-algebra. A control is a measurable map $u : [0, T] \to K$. The dynamics are a map $f : \mathbb R^n \times K \times [0, T] \to \mathbb R^n$, and the state obeys

$$\frac{dx}{dt}(t) = f(x(t), u(t), t) \ \text{ a.e.}, \qquad x(0) = x_0. \qquad (7.1)$$

A trajectory of $u$ (Lean: IsTrajectory f x₀ T u x) is a function $x$ continuous on $[0, T]$ with $x(t) = x_0 + \int_0^t f(x(s), u(s), s)\,ds$ for all $t \in [0, T]$. The standing hypotheses are:

• (a) $f$ and its state Jacobian $f_x' = (\partial f/\partial x_1, \dots, \partial f/\partial x_n)$ (Lean: fx) are continuous on $\mathbb R^n \times K \times [0, T]$;
• (b) $\langle x, f(x, u, t)\rangle \le c\,(1 + \|x\|^2)$ for some constant $c$.

The terminal cost is given by a $C^1$ function $g : \mathbb R^n \to \mathbb R$, and the problem is to minimize $g(x(T))$ over all controls. The adjoint vector $p$ along a pair $(u, x)$ (Lean: IsAdjoint fx g T u x p) solves the linear equation

$$\frac{dp}{dt}(t) = -{}^t f_x'(x(t), u(t), t)\, p(t), \qquad p(T) = g'(x(T)),$$

where ${}^t A$ is the transpose. The control distance (Lean: ctrlDist T u₁ u₂) is

$$\delta(u_1, u_2) = \operatorname{meas}\{t \in [0, T] \mid u_1(t) \neq u_2(t)\},$$

and the needle variation $v_\tau$ of a control $u_\varepsilon$ at $t_0$ with value $u_0 \in K$ (Lean: needle T uε u₀ t₀ τ) equals $u_0$ on $[0, T] \cap\, ]t_0 - \tau, t_0[$ and $u_\varepsilon$ elsewhere.

Formalization targets

Goal: Theorem 7.1

For every $\varepsilon > 0$ there is a control $u_\varepsilon$ with trajectory $x_\varepsilon$ and adjoint vector $p_\varepsilon$ such that

$$g(x_\varepsilon(T)) \le \inf_u g(x(T)) + \varepsilon, \qquad \langle f(x_\varepsilon(t), u_\varepsilon(t), t), p_\varepsilon(t)\rangle \le \min_{w \in K} \langle f(x_\varepsilon(t), w, t), p_\varepsilon(t)\rangle + \varepsilon \ \text{ a.e. on } [0, T].$$

Milestones

1. (7.2), a priori bound: every trajectory satisfies $\|x(t)\|^2 \le (\|x_0\|^2 + 2cT)e^{2cT}$.
2. Well-posedness (p. 348): every control has exactly one trajectory on $[0, T]$.
3. Lemma 7.2: $(\mathcal U, \delta)$ is a complete metric space (on almost-everywhere classes).
4. Lemma 7.3: $u \mapsto g(x(T))$ is continuous on $(\mathcal U, \delta)$.
5. (7.15)–(7.16): a control $u_\varepsilon$ with $F(u_\varepsilon) \le \inf F + \varepsilon^2$ and $F(u) \ge F(u_\varepsilon) - \varepsilon\,\delta(u, u_\varepsilon)$ for all $u$, where $F(u) = g(x(T))$.
6. Lemma 7.4: the right derivative of $\tau \mapsto g(x_\tau(T))$ at $\tau = 0$, for the needle variations $v_\tau$, equals $\langle f(x_\varepsilon(t_0), u_0, t_0) - f(x_\varepsilon(t_0), u_\varepsilon(t_0), t_0), p_\varepsilon(t_0)\rangle$.

Significance

The result. Theorem 7.1 decouples the maximum principle from existence of optimal controls. Any minimizing sequence can be replaced by one consisting of controls that satisfy the necessary condition up to a vanishing error, so approximate extremals are available for numerical schemes and for limiting arguments (relaxation, convergence of extremals) in problems without compactness or convexity of the velocity sets. The same scheme, a complete metric on controls plus Ekeland's principle plus needle variations, underlies later proofs of the maximum principle with state constraints and in nonsmooth settings.

Formalizing it. The theorem has a published proof, which the paper sketches in four pages and partly defers to classical results (local existence for measurable controls, differentiability of trajectories with respect to needle variations). Neither Mathlib nor the platform contains this theorem or a maximum principle for measurable controls with time-dependent dynamics; the nearest platform items assume an exact optimum, a running cost and globally Lipschitz autonomous dynamics. A formalization requires a Carathéodory theory of ODEs in Lean, the complete metric space of controls, and a rigorous version of the classical first-variation computation. Each of these is useful well beyond this paper.

Difficulty

The obvious argument fails at its first step: a minimizing sequence of controls has no convergent subsequence in any useful sense, because measurable controls with values in $K$ are not compact in the metric $\delta$ and their weak limits are relaxed controls, which are not controls. Ekeland's principle avoids compactness, but it needs a complete metric space on which the cost is lower semicontinuous. Completeness of $(\mathcal U, \delta)$ (Lemma 7.2) and continuity of the cost (Lemma 7.3) both require care. Continuity must hold for trajectories driven by merely measurable controls, which converge only in measure. The needle derivative (Lemma 7.4) holds only at times where the trajectory satisfies the state equation in the classical sense, which is almost every time but not every time.

Formalization scope

• Controls are functions ℝ → K with Measurable u; only values on $[0, T]$ matter. Trajectories and adjoint vectors are functions ℝ → EuclideanSpace ℝ (Fin n), continuous on $[0, T]$ and solving the integral form of their equation. The paper uses the same form in (7.13). A definition that asks for a derivative at every time would be unsatisfiable for discontinuous controls and would make the goal vacuous; the integral form avoids this.
• Hypothesis (a) is stated as joint continuity of f and fx on univ ×ˢ univ ×ˢ Icc 0 T together with HasFDerivAt (fun y => f y u t) (fx x u t) x. Hypothesis (b) is ∃ c, … with the order of arguments $f(x, u, t)$; the page prints $f(t, x, u)$ in (b), a slip.
• The transpose ${}^t f_x'$ is ContinuousLinearMap.adjoint, and $g'(x)$ is gradient g x.
• Infima over controls are never taken as real ⨅; (7.4) and (7.15) are stated as "for every control $u$ with trajectory $x$".
• (7.5) is printed with "$\times\,\varepsilon$". The proof's last line (7.21) gives "$+\,\varepsilon$", which is what is stated. The minimum over the compact $K$ is replaced by the equivalent "for every $w \in K$", with one null set for all $w$.
• Added hypothesis: [Nonempty K] in the goal and milestone 5. With $K$ empty no control exists and the existential statements would be false.
• Lemma 7.2 is stated as the triangle inequality, "$\delta = 0$ iff almost-everywhere equality on $[0, T]$", and sequential completeness for measurable controls. Lemma 7.3 is sequential continuity. Lemma 7.4 is a one-sided derivative within $[0, t_0]$ at $0$, stated for an arbitrary measurable $u_\varepsilon$.
• Theorem 1.1 (Ekeland's principle) is a separate mission of this series and still a draft, so milestone 5 states the instance used here directly.
• Out of scope: the uniform bound (7.3) and the remark after Theorem 7.1 that one may take $\varepsilon = 0$ in (7.5) when (7.4) holds with $\varepsilon = 0$.

Welcome contributions include Carathéodory existence and uniqueness for ODEs with measurable time dependence, Gronwall-type estimates for absolutely continuous functions, the complete metric space of measurable maps under the disagreement measure, and differentiability of flows with respect to initial data.

Selected references

• I. Ekeland, On the Variational Principle, J. Math. Anal. Appl. 47 (1974), 324–353. https://doi.org/10.1016/0022-247X(74)90025-0
• I. Ekeland, Nonconvex minimization problems, Bull. Amer. Math. Soc. (N.S.) 1 (1979), 443–474. https://doi.org/10.1090/S0273-0979-1979-14595-6
• R. Pallu de la Barrière, Optimal Control Theory, Saunders, Philadelphia, 1967.
• L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, The Mathematical Theory of Optimal Processes, Interscience, New York, 1962.