Affine dispersers

Over 𝔽₂, a map between additive groups is affine when it preserves sums of three points: g (x + y + z) = g x + g y + g z (Cslib.BitString.IsAffine). For maps between 𝔽₂-vector spaces this is the usual notion, a translate of a linear map (Cslib.BitString.IsAffine.toAffineMap in Complexity/Foundations/Combinatorics/AffineDisperser/AffineSubspace.lean), and the image of an injective affine map from BitString d is an affine subspace of dimension d of the cube BitString n (Cslib.BitString.IsAffine.finrank_direction_map_top), so nonconstancy on every d-dimensional affine subspace gives an affine disperser (Cslib.BitString.isAffineDisperser_of_forall_exists_ne); everything in this file is stated in terms of affine maps.

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 (IsAffineDisperser.mono), and no function is a disperser for dimension 0 (not_isAffineDisperser_zero).

Affine dispersers exist for every dimension d with n (d + 1) + 1 < 2 ^ d (exists_isAffineDisperser), for instance for n = 100 and d = 11. The proof counts: an affine map from BitString d is determined by its values at 0 and at the unit vectors (IsAffine.ext_single), so there are at most 2 ^ (n (d + 1)) of them (card_isAffine_le), and at most 2 · 2 ^ (2 ^ n - 2 ^ d) functions are constant on the image of each injective one (card_const_on_range_le); together these are fewer than the 2 ^ 2 ^ n functions on n bits.

Main definitions

• Cslib.BitString.IsAffine: affine maps over 𝔽₂.
• Cslib.BitString.IsAffineDisperser: affine dispersers.
• Cslib.BitString.zeroExtend: extension of a bit string by zeros to a longer length.

Main results

• Cslib.BitString.IsAffine.comp: affine maps compose.
• Cslib.BitString.IsAffineDisperser.mono: dispersers for smaller dimension are dispersers for larger dimension.
• 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.IsAffine {α : Type u_1} {β : Type u_2} [Add α] [Add β] (g : α → β) : Prop

A map is affine over 𝔽₂ when it preserves sums of three points.

theorem Cslib.BitString.IsAffine.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Add α] [Add β] [Add γ] {g : β → γ} {h : α → β} (hg : IsAffine g) (hh : IsAffine h) : IsAffine (g ∘ h)

The composition of affine maps is affine.

theorem Cslib.BitString.isAffine_const {α : Type u_1} {β : Type u_2} [Add α] [AddGroup β] (h : ∀ (b : β), b + b = 0) (c : β) : IsAffine fun (x : α) => c

Constant maps into a group in which every element is its own negative (b + b = 0) are affine.

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).

def Cslib.BitString.zeroExtend {d d' : ℕ} (x : BitString d) : BitString d'

The extension of a point of BitString d by zeros to BitString d', for d ≤ d'.

theorem Cslib.BitString.isAffine_zeroExtend {d d' : ℕ} : IsAffine zeroExtend

Extension by zeros is affine.

theorem Cslib.BitString.zeroExtend_injective {d d' : ℕ} (h : d ≤ d') : Function.Injective zeroExtend

Extension by zeros from BitString d to BitString d' is injective when d ≤ d'.

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.

Existence of affine dispersers by counting

@[instance_reducible]

instance Cslib.BitString.instDecidableIsAffineOfFintypeOfDecidableEq {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] [Add α] [Add β] (g : α → β) : Decidable (IsAffine g)

Affinity of a map between finite types is decidable.

theorem Cslib.BitString.IsAffine.ext_single {d n : ℕ} {g g' : BitString d → BitString n} (hg : IsAffine g) (hg' : IsAffine g') (h0 : g 0 = g' 0) (hi : ∀ (i : Fin d), g (Pi.single i true) = g' (Pi.single i true)) : g = g'

Affine maps from BitString d agreeing at 0 and at the unit vectors are equal.

theorem Cslib.BitString.card_isAffine_le (d n : ℕ) : {g : BitString d → BitString n | IsAffine g}.card ≤ 2 ^ (n * (d + 1))

At most 2 ^ (n (d + 1)) maps from BitString d to BitString n are affine.

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.