Existence of Nisan–Wigderson designs

Nisan and Wigderson build designs from polynomials over a finite field F with q elements [NW94]. The universe is the plane F × F, and each polynomial P of degree less than k contributes its graph {(x, P x) | x ∈ F}, a set of q points. Two distinct such polynomials agree on at most k - 1 points, because their difference is a nonzero polynomial of degree less than k, so two distinct graphs share at most k - 1 points. There are q ^ k polynomials of degree less than k, one for each list of k coefficients. Numbering the points of the plane and the polynomials gives a (q ^ 2, q, k - 1)-design with q ^ k blocks. Since finite fields exist in every prime power order, such a design exists whenever q is a prime power.

Designs can be adjusted: one may keep only some of the blocks, embed the universe in a larger one, weaken the bound on intersections, or replace each block by a subset of a given size, since intersections of subsets are no larger than intersections of the original blocks. Combined with Bertrand's postulate, which yields a prime p with n < p ≤ 2 n, this gives for all n and k a (4 n ^ 2, n, k - 1)-design with (n + 1) ^ k blocks.

Arora and Barak construct designs greedily instead Arora and Barak, Chapter 20; the greedy construction is not formalized here.

Main definitions

• Cslib.Crypto.PRG.NisanWigderson.Design.ofFamily: the design formed by a family of finite sets of equal size and small pairwise intersections, indexed by and living in arbitrary types.
• Cslib.Crypto.PRG.NisanWigderson.Design.subfamily, Cslib.Crypto.PRG.NisanWigderson.Design.map, Cslib.Crypto.PRG.NisanWigderson.Design.weaken, Cslib.Crypto.PRG.NisanWigderson.Design.shrink: fewer blocks, a larger universe, a weaker intersection bound, and smaller blocks; Cslib.Crypto.PRG.NisanWigderson.Design.castLE does all four at once.
• Cslib.Crypto.PRG.NisanWigderson.polynomialBlock: the graph of a polynomial over a finite field, given by its coefficients.
• Cslib.Crypto.PRG.NisanWigderson.Design.polynomial: the Nisan–Wigderson design of the graphs of the polynomials of degree less than k over a finite field.

Main results

• Cslib.Crypto.PRG.NisanWigderson.card_polynomialBlock_inter_le: the graphs of two distinct polynomials of degree less than k share at most k - 1 points.
• Cslib.Crypto.PRG.NisanWigderson.Design.nonempty_of_isPrimePow: for every prime power q and every k, there is a (q ^ 2, q, k - 1)-design with q ^ k blocks.
• Cslib.Crypto.PRG.NisanWigderson.Design.nonempty_four_mul_sq: for all n and k, there is a (4 n ^ 2, n, k - 1)-design with (n + 1) ^ k blocks.

References

• N. Nisan, A. Wigderson, Hardness vs randomness
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 20

Building and adjusting designs

def Cslib.Crypto.PRG.NisanWigderson.Design.ofFamily {ℓ n a m : ℕ} {ι : Type u_1} {U : Type u_2} [DecidableEq U] (B : ι → Finset U) (card_B : ∀ (i : ι), (B i).card = n) (card_B_inter_le : Pairwise fun (i j : ι) => (B i ∩ B j).card ≤ a) (g : Fin m ↪ ι) (e : U ↪ Fin ℓ) : Design ℓ n a m

The design formed by a family B of n-element subsets of a type U, any two distinct members of which share at most a elements: its i-th block is the member B (g i) selected by an injection g : Fin m ↪ ι, carried to Fin ℓ by an injection e : U ↪ Fin ℓ.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.ofFamily_block {ℓ n a m : ℕ} {ι : Type u_1} {U : Type u_2} [DecidableEq U] (B : ι → Finset U) (card_B : ∀ (i : ι), (B i).card = n) (card_B_inter_le : Pairwise fun (i j : ι) => (B i ∩ B j).card ≤ a) (g : Fin m ↪ ι) (e : U ↪ Fin ℓ) (i : Fin m) : (ofFamily B card_B card_B_inter_le g e).block i = Finset.map e (B (g i))

def Cslib.Crypto.PRG.NisanWigderson.Design.subfamily {ℓ n a m m' : ℕ} (D : Design ℓ n a m) (g : Fin m' ↪ Fin m) : Design ℓ n a m'

The design formed by the blocks D.block (g i) of D selected by an injection g : Fin m' ↪ Fin m.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.subfamily_block {ℓ n a m m' : ℕ} (D : Design ℓ n a m) (g : Fin m' ↪ Fin m) (i : Fin m') : (D.subfamily g).block i = D.block (g i)

def Cslib.Crypto.PRG.NisanWigderson.Design.map {ℓ n a m ℓ' : ℕ} (D : Design ℓ n a m) (e : Fin ℓ ↪ Fin ℓ') : Design ℓ' n a m

The design D carried to a larger universe Fin ℓ' by an injection e : Fin ℓ ↪ Fin ℓ'.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.map_block {ℓ n a m ℓ' : ℕ} (D : Design ℓ n a m) (e : Fin ℓ ↪ Fin ℓ') (i : Fin m) : (D.map e).block i = Finset.map e (D.block i)

def Cslib.Crypto.PRG.NisanWigderson.Design.weaken {ℓ n a m a' : ℕ} (D : Design ℓ n a m) (h : a ≤ a') : Design ℓ n a' m

The design D, seen as a design with the weaker intersection bound a' ≥ a.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.weaken_block {ℓ n a m a' : ℕ} (D : Design ℓ n a m) (h : a ≤ a') (a✝ : Fin m) : (D.weaken h).block a✝ = D.block a✝

def Cslib.Crypto.PRG.NisanWigderson.Design.shrink {ℓ n a m n' : ℕ} (D : Design ℓ n a m) (h : n' ≤ n) : Design ℓ n' a m

The design whose blocks consist of the n' smallest elements of the blocks of D, for n' ≤ n. Shrinking blocks does not enlarge their intersections, so the intersection bound a is kept.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.shrink_block {ℓ n a m n' : ℕ} (D : Design ℓ n a m) (h : n' ≤ n) (i : Fin m) : (D.shrink h).block i = Finset.map ((Fin.castLEEmb h).trans ((D.block i).orderEmbOfFin ⋯).toEmbedding) Finset.univ

def Cslib.Crypto.PRG.NisanWigderson.Design.castLE {ℓ n a m ℓ' n' a' m' : ℕ} (D : Design ℓ n a m) (hℓ : ℓ ≤ ℓ') (hn : n' ≤ n) (ha : a ≤ a') (hm : m' ≤ m) : Design ℓ' n' a' m'

The design D with fewer blocks (the first m'), smaller blocks (of size n'), a larger universe (Fin ℓ') and a weaker intersection bound (a').

The polynomial construction

def Cslib.Crypto.PRG.NisanWigderson.polynomialBlock (F : Type u_1) [Field F] [Fintype F] (k : ℕ) (c : Fin k → F) : Finset (F × F)

The graph {(x, c₀ + c₁ x + ⋯ + cₖ₋₁ x ^ (k - 1)) | x ∈ F} of the polynomial over F with coefficients c : Fin k → F, a block of the Nisan–Wigderson design Design.polynomial F k.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.mem_polynomialBlock {F : Type u_1} [Field F] [Fintype F] {k : ℕ} {c : Fin k → F} {p : F × F} : p ∈ polynomialBlock F k c ↔ p.2 = ∑ i : Fin k, c i * p.1 ^ ↑i

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.card_polynomialBlock {F : Type u_1} [Field F] [Fintype F] {k : ℕ} (c : Fin k → F) : (polynomialBlock F k c).card = Fintype.card F

The graph of a polynomial over F has one point above each x ∈ F.

theorem Cslib.Crypto.PRG.NisanWigderson.card_polynomialBlock_inter_le {F : Type u_1} [Field F] [Fintype F] {k : ℕ} [DecidableEq F] {c d : Fin k → F} (hcd : c ≠ d) : (polynomialBlock F k c ∩ polynomialBlock F k d).card ≤ k - 1

The graphs of two distinct polynomials over F of degree less than k share at most k - 1 points: the difference of the polynomials is nonzero and has degree less than k, so it has at most k - 1 roots [NW94].

noncomputable def Cslib.Crypto.PRG.NisanWigderson.Design.polynomial (F : Type u_1) [Field F] [Fintype F] (k : ℕ) [DecidableEq F] : Design (Fintype.card F ^ 2) (Fintype.card F) (k - 1) (Fintype.card F ^ k)

The Nisan–Wigderson design over a finite field F with q elements [NW94]: a (q ^ 2, q, k - 1)-design with q ^ k blocks. Its blocks are the graphs polynomialBlock F k c of the polynomials of degree less than k over F, with the points of the plane F × F and the coefficient vectors c : Fin k → F numbered in some order.

theorem Cslib.Crypto.PRG.NisanWigderson.Design.nonempty_of_isPrimePow {q : ℕ} (hq : IsPrimePow q) (k : ℕ) : Nonempty (Design (q ^ 2) q (k - 1) (q ^ k))

For every prime power q and every k, there is a (q ^ 2, q, k - 1)-design with q ^ k blocks: the polynomial design Design.polynomial over a field with q elements [NW94].

theorem Cslib.Crypto.PRG.NisanWigderson.Design.nonempty_four_mul_sq (n k : ℕ) : Nonempty (Design (4 * n ^ 2) n (k - 1) ((n + 1) ^ k))

For all n and k, there is a (4 n ^ 2, n, k - 1)-design with (n + 1) ^ k blocks. By Bertrand's postulate there is a prime p with n < p ≤ 2 n; the polynomial design over the field with p elements has p ^ 2 ≤ 4 n ^ 2 points and p ^ k ≥ (n + 1) ^ k blocks of size p ≥ n, and keeping the n smallest elements of each block keeps the intersection bound.