Affine dispersers

A Boolean function f on n bits is an affine disperser for dimension d when it is nonconstant on the image of every injective affine map from BitString d (Cslib.BitString.IsAffineDisperser), informally on every affine subspace of dimension d. Dispersers for dimension d are dispersers for every larger dimension (Cslib.BitString.IsAffineDisperser.mono), and no function is a disperser for dimension 0 (Cslib.BitString.not_isAffineDisperser_zero).

Affine dispersers exist for every dimension d with n (d + 1) + 1 < 2 ^ d (Cslib.BitString.exists_isAffineDisperser), for instance for n = 100 and d = 11. There are at most 2 ^ (n (d + 1)) affine maps from BitString d to BitString n (Cslib.BitString.card_isAffine_le), and at most 2 · 2 ^ (2 ^ n - 2 ^ d) functions are constant on the image of each injective one (Cslib.BitString.card_const_on_range_le); together these are fewer than the 2 ^ 2 ^ n functions on n bits.

Main definitions

• Cslib.BitString.IsAffineDisperser: affine dispersers for dimension d.

Main results

• Cslib.BitString.IsAffineDisperser.mono: dispersers for smaller dimension are dispersers for larger dimension.
• Cslib.BitString.not_isAffineDisperser_zero: no function is an affine disperser for dimension 0.
• Cslib.BitString.exists_isAffineDisperser: affine dispersers exist for every dimension d with n (d + 1) + 1 < 2 ^ d.

References

• O. S. Mishra and R. Santhanam, An Explicit 3.5n − o(n) Size Lower Bound against General Boolean Circuits, Definition 2.1

def Cslib.BitString.IsAffineDisperser {n : ℕ} (f : BitString n → Bool) (d : ℕ) : Prop

f is an affine disperser for dimension d: it is nonconstant on the image of every injective affine map from BitString d. By Cslib.BitString.IsAffine.finrank_direction_map_top each such image is an affine subspace of dimension d, so nonconstancy on d-dimensional affine subspaces suffices (Cslib.BitString.isAffineDisperser_of_forall_exists_ne).

theorem Cslib.BitString.IsAffineDisperser.mono {n d d' : ℕ} {f : BitString n → Bool} (hf : IsAffineDisperser f d) (h : d ≤ d') : IsAffineDisperser f d'

Dispersers for dimension d are dispersers for every larger dimension.

theorem Cslib.BitString.not_isAffineDisperser_zero {n : ℕ} (f : BitString n → Bool) : ¬IsAffineDisperser f 0

No function is an affine disperser for dimension 0: it is constant on every point.

theorem Cslib.BitString.card_const_on_range_le {d n : ℕ} {g : BitString d → BitString n} (hg : Function.Injective g) : {f : BitString n → Bool | ∀ (x y : BitString d), f (g x) = f (g y)}.card ≤ 2 * 2 ^ (2 ^ n - 2 ^ d)

At most 2 · 2 ^ (2 ^ n - 2 ^ d) functions on n bits are constant on the image of an injective map from BitString d.

theorem Cslib.BitString.exists_isAffineDisperser {n d : ℕ} (h : n * (d + 1) + 1 < 2 ^ d) : ∃ (f : BitString n → Bool), IsAffineDisperser f d

Affine dispersers exist for every dimension d with n (d + 1) + 1 < 2 ^ d: fewer functions on n bits are constant on the image of some injective affine map from BitString d than there are functions.