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.

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.

Depends on

Used by

Dependency tree · two levels

65 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 (standard reference, not scraped)