Affine dispersers from nonconstancy on affine subspaces

Because the image of an injective affine map from BitString d is an affine subspace of BitString n of dimension d (Cslib.BitString.IsAffine.finrank_direction_map_top), any function nonconstant on every d-dimensional affine subspace is an affine disperser for dimension d (Cslib.BitString.isAffineDisperser_of_forall_exists_ne). This turns nonconstancy theorems stated with AffineSubspace, such as Ben-Sasson and Kopparty's, into affine dispersers. The converse, that every affine subspace of dimension d contains such an image, is not formalized here: Mathlib has no Field Bool instance, so a basis of the direction is not available over Bool.

Main results

• Cslib.BitString.isAffineDisperser_of_forall_exists_ne: a function nonconstant on every affine subspace of dimension d is an affine disperser for dimension d.

References

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

theorem Cslib.BitString.isAffineDisperser_of_forall_exists_ne {n d : ℕ} {f : BitString n → Bool} (h : ∀ (A : AffineSubspace Bool (BitString n)), Module.finrank Bool ↥A.direction = d → ∃ x ∈ A, ∃ y ∈ A, f x ≠ f y) : IsAffineDisperser f d

A function nonconstant on every affine subspace of BitString n of dimension d is an affine disperser for dimension d: the image of an injective affine map from BitString d is such a subspace.