Theorem 1.4: $\ell^1$ minimization recovers every $S$-sparse vector when $\delta_S + \theta_{S,S} + \theta_{S,2S} < 1$

Read-back of l1_recovers_sparse_vector

Setting and notation. Throughout, $p$ and $m$ are natural numbers (a priori either may be $0$; see the edge cases below), $[m]=\{0,1,\dots,m-1\}$ and $[p]=\{0,\dots,p-1\}$ are the index sets, and $F=(F_{ij})_{i\in[p],\,j\in[m]}$ is a real $p\times m$ matrix. For $c\in\mathbb{R}^m$, $Fc\in\mathbb{R}^p$ is the ordinary matrix–vector product $(Fc)_i=\sum_{j\in[m]}F_{ij}c_j$, and for $x,y\in\mathbb{R}^p$, $\langle x,y\rangle=\sum_{i\in[p]}x_iy_i$ is the ordinary dot product. Sets of indices $T\subseteq[m]$ are always finite, and $|T|$ is their cardinality. The following notions are the bundle's own definitions, unfolded here.

• Support. For $c\in\mathbb{R}^m$ and $T\subseteq[m]$, "$c$ is supported on $T$" means: for every $j\in[m]$ with $j\notin T$, $c_j=0$. So $\operatorname{supp}(c)\subseteq T$; $c$ may vanish on part or all of $T$, and $T=\varnothing$ forces $c=0$. A vector supported on some $T$ with $|T|\le S$ is therefore a vector with at most $S$ nonzero entries.

• $\ell^1$ norm. $\|c\|_1=\sum_{j\in[m]}|c_j|$.

• $\ell^2$ norm. $\|x\|_2=\sqrt{\sum_i x_i^2}$, using Mathlib's real square root (which returns $0$ on negative inputs; here the argument is a sum of squares, so this is the usual Euclidean norm). Hence $\|x\|_2^2=\sum_i x_i^2$. When $p=0$ the sum defining $\|Fc\|_2$ is empty, so $\|Fc\|_2=0$ for every $c$.

• Restricted isometry constant $\delta_S(F)$. For a natural number $S$,

$$\begin{aligned} \delta_S(F)=\inf\Bigl\{\,\delta\in\mathbb{R}\;:\;&\delta\ge 0,\ \text{and for every } T\subseteq[m] \text{ with } |T|\le S \text{ and every } c\in\mathbb{R}^m \text{ supported on } T,\\ &(1-\delta)\,\|c\|_2^2\;\le\;\|Fc\|_2^2 \quad\text{and}\quad \|Fc\|_2^2\;\le\;(1+\delta)\,\|c\|_2^2\,\Bigr\}. \end{aligned}$$

Here $T$ ranges over all subsets of $[m]$ of size at most $S$ (including $\varnothing$, for which only $c=0$ qualifies and both inequalities are trivial), and both inequalities are non-strict.

• Restricted orthogonality constant $\theta_{S,S'}(F)$. For natural numbers $S,S'$,

$$\begin{aligned} \theta_{S,S'}(F)=\inf\Bigl\{\,\theta\in\mathbb{R}\;:\;&\theta\ge 0,\ \text{and for all } T,T'\subseteq[m] \text{ with } T\cap T'=\varnothing,\ |T|\le S,\ |T'|\le S',\\ &\text{and all } c,c'\in\mathbb{R}^m \text{ with } c \text{ supported on } T \text{ and } c' \text{ supported on } T',\\ &\bigl|\langle Fc,\,Fc'\rangle\bigr|\;\le\;\theta\,\|c\|_2\,\|c'\|_2\,\Bigr\}. \end{aligned}$$

The bound on the right is $\theta$ times the product of the two (unsquared) Euclidean norms; $T$ and $T'$ may be empty.

• Unique $\ell^1$ minimizer. For $f\in\mathbb{R}^p$ and $c\in\mathbb{R}^m$, "$c$ is the unique $\ell^1$ minimizer for $(F,f)$" means

$$Fc=f \quad\text{and}\quad \forall d\in\mathbb{R}^m:\ \bigl(Fd=f\ \text{ and }\ d\neq c\bigr)\ \Longrightarrow\ \|c\|_1<\|d\|_1 .$$

The inequality is strict, so this says that $c$ minimizes $\|\cdot\|_1$ over the affine set $\{d\in\mathbb{R}^m : Fd=f\}$ and that no other point of that set attains the same value.

About the two infima. In Mathlib, the infimum $\inf A$ of a set $A\subseteq\mathbb{R}$ is the genuine greatest lower bound when $A$ is nonempty and bounded below, and is defined to be $0$ when $A$ is empty or not bounded below. Both defining sets above consist of nonnegative reals, so they are bounded below by $0$, and both are nonempty: by Cauchy–Schwarz, $\|Fc\|_2^2\le\bigl(\sum_{i,j}F_{ij}^2\bigr)\|c\|_2^2$ for every $c$, so $\delta=1+\sum_{i,j}F_{ij}^2$ lies in the first set and $\theta=\sum_{i,j}F_{ij}^2$ lies in the second. Consequently $\delta_S(F)$ and $\theta_{S,S'}(F)$ are honest infima and both are $\ge 0$. Each set is moreover upward closed (if $\delta$ qualifies, so does every $\delta'\ge\delta$; likewise for $\theta$) and cut out by non-strict inequalities, so each is a closed half-line and its infimum is attained: $\delta_S(F)$ is the least $\delta\ge 0$ for which the two-sided inequality holds for all vectors with at most $S$ nonzero entries, and $\theta_{S,S'}(F)$ is the least $\theta\ge0$ for which the dot-product bound holds for all disjointly supported pairs of the stated sparsities.

The statement. Let $p,m\in\mathbb{N}$, let $F$ be a real $p\times m$ matrix, and let $S\in\mathbb{N}$. Assume:

1. $1\le S$;
2. $3S\le m$ (ordinary multiplication and comparison of natural numbers);

$$\delta_S(F)\;+\;\theta_{S,S}(F)\;+\;\theta_{S,2S}(F)\;<\;1,$$

where $\theta_{S,S}$ concerns disjoint index sets of size at most $S$ each, and $\theta_{S,2S}$ concerns disjoint index sets of size at most $S$ and at most $2S$ respectively; 4. $T\subseteq[m]$ is a set of indices with $|T|\le S$; 5. $c\in\mathbb{R}^m$ is supported on $T$, i.e. $c_j=0$ for every $j\notin T$.

Then $c$ is the unique $\ell^1$ minimizer for $(F,\,Fc)$. Unfolded, and noting that the first conjunct $Fc=Fc$ holds trivially, the conclusion is exactly

$$\forall d\in\mathbb{R}^m:\qquad Fd=Fc\ \ \text{and}\ \ d\neq c\quad\Longrightarrow\quad \sum_{j\in[m]}|c_j|\;<\;\sum_{j\in[m]}|d_j| .$$

Here $Fd=Fc$ is exact equality of two vectors in $\mathbb{R}^p$, and $d$ ranges over all of $\mathbb{R}^m$ with no sparsity restriction.

Edge cases and what the quantifiers silently include.

• Hypotheses 1 and 2 together force $m\ge 3$ (so $m=0$ is excluded), $S\le m/3$, and $2S\le m-S$, so disjoint index sets of the sizes named in $\theta_{S,S}$ and $\theta_{S,2S}$ do exist inside $[m]$. Nothing is assumed about $p$ relative to $m$ or $S$.
• Since all three constants are $\ge 0$, hypothesis 3 implies that each of $\delta_S(F)$, $\theta_{S,S}(F)$, $\theta_{S,2S}(F)$ is individually $<1$.
• If some nonzero vector $c_0$ with at most $S$ nonzero entries satisfies $Fc_0=0$, then every $\delta$ in the defining set satisfies $(1-\delta)\|c_0\|_2^2\le 0$, hence $\delta\ge1$, so $\delta_S(F)\ge 1$ and hypothesis 3 cannot hold: the theorem is vacuous for such $F$. In particular this happens when $p=0$ ($F$ has no rows, $Fc=0$ for every $c$, and a nonzero $1$-sparse vector exists because $m\ge 3$ and $S\ge1$), so the hypotheses implicitly force $p\ge 1$.
• $T$ may be empty or have fewer than $S$ elements, and $c$ may vanish on some or all of $T$; in particular $c=0$ is allowed, in which case the conclusion reads "every $d\neq 0$ with $Fd=0$ has $\|d\|_1>0$", which is automatic.
• The statement concerns one fixed, deterministic matrix $F$: there is no probability, no normalization of the columns of $F$, and no relation such as $p\le m$ is imposed.
• The bundle also defines the $j$-th column of $F$ and the linear span of all columns of $F$; neither is referenced by this statement.