CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Normalised positive definite functions correspond to probability measures

Statement

Assume the Axiom of Choice and Dependent Choice, and let $G$ be a locally compact Hausdorff abelian group. Under Bochner's theorem Bochner's theorem for LCA groups, a continuous positive definite $ϕ : G \to C$ satisfies $ϕ (0) = 1$ if and only if its representing finite positive Radon measure on $\hat{G}$ is a probability measure. In particular continuous positive definite functions with $ϕ (0) = 1$ are exactly the Fourier-Stieltjes transforms of Radon probability measures on $\hat{G}$ .

Facts & Assumptions

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

[F1]

By Bochner's theorem, $ϕ$ is continuous positive definite if and only if it has a unique representing finite positive Radon measure $μ$ on $\hat{G}$ , characterized by $ϕ (x) = \int_{\hat{G}} γ (x) d μ (γ)$ for all $x \in G$ , and then $μ (\hat{G}) = ϕ (0)$ (Bochner's theorem for LCA groups, Positive definite functions on an abelian group, Radon measure on an LCH space).

[F2]

A probability measure on the Borel $σ$ -algebra of $\hat{G}$ is a measure $P$ with $P (\hat{G}) = 1$ (Probability measures and probability spaces); a finite positive Radon measure is a probability measure exactly when its total mass is $1$ .

[F3]

For every finite positive Radon measure $μ$ on $\hat{G}$ , its Fourier-Stieltjes transform $ϕ_{μ} (x) = \int_{\hat{G}} γ (x) d μ (γ)$ is continuous and positive definite with $ϕ_{μ} (0) = μ (\hat{G})$ (Fourier-Stieltjes transforms of positive measures are continuous positive definite).

Proof

technique · direct

1.1F1F2

(Normalised function gives probability measure.) Let $ϕ$ be continuous and positive definite with representing measure $μ$ and $ϕ (0) = 1$ . By [F1], $μ (\hat{G}) = ϕ (0) = 1$ , so by [F2] $μ$ is a probability measure.

1.2F1F2F3

(Probability measure gives normalised function.) Let $P$ be a Radon probability measure on $\hat{G}$ and put $ϕ (x) : = \int_{\hat{G}} γ (x) d P (γ)$ . By [F3] $ϕ$ is continuous and positive definite with $ϕ (0) = P (\hat{G}) = 1$ , and [F1] identifies $P$ as its unique representing measure.

2.1step 1.1step 1.2

(The correspondence.) Combining steps 1.1 and 1.2: continuous positive definite functions with $ϕ (0) = 1$ correspond exactly to their representing measures, and those are exactly the Radon probability measures; conversely the Fourier-Stieltjes transform of a Radon probability measure is a continuous positive definite function with value $1$ at $0$ .

3.1step 1.1step 1.2step 2.1∎

Steps 1.1 and 1.2 prove the equivalence, and step 2.1 records the stated identification of continuous positive definite functions with $ϕ (0) = 1$ and Fourier-Stieltjes transforms of Radon probability measures.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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)