Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated
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.

Fell convergence of the characters of the real line

Example

Assume the Axiom of Choice. For G=R the unitary dual is R^={χt:t∈R},χt(x)=eitx, and a net χti converges to χt in the Fell topology (The Fell topology on the unitary dual) if and only if ti→t in R. For characters, weak containment χs≺χt (Weak containment of unitary representations) holds if and only if s=t.

Facts & Assumptions

Given: AC; the additive group R; the parametrized characters χt(x)=eitx; the Fell topology on the unitary dual.

[F1]

Schur's lemma: every bounded self-intertwiner of an irreducible strongly continuous unitary representation is a scalar multiple of the identity, and a nonzero bounded intertwiner between irreducible representations is a unitary equivalence up to a scalar (Schur lemma for complex unitary representations).

[F2]

Every continuous group homomorphism R→T is exp⁡(2πiξ ⋅) for a unique ξ∈R; writing t=2πξ, these are exactly the maps χt (Continuous characters of the real line are exponentials, The Pontryagin dual with the compact-open topology).

[F3]

Fell basis: a basic neighbourhood of a class π is determined by finitely many functions of positive type associated to π, a compact set Q and ϵ>0, and consists of the classes whose coefficients approximate each of them to within ϵ on Q (The Fell topology on the unitary dual). For a one-dimensional unitary character χ, a diagonal coefficient at a vector z∈C is ∣z∣2χ, so the functions of positive type associated to χ are exactly the nonnegative multiples cχ, c≥0, and finite sums of them are again of this form (Strongly continuous unitary representations, invariant linear subspaces and intertwiners).

Verification

technique · direct

Given: AC, the additive group R, and the characters χt(x)=eitx.

1.1F1

Every irreducible strongly continuous unitary representation of the abelian group R is one-dimensional. Indeed, for fixed g the operator π(g) commutes with every π(h), hence is a bounded self-intertwiner of π; [F1] makes it a scalar χ(g)I. Every linear subspace is then invariant, so irreducibility forces dim⁡H=1; the resulting map χ:R→T is a continuous unitary character.

1.2F2

By [F2] every continuous unitary character of R is χt for a unique t∈R, and each χt is a continuous unitary character of R.

2.1F2step 1.1step 1.2

Hence R^={χt:t∈R}, with t↦χt bijective: step 1.1 exhibits every irreducible class as a character, step 1.2 identifies the characters, and distinct t give distinct characters (evaluate at a suitable x).

3.1F3step 2.1

Fell convergence is compact-uniform convergence of the parameters. If ti→t, then for a compact Q⊆R and R:=sup⁡x∈Q∣x∣ one has sup⁡x∈Q∣χti(x)−χt(x)∣≤R ∣ti−t∣→0; hence for every finite family cjχt of tests, every compact Q and every ϵ>0, the test cjχt is within ϵ on Q of the coefficient cjχti once i is large, so χti∈W(χt;⋅,Q,ϵ) eventually and χti→χt in the Fell topology. Conversely, suppose χti→χt, let 0<ϵ<1 and fix δ>0; put Q:=[−π/δ,π/δ]. By [F3] the neighbourhood determined by the coefficient χt, the set Q and ϵ is met eventually: there are ci′≥0 with sup⁡Q∣χt−ci′χti∣<ϵ. Evaluating at x=0 gives ∣1−ci′∣<ϵ, hence ci′>1−ϵ. If ∣ti−t∣≥δ, then xi:=π/∣ti−t∣ lies in Q and χti(xi)=−χt(xi), so ∣χt(xi)−ci′χti(xi)∣=1+ci′>2−ϵ>1>ϵ, a contradiction. Hence eventually ∣ti−t∣<δ, and since δ>0 was arbitrary, ti→t.

4.1F3step 2.1step 3.1

Weak containment of characters: if χs≺χt, then applying the defining approximation to the coefficient χs (the diagonal coefficient at a unit vector), the compact set Q=[−π/δ,π/δ] and some 0<ϵ<1, and using [F3], we find c′≥0 with sup⁡Q∣χs−c′χt∣<ϵ; evaluating at 0 gives c′>1−ϵ, and if ∣s−t∣≥δ, the point x=π/∣s−t∣∈Q gives ∣χs(x)−c′χt(x)∣=1+c′>1>ϵ, a contradiction. Hence ∣s−t∣<δ for every δ>0, so s=t; the converse is immediate by taking the identical coefficient. This agrees with The Fell closure of a single representation is its weak containment closure, since by step 3.1 the point χs lies in the Fell closure of {χt} exactly when s=t.

5.1givenF1F2∎

The Axiom of Choice is inherited from Schur's lemma and the Fell topology suppliers; the character and parameter computations use no further choice (The Axiom of Choice).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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