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.

Normalized coefficient approximation for irreducible weak containment

Statement

Assume the Axiom of Choice. Let $G$ be an LCH group, let $π$ be an irreducible strongly continuous unitary representation of $G$ and let $ρ$ be a strongly continuous unitary representation with $π ≺ ρ$ (Weak containment of unitary representations, Strongly continuous unitary representations, invariant linear subspaces and intertwiners). Then $ρ$ is nonzero, and for every normalized function of positive type $ϕ$ associated to $π$ (that is, $ϕ (g) = ⟨ π (g) ξ, ξ ⟩$ with $∥ ξ ∥ = 1$ , Continuous positive-type functions and normalization, Matrix coefficient of a unitary representation), every compact $Q \subseteq G$ and every $ϵ > 0$ there is a unit vector $η \in H_{ρ}$ with $\sup_{g \in Q} ∣ ϕ (g) - ⟨ ρ (g) η, η ⟩ ∣ < ϵ .$ Thus a normalized coefficient of $π$ is a compact-uniform limit of single normalized coefficients of $ρ$ , not merely of finite sums of them.

Facts & Assumptions

Given: AC; an LCH group $G$ ; an irreducible unitary representation $π$ ; a unitary representation $ρ$ with $π ≺ ρ$ ; a normalized function of positive type $ϕ$ associated to $π$ .

[F1]

Every diagonal coefficient has $φ (e) = ∥ ξ ∥^{2}$ and $∣ φ (g) ∣ \leq ∥ ξ ∥^{2}$ , so a normalized one satisfies $ϕ (e) = 1$ ; weak containment $π ≺ ρ$ requires every function of positive type associated to $π$ to be approximated uniformly on compacta by finite sums of functions of positive type associated to $ρ$ (Weak containment of unitary representations, Continuous positive-type functions and normalization, Matrix coefficient of a unitary representation).

[F2]

Family selection: if $(ρ_{s})_{s \in S}$ is a set-indexed family of nonzero unitary representations and $π ≺ {⨁^{^}}_{s \in S} ρ_{s}$ for an irreducible $π$ , then for every unit $ξ \in H_{π}$ , compact $Q$ and $ϵ > 0$ there are $s \in S$ and a unit vector $η \in H_{ρ_{s}}$ with $\sup_{Q} ∣ ⟨ π (g) ξ, ξ ⟩ - ⟨ ρ_{s} (g) η, η ⟩ ∣ < ϵ$ (Irreducible weak containment in a family selects one coefficient, Hilbert direct sums of unitary representations).

Proof

technique · direct

Given: AC, an LCH group $G$ , an irreducible unitary representation $π$ , a unitary representation $ρ$ with $π ≺ ρ$ , and a normalized positive-type function $ϕ$ associated to $π$ .

1.1F1

$ρ$ is nonzero. If $H_{ρ} = {0}$ , then the only function of positive type associated to $ρ$ is $0$ , so no finite sum of such functions can be within $1 / 2$ of $ϕ$ on the compact set ${e}$ , where $ϕ (e) = 1$ by [F1]; this contradicts $π ≺ ρ$ .

2.1F2step 1.1

The approximation holds. Apply [F2] to the singleton family $S = {0}$ with $ρ_{0} : = ρ$ , whose direct sum is $ρ$ itself: since $π ≺ ρ$ and $ρ$ is nonzero by step 1.1, for the unit vector $ξ$ with $ϕ = ⟨ π (\cdot) ξ, ξ ⟩$ , the compact set $Q$ and the given $ϵ$ , there are $s \in S$ and a unit vector $η \in H_{ρ_{s}} = H_{ρ}$ with $\sup_{Q} ∣ ϕ (g) - ⟨ ρ (g) η, η ⟩ ∣ < ϵ$ , which is the assertion.

3.1givenF1∎

The Axiom of Choice is inherited from the family-selection lemma; the singleton specialization, the positivity of $ϕ$ and the normalization at $e$ use no further choice (The Axiom of Choice).

Depends on

Used by

Dependency tree · two levels

33 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

Bachir Bekka, Pierre de la Harpe and Alain Valette, Kazhdan's Property (T) (Cambridge University Press 2008; author-hosted complete text) (standard reference, not scraped)
Bachir Bekka and Pierre de la Harpe, Unitary Representations of Groups, Duals, and Characters (arXiv:1912.07262v1, 16 December 2019) (standard reference, not scraped)