All missions

Motivation

Conic quadratic problems (also called second-order cone programs) arise directly in applications such as contact problems with Coulomb friction, and a wide range of nonlinear convex problems can be rewritten in this form (Lobo, Vandenberghe, Boyd and Lebret 1998). Interior-point methods solve them in polynomial time, but around 2000 the available software for conic quadratic problems handled far fewer variables than linear programming software. Ben-Tal and Nemirovski (2001) therefore asked whether a conic quadratic problem can be replaced by a linear program of comparable size. Their construction replaces each second-order cone by a polyhedral cone that is exact up to a factor $1+\varepsilon$. The feasible set of the resulting linear program, projected back to the original variables, lies between the feasible set of the original problem and that of its $\varepsilon$-relaxation.

This sandwich is only useful if the relaxed problem is close to the original one, and in general it is not: the paper notes that (CQP) can be infeasible while every relaxation with $\varepsilon>0$ is feasible. Proposition 4.1 of the paper, the target of this mission, gives a sufficient condition under which the two feasible sets are $O(\varepsilon)$-close.

Setting

For $y\in\mathbb R^k$ let $\|y\|_2=\sqrt{y^Ty}$ be the Euclidean norm. A conic quadratic problem in the variable $x\in\mathbb R^n$ is

$$\text{(CQP)}\qquad \min_x\bigl\{e^Tx \bigm| Ax\ge b,\ \|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell,\ \ell=1,\dots,m\bigr\},$$

where $A$ is a $k_0\times n$ matrix and $b\in\mathbb R^{k_0}$ (the inequality $Ax\ge b$ is componentwise), and for each $\ell$ the matrix $A_\ell$ is $k_\ell\times n$, $b_\ell\in\mathbb R^{k_\ell}$, $c_\ell\in\mathbb R^n$ and $d_\ell\in\mathbb R$. For $\varepsilon>0$ the $\varepsilon$-relaxation is

$$\text{(CQP}_\varepsilon)\qquad \min_x\bigl\{e^Tx \bigm| Ax\ge b,\ \|A_\ell x-b_\ell\|_2\le (1+\varepsilon)\bigl[c_\ell^Tx-d_\ell\bigr],\ \ell=1,\dots,m\bigr\}.$$

$\mathrm{Feas}(P)$ denotes the feasible set of a problem $(P)$; in Lean these are feas P and feasRelaxed P ε, subsets of Fin n → ℝ, for a problem datum P : CQP n k₀ m.

Two conditions on (CQP) are used.

1. Strict feasibility: there are $\bar x$ and $r>0$ with $A\bar x\ge b$ and $\|A_\ell\bar x-b_\ell\|_2\le[c_\ell^T\bar x-d_\ell]-r$ for every $\ell$ (IsStrictlyFeasible P x̄ r).
2. Semiboundedness: there is $R$ such that every feasible $x$ of (CQP) satisfies $c_\ell^Tx-d_\ell\le R$ for every $\ell$ (IsSemibounded P R).

Put $\gamma(\varepsilon)=R\varepsilon/r$.

Formalization targets

Goal: Proposition 4.1

If (CQP) has $m\ge1$ conic constraints and is strictly feasible and semibounded, then for every $\varepsilon>0$ with $\gamma(\varepsilon)<1$,

$$\gamma(\varepsilon)\bar x+(1-\gamma(\varepsilon))\,\mathrm{Feas}(\mathrm{CQP}_\varepsilon)\ \subseteq\ \mathrm{Feas}(\mathrm{CQP})\ \subseteq\ \mathrm{Feas}(\mathrm{CQP}_\varepsilon). \tag{14}$$

The left-hand side is the image of $\mathrm{Feas}(\mathrm{CQP}_\varepsilon)$ under $y\mapsto\gamma(\varepsilon)\bar x+(1-\gamma(\varepsilon))y$, not a Minkowski sum.

Milestones

The milestones follow the paper's proof in order.

1. The right inclusion $\mathrm{Feas}(\mathrm{CQP})\subseteq\mathrm{Feas}(\mathrm{CQP}_\varepsilon)$ for $\varepsilon>0$.
2. For $y\in\mathrm{Feas}(\mathrm{CQP}_\varepsilon)$ and $t_\ell=c_\ell^Ty-d_\ell$, every $\delta\in[0,1]$ with $\delta\ge\varepsilon t_\ell/(r+\varepsilon t_\ell)$ for all $\ell$ makes $x_\delta=(1-\delta)y+\delta\bar x$ feasible for (CQP).
3. Under semiboundedness, the same $\delta$ satisfies $(1-\delta)t_\ell\le R$ for all $\ell$.
4. If $\delta=\varepsilon t/(r+\varepsilon t)$ with $t\ge0$, $(1-\delta)t\le R$ and $\gamma(\varepsilon)<1$, then $t\le R/(1-\gamma(\varepsilon))$ and $\delta\le\gamma(\varepsilon)$.

Significance

The result. Proposition 4.1 turns the qualitative sandwich "exact ⊆ polyhedral ⊆ relaxed" into a quantitative statement. When a problem is strictly feasible with margin $r$ and its conic right-hand sides are bounded by $R$ on the feasible set, the relaxed feasible set, shrunk towards $\bar x$ by $1-\gamma(\varepsilon)$, lies inside the exact one. The error of the relaxation is thus controlled by $\gamma(\varepsilon)=R\varepsilon/r$, which is linear in $\varepsilon$. Together with the paper's main theorem, that a polyhedral $\varepsilon$-approximation of the Lorentz cone with $O(k\ln(1/\varepsilon))$ variables and inequalities exists, this measures how well a linear program of moderate size approximates the conic problem. The paper uses it this way for the examples in its introduction.

The formalization. The proposition is proved in the paper; no machine-checked version is known. This mission produces a Lean formalization of conic quadratic problems and their relaxations with the Euclidean norm, together with the strict feasibility and semiboundedness conditions and the proof. The Lorentz-cone approximation results of the same paper are the subject of the companion missions I and II of this series.

Difficulty

The right inclusion is immediate. The left inclusion does not follow from convexity alone. A relaxed-feasible point $y$ may violate every conic constraint of (CQP), and nothing about $y$ bounds how far it is from $\mathrm{Feas}(\mathrm{CQP})$. The needed information comes from semiboundedness, which constrains only feasible points of (CQP). That hypothesis therefore cannot be applied to $y$ itself, and the shrink factor $\gamma(\varepsilon)$ must be obtained without any bound on $c_\ell^Ty-d_\ell$ given in advance. The obvious attempt, bounding the violation at $y$ by $\varepsilon R$, fails for exactly this reason.

Formalization scope

• Vectors of $\mathbb R^n$ are Fin n → ℝ; the $m$ conic constraints are indexed by Fin m (0-based) with a dependent family of matrices (ℓ : Fin m) → Matrix (Fin (k ℓ)) (Fin n) ℝ, so the row sizes $k_\ell$ may differ. The norm is written out as eucNorm y = √(∑ i, y i ^ 2); Mathlib's norm on Fin k → ℝ is the sup norm and is not used.
• Only feasible sets are compared; the objective $e$ is carried as data but plays no role.
• Correction 1. In hypothesis (i) the page prints $[c_\ell^Tx-d_\ell]-r$ without the bar over $x$. The proof uses $c_\ell^T\bar x-d_\ell-r$, which is what IsStrictlyFeasible states.
• Correction 2. The goal assumes $m\ge1$, which the paper leaves implicit. With $m=0$, semiboundedness is vacuous and $R$ may be negative, so $\gamma(\varepsilon)<0$. Then the map $y\mapsto\gamma\bar x+(1-\gamma)y$ extrapolates beyond $y$ and can leave $\{Ax\ge b\}$. An example is $n=1$, $A=[1]$, $b=0$, $\bar x=1$, $y=0$, $R=-1$, $r=\varepsilon=1$. For $m\ge1$ the hypotheses force $R\ge r>0$.
• $\varepsilon$ ranges over all $\varepsilon>0$ with $\gamma(\varepsilon)<1$, as in the paper; it is not restricted to $(0,1]$.
• The second milestone is stated for every $\delta\in[0,1]$ that dominates all ratios $\varepsilon t_\ell/(r+\varepsilon t_\ell)$, rather than only for the paper's $\delta=\max_\ell$. This includes the paper's case.
• The goal cannot be satisfied trivially. The strict feasibility and semiboundedness hypotheses are jointly satisfiable (for example $n=m=1$, the constraint $|x|\le 1$ written as $\|x\|_2\le 1$, $\bar x=0$, $r=1$, $R=1$), and the conclusion is the full two-sided inclusion with the paper's $\gamma(\varepsilon)$, not the existence of some contraction factor.
• Needed infrastructure: Euclidean-norm convexity (the triangle inequality and homogeneity for eucNorm, or a transfer to EuclideanSpace ℝ (Fin k)) and linearity of Matrix.mulVec and dotProduct. A convexity lemma for feas P would be reusable beyond this mission, and contributions of it are welcome.

Selected references

• A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
• M. S. Lobo, L. Vandenberghe, S. Boyd and H. Lebret, Applications of Second-Order Cone Programming, Linear Algebra and its Applications 284:193–228, 1998. https://doi.org/10.1016/S0024-3795(98)10032-0
• Yu. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791

Motivation

Many objective functions in optimization are pointwise maxima: the worst case of a loss over an uncertainty set, the value of a minimax problem as a function of the outer variable, a penalty $\max_i g_i(x)$ for a system of constraints, or the largest eigenvalue of a symmetric matrix. Such a function

$$f(x)=\max\{g(x,u):u\in U\}$$

is typically not differentiable even when every piece $g(\cdot,u)$ is smooth, because the maximizing $u$ jumps. Descent methods, optimality conditions and sensitivity analysis for these problems all need a substitute for the gradient of $f$ and a formula for its directional derivatives.

Danskin's theorem (Danskin 1966) answers this when $\nabla_x g(x,u)$ exists and is continuous in $(x,u)$ and $U$ is compact: $f$ has one-sided directional derivatives $f'(x;v)=\max\{\nabla_x g(x,u)\cdot v:u\in M(x)\}$, where $M(x)$ is the set of maximizers. Convex analysis gives the analogue when each $g(\cdot,u)$ is convex (Rockafellar 1970). In Generalized gradients and applications (Clarke 1975) Frank Clarke introduced the generalized gradient of a locally Lipschitz function and proved, as his first application, a single theorem, Theorem (2.1), that contains both cases. The generalized gradient became the standard object of nonsmooth analysis (Clarke 1983), and Theorem (2.1) is the prototype of every "subdifferential of a max function" rule used in minimax optimization.

Setting

Work in $\mathbb R^n$ with the Euclidean norm $|\cdot|$ and inner product $\zeta\cdot v$. A function $f:\mathbb R^n\to\mathbb R$ is locally Lipschitz if for every bounded set $B$ there is $K$ with $|f(x_1)-f(x_2)|\le K|x_1-x_2|$ for $x_1,x_2\in B$. By Rademacher's theorem such $f$ is differentiable almost everywhere.

• The generalized gradient $\partial f(x)$ (Definition (1.1)) is the convex hull of all limits $\lim_i\nabla f(x+h_i)$, where $h_i\to0$, $f$ is differentiable at each $x+h_i$, and the gradients converge.
• The generalized directional derivative (Definition (1.3)) is

$$f^\circ(x;v)=\limsup_{h\to0,\ \delta\downarrow0}\frac{f(x+h+\delta v)-f(x+h)}{\delta},$$

and the one-sided directional derivative is $f'(x;v)=\lim_{\delta\downarrow0}[f(x+\delta v)-f(x)]/\delta$ when the limit exists.

• A multifunction $\Phi$ into subsets of $\mathbb R^n$ is upper semicontinuous if $x_i\to x$, $v_i\to v$ and $v_i\in\Phi(x_i)$ imply $v\in\Phi(x)$.

For the max function, $U$ is a nonempty sequentially compact topological space and $g:\mathbb R^n\times U\to\mathbb R$. Write $\partial_xg(x,u)$, $g^\circ_x(x,u;v)$, $g'_x(x,u;v)$ for the objects above applied to $y\mapsto g(y,u)$ at $x$. Let $f(x)=\max_{u\in U}g(x,u)$ and $M(x)=\{u\in U:g(x,u)=f(x)\}$. The hypotheses of Theorem (2.1) are:

• (a) $g$ is upper semicontinuous in $(x,u)$;
• (b) $g$ is locally Lipschitz in $x$ uniformly in $u$: for each bounded $B$ one constant $K$ serves for every $u\in U$;
• (c) for all $x,u,v$, $g'_x(x,u;v)$ exists and equals $g^\circ_x(x,u;v)$;
• (d) $(x,u)\mapsto\partial_xg(x,u)$ is upper semicontinuous on $\mathbb R^n\times U$.

Formalization targets

Goal: Theorem (2.1)

Under (a)–(d):

1. $f$ is locally Lipschitz;
2. $f'(x;v)$ exists for all $x,v$;
3. $f'(x;v)=f^\circ(x;v)=\max\{\zeta\cdot v:\zeta\in\partial_xg(x,u),\ u\in M(x)\}$;
4. for every $x$,

$$\partial f(x)=\operatorname{co}\{\partial_xg(x,u):u\in M(x)\}.$$

Milestones

• Proposition (1.4): $f^\circ(x;v)=\max\{\zeta\cdot v:\zeta\in\partial f(x)\}$ for locally Lipschitz $f$.
• Corollary (1.10): if $\zeta\cdot v\le\limsup_{\delta\downarrow0}[f(x+\delta v)-f(x)]/\delta$ for all $v$, then $\zeta\in\partial f(x)$.
• Theorem (2.1)(1): under (a), (b), $f$ is locally Lipschitz.
• (2.2): $\operatorname{co}\{\partial_xg(x,u):u\in M(x)\}\subseteq\partial f(x)$.
• (2.3): if $f$ is differentiable at $\bar x$ and $u\in M(\bar x)$, then $\partial_xg(\bar x,u)=\{\nabla f(\bar x)\}$.
• Theorem (2.1)(4): the equality above.

Significance

The result. Theorem (2.1) computes the directional derivatives and the generalized gradient of a max function from those of its active pieces. It yields Danskin's theorem when $\nabla_xg$ is continuous, and the convex max rule when each $g(\cdot,u)$ is convex, and it applies to nonsmooth, nonconvex families satisfying (c), a property later called regularity (Clarke 1983, §2.3). In the same paper it is applied to the distance function $d_E(x)=\min_{e\in E}|x-e|$ to compute $\partial d_E$ (Proposition (2.4), Corollary (2.5)), which then drives the characterization of flow-invariant sets in §4. Proposition (1.4) and Corollary (1.10), which the theorem rests on, are the duality between $\partial f$ and $f^\circ$ used throughout nonsmooth optimization: Clarke stationarity, bundle methods and subgradient methods for weakly convex functions all state their results against them.

Formalizing it. The results are classical and proved; none of them, to the platform's knowledge, has a machine-checked proof. Mathlib has Rademacher's theorem, gradients and convex hulls, but no Clarke generalized gradient. This mission builds the first layer of nonsmooth analysis: the definitions of $\partial f$, $f^\circ$, $f'$ and upper semicontinuity of multifunctions, the support-function duality, and the max rule.

Difficulty

The obvious approach reads $\partial f(x)$ off a single active piece. It fails because the active set $M(x+h)$ changes as $h\to0$, may be infinite, and need not converge; $f$ can be differentiable at points where no individual piece is known to be. Hypothesis (c) cannot be dropped: for $U$ a single point and $g(x,u)=-|x|$ on $\mathbb R$, $f=g$ has $f'(0;v)=-|v|$ while $f^\circ(0;v)=|v|$, so conclusion (3) fails. Limits of maximizers exist only through the sequential compactness of $U$ together with (a), and limits of gradients only through the joint closed-graph condition (d) in $(x,u)$; continuity in $x$ for each fixed $u$ is not enough. Proposition (1.4), on which everything rests, is itself a measure-theoretic statement: it relates the upper limit of difference quotients over all nearby base points to gradients that exist only almost everywhere.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\zeta\cdot v$ is inner ℝ ζ v, $\nabla f$ is Mathlib's gradient, and "$\nabla f(x)$ exists" is DifferentiableAt ℝ f x.
• "Locally Lipschitz" is the paper's bounded-set form, LipschitzOnBounded. Hypothesis (b) is ∀ B bounded, ∃ K, ∀ u, LipschitzOnWith K (g · u) B: the constant is uniform in $u$.
• $\partial f(x)$ is the plain convex hull (no closure) of limits of gradients taken only at differentiability points; without that restriction $0$ would belong to every $\partial f(x)$, because gradient is $0$ where $f$ is not differentiable.
• $f^\circ$ is Filter.limsup in $\mathbb R$ along $\mathcal N(0)\times\mathcal N_{>}(0)$; this is a junk value for non-Lipschitz $f$, so every statement using $f^\circ$ assumes the Lipschitz hypothesis. The one-sided derivative is a Tendsto along $\mathcal N_{>}(0)$.
• "max" in conclusions is IsGreatest, which asserts attainment. The max function is ⨆ u, g x u; $U$ is nonempty ([Nonempty U]) and SeqCompactSpace, and (a) is Mathlib's UpperSemicontinuous on $\mathbb R^n\times U$. The paper uses $U\ne\emptyset$ implicitly; with $U=\emptyset$ conclusion (4) would be false.
• (d) is the sequential closed-graph property in $(x,u)$ jointly, not Mathlib's UpperHemicontinuous.
• A formalization in which $\partial f$ contains junk gradients, $f^\circ$ is a limsup without the Lipschitz hypothesis, or "max" is sSup without attainment would make the statements trivial or false; these are ruled out as above.

Contributions welcome: proofs of the milestones, in particular Proposition (1.4) and Corollary (1.10), which are reusable for every later nonsmooth-analysis mission; lemmas that $\partial f(x)$ is nonempty and compact; the equivalence of LipschitzOnBounded with Mathlib's LocallyLipschitz.

Selected references

• F. H. Clarke, Generalized gradients and applications, Trans. Amer. Math. Soc. 205 (1975), 247–262. https://doi.org/10.1090/s0002-9947-1975-0367131-6
• J. M. Danskin, The theory of max-min, with applications, SIAM J. Appl. Math. 14 (1966), 641–664. https://doi.org/10.1137/0114053
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; SIAM Classics reprint 1990. https://doi.org/10.1137/1.9781611971309

Motivation

A linear program is solved with known data, but in planning problems the data are often only known in distribution when the main decision is taken: demands, yields and requirements are revealed later, and a corrective action is taken after they are. E. M. L. Beale's 1955 paper On Minimizing a Convex Function Subject to Linear Inequalities formulates this situation in its §5, "Linear Programming with Random Coefficients", as what is now called a two-stage stochastic linear program with recourse. Beale's motivating example is the transportation problem of Hitchcock (1941) with random requirements at the destinations, where every unit of shortage or excess incurs a loss. The same model was put forward in the same year by Dantzig, Linear Programming under Uncertainty (Management Science, 1955), as the paper's note added in proof acknowledges.

Timeline:

• 1955. Beale (§5, Theorems 2 and 3) and Dantzig independently introduce two-stage linear programs with random data; Beale proves that the expected cost is convex in the first-stage decision, and that the cost is convex in the random data for fixed decision.
• 1967. Walkup and Wets, Stochastic Programs with Recourse, study the domain of the expected recourse function and its properties under fixed recourse.
• 1974. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, gives the systematic treatment of convexity, finiteness and polyhedrality of the expected recourse function, now textbook material (Birge and Louveaux, Introduction to Stochastic Programming, Ch. 3).

Setting

Constants $c\in\mathbb R^n$, $f\in\mathbb R^p$ and an $m\times p$ matrix $D=(d_{ik})$ are given. The data $A=(\alpha_{ij})$, an $m\times n$ matrix, and $\beta\in\mathbb R^m$ are random variables on a probability space $(\Omega,P)$: their distribution is known when the first-stage decision $x\in\mathbb R^n$, $x\ge0$, is chosen, and their values are known when the second-stage decision $y\in\mathbb R^p$, $y\ge0$, is chosen. The cost is

$$C=c'x+f'y,\qquad Ax+Dy=\beta. \qquad(5.3),(5.4)$$

For a right-hand side $b\in\mathbb R^m$ the second-stage value is

$$Q(b)=\min\{f'y : y\ge0,\ Dy=b\},$$

and for fixed data the cost of a first-stage decision is $C(x)=c'x+Q(\beta-Ax)$. The expected cost is

$$E(C)(x)=\int_\Omega \bigl(c'x+Q(\beta(\omega)-A(\omega)x)\bigr)\,dP(\omega).$$

The problem is to choose $x\ge0$ minimising $E(C)$. In Lean the value is secondStageValue D f b, the cost is cost c f D A β x, and the expected cost is expectedCost P c f D A β x, all in the namespace BealeConvexMin.RandomLP.

Formalization targets

Goal: Theorem 2 (p. 182)

Assume that for every $x\ge0$ the second-stage minimum is attained for almost every outcome and that $\omega\mapsto C(x,\omega)$ is integrable. Then

$$E(C)(\lambda_1x_1+\lambda_2x_2)\le\lambda_1E(C)(x_1)+\lambda_2E(C)(x_2)\qquad(x_1,x_2\ge0,\ \lambda_1,\lambda_2\ge0,\ \lambda_1+\lambda_2=1),$$

that is, $E(C)$ is convex on the non-negative orthant. The statement fixes no distribution class: it is claimed for any known distribution of $(A,\beta)$.

Milestones

1. Pointwise convexity (last display of the proof of Theorem 2, p. 182): for fixed data $(A,\beta)$, with the minimum attained at every $x\ge0$,

$$C(\lambda_1x_1+\lambda_2x_2)\le\lambda_1C(x_1)+\lambda_2C(x_2).$$

2. Theorem 3 (p. 182): for fixed $x$, the cost $(A,\beta)\mapsto c'x+Q(\beta-Ax)$ is jointly convex on every convex set of data on which the second-stage minimum is attained.
3. Eqs. (5.5)–(5.6) (p. 182): for a finitely supported distribution, $A=A_r$ and $\beta=\beta_r$ with probability $p_r$, the value $E(C)(x)$ is the minimum of $c'x+\sum_r p_r f'y_r$ over non-negative $y_r$ with $A_rx+Dy_r=\beta_r$ for all $r$; minimising $E(C)$ is then a linear program.

Significance

The result. Theorem 2 is the basic structural fact of two-stage stochastic linear programming: the first-stage problem is a convex program in $x$, whatever the distribution of the data. It is what makes local optimality global for the first-stage problem, what justifies cutting-plane and decomposition methods that approximate $E(C)$ from below by supporting hyperplanes, and what makes sample-average approximations convex programs. Theorem 3, joint convexity in the data, gives through Jensen's inequality the comparison between the stochastic problem and its mean-value problem that Beale draws on p. 182. The discrete reformulation (5.5)–(5.6) is the deterministic-equivalent linear program used for finitely many scenarios.

Formalizing it. The theorems are proved in the paper, and their content is classical. The mission produces machine-checked statements of the model with its implicit hypotheses made explicit (attainment of the second stage, integrability of the cost), and proofs of the three results in Lean. The platform already has related statements in other models (finite scenario sets with extended-real recourse, and a complete-recourse, finite-second-moment version); none has Beale's hypotheses, and none states convexity of $c'x+E\,Q$ for an arbitrary distribution.

Difficulty

The mathematics is short; the difficulty is in the encoding. The second-stage value is a minimum that may fail to exist: the second stage may be infeasible for some $x$ and some outcomes, or unbounded below. A real-valued infimum then takes an arbitrary default value, and convexity would become a statement about that default. Similarly, the mean value only exists when the cost is integrable. A faithful statement has to carry attainment and integrability exactly where the paper tacitly assumes them, on the domain $x\ge0$ the paper uses, and no stronger condition (such as complete recourse or moment bounds) that the paper does not make. In the discrete reformulation, the minimum over the whole family $(y_r)_r$ has to be matched with the probability-weighted sum of per-scenario minima.

Formalization scope

• Vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, inner products dotProduct, and $y\ge0$ is the componentwise order. The random data are functions A : Ω → Matrix (Fin m) (Fin n) ℝ and β : Ω → Fin m → ℝ on a measurable space with a probability measure P; no measurability of the data is assumed beyond integrability of the cost.
• The second-stage value is the real infimum of $f'y$ over the feasible set. It equals $0$ on an infeasible or unbounded-below second stage, so each theorem assumes attainment of the minimum where it is evaluated (the paper's "value of $y$ that minimizes $C$"). The goal assumes attainment for almost every outcome at every $x\ge0$.
• $E(C)$ is the Bochner integral, which is $0$ for a non-integrable integrand, so the goal assumes integrability of $C(x,\cdot)$ at every $x\ge0$ (the paper's "mean value $E(C)$").
• Convexity is claimed on $\{x : x\ge0\}$, the paper's domain, not on all of $\mathbb R^n$. Theorem 3 is stated for fixed non-negative $x$ (the model's first-stage domain) and on every convex set of data on which the minimum is attained, since the paper names no domain.
• A formalization in which the value is an unconstrained infimum without attainment, or the expectation is taken without integrability, is trivially convex on the region where the default values apply and does not state Beale's theorem; such variants are ruled out.
• Reusable beyond this mission: basic facts on the optimal value of a parametric linear program in its right-hand side and cost data, and convexity of integrals of pointwise-convex integrands. Proofs of the milestones and of the goal, and alternative formulations in extended reals, are welcome.

Selected references

• E. M. L. Beale, On Minimizing a Convex Function Subject to Linear Inequalities, Journal of the Royal Statistical Society, Series B 17(2):173–184, 1955. https://doi.org/10.1111/j.2517-6161.1955.tb00191.x
• G. B. Dantzig, Linear Programming under Uncertainty, Management Science 1(3–4):197–206, 1955. https://doi.org/10.1287/mnsc.1.3-4.197
• F. L. Hitchcock, The Distribution of a Product from Several Sources to Numerous Localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224
• D. W. Walkup and R. J.-B. Wets, Stochastic Programs with Recourse, SIAM Journal on Applied Mathematics 15(5):1299–1314, 1967. https://doi.org/10.1137/0115113
• R. J.-B. Wets, Stochastic Programs with Fixed Recourse: The Equivalent Deterministic Program, SIAM Review 16(3):309–339, 1974. https://doi.org/10.1137/1016053
• J. R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4

Motivation

Many computations in scientific computing, statistics and machine learning need the trace of a matrix $A$ that is never formed explicitly: $A$ may be $f(B)$ for a large sparse $B$, an inverse $B^{-1}$, or a product of operators, and the only access to it is the ability to compute products $Az$ for chosen vectors $z$. Examples are log-determinant estimation in Gaussian process regression, counting triangles in graphs through $\mathrm{trace}(B^3)$, computing charge densities in electronic structure calculations, and generalized cross-validation in regularized regression. For such matrices the $n$ diagonal entries are not available, and computing them one at a time costs $n$ matrix–vector products.

Randomized trace estimators replace this by a small number $M$ of products: draw random vectors $z_1,\ldots,z_M$ from a fixed distribution with $\mathrm{E}(z_i^T A z_i) = \mathrm{trace}(A)$ and average the quadratic forms. Hutchinson (1989) introduced the estimator with Rademacher vectors and computed its variance; Silver and Röder (1997) used Gaussian vectors. Before Avron and Toledo (2011), the analyses of these estimators were variance computations, which do not say how many samples guarantee a given relative accuracy with a given probability. Avron and Toledo gave the first such sample bounds for several estimators, stated in terms of an $(\epsilon,\delta)$ guarantee; this mission formalizes their bound for the Gaussian estimator. Later work (Roosta-Khorasani and Ascher 2015; Cortinovis and Kressner 2022) sharpened these bounds and extended them to indefinite matrices.

Setting

Let $A \in \mathbb{R}^{n\times n}$ be symmetric positive semi-definite, and write $\tau = \mathrm{trace}(A)$. Fix a number of samples $M \ge 1$. Let $z_1, \ldots, z_M \in \mathbb{R}^n$ be random vectors whose $Mn$ entries are independent standard normal random variables. The Gaussian trace estimator (Definition 3.1) is

$$G_M = \frac{1}{M}\sum_{i=1}^{M} z_i^T A z_i .$$

Each term $z_i^TAz_i$ has expectation $\mathrm{trace}(A)$, so $G_M$ is unbiased. A randomized trace estimator $T$ is an $(\epsilon,\delta)$-approximator of $\mathrm{trace}(A)$ (Definition 4.1) if

$$\Pr\bigl(|T - \mathrm{trace}(A)| \le \epsilon\,\mathrm{trace}(A)\bigr) \ge 1-\delta ,$$

that is, if its relative error is at most $\epsilon$ except on an event of probability at most $\delta$.

The analysis uses the eigenvalues $\lambda_1,\ldots,\lambda_n \ge 0$ of $A$, listed with multiplicity, and the polynomial $h(t) = \sum_{s=2}^{n}(-2)^s t^s \sum_{|S| = s}\prod_{i\in S}\lambda_i$, where $S$ ranges over subsets of $\{1,\ldots,n\}$; it satisfies $\prod_i(1-2\lambda_i t) = 1 - 2\tau t + h(t)$.

Formalization targets

Goal: Theorem 5.2 (corrected)

For every symmetric positive semi-definite $A$, every $0 < \epsilon \le 1/10$, every $0<\delta<1$ and every natural number $M$ with

$$M \ge 20\,\epsilon^{-2}\ln(2/\delta),$$

the estimator $G_M$ is an $(\epsilon,\delta)$-approximator of $\mathrm{trace}(A)$. The sample count depends on neither $n$ nor $A$.

Milestones

1. Lemma 5.1. For symmetric $A$, $\mathrm{E}(G_1) = \mathrm{trace}(A)$ and $\mathrm{Var}(G_1) = 2\|A\|_F^2$.
2. Eq. (1). For symmetric $A$ and every $t$ with $2\lambda_i t < 1$ for all $i$, the moment generating function of $Z = MG_M$ is

$$m_Z(t) = \prod_{i=1}^{n}(1-2\lambda_i t)^{-M/2} = (1 - 2\tau t + h(t))^{-M/2}.$$

3. Elementary symmetric sums (p. 8:8). For non-negative $x_1,\ldots,x_n$ and $1\le i\le n$, $\sum_{|S|=i}\prod_{j\in S}x_j \le (\sum_j x_j)^i$; hence $|h(t)| \le \sum_{j=2}^{n}(2\tau t)^j$ for $t\ge0$ when all $\lambda_i\ge0$.
4. Upper tail (pp. 8:8–8:9). If $\tau > 0$, $M\ge1$ and $0<\epsilon\le 0.1$, then

$$\Pr\bigl(G_M \ge \tau(1+\epsilon)\bigr) \le \exp(-M\epsilon^2/20).$$

5. Both tails (p. 8:9). If $\tau>0$, $0<\epsilon\le0.1$ and $M \ge 20\epsilon^{-2}\ln(2/\delta)$, then $\Pr(G_M \ge \tau(1+\epsilon)) \le \delta/2$ and $\Pr(G_M \le \tau(1-\epsilon)) \le \delta/2$.

Significance

The theorem gives a number of matrix–vector products, $O(\epsilon^{-2}\ln(1/\delta))$, that suffices for a relative-error guarantee on the trace of any positive semi-definite matrix, independent of its dimension and spectrum. It is the reference row of the paper's Table I, against which the Hutchinson, normalized Rayleigh-quotient and unit-vector estimators are compared, and it is the form in which trace estimation enters the analysis of randomized algorithms for log-determinants, spectral densities and matrix functions.

The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The mission produces a machine-checked version with the constant $20$ and the range of $\epsilon$ made explicit, and with the misprints of the printed argument resolved (see Formalization scope). It also produces reusable pieces: the moment generating function of a Gaussian quadratic form, and the bound on elementary symmetric sums by powers of the power sum. Sharper constants, the removal of the restriction $\epsilon\le 0.1$, or a direct formalization of the lower tail through a $\chi^2$ tail bound are welcome as further theorems.

Difficulty

Unbiasedness and the variance formula do not give the result: Chebyshev's inequality with $\mathrm{Var}(G_M) = 2\|A\|_F^2/M \le 2\tau^2/M$ yields $M \ge 2\epsilon^{-2}\delta^{-1}$, with a polynomial rather than logarithmic dependence on $1/\delta$. A logarithmic bound needs exponential moments of $G_M$, and the exponential moment of $z^TAz$ is finite only for $t$ below $1/(2\lambda_{\max})$; the argument has to choose $t$ inside that range uniformly in the spectrum, using only $\lambda_{\max}\le\tau$. The second obstacle is distributional: $z^TAz$ is not a sum of independent terms in the coordinates of $z$, and reducing it to a weighted sum of independent $\chi^2$ variables requires the rotation invariance of the standard Gaussian vector. The paper proves only the upper tail with an explicit constant and states that the lower tail follows "using the same technique"; that step has to be supplied.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ; "symmetric positive semi-definite" is A.PosSemidef, "symmetric" is A.IsHermitian, and eigenvalues are Matrix.IsHermitian.eigenvalues. The sample space is Fin M → Fin n → ℝ with the product measure of $Mn$ copies of gaussianReal 0 1, so the law of the samples is constructed, not assumed; $G_M(\omega) = (M:\mathbb{R})^{-1}\sum_i \omega_i\cdot(A\omega_i)$. Probabilities are Measure.real; the moment generating function is Mathlib's mgf; the variance is Mathlib's variance, and Lemma 5.1 asserts square integrability so that neither the integral nor the variance takes its default value. The sample count is a natural number $M\ge1$; $\epsilon$ and $\delta$ are real.

Corrections of the printed text, each recorded in the item's Formalization Note:

• Theorem 5.2 is printed without a range for $\epsilon$ and is false without one (for rank-one $A$, $\epsilon=100$, $\delta=e^{-400}$ the threshold allows $M=1$, while $\Pr(\chi^2_1>101)\approx e^{-50}>\delta$). The proof gives its key bound "for $\epsilon\le0.1$"; the goal is stated for $0<\epsilon\le 1/10$.
• Eq. (1) is printed for $|\lambda_i t|\le\frac12$, which admits $1-2\lambda_it = 0$, where the moment generating function is infinite. It is stated for $2\lambda_i t<1$. The page's sum over subsets of "the set $\Lambda$ of eigenvalues" is taken over index sets, so repeated eigenvalues count with multiplicity.
• The last paragraph of the proof prints $\Pr(G_M\le\tau(1+\epsilon))\le\delta/2$ for the upper tail and $\Pr(|G_M-\tau|\le\tau(1+\epsilon))\le\delta$ for the conclusion; the intended statements are $\Pr(G_M\ge\tau(1+\epsilon))\le\delta/2$ and $\Pr(|G_M-\tau|>\epsilon\tau)\le\delta$. Milestone 5 states the upper and lower tail bounds.
• Lemma 5.1 is followed by the remark that it "also applies when $A$ is non-symmetric"; this is false for the variance and is not formalized. Definition 3.1 says "positive-definite"; the estimator is defined for every matrix and each theorem carries its own hypothesis.
• The one-sided tail milestones assume $\mathrm{trace}(A)>0$; for $A=0$ their events are certain, while the goal holds trivially.

A formalization that makes the goal trivial is ruled out: the estimator's law is the explicit product Gaussian measure rather than a hypothesis, $M$ ranges over all natural numbers above the threshold, and the approximator predicate is evaluated on the genuine event $|G_M - \mathrm{trace}(A)|\le\epsilon\,\mathrm{trace}(A)$.

A complete development needs rotation invariance of the standard Gaussian on $\mathbb{R}^n$ (Mathlib's stdGaussian_map), the moment generating function of a squared standard normal, independence of products of Gaussian vectors, and a Chernoff bound from the moment generating function. The Gaussian quadratic-form results (milestones 1 and 2) are reusable for the other Gaussian estimators of the paper, such as the rank estimator of Lemma 5.3. Proofs of any milestone, alternative proofs of the lower tail, and helper lemmas on $\chi^2$ moment generating functions are welcome.

Selected references

• H. Avron and S. Toledo, Randomized algorithms for estimating the trace of an implicit symmetric positive semi-definite matrix, Journal of the ACM 58(2), Article 8, 2011. https://doi.org/10.1145/1944345.1944349
• M. F. Hutchinson, A stochastic estimator of the trace of the influence matrix for Laplacian smoothing splines, Communications in Statistics – Simulation and Computation 18(3), 1059–1076, 1989. https://doi.org/10.1080/03610918908812806
• R. N. Silver and H. Röder, Calculation of densities of states and spectral functions by Chebyshev recursion and maximum entropy, Physical Review E 56(4), 4822–4829, 1997. https://doi.org/10.1103/PhysRevE.56.4822
• F. Roosta-Khorasani and U. Ascher, Improved bounds on sample size for implicit matrix trace estimators, Foundations of Computational Mathematics 15, 1187–1212, 2015. https://doi.org/10.1007/s10208-014-9220-1
• A. Cortinovis and D. Kressner, On randomized trace estimates for indefinite matrices with an application to determinants, Foundations of Computational Mathematics 22, 875–903, 2022. https://doi.org/10.1007/s10208-021-09525-9

Motivation

Retailers of fashion and seasonal goods sell at a premium price early in the season and mark down later. When customers anticipate the markdown, some of them wait, and the seller's pricing problem becomes a game between the seller and a population of forward-looking (strategic) customers. Aviv and Pazgal (MSOM 10(3), 2008) study this game in a model with limited inventory, stochastic arrivals and valuations that decline over the season, under two classes of seller policies: contingent pricing, where the discount depends on the inventory left, and announced fixed-discount pricing, where the seller commits to both prices upfront. Their numerical study (§7.3) compares the two classes and finds that precommitment can raise expected revenue by up to about 8%.

That comparison needs, for every announced price path, the customers' equilibrium response. Theorem 2 of the paper (p. 348) supplies it: a threshold purchasing policy, pinned down by a scalar fixed-point equation for the probability that a waiting customer is served. This mission formalizes Theorem 2. A companion mission of the same series formalizes Theorem 1, the contingent-pricing counterpart.

Setting

A seller has $Q \ge 1$ units to sell over a season $[0, H]$, split at a fixed time $T$ with $0 < T \le H$. Customers arrive by a Poisson process with rate $\lambda > 0$. Customer $j$ has a base valuation $V_j$ drawn from a continuous distribution $F$ (tail $\bar F = 1 - F$), and at time $t$ values the product at $V_j(t) = V_j e^{-\alpha t}$, where the decline factor $\alpha \ge 0$ is common to all customers.

Under an announced price path the seller commits to a premium price $p_1$ on $[0, T)$ and a discount price $p_2 \le p_1$ from $T$ on; $p_2$ does not depend on the remaining inventory. Customers know the initial inventory but not the current one.

A customer arriving at $t < T$ buys immediately if and only if (i) the current surplus $V(t) - p_1$ is nonnegative and (ii) it is at least the expected surplus of waiting,

$$\omega\cdot\max\{V(T) - p_2, 0\},$$

where $\omega$ is the probability that a unit will be allocated to the customer at time $T$. Units left at $T$ are rationed at random among the customers who request one.

For a threshold function $\psi$ on $[0, T)$ the paper defines three segment rates: $\Lambda_I(\psi)$, the expected number of customers who buy at $p_1$; $\Lambda_S(\psi, p_1, p_2)$, those who could buy at $p_1$ but wait and want to buy at $p_2$; and $\Lambda_W(p_1, p_2)$, those whose valuation was below $p_1$ and who want to buy at $p_2$. Each is $\lambda$ times an integral over $[0, T]$ of $\bar F$ at scaled prices (p. 345). With $P(x \mid \Lambda)$ the Poisson probabilities, the allocation probability of $q$ units is

$$A(q \mid \Lambda) = \sum_{y=0}^{\infty} \frac{q}{\max\{1+y, q\}}\,P(y \mid \Lambda).$$

Formalization targets

Goal: Theorem 2 (p. 348)

For $w \in [0,1]$ let

$$\psi_A(t) = \max\left\{p_1, \frac{p_1 - wp_2}{1 - we^{-\alpha(T-t)}}\right\},\qquad 0 \le t < T, \tag{7}$$

and suppose $w$ solves

$$w = \sum_{x=0}^{Q-1} P\big(x \mid \Lambda_I(\psi_A)\big)\cdot A\big(Q-x \mid \Lambda_S(\psi_A, p_1, p_2) + \Lambda_W(p_1, p_2)\big). \tag{8}$$

Then, when all other customers use $\psi_A$ (so that a waiting customer is served with the probability on the right of (8)), every customer arriving at $t \in [0, T)$ buys immediately if and only if $V(t) \ge \psi_A(t)$: the symmetric threshold profile is a Nash equilibrium.

Milestones: the two cases of the proof (p. 358)

1. If $e^{-\alpha(T-t)} \le p_2/p_1$, the threshold is $p_1$.
2. If $e^{-\alpha(T-t)} > p_2/p_1$, the threshold is $(p_1 - wp_2)/(1 - we^{-\alpha(T-t)}) \ge p_1$.

Significance

Theorem 2 reduces the customers' equilibrium under an announced path to a single scalar $w$. Everything downstream in §5 and §7 rests on it: the seller's expected revenue $\pi_{A/S}(p_1, p_2)$ (p. 348) is written in terms of $\psi_A$, the seller's optimal announced path maximizes it, and the comparison between announced and contingent pricing uses the resulting value $\pi^*_{A/S}$. The theorem also explains the qualitative prediction of the model: the threshold exceeds $p_1$ exactly when the announced discount is deep relative to the decline of valuations, and it rises with the perceived availability $w$.

The result is proved in the paper; to the best of our search it has no machine-checked proof. A formal development contributes the model objects (segment rates for threshold policies, the allocation probability for random rationing among Poisson requesters) in a form reusable by the rest of the series and by other strategic-customer pricing models, and a checked proof of the equilibrium property. The existence of a solution to (8) is not proved in the paper and is a natural further target.

Difficulty

The best-response part of the argument is elementary once the availability is known. The substance of the statement lies in the availability itself: the probability that a waiting customer is served is not a free parameter but the one generated, through (8), by the other customers' use of the same threshold. A formalization must connect the segment rates, the Poisson counts and random rationing into one expression and keep the fixed-point coupling between $w$ and $\psi_A$ intact; dropping it turns the theorem into a one-line inequality about an arbitrary $w$. The division by $1 - we^{-\alpha(T-t)}$ also degenerates when $w = 1$ and $\alpha = 0$, and has to be excluded explicitly.

Formalization scope

The Lean development lives in namespace SeasonalPricing.Announced. Conventions:

• Time is real; base valuations have law μ : Measure ℝ with IsProbabilityMeasure μ, $F$ = ProbabilityTheory.cdf μ, and continuity of $F$ (the paper's "continuous distribution") is a hypothesis of the goal. No support condition on $[0,\infty)$ is imposed; the statement quantifies over every real base valuation $V$.
• $\Lambda_I, \Lambda_S, \Lambda_W$ are interval integrals over $[0, T]$ exactly as printed. $P(x \mid \Lambda) = e^{-\Lambda}\Lambda^x/x!$ is written out; $A(q\mid\Lambda)$ is the infinite series (tsum) as printed, not its closed form.
• availability is the right-hand side of (8), with $\psi_A$ built from $w$ by (7).

Readings of the paper's informal words:

• "Nash equilibrium" is read as the best-response property the paper's proof checks: against the availability generated by (8), the immediate-purchase rule of p. 344 coincides with the threshold $\psi_A$ at every $t \in [0, T)$ and every valuation. The paper defines no strategy space beyond threshold rules.
• "$w$ is a solution to (8)": the theorem is conditional on a solution; its existence is neither assumed elsewhere nor claimed. The conditional statement has content only when (8) has a solution, which the paper does not prove.
• $w$ as a likelihood: $0 \le w \le 1$ is a hypothesis (it also follows from (8)).
• Added hypothesis: $\alpha > 0$ or $w < 1$, which keeps $1 - we^{-\alpha(T-t)} > 0$ for $t < T$; the paper's formula is undefined when it fails. In the milestones the same condition appears as $we^{-\alpha(T-t)} < 1$, and $0 < p_1$ is added so that $p_2/p_1$ is meaningful.
• The rule on $[T, H]$ (buy at $T$ iff $V(T) > p_2$) is part of the model and is not restated; $H$ does not enter the statements.

A formalization in which $w$ is an arbitrary number in $[0,1]$, not tied to (8), is ruled out: it is the best-response lemma alone, not Theorem 2. Contributions welcome: proofs of the two milestones and the goal; lemmas such as $0 \le A(q\mid\Lambda) \le 1$ and summability of its series; the closed form of $A(q \mid \Lambda)$ printed on p. 346; and an existence result for (8).

Selected references

• Y. Aviv and A. Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3):339–359, 2008. https://doi.org/10.1287/msom.1070.0183
• G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• X. Su, Intertemporal Pricing with Strategic Customer Behavior, Management Science 53(5):726–741, 2007. https://doi.org/10.1287/mnsc.1060.0667

Motivation

In high-dimensional regression the number of candidate predictors $M$ can far exceed the number of observations $n$. A regression function can then be estimated only if it is well approximated by a combination of a few elements of a large dictionary. The Lasso is the most widely used estimator in this regime. The question this mission formalizes is how well the Lasso predicts when the truth is not assumed to be sparse, or even to lie in the span of the dictionary.

A sparsity oracle inequality answers it. It bounds the prediction error of the estimator by the error of the best sparse approximation of the truth, which only an oracle knowing the truth could compute, plus a remainder proportional to the sparsity of that approximation times $\log M/n$. Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) proved such an inequality for the Lasso under their restricted eigenvalue (RE) condition. Earlier oracle inequalities for Lasso-type estimators in fixed design (Bunea, Tsybakov and Wegkamp, 2006–2007) required the Gram matrix to be positive definite or to satisfy a mutual-coherence condition. The RE condition is weaker and allows $M\gg n$, and it is now the standard hypothesis in this literature.

Setting

A dictionary $f_1,\dots,f_M$ is evaluated at fixed points $Z_1,\dots,Z_n$. This gives the design matrix $X=(f_j(Z_i))\in\mathbb R^{n\times M}$ and, for an unknown regression function $f$, the vector $f=(f(Z_1),\dots,f(Z_n))^\top$. The observations are

$$y=f+W,\qquad W_1,\dots,W_n\ \text{independent}\ \mathcal N(0,\sigma^2),\ \sigma>0 .$$

Nothing is assumed about $f$. For $v\in\mathbb R^n$ the empirical norm is $\|v\|_n=(\frac1n\sum_iv_i^2)^{1/2}$, and for $\beta\in\mathbb R^M$ we write $f_\beta=X\beta$. The column norms $\|f_j\|_n$ are assumed nonzero, with $f_{\max}=\max_j\|f_j\|_n$ and $f_{\min}=\min_j\|f_j\|_n$. The support of $\beta$ is $J(\beta)=\{j:\beta_j\neq0\}$ and its sparsity is $\mathcal M(\beta)=|J(\beta)|$.

The Lasso $\hat\beta_L$ is any minimiser of

$$\frac1n\sum_{i=1}^n\big(y_i-(X\beta)_i\big)^2+2r\sum_{j=1}^M\|f_j\|_n|\beta_j|,\qquad r=A\sigma\sqrt{\frac{\log M}{n}},\ A>2\sqrt2,$$

and $\hat f_L=X\hat\beta_L$.

Assumption RE$(s,c_0)$ holds with constant $\kappa>0$ if, for every $J_0\subseteq\{1,\dots,M\}$ with $|J_0|\le s$ and every $\delta\neq0$ with $|\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1$,

$$\kappa\sqrt n\,|\delta_{J_0}|_2\le|X\delta|_2 .$$

The paper's $\kappa(s,c_0)$ is the largest such constant.

Formalization targets

Goal: Theorem 6.1

Fix $\varepsilon>0$, $n\ge1$, $M\ge2$, $1\le s\le M$, and let RE$(s,(3+4/\varepsilon)f_{\max}/f_{\min})$ hold with constant $\kappa$. With probability at least $1-M^{1-A^2/8}$, every Lasso solution satisfies, simultaneously for all $\beta$ with $\mathcal M(\beta)\le s$,

$$\|\hat f_L-f\|_n^2\le(1+\varepsilon)\Big\{\|f_\beta-f\|_n^2+C(\varepsilon)\frac{f_{\max}^2A^2\sigma^2}{\kappa^2}\,\frac{\mathcal M(\beta)\log M}{n}\Big\},\qquad C(\varepsilon)=\frac{4(2+\varepsilon)^2}{\varepsilon(1+\varepsilon)} .$$

Milestones

1. (B.4): the noise event $\mathcal A=\bigcap_j\{2|V_j|\le r\|f_j\|_n\}$, with $V_j=n^{-1}\sum_iX_{ij}W_i$, satisfies $P(\mathcal A^c)\le M^{1-A^2/8}$.
2. (B.1) on $\mathcal A$: for every Lasso solution and every $\beta$,

$$\|\hat f_L-f\|_n^2+r\sum_j\|f_j\|_n|\hat\beta_j-\beta_j|\le\|f_\beta-f\|_n^2+4r\sum_{j\in J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j| .$$

3. Lemma B.1: the same inequality with probability at least $1-M^{1-A^2/8}$.
4. Cone step: in the case $\varepsilon\|f_\beta-f\|_n^2<4r\sum_{J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j|$, the difference $\hat\beta_L-\beta$ lies in the cone with constant $(3+4/\varepsilon)f_{\max}/f_{\min}$ at $J(\beta)$.
5. Inequality before decoupling: $\|\hat f_L-f\|_n^2\le\|f_\beta-f\|_n^2+4rf_{\max}\kappa^{-1}\sqrt{\mathcal M(\beta)}\,(\|\hat f_L-f\|_n+\|f_\beta-f\|_n)$.
6. Decoupled bound: $\|\hat f_L-f\|_n^2\le\frac{b+1}{b-1}\|f_\beta-f\|_n^2+\frac{8b^2f_{\max}^2}{(b-1)\kappa^2}r^2\mathcal M(\beta)$ for all $b>1$.
7. Corollary 6.2: the same oracle inequality with $\gamma$ in place of $\kappa$ and no global RE assumption. The infimum runs over those $\beta$ with $\mathcal M(\beta)\le s$ whose support alone satisfies the restricted eigenvalue inequality with constant $\gamma$.

Significance

The theorem says that, up to the factor $1+\varepsilon$ and a remainder of order $\mathcal M(\beta)\log M/n$, the Lasso predicts as well as the best $s$-sparse linear combination of the dictionary. This is the case even when $f$ is not sparse and not in the span of the dictionary. The remainder is the parametric rate for $\mathcal M(\beta)$ parameters, inflated by $\log M$ and by the ill-posedness factor $f_{\max}^2/\kappa^2$. Together with Theorem 5.1 of the same paper (mission II of this series), it shows that the Lasso and the Dantzig selector are within the same distance of the sparse oracle. The oracle inequality is used in aggregation, in model selection, and as a black box in later sparse-estimation papers.

The result is proved in the paper. It has not been formalized: at the time of writing, no Lasso oracle inequality and no probabilistic Lasso bound exist on Prove2Me or in Mathlib. What this mission contributes is a machine-checked proof of the paper's Theorem 6.1 with an explicit constant $C(\varepsilon)$. The paper leaves $C(\varepsilon)$ unspecified, and its proof fixes the value used here. The mission also formalizes the Gaussian-tail step (B.4) and the deterministic basic inequality (B.1), both of which are shared with the paper's other Lasso results.

Difficulty

There is no sparse truth, so the usual argument does not apply. That argument places the error $\hat\beta_L-\beta^*$ in the RE cone and reads off a rate. Here the competitor $\beta$ is arbitrary, and the approximation error $\|f_\beta-f\|_n$ can dominate the penalty terms, in which case the error is not in the cone. The RE assumption can be used only where the error does lie in a cone, and the cone constant available there depends on $\varepsilon$ and on the column-norm ratio $f_{\max}/f_{\min}$, because the penalty is weighted while RE is stated for unweighted vectors. What RE then yields is an inequality quadratic in $\|\hat f_L-f\|_n$ with a cross term, not the $(1+\varepsilon)$ form directly, and the constant $C(\varepsilon)$ is determined by how that cross term is absorbed. On the probabilistic side, the whole argument must run on one event of probability at least $1-M^{1-A^2/8}$. That event may depend neither on $\beta$ nor on the choice of minimiser. The Lasso need not have a unique solution.

Formalization scope

• The dictionary enters only through $X\in\mathbb R^{n\times M}$ (Matrix (Fin n) (Fin M) ℝ) and the target only through $f\in\mathbb R^n$, which is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, independent random variables, each with law gaussianReal 0 σ², and $\sigma>0$.
• The Lasso is an argmin predicate, and every statement is made for every minimiser. "With probability at least $p$" means a measurable event $E$ with $P(E)\ge p$, chosen before the competitor $\beta$ and the minimiser.
• RE is stated through a witness $\kappa>0$. Since $\kappa(s,c_0)$ is attained and every bound decreases in $\kappa$, this is equivalent to the paper's form, and it avoids a real infimum over an empty set.
• The infimum over $\{\beta:\mathcal M(\beta)\le s\}$ is written as "for every such $\beta$". This is equivalent, because the set contains $\beta=0$ and the bracket is nonnegative.
• Correction/strengthening. The printed theorem has an unspecified $C(\varepsilon)>0$. The goal instead uses the value $C(\varepsilon)=4(2+\varepsilon)^2/(\varepsilon(1+\varepsilon))$ that the proof yields with $b=1+2/\varepsilon$, and this implies the printed statement. Corollary 6.2 uses the same explicit constant.
• The standing assumptions of Section 2 ($M\ge2$ and every $\|f_j\|_n\neq0$) are hypotheses of every theorem.
• Some formalizations would make the result trivial, and they are excluded here. The noise must be exactly i.i.d. $\mathcal N(0,\sigma^2)$ with $\sigma>0$ and must enter only through $y=f+W$. The target $f$ must not be restricted to $X\beta^*$. The event must be measurable. The constant must depend on $\varepsilon$ alone.
• A single definition file provides the empirical norms, $f_{\max}$, $f_{\min}$, support and sparsity, the weighted Lasso, RE and its single-set version (the family $\Lambda_{s,\gamma,c_0}$ of Corollary 6.2), the Gaussian noise model and the event $\mathcal A$. The same objects appear in the other missions of this series. Gaussian-tail and union-bound lemmas proved along the way are reusable, and contributions of such lemmas are welcome.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. Cited version: arXiv:0801.1095v3; DOI 10.1214/08-AOS620.
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 169–194, 2007. DOI 10.1214/07-EJS008.
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Aggregation for Gaussian regression, Ann. Statist. 35(4), 1674–1697, 2007. DOI 10.1214/009053606000001587.
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. DOI 10.1111/j.2517-6161.1996.tb02080.x.