Rectangles and rectangle-free sets

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^c. The rectangle with sides A and B is the set of inputs whose part on X lies in A and whose part on X^c lies in B.

A set of inputs S is K-rectangle-free when every rectangle inside S, for every way of cutting the coordinates, has a side with fewer than K elements. This is the only property of the hard function that the lower bound uses.

The support lemma RectangleFree.pow_ncard_compl_lt is the only other fact we need about such sets: a large rectangle-free set depends on all but fewer than log_|U| K coordinates. Indeed, if S ignored a set D of log_|U| K coordinates, then S would contain the rectangle whose side on D is everything, so its other side, and hence S, would be small.

Main definitions

• Frontier.rectangle X A B: the rectangle with sides A on X and B on X^c.
• Frontier.RectangleFree S K: every rectangle inside S has a side with fewer than K elements.

Main results

• Frontier.RectangleFree.ncard_le_of_dependsOn: a rectangle-free set that ignores the coordinates in D, with K ≤ |U| ^ |D|, has at most |U| ^ |D| * (K - 1) elements.
• Frontier.RectangleFree.pow_ncard_compl_lt: the support lemma.

def Complexity.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^c lies in B.

Equations

• Complexity.Frontier.rectangle X A B = {x : ι → U | X.domRestrict x ∈ A ∧ Xᶜ.domRestrict x ∈ B}

theorem Complexity.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

def Complexity.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.

Equations

• Complexity.Frontier.RectangleFree S K = ∀ (X : Set ι) (A : Set (↑X → U)) (B : Set (↑Xᶜ → U)), Complexity.Frontier.rectangle X A B ⊆ S → A.ncard < K ∨ B.ncard < K

theorem Complexity.Frontier.eq_of_domRestrict_eq {ι : Type u_1} {U : Type u_2} {X : Set ι} {x y : ι → U} (h₁ : X.domRestrict x = X.domRestrict y) (h₂ : Xᶜ.domRestrict x = Xᶜ.domRestrict y) : x = y

An input is determined by its two parts.

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

Splitting an input into its two parts is injective.

theorem Complexity.Frontier.RectangleFree.ncard_le_of_dependsOn {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] {S : Set (ι → U)} {K : ℕ} (hS : RectangleFree S K) {D : Set ι} (hD : DependsOn (fun (x : ι → U) => x ∈ S) Dᶜ) (hK : K ≤ Nat.card U ^ D.ncard) : S.ncard ≤ Nat.card U ^ D.ncard * (K - 1)

A rectangle-free set that does not depend on the coordinates in D is small: if D alone carries at least K assignments, then S has at most |U| ^ |D| * (K - 1) elements.

The rectangle whose side on D is every assignment and whose side on D^c is the set of D^c-parts of S lies inside S. Its first side is large, so its second side is small.

theorem Complexity.Frontier.RectangleFree.pow_ncard_compl_lt {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] [Nonempty U] {S : Set (ι → U)} {K : ℕ} (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 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^c| < K.