Average-case hardness from sumset bias

The flat-source hypothesis below is the part of the sumset-extractor guarantee used by the proof: independent uniform sources on any two sets of size at least K have XOR output bias at most β. A one-bit extractor of statistical error b supplies β = 2 b. No explicit extractor construction or polynomial-time evaluation is assumed to be formalized.

def Complexity.Frontier.xorInputs {ι : Type u_3} (x y : ι → Bool) : ι → Bool

Coordinatewise XOR of two Boolean inputs.

Equations

• Complexity.Frontier.xorInputs x y i = (x i ^^ y i)

def Complexity.Frontier.FlatSumsetBias {ι : Type u_3} [Finite ι] (f : (ι → Bool) → Bool) (K : ℕ) (bias : ℝ) : Prop

The signed-bias guarantee for sums of two independent uniform (flat) sources.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Frontier.FlatSumsetBias.affine_pullback {ι : Type u_3} {κ : Type u_4} [Finite ι] [Finite κ] {f : (ι → Bool) → Bool} {K : ℕ} {bias : ℝ} (hf : FlatSumsetBias f K bias) (L : (κ → Bool) → ι → Bool) (hL : Function.Injective L) (hadd : ∀ (x y : κ → Bool), L (xorInputs x y) = xorInputs (L x) (L y)) (a : ι → Bool) : FlatSumsetBias (fun (x : κ → Bool) => f (xorInputs a (L x))) K bias

Sumset bias survives an injective affine change of input coordinates. The two independent sources are mapped separately, putting the translation in the first one. This permits affine preparation of a circuit without changing the target's bias bound.

theorem Complexity.Frontier.FlatSumsetBias.rectangleBias {ι : Type u_3} [Finite ι] {f : (ι → Bool) → Bool} {K : ℕ} {bias : ℝ} (hf : FlatSumsetBias f K bias) : RectangleBias f K bias

Sumset bias implies the required coordinate-rectangle bias, without entropy loss.

theorem Complexity.Frontier.averageCase_sumset {ε : ℝ} (hε : 0 < ε) (f : (n : ℕ) → (Fin n → Bool) → Bool) (K : ℕ → ℕ) (b : ℕ → ℝ) (hK2 : ∀ᶠ (n : ℕ) in Filter.atTop, 1 < K n) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hb : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ b n) (hf : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetBias (f n) (K n) (2 * b n)) : ∃ (γ : ℝ), 0 < γ ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost 2 → ↑c.innerSize ≤ (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n → (agreement (f n) fun (x : Fin n → Bool) => c.eval I x 0) ≤ 1 / 2 + b n + 2 ^ (-γ * ↑n)

Average-case lower bound for sumset extractors, in the flat-source form used here.

theorem Complexity.Frontier.averageCase_sumset_polynomial {ε : ℝ} (hε : 0 < ε) (f : (n : ℕ) → (Fin n → Bool) → Bool) (K : ℕ → ℕ) (b : ℕ → ℝ) (hK2 : ∀ᶠ (n : ℕ) in Filter.atTop, 1 < K n) (hK : (fun (n : ℕ) => Real.log ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (hb : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ b n) (hf : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetBias (f n) (K n) (2 * b n)) {α C : ℝ} (hpoly : ∀ᶠ (n : ℕ) in Filter.atTop, b n ≤ C * ↑n ^ (-α)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ Bool) (c : Cslib.Circuits.Circuit σ n 1), c.FanInAtMost 2 → ↑c.innerSize ≤ (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑n → (agreement (f n) fun (x : Fin n → Bool) => c.eval I x 0) ≤ 1 / 2 + (C + 1) * ↑n ^ (-α)

Polynomially small extractor error gives polynomially small agreement advantage. The entropy hypothesis is still only log K = o(n), allowing polylogarithmic entropy. The exponent α may be any real number; a positive exponent gives the intended decay.