All missions

Motivation

The economic order quantity (EOQ) is the most widely used formula in inventory management. It assumes that demand is a deterministic constant stream. Real demand is random, and the model that accounts for this, the continuous-review $(Q, r)$ policy with stochastic demand, has no closed-form optimum: for decades its optimal parameters were computed numerically, one instance at a time, which gave little insight into how the stochastic system behaves. Practitioners nevertheless kept using the EOQ quantity in stochastic systems and observed that the cost penalty was small (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), without an analytical explanation.

Zheng (Management Science 38(1), 1992) supplied that explanation. By minimising the average cost first over the reorder point and then over the order quantity, he obtained two simple optimality equations and compared the stochastic model with the EOQ model under the same cost structure. One of the results is the goal of this mission: for every leadtime-demand distribution, using the EOQ order quantity in the stochastic system raises the average cost by at most one eighth. The paper extends Federgruen and Zheng (1988), who treated the discrete-demand version of the cost function.

Setting

A single item faces demand at rate $\lambda > 0$. Orders are delivered after a fixed leadtime $L > 0$, and stockouts are backordered. Each order costs a fixed $K > 0$. Inventory is held at cost rate $h > 0$ per unit and backorders are penalised at cost rate $p > 0$ per unit. Let $D \ge 0$ be the demand during a leadtime, with mean $E(D) = \lambda L$. The newsvendor cost

$$G(y) = E\big[h(y - D)^+ + p(D - y)^+\big]$$

is the rate at which expected inventory costs accrue at time $t + L$ when the inventory position at time $t$ is $y$. It is convex, and it is assumed, as in the paper, to attain its minimum at a unique point $y^0$.

A $(Q, r)$ policy orders $Q$ units whenever the inventory position falls to the reorder point $r$. Its long-run average cost is

$$c(Q, r) = \frac{\lambda K + \int_r^{r+Q} G(y)\,dy}{Q}. \qquad (1)$$

For a fixed $Q > 0$ let $r(Q)$ be an optimal reorder point, and set

$$H(Q) = G(r(Q)) \ (Q > 0),\quad H(0) = G(y^0),\quad C(Q) = c(Q, r(Q)),\quad A(Q) = Q H(Q) - \int_0^Q H(y)\,dy .$$

$C(Q)$ is the average cost when the reorder point is chosen optimally for $Q$; an order quantity $Q^* > 0$ minimising $C$ over $Q > 0$ is the optimal order quantity, and $C^* = C(Q^*)$ is the optimal cost.

The EOQ model is the special case in which the leadtime demand is the constant $\lambda L$. Its cost rate is $G_d(y) = h(y - \lambda L)^+ + p(\lambda L - y)^+$, and its optimal order quantity is

$$Q^*_d = \sqrt{\frac{2\lambda K(h+p)}{hp}} .$$

The subscript $d$ marks every object of the EOQ model ($r_d$, $H_d$, $A_d$).

Formalization targets

Goal: Theorem 5

$$R = \frac{C(Q^*_d) - C^*}{C^*} \;\le\; \frac18 - \frac12\left(\frac12 - \frac{Q^*_d}{Q^*}\right)^2 \;\le\; \frac18 .$$

$C(Q^*_d)$ is the stochastic cost at the EOQ quantity with the reorder point re-optimised for it. The bound holds for every leadtime-demand distribution and every value of the parameters.

Milestones

In the order the goal's proof uses them:

• Lemma 1 (joint convexity of $c$), Lemma 2 ($r = r(Q) \iff G(r) = G(r+Q)$), Lemma 3 (properties of $r(Q)$), Corollary 1 ($G(r(Q)) \le \max(G(r), G(r+Q))$);
• Eq. (7) ($C(Q) = (\lambda K + \int_0^Q H)/Q$), Lemma 4 ($H$ increasing, convex, asymptotic slope $hp/(h+p)$), Lemma 5 ($C$ convex), Eq. (8) ($H(Q^*) = C(Q^*)$), Theorem 1 ($(Q, r)$ optimal iff $c(Q,r) = G(r) = G(r+Q)$), Lemma 6 ($A$ increasing convex, $Q = Q^* \iff A(Q) = \lambda K$, comparative statics in $K$);
• Eqs. (18), (20) (the EOQ model: $H_d(Q) = hpQ/(h+p)$ and the formula for $Q^*_d$), Eq. (22) ($G_d \le G$), Lemma 7 ($H_0 \le H_d \le H$, $A \le A_d$), and the first inequality of Theorem 2, $Q^*_d \le Q^*$.

Significance

The theorem is a distribution-free worst-case guarantee for the most common heuristic in inventory practice. It says that the EOQ formula, which needs only the mean demand rate and three cost parameters, loses at most $12.5\%$ against the true optimum, and that the loss is smaller when $Q^*_d/Q^*$ is close to $\frac12$ or to $1$. Combined with the paper's Theorem 2 (the gap $Q^* - Q^*_d$ is bounded as $K$ grows), it implies that the relative loss vanishes as the fixed ordering cost grows. The milestones along the way (the optimality conditions of Theorem 1, the monotonicity of the optimal reorder point, the comparison of $H$ with its EOQ counterpart) are the standard structural facts about continuous $(Q, r)$ systems and are reused throughout the inventory literature.

The result is proved in the paper. No machine-checked version of it, or of the $(Q, r)$ optimality conditions for the continuous cost (1), is known to exist. The platform has related but different formalizations: the discrete cost function with integer $Q$ (InventoryControl_rqDiscrete), the $(R, Q)$ cost under normal demand (InventoryControl_rq), and the EOQ without backorders (InventoryControl_eoq). A complete development here provides the continuous $(Q, r)$ machinery for an arbitrary leadtime-demand distribution.

Difficulty

The paper's proofs differentiate $r(Q)$ and $H(Q)$ twice (Eqs. (4), (5)), which presupposes a leadtime demand with a smooth density. The formalization does not assume one, so that discrete demand, such as the Poisson demand of the paper's own numerical study, is covered. Every step that the paper takes through derivatives, in particular the convexity of $H$ and the slope bound $H' \le hp/(h+p)$, has to be established by other means: through one-sided derivatives or chord arguments for the convex function $G$, whose kinks are where the derivative-based argument breaks. The definition of $r(Q)$ as a minimiser also means its existence and uniqueness must be proved before any property of $H$, $C$ or $A$ can be used.

Formalization scope

• The model is a probability measure $\mu$ on $\mathbb{R}$ (the law of $D$), concentrated on $[0,\infty)$, integrable, with mean $\lambda L$; $G$ is the integral of $h\max(y-x,0) + p\max(x-y,0)$ against $\mu$. The standing assumptions are bundled in IsQRModel: $\lambda, L, h, p > 0$, the conditions on $\mu$, and the unique minimiser of $G$ (paper, p. 90). $K > 0$ is a separate hypothesis. No density is assumed.
• $c$, $r(Q)$, $y^0$, $H$, $H_0$, $C$, $A$ and optimality of an order quantity are defined for an arbitrary cost rate $G$ and applied both to the newsvendor cost and to $G_d$; the EOQ objects $r_d$, $H_d$, $A_d$ are these definitions at $G_d$, and Eqs. (18), (20) are theorems.
• $r(Q)$ is a chosen minimiser of $c(Q,\cdot)$ (never defined by $G(r) = G(r+Q)$, which is Lemma 2). $H(0) := G(y^0)$; right-continuity of $H$ at $0$ is part of the Lemma 4 milestone. Order quantities range over $(0,\infty)$ for $c$ and $C$ and over $[0,\infty)$ for $H$, $H_0$, $A$.
• $Q^*$ in the goal is any $Q > 0$ with $C(Q) \le C(Q')$ for all $Q' > 0$; Lemma 6 asserts that exactly one exists, so the goal is not vacuous. $Q^*_d$ is the explicit square-root formula.
• Readings of informal words: "increasing" in Lemmas 4 and 6 means strictly increasing on $[0,\infty)$; "$Q^*$ increasing, $r^*$ decreasing in $K$" means strictly; "asymptotic slope $hp/(h+p)$" means that every chord of $H$ on $[0,\infty)$ has slope at most $hp/(h+p)$ and $H(Q)/Q \to hp/(h+p)$; Lemma 3 part 3 is stated as strict monotonicity of $r(Q)$ and $r(Q) + Q$, and its derivative clause $-1 < r'(Q) < 0$ is omitted because $r$ need not be differentiable without a density; "the optimal order quantity" means existence and uniqueness; Lemma 7 is stated for $Q \ge 0$.
• A trivializing formalization is ruled out: $C(Q^*_d)$ is the stochastic cost with the reorder point re-optimised in the stochastic model (not the EOQ reorder point $r^*_d$), and no positivity of $C^*$ is assumed (it follows from the model).
• Out of scope: the discrete cost (2), the §4 numerical study, and the unnumbered remarks after Theorem 5.
• Needed infrastructure: interval integrals of convex functions, partial minimisation of jointly convex functions, Jensen's inequality for $\mu$, and one-sided derivatives of convex functions. The generic $(Q, r)$ machinery (optimality conditions for arbitrary convex $G$) is reusable for other continuous-review models. Proofs of any milestone, and alternative proofs that avoid the paper's differentiability assumptions, are welcome.

Selected references

• Yu-Sheng Zheng, On Properties of Stochastic Inventory Systems, Management Science 38(1):87–103, 1992. https://doi.org/10.1287/mnsc.38.1.87
• Awi Federgruen and Yu-Sheng Zheng, An Efficient Algorithm for Computing an Optimal (r, Q) Policy in Continuous Review Stochastic Inventory Systems, Operations Research 40(4):808–813, 1992. https://doi.org/10.1287/opre.40.4.808
• Paul H. Zipkin, Inventory Service-Level Measures: Convexity and Approximation, Management Science 32(8):975–981, 1986. https://doi.org/10.1287/mnsc.32.8.975
• George Hadley and Thomson M. Whitin, Analysis of Inventory Systems, Prentice-Hall, 1963.
• Daniel P. Heyman and Matthew J. Sobel, Stochastic Models in Operations Research, Vol. II, McGraw-Hill, 1984.

Motivation

In stochastic optimization the law of a random return $r$ is rarely known exactly, while its mean and variance can be estimated. A robust mean-covariance decision maker therefore evaluates a utility $u$ by its worst case

$$U=\inf\{\,E_\nu[u(r)] : \nu \text{ a law on } \mathbb R \text{ with mean } \mu \text{ and variance } \sigma^2\,\}.$$

Popescu (Operations Research 55(1), 2007) shows that for large classes of utilities this infinite-dimensional problem collapses to a one-dimensional one. The paper projects multivariate problems to a single dimension (the subject of the first mission of this series) and then asks for which $u$ the univariate worst case sits on laws with two support points. This mission formalizes the answer the paper gives for utilities whose marginal utility $u'$ is decreasing and changes curvature once, with finite limits: log-logistic utilities $C+\log\frac{1}{1+e^{-ax}}$ used in statistics and classification, and catenary-type utilities $C-b\cosh(ax)$, each plus a concave quadratic.

The result has a bounded-support precursor: Birge and Dulá (Annals of Operations Research 30, 1991, Theorem 5.1, as cited on p. 102 of Popescu 2007) proved an analogous two-point statement for functions on a bounded interval. Popescu's Proposition 5 is the unbounded version on the whole real line.

Setting

Let $u:\mathbb R\to\mathbb R$.

• The family $\mathcal Q$ collects the coefficient triples of quadratics lying below $u$: $\mathcal Q=\{(A,B,C) \mid q(y)=Ay^2+By+C\le u(y)\ \forall y\in\mathbb R\}$.
• A two-point law with support $\{a,b\}$, $a<b$, puts mass $p\in(0,1)$ on $a$ and $1-p$ on $b$. It has mean $\mu$ and variance $\sigma^2$ when $pa+(1-p)b=\mu$ and $p(a-\mu)^2+(1-p)(b-\mu)^2=\sigma^2$.
• Two-point support property (Definition 1). $u$ has it with respect to $(\mu,\sigma^2)$ if some quadratic $q$ with coefficients in $\mathcal Q$ meets $u$ at two points $a<b$, i.e. $q(a)=u(a)$, $q(b)=u(b)$, and a two-point law with support $\{a,b\}$, mean $\mu$ and variance $\sigma^2$ exists. $u$ has the two-point support property if this holds for every $\mu\in\mathbb R$ and every $\sigma>0$.
• Shapes (Definition 2). $f:\mathbb R\to\mathbb R$ is convex-concave if for some $x_0$ it is convex on $(-\infty,x_0)$ and concave on $(x_0,\infty)$; concave-convex if $-f$ is convex-concave; S-shaped if increasing and convex-concave; inverse S-shaped if $-f$ is S-shaped. So an inverse S-shaped $f$ is decreasing, concave on $(-\infty,x_0)$ and convex on $(x_0,\infty)$.
• Lemma 1's quadratic. For $a<b$ and slopes $q_a,q_b$, set

$$A=\frac{q_b-q_a}{2(b-a)},\quad B=\frac{bq_a-aq_b}{b-a},\quad C=\frac{bu(a)-au(b)}{b-a}-ab\,\frac{q_a-q_b}{2(b-a)},$$

and $q(y)=Ay^2+By+C$ (lemma1Quad).

• The function $g$. For $\mu\in\mathbb R$, $\sigma>0$ and $y<\mu$ let $z=\mu+\sigma^2/(\mu-y)$ (partnerPoint) and $g(y)=\frac{u(z)-u(y)}{z-y}-\frac{u'(y)+u'(z)}{2}$ (prop5Gap).

Formalization targets

Goal: Proposition 5 (p. 102)

If $u$ is differentiable, $u'$ is inverse S-shaped, and the limits $\lim_{y\to-\infty}u'(y)$ and $\lim_{y\to+\infty}u'(y)$ exist and are finite, then

$$u \text{ satisfies the two-point support property.}$$

Milestones

1. Proof of Lemma 1, first sentence. If $a<b$ and $\frac{u(b)-u(a)}{b-a}=\frac{q_a+q_b}{2}$, then $q(a)=u(a)$ and $q(b)=u(b)$.
2. Tangency (p. 110). $q'(a)=q_a$ and $q'(b)=q_b$.
3. Lemma 1. $u$ has two-point support if and only if for all $\mu$ and $\sigma>0$ there are $a<b$ and $q_a,q_b$ with

$$(b-\mu)(\mu-a)=\sigma^2,\qquad \frac{u(b)-u(a)}{b-a}=\frac{q_a+q_b}{2},\qquad q\le u \text{ on } \mathbb R.$$

4. Limits of $g$ (p. 110). Under the goal's hypotheses, with $\ell_\pm=\lim_{y\to\pm\infty}u'(y)$,

$$\lim_{y\to-\infty}g(y)=\frac{\ell_--u'(\mu)}{2}>0,\qquad \lim_{y\to\mu^-}g(y)=\frac{\ell_+-u'(\mu)}{2}<0 .$$

5. A zero of $g$ (p. 110). There is $a<\mu$ with $g(a)=0$; with $b=\mu+\sigma^2/(\mu-a)$ one has $a<b$, $(b-\mu)(\mu-a)=\sigma^2$ and $\frac{u(b)-u(a)}{b-a}=\frac{u'(a)+u'(b)}{2}$.

Significance

The result. Through the paper's Proposition 4, two-point support turns the worst-case expected utility over all laws with mean $\mu$ and variance $\sigma^2$ into a minimization over a single parameter $p\in(0,1)$ of $pu(\mu+\sqrt{(1-p)/p}\,\sigma)+(1-p)u(\mu-\sqrt{p/(1-p)}\,\sigma)$. Combined with the projection property of the paper's Section 2, this gives tractable robust counterparts of multivariate stochastic programs whose objective depends on a linear combination $x'R$ of random returns. Proposition 5 is the paper's sufficient condition that places a concrete class of utilities in this regime; it is also closed under adding any quadratic.

Formalizing it. The result is proved on paper; no machine-checked version is known. The formalization produces a checked characterization of two-point support (Lemma 1), a reusable encoding of convex-concave and S-shaped functions, and a proof of Proposition 5. The printed final step of the paper's proof is incomplete (see Difficulty), so a complete formal proof requires an argument the paper does not spell out.

Difficulty

Conditions (a) and (b) of Lemma 1 come from a sign change of $g$ on $(-\infty,\mu)$: the two limits in milestone 4 need a l'Hôpital-type argument and the continuity of a monotone derivative. The central difficulty is condition (c): showing that the quadratic built from a pair $(a,b)$ lies below $u$ on the whole line. The obvious argument takes any zero $a$ of $g$ and counts the intersections of the linear $q'$ with the inverse S-shaped $u'$. This fails when $u'$ is affine on an interval: a zero of $g$ can then produce a quadratic that coincides with $u$ on $[a,b]$ but crosses above $u$ just left of $a$. A proof must therefore choose the zero of $g$, or the pair $(a,b)$, with care, and the curvature hypotheses are not strict.

Formalization scope

• Functions are ℝ → ℝ; $u'$ is deriv u, and the goal assumes Differentiable ℝ u. Finite limits are Tendsto (deriv u) atBot (𝓝 l) and Tendsto (deriv u) atTop (𝓝 l) for some real l; the one-sided limit at $\mu$ is along 𝓝[<] μ.
• "Increasing" in Definition 2 is strict (StrictMono); the paper writes "nondecreasing" for the weak notion. Convexity and concavity are ConvexOn/ConcaveOn on the open half-lines Set.Iio x₀, Set.Ioi x₀, as printed.
• A two-point law is encoded by its mass $p\in(0,1)$ on $a$, with $a<b$; this is equivalent to a probability measure on $\mathbb R$ with support $\{a,b\}$, mean $\mu$ and variance $\sigma^2$.
• "Intersects it at two points $a,b$" is read as $q(a)=u(a)$ and $q(b)=u(b)$ for some $a<b$ (at least two contact points). This is the reading under which Lemma 1 is an equivalence.
• The two-point support property quantifies over $\sigma>0$: no two-point law has variance $0$, so including $\sigma=0$ would make the property false for every $u$.
• The two-point support property is defined from Definition 1 (supporting quadratic plus feasible law), not from Lemma 1's conditions, so Lemma 1 is not a tautology. Every division by $b-a$, $z-y$ or $\mu-y$ occurs under $a<b$ or $y<\mu$.

Useful infrastructure: l'Hôpital's rule at infinity (Analysis/Calculus/LHopital), Darboux's theorem for derivatives, the intermediate value theorem, and one-sided limits of monotone functions. The shape definitions of Definition 2 are reusable for S-shaped value functions elsewhere (prospect theory, sigmoidal utilities). Proofs of the milestones, of the goal, and alternative arguments for condition (c) are all welcome. Related platform work: Wasserstein Distributionally Robust Optimization II.

Selected references

• I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30:277–298, 1991 (cited in Popescu 2007, reference list)

Motivation

Online convex optimization is a repeated game between a learner and an adversary. In each round $t=1,\dots,T$ the learner commits to a point $x_t$ of a convex set $\mathcal P\subseteq\mathbb R^n$; only then is a convex cost function $f_t$ revealed, and the learner pays $f_t(x_t)$. The learner is judged by its regret: its total cost minus the total cost of the best fixed point chosen in hindsight. The model covers online portfolio selection, online regression, prediction with expert advice and the analysis of stochastic gradient methods, and it is the standard language of online learning theory.

Zinkevich (ICML 2003) showed that projected gradient descent with step sizes of order $1/\sqrt t$ has regret $O(GD\sqrt T)$ for any convex costs with gradients bounded by $G$ on a set of diameter $D$, and this rate cannot be improved for linear costs. Hazan, Agarwal and Kale (Machine Learning 69, 2007) asked what curvature buys. Their first result, the subject of this mission, is that the same algorithm with the faster step sizes $1/(Ht)$ has regret only logarithmic in $T$ once every cost function is $H$-strongly convex. The paper's other three results (the Online Newton Step, Follow the Approximate Leader and Exponentially Weighted Online Optimization, for exp-concave costs) are the subject of the other missions of this series.

Setting

Fix $n\in\mathbb N$ and a nonempty, closed, bounded, convex set $\mathcal P\subseteq\mathbb R^n$, with the Euclidean norm $\|\cdot\|_2$ (§2.1, p. 171).

• Cost functions. A sequence $f_1,f_2,\dots:\mathbb R^n\to\mathbb R$. Write $\nabla f_t(x)$ for the gradient and $\nabla^2 f_t(x)$ for the Hessian.
• Gradient bound. A number $G$ with $\|\nabla f_t(x)\|_2\le G$ for all $x\in\mathcal P$ and all rounds $t$ (p. 172).
• $H$-strong convexity (p. 172). For $H>0$, $f$ is $H$-strongly convex on $\mathcal P$ when it is twice differentiable and $\nabla^2 f(x)\succeq H I_n$ for every $x\in\mathcal P$, i.e. $v^\top\nabla^2 f(x)v\ge H\|v\|_2^2$ for all $v$.
• Euclidean projection. $\Pi_{\mathcal P}(y)$ is the point of $\mathcal P$ nearest to $y$, $\Pi_{\mathcal P}(y)=\arg\min_{x\in\mathcal P}\|x-y\|_2$ (IsProj P y z).
• Online Gradient Descent (Fig. 1, p. 174), with step sizes $\eta_1,\eta_2,\dots$: $x_1\in\mathcal P$ is arbitrary, and in iteration $t>1$

$$x_t=\Pi_{\mathcal P}\bigl(x_{t-1}-\eta_t\nabla f_{t-1}(x_{t-1})\bigr)$$

(IsOGDRun P η f x).

• Regret (p. 171): $\mathrm{Regret}_T=\sum_{t=1}^T f_t(x_t)-\min_{x\in\mathcal P}\sum_{t=1}^T f_t(x)$, and $\mathrm{Regret}_T(\mathrm{OGD})$ is its supremum over all cost sequences.

Formalization targets

Goal: Theorem 1 (p. 175)

For $H>0$, cost functions that are $H$-strongly convex on $\mathcal P$ with gradients bounded by $G$ on $\mathcal P$, and any run of Online Gradient Descent whose step after round $t$ is $\eta_{t+1}=1/(Ht)$, for every $T\ge1$ and every $u\in\mathcal P$:

$$\sum_{t=1}^{T}\bigl(f_t(x_t)-f_t(u)\bigr)\ \le\ \frac{G^2}{2H}\,\bigl(1+\log T\bigr).$$

This is LogRegretOCO.OGD.ogd_regret_bound. The constant is the paper's, and at $T=1$ the bound reads $G^2/(2H)$.

Milestones

1. Eq. (1), the strong-convexity inequality: for $x,y\in\mathcal P$, $2(f(x)-f(y))\le 2\nabla f(x)^\top(x-y)-H\|y-x\|_2^2$.
2. Lemma 8 with $A=I_n$: for a convex $\mathcal P$, $z=\Pi_{\mathcal P}(y)$ and $a\in\mathcal P$, $\|y-a\|_2^2\ge\|z-a\|_2^2$. This is already on the platform, proved, as UnderstandingML.projection_lemma, and is reused as a reference item.
3. Eq. (2), the one-step inequality: for $z=\Pi_{\mathcal P}(x-\eta g)$, $\eta>0$, $\|g\|_2\le G$ and $u\in\mathcal P$, $2g^\top(x-u)\le(\|x-u\|_2^2-\|z-u\|_2^2)/\eta+\eta G^2$.

The last step of the argument is the harmonic-sum bound $\sum_{t=1}^T 1/t\le 1+\log T$, which Mathlib already provides (harmonic_le_one_add_log).

Significance

The result. Theorem 1 separates two regimes of online convex optimization: $\Theta(\sqrt T)$ regret for general convex costs and $O(\log T)$ for strongly convex ones, with an algorithm that costs one gradient and one projection per round. Through the online-to-batch conversion, the same step-size schedule gives the $O(\log T/T)$ rate of stochastic gradient descent on strongly convex objectives. The theorem is also the reference point for the paper's weaker exp-concavity assumption, under which the other three algorithms obtain $O(n\log T)$ regret.

Formalizing it. The result is proved and well known; what this mission adds is a machine-checked proof with the paper's exact constant. The Prove2Me platform holds a statement of the textbook version of this theorem (Hazan, Introduction to Online Convex Optimization, Theorem 3.3), OnlineConvexOpt.FirstOrder.online_gradient_descent_strongly_convex_regret, but it is Disproved: its regret is written with a real infimum over the decision set, which Lean evaluates to a junk value. No proved version of the logarithmic bound is on the platform. The strong-convexity inequality, the one-step projected-gradient inequality and the telescoping argument are reusable by every later formalization of gradient methods on the platform.

Difficulty

The argument is short, and its difficulty lies in the bookkeeping. The telescoping sum of squared distances cancels exactly only with the right step-size indexing: the step taken after round $t$ must be $1/(Ht)$. Reading Fig. 1 literally with $\eta_t=1/(Ht)$ makes the step after round $t$ equal to $1/(H(t+1))$, and the sum then leaves an uncancelled term $\frac H2\|x_1-x^*\|_2^2$ that the printed bound does not contain. Strong convexity is a statement about the Hessian, so the curvature inequality (1) needs a second-order Taylor expansion along a segment of $\mathcal P$; convexity of $\mathcal P$ keeps the segment inside the set where the Hessian bound holds. The projection step needs the obtuse-angle property of Euclidean projection onto a convex set.

Formalization scope

Points are EuclideanSpace ℝ (Fin n), so $\|\cdot\|$ is the Euclidean norm (the sup norm of Fin n → ℝ would change the gradient bound). Cost functions are functions on all of $\mathbb R^n$, as the paper's use of gradients and Hessians presupposes; the gradient is Mathlib's gradient, and the Hessian quadratic form is the second Fréchet derivative applied to $(v,v)$. Rounds are 1-based: x 0, f 0 and η 1 are never read, and sums run over Finset.Icc 1 T. The run of the algorithm is a predicate on the whole trajectory, required at every round; the projection is a predicate (nearest point of $\mathcal P$), which is unique for nonempty closed convex $\mathcal P$.

Choices and corrections relative to the printed text:

• Step-size index. Theorem 1 prints "step sizes $\eta_t=\frac1{Ht}$", while its proof sets $\eta_{t+1}=1/(Ht)$ for the step after round $t$. The goal uses the proof's indexing, as a hypothesis η (t + 1) = 1 / (H * t) for $t\ge1$ on the step sizes of Fig. 1.
• Eq. (2). The paper prints "$5\nabla_t^\top(x_t-x^*)$"; the $5$ is a typo for $2$, and the milestone states $2$. The verbatim milestone text keeps the printed $5$.
• Regret. Regret is stated against every comparator $u\in\mathcal P$; the minimum over the compact set $\mathcal P$ is attained, so this is the paper's statement. The expectation in the paper's regret is vacuous for this deterministic algorithm, and the supremum over cost sequences is the universal quantifier over $f$.
• Hypotheses. Strong convexity and the gradient bound are required for the rounds $1,\dots,T$ only. Convexity of each $f_t$, a standing assumption of §2.2, follows from $H$-strong convexity on the convex set $\mathcal P$ and is not added. No diameter bound enters Theorem 1.

A regret bound written with a real ⨅/sInf over $\mathcal P$, or a bound for an arbitrary sequence satisfying Eq. (2) instead of a run of the paper's algorithm, would not be Theorem 1; the goal quantifies over every comparator in $\mathcal P$ and carries the run predicate, the Hessian hypothesis and the gradient bound. The hypotheses are jointly satisfiable: on the closed unit ball, $f_t(x)=\frac H2\|x\|_2^2$ with $G=H$ meets all of them.

Contributions welcome: proofs of the two inequalities and of the goal; a general projection lemma for positive semidefinite $A$ (Lemma 8 in full, needed by the Online Newton Step mission) is reusable beyond this mission.

Selected references

• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007), 169–192. https://doi.org/10.1007/s10994-007-5016-8
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press 2022 (Theorem 3.3). https://arxiv.org/abs/1909.05207
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014 (Lemma 14.9, the projection lemma). https://doi.org/10.1017/CBO9781107298019

Motivation

In many operational problems (shortest paths, assignment, planning) the decision solves a linear program whose cost vector is unknown at decision time and is predicted from contextual features. The predict-then-optimize pipeline fits a model $f$ that maps a feature vector $x$ to a predicted cost vector $\hat c=f(x)$, and then acts on the decision that is optimal for $\hat c$. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed to measure the quality of such a model not by the prediction error but by the SPO loss (Smart Predict-then-Optimize loss): the excess true cost of the decision induced by the prediction over the best decision in hindsight.

The question is whether a small SPO loss on the training sample implies a small SPO loss on new data, uniformly over the models a training procedure may return. The SPO loss is neither convex nor continuous in the prediction, so the standard Lipschitz-based bounds for regression do not apply. El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3, Mathematics of Operations Research 2023; a preliminary version appeared at NeurIPS 2019) give the first such generalization bounds. This mission formalizes their first one, for polyhedral feasible regions, which treats every vertex of the feasible region as a class label of a multiclass classification problem. The bound has since been used by later work, e.g. Hu, Kallus and Mao (Fast rates for contextual linear optimization, Management Science 2022), who sharpen it by a $\sqrt{\log n}$ factor (as noted on p. 4 of the paper).

Setting

A feasible region $S\subseteq\mathbb R^d$ is nonempty, compact and convex. For a cost vector $c\in\mathbb R^d$ the nominal problem is $\min_{w\in S}c^\top w$. An optimization oracle is a fixed map $w^*:\mathbb R^d\to S$ with $w^*(c)\in\arg\min_{w\in S}c^\top w$ for every $c$; nothing is assumed about how it breaks ties. The SPO loss of a prediction $\hat c$ when the realized cost is $c$ is

$$\ell_{\rm SPO}(\hat c,c)=c^\top w^*(\hat c)-c^\top w^*(c)\ \ge 0 .$$

The linear optimization gap is $\omega_S(c)=\max_{w\in S}c^\top w-\min_{w\in S}c^\top w$, and for a set $\mathcal C$ of cost vectors $\omega_S(\mathcal C)=\sup_{c\in\mathcal C}\omega_S(c)$; the SPO loss of a cost in $\mathcal C$ lies in $[0,\omega_S(\mathcal C)]$.

Data are pairs $(x,c)$ drawn from a distribution $\mathcal D$ on $\mathcal X\times\mathcal C$. A hypothesis class $\mathcal H$ is a family of predictors $f:\mathcal X\to\mathbb R^d$. The SPO risk is $R_{\rm SPO}(f)=\mathbb E_{\mathcal D}[\ell_{\rm SPO}(f(x),c)]$, and on an i.i.d. sample $(x_1,c_1),\dots,(x_n,c_n)$ the empirical SPO risk is $\hat R_{\rm SPO}(f)=\frac1n\sum_i\ell_{\rm SPO}(f(x_i),c_i)$. The empirical Rademacher complexity with respect to the SPO loss is

$$\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)=\mathbb E_\sigma\Big[\sup_{f\in\mathcal H}\frac1n\sum_{i=1}^n\sigma_i\,\ell_{\rm SPO}(f(x_i),c_i)\Big]$$

with independent uniform signs $\sigma_i\in\{\pm1\}$, and $\mathfrak R^n_{\rm SPO}(\mathcal H)$ is its expectation over the sample.

The decisions induced by $\mathcal H$ form the class $w^*(\mathcal H)=\{x\mapsto w^*(f(x)):f\in\mathcal H\}$. A class $\mathcal F$ N-shatters a finite set $\mathbb X\subseteq\mathcal X$ if there are two labelings $g_1,g_2$ that differ at every point of $\mathbb X$ such that every mixture of them (follow $g_1$ on a subset $T$, $g_2$ on the rest) is realized by some member of $\mathcal F$. The Natarajan dimension $d_N(\mathcal F)$ is the largest size of an N-shattered set. When $S$ is a polyhedron, $\mathfrak S$ denotes its finite set of extreme points.

Formalization targets

Goal: Theorem 2, second display (p. 11)

For a polyhedral $S$ and every $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample of size $n$, every $f\in\mathcal H$ satisfies

$$R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\,\omega_S(\mathcal C)\sqrt{\frac{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)}{n}}+\omega_S(\mathcal C)\sqrt{\frac{\log(1/\delta)}{2n}} .$$

Milestones, in attack order

1. Theorem 1 (p. 9): with probability $1-\delta$, $R_{\rm SPO}(f)\le\hat R_{\rm SPO}(f)+2\mathfrak R^n_{\rm SPO}(\mathcal H)+\omega_S(\mathcal C)\sqrt{\log(1/\delta)/(2n)}$ for all $f\in\mathcal H$.
2. Massart step (Appendix B.1, p. 31): for a fixed sample with costs in $\mathcal C$, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2\log|\mathfrak F_{|\mathbb X}|/n}$, where $\mathfrak F_{|\mathbb X}$ is the set of decision vectors $(w^*(f(x_1)),\dots,w^*(f(x_n)))$.
3. Natarajan lemma (cited on p. 31; proved on the platform as UnderstandingML.natarajan_lemma): a class from an $m$-point set to $k$ labels with Natarajan dimension $d$ has at most $m^d k^{2d}$ members.
4. Empirical bound (Appendix B.1, p. 31): for a fixed sample, $\hat{\mathfrak R}^n_{\rm SPO}(\mathcal H)\le\omega_S(\mathcal C)\sqrt{2d_N(w^*(\mathcal H))\log(n|\mathfrak S|^2)/n}$.
5. Theorem 2, first display (p. 11): the same bound for the expected complexity $\mathfrak R^n_{\rm SPO}(\mathcal H)$.

Significance

The bound controls the out-of-sample decision cost of every predictor in the class, not only of an empirical risk minimizer, so it applies to any training procedure (SPO+ surrogate minimization, decision trees, heuristics) that returns a member of $\mathcal H$. Its dependence on the feasible region is only through $\omega_S(\mathcal C)$ and $\log|\mathfrak S|$: the number of vertices of a combinatorial polytope is typically exponential in $d$, and enters only logarithmically. For linear predictors $x\mapsto Bx$ the paper's Corollary 2 bounds $d_N(w^*(\mathcal H_{\rm lin}))$ by $dp$, giving a rate of order $\sqrt{dp\log(n|\mathfrak S|)/n}$.

The results are proved in the paper; this mission formalizes them. No statement about predict-then-optimize or the SPO loss is known to have a machine-checked proof. The platform already has the Natarajan lemma (proved) and several Massart-type lemmas for generic classes; this mission connects that multiclass machinery to decision losses, and its Theorem 1 is a reusable Rademacher generalization bound for a loss with range $[0,\omega]$.

Difficulty

The obvious route through Lipschitz contraction fails: the SPO loss jumps when the prediction crosses a point where the optimum is not unique, so the Rademacher complexity of the composed class cannot be bounded by that of $\mathcal H$ times a Lipschitz constant. Any argument through the finitely many vertices of $S$ needs the decisions $w^*(f(x_i))$ to take finitely many values on a sample, i.e. the oracle to return vertices; for an oracle that returns a non-vertex optimal point under ties, $w^*(\mathcal H)$ may take infinitely many values on a sample. On the probabilistic side, the passage from the empirical to the expected complexity and the McDiarmid concentration step (Theorem 1) require the suprema over an uncountable class to be measurable, which the paper does not discuss.

Formalization scope

Lean works in $\mathbb R^d$ = EuclideanSpace ℝ (Fin d); cost vectors and decisions live in the same space and $c^\top w$ is the inner product. The standing assumptions of §2 are hypotheses of every theorem: $S$ nonempty, compact and convex; $w^*$ an arbitrary oracle (a hypothesis IsOracle S w, never a specific selection); $\mathcal C$ nonempty and bounded, with the cost component of $\mathcal D$ in $\mathcal C$ almost surely (or, for fixed-sample statements, every $c_i\in\mathcal C$); $n\ge1$. "Polyhedron" means the solution set of finitely many linear inequalities; with compactness it is a polytope, and $|\mathfrak S|$ is the cardinality of Set.extremePoints ℝ S. The expectation over signs is the exact average over the $2^n$ sign vectors; $R_{\rm SPO}$ and $\mathfrak R^n_{\rm SPO}$ are Bochner integrals. "With probability at least $1-\delta$" is stated as: the product measure of the set of samples on which some $f\in\mathcal H$ violates the bound is at most $\delta$.

The formalization commits to the following disclosed additions:

• In the empirical bound, Theorem 2 and its first display, the oracle returns extreme points of $S$. This is the proof's own "w.l.o.g." (p. 31), made explicit because p. 10 allows non-vertex outputs under ties. The hypothesis is needed: on the unit square, an oracle that returns distinct interior points of an edge under ties can have $d_N(w^*(\mathcal H))=1$ and empirical complexity near $\frac12$, which exceeds the printed bound for large $n$.
• The Natarajan dimension is not defined as a number (a supremum in $\mathbb N$ would silently be $0$ for unboundedly large shattered sets). Statements carry a natural number $k$ bounding the size of every N-shattered set, in place of $d_N(w^*(\mathcal H))$. This is equivalent when $d_N$ is finite; the printed bound is vacuous otherwise.
• Theorem 1 and the goal carry three measurability hypotheses: each loss function $z\mapsto\ell_{\rm SPO}(f(z_1),z_2)$ is measurable; the uniform deviation $\sup_f(R_{\rm SPO}(f)-\hat R_{\rm SPO}(f))$ and, for each sign vector, the signed supremum $\sup_f\frac1n\sum_i\sigma_i\ell_{\rm SPO}(f(x_i),c_i)$ are almost-everywhere measurable functions of the sample. Without them the integral defining $\mathfrak R^n_{\rm SPO}$ could default to $0$.
• The Massart step assumes $\mathfrak F_{|\mathbb X}$ finite, the case in which its printed right-hand side is finite.

A formalization that let $d_N$ be an sSup in $\mathbb N$, or chose a specific tie-breaking oracle inside the definitions, would prove a different and in part trivial statement; both are excluded.

Infrastructure needed: McDiarmid's bounded-differences inequality and symmetrization for the product measure; Massart's finite-class lemma (a proved version is on the platform as RademacherMassart.rad_le_massart, with its own normalization); the Natarajan lemma (proved, UnderstandingML.natarajan_lemma, stated with its own but identical notion of N-shattering over finite types); finiteness and nonemptiness of the extreme points of a nonempty polytope. Theorem 1 and the Massart step do not use polyhedrality and are reusable for any bounded decision loss. Contributions of these infrastructure lemmas are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, arXiv:1905.11488v3, 2022; Mathematics of Operations Research, 2023. https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 9–26, 2022. https://arxiv.org/abs/1710.08005
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian complexities: risk bounds and structural results, Journal of Machine Learning Research 3, 463–482, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• B. K. Natarajan, On learning sets and functions, Machine Learning 4(1), 67–97, 1989. https://doi.org/10.1007/BF00114804
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014 (Lemma 29.4). https://doi.org/10.1017/CBO9781107298019
• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018 (Theorem 3.3, Corollary 3.8). https://cs.nyu.edu/~mohri/mlbook/