Documentation

Complexity.Computability.Circuit.Boolean.MassProduction.Uhlig

Uhlig's mass-production theorem #

Every Boolean function on n inputs can be evaluated on 2 ^ d(n) independent inputs with (1 + o(1)) 2 ^ n / n gates, as long as d(n) log₂ n = o(n) [Uhl92]. This is Lupanov's worst-case bound for a single copy: up to this many copies of any function fit within the asymptotic single-copy ceiling 2 ^ n / n. The theorem does not compare them with the complexity of the particular function.

d layers of Uhlig.complexity_directProduct_two_mul_le with prefixes of p bits turn single copies on m inputs into 2 ^ d copies on d p + m inputs, multiplying the size by (2 ^ p + 1) ^ d and adding at most (2 ^ p + 1) ^ d d 2 ^ d times the overhead of one pair (complexity_directProduct_two_pow_le). With p = 2 log₂ n + 2 and Lupanov's synthesis on the remaining m inputs, the leading term is (2 ^ p + 1) ^ d 2 ^ m / m = (1 + o(1)) 2 ^ n / n, and every overhead is 2 ^ (o(n)).

The statements are denominator-free: for every precision P, eventually P * n * cost ≤ (P + 1) * 2 ^ n. For P > 0 this is cost ≤ (1 + 1 / P) 2 ^ n / n; the precision P = 0 is allowed but says nothing. The copy count may be any number up to 2 ^ d(n), including zero. Sizes count all gates; massComplexity charges NOT, AND and OR once and constants never. These are bounds on circuit size, not on the running time of a circuit constructor.

Main definitions #

Main results #

References #

The finite recursion #

source
theorem Cslib.Circuits.Boolean.MassProduction.layerOverhead_mono {p w w' : ℕ} (h : w ≤ w') :
Uhlig.layerOverhead p w ≤ Uhlig.layerOverhead p w'
source
theorem Cslib.Circuits.Boolean.MassProduction.layerOverhead_le (p w : ℕ) :
Uhlig.layerOverhead p w ≤ 32 * 8 ^ p * (p + 1) * (w + 2)

A crude polynomial bound on the overhead of one pair.

source
theorem Cslib.Circuits.Boolean.MassProduction.complexity_directProduct_two_pow_le {p m L H : ℕ} (hL : ∀ (g : BooleanFunction m), complexity interpretation (directProduct g 1) ≤ L) (d n : ℕ) :
n = d * p + m → (∀ e < d, Uhlig.layerOverhead p (e * p + m) ≤ H) → ∀ (f : BooleanFunction n), complexity interpretation (directProduct f (2 ^ d)) ≤ (2 ^ p + 1) ^ d * (L + d * 2 ^ d * H)

Iterated Uhlig layers. If every function on m inputs has a single copy of size at most L, then every function on d * p + m inputs has 2 ^ d copies of size at most (2 ^ p + 1) ^ d * (L + d * 2 ^ d * H), where H bounds the overhead of each layer.

Arithmetic estimates #

source
theorem Cslib.Circuits.Boolean.MassProduction.mul_add_one_pow_le {R M d : ℕ} (h : (R + 1) * d ≤ M) :
R * (M + 1) ^ d ≤ (R + 1) * M ^ d

(1 + 1 / M) ^ d ≤ 1 + 1 / R when (R + 1) d ≤ M, without denominators.

Asymptotics #

source
theorem Cslib.Circuits.Boolean.MassProduction.eventually_mul_complexity_single_le (Q : ℕ) :
∀ᶠ (m : ℕ) in Filter.atTop, ∀ (g : BooleanFunction m), Q * m * complexity interpretation (single g) ≤ (Q + 1) * 2 ^ m

Lupanov's bound for single copies, without denominators: for every precision Q, eventually Q * m * size ≤ (Q + 1) * 2 ^ m for every function on m inputs.

source
theorem Cslib.Circuits.Boolean.MassProduction.eventually_overhead_le (P : ℕ) :
∀ᶠ (n : ℕ) in Filter.atTop, 4 * P * n * (32 * 8 ^ (2 * Nat.log 2 n + 2) * (2 * Nat.log 2 n + 3) * (n + 2)) ≤ 2 ^ (n / 2)

The per-layer overhead with prefixes of 2 log₂ n + 2 bits is eventually below 2 ^ (n / 2), even after multiplication by 4 P n.

source
def Cslib.Circuits.Boolean.MassProduction.IsUhligDepth (depth : ℕ → ℕ) :
Prop

Discrete form of d(n) log₂ n = o(n): for every multiplier c, eventually c * d n * log₂ n ≤ n.

Instances For
    source
    theorem Cslib.Circuits.Boolean.MassProduction.mul_complexity_directProduct_le {P X n d p m : ℕ} (hX : 2 * P * (X + 1) ^ 3 ≤ (2 * P + 1) * X ^ 3) (hX0 : 0 < X) (hnm : n = d * p + m) (hm : 0 < m) (hdp : (X + 1) * (d * p) ≤ n) (hd : (X + 1) * d ≤ 2 ^ p) (hL : ∀ (g : BooleanFunction m), X * m * complexity interpretation (single g) ≤ (X + 1) * 2 ^ m) (hH : 4 * P * n * Uhlig.layerOverhead p n * 2 ^ (p * d + (d + d)) ≤ 2 ^ n) (f : BooleanFunction n) {k : ℕ} (hk : k ≤ 2 ^ d) :
    P * n * complexity interpretation (directProduct f k) ≤ (P + 1) * 2 ^ n

    Finite form of Uhlig's theorem. Split n = d * p + m inputs into d prefixes of p bits and m > 0 remaining inputs, and let X be a slack with 2 P (X + 1) ^ 3 ≤ (2 P + 1) X ^ 3. Suppose the prefixes use at most a 1 / (X + 1) fraction of the input, the 2 ^ p assignments of one prefix number at least (X + 1) d, single copies on m inputs have size at most (1 + 1 / X) 2 ^ m / m, and the overhead of all layers is negligible. Then every function on n inputs has k ≤ 2 ^ d independent copies of size s with P * n * s ≤ (P + 1) * 2 ^ n, that is, at most (1 + 1 / P) 2 ^ n / n when P > 0.

    source
    theorem Cslib.Circuits.Boolean.MassProduction.eventually_mul_complexity_directProduct_le {depth : ℕ → ℕ} (hdepth : IsUhligDepth depth) (P : ℕ) :
    ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (f : BooleanFunction n), ∀ k ≤ 2 ^ depth n, P * n * complexity interpretation (directProduct f k) ≤ (P + 1) * 2 ^ n

    Uhlig's theorem for circuit size. If d(n) log₂ n = o(n), then for every precision P, eventually every function on n inputs has k ≤ 2 ^ d(n) independent copies of size s with P * n * s ≤ (P + 1) * 2 ^ n: for P > 0, at most (1 + 1 / P) 2 ^ n / n. The case P = 0 holds trivially. Prefixes have 2 log₂ n + 2 bits.

    source
    theorem Cslib.Circuits.Boolean.MassProduction.eventually_mul_massComplexity_le {depth : ℕ → ℕ} (hdepth : IsUhligDepth depth) (P : ℕ) :
    ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (f : BooleanFunction n), ∀ k ≤ 2 ^ depth n, ↑P * ↑n * massComplexity f k ≤ ↑((P + 1) * 2 ^ n)

    Uhlig's theorem for mass complexity, which charges NOT, AND and OR once and constants never. If d(n) log₂ n = o(n), then for every precision P, eventually P * n * massComplexity f k ≤ (P + 1) * 2 ^ n for every function f on n inputs and every number of copies k ≤ 2 ^ d(n). For P > 0 the bound is (1 + 1 / P) 2 ^ n / n; the case P = 0 holds trivially.