The rank of the inner-product matrix

The sign matrix H of the inner product modulo two of bit strings indexed by ι, with entry (-1) ^ (x ⬝ᵥ y) at x and y, is a Hadamard matrix: H H = 2 ^ |ι| I (signMatrix_dotProduct_mul_self), by character orthogonality ∑_y (-1) ^ (w ⬝ᵥ y) = 2 ^ |ι| [w = 0] (BitString.sum_ite_dotProduct); as H is symmetric with entries ±1, it is a Hadamard matrix in the sense of Mathlib's Matrix.IsHadamard (isHadamard_signMatrix_dotProduct). So over a field in which 2 is invertible it has full rank 2 ^ |ι| (rank_signMatrix_dotProduct), and the 0/1 communication matrix of the inner product, whose rank differs from that of H by at most one and which has a zero row, has rank exactly 2 ^ |ι| - 1 (rank_communicationMatrix_dotProduct) Kushilevitz and Nisan, Chapter 1.

By the rank bound, a protocol computing the inner product has at least 2 ^ |ι| - 1 leaves labelled true (two_pow_sub_one_le_card_true_leaves_of_run_eq_dotProduct). The area bound |A| |B| ≤ 2 ^ |ι| for rectangles on which the inner product is constant, from which two_pow_lt_leaves_of_run_eq_dotProduct follows, gives only about half as many.

Main results

• Cslib.Communication.signMatrix_dotProduct_mul_self, Cslib.Communication.isHadamard_signMatrix_dotProduct: the sign matrix of the inner product is a Hadamard matrix.
• Cslib.Communication.rank_signMatrix_dotProduct: it has full rank.
• Cslib.Communication.rank_communicationMatrix_dotProduct: the communication matrix of the inner product has rank 2 ^ |ι| - 1.
• Cslib.Communication.two_pow_sub_one_le_card_true_leaves_of_run_eq_dotProduct: a protocol computing the inner product has at least 2 ^ |ι| - 1 leaves labelled true.

References

• E. Kushilevitz and N. Nisan, Communication Complexity

theorem Cslib.Communication.signMatrix_dotProduct_mul_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] (R : Type u_2) [Ring R] : ((signMatrix R fun (x y : ι → Bool) => x ⬝ᵥ y) * signMatrix R fun (x y : ι → Bool) => x ⬝ᵥ y) = 2 ^ Fintype.card ι • 1

The square of the sign matrix of the inner product is 2 ^ |ι| times the identity.

theorem Cslib.Communication.isHadamard_signMatrix_dotProduct {ι : Type u_1} [Fintype ι] [DecidableEq ι] (R : Type u_2) [Ring R] [StarRing R] : (signMatrix R fun (x y : ι → Bool) => x ⬝ᵥ y).IsHadamard

The sign matrix of the inner product is a Hadamard matrix in the sense of Matrix.IsHadamard: its entries ±1 are unitary, and it is symmetric with square 2 ^ |ι| times the identity.

theorem Cslib.Communication.rank_signMatrix_dotProduct {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [Field R] [NeZero 2] : (signMatrix R fun (x y : ι → Bool) => x ⬝ᵥ y).rank = 2 ^ Fintype.card ι

Over a field in which 2 is invertible, the sign matrix of the inner product on bit strings indexed by ι has full rank 2 ^ |ι|.

theorem Cslib.Communication.rank_communicationMatrix_dotProduct {ι : Type u_1} [Fintype ι] [DecidableEq ι] {R : Type u_2} [Field R] [NeZero 2] : (communicationMatrix R fun (x y : ι → Bool) => x ⬝ᵥ y).rank = 2 ^ Fintype.card ι - 1

The rank of the inner-product matrix Kushilevitz and Nisan, Chapter 1: over a field in which 2 is invertible, such as ℚ or ℝ, the communication matrix of the inner product modulo two on bit strings indexed by ι has rank 2 ^ |ι| - 1.

theorem Cslib.Communication.two_pow_sub_one_le_card_true_leaves_of_run_eq_dotProduct {ι : Type u_1} [Fintype ι] {p : Protocol (ι → Bool) (ι → Bool) Bool} (hp : p.run = fun (x y : ι → Bool) => x ⬝ᵥ y) : 2 ^ Fintype.card ι - 1 ≤ {i : Fin p.leaves | p.leafOutput i = true}.card

A protocol computing the inner product has at least 2 ^ |ι| - 1 leaves labelled true, by the rank bound and rank_communicationMatrix_dotProduct.