Monochromatic rectangles for the Hadamard code

The existing BitString.hadamardCode x y is the inner product modulo two. Lindsey's lemma bounds its signed sum over a rectangle A × B of bit strings indexed by ι by √(|A| |B| 2 ^ |ι|) in absolute value (BitString.sq_sum_signVal_dotProduct_le). So if it is constant on A × B, the rectangle has at most 2 ^ Fintype.card ι entries. Empty sides, zero coordinates, and both constant values are included.

The proof specializes Lindsey's bilinear bound to the identity matrix after the standard ring equivalence between Boolean values and ZMod 2; it introduces no alternative inner product.

Main results

• Cslib.BitString.sq_sum_signVal_dotProduct_le: Lindsey's lemma for signed sums of the inner product over rectangles.
• Cslib.BitString.card_mul_le_two_pow_of_hadamardCode_eq: the Hadamard rectangle bound.

References

• S. Jukna, Extremal Combinatorics, Ch. 14
• [Threshold Circuits as Decision Trees and Finite-State Programs, Lemma 2.4] [26]

theorem Cslib.BitString.sq_sum_signVal_dotProduct_le {ι : Type u_1} [Fintype ι] (A B : Finset (ι → Bool)) : (∑ x ∈ A, ∑ y ∈ B, signVal (x ⬝ᵥ y)) ^ 2 ≤ ↑A.card * ↑B.card * 2 ^ Fintype.card ι

Lindsey's lemma for the inner product: the signed sum of the inner product modulo two over a rectangle A × B of bit strings indexed by ι is at most √(|A| |B| 2 ^ |ι|) in absolute value.

theorem Cslib.BitString.card_mul_le_two_pow_of_hadamardCode_eq {ι : Type u_1} [Fintype ι] (A B : Finset (ι → Bool)) (b : Bool) (h : ∀ x ∈ A, ∀ y ∈ B, hadamardCode x y = b) : A.card * B.card ≤ 2 ^ Fintype.card ι

A rectangle on which the inner product modulo two is constant has at most 2 ^ Fintype.card ι entries. Neither side is required to be nonempty.