Depth-three lower bounds from subcube-free accepted sets -- proofs

Internal proofs for Complexitylib.Circuits.DepthThree.

Every function has a Σ₃^1 formula (an OR of minterms), so Σ₃^k(f) is attained for k ≥ 1. De Morgan duality identifies Π₃^k(f) with Σ₃^k(¬f). If f = F_1 ∨ … ∨ F_t, every F_i accepts only inputs of f, so none of them contains a subcube of dimension D when f does not, and Theorem A bounds |f⁻¹(1)| ≤ t · 2 ^ ((1 - 1/k + ε) N + C D). A subcube of dimension 2 m with 2 ^ m ≥ K splits into a rectangle with both sides of size 2 ^ m, so a K-rectangle-free set contains no such subcube.

def Complexity.DepthThree.minterm {N : ℕ} (x : BitString N) : CNF N

The CNF accepting exactly x: one unit clause per variable.

Equations

• Complexity.DepthThree.minterm x = { clauses := List.map (fun (i : Fin N) => [{ var := i, polarity := x i }]) (List.finRange N) }

theorem Complexity.DepthThree.eval_minterm_eq_true_iff {N : ℕ} (x y : BitString N) : (minterm x).eval y = true ↔ y = x

theorem Complexity.DepthThree.width_minterm_le {N : ℕ} (x : BitString N) : (minterm x).width ≤ 1

theorem Complexity.DepthThree.exists_isSigmaThree {N k : ℕ} (hk : 1 ≤ k) (f : BitString N → Bool) : ∃ (Fs : List (CNF N)), IsSigmaThree k f Fs

Every function has a Σ₃^k formula for k ≥ 1: the OR of the minterms of its accepted inputs.

theorem Complexity.DepthThree.sigmaThreeSize_spec {N k : ℕ} (hk : 1 ≤ k) (f : BitString N → Bool) : ∃ (Fs : List (CNF N)), IsSigmaThree k f Fs ∧ Fs.length = sigmaThreeSize k f

theorem Complexity.DepthThree.sigmaThreeSize_le {N k : ℕ} {f : BitString N → Bool} {Fs : List (CNF N)} (h : IsSigmaThree k f Fs) : sigmaThreeSize k f ≤ Fs.length

theorem Complexity.DepthThree.isPiThree_iff {N k : ℕ} {f : BitString N → Bool} (Gs : List (DNF N)) : IsPiThree k f Gs ↔ IsSigmaThree k (fun (x : BitString N) => !f x) (List.map DNF.neg Gs)

De Morgan duality: an AND of DNFs computes f exactly when the OR of their negations, which are CNFs of the same widths, computes ¬f.

theorem Complexity.DepthThree.piThreeSize_eq_sigmaThreeSize_not {N : ℕ} (k : ℕ) (f : BitString N → Bool) : piThreeSize k f = sigmaThreeSize k fun (x : BitString N) => !f x

theorem Complexity.DepthThree.card_accepting_le (k : ℕ) (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (N : ℕ) (f : BitString N → Bool) (D : ℕ) (Fs : List (CNF N)), IsSigmaThree k f Fs → ¬ContainsSubcube {x : BitString N | f x = true} D → ↑{x : BitString N | f x = true}.card ≤ ↑Fs.length * 2 ^ ((1 - 1 / ↑k + ε) * ↑N + C * ↑D)

The finite bound. For k ≥ 1 and ε > 0 there is C ≥ 0 such that every OR of t CNFs of width at most k computing a function whose accepted inputs contain no subcube of dimension D has |f⁻¹(1)| ≤ t · 2 ^ ((1 - 1/k + ε) N + C D).

theorem Complexity.DepthThree.ncard_setOf_eq_card_filter {N : ℕ} (f : BitString N → Bool) : {x : BitString N | f x = true}.ncard = {x : BitString N | f x = true}.card

theorem Complexity.DepthThree.eventually_le_sigmaThreeSize {f : (n : ℕ) → BitString n → Bool} {D : ℕ → ℕ} (hD : (fun (n : ℕ) => ↑(D n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hfree : ∀ᶠ (n : ℕ) in Filter.atTop, ¬ContainsSubcube {x : BitString n | f n x = true} (D n)) (hdense : (fun (n : ℕ) => ↑n * Real.log 2 - Real.log ↑{x : BitString n | f n x = true}.ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {k : ℕ} (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ ((1 / ↑k - ε) * ↑n) ≤ ↑(sigmaThreeSize k (f n))

The asymptotic bound. Let f be a family of Boolean functions whose accepted sets eventually contain no subcube of dimension D n = o(n) and have logarithmic density deficit o(n). Then for every k ≥ 1 and ε > 0, eventually Σ₃^k(f n) ≥ 2 ^ ((1/k - ε) n).

theorem Complexity.DepthThree.not_containsSubcube_of_rectangleFree {N : ℕ} {S : Set (BitString N)} {K m : ℕ} (hS : Frontier.RectangleFree S K) (hK : K ≤ 2 ^ m) : ¬ContainsSubcube S (2 * m)

Rectangle-free sets contain no large subcubes. If K ≤ 2 ^ m, a K-rectangle-free set of inputs contains no subcube of dimension 2 m: such a subcube splits into a rectangle with both sides of size 2 ^ m.

theorem Complexity.DepthThree.clog_le_logb_add_one (K : ℕ) : ↑(Nat.clog 2 K) ≤ Real.logb 2 ↑K + 1

⌈log₂ K⌉ ≤ log₂ K + 1.

theorem Complexity.DepthThree.isLittleO_two_mul_clog {K : ℕ → ℕ} (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : (fun (n : ℕ) => ↑(2 * Nat.clog 2 (K n))) =o[Filter.atTop] fun (n : ℕ) => ↑n

If log K = o(n), then 2 ⌈log₂ K⌉ = o(n).