Average-case frontier lower bounds

Let S ⊆ U^n have density within b of 1/2 on rectangles with both sides of size at least K (RectangleBias). A circuit splits the inputs into those it accepts and those it rejects, and each part is the accepted set of a constraint network whose branching program is unambiguous. Peeling (Cslib.Circuits.Frontier.Network.abs_signedCount_accepted_le) shows that on each part, too, the density of S is within b of 1/2, up to a residual of (K - 1) ^ 2 times the size of the program. So the circuit agrees with S on at most a 1/2 + b fraction of the inputs plus the residual (agreement_le_of_layout). A circuit that leaves inputs carrying K assignments unread is handled directly (agreement_le_of_unread).

Below (1 + 1/A - ε) n inner gates, the layout hypothesis LayoutBound 3 A makes the program exponentially smaller than the |U| ^ n inputs (eventually_add_lt_of_le), so the residual is an exponentially small fraction (averageCaseBound_of_layoutBound).

The average-case claim (AverageCaseBound L). For every ε > 0 there is a γ > 0, uniform over the alphabet and all admissible families, such that every circuit of fan-in at most two with at most (L - ε) n gates of positive arity agrees with S_n on at most a 1/2 + b_n + exp (-γ n) fraction of inputs, whenever S_n has bias at most b_n on rectangles with both sides of size at least K_n and log K_n = o(n).

Main definitions

• Cslib.Circuits.Frontier.agreement S T: the fraction of inputs on which membership in S and in T agree.
• Cslib.Circuits.Frontier.correlation S T: agreement minus disagreement.
• Cslib.Circuits.Frontier.AverageCaseBound L: the average-case claim with coefficient L.

Main results

• Cslib.Circuits.Frontier.correlation_eq_two_mul_agreement_sub_one: on finite inputs over a nonempty alphabet, correlation is twice agreement minus one.
• Cslib.Circuits.Frontier.correlation_mul_card_eq_sum: correlation as a signed sum.
• Cslib.Circuits.Frontier.agreement_le: agreement from the bias on a set and its complement.
• Cslib.Circuits.Frontier.agreement_le_of_layout, Cslib.Circuits.Frontier.agreement_le_of_unread: the agreement of one circuit.
• Cslib.Circuits.Frontier.averageCaseBound_of_layoutBound: the average-case claim with coefficient 1 + 1/A under the layout hypothesis LayoutBound 3 A.

noncomputable def Cslib.Circuits.Frontier.agreement {ι : Type u_1} {U : Type u_2} (S T : Set (ι → U)) : ℝ

The agreement of two sets of inputs: the fraction of inputs on which membership in S and membership in T agree.

Correlation

noncomputable def Cslib.Circuits.Frontier.correlation {ι : Type u_1} {U : Type u_2} (S T : Set (ι → U)) : ℝ

The correlation of two sets of inputs: the fraction of inputs on which membership in S and membership in T agree, minus the fraction on which it differs.

@[simp]

theorem Cslib.Circuits.Frontier.correlation_compl_right {ι : Type u_1} {U : Type u_2} (S T : Set (ι → U)) : correlation S Tᶜ = -correlation S T

Complementing the second set negates the correlation.

theorem Cslib.Circuits.Frontier.agreement_add_agreement_compl {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] [Nonempty U] (S T : Set (ι → U)) : agreement S T + agreement S Tᶜ = 1

Membership in S agrees with membership in T or with membership in Tᶜ.

theorem Cslib.Circuits.Frontier.correlation_eq_two_mul_agreement_sub_one {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] [Nonempty U] (S T : Set (ι → U)) : correlation S T = 2 * agreement S T - 1

Correlation and agreement. The correlation of S and T is 2 · agreement S T - 1.

theorem Cslib.Circuits.Frontier.abs_correlation_le_one {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] [Nonempty U] (S T : Set (ι → U)) : |correlation S T| ≤ 1

The correlation is at most one in absolute value.

theorem Cslib.Circuits.Frontier.agreement_le_of_abs_correlation_le {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] [Nonempty U] {S T : Set (ι → U)} {ε : ℝ} (h : |correlation S T| ≤ ε) : agreement S T ≤ 1 / 2 + ε / 2

A correlation of absolute value at most ε is an agreement of at most (1 + ε) / 2.

theorem Cslib.Circuits.Frontier.correlation_mul_card_eq_sum {ι : Type u_1} {U : Type u_2} [Fintype ι] [Fintype U] [DecidableEq ι] [Nonempty U] (S T : Set (ι → U)) [DecidablePred fun (x : ι → U) => x ∈ S] [DecidablePred fun (x : ι → U) => x ∈ T] : correlation S T * ↑(Fintype.card (ι → U)) = ∑ x : ι → U, if x ∈ S ↔ x ∈ T then 1 else -1

The correlation, scaled by the number of inputs, is the sum of ±1 over the inputs: +1 where membership in S and in T agree and -1 where it differs.

theorem Cslib.Circuits.Frontier.agreement_le {ι : Type u_1} {U : Type u_2} [Finite ι] [Finite U] [Nonempty U] {S T : Set (ι → U)} {β R₁ R₂ : ℝ} (h₁ : |signedCount S T| ≤ β * ↑T.ncard + R₁) (h₂ : |signedCount S Tᶜ| ≤ β * ↑Tᶜ.ncard + R₂) : agreement S T ≤ (1 + β) / 2 + (R₁ + R₂) / (2 * ↑(Nat.card (ι → U)))

Agreement from bias. If S has bias at most β on T and on its complement, up to the residuals R₁ and R₂, then membership in S and in T agree on at most a (1 + β)/2 + (R₁ + R₂)/(2 N) fraction of the N inputs.

theorem Cslib.Circuits.Frontier.accepted_network_eq_eval {U : Type u} {σ : Signature} {n : ℕ} (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ n 1) : (Compiler.network c I fun (x : Fin 1) => Acc).accepted = {x : Fin n → U | c.eval I x 0 ∈ Acc}

The inputs on which the output of a circuit lies in Acc are the accepted inputs of its constraint network.

theorem Cslib.Circuits.Frontier.agreement_le_of_unread {U : Type u} {σ : Signature} {n : ℕ} (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ n 1) [Finite U] [Nontrivial U] {S : Set (Fin n → U)} {K : ℕ} {b : ℝ} (hS : RectangleBias S K b) (hb : 0 ≤ b) (hK : 1 ≤ K) (hu : K ≤ Nat.card U ^ (Compiler.network c I fun (x : Fin 1) => Acc).readᶜ.ncard) : agreement S {x : Fin n → U | c.eval I x 0 ∈ Acc} ≤ 1 / 2 + b + ↑(Nat.card U * K ^ 2) / ↑(Nat.card U) ^ n

A circuit that leaves many inputs unread. If the inputs a circuit does not read carry at least K ≥ 1 assignments, it agrees with a set S of bias at most b ≥ 0 on large rectangles on at most a 1/2 + b + |U| K ^ 2 / |U| ^ n fraction of the inputs.

theorem Cslib.Circuits.Frontier.agreement_le_of_layout {U : Type u} {σ : Signature} {n : ℕ} (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ n 1) [Finite U] [Nontrivial U] {S : Set (Fin n → U)} {K : ℕ} {b : ℝ} (hS : RectangleBias S K b) (hb : 0 ≤ b) (hfan : c.FanInAtMost 2) (hu : Nat.card U ^ (Compiler.network c I fun (x : Fin 1) => Acc).readᶜ.ncard < K) (π : Layout (Compiler.Vertex c)) {w : ℕ} (hw : (Compiler.graph c).width π ≤ w) : agreement S {x : Fin n → U | c.eval I x 0 ∈ Acc} ≤ 1 / 2 + b + ↑(K ^ 3 * (Nat.card (Compiler.Vertex c) + 1) * Nat.card U ^ (w + 4)) / ↑(Nat.card U) ^ n

A circuit with a narrow layout. Let the inputs a circuit of fan-in at most two does not read carry fewer than K assignments, and let a layout of its graph have width at most w. Then the circuit agrees with a set S of bias at most b ≥ 0 on large rectangles on at most a 1/2 + b + K ^ 3 (|V| + 1) |U| ^ (w + 4) / |U| ^ n fraction of the inputs.

theorem Cslib.Circuits.Frontier.exists_layout_le {U : Type u} {σ : Signature} {n : ℕ} (I : Interpretation σ U) (Acc : Set U) (c : Circuit σ n 1) [Finite U] [Nontrivial U] {A η C : ℝ} (hAη : 0 ≤ A + η) (hC : ∀ (V E : Type) [Finite V] [inst : Finite E] (G : Multigraph V E), G.toSimpleGraph.Connected → G.Loopless → G.MaxDegreeLE 3 → ∃ (π : Layout V), ↑(G.width π) ≤ (A + η) * ↑G.cycleRank + η * ↑(Nat.card V) + C) (hfan : c.FanInAtMost 2) {K : ℕ} (hu : Nat.card U ^ (Compiler.network c I fun (x : Fin 1) => Acc).readᶜ.ncard < K) : ∃ (π : Layout (Compiler.Vertex c)), ↑((Compiler.graph c).width π) ≤ (A + η) * (↑c.innerSize - ↑n + Real.logb ↑(Nat.card U) ↑K + 1) + η * ↑(Nat.card (Compiler.Vertex c)) + C

A narrow layout of a circuit. Suppose that connected, loopless multigraphs of maximum degree three have layouts of width at most (A + η) β₁ + η |V| + C. If the inputs a circuit of fan-in at most two does not read carry fewer than K assignments, its graph has a layout of width at most (A + η) (s - n + log_q K + 1) + η |V| + C for s inner gates.

def Cslib.Circuits.Frontier.AverageCaseBound (L : ℝ) : Prop

The average-case claim with coefficient L. For every ε > 0 there is a γ > 0 such that the following holds for every finite alphabet U with at least two symbols. Let S_n ⊆ U^n have density within b_n of 1/2 on every rectangle with both sides of size at least K_n (RectangleBias), where log K_n = o(n). Then for all large n, every circuit of fan-in at most two with at most (L - ε) n gates of positive arity, over any basis on U and accepting any set of values, agrees with S_n on at most a 1/2 + b_n + exp (-γ n) fraction of the inputs.

The alphabet lives in the universe u and the basis in the universe v.

theorem Cslib.Circuits.Frontier.AverageCaseBound.mono {L L' : ℝ} (h : AverageCaseBound L) (hL : L' ≤ L) : AverageCaseBound L'

An average-case bound holds for every smaller coefficient.

theorem Cslib.Circuits.Frontier.averageCaseBound_of_layoutBound {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound 3 A) : AverageCaseBound (1 + 1 / A)

The average-case frontier lower bound. If subcubic graphs have layouts of width (A + o(1)) β₁ + o(|V|) (LayoutBound 3 A), then the average-case claim holds with coefficient 1 + 1/A: below (1 + 1/A - ε) n inner gates, a circuit of fan-in at most two agrees with a set of bias at most b_n on large rectangles on at most a 1/2 + b_n + exp (-γ n) fraction of the inputs.