Affine maps over 𝔽₂

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_iff_exists_affineMap in Complexity/Foundations/Data/BitString/AffineSubspace.lean).

An affine map from BitString d is determined by its values at 0 and at the unit vectors (Cslib.BitString.IsAffine.ext_single), so there are at most 2 ^ (n (d + 1)) affine maps from BitString d to BitString n (Cslib.BitString.card_isAffine_le).

Main definitions

• Cslib.BitString.IsAffine: affine maps over 𝔽₂.

Main results

• Cslib.BitString.IsAffine.comp: affine maps compose.
• Cslib.BitString.isAffine_zeroExtend: extension by zeros is affine.
• Cslib.BitString.IsAffine.ext_single: an affine map from BitString d is determined by its values at 0 and at the unit vectors.
• Cslib.BitString.card_isAffine_le: at most 2 ^ (n (d + 1)) maps from BitString d to BitString n are affine.
• Cslib.BitString.exists_affine_of_add_add: a Boolean function satisfying g (u + w) = g u + g w + g 0 and depending only on a finite set M is g u = g 0 + ∑ i ∈ T, u i for some T ⊆ M.
• Cslib.BitString.eq_add_sum_of_step: prefix sums of a step recurrence z (j + 1) = z j + f j over 𝔽₂.

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.

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

Extension by zeros is affine.

Counting affine maps

@[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.exists_affine_of_add_add {ι : Type u_1} {M : Finset ι} {g : (ι → Bool) → Bool} (hcongr : ∀ (u u' : ι → Bool), (∀ j ∈ M, u j = u' j) → g u = g u') (hadd : ∀ (u u' u'' : ι → Bool), g (u + u' + u'') = g u + g u' + g u'') : ∃ T ⊆ M, ∀ (u : ι → Bool), g u = g 0 + ∑ j ∈ T, u j

A function of bits that depends only on the coordinates in M and preserves sums of three points is affine: a constant plus the sum of the coordinates in some T ⊆ M.

theorem Cslib.BitString.eq_add_sum_of_step {z f : ℕ → Bool} {c : Bool} {n : ℕ} (h0 : z 0 = c) (hstep : ∀ j < n, z (j + 1) = (z j ^^ f j)) (j : ℕ) : j ≤ n → z j = c + ∑ j' ∈ Finset.range j, f j'

A sequence that starts at c and adds f j at each step j < n holds c + ∑ j' < j, f j' up to step n.