Definitions/Def_RepTheory_LevelDensity.lean

The module fixes a topological group G, complex vector spaces V and S, a monoid homomorphism \pi : G \to \operatorname{End}_{\mathbb C}(V) into the multiplicative monoid of complex-linear endomorphisms of V (so V is a representation of G without any continuity, admissibility or smoothness assumption), and a complex-linear map H : S \to \operatorname{End}_{\mathbb C}(V), thought of as the action of a test module S on V; note that S carries no multiplication and H is required only to be linear, not multiplicative. In this context the single declaration TwistedPairing.IsLevelDenseAction is the predicate on H (with \pi an explicit argument) asserting the following: for every subgroup K \le G whose underlying subset of G is both compact and open, for every complex-linear functional \ell : V \to \mathbb C that is K-invariant in the sense that \ell(\pi(k)x) = \ell(x) for all k \in K and all x \in V, and for every vector x_0 \in V fixed by K, i.e. \pi(k)x_0 = x_0 for all k \in K, there exists \varphi \in S with H(\varphi)\,x = \ell(x)\,x_0 \qquad\text{for all } x \in V. Thus the predicate demands that every rank-\le 1 operator of the shape x \mapsto \ell(x)x_0 built from a K-invariant functional and a K-fixed vector, at every compact open level K, be realised exactly (not merely approximated) by the action of a single element of S. The quantification is over all compact open subgroups of G simultaneously, which is the sense in which the density is 'level-wise'; no topology on V or S is involved, and the conclusion is an identity of operators on all of V.