Hard sets from sumset dispersers

The lower bound needs dense rectangle-free sets. Over an alphabet U with an addition, a rectangle is a sumset: an input whose part on X lies in A and whose part on the complement of X lies in B is the sum a + b of the input a that agrees with it on X and vanishes elsewhere, and the input b that agrees with it off X and vanishes on X. So a function that is not constant on any sumset A + B of two large sets of inputs has rectangle-free fibers (Frontier.SumsetDisperser.rectangleFree).

Such functions are sumset dispersers. A sumset extractor is better: its output on X + Y, for independent random inputs X and Y with enough min-entropy, is close to uniform. An extractor with error less than 1/2 disperses sumsets. Over a finite additive group its fibers are dense, since X + Y is uniform when X and Y are.

For U = {0, 1} with addition modulo two, polynomial-time computable extractors for the sum of two independent sources of min-entropy c log n are known (Xin Li, Two source extractors for asymptotically optimal entropy, and (many) more, FOCS 2023, Theorem 7.13). Their fibers are dense and n^c-rectangle-free, so Frontier.lowerBound_sumsetDisperser applies to them: there is a language in P whose circuits of fan-in two over any binary basis need (L - ε) n gates, with L ≈ 4.5625. The extractor itself is not formalized here.

Main definitions

• Frontier.SumsetDisperser f K: f takes both values on every sumset of two sets of size at least K.

Main results

• Frontier.SumsetDisperser.rectangleFree: the fibers of a sumset disperser are rectangle-free.
• Frontier.lowerBound_sumsetDisperser: the (L - ε) n lower bound for balanced sumset dispersers.

def Complexity.Frontier.SumsetDisperser {ι : Type u_1} {U : Type u_2} [Add U] (f : (ι → U) → Bool) (K : ℕ) : Prop

A function f disperses sumsets of size K when it takes both values on the sumset A + B of any two sets of inputs with at least K elements each.

Equations

• Complexity.Frontier.SumsetDisperser f K = ∀ (A B : Set (ι → U)), K ≤ A.ncard → K ≤ B.ncard → ∀ (b : Bool), ∃ x ∈ A, ∃ y ∈ B, f (x + y) ≠ b

noncomputable def Complexity.Frontier.pad {ι : Type u_1} {U : Type u_2} [Zero U] (X : Set ι) (a : ↑X → U) : ι → U

The input that agrees with a on X and vanishes elsewhere.

Equations

• Complexity.Frontier.pad X a i = if h : i ∈ X then a ⟨i, h⟩ else 0

theorem Complexity.Frontier.pad_injective {ι : Type u_1} {U : Type u_2} [Zero U] (X : Set ι) : Function.Injective (pad X)

theorem Complexity.Frontier.domRestrict_pad_add_pad {ι : Type u_1} {U : Type u_2} [AddZeroClass U] (X : Set ι) (a : ↑X → U) (b : ↑Xᶜ → U) : X.domRestrict (pad X a + pad Xᶜ b) = a ∧ Xᶜ.domRestrict (pad X a + pad Xᶜ b) = b

theorem Complexity.Frontier.SumsetDisperser.rectangleFree {ι : Type u_1} {U : Type u_2} [AddZeroClass U] {f : (ι → U) → Bool} {K : ℕ} (hf : SumsetDisperser f K) (b : Bool) : RectangleFree {x : ι → U | f x = b} K

The fibers of a sumset disperser are rectangle-free. A rectangle with sides A and B is the sumset of the inputs supported on X with parts in A and those supported off X with parts in B.

theorem Complexity.Frontier.isLittleO_of_card_le {U : Type u_2} [Finite U] [Nonempty U] (S : (n : ℕ) → Set (Fin n → U)) {δ : ℝ} (hδ : 0 < δ) (hS : ∀ᶠ (n : ℕ) in Filter.atTop, δ * ↑(Nat.card U) ^ n ≤ ↑(S n).ncard) : (fun (n : ℕ) => ↑n * Real.log ↑(Nat.card U) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n

A set containing at least a fixed fraction of all inputs is dense: n log |U| - log |S_n| = O(1).

theorem Complexity.Frontier.lowerBound_sumsetDisperser {U : Type u} [AddZeroClass U] [Finite U] [Nontrivial U] (f : (n : ℕ) → (Fin n → U) → Bool) (K : ℕ → ℕ) (hf : ∀ᶠ (n : ℕ) in Filter.atTop, SumsetDisperser (f n) (K n)) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {δ : ℝ} (hδ : 0 < δ) (hbal : ∀ᶠ (n : ℕ) in Filter.atTop, δ * ↑(Nat.card U) ^ n ≤ ↑{x : Fin n → U | f n x = true}.ncard) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (Acc : Set U) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost 2 → Decides c I Acc {x : Fin n → U | f n x = true} → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n < ↑c.size

The (L - ε) n lower bound for sumset dispersers. Let f_n be functions on U^n, over a finite alphabet with an addition, that disperse sumsets of size K_n with log K_n = o(n) and take the value true on at least a fixed fraction δ > 0 of all inputs. Then for every ε > 0 and all large n, every circuit of fan-in two over any basis on U deciding where f_n is true has more than (L - ε) n gates, with L = 1 + π / (3 arccos ((1 + 2√2)/4)) ≈ 4.5625.