All missions

Motivation

The augmented Lagrangian method (method of multipliers) of Hestenes, Powell and Rockafellar solves a constrained nonlinear program by repeatedly minimizing an unconstrained merit function in the primal variables and then updating the multipliers. For inequality constraints, the augmented Lagrangian in the form the paper takes from Rockafellar (Rockafellar 1981) is continuously differentiable but not twice differentiable, even when all problem data are smooth: its Hessian jumps across the surfaces where a constraint switches between the "active" and "inactive" formula. Newton's method for the inner minimization therefore has no classical Hessian to work with on those surfaces.

Qi and Sun (Math. Programming 58, 1993) extended Newton's method to equations $F(x) = 0$ with $F$ locally Lipschitz, replacing the Jacobian by an element of Clarke's generalized Jacobian, and proved local superlinear convergence when $F$ is semismooth. Section 4 of the paper, an example suggested by Rockafellar, shows that the gradient of the augmented Lagrangian of a $C^2$ program is semismooth, so the nonsmooth Newton method applies to the stationarity equation $\nabla L_r = 0$. This mission formalizes that result, Theorem 4.1.

Setting

Let $f_0, f_1, \dots, f_m : \mathbb{R}^n \to \mathbb{R}$ be of class $C^2$ and consider

$$\text{(NLP)}\quad \min f_0(x)\ \text{ s.t. }\ f_i(x) = 0,\ i = 1,\dots,p,\qquad f_i(x) \le 0,\ i = p+1,\dots,m. \tag{4.1}$$

Fix $r > 0$. For a constraint value $a$ and a multiplier $y$ put

$$\phi(r, a, y) = \begin{cases} y a + \tfrac12 r a^2, & y + r a \ge 0,\\ -\tfrac{1}{2r} y^2, & y + r a \le 0,\end{cases}$$

(the two cases agree when $y + ra = 0$). The augmented Lagrangian is the function of $(x, y) \in \mathbb{R}^n \times \mathbb{R}^m$

$$L_r(x, y) = f_0(x) + \sum_{i=1}^{p}\Big(y_i f_i(x) + \tfrac12 r f_i(x)^2\Big) + \sum_{i=p+1}^{m} \phi\big(r, f_i(x), y_i\big).$$

For a locally Lipschitz map $F$ between finite-dimensional spaces, let $D_F$ be the set where $F$ is differentiable. Clarke's generalized Jacobian is $\partial F(x) = \mathrm{co}\{\lim JF(x_i) : x_i \to x,\ x_i \in D_F\}$. $F$ is semismooth at $x$ if it is locally Lipschitz near $x$ and, for every direction $h$, the limit of $V h'$ over $V \in \partial F(x + t h')$, $h' \to h$, $t \downarrow 0$, exists.

For a single constraint function $g$ the proof works with $\eta(x, s) = \phi(r, g(x), s)$ on $\mathbb{R}^n \times \mathbb{R}$, and with the surface $s + r g(x) = 0$ on which the two formulas for $\phi$ meet.

Formalization targets

Goal: Theorem 4.1

For $r > 0$ and $f_0, \dots, f_m \in C^2$:

$$L_r \in C^1, \qquad \nabla L_r \text{ semismooth at } (x,y) \text{ whenever } \exists\, i > p:\ y_i + r f_i(x) = 0,$$ $$\nabla L_r \in C^1 \text{ near } (x, y) \text{ whenever } y_i + r f_i(x) \neq 0 \text{ for all } i > p.$$

All three clauses are the theorem; the last two together cover every point.

Milestones

1. $\eta \in C^1$, with $\nabla\eta(x,s) = \big((s + r g(x))\nabla g(x),\ g(x)\big)$ if $s + r g(x) \ge 0$ and $(0, -s/r)$ if $s + r g(x) \le 0$, and $\nabla \eta$ is locally Lipschitz.
2. Eq. (4.2): the Hessian of $\eta$ on each side of the surface, and $\nabla\eta \in C^1$ near every point off it.
3. Eq. (4.7): if $\bar s + r g(\bar x) = 0$ and $\bar s + t_j\alpha_j + r g(\bar x + t_j h_j) = 0$ with $h_j \to h$, $\alpha_j \to \alpha$, $t_j \downarrow 0$, then $\alpha + r\nabla g(\bar x)^{\mathsf T} h = 0$.
4. $\nabla\eta$ is semismooth, jointly in $(x, s)$, at every point of the surface.

Significance

The result places the inner problem of the augmented Lagrangian method inside the scope of the paper's convergence theory: with $F = \nabla L_r$, the generalized-Jacobian Newton iteration converges locally superlinearly at a root where every element of $\partial F$ is nonsingular. Its practical content is that second-order methods can be run on $L_r$ even though $L_r$ is only $C^{1}$, with the elements of $\partial \nabla L_r$ playing the role of Hessians. The same pattern (a $C^1$ merit function with semismooth gradient) recurs in extended linear-quadratic programming and in semismooth Newton methods for complementarity problems.

The theorem is proved in the paper by direct computation. As far as a search of the platform showed, none of the objects involved (Clarke's generalized Jacobian, semismoothness, Rockafellar's augmented Lagrangian) has a published formalization there, and Mathlib has none of them. The mission produces a machine-checked version of the computation and, as a by-product, reusable statements about $C^1$ functions obtained by gluing two $C^2$ pieces along a hypersurface.

Difficulty

Clauses 1 and 3 are calculus with a case split: one has to check that the two formulas for $\phi$ and for its gradient match on the surface. Clause 2 is where the argument is not routine. On the surface, $\nabla\eta$ is not differentiable, and the generalized Jacobian $\partial\nabla\eta$ there contains convex combinations of the two one-sided Hessians of (4.2). Semismoothness asks that $V(h', \alpha')$ have a single limit over all such $V$, for all approaches $(h', \alpha') \to (h, \alpha)$, $t \downarrow 0$, including approaches that cross the surface infinitely often. The two one-sided Hessians are different matrices, so no single derivative describes $\nabla\eta$ near the surface, and the existence of the limit must be shown for approaches that alternate between the two sides and for the convex combinations that $\partial\nabla\eta$ contains on the surface itself. General theorems that piecewise-smooth maps are semismooth appear in later literature but are not available in Mathlib, so they cannot be invoked as a shortcut. A second obstacle is infrastructure: Mathlib has no generalized Jacobian, so every fact about $\partial\nabla\eta$ (which limits of derivatives occur near the surface) must be derived from the definition.

Formalization scope

• $\mathbb{R}^n$ and $\mathbb{R}^m$ are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m); $L_r$ is a function on their product, and $\eta$ on EuclideanSpace ℝ (Fin n) × ℝ.
• The constraint index $i \in \{1,\dots,m\}$ is i : Fin m with paper index i.val + 1; equality constraints are i.val < p, inequality constraints p ≤ i.val. The paper's implicit $p \le m$ is not assumed (for $p > m$ there are no inequality constraints).
• The paper's first sum prints $h(r_i, f_i(x), y_i)$; the single $r$ is used, as in the paper's definition of $h$.
• $\phi$ uses the first branch when $y + ra \ge 0$; the branches agree on the boundary. Every statement assumes $r > 0$.
• $C^2$ is ContDiff ℝ 2 on all of $\mathbb{R}^n$; "smooth" is the paper's continuously differentiable, ContDiffAt ℝ 1 of the gradient at the point.
• $\nabla L_r$ and $\nabla\eta$ are Fréchet derivatives, valued in continuous linear functionals; semismoothness is invariant under the Riesz isometry to gradient vectors and under equivalent norms on the domain (Mathlib's product has the sup norm).
• The Jacobian in Clarke's definition is fderiv, limits are along sequences, and no closure is taken in the convex hull. Semismoothness is the explicit $\varepsilon$–$\delta$ form of the paper's limit, uniform over $V \in \partial F(x + th')$.
• Hessians in (4.2) are stated as the Fréchet derivative of the gradient map applied to a direction.

A formalization that states only $L_r \in C^1$, or only the semismoothness of one term $\eta$, is not Theorem 4.1; the goal contains all three clauses for the full $L_r$. The combination step from the terms $\eta$ to $L_r$ uses that sums of semismooth maps and $C^1$ maps with locally Lipschitz derivative are semismooth; the paper cites this without proof, and a solver will need to prove it.

Contributions welcome: the lemmas above; general facts about clarkeJac (it contains fderiv at points of strict differentiability; it is a singleton for $C^1$ maps; behaviour under sums and linear maps); and the semismoothness of sums.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• R. T. Rockafellar, Proximal subgradients, marginal values, and augmented Lagrangians in nonconvex optimization, Mathematics of Operations Research 6 (1981) 427–437. https://doi.org/10.1287/moor.6.3.427
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (reprinted SIAM Classics in Applied Mathematics 5, 1990). https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM J. Control Optim. 15 (1977) 959–972. https://doi.org/10.1137/0315061

Motivation

A decision maker who chooses a portfolio $x\in\mathbb R^n$ of risky assets with random return vector $R$ receives the scalar return $x'R$ and evaluates it by an expected utility $E[u(x'R)]$. In practice the law of $R$ is not known; what can be estimated with some confidence are its mean $\mu$ and covariance $\Sigma$. The robust mean-covariance objective replaces the unknown law by the worst law consistent with these two moments:

$$U(x)=\inf\{E[u(x'R)] : R \text{ has mean } \mu \text{ and covariance } \Sigma\}.$$

Ioana Popescu (Operations Research 55(1), 2007) showed that $U(x)$ depends on $x$ only through $\mu_x=x'\mu$ and $\sigma_x^2=x'\Sigma x$, and that for large classes of utilities it has a closed form or reduces to a one-dimensional search. This turns a robust stochastic program into a parametric mean-variance program, which is the practical point of the paper. This mission formalizes the closed form for concave utilities with a monotone second derivative (Proposition 7), a class that contains the exponential utility $1-e^{-ay}$ and all concave quadratics. The reduction to $(\mu_x,\sigma_x)$ is the subject of the companion mission Robust Mean-Covariance Solutions for Stochastic Optimization I; the two-point case is mission II.

The underlying univariate question is a moment problem in the tradition of Chebyshev-type bounds: the extremal value of $E[u(r)]$ over all laws with prescribed mean and variance. Scarf (1958) solved an instance for a piecewise-linear inventory cost, and Birge and Dulá (1991) treated two-point extremal laws on bounded domains.

Setting

Fix $m\in\mathbb R$ and $s\ge 0$. The mean-variance class $\mathbb M_{(m,s^2)}$ is the set of Borel probability measures $\nu$ on $\mathbb R$ with $\int r^2\,d\nu<\infty$, $\int r\,d\nu=m$ and $\int (r-m)^2\,d\nu=s^2$ (Lean: MeanVarClass m (s ^ 2)). For a utility $u:\mathbb R\to\mathbb R$ the robust objective is

$$U(m,s)=\inf\Big\{\int u\,d\nu : \nu\in\mathbb M_{(m,s^2)}\Big\},$$

with $\min$ read, as in the paper, "in the wide sense of $\inf$", so the value $-\infty$ is allowed. The paper's $U(x)$ is $U(\mu_x,\sigma_x)$.

For $p\in(0,1)$ the two-point law $r_p$ puts mass $p$ on $b=m+\sqrt{(1-p)/p}\,s$ and mass $1-p$ on $a=m-\sqrt{p/(1-p)}\,s$; these are exactly the two-point laws of $\mathbb M_{(m,s^2)}$. Its expected utility is the two-point objective (8),

$$U(p)=p\,u(b)+(1-p)\,u(a)\qquad(\texttt{twoPointValue u m s p}).$$

A supporting quadratic of $u$ is $q(y)=Ay^2+By+C$ with $q\le u$ on $\mathbb R$; the set of their coefficients is $\mathcal Q$. Since every $r\sim(m,s^2)$ has $E[q(r)]=A(m^2+s^2)+Bm+C$, each element of $\mathcal Q$ gives a lower bound on $U(m,s)$ (Proposition 3). The function $u$ has the one-point support property with respect to $(m,s^2)$ (Definition 3, OnePointSupportWrt u m s) if some supporting quadratic touches $u$ at $m$ and $E[u(r_p)]\to E[q(r_p)]$ as $p\to0^+$ or as $p\to1^-$; it has one-point support (OnePointSupport u) if this holds for every $m$ and every $s\ge0$.

Formalization targets

Goal: Proposition 7

Let $u$ be concave and twice differentiable with monotone $u''$.

(a) If $u'$ is convex, then

$$U(m,s)=u(m)+\lim_{y\to-\infty}u''(y)\,\frac{s^2}{2}\qquad\text{for all } m,\ s.$$

(b) If $u'$ is concave, the same holds with $\lim_{y\to+\infty}u''(y)$.

In each part the limit $L$ of $u''$ exists in $[-\infty,0]$. When $L$ is finite the goal asserts that $u$ is integrable under every law of every class, that $u(m)+Ls^2/2$ is the greatest lower bound of the expected utilities, and that $u$ has one-point support. When $L=-\infty$ and $s>0$ it asserts $U(m,s)=-\infty$.

Milestones

1. Display (9): $\partial U/\partial p=u(b)-u(a)-(b-a)\,\frac{u'(b)+u'(a)}{2}$.
2. For convex $u'$ and $s>0$, $U(p)$ is nonincreasing on $(0,1)$.
3. Appendix (4): $\lim_{p\to1^-}U(p)=u(m)+\frac{s^2}{2}\lim_{y\to-\infty}u''(y)$, including the value $-\infty$.
4. Proposition 3: every $E[u(r)]$ dominates every $A(m^2+s^2)+Bm+C$ with $(A,B,C)\in\mathcal Q$.
5. The function $d(y)=\frac{u(y)-u(m)}{(y-m)^2}-\frac{u'(m)}{y-m}$ is nondecreasing on $\{y \neq m\}$ when $u'$ is convex.
6. Appendix (5): $q(y)=\tfrac12u''(-\infty)(y-m)^2+u'(m)(y-m)+u(m)$ supports $u$, and $\inf_{y\ne m}d(y)=\lim_{y\to-\infty}d(y)=\tfrac12u''(-\infty)$.

An additional item states Proposition 8: a monotone convex $u$ has one-point support and $U(m,s)=u(m)$.

Significance

Proposition 7 turns the worst-case expected utility into a mean-variance criterion with an explicit risk weight: a prudent investor ($u'$ convex) is penalized by $\tfrac12\lim_{y\to-\infty}u''(y)$ per unit of variance, an imprudent one by the limit at $+\infty$. With Proposition 1, the robust portfolio problem becomes $\max_x\ u(\mu_x)+\tfrac12 L\,\sigma_x^2$, a concave mean-variance program. For exponential utility the weight is $-\infty$ (Example 3 of the paper), so the robust investor must eliminate variance entirely; this is a qualitative statement about robustness that follows only from the $-\infty$ case of the theorem.

The result is published with a proof in the appendix of the paper. It has, to the best of our search, no machine-checked version, and the platform currently holds no statement of Propositions 3, 7 or 8 or Definition 3. A formal proof would also check two points where the printed argument is incomplete: the proof's step "$\lim_{y\to-\infty}u'(y)=\infty$" fails for affine $u$, where the theorem nevertheless holds, and the claim that $u$ "has one-point support" fails when $\lim u''=-\infty$ (see the scope section). Related platform work on worst-case expectations over ambiguity sets is the mission Wasserstein Distributionally Robust Optimization II, which uses a different ambiguity set.

Difficulty

The infimum ranges over all laws with two prescribed moments, an infinite-dimensional set with no compactness, and in the relevant cases it is not attained. The natural first idea, restricting to two-point laws and minimizing over $p$, gives only an upper bound (display (7)), and here the minimizing $p$ runs off to the boundary: the extremal law puts vanishing mass on a point escaping to $-\infty$. Identifying the limiting value requires controlling $u(m-sq)/(1+q^2)$ as $q\to\infty$, a second-order asymptotic statement about $u$ at $-\infty$. The matching lower bound requires a supporting quadratic whose curvature is exactly $\tfrac12\lim u''$; showing that it lies below $u$ everywhere, not only near $m$, is a global statement that uses the convexity of $u'$ on the whole line. The finite-limit and infinite-limit cases also behave differently: in the second, no supporting quadratic exists at all.

Formalization scope

Laws are Measure ℝ with IsProbabilityMeasure, finite second moment is MemLp id 2, and the class is parameterized by mean $m$ and variance $s^2$ with $s\ge0$. The statements are univariate: $U(x)$ of the paper is the univariate objective at $(\mu_x,\sigma_x)$ by Proposition 1 of the paper (mission I). Derivatives are deriv u and deriv (deriv u); "twice differentiable" is differentiability of $u$ and of $u'$. Limits of $u''$ are explicit hypotheses (Tendsto … atBot (𝓝 L) or Tendsto … atBot atBot), never limUnder. Limits in $p$ are one-sided inside $(0,1)$. Expectations under two-point laws are written by the explicit formula (8).

"Min" is never a real ⨅, which Lean evaluates to $0$ on sets unbounded below. The finite case uses IsGLB together with integrability of $u$ under every law of the class; the infinite case asserts that integrable laws with arbitrarily small expected utility exist; Proposition 3 is stated as "every value $\ge$ every value". Proposition 3 assumes $u$ integrable under the law; Proposition 8 takes the infimum over laws under which $u$ is integrable, which for convex $u$ loses nothing.

One correction to the printed statement: Proposition 7 opens with "then $u$ has one-point support", which is false when $\lim u''=-\infty$, since no quadratic lies below $1-e^{-ay}$ on $\mathbb R$. The formalization asserts one-point support only in the finite-limit case and the value $-\infty$ in the other. A formalization that took $\min$ as a real infimum, dropped the integrability conjunct, or asserted one-point support unconditionally would be either trivially satisfiable or false; none of these is used.

A complete development needs: moments of two-point laws, a second-order l'Hôpital or Taylor argument at $-\infty$, the trapezoid inequality for convex functions, and Jensen-type integration of quadratic lower bounds. The mean-variance class, the two-point objective and the supporting-quadratic lemmas are reusable for mission II and for other moment-problem bounds. Proofs of any milestone, and of part (b), are welcome.

Selected references

• I. Popescu, Robust Mean-Covariance Solutions for Stochastic Optimization, Operations Research 55(1):98–112, 2007. https://doi.org/10.1287/opre.1060.0353
• H. Scarf, A min-max solution of an inventory problem, in Studies in the Mathematical Theory of Inventory and Production, Stanford University Press, 1958.
• J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30, 1991.
• S. Karlin, W. J. Studden, Tchebycheff Systems: With Applications in Analysis and Statistics, Interscience, 1966.

Motivation

For dense graphs, convergence of subgraph densities was shown by Lovász and Szegedy (2006) to have graphons as limit objects, and Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) proved that the same convergence is metric: a graph sequence converges exactly when it is Cauchy in the cut distance. The metric view is what makes the space of graphons compact and connects limit theory with regularity lemmas and property testing.

Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) developed the corresponding theory for permutations. Besides the existence of limits (the subject of mission I of this series), they introduced a rectangular distance $d_\square$ between permutations, a normalized version of Cooper's discrepancy (Cooper, J. Combin. Theory Ser. A, 2004; reference [7] of the paper), and proved in Theorem 1.8 that convergence of a permutation sequence is the same as being Cauchy for $d_\square$. This mission formalizes that theorem.

Timeline:

• 2004. Cooper introduces the discrepancy of a permutation as a measure of quasirandomness.
• 2006–2008. Lovász–Szegedy and Borgs et al. establish graph limits and the cut-distance characterization of convergence.
• 2011–2013. Hoppen et al. prove the permutation analogues, including Theorem 1.8 (this paper).

Setting

For $n \ge 1$, $S_n$ is the set of permutations of $[n]=\{1,\dots,n\}$, $|\pi| = n$ for $\pi\in S_n$, and $\mathcal S=\bigcup_n S_n$. For $\tau\in S_k$ and $\pi\in S_n$, $\Lambda(\tau,\pi)$ counts the increasing $k$-tuples $x_1<\dots<x_k$ in $[n]$ with $\pi(x_i)<\pi(x_j)\iff\tau(i)<\tau(j)$, and the subpermutation density is $t(\tau,\pi)=\Lambda(\tau,\pi)/\binom nk$ for $k\le n$ and $0$ for $k>n$. A permutation sequence $(\sigma_n)$ is convergent if $t(\tau,\sigma_n)$ converges for every fixed $\tau\in\mathcal S$.

A limit permutation is a Lebesgue measurable $Z:[0,1]^2\to[0,1]$ such that $Z(x,\cdot)$ is a cdf (non-decreasing, right-continuous, $Z(x,1)=1$) for every $x$ and $\int_0^1 Z(x,y)\,dx=y$ for every $y$; the set of them is $\mathcal Z$. Each $Z$ has an associated random point $(X,Y)$ with $X\sim U[0,1]$ and conditional cdf $Z(X,\cdot)$, joint distribution function $F(x,y)=\int_0^x Z(t,y)\,dt$, and pattern densities $t(\tau,Z)$ (the probability that $k$ independent copies of $(X,Y)$ form the pattern $\tau$).

For $\sigma\in S_n$, the step limit permutation $Z_\sigma$ spreads the permutation matrix of $\sigma$ uniformly over the corresponding $n\times n$ grid cells. The rectangular distance of $Z_1,Z_2\in\mathcal Z$ is

$$d_\square(Z_1,Z_2)=\sup_{x_1<x_2,\ y_1<y_2}\left|\int_{x_1}^{x_2}\big(Z_1(x,y_2)-Z_1(x,y_1)\big)dx-\int_{x_1}^{x_2}\big(Z_2(x,y_2)-Z_2(x,y_1)\big)dx\right|,$$

the largest difference between the probabilities the two random points give to an axis-parallel rectangle, and $d_\infty(Z_1,Z_2)=\sup_{x,y}|F_1(x,y)-F_2(x,y)|$. On permutations of possibly different lengths, $d_\square(\sigma,\pi):=d_\square(Z_\sigma,Z_\pi)$. A sequence is Cauchy with respect to $d_\square$ if for every $\varepsilon>0$ there is $n_0$ with $d_\square(\sigma_n,\sigma_m)<\varepsilon$ for all $n,m\ge n_0$.

Formalization targets

Goal: Theorem 1.8, under $|\sigma_n|\to\infty$

$$|\sigma_n|\to\infty\ \Longrightarrow\ \Big((\sigma_n)\ \text{convergent}\iff(\sigma_n)\ \text{is } d_\square\text{-Cauchy}\Big).$$

Milestones

In the order the proof uses them:

1. Lemma 3.5: $|t(\tau,\sigma)-t(\tau,Z_\sigma)|\le\frac1n\binom k2$ for $\tau\in S_k$, $\sigma\in S_n$, $k\le n$.
2. Eq. (49): for $|\sigma_n|\to\infty$, $\sigma_n\to Z\iff Z_{\sigma_n}\xrightarrow{t}Z$.
3. Eq. (34): $d_\infty\le d_\square\le 4\,d_\infty$ on $\mathcal Z$.
4. Lemma 2.1: for uniform marginals, weak convergence is equivalent to uniform convergence of joint distribution functions.
5. Lemma 2.2 (a): every law on $[0,1]^2$ with uniform marginals has a limit permutation as its conditional cdf.
6. Lemma 5.3: weak, $d_\square$- and density convergence on $\mathcal Z$ coincide.
7. Theorem 1.6 (i): a convergent sequence with $|\sigma_n|\to\infty$ converges to some $Z\in\mathcal Z$.
8. Claim 2.4: a convergent sequence with $|\sigma_n|\not\to\infty$ is eventually constant.
9. Theorem 1.8 ($\Rightarrow$): every convergent sequence is $d_\square$-Cauchy, with no condition on lengths.

Significance

Theorem 1.8 identifies density convergence, defined through infinitely many pattern counts, with a single metric condition. With Theorem 1.6 it shows that the completion of $(\mathcal S,d_\square)$ is $\mathcal Z$ modulo almost-everywhere equality, which is compact; permutations are isolated points of it (Claim 2.4). This is the permutation counterpart of the cut-distance theory of graph limits, and it is the metric in which the paper's testability and sampling results (Lemma 4.2) are quantitative.

The theorem is proved in the paper. To the best of current knowledge neither it nor the underlying permuton theory is formalized in any proof assistant. The mission produces machine-checked statements of the rectangular distance, its comparison with the sup-norm distance of distribution functions, and the Cauchy characterization, all reusable for quasirandom permutations and permutation property testing.

Difficulty

The direction "convergent $\Rightarrow$ Cauchy" needs a limit permutation for the sequence and the equivalence of density and $d_\square$ convergence on $\mathcal Z$ (Lemma 5.3), which is not formal: density convergence involves every pattern, $d_\square$ a supremum over rectangles. For "Cauchy $\Rightarrow$ convergent", completeness of bounded functions under the sup norm gives a uniform limit $F$ of the distribution functions, but a uniform limit of distribution functions of limit permutations is not visibly the distribution function of a limit permutation. Identifying it needs weak compactness, Lemma 2.1 and the regular conditional cdf of Lemma 2.2.

The literal statement also fails for sequences whose lengths do not tend to infinity, as explained under Formalization scope; the reduction "we may assume $|\sigma_n|\to\infty$" covers only one direction.

Formalization scope

• $[0,1]$ is Mathlib's unitInterval with Lebesgue measure; a limit permutation is a curried real function Z : I → I → ℝ, almost-everywhere measurable on the square, with the cdf and integral conditions for every $x$ and every $y$. $S_n$ is Equiv.Perm (Fin n) (0-based) and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n).
• $d_\square$ on $\mathcal Z$ is the integral form of the paper's Eq. (32); $d_\infty$ is Eq. (33) with $F_i(x,y)=\int_0^x Z_i(t,y)\,dt$. Both are real suprema of bounded families. $Z_\sigma$ is in closed form, with the first row used at $x=0$ (a null-set choice).
• $d_\square$ on permutations is defined for every pair of lengths as $d_\square(Z_\sigma,Z_\pi)$, the paper's extension (Sect. 4.1); the same-length formula (31) is not needed. A definition that returned $0$ or junk for different lengths would make every sequence with growing lengths Cauchy and is ruled out.
• Correction. The paper states Theorem 1.8 for all sequences. Without $|\sigma_n|\to\infty$, "Cauchy $\Rightarrow$ convergent" is false: interleaving $\sigma=(1,2)$ with permutations $\tau_k$, $|\tau_k|\to\infty$, $d_\square(Z_{\tau_k},Z_\sigma)\to0$, gives a Cauchy sequence along which $t(\sigma,\cdot)$ alternates between $1$ and values tending to $3/4$. The goal carries $|\sigma_n|\to\infty$; the true direction without it is milestone 9.
• "Convergent" is the paper's Definition 1.2 (all densities converge), not the existence of a limit $Z$. The Cauchy condition uses the explicit $\varepsilon$–$n_0$ form with strict inequality, not a metric-space instance.
• Theorem 1.6 (i) is also the goal of mission I; it is restated here in this mission's namespace.

Needed infrastructure: Prokhorov compactness of probability measures on the square, the Portmanteau theorem, completeness of bounded functions under the sup norm, and conditional cdfs (ProbabilityTheory.condCDF). Contributions on any milestone, and alternative proofs of the Cauchy characterization, are welcome.

Selected references

• C. Hoppen, Y. Kohayakawa, C. G. Moreira, B. Ráth, R. M. Sampaio, Limits of permutation sequences, arXiv:1103.5844v2, 2012; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1103.5844v2
• J. N. Cooper, Quasirandom permutations, J. Combin. Theory Ser. A 106 (2004) no. 1, 123–143 (cited as [7] in arXiv:1103.5844v2).
• L. Lovász, B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96 (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002
• C. Borgs, J. T. Chayes, L. Lovász, V. T. Sós, K. Vesztergombi, Convergent sequences of dense graphs I: Subgraph frequencies, metric properties and testing, Adv. Math. 219 (2008) 1801–1851. https://doi.org/10.1016/j.aim.2007.08.004
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962

Motivation

Many polytopes of combinatorial optimization have exponentially many facets, yet linear optimization over them is tractable because they are projections of simpler convex sets: affine slices of a nonnegative orthant (linear programming) or of the cone of positive semidefinite matrices (semidefinite programming). The size of such a representation, the number of variables of the extended formulation, is the natural measure of how compactly a polytope can be optimized over. Yannakakis (Expressing combinatorial optimization problems by linear programs, JCSS 1991) characterized polyhedral representations through nonnegative factorizations of the slack matrix. Gouveia, Parrilo and Thomas (arXiv:1111.3164, Mathematics of Operations Research 2013) extended the characterization to lifts into arbitrary closed convex cones, in particular to cones of positive semidefinite matrices.

The stable set polytope of a graph is the standard test case. For a perfect graph on $n$ vertices it is a linear image of an affine slice of the cone of $(n+1)\times(n+1)$ positive semidefinite matrices (Lovász's theta body construction, stated in the paper as Theorem 5.1 with a citation to Lovász & Schrijver, SIAM J. Optim. 1991); this is the reason the maximum weight stable set problem is solvable in polynomial time on perfect graphs. The question addressed by this mission is whether a smaller matrix size could suffice. Theorem 5.2 of Gouveia–Parrilo–Thomas answers it: for every graph on $n$ vertices, matrices of size $n$ do not suffice.

Setting

Let $G$ be a graph with vertex set $V = \{1,\dots,n\}$. A set $S \subseteq V$ is stable if no edge joins two of its elements, and its incidence vector $\chi_S \in \{0,1\}^n$ has $(\chi_S)_i = 1$ exactly when $i \in S$. The stable set polytope is

$$\mathrm{STAB}(G) = \mathrm{conv}\{\chi_S : S \text{ stable}\} \subseteq \mathbb R^n .$$

Let $\mathcal S^k_+$ be the cone of $k \times k$ real symmetric positive semidefinite matrices, with the trace inner product $\langle A, B\rangle = \mathrm{tr}(AB)$, under which it is self-dual. For a closed convex cone $K$, a set $C$ has a $K$-lift if $C = \pi(K \cap L)$ for an affine subspace $L$ and a linear map $\pi$; the lift is proper if $L$ meets the interior of $K$.

For a polytope $P$ with vertices $p_1,\dots,p_v$ and facet inequalities $h_1(x) \ge 0, \dots, h_f(x) \ge 0$, the slack matrix is the nonnegative $v\times f$ matrix $(h_j(p_i))$. A $K$-factorization of a nonnegative matrix $M$ assigns $a^i \in K$ to each row and $b^j \in K^*$ to each column with $\langle a^i, b^j\rangle = M_{ij}$. In Lean the objects are stab, HasPSDLift, HasConeLift, HasProperConeLift, IsSlackMatrix, HasConeFactorization and HasPSDFactorization in the namespace ConeLifts.StableSet.

Formalization targets

Goal: Theorem 5.2

For every $n \ge 1$ and every graph $G$ on $n$ vertices,

$$\neg\ \exists\, L,\ \pi:\quad \mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L).$$

The statement excludes all lifts, proper or not, and holds for every graph, perfect or not.

Milestones

1. Theorem 3.3 (first sentence). If a full-dimensional polytope $P$ with the origin in its interior has a proper $K$-lift, then every slack matrix of $P$ admits a $K$-factorization.
2. Rows of the submatrix. The origin and $e_1,\dots,e_n$ are vertices of $\mathrm{STAB}(G)$.
3. Columns of the submatrix. For $n \ge 1$, each $\{x \in \mathrm{STAB}(G) : x_i = 0\}$ is a facet, and some facet does not contain the origin.
4. The core lemma. For every $s \in \mathbb R^n$ the block matrix

$$S' = \begin{pmatrix} 1 & 0_n \\ s & I_n\end{pmatrix}$$

has no $\mathcal S^n_+$-factorization.

Significance

Theorem 5.2 shows that the semidefinite representation of $\mathrm{STAB}(G)$ for perfect graphs has the smallest possible matrix size: $n+1$ cannot be lowered to $n$. As Remark 5.3 of the paper notes, the same argument shows that no polytope in $\mathbb R^n$ with a vertex at which it locally looks like the nonnegative orthant has an $\mathcal S^n_+$-lift. It is also an instance of the factorization method: a statement about all possible semidefinite representations is reduced to a finite obstruction on a small submatrix of the slack matrix.

The theorem is proved in the paper. To the best of our knowledge no machine-checked proof of it, of the factorization theorem for cone lifts, or of any positive semidefinite lower bound for a polytope exists in Mathlib or on this platform. A formalization produces reusable statements about positive semidefinite factorizations, slack matrices and lifts, and a verified instance of the general lower-bound technique.

Difficulty

The step from lifts to factorizations is where the direct argument fails. Theorem 3.3 applies only to proper lifts and only to polytopes with the origin in their interior, while the goal concerns all lifts of a polytope that has the origin as a vertex. Applying Theorem 3.3 to $\mathrm{STAB}(G)$ and an arbitrary lift therefore does not match its hypotheses, and the printed proof does not spell out how the two gaps are closed (see Formalization scope). Theorem 3.3 itself is a consequence of the general factorization theorem of the paper (Theorem 2.4), whose proof rests on conic duality. The core lemma about $S'$ is a statement about every family of $2(n+1)$ positive semidefinite matrices, so it cannot be settled by any finite search.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); vertex $i+1$ of the paper is i : Fin n; graphs are SimpleGraph (Fin n) and stability is SimpleGraph.IsIndepSet. Vertices of a polytope are Set.extremePoints ℝ. $\mathcal S^k_+$ is the set of real $k\times k$ matrices satisfying Matrix.PosSemidef (which includes symmetry), and the ambient space of a positive semidefinite lift is all $k \times k$ matrices; this does not change which sets have lifts, because a lift in the symmetric matrices extends linearly and a lift in all matrices restricts to them. Positive semidefinite factorizations require both factor families to be positive semidefinite and use $\mathrm{tr}(A_iB_j)$.

Reading decisions: the goal assumes $n \ge 1$, the paper's meaning of "a graph with $n$ vertices", since for $n = 0$ the polytope $\{0\}$ is the image of $\mathcal S^0_+$ and the printed statement fails. Milestone 3 also assumes $n \ge 1$, and so does Milestone 1 (Theorem 3.3): in $\mathbb R^0$ the point $\{0\}$ has a proper lift to the whole space $\mathbb R^m$, whose dual cone $\{0\}$ cannot factor the slack matrix $(1)$. In Milestone 4 the column $*_n$ is an arbitrary real vector. The slack matrices of Theorem 3.3 are encoded through the identification on p. 9 of the paper: rows are vertices of $P$, columns are extreme points $y$ of the polar $P^\circ = \{y : \langle x, y \rangle \le 1\ \forall x \in P\}$, the canonical entry is $1 - \langle p, y\rangle$, and every slack matrix is the canonical one with positively scaled columns. Facets in Milestone 3 are nonempty proper exposed faces of dimension one less than the polytope.

The goal must not be weakened to proper lifts, and lifts must use equality $\mathrm{STAB}(G) = \pi(\mathcal S^n_+ \cap L)$ with $\pi$ linear and $L$ affine; with inclusion, or with arbitrary maps, the statement becomes trivial or false. The core lemma is meaningful only with both factor families positive semidefinite; without that requirement $S'$ factors trivially.

Beyond the milestones, a complete proof of the goal needs two facts the paper uses without stating them as claims of this proof: (a) an $\mathcal S^n_+$-lift that is not proper is a proper lift to a face of $\mathcal S^n_+$ (p. 5), every face of $\mathcal S^n_+$ is isomorphic to some $\mathcal S^r_+$ with $r \le n$ (Example 4.2, p. 12), and an $\mathcal S^r_+$-factorization yields an $\mathcal S^n_+$-factorization; (b) lifts are preserved by affine maps (Proposition 2.9, pp. 6–7), and translating a polytope changes its slack matrices only by positive column scalings, which is how Theorem 3.3 applies to $\mathrm{STAB}(G)$, whose origin is a vertex rather than an interior point. Stating (a) and (b) as separate lemmas is welcome.

Needed infrastructure: positive semidefinite matrices and the trace pairing, the face structure of $\mathcal S^n_+$, invariance of lifts under affine maps, and conic duality for Theorem 3.3. All of these are reusable beyond this mission. Contributions welcome: proofs of the milestones, the bridging facts (a) and (b), and alternative routes to the goal.

Selected references

• J. Gouveia, P. A. Parrilo, R. R. Thomas, Lifts of Convex Sets and Cone Factorizations, Mathematics of Operations Research 38(2):248–264, 2013. arXiv:1111.3164v2. https://arxiv.org/abs/1111.3164
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, Journal of Computer and System Sciences 43(3):441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• L. Lovász, A. Schrijver, Cones of matrices and set-functions and 0-1 optimization, SIAM Journal on Optimization 1(2):166–190, 1991. https://doi.org/10.1137/0801013

Motivation

Matroids abstract the combinatorial content of linear independence: which sets of columns of a matrix are independent, which are maximal (bases), and how bases relate to each other. This abstraction, isolated independently by Whitney (1935) and van der Waerden's school, turned out to be exactly the right level of generality for a large family of greedy and augmenting-path algorithms — a base of a matroid can always be reached from another by a sequence of single-element swaps, and this exchange property is what makes local search on bases correct and efficient.

A natural question, raised in the 1980s once matroid-based combinatorial optimization was mature, is what happens when bases are not merely present or absent but carry real-valued weights that must interact well with the exchange structure. Dress and Wenzel answered this with the notion of a valuated matroid: a real-valued function on the bases of a matroid satisfying a weighted strengthening of the exchange axiom. Their motivation was explicitly algorithmic — valuated matroids are exactly the structures for which a greedy algorithm computes an optimal basis under linear objectives, and more generally under the family of "tilted" objectives obtained by adding an arbitrary linear functional. Independently, valuated matroids arise from the classical Grassmann–Plücker relation applied to matrices over a field with a valuation (hence the name), connecting them to tropical geometry.

This mission formalizes the two theorems of Murota's Discrete Convex Analysis (2003, §2.4) that make this story precise: the classical correspondence between a matroid's base family and its rank function (Theorem 2.29), and the characterization of valuations by a perturbation-robustness property (Theorem 2.32). Theorem 2.32 is also historically the entry point of the book's central theme — it is the special case, for the two-valued lattice $\{0,1\}^V$, of the general local-exchange criterion for M-convex functions that occupies chapters 6 and 7.

Setting

Let $V$ be a finite set (the ground set). A matroid on $V$ is a pair $(V, \mathcal B)$ where $\mathcal B$, the base family, is a nonempty family of subsets of $V$ satisfying the simultaneous exchange axiom (B): for every $J, J' \in \mathcal B$ and every $i \in J \setminus J'$, there exists $j \in J' \setminus J$ such that both

$$J - i + j := (J \setminus \{i\}) \cup \{j\} \in \mathcal B \quad\text{and}\quad J' + i - j := (J' \setminus \{j\}) \cup \{i\} \in \mathcal B.$$

Equivalently (Theorem 2.29 below), a matroid can be described by its rank function $\rho : 2^V \to \mathbb Z$, a set function satisfying:

• (R1) $0 \le \rho(X) \le |X|$ for every $X \subseteq V$;
• (R2) monotonicity: $X \subseteq Y \implies \rho(X) \le \rho(Y)$;
• (R3) submodularity: $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$.

A valuation of a base family $\mathcal B$ is a function $\omega : \mathcal B \to \mathbb R$ satisfying the axiom (VM): for every $J, J' \in \mathcal B$ and $i \in J \setminus J'$, there is $j \in J' \setminus J$ with $J - i + j, J' + i - j \in \mathcal B$ and

$$\omega(J) + \omega(J') \le \omega(J - i + j) + \omega(J' + i - j).$$

The pair $(V, \omega)$ is then a valuated matroid. For $p : V \to \mathbb R$, the perturbation of $\omega$ by $p$ is

$$\omega[-p](J) = \omega(J) - \sum_{j \in J} p(j).$$

Formalization targets

Goal: Theorem 2.32 (the valuated matroid characterization)

$$\omega \text{ is a valuation of } \mathcal B \iff \forall\, p : V \to \mathbb R,\ \{J \in \mathcal B : \omega[-p](J') \le \omega[-p](J)\ \forall J' \in \mathcal B\} \text{ is a nonempty family satisfying (B)}.$$

The right-hand side says: for every linear perturbation $p$, the set of $\omega[-p]$-maximal bases is again the base family of a matroid. The universal quantifier over $p$ is not optional — a version of this statement quantified over a single fixed $p$ is either vacuous or false, and does not capture what makes valuated matroids useful.

Milestone: Theorem 2.29 (the base-family / rank-function correspondence)

The maps

$$\rho(X) = \max\{|X \cap J| : J \in \mathcal B\}, \qquad \mathcal B = \{J \subseteq V : \rho(J) = |J| = \rho(V)\}$$

are mutually inverse bijections between nonempty families satisfying (B) and set functions satisfying (R1)-(R3). This is weaker groundwork than the goal, stated first because it fixes the exact axiomatic vocabulary — (B) and (R) — that Theorem 2.32 is built on.

Significance

The result itself. Theorem 2.32 is the reason valuated matroids are the right object for weighted combinatorial optimization on matroids: it says a function on bases behaves correctly under every linear re-weighting of the ground set exactly when it satisfies the local exchange inequality (VM). This is what guarantees, for instance, that a greedy algorithm which is correct for the unweighted matroid extends correctly to families of tilted objectives, and it is the germ of the general local-optimality criterion for M-convex functions (chapters 6–7), which underlies most of the algorithmic content of the rest of the book. Theorem 2.29 is the classical result — due jointly to the development of matroid theory from the 1930s onward — that the base-exchange and rank-submodularity axiomatizations of a matroid carry the same information; it is the finite, unweighted precursor of Theorem 2.32.

Formalizing it. Neither theorem has a machine-checked proof on the platform prior to this mission (see Formalization scope for the prior-art check). Theorem 2.29's own proof is elementary but has two independent halves (each map preserves its target axiom class, and the two maps compose to the identity in both directions) that must all be established; Theorem 2.32's proof, as given in the source, defers entirely to a later, more general chapter-6 theorem, so a solver working only from this mission must either reconstruct a direct combinatorial argument for this special case or await chunk 06 (DiscreteConvex.MConvexFunctions, a separate mission) and specialize its main theorem.

Difficulty

The obvious approach to Theorem 2.32 — fix an optimal basis $J$ for $\omega[-p]$ and try to show the exchange condition on maximizers directly from (VM) — proves one direction (VM implies the maximizer property) in a few lines, since perturbing does not change which exchange moves are available. The converse is the substantial direction: from "the maximizer set is always a matroid, for every $p$," one must recover the single global inequality (VM) that must hold for all pairs $J, J' \in \mathcal B$, not just optimal ones. The standard argument constructs, for a given non-optimal pair, a perturbation $p$ under which that specific pair becomes simultaneously optimal, and this construction is exactly the step the book skips by citing chapter 6's general theorem. A formalization attempting to bypass this by only checking the maximizer property for a finite or generic sample of perturbations would trivialize the statement to something false or vacuous — a pitfall the goal's explicit ∀ p is designed to prevent.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $2^V$ is represented as Finset (Finset V), and $V \to \mathbb R$ as a plain function type. The rank function is $\mathbb Z$-valued (matching the book's own convention for matroid rank, as opposed to the $\mathbb R$-valued conventions used from chapter 6 onward for general M-convex functions); RankOfFamily is implemented with Finset.sup over $\mathbb N$ rather than a partial max', so that it is a total function — its junk value at the empty family is never invoked, since every hypothesis in this mission supplies nonemptiness explicitly, matching the book's own phrasing.

A trivializing formalization of the goal is one that quantifies over a single fixed $p$, or allows $\mathcal B$ to be empty; both are explicitly excluded by keeping $\mathcal B.\text{Nonempty}$ a hypothesis and $p$ universally quantified inside the theorem statement itself.

Checked against Mathlib (commit 0df444a360eaa60ab8c11dca51a86af692955474): Mathlib's Matroid structure is axiomatized via the single-element (asymmetric) exchange property, classically but not definitionally equivalent to Murota's simultaneous axiom (B) used throughout this book, and Mathlib provides no constructor recovering a base family or a Matroid from a bare rank function satisfying (R1)-(R3). Theorem 2.29 is therefore genuine, reusable infrastructure, not a restatement of existing Mathlib API. No reference item was found on the platform for either theorem (GET /theorems?q=matroid, q=valuated matroid return only unrelated tropical-geometry and k-server results). Contributions to a shared DiscreteConvex.Combinatorial definitions layer (the exchange and rank axioms) are welcome from later chunks of this series that build on matroid or base-polyhedron structure.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• H. Whitney, "On the abstract properties of linear dependence," American Journal of Mathematics, 57(3), 1935, pp. 509–533.
• A. W. M. Dress, W. Wenzel, "Valuated matroids," Advances in Mathematics, 93(2), 1992, pp. 214–250.
• R. A. Brualdi, "Comments on bases in dependence structures," Bulletin of the Australian Mathematical Society, 1(2), 1969, pp. 161–167.

Why robustify a sampled stochastic program

Many decision problems under uncertainty take the form of a stochastic program: choose a decision $v$ from a feasible set $\mathcal F$ to maximise the expected utility $\mathbb E_{x\sim\mu}[f(v,x)]$, where the distribution $\mu$ of the uncertain parameter $x\in\mathbb R^m$ is known only through i.i.d. samples $x_1,\dots,x_n$. The standard remedy, sample average approximation, maximises $\frac1n\sum_i f(v,x_i)$ instead. Its consistency (convergence of the optimal expected utility of its solutions to the true optimum) is classical, but it needs regularity assumptions of its own, for example those of King and Wets (Stochastics and Stochastic Reports, 1991), cited on p. 98 of the paper; the paper presents its construction as a route to consistency under weaker conditions.

Robust optimization (RO) takes a different route: it protects each sample by an uncertainty set and optimises against the worst point in it. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that RO over several overlapping uncertainty sets is equivalent to a distributionally robust stochastic program (their Theorem 2.1, the subject of mission I of this series). Section 3 of the paper uses that equivalence to show that a specific robustification of the sampled problem, with $\ell_\infty$ boxes of shrinking radius around each sample, is consistent under only boundedness and equicontinuity of $f$. This mission formalizes that result, Theorem 3.1.

Setting

Equip $\mathbb R^m$ with the sup norm $\|z\|_\infty=\max_k|z_k|$, its Borel $\sigma$-algebra and Lebesgue measure $dx$. The data are:

• a set of decisions $V$ and a nonempty feasible set $\mathcal F\subseteq V$;
• a utility $f:V\times\mathbb R^m\to\mathbb R$, Borel measurable in $x$ for each $v$;
• a true density $h^*$ on $\mathbb R^m$ (nonnegative, $\int h^*\,dx=1$) and i.i.d. samples $x_1,x_2,\dots$ with distribution $h^*(x)\,dx$;
• radii $\epsilon(n)>0$.

For a sample $x_1,\dots,x_n$ the boxes are $\mathcal Z_i=\{x_i+\delta\mid\|\delta\|_\infty\le\epsilon(n)\}$, and the box-robust sample objective is

$$J_n(v)=\frac1n\sum_{i=1}^n\ \inf_{\|\delta_i\|_\infty\le\epsilon(n)}f(v,x_i+\delta_i)=\sum_{i=1}^n\frac1n\inf_{x_i'\in\mathcal Z_i}f(v,x_i').$$

The RO solution $v(n)$ is a maximiser of $J_n$ over $\mathcal F$. The equicontinuity modulus of $f$ is

$$d(\epsilon)=\sup_{v,\,x,\ \|\delta\|_\infty\le\epsilon}|f(v,x)-f(v,x+\delta)|.$$

The proof works with the distribution set $\mathcal P_n$ of probability measures $\mu$ with $\mu(\bigcup_{i\in S}\mathcal Z_i)\ge|S|/n$ for every $S\subseteq\{1,\dots,n\}$, and with the uniform box kernel density estimator

$$h_n(x)=(n\epsilon(n)^m)^{-1}\sum_{i=1}^nK\Big(\frac{x-x_i}{\epsilon(n)}\Big),\qquad K(z)=\frac{\mathbf 1(\|z\|_\infty\le1)}{2^m}.$$

Formalization targets

Goal: Theorem 3.1 (p. 98)

Assume $|f(v,x)|\le C$ for all $v,x$; $d(\epsilon)\to0$ as $\epsilon\downarrow0$; $\epsilon(n)\downarrow0$ and $n\epsilon(n)^m\uparrow\infty$. Then for every choice of maximisers $v(n)$, with probability one,

$$\lim_{n\to\infty}\int_{\mathbb R^m}f(v(n),x)\,h^*(x)\,dx=\sup_{v\in\mathcal F}\int_{\mathbb R^m}f(v,x)\,h^*(x)\,dx .$$

Milestones (proof of Theorem 3.1, p. 99)

1. $h_n$ is the density of a probability measure in $\mathcal P_n$.
2. $J_n(v)\le\int f(v,x)\,h_n(x)\,dx$ for every $v$.
3. Oscillation over a box: $\sup_{\mathcal Z_i}f(v,\cdot)-\inf_{\mathcal Z_i}f(v,\cdot)\le d(2\epsilon(n))$.
4. Eq. (7): with $M_n=C\int|h_n-h^*|\,dx$, for every $v$,

$$J_n(v)-M_n\le\int f(v,x)h^*(x)\,dx\le J_n(v)+M_n+d(2\epsilon(n)).$$

5. Strong $L^1$ consistency of the box kernel density estimator: if $\epsilon(n)\to0$ and $n\epsilon(n)^m\to\infty$, then $\int|h_n-h^*|\,dx\to0$ almost surely.

Milestones 1–4 are deterministic statements about a fixed sample; milestone 5 is the only probabilistic input.

Significance

Theorem 3.1 gives consistency of a tractable robust reformulation of a sampled stochastic program under conditions the paper notes are weaker than those of King and Wets for sampled stochastic programs: $f$ need only be bounded and equicontinuous in $x$, uniformly in $v$, and the true distribution need only have a density. It also gives an explicit schedule for the size of the uncertainty set, $\epsilon(n)\to0$ with $n\epsilon(n)^m\to\infty$, the bandwidth condition of kernel density estimation. Section 4 of the paper applies the same distributional interpretation to regularised learning methods such as the support vector machine and the Lasso.

The result is proved in the paper, with the $L^1$ consistency of kernel density estimators (Devroye 1983; Devroye and Györfi 1985) cited rather than proved. No part of it is formalized in Lean or on this platform as far as a search of the platform found. A complete development would produce, besides Theorem 3.1, a machine-checked strong $L^1$ consistency theorem for kernel density estimators, which is a basic result of nonparametric statistics in its own right.

Difficulty

The deterministic part (milestones 1–4) is measure-theoretic bookkeeping: the kernel integrates to one only because the box is a sup-norm ball of volume $(2\epsilon)^m$, and every infimum and supremum must be handled with care, since $f$ need not attain them.

The obstacle is milestone 5. Almost-sure $L^1$ convergence of $h_n$ to an arbitrary density $h^*$, with no continuity or support assumption, does not follow from the strong law of large numbers applied pointwise: $h_n(x)$ is an average of $n$ terms whose law changes with $n$ through $\epsilon(n)$, and almost-sure convergence at each fixed $x$ does not give convergence of the integral along a single sample path. The theorem needs both a bias estimate valid for every integrable density and a concentration estimate for the random $L^1$ error. Mathlib has Lebesgue differentiation and the strong law, but no kernel density estimator and no such concentration result.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ, whose Mathlib norm is the sup norm; boxes are Metric.closedBall. The integrals $\int f(v,x)h^*(x)\,dx$ are Bochner integrals against Lebesgue measure of integrable integrands.
• The samples are a sequence X : ℕ → Ω → Fin m → ℝ on a probability space, independent (iIndepFun) and each with law volume.withDensity h*; $x_1,x_2,\dots$ become X 0, X 1, …, and the $n$-th problem uses the first $n$. "With probability one" is ∀ᵐ ω ∂P.
• The goal quantifies over every selection $v(n)$ of maximisers, with no measurability assumed; a version with one chosen maximiser would be weaker and is ruled out.
• Readings and corrections of the printed text:
  • the kernel argument printed $(x-x_i)/\epsilon$ on p. 98 is read as $(x-x_i)/\epsilon(n)$, as the proof on p. 99 writes it;
  • "$\max_{v,x}|f(v,x)|\le C$" is read as the uniform bound $|f|\le C$ and the "max" in $d(\epsilon)$ as a supremum;
  • "$d(\epsilon)\downarrow0$" is read as $d(\epsilon)\to0$ as $\epsilon\downarrow0$;
  • implicit hypotheses made explicit: $\mathcal F\ne\emptyset$, $\epsilon(n)>0$, measurability of $f(v,\cdot)$, $h^*$ a Lebesgue density;
  • the monotonicity in "$\epsilon(n)\downarrow0$, $n\epsilon(n)^m\uparrow\infty$" is kept in the goal; milestone 5 uses the limits only, as the paper states it;
  • the paper's $M_n$ ("there exists $\{M_n\}\to0$") is made explicit as $M_n=C\int|h_n-h^*|$, so Eq. (7) is stated for every sample.
• Remark 3.2 and Appendix B (an integrable envelope in place of boundedness) are not part of this mission.
• Every real infimum and supremum ranges over a nonempty set of values bounded by $C$ in absolute value, so no statement holds through a junk value; a formalization in which the supremum over $\mathcal F$ or the box infimum could be vacuous is excluded.
• The definitions (boxes, $\mathcal P_n$, the kernel, the estimator, $J_n$, $d$) live in one definition file. $\mathcal P_n$ duplicates, with weights $1/n$, the distribution set of mission I; the duplication is deliberate because draft missions cannot import each other.
• Welcome contributions: the kernel density estimator and its strong $L^1$ consistency as reusable infrastructure, and any of the deterministic milestones.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• L. Devroye, The equivalence of weak, strong and complete convergence in $L_1$ for kernel density estimates, Annals of Statistics 11(3):896–904, 1983.
• L. Devroye, L. Györfi, Nonparametric Density Estimation: The $L_1$ View, Wiley, 1985.
• A. J. King, R. J.-B. Wets, Epi-consistency of convex stochastic programs, Stochastics and Stochastic Reports 34(1), 1991 (reference [22] of the paper).