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: 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.

Frontier.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.

Main results

• Frontier.eventually_lt_of_demand: demand n - o(n) and supply A (s - n + o(n)) + o(n) force s > (1 + 1/A - ε) n.
• Frontier.isLittleO_log_affine: log (α n + β) = o(n).

theorem Complexity.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 Complexity.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.