Moore determinants in characteristic two

The Moore matrix of u : Fin k → F is (u l ^ 2 ^ m)_{l, m}; its determinant is the Moore determinant of u over 𝔽₂. In characteristic two determinants and permanents agree.

The Moore determinant is the k-th finite difference of x ↦ x ^ (2 ^ k - 1): since x ^ (2 ^ k - 1) = ∏_{m < k} x ^ 2 ^ m is a product of k additive functions, ∑_{c ∈ 𝔽₂ᵏ} (a + ∑ cₗ uₗ) ^ (2 ^ k - 1) = det (u l ^ 2 ^ m) for every base point a.

For a linearized function Q x = ∑_{j ∈ ℤ/n} a j * x ^ 2 ^ j on a field with 2 ^ n elements, the Moore permanent of Q ∘ w expands in the monomials ∏ₗ wₗ ^ 2 ^ τₗ, τ : Fin k → ℤ/n, with coefficient the permanent of (a (τ l - m) ^ 2 ^ m)_{l, m} [BenSassonKopparty2012, Lemma 3.13].

Main definitions

• Cslib.mooreMatrix: the matrix (u l ^ 2 ^ m).

Main results

• Matrix.det_eq_permanent_of_charTwo: determinant and permanent agree in characteristic two.
• Cslib.sum_cube_pow_eq_det_mooreMatrix: the Moore determinant as a finite difference.
• Cslib.permanent_mooreMatrix_linearizedEval: the monomial expansion of the Moore permanent of a composition with a linearized function.

References

• E. Ben-Sasson, S. Kopparty, Affine dispersers from subspace polynomials

def Cslib.mooreMatrix {F : Type u_1} [Field F] {k : ℕ} (u : Fin k → F) : Matrix (Fin k) (Fin k) F

The Moore matrix (u l ^ 2 ^ m)_{l, m} of a family u : Fin k → F.

@[simp]

theorem Cslib.mooreMatrix_apply {F : Type u_1} [Field F] {k : ℕ} (u : Fin k → F) (l m : Fin k) : mooreMatrix u l m = u l ^ 2 ^ ↑m

Entry (l, m) of the Moore matrix is u l ^ 2 ^ m.

theorem Matrix.det_eq_permanent_of_charTwo {R : Type u_2} {ι : Type u_3} [CommRing R] [CharP R 2] [Fintype ι] [DecidableEq ι] (M : Matrix ι ι R) : M.det = M.permanent

In characteristic two the determinant of a matrix is its permanent.

theorem Cslib.pow_two_pow_sub_one_eq_prod {R : Type u_2} [CommMonoid R] (x : R) (k : ℕ) : x ^ (2 ^ k - 1) = ∏ m : Fin k, x ^ 2 ^ ↑m

x ^ (2 ^ k - 1) is the product of the k additive powers x ^ 2 ^ m, m < k.

theorem Cslib.sum_cube_pow_eq_det_mooreMatrix {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {k : ℕ} (a : F) (u : Fin k → F) : ∑ c : Fin k → ZMod 2, (a + ∑ l : Fin k, c l • u l) ^ (2 ^ k - 1) = (mooreMatrix u).det

The Moore determinant is a finite difference: for every base point a, ∑_{c ∈ 𝔽₂ᵏ} (a + ∑ cₗ uₗ) ^ (2 ^ k - 1) is the Moore determinant of u.

theorem Cslib.permanent_mooreMatrix_linearizedEval {F : Type u_1} [Field F] [Algebra (ZMod 2) F] [Finite F] {n : ℕ} [NeZero n] (hn : Module.finrank (ZMod 2) F = n) (a : ZMod n → F) {k : ℕ} (w : Fin k → F) : (mooreMatrix fun (l : Fin k) => linearizedEval a (w l)).permanent = ∑ τ : Fin k → ZMod n, (Matrix.of fun (l m : Fin k) => a (τ l - ↑↑m) ^ 2 ^ ↑m).permanent * ∏ l : Fin k, w l ^ 2 ^ (τ l).val

Monomial expansion of a Moore permanent, an analogue of [BenSassonKopparty2012, Lemma 3.13]: for the linearized function Q = linearizedEval a on a field with 2 ^ n elements, per (Q (w l) ^ 2 ^ m) = ∑_τ per (a (τ l - m) ^ 2 ^ m) * ∏ₗ w l ^ 2 ^ τ l, the sum ranging over all τ : Fin k → ZMod n.