LemmaStatement: 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.

Fourier transform intertwines translation, modulation and convolution

Statement

Assume 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 with Haar measure $m_{G}$ . For $f, g \in L^{1} (G, m_{G})$ , $x \in G$ and a character $γ_{0} \in \hat{G}$ , the following identities hold pointwise on $\hat{G}$ : $\hat{T_{x} f} (γ) = \overline{γ (x)} \hat{f} (γ), \hat{γ_{0} f} (γ) = \hat{f} (γ_{0}^{- 1} γ), \hat{f * g} (γ) = \hat{f} (γ) \hat{g} (γ), \hat{f^{*}} (γ) = \overline{\hat{f} (γ)},$ where $T_{x} f = f (\cdot - x)$ , $(γ_{0} f) (x) = γ_{0} (x) f (x)$ and $f^{*} (x) = \overline{f (- x)}$ . All four identities are identities of bounded complex-valued functions on $\hat{G}$ ; the first three are used only after the transform codomain has been identified.

Facts & Assumptions

Given: Dependent Choice, a locally compact Hausdorff abelian group $G$ with Haar measure $m_{G}$ , functions $f, g \in L^{1} (G, m_{G})$ (The space $L^{p} (μ)$ as the quotient by null functions, Integrable real and complex functions, and their integrals), a point $x \in G$ and a character $γ_{0} \in \hat{G}$ .

[F1]

Each $γ \in \hat{G}$ is a continuous homomorphism into the unit circle, so $γ (y - x) = γ (y) \overline{γ (x)}$ , $γ_{0}^{- 1} γ$ is again a character, $γ (- y) = \overline{γ (y)}$ and $∣ γ ∣ = 1$ (The Pontryagin dual with the compact-open topology, The multiplicative unit circle is a compact metrizable topological abelian group, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F2]

$m_{G}$ is translation invariant and inversion invariant (The Fourier transform on an LCA group, Haar measure on an abelian group is invariant under inversion); the transform is defined by $\hat{h} (γ) = \int_{G} h (y) \overline{γ (y)} d m_{G} (y)$ and $∣ \hat{h} ∣ \leq ∥ h ∥_{1}$ (The Fourier transform on an LCA group).

[F3]

The convolution $f * g$ of two $L^{1}$ functions is a well-defined class in $L^{1}$ ; its defining integral may be computed after restricting to $σ$ -compact essential supports, where Tonelli's theorem and Fubini's theorem for $L^{1}$ functions apply to the $σ$ -finite product (L^1 of an LCA group is a commutative Banach star algebra under convolution, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Fubini's theorem for L^1 functions on a sigma-finite product).

Proof

technique · direct

1.1F1F2

(Translation and modulation.) For every $γ$ , [F2] gives $\hat{T_{x} f} (γ) = \int_{G} f (y - x) \overline{γ (y)} d m_{G} (y) = \int_{G} f (z) \overline{γ (z + x)} d m_{G} (z) = \overline{γ (x)} \int_{G} f (z) \overline{γ (z)} d m_{G} (z) = \overline{γ (x)} \hat{f} (γ),$ substituting $z = y - x$ (a translation) and using $γ (z + x) = γ (z) γ (x)$ from [F1]. Likewise $\hat{γ_{0} f} (γ) = \int_{G} γ_{0} (y) f (y) \overline{γ (y)} d m_{G} (y) = \int_{G} f (y) \overline{(γ_{0}^{- 1} γ) (y)} d m_{G} (y) = \hat{f} (γ_{0}^{- 1} γ),$ since $γ_{0} (y) \overline{γ (y)} = \overline{γ_{0} (y)^{- 1} γ (y)}$ and $γ_{0}^{- 1} γ$ is a character by [F1].

1.2F1F3

(Convolution.) By [F3] choose $σ$ -compact essential supports $S, T$ of $f, g$ ; the function $(y, z) \mapsto f (y) g (z) \overline{γ (y + z)}$ is integrable over the $σ$ -finite product $S \times T$ and Tonelli and Fubini give $\hat{f * g} (γ) = \int_{G} (\int_{G} f (y) g (x - y) d m_{G} (y)) \overline{γ (x)} d m_{G} (x) = \int_{S} \int_{T} f (y) g (z) \overline{γ (y + z)} d m_{G} (z) d m_{G} (y) = \hat{f} (γ) \hat{g} (γ),$ the middle step substituting $x = y + z$ (a translation) and the last step using $γ (y + z) = γ (y) γ (z)$ and factoring.

1.3F1F2

(Conjugation.) Using inversion invariance [F2] in the substitution $y \mapsto - y$ and then $γ (- y) = \overline{γ (y)}$ from [F1], $\hat{f^{*}} (γ) = \int_{G} \overline{f (- y)} \overline{γ (y)} d m_{G} (y) = \int_{G} \overline{f (y)} \overline{γ (- y)} d m_{G} (y) = \int_{G} \overline{f (y) \overline{γ (y)}} d m_{G} (y) = \overline{\hat{f} (γ)} .$

2.1F2step 1.1step 1.2step 1.3∎

(Conclusion.) Steps 1.1, 1.2 and 1.3 establish the four displayed identities at every $γ \in \hat{G}$ ; both sides are bounded because $∣ \hat{h} ∣ \leq ∥ h ∥_{1}$ by [F2], so the identities are identities of bounded functions on $\hat{G}$ .

Depends on

Used by

Dependency tree · two levels

91 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.2-C.3 (course-hosted full text) (standard reference, not scraped)