Counting De Morgan circuits

This file specializes the generic circuit counting bound to the five De Morgan operations, all of arity at most two. The resulting factorial correction is used in Shannon's lower bound.

@[reducible, inline]

noncomputable abbrev Cslib.Circuits.Boolean.computableFunctions (n s : ℕ) : Finset (BooleanFunction n)

Boolean functions on n inputs computable with at most s De Morgan gates.

Equations

• Cslib.Circuits.Boolean.computableFunctions n s = Cslib.Circuits.computableFunctions Cslib.Circuits.Boolean.interpretation n s

theorem Cslib.Circuits.Boolean.mem_computableFunctions {n s : ℕ} {f : BooleanFunction n} : f ∈ computableFunctions n s ↔ ∃ (c : Circuit signature n 1), (c.Computes interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) ∧ c.size ≤ s

theorem Cslib.Circuits.Boolean.card_computableFunctions_mul_factorial_le (n s : ℕ) : (computableFunctions n s).card * s.factorial ≤ (s + 1) * (5 * (n + s + 1) ^ 2) ^ s * (n + s)

The De Morgan counting bound, accounting for gate relabelings.