TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedjudge pass (gpt-6.1-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.

Bochner's theorem for LCA groups

Statement

Assume the Axiom of Choice and Dependent Choice. Let $G$ be a locally compact Hausdorff abelian group with dual $\hat{G}$ . A continuous function $ϕ : G \to C$ is positive definite if and only if there is a unique finite positive Radon measure $μ$ on $\hat{G}$ with $ϕ (x) = \int_{\hat{G}} γ (x) d μ (γ) (x \in G),$ and then $μ (\hat{G}) = ϕ (0)$ . The measure is called the representing measure of $ϕ$ .

Facts & Assumptions

Given: The Axiom of Choice and Dependent Choice, a locally compact Hausdorff abelian group $G$ with Haar measure $m_{G}$ and dual $\hat{G}$ , and a continuous function $ϕ : G \to C$ .

[F1]

If $μ$ is a finite positive Radon measure on $\hat{G}$ , then $ϕ_{μ} (x) : = \int_{\hat{G}} γ (x) d μ (γ)$ is continuous and positive definite, and $ϕ_{μ} (0) = μ (\hat{G})$ (Fourier-Stieltjes transforms of positive measures are continuous positive definite, Positive definite functions on an abelian group, Radon measure on an LCH space).

[F2]

If $ϕ$ is continuous and positive definite with $k = ϕ (0)$ , then the transform-core functional $F_{ϕ}$ of the preceding lemmas extends uniquely to a bounded positive linear functional $L$ on $C_{0} (\hat{G})$ with norm $k$ , there is a finite positive Radon measure $μ_{ϕ}$ on $\hat{G}$ with $L (H) = \int_{\hat{G}} H d μ_{ϕ}$ for all $H \in C_{0} (\hat{G})$ and $μ_{ϕ} (\hat{G}) = k$ , and for every $f \in L^{1} (G, m_{G})$ one has $F_{ϕ} (\hat{f}) = L_{ϕ} (f) = \int_{G} f (x) ϕ (- x) d m_{G} (x)$ (Positive definite functions give positive bounded functionals on the transform core, The Bochner functional extends and has a Radon representing measure, The Fourier transform on an LCA group).

[F3]

Two finite regular complex Borel measures on $\hat{G}$ with the same inverse transform $x \mapsto \int_{\hat{G}} γ (x) d σ (γ)$ are equal (Fourier-Stieltjes transforms determine finite Radon measures, Regular complex Borel measures).

[F4]

For $f \in C_{c} (G)$ and the finite measure $μ_{ϕ}$ , Fubini gives $\int_{\hat{G}} \hat{f} d μ_{ϕ} = \int_{G} f (x) (\int_{\hat{G}} γ (- x) d μ_{ϕ} (γ)) d m_{G} (x)$ ; the function $x \mapsto \int_{\hat{G}} γ (x) d μ_{ϕ} (γ)$ is continuous because $∣ μ_{ϕ} ∣$ is inner regular and characters converge uniformly on compact sets; and a continuous function on $G$ annihilated by every nonnegative compactly supported bump is identically zero, since Haar measure is positive on nonempty open sets and Urysohn cutoffs exist (Fubini's theorem for L^1 functions on a sigma-finite product, Radon measure on an LCH space, 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, LCH Urysohn cutoff, Compact support, $C_{c} (X)$ , and $C_{0} (X)$ ).

[F5]

Haar measure is invariant under the substitution $x \mapsto - x$ (Haar measure on an abelian group is invariant under inversion, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, The Axiom of Choice).

Proof

technique · direct

1.1F1

(The easy direction.) Assume $ϕ (x) = \int_{\hat{G}} γ (x) d μ (γ)$ for a finite positive Radon measure $μ$ . Then by [F1] $ϕ$ is continuous and positive definite with $ϕ (0) = μ (\hat{G})$ ; this proves the reverse implication and the mass identity for that direction.

1.2F2

(The converse: construction of the measure.) Assume $ϕ$ continuous and positive definite, and put $k : = ϕ (0)$ . By [F2] there is a finite positive Radon measure $μ_{ϕ}$ on $\hat{G}$ with $μ_{ϕ} (\hat{G}) = k$ , representing the extension $L$ of $F_{ϕ}$ on $C_{0} (\hat{G})$ , and with $\int_{\hat{G}} \hat{f} d μ_{ϕ} = F_{ϕ} (\hat{f}) = \int_{G} f (x) ϕ (- x) d m_{G} (x)$ for every $f \in L^{1} (G, m_{G})$ .

2.1F2F4F5step 1.2

(The representation $ϕ = {\overset{ˇ}{μ}}_{ϕ}$ .) Let $f \in C_{c} (G) \subseteq L^{1} (G, m_{G})$ and put $Ψ (x) : = \int_{\hat{G}} γ (x) d μ_{ϕ} (γ)$ . By [F4], Fubini and step 1.2 give $0 = \int_{G} f (x) ϕ (- x) d m_{G} (x) - \int_{\hat{G}} \hat{f} d μ_{ϕ} = \int_{G} f (x) (ϕ (- x) - Ψ (- x)) d m_{G} (x) .$ Replacing $f$ by $f (- \cdot)$ , which still ranges over $C_{c} (G)$ , and using the inversion invariance of Haar measure [F5] yields $\int_{G} f (x) (ϕ - Ψ) (x) d m_{G} (x) = 0$ for every $f \in C_{c} (G)$ . The function $D : = ϕ - Ψ$ is continuous by hypothesis and [F4]. If $D (y_{0}) \neq 0$ , choose $c \in C$ with $∣ c ∣ = 1$ and $Re (c D (y_{0})) > 0$ ; continuity gives a nonempty open neighbourhood $V$ of $y_{0}$ on which $Re (c D) > 0$ . Choose a nonzero nonnegative bump $f \in C_{c} (G)$ supported in $V$ . Since Haar measure is positive on nonempty open sets, $\int_{G} f (x) Re (c D (x)) d m_{G} (x) > 0$ , contradicting $c \int_{G} f (x) D (x) d m_{G} (x) = 0$ . Thus $D = 0$ , so $ϕ (x) = Ψ (x) = \int_{\hat{G}} γ (x) d μ_{ϕ} (γ)$ for every $x \in G$ .

2.2F3step 1.1

(Uniqueness of the representing measure.) Suppose finite positive Radon measures $μ, ν$ on $\hat{G}$ satisfy $\int_{\hat{G}} γ (x) d μ (γ) = \int_{\hat{G}} γ (x) d ν (γ)$ for every $x \in G$ . Then $σ : = μ - ν$ is a finite regular complex Borel measure whose inverse transform vanishes identically, so $σ = 0$ by [F3], that is, $μ = ν$ .

3.1step 1.1step 1.2step 2.1step 2.2∎

(Conclusion.) Step 2.1 proves that every continuous positive definite $ϕ$ has a representing finite positive Radon measure $μ_{ϕ}$ with $μ_{ϕ} (\hat{G}) = ϕ (0)$ by step 1.2, step 2.2 proves uniqueness, and step 1.1 proves the converse direction and its mass identity.

Depends on

Used by

Normalised positive definite functions correspond to probability measures Corollary
A character is positive definite Example
Continuous characters separate points of an LCA group Lemma
Compatible dual Haar normalisation Theorem

Dependency tree · two levels

76 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

Lynn H. Loomis, Introduction to Abstract Harmonic Analysis, D. Van Nostrand, 1953 (Harvard-hosted full scan) (standard reference, not scraped)
T. W. Koerner, Topological Groups (author PDF, Internet Archive snapshot of the dpmms.cam.ac.uk Topg.pdf file) (standard reference, not scraped)
Manfred Einsiedler and Thomas Ward, Ergodic Theory with a View Towards Number Theory, Appendix C.2-C.3 (course-hosted full text) (standard reference, not scraped)