Lemma 2.1: dual sparse reconstruction property, $\ell^2$ version

Read-back of dual_reconstruction_l2

Standing notation. Throughout, $p, m$ are natural numbers (any values, including $0$); $F \in \mathbb{R}^{p \times m}$ is a real matrix whose rows are indexed by a set $[p]$ of $p$ labels and whose columns are indexed by a set $[m]$ of $m$ labels; $F_j \in \mathbb{R}^p$ is the $j$-th column of $F$, so $(F_j)_i = F_{ij}$; $Fc \in \mathbb{R}^p$ is the matrix–vector product $(Fc)_i = \sum_{j \in [m]} F_{ij} c_j$; $\langle u, v\rangle = \sum_i u_i v_i$ is the ordinary dot product; and

$$\|x\|_2 = \sqrt{\textstyle\sum_i x_i^2}$$

is the Euclidean norm (the square root is applied to a non-negative number, so it is the usual one; Mathlib's real square root would return $0$ on a negative input, which cannot happen here). For a finite set $T \subseteq [m]$ and $c \in \mathbb{R}^m$, "$c$ is supported on $T$" means $c_j = 0$ for every $j \notin T$; nothing is required of $c$ on $T$, so $c$ may also vanish on part or all of $T$.

Definitions used, unfolded.

Restricted isometry constant. For $S \in \mathbb{N}$,

$$\delta_S(F) := \inf\Big\{\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 \le (1+\delta)\|c\|_2^2 \Big\}.$$

Restricted orthogonality constant. For $S, S' \in \mathbb{N}$,

$$\theta_{S,S'}(F) := \inf\Big\{\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,\ c' \text{ supported on } T',\ \ |\langle Fc, Fc'\rangle| \le \theta\,\|c\|_2\,\|c'\|_2 \Big\}.$$

In both definitions the sets $T, T'$ range over all subsets of the stated sizes, including the empty set and sets strictly smaller than $S$ or $S'$, and the first size parameter of $\theta_{S,S'}$ goes with $T$, the second with $T'$.

About the infima. Mathlib's infimum of a set of real numbers returns $0$ when the set is empty or has no lower bound. Neither situation occurs here: both sets are contained in $[0,\infty)$, and both contain every sufficiently large real number (by Cauchy–Schwarz, every $\delta \ge \max\big(1, \sum_{i,j} F_{ij}^2\big)$ lies in the first set and every $\theta \ge \sum_{i,j} F_{ij}^2$ lies in the second). So $\delta_S(F)$ and $\theta_{S,S'}(F)$ are genuine infima and are $\ge 0$. Moreover each set is upward closed and defined by non-strict inequalities, hence is a closed ray $[\delta^{*}, \infty)$; the infimum is therefore attained, i.e. $\delta_S(F)$ itself satisfies the two-sided inequality for every admissible $(T, c)$, and $\theta_{S,S'}(F)$ itself satisfies the orthogonality inequality for every admissible $(T, T', c, c')$.

Column span. $\operatorname{col}(F) := \operatorname{span}_{\mathbb{R}}\{F_1, \dots, F_m\} \subseteq \mathbb{R}^p$, i.e. the set of vectors of the form $Fv$ with $v \in \mathbb{R}^m$.

The statement.

There exists a function $K : \mathbb{R} \to \mathbb{R}$ such that

1. $K(\delta) > 0$ for every real number $\delta$ (including $\delta < 0$ and $\delta \ge 1$, values at which $K$ is never evaluated below); and

2. for all natural numbers $p, m$, every matrix $F \in \mathbb{R}^{p \times m}$, and all natural numbers $S, S'$ satisfying

$$1 \le S, \qquad 1 \le S', \qquad S + S' \le m, \qquad \delta_S(F) < 1,$$

and for every finite set $T \subseteq [m]$ and every vector $c \in \mathbb{R}^m$ with

$$|T| \le S \qquad\text{and}\qquad c \text{ supported on } T,$$

there exists a vector $w \in \mathbb{R}^p$ for which all four of the following hold:

(a) $w \in \operatorname{col}(F)$, i.e. $w = Fv$ for some $v \in \mathbb{R}^m$;

(b) $\langle w, F_j\rangle = c_j$ for every $j \in T$;

(c) there exists a finite set $E \subseteq [m]$ such that

• $E \cap T = \varnothing$,
• $|E| \le S'$,
• for every index $j \in [m]$ with $j \notin T$ and $j \notin E$,

$$|\langle w, F_j\rangle| \;\le\; \frac{\theta_{S,S'}(F)}{\big(1-\delta_S(F)\big)\sqrt{S'}}\;\|c\|_2 ,$$

• and

$$\sqrt{\sum_{j \in E} \langle w, F_j\rangle^2} \;\le\; \frac{\theta_{S,S'}(F)}{1-\delta_S(F)}\;\|c\|_2 ;$$

(d) $\|w\|_2 \le K\big(\delta_S(F)\big)\,\|c\|_2$.

Here $\langle w, F_j\rangle = \sum_{i \in [p]} w_i F_{ij}$ is the $j$-th coordinate of $F^{\mathsf T} w$, and $\sqrt{S'}$ is the real square root of the natural number $S'$ after casting it to a real; since $S' \ge 1$, this is the ordinary positive square root and is $\ge 1$.

Order of quantifiers and dependencies. $K$ is chosen first, before $p, m, F, S, S'$: a single function must serve every dimension, every matrix and every pair $(S, S')$, and it enters the conclusion only through its value at the number $\delta_S(F)$, which under the hypotheses lies in $[0, 1)$. Nothing beyond positivity is asked of $K$: no monotonicity, continuity, or boundedness as $\delta \to 1$, and no relation to the explicit constants in (c). The vector $w$ may depend on all of $F, S, S', T, c$; the set $E$ may depend on all of these and on $w$. Only existence is asserted for $w$ and for $E$, not uniqueness.

Edge cases and conventions.

• The hypotheses $1 \le S$, $1 \le S'$, $S + S' \le m$ force $m \ge 2$; $p$ is not constrained by any explicit hypothesis. If $p = 0$ (no rows) then $\|Fc\|_2 = 0$ for every $c$, and with $m \ge 1$, $S \ge 1$ this gives $\delta_S(F) = 1$; so the hypothesis $\delta_S(F) < 1$ excludes $p = 0$, and the statement is vacuous there.
• Because $\delta_S(F) < 1$ and $\sqrt{S'} \ge 1$, the denominators $\big(1-\delta_S(F)\big)\sqrt{S'}$ and $1-\delta_S(F)$ are strictly positive, so Lean's convention $x/0 = 0$ is never triggered in the two displayed bounds. Both right-hand sides in (c) are $\ge 0$ since $\theta_{S,S'}(F) \ge 0$.
• $|T| \le S$, not $|T| = S$, and $T$ may be empty. If $T = \varnothing$, or more generally if $c = 0$, then every right-hand side in (c) and (d) equals $0$; (d) then forces $w = 0$, and $w = 0$ does satisfy (a)–(c) (e.g. with $E = \varnothing$), so in that case the conclusion holds trivially.
• $|E| \le S'$, not $|E| = S'$, and $E$ may be empty, in which case the pointwise bound in (c) applies to every $j \notin T$ and the sum over $E$ is $0$.
• Indices $j \in T$ are pinned exactly by (b). Indices $j \in E$ are exempt from the pointwise bound and are controlled only through the aggregate $\ell^2$ bound over $E$; no bound is stated for any individual $\langle w, F_j\rangle$ with $j \in E$. Indices outside $T \cup E$ get only the pointwise bound.
• The constant in (c) is $\theta_{S,S'}(F)$ with first parameter $S$ (matching $|T| \le S$) and second parameter $S'$ (matching $|E| \le S'$); no hypothesis is placed on $\theta_{S,S'}(F)$.
• No assumption on $F$ appears beyond $\delta_S(F) < 1$: no normalisation of columns, no rank condition, no relation between $p$ and $m$.