Lemma 2.2: dual sparse reconstruction property, $\ell^\infty$ version

Read-back of dual_reconstruction_linf

Objects and notation. Throughout, $p$ and $m$ are natural numbers (the binders allow either to be $0$), $F$ is a real $p \times m$ matrix with rows indexed by $\{0,\dots,p-1\}$ and columns by $\{0,\dots,m-1\}$, and $S$ is a natural number. For a vector $x \in \mathbb{R}^n$ write

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

where $\sqrt{\cdot}$ is Mathlib's real square root (it returns $0$ on negative inputs, which cannot occur here because the argument is a sum of squares); so $\|\cdot\|_2$ is the ordinary Euclidean norm, and $\|x\|_2^2 = \sum_i x_i^2$. For $j \in \{0,\dots,m-1\}$, $F_{\cdot j} \in \mathbb{R}^p$ denotes the $j$-th column of $F$, i.e. $(F_{\cdot j})_i = F_{ij}$. For $u, v \in \mathbb{R}^p$, $\langle u, v\rangle = \sum_i u_i v_i$ is the standard dot product; in particular $\langle w, F_{\cdot j}\rangle = \sum_i w_i F_{ij} = (F^{\mathsf T} w)_j$. $Fc$ is the usual matrix–vector product, $(Fc)_i = \sum_j F_{ij} c_j$. A vector $c \in \mathbb{R}^m$ is said to be supported on a finite set $T \subseteq \{0,\dots,m-1\}$ if

$$c_j = 0 \quad \text{for every } j \notin T;$$

nothing is required of $c_j$ for $j \in T$ (so $c = 0$ is supported on every $T$, and $c$ may vanish on part of $T$). The column span of $F$ is the $\mathbb{R}$-linear span of the set of columns $\{F_{\cdot j} : 0 \le j < m\}$, a linear subspace of $\mathbb{R}^p$ (equivalently, $\{Fv : v \in \mathbb{R}^m\}$).

The restricted isometry constant. For a natural number $S$,

$$\delta_S := \inf\Big\{\delta \in \mathbb{R} \;:\; \delta \ge 0 \ \text{ and }\ \forall\, T \subseteq \{0,\dots,m-1\} \text{ with } |T| \le S,\ \forall\, c \in \mathbb{R}^m \text{ supported on } T:\ (1-\delta)\,\|c\|_2^2 \le \|Fc\|_2^2 \ \text{ and }\ \|Fc\|_2^2 \le (1+\delta)\,\|c\|_2^2 \Big\}.$$

Here $T$ ranges over all subsets of size at most $S$ (including $\varnothing$), and $c$ over all vectors supported on $T$ (including $c = 0$).

The restricted orthogonality constant. For natural numbers $S, S'$,

$$\theta_{S,S'} := \inf\Big\{\theta \in \mathbb{R} \;:\; \theta \ge 0 \ \text{ and }\ \forall\, T, T' \subseteq \{0,\dots,m-1\} \text{ with } T \cap T' = \varnothing,\ |T| \le S,\ |T'| \le S',\ \forall\, c, c' \in \mathbb{R}^m \text{ with } c \text{ supported on } T \text{ and } c' \text{ supported on } T':\ \big|\langle Fc,\, Fc'\rangle\big| \le \theta\,\|c\|_2\,\|c'\|_2 \Big\}.$$

Infimum convention. Both infima are Mathlib's $\inf$ on $\mathbb{R}$, which by convention returns $0$ for the empty set and $0$ for a set that has no lower bound. Each of the two sets above is bounded below by $0$ by construction, and each is nonempty for every finite matrix $F$ (every sufficiently large $\delta$, resp. $\theta$, belongs; e.g. $\delta = \theta = \max\big(1, \sum_{i,j} F_{ij}^2\big)$ works by Cauchy–Schwarz). So in both cases the infimum is the ordinary greatest lower bound, and $\delta_S \ge 0$, $\theta_{S,S'} \ge 0$.

Hypotheses. The theorem assumes:

1. $p, m \in \mathbb{N}$, $F \in \mathbb{R}^{p \times m}$, $S \in \mathbb{N}$ as above;
2. $1 \le S$;
3. $3S \le m$ (hence $m \ge 3$; no condition at all is placed on $p$);
4. $\delta_S + \theta_{S,\,2S} < 1$ (strict);
5. a finite set $T \subseteq \{0,\dots,m-1\}$ with $|T| \le S$;
6. a vector $c \in \mathbb{R}^m$ supported on $T$, i.e. $c_j = 0$ for all $j \notin T$.

Conclusion. There exists (at least one; uniqueness is not asserted) a vector $w \in \mathbb{R}^p$ such that all three of the following hold simultaneously:

(a) $w$ lies in the column span of $F$;

(b) for every $j \in T$:

$$\langle w, F_{\cdot j}\rangle = c_j;$$

(c) for every index $j \in \{0,\dots,m-1\}$ with $j \notin T$:

$$\big|\langle w, F_{\cdot j}\rangle\big| \;\le\; \frac{\theta_{S,S}}{\big(1 - \delta_S - \theta_{S,\,2S}\big)\,\sqrt{S}}\;\|c\|_2 .$$

The right-hand side of (c) is parsed as $\Big(\theta_{S,S} \big/ \big((1-\delta_S-\theta_{S,2S})\cdot\sqrt{S}\big)\Big)\cdot \|c\|_2$, with $1 - \delta_S - \theta_{S,2S}$ meaning $(1-\delta_S)-\theta_{S,2S}$. The numerator is the orthogonality constant with parameters $(S, S)$, whereas hypothesis 4 involves the one with parameters $(S, 2S)$. $\sqrt{S}$ is the real square root of the natural number $S$ regarded as a real number; since $S \ge 1$ this is the ordinary positive root and $\sqrt{S} \ge 1$.

Edge cases and conventions.

• Division. In Lean, $x/0 = 0$ for real $x$. Under hypothesis 4, $1 - \delta_S - \theta_{S,2S} > 0$, and $\sqrt{S} \ge 1 > 0$, so the denominator in (c) is strictly positive and the division-by-zero convention is not triggered; the fraction is the ordinary real quotient.
• $T = \varnothing$ is allowed by hypothesis 5; then $c = 0$, condition (b) is vacuous, and (c) demands $|\langle w, F_{\cdot j}\rangle| \le 0$ for every $j$. More generally $c = 0$ is allowed with any $T$, and $c$ need not be nonzero on all of $T$.
• $p = 0$ is allowed by the binders. Then $\mathbb{R}^p$ is the zero space and $Fc = 0$ for every $c$; since $m \ge 3$ and $S \ge 1$, there is a nonzero $c$ supported on a singleton, so every admissible $\delta$ in the definition of $\delta_S$ must satisfy $(1-\delta)\|c\|_2^2 \le 0$, i.e. $\delta \ge 1$. Hence $\delta_S \ge 1$, and as $\theta_{S,2S} \ge 0$, hypothesis 4 cannot hold: for $p = 0$ the statement is vacuously true.
• All cardinality conditions ($|T| \le S$ in hypothesis 5 and inside $\delta_S$, $\theta_{S,S'}$) are non-strict, and the final bound (c) is a non-strict inequality $\le$.
• No hypothesis constrains the rank of $F$, the size of $T$ beyond $|T| \le S$, or the relation between $p$ and $m$ or $S$ beyond $3S \le m$.