Gowers–Hatami Stability Theorem

This file formalises the definitions and statements from the chapter on approximate representations and the Gowers–Hatami theorem.

Sections

• SigmaInnerProduct — the σ-weighted inner product on matrices
• RepresentationTheory — standard representation-theoretic notions
• GowersHatami — the main stability theorem

Section 1: Preliminaries

σ inner product

[ \langle A, B \rangle_{\sigma} = \operatorname{Tr}(A^* B \sigma) ] where $\sigma \geq 0$ is a positive semidefinite matrix of trace 1.

Note: Matrix.PosSemidef requires [PartialOrder R] on the scalar field. For ℂ, this is provided by opening the ComplexOrder locale (from Mathlib.Analysis.Complex.Basic), which gives ℂ the partial order $z \leq w \iff z.\mathrm{re} \leq w.\mathrm{re} \wedge z.\mathrm{im} = w.\mathrm{im}$.

noncomputable def sigmaInner {n : ℕ} (σ A B : Matrix (Fin n) (Fin n) ℂ) : ℂ

Equations

• sigmaInner σ A B = (A.conjTranspose * B * σ).trace

noncomputable def sigmaNormSq {n : ℕ} (σ A : Matrix (Fin n) (Fin n) ℂ) : ℝ

Equations

• sigmaNormSq σ A = (sigmaInner σ A A).re

Identity for unitary matrices

For unitary matrices $A, B$ and a state $\sigma$, [ |A - B|\sigma^2 = 2 - 2,\Re\langle A, B\rangle\sigma. ]

theorem sigmaNormSq_sub_unitary {d : ℕ} (σ A B : Matrix (Fin d) (Fin d) ℂ) (hσ : σ.PosSemidef) (hσtr : σ.trace = 1) (hA : A ∈ Matrix.unitaryGroup (Fin d) ℂ) (hB : B ∈ Matrix.unitaryGroup (Fin d) ℂ) : sigmaNormSq σ (A - B) = 2 - 2 * (sigmaInner σ A B).re

ε-proximity in σ-norm vs. inner product

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

theorem sigma_proximity_iff {d : ℕ} (G : Type u_1) [Group G] [Fintype G] (σ : Matrix (Fin d) (Fin d) ℂ) (f f₂ : G → Matrix (Fin d) (Fin d) ℂ) (ε : ℝ) : (∑ x : G, sigmaNormSq σ (f x - f₂ x)) / ↑(Fintype.card G) ≤ 2 * ε ↔ (∑ x : G, (sigmaInner σ (f x) (f₂ x)).re) / ↑(Fintype.card G) ≥ 1 - ε

Section 2: Approximate Representations

(ε, σ)-representation

Given a finite group $G$, an integer $d \ge 1$, $\varepsilon \ge 0$, and a $d$-dimensional density matrix $\sigma$, an $(\varepsilon, \sigma)$-representation of $G$ is a map $f : G \to U_d(\mathbb{C})$ such that [ \mathbb{E}{x,y \in G} \Re!\left(\langle f(x)^* f(y),, f(x^{-1}y)\rangle\sigma\right) \ge 1 - \varepsilon. ]

def IsApproxRepresentation {d : ℕ} (G : Type u_1) [Group G] [Fintype G] (σ : Matrix (Fin d) (Fin d) ℂ) (f : G → Matrix (Fin d) (Fin d) ℂ) (ε : ℝ) : Prop

Equations

• IsApproxRepresentation G σ f ε = ((∑ x : G, ∑ y : G, (sigmaInner σ (f x * f y) (f (x * y))).re) / ↑(Fintype.card G) ^ 2 ≥ 1 - ε)

Section 3: Representation Theory

Representation

A representation of a group $G$ on a finite-dimensional $\mathbb{C}$-vector space $V$ is a group homomorphism $\rho : G \to \mathrm{GL}(V)$, i.e. [ \rho(xy) = \rho(x)\rho(y) \quad \text{for all } x, y \in G. ]

@[reducible, inline]

abbrev UnitaryRep (G : Type u_2) [Group G] (d : ℕ) : Type u_2

Equations

• UnitaryRep G d = (G →* ↥(Matrix.unitaryGroup (Fin d) ℂ))

Irreducible representation

A representation $\rho : G \to \mathrm{GL}(V)$ is irreducible if the only $G$-invariant subspaces of $V$ are $\{0\}$ and $V$ itself.

Character

The character of a representation $\rho$ is [ \chi_\rho(x) = \operatorname{Tr}[\rho(x)]. ]

noncomputable def UnitaryRep.character (G : Type u_1) [Group G] {d : ℕ} (ρ : UnitaryRep G d) : G → ℂ

Equations

• UnitaryRep.character G ρ x = (↑(ρ x)).trace

Maschke theorem

Finite dimensional representations of finite groups are completely reducible: every representation can be decomposed into a direct sum of irreducible representations. [ \rho \cong \bigoplus_{m} r_m \cdot \rho_m, ] where $\rho_m$ are the irreducible representations of $G$ and $r_m$ are their multiplicities.

theorem Maschke {d : ℕ} (G : Type u_1) [Group G] [Fintype G] (ρ : UnitaryRep G d) : ∃ (σ : UnitaryRep G d), True

Regular representation

The regular representation $R : G \to \mathbb{C}[G]$ acts by left multiplication: [ R(x),|g\rangle = |xg\rangle. ]

noncomputable def regularRep (G : Type u_1) [Group G] : G →* (G →₀ ℂ) →ₗ[ℂ] G →₀ ℂ

Equations

• regularRep G = { toFun := fun (x : G) => Finsupp.lmapDomain ℂ ℂ fun (x_1 : G) => x * x_1, map_one' := ⋯, map_mul' := ⋯ }

Character of the regular representation

[ \sum_{\rho \in \hat G} d_\rho, \operatorname{Tr}(\rho(x)) = |G|,\delta_{x,e}. ]

theorem regular_repr_character (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (irreps : Finset ((d : ℕ) × UnitaryRep G d)) (x : G) : ∑ p ∈ irreps, ↑p.fst * UnitaryRep.character G p.snd x = ↑(if x = 1 then Fintype.card G else 0)

Dimension formula

theorem sum_dim_sq_eq_card (G : Type u_1) [Group G] [Fintype G] (irreps : Finset ((d : ℕ) × UnitaryRep G d)) : ∑ p ∈ irreps, p.fst ^ 2 = Fintype.card G

The sum of squares of dimensions of irreducible representations satisfies [ \sum_{\rho \in \hat G} d_\rho^2 = |G|. ]

Section 4: Group Fourier Transform

Group Fourier transform

For $f : G \to U_d(\mathbb{C})$ and an irrep $\rho : G \to U_{d_\rho}(\mathbb{C})$, the Fourier transform of $f$ at $\rho$ is [ \hat f(\rho) = \mathbb{E}_{x \in G}, f(x) \otimes \overline{\rho(x)}. ]

noncomputable def groupFourierTransform {d : ℕ} (G : Type u_1) [Group G] [Fintype G] {dρ : ℕ} (f : G → Matrix (Fin d) (Fin d) ℂ) (ρ : UnitaryRep G dρ) : Matrix (Fin d × Fin dρ) (Fin d × Fin dρ) ℂ

Equations

• groupFourierTransform G f ρ = (↑(Fintype.card G))⁻¹ • ∑ x : G, (f x).kronecker ((↑(ρ x)).map ⇑(starRingEnd ℂ))

Section 5: Gowers–Hatami Theorem

Gowers–Hatami Theorem

Let $G$ be a finite group, $\varepsilon \ge 0$, and $f : G \to U_d(\mathbb{C})$ an $(\varepsilon, \sigma)$-representation of $G$. Then there exist $d' \ge d$, an isometry $V : \mathbb{C}^d \to \mathbb{C}^{d'}$, and an exact representation $g : G \to U_{d'}(\mathbb{C})$ such that [ \mathbb{E}{x \in G},|f(x) - V^* g(x) V|\sigma^2 \le 2\varepsilon. ]

Proof sketch. The isometry is defined by [ V u = \bigoplus_\rho d_\rho^{1/2} \sum_{i=1}^{d_\rho} \bigl(\hat f(\rho)(u \otimes e_i)\bigr) \otimes e_i, ] and the exact representation by [ g(x) = \bigoplus_\rho \bigl(I_d \otimes I_{d_\rho} \otimes \rho(x)\bigr). ] Both ingredients rely on the character identity for the regular representation (Fact character_regular_rep):

1. $V^* V = I_d$ (isometry).
2. $V^* g(x) V = \mathbb{E}_z f(z)^* f(zx)$ for all $x \in G$.

theorem gowers_hatami {d : ℕ} (G : Type u_1) [Group G] [Fintype G] (σ : Matrix (Fin d) (Fin d) ℂ) (hσ : σ.PosSemidef) (hσtr : σ.trace = 1) (f : G → Matrix (Fin d) (Fin d) ℂ) (ε : ℝ) (hε : 0 ≤ ε) (hf : IsApproxRepresentation G σ f ε) : ∃ (d' : ℕ) (_ : d ≤ d') (V : Matrix (Fin d) (Fin d') ℂ) (_ : V.conjTranspose * V = 1) (g : G →* ↥(Matrix.unitaryGroup (Fin d') ℂ)), (∑ x : G, sigmaNormSq σ (f x - V * ↑(g x) * V.conjTranspose)) / ↑(Fintype.card G) ≤ 2 * ε