Shannon's lower bound for De Morgan circuits

This is the De Morgan specialization of Cslib.Circuits.Shannon.exists_hard_function, stated for circuits and for circuit complexity. Together with Lupanov's construction, it gives the asymptotically sharp gate count 2ⁿ/n.

theorem Cslib.Circuits.Boolean.Shannon.exists_hard_function : ∃ (N : ℕ), ∀ n ≥ N, ∃ (f : BooleanFunction n), ∀ (c : Circuit signature n 1), (c.Computes interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) → 2 ^ n / ↑n < ↑c.size

For all sufficiently large n, some Boolean function on n inputs requires more than 2ⁿ/n De Morgan gates, counting constants and negations.

theorem Cslib.Circuits.Boolean.Shannon.lt_complexity : ∃ (N : ℕ), ∀ n ≥ N, ∃ (f : BooleanFunction n), 2 ^ n / ↑n < ↑(complexity interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x)

Shannon's lower bound for circuit complexity: for all sufficiently large n, some Boolean function on n inputs has complexity more than 2ⁿ/n.