Expansion of the axis-parallel line closure

The line closure of a set S of points of X ^ n is the union of the axis-parallel lines through the points of S: the points y such that changing one coordinate of y lands in S (Cslib.lineClosure). This is the closure S̄ = ⋃ᵢ πᵢ⁻¹(πᵢ(S)) of Babai, Fortnow, Lund, Definition 5.7, where πᵢ forgets the i-th coordinate. The closure of a set of at most half of the points is larger than the set by a factor 1 + 1 / (2 n) (Cslib.card_le_two_mul_card_lineClosure_sdiff, Cslib.card_lineClosure_ge), the Expansion Lemma Babai, Fortnow, Lund, Lemma 5.8, which they attribute to Aldous.

Our proof is a canonical-path argument, not Aldous's. For x ∈ S and z ∉ S, the path from x to z that replaces the coordinates of x by those of z in increasing order leaves S along some edge (u, update u c (z c)) with u ∈ S. Swapping the first c coordinates of x and z is a bijection of pairs that sends this event to the event that changing the c-th coordinate of a point u ∈ S to that of an arbitrary point leaves S. Counting, |S| |Sᶜ| ≤ n |X| ^ n |S̄ \ S|, and |Sᶜ| ≥ |X| ^ n / 2 gives |S| ≤ 2 n |S̄ \ S|.

Main definitions

• Cslib.lineClosure: the union of the axis-parallel lines through the points of a set.

Main results

• Cslib.card_mul_card_compl_le: |S| |Sᶜ| ≤ n |X| ^ n |S̄ \ S|.
• Cslib.card_le_two_mul_card_lineClosure_sdiff, Cslib.card_lineClosure_ge: the Expansion Lemma.

References

• L. Babai, L. Fortnow, C. Lund, Non-deterministic exponential time has two-prover interactive protocols, Section 5.2

def Cslib.lineClosure {X : Type u_1} [Fintype X] [DecidableEq X] {n : ℕ} (S : Finset (Fin n → X)) : Finset (Fin n → X)

The line closure of a set S of points of X ^ n: the points y that agree with some point of S in all coordinates but one, that is, the union of the axis-parallel lines through the points of S Babai, Fortnow, Lund, Definition 5.7.

theorem Cslib.mem_lineClosure {X : Type u_1} [Fintype X] [DecidableEq X] {n : ℕ} {S : Finset (Fin n → X)} {y : Fin n → X} : y ∈ lineClosure S ↔ ∃ (i : Fin n) (t : X), Function.update y i t ∈ S

Membership in the line closure.

theorem Cslib.subset_lineClosure {X : Type u_1} [Fintype X] [DecidableEq X] {n : ℕ} {S : Finset (Fin n → X)} (hn : 0 < n) : S ⊆ lineClosure S

In positive dimension, a set lies in its line closure.

theorem Cslib.card_mul_card_compl_le {X : Type u_1} [Fintype X] [DecidableEq X] {n : ℕ} (S : Finset (Fin n → X)) : S.card * Sᶜ.card ≤ n * Fintype.card X ^ n * (lineClosure S \ S).card

Edge counting for the line closure: |S| |Sᶜ| ≤ n |X| ^ n |S̄ \ S|.

theorem Cslib.card_le_two_mul_card_lineClosure_sdiff {X : Type u_1} [Fintype X] [DecidableEq X] {n : ℕ} {S : Finset (Fin n → X)} (hS : 2 * S.card ≤ Fintype.card X ^ n) : S.card ≤ 2 * n * (lineClosure S \ S).card

The Expansion Lemma: if S has at most half of the points of X ^ n, then |S| ≤ 2 n |S̄ \ S| Babai, Fortnow, Lund, Lemma 5.8.

theorem Cslib.card_lineClosure_ge {X : Type u_1} [Fintype X] [DecidableEq X] {n : ℕ} {S : Finset (Fin n → X)} (hn : 0 < n) (hS : 2 * S.card ≤ Fintype.card X ^ n) : (2 * n + 1) * S.card ≤ 2 * n * (lineClosure S).card

The Expansion Lemma in the form of Babai, Fortnow, Lund, Lemma 5.8: in positive dimension, if |S| ≤ |X| ^ n / 2 then |S̄| ≥ |S| (1 + 1 / (2 n)).