A *Følner sequence* $(F_n)_{n \ge 0}$ is a sequence of finite subsets of $G$ such that for any fixed $R > 0$ we have $$\lim_{n \to \infty} \frac{|\partial_RF_n|}{|F_n|} = 0,$$ where $\partial_RF_n=\{g \in G \mid d(g,F_k) \le R \; \text{and}\; d(g,G\setminus F_k) \le R\}$.

Let $k$ be an arbitrary skew field endowed with the discrete topology and let $\mathbb{N}$ denote the positive integers $\{1,2,\dots\}$. Let $n\in{{\mathbb N}}$. We equip the space of functions ${\operatorname{map}}(G, k^n)=\prod_{g\in G}k^n$ with the product topology, which is the same as the topology of pointwise convergence. The natural right $G$-action on ${\operatorname{map}}(G, k^n)$ is defined by $$(\phi g)(x)=\phi(xg^{-1})\text{ for $g,x\in G,\phi\in{\operatorname{map}}(G,k^n)$.}$$ Also ${\operatorname{map}}(G,k^n)$ is a right $k$-vector space by defining $(\phi
k)(x) = \phi(x)k$. For any subset $S\subset G$ and any subset $W\subset{\operatorname{map}}(G,k^n)$ let $$W\vert_S=\{f:S\to k^n \mid \exists g\in W \;\text{with} \; g\vert_S=f\}.$$ A right $k$-linear subspace $V\subset{\operatorname{map}}(G,k^n)$ is called *invariant* if $V$ is closed and invariant under the right $G$-action.

Elek defines the *average dimension* $\dim_G^{{\mathcal A}}(V)$ of an invariant subspace $V$ by choosing a Følner sequence $(F_n)_{n\in{{\mathbb N}}}$ of $G$ and setting $$\label{eq:average_dimension}
    \dim_G^{{\mathcal A}}(V)=\limsup_{n\to\infty}\frac{\dim_k \bigl(V\vert_{F_n}\bigr)}{|F_n|}.$$

The sequence in  converges and its limit $\dim_G^{{\mathcal A}}(V)$ is independent of the choice of the Følner sequence.

