Lupanov's asymptotically optimal upper bound

Every Boolean function on n inputs has a De Morgan circuit with at most (1 + ε) * 2 ^ n / n gates for all sufficiently large n, given any ε > 0. The threshold is uniform in the function; size counts constants and negations. This matches Shannon's counting lower bound up to the factor 1 + ε, which is why the bound is called asymptotically optimal.

This file only does the asymptotics. The circuit comes from the block construction in LupanovConstruction.lean, which gives, for any split of the inputs into k address bits and d data bits and any positive block size s, a circuit with at most bound k d s gates.

Choosing the parameters

Write l = log₂ n. We take k = 3 l address bits, d = n - 3 l data bits, and blocks of s = n - 5 l rows. Then:

• the leading term of bound is (2 ^ k / s + 1) · 2 ^ d ≈ 2 ^ n / s, and since s = n - 5 l is n (1 - o(1)), this is (1 + o(1)) 2 ^ n / n (mainTerm_le);
• the minterms cost about (2 ^ k + 2 ^ d) · 2 n = O(n ^ 4) + O(2 ^ n / n ^ 2), using 2 ^ k ≤ n ^ 3;
• the left parts cost about (2 ^ k / s) · 2 ^ s · 2 s ≈ 2 ^ (k + s) = 2 ^ (n - 2 l), which is O(2 ^ n / n ^ 2).

bound_le packages the two error terms as 3 n ^ 4 + 16 n · 2 ^ d; Nat.eventually_mul_pow_le_pow and error_le show that the polynomial and the exponential term are each o(2 ^ n / n). Then eventually_bound_le combines everything into P · n · bound ≤ (P + 1) · 2 ^ n for all large n, for any natural number P. Taking P > 1 / ε in exists_circuit gives the theorem.

References

• O. B. Lupanov, On a Method of Circuit Synthesis, Theorem 4 and Section 6, pp. 131-135: the upper bound for general weighted bases, specialized here to the De Morgan basis.
• Stasys Jukna, Boolean Function Complexity: Advances and Frontiers, Theorem 1.15: a modern exposition.

theorem Cslib.Circuits.Boolean.Lupanov.exists_circuit (ε : ℝ) (hε : 0 < ε) : ∃ (N : ℕ), ∀ n ≥ N, ∀ (f : BooleanFunction n), ∃ (g : ℕ) (c : Circuit signature n g 1), c.Computes interpretation f ∧ ↑c.size ≤ (1 + ε) * 2 ^ n / ↑n

Lupanov's upper bound: every Boolean function on n inputs has a De Morgan circuit with at most (1 + ε) 2ⁿ/n gates, uniformly for sufficiently large n.

Pick a natural number P > 1 / ε, so that (P + 1) / P < 1 + ε; then the threshold N comes from eventually_bound_le P.