Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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 inversion for integrable transforms on LCA groups

Statement

Assume the Axiom of Choice and Dependent Choice. Let G be a locally compact Hausdorff abelian group with Haar measure mG and dual G^ equipped with the compatible dual Haar normalisation proved earlier on this page. If f∈L1(G,mG) and f^∈L1(G^,mG^), then ∫G^f^(γ) γ(x) dmG^(γ) converges absolutely for every x∈G and defines a bounded uniformly continuous function f∨∈L∞(G,mG), and f∨=f mG-almost everywhere. Consequently the class of f has a unique continuous representative, namely f∨, and at every point x at which a chosen representative of f is continuous one has f∨(x)=f(x). No pointwise statement is made at the remaining points of an arbitrary representative.

Facts & Assumptions

Given: The Axiom of Choice and Dependent Choice, a locally compact Hausdorff abelian group G with Haar measure mG, the compatible dual Haar measure mG^ on G^, and f∈L1(G,mG) with f^∈L1(G^,mG^).

[F1]

The compatible dual Haar normalisation gives inversion, with integrable transform, for every element of its declared core; in particular for every q=g∗g~ with real g∈Cc(G;R) one has q(x)=∫G^q^(γ)γ(x) dmG^(γ) for mG-almost every x, and q^∈L1(G^,mG^) (Compatible dual Haar normalisation). Such squares are continuous with compact support and lie in L1∩L2; they also belong to the complex-generator core E of Positive convolution squares form a dense inversion core.

[F2]

The Fourier transform is linear with ∣u^(γ)∣≤∥u∥1, takes L1(G) into C0(G^), and satisfies u∗v^=u^v^ and u∗^=u^‾ (The Fourier transform on an LCA group, Riemann-Lebesgue lemma on LCA groups, Fourier transform intertwines translation, modulation and convolution); real Cc(G) is dense in real L1(G,mG), and approximation of real and imaginary parts separately makes Cc(G;C) dense in complex L1 (C_c(X) is dense in L^p(mu) for a Radon measure, The space Lp(μ) as the quotient by null functions).

[F4]

The dual G^ is locally compact Hausdorff (The dual of a locally compact abelian group is locally compact abelian), so real Cc(G^) is dense in real L1(G^,mG^) by the Cc density theorem (C_c(X) is dense in L^p(mu) for a Radon measure). Thus every v∈L1(G^) has arbitrarily small tails outside a compact set: approximate ∣v∣ in real L1 by a compactly supported continuous function. Character evaluation is jointly continuous (Evaluation of characters is jointly continuous, The Pontryagin dual with the compact-open topology); Haar measure is positive on nonempty open sets and finite on compact sets (Haar measure is positive on nonempty open sets and finite on compact sets).

[F5]

The elements of L1(G,mG) are equivalence classes, so pointwise statements require a representative (The space Lp(μ) as the quotient by null functions).

[F6]

The translation/approximate-identity supplier proves ∥r∗f∥1≤∥r∥1∥f∥1 and ∥q∗f−f∥1≤∫q(y)∥Tyf−f∥1 dmG(y)≤sup⁡y∈supp⁡q∥Tyf−f∥1 for compactly supported r and nonnegative mass-one q. Its proof restricts the kernel variable to compact K and the output variable to S+K, where f is represented as zero off a σ-compact essential support S; for the difference estimate use S∪(S+K). These restrictions are σ-finite, so Minkowski applies there and the functions extend by zero to G. Translation continuity then gives the approximate-identity limits without assuming globally σ-finite Haar measure. Use all admissible pairs i=(U,u), putting ui=u and Ui=U; for symmetric real ui, qi=ui∗ui~ is a positive-core generator, and Tonelli on compact kernel supports gives ∫qi=(∫ui)2=1 (Translation continuity and normalised local approximate identities on an LCA group, Minkowski's integral inequality, Positive convolution squares form a dense inversion core, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F7]

Under Countable Choice, norm convergence in L1 admits an almost-everywhere convergent subsequence on any measure space (Riesz-Fischer completeness of Lp for 1≤p≤∞). This applies to complex functions by applying the real result successively to their real and imaginary parts. For a countable sequence, replacing the supplied representatives by any specified representatives changes the convergence only on a countable union of null sets. The assumed Axiom of Choice supplies the countable selections below.

[F8]

Each integrable scalar function for a Haar measure on an LCH group has a σ-compact essential support: its positive level sets have finite measure, outer regularity puts them in finite-measure open sets, and inner regularity exhausts those open sets up to null sets by countably many compact sets. The assumed choice principles supply these countable selections. Haar measure is finite on compact sets, so two such supports give a σ-finite product. Fubini applies to an absolutely integrable product-measurable complex kernel on that product (Radon measure on an LCH space, Haar measure is positive on nonempty open sets and finite on compact sets, Fubini's theorem for L^1 functions on a sigma-finite product).

Proof

technique · direct
1.1F1F2

(Absolute convergence and the L∞ bound.) Since ∣f^(γ)γ(x)∣=∣f^(γ)∣ and f^∈L1(G^,mG^), the integral defining f∨(x):=∫G^f^(γ)γ(x) dmG^(γ) converges absolutely for every x and ∥f∨∥∞≤∥f^∥L1(G^,mG^); thus f∨∈L∞(G,mG).

1.2F2F4

(Uniform continuity of f∨.) For a net xi→x0 in G and ε>0, compact approximation in [F4] gives a compact K⊆G^ with ∫G^∖K∣f^∣ dmG^<ε/4; by joint continuity [F4] and compactness of K one has sup⁡γ∈K∣γ(xi)−γ(x0)∣<ε/(2∥f^∥1+2) eventually, whence ∣f∨(xi)−f∨(x0)∣≤∫K∣f^(γ)∣ ∣γ(xi)−γ(x0)∣ dmG^(γ)+2∫G^∖K∣f^∣ dmG^<ε. For uniform continuity, use ∣γ(x+z)−γ(x)∣=∣γ(z)−1∣: the same compact-tail bound at z=0 gives one identity neighbourhood working for every x. Hence f∨ is uniformly continuous.

1.3F1F4F6

(Positive convolution-square approximate identities.) For each admissible pair i=(U,u) use its symmetric normalized ui from [F6] and put qi:=ui∗ui~=ui∗ui. Then qi∈E, qi≥0, ∫Gqi=1, and supp⁡qi⊆Ui−Ui, so qi is an approximate identity in L1 by [F6]. Also q^i=∣u^i∣2∈L1(G^,mG^) by [F1], 0≤q^i≤1, and q^i→1 uniformly on every compact subset of G^: for compact K, joint continuity of (γ,x)↦γ(x) makes γ(x)→1 uniformly for γ∈K as x→0, while qi has mass one and support shrinking to 0.

2.1F1F2F4F8step 1.2step 1.3

(Inversion for f∗qi.) Fix an admissible pair i. Step 1.3 gives qi∈Cc(G;R) and q^i∈L1(G^). The inverse integral of q^i is continuous by the compact-tail argument of step 1.2 and agrees with qi a.e. by [F1]; since qi is continuous and Haar measure is positive on nonempty open sets, they agree everywhere. Choose representatives of f and q^i zero off σ-compact essential supports S⊆G and T⊆G^ by [F8]. For fixed x, the kernel f(y)q^i(γ)γ(x−y) is product measurable on S×T: on each compact rectangle, joint continuity of evaluation permits uniform approximation of γ(x−y) by finite sums of products of Borel functions in the separate variables (take finite rectangular covers and disjointify their coordinate covers). Taking a countable exhaustion and multiplying by the scalar measurable factors proves the assertion. Its absolute integral is ∥f∥1∥q^i∥1<∞, so [F8] permits Fubini. Since the convolution integral is absolutely convergent for every x by ∫∣f(y)qi(x−y)∣ dmG(y)≤∥f∥1∥qi∥∞, we obtain Hi(x):=(f∗qi)(x)=∫Gf(y)∫G^q^i(γ)γ(x−y) dmG^(γ) dmG(y)=∫G^f^(γ)q^i(γ)γ(x) dmG^(γ). Changes on the null sets used for the support restrictions affect neither integral. Thus Hi represents f∗qi and is continuous by step 1.2's compact-tail argument, since f^q^i is integrable by [F2].

3.1F4F6F7step 1.3step 2.1

(Uniform inverse convergence and almost-everywhere equality.) By step 2.1, Hi represents f∗qi and is the inverse integral of f^q^i. Step 1.3 gives 0≤q^i≤1 and uniform convergence to 1 on compact dual sets. Since f^∈L1(G^), the compact-tail estimate of [F4] therefore gives ∥f^(q^i−1)∥1→0. Consequently ∥Hi−f∨∥∞≤∥f^(q^i−1)∥1→0, while ∥f∗qi−f∥1→0 by [F6]. For each n≥1 choose an admissible pair in=(Un,un) for which both errors are below 1/n; the assumptions supply Countable Choice, and no countable neighbourhood base is required. By [F7] a subsequence of the specified representatives Hin converges almost everywhere to a representative of f. Uniform convergence makes that subsequence converge everywhere to f∨. Thus f=f∨ almost everywhere on G.

4.1F4F5step 1.1step 1.2step 3.1

(The continuous representative.) By steps 1.1 and 1.2, f∨ is a bounded uniformly continuous function; by step 3.1 it represents the class of f. If g is another continuous representative, then g−f∨ is continuous and vanishes a.e.; if it were nonzero at some x0, it would stay nonzero on a nonempty open neighborhood, which has positive Haar measure [F4], a contradiction. Thus f∨ is the unique continuous representative. If a chosen representative g is continuous at x and g(x)≠f∨(x), continuity at x makes ∣g−f∨∣ bounded below on an open neighbourhood of x, again contradicting almost-everywhere equality and Haar positivity. Hence g(x)=f∨(x) at every such point.

5.1step 1.1step 1.2step 3.1step 4.1∎

Steps 1.1 and 1.2 show absolute convergence and bounded uniform continuity of f∨, step 3.1 shows f∨=f mG-a.e., and step 4.1 gives uniqueness of the continuous representative and the statement at continuity points; no value at a point of discontinuity of an arbitrary representative is claimed.

Depends on

Used by

Dependency tree · two levels

95 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