Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Definition

LaTeX

Lemma

LaTeX

Definition 2.1.2$(\epsilon , \sigma )$-representation.

Given a finite group $G$, an integer $d \geq 1, \varepsilon \geq 0$, and a $d$-dimensional positive semidefinite matrix $\sigma $ with trace 1 , an $(\varepsilon , \sigma )$-representation of $G$ is a map $f: G \rightarrow U_{d}(\mathbb {C})$, to the $d \times d$ unitary matrices, such that

\begin{equation} \mathbb {E}_{x, y \in G} \Re \left(\left\langle f(x)^{*} f(y), f\left(x^{-1} y\right)\right\rangle _{\sigma }\right) \geq 1-\varepsilon , \end{equation}

where $\Re $ denotes taking real part of the inner product.

LaTeX Lean

Definition 1.1.2Additive characters

For $\alpha \in {\mathbb F}_q^n$, define the additive character $\chi _\alpha : {\mathbb F}_q^n\to {\mathbb C}$ by

\[ \chi _\alpha (x) := \omega _p^{{\rm Tr}(\langle \alpha , x \rangle )}, \]

where $\langle \alpha , x \rangle =\sum _{i=1}^n \alpha _i x_i\in {\mathbb F}_q$.

LaTeX

Definition 1.1.1Field trace

The field trace ${\rm Tr}: {\mathbb F}_q \to {\mathbb F}_p$ is

\[ {\rm Tr}(z) := \sum _{i=0}^{s-1} z^{p^i}. \]

LaTeX

Definition 1.1.13Finite-field BLR test

Given oracle access to $f:{\mathbb F}_q^n\to {\mathbb F}_q$, the finite-field BLR verifier ${}$

LaTeX

Definition 1.1.3Inner product and Fourier coefficient

For functions $h_1,h_2:{\mathbb F}_q^n\to {\mathbb C}$, define

\[ \langle h_1, h_2 \rangle := {\mathbb E}_{x\in {\mathbb F}_q^n}\left[h_1(x)\overline{h_2(x)}\right]. \]

For $h:{\mathbb F}_q^n\to {\mathbb C}$ and $\alpha \in {\mathbb F}_q^n$, define

\[ \widehat h(\alpha ) := \langle h, \chi _\alpha \rangle = {\mathbb E}_{x\in {\mathbb F}_q^n}\left[h(x)\overline{\chi _\alpha (x)}\right]. \]

LaTeX

Definition 1.1.6Fourier expansion of a finite-field-valued function

Let $f:{\mathbb F}_q^n\to {\mathbb F}_q$. For each $c\in {\mathbb F}_q^\times $, define

\[ {\varphi }_{c}(x) := \omega _p^{{\rm Tr}(c f(x))}. \]

The Fourier expansion of $f$ is the family

\[ \left\{ {\varphi }_{c}\right\} _{c\in {\mathbb F}_q^\times }. \]

LaTeX

Definition 1.1.9Linear functions

For $\alpha \in {\mathbb F}_q^n$, define $\ell _\alpha :{\mathbb F}_q^n\to {\mathbb F}_q$ by

\[ \ell _\alpha (x):=\langle \alpha , x \rangle . \]

The set of linear functions is

\[ {\text{$\mathcal{LIN}$}}:= \left\{ \ell _\alpha \mid \alpha \in {\mathbb F}_q^n\right\} . \]

The distance from $f:{\mathbb F}_q^n\to {\mathbb F}_q$ to linearity is

\[ \delta (f,{\text{$\mathcal{LIN}$}}):=\min _{\alpha \in {\mathbb F}_q^n}\delta (f,\ell _\alpha ). \]

LaTeX

Definition 1.1.8Relative Hamming distance

For $f,g:{\mathbb F}_q^n\to {\mathbb F}_q$, define

\[ \delta (f,g) := \Pr _{x\in {\mathbb F}_q^n}\left[f(x)\ne g(x)\right]. \]

LaTeX

Theorem 2.3.1Gowers-Hatami

Let $G$ be a finite group, $\varepsilon \geq 0$, and $f: G \rightarrow U_{d}(\mathbb {C})$ an $(\varepsilon , \sigma )$-representation of $G$. Then there exists a $d^{\prime } \geq d$, an isometry $V: \mathbb {C}^{d} \rightarrow \mathbb {C}^{d^{\prime }}$, and a representation $g: G \rightarrow U_{d^{\prime }}(\mathbb {C})$ such that

\begin{equation} \mathbb {E}_{x \in G}\left\| f(x)-V^{*} g(x) V\right\| _{\sigma }^{2} \leq 2 \varepsilon . \end{equation}

LaTeX Lean

Theorem 2.3.2Gowers-Hatami-2

Let $G$ be a finite group, $\varepsilon \geq 0$, and $\rho : G \rightarrow U(\mathcal{H})$ an $(\varepsilon , \sigma )$-representation of $G$ on space $\mathcal{H}=\mathbb {C}^{d}$. Then there exists an isometry $V: \mathcal{H} \rightarrow \mathcal{H}^\prime $ to a different space $\mathcal{H}^\prime $, and a representation $\rho ^\prime : G \rightarrow \mathcal{H}^\prime $ such that

\begin{equation} \mathbb {E}_{x \in G}\left\| \rho (x)-V^{*} \rho ^\prime (x) V\right\| _{\sigma }^{2} \leq 2 \varepsilon . \end{equation}

LaTeX Lean

Definition 2.2.6Group fourier transform

Let $f: G \rightarrow U_d(\mathbb {C})$ be a map and $\rho : G \rightarrow U_{d_{\rho }}(\mathbb {C})$ be a unitary irrep. The fourier transform of $f$ at the representation $\rho $ is denoted by $\hat{f}$:

\begin{equation} \hat{f}(\rho )=\mathbb {E}_{x \in G} f(x) \otimes \overline{\rho (x)}, \end{equation}

where $\overline{\rho (x)}$ denotes complex conjugate of $\rho (x)$.

LaTeX Lean

Lemma 1.1.14Completeness

If $f\in {}$

LaTeX

Lemma 1.1.4Character orthogonality

For every $\alpha ,\beta \in {\mathbb F}_q^n$,

\[ {\mathbb E}_{x\in {\mathbb F}_q^n}\left[\chi _\alpha (x)\overline{\chi _\beta (x)}\right] = \begin{cases} 1 & \text{if } \alpha =\beta ,\\ 0 & \text{if } \alpha \ne \beta . \end{cases} \]

Equivalently, ${\mathbb E}_x[\chi _\alpha (x)]=0$ for $\alpha \ne 0$ and equals $1$ for $\alpha =0$.

LaTeX

Lemma 1.1.7Character-sum indicator

For every $z\in {\mathbb F}_q$,

\[ \mathbbm {1}[z=0] = \frac{1}{q}\sum _{c\in {\mathbb F}_q}\omega _p^{{\rm Tr}(cz)}. \]

Consequently, for every $u,v\in {\mathbb F}_q$,

\[ \mathbbm {1}[u=v] = \frac{1}{q}\sum _{c\in {\mathbb F}_q}\omega _p^{{\rm Tr}(c(u-v))}. \]

LaTeX

Lemma 1.1.10Distance formula

Let $f,g:{\mathbb F}_q^n\to {\mathbb F}_q$. Let $\{ {\varphi }_{c}\} _{c\in {\mathbb F}_q^\times }$ and $\{ {\gamma }_{c}\} _{c\in {\mathbb F}_q^\times }$ be their Fourier expansions. Then

\[ \delta (f,g) = 1-\frac{1}{q}\left(1+ \sum _{c\in {\mathbb F}_q^\times } \langle {\varphi }_{c}, {\gamma }_{c} \rangle \right). \]

Equivalently,

\[ \delta (f,g) = 1-\frac{1}{q}\left(1+ \sum _{c\in {\mathbb F}_q^\times } \sum _{\alpha \in {\mathbb F}_q^n} \widehat{{\varphi }_{c}}(\alpha ) \overline{\widehat{{\gamma }_{c}}(\alpha )} \right). \]

LaTeX

Lemma 1.1.12Distance to linearity in Fourier form

Let $f:{\mathbb F}_q^n\to {\mathbb F}_q$ have Fourier expansion $\{ {\varphi }_{c}\} _{c\in {\mathbb F}_q^\times }$. Then

\[ \delta (f,{\text{$\mathcal{LIN}$}}) = 1-\frac{1}{q}\left(1+ \max _{\alpha \in {\mathbb F}_q^n} \sum _{c\in {\mathbb F}_q^\times } \widehat{{\varphi }_{c}}(c\alpha ) \right). \]

Moreover, for every $\alpha \in {\mathbb F}_q^n$, the quantity

\[ S_\alpha := \sum _{c\in {\mathbb F}_q^\times } \widehat{{\varphi }_{c}}(c\alpha ) \]

is real and satisfies $-1\le S_\alpha \le q-1$.

LaTeX

Lemma 1.1.15Exact BLR acceptance formula

Let $f:{\mathbb F}_q^n\to {\mathbb F}_q$ have Fourier expansion $\{ {\varphi }_{c}\} _{c\in {\mathbb F}_q^\times }$. For each $\alpha \in {\mathbb F}_q^n$, define

\[ S_\alpha := \sum _{c\in {\mathbb F}_q^\times } \widehat{{\varphi }_{c}}(c\alpha ). \]

Then

\[ \Pr [{\text{$\mathsf{V}_{\mathsf{BLR}}^f$ }}=1] = \frac{1}{q}\left(1+\frac{1}{(q-1)^2} \sum _{\alpha \in {\mathbb F}_q^n} S_\alpha ^3 \right). \]

LaTeX

Lemma 1.1.5Fourier inversion and Parseval

For every function $h:{\mathbb F}_q^n\to {\mathbb C}$,

\[ h(x)=\sum _{\alpha \in {\mathbb F}_q^n}\widehat h(\alpha )\chi _\alpha (x) \quad \text{for every }x\in {\mathbb F}_q^n, \]

and

\[ \sum _{\alpha \in {\mathbb F}_q^n}\left\lvert {\widehat h(\alpha )}\right\rvert ^2 = {\mathbb E}_{x\in {\mathbb F}_q^n}\left[\left\lvert {h(x)}\right\rvert ^2\right]. \]

In particular, if $\left\lvert {h(x)}\right\rvert =1$ for every $x$, then $\sum _{\alpha \in {\mathbb F}_q^n}\left\lvert {\widehat h(\alpha )}\right\rvert ^2=1$.

LaTeX

Lemma 1.1.11Fourier expansion of a linear function

Fix $\alpha \in {\mathbb F}_q^n$ and $c\in {\mathbb F}_q^\times $. Let $\lambda _{c}(x):=\omega _p^{{\rm Tr}(c\ell _\alpha (x))}$. Then

\[ \lambda _{c}=\chi _{c\alpha }. \]

Equivalently, for every $\beta \in {\mathbb F}_q^n$,

\[ \widehat{\lambda _{c}}(\beta ) = \begin{cases} 1 & \text{if } \beta =c\alpha ,\\ 0 & \text{if } \beta \ne c\alpha . \end{cases} \]

LaTeX

Lemma 1.1.16Second moment bound

With $S_\alpha $ as in lemma 1.1.15,

\[ \sum _{\alpha \in {\mathbb F}_q^n} S_\alpha ^2 \le (q-1)^2. \]

LaTeX

Definition 3.1.1

For a field $\mathbb {F}$ and parameters $m, n \in \mathbb {N}$, we define the language

\[ \mathrm{LINEQ}(\mathbb {F},m,n) := \{ (M, c) \in \mathbb {F}^{m\times n} \times \mathbb {F}^{m} \mid \exists b\in \mathbb {F}^n, \, Mb = c \} . \]

LaTeX Lean

Definition 3.1.2

Let $V_{\mathrm{LINEQ}(\mathbb {F},m,n)}^{\langle b, \cdot \rangle } (M,c)$ be the LPCP verifier defined as follows:

Sample $r \leftarrow \mathbb {F}^m$.
Query $b\in \mathbb {F}^n $ at $u:= M^{\intercal }r \in \mathbb {F}^n$.
Accept if and only if $\langle b,u\rangle = \langle c, r\rangle $.

LaTeX Lean

Theorem 3.1.3

\[ \mathrm{LINEQ}(\mathbb {F},m,n) \in \mathrm{LPCP}\left[\varepsilon _c=0, \varepsilon _s= 1 / |\mathbb {F}|, \Sigma = \mathbb {F}, \ell = |x|, q = 1, r = m \log |\mathbb {F}|\right]. \]

LaTeX Lean

Definition 3.0.6

A language $L \subseteq \{ 0,1\} ^*$ is in $\mathrm{LPCP}[\varepsilon _c, \varepsilon _s, \Sigma , \ell , q, r]$ if there exists a polynomial-time LPCP verifier $V$ such that for every $x \in \{ 0,1\} ^*$, $V$ makes at most $q(|x|)$ queries to the linear proof oracle, uses at most $r(|x|)$ bits of randomness, and the following holds:

Completeness: If $x \in L$, then $\exists \pi \in \Sigma ^{\ell (|x|)}, \, \Pr \left[V^{\langle \pi , \cdot \rangle }(x)=1 \right] \geq 1 - \varepsilon _c$.
Soundness: If $x \notin L$, then $\forall \widetilde{\pi } \in \Sigma ^{\ell (|x|)},\, \Pr \left[V^{\langle \widetilde{\pi }, \cdot \rangle }(x)=1 \right] \leq \varepsilon _s$.

LaTeX Lean

Definition 3.0.5

A LPCP verifier is a probabilistic oracle Turing machine $V$ with query access to a linear function $\langle \pi ,\cdot \rangle : \Sigma ^{\ell (|x|)} \to \Sigma $.

LaTeX Lean

Theorem 2.2.3Maschke’s theorem

Let $G$ be a finite group and let $\rho : G \to \mathrm{GL}(V)$ be a finite-dimensional representation over $\mathbb {C}$. Then $\rho $ is completely reducible. In particular, there exists a decomposition

\begin{equation} \rho \cong \bigoplus _{m} r_m \, \rho _m, \end{equation}

where $\{ \rho _m\} $ is a set of inequivalent irreducible representations of $G$, and $r_m \in \mathbb {Z}^+$ are the multiplicities.

LaTeX Lean

Definition 3.0.3

A language $L \subseteq \{ 0,1\} ^*$ is in $\mathrm{PCP}[\varepsilon _c, \varepsilon _s, \Sigma , \ell , q, r]$ if there exists a polynomial-time PCP verifier $V$ such that for every $x \in \{ 0,1\} ^*$, $V$ makes at most $q(|x|)$ queries to the proof oracle, uses at most $r(|x|)$ bits of randomness, and the following holds:

Completeness: If $x \in L$, then $\exists \pi \in \Sigma ^{\ell (|x|)}, \, \Pr \left[V^\pi (x)=1 \right] \geq 1 - \varepsilon _c$.
Soundness: If $x \notin L$, then $\forall \widetilde{\pi } \in \Sigma ^{\ell (|x|)},\, \Pr \left[V^{\widetilde{\pi }}(x)=1 \right] \leq \varepsilon _s$.

LaTeX Lean

Definition 3.0.2

A PCP verifier is a probabilistic oracle Turing machine $V$ with query access to a function $\pi : [\ell (|x|)] \to \Sigma $.

LaTeX Lean

Definition 3.0.1

A system of $m$ quadratic equations in $n$ variables over a field $\mathbb {F}$ is a list of polynomials $p_1, \ldots , p_m \in \mathbb {F}[x_1, \ldots , x_n]$ where each $p_i$ has total degree at most $2$.

\[ \mathrm{QESAT}(\mathbb {F},n) := \{ (p_1, \ldots , p_m) \mid \exists a_1, \ldots , a_n \in \mathbb {F}, \, \forall i \in [m], \, p_i(a_1, \ldots , a_n) = 0 \} . \]

LaTeX Lean

Theorem 3.0.4

\[ \mathrm{QESAT}(\mathbb {F}_2,n) \in \mathrm{PCP}[ \varepsilon _c = 0, \varepsilon _s = 1/2, \Sigma = \mathbb {F}_2, \ell = \exp (|x|), q = O(1), r = |x|^{O(1)} ]. \]

LaTeX Lean

Proposition 2.2.4Decomposition of the regular representation

Let $R : G \to \mathrm{GL}(\mathbb {C}[G])$ be the regular representation of a finite group $G$. Then

\begin{equation} R \cong \bigoplus _{\rho \in \widehat{G}} d_\rho \, \rho , \end{equation}

where $\widehat{G}$ is a complete set of inequivalent irreducible representations of $G$, and $d_\rho = \dim (V_\rho )$ is the dimension of $\rho $.

LaTeX Lean

Proposition 2.2.5Character of regular representation.

Let $G$ be a finite group and $\sum _\rho $ denotes summing over the complete set of inequivalent irreps $\hat{G}$

\begin{equation} \label{eq:regular_repr_characterr} \sum _{\rho \in \hat{G}} d_{\rho } \operatorname {Tr}(\rho (x))=|G| \delta _{x, e}. \end{equation}

LaTeX Lean

Definition 2.2.2Regular representation

Let $R: G \rightarrow \mathbb {C}[G]$ be a regular representation where $\{ \mbox{$ | g \rangle $}, g\in G\} $ forms a basis of $\mathbb {C}[G]$. The representation is given by

\begin{equation} R(x) \mbox{$ | g \rangle $} = \mbox{$ | xg \rangle $}. \end{equation}

LaTeX Lean

Definition 2.1.1$\sigma $ inner product.

The $\sigma $ inner product between matrices $A$ and $B$ is defined as

\begin{equation} \langle A, B \rangle _{\sigma } = {\rm Tr}(A^* B \sigma ), \end{equation}

where $\sigma \geq 0$ and $A^*$ denotes conjugate-transpose.

LaTeX Lean

Definition 3.2.2

For a field $\mathbb {F}$ and $n \in \mathbb {N}$, define the tensor test language

\[ \mathrm{TENSORQ}(\mathbb {F}, n) := \bigl\{ (a, b) \in \mathbb {F}^n \times \mathbb {F}^{n^2} \mid b = \mathrm{flat}(a \otimes a) \bigr\} . \]

LaTeX

Theorem 3.2.3

For every finite field $\mathbb {F}$ and $n \in \mathbb {N}$,

\[ \mathrm{TENSORQ}(\mathbb {F}, n) \in \mathrm{LPCP}\! \left[ \varepsilon _c = 0,\; \varepsilon _s = \frac{2|\mathbb {F}|-1}{|\mathbb {F}|^2},\; \Sigma = \mathbb {F},\; \ell = n + n^2,\; q = 2,\; r = 2n \cdot \log (|\mathbb {F}|) \right]. \]

LaTeX

Corollary 3.2.4

\[ \mathrm{TENSORQ}(\mathbb {F}_2, n) \in \mathrm{LPCP}\! \left[ \varepsilon _c = 0,\; \varepsilon _s = \frac{3}{4},\; \Sigma = \mathbb {F}_2,\; \ell = n + n^2,\; q = 2,\; r = 2 \log (2) \cdot n \right]. \]

LaTeX

Definition 3.2.1

For a field $\mathbb {F}$, vectors $a \in \mathbb {F}^n$ and $b \in \mathbb {F}^m$, the tensor product $a \otimes b \in \mathbb {F}^{n \times m}$ is the matrix defined by

\[ (a \otimes b)_{i,j} := a_i \cdot b_j \quad \forall i \in [n],\, j \in [m]. \]

We write $\mathrm{flat}(a \otimes b) \in \mathbb {F}^{n \cdot m}$ for the row-concatenation of $a \otimes b$.

LaTeX

Theorem 1.1.17Soundness of the finite-field BLR test

For every function $f:{\mathbb F}_q^n\to {\mathbb F}_q$,

\[ \Pr [{\text{$\mathsf{V}_{\mathsf{BLR}}^f$ }}=0] \ge \delta (f,{\text{$\mathcal{LIN}$}}). \]

Equivalently,

\[ \Pr [{\text{$\mathsf{V}_{\mathsf{BLR}}^f$ }}=1] \le 1-\delta (f,{\text{$\mathcal{LIN}$}}). \]

LaTeX

Definition 2.2.1Unitary Representation

A unitary representation of $G$ is a representation to unitary matrices $\rho : G \to U(V)$.

LaTeX Lean

Proposition 2.1.3

Let $G$ be a finite group, and let $f, f_2 : G \to U(n)$ be functions into the unitary matrices. Then

\[ \mathbb {E}_{x \in G}\| f(x) - f_2(x)\| _\sigma ^2 \le 2\varepsilon \quad \Longleftrightarrow \quad \mathbb {E}_{x \in G} \Re \! \left(\langle f(x), f_2(x)\rangle _\sigma \right) \ge 1 - \varepsilon . \]

LaTeX Lean