Probability

Why the worst case matters

Distributionally robust optimization (DRO) replaces the expected loss $E_{P_0}[\ell(\beta^{\mathsf T}X)]$ of a linear decision rule $\beta$ by its worst case over all data laws $P$ within transport distance $\delta$ of the baseline $P_0$. When $P_0$ is an empirical distribution this covers regularized regression and classification (Blanchet, Kang, Murthy 2019; Esfahani, Kuhn 2018). The optimal value is one number; a practitioner also wants to know which distribution realizes it, the adversary's best response. It shows which data points the robust model guards against, it gives stress-test scenarios, and its structure is what the paper's comparative statics (Theorem 7) and iterative schemes build on.

J. Blanchet, K. Murthy and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes (arXiv:1810.02403v3; Math. Oper. Res. 47(2), 2022), answer this for a state-dependent Mahalanobis cost. Theorem 6 of that paper describes the worst-case distribution through the solution of the one-dimensional dual problem. This mission formalizes Theorem 6.

Setting

The data $X$ take values in $\mathbb R^d$ with law $P_0$, a Borel probability measure. The decision $\beta$ ranges over a convex set $B\subseteq\mathbb R^d$ (a standing assumption of the paper). Moving mass from $x$ to $x'$ costs

$$c(x,x')=(x-x')^{\mathsf T}A(x)(x-x'),$$

where $A(x)$ is positive definite. Assumption 1 asks that $c$ be lower semicontinuous and that $\rho_{\min}\|v\|^2\le v^{\mathsf T}A(x)v\le\rho_{\max}\|v\|^2$ for $P_0$-almost every $x$, with $\rho_{\min}>0$. The optimal transport cost $D_c(P_0,P)$ is the least value of $E_\pi[c(X,X')]$ over couplings $\pi$ of $P_0$ and $P$. For $\delta>0$ the worst-case objective is

$$\sup_{P:\,D_c(P_0,P)\le\delta}E_P\bigl[\ell(\beta^{\mathsf T}X)\bigr].\tag{6}$$

Assumption 2 asks that the loss $\ell:\mathbb R\to\mathbb R$ be convex, that the growth exponent $\kappa=\inf\{s\ge0:\sup_u(\ell(u)-su^2)<\infty\}$ be finite, and that $E_{P_0}\|X\|^4<\infty$.

The dual side is built from

$$F(\gamma,\beta,\lambda;x)=\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,\beta^{\mathsf T}A(x)^{-1}\beta\bigr)-\lambda\sqrt\delta\bigl(\gamma^2\beta^{\mathsf T}A(x)^{-1}\beta-1\bigr),$$

the robust loss $\ell_{\rm rob}(\beta,\lambda;x)=\sup_{\gamma}F$, the dual objective $f_\delta(\beta,\lambda)=E_{P_0}[\ell_{\rm rob}(\beta,\lambda;X)]\in\mathbb R\cup\{\infty\}$ and the maximizer set $\Gamma^*(\beta,\lambda;x)=\arg\max_\gamma F(\gamma,\beta,\lambda;x)$. By the paper's Theorem 1, (6) equals $\inf_{\lambda\ge0}f_\delta(\beta,\lambda)$, and a minimizer $\lambda_*(\beta)$, the dual optimizer, exists. The threshold is $\lambda_{thr}(\beta)=\kappa\sqrt\delta\,\mathrm{ess\,sup}_{P_0}\,\beta^{\mathsf T}A(X)^{-1}\beta$; below it $f_\delta=\infty$.

Formalization targets

Goal: Theorem 6(c)

Let $\beta\ne0$ and $\lambda_*(\beta)>\lambda_{thr}(\beta)$. Let $G_\pm(x)\in\Gamma^*(\beta,\lambda_*(\beta);x)$ be measurable selections with the largest and smallest square, $\bar c=E[G_+^2\beta^{\mathsf T}A(X)^{-1}\beta]$, $\underline c=E[G_-^2\beta^{\mathsf T}A(X)^{-1}\beta]$, and let $Z\sim\mathrm{Bernoulli}(q)$ be independent of $X$ with $q=(\bar c-1)/(\bar c-\underline c)\in[0,1]$. Then

$$X^*=X+\sqrt\delta\,\bigl(ZG_-+(1-Z)G_+\bigr)A(X)^{-1}\beta,\qquad E[c(X,X^*)]=\delta,$$

and the law of $X^*$ attains the supremum in (6).

Milestones

• Lemma 1: $\Gamma^*\ne\emptyset$ and $\ell_{\rm rob}<\infty$ when $\lambda>\kappa\sqrt\delta\,\beta^{\mathsf T}A(x)^{-1}\beta$, and $\ell_{\rm rob}=\infty$ below that; hence $\{\lambda>\lambda_{thr}\}\subseteq\{f_\delta<\infty\}\subseteq\{\lambda\ge\lambda_{thr}\}$.
• Lemma 3(a): $\sqrt\delta|g|\beta^{\mathsf T}A(x)^{-1}\beta\le1+C_1\varepsilon^{-1}(1+|\beta^{\mathsf T}x|)$ for $g\in\Gamma^*$ once $\lambda\ge(\kappa+\varepsilon)\sqrt\delta\beta^{\mathsf T}A(x)^{-1}\beta$.
• Proposition 2 (a) and its $\lambda$-part: the one-sided $\lambda$-derivatives of $\ell_{\rm rob}$ are the minimum and the maximum of $-\sqrt\delta(\gamma^2\beta^{\mathsf T}A(x)^{-1}\beta-1)$ over $\Gamma^*$.
• The one-sided $\lambda$-derivatives of $f_\delta$ on $\{\lambda>\lambda_{thr}\}$:

$$\partial_\pm f_\delta/\partial\lambda=\sqrt\delta\bigl(1-E[\beta^{\mathsf T}A(X)^{-1}\beta\,\inf/\sup_{g\in\Gamma^*}g^2]\bigr).$$

• [Blanchet–Murthy 2019, Theorem 1]: strong duality and complementary slackness (already proved on the platform).

Companion statements

Theorem 6(a): $\lambda_*>0$ unless $\ell$ is constant. Theorem 6(b): $\lambda_*\ge\lambda_{thr}$. Theorem 6(d), as the paper's example: for $\ell(u)=u^2-|u|(1-e^{-|u|})$, $P_0=\delta_0$, $A=I$ and $\|\beta\|=1$, $\lambda_*=\lambda_{thr}=\sqrt\delta$ and no distribution attains the value $\delta$. Theorem 6(e), with Lemma 8: if $\ell''\le M$ and $\lambda_*>\tfrac12M\sqrt\delta\,\mathrm{ess\,sup}\,\beta^{\mathsf T}A(X)^{-1}\beta$, then $\Gamma^*$ is a singleton $\{G(x)\}$ almost surely and the law of $X+\sqrt\delta G(X)A(X)^{-1}\beta$ is the unique worst case.

Significance

The result reduces a search over all probability measures to a scalar problem per data point. Each point is pushed along the single direction $A(x)^{-1}\beta$, by an amount read off the maximizers of $F$, and the budget $\delta$ is always spent completely. When the maximizer is not unique, randomization between two extreme maximizers is needed and suffices. Part (d) shows that the threshold condition cannot be removed, and part (e) gives a deterministic transport map (a Monge solution) under smoothness. Theorem 7 of the paper, the monotone growth of worst-case displacements in $\delta$, is a statement about the random variable $G$ produced here.

None of these statements has been machine-checked before. The general strong duality with complementary slackness of Blanchet–Murthy (arXiv:1604.01446) is proved on the platform, so this mission connects that abstract theorem to an explicit worst-case law. A formal proof also has to settle one point the printed text leaves loose: which extreme maximizers enter the mixture (see Formalization scope).

Difficulty

The first idea is to take the pointwise maximizers of $F$ at $\lambda_*$ and push $P_0$ forward. That works only when the maximizer is unique and the budget constraint happens to be tight. In general the maximizer set is not a singleton, and the derivative of $f_\delta$ at $\lambda_*$ only lies between a left and a right derivative. Turning the first-order condition $\partial_+f_\delta\ge0\ge\partial_-f_\delta$ into an exact cost $\delta$ needs three things. The one-sided derivatives must be identified as expectations over $\Gamma^*$, an envelope theorem under an integral with a non-compact parameter set. The extreme maximizers must be compact and measurably selectable. Finally the resulting coupling must be certified optimal through complementary slackness. Each step needs a hypothesis that is easy to lose: the growth control of Lemma 3, the essential supremum in $\lambda_{thr}$, measurability of selections.

Formalization scope

Points of $\mathbb R^d$ are EuclideanSpace ℝ (Fin d), $\beta^{\mathsf T}x$ is the inner product, and $\beta^{\mathsf T}A(x)^{-1}\beta$ is quadInv A β x. $\ell_{\rm rob}$ and $f_\delta$ are extended-real valued; $f_\delta$ uses the published extended integral ModelRiskOT.Duality.extIntegral. The worst-case objective (6) is the published primal problem primalValue: a supremum over couplings $\pi$ with first marginal $P_0$ and $\int c\,d\pi\le\delta$ (primalFeasible). A distribution attains (6) when a coupling with that second marginal has value primalValue. The random worst case $X^*$ is encoded by the joint law of $(X,X^*)$, a mixture of two graph couplings, because $E[c(X,X^*)]$ depends on the pair. A dual optimizer is a real $\lambda_*\ge0$ minimizing $f_\delta(\beta,\cdot)$ on $[0,\infty)$.

Standing hypotheses on every statement: $P_0$ a probability measure, Assumptions 1 and 2, $\delta>0$, $B$ convex. The following departures from the printed text are disclosed in each item:

• In (c), $G_\pm$ are the selections of extreme square used in the proof (p. 40), not $\inf\Gamma^*$ and $\sup\Gamma^*$ as printed; a two-point example shows the printed choice can fail.
• In (e), "for every $x$" is read as "for $P_0$-almost every $x$", which is what the proof gives.
• Lemma 8 is stated for $\beta\ne0$.
• Proposition 2 is formalized for part (a) and the $\lambda$-derivatives only.

Every expectation used in the goal ($\bar c$, $\underline c$) carries an integrability conjunct. The cost identity and optimality are asserted for the measure itself, so no junk value of a non-integrable integral can make the goal hold vacuously. A statement asserting only first-order conditions for $\lambda_*$ would not be Theorem 6. The goal asserts primal attainment and the exact cost.

Needed infrastructure, reusable beyond this mission: envelope (Danskin) theorems for one-sided derivatives of suprema, differentiation of convex integral functionals, measurable selection of argmax sets, and complementary slackness through the published Blanchet–Murthy theorem. Contributions of any of these as standalone lemmas are welcome.

Selected references

• J. Blanchet, K. Murthy, F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Math. Oper. Res. 47(2), 2022. arXiv:1810.02403v3, doi:10.1287/moor.2021.1178
• J. Blanchet, K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Math. Oper. Res. 44(2), 2019. arXiv:1604.01446
• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019. doi:10.1017/jpr.2019.49
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Math. Program. 171, 2018. doi:10.1007/s10107-017-1172-1
• D. P. Bertsekas, S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978 (Proposition 7.50, measurable selection).

Motivation

Distributionally robust optimization chooses a decision against a range of plausible probability laws instead of a single fitted law. Here the decision is a linear rule evaluated through a loss function. The range of laws is specified by how much probability mass may be transported away from a baseline law. A conventional transport cost depends only on the displacement. Blanchet, Murthy and Zhang allow the cost of moving a point to depend on its starting location, so the uncertainty model can reflect local information. Their introduction gives a portfolio example: uncertainty about returns may differ across market conditions, and a state dependent cost can encode that difference. The paper develops a dual reformulation as the basis for its later convexity, optimizer, and algorithmic results.

The theorem in this mission is the first structural result of that development. It says that evaluating the worst-case loss does not require optimizing directly over all probability distributions. A dual objective built from the baseline law gives the same value, and its nonnegative scalar multiplier attains the best value. The earlier general transport duality theorem of Blanchet and Murthy is already formalized and proved on Prove2Me; the remaining target here is the state dependent Mahalanobis specialization and its explicit scalar form.

Setting

Let $X\in\mathbb R^d$ have a baseline law $P_0$, and let $B\subseteq\mathbb R^d$ be a convex set of decisions. A decision $\beta\in B$ incurs loss $\ell(\beta^{\mathsf T}X)$, where $\ell:\mathbb R\to\mathbb R$. The transport cost of moving $x$ to $x'$ is

$$c(x,x')=(x-x')^{\mathsf T}A(x)(x-x'),$$

where $A(x)$ is positive definite at every $x$. Under Assumption 1, $c$ is lower semicontinuous, and the eigenvalues of $A(x)$ lie between fixed positive bounds $\rho_{\min}$ and $\rho_{\max}$ for $P_0$-almost every $x$. Since $A$ depends on the starting point, $c$ need not be symmetric. For two laws $P_0$ and $P$, $D_c(P_0,P)$ is the least expected cost among couplings whose first and second marginals are $P_0$ and $P$. The ambiguity set at radius $\delta>0$ consists of laws satisfying $D_c(P_0,P)\le\delta$. The paper writes the worst-case loss as an equivalent supremum over couplings with first marginal $P_0$ and cost at most $\delta$ (§2.1, p. 9).

For $x,\beta\in\mathbb R^d$, write $q_A(\beta,x)=\beta^{\mathsf T}A(x)^{-1}\beta$. The paper introduces a pointwise robust loss from

$$F(\gamma,\beta,\lambda;x)=\ell\bigl(\beta^{\mathsf T}x+\gamma\sqrt\delta\,q_A(\beta,x)\bigr)-\lambda\sqrt\delta\bigl(\gamma^2q_A(\beta,x)-1\bigr),$$

by setting $\ell_{\rm rob}(\beta,\lambda;x)=\sup_{\gamma\in\mathbb R}F(\gamma,\beta,\lambda;x)$ and $f_\delta(\beta,\lambda)=E_{P_0}[\ell_{\rm rob}(\beta,\lambda;X)]$. This expectation may be extended real. These are the objects of display (7) and Theorem 1 on p. 10.

Formalization targets

The goal is Theorem 1 of the paper. If $\ell$ is upper semicontinuous and the baseline loss is integrable, then for each $\beta\in B$,

$$\sup_{P:\,D_c(P_0,P)\le\delta}E_P[\ell(\beta^{\mathsf T}X)]=\inf_{\lambda\ge0}f_\delta(\beta,\lambda),$$

and a multiplier $\lambda^*(\beta)\ge0$ attains the infimum. The target retains the state dependence of $A$, the full range of $\beta$ in $B$, and the possible extended value of the worst-case loss. It asserts both the value identity and attainment; the latter is part of the printed theorem.

The milestone list follows the paper's proof on p. 32: the previously proved general strong duality theorem, the quadratic minimum under a linear constraint, and pointwise equality (25) between the transport envelope and $\ell_{\rm rob}$. The quadratic minimum is stated with attainment. The pointwise equality includes $\beta=0$ and records the change from the original transport multiplier to the scaled multiplier used in $F$.

Significance

The formula replaces a search over probability laws with a scalar outer optimization and an expectation under $P_0$. That representation is the paper's starting point for examining the shape of $f_\delta$, locating dual optimizers, describing worst-case laws, and designing iterative schemes. Without a faithful dual identity, those later claims would concern a function whose connection to the original distributional problem had not been established (Theorems 2–7).

The general Blanchet–Murthy strong duality theorem has a machine-checked proof on Prove2Me. This mission supplies the specialized model, the quadratic reduction, and the equality with the paper's $f_\delta$. Those declarations can then serve as a stable interface for the remaining missions in this series. The current goal and its new milestones are open Lean statements; the paper result itself is proved in the cited work.

Difficulty

The general duality theorem returns a dual problem whose envelope is a supremum over destination points in $\mathbb R^d$. The paper's formula instead uses one scalar $\gamma$, and its multiplier is scaled by $\sqrt\delta$. Showing that these describe the same value requires controlling a positive definite quadratic cost with a state dependent matrix at every starting point. At $\beta=0$, the hyperplane formula used in the nonzero case has a zero denominator, while equation (25) remains meaningful. Extended values also matter: the pointwise supremum can be infinite, and replacing it with a real-valued approximation could alter the theorem.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), laws are Borel probability measures, and matrices are real positive definite matrices. The local Setting definition fixes $c$, $q_A$, $F$, $\ell_{\rm rob}$, and $f_\delta$ using the paper's notation. The worst-case objective reuses the published coupling form ModelRiskOT.Duality.primalValue; its feasible plans already enforce the first marginal and cost budget. EReal carries the primal value, pointwise supremum, integral, and outer infimum. The extended integral is the published ModelRiskOT.Duality.extIntegral, with its documented convention for a difference of two infinite parts. The multiplier ranges over $\lambda\ge0$, and $\delta>0$ is explicit so its square root can be used in the rescaling.

The goal retains the paper's standing convexity of $B$, Assumption 1, and $\beta\in B$. It adds integrability of $x\mapsto\ell(\beta^{\mathsf T}x)$, required by the cited general duality theorem but omitted from the printed Theorem 1. This addition is disclosed so the statement's scope is clear. The goal equates the primal worst-case loss with the explicit infimum of $f_\delta$ and asserts attainment; an identity between two dual notations would leave the main claim unaddressed. Contributions to the positive definite quadratic minimization, the pointwise envelope equality, and their connection to the general duality theorem are in scope. The shared Setting layer is intended for reuse in the later convexity and worst-case-law missions.

Selected references

• J. Blanchet, K. Murthy and F. Zhang, Optimal Transport-Based Distributionally Robust Optimization: Structural Properties and Iterative Schemes, Mathematics of Operations Research 47(2), 2022. arXiv:1810.02403v3
• J. Blanchet and K. Murthy, Quantifying Distributional Model Risk via Optimal Transport, Mathematics of Operations Research 44(2), 2019. arXiv:1604.01446v2

Motivation

The lost-sales inventory model with a positive lead time is one of the basic models of inventory theory. A retailer reviews stock once per period, places an order that arrives $L$ periods later, and loses (rather than backlogs) any demand that cannot be met from stock on hand. Lost sales are the norm in retail, where a customer facing an empty shelf buys elsewhere. The optimal policy is the solution of a dynamic program whose state is the on-hand inventory together with the whole pipeline of $L$ outstanding orders. The state dimension therefore grows with the lead time, and computing the optimal policy is intractable beyond small $L$: for a lead time of four and geometric demand the dynamic program already has 228,581 states (Zipkin 2008a, Operations Research 56(5), 1256–1263).

Heuristics (base-stock, myopic, cost-balancing) have been studied at length. Reiman (2004) analyzed an open-loop policy that orders one unit at fixed intervals in a continuous-review lost-sales model with Poisson demand. Zipkin (2008a) observed numerically that ordering the same constant amount every period performs well already at lead time four. Huh, Janakiraman, Muckstadt and Rusmevichientong (2009) proved that order-up-to policies are asymptotically optimal as the lost-sales penalty grows. Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante proved that a constant-order policy is asymptotically optimal as the lead time grows, with an explicit threshold. This mission formalizes that result, Theorem 1 of their paper.

Setting

Fix a holding cost $h>0$ per unit left over at the end of a period, a lost-demand penalty $c>0$ per unit of unmet demand, a lead time $L\ge1$, and a horizon $T>L$. Demands $D_1,D_2,\dots$ are i.i.d. with a law $\mathcal D$ on $[0,\infty)$ that has a finite third moment and is not deterministic. At the start of period $t$ the system holds inventory $I_t$ and a pipeline $\mathbf x_t=(x_{1,t},\dots,x_{L,t})$ of outstanding orders. First $x_{1,t}$ arrives; then an order is placed and joins the end of the pipeline; then $D_t$ is realized, and

$$I_{t+1}=(I_t+x_{1,t}-D_t)^+,\qquad C_t=hI_{t+1}+c\,(I_t+x_{1,t}-D_t)^-.$$

The system starts empty. A policy chooses each order from the information available before the period's demand, possibly with randomization. Problem (1) is

$$\mathrm{OPT}(L,T)=\inf_{\pi}\sum_{t=L+1}^{T+L}\mathbb E[C^\pi_t].$$

For $r\ge0$ let $I^r_\infty=\sup_{k\ge0}\big(kr-\sum_{i=1}^kD_i\big)$, the steady-state waiting time of a GI/D/1 queue. For $r<\mathbb E[D]$ the constant-order policy $\pi_r$ orders the random amount $I^r_\infty+r$ (drawn independently of the demands) in the first period and $r$ in every later period. The best constant is $z=\arg\min_{v\ge0}(h\mathbb E[I^v_\infty]-cv)$ (the smallest minimizer). With $Q$ the $c/(c+h)$ quantile of $\mathcal D$, $g=h\mathbb E[(Q-D)^+]+c\mathbb E[(D-Q)^+]$, $\sigma$ the standard deviation and $\zeta$ the skewness of $D$, set $m=\lceil(26(3\zeta+c(h\sigma)^{-1}\mathbb E[D]+1))^2\rceil$ and

$$y(\epsilon)=\max\Big(2^{14}h(Q+2^{3/2}\mathbb E[D])(\mathbb E^2[D]+\mathbb E[D^2])^3\sigma^{-6}m^3g^{-1}\epsilon^{-1},\ \big(12c\,\mathbb E[D]\,g^{-1}((2ch^{-1})^{1/2}+3)\big)^2\epsilon^{-2}\Big).$$

Formalization targets

Goal: Theorem 1

For all $\epsilon\in(0,1)$, $L\ge y(\epsilon)$ and $T\ge(1+3\epsilon^{-1})L$,

$$\mathbb E\Big[\sum_{t=L+1}^{T+L}C^{\pi_z}_t\Big]\ \le\ (1+\epsilon)\,\mathrm{OPT}(L,T).$$

Milestones

The milestones follow the paper's argument in its order:

• the cost of $L$ consecutive periods from a given state (Lemma 3) and under $\pi_r$ (Lemma 4);
• a bounded optimal policy (Lemma 5) and the existence of a most favourable state $(\mathbf x^*,\mathcal I^*)$ (§5);
• lower bounds on the optimal cost over $L$ periods (Lemmas 6, 7);
• random-walk estimates ((26) and Lemma 9) and the per-window gap of $\pi_{r^*}$, $r^*=L^{-1}\sum_ix^*_i$ (Theorem 8);
• an explicit Lipschitz CLT rate (Theorem 11), the separation $\mathbb E[D]-r^*\ge\frac12\sigma m^{-1/2}$ (Lemma 10), and the resulting explicit gap (Corollary 12);
• the newsvendor bound $\mathbb E[C^\pi_t]\ge g$ (§3.1) and the stationary cost of $\pi_r$, (25).

Significance

The theorem says that the policy which ignores the state entirely, ordering the same amount every period after a single randomized first order, loses at most a factor $1+\epsilon$ against the optimal policy once the lead time exceeds an explicit threshold. The threshold depends only on $h$, $c$ and the demand law. Optimal policies are out of computational reach precisely when $L$ is large, so this is the first guarantee of near-optimality whose computation does not grow with the lead time. The paper's Corollary 2 (the ratio tends to $1$ as $L\to\infty$) follows directly.

The result is proved in the paper (up to the correction below); this platform holds no formalization of it or of its lemmas. A formalization would produce reusable statements about suprema of random walks with negative drift (Lemma 9, (26)), a quantitative central limit theorem for Lipschitz test functions (Theorem 11), and the finite-horizon lost-sales problem built on the published model of this platform.

Difficulty

The obvious comparison fails. An optimal policy may vary its orders arbitrarily over time, so its pipeline need not look like a constant stream. Comparing it period by period with $\pi_r$ gives nothing, because the inventory of $\pi_r$ is driven by an unbounded random-walk supremum.

The paper instead bounds the optimal cost over any $L$ consecutive periods by the cost from the most favourable state. It then has to show that the average $r^*$ of that state's pipeline stays bounded away from $\mathbb E[D]$ uniformly in $L$. This last step is the crux. The components of $\mathbf x^*$ may vary considerably over the window, and a qualitative central limit theorem is not enough: the argument needs an explicit rate (Theorem 11) with constants that survive summation over $L$ windows. On the probabilistic side, the expectations of random indices $i^r_k$ at which random walks attain their maxima are not adapted to the demand filtration. They are controlled only through the distributional identity of Lemma 9 and the geometric tail (26).

Formalization scope

The model is the published CappedBaseStock_Model. Its parameter record supplies $L\ge1$, $h>0$ and the penalty $c>0$ (field p; the record is called prm). Its demand law supplies a probability law on $[0,\infty)$ with finite positive mean. The finite third moment and non-determinism are explicit hypotheses. $Q$ and $g$ are the published newsvendorLevel and backorderCost. The conventions:

• Time is zero-based: Lean period $t$ is the paper's period $t+1$, and a window starting at Lean $t_0$ is the paper's $\tau=t_0+1$. Pipeline slot $i$ is $x_{i+1}$.
• Costs, OPT and expectations of nonnegative quantities are lower integrals in $[0,\infty]$, and $I^r_\infty$ is valued in $[0,\infty]$. Real expectations appear only for integrable quantities.
• OPT is the infimum over the model's admissible policies: measurable functions of past demands and a private uniform seed. This class contains the paper's policy class, so OPT is at most the paper's and the goal is at least as strong as the page.
• "Conditional on $\mathbf x^\pi_\tau=\mathbf x$, $I^\pi_\tau=\mathcal I$" is rendered by running the system from that state. Lemma 3 states that this integrates back to the policy's cost.
• Lemmas 6–7, Theorem 8 and Corollary 12 are stated for every policy that almost surely never orders more than $Q$, which includes the paper's optimal $\bar\pi$; their proofs use only that bound.
• $\pi_r$ draws its first order as the quantile function of $I^r_\infty$ at the policy's uniform seed.
• The ratio of Theorem 1 is stated multiplicatively. A ratio would read $0$ at $\mathrm{OPT}=0$, whereas $\mathrm{OPT}(L,T)\ge Tg>0$.

A correction. As printed, the second term of $y(\epsilon)$ (p. 5) and of Corollary 12 (p. 14) lack a factor $\mathbb E[D]$. The proof of Corollary 12 establishes $\mathcal I^*\le(\lceil(2ch^{-1}L)^{1/2}\rceil+2)\mathbb E[D]$, and the printed bounds are not invariant under rescaling the demand. Both are stated here with the factor restored, and each item's note says so.

Neither a long-run average cost nor a restricted comparator (stationary, Markov, or bounded-order) may replace the finite-horizon OPT. The demand law may not be specialized, and $\pi_r$ may not order $r$ in its first period: each change makes the goal a different, easier theorem.

A complete development needs Lindley-type recursions and the stationarity of the GI/D/1 waiting time, Chernoff and moment bounds for random-walk maxima, a Stein-method CLT rate, and the existence of optimal policies for a finite-horizon problem with a continuous state. The random-walk and CLT parts are independent of inventory theory and reusable. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• D. A. Goldberg, D. A. Katz-Rogozhnikov, Y. Lu, M. Sharma, M. S. Squillante, Asymptotic Optimality of Constant-Order Policies for Lost Sales Inventory Models with Large Lead Times, Mathematics of Operations Research, 2016; preprint arXiv:1211.4063v2 (cited version). https://arxiv.org/abs/1211.4063
• P. Zipkin, Old and New Methods for Lost-Sales Inventory Systems, Operations Research 56(5), 1256–1263, 2008.
• P. Zipkin, On the Structure of Lost-Sales Inventory Models, Operations Research 56(4), 937–944, 2008.
• W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science 55(3), 404–420, 2009.
• M. Reiman, A New and Simple Policy for a Continuous Review Lost-Sales Inventory Model, unpublished manuscript, 2004.
• L. H. Y. Chen, Q.-M. Shao, Stein's Method for Normal Approximation, in An Introduction to Stein's Method, 1–59, 2005.
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003.

Motivation

Sums of random matrices appear throughout numerical linear algebra, statistics, combinatorics and quantum information: randomized sketching and sparsification, covariance estimation, graph sparsifiers, and the analysis of random features all reduce to controlling the largest eigenvalue of a sum of random self-adjoint matrices. Scalar concentration inequalities (Chernoff, Hoeffding, Bernstein, Azuma) have matrix analogues, and J. A. Tropp's User-Friendly Tail Bounds for Sums of Random Matrices (arXiv:1004.4389v7, Found. Comput. Math. 12 (2012) 389–434, doi:10.1007/s10208-011-9099-z) gives a unified derivation of them with explicit constants.

Many applications do not have independent summands: adaptive algorithms, online learning and sequential estimation produce sums whose terms depend on the past. The scalar tool for such sums is Azuma's inequality for martingales with bounded differences, and its corollary, McDiarmid's bounded differences inequality (McDiarmid 1998). This mission is the fifth of a series formalizing Tropp's paper; it targets §7, the matrix Azuma inequality.

Timeline. Ahlswede and Winter (2002) introduced a matrix analogue of the Laplace transform bound for independent sums; Oliveira (2010) gave the variant used in this paper. Tropp (this paper, 2010–2012) proved the matrix Azuma and McDiarmid inequalities below. More refined matrix martingale inequalities appear in Oliveira (2010) and in Tropp's Freedman's inequality for matrix martingales (2011), which the paper cites (p. 27) as requiring additional machinery.

Setting

All matrices are $d\times d$ with complex entries, $d\ge 1$. A matrix is self-adjoint (s.a.) when it is Hermitian. For s.a. $A$, $\lambda_{\max}(A)$ is its largest eigenvalue and $\|A\|$ its spectral norm. Functions of s.a. matrices are defined spectrally: if $A=Q\Lambda Q^*$ then $e^{A}=Qe^{\Lambda}Q^*$, and $\log$ is defined the same way on positive-definite matrices. $A\preceq B$ is the semidefinite order: $B-A$ is positive semidefinite.

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space with a filtration $\mathcal F_0\subset\mathcal F_1\subset\cdots\subset\mathcal F$, and write $\mathbb E_k[\,\cdot\,]=\mathbb E[\,\cdot\mid\mathcal F_k]$. The expectation and the conditional expectation of a random matrix are taken entrywise. A sequence $X_1,\dots,X_n$ of random matrices is adapted when each $X_k$ is $\mathcal F_k$-measurable. A matrix martingale is an adapted sequence of s.a. matrices $Y_k$ with $\mathbb E\|Y_k\|<\infty$ and $\mathbb E_{k-1}Y_k=Y_{k-1}$; its difference sequence $X_k=Y_k-Y_{k-1}$ satisfies $\mathbb E_{k-1}X_k=0$.

The hypotheses of the main theorem are: $X_1,\dots,X_n$ is an adapted sequence of random s.a. matrices, and $A_1,\dots,A_n$ is a fixed (non-random) sequence of s.a. matrices, with

$$\mathbb E_{k-1}X_k = 0 \qquad\text{and}\qquad X_k^2\preceq A_k^2\ \text{ almost surely.}$$

The variance parameter is $\sigma^2 := \big\|\sum_k A_k^2\big\|$.

Formalization targets

Goal: Theorem 7.1 (Matrix Azuma), p. 27

For all $t\ge 0$,

$$\mathbb P\Big\{\lambda_{\max}\Big(\sum_{k}X_k\Big)\ge t\Big\}\le d\cdot e^{-t^2/8\sigma^2}.$$

Milestones

In the order they are used:

1. Display (2.6), Golden–Thompson: $\operatorname{tr}e^{A+H}\le\operatorname{tr}(e^Ae^H)$ for s.a. $A,H$.
2. Proposition 3.1, the Laplace transform method: $\mathbb P\{\lambda_{\max}(Y)\ge t\}\le\inf_{\theta>0}e^{-\theta t}\,\mathbb E\operatorname{tr}e^{\theta Y}$.
3. Corollary 3.3: $\mathbb E\operatorname{tr}\exp(H+X)\le\operatorname{tr}\exp(H+\log\mathbb E e^{X})$.
4. Lemma 4.3, Rademacher half: $\mathbb E e^{\varepsilon\theta A}\preceq e^{\theta^2A^2/2}$.
5. Lemma 7.6 (Symmetrization): $\mathbb E\operatorname{tr}e^{H+X}\le\mathbb E\operatorname{tr}e^{H+2\varepsilon X}$ when $\mathbb EX=0$ and $\varepsilon$ is an independent Rademacher variable.
6. Lemma 7.7 (Azuma cgf): $\log\mathbb E[e^{2\varepsilon\theta X}\mid X]\preceq2\theta^2A^2$ when $X^2\preceq A^2$.
7. Display (7.5): $\mathbb E\operatorname{tr}\exp(\sum_k\theta X_k)\le\operatorname{tr}\exp(2\theta^2\sum_kA_k^2)$ under the hypotheses of the goal.

Further statements

Corollary 7.2 is the martingale form, $\mathbb P\{\lambda_{\max}(Y_n-\mathbb EY_n)\ge t\}\le d\,e^{-t^2/8\sigma^2}$. Corollary 7.5 (Matrix Bounded Differences) is the matrix McDiarmid inequality, $\mathbb P\{\lambda_{\max}(H(z)-\mathbb EH(z))\ge t\}\le d\,e^{-t^2/8\sigma^2}$ for a matrix-valued function $H$ of independent variables whose changes in one coordinate $k$ have squares bounded by $A_k^2$.

Significance

The result. The bound has the scalar subgaussian shape with two matrix features: a dimensional factor $d$, and a variance parameter equal to the norm of the sum $\sum_kA_k^2$ rather than the sum of the norms $\sum_k\|A_k\|^2$. In the commuting case the two coincide; in general the first can be smaller by a factor of up to $n$. The theorem needs no independence, so it covers adapted constructions such as Doob martingales. Corollary 7.5, obtained from it, is the standard matrix tool for concentration of matrix-valued functions of independent data. With independent summands the theorem gives a matrix Hoeffding inequality (Theorem 1.3 of the paper).

Formalizing it. The result is proved in the paper; none of it is formalized. Mathlib has the continuous functional calculus, conditional expectation and filtrations, but no Golden–Thompson inequality, no Lieb concavity theorem, and no matrix tail inequality. A formalization produces a machine-checked matrix Azuma inequality, the Golden–Thompson inequality, and a symmetrization lemma for the trace exponential, all of which have uses beyond this paper.

Difficulty

The scalar proof of Azuma's inequality multiplies conditional moment generating functions, $\mathbb E e^{\theta\sum X_k}=\mathbb E\big[e^{\theta\sum_{k<n}X_k}\,\mathbb E_{n-1}e^{\theta X_n}\big]$, and bounds each factor. For matrices this fails: $e^{A+B}\neq e^Ae^B$ unless $A$ and $B$ commute, and $\operatorname{tr}e^{A+B+C}\le\operatorname{tr}(e^Ae^Be^C)$ is false, so the Golden–Thompson inequality cannot be iterated over $n$ terms. The paper itself notes (p. 28) that the classical approach does not seem to extend. A second obstacle is that the hypothesis $X_k^2\preceq A_k^2$ bounds squares, not the matrices themselves; it does not give $X_k\preceq A_k$, so the scalar Hoeffding lemma for bounded centred variables has no direct matrix analogue. The infrastructure is also heavy: Lieb's concavity theorem underlies Corollary 3.3, and operator monotonicity of the logarithm is needed.

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℂ, self-adjointness is IsHermitian, and $\preceq$ is Mathlib's order under MatrixOrder. Matrix exponential and logarithm are cfc Real.exp and cfc Real.log. $\lambda_{\max}$ is the supremum of the real spectrum, which is why $d\ge1$ is assumed (NeZero d). Expectation and conditional expectation of matrices are entrywise Bochner integrals; adaptedness is entrywise strong measurability with respect to a Mathlib Filtration ℕ. The summands are indexed by $k=1,\dots,n$, so $\mathcal F_{k-1}$ is never truncated. The bound $X_k^2\preceq A_k^2$ is required almost surely. The bounds $A_k$ are deterministic matrices. The infimum over $\theta>0$ in Proposition 3.1 is posed as the bound for each $\theta>0$ at which the expectation is finite.

The hypotheses must not be made vacuous. Integrability of each $X_k$ is assumed explicitly, because for a non-integrable variable Lean's conditional expectation is $0$ and the centring hypothesis would say nothing. The $X_k$ are not assumed independent: an independence hypothesis would turn the goal into the weaker matrix Hoeffding inequality.

Two readings are recorded in the statements. In Lemma 7.7 the conditional expectation given $X$ is replaced by the expectation over $\varepsilon$ at each fixed value $x$ with $x^2\preceq A^2$; by independence these agree. Corollary 7.2 adds the hypothesis that $Y_0$ is almost surely constant, without which $Y_n-\mathbb EY_n\neq\sum_kX_k$.

A complete development needs: Golden–Thompson; Lieb's concavity theorem (or Corollary 3.3 directly); operator monotonicity of the matrix logarithm; monotonicity of the trace exponential; conditional expectation of matrix-valued variables and its interaction with the semidefinite order. All of these are reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.1, Corollary 3.3 and Lemma 4.3 are also milestones of other missions in this series.

Selected references

• J. A. Tropp, User-Friendly Tail Bounds for Sums of Random Matrices, Found. Comput. Math. 12 (2012) 389–434; cited version arXiv:1004.4389v7 (2011). https://arxiv.org/abs/1004.4389v7
• R. Ahlswede and A. Winter, Strong converse for identification via quantum channels, IEEE Trans. Inform. Theory 48 (2002) 569–579. https://doi.org/10.1109/18.985947
• R. I. Oliveira, Sums of random Hermitian matrices and an inequality by Rudelson, Electron. Commun. Probab. 15 (2010) 203–212. https://arxiv.org/abs/1004.3821
• J. A. Tropp, Freedman's inequality for matrix martingales, Electron. Commun. Probab. 16 (2011) 262–270. https://arxiv.org/abs/1101.3039
• R. I. Oliveira, Concentration of the adjacency matrix and of the Laplacian in random graphs with independent edges, arXiv:0911.0600 (2010). https://arxiv.org/abs/0911.0600
• C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer (1998) 195–248. https://doi.org/10.1007/978-3-662-12788-9_6
• R. Bhatia, Matrix Analysis, Springer GTM 169 (1997), Sec. IX.3. https://doi.org/10.1007/978-1-4612-0653-8
• E. H. Lieb, Convex trace functions and the Wigner–Yanase–Dyson conjecture, Adv. Math. 11 (1973) 267–288. https://doi.org/10.1016/0001-8708(73)90011-X

Motivation

A retailer who orders a seasonal product before demand is known faces the newsvendor trade-off. Ordering too much leaves unsold stock, and ordering too little forgoes sales. A risk-neutral newsvendor orders a critical fractile of demand. A risk-averse one orders less, since inventory is a risky investment, and this reduction has been shown under constant and decreasing absolute risk aversion (Eeckhoudt, Gollier and Schlesinger, Management Science 41(5), 1995, doi:10.1287/mnsc.41.5.786). Agrawal and Seshadri (2000) and Chen and Federgruen (2000) reached related conclusions.

Demand for many products moves with traded financial quantities: a stock index, a commodity price, an exchange rate. V. Gaur and S. Seshadri (Manufacturing & Service Operations Management 7(2), 2005, pp. 103–120, doi:10.1287/msom.1040.0061) ask what happens when the newsvendor can trade a financial instrument correlated with demand. Their Proposition 7 answers one half of the question: hedging moves the risk-averse newsvendor's order up, towards the risk-neutral quantity. This mission formalizes Proposition 7 and the steps of its appendix proof. The source is the published article, a library scan.

Setting

Let $S_T$ be the price at time $T$ of a traded asset, with law $\nu$ on $\mathbb R$. Demand is $D=a+b(S_T+\varepsilon)$ with $b>0$. Here $\varepsilon$ is the scaled forecast error, independent of $S_T$, with law $G$, $E[\varepsilon]=0$ and $E[\varepsilon^2]<\infty$. The unit selling price, cost and salvage value are $p>ce^{rT}>s$. In the paper's scaled units ((11), p. 110) these collapse into one cost parameter $c_1$ with $0<c_1$ and $c_1b<1$, and an initial-wealth term $W$.

A hedge is a portfolio with time-$T$ payoff $X_T=\varphi(S_T)$ for a nondecreasing function $\varphi$, and time-0 price $X_0$. It is a fair gamble, $E[X_T]=X_0e^{rT}$ (display (12)). A firm that stocks $I>\max\{a,0\}$ units and shorts $\alpha$ units of the hedge ends with the scaled wealth (14)

$$\Pi_H(I,\alpha)=W+\min\Big\{S_T+\varepsilon,\ \frac{I-a}{b}\Big\}-c_1I-\alpha X_T+\alpha X_0e^{rT}.$$

A decision maker with utility $u:\mathbb R\to\mathbb R$ ranks $(I,\alpha)$ by $E[u(\Pi_H(I,\alpha))]$, and $I^*(\alpha)$ maximizes it over $I$.

The absolute risk aversion is $R_A(w)=-u''(w)/u'(w)$ and the absolute prudence is $-u'''(w)/u''(w)$. The utility displays DARA or CARA when $R_A$ is decreasing or constant, and DAP when prudence is decreasing or constant.

The hedge ratio is bounded by $\bar\alpha$, chosen so that $E_\varepsilon[\Pi_H(I,\alpha)\mid S_T]$ is nondecreasing in $S_T$ for $0\le\alpha\le\bar\alpha$. Beyond $\bar\alpha$ the firm over-hedges: its expected profit falls as the asset price rises.

Formalization targets

Goal: Proposition 7 (p. 112)

For an increasing, concave, differentiable utility with constant or decreasing absolute risk aversion and constant or decreasing absolute prudence,

$$\frac{dI^*}{d\alpha}\ \ge\ 0\qquad\text{for }0\le\alpha\le\bar\alpha,$$

stated as: $\alpha\mapsto I^*(\alpha)$ is nondecreasing on $[0,\bar\alpha]$.

Milestones

1. Lemma 2 (p. 118), in its weak form. If $f$ is decreasing with $E[f(X)]=0$, then $E[w(X)f(X)]\ge0$ for decreasing nonnegative $w$, and $E[w(X)f(X)]\le0$ for increasing nonnegative $w$.
2. Utility facts of §3.2 (p. 111). DARA or CARA implies $u'''\ge0$, and DAP implies that $u'''$ is decreasing.
3. Steps of the proof (pp. 118–119).
   • $E_\varepsilon[u''(\Pi)\mid S_T]$ is increasing in $S_T$.
   • The first term of the cross-partial representation (25) is nonnegative.
   • The quantity $(1/b)R_A(\Pi_0)u'(\Pi_0)\Pr\{\varepsilon>(I-a)/b-S_T\}\,\partial\Pi/\partial\alpha$ has nonpositive mean.
   • $\partial^2E[u(\Pi)]/\partial I\partial\alpha\ge0$, as increasing differences of $E[u(\Pi_H(I,\alpha))]$ on $(\max\{a,0\},\infty)\times[0,\bar\alpha]$.

Significance

Proposition 7 reverses the conclusion of Eeckhoudt et al. Those authors find that an additional uncorrelated background risk lowers the risk-averse newsvendor's order. Here a correlated financial position that offsets the inventory risk raises it. Hedging therefore increases expected profit as well as reducing variance, and brings a risk-averse firm's operational decision closer to the risk-neutral one. The result is one of the basic statements linking operational and financial risk management in supply-chain finance.

The formalization adds three things.

• Corrected lemmas. The proof rests on a one-variable Chebyshev inequality (Lemma 2) whose printed strict form is false, and on a cross-partial computation that differentiates under the expectation without comment. A machine-checked proof fixes the correct hypotheses: the weak inequalities, and the integrability under which (24)–(25) hold.
• Reusable monotone comparative statics. The steps from increasing differences in (inventory, hedge ratio) to a monotone argmax apply to other stochastic inventory models with expected-utility objectives.
• Formal status. The result is proved in the paper. To our knowledge no part of it has been formalized.

Difficulty

The obvious argument signs the cross-partial derivative directly: $E[u''(\Pi)\,\partial\Pi/\partial I\,\partial\Pi/\partial\alpha]$, with $\partial\Pi/\partial\alpha=X_0e^{rT}-X_T$ of mean zero. That needs the sign of a covariance between $\partial\Pi/\partial\alpha$ and $u''(\Pi)\,\partial\Pi/\partial I$, a weight that depends on both $S_T$ and $\varepsilon$ and is not monotone in either.

The paper first conditions on $S_T$ and splits the weight into two terms. The first is a conditional mean of $u''(\Pi)$. The second is concentrated on the sell-out event. Each term then needs its own monotonicity in $S_T$.

• For the second term, monotonicity comes from DARA alone.
• For the first term, $E_\varepsilon[u''(\Pi)\mid S_T]$, a second application of the Chebyshev inequality, in $\varepsilon$, is needed. It uses prudence (DAP) and the bound $\alpha\le\bar\alpha$.

Neither ingredient can be dropped. Without $\alpha\le\bar\alpha$ the conditional mean payoff decreases in $S_T$ and the first term changes sign.

Two further obstacles are technical:

• the expectation is not differentiable in $I$ where $\varepsilon=(I-a)/b-S_T$ has an atom;
• the hedge $\varphi$ is only monotone, hence differentiable only almost everywhere.

Formalization scope

Representation.

• $S_T\sim\nu$ and $\varepsilon\sim G$ are probability measures on $\mathbb R$, and every expectation is taken over $\nu\otimes G$. Independence is built in, and $E_\varepsilon[\,\cdot\mid S_T=s]$ is the integral over $G$ at fixed $s$.
• The parameters are the scaled $W,a,b,c_1$ of (11). The constraint $p>ce^{rT}>s$ becomes $0<c_1$ and $c_1b<1$, an exact reparametrization.
• The hedge is a nondecreasing, measurable, $\nu$-integrable $\varphi$ with $\int\varphi\,d\nu=X_0e^{rT}$. The paper's "piecewise continuous, differentiable a.e." is dropped, so the formal statement is more general.
• $R_A$ is the platform's Arrow–Pratt coefficient MDPFinance.FinancialMarkets.arrowPrattCoefficient, referenced rather than redefined.

Conventions.

• "Increasing, concave, differentiable" is taken as $C^3$ with $u'>0$ and $u''<0$ on all of $\mathbb R$. Absolute prudence $-u'''/u''$ requires $u''\ne0$, and the proof uses $u''<0$.
• DARA/CARA and DAP are stated as $R_A$ and the prudence being nonincreasing.
• $\bar\alpha$ is any value for which the conditional mean payoff is nondecreasing in $S_T$ for every $\alpha\in[0,\bar\alpha]$ and every admissible $I>\max\{a,0\}$.
• $I^*$ is any selection of maximizers over $I>\max\{a,0\}$; the maximizer is unique by strict concavity.
• $dI^*/d\alpha\ge0$ is stated as monotonicity of $I^*$. The cross-partial claim is stated as increasing differences.
• Lemma 2 and "the second term is negative" are weakened to the non-strict inequalities, because the printed strict forms fail for constant weights.

Integrability. The goal and the increasing-differences milestone assume integrability of $u(\Pi)$, $u'(\Pi)$, $u''(\Pi)$ and of their products with $\partial\Pi/\partial\alpha$ on the whole region, which is the regularity the proof uses. Without it a Bochner integral would silently be $0$: the objective would be constant in $I$ and every $I$ a maximizer. A hypothesis set that forces $\bar\alpha=0$ would also trivialize the goal. A sorry-free check file exhibits the utility class, the standing assumptions and the $\bar\alpha$-condition with $\bar\alpha=1/2$ for $u(w)=-e^{-w}$, $\varepsilon=\pm1$ with equal probability and $\varphi(s)=\min\{s,-1/2\}$.

Infrastructure and contributions. A one-variable Chebyshev association inequality for monotone functions is needed. So are differentiation under the integral, or an integrated mean-value argument, for piecewise-linear payoffs, and the step from increasing differences plus a unique maximizer to a monotone argmax. All three are reusable. Proofs of the milestones in any order are welcome, as are alternative arguments that avoid the cross-partial derivative altogether.

Selected references

• V. Gaur, S. Seshadri, Hedging Inventory Risk Through Market Instruments, Manufacturing & Service Operations Management 7(2), 103–120, 2005. https://doi.org/10.1287/msom.1040.0061
• L. Eeckhoudt, C. Gollier, H. Schlesinger, The Risk-Averse (and Prudent) Newsboy, Management Science 41(5), 786–794, 1995. https://doi.org/10.1287/mnsc.41.5.786
• M. S. Kimball, Precautionary Saving in the Small and in the Large, Econometrica 58(1), 53–73, 1990. https://doi.org/10.2307/2938334
• K. J. Arrow, Essays in the Theory of Risk-Bearing, North-Holland, 1971.
• P. Milgrom, C. Shannon, Monotone Comparative Statics, Econometrica 62(1), 157–180, 1994. https://doi.org/10.2307/2951479

Motivation

Stochastic gradient descent (SGD) is the standard first-order method for stochastic convex optimization and for training linear predictors on large data sets: at each step it queries a noisy subgradient of the objective, takes a step against it and projects back onto the feasible set. When the objective is strongly convex, the classical online-learning analysis of SGD with step sizes $\eta_t=\Theta(1/t)$ bounds the expected suboptimality of the averaged iterate $\bar w_T=\frac1T(w_1+\dots+w_T)$ by $O(\log(T)/T)$ (Hazan, Agarwal, Kale 2007). The information-theoretically optimal rate for this problem class is $O(1/T)$, and it is attained by other algorithms (Hazan, Kale 2011; Juditsky, Nesterov 2010).

This left a concrete question: is the logarithmic factor an artifact of the analysis, or a property of SGD with averaging? Rakhlin, Shamir and Sridharan (arXiv:1109.5647v7, ICML 2012) answer it by exhibiting strongly convex problems on which averaged SGD provably loses the logarithm. The same paper shows that for objectives that are smooth at the optimum the averaged iterate attains $O(1/T)$, and that averaging only a suffix of the iterates restores $O(1/T)$ in general. This mission is the lower-bound half of that picture; the two upper bounds are sibling missions of the same series.

Setting

Points live in $\mathbb R^d$, $d\ge1$, with the Euclidean norm; for a point $w$, $w_1$ denotes its first coordinate. A stochastic gradient oracle for an objective $F$ returns, at a query point $w_t$, a random vector $\hat g_t$ whose mean is a subgradient of $F$ at $w_t$. Projected SGD on a domain $W$ with step sizes $\eta_t=c/t$, $c>0$, starts at a point $w_1\in W$ and sets

$$w_{t+1}=\Pi_W\big(w_t-\eta_t\hat g_t\big),\qquad t=1,2,\dots,$$

where $\Pi_W$ is the Euclidean projection onto $W$. The output studied here is the average $\bar w_T=\frac1T(w_1+\dots+w_T)$. Throughout, $Z_1,Z_2,\dots$ are independent random variables, each uniformly distributed on $[-1,3]$.

Example A. $W=[0,1]^d$, $F(w)=\tfrac12\|w\|^2+w_1$, and the oracle returns $\hat g_t=w_t+(Z_t,0,\dots,0)$. The global minimum over $W$ is at $w^*=0$, a corner of the box.

Example B. $W=[-1,1]^d$ and

$$F(w)=\tfrac12\|w\|^2+\begin{cases}w_1&w_1\ge0\\-7w_1&w_1<0,\end{cases}\qquad \hat g_t=w_t+\begin{cases}(Z_t,0,\dots,0)&w_{t,1}\ge0\\(-7,0,\dots,0)&w_{t,1}<0.\end{cases}$$

Here $F$ is $1$-strongly convex and non-smooth along the hyperplane $w_1=0$, and its minimizer $w^*=0$ lies in the interior of $W$. The oracle is state-dependent: which branch it uses depends on the sign of the first coordinate of the query point. In both examples $\mathbb E[\hat g_t]$ is a subgradient of $F$ at $w_t$ and $\mathbb E\|\hat g_t\|^2$ is bounded for fixed $d$.

Formalization targets

Goal: Theorem 4 (p. 5)

In Example B, for every $c>0$, every starting point $w_1\in W$ with $w_{1,1}\ge0$, $T_0=\max\{2,6c+1\}$ and every integer $T\ge T_0+2$,

$$\mathbb E\big[F(\bar w_T)-F(w^*)\big]\ \ge\ \frac{3c}{16T}\sum_{t=T_0+2}^{T}\frac1t-\frac{T_0}{T}.$$

For fixed $c$ this is $\Omega(\log(T)/T)$. The goal is the paper's statement with its constants.

Milestones

1. Theorem 3 (p. 5). In Example A, for every $c>0$, every $w_1\in W$, $T_0=\max\{2,c/2\}$ and every integer $T\ge T_0+1$,

$$\mathbb E\big[F(\bar w_T)-F(w^*)\big]\ \ge\ \frac{c}{16T}\sum_{t=T_0}^{T-1}\frac1t.$$

2. Eq. (9) (p. 16). The pathwise recursion of the first coordinate in Example B:

$$w_{t+1,1}=\Pi_{[-1,1]}\Big(\big(1-\tfrac ct\big)w_{t,1}-\begin{cases}Z_t\,c/t&w_{t,1}\ge0\\-7c/t&w_{t,1}<0\end{cases}\Big).$$

3. App. B.5, p. 17. In Example B, whenever $c/t<1$,

$$\Pr\big(w_{t,1}\notin[0,c/t]\ \big|\ w_{t-1,1}\ge0\big)\ \ge\ \tfrac34 .$$

Significance

The result. Theorem 4 shows that the $O(\log(T)/T)$ guarantee for SGD with full averaging is tight up to constants on strongly convex problems, even when the optimum is interior. It separates SGD with averaging from algorithms that reach $O(1/T)$, and it is the reason the paper introduces $\alpha$-suffix averaging. It also explains why smoothness at the optimum (the paper's §3) matters: Example B is non-smooth exactly at $w^*$.

Formalizing it. The result is proved on paper but, as far as the platform's index shows, has no machine-checked proof. Formalization adds a verified lower bound with explicit constants. It also settles the paper's own argument. The printed proof of Theorem 4 relies on Lemma 4 (p. 16), whose first claim uses $Z_t\ge-1$ where the recursion subtracts $(c/t)Z_t$ with $Z_t$ up to $3$, so Lemma 4 fails with positive probability. Theorem 4 is believed true, but a complete proof needs a repaired argument. Theorem 3's printed proof uses $\eta_t\le1$ in step (8), while $t\ge T_0$ only gives $\eta_t\le2$. Numerical checks of Theorem 3 itself found no violation.

Difficulty

An expectation lower bound on the average needs control of every iterate $w_t$, not just of the last one, and the iterates form a non-linear Markov chain because of the projection and, in Example B, because of the state-dependent oracle. Upper-bound techniques do not transfer: they bound $\mathbb E\|w_t-w^*\|^2$ from above, which says nothing about the sign of $w_{t,1}$. In Example B, the natural first idea is to argue that $w_{t,1}$ never stays negative, so that it behaves like the constrained Example A; this is the claim of the paper's Lemma 4, and as stated it does not hold, because a single noise draw near $3$ can push the first coordinate below the level the lemma asserts. A proof must handle that event with explicit constants and still produce the $T_0/T$ slack of the statement.

Formalization scope

• Space. $\mathbb R^d$ is UnderstandingML.Vec d = EuclideanSpace ℝ (Fin d) with [NeZero d]; the paper's first coordinate is index 0.
• Projection. $\Pi_W$ onto the box $[lo,hi]^d$ is coordinatewise clamping $v_i\mapsto\max\{lo,\min\{hi,v_i\}\}$, which is the Euclidean projection onto the box.
• Indexing. sgdRun … k is the paper's $w_{k+1}$; the step at index $k$ uses $\eta_{k+1}=c/(k+1)$ and the noise value $Z$ at index $k$. The starting point is arbitrary (not $0$), as in Theorems 3–4.
• Noise. Each $Z_t$ has law ProbabilityTheory.cond volume (Set.Icc (-1) 3) (uniform on $[-1,3]$); a horizon-$T$ sequence has the product law UnderstandingML.iidLaw. Expectations are Bochner integrals over it.
• Constants and ranges. $c>0$ is the only condition on $c$. $T_0$ is real; $T$ is a natural number; $\sum_{t=T_0}^{T-1}$ is over the integers $\lceil T_0\rceil\le t\le T-1$, and $\sum_{t=T_0+2}^{T}$ over $\lceil T_0\rceil+2\le t\le T$. $F(w^*)$ is written $F(0)$.
• No junk integrals. Theorems 3 and 4 also assert integrability of $F(\bar w_T)-F(0)$, so the inequality cannot hold because an integral defaulted to $0$. The probability milestone is stated multiplicatively, $\Pr(A\cap B)\ge\frac34\Pr(B)$, rather than through ProbabilityTheory.cond, which would be the zero measure on a null conditioning event.
• Not trivializable. The examples (the constant $7$, the noise interval $[-1,3]$, the boxes $[0,1]^d$, $[-1,1]^d$) are fixed by the paper; replacing the oracle or the domain is a different theorem. Since $F(\bar w_T)\ge F(0)$ always, Theorem 4 is immediate whenever its right-hand side is negative, but it is a non-trivial inequality for large $T$, and the statement quantifies over all $T\ge T_0+2$.
• Not posed. Lemma 4 (false as stated), step (8) of App. B.4, and Eq. (10) with the displays after it in App. B.5 (they depend on Lemma 4).
• Infrastructure. Measurability of the SGD run in the noise sequence, independence of $Z_t$ from the past iterates under the product law, and probabilities of intervals under the uniform law are reusable for any analysis of SGD on explicit examples. Proofs of the milestones, a repaired proof of Lemma 4's role, and a complete proof of Theorem 4 are all welcome.

Selected references

• A. Rakhlin, O. Shamir, K. Sridharan, Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization, ICML 2012; arXiv:1109.5647v7, 2012. https://arxiv.org/abs/1109.5647v7
• E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69, 2007. https://doi.org/10.1007/s10994-007-5016-8
• E. Hazan, S. Kale, Beyond the regret minimization barrier: an optimal algorithm for stochastic strongly-convex optimization, COLT 2011. https://proceedings.mlr.press/v19/hazan11a.html
• A. Juditsky, Y. Nesterov, Primal-dual subgradient methods for minimizing uniformly convex functions, 2010. https://hal.science/hal-00508933
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19(4), 2009. https://doi.org/10.1137/070704277