Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated
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.

Fourier transform as the Gelfand transform of an LCA group algebra

Example

Assume the Axiom of Choice. Let G be a locally compact Hausdorff abelian group with a fixed nonzero Haar measure m. With convolution and conjugate-reflection as in Scalar unitisation of L1 of an LCA group: characters, spectrum and identity criterion, the space A=L1(G,m;C) is a commutative Banach star algebra, unital exactly when G is discrete. These analytical assertions are proved in the cited lemma; AC implies the Dependent Choice used there.

For nondiscrete G, put B=C⊕A and set ∥(z,f)∥=∣z∣+∥f∥1,(z,f)(v,g)=(zv,zg+vf+f∗g),(z,f)∗=(z‾,f∗). Then B is a commutative unital Banach star algebra. Under the proved identification of Δ(B) with the one-point compactification of G^, its Gelfand transform is ΓB(z,f)(hw)=z+f^(w),f^(w)=∫Gf(t)w(t) dm(t),ΓB(z,f)(q)=z. The cited lemma uses the conjugate-phase convention: here hw=hw‾+, since w(t)‾‾=w(t). Conjugation w↦w‾ is a homeomorphism of the compact-open dual, so this reparametrization preserves the asserted topology. Thus the Fourier transform with this character convention is precisely the restriction of ΓB(0,f) to G^. No C-star norm assertion is made.

Facts & Assumptions

Given: The Axiom of Choice, G,m,A and, in the nondiscrete case, B as displayed.

[F1]

The L1 convolution algebra, norm and involution facts, the unit criterion, and the complete character/topology identification for B are proved in the scalar-unitization lemma (Scalar unitisation of L1 of an LCA group: characters, spectrum and identity criterion).

[F2]

For a commutative unital complex algebra the Gelfand transform is ΓB(b)(χ)=χ(b) (Gelfand transform).

Verification

1.1F1F3givenalgebra

For b=(z,f) and c=(v,g), the norm estimate in [F1] gives ∥bc∥≤∣zv∣+∣z∣∥g∥1+∣v∣∥f∥1+∥f∥1∥g∥1=(∣z∣+∥f∥1)(∣v∣+∥g∥1). A Cauchy sequence in B has Cauchy scalar and A coordinates; completeness of C from [F3] and of A from [F1] makes it converge in the sum norm.

2.1F1step 1.1givenalgebra

Bilinearity and commutativity follow from [F1], and (1,0) is the identity. For b=(z,f), c=(v,g) and d=(u,k), either bracketing of bcd has scalar part zvu and A part zvk+zug+vuf+z(g∗k)+v(f∗k)+u(f∗g)+(f∗g)∗k, by convolution associativity. Conjugate-linearity, involutivity and isometry of the star follow coordinatewise from [F1]; expanding the product and applying (f∗g)∗=g∗∗f∗ gives (bc)∗=c∗b∗.

3.1F1F2step 2.1algebra∎

In the conjugate-phase notation of [F1], set γ=w‾. Then hγ+(z,f)=z+∫Gf(t)γ(t)‾ dm(t)=hw(z,f). The map w↦w‾ is its own inverse and preserves uniform convergence on each compact set, hence is a homeomorphism of the compact-open dual. Therefore [F1] makes every character of B one of the displayed hw or q, with the asserted topology. Applying [F2] gives ΓB(z,f)(hw)=hw(z,f)=z+f^(w) and ΓB(z,f)(q)=q(z,f)=z. Taking z=0 and restricting to the dual gives the Fourier/Gelfand identity.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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