All missions

Motivation

In classical optimal transport, a transport plan that minimizes the total cost is characterized through its support: an optimal plan is $c$-cyclically monotone, meaning that no finite collection of its transported particles can be re-paired more cheaply (Villani, Optimal Transport, Old and New, 2009, Ch. 4–5). This pointwise criterion is how most structural results in optimal transport are proved: it is what turns a global minimization over measures into a statement about finitely many points.

The martingale transport problem adds a constraint motivated by mathematical finance: the plan must be the law of a one-step martingale $(X, Y)$ with given marginals $X\sim\mu$, $Y\sim\nu$. Its value gives model-independent bounds on the price of an exotic option whose payoff is the cost function, given the prices of all vanilla options at two dates (Beiglböck, Henry-Labordère, Penkner, Model-independent bounds for option prices, Finance Stoch. 2013). Because the martingale constraint ties together all points with the same first coordinate, the classical re-pairing argument does not carry over: swapping two destinations generally destroys the martingale property.

M. Beiglböck and N. Juillet (On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 2016; arXiv:1208.1509v2) prove a martingale replacement for $c$-cyclical monotonicity, the variational lemma (Lemma 1.11). It is the tool from which they derive the left-monotone structure of optimal plans, the uniqueness of the left-curtain coupling as optimizer for costs $h(y-x)$ with $h'$ strictly convex, and the support bounds for optimizers. This mission is the first of a series formalizing that paper.

Setting

All measures live on $\mathbb R$ or $\mathbb R\times\mathbb R$ with their Borel $\sigma$-algebras. Two probability measures $\mu,\nu$ on $\mathbb R$ with finite first moment are in convex order, $\mu\preceq_C\nu$, if $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi:\mathbb R\to\mathbb R$.

A transport plan is a measure $\pi$ on $\mathbb R^2$ with first marginal $\mu$ and second marginal $\nu$. It is a martingale transport plan, $\pi\in\Pi_M(\mu,\nu)$, if under $\pi$ the conditional mean of $y$ given $x$ equals $x$; equivalently,

$$\int\rho(x)\,(y-x)\,d\pi(x,y)=0\quad\text{for every bounded Borel }\rho .$$

A cost is a Borel function $c:\mathbb R^2\to\mathbb R$ satisfying the sufficient integrability condition $c(x,y)\ge a(x)+b(y)$ with $a\in L^1(\mu)$, $b\in L^1(\nu)$; then the cost of a plan, $\int c\,d\pi$, is well defined in $(-\infty,+\infty]$. A plan $\pi\in\Pi_M(\mu,\nu)$ is optimal if $\int c\,d\pi\le\int c\,d\pi'$ for every $\pi'\in\Pi_M(\mu,\nu)$, and it leads to finite costs if $\int c\,d\pi<+\infty$.

A measure $\alpha'$ on $\mathbb R^2$ is a competitor of $\alpha$ (Definition 1.10) if it has the same two marginals as $\alpha$ and the same conditional barycentres: $\int y\,d\alpha_x(y)=\int y\,d\alpha'_x(y)$ for almost every $x$, where $(\alpha_x)$, $(\alpha'_x)$ are disintegrations with respect to the first marginal. A competitor redistributes the mass of $\alpha$ in a way that a martingale plan could absorb: replacing a piece $\alpha$ of a martingale plan by $\alpha'$ keeps both marginals and the martingale property.

Formalization targets

Goal: the variational lemma (Lemma 1.11, p. 8)

Let $\mu\preceq_C\nu$ be probability measures, $c$ a Borel cost satisfying the sufficient integrability condition, and $\pi\in\Pi_M(\mu,\nu)$ optimal with $\int c\,d\pi<+\infty$. Then there is a Borel set $\Gamma\subseteq\mathbb R^2$ with $\pi(\Gamma)=1$ such that

$$\int c\,d\alpha\le\int c\,d\alpha'\quad\text{for every finitely supported }\alpha\text{ with }\operatorname{spt}\alpha\subseteq\Gamma\text{ and every competitor }\alpha'\text{ of }\alpha .$$

The set $\Gamma$ is chosen once, before $\alpha$; the quantifier order is the content.

Milestones

The milestones are the steps of the paper's proof (§3, pp. 16–19), in attack order:

1. Theorem 3.1 (p. 17), Kellerer's duality in the form of Beiglböck–Goldstern–Maresch–Schachermayer: for a Polish probability space $(Z,\zeta)$ and a Borel $M\subseteq Z^n$, either $M\subseteq\bigcup_i M_i$ with $\zeta(\operatorname{proj}^iM_i)=0$, or some measure $\gamma$ with $\gamma(M)>0$ has all marginals $\le\zeta$.
2. The set $M\subseteq(\mathbb R^2)^n$ of $n$-tuples carrying a non-optimal finite measure is Borel (p. 17).
3. In case (1), a Borel $\Gamma_n$ of full $\pi$-measure supports no improvable $\alpha$ with $|\operatorname{spt}\alpha|\le n$ (p. 18).
4. Every finitely supported $\alpha$ has a cost-minimizing competitor (p. 18).
5. If $\omega\le\pi$ and a competitor $\omega'$ is cheaper than $\omega$, then $\pi-\omega+\omega'$ is a cheaper martingale plan (p. 18).
6. For an optimal $\pi$ of finite cost, case (2) cannot occur (pp. 18–19).
7. $\Gamma=\bigcap_n\Gamma_n$ is as required (p. 17).

Significance

The result. The variational lemma converts optimality of a martingale plan, a property of a measure, into a condition on finite configurations of points in its support. In the paper it is applied, together with a lemma on accumulation points of sections (Lemma 3.2), to show that optimizers for costs $h(y-x)$ with $h'$ strictly convex are left-monotone, which by the paper's Theorem 1.5 identifies them as the left-curtain coupling; it also yields the bound $|\operatorname{spt}\pi_x|\le k$ of Theorem 7.1 and the two-graph structure of the optimizers for $\pm|y-x|$. Later missions of this series use it as a milestone. Its converse, under continuity assumptions, is the separate Lemma A.2 of the paper's appendix.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization needs a usable form of Kellerer's duality for multi-marginal problems, which is not in Mathlib, and the bookkeeping that finite rearrangements of a martingale plan stay in $\Pi_M(\mu,\nu)$. Both are reusable well beyond this paper: Kellerer's theorem underlies the analogous results for classical, multi-marginal and martingale transport.

Difficulty

The classical proof of $c$-cyclical monotonicity perturbs an optimal plan by moving a small amount of mass around a finite cycle of its support points. For martingale plans this fails: the perturbation must preserve the conditional barycentre of every $x$, and mass sitting at isolated points of a non-atomic plan cannot be moved without moving mass at uncountably many other points. The proof therefore cannot argue point by point. It works with whole families of bad configurations at once, which requires the measure-theoretic duality of Kellerer (resting on Choquet's capacitability theorem) and a measurable choice of an optimal competitor for each configuration. Proving that the set of bad configurations is Borel, and that a positive-mass family of them can be glued into a cheaper competitor $\omega'$ of a piece $\omega\le\pi$, is the technical core.

Formalization scope

The Lean development uses Mathlib's Measure ℝ and Measure (ℝ × ℝ). Costs and integrals that may be infinite take values in EReal, through the published definition ModelRiskOT.Duality.extIntegral ($\int f^+-\int f^-$, with $(+\infty)-(+\infty)=-\infty$); no Bochner integral of a possibly non-integrable function is compared. Martingale plans and competitors are encoded through test functions $\rho(x)$ (the paper's characterization (4), p. 10) instead of disintegrations. A finitely supported finite measure is written $\sum_{s\in S}w_s\delta_s$ with $S$ a finite set and weights $w_s\ge0$; this covers every such measure, and masses are taken finite. $(\mathbb R^2)^n$ is Fin n → ℝ × ℝ.

Committed conventions and disclosed additions:

• the goal's hypothesis "leads to finite costs" is $\int c\,d\pi<+\infty$; without it, a cost under which every plan has infinite cost makes optimality empty;
• Theorem 3.1 is stated for Borel $M$, the case proved in the cited source and the only case the paper uses; $\zeta(\operatorname{proj}^iM_i)=0$ is the outer measure, since the projections need not be Borel;
• in milestone 3, $\Gamma_n$ is a Borel subset of the paper's $\mathbb R^2\setminus N$ of full measure, because $N$ need not be Borel;
• milestone 4 states, for the uniform measure $\alpha_p$ on the points of an $n$-tuple $p$, both that an optimal competitor $\alpha'_p$ exists and that it can be chosen measurably in $p$ (p. 18), with Mathlib's σ-algebra on the space of measures.

A formalization in which $\Gamma$ is empty or $\pi$-null, or in which $\Gamma$ is allowed to depend on $\alpha$, is trivial and is ruled out by the statement: $\pi(\Gamma^c)=0$ and $\exists\Gamma\,\forall\alpha$. The competitor $\alpha'$ ranges over all measures, not only finitely supported ones.

Welcome contributions: a general form of Kellerer's duality theorem (milestone 1), the Borel-measurability of the bad set, and the gluing step of milestone 6.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509, doi:10.1214/14-AOP966
• M. Beiglböck, M. Goldstern, G. Maresch, W. Schachermayer, Optimal and better transport plans, J. Funct. Anal. 256(6), 1907–1927, 2009. doi:10.1016/j.jfa.2009.01.013
• H. G. Kellerer, Duality theorems for marginal problems, Z. Wahrsch. Verw. Gebiete 67(4), 399–432, 1984. doi:10.1007/BF00532047
• M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17(3), 477–501, 2013. doi:10.1007/s00780-013-0205-8
• C. Villani, Optimal Transport, Old and New, Springer, 2009. doi:10.1007/978-3-540-71050-9

Motivation

Peaceman–Rachford splitting and its relaxed forms solve the problem of minimizing a sum $f+g$ by evaluating the two proximal maps separately. This is useful when minimizing either function by itself is simple while minimizing their sum directly is not. Douglas–Rachford splitting is the half-relaxed case. Davis and Yin study which properties of $f$ and $g$ turn the basic convergence of this iteration into quantitative rates. Their Theorem 2.1 supplies the regularity estimates used throughout their later objective and fixed-point analyses (Davis and Yin, arXiv:1407.5210v3, §§1–2).

The theorem measures progress using a term that can respond to strong convexity, a Lipschitz gradient, or both. Its conclusions distinguish three observations of the same run: the best iterate found so far, a weighted average of the auxiliary points, and the current iterate. This distinction matters because a rate for a best iterate need not hold for every iterate; the authors explicitly leave open whether their best-iterate conclusion can be improved in that way (Davis and Yin, p. 9).

Setting

Let $H$ be a real Hilbert space. The functions $f,g:H\to(-\infty,+\infty]$ are closed, proper, and convex. For a positive step size $\gamma$, the proximal map of $f$ sends $z$ to the unique minimizer of $f(x)+\|x-z\|^2/(2\gamma)$. Define the reflection $R_f=2\operatorname{prox}_{\gamma f}-I$ and likewise $R_g$. The Peaceman–Rachford map is $T_{\mathrm{PRS}}=R_f\circ R_g$. Given relaxation parameters $\lambda_k\in(0,1]$, Algorithm 1 generates

$$z^{k+1}=(1-\lambda_k)z^k+\lambda_kT_{\mathrm{PRS}}z^k.$$

At $z^k$, set $x_g^k=\operatorname{prox}_{\gamma g}(z^k)$ and $x_f^k=\operatorname{prox}_{\gamma f}(R_gz^k)$. These points may differ, so the theorem tracks them separately. Their selected proximal subgradients are $\widetilde\nabla g(x_g^k)=\gamma^{-1}(z^k-x_g^k)$ and $\widetilde\nabla f(x_f^k)=\gamma^{-1}(R_gz^k-x_f^k)$. The tilde means a particular member of a subdifferential when the function is not differentiable (Lemma 1.1, p. 7).

Suppose $z^*$ is a fixed point of $T_{\mathrm{PRS}}$ and put $x^*=\operatorname{prox}_{\gamma g}(z^*)$. Each function $h\in\{f,g\}$ has a nonnegative strong-convexity parameter $\mu_h$ and a nonnegative smoothness parameter $\beta_h$. If $\beta_h>0$, the function is differentiable and its gradient is $\beta_h^{-1}$-Lipschitz; a zero parameter imposes no such property. For the selected subgradients at $x$ and $y$, define the regularity term

$$S_h(x,y)=\max\left\{\frac{\mu_h}{2}\|x-y\|^2,\frac{\beta_h}{2}\|\widetilde\nabla h(x)-\widetilde\nabla h(y)\|^2\right\}.$$

The partial relaxation weight is $\Lambda_k=\sum_{i=0}^k\lambda_i$. All of these conventions are from the paper's notation, Algorithm 1, and equations (1.13)–(1.14) (Davis and Yin, pp. 3–8).

Formalization targets

One-step and summed bounds

The goal first asserts the exact one-step inequality (2.1):

$$8\gamma\lambda_k\bigl(S_f(x_f^k,x^*)+S_g(x_g^k,x^*)\bigr)\le \|z^k-z^*\|^2-\|z^{k+1}-z^*\|^2+ \left(1-\frac1{\lambda_k}\right)\|z^{k+1}-z^k\|^2.$$

It also asserts that $\sum_{i\ge0}\lambda_i(S_f(x_f^i,x^*)+S_g(x_g^i,x^*))$ converges and that eight times $\gamma$ times this sum is at most $\|z^0-z^*\|^2$. These are Theorem 2.1's common quantitative bounds (p. 8).

Best-iterate, ergodic, and nonergodic rates

If the $\lambda_j$ are bounded below by a positive constant, the minimum through $k$ of each regularity term is $o(1/(k+1))$. The weighted averages of $x_f^i$ and $x_g^i$, together with the matching weighted averages of their selected subgradients, have regularity terms whose sum is at most $\|z^0-z^*\|^2/(8\gamma\Lambda_k)$. Finally, if the products $\lambda_j(1-\lambda_j)$ have a positive lower bound, the sum of the two current regularity terms is $o(1/\sqrt{k+1})$ (Theorem 2.1, p. 9).

Significance

Strong convexity makes the regularity term control squared distance to $x^*$; a positive smoothness parameter makes it control the difference between selected gradients. Theorem 2.1 therefore connects properties of the objectives to rates for quantities produced by Algorithm 1. The one-step bound is also the stated input to later linear-convergence arguments in the same paper (§4, pp. 13–16). Without this result, those applications lack their common quantitative estimate.

The paper proves Theorem 2.1. This mission asks for a machine-checked proof of its precise statement and supporting claims, not for a new asymptotic rate. The proximal-map and subdifferential definitions already exist as published formal objects; the reusable remaining work includes their quantitative inequalities and the summable-sequence rate facts. The draft goal and milestones are theorem statements with proof holes and do not yet constitute verified proofs.

Difficulty

The obvious inference from a finite sum of nonnegative regularity terms gives a bound on cumulative error, but it does not directly give little-$o$ rates for the current term. The theorem also separates a best-iterate conclusion from a last-iterate conclusion: the regularity terms need not be monotone, and the stronger condition on $\lambda_j(1-\lambda_j)$ is required for the latter. The ergodic conclusion concerns weighted averages of both points and subgradients, so bounding only the average of pointwise regularity terms does not by itself state the result (Theorem 2.1 and its discussion, pp. 8–9).

Formalization scope

Lean uses EReal for the objectives, a complete real inner-product space for $H$, and published predicates for closed proper convex functions, proximal maps, and subgradients. A proximal map is supplied as a function satisfying the minimization property; uniqueness under the stated assumptions makes it the paper's map. Selected subgradients are fixed difference quotients from Lemma 1.1. The parameters $\mu_f,\beta_f,\mu_g,\beta_g$ are nonnegative, and positive $\beta$ requires a real-valued differentiable function with $\beta^{-1}$-Lipschitz gradient. A fixed point $z^*$ states the solution-existence assumption in the form used by Theorem 2.1. No hypothesis asserts any conclusion of the theorem.

The finite minimum uses the nonempty index range $0,\ldots,k$; little-$o$ uses Mathlib's asymptotic relation at infinity. The denominators $\lambda_k$, $\Lambda_k$, and $\sqrt{k+1}$ are positive under the stated bounds. In supporting objective inequalities, conversion from EReal to real numbers occurs only at proximal outputs and points with subgradients, where function values are finite. The printed unweighted, repeated-$k$ subgradient sum in the ergodic clause is corrected to the $\lambda_i$-weighted average consistent with the page's definition of $\bar x_f^k$ and with the result it states. Contributions proving the exact goal, any milestone, or reusable proximal and sequence lemmas are in scope.

Selected references

• Damek Davis and Wotao Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions, Mathematics of Operations Research 42(3), 2017; preprint arXiv:1407.5210v3, 2015. arXiv · DOI

Why lost-sales inventory with lead times matters

In many retail and spare-parts settings, demand that cannot be met from stock is lost rather than backlogged, and replenishment orders arrive only after a positive lead time. The resulting lost-sales inventory model is a basic model of inventory theory. Its optimal policy depends on the whole pipeline of outstanding orders, so dynamic programming over that state becomes intractable as the lead time grows. This is why the model is often replaced by its backlogged counterpart, even when that approximation is poor (Bijvank and Vis, 2011).

Simple heuristics are therefore of practical interest. The simplest is the constant-order policy, which orders the same amount in every period regardless of the state. Reiman (2004, unpublished manuscript) showed that the best constant-order policy sometimes outperforms the base-stock policy, and Goldberg, Katz-Rogozhnikov, Lu, Sharma and Squillante (arXiv:1211.4063, Math. Oper. Res. 2016) proved that it is asymptotically optimal as the lead time grows, with a gap that decays polynomially in the lead time. Xin and Goldberg (arXiv:1409.1499v2, Oper. Res. 2016) proved that for the infinite-horizon average-cost problem the gap actually decays exponentially, with an explicit rate and explicit constants. This mission formalizes that result.

Timeline:

• 1958: Karlin and Scarf introduce the lost-sales model with a positive lead time; convexity results follow in Karlin and Scarf (1958) and Morton (1969).
• 1962: Kingman bounds how fast the expected waiting time of an initially empty GI/G/1 queue approaches its steady-state value (doi).
• 2004: Reiman finds that the best constant-order policy can outperform the base-stock policy.
• 2009: Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 55(3)) prove base-stock policies asymptotically optimal as the lost-sales penalty grows.
• 2011: Huh, Janakiraman and Nagarajan (Operations Research 59(1)) give the existence of stationary optimal policies used by the paper.
• 2015–2016: Goldberg et al. prove asymptotic optimality of constant-order policies as the lead time grows; Xin and Goldberg prove exponential decay of the gap.

The setting

Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with law $\mathcal D$, finite mean $\mathbb E[D]$ and strictly positive variance. The lead time $L\ge1$ is an integer, $h>0$ is the unit holding cost and $p>0$ the unit lost-sales penalty. At the start of period $t$ there is on-hand inventory $I_t$ and a pipeline $\mathbf x_t=(x_{1,t},\dots,x_{L,t})$ of orders placed but not yet delivered. In each period, $x_{1,t}$ arrives, a new order is placed (it enters the end of the pipeline), demand $D_t$ is realized, and the period cost

$$C_t=h\,(I_t+x_{1,t}-D_t)^++p\,(I_t+x_{1,t}-D_t)^-$$

is incurred; then $I_{t+1}=(I_t+x_{1,t}-D_t)^+$. The system starts empty. A policy $\pi$ chooses orders from the information available, and its long-run average cost is $C(\pi)=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$. The optimal cost is $\mathrm{OPT}(L)=\inf_\pi C(\pi)$.

The constant-order policy $\pi_r$ orders $r$ in every period. Its cost is governed by the random walk $jr-\sum_{i=1}^jD_i$ through

$$I^r_\infty=\sup_{j\ge0}\Big(jr-\sum_{i=1}^jD_i\Big),\qquad I^r_L=\max_{j=0,\dots,L}\Big(jr-\sum_{i=1}^jD_i\Big),$$

the steady-state and $L$-th waiting times of a single-server queue with interarrival law $\mathcal D$ and constant service time $r$. The best constant order $r_\infty$ is the least minimizer of $C(\pi_r)$ over $0\le r\le\mathbb E[D]$. The rate and constants are

$$\gamma=\inf_{\theta\ge0}e^{\theta r_\infty}\mathbb E[e^{-\theta D}],\qquad g=\inf_{x\in\mathbb R}\mathbb E\big[h(x-D)^++p(x-D)^-\big],$$

with $\vartheta$ the largest minimizer in the definition of $\gamma$ ($\vartheta=\infty$ if the infimum is not attained, and $1/\infty=0$).

Formalization targets

Goal: Theorem 1 (p. 8)

$$\frac{C(\pi_{r_\infty})}{\mathrm{OPT}(L)}\le1+h\big((1-\gamma)g\big)^{-1}\Big(\mathbb E[D]-r_\infty+\big(e\vartheta(L+1)\big)^{-1}\Big)\gamma^{L+1}\qquad\text{for all }L\ge1 .$$

The quantities $r_\infty,\gamma,\vartheta,g$ depend on $\mathcal D,h,p$ but not on $L$.

Milestones, in the order the proof uses them

• Eq. (3): $C(\pi_r)=h\,\mathbb E[I^r_\infty]+p\,\mathbb E[D]-pr$ for $r\in[0,\mathbb E[D])$.
• Sec. 2.2: the best constant exists and $r_\infty<\mathbb E[D]$; Sec. 2.3: $\vartheta>0$, $\gamma\in[0,1)$, $g>0$ and $\mathrm{OPT}(L)\ge g$.
• Observation 1 (convexity of $\mathfrak f_{\mathbf d}$ and a Jensen bound) and Lemma 2: $\mathrm{OPT}(L)\ge C_L(r_L)$ and the decomposition (5) of $C(\pi_{r_\infty})-\mathrm{OPT}(L)$.
• Lemma 3 (Kingman's series and the tail bound), Lemma 4 ($r_\infty\le r_L$), Lemma 5 ($\sum_n\mathbb P(nr_\infty\ge\sum_{i\le n}D_i)\ge p/h$), the Chernoff step $\mathbb P(nr_\infty\ge\sum_{i\le n}D_i)\le\gamma^n$, and the bound on the term (6).
• Further: Lemma 1 (monotonicity of $\gamma$ in $p/h$) and Corollary 1 (the closed form for exponential demand).

Significance

The theorem shows that a lead time of order $\log(\epsilon^{-1})$ suffices for the constant-order policy to be within a factor $1+\epsilon$ of optimal, whereas the earlier bounds of Goldberg et al. needed a lead time polynomial in $\epsilon^{-1}$. The constants are explicit and computable from the demand law: for exponential demand with $p=h$ and $L=1$ the bound is already about $3.36$, and it approaches $1$ quickly as $L$ grows (Table 1 of the paper). Lemma 1 adds that the rate $\gamma$ worsens as $p/h$ grows, the regime opposite to the one in which base-stock policies are known to be nearly optimal.

The result is proved on paper; no machine-checked proof is known to exist. A formalization would produce a checked infinite-horizon lost-sales model and a checked statement of Kingman's random-walk identities for this queue. It would also produce checked comparisons of an arbitrary history-dependent policy with constant-order policies through convexity. The statement here is taken over a policy class at least as large as the paper's, so a proof also extends the result to randomized history-dependent policies.

Difficulty

The cost of the constant-order policy is the expected supremum of a random walk, while the optimal policy has no closed form and may not even induce a stationary distribution. The paper avoids the steady state of the optimal policy by constructing a random vector with the needed stationarity properties (Theorem 2). That construction is not part of this mission. Here, the lower bound on $\mathrm{OPT}(L)$ in Lemma 2 instead goes through the published, proved lower certificate for the full policy class. The second obstacle is quantitative: the exponential rate comes from comparing the minimizers $r_\infty$ and $r_L$ of two different convex functions (Lemma 4) and from a first-order optimality condition involving a non-differentiable expectation (Lemma 5). Neither follows from the observation that one function dominates the other.

Formalization scope

The model is the published CappedBaseStock model: zero-based time, an empty initial state, demand laws on $[0,\infty)$ with finite positive mean, and costs and long-run averages in $[0,\infty]$. $\mathrm{OPT}(L)$ is the infimum over all measurable, history-dependent, possibly randomized policies. That class contains the paper's Markov deterministic class $\Pi$, so every statement involving $\mathrm{OPT}(L)$ is at least as strong as printed. "Strictly positive variance" is encoded as "the demand law is not a point mass". It is a hypothesis wherever the paper's argument needs it; the Chernoff step, eq. (3) and Corollary 1 do not need it.

$C(\pi_r)$ is the model's long-run cost of the constant policy, not formula (3), and $\mathbb E[I^r_\infty]$ is a lower integral in $[0,\infty]$, so that eq. (3) and Lemma 3 are not true by definition. $r_\infty$ and $r_L$ are infima of the argmin sets, whose nonemptiness is a milestone. $1/\vartheta$ is encoded with the paper's convention $1/\infty=0$. Lemma 3's tail bound is stated additively in $[0,\infty]$, and the series in Lemmas 3 and 5 are extended-real series indexed from $0$. The goal's ratio is taken in $[0,\infty]$, where $x/0=\infty$ for $x\neq0$. None of $\gamma<1$, $g>0$ or $r_\infty<\mathbb E[D]$ is assumed: all three are milestones. A formalization that defines $\mathrm{OPT}$ over constant-order policies only, fixes $r$ instead of $r_\infty$, treats $\gamma,\vartheta,g$ as free parameters, or takes the ratio in $\mathbb R$ after truncating infinite costs would make the goal trivial and is ruled out. The objects are defined from the full parameter record, which includes $L$. That they do not depend on $L$ follows from eq. (3) and the existence milestone.

No statement corrects a printed slip. Theorem 2 (existence of the stationary vector) and eq. (2) (bounded stationary optimal policies) are not stated; Observation 1 instead takes Theorem 2's properties (i)–(iii) as hypotheses on an arbitrary law. The source is arXiv:1409.1499v2, whose printed page numbers equal the PDF's. Useful infrastructure: Lindley-type random-walk suprema, Spitzer–Kingman identities, Chernoff bounds for i.i.d. sums (Mathlib's measure_le_le_exp_mul_mgf), and Cesàro limits of expected costs. All of it is reusable for other queueing and inventory missions. Proofs of any milestone are welcome, and the Chernoff step is the natural entry point.

Selected references

• L. Xin, D. A. Goldberg, Optimality gap of constant-order policies decays exponentially in the lead time for lost sales models, Operations Research 64(6), 2016; preprint arXiv:1409.1499v2. https://arxiv.org/abs/1409.1499v2
• 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.4063. https://arxiv.org/abs/1211.4063
• J. F. C. Kingman, Some inequalities for the queue GI/G/1, Biometrika 49, 1962. https://doi.org/10.1093/biomet/49.3-4.315
• M. Bijvank, I. F. A. Vis, Lost-sales inventory theory: a review, European Journal of Operational Research 215(1), 2011. https://doi.org/10.1016/j.ejor.2011.02.004
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

Small complete caps in Galois spaces

A cap in an affine or projective space over a finite field is a set of points no three of which are collinear; a cap is complete when it is maximal with respect to inclusion, so that every point outside it lies on a line through two of its points. Caps are closely connected with error-correcting codes: projective caps can serve as parity-check columns for linear codes with minimum distance at least 4. Constructing small complete caps explicitly is a long-standing question in finite geometry; Giulietti's survey collects the known families.

Counting the lines through pairs of points gives the trivial lower bound

$$\sqrt{2} \cdot \sqrt{q^{n-1}} \qquad (1)$$

for the size of a complete cap in a Galois space of dimension $n$ and order $q$. A short timeline:

• Segre (1959) constructed complete caps of size $3q + 2$ in $PG(3, q)$, $q$ even.
• Pambianco and Storme (1996) generalized this to complete caps of size $2q^s$ in $AG(2s+1, q)$, $q$ even: bound (1) is sharp up to a constant in odd dimension, for even $q$.
• Giulietti (2007) studied translation caps in $AG(r, 2^t)$ and the doubling construction, which turns a translation cap of the largest possible size into a complete cap one dimension higher.
• Bartoli, Giulietti, Marino and Polverino (arXiv 2015, Combinatorica 2017) proved that (1) is sharp up to a constant also in even dimension $n \ge 4$, when $q$ is an even square. This mission formalizes that result.

Setting

Let $q = 2^t$ and let $\mathbb F_q$ be the field with $q$ elements. The affine space $AG(r, q)$ has as points the vectors $(a_1, \dots, a_r) \in \mathbb F_q^r$; three points are collinear when they lie on a common affine line over $\mathbb F_q$.

For an additive subgroup $G$ of $\mathbb F_q^r$, $\mathcal K_G$ is the set of points whose coordinate vectors lie in $G$. A translation cap is a cap of the form $\mathcal K_G$. By Giulietti, Proposition 2.5, for $t > 1$ a translation cap has at most $q^{r/2}$ points; one attaining this bound is a maximal translation cap.

On the projective side, let $V = \mathbb F_{2^t}^r$, so that $PG(V, \mathbb F_{2^t}) = PG(r-1, 2^t)$. An $\mathbb F_2$-subspace $U$ of $V$ (an additive subgroup) of $\mathbb F_2$-dimension $k$, the rank, defines the $\mathbb F_2$-linear set $L_U = \{\langle u \rangle_{\mathbb F_{2^t}} : u \in U \setminus \{0\}\}$. It is scattered when every point $\langle u\rangle$ meets $U$ in exactly $\{0, u\}$, i.e. has weight one. A scattered linear set has rank at most $rt/2$ (Blokhuis–Lavrauw); one of rank $3t/2$ in the plane $PG(2, 2^t)$ is called maximum.

Formalization targets

Goal: Theorem 1.3

For $q = 2^t$, $t$ even, and $n \ge 4$ even, there is a complete cap $S$ in $AG(n, q)$ with

$$|S| = 2\sqrt{q^{n-1}}.$$

The exponent $t(n-1)/2$ is an integer because $t$ is even.

Milestones

1. Theorem 4.2 ([6, Lemma 2.1]): for $q$ even, $\mathcal K_G$ is a translation cap iff any two distinct non-zero vectors of $G$ are $\mathbb F_q$-linearly independent.
2. Proposition 4.3: for $t > 1$, $L_U$ is a scattered $\mathbb F_2$-linear set of $PG(r-1, 2^t)$ iff $\mathcal K_U$ is a translation cap of $AG(r, 2^t)$.
3. The bound of [6, Prop. 2.5]: a translation cap in $AG(r, 2^t)$, $t > 1$, has at most $q^{r/2}$ points.
4. Lemma 4.5 ([6, Prop. 2.8]): the product of maximal translation caps in $AG(r, 2^t)$ and $AG(\bar r, 2^t)$ is a maximal translation cap in $AG(r + \bar r, 2^t)$.
5. The parabola $\{(x, x^2) : x \in \mathbb F_{2^t}\}$ is a translation cap in $AG(2, 2^t)$.
6. Lemma 4.6 (doubling, [6, Cor. 2.12]): if $\mathcal K_G$ is a maximal translation cap in $AG(r, 2^t)$, then $\mathcal K_{G \times \{0,1\}}$ is a complete cap in $AG(r+1, 2^t)$.
7. Proposition 4.7: a maximum scattered linear set in $PG(2, q)$ yields a complete cap in $AG(n, q)$ of size $2q^{(n-1)/2}$.
8. The existence input, restated from Section 2: Lemma 2.8 and Proposition 2.9 (a suitable coefficient $b$), Theorem 2.10 (the scattered $\mathbb F_2$-linear set $\{x^2 + bx^{2^{2n+1}} + x\omega\}$ of rank $3n$ in $PG(2, 2^{2n})$, covering $t = 2n \ge 4$), and the Baer-subplane case $r = 3$, $t = 2$ (covering $q = 4$).

Significance

Theorem 1.3 shows that the trivial bound (1) is sharp up to the factor $\sqrt 2$ in even dimension $n \ge 4$ for every even square $q$, extending to even dimension what the constructions of Segre and Pambianco–Storme give in odd dimension. The construction supplies caps near the elementary size lower bound in a parameter range where the paper reports no comparably small infinite family. Remark 4.8 of the paper extends the construction to complete caps of comparable size in $PG(n, q)$. The proof also establishes Proposition 4.3, a dictionary between scattered $\mathbb F_2$-linear sets and translation caps, so that any new maximum scattered linear set yields new small complete caps.

The result is proved on paper; no machine-checked proof of it or of the cited results of [6] (Lemmas 4.5, 4.6 and the bound of Prop. 2.5, whose proofs are not in this paper) is known to exist. The mission produces a formal statement of Theorem 1.3, the cap–linear set correspondence, and formal statements of the three results the paper imports from [6].

Difficulty

Assembling Proposition 4.7 from the milestones is short. The difficulty lies in the inputs. The doubling construction requires showing that every point of $AG(r+1, q)$ outside $\mathcal K_{G\times\{0,1\}}$ lies on a secant, which uses the maximality $|G| = q^{r/2}$ in a counting argument; it is cited from [6], not proved in the paper. The existence of a maximum scattered linear set in $PG(2, 2^t)$ is the deep input: Lemma 2.8 needs a bound on the value set of a non-permutation polynomial (Turnwald) and a point count on a plane curve over $\mathbb F_{2^{3n}}$. A tempting shortcut, taking any maximal cap obtained by greedy extension, gives a complete cap of unknown and generally much larger size; the content of the theorem is the exact size.

Formalization scope

• $AG(r, q)$ is Fin r → K for a finite field $K$ with $|K| = 2^t$; collinearity is Mathlib's affine Collinear K, over $K$ itself. A complete cap is quantified against every point of $AG(r, q)$.
• Sizes are Set.ncard. The goal's size $2\sqrt{q^{n-1}}$ is written $2\cdot 2^{t(n-1)/2}$ with natural-number division, exact because $t$ is even; maximality of a translation cap is the squared form $|S|^2 = q^r$, and the [6] bound is $|S|^2 \le q^r$.
• Scattered-ness is the weight-one condition "$c\,u \in U$, $c \in \mathbb F_{2^t}$, $u \ne 0$ imply $c \in \mathbb F_2$"; rank $k$ means $|U| = 2^k$. "Maximum" in Proposition 4.7 is read as rank $3t/2$, as in the first line of its proof.
• In Section 2, $\mathbb F_{2^m}$ is the fixed field of $x \mapsto x^{2^m}$ inside $E$ with $|E| = 2^{6n}$; norms are explicit Frobenius products. $\omega$ ranges over all of $\mathbb F_{2^{2n}} \setminus \mathbb F_{2^n}$ (the paper's standing $\omega$). Proposition 2.9 carries the standing assumption $n \ge 2$ of Section 2.
• Lemmas 4.5, 4.6 and the [6] bound carry $t > 1$; for $t = 1$ every subset of $AG(r, 2)$ is a cap and Lemma 4.6 fails.
• Ruled out: stating the goal with $\le$ or $\ge$ in place of the exact size, or measuring collinearity over $\mathbb F_2$ (over which every set is a cap), would make it trivial.
• Citation basis: arXiv:1512.07467v1; all theorem numbers and pages refer to that version.

Welcome contributions: a general library of caps and translation caps in $AG(r, q)$; the scattered-linear-set/translation-cap dictionary; a formalization of the doubling construction of [6]; transport of the $\mathbb F_{2^{6n}}$-model of Theorem 2.10 to coordinates $\mathbb F_{2^{2n}}^3$. The linear-set definitions mirror those of the companion mission on scattered linear sets and are reusable there.

Selected references

• D. Bartoli, M. Giulietti, G. Marino, O. Polverino, Maximum scattered linear sets and complete caps in Galois spaces, arXiv:1512.07467v1, 2015; Combinatorica 37 (2017). arXiv:1512.07467v1
• [3] A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243. https://doi.org/10.1023/A:1005283806897
• [6] M. Giulietti, Small complete caps in PG(N, q), q even, J. Combin. Des. 15(5) (2007), 420–436. https://doi.org/10.1002/jcd.20131
• [7] M. Giulietti, The geometry of covering codes: small complete caps and saturating sets in Galois spaces, in Surveys in Combinatorics 2013, LMS Lecture Note Series 409, Cambridge University Press, 2013, pp. 51–90. https://doi.org/10.1017/CBO9781139506748.003
• [17] F. Pambianco, L. Storme, Small complete caps in spaces of even characteristic, J. Combin. Theory Ser. A 75(1) (1996), 70–84. https://doi.org/10.1006/jcta.1996.0064
• [19] B. Segre, On complete caps and ovaloids in three-dimensional Galois spaces of characteristic two, Acta Arith. 5 (1959), 315–332. https://doi.org/10.4064/aa-5-3-315-332
• [20] G. Turnwald, A new criterion for permutation polynomials, Finite Fields Appl. 1 (1995), 64–82. https://doi.org/10.1006/ffta.1995.1005

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

The alternating direction method of multipliers (ADMM) solves linearly constrained problems whose objective splits into separately treatable blocks. For two blocks, $\min\{\theta_1(x_1)+\theta_2(x_2) : A_1x_1+A_2x_2=b\}$, it alternates one minimisation of the augmented Lagrangian in each block with a multiplier update. Its convergence for closed convex $\theta_1,\theta_2$ has been known since the work of Glowinski–Marrocco (1975) and Gabay–Mercier (1976), and the survey of Boyd, Parikh, Chu, Peleato and Eckstein (2011) made it a standard tool in statistics, imaging and machine learning.

Many applications have three or more blocks: robust principal component analysis with noisy and incomplete data, latent-variable graphical model selection, image alignment. Practitioners therefore apply the direct extension of ADMM, which simply cycles through all blocks in Gauss–Seidel order before updating the multiplier. Whether this extension converges for convex problems remained open for years: convergence was known under extra assumptions (strong convexity with a restricted penalty, Han–Yuan 2012; orthogonality of coefficient matrices, Section 2 of the source paper), and modified schemes with correction steps were proposed precisely because no proof was available.

Chen, He, Ye and Yuan (Math. Program., 2014) settled the question negatively by an explicit three-block example. This mission formalizes that example and the paper's main theorem.

Setting

Problem (1.1). Given $A_i\in\mathbb R^{p\times n_i}$, $b\in\mathbb R^p$, closed convex sets $\mathcal X_i\subseteq\mathbb R^{n_i}$ and convex functions $\theta_i:\mathbb R^{n_i}\to\mathbb R$ $(i=1,2,3)$, with a nonempty solution set,

$$\min\ \theta_1(x_1)+\theta_2(x_2)+\theta_3(x_3)\quad\text{s.t.}\quad A_1x_1+A_2x_2+A_3x_3=b,\ x_i\in\mathcal X_i .$$

Augmented Lagrangian (1.6). For a penalty $\beta>0$ and multiplier $\lambda\in\mathbb R^p$,

$$\mathcal L_{\mathcal A}(x_1,x_2,x_3,\lambda)=\sum_{i=1}^3\theta_i(x_i)-\lambda^T(A_1x_1+A_2x_2+A_3x_3-b)+\tfrac{\beta}{2}\|A_1x_1+A_2x_2+A_3x_3-b\|^2 .$$

Direct extension of ADMM (1.5). From $(x_2^k,x_3^k,\lambda^k)$: $x_1^{k+1}$ minimises $\mathcal L_{\mathcal A}(\cdot,x_2^k,x_3^k,\lambda^k)$ over $\mathcal X_1$; $x_2^{k+1}$ minimises $\mathcal L_{\mathcal A}(x_1^{k+1},\cdot,x_3^k,\lambda^k)$ over $\mathcal X_2$; $x_3^{k+1}$ minimises $\mathcal L_{\mathcal A}(x_1^{k+1},x_2^{k+1},\cdot,\lambda^k)$ over $\mathcal X_3$; and $\lambda^{k+1}=\lambda^k-\beta(A_1x_1^{k+1}+A_2x_2^{k+1}+A_3x_3^{k+1}-b)$. A sequence satisfying these four conditions for every $k$ is a run (IsRun15).

The example. System (3.1) is $A_1x_1+A_2x_2+A_3x_3=0$ with columns $A_i\in\mathbb R^3$, scalar unknowns, zero objective, $b=0$ and $\mathcal X_i=\mathbb R$; its unique solution is $x=0$ when $[A_1,A_2,A_3]$ is nonsingular. The paper takes

$$A=(A_1,A_2,A_3)=\begin{pmatrix}1&1&1\\1&1&2\\1&2&2\end{pmatrix}\qquad(3.10),$$

the instance example310. With the scaled multiplier $\mu=\lambda/\beta$, the state is $z=(x_2,x_3,\mu_1,\mu_2,\mu_3)\in\mathbb R^5$ (stateVec). The $5\times5$ matrices $L$ (3.6) and $R$ (3.7) are built from the inner products $A_i^TA_j$ and the columns, and $M=L^{-1}R$ (3.9).

Formalization targets

Goal: Theorem 3.1

For the instance (3.10), which satisfies the standing assumptions of (1.1), there are a three-dimensional subspace $S\subseteq\mathbb R^5$ and a nonzero linear functional $\varphi$ on $S$ such that for every $\beta>0$ and every starting point with

$$\bigl(x_2^0,\,x_3^0,\,\lambda^0/\beta\bigr)\in S,\qquad \varphi\bigl(x_2^0,x_3^0,\lambda^0/\beta\bigr)>0,$$

a run of (1.5) from $(x_2^0,x_3^0,\lambda^0)$ exists and no such run converges.

Milestones

1. (3.4)–(3.5): on (3.1), every run satisfies $x_1^{k+1}=\frac{1}{A_1^TA_1}(-A_1^TA_2x_2^k-A_1^TA_3x_3^k+A_1^T\mu^k)$ and $Lz^{k+1}=Rz^k$, with $L,R$ independent of $\beta$.
2. (3.8)–(3.9): $z^k=M^kz^0$.
3. $L$, $R$, $M$ for (3.10): the printed $5\times5$ matrices, $\det L=54$ and $M=L^{-1}R$.
4. $\rho(M)=|d_1|=|d_2|>1$: $M$ has a non-real eigenvalue of maximal modulus, and that modulus exceeds $1$.
5. (3.12)–(3.13): a three-dimensional real subspace and a nonzero functional $\varphi$ on it such that $\|M^kz\|\to\infty$ whenever $\varphi(z)\neq0$.

Significance

The theorem shows that convexity alone does not make the cyclic three-block ADMM convergent, and the failure is robust: it holds for every penalty parameter and for an open half of a three-dimensional subspace of starting points, on a problem as simple as a nonsingular homogeneous linear system with zero objective. It explains why later convergent variants add assumptions (strong convexity, orthogonality, small step sizes, randomised block order) or modify the scheme, and it is the standard reference for that fact in the operator-splitting literature.

The result is proved in the paper; no machine-checked version is known. A formal version produces a certified negative example for the most widely used multi-block splitting heuristic, a reusable formal model of the extended ADMM (Problem, augLag, IsRun15) on which convergent variants can later be stated, and a worked instance of turning a numerically presented spectral argument (the paper prints its eigen-decomposition to four digits) into exact statements.

Difficulty

The first step, that the iteration on (3.1) is linear in $(x_2,x_3,\mu)$ and independent of $\beta$, is elementary but requires extracting minimisers of convex quadratics from the minimiser conditions of the run. The main difficulty is exact spectral information about a specific $5\times5$ rational matrix whose characteristic polynomial is $x$ times an irreducible quartic over $\mathbb Q$ with two pairs of complex roots of moduli about $1.0278$ and $0.9044$. The paper's evidence is a floating-point eigen-decomposition; a proof must instead locate the roots exactly, for example by certified bounds, and must show that the divergent component is present for a whole real subspace of starting points rather than for one numerically chosen vector. Finally, unboundedness of the scaled state has to be transferred back to the original sequence $(x_1^k,x_2^k,x_3^k,\lambda^k)$ for every $\beta>0$.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin p) (Fin n) ℝ, and $\|r\|^2$ in (1.6) is the dot product $r\cdot r$. Each $\theta_i$ is real-valued and convex on all of $\mathbb R^{n_i}$; "closed" is automatic for such functions and is not stated separately. "Argmin" is read as "a minimiser": the run predicate does not select a minimiser, and the goal asserts that a run exists, so the non-convergence claim is not vacuous. The paper's blocks and multiplier components are 1-based, the Lean components 0-based. Convergence of the sequence is convergence of $(x_1^k,x_2^k,x_3^k,\lambda^k)$ in the product topology; $x_1^0$ is never read by (1.5). "Divergent" means "not convergent". The "continuously dense half space of dimension 3" is $\{z\in S:\varphi(z)>0\}$ for a three-dimensional subspace $S$ and nonzero linear $\varphi$, expressed in the coordinates $(x_2^0,x_3^0,\lambda^0/\beta)$; $S$ and $\varphi$ are chosen before $\beta$, as in the paper. Requiring $\dim S=3$ and $\varphi\neq0$ rules out the trivial choices $S=\{0\}$ or $\varphi=0$. Eigenvalues are complex roots of the characteristic polynomial; a statement using only real eigenvalues would be wrong, since the only real eigenvalue of $M$ is $0$. Norms enter only through "$\to\infty$", where the choice of norm on $\mathbb R^5$ is irrelevant. The rounded numbers of (3.11) are not used anywhere.

Every object is defined in ExtADMM.Diverge.Setting. The general definitions (problem, augmented Lagrangian, run) are written for arbitrary dimensions and are intended for reuse by later missions on multi-block splitting. Contributions welcome: proofs of the milestones, exact root localisation for the quartic factor of the characteristic polynomial, and general lemmas such as "a real matrix with an eigenvalue of modulus above one has unbounded orbits on a real subspace".

Selected references

• C. Chen, B. He, Y. Ye, X. Yuan, The direct extension of ADMM for multi-block convex minimization problems is not necessarily convergent, Mathematical Programming 155 (2016) 57–79. https://doi.org/10.1007/s10107-014-0826-5
• D. Gabay, B. Mercier, A dual algorithm for the solution of nonlinear variational problems via finite element approximation, Computers & Mathematics with Applications 2 (1976) 17–40. https://doi.org/10.1016/0898-1221(76)90003-1
• R. Glowinski, A. Marrocco, Sur l'approximation, par éléments finis d'ordre un, et la résolution, par pénalisation-dualité, d'une classe de problèmes de Dirichlet non linéaires, RAIRO Analyse Numérique 9 (1975) 41–76. https://doi.org/10.1051/m2an/197509R200411
• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Foundations and Trends in Machine Learning 3 (2011) 1–122. https://doi.org/10.1561/2200000016
• D. Han, X. Yuan, A note on the alternating direction method of multipliers, Journal of Optimization Theory and Applications 155 (2012) 227–238. https://doi.org/10.1007/s10957-012-0003-z