CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Compact and discrete transforms are the two extreme Plancherel cases

Statement

Assume the Axiom of Choice (The Axiom of Choice) and Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain). Let $G$ be a locally compact Hausdorff abelian group.

(1) If $G$ is compact with $m_{G} (G) = 1$ , its dual $\hat{G}$ is discrete and the compatible dual Haar measure gives each point mass $1$ ; the Plancherel theorem then reads as the Fourier-series identity $∥ f ∥_{2}^{2} = \sum_{γ \in \hat{G}} ∣ \hat{f} (γ) ∣^{2}, f \in L^{2} (G) .$

(2) If $G$ is discrete with $m_{G}$ the counting measure (each point of mass $1$ ), then $\hat{G}$ is compact and the compatible dual Haar measure is the normalised Haar measure of $\hat{G}$ , and Plancherel reads $\sum_{x \in G} ∣ f (x) ∣^{2} = ∥ \hat{f} ∥_{2}^{2}, f \in ℓ^{2} (G) .$

Without the stated normalisation of $m_{G}$ the identification of the dual measure in (2) is false; the compatible scale is reciprocal in $m_{G}$ , as Compatible dual Haar normalisation records. For a general $L^{2}$ function, $\hat{f}$ denotes the Plancherel transform $F f$ ; its pointwise integral formula is asserted only when $f \in L^{1}$ .

Facts & Assumptions

Given: A locally compact Hausdorff abelian group $G$ with Haar measure $m_{G}$ , its dual $\hat{G}$ with the compatible dual Haar measure $m_{\hat{G}}$ , and the unitary Plancherel transform $F$ .

[F1]

If $G$ is compact then $\hat{G}$ is discrete; if $G$ is discrete then, assuming Choice, $\hat{G}$ is compact. (Compact groups have discrete duals and discrete groups have compact duals)

[F2]

The Haar integral is translation invariant: $\int_{G} f (x + a) d m_{G} (x) = \int_{G} f (x) d m_{G} (x)$ for $f \in L^{1} (G)$ and $a \in G$ . Characters are continuous homomorphisms into $T$ , so $γ_{0} \overline{χ} = γ_{0} χ^{- 1}$ is a character, trivial exactly when $γ_{0} = χ$ , and every nontrivial character takes a value different from $1$ . (Left Haar integral and left Haar measure, Topological group: multiplication and inversion are continuous, The Pontryagin dual with the compact-open topology)

[F3]

The Plancherel transform $F$ is unitary and agrees on $L^{1} (G) \cap L^{2} (G)$ with the Fourier transform $\hat{f} (χ) = \int_{G} f (x) \overline{χ (x)} d m_{G} (x)$ . (The Plancherel theorem for locally compact abelian groups, The Fourier transform on an LCA group)

[F4]

Counting measure on a set $X$ assigns $∣ E ∣$ to finite $E$ , and on a discrete group it is a Haar measure: translation is a bijection, so it preserves cardinalities and hence the counting set function, which is positive on nonempty open sets and finite on compact sets. The space $L^{2} (X, #_{X})$ is the space $ℓ^{2} (X)$ of square-summable families with norm $(\sum_{x} ∣ f (x) ∣^{2})^{1 / 2}$ . (Counting measure on an arbitrary set, Left Haar integral and left Haar measure, Square-summable families on an arbitrary index set and the space $ℓ^{2} (I)$ , The space $L^{p} (μ)$ as the quotient by null functions)

[F5]

A Haar measure on a locally compact group is finite on compact sets and positive on nonempty open sets; any two Haar measures on a locally compact group are positive scalar multiples of each other. (Haar measure is positive on nonempty open sets and finite on compact sets, Uniqueness of left Haar measure up to scale)

Proof

1.1F2F3

Suppose first that $G$ is compact with $m_{G} (G) = 1$ ; then $\hat{G}$ is discrete by [F1]. For characters $γ_{0}, χ \in \hat{G}$ the transform of $γ_{0}$ is $\hat{γ_{0}} (χ) = \int_{G} γ_{0} (x) \overline{χ (x)} d m_{G} (x) = \int_{G} (γ_{0} χ^{- 1}) (x) d m_{G} (x)$ ; the character $ψ : = γ_{0} χ^{- 1}$ is trivial exactly when $γ_{0} = χ$ , and if it is nontrivial then $ψ (a) \neq 1$ for some $a$ and translation invariance gives $\int_{G} ψ d m_{G} = ψ (a) \int_{G} ψ d m_{G}$ , hence $\int_{G} ψ d m_{G} = 0$ . Therefore $\hat{γ_{0}} (χ) = 1$ for $χ = γ_{0}$ and $0$ otherwise, that is $F γ_{0} = 1_{{γ_{0}}}$ .

1.2F2F3F4

Suppose next that $G$ is discrete with $m_{G}$ the counting measure; then $\hat{G}$ is compact by [F1]. The function $f_{0} : = 1_{{0}}$ lies in $L^{1} (G) \cap L^{2} (G)$ with $∥ f_{0} ∥_{2}^{2} = m_{G} ({0}) = 1$ and $\hat{f_{0}} (χ) = \overline{χ (0)} m_{G} ({0}) = 1$ for every $χ \in \hat{G}$ , so $F f_{0}$ is the constant function $1$ on $\hat{G}$ and $∥ F f_{0} ∥_{2}^{2} = m_{\hat{G}} (\hat{G})$ .

2.1F3F4step 1.1

In the situation of step 1.1, $F$ is an isometry and $∥ γ_{0} ∥_{2}^{2} = m_{G} (G) = 1$ , while $∥ F γ_{0} ∥_{2}^{2} = ∥ 1_{{γ_{0}}} ∥_{2}^{2} = m_{\hat{G}} ({γ_{0}})$ ; hence $m_{\hat{G}} ({γ_{0}}) = 1$ for every $γ_{0} \in \hat{G}$ . Every subset $E$ of the discrete dual is open and its compact subsets are finite, so Haar inner regularity gives $m_{\hat{G}} (E) = \sup_{F \subseteq E finite} ∣ F ∣$ . Thus $m_{\hat{G}}$ is counting measure on $\hat{G}$ , and Plancherel for $f \in L^{2} (G)$ reads $∥ f ∥_{2}^{2} = ∥ F f ∥_{2}^{2} = \sum_{γ \in \hat{G}} ∣ F f (γ) ∣^{2} = \sum_{γ \in \hat{G}} ∣ \hat{f} (γ) ∣^{2}$ .

2.2F3F4F5step 1.2

In the situation of step 1.2, $1 = ∥ f_{0} ∥_{2}^{2} = ∥ F f_{0} ∥_{2}^{2} = m_{\hat{G}} (\hat{G})$ ; since $\hat{G}$ is compact, $m_{\hat{G}}$ is a Haar measure of total mass $1$ , that is the normalised Haar measure, and it is unique with that property by [F5]. With the counting measure on the discrete group $G$ one has $∥ f ∥_{2}^{2} = \sum_{x \in G} ∣ f (x) ∣^{2}$ for $f \in ℓ^{2} (G)$ by [F4], so Plancherel reads $\sum_{x \in G} ∣ f (x) ∣^{2} = ∥ F f ∥_{2}^{2} = ∥ \hat{f} ∥_{2}^{2}$ .

3.1step 2.1step 2.2∎

Assembling steps 2.1 and 2.2: for a compact group with normalised Haar measure the Plancherel identity is the Fourier-series identity of (1), and for a discrete group with counting measure it is the $ℓ^{2}$ identity of (2); these are the two extreme Plancherel cases appearing in the statement.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

138 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)
Manfred Einsiedler and Thomas Ward, Ergodic Theory with a View Towards Number Theory, Appendix C (course-hosted full text) (standard reference, not scraped)