Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02
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² convolution on a compact group is Hilbert–Schmidt

Statement

Assume the Axiom of Choice. Let K be a compact Hausdorff group with normalized Haar probability measure μ (Normalized Haar probability on a compact group) and let f∈L2(K,μ;C) be a class (Complex Haar L^p spaces and compactly supported functions). Then the left convolution Cf on L2(K,μ;C),

(Cfh)(x)=∫Kf(xy−1)h(y) dμ(y),

is a well-defined bounded linear operator whose definition does not depend on the chosen measurable representative of f and which is Hilbert–Schmidt with ∥Cf∥HS=∥f∥2; in particular Cf is compact. The operator acts on the regular representation only; no assertion is made about integrating a convolution kernel on an arbitrary irreducible representation.

Facts & Assumptions

Given: a compact Hausdorff group K with normalized Haar probability μ, a class f∈L2(K,μ;C), and Countable Choice as a consequence of AC.

[A1]

The Axiom of Choice is assumed. (The Axiom of Choice)

[F1]

Assume AC. For a Radon measure μ on an LCH space X the complex spaces L1(X,μ;C) and L2(X,μ;C) are complete, and Cc(X;C) is dense in both. (Completeness of the complex Haar L1 and L2 spaces and density of Cc)

[F2]

Under AC a class of the completed product of two sigma-finite measure spaces defines a bounded kernel operator, with ∑e∥Tke∥2=∥k∥22 for every Hilbert basis, so Tk is Hilbert–Schmidt with ∥Tk∥HS=∥k∥2; the operator is independent of the chosen representative of k. (L two kernels give Hilbert–Schmidt operators)

[F3]

Under Countable Choice every Hilbert–Schmidt operator is compact. (Hilbert–Schmidt operators are compact)

[F4]

For sigma-finite measure spaces and a product-measurable nonnegative function the iterated integrals exist and agree with the product integral. (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product)

[F5]

The normalized Haar probability is a left Haar measure, is inversion invariant, and left translations and inversion preserve it; integrals of nonnegative measurable functions and of integrable real or complex functions are invariant under measure-preserving maps. (Normalized Haar probability on a compact group, Left Haar integral and left Haar measure, Integral invariance under measure-preserving maps)

[F6]

AC implies Countable Choice, the hypothesis needed for the Hilbert-space and completed-product L2 results [F9, F10] and the compactness conclusion [F3]. (AC supplies the countable and dependent choices used in Banach integration, The Axiom of Countable Choice (ACω))

[F8]

The product sigma-algebra is the sigma-algebra generated by measurable rectangles; pointwise limits of measurable functions are measurable. (The product sigma-algebra and its finite iterates, Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable)

[F9]

Under Countable Choice L2 of a measure space is a Hilbert space for the integral pairing, so Cauchy–Schwarz holds for it (L2 with the integral pairing is a Hilbert space, Cauchy–Schwarz: ∣⟨x,y⟩∣≤∥x∥ ∥y∥, with equality exactly for dependent pairs).

[F10]

The completed product measure is the completion of the product measure on the product sigma-algebra. (The completed product measure)

Proof

technique · direct
1.1F7

Let u∈C(K) and put qu(x,y):=u(xy−1). Inversion and multiplication are continuous, so qu is continuous on the compact space K×K.

2.1F7F8step 1.1

For each ϵ>0, continuity gives an open-rectangle cover of K×K on each member of which qu varies by less than ϵ; compactness gives a finite subcover. Disjointify its rectangles by successive differences and on each nonempty piece use a value of qu from its rectangle. These pieces are measurable in the product sigma-algebra, so this gives a measurable simple function within ϵ of qu everywhere. Taking ϵ=1/n and applying pointwise-limit measurability to the real and imaginary parts shows that qu is product-measurable.

3.1F4F5step 2.1

For fixed x, the map y↦xy−1 preserves μ by [F5]. Tonelli applied to the measurable function ∣qu∣2 therefore gives ∥qu∥L2(μ×μ)2=∫K∫K∣u(xy−1)∣2 dμ(y)dμ(x)=∥u∥22.

4.1A1F1F9F10step 3.1

The map u↦qu is an isometry from C(K) into L2 of the completed product measure by step 3.1. Since C(K) is dense in L2(K) and the completed-product L2 space is complete, it extends to an isometry U:L2(K)→L2(μ×μ‾). Choose un∈C(K) with ∥f−un∥2→0 and put κ:=Uf=lim⁡nqun; then ∥κ∥2=∥f∥2, and the class κ is independent of the approximating sequence.

5.1F2F5F7F9step 1.1step 4.1

Choose measurable representatives of f and h∈L2(K) and define Cfh(x):=∫Kf(xy−1)h(y) dμ(y). For each x, the change of variables y↦xy−1 preserves μ, so Cauchy–Schwarz makes this integral finite and gives ∣Cfh(x)−Cunh(x)∣≤∥f−un∥2∥h∥2 for every continuous approximant un chosen in step 4.1, uniformly in x. Each Cunh is continuous: joint continuity of qun from step 1.1 and compactness of K give sup⁡y∣qun(x,y)−qun(x0,y)∣→0 as x→x0, and h∈L1(K) since μ(K)=1. Thus Cfh is a measurable uniform limit. By [F2], Tqun=Cun and ∥Tqun−Tκ∥≤∥qun−κ∥2→0, so the uniform limit also gives Cfh=Tκh as an L2 class.

6.1F2step 4.1step 5.1

The kernel theorem [F2] makes Tκ Hilbert–Schmidt with ∥Tκ∥HS=∥κ∥2=∥f∥2. By step 5.1 this operator is exactly Cf, so Cf is bounded and has the asserted Hilbert–Schmidt norm.

7.1F3F5F6step 6.1∎

If f is changed on a null set N, then for each x the convolution integrand changes only for y∈N−1x, since xy−1∈N iff y∈N−1x; this set is null by inversion and right invariance of μ. Changing the representative of the input h also leaves every section integral unchanged. Thus Cf is representative-independent; since Countable Choice holds, [F3] makes this Hilbert–Schmidt operator compact.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

120 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