Alphabeta Math
TheoremStatement: AI-adaptedProof: 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.

L two kernels give Hilbert–Schmidt operators

Statement

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 μ×ν 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 k be a class in L2(μ×ν;C). Write L2(ν;C) and L2(μ;C) for the complex L2 spaces of the original measures, with f,g=fg linear in the first variable (The complex L2 pairing is well-defined and satisfies Cauchy–Schwarz, L2 with the integral pairing is a Hilbert space). Then:

  1. (representative of finite norm) there is a (AB)-measurable representative k0 of k with k02d(μ×ν)<+, and its norm equals k2;
  2. (the kernel operator) for every fL2(ν;C) the section integral (Tkf)(x):=Yk0(x,y)f(y)dν(y) converges for μ-almost every x, agrees almost everywhere with a μ-measurable function, and its class in L2(μ;C) depends only on the classes of f and k; the resulting map Tk:L2(ν;C)L2(μ;C) is linear and bounded with Tkk2 (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum);
  3. (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 E of L2(ν;C) and every Hilbert basis F of L2(μ;C), eETke2=fFTkf2=k22, the sums being finite-subset suprema (Square-summable families on an arbitrary index set and the space 2(I)); consequently Tk is Hilbert–Schmidt relative to every such basis and TkHS=k2 (Hilbert–Schmidt operator and Hilbert–Schmidt norm, The Hilbert–Schmidt norm is basis independent).

The operator is interpreted through the representative k0 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 L2 spaces of the original factors.

Facts & Assumptions

Given: The Axiom of Choice, sigma-finite (X,A,μ) and (Y,B,ν), their product ρ:=μ×ν and completed product ρ, and a class kL2(ρ;C).

[F2]

The product measure is the unique measure on AB with (μ×ν)(A×B)=μ(A)ν(B) 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 (AB)-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).

[F3]

Tonelli applies to a nonnegative (AB)-measurable function g: the section-integral function is measurable and gdρ=X(Ygxdν)dμ; sections of (AB)-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 0 exactly when it vanishes almost everywhere).

[F4]

Fubini applies to every gL1(ρ;C): for μ-almost every x the section gx is ν-integrable, the section integrals form a μ-integrable function after zero extension, and the iterated integral equals gdρ (Fubini's theorem for L^1 functions on a sigma-finite product).

[F5]

On complex L2 the pairing h1,h2=h1h2 is representative-independent, linear in the first variable, conjugate-symmetric and positive definite, satisfies Cauchy–Schwarz, and complex L2 of a measure space is a Hilbert space under Countable Choice (The complex L2 pairing is well-defined and satisfies Cauchy–Schwarz, L2 with the integral pairing is a Hilbert space).

[F6]

Finite complex simple functions with finite-measure nonzero sets are dense in complex L2 (Complex finite-simple and smooth compact-support density for finite p).

[F7]

Finite complex linear combinations of finite-measure rectangle kernels are dense in L2(ρ;C) and in L2(ρ;C) (Product rectangle kernels are dense in product L two).

[F8]

Under Countable Choice every ρ-measurable real function agrees ρ-almost everywhere with an (AB)-measurable function (A function measurable for a completion is almost everywhere equal to one measurable for the original sigma-algebra).

[F9]

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).

[F10]

For a Hilbert basis G of a Hilbert space and h in it, h2=gGh,g2, and the finite-subset net of partial sums converges to h (Parseval equivalences for an orthonormal family, Fourier expansion in a Hilbert space).

[F11]

For an orthonormal family (ψi) in an inner-product space and h in it, ih,ψi2h2; if h lies in the span of a finite orthonormal family A, then ψAh,ψ2=h2 (the finite Parseval identity) (The Bessel inequality for an arbitrary orthonormal family, The finite Bessel inequality and best approximation by a finite orthonormal family).

[F12]

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 h=m+n with m in the subspace and n orthogonal to it (Zorn's lemma, Orthogonal decomposition by a closed subspace).

[F13]

Choice implies Countable Choice and Dependent Choice; Countable Choice is the hypothesis consumed by the completion-representative interface, the Hilbert structure of L2, and Parseval, and Riesz representation supplies the Hilbert adjoint Tk with Tke,f=e,Tkf (AC supplies the countable and dependent choices used in Banach integration, The Axiom of Countable Choice (ACω), The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).

[F14]

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).

[F15]

The operator Tk is Hilbert–Schmidt relative to a Hilbert basis G of L2(ν;C) exactly when eGTke2<+, its Hilbert–Schmidt norm is then the square root of that sum, and the finiteness and the value are independent of G (Hilbert–Schmidt operator and Hilbert–Schmidt norm, The Hilbert–Schmidt norm is basis independent).

Proof

technique · direct

Given: Choice, sigma-finite (X,A,μ), (Y,B,ν), the product measure ρ=μ×ν with completion ρ, a class kL2(ρ;C), and the complex L2 spaces L2(ν;C), L2(μ;C) with their first-variable-linear pairings.

1.1

Hilbert bases exist. For a real or complex Hilbert space H, let P be the set of orthonormal subsets of H ordered by inclusion; P is nonempty because is orthonormal, and the union of a chain in P 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 E. If the closed linear span M of E were a proper closed subspace, then [F12] applied to some xM would give x=m+n with mM and n orthogonal to M and n0; then e:=n/n would satisfy e=1 and be orthogonal to every element of EM, so E{e} would be an orthonormal set strictly containing E, contradicting maximality; hence M=H and E is a Hilbert basis of H. In particular L2(ν;C) and L2(μ;C), being Hilbert spaces by [F5], admit Hilbert bases.

F5F12F13
1.2

A base-measurable representative with the same norm. Apply [F8] to the real and imaginary parts of k and replace infinite values of the resulting representatives by 0; combining them gives an (AB)-measurable complex function k0 with k0=k ρ-almost everywhere. Then g:=k02 is (AB)-measurable and nonnegative. For every nonnegative simple (AB)-measurable sg, the integrals against ρ and ρ agree, because the two measures agree on the finitely many base-measurable level sets occurring in s by [F2] and [F9]. Conversely, let tg be a nonnegative ρ-measurable simple function and write its positive-level representation as t=j=1mcj1Ej, where the cj>0 and the completed-measurable sets Ej are pairwise disjoint. By the definition of the completion, write Ej=AjNj, where Aj is (AB)-measurable and Nj is contained in a base-measurable ρ-null set. Since AjEj, the sets Aj remain pairwise disjoint, and s:=j=1mcj1Aj is a base-measurable simple function satisfying 0stg. Moreover [F2] and [F9] give sdρ=jcjρ(Aj)=jcjρ(Ej)=tdρ. 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 gdρ=gdρ. Finally k0=k ρ-almost everywhere, so the norm of the class k gives gdρ=k2dρ<+. Hence k0L2(ρ;C) and k0L2(ρ)=k2.

F2F8F9F13
2.1

Almost every section is square integrable. By [F3] applied to the nonnegative function (x,y)k0(x,y)2, whose integral is k0L2(ρ)2<+ by [step 1.2], the function xYk0(x,y)2dν(y) is measurable with finite integral; hence k0(x,)L2(ν)<+ for μ-almost every x, and Xk0(x,)L2(ν)2dμ(x)=k0L2(ρ)2.

step 1.2F3
3.1

The section integral exists almost everywhere and is bounded by the section norm. Let fL2(ν;C). For every x with k0(x,)L2(ν)<+ the section k0(x,) is B-measurable by [F3] and f is ν-measurable, so yk0(x,y)f(y) is ν-measurable, and Cauchy–Schwarz in L2(ν) by [F5] gives Yk0(x,y)f(y)dν(y)k0(x,)L2(ν)fL2(ν)<+ together with (Tk0f)(x)=Yk0(x,y)f(y)dν(y)k0(x,)L2(ν)fL2(ν). By [step 2.1] these estimates hold for μ-almost every x, which is where (Tk0f)(x) is defined.

step 2.1F3F5
4.1

Measurability. If f=j<mcj1Bj is a finite simple function with ν(Bj)<+, then for every j the indicator 1Bj lies in L2(ν;C) because ν(Bj)<+, so [step 3.1] applied to it shows that the integral xYk0(x,y)1Bj(y)dν(y) is defined and finite for μ-almost every x. It is also μ-measurable: the four nonnegative functions (Regj)+,(Regj),(Imgj)+,(Imgj), where gj(x,y):=k0(x,y)1Bj(y) is (AB)-measurable, have μ-measurable section integrals by Tonelli [F3], and on the conull set where the integral of gj 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 Tk0f is μ-measurable for such f. For arbitrary fL2(ν;C), [F6] gives finite simple functions fj with fjfL2(ν)0; by [step 3.1], Tk0(fjf)(x)k0(x,)L2(ν)fjfL2(ν)0 for μ-almost every x, so Tk0f agrees μ-almost everywhere with the limit superior of the measurable functions Tk0fj, which is μ-measurable by [F14].

step 3.1F3F5F6F14
4.2

Independence of representatives and linearity. If f=f ν-almost everywhere then k0(x,)(ff)=0 ν-almost everywhere for every x, so Tk0f=Tk0f wherever both are defined, in particular μ-almost everywhere. If k1 is a second (AB)-measurable representative of k of finite L2(ρ) norm, then k0k1 has ρ-integral 0, so [F3] gives Yk0(x,y)k1(x,y)dν(y)=0 for μ-almost every x, hence the sections agree ν-almost everywhere for μ-almost every x and Tk0f=Tk1f μ-almost everywhere; linearity in f is linearity of the integral.

step 3.1F3F5
4.3

The orthonormal family of product kernels and the pairing identity. Fix a Hilbert basis E of L2(ν;C) and a Hilbert basis F of L2(μ;C), both of which exist by [step 1.1], and for fF, eE let ψf,e be the class in L2(ρ;C) of (x,y)f(x)e(y); this function is (AB)-measurable with ψf,eL2(ρ)2=fL2(μ)2eL2(ν)2=1 by Tonelli [F3], and for f,fF, e,eE the pairing ψf,e,ψf,e=XffdμYeedν=f,fL2(μ)e,eL2(ν) vanishes unless f=f and e=e, again by [F3]; so (ψf,e) is an orthonormal family in L2(ρ;C). Moreover Tke,fL2(μ)=X(Yk0(x,y)e(y)dν(y))f(x)dμ(x)=X×Yk0(x,y)e(y)f(x)dρ(x,y)=k,ψf,eL2(ρ), where the middle equality is Fubini [F4] applied to the L1(ρ) function (x,y)k0(x,y)e(y)f(x), whose absolute value has ρ-integral at most k0L2(ρ)eL2(ν)fL2(μ) by Cauchy–Schwarz and Tonelli [F3], [F5].

step 1.1step 3.1F3F4F5
5.1

Boundedness. For fL2(ν;C), the class of Tk0f is in L2(μ;C) and Tk0fL2(μ)2=X(Tk0f)(x)2dμ(x)Xk0(x,)L2(ν)2dμ(x)fL2(ν)2=k0L2(ρ)2fL2(ν)2 by [step 2.1] and [step 3.1], using measurability from [step 4.1] to integrate the squared estimate; hence Tk:=Tk0 is linear and bounded with Tkk0L2(ρ)=k2 by [step 1.2].

step 1.2step 2.1step 3.1step 4.1
5.2

Rectangle kernels lie in the closed span of the family. Let AA, BB have finite measure, so 1AL2(μ;C) and 1BL2(ν;C); by [F10] the finite-subset nets fG1A,ff over finite GF and eH1B,ee over finite HE converge to 1A and 1B. For such finite G,H the function uG(x)vH(y) with uG:=fG1A,ff and vH:=eH1B,ee is a finite linear combination of the functions f(x)e(y), hence its class lies in the span of the family (ψf,e); and uvuGvHL2(ρ)uL2(μ)vvHL2(ν)+uuGL2(μ)vHL2(ν)0 by Tonelli [F3] and convergence of the two nets, so the rectangle kernel 1A(x)1B(y)=1A(x)1B(y) lies in the closed span of (ψf,e).

step 4.3F3F10
6.1

The kernel lies in that closed span. By [step 5.2] and [F7] every class of L2(ρ;C) — in particular k0, whose L2(ρ) class exists by [step 1.2] — lies in the closed span of the orthonormal family (ψf,e).

step 1.2step 5.2F7
7.1

Exact norm of the family expansion. Bessel's inequality [F11] applied to k0 and the orthonormal family (ψf,e) gives f,ek0,ψf,e2k0L2(ρ)2. For the reverse inequality fix a real ε>0 and, by [step 6.1], a vector h in the span of finitely many ψf,e with hk0L2(ρ)<ε; if k0L2(ρ)=0 then k0 is the zero class and both sides vanish, and otherwise h0 for small ε and the finite Parseval identity and Cauchy–Schwarz on the finitely many coefficients give f,ek0,ψf,e2k0,h2/hL2(ρ)2k0L2(ρ)2(k0L2(ρ)ε)2/(k0L2(ρ)+ε)2, where the last bound uses k0,hk02k0ε and hk0+ε and tends to k0L2(ρ)2 as ε0; hence f,ek0,ψf,e2=k0L2(ρ)2=k22 by [step 1.2].

step 1.2step 6.1F11
8.1

Transfer to the basis sums. For each eE the vector Tke lies in L2(μ;C) by [step 5.1], so [F10] applied with the Hilbert basis F gives TkeL2(μ)2=fFTke,f2, and [step 4.3] identifies each summand with k0,ψf,e2; since every finite subset of E×F is contained in a rectangle and all terms are nonnegative, taking suprema over finite subsets gives eETke2=f,ek0,ψf,e2=k22 by [step 7.1]. The same computation with the roles of E and F interchanged, using the adjoint identity Tke,f=e,Tkf of [F13] and Parseval with respect to E applied to the vectors Tkf, gives fFTkf2=k22 as well.

step 5.1step 4.3step 7.1F10F13
9.1

Conclusion. The bases E and F in [step 8.1] were arbitrary Hilbert bases of L2(ν;C) and L2(μ;C), and by [step 1.1] such bases exist; by [step 8.1] every one of them realizes the value k22, so by [F15] the operator Tk is Hilbert–Schmidt with TkHS=k2, the operator itself being independent of the representative k0 by [step 4.2] and bounded with Tkk2 by [step 5.1]. This proves all three claims.

step 1.1step 4.2step 5.1step 8.1F15

Depends on

Used by

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