Rectangles, rectangle-free sets and bias

An input is a function x : ι → U from a type of coordinates to an alphabet. A set of coordinates X cuts an input into two parts: its restriction to X and its restriction to the complement Xᶜ. The rectangle with sides A and B is the set of inputs whose part on X lies in A and whose part on Xᶜ lies in B: a combinatorial rectangle in the sense of communication complexity, for the cut of the coordinates into X and Xᶜ.

A set of inputs S is K-rectangle-free when every rectangle inside S, for every cut of the coordinates, has a side with fewer than K elements. This is the property of a hard set that the worst-case frontier lower bounds use.

Thick or small (exists_thick_or_ncard_lt). A set that ignores coordinates carrying at least K assignments is a rectangle with both sides of size at least K, or it has fewer than |U| K ^ 2 elements. Two consequences:

• the support lemma (RectangleFree.pow_ncard_compl_lt): a large rectangle-free set depends on all but fewer than log_|U| K coordinates;
• bias on sets that ignore many coordinates (RectangleBias.abs_signedCount_le_of_dependsOn).

The average-case lower bounds use a quantitative form of rectangle-freeness: S has bias at most b on large rectangles (RectangleBias) when on every rectangle with both sides of size at least K, the density of S is within b of 1/2. Then the inputs of such a rectangle in S and those outside S differ in number by at most a 2 b fraction (signedCount).

Main definitions

• Cslib.Circuits.Frontier.rectangle X A B: the rectangle with sides A on X and B on Xᶜ.
• Cslib.Circuits.Frontier.RectangleFree S K: every rectangle inside S has a side with fewer than K elements.
• Cslib.Circuits.Frontier.signedCount S R: the inputs of R in S minus those outside S.
• Cslib.Circuits.Frontier.RectangleBias S K b: on every rectangle with both sides of size at least K, the density of S is within b of 1/2.

Main results

• Cslib.Circuits.Frontier.ncard_rectangle: a rectangle has |A| |B| inputs.
• Cslib.Circuits.Frontier.signedCount_eq_sum: the signed count as a sum over the counted set.
• Cslib.Circuits.Frontier.exists_thick_or_ncard_lt: thick or small.
• Cslib.Circuits.Frontier.RectangleFree.pow_ncard_compl_lt: the support lemma.
• Cslib.Circuits.Frontier.RectangleBias.abs_signedCount_le_of_dependsOn: bias on a set that ignores many coordinates.
• Cslib.Circuits.Frontier.rectangleBias_one_half: every set has bias at most 1/2.

References

• E. Kushilevitz, N. Nisan, Communication Complexity, Ch. 1

def Cslib.Circuits.Frontier.rectangle {ι : Type u_1} {U : Type u_2} (X : Set ι) (A : Set (↑X → U)) (B : Set (↑Xᶜ → U)) : Set (ι → U)

The rectangle with sides A and B for the cut X: the inputs whose part on X lies in A and whose part on the complement Xᶜ lies in B.

@[simp]

theorem Cslib.Circuits.Frontier.mem_rectangle {ι : Type u_1} {U : Type u_2} {X : Set ι} {A : Set (↑X → U)} {B : Set (↑Xᶜ → U)} {x : ι → U} : x ∈ rectangle X A B ↔ X.domRestrict x ∈ A ∧ Xᶜ.domRestrict x ∈ B

theorem Cslib.Circuits.Frontier.ncard_rectangle {ι : Type u_1} {U : Type u_2} (X : Set ι) (A : Set (↑X → U)) (B : Set (↑Xᶜ → U)) : (rectangle X A B).ncard = A.ncard * B.ncard

A rectangle has as many inputs as pairs of its sides.

theorem Cslib.Circuits.Frontier.domRestrict_prodMk_injective {ι : Type u_1} {U : Type u_2} (X : Set ι) : Function.Injective fun (x : ι → U) => (X.domRestrict x, Xᶜ.domRestrict x)

An input is determined by its two parts: cutting along X is injective.

theorem Cslib.Circuits.Frontier.eq_rectangle_of_dependsOn {ι : Type u_1} {U : Type u_2} {T : Set (ι → U)} {D : Set ι} (hD : DependsOn (fun (x : ι → U) => x ∈ T) Dᶜ) : T = rectangle D Set.univ (Dᶜ.domRestrict '' T)

A set that does not depend on the coordinates in D is the rectangle whose side on D is every assignment and whose side on Dᶜ is the set of its parts there.

theorem Cslib.Circuits.Frontier.exists_thick_or_ncard_lt {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] [Nonempty U] {T : Set (ι → U)} {R : Set ι} (hR : DependsOn (fun (x : ι → U) => x ∈ T) R) {K : ℕ} (hK : 1 ≤ K) (hle : K ≤ Nat.card U ^ Rᶜ.ncard) : (∃ (X : Set ι) (A : Set (↑X → U)) (B : Set (↑Xᶜ → U)), T = rectangle X A B ∧ K ≤ A.ncard ∧ K ≤ B.ncard) ∨ T.ncard < Nat.card U * K ^ 2

Thick or small. Let T depend only on the coordinates in R, and let the other coordinates carry at least K ≥ 1 assignments. Then T is a rectangle with both sides of size at least K, or T has fewer than |U| K ^ 2 elements.

Take a smallest set D of ignored coordinates carrying at least K assignments, so that |U| ^ |D| ≤ |U| (K - 1). Then T is the rectangle whose side on D is everything; if its other side has fewer than K elements, T has at most |U| ^ |D| (K - 1) of them.

Rectangle-free sets

def Cslib.Circuits.Frontier.RectangleFree {ι : Type u_1} {U : Type u_2} (S : Set (ι → U)) (K : ℕ) : Prop

A set of inputs S is K-rectangle-free when every rectangle contained in S, for every cut of the coordinates, has a side with fewer than K elements.

Sides are counted with Set.encard, so that an infinite side is never small. Over finitely many coordinates and a finite alphabet the sides may be counted with Set.ncard instead (rectangleFree_iff).

theorem Cslib.Circuits.Frontier.RectangleFree.ncard_lt_or {ι : Type u_1} {U : Type u_2} {S : Set (ι → U)} {K : ℕ} (hS : RectangleFree S K) (X : Set ι) (A : Set (↑X → U)) (B : Set (↑Xᶜ → U)) (hAB : rectangle X A B ⊆ S) : A.ncard < K ∨ B.ncard < K

Inside a rectangle-free set, one side of every rectangle is a finite set with fewer than K elements.

theorem Cslib.Circuits.Frontier.RectangleFree.pos {ι : Type u_1} {U : Type u_2} {S : Set (ι → U)} {K : ℕ} (h : RectangleFree S K) : 0 < K

The threshold of a rectangle-free set is positive: the empty rectangle has empty sides.

theorem Cslib.Circuits.Frontier.RectangleFree.one_lt {ι : Type u_1} {U : Type u_2} {S : Set (ι → U)} {K : ℕ} (h : RectangleFree S K) (hS : S.Nonempty) : 1 < K

A nonempty K-rectangle-free set has 1 < K: a single input is a rectangle with sides of one element each, for the cut of the coordinates into all and none.

theorem Cslib.Circuits.Frontier.RectangleFree.subset {ι : Type u_1} {U : Type u_2} {S T : Set (ι → U)} {K : ℕ} (h : RectangleFree S K) (hTS : T ⊆ S) : RectangleFree T K

A subset of a rectangle-free set is rectangle-free.

theorem Cslib.Circuits.Frontier.RectangleFree.mono {ι : Type u_1} {U : Type u_2} {S : Set (ι → U)} {K K' : ℕ} (h : RectangleFree S K) (hK : K ≤ K') : RectangleFree S K'

Raising the threshold keeps a set rectangle-free.

theorem Cslib.Circuits.Frontier.RectangleFree.pow_ncard_compl_lt {ι : Type u_1} {U : Type u_2} {S : Set (ι → U)} {K : ℕ} [Finite ι] [Finite U] [Nonempty U] (hS : RectangleFree S K) {R : Set ι} (hR : DependsOn (fun (x : ι → U) => x ∈ S) R) (hbig : Nat.card U * K ^ 2 ≤ S.ncard) : Nat.card U ^ Rᶜ.ncard < K

The support lemma. A K-rectangle-free set with at least |U| * K ^ 2 elements depends on all but fewer than log_|U| K coordinates: if S depends only on the coordinates in R, then |U| ^ |Rᶜ| < K.

theorem Cslib.Circuits.Frontier.rectangleFree_iff {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] {S : Set (ι → U)} {K : ℕ} : RectangleFree S K ↔ ∀ (X : Set ι) (A : Set (↑X → U)) (B : Set (↑Xᶜ → U)), rectangle X A B ⊆ S → A.ncard < K ∨ B.ncard < K

Over finitely many coordinates and a finite alphabet, a set is K-rectangle-free exactly when every rectangle inside it has a side with fewer than K elements counted with ncard.

Bias

noncomputable def Cslib.Circuits.Frontier.signedCount {ι : Type u_1} {U : Type u_2} (S R : Set (ι → U)) : ℝ

The signed count of S on R: the number of inputs of R in S minus the number of inputs of R outside S.

theorem Cslib.Circuits.Frontier.signedCount_eq_sum {ι : Type u_1} {U : Type u_2} [Fintype ι] [Fintype U] [DecidableEq ι] (S R : Set (ι → U)) [DecidablePred fun (x : ι → U) => x ∈ S] [DecidablePred fun (x : ι → U) => x ∈ R] : signedCount S R = ∑ x : ι → U with x ∈ R, if x ∈ S then 1 else -1

The signed count of S on R is the sum of ±1 over R: +1 on the inputs in S and -1 on the others.

theorem Cslib.Circuits.Frontier.abs_signedCount_le {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] (S R : Set (ι → U)) : |signedCount S R| ≤ ↑R.ncard

A signed count is at most the size of the set counted.

theorem Cslib.Circuits.Frontier.signedCount_eq_add_sdiff {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] (S : Set (ι → U)) {R D : Set (ι → U)} (h : R ⊆ D) : signedCount S D = signedCount S R + signedCount S (D \ R)

Signed counts add over a set R and its complement in a larger set D.

theorem Cslib.Circuits.Frontier.signedCount_eq_two_mul {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] (S R : Set (ι → U)) : signedCount S R = 2 * (↑(R ∩ S).ncard - ↑R.ncard / 2)

The signed count is twice the deviation of |R ∩ S| from |R| / 2.

def Cslib.Circuits.Frontier.RectangleBias {ι : Type u_1} {U : Type u_2} (S : Set (ι → U)) (K : ℕ) (b : ℝ) : Prop

A set of inputs S has bias at most b on rectangles with both sides of size at least K when on every such rectangle R, for every cut of the coordinates, the density of S is within b of 1/2:

| |R ∩ S| - |R| / 2 | ≤ b |R|.

Sizes are counted with Set.ncard, so the notion is meant for finitely many coordinates and a finite alphabet.

theorem Cslib.Circuits.Frontier.rectangleBias_one_half {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] (S : Set (ι → U)) (K : ℕ) : RectangleBias S K (1 / 2)

Every set has bias at most 1/2: the size of R ∩ S lies between 0 and |R|.

theorem Cslib.Circuits.Frontier.RectangleBias.mono {ι : Type u_1} {U : Type u_2} {S : Set (ι → U)} {K K' : ℕ} {b : ℝ} (h : RectangleBias S K b) (hK : K ≤ K') : RectangleBias S K' b

A bias bound for rectangles with sides of size at least K holds for larger sides.

theorem Cslib.Circuits.Frontier.RectangleBias.abs_signedCount_rectangle_le {ι : Type u_1} {U : Type u_2} {S : Set (ι → U)} {K : ℕ} {b : ℝ} [Finite ι] [Finite U] (hS : RectangleBias S K b) {X : Set ι} {A : Set (↑X → U)} {B : Set (↑Xᶜ → U)} (hA : K ≤ A.ncard) (hB : K ≤ B.ncard) : |signedCount S (rectangle X A B)| ≤ 2 * b * ↑(rectangle X A B).ncard

On a rectangle with both sides of size at least K, a set with bias at most b has signed count at most 2 b times the size of the rectangle.

theorem Cslib.Circuits.Frontier.RectangleBias.nonneg {ι : Type u_1} {U : Type u_2} {S : Set (ι → U)} {K : ℕ} {b : ℝ} [Finite ι] [Finite U] [Nonempty U] (hS : RectangleBias S K b) (hK : K ≤ Nat.card U ^ (Nat.card ι / 2)) : 0 ≤ b

A bias bound is nonnegative once half of the coordinates carry at least K assignments: the whole input space is then a rectangle with both sides of size at least K.

theorem Cslib.Circuits.Frontier.RectangleBias.abs_signedCount_le_of_dependsOn {ι : Type u_1} {U : Type u_2} {S : Set (ι → U)} {K : ℕ} {b : ℝ} [Finite ι] [Finite U] [Nonempty U] (hS : RectangleBias S K b) (hb : 0 ≤ b) {T : Set (ι → U)} {R : Set ι} (hR : DependsOn (fun (x : ι → U) => x ∈ T) R) (hK : 1 ≤ K) (hle : K ≤ Nat.card U ^ Rᶜ.ncard) : |signedCount S T| ≤ 2 * b * ↑T.ncard + ↑(Nat.card U * K ^ 2)

Bias on a set that ignores many coordinates. If T depends only on the coordinates in R and the others carry at least K ≥ 1 assignments, then either T is a rectangle with both sides of size at least K, on which S has bias at most b, or T is small. Either way the signed count of S on T is at most 2 b |T| + |U| K ^ 2.