TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)verified 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.

Robust nullspace property gives stable noisy recovery

Statement

Let $m, n, s \in N$ with $m, n \geq 1$ and $1 \leq s \leq n$ . Use one-based coordinate labels $[n] = {1, \dots, n}$ , with label $j$ corresponding to library coordinate $j - 1$ , and interpret natural numbers in real scalar expressions as their canonical real images. Let $A \in R^{m \times n}$ and suppose that for some $0 < ρ < 1$ and $τ > 0$ , $∥ h_{S} ∥_{2} \leq \frac{ρ}{\sqrt{s}} ∥ h_{S^{c}} ∥_{1} + τ ∥ A h ∥_{2}$ for every $h \in R^{n}$ and every $S \subseteq [n]$ with $∣ S ∣ \leq s$ , where for any vector $v \in R^{n}$ , $v_{S}$ agrees with $v$ on $S$ and vanishes on $S^{c} = [n] ∖ S$ . Let $x^{†} \in R^{n}$ , $ϵ \geq 0$ , and $e \in R^{m}$ satisfy $y = A x^{†} + e$ and $∥ e ∥_{2} \leq ϵ$ . Define $σ_{s} (x^{†})_{1} : = \min {∥ x_{T^{c}}^{†} ∥_{1} : T \subseteq [n], ∣ T ∣ \leq s} .$ The indexing family is finite and nonempty, so this minimum is attained; it also equals the minimum of $∥ x^{†} - z ∥_{1}$ over vectors $z$ with at most $s$ nonzero coordinates. Then the basis-pursuit denoising problem $\min_{z \in R^{n}} ∥ z ∥_{1} subject to ∥ A z - y ∥_{2} \leq ϵ$ has a minimizer. Every minimizer $\hat{x}$ satisfies $∥ \hat{x} - x^{†} ∥_{2} \leq C_{1} \frac{σ_{s} (x^{†})_{1}}{\sqrt{s}} + C_{2} ϵ, ∥ \hat{x} - x^{†} ∥_{1} \leq C_{3} σ_{s} (x^{†})_{1} + C_{4} \sqrt{s} ϵ,$ where $C_{1} = \frac{2 (1 + 2 ρ)}{1 - ρ}, C_{2} = \frac{6 τ}{1 - ρ}, C_{3} = \frac{2 (1 + ρ)}{1 - ρ}, C_{4} = \frac{4 τ}{1 - ρ} .$ If the certified finite basis-pursuit denoising procedure returns success, its returned vector is a minimizer and satisfies these same bounds. Only reconstruction error is bounded; the theorem asserts neither uniqueness nor support recovery.

Statement references

Tail-ℓ1, head-ℓ2 robust nullspace property

Finite coordinate-tail definition of best s-term error

Equivalence with the sparse-vector approximation definition

Largest-coordinate attainment of the best s-term error

Block-tail estimate

BPDN minimizer existence

Capped primal-dual BPDN procedure

Exact success certificate implies optimality

Foucart and Rauhut, A Mathematical Introduction to Compressive Sensing, §4.3, Theorem 4.22, printed pp. 87–88

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

Facts & Assumptions

Given: Integers $m, n \geq 1$ , $1 \leq s \leq n$ , a real matrix $A$ satisfying the robust nullspace inequality, a truth $x^{†}$ , a radius $ϵ \geq 0$ , a perturbation $e$ with $y = A x^{†} + e$ and $∥ e ∥_{2} \leq ϵ$ , and any minimizer $\hat{x}$ of the residual-constrained $ℓ^{1}$ problem.

[F1]

The ℓ2 robust nullspace property: for every $h$ and every $S \subseteq [n]$ with $∣ S ∣ \leq s$ , $∥ h_{S} ∥_{2} \leq \frac{ρ}{\sqrt{s}} ∥ h_{S^{c}} ∥_{1} + τ ∥ A h ∥_{2}$ .

[F2]

Best s-term ℓ1 approximation error and The coordinate-tail and sparse-vector formulations of best s-term error agree: $σ_{s} (x^{†})_{1}$ is the finite coordinate-tail minimum and equals the minimum $ℓ^{1}$ error over vectors with at most $s$ nonzero coordinates.

[F3]

The largest coordinates attain the best s-term ℓ1 error: the first $s$ largest coordinates attain this minimum and maximize the retained $ℓ^{1}$ mass over all sets of size at most $s$ .

[F4]

A block-tail estimate for the largest coordinates: if $S$ is the first $s$ coordinates of $h$ ordered by decreasing absolute value with increasing-index tie breaks, then $∥ h_{S^{c}} ∥_{2} \leq ∥ h_{S} ∥_{2} + ∥ h_{S^{c}} ∥_{1} / \sqrt{s}$ .

[F5]

A feasible finite-dimensional BPDN problem attains its minimum: nonempty finite-dimensional residual balls admit a global $ℓ^{1}$ minimizer.

[F6]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ and 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: the finite-dimensional one- and two-norms obey their triangle and homogeneity laws.

[F7]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∥ v ∥_{1} \leq \sqrt{k} ∥ v ∥_{2}$ on a coordinate set of size $k$ .

[F8]

Laws of finite sums and finite products: finite sums preserve coordinatewise inequalities and split over disjoint sets.

[F9]

The canonical natural $ι (n) = n \cdot 1_{F}$ of a field: $\sqrt{s}$ means $\sqrt{s}$ in real scalar expressions.

[F10]

Canonical naturals are positive and strictly increasing: $s > 0$ , so all divisions by $\sqrt{s}$ are defined.

[F11]

Certified basis-pursuit denoising by primal-dual hybrid gradient: a returned success vector is accompanied by the exact feasibility and primal-dual certificate checks stated in the Algorithm.

[F12]

Primal and infeasibility certificates for basis pursuit denoising: those exact checks imply that the returned feasible vector is a global minimizer.

Proof

1.1givenF5F6construct

The truth $x^{†}$ is feasible because $∥ A x^{†} - y ∥_{2} = ∥ e ∥_{2} \leq ϵ$ . Thus the feasible set is nonempty, and [F5] supplies at least one minimizer. Fix any minimizer $\hat{x}$ and put $h = \hat{x} - x^{†}$ .

1.2givenF2F3F6F8constructalgebra

Order the coordinates of $x^{†}$ by decreasing magnitude, breaking ties by increasing index, and let $T$ be the first $s$ indices. By [F2,F3], $∥ x_{T^{c}}^{†} ∥_{1} = σ_{s} (x^{†})_{1} = : σ$ . Minimality of $\hat{x}$ and the triangle inequality give $∥ x_{T}^{†} + h_{T} ∥_{1} + ∥ x_{T^{c}}^{†} + h_{T^{c}} ∥_{1} \leq ∥ x_{T}^{†} ∥_{1} + ∥ x_{T^{c}}^{†} ∥_{1} .$ Applying $∥ a + b ∥_{1} \geq ∥ b ∥_{1} - ∥ a ∥_{1}$ to the two disjoint restrictions yields $∥ x_{T}^{†} ∥_{1} - ∥ h_{T} ∥_{1} + ∥ h_{T^{c}} ∥_{1} - ∥ x_{T^{c}}^{†} ∥_{1} \leq ∥ x_{T}^{†} ∥_{1} + ∥ x_{T^{c}}^{†} ∥_{1} .$ After cancellation this is $∥ h_{T^{c}} ∥_{1} - ∥ h_{T} ∥_{1} \leq 2 σ$ , hence the cone estimate $∥ h_{T^{c}} ∥_{1} \leq ∥ h_{T} ∥_{1} + 2 σ$ .

2.1givenF3F6step 1.2algebra

Independently order $h$ by decreasing magnitude with the same deterministic tie break and let $S$ be its first $s$ indices. Since $T$ has size $s$ , [F3] gives $∥ h_{T} ∥_{1} \leq ∥ h_{S} ∥_{1}$ and $∥ h_{S^{c}} ∥_{1} \leq ∥ h_{T^{c}} ∥_{1}$ . Step 1.2 therefore yields $∥ h_{S^{c}} ∥_{1} \leq ∥ h_{S} ∥_{1} + 2 σ .$ The data relation and feasibility give $A h = (A \hat{x} - y) + e$ , so the triangle inequality gives $∥ A h ∥_{2} \leq 2 ϵ$ .

3.1F1F7F9F10step 2.1algebra

Set $u = ∥ h_{S} ∥_{2} \geq 0$ . Applying [F1] to this $S$ , then using step 2.1 and Cauchy–Schwarz on its $s$ coordinates, gives $u \leq \frac{ρ}{\sqrt{s}} ∥ h_{S^{c}} ∥_{1} + τ ∥ A h ∥_{2} \leq ρ u + \frac{2 ρ σ}{\sqrt{s}} + 2 τ ϵ .$ Since $1 - ρ > 0$ , rearranging proves $u \leq \frac{2 ρ}{1 - ρ} \frac{σ}{\sqrt{s}} + \frac{2 τ}{1 - ρ} ϵ .$

4.1F4F6F7step 2.1step 3.1algebra

Apply [F4] to $h$ and its chosen largest-coordinate set $S$ . Step 2.1 and [F7] show $∥ h_{S^{c}} ∥_{2} \leq u + \frac{∥ h_{S^{c}} ∥_{1}}{\sqrt{s}} \leq u + \frac{\sqrt{s} u + 2 σ}{\sqrt{s}} = 2 u + \frac{2 σ}{\sqrt{s}} .$ By the triangle inequality on $h = h_{S} + h_{S^{c}}$ , $∥ h ∥_{2} \leq 3 u + 2 σ / \sqrt{s}$ . Substitute step 3.1 and simplify: $∥ h ∥_{2} \leq (\frac{6 ρ}{1 - ρ} + 2) \frac{σ}{\sqrt{s}} + \frac{6 τ}{1 - ρ} ϵ = \frac{2 (1 + 2 ρ)}{1 - ρ} \frac{σ}{\sqrt{s}} + \frac{6 τ}{1 - ρ} ϵ .$

4.2F7F8step 1.1step 2.1step 3.1algebra

Disjoint coordinates and step 2.1 give $∥ h ∥_{1} \leq ∥ h_{S} ∥_{1} + ∥ h_{S^{c}} ∥_{1} \leq 2 \sqrt{s} u + 2 σ$ by [F7]. Substituting step 3.1 yields $∥ h ∥_{1} \leq (\frac{4 ρ}{1 - ρ} + 2) σ + \frac{4 τ}{1 - ρ} \sqrt{s} ϵ = \frac{2 (1 + ρ)}{1 - ρ} σ + \frac{4 τ}{1 - ρ} \sqrt{s} ϵ .$ This proves both bounds for the arbitrary minimizer fixed at step 1.1.

5.1F11F12step 1.2step 2.1step 3.1step 4.1step 4.2∎

If the finite procedure returns success, [F11] gives the same exact feasibility and certificate conditions, and [F12] makes its vector a minimizer. Steps 1.2, 2.1, 3.1, 4.1, and 4.2 therefore apply to that vector as well. No step uses uniqueness or identifies a support.

Depends on

Used by

Bounded noise, compressible truth, and a large nullspace component Example

Dependency tree · two levels

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