Lemma 1.3: an $S$-sparse representation is unique when $\delta_{2S} < 1$

Read-back of sparse_representation_unique

Data and notation. Fix natural numbers $p$ and $m$ (both are arbitrary a priori, including $0$; see the edge cases below), a real $p \times m$ matrix $F = (F_{ij})_{i \in [p],\, j \in [m]}$, where $[k]$ denotes the index set $\{0, 1, \dots, k-1\}$, and a natural number $S$. Vectors indexed by $[m]$ are written $c = (c_j)_{j \in [m]} \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$. Throughout, $\|x\| := \sqrt{\sum_i x_i^2}$ is the Euclidean norm of a real vector (the square root is applied to a non-negative number, so no convention for negative arguments is involved), so that $\|x\|^2 = \sum_i x_i^2$.

Custom notions, unfolded.

• "$c$ is supported on $T$", for $c \in \mathbb{R}^m$ and a finite set $T \subseteq [m]$, means: for every index $j \in [m]$ with $j \notin T$, one has $c_j = 0$. Equivalently, $\operatorname{supp}(c) \subseteq T$. It does not require $c_j \neq 0$ for $j \in T$; in particular the zero vector is supported on every $T$, including $T = \emptyset$, and the only vector supported on $\emptyset$ is $0$.

• The restricted isometry constant of order $k$ of $F$, written here $\delta_k(F)$, is the real number

All inequalities are non-strict. The quantification runs over every subset $T$ of $[m]$ of cardinality at most $k$ (including $T = \emptyset$ and all sizes strictly below $k$) and over every real vector supported on $T$ (including $c = 0$, for which both inequalities read $0 \le 0$).

The infimum is Mathlib's infimum on $\mathbb{R}$, which carries the convention that the infimum of the empty set, or of a set that is not bounded below, is $0$. For this particular set: it is bounded below by $0$ by construction (every member satisfies $\delta \ge 0$), and it contains every sufficiently large $\delta$ (for $\delta \ge 1$ the left inequality holds automatically because its left-hand side is $\le 0 \le \|Fc\|^2$, and for $\delta \ge \sum_{i,j} F_{ij}^2$ the right inequality holds for all $c$ by Cauchy–Schwarz), so it is non-empty. Hence the $0$-convention is not triggered and $\delta_k(F)$ is the genuine infimum, a real number $\ge 0$. Moreover, since all the defining inequalities are non-strict, the set is closed in $\mathbb{R}$, so the infimum is attained; consequently the condition "$\delta_k(F) < 1$" says exactly that there is some $\delta \in [0,1)$ such that $(1-\delta)\|c\|^2 \le \|Fc\|^2 \le (1+\delta)\|c\|^2$ for all $T$ with $|T| \le k$ and all $c$ supported on $T$.

(The preamble also defines an $\ell^1$ norm, the columns and column span of $F$, and a restricted orthogonality constant; none of these occur in this theorem.)

The statement. For every $p, m, F, S$ as above, assume:

1. $1 \le S$;
2. $2S \le m$;
3. $\delta_{2S}(F) < 1$: the restricted isometry constant of $F$ of order $2S$, as unfolded above, is strictly less than $1$;
4. $T, T' \subseteq [m]$ are finite index sets with $|T| \le S$ and $|T'| \le S$ (no other relation between $T$ and $T'$ is assumed: they may overlap, coincide, be disjoint, or be empty);
5. $c, c' \in \mathbb{R}^m$ with $c$ supported on $T$ and $c'$ supported on $T'$, i.e. $c_j = 0$ for all $j \notin T$ and $c'_j = 0$ for all $j \notin T'$;
6. $Fc = Fc'$ as vectors in $\mathbb{R}^p$, i.e. $\sum_{j} F_{ij}\, c_j = \sum_{j} F_{ij}\, c'_j$ for every $i \in [p]$.

Then $c = c'$, i.e. $c_j = c'_j$ for every $j \in [m]$.

In compact form: for every real $p \times m$ matrix $F$ and every natural number $S$ with $1 \le S$, $2S \le m$ and $\delta_{2S}(F) < 1$,

Edge cases and what the quantifiers silently include.

• $p = 0$: then $\mathbb{R}^p$ has a single element, $Fc$ is the empty vector and $\|Fc\|^2 = 0$ for every $c$. Because hypotheses 1–2 give $m \ge 2S \ge 2$, the index $0$ exists; taking $T = \{0\}$ and $c = e_0$ (the vector with $c_0 = 1$ and all other entries $0$) in the definition of $\delta_{2S}(F)$ forces $1 - \delta \le 0$, so the defining set is exactly $[1, \infty)$ and $\delta_{2S}(F) = 1$. Hypothesis 3 then fails, and the statement holds vacuously for $p = 0$.
• $m \in \{0, 1\}$ and $S = 0$ are excluded by hypotheses 1–2 (together they give $m \ge 2$). Otherwise $m$ and $p$ are unrestricted; in particular $p$ may be smaller than, equal to, or larger than $m$.
• The conclusion is demanded in particular when $T = T'$, when $c = c' = 0$, and when exactly one of $c, c'$ is the zero vector; hypothesis 5 never forces any entry to be non-zero.
• Hypothesis 3 concerns supports of cardinality up to $2S$, whereas $T$ and $T'$ in hypothesis 4 each have cardinality at most $S$. The theorem asserts nothing about pairs of vectors whose supports have more than $S$ elements, and nothing about matrices with $\delta_{2S}(F) \ge 1$.
• $S$ and the cardinality bounds are natural numbers; $2S$ is the natural number $S + S$, with no truncation or rounding involved.