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.

A Hilbert–Schmidt kernel operator is compact on L two

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $(X, A, μ)$ and $(Y, B, ν)$ be sigma-finite measure spaces (Finite, sigma-finite, and semifinite measures), let $\overline{μ \times ν}$ be the completed product measure (The completed product measure), and let $k$ be a class in $L^{2} (\overline{μ \times ν}; C)$ . Then the kernel operator $T_{k} : L^{2} (ν; C) \to L^{2} (μ; C)$ of L two kernels give Hilbert–Schmidt operators is compact (Compact linear operator), and this needs no continuity of the kernel: the discontinuous kernel of A square-integrable kernel without a continuous representative is square integrable, so its integral operator is compact as well, even though the kernel has no continuous representative. Thus compactness of the integral operator here strictly extends the continuous-kernel compactness results.

Facts & Assumptions

Given: The Axiom of Choice, sigma-finite $(X, A, μ)$ and $(Y, B, ν)$ , the completed product, and $k \in L^{2} (\overline{μ \times ν}; C)$ .

[F1]

The kernel theorem supplies the bounded operator $T_{k}$ , and it supplies a Hilbert basis $E$ of $L^{2} (ν; C)$ together with the identity $\sum_{e \in E} ∥ T_{k} e ∥^{2} = ∥ k ∥_{2}^{2} < + \infty$ , the sum being a finite-subset supremum (L two kernels give Hilbert–Schmidt operators).

[F2]

A bounded operator that is Hilbert–Schmidt relative to a Hilbert basis of its domain is compact under Countable Choice (Hilbert–Schmidt operators are compact, Hilbert–Schmidt operator and Hilbert–Schmidt norm).

[F3]

The preceding example exhibits a square-integrable kernel in $L^{2} (\overline{μ \times ν}; C)$ for the square with the completed product measure that has no continuous representative (A square-integrable kernel without a continuous representative).

[F4]

Choice implies Countable Choice (The Axiom of Choice, AC supplies the countable and dependent choices used in Banach integration, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Verification

technique · direct

Given: The objects above, the kernel theorem's operator $T_{k}$ , and a Hilbert basis $E$ of $L^{2} (ν; C)$ with $\sum_{e \in E} ∥ T_{k} e ∥^{2} < + \infty$ from [F1].

1.1

By [F1] the operator $T_{k}$ is well defined and bounded, and relative to the Hilbert basis $E$ of $L^{2} (ν; C)$ its Hilbert–Schmidt square-sum is $∥ k ∥_{2}^{2} < + \infty$ ; thus $T_{k}$ is Hilbert–Schmidt relative to $E$ .

2.1

The target $L^{2} (μ; C)$ is a Hilbert space, hence a Banach space, and $T_{k}$ is compact by [F2] applied with [step 1.1], Countable Choice being available by [F4]; since $k$ was an arbitrary square-integrable kernel, every kernel operator of the pair is compact.

step 1.1F2F4

3.1

In particular, for the kernel of [F3] — square integrable, rank one, and without continuous representative — the hypotheses of [step 2.1] hold, so its integral operator is compact although the kernel is discontinuous; this is the sense in which the present compactness statement strictly extends the continuous-kernel results.

step 2.1F3

4.1

Steps 2.1 and 3.1 prove both assertions: compactness of $T_{k}$ for every square-integrable kernel over sigma-finite factors, and the specific discontinuous witness.

step 2.1step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

72 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

John Roe, Lectures on Analysis — Proposition 13.5 and Exercise 13.4, printed p. 68 (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §3.6, Lemma 3.23, printed pp. 93–94 (standard reference, not scraped)