Monochromatic rectangles for the inner product

Lindsey's lemma bounds the signed sum of the inner product modulo two x ⬝ᵥ y 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 x ⬝ᵥ y 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.

With real weights in place of sets, the sign matrix (-1)^{x ⬝ᵥ y} multiplies squared norms by exactly 2 ^ |ι| (BitString.sum_sq_sum_mul_signVal_dotProduct), so weighted bilinear sums obey (∑ₓ ∑ᵧ a(x) b(y) (-1)^{x ⬝ᵥ y})² ≤ 2 ^ |ι| ‖a‖² ‖b‖² (BitString.sq_sum_mul_signVal_dotProduct_le), by Cauchy–Schwarz and character orthogonality. For probability weights this is the bias bound behind the Chor–Goldreich two-source extractor Chor and Goldreich.

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_dotProduct_eq: the monochromatic inner-product rectangle bound.
• Cslib.BitString.sum_sq_sum_mul_signVal_dotProduct: Parseval's identity for the Hadamard transform.
• Cslib.BitString.sq_sum_mul_signVal_dotProduct_le: Lindsey's lemma with real weights.

References

• S. Jukna, Extremal Combinatorics, Ch. 14
• B. Chor and O. Goldreich, Unbiased bits from sources of weak randomness and probabilistic communication complexity
• [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_dotProduct_eq {ι : Type u_1} [Fintype ι] (A B : Finset (ι → Bool)) (b : Bool) (h : ∀ x ∈ A, ∀ y ∈ B, 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.

Weighted sums: the Hadamard transform in ℓ²

theorem Cslib.BitString.sum_sq_sum_mul_signVal_dotProduct {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : (ι → Bool) → ℝ) : ∑ y : ι → Bool, (∑ x : ι → Bool, a x * signVal (x ⬝ᵥ y)) ^ 2 = 2 ^ Fintype.card ι * ∑ x : ι → Bool, a x ^ 2

Parseval's identity for the Hadamard transform. For real weights a on the bit strings indexed by ι, the transform y ↦ ∑ₓ a(x) (-1)^{x ⬝ᵥ y} has squared norm 2 ^ |ι| times that of a: the sign matrix (-1)^{x ⬝ᵥ y} has orthogonal rows of squared length 2 ^ |ι|.

theorem Cslib.BitString.sq_sum_mul_signVal_dotProduct_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a b : (ι → Bool) → ℝ) : (∑ x : ι → Bool, ∑ y : ι → Bool, a x * b y * signVal (x ⬝ᵥ y)) ^ 2 ≤ (2 ^ Fintype.card ι * ∑ x : ι → Bool, a x ^ 2) * ∑ y : ι → Bool, b y ^ 2

Lindsey's lemma with weights. For real weights a and b on the bit strings indexed by ι, (∑ₓ ∑ᵧ a(x) b(y) (-1)^{x ⬝ᵥ y})² ≤ 2 ^ |ι| ‖a‖² ‖b‖². Indicators of A and B recover sq_sum_signVal_dotProduct_le.