Optimization

Motivation

Neural networks trained by empirical risk minimization are sensitive to small, deliberately chosen perturbations of their inputs ("adversarial examples"). A standard defence is adversarial training: at each step, perturb the training example to increase the loss, then take a gradient step at the perturbed point. Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) recast adversarial training as distributionally robust optimization over a Wasserstein ball around the data distribution, and replaced the hard ball constraint by a Lagrangian penalty. The resulting procedure perturbs each example by solving a penalized inner maximization, and the paper shows that, when the penalty is large enough relative to the smoothness of the loss, this inner problem is strongly concave and therefore tractable.

This mission formalizes the paper's computational guarantee, Theorem 2: stochastic gradient descent on the penalized robust objective, with an inexact adversary, reaches an approximate stationary point at the rate of smooth nonconvex stochastic optimization. The analysis follows Ghadimi and Lan's argument for nonconvex SGD (arXiv:1309.5549), adapted to a gradient oracle that is biased by the inexact inner maximization.

Setting

Parameters $\theta$ live in $\Theta=\mathbb R^d$ and data in a set $Z\subseteq\mathbb R^m$; both spaces carry the Euclidean norm $\|\cdot\|_2$. Data are drawn from a probability distribution $P_0$ on $Z$.

A transportation cost $c:Z\times Z\to[0,\infty)$ measures how expensive it is to move a data point $z_0$ to $z$. Assumption A: $c$ is continuous, $c(z,z)=0$, and for each $z_0\in Z$ the map $z\mapsto c(z,z_0)$ is $1$-strongly convex. The canonical example is $c(z,z_0)=\tfrac12\|z-z_0\|_2^2$.

A loss $\ell(\theta;z)$ has partial gradients $\nabla_\theta\ell$ and $\nabla_z\ell$. Assumption B: these gradients are Lipschitz in each argument,

$$\|\nabla_\theta\ell(\theta;z)-\nabla_\theta\ell(\theta';z)\|\le L_{\theta\theta}\|\theta-\theta'\|,\quad \|\nabla_z\ell(\theta;z)-\nabla_z\ell(\theta;z')\|\le L_{zz}\|z-z'\|,$$ $$\|\nabla_\theta\ell(\theta;z)-\nabla_\theta\ell(\theta;z')\|\le L_{\theta z}\|z-z'\|,\quad \|\nabla_z\ell(\theta;z)-\nabla_z\ell(\theta';z)\|\le L_{z\theta}\|\theta-\theta'\|.$$

For a penalty $\gamma>0$, the robust surrogate and the robust objective are

$$\varphi_\gamma(\theta;z_0)=\sup_{z\in Z}\{\ell(\theta;z)-\gamma c(z,z_0)\},\qquad F(\theta)=\mathbb E_{P_0}[\varphi_\gamma(\theta;Z)].$$

By Wasserstein duality, $F(\theta)$ equals the worst-case expected loss over all distributions $P$, penalized by $\gamma$ times the transport distance from $P$ to $P_0$.

Algorithm 1 (with $\Theta=\mathbb R^d$ and constant stepsize $\alpha$): from $\theta^0$, for $t=0,\dots,T-1$, draw $z^t\sim P_0$ independently, find an $\epsilon$-approximate maximizer $\hat z^t\in Z$, meaning $\ell(\theta^t;\hat z^t)-\gamma c(\hat z^t,z^t)\ge\varphi_\gamma(\theta^t;z^t)-\epsilon$, and set $\theta^{t+1}=\theta^t-\alpha\nabla_\theta\ell(\theta^t;\hat z^t)$.

Formalization targets

Goal: Theorem 2 (p. 6)

Let $\gamma>L_{zz}$, $L_\varphi=L_{\theta\theta}+L_{\theta z}L_{z\theta}/(\gamma-L_{zz})$, $\Delta_F\ge F(\theta^0)-\inf_\theta F(\theta)$, and assume $\mathbb E\|\nabla F(\theta)-\nabla_\theta\varphi_\gamma(\theta;Z)\|_2^2\le\sigma^2$ for all $\theta$. With $\alpha=\sqrt{\Delta_F/(L_\varphi T\sigma^2)}$ and $T\ge L_\varphi\Delta_F/\sigma^2$,

$$\frac1T\sum_{t=0}^{T-1}\mathbb E\big[\|\nabla F(\theta^t)\|_2^2\big]-\frac{4L_{\theta z}^2}{\gamma-L_{zz}}\,\epsilon\le4\sigma\sqrt{\frac{L_\varphi\Delta_F}{T}}.$$

Milestones

1. (4), p. 4: for $\gamma\ge L_{zz}$, $z\mapsto\ell(\theta;z)-\gamma c(z,z_0)$ is $(\gamma-L_{zz})$-strongly concave.
2. Lemma 1, p. 5: the supremum $\bar f(\theta)=\sup_{z\in Z}f(\theta,z)$ of a $\lambda$-strongly concave family satisfying Assumption B is differentiable, with $\nabla\bar f(\theta)=\nabla_\theta f(\theta,z_\star(\theta))$, a $(L_{z\theta}/\lambda)$-Lipschitz maximizer and a $(L_{\theta\theta}+L_{\theta z}L_{z\theta}/\lambda)$-Lipschitz gradient.
3. §2.1, p. 6: $\varphi_\gamma(\cdot;z_0)$ has $L_\varphi$-Lipschitz gradient $\nabla_\theta\varphi_\gamma(\theta;z_0)=\nabla_\theta\ell(\theta;z_\star(z_0,\theta))$.
4. (31) and (32), p. 40: the descent inequality for an $L_\varphi$-smooth objective, and its form with the bias $\delta=g-\nabla_\theta\varphi_\gamma$ separated, for $\alpha\le1/L_\varphi$.
5. The bias bound, p. 41: $\|\delta\|_2^2\le 2L_{\theta z}^2\epsilon/(\gamma-L_{zz})$.
6. The one-step bound in conditional expectation and the averaged bound, p. 41:

$$\frac1T\sum_{t<T}\mathbb E\|\nabla F(\theta^t)\|_2^2\le2\hat\epsilon+\frac{2\Delta_F}{\alpha T}+2L_\varphi\alpha\sigma^2,\qquad\hat\epsilon=\frac{2L_{\theta z}^2}{\gamma-L_{zz}}\epsilon,$$

for every constant stepsize $0<\alpha\le1/L_\varphi$. The goal is this bound at the balancing stepsize.

Significance

The result. Theorem 2 certifies that the robust training procedure is no harder, in iteration count, than ordinary nonconvex SGD: the stationarity measure decays as $T^{-1/2}$, and the inexactness of the adversary enters only as an additive term proportional to $\epsilon$, independent of $T$. This is what licenses running a few steps of gradient ascent for the inner problem rather than solving it exactly. It also explains the role of the penalty: the guarantee requires $\gamma>L_{zz}$, so smoothness of the loss in the data (smooth activations rather than ReLUs) is what makes the robust problem tractable.

Formalizing it. The result and its proof are published; nothing here is open. To our knowledge none of it is machine-checked. A formal proof would add a verified Danskin-type theorem for strongly concave suprema with explicit Lipschitz constants (Lemma 1), which is reusable well beyond this paper, and a verified nonconvex SGD analysis with a biased oracle, including the measure-theoretic bookkeeping (independence of the fresh sample from the current iterate, differentiation under the integral) that the paper's proof compresses into one line.

Difficulty

The deterministic inequalities (31), (32) and the bias bound are short. The weight sits elsewhere. First, Lemma 1 requires differentiability of a supremum over a possibly unbounded set, with the maximizer depending on $\theta$; the paper invokes a Danskin-type theorem that is not in Mathlib, and the cost $c$ is not assumed differentiable, so the first-order optimality conditions for the inner problem must be derived from strong convexity alone. Second, the expectation step uses $\mathbb E[\nabla_\theta\varphi_\gamma(\theta^t;z^t)\mid\theta^t]=\nabla F(\theta^t)$, which needs both differentiation under the integral sign for $F$ and the independence of $z^t$ from $\theta^t$ along the run. Third, finiteness of every expectation along the run is not assumed and must be propagated from step to step.

Formalization scope

Lean representation: $\Theta$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); $Z$ is a set in the latter. The loss is a function on all of $\mathbb R^d\times\mathbb R^m$; its partial gradients are required at points of $Z$ and the Lipschitz conditions on $Z$ only. Strong convexity is Mathlib's StrongConvexOn, whose modulus convention matches the paper. Suprema are sSup over the image of $Z$. $F$ is a Bochner integral, and $\varphi_\gamma(\theta;\cdot)$ is assumed $P_0$-integrable for every $\theta$. The run is driven by $(z^0,\dots,z^{T-1})\sim P_0^{\otimes T}$ (Measure.pi). The expectations in the conclusion and in the variance hypothesis are lower Lebesgue integrals in $[0,\infty]$; the $\epsilon$-term of Theorem 2 is moved to the right-hand side.

Hypotheses made explicit that the paper leaves implicit: $\gamma>L_{zz}$ (the paper writes $\gamma\ge L_{zz}$ but divides by $\gamma-L_{zz}$); $Z$ nonempty, convex and closed; Lipschitz constants nonnegative; $\sigma>0$, $\Delta_F>0$, $T\ge1$, $\epsilon\ge0$; $F$ bounded below (so $\inf_\theta F$ is a real number); integrability of $\varphi_\gamma(\theta;\cdot)$; $P_0(Z)=1$; joint measurability of the oracle $(\theta,z_0)\mapsto\hat z(\theta,z_0)$; and, in (32) and the later milestones, $0<\alpha\le1/L_\varphi$, which the paper assumes "in the rest of the proof". Lemma 1 is specialized to the Euclidean norm, the case Theorem 2 uses. The cost $c$ is not assumed differentiable.

A trivializing formalization is ruled out: the run uses an oracle tied to $\varphi_\gamma$ by the $\epsilon$-gap and to $Z$ by membership, $\varphi_\gamma$ is the supremum of the penalized loss over $Z$, $F$ is its $P_0$-integral, and the hypotheses are satisfiable (for instance $\ell(\theta;z)=\tfrac12\|\theta\|^2$, $c(z,z_0)=\tfrac12\|z-z_0\|^2$, $Z=\mathbb R^m$, $P_0$ a point mass, $\epsilon=0$). Expectations as lower integrals prevent a non-integrable $\|\nabla F(\theta^t)\|^2$ from being read as $0$.

Infrastructure a complete development needs: the descent lemma for functions with Lipschitz gradient; first-order characterizations of strong concavity on a convex set; a Danskin/envelope theorem for strongly concave suprema; differentiation under the integral for $F$; and conditional-expectation bookkeeping for Markov-type recursions driven by i.i.d. samples on a finite product space. The first three are reusable in any minimax or bilevel analysis. Contributions to any milestone, or to these supporting facts as separate lemmas, are welcome.

Selected references

• A. Sinha, H. Namkoong, R. Volpi, J. Duchi, Certifying Some Distributional Robustness with Principled Adversarial Training, ICLR 2018; arXiv:1710.10571v5, 2020. https://arxiv.org/abs/1710.10571
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. https://doi.org/10.1137/120880811
• J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research 48(2), 2023; arXiv:1604.02199. https://arxiv.org/abs/1604.02199

Motivation

Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) train classifiers against adversarial perturbations by solving a Lagrangian relaxation of a Wasserstein distributionally robust problem. The inner problem, $\sup_z \{\ell(\theta;z)-\gamma\, c(z,z_0)\}$, is strongly concave, and hence solvable by gradient ascent with the paper's certificates, exactly when the penalty $\gamma$ exceeds the input-smoothness constant $L_{zz}$ of the loss: the Lipschitz constant of $z\mapsto\nabla_z\ell(\theta;z)$. For a deep network this constant is not given; §4 of the paper ("Bounds on smoothness of neural networks") supplies an explicit upper bound in terms of the weights' spectral norms and per-layer constants of the activations. The bound tells a practitioner how large $\gamma$ must be for the robustness guarantees to apply, and it is of the same type as the spectral-norm Lipschitz bounds used for adversarial robustness and generalization of deep networks (Szegedy et al. 2014; Bartlett, Foster, Telgarsky 2017), but at the level of the derivative rather than the function.

Setting

A layered network of depth $L$ has widths $d_{l,I}$ (pre-activation of layer $l$) and $d_{l,O}$ (output of layer $l$), with $d_{0,O}=p$ the input dimension and $d_{L,O}=K$ the number of classes. Its parameters are weight matrices $\theta_l:\mathbb R^{d_{l-1,O}}\to\mathbb R^{d_{l,I}}$, and each linear layer is followed by a nonlinear operation $\sigma_l:\mathbb R^{d_{l,I}}\to\mathbb R^{d_{l,O}}$ (an activation, possibly combined with pooling). The output of the first $l$ layers is

$$F_0(\theta;x)=x,\qquad F_l(\theta;x)=\sigma_l\big(\theta_l\cdot F_{l-1}(\theta;x)\big),$$

and its Jacobian in $x$ is $J_xF_l(\theta;x)$. All spaces carry the Euclidean norm $\|\cdot\|_2$, and $\|\cdot\|_{\mathrm{op}}$ is the $\ell_2$-operator (spectral) norm.

Assumption E. For $l=1,\dots,L$, the map $\sigma_l$ is $L^0_l$-Lipschitz for $\|\cdot\|_2$, its Jacobian $J\sigma_l$ is $L^1_l$-Lipschitz from $\|\cdot\|_2$ to $\|\cdot\|_{\mathrm{op}}$, and $L^0_l>0$. From these constants define

$$\alpha_l(\theta)=\prod_{j=1}^{l}L^0_j\,\|\theta_j\|_{\mathrm{op}},\qquad \beta_l(\theta)=\alpha_l(\theta)\sum_{j=1}^{l}\frac{L^1_j}{(L^0_j)^2}\,\alpha_j(\theta).$$

The classification loss is the softmax loss $\ell(\theta;(x,y))=-\log p_y(\theta;x)$ with $p_y(\theta;x)=\exp(F_{L,y}(\theta;x))/\sum_{k=1}^K\exp(F_{L,k}(\theta;x))$, for a class $y\in\{1,\dots,K\}$.

Formalization targets

Goal: Corollary 4

Under Assumption E, for every class $y$ and all inputs $x,x'$,

$$\big\|\nabla_x\ell(\theta;(x,y))-\nabla_x\ell(\theta;(x',y))\big\|_2\le\big(\sqrt2\,\beta_L(\theta)+\alpha_L(\theta)^2\big)\,\|x-x'\|_2 .$$

Proposition 5

Under Assumption E, for $l=1,\dots,L$,

$$\|F_l(\theta;x)-F_l(\theta;x')\|_2\le\alpha_l(\theta)\|x-x'\|_2,\qquad \|J_xF_l(\theta;x)-J_xF_l(\theta;x')\|_{\mathrm{op}}\le\beta_l(\theta)\|x-x'\|_2 .$$

Milestones

In the order the paper's proof uses them: Lemma 6 (the chain rule for $J_xF_l$, recursively and as a product); Proposition 5, first part; the telescoping representation (34) of $J_xF_l(\theta;x)-J_xF_l(\theta;x')$; Proposition 5, second part; the softmax constants of §B.9 (gradient $p(v)-e_y$, Lipschitz constant $\sqrt2$, smoothness constant $1$); and the recursion of §B.9 for $\alpha_l,\beta_l$ with its instance $\beta_{L+1}=\sqrt2\,\beta_L+\alpha_L^2$ for a softmax output layer.

Significance

Corollary 4 converts the abstract hypothesis $\gamma>L_{zz}$ of the paper's convergence and certification results (missions 1 and 2 of this series) into a checkable condition on a trained network: $L_{zz}\le\sqrt2\,\beta_L(\theta)+\alpha_L(\theta)^2$, computable from spectral norms of the weights and from constants of standard activations (the paper lists average pooling, sigmoid and ELU). Proposition 5 is a reusable statement about any composition of smooth maps with linear layers, independent of the softmax and of robust optimization.

The results are proved in the paper (§B.8–§B.9). No machine-checked proof of them is known to exist. This mission produces a formal development of the input Jacobian of a layered network with varying widths, the telescoping estimate for its variation, and the smoothness constants of the softmax loss, all with the paper's explicit constants.

Difficulty

The function-level bound (first part of Proposition 5) is a direct induction. The derivative-level bound is not: the obvious induction on $J_xF_{l+1}=J\sigma_{l+1}\cdot\theta_{l+1}\cdot J_xF_l$ needs both a bound on $\|J_xF_l\|_{\mathrm{op}}$, which comes from the Lipschitz half and the differentiability of every layer, and a bound on the variation of the Jacobian of the previous layers, and the two must be combined so that the constant comes out as exactly $\beta_l(\theta)$ of (21), whose definition uses quotients by $(L^0_j)^2$. For the corollary, the softmax loss must be shown to have Lipschitz constant $\sqrt2$ (a supremum that is not attained) and a $1$-Lipschitz derivative; the paper's eigenvalue argument for the latter is loose and its displayed initial condition for the recursion of the constants is misprinted, so the printed text cannot be transcribed line by line. In Lean, the widths change from layer to layer, so the network is a family of maps between different Euclidean spaces, and every product of Jacobians is a dependently typed composition.

Formalization scope

• Inputs, pre-activations and outputs are EuclideanSpace ℝ (Fin n); weights are continuous linear maps, so ‖θ l‖ is the spectral norm; Jacobians are Fréchet derivatives with the operator norm. A Frobenius or entrywise norm would state a different theorem and is not used.
• Layers are indexed from $0$ in Lean: Lean layer l is the paper's layer $l+1$ (θ l, σ l, L0 l, L1 l); F l, α L0 l, β L0 L1 l carry the paper's index $l$. Widths vary with the layer; they are not collapsed to a single dimension.
• Assumption E is stated for the first $L$ layers and includes two hypotheses implicit on the page: each $\sigma_l$ is differentiable (the assumption speaks of its Jacobian) and $L^1_l\ge0$. The paper's $L^0_l>0$ is kept.
• $\alpha_l$ and $\beta_l$ are the explicit product and sum of (21); they are definitions, not free parameters. Consequently $\alpha_0=1$ and $\beta_0=0$; the paper's "$\beta_0(\theta)=\alpha_0(\theta)=1$" in §B.9 is a misprint and is not followed. The recursion $\beta_{l+1}=(\alpha_{l+1}/\alpha_l)\beta_l+\dots$ is stated in the division-free form $\beta_{l+1}=L^0_{l+1}\|\theta_{l+1}\|_{\mathrm{op}}\beta_l+\dots$, and in the paper's form when $\alpha_l\ne0$.
• In (34) the first displayed line (a "product of differences") is a misprint; only the telescoped sum is formalized.
• The softmax loss is real-valued on $\mathbb R^K$ with $K=d_{L,O}$ and a class $y$ in Fin K; the goal uses Mathlib's gradient, whose norm equals the operator norm of the derivative.
• The goal is not trivialized by free constants: a version with $\alpha,\beta$ as arbitrary parameters, or with the loss not tied to $F_L$, would not be Corollary 4 and is not what is posed.
• Not formalized: the Hessian formula $\nabla^2\sigma_y=\operatorname{diag}p-pp^T$ and the eigenvalue argument (only their conclusion $L^1=1$ is stated); attainment of $\sup_x\|p(x)-e_y\|_2=\sqrt2$ (the value of the supremum, for $K\ge2$, is stated; it is not attained); Examples 1–3 (constants of pooling, sigmoid and ELU).

A complete development needs the chain rule for the network map, the mean value inequality for the softmax loss, and the algebra of (21). The definitions of the layered network and of the softmax loss are independent of robust optimization and are reusable for other Lipschitz and smoothness bounds of deep networks. Proofs of any milestone, and alternative arguments with sharper constants stated as separate theorems, are welcome.

Selected references

• A. Sinha, H. Namkoong, R. Volpi, J. Duchi, Certifying Some Distributional Robustness with Principled Adversarial Training, ICLR 2018; arXiv:1710.10571v5, 2020. https://arxiv.org/abs/1710.10571
• C. Szegedy et al., Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
• P. Bartlett, D. Foster, M. Telgarsky, Spectrally-normalized margin bounds for neural networks, NeurIPS 2017. https://arxiv.org/abs/1706.08498

Motivation

Distributionally robust optimization (DRO) evaluates a decision against a collection of probability distributions near an empirical one. In a finite scenario model, the familiar construction puts a divergence ball around the histogram of observed scenarios. Lam's empirical construction instead gives one weight to each observation, even when several observations have the same value. The distinction matters because a sample can contain repeated values and can omit some points of the stated support. The paper uses a Burg-entropy ball on those observation weights to recover statistical guarantees for an expected loss, despite the empirical ball having low probability of containing the true distribution. Lam, §§2.1–2.3, pp. 5–9.

Proposition 1 identifies what this observation-level construction becomes when the random quantity has finite support: its lower and upper DRO values coincide with values from a Burg-divergence ball on the support histogram. This links a method defined on individual data points to the standard finite-scenario formulation. The radius uses a one-degree-of-freedom chi-square quantile because the paper calibrates an expected value at a fixed decision; it does not use the $k-1$ degrees of freedom associated with estimating a full $k$-point distribution. Lam, Proposition 1, p. 11, and the discussion on pp. 8–9.

Setting

Fix a decision $x$ and a real loss $h(x;s_i)$ at each of $k$ support points $s_1,\ldots,s_k$. A sample of size $n$ has an assignment $c(j)$ telling which support point produced observation $j$. Write $n_i$ for the number of assignments to point $i$ and $\hat p_i=n_i/n$ for the empirical histogram. The support points need not all appear in the sample. The decision and loss only determine a finite vector of loss values; no probability space is needed for this deterministic comparison. Lam, §2.1, p. 6, and Proposition 1, p. 11.

The empirical Burg ball $\mathcal U_n(\eta)$ consists of observation weights $w_1,\ldots,w_n$ that are nonnegative, sum to one, and obey $-n^{-1}\sum_j\log(nw_j)\le\eta$. The support Burg ball $\mathcal U'_{\mathrm{Burg}}(\eta)$ consists of support weights $p_1,\ldots,p_k$ that are nonnegative, sum to one, are absolutely continuous with respect to $\hat p$, and obey $-\sum_i\hat p_i\log(p_i/\hat p_i)\le\eta$. At an observed point, finite Burg divergence requires $p_i>0$; at an unobserved point, absolute continuity requires $p_i=0$. Lam, (13)–(15), pp. 5–6; (19), p. 8; (28), p. 11.

For a support weight vector $p$, the expected loss is $\sum_i p_i h(x;s_i)$. For an observation weight vector $w$, it is $\sum_j w_j h(x;s_{c(j)})$. The empirical lower and upper values are the minimum and maximum over $\mathcal U_n(\eta)$; the support values use $\mathcal U'_{\mathrm{Burg}}(\eta)$. The same empirical ball is used for both bounds. Lam, (26)–(28), p. 11.

Formalization targets

The goal is Proposition 1. For every $n>0$, every assignment of the sample to finite support points, every fixed decision $x$, and every $\kappa\ge0$, set $\eta=\kappa/(2n)$. Then

$$\min_{w\in\mathcal U_n(\eta)}\sum_{j=1}^n w_jh(x;s_{c(j)}) =\min_{p\in\mathcal U'_{\mathrm{Burg}}(\eta)}\sum_{i=1}^k p_ih(x;s_i),$$ $$\max_{w\in\mathcal U_n(\eta)}\sum_{j=1}^n w_jh(x;s_{c(j)}) =\max_{p\in\mathcal U'_{\mathrm{Burg}}(\eta)}\sum_{i=1}^k p_ih(x;s_i).$$

The printed proposition takes $\kappa=\chi^2_{1,1-\alpha}$. The deterministic identity holds at every nonnegative $\kappa$, including zero. The two milestones record the source proof's statements that a feasible support vector gives a feasible observation vector with the same objective value, and conversely that a feasible observation vector gives a feasible support vector with the same objective value. Lam, Proposition 1, p. 11, proof p. 24.

Significance

The identity lets a finite-support user compute the empirical DRO values with one variable per distinct support point instead of one per observation, without changing either bound. It also shows precisely how Lam's empirical calibration relates to a conventional histogram-based divergence model: the ambiguity sets have different coordinates, but the resulting extrema of any loss constant on each class agree. This is the finite-support interpretation stated immediately after Theorem 2, and it explains the radius comparison on pp. 8–9. Lam, pp. 8–9 and Proposition 1, p. 11.

The result is proved in the paper; the remaining task is a machine-checked proof of the two transformations and the equality of extrema. The published formal library already contains the observation-level $\phi$-divergence ball and its robust upper mean, and a shared setting supplies the Burg generator and lower empirical value. This mission adds the support histogram, its Burg ball, and the bridge between the two representations. Those definitions and transformations can also be reused for other finite-support losses. The paper's separate pointwise coverage and consistency results are goals of other missions in this series. Lam, Theorems 2–3 and Proposition 1, pp. 11–12.

Difficulty

Repeated observations make the two weight spaces different: the empirical problem has $n$ coordinates and the support problem has $k$. Simply identifying coordinates loses multiplicities in both the normalization and the logarithmic divergence. Empty classes create a second boundary case, since no observation weight can be assigned to an unobserved support point. A statement that silently permits such mass changes the support optimization value. The full reduction must preserve feasible objective values in both directions, for the lower and upper extrema. Lam, proof of Proposition 1, p. 24.

Formalization scope

Lean uses Fin n for observations and Fin k for support points, with zero-based indices, a class map $c$, real loss values, and the paper's Burg generator valued in EReal. Nonpositive likelihood ratios receive $+\infty$. The empirical ball reuses the published PhiDivRobust.Counterpart.probUncertaintySet; its upper value is the published GenEmpLik.Expansion.robustMean. The lower value is a real infimum over the same ball. The condition $n>0$ and the nonnegative radius make both feasible value sets nonempty and bounded, so the real infimum and supremum mean the paper's minimum and maximum. The histogram can have zero entries. Lam, (19), (26)–(28), pp. 8, 11.

Display (28) omits a condition from the preceding definition of a divergence ball: $p$ must be absolutely continuous with respect to $\hat p$. Without it, an unobserved support point can receive positive mass and Proposition 1 is false. The formal support ball includes $\hat p_i=0\Rightarrow p_i=0$ from (13)–(14). It also requires $p_i>0$ where $\hat p_i>0$, because Lean's real logarithm returns zero at zero whereas the paper's Burg divergence is infinite there. These conditions, together with $n>0$, exclude trivial values from empty balls, division by zero, and logarithms at invalid weights. The decision set $\Theta$ is omitted because the paper fixes one $x$ and the result holds for every such $x$. Lam, (13)–(14), pp. 5–6, and (28), p. 11.

The development needs finite-sum identities, elementary properties of the probability simplex, the logarithm's concavity, and bounds on the extrema of bounded nonempty finite-dimensional value sets. Contributions that establish the two direction statements, or reusable facts about aggregation of finite probability weights, directly advance this mission. The paper's uniform calibration theorem, Theorem 4, is outside this scope: it needs a Donsker class, a data-dependent chi-square process, and its supremum quantile, none of which enters Proposition 1. Lam, Theorem 4, pp. 13–14.

Selected references

• Henry Lam, Recovering Best Statistical Guarantees via the Empirical Divergence-Based Distributionally Robust Optimization, arXiv:1605.09349v1, 2016; published in Operations Research 67(4), 2019. arXiv, DOI.

Motivation

First-order primal-dual methods (PDHG, extragradient, ADMM) are the engine of a new generation of large-scale linear programming solvers, such as PDLP, because they need only matrix–vector products with the constraint matrix. Their textbook guarantees for convex–concave saddle-point problems are sublinear, $O(1/t)$ for the averaged iterate, while in practice restarted variants converge linearly on linear programs. Applegate, Hinder, Lu and Lubin (arXiv:2105.12715v4, Math. Program. 2022) explain this gap through a sharpness condition on the normalized duality gap, and show that restarts turn sharpness into linear convergence.

This mission formalizes the part of that paper which shows that linear programming is sharp: Lemma 5 (p. 15), together with the bound of the KKT residual by the normalized duality gap (Lemma 4, p. 14) and the bilinear results of §3.2. The restart theorems that consume this property are the subject of the companion missions II and III of this series.

Setting

Let $A\in\mathbb R^{m\times n}$, $b\in\mathbb R^m$, $c\in\mathbb R^n$. The standard-form LP and its dual are

$$\min_{x\in\mathbb R^n} c^\top x\ \text{ s.t. } Ax=b,\ x\ge0 \qquad (17), \qquad\quad \max_{y\in\mathbb R^m} b^\top y\ \text{ s.t. } A^\top y\le c \qquad (18),$$

and their Lagrangian form is the saddle-point problem

$$\min_{x\ge0}\ \max_{y\in\mathbb R^m}\ L(x,y)=c^\top x+y^\top b-y^\top Ax. \qquad (19)$$

A primal-dual point is $z=(x,y)$, the feasible region is $Z=\{x\ge0\}\times\mathbb R^m$, and $Z^\star$ is the set of saddle points of $L$ on $Z$. On $\mathbb R^{n+m}$ the norm is the Euclidean norm $\|(x,y)\|=\sqrt{\|x\|_2^2+\|y\|_2^2}$, and $\operatorname{dist}(z,Z^\star)=\inf_{\hat z\in Z^\star}\|z-\hat z\|$.

For $r>0$ let $W_r(z)=\{\hat z\in Z:\|z-\hat z\|\le r\}$. The normalized duality gap (4a) is

$$\rho_r(z)=\sup_{\hat z\in W_r(z)}\frac{L(x,\hat y)-L(\hat x,y)}{r}.$$

The problem is $\alpha$-sharp on a set $S\subseteq Z$ (Definition 1) if $\alpha\,\operatorname{dist}(z,Z^\star)\le\rho_r(z)$ for all $z\in S$ and all $r\in(0,\operatorname{diam}(S)]$.

The KKT system (20) collects primal feasibility, dual feasibility and a nonpositive duality gap as $Kz\ge h$, with

$$K=\begin{pmatrix} I & 0\\ -A & 0\\ A & 0\\ 0 & -A^\top\\ -c^\top & b^\top\end{pmatrix},\qquad h=\begin{pmatrix}0\\-b\\b\\-c\\0\end{pmatrix}.$$

The KKT residual $\|(h-Kz)^+\|$ is the Euclidean norm of the componentwise positive part, a standard stopping criterion of LP solvers. A Hoffman constant $H(K)$ (Hoffman 1952) is a constant with

$$\operatorname{dist}(z,Z^\star)\le H(K)\,\|(h-Kz)^+\|\quad\text{for all } z\in\mathbb R^{n+m}. \qquad (26)$$

Formalization targets

Goal: Lemma 5 (Sharpness of linear programming), p. 15

If (19) has a solution and $H(K)>0$ satisfies (26), then for every $R\in(0,\infty)$ the problem (19) is $\alpha$-sharp on $W_R(0)=\{z\in Z:\|z\|\le R\}$ with

$$\alpha=\frac{1}{H(K)\sqrt{1+4R^2}}.$$

Milestones (proof of Lemma 4, p. 14)

With $v=\big((-c+A^\top y)^+,\ b-Ax\big)$:

$$\text{(22)}\quad \rho_r(z)\ge\|v\|\quad (z\in Z,\ r>0),\qquad\qquad \text{(25)}\quad \rho_r(z)\ge\tfrac1R\,(c^\top x-b^\top y)^+\quad (z\in W_R(0),\ 0<r\le R),$$

and their combination, Lemma 4:

$$\|(h-Kz)^+\|\le\rho_r(z)\sqrt{1+R^2}\qquad (R>0,\ r\in(0,R],\ z\in W_R(0)).$$

Companion statements

• §3.3, p. 13: if (17) and (18) are feasible, $Z^\star=\{z: Kz\ge h\}$, so that (26) is Hoffman's bound for a polyhedron.
• Lemma 2, p. 12: for $S=\{z:Hz=h\}\neq\emptyset$, $\operatorname{dist}(S,z)\le\|Hz-h\|/\sigma^+_{\min}(H)$.
• Lemma 3, p. 12: the unconstrained bilinear problem $L(x,y)=c^\top x-y^\top Ax+b^\top y$ on $\mathbb R^{n+m}$ is $\sigma^+_{\min}(A)$-sharp on all of $\mathbb R^{n+m}$; with the identities (14) and (15) from its proof.

Significance

Lemma 5 is the input that makes the paper's restart theorems apply to linear programming: combined with Theorems 1 and 2 (missions II and III), it yields linear convergence of restarted PDHG, extragradient and ADMM on any feasible LP, with a rate governed by the Hoffman constant of the KKT system. Lemma 4 is of independent use: it shows that the normalized duality gap, which restart schemes can monitor, controls the KKT residual that solvers report.

The results are proved in the paper. As far as the platform and Mathlib show, none of them is formalized: there is no normalized duality gap, no primal-dual sharpness and no Hoffman bound for KKT systems in Mathlib. The remaining work is to formalize the paper's proofs. Strong duality for standard-form LP, needed for the §3.3 companion, exists on the platform (Polyhedral.lp_strong_duality, LinearOptimization.lp_strong_duality) in a different form.

Difficulty

The sharpness inequality relates two quantities of different nature: $\operatorname{dist}(z,Z^\star)$ is a geometric distance to an implicitly defined polyhedron, while $\rho_r(z)$ is a supremum of a bilinear gap over a truncated ball $W_r(z)$ that is cut by the constraint $x\ge0$. The unconstrained argument of Lemma 3, which identifies $\rho_r(z)$ with $\|F(z)\|$, fails once $x\ge0$ is imposed, because the ball is no longer symmetric around $z$ and the maximizing direction may leave $Z$. Control of the duality-gap row of the KKT system also depends on the size of $z$, which is why the constant degrades with $R$ and sharpness is claimed only on bounded sets $W_R(0)$. In Lean the normalized duality gap is an extended-real supremum over a set defined by a non-default norm, so each lower bound requires exhibiting a feasible point of $W_r(z)$ and computing its gap.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), and a primal-dual point is a pair. The norm on pairs is the $L^2$ norm of WithLp 2, eucl. The norm instance of the bare product type is the sup norm and is not used: with the sup norm the constants $\sqrt{1+R^2}$ and $\sqrt{1+4R^2}$ would describe different statements. $\rho_r$ and $\operatorname{diam}$ are suprema in EReal. $\operatorname{dist}(z,Z^\star)$ is a real infimum, and every statement that uses it assumes $Z^\star\neq\emptyset$ ("(19) has a solution"). $Z^\star$ is defined as the set of saddle points of $L$ on $Z$. $K$ and $h$ are encoded row block by row block exactly as (20) prints them; the page's "$A^\top y\ge c$" in (18) is a misprint for $A^\top y\le c$, which is what (20) encodes.

The Hoffman constant enters only through its defining property (26), quantified over all $z\in\mathbb R^{n+m}$, together with $H(K)>0$. Lemma 5 is stated for every such constant. Sharpness follows Definition 1 literally, with $r\in(0,\operatorname{diam}(W_R(0))]$; replacing that range by $(0,2R]$ would be a different statement. A formalization that restricts (26) to $z\in Z$, uses the sup norm, or takes a real-valued supremum for $\rho_r$ would trivialize or change the goal and is ruled out. $\sigma^+_{\min}(H)$ is the least $\sigma>0$ with $\sigma^2$ an eigenvalue of $H^\top H$; its Lean value for $H=0$ is $0$.

Contributions welcome: proofs of (22) and (25), whose combination gives Lemma 4 and then Lemma 5; general lemmas on suprema over Euclidean balls in WithLp 2 products; and a Hoffman-type existence theorem for $\{Kz\ge h\}$, which this mission does not pose. The bilinear statements (Lemmas 2–3) need a minimum-nonzero-singular-value API and are reusable beyond this mission.

Selected references

• D. Applegate, O. Hinder, H. Lu, M. Lubin, Faster First-Order Primal-Dual Methods for Linear Programming using Restarts and Sharpness, Math. Program. (2022); cited from arXiv:2105.12715v4. https://arxiv.org/abs/2105.12715 · https://doi.org/10.1007/s10107-022-01901-9
• A. J. Hoffman, On approximate solutions of systems of linear inequalities, J. Res. Natl. Bur. Stand. 49 (1952) 263–265. https://doi.org/10.6028/jres.049.027
• D. Applegate, M. Díaz, O. Hinder, H. Lu, M. Lubin, B. O'Donoghue, W. Schudy, Practical Large-Scale Linear Programming using Primal-Dual Hybrid Gradient, NeurIPS 2021. https://arxiv.org/abs/2106.04756
• A. Chambolle, T. Pock, A first-order primal-dual algorithm for convex problems with applications to imaging, J. Math. Imaging Vis. 40 (2011) 120–145. https://doi.org/10.1007/s10851-010-0251-1

Why reduce scenarios with the cost in view

A two-stage stochastic programme chooses a decision $z$ before an uncertain parameter $\xi$ is revealed and pays a cost $c(z;\xi)$. When $\xi$ is known only through $n$ data points, or through a law with many atoms, the expected cost is expensive to optimize, and practitioners replace the law by a small set of $m$ reduced scenarios. Classical scenario reduction chooses these scenarios to be close to the data in a Wasserstein distance, without looking at the cost (Dupačová, Gröwe-Kuska and Römisch, 2003; Rujeerapaiboon, Schindler, Kuhn and Wiesemann, 2022). Bertsimas and Mundru (Operations Research, 2023) propose problem-dependent scenario reduction: the distance between two scenarios measures how much the optimal decision for one costs when evaluated on the other. Their method needs, for each cluster of data, the scenario that minimizes a cost-dependent dissimilarity, which they replace by a convex upper bound, problem (16).

Theorem 3 of the paper is the sanity check for that upper bound. For the simplest cost to which it applies and a single reduced scenario ($m=1$), under a symmetry assumption on the law, the minimizer of the upper bound is the mean of $\xi$, which is also what Wasserstein scenario reduction returns for $m=1$. This mission formalizes that statement.

Setting

Decisions and parameters both live in $\mathbb R^d$, with the Euclidean inner product $z'\xi$. The feasible set is a polytope

$$\mathcal Z = \{ z\in\mathbb R^d_+ : Pz\le q\},$$

for a matrix $P\in\mathbb R^{r\times d}$ and a vector $q\in\mathbb R^r$, assumed nonempty and bounded. The cost is $c(z;\xi)=\max\{z'\xi,0\}$, a special case of the piecewise bilinear costs $\max_{1\le t\le k} z'A_t\xi$ of (15) (take $k=2$, $A_1=I$, $A_2=0$).

An optimal-decision map is any function $z^*:\mathbb R^d\to\mathbb R^d$ with $z^*(\xi)\in\arg\min_{z\in\mathcal Z} z'\xi$ for every $\xi$; for a vector $v$, $\mathcal Z^*(v)=\arg\min_{z\in\mathcal Z} z'v$ is the whole set of minimizers. The set of cost-reducing parameters is

$$\mathcal U=\Big\{\xi : \min_{z\in\mathcal Z} z'\xi<0\Big\}.$$

For a candidate reduced scenario $\zeta\in\mathbb R^d$, the per-scenario upper-bound loss is

$$L(\xi,\zeta)=\max\Big\{\max_{z\in\mathcal Z} z'(\xi-2\zeta),\,0\Big\}+2\max\{z^*(\xi)'\zeta,\,0\}.$$

For this cost it is the optimal value, in the auxiliary variables $(\lambda,\theta,\gamma)$, of the per-point linear programme in (16). With a random parameter $\xi$ of law $\mu$, the upper-bound objective for $m=1$ is $\mathbb E[L(\xi,\zeta)]$. The squared cost for Wasserstein reduction to one atom is $W(\zeta)=\int\|\xi-\zeta\|_2^2\,d\mu$; (4) takes its square root, which preserves minimizers.

Assumption 5 (p. 24) asks:

• (a) $\xi$ has a continuous distribution on $\mathcal U$ and density $0$ elsewhere;
• (b) the mean $\bar\xi=\mathbb E[\xi]$ is finite and $z^*(\bar\xi)'\bar\xi>0$;
• (c) the law of $\xi$ is symmetric about $\bar\xi$, that is, $\xi$ and $2\bar\xi-\xi$ are equal in distribution.

Formalization targets

Goal: Theorem 3 (p. 24)

Under Assumption 5, for every measurable optimal-decision map $z^*$,

$$\mathbb E\big[L(\xi,\bar\xi)\big]\;\le\;\mathbb E\big[L(\xi,\zeta)\big]\quad\text{and}\quad W(\bar\xi)\le W(\zeta)\qquad\text{for all }\zeta\in\mathbb R^d.$$

The page's "the solution … is simply the mean" is read as "the mean is a minimizer", which is what the proof concludes; uniqueness is not claimed.

Milestones (steps of the proof, pp. 24–25)

1. For each $\xi$, $\zeta\mapsto L(\xi,\zeta)$ is convex.
2. $L(\xi,\zeta)\le\big|\max_{z\in\mathcal Z} z'(\xi-2\zeta)\big|+2|\zeta'z^*(\xi)|\le(\|\xi-2\zeta\|_1+2\|\zeta\|_1)\max_{z\in\mathcal Z}\|z\|_\infty\le(\|\xi\|_1+4\|\zeta\|_1)\max_{z\in\mathcal Z}\|z\|_\infty$.
3. With probability one, $2\bar\xi-\xi\in\mathcal U$ and $\mathcal Z^*(2\bar\xi-\xi)$ is a singleton.
4. Under symmetry, $\mathbb E[z^*(2\bar\xi-\xi)]=\mathbb E[z^*(\xi)]$.
5. If $z^*(\bar\xi)'\bar\xi>0$ then $z'\bar\xi\ge z^*(\bar\xi)'\bar\xi>0$ for every $z\in\mathcal Z$.

Significance

The upper bound (16) is the computational core of the paper's Algorithm 1: each alternating-minimization step solves one instance of it per cluster. Theorem 3 is the only result in the paper that identifies its minimizer in closed form, and it shows that, in a symmetric case, the cost-aware reduction agrees with the classical one at $m=1$. It is the paper's justification that the upper bound is a sensible surrogate and not an arbitrary convex relaxation.

The argument is a variant of the mean-minimizes-the-surrogate result of Elmachtoub and Grigas for the SPO+ loss (Management Science, 2022, Proposition 6(a)), with both terms clipped at zero and with a law living only on $\mathcal U$ instead of all of $\mathbb R^d$. Theorem 3 is proved on paper; it has not been formalized, and on Prove2Me the Elmachtoub–Grigas statement is posed but open. The work here is to formalize the known proof, including the measure-theoretic steps the paper treats in one sentence each: integrability of the loss, exchange of the subdifferential and the expectation, and the almost-sure uniqueness of linear minimizers over a polytope.

Difficulty

Convexity of the objective and a vanishing subgradient at $\bar\xi$ would settle the theorem, but two steps of that argument are not routine. First, the objective is not differentiable everywhere, and the subdifferential of $\zeta\mapsto\mathbb E[L(\xi,\zeta)]$ is not in general the expectation of the pointwise subdifferentials: the exchange needs the integrable bound of milestone 2 and the almost-sure uniqueness of milestone 3. Second, that uniqueness is a statement about the geometry of polytopes and about the law of the reflected parameter $2\bar\xi-\xi$ together: neither convexity nor absolute continuity alone gives it. The clipping at zero adds a third point: one has to check that it is inactive at $\zeta=\bar\xi$ almost surely, which is where Assumption 5a's support condition on $\mathcal U$ and Assumption 5b enter. Dropping either half of Assumption 5a breaks the argument: a two-atom symmetric law can put both atoms where $\mathcal Z^*(2\bar\xi-\xi)$ is a whole edge, and a law charging the complement of $\mathcal U$ can make the first clipping active at $\bar\xi$.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d) and $z'\xi$ is ⟪z, ξ⟫_ℝ. Decision and parameter spaces coincide ($n_z=d$), as the cost $z'\xi$ requires.
• $\mathcal Z$ is polytope P qv, with the hypotheses that it is nonempty and bounded (§1 of the paper assumes $\mathcal Z$ nonempty and compact; the polytope is closed).
• The maximum and minimum of $z'v$ over $\mathcal Z$ and the argmin set are the published definitions SmartPTO.Fisher.xi, SmartPTO.Fisher.zstar and SmartPTO.Fisher.Wstar; "symmetric about its mean" is the published SmartPTO.Fisher.CentrallySymmetric.
• $z^*$ is a function zsel with the hypothesis that zsel ξ is a minimizer for every $\xi$, and it is assumed measurable (needed for $\mathbb E[z^*(\xi)]$; not on the page). The theorem holds for every such selection; uniqueness of minimizers is not assumed.
• The law is a probability measure $\mu$. Assumption 5a is two hypotheses: $\mu\ll$ Lebesgue and $\mu(\mathbb R^d\setminus\mathcal U)=0$. Full support is not assumed and would contradict the second. Assumption 5b is integrability of $\xi$ plus $z^*(\bar\xi)'\bar\xi>0$ with $\bar\xi=\int\xi\,d\mu$.
• The goal is stated on $\mathbb E[L(\xi,\zeta)]$, the first display of the proof, not on the linear programme (16) with its auxiliary variables; for this cost the two coincide by LP duality (Proposition 3's proof), and Theorem 3 is the population, $m=1$ version.
• Expectations are Bochner integrals, which return $0$ for non-integrable integrands. Under the stated hypotheses $\xi\mapsto L(\xi,\zeta)$ is dominated by $(\|\xi\|_1+4\|\zeta\|_1)\max_{z\in\mathcal Z}\|z\|_\infty$ and is integrable, so the goal is not satisfied by junk values; integrability and measurability hypotheses must not be weakened.
• The Wasserstein clause uses an extended nonnegative integral for $W$. This expresses the theorem without adding a second-moment hypothesis absent from Assumption 5. With a finite second moment it is the usual squared Wasserstein objective; with an infinite second moment every one-atom value is infinite, so the clause has only the extended-value meaning.

Useful infrastructure, reusable beyond this mission: support functions of polytopes and their directional derivatives; the fact that a linear function has a unique minimizer over a polytope for Lebesgue-almost every cost vector; differentiation of convex integral functionals under the integral sign. Contributions of any of these as stand-alone lemmas are welcome.

The source is the authors' accepted manuscript (MIT DSpace, "Submitted to Operations Research"), not the published article; all page and theorem numbers refer to the manuscript, whose printed page numbers equal its PDF page numbers.

Selected references

• D. Bertsimas and N. Mundru, Optimization-based Scenario Reduction for Data-Driven Two-stage Stochastic Optimization, Operations Research, 2023 (author manuscript, MIT DSpace). https://doi.org/10.1287/opre.2022.2265
• A. N. Elmachtoub and P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
• J. Dupačová, N. Gröwe-Kuska and W. Römisch, Scenario reduction in stochastic programming: an approach using probability metrics, Mathematical Programming 95, 2003. https://doi.org/10.1007/s10107-002-0331-0
• N. Rujeerapaiboon, K. Schindler, D. Kuhn and W. Wiesemann, Scenario Reduction Revisited: Fundamental Limits and Guarantees, Mathematical Programming 191, 2022. https://doi.org/10.1007/s10107-018-1269-1

Motivation

Maximizing a homogeneous polynomial $p$ over the unit sphere, $p_{\max}=\max_{x\in S^{d-1}}p(x)$, covers the largest stable set of a graph (degree three), the $2\to4$ norm of a matrix (degree four) and the best separable state problem of quantum information. For quadratic $p$ it is an eigenvalue problem; for degree at least three it is NP-hard. The sum-of-squares hierarchy of Parrilo and Lasserre replaces "$\gamma-p\ge0$ on the sphere" by "$\gamma-p$ is a sum of squares of polynomials of degree at most $\ell$ on the sphere", giving upper bounds $p_\ell\ge p_{\max}$ that are computable by a semidefinite program of size $d^{O(\ell)}$ and decrease to $p_{\max}$. How fast they converge decides how large $\ell$ has to be for a given accuracy. Fang–Fawzi, §1–1.1

Timeline:

• 1995. Reznick shows, for $p_{\min}=0$, that $p_\ell/p_{\max}\to1$ at rate $d/\ell$ for $\ell$ large enough. Rez95
• 2012. Doherty and Wehner study the same hierarchy on the hypersphere and obtain the same rate. DW12
• 2019. De Klerk and Laurent prove a rate $O(1/\ell^2)$ for a hierarchy of lower bounds on $p_{\max}$, and ask whether the upper bounds $p_\ell$ converge at the same rate. dKL19
• 2019. Fang and Fawzi answer this: for $\ell\ge C_nd$ the error is $O((d/\ell)^2)$, and the statement holds for symmetric matrix-valued polynomials with constants that do not depend on the matrix size. Fang–Fawzi, Theorems 1–2

Setting

Write $x=(x_1,\dots,x_d)$, $\|x\|^2=\sum_ix_i^2$, and $S^{d-1}=\{x\in\mathbb R^d:\|x\|^2=1\}$. A $k\times k$ matrix polynomial $F$ has a real polynomial in each entry, and $F(x)$ is the real matrix of values. $A\succeq0$ means that the symmetric matrix $A$ is positive semidefinite. A matrix polynomial $G$ is $\ell$-sos on $S^{d-1}$ if there are finitely many $k\times k$ matrix polynomials $U_j$, each entry of total degree at most $\ell$, with

$$G(x)=\sum_jU_j(x)U_j(x)^{\mathsf T}\qquad\text{for all }x\in S^{d-1}.$$

For a scalar polynomial $p$, $p_\ell$ is the least $\gamma$ such that $\gamma-p$ (a $1\times1$ matrix) is $\ell$-sos on $S^{d-1}$, and $p_{\min}$ is the minimum of $p$ on $S^{d-1}$. The level value is $+\infty$ when no such $\gamma$ exists.

The milestones use three further objects. A harmonic decomposition of a homogeneous $f$ of degree $2n$ is $f=\sum_{k=0}^n\|x\|^{2(n-k)}f_{2k}$ with $f_{2k}$ homogeneous of degree $2k$ and $\Delta f_{2k}=0$. $B_{2n}$ is the least constant with $\max_{S^{d-1}}|f_{2k}|\le B_{2n}\max_{S^{d-1}}|f|$ for all such $f$ in all dimensions. The Gegenbauer coefficients $\lambda_i(\phi)$ of a univariate polynomial $\phi$ are its coefficients against the orthogonal polynomials $C_i$ for the weight $(1-t^2)^{(d-3)/2}$ on $[-1,1]$, equation (9). For $q$ of degree at most $\ell$, the kernel error is

$$\rho_{2n}(d,\ell)=\min_{\deg q\le\ell,\ \lambda_0(q^2)=1}\ \sum_{k=1}^n\big|\lambda_{2k}(q^2)^{-1}-1\big|.$$

Formalization targets

Goal: Theorem 2 (p. 3)

For every $n$ there are constants $C_n,C'_n$ depending only on $n$ such that, for all $d,k,\ell$ and every $k\times k$ matrix polynomial $F$, homogeneous of degree $2n$ with $n\le d$, symmetric at every $x$, with $0\preceq F(x)\preceq I$ on $S^{d-1}$:

$$\ell\ge C_nd\ \Longrightarrow\ F+C'_n\Big(\frac d\ell\Big)^2I\ \text{is }\ell\text{-sos on }S^{d-1}.$$

The goal fixes only the shape $(d/\ell)^2$ and the regime $\ell\ge C_nd$, and leaves the constants open.

Milestones

They follow the paper's proof, in attack order:

1. Harmonic projection: Lemma 16 (Reznick's bound on $\Delta^kf$), Proposition 5 ($B_{2n}$ is independent of $d$, with $B_2\le2$, $B_4\le9$), the explicit value (34), and Proposition 17 (matrices, spectral norm).
2. Kernels: the Funk–Hecke formula (8), Remark 1, and the first part of Theorem 6: $F+\frac{B_{2n}}2\sum_k|\lambda_{2k}^{-1}-1|\,I$ is $\ell$-sos for every admissible $q$.
3. The kernel error: $C_i'(1)/C_i(1)=i(i+d-2)/(d-1)$, Proposition 18 (tangent line at $1$), Proposition 8 (spectra of Toeplitz matrices of linear functions), the value of $h'(1)$ and the eigenvalue comparison from the proof of Proposition 7, Proposition 9 ($\rho\le\tilde\rho/(1-\tilde\rho)$), and the second part of Theorem 6:

$$\rho_{2n}(d,\ell)\le C_n\Big(\frac d\ell\Big)^2\qquad(\ell\ge C'_nd).$$

4. Corollary: Theorem 1, $1\le\frac{p_\ell-p_{\min}}{p_{\max}-p_{\min}}\le1+(C_nd/\ell)^2$ for $\ell\ge C_nd$.

Significance

Theorem 2 says how the level must grow with the dimension: $\ell=\Theta(d/\sqrt\varepsilon)$ suffices for relative error $\varepsilon$, where Reznick's analysis needs $\ell=\Theta(d/\varepsilon)$. Theorem 10 of the paper shows that, for $n=1$, the kernel error of this technique really is of order $(d/\ell)^2$. Independence of the matrix size gives certificates for polynomials that are bihomogeneous of degree $(2n,2)$ on $S^{k-1}\times S^{d-1}$. The paper's Theorem 15 uses this, together with the DPS duality of the companion mission, to bound the convergence of the DPS hierarchy for separability. Fang–Fawzi, pp. 3, 10, 14

The theorem is proved in the 2019 preprint and was published in Mathematical Programming in 2021. No machine-checked proof of it or of its ingredients is known. Proving it formally takes reusable infrastructure: degree-bounded matrix SOS on the sphere, harmonic decomposition of homogeneous polynomials, Gegenbauer polynomials with their coefficients and the Funk–Hecke formula, and spectra of Jacobi matrices of orthogonal polynomials. The milestones also correct the printed text, as listed under Formalization scope.

Difficulty

Positive semidefiniteness of $F+\delta I$ at each point of the sphere does not give a factorization with factors of prescribed degree, and Reznick's kernel $\langle x,y\rangle^{2\ell}$ only reaches error $d/\ell$. Two estimates must be uniform at once. First, harmonic projection of a degree-$2n$ form must be bounded in sup norm independently of $d$; the $L^2$ bound is easy, and the sup-norm bound is the content of Proposition 5. Second, the kernel error $\rho_{2n}(d,\ell)$ must be bounded throughout the regime $\ell\ge C_nd$, which comes down to the location of the largest zero of a Gegenbauer polynomial. The printed bounds on that zero and on $\lambda_{\max}$ in Proposition 7 are false in small dimensions, so the paper's explicit constants cannot be relied on.

Formalization scope

• Objects. $\mathbb R^d$ is Fin d → ℝ (0-based coordinates), and $S^{d-1}$ is the equation $\sum_ix_i^2=1$, not the sup-norm sphere. Matrix polynomials are matrices over MvPolynomial (Fin d) ℝ, evaluated entrywise, and homogeneity is entrywise.
• $\ell$-sos. A finite family of $k\times k$ factors, every entry of total degree at most $\ell$, with equality on the sphere only. Without the degree bound the level disappears; with equality on all of $\mathbb R^d$ Theorem 2 becomes false. Neither change is a faithful reading.
• Constants. In the goal the constants are chosen before $d$, $k$, $\ell$ and $F$. No assumption $d\ge2$ is added: the cases $d=0,1$ are true and elementary.
• Standing assumption $d\ge2$. Every milestone that uses the Gegenbauer objects assumes it, as §2–3 do: the weight $(1-t^2)^{(d-3)/2}$, $\omega_{d-1}/\omega_d$ and the divisions by $d-1$ need it. Gegenbauer polynomials are normalized by $C_i(1)$ and defined by their three-term recurrence. $\sigma$ is the normalized surface measure built from Mathlib's Measure.toSphere.
• $B_{2n}$. It is not defined (it would be a real infimum). Statements quantify over every constant $B$ with the defining property, and $B_{2n}$ is one of them.
• $\rho_{2n}$. It takes values in $[0,\infty]$, with $|\lambda^{-1}-1|=\infty$ at $\lambda=0$ and $\infty$ on an empty feasible set. Its sum runs over $k=1,\dots,n$, following (12), (13) and (16); (10) prints $2n$, a slip. Its minimum is over $\deg q\le\ell$, as in (13). The first part of Theorem 6 is posed per polynomial $q$, which is what (12) proves and implies the printed form.
• Other conventions. Proposition 17's spectral norm is written as $\max_{\|y\|=1}|y^{\mathsf T}Ay|$, and homogeneity of $F$ is explicit there. Theorem 1 is stated cross-multiplied, so that it is meaningful when $p$ is constant on the sphere. Its level value is extended real to record infeasibility; the theorem asserts a finite attained value and a degree-bounded SOS certificate.
• Not posed. Proposition 7 ($\lambda_{\max}(\mathcal T[h])\ge1-\frac{7n}{12}\frac{d^2}{\ell^2}$) fails, for example, at $d=2$, $n=1$, $\ell=10$. The zero bound it quotes and the explicit constants at the end of p. 9 are not posed either; the true first inequality of its proof is.

Proofs of any milestone are welcome. So are reusable developments of Gegenbauer polynomials, spherical harmonics, the Funk–Hecke formula, Jacobi matrices, and Carathéodory-type finite quadratures that turn an integral of squares into a finite sum of squares.

Selected references

• K. Fang, H. Fawzi, The sum-of-squares hierarchy on the sphere, and applications in quantum information theory, arXiv preprint, 2019. https://arxiv.org/abs/1908.05155v1
• B. Reznick, Uniform denominators in Hilbert's seventeenth problem, Mathematische Zeitschrift 220(1), 75–97, 1995. https://doi.org/10.1007/BF02572604
• A. C. Doherty, S. Wehner, Convergence of SDP hierarchies for polynomial optimization on the hypersphere, arXiv preprint, 2012. https://arxiv.org/abs/1210.5048
• E. de Klerk, M. Laurent, Convergence analysis of a Lasserre hierarchy of upper bounds for polynomial minimization on the sphere, arXiv preprint, 2019. https://arxiv.org/abs/1904.08828
• J. B. Lasserre, Global optimization with polynomials and the problem of moments, SIAM Journal on Optimization 11(3), 796–817, 2001. https://doi.org/10.1137/S1052623400366802