Average-case circuit lower bounds

Rectangle bias 2 b bounds the agreement of circuits of size (1 + 1/A - ε)n by 1/2 + b + 2^(-γ n) for every 0 < γ < min(1, A ε). The theorem includes the compiler, weighted peeling, unused inputs, and the layout comparison. Only the extractor's bias hypothesis is external.

theorem Complexity.Frontier.averageCase {A ε γ : ℝ} (hA : 0 < A) (hlayout : LayoutBound 3 A) (hε : 0 < ε) (hγ1 : γ < 1) (hγε : γ < A * ε) (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, RectangleBias (f n) (K n) (2 * b 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 + 1 / A - ε) * ↑n → (agreement (f n) fun (x : Fin n → Bool) => c.eval I x 0) ≤ 1 / 2 + b n + 2 ^ (-γ * ↑n)

Average-case frontier lower bound. Bias 2 b_n on all sufficiently large coordinate rectangles bounds agreement with every binary circuit a fixed linear distance below L n. The exponential rate can be any γ < min(1, A ε).

theorem Complexity.Frontier.averageCase_abs {A ε γ : ℝ} (hA : 0 < A) (hlayout : LayoutBound 3 A) (hε : 0 < ε) (hγ1 : γ < 1) (hγε : γ < A * ε) (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, RectangleBias (f n) (K n) (2 * b 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 + 1 / A - ε) * ↑n → |(2 * agreement (f n) fun (x : Fin n → Bool) => c.eval I x 0) - 1| ≤ 2 * b n + 2 * 2 ^ (-γ * ↑n)

The same theorem bounds absolute signed correlation, with the correct normalization.

theorem Complexity.Frontier.averageCase_gaussian {ε : ℝ} (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, RectangleBias (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)

The Gaussian average-case bound. At every fixed linear gap below L = 4.562497..., rectangle bias 2 b_n bounds agreement by 1/2 + b_n + 2^(-Ω(n)).