The discrepancy bound and the inner product

The discrepancy of f : X → Y → Bool under a distribution ν on X × Y is the largest imbalance |ν(S ∩ f⁻¹ false) - ν(S ∩ f⁻¹ true)| over rectangles S = A × B (discrepancy) Kushilevitz and Nisan, Chapter 3. The output of a protocol is constant on each leaf rectangle, so its correlation with f under ν, which is 1 - 2 ε for a protocol erring with probability ε on inputs drawn from ν, is at most the number of leaves times the discrepancy (Protocol.abs_sum_mul_signVal_le, splitting the sum by Protocol.sum_eq_sum_leaves). Hence a protocol sending c bits with error 1 / 2 - γ under ν has 2 γ ≤ 2 ^ c disc_ν(f) (Protocol.two_mul_le_two_pow_mul_discrepancy), and by averaging the same holds for public-coin protocols with error 1 / 2 - γ on every input (PublicCoin.two_mul_le_two_pow_mul_discrepancy).

For the inner product, Lindsey's lemma (Matrix.sq_sum_bilinear_mul_two_pow_rank_le) bounds the signed sum of the inner product modulo two over a rectangle A × B of n-bit strings by √(|A| |B| 2 ^ n) (BitString.sq_sum_signVal_dotProduct_le), so under the uniform distribution the inner product has discrepancy at most 2 ^ (-n / 2) (discrepancy_dotProduct_sq_mul_two_pow_le). So public-coin protocols for the inner product with error 1 / 2 - γ send c bits with (2 γ)² 2 ^ n ≤ 4 ^ c (PublicCoin.Solves.sq_mul_two_pow_le_four_pow_of_dotProduct), and with error 1 / 3 at least (n - 3) / 2 bits: R(IP) = Ω(n) (PublicCoin.le_two_mul_ecomplexityFun_dotProduct_add_three) Chor and Goldreich.

Main definitions

• Cslib.Communication.discrepancy: the discrepancy of a Boolean function under a distribution.

Main results

• Cslib.Communication.Protocol.two_mul_le_two_pow_mul_discrepancy, Cslib.Communication.PublicCoin.two_mul_le_two_pow_mul_discrepancy: the discrepancy bound.
• Cslib.Communication.discrepancy_dotProduct_sq_mul_two_pow_le: the discrepancy of the inner product.
• Cslib.Communication.PublicCoin.le_two_mul_ecomplexityFun_dotProduct_add_three, Cslib.Communication.PrivateCoin.le_two_mul_ecomplexityFun_dotProduct_add_three: randomized protocols for the inner product of n bits send Ω(n) bits.

References

• E. Kushilevitz and N. Nisan, Communication Complexity
• B. Chor and O. Goldreich, Unbiased bits from sources of weak randomness and probabilistic communication complexity
• S. Jukna, Extremal Combinatorics, Ch. 14

Discrepancy

noncomputable def Cslib.Communication.discrepancy {X : Type u_1} {Y : Type u_2} (ν : PMF (X × Y)) (f : X → Y → Bool) : ℝ

The discrepancy of f : X → Y → Bool under a distribution ν on X × Y: the largest imbalance |ν(S ∩ f⁻¹ false) - ν(S ∩ f⁻¹ true)| of f on a rectangle S = A × B, written as the signed sum |∑_{x ∈ A, y ∈ B} ν(x, y) (-1)^{f x y}|. The results about it assume that X and Y are finite.

theorem Cslib.Communication.abs_sum_le_discrepancy {X : Type u_1} {Y : Type u_2} [Finite X] [Finite Y] (ν : PMF (X × Y)) (f : X → Y → Bool) (A : Finset X) (B : Finset Y) : |∑ x ∈ A, ∑ y ∈ B, (ν (x, y)).toReal * BitString.signVal (f x y)| ≤ discrepancy ν f

theorem Cslib.Communication.exists_abs_sum_eq_discrepancy {X : Type u_1} {Y : Type u_2} [Finite X] [Finite Y] (ν : PMF (X × Y)) (f : X → Y → Bool) : ∃ (A : Finset X) (B : Finset Y), |∑ x ∈ A, ∑ y ∈ B, (ν (x, y)).toReal * BitString.signVal (f x y)| = discrepancy ν f

The discrepancy is attained on some rectangle.

theorem Cslib.Communication.discrepancy_nonneg {X : Type u_1} {Y : Type u_2} {ν : PMF (X × Y)} {f : X → Y → Bool} [Finite X] [Finite Y] : 0 ≤ discrepancy ν f

The discrepancy bound

theorem Cslib.Communication.Protocol.abs_sum_mul_signVal_le {X : Type u_1} {Y : Type u_2} [Fintype X] [Fintype Y] (p : Protocol X Y Bool) (ν : PMF (X × Y)) (f : X → Y → Bool) : |∑ x : X, ∑ y : Y, (ν (x, y)).toReal * BitString.signVal (f x y) * BitString.signVal (p.run x y)| ≤ ↑p.leaves * discrepancy ν f

Correlation with a protocol is bounded by discrepancy: the correlation under ν of f with the output of a protocol is at most the number of its leaves times the discrepancy of f under ν.

theorem Cslib.Communication.Protocol.two_mul_le_two_pow_mul_discrepancy {X : Type u_1} {Y : Type u_2} {ν : PMF (X × Y)} {f : X → Y → Bool} [Finite X] [Finite Y] (p : Protocol X Y Bool) {γ : ℝ} (hp : (p.distributionalError ν fun (x : X) (y : Y) (b : Bool) => f x y = b) ≤ 1 / 2 - γ) : 2 * γ ≤ 2 ^ p.depth * discrepancy ν f

The discrepancy bound for deterministic protocols: a protocol erring with probability at most 1 / 2 - γ on inputs drawn from ν has 2 γ ≤ 2 ^ depth · disc_ν(f).

theorem Cslib.Communication.PublicCoin.Solves.two_mul_le_two_pow_mul_discrepancy {X : Type u_1} {Y : Type u_2} {f : X → Y → Bool} [Finite X] [Finite Y] {μ : PublicCoin X Y Bool} {γ : ℝ} {c : ℕ} (hμ : μ.Solves (1 / 2 - γ) (fun (x : X) (y : Y) (b : Bool) => f x y = b) Set.univ Set.univ) (hc : μ.depth ≤ ↑c) (ν : PMF (X × Y)) : 2 * γ ≤ 2 ^ c * discrepancy ν f

The discrepancy bound for public-coin protocols: a public-coin protocol sending at most c bits and computing f with error at most 1 / 2 - γ on every input has 2 γ ≤ 2 ^ c · disc_ν(f) for every distribution ν.

theorem Cslib.Communication.PublicCoin.two_mul_le_two_pow_mul_discrepancy {X : Type u_1} {Y : Type u_2} {f : X → Y → Bool} [Finite X] [Finite Y] {γ : ℝ} {c : ℕ} (h : ecomplexityFun (1 / 2 - γ) f ≤ ↑c) (ν : PMF (X × Y)) : 2 * γ ≤ 2 ^ c * discrepancy ν f

The discrepancy bound: if f has public-coin communication complexity at most c with error 1 / 2 - γ, then 2 γ ≤ 2 ^ c · disc_ν(f) for every distribution ν.

The inner product

theorem Cslib.Communication.discrepancy_dotProduct_sq_mul_two_pow_le (n : ℕ) : (discrepancy (Probability.PMF.uniformOfFintype (BitString n × BitString n)) fun (x y : BitString n) => x ⬝ᵥ y) ^ 2 * 2 ^ n ≤ 1

The inner product has discrepancy at most 2 ^ (-n / 2) under the uniform distribution on pairs of n-bit strings, in the form disc² · 2 ^ n ≤ 1.

theorem Cslib.Communication.PublicCoin.Solves.sq_mul_two_pow_le_four_pow_of_dotProduct {n c : ℕ} {γ : ℝ} {μ : PublicCoin (BitString n) (BitString n) Bool} (hμ : μ.Solves (1 / 2 - γ) (fun (x y : BitString n) (b : Bool) => x ⬝ᵥ y = b) Set.univ Set.univ) (hc : μ.depth ≤ ↑c) (hγ : 0 ≤ γ) : (2 * γ) ^ 2 * 2 ^ n ≤ 4 ^ c

Randomized protocols for the inner product: a public-coin protocol computing the inner product modulo two of two n-bit strings with error at most 1 / 2 - γ, for γ ≥ 0, and sending at most c bits has (2 γ)² 2 ^ n ≤ 4 ^ c.

theorem Cslib.Communication.PublicCoin.le_two_mul_ecomplexityFun_dotProduct_add_three (n : ℕ) : ↑n ≤ (2 * ecomplexityFun (1 / 3) fun (x y : BitString n) => x ⬝ᵥ y) + 3

The inner product needs Ω(n) bits with public coins: computing the inner product modulo two of two n-bit strings with error 1 / 3 needs at least (n - 3) / 2 bits.

theorem Cslib.Communication.PrivateCoin.le_two_mul_ecomplexityFun_dotProduct_add_three (n : ℕ) : ↑n ≤ (2 * ecomplexityFun (1 / 3) fun (x y : BitString n) => x ⬝ᵥ y) + 3

The inner product needs Ω(n) bits with private coins: computing the inner product modulo two of two n-bit strings with error 1 / 3 needs at least (n - 3) / 2 bits.