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.
L two kernels give Hilbert–Schmidt operators
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let and be sigma-finite measure spaces (Finite, sigma-finite, and semifinite measures), let be their product measure (For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique), let be its completion (The completed product measure), and let be a class in . Write and for the complex spaces of the original measures, with linear in the first variable (The complex pairing is well-defined and satisfies Cauchy–Schwarz, with the integral pairing is a Hilbert space). Then:
- (representative of finite norm) there is a -measurable representative of with , and its norm equals ;
- (the kernel operator) for every the section integral converges for -almost every , agrees almost everywhere with a -measurable function, and its class in depends only on the classes of and ; the resulting map is linear and bounded with (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum);
- (exact Hilbert–Schmidt norm) every Hilbert space admits a Hilbert basis under the Axiom of Choice (Orthonormal families, complete orthonormal systems and Hilbert bases), and for every Hilbert basis of and every Hilbert basis of , the sums being finite-subset suprema (Square-summable families on an arbitrary index set and the space ); consequently is Hilbert–Schmidt relative to every such basis and (Hilbert–Schmidt operator and Hilbert–Schmidt norm, The Hilbert–Schmidt norm is basis independent).
The operator is interpreted through the representative of claim 1, and claim 2 asserts that no other choice of representative changes the resulting classes; this is the sense in which a kernel of the completed product defines an operator on the spaces of the original factors.
Facts & Assumptions
Given: The Axiom of Choice, sigma-finite and , their product and completed product , and a class .
The product measure is the unique measure on with on measurable rectangles and is sigma-finite; the completed product is its completion, so it is a complete measure extending and agrees with on every -measurable set (For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique, The completed product measure, Assuming countable choice, every measure space has a unique complete extension to its completion).
Tonelli applies to a nonnegative -measurable function : the section-integral function is measurable and ; sections of -measurable sets are measurable, is countably additive and monotone, and a nonnegative measurable function has zero integral exactly when it vanishes almost everywhere (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Every section of a product-measurable set is measurable, A nonnegative measurable function has integral exactly when it vanishes almost everywhere).
Fubini applies to every : for -almost every the section is -integrable, the section integrals form a -integrable function after zero extension, and the iterated integral equals (Fubini's theorem for L^1 functions on a sigma-finite product).
On complex the pairing is representative-independent, linear in the first variable, conjugate-symmetric and positive definite, satisfies Cauchy–Schwarz, and complex of a measure space is a Hilbert space under Countable Choice (The complex pairing is well-defined and satisfies Cauchy–Schwarz, with the integral pairing is a Hilbert space).
Finite complex simple functions with finite-measure nonzero sets are dense in complex (Complex finite-simple and smooth compact-support density for finite p).
Finite complex linear combinations of finite-measure rectangle kernels are dense in and in (Product rectangle kernels are dense in product L two).
Under Countable Choice every -measurable real function agrees -almost everywhere with an -measurable function (A function measurable for a completion is almost everywhere equal to one measurable for the original sigma-algebra).
The nonnegative integral is the supremum of the integrals of the nonnegative simple functions it dominates, and the integral of a nonnegative simple function is the corresponding finite sum of set values (The nonnegative Lebesgue integral, The integral of a nonnegative simple function).
For a Hilbert basis of a Hilbert space and in it, , and the finite-subset net of partial sums converges to (Parseval equivalences for an orthonormal family, Fourier expansion in a Hilbert space).
For an orthonormal family in an inner-product space and in it, ; if lies in the span of a finite orthonormal family , then (the finite Parseval identity) (The Bessel inequality for an arbitrary orthonormal family, The finite Bessel inequality and best approximation by a finite orthonormal family).
Assuming Choice, every nonempty poset in which every chain has an upper bound has a maximal element; and in a Hilbert space a proper closed subspace has a nonzero orthogonal vector, every vector decomposing as with in the subspace and orthogonal to it (Zorn's lemma, Orthogonal decomposition by a closed subspace).
Choice implies Countable Choice and Dependent Choice; Countable Choice is the hypothesis consumed by the completion-representative interface, the Hilbert structure of , and Parseval, and Riesz representation supplies the Hilbert adjoint with (AC supplies the countable and dependent choices used in Banach integration, The Axiom of Countable Choice (), The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).
A pointwise almost-everywhere limit of a sequence of measurable functions is measurable when represented by its limit superior (Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable).
The operator is Hilbert–Schmidt relative to a Hilbert basis of exactly when , its Hilbert–Schmidt norm is then the square root of that sum, and the finiteness and the value are independent of (Hilbert–Schmidt operator and Hilbert–Schmidt norm, The Hilbert–Schmidt norm is basis independent).
Proof
Given: Choice, sigma-finite , , the product measure with completion , a class , and the complex spaces , with their first-variable-linear pairings.
Hilbert bases exist. For a real or complex Hilbert space , let be the set of orthonormal subsets of ordered by inclusion; is nonempty because is orthonormal, and the union of a chain in is orthonormal, because any two of its elements already lie in a common member of the chain, so it is an upper bound. By [F12] there is a maximal element . If the closed linear span of were a proper closed subspace, then [F12] applied to some would give with and orthogonal to and ; then would satisfy and be orthogonal to every element of , so would be an orthonormal set strictly containing , contradicting maximality; hence and is a Hilbert basis of . In particular and , being Hilbert spaces by [F5], admit Hilbert bases.
A base-measurable representative with the same norm. Apply [F8] to the real and imaginary parts of and replace infinite values of the resulting representatives by ; combining them gives an -measurable complex function with -almost everywhere. Then is -measurable and nonnegative. For every nonnegative simple -measurable , the integrals against and agree, because the two measures agree on the finitely many base-measurable level sets occurring in by [F2] and [F9]. Conversely, let be a nonnegative -measurable simple function and write its positive-level representation as , where the and the completed-measurable sets are pairwise disjoint. By the definition of the completion, write , where is -measurable and is contained in a base-measurable -null set. Since , the sets remain pairwise disjoint, and is a base-measurable simple function satisfying . Moreover [F2] and [F9] give . Thus every completed-simple minorant contributes the value of a base-simple minorant, while every base-simple minorant is also completed-simple; the two suprema in [F9] coincide and . Finally -almost everywhere, so the norm of the class gives . Hence and .
Almost every section is square integrable. By [F3] applied to the nonnegative function , whose integral is by [step 1.2], the function is measurable with finite integral; hence for -almost every , and .
The section integral exists almost everywhere and is bounded by the section norm. Let . For every with the section is -measurable by [F3] and is -measurable, so is -measurable, and Cauchy–Schwarz in by [F5] gives together with . By [step 2.1] these estimates hold for -almost every , which is where is defined.
Measurability. If is a finite simple function with , then for every the indicator lies in because , so [step 3.1] applied to it shows that the integral is defined and finite for -almost every . It is also -measurable: the four nonnegative functions , where is -measurable, have -measurable section integrals by Tonelli [F3], and on the conull set where the integral of is finite the real and imaginary parts of that integral are differences of these measurable functions, so zero-extension over the exceptional null set makes the section-integral function measurable; a finite linear combination of these is -measurable, so is -measurable for such . For arbitrary , [F6] gives finite simple functions with ; by [step 3.1], for -almost every , so agrees -almost everywhere with the limit superior of the measurable functions , which is -measurable by [F14].
Independence of representatives and linearity. If -almost everywhere then -almost everywhere for every , so wherever both are defined, in particular -almost everywhere. If is a second -measurable representative of of finite norm, then has -integral , so [F3] gives for -almost every , hence the sections agree -almost everywhere for -almost every and -almost everywhere; linearity in is linearity of the integral.
The orthonormal family of product kernels and the pairing identity. Fix a Hilbert basis of and a Hilbert basis of , both of which exist by [step 1.1], and for , let be the class in of ; this function is -measurable with by Tonelli [F3], and for , the pairing vanishes unless and , again by [F3]; so is an orthonormal family in . Moreover , where the middle equality is Fubini [F4] applied to the function , whose absolute value has -integral at most by Cauchy–Schwarz and Tonelli [F3], [F5].
Boundedness. For , the class of is in and by [step 2.1] and [step 3.1], using measurability from [step 4.1] to integrate the squared estimate; hence is linear and bounded with by [step 1.2].
Rectangle kernels lie in the closed span of the family. Let , have finite measure, so and ; by [F10] the finite-subset nets over finite and over finite converge to and . For such finite the function with and is a finite linear combination of the functions , hence its class lies in the span of the family ; and by Tonelli [F3] and convergence of the two nets, so the rectangle kernel lies in the closed span of .
The kernel lies in that closed span. By [step 5.2] and [F7] every class of — in particular , whose class exists by [step 1.2] — lies in the closed span of the orthonormal family .
Exact norm of the family expansion. Bessel's inequality [F11] applied to and the orthonormal family gives . For the reverse inequality fix a real and, by [step 6.1], a vector in the span of finitely many with ; if then is the zero class and both sides vanish, and otherwise for small and the finite Parseval identity and Cauchy–Schwarz on the finitely many coefficients give , where the last bound uses and and tends to as ; hence by [step 1.2].
Transfer to the basis sums. For each the vector lies in by [step 5.1], so [F10] applied with the Hilbert basis gives , and [step 4.3] identifies each summand with ; since every finite subset of is contained in a rectangle and all terms are nonnegative, taking suprema over finite subsets gives by [step 7.1]. The same computation with the roles of and interchanged, using the adjoint identity of [F13] and Parseval with respect to applied to the vectors , gives as well.
Conclusion. The bases and in [step 8.1] were arbitrary Hilbert bases of and , and by [step 1.1] such bases exist; by [step 8.1] every one of them realizes the value , so by [F15] the operator is Hilbert–Schmidt with , the operator itself being independent of the representative by [step 4.2] and bounded with by [step 5.1]. This proves all three claims.
Depends on
- Hilbert–Schmidt operator and Hilbert–Schmidt norm
- The Hilbert–Schmidt norm is basis independent
- Hilbert space
- Square-summable families on an arbitrary index set and the space $\ell^2(I)$
- Orthonormal families, complete orthonormal systems and Hilbert bases
- Finite, sigma-finite, and semifinite measures
- For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique
- The completed product measure
- Assuming countable choice, every measure space has a unique complete extension to its completion
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Fubini's theorem for L^1 functions on a sigma-finite product
- Every section of a product-measurable set is measurable
- A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere
- The nonnegative Lebesgue integral
- The integral of a nonnegative simple function
- The complex $L^2$ pairing is well-defined and satisfies Cauchy–Schwarz
- $L^2$ with the integral pairing is a Hilbert space
- Complex finite-simple and smooth compact-support density for finite p
- Product rectangle kernels are dense in product L two
- A function measurable for a completion is almost everywhere equal to one measurable for the original sigma-algebra
- Parseval equivalences for an orthonormal family
- Fourier expansion in a Hilbert space
- The Bessel inequality for an arbitrary orthonormal family
- The finite Bessel inequality and best approximation by a finite orthonormal family
- Zorn's lemma
- Orthogonal decomposition by a closed subspace
- The Hilbert-space adjoint of a bounded operator
- Hilbert-adjoint identities
- Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
- The Axiom of Choice
- AC supplies the countable and dependent choices used in Banach integration
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- A bounded linear operator between normed spaces
- The operator norm as the least bound and as the unit-sphere or unit-ball supremum
Used by
- A Hilbert–Schmidt kernel operator is compact on L two Example
- A square-integrable separable product kernel Example
- Finite-rank truncations of a square-integrable kernel Example
- Integral operator trace under a valid diagonal hypothesis Example
- Volterra operator is Hilbert Schmidt and quasinilpotent Example
- Continuous convolution operators are Hilbert–Schmidt Lemma
Dependency tree · two levels
134 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 — Lecture 13, Proposition 13.5, printed pp. 67–68 (standard reference, not scraped)
- Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §3.6, Lemma 3.23 and the matrix-coefficient characterization, printed pp. 93–95 (standard reference, not scraped)
- Sheldon Axler, Measure, Integration & Real Analysis — product-measure Fubini/Tonelli and Lp approximation, §§7A, 10C (standard reference, not scraped)