Pipeline-generated

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.

Stable compressed sensing with noise

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Primal and infeasibility certificates for basis pursuit denoising

Statement

Let $m, n \in N$ with $m, n \geq 1$ , let $A \in R^{m \times n}$ act by matrix multiplication in the standard finite coordinate bases, with row and column labels $1$ through their dimensions corresponding to library coordinates $0$ through one less, let $y \in R^{m}$ , and let $ϵ \geq 0$ . Define $g : R^{m} \to {0, + \infty}$ by $g (u) = 0$ when $∥ u - y ∥_{2} \leq ϵ$ and $g (u) = + \infty$ otherwise. For $p \in R^{m}$ , define $g^{*} (p) : = \sup_{u \in R^{m}} {⟨ p, u ⟩ - g (u)}$ . Then $g^{*} (p) = ⟨ p, y ⟩ + ϵ ∥ p ∥_{2} (p \in R^{m}) .$ Let $A^{*} : R^{m} \to R^{n}$ be the Euclidean adjoint, characterized by $⟨ A^{*} p, z ⟩ = ⟨ p, A z ⟩$ for all $p, z$ . If $x \in R^{n}$ satisfies $∥ A x - y ∥_{2} \leq ϵ$ and a vector $p \in R^{m}$ satisfies $∥ A^{*} p ∥_{\infty} \leq 1$ and $∥ x ∥_{1} = - ⟨ p, y ⟩ - ϵ ∥ p ∥_{2},$ then $x$ minimizes $∥ z ∥_{1}$ over that residual ball. If instead $p \neq 0$ , $A^{*} p = 0$ , and $∣ ⟨ p, y ⟩ ∣ > ϵ ∥ p ∥_{2}$ , then the residual ball is disjoint from the range of $A$ .

Statement references

Fenchel conjugate

Euclidean adjoint

Existence of the finite-dimensional adjoint

Finite-dimensional one-, two-, and maximum norms

Cauchy–Schwarz for Euclidean norms

Positive definiteness of the Euclidean norm

Chambolle and Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, §2

Foucart and Rauhut, A Mathematical Introduction to Compressive Sensing, §4.3

Facts & Assumptions

Given: Integers $m, n \geq 1$ , a real linear map $A : R^{n} \to R^{m}$ , its Euclidean adjoint $A^{*}$ , a vector $y \in R^{m}$ , a radius $ϵ \geq 0$ , and the residual ball ${u : ∥ u - y ∥_{2} \leq ϵ}$ .

[F1]

Fenchel conjugate of an extended-real function: $g^{*} (p) = \sup_{u \in R^{m}} {⟨ p, u ⟩ - g (u)}$ .

[F2]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $⟨ p, u ⟩$ is the finite Euclidean coordinate pairing and $∥ p ∥_{2}^{2} = ⟨ p, p ⟩$ .

[F3]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ : $∥ z ∥_{1} = \sum_{j = 1}^{n} ∣ z_{j} ∣$ , $∥ u ∥_{2} = (\sum_{i} ∣ u_{i} ∣^{2})^{1 / 2}$ , and $∥ v ∥_{\infty} = \max_{j} ∣ v_{j} ∣$ in positive dimensions.

[F4]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ A^{*} p, z ⟩ = ⟨ p, A z ⟩$ for every $p, z$ .

[F5]

Every linear map between finite-dimensional inner product spaces has a unique adjoint: the Euclidean adjoint $A^{*}$ exists and is unique.

[F6]

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

[F7]

Laws of finite sums and finite products: finite sums of nonnegative terms are nonnegative.

[F8]

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 Euclidean $2$ -norm is positive definite, so $∥ p ∥_{2} > 0$ whenever $p \neq 0$ .

Proof

1.1givenF1F2F3F6F8choosealgebra

In the supremum defining $g^{*} (p)$ , only $u$ in the residual ball contributes. Write $u = y + v$ with $∥ v ∥_{2} \leq ϵ$ . For $p \in R^{m}$ , define $g^{*} (p) : = \sup_{u \in R^{m}} {⟨ p, u ⟩ - g (u)}$ . Then $g^{*} (p) = ⟨ p, y ⟩ + \sup_{∥ v ∥_{2} \leq ϵ} ⟨ p, v ⟩ .$ By [F6], the last supremum is at most $ϵ ∥ p ∥_{2}$ . If $p = 0$ or $ϵ = 0$ , $v = 0$ attains this value. Otherwise $v = ϵ p / ∥ p ∥_{2}$ is feasible and gives $⟨ p, v ⟩ = ϵ ∥ p ∥_{2}$ . This proves the conjugate formula, including the zero cases.

1.2givenF3F4F5F6F7algebra

Let $z$ be any feasible vector and put $q = A^{*} p$ . The condition $∥ q ∥_{\infty} \leq 1$ means $∣ q_{j} ∣ \leq 1$ for every coordinate. Hence each term $∣ z_{j} ∣ + q_{j} z_{j}$ is nonnegative, and [F7] gives $∥ z ∥_{1} + ⟨ q, z ⟩ = \sum_{j} (∣ z_{j} ∣ + q_{j} z_{j}) \geq 0.$ By [F4], $∥ z ∥_{1} \geq - ⟨ p, A z ⟩$ . Feasibility and [F6] give $∣ ⟨ p, A z - y ⟩ ∣ \leq ϵ ∥ p ∥_{2}$ , so $∥ z ∥_{1} \geq - ⟨ p, A z ⟩ \geq - ⟨ p, y ⟩ - ϵ ∥ p ∥_{2} .$ If $x$ is feasible and attains equality with the last quantity, it has objective no larger than any feasible $z$ , proving the optimality certificate.

2.1givenF4F6F8algebra∎

If $p \neq 0$ , $A^{*} p = 0$ , and $∣ ⟨ p, y ⟩ ∣ > ϵ ∥ p ∥_{2}$ , then for every $z \in R^{n}$ , [F4] gives $∣ ⟨ p, A z - y ⟩ ∣ = ∣ ⟨ A^{*} p, z ⟩ - ⟨ p, y ⟩ ∣ = ∣ ⟨ p, y ⟩ ∣ > ϵ ∥ p ∥_{2} .$ By [F6], this forces $∥ A z - y ∥_{2} > ϵ$ . Thus no $z$ is feasible, proving the infeasibility certificate.

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

The basis-pursuit denoising objective and residual indicator are proper closed convex

Statement

Let $m, n \in N$ with $m, n \geq 1$ , let $y \in R^{m}$ , and let $ϵ \geq 0$ . Define $f : R^{n} \to R$ by $f (x) = ∥ x ∥_{1}$ , and define $g : R^{m} \to (- \infty, + \infty]$ by $g (u) = 0$ when $∥ u - y ∥_{2} \leq ϵ$ and $g (u) = + \infty$ otherwise. Then $f$ and $g$ are proper (finite somewhere), closed (their epigraphs are closed), and convex (they satisfy the extended-real convex-combination inequality) on their respective finite-dimensional Euclidean spaces.

Statement references

Finite-dimensional one- and two-norms

Euclidean comparison bound for the one-norm

Canonical natural scalar convention

Positivity of positive natural scalars

Norm and triangle properties

Properness, convexity, and closed-epigraph convention

Convex-function inequality

Convex-set convention

Extended-real indicator

Chambolle and Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, §2

Facts & Assumptions

Given: Positive integers $m, n$ , a center $y \in R^{m}$ , a radius $ϵ \geq 0$ , the functions $f (x) = ∥ x ∥_{1}$ and $g = ι_{C}$ for $C = {u : ∥ u - y ∥_{2} \leq ϵ}$ .

[F1]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , 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, and 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}$ : the one- and two-norms are finite-valued norms, satisfy homogeneity and both triangle inequalities, and $∥ x ∥_{1} \leq \sqrt{n} ∥ x ∥_{2}$ for $n \geq 1$ .

[F2]

Proper closed convex extended-real functions on $R^{n}$ : a function is proper when its finite domain is nonempty, convex under real convex combinations, and closed when its epigraph is closed.

[F3]

Convex and strictly convex functionals on a convex subset of a real vector space: for $0 \leq θ \leq 1$ , convexity is the inequality $q ((1 - θ) a + θ b) \leq (1 - θ) q (a) + θ q (b)$ , with $0 \cdot (+ \infty) = 0$ at endpoints.

[F4]

A convex subset of $R^{m}$ contains every line segment between two of its points: a set is convex when every segment between two of its points remains in it.

[F5]

Extended-real indicator of a set: $ι_{C}$ equals $0$ on $C$ and $+ \infty$ outside it.

[F6]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the Euclidean norm on a product coordinate space is the square root of the sum of squared coordinate differences.

[F7]

The canonical natural $ι (n) = n \cdot 1_{F}$ of a field: $n$ denotes the canonical real image of $n$ .

[F8]

Canonical naturals are positive and strictly increasing: $n > 0$ for $n \geq 1$ .

[F9]

Laws of finite sums and finite products and Squaring is monotone on the nonnegatives: finite sums preserve inequalities, and $a^{2} \leq b^{2}$ for nonnegative reals implies $a \leq b$ .

Proof

1.1givenF1F2F3algebra

The function $f$ is finite everywhere because it is a finite sum of absolute values, and $f (0) = 0$ , so its effective domain is nonempty. For $0 \leq θ \leq 1$ , the triangle inequality and homogeneity in [F1] give $f ((1 - θ) x + θ z) \leq f ((1 - θ) x) + f (θ z) = (1 - θ) f (x) + θ f (z) .$ Thus $f$ is proper and convex by [F2,F3].

1.2givenF1F6F7F8F9constructalgebra

For $(x, t) \in R^{n + 1}$ outside $epi f$ , the gap $d = f (x) - t$ is positive. Put $L = \sqrt{n} + 1 > 0$ . If $(x^{'}, t^{'})$ has product Euclidean distance $D < d / (2 L)$ from $(x, t)$ , then coordinate-square domination gives $∥ x^{'} - x ∥_{2} \leq D$ and $∣ t^{'} - t ∣ \leq D$ . By [F1], $f (x^{'}) - t^{'} \geq f (x) - t - ∣ f (x^{'}) - f (x) ∣ - ∣ t^{'} - t ∣ \geq d - (\sqrt{n} + 1) D > d / 2 > 0.$ So the complement of $epi f$ is open and its epigraph is closed. The scalar $L$ is positive by [F8]; the coordinate-square domination follows by comparing a partial sum with the full nonnegative sum and using [F9].

1.3givenF1F4constructalgebra

The residual ball $C$ contains $y$ because $ϵ \geq 0$ . If $u, v \in C$ and $0 \leq θ \leq 1$ , homogeneity and the triangle inequality in [F1] give $∥ (1 - θ) u + θ v - y ∥_{2} \leq (1 - θ) ∥ u - y ∥_{2} + θ ∥ v - y ∥_{2} \leq ϵ,$ so $C$ is convex. If $u \notin C$ , the gap $d = ∥ u - y ∥_{2} - ϵ > 0$ and the reverse triangle inequality show that every $v$ with $∥ v - u ∥_{2} < d / 2$ also lies outside $C$ . Thus $C$ is closed.

2.1F2F3F5step 1.3constructalgebra∎

By [F5], $epi g = C \times [0, \infty)$ . If $(u, t)$ is outside this epigraph, either $u \notin C$ or $t < 0$ . In the first case step 1.3 supplies an open ball about $u$ disjoint from $C$ , hence a product neighborhood disjoint from the epigraph; in the second case an interval about $t$ contained in $(- \infty, 0)$ supplies such a product neighborhood. Therefore $epi g$ is closed. Since $C$ is nonempty by step 1.3, $g$ is proper. If both endpoints lie in $C$ , their convex combination lies in $C$ by step 1.3 and $g$ is zero there; if either endpoint has value $+ \infty$ with positive coefficient, the convexity inequality has right side $+ \infty$ . Endpoint coefficients reduce to equality at the endpoint with coefficient one. Thus $g$ is convex, and [F2] proves that both functions have the asserted proper, closed, convex properties.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Best s-term ℓ1 approximation error

Definition

Let $n, s \in N$ with $n \geq 1$ and $1 \leq s \leq n$ , and let $x \in R^{n}$ . Use one-based labels $[n] = {1, \dots, n}$ , identifying label $j$ with library coordinate $j - 1$ . For $T \subseteq [n]$ , let $x_{T^{c}}$ retain the coordinates outside $T$ and vanish on $T$ , where $T^{c} = [n] ∖ T$ . Define the best $s$ -term $ℓ^{1}$ approximation error by $σ_{s} (x)_{1} : = \min {∥ x_{T^{c}} ∥_{1} : T \subseteq [n], ∣ T ∣ \leq s} .$ The indexing family is finite and nonempty, so the displayed minimum exists and is attained.

Definition references

One-based coordinate labels and coordinate restrictions

The finite-dimensional one-norm

Minimum of a real set

Attainment of minima on finite nonempty real sets

Finiteness of the power set of a finite set

Finiteness of a subfamily of a finite set

Finite-set convention

Cardinalities of finite sets, including the empty set

Bijection convention for equinumerous sets

Every nonzero natural number is a successor

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

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

Remarks

The attainment clause follows from an explicit finite enumeration. The canonical relabeling $j \mapsto j - 1$ identifies $[n]$ bijectively with the library index set $n = {0, \dots, n - 1}$ , so $[n]$ is finite and its power set is finite; the family $T_{s} : = {T \subseteq [n] : ∣ T ∣ \leq s}$ is a subset of that power set and is therefore finite. It is nonempty because $\emptyset \in T_{s}$ . Since $T_{s}$ is finite, there are a natural number $k$ and a bijection $e : k \to T_{s}$ . Nonemptiness implies $k \neq 0$ , so write $k = ℓ + 1$ . For each $0 \leq j \leq ℓ$ , put $a_{j} : = ∥ x_{e (j)^{c}} ∥_{1}$ . Surjectivity of $e$ gives ${∥ x_{T^{c}} ∥_{1} : T \in T_{s}} = {a_{0}, \dots, a_{ℓ}} .$ This is a finite nonempty set of real numbers. Applying the finite-list minimum result to $a_{0}, \dots, a_{ℓ}$ gives a minimum that is one of these values, hence belongs to the displayed value set. Therefore the displayed minimum in the Definition is attained.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

The ℓ2 robust nullspace property

Definition

Let $m, n, s \in N$ with $m, n \geq 1$ and $1 \leq s \leq n$ , let $A \in R^{m \times n}$ , and let $0 < ρ < 1$ and $τ > 0$ . In real scalar expressions, a natural number denotes its canonical real image. Use one-based coordinate labels $[n] = {1, \dots, n}$ , identifying coordinate label $j$ with library coordinate $j - 1$ . For $h \in R^{n}$ and $S \subseteq [n]$ , let $h_{S}$ agree with $h$ on $S$ and vanish on $S^{c} = [n] ∖ S$ . The matrix $A$ satisfies the $ℓ^{2}$ robust nullspace property of order $s$ with constants $(ρ, τ)$ if $∥ 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$ . This condition applies to all vectors, including vectors with $A h \neq 0$ .

Definition references

One-based coordinates and zero-extended restrictions

Finite-dimensional one- and two-norms

Canonical real image of the natural scalar $s$

Positivity of the natural scalar $s$

Mendelson, Rauhut, and Ward, Improved Bounds for Sparse Recovery from Subsampled Random Convolutions, §2.1, Definition 2.1, printed pp. 4–5

Foucart and Rauhut, A Mathematical Introduction to Compressive Sensing, §4.3, Definitions 4.17 and 4.21

LemmaStatement: AI-adaptedProof: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

A feasible finite-dimensional BPDN problem attains its minimum

Statement

Let $m, n \in N$ with $m, n \geq 1$ , let $A \in R^{m \times n}$ act in the standard finite coordinate bases, with labels $j = 1, \dots, n$ corresponding to library coordinates $j - 1$ , $y \in R^{m}$ , and $ϵ \geq 0$ . If $F : = {z \in R^{n} : ∥ A z - y ∥_{2} \leq ϵ}$ is nonempty, then $z \mapsto ∥ z ∥_{1}$ attains a minimum on $F$ .

Statement references

Finite matrix action and coordinate conventions

Finite-dimensional one- and two-norms

Norm properties of the finite-dimensional norms

Continuity and norm comparison on finite-dimensional spaces

Cauchy–Schwarz for finite coordinate lists

Compactness and attainment of extrema in finite-dimensional real spaces

Foucart and Rauhut, A Mathematical Introduction to Compressive Sensing, §4.3, the quadratically constrained basis-pursuit problem

Facts & Assumptions

Given: Integers $m, n \geq 1$ , a real matrix $A \in R^{m \times n}$ , a vector $y \in R^{m}$ , a radius $ϵ \geq 0$ , and a nonempty set $F = {z : ∥ A z - y ∥_{2} \leq ϵ}$ .

[F1]

The strict nullspace property: $(A u)_{i} = \sum_{j = 1}^{n} A_{i j} u_{j}$ under the one-based labels identified with library coordinate $j - 1$ .

[F2]

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

[F3]

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 and 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 $n \geq 1$ , $∥ \cdot ∥_{2}$ is a positive-definite norm, and every norm $N$ satisfies $∣ N (u) - N (v) ∣ \leq N (u - v)$ , $∥ u ∥_{1} \leq \sqrt{n} ∥ u ∥_{2}$ , and $∥ u ∥_{2} \leq ∥ u ∥_{1}$ .

[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 finite real coordinate lists, $∣ \sum_{j} a_{j} b_{j} ∣ \leq (\sum_{j} a_{j}^{2})^{1 / 2} (\sum_{j} b_{j}^{2})^{1 / 2}$ .

[F5]

Laws of finite sums and finite products: finite sums preserve termwise inequalities and sums of nonnegative terms are nonnegative.

[F6]

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

[F7]

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: in $R^{n}$ with $n \geq 1$ , closed bounded sets are compact, and every continuous real-valued function on a nonempty compact set attains its minimum and maximum; this is a ZF theorem.

[F8]

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

[F9]

Canonical naturals are positive and strictly increasing: because $n \geq 1$ , $n > 0$ .

Proof

1.1givenF1F2F3F4F5F6constructalgebra

Put $M_{A} = (\sum_{i = 1}^{m} \sum_{j = 1}^{n} A_{i j}^{2})^{1 / 2}$ . For $u, v \in R^{n}$ , rowwise Cauchy–Schwarz [F4] and finite-sum monotonicity [F5] give $∥ A (u - v) ∥_{2}^{2} = \sum_{i = 1}^{m} {(\sum_{j = 1}^{n} A_{i j} (u_{j} - v_{j}))}^{2} \leq M_{A}^{2} ∥ u - v ∥_{2}^{2} .$ By [F6], $∥ A (u - v) ∥_{2} \leq M_{A} ∥ u - v ∥_{2}$ . The reverse triangle inequality [F3] now gives $∣ ∥ A u - y ∥_{2} - ∥ A v - y ∥_{2} ∣ \leq ∥ A (u - v) ∥_{2} \leq M_{A} ∥ u - v ∥_{2} .$ If $M_{A} = 0$ , the displayed bound gives $∥ A (u - v) ∥_{2} = 0$ for every $u, v$ ; positive definiteness in [F3] gives $A (u - v) = 0$ , so the residual function is constant and nonemptiness gives $F = R^{n}$ . If $M_{A} > 0$ and $z \notin F$ , the positive gap $d = ∥ A z - y ∥_{2} - ϵ$ shows that every $u$ with $∥ u - z ∥_{2} < d / (2 M_{A})$ also lies outside $F$ . Thus $F$ is closed.

2.1givenF2F3F7F8F9step 1.1choose

Fix one $z_{0} \in F$ and set $K = F \cap {z : ∥ z ∥_{1} \leq ∥ z_{0} ∥_{1}}$ . This set is nonempty because it contains $z_{0}$ . If $∥ z ∥_{1} > ∥ z_{0} ∥_{1}$ , the positive gap $d = ∥ z ∥_{1} - ∥ z_{0} ∥_{1}$ and [F3] show that every $u$ with $∥ u - z ∥_{2} < d / (2 \sqrt{n})$ still has $∥ u ∥_{1} > ∥ z_{0} ∥_{1}$ ; the denominator is positive by [F9]. Thus the second factor is closed, and $K$ is closed by step 1.1. It is bounded since [F3] gives $∥ z ∥_{2} \leq ∥ z ∥_{1} \leq ∥ z_{0} ∥_{1}$ for every $z \in K$ . By [F7], $K$ is compact.

3.1givenF3F7step 2.1algebra∎

The function $z \mapsto ∥ z ∥_{1}$ is continuous by [F3], so [F7] gives a minimizer on the nonempty compact set $K$ . Every feasible point outside $K$ has $∥ z ∥_{1} > ∥ z_{0} ∥_{1}$ , while the minimum on $K$ is at most $∥ z_{0} ∥_{1}$ . Hence this minimum is global on $F$ . The proof selects only one witness $z_{0}$ and uses the stated ZF compactness theorem; no choice axiom is used.

LemmaStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

A block-tail estimate for the largest coordinates

Statement

Let $n, s \in N$ with $n \geq 1$ and $1 \leq s \leq n$ , and let $h \in R^{n}$ use one-based coordinate labels $[n] = {1, \dots, n}$ , with label $j$ corresponding to library coordinate $j - 1$ . In real scalar expressions, a natural number denotes its canonical real image. Order the coordinates by decreasing $∣ h_{j} ∣$ , breaking ties by increasing $j$ . Let $S$ consist of the first $s$ indices, and partition $S^{c}$ in this same order into consecutive nonempty blocks $T_{1}, \dots, T_{q}$ of size $s$ , with only the last block possibly smaller; if $S^{c} = \emptyset$ , take $q = 0$ . Then $∥ h_{S^{c}} ∥_{2} \leq ∥ h_{S} ∥_{2} + \frac{∥ h_{S^{c}} ∥_{1}}{\sqrt{s}} .$

Statement references

One-based finite coordinate restrictions

Finite-dimensional one- and two-norms

Canonical real image of the natural scalar $s$

Triangle inequality for the finite-dimensional two-norm

Positivity and strict increase of canonical natural scalars

Foucart and Rauhut, A Mathematical Introduction to Compressive Sensing, §4.3, proof of Theorem 4.25, printed pp. 89–90

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 $n \geq 1$ , $1 \leq s \leq n$ , a vector $h \in R^{n}$ , the deterministic ordered coordinate list $j_{1}, \dots, j_{n}$ , its first- $s$ set $S = {j_{1}, \dots, j_{s}}$ , and the finite successive tail blocks $T_{1}, \dots, T_{q}$ .

[F1]

The strict nullspace property: $h_{S}$ agrees with $h$ on $S$ and is zero on $S^{c}$ ; the coordinate labels are one-based with label $j$ identified with library coordinate $j - 1$ .

[F2]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ : $∥ v ∥_{1} = \sum_{j} ∣ v_{j} ∣$ and $∥ v ∥_{2} = (\sum_{j} ∣ v_{j} ∣^{2})^{1 / 2}$ on finite-dimensional real coordinate spaces.

[F3]

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: $∥ \cdot ∥_{2}$ is a norm and obeys the triangle inequality.

[F4]

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

[F5]

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

[F6]

The canonical natural $ι (n) = n \cdot 1_{F}$ of a field: a natural number used as a real scalar denotes its canonical real image.

[F7]

Canonical naturals are positive and strictly increasing: the canonical real image of $s$ is positive for $s \geq 1$ ; if $k_{r} \leq s$ as natural numbers, then their canonical real images satisfy $k_{r} \leq s$ .

Proof

1.1givenF1F2F4F5algebra

If $q = 0$ , then $S^{c} = \emptyset$ and the conclusion is $0 \leq ∥ h_{S} ∥_{2}$ . If $q \geq 1$ , write $r = ∣ T_{1} ∣ \leq s$ . The order gives $T_{1} = {j_{s + 1}, \dots, j_{s + r}}$ and $S = {j_{1}, \dots, j_{s}}$ , with $∣ h_{j_{s + k}} ∣ \leq ∣ h_{j_{k}} ∣$ for every $1 \leq k \leq r$ . Termwise squaring and finite-sum monotonicity therefore give $∥ h_{T_{1}} ∥_{2}^{2} = \sum_{k = 1}^{r} ∣ h_{j_{s + k}} ∣^{2} \leq \sum_{k = 1}^{r} ∣ h_{j_{k}} ∣^{2} \leq \sum_{k = 1}^{s} ∣ h_{j_{k}} ∣^{2} = ∥ h_{S} ∥_{2}^{2} .$ Both norms are nonnegative, so [F5] gives $∥ h_{T_{1}} ∥_{2} \leq ∥ h_{S} ∥_{2}$ .

2.1givenF2F3F4F5F6F7step 1.1algebra∎

For each $2 \leq r \leq q$ , the preceding block $T_{r - 1}$ has size $s$ . Its last ordered coordinate has magnitude no greater than any earlier entry, hence no greater than the average magnitude on $T_{r - 1}$ . Every entry of $T_{r}$ is no greater than that last entry. Put $c = ∥ h_{T_{r - 1}} ∥_{1} / s$ . Then each entry of $T_{r}$ has magnitude at most $c$ . If $k_{r} = ∣ T_{r} ∣$ , termwise comparison gives $∥ h_{T_{r}} ∥_{2}^{2} = \sum_{j \in T_{r}} ∣ h_{j} ∣^{2} \leq k_{r} c^{2} \leq s c^{2} = \frac{∥ h_{T_{r - 1}} ∥_{1}^{2}}{s},$ using $k_{r} \leq s$ as natural numbers: padding the sum of $k_{r}$ copies of the nonnegative number $c^{2}$ by the remaining nonnegative copies gives the sum of $s$ copies, by [F4]; [F6,F7] interpret these counts as real scalars. Since both sides are nonnegative, [F5] gives $∥ h_{T_{r}} ∥_{2} \leq \frac{∥ h_{T_{r - 1}} ∥_{1}}{\sqrt{s}} .$ The blocks are disjoint and finite. By [F6], [F7], the triangle inequality, step 1.1, and this block bound, $∥ h_{S^{c}} ∥_{2} = ∥ \sum_{r = 1}^{q} h_{T_{r}} ∥_{2} \leq \sum_{r = 1}^{q} ∥ h_{T_{r}} ∥_{2} \leq ∥ h_{S} ∥_{2} + \frac{1}{\sqrt{s}} \sum_{r = 1}^{q - 1} ∥ h_{T_{r}} ∥_{1} \leq ∥ h_{S} ∥_{2} + \frac{∥ h_{S^{c}} ∥_{1}}{\sqrt{s}} .$ This proves the claimed estimate, including a final block smaller than $s$ .

Remarks

The tie-breaking rule makes the block partition deterministic. The proof uses only finite coordinate comparisons and the Euclidean triangle inequality; no choice axiom is used.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Certified basis-pursuit denoising by primal-dual hybrid gradient

Definition

Inputs are integers $m, n \geq 1$ , a matrix $A \in R^{m \times n}$ in the standard finite coordinate bases, a vector $y \in R^{m}$ , a radius $ϵ \geq 0$ , positive real step sizes $α, β$ , an initial primal-dual state $x^{0} \in R^{n}$ , $p^{0} \in R^{m}$ , a nonnegative integer sweep cap $N$ , positive integer proximal-call caps $C_{f}, C_{g^{*}}$ , and deterministic finite solver programs with Boolean certificate checkers for the two proximal calls. Each solver/checker record must be complete and well-formed. Admissible solver/checker pairs satisfy the soundness condition that an accepted output is an exact minimizer of its stated proximal subproblem; this is an input assumption, not a finite proof search performed by the procedure.

Set $f (x) = ∥ x ∥_{1}$ and $g (u) = 0$ when $∥ u - y ∥_{2} \leq ϵ$ , with $g (u) = + \infty$ otherwise. Define the Fenchel conjugate by $g^{*} (p) = \sup_{u \in R^{m}} (⟨ p, u ⟩ - g (u))$ . For a proper closed convex function $q$ and $t > 0$ , ${prox}_{t q} (v)$ denotes the unique minimizer of $q (w) + ∥ w - v ∥_{2}^{2} / (2 t)$ . Let $A^{*}$ be the Euclidean adjoint and let $∥ A ∥_{2} = \sup_{∥ v ∥_{2} \leq 1} ∥ A v ∥_{2}$ . The target is $\min_{z \in R^{n}} ∥ z ∥_{1} subject to ∥ A z - y ∥_{2} \leq ϵ .$

Return invalid-input if dimensions or vectors do not match, if $ϵ < 0$ , if $N$ is not a nonnegative integer, if either proximal cap is not a positive integer, if either step size is nonpositive, if either solver/checker record is missing or malformed, or if the exact strict check $α β ∥ A ∥_{2}^{2} < 1$ fails. For admissible inputs initialize ${\overset{ˉ}{x}}^{0} = x^{0}$ and perform the exact primal-dual hybrid-gradient recurrence for at most $N$ sweeps: $p^{k + 1} = {prox}_{β g^{*}} (p^{k} + β A {\overset{ˉ}{x}}^{k}), x^{k + 1} = {prox}_{α f} (x^{k} - α A^{*} p^{k + 1}), {\overset{ˉ}{x}}^{k + 1} = 2 x^{k + 1} - x^{k} .$ Use the supplied solver/checker pairs and caps for the corresponding proximal calls. Propagate any invalid-input, prox-call-failed, or prox-cap-exhausted status and the state returned by the primal-dual procedure. If all $N$ sweeps complete, let $(x, p)$ be the final primal-dual state and perform these exact tests in order:

If $p \neq 0$ , $A^{*} p = 0$ , and $∣ ⟨ p, y ⟩ ∣ > ϵ ∥ p ∥_{2}$ , return infeasible.
Otherwise, if $∥ A x - y ∥_{2} \leq ϵ$ , $∥ A^{*} p ∥_{\infty} \leq 1$ , and $∥ x ∥_{1} = - ⟨ p, y ⟩ - ϵ ∥ p ∥_{2}$ , return success with $x$ .
If neither certificate passes, return budget-exhausted with the final state.

For $N = 0$ , test the initial state. The certificate tests use exact real comparisons. The procedure makes no guarantee that a finite run finds a certificate and makes no convergence or finite-termination claim.

Definition references

Primal-dual hybrid-gradient recurrence, proximal-call interface, caps, and statuses

Exact primal optimality and infeasibility certificates

Proper, closed, and convex BPDN objectives

Existence of a minimizer when the residual ball is nonempty

Induced Euclidean operator norm

Proximal mapping as a global minimizer

Existence and uniqueness of proximal minimizers

Euclidean adjoint

Finite-dimensional norms

Chambolle and Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, §§2–3.1

Foucart and Rauhut, A Mathematical Introduction to Compressive Sensing, §4.3

LemmaStatement: Literature-sourcedProof: AI-generatedverified 2026-10-22 (gpt-6.1-sol)Open item page →

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.

LemmaStatement: Literature-sourcedProof: AI-generatedverified 2026-10-22 (gpt-6.1-sol)Open item page →

The largest coordinates attain the best s-term ℓ1 error

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 coordinate labels $[n] = {1, \dots, n}$ , with label $j$ corresponding to library coordinate $j - 1$ . Order the coordinates by decreasing $∣ x_{j} ∣$ , breaking ties by increasing $j$ , and let $S$ be the first $s$ indices. For every $U \subseteq [n]$ , let $x_{U}$ agree with $x$ on $U$ and vanish on $U^{c}$ . Then for every $T \subseteq [n]$ with $∣ T ∣ \leq s$ , $∥ x_{T} ∥_{1} \leq ∥ x_{S} ∥_{1} and ∥ x_{S^{c}} ∥_{1} \leq ∥ x_{T^{c}} ∥_{1} .$ Consequently $σ_{s} (x)_{1} = ∥ x_{S^{c}} ∥_{1}$ , so the best $s$ -term tail error is attained by retaining the first $s$ coordinates in the specified order.

Statement references

Finite-minimum definition of the best s-term tail error

Finite-dimensional one-norm

Monotonicity and additivity 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

Facts & Assumptions

Given: Integers $n \geq 1$ , $1 \leq s \leq n$ , a vector $x \in R^{n}$ , its deterministic decreasing-magnitude order $j_{1}, \dots, j_{n}$ , the set $S = {j_{1}, \dots, j_{s}}$ , and an arbitrary $T \subseteq [n]$ with $∣ T ∣ \leq s$ .

[F1]

Best s-term ℓ1 approximation error: $σ_{s} (x)_{1} = \min {∥ x_{U^{c}} ∥_{1} : U \subseteq [n], ∣ U ∣ \leq s}$ .

[F2]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ : $∥ v ∥_{1} = \sum_{j = 1}^{n} ∣ v_{j} ∣$ for $v \in R^{n}$ , using the stated coordinate relabeling. In particular, for the zero-extended restriction $x_{U}$ , the summand is $∣ x_{j} ∣$ on $U$ and zero elsewhere.

[F3]

Laws of finite sums and finite products, clauses 1, 3 and 4: finite sums are additive for two sequences on the same index range, split at a contiguous index cut, and preserve termwise inequalities; sums of nonnegative terms are nonnegative.

Proof

1.1givenF2F3algebra

If $T = \emptyset$ , its retained mass is zero and is no larger than the nonnegative sum on $S$ . Otherwise write the ranks of the elements of $T$ in increasing order as $r_{1} < \dots < r_{k}$ , where $k = ∣ T ∣ \leq s$ . Then $r_{ℓ} \geq ℓ$ , so the specified ordering gives $∣ x_{j_{r_{ℓ}}} ∣ \leq ∣ x_{j_{ℓ}} ∣$ for each $ℓ$ . The coordinate sum in [F2] may be reordered by successive adjacent swaps, each preserving the sum by associativity and commutativity of real addition; zero terms may be omitted. Thus $∥ x_{T} ∥_{1} = \sum_{ℓ = 1}^{k} ∣ x_{j_{r_{ℓ}}} ∣ \leq \sum_{ℓ = 1}^{k} ∣ x_{j_{ℓ}} ∣ \leq \sum_{ℓ = 1}^{s} ∣ x_{j_{ℓ}} ∣ = ∥ x_{S} ∥_{1}$ , using termwise monotonicity and then the contiguous split at $k$ with a nonnegative remainder.

2.1F1F2F3step 1.1algebra∎

For every $U \subseteq [n]$ and $j \in [n]$ , the zero-extended restrictions satisfy $∣ x_{j} ∣ = ∣ (x_{U})_{j} ∣ + ∣ (x_{U^{c}})_{j} ∣$ . Summing over the original full coordinate range and applying [F2] and the same-range additivity in [F3] gives $∥ x ∥_{1} = ∥ x_{U} ∥_{1} + ∥ x_{U^{c}} ∥_{1}$ . Taking $U = T$ and $U = S$ and subtracting the retained masses, step 1.1 implies $∥ x_{S^{c}} ∥_{1} \leq ∥ x_{T^{c}} ∥_{1}$ . Applying this inequality to every admissible $T$ , while $S$ itself is admissible, shows that the finite minimum in [F1] equals $∥ x_{S^{c}} ∥_{1}$ .

TheoremStatement: Literature-sourcedProof: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

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.

4 · Examples, counterexamples and false statements

None yet.

Stable compressed sensing with noise

2 · Logical flowchart

3 · Definitions, theorems and proofs

Primal and infeasibility certificates for basis pursuit denoising

Statement

Statement references

Facts & Assumptions

Proof

The basis-pursuit denoising objective and residual indicator are proper closed convex

Statement

Statement references

Facts & Assumptions

Proof

Best s-term ℓ1 approximation error

Definition

Definition references

Remarks

The ℓ2 robust nullspace property

Definition

Definition references

A feasible finite-dimensional BPDN problem attains its minimum

Statement

Statement references

Facts & Assumptions

Proof

A block-tail estimate for the largest coordinates

Statement

Statement references

Facts & Assumptions

Proof

Remarks

Certified basis-pursuit denoising by primal-dual hybrid gradient

Definition

Definition references

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

Statement

Statement references

Facts & Assumptions

Proof

The largest coordinates attain the best s-term ℓ1 error

Statement

Statement references

Facts & Assumptions

Proof

Robust nullspace property gives stable noisy recovery

Statement

Statement references

Facts & Assumptions

Proof

4 · Examples, counterexamples and false statements

Sources