Affine dispersers from nonconstancy on affine subspaces

An affine disperser for dimension d (Cslib.BitString.IsAffineDisperser) is nonconstant on the image of every injective map g : BitString d → BitString n that preserves sums of three points (Cslib.BitString.IsAffine). Such an image is an affine subspace of dimension d in Mathlib's sense over 𝔽₂ = Bool: g is a Mathlib affine map with linear part x ↦ g x + g 0 (Cslib.BitString.IsAffine.toAffineMap), the image is the affine subspace ⊤.map g, and its direction, the range of the injective linear part, has dimension d (Cslib.BitString.IsAffine.finrank_direction_map_top).

Hence a function nonconstant on every affine subspace of dimension d 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 definitions

• Cslib.BitString.IsAffine.linearMap: the linear part x ↦ g x + g 0 of an affine map over 𝔽₂.
• Cslib.BitString.IsAffine.toAffineMap: an affine map over 𝔽₂ as a Mathlib affine map.

Main results

• Cslib.BitString.IsAffine.finrank_direction_map_top: the image of an injective affine map from V is an affine subspace whose direction has dimension finrank Bool V.
• 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

def Cslib.BitString.IsAffine.linearMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) : V →ₗ[Bool] W

The linear part x ↦ g x + g 0 of a map g that is affine over 𝔽₂.

@[simp]

theorem Cslib.BitString.IsAffine.linearMap_apply {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) (x : V) : hg.linearMap x = g x + g 0

The linear part of g sends x to g x + g 0.

theorem Cslib.BitString.IsAffine.linearMap_injective {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) (hinj : Function.Injective g) : Function.Injective ⇑hg.linearMap

The linear part of an injective map that is affine over 𝔽₂ is injective.

def Cslib.BitString.IsAffine.toAffineMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) : V →ᵃ[Bool] W

A map that is affine over 𝔽₂ (IsAffine) as a Mathlib affine map over Bool, with linear part x ↦ g x + g 0.

@[simp]

theorem Cslib.BitString.IsAffine.coe_toAffineMap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) : ⇑hg.toAffineMap = g

As a function, the Mathlib affine map of g is g itself.

theorem Cslib.BitString.IsAffine.finrank_direction_map_top {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module Bool V] [AddCommGroup W] [Module Bool W] {g : V → W} (hg : IsAffine g) (hinj : Function.Injective g) : Module.finrank Bool ↥(AffineSubspace.map hg.toAffineMap ⊤).direction = Module.finrank Bool V

The image of an injective map from V that is affine over 𝔽₂ is an affine subspace whose direction has the dimension of V.

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.