Documentation

Complexity.Computability.Communication.Lifting.Density

Dense pointer sets and the full-range lemma #

A set X of Alice's pointer vectors x : Fin n → Fin m is τ-dense on a set F of coordinates (Communication.Lifting.IsDense) when no assignment to a nonempty set I ⊆ F of coordinates is shared by more than a τ ^ (-#I) fraction of X. This is blockwise min-entropy log₂ τ Göös, Pitassi and Watson 2017, Mertz and Pitassi, Definition 2.2.

Full range. Let X be r-dense on F, let Y be a set of Bob's inputs with at most D bits of deficiency on the blocks in F, and let 16 #F (D + 1) ≤ r. If both sets are fixed outside F, then some pair (x, y) ∈ X × Y gives the index gadget the value β x on F, for any target values β x (Communication.Lifting.exists_forall_eq_of_isDense) Mertz and Pitassi, Lemma 3.2. The pointer vectors of X, read as sets of pointers into the blocks, form an r-spread family. So few sets of Bob's ones avoid every target pattern (Cslib.card_filter_avoidsPatterns_mul_two_pow_le_of_spread), and Y is too large to avoid them all. Mertz and Pitassi use the blockwise approximate sunflower lemma for this step and need only r ≥ C #F log (#F / ε). The greedy Janson bound used here needs the larger spread r ≥ 16 #F (D + 1), which still allows gadget size polynomial in n.

Main definitions #

Main results #

References #

source
def Cslib.Communication.Lifting.IsDense {n m : ℕ} (τ : ℝ) (F : Finset (Fin n)) (X : Finset (Fin n → Fin m)) :
Prop

X is τ-dense on the coordinates F: for every nonempty I ⊆ F and every assignment α, at most a τ ^ (-#I) fraction of X agrees with α on I.

Instances For
    source
    theorem Cslib.Communication.Lifting.IsDense.of_subset {n m : ℕ} {τ c : ℝ} {F : Finset (Fin n)} {X X' : Finset (Fin n → Fin m)} (hX : IsDense τ F X) (hτ : 0 ≤ τ) (hc : 1 ≤ c) (hsub : X' ⊆ X) (hcard : ↑X.card ≤ c * ↑X'.card) :
    IsDense (τ / c) F X'

    A subset holding at least a 1 / c fraction of a τ-dense set is τ / c-dense.

    source
    theorem Cslib.Communication.Lifting.IsDense.mono {n m : ℕ} {τ : ℝ} {F F' : Finset (Fin n)} {X : Finset (Fin n → Fin m)} (hX : IsDense τ F X) (hF : F' ⊆ F) :
    IsDense τ F' X

    A set dense on F is dense on every subset of F.

    source
    theorem Cslib.Communication.Lifting.exists_forall_eq_of_isDense {n m : ℕ} {F : Finset (Fin n)} {X : Finset (Fin n → Fin m)} {Y : Finset (Fin n → Fin m → Bool)} {r : ℝ} {D : ℕ} (hr : 0 < r) (hX : X.Nonempty) (hXfix : ∀ x ∈ X, ∀ x' ∈ X, ∀ i ∉ F, x i = x' i) (hdense : IsDense r F X) (hYfix : ∀ y ∈ Y, ∀ y' ∈ Y, ∀ i ∉ F, y i = y' i) (hY : 2 ^ (F.card * m) ≤ 2 ^ D * ↑Y.card) (hrD : 16 * ↑F.card * (↑D + 1) ≤ r) (β : (Fin n → Fin m) → Fin n → Bool) :
    ∃ x ∈ X, ∃ y ∈ Y, ∀ i ∈ F, y i (x i) = β x i

    The full-range lemma. Let X be r-dense on F and let Y have at most D bits of deficiency on the blocks of F, with 16 #F (D + 1) ≤ r, both fixed outside F. Then for any target values β x, some x ∈ X and y ∈ Y give the index gadget the value β x on F Mertz and Pitassi, Lemma 3.2.