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.

The coordinate-tail and sparse-vector formulations of best s-term error agree

Statement

Let $n, s \in N$ with $n \geq 1$ and $1 \leq s \leq n$ , and let $x \in R^{n}$ use the one-based labels $[n] = {1, \dots, n}$ , with label $j$ corresponding to library coordinate $j - 1$ . For $T \subseteq [n]$ , $x_{T^{c}}$ agrees with $x$ off $T$ and is zero on $T$ . Define $σ_{s} (x)_{1} : = \min {∥ x_{T^{c}} ∥_{1} : T \subseteq [n], ∣ T ∣ \leq s}$ . Define $supp (z) : = {j \in [n] : z_{j} \neq 0}$ using the one-based labels $[n] = {1, \dots, n}$ , with label $j$ corresponding to library coordinate $j - 1$ . Then $σ_{s} (x)_{1} = \min {∥ x - z ∥_{1} : z \in R^{n}, ∣ supp (z) ∣ \leq s},$ and this sparse-vector minimum is attained.

Statement references

Finite minimum of coordinate-tail errors

Finite-dimensional one-norm

Termwise monotonicity of finite sums

Foucart and Rauhut, A Mathematical Introduction to Compressive Sensing, §2.1 Definition 2.2, printed p. 42

Mendelson, Rauhut, and Ward, Improved Bounds for Sparse Recovery from Subsampled Random Convolutions, §2.1, printed p. 5

Facts & Assumptions

Given: A vector $x \in R^{n}$ , positive integers $n, s$ with $1 \leq s \leq n$ , and the coordinate-tail quantity $σ_{s} (x)_{1}$ .

[F1]

Best s-term ℓ1 approximation error: $σ_{s} (x)_{1} = \min {∥ x_{T^{c}} ∥_{1} : T \subseteq [n], ∣ T ∣ \leq s}$ , and the finite nonempty indexing family has a minimizing member.

[F2]

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

[F3]

Laws of finite sums and finite products, clause 4: finite sums preserve termwise inequalities, and a finite sum of nonnegative terms is nonnegative.

Proof

1.1givenF1F2F3algebra

Let $z$ be any vector with $∣ supp (z) ∣ \leq s$ , and put $T = supp (z)$ . For every $j \in T^{c}$ , $z_{j} = 0$ , so $∣ x_{j} - z_{j} ∣ = ∣ (x_{T^{c}})_{j} ∣$ . For every $j \in T$ , $∣ (x_{T^{c}})_{j} ∣ = 0 \leq ∣ x_{j} - z_{j} ∣$ . Thus [F2,F3], applied in the original coordinate order, give $∥ x - z ∥_{1} = \sum_{j = 1}^{n} ∣ x_{j} - z_{j} ∣ \geq \sum_{j = 1}^{n} ∣ (x_{T^{c}})_{j} ∣ = ∥ x_{T^{c}} ∥_{1} \geq σ_{s} (x)_{1}$ , where the final inequality follows from [F1] because $∣ T ∣ \leq s$ . Thus every admissible sparse vector has error at least $σ_{s} (x)_{1}$ .

2.1givenF1F2step 1.1choosealgebra∎

By [F1], choose a minimizing set $T_{0} \subseteq [n]$ with $∣ T_{0} ∣ \leq s$ . Define $z_{0} = (x_{T_{0}})$ , equal to $x$ on $T_{0}$ and zero on $T_{0}^{c}$ . Define $z_{0}$ coordinatewise by $(z_{0})_{j} = x_{j}$ for $j \in T_{0}$ and $(z_{0})_{j} = 0$ otherwise. Then $supp (z_{0}) \subseteq T_{0}$ , so it is admissible, and direct coordinate summation gives $∥ x - z_{0} ∥_{1} = ∥ x_{T_{0}^{c}} ∥_{1} = σ_{s} (x)_{1} .$ Together with step 1.1 this proves equality and attainment. The proof chooses one witness from a finite nonempty set and uses no choice axiom.

Depends on

Used by

Robust nullspace property gives stable noisy recovery Theorem

Dependency tree · two levels

37 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, §2.1 Definition 2.2 (standard reference, not scraped)
Shahar Mendelson, Holger Rauhut, and Rachel Ward, Improved Bounds for Sparse Recovery from Subsampled Random Convolutions, §2.1 (standard reference, not scraped)