LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedverified 2026-10-22 (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A uniform stability margin for the nullspace cone

Statement

Let $m, n, s \in N$ with $m, n \geq 1$ and $1 \leq s \leq n$ , and let $A \in R^{m \times n}$ . Use one-based coordinate labels $j = 1, \dots, n$ , with coordinate $j$ identified with the library's coordinate $j - 1$ . Assume that $\sum_{j \in S} ∣ h_{j} ∣ < \sum_{j \notin S} ∣ h_{j} ∣$ for every nonzero $h \in R^{n}$ with $A h = 0$ and every $S \subseteq {1, \dots, n}$ with $∣ S ∣ \leq s$ . Then there is a constant $ρ \in (0, 1)$ such that $\sum_{j \in S} ∣ h_{j} ∣ \leq ρ \sum_{j \notin S} ∣ h_{j} ∣$ for every $h \in R^{n}$ with $A h = 0$ and every $S \subseteq {1, \dots, n}$ with $∣ S ∣ \leq s$ . The estimate is only on the exact kernel and gives no bound for vectors with $A h \neq 0$ .

Statement references

Strict nullspace property and coordinate conventions

Finite-dimensional one-norm and Euclidean norm

The Euclidean inner product and norm

Norm properties of finite-dimensional p-norms

Continuity of finite-dimensional norms

A finite set of real numbers has a maximum

Cauchy–Schwarz for the Euclidean inner product

Heine–Borel and extreme-value theorem in finite dimensions

Foucart and Rauhut, A Mathematical Introduction to Compressive Sensing, §4.2, Definition 4.11 and Remark 4.16, pp. 82–85

Facts & Assumptions

Given: Integers $m, n \geq 1$ , $1 \leq s \leq n$ , a matrix $A \in R^{m \times n}$ satisfying the strict nullspace inequalities in the Statement, and $\ker A : = {h \in R^{n} : A h = 0}$ .

[F1]

The strict nullspace property: for every nonzero $h \in \ker A$ and every $S \subseteq [n]$ with $∣ S ∣ \leq s$ , $∥ h_{S} ∥_{1} < ∥ h_{S^{c}} ∥_{1}$ , where $h_{S}$ is zero outside $S$ .

[F2]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ : $∥ x ∥_{1} = \sum_{j = 1}^{n} ∣ x_{j} ∣$ on $R^{n}$ .

[F3]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ : $∥ x ∥_{2} = (\sum_{j = 1}^{n} x_{j}^{2})^{1 / 2}$ on $R^{n}$ .

[F4]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: for $a, u, v \in R^{n}$ , $∣ ⟨ a, u - v ⟩ ∣ \leq ∥ a ∥_{2} ∥ u - v ∥_{2}$ .

[F5]

Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page: both $∥ \cdot ∥_{1}$ and $∥ \cdot ∥_{2}$ are norms on $R^{n}$ , and $d_{2} (u, v) = ∥ u - v ∥_{2}$ for $n \geq 1$ .

[F6]

A norm on a real vector space, the induced metric, and the dictionary with the metric axioms: a norm satisfies absolute homogeneity, $N (λ v) = ∣ λ ∣ N (v)$ .

[F7]

The finite and reverse triangle inequalities for a norm; and for $n \geq 1$ every norm $N$ on $R^{n}$ satisfies $N (x) \leq C ∥ x ∥_{1}$ and is Lipschitz, hence continuous, for $d_{2}$ : every norm on $R^{n}$ is continuous for the Euclidean metric.

[F8]

For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent: closed bounded subsets of $R^{n}$ are compact, and continuous real-valued functions on nonempty compact subsets attain their maxima; this result is choice-free.

[F9]

Every nonempty finite set of reals has a maximum and a minimum: every nonempty finite set of real numbers has a maximum.

[F10]

Laws of finite sums and finite products: finite sums are monotone termwise; every nonnegative term is at most its sum, and adjoining nonnegative terms cannot decrease the sum.

[F11]

The strict nullspace property: under its coordinate relabeling, $(A u)_{i} = \sum_{j = 1}^{n} A_{i j} u_{j}$ for each row $i$ .

[F12]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : for the row vector $r_{i}$ with coordinates $(r_{i})_{j} = A_{i j}$ , $⟨ r_{i}, u ⟩ = \sum_{j = 1}^{n} A_{i j} u_{j}$ .

[F13]

Laws of finite sums and finite products: additivity and scalar multiplication of finite sums give $\sum_{j = 1}^{n} A_{i j} (u_{j} - v_{j}) = \sum_{j = 1}^{n} A_{i j} u_{j} - \sum_{j = 1}^{n} A_{i j} v_{j}$ .

[F14]

The finite and reverse triangle inequalities for a norm; and for $n \geq 1$ every norm $N$ on $R^{n}$ satisfies $N (x) \leq C ∥ x ∥_{1}$ and is Lipschitz, hence continuous, for $d_{2}$ : for every norm $N$ , $∣ N (u) - N (v) ∣ \leq N (u - v)$ .

[F15]

Squaring is monotone on the nonnegatives: for nonnegative reals $a, b$ , $a \leq b$ if and only if $a^{2} \leq b^{2}$ .

Proof

1.1givenF3F4F5F8F11F12F13F14constructchoose

If $\ker A = {0}$ , choose $ρ = 1 / 2$ . The only $h \in \ker A$ is zero, so both sides of the required inequality are zero for every $S$ . Now suppose $\ker A \neq {0}$ and define $K : = {h \in \ker A : ∥ h ∥_{2} = 1}$ . This set is nonempty by normalizing a nonzero kernel vector, since [F5] makes its norm positive. To show $K$ is closed, fix $x \notin K$ . If $A x \neq 0$ , choose a row $i$ with $c : = (A x)_{i} \neq 0$ and let $r_{i}$ be that row as a vector in $R^{n}$ . By [F11], [F12], and [F13], $f_{i} (u) : = (A u)_{i} = ⟨ r_{i}, u ⟩$ and $f_{i} (y) - f_{i} (x) = ⟨ r_{i}, y - x ⟩$ . By [F4], $∣ f_{i} (y) - c ∣ \leq ∥ r_{i} ∥_{2} ∥ y - x ∥_{2}$ . Moreover, $∥ r_{i} ∥_{2} > 0$ : otherwise [F5] gives $r_{i} = 0$ , which would imply $c = ⟨ r_{i}, x ⟩ = 0$ . Thus $δ : = ∣ c ∣ / (2 ∥ r_{i} ∥_{2}) > 0$ , and whenever $∥ y - x ∥_{2} < δ$ we have $∣ f_{i} (y) - c ∣ < ∣ c ∣ / 2$ , so $f_{i} (y) \neq 0$ and $y \notin K$ . If $A x = 0$ , then $∥ x ∥_{2} \neq 1$ ; put $δ : = ∣ ∥ x ∥_{2} - 1 ∣ / 2 > 0$ . By [F14], $∣ ∥ y ∥_{2} - ∥ x ∥_{2} ∣ \leq ∥ y - x ∥_{2}$ , so $∥ y - x ∥_{2} < δ$ precludes $∥ y ∥_{2} = 1$ and again $y \notin K$ . Hence every point outside $K$ has a ball disjoint from $K$ , so $K$ is closed. It is bounded because every $h \in K$ has $∥ h ∥_{2} = 1$ and [F5] identifies this with its Euclidean distance from $0$ . By [F8], $K$ is compact.

2.1step 1.1F1F2F3F5F7F8F10F15algebra

Fix $S \subseteq [n]$ with $∣ S ∣ \leq s$ and define $P_{S}, P_{S^{c}} : R^{n} \to R^{n}$ by $P_{S} u : = u_{S}$ and $P_{S^{c}} u : = u_{S^{c}}$ . For all $u, v \in R^{n}$ and every coordinate $j$ , $∣ (P_{S} u - P_{S} v)_{j} ∣ \leq ∣ u_{j} - v_{j} ∣$ ; both sides are nonnegative, so the forward implication in [F15] and then [F10] give $∥ P_{S} u - P_{S} v ∥_{2}^{2} \leq ∥ u - v ∥_{2}^{2}$ . Both Euclidean norms are nonnegative by [F5], so the converse implication in [F15] yields $∥ P_{S} u - P_{S} v ∥_{2} \leq ∥ u - v ∥_{2}$ . The same argument applies to $P_{S^{c}}$ , making both coordinate projections $1$ -Lipschitz, hence continuous for $d_{2}$ . Since $∥ \cdot ∥_{1}$ is a norm by [F5] and every norm on $R^{n}$ is continuous for $d_{2}$ by [F7], the compositions $a_{S} (h) : = ∥ h_{S} ∥_{1}$ and $b_{S} (h) : = ∥ h_{S^{c}} ∥_{1}$ are continuous. For each $h \in K$ , [F1] gives $a_{S} (h) < b_{S} (h)$ , hence $b_{S} (h) > 0$ . To verify continuity of $r_{S} : = a_{S} / b_{S}$ at any $h_{0} \in K$ , put $a_{0} : = a_{S} (h_{0})$ and $b_{0} : = b_{S} (h_{0}) > 0$ . Continuity of $b_{S}$ gives a neighborhood of $h_{0}$ in $K$ on which $b_{S} (h) > b_{0} / 2$ . There, $∣ r_{S} (h) - r_{S} (h_{0}) ∣ \leq \frac{2}{b_{0}} ∣ a_{S} (h) - a_{0} ∣ + \frac{2 a_{0}}{b_{0}^{2}} ∣ b_{S} (h) - b_{0} ∣,$ by splitting the difference of the two quotients. The right side tends to $0$ as $h \to h_{0}$ , since $a_{S}$ and $b_{S}$ are continuous; thus $r_{S}$ is continuous on $K$ . By [F8] it attains a maximum $q_{S}$ on $K$ , and [F1] at a maximizing point gives $0 \leq q_{S} < 1$ .

3.1step 1.1step 2.1givenF1F2F9choosealgebra

There are finitely many sets $S \subseteq [n]$ with $∣ S ∣ \leq s$ , and this family is nonempty because it contains $\emptyset$ . Therefore [F9] gives $q : = \max_{∣ S ∣ \leq s} q_{S} < 1$ . Choose any $h \in K$ and a coordinate $j$ with $h_{j} \neq 0$ ; then $S = {j}$ is admissible because $s \geq 1$ , and [F2] gives $r_{S} (h) > 0$ , so $q > 0$ . Set $ρ : = (1 + q) / 2$ ; then $q < ρ < 1$ .

4.1step 1.1step 3.1F1F2F3F5F6algebra∎

Let $h \in \ker A$ . If $h = 0$ , the required inequality is immediate. Otherwise $\tilde{h} : = h / ∥ h ∥_{2}$ belongs to $K$ . For every admissible $S$ , [F6] gives $r_{S} (h) = r_{S} (\tilde{h}) \leq q < ρ$ , so $∥ h_{S} ∥_{1} \leq ρ ∥ h_{S^{c}} ∥_{1}$ . This proves the estimate with one constant for all $S$ and all kernel vectors.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Simon Foucart and Holger Rauhut, A Mathematical Introduction to Compressive Sensing, §4.2, Definition 4.11 and Remark 4.16 (standard reference, not scraped)