Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedverified 2026-09-26 (gpt-6-sol)
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.

Wiener's lemma for absolutely convergent Fourier series

Statement

Assume the Axiom of Choice. If f∈A(T) and its continuous representative has f(x)≠0 for every x∈T, then 1/f∈A(T).

Facts & Assumptions

Given: The Axiom of Choice and a nowhere-zero f∈A(T).

[L1]

A(T) is a unital commutative Banach algebra (The Wiener algebra is a unital commutative Banach algebra).

[L2]

Every ℓ1(Z) coefficient sequence has a continuous uniform synthesis with exactly those Fourier coefficients (Absolutely summable Fourier coefficients give uniform convergence).

[L3]

Under the Axiom of Choice, every proper ideal in a nonzero commutative unital complex Banach algebra is contained in the kernel of a character (Maximal ideals and characters of a commutative Banach algebra, The Axiom of Choice).

[L4]

Every character on a nonzero unital complex Banach algebra is bounded and continuous (Characters on a unital Banach algebra are continuous).

Proof

technique · direct
1.1L1L2L4algebra

Let χ be a character of A(T) and put z=χ(e1). Since ene−n=1 and ∥e±n∥A=1, boundedness from [L4] applied for every n≥1 gives ∣z∣n≤∥χ∥ and ∣z∣−n≤∥χ∥, hence ∣z∣=1. By [L2], every f∈A(T) is the A-norm limit of its finite Fourier sums, so continuity from [L4] gives χ(f)=∑k∈Zf^(k)zk. Thus the characters of A(T) are exactly evaluations at points of T.

2.1L1L3step 1.1givenalgebra

If f were a nonunit, the ideal (f) would be proper, so [L3] would give a character χ with χ(f)=0. By step 1.1 this character is evaluation at a point of T, contradicting the hypothesis. Conversely, a character vanishing on an element rules out a multiplicative inverse. Thus f is a unit exactly when it has no zero on T.

3.1step 2.1algebra∎

The hypothesis makes f a unit, so its algebra inverse is the pointwise reciprocal 1/f.

Depends on

Used by

Dependency tree · two levels

18 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