The density-restoring partition

This file proves the two partition lemmas behind the simulation in the proof of the lifting theorem Mertz and Pitassi, §3.1 Göös, Pitassi and Watson 2017, §3.

Phase I (Communication.Lifting.exists_pieces). A set X of pointer vectors splits into disjoint pieces covering at least half of it. Each piece P is fixed to some α on a set I of coordinates and is τ-dense on the rest of F. The coordinates I are a maximal set on which the remaining vectors are too concentrated, so P holds at least a τ ^ (-#I) / 2 fraction of X Mertz and Pitassi, Algorithm 1, Claims 3.4 and 3.5.

Choosing a piece (Communication.Lifting.exists_piece_forall_le_card_filter). Suppose X is half of a dense set and Bob's set Y is large. Then some piece (I, α, P) leaves every value β of the gadget on I possible for at least a (4 τ) ^ (-#I) fraction of Y Mertz and Pitassi, Lemma 3.6. Otherwise each piece has a value β that few y allow. Summing over the pieces, at least half of Y allows none of these values, and the full-range lemma gives a contradiction. We sum the bounds using the sizes of the pieces rather than counting the possible pairs (I, α), so the threshold is (4 τ) ^ (-#I) instead of m ^ (-2 #I).

Phase II (Communication.Lifting.exists_fix_blocks). Bob's inputs allowing the value β can be fixed on the blocks of I at the cost of a factor 2 ^ (m #I).

Main definitions

• Cslib.Communication.Lifting.Piece: a piece of a density-restoring partition.

Main results

• Cslib.Communication.Lifting.exists_pieces: the density-restoring partition.
• Cslib.Communication.Lifting.exists_piece_forall_le_card_filter: choosing a piece.
• Cslib.Communication.Lifting.exists_fix_blocks: fixing Bob's blocks.

References

• I. Mertz and T. Pitassi, Lifting: As Easy As 1, 2, 3
• M. Göös, T. Pitassi and T. Watson, Query-to-communication lifting for BPP

structure Cslib.Communication.Lifting.Piece (n m : ℕ) : Type

A piece of a density-restoring partition: the pointer vectors P, all fixed to α on the coordinates I.

• I : Finset (Fin n)

  The fixed coordinates.

• α : Fin n → Fin m

  The fixed values.

• P : Finset (Fin n → Fin m)

  The pointer vectors.

structure Cslib.Communication.Lifting.IsPartition {n m : ℕ} (τ : ℝ) (F : Finset (Fin n)) (X : Finset (Fin n → Fin m)) (L : List (Piece n m)) : Prop

The pieces of a density-restoring partition of X with density τ on F.

• subset (q : Piece n m) : q ∈ L → q.P ⊆ X
• pairwise : List.Pairwise (fun (q q' : Piece n m) => Disjoint q.P q'.P) L
• I_subset (q : Piece n m) : q ∈ L → q.I ⊆ F
• fixed (q : Piece n m) : q ∈ L → ∀ x ∈ q.P, ∀ i ∈ q.I, x i = q.α i
• dense (q : Piece n m) : q ∈ L → IsDense τ (F \ q.I) q.P
• card_le (q : Piece n m) : q ∈ L → ↑X.card ≤ 2 * ↑q.P.card * τ ^ q.I.card
• cover : ↑X.card ≤ 2 * (List.map (fun (q : Piece n m) => ↑q.P.card) L).sum

@[reducible, inline]

abbrev Cslib.Communication.Lifting.agreeOn {n m : ℕ} (W : Finset (Fin n → Fin m)) (I : Finset (Fin n)) (α : Fin n → Fin m) : Finset (Fin n → Fin m)

The vectors of W that agree with α on I.

def Cslib.Communication.Lifting.Violates {n m : ℕ} (τ : ℝ) (W : Finset (Fin n → Fin m)) (I : Finset (Fin n)) (α : Fin n → Fin m) : Prop

The vectors of W are too concentrated on I: more than a τ ^ (-#I) fraction agrees with α there.

theorem Cslib.Communication.Lifting.isDense_agreeOn {n m : ℕ} {τ : ℝ} {F : Finset (Fin n)} (hτ : 0 < τ) {W : Finset (Fin n → Fin m)} {I : Finset (Fin n)} {α : Fin n → Fin m} (hW : ↑W.card ≤ ↑(agreeOn W I α).card * τ ^ I.card) (hmax : ∀ I' ⊆ F, ∀ (α' : Fin n → Fin m), Violates τ W I' α' → I'.card ≤ I.card) (hIF : I ⊆ F) (hstrict : I.Nonempty → Violates τ W I α) : IsDense τ (F \ I) (agreeOn W I α)

Claim 3.4 of Mertz and Pitassi. Fixing a set W on a maximal concentrated set I of coordinates leaves it dense on the other coordinates.

theorem Cslib.Communication.Lifting.exists_pieces {n m : ℕ} {τ : ℝ} (hτ : 0 < τ) (F : Finset (Fin n)) (X : Finset (Fin n → Fin m)) : ∃ (L : List (Piece n m)), IsPartition τ F X L

Phase I: the density-restoring partition Mertz and Pitassi, Algorithm 1, Claims 3.4 and 3.5. Every set of pointer vectors has a density-restoring partition.

theorem Cslib.Communication.Lifting.sum_card_le_of_pairwise {n m : ℕ} {S : Finset (Fin n → Fin m)} {L : List (Piece n m)} : (∀ q ∈ L, q.P ⊆ S) → List.Pairwise (fun (q q' : Piece n m) => Disjoint q.P q'.P) L → (List.map (fun (q : Piece n m) => ↑q.P.card) L).sum ≤ ↑S.card

Pairwise disjoint pieces inside S have at most #S vectors in total.

def Cslib.Communication.Lifting.unionOf {β : Type u_1} [DecidableEq β] (L : List (Finset β)) : Finset β

The union of a list of finite sets.

theorem Cslib.Communication.Lifting.mem_unionOf {β : Type u_1} [DecidableEq β] {L : List (Finset β)} {y : β} : y ∈ unionOf L ↔ ∃ s ∈ L, y ∈ s

theorem Cslib.Communication.Lifting.card_unionOf_le {β : Type u_1} [DecidableEq β] (L : List (Finset β)) : ↑(unionOf L).card ≤ (List.map (fun (s : Finset β) => ↑s.card) L).sum

A union of finite sets has at most the sum of their sizes.

@[reducible, inline]

abbrev Cslib.Communication.Lifting.allowing {n m : ℕ} (Y : Finset (Fin n → Fin m → Bool)) (I : Finset (Fin n)) (α : Fin n → Fin m) (β : Fin n → Bool) : Finset (Fin n → Fin m → Bool)

The inputs of Y on which the gadget takes the value β on I at the pointers α.

theorem Cslib.Communication.Lifting.exists_piece_forall_le_card_filter {n m : ℕ} {τ : ℝ} {F : Finset (Fin n)} {X X₀ : Finset (Fin n → Fin m)} {Y : Finset (Fin n → Fin m → Bool)} {L : List (Piece n m)} {D : ℕ} (hτ : 0 < τ) (hL : IsPartition τ F X L) (hX : X.Nonempty) (hX₀ : IsDense τ F X₀) (hXX₀ : X ⊆ X₀) (hcard : ↑X₀.card ≤ 2 * ↑X.card) (hXfix : ∀ x ∈ X, ∀ x' ∈ X, ∀ i ∉ F, x i = x' i) (hYfix : ∀ y ∈ Y, ∀ y' ∈ Y, ∀ i ∉ F, y i = y' i) (hY : 2 ^ (F.card * m) ≤ 2 ^ D * ↑Y.card) (hτD : 64 * ↑F.card * (↑D + 2) ≤ τ) : ∃ q ∈ L, ∀ (β : Fin n → Bool), ↑Y.card ≤ ↑(allowing Y q.I q.α β).card * (4 * τ) ^ q.I.card

Choosing a piece Mertz and Pitassi, Lemma 3.6. Let X hold at least half of a τ-dense set and let Y have at most D bits of deficiency on the blocks of F, with 64 #F (D + 2) ≤ τ, both fixed outside F. Then some piece (I, α, P) of a density-restoring partition of X leaves every value β of the gadget on I possible for at least a (4 τ) ^ (-#I) fraction of Y.

theorem Cslib.Communication.Lifting.exists_fix_blocks {n m : ℕ} (Y : Finset (Fin n → Fin m → Bool)) (I : Finset (Fin n)) (α : Fin n → Fin m) (β : Fin n → Bool) : ∃ (η : Fin n → Fin m → Bool), (∀ i ∈ I, η i (α i) = β i) ∧ ↑(allowing Y I α β).card ≤ ↑{y ∈ Y | ∀ i ∈ I, y i = η i}.card * 2 ^ (m * I.card)

Phase II: fixing Bob's blocks. The inputs of Y allowing the value β on I can be fixed on the blocks of I, keeping at least a 2 ^ (-m #I) fraction of them.