The Hamming weight of a vector \(x : \operatorname {Fin} n \to \mathbb {F}_2\), denoted \(|x|\), is the number of nonzero entries of \(x\). This is the specialization of hammingNorm from Mathlib to vectors over \(\mathbb {F}_2\).

A matrix \(A \in \mathbb {F}_2^{m \times n}\) is called \((\alpha , \beta )\)-expanding, where \(\alpha , \beta \in \mathbb {R}\), if the following conditions hold:

1. \(0 {\lt} \alpha \leq 1\),

2. \(0 {\lt} \beta \),

3. for every vector \(x \in \mathbb {F}_2^n\) satisfying \(|x| \leq \alpha \cdot n\), we have \(|Ax| \geq \beta \cdot |x|\),

where \(|\cdot |\) denotes the Hamming weight, and \(Ax\) denotes the matrix-vector product \(A \cdot x\) over \(\mathbb {F}_2\).

Formally, \(\operatorname {IsExpanding}(A, \alpha , \beta )\) holds if and only if