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.

Evaluation of characters is jointly continuous

Statement

Let $G$ be a locally compact Hausdorff abelian group (Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space). The evaluation pairing $\hat{G} \times G \to T, (γ, x) \mapsto γ (x),$ is continuous for the compact-open topology on $\hat{G}$ (The Pontryagin dual with the compact-open topology) and the given topology on $G$ (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Continuity of a map of topological spaces at a point and globally).

Facts & Assumptions

[F1]

$G$ is a topological group whose translations and inversion are homeomorphisms, and $G$ is locally compact: every point has a compact neighbourhood. (Left and right translations and inversion in a topological group are homeomorphisms, Locally compact topological space: every point has a compact neighbourhood; and what this says in a metric space)

[F2]

In a locally compact Hausdorff space, every open neighbourhood $U$ of a point $x$ contains an open set $V$ with $x \in V \subseteq \overline{V} \subseteq U$ and $\overline{V}$ compact. (In a locally compact Hausdorff space every open set containing a point contains an open set containing it whose closure is compact and still inside; such a space is regular, Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open)

[F3]

The dual consists of the continuous homomorphisms $γ : G \to T$ , with the compact-open subbasis $S (K, V) = {γ : γ [K] \subseteq V}$ for compact $K \subseteq G$ and open $V \subseteq T$ ; every such set is open in the subspace topology and contains every character mapping $K$ into $V$ . (The Pontryagin dual with the compact-open topology, Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace)

[F4]

Continuous images of compact sets are compact, and a translate of a compact set is compact; a translate of an open set is open. (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, Left and right translations and inversion in a topological group are homeomorphisms, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right)

[F5]

For all $z, w \in T$ : $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ , $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ , $z^{- 1}$ has modulus $1$ , and $∣ z^{- 1} - w^{- 1} ∣ = ∣ z - w ∣$ ; in particular every $γ (x)$ and every $γ_{0} (x_{0})$ has modulus $1$ . (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)

Proof

Given: A locally compact Hausdorff abelian group $G$ , a character $γ_{0} \in \hat{G}$ , a point $x_{0} \in G$ , and $ε > 0$ .

1.1F1F2F3

Choose an open neighbourhood $U$ of $x_{0}$ with $γ_{0} [U] \subseteq B (γ_{0} (x_{0}), ε / 2)$ , possible because $γ_{0}$ is continuous at $x_{0}$ by [F3]; by [F2] choose an open $V$ with $x_{0} \in V \subseteq \overline{V} \subseteq U$ and $K : = \overline{V}$ compact. Then $K$ is a compact neighbourhood of $x_{0}$ with $γ_{0} [K] \subseteq B (γ_{0} (x_{0}), ε / 2)$ .

2.1step 1.1F1F3F4F5

The translate $K - x_{0} = {x - x_{0} : x \in K}$ is compact and is a neighbourhood of $0$ : it is the image of $K$ under the homeomorphism $x \mapsto x - x_{0}$ of [F1, F4], and it contains the open translate $V - x_{0}$ of $V$ , which contains $0$ . Moreover $γ_{0} [K - x_{0}] \subseteq B (1, ε / 2)$ , because for $x \in K \subseteq U$ one has $γ_{0} (x - x_{0}) = γ_{0} (x) γ_{0} (x_{0})^{- 1}$ and $∣ γ_{0} (x) γ_{0} (x_{0})^{- 1} - 1 ∣ = ∣ γ_{0} (x) - γ_{0} (x_{0}) ∣ < ε / 2$ by [F5].

3.1step 2.1F3F5

Let $γ \in S ({x_{0}}, B (γ_{0} (x_{0}), ε / 2)) \cap S (K - x_{0}, B (1, ε / 2))$ and $x \in K$ . Since $γ$ is a homomorphism, $γ (x) = γ (x_{0}) γ (x - x_{0})$ , so $γ (x) - γ_{0} (x_{0}) = (γ (x_{0}) - γ_{0} (x_{0})) γ (x - x_{0}) + γ_{0} (x_{0}) (γ (x - x_{0}) - 1)$ and hence $∣ γ (x) - γ_{0} (x_{0}) ∣ \leq ∣ γ (x_{0}) - γ_{0} (x_{0}) ∣ + ∣ γ (x - x_{0}) - 1 ∣ < ε / 2 + ε / 2 = ε$ by [F5] and the choice of $γ$ .

4.1step 1.1step 2.1step 3.1F2F3∎

The set $W : = (S ({x_{0}}, B (γ_{0} (x_{0}), ε / 2)) \cap S (K - x_{0}, B (1, ε / 2))) \times V$ is a neighbourhood of $(γ_{0}, x_{0})$ in $\hat{G} \times G$ : it is a product of an open set containing $γ_{0}$ and an open set containing $x_{0}$ , the first because $γ_{0} (x_{0}) \in B (γ_{0} (x_{0}), ε / 2)$ and $γ_{0} [K - x_{0}] \subseteq B (1, ε / 2)$ by step 2.1, the second because $V$ is open and $x_{0} \in V \subseteq K$ . By step 3.1 the pairing maps $W$ into $B (γ_{0} (x_{0}), ε)$ ; since open balls form a neighbourhood base at $γ_{0} (x_{0})$ , the pairing is continuous at the arbitrary point $(γ_{0}, x_{0})$ , hence continuous.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

80 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, Chapter VII, Sections 34-35 (printed pp. 134-140) (standard reference, not scraped)
Dikran D. Dikranjan, Introduction to Topological Groups (author lecture notes, Universita di Udine / Universidad Complutense de Madrid, 2007) (standard reference, not scraped)