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 be a compact Hausdorff group with normalized Haar probability measure (Normalized Haar probability on a compact group) and let be a class (Complex Haar L^p spaces and compactly supported functions). Then the left convolution on ,
is a well-defined bounded linear operator whose definition does not depend on the chosen measurable representative of and which is Hilbert–Schmidt with ; in particular 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 with normalized Haar probability , a class , and Countable Choice as a consequence of AC.
The Axiom of Choice is assumed. (The Axiom of Choice)
Assume AC. For a Radon measure on an LCH space the complex spaces and are complete, and is dense in both. (Completeness of the complex Haar L1 and L2 spaces and density of Cc)
Under AC a class of the completed product of two sigma-finite measure spaces defines a bounded kernel operator, with for every Hilbert basis, so is Hilbert–Schmidt with ; the operator is independent of the chosen representative of . (L two kernels give Hilbert–Schmidt operators)
Under Countable Choice every Hilbert–Schmidt operator is compact. (Hilbert–Schmidt operators are compact)
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)
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)
AC implies Countable Choice, the hypothesis needed for the Hilbert-space and completed-product results [F9, F10] and the compactness conclusion [F3]. (AC supplies the countable and dependent choices used in Banach integration, The Axiom of Countable Choice ())
A topological group has continuous multiplication and inversion, and a finite product of compact spaces is compact; a composite of continuous maps is continuous. (Topological group: multiplication and inversion are continuous, The product set of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, A product of finitely many compact spaces is compact in the product topology, Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous, claim 1)
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)
Under Countable Choice of a measure space is a Hilbert space for the integral pairing, so Cauchy–Schwarz holds for it ( with the integral pairing is a Hilbert space, Cauchy–Schwarz: , with equality exactly for dependent pairs).
The completed product measure is the completion of the product measure on the product sigma-algebra. (The completed product measure)
Proof
Let and put . Inversion and multiplication are continuous, so is continuous on the compact space .
For each , continuity gives an open-rectangle cover of on each member of which varies by less than ; compactness gives a finite subcover. Disjointify its rectangles by successive differences and on each nonempty piece use a value of from its rectangle. These pieces are measurable in the product sigma-algebra, so this gives a measurable simple function within of everywhere. Taking and applying pointwise-limit measurability to the real and imaginary parts shows that is product-measurable.
For fixed , the map preserves by [F5]. Tonelli applied to the measurable function therefore gives .
The map is an isometry from into of the completed product measure by step 3.1. Since is dense in and the completed-product space is complete, it extends to an isometry . Choose with and put ; then , and the class is independent of the approximating sequence.
Choose measurable representatives of and and define . For each , the change of variables preserves , so Cauchy–Schwarz makes this integral finite and gives for every continuous approximant chosen in step 4.1, uniformly in . Each is continuous: joint continuity of from step 1.1 and compactness of give as , and since . Thus is a measurable uniform limit. By [F2], and , so the uniform limit also gives as an class.
The kernel theorem [F2] makes Hilbert–Schmidt with . By step 5.1 this operator is exactly , so is bounded and has the asserted Hilbert–Schmidt norm.
If is changed on a null set , then for each the convolution integrand changes only for , since iff ; this set is null by inversion and right invariance of . Changing the representative of the input also leaves every section integral unchanged. Thus is representative-independent; since Countable Choice holds, [F3] makes this Hilbert–Schmidt operator compact.
Depends on
- The Axiom of Choice
- Normalized Haar probability on a compact group
- Left Haar integral and left Haar measure
- Complex Haar L^p spaces and compactly supported functions
- Completeness of the complex Haar L1 and L2 spaces and density of Cc
- L two kernels give Hilbert–Schmidt operators
- Hilbert–Schmidt operators are compact
- The completed product measure
- $L^2$ with the integral pairing is a Hilbert space
- Tonelli's theorem for nonnegative measurable functions on a sigma-finite product
- Cauchy–Schwarz: $|\langle x,y\rangle|\le\|x\|\,\|y\|$, with equality exactly for dependent pairs
- Integral invariance under measure-preserving maps
- AC supplies the countable and dependent choices used in Banach integration
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Topological group: multiplication and inversion are continuous
- The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space
- A product of finitely many compact spaces is compact in the product topology
- Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous
- The product sigma-algebra and its finite iterates
- Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
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
- Emmanuel Kowalski, An Introduction to the Representation Theory of Groups, §§5.2–5.6 (standard reference, not scraped)
- David Vogan, Review of Harmonic Analysis on Compact Groups, §§2.1–2.16 (standard reference, not scraped)