The Gowers–Hatami theorem

This file proves the Gowers–Hatami stability theorem for approximate unitary representations of a finite group G, in the dimension-normalized Hilbert–Schmidt norm of MIPRE.Foundations.Distances: every ε-approximate representation ρ : G → U(ℂᵈ) is, on average over G, 2ε-close to the compression of an exact unitary representation on a larger space.

The proof follows the "regular representation" model, which avoids the group Fourier transform and the decomposition into irreducible representations. Given an approximate representation ρ, it uses

• the enlarged space L(G, ℂᵈ) of functions G → ℂᵈ with the uniform inner product, whose matrix index type is GowersHatami.Index G d = G × Fin d;
• the isometry V : ℂᵈ → L(G, ℂᵈ), V u = (x ↦ ρ(x) u) (GowersHatami.embedding, stored as the d × (G × d) matrix of its adjoint);
• the right regular representation ρ₀, (ρ₀(x) F)(y) = F (y * x) (GowersHatami.rightRegular).

The two identities driving the proof are that V is an isometry (GowersHatami.embedding_isometry) and that the compression of ρ₀(x) by V is the average 𝔼_y ρ(y)ᴴ ρ(y * x) (GowersHatami.compression_eq_average).

Main definitions

• MIPRE.IsApproxRepresentation: ε-approximate representations of a finite group, i.e. unitary-valued maps f with 𝔼_{x,y} Re ⟨f(x) f(y), f(xy)⟩_hs ≥ 1 - ε.

Main results

• MIPRE.gowers_hatami_prod: the Gowers–Hatami theorem, with the exact representation living on the concrete index type G × Fin d.
• MIPRE.gowers_hatami: the same statement with the enlarged space reindexed to Fin d' for some d' ≥ d (namely d' = |G| * d).

Implementation notes

• Matrices act on row vectors, so an operator H₁ → H₂ is stored as a H₁ × H₂-indexed matrix and the isometry condition for V reads V * Vᴴ = 1; the compression of an operator R on the enlarged space is V * R * Vᴴ.
• The approximation hypothesis is stated in correlation form (𝔼 Re ⟨f(x) f(y), f(xy)⟩_hs ≥ 1 - ε); for unitary-valued f this is equivalent to the defect form 𝔼 ‖f(x) f(y) - f(xy)‖²_hs ≤ 2ε by hsNormSq_sub_eq.
• No positivity assumption on ε and no positivity assumption on d are needed: all bounds on unitaries are stated as inequalities (hsNormSq U ≤ 1), which hold trivially when d = 0.
• The section "Hilbert–Schmidt norm toolkit" collects general facts about hsInner/hsNormSq; these are natural candidates to move into MIPRE.Foundations.Distances.

Hilbert–Schmidt norm toolkit

theorem MIPRE.hsInner_conj_symm {n : Type u_2} [Fintype n] (A B : Matrix n n ℂ) : star (hsInner A B) = hsInner B A

theorem MIPRE.hsInner_re_comm {n : Type u_2} [Fintype n] (A B : Matrix n n ℂ) : (hsInner B A).re = (hsInner A B).re

theorem MIPRE.hsNormSq_sub_eq {n : Type u_2} [Fintype n] (A B : Matrix n n ℂ) : hsNormSq (A - B) = hsNormSq A + hsNormSq B - 2 * (hsInner A B).re

Algebraic expansion of the squared Hilbert–Schmidt norm of a difference.

theorem MIPRE.hsNormSq_sub_le_of_le_one {n : Type u_2} [Fintype n] (A B : Matrix n n ℂ) (hA : hsNormSq A ≤ 1) (hB : hsNormSq B ≤ 1) : hsNormSq (A - B) ≤ 2 - 2 * (hsInner A B).re

If two matrices have squared Hilbert–Schmidt norm at most one, then the usual unitary distance/correlation identity becomes an inequality.

This is the form needed for compressions of unitaries: the compression need not be unitary, but it is enough to know its norm is bounded by one.

theorem MIPRE.hsNormSq_le_one_of_mem_unitaryGroup {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A ∈ Matrix.unitaryGroup n ℂ) : hsNormSq A ≤ 1

A unitary matrix has squared normalized Hilbert–Schmidt norm at most one (with equality as soon as the dimension is positive; the inequality also covers dimension zero).

theorem MIPRE.norm_average_le_one (G : Type u_1) [Group G] [Fintype G] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (F : G → E) (hF : ∀ (x : G), ‖F x‖ ≤ 1) : ‖(↑(Fintype.card G))⁻¹ • ∑ x : G, F x‖ ≤ 1

The average of vectors of norm at most one still has norm at most one.

theorem MIPRE.hsNormSq_average_le_one (G : Type u_1) [Group G] [Fintype G] {n : Type u_2} [Fintype n] [DecidableEq n] (F : G → Matrix n n ℂ) (hF : ∀ (x : G), hsNormSq (F x) ≤ 1) : hsNormSq ((↑(Fintype.card G))⁻¹ • ∑ x : G, F x) ≤ 1

The Hilbert–Schmidt unit ball is convex: an average of matrices of squared norm at most one has squared norm at most one. The proof equips matrices with the seminorm induced by the density matrix |n|⁻¹ • 1, for which hsNormSq is the squared norm, and applies the triangle inequality.

theorem MIPRE.average_two_sub_two_mul (G : Type u_1) [Group G] [Fintype G] (c : G → ℝ) : (∑ x : G, (2 - 2 * c x)) / ↑(Fintype.card G) = 2 - 2 * ((∑ x : G, c x) / ↑(Fintype.card G))

Averaging the affine expression 2 - 2 c_x.

Approximate representations

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

An ε-approximate representation of a finite group G (blueprint def:approx-rep) is a function f : G → U(ℂᵈ) whose multiplicativity defect, measured on average in the normalized Hilbert–Schmidt inner product, is at most ε: 𝔼_{x,y ∈ G} Re ⟨f(x) f(y), f(xy)⟩_hs ≥ 1 - ε.

Equations

• MIPRE.IsApproxRepresentation G f ε = ((∀ (x : G), f x ∈ Matrix.unitaryGroup (Fin d) ℂ) ∧ (∑ x : G, ∑ y : G, (MIPRE.hsInner (f x * f y) (f (x * y))).re) / ↑(Fintype.card G) ^ 2 ≥ 1 - ε)

Unitaries and reindexing

theorem MIPRE.unitary_col_sum {d : ℕ} (A : Matrix (Fin d) (Fin d) ℂ) (hA : A ∈ Matrix.unitaryGroup (Fin d) ℂ) (i j : Fin d) : ∑ k : Fin d, (starRingEnd ℂ) (A k i) * A k j = 1 i j

Column orthogonality for a unitary matrix.

theorem MIPRE.unitary_conjTranspose_mul {d : ℕ} {A B : Matrix (Fin d) (Fin d) ℂ} (hA : A ∈ Matrix.unitaryGroup (Fin d) ℂ) (hB : B ∈ Matrix.unitaryGroup (Fin d) ℂ) : A.conjTranspose * B ∈ Matrix.unitaryGroup (Fin d) ℂ

If A and B are unitary, then Aᴴ * B is unitary.

@[simp]

theorem MIPRE.matrix_reindex_one {n : Type u_2} {n' : Type u_3} [Fintype n] [Fintype n'] [DecidableEq n] [DecidableEq n'] (e : n ≃ n') : (Matrix.reindex e e) 1 = 1

noncomputable def MIPRE.reindexUnitary {n : Type u_2} {n' : Type u_3} [Fintype n] [Fintype n'] [DecidableEq n] [DecidableEq n'] (e : n ≃ n') (U : ↥(Matrix.unitaryGroup n ℂ)) : ↥(Matrix.unitaryGroup n' ℂ)

Reindexing a unitary matrix along an equivalence gives a unitary matrix.

Equations

• MIPRE.reindexUnitary e U = ⟨(Matrix.reindex e e) ↑U, ⋯⟩

@[simp]

theorem MIPRE.reindexUnitary_coe {n : Type u_2} {n' : Type u_3} [Fintype n] [Fintype n'] [DecidableEq n] [DecidableEq n'] (e : n ≃ n') (U : ↥(Matrix.unitaryGroup n ℂ)) : ↑(reindexUnitary e U) = (Matrix.reindex e e) ↑U

noncomputable def MIPRE.reindexUnitaryRep (G : Type u_1) [Group G] {n : Type u_2} {n' : Type u_3} [Fintype n] [Fintype n'] [DecidableEq n] [DecidableEq n'] (e : n ≃ n') (ρ₀ : G →* ↥(Matrix.unitaryGroup n ℂ)) : G →* ↥(Matrix.unitaryGroup n' ℂ)

Reindex a unitary representation along an equivalence of index types.

Equations

• MIPRE.reindexUnitaryRep G e ρ₀ = { toFun := fun (x : G) => MIPRE.reindexUnitary e (ρ₀ x), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MIPRE.reindexUnitaryRep_apply (G : Type u_1) [Group G] {n : Type u_2} {n' : Type u_3} [Fintype n] [Fintype n'] [DecidableEq n] [DecidableEq n'] (e : n ≃ n') (ρ₀ : G →* ↥(Matrix.unitaryGroup n ℂ)) (x : G) : ↑((reindexUnitaryRep G e ρ₀) x) = (Matrix.reindex e e) ↑(ρ₀ x)

@[simp]

theorem MIPRE.reindex_compression {d : ℕ} {n : Type u_2} {n' : Type u_3} [Fintype n] [Fintype n'] [DecidableEq n] [DecidableEq n'] (e : n ≃ n') (V : Matrix (Fin d) n ℂ) (R : Matrix n n ℂ) : (Matrix.reindex (Equiv.refl (Fin d)) e) V * (Matrix.reindex e e) R * ((Matrix.reindex (Equiv.refl (Fin d)) e) V).conjTranspose = V * R * V.conjTranspose

Reindexing the enlarged space preserves the compressed operator V * R * Vᴴ.

theorem MIPRE.reindex_isometry {d : ℕ} {n : Type u_2} {n' : Type u_3} [Fintype n] [Fintype n'] [DecidableEq n] [DecidableEq n'] (e : n ≃ n') (V : Matrix (Fin d) n ℂ) (hV : V * V.conjTranspose = 1) : (Matrix.reindex (Equiv.refl (Fin d)) e) V * ((Matrix.reindex (Equiv.refl (Fin d)) e) V).conjTranspose = 1

Reindexing the enlarged space preserves the isometry equation.

The regular representation model

@[reducible, inline]

abbrev MIPRE.GowersHatami.Index (G : Type u_2) (d : ℕ) : Type u_2

Matrix index for the enlarged space L(G, ℂᵈ), identified with G × Fin d.

Equations

• MIPRE.GowersHatami.Index G d = (G × Fin d)

noncomputable def MIPRE.GowersHatami.scale (G : Type u_2) [Fintype G] : ℂ

The normalization constant |G|^(-1/2) for the uniform inner product on L(G, ℂᵈ).

Equations

• MIPRE.GowersHatami.scale G = (↑√↑(Fintype.card G))⁻¹

theorem MIPRE.GowersHatami.scale_mul_self (G : Type u_2) [Fintype G] [Nonempty G] : scale G * scale G = (↑(Fintype.card G))⁻¹

The square of the normalization constant is 1 / |G|.

@[simp]

theorem MIPRE.GowersHatami.starRingEnd_scale (G : Type u_2) [Fintype G] : (starRingEnd ℂ) (scale G) = scale G

The normalization constant is real, hence fixed by complex conjugation.

noncomputable def MIPRE.GowersHatami.embedding {d : ℕ} (G : Type u_1) [Fintype G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) : Matrix (Fin d) (Index G d) ℂ

The isometry V : ℂᵈ → L(G, ℂᵈ), V u = (x ↦ ρ(x) u), stored as the d × (G × d) matrix of its adjoint: the (i, (x, j)) entry is |G|^(-1/2) times the (i, j) entry of ρ(x)ᴴ.

Equations

• MIPRE.GowersHatami.embedding G ρ i xj = MIPRE.GowersHatami.scale G * (starRingEnd ℂ) (ρ xj.1 xj.2 i)

def MIPRE.GowersHatami.rightShift {d : ℕ} (G : Type u_1) [Group G] (x : G) : Equiv.Perm (Index G d)

The right shift (y, i) ↦ (y * x, i) on the index of L(G, ℂᵈ); this is the permutation underlying the right regular representation (ρ₀(x) F)(y) = F (y * x).

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.GowersHatami.rightRegularMatrix {d : ℕ} (G : Type u_1) [Group G] [DecidableEq G] (x : G) : Matrix (Index G d) (Index G d) ℂ

The matrix of the right regular representation at x, acting on L(G, ℂᵈ).

Equations

• MIPRE.GowersHatami.rightRegularMatrix G x = Equiv.Perm.permMatrix ℂ (MIPRE.GowersHatami.rightShift G x)

theorem MIPRE.GowersHatami.rightShift_mul (G : Type u_2) [Group G] {d : ℕ} (x y : G) : rightShift G (x * y) = rightShift G y * rightShift G x

Right shifts compose contravariantly, as functions act on the right.

theorem MIPRE.GowersHatami.rightRegularMatrix_unitary {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (x : G) : rightRegularMatrix G x ∈ Matrix.unitaryGroup (Index G d) ℂ

The right regular matrix is unitary.

theorem MIPRE.GowersHatami.rightRegularMatrix_one (G : Type u_2) [Group G] [DecidableEq G] {d : ℕ} : rightRegularMatrix G 1 = 1

The identity element acts as the identity matrix.

theorem MIPRE.GowersHatami.rightRegularMatrix_mul {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (x y : G) : rightRegularMatrix G (x * y) = rightRegularMatrix G x * rightRegularMatrix G y

Right regular matrices multiply according to the group multiplication.

def MIPRE.GowersHatami.rightRegularUnitary {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (x : G) : ↥(Matrix.unitaryGroup (Index G d) ℂ)

The right regular matrix, bundled as a unitary matrix.

Equations

• MIPRE.GowersHatami.rightRegularUnitary G x = ⟨MIPRE.GowersHatami.rightRegularMatrix G x, ⋯⟩

noncomputable def MIPRE.GowersHatami.rightRegular (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (d : ℕ) : G →* ↥(Matrix.unitaryGroup (Index G d) ℂ)

The right regular representation of G on L(G, ℂᵈ), as a homomorphism into the unitary group.

Equations

• MIPRE.GowersHatami.rightRegular G d = { toFun := MIPRE.GowersHatami.rightRegularUnitary G, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MIPRE.GowersHatami.rightRegular_apply {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (x : G) : ↑((rightRegular G d) x) = rightRegularMatrix G x

@[simp]

theorem MIPRE.GowersHatami.rightRegularMatrix_mul_apply {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (x : G) (M : Matrix (Index G d) (Fin d) ℂ) (y : Index G d) (j : Fin d) : (rightRegularMatrix G x * M) y j = M (y.1 * x, y.2) j

Multiplying on the left by the right regular matrix shifts the row index: (R_x M)(y, i) = M(y * x, i).

@[simp]

theorem MIPRE.GowersHatami.rightRegularMatrix_mul_embedding_conjTranspose_apply {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (x : G) (y : Index G d) (j : Fin d) : (rightRegularMatrix G x * (embedding G ρ).conjTranspose) y j = scale G * ρ (y.1 * x) y.2 j

Applying the right regular matrix to Vᴴ evaluates ρ at the shifted group element.

theorem MIPRE.GowersHatami.embedding_mul_conjTranspose_apply {d : ℕ} (G : Type u_1) [Fintype G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (i j : Fin d) : (embedding G ρ * (embedding G ρ).conjTranspose) i j = ∑ x : G, scale G * scale G * ∑ k : Fin d, (starRingEnd ℂ) (ρ x k i) * ρ x k j

Entrywise expansion of V * Vᴴ. This is the only bookkeeping step in the isometry proof; embedding_isometry then just applies column orthogonality.

theorem MIPRE.GowersHatami.embedding_isometry {d : ℕ} (G : Type u_1) [Group G] [Fintype G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (hρ : ∀ (x : G), ρ x ∈ Matrix.unitaryGroup (Fin d) ℂ) : embedding G ρ * (embedding G ρ).conjTranspose = 1

The map V u = (x ↦ ρ(x) u) is an isometry.

theorem MIPRE.GowersHatami.compression_apply {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (x : G) (i j : Fin d) : (embedding G ρ * rightRegularMatrix G x * (embedding G ρ).conjTranspose) i j = ∑ y : G, ∑ k : Fin d, scale G * scale G * ((starRingEnd ℂ) (ρ y k i) * ρ (y * x) k j)

Entrywise expansion of the compression V * R_x * Vᴴ. compression_eq_average then packages this expansion as the average from the proof sketch.

theorem MIPRE.GowersHatami.compression_eq_average {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (x : G) : embedding G ρ * rightRegularMatrix G x * (embedding G ρ).conjTranspose = (↑(Fintype.card G))⁻¹ • ∑ y : G, (ρ y).conjTranspose * ρ (y * x)

The compression of the right regular representation by V is the average 𝔼_y ρ(y)ᴴ ρ(y * x).

theorem MIPRE.GowersHatami.compression_hsNormSq_le_one {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (x : G) (hρ : ∀ (y : G), ρ y ∈ Matrix.unitaryGroup (Fin d) ℂ) : hsNormSq (embedding G ρ * rightRegularMatrix G x * (embedding G ρ).conjTranspose) ≤ 1

Compression of a unitary has squared Hilbert–Schmidt norm at most one.

After rewriting the compression as an average, each summand is a product of unitaries, hence has norm at most one; the convexity lemma hsNormSq_average_le_one then gives the bound.

theorem MIPRE.GowersHatami.hsInner_compression {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (x : G) : hsInner (ρ x) (embedding G ρ * rightRegularMatrix G x * (embedding G ρ).conjTranspose) = (↑(Fintype.card G))⁻¹ * ∑ y : G, hsInner (ρ y * ρ x) (ρ (y * x))

Taking the Hilbert–Schmidt inner product against the compressed right regular action recovers the approximate-representation correlation, averaged over the auxiliary group element.

theorem MIPRE.GowersHatami.average_correlation {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (ε : ℝ) (hApprox : IsApproxRepresentation G ρ ε) : (∑ x : G, (hsInner (ρ x) (embedding G ρ * rightRegularMatrix G x * (embedding G ρ).conjTranspose)).re) / ↑(Fintype.card G) ≥ 1 - ε

The approximate-representation hypothesis gives high average correlation between ρ(x) and the compressed exact representation.

theorem MIPRE.GowersHatami.witness_reindex {d : ℕ} (G : Type u_1) [Group G] [Fintype G] {n : Type u_2} [Fintype n] [DecidableEq n] {d' : ℕ} (e : n ≃ Fin d') (hd_le : d ≤ d') (ρ : G → Matrix (Fin d) (Fin d) ℂ) (ε : ℝ) (V : Matrix (Fin d) n ℂ) (hV : V * V.conjTranspose = 1) (ρ₀ : G →* ↥(Matrix.unitaryGroup n ℂ)) (hprox : (∑ x : G, hsNormSq (ρ x - V * ↑(ρ₀ x) * V.conjTranspose)) / ↑(Fintype.card G) ≤ 2 * ε) : ∃ (d' : ℕ) (_ : d ≤ d') (V' : Matrix (Fin d) (Fin d') ℂ) (_ : V' * V'.conjTranspose = 1) (ρ₀' : G →* ↥(Matrix.unitaryGroup (Fin d') ℂ)), (∑ x : G, hsNormSq (ρ x - V' * ↑(ρ₀' x) * V'.conjTranspose)) / ↑(Fintype.card G) ≤ 2 * ε

Transport a Gowers–Hatami witness along an equivalence of the enlarged index type.

The Gowers–Hatami theorem

theorem MIPRE.gowers_hatami_prod {d : ℕ} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (ε : ℝ) (hApprox : IsApproxRepresentation G ρ ε) : ∃ (V : Matrix (Fin d) (GowersHatami.Index G d) ℂ) (_ : V * V.conjTranspose = 1) (ρ₀ : G →* ↥(Matrix.unitaryGroup (GowersHatami.Index G d) ℂ)), (∑ x : G, hsNormSq (ρ x - V * ↑(ρ₀ x) * V.conjTranspose)) / ↑(Fintype.card G) ≤ 2 * ε

The Gowers–Hatami theorem in the concrete enlarged space L(G, ℂᵈ).

This is the statement proved directly by the regular representation model: the exact representation is the right regular representation on L(G, ℂᵈ), and the isometry is u ↦ (x ↦ ρ(x) u).

theorem MIPRE.gowers_hatami {d : ℕ} (G : Type u_1) [Group G] [Fintype G] (ρ : G → Matrix (Fin d) (Fin d) ℂ) (ε : ℝ) (hApprox : IsApproxRepresentation G ρ ε) : ∃ (d' : ℕ) (_ : d ≤ d') (V : Matrix (Fin d) (Fin d') ℂ) (_ : V * V.conjTranspose = 1) (ρ₀ : G →* ↥(Matrix.unitaryGroup (Fin d') ℂ)), (∑ x : G, hsNormSq (ρ x - V * ↑(ρ₀ x) * V.conjTranspose)) / ↑(Fintype.card G) ≤ 2 * ε

The Gowers–Hatami theorem (blueprint thm:gowers-hatami). Let G be a finite group and ρ : G → U(ℂᵈ) an ε-approximate representation of G. Then there are a dimension d' ≥ d, an isometry V (given as a d × d' matrix with V * Vᴴ = 1), and an exact representation ρ₀ : G →* U(ℂ^d') such that 𝔼_x ‖ρ(x) - V ρ₀(x) Vᴴ‖²_hs ≤ 2ε.

The witness is the right regular representation on L(G, ℂᵈ), reindexed to Fin d' with d' = |G| * d.