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.

Finite-rank truncations of a square-integrable kernel

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $a = (a_{n})_{n \in N}$ be a square-summable complex family, that is an element of $ℓ^{2} (N, C)$ (Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ ), and let $X = Y = N$ carry counting measure $#$ (Counting measure on an arbitrary set, Counting measure is a measure), so that $L^{2} (#; C)$ is the space of complex square-summable sequences ( $ℓ^{p}$ is the $L^{p}$ space of counting measure, The space $L^{p} (μ)$ as the quotient by null functions). Put

$k (m, n) : = {\begin{cases} a_{n}, & m = n, \\ 0, & m \neq n, \end{cases} (m, n) \in N^{2} .$

Then $k \in L^{2} (# \times #; C)$ with $∥ k ∥_{2} = ∥ a ∥_{2}$ , the kernel operator of L two kernels give Hilbert–Schmidt operators is the diagonal operator $(T_{k} f) (m) = a_{m} f (m)$ , and for every $N \in N$ the truncation $k_{N} (m, n) : = k (m, n)$ for $n \leq N$ and $k_{N} (m, n) : = 0$ for $n > N$ satisfies:

$T_{k_{N}}$ has finite rank: its range admits the ordered basis $(e_{j_{q}})_{q < r}$ of Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, where $J = {n \leq N : a_{n} \neq 0} = {j_{0} < \dots < j_{r - 1}}$ is the increasing enumeration of $J$ and $e_{n}$ is the class of $1_{{n}}$ , so $T_{k_{N}}$ is compact (Bounded finite rank operators are compact);
$∥ T_{k} - T_{k_{N}} ∥_{H S} = (\sum_{n > N} ∣ a_{n} ∣^{2})^{1 / 2}$ (Hilbert–Schmidt operator and Hilbert–Schmidt norm);
$∥ T_{k} - T_{k_{N}} ∥ = \sup_{n > N} ∣ a_{n} ∣$ , the supremum being a real number (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

Facts & Assumptions

Given: The Axiom of Choice, a square-summable complex family $(a_{n})$ , counting measure on $N$ , the diagonal kernel $k$ and its truncations $k_{N}$ , and the standard vectors $e_{n}$ of $L^{2} (#; C)$ .

[F1]

Counting measure is a sigma-finite measure on $(N, P (N))$ , since $N = ⋃_{N} {0, \dots, N}$ and each finite set has finite counting measure; every function on $N$ is measurable, $\int g d #$ is the series sum of $g$ for nonnegative $g$ and for integrable $g$ , and almost-everywhere equality is equality everywhere (Counting measure on an arbitrary set, Counting measure is a measure, $ℓ^{p}$ is the $L^{p}$ space of counting measure, Finite, sigma-finite, and semifinite measures).

[F2]

Tonelli applies to nonnegative product-measurable functions on $N \times N$ : $\int g d (# \times #) = \sum_{m} \sum_{n} g (m, n)$ (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Counting measure on an arbitrary set).

[F3]

The kernel theorem gives the well-defined bounded kernel operator, its exact Hilbert–Schmidt norm $∥ T_{h} ∥_{H S} = ∥ h ∥_{2}$ for every square-integrable kernel $h$ , and the Hilbert–Schmidt compactness theorem gives that such an operator is compact under Countable Choice (L two kernels give Hilbert–Schmidt operators, Hilbert–Schmidt operator and Hilbert–Schmidt norm, Hilbert–Schmidt operators are compact).

[F4]

A bounded linear operator whose range admits an ordered basis of finite length is compact (Bounded finite rank operators are compact, A bounded linear operator between normed spaces).

[F5]

The vectors $e_{n}$ are orthonormal, hence linearly independent with $∥ e_{n} ∥ = 1$ , and they span the ranges considered below; an ordered basis is an injective finite list whose image is a basis (Orthonormal families, complete orthonormal systems and Hilbert bases, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Linear combination of a finite list, and the span $span (S)$ as the smallest linear subspace containing $S$ ).

[F6]

The operator norm is the supremum of $∥ D f ∥$ over $∥ f ∥ \leq 1$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F7]

Since $∣ a_{n} ∣^{2} \leq \sum_{k} ∣ a_{k} ∣^{2} = ∥ a ∥_{2}^{2}$ , the set ${∣ a_{n} ∣ : n > N}$ is nonempty and bounded above in $R$ , so its supremum is a real number by the least-upper-bound property (Complete ordered field (least-upper-bound property), Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , The natural numbers $N$ (von Neumann)).

[F8]

Choice implies Countable Choice (The Axiom of Choice, AC supplies the countable and dependent choices used in Banach integration).

Verification

technique · direct

Given: The objects above, a square-summable $(a_{n})$ , the diagonal kernel $k$ , its truncations $k_{N}$ , and for $N \in N$ the finite set $J = {n \leq N : a_{n} \neq 0}$ .

1.1

By [F1] the counting measures are sigma-finite and every subset of $N^{2}$ is measurable, and by [F2] applied to $∣ k ∣^{2}$ one has $∥ k ∥_{L^{2} (# \times #)}^{2} = \sum_{m} \sum_{n} ∣ k (m, n) ∣^{2} = \sum_{n} ∣ a_{n} ∣^{2} = ∥ a ∥_{2}^{2} < + \infty$ ; hence $k$ is a square-integrable kernel with $∥ k ∥_{2} = ∥ a ∥_{2}$ , and the same computation applies to every diagonal kernel with square-summable coefficients.

F1F2F8

2.1

For every $m$ , the defining integral of the kernel operator is the counting sum $\int k (m, n) f (n) d # (n) = \sum_{n} k (m, n) f (n)$ , in which the only possibly nonzero term is $n = m$ , so $(T_{k} f) (m) = a_{m} f (m)$ ; by [F3] this diagonal operator is well defined on $L^{2} (#; C)$ and bounded with $∥ T_{k} ∥ \leq ∥ k ∥_{2} = ∥ a ∥_{2}$ .

step 1.1F1F3

2.2

The truncated kernels. For fixed $N$ the kernel $k - k_{N}$ is diagonal with coefficients $a_{n} 1_{n > N}$ , a square-summable family, so [step 1.1] applied to it gives $∥ T_{k} - T_{k_{N}} ∥_{H S} = ∥ k - k_{N} ∥_{L^{2} (# \times #)} = (\sum_{n > N} ∣ a_{n} ∣^{2})^{1 / 2}$ by the exact-norm part of [F3]; moreover $k_{N}$ is the diagonal kernel with coefficients $a_{n} 1_{n \leq N}$ , so $T_{k_{N}}$ is the diagonal operator with those coefficients.

step 1.1F3

3.1

Finite rank of the truncations. By [step 2.2] the range of $T_{k_{N}}$ is the set of sequences $a_{n} 1_{n \leq N} f (n) e_{n}$ , which is exactly the span of ${e_{n} : n \in J}$ . Since $J \subseteq {0, \dots, N}$ is finite, write its increasing enumeration as $J = {j_{0} < \dots < j_{r - 1}}$ for some $r \in N$ . The map $q \mapsto e_{j_{q}}$ with domain the von Neumann natural $r$ is an injective finite list whose image is an orthonormal family, hence is linearly independent, and it spans the range. Thus $(e_{j_{q}})_{q < r}$ is an ordered basis of the range, and $T_{k_{N}}$ is compact by [F4], while its Hilbert–Schmidt norm is finite by [step 2.2].

step 2.2F4F5

3.2

Operator norm of the difference. Let $D : = T_{k} - T_{k_{N}}$ , so that $(D f) (m) = a_{m} 1_{m > N} f (m)$ by [step 2.2]. For every $f$ in $L^{2} (#; C)$ one has $∥ D f ∥^{2} = \sum_{m > N} ∣ a_{m} ∣^{2} ∣ f (m) ∣^{2} \leq S_{N}^{2} ∥ f ∥^{2}$ where $S_{N} : = \sup_{n > N} ∣ a_{n} ∣$ is the real number of [F7], so $∥ D ∥ \leq S_{N}$ by [F6]; conversely for each $m > N$ the vector $e_{m}$ has norm one by [F5] and $D e_{m} = a_{m} e_{m}$ , so $∥ D ∥ \geq ∣ a_{m} ∣$ and hence $∥ D ∥ \geq S_{N}$ . Therefore $∥ D ∥ = S_{N} = \sup_{n > N} ∣ a_{n} ∣$ .

step 2.2F5F6F7

4.1

Collecting the results, $k$ is a square-integrable diagonal kernel with $∥ k ∥_{2} = ∥ a ∥_{2}$ , $T_{k}$ is the diagonal operator of [step 2.1], the truncations $T_{k_{N}}$ are finite rank and compact by [step 3.1], and the two exact truncation errors are [step 2.2] and [step 3.2].

step 2.1step 2.2step 3.1step 3.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

111 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.6, diagonal Hilbert–Schmidt operators, printed pp. 93–95 (standard reference, not scraped)
John Roe, Lectures on Analysis — Lecture 13, diagonal examples after Definition 13.1, printed p. 67 (standard reference, not scraped)