Lindsey's lemma over 𝔽₂

Read an element z of 𝔽₂ = ZMod 2 as the sign (-1) ^ z. For a matrix B over 𝔽₂ with rows indexed by α and columns by β, sets P and Q of vectors, and weights g and h of absolute value at most one,

(∑_{p ∈ P} ∑_{q ∈ Q} g(p) h(q) (-1)^{p ⬝ᵥ B q})² · 2^{rank B} ≤ |P| |Q| 2^{|α|} 2^{|β|}

(Matrix.sq_sum_bilinear_mul_two_pow_rank_le). This is Lindsey's lemma: a bilinear form of large rank is nearly balanced on every large combinatorial rectangle Jukna, Ch. 14. For a square B of full rank the sign matrix (-1)^{p ⬝ᵥ B q} is a Hadamard matrix, and the bound is Lindsey's bound |P| |Q| 2^{|α|} on its sums over rectangles; the rank refines it.

The proof is Cauchy–Schwarz over p, character orthogonality ∑_p (-1)^{p ⬝ᵥ v} = 2^{|α|} [v = 0] (Matrix.sum_neg_one_pow_val_dotProduct), and the count |{q' : B q' = B q}| = 2^{|β| - rank B} of a fibre of B (Matrix.card_ker_mul_two_pow_rank).

Main results

• ZMod.neg_one_pow_val_add: the sign of a sum in 𝔽₂ is the product of the signs.
• Matrix.sum_neg_one_pow_val_dotProduct: character orthogonality.
• Matrix.card_ker_mul_two_pow_rank: the kernel of a matrix over 𝔽₂ has 2^{|β| - rank} elements.
• Matrix.sq_sum_bilinear_mul_two_pow_rank_le: Lindsey's lemma.

References

• S. Jukna, Extremal Combinatorics, Ch. 14

theorem ZMod.neg_one_pow_val_add {R : Type u_1} [Ring R] (a b : ZMod 2) : (-1) ^ (a + b).val = (-1) ^ a.val * (-1) ^ b.val

The sign of a sum in 𝔽₂ is the product of the signs.

theorem Matrix.sum_neg_one_pow_val_dotProduct {α : Type u_1} [Fintype α] [DecidableEq α] (v : α → ZMod 2) : ∑ p : α → ZMod 2, (-1) ^ (p ⬝ᵥ v).val = if v = 0 then 2 ^ Fintype.card α else 0

Character orthogonality over 𝔽₂. The signs (-1)^{p ⬝ᵥ v} cancel over all p unless v = 0.

theorem Matrix.card_filter_mulVec_eq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (B : Matrix α β (ZMod 2)) (q : β → ZMod 2) : {z : β → ZMod 2 | B.mulVec z = B.mulVec q}.card = {z : β → ZMod 2 | B.mulVec z = 0}.card

All fibres of a linear map have the size of its kernel.

theorem Matrix.card_ker_mul_two_pow_rank {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (B : Matrix α β (ZMod 2)) : {z : β → ZMod 2 | B.mulVec z = 0}.card * 2 ^ B.rank = 2 ^ Fintype.card β

The kernel of a matrix over 𝔽₂ has 2^{|β| - rank B} elements.

theorem Matrix.sq_sum_bilinear_mul_two_pow_rank_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (B : Matrix α β (ZMod 2)) (P : Finset (α → ZMod 2)) (Q : Finset (β → ZMod 2)) (g : (α → ZMod 2) → ℝ) (h : (β → ZMod 2) → ℝ) (hg : ∀ (p : α → ZMod 2), |g p| ≤ 1) (hh : ∀ (q : β → ZMod 2), |h q| ≤ 1) : (∑ p ∈ P, ∑ q ∈ Q, g p * h q * (-1) ^ (p ⬝ᵥ B.mulVec q).val) ^ 2 * 2 ^ B.rank ≤ ↑P.card * ↑Q.card * 2 ^ Fintype.card α * 2 ^ Fintype.card β

Lindsey's lemma over 𝔽₂. For a matrix B over 𝔽₂, sets P and Q of vectors, and weights g and h of absolute value at most one, (∑_{p ∈ P} ∑_{q ∈ Q} g(p) h(q) (-1)^{p ⬝ᵥ B q})² · 2^{rank B} ≤ |P| |Q| 2^{|α|} 2^{|β|}.