Demand and supply at the frontier

Every lower bound proved by the frontier method ends with the same comparison. On one side is the demand of the problem: every layout of the graph of a circuit for it must, at some time, have a frontier of about n edges, the information that must cross from the inputs read to the inputs not yet read. On the other side is the supply of the layout hypothesis (Cslib.Circuits.Frontier.LayoutBound): the graph of a circuit of size s has cycle rank about s - n, so it has a layout whose frontiers carry at most about A (s - n) edges. Demand cannot exceed supply, so n ≤ A (s - n), that is, s ≥ (1 + 1/A) n.

eventually_lt_of_demand makes this precise with every lower-order term in place. The slack η of the layout hypothesis is chosen first, depending only on A, ε, and a constant κ bounding the size of the graph; the constant C of the layout hypothesis and the error e(n) = o(n) of the problem come afterwards.

The average-case lower bounds need the comparison with a margin (eventually_add_lt_of_le): below (1 + 1/A - ε) n gates, the frontier, the error and the logarithmic term fall short of n by a linear amount, which makes the counting residual an exponentially small fraction of the inputs.

Main results

• Cslib.Circuits.Frontier.eventually_lt_of_demand: demand n - o(n) and supply A (s - n + o(n)) + o(n) force s > (1 + 1/A - ε) n.
• Cslib.Circuits.Frontier.eventually_add_lt_of_le: demand with a margin.
• Cslib.Circuits.Frontier.isLittleO_log_affine: log (α n + β) = o(n).
• Cslib.Circuits.Frontier.logb_le_mul_log: changing from base q ≥ 2 to the natural logarithm.

theorem Cslib.Circuits.Frontier.isLittleO_log_affine {α β : ℝ} (hα : 0 ≤ α) (hβ : 1 ≤ β) : (fun (n : ℕ) => Real.log (α * ↑n + β)) =o[Filter.atTop] fun (n : ℕ) => ↑n

log (α n + β) = o(n) for constants α ≥ 0 and β ≥ 1.

theorem Cslib.Circuits.Frontier.logb_le_mul_log {q x : ℝ} (hq : 2 ≤ q) (hx : 1 ≤ x) : Real.logb q x ≤ (4 + 1 / Real.log 2) * Real.log x

Changing from base q ≥ 2 to the natural logarithm costs at most the factor 1 / log 2 ≤ 4 + 1 / log 2.

theorem Cslib.Circuits.Frontier.eventually_lt_of_demand {A : ℝ} (hA : 0 < A) {κ : ℝ} (hκ : 0 ≤ κ) {ε : ℝ} (hε : 0 < ε) : ∃ η₀ > 0, ∀ (η : ℝ), 0 < η → η ≤ η₀ → ∀ (C : ℝ) (e : ℕ → ℝ), (e =o[Filter.atTop] fun (n : ℕ) => ↑n) → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s v w : ℝ), 0 ≤ s → 0 ≤ v → v ≤ κ * (↑n + s + 1) → ↑n ≤ w + e n + κ * Real.log (v + 1) → w ≤ (A + η) * (s - ↑n + e n) + η * v + C → (1 + 1 / A - ε) * ↑n < s

Demand and supply at the frontier. Fix A > 0, ε > 0, and a constant κ ≥ 0. For every small enough slack η > 0, every constant C, and every error e(n) = o(n), for all large n the following holds. If a graph with v ≤ κ (n + s + 1) vertices has a layout of width w that is

• at least the demand: n ≤ w + e(n) + κ log (v + 1), and
• at most the supply: w ≤ (A + η) (s - n + e(n)) + η v + C,

then s > (1 + 1/A - ε) n.

In applications, s is (r - 1) times the number of gates of a circuit of fan-in r, the supply is the layout hypothesis applied to a graph of cycle rank at most s - n + e(n), and the demand is a counting argument for the problem. The slack is chosen before the layout hypothesis provides C.

theorem Cslib.Circuits.Frontier.eventually_add_lt_of_le {A : ℝ} (hA : 0 < A) {κ : ℝ} (hκ : 0 ≤ κ) {ε : ℝ} (hε : 0 < ε) : ∃ η > 0, ∀ (C : ℝ) (e : ℕ → ℝ), (e =o[Filter.atTop] fun (n : ℕ) => ↑n) → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s v w : ℝ), 0 ≤ s → 0 ≤ v → v ≤ κ * (↑n + s + 1) → s ≤ (1 + 1 / A - ε) * ↑n → w ≤ (A + η) * (s - ↑n + e n) + η * v + C → w + e n + κ * Real.log (v + 1) < (1 - A * ε / 2) * ↑n

Demand with a margin. Below (1 + 1/A - ε) n, the frontier, the error, and the logarithmic term fall short of n by the linear margin A ε n / 2: for some slack η > 0, every constant C, and every error e(n) = o(n), for all large n, if s ≤ (1 + 1/A - ε) n, v ≤ κ (n + s + 1), and w ≤ (A + η) (s - n + e(n)) + η v + C, then

w + e(n) + κ log (v + 1) < (1 - A ε / 2) n.

This is the comparison eventually_lt_of_demand with ε / 2, applied to the frontier w + A ε n / 2 and the gate budget s + (A ε n / 2) / (A + η).