ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Integral operator trace under a valid diagonal hypothesis

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $(X, d)$ be a compact metric space, let $μ$ be a finite regular Borel measure on $X$ (Finite, sigma-finite, and semifinite measures, Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ ) and let $k : X \times X \to C$ be continuous, Hermitian, $k (y, x) = \overline{k (x, y)}$ , and positive semidefinite, that is $\sum_{i, j = 1}^{n} c_{i} \overline{c_{j}} k (x_{i}, x_{j}) \geq 0$ for all finite families $x_{1}, \dots, x_{n} \in X$ and scalars $c_{1}, \dots, c_{n} \in C$ . Let $T_{k}$ be the integral operator on the complex Hilbert space $L^{2} (X, μ; C)$ ( $L^{2}$ with the integral pairing is a Hilbert space, The complex $L^{2}$ pairing is well-defined and satisfies Cauchy–Schwarz) $T_{k} f (x) : = \int_{X} k (x, y) f (y) d μ (y) .$ Then:

$T_{k}$ is a bounded Hilbert–Schmidt operator with $∥ T_{k} ∥_{H S} = ∥ k ∥_{L^{2} (μ \times μ)}$ and $∥ T_{k} ∥ \leq ∥ k ∥_{L^{2} (μ \times μ)}$ , hence compact (L two kernels give Hilbert–Schmidt operators, Hilbert–Schmidt operator and Hilbert–Schmidt norm, Compact linear operator);
$T_{k}$ is self-adjoint and positive: $T_{k}^{*} = T_{k}$ and $⟨ T_{k} f, f ⟩ \geq 0$ for all $f$ (Self-adjoint, positive, unitary and normal operators);
$T_{k}$ is trace class and $tr (T_{k}) = \int_{X} k (x, x) d μ (x)$ (Trace class operator, Trace is absolutely convergent and basis independent);
two boundaries are part of the statement. First, a class in $L^{2} (X \times X, μ \times μ)$ does not in general determine diagonal values: when $μ$ is nonzero and nonatomic, representatives may be changed on the product-null diagonal, changing their diagonal integrals. Thus the displayed identity is a theorem under the continuity and positivity hypotheses and is not a definition of the trace. Second, continuity of $k$ alone does not imply trace class: it only gives Hilbert–Schmidt, and a continuous Hermitian kernel that is not positive semidefinite may fail to be trace class.

Facts & Assumptions

Given: AC, the compact metric space $X$ , the finite regular Borel measure $μ$ , the continuous Hermitian positive semidefinite kernel $k$ , and the symbols $k_{x} : = k (\cdot, x)$ .

[A1]

Kernel arithmetic. $k$ is bounded and measurable on $X \times X$ with $∥ k ∥_{2}^{2} = \int_{X \times X} ∣ k ∣^{2} d (μ \times μ) \leq μ (X)^{2} \sup ∣ k ∣^{2} < + \infty$ , the completed product measure is finite and Tonelli applies to nonnegative measurable functions (The completed product measure, Tonelli and Fubini for the completed product, with only almost-everywhere section measurability, Finite, sigma-finite, and semifinite measures, Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ ).

[A2]

Kernel operators. For $k$ of finite square norm the operator $T_{k}$ is bounded with $∥ T_{k} ∥ \leq ∥ k ∥_{2}$ , is Hilbert–Schmidt with $∥ T_{k} ∥_{H S} = ∥ k ∥_{2}$ , and is compact by Hilbert–Schmidt operators are compact applied to the Hilbert basis supplied under AC by the kernel theorem; the complex space $L^{2} (X, μ; C)$ with $⟨ f, g ⟩ = \int f \overline{g} d μ$ is a Hilbert space (L two kernels give Hilbert–Schmidt operators, $L^{2}$ with the integral pairing is a Hilbert space, The complex $L^{2}$ pairing is well-defined and satisfies Cauchy–Schwarz, Hilbert–Schmidt operator and Hilbert–Schmidt norm, A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Hilbert space, Banach space, Compact linear operator).

[A3]

The reproducing-kernel space. On the complex span $E_{0}$ of the functions $k_{x}$ put $⟨ \sum_{i} a_{i} k_{x_{i}}, \sum_{j} b_{j} k_{y_{j}} ⟩_{0} : = \sum_{i, j} a_{i} \overline{b_{j}} k (y_{j}, x_{i})$ . Positive semidefiniteness and Hermitian symmetry make this a positive semidefinite Hermitian form, so $∣ ⟨ h, g ⟩_{0} ∣^{2} \leq ⟨ h, h ⟩_{0} ⟨ g, g ⟩_{0}$ and the null set $N : = {h : ⟨ h, h ⟩_{0} = 0}$ is a subspace on which the form vanishes identically and whose elements are exactly the functions vanishing on $X$ , because $∣ h (x) ∣ = ∣ ⟨ h, k_{x} ⟩_{0} ∣ \leq ∥ h ∥_{0} ∥ k_{x} ∥_{0} = ∥ h ∥_{0} \sqrt{k (x, x)}$ for $h \in E_{0}$ ; the quotient $E_{0} / N$ with the induced inner product has a completion $H_{k}$ , a Hilbert space (The norm completion of an inner-product space is a Hilbert space, Real and complex inner-product spaces and their induced length, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, Orthogonality and the orthogonal complement). In $H_{k}$ the reproducing identity $h (x) = ⟨ h, k_{x} ⟩$ and the bound $∣ h (x) ∣ \leq ∥ h ∥ \sqrt{k (x, x)}$ hold, the inclusion $J : H_{k} \to L^{2} (X, μ)$ , $J h : = h$ , is a well-defined bounded linear map with $∥ J ∥ \leq \sqrt{μ (X) \sup_{x} k (x, x)}$ , and $T_{k} = J J^{*}$ (Hilbert-adjoint identities, The Hilbert-space adjoint of a bounded operator).

[A4]

A finite or countable orthonormal basis of $H_{k}$ . By compactness $X$ is totally bounded, so for each integer $n \geq 1$ there is a finite $(1 / n)$ -net of $X$ (A compact metric space is complete and totally bounded, and neither implication uses any choice principle); AC chooses one net for each $n \geq 1$ , their union $D$ is at most countable and dense, and the $Q (i)$ -span of ${k_{d} : d \in D}$ is an at most countable dense subset of $H_{k}$ , because $∥ k_{x} - k_{y} ∥^{2} = k (x, x) - k (x, y) - k (y, x) + k (y, y) \to 0$ as $y \to x$ by continuity and Hermitian symmetry. The separable-basis theorem therefore provides a Hilbert basis $(e_{i})_{i \in I}$ of $H_{k}$ , where $I$ is empty, finite, or countably infinite (A Hilbert space with a dense sequence has a finite or countable orthonormal basis, Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, Finite, countably infinite, countable, uncountable, Every subset of an at most countable set is at most countable, Countable unions of at most countable sets, assuming ${A C}_{ω}$ , Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ , Orthonormal families, complete orthonormal systems and Hilbert bases). Using its canonical order, write the basis as $(e_{1}, \dots, e_{r})$ when it is finite and as $(e_{j})_{j \geq 1}$ when it is infinite, and define a positive-integer-indexed family $(h_{j})_{j \geq 1}$ by $h_{j} = e_{j}$ on the existing indices and $h_{j} = 0$ after $r$ in the finite case (all terms are zero when $I = \emptyset$ ).

[A5]

Nuclear series, Parseval and Tonelli. A positive-integer-indexed nuclear family whose shifted coefficient-norm series is summable has zero-based partial sums converging in operator norm and defines a trace-class operator, whose trace is the corresponding shifted sum $\sum_{j \geq 1} ⟨ v_{j}, u_{j} ⟩$ with $∥ T ∥_{1} \leq \sum_{j \geq 1} ∥ u_{j} ∥ ∥ v_{j} ∥$ ; and for the Hilbert basis $(e_{i})_{i \in I}$ of $H_{k}$ , Parseval gives $\sum_{i \in I} ∣ e_{i} (x) ∣^{2} = \sum_{i \in I} ∣ ⟨ k_{x}, e_{i} ⟩ ∣^{2} = k (x, x)$ for every $x$ , while Tonelli for this at most countable nonnegative family gives $\int_{X} \sum_{i \in I} ∣ e_{i} (x) ∣^{2} d μ (x) = \sum_{i \in I} ∥ J e_{i} ∥^{2}$ (Nuclear series characterizes trace norm, Trace is absolutely convergent and basis independent, Trace of a trace class operator, Parseval equivalences for an orthonormal family, Tonelli and Fubini for the completed product, with only almost-everywhere section measurability).

Verification

technique · direct

Given: AC, the data above, the space $H_{k}$ with its basis $(e_{i})_{i \in I}$ , its zero-padded positive enumeration $(h_{j})_{j \geq 1}$ , and the inclusion $J$ .

1.1

The operator and its factorization. By [A1] the class of $k$ has finite square norm, so [A2] makes $T_{k}$ a bounded Hilbert–Schmidt compact operator with the stated norms. By [A3] the inclusion $J$ is bounded with $T_{k} = J J^{*}$ : for $f \in L^{2}$ and every $x$ , $(J J^{*} f) (x) = ⟨ J^{*} f, k_{x} ⟩ = ⟨ f, J k_{x} ⟩_{L^{2}} = \int_{X} f (y) \overline{k (y, x)} d μ (y) = \int_{X} k (x, y) f (y) d μ (y) = (T_{k} f) (x)$ , using the reproducing identity and Hermitian symmetry.

A1A2A3

1.2

$J$ is Hilbert–Schmidt and $T_{k}$ is positive. By [A4] the family $(e_{i})_{i \in I}$ is a Hilbert basis of the domain $H_{k}$ of $J$ , so $\sum_{i \in I} ∥ J e_{i} ∥^{2} = \int_{X} \sum_{i \in I} ∣ e_{i} (x) ∣^{2} d μ (x) = \int_{X} k (x, x) d μ (x)$ by [A5], and the right-hand side is finite because $k (x, x)$ is continuous on the compact space $X$ ; hence $J$ is Hilbert–Schmidt relative to this supplied basis, including the finite and zero-dimensional cases. Moreover $T_{k}^{*} = (J J^{*})^{*} = J J^{*} = T_{k}$ and $⟨ T_{k} f, f ⟩ = ⟨ J^{*} f, J^{*} f ⟩ \geq 0$ for all $f$ by [A3], so $T_{k}$ is self-adjoint and positive.

A1A3A4A5

1.3

Trace class and the trace formula. Expanding $J^{*}$ in the Hilbert basis and then using the zero-padded enumeration of [A4] gives $J^{*} f = \sum_{i \in I} ⟨ J^{*} f, e_{i} ⟩ e_{i} = \sum_{j \geq 1} ⟨ f, J h_{j} ⟩ h_{j},$ where the first expression is a finite-subset net and the second is its ordinary positive-indexed enumeration (eventually zero in finite dimension). Applying $J$ gives the positive-indexed nuclear representation $T_{k} = J J^{*} = \sum_{j \geq 1} ⟨ \cdot, J h_{j} ⟩ J h_{j} .$ Its zero-based partial sums converge in operator norm by [A5], and its shifted coefficient-norm series satisfies $\sum_{j \geq 1} ∥ J h_{j} ∥^{2} = \sum_{i \in I} ∥ J e_{i} ∥^{2} = \int_{X} k (x, x) d μ (x) < + \infty$ by [step 1.2]. Hence [A5] makes $T_{k}$ trace class with $∥ T_{k} ∥_{1} \leq \int_{X} k (x, x) d μ (x)$ and $tr (T_{k}) = \sum_{j \geq 1} ⟨ J h_{j}, J h_{j} ⟩ = \sum_{i \in I} ∥ J e_{i} ∥^{2} = \int_{X} k (x, x) d μ (x)$ .

step 1.2A4A5

2.1

Conclusion and both boundaries. Claims 1–3 are [step 1.1], [step 1.2] and [step 1.3]. For the first boundary, the diagonal $Δ$ is closed and product-measurable (a compact metric space has a countable base). If $μ$ is nonatomic, Tonelli in [A1] gives $(μ \times μ) (Δ) = \int_{X} μ ({x}) d μ (x) = 0$ . For nonzero $μ$ , the representatives $k$ and $k + 1_{Δ}$ therefore give the same $L^{2}$ class but their diagonal integrals differ by $μ (X) > 0$ . This is a failure in general, not in every measure space: on a singleton with unit mass the kernel class does determine its diagonal value. For the second boundary, here is a continuous Hermitian kernel whose operator is not trace class. For each $n \geq 1$ put $N_{n} = 2^{4 n}$ and choose the explicit finite cluster $X_{n} = {2^{- n} (1 + \frac{j}{2 N_{n}}) : 0 \leq j < N_{n}}, X = {0} \cup ⋃_{n \geq 1} X_{n} .$ The clusters are disjoint, all their points are isolated, and their only accumulation point is $0$ , so $X$ is compact. Give each point of $X_{n}$ mass $2^{- n} / N_{n}$ and give $0$ mass zero. This defines a finite Borel measure of total mass $1$ , regular because finite subsets approximate the mass of any set from inside, and complements of finite subsets of its complement approximate it from outside. Index $X_{n}$ by binary vectors $u \in {0, 1}^{4 n}$ in lexicographic order, and set $H_{n} (u, v) = (- 1)^{u \cdot v}, k (x_{u}, x_{v}) = 2^{- n} H_{n} (u, v) (x_{u}, x_{v} \in X_{n}),$ with $k = 0$ on different clusters and whenever either coordinate is $0$ . The dot product in the exponent is taken modulo $2$ . This real symmetric kernel is continuous: away from $0$ points are isolated; near $(0, 0)$ nonzero block values have modulus $2^{- n} \to 0$ ; near $(0, x)$ or $(x, 0)$ with $x \neq 0$ the kernel is eventually zero. A vector $u$ of odd parity gives $k (x_{u}, x_{u}) = - 2^{- n}$ , so the kernel is not positive semidefinite. Pairing binary vectors differing in a coordinate where $u \neq w$ shows $\sum_{v} (- 1)^{(u + w) \cdot v} = 0$ ; for $u = w$ the sum is $N_{n}$ . Thus $H_{n}^{2} = N_{n} I$ . The normalized singleton indicators form a complete orthonormal basis of this atomic $L^{2}$ space (truncating a square-summable atomic integral proves completeness). On its $X_{n}$ block the operator matrix is $2^{- n} (2^{- n} / N_{n}) H_{n} = 2^{- 6 n} H_{n}$ . Consequently $T_{k}^{*} T_{k}$ is $2^{- 8 n} I$ on that block and $∣ T_{k} ∣$ is $2^{- 4 n} I$ . The block singular values are $2^{- 4 n}$ , repeated $N_{n} = 2^{4 n}$ times. Their squared sum is $\sum_{n \geq 1} 2^{- 4 n} < \infty$ ; their sum is $\sum_{n \geq 1} 1 = \infty$ , so $T_{k}$ is not trace class by Trace class operator. Compactness follows from [A2], or directly because the block norms tend to zero and finite block truncations have finite rank. This proves the second boundary while retaining the positive-kernel conclusion: positivity supplies trace-class membership here; continuity alone does not.

step 1.1step 1.2step 1.3A1A2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

165 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 — §10.5, Lemma 10.26 and Theorem 10.27 (Mercer, printed pp. 304–306) (standard reference, not scraped)