Restricted isometry constants $\delta_S$ and restricted orthogonality constants $\theta_{S,S'}$ (Definition 1.1)

column — Let $p$ and $m$ be natural numbers (implicit parameters; either may be $0$), let $F$ be a real matrix with $p$ rows and $m$ columns, rows indexed by $[p] = \{0,1,\dots,p-1\}$ and columns by $[m] = \{0,1,\dots,m-1\}$, and let $j \in [m]$ be a column index. Then $\operatorname{column}(F, j)$ is the vector in $\mathbb{R}^p$ (a function $[p] \to \mathbb{R}$) whose $i$-th entry is the $(i,j)$ entry of $F$:

That is, it is the $j$-th column of $F$ regarded as a vector. No hypothesis is placed on $F$. If $p = 0$ the result is the unique (empty) vector of $\mathbb{R}^0$; if $m = 0$ there is no admissible index $j$, so the definition has no instances at all.

columnSpan — Let $p, m$ be natural numbers (implicit; either may be $0$) and $F$ a real $p \times m$ matrix indexed as above. Then $\operatorname{columnSpan}(F)$ is the $\mathbb{R}$-linear subspace of $\mathbb{R}^p$ (with the usual entrywise addition and scalar multiplication) spanned by the columns of $F$:

Here the span is the smallest linear subspace containing the listed vectors, equivalently the set of all real linear combinations $\sum_{j \in [m]} a_j\,\operatorname{column}(F,j)$ with $a_j \in \mathbb{R}$; the result is a subspace object (a submodule of $\mathbb{R}^p$ over $\mathbb{R}$), not merely a set of vectors. When $m = 0$ the spanning set is empty and the result is the zero subspace $\{0\}$; when $p = 0$ the ambient space $\mathbb{R}^0$ is itself $\{0\}$.

restrictedIsometryConst — Let $p, m$ be natural numbers (implicit; either may be $0$), $F$ a real $p \times m$ matrix, and $S$ a natural number (possibly $0$; possibly larger than $m$). Notation: for $x \in \mathbb{R}^n$ write $\|x\|_2 = \sqrt{\sum_{i} x_i^2}$ (the earlier file's $\ell^2$ norm; the radicand is nonnegative, so $\|x\|_2^2 = \sum_i x_i^2$ exactly); for $c \in \mathbb{R}^m$ write $Fc \in \mathbb{R}^p$ for the matrix–vector product $(Fc)_i = \sum_{j \in [m]} F_{ij}\,c_j$; and say that $c \in \mathbb{R}^m$ is supported on $T \subseteq [m]$ when $c_j = 0$ for every $j \notin T$ (the earlier file's "SupportedOn"; $c$ may also vanish at some or all indices of $T$, and $c = 0$ is supported on every $T$, including $T = \emptyset$). Define

Then

Both inequalities are non-strict; $T$ ranges over all subsets of $[m]$ of cardinality at most $S$ (not exactly $S$), including $T = \emptyset$; and $\delta$ has no upper bound, so $\delta \ge 1$ is allowed (for such $\delta$ the first inequality holds automatically, its left side being $\le 0$). The set $\Delta_S(F)$ is bounded below by $0$ and is upward closed: if $\delta \in \Delta_S(F)$ and $\delta' \ge \delta$ then $\delta' \in \Delta_S(F)$, because $\|c\|_2^2 \ge 0$. About the infimum: Mathlib's infimum of a set of reals returns $0$ whenever the set is empty or not bounded below. $\Delta_S(F)$ is always bounded below, so the value is the genuine greatest lower bound of $\Delta_S(F)$ when this set is nonempty, and $0$ by convention when it is empty; in fact for any real $p \times m$ matrix every sufficiently large $\delta$ (e.g. any $\delta \ge \max(1, \|F\|_{\mathrm{op}}^2 - 1)$) belongs to $\Delta_S(F)$, so the set is nonempty. Nothing in the definition requires the infimum to be attained, nor requires the value to be $< 1$. Degenerate cases: if $S = 0$ the only admissible $T$ is $\emptyset$, so $c$ must be $0$ and both inequalities read $0 \le 0$, giving $\Delta_0(F) = [0,\infty)$ and value $0$; the same happens when $m = 0$; if $p = 0$ then $Fc$ is the empty vector and $\|Fc\|_2^2 = 0$ for every $c$, so the first inequality forces $\delta \ge 1$ as soon as $m \ge 1$ and $S \ge 1$, and the value is then exactly $1$.

restrictedOrthogonalityConst — Let $p, m$ be natural numbers (implicit; either may be $0$), $F$ a real $p \times m$ matrix, and $S, S'$ natural numbers (each possibly $0$; no relation among $S$, $S'$ and $m$ is required). With $\|\cdot\|_2$, $Fc$ and "supported on" as in the previous paragraph, and with $\langle x, y\rangle = \sum_{i \in [p]} x_i\,y_i$ the standard dot product on $\mathbb{R}^p$, define

Then

The right-hand side of the constraint uses the norms themselves, not their squares; the inequality is non-strict; $|\cdot|$ is the ordinary absolute value on $\mathbb{R}$; the pair $(T,T')$ is ordered, with the bound $S$ attached to $T$ and $S'$ to $T'$; $T$ and $T'$ may have fewer than $S$, resp. $S'$, elements, including being empty; and $\theta$ has no upper bound. The set $\Theta_{S,S'}(F)$ is bounded below by $0$ and upward closed (if $\theta$ satisfies the constraint so does every $\theta' \ge \theta$, since $\|c\|_2\|c'\|_2 \ge 0$). About the infimum: Mathlib's infimum of a set of reals returns $0$ whenever the set is empty or not bounded below; $\Theta_{S,S'}(F)$ is always bounded below, so the value is its genuine greatest lower bound when it is nonempty and $0$ by convention when it is empty; in fact for any real $p \times m$ matrix every $\theta \ge \|F\|_{\mathrm{op}}^2$ satisfies the constraint (by the Cauchy–Schwarz inequality), so the set is nonempty. Whenever $c = 0$ or $c' = 0$ both sides of the constraint are $0$, so only pairs of nonzero vectors with disjoint supports of the stated sizes actually restrict $\theta$. Degenerate cases: if $S = 0$ or $S' = 0$, one of $T, T'$ must be $\emptyset$, forcing $c = 0$ or $c' = 0$, so $\Theta_{S,S'}(F) = [0,\infty)$ and the value is $0$; the same holds when $m = 0$ (no nonzero vectors exist), when $m = 1$ (two disjoint subsets of a one-element set cannot both be nonempty), and when $p = 0$ (every dot product $\langle Fc, Fc'\rangle$ is an empty sum, i.e. $0$).