ExampleConstruction: Literature-sourcedVerification: 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.

Haar normalisations on a finite abelian group and its dual

Statement

Let $G$ be a finite abelian group with its probability Haar measure $m_{G} (E) = ∣ E ∣ / ∣ G ∣$ and let $\hat{G}$ be its dual group. The compatible dual Haar measure is counting measure on $\hat{G}$ , so for $f : G \to C$ the inversion formula is $f (x) = \sum_{γ \in \hat{G}} \hat{f} (γ) γ (x), \hat{f} (γ) = \frac{1}{∣ G ∣} \sum_{x \in G} f (x) \overline{γ (x)}, i.e. f = \frac{1}{∣ G ∣} \sum_{γ \in \hat{G}} (\sum_{x \in G} f (x) \overline{γ (x)}) γ .$ Writing $N : = ∣ G ∣$ , the unitary discrete Fourier transform on the counting-measure spaces is $U f (γ) : = N^{- 1 / 2} \sum_{x \in G} f (x) \overline{γ (x)} = N^{1 / 2} \hat{f} (γ), f (x) = N^{- 1 / 2} \sum_{γ \in \hat{G}} U f (γ) γ (x) .$ Thus, for the same input $f$ , passage from the probability-Haar transform to the unitary DFT multiplies the output by $N^{1 / 2}$ . The factor $N^{- 1 / 2}$ is the coefficient in the unitary forward and inverse sums.

Facts & Assumptions

Given: A finite abelian group $G$ written additively, its dual $\hat{G}$ equipped with the compact-open topology, and the LCA Fourier transform normalized by the probability Haar measure $m_{G} (E) = ∣ E ∣ / ∣ G ∣$ .

[F1]

A finite group is compact and discrete. The measure $m_{G} (E) = ∣ E ∣ / ∣ G ∣$ is a left-invariant probability measure by finite counting, so $\int f d m_{G} = ∣ G ∣^{- 1} \sum_{x \in G} f (x)$ (Left Haar integral and left Haar measure).

[F2]

Counting measure $# (E) = ∣ E ∣$ on a finite discrete group is a nonzero Radon measure invariant under every translation, and hence is Haar (Radon measure on an LCH space, Left Haar integral and left Haar measure).

[F3]

A nontrivial finite abelian group is an internal direct product of indecomposable subgroups, and each indecomposable factor is cyclic of prime-power order; the trivial group is the empty product (Every nontrivial finite abelian group is an internal direct product of indecomposable subgroups, The indecomposable finite abelian groups are exactly the nontrivial cyclic groups of prime-power order). The dual of a finite product is the product of the duals (the finite-product clause of Duals of finite products and of discrete direct sums, The Pontryagin dual with the compact-open topology). The character group of $Z / N Z$ is $Z / N Z$ : a character is determined by the $N$ -th root of unity $z = χ ([1])$ , and the kernel theorem for the complex exponential gives $z = \exp (2 π i k / N)$ for a unique $k \in Z / N Z$ (The complex exponential by its power series, $\ker (\exp) = 2 π i Z$ , and $\exp z = \exp w$ exactly when $z - w \in 2 π i Z$ , Additive characters are exactly one-dimensional complex representation characters).

[F4]

The dual group is an abelian group under pointwise multiplication (The Pontryagin dual with the compact-open topology), so translation $γ \mapsto γ_{0} γ$ is a bijection of $\hat{G}$ ; moreover the local cyclic characters of [F3] separate the points of $G$ : under the product decomposition every nonzero $z \in G$ has a nonzero coordinate in some cyclic factor, and the character of that factor with frequency $k = 1$ , extended to $G$ through the product duality of [F3], takes a value different from $1$ at $z$ .

[F5]

The transform on the finite group is $\hat{f} (γ) = ∣ G ∣^{- 1} \sum_{x \in G} f (x) \overline{γ (x)}$ (The Fourier transform on an LCA group). A Haar measure on the finite dual is compatible when this inversion formula holds with that measure.

Proof

technique · direct

1.1F1F2F3

(Order and topology of the dual.) If $G$ is trivial, take the empty product; otherwise [F3] writes $G ≅ Z_{1} \oplus \dots \oplus Z_{k}$ with $Z_{j} = Z / N_{j} Z$ . The local computation in [F3] shows $\hat{Z_{j}} ≅ Z / N_{j} Z$ , so by the finite-product duality $\hat{G} ≅ \prod_{j} Z / N_{j} Z$ and $∣ \hat{G} ∣ = \prod_{j} N_{j} = ∣ G ∣$ . The same statement holds for the trivial group, whose dual is trivial. Thus $\hat{G}$ is finite and discrete, and by [F2] counting measure is a Haar measure of total mass $∣ \hat{G} ∣ = ∣ G ∣$ .

2.1F4step 1.1

(Orthogonality.) For $z \in G$ , if $z = 0$ then $γ (z) = 1$ for every $γ$ and $\sum_{γ \in \hat{G}} γ (z) = ∣ \hat{G} ∣ = ∣ G ∣$ . If $z \neq 0$ , step 1.1 and [F4] provide $γ_{0}$ with $γ_{0} (z) \neq 1$ ; since $γ \mapsto γ_{0} γ$ is a bijection of $\hat{G}$ , $\sum_{γ} γ (z) = \sum_{γ} (γ_{0} γ) (z) = γ_{0} (z) \sum_{γ} γ (z)$ , hence $\sum_{γ \in \hat{G}} γ (z) = 0$ . Therefore $\sum_{γ \in \hat{G}} γ (x - y) = ∣ G ∣ δ_{x, y}$ for all $x, y \in G$ , which is the displayed orthogonality relation.

3.1F5step 2.1

(Inversion.) For $f : G \to C$ and $γ \in \hat{G}$ , the transform is $\hat{f} (γ) = ∣ G ∣^{- 1} \sum_{x \in G} f (x) \overline{γ (x)}$ by [F5]. Hence, using the orthogonality of step 2.1, $\sum_{γ \in \hat{G}} \hat{f} (γ) γ (x) = \frac{1}{∣ G ∣} \sum_{y \in G} f (y) \sum_{γ \in \hat{G}} γ (x - y) = \frac{1}{∣ G ∣} \sum_{y \in G} f (y) ∣ G ∣ δ_{x, y} = f (x),$ which is the displayed inversion formula.

4.1F2step 1.1step 3.1algebra

(The compatible measure is counting measure.) Counting measure on the finite group $\hat{G}$ is Haar. Any Haar measure $ν$ on this finite group assigns the same mass $c$ to every point by translation invariance, so $ν = c #$ . If $ν$ is compatible with the transform, applying inversion to $δ_{0}$ gives $1 = \int_{\hat{G}} \hat{δ_{0}} (γ) d ν (γ) = c ∣ \hat{G} ∣ / ∣ G ∣ = c$ , using $∣ \hat{G} ∣ = ∣ G ∣$ from step 1.1. Thus counting measure is the unique compatible dual Haar measure.

4.2step 1.1step 2.1step 3.1algebra

(Unitary normalisation.) Set $N : = ∣ G ∣$ and $U f (γ) : = N^{- 1 / 2} \sum_{x} f (x) \overline{γ (x)} = N^{1 / 2} \hat{f} (γ)$ . By step 3.1, $N^{- 1 / 2} \sum_{γ \in \hat{G}} U f (γ) γ (x) = \sum_{γ \in \hat{G}} \hat{f} (γ) γ (x) = f (x) .$ Expanding the finite sum and using step 2.1 gives $\sum_{γ \in \hat{G}} ∣ U f (γ) ∣^{2} = N^{- 1} \sum_{x, y \in G} f (x) \overline{f (y)} \sum_{γ \in \hat{G}} γ (y - x) = \sum_{x \in G} ∣ f (x) ∣^{2} .$ Hence $U$ is a linear isometry for the counting-measure norms; the displayed inversion and $∣ \hat{G} ∣ = ∣ G ∣$ make it bijective, so it is unitary. Its relation to the probability-Haar transform is $U f = N^{1 / 2} \hat{f}$ .

5.1step 2.1step 3.1step 4.1step 4.2∎

Step 2.1 gives the orthogonality relation, step 3.1 gives the nonunitary inversion formula, step 4.1 identifies counting measure as the compatible dual Haar measure, and step 4.2 gives the unitary DFT, its inverse coefficient $∣ G ∣^{- 1 / 2}$ and the output conversion $U f = ∣ G ∣^{1 / 2} \hat{f}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

83 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

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)
Michael E. Taylor, Fourier Analysis, Distributions, and Concentration (course text) (standard reference, not scraped)