LemmaStatement: AI-adaptedProof: 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.

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.

Depends on

Used by

Dependency tree · two levels

55 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

Antonin Chambolle and Thomas Pock, A First-Order Primal-Dual Algorithm for Convex Problems with Applications to Imaging, §2 (standard reference, not scraped)
Simon Foucart and Holger Rauhut, A Mathematical Introduction to Compressive Sensing, §4.3 (standard reference, not scraped)