The powering construction of small-bias spaces

Let F be a field with 2 ^ m elements, written as m-bit strings by an additive bijection bits : F ≃+ BitString m. The powering sample space of Alon, Goldreich, Håstad and Peralta Alon, Goldreich, Håstad and Peralta, Section 3 maps a seed (x, y) ∈ F × F, which is 2 m bits, to the n bits ⟨bits (x ^ i), bits y⟩, i < n, where ⟨u, v⟩ = u ⬝ᵥ v is the inner product of bit strings modulo two (Cslib.BitString.powering).

The parity of the bits in a set S is ⟨bits (p_S x), bits y⟩ for the polynomial p_S = ∑_{i ∈ S} X ^ i. For a fixed x with p_S x ≠ 0 this is an unbiased bit over the uniform y, and with p_S x = 0 it is constantly zero, so the bias at S is the fraction of roots of p_S in F (Cslib.BitString.bias_powering). A nonempty S gives a nonzero p_S of degree less than n, so the powering space is ((n - 1) / 2 ^ m)-biased (Cslib.BitString.isSmallBias_powering). Fields with 2 ^ m elements exist for every m ≠ 0, so 2 m uniform bits can be stretched to n bits with bias at most (n - 1) / 2 ^ m (Cslib.BitString.exists_isSmallBias_uniformOfFintype_map).

These are statements about distributions; computing the sample space efficiently needs arithmetic in F, which is not certified here.

Main definitions

• Cslib.BitString.powering: the powering sample space.

Main results

• Cslib.BitString.bias_powering: the bias of the powering space at S is the fraction of roots of ∑_{i ∈ S} X ^ i.
• Cslib.BitString.isSmallBias_powering: the powering space is ((n - 1) / |F|)-biased.
• Cslib.BitString.exists_isSmallBias_uniformOfFintype_map: 2 m uniform bits stretch to n bits with bias at most (n - 1) / 2 ^ m.

References

• N. Alon, O. Goldreich, J. Håstad, R. Peralta, Simple constructions of almost k-wise independent random variables

def Cslib.BitString.powering {F : Type u_1} [Field F] {m : ℕ} (bits : F ≃+ BitString m) (n : ℕ) (s : F × F) : BitString n

The powering sample space of Alon, Goldreich, Håstad and Peralta Alon, Goldreich, Håstad and Peralta, Section 3: the seed (x, y) ∈ F × F gives the n bits ⟨bits (x ^ i), bits y⟩, i < n, inner products of bit strings modulo two.

theorem Cslib.BitString.bias_powering {F : Type u_1} [Field F] [Fintype F] {m : ℕ} (bits : F ≃+ BitString m) {n : ℕ} [DecidableEq F] (S : Finset (Fin n)) : bias (PMF.map (powering bits n) (Probability.PMF.uniformOfFintype (F × F))) S = ↑{x : F | ∑ i ∈ S, x ^ ↑i = 0}.dens

The bias of the powering space at S is the fraction of the roots of ∑_{i ∈ S} X ^ i in F.

theorem Cslib.BitString.isSmallBias_powering {F : Type u_1} [Field F] [Fintype F] {m : ℕ} (bits : F ≃+ BitString m) {n : ℕ} : IsSmallBias (↑(n - 1) / ↑(Fintype.card F)) (PMF.map (powering bits n) (Probability.PMF.uniformOfFintype (F × F)))

The powering space has small bias Alon, Goldreich, Håstad and Peralta, Section 3: it is ((n - 1) / |F|)-biased.

theorem Cslib.BitString.exists_isSmallBias_uniformOfFintype_map (n : ℕ) {m : ℕ} (hm : m ≠ 0) : ∃ (g : BitString (2 * m) → BitString n), IsSmallBias (↑(n - 1) / 2 ^ m) (PMF.map g (Probability.PMF.uniformOfFintype (BitString (2 * m))))

Small-bias spaces from the powering construction: for every m ≠ 0 there is a map from 2 m bits to n bits whose image of the uniform distribution is ((n - 1) / 2 ^ m)-biased.