Support, $\ell^1$ norm and Euclidean norm on $\mathbb{R}^m$

Definition

CandesTao_Decoding_Norms

by naimengye · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

compressed-sensingerror-correcting-codesl1-minimizationlinear-programmingrestricted-isometrysparse-recovery

Three elementary notions used throughout the mission, for real vectors indexed by $\{1,\dots,m\}$ .

A vector $c \in \mathbb{R}^m$ is supported on an index set $T \subseteq \{1,\dots,m\}$ when $c_j = 0$ for every $j \notin T$ . This is how the paper's "real vector supported on a set $T$ " and its coefficient vectors $(c_j)_{j \in T}$ are represented: a vector of full length $m$ whose coordinates outside $T$ vanish, so that $F_T c = \sum_{j \in T} c_j v_j$ is simply the matrix–vector product $Fc$ .
The $\ell^1$ norm $\|c\|_{\ell^1} = \sum_{j=1}^m |c_j|$ (paper, Section 1.2).
The Euclidean norm $\|x\| = \big(\sum_i x_i^2\big)^{1/2}$ , used both for coefficient vectors in $\mathbb{R}^m$ and for vectors in $\mathbb{R}^p$ ; the paper writes it $\|\cdot\|$ or $\|\cdot\|_H$ .

These are the only norms that enter the restricted isometry constants of Definition 1.1 and the two $\ell^1$ -minimization problems $(P_1)$ and $(P_1')$ of the mission.

Formalization Note Both norms are explicit finite sums rather than instances of Mathlib's normed-space structure on EuclideanSpace, so that every statement of the mission can be audited by hand against the paper.

Definition code

import Mathlib.Analysis.Real.Sqrt
import Mathlib.Data.Matrix.Mul

namespace CandesTao.Decoding

/-- A vector `c ∈ ℝ^m` is supported on the index set `T` when every coordinate outside `T`
is zero. -/
def SupportedOn {m : ℕ} (c : Fin m → ℝ) (T : Finset (Fin m)) : Prop :=
  ∀ j, j ∉ T → c j = 0

/-- The ℓ¹ norm `‖c‖_{ℓ¹} = ∑_j |c_j|`. -/
def l1Norm {m : ℕ} (c : Fin m → ℝ) : ℝ := ∑ j, |c j|

/-- The Euclidean (ℓ²) norm `‖x‖ = (∑_i x_i²)^{1/2}`. -/
noncomputable def l2Norm {n : ℕ} (x : Fin n → ℝ) : ℝ := Real.sqrt (∑ i, x i ^ 2)

end CandesTao.Decoding

Source

Candès--Tao 2005, Decoding by Linear Programming, IEEE Trans. Inform. Theory 51(12):4203-4215, doi:10.1109/TIT.2005.858979; arXiv:math/0502327v1 (https://arxiv.org/abs/math/0502327), pp. 2-5: support (Lemma 1.3, Theorem 1.4), l1 norm eq. (1.4), Euclidean norm eq. (1.7)-(1.8)

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

SupportedOn (full name CandesTao.Decoding.SupportedOn). This is a definition of a proposition (a truth-valued statement), not a theorem. It takes three inputs: a natural number $m \ge 0$ (an implicit argument, inferred from $c$ ), a vector $c = (c_0, c_1, \dots, c_{m-1})$ of real numbers indexed by $\{0, 1, \dots, m-1\}$ , and a finite set $T \subseteq \{0, 1, \dots, m-1\}$ of indices (since the index set is itself finite, $T$ may be any subset of it). The proposition $\mathrm{SupportedOn}(c, T)$ asserts

\forall j \in \{0, \dots, m-1\},\qquad j \notin T \implies c_j = 0,

i.e. every coordinate of $c$ whose index lies outside $T$ is exactly zero; equivalently, the set $\{\, j : c_j \neq 0 \,\}$ is contained in $T$ . Nothing is asserted about the coordinates $c_j$ with $j \in T$ (they may be zero or nonzero), so this is containment of the support in $T$ , not equality of the support with $T$ . Edge cases: if $T$ is the whole index set the proposition holds for every $c$ ; if $T = \emptyset$ it says that $c$ is the zero vector; if $m = 0$ the index set is empty, the only possible $T$ is $\emptyset$ , and the proposition holds vacuously for the unique (empty) vector $c$ .

l1Norm (full name CandesTao.Decoding.l1Norm). This is a definition of a real number. It takes a natural number $m \ge 0$ (implicit, inferred from $c$ ) and a vector $c = (c_0, \dots, c_{m-1})$ of real numbers indexed by $\{0, \dots, m-1\}$ , and returns

\|c\|_{1} := \sum_{j=0}^{m-1} |c_j| ,

the sum, over every index $j$ in the full index set $\{0,\dots,m-1\}$ (not over any subset), of the ordinary absolute value of the real number $c_j$ . Edge case: for $m = 0$ the sum is empty and the value is $0$ . The definition asserts nothing beyond this formula (for instance, it does not itself state nonnegativity or that this is a norm); it simply names this real number.

l2Norm (full name CandesTao.Decoding.l2Norm). This is a definition of a real number (flagged as noncomputable, which carries no mathematical content). It takes a natural number $n \ge 0$ (implicit, inferred from $x$ ; note the dimension variable is called $n$ here whereas the two declarations above use $m$ , and there is no linkage between them) and a vector $x = (x_0, \dots, x_{n-1})$ of real numbers indexed by $\{0, \dots, n-1\}$ , and returns

\|x\|_{2} := \sqrt{\sum_{i=0}^{n-1} x_i^{2}},

where $x_i^{2}$ means $x_i \cdot x_i$ (the exponent is the natural number $2$ ) and the sum runs over the entire index set. The square root is Mathlib's real square-root function $\sqrt{\cdot} : \mathbb{R} \to \mathbb{R}$ , which on a nonnegative argument $a \ge 0$ returns the unique nonnegative real $s$ with $s^{2} = a$ , and on a negative argument returns the junk value $0$ . Here the radicand is a sum of squares of real numbers and hence always $\ge 0$ , so the junk branch is never reached and the value is the ordinary nonnegative square root. Edge case: for $n = 0$ the sum is empty, the radicand is $0$ , and the value is $\sqrt{0} = 0$ . Nothing beyond this formula (for example, that it is a norm) is asserted by the definition.

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Support, ℓ1\ell^1ℓ1 norm and Euclidean norm on Rm\mathbb{R}^mRm

Support, $\ell^1$ norm and Euclidean norm on $\mathbb{R}^m$