Depth-three lower bounds for subcube dispersers

A Σ₃^k formula is an OR of k-CNFs (IsSigmaThree), and Σ₃^k(f) is the least number of k-CNFs in one computing f (sigmaThreeSize); Π₃^k(f) = Σ₃^k(¬f) (piThreeSize). If the accepted inputs of f contain no subcube of dimension D, neither do those of any k-CNF in an OR computing f, so Theorem A (CNF.card_accepting_le_of_not_containsSubcube) gives

|f⁻¹(1)| ≤ Σ₃^k(f) · 2 ^ ((1 - 1/k + ε) N + C D).

For a family of functions that accept at least 2 ^ (n - o(n)) inputs and whose accepted sets contain no subcube of dimension o(n) (a subcube disperser), this is Σ₃^k(f) ≥ 2 ^ ((1/k - o(1)) n) for every fixed k. Rectangle-free sets with threshold 2 ^ o(n), such as those of the frontier method (Complexity.Frontier.RectangleFree), are subcube dispersers. Complexitylib.Circuits.DepthThree.Explicit applies this to an explicit family in P.

The exponent 1/k cannot be improved for subcube dispersers: parity accepts no subcube of dimension one, and when k divides n it is the OR of 2 ^ (n/k - 1) k-CNFs, one for each even-weight pattern of the parities of n/k blocks of k variables (Paturi, Pudlák and Zane). For comparison, Frankl, Gryaznov and Talebanfard (ITCS 2022) prove Σ₃^3 ≥ 2 ^ (0.064 n) and Σ₃^k ≥ 2 ^ (n/(10k)) for affine dispersers through the switching lemma. A subcube is an affine subspace, so an affine disperser for sublinear dimension that accepts 2 ^ (n - o(n)) inputs is a subcube disperser, and the bound here has exponent 1/k - o(1) for it.

Main results

• exists_isSigmaThree_length_eq_sigmaThreeSize, sigmaThreeSize_le_length: Σ₃^k(f) is attained for k ≥ 1.
• piThreeSize_eq_sigmaThreeSize_not: De Morgan duality.
• card_accepting_le_sigmaThreeSize: the finite bound.
• eventually_two_rpow_le_sigmaThreeSize, eventually_two_rpow_le_piThreeSize: the asymptotic bounds for subcube dispersers.
• not_containsSubcube_of_rectangleFree, eventually_two_rpow_le_sigmaThreeSize_of_rectangleFree: rectangle-free families.

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

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

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

For k ≥ 1, Σ₃^k(f) is the size of some Σ₃^k formula for f.

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

Σ₃^k(f) is at most the size of every Σ₃^k formula for f.

theorem Complexity.isPiThree_iff_isSigmaThree_map_neg {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, CNFs of the same widths, computes ¬f.

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

Π₃^k(f) = Σ₃^k(¬f).

theorem Complexity.IsSigmaThree.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 every k ≥ 1 and ε > 0 there is C ≥ 0 such that, if the accepted inputs of f contain no subcube of dimension D, then every OR of t CNFs of width at most k computing f has |f⁻¹(1)| ≤ t · 2 ^ ((1 - 1/k + ε) N + C D).

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

The finite bound for Σ₃^k. For every k ≥ 1 and ε > 0 there is C ≥ 0 such that every f whose accepted inputs contain no subcube of dimension D has |f⁻¹(1)| ≤ Σ₃^k(f) · 2 ^ ((1 - 1/k + ε) N + C D).

theorem Complexity.eventually_two_rpow_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))

Σ₃^k lower bound for subcube dispersers. 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 n log 2 - log |f⁻¹(1)| = o(n). Then for every k ≥ 1 and ε > 0, for all large n, Σ₃^k(f n) ≥ 2 ^ ((1/k - ε) n).

theorem Complexity.eventually_two_rpow_le_piThreeSize {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 = false} (D n)) (hdense : (fun (n : ℕ) => ↑n * Real.log 2 - Real.log ↑{x : BitString n | f n x = false}.ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) {k : ℕ} (hk : 1 ≤ k) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ ((1 / ↑k - ε) * ↑n) ≤ ↑(piThreeSize k (f n))

Π₃^k lower bound. If the rejected sets of f eventually contain no subcube of dimension D n = o(n) and have logarithmic density deficit o(n), then for every k ≥ 1 and ε > 0, for all large n, Π₃^k(f n) ≥ 2 ^ ((1/k - ε) n).

theorem Complexity.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 whose two sides have 2 ^ m elements each.

theorem Complexity.eventually_two_rpow_le_sigmaThreeSize_of_rectangleFree {f : (n : ℕ) → BitString n → Bool} {K : ℕ → ℕ} (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Frontier.RectangleFree {x : Fin n → Bool | f n x = true} (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑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))

Σ₃^k lower bound for rectangle-free families. Under the hypotheses of the frontier method (accepted sets eventually K n-rectangle-free with log K = o(n), and logarithmic density deficit o(n)), for every k ≥ 1 and ε > 0, for all large n, Σ₃^k(f n) ≥ 2 ^ ((1/k - ε) n).