Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

Spectral convolution eigenspaces are finite-dimensional and invariant

Statement

Assume the Axiom of Choice. Let G be a compact Lie group and kC(G).

  1. The Hilbert adjoint of Tk is Tk with k(x)=k(x1), and Tk commutes with every left translation Lg.
  2. If k=k, then Tk is compact self-adjoint, its nonzero eigenspaces are finite-dimensional and left-invariant, and the closed span of the eigenspaces is the closure of the range of Tk.
  3. For arbitrary k the operator TkTk is compact, positive and self-adjoint; its nonzero eigenspaces are finite-dimensional and left-invariant, and their closed span is ran(TkTk)=(ker(TkTk)).

Facts & Assumptions

Given: Assume the Axiom of Choice, a compact Lie group G with normalized Haar measure, and kC(G).

[A1]

The Axiom of Choice is The Axiom of Choice; it enters through the compactness and spectral theory cited.

[L1]

Tk is a compact operator on L2(G) with kernel K(x,y)=k(x1y); the left and right regular representations are unitary and satisfy LgRh=RhLg (Continuous convolution operators are Hilbert–Schmidt, Left and right regular representations on L2(G)).

[L2]

Hilbert adjoints satisfy (TS)=ST, T=T and TT=T2; for a compact self-adjoint operator the set of nonzero eigenvalues consists of real numbers with finite-dimensional eigenspaces and the closed span of the eigenspaces is the orthogonal complement of the kernel, equal to the closure of the range (Hilbert-adjoint identities, Spectral theorem for compact self adjoint operators).

[L3]

Integrals are invariant under left translation (Haar integration is translation and conjugation invariant), and Fubini applies to integrable functions on the finite product measure space (Fubini's theorem for L^1 functions on a sigma-finite product).

[L4]

The complex L2 pairing is linear in its first variable and satisfies Cauchy–Schwarz (The complex L2 pairing is well-defined and satisfies Cauchy–Schwarz).

Proof

technique · direct
1.1

Since Haar measure has mass one, [L4] applied to f,1 gives f1f2, and similarly for h. Thus k(x1y)f(y)h(x) is absolutely integrable, with integral of its modulus at most kf1h1. Fubini gives Tkf,h=Gf(y)Gk(x1y)h(x)dxdy=f,Tkh, because k(y1x)=k(x1y). The continuous function k defines a bounded operator by [L1], so uniqueness of the adjoint gives Tk=Tk. No substitution reversing the two kernel arguments is made.

A1L1L2L3L4
1.2

For gG, (LgTkf)(x)=Gk(x1gy)f(y)dy. Substituting u=gy, using left invariance, gives Gk(x1u)f(g1u)du=(TkLgf)(x). Hence LgTk=TkLg.

L1L3
2.1

If k=k, step 1.1 makes Tk self-adjoint. Compactness [L1] and the spectral theorem [L2] give finite-dimensional nonzero eigenspaces whose closed span is (kerTk)=ranTk. If Tkv=λv, step 1.2 gives TkLgv=λLgv; applying this also to g1 proves invariance of the eigenspace. The standing AC assumption supplies the countable choice required by the spectral theorem.

A1L1L2step 1.1step 1.2
3.1

Put S=TkTk. The adjoint identities give S=TkTk=S, and Sf,f=Tkf220. It is compact: the image under Tk of the unit ball has compact closure, and its image under the bounded, hence continuous, operator Tk is compact and contains S of that ball. By steps 1.1–1.2, both factors commute with every Lg, so S does too. Apply the compact self-adjoint spectral theorem directly to S: its nonzero eigenspaces are finite-dimensional, and their closed span is (kerS)=ranS. Commutation and the inverse translation prove their left invariance exactly as for Tk. If k=0, both operators vanish and the nonzero-eigenspace family is empty with closed span {0}; no finite-dimensionality assertion is made about a zero eigenspace.

A1L1L2L4step 1.1step 1.2

Depends on

Used by

Dependency tree · two levels

73 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