ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Diagonal operator on ell p is compact iff diagonal tends to zero

Example

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). Let $K = R$ or $C$ , let $1 \leq p \leq \infty$ and let $a : N \to K$ , $n \mapsto a_{n}$ , be bounded in modulus: there is a real $M \geq 0$ such that $∣ a_{n} ∣ \leq M$ for every $n$ . Write $ℓ^{p} (N, K)$ for the counting-measure space $L^{p} (#; K)$ on $(N, P (N), #)$ , read as the space of scalar sequences $x$ with $\sum_{n} ∣ x_{n} ∣^{p} < \infty$ for $p < \infty$ and with $\sup_{n} ∣ x_{n} ∣ < \infty$ for $p = \infty$ (Counting measure on an arbitrary set, Counting measure is a measure, $ℓ^{p}$ is the $L^{p}$ space of counting measure, Complex Lp classes and Euclidean test-function conventions), and let

$D_{a} : ℓ^{p} (N, K) ⟶ ℓ^{p} (N, K), (D_{a} x)_{n} : = a_{n} x_{n},$

be the diagonal operator. Then $D_{a}$ is compact (Compact linear operator) if and only if $a_{n} \to 0$ , meaning that for every real $ε > 0$ there is $N \in N$ such that $∣ a_{n} ∣ < ε$ whenever $n \geq N$ .

Facts & Assumptions

[A1]

On $(N, P (N), #)$ every real function is measurable, for real $f$ one has $\int ∣ f ∣^{p} d # = \sum_{n} ∣ f (n) ∣^{p}$ for $0 < p < \infty$ and $∥ f ∥_{\infty} = \sup_{n} ∣ f (n) ∣$ , and almost-everywhere equality is equality everywhere ( $ℓ^{p}$ is the $L^{p}$ space of counting measure, Counting measure on an arbitrary set); for complex $f = u + i v$ measurability means measurability of $u, v$ , so every complex function on $N$ is measurable, and $L^{p} (#; C)$ is complete under ${A C}_{ω}$ (Complex Lp classes and Euclidean test-function conventions, Complex completeness, density, and inner product: the consumer interface).

[A2]

Real $L^{p} (#)$ is complete under countable choice (Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$ ); completeness of the target is what the norm-closure theorem needs for a compact conclusion (Banach space, A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[A3]

For $λ$ a scalar and $n$ fixed, the sequence $e_{n}$ that is $1$ at $n$ and $0$ elsewhere lies in $ℓ^{p}$ with $∥ e_{n} ∥_{p} = 1$ for every $1 \leq p \leq \infty$ (Counting measure on an arbitrary set, $ℓ^{p}$ is the $L^{p}$ space of counting measure, Complex Lp classes and Euclidean test-function conventions).

[A4]

A bounded finite-rank operator is compact (Bounded finite rank operators are compact); under ${A C}_{ω}$ a norm limit of compact operators with Banach target is compact (Norm limit of compact operators is compact); under DC a compact operator sends bounded sequences to sequences with convergent subsequences (Sequential characterization of compact operators, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, The Axiom of Countable Choice ( ${A C}_{ω}$ ), Dependent choice implies countable choice).

[A5]

The operator norm bounds $∥ T x ∥ \leq ∥ T ∥ ∥ x ∥$ and equals the supremum of $∥ T x ∥$ over the closed unit ball (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces, Open ball, closed ball and sphere in a metric space); operator-norm convergence is metric convergence (Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ), while scalar convergence has the explicit epsilon meaning in the statement.

Verification

technique · direct

Given: $D C$ , $K \in {R, C}$ , $1 \leq p \leq \infty$ , a bounded sequence $a$ , the operator $D_{a}$ on $ℓ^{p} (N, K)$ , and the truncations $D_{a}^{(N)}$ defined by $(D_{a}^{(N)} x)_{n} = a_{n} x_{n}$ for $n < N$ and $0$ for $n \geq N$ .

1.1

$D_{a}$ is well defined and bounded with $∥ D_{a} x ∥_{p} \leq ∥ a ∥_{\infty} ∥ x ∥_{p}$ , because $∣ a_{n} x_{n} ∣ \leq ∥ a ∥_{\infty} ∣ x_{n} ∣$ for every $n$ ; so $∥ D_{a} ∥ \leq ∥ a ∥_{\infty}$ .

A1A5algebra

1.2

Each truncation $D_{a}^{(N)}$ is bounded, and its range is contained in the linear span of $e_{0}, \dots, e_{N - 1}$ , so $D_{a}^{(N)}$ has finite rank and is compact by [A4].

A3A4

1.3

If $a_{n} \to̸ 0$ , then there is a real $ε > 0$ and a strictly increasing $n$ with $∣ a_{n_{k}} ∣ \geq ε$ for all $k$ : this is the negation of convergence, and the indices are chosen by DC (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, A strictly increasing index map satisfies $n_{k} \geq k$ ).

2.1

For every $N$ one has $∥ D_{a} - D_{a}^{(N)} ∥ = \sup_{n \geq N} ∣ a_{n} ∣$ : the upper bound is [step 1.1] applied to the tail sequence, and the lower bound follows by testing $e_{n}$ for $n \geq N$ , where $∥ (D_{a} - D_{a}^{(N)}) e_{n} ∥_{p} = ∣ a_{n} ∣$ .

step 1.1A3A5

2.2

Under the hypothesis of [step 1.3], the bounded sequence $(e_{n_{k}})$ has $∥ D_{a} e_{n_{k}} - D_{a} e_{n_{l}} ∥_{p} \geq ε$ for all $k \neq l$ (indeed it is at least $(ε^{p} + ε^{p})^{1 / p}$ for $p < \infty$ and at least $ε$ for $p = \infty$ ), so the sequence of images has no convergent subsequence; by the sequential characterization [A4] the operator $D_{a}$ is not compact.

step 1.3A3A4A5

3.1

If $a_{n} \to 0$ , then for every real $ε > 0$ there is $N$ with $∣ a_{n} ∣ < ε$ for all $n \geq N$ , so $∥ D_{a} - D_{a}^{(N)} ∥ \leq ε$ by [step 2.1]; hence $D_{a}$ is a norm limit of the compact operators $D_{a}^{(N)}$ and is compact by [A4], the target $ℓ^{p}$ being Banach by [A1] and [A2].

step 1.2step 2.1A1A2A4

4.1

Steps [step 3.1] and [step 2.2] are the two directions of the equivalence, so the diagonal operator $D_{a}$ on $ℓ^{p} (N, K)$ is compact exactly when $a_{n} \to 0$ .

step 3.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

116 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

Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §3.1 p.70, example after Theorem 3.2 (standard reference, not scraped)
Theo Bühler and Dietmar Salamon, Functional Analysis — §4.2 p.186, Example 4.26 (standard reference, not scraped)