Boolean algebraic normal forms

A squarefree monomial is a finite set of input variables. Multiplication is set union, so the resulting monoid algebra over ZMod 2 is exactly the Boolean ANF quotient in canonical normal form.

@[reducible, inline]

abbrev UnrestrictedBooleanMul.F₂ : Type

The two-element field of Boolean coefficients.

Equations

• UnrestrictedBooleanMul.F₂ = ZMod 2

structure UnrestrictedBooleanMul.Monomial (m : ℕ) : Type

A squarefree monomial in m Boolean variables.

• vars : Finset (Fin m)

  Variables occurring in this squarefree monomial.

theorem UnrestrictedBooleanMul.Monomial.ext {m : ℕ} {x y : Monomial m} (vars : x.vars = y.vars) : x = y

theorem UnrestrictedBooleanMul.Monomial.ext_iff {m : ℕ} {x y : Monomial m} : x = y ↔ x.vars = y.vars

@[instance_reducible]

instance UnrestrictedBooleanMul.instDecidableEqMonomial {m✝ : ℕ} : DecidableEq (Monomial m✝)

Equations

• UnrestrictedBooleanMul.instDecidableEqMonomial = UnrestrictedBooleanMul.instDecidableEqMonomial.decEq

def UnrestrictedBooleanMul.instDecidableEqMonomial.decEq {m✝ : ℕ} (x✝ x✝¹ : Monomial m✝) : Decidable (x✝ = x✝¹)

Equations

• UnrestrictedBooleanMul.instDecidableEqMonomial.decEq { vars := a } { vars := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def UnrestrictedBooleanMul.Monomial.equivFinset {m : ℕ} : Monomial m ≃ Finset (Fin m)

Identify a squarefree monomial with its finite set of variables.

Equations

• UnrestrictedBooleanMul.Monomial.equivFinset = { toFun := UnrestrictedBooleanMul.Monomial.vars, invFun := UnrestrictedBooleanMul.Monomial.mk, left_inv := ⋯, right_inv := ⋯ }

@[instance_reducible]

instance UnrestrictedBooleanMul.Monomial.instFintype {m : ℕ} : Fintype (Monomial m)

Equations

• UnrestrictedBooleanMul.Monomial.instFintype = Fintype.ofEquiv (Finset (Fin m)) UnrestrictedBooleanMul.Monomial.equivFinset.symm

@[instance_reducible]

instance UnrestrictedBooleanMul.instCommMonoidMonomial {m : ℕ} : CommMonoid (Monomial m)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UnrestrictedBooleanMul.Monomial.one_vars {m : ℕ} : vars 1 = ∅

@[simp]

theorem UnrestrictedBooleanMul.Monomial.mul_vars {m : ℕ} (s t : Monomial m) : (s * t).vars = s.vars ∪ t.vars

@[simp]

theorem UnrestrictedBooleanMul.Monomial.singleton_mul_singleton {m : ℕ} (i j : Fin m) : { vars := {i} } * { vars := {j} } = { vars := {i, j} }

@[reducible, inline]

abbrev UnrestrictedBooleanMul.ANF (m : ℕ) : Type

Canonical Boolean algebraic normal forms in m variables.

Equations

• UnrestrictedBooleanMul.ANF m = MonoidAlgebra UnrestrictedBooleanMul.F₂ (UnrestrictedBooleanMul.Monomial m)

noncomputable def UnrestrictedBooleanMul.monomial {m : ℕ} (s : Finset (Fin m)) : ANF m

The ANF consisting of one squarefree monomial.

Equations

• UnrestrictedBooleanMul.monomial s = MonoidAlgebra.single { vars := s } 1

@[simp]

theorem UnrestrictedBooleanMul.coeff_monomial {m : ℕ} (s t : Finset (Fin m)) : (monomial s).coeff { vars := t } = if s = t then 1 else 0

theorem UnrestrictedBooleanMul.coeff_sum_smul_mul_sum_smul {m : ℕ} {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (p : ι → ANF m) (q : κ → ANF m) (a : ι → F₂) (b : κ → F₂) (s : Monomial m) : ((∑ i : ι, a i • p i) * ∑ j : κ, b j • q j).coeff s = ∑ i : ι, ∑ j : κ, a i * b j * (p i * q j).coeff s

Extract a product coefficient bilinearly, before expanding either ANF.

noncomputable def UnrestrictedBooleanMul.X {m : ℕ} (i : Fin m) : ANF m

The ith input variable.

Equations

• UnrestrictedBooleanMul.X i = UnrestrictedBooleanMul.monomial {i}

@[simp]

theorem UnrestrictedBooleanMul.monomial_mul {m : ℕ} (s t : Finset (Fin m)) : monomial s * monomial t = monomial (s ∪ t)

theorem UnrestrictedBooleanMul.X_mul_self {m : ℕ} (i : Fin m) : X i * X i = X i

@[simp]

theorem UnrestrictedBooleanMul.anf_add_self {m : ℕ} (p : ANF m) : p + p = 0

@[simp]

theorem UnrestrictedBooleanMul.anf_two_eq_zero {m : ℕ} : 2 = 0

@[simp]

theorem UnrestrictedBooleanMul.anf_four_eq_zero {m : ℕ} : 4 = 0

def UnrestrictedBooleanMul.eval {m : ℕ} (p : ANF m) (x : Fin m → F₂) : F₂

Evaluation of a canonical ANF on a Boolean input.

Equations

• UnrestrictedBooleanMul.eval p x = p.coeff.sum fun (s : UnrestrictedBooleanMul.Monomial m) (c : UnrestrictedBooleanMul.F₂) => c * ∏ i ∈ s.vars, x i

@[simp]

theorem UnrestrictedBooleanMul.eval_monomial {m : ℕ} (s : Finset (Fin m)) (x : Fin m → F₂) : eval (monomial s) x = ∏ i ∈ s, x i

@[simp]

theorem UnrestrictedBooleanMul.eval_X {m : ℕ} (i : Fin m) (x : Fin m → F₂) : eval (X i) x = x i

@[simp]

theorem UnrestrictedBooleanMul.anf_one_coeff {m : ℕ} (s : Monomial m) : (MonoidAlgebra.coeff 1) s = if s = 1 then 1 else 0

theorem UnrestrictedBooleanMul.f2_eq_zero_or_one (x : F₂) : x = 0 ∨ x = 1

theorem UnrestrictedBooleanMul.prod_union_f2 {m : ℕ} (x : Fin m → F₂) (s t : Finset (Fin m)) : ∏ i ∈ s ∪ t, x i = (∏ i ∈ s, x i) * ∏ i ∈ t, x i

def UnrestrictedBooleanMul.monomialEval {m : ℕ} (x : Fin m → F₂) : Monomial m →* F₂

Evaluation of a squarefree monomial as a monoid homomorphism.

Equations

• UnrestrictedBooleanMul.monomialEval x = { toFun := fun (s : UnrestrictedBooleanMul.Monomial m) => ∏ i ∈ s.vars, x i, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def UnrestrictedBooleanMul.evalHom {m : ℕ} (x : Fin m → F₂) : ANF m →ₐ[F₂] F₂

Evaluation at a Boolean point as an F₂-algebra homomorphism.

Equations

• UnrestrictedBooleanMul.evalHom x = (MonoidAlgebra.lift UnrestrictedBooleanMul.F₂ UnrestrictedBooleanMul.F₂ (UnrestrictedBooleanMul.Monomial m)) (UnrestrictedBooleanMul.monomialEval x)

theorem UnrestrictedBooleanMul.eval_eq_evalHom {m : ℕ} (p : ANF m) (x : Fin m → F₂) : eval p x = (evalHom x) p

@[simp]

theorem UnrestrictedBooleanMul.eval_zero' {m : ℕ} (x : Fin m → F₂) : eval 0 x = 0

@[simp]

theorem UnrestrictedBooleanMul.eval_one' {m : ℕ} (x : Fin m → F₂) : eval 1 x = 1

@[simp]

theorem UnrestrictedBooleanMul.eval_add' {m : ℕ} (p q : ANF m) (x : Fin m → F₂) : eval (p + q) x = eval p x + eval q x

@[simp]

theorem UnrestrictedBooleanMul.eval_mul' {m : ℕ} (p q : ANF m) (x : Fin m → F₂) : eval (p * q) x = eval p x * eval q x

@[simp]

theorem UnrestrictedBooleanMul.eval_smul' {m : ℕ} (c : F₂) (p : ANF m) (x : Fin m → F₂) : eval (c • p) x = c * eval p x

noncomputable def UnrestrictedBooleanMul.evalLinearMap (m : ℕ) : ANF m →ₗ[F₂] (Fin m → F₂) → F₂

Simultaneous evaluation at all Boolean inputs, as a linear map.

Equations

• UnrestrictedBooleanMul.evalLinearMap m = { toFun := fun (p : UnrestrictedBooleanMul.ANF m) => UnrestrictedBooleanMul.eval p, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def UnrestrictedBooleanMul.pointIndicator {m : ℕ} (x : Fin m → F₂) : ANF m

The Boolean polynomial which is one at x and zero at every other input.

Equations

• UnrestrictedBooleanMul.pointIndicator x = ∏ i : Fin m, if x i = 1 then UnrestrictedBooleanMul.X i else 1 + UnrestrictedBooleanMul.X i

@[simp]

theorem UnrestrictedBooleanMul.eval_pointIndicator {m : ℕ} (x y : Fin m → F₂) : eval (pointIndicator x) y = if y = x then 1 else 0

theorem UnrestrictedBooleanMul.evalLinearMap_surjective (m : ℕ) : Function.Surjective ⇑(evalLinearMap m)

theorem UnrestrictedBooleanMul.evalLinearMap_finrank (m : ℕ) : Module.finrank F₂ (ANF m) = Module.finrank F₂ ((Fin m → F₂) → F₂)

theorem UnrestrictedBooleanMul.eval_injective (m : ℕ) : Function.Injective fun (p : ANF m) => eval p

Canonical Boolean ANFs are determined by their values on Boolean inputs.

noncomputable def UnrestrictedBooleanMul.evalLinearEquiv (m : ℕ) : ANF m ≃ₗ[F₂] (Fin m → F₂) → F₂

Canonical Boolean ANFs are linearly equivalent to all Boolean functions.

Equations

• UnrestrictedBooleanMul.evalLinearEquiv m = LinearEquiv.ofBijective (UnrestrictedBooleanMul.evalLinearMap m) ⋯

noncomputable def UnrestrictedBooleanMul.affine (m : ℕ) : Submodule F₂ (ANF m)

The subspace of constants and input-linear functions.

Equations

• UnrestrictedBooleanMul.affine m = Submodule.span UnrestrictedBooleanMul.F₂ ({1} ∪ Set.range UnrestrictedBooleanMul.X)

theorem UnrestrictedBooleanMul.one_mem_affine (m : ℕ) : 1 ∈ affine m

theorem UnrestrictedBooleanMul.X_mem_affine {m : ℕ} (i : Fin m) : X i ∈ affine m