Lemma 1.2: $\theta_{S,S'} \le \delta_{S+S'} \le \theta_{S,S'} + \max(\delta_S, \delta_{S'})$

Read-back of theta_le_delta_le_theta_add_max

Binders and hypotheses. Fix natural numbers $p$ and $m$ (implicit; a priori unrestricted, so $p = 0$ is allowed), a real $p \times m$ matrix $F = (F_{ij})$ with rows indexed by $\{0,\dots,p-1\}$ and columns by $\{0,\dots,m-1\}$, and natural numbers $S, S'$. Three hypotheses are assumed:

$$1 \le S, \qquad 1 \le S', \qquad S + S' \le m .$$

Consequently $m \ge 2$. No other assumption is made: $F$ is an arbitrary real matrix (no normalization of columns, no rank or size condition), and nothing further constrains $p$, $S$, $S'$.

Notation unfolded from the bundle's definitions.

• For $c \in \mathbb{R}^m$ and $T \subseteq \{0,\dots,m-1\}$, "$c$ is supported on $T$" means $c_j = 0$ for every $j \notin T$. It does not require $c_j \neq 0$ for $j \in T$: the zero vector is supported on every $T$ (including $T = \varnothing$), and it is the only vector supported on $\varnothing$.
• $\|x\|_2 := \sqrt{\sum_i x_i^2}$ for a real vector $x$ (in $\mathbb{R}^m$ or $\mathbb{R}^p$); the radicand is always $\ge 0$, so this is the ordinary square root and $\|x\|_2^2 = \sum_i x_i^2$. When $p = 0$, the unique vector of $\mathbb{R}^0$ has $\|\cdot\|_2 = 0$.
• $Fc \in \mathbb{R}^p$ is the usual product, $(Fc)_i = \sum_{j=0}^{m-1} F_{ij}\,c_j$, and $\langle u, v\rangle := \sum_{i=0}^{p-1} u_i v_i$ is the standard dot product on $\mathbb{R}^p$.
• $|T|$ is the number of elements of $T$; "$T$ and $T'$ are disjoint" means $T \cap T' = \varnothing$.

Restricted isometry constant $\delta_k(F)$. For a natural number $k$, let $\Delta_k(F)$ be the set of real numbers $\delta$ such that

• $\delta \ge 0$, and
• for every subset $T \subseteq \{0,\dots,m-1\}$ with $|T| \le k$ and every $c \in \mathbb{R}^m$ supported on $T$,

$$(1-\delta)\,\|c\|_2^2 \;\le\; \|Fc\|_2^2 \qquad\text{and}\qquad \|Fc\|_2^2 \;\le\; (1+\delta)\,\|c\|_2^2 .$$

Then $\delta_k(F) := \inf \Delta_k(F)$. Inside this definition $T$ ranges over all subsets of size at most $k$, including $T = \varnothing$, and $c$ over all vectors vanishing off $T$, including $c = 0$ (for which both inequalities read $0 \le 0$). Nothing relates $k$ to $m$ here: if $k \ge m$, every $T$ qualifies and the constraint runs over all of $\mathbb{R}^m$.

Restricted orthogonality constant $\theta_{k,k'}(F)$. For natural numbers $k, k'$, let $\Theta_{k,k'}(F)$ be the set of real numbers $\theta$ such that

• $\theta \ge 0$, and
• for all subsets $T, T' \subseteq \{0,\dots,m-1\}$ with $T \cap T' = \varnothing$, $|T| \le k$, $|T'| \le k'$, and all $c, c' \in \mathbb{R}^m$ with $c$ supported on $T$ and $c'$ supported on $T'$,

$$\bigl|\langle Fc,\, Fc'\rangle\bigr| \;\le\; \theta\,\|c\|_2\,\|c'\|_2 .$$

Then $\theta_{k,k'}(F) := \inf \Theta_{k,k'}(F)$. Either of $T, T'$ may be empty, and $c$ or $c'$ may be zero.

Meaning of $\inf$. Both infima are Mathlib's infimum of a set of real numbers, which carries a convention: if the set is empty, or is nonempty but not bounded below, the value is $0$; otherwise it is the greatest lower bound of the set. Every member of $\Delta_k(F)$ and of $\Theta_{k,k'}(F)$ is $\ge 0$ by the first clause, so both sets are bounded below by $0$, and the fallback $0$ could only arise from emptiness. (For a fixed finite real matrix every sufficiently large real belongs to each set — e.g. any $\delta \ge \max\{1, \|F\|_{\mathrm{op}}^2 - 1\}$ lies in $\Delta_k(F)$ and any $\theta \ge \|F\|_{\mathrm{op}}^2$ lies in $\Theta_{k,k'}(F)$ by Cauchy–Schwarz — so the sets are nonempty and each constant is a genuine greatest lower bound.)

The assertion. Under the hypotheses $1 \le S$, $1 \le S'$, $S + S' \le m$, both of the following non-strict inequalities hold (the statement is their conjunction):

$$\theta_{S,S'}(F) \;\le\; \delta_{S+S'}(F)$$

and

$$\delta_{S+S'}(F) \;\le\; \theta_{S,S'}(F) \;+\; \max\bigl\{\delta_S(F),\; \delta_{S'}(F)\bigr\}.$$

Here $S + S'$ is the ordinary sum of natural numbers and $\max$ is the maximum of two real numbers.

Edge cases made explicit.

• $p = 0$ is permitted: $\mathbb{R}^p$ is the zero space, $Fc$ is the empty vector, so $\|Fc\|_2 = 0$ and $\langle Fc, Fc'\rangle = 0$ for all $c, c'$, and the constants are whatever the definitions above give from those values.
• The hypotheses force $m \ge S + S' \ge 2$, so $m \in \{0, 1\}$ is excluded, and $S, S' \le m-1$. The case $S + S' = m$ is included; there $\delta_{S+S'}(F)$ quantifies over every subset $T$ of $\{0,\dots,m-1\}$, i.e. over all $c \in \mathbb{R}^m$.
• The hypotheses are jointly satisfiable (e.g. $S = S' = 1$, $m = 2$), so the statement is not vacuous.
• All inequalities in the statement and in the defining sets are non-strict ($\le$), and all sets $T$ include the empty set and all vectors include $0$.
• The bundle's other definitions ($\ell^1$ norm, columns, column span) do not occur in this statement.