LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Positive-type functions define the GNS pre-Hilbert form

Statement

Let $G$ be a topological group and let $φ : G \to C$ be a continuous function of positive type. Write $C^{(G)}$ for the complex vector space of all finitely supported functions $f : G \to C$ ; no continuity or compact-support condition is imposed on these functions. For $f, h \in C^{(G)}$ , define $B_{φ} (f, h) = \sum_{x, y \in G} f (x) \overline{h (y)} φ (y^{- 1} x) .$ Then $B_{φ}$ is a positive-semidefinite sesquilinear form, linear in its first argument. Its null space $N_{φ} = {f \in C^{(G)} : B_{φ} (f, f) = 0}$ is orthogonal to all of $C^{(G)}$ , and $B_{φ}$ induces an inner product on the quotient $C^{(G)} / N_{φ}$ . In particular, $B_{φ} (δ_{x}, δ_{y}) = φ (y^{- 1} x) (x, y \in G),$ where $δ_{x}$ is the function equal to $1$ at $x$ and $0$ elsewhere.

Facts & Assumptions

[A1]

For every finite list $g_{1}, \dots, g_{n} \in G$ , the matrix $(φ (g_{i}^{- 1} g_{j}))_{i, j}$ is positive semidefinite; its quadratic form with coefficients $a_{1}, \dots, a_{n}$ is nonnegative (Continuous positive-type functions and normalization).

[A2]

The complex inner-product convention is linear in the first argument and conjugate-symmetric (Real and complex inner-product spaces and their induced length).

Proof

Given: A topological group $G$ and a continuous positive-type function $φ : G \to C$ .

Proof technique: direct.

1.1A2algebra

The sums defining $B_{φ} (f, h)$ are finite because $f$ and $h$ have finite support, and the formula is linear in $f$ and conjugate-linear in $h$ , hence sesquilinear with the convention in [A2].

1.2A1

If $f = 0$ , then $B_{φ} (f, f) = 0$ ; otherwise list its finite support as $g_{1}, \dots, g_{n}$ and put $a_{i} = f (g_{i})$ . By [A1] and reindexing the finite sum, $B_{φ} (f, f) = \sum_{i, j} a_{i} \overline{a_{j}} φ (g_{j}^{- 1} g_{i}) = \sum_{i, j} \overline{a_{i}} φ (g_{i}^{- 1} g_{j}) a_{j} \geq 0$ . Thus every diagonal value is real and nonnegative.

2.1step 1.1step 1.2algebra

For any $f, h$ and $z \in C$ , step 1.2 applied to $f + z h$ shows $B_{φ} (f + z h, f + z h) \in R$ . Expanding by step 1.1, the diagonal terms are real and the cross term is $z B_{φ} (h, f) + \overline{z} B_{φ} (f, h)$ ; its being real for $z = 1$ and $z = i$ implies $B_{φ} (h, f) = \overline{B_{φ} (f, h)}$ . Hence the form is Hermitian.

3.1step 1.2step 2.1algebra

Put $a = B_{φ} (f, f)$ , $b = B_{φ} (h, h)$ and $c = B_{φ} (f, h)$ . By steps 1.2 and 2.1, $B_{φ} (f + z h, f + z h) = a + 2 Re (z \overline{c}) + ∣ z ∣^{2} b \geq 0$ for every $z \in C$ . If $b > 0$ , take $z = - c / b$ to obtain $∣ c ∣^{2} \leq a b$ . If $b = 0$ and $c \neq 0$ , take $z = - t c / ∣ c ∣$ with $t > a / (2 ∣ c ∣)$ ; the displayed quantity is $a - 2 t ∣ c ∣ < 0$ , a contradiction. Thus $∣ B_{φ} (f, h) ∣^{2} \leq B_{φ} (f, f) B_{φ} (h, h)$ in all cases.

4.1A2step 1.1step 2.1step 3.1

By step 3.1, every $f \in N_{φ}$ satisfies $B_{φ} (f, h) = 0$ for every $h$ . This radical property makes $N_{φ}$ a complex linear subspace, since sums of null vectors and scalar multiples remain null. Changing either representative by an element of $N_{φ}$ leaves $B_{φ}$ unchanged. The induced form on the quotient is positive definite: if $B_{φ} ([f], [f]) = 0$ , then $f \in N_{φ}$ and $[f] = 0$ . It is therefore an inner product under [A2], including the zero quotient when $φ = 0$ .

5.1algebra∎

For $δ_{x}$ and $δ_{y}$ , only the summand with first index $x$ and second index $y$ survives, so $B_{φ} (δ_{x}, δ_{y}) = φ (y^{- 1} x)$ .

Depends on

Used by

Dependency tree · two levels

6 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

Bekka and de la Harpe, Unitary Representations of Groups, Duals, and Characters, Construction 1.B.5, Chapter 1 §1.B, printed pp. 27–28 (standard reference, not scraped)
Bekka, de la Harpe and Valette, Kazhdan's Property (T), Appendix C §C.4, proof of Theorem C.4.10, printed pp. 375–376 (standard reference, not scraped)